Make rename take 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 want the transformation to happen
in-place, we can use std::move.

Author: romainbrenguier

src/goto-instrument/accelerate/scratch_program.cpp

@@ -69,11 +69,7 @@ bool scratch_programt::check_sat(bool do_slice)
 
 exprt scratch_programt::eval(const exprt &e)
 {
-  exprt ssa=e;
-
-  symex_state->rename<goto_symex_statet::L2>(ssa, ns);
-
-  return checker->get(ssa);
+  return checker->get(symex_state->rename<goto_symex_statet::L2>(e, ns));
 }
 
 void scratch_programt::append(goto_programt::instructionst &new_instructions)

src/goto-symex/goto_symex_state.cpp

@@ -281,7 +281,7 @@ goto_symex_statet::rename_level1_ssa(ssa_exprt ssa, const namespacet &ns)
 }
 
 template <goto_symex_statet::levelt level>
-void goto_symex_statet::rename(exprt &expr, const namespacet &ns)
+exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
 
@@ -329,13 +329,9 @@ void goto_symex_statet::rename(exprt &expr, const namespacet &ns)
   {
     // we never rename function symbols
     if(as_const(expr).type().id() == ID_code)
-    {
       rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
-      return;
-    }
-
-    expr=ssa_exprt(expr);
-    rename<level>(expr, ns);
+    else
+      expr = rename<level>(ssa_exprt(expr), ns);
   }
   else if(expr.id()==ID_address_of)
   {
@@ -350,7 +346,7 @@ void goto_symex_statet::rename(exprt &expr, const namespacet &ns)
 
     // do this recursively
     Forall_operands(it, expr)
-      rename<level>(*it, ns);
+      *it = rename<level>(std::move(*it), ns);
 
     const exprt &c_expr = as_const(expr);
     INVARIANT(
@@ -362,6 +358,7 @@ void goto_symex_statet::rename(exprt &expr, const namespacet &ns)
       "Type of renamed expr should be the same as operands for with_exprt and "
       "if_exprt");
   }
+  return expr;
 }
 
 /// thread encoding
@@ -571,13 +568,13 @@ void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
       expr.type() = to_array_type(index_expr.array().type()).subtype();
 
       // the index is not an address
