Merge pull request #1827 from karkhaz/kk-symex-operator-tidy

[path explore 1/8] Tidy up symext top-level funs

Author: tautschnig

src/cbmc/bmc.cpp

@@ -360,7 +360,7 @@ safety_checkert::resultt bmct::execute(const goto_functionst &goto_functions)
   try
   {
     // perform symbolic execution
-    symex(goto_functions);
+    symex.symex_from_entry_point_of(goto_functions);
 
     // add a partial ordering, if required
     if(equation.has_threads())

src/goto-instrument/accelerate/scratch_program.cpp

@@ -39,7 +39,7 @@ bool scratch_programt::check_sat(bool do_slice)
   symex.constant_propagation=constant_propagation;
   goto_symex_statet::propagationt::valuest constants;
 
-  symex(symex_state, functions, *this);
+  symex.symex_with_state(symex_state, functions, *this);
 
   if(do_slice)
   {

src/goto-symex/goto_symex.h

@@ -37,8 +37,7 @@ class side_effect_exprt;
 class symex_targett;
 class typecast_exprt;
 
-/*! \brief The main class for the forward symbolic simulator
-*/
+/// \brief The main class for the forward symbolic simulator
 class goto_symext
 {
 public:
@@ -68,17 +67,23 @@ class goto_symext
 
   typedef goto_symex_statet statet;
 
-  /** symex all at once, starting from entry point */
-  virtual void operator()(
+  /// \brief symex entire program starting from entry point
+  ///
+  /// The state that goto_symext maintains has a large memory footprint.
+  /// This method deallocates the state as soon as symbolic execution
+  /// has completed, so use it if you don't care about having the state
+  /// around afterwards.
+  virtual void symex_from_entry_point_of(
     const goto_functionst &goto_functions);
 
-  /** symex starting from given goto program */
-  virtual void operator()(
-    const goto_functionst &goto_functions,
-    const goto_programt &goto_program);
-
-  /** start symex in a given state */
-  virtual void operator()(
+  //// \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 &state,
     const goto_functionst &goto_functions,
     const goto_programt &goto_program);
@@ -91,20 +96,21 @@ class goto_symext
   /// \param goto_functions GOTO model to symex.
   /// \param first Entry point in form of a first instruction.
   /// \param limit Final instruction, which itself will not be symexed.
-  virtual void operator()(
+  virtual void symex_instruction_range(
     statet &state,
     const goto_functionst &goto_functions,
     goto_programt::const_targett first,
     goto_programt::const_targett limit);
 
+protected:
   /// Initialise the symbolic execution and the given state with <code>pc</code>
   /// as entry point.
   /// \param state Symex state to initialise.
   /// \param goto_functions GOTO model to symex.
   /// \param pc first instruction to symex
   /// \param limit final instruction, which itself will not
   /// be symexed.
-  void symex_entry_point(
+  void initialize_entry_point(
     statet &state,
     const goto_functionst &goto_functions,
     goto_programt::const_targett pc,
@@ -122,6 +128,7 @@ class goto_symext
     const goto_functionst &goto_functions,
     statet &state);
 
+public:
   // these bypass the target maps
   virtual void symex_step_goto(statet &state, bool taken);
 

src/goto-symex/symex_main.cpp

@@ -124,7 +124,7 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
   }
 }
 
-void goto_symext::symex_entry_point(
+void goto_symext::initialize_entry_point(
   statet &state,
   const goto_functionst &goto_functions,
   const goto_programt::const_targett pc,
@@ -159,14 +159,13 @@ void goto_symext::symex_threaded_step(
   }
 }
 
-/// symex from given state
-void goto_symext::operator()(
+void goto_symext::symex_with_state(
   statet &state,
   const goto_functionst &goto_functions,
   const goto_programt &goto_program)
 {
   PRECONDITION(!goto_program.instructions.empty());
-  symex_entry_point(
+  initialize_entry_point(
     state,
     goto_functions,
     goto_program.instructions.begin(),
@@ -179,28 +178,20 @@ void goto_symext::operator()(
   state.dirty=nullptr;
 }
 
-void goto_symext::operator()(
+void goto_symext::symex_instruction_range(
   statet &state,
   const goto_functionst &goto_functions,
   const goto_programt::const_targett first,
   const goto_programt::const_targett limit)
 {
-  symex_entry_point(state, goto_functions, first, limit);
+  initialize_entry_point(state, goto_functions, first, limit);
   while(state.source.pc->function!=limit->function || state.source.pc!=limit)
     symex_threaded_step(state, goto_functions);
 }
 
-/// symex starting from given program
-void goto_symext::operator()(
-  const goto_functionst &goto_functions,
-  const goto_programt &goto_program)
-{
-  statet state;
-  operator() (state, goto_functions, goto_program);
-}
-
 /// symex from entry point
-void goto_symext::operator()(const goto_functionst &goto_functions)
+void goto_symext::symex_from_entry_point_of(
+    const goto_functionst &goto_functions)
 {
   goto_functionst::function_mapt::const_iterator it=
     goto_functions.function_map.find(goto_functionst::entry_point());
@@ -210,7 +201,8 @@ void goto_symext::operator()(const goto_functionst &goto_functions)
 
   const goto_programt &body=it->second.body;
 
-  operator()(goto_functions, body);
+  statet state;
+  symex_with_state(state, goto_functions, body);
 }
 
 /// do just one step