Use type equality, not base_type_eq in local safe pointers

jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp

@@ -74,7 +74,7 @@ SCENARIO(
         // This analysis checks that any usage of a pointer is preceded by an
         // assumption that it is non-null
         // (e.g. assume(x != nullptr); y = x->...)
-        local_safe_pointerst safe_pointers(ns);
+        local_safe_pointerst safe_pointers;
         safe_pointers(main_function.body);
 
         for(auto instrit = main_function.body.instructions.begin(),

src/analyses/local_safe_pointers.cpp

@@ -11,7 +11,6 @@ Author: Diffblue Ltd
 
 #include "local_safe_pointers.h"
 
-#include <util/base_type.h>
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/format_expr.h>
@@ -82,8 +81,7 @@ static optionalt<goto_null_checkt> get_null_checked_expr(const exprt &expr)
 /// \param goto_program: program to analyse
 void local_safe_pointerst::operator()(const goto_programt &goto_program)
 {
-  std::set<exprt, base_type_comparet> checked_expressions(
-    base_type_comparet{ns});
+  std::set<exprt, type_comparet> checked_expressions(type_comparet{});
 
   for(const auto &instruction : goto_program.instructions)
   {
@@ -98,8 +96,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
         checked_expressions = findit->second;
       else
       {
-        checked_expressions =
-          std::set<exprt, base_type_comparet>(base_type_comparet{ns});
+        checked_expressions = std::set<exprt, type_comparet>(type_comparet{});
       }
     }
 
@@ -179,8 +176,11 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
 /// \param out: stream to write output to
 /// \param goto_program: GOTO program analysed (the same one passed to
 ///   operator())
+/// \param ns: namespace
 void local_safe_pointerst::output(
-  std::ostream &out, const goto_programt &goto_program)
+  std::ostream &out,
+  const goto_programt &goto_program,
+  const namespacet &ns)
 {
   forall_goto_program_instructions(i_it, goto_program)
   {
@@ -220,8 +220,11 @@ void local_safe_pointerst::output(
 /// \param out: stream to write output to
 /// \param goto_program: GOTO program analysed (the same one passed to
 ///   operator())
+/// \param ns: namespace
 void local_safe_pointerst::output_safe_dereferences(
-  std::ostream &out, const goto_programt &goto_program)
+  std::ostream &out,
+  const goto_programt &goto_program,
+  const namespacet &ns)
 {
   forall_goto_program_instructions(i_it, goto_program)
   {
@@ -268,17 +271,6 @@ bool local_safe_pointerst::is_non_null_at_program_point(
   auto findit = non_null_expressions.find(program_point->location_number);
   if(findit == non_null_expressions.end())
     return false;
-  const exprt *tocheck = &expr;
-  while(tocheck->id() == ID_typecast)
-    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;
+  return findit->second.count(skip_typecast(expr)) != 0;
 }

src/analyses/local_safe_pointers.h

@@ -23,45 +23,19 @@ Author: Diffblue Ltd
 /// possibly-aliasing operations are handled pessimistically.
 class local_safe_pointerst
 {
-  /// Comparator that regards base_type_eq expressions as equal, and otherwise
+  /// Comparator that regards type-equal 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
+  struct 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)
+    bool operator()(const exprt &e1, const exprt &e2) const
     {
-      INVARIANT(&ns == &other.ns, "base_type_comparet: clashing namespaces");
-      return *this;
+      return e1.type() != e2.type() && e1 < e2;
     }
-
-    bool operator()(const exprt &e1, const exprt &e2) const;
   };
 
-  std::map<unsigned, std::set<exprt, base_type_comparet>> non_null_expressions;
-
-  const namespacet &ns;
+  std::map<unsigned, std::set<exprt, type_comparet>> non_null_expressions;
 
 public:
-  local_safe_pointerst(const namespacet &ns)
-    : ns(ns)
-  {
-  }
-
   void operator()(const goto_programt &goto_program);
 
   bool is_non_null_at_program_point(
@@ -74,10 +48,15 @@ class local_safe_pointerst
     return is_non_null_at_program_point(deref.op(), program_point);
   }
 
-  void output(std::ostream &stream, const goto_programt &program);
+  void output(
+    std::ostream &stream,
+    const goto_programt &program,
+    const namespacet &ns);
 
   void output_safe_dereferences(
-    std::ostream &stream, const goto_programt &program);
+    std::ostream &stream,
+    const goto_programt &program,
+    const namespacet &ns);
 };
 
 #endif // CPROVER_ANALYSES_LOCAL_SAFE_POINTERS_H

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -319,17 +319,17 @@ int goto_instrument_parse_optionst::doit()
 
       forall_goto_functions(it, goto_model.goto_functions)
       {
-        local_safe_pointerst local_safe_pointers(ns);
+        local_safe_pointerst local_safe_pointers;
         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);
+          local_safe_pointers.output(std::cout, it->second.body, ns);
         else
         {
           local_safe_pointers.output_safe_dereferences(
-            std::cout, it->second.body);
+            std::cout, it->second.body, ns);
         }
         std::cout << '\n';
       }

src/goto-symex/goto_symex.h

@@ -17,9 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/abstract_goto_model.h>
 
-#include "goto_symex_state.h"
 #include "path_storage.h"
-#include "symex_target_equation.h"
 
 class byte_extract_exprt;
 class typet;

src/goto-symex/goto_symex_state.h

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
 #include <unordered_set>
 
 #include <analyses/dirty.h>
-#include <analyses/local_safe_pointers.h>
 
 #include <util/invariant.h>
 #include <util/guard.h>
@@ -68,7 +67,6 @@ class goto_statet
   /// Threads
   unsigned atomic_section_id = 0;
 
-  std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
   unsigned total_vccs = 0;
   unsigned remaining_vccs = 0;
 
@@ -320,7 +318,6 @@ inline goto_statet::goto_statet(const class goto_symex_statet &s)
     source(s.source),
     propagation(s.propagation),
     atomic_section_id(s.atomic_section_id),
-    safe_pointers(s.safe_pointers),
     total_vccs(s.total_vccs),
     remaining_vccs(s.remaining_vccs)
 {

src/goto-symex/path_storage.h

@@ -5,16 +5,18 @@
 #ifndef CPROVER_GOTO_SYMEX_PATH_STORAGE_H
 #define CPROVER_GOTO_SYMEX_PATH_STORAGE_H
 
-#include "goto_symex_state.h"
-#include "symex_target_equation.h"
-
-#include <util/options.h>
 #include <util/cmdline.h>
-#include <util/ui_message.h>
 #include <util/invariant.h>
+#include <util/message.h>
+#include <util/options.h>
+
+#include <analyses/local_safe_pointers.h>
 
 #include <memory>
 
+#include "goto_symex_state.h"
+#include "symex_target_equation.h"
+
 /// Functor generating fresh nondet symbols
 class symex_nondet_generatort
 {
@@ -90,6 +92,12 @@ class path_storaget
   /// Counter for nondet objects, which require unique names
   symex_nondet_generatort build_symex_nondet;
 
+  /// Map function identifiers to \ref local_safe_pointerst instances. This is
+  /// to identify derferences that are guaranteed to be safe in a given
+  /// execution context, thus helping to avoid symex to follow spurious
+  /// error-handling paths.
+  std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
+
 private:
   // Derived classes should override these methods, allowing the base class to
   // enforce preconditions.

src/goto-symex/symex_dereference.cpp

@@ -211,9 +211,8 @@ void goto_symext::dereference_rec(exprt &expr, statet &state)
       {
         get_original_name(to_check);
 
-        expr_is_not_null =
-          state.safe_pointers.at(expr_function).is_safe_dereference(
-            to_check, state.source.pc);
+        expr_is_not_null = path_storage.safe_pointers.at(expr_function)
+                             .is_safe_dereference(to_check, state.source.pc);
       }
     }
 

src/goto-symex/symex_function_call.cpp

@@ -240,7 +240,7 @@ void goto_symext::symex_function_call_code(
   state.dirty.populate_dirty_for_function(identifier, goto_function);
 
   auto emplace_safe_pointers_result =
-    state.safe_pointers.emplace(identifier, local_safe_pointerst{ns});
+    path_storage.safe_pointers.emplace(identifier, local_safe_pointerst{});
   if(emplace_safe_pointers_result.second)
     emplace_safe_pointers_result.first->second(goto_function.body);
 

src/goto-symex/symex_main.cpp

@@ -310,7 +310,7 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
 
   // initialize support analyses
   auto emplace_safe_pointers_result =
-    state->safe_pointers.emplace(entry_point_id, local_safe_pointerst{ns});
+    path_storage.safe_pointers.emplace(entry_point_id, local_safe_pointerst{});
   if(emplace_safe_pointers_result.second)
     emplace_safe_pointers_result.first->second(start_function->body);