Refactor path storage

src/goto-checker/bmc_util.cpp

@@ -302,7 +302,7 @@ void output_coverage_report(
   }
 }
 
-static void postprocess_equation(
+void postprocess_equation(
   symex_bmct &symex,
   symex_target_equationt &equation,
   const optionst &options,
@@ -329,44 +329,3 @@ static void postprocess_equation(
     symex.validate(validation_modet::INVARIANT);
   }
 }
-
-void perform_symex(
-  abstract_goto_modelt &goto_model,
-  symex_bmct &symex,
-  symbol_tablet &symex_symbol_table,
-  symex_target_equationt &equation,
-  const optionst &options,
-  const namespacet &ns,
-  ui_message_handlert &ui_message_handler)
-{
-  auto get_goto_function =
-    [&goto_model](
-      const irep_idt &id) -> const goto_functionst::goto_functiont & {
-    return goto_model.get_goto_function(id);
-  };
-
-  symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
-
-  postprocess_equation(symex, equation, options, ns, ui_message_handler);
-}
-
-void perform_symex(
-  abstract_goto_modelt &goto_model,
-  symex_bmct &symex,
-  path_storaget::patht &resume,
-  symbol_tablet &symex_symbol_table,
-  const optionst &options,
-  const namespacet &ns,
-  ui_message_handlert &ui_message_handler)
-{
-  auto get_goto_function =
-    [&goto_model](
-      const irep_idt &id) -> const goto_functionst::goto_functiont & {
-    return goto_model.get_goto_function(id);
-  };
-
-  symex.resume_symex_from_saved_state(
-    get_goto_function, resume.state, &resume.equation, symex_symbol_table);
-
-  postprocess_equation(symex, resume.equation, options, ns, ui_message_handler);
-}

src/goto-checker/bmc_util.h

@@ -70,25 +70,16 @@ void slice(
   const optionst &,
   ui_message_handlert &);
 
-/// Perform symbolic execution from the entry point
-void perform_symex(
-  abstract_goto_modelt &,
-  symex_bmct &,
-  symbol_tablet &,
-  symex_target_equationt &,
-  const optionst &,
-  const namespacet &,
-  ui_message_handlert &);
-
-/// Perform symbolic execution starting from \p resume.
-void perform_symex(
-  abstract_goto_modelt &,
-  symex_bmct &,
-  path_storaget::patht &resume,
-  symbol_tablet &,
-  const optionst &,
-  const namespacet &,
-  ui_message_handlert &);
+/// Post process the equation
+/// - add partial order constraints
+/// - slice
+/// - perform validation
+void postprocess_equation(
+  symex_bmct &symex,
+  symex_target_equationt &equation,
+  const optionst &options,
+  const namespacet &ns,
+  ui_message_handlert &ui_message_handler);
 
 /// Output a coverage report as generated by \ref symex_coveraget
 /// if \p cov_out is non-empty.

src/goto-checker/multi_path_symex_checker.cpp

@@ -41,14 +41,9 @@ operator()(propertiest &properties)
   // we haven't got an equation yet
   if(!equation_generated)
   {
-    perform_symex(
-      goto_model,
-      symex,
-      symex_symbol_table,
-      equation,
-      options,
-      ns,
-      ui_message_handler);
+    symex.symex_from_entry_point_of(
+      goto_symext::get_goto_function(goto_model), symex_symbol_table);
+    postprocess_equation(symex, equation, options, ns, ui_message_handler);
 
     output_coverage_report(
       options.get_option("symex-coverage-report"),

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -39,14 +39,9 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
 incremental_goto_checkert::resultt multi_path_symex_only_checkert::
 operator()(propertiest &properties)
 {
-  perform_symex(
-    goto_model,
-    symex,
-    symex_symbol_table,
-    equation,
-    options,
-    ns,
-    ui_message_handler);
+  symex.symex_from_entry_point_of(
+    goto_symext::get_goto_function(goto_model), symex_symbol_table);
+  postprocess_equation(symex, equation, options, ns, ui_message_handler);
 
   output_coverage_report(
     options.get_option("symex-coverage-report"),

src/goto-checker/single_path_symex_checker.cpp

@@ -30,45 +30,6 @@ operator()(propertiest &properties)
 {
   resultt result(resultt::progresst::DONE);
 
-  // Unfortunately, the initial symex run is currently handled differently
-  // from the subsequent runs
-  if(!initial_symex_has_run)
-  {
-    initial_symex_has_run = true;
-    first_equation = symex_target_equationt();
-    symex_bmct symex(
-      ui_message_handler,
-      goto_model.get_symbol_table(),
-      first_equation.value(),
-      options,
-      *worklist);
-
-    setup_symex(symex);
-    perform_symex(
-      goto_model,
-      symex,
-      symex_symbol_table,
-      first_equation.value(),
-      options,
-      ns,
-      ui_message_handler);
-
-    output_coverage_report(
-      options.get_option("symex-coverage-report"),
-      goto_model,
-      symex,
-      ui_message_handler);
-
-    if(symex.get_remaining_vccs() > 0)
-    {
-      prepare(result, properties, first_equation.value());
-      decide(result, properties);
-
-      if(result.progress == resultt::progresst::FOUND_FAIL)
-        return result;
-    }
-  }
-
   // There might be more solutions from the previous equation.
   if(property_decider)
   {
@@ -77,24 +38,28 @@ operator()(propertiest &properties)
       return result;
   }
 
-  if(first_equation.has_value())
+  if(!worklist->empty())
   {
-    // We are in the second iteration. We don't need the equation
-    // from the first iteration anymore.
-    first_equation = {};
+    // We pop the item processed in the previous iteration.
+    worklist->pop();
   }
-  else
+
+  if(!symex_initialized)
   {
-    if(!worklist->empty())
-    {
-      // We are in iteration 3 or later; we pop the item processed
-      // in the previous iteration.
-      worklist->pop();
-    }
-    else
-    {
-      // We are already done.
-    }
+    symex_initialized = true;
+
+    // Put initial state into the work list
+    symex_target_equationt equation;
+    symex_bmct symex(
+      ui_message_handler,
+      goto_model.get_symbol_table(),
+      equation,
+      options,
+      *worklist);
+    setup_symex(symex);
+
+    symex.initialize_path_storage_from_entry_point_of(
+      goto_symext::get_goto_function(goto_model), symex_symbol_table);
   }
 
   while(!worklist->empty())
@@ -106,16 +71,15 @@ operator()(propertiest &properties)
       resume.equation,
       options,
       *worklist);
-
     setup_symex(symex);
-    perform_symex(
-      goto_model,
-      symex,
-      resume,
-      symex_symbol_table,
-      options,
-      ns,
-      ui_message_handler);
+
+    symex.resume_symex_from_saved_state(
+      goto_symext::get_goto_function(goto_model),
+      resume.state,
+      &resume.equation,
+      symex_symbol_table);
+    postprocess_equation(
+      symex, resume.equation, options, ns, ui_message_handler);
 
     output_coverage_report(
       options.get_option("symex-coverage-report"),

src/goto-checker/single_path_symex_checker.h

@@ -43,8 +43,7 @@ class single_path_symex_checkert : public single_path_symex_only_checkert,
   virtual ~single_path_symex_checkert() = default;
 
 protected:
-  bool initial_symex_has_run = false;
-  optionalt<symex_target_equationt> first_equation; // for building traces
+  bool symex_initialized = false;
   std::unique_ptr<goto_symex_property_decidert> property_decider;
 
   void prepare(

src/goto-checker/single_path_symex_only_checker.cpp

@@ -37,29 +37,19 @@ operator()(propertiest &properties)
 {
   resultt result(resultt::progresst::DONE);
 
-  // First run goto-symex from entry point to initialize worklist
   {
-    symex_target_equationt first_equation;
+    // Put initial state into the work list
+    symex_target_equationt equation;
     symex_bmct symex(
       ui_message_handler,
       goto_model.get_symbol_table(),
-      first_equation,
+      equation,
       options,
       *worklist);
-
     setup_symex(symex);
-    perform_symex(
-      goto_model,
-      symex,
-      symex_symbol_table,
-      first_equation,
-      options,
-      ns,
-      ui_message_handler);
 
-    equation_output(symex, first_equation);
-    update_properties_status_from_symex_target_equation(
-      properties, result.updated_properties, first_equation);
+    symex.initialize_path_storage_from_entry_point_of(
+      goto_symext::get_goto_function(goto_model), symex_symbol_table);
   }
 
   while(!worklist->empty())
@@ -71,17 +61,18 @@ operator()(propertiest &properties)
       resume.equation,
       options,
       *worklist);
-
     setup_symex(symex);
-    perform_symex(
-      goto_model,
-      symex,
-      resume,
-      symex_symbol_table,
-      options,
-      ns,
-      ui_message_handler);
+
+    symex.resume_symex_from_saved_state(
+      goto_symext::get_goto_function(goto_model),
+      resume.state,
+      &resume.equation,
+      symex_symbol_table);
+    postprocess_equation(
+      symex, resume.equation, options, ns, ui_message_handler);
+
     equation_output(symex, resume.equation);
+
     update_properties_status_from_symex_target_equation(
       properties, result.updated_properties, resume.equation);
 

src/goto-instrument/accelerate/scratch_program.cpp

@@ -35,7 +35,12 @@ bool scratch_programt::check_sat(bool do_slice)
   output(ns, "scratch", std::cout);
 #endif
 
-  symex.symex_with_state(symex_state, functions, symex_symbol_table);
+  symex.symex_with_state(
+    symex_state,
+    [this](const irep_idt &key) -> const goto_functionst::goto_functiont & {
+      return functions.function_map.at(key);
+    },
+    symex_symbol_table);
 
   if(do_slice)
   {

src/goto-symex/goto_symex.h

@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/options.h>
 #include <util/message.h>
 
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/abstract_goto_model.h>
 
 #include "goto_symex_state.h"
 #include "path_storage.h"
@@ -97,6 +97,9 @@ class goto_symext
     std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
     get_goto_functiont;
 
+  /// Return a function to get/load a goto function from the given goto model
+  static get_goto_functiont get_goto_function(abstract_goto_modelt &);
+
   /// \brief symex entire program starting from entry point
   ///
   /// The state that goto_symext maintains has a large memory footprint.
@@ -107,6 +110,11 @@ class goto_symext
     const get_goto_functiont &get_goto_function,
     symbol_tablet &new_symbol_table);
 
+  /// Puts the initial state of the entry point function into the path storage
+  virtual void initialize_path_storage_from_entry_point_of(
+    const get_goto_functiont &get_goto_function,
+    symbol_tablet &new_symbol_table);
+
   /// Performs symbolic execution using a state and equation that have
   /// already been used to symex part of the program. The state is not
   /// re-initialized; instead, symbolic execution resumes from the program
@@ -117,18 +125,6 @@ class goto_symext
     symex_target_equationt *saved_equation,
     symbol_tablet &new_symbol_table);
 
-  //// \brief symex entire program starting from entry point
-  ///
-  /// This method uses the `state` argument as the symbolic execution
-  /// state, which is useful for examining the state after this method
-  /// returns. The state that goto_symext maintains has a large memory
-  /// footprint, so if keeping the state around is not necessary,
-  /// clients should instead call goto_symext::symex_from_entry_point_of().
-  virtual void symex_with_state(
-    statet &,
-    const goto_functionst &,
-    symbol_tablet &);
-
   //// \brief symex entire program starting from entry point
   ///
   /// This method uses the `state` argument as the symbolic execution
@@ -168,6 +164,14 @@ class goto_symext
     goto_programt::const_targett pc,
     goto_programt::const_targett limit);
 
+  /// Initialize the symbolic execution and the given state with
+  /// the beginning of the entry point function.
+  /// \param get_goto_function: producer for GOTO functions
+  /// \param state: Symex state to initialize.
+  void initialize_entry_point_state(
+    const get_goto_functiont &get_goto_function,
+    statet &state);
+
   /// Invokes symex_step and verifies whether additional threads can be
   /// executed.
   /// \param state: Current GOTO symex step.