Merge pull request #4827 from romainbrenguier/bugfix/symex-assign-symbol

Refactor and unit test symex_assign_symbol

Author: romainbrenguier

src/goto-symex/goto_symex.cpp

@@ -10,7 +10,10 @@ Author: Daniel Kroening, [email protected]
 /// Symbolic Execution
 
 #include "goto_symex.h"
+#include "symex_assign.h"
 
+#include <util/format_expr.h>
+#include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 
 unsigned goto_symext::dynamic_counter=0;
@@ -20,3 +23,63 @@ void goto_symext::do_simplify(exprt &expr)
   if(symex_config.simplify_opt)
     simplify(expr, ns);
 }
+
+void goto_symext::symex_assign(statet &state, const code_assignt &code)
+{
+  exprt lhs = clean_expr(code.lhs(), state, true);
+  exprt rhs = clean_expr(code.rhs(), state, false);
+
+  DATA_INVARIANT(
+    lhs.type() == rhs.type(), "assignments must be type consistent");
+
+  log.conditional_output(
+    log.debug(), [this, &lhs](messaget::mstreamt &mstream) {
+      mstream << "Assignment to " << format(lhs) << " ["
+              << pointer_offset_bits(lhs.type(), ns).value_or(0) << " bits]"
+              << messaget::eom;
+    });
+
+  if(rhs.id() == ID_side_effect)
+  {
+    const side_effect_exprt &side_effect_expr = to_side_effect_expr(rhs);
+    const irep_idt &statement = side_effect_expr.get_statement();
+
+    if(
+      statement == ID_cpp_new || statement == ID_cpp_new_array ||
+      statement == ID_java_new_array_data)
+    {
+      symex_cpp_new(state, lhs, side_effect_expr);
+    }
+    else if(statement == ID_allocate)
+      symex_allocate(state, lhs, side_effect_expr);
+    else if(statement == ID_va_start)
+      symex_va_start(state, lhs, side_effect_expr);
+    else
+      UNREACHABLE;
+  }
+  else
+  {
+    assignment_typet assignment_type = symex_targett::assignment_typet::STATE;
+
+    // Let's hide return value assignments.
+    if(
+      lhs.id() == ID_symbol &&
+      id2string(to_symbol_expr(lhs).get_identifier()).find("#return_value!") !=
+        std::string::npos)
+    {
+      assignment_type = symex_targett::assignment_typet::HIDDEN;
+    }
+
+    // We hide if we are in a hidden function.
+    if(state.call_stack().top().hidden_function)
+      assignment_type = symex_targett::assignment_typet::HIDDEN;
+
+    // We hide if we are executing a hidden instruction.
+    if(state.source.pc->source_location.get_hide())
+      assignment_type = symex_targett::assignment_typet::HIDDEN;
+
+    exprt::operandst lhs_if_then_else_conditions;
+    symex_assignt{state, assignment_type, ns, symex_config, target}.assign_rec(
+      lhs, nil_exprt(), rhs, lhs_if_then_else_conditions);
+  }
+}

src/goto-symex/goto_symex.h

@@ -533,7 +533,8 @@ class goto_symext
 
   typedef symex_targett::assignment_typet assignment_typet;
 
-  /// Execute any let expressions in \p expr using \ref symex_assign_symbol.
+  /// Execute any let expressions in \p expr using
+  /// \ref symex_assignt::assign_symbol.
   /// The assignments will be made in bottom-up topological but otherwise
   /// arbitrary order (i.e. in `(let x = let y = 0 in x + y) + (let z = 0 in z)
   /// we will define `y` before `x`, but `z` and `x` could come in either order)
@@ -545,63 +546,6 @@ class goto_symext
   /// meaning it will be killed when \ref symex_step concludes.
   void lift_let(statet &state, const let_exprt &let_expr);
 
-  void symex_assign_rec(
-    statet &,
-    const exprt &lhs,
-    const exprt &full_lhs,
-    const exprt &rhs,
-    exprt::operandst &,
-    assignment_typet);
-  void symex_assign_from_struct(
-    statet &,
-    const ssa_exprt &lhs,
-    const exprt &full_lhs,
-    const struct_exprt &rhs,
-    const exprt::operandst &,
-    assignment_typet);
-  void symex_assign_symbol(
-    statet &,
-    const ssa_exprt &lhs,
-    const exprt &full_lhs,
-    const exprt &rhs,
-    const exprt::operandst &,
-    assignment_typet);
-  void symex_assign_typecast(
-    statet &,
-    const typecast_exprt &lhs,
-    const exprt &full_lhs,
-    const exprt &rhs,
-    exprt::operandst &,
-    assignment_typet);
-  void symex_assign_array(
-    statet &,
-    const index_exprt &lhs,
-    const exprt &full_lhs,
-    const exprt &rhs,
-    exprt::operandst &,
-    assignment_typet);
-  void symex_assign_struct_member(
-    statet &,
-    const member_exprt &lhs,
-    const exprt &full_lhs,
-    const exprt &rhs,
-    exprt::operandst &,
-    assignment_typet);
-  void symex_assign_if(
-    statet &,
-    const if_exprt &lhs,
-    const exprt &full_lhs,
-    const exprt &rhs,
-    exprt::operandst &,
-    assignment_typet);
-  void symex_assign_byte_extract(
-    statet &,
-    const byte_extract_exprt &lhs,
-    const exprt &full_lhs,
-    const exprt &rhs,
-    exprt::operandst &,
-    assignment_typet);
-
   virtual void
   symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &);