diff --git a/kani-driver/src/args/common.rs b/kani-driver/src/args/common.rs index dcd2262ab2f7..b8434c76e7b8 100644 --- a/kani-driver/src/args/common.rs +++ b/kani-driver/src/args/common.rs @@ -55,3 +55,34 @@ impl ValidateArgs for CommonArgs { Ok(()) } } + +/// The verbosity level to be used in Kani. +pub trait Verbosity { + /// Whether we should be quiet. + fn quiet(&self) -> bool; + /// Whether we should be verbose. + /// Note that `debug() == true` must imply `verbose() == true`. + fn verbose(&self) -> bool; + /// Whether we should emit debug messages. + fn debug(&self) -> bool; + /// Whether any verbosity was selected. + fn is_set(&self) -> bool; +} + +impl Verbosity for CommonArgs { + fn quiet(&self) -> bool { + self.quiet + } + + fn verbose(&self) -> bool { + self.verbose || self.debug + } + + fn debug(&self) -> bool { + self.debug + } + + fn is_set(&self) -> bool { + self.quiet || self.verbose || self.debug + } +} diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index f0918ec78411..f325c7e012b4 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -4,6 +4,7 @@ pub mod assess_args; pub mod common; +pub mod playback_args; pub use assess_args::*; @@ -60,14 +61,29 @@ const DEFAULT_OBJECT_BITS: u32 = 16; version, name = "kani", about = "Verify a single Rust crate. For more information, see https://github.com/model-checking/kani", - args_override_self = true + args_override_self = true, + subcommand_negates_reqs = true, + subcommand_precedence_over_arg = true, + args_conflicts_with_subcommands = true )] pub struct StandaloneArgs { /// Rust file to verify - pub input: PathBuf, + #[arg(required = true)] + pub input: Option, #[command(flatten)] pub verify_opts: VerificationArgs, + + #[command(subcommand)] + pub command: Option, +} + +/// Kani takes optional subcommands to request specialized behavior. +/// When no subcommand is provided, there is an implied verification subcommand. +#[derive(Debug, clap::Subcommand)] +pub enum StandaloneSubcommand { + /// Execute concrete playback testcases of a local crate. + Playback(Box), } #[derive(Debug, clap::Parser)] @@ -85,11 +101,14 @@ pub struct CargoKaniArgs { pub verify_opts: VerificationArgs, } -// cargo-kani takes optional subcommands to request specialized behavior +/// cargo-kani takes optional subcommands to request specialized behavior #[derive(Debug, clap::Subcommand)] pub enum CargoKaniSubcommand { #[command(hide = true)] Assess(Box), + + /// Execute concrete playback testcases of a local package. + Playback(Box), } // Common arguments for invoking Kani for verification purpose. This gets put into KaniContext, @@ -361,6 +380,42 @@ impl CargoArgs { } result } + + /// Convert the arguments back to a format that cargo can understand. + /// Note that the `exclude` option requires special processing and it's not included here. + pub fn to_cargo_args(&self) -> Vec { + let mut cargo_args: Vec = vec![]; + if self.all_features { + cargo_args.push("--all-features".into()); + } + + if self.no_default_features { + cargo_args.push("--no-default-features".into()); + } + + let features = self.features(); + if !features.is_empty() { + cargo_args.push(format!("--features={}", features.join(",")).into()); + } + + if let Some(path) = &self.manifest_path { + cargo_args.push("--manifest-path".into()); + cargo_args.push(path.into()); + } + if self.workspace { + cargo_args.push("--workspace".into()) + } + + cargo_args.extend(self.package.iter().map(|pkg| format!("-p={pkg}").into())); + cargo_args + } +} + +/// Leave it for Cargo to validate these for now. +impl ValidateArgs for CargoArgs { + fn validate(&self) -> Result<(), Error> { + Ok(()) + } } #[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum)] @@ -463,16 +518,36 @@ impl CheckArgs { impl ValidateArgs for StandaloneArgs { fn validate(&self) -> Result<(), Error> { self.verify_opts.validate()?; - if !self.input.is_file() { - Err(Error::raw( - ErrorKind::InvalidValue, - &format!( - "Invalid argument: Input invalid. `{}` is not a regular file.", - self.input.display() - ), - )) - } else { - Ok(()) + if let Some(input) = &self.input { + if !input.is_file() { + return Err(Error::raw( + ErrorKind::InvalidValue, + &format!( + "Invalid argument: Input invalid. `{}` is not a regular file.", + input.display() + ), + )); + } + } + Ok(()) + } +} + +impl ValidateArgs for Option +where + T: ValidateArgs, +{ + fn validate(&self) -> Result<(), Error> { + self.as_ref().map_or(Ok(()), |inner| inner.validate()) + } +} + +impl ValidateArgs for CargoKaniSubcommand { + fn validate(&self) -> Result<(), Error> { + match self { + // Assess doesn't implement validation yet. + CargoKaniSubcommand::Assess(_) => Ok(()), + CargoKaniSubcommand::Playback(playback) => playback.validate(), } } } @@ -480,6 +555,7 @@ impl ValidateArgs for StandaloneArgs { impl ValidateArgs for CargoKaniArgs { fn validate(&self) -> Result<(), Error> { self.verify_opts.validate()?; + self.command.validate()?; // --assess requires --enable-unstable, but the subcommand needs manual checking if (matches!(self.command, Some(CargoKaniSubcommand::Assess(_))) || self.verify_opts.assess) && !self.verify_opts.common_args.enable_unstable @@ -886,4 +962,12 @@ mod tests { assert_eq!(parse(&["kani", "--features", "a", "--features", "b,c"]), ["a", "b", "c"]); assert_eq!(parse(&["kani", "--features", "a b", "-Fc"]), ["a", "b", "c"]); } + + #[test] + fn check_kani_playback() { + let input = "kani playback --test dummy file.rs".split_whitespace(); + let args = StandaloneArgs::try_parse_from(input).unwrap(); + assert_eq!(args.input, None); + assert!(matches!(args.command, Some(StandaloneSubcommand::Playback(..)))); + } } diff --git a/kani-driver/src/args/playback_args.rs b/kani-driver/src/args/playback_args.rs new file mode 100644 index 000000000000..05544b3f5c36 --- /dev/null +++ b/kani-driver/src/args/playback_args.rs @@ -0,0 +1,154 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Implements the subcommand handling of the playback subcommand + +use crate::args::common::UnstableFeatures; +use crate::args::{CargoArgs, CommonArgs, ValidateArgs}; +use clap::error::ErrorKind; +use clap::{Error, Parser, ValueEnum}; +use std::path::PathBuf; + +/// Execute concrete playback testcases of a local package. +#[derive(Debug, Parser)] +pub struct CargoPlaybackArgs { + #[command(flatten)] + pub playback: PlaybackArgs, + + /// Arguments to pass down to Cargo + #[command(flatten)] + pub cargo: CargoArgs, +} + +/// Execute concrete playback testcases of a local crate. +#[derive(Debug, Parser)] +pub struct KaniPlaybackArgs { + /// Rust crate's top file location. + pub input: PathBuf, + + #[command(flatten)] + pub playback: PlaybackArgs, +} + +/// Playback subcommand arguments. +#[derive(Debug, clap::Args)] +pub struct PlaybackArgs { + /// Common args always available to Kani subcommands. + #[command(flatten)] + pub common_opts: CommonArgs, + + /// Specify which test will be executed by the playback args. + #[arg(long)] + pub test: String, + + /// Compile but don't actually run the tests. + #[arg(long)] + pub only_codegen: bool, + + // TODO: We should make this a common option to all subcommands. + /// Control the subcommand output. + #[arg(long, default_value = "human")] + pub message_format: MessageFormat, +} + +/// Message formats available for the subcommand. +#[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum, strum_macros::Display)] +#[strum(serialize_all = "kebab-case")] +pub enum MessageFormat { + /// Print diagnostic messages in a user friendly format. + Human, + /// Print diagnostic messages in JSON format. + Json, +} + +impl ValidateArgs for CargoPlaybackArgs { + fn validate(&self) -> Result<(), Error> { + self.playback.validate()?; + self.cargo.validate() + } +} + +impl ValidateArgs for KaniPlaybackArgs { + fn validate(&self) -> Result<(), Error> { + self.playback.validate()?; + if !self.input.is_file() { + return Err(Error::raw( + ErrorKind::InvalidValue, + &format!( + "Invalid argument: Input invalid. `{}` is not a regular file.", + self.input.display() + ), + )); + } + Ok(()) + } +} + +impl ValidateArgs for PlaybackArgs { + fn validate(&self) -> Result<(), Error> { + self.common_opts.validate()?; + if !self.common_opts.unstable_features.contains(&UnstableFeatures::ConcretePlayback) { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + "The `playback` subcommand is unstable and requires `-Z concrete-playback` \ + to be used.", + )); + } + Ok(()) + } +} + +#[cfg(test)] +mod tests { + use clap::Parser; + + use super::*; + + #[test] + fn check_cargo_parse_test_works() { + let input = "playback -Z concrete-playback --test TEST_NAME".split_whitespace(); + let args = CargoPlaybackArgs::try_parse_from(input.clone()).unwrap(); + args.validate().unwrap(); + assert_eq!(args.playback.test, "TEST_NAME"); + // The default value is human friendly. + assert_eq!(args.playback.message_format, MessageFormat::Human); + } + + #[test] + fn check_cargo_parse_pkg_works() { + let input = "playback -Z concrete-playback --test TEST_NAME -p PKG_NAME".split_whitespace(); + let args = CargoPlaybackArgs::try_parse_from(input).unwrap(); + args.validate().unwrap(); + assert_eq!(args.playback.test, "TEST_NAME"); + assert_eq!(&args.cargo.package, &["PKG_NAME"]) + } + + #[test] + fn check_parse_format_works() { + let input = "playback -Z concrete-playback --test TEST_NAME --message-format=json" + .split_whitespace(); + let args = CargoPlaybackArgs::try_parse_from(input).unwrap(); + args.validate().unwrap(); + assert_eq!(args.playback.test, "TEST_NAME"); + assert_eq!(args.playback.message_format, MessageFormat::Json) + } + + #[test] + fn check_kani_parse_test_works() { + let input = "playback -Z concrete-playback --test TEST_NAME input.rs".split_whitespace(); + let args = KaniPlaybackArgs::try_parse_from(input).unwrap(); + // Don't validate this since we check if the input file exists. + //args.validate().unwrap(); + assert_eq!(args.playback.test, "TEST_NAME"); + assert_eq!(args.input, PathBuf::from("input.rs")); + // The default value is human friendly. + assert_eq!(args.playback.message_format, MessageFormat::Human); + } + + #[test] + fn check_kani_no_unstable_fails() { + let input = "playback --test TEST_NAME input.rs".split_whitespace(); + let args = KaniPlaybackArgs::try_parse_from(input).unwrap(); + let err = args.validate().unwrap_err(); + assert_eq!(err.kind(), ErrorKind::MissingRequiredArgument); + } +} diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 3a65a4cf6ee1..ce53584f3418 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -3,7 +3,7 @@ use anyhow::Result; use std::ffi::OsString; -use std::path::Path; +use std::path::{Path, PathBuf}; use std::process::Command; use crate::session::{base_folder, lib_folder, KaniSession}; @@ -117,41 +117,7 @@ impl KaniSession { /// This function generates all rustc configurations required by our goto-c codegen. pub fn kani_rustc_flags(&self) -> Vec { let lib_path = lib_folder().unwrap(); - let kani_std_rlib = lib_path.join("libstd.rlib"); - let kani_std_wrapper = format!("noprelude:std={}", kani_std_rlib.to_str().unwrap()); - let sysroot = base_folder().unwrap(); - let args = vec![ - "-C", - "overflow-checks=on", - "-C", - "panic=abort", - "-C", - "symbol-mangling-version=v0", - "-Z", - "unstable-options", - "-Z", - "panic_abort_tests=yes", - "-Z", - "trim-diagnostic-paths=no", - "-Z", - "human_readable_cgu_names", - "-Z", - "always-encode-mir", - "--cfg=kani", - "-Z", - "crate-attr=feature(register_tool)", - "-Z", - "crate-attr=register_tool(kanitool)", - "--sysroot", - sysroot.to_str().unwrap(), - "-L", - lib_path.to_str().unwrap(), - "--extern", - "kani", - "--extern", - kani_std_wrapper.as_str(), - ]; - let mut flags: Vec<_> = args.iter().map(OsString::from).collect(); + let mut flags: Vec<_> = base_rustc_flags(lib_path); if self.args.use_abs { flags.push("-Z".into()); flags.push("force-unstable-if-unmarked=yes".into()); // ?? @@ -184,6 +150,45 @@ impl KaniSession { } } +pub fn base_rustc_flags(lib_path: PathBuf) -> Vec { + let kani_std_rlib = lib_path.join("libstd.rlib"); + let kani_std_wrapper = format!("noprelude:std={}", kani_std_rlib.to_str().unwrap()); + let sysroot = base_folder().unwrap(); + [ + "-C", + "overflow-checks=on", + "-C", + "panic=abort", + "-C", + "symbol-mangling-version=v0", + "-Z", + "unstable-options", + "-Z", + "panic_abort_tests=yes", + "-Z", + "trim-diagnostic-paths=no", + "-Z", + "human_readable_cgu_names", + "-Z", + "always-encode-mir", + "--cfg=kani", + "-Z", + "crate-attr=feature(register_tool)", + "-Z", + "crate-attr=register_tool(kanitool)", + "--sysroot", + sysroot.to_str().unwrap(), + "-L", + lib_path.to_str().unwrap(), + "--extern", + "kani", + "--extern", + kani_std_wrapper.as_str(), + ] + .map(OsString::from) + .to_vec() +} + /// This function can be used to convert Kani compiler specific arguments into a rustc one. /// We currently pass Kani specific arguments using the `--llvm-args` structure which is the /// hacky mechanism used by other rustc backend to receive arguments unknown to rustc. diff --git a/kani-driver/src/concrete_playback/mod.rs b/kani-driver/src/concrete_playback/mod.rs new file mode 100644 index 000000000000..ccad3877f66a --- /dev/null +++ b/kani-driver/src/concrete_playback/mod.rs @@ -0,0 +1,6 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Implements the logic related to concrete playback + +pub mod playback; +pub mod test_generator; diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs new file mode 100644 index 000000000000..b7ad89424db9 --- /dev/null +++ b/kani-driver/src/concrete_playback/playback.rs @@ -0,0 +1,125 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Implements the logic related to the playback subcommand +//! This can be achieved with playback --test + +use crate::args::common::Verbosity; +use crate::args::playback_args::{CargoPlaybackArgs, KaniPlaybackArgs, MessageFormat}; +use crate::call_single_file::base_rustc_flags; +use crate::session::{lib_playback_folder, InstallType}; +use crate::{session, util}; +use anyhow::Result; +use std::ffi::OsString; +use std::ops::Deref; +use std::path::{Path, PathBuf}; +use std::process::Command; +use tracing::debug; + +pub fn playback_cargo(args: CargoPlaybackArgs) -> Result<()> { + let install = InstallType::new()?; + cargo_test(&install, args) +} + +pub fn playback_standalone(args: KaniPlaybackArgs) -> Result<()> { + let install = InstallType::new()?; + let artifact = build_test(&install, &args)?; + debug!(?artifact, "playback_standalone"); + + if !args.playback.common_opts.quiet() { + print_artifact(&artifact, args.playback.message_format) + } + + if !args.playback.only_codegen { + run_test(&artifact, &args)?; + } + + Ok(()) +} + +fn print_artifact(artifact: &Path, format: MessageFormat) { + match format { + MessageFormat::Json => { + println!(r#"{{"artifact":"{}"}}"#, artifact.display()) + } + MessageFormat::Human => { + println!("Executable {}", artifact.display()) + } + } +} + +fn run_test(exe: &Path, args: &KaniPlaybackArgs) -> Result<()> { + let mut cmd = Command::new(exe); + cmd.arg(&args.playback.test); + + if args.playback.common_opts.verbose() { + cmd.arg("--nocapture"); + } + + session::run_terminal(&args.playback.common_opts, cmd)?; + Ok(()) +} + +fn build_test(install: &InstallType, args: &KaniPlaybackArgs) -> Result { + const TEST_BIN_NAME: &str = "kani_concrete_playback"; + + if !args.playback.common_opts.quiet() { + util::info_operation("Building", args.input.to_string_lossy().deref()); + } + + let mut rustc_args = base_rustc_flags(lib_playback_folder()?); + rustc_args.push("--test".into()); + rustc_args.push(OsString::from(&args.input)); + rustc_args.push(format!("--crate-name={TEST_BIN_NAME}").into()); + + if args.playback.common_opts.verbose() { + rustc_args.push("--verbose".into()); + } + + if args.playback.message_format == MessageFormat::Json { + rustc_args.push("--error-format=json".into()); + } + + let mut cmd = Command::new(&install.kani_compiler()?); + cmd.args(rustc_args); + + session::run_terminal(&args.playback.common_opts, cmd)?; + + Ok(PathBuf::from(TEST_BIN_NAME).canonicalize()?) +} + +/// 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<()> { + let rustc_args = base_rustc_flags(lib_playback_folder()?); + let mut cargo_args: Vec = vec!["test".into()]; + + if args.playback.common_opts.verbose() { + cargo_args.push("--verbose".into()); + } else if args.playback.common_opts.quiet { + cargo_args.push("--quiet".into()) + } + + if args.playback.message_format == MessageFormat::Json { + cargo_args.push("--message-format=json".into()); + } + + if args.playback.only_codegen { + cargo_args.push("--no-run".into()); + } + + cargo_args.append(&mut args.cargo.to_cargo_args()); + cargo_args.push(args.playback.test.into()); + + // Arguments that will only be passed to the target package. + let mut cmd = Command::new("cargo"); + 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 + .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(&OsString::from("\x1f"))) + .env("CARGO_TERM_PROGRESS_WHEN", "never"); + + session::run_terminal(&args.playback.common_opts, cmd)?; + Ok(()) +} diff --git a/kani-driver/src/concrete_playback.rs b/kani-driver/src/concrete_playback/test_generator.rs similarity index 100% rename from kani-driver/src/concrete_playback.rs rename to kani-driver/src/concrete_playback/test_generator.rs diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 6c6ddaa25475..ff0a97cce053 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -10,6 +10,8 @@ use anyhow::Result; use args::{check_is_valid, CargoKaniSubcommand}; use args_toml::join_args; +use crate::args::StandaloneSubcommand; +use crate::concrete_playback::playback::{playback_cargo, playback_standalone}; use crate::project::Project; use crate::session::KaniSession; use clap::Parser; @@ -61,9 +63,17 @@ fn cargokani_main(input_args: Vec) -> Result<()> { check_is_valid(&args); let session = session::KaniSession::new(args.verify_opts)?; - if let Some(CargoKaniSubcommand::Assess(args)) = args.command { - return assess::run_assess(session, *args); - } else if session.args.assess { + match args.command { + Some(CargoKaniSubcommand::Assess(args)) => { + return assess::run_assess(session, *args); + } + Some(CargoKaniSubcommand::Playback(args)) => { + return playback_cargo(*args); + } + None => {} + } + + if session.args.assess { return assess::run_assess(session, assess::AssessArgs::default()); } @@ -75,9 +85,13 @@ fn cargokani_main(input_args: Vec) -> Result<()> { fn standalone_main() -> Result<()> { let args = args::StandaloneArgs::parse(); check_is_valid(&args); - let session = session::KaniSession::new(args.verify_opts)?; - let project = project::standalone_project(&args.input, &session)?; + if let Some(StandaloneSubcommand::Playback(args)) = args.command { + return playback_standalone(*args); + } + + let session = session::KaniSession::new(args.verify_opts)?; + let project = project::standalone_project(&args.input.unwrap(), &session)?; if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } } diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 466e18c283ee..6a9bd411c879 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -1,6 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +use crate::args::common::Verbosity; use crate::args::VerificationArgs; use crate::util::render_command; use anyhow::{bail, Context, Result}; @@ -13,6 +14,7 @@ use strum_macros::Display; use tracing::level_filters::LevelFilter; use tracing_subscriber::{layer::SubscriberExt, EnvFilter, Registry}; use tracing_tree::HierarchicalLayer; + /// Environment variable used to control this session log tracing. /// This is the same variable used to control `kani-compiler` logs. Note that you can still control /// the driver logs separately, by using the logger directives to select the kani-driver crate. @@ -41,7 +43,7 @@ pub struct KaniSession { } /// Represents where we detected Kani, with helper methods for using that information to find critical paths -enum InstallType { +pub enum InstallType { /// We're operating in a a checked out repo that's been built locally. /// The path here is to the root of the repo. DevRepo(PathBuf), @@ -117,118 +119,151 @@ impl Drop for KaniSession { } impl KaniSession { - // The below suite of helper functions for executing Commands are meant to be a common handler - // for various cmdline flags like 'verbose' and 'quiet'. These functions are temporary: in the - // longer run we'll switch to a graph-interpreter style of constructing and executing jobs. - // (In other words: higher-level data structures, rather than passing around Commands.) - // (e.g. to support emitting Litani build graphs, or to better parallelize our work) - - // We basically have three different output policies: - // No error Error Notes - // Default Quiet Verbose Default Quiet Verbose - // run_terminal Y N Y Y N Y (inherits terminal) - // run_suppress N N Y Y N Y (buffered text only) - // run_redirect (not applicable, always to the file) (only option where error is acceptable) - - /// Run a job, leave it outputting to terminal (unless --quiet), and fail if there's a problem. - pub fn run_terminal(&self, mut cmd: Command) -> Result<()> { - if self.args.common_args.quiet { - cmd.stdout(std::process::Stdio::null()); - cmd.stderr(std::process::Stdio::null()); - } - if self.args.common_args.verbose { - println!("[Kani] Running: `{}`", render_command(&cmd).to_string_lossy()); - } - let program = cmd.get_program().to_string_lossy().to_string(); - let result = self.with_timer( - || { - cmd.status() - .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy())) - }, - &program, - )?; - if !result.success() { - bail!("{} exited with status {}", cmd.get_program().to_string_lossy(), result); - } - Ok(()) + /// Call [run_terminal] with the verbosity configured by the user. + pub fn run_terminal(&self, cmd: Command) -> Result<()> { + run_terminal(&self.args.common_args, cmd) } - /// Run a job, but only output (unless --quiet) if it fails, and fail if there's a problem. - pub fn run_suppress(&self, mut cmd: Command) -> Result<()> { - let verbosity = &self.args.common_args; - if verbosity.quiet | verbosity.verbose | verbosity.debug { - return self.run_terminal(cmd); - } - let result = cmd - .output() - .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()))?; - if !result.status.success() { - // Don't suppress the output. There doesn't seem to be a way to easily get Command - // to give one output stream of both out/err with interleaving correct, it seems - // you'd have to resort to some lower-level interface. - let stdout = std::io::stdout(); - let mut handle = stdout.lock(); - handle.write_all(&result.stdout)?; - handle.write_all(&result.stderr)?; - bail!("{} exited with status {}", cmd.get_program().to_string_lossy(), result.status); - } - Ok(()) + /// Call [run_suppress] with the verbosity configured by the user. + pub fn run_suppress(&self, cmd: Command) -> Result<()> { + run_suppress(&self.args.common_args, cmd) } - /// Run a job, redirect its output to a file, and allow the caller to decide what to do with failure. - pub fn run_redirect(&self, mut cmd: Command, stdout: &Path) -> Result { - if self.args.common_args.verbose { - println!( - "[Kani] Running: `{} > {}`", - render_command(&cmd).to_string_lossy(), - stdout.display() - ); - } - let output_file = std::fs::File::create(&stdout)?; - cmd.stdout(output_file); - - let program = cmd.get_program().to_string_lossy().to_string(); - self.with_timer( - || { - cmd.status() - .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy())) - }, - &program, - ) + /// Call [run_redirect] with the verbosity configured by the user. + pub fn run_redirect(&self, cmd: Command, stdout: &Path) -> Result { + run_redirect(&self.args.common_args, cmd, stdout) } - /// Run a job and pipe its output to this process. - /// Returns an error if the process could not be spawned. - /// - /// NOTE: Unlike other `run_` functions, this function does not attempt to indicate - /// the process exit code, you need to remember to check this yourself. - pub fn run_piped(&self, mut cmd: Command) -> Result> { - if self.args.common_args.verbose { - println!("[Kani] Running: `{}`", render_command(&cmd).to_string_lossy()); - } - // Run the process as a child process - let process = cmd - .stdout(Stdio::piped()) - .spawn() - .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()))?; - - Ok(Some(process)) + /// Call [run_piped] with the verbosity configured by the user. + pub fn run_piped(&self, cmd: Command) -> Result> { + run_piped(&self.args.common_args, cmd) } - /// Execute the provided function and measure the clock time it took for its execution. - /// Print the time with the given description if we are on verbose or debug mode. + /// Call [with_timer] with the verbosity configured by the user. pub fn with_timer(&self, func: F, description: &str) -> T where F: FnOnce() -> T, { - let start = Instant::now(); - let ret = func(); - if self.args.common_args.verbose || self.args.common_args.debug { - let elapsed = start.elapsed(); - println!("Finished {description} in {}s", elapsed.as_secs_f32()) - } - ret + with_timer(&self.args.common_args, func, description) + } +} + +// The below suite of helper functions for executing Commands are meant to be a common handler +// for various cmdline flags like 'verbose' and 'quiet'. These functions are temporary: in the +// longer run we'll switch to a graph-interpreter style of constructing and executing jobs. +// (In other words: higher-level data structures, rather than passing around Commands.) +// (e.g. to support emitting Litani build graphs, or to better parallelize our work) + +// We basically have three different output policies: +// No error Error Notes +// Default Quiet Verbose Default Quiet Verbose +// run_terminal Y N Y Y N Y (inherits terminal) +// run_suppress N N Y Y N Y (buffered text only) +// run_redirect (not applicable, always to the file) (only option where error is acceptable) + +/// Run a job, leave it outputting to terminal (unless --quiet), and fail if there's a problem. +pub fn run_terminal(verbosity: &impl Verbosity, mut cmd: Command) -> Result<()> { + if verbosity.quiet() { + cmd.stdout(std::process::Stdio::null()); + cmd.stderr(std::process::Stdio::null()); } + if verbosity.verbose() { + println!("[Kani] Running: `{}`", render_command(&cmd).to_string_lossy()); + } + let program = cmd.get_program().to_string_lossy().to_string(); + let result = with_timer( + verbosity, + || { + cmd.status() + .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy())) + }, + &program, + )?; + if !result.success() { + bail!("{} exited with status {}", cmd.get_program().to_string_lossy(), result); + } + Ok(()) +} + +/// Run a job, but only output (unless --quiet) if it fails, and fail if there's a problem. +pub fn run_suppress(verbosity: &impl Verbosity, mut cmd: Command) -> Result<()> { + if verbosity.is_set() { + return run_terminal(verbosity, cmd); + } + let result = cmd + .output() + .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()))?; + if !result.status.success() { + // Don't suppress the output. There doesn't seem to be a way to easily get Command + // to give one output stream of both out/err with interleaving correct, it seems + // you'd have to resort to some lower-level interface. + let stdout = std::io::stdout(); + let mut handle = stdout.lock(); + handle.write_all(&result.stdout)?; + handle.write_all(&result.stderr)?; + bail!("{} exited with status {}", cmd.get_program().to_string_lossy(), result.status); + } + Ok(()) +} + +/// Run a job, redirect its output to a file, and allow the caller to decide what to do with failure. +pub fn run_redirect( + verbosity: &impl Verbosity, + mut cmd: Command, + stdout: &Path, +) -> Result { + if verbosity.verbose() { + println!( + "[Kani] Running: `{} > {}`", + render_command(&cmd).to_string_lossy(), + stdout.display() + ); + } + let output_file = std::fs::File::create(&stdout)?; + cmd.stdout(output_file); + + let program = cmd.get_program().to_string_lossy().to_string(); + with_timer( + verbosity, + || { + cmd.status() + .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy())) + }, + &program, + ) +} + +/// Run a job and pipe its output to this process. +/// Returns an error if the process could not be spawned. +/// +/// NOTE: Unlike other `run_` functions, this function does not attempt to indicate +/// the process exit code, you need to remember to check this yourself. +pub fn run_piped(verbosity: &impl Verbosity, mut cmd: Command) -> Result> { + if verbosity.verbose() { + println!("[Kani] Running: `{}`", render_command(&cmd).to_string_lossy()); + } + // Run the process as a child process + let process = cmd + .stdout(Stdio::piped()) + .spawn() + .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()))?; + + Ok(Some(process)) +} + +/// Execute the provided function and measure the clock time it took for its execution. +/// Print the time with the given description if we are on verbose or debug mode. +fn with_timer(verbosity: &impl Verbosity, func: F, description: &str) -> T +where + F: FnOnce() -> T, +{ + let start = Instant::now(); + let ret = func(); + if verbosity.verbose() { + let elapsed = start.elapsed(); + println!("Finished {description} in {}s", elapsed.as_secs_f32()) + } + ret } /// Return the path for the folder where the current executable is located. @@ -243,6 +278,11 @@ pub fn lib_folder() -> Result { Ok(base_folder()?.join("lib")) } +/// Return the path for the folder where the pre-compiled rust libraries are located. +pub fn lib_playback_folder() -> Result { + Ok(base_folder()?.join("lib-playback")) +} + /// Return the base folder for the entire kani installation. pub fn base_folder() -> Result { Ok(bin_folder()? diff --git a/kani-driver/src/util.rs b/kani-driver/src/util.rs index 2a4f7f1d926e..66fc39e59841 100644 --- a/kani-driver/src/util.rs +++ b/kani-driver/src/util.rs @@ -176,6 +176,13 @@ pub fn error(msg: &str) { println!("{error} {msg_fmt}") } +/// Print an info message. This will print the stage in bold green and the rest in regular style. +pub fn info_operation(op: &str, msg: &str) { + let op_fmt = console::style(op).bold().green(); + let msg_fmt = console::style(msg); + println!("{op_fmt} {msg_fmt}") +} + #[cfg(test)] mod tests { use super::*; diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index d54684cbff87..6cded7052369 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -194,7 +194,7 @@ mod sysroot { /// This module provides dummy implementations of Kani attributes which cannot be interpreted by /// other tools such as MIRI and the regular rust compiler. /// -/// This allow users to use code marked with Kani attributes, for example, during concrete playback. +/// This allow users to use code marked with Kani attributes, for example, for IDE code inspection. #[cfg(not(kani_sysroot))] mod regular { use super::*; diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 550a9433bbfb..c8b1c941fdf0 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -12,3 +12,6 @@ publish = false [dependencies] kani = {path="../kani"} + +[features] +concrete_playback = ["kani/concrete_playback"] diff --git a/tests/script-based-pre/cargo_playback_opts/config.yml b/tests/script-based-pre/cargo_playback_opts/config.yml new file mode 100644 index 000000000000..6dd660716457 --- /dev/null +++ b/tests/script-based-pre/cargo_playback_opts/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: playback_opts.sh +expected: playback_opts.expected diff --git a/tests/script-based-pre/cargo_playback_opts/playback_opts.expected b/tests/script-based-pre/cargo_playback_opts/playback_opts.expected new file mode 100644 index 000000000000..571f9ef0dd9f --- /dev/null +++ b/tests/script-based-pre/cargo_playback_opts/playback_opts.expected @@ -0,0 +1,6 @@ +[TEST] Only codegen test... + Executable unittests src/lib.rs +[TEST] Only codegen test... + Finished test +[TEST] Executable +sample_crate/target/debug/deps/sample_crate- diff --git a/tests/script-based-pre/cargo_playback_opts/playback_opts.sh b/tests/script-based-pre/cargo_playback_opts/playback_opts.sh new file mode 100755 index 000000000000..8ee42bd5a140 --- /dev/null +++ b/tests/script-based-pre/cargo_playback_opts/playback_opts.sh @@ -0,0 +1,21 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set +e + +pushd sample_crate > /dev/null +cargo clean + +echo "[TEST] Only codegen test..." +cargo kani playback -Z concrete-playback --test kani_concrete_playback --only-codegen + +echo "[TEST] Only codegen test..." +output=$(cargo kani playback -Z concrete-playback --test kani_concrete_playback --only-codegen --message-format=json) +executable=$(echo ${output} | jq 'select(.reason == "compiler-artifact") | .executable') + +echo "[TEST] Executable" +echo ${executable} + +cargo clean +popd > /dev/null diff --git a/tests/script-based-pre/cargo_playback_opts/sample_crate/Cargo.toml b/tests/script-based-pre/cargo_playback_opts/sample_crate/Cargo.toml new file mode 100644 index 000000000000..c00d0ccc4bdb --- /dev/null +++ b/tests/script-based-pre/cargo_playback_opts/sample_crate/Cargo.toml @@ -0,0 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "sample_crate" +version = "0.1.0" +edition = "2021" diff --git a/tests/script-based-pre/cargo_playback_opts/sample_crate/src/lib.rs b/tests/script-based-pre/cargo_playback_opts/sample_crate/src/lib.rs new file mode 100644 index 000000000000..551f9f0830cb --- /dev/null +++ b/tests/script-based-pre/cargo_playback_opts/sample_crate/src/lib.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test is used to test playback command on a unit test generated by the concrete playback. + +#[cfg(kani)] +mod harnesses { + #[kani::proof] + fn harness() { + let result_1: Result = kani::any(); + let result_2: Result = kani::any(); + assert!(!(result_1 == Ok(101) && result_2 == Err(102))); + } + + #[test] + fn kani_concrete_playback_harness_15598097466099501582() { + let concrete_vals: Vec> = vec![ + // 1 + vec![1], + // 101 + vec![101], + // 0 + vec![0], + // 102 + vec![102], + ]; + kani::concrete_playback_run(concrete_vals, harness); + } +} diff --git a/tests/script-based-pre/concrete_playback_e2e/config.yml b/tests/script-based-pre/concrete_playback_e2e/config.yml new file mode 100644 index 000000000000..ba19d0233909 --- /dev/null +++ b/tests/script-based-pre/concrete_playback_e2e/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: playback_e2e.sh +expected: playback_e2e.expected diff --git a/tests/script-based-pre/concrete_playback_e2e/playback_e2e.expected b/tests/script-based-pre/concrete_playback_e2e/playback_e2e.expected new file mode 100644 index 000000000000..3af011d90695 --- /dev/null +++ b/tests/script-based-pre/concrete_playback_e2e/playback_e2e.expected @@ -0,0 +1,19 @@ +Run verification... +Checking harness verify::any_is_err... +Complete - 2 successfully verified harnesses, 0 failures, 2 total. + +Run ok test... +test verify::kani_concrete_playback_any_is_ok\ +\ +test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 1 filtered out; + +Run error test... +test verify::kani_concrete_playback_any_is_err\ +\ +test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 1 filtered out; + +Run all tests... +running 2 tests +test verify::kani_concrete_playback_any_is_err +test verify::kani_concrete_playback_any_is_ok +test result: ok. 2 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; diff --git a/tests/script-based-pre/concrete_playback_e2e/playback_e2e.sh b/tests/script-based-pre/concrete_playback_e2e/playback_e2e.sh new file mode 100755 index 000000000000..defe4d5d69d7 --- /dev/null +++ b/tests/script-based-pre/concrete_playback_e2e/playback_e2e.sh @@ -0,0 +1,29 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set +e + +OUT_DIR=tmp_sample_crate + +# Ensure output folder is clean +rm -rf ${OUT_DIR} + +# Move the original source to the output folder since it will be modified +cp -r sample_crate ${OUT_DIR} +pushd $OUT_DIR + +echo "Run verification..." +cargo kani + +echo "Run ok test..." +cargo kani playback -Z concrete-playback --test any_is_ok + +echo "Run error test..." +cargo kani playback -Z concrete-playback --test any_is_err + +echo "Run all tests..." +cargo kani playback -Z concrete-playback --test concrete_playback + +popd +rm -rf ${OUT_DIR} \ No newline at end of file diff --git a/tests/script-based-pre/concrete_playback_e2e/sample_crate/Cargo.toml b/tests/script-based-pre/concrete_playback_e2e/sample_crate/Cargo.toml new file mode 100644 index 000000000000..4a7016cb51ed --- /dev/null +++ b/tests/script-based-pre/concrete_playback_e2e/sample_crate/Cargo.toml @@ -0,0 +1,12 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "sample_crate" +version = "0.1.0" +edition = "2021" + +[package.metadata.kani.flags] +concrete-playback = "inplace" + +[package.metadata.kani.unstable] +concrete-playback = true diff --git a/tests/script-based-pre/concrete_playback_e2e/sample_crate/src/lib.rs b/tests/script-based-pre/concrete_playback_e2e/sample_crate/src/lib.rs new file mode 100644 index 000000000000..3cf83c8e3597 --- /dev/null +++ b/tests/script-based-pre/concrete_playback_e2e/sample_crate/src/lib.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks that we can correctly generate tests from a cover statement and run them. + +#[cfg(kani)] +mod verify { + #[kani::proof] + fn any_is_ok() { + let result: Result = kani::any(); + kani::cover!(result.is_ok()); + } + + #[kani::proof] + fn any_is_err() { + let result: Result = kani::any(); + kani::cover!(result.is_err()); + } +} diff --git a/tests/script-based-pre/playback_opts/config.yml b/tests/script-based-pre/playback_opts/config.yml new file mode 100644 index 000000000000..6dd660716457 --- /dev/null +++ b/tests/script-based-pre/playback_opts/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: playback_opts.sh +expected: playback_opts.expected diff --git a/tests/script-based-pre/playback_opts/original.rs b/tests/script-based-pre/playback_opts/original.rs new file mode 100644 index 000000000000..34879f77580f --- /dev/null +++ b/tests/script-based-pre/playback_opts/original.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that Kani correctly adds tests to the cover checks reachable in a harness. +//! This should emit two tests, but we currently only support one test. See +//! for more details. +extern crate kani; + +#[cfg(kani)] +mod verify { + use kani::cover; + use std::convert::TryFrom; + use std::num::NonZeroU8; + + #[kani::proof] + fn try_nz_u8() { + let val: u8 = kani::any(); + let result = NonZeroU8::try_from(val); + match result { + Ok(nz_val) => { + cover!(true, "Ok"); + assert_eq!(nz_val.get(), val); + } + Err(_) => { + cover!(true, "Not ok"); + assert_eq!(val, 0); + } + } + } +} diff --git a/tests/script-based-pre/playback_opts/playback_opts.expected b/tests/script-based-pre/playback_opts/playback_opts.expected new file mode 100644 index 000000000000..0f2f810c508f --- /dev/null +++ b/tests/script-based-pre/playback_opts/playback_opts.expected @@ -0,0 +1,12 @@ +[TEST] Generate test... +Checking harness verify::try_nz_u8 + +[TEST] Only codegen test... +Building modified.rs +playback_opts/kani_concrete_playback + +[TEST] Run test... +test result: ok. 1 passed; 0 failed; + +[TEST] Json format... +{"artifact": diff --git a/tests/script-based-pre/playback_opts/playback_opts.sh b/tests/script-based-pre/playback_opts/playback_opts.sh new file mode 100755 index 000000000000..51f108012f7b --- /dev/null +++ b/tests/script-based-pre/playback_opts/playback_opts.sh @@ -0,0 +1,24 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# Test that concrete playback -Z concrete-playback executes as expected +set -o pipefail +set -o nounset + +RS_FILE="modified.rs" +cp original.rs ${RS_FILE} + +echo "[TEST] Generate test..." +kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace + +echo "[TEST] Only codegen test..." +kani playback -Z concrete-playback --test kani_concrete_playback --only-codegen ${RS_FILE} + +echo "[TEST] Run test..." +kani playback -Z concrete-playback --test kani_concrete_playback ${RS_FILE} + +echo "[TEST] Json format..." +kani playback -Z concrete-playback --test kani_concrete_playback ${RS_FILE} --only-codegen --message-format=json + +# Cleanup +rm ${RS_FILE} diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs index 74958879679f..200614ae3c07 100644 --- a/tools/build-kani/src/main.rs +++ b/tools/build-kani/src/main.rs @@ -10,7 +10,7 @@ mod parser; mod sysroot; -use crate::sysroot::{build_bin, build_lib, kani_sysroot_lib}; +use crate::sysroot::{build_bin, build_lib, kani_playback_lib, kani_sysroot_lib}; use anyhow::{bail, Result}; use clap::Parser; use std::{ffi::OsString, path::Path, process::Command}; @@ -96,6 +96,7 @@ fn bundle_kani(dir: &Path) -> Result<()> { // 4. Pre-compiled library files cp_dir(&kani_sysroot_lib(), dir)?; + cp_dir(&kani_playback_lib(), dir)?; // 5. Record the exact toolchain we use std::fs::write(dir.join("rust-toolchain-version"), env!("RUSTUP_TOOLCHAIN"))?; diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index b53202ac4478..a4cef0e9bf3a 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -50,15 +50,38 @@ pub fn kani_sysroot_lib() -> PathBuf { path_buf!(kani_sysroot(), "lib") } +/// Returns the path to where Kani libraries for concrete playback is kept. +pub fn kani_playback_lib() -> PathBuf { + path_buf!(kani_sysroot(), "lib-playback") +} + /// Returns the path to where Kani's pre-compiled binaries are stored. pub fn kani_sysroot_bin() -> PathBuf { path_buf!(kani_sysroot(), "bin") } -/// Build the `lib/` folder for the new sysroot. -/// This will include Kani's libraries as well as the standard libraries compiled with --emit-mir. -/// TODO: Don't copy Kani's libstd. +/// Build the `lib/` folder and `lib-playback/` for the new sysroot. +/// - The `lib/` folder contains the sysroot for verification. +/// - The `lib-playback/` folder contains the sysroot used for playback. pub fn build_lib() -> Result<()> { + build_verification_lib()?; + build_playback_lib() +} + +/// Build the `lib/` folder for the new sysroot used during verification. +/// This will include Kani's libraries as well as the standard libraries compiled with --emit-mir. +fn build_verification_lib() -> Result<()> { + build_kani_lib(&kani_sysroot_lib(), &[]) +} + +/// Build the `lib-playback/` folder that will be used during counter example playback. +/// This will include Kani's libraries compiled with `concrete-playback` feature enabled. +fn build_playback_lib() -> Result<()> { + let extra_args = ["--features=std/concrete_playback,kani/concrete_playback"]; + build_kani_lib(&kani_playback_lib(), &extra_args) +} + +fn build_kani_lib(path: &Path, extra_args: &[&str]) -> Result<()> { // Run cargo build with -Z build-std let target = env!("TARGET"); let target_dir = env!("KANI_BUILD_LIBS"); @@ -101,6 +124,7 @@ pub fn build_lib() -> Result<()> { ["--cfg=kani", "--cfg=kani_sysroot", "-Z", "always-encode-mir"].join("\x1f"), ) .args(args) + .args(extra_args) .stdout(Stdio::piped()) .spawn() .expect("Failed to run `cargo build`."); @@ -115,7 +139,12 @@ pub fn build_lib() -> Result<()> { } // Create sysroot folder hierarchy. - let sysroot_lib = kani_sysroot_lib(); + copy_artifacts(&artifacts, path, target) +} + +/// Copy all the artifacts to their correct place to generate a valid sysroot. +fn copy_artifacts(artifacts: &[Artifact], sysroot_lib: &Path, target: &str) -> Result<()> { + // Create sysroot folder hierarchy. sysroot_lib.exists().then(|| fs::remove_dir_all(&sysroot_lib)); let std_path = path_buf!(&sysroot_lib, "rustlib", target, "lib"); fs::create_dir_all(&std_path).expect(&format!("Failed to create {std_path:?}")); @@ -124,7 +153,6 @@ pub fn build_lib() -> Result<()> { copy_libs(&artifacts, &sysroot_lib, &is_kani_lib); // Copy standard libraries into rustlib//lib/ folder. copy_libs(&artifacts, &std_path, &is_std_lib); - Ok(()) }