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);
 }

src/goto-symex/symex_main.cpp

@@ -34,7 +34,9 @@ class goto_program_dereferencet:protected dereference_callbackt
     options(_options),
     ns(_ns),
     value_sets(_value_sets),
-    dereference(_ns, _new_symbol_table, _options, *this, ID_nil) { }
+    dereference(_ns, _new_symbol_table, _options, *this, ID_nil, false)
+    {
+    }
 
   void dereference_program(
     goto_programt &goto_program,

src/pointer-analysis/goto_program_dereference.h

@@ -104,10 +104,14 @@ exprt value_set_dereferencet::dereference(
 
     #if 0
     std::cout << "V: " << format(value.pointer_guard) << " --> ";
-    std::cout << format(value.value) << '\n';
+    std::cout << format(value.value);
+    if(value.ignore)
+      std::cout << " (ignored)";
+    std::cout << '\n';
     #endif
 
-    values.push_back(value);
+    if(!value.ignore)
+      values.push_back(value);
   }
 
   // can this fail?
@@ -313,7 +317,11 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
 
   if(root_object.id() == ID_null_object)
   {
-    if(options.get_bool_option("pointer-check"))
+    if(exclude_null_derefs)
+    {
+      result.ignore = true;
+    }
+    else if(options.get_bool_option("pointer-check"))
     {
       guardt tmp_guard(guard);
 
@@ -409,9 +417,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     // This is stuff like *((char *)5).
     // This is turned into an access to __CPROVER_memory[...].
 
-    if(language_mode==ID_java)
+    if(language_mode == ID_java)
     {
-      result.value=nil_exprt();
+      result.ignore = true;
       return result;
     }
 

src/pointer-analysis/value_set_dereference.cpp

@@ -35,18 +35,24 @@ class value_set_dereferencet
    * \param _options Options, in particular whether pointer checks are
             to be performed
    * \param _dereference_callback Callback object for error reporting
+   * \param _language_mode Mode for any new symbols created to represent
+            a dereference failure
+   * \param _exclude_null_derefs Ignore value-set entries that indicate a given
+            dereference may follow a null pointer
   */
   value_set_dereferencet(
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
     const optionst &_options,
     dereference_callbackt &_dereference_callback,
-    const irep_idt _language_mode):
+    const irep_idt _language_mode,
+    bool _exclude_null_derefs):
     ns(_ns),
     new_symbol_table(_new_symbol_table),
     options(_options),
     dereference_callback(_dereference_callback),
-    language_mode(_language_mode)
+    language_mode(_language_mode),
+    exclude_null_derefs(_exclude_null_derefs)
   { }
 
   virtual ~value_set_dereferencet() { }
@@ -82,6 +88,9 @@ class value_set_dereferencet
   /// language_mode: ID_java, ID_C or another language identifier
   /// if we know the source language in use, irep_idt() otherwise.
   const irep_idt language_mode;
+  /// Flag indicating whether `value_set_dereferencet::dereference` should
+  /// disregard an apparent attempt to dereference NULL
+  const bool exclude_null_derefs;
   static unsigned invalid_counter;
 
   bool dereference_type_compare(
@@ -92,17 +101,38 @@ class value_set_dereferencet
     exprt &dest,
     const exprt &offset) const;
 
+  /// Return value for `build_reference_to`; see that method for documentation.
   class valuet
   {
   public:
     exprt value;
     exprt pointer_guard;
+    bool ignore;
 
-    valuet():value(nil_exprt()), pointer_guard(false_exprt())
+    valuet():value(nil_exprt()), pointer_guard(false_exprt()), ignore(false)
     {
     }
   };
 
+  /// Get a guard and expression to access `what` under `guard`.
+  /// \param what: value set entry to convert to an expression: either
+  ///   ID_unknown, ID_invalid, or an object_descriptor_exprt giving a referred
+  ///   object and offset.
+  /// \param mode: whether the pointer is being read or written; used to create
+  ///   pointer validity checks if need be
+  /// \param pointer: pointer expression that may point to `what`
+  /// \param guard: guard under which the pointer is dereferenced
+  /// \return
+  ///    * If we were explicitly instructed to ignore `what` as a possible
+  ///        pointer target: a `valuet` with `ignore` = true, and `value` and
+  ///        `pointer_guard` set to nil.
+  ///    * If we could build an expression corresponding to `what`:
+  ///        A `valuet` with non-nil `value`, and `pointer_guard` set to an
+  ///        appropriate check to determine if `pointer_expr` really points to
+  ///        `what` (for example, we might return
+  ///        `{.value = global, .pointer_guard = (pointer_expr == &global)}`
+  ///    * Otherwise, if we couldn't build an expression (e.g. for `what` ==
+  ///        ID_unknown), a `valuet` with nil `value` and `ignore` == false.
   valuet build_reference_to(
     const exprt &what,
     const modet mode,