Pass shadow_memory to symex_assignt

We need to call the shadow memory instrumentation API
from there.

Author: peterschrammel

src/goto-symex/goto_symex.cpp

@@ -104,7 +104,7 @@ void goto_symext::symex_assign(
       assignment_type = symex_targett::assignment_typet::HIDDEN;
 
     symex_assignt symex_assign{
-      state, assignment_type, ns, symex_config, target};
+      shadow_memory, state, assignment_type, ns, symex_config, target};
 
     // Try to constant propagate potential side effects of the assignment, when
     // simplification is turned on and there is one thread only. Constant
@@ -118,8 +118,9 @@ void goto_symext::symex_assign(
     }
 
     exprt::operandst lhs_if_then_else_conditions;
-    symex_assign.assign_rec(
-      lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions);
+    symex_assignt{
+      shadow_memory, state, assignment_type, ns, symex_config, target}
+      .assign_rec(lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions);
   }
 }
 

src/goto-symex/symex_assign.cpp

@@ -11,12 +11,12 @@ Author: Daniel Kroening, [email protected]
 
 #include "symex_assign.h"
 
-#include "expr_skeleton.h"
-#include "goto_symex_state.h"
 #include <util/byte_operators.h>
 #include <util/expr_util.h>
 #include <util/range.h>
 
+#include "expr_skeleton.h"
+#include "goto_symex_state.h"
 #include "symex_config.h"
 
 // We can either use with_exprt or update_exprt when building expressions that

src/goto-symex/symex_assign.h

@@ -12,9 +12,11 @@ Author: Romain Brenguier, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_SYMEX_ASSIGN_H
 #define CPROVER_GOTO_SYMEX_SYMEX_ASSIGN_H
 
-#include "symex_target.h"
 #include <util/expr.h>
 
+#include "shadow_memory.h"
+#include "symex_target.h"
+
 class byte_extract_exprt;
 class expr_skeletont;
 class goto_symex_statet;
@@ -26,12 +28,14 @@ class symex_assignt
 {
 public:
   symex_assignt(
+    optionalt<shadow_memoryt> shadow_memory,
     goto_symex_statet &state,
     symex_targett::assignment_typet assignment_type,
     const namespacet &ns,
     const symex_configt &symex_config,
     symex_targett &target)
-    : state(state),
+    : shadow_memory(shadow_memory),
+      state(state),
       assignment_type(assignment_type),
       ns(ns),
       symex_config(symex_config),
@@ -56,6 +60,7 @@ class symex_assignt
     exprt::operandst &guard);
 
 private:
+  optionalt<shadow_memoryt> shadow_memory;
   goto_symex_statet &state;
   symex_targett::assignment_typet assignment_type;
   const namespacet &ns;

src/goto-symex/symex_clean_expr.cpp

@@ -184,7 +184,12 @@ void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
 
   exprt::operandst value_assignment_guard;
   symex_assignt{
-    state, symex_targett::assignment_typet::HIDDEN, ns, symex_config, target}
+    shadow_memory,
+    state,
+    symex_targett::assignment_typet::HIDDEN,
+    ns,
+    symex_config,
+    target}
     .assign_symbol(
       to_ssa_expr(state.rename<L1>(let_expr.symbol(), ns).get()),
       expr_skeletont{},

src/goto-symex/symex_dereference.cpp

@@ -230,7 +230,12 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state)
   lift_lets(state, cache_value);
 
   auto assign = symex_assignt{
-    state, symex_targett::assignment_typet::STATE, ns, symex_config, target};
+    shadow_memory,
+    state,
+    symex_targett::assignment_typet::STATE,
+    ns,
+    symex_config,
+    target};
 
   auto cache_symbol_expr = cache_symbol.symbol_expr();
   assign.assign_symbol(

src/goto-symex/symex_function_call.cpp

@@ -130,7 +130,8 @@ void goto_symext::parameter_assignments(
       rhs = clean_expr(std::move(rhs), state, false);
 
       exprt::operandst lhs_conditions;
-      symex_assignt{state, assignment_type, ns, symex_config, target}
+      symex_assignt{
+        shadow_memory, state, assignment_type, ns, symex_config, target}
         .assign_rec(lhs, expr_skeletont{}, rhs, lhs_conditions);
     }
 

src/goto-symex/symex_start_thread.cpp

@@ -94,7 +94,12 @@ void goto_symext::symex_start_thread(statet &state)
     exprt::operandst lhs_conditions;
     state.record_events.push(false);
     symex_assignt{
-      state, symex_targett::assignment_typet::HIDDEN, ns, symex_config, target}
+      shadow_memory,
+      state,
+      symex_targett::assignment_typet::HIDDEN,
+      ns,
+      symex_config,
+      target}
       .assign_symbol(lhs_l1, expr_skeletont{}, rhs, lhs_conditions);
     const exprt l2_lhs = state.rename(lhs_l1, ns).get();
     state.record_events.pop();
@@ -140,7 +145,12 @@ void goto_symext::symex_start_thread(statet &state)
 
     exprt::operandst lhs_conditions;
     symex_assignt{
-      state, symex_targett::assignment_typet::HIDDEN, ns, symex_config, target}
+      shadow_memory,
+      state,
+      symex_targett::assignment_typet::HIDDEN,
+      ns,
+      symex_config,
+      target}
       .assign_symbol(lhs, expr_skeletont{}, rhs, lhs_conditions);
   }
 }

unit/goto-symex/symex_assign.cpp

@@ -82,11 +82,13 @@ SCENARIO(
     WHEN("Symbol `foo` is assigned constant integer `475`")
     {
       const exprt rhs1 = from_integer(475, int_type);
-      symex_assignt{state,
-                    symex_targett::assignment_typet::STATE,
-                    ns,
-                    symex_config,
-                    target_equation}
+      symex_assignt{
+        {},
+        state,
+        symex_targett::assignment_typet::STATE,
+        ns,
+        symex_config,
+        target_equation}
         .assign_symbol(ssa_foo, expr_skeletont{}, rhs1, guard);
       THEN("An equation is added to the target")
       {
@@ -136,11 +138,13 @@ SCENARIO(
     {
       const exprt rhs1 = from_integer(5721, int_type);
       symex_target_equationt target_equation{null_message_handler};
-      symex_assignt symex_assign{state,
-                                 symex_targett::assignment_typet::STATE,
-                                 ns,
-                                 symex_config,
-                                 target_equation};
+      symex_assignt symex_assign{
+        {},
+        state,
+        symex_targett::assignment_typet::STATE,
+        ns,
+        symex_config,
+        target_equation};
       symex_assign.assign_symbol(ssa_foo, expr_skeletont{}, rhs1, guard);
       THEN("An equation with an empty guard is added to the target")
       {
@@ -217,11 +221,13 @@ SCENARIO(
 
     WHEN("Symbol `struct1` is assigned `struct1 with [field1 <- 234]`")
     {
-      symex_assignt{state,
-                    symex_targett::assignment_typet::STATE,
-                    ns,
-                    symex_config,
-                    target_equation}
+      symex_assignt{
+        {},
+        state,
+        symex_targett::assignment_typet::STATE,
+        ns,
+        symex_config,
+        target_equation}
         .assign_symbol(struct1_ssa, skeleton, rhs, guard);
       THEN("Two equations are added to the target")
       {