Use the sharing map for the renaming level maps

Author: danpoe

src/goto-symex/auto_objects.cpp

@@ -91,9 +91,7 @@ void goto_symext::trigger_auto_object(const exprt &expr, statet &state)
       if(has_prefix(id2string(symbol.base_name), "auto_object"))
       {
         // done already?
-        if(
-          state.get_level2().current_names.find(ssa_expr.get_identifier()) ==
-          state.get_level2().current_names.end())
+        if(!state.get_level2().current_names.has_key(ssa_expr.get_identifier()))
         {
           initialize_auto_object(expr, state);
         }

src/goto-symex/goto_state.cpp

@@ -28,13 +28,22 @@ std::size_t goto_statet::increase_generation(
   const ssa_exprt &lhs,
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
 {
-  auto current_emplace_res =
-    level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0));
+  std::size_t n = fresh_l2_name_provider(l1_identifier);
 
-  current_emplace_res.first->second.second =
-    fresh_l2_name_provider(l1_identifier);
+  const auto r_opt = level2.current_names.find(l1_identifier);
 
-  return current_emplace_res.first->second.second;
+  if(!r_opt)
+  {
+    level2.current_names.insert(l1_identifier, std::make_pair(lhs, n));
+  }
+  else
+  {
+    std::pair<ssa_exprt, unsigned> copy = r_opt->get();
+    copy.second = n;
+    level2.current_names.replace(l1_identifier, copy);
+  }
+
+  return n;
 }
 
 /// Given a condition that must hold on this path, propagate as much knowledge

src/goto-symex/goto_symex_state.cpp

@@ -776,16 +776,20 @@ ssa_exprt goto_symex_statet::add_object(
   const irep_idt l0_name = ssa.get_identifier();
   const std::size_t l1_index = index_generator(l0_name);
 
-  // save old L1 name, if any
-  auto existing_or_new_entry = level1.current_names.emplace(
-    std::piecewise_construct,
-    std::forward_as_tuple(l0_name),
-    std::forward_as_tuple(ssa, l1_index));
+  const auto r_opt = level1.current_names.find(l0_name);
 
-  if(!existing_or_new_entry.second)
+  if(!r_opt)
   {
-    frame.old_level1.emplace(l0_name, existing_or_new_entry.first->second);
-    existing_or_new_entry.first->second = std::make_pair(ssa, l1_index);
+    level1.current_names.insert(l0_name, std::make_pair(ssa, l1_index));
+  }
+  else
+  {
+    if(!frame.old_level1.has_key(l0_name))
+    {
+      frame.old_level1.insert(l0_name, r_opt->get());
+    }
+
+    level1.current_names.replace(l0_name, std::make_pair(ssa, l1_index));
   }
 
   ssa = rename_ssa<L1>(std::move(ssa), ns).get();

src/goto-symex/goto_symex_state.h

@@ -223,15 +223,16 @@ class goto_symex_statet final : public goto_statet
   }
 
   /// Drops an L1 name from the local L2 map
-  void drop_l1_name(symex_renaming_levelt::current_namest::const_iterator it)
+  void drop_existing_l1_name(const irep_idt &l1_identifier)
   {
-    level2.current_names.erase(it);
+    level2.current_names.erase(l1_identifier);
   }
 
   /// Drops an L1 name from the local L2 map
   void drop_l1_name(const irep_idt &l1_identifier)
   {
-    level2.current_names.erase(l1_identifier);
+    if(level2.current_names.has_key(l1_identifier))
+      level2.current_names.erase(l1_identifier);
   }
 
   std::function<std::size_t(const irep_idt &)> get_l2_name_provider() const

src/goto-symex/renaming_level.cpp

@@ -55,12 +55,15 @@ operator()(renamedt<ssa_exprt, L0> l0_expr) const
 
   const irep_idt l0_name = l0_expr.get().get_l1_object_identifier();
 
-  const auto it = current_names.find(l0_name);
-  if(it == current_names.end())
+  const auto r_opt = current_names.find(l0_name);
+
+  if(!r_opt)
+  {
     return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
+  }
 
   // rename!
-  l0_expr.value().set_level_1(it->second.second);
+  l0_expr.value().set_level_1(r_opt->get().second);
   return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
 }
 
