Merge pull request #517 from CROSSINGTUD/fix/final_predicate_check

Add final predicate check
CROSSINGTUD · Jan 15, 2024 · 10948c6 · 10948c6
2 parents 32ade39 + 01e7000
commit 10948c6
Show file tree

Hide file tree

Showing 8 changed files with 90 additions and 6 deletions.
diff --git a/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java b/CryptoAnalysis/src/main/java/crypto/analysis/AnalysisSeedWithSpecification.java
@@ -371,15 +371,14 @@ private Collection<? extends State> getTargetStates(TransitionFunction value) {
 
 	private boolean checkConstraintSystem() {
 		cryptoScanner.getAnalysisListener().beforePredicateCheck(this);
-		Set<ISLConstraint> relConstraints = constraintSolver.getRelConstraints();
-		boolean checkPredicates = checkPredicates(relConstraints);
+		boolean checkPredicates = checkPredicates();
 		cryptoScanner.getAnalysisListener().afterPredicateCheck(this);
 		if (!checkPredicates)
 			return false;
 		return internalConstraintSatisfied;
 	}
 
-	private boolean checkPredicates(Collection<ISLConstraint> relConstraints) {
+	public boolean checkPredicates() {
 		List<ISLConstraint> requiredPredicates = Lists.newArrayList();
 		for (ISLConstraint con : constraintSolver.getRequiredPredicates()) {
 			if (!ConstraintSolver.predefinedPreds.contains((con instanceof RequiredCrySLPredicate) ? ((RequiredCrySLPredicate) con).getPred().getPredName()

diff --git a/CryptoAnalysis/src/main/java/crypto/predicates/PredicateHandler.java b/CryptoAnalysis/src/main/java/crypto/predicates/PredicateHandler.java
@@ -221,6 +221,8 @@ public void checkPredicates() {
 
 	private void checkMissingRequiredPredicates() {
 		for (AnalysisSeedWithSpecification seed : cryptoScanner.getAnalysisSeeds()) {
+			seed.checkPredicates();
+
 			Set<ISLConstraint> missingPredicates = seed.getMissingPredicates();
 			for (ISLConstraint pred : missingPredicates) {
 				if (pred instanceof RequiredCrySLPredicate) {

diff --git a/CryptoAnalysis/src/test/java/tests/custom/issue318/First.java b/CryptoAnalysis/src/test/java/tests/custom/issue318/First.java
@@ -0,0 +1,8 @@
+package tests.custom.issue318;
+
+public class First {
+
+    public First() {}
+
+    public void read() {}
+}
diff --git a/CryptoAnalysis/src/test/java/tests/custom/issue318/Issue318Test.java b/CryptoAnalysis/src/test/java/tests/custom/issue318/Issue318Test.java
@@ -0,0 +1,35 @@
+package tests.custom.issue318;
+
+import crypto.analysis.CrySLRulesetSelector;
+import org.junit.Test;
+import test.UsagePatternTestingFramework;
+import test.assertions.Assertions;
+
+public class Issue318Test extends UsagePatternTestingFramework {
+
+    @Override
+    protected CrySLRulesetSelector.Ruleset getRuleSet() {
+        return CrySLRulesetSelector.Ruleset.CustomRules;
+    }
+
+    @Override
+    protected String getRulesetPath() {
+        return "issue318";
+    }
+
+    @Test
+    public void testIssue318() {
+        First f = new First();
+        Assertions.notHasEnsuredPredicate(f);
+
+        Second s = new Second(f);
+        Assertions.notHasEnsuredPredicate(s);
+
+        f.read();
+        s.goOn();
+        Assertions.hasEnsuredPredicate(f);
+        Assertions.notHasEnsuredPredicate(s);
+
+        Assertions.predicateErrors(1);
+    }
+}
diff --git a/CryptoAnalysis/src/test/java/tests/custom/issue318/Second.java b/CryptoAnalysis/src/test/java/tests/custom/issue318/Second.java
@@ -0,0 +1,12 @@
+package tests.custom.issue318;
+
+public class Second {
+
+    private First f;
+
+    public Second(First f) {
+        this.f = f;
+    }
+
+    public void goOn() {}
+}
diff --git a/CryptoAnalysis/src/test/java/tests/headless/BouncyCastleHeadlessTest.java b/CryptoAnalysis/src/test/java/tests/headless/BouncyCastleHeadlessTest.java
@@ -224,7 +224,7 @@ public void testBCEllipticCurveExamples() {
 				.withTPs(RequiredPredicateError.class, 3)
 				.build());
 		setErrorsCount(new ErrorSpecification.Builder("<transforms.ECFixedTransformTest: void testSix(java.lang.String)>")
-				.withTPs(RequiredPredicateError.class, 2)
+				.withTPs(RequiredPredicateError.class, 3)
 				.withTPs(IncompleteOperationError.class, 1)
 				.build());
 
@@ -233,7 +233,7 @@ public void testBCEllipticCurveExamples() {
 				.build());
 		setErrorsCount(new ErrorSpecification.Builder("<transforms.ECNewPublicKeyTransformTest: void testFour(java.lang.String)>")
 				.withTPs(IncompleteOperationError.class, 1)
-				.withTPs(RequiredPredicateError.class, 3)
+				.withTPs(RequiredPredicateError.class, 4)
 				.build());
 		setErrorsCount(new ErrorSpecification.Builder("<transforms.ECNewPublicKeyTransformTest: void testFive(java.lang.String)>")
 				.withTPs(RequiredPredicateError.class, 4)
@@ -253,7 +253,7 @@ public void testBCEllipticCurveExamples() {
 				.build());
 		setErrorsCount(new ErrorSpecification.Builder("<transforms.ECNewRandomessTransformTest: void testFour(java.lang.String)>")
 				.withTPs(IncompleteOperationError.class, 1)
-				.withTPs(RequiredPredicateError.class, 3)
+				.withTPs(RequiredPredicateError.class, 4)
 				.build());
 		setErrorsCount(new ErrorSpecification.Builder("<transforms.ECNewRandomessTransformTest: void testFive(java.lang.String)>")
 				.withTPs(RequiredPredicateError.class, 4)

diff --git a/CryptoAnalysis/src/test/resources/testrules/issue318/First.crysl b/CryptoAnalysis/src/test/resources/testrules/issue318/First.crysl
@@ -0,0 +1,14 @@
+SPEC tests.custom.issue318.First
+
+OBJECTS
+	tests.custom.issue318.First f;
+
+EVENTS
+	c: f = First();
+	r: read();
+
+ORDER
+	c, r
+
+ENSURES
+	first[this] after r;
diff --git a/CryptoAnalysis/src/test/resources/testrules/issue318/Second.crysl b/CryptoAnalysis/src/test/resources/testrules/issue318/Second.crysl
@@ -0,0 +1,14 @@
+SPEC tests.custom.issue318.Second
+
+OBJECTS
+	tests.custom.issue318.First f;
+
+EVENTS
+	c: Second(f);
+	g: goOn();
+
+ORDER
+	c, g
+
+REQUIRES
+	first[f];