diff --git a/MODULE.bazel b/MODULE.bazel index 4f86bf6..60f6e4b 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -18,7 +18,13 @@ bazel_dep(name = "platforms", version = "0.0.10") # Low minimum version: consumers control their own rules_rust version. # Consumers MUST register a Rust toolchain that includes the version # matching Verus's rust_verify (see rust_version in extensions.bzl). -bazel_dep(name = "rules_rust", version = "0.56.0") +# +# Minimum 0.58.0: earlier releases used the Bazel built-in `CcInfo` +# symbol, which was removed from current Bazel. 0.58.0 was the first +# release to load `CcInfo` from `@rules_cc//cc/common:cc_info.bzl`. +# Pinning lower forced consumers (e.g. pulseengine/rivet) to mark Verus +# CI as continue-on-error since the load failed at module evaluation. +bazel_dep(name = "rules_rust", version = "0.58.0") # Crate dependencies for verus-strip crate = use_extension("@rules_rust//crate_universe:extensions.bzl", "crate") diff --git a/README.md b/README.md index 342d1d1..b00e9f6 100644 --- a/README.md +++ b/README.md @@ -306,7 +306,9 @@ sysroot (`librustc_driver`, `libstd`, etc.) alongside the Verus binaries. This m Verus was built against - **Full sandbox support** — all files are available as Bazel inputs - **`rules_rust` is only needed for `verus_strip`** (building from source via `crate_universe`), - and uses a low minimum version (`>= 0.56.0`) to avoid conflicts + and uses a low minimum version (`>= 0.58.0`) to avoid conflicts. + The 0.58.0 floor is required because earlier releases used the Bazel + built-in `CcInfo` symbol that current Bazel has removed. ## License diff --git a/tools/verus-strip/src/lib.rs b/tools/verus-strip/src/lib.rs index 850edad..bdcb7ac 100644 --- a/tools/verus-strip/src/lib.rs +++ b/tools/verus-strip/src/lib.rs @@ -23,11 +23,14 @@ pub struct StripResult { /// Strip Verus annotations from a Rust source file. pub fn strip_file(input: &str) -> StripResult { - let (preamble, body, _after) = split_at_verus_macro(input); + let (preamble, body, after) = split_at_verus_macro(input); let clean_preamble = strip_vstd_imports(&preamble); let stripped_body = strip_body(&body); + // Plain Rust trailing the verus!{} block (e.g. `#[cfg(test)] mod tests`) + // is passed through with vstd imports stripped, but otherwise as-is. + let clean_after = strip_vstd_imports(&strip_verus_close_marker(&after)); - // Reassemble: preamble (comments + use statements) + stripped body + // Reassemble: preamble (comments + use statements) + stripped body + after let mut raw = String::new(); let trimmed_pre = clean_preamble.trim_end(); if !trimmed_pre.is_empty() { @@ -42,6 +45,14 @@ pub fn strip_file(input: &str) -> StripResult { raw.push_str(trimmed_body); raw.push('\n'); } + let trimmed_after = clean_after.trim(); + if !trimmed_after.is_empty() { + if !raw.is_empty() { + raw.push('\n'); + } + raw.push_str(trimmed_after); + raw.push('\n'); + } // Parse and re-format with prettyplease for clean output match syn::parse_file(&raw) { @@ -85,13 +96,66 @@ pub fn strip_file(input: &str) -> StripResult { // ─── Phase 1: Find verus! macro ───────────────────────────────────────── +/// Find the byte position of the `verus!` macro identifier, skipping over +/// line comments, block comments, string literals, and identifier matches +/// (e.g. `myverus!` would not match — `verus!` must be a token boundary). +/// +/// This guards against a real bug: backtick-escaped tokens like +/// /// Use `verus!{}` to wrap your spec +/// would otherwise match the `find("verus!")` and corrupt the split. +fn find_verus_macro_pos(input: &str) -> Option { + let bytes = input.as_bytes(); + let mut pos = 0; + while pos < bytes.len() { + // Line comment — runs to end of line. Doc comments (//, ///, //!) all start with //. + if pos + 1 < bytes.len() && bytes[pos] == b'/' && bytes[pos + 1] == b'/' { + while pos < bytes.len() && bytes[pos] != b'\n' { + pos += 1; + } + continue; + } + // Block comment — handles /* ... */ but not nested. + if pos + 1 < bytes.len() && bytes[pos] == b'/' && bytes[pos + 1] == b'*' { + pos += 2; + while pos + 1 < bytes.len() && !(bytes[pos] == b'*' && bytes[pos + 1] == b'/') { + pos += 1; + } + pos = (pos + 2).min(bytes.len()); + continue; + } + // String literal — skip past closing quote, honoring backslash escapes. + if bytes[pos] == b'"' { + pos += 1; + while pos < bytes.len() && bytes[pos] != b'"' { + if bytes[pos] == b'\\' && pos + 1 < bytes.len() { + pos += 2; + continue; + } + pos += 1; + } + pos = (pos + 1).min(bytes.len()); + continue; + } + // Match `verus!` only if preceded by non-identifier char (token boundary). + if pos + 6 <= bytes.len() && &bytes[pos..pos + 6] == b"verus!" { + let prev_is_ident_char = pos > 0 + && (bytes[pos - 1].is_ascii_alphanumeric() || bytes[pos - 1] == b'_'); + if !prev_is_ident_char { + return Some(pos); + } + } + pos += 1; + } + None +} + /// Split input at the `verus! { ... }` macro boundary. /// Returns (text_before, body_inside_braces, text_after). fn split_at_verus_macro(input: &str) -> (String, String, String) { // Find "verus!" followed by a brace-delimited block. // We scan for the token sequence rather than parsing, since the // body contains non-standard Rust that confuses full parsers. - if let Some(macro_start) = input.find("verus!") { + if let Some(macro_start) = find_verus_macro_pos(input) { let after_bang = macro_start + "verus!".len(); // Find the opening { let rest = &input[after_bang..]; @@ -144,6 +208,31 @@ fn strip_vstd_imports(text: &str) -> String { .join("\n") } +/// Strip a leading `} // verus!` style closing-marker line from `after`. +/// The split positions us right after the closing `}` of the macro body; +/// the rest of that line typically holds an end-of-block marker comment +/// like `// verus!` which prettyplease then drops anyway. +fn strip_verus_close_marker(text: &str) -> String { + // The split puts `after` starting right after the `}`. Drop everything + // up to the next newline if it's just whitespace + a // comment. + let mut chars = text.char_indices(); + let mut newline_pos: Option = None; + for (idx, ch) in chars.by_ref() { + if ch == '\n' { + newline_pos = Some(idx); + break; + } + if ch != ' ' && ch != '\t' && ch != '/' { + // Line has real content — keep entire input as-is. + return text.to_string(); + } + } + match newline_pos { + Some(p) => text[p + 1..].to_string(), + None => String::new(), + } +} + // ─── Phase 2: Strip verus body using token trees ──────────────────────── /// Strip Verus annotations from the body of a `verus! { }` block. @@ -214,6 +303,14 @@ fn strip_body(body: &str) -> String { continue; } + // Check for Verus mode qualifier `exec` in `pub exec const`, + // `pub exec fn`, etc. The keyword is meaningless in plain Rust + // and would otherwise leak through and fail parsing. + if is_mode_qualifier_at(&trees, i) { + i += 1; // skip the `exec` ident + continue; + } + // Check for named return type: -> (name: Type) if is_arrow_at(&trees, i) { if let Some((replacement, skip_to)) = try_strip_named_return(&trees, i) { @@ -481,6 +578,25 @@ fn skip_doc_attrs(trees: &[TokenTree], pos: usize) -> usize { j } +/// Check if `trees[pos]` is a Verus mode qualifier (`exec`) used as an +/// item modifier — i.e. immediately followed by `const`/`fn`/`static`. +/// Does NOT match `spec` or `proof` because those mark items that get +/// stripped wholesale by try_skip_verus_item. +fn is_mode_qualifier_at(trees: &[TokenTree], pos: usize) -> bool { + let kw = match trees.get(pos) { + Some(TokenTree::Ident(id)) => id.to_string(), + _ => return false, + }; + if kw != "exec" { + return false; + } + let next = match trees.get(pos + 1) { + Some(TokenTree::Ident(id)) => id.to_string(), + _ => return false, + }; + matches!(next.as_str(), "const" | "fn" | "static") +} + fn is_verifier_attr_at(trees: &[TokenTree], pos: usize) -> bool { if let Some(TokenTree::Punct(p)) = trees.get(pos) { if p.as_char() == '#' { @@ -801,6 +917,91 @@ pub proof fn lemma_foo() assert!(result.output.contains("//! Module doc."), "missing doc"); } + // ─── Regression tests for three bugs hit in pulseengine/relay ────── + + /// Bug 1: `pub exec const FOO = ...` was passed through as-is, leaving + /// the `exec` keyword in plain output where it does not parse. + #[test] + fn test_strip_exec_const_qualifier() { + let input = r#" +use vstd::prelude::*; + +verus! { +#[verifier::external_body] +pub exec const TABLE: [u32; 4] = [1, 2, 3, 4]; +} // verus! +"#; + let result = strip_file(input); + assert!(result.errors.is_empty(), "parse errors: {:?}\noutput:\n{}", result.errors, result.output); + assert!(!result.output.contains("exec const"), "still contains `exec const`:\n{}", result.output); + assert!(result.output.contains("pub const TABLE"), "missing const decl:\n{}", result.output); + assert!(!result.output.contains("verifier"), "verifier attr leaked:\n{}", result.output); + } + + /// Bug 1 variant: `pub exec fn` should also have `exec` stripped. + #[test] + fn test_strip_exec_fn_qualifier() { + let input = r#" +use vstd::prelude::*; +verus! { +pub exec fn double(x: u32) -> u32 { x * 2 } +} // verus! +"#; + let result = strip_file(input); + assert!(result.errors.is_empty(), "parse errors: {:?}\noutput:\n{}", result.errors, result.output); + assert!(!result.output.contains("exec fn"), "still contains `exec fn`:\n{}", result.output); + assert!(result.output.contains("pub fn double"), "missing fn decl:\n{}", result.output); + } + + /// Bug 2: A backtick-escaped `verus!` token inside a `///` doc comment + /// matched the naive `find("verus!")` and corrupted the macro split. + /// Real-world example from relay/relay-primitives/src/crc32.rs. + #[test] + fn test_backtick_verus_in_doc_comment_does_not_split_early() { + let input = r#" +//! Module doc. + +/// Declared outside `verus!{}` so it's accepted by both Verus and stripped Rust. +pub const SIZE: usize = 6; + +use vstd::prelude::*; + +verus! { +pub fn real_fn() -> u32 { 42 } +} // verus! +"#; + let result = strip_file(input); + assert!(result.errors.is_empty(), "parse errors: {:?}\noutput:\n{}", result.errors, result.output); + assert!(result.output.contains("pub const SIZE"), "lost the pre-macro const:\n{}", result.output); + assert!(result.output.contains("real_fn"), "lost the in-macro fn:\n{}", result.output); + } + + /// Bug 3: Content after `verus!{}` (test modules, additional impls) was + /// silently dropped because `_after` was discarded in strip_file. + #[test] + fn test_preserves_content_after_verus_block() { + let input = r#" +use vstd::prelude::*; +verus! { +pub fn add(a: u32, b: u32) -> u32 { a + b } +} // verus! + +#[cfg(test)] +mod tests { + use super::*; + #[test] + fn one_plus_one() { + assert_eq!(add(1, 1), 2); + } +} +"#; + let result = strip_file(input); + assert!(result.errors.is_empty(), "parse errors: {:?}\noutput:\n{}", result.errors, result.output); + assert!(result.output.contains("fn add"), "lost the verus fn:\n{}", result.output); + assert!(result.output.contains("mod tests"), "lost the trailing test module:\n{}", result.output); + assert!(result.output.contains("one_plus_one"), "lost the test fn:\n{}", result.output); + } + #[test] fn test_proof_fn_with_block_ensures() { let body = r#" diff --git a/verus/private/repo.bzl b/verus/private/repo.bzl index 3d28f6f..092159d 100644 --- a/verus/private/repo.bzl +++ b/verus/private/repo.bzl @@ -182,19 +182,37 @@ def _verus_release_impl(rctx): ) # 2. Download rust-std component (libstd, libcore, liballoc, etc.) - rctx.download_and_extract( - url = "https://static.rust-lang.org/dist/rust-std-{v}-{t}.tar.xz".format( - v = rust_version, t = platform, - ), - output = "rust_std_tmp", - stripPrefix = "rust-std-{v}-{t}/rust-std-{t}".format( - v = rust_version, t = platform, - ), + # Use download + tar directly instead of download_and_extract + cp -R, + # because the Bazel stripPrefix + cp merge fails silently on some + # platforms (the rlib files don't end up in the sysroot). + rust_std_url = "https://static.rust-lang.org/dist/rust-std-{v}-{t}.tar.xz".format( + v = rust_version, t = platform, ) - - # Merge rust-std into sysroot (trailing slash copies contents, not directory) - rctx.execute(["cp", "-R", "rust_std_tmp/lib/rustlib/", "rust_sysroot/lib/rustlib/"]) - rctx.execute(["rm", "-rf", "rust_std_tmp"]) + rctx.download(url = rust_std_url, output = "rust_std.tar.xz") + + # Extract directly into sysroot, stripping the 2 top-level dirs: + # rust-std-{v}-{t}/rust-std-{t}/lib/... → lib/... + # This merges rust-std's lib/rustlib/{target}/lib/*.rlib alongside + # the rustc component's lib/librustc_driver-*.so already in rust_sysroot. + extract = rctx.execute([ + "tar", "-xf", "rust_std.tar.xz", + "-C", "rust_sysroot", + "--strip-components=2", + ]) + if extract.return_code != 0: + fail("Failed to extract rust-std into sysroot: " + extract.stderr) + + rctx.execute(["rm", "rust_std.tar.xz"]) + + # Verify the sysroot has libcore for this target + verify = rctx.execute(["sh", "-c", + "ls rust_sysroot/lib/rustlib/{t}/lib/libcore-*.rlib 2>/dev/null | head -1".format(t = platform), + ]) + if verify.return_code != 0 or not verify.stdout.strip(): + debug = rctx.execute(["find", "rust_sysroot/lib/rustlib", "-maxdepth", "3", "-type", "f"]) + fail("Sysroot missing libcore for {t}. Contents:\n{d}".format( + t = platform, d = debug.stdout[:500], + )) else: # No version known — create empty sysroot directory rctx.execute(["mkdir", "-p", "rust_sysroot/lib"]) diff --git a/verus/private/verus.bzl b/verus/private/verus.bzl index 9f01b2d..9c7d2ad 100644 --- a/verus/private/verus.bzl +++ b/verus/private/verus.bzl @@ -156,8 +156,9 @@ set -euo pipefail # rust_verify needs rustc's libraries and Verus libraries. # Derive sysroot from rust_verify location — both live in the same repo root. +# Resolve to absolute path to avoid issues with symlink-based runfiles. TOOLCHAIN_DIR=$(dirname "{rust_verify}") -SYSROOT="$TOOLCHAIN_DIR/rust_sysroot" +SYSROOT="$(cd "$TOOLCHAIN_DIR/rust_sysroot" 2>/dev/null && pwd)" || SYSROOT="$TOOLCHAIN_DIR/rust_sysroot" case "$(uname)" in Darwin) export DYLD_LIBRARY_PATH="$SYSROOT/lib:$TOOLCHAIN_DIR:${{DYLD_LIBRARY_PATH:-}}" ;; *) export LD_LIBRARY_PATH="$SYSROOT/lib:$TOOLCHAIN_DIR:${{LD_LIBRARY_PATH:-}}" ;; @@ -310,7 +311,10 @@ set -euo pipefail # This ensures the path is correct whether using f.path or f.short_path. RUST_VERIFY="{rust_verify}" TOOLCHAIN_DIR=$(dirname "$RUST_VERIFY") -SYSROOT="$TOOLCHAIN_DIR/rust_sysroot" + +# Resolve sysroot to absolute path to avoid issues with symlink-based runfiles +SYSROOT="$(cd "$TOOLCHAIN_DIR/rust_sysroot" 2>/dev/null && pwd)" || SYSROOT="$TOOLCHAIN_DIR/rust_sysroot" + case "$(uname)" in Darwin) export DYLD_LIBRARY_PATH="$SYSROOT/lib:$TOOLCHAIN_DIR:${{DYLD_LIBRARY_PATH:-}}" ;; *) export LD_LIBRARY_PATH="$SYSROOT/lib:$TOOLCHAIN_DIR:${{LD_LIBRARY_PATH:-}}" ;; @@ -326,6 +330,17 @@ echo "Crate: {crate_name}" echo "Source: $SRC" echo "Verifier: $RUST_VERIFY" echo "Rust sysroot: $SYSROOT" + +# Verify sysroot contains the target standard library +TARGET_LIB="$SYSROOT/lib/rustlib/x86_64-unknown-linux-gnu/lib" +if [ -d "$TARGET_LIB" ]; then + CORE_COUNT=$(ls "$TARGET_LIB"/libcore* 2>/dev/null | wc -l) + echo "Sysroot target libs: $CORE_COUNT core files in $TARGET_LIB" +else + echo "WARNING: target lib dir missing: $TARGET_LIB" + echo " Sysroot contents:" + find "$SYSROOT" -maxdepth 4 -type f -o -type l 2>/dev/null | head -20 || echo " (empty or missing)" +fi echo "" "$RUST_VERIFY" --edition=2021 --crate-type lib --sysroot "$SYSROOT" \\