diff --git a/Cargo.lock b/Cargo.lock index d03ef6d..af7878e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -243,6 +243,16 @@ dependencies = [ "clap_derive", ] +[[package]] +name = "clap-cargo" +version = "0.18.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "936551935c8258754bb8216aec040957d261f977303754b9bf1a213518388006" +dependencies = [ + "anstyle", + "clap", +] + [[package]] name = "clap_builder" version = "4.6.0" @@ -1154,6 +1164,7 @@ dependencies = [ "askama", "cargo_metadata", "clap", + "clap-cargo", "colored", "dotenv", "git2", diff --git a/Cargo.toml b/Cargo.toml index f465bd8..0d3a16e 100644 --- a/Cargo.toml +++ b/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 = "*" } diff --git a/README.md b/README.md index 1105234..454eed6 100644 --- a/README.md +++ b/README.md @@ -29,6 +29,21 @@ pre-commit = "run --manifest-path dv/Cargo.toml --bin pre_commit --" cargo dv verify --targets ... ``` +### 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 diff --git a/src/main.rs b/src/main.rs index 26a3565..ffbc94b 100644 --- a/src/main.rs +++ b/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, - #[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, } #[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, + verus_args: Vec, } #[derive(Parser, Debug)] @@ -412,6 +422,21 @@ struct FmtArgs { paths: Vec, } +fn cargo_feature_args(features: &clap_cargo::Features) -> Vec { + 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([ diff --git a/src/verus.rs b/src/verus.rs index 822094c..e9fcdcd 100644 --- a/src/verus.rs +++ b/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, + /// feature options passed to cargo-verus before the verifier separator + pub cargo_args: Vec, + /// pass-through options to the Verus verifier + pub verus_args: Vec, /// 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::>(); + 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::>(); + assert_eq!( + args, + [ + "build", + "-p", + "ostd", + "--features", + "allow_panic", + "--release", + "--target", + VERIFICATION_RUST_TARGET, + ] + ); + } +} + pub mod install { use super::*; use crate::toolchain;