Merge pull request #7538 from NlightNFotis/structured_verification_results

Add a structured verification results class in the C++ API

Author: NlightNFotis

src/libcprover-cpp/api.cpp

@@ -177,6 +177,60 @@ void api_sessiont::verify_model() const
   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()
+{
+  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);
+  verification_resultt result;
+  auto results = verifier();
+  result.set_result(results);
+  auto properties = verifier.get_properties();
+  result.set_properties(properties);
+  return result;
+}
+
 void api_sessiont::drop_unused_functions() const
 {
   INVARIANT(

src/libcprover-cpp/api.h

@@ -18,6 +18,7 @@ struct api_session_implementationt;
 // as the design principle is to be followed.)
 
 #include "api_options.h" // IWYU pragma: keep
+#include "verification_result.h" // IWYU pragma: keep
 
 /// Opaque message type. Properties of messages to be fetched through further
 /// api calls.
@@ -80,6 +81,9 @@ 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-cpp/verification_result.cpp

@@ -0,0 +1,151 @@
+// Copyright (c) 2023 Fotis Koutoulakis for Diffblue Ltd.
+
+/// \file
+/// Interface for the various verification engines providing results
+//  in a structured form.
+
+#include "verification_result.h"
+
+#include <util/invariant.h>
+#include <util/make_unique.h>
+
+#include <goto-checker/properties.h>
+
+#include <algorithm>
+#include <string>
+#include <vector>
+
+class verification_resultt::verification_result_implt
+{
+  propertiest _properties;
+  resultt _verifier_result;
+
+public:
+  verification_result_implt() = default;
+  verification_result_implt(const verification_result_implt &other) = default;
+  ~verification_result_implt() = default;
+
+  void set_properties(propertiest &properties);
+  void set_result(resultt &verification_result);
+
+  resultt get_result();
+  const propertiest &get_properties();
+};
+
+// Impl
+
+void verification_resultt::verification_result_implt::set_properties(
+  propertiest &properties)
+{
+  _properties = properties;
+}
+
+void verification_resultt::verification_result_implt::set_result(
+  resultt &result)
+{
+  _verifier_result = result;
+}
+
+resultt verification_resultt::verification_result_implt::get_result()
+{
+  return _verifier_result;
+}
+
+const propertiest &
+verification_resultt::verification_result_implt::get_properties()
+{
+  return _properties;
+}
+
+// Verification_result
+
+verification_resultt::verification_resultt()
+  : _impl(util_make_unique<verification_resultt::verification_result_implt>())
+{
+}
+
+verification_resultt::~verification_resultt()
+{
+}
+
+verification_resultt::verification_resultt(const verification_resultt &other)
+  : _impl(util_make_unique<verification_result_implt>(*other._impl))
+{
+}
+
+verification_resultt &
+verification_resultt::operator=(verification_resultt &&) = default;
+verification_resultt &
+verification_resultt::operator=(const verification_resultt &other)
+{
+  *_impl = *other._impl;
+  return *this;
+}
+
+void verification_resultt::set_properties(propertiest &properties)
+{
+  _impl->set_properties(properties);
+}
+
+void verification_resultt::set_result(resultt &result)
+{
+  _impl->set_result(result);
+}
+
+verifier_resultt verification_resultt::final_result() const
+{
+  switch(_impl->get_result())
+  {
+  case resultt::ERROR:
+    return verifier_resultt::ERROR;
+  case resultt::FAIL:
+    return verifier_resultt::FAIL;
+  case resultt::PASS:
+    return verifier_resultt::PASS;
+  case resultt::UNKNOWN:
+    return verifier_resultt::UNKNOWN;
+  }
+  // Required to silence compiler warnings that are promoted as errors!
+  UNREACHABLE;
+}
+
+std::vector<std::string> verification_resultt::get_property_ids() const
+{
+  std::vector<std::string> result;
+  for(const auto &props : _impl->get_properties())
+  {
+    result.push_back(as_string(props.first));
+  }
+  return result;
+}
+
+std::string verification_resultt::get_property_description(
+  const std::string &property_id) const
+{
+  auto irepidt_property = irep_idt(property_id);
+  const auto description =
+    _impl->get_properties().at(irepidt_property).description;
+  return description;
+}
+
+prop_statust
+verification_resultt::get_property_status(const std::string &property_id) const
+{
+  auto irepidt_property = irep_idt(property_id);
+  switch(_impl->get_properties().at(irepidt_property).status)
+  {
+  case property_statust::ERROR:
+    return prop_statust::ERROR;
+  case property_statust::FAIL:
+    return prop_statust::FAIL;
+  case property_statust::NOT_CHECKED:
+    return prop_statust::NOT_CHECKED;
+  case property_statust::NOT_REACHABLE:
+    return prop_statust::NOT_REACHABLE;
+  case property_statust::PASS:
+    return prop_statust::PASS;
+  case property_statust::UNKNOWN:
+    return prop_statust::UNKNOWN;
+  }
+  UNREACHABLE;
+}

src/libcprover-cpp/verification_result.h

@@ -0,0 +1,83 @@
+// Copyright (c) 2023 Fotis Koutoulakis for Diffblue Ltd.
+
+/// \file
+/// Interface for the various verification engines providing results
+//  in a structured form.
+
+#ifndef CPROVER_LIBCPROVER_CPP_VERIFICATION_RESULT_H
+#define CPROVER_LIBCPROVER_CPP_VERIFICATION_RESULT_H
+
+#include <map>
+#include <memory>
+#include <string>
+#include <vector>
+
+#ifndef USE_STD_STRING
+#  define USE_DSTRING
+#endif
+
+#ifdef USE_DSTRING
+class dstringt;
+typedef dstringt irep_idt;
+#else
+typedef std::string irep_idt;
+#endif
+
+struct property_infot;
+using propertiest = std::map<irep_idt, property_infot>;
+enum class resultt;
+
+// The enumerations here mirror the ones in properties.h.
+// The reason we do so is that we want to expose the same information
+// to users of the API, without including (and therefore, exposing)
+// CBMC internal headers.
+
+enum class prop_statust
+{
+  /// The property was not checked (also used for initialization)
+  NOT_CHECKED,
+  /// The checker was unable to determine the status of the property
+  UNKNOWN,
+  /// The property was proven to be unreachable
+  NOT_REACHABLE,
+  /// The property was not violated
+  PASS,
+  /// The property was violated
+  FAIL,
+  /// An error occurred during goto checking
+  ERROR
+};
+
+enum class verifier_resultt
+{
+  UNKNOWN,
+  /// No properties were violated
+  PASS,
+  /// Some properties were violated
+  FAIL,
+  /// An error occurred during goto checking
+  ERROR
+};
+
+struct verification_resultt
+{
+  verification_resultt();
+  verification_resultt(const verification_resultt &other);
+  ~verification_resultt();
+  verification_resultt &operator=(verification_resultt &&);
+  verification_resultt &operator=(const verification_resultt &other);
+
+  void set_result(resultt &result);
+  void set_properties(propertiest &properties);
+
+  verifier_resultt final_result() const;
+  std::vector<std::string> get_property_ids() const;
+  std::string get_property_description(const std::string &property_id) const;
+  prop_statust get_property_status(const std::string &property_id) const;
+
+private:
+  class verification_result_implt;
+  std::unique_ptr<verification_result_implt> _impl;
+};
+
+#endif // CPROVER_GOTO_CHECKER_VERIFICATION_RESULT_H

unit/libcprover-cpp/test2.c

@@ -0,0 +1,8 @@
+// Input file to test reading through API, not for compiling!
+// Compared to test.c, this is supposed to have a passing assertion.
+
+int main(int argc, char *argv[])
+{
+  int arr[] = {0, 1, 2, 3, 4};
+  __CPROVER_assert(arr[3] == 3, "expected success: arr[3] to be 3");
+}