Add --manifest-path and --features (#2085)

kani-driver/src/args.rs

@@ -4,14 +4,14 @@
 #[cfg(feature = "unsound_experiments")]
 use crate::unsound_experiments::UnsoundExperimentArgs;
 
-use clap::{error::Error, error::ErrorKind, CommandFactory, Parser, ValueEnum};
+use clap::{error::Error, error::ErrorKind, CommandFactory, ValueEnum};
 use std::ffi::OsString;
 use std::path::PathBuf;
 
 // By default we configure CBMC to use 16 bits to represent the object bits in pointers.
 const DEFAULT_OBJECT_BITS: u32 = 16;
 
-#[derive(Debug, Parser)]
+#[derive(Debug, clap::Parser)]
 #[command(
     version,
     name = "kani",
@@ -26,7 +26,7 @@ pub struct StandaloneArgs {
     pub common_opts: KaniArgs,
 }
 
-#[derive(Debug, Parser)]
+#[derive(Debug, clap::Parser)]
 #[command(
     version,
     name = "cargo-kani",
@@ -42,15 +42,15 @@ pub struct CargoKaniArgs {
 }
 
 // cargo-kani takes optional subcommands to request specialized behavior
-#[derive(Debug, Parser)]
+#[derive(Debug, clap::Subcommand)]
 pub enum CargoKaniSubcommand {
     #[command(hide = true)]
     Assess(crate::assess::AssessArgs),
 }
 
 // Common arguments for invoking Kani. This gets put into KaniContext, whereas
 // anything above is "local" to "main"'s control flow.
-#[derive(Debug, Parser)]
+#[derive(Debug, clap::Args)]
 pub struct KaniArgs {
     /// Temporary option to trigger assess mode for out test suite
     /// where we are able to add options but not subcommands
@@ -98,8 +98,7 @@ pub struct KaniArgs {
     /// Generate C file equivalent to inputted program.
     /// This feature is unstable and it requires `--enable-unstable` to be used
     #[arg(long, hide_short_help = true, requires("enable_unstable"),
-        conflicts_with_all(&["function", "legacy_linker"])
-)]
+        conflicts_with_all(&["function", "legacy_linker"]))]
     pub gen_c: bool,
 
     /// Directory for all generated artifacts.
@@ -149,16 +148,6 @@ pub struct KaniArgs {
     #[arg(long, conflicts_with("legacy_linker"), hide = true)]
     pub mir_linker: bool,
 
-    /// Compiles Kani harnesses in all features of all packages selected on the command-line.
-    #[arg(long)]
-    pub all_features: bool,
-    /// Run Kani on 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>,
-
     /// Specify the value used for loop unwinding in CBMC
     #[arg(long)]
     pub default_unwind: Option<u32>,
@@ -241,6 +230,10 @@ pub struct KaniArgs {
         conflicts_with("concrete_playback")
     )]
     pub enable_stubbing: bool,
+
+    /// Arguments to pass down to Cargo
+    #[command(flatten)]
+    pub cargo: CargoArgs,
 }
 
 impl KaniArgs {
@@ -273,6 +266,51 @@ impl KaniArgs {
     }
 }
 
+/// 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, 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 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>,
+}
+
+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
+    }
+}
+
 #[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum)]
 pub enum ConcretePlaybackMode {
     Print,
@@ -314,7 +352,7 @@ impl AbstractionType {
     }
 }
 
