Merge pull request #7275 from tautschnig/cleanup/symex-return

goto-symex interface: return symbol tables by value

Author: tautschnig

Diff for: src/goto-checker/multi_path_symex_only_checker.cpp

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

Diff for: src/goto-checker/single_path_symex_only_checker.cpp

@@ -99,11 +99,8 @@ bool single_path_symex_only_checkert::resume_path(path_storaget::patht &path)
     unwindset);
   setup_symex(symex);
 
-  symex.resume_symex_from_saved_state(
-    goto_symext::get_goto_function(goto_model),
-    path.state,
-    &path.equation,
-    symex_symbol_table);
+  symex_symbol_table = symex.resume_symex_from_saved_state(
+    goto_symext::get_goto_function(goto_model), path.state, &path.equation);
 
   const auto symex_stop = std::chrono::steady_clock::now();
   symex_runtime += std::chrono::duration<double>(symex_stop - symex_start);

Diff for: src/goto-checker/symex_bmc_incremental_one_loop.cpp

@@ -128,7 +128,7 @@ bool symex_bmc_incremental_one_loopt::from_entry_point_of(
 {
   state = initialize_entry_point_state(get_goto_function);
 
-  symex_with_state(*state, get_goto_function, new_symbol_table);
+  new_symbol_table = symex_with_state(*state, get_goto_function);
 
   return should_pause_symex;
 }
@@ -138,7 +138,7 @@ bool symex_bmc_incremental_one_loopt::resume(
 {
   should_pause_symex = false;
 
-  symex_with_state(*state, get_goto_function, state->symbol_table);
+  state->symbol_table = symex_with_state(*state, get_goto_function);
 
   return should_pause_symex;
 }

Diff for: src/goto-instrument/accelerate/scratch_program.cpp

@@ -47,7 +47,7 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
 
   symex_state = symex.initialize_entry_point_state(get_goto_function);
 
-  symex.symex_with_state(*symex_state, get_goto_function, symex_symbol_table);
+  symex_symbol_table = symex.symex_with_state(*symex_state, get_goto_function);
 
   if(do_slice)
   {

Diff for: src/goto-symex/goto_symex.h

@@ -98,11 +98,11 @@ class goto_symext
   /// having the state around afterwards.
   /// \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
-  virtual void symex_from_entry_point_of(
-    const get_goto_functiont &get_goto_function,
-    symbol_tablet &new_symbol_table);
+  /// \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);
 
   /// Puts the initial state of the entry point function into the path storage
   virtual void initialize_path_storage_from_entry_point_of(
@@ -117,13 +117,13 @@ class goto_symext
   ///   \ref get_goto_functiont)
   /// \param saved_state: The symbolic execution state to resume from
   /// \param saved_equation: The equation as previously built up
-  /// \param new_symbol_table: A symbol table to store the symbols added during
-  ///   symbolic execution
-  virtual void resume_symex_from_saved_state(
+  /// \return A symbol table holding the symbols added during symbolic
+  ///   execution.
+  NODISCARD
+  virtual symbol_tablet resume_symex_from_saved_state(
     const get_goto_functiont &get_goto_function,
     const statet &saved_state,
-    symex_target_equationt *saved_equation,
-    symbol_tablet &new_symbol_table);
+    symex_target_equationt *saved_equation);
 
   //// \brief Symbolically execute the entire program starting from entry point
   ///
@@ -135,12 +135,11 @@ class goto_symext
   /// \param state: The symbolic execution state to use for the execution
   /// \param get_goto_functions: A functor to retrieve function bodies to
   ///   execute
-  /// \param new_symbol_table: A symbol table to store the symbols added during
-  ///   symbolic execution
-  virtual void symex_with_state(
-    statet &state,
-    const get_goto_functiont &get_goto_functions,
-    symbol_tablet &new_symbol_table);
+  /// \return A symbol table holding the symbols added during symbolic
+  ///   execution.
+  NODISCARD
+  virtual symbol_tablet
+  symex_with_state(statet &state, const get_goto_functiont &get_goto_functions);
 
   /// \brief Set when states are pushed onto the workqueue
   /// If this flag is set at the end of a symbolic execution run, it means that

Diff for: src/goto-symex/symex_main.cpp

@@ -320,10 +320,9 @@ void goto_symext::symex_threaded_step(
   }
 }
 
-void goto_symext::symex_with_state(
+symbol_tablet goto_symext::symex_with_state(
   statet &state,
-  const get_goto_functiont &get_goto_function,
-  symbol_tablet &new_symbol_table)
+  const get_goto_functiont &get_goto_function)
 {
   // resets the namespace to only wrap a single symbol table, and does so upon
   // destruction of an object of this type; instantiating the type is thus all
@@ -360,28 +359,27 @@ void goto_symext::symex_with_state(
 
   symex_threaded_step(state, get_goto_function);
   if(should_pause_symex)
-    return;
+    return state.symbol_table;
+
   while(!state.call_stack().empty())
   {
     state.has_saved_jump_target = false;
     state.has_saved_next_instruction = false;
     symex_threaded_step(state, get_goto_function);
     if(should_pause_symex)
-      return;
+      return state.symbol_table;
   }
 
   // Clients may need to construct a namespace with both the names in
   // the original goto-program and the names generated during symbolic
   // execution, so return the names generated through symbolic execution
-  // through `new_symbol_table`.
-  new_symbol_table = state.symbol_table;
+  return state.symbol_table;
 }
 
-void goto_symext::resume_symex_from_saved_state(
+symbol_tablet goto_symext::resume_symex_from_saved_state(
   const get_goto_functiont &get_goto_function,
   const statet &saved_state,
-  symex_target_equationt *const saved_equation,
-  symbol_tablet &new_symbol_table)
+  symex_target_equationt *const saved_equation)
 {
   // saved_state contains a pointer to a symex_target_equationt that is
   // almost certainly stale. This is because equations are owned by bmcts,
@@ -393,10 +391,7 @@ void goto_symext::resume_symex_from_saved_state(
 
   // Do NOT do the same initialization that `symex_with_state` does for a
   // fresh state, as that would clobber the saved state's program counter
-  symex_with_state(
-      state,
-      get_goto_function,
-      new_symbol_table);
+  return symex_with_state(state, get_goto_function);
 }
 
 std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
@@ -466,13 +461,12 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
   return state;
 }
 
-void goto_symext::symex_from_entry_point_of(
-  const get_goto_functiont &get_goto_function,
-  symbol_tablet &new_symbol_table)
+symbol_tablet goto_symext::symex_from_entry_point_of(
+  const get_goto_functiont &get_goto_function)
 {
   auto state = initialize_entry_point_state(get_goto_function);
 
-  symex_with_state(*state, get_goto_function, new_symbol_table);
+  return symex_with_state(*state, get_goto_function);
 }
 
 void goto_symext::initialize_path_storage_from_entry_point_of(

Diff for: unit/path_strategies.cpp

@@ -446,11 +446,10 @@ void _check_with_strategy(
       unwindset);
     setup_symex(symex, ns, options, ui_message_handler);
 
-    symex.resume_symex_from_saved_state(
+    symex_symbol_table = symex.resume_symex_from_saved_state(
       goto_symext::get_goto_function(goto_model),
       resume.state,
-      &resume.equation,
-      symex_symbol_table);
+      &resume.equation);
     postprocess_equation(
       symex, resume.equation, options, ns, ui_message_handler);