feat(ci): add Miri UB verification to CI - #93
Merged
Conversation
Documents which code runs under Miri and why, the measured runtime that drove the exclusion list, and the known parallel+simd coverage gap. Also records four factual corrections to issue #81: structural.rs has no unsafe block, data_ptr/data_ptr_mut live in matrix.rs and contain no unsafe, excluding the simd feature would audit zero production unsafe, and --workspace contradicts the stated wasm exclusion. .agents/* is gitignored, so the plan is un-ignored by exception in the same style as instructions.md and workflows/. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Two matrix legs against `-p purecv --lib`: a required baseline on `std`, and an advisory leg on `std,simd` that reaches the unsafe slice reinterpretations in arithm.rs and derivatives.rs. Kept in its own workflow file because GitHub badges are per-workflow, not per-job, and to keep nightly flakiness out of the main CI badge. MIRIFLAGS uses -Zmiri-deterministic-floats, not the -Zmiri-strict-provenance the issue proposed: strict provenance is now Miri's default and that flag is deprecated, while Miri's float error injection breaks the Box-Muller determinism test in rng.rs. --lib skips doc-tests, where two ORB examples cost 767s under interpretation while duplicating unit-test coverage. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Nine tests exceed 30s under Miri interpretation and together account for 94% of the suite's runtime; the remaining 293 tests finish in 139s. The annotations take a full run from 41 minutes to roughly 4. Excluded for runtime only — none of the nine contains or reaches unsafe, and nothing in the suite proved Miri-incompatible. Each carries a reason comment so the exclusion list stays derivable by grep. test_build_pyramid_with_derivatives was the one borderline case: it exercises the Sobel unsafe fast path, but that coverage is retained by imgproc::tests::test_sobel, which hits the same f32/ksize-3 trigger in 0.8s under Miri. The attributes vanish under normal cargo test — all tests still run there. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The Portable SIMD bullet claimed "Zero unsafe, zero #[cfg(target_arch)]". The second half is true; the first is not — arithm.rs and derivatives.rs use from_raw_parts to feed pulp. Reworded to state that those reinterpretations are Miri-checked in CI, turning a claim Miri would contradict into one it actively backs. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
3 tasks
kalwalt
added
enhancement
The simd leg was introduced advisory in case Miri's target-dependent intrinsic support differed between the local Windows host and CI. It ran green on ubuntu-latest with counts identical to local — 355 passed, 0 failed, 9 ignored on both — so the hedge has served its purpose. Leaving it advisory would mean the only leg that reaches production unsafe could not actually block a bad merge. Plan document updated to match: leg 2 is now documented as required, and the header records the verification result and links to the follow-up issue for the parallel+simd coverage gap. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Section 8 was written before the spike and its commands no longer worked. Copy-pasting them hit three walls in sequence: --report-time is rejected without -Zunstable-options, the missing MIRIFLAGS made test_randn_determinism fail on a last-ULP float difference, and the missing --lib pulled in ~13 minutes of ORB doc-tests. Replaced with the exact commands CI runs, plus a table of what each omitted flag does so a failure is recognisable as configuration rather than a real regression. Also reframes the section as a record of what shipped rather than a pending checklist, and corrects commit 3's title to the one actually used. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Merged
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds a Miri job that checks PureCV's
unsafeslice reinterpretations for undefined behaviour on every push and PR, plus a plan document, a README badge, and a correction to a safety claim the code did not support.Result: no undefined behaviour found. Both legs run clean — 0 failures, 0 unsupported operations, 0 Stacked Borrows violations. All six production
unsafeblocks reachable withoutparallelare verified.std)std,simd)Why the approach differs from the issue
The plan in #81 would have verified nothing. Every production
unsafeblock issimd-gated, so the proposed no-features run touches none of them — the issue's "exclude pulp SIMD" and "verify all unsafe code" requirements are mutually exclusive as written. This uses two legs instead: a fast required baseline, and astd,simdleg that reaches the realunsafe.Four other corrections are documented in
.agents/MIRI_PLAN.md§7 — notablystructural.rshas nounsafeblock (line 278 is a comment explaining why it was avoided), anddata_ptr/data_ptr_mutlive inmatrix.rsand contain nounsafe.Decisions that needed measurement
#[cfg_attr(miri, ignore)]annotations bring it to ~4 minutes. Excluded for runtime only — none of the nine touchesunsafe, and nothing in the suite proved Miri-incompatible.--libskips them. There is notests/directory, so--libis the whole suite;cargo testinci.ymlstill runs doc-tests.-Zmiri-strict-provenance, which is now Miri's default and deprecated — passing it risks hard-failing on a future nightly. What is actually needed is-Zmiri-deterministic-floats: Miri injects random error into transcendental float ops, which breaks the Box-Muller determinism test inrng.rson a last-ULP difference. The flag keeps that test running rather than ignoring it.ci.yml" and "add a badge" requirements are incompatible. A separate file also keeps nightly flakiness out of the main CI badge.Notes for review
The simd leg is
continue-on-error: true. pulp turned out fully Miri-compatible, so this is stricter than necessary — but all local evidence is fromx86_64-pc-windows-msvcand CI runsubuntu-latest, where Miri's intrinsic support differs. Please flipexperimental: falseonce it is seen green on Linux; it is a one-word diff.Known coverage gap. The
parallel + simdchunkedfrom_raw_parts_mutinarithm.rsstays unverified — neither leg enablesparallel. The sequential equivalents share the same reinterpretation logic and are covered. Tracked in #94..gitignorechange..agents/*is ignored, so the plan document is un-ignored by exception, matching the existing pattern forinstructions.mdandworkflows/.The badge will 404 until this merges and the workflow runs on
dev.Fixes #81