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

Clean-up symex assignments

Author: romainbrenguier

src/goto-symex/goto_symex.h

@@ -557,14 +557,14 @@ class goto_symext
     const ssa_exprt &lhs,
     const exprt &full_lhs,
     const struct_exprt &rhs,
-    exprt::operandst &,
+    const exprt::operandst &,
     assignment_typet);
   void symex_assign_symbol(
     statet &,
     const ssa_exprt &lhs,
     const exprt &full_lhs,
     const exprt &rhs,
-    exprt::operandst &,
+    const exprt::operandst &,
     assignment_typet);
   void symex_assign_typecast(
     statet &,
@@ -602,14 +602,6 @@ class goto_symext
     exprt::operandst &,
     assignment_typet);
 
-  /// Store the \p what expression by recursively descending into the operands
-  /// of \p lhs until the first operand \c op0 is _nil_: this _nil_ operand
-  /// is then replaced with \p what.
-  /// \param lhs: Non-symbol pointed-to expression
-  /// \param what: The expression to be added to the \p lhs
-  /// \return The resulting expression
-  static exprt add_to_lhs(const exprt &lhs, const exprt &what);
-
   virtual void
   symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &);
 

src/goto-symex/ssa_step.cpp

@@ -213,3 +213,25 @@ irep_idt SSA_stept::get_property_id() const
 
   return property_id;
 }
+
+SSA_assignment_stept::SSA_assignment_stept(
+  symex_targett::sourcet source,
+  exprt _guard,
+  ssa_exprt _ssa_lhs,
+  exprt _ssa_full_lhs,
+  exprt _original_full_lhs,
+  exprt _ssa_rhs,
+  exprt _cond_expr,
+  symex_targett::assignment_typet _assignment_type,
+  bool _hidden)
+  : SSA_stept(source, goto_trace_stept::typet::ASSIGNMENT)
+{
+  guard = std::move(_guard);
+  ssa_lhs = std::move(_ssa_lhs);
+  ssa_full_lhs = std::move(_ssa_full_lhs);
+  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;
+}

src/goto-symex/ssa_step.h

@@ -195,4 +195,19 @@ class SSA_stept
   void validate(const namespacet &ns, const validation_modet vm) const;
 };
 
+class SSA_assignment_stept : public SSA_stept
+{
+public:
+  SSA_assignment_stept(
+    symex_targett::sourcet source,
+    exprt guard,
+    ssa_exprt ssa_lhs,
+    exprt ssa_full_lhs,
+    exprt original_full_lhs,
+    exprt ssa_rhs,
+    exprt cond_expr,
+    symex_targett::assignment_typet assignment_type,
+    bool hidden);
+};
+
 #endif // CPROVER_GOTO_SYMEX_SSA_STEP_H

src/goto-symex/symex_assign.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
 #include <util/exception_utils.h>
+#include <util/expr_util.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 
@@ -79,9 +80,13 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
   }
 }
 
