Add lazy_goto_functions_mapt

Add lazy_goto_functions_mapt, a lazily populated function map, and use it in lazy_goto_modelt
Allow post-processing functions run on a function-by-function basis
Update lazy_goto_modelt to run module passes

Author: NathanJPhillips

src/goto-programs/lazy_goto_functions_map.h

@@ -0,0 +1,161 @@
+// Copyright 2016-2017 Diffblue Limited. All Rights Reserved.
+
+/// \file
+/// A lazy wrapper for goto_functionst.
+
+#ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
+#define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
+
+#include <unordered_set>
+#include "goto_functions.h"
+#include "goto_convert_functions.h"
+#include <util/message.h>
+#include <util/language_file.h>
+
+
+/// Provides a wrapper for a map of lazily loaded goto_functiont.
+/// This incrementally builds a goto-functions object, while permitting
+/// access to goto programs while they are still under construction.
+/// The intended workflow:
+/// 1. The front-end registers the functions that are potentially
+///   available, probably by use of util/language_files.h
+/// 2. The main function registers functions that should be run on
+///   each program, in sequence, after it is converted.
+/// 3. Analyses will then access functions using the `at` function
+/// \tparam bodyt: The type of the function bodies, usually goto_programt
+template<typename bodyt>
+class lazy_goto_functions_mapt final
+{
+public:
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef irep_idt key_type;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef goto_function_templatet<bodyt> &mapped_type;
+  /// The type of elements returned by const members
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches mapped_type
+  typedef const goto_function_templatet<bodyt> &const_mapped_type;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef std::pair<const key_type, goto_function_templatet<bodyt>> value_type;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef value_type &reference;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef const value_type &const_reference;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef value_type *pointer;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef const value_type *const_pointer;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef std::size_t size_type;
+
+  typedef
+  std::function<void(goto_functionst::goto_functiont &function)>
+    post_process_functiont;
+
+private:
+  typedef std::map<key_type, goto_function_templatet<bodyt>> underlying_mapt;
+  underlying_mapt &goto_functions;
+  /// Names of functions that are already fully available in the programt state.
+  /// \remarks These functions do not need processing before being returned
+  /// whenever they are requested
+  mutable std::unordered_set<irep_idt, irep_id_hash> processed_functions;
+
+  language_filest &language_files;
+  symbol_tablet &symbol_table;
+  // This is mutable because it has internal state that it changes during the
+  // course of conversion. Strictly it should make that state mutable or
+  // recreate it for each conversion, but it's easier just to store it mutable.
+  mutable goto_convert_functionst convert_functions;
+  const post_process_functiont post_process_function;
+
+public:
+  /// Creates a lazy_goto_functions_mapt.
+  lazy_goto_functions_mapt(
+    underlying_mapt &goto_functions,
+    language_filest &language_files,
+    symbol_tablet &symbol_table,
+    post_process_functiont post_process_function,
+    message_handlert &message_handler)
+  : goto_functions(goto_functions),
+    language_files(language_files),
+    symbol_table(symbol_table),
+    convert_functions(symbol_table, message_handler),
+    post_process_function(std::move(post_process_function))
+  {
+  }
+
+  /// Gets the number of functions in the map.
+  /// \return The number of functions in the map.
+  size_type size() const
+  {
+    return language_files.lazy_method_map.size();
+  }
+
+  /// Returns whether the map contains any mappings.
+  /// \return Whether the map contains any mappings.
+  bool empty() const { return language_files.lazy_method_map.empty(); }
+
+  /// Checks whether a given function exists in the map.
+  /// \param name: The name of the function to search for.
+  /// \return True if the map contains the given function.
+  bool contains(const key_type &name) const
+  {
+    return language_files.lazy_method_map.count(name)!=0;
+  }
+
+  /// Gets the body for a given function.
+  /// \param name: The name of the function to search for.
+  /// \return The function body corresponding to the given function.
+  const_mapped_type at(const key_type &name) const
+  {
+    return ensure_function_loaded_internal(name).second;
+  }
+
+  /// Gets the body for a given function.
+  /// \param name: The name of the function to search for.
+  /// \return The function body corresponding to the given function.
+  mapped_type at(const key_type &name)
+  {
+    return ensure_function_loaded_internal(name).second;
+  }
+
+  void unload(const key_type &name) const { goto_functions.erase(name); }
+
+private:
+  // This returns a non-const reference, but if you use this method from a
+  // const method then you should not return such a reference without making it
+  // const first
+  reference ensure_function_loaded_internal(const key_type &name) const
+  {
+    reference named_function=ensure_entry_converted(name);
+    mapped_type function=named_function.second;
+    if(processed_functions.count(name)==0)
+    {
+      // Run function-pass conversions
+      post_process_function(function);
+      // Assign procedure-local location numbers for now
+      function.body.compute_location_numbers();
+      processed_functions.insert(name);
+    }
+    return named_function;
+  }
+
+  reference ensure_entry_converted(const key_type &name) const
+  {
+    typename underlying_mapt::iterator it=goto_functions.find(name);
+    if(it!=goto_functions.end())
+      return *it;
+    if(symbol_table.lookup_ref(name).value.is_nil())
+    {
+      // Fill in symbol table entry body
+      // If this returns false then it's a stub
+      language_files.convert_lazy_method(name, symbol_table);
+    }
+    // Create goto_functiont
+    goto_functionst::goto_functiont function;
+    convert_functions.convert_function(name, function);
+    // Add to map
+    return *goto_functions.emplace(name, std::move(function)).first;
+  }
+};
+
+#endif  // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H

