Pass preprocessed shadow memory fields to goto_symex

Initializees the shadow_memory member of the goto_symex_state
that tracks the shadow memory information during
symbolic execution.

Author: peterschrammel

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -79,8 +79,8 @@ void multi_path_symex_only_checkert::generate_equation()
 
   const auto symex_start = std::chrono::steady_clock::now();
 
-  symex_symbol_table =
-    symex.symex_from_entry_point_of(goto_symext::get_goto_function(goto_model));
+  symex_symbol_table = symex.symex_from_entry_point_of(
+    goto_symext::get_goto_function(goto_model), fields);
 
   const auto symex_stop = std::chrono::steady_clock::now();
   std::chrono::duration<double> symex_runtime =

src/goto-checker/single_path_symex_only_checker.cpp

@@ -79,7 +79,7 @@ void single_path_symex_only_checkert::initialize_worklist()
     shadow_memoryt::gather_field_declarations(goto_model, ui_message_handler);
 
   symex.initialize_path_storage_from_entry_point_of(
-    goto_symext::get_goto_function(goto_model), symex_symbol_table);
+    goto_symext::get_goto_function(goto_model), symex_symbol_table, fields);
 }
 
 bool single_path_symex_only_checkert::has_finished_exploration(

src/goto-symex/goto_symex.h

@@ -22,6 +22,7 @@ class address_of_exprt;
 class function_application_exprt;
 class goto_symex_statet;
 class path_storaget;
+class shadow_memory_field_definitionst;
 class side_effect_exprt;
 class symex_assignt;
 class typet;
@@ -98,16 +99,22 @@ class goto_symext
   /// having the state around afterwards.
   /// \param get_goto_function: The delegate to retrieve function bodies (see
   ///   \ref get_goto_functiont)
-  /// \return A symbol table holding the symbols added during symbolic
-  ///   execution.
+  /// \param fields The shadow memory field declarations
   NODISCARD
-  virtual symbol_tablet
-  symex_from_entry_point_of(const get_goto_functiont &get_goto_function);
+  virtual symbol_tablet symex_from_entry_point_of(
+    const get_goto_functiont &get_goto_function,
+    const shadow_memory_field_definitionst &fields);
 
   /// Puts the initial state of the entry point function into the path storage
+  /// \param get_goto_function: The delegate to retrieve function bodies (see
+  ///   \ref get_goto_functiont)
+  /// \param new_symbol_table: A symbol table to store the symbols added during
+  /// symbolic execution
+  /// \param fields The shadow memory field declarations
   virtual void initialize_path_storage_from_entry_point_of(
     const get_goto_functiont &get_goto_function,
-    symbol_table_baset &new_symbol_table);
+    symbol_table_baset &new_symbol_table,
+    const shadow_memory_field_definitionst &fields);
 
   /// Performs symbolic execution using a state and equation that have
   /// already been used to symbolically execute part of the program. The state

src/goto-symex/symex_main.cpp

@@ -465,18 +465,24 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
 }
 
 symbol_tablet goto_symext::symex_from_entry_point_of(
-  const get_goto_functiont &get_goto_function)
+  const get_goto_functiont &get_goto_function,
+  const shadow_memory_field_definitionst &fields)
 {
   auto state = initialize_entry_point_state(get_goto_function);
+  // Initialize declared shadow memory fields
+  state->shadow_memory.fields = fields;
 
   return symex_with_state(*state, get_goto_function);
 }
 
 void goto_symext::initialize_path_storage_from_entry_point_of(
   const get_goto_functiont &get_goto_function,
-  symbol_table_baset &new_symbol_table)
+  symbol_table_baset &new_symbol_table,
+  const shadow_memory_field_definitionst &fields)
 {
   auto state = initialize_entry_point_state(get_goto_function);
+  // Initialize declared shadow memory fields
+  state->shadow_memory.fields = fields;
 
   path_storaget::patht entry_point_start(target, *state);
   entry_point_start.state.saved_target = state->source.pc;

unit/path_strategies.cpp

@@ -426,7 +426,9 @@ void _check_with_strategy(
     setup_symex(symex, ns, options, ui_message_handler);
 
     symex.initialize_path_storage_from_entry_point_of(
-      goto_symext::get_goto_function(goto_model), symex_symbol_table);
+      goto_symext::get_goto_function(goto_model),
+      symex_symbol_table,
+      shadow_memory_field_definitionst{});
   }
 
   std::size_t expected_results_cnt = 0;