goto-symex: move safe_pointers to path storage

As local_safe_pointerst no longer needs a namespace we can do a partial revert
of 959c7a5 (Bugfix: Maintain safe_pointers per-path). On SV-COMP's
ReachSafety-ECA, copying safe_pointers accounted for 14% of the time spent in
goto_symext::symex_goto (715 of 5119 seconds).

Author: tautschnig

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{});
+    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{});
+    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);