Use rename_level1_ssa where possible

In places where rename_level1 is know 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/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_level1(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)

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_level1(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_level1(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_level1(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_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_level1(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_level1(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,