Merge pull request #4642 from romainbrenguier/refactor/symex_assign

Refactoring of symex_assign_symbol

Author: tautschnig

src/goto-symex/field_sensitivity.cpp

@@ -222,9 +222,15 @@ void field_sensitivityt::field_assignments_rec(
     exprt ssa_rhs = state.rename(lhs, ns).get();
     simplify(ssa_rhs, ns);
 
-    ssa_exprt ssa_lhs = to_ssa_expr(lhs_fs);
-    state.assignment(
-      ssa_lhs, ssa_rhs, ns, true, true, allow_pointer_unsoundness);
+    const ssa_exprt ssa_lhs = state
+                                .assignment(
+                                  to_ssa_expr(lhs_fs),
+                                  ssa_rhs,
+                                  ns,
+                                  true,
+                                  true,
+                                  allow_pointer_unsoundness)
+                                .get();
 
     // do the assignment
     target.assignment(

src/goto-symex/goto_symex_state.cpp

@@ -38,7 +38,7 @@ goto_symex_statet::goto_symex_statet(
     source(_source),
     guard_manager(manager),
     symex_target(nullptr),
-    record_events(true),
+    record_events({true}),
     fresh_l2_name_provider(fresh_l2_name_provider)
 {
   threads.emplace_back(guard_manager);
@@ -47,7 +47,8 @@ goto_symex_statet::goto_symex_statet(
 
 goto_symex_statet::~goto_symex_statet()=default;
 
-/// write to a variable
+/// Check that \p expr is correctly renamed to level 2 and return true in case
+/// an error is detected.
 static bool check_renaming(const exprt &expr);
 
 static bool check_renaming(const typet &type)
@@ -151,9 +152,9 @@ goto_symex_statet::set_indices<L2>(ssa_exprt ssa_expr, const namespacet &ns)
   return level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
 }
 
-void goto_symex_statet::assignment(
-  ssa_exprt &lhs, // L0/L1
-  const exprt &rhs,  // L2
+renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
+  ssa_exprt lhs,    // L0/L1
+  const exprt &rhs, // L2
   const namespacet &ns,
   bool rhs_is_simplified,
   bool record_value,
@@ -182,7 +183,8 @@ void goto_symex_statet::assignment(
 
   // do the l2 renaming
   increase_generation(l1_identifier, lhs);
-  lhs = set_indices<L2>(std::move(lhs), ns).get();
+  renamedt<ssa_exprt, L2> l2_lhs = set_indices<L2>(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);
@@ -233,6 +235,8 @@ void goto_symex_statet::assignment(
   value_set.output(ns, std::cout);
   std::cout << "**********************\n";
 #endif
+
+  return l2_lhs;
 }
 
 template <levelt level>
@@ -442,21 +446,21 @@ bool goto_symex_statet::l2_thread_read_encoding(
     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;
-    assignment(ssa_l1, tmp, ns, true, true);
-    record_events=record_events_bak;
+    record_events.push(false);
+    ssa_exprt ssa_l2 = assignment(std::move(ssa_l1), tmp, ns, true, true).get();
+    record_events.pop();
 
     symex_target->assignment(
       guard_as_expr,
-      ssa_l1,
-      ssa_l1,
-      ssa_l1.get_original_expr(),
+      ssa_l2,
+      ssa_l2,
+      ssa_l2.get_original_expr(),
       tmp,
       source,
       symex_targett::assignment_typet::PHI);
 
-    expr = set_indices<L2>(std::move(ssa_l1), ns).get();
+    INVARIANT(!check_renaming(ssa_l2), "expr should be renamed to L2");
+    expr = std::move(ssa_l2);
 
     a_s_read.second.push_back(guard);
     if(!no_write.op().is_false())
@@ -466,7 +470,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
   }
 
   // No event and no fresh index, but avoid constant propagation
-  if(!record_events)
+  if(!record_events.top())
   {
     expr = set_indices<L2>(std::move(ssa_l1), ns).get();
     return true;
@@ -488,7 +492,7 @@ goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(
   const ssa_exprt &expr,
   const namespacet &ns) const
 {
-  if(!record_events)
+  if(!record_events.top())
     return write_is_shared_resultt::NOT_SHARED;
 
   PRECONDITION(dirty != nullptr);

src/goto-symex/goto_symex_state.h

@@ -108,13 +108,14 @@ class goto_symex_statet final : public goto_statet
   template <levelt level = L2>
   void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);
 
-  void assignment(
-    ssa_exprt &lhs, // L0/L1
-    const exprt &rhs,  // L2
+  /// \return lhs renamed to level 2
+  renamedt<ssa_exprt, L2> assignment(
+    ssa_exprt lhs,    // L0/L1
+    const exprt &rhs, // L2
     const namespacet &ns,
     bool rhs_is_simplified,
     bool record_value,
-    bool allow_pointer_unsoundness=false);
+    bool allow_pointer_unsoundness = false);
 
   field_sensitivityt field_sensitivity;
 
@@ -197,7 +198,7 @@ class goto_symex_statet final : public goto_statet
   write_is_shared_resultt
   write_is_shared(const ssa_exprt &expr, const namespacet &ns) const;
 
-  bool record_events;
+  std::stack<bool> record_events;
 
   const incremental_dirtyt *dirty = nullptr;
 

src/goto-symex/postcondition.cpp

@@ -130,8 +130,8 @@ void postconditiont::strengthen(exprt &dest)
        SSA_step.ssa_lhs.type().id()==ID_struct)
       return;
 
-    equal_exprt equality(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
-    get_original_name(equality);
+    exprt equality =
+      get_original_name(equal_exprt{SSA_step.ssa_lhs, SSA_step.ssa_rhs});
 
     if(dest.is_true())
       dest.swap(equality);
@@ -169,8 +169,7 @@ bool postconditiont::is_used(
         it!=expr_set.end();
         it++)
     {
-      exprt tmp(*it);
-      get_original_name(tmp);
+      const exprt tmp = get_original_name(*it);
       find_symbols(tmp, symbols);
     }
 

src/goto-symex/precondition.cpp

@@ -140,8 +140,7 @@ void preconditiont::compute_rec(exprt &dest)
   }
   else if(dest==SSA_step.ssa_lhs.get_original_expr())
   {
-    dest=SSA_step.ssa_rhs;
-    get_original_name(dest);
+    dest = get_original_name(SSA_step.ssa_rhs);
   }
   else
     Forall_operands(it, dest)

src/goto-symex/renaming_level.cpp

@@ -97,37 +97,42 @@ void symex_level1t::restore_from(const current_namest &other)
   }
 }
 
-void get_original_name(exprt &expr)
+exprt get_original_name(exprt expr)
 {
-  get_original_name(expr.type());
+  expr.type() = get_original_name(std::move(expr.type()));
 
   if(expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol))
-    expr = to_ssa_expr(expr).get_original_expr();
+    return to_ssa_expr(expr).get_original_expr();
   else
+  {
     Forall_operands(it, expr)
-      get_original_name(*it);
+      *it = get_original_name(std::move(*it));
+    return expr;
+  }
 }
 
-void get_original_name(typet &type)
+typet get_original_name(typet type)
 {
   // rename all the symbols with their last known value
 
   if(type.id() == ID_array)
   {
     auto &array_type = to_array_type(type);
-    get_original_name(array_type.subtype());
-    get_original_name(array_type.size());
+    array_type.subtype() = get_original_name(std::move(array_type.subtype()));
+    array_type.size() = get_original_name(std::move(array_type.size()));
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
   {
     struct_union_typet &s_u_type = to_struct_union_type(type);
     struct_union_typet::componentst &components = s_u_type.components();
 
     for(auto &component : components)
-      get_original_name(component.type());
+      component.type() = get_original_name(std::move(component.type()));
   }
   else if(type.id() == ID_pointer)
   {
-    get_original_name(to_pointer_type(type).subtype());
+    type.subtype() =
+      get_original_name(std::move(to_pointer_type(type).subtype()));
   }
+  return type;
 }

src/goto-symex/renaming_level.h

@@ -148,9 +148,9 @@ struct symex_level2t : public symex_renaming_levelt
 };
 
 /// Undo all levels of renaming
-void get_original_name(exprt &expr);
+exprt get_original_name(exprt expr);
 
 /// Undo all levels of renaming
-void get_original_name(typet &type);
+typet get_original_name(typet type);
 
 #endif // CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H