Add tests for IncompleteOperationErrors

CryptoAnalysis/src/test/java/test/UsagePatternTestingFramework.java

@@ -61,6 +61,7 @@
 import test.assertions.ExtractedValueAssertion;
 import test.assertions.HasEnsuredPredicateAssertion;
 import test.assertions.InAcceptingStateAssertion;
+import test.assertions.IncompleteOperationErrorCountAssertion;
 import test.assertions.MissingTypestateChange;
 import test.assertions.NoMissingTypestateChange;
 import test.assertions.NotHasEnsuredPredicateAssertion;
@@ -163,18 +164,23 @@ public void visit(TypestateError typestateError) {
 									public void visit(IncompleteOperationError incompleteOperationError) {
 										boolean hasTypestateChangeError = false;
 										boolean expectsTypestateChangeError = false;
-										for(Assertion a: expectedResults){
-											if(a instanceof MissingTypestateChange){
+										for (Assertion a: expectedResults){
+											if (a instanceof MissingTypestateChange) {
 												MissingTypestateChange missingTypestateChange = (MissingTypestateChange) a;
-												if(missingTypestateChange.getStmt().equals(incompleteOperationError.getErrorLocation().getUnit().get())){
+												if (missingTypestateChange.getStmt().equals(incompleteOperationError.getErrorLocation().getUnit().get())) {
 													missingTypestateChange.trigger();
 													hasTypestateChangeError = true;
 												}
 												expectsTypestateChangeError = true;
 											}
-											if(a instanceof NoMissingTypestateChange){
+											if (a instanceof NoMissingTypestateChange) {
 												throw new RuntimeException("Reports a typestate error that should not be reported");
 											}
+
+											if (a instanceof IncompleteOperationErrorCountAssertion) {
+												IncompleteOperationErrorCountAssertion errorCountAssertion = (IncompleteOperationErrorCountAssertion) a;
+												errorCountAssertion.increaseCount();
+											}
 										}
 										if(hasTypestateChangeError != expectsTypestateChangeError){
 											throw new RuntimeException("Reports a typestate error that should not be reported");
@@ -542,6 +548,16 @@ private void extractBenchmarkMethods(SootMethod m, Set<Assertion> queries, Set<S
 				queries.add(new TypestateErrorCountAssertion(queryVar.value));
 			}
 
+			if (invocationName.startsWith("incompleteOperationErrors")) {
+				Value param = invokeExpr.getArg(0);
+				if (!(param instanceof IntConstant)) {
+					continue;
+				}
+
+				IntConstant queryVar = (IntConstant) param;
+				queries.add(new IncompleteOperationErrorCountAssertion(queryVar.value));
+			}
+
 			if (invocationName.startsWith("dependentError")) {
 				// extract parameters
 				List<Value> params = invokeExpr.getArgs();

CryptoAnalysis/src/test/java/test/assertions/Assertions.java

@@ -36,6 +36,8 @@ public static void constraintErrors(int i) {}
 
 	public static void typestateErrors(int i) {}
 
+	public static void incompleteOperationErrors(int i) {}
+
 	public static void dependentError(int thisErrorNr) {}
 
 	public static void dependentError(int thisErrorNr, int precedingError1) {}

CryptoAnalysis/src/test/java/test/assertions/IncompleteOperationErrorCountAssertion.java

@@ -0,0 +1,32 @@
+package test.assertions;
+
+import test.Assertion;
+
+public class IncompleteOperationErrorCountAssertion implements Assertion {
+
+    private int expectedErrorCounts;
+    private int actualErrorCounts;
+
+    public IncompleteOperationErrorCountAssertion(int numberOfCounts) {
+        this.expectedErrorCounts = numberOfCounts;
+    }
+
+    public void increaseCount(){
+        actualErrorCounts++;
+    }
+
+    @Override
+    public boolean isSatisfied() {
+        return expectedErrorCounts <= actualErrorCounts;
+    }
+
+    @Override
+    public boolean isImprecise() {
+        return expectedErrorCounts != actualErrorCounts;
+    }
+
+    @Override
+    public String toString() {
+        return "Expected " + expectedErrorCounts + " incomplete operation errors, but got " + actualErrorCounts;
+    }
+}

CryptoAnalysis/src/test/java/tests/custom/incompleteoperation/IncompleteOperationTest.java

@@ -0,0 +1,115 @@
+package tests.custom.incompleteoperation;
+
+import crypto.analysis.CrySLRulesetSelector.Ruleset;
+import org.junit.Test;
+import test.UsagePatternTestingFramework;
+import test.assertions.Assertions;
+
+public class IncompleteOperationTest extends UsagePatternTestingFramework {
+
+    @Override
+    public Ruleset getRuleSet() {
+        return Ruleset.CustomRules;
+    }
+
+    @Override
+    public String getRulesetPath() {
+        return "incompleteOperation";
+    }
+
+    @Test
+    public void testNoIncompleteOperation() {
+        Operations operations1 = new Operations();
+        operations1.operation1();
+        operations1.operation2();
+        operations1.operation3();
+        operations1.operation4();
+
+        Operations operations2 = new Operations();
+        operations2.operation1();
+        operations2.operation2();
+        operations2.operation3();
+        // operation 4 is optional, i.e. no incomplete operation
+
+        Assertions.incompleteOperationErrors(0);
+    }
+
+    @Test
+    public void testMissingOperation() {
+        Operations operations = new Operations();
+        operations.operation1();
+        operations.operation2();
+        // operation3 is missing
+
+        Assertions.incompleteOperationErrors(1);
+    }
+
+    @Test
+    public void testSingleDataflowPathWithIncompleteOperation() {
+        Operations operations = new Operations();
+        operations.operation1();
+        operations.operation2();
+
+        // Dataflow path without operation3 exists => incomplete operation
+        if (Math.random() > 0.5) {
+            operations.operation3();
+        }
+
+        Assertions.incompleteOperationErrors(1);
+    }
+
+    @Test
+    public void testMultipleDataflowPathsWithIncompleteOperations() {
+        Operations operations = new Operations();
+        operations.operation1();
+
+        // On both dataflow paths a call two operation3 is missing => 2 incomplete operations
+        if (Math.random() > 0.5) {
+            operations.operation2();
+        } else {
+            operations.operation2();
+        }
+
+        Assertions.incompleteOperationErrors(2);
+    }
+
+    @Test
+    public void testMultipleDataflowPathsWithoutIncompleteOperations() {
+        Operations operations = new Operations();
+        operations.operation1();
+
+        // Both dataflow path are completed with operation3
+        if (Math.random() > 0.5) {
+            operations.operation2();
+        } else {
+            operations.operation2();
+        }
+        operations.operation3();
+
+        Assertions.incompleteOperationErrors(0);
+    }
+
+    @Test
+    public void testIncompleteOperationWithLoops() {
+        Operations operations1 = new Operations();
+        operations1.operation1();
+        operations1.operation2();
+
+        // Dataflow path without call to operation3
+        while (Math.random() > 0.5) {
+            operations1.operation3();
+        }
+
+        Operations operations2 = new Operations();
+        operations2.operation1();
+        operations2.operation2();
+
+        // Dataflow path without call to operation3
+        for (int i = 0; i < 1; i++) {
+            operations2.operation3();
+        }
+
+        Assertions.incompleteOperationErrors(2);
+    }
+
+}

CryptoAnalysis/src/test/java/tests/custom/incompleteoperation/Operations.java

@@ -0,0 +1,12 @@
+package tests.custom.incompleteoperation;
+
+public class Operations {
+
+    public void operation1() {}
+
+    public void operation2() {}
+
+    public void operation3() {}
+
+    public void operation4() {}
+}

CryptoAnalysis/src/test/resources/testrules/incompleteOperation/Operations.crysl

@@ -0,0 +1,11 @@
+SPEC tests.custom.incompleteoperation.Operations
+
+EVENTS
+    Con: Operations();
+    op1: operation1();
+    op2: operation2();
+    op3: operation3();
+    op4: operation4();
+
+ORDER
+    Con, op1, op2, op3, op4*