Skip to content

Conversation

carolynzech
Copy link
Contributor

Summary

Change our invocation of cargo metadata to use Kani's toolchain.

Explanation

Kani uses the cargo_metadata API to invoke cargo metadata. We were neglecting to override the Rust toolchain version with the one from our rust-toolchain.toml file, so the command would use the toolchain from the target crate. The issue is that Rust 1.77 stabilized the package id format, so Kani, which is past 1.77, would expect the new version, and therefore can do this:

.args(vec!["-p", &package.id.to_string()])

and know that the string representation of the package ID will work with -p. Pre-stabilization, Cargo made no such guarantees, so fetching the metadata with a pre 1.77 toolchain would return an id that's not compatible with the -p flag.

Resolves #3997

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@carolynzech
Copy link
Contributor Author

Thanks to @weihanglo for suggesting the CARGO environment variable!

@carolynzech carolynzech force-pushed the cargo-metadata-toolchain branch from 37fa819 to c314879 Compare May 20, 2025 15:37
@carolynzech
Copy link
Contributor Author

std::env::var didn't work; that pointed to s2n-quic's cargo. That's what's causing this bug in the first place; since we don't set cargo_path, cargo_metadata uses the CARGO env variable at runtime, which points to s2n-quic's toolchain instead of ours. So I changed the behavior to use env!("CARGO") on a development build, since we want to use the cargo that we compiled this code with, i.e. the one in Kani's rust-toolchain.toml. For release builds, we look in the symlinked toolchain, which is the same strategy we use in setup_cargo_command.

I tested this on s2n-quic locally and verified that it works on both development and release builds of Kani.

Development:

Kani Rust Verifier 0.62.0 (cargo plugin)
[kani-driver/src/call_cargo.rs:254:9] &cargo_path = "/Users/cmzech/.rustup/toolchains/nightly-2025-05-19-aarch64-apple-darwin/bin/cargo"

Release:

Kani Rust Verifier 0.63.0 (cargo plugin)
[kani-driver/src/call_cargo.rs:252:9] &cargo_path = "/Users/cmzech/.kani/kani-0.63.0/toolchain/bin/cargo"

(The 0.63.0 is because I built the test release bundle with that version; I wanted a sanity check that I was running the local release one and not the 0.62.0 from crates.io).

