Fwd/Bwd edge traversal #120

lisa-analyzer · Oct 3, 2023 · cebe6fe · cebe6fe
1 parent 88217bf
commit cebe6fe
Show file tree

Hide file tree

Showing 6 changed files with 62 additions and 22 deletions.
diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/Edge.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/Edge.java
@@ -96,19 +96,37 @@ public boolean equals(
 	public abstract String toString();
 
 	/**
-	 * Traverses this edge, optionally modifying the given {@code sourceState}
-	 * by applying semantic assumptions.
+	 * Traverses this edge in the forward direction, proceeding from source to
+	 * destination, optionally modifying the given {@code sourceState} by
+	 * applying semantic assumptions.
 	 * 
-	 * @param <A>         the concrete {@link AbstractState} instance
-	 * @param sourceState the {@link AnalysisState} computed at the source of
-	 *                        this edge
+	 * @param <A>   the concrete {@link AbstractState} instance
+	 * @param state the {@link AnalysisState} computed at the source of this
+	 *                  edge
 	 * 
 	 * @return the {@link AnalysisState} after traversing this edge
 	 * 
 	 * @throws SemanticException if something goes wrong during the computation
 	 */
-	public abstract <A extends AbstractState<A>> AnalysisState<A> traverse(
-			AnalysisState<A> sourceState)
+	public abstract <A extends AbstractState<A>> AnalysisState<A> traverseForward(
+			AnalysisState<A> state)
+			throws SemanticException;
+
+	/**
+	 * Traverses this edge in the backward direction, from destination to
+	 * source, optionally modifying the given {@code sourceState} by applying
+	 * semantic assumptions.
+	 * 
+	 * @param <A>   the concrete {@link AbstractState} instance
+	 * @param state the {@link AnalysisState} computed at the destination of
+	 *                  this edge
+	 * 
+	 * @return the {@link AnalysisState} after traversing this edge
+	 * 
+	 * @throws SemanticException if something goes wrong during the computation
+	 */
+	public abstract <A extends AbstractState<A>> AnalysisState<A> traverseBackwards(
+			AnalysisState<A> state)
 			throws SemanticException;
 
 	@Override

diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/FalseEdge.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/FalseEdge.java
@@ -37,22 +37,29 @@ public String toString() {
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> traverse(
-			AnalysisState<A> sourceState)
+	public <A extends AbstractState<A>> AnalysisState<A> traverseForward(
+			AnalysisState<A> state)
 			throws SemanticException {
-		ExpressionSet exprs = sourceState.getComputedExpressions();
-		AnalysisState<A> result = sourceState.bottom();
+		ExpressionSet exprs = state.getComputedExpressions();
+		AnalysisState<A> result = state.bottom();
 		for (SymbolicExpression expr : exprs) {
 			UnaryExpression negated = new UnaryExpression(
 					expr.getStaticType(),
 					expr,
 					LogicalNegation.INSTANCE,
 					expr.getCodeLocation());
-			result = result.lub(sourceState.assume(negated, getSource(), getDestination()));
+			result = result.lub(state.assume(negated, getSource(), getDestination()));
 		}
 		return result;
 	}
 
+	@Override
+	public <A extends AbstractState<A>> AnalysisState<A> traverseBackwards(
+			AnalysisState<A> state)
+			throws SemanticException {
+		return traverseForward(state);
+	}
+
 	@Override
 	public boolean isUnconditional() {
 		return false;

diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/SequentialEdge.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/SequentialEdge.java
@@ -2,6 +2,7 @@
 
 import it.unive.lisa.analysis.AbstractState;
 import it.unive.lisa.analysis.AnalysisState;
+import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.program.cfg.statement.Statement;
 
 /**
@@ -37,9 +38,16 @@ public String toString() {
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> traverse(
-			AnalysisState<A> sourceState) {
-		return sourceState;
+	public <A extends AbstractState<A>> AnalysisState<A> traverseForward(
+			AnalysisState<A> state) {
+		return state;
+	}
+
+	@Override
+	public <A extends AbstractState<A>> AnalysisState<A> traverseBackwards(
+			AnalysisState<A> state)
+			throws SemanticException {
+		return traverseForward(state);
 	}
 
 	@Override

diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/TrueEdge.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/TrueEdge.java
@@ -34,16 +34,23 @@ public String toString() {
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> traverse(
-			AnalysisState<A> sourceState)
+	public <A extends AbstractState<A>> AnalysisState<A> traverseForward(
+			AnalysisState<A> state)
 			throws SemanticException {
-		ExpressionSet exprs = sourceState.getComputedExpressions();
-		AnalysisState<A> result = sourceState.bottom();
+		ExpressionSet exprs = state.getComputedExpressions();
+		AnalysisState<A> result = state.bottom();
 		for (SymbolicExpression expr : exprs)
-			result = result.lub(sourceState.assume(expr, getSource(), getDestination()));
+			result = result.lub(state.assume(expr, getSource(), getDestination()));
 		return result;
 	}
 
+	@Override
+	public <A extends AbstractState<A>> AnalysisState<A> traverseBackwards(
+			AnalysisState<A> state)
+			throws SemanticException {
+		return traverseForward(state);
+	}
+
 	@Override
 	public boolean isUnconditional() {
 		return false;

diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/BackwardCFGFixpoint.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/BackwardCFGFixpoint.java
@@ -74,7 +74,7 @@ public CompoundState<A> traverse(
 			Edge edge,
 			CompoundState<A> entrystate)
 			throws SemanticException {
-		AnalysisState<A> approx = edge.traverse(entrystate.postState);
+		AnalysisState<A> approx = edge.traverseBackwards(entrystate.postState);
 
 		// we remove out of scope variables here
 		List<VariableTableEntry> toRemove = new LinkedList<>();

diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/CFGFixpoint.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/CFGFixpoint.java
@@ -76,7 +76,7 @@ public CompoundState<A> traverse(
 			Edge edge,
 			CompoundState<A> entrystate)
 			throws SemanticException {
-		AnalysisState<A> approx = edge.traverse(entrystate.postState);
+		AnalysisState<A> approx = edge.traverseForward(entrystate.postState);
 
 		// we remove out of scope variables here
 		List<VariableTableEntry> toRemove = new LinkedList<>();