Strengthen local_safe_pointers to handle common Java operations

The local-safe-pointers analysis can already inform symex that certain pointers
are known not to be null at particular program points. This strengthens the analysis
to spot more cases such that it can determine no null pointer is dereferenced in the
new regression test `jbmc/clean_derefs`, which exercises many common Java operations
including array accesses.

The specific improvements to local-safe-pointers:
 * Look through typecasts. This was already done for GOTO instructions, but now works
   for ASSUME as well.
 * Search for not-null expressions using base_type_eq instead of just irept::operator<.
   This means that when symex uses namespacet::follow to remove a symbol_typet that does
   not prevent local-safe-pointers from noting it is not null in a particular context.

Author: smowton

jbmc/regression/jbmc/clean_derefs/Container.class

@@ -0,0 +1,50 @@
+
+public class Test {
+
+  public int field;
+
+  public Test(int f) { field = f; }
+
+  public static void main(int nondet) {
+
+    // This test creates and uses objects in a few different contexts to check
+    // that in all cases goto-symex realises that the dereferenced object cannot
+    // be null (due to the NullPointerException check that guards all derefs),
+    // therefore symex never generates a reference to any $failed_object symbol
+    // that for a C program would stand in for an unknown or invalid object such
+    // as a dereferenced null pointer.
+
+    Test t1 = new Test(nondet);
+    Test t2 = new Test(nondet);
+
+    Test[] tarray = new Test[5];
+    tarray[0] = null;
+    tarray[1] = t2;
+    tarray[2] = t1;
+
+    t1.field++;
+    (nondet == 10 ? t1 : t2).field--;
+    tarray[nondet % 5].field++;
+    (nondet == 20 ? t1 : tarray[2]).field++;
+
+    Container c1 = new Container(t1);
+    Container c2 = new Container(t2);
+    Container c3 = new Container(null);
+
+    c1.t.field++;
+    (nondet == 30 ? c1 : c3).t.field++;
+    (nondet == 40 ? c2.t : tarray[3]).field--;
+
+    assert false;
+
+  }
+
+}
+
+class Container {
+
+  public Container(Test _t) { t = _t; }
+
+  public Test t;
+
+}

jbmc/regression/jbmc/clean_derefs/Test.class

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--function Test.main --show-vcc
+^EXIT=0$
+^SIGNAL=0$
+--
+invalid
+--
+This checks that no invalid_object references are generated -- these would be created if
+symex thought it might follow a null or other invalid pointer, whereas Java dereferences
+should always be checked not-null beforehand.

jbmc/regression/jbmc/clean_derefs/Test.java

@@ -13,66 +13,61 @@ Author: Diffblue Ltd
 
 #include <util/expr_iterator.h>
 #include <util/format_expr.h>
+#include <util/base_type.h>
 
-/// If `expr` is of the form `x != nullptr`, return x. Otherwise return null
-static const exprt *get_null_checked_expr(const exprt &expr)
-{
-  if(expr.id() == ID_notequal)
-  {
-    const exprt *op0 = &expr.op0(), *op1 = &expr.op1();
-    if(op0->type().id() == ID_pointer &&
-       *op0 == null_pointer_exprt(to_pointer_type(op0->type())))
-    {
-      std::swap(op0, op1);
-    }
-
-    if(op1->type().id() == ID_pointer &&
-       *op1 == null_pointer_exprt(to_pointer_type(op1->type())))
-    {
-      while(op0->id() == ID_typecast)
-        op0 = &op0->op0();
-      return op0;
-    }
-  }
-
-  return nullptr;
-}
-
-/// Return structure for `get_conditional_checked_expr`
+/// Return structure for `get_null_checked_expr` and
+/// `get_conditional_checked_expr`
 struct goto_null_checkt
 {
-  /// If true, the given GOTO tests that a pointer expression is non-null on the
-  /// taken branch; otherwise, on the not-taken branch.
+  /// If true, the given GOTO/ASSUME tests that a pointer expression is non-null
+  /// on the taken branch or passing case; otherwise, on the not-taken branch
+  /// or on failure.
   bool checked_when_taken;
 
   /// Null-tested pointer expression
   exprt checked_expr;
 };
 
-/// Check if a GOTO guard expression tests if a pointer is null
-/// \param goto_guard: expression to check
+/// Check if `expr` tests if a pointer is null
+/// \param expr: expression to check
 /// \return a `goto_null_checkt` indicating what expression is tested and
 ///   whether the check applies on the taken or not-taken branch, or an empty
 ///   optionalt if this isn't a null check.
