diff --git a/CryptoAnalysis/src/test/java/test/UsagePatternTestingFramework.java b/CryptoAnalysis/src/test/java/test/UsagePatternTestingFramework.java index d58c41dfb..b00d33406 100644 --- a/CryptoAnalysis/src/test/java/test/UsagePatternTestingFramework.java +++ b/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 queries, Set params = invokeExpr.getArgs(); diff --git a/CryptoAnalysis/src/test/java/test/assertions/Assertions.java b/CryptoAnalysis/src/test/java/test/assertions/Assertions.java index 9b604e7f1..ad79d161a 100644 --- a/CryptoAnalysis/src/test/java/test/assertions/Assertions.java +++ b/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) {} diff --git a/CryptoAnalysis/src/test/java/test/assertions/IncompleteOperationErrorCountAssertion.java b/CryptoAnalysis/src/test/java/test/assertions/IncompleteOperationErrorCountAssertion.java new file mode 100644 index 000000000..ea63ddd0b --- /dev/null +++ b/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; + } +} diff --git a/CryptoAnalysis/src/test/java/tests/custom/incompleteoperation/IncompleteOperationTest.java b/CryptoAnalysis/src/test/java/tests/custom/incompleteoperation/IncompleteOperationTest.java new file mode 100644 index 000000000..7f658393f --- /dev/null +++ b/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); + } + +} diff --git a/CryptoAnalysis/src/test/java/tests/custom/incompleteoperation/Operations.java b/CryptoAnalysis/src/test/java/tests/custom/incompleteoperation/Operations.java new file mode 100644 index 000000000..50465e0fe --- /dev/null +++ b/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() {} +} diff --git a/CryptoAnalysis/src/test/resources/testrules/incompleteOperation/Operations.crysl b/CryptoAnalysis/src/test/resources/testrules/incompleteOperation/Operations.crysl new file mode 100644 index 000000000..b363a5a52 --- /dev/null +++ b/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*