Merge pull request diffblue#185 from diffblue/nathan/feature/lazy-function-loading

SEC-20: Lazy function loading

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>
@@ -32,9 +33,9 @@
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/remove_exceptions.h>
 #include <goto-programs/remove_java_new.h>
+
 #include <analyses/call_graph.h>
 #include <analyses/call_graph_helpers.h>
-
 #include <analyses/goto_check.h>
 #include <analyses/local_may_alias.h>
 
@@ -140,10 +141,36 @@ 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);
+
+  status() << "Generating GOTO Program" << messaget::eom;
+  lazy_goto_model.load_all_functions();
+
+  // Show the symbol table before process_goto_functions mangles return
+  // values, etc
+  if(cmdline.isset("show-symbol-table"))
+  {
+    ::show_symbol_table(lazy_goto_model.symbol_table, get_ui());
+    return 6;
+  }
 
-  if(process_goto_program(options))
+  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;
+
+  // show it?
+  if(cmdline.isset("show-goto-functions"))
+  {
+    namespacet ns(goto_model.symbol_table);
+
+    goto_model.goto_functions.output(ns, std::cout);
+    return 6;
+  }
 
   if (cmdline.isset("security-scanner"))
   {
@@ -292,16 +319,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;
@@ -339,25 +395,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"))
-    {
-      namespacet ns(goto_model.symbol_table);
-
-      goto_model.goto_functions.output(ns, std::cout);
-      return true;
-    }
-
-    // show it?
-    if(cmdline.isset("show-symbol-table"))
-    {
-      ::show_symbol_table(goto_model, get_ui());
-      return true;
-    }
   }
 
   catch(const char *e)

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();
 };
 

src/taint-slicer/slicing_tasks_builder.cpp

@@ -255,12 +255,11 @@ std::pair<taint_slicing_taskt,std::string> build_slicing_task(
         symbol_table, logger->get_message_handler());
       for(const auto &elem : symbol_table.symbols)
       {
-        if(elem.second.value.id()==ID_code &&
-           converted.count(elem.second.name)==0UL)
+        irep_idt fn_name = elem.second.name;
+        if(elem.second.value.id() == ID_code && converted.count(fn_name) == 0UL)
         {
           converter.convert_function(
-            elem.second.name,
-            goto_functions.function_map[elem.second.name]);
+            fn_name, goto_functions.function_map[fn_name]);
         }
       }
     }