Memory oracle methods #291

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java

@@ -3,6 +3,7 @@
 import it.unive.lisa.analysis.heap.HeapDomain;
 import it.unive.lisa.analysis.heap.HeapSemanticOperation.HeapReplacement;
 import it.unive.lisa.analysis.lattices.ExpressionSet;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.analysis.type.TypeDomain;
 import it.unive.lisa.analysis.value.ValueDomain;
 import it.unive.lisa.program.cfg.ProgramPoint;
@@ -668,5 +669,45 @@ public String toString() {
 					TYPE_REPRESENTATION_KEY, t,
 					VALUE_REPRESENTATION_KEY, v)).toString();
 		}
+
+		@Override
+		public Satisfiability alias(
+				SymbolicExpression x,
+				SymbolicExpression y,
+				ProgramPoint pp,
+				SemanticOracle oracle)
+				throws SemanticException {
+			return heap.alias(x, y, pp, oracle);
+		}
+
+		@Override
+		public Satisfiability isReachableFrom(
+				SymbolicExpression x,
+				SymbolicExpression y,
+				ProgramPoint pp,
+				SemanticOracle oracle)
+				throws SemanticException {
+			return heap.isReachableFrom(x, y, pp, oracle);
+		}
+	}
+
+	@Override
+	public Satisfiability alias(
+			SymbolicExpression x,
+			SymbolicExpression y,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		return heapState.alias(x, y, pp, oracle);
+	}
+
+	@Override
+	public Satisfiability isReachableFrom(
+			SymbolicExpression x,
+			SymbolicExpression y,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		return heapState.isReachableFrom(x, y, pp, oracle);
 	}
 }

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/combination/CartesianProduct.java

@@ -5,6 +5,7 @@
 import it.unive.lisa.analysis.SemanticDomain;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SemanticOracle;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.analysis.nonrelational.Environment;
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.SymbolicExpression;

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/combination/NonRelationalValueCartesianProduct.java

@@ -1,8 +1,8 @@
 package it.unive.lisa.analysis.combination;
 
-import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SemanticOracle;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
 import it.unive.lisa.analysis.nonrelational.value.NonRelationalValueDomain;
 import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;

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

@@ -4,6 +4,7 @@
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SemanticOracle;
 import it.unive.lisa.analysis.lattices.ExpressionSet;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.heap.AccessChild;
@@ -245,4 +246,24 @@ public boolean knowsIdentifier(
 			Identifier id) {
 		return false;
 	}
+
+	@Override
+	public Satisfiability alias(
+			SymbolicExpression x,
+			SymbolicExpression y,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	public Satisfiability isReachableFrom(
+			SymbolicExpression x,
+			SymbolicExpression y,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		return Satisfiability.UNKNOWN;
+	}
 }

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

@@ -3,6 +3,7 @@
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SemanticOracle;
 import it.unive.lisa.analysis.lattices.ExpressionSet;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.heap.AccessChild;
@@ -25,6 +26,7 @@
 import java.util.List;
 import java.util.Set;
 import java.util.function.Predicate;
