Skip to content

Commit b3df1eb

Browse files
authored
Use our toolchain when invoking cargo metadata (#4090)
## Summary Change our invocation of `cargo metadata` to use Kani's toolchain. ## Explanation Kani uses the [cargo_metadata](https://crates.io/crates/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](https://doc.rust-lang.org/nightly/cargo/CHANGELOG.html#cargo-177-2024-03-21), so Kani, which is past 1.77, would expect the new version, and therefore can do this: https://github.com/model-checking/kani/blob/5d76510f8881153292124176d02300e6c13c2ffa/kani-driver/src/call_cargo.rs#L207 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.
1 parent 485d8e0 commit b3df1eb

File tree

2 files changed

+21
-1
lines changed

2 files changed

+21
-1
lines changed

kani-driver/src/call_cargo.rs

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,9 @@
44
use crate::args::VerificationArgs;
55
use crate::call_single_file::{LibConfig, to_rustc_arg};
66
use crate::project::Artifact;
7-
use crate::session::{KaniSession, lib_folder, lib_no_core_folder, setup_cargo_command};
7+
use crate::session::{
8+
KaniSession, get_cargo_path, lib_folder, lib_no_core_folder, setup_cargo_command,
9+
};
810
use crate::util;
911
use anyhow::{Context, Result, bail};
1012
use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
@@ -247,6 +249,10 @@ crate-type = ["lib"]
247249
pub fn cargo_metadata(&self, build_target: &str) -> Result<Metadata> {
248250
let mut cmd = MetadataCommand::new();
249251

252+
// Use Kani's toolchain when running `cargo metadata`
253+
let cargo_path = get_cargo_path().unwrap();
254+
cmd.cargo_path(cargo_path);
255+
250256
// restrict metadata command to host platform. References:
251257
// https://github.com/rust-lang/rust-analyzer/issues/6908
252258
// https://github.com/rust-lang/rust-analyzer/pull/6912

kani-driver/src/session.rs

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -439,3 +439,17 @@ pub fn setup_cargo_command() -> Result<Command> {
439439

440440
Ok(cmd)
441441
}
442+
443+
// Get the cargo path corresponding to the toolchain version in rust-toolchain.toml.
444+
// If kani is being run in developer mode, then we use the compile-time toolchain, i.e. the one used during cargo build-dev.
445+
// For release versions of Kani, we use a version of cargo that's in the toolchain that's been symlinked during `cargo-kani` setup.
446+
pub fn get_cargo_path() -> Result<PathBuf> {
447+
let install_type = InstallType::new()?;
448+
449+
let cargo_path = match install_type {
450+
InstallType::DevRepo(_) => env!("CARGO").into(),
451+
InstallType::Release(kani_dir) => kani_dir.join("toolchain").join("bin").join("cargo"),
452+
};
453+
454+
Ok(cargo_path)
455+
}

0 commit comments

Comments
 (0)