Use rename_level1_ssa where possible

In places where rename<L1> is known to be called on an ssa_exprt, we
replace the call by a call to rename_level1_ssa to avoid unecessary
decision making and show more information in the return type.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -162,7 +162,7 @@ void goto_symex_statet::assignment(
   bool allow_pointer_unsoundness)
 {
   // identifier should be l0 or l1, make sure it's l1
-  rename<L1>(lhs, ns);
+  lhs = rename_level1_ssa(std::move(lhs), ns);
   irep_idt l1_identifier=lhs.get_identifier();
 
   // the type might need renaming

src/goto-symex/symex_dead.cpp

@@ -26,8 +26,7 @@ void goto_symext::symex_dead(statet &state)
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.
 
-  ssa_exprt ssa(code.symbol());
-  state.rename<goto_symex_statet::L1>(ssa, ns);
+  ssa_exprt ssa = state.rename_level1_ssa(ssa_exprt{code.symbol()}, ns);
 
   // in case of pointers, put something into the value set
   if(code.symbol().type().id() == ID_pointer)
@@ -42,8 +41,7 @@ void goto_symext::symex_dead(statet &state)
     state.value_set.assign(ssa, rhs, ns, true, false);
   }
 
-  ssa_exprt ssa_lhs=to_ssa_expr(ssa);
-  const irep_idt &l1_identifier=ssa_lhs.get_identifier();
+  const irep_idt &l1_identifier = ssa.get_identifier();
 
   // prevent propagation
   state.propagation.erase(l1_identifier);

src/goto-symex/symex_decl.cpp

@@ -37,9 +37,8 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.
 
-  ssa_exprt ssa(expr);
-  state.rename<goto_symex_statet::L1>(ssa, ns);
-  const irep_idt &l1_identifier=ssa.get_identifier();
+  ssa_exprt ssa = state.rename_level1_ssa(ssa_exprt{expr}, ns);
+  const irep_idt &l1_identifier = ssa.get_identifier();
 
   // rename type to L2
   state.rename(ssa.type(), l1_identifier, ns);

src/goto-symex/symex_dereference_state.cpp

@@ -50,9 +50,9 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
     {
       symbolt sym=*symbol;
       symbolt *sym_ptr=nullptr;
-      symbol_exprt sym_expr=sym.symbol_expr();
-      state.rename<goto_symex_statet::L1>(sym_expr, ns);
-      sym.name=to_ssa_expr(sym_expr).get_identifier();
+      const ssa_exprt sym_expr =
+        state.rename_level1_ssa(ssa_exprt{sym.symbol_expr()}, ns);
+      sym.name = sym_expr.get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       return sym_ptr;
     }
@@ -70,9 +70,9 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
     {
       symbolt sym=*symbol;
       symbolt *sym_ptr=nullptr;
-      symbol_exprt sym_expr=sym.symbol_expr();
-      state.rename<goto_symex_statet::L1>(sym_expr, ns);
-      sym.name=to_ssa_expr(sym_expr).get_identifier();
+      const ssa_exprt sym_expr =
+        state.rename_level1_ssa(ssa_exprt{sym.symbol_expr()}, ns);
+      sym.name = sym_expr.get_identifier();
       state.symbol_table.move(sym, sym_ptr);
       return sym_ptr;
     }

src/goto-symex/symex_function_call.cpp

@@ -418,17 +418,17 @@ static void locality(
     // identifiers may be shared among functions
     // (e.g., due to inlining or other code restructuring)
 
-    state.rename<goto_symex_statet::L1>(ssa, ns);
+    ssa_exprt ssa_l1 = state.rename_level1_ssa(std::move(ssa), ns);
 
-    irep_idt l1_name=ssa.get_identifier();
+    irep_idt l1_name = ssa_l1.get_identifier();
     unsigned offset=0;
 
     while(state.l1_history.find(l1_name)!=state.l1_history.end())
     {
       symex_renaming_levelt::increase_counter(c_it);
       ++offset;
-      ssa.set_level_1(frame_nr+offset);
-      l1_name=ssa.get_identifier();
+      ssa_l1.set_level_1(frame_nr + offset);
+      l1_name = ssa_l1.get_identifier();
     }
 
     // now unique -- store

src/goto-symex/symex_goto.cpp

@@ -248,8 +248,8 @@ void goto_symext::symex_goto(statet &state)
         symbol_exprt(statet::guard_identifier(), bool_typet());
       exprt new_rhs = boolean_negate(new_guard);
 
-      ssa_exprt new_lhs(guard_symbol_expr);
-      state.rename<goto_symex_statet::L1>(new_lhs, ns);
+      ssa_exprt new_lhs =
+        state.rename_level1_ssa(ssa_exprt{guard_symbol_expr}, ns);
       state.assignment(new_lhs, new_rhs, ns, true, false);
 
       guardt guard{true_exprt{}};

src/goto-symex/symex_start_thread.cpp

@@ -73,8 +73,8 @@ void goto_symext::symex_start_thread(statet &state)
       std::forward_as_tuple(lhs.get_l1_object_identifier()),
       std::forward_as_tuple(lhs, 0));
     CHECK_RETURN(emplace_result.second);
-    state.rename<goto_symex_statet::L1>(lhs, ns);
-    const irep_idt l1_name=lhs.get_l1_object_identifier();
+    const ssa_exprt lhs_l1 = state.rename_level1_ssa(std::move(lhs), ns);
+    const irep_idt l1_name = lhs_l1.get_l1_object_identifier();
     // store it
     state.l1_history.insert(l1_name);
     new_thread.call_stack.back().local_objects.insert(l1_name);
@@ -87,7 +87,7 @@ void goto_symext::symex_start_thread(statet &state)
     state.record_events=false;
     symex_assign_symbol(
       state,
-      lhs,
+      lhs_l1,
       nil_exprt(),
       rhs,
       guard,