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,12 @@ safety_checkert::resultt bmct::execute(
     const goto_functionst &goto_functions =
       goto_model.get_goto_functions();
 
+    // This provides the frontend the opportunity to do things like a
+    // symbol-table or goto-functions dump instead of actually running the
+    // checker, like show-vcc except frontend specific.
+    if(frontend_callback_after_symex && frontend_callback_after_symex())
+      return safety_checkert::resultt::SAFE; // to indicate non-error
+
     // add a partial ordering, if required
     if(equation.has_threads())
     {
@@ -623,7 +629,8 @@ int bmct::do_language_agnostic_bmc(
   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 &)> frontend_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 +644,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(frontend_configure_bmc)
+        frontend_configure_bmc(bmc, symbol_table);
       result = bmc.run(model);
     }
     INVARIANT(
@@ -682,8 +690,10 @@ int bmct::do_language_agnostic_bmc(
         pc,
         resume.equation,
         resume.state,
-        worklist);
-      frontend_configure_bmc(pe, symbol_table);
+        worklist,
+        callback_after_symex);
+      if(frontend_configure_bmc)
+        frontend_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),
+      frontend_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 &)>
+      frontend_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),
+      frontend_callback_after_symex(callback_after_symex)
   {
     symex.constant_propagation = options.get_bool_option("propagation");
     symex.record_coverage =
@@ -238,6 +241,8 @@ 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);
+
+  std::function<bool(void)> frontend_callback_after_symex;
 };
 
 /// \brief Symbolic execution from a saved branch point
@@ -260,14 +265,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)
   {
   }