From 3e450b78ff2c65812c45f113a016daa7c750cb82 Mon Sep 17 00:00:00 2001 From: Luca Negrini Date: Thu, 1 Aug 2024 10:18:06 +0200 Subject: [PATCH 1/5] Visiting for generic expressions #313 --- .../it/unive/lisa/TestParameterProvider.java | 6 ++ .../lisa/analysis/heap/BaseHeapDomain.java | 20 ++++++ .../inference/BaseInferredValue.java | 69 +++++++++++++++++++ .../value/BaseNonRelationalTypeDomain.java | 57 +++++++++++++++ .../value/BaseNonRelationalValueDomain.java | 57 +++++++++++++++ .../lisa/symbolic/ExpressionVisitor.java | 58 ++++++++++++++++ 6 files changed, 267 insertions(+) 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-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..b1ecce964 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 @@ -240,5 +240,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 From bfd3cebacd675256baf0d2670d35fe0c1540d948 Mon Sep 17 00:00:00 2001 From: Luca Negrini Date: Thu, 1 Aug 2024 11:45:39 +0200 Subject: [PATCH 2/5] Test for #300 --- .../heap/pointbased/PointBasedHeapTest.java | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) 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)); + } } From d7402894cfe79d4f22111f301edeae13e2509642 Mon Sep 17 00:00:00 2001 From: Luca Negrini Date: Thu, 1 Aug 2024 11:46:14 +0200 Subject: [PATCH 3/5] Ignoring conversions on receivers #300 --- .../lisa/analysis/heap/TypeBasedHeap.java | 9 ++++-- .../heap/pointbased/AllocationSite.java | 10 ++++++ .../AllocationSiteBasedAnalysis.java | 14 ++++++--- .../FieldSensitivePointBasedHeap.java | 4 ++- .../heap/pointbased/HeapAllocationSite.java | 6 ++++ .../heap/pointbased/StackAllocationSite.java | 6 ++++ .../lisa/analysis/heap/BaseHeapDomain.java | 31 +++++++++++++++++-- 7 files changed, 70 insertions(+), 10 deletions(-) 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..5558dc9dd 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-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 b1ecce964..5c8d38eb5 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 @@ -1,5 +1,9 @@ package it.unive.lisa.analysis.heap; +import java.util.HashSet; +import java.util.List; +import java.util.Set; + import it.unive.lisa.analysis.BaseLattice; import it.unive.lisa.analysis.ScopeToken; import it.unive.lisa.analysis.SemanticException; @@ -18,9 +22,8 @@ import it.unive.lisa.symbolic.value.TernaryExpression; import it.unive.lisa.symbolic.value.UnaryExpression; import it.unive.lisa.symbolic.value.ValueExpression; -import java.util.HashSet; -import java.util.List; -import java.util.Set; +import it.unive.lisa.symbolic.value.operator.TypeOperator; +import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator; /** * A base implementation of the {@link HeapDomain} interface, handling base @@ -148,6 +151,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, From 0d1b881893dc0ca309bff9b39654b74b83d61aee Mon Sep 17 00:00:00 2001 From: Luca Negrini Date: Thu, 1 Aug 2024 11:49:04 +0200 Subject: [PATCH 4/5] Formatting --- .../lisa/analysis/heap/pointbased/AllocationSite.java | 2 +- .../java/it/unive/lisa/analysis/heap/BaseHeapDomain.java | 7 +++---- 2 files changed, 4 insertions(+), 5 deletions(-) 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 5558dc9dd..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 @@ -181,7 +181,7 @@ public abstract AllocationSite withField( SymbolicExpression field); /** - * Yields a modified version of this allocation site with the given type + * Yields a modified version of this allocation site with the given type. * * @param type the new type * 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 5c8d38eb5..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 @@ -1,9 +1,5 @@ package it.unive.lisa.analysis.heap; -import java.util.HashSet; -import java.util.List; -import java.util.Set; - import it.unive.lisa.analysis.BaseLattice; import it.unive.lisa.analysis.ScopeToken; import it.unive.lisa.analysis.SemanticException; @@ -24,6 +20,9 @@ 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; /** * A base implementation of the {@link HeapDomain} interface, handling base From e07d9161b5eddac03b0ef96d0431053ff8f6fde2 Mon Sep 17 00:00:00 2001 From: Luca Negrini Date: Thu, 1 Aug 2024 15:05:25 +0200 Subject: [PATCH 5/5] Increasing version number --- lisa/gradle.properties | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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