Merge pull request #671 from CROSSINGTUD/fix/issue-215

Adapt test case from #215
CROSSINGTUD · Jul 22, 2024 · 92702a7 · 92702a7
2 parents 15eafcc + aba497f
commit 92702a7
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 24 deletions.
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java
@@ -162,33 +162,26 @@ private Optional<CrySLForbiddenMethod> isForbiddenMethod(DeclaredMethod declared
 	private void evaluateTypestateOrder() {
 		Collection<ControlFlowGraph.Edge> allTypestateChangeStatements = new HashSet<>();
 		for (Table.Cell<ControlFlowGraph.Edge, Val, TransitionFunction> cell : analysisResults.asStatementValWeightTable().cellSet()) {
-			allTypestateChangeStatements.addAll(cell.getValue().getLastStateChangeStatements());
+			Collection<ControlFlowGraph.Edge> edges = cell.getValue().getLastStateChangeStatements();
+			allTypestateChangeStatements.addAll(edges);
 		}
 
 		for (Table.Cell<ControlFlowGraph.Edge, Val, TransitionFunction> c : analysisResults.asStatementValWeightTable().cellSet()) {
 			ControlFlowGraph.Edge curr = c.getRowKey();
 
-			// For some reason, constructors are the start and not the target statement...
-			Statement errorStatement;
-			Statement start = curr.getStart();
-			Statement target = curr.getTarget();
-			if (start.containsInvokeExpr()) {
-				DeclaredMethod declaredMethod = start.getInvokeExpr().getMethod();
-
-				if (declaredMethod.isConstructor()) {
-					errorStatement = start;
-				} else {
-					errorStatement = target;
-				}
+			// 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 {
-				errorStatement = target;
+				typestateChangeStatement = curr.getTarget();
 			}
 
 			if (allTypestateChangeStatements.contains(curr)) {
 				Collection<? extends State> targetStates = getTargetStates(c.getValue());
 
 				for (State newStateAtCurr : targetStates) {
-					typeStateChangeAtStatement(errorStatement, newStateAtCurr);
+					typeStateChangeAtStatement(typestateChangeStatement, newStateAtCurr);
 				}
 			}
 		}
@@ -465,7 +458,7 @@ private boolean containsTargetState(TransitionFunction value, State stateNode) {
 		return getTargetStates(value).contains(stateNode);
 	}
 
-	private Collection<? extends State> getTargetStates(TransitionFunction value) {
+	private Collection<State> getTargetStates(TransitionFunction value) {
 		Collection<State> res = Sets.newHashSet();
 		for (ITransition t : value.values()) {
 			if (t.to() != null)

diff --git a/CryptoAnalysis/src/main/java/crypto/typestate/MatcherTransitionCollection.java b/CryptoAnalysis/src/main/java/crypto/typestate/MatcherTransitionCollection.java
@@ -85,11 +85,7 @@ private TransitionFunction getDefaultTransitionFunction(ControlFlowGraph.Edge st
         return new TransitionFunction(initialTransitions, Collections.singleton(stmt));
     }
 
-    public Collection<TransitionEdge> getInitialTransitions() {
-        return smg.getInitialTransitions();
-    }
-
-    public Set<LabeledMatcherTransition> getAllTransitions() {
+    public Collection<LabeledMatcherTransition> getAllTransitions() {
         return transitions;
     }
 
@@ -115,18 +111,18 @@ private void initializeErrorTransitions() {
 
         for (StateNode node : smg.getNodes()) {
             // Collect the methods that are on an outgoing edge
-            Set<CrySLMethod> existingMethods = new HashSet<>();
+            Collection<CrySLMethod> existingMethods = new HashSet<>();
             for (TransitionEdge edge : smg.getAllOutgoingEdges(node)) {
                 existingMethods.addAll(edge.getLabel());
             }
 
             // Remove the existing methods; all remaining methods lead to an error state
-            Set<CrySLMethod> remainingMethods = new HashSet<>(allMethods);
+            Collection<CrySLMethod> remainingMethods = new HashSet<>(allMethods);
             remainingMethods.removeAll(existingMethods);
 
             // Create the error state, where typestate errors are reported
             WrappedState state = createWrappedState(node);
-            ReportingErrorStateNode repErrorState = new ReportingErrorStateNode(remainingMethods);
+            ReportingErrorStateNode repErrorState = new ReportingErrorStateNode(existingMethods);
             LabeledMatcherTransition repErrorTransition = new LabeledMatcherTransition(state, remainingMethods, repErrorState);
             transitions.add(repErrorTransition);
 

diff --git a/CryptoAnalysis/src/test/java/tests/jca/BouncyCastleTest.java b/CryptoAnalysis/src/test/java/tests/jca/BouncyCastleTest.java
@@ -117,6 +117,9 @@ public void testORingTwoPredicates2() throws IllegalStateException, InvalidCiphe
 		GCMBlockCipher cipher1 = (GCMBlockCipher) GCMBlockCipher.newInstance(engine);
 		cipher1.init(false, params);
 		cipher1.processAADBytes(input, 0, input.length);
+		Assertions.hasEnsuredPredicate(cipher1);
+
+		// Missing call to 'processBytes' causes TypestateError -> No predicate at 'doFinal' call
 		cipher1.doFinal(output, 0);
 		Assertions.notHasEnsuredPredicate(cipher1);
 		Assertions.mustNotBeInAcceptingState(cipher1);