-exprt goto_symext::add_to_lhs(
-  const exprt &lhs,
-  const exprt &what)
+/// Store the \p what expression by recursively descending into the operands
+/// of \p lhs until the first operand \c op0 is _nil_: this _nil_ operand
+/// is then replaced with \p what.
+/// \param lhs: Non-symbol pointed-to expression
+/// \param what: The expression to be added to the \p lhs
+/// \return The resulting expression
+static exprt add_to_lhs(const exprt &lhs, const exprt &what)
 {
   PRECONDITION(lhs.id() != ID_symbol);
   exprt tmp_what=what;
@@ -387,7 +392,7 @@ void goto_symext::symex_assign_from_struct(
   const ssa_exprt &lhs, // L1
   const exprt &full_lhs,
   const struct_exprt &rhs,
-  exprt::operandst &guard,
+  const exprt::operandst &guard,
   assignment_typet assignment_type)
 {
   const struct_typet &type = to_struct_type(ns.follow(lhs.type()));
@@ -419,7 +424,7 @@ void goto_symext::symex_assign_symbol(
   const ssa_exprt &lhs, // L1
   const exprt &full_lhs,
   const exprt &rhs,
-  exprt::operandst &guard,
+  const exprt::operandst &guard,
   assignment_typet assignment_type)
 {
   // Shortcut the common case of a whole-struct initializer:
@@ -452,16 +457,16 @@ void goto_symext::symex_assign_symbol(
 
   do_simplify(assignment.rhs);
 
-  ssa_exprt &l1_lhs = assignment.lhs;
-  ssa_exprt l2_lhs = state
-                       .assignment(
-                         assignment.lhs,
-                         assignment.rhs,
-                         ns,
-                         symex_config.simplify_opt,
-                         symex_config.constant_propagation,
-                         symex_config.allow_pointer_unsoundness)
-                       .get();
+  const ssa_exprt &l1_lhs = assignment.lhs;
+  const ssa_exprt l2_lhs = state
+                             .assignment(
+                               assignment.lhs,
+                               assignment.rhs,
+                               ns,
+                               symex_config.simplify_opt,
+                               symex_config.constant_propagation,
+                               symex_config.allow_pointer_unsoundness)
+                             .get();
 
   exprt ssa_full_lhs = add_to_lhs(full_lhs, l2_lhs);
   state.record_events.push(false);
@@ -481,12 +486,12 @@ void goto_symext::symex_assign_symbol(
               << messaget::eom;
     });
 
-  // Temporarily add the state guard
-  guard.emplace_back(state.guard.as_expr());
+  const exprt assignment_guard =
+    make_and(state.guard.as_expr(), conjunction(guard));
 
   const exprt original_lhs = get_original_name(l2_full_lhs);
   target.assignment(
-    conjunction(guard),
+    assignment_guard,
     l2_lhs,
     l2_full_lhs,
     original_lhs,
@@ -505,9 +510,6 @@ void goto_symext::symex_assign_symbol(
     state.propagation.erase_if_exists(l1_lhs.get_identifier());
     state.value_set.erase_symbol(l1_lhs, ns);
   }
-
-  // Restore the guard
-  guard.pop_back();
 }
 
 void goto_symext::symex_assign_typecast(
@@ -564,10 +566,8 @@ void goto_symext::symex_assign_array(
   // into
   //   a'==a WITH [i:=e]
 
-  with_exprt new_rhs(lhs_array, lhs_index, rhs);
-  new_rhs.type() = lhs_index_type;
-
-  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
+  const with_exprt new_rhs{lhs_array, lhs_index, rhs};
+  const exprt new_full_lhs = add_to_lhs(full_lhs, lhs);
 
   symex_assign_rec(
     state, lhs_array, new_full_lhs, new_rhs, guard, assignment_type);

src/goto-symex/symex_target_equation.cpp

@@ -114,21 +114,19 @@ void symex_target_equationt::assignment(
 {
   PRECONDITION(ssa_lhs.is_not_nil());
 
-  SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSIGNMENT);
-  SSA_stept &SSA_step=SSA_steps.back();
-
-  SSA_step.guard=guard;
-  SSA_step.ssa_lhs=ssa_lhs;
-  SSA_step.ssa_full_lhs=ssa_full_lhs;
-  SSA_step.original_full_lhs=original_full_lhs;
-  SSA_step.ssa_rhs=ssa_rhs;
-  SSA_step.assignment_type=assignment_type;
-
-  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
-  SSA_step.hidden=(assignment_type!=assignment_typet::STATE &&
-                   assignment_type!=assignment_typet::VISIBLE_ACTUAL_PARAMETER);
-
-  merge_ireps(SSA_step);
+  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});
+
+  merge_ireps(SSA_steps.back());
 }
 
 void symex_target_equationt::decl(

src/solvers/prop/bdd_expr.cpp

@@ -91,18 +91,6 @@ bddt bdd_exprt::from_expr(const exprt &expr)
   return from_expr_rec(expr);
 }
 
-/// Conjunction of two expressions. If the second is already an `and_exprt`
-/// add to its operands instead of creating a new expression.
-static exprt make_and(exprt a, exprt b)
-{
-  if(b.id() == ID_and)
-  {
-    b.add_to_operands(std::move(a));
-    return b;
-  }
-  return and_exprt{std::move(a), std::move(b)};
-}
-
 /// Disjunction of two expressions. If the second is already an `or_exprt`
 /// add to its operands instead of creating a new expression.
 static exprt make_or(exprt a, exprt b)

src/util/expr_util.cpp

@@ -289,3 +289,26 @@ constant_exprt make_boolean_expr(bool value)
   else
     return false_exprt();
 }
+
+exprt make_and(exprt a, exprt b)
+{
+  PRECONDITION(a.type().id() == ID_bool && b.type().id() == ID_bool);
+  if(b.is_constant())
+  {
+    if(b.get(ID_value) == ID_false)
+      return false_exprt{};
+    return a;
+  }
+  if(a.is_constant())
+  {
+    if(a.get(ID_value) == ID_false)
+      return false_exprt{};
+    return b;
+  }
+  if(b.id() == ID_and)
+  {
+    b.add_to_operands(std::move(a));
+    return b;
+  }
+  return and_exprt{std::move(a), std::move(b)};
+}

src/util/expr_util.h

@@ -100,4 +100,9 @@ class is_constantt
 /// returns true_exprt if given true and false_exprt otherwise
 constant_exprt make_boolean_expr(bool);
 
+/// Conjunction of two expressions. If the second is already an `and_exprt`
+/// add to its operands instead of creating a new expression. If one is `true`,
+/// return the other expression. If one is `false` returns `false`.
+exprt make_and(exprt a, exprt b);
+
 #endif // CPROVER_UTIL_EXPR_UTIL_H