Centralize generational increases of level2 names

Refactor all local name operations to within the level2 object itself to allow for shadowing global state with the local dictionary.

Author: JohnDumbell

src/goto-symex/goto_symex_state.cpp

@@ -181,9 +181,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);
+  level2.increase_generation(l1_identifier, lhs);
   set_l2_indices(lhs, ns);
 
   // in case we happen to be multi-threaded, record the memory access
@@ -429,10 +427,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);
+      level2.increase_generation(l1_identifier, ssa_l1);
       a_s_read.first=level2.current_count(l1_identifier);
     }
 
@@ -468,10 +463,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)
   {
@@ -481,7 +472,8 @@ bool goto_symex_statet::l2_thread_read_encoding(
   }
 
   // produce a fresh L2 name
-  symex_renaming_levelt::increase_counter(level2_it);
+  level2.increase_generation(l1_identifier, ssa_l1);
+
   set_l2_indices(ssa_l1, ns);
   expr=ssa_l1;
 

src/goto-symex/renaming_level.h

@@ -14,9 +14,11 @@ Author: Romain Brenguier, [email protected]
 
 #include <map>
 #include <unordered_set>
+#include <memory>
 
 #include <util/irep.h>
 #include <util/ssa_expr.h>
+#include <iostream>
 
 /// Wrapper for a \c current_names map, which maps each identifier to an SSA
 /// expression and a counter.
@@ -31,7 +33,7 @@ struct symex_renaming_levelt
   current_namest current_names;
 
   /// Counter corresponding to an identifier
-  unsigned current_count(const irep_idt &identifier) const
+  virtual unsigned current_count(const irep_idt &identifier) const
   {
     const auto it = current_names.find(identifier);
     return it == current_names.end() ? 0 : it->second.second;
@@ -84,6 +86,77 @@ struct symex_level2t : public symex_renaming_levelt
 {
   symex_level2t() = default;
   ~symex_level2t() override = default;
+
+  /// In the case of a state split, we want to keep track of the overall
+  /// name generation across all states for identifier creation.
+  optionalt<current_namest> local_generations;
+
+  void erase(const irep_idt &identifier)
+  {
+    current_names.erase(identifier);
+    if (local_generations)
+      local_generations->erase(identifier);
+  }
+
+  /// If we have a local counter, use that instead of our global.
+  unsigned current_count(const irep_idt &identifier) const override
+  {
+    if(local_generations)
+    {
+      const auto it = local_generations->find(identifier);
+      return it == local_generations->end() ? 0 : it->second.second;
+    }
+    else
+    {
+      return symex_renaming_levelt::current_count(identifier);
+    }
+  }
+
+  /// Ages the generation of an ssa expression by one.
+  void increase_generation(
+    const irep_idt l1_identifier,
+    const ssa_exprt &lhs)
+  {
+    current_names.emplace(l1_identifier, std::make_pair(lhs, 0));
+    increase_generation(l1_identifier);
+  }
+
+  /// Ages the generation of an ssa expression by one. Does nothing
+  /// if there isn't an expression keyed by the l1 identifier.
+  void increase_generation(
+    const irep_idt l1_identifier)
+  {
+    auto current_names_iter = current_names.find(l1_identifier);
+    if (current_names_iter == current_names.end())
+      return;
+
+    current_names_iter->second.second++;
+    if(local_generations)
+    {
+      auto local_iter = local_generations->find(l1_identifier);
+      if (local_iter != local_generations->end()) {}
+        local_iter->second.second = current_names_iter->second.second;
+    }
+  }
+
+  current_namest get_current_names()
+  {
+    return local_generations ? *local_generations : current_names;
+  }
+
+  void print_differences()
+  {
+    if (!local_generations)
+      return;
+
+    for(const auto &dave : *local_generations)
+    {
+      auto local = dave.second.second;
+      auto global = current_names->find(dave.first)->second.second;
+      if (local != global)
+        std::cout << "ID: " << id2string(dave.first) << ", local: " << local << " global: " << global << '\n';
+    }
+  }
 };
 
 /// Undo all levels of renaming

src/goto-symex/symex_dead.cpp

@@ -52,7 +52,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.level2.increase_generation(l1_identifier);
 }

src/goto-symex/symex_decl.cpp

@@ -68,10 +68,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.level2.increase_generation(l1_identifier, ssa);
+
   const bool record_events=state.record_events;
   state.record_events=false;
   state.rename(ssa, ns);

src/goto-symex/symex_function_call.cpp

@@ -361,7 +361,7 @@ static void pop_frame(goto_symext::statet &state)
       }
       auto cur = c_it;
       ++c_it;
-      state.level2.current_names.erase(cur);
+      state.level2.erase(cur->first);
     }
   }