Make symex_level2t::operator() return a renamedt

This makes it in the type the result has been renamed and a level 1
expression is expected as argument.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -261,9 +261,9 @@ void goto_symex_statet::set_l2_indices(
 {
   if(!ssa_expr.get_level_2().empty())
     return;
-  renamedt<ssa_exprt, L1> l1 =
-    level1(level0(std::move(ssa_expr), ns, source.thread_nr);
-  ssa_expr = level2(l1.get());
+  renamedt<ssa_exprt, L2> l2 =
+    level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
+  ssa_expr = l2.get();
 }
 
 template <levelt level>
@@ -287,6 +287,8 @@ ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
 /// Ensure `rename_ssa` gets compiled for L0
 template ssa_exprt
 goto_symex_statet::rename_ssa<L0>(ssa_exprt ssa, const namespacet &ns);
+template ssa_exprt
+goto_symex_statet::rename_ssa<L1>(ssa_exprt ssa, const namespacet &ns);
 
 template <levelt level>
 exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
@@ -369,6 +371,8 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
   return expr;
 }
 
+template exprt goto_symex_statet::rename<L1>(exprt expr, const namespacet &ns);
+
 /// thread encoding
 bool goto_symex_statet::l2_thread_read_encoding(
   ssa_exprt &expr,

src/goto-symex/renaming_level.cpp

@@ -60,10 +60,11 @@ operator()(renamedt<ssa_exprt, L0> l0_expr) const
   return renamedt<ssa_exprt, L1>{std::move(l0_expr.value)};
 }
 
-ssa_exprt symex_level2t::operator()(ssa_exprt ssa_expr) const
+renamedt<ssa_exprt, L2> symex_level2t::
+operator()(renamedt<ssa_exprt, L1> l1_expr) const
 {
-  ssa_expr.set_level_2(current_count(ssa_expr.get_identifier()));
-  return ssa_expr;
+  l1_expr.value.set_level_2(current_count(l1_expr.get().get_identifier()));
+  return renamedt<ssa_exprt, L2>{std::move(l1_expr.value)};
 }
 
 void symex_level1t::restore_from(

src/goto-symex/renaming_level.h

@@ -121,7 +121,7 @@ struct symex_level1t : public symex_renaming_levelt
 /// This is to ensure each variable is only assigned once.
 struct symex_level2t : public symex_renaming_levelt
 {
-  ssa_exprt operator()(ssa_exprt ssa_expr) const;
+  renamedt<ssa_exprt, L2> operator()(renamedt<ssa_exprt, L1> l1_expr) const;
 
   symex_level2t() = default;
   ~symex_level2t() override = default;