Add tests for symex condition propagation

Author: smowton

jbmc/regression/jbmc/exception-cleanup/Test.class

@@ -0,0 +1,44 @@
+public class Test {
+
+  public static void main(int unknown) {
+
+    try {
+      mayThrow(unknown % 7 == 5);
+    }
+    catch(Exception e) {
+    }
+
+    // This test checks that symex can tell there is no exception in flight
+    // (i.e. @inflight_exception is null) at this point, requiring it to
+    // converge the `if @inflight_exception == null` test on mayThrow's return
+    // with the explicit `@inflight_exception = null;` assignment that concludes
+    // the catch block.
+
+    // If it knows that, it will also know the following catch block is
+    // unreachable; if not it will pursue both paths.
+    try {
+      mayThrow(false);
+    }
+    catch(Exception e) {
+      unreachable();
+    }
+
+    // Try it once more, to check we also know after an unreachable catch that
+    // there is still no inflight exception
+    try {
+      mayThrow(false);
+    }
+    catch(Exception e) {
+      unreachable();
+    }
+
+  }
+
+  public static void mayThrow(boolean shouldThrow) throws Exception {
+    if(shouldThrow)
+      throw new Exception();
+  }
+
+  public static void unreachable() { assert false; }
+
+}

jbmc/regression/jbmc/exception-cleanup/Test.java

@@ -0,0 +1,14 @@
+CORE
+Test.class
+--function Test.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+1 remaining after simplification$
+--
+^warning: ignoring
+--
+The function "unreachable" should be successfully noted as unreachable by symex,
+but the final uncaught-exception test in __CPROVER__start is not yet decidable
+in symex, as it requires symex to note that within a catch block
+@inflight_exception is definitely *not* null, which it can't just yet.

jbmc/regression/jbmc/exception-cleanup/test.desc

@@ -0,0 +1,15 @@
+CORE
+Test.class
+--function Test.main --show-vcc
+^EXIT=0$
+^SIGNAL=0$
+file Test\.java line 6 function java::Test.main:\(I\)V
+no uncaught exception
+--
+file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5
+assertion at file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5
+java::Test\.unreachable:\(\)V
+^warning: ignoring
+--
+Supplemental to test.desc, check that the right condition remains to be tested by the solver,
+and the unreachable function indeed does not occur in the VCCs.

jbmc/regression/jbmc/exception-cleanup/vccs.desc

@@ -0,0 +1,5 @@
+int main(int argc, char **argv)
+{
+  if(argc == 1)
+    assert(argc == 1);
+}

regression/cbmc/condition-propagation-1/test.c

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

regression/cbmc/condition-propagation-1/test.desc

@@ -0,0 +1,5 @@
+int main(int argc, char **argv)
+{
+  __CPROVER_assume(argc == 1);
+  assert(argc == 1);
+}

regression/cbmc/condition-propagation-2/test.c

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

regression/cbmc/condition-propagation-2/test.desc

@@ -0,0 +1,10 @@
+int main(int argc, char **argv)
+{
+  if(argc != 1)
+  {
+  }
+  else
+  {
+    assert(argc == 1);
+  }
+}

regression/cbmc/condition-propagation-3/test.c

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

regression/cbmc/condition-propagation-3/test.desc

@@ -0,0 +1,15 @@
+int main(int argc, char **argv)
+{
+  int unknown;
+
+  if(argc != 1)
+  {
+  }
+  else
+  {
+    if(unknown == argc)
+    {
+      assert(unknown == 1);
+    }
+  }
+}

regression/cbmc/condition-propagation-4/test.c

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.