rename_level1 takes a copy instead of reference

This makes the interface clearer as there is no argument that is both an
input and an output.
This also corresponds to how the function was used in a lot of
occurences, in which case the code is now simpler.
In the cases where we actually what the transformation to happen
in-place, we can use std::move.

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_level1(lhs, ns);
+  lhs = rename_level1_ssa(std::move(lhs), ns);
   irep_idt l1_identifier=lhs.get_identifier();
 
   // the type might need renaming
@@ -353,7 +353,7 @@ goto_symex_statet::rename_level1_ssa(ssa_exprt ssa, const namespacet &ns)
   return ssa;
 }
 
-void goto_symex_statet::rename_level1(exprt &expr, const namespacet &ns)
+exprt goto_symex_statet::rename_level1(exprt expr, const namespacet &ns)
 {
   renaming_strategyt strategy;
   strategy.rename_ssa = [this](ssa_exprt ssa, const namespacet &ns) -> exprt {
@@ -368,6 +368,7 @@ void goto_symex_statet::rename_level1(exprt &expr, const namespacet &ns)
       rename(type, irep_idt(), ns, L1);
     };
   ::rename(expr, strategy, ns);
+  return expr;
 }
 
 void goto_symex_statet::rename_level2(exprt &expr, const namespacet &ns)
@@ -596,7 +597,7 @@ void goto_symex_statet::rename_address(
   PRECONDITION(level != L0);
   auto rename_expr = [&](exprt &e) {
     if(level == L1)
-      rename_level1(e, ns);
+      e = rename_level1(e, ns);
     else
       rename_level2(e, ns);
   };
@@ -744,7 +745,7 @@ void goto_symex_statet::rename(
     if(level == L0)
       rename_level0(e, ns);
     else if(level == L1)
-      rename_level1(e, ns);
+      e = rename_level1(std::move(e), ns);
     else
       rename_level2(e, ns);
   };

src/goto-symex/goto_symex_state.h

@@ -181,7 +181,7 @@ class goto_symex_statet final : public goto_statet
   /// the SSA section of background-concepts.md.
   ssa_exprt rename_level0_ssa(ssa_exprt ssa, const namespacet &ns);
   ssa_exprt rename_level1_ssa(ssa_exprt expr, const namespacet &ns);
-  void rename_level1(exprt &expr, const namespacet &ns);
+  exprt rename_level1(exprt expr, const namespacet &ns);
   void rename_level2(exprt &expr, const namespacet &ns);
   void rename(
     typet &type,

src/goto-symex/symex_dead.cpp

@@ -37,12 +37,11 @@ void goto_symext::symex_dead(statet &state)
     else
       rhs=exprt(ID_invalid);
 
-    state.rename_level1(rhs, ns);
-    state.value_set.assign(ssa, rhs, ns, true, false);
+    exprt l1_rhs = state.rename_level1(std::move(rhs), ns);
+    state.value_set.assign(ssa, l1_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

@@ -53,8 +53,8 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     else
       rhs=exprt(ID_invalid);
 
-    state.rename_level1(rhs, ns);
-    state.value_set.assign(ssa, rhs, ns, true, false);
+    exprt l1_rhs = state.rename_level1(std::move(rhs), ns);
+    state.value_set.assign(ssa, l1_rhs, ns, true, false);
   }
 
   // prevent propagation

src/goto-symex/symex_dereference.cpp

@@ -357,11 +357,11 @@ void goto_symext::dereference(exprt &expr, statet &state)
   // from different frames. Would be enough to rename
   // symbols whose address is taken.
   PRECONDITION(!state.call_stack().empty());
-  state.rename_level1(expr, ns);
+  expr = state.rename_level1(std::move(expr), ns);
 
   // start the recursion!
   dereference_rec(expr, state);
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
-  state.rename_level1(expr, ns);
+  expr = state.rename_level1(std::move(expr), ns);
 }

src/goto-symex/symex_function_call.cpp

@@ -427,17 +427,17 @@ static void locality(
     // identifiers may be shared among functions
     // (e.g., due to inlining or other code restructuring)
 
-    state.rename_level1(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