Symex: ignore null dereferences when targeting Java

jbmc/regression/jbmc/symex_should_exclude_null_pointers/test.desc

@@ -0,0 +1,14 @@
+CORE
+test.class
+--function test.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+Null pointer check: FAILURE$
+assertion at file test\.java line 21 .*: SUCCESS$
+--
+^warning: ignoring
+--
+JBMC should reports failure, as it might dereference a null pointer, but as Java
+is a safe language we should statically determine that if we reach the assertion
+it cannot be violated.

jbmc/regression/jbmc/symex_should_exclude_null_pointers/test.java

@@ -0,0 +1,25 @@
+public class test {
+
+  public int field;
+
+  public test(int value) {
+
+    field = value;
+
+  }
+
+  public static void main(boolean unknown) {
+
+    test t = new test(12345);
+    test maybe_t = unknown ? null : t;
+
+    // t could still be null, but symex ought to notice that as the Java frontend introduces
+    // checks before all pointer dereference operations, it can statically eliminate
+    // the assertion below.
+
+    int field_value = maybe_t.field;
+    assert field_value == 12345;
+
+  }
+
+}

jbmc/regression/jbmc/symex_should_exclude_null_pointers/test_vccs.desc

@@ -0,0 +1,11 @@
+CORE
+test.class
+--show-vcc --function test.main
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+assertion at file test\.java line 22
+--
+Because symex should statically determine the assertion can't be violated there should not be a goal for it
+by the time --show-vccs prints the equation.

regression/cbmc/symex_should_exclude_null_pointers/main.c

@@ -0,0 +1,74 @@
+static void noop() { }
+
+int main(int argc, char **argv) {
+
+  int x;
+  int *maybe_null = argc & 1 ? &x : 0;
+
+  // Should work (guarded by assume):
+  int *ptr1 = maybe_null;
+  __CPROVER_assume(ptr1 != 0);
+  int deref1 = *ptr1;
+
+  // Should work (guarded by else):
+  int *ptr2 = maybe_null;
+  if(ptr2 == 0)
+  {
+  }
+  else
+  {
+    int deref2 = *ptr2;
+  }
+
+  // Should work (guarded by if):
+  int *ptr3 = maybe_null;
+  if(ptr3 != 0)
+  {
+    int deref3 = *ptr3;
+  }
+
+  // Shouldn't work yet despite being safe (guarded by backward goto):
+  int *ptr4 = maybe_null;
+  goto check;
+
+deref:
+  int deref4 = *ptr4;
+  goto end_test4;
+
+check:
+  __CPROVER_assume(ptr4 != 0);
+  goto deref;
+
+end_test4:
+
+  // Shouldn't work yet despite being safe (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):
+  int *ptr6 = maybe_null;
+  if(argc == 6)
+    __CPROVER_assume(ptr6 != 0);
+  else
+  {
+  }
+  int deref6 = *ptr6;
+
+  // Shouldn't work due to suspicion write to ptr6 might alter ptr7:
+  int *ptr7 = maybe_null;
+  __CPROVER_assume(ptr7 != 0);
+  ptr6 = 0;
+  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;
+
+  assert(0);
+}

regression/cbmc/symex_should_exclude_null_pointers/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--show-vcc
+^EXIT=0$
+^SIGNAL=0$
+ptr4\$object
+ptr5\$object
+ptr6\$object
+ptr7\$object
+ptr8\$object
+--
+ptr[1-3]\$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.

regression/goto-instrument/safe-dereferences/main.c

@@ -0,0 +1,71 @@
+static void noop() { }
+
+int main(int argc, char **argv) {
+
+  int x;
+
+  // Should work (guarded by assume):
+  int *ptr1 = &x;
+  __CPROVER_assume(ptr1 != 0);
+  int deref1 = *ptr1;
+
+  // Should work (guarded by else):
+  int *ptr2 = &x;
+  if(ptr2 == 0)
+  {
+  }
+  else
+  {
+    int deref2 = *ptr2;
+  }
+
+  // Should work (guarded by if):
+  int *ptr3 = &x;
+  if(ptr3 != 0)
+  {
+    int deref3 = *ptr3;
+  }
+
+  // Shouldn't work yet despite being safe (guarded by backward goto):
+  int *ptr4 = &x;
+  goto check;
+
+deref:
+  int deref4 = *ptr4;
+  goto end_test4;
+
+check:
+  __CPROVER_assume(ptr4 != 0);
+  goto deref;
+
+end_test4:
+
+  // Shouldn't work yet despite being safe (guarded by confluence):
+  int *ptr5 = &x;
+  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):
+  int *ptr6 = &x;
+  if(argc == 6)
+    __CPROVER_assume(ptr6 != 0);
+  else
+  {
+  }
+  int deref6 = *ptr6;
+
+  // Shouldn't work due to suspicion *ptr6 might alter ptr7:
+  int *ptr7 = &x;
+  __CPROVER_assume(ptr7 != 0);
+  ptr6 = 0;
+  int deref7 = *ptr7;
+
+  // Shouldn't work due to suspicion noop() call might alter ptr8:
+  int *ptr8 = &x;
+  __CPROVER_assume(ptr8 != 0);
+  noop();
+  int deref8 = *ptr8;
+}

regression/goto-instrument/safe-dereferences/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--show-safe-dereferences
+^EXIT=0$
+^SIGNAL=0$
+Safe \(known-not-null\) dereferences: \{main::[0-9]+::ptr1\}
+Safe \(known-not-null\) dereferences: \{main::[0-9]+::ptr2\}
+Safe \(known-not-null\) dereferences: \{main::[0-9]+::ptr3\}
+--
+Safe \(known-not-null\) dereferences: \{main::[0-9]+::ptr[4-8]\}
+^warning: ignoring
+--
+See comments in main.c for details about what each ptr variable is testing, and why they
+should or shouldn't be seen as safe accesses.

src/analyses/Makefile

@@ -20,6 +20,7 @@ SRC = ai.cpp \
       local_bitvector_analysis.cpp \
       local_cfg.cpp \
       local_may_alias.cpp \
+      local_safe_pointers.cpp \
       locals.cpp \
       natural_loops.cpp \
       reaching_definitions.cpp \