Make symex_level1t::operator() return a renamedt

This makes it explicit in the type that the expression has been renamed.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -252,7 +252,8 @@ void goto_symex_statet::set_l1_indices(
     return;
   renamedt<ssa_exprt, L0> l0 =
     level0(std::move(ssa_expr), ns, source.thread_nr);
-  ssa_expr = level1(l0.get());
+  renamedt<ssa_exprt, L1> l1 = level1(std::move(l0));
+  ssa_expr = l1.get();
 }
 
 void goto_symex_statet::set_l2_indices(
@@ -263,8 +264,8 @@ void goto_symex_statet::set_l2_indices(
     return;
   renamedt<ssa_exprt, L0> l0 =
     level0(std::move(ssa_expr), ns, source.thread_nr);
-  ssa_exprt l1 = level1(l0.get());
-  ssa_expr = level2(std::move(l1));
+  renamedt<ssa_exprt, L1> l1 = level1(std::move(l0));
+  ssa_expr = level2(l1.get());
 }
 
 template <levelt level>

src/goto-symex/renaming_level.cpp

@@ -43,21 +43,21 @@ operator()(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr) const
   return renamedt<ssa_exprt, L0>{ssa_expr};
 }
 
-ssa_exprt symex_level1t::operator()(ssa_exprt ssa_expr) const
+renamedt<ssa_exprt, L1> symex_level1t::
+operator()(renamedt<ssa_exprt, L0> l0_expr) const
 {
-  // already renamed?
-  if(!ssa_expr.get_level_1().empty())
-    return std::move(ssa_expr);
+  if(!l0_expr.get().get_level_1().empty())
+    return renamedt<ssa_exprt, L1>{std::move(l0_expr.value)};
 
-  const irep_idt l0_name = ssa_expr.get_l1_object_identifier();
+  const irep_idt l0_name = l0_expr.get().get_l1_object_identifier();
 
   const auto it = current_names.find(l0_name);
   if(it == current_names.end())
-    return std::move(ssa_expr);
+    return renamedt<ssa_exprt, L1>{std::move(l0_expr.value)};
 
   // rename!
-  ssa_expr.set_level_1(it->second.second);
-  return ssa_expr;
+  l0_expr.value.set_level_1(it->second.second);
+  return renamedt<ssa_exprt, L1>{std::move(l0_expr.value)};
 }
 
 ssa_exprt symex_level2t::operator()(ssa_exprt ssa_expr) const

src/goto-symex/renaming_level.h

@@ -107,7 +107,7 @@ struct symex_level0t : public symex_renaming_levelt
 /// This is to preserve locality in case of recursion
 struct symex_level1t : public symex_renaming_levelt
 {
-  ssa_exprt operator()(ssa_exprt ssa_expr) const;
+  renamedt<ssa_exprt, L1> operator()(renamedt<ssa_exprt, L0> l0_expr) const;
 
   /// Insert the content of \p other into this renaming
   void restore_from(const current_namest &other);