Merge pull request #4793 from romainbrenguier/clean-up/symex-assign-symbol

Clean_up related to symex_assign_symbol

Author: romainbrenguier

src/goto-symex/goto_state.cpp

@@ -31,19 +31,17 @@ std::size_t goto_statet::increase_generation(
   const ssa_exprt &lhs,
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
 {
-  std::size_t n = fresh_l2_name_provider(l1_identifier);
+  const std::size_t n = fresh_l2_name_provider(l1_identifier);
 
-  const auto r_opt = level2.current_names.find(l1_identifier);
-
-  if(!r_opt)
+  if(const auto r_opt = level2.current_names.find(l1_identifier))
   {
-    level2.current_names.insert(l1_identifier, std::make_pair(lhs, n));
+    std::pair<ssa_exprt, std::size_t> copy = r_opt->get();
+    copy.second = n;
+    level2.current_names.replace(l1_identifier, std::move(copy));
   }
   else
   {
-    std::pair<ssa_exprt, unsigned> copy = r_opt->get();
-    copy.second = n;
-    level2.current_names.replace(l1_identifier, std::move(copy));
+    level2.current_names.insert(l1_identifier, std::make_pair(lhs, n));
   }
 
   return n;

src/goto-symex/goto_symex_state.cpp

@@ -514,6 +514,7 @@ goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(
 }
 
 /// thread encoding
+/// \return true if \p expr is shared between threads
 bool goto_symex_statet::l2_thread_write_encoding(
   const ssa_exprt &expr,
   const namespacet &ns)

src/goto-symex/goto_symex_state.h

@@ -217,7 +217,7 @@ class goto_symex_statet final : public goto_statet
   unsigned remaining_vccs = 0;
 
   /// Allocates a fresh L2 name for the given L1 identifier, and makes it the
-  //  latest generation on this path.
+  /// latest generation on this path.
   std::size_t
   increase_generation(const irep_idt l1_identifier, const ssa_exprt &lhs)
   {

src/goto-symex/renamed.h

@@ -50,7 +50,7 @@ class renamedt : private underlyingt
   };
 
   friend renamedt<ssa_exprt, L0>
-  symex_level0(ssa_exprt, const namespacet &, unsigned);
+  symex_level0(ssa_exprt, const namespacet &, std::size_t);
   friend struct symex_level1t;
   friend struct symex_level2t;
   friend class goto_symex_statet;

src/goto-symex/renaming_level.cpp

@@ -31,7 +31,7 @@ void get_variables(
 }
 
 renamedt<ssa_exprt, L0>
-symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr)
+symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)
 {
   // already renamed?
   if(!ssa_expr.get_level_0().empty())
@@ -56,21 +56,23 @@ symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr)
   return renamedt<ssa_exprt, L0>{ssa_expr};
 }
 
-void symex_level1t::insert(const renamedt<ssa_exprt, L0> &ssa, unsigned index)
+void symex_level1t::insert(
+  const renamedt<ssa_exprt, L0> &ssa,
+  std::size_t index)
 {
   current_names.insert(
     ssa.get().get_identifier(), std::make_pair(ssa.get(), index));
 }
 
