Symex: ignore null dereferences when targeting Java

In Java (and other safe languages) we know that any path that led to dereferencing
a null pointer would have thrown or asserted beforehand (i.e. all pointer dereferences
are checked). Therefore when dereferencing a pointer with value-set {NULL, someobj}
there is no need to generate (for example)
`ptr == &someobj ? someobj.somefield : invalid_object.somefield`, but rather we can simply
produce `someobj.somefield`.

In principle this could also be extended to C programs that have `--pointer-check` enabled,
to other safe languages, and to specific pointer accesses that are analysed never-null at a
particular program point.

Author: smowton

regression/cbmc-java/symex_should_exclude_null_pointers/test.class

@@ -0,0 +1,13 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+Throw null: FAILURE$
+assertion at file test\.java line 21 .*: SUCCESS$
+--
+^warning: ignoring
+--
+The test should fail, 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.

regression/cbmc-java/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 know that as this is Java source,
+    // we must have a null check prior to dereferencing, so it can statically eliminate
+    // the assertion below.
+
+    int field_value = maybe_t.field;
+    assert field_value == 12345;
+
+  }
+
+}

regression/cbmc-java/symex_should_exclude_null_pointers/test.java

@@ -0,0 +1,11 @@
+CORE
+test.class
+--show-vcc
+^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-java/symex_should_exclude_null_pointers/test_vccs.desc

@@ -116,6 +116,16 @@ class bmct:public safety_checkert
     symex.add_recursion_unwind_handler(handler);
   }
 
+  void set_program_cannot_dereference_null(bool value)
+  {
+    symex.set_program_cannot_dereference_null(value);
+  }
+
+  void set_program_cannot_dereference_int_as_pointer(bool value)
+  {
+    symex.set_program_cannot_dereference_int_as_pointer(value);
+  }
+
   static int do_language_agnostic_bmc(
     const path_strategy_choosert &path_strategy_chooser,
     const optionst &opts,

src/cbmc/bmc.h

@@ -62,6 +62,8 @@ class goto_symext
       ns(outer_symbol_table),
       target(_target),
       atomic_section_counter(0),
+      program_cannot_dereference_null(false),
+      program_cannot_dereference_int_as_pointer(false),
       log(mh),
       guard_identifier("goto_symex::\\guard"),
       path_storage(path_storage)
@@ -169,6 +171,16 @@ class goto_symext
   /// successor state to continue executing, and resume symex from that state.
   bool should_pause_symex;
 
+  void set_program_cannot_dereference_null(bool value)
+  {
+    program_cannot_dereference_null = value;
+  }
+
+  void set_program_cannot_dereference_int_as_pointer(bool value)
+  {
+    program_cannot_dereference_int_as_pointer = value;
+  }
+
 protected:
   /// Initialise the symbolic execution and the given state with <code>pc</code>
   /// as entry point.
@@ -228,6 +240,12 @@ class goto_symext
   symex_target_equationt &target;
   unsigned atomic_section_counter;
 
+  /// Indicates if the source program always guards against certain kinds of
+  /// pointer abuse that would normally make symex conservatively assume it
+  /// cannot resolve a dereference to a constant, for example:
+  bool program_cannot_dereference_null;
+  bool program_cannot_dereference_int_as_pointer;
+
   mutable messaget log;
 
   friend class symex_dereference_statet;

src/goto-symex/goto_symex.h

@@ -246,7 +246,13 @@ 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,
+      program_cannot_dereference_null,
+      program_cannot_dereference_int_as_pointer);
 
     // std::cout << "**** " << format(tmp1) << '\n';
     exprt tmp2=

src/goto-symex/symex_dereference.cpp

@@ -95,6 +95,13 @@ void jbmc_parse_optionst::eval_verbosity()
   ui_message_handler.set_verbosity(v);
 }
 
+/// Set symex flags that always hold for Java programs:
+static void jbmc_configure_bmc(bmct &bmc, const symbol_tablet &symbol_table)
+{
+  bmc.set_program_cannot_dereference_null(true);
+  bmc.set_program_cannot_dereference_int_as_pointer(true);
+}
+
 void jbmc_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -502,10 +509,13 @@ int jbmc_parse_optionst::doit()
     return 0;
   }
 
-  std::function<void(bmct &, const symbol_tablet &)> configure_bmc = nullptr;
+  std::function<void(bmct &, const symbol_tablet &)> configure_bmc =
+    jbmc_configure_bmc;
   if(options.get_bool_option("java-unwind-enum-static"))
   {
     configure_bmc = [](bmct &bmc, const symbol_tablet &symbol_table) {
+      jbmc_configure_bmc(bmc, symbol_table);
+
       bmc.add_loop_unwind_handler(
         [&symbol_table](
           const irep_idt &function_id,

src/jbmc/jbmc_parse_options.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, false)
+    {
+    }
 
   void dereference_program(
     goto_programt &goto_program,

src/pointer-analysis/goto_program_dereference.h

@@ -106,10 +106,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?
@@ -288,7 +292,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);
 
@@ -384,9 +392,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(exclude_int_as_pointer_derefs)
     {
-      result.value=nil_exprt();
+      result.ignore = true;
       return result;
     }
 

src/pointer-analysis/value_set_dereference.cpp

@@ -35,18 +35,29 @@ 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
+   * \param _exclude_int_as_pointer_derefs Ignore value-set entries that
+            indicate a given dereference may follow an integer cast to a pointer
+            (e.g. `(char*)5`)
   */
   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,
+    bool _exclude_int_as_pointer_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),
+    exclude_int_as_pointer_derefs(_exclude_int_as_pointer_derefs)
   { }
 
   virtual ~value_set_dereferencet() { }
@@ -82,6 +93,13 @@ 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;
+  /// Flag indicating whether `value_set_dereferencet::dereference` should
+  /// disregard an apparent attempt to dereference an integer cast to a pointer
+  /// (e.g. `(char*)5`)
+  const bool exclude_int_as_pointer_derefs;
   static unsigned invalid_counter;
 
   bool dereference_type_compare(
@@ -92,17 +110,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,
@@ -138,6 +177,10 @@ class value_set_dereferencet
     const typet &type,
     const guardt &guard,
     const exprt &offset);
+
+  /// Returns true if due to language guarantees or some pre-processing pass
+  /// we always know pointers being dereferenced cannot be null.
+  bool null_dereference_is_impossible() const;
 };
 
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H