level2t type for results of rename_level2

Makes it clear from the type that rename_level2 rename an expression up
to level2, and allows us to the renaming level in the type.
The argument is now passed by copy and a new expression
is returned, which also makes the interface of the function clearer.
Note that because of that we need a new version of rename_level2
returning a level2t<ssa_exprt>: before, an ssa_exprt was given as
argument and the type left unchanged but new the argument is copied, so
the returned type would only be level2t<exprt>.

Author: romainbrenguier

src/goto-instrument/accelerate/scratch_program.cpp

@@ -62,7 +62,7 @@ bool scratch_programt::check_sat(bool do_slice)
 
 exprt scratch_programt::eval(const exprt &e)
 {
-  return checker->get(symex_state.rename_level2(e, ns));
+  return checker->get(symex_state.rename_level2(e, ns).expr);
 }
 
 void scratch_programt::append(goto_programt::instructionst &new_instructions)

src/goto-symex/goto_symex_state.cpp

@@ -412,7 +412,7 @@ goto_symex_statet::rename_level1(exprt expr, const namespacet &ns)
   }
 }
 
-ssa_exprt
+level2t<ssa_exprt>
 goto_symex_statet::rename_level2_ssa(ssa_exprt ssa, const namespacet &ns)
 {
   set_l1_indices(level0, level1, ssa, source.thread_nr, ns);
@@ -438,10 +438,11 @@ goto_symex_statet::rename_level2_ssa(ssa_exprt ssa, const namespacet &ns)
     else
       set_l2_indices(level0, level1, level2, ssa, source.thread_nr, ns);
   }
-  return ssa;
+  return level2t<ssa_exprt>{ssa};
 }
 
-exprt goto_symex_statet::rename_level2(exprt expr, const namespacet &ns)
+level2t<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 &&
@@ -497,11 +498,11 @@ exprt goto_symex_statet::rename_level2(exprt expr, const namespacet &ns)
 
     // do this recursively
     Forall_operands(it, expr)
-      *it = rename_level2(std::move(*it), ns);
+      *it = rename_level2(std::move(*it), ns).expr;
 
     fix_type(expr);
   }
-  return expr;
+  return level2t<exprt>{expr};
 }
 
 /// thread encoding
@@ -792,7 +793,7 @@ void goto_symex_statet::rename(
     if(level == L1)
       e = rename_level1(e, ns).expr;
     else
-      rename_level2(e, ns);
+      e = rename_level2(e, ns).expr;
   };
 
   // rename all the symbols with their last known value

src/goto-symex/goto_symex_state.h

@@ -78,7 +78,8 @@ class goto_symex_statet final
   level1t<exprt> rename_level1(exprt expr, const namespacet &ns);
   level1t<ssa_exprt>
   rename_level1(level0t<ssa_exprt> l0_expr, const namespacet &ns);
-  void rename_level2(exprt &expr, const namespacet &ns);
+  level2t<exprt> rename_level2(exprt expr, const namespacet &ns);
+  level2t<ssa_exprt> rename_level2(ssa_exprt ssa, const namespacet &ns);
   void rename(
     typet &type,
     const irep_idt &l1_identifier,

src/goto-symex/renaming_level.h

@@ -71,6 +71,16 @@ struct level1t
   underlyingt expr;
 };
 
