Merge pull request #7438 from esteffin/esteffin/add-validate-drop-unused-functions-to-api

Expose two goto-instrument passes that Kani uses to C++ API

Author: NlightNFotis

regression/libcprover-cpp/call_bmc.cpp

@@ -6,6 +6,8 @@
 #include <libcprover-cpp/api.h>
 #include <libcprover-cpp/options.h>
 
+#include "goto_model.h"
+
 #include <iostream>
 #include <vector>
 
@@ -26,7 +28,10 @@ int main(int argc, char *argv[])
     std::vector<std::string> arguments(argv + 1, argv + argc);
 
     // Create API options object, to pass to initialiser of API object.
-    auto api_options = api_optionst::create().simplify(false);
+    auto api_options = api_optionst::create()
+                         .simplify(false)
+                         .validate_goto_model(true)
+                         .drop_unused_functions(true);
 
     // Initialise API dependencies and global configuration in one step.
     api_sessiont api(api_options);
@@ -36,6 +41,19 @@ int main(int argc, char *argv[])
     api.load_model_from_files(arguments);
 
     std::cout << "Successfully initialised goto_model" << std::endl;
+
+    // Demonstrate the validation of an already loaded goto-model
+    api.validate_goto_model();
+
+    std::cout << "Successfully validated goto_model" << std::endl;
+
+    // Demonstrate the dropping of unused functions from an already loaded
+    // goto-model
+    api.drop_unused_functions();
+
+    std::cout << "Successfully dropped unused functions from goto_model"
+              << std::endl;
+
     return 0;
   }
   catch(const invalid_command_line_argument_exceptiont &e)

src/libcprover-cpp/api.cpp

@@ -4,6 +4,7 @@
 
 #include <util/cmdline.h>
 #include <util/config.h>
+#include <util/invariant.h>
 #include <util/message.h>
 #include <util/options.h>
 #include <util/ui_message.h>
@@ -13,6 +14,7 @@
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/process_goto_program.h>
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/set_properties.h>
 
 #include <ansi-c/ansi_c_language.h>
@@ -159,3 +161,32 @@ void api_sessiont::verify_model()
   (void)verifier();
   verifier.report();
 }
+
+void api_sessiont::drop_unused_functions()
+{
+  INVARIANT(
+    implementation->model != nullptr,
+    "Model has not been loaded. Load it first using "
+    "api::load_model_from_files");
+
+  messaget log{*implementation->message_handler};
+  log.status() << "Performing instrumentation pass: dropping unused functions"
+               << messaget::eom;
+
+  remove_unused_functions(
+    *implementation->model, *implementation->message_handler);
+}
+
+void api_sessiont::validate_goto_model()
+{
+  INVARIANT(
+    implementation->model != nullptr,
+    "Model has not been loaded. Load it first using "
+    "api::load_model_from_files");
+
+  messaget log{*implementation->message_handler};
+  log.status() << "Validating consistency of goto-model supplied to API session"
+               << messaget::eom;
+
+  implementation->model->validate();
+}

src/libcprover-cpp/api.h

@@ -71,6 +71,12 @@ struct api_sessiont
   /// Verify previously loaded model.
   void verify_model();
 
+  /// Drop unused functions from the loaded goto_model simplifying it
+  void drop_unused_functions();
+
+  /// Validate the loaded goto model
+  void validate_goto_model();
+
 private:
   std::unique_ptr<api_session_implementationt> implementation;
 };

src/libcprover-cpp/options.cpp

@@ -14,12 +14,6 @@ api_optionst api_optionst::create()
   return api_optionst{};
 }
 
-api_optionst &api_optionst::simplify(bool on)
-{
-  simplify_enabled = on;
-  return *this;
-}
-
 static std::unique_ptr<optionst> make_internal_default_options()
 {
   std::unique_ptr<optionst> options = util_make_unique<optionst>();
@@ -33,6 +27,24 @@ static std::unique_ptr<optionst> make_internal_default_options()
   return options;
 }
 
+api_optionst &api_optionst::simplify(bool on)
+{
+  simplify_enabled = on;
+  return *this;
+}
+
+api_optionst &api_optionst::drop_unused_functions(bool on)
+{
+  drop_unused_functions_enabled = on;
+  return *this;
+}
+
+api_optionst &api_optionst::validate_goto_model(bool on)
+{
+  validate_goto_model_enabled = on;
+  return *this;
+}
+
 std::unique_ptr<optionst> api_optionst::to_engine_options() const
 {
   auto engine_options = make_internal_default_options();

src/libcprover-cpp/options.h

@@ -12,6 +12,12 @@ class api_optionst
   // Options for the verification engine
   bool simplify_enabled;
 
+  // Option for dropping unused function
+  bool drop_unused_functions_enabled;
+
+  // Option for validating the goto model
+  bool validate_goto_model_enabled;
+
   // Private interface methods
   api_optionst() = default;
 
@@ -20,6 +26,10 @@ class api_optionst
 
   api_optionst &simplify(bool on);
 
+  api_optionst &drop_unused_functions(bool on);
+
+  api_optionst &validate_goto_model(bool on);
+
   std::unique_ptr<optionst> to_engine_options() const;
 };