Make set_l2_indices return a renamedt

This captures the information of which renaming the expression has been
through.

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -188,19 +188,22 @@ void goto_symex_statet::assignment(
   const auto level2_it =
     level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0)).first;
   symex_renaming_levelt::increase_counter(level2_it);
-  lhs = set_l2_indices(lhs, ns);
+  const renamedt<ssa_exprt, L2> l2_lhs = set_l2_indices(std::move(lhs), ns);
+  lhs = l2_lhs.get();
 
   // in case we happen to be multi-threaded, record the memory access
-  bool is_shared=l2_thread_write_encoding(lhs, ns);
+  bool is_shared = l2_thread_write_encoding(l2_lhs.get(), ns);
 
   if(run_validation_checks)
   {
-    DATA_INVARIANT(!check_renaming(lhs), "lhs renaming failed on l2");
+    DATA_INVARIANT(!check_renaming(l2_lhs.get()), "lhs renaming failed on l2");
     DATA_INVARIANT(!check_renaming(rhs), "rhs renaming failed on l2");
   }
 
   // see #305 on GitHub for a simple example and possible discussion
-  if(is_shared && lhs.type().id() == ID_pointer && !allow_pointer_unsoundness)
+  if(
+    is_shared && l2_lhs.get().type().id() == ID_pointer &&
+    !allow_pointer_unsoundness)
     throw unsupported_operation_exceptiont(
       "pointer handling for concurrency is unsound");
 
@@ -216,7 +219,7 @@ void goto_symex_statet::assignment(
     exprt l1_rhs(rhs);
     get_l1_name(l1_rhs);
 
-    ssa_exprt l1_lhs(lhs);
+    ssa_exprt l1_lhs{l2_lhs.get()};
     l1_lhs.remove_level_2();
 
     if(run_validation_checks)
@@ -247,12 +250,10 @@ goto_symex_statet::set_l1_indices(ssa_exprt ssa_expr, const namespacet &ns)
   return level1(level0(std::move(ssa_expr), ns, source.thread_nr));
 }
 
-ssa_exprt
+renamedt<ssa_exprt, L2>
 goto_symex_statet::set_l2_indices(ssa_exprt ssa_expr, const namespacet &ns)
 {
-  renamedt<ssa_exprt, L2> l2 =
-    level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
-  return l2.get();
+  return level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
 }
 
 template <levelt level>
@@ -327,7 +328,11 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
         if(p_it != propagation.end())
           expr=p_it->second; // already L2
         else
-          ssa = set_l2_indices(ssa, ns);
+        {
+          const renamedt<ssa_exprt, L2> l2_ssa =
+            set_l2_indices(std::move(ssa), ns);
+          ssa = l2_ssa.get();
+        }
       }
     }
   }
@@ -441,8 +446,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
     if(!no_write.op().is_false())
       cond |= guardt{no_write.op()};
 
-    if_exprt tmp(cond.as_expr(), ssa_l1, ssa_l1);
-    tmp.true_case() = set_l2_indices(to_ssa_expr(tmp.true_case()), ns);
+    const renamedt<ssa_exprt, L2> l2_true_case = set_l2_indices(ssa_l1, ns);
 
     if(a_s_read.second.empty())
     {
@@ -452,8 +456,9 @@ bool goto_symex_statet::l2_thread_read_encoding(
       symex_renaming_levelt::increase_counter(level2_it);
       a_s_read.first=level2.current_count(l1_identifier);
     }
+    const renamedt<ssa_exprt, L2> l2_false_case = set_l2_indices(ssa_l1, ns);
 
-    to_ssa_expr(tmp.false_case()).set_level_2(a_s_read.first);
+    if_exprt tmp{cond.as_expr(), l2_true_case.get(), l2_false_case.get()};
 
     if(cond.is_false())
     {
@@ -475,7 +480,9 @@ bool goto_symex_statet::l2_thread_read_encoding(
       source,
       symex_targett::assignment_typet::PHI);
 
-    expr = set_l2_indices(ssa_l1, ns);
+    const renamedt<ssa_exprt, L2> ssa_l2 =
+      set_l2_indices(std::move(ssa_l1), ns);
+    expr = ssa_l2.get();
 
     a_s_read.second.push_back(guard);
     if(!no_write.op().is_false())
@@ -491,13 +498,16 @@ bool goto_symex_statet::l2_thread_read_encoding(
   // No event and no fresh index, but avoid constant propagation
   if(!record_events)
   {
-    expr = set_l2_indices(ssa_l1, ns);
+    const renamedt<ssa_exprt, L2> ssa_l2 =
+      set_l2_indices(std::move(ssa_l1), ns);
+    expr = ssa_l2.get();
     return true;
   }
 
   // produce a fresh L2 name
   symex_renaming_levelt::increase_counter(level2_it);
-  expr = set_l2_indices(ssa_l1, ns);
+  const renamedt<ssa_exprt, L2> ssa_l2 = set_l2_indices(std::move(ssa_l1), ns);
+  expr = ssa_l2.get();
 
   // and record that
   INVARIANT_STRUCTURED(

src/goto-symex/goto_symex_state.h

@@ -120,7 +120,7 @@ class goto_symex_statet final : public goto_statet
   renamedt<ssa_exprt, L1> set_l1_indices(ssa_exprt expr, const namespacet &ns);
 
   /// Update level 0, 1 and 2 values.
-  ssa_exprt set_l2_indices(ssa_exprt expr, const namespacet &ns);
+  renamedt<ssa_exprt, L2> set_l2_indices(ssa_exprt expr, const namespacet &ns);
 
   // this maps L1 names to (L2) types
   typedef std::unordered_map<irep_idt, typet> l1_typest;