+/// Wrapper for expressions that have been renamed at level2
+template <typename underlyingt>
+struct level2t
+{
+  static_assert(
+    std::is_base_of<exprt, underlyingt>::value,
+    "underlyingt should inherit from exprt");
+  underlyingt expr;
+};
+
 inline level1t<ssa_exprt> remove_level2(ssa_exprt ssa)
 {
   ssa.remove_level_2();

src/goto-symex/symex_assign.cpp

@@ -212,13 +212,13 @@ void goto_symext::symex_assign_symbol(
     tmp_ssa_rhs.swap(ssa_rhs);
   }
 
-  exprt l2_rhs = state.rename_level2(std::move(ssa_rhs), ns);
-  do_simplify(l2_rhs);
+  level2t<exprt> l2_rhs = state.rename_level2(ssa_rhs, ns);
+  do_simplify(l2_rhs.expr);
 
   ssa_exprt ssa_lhs=lhs;
   state.assignment(
     ssa_lhs,
-    l2_rhs,
+    l2_rhs.expr,
     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;
-  exprt l2_full_lhs = state.rename_level2(std::move(ssa_full_lhs), ns);
+  level2t<exprt> l2_full_lhs = state.rename_level2(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,
-    l2_full_lhs, add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
-    ssa_rhs,
+    l2_full_lhs.expr,
+    add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
+    l2_rhs.expr,
     state.source,
     assignment_type);
 }
@@ -407,20 +408,20 @@ void goto_symext::symex_assign_if(
 
   guardt old_guard=guard;
 
-  exprt renamed_guard = state.rename_level2(lhs.cond(), ns);
-  do_simplify(renamed_guard);
+  level2t<exprt> renamed_guard = state.rename_level2(lhs.cond(), ns);
+  do_simplify(renamed_guard.expr);
 
-  if(!renamed_guard.is_false())
+  if(!renamed_guard.expr.is_false())
   {
-    guard.add(renamed_guard);
+    guard.add(renamed_guard.expr);
     symex_assign_rec(
       state, lhs.true_case(), full_lhs, rhs, guard, assignment_type);
     guard = std::move(old_guard);
   }
 
-  if(!renamed_guard.is_true())
+  if(!renamed_guard.expr.is_true())
   {
-    guard.add(not_exprt(renamed_guard));
+    guard.add(not_exprt(renamed_guard.expr));
     symex_assign_rec(
       state, lhs.false_case(), full_lhs, rhs, guard, assignment_type);
     guard = std::move(old_guard);

src/goto-symex/symex_builtin_functions.cpp

@@ -70,36 +70,36 @@ void goto_symext::symex_allocate(
   else
   {
     // to allow constant propagation
-    exprt tmp_size = state.rename_level2(size, ns);
-    simplify(tmp_size, ns);
+    level2t<exprt> tmp_size = state.rename_level2(size, ns);
+    simplify(tmp_size.expr, ns);
 
     // special treatment for sizeof(T)*x
     {
-      const auto tmp_type = c_sizeof_type_rec(tmp_size);
+      const auto tmp_type = c_sizeof_type_rec(tmp_size.expr);
 
       if(tmp_type.has_value())
       {
         // Did the size get multiplied?
         auto elem_size = pointer_offset_size(*tmp_type, ns);
-        const auto alloc_size = numeric_cast<mp_integer>(tmp_size);
+        const auto alloc_size = numeric_cast<mp_integer>(tmp_size.expr);
 
         if(!elem_size.has_value() || *elem_size==0)
         {
         }
         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()))
+          !alloc_size.has_value() && tmp_size.expr.id() == ID_mult &&
+          tmp_size.expr.operands().size() == 2 &&
+          (tmp_size.expr.op0().is_constant() ||
+           tmp_size.expr.op1().is_constant()))
         {
-          exprt s = tmp_size.op0();
+          exprt s = tmp_size.expr.op0();
           if(s.is_constant())
           {
-            s = tmp_size.op1();
-            PRECONDITION(*c_sizeof_type_rec(tmp_size.op0()) == *tmp_type);
+            s = tmp_size.expr.op1();
+            PRECONDITION(*c_sizeof_type_rec(tmp_size.expr.op0()) == *tmp_type);
           }
           else
-            PRECONDITION(*c_sizeof_type_rec(tmp_size.op1()) == *tmp_type);
+            PRECONDITION(*c_sizeof_type_rec(tmp_size.expr.op1()) == *tmp_type);
 
           object_type = array_typet(*tmp_type, s);
         }
@@ -112,15 +112,15 @@ void goto_symext::symex_allocate(
             mp_integer elements = *alloc_size / (*elem_size);
 
             if(elements * (*elem_size) == *alloc_size)
-              object_type =
-                array_typet(*tmp_type, from_integer(elements, tmp_size.type()));
+              object_type = array_typet(
+                *tmp_type, from_integer(elements, tmp_size.expr.type()));
           }
         }
       }
     }
 
     if(!object_type.has_value())
-      object_type=array_typet(unsigned_char_type(), tmp_size);
+      object_type = array_typet(unsigned_char_type(), tmp_size.expr);
 
     // we introduce a fresh symbol for the size
     // to prevent any issues of the size getting ever changed
@@ -136,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.expr.type();
       size_symbol.mode = mode;
       size_symbol.type.set(ID_C_constant, true);
       size_symbol.value = array_size;
@@ -163,14 +163,14 @@ void goto_symext::symex_allocate(
   state.symbol_table.add(value_symbol);
 
   // to allow constant propagation
-  exprt zero_init = state.rename_level2(code.op1(), ns);
-  simplify(zero_init, ns);
+  level2t<exprt> zero_init = state.rename_level2(code.op1(), ns);
+  simplify(zero_init.expr, ns);
 
   INVARIANT(
-    zero_init.is_constant(),
+    zero_init.expr.is_constant(),
     "allocate expects constant as second argument");
 
-  if(!zero_init.is_zero() && !zero_init.is_false())
+  if(!zero_init.expr.is_zero() && !zero_init.expr.is_false())
   {
     const auto zero_value =
       zero_initializer(*object_type, code.source_location(), ns);
@@ -234,9 +234,9 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
     return; // ignore
 
   // to allow constant propagation
-  exprt tmp = state.rename_level2(code.op0(), ns);
-  do_simplify(tmp);
-  irep_idt id = get_symbol(tmp);
+  level2t<exprt> tmp = state.rename_level2(code.op0(), ns);
+  do_simplify(tmp.expr);
+  irep_idt id = get_symbol(tmp.expr);
 
   const auto zero = zero_initializer(lhs.type(), code.source_location(), ns);
   CHECK_RETURN(zero.has_value());
@@ -311,10 +311,10 @@ void goto_symext::symex_printf(
 {
   PRECONDITION(!rhs.operands().empty());
 
-  exprt tmp_rhs = state.rename_level2(rhs, ns);
-  do_simplify(tmp_rhs);
+  level2t<exprt> tmp_rhs = state.rename_level2(rhs, ns);
+  do_simplify(tmp_rhs.expr);
 
-  const exprt::operandst &operands = tmp_rhs.operands();
+  const exprt::operandst &operands = tmp_rhs.expr.operands();
   std::list<exprt> args;
 
   for(std::size_t i=1; i<operands.size(); i++)
@@ -335,19 +335,19 @@ void goto_symext::symex_input(
 {
   PRECONDITION(code.operands().size() >= 2);
 
-  exprt id_arg = state.rename_level2(code.op0(), ns);
+  level2t<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]);
-    exprt l2_arg = state.rename_level2(args.back(), ns);
-    do_simplify(l2_arg);
-    args.back() = std::move(l2_arg);
+    level2t<exprt> l2_arg = state.rename_level2(args.back(), ns);
+    do_simplify(l2_arg.expr);
+    args.back() = std::move(l2_arg.expr);
   }
 
-  const irep_idt input_id = get_string_argument(id_arg, ns);
+  const irep_idt input_id = get_string_argument(id_arg.expr, ns);
 
   target.input(state.guard.as_expr(), state.source, input_id, args);
 }
@@ -357,19 +357,19 @@ void goto_symext::symex_output(
   const codet &code)
 {
   PRECONDITION(code.operands().size() >= 2);
-  exprt id_arg = state.rename_level2(code.op0(), ns);
+  level2t<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]);
-    exprt l2_arg = state.rename_level2(args.back(), ns);
-    do_simplify(l2_arg);
-    args.back() = std::move(l2_arg);
+    level2t<exprt> l2_arg = state.rename_level2(args.back(), ns);
+    do_simplify(l2_arg.expr);
+    args.back() = std::move(l2_arg.expr);
   }
 
-  const irep_idt output_id=get_string_argument(id_arg, ns);
+  const irep_idt output_id = get_string_argument(id_arg.expr, ns);
 
   target.output(state.guard.as_expr(), state.source, output_id, args);
 }
