Merge pull request #7645 from NlightNFotis/rust_verification_result

Translate verification results from C++ to Rust

Author: TGWDB

src/libcprover-cpp/api.cpp

@@ -133,57 +133,7 @@ void api_sessiont::load_model_from_files(
     files, *implementation->message_handler, *implementation->options));
 }
 
-void api_sessiont::verify_model() const
-{
-  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();
-}
-
-// TODO: This is a temporary function - it's basically `verify_model`, tweaked
-// to return the results in a structured format. It's temporary in the sense
-// that this will get folded into the `verify_model` function, but I want to do
-// this slightly later because modifying the interface of `verify_model` from
-// the C++ end breaks the Rust API for now, and I want to take steps one at
-// a time.
-verification_resultt api_sessiont::produce_results()
+std::unique_ptr<verification_resultt> api_sessiont::verify_model() const
 {
   PRECONDITION(implementation->model);
 
@@ -225,10 +175,13 @@ verification_resultt api_sessiont::produce_results()
       *implementation->options, ui_message_handler, *implementation->model);
   verification_resultt result;
   auto results = verifier();
+  // Print messages collected to callback buffer.
+  verifier.report();
+  // Set results object before returning.
   result.set_result(results);
   auto properties = verifier.get_properties();
   result.set_properties(properties);
-  return result;
+  return util_make_unique<verification_resultt>(result);
 }
 
 void api_sessiont::drop_unused_functions() const

src/libcprover-cpp/api.h

@@ -69,8 +69,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) const;
 
-  /// Verify previously loaded model.
-  void verify_model() const;
+  // Run the verification engine against previously loaded model and return
+  // results object pointer.
+  std::unique_ptr<verification_resultt> verify_model() const;
 
   /// Drop unused functions from the loaded goto_model simplifying it
   void drop_unused_functions() const;
@@ -81,9 +82,6 @@ struct api_sessiont
   // A simple API version information function.
   std::unique_ptr<std::string> get_api_version() const;
 
-  /// Run the verification engine and return results.
-  verification_resultt produce_results();
-
 private:
   std::unique_ptr<api_session_implementationt> implementation;
 };

src/libcprover-rust/include/c_api.h

@@ -3,6 +3,7 @@
 #pragma once
 
 #include <memory>
+#include <stdexcept>
 #include <string>
 
 // NOLINTNEXTLINE(build/include)
@@ -11,6 +12,9 @@
 #include "include/c_errors.h"
 
 struct api_sessiont;
+struct verification_resultt;
+enum class verifier_resultt;
+enum class prop_statust;
 
 // Helper function
 std::vector<std::string> const &
@@ -20,6 +24,18 @@ _translate_vector_of_string(rust::Vec<rust::String> elements);
 std::unique_ptr<api_sessiont> new_api_session();
 std::vector<std::string> const &get_messages();
 
+// Exposure of verification result related functions.
+verifier_resultt
+get_verification_result(const std::unique_ptr<verification_resultt> &v);
+std::vector<std::string> const &
+get_property_ids(const std::unique_ptr<verification_resultt> &);
+std::string const &get_property_description(
+  const std::unique_ptr<verification_resultt> &,
+  const std::string &);
+prop_statust get_property_status(
+  const std::unique_ptr<verification_resultt> &,
+  const std::string &);
+
 // NOLINTNEXTLINE(readability/namespace)
 namespace rust
 {
@@ -41,6 +57,16 @@ static void trycatch(Try &&func, Fail &&fail) noexcept
   {
     fail(i.what());
   }
+  catch(const std::out_of_range &our)
+  {
+    fail(our.what());
+  }
+  catch(const std::exception &exc)
+  {
+    // collective catch-all for all exceptions that derive
+    // from standard exception class.
+    fail(exc.what());
+  }
 }
 
 } // namespace behavior

src/libcprover-rust/include/c_errors.h

@@ -2,6 +2,8 @@
 
 #pragma once
 
+#include <string>
+
 // The following type is cloning two types from the `util/exception_utils.h` and
 // `util/invariant.h` files.
 //

src/libcprover-rust/src/c_api.cc

@@ -59,3 +59,33 @@ std::vector<std::string> const &get_messages()
 {
   return output;
 }
+
+verifier_resultt get_verification_result(
+  const std::unique_ptr<verification_resultt> &verifier_result)
+{
+  return verifier_result->final_result();
+}
+
+std::vector<std::string> const &
+get_property_ids(const std::unique_ptr<verification_resultt> &verifier_result)
+{
+  std::vector<std::string> *property_ids = new std::vector<std::string>();
+  *property_ids = verifier_result->get_property_ids();
+  return *property_ids;
+}
+
+std::string const &get_property_description(
+  const std::unique_ptr<verification_resultt> &verifier_result,
+  const std::string &property_id)
+{
+  std::string *description = new std::string();
+  *description = verifier_result->get_property_description(property_id);
+  return *description;
+}
+
+prop_statust get_property_status(
+  const std::unique_ptr<verification_resultt> &verifier_result,
+  const std::string &property_id)
+{
+  return verifier_result->get_property_status(property_id);
+}