Add callback after symex to bmct

This permits frontend programs to intervene after symex executes, either in addition to
or instead of running bmc. Its current use case is to implement show-goto-functions and
similar debug output options when symex-driven lazy loading means that function bodies are
not populated until symex has run.

When --paths is in use, the callback will be made every time symex finishes a path.

Author: smowton

src/cbmc/bmc.cpp

@@ -377,6 +377,15 @@ safety_checkert::resultt bmct::execute(
     const goto_functionst &goto_functions =
       goto_model.get_goto_functions();
 
+    // This provides the driver program the opportunity to do things like a
+    // symbol-table or goto-functions dump instead of actually running the
+    // checker, like show-vcc except driver-program specific.
+    // In particular clients that use symex-driven program loading need to print
+    // GOTO functions after symex, as function bodies are not produced until
+    // symex first requests them.
+    if(driver_callback_after_symex && driver_callback_after_symex())
+      return safety_checkert::resultt::SAFE; // to indicate non-error
+
     // add a partial ordering, if required
     if(equation.has_threads())
     {
@@ -616,14 +625,15 @@ void bmct::setup_unwind()
 //    creating those function bodies on demand.
 /// \param ui: user-interface mode (plain text, XML output, JSON output, ...)
 /// \param message: used for logging
-/// \param frontend_configure_bmc: function provided by the frontend program,
-///   which applies frontend-specific configuration to a bmct before running.
+/// \param driver_configure_bmc: function provided by the driver program,
+///   which applies driver-specific configuration to a bmct before running.
 int bmct::do_language_agnostic_bmc(
   const optionst &opts,
   abstract_goto_modelt &model,
   const ui_message_handlert::uit &ui,
   messaget &message,
-  std::function<void(bmct &, const symbol_tablet &)> frontend_configure_bmc)
+  std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc,
+  std::function<bool(void)> callback_after_symex)
 {
   const symbol_tablet &symbol_table = model.get_symbol_table();
   message_handlert &mh = message.get_message_handler();
@@ -637,9 +647,10 @@ int bmct::do_language_agnostic_bmc(
       std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
       cbmc_solver = solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();
-      bmct bmc(opts, symbol_table, mh, pc, worklist);
+      bmct bmc(opts, symbol_table, mh, pc, worklist, callback_after_symex);
       bmc.set_ui(ui);
-      frontend_configure_bmc(bmc, symbol_table);
+      if(driver_configure_bmc)
+        driver_configure_bmc(bmc, symbol_table);
       result = bmc.run(model);
     }
     INVARIANT(
@@ -682,8 +693,10 @@ int bmct::do_language_agnostic_bmc(
         pc,
         resume.equation,
         resume.state,
-        worklist);
-      frontend_configure_bmc(pe, symbol_table);
+        worklist,
+        callback_after_symex);
+      if(driver_configure_bmc)
+        driver_configure_bmc(pe, symbol_table);
       result &= pe.run(model);
       worklist.pop_front();
     }

src/cbmc/bmc.h

@@ -74,7 +74,8 @@ class bmct:public safety_checkert
     const symbol_tablet &outer_symbol_table,
     message_handlert &_message_handler,
     prop_convt &_prop_conv,
-    goto_symext::branch_worklistt &_branch_worklist)
+    goto_symext::branch_worklistt &_branch_worklist,
+    std::function<bool(void)> callback_after_symex)
     : safety_checkert(ns, _message_handler),
       options(_options),
       outer_symbol_table(outer_symbol_table),
@@ -83,7 +84,8 @@ class bmct:public safety_checkert
       branch_worklist(_branch_worklist),
       symex(_message_handler, outer_symbol_table, equation, branch_worklist),
       prop_conv(_prop_conv),
-      ui(ui_message_handlert::uit::PLAIN)
+      ui(ui_message_handlert::uit::PLAIN),
+      driver_callback_after_symex(callback_after_symex)
   {
     symex.constant_propagation=options.get_bool_option("propagation");
     symex.record_coverage=
@@ -128,10 +130,9 @@ class bmct:public safety_checkert
     abstract_goto_modelt &goto_model,
     const ui_message_handlert::uit &ui,
     messaget &message,
-    std::function<void(bmct &, const symbol_tablet &)> frontend_configure_bmc =
-      [](bmct &_bmc, const symbol_tablet &) { // NOLINT (*)
-        // Empty default implementation
-      });
+    std::function<void(bmct &, const symbol_tablet &)>
+      driver_configure_bmc = nullptr,
+    std::function<bool(void)> callback_after_symex = nullptr);
 
 protected:
   /// \brief Constructor for path exploration from saved state
@@ -147,7 +148,8 @@ class bmct:public safety_checkert
     message_handlert &_message_handler,
     prop_convt &_prop_conv,
     symex_target_equationt &_equation,
-    goto_symext::branch_worklistt &_branch_worklist)
+    goto_symext::branch_worklistt &_branch_worklist,
+    std::function<bool(void)> callback_after_symex)
     : safety_checkert(ns, _message_handler),
       options(_options),
       outer_symbol_table(outer_symbol_table),
@@ -156,7 +158,8 @@ class bmct:public safety_checkert
       branch_worklist(_branch_worklist),
       symex(_message_handler, outer_symbol_table, equation, branch_worklist),
       prop_conv(_prop_conv),
-      ui(ui_message_handlert::uit::PLAIN)
+      ui(ui_message_handlert::uit::PLAIN),
+      driver_callback_after_symex(callback_after_symex)
   {
     symex.constant_propagation = options.get_bool_option("propagation");
     symex.record_coverage =
@@ -238,6 +241,12 @@ class bmct:public safety_checkert
   /// full-program model-checking from the entry point of the program.
   virtual void perform_symbolic_execution(
     goto_symext::get_goto_functiont get_goto_function);
+
+  /// Optional callback, to be run after symex but before handing the resulting
+  /// equation to the solver. If it returns true then we will skip the solver
+  /// stage and return "safe" (no assertions violated / coverage goals reached),
+  /// similar to the behaviour when 'show-vcc' or 'program-only' are specified.
+  std::function<bool(void)> driver_callback_after_symex;
 };
 
 /// \brief Symbolic execution from a saved branch point
@@ -260,14 +269,16 @@ class path_explorert : public bmct
     prop_convt &_prop_conv,
     symex_target_equationt &saved_equation,
     const goto_symex_statet &saved_state,
-    goto_symext::branch_worklistt &branch_worklist)
+    goto_symext::branch_worklistt &branch_worklist,
+    std::function<bool(void)> callback_after_symex)
     : bmct(
         _options,
         outer_symbol_table,
         _message_handler,
         _prop_conv,
         saved_equation,
-        branch_worklist),
+        branch_worklist,
+        callback_after_symex),
       saved_state(saved_state)
   {
   }