Make increase_counter take iterator

Taking an iterator instead of an identifier removes the need for a
precondition (thus avoiding a lookup) and can avoid an additional
lookup.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -185,8 +185,9 @@ void goto_symex_statet::assignment(
 #endif
 
   // do the l2 renaming
-  level2.current_names.emplace(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
@@ -439,8 +440,10 @@ bool goto_symex_statet::l2_thread_read_encoding(
 
     if(a_s_read.second.empty())
     {
-      level2.current_names.emplace(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);
     }
 
@@ -476,7 +479,9 @@ bool goto_symex_statet::l2_thread_read_encoding(
     return true;
   }
 
-  level2.current_names.emplace(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)
@@ -487,7 +492,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,8 +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
-  state.level2.current_names.emplace(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,7 +408,7 @@ 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())
     {
@@ -417,8 +417,9 @@ void goto_symext::locality(
     }
     else
     {
-      state.level1.current_names.emplace(
-        l0_name, std::make_pair(ssa, frame_nr));
+      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
@@ -432,7 +433,7 @@ void goto_symext::locality(
 
     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();