-static optionalt<goto_null_checkt>
-get_conditional_checked_expr(const exprt &goto_guard)
+static optionalt<goto_null_checkt> get_null_checked_expr(const exprt &expr)
 {
-  exprt normalized_guard = goto_guard;
+  exprt normalized_expr = expr;
   bool checked_when_taken = true;
-  while(normalized_guard.id() == ID_not || normalized_guard.id() == ID_equal)
+  while(normalized_expr.id() == ID_not || normalized_expr.id() == ID_equal)
   {
-    if(normalized_guard.id() == ID_not)
-      normalized_guard = normalized_guard.op0();
+    if(normalized_expr.id() == ID_not)
+      normalized_expr = normalized_expr.op0();
     else
-      normalized_guard.id(ID_notequal);
+      normalized_expr.id(ID_notequal);
     checked_when_taken = !checked_when_taken;
   }
 
-  const exprt *checked_expr = get_null_checked_expr(normalized_guard);
-  if(!checked_expr)
-    return {};
-  else
-    return goto_null_checkt { checked_when_taken, *checked_expr };
+  if(normalized_expr.id() == ID_notequal)
+  {
+    const exprt *op0 = &normalized_expr.op0(), *op1 = &normalized_expr.op1();
+    while(op0->id() == ID_typecast)
+      op0 = &op0->op0();
+    while(op1->id() == ID_typecast)
+      op1 = &op1->op0();
+
+    if(op0->type().id() == ID_pointer &&
+       *op0 == null_pointer_exprt(to_pointer_type(op0->type())))
+    {
+      std::swap(op0, op1);
+    }
+
+    if(op1->type().id() == ID_pointer &&
+       *op1 == null_pointer_exprt(to_pointer_type(op1->type())))
+    {
+      return { { checked_when_taken, *op0 } };
+    }
+  }
+
+  return {};
 }
 
 /// Compute safe dereference expressions for a given GOTO program. This
