#12 refinement of the whole framework

lisa/src/main/java/it/unive/lisa/analysis/AbstractState.java

@@ -1,11 +1,8 @@
 package it.unive.lisa.analysis;
 
-import it.unive.lisa.symbolic.Identifier;
 import it.unive.lisa.symbolic.SymbolicExpression;
-import it.unive.lisa.symbolic.heap.HeapExpression;
-import it.unive.lisa.symbolic.heap.HeapIdentifier;
+import it.unive.lisa.symbolic.value.Identifier;
 import it.unive.lisa.symbolic.value.ValueExpression;
-import it.unive.lisa.symbolic.value.ValueIdentifier;
 
 /**
  * An abstract state of the analysis, composed by a heap state modeling the
@@ -64,67 +61,62 @@ public V getValueState() {
 	}
 
 	@Override
-	public AbstractState<H, V> assign(Identifier id, SymbolicExpression value) {
-		H heap = heapState;
-		V val = valueState;
+	public AbstractState<H, V> assign(Identifier id, SymbolicExpression expression) throws SemanticException {
+		H heap = heapState.assign(id, expression);
+		ValueExpression expr = heap.getRewrittenExpression();
 
-		if (id instanceof ValueIdentifier)
-			val = val.assign((ValueIdentifier) id, (ValueExpression) value);
-		else
-			// TODO we should take care of replacements
-			heap = heap.assign((HeapIdentifier) id, (HeapExpression) value);
+		V value = valueState;
+		if (heap.getSubstitution() != null && !heap.getSubstitution().isEmpty())
+			value = value.applySubstitution(heap.getSubstitution());
 
-		return new AbstractState<>(heap, val);
+		value = value.assign(id, expr);
+		return new AbstractState<>(heap, value);
 	}
 
 	@Override
-	public AbstractState<H, V> smallStepSemantics(SymbolicExpression expression) {
-		H heap = heapState;
-		V val = valueState;
+	public AbstractState<H, V> smallStepSemantics(SymbolicExpression expression) throws SemanticException {
+		H heap = heapState.smallStepSemantics(expression);
+		ValueExpression expr = heap.getRewrittenExpression();
 
-		if (expression instanceof ValueExpression)
-			val = val.smallStepSemantics((ValueExpression) expression);
-		else
-			// TODO we should take care of replacements
-			heap = heap.smallStepSemantics((HeapExpression) expression);
+		V value = valueState;
+		if (heap.getSubstitution() != null && !heap.getSubstitution().isEmpty())
+			value = value.applySubstitution(heap.getSubstitution());
 
-		return new AbstractState<>(heap, val);
+		value = value.smallStepSemantics(expr);
+		return new AbstractState<>(heap, value);
 	}
 
 	@Override
-	public AbstractState<H, V> assume(SymbolicExpression expression) {
-		H heap = heapState;
-		V val = valueState;
+	public AbstractState<H, V> assume(SymbolicExpression expression) throws SemanticException {
+		H heap = heapState.assume(expression);
+		ValueExpression expr = heap.getRewrittenExpression();
 
-		if (expression instanceof ValueExpression)
-			val = val.assume((ValueExpression) expression);
-		else
-			// TODO we should take care of replacements
-			heap = heap.assume((HeapExpression) expression);
+		V value = valueState;
+		if (heap.getSubstitution() != null && !heap.getSubstitution().isEmpty())
+			value = value.applySubstitution(heap.getSubstitution());
 
-		return new AbstractState<>(heap, val);
+		value = value.assume(expr);
+		return new AbstractState<>(heap, value);
 	}
 
 	@Override
-	public Satisfiability satisfy(SymbolicExpression expression) {
-		if (expression instanceof ValueExpression)
-			return valueState.satisfy((ValueExpression) expression);
-		else
-			return heapState.satisfy((HeapExpression) expression);
+	public Satisfiability satisfies(SymbolicExpression expression) throws SemanticException {
+		return heapState.satisfies(expression)
+				.glb(valueState.satisfies(heapState.smallStepSemantics(expression).getRewrittenExpression()));
 	}
 
 	@Override
-	public AbstractState<H, V> lub(AbstractState<H, V> other) {
+	public AbstractState<H, V> lub(AbstractState<H, V> other) throws SemanticException {
 		return new AbstractState<>(heapState.lub(other.heapState), valueState.lub(other.valueState));
 	}
 
 	@Override
-	public AbstractState<H, V> widening(AbstractState<H, V> other) {
+	public AbstractState<H, V> widening(AbstractState<H, V> other) throws SemanticException {
 		return new AbstractState<>(heapState.widening(other.heapState), valueState.widening(other.valueState));
 	}
 
 	@Override
-	public boolean lessOrEqual(AbstractState<H, V> other) {
+	public boolean lessOrEqual(AbstractState<H, V> other) throws SemanticException {
 		return heapState.lessOrEqual(other.heapState) && valueState.lessOrEqual(other.valueState);
 	}
 
@@ -147,4 +139,9 @@ public boolean isTop() {
 	public boolean isBottom() {
 		return heapState.isBottom() && valueState.isBottom();
 	}
+
+	@Override
+	public AbstractState<H, V> forgetIdentifier(Identifier id) throws SemanticException {
+		return new AbstractState<>(heapState.forgetIdentifier(id), valueState.forgetIdentifier(id));
+	}
 }

lisa/src/main/java/it/unive/lisa/analysis/AnalysisState.java

@@ -1,8 +1,8 @@
 package it.unive.lisa.analysis;
 
-import it.unive.lisa.symbolic.Identifier;
 import it.unive.lisa.symbolic.Skip;
 import it.unive.lisa.symbolic.SymbolicExpression;
+import it.unive.lisa.symbolic.value.Identifier;
 
 /**
  * The abstract analysis state at a given program point. An analysis state is
@@ -65,45 +65,51 @@ public SymbolicExpression getLastComputedExpression() {
 	}
 
 	@Override
-	public AnalysisState<H, V> assign(Identifier id, SymbolicExpression value) {
-		return new AnalysisState<>(getState().assign(id, value), (SymbolicExpression) id);
+	public AnalysisState<H, V> assign(Identifier id, SymbolicExpression value) throws SemanticException {
+		return new AnalysisState<>(getState().assign(id, value), id);
 	}
 
 	@Override
-	public AnalysisState<H, V> smallStepSemantics(SymbolicExpression expression) {
-		// TODO should we return an expression that contains the value?
-		// answer: yes, but how to do this
-		return new AnalysisState<>(state.smallStepSemantics(expression), new Skip());
+	public AnalysisState<H, V> smallStepSemantics(SymbolicExpression expression) throws SemanticException {
+		AbstractState<H, V> s = state.smallStepSemantics(expression);
+		return new AnalysisState<>(s, s.getHeapState().getRewrittenExpression());
 	}
 
 	@Override
-	public AnalysisState<H, V> assume(SymbolicExpression expression) {
-		return new AnalysisState<>(state.assume(expression), new Skip());
+	public AnalysisState<H, V> assume(SymbolicExpression expression) throws SemanticException {
+		return new AnalysisState<>(state.assume(expression), lastComputedExpression);
 	}
 
 	@Override
-	public Satisfiability satisfy(SymbolicExpression expression) {
-		return state.satisfy(expression);
+	public Satisfiability satisfies(SymbolicExpression expression) throws SemanticException {
+		return state.satisfies(expression);
 	}
 
 	@Override
-	public AnalysisState<H, V> lub(AnalysisState<H, V> other) {
-		// TODO should we perform some check on the expression too?
+	public AnalysisState<H, V> lub(AnalysisState<H, V> other) throws SemanticException {
+		checkExpression(other);
 		return new AnalysisState<>(state.lub(other.state), lastComputedExpression);
 	}
 
 	@Override
-	public AnalysisState<H, V> widening(AnalysisState<H, V> other) {
-		// TODO should we perform some check on the expression too?
+	public AnalysisState<H, V> widening(AnalysisState<H, V> other) throws SemanticException {
+		checkExpression(other);
 		return new AnalysisState<>(state.widening(other.state), lastComputedExpression);
 	}
 
 	@Override
-	public boolean lessOrEqual(AnalysisState<H, V> other) {
-		// TODO should we perform some check on the expression too?
+	public boolean lessOrEqual(AnalysisState<H, V> other) throws SemanticException {
+		checkExpression(other);
 		return state.lessOrEqual(other.state);
 	}
 
+	private void checkExpression(AnalysisState<H, V> other) throws SemanticException {
+		// TODO we want to eventually support this
+		if (!lastComputedExpression.equals(other.lastComputedExpression))
+			throw new SemanticException(
+					"Semantic operations on instances with different expressions is not yet supported");
+	}
+
 	@Override
 	public AnalysisState<H, V> top() {
 		return new AnalysisState<>(state.top(), new Skip());
@@ -113,14 +119,19 @@ public AnalysisState<H, V> top() {
 	public AnalysisState<H, V> bottom() {
 		return new AnalysisState<>(state.bottom(), new Skip());
 	}
-	
+
 	@Override
 	public boolean isTop() {
 		return state.isTop() && lastComputedExpression instanceof Skip;
 	}
-	
+
 	@Override
 	public boolean isBottom() {
 		return state.isBottom() && lastComputedExpression instanceof Skip;
 	}
+
+	@Override
+	public AnalysisState<H, V> forgetIdentifier(Identifier id) throws SemanticException {
+		return new AnalysisState<>(state.forgetIdentifier(id), lastComputedExpression);
+	}
 }

lisa/src/main/java/it/unive/lisa/analysis/BaseLattice.java

@@ -14,7 +14,7 @@ public abstract class BaseLattice<L extends BaseLattice<L>> implements Lattice<L
 
 	@Override
 	@SuppressWarnings("unchecked")
-	public final L lub(L other) {
+	public final L lub(L other) throws SemanticException {
 		if (other == null || other == bottom() || this == top() || this == other || equals(other))
 			return (L) this;
 
@@ -37,12 +37,13 @@ public final L lub(L other) {
 	 * 
 	 * @param other the other lattice element
 	 * @return the least upper bound
+	 * @throws SemanticException if an error occurs during the computation
 	 */
