Merge pull request #3554 from romainbrenguier/optimize/symex-assignment

Optimize calls to increase_counter

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -187,9 +187,9 @@ void goto_symex_statet::assignment(
 #endif
 
   // do the l2 renaming
-  if(level2.current_names.find(l1_identifier)==level2.current_names.end())
-    level2.current_names[l1_identifier]=std::make_pair(lhs, 0);
-  level2.increase_counter(l1_identifier);
+  const auto level2_it =
+    level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0)).first;
+  symex_renaming_levelt::increase_counter(level2_it);
   set_l2_indices(lhs, ns);
 
   // in case we happen to be multi-threaded, record the memory access
@@ -442,9 +442,10 @@ bool goto_symex_statet::l2_thread_read_encoding(
 
     if(a_s_read.second.empty())
     {
-      if(level2.current_names.find(l1_identifier)==level2.current_names.end())
-        level2.current_names[l1_identifier]=std::make_pair(ssa_l1, 0);
-      level2.increase_counter(l1_identifier);
+      auto level2_it =
+        level2.current_names.emplace(l1_identifier, std::make_pair(ssa_l1, 0))
+          .first;
+      symex_renaming_levelt::increase_counter(level2_it);
       a_s_read.first=level2.current_count(l1_identifier);
     }
 
@@ -480,8 +481,9 @@ bool goto_symex_statet::l2_thread_read_encoding(
     return true;
   }
 
-  if(level2.current_names.find(l1_identifier)==level2.current_names.end())
-    level2.current_names[l1_identifier]=std::make_pair(ssa_l1, 0);
+  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)
@@ -492,7 +494,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
   }
 
   // produce a fresh L2 name
-  level2.increase_counter(l1_identifier);
+  symex_renaming_levelt::increase_counter(level2_it);
   set_l2_indices(ssa_l1, ns);
   expr=ssa_l1;
 

src/goto-symex/renaming_level.h

@@ -38,10 +38,9 @@ struct symex_renaming_levelt
   }
 
   /// Increase the counter corresponding to an identifier
-  void increase_counter(const irep_idt &identifier)
+  static void increase_counter(const current_namest::iterator &it)
   {
-    PRECONDITION(current_names.find(identifier) != current_names.end());
-    ++current_names[identifier].second;
+    ++it->second.second;
   }
 
   /// Add the \c ssa_exprt of current_names to vars

src/goto-symex/symex_dead.cpp

@@ -52,7 +52,7 @@ void goto_symext::symex_dead(statet &state)
   state.propagation.erase(l1_identifier);
 
   // L2 renaming
-  if(state.level2.current_names.find(l1_identifier)!=
-     state.level2.current_names.end())
-    state.level2.increase_counter(l1_identifier);
+  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);
 }

src/goto-symex/symex_decl.cpp

@@ -68,10 +68,10 @@ 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
-  if(state.level2.current_names.find(l1_identifier)==
-     state.level2.current_names.end())
-    state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0);
-  state.level2.increase_counter(l1_identifier);
+  const auto level2_it =
+    state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 0))
+      .first;
+  symex_renaming_levelt::increase_counter(level2_it);
   const bool record_events=state.record_events;
   state.record_events=false;
   state.rename(ssa, ns);

src/goto-symex/symex_function_call.cpp

@@ -408,25 +408,32 @@ void goto_symext::locality(
     const irep_idt l0_name=ssa.get_identifier();
 
     // save old L1 name for popping the frame
-    const 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[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))
+               .first;
+    }
 
     // do L1 renaming -- these need not be unique, as
     // identifiers may be shared among functions
     // (e.g., due to inlining or other code restructuring)
 
-    state.level1.current_names[l0_name]=
-      std::make_pair(ssa, frame_nr);
     state.rename(ssa, ns, goto_symex_statet::L1);
 
     irep_idt l1_name=ssa.get_identifier();
     unsigned offset=0;
 
     while(state.l1_history.find(l1_name)!=state.l1_history.end())
     {
-      state.level1.increase_counter(l0_name);
+      symex_renaming_levelt::increase_counter(c_it);
       ++offset;
       ssa.set_level_1(frame_nr+offset);
       l1_name=ssa.get_identifier();