Make set_l1_indices return a renamedt

This carries the information about which renaming the expression has
been through.
This requires a change in symex_level1t::operator() so that it takes
care of the non-empty level 2 case.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -242,17 +242,11 @@ renamedt<ssa_exprt, L0> goto_symex_statet::set_l0_indices(
   return level0(std::move(ssa_expr), ns, source.thread_nr);
 }
 
-void goto_symex_statet::set_l1_indices(
-  ssa_exprt &ssa_expr,
+renamedt<ssa_exprt, L1> goto_symex_statet::set_l1_indices(
+  ssa_exprt ssa_expr,
   const namespacet &ns)
 {
-  if(!ssa_expr.get_level_2().empty())
-    return;
-  if(!ssa_expr.get_level_1().empty())
-    return;
-  renamedt<ssa_exprt, L1> l1 =
-    level1(level0(std::move(ssa_expr), ns, source.thread_nr));
-  ssa_expr = l1.get();
+  return level1(level0(std::move(ssa_expr), ns, source.thread_nr));
 }
 
 void goto_symex_statet::set_l2_indices(
@@ -278,7 +272,10 @@ ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
     ssa = ssa_l0.get();
   }
   else if(level == L1)
-    set_l1_indices(ssa, ns);
+  {
+    const renamedt<ssa_exprt, L1> ssa_l1 = set_l1_indices(std::move(ssa), ns);
+    ssa = ssa_l1.get();
+  }
   else
     UNREACHABLE;
 
@@ -313,7 +310,8 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
     }
     else if(level==L2)
     {
-      set_l1_indices(ssa, ns);
+      const renamedt<ssa_exprt, L1> ssa_l1 = set_l1_indices(std::move(ssa), ns);
+      ssa = ssa_l1.get();
       rename<level>(expr.type(), ssa.get_identifier(), ns);
       ssa.update_type();
 
@@ -564,8 +562,8 @@ void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
     ssa_exprt &ssa=to_ssa_expr(expr);
 
     // only do L1!
-    set_l1_indices(ssa, ns);
-
+    const renamedt<ssa_exprt, L1> ssa_l1 = set_l1_indices(std::move(ssa), ns);
+    ssa = ssa_l1.get();
     rename<level>(expr.type(), ssa.get_identifier(), ns);
     ssa.update_type();
   }

src/goto-symex/goto_symex_state.h

@@ -117,7 +117,7 @@ class goto_symex_statet final : public goto_statet
   renamedt<ssa_exprt, L0> set_l0_indices(ssa_exprt expr, const namespacet &ns);
 
   /// Update level 0 and 1 values.
-  void set_l1_indices(ssa_exprt &expr, const namespacet &ns);
+  renamedt<ssa_exprt, L1> set_l1_indices(ssa_exprt expr, const namespacet &ns);
 
   /// Update level 0, 1 and 2 values.
   void set_l2_indices(ssa_exprt &expr, const namespacet &ns);

src/goto-symex/renaming_level.cpp

@@ -46,8 +46,13 @@ operator()(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr) const
 renamedt<ssa_exprt, L1> symex_level1t::
 operator()(renamedt<ssa_exprt, L0> l0_expr) const
 {
-  if(!l0_expr.get().get_level_1().empty())
+  if(!l0_expr.get().get_level_1().empty() ||
+     !l0_expr.get().get_level_2().empty())
+  {
+    // TODO reaching here means the information that l0_expr was L1 or L2 has
+    // TODO been lost somewhere during execution, which should be avoided
     return renamedt<ssa_exprt, L1>{std::move(l0_expr.value)};
+  }
 
   const irep_idt l0_name = l0_expr.get().get_l1_object_identifier();