Support Cargo features in verify and build

Cargo.toml

@@ -24,6 +24,7 @@ path = "src/lib.rs"
 
 [dependencies]
 clap = { version = "4.5.35", features = ["derive"] }
+clap-cargo = "0.18.3"
 cargo_metadata = { version = "*" }
 memoize = { version = "*" }
 colored = { version = "*" }

README.md

@@ -29,6 +29,21 @@ pre-commit = "run --manifest-path dv/Cargo.toml --bin pre_commit --"
 cargo dv verify --targets <target1> <target2> ...
 ```
 
+### Cargo features and Verus arguments
+
+The `verify` and `build` commands accept Cargo's standard feature options:
+`-F`/`--features`, `--all-features`, and `--no-default-features`. DV forwards
+these options to `cargo-verus` before the verifier argument separator. Arguments
+after `--` continue to be passed directly to Verus.
+
+For example, this enables the `irc11` Cargo feature while asking Verus to check
+only one module:
+
+```bash
+cargo dv verify --targets ostd --features irc11 -- \
+  --verify-only-module sync::rcu
+```
+
 ## Bootstrapping Verus
 
 By default, `cargo dv bootstrap` builds the `main` branch of

src/main.rs

@@ -187,13 +187,6 @@ struct VerifyArgs {
     )]
     focus: bool,
 
-    #[arg(
-        last = true,
-        help = "Pass-through arguments to the Verus verifier",
-        allow_hyphen_values = true
-    )]
-    pass_through: Vec<String>,
-
     #[arg(
         short = 'c',
         long = "count-line",
@@ -202,6 +195,18 @@ struct VerifyArgs {
         action = ArgAction::SetTrue
     )]
     count_line: bool,
+
+    #[command(flatten, next_help_heading = "Cargo feature options")]
+    cargo_features: clap_cargo::Features,
+
+    #[arg(
+        last = true,
+        value_name = "VERUS_ARGS",
+        help = "Arguments passed to the Verus verifier after `--`",
+        help_heading = "Verus options",
+        allow_hyphen_values = true
+    )]
+    verus_args: Vec<String>,
 }
 
 #[derive(Parser, Debug)]
@@ -298,12 +303,17 @@ struct BuildArgs {
         action = ArgAction::SetTrue)]
     disasm: bool,
 
+    #[command(flatten, next_help_heading = "Cargo feature options")]
+    cargo_features: clap_cargo::Features,
+
     #[arg(
         last = true,
-        help = "Pass-through arguments to the Verus verifier",
+        value_name = "VERUS_ARGS",
+        help = "Arguments passed to the Verus verifier after `--`",
+        help_heading = "Verus options",
         allow_hyphen_values = true
     )]
-    pass_through: Vec<String>,
+    verus_args: Vec<String>,
 }
 
 #[derive(Parser, Debug)]
@@ -412,6 +422,21 @@ struct FmtArgs {
     paths: Vec<PathBuf>,
 }
 
+fn cargo_feature_args(features: &clap_cargo::Features) -> Vec<String> {
+    let mut args = Vec::new();
+    if features.all_features {
+        args.push("--all-features".to_string());
+    }
+    if features.no_default_features {
+        args.push("--no-default-features".to_string());
+    }
+    if !features.features.is_empty() {
+        args.push("--features".to_string());
+        args.push(features.features.join(" "));
+    }
+    args
+}
+
 fn verify(args: &VerifyArgs) -> Result<(), DynError> {
     let targets = args.targets.clone();
     let options = verus::ExtraOptions {
@@ -420,7 +445,8 @@ fn verify(args: &VerifyArgs) -> Result<(), DynError> {
         release: !args.debug,
         trace: args.trace,
         disasm: false,
-        pass_through: args.pass_through.clone(),
+        cargo_args: cargo_feature_args(&args.cargo_features),
+        verus_args: args.verus_args.clone(),
         count_line: args.count_line,
         focus: args.focus,
     };
@@ -462,7 +488,8 @@ fn build(args: &BuildArgs) -> Result<(), DynError> {
         trace: args.trace,
         release: !args.debug,
         disasm: args.disasm,
-        pass_through: args.pass_through.clone(),
+        cargo_args: cargo_feature_args(&args.cargo_features),
+        verus_args: args.verus_args.clone(),
         count_line: false,
         focus: false,
     };
@@ -555,6 +582,44 @@ fn main() {
 mod tests {
     use super::*;
 
+    #[test]
+    fn verify_separates_cargo_features_from_verus_arguments() {
+        let cli = Cli::try_parse_from([
+            "dv",
+            "verify",
+            "--features",
+            "irc11 alloc",
+            "--no-default-features",
+            "--",
+            "--verify-only-module",
+            "sync::rcu",
+        ])
+        .unwrap();
+
+        let Commands::Verify(args) = cli.command else {
+            panic!("expected verify command");
+        };
+        assert_eq!(args.cargo_features.features, ["irc11", "alloc"]);
+        assert!(args.cargo_features.no_default_features);
+        assert_eq!(
+            cargo_feature_args(&args.cargo_features),
+            ["--no-default-features", "--features", "irc11 alloc"]
+        );
+        assert_eq!(args.verus_args, ["--verify-only-module", "sync::rcu"]);
+    }
+
+    #[test]
+    fn build_accepts_all_features() {
+        let cli = Cli::try_parse_from(["dv", "build", "--all-features"]).unwrap();
+
+        let Commands::Build(args) = cli.command else {
+            panic!("expected build command");
+        };
+        assert!(args.cargo_features.all_features);
+        assert_eq!(cargo_feature_args(&args.cargo_features), ["--all-features"]);
+        assert!(args.verus_args.is_empty());
+    }
+
     #[test]
     fn bootstrap_accepts_upstream_irc11_build_argument() {
         let cli = Cli::try_parse_from([

src/verus.rs

@@ -191,8 +191,10 @@ pub struct ExtraOptions {
     pub max_errors: usize,
     /// needs to disassemble the output
     pub disasm: bool,
-    /// pass-through options to the verifier
-    pub pass_through: Vec<String>,
+    /// feature options passed to cargo-verus before the verifier separator
+    pub cargo_args: Vec<String>,
+    /// pass-through options to the Verus verifier
+    pub verus_args: Vec<String>,
     /// count lines of code
     pub count_line: bool,
     /// use cargo-verus focus instead of cargo-verus verify
@@ -623,13 +625,15 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<()
         cmd.env("RUSTC_BOOTSTRAP", "1")
             .env("VERUS_Z3_PATH", &z3)
             .arg(if options.focus { "focus" } else { "verify" });
-        if !options.focus && verus_args_should_apply_to_roots_only(&options.pass_through) {
+        if !options.focus && verus_args_should_apply_to_roots_only(&options.verus_args) {
             cmd.arg("--fwd-verus-args-to").arg("roots");
         }
-        if let Some(target) = target {
-            cmd.arg("-p").arg(&target.name);
-        }
-        cmd.arg("--target").arg(VERIFICATION_RUST_TARGET);
+        push_cargo_args(
+            cmd,
+            target.map(|target| target.name.as_str()),
+            &options.cargo_args,
+            false,
+        );
 
         let mut verus_args = Vec::new();
         if options.log {
@@ -643,10 +647,8 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<()
             verus_args.push("--emit=dep-info".to_string());
         }
         verus_args.push(format!("--multiple-errors={}", options.max_errors));
-        verus_args.extend(options.pass_through.clone());
-        if !verus_args.is_empty() {
-            cmd.arg("--").args(verus_args);
-        }
+        verus_args.extend(options.verus_args.clone());
+        push_verus_args(cmd, &verus_args);
 
         info!(
             "  {} {} {}",
@@ -839,6 +841,25 @@ fn verus_args_should_apply_to_roots_only(args: &[String]) -> bool {
     })
 }
 
+fn push_cargo_args(cmd: &mut Command, package: Option<&str>, cargo_args: &[String], release: bool) {
+    if let Some(package) = package {
+        cmd.arg("-p").arg(package);
+    }
+    // cargo-verus stops recognizing Verus-relevant Cargo options after options
+    // such as --release and --target, so features must be inserted first.
+    cmd.args(cargo_args);
+    if release {
+        cmd.arg("--release");
+    }
+    cmd.arg("--target").arg(VERIFICATION_RUST_TARGET);
+}
+
+fn push_verus_args(cmd: &mut Command, verus_args: &[String]) {
+    if !verus_args.is_empty() {
+        cmd.arg("--").args(verus_args);
+    }
+}
+
 pub fn disassemble(target: &VerusTarget) -> Result<(), DynError> {
     let objdump = commands::get_objdump();
     let cmd = &mut Command::new(&objdump);
@@ -878,16 +899,15 @@ pub fn exec_build(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(),
         cmd.env("RUSTC_BOOTSTRAP", "1")
             .env("VERUS_Z3_PATH", &z3)
             .arg("build");
-        if verus_args_should_apply_to_roots_only(&options.pass_through) {
+        if verus_args_should_apply_to_roots_only(&options.verus_args) {
             cmd.arg("--fwd-verus-args-to").arg("roots");
         }
-        if let Some(target) = target {
-            cmd.arg("-p").arg(&target.name);
-        }
-        if options.release {
-            cmd.arg("--release");
-        }
-        cmd.arg("--target").arg(VERIFICATION_RUST_TARGET);
+        push_cargo_args(
+            cmd,
+            target.map(|target| target.name.as_str()),
+            &options.cargo_args,
+            options.release,
+        );
 
         let mut verus_args = Vec::new();
         if options.log {
@@ -898,10 +918,8 @@ pub fn exec_build(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(),
             verus_args.push("--trace".to_string());
         }
         verus_args.push(format!("--multiple-errors={}", options.max_errors));
-        verus_args.extend(options.pass_through.clone());
-        if !verus_args.is_empty() {
-            cmd.arg("--").args(verus_args);
-        }
+        verus_args.extend(options.verus_args.clone());
+        push_verus_args(cmd, &verus_args);
 
         let target_name = target
             .map(|target| target.name.as_str())
@@ -954,6 +972,73 @@ pub fn exec_clean() -> Result<(), DynError> {
     }
 }
 
+#[cfg(test)]
+mod argument_tests {
+    use super::*;
+
+    #[test]
+    fn cargo_features_precede_target_and_verus_args() {
+        let mut cmd = Command::new("cargo-verus");
+        cmd.arg("verify");
+        push_cargo_args(
+            &mut cmd,
+            Some("ostd"),
+            &["--features".to_string(), "irc11".to_string()],
+            false,
+        );
+        push_verus_args(&mut cmd, &["--verify-only-module=sync::rcu".to_string()]);
+
+        let args = cmd
+            .get_args()
+            .map(|arg| arg.to_str().unwrap())
+            .collect::<Vec<_>>();
+        assert_eq!(
+            args,
+            [
+                "verify",
+                "-p",
+                "ostd",
+                "--features",
+                "irc11",
+                "--target",
+                VERIFICATION_RUST_TARGET,
+                "--",
+                "--verify-only-module=sync::rcu",
+            ]
+        );
+    }
+
+    #[test]
+    fn cargo_features_precede_release_for_build() {
+        let mut cmd = Command::new("cargo-verus");
+        cmd.arg("build");
+        push_cargo_args(
+            &mut cmd,
+            Some("ostd"),
+            &["--features".to_string(), "allow_panic".to_string()],
+            true,
+        );
+
+        let args = cmd
+            .get_args()
+            .map(|arg| arg.to_str().unwrap())
+            .collect::<Vec<_>>();
+        assert_eq!(
+            args,
+            [
+                "build",
+                "-p",
+                "ostd",
+                "--features",
+                "allow_panic",
+                "--release",
+                "--target",
+                VERIFICATION_RUST_TARGET,
+            ]
+        );
+    }
+}
+
 pub mod install {
     use super::*;
     use crate::toolchain;