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