From 7b886f9988359a3388c53afbc2ddd2a16c19e75b Mon Sep 17 00:00:00 2001 From: jaisnan Date: Mon, 4 Mar 2024 14:35:11 +0000 Subject: [PATCH 1/8] Add --use-local-toolchain w/o changes to cargo --- .gitignore | 1 + Cargo.lock | 76 +++++++++++++++++++++++++++++++++++++--- Cargo.toml | 1 + kani-compiler/build.rs | 2 ++ src/lib.rs | 79 +++++++++++++++++++++++++++++++----------- src/setup.rs | 19 +++++++--- 6 files changed, 147 insertions(+), 31 deletions(-) diff --git a/.gitignore b/.gitignore index a31c86965494..a4cfe4ff4e2b 100644 --- a/.gitignore +++ b/.gitignore @@ -16,6 +16,7 @@ desktop.ini Session.vim .cproject .idea +toolchains/ *.iml .vscode .project diff --git a/Cargo.lock b/Cargo.lock index 434c0e7bb330..708f0690067f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -33,6 +33,15 @@ dependencies = [ "memchr", ] +[[package]] +name = "ansi_term" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2" +dependencies = [ + "winapi", +] + [[package]] name = "anstream" version = "0.6.12" @@ -87,6 +96,17 @@ version = "1.0.80" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5ad32ce52e4161730f7098c077cd2ed6229b5804ccf99e5366be1ab72a98b4e1" +[[package]] +name = "atty" +version = "0.2.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8" +dependencies = [ + "hermit-abi", + "libc", + "winapi", +] + [[package]] name = "autocfg" version = "1.1.0" @@ -125,7 +145,7 @@ version = "0.47.0" dependencies = [ "anyhow", "cargo_metadata", - "clap", + "clap 4.5.1", "which", ] @@ -167,6 +187,21 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" +[[package]] +name = "clap" +version = "2.34.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a0610544180c38b88101fecf2dd634b174a62eef6946f84dfc6a7127512b381c" +dependencies = [ + "ansi_term", + "atty", + "bitflags 1.3.2", + "strsim 0.8.0", + "textwrap", + "unicode-width", + "vec_map", +] + [[package]] name = "clap" version = "4.5.1" @@ -186,7 +221,7 @@ dependencies = [ "anstream", "anstyle", "clap_lex", - "strsim", + "strsim 0.11.0", ] [[package]] @@ -392,6 +427,15 @@ version = "0.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8" +[[package]] +name = "hermit-abi" +version = "0.1.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33" +dependencies = [ + "libc", +] + [[package]] name = "home" version = "0.5.9" @@ -437,7 +481,7 @@ dependencies = [ name = "kani-compiler" version = "0.47.0" dependencies = [ - "clap", + "clap 4.5.1", "cprover_bindings", "home", "itertools", @@ -460,7 +504,7 @@ version = "0.47.0" dependencies = [ "anyhow", "cargo_metadata", - "clap", + "clap 4.5.1", "comfy-table", "console", "glob", @@ -487,6 +531,7 @@ name = "kani-verifier" version = "0.47.0" dependencies = [ "anyhow", + "clap 2.34.0", "home", "os_info", ] @@ -505,7 +550,7 @@ dependencies = [ name = "kani_metadata" version = "0.47.0" dependencies = [ - "clap", + "clap 4.5.1", "cprover_bindings", "serde", "strum 0.26.1", @@ -1050,6 +1095,12 @@ dependencies = [ "serde", ] +[[package]] +name = "strsim" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a" + [[package]] name = "strsim" version = "0.11.0" @@ -1127,6 +1178,15 @@ dependencies = [ "windows-sys", ] +[[package]] +name = "textwrap" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d326610f408c7a4eb6f51c37c330e496b08506c9457c9d34287ecc38809fb060" +dependencies = [ + "unicode-width", +] + [[package]] name = "thiserror" version = "1.0.57" @@ -1305,6 +1365,12 @@ version = "0.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "830b7e5d4d90034032940e4ace0d9a9a057e7a45cd94e6c007832e39edb82f6d" +[[package]] +name = "vec_map" +version = "0.8.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191" + [[package]] name = "version_check" version = "0.9.4" diff --git a/Cargo.toml b/Cargo.toml index b842bf8fbf0e..845751118363 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -19,6 +19,7 @@ include = ["/src", "/build.rs", "/rust-toolchain.toml", "/LICENSE-*", "/README.m [dependencies] anyhow = "1" home = "0.5" +clap = "2.33.3" os_info = { version = "3", default-features = false } [[bin]] diff --git a/kani-compiler/build.rs b/kani-compiler/build.rs index 37a9471a167d..497e9dfa13d2 100644 --- a/kani-compiler/build.rs +++ b/kani-compiler/build.rs @@ -20,6 +20,8 @@ macro_rules! path_str { /// kani-compiler with nightly only. We also link to the rustup rustc_driver library for now. pub fn main() { // Add rustup to the rpath in order to properly link with the correct rustc version. + + // This is for dev purposes only, if dev point/search toolchain in .rustup/toolchains/ let rustup_home = env::var("RUSTUP_HOME").unwrap(); let rustup_tc = env::var("RUSTUP_TOOLCHAIN").unwrap(); let rustup_lib = path_str!([&rustup_home, "toolchains", &rustup_tc, "lib"]); diff --git a/src/lib.rs b/src/lib.rs index 9a1ac90f5dda..87db3337e85a 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -16,6 +16,7 @@ mod cmd; mod os_hacks; mod setup; +use clap::{App, Arg, SubCommand}; use std::ffi::OsString; use std::os::unix::prelude::CommandExt; use std::path::{Path, PathBuf}; @@ -28,16 +29,16 @@ use anyhow::{bail, Context, Result}; /// `bin` should be either `kani` or `cargo-kani` pub fn proxy(bin: &str) -> Result<()> { match parse_args(env::args_os().collect()) { - ArgsResult::ExplicitSetup { use_local_bundle } => setup::setup(use_local_bundle), + ArgsResult::ExplicitSetup { use_local_bundle, use_local_toolchain } => setup::setup(use_local_bundle, use_local_toolchain), ArgsResult::Default => { fail_if_in_dev_environment()?; if !setup::appears_setup() { - setup::setup(None)?; + setup::setup(None, None)?; } else { // This handles cases where the setup was left incomplete due to an interrupt // For example - https://github.com/model-checking/kani/issues/1545 if let Some(path_to_bundle) = setup::appears_incomplete() { - setup::setup(Some(path_to_bundle.clone().into_os_string()))?; + setup::setup(Some(path_to_bundle.clone().into_os_string()), None)?; // Suppress warning with unused assignment // and remove the bundle if it still exists let _ = fs::remove_file(path_to_bundle); @@ -51,28 +52,52 @@ pub fn proxy(bin: &str) -> Result<()> { /// Minimalist argument parsing result type #[derive(PartialEq, Eq, Debug)] enum ArgsResult { - ExplicitSetup { use_local_bundle: Option }, + ExplicitSetup { use_local_bundle: Option, use_local_toolchain: Option}, Default, } /// Parse `args` and decide what to do. fn parse_args(args: Vec) -> ArgsResult { - // In an effort to keep our dependencies minimal, we do the bare minimum argument parsing manually. - // `args_ez` makes it easy to do crude arg parsing with match. - let args_ez: Vec> = args.iter().map(|x| x.to_str()).collect(); - // "cargo kani setup" comes in as "cargo-kani kani setup" - // "cargo-kani setup" comes in as "cargo-kani setup" - match &args_ez[..] { - &[_, Some("setup"), Some("--use-local-bundle"), _] => { - ArgsResult::ExplicitSetup { use_local_bundle: Some(args[3].clone()) } - } - &[_, Some("kani"), Some("setup"), Some("--use-local-bundle"), _] => { - ArgsResult::ExplicitSetup { use_local_bundle: Some(args[4].clone()) } - } - &[_, Some("setup")] | &[_, Some("kani"), Some("setup")] => { - ArgsResult::ExplicitSetup { use_local_bundle: None } + let matches = App::new("kani") + .subcommand( + SubCommand::with_name("setup") + .arg(Arg::with_name("use-local-bundle").long("use-local-bundle").takes_value(true)) + .arg( + Arg::with_name("use-local-toolchain") + .long("use-local-toolchain") + .takes_value(true), + ), + ) + .subcommand( + SubCommand::with_name("kani") + .subcommand( + SubCommand::with_name("setup") + .arg(Arg::with_name("use-local-bundle").long("use-local-bundle").takes_value(true)) + .arg( + Arg::with_name("use-local-toolchain") + .long("use-local-toolchain") + .takes_value(true), + ), + ), + ) + .get_matches_from(args); + + // Default is the behaviour for Kani when cargo-kani/ cargo kani runs on its own and sees that there is no setup done yet + // Explicit is when the user uses the sub-command cargo-kani setup explicitly + if let Some(matches) = matches.subcommand_matches("setup") { + let use_local_toolchain = matches.value_of_os("use-local-toolchain").map(OsString::from); + let use_local_bundle = matches.value_of_os("use-local-bundle").map(OsString::from); + ArgsResult::ExplicitSetup { use_local_bundle: use_local_bundle, use_local_toolchain: use_local_toolchain } + } else if let Some(matches) = matches.subcommand_matches("kani") { + if let Some(matches) = matches.subcommand_matches("setup") { + let use_local_toolchain = matches.value_of_os("use-local-toolchain").map(OsString::from); + let use_local_bundle = matches.value_of_os("use-local-bundle").map(OsString::from); + ArgsResult::ExplicitSetup { use_local_bundle: use_local_bundle, use_local_toolchain: use_local_toolchain } + } else { + ArgsResult::Default } - _ => ArgsResult::Default, + } else { + ArgsResult::Default } } @@ -223,16 +248,28 @@ mod tests { assert_eq!(e, trial(&[])); } { - let e = ArgsResult::ExplicitSetup { use_local_bundle: None }; + let e = ArgsResult::ExplicitSetup { use_local_bundle: None, use_local_toolchain: None }; assert_eq!(e, trial(&["cargo-kani", "kani", "setup"])); assert_eq!(e, trial(&["cargo", "kani", "setup"])); assert_eq!(e, trial(&["cargo-kani", "setup"])); } { - let e = ArgsResult::ExplicitSetup { use_local_bundle: Some(OsString::from("FILE")) }; + let e = ArgsResult::ExplicitSetup { use_local_bundle: Some(OsString::from("FILE")), use_local_toolchain: None }; assert_eq!(e, trial(&["cargo-kani", "kani", "setup", "--use-local-bundle", "FILE"])); assert_eq!(e, trial(&["cargo", "kani", "setup", "--use-local-bundle", "FILE"])); assert_eq!(e, trial(&["cargo-kani", "setup", "--use-local-bundle", "FILE"])); } + { + let e = ArgsResult::ExplicitSetup { use_local_bundle: None, use_local_toolchain: Some(OsString::from("TOOLCHAIN")) }; + assert_eq!(e, trial(&["cargo-kani", "kani", "setup", "--use-local-toolchain", "TOOLCHAIN"])); + assert_eq!(e, trial(&["cargo", "kani", "setup", "--use-local-toolchain", "TOOLCHAIN"])); + assert_eq!(e, trial(&["cargo-kani", "setup", "--use-local-toolchain", "TOOLCHAIN"])); + } + { + let e = ArgsResult::ExplicitSetup { use_local_bundle: Some(OsString::from("FILE")), use_local_toolchain: Some(OsString::from("TOOLCHAIN")) }; + assert_eq!(e, trial(&["cargo-kani", "kani", "setup", "--use-local-bundle", "FILE", "--use-local-toolchain", "TOOLCHAIN"])); + assert_eq!(e, trial(&["cargo", "kani", "setup", "--use-local-bundle", "FILE", "--use-local-toolchain", "TOOLCHAIN"])); + assert_eq!(e, trial(&["cargo-kani", "setup", "--use-local-bundle", "FILE", "--use-local-toolchain", "TOOLCHAIN"])); + } } } diff --git a/src/setup.rs b/src/setup.rs index ffdcf340e336..2a41f888e95e 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -70,7 +70,7 @@ pub fn appears_incomplete() -> Option { } /// Sets up Kani by unpacking/installing to `~/.kani/kani-VERSION` -pub fn setup(use_local_bundle: Option) -> Result<()> { +pub fn setup(use_local_bundle: Option, use_local_toolchain: Option) -> Result<()> { let kani_dir = kani_dir()?; let os = os_info::get(); @@ -81,7 +81,7 @@ pub fn setup(use_local_bundle: Option) -> Result<()> { setup_kani_bundle(&kani_dir, use_local_bundle)?; - setup_rust_toolchain(&kani_dir)?; + setup_rust_toolchain(&kani_dir, use_local_toolchain)?; setup_python_deps(&kani_dir)?; @@ -139,14 +139,22 @@ pub(crate) fn get_rust_toolchain_version(kani_dir: &Path) -> Result { } /// Install the Rust toolchain version we require -fn setup_rust_toolchain(kani_dir: &Path) -> Result { +fn setup_rust_toolchain(kani_dir: &Path, use_local_toolchain: Option) -> Result { // Currently this means we require the bundle to have been unpacked first! let toolchain_version = get_rust_toolchain_version(kani_dir)?; println!("[3/5] Installing rust toolchain version: {}", &toolchain_version); - Command::new("rustup").args(["toolchain", "install", &toolchain_version]).run()?; - let toolchain = home::rustup_home()?.join("toolchains").join(&toolchain_version); + // Symlink to a local toolchain if the user explicitly requests + if let Some(local_toolchain_path) = use_local_toolchain { + let toolchain_path = Path::new(&local_toolchain_path); + // TODO: match the version against which kani was built + symlink_rust_toolchain(toolchain_path, kani_dir)?; + return Ok(toolchain_version); + } + // This is the default behaviour when no explicit path to a toolchain is mentioned + Command::new("rustup").args(["toolchain", "install", &toolchain_version]).run()?; + let toolchain = home::rustup_home()?.join("toolchains").join(&toolchain_version); symlink_rust_toolchain(&toolchain, kani_dir)?; Ok(toolchain_version) } @@ -201,6 +209,7 @@ fn fail_if_unsupported_target() -> Result<()> { fn symlink_rust_toolchain(toolchain: &Path, kani_dir: &Path) -> Result<()> { let path = kani_dir.join("toolchain"); // We want setup to be idempotent, so if the symlink already exists, delete instead of failing + // There's a chance that we might need to delete actual toolchain folders in the repo if they exist if path.exists() && path.is_symlink() { std::fs::remove_file(&path)?; } From 4bd86b64098f433e2d070287b99fba8dd0b04cf7 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Tue, 5 Mar 2024 17:46:02 +0000 Subject: [PATCH 2/8] Add change to switch cargo version based on the mode of Kani being used --- kani-driver/src/assess/scan.rs | 3 +- kani-driver/src/call_cargo.rs | 5 +- kani-driver/src/concrete_playback/playback.rs | 19 +++- kani-driver/src/session.rs | 25 ++++++ src/lib.rs | 90 +++++++++++++++---- src/setup.rs | 6 +- 6 files changed, 122 insertions(+), 26 deletions(-) diff --git a/kani-driver/src/assess/scan.rs b/kani-driver/src/assess/scan.rs index 5e4dc81d7e2a..2bc58e074f10 100644 --- a/kani-driver/src/assess/scan.rs +++ b/kani-driver/src/assess/scan.rs @@ -168,7 +168,8 @@ fn invoke_assess( ) -> Result<()> { let dir = manifest.parent().expect("file not in a directory?"); let log = std::fs::File::create(logfile)?; - let mut cmd = Command::new("cargo"); + + let mut cmd = session.setup_cargo_command()?; cmd.arg("kani"); // Use of options before 'assess' subcommand is a hack, these should be factored out. // TODO: --only-codegen should be outright an option to assess. (perhaps tests too?) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 66166913c9cb..3fc800133f6d 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -109,9 +109,8 @@ impl KaniSession { let mut failed_targets = vec![]; for package in packages { for verification_target in package_targets(&self.args, package) { - let mut cmd = Command::new("cargo"); - cmd.arg(session::toolchain_shorthand()) - .args(&cargo_args) + let mut cmd = self.setup_cargo_command()?; + cmd.args(&cargo_args) .args(vec!["-p", &package.name]) .args(&verification_target.to_args()) .args(&pkg_args) diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs index 96ed30da904d..226b0b6a57bd 100644 --- a/kani-driver/src/concrete_playback/playback.rs +++ b/kani-driver/src/concrete_playback/playback.rs @@ -96,6 +96,21 @@ fn build_test(install: &InstallType, args: &KaniPlaybackArgs) -> Result /// TODO: This should likely be inside KaniSession, but KaniSession requires `VerificationArgs` today. /// For now, we just use InstallType directly. fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> { + // Recreating the match from `setup_cargo_command` here because this function takes InstallType + // This whole function needs refactoring to use KaniSession instead + let mut cmd = match install { + InstallType::DevRepo(_) => { + let mut cmd = Command::new("cargo"); + cmd.arg(session::toolchain_shorthand()); + cmd + } + InstallType::Release(kani_dir) => { + let cargo_path = kani_dir.join("toolchain").join("bin").join("cargo"); + let cmd = Command::new(cargo_path); + cmd + } + }; + let rustc_args = base_rustc_flags(lib_playback_folder()?); let mut cargo_args: Vec = vec!["test".into()]; @@ -123,9 +138,7 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> { } // Arguments that will only be passed to the target package. - let mut cmd = Command::new("cargo"); - cmd.arg(session::toolchain_shorthand()) - .args(&cargo_args) + cmd.args(&cargo_args) .env("RUSTC", &install.kani_compiler()?) // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See // https://doc.rust-lang.org/cargo/reference/environment-variables.html diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 5b9b90854789..ae94f7996b5b 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -64,6 +64,31 @@ impl KaniSession { }) } + /* + Setup the default version of cargo being run, based on the type/mode of installation for kani + If kani is being run in developer mode, then we use the one provided by rustup as we can assume that the developer will have rustup installed + For release versions of Kani, we use a version of cargo that's in the toolchain that's been symlinked during `cargo-kani` setup. This will allow + Kani to remove the runtime dependency on rustup later on. + */ + pub fn setup_cargo_command(&self) -> Result { + let install_type = InstallType::new()?; + + let cmd = match install_type { + InstallType::DevRepo(_) => { + let mut cmd = Command::new("cargo"); + cmd.arg(self::toolchain_shorthand()); + cmd + } + InstallType::Release(kani_dir) => { + let cargo_path = kani_dir.join("toolchain").join("bin").join("cargo"); + let cmd = Command::new(cargo_path); + cmd + } + }; + + Ok(cmd) + } + /// Record a temporary file so we can cleanup after ourselves at the end. /// Note that there will be no failure if the file does not exist. pub fn record_temporary_file>(&self, temp: &T) { diff --git a/src/lib.rs b/src/lib.rs index 87db3337e85a..6f9765769b62 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -29,7 +29,9 @@ use anyhow::{bail, Context, Result}; /// `bin` should be either `kani` or `cargo-kani` pub fn proxy(bin: &str) -> Result<()> { match parse_args(env::args_os().collect()) { - ArgsResult::ExplicitSetup { use_local_bundle, use_local_toolchain } => setup::setup(use_local_bundle, use_local_toolchain), + ArgsResult::ExplicitSetup { use_local_bundle, use_local_toolchain } => { + setup::setup(use_local_bundle, use_local_toolchain) + } ArgsResult::Default => { fail_if_in_dev_environment()?; if !setup::appears_setup() { @@ -52,7 +54,7 @@ pub fn proxy(bin: &str) -> Result<()> { /// Minimalist argument parsing result type #[derive(PartialEq, Eq, Debug)] enum ArgsResult { - ExplicitSetup { use_local_bundle: Option, use_local_toolchain: Option}, + ExplicitSetup { use_local_bundle: Option, use_local_toolchain: Option }, Default, } @@ -69,17 +71,20 @@ fn parse_args(args: Vec) -> ArgsResult { ), ) .subcommand( - SubCommand::with_name("kani") - .subcommand( + SubCommand::with_name("kani").subcommand( SubCommand::with_name("setup") - .arg(Arg::with_name("use-local-bundle").long("use-local-bundle").takes_value(true)) + .arg( + Arg::with_name("use-local-bundle") + .long("use-local-bundle") + .takes_value(true), + ) .arg( Arg::with_name("use-local-toolchain") .long("use-local-toolchain") .takes_value(true), ), - ), - ) + ), + ) .get_matches_from(args); // Default is the behaviour for Kani when cargo-kani/ cargo kani runs on its own and sees that there is no setup done yet @@ -87,12 +92,19 @@ fn parse_args(args: Vec) -> ArgsResult { if let Some(matches) = matches.subcommand_matches("setup") { let use_local_toolchain = matches.value_of_os("use-local-toolchain").map(OsString::from); let use_local_bundle = matches.value_of_os("use-local-bundle").map(OsString::from); - ArgsResult::ExplicitSetup { use_local_bundle: use_local_bundle, use_local_toolchain: use_local_toolchain } + ArgsResult::ExplicitSetup { + use_local_bundle: use_local_bundle, + use_local_toolchain: use_local_toolchain, + } } else if let Some(matches) = matches.subcommand_matches("kani") { if let Some(matches) = matches.subcommand_matches("setup") { - let use_local_toolchain = matches.value_of_os("use-local-toolchain").map(OsString::from); + let use_local_toolchain = + matches.value_of_os("use-local-toolchain").map(OsString::from); let use_local_bundle = matches.value_of_os("use-local-bundle").map(OsString::from); - ArgsResult::ExplicitSetup { use_local_bundle: use_local_bundle, use_local_toolchain: use_local_toolchain } + ArgsResult::ExplicitSetup { + use_local_bundle: use_local_bundle, + use_local_toolchain: use_local_toolchain, + } } else { ArgsResult::Default } @@ -254,22 +266,66 @@ mod tests { assert_eq!(e, trial(&["cargo-kani", "setup"])); } { - let e = ArgsResult::ExplicitSetup { use_local_bundle: Some(OsString::from("FILE")), use_local_toolchain: None }; + let e = ArgsResult::ExplicitSetup { + use_local_bundle: Some(OsString::from("FILE")), + use_local_toolchain: None, + }; assert_eq!(e, trial(&["cargo-kani", "kani", "setup", "--use-local-bundle", "FILE"])); assert_eq!(e, trial(&["cargo", "kani", "setup", "--use-local-bundle", "FILE"])); assert_eq!(e, trial(&["cargo-kani", "setup", "--use-local-bundle", "FILE"])); } { - let e = ArgsResult::ExplicitSetup { use_local_bundle: None, use_local_toolchain: Some(OsString::from("TOOLCHAIN")) }; - assert_eq!(e, trial(&["cargo-kani", "kani", "setup", "--use-local-toolchain", "TOOLCHAIN"])); + let e = ArgsResult::ExplicitSetup { + use_local_bundle: None, + use_local_toolchain: Some(OsString::from("TOOLCHAIN")), + }; + assert_eq!( + e, + trial(&["cargo-kani", "kani", "setup", "--use-local-toolchain", "TOOLCHAIN"]) + ); assert_eq!(e, trial(&["cargo", "kani", "setup", "--use-local-toolchain", "TOOLCHAIN"])); assert_eq!(e, trial(&["cargo-kani", "setup", "--use-local-toolchain", "TOOLCHAIN"])); } { - let e = ArgsResult::ExplicitSetup { use_local_bundle: Some(OsString::from("FILE")), use_local_toolchain: Some(OsString::from("TOOLCHAIN")) }; - assert_eq!(e, trial(&["cargo-kani", "kani", "setup", "--use-local-bundle", "FILE", "--use-local-toolchain", "TOOLCHAIN"])); - assert_eq!(e, trial(&["cargo", "kani", "setup", "--use-local-bundle", "FILE", "--use-local-toolchain", "TOOLCHAIN"])); - assert_eq!(e, trial(&["cargo-kani", "setup", "--use-local-bundle", "FILE", "--use-local-toolchain", "TOOLCHAIN"])); + let e = ArgsResult::ExplicitSetup { + use_local_bundle: Some(OsString::from("FILE")), + use_local_toolchain: Some(OsString::from("TOOLCHAIN")), + }; + assert_eq!( + e, + trial(&[ + "cargo-kani", + "kani", + "setup", + "--use-local-bundle", + "FILE", + "--use-local-toolchain", + "TOOLCHAIN" + ]) + ); + assert_eq!( + e, + trial(&[ + "cargo", + "kani", + "setup", + "--use-local-bundle", + "FILE", + "--use-local-toolchain", + "TOOLCHAIN" + ]) + ); + assert_eq!( + e, + trial(&[ + "cargo-kani", + "setup", + "--use-local-bundle", + "FILE", + "--use-local-toolchain", + "TOOLCHAIN" + ]) + ); } } } diff --git a/src/setup.rs b/src/setup.rs index 2a41f888e95e..c0f3a9ef6cec 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -70,7 +70,10 @@ pub fn appears_incomplete() -> Option { } /// Sets up Kani by unpacking/installing to `~/.kani/kani-VERSION` -pub fn setup(use_local_bundle: Option, use_local_toolchain: Option) -> Result<()> { +pub fn setup( + use_local_bundle: Option, + use_local_toolchain: Option, +) -> Result<()> { let kani_dir = kani_dir()?; let os = os_info::get(); @@ -209,7 +212,6 @@ fn fail_if_unsupported_target() -> Result<()> { fn symlink_rust_toolchain(toolchain: &Path, kani_dir: &Path) -> Result<()> { let path = kani_dir.join("toolchain"); // We want setup to be idempotent, so if the symlink already exists, delete instead of failing - // There's a chance that we might need to delete actual toolchain folders in the repo if they exist if path.exists() && path.is_symlink() { std::fs::remove_file(&path)?; } From 192c4a9a33fed35a70c962ade91a75a17d2fb254 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Tue, 5 Mar 2024 19:32:44 +0000 Subject: [PATCH 3/8] remove command import --- kani-driver/src/assess/scan.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/kani-driver/src/assess/scan.rs b/kani-driver/src/assess/scan.rs index 2bc58e074f10..3be3861fc8e6 100644 --- a/kani-driver/src/assess/scan.rs +++ b/kani-driver/src/assess/scan.rs @@ -4,7 +4,6 @@ use std::collections::HashSet; use std::path::Path; use std::path::PathBuf; -use std::process::Command; use std::time::Instant; use anyhow::Result; From 7d5a40088c4c81bbbce86a91e6eb2eb5031207eb Mon Sep 17 00:00:00 2001 From: jaisnan Date: Tue, 5 Mar 2024 19:35:31 +0000 Subject: [PATCH 4/8] fix Clippy warnings --- kani-driver/src/call_cargo.rs | 2 +- kani-driver/src/concrete_playback/playback.rs | 4 ++-- kani-driver/src/session.rs | 4 ++-- src/lib.rs | 8 ++++---- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 3fc800133f6d..1abcaa7fdf72 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -5,7 +5,7 @@ use crate::args::VerificationArgs; use crate::call_single_file::to_rustc_arg; use crate::project::Artifact; use crate::session::KaniSession; -use crate::{session, util}; +use crate::{util}; use anyhow::{bail, Context, Result}; use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel}; use cargo_metadata::{Message, Metadata, MetadataCommand, Package, Target}; diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs index 226b0b6a57bd..c319fb26449a 100644 --- a/kani-driver/src/concrete_playback/playback.rs +++ b/kani-driver/src/concrete_playback/playback.rs @@ -106,8 +106,8 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> { } InstallType::Release(kani_dir) => { let cargo_path = kani_dir.join("toolchain").join("bin").join("cargo"); - let cmd = Command::new(cargo_path); - cmd + + Command::new(cargo_path) } }; diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index ae94f7996b5b..94f3b267fd21 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -81,8 +81,8 @@ impl KaniSession { } InstallType::Release(kani_dir) => { let cargo_path = kani_dir.join("toolchain").join("bin").join("cargo"); - let cmd = Command::new(cargo_path); - cmd + + Command::new(cargo_path) } }; diff --git a/src/lib.rs b/src/lib.rs index 6f9765769b62..4821c3a1e512 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -93,8 +93,8 @@ fn parse_args(args: Vec) -> ArgsResult { let use_local_toolchain = matches.value_of_os("use-local-toolchain").map(OsString::from); let use_local_bundle = matches.value_of_os("use-local-bundle").map(OsString::from); ArgsResult::ExplicitSetup { - use_local_bundle: use_local_bundle, - use_local_toolchain: use_local_toolchain, + use_local_bundle , + use_local_toolchain, } } else if let Some(matches) = matches.subcommand_matches("kani") { if let Some(matches) = matches.subcommand_matches("setup") { @@ -102,8 +102,8 @@ fn parse_args(args: Vec) -> ArgsResult { matches.value_of_os("use-local-toolchain").map(OsString::from); let use_local_bundle = matches.value_of_os("use-local-bundle").map(OsString::from); ArgsResult::ExplicitSetup { - use_local_bundle: use_local_bundle, - use_local_toolchain: use_local_toolchain, + use_local_bundle, + use_local_toolchain, } } else { ArgsResult::Default From 5f825737c9461e8375c8b6fc752cf03166a15b09 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Tue, 5 Mar 2024 19:44:58 +0000 Subject: [PATCH 5/8] run rustfmt --- kani-driver/src/call_cargo.rs | 2 +- kani-driver/src/concrete_playback/playback.rs | 1 - kani-driver/src/session.rs | 1 - src/lib.rs | 10 ++-------- 4 files changed, 3 insertions(+), 11 deletions(-) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 1abcaa7fdf72..7b06b94ee504 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -5,7 +5,7 @@ use crate::args::VerificationArgs; use crate::call_single_file::to_rustc_arg; use crate::project::Artifact; use crate::session::KaniSession; -use crate::{util}; +use crate::util; use anyhow::{bail, Context, Result}; use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel}; use cargo_metadata::{Message, Metadata, MetadataCommand, Package, Target}; diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs index c319fb26449a..c9716894850e 100644 --- a/kani-driver/src/concrete_playback/playback.rs +++ b/kani-driver/src/concrete_playback/playback.rs @@ -106,7 +106,6 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> { } InstallType::Release(kani_dir) => { let cargo_path = kani_dir.join("toolchain").join("bin").join("cargo"); - Command::new(cargo_path) } }; diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 94f3b267fd21..ac1e390701c3 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -81,7 +81,6 @@ impl KaniSession { } InstallType::Release(kani_dir) => { let cargo_path = kani_dir.join("toolchain").join("bin").join("cargo"); - Command::new(cargo_path) } }; diff --git a/src/lib.rs b/src/lib.rs index 4821c3a1e512..202d46f0e5ac 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -92,19 +92,13 @@ fn parse_args(args: Vec) -> ArgsResult { if let Some(matches) = matches.subcommand_matches("setup") { let use_local_toolchain = matches.value_of_os("use-local-toolchain").map(OsString::from); let use_local_bundle = matches.value_of_os("use-local-bundle").map(OsString::from); - ArgsResult::ExplicitSetup { - use_local_bundle , - use_local_toolchain, - } + ArgsResult::ExplicitSetup { use_local_bundle, use_local_toolchain } } else if let Some(matches) = matches.subcommand_matches("kani") { if let Some(matches) = matches.subcommand_matches("setup") { let use_local_toolchain = matches.value_of_os("use-local-toolchain").map(OsString::from); let use_local_bundle = matches.value_of_os("use-local-bundle").map(OsString::from); - ArgsResult::ExplicitSetup { - use_local_bundle, - use_local_toolchain, - } + ArgsResult::ExplicitSetup { use_local_bundle, use_local_toolchain } } else { ArgsResult::Default } From cb9aa4d3386f4f75a0cb89b44cb0733fc8b0beab Mon Sep 17 00:00:00 2001 From: jaisnan Date: Wed, 6 Mar 2024 16:34:50 +0000 Subject: [PATCH 6/8] Move function from KaniSession --- kani-driver/src/assess/scan.rs | 3 +- kani-driver/src/call_cargo.rs | 4 +- kani-driver/src/concrete_playback/playback.rs | 17 ++----- kani-driver/src/session.rs | 46 +++++++++---------- 4 files changed, 29 insertions(+), 41 deletions(-) diff --git a/kani-driver/src/assess/scan.rs b/kani-driver/src/assess/scan.rs index 3be3861fc8e6..ef33f91eb522 100644 --- a/kani-driver/src/assess/scan.rs +++ b/kani-driver/src/assess/scan.rs @@ -9,6 +9,7 @@ use std::time::Instant; use anyhow::Result; use cargo_metadata::Package; +use crate::session::setup_cargo_command; use crate::session::KaniSession; use super::metadata::AssessMetadata; @@ -168,7 +169,7 @@ fn invoke_assess( let dir = manifest.parent().expect("file not in a directory?"); let log = std::fs::File::create(logfile)?; - let mut cmd = session.setup_cargo_command()?; + let mut cmd = setup_cargo_command()?; cmd.arg("kani"); // Use of options before 'assess' subcommand is a hack, these should be factored out. // TODO: --only-codegen should be outright an option to assess. (perhaps tests too?) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 7b06b94ee504..b68d18c84a40 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -4,7 +4,7 @@ use crate::args::VerificationArgs; use crate::call_single_file::to_rustc_arg; use crate::project::Artifact; -use crate::session::KaniSession; +use crate::session::{setup_cargo_command, KaniSession}; use crate::util; use anyhow::{bail, Context, Result}; use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel}; @@ -109,7 +109,7 @@ impl KaniSession { let mut failed_targets = vec![]; for package in packages { for verification_target in package_targets(&self.args, package) { - let mut cmd = self.setup_cargo_command()?; + let mut cmd = setup_cargo_command()?; cmd.args(&cargo_args) .args(vec!["-p", &package.name]) .args(&verification_target.to_args()) diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs index c9716894850e..a28749c2fdfe 100644 --- a/kani-driver/src/concrete_playback/playback.rs +++ b/kani-driver/src/concrete_playback/playback.rs @@ -7,7 +7,7 @@ use crate::args::common::Verbosity; use crate::args::playback_args::{CargoPlaybackArgs, KaniPlaybackArgs, MessageFormat}; use crate::call_cargo::cargo_config_args; use crate::call_single_file::base_rustc_flags; -use crate::session::{lib_playback_folder, InstallType}; +use crate::session::{lib_playback_folder, setup_cargo_command, InstallType}; use crate::{session, util}; use anyhow::Result; use std::ffi::OsString; @@ -96,19 +96,8 @@ fn build_test(install: &InstallType, args: &KaniPlaybackArgs) -> Result /// TODO: This should likely be inside KaniSession, but KaniSession requires `VerificationArgs` today. /// For now, we just use InstallType directly. fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> { - // Recreating the match from `setup_cargo_command` here because this function takes InstallType - // This whole function needs refactoring to use KaniSession instead - let mut cmd = match install { - InstallType::DevRepo(_) => { - let mut cmd = Command::new("cargo"); - cmd.arg(session::toolchain_shorthand()); - cmd - } - InstallType::Release(kani_dir) => { - let cargo_path = kani_dir.join("toolchain").join("bin").join("cargo"); - Command::new(cargo_path) - } - }; + + let mut cmd = setup_cargo_command()?; let rustc_args = base_rustc_flags(lib_playback_folder()?); let mut cargo_args: Vec = vec!["test".into()]; diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index ac1e390701c3..8cf4a20450f5 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -64,30 +64,6 @@ impl KaniSession { }) } - /* - Setup the default version of cargo being run, based on the type/mode of installation for kani - If kani is being run in developer mode, then we use the one provided by rustup as we can assume that the developer will have rustup installed - For release versions of Kani, we use a version of cargo that's in the toolchain that's been symlinked during `cargo-kani` setup. This will allow - Kani to remove the runtime dependency on rustup later on. - */ - pub fn setup_cargo_command(&self) -> Result { - let install_type = InstallType::new()?; - - let cmd = match install_type { - InstallType::DevRepo(_) => { - let mut cmd = Command::new("cargo"); - cmd.arg(self::toolchain_shorthand()); - cmd - } - InstallType::Release(kani_dir) => { - let cargo_path = kani_dir.join("toolchain").join("bin").join("cargo"); - Command::new(cargo_path) - } - }; - - Ok(cmd) - } - /// Record a temporary file so we can cleanup after ourselves at the end. /// Note that there will be no failure if the file does not exist. pub fn record_temporary_file>(&self, temp: &T) { @@ -403,3 +379,25 @@ fn init_logger(args: &VerificationArgs) { ); tracing::subscriber::set_global_default(subscriber).unwrap(); } + +// Setup the default version of cargo being run, based on the type/mode of installation for kani +// If kani is being run in developer mode, then we use the one provided by rustup as we can assume that the developer will have rustup installed +// For release versions of Kani, we use a version of cargo that's in the toolchain that's been symlinked during `cargo-kani` setup. This will allow +// Kani to remove the runtime dependency on rustup later on. +pub fn setup_cargo_command() -> Result { + let install_type = InstallType::new()?; + + let cmd = match install_type { + InstallType::DevRepo(_) => { + let mut cmd = Command::new("cargo"); + cmd.arg(self::toolchain_shorthand()); + cmd + } + InstallType::Release(kani_dir) => { + let cargo_path = kani_dir.join("toolchain").join("bin").join("cargo"); + Command::new(cargo_path) + } + }; + + Ok(cmd) +} From 24c659287943ac5a9f0541a65e6735ed037045e3 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Wed, 6 Mar 2024 17:41:50 +0000 Subject: [PATCH 7/8] Address comments --- kani-driver/src/concrete_playback/playback.rs | 11 +++++------ src/setup.rs | 1 + 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs index a28749c2fdfe..ab644fa67a28 100644 --- a/kani-driver/src/concrete_playback/playback.rs +++ b/kani-driver/src/concrete_playback/playback.rs @@ -17,8 +17,7 @@ use std::process::Command; use tracing::debug; pub fn playback_cargo(args: CargoPlaybackArgs) -> Result<()> { - let install = InstallType::new()?; - cargo_test(&install, args) + cargo_test(args) } pub fn playback_standalone(args: KaniPlaybackArgs) -> Result<()> { @@ -93,10 +92,10 @@ fn build_test(install: &InstallType, args: &KaniPlaybackArgs) -> Result } /// Invokes cargo test using Kani compiler and the provided arguments. -/// TODO: This should likely be inside KaniSession, but KaniSession requires `VerificationArgs` today. -/// For now, we just use InstallType directly. -fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> { - +/// TODO: Refactor to remove installtype +/// Issue: https://github.com/model-checking/kani/issues/3060 +fn cargo_test(args: CargoPlaybackArgs) -> Result<()> { + let install = InstallType::new()?; let mut cmd = setup_cargo_command()?; let rustc_args = base_rustc_flags(lib_playback_folder()?); diff --git a/src/setup.rs b/src/setup.rs index c0f3a9ef6cec..050a8e166334 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -151,6 +151,7 @@ fn setup_rust_toolchain(kani_dir: &Path, use_local_toolchain: Option) if let Some(local_toolchain_path) = use_local_toolchain { let toolchain_path = Path::new(&local_toolchain_path); // TODO: match the version against which kani was built + // Issue: https://github.com/model-checking/kani/issues/3060 symlink_rust_toolchain(toolchain_path, kani_dir)?; return Ok(toolchain_version); } From 12b697d7b0296a868296c0870bfefc6b759898fa Mon Sep 17 00:00:00 2001 From: jaisnan Date: Wed, 6 Mar 2024 17:42:32 +0000 Subject: [PATCH 8/8] Remove comment --- kani-driver/src/concrete_playback/playback.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs index ab644fa67a28..d8c1762da92b 100644 --- a/kani-driver/src/concrete_playback/playback.rs +++ b/kani-driver/src/concrete_playback/playback.rs @@ -92,8 +92,6 @@ fn build_test(install: &InstallType, args: &KaniPlaybackArgs) -> Result } /// Invokes cargo test using Kani compiler and the provided arguments. -/// TODO: Refactor to remove installtype -/// Issue: https://github.com/model-checking/kani/issues/3060 fn cargo_test(args: CargoPlaybackArgs) -> Result<()> { let install = InstallType::new()?; let mut cmd = setup_cargo_command()?;