src/goto-programs/lazy_goto_model.cpp

@@ -16,10 +16,24 @@
 
 #include <fstream>
 
-lazy_goto_modelt::lazy_goto_modelt(message_handlert &message_handler)
+//! @cond Doxygen_suppress_Lambda_in_initializer_list
+lazy_goto_modelt::lazy_goto_modelt(
+  post_process_functiont post_process_function,
+  post_process_functionst post_process_functions,
+  message_handlert &message_handler)
   : goto_model(new goto_modelt()),
     symbol_table(goto_model->symbol_table),
-    goto_functions(goto_model->goto_functions),
+    goto_functions(
+      goto_model->goto_functions.function_map,
+      language_files,
+      symbol_table,
+      [this] (goto_functionst::goto_functiont &function) -> void
+      {
+        this->post_process_function(function, symbol_table);
+      },
+      message_handler),
+    post_process_function(std::move(post_process_function)),
+    post_process_functions(std::move(post_process_functions)),
     message_handler(message_handler)
 {
   language_files.set_message_handler(message_handler);
@@ -28,11 +42,22 @@ lazy_goto_modelt::lazy_goto_modelt(message_handlert &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),
+    goto_functions(
+      goto_model->goto_functions.function_map,
+      language_files,
+      symbol_table,
+      [this] (goto_functionst::goto_functiont &function) -> void
+      {
+        this->post_process_function(function, symbol_table);
+      },
+      other.message_handler),
     language_files(std::move(other.language_files)),
+    post_process_function(std::move(other.post_process_function)),
+    post_process_functions(std::move(other.post_process_functions)),
     message_handler(other.message_handler)
 {
 }
+//! @endcond
 
 void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
 {
@@ -115,15 +140,12 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
     }
   }
 
-  for(const auto &file : binaries)
+  for(const std::string &file : binaries)
   {
     msg.status() << "Reading GOTO program from file" << messaget::eom;
 
-    if(read_object_and_link(
-      file, symbol_table, goto_functions, message_handler))
-    {
+    if(read_object_and_link(file, *goto_model, message_handler))
       throw 0;
-    }
   }
 
   bool binaries_provided_start =
@@ -177,3 +199,11 @@ void lazy_goto_modelt::load_all_functions() const
 {
   goto_convert(*goto_model, message_handler);
 }
+
+
+bool lazy_goto_modelt::finalize()
+{
+  language_files.clear();
+
+  return post_process_functions(*goto_model);
+}

src/goto-programs/lazy_goto_model.h

@@ -9,16 +9,26 @@
 #include <util/language_file.h>
 
 #include "goto_model.h"
+#include "lazy_goto_functions_map.h"
 #include "goto_convert_functions.h"
 
 class cmdlinet;
+class optionst;
 
 
 /// Model that holds partially loaded map of functions
 class lazy_goto_modelt
 {
 public:
-  explicit lazy_goto_modelt(message_handlert &message_handler);
+  typedef std::function<void(
+    goto_functionst::goto_functiont &function,
+    symbol_tablet &symbol_table)> post_process_functiont;
+  typedef std::function<bool(goto_modelt &goto_model)> post_process_functionst;
+
+  explicit lazy_goto_modelt(
+    post_process_functiont post_process_function,
+    post_process_functionst post_process_functions,
+    message_handlert &message_handler);
 
   lazy_goto_modelt(lazy_goto_modelt &&other);
 
@@ -29,6 +39,33 @@ class lazy_goto_modelt
     return *this;
   }
 
+  /// Create a lazy_goto_modelt from a object that defines function/module pass
+  /// handlers
+  /// \param handler: An object that defines the handlers
+  /// \param options: The options passed to process_goto_functions
+  /// \param message_handler: The message_handler to use for logging
+  /// \tparam THandler a type that defines methods process_goto_function and
+  /// process_goto_functions
+  template<typename THandler>
+  static lazy_goto_modelt from_handler_object(
+    THandler &handler,
+    const optionst &options,
+    message_handlert &message_handler)
+  {
+    return lazy_goto_modelt(
+      [&handler] (
+        goto_functionst::goto_functiont &function,
+        symbol_tablet &symbol_table) -> void
+      {
+        handler.process_goto_function(function, symbol_table);
+      },
+      [&handler, &options] (goto_modelt &goto_model) -> bool
+      {
+        return handler.process_goto_functions(goto_model, options);
+      },
+      message_handler);
+  }
+
   void initialize(const cmdlinet &cmdline);
 
   /// Eagerly loads all functions from the symbol table.
@@ -37,10 +74,14 @@ class lazy_goto_modelt
   /// 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.
+  /// Before freezing the functions all module-level passes are run
   /// \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)
+  static std::unique_ptr<goto_modelt> process_whole_model_and_freeze(
+    lazy_goto_modelt &&model)
   {
+    if(model.finalize())
+      return nullptr;
     return std::move(model.goto_model);
   }
 
@@ -50,13 +91,19 @@ class lazy_goto_modelt
 public:
   /// Reference to symbol_table in the internal goto_model
   symbol_tablet &symbol_table;
-  goto_functionst &goto_functions;
+  const lazy_goto_functions_mapt<goto_programt> goto_functions;
 
 private:
   language_filest language_files;
 
+  // Function/module processing functions
+  const post_process_functiont post_process_function;
+  const post_process_functionst post_process_functions;
+
   /// Logging helper field
   message_handlert &message_handler;
+
+  bool finalize();
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H