Polish cargo test arguments + add test (rust-lang#2492)

This is a continuation from rust-lang#2491. For completeness, I'm adding --bin option. I've also added a test for these options. Finally, I moved cargo specific arguments to its own module.

Author: celinval

kani-driver/src/args/cargo.rs

@@ -0,0 +1,140 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Module that define parsers that mimic Cargo options.
+
+use crate::args::ValidateArgs;
+use clap::error::Error;
+use std::ffi::OsString;
+use std::path::PathBuf;
+
+/// Arguments that Kani pass down into Cargo essentially uninterpreted.
+/// These generally have to do with selection of packages or activation of features.
+/// These do not (currently) include cargo args that kani pays special attention to:
+/// for instance, we keep `--tests` and `--target-dir` elsewhere.
+#[derive(Debug, Default, clap::Args)]
+pub struct CargoCommonArgs {
+    /// Activate all package features
+    #[arg(long)]
+    pub all_features: bool,
+    /// Do not activate the `default` feature
+    #[arg(long)]
+    pub no_default_features: bool,
+
+    // This tolerates spaces too, but we say "comma" only because this is the least error-prone approach...
+    /// Comma separated list of package features to activate
+    #[arg(short = 'F', long)]
+    features: Vec<String>,
+
+    /// Path to Cargo.toml
+    #[arg(long, name = "PATH")]
+    pub manifest_path: Option<PathBuf>,
+
+    /// Build all packages in the workspace
+    #[arg(long)]
+    pub workspace: bool,
+
+    /// Run Kani on the specified packages.
+    #[arg(long, short, conflicts_with("workspace"), num_args(1..))]
+    pub package: Vec<String>,
+
+    /// Exclude the specified packages
+    #[arg(long, short, requires("workspace"), conflicts_with("package"), num_args(1..))]
+    pub exclude: Vec<String>,
+}
+
+impl CargoCommonArgs {
+    /// Parse the string we're given into a list of feature names
+    ///
+    /// clap can't do this for us because it accepts multiple different delimeters
+    pub fn features(&self) -> Vec<String> {
+        let mut result = Vec::new();
+
+        for s in &self.features {
+            for piece in s.split(&[' ', ',']) {
+                result.push(piece.to_owned());
+            }
+        }
+        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 CargoCommonArgs {
+    fn validate(&self) -> Result<(), Error> {
+        Ok(())
+    }
+}
+
+/// Arguments that Kani pass down into Cargo test essentially uninterpreted.
+#[derive(Debug, Default, clap::Args)]
+pub struct CargoTestArgs {
+    /// Test only the specified binary target.
+    #[arg(long)]
+    pub bin: Vec<String>,
+
+    /// Test all binaries.
+    #[arg(long)]
+    pub bins: bool,
+
+    /// Test only the package's library unit tests.
+    #[arg(long)]
+    pub lib: bool,
+
+    /// Arguments to pass down to Cargo
+    #[command(flatten)]
+    pub common: CargoCommonArgs,
+}
+
+impl CargoTestArgs {
+    /// Convert the arguments back to a format that cargo can understand.
+    pub fn to_cargo_args(&self) -> Vec<OsString> {
+        let mut cargo_args = self.common.to_cargo_args();
+
+        if self.bins {
+            cargo_args.push("--bins".into());
+        }
+
+        if self.lib {
+            cargo_args.push("--lib".into());
+        }
+
+        cargo_args.extend(self.bin.iter().map(|binary| format!("--bin={binary}").into()));
+        cargo_args
+    }
+}
+
+/// Leave it for Cargo to validate these for now.
+impl ValidateArgs for CargoTestArgs {
+    fn validate(&self) -> Result<(), Error> {
+        self.common.validate()
+    }
+}

kani-driver/src/args/mod.rs

@@ -3,13 +3,15 @@
 //! Module that define Kani's command line interface. This includes all subcommands.
 
 pub mod assess_args;
+pub mod cargo;
 pub mod common;
 pub mod playback_args;
 
 pub use assess_args::*;
 
 use self::common::*;
 use crate::util::warning;
+use cargo::CargoCommonArgs;
 use clap::builder::{PossibleValue, TypedValueParser};
 use clap::{error::ContextKind, error::ContextValue, error::Error, error::ErrorKind, ValueEnum};
 use kani_metadata::CbmcSolver;
@@ -295,7 +297,7 @@ pub struct VerificationArgs {
 
     /// Arguments to pass down to Cargo
     #[command(flatten)]
-    pub cargo: CargoArgs,
+    pub cargo: CargoCommonArgs,
 
     #[command(flatten)]
     pub common_args: CommonArgs,
@@ -331,93 +333,6 @@ impl VerificationArgs {
     }
 }
 
-/// Arguments that Kani pass down into Cargo essentially uninterpreted.
-/// These generally have to do with selection of packages or activation of features.
-/// These do not (currently) include cargo args that kani pays special attention to:
-/// for instance, we keep `--tests` and `--target-dir` elsewhere.
-#[derive(Debug, Default, clap::Args)]
-pub struct CargoArgs {
-    /// Activate all package features
-    #[arg(long)]
-    pub all_features: bool,
-    /// Do not activate the `default` feature
-    #[arg(long)]
-    pub no_default_features: bool,
-
-    // This tolerates spaces too, but we say "comma" only because this is the least error-prone approach...
-    /// Comma separated list of package features to activate
-    #[arg(short = 'F', long)]
-    features: Vec<String>,
-
-    /// Path to Cargo.toml
-    #[arg(long, name = "PATH")]
-    pub manifest_path: Option<PathBuf>,
-
-    /// Build all packages in the workspace
-    #[arg(long)]
-    pub workspace: bool,
-
-    /// Run Kani on the specified packages.
-    #[arg(long, short, conflicts_with("workspace"), num_args(1..))]
-    pub package: Vec<String>,
-
-    /// Exclude the specified packages
-    #[arg(long, short, requires("workspace"), conflicts_with("package"), num_args(1..))]
-    pub exclude: Vec<String>,
-}
-
-impl CargoArgs {
-    /// Parse the string we're given into a list of feature names
-    ///
-    /// clap can't do this for us because it accepts multiple different delimeters
-    pub fn features(&self) -> Vec<String> {
-        let mut result = Vec::new();
-
-        for s in &self.features {
-            for piece in s.split(&[' ', ',']) {
-                result.push(piece.to_owned());
-            }
-        }
-        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)]
 pub enum ConcretePlaybackMode {
     Print,

kani-driver/src/args/playback_args.rs

@@ -2,8 +2,9 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! Implements the subcommand handling of the playback subcommand
 
+use crate::args::cargo::CargoTestArgs;
 use crate::args::common::UnstableFeatures;
-use crate::args::{CargoArgs, CommonArgs, ValidateArgs};
+use crate::args::{CommonArgs, ValidateArgs};
 use clap::error::ErrorKind;
 use clap::{Error, Parser, ValueEnum};
 use std::path::PathBuf;
@@ -14,17 +15,9 @@ pub struct CargoPlaybackArgs {
     #[command(flatten)]
     pub playback: PlaybackArgs,
 
-    /// Test all binaries.
-    #[arg(long)]
-    pub bins: bool,
-
-    /// Test only the package's library unit tests.
-    #[arg(long)]
-    pub lib: bool,
-
-    /// Arguments to pass down to Cargo
+    /// Arguments to pass down to Cargo that are specific to tests.
     #[command(flatten)]
-    pub cargo: CargoArgs,
+    pub cargo: CargoTestArgs,
 }
 
 /// Execute concrete playback testcases of a local crate.
@@ -126,7 +119,7 @@ mod tests {
         let input = "playback -Z concrete-playback -p PKG_NAME".split_whitespace();
         let args = CargoPlaybackArgs::try_parse_from(input).unwrap();
         args.validate().unwrap();
-        assert_eq!(&args.cargo.package, &["PKG_NAME"])
+        assert_eq!(&args.cargo.common.package, &["PKG_NAME"])
     }
 
     #[test]

kani-driver/src/concrete_playback/playback.rs

@@ -112,14 +112,6 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> {
         cargo_args.push("--no-run".into());
     }
 
-    if args.bins {
-        cargo_args.push("--bins".into());
-    }
-
-    if args.lib {
-        cargo_args.push("--lib".into());
-    }
-
     cargo_args.append(&mut args.cargo.to_cargo_args());
     cargo_args.push("--target".into());
     cargo_args.push(env!("TARGET").into());

tests/script-based-pre/cargo_playback_target/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: playback_target.sh
+expected: playback_target.expected

tests/script-based-pre/cargo_playback_target/playback_target.expected

@@ -0,0 +1,14 @@
+[TEST] Run all...\
+test verify::kani_concrete_playback_cover_bar_1234\
+test verify::kani_concrete_playback_cover_foo_1234\
+test verify::kani_concrete_playback_cover_lib_1234
+
+[TEST] Run lib...\
+test verify::kani_concrete_playback_cover_lib_1234
+
+[TEST] Run bins...\
+test verify::kani_concrete_playback_cover_bar_1234\
+test verify::kani_concrete_playback_cover_foo_1234
+
+[TEST] Only foo tests...\
+test verify::kani_concrete_playback_cover_foo_1234

tests/script-based-pre/cargo_playback_target/playback_target.sh

@@ -0,0 +1,36 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set +e
+
+function check_playback {
+  local OUTPUT=output.log
+  cargo kani playback "${@}" >& $OUTPUT
+  # Sort output so we can rely on the order.
+  echo "$(grep "test verify::.* ok" $OUTPUT | sort)"
+  echo
+  echo "======= Raw Output ======="
+  cat $OUTPUT
+  echo "=========================="
+  echo
+  rm $OUTPUT
+}
+
+pushd sample_crate > /dev/null
+cargo clean
+
+echo "[TEST] Run all..."
+check_playback -Z concrete-playback
+
+echo "[TEST] Run lib..."
+check_playback -Z concrete-playback --lib
+
+echo "[TEST] Run bins..."
+check_playback -Z concrete-playback --bins
+
+echo "[TEST] Only foo tests..."
+check_playback -Z concrete-playback --bin foo
+
+cargo clean
+popd > /dev/null

tests/script-based-pre/cargo_playback_target/sample_crate/Cargo.toml

@@ -0,0 +1,17 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "sample_crate"
+version = "0.1.0"
+edition = "2021"
+doctest = false
+
+[[bin]]
+name = "foo"
+doctest = false
+
+
+[[bin]]
+name = "bar"
+doctest = false
+