Use abstract_goto_modelt instead of goto_functionst in bmc reporting phase

smowton · smowton · commit 8c501cc1fc8c · 2018-03-20T13:39:53.000Z
This allows lazy_goto_modelt to be passed in instead of a goto_modelt's functions
map as was used previously.
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
@@ -357,11 +357,25 @@ void bmct::setup()
     setup_unwind();
 }
 
-safety_checkert::resultt bmct::execute(const goto_functionst &goto_functions)
+safety_checkert::resultt bmct::execute(
+  abstract_goto_modelt &goto_model)
 {
   try
   {
-    perform_symbolic_execution(goto_functions);
+    auto get_goto_function = [&goto_model](const irep_idt &id) ->
+      const goto_functionst::goto_functiont &
+    {
+      return goto_model.get_goto_function(id);
+    };
+
+    perform_symbolic_execution(get_goto_function);
+
+    // Borrow a reference to the goto functions map. This reference, or
+    // iterators pointing into it, must not be stored by this function or its
+    // callees, as goto_model.get_goto_function (as used by symex)
+    // will have side-effects on it.
+    const goto_functionst &goto_functions =
+      goto_model.get_goto_functions();
 
     // add a partial ordering, if required
     if(equation.has_threads())
@@ -492,11 +506,11 @@ void bmct::slice()
 }
 
 safety_checkert::resultt bmct::run(
-  const goto_functionst &goto_functions)
+  abstract_goto_modelt &goto_model)
 {
   setup();
 
-  return execute(goto_functions);
+  return execute(goto_model);
 }
 
 safety_checkert::resultt bmct::decide(
@@ -595,29 +609,38 @@ void bmct::setup_unwind()
     symex.set_unwind_limit(options.get_unsigned_int_option("unwind"));
 }
 
+/// Perform core BMC, using an abstract model to supply GOTO function bodies
+/// (perhaps created on demand).
+/// \param opts: command-line options affecting BMC
+/// \param model: provides goto function bodies and the symbol table, perhaps
+//    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.
 int bmct::do_language_agnostic_bmc(
   const optionst &opts,
-  const goto_modelt &goto_model,
+  abstract_goto_modelt &model,
   const ui_message_handlert::uit &ui,
   messaget &message,
-  std::function<void(bmct &, const goto_modelt &)> frontend_configure_bmc)
+  std::function<void(bmct &, const symbol_tablet &)> frontend_configure_bmc)
 {
+  const symbol_tablet &symbol_table = model.get_symbol_table();
   message_handlert &mh = message.get_message_handler();
   safety_checkert::resultt result;
   goto_symext::branch_worklistt worklist;
   try
   {
     {
-      cbmc_solverst solvers(
-        opts, goto_model.symbol_table, message.get_message_handler());
+      cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
       solvers.set_ui(ui);
       std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
       cbmc_solver = solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();
-      bmct bmc(opts, goto_model.symbol_table, mh, pc, worklist);
+      bmct bmc(opts, symbol_table, mh, pc, worklist);
       bmc.set_ui(ui);
-      frontend_configure_bmc(bmc, goto_model);
-      result = bmc.run(goto_model.goto_functions);
+      frontend_configure_bmc(bmc, symbol_table);
+      result = bmc.run(model);
     }
     INVARIANT(
       opts.get_bool_option("paths") || worklist.empty(),
@@ -646,23 +669,22 @@ int bmct::do_language_agnostic_bmc(
                        << "Starting new path (" << worklist.size()
                        << " to go)\n"
                        << message.eom;
-      cbmc_solverst solvers(
-        opts, goto_model.symbol_table, message.get_message_handler());
+      cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
       solvers.set_ui(ui);
       std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
       cbmc_solver = solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();
       goto_symext::branch_pointt &resume = worklist.front();
       path_explorert pe(
         opts,
-        goto_model.symbol_table,
+        symbol_table,
         mh,
         pc,
         resume.equation,
         resume.state,
         worklist);
-      frontend_configure_bmc(pe, goto_model);
-      result &= pe.run(goto_model.goto_functions);
+      frontend_configure_bmc(pe, symbol_table);
+      result &= pe.run(model);
       worklist.pop_front();
     }
   }
@@ -694,18 +716,19 @@ int bmct::do_language_agnostic_bmc(
   UNREACHABLE;
 }
 
-void bmct::perform_symbolic_execution(const goto_functionst &goto_functions)
+void bmct::perform_symbolic_execution(
+  goto_symext::get_goto_functiont get_goto_function)
 {
-  symex.symex_from_entry_point_of(goto_functions, symex_symbol_table);
+  symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
   INVARIANT(
     options.get_bool_option("paths") || branch_worklist.empty(),
     "Branch points were saved even though we should have been "
     "executing the entire program and merging paths");
 }
 
 void path_explorert::perform_symbolic_execution(
-  const goto_functionst &goto_functions)
+  goto_symext::get_goto_functiont get_goto_function)
 {
   symex.resume_symex_from_saved_state(
-    goto_functions, saved_state, &equation, symex_symbol_table);
+    get_goto_function, saved_state, &equation, symex_symbol_table);
 }
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
@@ -90,9 +90,14 @@ class bmct:public safety_checkert
       !options.get_option("symex-coverage-report").empty();
   }
 
