Simply TypestateError detection and rework corresponding test assertions

CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java

@@ -8,7 +8,6 @@
 import boomerang.scene.Val;
 import com.google.common.collect.HashMultimap;
 import com.google.common.collect.Multimap;
-import com.google.common.collect.Sets;
 import com.google.common.collect.Table;
 import crypto.analysis.errors.AbstractConstraintsError;
 import crypto.analysis.errors.ForbiddenMethodError;
@@ -50,9 +49,7 @@ public class AnalysisSeedWithSpecification extends IAnalysisSeed {
     private final ConstraintsAnalysis constraintsAnalysis;
     private boolean internalConstraintsSatisfied;
 
-    private final Multimap<Statement, State> typeStateChange = HashMultimap.create();
     private final Collection<Statement> allCallsOnObject;
-
     private final Multimap<Statement, Integer> relevantStatements = HashMultimap.create();
     private final Collection<AbstractPredicate> indirectlyEnsuredPredicates = new HashSet<>();
 
@@ -141,50 +138,29 @@ private Optional<CrySLForbiddenMethod> isForbiddenMethod(DeclaredMethod declared
         return Optional.empty();
     }
 
+    /**
+     * Check the ORDER section and report a corresponding {@link TypestateError} for each sequence
+     * of statements that visits a {@link ReportingErrorStateNode}
+     */
     private void evaluateTypestateOrder() {
-        Collection<ControlFlowGraph.Edge> allTypestateChangeStatements = new HashSet<>();
-        for (Table.Cell<ControlFlowGraph.Edge, Val, TransitionFunction> cell :
-                analysisResults.asEdgeValWeightTable().cellSet()) {
-            Collection<ControlFlowGraph.Edge> edges =
-                    cell.getValue().getLastStateChangeStatements();
-            allTypestateChangeStatements.addAll(edges);
-        }
-
-        for (Table.Cell<ControlFlowGraph.Edge, Val, TransitionFunction> c :
-                analysisResults.asEdgeValWeightTable().cellSet()) {
-            ControlFlowGraph.Edge curr = c.getRowKey();
-
-            // The initial statement is always the start of the CFG edge, all other statements are
-            // targets
-            Statement typestateChangeStatement;
-            if (curr.getStart().equals(getOrigin())) {
-                typestateChangeStatement = curr.getStart();
-            } else {
-                typestateChangeStatement = curr.getTarget();
-            }
-
-            if (allTypestateChangeStatements.contains(curr)) {
-                Collection<? extends State> targetStates = getTargetStates(c.getValue());
-
-                for (State newStateAtCurr : targetStates) {
-                    typeStateChangeAtStatement(typestateChangeStatement, newStateAtCurr);
+        for (Statement statement : allCallsOnObject) {
+            Collection<State> statesAtStatement = getStatesAtStatement(statement);
+            for (State state : statesAtStatement) {
+                if (state instanceof ReportingErrorStateNode errorStateNode) {
+                    TypestateError typestateError =
+                            new TypestateError(
+                                    this, statement, specification, errorStateNode.expectedCalls());
+                    this.addError(typestateError);
+                    scanner.getAnalysisReporter().reportError(this, typestateError);
                 }
             }
         }
     }
 
-    private void typeStateChangeAtStatement(Statement statement, State stateNode) {
-        if (typeStateChange.put(statement, stateNode)) {
-            if (stateNode instanceof ReportingErrorStateNode errorStateNode) {
-                TypestateError typestateError =
-                        new TypestateError(
-                                this, statement, specification, errorStateNode.expectedCalls());
-                this.addError(typestateError);
-                scanner.getAnalysisReporter().reportError(this, typestateError);
-            }
-        }
-    }
-
+    /**
+     * Check the ORDER section and report a corresponding {@link IncompleteOperationError} for each
+     * sequence of statements that do not end in an accepting state
+     */
     private void evaluateIncompleteOperations() {
         Table<ControlFlowGraph.Edge, Val, TransitionFunction> endPathOfPropagation =
                 analysisResults.getObjectDestructingStatements();
@@ -445,12 +421,7 @@ private void propagatePredicate(
             if (allStatesNonGenerating) {
                 allViolations.add(UnEnsuredPredicate.Violations.GeneratingStateIsNeverReached);
             } else if (someStatesNonGenerating) {
-                /* TODO
-                 *  Due to a bug, IDEal returns the states [0,1] whenever there is a
-                 *  single call to a method, e.g. Object o = new Object(); o.m();. After
-                 *  the call to m1(), o is always in state 0 and 1, although it should only be 1
-                 */
-                // allViolations.add(UnEnsuredPredicate.Violations.GeneratingStateMayNotBeReached);
+                allViolations.add(UnEnsuredPredicate.Violations.GeneratingStateMayNotBeReached);
             }
 
             if (isIndirectlyEnsured) {
@@ -670,31 +641,6 @@ private boolean doesStateGeneratePredicate(State state, CrySLPredicate predicate
                 && !isPredicateNegatingState(predicate, state);
     }
 
-    private Collection<State> getStatesAtStatement(Statement statement) {
-        Collection<State> states = new HashSet<>();
-
-        if (statement.containsInvokeExpr()) {
-            Collection<TransitionFunction> functions =
-                    statementValWeightTable.row(statement).values();
-
-            for (TransitionFunction function : functions) {
-                Collection<State> targets = getTargetStates(function);
-
-                states.addAll(targets);
-            }
-        }
-
-        return states;
-    }
-
-    private Collection<State> getTargetStates(TransitionFunction value) {
-        Collection<State> res = Sets.newHashSet();
-        for (ITransition t : value.values()) {
-            if (t.to() != null) res.add(t.to());
-        }
-        return res;
-    }
-
     private boolean isPredicateGeneratingState(CrySLPredicate ensPred, State stateNode) {
         // Predicate has a condition, i.e. "after" is specified -> Active predicate for
         // corresponding states

CryptoAnalysis/src/main/java/crypto/analysis/IAnalysisSeed.java

@@ -20,6 +20,8 @@
 import java.util.Objects;
 import java.util.Optional;
 import typestate.TransitionFunction;
+import typestate.finiteautomata.ITransition;
+import typestate.finiteautomata.State;
 
 public abstract class IAnalysisSeed implements IPredicateCheckListener {
 
@@ -62,6 +64,30 @@ public Collection<Val> getAliasesAtStatement(Statement statement) {
         return statementValWeightTable.row(statement).keySet();
     }
 
+    public Collection<State> getStatesAtStatement(Statement statement) {
+        Collection<State> states = new HashSet<>();
+
+        Collection<TransitionFunction> transitions =
+                statementValWeightTable.row(statement).values();
+        for (TransitionFunction transition : transitions) {
+            Collection<State> targetStates = getTargetStates(transition);
+
+            states.addAll(targetStates);
+        }
+
+        return states;
+    }
+
+    private Collection<State> getTargetStates(TransitionFunction transitionFunction) {
+        Collection<State> states = new HashSet<>();
+
+        for (ITransition transition : transitionFunction.values()) {
+            states.add(transition.to());
+        }
+
+        return states;
+    }
+
     public void addPredicateStateChangeListener(IPredicateStateChangeListener listener) {
         predicateStateChangeListeners.add(listener);
     }

CryptoAnalysis/src/main/java/crypto/analysis/SeedGenerator.java

@@ -1,13 +1,11 @@
 package crypto.analysis;
 
 import boomerang.results.ForwardBoomerangResults;
-import boomerang.scene.CallGraph;
-import boomerang.scene.DataFlowScope;
 import boomerang.scene.Statement;
 import boomerang.scene.Val;
+import crypto.definition.Definitions;
 import crypto.typestate.ForwardSeedQuery;
 import crypto.typestate.TypestateAnalysis;
-import crypto.typestate.TypestateDefinition;
 import crysl.rule.CrySLRule;
 import java.util.Collection;
 import java.util.Collections;
@@ -23,29 +21,12 @@ public class SeedGenerator {
     public SeedGenerator(CryptoScanner scanner, Collection<CrySLRule> rules) {
         this.scanner = scanner;
 
-        TypestateDefinition definition =
-                new TypestateDefinition() {
-                    @Override
-                    public Collection<CrySLRule> getRuleset() {
-                        return rules;
-                    }
-
-                    @Override
-                    public CallGraph getCallGraph() {
-                        return scanner.getCallGraph();
-                    }
-
-                    @Override
-                    public DataFlowScope getDataFlowScope() {
-                        return scanner.getDataFlowScope();
-                    }
-
-                    @Override
-                    public int getTimeout() {
-                        return scanner.getTimeout();
-                    }
-                };
-
+        Definitions.TypestateDefinition definition =
+                new Definitions.TypestateDefinition(
+                        rules,
+                        scanner.getCallGraph(),
+                        scanner.getDataFlowScope(),
+                        scanner.getTimeout());
         typestateAnalysis = new TypestateAnalysis(definition);
     }
 

CryptoAnalysis/src/main/java/crypto/definition/Definitions.java

@@ -4,6 +4,8 @@
 import boomerang.scene.DataFlowScope;
 import boomerang.scene.sparse.SparseCFGCache;
 import crypto.listener.AnalysisReporter;
+import crysl.rule.CrySLRule;
+import java.util.Collection;
 
 public interface Definitions {
 
@@ -14,6 +16,12 @@ record SeedDefinition(
             SparseCFGCache.SparsificationStrategy strategy,
             AnalysisReporter reporter) {}
 
+    record TypestateDefinition(
+            Collection<CrySLRule> rules,
+            CallGraph callGraph,
+            DataFlowScope dataFlowScope,
+            int timeout) {}
+
     record ConstraintsDefinition(
             CallGraph callGraph,
             DataFlowScope dataFlowScope,

CryptoAnalysis/src/main/java/crypto/typestate/ErrorStateNode.java

@@ -2,9 +2,25 @@
 
 import typestate.finiteautomata.State;
 
+/**
+ * Final error state that cannot be left. All ingoing transitions should originate from a {@link
+ * ReportingErrorStateNode}.
+ */
 public class ErrorStateNode implements State {
 
-    public ErrorStateNode() {}
+    public static final String LABEL = "ERR (final)";
+
+    private static ErrorStateNode errorState;
+
+    private ErrorStateNode() {}
+
+    public static ErrorStateNode getInstance() {
+        if (errorState == null) {
+            errorState = new ErrorStateNode();
+        }
+
+        return errorState;
+    }
 
     @Override
     public boolean isErrorState() {
@@ -23,7 +39,7 @@ public boolean isAccepting() {
 
     @Override
     public String toString() {
-        return "ERR";
+        return LABEL;
     }
 
     @Override

CryptoAnalysis/src/main/java/crypto/typestate/ForwardSeedQuery.java

@@ -40,6 +40,6 @@ public CrySLRule getRule() {
     }
 
     public Collection<LabeledMatcherTransition> getAllTransitions() {
-        return transitions.getAllTransitions();
+        return transitions.getStateMachineTransitions();
     }
 }