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

@@ -37,7 +37,11 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
 
   symex_state = util_make_unique<goto_symex_statet>(
     symex_targett::sourcet(goto_functionst::entry_point(), *this),
-    guard_manager);
+    guard_manager,
+    [this](const irep_idt &id) {
+      return path_storage.get_unique_l2_index(id);
+    });
+
   symex.symex_with_state(
     *symex_state,
     [this](const irep_idt &key) -> const goto_functionst::goto_functiont & {

src/goto-symex/goto_symex_state.cpp

@@ -31,12 +31,14 @@ static void get_l1_name(exprt &expr);
 
 goto_symex_statet::goto_symex_statet(
   const symex_targett::sourcet &_source,
-  guard_managert &manager)
+  guard_managert &manager,
+  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
   : goto_statet(_source, manager),
     guard_manager(manager),
     symex_target(nullptr),
     record_events(true),
-    dirty()
+    dirty(),
+    fresh_l2_name_provider(fresh_l2_name_provider)
 {
   threads.emplace_back(guard_manager);
   call_stack().new_frame(source);
@@ -212,9 +214,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);
   lhs = set_indices<L2>(std::move(lhs), ns).get();
 
   // in case we happen to be multi-threaded, record the memory access
@@ -439,10 +439,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);
     }
     const renamedt<ssa_exprt, L2> l2_false_case = set_indices<L2>(ssa_l1, ns);
@@ -476,10 +473,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)
   {
@@ -488,7 +481,7 @@ 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);
   expr = set_indices<L2>(std::move(ssa_l1), ns).get();
 
   // and record that
@@ -499,6 +492,32 @@ 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));
+
+  current_emplace_res.first->second.second =
+    fresh_l2_name_provider(l1_identifier);
+}
+
+/// 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, this is a no-op.
+  auto current_names_iter = level2.current_names.find(identifier);
+  if(current_names_iter == level2.current_names.end())
+    return;
+
+  current_names_iter->second.second = fresh_l2_name_provider(identifier);
+}
+
 /// thread encoding
 bool goto_symex_statet::l2_thread_write_encoding(
   const ssa_exprt &expr,

src/goto-symex/goto_symex_state.h

@@ -42,7 +42,10 @@ Author: Daniel Kroening, [email protected]
 class goto_symex_statet final : public goto_statet
 {
 public:
-  goto_symex_statet(const symex_targett::sourcet &, guard_managert &manager);
+  goto_symex_statet(
+    const symex_targett::sourcet &,
+    guard_managert &manager,
+    std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
   ~goto_symex_statet();
 
   /// \brief Fake "copy constructor" that initializes the `symex_target` member
@@ -200,7 +203,17 @@ class goto_symex_statet final : public goto_statet
   unsigned total_vccs = 0;
   unsigned remaining_vccs = 0;
 
+  /// 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:
+  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
+
   /// \brief Dangerous, do not use
   ///
   /// Copying a state S1 to S2 risks S2 pointing to a deallocated

src/goto-symex/path_storage.h

@@ -98,15 +98,16 @@ class path_storaget
   /// error-handling paths.
   std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
 
-  /// Provide a unique index for a given \p id, starting from \p minimum_index.
-  std::size_t get_unique_index(const irep_idt &id, std::size_t minimum_index)
+  /// Provide a unique L1 index for a given \p id, starting from
+  /// \p minimum_index.
+  std::size_t get_unique_l1_index(const irep_idt &id, std::size_t minimum_index)
   {
-    auto entry = unique_index_map.emplace(id, minimum_index);
-
-    if(!entry.second)
-      entry.first->second = std::max(entry.first->second + 1, minimum_index);
+    return get_unique_index(l1_indices, id, minimum_index);
+  }
 
-    return entry.first->second;
+  std::size_t get_unique_l2_index(const irep_idt &id)
+  {
+    return get_unique_index(l2_indices, id, 1);
   }
 
 private:
@@ -115,8 +116,24 @@ class path_storaget
   virtual patht &private_peek() = 0;
   virtual void private_pop() = 0;
 
+  typedef std::unordered_map<irep_idt, std::size_t> name_index_mapt;
+
+  std::size_t get_unique_index(
+    name_index_mapt &unique_index_map,
+    const irep_idt &id,
+    std::size_t minimum_index)
+  {
+    auto entry = unique_index_map.emplace(id, minimum_index);
+
+    if(!entry.second)
+      entry.first->second = std::max(entry.first->second + 1, minimum_index);
+
+    return entry.first->second;
+  }
+
   /// Storage used by \ref get_unique_index.
-  std::unordered_map<irep_idt, std::size_t> unique_index_map;
+  name_index_mapt l1_indices;
+  name_index_mapt l2_indices;
 };
 
 /// \brief LIFO save queue: depth-first search, try to finish paths

src/goto-symex/renaming_level.cpp

@@ -73,8 +73,7 @@ operator()(renamedt<ssa_exprt, L1> l1_expr) const
   return renamedt<ssa_exprt, L2>{std::move(l1_expr.value)};
 }
 
-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

@@ -43,9 +43,8 @@ void goto_symext::symex_dead(statet &state)
   // map is safe as 1) it is local to a path and 2) this instance can no longer
   // appear
   state.propagation.erase(l1_identifier);
+
   // increment the L2 index to ensure a merge on join points will propagate the
   // value for branches that are still live
-  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

@@ -43,7 +43,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   ssa_exprt ssa = state.add_object(
     expr,
     [this](const irep_idt &l0_name) {
-      return path_storage.get_unique_index(l0_name, 1);
+      return path_storage.get_unique_l1_index(l0_name, 1);
     },
     ns);
   const irep_idt &l1_identifier = ssa.get_identifier();
@@ -70,6 +70,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 1))
       .second;
   CHECK_RETURN(is_new);
+
   const bool record_events=state.record_events;
   state.record_events=false;
   exprt expr_l2 = state.rename(std::move(ssa), ns);

src/goto-symex/symex_function_call.cpp

@@ -402,7 +402,7 @@ static void locality(
     (void)state.add_object(
       ns.lookup(param).symbol_expr(),
       [&path_storage, &frame_nr](const irep_idt &l0_name) {
-        return path_storage.get_unique_index(l0_name, frame_nr);
+        return path_storage.get_unique_l1_index(l0_name, frame_nr);
       },
       ns);
   }

src/goto-symex/symex_main.cpp

@@ -327,7 +327,11 @@ 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),
-    guard_manager);
+    guard_manager,
+    [this](const irep_idt &id) {
+      return path_storage.get_unique_l2_index(id);
+    });
+
   CHECK_RETURN(!state->threads.empty());
   CHECK_RETURN(!state->call_stack().empty());
 

src/goto-symex/symex_start_thread.cpp

@@ -67,7 +67,7 @@ void goto_symext::symex_start_thread(statet &state)
     // get L0 name for current thread
     lhs.set_level_0(t);
     const irep_idt &l0_name = lhs.get_identifier();
-    std::size_t l1_index = path_storage.get_unique_index(l0_name, 0);
+    std::size_t l1_index = path_storage.get_unique_l1_index(l0_name, 0);
     CHECK_RETURN(l1_index == 0);
 
     // set up L1 name