diff --git a/lisa/gradle.properties b/lisa/gradle.properties index 114baa7bf..0d9b3f0eb 100644 --- a/lisa/gradle.properties +++ b/lisa/gradle.properties @@ -1,6 +1,6 @@ # project properties group = 'it.unive' -version = 0.1b9 +version = 0.1 # gradle build properties org.gradle.caching=true diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java index 36249a0a5..1bfd6aabf 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java @@ -259,7 +259,8 @@ public ExpressionSet visit( ProgramPoint pp = (ProgramPoint) params[0]; SemanticOracle oracle = (SemanticOracle) params[1]; - for (SymbolicExpression rec : receiver) + for (SymbolicExpression rec : receiver) { + rec = removeTypingExpressions(rec); if (rec instanceof MemoryPointer) { MemoryPointer pid = (MemoryPointer) rec; for (Type t : oracle.getRuntimeTypesOf(pid, pp, oracle)) @@ -270,6 +271,7 @@ public ExpressionSet visit( result.add(e); } } + } return new ExpressionSet(result); } @@ -298,7 +300,8 @@ public ExpressionSet visit( ProgramPoint pp = (ProgramPoint) params[0]; SemanticOracle oracle = (SemanticOracle) params[1]; - for (SymbolicExpression refExp : ref) + for (SymbolicExpression refExp : ref) { + refExp = removeTypingExpressions(refExp); if (refExp instanceof HeapLocation) { Set rt = oracle.getRuntimeTypesOf(refExp, pp, oracle); Type sup = Type.commonSupertype(rt, Untyped.INSTANCE); @@ -308,6 +311,7 @@ public ExpressionSet visit( refExp.getCodeLocation()); result.add(e); } + } return new ExpressionSet(result); } @@ -323,6 +327,7 @@ public ExpressionSet visit( SemanticOracle oracle = (SemanticOracle) params[1]; for (SymbolicExpression derefExp : deref) { + derefExp = removeTypingExpressions(derefExp); if (derefExp instanceof Variable) { Variable var = (Variable) derefExp; for (Type t : oracle.getRuntimeTypesOf(var, pp, oracle)) diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSite.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSite.java index 8bedbcfa7..dc4eb8835 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSite.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSite.java @@ -179,4 +179,14 @@ public String getField() { */ public abstract AllocationSite withField( SymbolicExpression field); + + /** + * Yields a modified version of this allocation site with the given type. + * + * @param type the new type + * + * @return the modified allocation site + */ + public abstract AllocationSite withType( + Type type); } diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java index a6dc81e94..dacd85a57 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java @@ -320,7 +320,8 @@ public ExpressionSet visit( Object... params) throws SemanticException { Set result = new HashSet<>(); - for (SymbolicExpression rec : receiver) + for (SymbolicExpression rec : receiver) { + rec = removeTypingExpressions(rec); if (rec instanceof MemoryPointer) { MemoryPointer pid = (MemoryPointer) rec; AllocationSite site = (AllocationSite) pid.getReferencedLocation(); @@ -347,7 +348,8 @@ public ExpressionSet visit( result.add(e); } else if (rec instanceof AllocationSite) - result.add(rec); + result.add(((AllocationSite) rec).withType(expression.getStaticType())); + } return new ExpressionSet(result); } @@ -387,7 +389,8 @@ public ExpressionSet visit( throws SemanticException { Set result = new HashSet<>(); - for (SymbolicExpression loc : arg) + for (SymbolicExpression loc : arg) { + loc = removeTypingExpressions(loc); if (loc instanceof AllocationSite) { AllocationSite allocSite = (AllocationSite) loc; MemoryPointer e = new MemoryPointer( @@ -403,6 +406,7 @@ public ExpressionSet visit( result.add(e); } else result.add(loc); + } return new ExpressionSet(result); } @@ -414,7 +418,8 @@ public ExpressionSet visit( throws SemanticException { Set result = new HashSet<>(); - for (SymbolicExpression ref : arg) + for (SymbolicExpression ref : arg) { + ref = removeTypingExpressions(ref); if (ref instanceof MemoryPointer) result.add(((MemoryPointer) ref).getReferencedLocation()); else if (ref instanceof Identifier) { @@ -444,6 +449,7 @@ else if (id.getStaticType().isInMemoryType() || id.getStaticType().isUntyped()) } } else result.add(ref); + } return new ExpressionSet(result); } diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/FieldSensitivePointBasedHeap.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/FieldSensitivePointBasedHeap.java index 368bf3736..0d230d787 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/FieldSensitivePointBasedHeap.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/FieldSensitivePointBasedHeap.java @@ -288,7 +288,8 @@ public ExpressionSet visit( throws SemanticException { Set result = new HashSet<>(); - for (SymbolicExpression rec : receiver) + for (SymbolicExpression rec : receiver) { + rec = removeTypingExpressions(rec); if (rec instanceof MemoryPointer) { AllocationSite site = (AllocationSite) ((MemoryPointer) rec).getReferencedLocation(); populate(expression, child, result, site); @@ -296,6 +297,7 @@ public ExpressionSet visit( AllocationSite site = (AllocationSite) rec; populate(expression, child, result, site); } + } return new ExpressionSet(result); } diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/HeapAllocationSite.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/HeapAllocationSite.java index ceab14071..e2f618032 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/HeapAllocationSite.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/HeapAllocationSite.java @@ -88,4 +88,10 @@ public AllocationSite withField( throw new IllegalStateException("Cannot add a field to an allocation site that already has one"); return new HeapAllocationSite(getStaticType(), getLocationName(), field, isWeak(), getCodeLocation()); } + + @Override + public AllocationSite withType( + Type type) { + return new HeapAllocationSite(type, getLocationName(), getField(), isWeak(), getCodeLocation()); + } } \ No newline at end of file diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/StackAllocationSite.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/StackAllocationSite.java index 5eac7631b..228a3f1ce 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/StackAllocationSite.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/StackAllocationSite.java @@ -88,4 +88,10 @@ public AllocationSite withField( throw new IllegalStateException("Cannot add a field to an allocation site that already has one"); return new StackAllocationSite(getStaticType(), getLocationName(), field, isWeak(), getCodeLocation()); } + + @Override + public AllocationSite withType( + Type type) { + return new StackAllocationSite(type, getLocationName(), getField(), isWeak(), getCodeLocation()); + } } diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/TestParameterProvider.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/TestParameterProvider.java index 9058aba21..3e9340218 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/TestParameterProvider.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/TestParameterProvider.java @@ -271,16 +271,22 @@ public static R provideParam( return (R) new ValueEnvironment<>(new SampleNRVD()); if (param == SampleNRVD.class || param == BaseNonRelationalValueDomain.class) return (R) new SampleNRVD(); + if (param == BaseNonRelationalValueDomain[].class) + return (R) new BaseNonRelationalValueDomain[0]; if (param == InferenceSystem.class) return (R) new InferenceSystem<>(new SampleIV()); if (param == SampleIV.class || param == BaseInferredValue.class) return (R) new SampleIV(); + if (param == BaseInferredValue[].class) + return (R) new BaseInferredValue[0]; if (param == TypeEnvironment.class) return (R) new TypeEnvironment<>(new SampleNRTD()); if (param == SampleNRTD.class || param == BaseNonRelationalTypeDomain.class) return (R) new SampleNRTD(); + if (param == BaseNonRelationalTypeDomain[].class) + return (R) new BaseNonRelationalTypeDomain[0]; if (param == SemanticOracle.class) return (R) DefaultConfiguration.defaultAbstractState(); diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeapTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeapTest.java index 30fe7b279..e752086b2 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeapTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeapTest.java @@ -17,6 +17,7 @@ import it.unive.lisa.program.cfg.CodeLocation; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.program.type.Int32Type; +import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.heap.AccessChild; import it.unive.lisa.symbolic.heap.HeapDereference; import it.unive.lisa.symbolic.heap.HeapExpression; @@ -29,7 +30,9 @@ import it.unive.lisa.symbolic.value.OutOfScopeIdentifier; import it.unive.lisa.symbolic.value.Variable; import it.unive.lisa.symbolic.value.operator.binary.NumericNonOverflowingAdd; +import it.unive.lisa.symbolic.value.operator.binary.TypeConv; import it.unive.lisa.type.Type; +import it.unive.lisa.type.TypeTokenType; import it.unive.lisa.type.Untyped; import java.util.Collections; import java.util.HashSet; @@ -459,4 +462,21 @@ public void testHeapDereferenceRewrite() throws SemanticException { expectedRewritten = new ExpressionSet(expectedUnknownAlloc); assertEquals(expectedRewritten, xAssign.rewrite(deref, pp1, fakeOracle)); } + + @Test + public void testIssue300() throws SemanticException { + // ((type) x) rewritten in x -> pp1 -> pp1 + PointBasedHeap xAssign = topHeap.assign(x, + new HeapReference(untyped, + new MemoryAllocation(untyped, loc1), loc1), + pp1, fakeOracle); + SymbolicExpression e = new AccessChild(intType, + new BinaryExpression(untyped, + new Constant(new TypeTokenType(Collections.singleton(intType)), intType, loc1), x, + TypeConv.INSTANCE, + loc1), + new Constant(intType, 1, loc1), loc1); + ExpressionSet expectedRewritten = new ExpressionSet(alloc1); + assertEquals(expectedRewritten, xAssign.rewrite(e, pp1, fakeOracle)); + } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/heap/BaseHeapDomain.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/heap/BaseHeapDomain.java index 736626be6..82c593771 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/heap/BaseHeapDomain.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/heap/BaseHeapDomain.java @@ -18,6 +18,8 @@ import it.unive.lisa.symbolic.value.TernaryExpression; import it.unive.lisa.symbolic.value.UnaryExpression; import it.unive.lisa.symbolic.value.ValueExpression; +import it.unive.lisa.symbolic.value.operator.TypeOperator; +import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator; import java.util.HashSet; import java.util.List; import java.util.Set; @@ -148,6 +150,28 @@ public abstract H semanticsOf( */ public abstract static class Rewriter implements ExpressionVisitor { + /** + * Extracts the inner expressions from casts/conversions. If {@code e} + * is of the form {@code (type) e1}, this method returns + * {@code removeTypingExpressions(e1)}. Otherwise, {@code e} is returned + * with no modifications. + * + * @param e the expression to strip from type operators + * + * @return the inner expression, if needed + */ + protected SymbolicExpression removeTypingExpressions( + SymbolicExpression e) { + if (e instanceof BinaryExpression) { + BinaryExpression be = (BinaryExpression) e; + BinaryOperator op = be.getOperator(); + if (op instanceof TypeOperator) + return removeTypingExpressions(be.getRight()); + } + + return e; + } + @Override public ExpressionSet visit( UnaryExpression expression, @@ -240,5 +264,25 @@ public ExpressionSet visit( throws SemanticException { return new ExpressionSet(expression); } + + @Override + public ExpressionSet visit( + HeapExpression expression, + ExpressionSet[] subExpressions, + Object... params) + throws SemanticException { + throw new SemanticException( + "No rewriting rule for heap expression of type " + expression.getClass().getName()); + } + + @Override + public ExpressionSet visit( + ValueExpression expression, + ExpressionSet[] subExpressions, + Object... params) + throws SemanticException { + throw new SemanticException( + "No rewriting rule for value expression of type " + expression.getClass().getName()); + } } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/inference/BaseInferredValue.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/inference/BaseInferredValue.java index e337eff7e..10054355b 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/inference/BaseInferredValue.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/inference/BaseInferredValue.java @@ -9,6 +9,7 @@ import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.heap.AccessChild; import it.unive.lisa.symbolic.heap.HeapDereference; +import it.unive.lisa.symbolic.heap.HeapExpression; import it.unive.lisa.symbolic.heap.HeapReference; import it.unive.lisa.symbolic.heap.MemoryAllocation; import it.unive.lisa.symbolic.value.BinaryExpression; @@ -30,6 +31,7 @@ import it.unive.lisa.symbolic.value.operator.unary.LogicalNegation; import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator; import it.unive.lisa.type.Type; +import java.lang.reflect.Array; import java.util.Set; /** @@ -68,6 +70,15 @@ public EvaluationVisitor( this.singleton = singleton; } + @Override + public InferredPair visit( + HeapExpression expression, + InferredPair[] subExpressions, + Object... params) + throws SemanticException { + throw new SemanticException(CANNOT_PROCESS_ERROR); + } + @Override public InferredPair visit( AccessChild expression, @@ -213,6 +224,29 @@ public InferredPair visit( (SemanticOracle) params[2]); } + @Override + public InferredPair visit( + ValueExpression expression, + InferredPair[] subExpressions, + Object... params) + throws SemanticException { + T[] subs = null; + if (subExpressions != null && subExpressions.length > 0) { + subs = (T[]) Array.newInstance(subExpressions[0].getInferred().getClass(), subExpressions.length); + for (int i = 0; i < subExpressions.length; i++) { + if (subExpressions[i].isBottom()) + return subExpressions[i]; + subs[i] = subExpressions[i].getInferred(); + } + } + + return singleton.evalValueExpression(expression, + subs, + ((InferenceSystem) params[0]).getExecutionState(), + (ProgramPoint) params[1], + (SemanticOracle) params[2]); + } + } @Override @@ -600,6 +634,41 @@ default InferredPair evalTernaryExpression( return new InferredPair<>(top, top, top); } + /** + * Yields the evaluation of a generic {@link ValueExpression}, where the + * recursive evaluation of its sub-expressions, if any, has already happened + * and is passed in the {@code subExpressions} parameters. It is guaranteed + * that no element of {@code subExpressions} is {@link #bottom()}.
+ *
+ * This method allows evaluating frontend-defined expressions. For all + * standard expressions defined within LiSA, the corresponding evaluation + * method will be invoked instead. + * + * @param expression the expression to evaluate + * @param subExpressions the instances of this domain representing the + * abstract values of all its sub-expressions, if + * any; if there are no sub-expressions, this + * parameter can be {@code null} or empty + * @param state the current execution state + * @param pp the program point that where this operation is + * being evaluated + * @param oracle the oracle for inter-domain communication + * + * @return the evaluation of the expression + * + * @throws SemanticException if an error occurs during the computation + */ + default InferredPair evalValueExpression( + ValueExpression expression, + T[] subExpressions, + T state, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + T top = top(); + return new InferredPair<>(top, top, top); + } + /** * Yields the satisfiability of an abstract value of type {@code }. * diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalTypeDomain.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalTypeDomain.java index 31a8a95ef..2d4a04018 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalTypeDomain.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalTypeDomain.java @@ -10,6 +10,7 @@ import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.heap.AccessChild; import it.unive.lisa.symbolic.heap.HeapDereference; +import it.unive.lisa.symbolic.heap.HeapExpression; import it.unive.lisa.symbolic.heap.HeapReference; import it.unive.lisa.symbolic.heap.MemoryAllocation; import it.unive.lisa.symbolic.value.BinaryExpression; @@ -71,6 +72,15 @@ public EvaluationVisitor( this.singleton = singleton; } + @Override + public T visit( + HeapExpression expression, + T[] subExpressions, + Object... params) + throws SemanticException { + throw new SemanticException(CANNOT_PROCESS_ERROR); + } + @Override public T visit( AccessChild expression, @@ -205,6 +215,21 @@ public T visit( return singleton.evalIdentifier(expression, (TypeEnvironment) params[0], (ProgramPoint) params[1], (SemanticOracle) params[2]); } + + @Override + public T visit( + ValueExpression expression, + T[] subExpressions, + Object... params) + throws SemanticException { + if (subExpressions != null) + for (T sub : subExpressions) + if (sub.isBottom()) + return sub; + + return singleton.evalValueExpression(expression, subExpressions, (ProgramPoint) params[1], + (SemanticOracle) params[2]); + } } @Override @@ -557,6 +582,38 @@ default T evalTernaryExpression( return top(); } + /** + * Yields the evaluation of a generic {@link ValueExpression}, where the + * recursive evaluation of its sub-expressions, if any, has already happened + * and is passed in the {@code subExpressions} parameters. It is guaranteed + * that no element of {@code subExpressions} is {@link #bottom()}.
+ *
+ * This method allows evaluating frontend-defined expressions. For all + * standard expressions defined within LiSA, the corresponding evaluation + * method will be invoked instead. + * + * @param expression the expression to evaluate + * @param subExpressions the instances of this domain representing the + * abstract values of all its sub-expressions, if + * any; if there are no sub-expressions, this + * parameter can be {@code null} or empty + * @param pp the program point that where this operation is + * being evaluated + * @param oracle the oracle for inter-domain communication + * + * @return the evaluation of the expression + * + * @throws SemanticException if an error occurs during the computation + */ + default T evalValueExpression( + ValueExpression expression, + T[] subExpressions, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return top(); + } + /** * Yields the satisfiability of an runtime types of type {@code }. * diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalValueDomain.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalValueDomain.java index 9ba2e9270..d0dd48081 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalValueDomain.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalValueDomain.java @@ -10,6 +10,7 @@ import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.heap.AccessChild; import it.unive.lisa.symbolic.heap.HeapDereference; +import it.unive.lisa.symbolic.heap.HeapExpression; import it.unive.lisa.symbolic.heap.HeapReference; import it.unive.lisa.symbolic.heap.MemoryAllocation; import it.unive.lisa.symbolic.value.BinaryExpression; @@ -73,6 +74,15 @@ public EvaluationVisitor( this.singleton = singleton; } + @Override + public T visit( + HeapExpression expression, + T[] subExpressions, + Object... params) + throws SemanticException { + throw new SemanticException(CANNOT_PROCESS_ERROR); + } + @Override public T visit( AccessChild expression, @@ -207,6 +217,21 @@ public T visit( return singleton.evalIdentifier(expression, (ValueEnvironment) params[0], (ProgramPoint) params[1], (SemanticOracle) params[2]); } + + @Override + public T visit( + ValueExpression expression, + T[] subExpressions, + Object... params) + throws SemanticException { + if (subExpressions != null) + for (T sub : subExpressions) + if (sub.isBottom()) + return sub; + + return singleton.evalValueExpression(expression, subExpressions, (ProgramPoint) params[1], + (SemanticOracle) params[2]); + } } @Override @@ -579,6 +604,38 @@ default T evalTernaryExpression( return top(); } + /** + * Yields the evaluation of a generic {@link ValueExpression}, where the + * recursive evaluation of its sub-expressions, if any, has already happened + * and is passed in the {@code subExpressions} parameters. It is guaranteed + * that no element of {@code subExpressions} is {@link #bottom()}.
+ *
+ * This method allows evaluating frontend-defined expressions. For all + * standard expressions defined within LiSA, the corresponding evaluation + * method will be invoked instead. + * + * @param expression the expression to evaluate + * @param subExpressions the instances of this domain representing the + * abstract values of all its sub-expressions, if + * any; if there are no sub-expressions, this + * parameter can be {@code null} or empty + * @param pp the program point that where this operation is + * being evaluated + * @param oracle the oracle for inter-domain communication + * + * @return the evaluation of the expression + * + * @throws SemanticException if an error occurs during the computation + */ + default T evalValueExpression( + ValueExpression expression, + T[] subExpressions, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return top(); + } + /** * Yields the satisfiability of an abstract value of type {@code }. * diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/symbolic/ExpressionVisitor.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/symbolic/ExpressionVisitor.java index 375294350..3b3d4263e 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/symbolic/ExpressionVisitor.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/symbolic/ExpressionVisitor.java @@ -3,6 +3,7 @@ import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.symbolic.heap.AccessChild; import it.unive.lisa.symbolic.heap.HeapDereference; +import it.unive.lisa.symbolic.heap.HeapExpression; import it.unive.lisa.symbolic.heap.HeapReference; import it.unive.lisa.symbolic.heap.MemoryAllocation; import it.unive.lisa.symbolic.value.BinaryExpression; @@ -13,6 +14,7 @@ import it.unive.lisa.symbolic.value.Skip; import it.unive.lisa.symbolic.value.TernaryExpression; import it.unive.lisa.symbolic.value.UnaryExpression; +import it.unive.lisa.symbolic.value.ValueExpression; /** * A visitor for {@link SymbolicExpression}s, to be used as parameter to @@ -26,6 +28,34 @@ */ public interface ExpressionVisitor { + /** + * Visits a generic {@link HeapExpression}. This callback is invoked after + * the inner expressions have been visited, and their produced value is + * passed as argument.
+ *
+ * This overload allows visiting frontend-defined expressions. For all + * standard expressions defined within LiSA, the corresponding overload will + * be invoked instead. + * + * @param expression the expression + * @param subExpressions the values produced by visiting the + * sub-expressions, if any; if there are no + * sub-expressions, this parameter can be + * {@code null} or empty + * @param params the additional parameters provided to + * {@link SymbolicExpression#accept(ExpressionVisitor, Object...)}, + * if any + * + * @return the value produced by visiting the expression + * + * @throws SemanticException if an error occurs during the visit operation + */ + T visit( + HeapExpression expression, + T[] subExpressions, + Object... params) + throws SemanticException; + /** * Visits an {@link AccessChild}. This callback is invoked after the inner * expressions have been visited, and their produced value is passed as @@ -108,6 +138,34 @@ T visit( Object... params) throws SemanticException; + /** + * Visits a generic {@link ValueExpression}. This callback is invoked after + * the inner expressions have been visited, and their produced value is + * passed as argument.
+ *
+ * This overload allows visiting frontend-defined expressions. For all + * standard expressions defined within LiSA, the corresponding overload will + * be invoked instead. + * + * @param expression the expression + * @param subExpressions the values produced by visiting the + * sub-expressions, if any; if there are no + * sub-expressions, this parameter can be + * {@code null} or empty + * @param params the additional parameters provided to + * {@link SymbolicExpression#accept(ExpressionVisitor, Object...)}, + * if any + * + * @return the value produced by visiting the expression + * + * @throws SemanticException if an error occurs during the visit operation + */ + T visit( + ValueExpression expression, + T[] subExpressions, + Object... params) + throws SemanticException; + /** * Visits a {@link UnaryExpression}. This callback is invoked after the * inner expressions have been visited, and their produced value is passed