Use local-safe-pointers analysis to improve Symex pointer resolution

This uses local_safe_pointerst to determine when symex dereferences a pointer
that cannot be null. When it does the null result is excluded from the possible
values, and therefore a $invalid_object reference may be excluded from the result
of dereferencing such a pointer. This can improve constant propagation.

Author: smowton

jbmc/regression/jbmc/symex_should_exclude_null_pointers/test.class

@@ -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.desc

@@ -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.java

@@ -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.

jbmc/regression/jbmc/symex_should_exclude_null_pointers/test_vccs.desc

@@ -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/main.c

@@ -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/cbmc/symex_should_exclude_null_pointers/test.desc

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
 
+#include <analyses/local_safe_pointers.h>
+
 #include <util/options.h>
 #include <util/message.h>
 
@@ -465,6 +467,8 @@ class goto_symext
   void rewrite_quantifiers(exprt &, statet &);
 
   path_storaget &path_storage;
+
+  std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H

src/goto-symex/goto_symex.h

@@ -236,6 +236,22 @@ void goto_symext::dereference_rec(
     if(expr.operands().size()!=1)
       throw "dereference takes one operand";
 
+    bool expr_is_not_null = false;
+
+    if(state.threads.size() == 1)
+    {
+      const irep_idt &expr_function = state.source.pc->function;
+      if(!expr_function.empty())
+      {
+        dereference_exprt to_check = to_dereference_expr(expr);
+        state.get_original_name(to_check);
+
+        expr_is_not_null =
+          safe_pointers.at(expr_function).is_safe_dereference(
+            to_check, state.source.pc);
+      }
+    }
+
     exprt tmp1;
     tmp1.swap(expr.op0());
 
@@ -246,7 +262,12 @@ void goto_symext::dereference_rec(
     symex_dereference_statet symex_dereference_state(*this, state);
 
     value_set_dereferencet dereference(
-      ns, state.symbol_table, options, symex_dereference_state, language_mode);
+      ns,
+      state.symbol_table,
+      options,
+      symex_dereference_state,
+      language_mode,
+      expr_is_not_null);
 
     // std::cout << "**** " << format(tmp1) << '\n';
     exprt tmp2=

src/goto-symex/symex_dereference.cpp

@@ -222,6 +222,11 @@ void goto_symext::symex_function_call_code(
 
   state.dirty.populate_dirty_for_function(identifier, goto_function);
 
+  auto emplace_safe_pointers_result =
+    safe_pointers.emplace(identifier, local_safe_pointerst{});
+  if(emplace_safe_pointers_result.second)
+    emplace_safe_pointers_result.first->second(goto_function.body);
+
   const bool stop_recursing=get_unwind_recursion(
     identifier,
     state.source.thread_nr,

src/goto-symex/symex_function_call.cpp

@@ -132,8 +132,15 @@ void goto_symext::initialize_entry_point(
 
   INVARIANT(
     !pc->function.empty(), "all symexed instructions should have a function");
-  state.dirty.populate_dirty_for_function(
-    pc->function, get_goto_function(pc->function));
+
+  const goto_functiont &entry_point_function = get_goto_function(pc->function);
+
+  auto emplace_safe_pointers_result =
+    safe_pointers.emplace(pc->function, local_safe_pointerst{});
+  if(emplace_safe_pointers_result.second)
+    emplace_safe_pointers_result.first->second(entry_point_function.body);
+
+  state.dirty.populate_dirty_for_function(pc->function, entry_point_function);
 
   symex_transition(state, state.source.pc);
 }