Translate exceptions from C++ API into Rust `Result` types. #7511

NlightNFotis · 2023-02-01T10:35:07Z

This PR is adding the capacity to the Rust API to translate exceptions from C++'s
end into Rust Result types that make handling of exceptions more robust and
ergonomic.

The last commit is not strictly related to the PR (it's a format using cargo fmt),
but I hadn't run it against this project yet, so this is including it so that it
starts being formatted and consistent with rust fmt.

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.

codecov · 2023-02-01T11:32:21Z

Codecov Report

Base: 78.50% // Head: 78.32% // Decreases project coverage by -0.18% ⚠️

Coverage data is based on head (3aa2b65) compared to base (4a5c1f9).
Patch has no changes to coverable lines.

❗ Current head 3aa2b65 differs from pull request most recent head f9da9dc. Consider uploading reports for the commit f9da9dc to get more accurate results

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7511      +/-   ##
===========================================
- Coverage    78.50%   78.32%   -0.18%     
===========================================
  Files         1663     1663              
  Lines       191297   191297              
===========================================
- Hits        150174   149830     -344     
- Misses       41123    41467     +344

Impacted Files	Coverage Δ
src/util/type.cpp	`27.27% <0.00%> (-45.46%)`	⬇️
src/util/symbol_table.cpp	`48.91% <0.00%> (-42.40%)`	⬇️
src/util/validate_expressions.cpp	`56.25% <0.00%> (-37.50%)`	⬇️
src/util/timestamper.h	`33.33% <0.00%> (-33.34%)`	⬇️
src/util/ui_message.h	`55.55% <0.00%> (-33.34%)`	⬇️
src/util/cout_message.cpp	`55.55% <0.00%> (-29.63%)`	⬇️
src/big-int/bigint.cc	`61.81% <0.00%> (-27.20%)`	⬇️
src/util/ssa_expr.cpp	`69.90% <0.00%> (-24.28%)`	⬇️
src/util/string_container.h	`81.81% <0.00%> (-18.19%)`	⬇️
src/util/validate_types.cpp	`76.66% <0.00%> (-16.67%)`	⬇️
... and 18 more

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 at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

TGWDB · 2023-02-01T12:58:42Z

src/libcprover-rust/src/lib.rs

@@ -119,10 +131,18 @@ mod tests {
        let vect = ffi::translate_vector_of_string(vec);
        assert_eq!(vect.len(), 1);

-        client.load_model_from_files(vect);
+        if let Err(_) = client.load_model_from_files(vect) {
+            println!("Panicking: load_model_from_files_failed");


Why does this one panic, but not others?

This is experimental code that I failed to remove 🤦🏻‍♂️

Technically, when an assert! macro fails, it calls panic! - I wanted to simulate this behaviour manually (or at least approximate part of it) and then I forgot to remove it.

TGWDB · 2023-02-01T12:59:18Z

src/libcprover-rust/include/c_api.h

+      } catch (const cprover_exception_baset &e) {
+        fail(e.what());
+      } catch (const invariant_failedt &i) {
+        fail(i.what());


I thought we had preferred project style to use longer and clearer names than e and i.

TGWDB · 2023-02-01T12:59:33Z

src/libcprover-rust/src/lib.rs


+        println!("Just before we print the messages");


Leftover debug code?

Yeah, this was removed in the next commit.

TGWDB · 2023-02-01T13:07:25Z

src/libcprover-rust/src/lib.rs

+        let validation_msg = "Validating consistency of goto-model supplied to API session";
        let msgs = ffi::get_messages();
-        print_response(msgs);
+        let msgs_assert = translate_response_buffer(msgs).clone();
+
+        assert!(msgs_assert.contains(&String::from(validation_msg)));


I recognise this is in test code and so not that significant, but it would be much nicer if validate_goto_model() actually returned a useful value instead of needing to string match over a collection of strings.

Yeah, this is very hard to do right now - the C++ API returns void, and that's also because the function it's delegating to, validate_goto_model in src/goto-programs/validate_goto_model.cpp:128 is also void.

This will require some deep refactoring for these to behave this way.

The assertions I have added are along the lines of "Test for behaviour - not interface", which are just making sure that a side-effect of the action has been performed accurately.

Not terribly robust tests, but better than nothing - until at least a better interface presents itself.

Understood that this is test code and proper result structures are future work.

TGWDB · 2023-02-01T13:08:48Z

src/libcprover-rust/src/lib.rs

+        let verification_msg = "VERIFICATION FAILED";
+
        let msgs = ffi::get_messages();
-        print_response(msgs);
+        let msgs_assert = translate_response_buffer(msgs).clone();
+
+        assert!(msgs_assert.contains(&String::from(verification_msg)));


As above, better to get something useful back.

…of print

NlightNFotis added Kani Bugs or features of importance to Kani Rust Verifier Rust API Issues pertaining to the CBCM Rust API labels Feb 1, 2023

NlightNFotis requested review from kroening, tautschnig and peterschrammel as code owners February 1, 2023 10:35

NlightNFotis self-assigned this Feb 1, 2023

NlightNFotis requested a review from chris-ryder as a code owner February 1, 2023 10:35

NlightNFotis linked an issue Feb 1, 2023 that may be closed by this pull request

Handling of exceptions in the new Rust API #7490

Closed

TGWDB reviewed Feb 1, 2023

View reviewed changes

NlightNFotis force-pushed the rust_api_exceptions_to_results branch from 3aa2b65 to fd6e3ec Compare February 1, 2023 14:40

Add translation of CBMC exceptions to the Rust Result type

449e22f

NlightNFotis force-pushed the rust_api_exceptions_to_results branch from fd6e3ec to 99f0370 Compare February 1, 2023 14:42

TGWDB approved these changes Feb 1, 2023

View reviewed changes

Add documentation for helper functions and make tests assert instead …

f9da9dc

…of print

NlightNFotis force-pushed the rust_api_exceptions_to_results branch from 99f0370 to f9da9dc Compare February 2, 2023 15:31

NlightNFotis requested a review from thomasspriggs as a code owner February 2, 2023 15:31

NlightNFotis merged commit c3024c6 into diffblue:develop Feb 2, 2023

NlightNFotis deleted the rust_api_exceptions_to_results branch February 2, 2023 17:05

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Translate exceptions from C++ API into Rust `Result` types. #7511

Translate exceptions from C++ API into Rust `Result` types. #7511

Uh oh!

NlightNFotis commented Feb 1, 2023

Uh oh!

codecov bot commented Feb 1, 2023 •

edited

Loading

Uh oh!

TGWDB Feb 1, 2023

Uh oh!

NlightNFotis Feb 1, 2023

Uh oh!

TGWDB Feb 1, 2023

Uh oh!

TGWDB Feb 1, 2023

Uh oh!

NlightNFotis Feb 1, 2023

Uh oh!

TGWDB Feb 1, 2023

Uh oh!

NlightNFotis Feb 1, 2023

Uh oh!

TGWDB Feb 1, 2023

Uh oh!

TGWDB Feb 1, 2023

Uh oh!

Uh oh!

Translate exceptions from C++ API into Rust Result types. #7511

Translate exceptions from C++ API into Rust Result types. #7511

Uh oh!

Conversation

NlightNFotis commented Feb 1, 2023

Uh oh!

codecov bot commented Feb 1, 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!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Translate exceptions from C++ API into Rust `Result` types. #7511

Translate exceptions from C++ API into Rust `Result` types. #7511

codecov bot commented Feb 1, 2023 •

edited

Loading