Filter value sets in symex

jbmc/regression/jbmc/virtual_filter_value_sets/test_with_deref.desc

@@ -0,0 +1,18 @@
+CORE
+virtual_filter_value_sets.class
+--show-vcc --function virtual_filter_value_sets.test_with_deref
+^EXIT=0$
+^SIGNAL=0$
+java::B\.f:\(\)I#return_value!0#.* = 9$
+--
+java::B\.f:\(\)I#return_value!0#.* = .*byte_extract_.*_endian
+^warning: ignoring
+--
+When B.f is called on `c.a_field`, it is guarded by a conditional which implies
+that `c.a_field` must be a B. Symex should filter the value set for `c.a_field`
+to remove anything which doesn't satisfy that condition. It will then be able
+to determine that the return value of B.f is 9. If it thinks that `c.a_field`
+might contain an A then it will create a more complicated expression for the
+return value of B.f, which will include byte_extract_little_endian or
+byte_extract_big_endian, as this is what it will produce when trying to read
+the field `int flag` from a class that doesn't have any fields.

jbmc/regression/jbmc/virtual_filter_value_sets/test_without_deref.desc

@@ -0,0 +1,18 @@
+CORE
+virtual_filter_value_sets.class
+--show-vcc --function virtual_filter_value_sets.test_without_deref
+^EXIT=0$
+^SIGNAL=0$
+java::B\.f:\(\)I#return_value!0#.* = 9$
+--
+java::B\.f:\(\)I#return_value!0#.* = .*byte_extract_.*_endian
+^warning: ignoring
+--
+When B.f is called on `a_or_b`, it is guarded by a conditional which implies
+that `a_or_b` must be a B. Symex should filter the value set for `a_or_b` to
+remove anything which doesn't satisfy that condition. It will then be able
+to determine that the return value of B.f is 9. If it thinks that `a_or_b`
+might contain an A then it will create a more complicated expression for the
+return value of B.f, which will include byte_extract_little_endian or
+byte_extract_big_endian, as this is what it will produce when trying to read
+the field `int flag` from a class that doesn't have any fields.

jbmc/regression/jbmc/virtual_filter_value_sets/virtual_filter_value_sets.java

@@ -0,0 +1,40 @@
+class A {
+  public int f() { return 1; }
+};
+
+class B extends A {
+  public int flag;
+
+  public int f() { return flag; }
+};
+
+class Container {
+  public A a_field;
+}
+
+class virtual_filter_value_sets {
+  public static void test_without_deref(boolean nondet_bool) {
+    A a = new A();
+
+    B b = new B();
+    b.flag = 9;
+
+    A a_or_b = nondet_bool ? a : b;
+    int retval = a_or_b.f();
+
+    assert false;
+  }
+
+  public static void test_with_deref(boolean nondet_bool) {
+    A a = new A();
+
+    B b = new B();
+    b.flag = 9;
+
+    Container c = new Container();
+    c.a_field = nondet_bool ? a : b;
+    int retval = c.a_field.f();
+
+    assert false;
+  }
+}

regression/cbmc/CMakeLists.txt

