diff --git a/README.md b/README.md index d87a94c..1105234 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,10 @@ # Rust Deductive Verifier -`cargo dv` is a thin project-specific wrapper around `cargo-verus`. -Verification and build commands are delegated to `cargo-verus verify`, -`cargo-verus focus`, and `cargo-verus build`, -while `cargo dv` keeps a few repository conveniences on top, -such as bootstrapping the Verus toolchain, formatting Verus/Rust sources, +`cargo dv` is a thin project-specific wrapper around `cargo-verus`. +Verification and build commands are delegated to `cargo-verus verify`, +`cargo-verus focus`, and `cargo-verus build`, +while `cargo dv` keeps a few repository conveniences on top, +such as bootstrapping the Verus toolchain, formatting Verus/Rust sources, generating docs, and running pre-commit checks. ## Deployment @@ -29,6 +29,33 @@ pre-commit = "run --manifest-path dv/Cargo.toml --bin pre_commit --" cargo dv verify --targets ... ``` +## Bootstrapping Verus + +By default, `cargo dv bootstrap` builds the `main` branch of +`asterinas/verus`. Use `--branch` to select another branch and repeat +`--build-arg` to pass additional arguments to `cargo-verus` when it builds +vstd. + +The `irc11` branch is hosted by `verus-lang/verus`, rather than the default +`asterinas/verus` remote, and requires its weak-memory vstd modules to be +enabled explicitly: + +```bash +cargo dv bootstrap --upstream-verus --branch irc11 \ + --build-arg=--vstd-weak-memory +``` + +For compatibility with the `irc11` branch's vargo spelling, DV translates +`--vstd-weak-memory` to the vstd feature arguments +`--features weak-memory` used by the current cargo-verus bootstrap path. + +The same arguments are honored by upgrades: + +```bash +cargo dv bootstrap --upgrade --upstream-verus --branch irc11 \ + --build-arg=--vstd-weak-memory +``` + Optionally, if you want to use the pre-commit hook, you can add the rusty-hook to your project: ```bash diff --git a/src/main.rs b/src/main.rs index 326ccbe..26a3565 100644 --- a/src/main.rs +++ b/src/main.rs @@ -113,6 +113,15 @@ struct BootstrapArgs { value_name = "BRANCH_NAME" )] branch: Option, + + #[arg( + long = "build-arg", + help = "An extra argument passed to `cargo-verus` when building vstd", + value_name = "ARG", + action = ArgAction::Append, + allow_hyphen_values = true + )] + build_args: Vec, } #[derive(Parser, Debug)] @@ -433,6 +442,7 @@ fn bootstrap(args: &BootstrapArgs) -> Result<(), DynError> { release: !args.debug, restart: args.restart, branch: args.branch.clone(), + build_args: args.build_args.clone(), force_reset: args.upgrade, upstream_verus: args.upstream_verus, }; @@ -540,3 +550,28 @@ fn main() { error!("Error when executing command `{:?}`: {}", cli.command, e); } } + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn bootstrap_accepts_upstream_irc11_build_argument() { + let cli = Cli::try_parse_from([ + "dv", + "bootstrap", + "--upstream-verus", + "--branch", + "irc11", + "--build-arg=--vstd-weak-memory", + ]) + .unwrap(); + + let Commands::Bootstrap(args) = cli.command else { + panic!("expected bootstrap command"); + }; + assert!(args.upstream_verus); + assert_eq!(args.branch.as_deref(), Some("irc11")); + assert_eq!(args.build_args, ["--vstd-weak-memory"]); + } +} diff --git a/src/verus.rs b/src/verus.rs index 6eab3b7..e0b0262 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -970,6 +970,7 @@ pub mod install { pub restart: bool, pub release: bool, pub branch: Option, + pub build_args: Vec, pub force_reset: bool, pub upstream_verus: bool, } @@ -1264,7 +1265,29 @@ pub mod install { Ok(()) } - pub fn build_verus(release: bool) -> Result<(), DynError> { + fn vstd_build_args(release: bool, extra_args: &[String]) -> Vec { + let mut args = vec![ + "-p".to_string(), + "cargo-verus".to_string(), + "--".to_string(), + "build".to_string(), + ]; + if release { + args.push("--release".to_string()); + } + args.extend(["--manifest-path".to_string(), "vstd/Cargo.toml".to_string()]); + + for arg in extra_args { + if arg == "--vstd-weak-memory" { + args.extend(["--features".to_string(), "weak-memory".to_string()]); + } else { + args.push(arg.clone()); + } + } + args + } + + pub fn build_verus(release: bool, extra_args: &[String]) -> Result<(), DynError> { let toolchain = verus_dir().join("rust-toolchain.toml"); let toolchain_name = toolchain::load_toolchain(&toolchain); let source_dir = verus_source_dir(); @@ -1290,11 +1313,7 @@ pub mod install { if release { vstd_cmd.arg("--release"); } - vstd_cmd.args(["-p", "cargo-verus", "--", "build"]); - if release { - vstd_cmd.arg("--release"); - } - vstd_cmd.args(["--manifest-path", "vstd/Cargo.toml"]); + vstd_cmd.args(vstd_build_args(release, extra_args)); for (mut cmd, description) in [ (clean_cmd, "Cleaning the Verus workspace"), @@ -1341,7 +1360,7 @@ pub mod install { install_z3()?; // Build Verus - build_verus(options.release)?; + build_verus(options.release, &options.build_args)?; // Update the workspace toolchain toolchain::sync_toolchain( @@ -1547,7 +1566,7 @@ pub mod install { status!("Verus repo updated to the latest version"); // Build Verus - build_verus(options.release)?; + build_verus(options.release, &options.build_args)?; // Update the workspace toolchain toolchain::sync_toolchain( @@ -1561,4 +1580,45 @@ pub mod install { status!("Verus upgrade complete"); Ok(()) } + + #[cfg(test)] + mod tests { + use super::*; + + #[test] + fn irc11_build_argument_enables_weak_memory_for_vstd() { + let extra_args = vec!["--vstd-weak-memory".to_string()]; + assert_eq!( + vstd_build_args(true, &extra_args), + [ + "-p", + "cargo-verus", + "--", + "build", + "--release", + "--manifest-path", + "vstd/Cargo.toml", + "--features", + "weak-memory", + ] + ); + } + + #[test] + fn extra_vstd_build_arguments_are_forwarded() { + let extra_args = vec!["--locked".to_string()]; + assert_eq!( + vstd_build_args(false, &extra_args), + [ + "-p", + "cargo-verus", + "--", + "build", + "--manifest-path", + "vstd/Cargo.toml", + "--locked", + ] + ); + } + } }