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).value);
 }
 
 void scratch_programt::append(goto_programt::instructionst &new_instructions)

src/goto-symex/goto_symex_state.cpp

@@ -163,15 +163,16 @@ void goto_symex_statet::assignment(
   bool allow_pointer_unsoundness)
 {
   // identifier should be l0 or l1, make sure it's l1
-  lhs = rename_ssa<L1>(std::move(lhs), ns);
+  renamedt<ssa_exprt, L1> l1_lhs = rename_ssa<L1>(std::move(lhs), ns);
   irep_idt l1_identifier=lhs.get_identifier();
 
   // the type might need renaming
-  rename<L2>(lhs.type(), l1_identifier, ns);
-  lhs.update_type();
+  rename<L2>(l1_lhs.value.type(), l1_identifier, ns);
+  l1_lhs.value.update_type();
   if(run_validation_checks)
   {
-    DATA_INVARIANT(!check_renaming_l1(lhs), "lhs renaming failed on l1");
+    DATA_INVARIANT(
+      !check_renaming_l1(l1_lhs.value), "lhs renaming failed on l1");
   }
 
 #if 0
@@ -184,7 +185,8 @@ void goto_symex_statet::assignment(
 
   // do the l2 renaming
   const auto level2_it =
-    level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0)).first;
+    level2.current_names.emplace(l1_identifier, std::make_pair(l1_lhs.value, 0))
+      .first;
   symex_renaming_levelt::increase_counter(level2_it);
   set_l2_indices(lhs, ns);
 
@@ -264,7 +266,8 @@ void goto_symex_statet::set_l2_indices(
 }
 
 template <levelt level>
-ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
+renamedt<ssa_exprt, level>
+goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
 {
   static_assert(
     level == L0 || level == L1,
@@ -278,15 +281,16 @@ ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
 
   rename<level>(ssa.type(), ssa.get_identifier(), ns);
   ssa.update_type();
-  return ssa;
+  return renamedt<ssa_exprt, level>{ssa};
 }
 
 /// Ensure `rename_ssa` gets compiled for L0
-template ssa_exprt
+template renamedt<ssa_exprt, L0>
 goto_symex_statet::rename_ssa<L0>(ssa_exprt ssa, const namespacet &ns);
 
 template <levelt level>
-exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
+renamedt<exprt, level>
+goto_symex_statet::rename(exprt expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
 
@@ -297,11 +301,11 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
 
     if(level == L0)
     {
-      ssa = rename_ssa<L0>(std::move(ssa), ns);
+      ssa = rename_ssa<L0>(std::move(ssa), ns).value;
     }
     else if(level == L1)
     {
-      ssa = rename_ssa<L1>(std::move(ssa), ns);
+      ssa = rename_ssa<L1>(std::move(ssa), ns).value;
     }
     else if(level==L2)
     {
@@ -336,7 +340,7 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
     if(as_const(expr).type().id() == ID_code)
       rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
     else
-      expr = rename<level>(ssa_exprt{expr}, ns);
+      expr = rename<level>(ssa_exprt{expr}, ns).value;
   }
   else if(expr.id()==ID_address_of)
   {
@@ -351,7 +355,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).value;
 
     const exprt &c_expr = as_const(expr);
     INVARIANT(
@@ -363,7 +367,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 renamedt<exprt, level>{expr};
 }
 
 /// thread encoding
@@ -573,13 +577,14 @@ 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
-      index_expr.index() = rename<level>(std::move(index_expr.index()), ns);
+      index_expr.index() =
+        rename<level>(std::move(index_expr.index()), ns).value;
     }
     else if(expr.id()==ID_if)
     {
       // the condition is not an address
       if_exprt &if_expr=to_if_expr(expr);
-      if_expr.cond() = rename<level>(std::move(if_expr.cond()), ns);
+      if_expr.cond() = rename<level>(std::move(if_expr.cond()), ns).value;
       rename_address<level>(if_expr.true_case(), ns);
       rename_address<level>(if_expr.false_case(), ns);
 
@@ -718,7 +723,7 @@ void goto_symex_statet::rename(
   {
     auto &array_type = to_array_type(type);
     rename<level>(array_type.subtype(), irep_idt(), ns);
-    array_type.size() = rename<level>(std::move(array_type.size()), ns);
+    array_type.size() = rename<level>(std::move(array_type.size()), ns).value;
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
   {
@@ -731,7 +736,8 @@ void goto_symex_statet::rename(
       if(component.type().id() == ID_array)
       {
         auto &array_type = to_array_type(component.type());
-        array_type.size() = rename<level>(std::move(array_type.size()), ns);
+        array_type.size() =
+          rename<level>(std::move(array_type.size()), ns).value;
       }
       else if(component.type().id() != ID_pointer)
         rename<level>(component.type(), irep_idt(), ns);

src/goto-symex/goto_symex_state.h

@@ -177,12 +177,12 @@ 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>
-  exprt rename(exprt expr, const namespacet &ns);
+  renamedt<exprt, level> rename(exprt expr, const namespacet &ns);
 
   /// Version of rename which is specialized for SSA exprt.
   /// Implementation only exists for level L0 and L1.
   template <levelt level>
-  ssa_exprt rename_ssa(ssa_exprt ssa, const namespacet &ns);
+  renamedt<ssa_exprt, level> rename_ssa(ssa_exprt ssa, const namespacet &ns);
 
   template <levelt level = L2>
   void rename(typet &type, const irep_idt &l1_identifier, 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);
   }
 
-  exprt l2_rhs = state.rename(std::move(ssa_rhs), ns);
-  do_simplify(l2_rhs);
+  renamedt<exprt, L2> l2_rhs = state.rename(std::move(ssa_rhs), ns);
+  do_simplify(l2_rhs.value);
 
   ssa_exprt ssa_lhs=lhs;
   state.assignment(
     ssa_lhs,
-    l2_rhs,
+    l2_rhs.value,
     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(std::move(ssa_full_lhs), ns);
+  renamedt<exprt, L2> l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns);
   state.record_events=record_events;
 
   guardt tmp_guard(state.guard);
@@ -254,9 +254,9 @@ void goto_symext::symex_assign_symbol(
   target.assignment(
     tmp_guard.as_expr(),
     ssa_lhs,
-    l2_full_lhs,
+    l2_full_lhs.value,
     add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
-    l2_rhs,
+    l2_rhs.value,
     state.source,
     assignment_type);
 }
@@ -407,20 +407,20 @@ void goto_symext::symex_assign_if(
 
   guardt old_guard=guard;
 
-  exprt renamed_guard = state.rename(lhs.cond(), ns);
-  do_simplify(renamed_guard);
+  renamedt<exprt, L2> renamed_guard = state.rename(lhs.cond(), ns);
+  do_simplify(renamed_guard.value);
 
-  if(!renamed_guard.is_false())
+  if(!renamed_guard.value.is_false())
   {
-    guard.add(renamed_guard);
+    guard.add(renamed_guard.value);
     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.value.is_true())
   {
-    guard.add(not_exprt(renamed_guard));
+    guard.add(not_exprt(renamed_guard.value));
     symex_assign_rec(
       state, lhs.false_case(), full_lhs, rhs, guard, assignment_type);
     guard = std::move(old_guard);