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 1/3] 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) } From 2f3cc47eba7d27754e36e31e69c5820a7ca08158 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 8 Mar 2024 12:39:31 -0800 Subject: [PATCH 2/3] Replace internal reverse_postorder by a stable one (#3064) The `reverse_postorder` function used before is internal to the compiler and reflects the internal body representation. Besides that, I would like to introduce transformation on the top of SMIR body, which will break the 1:1 relationship between basic blocks from internal body and monomorphic body from StableMIR. --- .../codegen_cprover_gotoc/codegen/block.rs | 32 ++++++++++++++++++- .../codegen_cprover_gotoc/codegen/function.rs | 6 ++-- .../context/current_fn.rs | 9 ------ 3 files changed, 33 insertions(+), 14 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs index 692fdb9c385b..5fe28097a2e0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs @@ -2,7 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::codegen_cprover_gotoc::GotocCtx; -use stable_mir::mir::{BasicBlock, BasicBlockIdx}; +use stable_mir::mir::{BasicBlock, BasicBlockIdx, Body}; +use std::collections::HashSet; use tracing::debug; pub fn bb_label(bb: BasicBlockIdx) -> String { @@ -72,3 +73,32 @@ impl<'tcx> GotocCtx<'tcx> { } } } + +/// Iterate over the basic blocks in reverse post-order. +/// +/// The `reverse_postorder` function used before was internal to the compiler and reflected the +/// internal body representation. +/// +/// As we introduce transformations on the top of SMIR body, there will be not guarantee of a +/// 1:1 relationship between basic blocks from internal body and monomorphic body from StableMIR. +pub fn reverse_postorder(body: &Body) -> impl Iterator { + postorder(body, 0, &mut HashSet::with_capacity(body.blocks.len())).into_iter().rev() +} + +fn postorder( + body: &Body, + bb: BasicBlockIdx, + visited: &mut HashSet, +) -> Vec { + if visited.contains(&bb) { + return vec![]; + } + visited.insert(bb); + + let mut result = vec![]; + for succ in body.blocks[bb].terminator.successors() { + result.append(&mut postorder(body, succ, visited)); + } + result.push(bb); + result +} diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 78c7e2b6cbd6..7cf4b979f407 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -3,10 +3,10 @@ //! This file contains functions related to codegenning MIR functions into gotoc +use crate::codegen_cprover_gotoc::codegen::block::reverse_postorder; use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{Expr, Stmt, Symbol}; use cbmc::InternString; -use rustc_middle::mir::traversal::reverse_postorder; use stable_mir::mir::mono::Instance; use stable_mir::mir::{Body, Local}; use stable_mir::ty::{RigidTy, TyKind}; @@ -67,9 +67,7 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_declare_variables(&body); // Get the order from internal body for now. - let internal_body = self.current_fn().body_internal(); - reverse_postorder(internal_body) - .for_each(|(bb, _)| self.codegen_block(bb.index(), &body.blocks[bb.index()])); + reverse_postorder(&body).for_each(|bb| self.codegen_block(bb, &body.blocks[bb])); let loc = self.codegen_span_stable(instance.def.span()); let stmts = self.current_fn_mut().extract_block(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs index adac294e30eb..5a542ca07cd2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs @@ -4,7 +4,6 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Stmt; use cbmc::InternedString; -use rustc_middle::mir::Body as BodyInternal; use rustc_middle::ty::Instance as InstanceInternal; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; @@ -21,8 +20,6 @@ pub struct CurrentFnCtx<'tcx> { instance: Instance, /// The crate this function is from krate: String, - /// The MIR for the current instance. This is using the internal representation. - mir: &'tcx BodyInternal<'tcx>, /// The current instance. This is using the internal representation. instance_internal: InstanceInternal<'tcx>, /// A list of local declarations used to retrieve MIR component types. @@ -53,7 +50,6 @@ impl<'tcx> CurrentFnCtx<'tcx> { Self { block: vec![], instance, - mir: gcx.tcx.instance_mir(instance_internal.def), instance_internal, krate: instance.def.krate().name, locals, @@ -94,11 +90,6 @@ impl<'tcx> CurrentFnCtx<'tcx> { self.instance } - /// The internal MIR for the function we are currently compiling using internal APIs. - pub fn body_internal(&self) -> &'tcx BodyInternal<'tcx> { - self.mir - } - /// The name of the function we are currently compiling pub fn name(&self) -> String { self.name.clone() From ea710b36c7ef81b038df4c1a9ef3c18d2f6ab0ef Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 8 Mar 2024 16:42:19 -0500 Subject: [PATCH 3/3] Add option to override `--crate-name` from `kani` (#3054) Adds a hidden `--crate-name` option to standalone Kani (i.e., `kani`) only. This option allows users to override the crate name used during the compilation of single-file Rust programs, making it easier to apply Kani to non-Cargo projects (see #3046 for more details). Resolves #3046 --- kani-driver/src/args/mod.rs | 3 ++ kani-driver/src/main.rs | 2 +- kani-driver/src/project.rs | 27 +++++++--- kani-driver/src/util.rs | 20 ------- .../script-based-pre/crate-name/a/src/lib.rs | 6 +++ .../script-based-pre/crate-name/b/src/lib.rs | 7 +++ .../script-based-pre/crate-name/c/src/lib.rs | 8 +++ tests/script-based-pre/crate-name/config.yml | 4 ++ .../crate-name/crate-name.expected | 1 + .../script-based-pre/crate-name/crate-name.sh | 54 +++++++++++++++++++ tests/script-based-pre/crate-name/my-code.rs | 6 +++ 11 files changed, 111 insertions(+), 27 deletions(-) create mode 100644 tests/script-based-pre/crate-name/a/src/lib.rs create mode 100644 tests/script-based-pre/crate-name/b/src/lib.rs create mode 100644 tests/script-based-pre/crate-name/c/src/lib.rs create mode 100644 tests/script-based-pre/crate-name/config.yml create mode 100644 tests/script-based-pre/crate-name/crate-name.expected create mode 100755 tests/script-based-pre/crate-name/crate-name.sh create mode 100644 tests/script-based-pre/crate-name/my-code.rs diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 39b3c1fd025f..aeda94168840 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -79,6 +79,9 @@ pub struct StandaloneArgs { #[command(subcommand)] pub command: Option, + + #[arg(long, hide = true)] + pub crate_name: Option, } /// Kani takes optional subcommands to request specialized behavior. diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 009f25b37b5a..798625560970 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -104,7 +104,7 @@ fn standalone_main() -> Result<()> { print_kani_version(InvocationType::Standalone); } - let project = project::standalone_project(&args.input.unwrap(), &session)?; + let project = project::standalone_project(&args.input.unwrap(), args.crate_name, &session)?; if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } } diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index b99a7e9aff07..fcf3805ab3df 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -18,7 +18,7 @@ use crate::metadata::{from_json, merge_kani_metadata, mock_proof_harness}; use crate::session::KaniSession; -use crate::util::{crate_name, guess_rlib_name}; +use crate::util::crate_name; use anyhow::{Context, Result}; use kani_metadata::{ artifact::convert_type, ArtifactType, ArtifactType::*, HarnessMetadata, KaniMetadata, @@ -270,8 +270,12 @@ pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result } /// Generate a project directly using `kani-compiler` on a single crate. -pub fn standalone_project(input: &Path, session: &KaniSession) -> Result { - StandaloneProjectBuilder::try_new(input, session)?.build() +pub fn standalone_project( + input: &Path, + crate_name: Option, + session: &KaniSession, +) -> Result { + StandaloneProjectBuilder::try_new(input, crate_name, session)?.build() } /// Builder for a standalone project. @@ -291,7 +295,7 @@ struct StandaloneProjectBuilder<'a> { impl<'a> StandaloneProjectBuilder<'a> { /// Create a `StandaloneProjectBuilder` from the given input and session. /// This will perform a few validations before the build. - fn try_new(input: &Path, session: &'a KaniSession) -> Result { + fn try_new(input: &Path, krate_name: Option, session: &'a KaniSession) -> Result { // Ensure the directory exist and it's in its canonical form. let outdir = if let Some(target_dir) = &session.args.target_dir { std::fs::create_dir_all(target_dir)?; // This is a no-op if directory exists. @@ -299,7 +303,7 @@ impl<'a> StandaloneProjectBuilder<'a> { } else { input.canonicalize().unwrap().parent().unwrap().to_path_buf() }; - let crate_name = crate_name(&input); + let crate_name = if let Some(name) = krate_name { name } else { crate_name(&input) }; let metadata = standalone_artifact(&outdir, &crate_name, Metadata); Ok(StandaloneProjectBuilder { outdir, @@ -313,7 +317,7 @@ impl<'a> StandaloneProjectBuilder<'a> { /// Build a project by compiling `self.input` file. fn build(self) -> Result { // Register artifacts that may be generated by the compiler / linker for future deletion. - let rlib_path = guess_rlib_name(&self.outdir.join(self.input.file_name().unwrap())); + let rlib_path = self.rlib_name(); self.session.record_temporary_file(&rlib_path); self.session.record_temporary_file(&self.metadata.path); @@ -339,6 +343,17 @@ impl<'a> StandaloneProjectBuilder<'a> { } result } + + /// Build the rlib name from the crate name. + /// This is only used by 'kani', never 'cargo-kani', so we hopefully don't have too many corner + /// cases to deal with. + fn rlib_name(&self) -> PathBuf { + let path = &self.outdir.join(self.input.file_name().unwrap()); + let basedir = path.parent().unwrap_or(Path::new(".")); + let rlib_name = format!("lib{}.rlib", self.crate_name); + + basedir.join(rlib_name) + } } /// Generate a `KaniMetadata` by extending the original metadata to contain the function under diff --git a/kani-driver/src/util.rs b/kani-driver/src/util.rs index 1e0957dc7726..bfbf9e8d04e1 100644 --- a/kani-driver/src/util.rs +++ b/kani-driver/src/util.rs @@ -26,18 +26,6 @@ pub fn crate_name(path: &Path) -> String { stem.replace(['-', '.'], "_") } -/// Attempt to guess the rlib name for rust source file. -/// This is only used by 'kani', never 'cargo-kani', so we hopefully don't have too many corner -/// cases to deal with. -/// In rustc, you can find some code dealing this this naming in: -/// compiler/rustc_codegen_ssa/src/back/link.rs -pub fn guess_rlib_name(path: &Path) -> PathBuf { - let basedir = path.parent().unwrap_or(Path::new(".")); - let rlib_name = format!("lib{}.rlib", crate_name(path)); - - basedir.join(rlib_name) -} - /// Given a path of some sort (usually from argv0), this attempts to extract the basename / stem /// of the executable. e.g. "/path/foo -> foo" "./foo.exe -> foo" "foo -> foo" pub fn executable_basename(argv0: &Option<&OsString>) -> Option { @@ -117,14 +105,6 @@ mod tests { assert_eq!(alter_extension(&q, "symtab.json"), PathBuf::from("file.more.symtab.json")); } - #[test] - fn check_guess_rlib_name() { - assert_eq!(guess_rlib_name(Path::new("mycrate.rs")), PathBuf::from("libmycrate.rlib")); - assert_eq!(guess_rlib_name(Path::new("my-crate.rs")), PathBuf::from("libmy_crate.rlib")); - assert_eq!(guess_rlib_name(Path::new("./foo.rs")), PathBuf::from("./libfoo.rlib")); - assert_eq!(guess_rlib_name(Path::new("a/b/foo.rs")), PathBuf::from("a/b/libfoo.rlib")); - } - #[test] fn check_exe_basename() { assert_eq!( diff --git a/tests/script-based-pre/crate-name/a/src/lib.rs b/tests/script-based-pre/crate-name/a/src/lib.rs new file mode 100644 index 000000000000..bff1d17f864a --- /dev/null +++ b/tests/script-based-pre/crate-name/a/src/lib.rs @@ -0,0 +1,6 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +pub fn add_a(left: usize, right: usize) -> usize { + left + right +} diff --git a/tests/script-based-pre/crate-name/b/src/lib.rs b/tests/script-based-pre/crate-name/b/src/lib.rs new file mode 100644 index 000000000000..5a1a11687fcf --- /dev/null +++ b/tests/script-based-pre/crate-name/b/src/lib.rs @@ -0,0 +1,7 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +extern crate a; + +pub fn add_b(left: usize, right: usize) -> usize { + a::add_a(left, right) +} diff --git a/tests/script-based-pre/crate-name/c/src/lib.rs b/tests/script-based-pre/crate-name/c/src/lib.rs new file mode 100644 index 000000000000..b4dadd69e1be --- /dev/null +++ b/tests/script-based-pre/crate-name/c/src/lib.rs @@ -0,0 +1,8 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +extern crate a; +extern crate b; + +pub fn add_c(left: usize, right: usize) -> usize { + b::add_b(left, right) +} diff --git a/tests/script-based-pre/crate-name/config.yml b/tests/script-based-pre/crate-name/config.yml new file mode 100644 index 000000000000..f022a9c03732 --- /dev/null +++ b/tests/script-based-pre/crate-name/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: crate-name.sh +expected: crate-name.expected diff --git a/tests/script-based-pre/crate-name/crate-name.expected b/tests/script-based-pre/crate-name/crate-name.expected new file mode 100644 index 000000000000..1a4e02d1ff62 --- /dev/null +++ b/tests/script-based-pre/crate-name/crate-name.expected @@ -0,0 +1 @@ +No proof harnesses (functions with #[kani::proof]) were found to verify. diff --git a/tests/script-based-pre/crate-name/crate-name.sh b/tests/script-based-pre/crate-name/crate-name.sh new file mode 100755 index 000000000000..229cc36938f9 --- /dev/null +++ b/tests/script-based-pre/crate-name/crate-name.sh @@ -0,0 +1,54 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# This test performs multiple checks focused on crate names. The first steps +# check expected results with the default naming scheme. The remaining ones +# check expected results with the `--crate-name=` feature which allows +# users to specify the crate name used for compilation with standalone `kani`. +set -eu + +check_file_exists() { + local file=$1 + if ! [ -e "${file}" ] + then + echo "error: expected \`${file}\` to have been generated" + exit 1 + fi +} + +# 1. Check expected results with the default naming scheme. +# Note: The assumed crate name is `lib`, so we generate `liblib.rlib`. +kani --only-codegen --keep-temps a/src/lib.rs +check_file_exists a/src/liblib.rlib +check_file_exists a/src/lib.kani-metadata.json +rm a/src/liblib.rlib +rm a/src/lib.kani-metadata.json + +# 2. Check expected results with the default naming scheme, which replaces +# some characters. +# Note: The assumed crate name is `my-code`, so we generate `libmy_code.rlib`. +kani --only-codegen --keep-temps my-code.rs +check_file_exists libmy_code.rlib +check_file_exists my_code.kani-metadata.json + +# 3. Check expected results with the `--crate-name=` feature. This feature +# allows users to specify the crate name used for compilation with standalone +# `kani`, enabling the compilation of multiple dependencies with similar +# names. +# Note: In the example below, compiling without `--crate-name=` would +# result in files named `liblib.rlib` for each dependency. +kani --only-codegen --keep-temps a/src/lib.rs --crate-name="a" +check_file_exists a/src/liba.rlib +check_file_exists a/src/a.kani-metadata.json + +RUSTFLAGS="--extern a=a/src/liba.rlib" kani --only-codegen --keep-temps b/src/lib.rs --crate-name="b" +check_file_exists b/src/libb.rlib +check_file_exists b/src/b.kani-metadata.json + +RUSTFLAGS="--extern b=b/src/libb.rlib --extern a=a/src/liba.rlib" kani c/src/lib.rs + +rm a/src/liba.rlib +rm a/src/a.kani-metadata.json +rm b/src/libb.rlib +rm b/src/b.kani-metadata.json diff --git a/tests/script-based-pre/crate-name/my-code.rs b/tests/script-based-pre/crate-name/my-code.rs new file mode 100644 index 000000000000..bff1d17f864a --- /dev/null +++ b/tests/script-based-pre/crate-name/my-code.rs @@ -0,0 +1,6 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +pub fn add_a(left: usize, right: usize) -> usize { + left + right +}