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 ab853a65e544..3af5e6232a76 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.13" @@ -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/kani-driver/src/assess/scan.rs b/kani-driver/src/assess/scan.rs index 5e4dc81d7e2a..ef33f91eb522 100644 --- a/kani-driver/src/assess/scan.rs +++ b/kani-driver/src/assess/scan.rs @@ -4,12 +4,12 @@ use std::collections::HashSet; use std::path::Path; use std::path::PathBuf; -use std::process::Command; 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 +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 = 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..b68d18c84a40 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -4,8 +4,8 @@ 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::session::{setup_cargo_command, KaniSession}; +use crate::util; use anyhow::{bail, Context, Result}; use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel}; use cargo_metadata::{Message, Metadata, MetadataCommand, Package, Target}; @@ -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 = 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..d8c1762da92b 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; @@ -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,9 +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<()> { +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()?); let mut cargo_args: Vec = vec!["test".into()]; @@ -123,9 +123,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..8cf4a20450f5 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -379,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) +} diff --git a/src/lib.rs b/src/lib.rs index 9a1ac90f5dda..202d46f0e5ac 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,18 @@ 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 +54,56 @@ 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_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 } + } else { + ArgsResult::Default } - _ => ArgsResult::Default, + } else { + ArgsResult::Default } } @@ -223,16 +254,72 @@ 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..050a8e166334 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) -> 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 +84,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 +142,23 @@ 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 + // Issue: https://github.com/model-checking/kani/issues/3060 + 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) }