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

@@ -62,11 +62,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

@@ -371,7 +371,36 @@ exprt goto_symex_statet::rename_level1(exprt expr, const namespacet &ns)
   }
 }
 
-void goto_symex_statet::rename_level2(exprt &expr, const namespacet &ns)
+ssa_exprt
+goto_symex_statet::rename_level2_ssa(ssa_exprt ssa, const namespacet &ns)
+{
+  set_l1_indices(level0, level1, ssa, source.thread_nr, ns);
+  rename(ssa.type(), ssa.get_identifier(), ns);
+  ssa.update_type();
+
+  if(l2_thread_read_encoding(ssa, ns))
+  {
+    // renaming taken care of by l2_thread_encoding
+  }
+  else if(!ssa.get_level_2().empty())
+  {
+    // already at L2
+  }
+  else
+  {
+    // We also consider propagation if we go up to L2.
+    // L1 identifiers are used for propagation!
+    auto p_it = propagation.find(ssa.get_identifier());
+
+    if(p_it != propagation.end())
+      ssa = to_ssa_expr(p_it->second); // already L2
+    else
+      set_l2_indices(level0, level1, level2, ssa, source.thread_nr, ns);
+  }
+  return ssa;
+}
+
+exprt goto_symex_statet::rename_level2(exprt expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
   if(expr.id()==ID_symbol &&
@@ -408,12 +437,11 @@ void goto_symex_statet::rename_level2(exprt &expr, const namespacet &ns)
     if(expr.type().id() == ID_code)
     {
       rename(expr.type(), to_symbol_expr(expr).get_identifier(), ns, L2);
-
-      return;
     }
-
-    expr=ssa_exprt(expr);
-    rename_level2(expr, ns);
+    else
+    {
+      return rename_level2_ssa(ssa_exprt{expr}, ns);
+    }
   }
   else if(expr.id()==ID_address_of)
   {
@@ -427,7 +455,7 @@ void goto_symex_statet::rename_level2(exprt &expr, const namespacet &ns)
 
     // do this recursively
     Forall_operands(it, expr)
-      rename_level2(*it, ns);
+      *it = rename_level2(std::move(*it), ns);
 
     INVARIANT(
       (expr.id() != ID_with ||
@@ -438,6 +466,7 @@ void goto_symex_statet::rename_level2(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

src/goto-symex/goto_symex_state.h

@@ -179,7 +179,8 @@ class goto_symex_statet final : public goto_statet
   ssa_exprt rename_level0(const symbol_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);
+  ssa_exprt rename_level2_ssa(ssa_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,7 +254,7 @@ 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()),
+    l2_full_lhs, add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
     ssa_rhs,
     state.source,
     assignment_type);
@@ -407,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
@@ -89,12 +89,13 @@ void goto_symext::symex_allocate(
         else if(
           !alloc_size.has_value() && tmp_size.id() == ID_mult &&
           tmp_size.operands().size() == 2 &&
-          (tmp_size.op0().is_constant() || tmp_size.op1().is_constant()))
+          (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 +136,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,12 +162,13 @@ 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(
-    zero_init.is_constant(), "allocate expects constant as second argument");
+    zero_init.is_constant(),
+    "allocate expects constant as second argument");
 
   if(!zero_init.is_zero() && !zero_init.is_false())
   {
@@ -231,10 +233,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());
@@ -309,11 +311,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++)
@@ -334,20 +335,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);
 }
@@ -357,18 +357,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);
@@ -479,11 +477,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,7 @@ 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);
+  state.rename_level2_ssa(ssa, ns);
   state.record_events=record_events;
 
   // we hide the declaration of auxiliary variables

src/goto-symex/symex_function_call.cpp

@@ -267,7 +267,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())
@@ -268,8 +267,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);