Move instead of merge symex L2 renaming map when possible

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

@@ -91,8 +91,9 @@ void goto_symext::trigger_auto_object(const exprt &expr, statet &state)
       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.get_level2().current_names.find(ssa_expr.get_identifier()) ==
+          state.get_level2().current_names.end())
         {
           initialize_auto_object(expr, state);
         }

src/goto-symex/goto_state.h

@@ -28,8 +28,15 @@ class goto_statet
   /// Distance from entry
   unsigned depth = 0;
 
+protected:
   symex_level2t level2;
 
+public:
+  const symex_level2t &get_level2() const
+  {
+    return level2;
+  }
+
   /// Uses level 1 names, and is used to do dereferencing
   value_sett value_set;
 
@@ -55,6 +62,12 @@ class goto_statet
   unsigned atomic_section_id = 0;
 
   /// Constructors
+  goto_statet() = default;
+  goto_statet &operator=(const goto_statet &other) = default;
+  goto_statet &operator=(goto_statet &&other) = default;
+  goto_statet(const goto_statet &other) = default;
+  goto_statet(goto_statet &&other) = default;
+
   explicit goto_statet(const class goto_symex_statet &s);
 
   explicit goto_statet(guard_managert &guard_manager)

src/goto-symex/goto_symex_state.cpp

@@ -31,13 +31,15 @@ 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(manager),
     source(_source),
     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);
@@ -213,9 +215,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
@@ -440,10 +440,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);
@@ -477,10 +474,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)
   {
@@ -489,7 +482,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
@@ -500,6 +493,35 @@ 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.
+/// \return the newly allocated generation number
+std::size_t 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);
+
+  return current_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, 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
@@ -202,7 +205,24 @@ 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.
+  std::size_t
+  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);
+
+  /// Drops an L1 name from the local L2 map
+  void drop_l1_name(symex_renaming_levelt::current_namest::const_iterator it)
+  {
+    level2.current_names.erase(it);
+  }
+
 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/renaming_level.h

@@ -32,7 +32,13 @@ enum levelt
 /// during symex to ensure static single assignment (SSA) form.
 struct symex_renaming_levelt
 {
+  symex_renaming_levelt() = default;
   virtual ~symex_renaming_levelt() = default;
+  symex_renaming_levelt &
+  operator=(const symex_renaming_levelt &other) = default;
+  symex_renaming_levelt &operator=(symex_renaming_levelt &&other) = default;
+  symex_renaming_levelt(const symex_renaming_levelt &other) = default;
+  symex_renaming_levelt(symex_renaming_levelt &&other) = default;
 
   /// Map identifier to ssa_exprt and counter
   typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned>> current_namest;
@@ -125,6 +131,10 @@ struct symex_level2t : public symex_renaming_levelt
 
   symex_level2t() = default;
   ~symex_level2t() override = default;
+  symex_level2t &operator=(const symex_level2t &other) = default;
+  symex_level2t &operator=(symex_level2t &&other) = default;
+  symex_level2t(const symex_level2t &other) = default;
+  symex_level2t(symex_level2t &&other) = default;
 };
 
 /// Undo all levels of renaming

src/goto-symex/symex_atomic_section.cpp

@@ -70,7 +70,7 @@ void goto_symext::symex_atomic_end(statet &state)
   for(const auto &pair : state.written_in_atomic_section)
   {
     ssa_exprt w = pair.first;
-    w.set_level_2(state.level2.current_count(w.get_identifier()));
+    w.set_level_2(state.get_level2().current_count(w.get_identifier()));
 
     // guard is the disjunction over writes
     PRECONDITION(!pair.second.empty());

src/goto-symex/symex_dead.cpp

@@ -45,7 +45,5 @@ void goto_symext::symex_dead(statet &state)
   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();
@@ -66,10 +66,9 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   }
 
   // L2 renaming
-  bool is_new =
-    state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 1))
-      .second;
-  CHECK_RETURN(is_new);
+  std::size_t generation = state.increase_generation(l1_identifier, ssa);
+  CHECK_RETURN(generation == 1);
+
   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

@@ -349,8 +349,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.get_level2().current_names.begin();
+        c_it != state.get_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
@@ -364,7 +364,7 @@ static void pop_frame(goto_symext::statet &state)
       }
       auto cur = c_it;
       ++c_it;
-      state.level2.current_names.erase(cur);
+      state.drop_l1_name(cur);
     }
   }
 
@@ -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);
   }