@@ -75,18 +78,18 @@ operator()(renamedt<ssa_exprt, L1> l1_expr) const
 
 void symex_level1t::restore_from(const current_namest &other)
 {
-  auto it = current_names.begin();
-  for(const auto &pair : other)
+  current_namest::delta_viewt delta_view;
+  other.get_delta_view(current_names, delta_view, false);
+
+  for(const auto &delta_item : delta_view)
   {
-    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(!delta_item.in_both)
+    {
+      current_names.insert(delta_item.k, delta_item.m);
+    }
+    else
     {
-      PRECONDITION(it->first == pair.first);
-      it->second = pair.second;
-      ++it;
+      current_names.replace(delta_item.k, delta_item.m);
     }
   }
 }

src/goto-symex/renaming_level.h

@@ -16,6 +16,7 @@ Author: Romain Brenguier, [email protected]
 #include <unordered_set>
 
 #include <util/irep.h>
+#include <util/sharing_map.h>
 #include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 
@@ -42,27 +43,26 @@ struct symex_renaming_levelt
   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;
+  typedef sharing_mapt<irep_idt, std::pair<ssa_exprt, unsigned>> current_namest;
   current_namest current_names;
 
   /// Counter corresponding to an identifier
   unsigned current_count(const irep_idt &identifier) const
   {
-    const auto it = current_names.find(identifier);
-    return it == current_names.end() ? 0 : it->second.second;
-  }
-
-  /// Increase the counter corresponding to an identifier
-  static void increase_counter(const current_namest::iterator &it)
-  {
-    ++it->second.second;
+    const auto r_opt = current_names.find(identifier);
+    return !r_opt ? 0 : r_opt->get().second;
   }
 
   /// 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)
+    current_namest::viewt view;
+    current_names.get_view(view);
+
+    for(const auto &pair : view)
+    {
       vars.insert(pair.second.first);
+    }
   }
 };
 

src/goto-symex/symex_function_call.cpp

@@ -351,23 +351,30 @@ pop_frame(goto_symext::statet &state, const path_storaget &path_storage)
     // restore L1 renaming
     state.level1.restore_from(frame.old_level1);
 
-    // clear function-locals from L2 renaming
-    for(auto c_it = state.get_level2().current_names.begin();
-        c_it != state.get_level2().current_names.end();) // no ++c_it
+    symex_renaming_levelt::current_namest::viewt view;
+    state.get_level2().current_names.get_view(view);
+
+    std::vector<irep_idt> keys_to_erase;
+
+    for(const auto &pair : view)
     {
-      const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
+      const irep_idt l1_o_id = pair.second.first.get_l1_object_identifier();
+
       // could use iteration over local_objects as l1_o_id is prefix
       if(
         frame.local_objects.find(l1_o_id) == frame.local_objects.end() ||
         (state.threads.size() > 1 &&
-         path_storage.dirty(c_it->second.first.get_object_name())))
+         path_storage.dirty(pair.second.first.get_object_name())))
       {
-        ++c_it;
         continue;
       }
-      auto cur = c_it;
-      ++c_it;
-      state.drop_l1_name(cur);
+
+      keys_to_erase.push_back(pair.first);
+    }
+
+    for(const irep_idt &key : keys_to_erase)
+    {
+      state.drop_existing_l1_name(key);
     }
   }
 

src/goto-symex/symex_goto.cpp

@@ -414,39 +414,6 @@ void goto_symext::merge_goto(
   }
 }
 
-/// Applies f to `(k, ssa, i, j)` if the first map maps k to (ssa, i) and
-/// the second to (ssa', j). If the first map has an entry for k but not the
-/// second one then j is 0, and when the first map has no entry for k then i = 0
-static void for_each2(
-  const std::map<irep_idt, std::pair<ssa_exprt, unsigned>> &first_map,
-  const std::map<irep_idt, std::pair<ssa_exprt, unsigned>> &second_map,
-  const std::function<void(const ssa_exprt &, unsigned, unsigned)> &f)
-{
-  auto second_it = second_map.begin();
-  for(const auto &first_pair : first_map)
-  {
-    while(second_it != second_map.end() && second_it->first < first_pair.first)
-    {
-      f(second_it->second.first, 0, second_it->second.second);
-      ++second_it;
-    }
-    const ssa_exprt &ssa = first_pair.second.first;
-    const unsigned count = first_pair.second.second;
-    if(second_it != second_map.end() && second_it->first == first_pair.first)
-    {
-      f(ssa, count, second_it->second.second);
-      ++second_it;
-    }
-    else
-      f(ssa, count, 0);
-  }
-  while(second_it != second_map.end())
-  {
-    f(second_it->second.first, 0, second_it->second.second);
-    ++second_it;
-  }
-}
-
 /// Helper function for \c phi_function which merges the names of an identifier
 /// for two different states.
 /// \param goto_state: first state