-  virtual resultt run(const goto_functionst &goto_functions);
+  virtual resultt run(const goto_functionst &goto_functions)
+  {
+    wrapper_goto_modelt model(outer_symbol_table, goto_functions);
+    return run(model);
+  }
+  resultt run(abstract_goto_modelt &);
   void setup();
-  safety_checkert::resultt execute(const goto_functionst &);
+  safety_checkert::resultt execute(abstract_goto_modelt &);
   virtual ~bmct() { }
 
   // additional stuff
@@ -118,22 +123,13 @@ class bmct:public safety_checkert
     symex.add_recursion_unwind_handler(handler);
   }
 
-  /// \brief common BMC code, invoked from language-specific frontends
-  ///
-  /// Do bounded model-checking after all language-specific program
-  /// preprocessing has been completed by language-specific frontends.
-  /// Language-specific frontends may customize the \ref bmct objects
-  /// that are used for model-checking by supplying a function object to
-  /// the `frontend_configure_bmc` parameter of this function; the
-  /// function object will be called with every \ref bmct object that
-  /// is constructed by `do_language_agnostic_bmc`.
   static int do_language_agnostic_bmc(
     const optionst &opts,
-    const goto_modelt &goto_model,
+    abstract_goto_modelt &goto_model,
     const ui_message_handlert::uit &ui,
     messaget &message,
-    std::function<void(bmct &, const goto_modelt &)> frontend_configure_bmc =
-      [](bmct &_bmc, const goto_modelt &) { // NOLINT (*)
+    std::function<void(bmct &, const symbol_tablet &)> frontend_configure_bmc =
+      [](bmct &_bmc, const symbol_tablet &) { // NOLINT (*)
         // Empty default implementation
       });
 
@@ -240,8 +236,8 @@ class bmct:public safety_checkert
   /// invoke the symbolic executor in a class-specific way. This
   /// implementation invokes goto_symext::operator() to perform
   /// full-program model-checking from the entry point of the program.
-  virtual void
-  perform_symbolic_execution(const goto_functionst &goto_functions);
+  virtual void perform_symbolic_execution(
+    goto_symext::get_goto_functiont get_goto_function);
 };
 
 /// \brief Symbolic execution from a saved branch point
@@ -285,8 +281,8 @@ class path_explorert : public bmct
   /// This overrides the base implementation to call the symbolic executor with
   /// the saved symex_target_equationt, symbol_tablet, and goto_symex_statet
   /// provided as arguments to the constructor of this class.
-  void
-  perform_symbolic_execution(const goto_functionst &goto_functions) override;
+  void perform_symbolic_execution(
+    goto_symext::get_goto_functiont get_goto_function) override;
 
 #define OPT_BMC                                                                \
   "(program-only)"                                                             \
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
@@ -105,16 +105,6 @@ class goto_symext
     const goto_functionst &goto_functions,
     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
