Use type equality, not base_type_eq in local safe pointers

We no longer need to resort to tag/symbol type resolution.

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)
   {
@@ -274,10 +277,10 @@ bool local_safe_pointerst::is_non_null_at_program_point(
   return findit->second.count(*tocheck) != 0;
 }
 
-bool local_safe_pointerst::base_type_comparet::operator()(
-  const exprt &e1, const exprt &e2) const
+bool local_safe_pointerst::type_comparet::
+operator()(const exprt &e1, const exprt &e2) const
 {
-  if(base_type_eq(e1, e2, ns))
+  if(e1.type() == e2.type())
     return false;
   else
     return e1 < e2;

src/analyses/local_safe_pointers.h

@@ -23,45 +23,17 @@ 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
+  class 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;
+  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 +46,15 @@ public:
     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

@@ -320,17 +320,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/symex_function_call.cpp

@@ -229,7 +229,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});
+    state.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});
+    state->safe_pointers.emplace(entry_point_id, local_safe_pointerst{});
   if(emplace_safe_pointers_result.second)
     emplace_safe_pointers_result.first->second(start_function->body);