@@ -592,23 +559,56 @@ void goto_symext::phi_function(
   // this gets the diff between the guards
   diff_guard -= dest_state.guard;
 
-  for_each2(
-    goto_state.get_level2().current_names,
-    dest_state.get_level2().current_names,
-    [&](const ssa_exprt &ssa, unsigned goto_count, unsigned dest_count) {
-      merge_names(
-        goto_state,
-        dest_state,
-        ns,
-        diff_guard,
-        log,
-        symex_config.simplify_opt,
-        target,
-        path_storage.dirty,
-        ssa,
-        goto_count,
-        dest_count);
-    });
+  symex_renaming_levelt::current_namest::delta_viewt delta_view;
+  goto_state.get_level2().current_names.get_delta_view(
+    dest_state.get_level2().current_names, delta_view, false);
+
+  for(const auto &delta_item : delta_view)
+  {
+    const ssa_exprt &ssa = delta_item.m.first;
+    unsigned goto_count = delta_item.m.second;
+    unsigned dest_count = !delta_item.in_both ? 0 : delta_item.other_m.second;
+
+    merge_names(
+      goto_state,
+      dest_state,
+      ns,
+      diff_guard,
+      log,
+      symex_config.simplify_opt,
+      target,
+      path_storage.dirty,
+      ssa,
+      goto_count,
+      dest_count);
+  }
+
+  delta_view.clear();
+  dest_state.get_level2().current_names.get_delta_view(
+    goto_state.get_level2().current_names, delta_view, false);
+
+  for(const auto &delta_item : delta_view)
+  {
+    if(delta_item.in_both)
+      continue;
+
+    const ssa_exprt &ssa = delta_item.m.first;
+    unsigned goto_count = 0;
+    unsigned dest_count = delta_item.m.second;
+
+    merge_names(
+      goto_state,
+      dest_state,
+      ns,
+      diff_guard,
+      log,
+      symex_config.simplify_opt,
+      target,
+      path_storage.dirty,
+      ssa,
+      goto_count,
+      dest_count);
+  }
 }
 
 void goto_symext::loop_bound_exceeded(

src/goto-symex/symex_start_thread.cpp

@@ -52,17 +52,19 @@ void goto_symext::symex_start_thread(statet &state)
   // create a copy of the local variables for the new thread
   framet &frame = state.call_stack().top();
 
-  for(auto c_it = state.get_level2().current_names.begin();
-      c_it != state.get_level2().current_names.end();
-      ++c_it)
+  symex_renaming_levelt::current_namest::viewt view;
+  state.get_level2().current_names.get_view(view);
+
+  for(const auto &pair : view)
   {
-    const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
+    const irep_idt l1_o_id = pair.second.first.get_l1_object_identifier();
+
     // could use iteration over local_objects as l1_o_id is prefix
     if(frame.local_objects.find(l1_o_id)==frame.local_objects.end())
       continue;
 
     // get original name
-    ssa_exprt lhs(c_it->second.first.get_original_expr());
+    ssa_exprt lhs(pair.second.first.get_original_expr());
 
     // get L0 name for current thread
     lhs.set_level_0(t);
@@ -71,18 +73,16 @@ void goto_symext::symex_start_thread(statet &state)
     CHECK_RETURN(l1_index == 0);
 
     // set up L1 name
-    auto emplace_result = state.level1.current_names.emplace(
-      std::piecewise_construct,
-      std::forward_as_tuple(lhs.get_l1_object_identifier()),
-      std::forward_as_tuple(lhs, 0));
-    CHECK_RETURN(emplace_result.second);
+    state.level1.current_names.insert(
+      lhs.get_l1_object_identifier(), std::make_pair(lhs, 0));
+
     const ssa_exprt lhs_l1 = state.rename_ssa<L1>(std::move(lhs), ns).get();
     const irep_idt l1_name = lhs_l1.get_l1_object_identifier();
     // store it
     new_thread.call_stack.back().local_objects.insert(l1_name);
 
     // make copy
-    ssa_exprt rhs=c_it->second.first;
+    ssa_exprt rhs = pair.second.first;
 
     exprt::operandst lhs_conditions;
     const bool record_events=state.record_events;

src/util/ssa_expr.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, [email protected]
 class ssa_exprt:public symbol_exprt
 {
 public:
+  ssa_exprt() : symbol_exprt("", typet()) {}
+
   /// Constructor
   /// \param expr: Expression to be converted to SSA symbol
   explicit ssa_exprt(const exprt &expr) : symbol_exprt(expr.type())