Create a playback command to make it easier to run Kani generated tes…

…ts (#2464)

Introduce the unstable subcommand playback to allow users to easily compile and run their test cases that were generated using Kani's concrete playback feature.

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
+    }
+}

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<PathBuf>,
 
     #[command(flatten)]
     pub verify_opts: VerificationArgs,
+
+    #[command(subcommand)]
+    pub command: Option<StandaloneSubcommand>,
+}
+
+/// 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<playback_args::KaniPlaybackArgs>),
 }
 
 #[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<crate::assess::AssessArgs>),
+
+    /// Execute concrete playback testcases of a local package.
+    Playback(Box<playback_args::CargoPlaybackArgs>),
 }
 
 // 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<OsString> {
+        let mut cargo_args: Vec<OsString> = 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,23 +518,44 @@ 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<T> ValidateArgs for Option<T>
+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(),
         }
     }
 }
 
 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(..))));
+    }
 }

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);
+    }
+}