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

src/pointer-analysis/value_set_dereference.cpp

@@ -44,6 +44,11 @@ const exprt &value_set_dereferencet::get_symbol(const exprt &expr)
   return expr;
 }
 
+bool value_set_dereferencet::null_dereference_is_impossible() const
+{
+  return language_mode == ID_java;
+}
+
 /// \par parameters: expression dest, to be dereferenced under given guard,
 /// and given mode
 /// \return returns pointer after dereferencing
@@ -102,6 +107,13 @@ exprt value_set_dereferencet::dereference(
       it!=points_to_set.end();
       it++)
   {
+    if(it->id() == ID_object_descriptor &&
+       to_object_descriptor_expr(*it).root_object().id() == ID_null_object &&
+       null_dereference_is_impossible())
+    {
+      continue;
+    }
+
     valuet value=build_reference_to(*it, mode, pointer, guard);
 
     #if 0

src/pointer-analysis/value_set_dereference.h

@@ -138,6 +138,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