-      rename<level>(index_expr.index(), ns);
+      index_expr.index() = rename<level>(std::move(index_expr.index()), ns);
     }
     else if(expr.id()==ID_if)
     {
       // the condition is not an address
       if_exprt &if_expr=to_if_expr(expr);
-      rename<level>(if_expr.cond(), ns);
+      if_expr.cond() = rename<level>(std::move(if_expr.cond()), ns);
       rename_address<level>(if_expr.true_case(), ns);
       rename_address<level>(if_expr.false_case(), ns);
 
@@ -716,7 +713,7 @@ void goto_symex_statet::rename(
   {
     auto &array_type = to_array_type(type);
     rename<level>(array_type.subtype(), irep_idt(), ns);
-    rename<level>(array_type.size(), ns);
+    array_type.size() = rename<level>(std::move(array_type.size()), ns);
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
   {
@@ -727,7 +724,10 @@ void goto_symex_statet::rename(
     {
       // be careful, or it might get cyclic
       if(component.type().id() == ID_array)
-        rename<level>(to_array_type(component.type()).size(), ns);
+      {
+        auto &array_type = to_array_type(component.type());
+        array_type.size() = rename<level>(std::move(array_type.size()), ns);
+      }
       else if(component.type().id() != ID_pointer)
         rename<level>(component.type(), irep_idt(), ns);
     }

src/goto-symex/goto_symex_state.h

@@ -180,7 +180,7 @@ 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.
   template <levelt level = L2>
-  void rename(exprt &expr, const namespacet &ns);
+  exprt rename(exprt expr, const namespacet &ns);
 
   ssa_exprt rename_level0_ssa(ssa_exprt ssa, const namespacet &ns);
 

src/goto-symex/symex_assign.cpp

@@ -212,13 +212,13 @@ void goto_symext::symex_assign_symbol(
     tmp_ssa_rhs.swap(ssa_rhs);
   }
 
-  state.rename(ssa_rhs, ns);
-  do_simplify(ssa_rhs);
+  exprt l2_rhs = state.rename(std::move(ssa_rhs), ns);
+  do_simplify(l2_rhs);
 
   ssa_exprt ssa_lhs=lhs;
   state.assignment(
     ssa_lhs,
-    ssa_rhs,
+    l2_rhs,
     ns,
     symex_config.simplify_opt,
     symex_config.constant_propagation,
@@ -228,7 +228,7 @@ void goto_symext::symex_assign_symbol(
   ssa_full_lhs=add_to_lhs(ssa_full_lhs, ssa_lhs);
   const bool record_events=state.record_events;
   state.record_events=false;
-  state.rename(ssa_full_lhs, ns);
+  exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns);
   state.record_events=record_events;
 
   guardt tmp_guard(state.guard);
@@ -254,8 +254,9 @@ void goto_symext::symex_assign_symbol(
   target.assignment(
     tmp_guard.as_expr(),
     ssa_lhs,
-    ssa_full_lhs, add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
-    ssa_rhs,
+    l2_full_lhs,
+    add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
+    l2_rhs,
     state.source,
     assignment_type);
 }
@@ -406,8 +407,7 @@ void goto_symext::symex_assign_if(
 
   guardt old_guard=guard;
 
-  exprt renamed_guard=lhs.cond();
-  state.rename(renamed_guard, ns);
+  exprt renamed_guard = state.rename(lhs.cond(), ns);
   do_simplify(renamed_guard);
 
   if(!renamed_guard.is_false())

src/goto-symex/symex_builtin_functions.cpp

@@ -70,8 +70,8 @@ void goto_symext::symex_allocate(
   }
   else
   {
-    exprt tmp_size=size;
-    state.rename(tmp_size, ns); // to allow constant propagation
+    // to allow constant propagation
+    exprt tmp_size = state.rename(size, ns);
     simplify(tmp_size, ns);
 
     // special treatment for sizeof(T)*x
@@ -162,8 +162,8 @@ void goto_symext::symex_allocate(
 
   state.symbol_table.add(value_symbol);
 
-  exprt zero_init=code.op1();
-  state.rename(zero_init, ns); // to allow constant propagation
+  // to allow constant propagation
+  exprt zero_init = state.rename(code.op1(), ns);
   simplify(zero_init, ns);
 
   INVARIANT(
@@ -231,8 +231,8 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
   if(lhs.is_nil())
     return; // ignore
 
-  exprt tmp=code.op0();
-  state.rename(tmp, ns); // to allow constant propagation
+  // to allow constant propagation
+  exprt tmp = state.rename(code.op0(), ns);
   do_simplify(tmp);
   irep_idt id=get_symbol(tmp);
 
@@ -309,8 +309,7 @@ void goto_symext::symex_printf(
 {
   PRECONDITION(!rhs.operands().empty());
 
-  exprt tmp_rhs=rhs;
-  state.rename(tmp_rhs, ns);
+  exprt tmp_rhs = state.rename(rhs, ns);
   do_simplify(tmp_rhs);
 
   const exprt::operandst &operands=tmp_rhs.operands();
@@ -334,17 +333,15 @@ void goto_symext::symex_input(
 {
   PRECONDITION(code.operands().size() >= 2);
 
-  exprt id_arg=code.op0();
-
-  state.rename(id_arg, ns);
+  exprt id_arg = state.rename(code.op0(), ns);
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
-    args.push_back(code.operands()[i]);
-    state.rename(args.back(), ns);
-    do_simplify(args.back());
+    exprt l2_arg = state.rename(code.operands()[i], ns);
+    do_simplify(l2_arg);
+    args.emplace_back(std::move(l2_arg));
   }
 
   const irep_idt input_id=get_string_argument(id_arg, ns);
@@ -357,18 +354,15 @@ void goto_symext::symex_output(
   const codet &code)
 {
   PRECONDITION(code.operands().size() >= 2);
-
-  exprt id_arg=code.op0();
-
-  state.rename(id_arg, ns);
+  exprt id_arg = state.rename(code.op0(), ns);
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
-    args.push_back(code.operands()[i]);
-    state.rename(args.back(), ns);
-    do_simplify(args.back());
+    exprt l2_arg = state.rename(code.operands()[i], ns);
+    do_simplify(l2_arg);
+    args.emplace_back(std::move(l2_arg));
   }
 
   const irep_idt output_id=get_string_argument(id_arg, ns);
@@ -479,11 +473,7 @@ void goto_symext::symex_trace(
     irep_idt event = to_string_constant(code.arguments()[1].op0()).get_value();
 
     for(std::size_t j=2; j<code.arguments().size(); j++)
-    {
-      exprt var(code.arguments()[j]);
-      state.rename(var, ns);
-      vars.push_back(var);
-    }
+      vars.push_back(state.rename(code.arguments()[j], ns));
 
     target.output(state.guard.as_expr(), state.source, event, vars);
   }

src/goto-symex/symex_dead.cpp

@@ -37,8 +37,9 @@ void goto_symext::symex_dead(statet &state)
     else
       rhs=exprt(ID_invalid);
 
-    state.rename<goto_symex_statet::L1>(rhs, ns);
-    state.value_set.assign(ssa, rhs, ns, true, false);
+    const exprt l1_rhs =
+      state.rename<goto_symex_statet::L1>(std::move(rhs), ns);
+    state.value_set.assign(ssa, l1_rhs, ns, true, false);
   }
 
   const irep_idt &l1_identifier = ssa.get_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<goto_symex_statet::L1>(rhs, ns);
-    state.value_set.assign(ssa, rhs, ns, true, false);
+    exprt l1_rhs = state.rename<goto_symex_statet::L1>(std::move(rhs), ns);
+    state.value_set.assign(ssa, l1_rhs, ns, true, false);
   }
 
   // prevent propagation
@@ -69,7 +69,11 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   symex_renaming_levelt::increase_counter(level2_it);
   const bool record_events=state.record_events;
   state.record_events=false;
-  state.rename(ssa, ns);
+  exprt expr_l2 = state.rename(std::move(ssa), ns);
+  INVARIANT(
+    expr_l2.id() == ID_symbol && expr_l2.get_bool(ID_C_SSA_symbol),
+    "symbol to declare should not be replaced by constant propagation");
+  ssa = to_ssa_expr(expr_l2);
   state.record_events=record_events;
 
   // we hide the declaration of auxiliary variables

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<goto_symex_statet::L1>(expr, ns);
+  exprt l1_expr = state.rename<goto_symex_statet::L1>(expr, ns);
 
   // start the recursion!
-  dereference_rec(expr, state);
+  dereference_rec(l1_expr, state);
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
-  state.rename<goto_symex_statet::L1>(expr, ns);
+  expr = state.rename<goto_symex_statet::L1>(std::move(l1_expr), ns);
 }

src/goto-symex/symex_function_call.cpp

@@ -261,7 +261,7 @@ void goto_symext::symex_function_call_code(
   // read the arguments -- before the locality renaming
   exprt::operandst arguments = call.arguments();
   for(auto &a : arguments)
-    state.rename(a, ns);
+    a = state.rename(std::move(a), ns);
 
   // we hide the call if the caller and callee are both hidden
   const bool hidden = state.top().hidden_function && goto_function.is_hidden();

src/goto-symex/symex_goto.cpp

@@ -37,8 +37,7 @@ void goto_symext::symex_goto(statet &state)
   exprt old_guard = instruction.get_condition();
   clean_expr(old_guard, state, false);
 
-  exprt new_guard=old_guard;
-  state.rename(new_guard, ns);
+  exprt new_guard = state.rename(old_guard, ns);
   do_simplify(new_guard);
 
   if(new_guard.is_false())
@@ -269,8 +268,7 @@ void goto_symext::symex_goto(statet &state)
         original_source,
         symex_targett::assignment_typet::GUARD);
 
-      guard_expr = boolean_negate(guard_symbol_expr);
-      state.rename(guard_expr, ns);
+      guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns);
     }
 
     if(state.has_saved_jump_target)

src/goto-symex/symex_main.cpp

@@ -95,18 +95,18 @@ void goto_symext::vcc(
   }
 
   // now rename, enables propagation
-  state.rename(expr, ns);
+  exprt l2_expr = state.rename(std::move(expr), ns);
 
   // now try simplifier on it
-  do_simplify(expr);
+  do_simplify(l2_expr);
 
-  if(expr.is_true())
+  if(l2_expr.is_true())
     return;
 
-  state.guard.guard_expr(expr);
+  state.guard.guard_expr(l2_expr);
 
   state.remaining_vccs++;
-  target.assertion(state.guard.as_expr(), expr, msg, state.source);
+  target.assertion(state.guard.as_expr(), l2_expr, msg, state.source);
 }
 
 void goto_symext::symex_assume(statet &state, const exprt &cond)
@@ -410,8 +410,7 @@ void goto_symext::symex_step(
     {
       exprt tmp = instruction.get_condition();
       clean_expr(tmp, state, false);
-      state.rename(tmp, ns);
-      symex_assume(state, tmp);
+      symex_assume(state, state.rename(std::move(tmp), ns));
     }
 
     symex_transition(state);