Merge pull request #7523 from peterschrammel/shadow-memory-basic

Shadow memory interface and integration hooks [blocks 7535]

Author: peterschrammel

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <util/ui_message.h>
 
+#include <goto-symex/shadow_memory.h>
 #include <goto-symex/show_program.h>
 #include <goto-symex/show_vcc.h>
 
@@ -72,10 +73,14 @@ operator()(propertiest &properties)
 
 void multi_path_symex_only_checkert::generate_equation()
 {
+  // Gather fields for shadow memory instrumentation
+  const auto fields =
+    shadow_memoryt::gather_field_declarations(goto_model, ui_message_handler);
+
   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

@@ -14,6 +14,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/ui_message.h>
 
 #include <goto-symex/path_storage.h>
+#include <goto-symex/shadow_memory.h>
 #include <goto-symex/show_program.h>
 #include <goto-symex/show_vcc.h>
 
@@ -73,8 +74,12 @@ void single_path_symex_only_checkert::initialize_worklist()
     unwindset);
   setup_symex(symex);
 
+  // Gather fields for shadow memory instrumentation
+  const auto fields =
+    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/Makefile

@@ -14,6 +14,7 @@ SRC = auto_objects.cpp \
       postcondition.cpp \
       precondition.cpp \
       renaming_level.cpp \
+      shadow_memory.cpp \
       show_program.cpp \
       show_vcc.cpp \
       slice.cpp \

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/goto_symex.h

@@ -15,13 +15,15 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/message.h>
 
 #include "complexity_limiter.h"
+#include "shadow_memory.h"
 #include "symex_config.h"
 #include "symex_target_equation.h"
 
 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;
@@ -65,7 +67,16 @@ class goto_symext
       path_segment_vccs(0),
       _total_vccs(std::numeric_limits<unsigned>::max()),
       _remaining_vccs(std::numeric_limits<unsigned>::max()),
-      complexity_module(mh, options)
+      complexity_module(mh, options),
+      shadow_memory(
+        std::bind(
+          &goto_symext::symex_assign,
+          this,
+          std::placeholders::_1,
+          std::placeholders::_2,
+          std::placeholders::_3),
+        ns,
+        mh)
   {
   }
 
@@ -98,16 +109,24 @@ class goto_symext
   /// having the state around afterwards.
   /// \param get_goto_function: The delegate to retrieve function bodies (see
   ///   \ref get_goto_functiont)
+  /// \param fields The shadow memory field declarations
   /// \return A symbol table holding the symbols added during symbolic
   ///   execution.
   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
@@ -446,6 +465,16 @@ class goto_symext
     statet &state,
     const goto_programt::instructiont &instruction);
 
+  /// Preserves locality of parameters of a given function by applying L1
+  /// renaming to them.
+  /// \param function_identifier The parameter identifier
+  /// \param state The current state
+  /// \param goto_function The goto function
+  virtual void locality(
+    const irep_idt &function_identifier,
+    goto_symext::statet &state,
+    const goto_functionst::goto_functiont &goto_function);
+
   /// Symbolically execute a END_FUNCTION instruction.
   /// \param state: Symbolic execution state for current instruction
   virtual void symex_end_of_function(statet &);
@@ -815,6 +844,9 @@ class goto_symext
 
   complexity_limitert complexity_module;
 
+  /// Shadow memory instrumentation API
+  shadow_memoryt shadow_memory;
+
 public:
   unsigned get_total_vccs() const
   {

src/goto-symex/goto_symex_state.h

@@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "field_sensitivity.h"
 #include "goto_state.h"
 #include "renaming_level.h"
+#include "shadow_memory_state.h"
 
 #include <functional>
 #include <memory>
@@ -121,6 +122,8 @@ class goto_symex_statet final : public goto_statet
 
   field_sensitivityt field_sensitivity;
 
+  shadow_memory_statet shadow_memory;
+
 protected:
   template <levelt>
   void rename_address(exprt &expr, const namespacet &ns);

src/goto-symex/shadow_memory.cpp

@@ -0,0 +1,111 @@
+/*******************************************************************\
+
+Module: Symex Shadow Memory Instrumentation
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Symex Shadow Memory Instrumentation
+
+#include "shadow_memory.h"
+
+#include <util/fresh_symbol.h>
+
+#include <langapi/language_util.h>
+
+#include "goto_symex_state.h"
+
+void shadow_memoryt::initialize_shadow_memory(
+  goto_symex_statet &state,
+  const exprt &expr,
+  const shadow_memory_field_definitionst::field_definitiont &fields)
+{
+  // To be implemented
+}
+
+symbol_exprt shadow_memoryt::add_field(
+  goto_symex_statet &state,
+  const exprt &expr,
+  const irep_idt &field_name,
+  const typet &field_type)
+{
+  // To be completed
+
+  const auto &function_symbol = ns.lookup(state.source.function_id);
+
+  symbolt &new_symbol = get_fresh_aux_symbol(
+    field_type,
+    id2string(state.source.function_id),
+    SHADOW_MEMORY_PREFIX + from_expr(expr) + "__" + id2string(field_name),
+    state.source.pc->source_location(),
+    function_symbol.mode,
+    state.symbol_table);
+
+  // Call some function on ns to silence the compiler in the meanwhile.
+  ns.get_symbol_table();
+
+  return new_symbol.symbol_expr();
+}
+
+void shadow_memoryt::symex_set_field(
+  goto_symex_statet &state,
+  const exprt::operandst &arguments)
+{
+  // To be implemented
+}
+
+void shadow_memoryt::symex_get_field(
+  goto_symex_statet &state,
+  const exprt &lhs,
+  const exprt::operandst &arguments)
+{
+  // To be implemented
+}
+
+void shadow_memoryt::symex_field_static_init(
+  goto_symex_statet &state,
+  const ssa_exprt &lhs)
+{
+  // To be implemented
+}
+
+void shadow_memoryt::symex_field_static_init_string_constant(
+  goto_symex_statet &state,
+  const ssa_exprt &expr,
+  const exprt &rhs)
+{
+  // To be implemented
+}
+
+void shadow_memoryt::symex_field_local_init(
+  goto_symex_statet &state,
+  const ssa_exprt &expr)
+{
+  // To be implemented
+}
+
+void shadow_memoryt::symex_field_dynamic_init(
+  goto_symex_statet &state,
+  const exprt &expr,
+  const side_effect_exprt &code)
+{
+  // To be implemented
+}
+
+shadow_memory_field_definitionst shadow_memoryt::gather_field_declarations(
+  abstract_goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  // To be implemented
+
+  return shadow_memory_field_definitionst();
+}
+
+void shadow_memoryt::convert_field_declaration(
+  const code_function_callt &code_function_call,
+  shadow_memory_field_definitionst::field_definitiont &fields)
+{
+  // To be implemented
+}