From cebe6fe7d9b7f75067150957aaeaaee7a80a1855 Mon Sep 17 00:00:00 2001 From: Luca Negrini Date: Tue, 3 Oct 2023 16:56:19 +0200 Subject: [PATCH] Fwd/Bwd edge traversal #120 --- .../it/unive/lisa/program/cfg/edge/Edge.java | 32 +++++++++++++++---- .../lisa/program/cfg/edge/FalseEdge.java | 17 +++++++--- .../lisa/program/cfg/edge/SequentialEdge.java | 14 ++++++-- .../unive/lisa/program/cfg/edge/TrueEdge.java | 17 +++++++--- .../cfg/fixpoints/BackwardCFGFixpoint.java | 2 +- .../program/cfg/fixpoints/CFGFixpoint.java | 2 +- 6 files changed, 62 insertions(+), 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 index 4d7733b07..b3c937bdc 100644 --- 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 the concrete {@link AbstractState} instance - * @param sourceState the {@link AnalysisState} computed at the source of - * this edge + * @param 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 > AnalysisState traverse( - AnalysisState sourceState) + public abstract > AnalysisState traverseForward( + AnalysisState 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 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 > AnalysisState traverseBackwards( + AnalysisState 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 index 1ff9e2dbb..1a28655aa 100644 --- 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 > AnalysisState traverse( - AnalysisState sourceState) + public > AnalysisState traverseForward( + AnalysisState state) throws SemanticException { - ExpressionSet exprs = sourceState.getComputedExpressions(); - AnalysisState result = sourceState.bottom(); + ExpressionSet exprs = state.getComputedExpressions(); + AnalysisState 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 > AnalysisState traverseBackwards( + AnalysisState 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 index b2b571936..50874123a 100644 --- 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 > AnalysisState traverse( - AnalysisState sourceState) { - return sourceState; + public > AnalysisState traverseForward( + AnalysisState state) { + return state; + } + + @Override + public > AnalysisState traverseBackwards( + AnalysisState 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 index 271bba697..29628b2c9 100644 --- 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 > AnalysisState traverse( - AnalysisState sourceState) + public > AnalysisState traverseForward( + AnalysisState state) throws SemanticException { - ExpressionSet exprs = sourceState.getComputedExpressions(); - AnalysisState result = sourceState.bottom(); + ExpressionSet exprs = state.getComputedExpressions(); + AnalysisState 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 > AnalysisState traverseBackwards( + AnalysisState 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 index 3bd38baa5..18731c434 100644 --- 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 traverse( Edge edge, CompoundState entrystate) throws SemanticException { - AnalysisState approx = edge.traverse(entrystate.postState); + AnalysisState approx = edge.traverseBackwards(entrystate.postState); // we remove out of scope variables here List 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 index 61adb67c5..774bf4852 100644 --- 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 traverse( Edge edge, CompoundState entrystate) throws SemanticException { - AnalysisState approx = edge.traverse(entrystate.postState); + AnalysisState approx = edge.traverseForward(entrystate.postState); // we remove out of scope variables here List toRemove = new LinkedList<>();