test(vcr-ra): reg_effect ↔ rewrite_op def/use consistency oracle (#242)#513
Merged
Conversation
The register allocator reads each op's def/use classification two ways that MUST agree: `reg_effect` (liveness — which registers an op defines vs uses) and `rewrite_op` (renaming — which fields it rewrites through the def-map vs the use-map). If they drift — an op edited in one but not the other, or a new op modeled inconsistently — the allocator renames a def as a use and silently miscompiles. liveness.rs is the actively-churned heart of VCR-RA and nothing pinned this invariant. This is the Track-A (allocator) analogue of the #511 Track-B (encoder) agreement oracle. There is no third ground truth here, so the achievable invariant is mutual CONSISTENCY, checked structurally without a register extractor: build the def/use maps FROM `reg_effect`'s classification (def regs → a def sentinel, use regs → a use sentinel, read-modify-write regs → one shared sentinel so `rewrite_op` doesn't decline), apply `rewrite_op`, then read the result back with `reg_effect`. If the two agree on every field, every register is rerouted to a sentinel; a SURVIVING original register means `rewrite_op` routed a field through the opposite map — the drift. What the oracle pins, for all 55 modeled ops: - the def/use ROLE of every field (survivor check), and - the read-modify-write PROPERTY of dual-role fields (Movt/MovtSym/SelectMove `rd`): a register `reg_effect` reports in both defs and uses must make `rewrite_op` DECLINE when the two maps disagree on it — otherwise the shared sentinel would mask a drift that turned the RMW field def-only or use-only. - `is_modeled`: a no-wildcard match over all 220 `ArmOp` variants — a new variant won't compile until classified (the tripwire; it already caught `B` and `Nop` being mis-bucketed during authoring). The modeled (true) side is exhaustive (careful 55-variant extraction, all constructed + checked); the unmodeled (false) side is spot-sampled. Scope: a regression GUARD, not a bug fix — the classification AGREES for every modeled op today (measured exhaustively). Test-only; no production code changes. Negative tests confirmed non-vacuous on BOTH branches: misrouting one op's `rd` (def→use) trips the survivor check; dropping `Movt`'s RMW decline trips the RMW check. 464 synth-synthesis lib tests green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
Jun 26, 2026
…ff) (#242) (#514) The optimized (non-`--relocatable`) ARM path re-materializes a constant at every use — the same `i32.const N` becomes a fresh movw/movt (or mov) each time. On the silicon hot path this is the dominant redundancy class (61% of flat_flight's const materializations target a value already in a register). Add a pressure-neutral const cache in `ir_to_arm` (optimizer_bridge.rs): when the wanted value already lives in a still-valid register, alias the new vreg to that register and emit NO materialization. Aliasing never adds register pressure — the value is already resident, so it can only SHARE a register, never demand one. The cache (`reg_holds_const`, keyed by u32 bit-pattern so a negative i32 matches its movw/movt reconstruction) is rebuilt from the EMITTED ARM at the top of each lowering step — so it survives the many `continue` arms — and RESET at every control-flow boundary (an unmodeled `reg_effect` op), confining reuse to straight-line segments. Byte-CHANGING codegen, so it ships DEFAULT-OFF (`SYNTH_CONST_CSE`): - OFF ⇒ byte-identical. Gated by const_cse_reduction_242.rs's golden, a pinned FNV-1a of the flag-off optimized-path `.text` for const_cse.wat, captured against the pre-change tree (stash-compare verified equal). The frozen differential fixtures compile `--relocatable` (direct path), so this golden is the ONLY gate pinning optimized-path-OFF bytes. - ON ⇒ semantics-preserving. New CI oracle const_cse_differential.py executes the flag-on build under unicorn and diffs the returned value vs wasmtime across large/small/negative/mixed consts, reuse across an if/else (cache must reset), and a 12-live-local function that forces real spills. - ON ⇒ real reduction on headroom: large3 (a >16-bit const reused 3×) is strictly smaller (movw+movt pairs collapse to aliases); inert under register pressure (never a regression). NOT a default-on flip — that is a separate, silicon-gated step. Two prerequisites are NAMED in the code and test, not assumed handled: - reg_effect DEF-COMPLETENESS (broader than the #513 consistency oracle, which only pins that reg_effect and rewrite_op AGREE — they could agree and both under-report a def, leaving a stale alias). - ALIAS-EVICTION: aliasing makes two live vregs share one register, breaking the spill model's vreg↔reg bijection. Not reachable today (the IR optimizer dedups consecutive identical consts upstream), but the flip must prove unreachability or make the spill path alias-aware. VCR-RA / epic #242. Behavior frozen on every shipped path. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
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.
What
A CI-gated oracle pinning a previously-unguarded register-allocator correctness invariant:
reg_effect(liveness — which registers an op defines vs uses) andrewrite_op(renaming — which fields it rewrites through the def-map vs the use-map) must classify every field of every op identically. If they drift, the allocator renames a def as a use → silent miscompile.liveness.rsis the actively-churned heart of VCR-RA and nothing pinned this.This is the Track-A (allocator) analogue of #511's Track-B (encoder) agreement oracle.
How
There's no third ground truth here, so the achievable invariant is mutual consistency, checked structurally without a register extractor:
reg_effect's classification (def regs → a def sentinel, use regs → a use sentinel, RMW regs → one shared sentinel sorewrite_opdoesn't decline).rewrite_op.reg_effect. If the two agree on every field, every register is rerouted to a sentinel — a surviving original register meansrewrite_oprouted a field through the opposite map (the drift).What it pins, for all 55 modeled ops:
Movt/MovtSym/SelectMoverd): a registerreg_effectcalls both def and use must makerewrite_opdecline when the two maps disagree — otherwise the shared sentinel would mask a drift that turned the RMW field def-only.is_modeledis a no-wildcard match over all 220ArmOpvariants — a new variant won't compile until classified (the tripwire; it caughtBandNopmis-bucketed during authoring). The modeled side is exhaustive (careful 55-variant extraction, all constructed + checked); the unmodeled side is spot-sampled.Verification
rd(def→use) trips the survivor check; droppingMovt's RMW decline trips the RMW check.Scope
A regression guard, not a bug fix — the classification agrees for every modeled op today (measured exhaustively). Test-only; no production code changes. Refs #242.
🤖 Generated with Claude Code