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/auto_objects.cpp

@@ -95,8 +95,8 @@ void goto_symext::trigger_auto_object(
       if(has_prefix(id2string(symbol.base_name), "auto_object"))
       {
         // done already?
-        if(state.level2.current_names.find(ssa_expr.get_identifier())==
-           state.level2.current_names.end())
+        if(state.level2.current_names->find(ssa_expr.get_identifier())==
+           state.level2.current_names->end())
         {
           initialize_auto_object(expr, state);
         }

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.cpp

@@ -50,8 +50,8 @@ void symex_level1t::operator()(ssa_exprt &ssa_expr)
 
   const irep_idt l0_name = ssa_expr.get_l1_object_identifier();
 
-  const auto it = current_names.find(l0_name);
-  if(it == current_names.end())
+  const auto it = current_names->find(l0_name);
+  if(it == current_names->end())
     return;
 
   // rename!
@@ -61,14 +61,14 @@ void symex_level1t::operator()(ssa_exprt &ssa_expr)
 void symex_level1t::restore_from(
   const symex_renaming_levelt::current_namest &other)
 {
-  auto it = current_names.begin();
+  auto it = current_names->begin();
   for(const auto &pair : other)
   {
-    while(it != current_names.end() && it->first < pair.first)
+    while(it != current_names->end() && it->first < pair.first)
       ++it;
-    if(it == current_names.end() || pair.first < it->first)
-      current_names.insert(it, pair);
-    else if(it != current_names.end())
+    if(it == current_names->end() || pair.first < it->first)
+      current_names->insert(it, pair);
+    else if(it != current_names->end())
     {
       PRECONDITION(it->first == pair.first);
       it->second = pair.second;

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.
@@ -28,13 +30,13 @@ struct symex_renaming_levelt
 
   /// Map identifier to ssa_exprt and counter
   typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned>> current_namest;
-  current_namest current_names;
+  current_namest *current_names = new current_namest;
 
   /// 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;
+    const auto it = current_names->find(identifier);
+    return it == current_names->end() ? 0 : it->second.second;
   }
 
   /// Increase the counter corresponding to an identifier
@@ -46,7 +48,7 @@ struct symex_renaming_levelt
   /// Add the \c ssa_exprt of current_names to vars
   void get_variables(std::unordered_set<ssa_exprt, irep_hash> &vars) const
   {
-    for(const auto &pair : current_names)
+    for(const auto &pair : *current_names)
       vars.insert(pair.second.first);
   }
 };
@@ -84,6 +86,80 @@ 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));
+    if (local_generations)
+      local_generations->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(const std::string &differences)
+  {
+    if (!local_generations)
+      return;
+
+    for(const auto &local_gen : *local_generations)
+    {
+      auto local = local_gen.second.second;
+      auto global = current_names->find(local_gen.first)->second.second;
+      if (local != global)
+        std::cout << differences << "ID: " << id2string(local_gen.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

@@ -346,8 +346,8 @@ static void pop_frame(goto_symext::statet &state)
     state.level1.restore_from(frame.old_level1);
 
     // clear function-locals from L2 renaming
-    for(auto c_it = state.level2.current_names.begin();
-        c_it != state.level2.current_names.end();) // no ++c_it
+    for(auto c_it = state.level2.current_names->begin();
+        c_it != state.level2.current_names->end();) // no ++c_it
     {
       const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
       // could use iteration over local_objects as l1_o_id is prefix
@@ -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);
     }
   }
 
@@ -409,17 +409,17 @@ static void locality(
     const irep_idt l0_name=ssa.get_identifier();
 
     // save old L1 name for popping the frame
-    auto c_it = state.level1.current_names.find(l0_name);
+    auto c_it = state.level1.current_names->find(l0_name);
 
-    if(c_it != state.level1.current_names.end())
+    if(c_it != state.level1.current_names->end())
     {
       frame.old_level1.emplace(l0_name, c_it->second);
       c_it->second = std::make_pair(ssa, frame_nr);
     }
     else
     {
       c_it = state.level1.current_names
-               .emplace(l0_name, std::make_pair(ssa, frame_nr))
+        ->emplace(l0_name, std::make_pair(ssa, frame_nr))
                .first;
     }
 

src/goto-symex/symex_start_thread.cpp

@@ -52,8 +52,8 @@ void goto_symext::symex_start_thread(statet &state)
   // create a copy of the local variables for the new thread
   framet &frame = state.top();
 
-  for(auto c_it = state.level2.current_names.begin();
-      c_it != state.level2.current_names.end();
+  for(auto c_it = state.level2.current_names->begin();
+      c_it != state.level2.current_names->end();
       ++c_it)
   {
     const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
@@ -68,7 +68,7 @@ void goto_symext::symex_start_thread(statet &state)
     lhs.set_level_0(t);
 
     // set up L1 name
-    if(!state.level1.current_names.insert(
+    if(!state.level1.current_names->insert(
         std::make_pair(lhs.get_l1_object_identifier(),
                        std::make_pair(lhs, 0))).second)
       UNREACHABLE;