-optionalt<std::pair<ssa_exprt, unsigned>> symex_level1t::insert_or_replace(
+optionalt<std::pair<ssa_exprt, std::size_t>> symex_level1t::insert_or_replace(
   const renamedt<ssa_exprt, L0> &ssa,
-  unsigned index)
+  std::size_t index)
 {
   const irep_idt &identifier = ssa.get().get_identifier();
   const auto old_value = current_names.find(identifier);
   if(old_value)
   {
-    std::pair<ssa_exprt, unsigned> result = *old_value;
+    std::pair<ssa_exprt, std::size_t> result = *old_value;
     current_names.replace(identifier, std::make_pair(ssa.get(), index));
     return result;
   }

src/goto-symex/renaming_level.h

@@ -29,7 +29,7 @@ Author: Romain Brenguier, [email protected]
 /// This is extended by the different symex_level structures which are used
 /// during symex to ensure static single assignment (SSA) form.
 using symex_renaming_levelt =
-  sharing_mapt<irep_idt, std::pair<ssa_exprt, unsigned>>;
+  sharing_mapt<irep_idt, std::pair<ssa_exprt, std::size_t>>;
 
 /// Add the \c ssa_exprt of current_names to vars
 DEPRECATED(SINCE(2019, 6, 5, "Unused"))
@@ -44,21 +44,21 @@ void get_variables(
 /// a guard, a shared variable or a function. \p ns is queried to decide
 /// whether we are in one of these cases.
 renamedt<ssa_exprt, L0>
-symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr);
+symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr);
 
 /// Functor to set the level 1 renaming of SSA expressions.
 /// Level 1 corresponds to function frames.
 /// This is to preserve locality in case of recursion
 struct symex_level1t
 {
   /// Assume \p ssa is not already known
-  void insert(const renamedt<ssa_exprt, L0> &ssa, unsigned index);
+  void insert(const renamedt<ssa_exprt, L0> &ssa, std::size_t index);
 
   /// Set the index for \p ssa to index.
   /// \return if an index for \p ssa was already know, returns it's previous
   ///   value.
-  optionalt<std::pair<ssa_exprt, unsigned>>
-  insert_or_replace(const renamedt<ssa_exprt, L0> &ssa, unsigned index);
+  optionalt<std::pair<ssa_exprt, std::size_t>>
+  insert_or_replace(const renamedt<ssa_exprt, L0> &ssa, std::size_t index);
 
   /// \return true if \p ssa has an associated index
   bool has(const renamedt<ssa_exprt, L0> &ssa) const;

src/goto-symex/ssa_step.cpp

@@ -221,9 +221,7 @@ SSA_assignment_stept::SSA_assignment_stept(
   exprt _ssa_full_lhs,
   exprt _original_full_lhs,
   exprt _ssa_rhs,
-  exprt _cond_expr,
-  symex_targett::assignment_typet _assignment_type,
-  bool _hidden)
+  symex_targett::assignment_typet _assignment_type)
   : SSA_stept(source, goto_trace_stept::typet::ASSIGNMENT)
 {
   guard = std::move(_guard);
@@ -232,6 +230,8 @@ SSA_assignment_stept::SSA_assignment_stept(
   original_full_lhs = std::move(_original_full_lhs);
   ssa_rhs = std::move(_ssa_rhs);
   assignment_type = _assignment_type;
-  cond_expr = std::move(_cond_expr);
-  hidden = _hidden;
+  cond_expr = equal_exprt{ssa_lhs, ssa_rhs};
+  hidden = assignment_type != symex_targett::assignment_typet::STATE &&
+           assignment_type !=
+             symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER;
 }

src/goto-symex/ssa_step.h

@@ -205,9 +205,7 @@ class SSA_assignment_stept : public SSA_stept
     exprt ssa_full_lhs,
     exprt original_full_lhs,
     exprt ssa_rhs,
-    exprt cond_expr,
-    symex_targett::assignment_typet assignment_type,
-    bool hidden);
+    symex_targett::assignment_typet assignment_type);
 };
 
 #endif // CPROVER_GOTO_SYMEX_SSA_STEP_H

src/goto-symex/symex_assign.cpp