+import org.apache.commons.collections4.CollectionUtils;
 import org.apache.commons.collections4.SetUtils;
 
 /**
@@ -336,4 +338,39 @@ public boolean knowsIdentifier(
 			Identifier id) {
 		return false;
 	}
+
+	@Override
+	public Satisfiability alias(
+			SymbolicExpression x,
+			SymbolicExpression y,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		if (isTop())
+			return Satisfiability.UNKNOWN;
+		if (isBottom())
+			return Satisfiability.BOTTOM;
+
+		Set<Type> ltypes = new HashSet<>();
+		for (SymbolicExpression e : rewrite(x, pp, oracle))
+			ltypes.addAll(oracle.getRuntimeTypesOf(e, pp, oracle));
+		Set<Type> rtypes = new HashSet<>();
+		for (SymbolicExpression e : rewrite(y, pp, oracle))
+			rtypes.addAll(oracle.getRuntimeTypesOf(e, pp, oracle));
+		if (CollectionUtils.intersection(ltypes, rtypes).isEmpty())
+			// no common types -> they cannot be "smashed" to the same location
+			return Satisfiability.NOT_SATISFIED;
+
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	public Satisfiability isReachableFrom(
+			SymbolicExpression x,
+			SymbolicExpression y,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		return Satisfiability.UNKNOWN;
+	}
 }

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

@@ -5,6 +5,7 @@
 import it.unive.lisa.analysis.SemanticOracle;
 import it.unive.lisa.analysis.heap.BaseHeapDomain;
 import it.unive.lisa.analysis.lattices.ExpressionSet;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.analysis.nonrelational.heap.HeapEnvironment;
 import it.unive.lisa.program.annotations.Annotation;
 import it.unive.lisa.program.cfg.CodeLocation;
@@ -22,6 +23,8 @@
 import it.unive.lisa.symbolic.value.Variable;
 import it.unive.lisa.type.ReferenceType;
 import it.unive.lisa.type.Type;
+import it.unive.lisa.util.collections.workset.VisitOnceFIFOWorkingSet;
+import it.unive.lisa.util.collections.workset.WorkingSet;
 import it.unive.lisa.util.representation.StructuredRepresentation;
 import java.util.Collections;
 import java.util.HashSet;
@@ -512,4 +515,74 @@ public boolean knowsIdentifier(
 		return heapEnv.knowsIdentifier(id) || (id instanceof AllocationSite
 				&& heapEnv.getValues().stream().anyMatch(as -> as.contains((AllocationSite) id)));
 	}
+
+	@Override
+	public Satisfiability alias(
+			SymbolicExpression x,
+			SymbolicExpression y,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		if (isTop())
+			return Satisfiability.UNKNOWN;
+		if (isBottom())
+			return Satisfiability.BOTTOM;
+
+		boolean atLeastOne = false;
+		boolean all = true;
+
+		ExpressionSet xrs = rewrite(x, pp, oracle);
+		ExpressionSet yrs = rewrite(y, pp, oracle);
+
+		for (SymbolicExpression xr : xrs)
+			for (SymbolicExpression yr : yrs)
+				if (xr instanceof MemoryPointer && yr instanceof MemoryPointer) {
+					HeapLocation xloc = ((MemoryPointer) xr).getReferencedLocation();
+					HeapLocation yloc = ((MemoryPointer) yr).getReferencedLocation();
+					if (xloc.equals(yloc)) {
+						atLeastOne = true;
+						all &= true;
+					} else
+						all = false;
+				} else
+					// they cannot be alias
+					all = false;
+
+		if (all && atLeastOne)
+			return Satisfiability.SATISFIED;
+		else if (atLeastOne)
+			return Satisfiability.UNKNOWN;
+		else
+			return Satisfiability.NOT_SATISFIED;
+	}
+
+	@Override
+	public Satisfiability isReachableFrom(
+			SymbolicExpression x,
+			SymbolicExpression y,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		if (isTop())
+			return Satisfiability.UNKNOWN;
+		if (isBottom())
+			return Satisfiability.BOTTOM;
+
+		WorkingSet<SymbolicExpression> ws = VisitOnceFIFOWorkingSet.mk();
+		rewrite(x, pp, oracle).elements().forEach(ws::push);
+		ExpressionSet targets = rewrite(y, pp, oracle);
+
+		while (!ws.isEmpty()) {
+			SymbolicExpression current = ws.peek();
+			if (targets.elements().contains(current))
+				return Satisfiability.SATISFIED;
+
+			if (current instanceof Identifier && heapEnv.knowsIdentifier((Identifier) current))
+				heapEnv.getState((Identifier) current).elements().forEach(ws::push);
+			else
+				rewrite(current, pp, oracle).elements().forEach(ws::push);
+		}
+
+		return Satisfiability.NOT_SATISFIED;
+	}
 }

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

@@ -1,9 +1,9 @@
 package it.unive.lisa.analysis.heap.pointbased;
 
-import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SemanticOracle;
 import it.unive.lisa.analysis.lattices.ExpressionSet;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.analysis.lattices.SetLattice;
 import it.unive.lisa.analysis.nonrelational.heap.HeapEnvironment;
 import it.unive.lisa.analysis.nonrelational.heap.NonRelationalHeapDomain;
@@ -188,4 +188,26 @@ public AllocationSites unknownVariable(
 		// possible information (top)
 		return bottom();
 	}
+
+	@Override
+	public Satisfiability alias(
+			SymbolicExpression x,
+			SymbolicExpression y,
+			HeapEnvironment<AllocationSites> environment,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	public Satisfiability isReachableFrom(
+			SymbolicExpression x,
+			SymbolicExpression y,
+			HeapEnvironment<AllocationSites> environment,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		return Satisfiability.UNKNOWN;
+	}
 }

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/nonRedundantSet/NonRedundantPowerset.java

@@ -5,6 +5,7 @@
 import it.unive.lisa.analysis.SemanticDomain;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SemanticOracle;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.analysis.lattices.SetLattice;
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.SymbolicExpression;

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/nonRedundantSet/NonRedundantPowersetOfBaseNonRelationalValueDomain.java

@@ -2,9 +2,9 @@
 
 import it.unive.lisa.analysis.BaseLattice;
 import it.unive.lisa.analysis.Lattice;
-import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SemanticOracle;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
 import it.unive.lisa.analysis.nonrelational.value.NonRelationalValueDomain;
 import it.unive.lisa.program.cfg.ProgramPoint;

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/IntegerConstantPropagation.java

@@ -2,9 +2,9 @@
 
 import it.unive.lisa.analysis.BaseLattice;
 import it.unive.lisa.analysis.Lattice;
-import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SemanticOracle;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
 import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
 import it.unive.lisa.program.cfg.ProgramPoint;

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Interval.java

@@ -2,9 +2,9 @@
 
 import it.unive.lisa.analysis.BaseLattice;
 import it.unive.lisa.analysis.Lattice;
-import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SemanticOracle;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
 import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
 import it.unive.lisa.program.cfg.ProgramPoint;

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Sign.java

@@ -2,9 +2,9 @@
 
 import it.unive.lisa.analysis.BaseLattice;
 import it.unive.lisa.analysis.Lattice;
-import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SemanticOracle;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
 import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
 import it.unive.lisa.program.cfg.ProgramPoint;

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/CharInclusion.java

@@ -1,9 +1,9 @@
 package it.unive.lisa.analysis.string;
 
 import it.unive.lisa.analysis.Lattice;
-import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SemanticOracle;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.value.Constant;

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/ContainsCharProvider.java

@@ -1,7 +1,7 @@
 package it.unive.lisa.analysis.string;
 
-import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
 import it.unive.lisa.analysis.SemanticException;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 
 /**
  * Interface for a string analysis that exposes the {@link #containsChar(char)}

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/Prefix.java

@@ -1,9 +1,9 @@
 package it.unive.lisa.analysis.string;
 
 import it.unive.lisa.analysis.Lattice;
-import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SemanticOracle;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.value.Constant;

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/Suffix.java

@@ -1,9 +1,9 @@
 package it.unive.lisa.analysis.string;
 
 import it.unive.lisa.analysis.Lattice;
-import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.SemanticOracle;
+import it.unive.lisa.analysis.lattices.Satisfiability;
 import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.value.Constant;