@@ -5,7 +5,7 @@ add_test_pl_tests(
 add_test_pl_profile(
     "cbmc-paths-lifo"
     "$<TARGET_FILE:cbmc> --paths lifo"
-    "-C;-X;thorough-paths;-X;smt-backend;-s;paths-lifo"
+    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;-s;paths-lifo"
     "CORE"
 )
 

regression/cbmc/Makefile

@@ -7,7 +7,7 @@ test-cprover-smt2:
 	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend
 
 test-paths-lifo:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend -X paths-lifo-expected-failure
 
 tests.log: ../test.pl test
 

regression/cbmc/symex_should_exclude_null_pointers/main.c

@@ -1,16 +1,22 @@
+#include <assert.h>
+
 static void noop() { }
 
 int main(int argc, char **argv) {
 
   int x;
   int *maybe_null = argc & 1 ? &x : 0;
 
-  // Should work (guarded by assume):
+  // There are two features of symex that might exclude null pointers: local
+  // safe pointer analysis (LSPA for the rest of this file) and value-set
+  // filtering (i.e. goto_symext::try_filter_value_sets()).
+
+  // Should be judged safe by LSPA and value-set filtering (guarded by assume):
   int *ptr1 = maybe_null;
   __CPROVER_assume(ptr1 != 0);
   int deref1 = *ptr1;
 
-  // Should work (guarded by else):
+  // Should be judged safe by LSPA and value-set filtering (guarded by else):
   int *ptr2 = maybe_null;
   if(ptr2 == 0)
   {
@@ -20,14 +26,15 @@ int main(int argc, char **argv) {
     int deref2 = *ptr2;
   }
 
-  // Should work (guarded by if):
+  // Should be judged safe by LSPA and value-set filtering (guarded by if):
   int *ptr3 = maybe_null;
   if(ptr3 != 0)
   {
     int deref3 = *ptr3;
   }
 
-  // Shouldn't work yet despite being safe (guarded by backward goto):
+  // Should be judged unsafe by LSPA and safe by value-set filtering
+  // (guarded by backward goto):
   int *ptr4 = maybe_null;
   goto check;
 
@@ -41,34 +48,58 @@ int main(int argc, char **argv) {
 
 end_test4:
 
-  // Shouldn't work yet despite being safe (guarded by confluence):
+  // Should be judged unsafe by LSPA and safe by value-set filtering
+  // (guarded by confluence):
   int *ptr5 = maybe_null;
   if(argc == 5)
     __CPROVER_assume(ptr5 != 0);
   else
     __CPROVER_assume(ptr5 != 0);
   int deref5 = *ptr5;
 
-  // Shouldn't work (unsafe as only guarded on one branch):
+  // Should be judged unsafe by LSPA (due to suspicion write to ptr5 might alter
+  // ptr6) and safe by value-set filtering:
   int *ptr6 = maybe_null;
-  if(argc == 6)
-    __CPROVER_assume(ptr6 != 0);
-  else
-  {
-  }
+  __CPROVER_assume(ptr6 != 0);
+  ptr5 = 0;
   int deref6 = *ptr6;
 
-  // Shouldn't work due to suspicion write to ptr6 might alter ptr7:
+  // Should be judged unsafe by LSPA (due to suspicion noop() call might alter
+  // ptr7) and safe by value-set filtering:
   int *ptr7 = maybe_null;
   __CPROVER_assume(ptr7 != 0);
-  ptr6 = 0;
+  noop();
   int deref7 = *ptr7;
 
-  // Shouldn't work due to suspicion noop() call might alter ptr8:
-  int *ptr8 = maybe_null;
-  __CPROVER_assume(ptr8 != 0);
-  noop();
-  int deref8 = *ptr8;
+  // Should be judged safe by LSPA and unsafe by value-set filtering (it
+  // isn't known what symbol *ptr_ptr8 refers to, so null can't be removed
+  // from a specific value set):
+  int r8_a = 1, r8_b = 2;
+  int *q8_a = argc & 2 ? &r8_a : 0;
+  int *q8_b = argc & 4 ? &r8_b : 0;
+  int **ptr8 = argc & 8 ? &q8_a : &q8_b;
+  __CPROVER_assume(*ptr8 != 0);
+  int deref8 = **ptr8;
+
+  // Should be judged safe by LSPA and unsafe by value-set filtering (it
+  // isn't known what symbol *ptr_ptr9 refers to, so null can't be removed
+  // from a specific value set):
+  int r9_a = 1, r9_b = 2;
+  int *q9_a = argc & 2 ? &r9_a : 0;
+  int *q9_b = argc & 4 ? &r9_b : 0;
+  int **ptr9 = argc & 8 ? &q9_a : &q9_b;
+  if(*ptr9 != 0)
+    int deref9 = **ptr9;
+
+  // Should be judged unsafe by LSPA and value-set filtering
+  // (unsafe as only guarded on one branch):
+  int *ptr10 = maybe_null;
+  if(argc == 10)
+    __CPROVER_assume(ptr10 != 0);
+  else
+  {
+  }
+  int deref10 = *ptr10;
 
   assert(0);
 }

regression/cbmc/symex_should_exclude_null_pointers/test.desc

@@ -3,15 +3,14 @@ main.c
 --show-vcc
 ^EXIT=0$
 ^SIGNAL=0$
-ptr4\$object
-ptr5\$object
-ptr6\$object
-ptr7\$object
-ptr8\$object
+ptr10\$object
 --
-ptr[1-3]\$object
+ptr[1-9]\$object
 ^warning: ignoring
 --
 ptrX\$object appearing in the VCCs indicates symex was unsure whether the pointer had a valid
 target, and uses the $object symbol as a referred object of last resort. ptr1-3 should be judged
-not-null by symex, so their $object symbols do not occur.
+not-null by local safe pointer analysis, so their $object symbols do not occur. ptr4-7 are
+not caught by local safe pointer analysis but they are judged safe by value-set filtering, i.e.
+goto_symext::try_filter_value_sets(). ptr8-9 are judged safe by local safe pointer analysis but
+not value-set filtering. ptr10 is not judged safe by either because it is not safe.

regression/cbmc/symex_should_filter_value_sets/main.c

@@ -0,0 +1,146 @@
+#include <assert.h>
+
+static void noop()
+{
+}
+
+int main(int argc, char **argv)
+{
+  __CPROVER_assume(argc == 5);
+
+  int a = 2;
+  int b = 1;
+  int *ptr_to_a_or_b = argv[0][0] == '0' ? &a : &b;
+
+  // Should work (value-set filtered by assume):
+  int *p1 = ptr_to_a_or_b;
+  __CPROVER_assume(p1 != &a);
+  int c1 = *p1;
+
+  int *p2 = ptr_to_a_or_b;
+  __CPROVER_assume(*p2 != 2);
+  int c2 = *p2;
+
+  // Should work (value-set filtered by else):
+  int c3 = 0;
+  int *p3 = ptr_to_a_or_b;
+  if(p3 == &a)
+  {
+  }
+  else
+  {
+    c3 = *p3;
+  }
+
+  int c4 = 0;
+  int *p4 = ptr_to_a_or_b;
+  if(*p4 == 2)
+  {
+  }
+  else
+  {
+    c4 = *p4;
+  }
+
+  // Should work (value-set filtered by if):
+  int c5 = 0;
+  int *p5 = ptr_to_a_or_b;
+  if(p5 != &a)
+  {
+    c5 = *p5;
+  }
+
+  int c6 = 0;
+  int *p6 = ptr_to_a_or_b;
+  if(*p6 != 2)
+  {
+    c6 = *p6;
+  }
+
+  // Should work (value-set filtered by assume before a backward goto):
+  int *p7 = ptr_to_a_or_b;
+  goto check7;
+
+divide7:
+  int c7 = *p7;
+  goto end_test7;
+
+check7:
+  __CPROVER_assume(p7 != &a);
+  goto divide7;
+
+end_test7:
+
+  int *p8 = ptr_to_a_or_b;
+  goto check8;
+
+divide8:
+  int c8 = *p8;
+  goto end_test8;
+
+check8:
+  __CPROVER_assume(*p8 != 2);
+  goto divide8;
+
+end_test8:
+
+  // Should work (value-set filtered by confluence of if and else):
+  int *p9 = ptr_to_a_or_b;
+  if(argv[1][0] == '0')
+    __CPROVER_assume(p9 != &a);
+  else
+    __CPROVER_assume(p9 != &a);
+  int c9 = *p9;
+
+  int *p10 = ptr_to_a_or_b;
+  if(argv[2][0] == '0')
+    __CPROVER_assume(*p10 != 2);
+  else
+    __CPROVER_assume(*p10 != 2);
+  int c10 = *p10;
+
+  // Should work (value-set filtered by assume, write through an unrelated
+  // pointer has no effect):
+  int c = 0;
+  int *ptr_to_c = &c;
+
+  int *p11 = ptr_to_a_or_b;
+  __CPROVER_assume(p11 != &a);
+  *ptr_to_c = 3;
+  int c11 = *p11;
+
+  int *p12 = ptr_to_a_or_b;
+  __CPROVER_assume(*p12 != 2);
+  *ptr_to_c = 4;
+  int c12 = *p12;
+
+  // Should work (value-set filtered by assume, function call has no effect):
+  int *p13 = ptr_to_a_or_b;
+  __CPROVER_assume(p13 != &a);
+  noop();
+  int c13 = *p13;
+
+  int *p14 = ptr_to_a_or_b;
+  __CPROVER_assume(*p14 != 2);
+  noop();
+  int c14 = *p14;
+
+  // Shouldn't work (unsafe as value-set only filtered by if on one branch):
+  int *p15 = ptr_to_a_or_b;
+  if(argv[3][0] == '0')
+    __CPROVER_assume(p15 != &a);
+  else
+  {
+  }
+  int c15 = *p15;
+
+  int *p16 = ptr_to_a_or_b;
+  if(argv[4][0] == '0')
+    __CPROVER_assume(*p16 != 2);
+  else
+  {
+  }
+  int c16 = *p16;
+
+  assert(0);
+}