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.

As a side effect we have to define a version that returns a ssa_exprt as
exprt is sometimes not precise enough.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -168,7 +168,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
@@ -324,31 +324,38 @@ goto_symex_statet::rename_level0(const symbol_exprt &expr, const namespacet &ns)
   return ssa;
 }
 
-void goto_symex_statet::rename_level1(exprt &expr, const namespacet &ns)
+ssa_exprt goto_symex_statet::rename_level1_ssa(
+  ssa_exprt ssa, const namespacet &ns)
+{
+  set_l1_indices(level0, level1, ssa, source.thread_nr, ns);
+  rename(ssa.type(), ssa.get_identifier(), ns, L1);
+  ssa.update_type();
+  return ssa;
+}
+
+exprt goto_symex_statet::rename_level1(exprt expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
   if(auto ssa = expr_try_dynamic_cast<ssa_exprt>(expr))
   {
-    set_l1_indices(level0, level1, *ssa, source.thread_nr, ns);
-    rename(expr.type(), ssa->get_identifier(), ns, L1);
-    ssa->update_type();
+    return rename_level1_ssa(*ssa, ns);
   }
   else if(expr.id() == ID_symbol)
   {
     // we never rename function symbols
     if(expr.type().id() == ID_code)
     {
       rename(expr.type(), to_symbol_expr(expr).get_identifier(), ns, L1);
-      return;
+      return expr;
     }
 
-    expr = ssa_exprt(expr);
-    rename_level1(expr, ns);
+    return rename_level1_ssa(ssa_exprt{expr}, ns);
   }
   else if(auto address_of_expr = expr_try_dynamic_cast<address_of_exprt>(expr))
   {
     rename_address(address_of_expr->object(), ns, L1);
     to_pointer_type(expr.type()).subtype() = address_of_expr->object().type();
+    return expr;
   }
   else
   {
@@ -357,9 +364,10 @@ void goto_symex_statet::rename_level1(exprt &expr, const namespacet &ns)
 
     // do this recursively
     for(auto &op : expr.operands())
-      rename_level1(op, ns);
+      op = rename_level1(std::move(op), ns);
 
     fix_type(expr);
+    return expr;
   }
 }
 
@@ -618,7 +626,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);
   };
@@ -722,7 +730,7 @@ void goto_symex_statet::rename(
     if(level == L0)
       e = rename_level0(std::move(e), ns);
     if(level == L1)
-      rename_level1(e, ns);
+      e = rename_level1(e, ns);
     else
       rename_level2(e, ns);
   };

src/goto-symex/goto_symex_state.h

@@ -177,7 +177,8 @@ class goto_symex_statet final : public goto_statet
   /// A full explanation of SSA (which is why we do this renaming) is in
   /// the SSA section of background-concepts.md.
   ssa_exprt rename_level0(const symbol_exprt &expr, const namespacet &ns);
-  void rename_level1(exprt &expr, const namespacet &ns);
+  ssa_exprt rename_level1_ssa(ssa_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

@@ -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)
@@ -38,12 +37,11 @@ void goto_symext::symex_dead(statet &state)
       return 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

@@ -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);
@@ -54,8 +53,8 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
       return 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
@@ -64,9 +63,9 @@ 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
-  const auto level2_it =
-    state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 0))
-      .first;
+  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;
@@ -84,14 +83,10 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     state.guard.as_expr(),
     ssa,
     state.source,
-    hidden?
-      symex_targett::assignment_typet::HIDDEN:
-      symex_targett::assignment_typet::STATE);
+    hidden ? symex_targett::assignment_typet::HIDDEN
+           : symex_targett::assignment_typet::STATE);
 
   if(state.dirty(ssa.get_object_name()) && state.atomic_section_id == 0)
     target.shared_write(
-      state.guard.as_expr(),
-      ssa,
-      state.atomic_section_id,
-      state.source);
+      state.guard.as_expr(), ssa, state.atomic_section_id, state.source);
 }

src/goto-symex/symex_dereference_state.cpp

@@ -36,9 +36,9 @@ bool symex_dereference_statet::has_failed_symbol(
     {
       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);
       symbol=sym_ptr;
       return true;
@@ -56,9 +56,9 @@ bool symex_dereference_statet::has_failed_symbol(
     {
       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);
       symbol=sym_ptr;
       return true;

src/goto-symex/symex_goto.cpp

@@ -247,8 +247,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{}};