-	protected abstract L lubAux(L other);
+	protected abstract L lubAux(L other) throws SemanticException;
 
 	@Override
 	@SuppressWarnings("unchecked")
-	public final L widening(L other) {
+	public final L widening(L other) throws SemanticException {
 		if (other == null || other == bottom() || this == top() || this == other || equals(other))
 			return (L) this;
 
@@ -65,11 +66,12 @@ public final L widening(L other) {
 	 * 
 	 * @param other the other lattice element
 	 * @return the least upper bound
+	 * @throws SemanticException if an error occurs during the computation
 	 */
-	protected abstract L wideningAux(L other);
+	protected abstract L wideningAux(L other) throws SemanticException;
 
 	@Override
-	public final boolean lessOrEqual(L other) {
+	public final boolean lessOrEqual(L other) throws SemanticException {
 		if (other == null)
 			return false;
 
@@ -95,6 +97,7 @@ public final boolean lessOrEqual(L other) {
 	 * 
 	 * @param other the other lattice element
 	 * @return {@code true} if and only if that condition holds
+	 * @throws SemanticException if an error occurs during the computation
 	 */
-	protected abstract boolean lessOrEqualAux(L other);
+	protected abstract boolean lessOrEqualAux(L other) throws SemanticException;
 }

lisa/src/main/java/it/unive/lisa/analysis/CFGWithAnalysisResults.java

@@ -8,8 +8,9 @@
 
 /**
  * A control flow graph, that has {@link Statement}s as nodes and {@link Edge}s
- * as edges. It also maps each expression to the result of a fixpoint
- * computation, in the form of an {@link AnalysisState} instance.
+ * as edges. It also maps each statement (and its inner expressions) to the
+ * result of a fixpoint computation, in the form of an {@link AnalysisState}
+ * instance.
  * 
  * @param <H> the type of {@link HeapDomain} contained into the computed
  *            abstract state
@@ -23,7 +24,7 @@ public class CFGWithAnalysisResults<H extends HeapDomain<H>, V extends ValueDoma
 	/**
 	 * The map storing the analysis results
 	 */
-	private final Map<Statement, AnalysisState<H, V>> results; // TODO should this be an abstract state?
+	private final Map<Statement, AnalysisState<H, V>> results;
 
 	/**
 	 * Builds the control flow graph, storing the given mapping between nodes and

lisa/src/main/java/it/unive/lisa/analysis/CallGraph.java

@@ -4,6 +4,8 @@
 
 import it.unive.lisa.cfg.CFG;
 import it.unive.lisa.cfg.statement.CFGCall;
+import it.unive.lisa.symbolic.SymbolicExpression;
+import it.unive.lisa.symbolic.value.Identifier;
 
 /**
  * A callgraph of the program to analyze, that knows how to resolve dynamic
@@ -28,7 +30,7 @@ public interface CallGraph {
 	 * callgraph. Each result is computed with
 	 * {@link CFG#fixpoint(Collection, AnalysisState, CallGraph, it.unive.lisa.util.workset.WorkingSet, int)}.
 	 * Results of individual cfgs are then available through
-	 * {@link #getAnalysisResultsOf(Class, CFG)}.
+	 * {@link #getAnalysisResultsOf(CFG)}.
 	 * 
 	 * @param <H>        the type of {@link HeapDomain} to compute
 	 * @param <V>        the type of {@link ValueDomain} to compute
@@ -41,16 +43,37 @@ public interface CallGraph {
 	 * Yields the results of the given analysis, identified by its class, on the
 	 * given {@link CFG}. Results are provided as {@link CFGWithAnalysisResults}.
 	 * 
-	 * @param <H>         the type of {@link HeapDomain} contained into the computed
-	 *                    abstract state
-	 * @param <V>         the type of {@link ValueDomain} contained into the
-	 *                    computed abstract state
-	 * @param valueDomain the class of the {@link ValueDomain} whose results needs
-	 *                    to be retrieved
-	 * @param cfg         the cfg whose fixpoint results needs to be retrieved
+	 * @param <H> the type of {@link HeapDomain} contained into the computed
+	 *            abstract state
+	 * @param <V> the type of {@link ValueDomain} contained into the computed
+	 *            abstract state
+	 * @param cfg the cfg whose fixpoint results needs to be retrieved
 	 * @return the result of the fixpoint computation of {@code valueDomain} over
 	 *         {@code cfg}
 	 */
-	<H extends HeapDomain<H>, V extends ValueDomain<V>> CFGWithAnalysisResults<H, V> getAnalysisResultsOf(
-			Class<V> valueDomain, CFG cfg);
+	<H extends HeapDomain<H>, V extends ValueDomain<V>> CFGWithAnalysisResults<H, V> getAnalysisResultsOf(CFG cfg);
+
+	/**
+	 * Resolves the given call to all of its possible runtime targets, and then
+	 * computes an analysis state that abstracts the execution of the possible
+	 * targets considering that they were given {@code parameters} as actual
+	 * parameters. The abstract value of each parameter is computed on
+	 * {@code entryState}.
+	 * 
+	 * @param <H>        the type of {@link HeapDomain} contained into the computed
+	 *                   abstract state
+	 * @param <V>        the type of {@link ValueDomain} contained into the computed
+	 *                   abstract state
+	 * @param call       the call to resolve and evaluate
+	 * @param entryState the abstract analysis state when the call is reached
+	 * @param parameters the expressions representing the actual parameters of the
+	 *                   call
+	 * @return an abstract analysis state representing the abstract result of the
+	 *         cfg call. The {@link AnalysisState#getLastComputedExpression()} will
+	 *         contain an {@link Identifier} pointing to the meta variable
+	 *         containing the abstraction of the returned value
+	 * @throws SemanticException if something goes wrong during the computation
+	 */
+	<H extends HeapDomain<H>, V extends ValueDomain<V>> AnalysisState<H, V> getAbstractResultOf(CFGCall call,
+			AnalysisState<H, V> entryState, SymbolicExpression[] parameters) throws SemanticException;
 }