Merge pull request #290 from lisa-analyzer/anns-propagation

Annotations propagation for point based heap analyses

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java

@@ -6,6 +6,7 @@
 import it.unive.lisa.analysis.heap.BaseHeapDomain;
 import it.unive.lisa.analysis.lattices.ExpressionSet;
 import it.unive.lisa.analysis.nonrelational.heap.HeapEnvironment;
+import it.unive.lisa.program.annotations.Annotation;
 import it.unive.lisa.program.cfg.CodeLocation;
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.SymbolicExpression;
@@ -348,6 +349,14 @@ public ExpressionSet visit(
 								site.getLocationName(),
 								true,
 								expression.getCodeLocation());
+
+					// propagates the annotations of the child value expression
+					// to the newly created allocation site
+					for (SymbolicExpression f : child)
+						if (f instanceof Identifier)
+							for (Annotation ann : e.getAnnotations())
+								e.addAnnotation(ann);
+
 					result.add(e);
 				} else if (rec instanceof AllocationSite)
 					result.add(rec);
@@ -373,6 +382,12 @@ public ExpressionSet visit(
 						expression.getCodeLocation().getCodeLocation(),
 						true,
 						expression.getCodeLocation());
+
+			// propagates the annotations of expression
+			// to the newly created allocation site
+			for (Annotation ann : expression.getAnnotations())
+				id.addAnnotation(ann);
+
 			return new ExpressionSet(id);
 		}
 
@@ -386,10 +401,17 @@ public ExpressionSet visit(
 
 			for (SymbolicExpression loc : arg)
 				if (loc instanceof AllocationSite) {
+					AllocationSite allocSite = (AllocationSite) loc;
 					MemoryPointer e = new MemoryPointer(
 							new ReferenceType(loc.getStaticType()),
-							(AllocationSite) loc,
+							allocSite,
 							loc.getCodeLocation());
+
+					// propagates the annotations of the allocation site
+					// to the newly created memory pointer
+					for (Annotation ann : allocSite.getAnnotations())
+						e.addAnnotation(ann);
+
 					result.add(e);
 				} else
 					result.add(loc);
@@ -424,6 +446,12 @@ else if (id.getStaticType().isInMemoryType() || id.getStaticType().isUntyped())
 						else
 							throw new SemanticException("The type " + id.getStaticType()
 									+ " cannot be allocated by point-based heap domains");
+
+						// propagates the annotations of the variable
+						// to the newly created allocation site
+						for (Annotation ann : id.getAnnotations())
+							site.addAnnotation(ann);
+
 						result.add(site);
 					}
 				} else

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/FieldSensitivePointBasedHeap.java

@@ -6,6 +6,7 @@
 import it.unive.lisa.analysis.lattices.ExpressionSet;
 import it.unive.lisa.analysis.lattices.GenericMapLattice;
 import it.unive.lisa.analysis.nonrelational.heap.HeapEnvironment;
+import it.unive.lisa.program.annotations.Annotation;
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.heap.AccessChild;
@@ -308,6 +309,13 @@ private void populate(
 							target,
 							site.isWeak(),
 							site.getCodeLocation());
+
+				// propagates the annotations of the child value expression to
+				// the newly created allocation site
+				if (target instanceof Identifier)
+					for (Annotation ann : e.getAnnotations())
+						e.addAnnotation(ann);
+
 				result.add(e);
 			}
 		}
@@ -330,6 +338,12 @@ public ExpressionSet visit(
 				e = new StackAllocationSite(expression.getStaticType(), pp, weak, expression.getCodeLocation());
 			else
 				e = new HeapAllocationSite(expression.getStaticType(), pp, weak, expression.getCodeLocation());
+
+			// propagates the annotations of expression
+			// to the newly created allocation site
+			for (Annotation ann : expression.getAnnotations())
+				e.getAnnotations().addAnnotation(ann);
+
 			return new ExpressionSet(e);
 		}
 	}

lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeapTest.java

@@ -11,6 +11,7 @@
 import it.unive.lisa.analysis.nonrelational.heap.HeapEnvironment;
 import it.unive.lisa.program.CodeElement;
 import it.unive.lisa.program.SourceCodeLocation;
+import it.unive.lisa.program.annotations.Annotations;
 import it.unive.lisa.program.cfg.CFG;
 import it.unive.lisa.program.cfg.CodeLocation;
 import it.unive.lisa.program.cfg.ProgramPoint;
