Add flow sensitivity to constraints and predicate evaluation

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

@@ -92,7 +92,7 @@ public Collection<State> getStatesAtStatement(Statement statement) {
     private Collection<State> getTargetStates(TransitionFunctionImpl transitionFunction) {
         Collection<State> states = new HashSet<>();
 
-        for (Transition transition : transitionFunction.getStateChangeStatements().keySet()) {
+        for (Transition transition : transitionFunction.getStateChangeSequences().keySet()) {
             states.add(transition.to());
         }
 

CryptoAnalysis/src/main/java/crypto/extractparameter/UnknownVal.java

@@ -154,6 +154,26 @@ public long getLongValue() {
         throw new RuntimeException("Unknown Val is not a long constant");
     }
 
+    @Override
+    public boolean isFloatConstant() {
+        return false;
+    }
+
+    @Override
+    public float getFloatValue() {
+        throw new RuntimeException("Unknown Val is not a float constant");
+    }
+
+    @Override
+    public boolean isDoubleConstant() {
+        return false;
+    }
+
+    @Override
+    public double getDoubleValue() {
+        throw new RuntimeException("Unknown Val is not a double constant");
+    }
+
     @Override
     public IArrayRef getArrayBase() {
         throw new RuntimeException("Unknown Val has no array base");

CryptoAnalysis/src/main/java/crypto/predicates/UnEnsuredPredicate.java

@@ -62,7 +62,13 @@ public enum Violations {
          * Violation if there is no dataflow path where the seed reaches an accepting state to
          * generate a predicate.
          */
-        GeneratingStateIsNeverReached
+        GeneratingStateIsNeverReached,
+
+        /**
+         * Violation if an accepting state is reached, but the predicate has an 'after' condition
+         * and the event is not called
+         */
+        GeneratingEventIsNotCalled
     }
 
     public UnEnsuredPredicate(

CryptoAnalysis/src/test/java/test/TestRules.java

@@ -63,6 +63,10 @@ public class TestRules {
 
     public static final String TRANSFORMATION = "transformation";
 
+    public static final String FLOW_SENSITIVITY_CONSTRAINTS = "flowSensitivity/constraints";
+
+    public static final String FLOW_SENSITIVITY_PREDICATES = "flowSensitivity/predicates";
+
     public static final String SEEDS = "seeds";
 
     public static final String ISSUE_314 = "issue314";

CryptoAnalysis/src/test/java/test/TestRunner.java

@@ -66,7 +66,7 @@ public class TestRunner {
     private static final String OPAL = "opal";
 
     /** Use this variable to configure the framework when running the tests locally */
-    private static final String LOCAL_TEST_FRAMEWORK = SOOT;
+    private static final String LOCAL_TEST_FRAMEWORK = SOOT_UP;
 
     private final TestSetup testSetup;
     private final CryptoScanner scanner;

CryptoAnalysis/src/test/java/tests/error/predicate/implication/PredicateImplicationTest.java

@@ -75,7 +75,7 @@ public void testImplicationUnsatisfiedOnReturn() {
 
         // i == 10 => generatedReceiver
         Receiver receiver = generator.generateReceiver();
-        Assertions.notHasEnsuredPredicate(receiver);
+        Assertions.hasEnsuredPredicate(receiver);
 
         // Condition satisfied (true) => predicate has to be ensured (false)
         receiver.condition(10);

CryptoAnalysis/src/test/java/tests/jca/CogniCryptTestGenTest.java

@@ -461,12 +461,10 @@ public void messageDigestInvalidTest11() throws NoSuchAlgorithmException {
     public void messageDigestInvalidTest12() throws NoSuchAlgorithmException, DigestException {
         // Related to issue 296: https://github.com/CROSSINGTUD/CryptoAnalysis/issues/296
         int off = 0;
-        byte[] inByteArr = null;
         int len = 0;
         byte[] out = null;
 
         MessageDigest messageDigest0 = MessageDigest.getInstance("SHA-256");
-        out = messageDigest0.digest(inByteArr);
         // update is skipped
         messageDigest0.digest(out, off, len);
         Assertions.notHasEnsuredPredicate(out);

CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/FlowSensitiveConstraint.java

@@ -0,0 +1,19 @@
+/********************************************************************************
+ * Copyright (c) 2017 Fraunhofer IEM, Paderborn, Germany
+ * <p>
+ * This program and the accompanying materials are made available under the
+ * terms of the Eclipse Public License 2.0 which is available at
+ * http://www.eclipse.org/legal/epl-2.0.
+ * <p>
+ * SPDX-License-Identifier: EPL-2.0
+ ********************************************************************************/
+package tests.misc.flowsensitivity.constraints;
+
+public class FlowSensitiveConstraint {
+
+    public FlowSensitiveConstraint() {}
+
+    public void operation1() {}
+
+    public void operation2(@SuppressWarnings("unused") int i) {}
+}

CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/FlowSensitiveConstraintsTest.java

@@ -0,0 +1,145 @@
+/********************************************************************************
+ * Copyright (c) 2017 Fraunhofer IEM, Paderborn, Germany
+ * <p>
+ * This program and the accompanying materials are made available under the
+ * terms of the Eclipse Public License 2.0 which is available at
+ * http://www.eclipse.org/legal/epl-2.0.
+ * <p>
+ * SPDX-License-Identifier: EPL-2.0
+ ********************************************************************************/
+package tests.misc.flowsensitivity.constraints;
+
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.extension.ExtendWith;
+import test.Ruleset;
+import test.TestRules;
+import test.TestRunnerInterceptor;
+import test.assertions.Assertions;
+
+@ExtendWith(TestRunnerInterceptor.class)
+@Ruleset(TestRules.FLOW_SENSITIVITY_CONSTRAINTS)
+public class FlowSensitiveConstraintsTest {
+
+    private boolean staticallyUnknown() {
+        return Math.random() > 0.5;
+    }
+
+    @Test
+    public void positiveSimpleConstraintsTest() {
+        FlowSensitiveConstraint constraint = new FlowSensitiveConstraint();
+        Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+
+        constraint.operation1();
+        Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+
+        constraint.operation2(10);
+        Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+
+        Assertions.constraintErrors(constraint, 0);
+        Assertions.typestateErrors(constraint, 0);
+        Assertions.incompleteOperationErrors(0);
+    }
+
+    @Test
+    public void negativeSimpleConstraintsTest() {
+        FlowSensitiveConstraint constraint = new FlowSensitiveConstraint();
+        Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+
+        constraint.operation1();
+        Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+
+        // At this point, we violate the constraint; hence, the object is not secure AFTER this
+        // statement
+        constraint.operation2(100);
+        Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint");
+
+        Assertions.constraintErrors(constraint, 1);
+        Assertions.typestateErrors(constraint, 0);
+        Assertions.incompleteOperationErrors(0);
+    }
+
+    @Test
+    public void satisfiedToViolatedConstraint() {
+        OverriddenConstraint constraint = new OverriddenConstraint();
+        Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+
+        // satisfied
+        constraint.operation(10);
+        Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+
+        // violated
+        constraint.operation(100);
+        Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint");
+
+        Assertions.constraintErrors(constraint, 1);
+        Assertions.typestateErrors(constraint, 0);
+        Assertions.incompleteOperationErrors(0);
+    }
+
+    @Test
+    public void violatedToSatisfiedConstraint() {
+        OverriddenConstraint constraint = new OverriddenConstraint();
+        Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+
+        // violated
+        constraint.operation(100);
+        Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint");
+
+        // satisfied
+        constraint.operation(10);
+        Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+
+        Assertions.constraintErrors(constraint, 1);
+        Assertions.typestateErrors(constraint, 0);
+        Assertions.incompleteOperationErrors(0);
+    }
+
+    @Test
+    public void satisfiedToViolatedBranchedConstraint() {
+        OverriddenConstraint constraint = new OverriddenConstraint();
+        Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+
+        if (staticallyUnknown()) {
+            // satisfied
+            constraint.operation(10);
+            Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+        }
+
+        Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+
+        if (staticallyUnknown()) {
+            // violated
+            constraint.operation(100);
+            Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint");
+        }
+
+        // Violated because there is a sequence to the violating call
+        Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint");
+
+        Assertions.constraintErrors(constraint, 1);
+        Assertions.typestateErrors(constraint, 0);
+        Assertions.incompleteOperationErrors(0);
+    }
+
+    @Test
+    public void violatedToSatisfiedBranchedConstraint() {
+        OverriddenConstraint constraint = new OverriddenConstraint();
+        Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+
+        if (staticallyUnknown()) {
+            // violated
+            constraint.operation(100);
+            Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint");
+        }
+
+        Assertions.notHasEnsuredPredicate(constraint, "generatedConstraint");
+
+        // satisfied
+        constraint.operation(10);
+        Assertions.hasEnsuredPredicate(constraint, "generatedConstraint");
+
+        Assertions.constraintErrors(constraint, 1);
+        Assertions.typestateErrors(constraint, 0);
+        Assertions.incompleteOperationErrors(0);
+    }
+}

CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/constraints/OverriddenConstraint.java

@@ -0,0 +1,17 @@
+/********************************************************************************
+ * Copyright (c) 2017 Fraunhofer IEM, Paderborn, Germany
+ * <p>
+ * This program and the accompanying materials are made available under the
+ * terms of the Eclipse Public License 2.0 which is available at
+ * http://www.eclipse.org/legal/epl-2.0.
+ * <p>
+ * SPDX-License-Identifier: EPL-2.0
+ ********************************************************************************/
+package tests.misc.flowsensitivity.constraints;
+
+public class OverriddenConstraint {
+
+    public OverriddenConstraint() {}
+
+    public void operation(@SuppressWarnings("unused") int i) {}
+}

CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateAfterTest.java

@@ -0,0 +1,94 @@
+/********************************************************************************
+ * Copyright (c) 2017 Fraunhofer IEM, Paderborn, Germany
+ * <p>
+ * This program and the accompanying materials are made available under the
+ * terms of the Eclipse Public License 2.0 which is available at
+ * http://www.eclipse.org/legal/epl-2.0.
+ * <p>
+ * SPDX-License-Identifier: EPL-2.0
+ ********************************************************************************/
+package tests.misc.flowsensitivity.predicates;
+
+import org.junit.jupiter.api.Disabled;
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.extension.ExtendWith;
+import test.Ruleset;
+import test.TestRules;
+import test.TestRunnerInterceptor;
+import test.assertions.Assertions;
+
+@ExtendWith(TestRunnerInterceptor.class)
+@Ruleset(TestRules.FLOW_SENSITIVITY_PREDICATES)
+public class PredicateAfterTest {
+
+    private boolean staticallyUnknown() {
+        return Math.random() > 0.5;
+    }
+
+    @Test
+    public void positivePredicateAfterBranchingTest() {
+        PredicateBranching branching = new PredicateBranching();
+        branching.operation1();
+        Assertions.hasEnsuredPredicate(branching, "generatedPredicateBranching");
+
+        branching.operation2();
+        Assertions.hasEnsuredPredicate(branching, "generatedPredicateBranching");
+
+        Assertions.typestateErrors(branching, 0);
+        Assertions.incompleteOperationErrors(0);
+    }
+
+    @Test
+    public void negativePredicateAfterBranchingTest() {
+        PredicateBranching branching = new PredicateBranching();
+        if (staticallyUnknown()) {
+            // After this call, there is only one path with the corresponding event Op1
+            branching.operation1();
+            Assertions.hasEnsuredPredicate(branching, "generatedPredicateBranching");
+        }
+
+        // After this call, there is a sequence where Op1 is not called -> do not ensure predicate
+        branching.operation2();
+        Assertions.notHasEnsuredPredicate(branching, "generatedPredicateBranching");
+
+        Assertions.typestateErrors(branching, 0);
+        Assertions.incompleteOperationErrors(0);
+    }
+
+    @Test
+    public void positivePredicateAfterGeneratedTest() {
+        PredicateGenerator generator = new PredicateGenerator();
+        PredicateReceiver receiver = generator.generate();
+
+        String secret = receiver.generateWord();
+        Assertions.hasEnsuredPredicate(secret, "generatedWord");
+
+        Assertions.typestateErrors(generator, 0);
+        Assertions.typestateErrors(receiver, 0);
+        Assertions.incompleteOperationErrors(0);
+    }
+
+    @Disabled("Requires rework of detection of seeds with multiple definition sites")
+    @Test
+    public void negativePredicateAfterGeneratedTest() {
+        PredicateGenerator generator = new PredicateGenerator();
+        PredicateReceiver receiver = generator.generate();
+
+        String secret = null;
+        if (staticallyUnknown()) {
+            secret = receiver.generateWord();
+            Assertions.hasEnsuredPredicate(secret, "generatedWord");
+        }
+
+        /* TODO
+         *  This requires a new approach because we need to make sure that both
+         *  'secret' definitions (null and generateWord()) define the same seed.
+         *  Note that this holds for seeds with and without rules
+         */
+        Assertions.notHasEnsuredPredicate(secret, "generatedWord");
+
+        Assertions.typestateErrors(generator, 0);
+        Assertions.typestateErrors(receiver, 0);
+        Assertions.incompleteOperationErrors(0);
+    }
+}

CryptoAnalysis/src/test/java/tests/misc/flowsensitivity/predicates/PredicateBranching.java

@@ -0,0 +1,19 @@
+/********************************************************************************
+ * Copyright (c) 2017 Fraunhofer IEM, Paderborn, Germany
+ * <p>
+ * This program and the accompanying materials are made available under the
+ * terms of the Eclipse Public License 2.0 which is available at
+ * http://www.eclipse.org/legal/epl-2.0.
+ * <p>
+ * SPDX-License-Identifier: EPL-2.0
+ ********************************************************************************/
+package tests.misc.flowsensitivity.predicates;
+
+public class PredicateBranching {
+
+    public PredicateBranching() {}
+
+    public void operation1() {}
+
+    public void operation2() {}
+}