@@ -477,7 +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++)
-      vars.push_back(state.rename_level2(code.arguments()[j], ns));
+      vars.push_back(state.rename_level2(code.arguments()[j], ns).expr);
 
     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.expr, ns);
+  level2t<ssa_exprt> l2_expr = state.rename_level2(ssa.expr, ns);
   state.record_events=record_events;
 
   // we hide the declaration of auxiliary variables
@@ -81,12 +81,17 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
 
   target.decl(
     state.guard.as_expr(),
-    ssa.expr,
+    l2_expr.expr,
     state.source,
     hidden ? symex_targett::assignment_typet::HIDDEN
            : symex_targett::assignment_typet::STATE);
 
-  if(state.dirty(ssa.expr.get_object_name()) && state.atomic_section_id == 0)
+  if(
+    state.dirty(l2_expr.expr.get_object_name()) && state.atomic_section_id == 0)
+    // TODO: make shared write take a level2 exprt
     target.shared_write(
-      state.guard.as_expr(), ssa.expr, state.atomic_section_id, state.source);
+      state.guard.as_expr(),
+      l2_expr.expr,
+      state.atomic_section_id,
+      state.source);
 }

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)
-    a = state.rename_level2(std::move(a), ns);
+    a = state.rename_level2(std::move(a), ns).expr;
 
   // we hide the call if the caller and callee are both hidden
   const bool hidden = state.top().hidden_function && goto_function.is_hidden();