Merge pull request #3986 from romainbrenguier/refactor/symex-rename

Make return type of set_l*_indices be a renamedt [blocks: #4333]

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -188,7 +188,7 @@ 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);
-  set_l2_indices(lhs, ns);
+  lhs = set_l2_indices(std::move(lhs), ns).get();
 
   // in case we happen to be multi-threaded, record the memory access
   bool is_shared=l2_thread_write_encoding(lhs, ns);
@@ -235,37 +235,22 @@ void goto_symex_statet::assignment(
   #endif
 }
 
-void goto_symex_statet::set_l0_indices(
-  ssa_exprt &ssa_expr,
-  const namespacet &ns)
+renamedt<ssa_exprt, L0>
+goto_symex_statet::set_l0_indices(ssa_exprt ssa_expr, const namespacet &ns)
 {
-  renamedt<ssa_exprt, L0> renamed =
-    level0(std::move(ssa_expr), ns, source.thread_nr);
-  ssa_expr = renamed.get();
+  return level0(std::move(ssa_expr), ns, source.thread_nr);
 }
 
-void goto_symex_statet::set_l1_indices(
-  ssa_exprt &ssa_expr,
-  const namespacet &ns)
+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(
-  ssa_exprt &ssa_expr,
-  const namespacet &ns)
+renamedt<ssa_exprt, L2>
+goto_symex_statet::set_l2_indices(ssa_exprt ssa_expr, const namespacet &ns)
 {
-  if(!ssa_expr.get_level_2().empty())
-    return;
-  renamedt<ssa_exprt, L2> l2 =
-    level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
-  ssa_expr = l2.get();
+  return level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
 }
 
 template <levelt level>
@@ -275,9 +260,9 @@ ssa_exprt goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns)
     level == L0 || level == L1,
     "rename_ssa can only be used for levels L0 and L1");
   if(level == L0)
-    set_l0_indices(ssa, ns);
+    ssa = set_l0_indices(std::move(ssa), ns).get();
   else if(level == L1)
-    set_l1_indices(ssa, ns);
+    ssa = set_l1_indices(std::move(ssa), ns).get();
   else
     UNREACHABLE;
 
@@ -312,7 +297,7 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
     }
     else if(level==L2)
     {
-      set_l1_indices(ssa, ns);
+      ssa = set_l1_indices(std::move(ssa), ns).get();
       rename<level>(expr.type(), ssa.get_identifier(), ns);
       ssa.update_type();
 
@@ -333,7 +318,7 @@ exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
         if(p_it != propagation.end())
           expr=p_it->second; // already L2
         else
-          set_l2_indices(ssa, ns);
+          ssa = set_l2_indices(std::move(ssa), ns).get();
       }
     }
   }
@@ -447,8 +432,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);
-    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())
     {
@@ -458,14 +442,13 @@ 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);
-
+    exprt tmp;
     if(cond.is_false())
-    {
-      exprt t=tmp.false_case();
-      t.swap(tmp);
-    }
+      tmp = l2_false_case.get();
+    else
+      tmp = if_exprt{cond.as_expr(), l2_true_case.get(), l2_false_case.get()};
 
     const bool record_events_bak=record_events;
     record_events=false;
@@ -481,8 +464,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
       source,
       symex_targett::assignment_typet::PHI);
 
-    set_l2_indices(ssa_l1, ns);
-    expr=ssa_l1;
+    expr = set_l2_indices(std::move(ssa_l1), ns).get();
 
     a_s_read.second.push_back(guard);
     if(!no_write.op().is_false())
@@ -498,15 +480,13 @@ bool goto_symex_statet::l2_thread_read_encoding(
   // No event and no fresh index, but avoid constant propagation
   if(!record_events)
   {
-    set_l2_indices(ssa_l1, ns);
-    expr=ssa_l1;
+    expr = set_l2_indices(std::move(ssa_l1), ns).get();
     return true;
   }
 
   // produce a fresh L2 name
   symex_renaming_levelt::increase_counter(level2_it);
-  set_l2_indices(ssa_l1, ns);
-  expr=ssa_l1;
+  expr = set_l2_indices(std::move(ssa_l1), ns).get();
 
   // and record that
   INVARIANT_STRUCTURED(
@@ -563,7 +543,7 @@ 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);
+    ssa = set_l1_indices(std::move(ssa), ns).get();
 
     rename<level>(expr.type(), ssa.get_identifier(), ns);
     ssa.update_type();

src/goto-symex/goto_symex_state.h

@@ -114,13 +114,13 @@ class goto_symex_statet final : public goto_statet
   void rename_address(exprt &expr, const namespacet &ns);
 
   /// Update level 0 values.
-  void set_l0_indices(ssa_exprt &expr, const namespacet &ns);
+  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);
+  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;

src/goto-symex/renaming_level.cpp

@@ -46,8 +46,12 @@ 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())
+  {
     return renamedt<ssa_exprt, L1>{std::move(l0_expr.value)};
+  }
 
   const irep_idt l0_name = l0_expr.get().get_l1_object_identifier();
 
@@ -63,6 +67,8 @@ operator()(renamedt<ssa_exprt, L0> l0_expr) const
 renamedt<ssa_exprt, L2> symex_level2t::
 operator()(renamedt<ssa_exprt, L1> l1_expr) const
 {
+  if(!l1_expr.get().get_level_2().empty())
+    return renamedt<ssa_exprt, L2>{std::move(l1_expr.value)};
   l1_expr.value.set_level_2(current_count(l1_expr.get().get_identifier()));
   return renamedt<ssa_exprt, L2>{std::move(l1_expr.value)};
 }