-  /// counter of the saved state.
-  virtual void resume_symex_from_saved_state(
-    const goto_functionst &goto_functions,
-    const statet &saved_state,
-    symex_target_equationt *const saved_equation,
-    symbol_tablet &new_symbol_table);
-
   /// \brief symex entire program starting from entry point
   ///
   /// The state that goto_symext maintains has a large memory footprint.
@@ -125,6 +115,16 @@ class goto_symext
     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
+  /// counter of the saved state.
+  virtual void 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);
+
   //// \brief symex entire program starting from entry point
   ///
   /// This method uses the `state` argument as the symbolic execution
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
@@ -211,14 +211,11 @@ void goto_symext::symex_with_state(
 }
 
 void goto_symext::resume_symex_from_saved_state(
-  const goto_functionst &goto_functions,
+  const get_goto_functiont &get_goto_function,
   const statet &saved_state,
   symex_target_equationt *const saved_equation,
   symbol_tablet &new_symbol_table)
 {
-  const get_goto_functiont get_goto_function = get_function_from_goto_functions(
-      goto_functions);
-
   // saved_state contains a pointer to a symex_target_equationt that is
   // almost certainly stale. This is because equations are owned by bmcts,
   // and we construct a new bmct for every path that we execute. We're on a
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
@@ -489,12 +489,12 @@ int jbmc_parse_optionst::doit()
   if(set_properties(goto_model))
     return 7; // should contemplate EX_USAGE from sysexits.h
 
-  std::function<void(bmct &, const goto_modelt &)> configure_bmc;
+  std::function<void(bmct &, const symbol_tablet &)> configure_bmc;
   if(options.get_bool_option("java-unwind-enum-static"))
   {
     configure_bmc = [](
-      bmct &bmc, const goto_modelt &goto_model) { // NOLINT (*)
-        bmc.add_loop_unwind_handler([&goto_model](
+      bmct &bmc, const symbol_tablet &symbol_table) { // NOLINT (*)
+        bmc.add_loop_unwind_handler([&symbol_table](
                                       const irep_idt &function_id,
                                       unsigned loop_number,
                                       unsigned unwind,
@@ -504,14 +504,14 @@ int jbmc_parse_optionst::doit()
             loop_number,
             unwind,
             max_unwind,
-            goto_model.symbol_table);
+            symbol_table);
         });
     };
   }
   else
   {
     configure_bmc = [](
-      bmct &bmc, const goto_modelt &goto_model) { // NOLINT (*)
+      bmct &bmc, const symbol_tablet &symbol_table) { // NOLINT (*)
       // NOOP
     };
   }
@@ -637,7 +637,7 @@ int jbmc_parse_optionst::get_goto_program(
 
 void jbmc_parse_optionst::process_goto_function(
   goto_model_functiont &function,
-  const can_produce_functiont &available_functions,
+  const abstract_goto_modelt &model,
   const optionst &options)
 {
   journalling_symbol_tablet &symbol_table = function.get_symbol_table();
@@ -651,9 +651,9 @@ void jbmc_parse_optionst::process_goto_function(
     remove_virtual_functions(function);
 
     auto function_is_stub =
-      [&symbol_table, &available_functions](const irep_idt &id) { // NOLINT(*)
+      [&symbol_table, &model](const irep_idt &id) { // NOLINT(*)
         return symbol_table.lookup_ref(id).value.is_nil() &&
-               !available_functions.can_produce_function(id);
+               !model.can_produce_function(id);
       };
 
     remove_returns(function, function_is_stub);
diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h
@@ -91,7 +91,7 @@ class jbmc_parse_optionst:
 
   void process_goto_function(
     goto_model_functiont &function,
-    const can_produce_functiont &,
+    const abstract_goto_modelt &,
     const optionst &);
   bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
 
diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp
@@ -88,7 +88,7 @@ symbol_tablet load_java_class(
   // Construct a lazy_goto_modelt
   null_message_handlert message_handler;
   lazy_goto_modelt lazy_goto_model(
-    [] (goto_model_functiont &function, const can_produce_functiont &cpf) { }, // NOLINT (*)
+    [] (goto_model_functiont &function, const abstract_goto_modelt &model) { }, // NOLINT (*)
     [] (goto_modelt &goto_model) { return false; }, // NOLINT (*)
     message_handler);
 