-#[derive(Debug, Parser)]
+#[derive(Debug, clap::Args)]
 pub struct CheckArgs {
     // Rust argument parsers (/clap) don't have the convenient '--flag' and '--no-flag' boolean pairs, so approximate
     // We're put both here then create helper functions to "intepret"
@@ -409,7 +447,7 @@ impl CargoKaniArgs {
     }
 }
 impl KaniArgs {
-    pub fn validate<T: Parser>(&self) {
+    pub fn validate<T: clap::Parser>(&self) {
         self.validate_inner()
             .or_else(|e| -> Result<(), ()> { e.format(&mut T::command()).exit() })
             .unwrap()
@@ -501,29 +539,37 @@ impl KaniArgs {
 
 #[cfg(test)]
 mod tests {
+    use clap::Parser;
+
     use super::*;
 
     #[test]
     fn check_arg_parsing() {
-        let a = StandaloneArgs::parse_from(vec![
+        let a = StandaloneArgs::try_parse_from(vec![
             "kani",
             "file.rs",
             "--enable-unstable",
             "--cbmc-args",
             "--multiple",
             "args",
             "--here",
-        ]);
+        ])
+        .unwrap();
         assert_eq!(a.common_opts.cbmc_args, vec!["--multiple", "args", "--here"]);
-        let _b =
-            StandaloneArgs::parse_from(vec!["kani", "file.rs", "--enable-unstable", "--cbmc-args"]);
+        let _b = StandaloneArgs::try_parse_from(vec![
+            "kani",
+            "file.rs",
+            "--enable-unstable",
+            "--cbmc-args",
+        ])
+        .unwrap();
         // no assertion: the above might fail if it fails to allow 0 args to cbmc-args
     }
     #[test]
     fn check_multiple_packages() {
         // accepts repeated:
-        let a = CargoKaniArgs::parse_from(vec!["cargo-kani", "-p", "a", "-p", "b"]);
-        assert_eq!(a.common_opts.package, vec!["a".to_owned(), "b".to_owned()]);
+        let a = CargoKaniArgs::try_parse_from(vec!["cargo-kani", "-p", "a", "-p", "b"]).unwrap();
+        assert_eq!(a.common_opts.cargo.package, vec!["a".to_owned(), "b".to_owned()]);
         let b = CargoKaniArgs::try_parse_from(vec![
             "cargo-kani",
             "-p",
@@ -576,15 +622,19 @@ mod tests {
     fn check_dry_run_fails() {
         // We don't support --dry-run anymore but we print a friendly reminder for now.
         let args = vec!["kani", "file.rs", "--dry-run"];
-        let err = StandaloneArgs::parse_from(&args).common_opts.validate_inner().unwrap_err();
+        let err = StandaloneArgs::try_parse_from(&args)
+            .unwrap()
+            .common_opts
+            .validate_inner()
+            .unwrap_err();
         assert_eq!(err.kind(), ErrorKind::ValueValidation);
     }
 
     /// Kani should fail if the argument given is not a file.
     #[test]
     fn check_invalid_input_fails() {
         let args = vec!["kani", "."];
-        let err = StandaloneArgs::parse_from(&args).valid_input().unwrap_err();
+        let err = StandaloneArgs::try_parse_from(&args).unwrap().valid_input().unwrap_err();
         assert_eq!(err.kind(), ErrorKind::InvalidValue);
     }
 
@@ -644,7 +694,7 @@ mod tests {
 
     /// Check if parsing the given argument string results in the given error.
     fn expect_validation_error(arg: &str, err: ErrorKind) {
-        let args = StandaloneArgs::parse_from(arg.split_whitespace());
+        let args = StandaloneArgs::try_parse_from(arg.split_whitespace()).unwrap();
         assert_eq!(args.common_opts.validate_inner().unwrap_err().kind(), err);
     }
 
@@ -674,4 +724,17 @@ mod tests {
                 .unwrap_err();
         assert_eq!(err.kind(), ErrorKind::ArgumentConflict);
     }
+
+    #[test]
+    fn check_features_parsing() {
+        fn parse(args: &[&str]) -> Vec<String> {
+            CargoKaniArgs::try_parse_from(args).unwrap().common_opts.cargo.features()
+        }
+
+        // spaces, commas, multiple repeated args, all ok
+        assert_eq!(parse(&["kani", "--features", "a b c"]), ["a", "b", "c"]);
+        assert_eq!(parse(&["kani", "--features", "a,b,c"]), ["a", "b", "c"]);
+        assert_eq!(parse(&["kani", "--features", "a", "--features", "b,c"]), ["a", "b", "c"]);
+        assert_eq!(parse(&["kani", "--features", "a b", "-Fc"]), ["a", "b", "c"]);
+    }
 }

kani-driver/src/args_toml.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use anyhow::{bail, Result};
+use clap::Parser;
 use std::collections::BTreeMap;
 use std::ffi::OsString;
 use std::path::PathBuf;
@@ -13,7 +14,7 @@ use toml::Value;
 ///
 /// The arguments passed via command line have precedence over the ones from the Cargo.toml.
 pub fn join_args(input_args: Vec<OsString>) -> Result<Vec<OsString>> {
-    let toml_path = cargo_locate_project();
+    let toml_path = cargo_locate_project(&input_args);
     if toml_path.is_err() {
         // We're not inside a Cargo project. Don't error... yet.
         return Ok(input_args);
@@ -65,16 +66,23 @@ fn merge_args(
 }
 
 /// `locate-project` produces a response like: `/full/path/to/src/cargo-kani/Cargo.toml`
-fn cargo_locate_project() -> Result<PathBuf> {
-    let cmd =
-        Command::new("cargo").args(["locate-project", "--message-format", "plain"]).output()?;
-    if !cmd.status.success() {
-        let err = std::str::from_utf8(&cmd.stderr)?;
-        bail!("{}", err);
+fn cargo_locate_project(input_args: &[OsString]) -> Result<PathBuf> {
+    // Try parsing our command line arguments as they presently look, to see if a "manifest-path" has been given.
+    let current_args = crate::args::CargoKaniArgs::parse_from(input_args);
+
+    if let Some(path) = current_args.common_opts.cargo.manifest_path {
+        Ok(path)
+    } else {
+        let cmd =
+            Command::new("cargo").args(["locate-project", "--message-format", "plain"]).output()?;
+        if !cmd.status.success() {
+            let err = std::str::from_utf8(&cmd.stderr)?;
+            bail!("{}", err);
+        }
+        let path = std::str::from_utf8(&cmd.stdout)?;
+        // A trim is essential: remove the trailing newline
+        Ok(path.trim().into())
     }
-    let path = std::str::from_utf8(&cmd.stdout)?;
-    // A trim is essential: remove the trailing newline
-    Ok(path.trim().into())
 }
 
 /// Parse a config toml string and extract the cargo-kani arguments we should try injecting.

kani-driver/src/assess/mod.rs

@@ -119,7 +119,7 @@ fn reconstruct_metadata_structure(
     let mut remaining_metas = kani_metadata.to_owned();
     let mut package_metas = vec![];
     for package in cargo_metadata.workspace_packages() {
-        if !session.args.package.is_empty() {
+        if !session.args.cargo.package.is_empty() {
             // If a specific package (set) is requested, skip all other packages.
             // This is a necessary workaround because we're reconstructing which metas go to which packages
             // based on the "crate name" given to the target, and the same workspace can have two
@@ -129,7 +129,7 @@ fn reconstruct_metadata_structure(
             // The best we can do for now is ignore packages we know we didn't build, to reduce the amount
             // of confusion we might suffer here (which at least solves the problem for 'scan' which only
             // builds 1 package at a time.)
-            if !session.args.package.contains(&package.name) {
+            if !session.args.cargo.package.contains(&package.name) {
                 continue;
             }
         }