Update tests for symex excluding null pointers

Value-set filtering means some of the tests pass that didn't before.
Also add tests that only pass because of local safe pointer analysis,
not value-set filtering, so we can tell if that stops working in future.

Author: Owen

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.