Add global name map to goto_symex_state

This global name map will be used to check what generation is currently
available for each level1 name, and shared across all states. This will
only be used when a particular state tries to find out what the next
free generation is.

The main draw of this is that all branches will now assign unique
generations that won't clash with assignments done across other
branches. One minor downside is that in VCC's the generation number
might jump sporadically (say from diffblue#4 to diffblue#40).

Author: JohnDumbell

src/goto-instrument/accelerate/scratch_program.cpp

@@ -35,8 +35,9 @@ bool scratch_programt::check_sat(bool do_slice)
   output(ns, "scratch", std::cout);
 #endif
 
+  global_name_mapt global_map;
   symex_state = util_make_unique<goto_symex_statet>(
-    symex_targett::sourcet(goto_functionst::entry_point(), *this));
+    symex_targett::sourcet(goto_functionst::entry_point(), *this), global_map);
   symex.symex_with_state(
     *symex_state,
     [this](const irep_idt &key) -> const goto_functionst::goto_functiont & {

src/goto-symex/goto_symex_state.cpp

@@ -29,8 +29,14 @@ Author: Daniel Kroening, [email protected]
 
 static void get_l1_name(exprt &expr);
 
-goto_symex_statet::goto_symex_statet(const symex_targett::sourcet &_source)
-  : goto_statet(_source), symex_target(nullptr), record_events(true), dirty()
+goto_symex_statet::goto_symex_statet(
+  const symex_targett::sourcet &_source,
+  global_name_mapt &global_map)
+  : goto_statet(_source),
+    symex_target(nullptr),
+    record_events(true),
+    dirty(),
+    global_name_map(global_map)
 {
   threads.resize(1);
   new_frame();
@@ -183,9 +189,7 @@ void goto_symex_statet::assignment(
 #endif
 
   // do the l2 renaming
-  const auto level2_it =
-    level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0)).first;
-  symex_renaming_levelt::increase_counter(level2_it);
+  increase_generation(l1_identifier, lhs);
   set_l2_indices(lhs, ns);
 
   // in case we happen to be multi-threaded, record the memory access
@@ -442,10 +446,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
 
     if(a_s_read.second.empty())
     {
-      auto level2_it =
-        level2.current_names.emplace(l1_identifier, std::make_pair(ssa_l1, 0))
-          .first;
-      symex_renaming_levelt::increase_counter(level2_it);
+      increase_generation(l1_identifier, ssa_l1);
       a_s_read.first=level2.current_count(l1_identifier);
     }
 
@@ -481,10 +482,6 @@ bool goto_symex_statet::l2_thread_read_encoding(
     return true;
   }
 
-  const auto level2_it =
-    level2.current_names.emplace(l1_identifier, std::make_pair(ssa_l1, 0))
-      .first;
-
   // No event and no fresh index, but avoid constant propagation
   if(!record_events)
   {
@@ -494,7 +491,8 @@ bool goto_symex_statet::l2_thread_read_encoding(
   }
 
   // produce a fresh L2 name
-  symex_renaming_levelt::increase_counter(level2_it);
+  increase_generation(l1_identifier, ssa_l1);
+
   set_l2_indices(ssa_l1, ns);
   expr=ssa_l1;
 
@@ -506,6 +504,43 @@ bool goto_symex_statet::l2_thread_read_encoding(
   return true;
 }
 
+/// Allocates a fresh L2 name for the given L1 identifier, and makes it the
+/// latest generation on this path.
+void goto_symex_statet::increase_generation(
+  const irep_idt l1_identifier,
+  const ssa_exprt &lhs)
+{
+  auto current_emplace_res =
+    level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0));
+  auto global_emplace_res =
+    global_name_map.emplace(l1_identifier, std::make_pair(lhs, 0));
+
+  global_emplace_res.first->second.second++;
+  current_emplace_res.first->second.second =
+    global_emplace_res.first->second.second;
+}
+
+/// Allocates a fresh L2 name for the given L1 identifier, and makes it the
+/// latest generation on this path. Does nothing if there isn't an expression
+/// keyed by the l1 identifier.
+void goto_symex_statet::increase_generation_if_exists(const irep_idt identifier)
+{
+  // If we can't find the name in the local scope, don't increase the global
+  // even if it exists there.
+  auto current_names_iter = level2.current_names.find(identifier);
+  if(current_names_iter == level2.current_names.end())
+    return;
+
+  // If we have a global store, increment its generation count, then assign
+  // that new value to our local scope.
+  auto global_names_iter = global_name_map.find(identifier);
+  if(global_names_iter != global_name_map.end())
+  {
+    global_names_iter->second.second++;
+    current_names_iter->second.second = global_names_iter->second.second;
+  }
+}
+
 /// thread encoding
 bool goto_symex_statet::l2_thread_write_encoding(
   const ssa_exprt &expr,

src/goto-symex/goto_symex_state.h

@@ -132,6 +132,8 @@ struct framet
   }
 };
 
