Merge pull request #7443 from thomasspriggs/tas/api-verification

Add verification API call

Author: thomasspriggs

src/libcprover-cpp/CMakeLists.txt

@@ -3,4 +3,4 @@ file(GLOB_RECURSE sources "*.cpp" "*.h")
 # This step builds the API in the form of a statically linked library (libcprover-api-cpp.a)
 add_library(cprover-api-cpp ${sources})
 generic_includes(cprover-api-cpp)
-target_link_libraries(cprover-api-cpp goto-programs util langapi ansi-c)
+target_link_libraries(cprover-api-cpp goto-checker goto-programs util langapi ansi-c)

src/libcprover-cpp/api.cpp

@@ -6,12 +6,22 @@
 #include <util/config.h>
 #include <util/message.h>
 #include <util/options.h>
+#include <util/ui_message.h>
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/link_to_library.h>
+#include <goto-programs/process_goto_program.h>
+#include <goto-programs/remove_skip.h>
+#include <goto-programs/set_properties.h>
 
 #include <ansi-c/ansi_c_language.h>
+#include <ansi-c/cprover_library.h>
+#include <assembler/remove_asm.h>
+#include <goto-checker/all_properties_verifier_with_trace_storage.h>
+#include <goto-checker/multi_path_symex_checker.h>
 #include <langapi/mode.h>
+#include <pointer-analysis/add_failed_symbols.h>
 
 #include <memory>
 #include <string>
@@ -105,3 +115,47 @@ void api_sessiont::load_model_from_files(const std::vector<std::string> &files)
   implementation->model = util_make_unique<goto_modelt>(initialize_goto_model(
     files, *implementation->message_handler, *implementation->options));
 }
+
+void api_sessiont::verify_model()
+{
+  PRECONDITION(implementation->model);
+
+  // Remove inline assembler; this needs to happen before adding the library.
+  remove_asm(*implementation->model);
+
+  // add the library
+  messaget log{*implementation->message_handler};
+  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
+               << messaget::eom;
+  link_to_library(
+    *implementation->model,
+    *implementation->message_handler,
+    cprover_c_library_factory);
+
+  // Common removal of types and complex constructs
+  if(::process_goto_program(
+       *implementation->model, *implementation->options, log))
+  {
+    return;
+  }
+
+  // add failed symbols
+  // needs to be done before pointer analysis
+  add_failed_symbols(implementation->model->symbol_table);
+
+  // label the assertions
+  // This must be done after adding assertions and
+  // before using the argument of the "property" option.
+  // Do not re-label after using the property slicer because
+  // this would cause the property identifiers to change.
+  label_properties(*implementation->model);
+
+  remove_skip(*implementation->model);
+
+  ui_message_handlert ui_message_handler(*implementation->message_handler);
+  all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>
+    verifier(
+      *implementation->options, ui_message_handler, *implementation->model);
+  (void)verifier();
+  verifier.report();
+}

src/libcprover-cpp/api.h

@@ -68,6 +68,9 @@ struct api_sessiont
   /// \param files: A vector<string> containing the filenames to be loaded
   void load_model_from_files(const std::vector<std::string> &files);
 
+  /// Verify previously loaded model.
+  void verify_model();
+
 private:
   std::unique_ptr<api_session_implementationt> implementation;
 };

src/libcprover-cpp/module_dependencies.txt

@@ -1,4 +1,7 @@
 ansi-c
-langapi
+assembler
+goto-checker
 goto-programs
+langapi
+pointer-analysis
 util

src/libcprover-cpp/options.cpp

@@ -2,9 +2,13 @@
 
 #include "options.h"
 
+#include <util/cmdline.h>
 #include <util/make_unique.h>
 #include <util/options.h>
 
+#include <ansi-c/goto_check_c.h>
+#include <goto-checker/solver_factory.h>
+
 api_optionst api_optionst::create()
 {
   return api_optionst{};
@@ -16,9 +20,22 @@ api_optionst &api_optionst::simplify(bool on)
   return *this;
 }
 
+static std::unique_ptr<optionst> make_internal_default_options()
+{
+  std::unique_ptr<optionst> options = util_make_unique<optionst>();
+  cmdlinet command_line;
+  PARSE_OPTIONS_GOTO_CHECK(command_line, (*options));
+  parse_solver_options(command_line, *options);
+  options->set_option("built-in-assertions", true);
+  options->set_option("arrays-uf", "auto");
+  options->set_option("depth", UINT32_MAX);
+  options->set_option("sat-preprocessor", true);
+  return options;
+}
+
 std::unique_ptr<optionst> api_optionst::to_engine_options() const
 {
-  optionst engine_options;
-  engine_options.set_option("simplify", simplify_enabled);
-  return util_make_unique<optionst>(engine_options);
+  auto engine_options = make_internal_default_options();
+  engine_options->set_option("simplify", simplify_enabled);
+  return engine_options;
 }

unit/libcprover-cpp/api.cpp

@@ -62,7 +62,9 @@ std::string contains_in_ordert::describe() const
   return description.str();
 }
 
-TEST_CASE("Test loading model from file.", "[core][libcprover-cpp]")
+TEST_CASE(
+  "Test loading and verifying model from file.",
+  "[core][libcprover-cpp]")
 {
   api_sessiont api(api_optionst::create());
 
@@ -76,13 +78,35 @@ TEST_CASE("Test loading model from file.", "[core][libcprover-cpp]")
       output.emplace_back(api_message_get_string(message));
     };
 
-  api.set_message_callback(write_output, &output);
-  api.load_model_from_files({"test.c"});
-  CHECK_THAT(
-    output,
-    (contains_in_ordert{
-      "Parsing test.c",
-      "Converting",
-      "Type-checking test",
-      "Generating GOTO Program"}));
+  SECTION("Load from file")
+  {
+    api.set_message_callback(write_output, &output);
+    api.load_model_from_files({"test.c"});
+    CHECK_THAT(
+      output,
+      (contains_in_ordert{
+        "Parsing test.c",
+        "Converting",
+        "Type-checking test",
+        "Generating GOTO Program"}));
+    output.clear();
+    SECTION("Verify")
+    {
+      api.verify_model();
+      CHECK_THAT(
+        output,
+        (contains_in_ordert{
+          "Removal of function pointers and virtual functions",
+          "Generic Property Instrumentation",
+          "Starting Bounded Model Checking",
+          "Generated 1 VCC(s), 1 remaining after simplification",
+          "Passing problem to propositional reduction",
+          "converting SSA",
+          "Running propositional reduction",
+          "Post-processing",
+          "SAT checker: instance is SATISFIABLE",
+          "[main.assertion.1] line 8 assertion a[4] != 4: FAILURE",
+          "VERIFICATION FAILED"}));
+    }
+  }
 }