Use lazy_goto_modelt

Don't eagerly convert functions during initialisation of goto_modelt.
Currently uses eager loading at a later stage.
Allow post-processing functions run on a function-by-function basis

Author: NathanJPhillips

src/driver/sec_driver_parse_options.cpp

@@ -15,6 +15,7 @@
 
 #include <json/json_parser.h>
 
+#include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
@@ -140,10 +141,19 @@ int sec_driver_parse_optionst::doit()
   register_languages();
   register_evs_pretty_printer();
 
-  goto_model=initialize_goto_model(cmdline, get_message_handler());
+  lazy_goto_modelt lazy_goto_model = lazy_goto_modelt::from_handler_object(
+    *this, options, get_message_handler());
+  lazy_goto_model.initialize(cmdline);
 
-  if(process_goto_program(options))
+  status() << "Generating GOTO Program" << messaget::eom;
+  lazy_goto_model.load_all_functions();
+
+  std::unique_ptr<goto_modelt> maybe_goto_model =
+    lazy_goto_modelt::process_whole_model_and_freeze(
+      std::move(lazy_goto_model));
+  if(maybe_goto_model == nullptr)
     return 6;
+  goto_modelt &goto_model = *maybe_goto_model;
 
   if (cmdline.isset("security-scanner"))
   {
@@ -292,16 +302,45 @@ int sec_driver_parse_optionst::doit()
   return 6;
 }
 
-bool sec_driver_parse_optionst::process_goto_program(
-  const optionst &options)
+void sec_driver_parse_optionst::process_goto_function(
+  goto_functionst::goto_functiont &function,
+  symbol_tablet &symbol_table)
 {
   try
   {
 #if 0
     // Remove inline assembler; this needs to happen before
     // adding the library.
-    remove_asm(goto_model);
+    remove_asm(function.body, symbol_table);
+#endif
+  }
+
+  catch(const char *e)
+  {
+    error() << e << eom;
+    throw;
+  }
+
+  catch(const std::string &e)
+  {
+    error() << e << eom;
+    throw;
+  }
+
+  catch(const std::bad_alloc &)
+  {
+    error() << "Out of memory" << eom;
+    throw;
+  }
+}
 
+bool sec_driver_parse_optionst::process_goto_functions(
+  goto_modelt &goto_model,
+  const optionst &options)
+{
+  try
+  {
+#if 0
     // add the library
     status() << "Adding CPROVER library ("
              << config.ansi_c.arch << ")" << eom;
@@ -340,9 +379,6 @@ bool sec_driver_parse_optionst::process_goto_program(
     // recalculate numbers, etc.
     goto_model.goto_functions.update();
 
-    // add loop ids
-    goto_model.goto_functions.compute_loop_numbers();
-
     // show it?
     if(cmdline.isset("show-goto-functions"))
     {

src/driver/sec_driver_parse_options.h

@@ -11,10 +11,10 @@
 
 #include <langapi/language_ui.h>
 
+#include <goto-programs/goto_functions.h>
 #include <goto-programs/initialize_goto_model.h>
 
 class bmct;
-class goto_functionst;
 class optionst;
 
 #define SEC_DRIVER_OPTIONS \
@@ -55,16 +55,18 @@ class sec_driver_parse_optionst final:
 
   sec_driver_parse_optionst(int argc, const char **argv);
 
+  void process_goto_function(
+    goto_functionst::goto_functiont &function,
+    symbol_tablet &symbol_table);
+  bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
+
 private:
   ui_message_handlert ui_message_handler;
-  goto_modelt goto_model;
 
   void register_languages();
 
   void get_command_line_options(optionst &options);
 
-  bool process_goto_program(const optionst &options);
-
   void eval_verbosity();
 };