Expose CProver API version tag through to Rust API #7410
Conversation
NlightNFotis
force-pushed
the
expose_version_tag_to_rust
branch
from
4d9a81d to
7ba2cb7
Compare
cprover-cpp-api/src/api.h
Outdated
|
|
||
| // A simple API version information function. | ||
| // TODO: Investigate best way to store and expose version string. | ||
| std::string get_api_version() const { return std::string{"0.1"}; } |
There was a problem hiding this comment.
Is there some kind of advantage to versioning the API separately from the rest of CBMC? We could just return the CBMC_VERSION constant here.
NlightNFotis
force-pushed
the
expose_version_tag_to_rust
branch
from
7ba2cb7 to
cb26ef2
Compare
cprover-rust-api/src/lib.rs
Outdated
| let client = ffi::new_cprover_api(); | ||
| let result = ffi::get_api_version(client); | ||
| println!("{}", *result); | ||
| // assert_eq!(*result, "0.1"); |
There was a problem hiding this comment.
This is an older version of the code - we do assert now.
cprover-rust-api/build.rs
Outdated
| .flag_if_supported("-std=c++11") | ||
| .compile("cprover-rust-api"); | ||
|
|
||
| println!("cargo:rustc-link-search=native=/Users/fotiskoutoulakis/Devel/cbmc/build/lib/"); |
There was a problem hiding this comment.
Yes, yes - I'm aware. I will fix this once I rebase on top of some changes we expect to go in soon that will affect the C++ side of things, forcing some changes to this bit as well.
On the build side of thing, it will also need us to install a CMake module (corrosion) for building the Rust project along the C++ project, but I will do them both at the same time.
cprover-cpp-api/src/options.h
Outdated
| class api_optionst | ||
| { | ||
| // Options for the verification engine | ||
| bool simplify_enabled; |
There was a problem hiding this comment.
It's not exported to the Rust side yet - there's some thinking we need to do as to what's the best way to support some of these items (be they options that feed a verification-pipeline, or exported as calls that the user can then call when they want).
src/libcprover-rust/build.rs
Outdated
| println!("cargo:rerun-if-changed=src/c_api.cc"); | ||
| println!("cargo:rerun-if-changed=include/c_api.h"); | ||
|
|
||
| println!("cargo:rustc-link-search=native=/Users/fotiskoutoulakis/Devel/cbmc/build/lib/"); |
There was a problem hiding this comment.
hardcoded to your machine?
There was a problem hiding this comment.
Ditto as above - we expect to fix imminently.
NlightNFotis
force-pushed
the
expose_version_tag_to_rust
branch
6 times, most recently
from
d5754a3 to
e5a5041
Compare
NlightNFotis
requested review from
a team,
esteffin,
TGWDB,
peterschrammel,
kroening,
tautschnig and
chris-ryder
as code owners
|
|
||
| /// Validate the loaded goto model | ||
| void validate_goto_model(); | ||
| void validate_goto_model() const; |
There was a problem hiding this comment.
All of these are void. How do we expect to get back information about the result of validating the model?
| @@ -0,0 +1,2 @@ | |||
| # Ignore build artefacts folder | |||
| @@ -0,0 +1,15 @@ | |||
| [package] | |||
There was a problem hiding this comment.
Is the plan to publish this to crates.io
| type api_sessiont; | ||
|
|
||
| // API Functions | ||
| fn new_api_session() -> UniquePtr<api_sessiont>; |
There was a problem hiding this comment.
Was this manually written, or autogenerated?
| fn print_response(vec: &CxxVector<CxxString>) { | ||
| let vec: Vec<String> = vec | ||
| .iter() | ||
| .map(|s| s.to_string_lossy().into_owned()) |
There was a problem hiding this comment.
What encoding does CBMC use? Do we need this, or would to_str be sufficient?
| fn print_response(vec: &CxxVector<CxxString>) { | ||
| let vec: Vec<String> = vec | ||
| .iter() | ||
| .map(|s| s.to_string_lossy().into_owned()) |
There was a problem hiding this comment.
Why is into_owned needed? Is this an expectation of the API that ownership move here?
|
|
||
| // Invoke load_model_from_files and see if the model | ||
| // has been loaded. | ||
| client.load_model_from_files(vect); |
There was a problem hiding this comment.
How does this check that the loading happened?
| client.validate_goto_model(); | ||
|
|
||
| let msgs = ffi::get_messages(); | ||
| print_response(msgs); |
NlightNFotis
force-pushed
the
expose_version_tag_to_rust
branch
from
e5a5041 to
2a0f03b
Compare
Codecov ReportBase: 78.47% // Head: 78.48% // Increases project coverage by
Additional details and impacted files@@ Coverage Diff @@
## develop #7410 +/- ##
=========================================
Coverage 78.47% 78.48%
=========================================
Files 1662 1663 +1
Lines 191013 191188 +175
=========================================
+ Hits 149899 150054 +155
- Misses 41114 41134 +20
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. |
NlightNFotis
force-pushed
the
expose_version_tag_to_rust
branch
4 times, most recently
from
b58d496 to
2fb16b4
Compare
At the moment this supports the capacity for * loading a goto_model from files * verifying the goto_model * performing a sample instrumentation pass
NlightNFotis
force-pushed
the
expose_version_tag_to_rust
branch
from
2fb16b4 to
b566c4f
Compare
This for now sets up the build infrastructure, both in
CMake(to be able to build the Rust bit as part of a CBMC build) and inside of the Rust project, withcargo(so that API tests can be run independently - by just issuingcargo testinside thesrc/libcprover-rust/folder).It also exposes the functions from the C++ API to the Rust project, which exercises them through its own test suite.