Make the result of rename be a renamedt

This makes explicit the fact that the expression has been renamed.

Author: romainbrenguier

src/goto-instrument/accelerate/scratch_program.cpp

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

src/goto-symex/goto_symex_state.cpp

@@ -262,13 +262,13 @@ void goto_symex_statet::set_l2_indices(
   ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
 }
 
-ssa_exprt
+renamedt<ssa_exprt, L0>
 goto_symex_statet::rename_level0_ssa(ssa_exprt ssa, const namespacet &ns)
 {
   set_l0_indices(ssa, ns);
   rename<L0>(ssa.type(), ssa.get_identifier(), ns);
   ssa.update_type();
-  return ssa;
+  return renamedt<ssa_exprt, L0>{ssa};
 }
 
 ssa_exprt
@@ -281,7 +281,8 @@ goto_symex_statet::rename_level1_ssa(ssa_exprt ssa, const namespacet &ns)
 }
 
 template <levelt level>
-exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
+template <levelt level>
+renamedt<exprt, level> goto_symex_statet::rename(exprt expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
 
@@ -346,7 +347,7 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
 
     // do this recursively
     Forall_operands(it, expr)
-      *it = rename<level>(std::move(*it), ns);
+      *it = rename<level>(std::move(*it), ns).expr;
 
     const exprt &c_expr = as_const(expr);
     INVARIANT(
@@ -358,7 +359,7 @@ exprt 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;
+  return level2t<exprt>{expr};
 }
 
 /// thread encoding

src/goto-symex/goto_symex_state.h

@@ -176,10 +176,11 @@ 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>
-  exprt rename(exprt expr, const namespacet &ns);
+  template <levelt level>
+  renamedt<exprt, level> rename(exprt expr, const namespacet &ns);
 
-  ssa_exprt rename_level0_ssa(ssa_exprt ssa, const namespacet &ns);
+  renamedt<ssa_exprt, L0> rename_level0_ssa(
+    ssa_exprt ssa, const namespacet &ns);
 
   ssa_exprt rename_level1_ssa(ssa_exprt ssa, const namespacet &ns);
 

src/goto-symex/renaming_level.h

@@ -76,6 +76,16 @@ struct symex_level0t : public symex_renaming_levelt
   ~symex_level0t() override = default;
 };
 
+/// 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;
+};
+
 /// Functor to set the level 1 renaming of SSA expressions.
 /// Level 1 corresponds to function frames.
 /// This is to preserve locality in case of recursion

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<L2>(std::move(ssa_rhs), ns);
-  do_simplify(l2_rhs);
+  level2t<exprt> l2_rhs = state.rename<L2>(std::move(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,
@@ -254,9 +254,9 @@ void goto_symext::symex_assign_symbol(
   target.assignment(
     tmp_guard.as_expr(),
     ssa_lhs,
-    l2_full_lhs,
+    l2_full_lhs.expr,
     add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
-    l2_rhs,
+    l2_rhs.expr,
     state.source,
     assignment_type);
 }
@@ -407,20 +407,20 @@ void goto_symext::symex_assign_if(
 
   guardt old_guard=guard;
 
-  exprt renamed_guard = state.rename<L2>(lhs.cond(), ns);
-  do_simplify(renamed_guard);
+  level2t<exprt> renamed_guard = state.rename<L2>(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

@@ -76,13 +76,13 @@ void goto_symext::symex_allocate(
 
     // 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)
         {
@@ -99,7 +99,7 @@ void goto_symext::symex_allocate(
             PRECONDITION(*c_sizeof_type_rec(tmp_size.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;
@@ -164,12 +164,12 @@ void goto_symext::symex_allocate(
 
   // to allow constant propagation
   exprt zero_init = state.rename<L2>(code.op1(), ns);
-  simplify(zero_init, ns);
+  simplify(zero_init.expr, ns);
 
   INVARIANT(
     zero_init.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);
@@ -312,7 +312,7 @@ void goto_symext::symex_printf(
   exprt tmp_rhs = state.rename<L2>(rhs, ns);
   do_simplify(tmp_rhs);
 
-  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++)
@@ -367,7 +367,7 @@ void goto_symext::symex_output(
     args.back() = std::move(l2_arg);
   }
 
-  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);
 }

src/goto-symex/symex_decl.cpp

@@ -85,7 +85,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
 
   target.decl(
     state.guard.as_expr(),
-    ssa,
+    l2_expr.expr,
     state.source,
     hidden?
       symex_targett::assignment_typet::HIDDEN:
@@ -94,7 +94,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   if(state.dirty(ssa.get_object_name()) && state.atomic_section_id == 0)
     target.shared_write(
       state.guard.as_expr(),
-      ssa,
+      l2_expr.expr,
       state.atomic_section_id,
       state.source);
 }

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)
-    a = state.rename<L2>(std::move(a), ns);
+    a = state.rename<L2>(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();
@@ -395,40 +395,40 @@ static void locality(
       it++)
   {
     // get L0 name
-    ssa_exprt ssa =
-      state.rename_level0_ssa(ssa_exprt(ns.lookup(*it).symbol_expr()), ns);
-    const irep_idt l0_name=ssa.get_identifier();
+    renamedt<ssa_exprt, L0> l0_ssa =
+      state.rename_level0(ns.lookup(*it).symbol_expr(), ns);
+    const irep_idt l0_name = l0_ssa.expr.get_identifier();
 
     // save old L1 name for popping the frame
     auto c_it = state.level1.current_names.find(l0_name);
 
     if(c_it != state.level1.current_names.end())
     {
       frame.old_level1.emplace(l0_name, c_it->second);
-      c_it->second = std::make_pair(ssa, frame_nr);
+      c_it->second = std::make_pair(l0_ssa.expr, frame_nr);
     }
     else
     {
       c_it = state.level1.current_names
-               .emplace(l0_name, std::make_pair(ssa, frame_nr))
+               .emplace(l0_name, std::make_pair(l0_ssa.expr, frame_nr))
                .first;
     }
 
     // do L1 renaming -- these need not be unique, as
     // identifiers may be shared among functions
     // (e.g., due to inlining or other code restructuring)
 
-    ssa_exprt ssa_l1 = state.rename_level1_ssa(std::move(ssa), ns);
+    ssa_exprt ssa_l1 = state.rename_level1_ssa(std::move(ssa.expr), ns);
 
-    irep_idt l1_name = ssa_l1.get_identifier();
+    irep_idt l1_name = ssa_l1.expr.get_identifier();
     unsigned offset=0;
 
     while(state.l1_history.find(l1_name)!=state.l1_history.end())
     {
       symex_renaming_levelt::increase_counter(c_it);
       ++offset;
-      ssa_l1.set_level_1(frame_nr + offset);
-      l1_name = ssa_l1.get_identifier();
+      ssa_l1.expr.set_level_1(frame_nr + offset);
+      l1_name = ssa_l1.expr.get_identifier();
     }
 
     // now unique -- store