Put initial state into path_storage

Allows us to perform the actual pathwise symex work
in a uniform way.
Required making path_storaget::push accept a single state.

Author: peterschrammel

src/goto-symex/goto_symex.h

@@ -110,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
@@ -159,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.

src/goto-symex/path_storage.cpp

@@ -29,12 +29,9 @@ path_storaget::patht &path_lifot::private_peek()
   return paths.back();
 }
 
-void path_lifot::push(
-  const path_storaget::patht &next_instruction,
-  const path_storaget::patht &jump_target)
+void path_lifot::push(const path_storaget::patht &path)
 {
-  paths.push_back(next_instruction);
-  paths.push_back(jump_target);
+  paths.push_back(path);
 }
 
 void path_lifot::private_pop()
@@ -62,12 +59,9 @@ path_storaget::patht &path_fifot::private_peek()
   return paths.front();
 }
 
-void path_fifot::push(
-  const path_storaget::patht &next_instruction,
-  const path_storaget::patht &jump_target)
+void path_fifot::push(const path_storaget::patht &path)
 {
-  paths.push_back(next_instruction);
-  paths.push_back(jump_target);
+  paths.push_back(path);
 }
 
 void path_fifot::private_pop()

src/goto-symex/path_storage.h

@@ -68,16 +68,8 @@ class path_storaget
   /// that check that the worklist is always empty when symex finishes.
   virtual void clear() = 0;
 
-  /// \brief Add paths to resume to the storage
-  ///
-  /// Symbolic execution is suspended when we reach a conditional goto
-  /// instruction with two successors. Thus, we always add a pair of paths to
-  /// the path storage.
-  ///
-  /// \param next_instruction: the instruction following the goto instruction
-  /// \param jump_target: the target instruction of the goto instruction
-  virtual void
-  push(const patht &next_instruction, const patht &jump_target) = 0;
+  /// \brief Add a path to resume to the storage
+  virtual void push(const patht &) = 0;
 
   /// \brief Remove the next path to resume from the storage
   void pop()
@@ -109,7 +101,7 @@ class path_storaget
 class path_lifot : public path_storaget
 {
 public:
-  void push(const patht &, const patht &) override;
+  void push(const patht &) override;
   std::size_t size() const override;
   void clear() override;
 
@@ -126,7 +118,7 @@ class path_lifot : public path_storaget
 class path_fifot : public path_storaget
 {
 public:
-  void push(const patht &, const patht &) override;
+  void push(const patht &) override;
   std::size_t size() const override;
   void clear() override;
 

src/goto-symex/symex_goto.cpp

@@ -207,7 +207,8 @@ void goto_symext::symex_goto(statet &state)
     log.debug() << "Saving jump target '"
                 << jump_target.state.saved_target->source_location << "'"
                 << log.eom;
-    path_storage.push(next_instruction, jump_target);
+    path_storage.push(next_instruction);
+    path_storage.push(jump_target);
 
     // It is now up to the caller of symex to decide which path to continue
     // executing. Signal to the caller that states have been pushed (therefore

src/goto-symex/symex_main.cpp

@@ -305,9 +305,9 @@ void goto_symext::resume_symex_from_saved_state(
       new_symbol_table);
 }
 
-void goto_symext::symex_from_entry_point_of(
+void goto_symext::initialize_entry_point_state(
   const get_goto_functiont &get_goto_function,
-  symbol_tablet &new_symbol_table)
+  statet &state)
 {
   const goto_functionst::goto_functiont *start_function;
   try
@@ -319,21 +319,41 @@ void goto_symext::symex_from_entry_point_of(
     throw unsupported_operation_exceptiont("the program has no entry point");
   }
 
-  statet state;
-
   state.run_validation_checks = symex_config.run_validation_checks;
 
   initialize_entry_point(
     state,
     get_goto_function,
     goto_functionst::entry_point(),
     start_function->body.instructions.begin(),
-    prev(start_function->body.instructions.end()));
+    std::prev(start_function->body.instructions.end()));
+}
+
+void goto_symext::symex_from_entry_point_of(
+  const get_goto_functiont &get_goto_function,
+  symbol_tablet &new_symbol_table)
+{
+  statet state;
+  initialize_entry_point_state(get_goto_function, state);
 
   symex_with_state(
     state, get_goto_function, new_symbol_table);
 }
 
+void goto_symext::initialize_path_storage_from_entry_point_of(
+  const get_goto_functiont &get_goto_function,
+  symbol_tablet &new_symbol_table)
+{
+  statet state;
+  initialize_entry_point_state(get_goto_function, state);
+
+  path_storaget::patht entry_point_start(target, state);
+  entry_point_start.state.saved_target = state.source.pc;
+  entry_point_start.state.has_saved_next_instruction = true;
+
+  path_storage.push(entry_point_start);
+}
+
 goto_symext::get_goto_functiont
 goto_symext::get_goto_function(abstract_goto_modelt &goto_model)
 {