@@ -82,7 +77,8 @@ get_conditional_checked_expr(const exprt &goto_guard)
 /// \param goto_program: program to analyse
 void local_safe_pointerst::operator()(const goto_programt &goto_program)
 {
-  std::set<exprt> checked_expressions;
+  std::set<exprt, base_type_comparet> checked_expressions(
+    base_type_comparet{ns});
 
   for(const auto &instruction : goto_program.instructions)
   {
@@ -91,11 +87,23 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
       checked_expressions.clear();
     // Retrieve working set for forward GOTOs:
     else if(instruction.is_target())
-      checked_expressions = non_null_expressions[instruction.location_number];
+    {
+      auto findit = non_null_expressions.find(instruction.location_number);
+      if(findit != non_null_expressions.end())
+        checked_expressions = findit->second;
+      else
+      {
+        checked_expressions =
+          std::set<exprt, base_type_comparet>(base_type_comparet{ns});
+      }
+    }
 
     // Save the working set at this program point:
     if(!checked_expressions.empty())
-      non_null_expressions[instruction.location_number] = checked_expressions;
+    {
+      non_null_expressions.emplace(
+        instruction.location_number, checked_expressions);
+    }
 
     switch(instruction.type)
     {
@@ -114,26 +122,35 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
     // Possible checks:
     case ASSUME:
       {
-        const exprt *checked_expr;
-        if((checked_expr = get_null_checked_expr(instruction.guard)) != nullptr)
+        if(auto assume_check = get_null_checked_expr(instruction.guard))
         {
-          checked_expressions.insert(*checked_expr);
+          if(assume_check->checked_when_taken)
+            checked_expressions.insert(assume_check->checked_expr);
         }
         break;
       }
 
     case GOTO:
       if(!instruction.is_backwards_goto())
       {
-        if(auto conditional_check =
-           get_conditional_checked_expr(instruction.guard))
-        {
-          auto &taken_checked_expressions =
-            non_null_expressions[instruction.get_target()->location_number];
-          taken_checked_expressions = checked_expressions;
+        // Copy current state to GOTO target:
+
+        auto target_emplace_result =
+          non_null_expressions.emplace(
+            instruction.get_target()->location_number, checked_expressions);
+        INVARIANT(
+          target_emplace_result.second,
+          "this is a forward analysis; target should not be visited yet");
 
+        if(auto conditional_check = get_null_checked_expr(instruction.guard))
+        {
+          // Add the GOTO condition to either the target or current state,
+          // as appropriate:
           if(conditional_check->checked_when_taken)
-            taken_checked_expressions.insert(conditional_check->checked_expr);
+          {
+            target_emplace_result.first->second.insert(
+              conditional_check->checked_expr);
+          }
           else
             checked_expressions.insert(conditional_check->checked_expr);
 
@@ -157,7 +174,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
 ///   operator())
 /// \param ns: global namespace
 void local_safe_pointerst::output(
-  std::ostream &out, const goto_programt &goto_program, const namespacet &ns)
+  std::ostream &out, const goto_programt &goto_program)
 {
   forall_goto_program_instructions(i_it, goto_program)
   {
@@ -199,7 +216,7 @@ void local_safe_pointerst::output(
 ///   operator())
 /// \param ns: global namespace
 void local_safe_pointerst::output_safe_dereferences(
-  std::ostream &out, const goto_programt &goto_program, const namespacet &ns)
+  std::ostream &out, const goto_programt &goto_program)
 {
   forall_goto_program_instructions(i_it, goto_program)
   {
@@ -251,3 +268,12 @@ bool local_safe_pointerst::is_non_null_at_program_point(
     tocheck = &tocheck->op0();
   return findit->second.count(*tocheck) != 0;
 }
+
+bool local_safe_pointerst::base_type_comparet::operator()(
+  const exprt &e1, const exprt &e2) const
+{
+  if(base_type_eq(e1, e2, ns))
+    return false;
+  else
+    return e1 < e2;
+}

jbmc/regression/jbmc/clean_derefs/test.desc

@@ -23,9 +23,45 @@ Author: Diffblue Ltd
 /// possibly-aliasing operations are handled pessimistically.
 class local_safe_pointerst
 {
-  std::map<unsigned, std::set<exprt>> non_null_expressions;
+  /// Comparator that regards base_type_eq expressions as equal, and otherwise
+  /// uses the natural (operator<) ordering on irept.
+  /// An expression is base_type_eq another one if their types, and types of
+  /// their subexpressions, are identical except that one may use a symbol_typet
+  /// while the other uses that type's expanded (namespacet::follow'd) form.
+  class base_type_comparet
+  {
+    const namespacet &ns;
+
+  public:
+    explicit base_type_comparet(const namespacet &ns)
+      : ns(ns)
+    {
+    }
+
+    base_type_comparet(const base_type_comparet &other)
+      : ns(other.ns)
+    {
+    }
+
+    base_type_comparet &operator=(const base_type_comparet &other)
+    {
+      INVARIANT(&ns == &other.ns, "base_type_comparet: clashing namespaces");
+      return *this;
+    }
+
+    bool operator()(const exprt &e1, const exprt &e2) const;
+  };
+
+  std::map<unsigned, std::set<exprt, base_type_comparet>> non_null_expressions;
+
+  const namespacet &ns;
+
+public:
+  local_safe_pointerst(const namespacet &ns)
+    : ns(ns)
+  {
+  }
 
- public:
   void operator()(const goto_programt &goto_program);
 
   bool is_non_null_at_program_point(
@@ -38,11 +74,10 @@ class local_safe_pointerst
     return is_non_null_at_program_point(deref.op0(), program_point);
   }
 
-  void output(
-    std::ostream &stream, const goto_programt &program, const namespacet &ns);
+  void output(std::ostream &stream, const goto_programt &program);
 
   void output_safe_dereferences(
-    std::ostream &stream, const goto_programt &program, const namespacet &ns);
+    std::ostream &stream, const goto_programt &program);
 };
 
 #endif // CPROVER_ANALYSES_LOCAL_SAFE_POINTERS_H

src/analyses/local_safe_pointers.cpp

@@ -297,17 +297,17 @@ int goto_instrument_parse_optionst::doit()
 
       forall_goto_functions(it, goto_model.goto_functions)
       {
-        local_safe_pointerst local_safe_pointers;
+        local_safe_pointerst local_safe_pointers(ns);
         local_safe_pointers(it->second.body);
         std::cout << ">>>>\n";
         std::cout << ">>>> " << it->first << '\n';
         std::cout << ">>>>\n";
         if(cmdline.isset("show-local-safe-pointers"))
-          local_safe_pointers.output(std::cout, it->second.body, ns);
+          local_safe_pointers.output(std::cout, it->second.body);
         else
         {
           local_safe_pointers.output_safe_dereferences(
-            std::cout, it->second.body, ns);
+            std::cout, it->second.body);
         }
         std::cout << '\n';
       }

src/analyses/local_safe_pointers.h

@@ -223,7 +223,7 @@ 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{});
+    safe_pointers.emplace(identifier, local_safe_pointerst{ns});
   if(emplace_safe_pointers_result.second)
     emplace_safe_pointers_result.first->second(goto_function.body);
 

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -136,7 +136,7 @@ void goto_symext::initialize_entry_point(
   const goto_functiont &entry_point_function = get_goto_function(pc->function);
 
   auto emplace_safe_pointers_result =
-    safe_pointers.emplace(pc->function, local_safe_pointerst{});
+    safe_pointers.emplace(pc->function, local_safe_pointerst{ns});
   if(emplace_safe_pointers_result.second)
     emplace_safe_pointers_result.first->second(entry_point_function.body);