Rust crate preparation - final touches #7625

NlightNFotis · 2023-03-28T16:14:28Z

This is the final PR before we publish the crate on crates.io.

Have slightly improved docs, build and added a test to verify that our translation
of C++ exceptions to Rust Result types work.

cargo test, cargo build, cargo doc and cargo publish --dry-run all work at this point.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

…esult types.

… internal headers

`other/` contains a C smoke test file, that we need to include so that a user of the crate can actually test the crate without getting errors related to lack of the file.

… docs

…ory. The build requirements have failed, and any other changes are very *very* brittle, as they require downloading a CBMC package (so that an `include/cprover/` folder is present), knowing the version and the location of the folder, and that will also fail on the release PRs incrementing the version (as the packaged versions and the reported version are going to be divergent).

codecov · 2023-03-28T17:11:20Z

Codecov Report

Patch and project coverage have no change.

Comparison is base (b34e991) 78.50% compared to head (8ca2615) 78.50%.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #7625   +/-   ##
========================================
  Coverage    78.50%   78.50%           
========================================
  Files         1671     1671           
  Lines       191847   191847           
========================================
  Hits        150618   150618           
  Misses       41229    41229

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

TGWDB · 2023-03-28T17:19:40Z

src/libcprover-rust/readme.md

@@ -27,7 +29,7 @@ directory of the CBMC project.)
 ```sh
 $ cd src/libcprover-rust
 $ cargo clean
-$ CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo build
+$ CBMC_INCLUDE_DIR=../../build/include CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo build


Maybe don't fix a version of CBMC here, use something like CBMC_VERSION=X.XX.X?

This is in the documentation, and I meant it as a concrete example.

Should I still change this? Perhaps a good middle ground might be to add a reference to the version schema in the description of the environment variable, starting in line 19.

I'm agnostic on it. On the one hand I can see someone simply copying and pasting, on the other hand a concrete example is nicer than one with further things to modify.

TGWDB · 2023-03-28T17:19:47Z

src/libcprover-rust/readme.md

@@ -36,7 +38,118 @@ look like this:
 ```sh
 $ cd src/libcprover-rust
 $ cargo clean
-$ CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo test -- --test-threads=1 --nocapture
+$ CBMC_INCLUDE_DIR=../../build/include CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo test -- --test-threads=1 --nocapture


TGWDB · 2023-03-28T21:34:59Z

src/libcprover-rust/readme.md

@@ -27,7 +29,7 @@ directory of the CBMC project.)
 ```sh
 $ cd src/libcprover-rust
 $ cargo clean
-$ CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo build
+$ CBMC_INCLUDE_DIR=../../build/include CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo build


I'm agnostic on it. On the one hand I can see someone simply copying and pasting, on the other hand a concrete example is nicer than one with further things to modify.

TGWDB · 2023-03-28T21:40:07Z

src/libcprover-rust/include/c_errors.h

-// those), and so because of the mechanism that cxx.rs uses, we need to have the
-// types present at compilation time (an incomplete type won't do - I've tried).
+// At the same time, we want to allow the Rust API to be able to catch at the
+// shimlevel the errors generated within CBMC, which are C++ types (and


shimlevel -> shim level

TGWDB · 2023-03-28T21:43:21Z

src/libcprover-rust/src/lib.rs

+
+        // The vector of string is supposed to contain a string denoting
+        // a filepath that is erroneous.
+        let vec: Vec<String> = vec!["/fkjsdlkjfisudifoj2309".to_owned()];


I have not tried to break this, but what happens if I have a valid input file at /fkjsdlkjfisudifoj2309? I'm also curious if the / is OS specific to any degree?

Well, that was my best attempt at making a random string + file path combo, without resorting to a more elaborate mechanism based on random strings or whatnot.

I'm personally happy with it failing if a user does have a randomly (?) named file locally present. If that happens, the user/developer can just have a look at the test, and see that we are looking for this file, inspect his filesystem and locate the file, and potentially alter the test/delete the file.

NlightNFotis added 6 commits March 28, 2023 16:15

Add a unit test for catching exceptions from C++ and returning Rust R…

761d62e

…esult types.

Include exception base classes in separate file to avoid depending on…

e95ce4e

… internal headers

Remove other/ from exclusion list for package code.

ac02ab8

`other/` contains a C smoke test file, that we need to include so that a user of the crate can actually test the crate without getting errors related to lack of the file.

Add environment variable for include folder in build and update build…

850e941

… docs

Fold tutorial into readme.md and move readme into top-level docs

a13c4ab

NlightNFotis requested review from a team, thomasspriggs, TGWDB and peterschrammel as code owners March 28, 2023 16:14

NlightNFotis self-assigned this Mar 28, 2023

Fix linting issues

8ca2615

NlightNFotis force-pushed the rust_api_crate_preparation branch from d9e315f to 8ca2615 Compare March 28, 2023 16:47

TGWDB reviewed Mar 28, 2023

View reviewed changes

TGWDB approved these changes Mar 28, 2023

View reviewed changes

NlightNFotis merged commit 378c902 into diffblue:develop Mar 29, 2023

NlightNFotis deleted the rust_api_crate_preparation branch March 29, 2023 09:14

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Rust crate preparation - final touches #7625

Rust crate preparation - final touches #7625

Uh oh!

NlightNFotis commented Mar 28, 2023

Uh oh!

codecov bot commented Mar 28, 2023 •

edited

Loading

Uh oh!

TGWDB Mar 28, 2023

Uh oh!

NlightNFotis Mar 28, 2023

Uh oh!

TGWDB Mar 28, 2023

Uh oh!

TGWDB Mar 28, 2023

Uh oh!

TGWDB Mar 28, 2023

Uh oh!

TGWDB Mar 28, 2023

Uh oh!

TGWDB Mar 28, 2023

Uh oh!

NlightNFotis Mar 29, 2023

Uh oh!

Uh oh!

Rust crate preparation - final touches #7625

Rust crate preparation - final touches #7625

Uh oh!

Conversation

NlightNFotis commented Mar 28, 2023

Uh oh!

codecov bot commented Mar 28, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov bot commented Mar 28, 2023 •

edited

Loading