Refactor API class to follow Session Facade pattern and own the memory of the API

Author: NlightNFotis

cpp_api/api.cpp

@@ -1,36 +1,46 @@
-#include <ansi-c/ansi_c_language.h>
+#include "api.h"
+
+#include <util/cmdline.h>
+#include <util/config.h>
+#include <util/message.h>
+#include <util/options.h>
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/initialize_goto_model.h>
 
+#include <ansi-c/ansi_c_language.h>
 #include <langapi/mode.h>
 
-#include <util/cmdline.h>
-#include <util/message.h>
-#include <util/options.h>
-
-#include "api.h"
+#include <memory>
 
-api_depst api_deps;
 extern configt config;
 
-void initialize() {
-    // Initialise a null-message handler (we don't print anything in the API)
-    api_deps.msg_handler = new null_message_handlert();
-    // Initialise default options
-    api_deps.opts = new optionst();
-    // Needed to initialise the language options correctly
-    cmdlinet cmdline;
-    // config is global in config.cpp
-    config.set(cmdline);
-    // Initialise C language mode
-    register_language(new_ansi_c_language);
+// Default initialise the api_dependencies object
+api_dependenciest::api_dependenciest()
+  : // We don't print anything to the console as part of the API
+    message_handler(new null_message_handlert()),
+    // We create a default options object which we are going to
+    // customise later.
+    options(new optionst())
+{
 }
 
-goto_modelt load_model_from_files(
-    const std::vector<std::string> &files,
-    const optionst &options)
+api_dependenciest::~api_dependenciest() = default;
+
+cbmc_api::cbmc_api() : dependencies(new api_dependenciest())
+{
+  // Needed to initialise the language options correctly
+  cmdlinet cmdline;
+  // config is global in config.cpp
+  config.set(cmdline);
+  // Initialise C language mode
+  register_language(new_ansi_c_language);
+}
+
+cbmc_api::~cbmc_api() = default;
+
+void cbmc_api::load_model_from_files(const std::vector<std::string> &files)
 {
-    // This could be nested inside a try/catch, but for now let's leave it alone.
-    return initialize_goto_model(files, *api_deps.msg_handler, options);
+  model = util_make_unique<goto_modelt>(initialize_goto_model(
+    files, *dependencies->message_handler, *dependencies->options));
 }

cpp_api/api.h

@@ -1,24 +1,36 @@
+#include <memory>
 #include <vector>
 
-#include <goto-programs/goto_model.h>
-
-#include <util/message.h>
-#include <util/options.h>
-#include <util/config.h>
+// Forward declaration of API dependencies
+class goto_modelt;
+class message_handlert;
+class optionst;
 
 // A struct containing the API dependencies (some of them, at least)
-struct api_depst {
-    message_handlert *msg_handler;
-    optionst *opts;
+struct api_dependenciest
+{
+  api_dependenciest();
+  ~api_dependenciest();
+
+  std::unique_ptr<message_handlert> message_handler;
+  std::unique_ptr<optionst> options;
 };
 
-/// Initialise API dependencies
-void initialize();
+// An object in the pattern of Session Facade - owning all of the memory
+// the API is using and being responsible for the management of that.
+struct cbmc_api
+{
+  // Initialising constructor
+  explicit cbmc_api();
+  ~cbmc_api();
 
-/// Load a goto_model from a given vector of filenames.
-/// \param files: A vector<string> containing the filenames to be loaded
-/// \param options: An options object, to be passed on to analysis or transformation
-///   passes. 
-goto_modelt load_model_from_files(
-    const std::vector<std::string> &files,
-    const optionst &options);
+  /// Load a goto_model from a given vector of filenames.
+  /// \param files: A vector<string> containing the filenames to be loaded
+  /// \param options: An options object, to be passed on to analysis or
+  /// transformation passes.
+  void load_model_from_files(const std::vector<std::string> &files);
+
+private:
+  std::unique_ptr<goto_modelt> model;
+  std::unique_ptr<api_dependenciest> dependencies;
+};

cpp_api/call_bmc.cpp

@@ -15,8 +15,6 @@
 
 #include "api.h"
 
-extern api_depst api_deps;
-
 int main(int argc, char *argv[])
 {
     try {
@@ -26,9 +24,10 @@ int main(int argc, char *argv[])
         std::vector<std::string> arguments(argv + 1, argv + argc);
 
         // Initialise API dependencies and global configuration in one step.
-        initialize();
+        cbmc_api api;
 
-        auto model = load_model_from_files(arguments, *api_deps.opts);
+        // Demonstrate the loading of a goto-model from the command line arguments
+        api.load_model_from_files(arguments);
 
         std::cout << "Successfully initialised goto_model" << std::endl;
         return 0;