@@ -395,8 +395,7 @@ void goto_symext::symex_assign_from_struct(
   const exprt::operandst &guard,
   assignment_typet assignment_type)
 {
-  const struct_typet &type = to_struct_type(ns.follow(lhs.type()));
-  const struct_union_typet::componentst &components = type.components();
+  const auto &components = to_struct_type(ns.follow(lhs.type())).components();
   PRECONDITION(rhs.operands().size() == components.size());
 
   for(std::size_t i = 0; i < components.size(); ++i)
@@ -435,16 +434,15 @@ void goto_symext::symex_assign_symbol(
     return;
   }
 
-  exprt l2_rhs = [&]() {
-    exprt guarded_rhs = rhs;
-    // put assignment guard into the rhs
-    if(!guard.empty())
-    {
-      guarded_rhs =
-        if_exprt{conjunction(guard), std::move(guarded_rhs), lhs, rhs.type()};
-    }
-    return state.rename(std::move(guarded_rhs), ns).get();
-  }();
+  exprt l2_rhs =
+    state
+      .rename(
+        // put assignment guard into the rhs
+        guard.empty()
+          ? rhs
+          : static_cast<exprt>(if_exprt{conjunction(guard), rhs, lhs}),
+        ns)
+      .get();
 
   // Note the following two calls are specifically required for
   // field-sensitivity. For example, with-expressions, which may have just been
@@ -457,7 +455,6 @@ void goto_symext::symex_assign_symbol(
 
   do_simplify(assignment.rhs);
 
-  const ssa_exprt &l1_lhs = assignment.lhs;
   const ssa_exprt l2_lhs = state
                              .assignment(
                                assignment.lhs,
@@ -468,15 +465,12 @@ void goto_symext::symex_assign_symbol(
                                symex_config.allow_pointer_unsoundness)
                              .get();
 
-  exprt ssa_full_lhs = add_to_lhs(full_lhs, l2_lhs);
   state.record_events.push(false);
-  const exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns).get();
+  const exprt l2_full_lhs =
+    state.rename(add_to_lhs(full_lhs, l2_lhs), ns).get();
   state.record_events.pop();
 
-  // do the assignment
-  const symbolt &symbol = ns.lookup(l2_lhs.get_object_name());
-
-  if(symbol.is_auxiliary)
+  if(ns.lookup(l2_lhs.get_object_name()).is_auxiliary)
     assignment_type=symex_targett::assignment_typet::HIDDEN;
 
   log.conditional_output(
@@ -486,19 +480,16 @@ void goto_symext::symex_assign_symbol(
               << messaget::eom;
     });
 
-  const exprt assignment_guard =
-    make_and(state.guard.as_expr(), conjunction(guard));
-
-  const exprt original_lhs = get_original_name(l2_full_lhs);
   target.assignment(
-    assignment_guard,
+    make_and(state.guard.as_expr(), conjunction(guard)),
     l2_lhs,
     l2_full_lhs,
-    original_lhs,
+    get_original_name(l2_full_lhs),
     assignment.rhs,
     state.source,
     assignment_type);
 
+  const ssa_exprt &l1_lhs = assignment.lhs;
   if(field_sensitivityt::is_divisible(l1_lhs))
   {
     // Split composite symbol lhs into its components

src/goto-symex/symex_target_equation.cpp

@@ -114,17 +114,13 @@ void symex_target_equationt::assignment(
 {
   PRECONDITION(ssa_lhs.is_not_nil());
 
-  SSA_steps.emplace_back(SSA_assignment_stept{
-    source,
-    guard,
-    ssa_lhs,
-    ssa_full_lhs,
-    original_full_lhs,
-    ssa_rhs,
-    equal_exprt(ssa_lhs, ssa_rhs),
-    assignment_type,
-    assignment_type != assignment_typet::STATE &&
-      assignment_type != assignment_typet::VISIBLE_ACTUAL_PARAMETER});
+  SSA_steps.emplace_back(SSA_assignment_stept{source,
+                                              guard,
+                                              ssa_lhs,
+                                              ssa_full_lhs,
+                                              original_full_lhs,
+                                              ssa_rhs,
+                                              assignment_type});
 
   merge_ireps(SSA_steps.back());
 }

src/util/ssa_expr.cpp

@@ -178,19 +178,19 @@ const irep_idt ssa_exprt::get_l1_object_identifier() const
 #endif
 }
 
-void ssa_exprt::set_level_0(unsigned i)
+void ssa_exprt::set_level_0(std::size_t i)
 {
   set(ID_L0, i);
   ::update_identifier(*this);
 }
 
-void ssa_exprt::set_level_1(unsigned i)
+void ssa_exprt::set_level_1(std::size_t i)
 {
   set(ID_L1, i);
   ::update_identifier(*this);
 }
 
-void ssa_exprt::set_level_2(unsigned i)
+void ssa_exprt::set_level_2(std::size_t i)
 {
   set(ID_L2, i);
   ::update_identifier(*this);

src/util/ssa_expr.h

@@ -52,11 +52,11 @@ class ssa_exprt:public symbol_exprt
     return o.get_identifier();
   }
 
-  void set_level_0(unsigned i);
+  void set_level_0(std::size_t i);
 
-  void set_level_1(unsigned i);
+  void set_level_1(std::size_t i);
 
-  void set_level_2(unsigned i);
+  void set_level_2(std::size_t i);
 
   void remove_level_2();