@carolynzech carolynzech marked this pull request as ready for review May 20, 2025 16:46
@carolynzech carolynzech requested a review from a team as a code owner May 20, 2025 16:46
@carolynzech carolynzech added this pull request to the merge queue May 23, 2025
Merged via the queue into model-checking:main with commit b3df1eb May 23, 2025
26 checks passed
@carolynzech carolynzech deleted the cargo-metadata-toolchain branch May 23, 2025 13:35
github-merge-queue bot pushed a commit that referenced this pull request Jun 9, 2025
These are the automatically-generated release notes:
```
## What's Changed
* Toolchain upgrade to nightly-2025-05-04 by @thanhnguyen-aws in #4059
* Automatic toolchain upgrade to nightly-2025-05-05 by @github-actions in #4060
* Automatic toolchain upgrade to nightly-2025-05-06 by @github-actions in #4061
* Enable target features: x87 and sse2 by @thanhnguyen-aws in #4062
* Fix the bug: Loop contracts are not composable with function contracts  by @thanhnguyen-aws in #3979
* Automatic cargo update to 2025-05-12 by @github-actions in #4066
* Bump tests/perf/s2n-quic from `6aa9975` to `5f323b7` by @dependabot in #4068
* Fix stabilization instructions in RFC intro by @carolynzech in #4067
* Add support for quantifiers by @qinheping in #3993
* Toolchain upgrade to nightly-2025-05-07 by @thanhnguyen-aws in #4070
* Automatic toolchain upgrade to nightly-2025-05-08 by @github-actions in #4071
* Automatic toolchain upgrade to nightly-2025-05-09 by @github-actions in #4072
* Automatic toolchain upgrade to nightly-2025-05-10 by @github-actions in #4073
* Clippy/Stylistic Fixes by @carolynzech in #4074
* Upgrade toolchain to 2025-05-14 by @zhassan-aws in #4076
* Autoharness argument validation: only error on `--quiet` if `--list` was passed by @carolynzech in #4069
* Upgrade Rust toolchain to 2025-05-16 by @zhassan-aws in #4080
* Automatic toolchain upgrade to nightly-2025-05-17 by @github-actions in #4081
* Add setup scripts for Ubuntu 20.04 by @zhassan-aws in #4082
* Automatic toolchain upgrade to nightly-2025-05-18 by @github-actions in #4083
* Automatic cargo update to 2025-05-19 by @github-actions in #4086
* Automatic toolchain upgrade to nightly-2025-05-19 by @github-actions in #4085
* Automatic toolchain upgrade to nightly-2025-05-20 by @github-actions in #4091
* Bump tests/perf/s2n-quic from `5f323b7` to `22434aa` by @dependabot in #4089
* Fix the error that Kani panics when there is no external parameter in quantifier's closure. by @thanhnguyen-aws in #4088
* Update toolchain to 2025-05-22 by @carolynzech in #4098
* Use our toolchain when invoking `cargo metadata` by @carolynzech in #4090
* Automatic toolchain upgrade to nightly-2025-05-23 by @github-actions in #4099
* Automatic toolchain upgrade to nightly-2025-05-24 by @github-actions in #4101
* Automatic toolchain upgrade to nightly-2025-05-25 by @github-actions in #4102
* Fix a bug codegening `SwitchInt`s with only an otherwise branch by @bkirwi in #4095
* Automatic toolchain upgrade to nightly-2025-05-26 by @github-actions in #4104
* Automatic cargo update to 2025-05-26 by @github-actions in #4105
* Bump tests/perf/s2n-quic from `22434aa` to `550afb3` by @dependabot in #4106
* Automatic toolchain upgrade to nightly-2025-05-27 by @github-actions in #4107
* Update `kani::mem` pointer validity documentation by @carolynzech in #4092
* Add support for edition 2018 crates using assert! (Fixes #3717) by @sintemal in #4096
* Automatic toolchain upgrade to nightly-2025-05-28 by @github-actions in #4113
* Automatic toolchain upgrade to nightly-2025-05-29 by @github-actions in #4115
* Automatic toolchain upgrade to nightly-2025-05-30 by @github-actions in #4118
* Handle generic defaults in BoundedArbitrary derives by @zhassan-aws in #4117
* Automatic cargo update to 2025-06-02 by @github-actions in #4121
* Bump tests/perf/s2n-quic from `550afb3` to `8f54b57` by @dependabot in #4122
* Upgrade Rust toolchain to 2025-06-02 by @zhassan-aws in #4123
* Automatic toolchain upgrade to nightly-2025-06-03 by @github-actions in #4125
* Finish deprecating `--enable-unstable`, `--restrict-vtable`, and `--write-json-symtab` by @carolynzech in #4110
* `ty_mangled_name`: only use non-mangled name if `-Zcffi` is enabled. by @carolynzech in #4114
* Improve Help Menu by @carolynzech in #4109
* Start stabilizing `--jobs` and `list`; deprecate default memory checks by @carolynzech in #4108
* Refactor simd_bitmask to reduce the number of iterations by @zhassan-aws in #4129
* Set target features depending on the target architecture by @zhassan-aws in #4127
* Bump some versions suggested by cargo-outdated by @zhassan-aws in #4131
* Improve linking error output for `#[no_std]` crates by @AlexanderPortland in #4126
* Fix the git log command in the toolchain update script by @zhassan-aws in #4139
* Gate quantifiers behind an experimental feature by @thanhnguyen-aws in #4141
* Automatic cargo update to 2025-06-09 by @github-actions in #4145

## New Contributors
* @bkirwi made their first contribution in #4095
* @sintemal made their first contribution in #4096
* @AlexanderPortland made their first contribution in #4126

**Full Changelog**: kani-0.62.0...kani-0.63.0
```


By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Carolyn Zech <carolynzech@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Kani fails on s2n-quic
3 participants