diff --git a/.cargo/config.toml b/.cargo/config.toml index fba592bc3..e9e6b7002 100644 --- a/.cargo/config.toml +++ b/.cargo/config.toml @@ -1,10 +1,12 @@ # Enable the Polonius alpha borrow-checking analysis for every Cargo -# invocation, including rust-analyzer and `cargo kani`, so editors and -# verification tooling agree with CI about what borrows are legal. +# invocation, including rust-analyzer, so editors and verification tooling +# agree with CI about what borrows are legal. # # Note: an inherited `RUSTFLAGS` environment variable overrides this table. # Wrappers that set `RUSTFLAGS` (see the Makefile) must re-state -# `-Zpolonius=next` themselves. See +# `-Zpolonius=next` themselves. `cargo kani` sets `CARGO_ENCODED_RUSTFLAGS` +# itself, which also bypasses this table, so the `kani-full` recipe passes +# the flag via `RUSTFLAGS`. See # docs/adr-006-adopt-polonius-nightly-toolchain.md. [build] rustflags = ["-Zpolonius=next"] diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a9bd0057c..fbf9c5339 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -112,6 +112,7 @@ jobs: kani-smoke: if: github.event_name == 'pull_request' runs-on: ubuntu-latest + timeout-minutes: 20 permissions: contents: read env: @@ -140,3 +141,5 @@ jobs: run: make install-kani - name: Kani version check run: make kani-check + - name: Run Kani harnesses + run: make kani-ir diff --git a/Makefile b/Makefile index 2ee022cb4..c56203d07 100644 --- a/Makefile +++ b/Makefile @@ -80,10 +80,10 @@ clean: ## Remove build artefacts test: test-nextest doctest ## Run every Rust test with warnings treated as errors test-nextest: ## Run all non-doctest Rust tests through cargo-nextest - RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(CARGO) nextest run --all-targets --all-features $(NEXTEST_BUILD_JOBS) + RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(CARGO) nextest run --all-targets --all-features $(NEXTEST_BUILD_JOBS) doctest: ## Run doctests, which cargo-nextest cannot execute - RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(CARGO) test --doc --all-features $(BUILD_JOBS) + RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(CARGO) test --doc --all-features $(BUILD_JOBS) test-workflow-contracts: ## Validate the mutation-testing caller contract uv run --with 'pytest>=8' --with 'pyyaml>=6' pytest tests/workflow_contracts -q @@ -97,10 +97,10 @@ lint: lint-clippy lint-whitaker ## Run Clippy and the Whitaker Dylint suite with lint-clippy: ## Run rustdoc and Clippy with warnings denied RUSTDOCFLAGS="$(RUSTDOC_FLAGS)" RUSTFLAGS="$${RUSTFLAGS-} $(POLONIUS_FLAGS)" $(CARGO) doc --no-deps - RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(CARGO) clippy $(CLIPPY_FLAGS) + RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(CARGO) clippy $(CLIPPY_FLAGS) lint-whitaker: ## Run the Whitaker Dylint suite with warnings denied - RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(WHITAKER) --all -- --all-targets --all-features + RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(WHITAKER) --all -- --all-targets --all-features fmt: ## Format Rust and Markdown sources $(CARGO) fmt --all @@ -110,7 +110,7 @@ check-fmt: ## Verify formatting $(CARGO) fmt --all -- --check typecheck: ## Typecheck all targets and features - RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)" $(CARGO) check --all-targets --all-features $(BUILD_JOBS) + RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)" $(CARGO) check --all-targets --all-features $(BUILD_JOBS) markdownlint: spelling ## Lint Markdown and enforce en-GB-oxendict spelling $(MDLINT) "**/*.md" @@ -146,7 +146,7 @@ kani-check: ## Check the installed Kani verifier version @$(PROVER_TOOLS) kani check-version --kani-command "$(KANI)" $(KANI_CHECK_FLAGS) || { status=$$?; printf 'prover-tools: target=kani-check failed exit=%s\n' "$$status" >&2; exit "$$status"; } kani-full: ## Run the full Kani verification suite - $(KANI) $(KANI_FLAGS) + RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }$(POLONIUS_FLAGS)" $(KANI) $(KANI_FLAGS) kani-ir: kani-full ## Run the IR Kani verification suite diff --git a/docs/adr-006-adopt-polonius-nightly-toolchain.md b/docs/adr-006-adopt-polonius-nightly-toolchain.md index de1374fc0..1618dd215 100644 --- a/docs/adr-006-adopt-polonius-nightly-toolchain.md +++ b/docs/adr-006-adopt-polonius-nightly-toolchain.md @@ -1,4 +1,4 @@ -# Architecture Decision Record (ADR): Adopt the Polonius borrow checker on a pinned nightly toolchain +# Architecture decision record (ADR): Adopt the Polonius borrow checker on a pinned nightly toolchain ## Status @@ -39,9 +39,12 @@ Adopt Polonius now, as a nightly-only source tree: - Pin the dated toolchain `nightly-2026-06-25` in `rust-toolchain.toml` so builds stay reproducible. - Enable `-Zpolonius=next` in `.cargo/config.toml` under `[build] rustflags`, - so plain Cargo invocations, rust-analyzer, and `cargo kani` all borrow-check - with the same analysis. Makefile recipes that set `RUSTFLAGS` (which - overrides that table) re-state the flag via the `POLONIUS_FLAGS` variable. + so plain Cargo invocations and rust-analyzer borrow-check with the same + analysis. Makefile recipes that set `RUSTFLAGS` (which overrides that table) + re-state the flag via the `POLONIUS_FLAGS` variable. `cargo kani` sets + `CARGO_ENCODED_RUSTFLAGS` itself, which also bypasses the table, so the + `kani-full` recipe passes the flag through the `RUSTFLAGS` environment + variable, which Kani appends to its own flags. - Collapse the CI matrices in `ci.yml` and `netsukefile-test.yml` to the pinned nightly, and align `coverage-main.yml`. Stable and MSRV legs are removed because the tree no longer compiles without Polonius. diff --git a/docs/developers-guide.md b/docs/developers-guide.md index 057fd489f..f033aff83 100644 --- a/docs/developers-guide.md +++ b/docs/developers-guide.md @@ -82,10 +82,16 @@ Netsuke builds on the dated nightly toolchain pinned in `rust-toolchain.toml` with the Polonius alpha borrow-checking analysis (`-Zpolonius=next`) enabled. `rustup` provisions the toolchain automatically, and `.cargo/config.toml` supplies the flag by default, covering Cargo invocations such as rust-analyzer -and `cargo kani` that run without `RUSTFLAGS` in the environment. Makefile -recipes that set `RUSTFLAGS` re-state the flag through the `POLONIUS_FLAGS` -variable because an inherited `RUSTFLAGS` environment variable overrides -`.cargo/config.toml`. +that run without `RUSTFLAGS` in the environment. Makefile recipes that set +`RUSTFLAGS` re-state the flag through the `POLONIUS_FLAGS` variable because an +inherited `RUSTFLAGS` environment variable overrides `.cargo/config.toml`. The +recipes that add `-D warnings` and `$(POLONIUS_FLAGS)` build the value as +`RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)"`; the +`$${RUSTFLAGS:+$$RUSTFLAGS }` expansion prepends any `RUSTFLAGS` already set by +the caller (for example a CI wrapper), so those flags survive rather than being +silently discarded. `cargo kani` sets `CARGO_ENCODED_RUSTFLAGS` itself, which +also overrides the table, so `make kani-full` passes the flag through +`RUSTFLAGS` as well. [ADR-006](adr-006-adopt-polonius-nightly-toolchain.md) records the policy decision, and the [polonius migration notes](polonius.md) track every site @@ -845,10 +851,12 @@ for the design rationale and re-entry criteria. Pull requests run a dedicated `kani-smoke` CI job alongside the ordinary `build-test` job. The job installs `uv`, installs the pinned Kani version -through `make install-kani`, and runs only `make kani-check`; it does not run -`make kani-full`, `make verus`, coverage, CodeScene upload, or the normal build -matrix. Its cache is intentionally separate from ordinary Cargo build -artefacts: the job uses a Kani-specific cache key derived from +through `make install-kani`, runs `make kani-check` as a version-drift guard, +and then runs the bounded harness suite through `make kani-ir` under a +20-minute job timeout; it does not run `make verus`, coverage, CodeScene +upload, or the normal build matrix. Its cache is intentionally separate from +ordinary Cargo build artefacts: the job uses a Kani-specific cache key derived +from `tools/kani/VERSION` and the Makefile, then caches the job-local Kani Cargo home plus Kani support-file home. @@ -858,9 +866,11 @@ home plus Kani support-file home. - `make test-nextest` — `cargo nextest run --all-targets --all-features`, with - `RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)"` (the Makefile re-states the - Polonius flag because a set `RUSTFLAGS` overrides `.cargo/config.toml`). This - runs every unit, integration, `rstest`, and `rstest-bdd` test. + `RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)"` (the + Makefile re-states the Polonius flag because a set `RUSTFLAGS` overrides + `.cargo/config.toml`, and the `$${RUSTFLAGS:+$$RUSTFLAGS }` prefix preserves + any `RUSTFLAGS` inherited from the caller). This runs every unit, + integration, `rstest`, and `rstest-bdd` test. - `make doctest` — `cargo test --doc --all-features`, with the same `RUSTFLAGS`. nextest cannot execute doctests, so they need their own pass. Note that the previous `cargo test --all-targets` invocation never ran diff --git a/docs/execplans/4-1-2-kani-smoke-ci-job.md b/docs/execplans/4-1-2-kani-smoke-ci-job.md index d903256c7..62db234c9 100644 --- a/docs/execplans/4-1-2-kani-smoke-ci-job.md +++ b/docs/execplans/4-1-2-kani-smoke-ci-job.md @@ -569,3 +569,19 @@ The references section should include: - Lody session: ``` + +## Addendum: 2026-08-02 — bounded harness wiring completed + +The bounded Kani harness work deferred at the time of this ExecPlan's +execution has since been completed, in follow-up work tracked as +[issue #445](https://github.com/leynos/netsuke/issues/445). The pull-request +`kani-smoke` job now runs `make kani-check` (the pinned-version drift guard) +and then `make kani-ir` (the bounded harness suite), after +`make install-kani`. The `kani-smoke` job declares `timeout-minutes: 20`. The +bounded suite contains 13 `#[kani::proof]` harnesses: 4 in +`src/ir/from_manifest_verification.rs` and 9 in +`src/ir/cycle_verification.rs`. +[Pull request #470](https://github.com/leynos/netsuke/pull/470) carries the +implementation and declares `Closes #445`; the issue itself remains open at +the time of writing and closes on merge. This addendum records later work and +does not amend the plan as executed. diff --git a/docs/formal-verification-methods-in-netsuke.md b/docs/formal-verification-methods-in-netsuke.md index d6605ba05..41b0843fa 100644 --- a/docs/formal-verification-methods-in-netsuke.md +++ b/docs/formal-verification-methods-in-netsuke.md @@ -216,8 +216,10 @@ development and continuous integration. These pins serve several purposes: The first formal-verification commands should extend the existing `Makefile` without disturbing the current developer workflow.[^2] -- `make kani-check` should run the fast installed-version check suitable for - pull requests until substantive Kani harnesses exist. +- `make kani-check` should run the fast pinned-version drift guard suitable + for pull requests. +- The bounded Kani harness suite now also runs on pull requests through + `make kani-ir`. - `make kani-full` should run the full Kani suite. - `make install-kani` should install the pinned Kani version through `rust-prover-tools`. @@ -236,12 +238,16 @@ Formal verification should not be folded into the existing `build-test` job. The current `CI` workflow already performs formatting, linting, tests, and coverage, and those checks should remain intact.[^3] -The first additional job should be a dedicated `kani-smoke` job that: +The `kani-smoke` job is a dedicated, pull-request-only job (it runs only when +`github.event_name == 'pull_request'`) that: - installs `uv` and then installs the pinned Kani toolchain through `make install-kani`, -- runs `make kani-check`, and -- caches tool downloads separately from the ordinary Rust build artefacts. +- runs `make kani-check` and then the bounded harness suite through + `make kani-ir` (13 harnesses across the manifest-verification and + cycle-verification modules), +- caches tool downloads separately from the ordinary Rust build artefacts, and +- is bounded by a 20-minute job timeout (`timeout-minutes: 20`). Any later Verus job should be added only after a stable proof kernel exists. diff --git a/docs/roadmap.md b/docs/roadmap.md index b2b92e2bd..44e74354f 100644 --- a/docs/roadmap.md +++ b/docs/roadmap.md @@ -355,11 +355,10 @@ and test workflow intact. See Requires 4.1.1. See [formal-verification-methods-in-netsuke.md §Continuous integration (CI)](formal-verification-methods-in-netsuke.md#continuous-integration-ci). - [x] Keep the existing `build-test` job unchanged. - - [x] Run the bounded smoke path on pull requests. As scoped for this item, - the `kani-smoke` job in `.github/workflows/ci.yml` runs `make install-kani` - and `make kani-check` (a Kani version check); the harness set was empty when - this lane shipped. Wiring the bounded harnesses since landed by `4.2.*` into - the pull-request job is tracked separately as + - [x] Run the bounded smoke path on pull requests. The `kani-smoke` job in + `.github/workflows/ci.yml` runs `make install-kani`, `make kani-check` (a + Kani version check), and `make kani-ir` (the bounded harnesses landed by + `4.2.*`). The harness wiring resolved the follow-up previously tracked as [issue #445](https://github.com/leynos/netsuke/issues/445). - [x] Cache Kani tool downloads separately from ordinary Cargo artefacts. - [x] 4.1.3. Record the phase-1 scope boundary for Verus and Stateright. See diff --git a/src/ir/cycle.rs b/src/ir/cycle.rs index 23a828372..cc82ba72b 100644 --- a/src/ir/cycle.rs +++ b/src/ir/cycle.rs @@ -28,7 +28,9 @@ mod cycle_property_tests; mod support; #[cfg(any(test, kani))] use support::canonicalize_cycle_by; -use support::{canonicalize_cycle, path_cmp, path_eq, state_for_path, target_entry_for_path}; +#[cfg(not(kani))] +use support::path_cmp; +use support::{canonicalize_cycle, path_eq, state_for_path, target_entry_for_path}; #[cfg(test)] #[path = "cycle_tests.rs"] diff --git a/src/ir/cycle_verification.rs b/src/ir/cycle_verification.rs index b13d2ead1..14e3883d9 100644 --- a/src/ir/cycle_verification.rs +++ b/src/ir/cycle_verification.rs @@ -1,5 +1,6 @@ //! Kani harnesses for bounded IR cycle-handling properties. +use super::support::rotate_index; use super::*; /// Prove a self-dependency reports a cycle and no missing dependency. diff --git a/tests/makefile_test_target.rs b/tests/makefile_test_target.rs index 26551f62f..ce8029ec5 100644 --- a/tests/makefile_test_target.rs +++ b/tests/makefile_test_target.rs @@ -1,16 +1,34 @@ -//! Contract tests for the canonical `make test` entry point. +//! Contract tests for the canonical `make test` entry point and for every +//! Makefile recipe that overrides `RUSTFLAGS`. //! //! `make test` is the single command local development and continuous //! integration (CI) both run. These tests pin the runner contract it encodes: -//! non-doctest tests go through cargo-nextest, doctests run separately because -//! nextest cannot execute them, and both passes deny warnings and re-state -//! the Polonius flag that an inherited RUSTFLAGS would otherwise strip. They also assert -//! that the checked-in nextest configuration still declares the narrow -//! serialisation group the environment-mutating suites depend on. +//! non-doctest tests go through cargo-nextest, and doctests run separately +//! because nextest cannot execute them. +//! +//! They also pin the `RUSTFLAGS` contract shared by every recipe that sets the +//! variable. Setting `RUSTFLAGS` at all overrides the `[build] rustflags` +//! table in `.cargo/config.toml`, so each such recipe re-states the Polonius +//! flag, and each prepends any value the caller already exported rather than +//! discarding it. `test-nextest`, `doctest`, `lint-clippy`'s Clippy line, +//! `lint-whitaker`, and `typecheck` additionally add `-D warnings`; +//! `kani-full` adds only the Polonius flag, because Kani compiles third-party +//! crates the workspace lint policy does not govern. The binary-build recipe +//! and `lint-clippy`'s rustdoc line preserve the caller's value through a +//! different expansion and add neither `-D warnings` nor anything else. +//! +//! The `RUSTFLAGS` tests extract each assignment from the Makefile, resolve +//! the Make variables it names, and expand the result in a shell. They assert +//! on the flags that expansion yields rather than on recipe text, so they stay +//! valid when the command a recipe runs changes. A guard test fails if a +//! recipe starts setting `RUSTFLAGS` without joining the covered set. use anyhow::{Context, Result, ensure}; use camino::Utf8Path; use cap_std::{ambient_authority, fs_utf8::Dir}; +use rstest::rstest; +use std::collections::BTreeSet; +use std::process::Command; use toml::Value; /// Opens the repository root as a capability-scoped directory handle. @@ -125,7 +143,8 @@ fn behavioural_make_test_composes_the_nextest_and_doctest_passes() -> Result<()> "test-nextest should enable all features, found {nextest_recipe:?}" ); ensure!( - nextest_recipe.contains(r#"RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)""#), + nextest_recipe + .contains(r#"RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)""#), "test-nextest should deny warnings and enable Polonius, found {nextest_recipe:?}" ); @@ -140,12 +159,343 @@ fn behavioural_make_test_composes_the_nextest_and_doctest_passes() -> Result<()> "doctests cannot run under nextest, found {doctest_recipe:?}" ); ensure!( - doctest_recipe.contains(r#"RUSTFLAGS="-D warnings $(POLONIUS_FLAGS)""#), + doctest_recipe + .contains(r#"RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings $(POLONIUS_FLAGS)""#), "doctest should deny warnings and enable Polonius, found {doctest_recipe:?}" ); Ok(()) } +/// The prefix introducing a quoted `RUSTFLAGS` assignment in a recipe. +const RUSTFLAGS_PREFIX: &str = "RUSTFLAGS=\""; + +/// A value a caller might already have exported before invoking `make`. +const CALLER_RUSTFLAGS: &str = "-C target-cpu=native"; + +const DENY_WARNINGS: &str = "-D warnings"; + +/// A recipe line that overrides `RUSTFLAGS`, and the contract it must meet. +#[derive(Clone, Copy, Debug)] +struct RustflagsCase { + /// The Make target owning the recipe. + target: &'static str, + /// Substring selecting the recipe line. `lint-clippy` sets `RUSTFLAGS` on + /// two lines — one for rustdoc, one for Clippy — with different contracts. + line_marker: &'static str, + /// Whether the recipe adds `-D warnings`. + denies_warnings: bool, + /// Whether the recipe must contribute its separator only alongside an + /// inherited value, so an unset `RUSTFLAGS` leaves no leading space. + /// + /// This is the contract the case asserts, deliberately not read back from + /// the Makefile: inferring it from the assignment would let a rewrite to a + /// bare `$RUSTFLAGS ` prefix delete the assertion along with the idiom. + separator_only_when_set: bool, +} + +impl RustflagsCase { + const fn test_nextest() -> Self { + Self { + target: "test-nextest", + line_marker: "nextest run", + denies_warnings: true, + separator_only_when_set: true, + } + } + + const fn doctest() -> Self { + Self { + target: "doctest", + line_marker: "--doc", + denies_warnings: true, + separator_only_when_set: true, + } + } + + const fn binary_build() -> Self { + Self { + target: "target/%/$(APP)", + line_marker: "build", + denies_warnings: false, + separator_only_when_set: false, + } + } + + const fn lint_clippy_rustdoc() -> Self { + Self { + target: "lint-clippy", + line_marker: "doc --no-deps", + denies_warnings: false, + separator_only_when_set: false, + } + } + + const fn lint_clippy() -> Self { + Self { + target: "lint-clippy", + line_marker: "clippy", + denies_warnings: true, + separator_only_when_set: true, + } + } + + const fn lint_whitaker() -> Self { + Self { + target: "lint-whitaker", + line_marker: "$(WHITAKER)", + denies_warnings: true, + separator_only_when_set: true, + } + } + + const fn typecheck() -> Self { + Self { + target: "typecheck", + line_marker: "check", + denies_warnings: true, + separator_only_when_set: true, + } + } + + const fn kani_full() -> Self { + Self { + target: "kani-full", + line_marker: "$(KANI)", + denies_warnings: false, + separator_only_when_set: true, + } + } +} + +/// Every `RUSTFLAGS`-setting recipe line under contract. +const RUSTFLAGS_CASES: [RustflagsCase; 8] = [ + RustflagsCase::test_nextest(), + RustflagsCase::doctest(), + RustflagsCase::binary_build(), + RustflagsCase::lint_clippy_rustdoc(), + RustflagsCase::lint_clippy(), + RustflagsCase::lint_whitaker(), + RustflagsCase::typecheck(), + RustflagsCase::kani_full(), +]; + +/// Returns the value of a simple `NAME ?= value` or `NAME = value` variable. +fn make_variable(contents: &str, name: &str) -> Option { + contents.lines().find_map(|line| { + let rest = line.strip_prefix(name)?; + let value = rest + .strip_prefix(" ?= ") + .or_else(|| rest.strip_prefix(" = "))?; + Some(value.trim().to_owned()) + }) +} + +/// Extracts the double-quoted `RUSTFLAGS` assignment from a recipe line. +/// +/// `RUSTDOCFLAGS="…"` does not contain `RUSTFLAGS="`, so a line setting both +/// still yields the `RUSTFLAGS` value. +fn rustflags_assignment(line: &str) -> Option<&str> { + let start = line.find(RUSTFLAGS_PREFIX)? + RUSTFLAGS_PREFIX.len(); + let rest = line.get(start..)?; + let end = rest.find('"')?; + rest.get(..end) +} + +/// Returns the recipe line `case` selects. +fn recipe_line(makefile: &str, case: RustflagsCase) -> Result { + let recipe = target_recipe(makefile, case.target) + .with_context(|| format!("Makefile should declare a {} target", case.target))?; + recipe + .lines() + .find(|line| line.contains(RUSTFLAGS_PREFIX) && line.contains(case.line_marker)) + .map(str::trim) + .map(ToOwned::to_owned) + .with_context(|| { + format!( + "{} should set RUSTFLAGS on a line matching {:?}", + case.target, case.line_marker + ) + }) +} + +/// Returns `case`'s `RUSTFLAGS` assignment as a shell expression. +/// +/// Make variable references are resolved, and Make's `$$` escape is reduced to +/// the single `$` the shell receives. +fn shell_expression(makefile: &str, case: RustflagsCase) -> Result { + let line = recipe_line(makefile, case)?; + let assignment = rustflags_assignment(&line).with_context(|| { + format!( + "{} should assign a double-quoted RUSTFLAGS value", + case.target + ) + })?; + let polonius = make_variable(makefile, "POLONIUS_FLAGS") + .context("Makefile should define POLONIUS_FLAGS")?; + let resolved = assignment.replace("$(POLONIUS_FLAGS)", &polonius); + ensure!( + !resolved.contains("$("), + "{}: RUSTFLAGS assignment {resolved:?} names a Make variable this test cannot resolve", + case.target + ); + Ok(resolved.replace("$$", "$")) +} + +/// Expands `expression` in a shell, exporting `inherited` as `RUSTFLAGS`. +/// +/// Only the assignment is expanded; the command the recipe would run is never +/// executed, so no test here invokes Cargo, Kani, nextest, or Dylint. +#[cfg(unix)] +fn expand(expression: &str, inherited: Option<&str>) -> Result { + ensure!( + !expression.contains('"') && !expression.contains('`'), + "the expansion helper cannot safely embed {expression:?}" + ); + let mut command = Command::new("sh"); + command + .arg("-c") + .arg(format!("printf '%s' \"{expression}\"")) + .env_remove("RUSTFLAGS"); + if let Some(value) = inherited { + command.env("RUSTFLAGS", value); + } + + let output = command + .output() + .with_context(|| format!("expand {expression:?} with sh"))?; + ensure!( + output.status.success(), + "sh should expand {expression:?}: {}", + String::from_utf8_lossy(&output.stderr) + ); + String::from_utf8(output.stdout).context("expanded RUSTFLAGS should be UTF-8") +} + +#[test] +fn unit_extracts_the_rustflags_assignment_from_a_recipe_line() { + assert_eq!( + rustflags_assignment(r#" RUSTFLAGS="$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings" $(CARGO) x"#), + Some(r"$${RUSTFLAGS:+$$RUSTFLAGS }-D warnings") + ); + // A line setting RUSTDOCFLAGS first still yields the RUSTFLAGS value. + assert_eq!( + rustflags_assignment(r#" RUSTDOCFLAGS="-D warnings" RUSTFLAGS="$${RUSTFLAGS-} -Z" x"#), + Some(r"$${RUSTFLAGS-} -Z") + ); + assert_eq!(rustflags_assignment("\tcargo build"), None); +} + +#[cfg(unix)] +#[rstest] +#[case(RustflagsCase::test_nextest())] +#[case(RustflagsCase::doctest())] +#[case(RustflagsCase::binary_build())] +#[case(RustflagsCase::lint_clippy_rustdoc())] +#[case(RustflagsCase::lint_clippy())] +#[case(RustflagsCase::lint_whitaker())] +#[case(RustflagsCase::typecheck())] +#[case(RustflagsCase::kani_full())] +fn behavioural_rustflags_recipes_preserve_inherited_flags( + #[case] case: RustflagsCase, +) -> Result<()> { + let makefile = read_repo_file(Utf8Path::new("Makefile"))?; + let polonius = make_variable(&makefile, "POLONIUS_FLAGS") + .context("Makefile should define POLONIUS_FLAGS")?; + let expanded = expand(&shell_expression(&makefile, case)?, Some(CALLER_RUSTFLAGS))?; + + ensure!( + expanded.contains(CALLER_RUSTFLAGS), + "{} should preserve the caller's RUSTFLAGS, expanded to {expanded:?}", + case.target + ); + ensure!( + expanded.contains(&polonius), + "{} should re-state {polonius} because setting RUSTFLAGS overrides \ + .cargo/config.toml, expanded to {expanded:?}", + case.target + ); + ensure!( + expanded.contains(DENY_WARNINGS) == case.denies_warnings, + "{} should {}deny warnings, expanded to {expanded:?}", + case.target, + if case.denies_warnings { "" } else { "not " } + ); + Ok(()) +} + +#[cfg(unix)] +#[rstest] +#[case(RustflagsCase::test_nextest())] +#[case(RustflagsCase::doctest())] +#[case(RustflagsCase::binary_build())] +#[case(RustflagsCase::lint_clippy_rustdoc())] +#[case(RustflagsCase::lint_clippy())] +#[case(RustflagsCase::lint_whitaker())] +#[case(RustflagsCase::typecheck())] +#[case(RustflagsCase::kani_full())] +fn behavioural_rustflags_recipes_are_well_formed_without_inherited_flags( + #[case] case: RustflagsCase, +) -> Result<()> { + let makefile = read_repo_file(Utf8Path::new("Makefile"))?; + let polonius = make_variable(&makefile, "POLONIUS_FLAGS") + .context("Makefile should define POLONIUS_FLAGS")?; + let expression = shell_expression(&makefile, case)?; + let expanded = expand(&expression, None)?; + + ensure!( + expanded.contains(&polonius), + "{} should re-state {polonius} even with no inherited RUSTFLAGS, \ + expanded to {expanded:?}", + case.target + ); + ensure!( + !expanded.contains(CALLER_RUSTFLAGS), + "{} should not invent flags the caller never set, expanded to {expanded:?}", + case.target + ); + // `${VAR:+VAR }` contributes its separator only alongside a value, so an + // unset RUSTFLAGS must not leave a leading space. Recipes spelling the + // expansion `${VAR-}` tolerate one, so the case declares which contract + // applies. This is what separates the idiom from a bare `$RUSTFLAGS ` + // prefix, which preserves the caller's flags but strands a separator. + if case.separator_only_when_set { + ensure!( + !expanded.starts_with(' '), + "{} should not emit a leading separator when RUSTFLAGS is unset, \ + expanded to {expanded:?}", + case.target + ); + } + Ok(()) +} + +#[test] +fn behavioural_every_rustflags_recipe_line_is_under_contract() -> Result<()> { + let makefile = read_repo_file(Utf8Path::new("Makefile"))?; + let declared: BTreeSet = makefile + .lines() + .filter(|line| line.starts_with('\t') && line.contains(RUSTFLAGS_PREFIX)) + .map(|line| line.trim().to_owned()) + .collect(); + let covered: BTreeSet = RUSTFLAGS_CASES + .iter() + .map(|case| recipe_line(&makefile, *case)) + .collect::>()?; + + let uncovered: Vec<&String> = declared.difference(&covered).collect(); + ensure!( + uncovered.is_empty(), + "every recipe setting RUSTFLAGS needs a RustflagsCase; uncovered: {uncovered:#?}" + ); + ensure!( + covered.len() == RUSTFLAGS_CASES.len(), + "each RustflagsCase should select a distinct recipe line, {} cases selected {} lines", + RUSTFLAGS_CASES.len(), + covered.len() + ); + Ok(()) +} + /// Returns the `[[profile.default.overrides]]` entries. fn profile_overrides(config: &Value) -> Option<&[Value]> { config diff --git a/tests/workflow_ci.rs b/tests/workflow_ci.rs index 0425d9ee0..a73e07170 100644 --- a/tests/workflow_ci.rs +++ b/tests/workflow_ci.rs @@ -254,17 +254,25 @@ fn behavioural_ci_workflow_wires_kani_smoke_job() -> Result<()> { "Kani smoke job should cache tools using the Kani version and Makefile" ); + let install_kani_index = steps + .iter() + .position(|step| step_has(step, StepField::Runs, "make install-kani")) + .context("Kani smoke job should install Kani through the Make target")?; + let kani_check_index = steps + .iter() + .position(|step| step_has(step, StepField::Runs, "make kani-check")) + .context("Kani smoke job should check Kani through the Make target")?; + let kani_ir_index = steps + .iter() + .position(|step| step_has(step, StepField::Runs, "make kani-ir")) + .context("Kani smoke job should run the bounded Kani harnesses through the Make target")?; ensure!( - steps - .iter() - .any(|step| step_has(step, StepField::Runs, "make install-kani")), - "Kani smoke job should install Kani through the Make target" + install_kani_index < kani_check_index && kani_check_index < kani_ir_index, + "Kani smoke job should install Kani, check its version, then run the bounded harnesses" ); ensure!( - steps - .iter() - .any(|step| step_has(step, StepField::Runs, "make kani-check")), - "Kani smoke job should check Kani through the Make target" + mapping_get(kani_job, YamlKey("timeout-minutes")).and_then(Value::as_u64) == Some(20), + "Kani smoke job should enforce the 20-minute cold-run ceiling" ); Ok(()) }