Merge pull request #7410 from NlightNFotis/expose_version_tag_to_rust

Expose CProver API version tag through to Rust API

Author: NlightNFotis

CMakeLists.txt

@@ -256,4 +256,32 @@ if(WITH_JBMC)
     add_subdirectory(jbmc)
 endif()
 
+option(WITH_RUST_API "Build with the CPROVER Rust API" ON)
+if(${CMAKE_VERSION} VERSION_LESS "3.19.0")
+    message("Unable to build the Rust API without version CMake 3.19.0")
+    message("(The Rust build depends on CMake plugins with dependencies on CMake 3.19.0 and above)")
+else()
+    if(WITH_RUST_API)
+    include(FetchContent)
+
+    FetchContent_Declare(
+        Corrosion
+        GIT_REPOSITORY https://github.com/corrosion-rs/corrosion.git
+        GIT_TAG v0.3.1
+    )
+
+    FetchContent_MakeAvailable(Corrosion)
+
+    corrosion_import_crate(MANIFEST_PATH src/libcprover-rust/Cargo.toml)
+    corrosion_set_env_vars(cprover-api-rust CBMC_BUILD_DIR=${CMAKE_BINARY_DIR} SAT_IMPL=${sat_impl})
+    corrosion_link_libraries(cprover-api-rust cprover-api-cpp)
+    install(TARGETS cprover-api-rust RUNTIME DESTINATION lib)
+    # NOTE: We want to rename to a name consistent with the name of the
+    # rest of the static libraries built as a result of a build. The reason
+    # we cannot set the target name directly is that Cargo doesn't support
+    # hyphens in names of packages, so it builds the name by default with
+    # an underscore.
+    endif()
+endif()
+
 include(cmake/packaging.cmake)

src/libcprover-cpp/CMakeLists.txt

@@ -3,4 +3,21 @@ 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-checker goto-programs util langapi ansi-c)
+target_link_libraries(cprover-api-cpp 
+    goto-checker
+    goto-programs
+    util
+    langapi
+    ansi-c
+    json-symtab-language
+    solvers
+    xml
+    cpp
+    cbmc-lib
+    analyses
+    statement-list
+    linking
+    pointer-analysis
+    goto-instrument-lib
+    goto-analyzer-lib
+    goto-cc-lib)

src/libcprover-cpp/api.cpp

@@ -31,6 +31,11 @@
 
 extern configt config;
 
+std::unique_ptr<std::string> api_sessiont::get_api_version() const
+{
+  return util_make_unique<std::string>(std::string{"0.1"});
+}
+
 struct api_session_implementationt
 {
   std::unique_ptr<goto_modelt> model;
@@ -112,13 +117,14 @@ void api_sessiont::set_message_callback(
     util_make_unique<api_message_handlert>(callback, context);
 }
 
-void api_sessiont::load_model_from_files(const std::vector<std::string> &files)
+void api_sessiont::load_model_from_files(
+  const std::vector<std::string> &files) const
 {
   implementation->model = util_make_unique<goto_modelt>(initialize_goto_model(
     files, *implementation->message_handler, *implementation->options));
 }
 
-void api_sessiont::verify_model()
+void api_sessiont::verify_model() const
 {
   PRECONDITION(implementation->model);
 
@@ -162,7 +168,7 @@ void api_sessiont::verify_model()
   verifier.report();
 }
 
-void api_sessiont::drop_unused_functions()
+void api_sessiont::drop_unused_functions() const
 {
   INVARIANT(
     implementation->model != nullptr,
@@ -177,7 +183,7 @@ void api_sessiont::drop_unused_functions()
     *implementation->model, *implementation->message_handler);
 }
 
-void api_sessiont::validate_goto_model()
+void api_sessiont::validate_goto_model() const
 {
   INVARIANT(
     implementation->model != nullptr,

src/libcprover-cpp/api.h

@@ -66,16 +66,19 @@ struct api_sessiont
 
   /// Load a goto_model from a given vector of filenames.
   /// \param files: A vector<string> containing the filenames to be loaded
-  void load_model_from_files(const std::vector<std::string> &files);
+  void load_model_from_files(const std::vector<std::string> &files) const;
 
   /// Verify previously loaded model.
-  void verify_model();
+  void verify_model() const;
 
   /// Drop unused functions from the loaded goto_model simplifying it
-  void drop_unused_functions();
+  void drop_unused_functions() const;
 
   /// Validate the loaded goto model
-  void validate_goto_model();
+  void validate_goto_model() const;
+
+  // A simple API version information function.
+  std::unique_ptr<std::string> get_api_version() const;
 
 private:
   std::unique_ptr<api_session_implementationt> implementation;

src/libcprover-rust/.gitignore

@@ -0,0 +1,2 @@
+# Ignore build artefacts folder
+target/

src/libcprover-rust/Cargo.lock

@@ -0,0 +1,15 @@
+[package]
+name = "cprover-api-rust"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+cxx = "1.0"
+
+[build-dependencies]
+cxx-build = "1.0"
+
+[lib]
+crate-type = ["staticlib"]