Extending point-based analyses to handle pointers to primitive types

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

@@ -404,7 +404,8 @@ public ExpressionSet<ValueExpression> visit(HeapReference expression, Expression
 				Object... params)
 				throws SemanticException {
 			Set<ValueExpression> result = new HashSet<>();
-
+			SymbolicExpression referred = expression.getExpression();
+
 			for (ValueExpression loc : arg)
 				if (loc instanceof AllocationSite) {
 					MemoryPointer e = new MemoryPointer(
@@ -414,6 +415,20 @@ public ExpressionSet<ValueExpression> visit(HeapReference expression, Expression
 					if (expression.hasRuntimeTypes())
 						e.setRuntimeTypes(expression.getRuntimeTypes(null));
 					result.add(e);
+				} else if (referred.hasRuntimeTypes() && referred.getRuntimeTypes(null).stream().anyMatch(t -> !t.isInMemoryType())) {
+//					if (loc.hasRuntimeTypes() && loc.getRuntimeTypes(null).stream().anyMatch(t -> !t.isInMemoryType())) {						
+						for (Type type : referred.getRuntimeTypes(null)) {
+							VariableAllocationSite site = new VariableAllocationSite(type, (Identifier) referred,
+									loc.getCodeLocation());
+							MemoryPointer e = new MemoryPointer(
+									new ReferenceType(type),
+									site,
+									site.getCodeLocation());
+							e.setRuntimeTypes(Collections.singleton(new ReferenceType(type)));
+							result.add(e);
+						}
+//					} else
+//						result.add(loc);
 				} else
 					result.add(loc);
 			return new ExpressionSet<>(result);
@@ -426,9 +441,15 @@ public ExpressionSet<ValueExpression> visit(HeapDereference expression, Expressi
 			Set<ValueExpression> result = new HashSet<>();
 
 			for (ValueExpression ref : arg)
-				if (ref instanceof MemoryPointer)
-					result.add(((MemoryPointer) ref).getReferencedLocation());
-				else if (ref instanceof Identifier) {
+				if (ref instanceof MemoryPointer) {
+					HeapLocation location = ((MemoryPointer) ref).getReferencedLocation();
+					if (location instanceof VariableAllocationSite)
+						// if location is a variable allocation site, it
+						// rewrites to the pointed variable
+						result.add(((VariableAllocationSite) location).getIdentifier());
+					else
+						result.add(location);
+				} else if (ref instanceof Identifier) {
 					// this could be aliasing!
 					Identifier id = (Identifier) ref;
 					if (heapEnv.getKeys().contains(id))
@@ -456,8 +477,10 @@ else if (id.getStaticType().isInMemoryType() || id.getStaticType().isUntyped())
 		@Override
 		public ExpressionSet<ValueExpression> visit(Identifier expression, Object... params)
 				throws SemanticException {
-			if (!(expression instanceof MemoryPointer) && heapEnv.getKeys().contains(expression))
-				return new ExpressionSet<>(resolveIdentifier(expression));
+			if (!(expression instanceof MemoryPointer)) {
+				if (heapEnv.getKeys().contains(expression))
+					return new ExpressionSet<>(resolveIdentifier(expression));
+			}
 
 			return new ExpressionSet<>(expression);
 		}

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

@@ -0,0 +1,69 @@
+package it.unive.lisa.analysis.heap.pointbased;
+
+import it.unive.lisa.program.cfg.CodeLocation;
+import it.unive.lisa.symbolic.value.Identifier;
+import it.unive.lisa.type.Type;
+import java.util.Objects;
+
+/**
+ * A variabile allocation site, namely an allocation site used by point-based
+ * analyses abstracting concrete pointers to variables containing primitive type
+ * values.
+ * 
+ * @author <a href="mailto:vincenzo.arceri@unipr.it">Vincenzo Arceri</a>
+ * @author <a href="mailto:simone.gazza@studenti.unipr.it">Simone Gazza</a>
+ */
+public class VariableAllocationSite extends AllocationSite {
+
+	/**
+	 * The identifier pointed by this allocation site.
+	 */
+	private final Identifier identifier;
+
+	/**
+	 * Builds the variable allocation site
+	 * 
+	 * @param staticType the static type
+	 * @param identifier the identifier pointed by this allocation site
+	 * @param location   the location of this allocation site
+	 */
+	public VariableAllocationSite(Type staticType, Identifier identifier, CodeLocation location) {
+		super(staticType, "&" + identifier.getName(), false, location);
+		this.identifier = identifier;
+	}
+
+	@Override
+	public String toString() {
+		return getName();
+	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = super.hashCode();
+		result = prime * result + Objects.hash(identifier);
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (this == obj)
+			return true;
+		if (!super.equals(obj))
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		VariableAllocationSite other = (VariableAllocationSite) obj;
+		return Objects.equals(identifier, other.identifier);
+	}
+
+	/**
+	 * Yields the identifier.
+	 * 
+	 * @return the identifier
+	 */
+	public Identifier getIdentifier() {
+		return identifier;
+	}
+
+}

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

@@ -1,5 +1,6 @@
 package it.unive.lisa.symbolic.heap;
 
+import it.unive.lisa.analysis.ScopeToken;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.program.cfg.CodeLocation;
 import it.unive.lisa.symbolic.ExpressionVisitor;
@@ -75,4 +76,24 @@ public <T> T accept(ExpressionVisitor<T> visitor, Object... params) throws Seman
 		T l = expression.accept(visitor, params);
 		return visitor.visit(this, l, params);
 	}
+
+	@Override
+	public SymbolicExpression pushScope(ScopeToken token) {
+		try {
+			return new HeapReference(getStaticType(), expression.pushScope(token), getCodeLocation());
+		} catch (SemanticException e) {
+			// TODO: this is here to make the code compile, change this ASAP
+			throw new IllegalStateException();
+		}
+	}
+
+	@Override
+	public SymbolicExpression popScope(ScopeToken token) throws SemanticException {
+		try {
+			return new HeapReference(getStaticType(), expression.popScope(token), getCodeLocation());
+		} catch (SemanticException e) {
+			// TODO: this is here to make the code compile, change this ASAP
+			throw new IllegalStateException();
+		} 
+	}
 }