Introduce lazy_goto_modelt

Introduces a class that holds a goto_modelt and language_filest to allow for lazy loading of functions.
Don't eagerly convert functions during initialisation of lazy_goto_modelt. Instead adds a function to allow eager loading at a later stage if required (it always is at the moment).

Author: NathanJPhillips

src/goto-programs/Makefile

@@ -27,6 +27,7 @@ SRC = basic_blocks.cpp \
       interpreter.cpp \
       interpreter_evaluate.cpp \
       json_goto_trace.cpp \
+      lazy_goto_model.cpp \
       link_goto_model.cpp \
       link_to_library.cpp \
       loop_ids.cpp \

src/goto-programs/goto_functions_template.h

@@ -121,6 +121,8 @@ class goto_functions_templatet
     return *this;
   }
 
+  void unload(const irep_idt &name) { function_map.erase(name); }
+
   void clear()
   {
     function_map.clear();

src/goto-programs/initialize_goto_model.cpp

@@ -132,10 +132,9 @@ goto_modelt initialize_goto_model(
     // Rebuild the entry-point, using the language annotation of the
     // existing __CPROVER_start function:
     rebuild_goto_start_functiont rebuild_existing_start(
-      msg.get_message_handler(),
       cmdline,
-      goto_model.symbol_table,
-      goto_model.goto_functions);
+      goto_model,
+      msg.get_message_handler());
     entry_point_generation_failed=rebuild_existing_start();
   }
   else if(!binaries_provided_start)

src/goto-programs/lazy_goto_model.cpp

@@ -0,0 +1,179 @@
+// Copyright 2017 Diffblue Limited. All Rights Reserved.
+
+/// \file
+/// Model for lazy loading of functions
+
+#include "lazy_goto_model.h"
+#include "read_goto_binary.h"
+#include "rebuild_goto_start_function.h"
+
+#include <langapi/mode.h>
+
+#include <util/cmdline.h>
+#include <util/config.h>
+#include <util/language.h>
+#include <util/unicode.h>
+
+#include <fstream>
+
+lazy_goto_modelt::lazy_goto_modelt(message_handlert &message_handler)
+  : goto_model(new goto_modelt()),
+    symbol_table(goto_model->symbol_table),
+    goto_functions(goto_model->goto_functions),
+    message_handler(message_handler)
+{
+  language_files.set_message_handler(message_handler);
+}
+
+lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
+  : goto_model(std::move(other.goto_model)),
+    symbol_table(goto_model->symbol_table),
+    goto_functions(goto_model->goto_functions),
+    language_files(std::move(other.language_files)),
+    message_handler(other.message_handler)
+{
+}
+
+void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
+{
+  messaget msg(message_handler);
+
+  const std::vector<std::string> &files=cmdline.args;
+  if(files.empty())
+  {
+    msg.error() << "Please provide a program" << messaget::eom;
+    throw 0;
+  }
+
+  std::vector<std::string> binaries, sources;
+  binaries.reserve(files.size());
+  sources.reserve(files.size());
+
+  for(const auto &file : files)
+  {
+    if(is_goto_binary(file))
+      binaries.push_back(file);
+    else
+      sources.push_back(file);
+  }
+
+  if(!sources.empty())
+  {
+    for(const auto &filename : sources)
+    {
+#ifdef _MSC_VER
+      std::ifstream infile(widen(filename));
+#else
+      std::ifstream infile(filename);
+#endif
+
+      if(!infile)
+      {
+        msg.error() << "failed to open input file `" << filename
+                    << '\'' << messaget::eom;
+        throw 0;
+      }
+
+      std::pair<language_filest::file_mapt::iterator, bool> result =
+        language_files.file_map.emplace(filename, language_filet());
+
+      language_filet &lf=result.first->second;
+
+      lf.filename=filename;
+      lf.language=get_language_from_filename(filename);
+
+      if(lf.language==nullptr)
+      {
+        source_locationt location;
+        location.set_file(filename);
+        msg.error().source_location=location;
+        msg.error() << "failed to figure out type of file" << messaget::eom;
+        throw 0;
+      }
+
+      languaget &language=*lf.language;
+      language.set_message_handler(message_handler);
+      language.get_language_options(cmdline);
+
+      msg.status() << "Parsing " << filename << messaget::eom;
+
+      if(language.parse(infile, filename))
+      {
+        msg.error() << "PARSING ERROR" << messaget::eom;
+        throw 0;
+      }
+
+      lf.get_modules();
+    }
+
+    msg.status() << "Converting" << messaget::eom;
+
+    if(language_files.typecheck(symbol_table))
+    {
+      msg.error() << "CONVERSION ERROR" << messaget::eom;
+      throw 0;
+    }
+  }
+
+  for(const auto &file : binaries)
+  {
+    msg.status() << "Reading GOTO program from file" << messaget::eom;
+
+    if(read_object_and_link(
+      file, symbol_table, goto_functions, message_handler))
+    {
+      throw 0;
+    }
+  }
+
+  bool binaries_provided_start =
+    symbol_table.has_symbol(goto_functionst::entry_point());
+
+  bool entry_point_generation_failed=false;
+
+  if(binaries_provided_start && cmdline.isset("function"))
+  {
+    // Rebuild the entry-point, using the language annotation of the
+    // existing __CPROVER_start function:
+    rebuild_lazy_goto_start_functiont rebuild_existing_start(
+      cmdline, *this, message_handler);
+    entry_point_generation_failed=rebuild_existing_start();
+  }
+  else if(!binaries_provided_start)
+  {
+    // Unsure of the rationale for only generating stubs when there are no
+    // GOTO binaries in play; simply mirroring old code in language_uit here.
+    if(binaries.empty())
+    {
+      // Enable/disable stub generation for opaque methods
+      bool stubs_enabled=cmdline.isset("generate-opaque-stubs");
+      language_files.set_should_generate_opaque_method_stubs(stubs_enabled);
+    }
+
+    // Allow all language front-ends to try to provide the user-specified
+    // (--function) entry-point, or some language-specific default:
+    entry_point_generation_failed=
+      language_files.generate_support_functions(symbol_table);
+  }
+
+  if(entry_point_generation_failed)
+  {
+    msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
+    throw 0;
+  }
+
+  if(language_files.final(symbol_table))
+  {
+    msg.error() << "FINAL STAGE CONVERSION ERROR" << messaget::eom;
+    throw 0;
+  }
+
+  // stupid hack
+  config.set_object_bits_from_symbol_table(symbol_table);
+}
+
+/// Eagerly loads all functions from the symbol table.
+void lazy_goto_modelt::load_all_functions() const
+{
+  goto_convert(*goto_model, message_handler);
+}

