Exposure of Rust API as a crates.io crate

[NlightNFotis]

(This item is to track feature development across the new Rust API for CBMC)

The Rust API for CBMC is now at the point where it can be built as part of the CBMC build, and its code has been integrated in the CBMC source tree (#7410 has been the work that covered this).

The next bit is to expose the crate in a way that integrates better with other Rust programs, i.e. exposing it as a crate to crates.io.

[NlightNFotis]

Hello,

I have been thinking about how best to structure the upcoming crate for the Rust API of CBMC.

Some Background

The build process of the Rust API we expose depends on knowing where the libraries it needs to link to (which are the various modules of CBMC in statically linked library format, e.g. build/lib/libgoto-programs.a) are located. This information is controlled by the CMake integration on our CBMC builds, and when we need to link to them outside of the CMake build (say, when running cargo test) we need to pass the location of these libraries in an environment variable.

Unfortunately, because of the structure of our build system, the names of the static libraries that we produce directly reflect the various modules (subdirectories) of CBMC, so we end up with some that have pretty generic names like libgcc.a or libcpp.a or libxml.a. It is hardly going to get us any favours if we install these on a user's system (because these may clash with other libraries of similar naming schemes but greater functional generality) and may create issues linking at user's machines. For this reason, our packages include our binaries, but not the precompiled static libraries that we produce.

Potential Solutions

I am outlining here a number of potential solutions to the issue described above, in the interest of API integrators, like the team working on Kani.

First Solution (Default): Rebuild CBMC and link Rust API against lib artefacts

This would be more or less emulating the state of the building of CBMC/Rust API as they are handled upstream (i.e. by us). What this means for usage and integration of the Rust API is that a build of CBMC (without the Rust API on) should be performed before any build of a consumer (say Kani).

The consumer's build process will then need to pass in the prerequisite local libraries path (something like cbmc/build/lib) as an environment variable to the build of the consumer, which is going to be consumed by our Rust API's build script to locate the libraries to link against.

This solution would offer the following benefits:

• Easy control of CBMC version (git checkout) would allow for quick relinking against other CBMC versions.
• Low maintenance load on both sides of the API.

But it would also suffer from the following drawbacks:

• The consumer's (e.g. Kani) build now has an implicit dependency on a build of CBMC - this might require more time in CI or a bit of extra complexity around the consumer's build.
  • Worth noting: A build (no tests) of CBMC in Github Actions takes around 10-15mins, but it's very amenable to caching. We can provide some guidance as to how this can go about, or the solution used by CBMC could be directly copied.

Alternative Solution: Bundle CBMC's module in a static library to be passed during linking

A potential alternative might be to bundle all of the static libraries into just one (for example a single artefact called libcbmc.a) that might then be a part of the packages that we produce and come pre-installed in the user's computer during the Rust APIs linking. This would allow for a cleaner build from our end, because compared to the static library linking in our build script, we would just have a links entry in our Cargo.toml and that would handle everything.

This solution has certain benefits:

• This allows for a potentially easier build for the consumers (as you now only have a binary dependency which might come preinstalled in your system).
• No time spent building all of CBMC during consumer's build.

But it also affords a certain amount of drawbacks:

• Versioning a static library that comes pre-installed in the system and having this version information interact with the build script may be as messy as the current solution.
• Because of the structure of our current build system, this would require ~a terrible hack ~ a less than elegant solution, which we would need to get back to and improve upon so that we can get our build system to be more dependable overall.
  • This won't be noticed by the consumers in terms of integration - in fact nothing would change there.
  • But it also implies that we would need to spend some development time improving the build, with the understanding that this improves integration reliability but no functional improvement on the API itself.

Alternative 2: Rename static libraries into prefixed names

This would simply be a step during the build which would attach a CBMC-specific prefix to all of the static libraries. This would allow us to install them to user's computers without necessarily polluting their local linking paths with libraries that might produce linking errors for their apps. This would mean that instead of libcpp.a we would install something like libcbmc-cpp.a - not a very clean solution, but potentially workable without any issues.

This would come with the following benefits:

• Fastest potential integration point for consumers - just make sure that a package containing those has been pre-installed.

But it would also have a certain number of defects:

• Version management of these is going to become slightly problematic - may require uninstalling a CBMC package and then installing another one.
• We are polluting the user's load paths with a number of fairly niche static libraries that are useful for only one program.
  • This is primarily an efficiency/aesthetic issue - it would be about the same thing if we had a single library that comes pre-installed, only that there wouldn't be so many static libraries because they would have all been folded into one.

Conclusion

I'm presenting the above in hope that these provide some insight to integrators of the API so that the alternatives can be evaluated and ordered from most appealing to least appealing.

[danielsn]

We discussed, and "Alternative Solution: Bundle CBMC's module in a static library to be passed during linking" was the preference of the team. One question: what is the difficulty in versioning this library (e.g. why not just have libcbmc-5-75.a)?

Few questions:

1. Do you have a sense how large this library would be?
2. Do you have a sense of how much of this library would be necessary to Kani? Could we strip symbols and save space?
3. Are there best practices for doing this on crates.io? Do you have examples of the various approaches in practice?

[NlightNFotis]

Hi @danielsn, I did some digging into and I can provide answers to at least the first two questions:

In my experiments on my local machine (MacOS) it seems that I can get a libcbmc.a which by default is 1.2GiB - that can be stripped down to 319MiB if symbols are removed.

If we go about this way, the static library is going to be part of the release artefacts and is going to be installed by a package manager before any engagement with the Rust API of CBMC.

For question 3 - I don't have easily accessible examples. I will research those a bit more and get back to you.

[NlightNFotis]

@feliperodri This is the issue I was talking about in our meeting.

Let me know if there are any questions about the status update so far.

[NlightNFotis]

The crate is now live at https://crates.io/crates/libcprover_rust

I did manage to create a new project and download and link from the crate. I would encourage people to start playing with it, and let us know if there are any issues with it or any feature requests pop up.

This was marked version 0.1.0 to allow for some experimentation and potential "yanking" of the package if it was found to be problematic.

Tomorrow we will be releasing CBMC 5.80.0, so the version of the API will be brought in sync with CBMC's version and kept in sync from that point onwards for every release.