@@ -174,7 +175,7 @@ public void testSmallStepSemantic() throws SemanticException {
 		// result.
 
 		// 1. Heap allocation
-		HeapExpression heapExpression = new MemoryAllocation(untyped, loc1);
+		HeapExpression heapExpression = new MemoryAllocation(untyped, loc1, new Annotations());
 
 		// from topState
 		PointBasedHeap sss = topHeap.semanticsOf(heapExpression, pp1, fakeOracle);
@@ -194,7 +195,7 @@ public void testSmallStepSemantic() throws SemanticException {
 
 		// 2. Heap reference
 		heapExpression = new HeapReference(untyped,
-				new MemoryAllocation(untyped, loc1), loc1);
+				new MemoryAllocation(untyped, loc1, new Annotations()), loc1);
 
 		// from topState
 		sss = topHeap.semanticsOf(heapExpression, pp1, fakeOracle);
@@ -225,7 +226,7 @@ public void testSmallStepSemantic() throws SemanticException {
 
 		// 4. Heap dereference
 		heapExpression = new HeapDereference(untyped, new HeapReference(untyped,
-				new MemoryAllocation(untyped, loc1), loc1), loc1);
+				new MemoryAllocation(untyped, loc1, new Annotations()), loc1), loc1);
 
 		// from topState
 		sss = topHeap.semanticsOf(heapExpression, pp1, fakeOracle);
@@ -483,7 +484,7 @@ public void testIdentifierRewrite() throws SemanticException {
 	public void testHeapDereferenceRewrite() throws SemanticException {
 		// *(&(new loc(pp1, fakeOracle)) rewritten in top -> pp1
 		HeapDereference deref = new HeapDereference(untyped, new HeapReference(untyped,
-				new MemoryAllocation(untyped, loc1), loc1), loc1);
+				new MemoryAllocation(untyped, loc1, new Annotations()), loc1), loc1);
 
 		ExpressionSet expectedRewritten = new ExpressionSet(alloc1);
 		assertEquals(expectedRewritten, topHeap.rewrite(deref, fakeProgramPoint, fakeOracle));

lisa/lisa-sdk/src/main/java/it/unive/lisa/symbolic/heap/MemoryAllocation.java

@@ -1,6 +1,7 @@
 package it.unive.lisa.symbolic.heap;
 
 import it.unive.lisa.analysis.SemanticException;
+import it.unive.lisa.program.annotations.Annotations;
 import it.unive.lisa.program.cfg.CodeLocation;
 import it.unive.lisa.symbolic.ExpressionVisitor;
 import it.unive.lisa.type.Type;
@@ -18,6 +19,11 @@ public class MemoryAllocation extends HeapExpression {
 	 */
 	private final boolean isStackAllocation;
 
+	/**
+	 * Annotations of this memory allocation.
+	 */
+	private final Annotations anns;
+
 	/**
 	 * Builds the heap allocation.
 	 * 
@@ -31,27 +37,60 @@ public MemoryAllocation(
 		this(staticType, location, false);
 	}
 
+	/**
+	 * Builds the heap allocation.
+	 * 
+	 * @param staticType the static type of this expression
+	 * @param location   the code location of the statement that has generated
+	 *                       this expression
+	 * @param anns       the annotations of this memory allocation
+	 */
+	public MemoryAllocation(
+			Type staticType,
+			CodeLocation location,
+			Annotations anns) {
+		this(staticType, location, anns, false);
+	}
+
+	/**
+	 * Builds the heap allocation.
+	 * 
+	 * @param staticType        the static type of this expression
+	 * @param location          the code location of the statement that has
+	 *                              generated this expression
+	 * @param isStackAllocation if this allocation is allocated in the stack
+	 */
+	public MemoryAllocation(
+			Type staticType,
+			CodeLocation location,
+			boolean isStackAllocation) {
+		this(staticType, location, new Annotations(), isStackAllocation);
+	}
+
 	/**
 	 * Builds the heap allocation.
 	 * 
 	 * @param staticType        the static type of this expression
 	 * @param location          the code location of the statement that has
 	 *                              generated this expression
+	 * @param anns              the annotations of this memory allocation
 	 * @param isStackAllocation if this allocation is allocated in the stack
 	 */
 	public MemoryAllocation(
 			Type staticType,
 			CodeLocation location,
+			Annotations anns,
 			boolean isStackAllocation) {
 		super(staticType, location);
 		this.isStackAllocation = isStackAllocation;
+		this.anns = anns;
 	}
 
 	@Override
 	public int hashCode() {
 		final int prime = 31;
 		int result = super.hashCode();
-		result = prime * result + Objects.hash(isStackAllocation);
+		result = prime * result + Objects.hash(anns, isStackAllocation);
 		return result;
 	}
 
@@ -64,6 +103,15 @@ public boolean isStackAllocation() {
 		return isStackAllocation;
 	}
 
+	/**
+	 * Yields the annotations of this expression.
+	 * 
+	 * @return the annotations of this expression
+	 */
+	public Annotations getAnnotations() {
+		return anns;
+	}
+
 	@Override
 	public boolean equals(
 			Object obj) {
@@ -74,7 +122,7 @@ public boolean equals(
 		if (getClass() != obj.getClass())
 			return false;
 		MemoryAllocation other = (MemoryAllocation) obj;
-		return isStackAllocation == other.isStackAllocation;
+		return Objects.equals(anns, other.anns) && isStackAllocation == other.isStackAllocation;
 	}
 
 	@Override