src/goto-programs/lazy_goto_model.h

@@ -0,0 +1,62 @@
+// Copyright 2016-2017 Diffblue Limited. All Rights Reserved.
+
+/// \file
+/// Model for lazy loading of functions
+
+#ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
+#define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
+
+#include <util/language_file.h>
+
+#include "goto_model.h"
+#include "goto_convert_functions.h"
+
+class cmdlinet;
+
+
+/// Model that holds partially loaded map of functions
+class lazy_goto_modelt
+{
+public:
+  explicit lazy_goto_modelt(message_handlert &message_handler);
+
+  lazy_goto_modelt(lazy_goto_modelt &&other);
+
+  lazy_goto_modelt &operator=(lazy_goto_modelt &&other)
+  {
+    goto_model = std::move(other.goto_model);
+    language_files = std::move(other.language_files);
+    return *this;
+  }
+
+  void initialize(const cmdlinet &cmdline);
+
+  /// Eagerly loads all functions from the symbol table.
+  void load_all_functions() const;
+
+  /// The model returned here has access to the functions we've already
+  /// loaded but is frozen in the sense that, with regard to the facility to
+  /// load new functions, it has let it go.
+  /// \param model: The lazy_goto_modelt to freeze
+  /// \returns The frozen goto_modelt or an empty optional if freezing fails
+  static std::unique_ptr<goto_modelt> freeze(lazy_goto_modelt &&model)
+  {
+    return std::move(model.goto_model);
+  }
+
+private:
+  std::unique_ptr<goto_modelt> goto_model;
+
+public:
+  /// Reference to symbol_table in the internal goto_model
+  symbol_tablet &symbol_table;
+  goto_functionst &goto_functions;
+
+private:
+  language_filest language_files;
+
+  /// Logging helper field
+  message_handlert &message_handler;
+};
+
+#endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H

src/goto-programs/rebuild_goto_start_function.cpp

@@ -8,7 +8,6 @@
 
 #include "rebuild_goto_start_function.h"
 
-#include <goto-programs/goto_functions.h>
 #include <util/language.h>
 #include <util/symbol.h>
 #include <util/symbol_table.h>
