Reverse to global_state being optional, local_state being required

Author: JohnDumbell

src/goto-symex/path_storage.h

@@ -90,6 +90,10 @@ class path_storaget
   /// Counter for nondet objects, which require unique names
   symex_nondet_generatort build_symex_nondet;
 
+  /// Storage for overall level two names across an entire symex run. This will
+  /// be shared across all states to allocate unique generations.
+  symex_renaming_levelt::current_namest level2_names;
+
 private:
   // Derived classes should override these methods, allowing the base class to
   // enforce preconditions.

src/goto-symex/renaming_level.h

@@ -14,7 +14,6 @@ Author: Romain Brenguier, [email protected]
 
 #include <map>
 #include <unordered_set>
-#include <memory>
 
 #include <util/irep.h>
 #include <util/ssa_expr.h>
@@ -87,29 +86,12 @@ 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;
+  optionalt<current_namest> global_names;
 
   void erase(const irep_idt &identifier)
   {
+    // We don't want to erase anything from the global scope if it exists.
     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.
@@ -118,8 +100,8 @@ struct symex_level2t : public symex_renaming_levelt
     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));
+    if (global_names)
+      global_names->emplace(l1_identifier, std::make_pair(lhs, 0));
 
     increase_generation(l1_identifier);
   }
@@ -129,35 +111,47 @@ struct symex_level2t : public symex_renaming_levelt
   void increase_generation(
     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 = current_names->find(identifier);
     if (current_names_iter == current_names->end())
       return;
 
-    current_names_iter->second.second++;
-    if(local_generations)
+    // If we have a global store, increment its generation count, then assign
+    // that new value to our local scope.
+    if (global_names)
     {
-      auto local_iter = local_generations->find(identifier);
-      if (local_iter != local_generations->end())
-        local_iter->second.second = current_names_iter->second.second;
+      auto global_names_iter = global_names->find(identifier);
+      if (global_names_iter == global_names->end())
+        global_names_iter->second.second++,
+        current_names_iter->second.second = global_names_iter->second.second;
+    }
+    else
+    {
+      // Otherwise simply increase our local scope.
+      current_names_iter->second.second++;
     }
   }
 
-  current_namest get_current_names()
-  {
-    return local_generations ? *local_generations : *current_names;
-  }
-
+  /// Prints the differences between the global and local naming maps (if they
+  /// exist)
   void print_differences(const std::string &differences)
   {
-    if (!local_generations)
+    if (!global_names)
       return;
 
-    for(const auto &local_gen : *local_generations)
+    std::cout << "Printing differences between local and global generations." << '\n';
+
+    for(const auto &local : *current_names)
     {
-      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';
+      auto global_iter = global_names->find(local.first);
+      if (global_iter == global_names->end())
+        continue;
+
+      auto global_count = global_iter->second.second;
+      auto local_count = local.second.second;
+      if (global_count != local_count)
+        std::cout << differences << "ID: " << id2string(local.first) << ", local: " << local_count << " global: " << global_count << '\n';
     }
   }
 };

src/goto-symex/symex_main.cpp

@@ -315,6 +315,7 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
     emplace_safe_pointers_result.first->second(start_function->body);
 
   state->dirty.populate_dirty_for_function(entry_point_id, *start_function);
+  state->level2.global_names = this->path_storage.level2_names;
 
   // make the first step onto the instruction pointed to by the initial program
   // counter