+using global_name_mapt = std::map<irep_idt, std::pair<ssa_exprt, unsigned>>;
+
 /// Central data structure: state.
 
 /// The state is a persistent data structure that symex maintains as it
@@ -143,7 +145,9 @@ struct framet
 class goto_symex_statet final : public goto_statet
 {
 public:
-  explicit goto_symex_statet(const symex_targett::sourcet &);
+  goto_symex_statet(
+    const symex_targett::sourcet &,
+    global_name_mapt &global_map);
   ~goto_symex_statet();
 
   /// \brief Fake "copy constructor" that initializes the `symex_target` member
@@ -319,7 +323,17 @@ class goto_symex_statet final : public goto_statet
   /// \brief Should the additional validation checks be run?
   bool run_validation_checks;
 
+  /// Allocates a fresh L2 name for the given L1 identifier, and makes it the
+  //  latest generation on this path.
+  void increase_generation(const irep_idt l1_identifier, const ssa_exprt &lhs);
+
+  /// Increases the generation of the L1 identifier. Does nothing if there
+  /// isn't an expression keyed by it.
+  void increase_generation_if_exists(const irep_idt identifier);
+
 private:
+  global_name_mapt &global_name_map;
+
   /// \brief Dangerous, do not use
   ///
   /// Copying a state S1 to S2 risks S2 pointing to a deallocated

src/goto-symex/path_storage.h

@@ -98,6 +98,10 @@ class path_storaget
   /// error-handling paths.
   std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
 
+  /// Tracks fresh L2 names across an entire symex run. This will be shared
+  /// across all states to allocate unique generations.
+  global_name_mapt level2_names;
+
 private:
   // Derived classes should override these methods, allowing the base class to
   // enforce preconditions.

src/goto-symex/renaming_level.cpp

@@ -58,8 +58,7 @@ void symex_level1t::operator()(ssa_exprt &ssa_expr) const
   ssa_expr.set_level_1(it->second.second);
 }
 
-void symex_level1t::restore_from(
-  const symex_renaming_levelt::current_namest &other)
+void symex_level1t::restore_from(const current_namest &other)
 {
   auto it = current_names.begin();
   for(const auto &pair : other)

src/goto-symex/symex_dead.cpp

@@ -48,7 +48,5 @@ void goto_symext::symex_dead(statet &state)
   state.propagation.erase(l1_identifier);
 
   // L2 renaming
-  auto level2_it = state.level2.current_names.find(l1_identifier);
-  if(level2_it != state.level2.current_names.end())
-    symex_renaming_levelt::increase_counter(level2_it);
+  state.increase_generation_if_exists(l1_identifier);
 }

src/goto-symex/symex_decl.cpp

@@ -63,10 +63,8 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   // L2 renaming
   // inlining may yield multiple declarations of the same identifier
   // within the same L1 context
-  const auto level2_it =
-    state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 0))
-      .first;
-  symex_renaming_levelt::increase_counter(level2_it);
+  state.increase_generation(l1_identifier, ssa);
+
   const bool record_events=state.record_events;
   state.record_events=false;
   exprt expr_l2 = state.rename(std::move(ssa), ns);

src/goto-symex/symex_main.cpp

@@ -294,7 +294,8 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
 
   // create and prepare the state
   auto state = util_make_unique<statet>(
-    symex_targett::sourcet(entry_point_id, start_function->body));
+    symex_targett::sourcet(entry_point_id, start_function->body),
+    path_storage.level2_names);
   CHECK_RETURN(!state->threads.empty());
   CHECK_RETURN(!state->call_stack().empty());