@@ -17,22 +16,21 @@
 #include <langapi/mode.h>
 #include <memory>
 
-/// To rebuild the _start funciton in the event the program was compiled into
+/// To rebuild the _start function in the event the program was compiled into
 /// GOTO with a different entry function selected.
+/// \param goto_model: The goto functions (to replace the body of the _start
+///   function) and symbol table (to replace the _start function symbol) of the
+///   program.
 /// \param _message_handler: The message handler to report any messages with
-/// \param symbol_table: The symbol table of the program (to replace the _start
-///   functions symbo)
-/// \param goto_functions: The goto functions of the program (to replace the
-///   body of the _start function).
-rebuild_goto_start_functiont::rebuild_goto_start_functiont(
-  message_handlert &_message_handler,
+template<typename goto_modelt>
+rebuild_goto_start_function_baset<goto_modelt>::
+rebuild_goto_start_function_baset(
   const cmdlinet &cmdline,
-  symbol_tablet &symbol_table,
-  goto_functionst &goto_functions):
-    messaget(_message_handler),
+  goto_modelt &goto_model,
+  message_handlert &message_handler):
+    messaget(message_handler),
     cmdline(cmdline),
-    symbol_table(symbol_table),
-    goto_functions(goto_functions)
+    goto_model(goto_model)
 {
 }
 
@@ -44,7 +42,8 @@ rebuild_goto_start_functiont::rebuild_goto_start_functiont(
 /// called from _start
 /// \return Returns true if either the symbol is not found, or something went
 ///   wrong with generating the start_function. False otherwise.
-bool rebuild_goto_start_functiont::operator()()
+template<typename goto_modelt>
+bool rebuild_goto_start_function_baset<goto_modelt>::operator()()
 {
   const irep_idt &mode=get_entry_point_mode();
 
@@ -58,43 +57,40 @@ bool rebuild_goto_start_functiont::operator()()
   remove_existing_entry_point();
 
   bool return_code=
-    language->generate_support_functions(symbol_table);
+    language->generate_support_functions(goto_model.symbol_table);
 
-  // Remove the function from the goto_functions so it is copied back in
+  // Remove the function from the goto functions so it is copied back in
   // from the symbol table during goto_convert
   if(!return_code)
-  {
-    const auto &start_function=
-      goto_functions.function_map.find(goto_functionst::entry_point());
-    if(start_function!=goto_functions.function_map.end())
-    {
-      goto_functions.function_map.erase(start_function);
-    }
-  }
+    goto_model.goto_functions.unload(goto_functionst::entry_point());
 
   return return_code;
 }
 
 /// Find out the mode of the current entry point to determine the mode of the
 /// replacement entry point
 /// \return A mode string saying which language to use
-irep_idt rebuild_goto_start_functiont::get_entry_point_mode() const
+template<typename goto_modelt>
+irep_idt
+rebuild_goto_start_function_baset<goto_modelt>::get_entry_point_mode() const
 {
   const symbolt &current_entry_point=
-    *symbol_table.lookup(goto_functionst::entry_point());
+    *goto_model.symbol_table.lookup(goto_functionst::entry_point());
   return current_entry_point.mode;
 }
 
 /// Eliminate the existing entry point function symbol and any symbols created
 /// in that scope from the symbol table.
-void rebuild_goto_start_functiont::remove_existing_entry_point()
+template<typename goto_modelt>
+void
+rebuild_goto_start_function_baset<goto_modelt>::remove_existing_entry_point()
 {
   // Remove the function itself
-  symbol_table.remove(goto_functionst::entry_point());
+  goto_model.symbol_table.remove(goto_functionst::entry_point());
 
   // And any symbols created in the scope of the entry point
   std::vector<irep_idt> entry_point_symbols;
-  for(const auto &symbol_entry : symbol_table.symbols)
+  for(const auto &symbol_entry : goto_model.symbol_table.symbols)
   {
     const bool is_entry_point_symbol=
       has_prefix(
@@ -107,6 +103,9 @@ void rebuild_goto_start_functiont::remove_existing_entry_point()
 
   for(const irep_idt &entry_point_symbol : entry_point_symbols)
   {
-    symbol_table.remove(entry_point_symbol);
+    goto_model.symbol_table.remove(entry_point_symbol);
   }
 }
+
+template class rebuild_goto_start_function_baset<goto_modelt>;
+template class rebuild_goto_start_function_baset<lazy_goto_modelt>;