From 45caad49ab8f8cec9c3a5b695261908ffec63f8d Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Thu, 7 Mar 2024 13:15:51 -0500 Subject: [PATCH] Add `--use-local-toolchain` to Kani setup (#3056) Adds `--use-local-toolchain` to Kani's setup flow, which accepts a local toolchain and then uses that to finish the Kani setup. Some notes: 1. Why? This is mainly for installing GPG verified toolchains. 2. This is missing some cleanup and refactoring work, like ensuring that the user defined toolchain matches the one that Kani was built against etc. Marked as Todo, for later. Resolves [#3058](https://github.com/model-checking/kani/issues/3058) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .gitignore | 1 + Cargo.lock | 76 ++++++++++- Cargo.toml | 1 + kani-compiler/build.rs | 2 + kani-driver/src/assess/scan.rs | 5 +- kani-driver/src/call_cargo.rs | 9 +- kani-driver/src/concrete_playback/playback.rs | 16 +-- kani-driver/src/session.rs | 22 +++ src/lib.rs | 129 +++++++++++++++--- src/setup.rs | 22 ++- 10 files changed, 236 insertions(+), 47 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 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) }