rename_level2 takes a copy instead of reference

Similar changes to the previous commit but for level2.

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-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_level2(ssa, ns);
-
-  return checker->get(ssa);
+  return checker->get(symex_state->rename_level2(e, ns));
 }
 
 void scratch_programt::append(goto_programt::instructionst &new_instructions)

src/goto-symex/goto_symex_state.cpp

@@ -399,7 +399,7 @@ exprt goto_symex_statet::rename_level2_ssa(ssa_exprt ssa, const namespacet &ns)
   return ssa;
 }
 
-void goto_symex_statet::rename_level2(exprt &expr, const namespacet &ns)
+exprt goto_symex_statet::rename_level2(exprt expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
   renaming_strategyt strategy;
@@ -415,6 +415,7 @@ void goto_symex_statet::rename_level2(exprt &expr, const namespacet &ns)
       rename(type, irep_idt(), ns, L2);
     };
   ::rename(expr, strategy, ns);
+  return expr;
 }
 
 /// thread encoding
@@ -604,7 +605,7 @@ void goto_symex_statet::rename_address(
     if(level == L1)
       e = rename_level1(e, ns);
     else
-      rename_level2(e, ns);
+      e = rename_level2(e, ns);
   };
 
   if(expr.id()==ID_symbol &&
@@ -752,7 +753,7 @@ void goto_symex_statet::rename(
     else if(level == L1)
       e = rename_level1(std::move(e), ns);
     else
-      rename_level2(e, ns);
+      e = rename_level2(e, ns);
   };
 
   // rename all the symbols with their last known value

src/goto-symex/goto_symex_state.h

@@ -183,7 +183,7 @@ class goto_symex_statet final : public goto_statet
   ssa_exprt rename_level1_ssa(ssa_exprt expr, const namespacet &ns);
   exprt rename_level1(exprt expr, const namespacet &ns);
   exprt rename_level2_ssa(ssa_exprt expr, const namespacet &ns);
-  void rename_level2(exprt &expr, const namespacet &ns);
+  exprt rename_level2(exprt expr, const namespacet &ns);
   void rename(
     typet &type,
     const irep_idt &l1_identifier,

src/goto-symex/symex_assign.cpp

@@ -212,13 +212,13 @@ void goto_symext::symex_assign_symbol(
     tmp_ssa_rhs.swap(ssa_rhs);
   }
 
-  state.rename_level2(ssa_rhs, ns);
-  do_simplify(ssa_rhs);
+  exprt l2_rhs = state.rename_level2(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_level2(ssa_full_lhs, ns);
+  exprt l2_full_lhs = state.rename_level2(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_level2(renamed_guard, ns);
+  exprt renamed_guard = state.rename_level2(lhs.cond(), ns);
   do_simplify(renamed_guard);
 
   if(!renamed_guard.is_false())

src/goto-symex/symex_builtin_functions.cpp

@@ -69,8 +69,8 @@ void goto_symext::symex_allocate(
   }
   else
   {
-    exprt tmp_size=size;
-    state.rename_level2(tmp_size, ns); // to allow constant propagation
+    // to allow constant propagation
+    exprt tmp_size = state.rename_level2(size, ns);
     simplify(tmp_size, ns);
 
     // special treatment for sizeof(T)*x
@@ -91,10 +91,10 @@ void goto_symext::symex_allocate(
           tmp_size.operands().size() == 2 &&
           (tmp_size.op0().is_constant() || tmp_size.op1().is_constant()))
         {
-          exprt s=tmp_size.op0();
+          exprt s = tmp_size.op0();
           if(s.is_constant())
           {
-            s=tmp_size.op1();
+            s = tmp_size.op1();
             PRECONDITION(*c_sizeof_type_rec(tmp_size.op0()) == *tmp_type);
           }
           else
@@ -135,7 +135,7 @@ void goto_symext::symex_allocate(
       size_symbol.base_name=
         "dynamic_object_size"+std::to_string(dynamic_counter);
       size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
-      size_symbol.type=tmp_size.type();
+      size_symbol.type = tmp_size.type();
       size_symbol.mode = mode;
       size_symbol.type.set(ID_C_constant, true);
       size_symbol.value = array_size;
@@ -161,8 +161,8 @@ void goto_symext::symex_allocate(
 
   state.symbol_table.add(value_symbol);
 
-  exprt zero_init=code.op1();
-  state.rename_level2(zero_init, ns); // to allow constant propagation
+  // to allow constant propagation
+  exprt zero_init = state.rename_level2(code.op1(), ns);
   simplify(zero_init, ns);
 
   INVARIANT(
@@ -230,10 +230,10 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
   if(lhs.is_nil())
     return; // ignore
 
-  exprt tmp=code.op0();
-  state.rename_level2(tmp, ns); // to allow constant propagation
+  // to allow constant propagation
+  exprt tmp = state.rename_level2(code.op0(), ns);
   do_simplify(tmp);
-  irep_idt id=get_symbol(tmp);
+  irep_idt id = get_symbol(tmp);
 
   const auto zero = zero_initializer(lhs.type(), code.source_location(), ns);
   CHECK_RETURN(zero.has_value());
@@ -308,11 +308,10 @@ void goto_symext::symex_printf(
 {
   PRECONDITION(!rhs.operands().empty());
 
-  exprt tmp_rhs=rhs;
-  state.rename_level2(tmp_rhs, ns);
+  exprt tmp_rhs = state.rename_level2(rhs, ns);
   do_simplify(tmp_rhs);
 
-  const exprt::operandst &operands=tmp_rhs.operands();
+  const exprt::operandst &operands = tmp_rhs.operands();
   std::list<exprt> args;
 
   for(std::size_t i=1; i<operands.size(); i++)
@@ -333,20 +332,19 @@ void goto_symext::symex_input(
 {
   PRECONDITION(code.operands().size() >= 2);
 
-  exprt id_arg=code.op0();
-
-  state.rename_level2(id_arg, ns);
+  exprt id_arg = state.rename_level2(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_level2(args.back(), ns);
-    do_simplify(args.back());
+    exprt l2_arg = state.rename_level2(args.back(), ns);
+    do_simplify(l2_arg);
+    args.back() = std::move(l2_arg);
   }
 
-  const irep_idt input_id=get_string_argument(id_arg, ns);
+  const irep_idt input_id = get_string_argument(id_arg, ns);
 
   target.input(state.guard.as_expr(), state.source, input_id, args);
 }
@@ -356,18 +354,16 @@ void goto_symext::symex_output(
   const codet &code)
 {
   PRECONDITION(code.operands().size() >= 2);
-
-  exprt id_arg=code.op0();
-
-  state.rename_level2(id_arg, ns);
+  exprt id_arg = state.rename_level2(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_level2(args.back(), ns);
-    do_simplify(args.back());
+    exprt l2_arg = state.rename_level2(args.back(), ns);
+    do_simplify(l2_arg);
+    args.back() = std::move(l2_arg);
   }
 
   const irep_idt output_id=get_string_argument(id_arg, ns);
@@ -478,11 +474,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_level2(var, ns);
-      vars.push_back(var);
-    }
+      vars.push_back(state.rename_level2(code.arguments()[j], ns));
 
     target.output(state.guard.as_expr(), state.source, event, vars);
   }

src/goto-symex/symex_decl.cpp

@@ -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_level2(ssa, ns);
+  exprt expr_l2 = state.rename_level2_ssa(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_function_call.cpp

@@ -272,7 +272,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_level2(a, ns);
+    a = state.rename_level2(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_level2(new_guard, ns);
+  exprt new_guard = state.rename_level2(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_level2(guard_expr, ns);
+      guard_expr = state.rename_level2(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_level2(expr, ns);
+  exprt l2_expr = state.rename_level2(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_level2(tmp, ns);
-      symex_assume(state, tmp);
+      symex_assume(state, state.rename_level2(std::move(tmp), ns));
     }
 
     symex_transition(state);