diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c61c6844..616a8480 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -955,6 +955,78 @@ jobs: - name: Run RV32 data-segment full-boot oracle (#798, rv32imac) run: SYNTH=./target/debug/synth python scripts/repro/rv32_data_798_boot_differential.py + instrument-independence-oracle: + name: VCR-VER-004 instrument independence (#242, v0.53's mutation re-run) + # THE LESSON THIS JOB PINS. v0.53 proved BY MUTATION that emptying + # `cfg_exit_observable` — the exit contract the join-aware graph allocator + # and its own CFG validator SHARE — emits code leaving the return value in + # the WRONG REGISTER, and that BOTH per-compilation validators accept it + # (`validate_cfg_rewrite` -> Ok, VCR-RA-003 -> Consistent). Only execution + # caught it: two independent-LOOKING instruments, one shared blind spot, + # and a counterexample to the claim that per-compilation validation is an + # independent check on the code generator. + # + # This job re-applies that EXACT mutation (the committed patch, not a + # reconstruction) and asserts on ONE compilation that the two dataflow + # validators are still GREEN while VCR-VER-004 `validate_abi_contract` + # REJECTS with a concrete violation naming the ABI result register — i.e. + # that the class is now caught STATICALLY, and by an instrument that fails + # DIFFERENTLY (forward value analysis, obligation = the AAPCS result + # registers hard-named in its own source, CFG re-derived from both streams, + # nothing taken from the pass). + # + # It asserts the BASELINE direction FIRST — the unmutated compiler must + # still apply AND must not be rejected — so a false-rejection regression + # (the v0.50 `JoinValueNotAvailable{R8}` class) fails this job before it + # ever reaches the mutation. Isolated job: the script mutates the working + # tree and rebuilds, then always restores it. + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + - name: Cache Cargo dependencies + uses: actions/cache@v6 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + target/ + key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} + restore-keys: | + ${{ runner.os }}-cargo- + - uses: actions/setup-python@v7 + with: + python-version: "3.x" + - name: Build synth + run: cargo build -p synth-cli + # THE DEFAULT PATH, not the spike. The gate above guards the flag-OFF + # graph-colouring allocator; this step asks the same ABI question of the + # allocator every `synth compile` actually runs, and holds the answer to a + # floor: ZERO violations (a violation is either a real shipping miscompile + # or — far likelier, since the shipping bytes are frozen-pinned and + # execution-differentialed — a FALSE REJECTION by the new instrument, and + # neither may pass silently), plus a pinned `Holds` count so a change that + # makes the checker SEE LESS of the shipping path is visible instead of + # absorbed. Red-first in both directions (injected violation; stub binary + # emitting no verdicts) — see the script docstring. + - name: Audit the SHIPPING allocator against the ABI contract (#242) + run: | + set -o pipefail + SYNTH=./target/debug/synth python scripts/repro/vcr_ver_004_shipping_path_audit.py | tee vcr_ver_004_ship.out + grep -q "^VCR-VER-004-SHIPPING .* VIOLATED=0 " vcr_ver_004_ship.out + test "$(grep -c '^ Holds ' vcr_ver_004_ship.out)" -eq 1 + # The grep asserts the machine-readable 4/4 AND a non-zero OK count (#890): + # exit 0 alone is not trusted, and a run that silently skipped every + # assertion would otherwise pass while gating nothing. + - name: Re-run the v0.53 mutation against all three instruments (#242) + run: | + set -o pipefail + python scripts/repro/vcr_ver_004_instrument_independence.py | tee vcr_ver_004.out + grep -q "^VCR-VER-004-INDEPENDENCE ASSERTIONS=4/4$" vcr_ver_004.out + test "$(grep -c '^OK ' vcr_ver_004.out)" -eq 5 + - name: Assert the tree was restored (the mutation must never persist) + run: git diff --exit-code + fact-spec-oracle: name: fact-spec elision oracle (#494 phases 2 + 2b + 3+ + bounds) # VCR-PERF-002 Phase 2 (#494): the proof-carrying-specialization lever diff --git a/CHANGELOG.md b/CHANGELOG.md index 68f5cdd3..63f9e503 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -141,6 +141,124 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 divergent call-containing functions) which the CI wiring re-asserts from the `CALLSHAPES=` summary field (#890). 56/56 checks, 19 engaged functions of which 6 are call shapes. +- **VCR-VER-004 — the ABI observable-contract validator: a per-compilation check + that fails *differently*** (#242). + + v0.53 measured something uncomfortable. Emptying `cfg_exit_observable` — the + exit contract the join-aware graph allocator and its own CFG validator *share* + — makes the compiler emit code that leaves the return value **in the wrong + register**, and **both** per-compilation validators accept it: + `validate_cfg_rewrite` returns `Ok` and VCR-RA-003 `validate_final_allocation` + returns `Consistent`. Only execution caught it. Two independent-*looking* + instruments, one shared blind spot — #872's lesson one level up, and a direct + counterexample to the claim that per-compilation validation is an independent + check on the code generator. + + The response is not a third file on the same axis. **Independence is not + obtained by writing a second checker, only by checking a different WAY**, and + `abi_contract::validate_abi_contract` differs on four axes that matter: + + - **Its obligation cannot be emptied.** The exit obligation is + `RETURN_CONTRACT_REGS = [R0, R1]`, a constant of the AAPCS hard-named in the + module's own source. Deleting `cfg_exit_observable` outright would not change + one line of it. + - **It is forward, and a forward value analysis is structurally incapable of + the fail-open mode that bit v0.53.** `validate_cfg_rewrite` is a backward + MUST-analysis whose obligation set is a *variable* — and the empty set is a + fixpoint, so an empty seed means zero obligations means vacuous green. A + forward evaluation always produces *exactly one* value for `R0` at each + return. There is no seed to shrink. + - **Its evidence is a value, not a name-pair.** Per side independently it + builds a value graph (`Init(r)` / `Def(i,k)` / `Phi(b,n)`) and compares by + **greatest-fixpoint bisimulation**; on a deterministic term graph that is + equality of the infinite unfoldings, so loops and back edges are handled + coinductively rather than by unrolling. `Init(r)` is one node *shared* by + both sides — the AAPCS **parameter** half of the anchor, so reading an + argument out of the wrong register is a value change too. + - **It takes nothing from the pass.** The signature is `(orig, rewritten)`; the + CFG is re-derived from both streams' label-form branch structure and the two + must agree. The v0.50 join attempt failed precisely by letting the pass hand + the checker its own seed. + + **Result, by re-running v0.53's exact mutation** (committed as + `scripts/repro/mutations/v053_shared_exit_contract.patch`, not reconstructed): + the two dataflow validators stay green on the same compilation while + VCR-VER-004 rejects with `Violated { sink: 81, reg: R0 }` on + `brif_outer_740::poll` — the function that returned `0x1111` instead of its + parameter — and the miscompile is **not emitted**. CI-wired as + `instrument-independence-oracle`, which asserts the *baseline* direction first + (the unmutated compiler must still apply and must not be rejected) so a + false-rejection regression fails before the mutation is even reached. The + script is proven red-first: make `abi_gate` treat `Violated` as an accept and + the mutated compiler goes back to emitting the miscompile. + + **The gate costs nothing.** Over the ARM repro corpus, composed with + VCR-DEC-001 increment 3 (#896): 617 functions, **307 applied**, + `40822 → 40722` bytes (−100 B relocatable, −120 B self-contained) — increment + 3's result *to the byte*, with the check conservative enough to demand both + `R0` and `R1` for every function and to decline whenever it cannot analyze. + `NotAttempted` is a **decline**, not an accept: if a decline counted as + acceptance, a change that made the check universally inapplicable would disable + it silently. + + **Calls are modelled, not exempted.** Increment 3 taught the allocator to + colour *across calls*, taking 57 of 68 `call` declines — every one of which + this gate would have declined again. The fix was to model the AAPCS call + effect, reusing `liveness::call_effect` (the *one* definition the pass and + `validate_cfg_rewrite` already share, because two divergent call models would + be a fresh instance of the very blind-spot class this module attacks) rather + than to weaken `abi_gate`. The forward design needed no special case: each + clobbered register `{R0-R3, R12, LR}` is rebound to a **fresh** node whose + operands are the *pre-call* argument values, while `R4-R11`/`SP` flow through. + So a call result is an opaque value equal across the sides exactly when the + same callee got the same arguments, and a value the rewrite parked in + caller-saved scratch *across* a call is rebound to the call's own node — it can + no longer bisimulate with what the original delivers at the return. Increment + 3's own warning ("a validator treating `bl` as effect-free would accept a + non-identity equation across it") is discharged here as a **value** + disagreement, with no liveness reasoning anywhere. The `Call`/`CallIndirect` + *pseudo*-ops still decline: they expand downstream into a guard + table load + + `blx`, so this stream's register footprint is not the final code's. + + **And it was measured against the shipping allocator, not just the spike.** + `SYNTH_ABI_CONTRACT_AUDIT=1` reports the same verdict for + `reallocate_function_post_exhaust`, the allocator every `synth compile` runs: + **`Holds` 422 · `NotAttempted` 195 · `Violated` 0** over 617 functions — the + observable return contract *proven* on ~68 % of the shipping path with zero + false rejections against a known-good allocator, declines named + (`unmodeled-op` 174, `indirect-call-pseudo-op` 11, `numeric-offset-branch` 10). + Modelling calls moved this from `Holds 376 / NotAttempted 241`: the 62 + direct-call declines are **gone**, not reclassified, while `unmodeled-op` rose + 159 → 174 because functions that used to stop at the call now get further and + reach an FP / i64-pair op instead. The decline *moved*; it did not vanish. + Held to a CI floor by `vcr_ver_004_shipping_path_audit.py` (zero violations, a + pinned `Holds` count so lost coverage is visible rather than absorbed), itself + red-first in both directions including the vacuity case where the hook is not + wired at all. + + Honest residuals, in the module docs and the FEATURE_MATRIX honest summary + rather than implied away: **memory is not in the obligation** (a store-only + misrename is a false negative here — the class `validate_cfg_rewrite` *does* + cover when its seed is intact; the two instruments are complementary, not + redundant); **the op model is still shared** via `liveness::reg_effect`, so a + mismodeled op remains a blind spot common to all three, and until + `synth-verify`'s independent `ArmSemantics` is pinned against it, "three + independent validators" would be an overclaim; and on the **default path this + is an audit, not a gate** — hard-erroring a user's compile on a checker whose + false-positive rate is measured rather than proven is a flip that wants its own + evidence. + + There is deliberately **no SMT solver** here, and deliberately no opt-out env + var. A renames-only rewrite changes no opcode and no immediate, so the two + sides' terms are ground applications of the *same* uninterpreted operators; + deciding their equality is congruence closure with no side conditions — exactly + the structural equality the partition refinement already computes. A solver + would cost a dependency (and the `synth-verify` → `synth-synthesis` edge runs + the wrong way) to decide the same thing. An opt-out would be a footgun, not + evidence. + + Frozen anchors 10/10; the graph allocator is flag-off and the shipping-path + hook is report-only, so no emitted byte moves. ## [0.53.0] - 2026-07-30 diff --git a/crates/synth-backend/src/arm_backend.rs b/crates/synth-backend/src/arm_backend.rs index e57da2a4..c31592c3 100644 --- a/crates/synth-backend/src/arm_backend.rs +++ b/crates/synth-backend/src/arm_backend.rs @@ -1019,6 +1019,22 @@ fn compile_wasm_to_arm( stats.needs_spill ); } + // VCR-VER-004 AUDIT (#242) — report-only, opt-in, never gating. + // + // The ABI observable-contract validator is a GATE on the flag-off + // graph-colouring spike. This hook asks the same question of the + // SHIPPING allocator's rewrite, so the answer is a MEASUREMENT rather + // than a claim: how much of the shipping path can a value-level, + // ABI-anchored check actually see today? Report-only DELIBERATELY — + // making it gate here would risk a false rejection on the default + // path, and the honest sequence is measure first, flip on evidence. + // `SYNTH_ABI_CONTRACT_AUDIT=1` prints one verdict per function. + if std::env::var_os("SYNTH_ABI_CONTRACT_AUDIT").is_some() { + eprintln!( + "[abi-contract-audit] {:?}", + synth_synthesis::abi_contract::validate_abi_contract(&arm_instrs, &out) + ); + } // VCR-RA-002 (#390, epic #242): eliminate a provably-dead stack frame // (`sub sp,#N`/`add sp,#N` reserved by `compute_local_layout` for locals // that promotion homed in registers, never accessed). Removing it saves diff --git a/crates/synth-synthesis/src/abi_contract.rs b/crates/synth-synthesis/src/abi_contract.rs new file mode 100644 index 00000000..4ef91df2 --- /dev/null +++ b/crates/synth-synthesis/src/abi_contract.rs @@ -0,0 +1,1128 @@ +//! **VCR-VER-004 — the ABI observable-contract validator.** +//! +//! # Why this module exists +//! +//! v0.53's VCR-DEC-001 lane proved BY MUTATION that emptying +//! [`crate::liveness::cfg_exit_observable`] — the exit contract the join-aware +//! graph allocator and its own CFG validator SHARE — makes the compiler emit +//! code that leaves the function's return value **in the wrong register**, and +//! that BOTH per-compilation validators accept it: +//! +//! * [`crate::liveness::validate_cfg_rewrite`] (the pass's acceptance oracle) +//! returns `Ok`, and +//! * [`crate::liveness::validate_final_allocation`] (VCR-RA-003, the +//! whole-function allocation validator) returns `Consistent`. +//! +//! Only *execution* caught it. Two independent-*looking* instruments, one +//! shared blind spot — the #872 shape ("a validator that shares its pass's +//! dataflow is necessary, not sufficient") one level up, and a direct +//! counterexample to the claim that per-compilation validation is an +//! independent check on the code generator. +//! +//! # The thesis +//! +//! **Independence is not obtained by writing a second checker, only by checking +//! a different WAY.** Both existing instruments reason about *liveness/dataflow +//! equations over register names*, backward, seeded from a table. Agreeing costs +//! them almost nothing, so their agreement carries little information. +//! +//! This validator is deliberately built on a different axis in four respects. +//! +//! 1. **Its obligation cannot be emptied.** The exit obligation is the AAPCS +//! return register set ([`RETURN_CONTRACT_REGS`]) — a constant of the ABI, +//! hard-named HERE. It is not read from `cfg_exit_observable`, not supplied +//! by the caller, and not derived from "what either side writes". Deleting +//! `cfg_exit_observable` outright would not change one line of this check. +//! +//! 2. **It is FORWARD, and a forward value analysis is structurally incapable of +//! the fail-open mode that bit v0.53.** `validate_cfg_rewrite` is a backward +//! MUST-analysis: its obligation set is a *variable*, and the empty set is a +//! fixpoint — an empty seed means zero obligations means vacuous `Ok`. A +//! forward symbolic evaluation always produces *exactly one* value for `R0` +//! at each return, so there is always exactly one obligation per sink. There +//! is no seed to shrink. +//! +//! 3. **Its evidence is a VALUE, not a name-pair.** The two existing checks can +//! only see a wrong-register return as a *disagreement between register +//! names* — and only if something told them to look at that name. This one +//! computes what `R0` actually *holds*: a symbolic term rooted at the +//! ABI-anchored entry symbols and the producing instruction indices, then +//! asks whether the two streams' terms are the same value. +//! +//! 4. **It takes nothing from the pass.** The signature is `(orig, rewritten)`. +//! The CFG is re-derived HERE from the label-form branch structure of BOTH +//! streams and the two must agree — the pass never hands this checker an +//! artifact of its own (the v0.50 join-enforcement attempt failed exactly +//! there, and v0.53's own doc comment names it as the anti-pattern). +//! +//! # The check +//! +//! For a **renames-only** rewrite (same length, same ops modulo register +//! operands, identical control flow — all re-verified here) build, **per side +//! independently**, a value graph whose nodes are: +//! +//! ```text +//! Init(r) the entry value of register r — SHARED between the sides +//! Def(i, k) the k-th result of instruction i (operands: the use-values) +//! Phi(b, n) block b's entry value of a register (operands: preds' values) +//! ``` +//! +//! `Init(r)` being one shared node per register *is* the AAPCS **parameter** +//! contract: arguments arrive in `R0`–`R3` on both sides, so a rewrite that +//! reads a parameter out of the wrong register produces a different term. +//! +//! ## Calls (VCR-DEC-001 increment 3, #896) +//! +//! A `bl`/`blx` is **not** effect-free, and treating it as one would be exactly +//! the fail-open mode this module exists to eliminate. It gets the ONE shared +//! AAPCS definition, [`crate::liveness::call_effect`] — the same +//! `defs = {R0..R3, R12, LR}` / `uses = {R0..R3}` (+ the `blx` target) that the +//! pass and `validate_cfg_rewrite` consume — deliberately reused rather than +//! restated, because two divergent call models would be a fresh instance of the +//! shared-blind-spot class this module attacks. +//! +//! In the forward walk that falls out naturally: each clobbered register is +//! rebound to a **fresh** `Def(call_i, k)` node whose operands are the *pre-call* +//! argument values, and `R4`–`R11`/`SP` flow through untouched. So +//! +//! * a call result is an opaque value, equal across the two sides exactly when +//! the same callee was handed the same arguments — a rewrite that renames what +//! feeds an argument is caught; +//! * a value the rewrite parked in caller-saved scratch *across* the call is +//! rebound to the call's own node, so it can no longer bisimulate with the +//! value the original delivers at the return — the "recoloured across a call" +//! miscompile is caught as a **value** disagreement, without any liveness +//! reasoning. +//! +//! The `Call`/`CallIndirect` **pseudo**-ops still decline: they expand downstream +//! into a guard + table load + `blx`, so this stream's register footprint is not +//! the final code's. +//! +//! Values are compared by **greatest-fixpoint bisimulation** (partition +//! refinement over the two graphs at once). On a deterministic term graph +//! bisimilarity is exactly equality of the infinite unfoldings, so loops and +//! back edges are handled coinductively rather than by unrolling. The obligation +//! is then, at **every** return sink: +//! +//! ```text +//! value_rewritten(R0) ≡ value_orig(R0) and value_rewritten(R1) ≡ value_orig(R1) +//! ``` +//! +//! # Why there is no SMT solver here +//! +//! The natural home for a value-level VC in this repo is `synth-verify`'s +//! ordeal QF_BV pipeline (the trap-preservation VC's shape). It is deliberately +//! *not* used, for two reasons that are worth stating rather than hiding: +//! +//! * **A solver would add no discrimination.** A renames-only rewrite changes no +//! opcode and no immediate, so the two sides' terms are ground applications of +//! the *same* uninterpreted operators. Deciding equality of such terms is +//! congruence closure with no side conditions — i.e. exactly structural +//! equality, which is what the refinement computes. The solver would cost a +//! dependency and a per-function query to decide the same thing. +//! * **The dependency runs the wrong way.** `synth-verify` depends on +//! `synth-synthesis`, not the reverse, so an in-allocator SMT gate would need +//! the edge inverted or the check hoisted out of the pass it guards. +//! +//! The residual is recorded honestly in the module's limitations below. +//! +//! # Known limitations (named, not hidden) +//! +//! * **Memory is not in the obligation.** The contract checked is the *register* +//! half of the ABI. A mis-renamed store address that a later load reads back is +//! a false NEGATIVE here (the load's value node is keyed on its instruction +//! index and address operands, not on a memory chain). That class IS covered by +//! `validate_cfg_rewrite`'s use-equations when its seed is intact — the two +//! instruments are complementary, which is what independence is supposed to +//! look like. Extending the obligation to a store chain is a named follow-up. +//! * **The op model is still shared.** Def/use extraction goes through +//! [`crate::liveness::reg_effect`], so a *mismodeled op* remains a blind spot +//! common to all three instruments. This validator closes the shared-*contract* +//! hole, not the shared-*op-model* hole. `synth-verify`'s +//! `ArmSemantics::encode_op` is a genuinely second model of the same ops, and +//! pinning the two against each other is the obvious next rung. +//! * **Scope is the label-form shape.** `BrTable`, numeric-offset branches, +//! computed `Bx`, the `Call`/`CallIndirect` pseudo-ops, +//! duplicate/unresolvable labels and any op `reg_effect` does not model produce +//! a loud [`AbiContractVerdict::NotAttempted`] naming the construct. There is +//! no silent pass on a shape this cannot analyze. +//! * **A call's MEMORY effect is not modeled** — a consequence of the memory +//! limitation above, restated because a call is where it is easiest to forget: +//! the callee may write memory, and a later load is keyed on its instruction +//! index and address operands rather than on a store chain. Sound for a +//! renames-only rewrite (both sides execute the same callee at the same point); +//! not a claim about the callee's effects. + +use crate::instruction_selector::ArmInstruction; +use crate::liveness::{call_effect, is_straight_line, reg_effect}; +use crate::rules::{ArmOp, Reg}; +use std::collections::BTreeMap; + +/// The AAPCS registers that carry a wasm function's result, and therefore the +/// registers whose VALUE this validator requires a rewrite to preserve at every +/// return: `R0` (an `i32`/`f32`-in-core result) and `R1` (the high half of an +/// `i64`/`f64`-in-core result — the selector's "result in (R0,R1)" convention). +/// +/// **This constant is the whole point of the module.** It is the obligation +/// source, and it is a fact about the *ABI*, not about the rewrite, not about +/// the pass, and not about any table the pass also reads. Compare +/// [`crate::liveness::cfg_exit_observable`], which the v0.53 mutation emptied: +/// emptying that changed what `validate_cfg_rewrite` demanded; nothing can empty +/// this without editing this line, and editing this line is visible in review as +/// "we stopped checking the return value". +/// +/// It is deliberately the CONSERVATIVE over-approximation: both result registers +/// are required for every function, because this validator is not told the +/// function's wasm result arity. Requiring `R1` of an `i32`-returning function +/// can only cost a DECLINE (the caller falls back to the shipping allocator), it +/// can never cost soundness — and on the unmutated compiler it costs nothing at +/// all, because the intact exit contract already pins both. +pub const RETURN_CONTRACT_REGS: [Reg; 2] = [Reg::R0, Reg::R1]; + +/// The verdict of [`validate_abi_contract`]. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum AbiContractVerdict { + /// Every return sink delivers the same symbolic value in every ABI result + /// register on both sides. + Holds, + /// At the return terminator with instruction index `sink`, ABI result + /// register `reg` holds a DIFFERENT symbolic value after the rewrite. + Violated { sink: usize, reg: Reg }, + /// Loud honest decline: a construct the value graph cannot model. NEVER a + /// silent pass. + NotAttempted { reason: &'static str }, +} + +impl AbiContractVerdict { + /// True only for [`AbiContractVerdict::Violated`] — a decline is not a + /// failure, and callers that gate on this must not treat it as one. + pub fn is_violation(&self) -> bool { + matches!(self, AbiContractVerdict::Violated { .. }) + } +} + +/// Number of modeled core registers (`R0`–`R12`, `SP`, `LR`, `PC`). +const NREG: usize = 16; + +fn reg_ix(r: Reg) -> usize { + match r { + Reg::R0 => 0, + Reg::R1 => 1, + Reg::R2 => 2, + Reg::R3 => 3, + Reg::R4 => 4, + Reg::R5 => 5, + Reg::R6 => 6, + Reg::R7 => 7, + Reg::R8 => 8, + Reg::R9 => 9, + Reg::R10 => 10, + Reg::R11 => 11, + Reg::R12 => 12, + Reg::SP => 13, + Reg::LR => 14, + Reg::PC => 15, + } +} + +/// A basic block of the INDEPENDENTLY re-derived label-form CFG. +#[derive(Debug, Clone, PartialEq, Eq)] +struct Blk { + start: usize, + end: usize, + succ: Vec, +} + +fn is_return_term(op: &ArmOp) -> bool { + match op { + ArmOp::Bx { rm } => *rm == Reg::LR, + ArmOp::Pop { regs } => regs.contains(&Reg::PC), + _ => false, + } +} + +/// How an instruction participates in the CFG. +/// +/// **Every** instruction is classified, wherever it sits — not just block +/// enders. An op that merely *fails* to be a recognized branch would otherwise +/// fall through the forward walk with no register effect, which is precisely the +/// fail-open mode this module exists to eliminate: a `bl` in the middle of a +/// block destroys `R0`–`R3`/`R12` and defines `R0`, and silently modeling it as +/// a no-op would let the checker certify a rewrite it cannot see through. +enum Cf<'a> { + /// Straight-line: [`reg_effect`] must model it. + Straight, + /// A direct or indirect CALL (`bl` / `blx`). Falls through like a + /// straight-line op, but its register effect is the AAPCS + /// [`call_effect`] rather than [`reg_effect`]. + CallOp, + /// A `Label` — starts a block, no effect. + Label, + /// Unconditional branch to a label. + Uncond(&'a str), + /// Conditional branch to a label (fallthrough is the other successor). + Cond(&'a str), + /// `bx lr` — a return sink with no register effect. + Return, + /// Outside the analyzable label-form leaf shape: loud decline. + Reject(&'static str), +} + +fn classify(op: &ArmOp) -> Cf<'_> { + use ArmOp::*; + match op { + Label { .. } => Cf::Label, + B { label } => Cf::Uncond(label.as_str()), + Bhs { label } | Blo { label } | Bcc { label, .. } => Cf::Cond(label.as_str()), + BOffset { .. } | BCondOffset { .. } => Cf::Reject("numeric-offset-branch"), + BrTable { .. } => Cf::Reject("br-table"), + Bx { rm } if *rm == Reg::LR => Cf::Return, + Bx { .. } => Cf::Reject("computed-branch"), + // VCR-DEC-001 increment 3 (#896): a `bl`/`blx` is MODELED, using the ONE + // shared AAPCS definition. Keyed on `call_effect` returning `Some` + // rather than on a variant list, so this classifier and the pass's + // notion of "a call this allocator may colour across" cannot drift + // apart — two divergent call models would be a fresh instance of the + // shared-blind-spot class this module exists to attack. The `Call` / + // `CallIndirect` PSEUDO-ops get `None` (they expand downstream into a + // guard + table load + `blx`, so this stream's register footprint is not + // the final code's) and fall through to the loud declines below. + op if call_effect(op).is_some() => Cf::CallOp, + Bl { .. } | Call { .. } => Cf::Reject("call-pseudo-op"), + Blx { .. } | CallIndirect { .. } => Cf::Reject("indirect-call-pseudo-op"), + // Anything left must be straight-line; `is_straight_line` is the shared + // predicate and this arm asserts the two classifications agree, so a new + // control-flow variant added to `ArmOp` without a case here cannot slip + // through as "straight-line with no effect". + other if is_straight_line(other) => Cf::Straight, + _ => Cf::Reject("unclassified-control-flow"), + } +} + +/// An instruction's register effect: `(defs, uses)`, in the order +/// [`reg_effect`] / [`call_effect`] report them. `None` = carries no register +/// effect at all (pure control flow). +type Effect = Option<(Vec, Vec)>; + +/// The register effect of instruction `op`, or `None` if it carries none +/// (pure control flow: `Label` / `B` / `Bcc` / `bx lr`). +/// +/// `Err` means "this checker cannot model it" — a loud decline, never a silent +/// no-effect walk-past. +fn effect_of(op: &ArmOp) -> Result { + match classify(op) { + Cf::Reject(why) => Err(why), + Cf::Straight => reg_effect(op) + .map(|e| Some((e.defs, e.uses))) + .ok_or("unmodeled-op"), + Cf::CallOp => call_effect(op) + .map(|e| Some((e.defs, e.uses))) + .ok_or("unmodeled-call"), + Cf::Label | Cf::Uncond(_) | Cf::Cond(_) | Cf::Return => Ok(None), + } +} + +/// Re-derive the label-form CFG from an instruction stream. +/// +/// Built HERE rather than accepted from the caller: a validator that consumes +/// the pass's own CFG can be made vacuous by a wrong CFG (a missing edge hides a +/// path). Blocks start at index 0, at every `Label`, and immediately after every +/// branch or return. Successors come from the block's last instruction. Any +/// construct outside the label-form leaf shape is a loud decline. +fn derive_cfg(instrs: &[ArmInstruction]) -> Result, &'static str> { + use ArmOp::*; + if instrs.is_empty() { + return Err("empty-stream"); + } + + // Label name -> instruction index. Duplicates make targets ambiguous. + let mut labels: BTreeMap<&str, usize> = BTreeMap::new(); + for (i, ins) in instrs.iter().enumerate() { + if let Label { name } = &ins.op + && labels.insert(name.as_str(), i).is_some() + { + return Err("duplicate-label"); + } + } + + // Leaders. EVERY instruction is classified here, so an op outside the + // analyzable shape is rejected wherever it sits — not only when it happens + // to end a block. + let mut is_leader = vec![false; instrs.len()]; + is_leader[0] = true; + for (i, ins) in instrs.iter().enumerate() { + let ends_block = match classify(&ins.op) { + Cf::Reject(why) => return Err(why), + Cf::Label => { + is_leader[i] = true; + false + } + Cf::Uncond(_) | Cf::Cond(_) | Cf::Return => true, + // A call FALLS THROUGH: it does not end a basic block. + Cf::Straight | Cf::CallOp => is_return_term(&ins.op), + }; + if ends_block && i + 1 < instrs.len() { + is_leader[i + 1] = true; + } + } + let starts: Vec = (0..instrs.len()).filter(|&i| is_leader[i]).collect(); + let block_of: BTreeMap = + starts.iter().enumerate().map(|(b, &s)| (s, b)).collect(); + + let mut blocks: Vec = Vec::with_capacity(starts.len()); + for (b, &s) in starts.iter().enumerate() { + let e = starts.get(b + 1).copied().unwrap_or(instrs.len()); + blocks.push(Blk { + start: s, + end: e, + succ: Vec::new(), + }); + } + + for b in 0..blocks.len() { + let last = &instrs[blocks[b].end - 1].op; + let fallthrough = block_of.get(&blocks[b].end).copied(); + let target = |name: &str| block_of.get(labels.get(name)?).copied(); + let succ: Vec = match classify(last) { + Cf::Reject(why) => return Err(why), + Cf::Uncond(l) => vec![target(l).ok_or("unresolved-label")?], + Cf::Cond(l) => vec![ + target(l).ok_or("unresolved-label")?, + fallthrough.ok_or("cond-branch-falls-off-end")?, + ], + Cf::Return => Vec::new(), + Cf::Label | Cf::Straight | Cf::CallOp => { + if is_return_term(last) { + Vec::new() + } else { + vec![fallthrough.ok_or("falls-off-end")?] + } + } + }; + blocks[b].succ = succ; + } + Ok(blocks) +} + +/// A value-graph node tag. Deliberately keyed on the SHARED SKELETON (the +/// instruction index / block index), never on the side, so the two streams' +/// corresponding nodes start out assumed-equal and are split only by evidence. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] +enum Tag { + /// Entry value of register `r` — ONE node shared by both sides (the AAPCS + /// parameter anchor). + Init(u8), + /// The `k`-th result of instruction `i`. + Def(u32, u8), + /// Block `b`'s entry value of some register; `n` = operand count. + Phi(u32, u8), +} + +struct Graph { + tag: Vec, + ops: Vec>, +} + +impl Graph { + fn push(&mut self, tag: Tag, ops: Vec) -> usize { + self.tag.push(tag); + self.ops.push(ops); + self.tag.len() - 1 + } +} + +/// Prove that a renames-only rewrite preserves the ABI observable contract. +/// +/// Takes ONLY the two instruction streams — no CFG, no live-out set, no seed +/// from the caller. See the module documentation for the independence argument. +pub fn validate_abi_contract( + orig: &[ArmInstruction], + rewritten: &[ArmInstruction], +) -> AbiContractVerdict { + use AbiContractVerdict::*; + + if orig.len() != rewritten.len() { + return NotAttempted { + reason: "length-mismatch", + }; + } + if orig.is_empty() { + return NotAttempted { + reason: "empty-stream", + }; + } + + // ---- The CFG, re-derived from BOTH streams; they must agree ---------- + let blocks = match derive_cfg(orig) { + Ok(b) => b, + Err(reason) => return NotAttempted { reason }, + }; + match derive_cfg(rewritten) { + Ok(b) if b == blocks => {} + Ok(_) => { + return NotAttempted { + reason: "control-flow-rewritten", + }; + } + Err(reason) => return NotAttempted { reason }, + } + + // ---- Renames-only precondition, re-checked here ---------------------- + // Control flow AND calls must be literally identical (a register allocator + // renames operands; it never rewrites control flow, and — the increment-3 + // rule `validate_cfg_rewrite` also enforces — never rewrites a call's + // architectural operands, `blx`'s target register included). Every + // straight-line pair must be the same operation with matching def/use arity. + let mut eff: Vec = Vec::with_capacity(orig.len()); + let mut eff_r: Vec = Vec::with_capacity(orig.len()); + for (o, r) in orig.iter().zip(rewritten) { + if !is_straight_line(&o.op) || !is_straight_line(&r.op) { + if o.op != r.op { + return NotAttempted { + reason: "control-flow-rewritten", + }; + } + // Identical ops, so the SAME effect twice — and for a `bl`/`blx` + // that effect is the AAPCS clobber, not nothing. + let e = match effect_of(&o.op) { + Ok(e) => e, + Err(reason) => return NotAttempted { reason }, + }; + eff.push(e.clone()); + eff_r.push(e); + continue; + } + let (Some(eo), Some(er)) = (reg_effect(&o.op), reg_effect(&r.op)) else { + return NotAttempted { + reason: "unmodeled-op", + }; + }; + if eo.defs.len() != er.defs.len() || eo.uses.len() != er.uses.len() { + return NotAttempted { + reason: "shape-mismatch", + }; + } + eff.push(Some((eo.defs, eo.uses))); + eff_r.push(Some((er.defs, er.uses))); + } + + // ---- Predecessors ----------------------------------------------------- + let nb = blocks.len(); + let mut preds: Vec> = vec![Vec::new(); nb]; + for (b, blk) in blocks.iter().enumerate() { + for &s in &blk.succ { + if s >= nb { + return NotAttempted { + reason: "bad-cfg-edge", + }; + } + preds[s].push(b); + } + } + + // ---- Build the value graph ------------------------------------------- + let mut g = Graph { + tag: Vec::new(), + ops: Vec::new(), + }; + // Entry symbols: ONE node per register, SHARED by both sides. + let init: Vec = (0..NREG) + .map(|r| g.push(Tag::Init(r as u8), Vec::new())) + .collect(); + + // Phi placeholders, per side / block / register. + // side 0 = orig, side 1 = rewritten. + let mut phi = [ + vec![[0usize; NREG]; nb], // orig + vec![[0usize; NREG]; nb], // rewritten + ]; + for b in 0..nb { + let n_ops = preds[b].len() + usize::from(b == 0); + if n_ops > u8::MAX as usize { + return NotAttempted { + reason: "phi-arity", + }; + } + for item in phi.iter_mut() { + for slot in item[b].iter_mut() { + *slot = g.push(Tag::Phi(b as u32, n_ops as u8), Vec::new()); + } + } + } + + // Forward walk, per side, per block. + let mut out = [vec![[0usize; NREG]; nb], vec![[0usize; NREG]; nb]]; + for side in 0..2 { + let effects = if side == 0 { &eff } else { &eff_r }; + for (b, blk) in blocks.iter().enumerate() { + let mut env = phi[side][b]; + // The effect vector is total: `None` means "carries no register + // effect" and is reached ONLY for pure control flow + // (`Label`/`B`/`Bcc`/`bx lr`), because `effect_of` turned every + // other unmodeled shape into a decline above. A `bl`/`blx` is + // `Some(call_effect)`, so it is NEVER walked past as a no-op — its + // clobbered registers get FRESH nodes below and its callee-saved + // registers flow through untouched. + for (i, e) in effects.iter().enumerate().take(blk.end).skip(blk.start) { + let Some((defs, uses)) = e else { + continue; + }; + let operands: Vec = uses.iter().map(|u| env[reg_ix(*u)]).collect(); + for (k, d) in defs.iter().enumerate() { + if k > u8::MAX as usize { + return NotAttempted { + reason: "def-arity", + }; + } + let n = g.push(Tag::Def(i as u32, k as u8), operands.clone()); + env[reg_ix(*d)] = n; + } + } + out[side][b] = env; + } + } + + // Wire the phi operands now that every block's exit state is known. + for b in 0..nb { + for side in 0..2 { + for r in 0..NREG { + let mut o: Vec = Vec::with_capacity(preds[b].len() + 1); + if b == 0 { + o.push(init[r]); + } + for &p in &preds[b] { + o.push(out[side][p][r]); + } + let id = phi[side][b][r]; + g.ops[id] = o; + } + } + } + + // ---- Greatest-fixpoint bisimulation (partition refinement) ----------- + // + // Start from the coarsest partition consistent with the tags (so the two + // sides' corresponding nodes are assumed EQUAL) and split whenever two + // nodes' operand classes differ. Refinement only ever splits, the class + // count is bounded by the node count, so this terminates; the limit is the + // coarsest stable partition, i.e. the greatest bisimulation. On a + // deterministic term graph that is exactly equality of the infinite + // unfoldings — which is why back edges need no unrolling. + let n = g.tag.len(); + let mut class: Vec = { + let mut ids: BTreeMap = BTreeMap::new(); + g.tag + .iter() + .map(|t| { + let next = ids.len(); + *ids.entry(*t).or_insert(next) + }) + .collect() + }; + let mut n_classes = class.iter().copied().max().map_or(0, |m| m + 1); + for _ in 0..=n { + let mut sigs: BTreeMap<(usize, Vec), usize> = BTreeMap::new(); + let mut next_class = vec![0usize; n]; + for (i, next_item) in next_class.iter_mut().enumerate() { + let key = ( + class[i], + g.ops[i].iter().map(|&o| class[o]).collect::>(), + ); + let next = sigs.len(); + *next_item = *sigs.entry(key).or_insert(next); + } + class = next_class; + if sigs.len() == n_classes { + break; + } + n_classes = sigs.len(); + } + + // ---- The obligation: the AAPCS result registers, at every return ----- + let mut sinks = 0usize; + for (b, blk) in blocks.iter().enumerate() { + if !blk.succ.is_empty() { + continue; + } + let term = &orig[blk.end - 1].op; + if !is_return_term(term) { + return NotAttempted { + reason: "unrecognized-return", + }; + } + // A return terminator that itself WRITES a result register would make + // the comparison read a value this model does not track (a `pop` loads + // from the stack, which is outside the register value graph) — that + // would be a silent vacuous pass, so decline instead. + if let ArmOp::Pop { regs } = term + && regs.iter().any(|r| RETURN_CONTRACT_REGS.contains(r)) + { + return NotAttempted { + reason: "return-restores-result-register", + }; + } + sinks += 1; + for reg in RETURN_CONTRACT_REGS { + let lo = out[0][b][reg_ix(reg)]; + let hi = out[1][b][reg_ix(reg)]; + if class[lo] != class[hi] { + return Violated { + sink: blk.end - 1, + reg, + }; + } + } + } + if sinks == 0 { + // No reachable return at all: nothing to certify. A vacuous `Holds` + // here would be exactly the failure this module exists to prevent. + return NotAttempted { + reason: "no-return-sink", + }; + } + + Holds +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::rules::{Condition, MemAddr, Operand2, VfpReg}; + + fn ins(op: ArmOp) -> ArmInstruction { + ArmInstruction { + op, + source_line: None, + } + } + + fn mov(rd: Reg, rm: Reg) -> ArmInstruction { + ins(ArmOp::Mov { + rd, + op2: Operand2::Reg(rm), + }) + } + + fn movw(rd: Reg, imm16: u16) -> ArmInstruction { + ins(ArmOp::Movw { rd, imm16 }) + } + + fn add(rd: Reg, rn: Reg, rm: Reg) -> ArmInstruction { + ins(ArmOp::Add { + rd, + rn, + op2: Operand2::Reg(rm), + }) + } + + fn label(n: &str) -> ArmInstruction { + ins(ArmOp::Label { + name: n.to_string(), + }) + } + + fn bx_lr() -> ArmInstruction { + ins(ArmOp::Bx { rm: Reg::LR }) + } + + // ---- straight-line --------------------------------------------------- + + #[test] + fn identity_rewrite_holds() { + let s = vec![add(Reg::R0, Reg::R0, Reg::R1), bx_lr()]; + assert_eq!(validate_abi_contract(&s, &s), AbiContractVerdict::Holds); + } + + #[test] + fn renaming_a_dead_temp_holds() { + // r2 is a scratch; renaming it to r3 must not disturb the contract. + let o = vec![movw(Reg::R2, 7), add(Reg::R0, Reg::R0, Reg::R2), bx_lr()]; + let r = vec![movw(Reg::R3, 7), add(Reg::R0, Reg::R0, Reg::R3), bx_lr()]; + assert_eq!(validate_abi_contract(&o, &r), AbiContractVerdict::Holds); + } + + #[test] + fn result_left_in_the_wrong_register_is_violated() { + // The v0.53 class, minimal: the sum lands in r4 instead of r0. + let o = vec![add(Reg::R0, Reg::R0, Reg::R1), bx_lr()]; + let r = vec![add(Reg::R4, Reg::R0, Reg::R1), bx_lr()]; + assert_eq!( + validate_abi_contract(&o, &r), + AbiContractVerdict::Violated { + sink: 1, + reg: Reg::R0 + } + ); + } + + #[test] + fn reading_a_parameter_from_the_wrong_register_is_violated() { + // The AAPCS parameter half of the anchor: `Init(R1)` and `Init(R0)` are + // distinct shared symbols, so swapping the source is a value change. + let o = vec![mov(Reg::R0, Reg::R1), bx_lr()]; + let r = vec![mov(Reg::R0, Reg::R2), bx_lr()]; + assert_eq!( + validate_abi_contract(&o, &r), + AbiContractVerdict::Violated { + sink: 1, + reg: Reg::R0 + } + ); + } + + #[test] + fn high_half_of_an_i64_result_is_in_the_contract() { + let o = vec![movw(Reg::R1, 9), bx_lr()]; + let r = vec![movw(Reg::R5, 9), bx_lr()]; + assert_eq!( + validate_abi_contract(&o, &r), + AbiContractVerdict::Violated { + sink: 1, + reg: Reg::R1 + } + ); + } + + // ---- across a join --------------------------------------------------- + + fn ifelse(then_dst: Reg, else_dst: Reg, join_src: Reg) -> Vec { + vec![ + ins(ArmOp::Cmp { + rn: Reg::R0, + op2: Operand2::Imm(0), + }), + ins(ArmOp::Bcc { + cond: Condition::EQ, + label: ".Lelse".to_string(), + }), + movw(then_dst, 1), + ins(ArmOp::B { + label: ".Ljoin".to_string(), + }), + label(".Lelse"), + movw(else_dst, 2), + label(".Ljoin"), + mov(Reg::R0, join_src), + bx_lr(), + ] + } + + #[test] + fn consistent_cross_arm_rename_across_a_join_holds() { + let o = ifelse(Reg::R4, Reg::R4, Reg::R4); + let r = ifelse(Reg::R6, Reg::R6, Reg::R6); + assert_eq!(validate_abi_contract(&o, &r), AbiContractVerdict::Holds); + } + + #[test] + fn one_armed_rename_across_a_join_is_violated() { + // Only the THEN arm is renamed: on the else path r6 is not the value the + // join consumes. A straight-line walk structurally cannot see this. + let o = ifelse(Reg::R4, Reg::R4, Reg::R4); + let r = ifelse(Reg::R6, Reg::R4, Reg::R6); + assert_eq!( + validate_abi_contract(&o, &r), + AbiContractVerdict::Violated { + sink: 8, + reg: Reg::R0 + } + ); + } + + // ---- loops (coinduction, no unrolling) -------------------------------- + + fn counted_loop(acc: Reg) -> Vec { + vec![ + movw(acc, 0), + label(".Lhead"), + ins(ArmOp::Add { + rd: acc, + rn: acc, + op2: Operand2::Imm(1), + }), + ins(ArmOp::Sub { + rd: Reg::R1, + rn: Reg::R1, + op2: Operand2::Imm(1), + }), + ins(ArmOp::Cmp { + rn: Reg::R1, + op2: Operand2::Imm(0), + }), + ins(ArmOp::Bcc { + cond: Condition::NE, + label: ".Lhead".to_string(), + }), + mov(Reg::R0, acc), + bx_lr(), + ] + } + + #[test] + fn loop_carried_rename_holds_by_coinduction() { + let o = counted_loop(Reg::R4); + let r = counted_loop(Reg::R7); + assert_eq!(validate_abi_contract(&o, &r), AbiContractVerdict::Holds); + } + + #[test] + fn loop_result_left_in_the_wrong_register_is_violated() { + let o = counted_loop(Reg::R4); + let mut r = counted_loop(Reg::R4); + // Return the loop COUNTER instead of the accumulator. + r[6] = mov(Reg::R0, Reg::R1); + assert_eq!( + validate_abi_contract(&o, &r), + AbiContractVerdict::Violated { + sink: 7, + reg: Reg::R0 + } + ); + } + + // ---- loud declines, never a silent pass ------------------------------- + + // ---- calls (VCR-DEC-001 increment 3, #896) --------------------------- + + fn bl(f: &str) -> ArmInstruction { + ins(ArmOp::Bl { + label: f.to_string(), + }) + } + + /// `held` carries a value across a call, then it is returned: + /// movw held,#7 ; bl f ; mov r0,held ; bx lr + fn across_call(held: Reg) -> Vec { + vec![movw(held, 7), bl("f"), mov(Reg::R0, held), bx_lr()] + } + + #[test] + fn a_call_is_modeled_not_declined() { + let s = across_call(Reg::R4); + assert_eq!(validate_abi_contract(&s, &s), AbiContractVerdict::Holds); + } + + #[test] + fn recolouring_a_callee_saved_value_to_another_callee_saved_holds() { + let o = across_call(Reg::R4); + let r = across_call(Reg::R7); + assert_eq!(validate_abi_contract(&o, &r), AbiContractVerdict::Holds); + } + + #[test] + fn recolouring_a_live_value_into_caller_saved_across_a_call_is_violated() { + // THE miscompile increment 3 must not commit: the value is parked in + // R2, which the AAPCS destroys at the call. The forward walk rebinds R2 + // to the CALL's own node, so it can no longer bisimulate with the + // original's `movw` — caught as a VALUE disagreement, with no liveness + // reasoning anywhere. + let o = across_call(Reg::R4); + let r = across_call(Reg::R2); + assert_eq!( + validate_abi_contract(&o, &r), + AbiContractVerdict::Violated { + sink: 3, + reg: Reg::R0 + } + ); + } + + #[test] + fn returning_the_call_result_directly_holds() { + // r0 after `bl` is the callee's result on both sides. + let s = vec![bl("f"), bx_lr()]; + assert_eq!(validate_abi_contract(&s, &s), AbiContractVerdict::Holds); + } + + #[test] + fn renaming_what_feeds_a_call_argument_is_violated() { + // Same callee, DIFFERENT argument value ⇒ the result node's operands + // differ ⇒ the returned value differs. `call_effect`'s `uses` are what + // make this visible; without them the two calls would look identical. + let o = vec![mov(Reg::R0, Reg::R4), bl("f"), bx_lr()]; + let r = vec![mov(Reg::R0, Reg::R5), bl("f"), bx_lr()]; + assert_eq!( + validate_abi_contract(&o, &r), + AbiContractVerdict::Violated { + sink: 2, + reg: Reg::R0 + } + ); + } + + #[test] + fn a_rewritten_call_target_declines_loudly() { + // A register allocator never rewrites a call's architectural operands — + // the rule `validate_cfg_rewrite` enforces too. A stream where one did + // must decline, not be analyzed under the shared-skeleton assumption. + let o = vec![bl("f"), bx_lr()]; + let r = vec![bl("g"), bx_lr()]; + assert_eq!( + validate_abi_contract(&o, &r), + AbiContractVerdict::NotAttempted { + reason: "control-flow-rewritten" + } + ); + } + + #[test] + fn the_call_pseudo_op_still_declines_loudly() { + // `Call` expands downstream into a guard + table load + `blx`, so this + // stream's register footprint is not the final code's. + let s = vec![ + ins(ArmOp::Call { + rd: Reg::R0, + func_idx: 3, + }), + bx_lr(), + ]; + assert_eq!( + validate_abi_contract(&s, &s), + AbiContractVerdict::NotAttempted { + reason: "call-pseudo-op" + } + ); + } + + #[test] + fn a_rewritten_branch_declines_loudly() { + let o = ifelse(Reg::R4, Reg::R4, Reg::R4); + let mut r = o.clone(); + r[1] = ins(ArmOp::Bcc { + cond: Condition::NE, + label: ".Lelse".to_string(), + }); + assert_eq!( + validate_abi_contract(&o, &r), + AbiContractVerdict::NotAttempted { + reason: "control-flow-rewritten" + } + ); + } + + #[test] + fn an_endless_loop_with_no_return_declines_rather_than_passing() { + let s = vec![ + label(".Lhead"), + ins(ArmOp::B { + label: ".Lhead".to_string(), + }), + ]; + assert_eq!( + validate_abi_contract(&s, &s), + AbiContractVerdict::NotAttempted { + reason: "no-return-sink" + } + ); + } + + #[test] + fn a_pop_that_restores_a_result_register_declines_rather_than_passing() { + let s = vec![ + ins(ArmOp::Push { + regs: vec![Reg::R0, Reg::LR], + }), + ins(ArmOp::Pop { + regs: vec![Reg::R0, Reg::PC], + }), + ]; + assert_eq!( + validate_abi_contract(&s, &s), + AbiContractVerdict::NotAttempted { + reason: "return-restores-result-register" + } + ); + } + + #[test] + fn a_normal_prologue_epilogue_is_analyzed_not_declined() { + let s = vec![ + ins(ArmOp::Push { + regs: vec![Reg::R4, Reg::LR], + }), + add(Reg::R0, Reg::R0, Reg::R1), + ins(ArmOp::Pop { + regs: vec![Reg::R4, Reg::PC], + }), + ]; + assert_eq!(validate_abi_contract(&s, &s), AbiContractVerdict::Holds); + } + + #[test] + fn an_unmodeled_straight_line_op_declines_loudly() { + // An FP op is straight-line but has no `reg_effect` model. It must + // DECLINE, not be walked past as a no-op. + let s = vec![ + ins(ArmOp::F32Add { + sd: VfpReg::S0, + sn: VfpReg::S1, + sm: VfpReg::S2, + }), + add(Reg::R0, Reg::R0, Reg::R1), + bx_lr(), + ]; + assert_eq!( + validate_abi_contract(&s, &s), + AbiContractVerdict::NotAttempted { + reason: "unmodeled-op" + } + ); + } + + #[test] + fn an_unanalyzable_op_in_the_middle_of_a_block_declines() { + // The fail-open bug this module's own red-first testing found: a `bl` + // that is not a block ENDER must still be rejected. Modeling it as a + // no-op would hide the AAPCS clobber of R0-R3/R12 — the same + // "unmodeled construct silently certified" shape as #872. + let s = vec![ + add(Reg::R0, Reg::R0, Reg::R1), + ins(ArmOp::BrTable { + rd: Reg::R0, + index_reg: Reg::R1, + targets: vec![], + default: 0, + }), + add(Reg::R0, Reg::R0, Reg::R1), + bx_lr(), + ]; + assert_eq!( + validate_abi_contract(&s, &s), + AbiContractVerdict::NotAttempted { reason: "br-table" } + ); + } + + #[test] + fn a_length_mismatch_declines() { + let o = vec![add(Reg::R0, Reg::R0, Reg::R1), bx_lr()]; + let r = vec![bx_lr()]; + assert_eq!( + validate_abi_contract(&o, &r), + AbiContractVerdict::NotAttempted { + reason: "length-mismatch" + } + ); + } + + #[test] + fn a_store_only_rewrite_is_a_named_false_negative() { + // DOCUMENTED LIMITATION, pinned so it cannot drift silently: memory is + // not in the obligation, so a mis-renamed store address that no register + // value depends on is invisible here. `validate_cfg_rewrite`'s + // use-equations cover this class when its seed is intact — the two + // instruments are COMPLEMENTARY, which is what independence looks like. + let st = |base: Reg| { + ins(ArmOp::Str { + rd: Reg::R0, + addr: MemAddr { + base, + offset: 4, + offset_reg: None, + }, + }) + }; + let o = vec![st(Reg::R11), bx_lr()]; + let r = vec![st(Reg::R10), bx_lr()]; + assert_eq!(validate_abi_contract(&o, &r), AbiContractVerdict::Holds); + } +} diff --git a/crates/synth-synthesis/src/graph_alloc.rs b/crates/synth-synthesis/src/graph_alloc.rs index a62c6455..94d944d9 100644 --- a/crates/synth-synthesis/src/graph_alloc.rs +++ b/crates/synth-synthesis/src/graph_alloc.rs @@ -57,15 +57,24 @@ //! [`crate::liveness::validate_final_allocation`] re-checks the final stream //! through an INDEPENDENTLY written CFG builder. //! -//! **And the validators are not sufficient.** `validate_cfg_rewrite` shares the -//! CFG shape with the pass it validates, so — #872's standing lesson — it cannot -//! catch an error in what they share. Increment 2's divergent bytes are therefore -//! EXECUTED against wasmtime by -//! `scripts/repro/vcr_dec_001_join_alloc_execution_differential.py`, which is -//! proven non-vacuous by mutation: emptying the shared exit contract emits code -//! that leaves the return value in the wrong register, and BOTH validators accept -//! it. - +//! **And the dataflow validators are not sufficient.** `validate_cfg_rewrite` +//! shares the CFG shape AND the exit contract with the pass it validates, so — +//! #872's standing lesson — it cannot catch an error in what they share. v0.53 +//! measured exactly what that costs: emptying [`crate::liveness::cfg_exit_observable`] +//! emits code that leaves the return value in the wrong register, and BOTH +//! `validate_cfg_rewrite` and VCR-RA-003 accept it. Increment 2's divergent bytes +//! are therefore also EXECUTED against wasmtime by +//! `scripts/repro/vcr_dec_001_join_alloc_execution_differential.py`. +//! +//! **VCR-VER-004 (v0.54) closes that specific hole statically.** Every rewrite +//! this module emits must ALSO satisfy +//! [`crate::abi_contract::validate_abi_contract`] — a forward, value-level check +//! whose obligation is the AAPCS result registers rather than a table the pass +//! reads, and which takes NOTHING from this pass (not the CFG, not a seed). Its +//! `NotAttempted` is treated as a DECLINE here, not as a pass: a function this +//! module applies to has been ABI-contract-certified, or it was not applied. + +use crate::abi_contract::{AbiContractVerdict, validate_abi_contract}; use crate::instruction_selector::ArmInstruction; use crate::liveness::{ apply_range_coloring, color_ranges, is_straight_line, range_interference, reg_effect, @@ -74,6 +83,28 @@ use crate::liveness::{ use crate::rules::Reg; use std::collections::{BTreeMap, BTreeSet}; +/// The VCR-VER-004 acceptance gate, applied on top of whichever dataflow +/// validator the caller already discharged. +/// +/// Returns the rewrite only if the ABI observable contract is PROVEN preserved. +/// A [`AbiContractVerdict::NotAttempted`] is a decline, deliberately: if a +/// decline counted as acceptance, a change that made this check universally +/// inapplicable would disable it silently — the vacuity failure this whole lane +/// exists to prevent. +fn abi_gate(orig: &[ArmInstruction], new: Vec) -> Option> { + match validate_abi_contract(orig, &new) { + AbiContractVerdict::Holds => Some(new), + v => { + if std::env::var("SYNTH_GRAPH_ALLOC_STATS").is_ok() { + eprintln!( + "[graph-alloc] REJECTED by the ABI observable contract (VCR-VER-004): {v:?}" + ); + } + None + } + } +} + /// Is `SYNTH_GRAPH_ALLOC` enabled? Any value other than `0` turns the spike on; /// unset or `0` keeps the shipping path (byte-identical). pub fn enabled() -> bool { @@ -226,7 +257,10 @@ fn reallocate_straight_line( // exact Err/Ok this match discharges to decline/accept). let new = apply_range_coloring(instrs, &assignment)?; match validate_segment_rewrite(instrs, &new) { - Ok(()) => Some(new), + // TWO instruments, on different axes: the backward name-equation trace + // check, and the forward ABI value contract (VCR-VER-004). Both must + // hold. + Ok(()) => abi_gate(instrs, new), Err(_) => None, } } @@ -1283,7 +1317,23 @@ mod joins { // (it may still find a segment-local win we did not). decline("identity-colouring") } else { - Some(out) + // Announce the dataflow ACCEPT before the second gate runs. + // This line is the machine-checkable half of the v0.53 + // finding: on the mutated compiler it is printed for the + // very function VCR-VER-004 then rejects, so "the two + // existing instruments are green on this input" is an + // OBSERVATION, not a claim + // (`scripts/repro/vcr_ver_004_instrument_independence.py`). + if std::env::var("SYNTH_GRAPH_ALLOC_STATS").is_ok() { + eprintln!( + "[graph-alloc] join colouring ACCEPTED by validate_cfg_rewrite (dataflow)" + ); + } + // VCR-VER-004: and the ABI observable contract, which shares + // neither the exit contract nor the CFG with this pass. This + // is the gate that catches the v0.53 mutation the two + // dataflow validators both accept. + abi_gate(instrs, out) } } Err(v) => { @@ -1334,6 +1384,12 @@ mod tests { rn: Reg::R2, op2: Operand2::Reg(Reg::R1), }), + // A WELL-FORMED function: it returns. VCR-VER-004 declines a stream + // with no return sink rather than passing it vacuously, so a fixture + // without an epilogue is not a function this pass may apply to. + ins(ArmOp::Pop { + regs: vec![Reg::R4, Reg::PC], + }), ]; let out = reallocate(&body, &POOL).expect("straight-line function colours"); // The rewrite must pass the trace-equality validator (it did, or @@ -1393,6 +1449,12 @@ mod tests { rn: Reg::R0, op2: Operand2::Reg(Reg::R0), }), + // 3: the epilogue — see the note in the test above. Appending it at + // index 3 leaves the def indices this test reasons about (0, 1, 2) + // untouched. + ins(ArmOp::Pop { + regs: vec![Reg::R4, Reg::PC], + }), ]; // The r1 range opened at instruction 1 is free (def index 1, overwritten // at 2). It is dead-on-arrival (defined, immediately overwritten), so it diff --git a/crates/synth-synthesis/src/lib.rs b/crates/synth-synthesis/src/lib.rs index 450c9863..9dde38cd 100644 --- a/crates/synth-synthesis/src/lib.rs +++ b/crates/synth-synthesis/src/lib.rs @@ -1,5 +1,6 @@ //! Synth Synthesis - Code synthesis engine +pub mod abi_contract; pub mod contracts; pub mod control_flow; pub mod graph_alloc; diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index 1c00bf09..ab401af8 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -145,3 +145,31 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. by `validate_cfg_rewrite` AND VCR-RA-003 *both*, caught only by execution (VCR-DEC-001, flag-off). Two validators sharing a blind spot agree without adding evidence. +- **That second residual is now closed STATICALLY** (VCR-VER-004, v0.54): + `abi_contract::validate_abi_contract` is a FORWARD, value-level check whose + obligation is the AAPCS result registers hard-named in its own source and whose + CFG is re-derived from both instruction streams — it takes nothing from the + pass, so emptying the shared exit contract cannot empty it. Re-running v0.53's + exact mutation, the two dataflow validators stay green (`validate_cfg_rewrite` + → Ok, VCR-RA-003 → Consistent) while this one rejects with a concrete violation + naming `R0`, and the miscompile is not emitted. That is a CI job, not a claim. +- What VCR-VER-004 does **not** close, stated plainly: + - It is a **gate only on the flag-off** graph-colouring allocator. On the + DEFAULT path it is a report-only audit held to a CI floor — measured + `Holds 422 / NotAttempted 195 / Violated 0` over 617 corpus functions, so it + proves the observable return contract on ~68 % of the shipping path — + `bl`/`blx` calls included, via the shared AAPCS `liveness::call_effect` — and + declines (never guesses) on the rest. Making it gate the default path means + hard-erroring a user's compile on a checker whose false-positive rate is + measured, not proven; that flip is deliberately not taken here. + - **Memory is not in its obligation.** A mis-renamed store address that a later + load reads back is a false negative for this instrument (it is covered by + `validate_cfg_rewrite`'s use-equations when that seed is intact — the two are + complementary, which is what independence looks like, not redundancy). + - **The op model is still shared.** Def/use extraction runs through + `liveness::reg_effect`, so a *mismodeled op* remains a blind spot common to + all three instruments. VCR-VER-004 closes the shared-*contract* hole, not the + shared-*op-model* hole. `synth-verify`'s `ArmSemantics::encode_op` is a + genuinely second model of the same operations; pinning the two against each + other is the next rung, and until it is done "three independent validators" + would be an overclaim. diff --git a/scripts/repro/mutations/v053_shared_exit_contract.patch b/scripts/repro/mutations/v053_shared_exit_contract.patch new file mode 100644 index 00000000..e4239d27 --- /dev/null +++ b/scripts/repro/mutations/v053_shared_exit_contract.patch @@ -0,0 +1,36 @@ +diff --git a/crates/synth-synthesis/src/graph_alloc.rs b/crates/synth-synthesis/src/graph_alloc.rs +index 94d944d..128d900 100644 +--- a/crates/synth-synthesis/src/graph_alloc.rs ++++ b/crates/synth-synthesis/src/graph_alloc.rs +@@ -926,11 +926,9 @@ mod joins { + } + } + let own = orig_colour.get(&n).copied(); +- let pick = own +- .filter(|&c| c < caller_saved && c < k && !used[c]) +- .or_else(|| (0..caller_saved.min(k)).find(|&c| !used[c])) +- .or_else(|| own.filter(|&c| c < k && !used[c])) +- .or_else(|| (0..k).find(|&c| !used[c])); ++ // ***L6 MUTATION (v0.53 reproduction): drop the churn bias.*** ++ let _ = (own, caller_saved); ++ let pick = (0..k).find(|&c| !used[c]); + match pick { + Some(c) => { + colour.insert(n, c); +diff --git a/crates/synth-synthesis/src/liveness.rs b/crates/synth-synthesis/src/liveness.rs +index 0f6e67c..4109561 100644 +--- a/crates/synth-synthesis/src/liveness.rs ++++ b/crates/synth-synthesis/src/liveness.rs +@@ -3490,9 +3490,9 @@ pub fn cfg_exit_observable(terminator: &ArmOp) -> BTreeSet { + ]; + let pop_return = matches!(terminator, ArmOp::Pop { regs } if regs.contains(&Reg::PC)); + const AAPCS_DEAD_AT_POP_RETURN: [Reg; 4] = [R2, R3, R12, LR]; +- ALL.into_iter() +- .filter(|r| !(pop_return && AAPCS_DEAD_AT_POP_RETURN.contains(r))) +- .collect() ++ // ***L6 MUTATION (v0.53 reproduction): empty the shared exit contract.*** ++ let _ = (ALL, pop_return, AAPCS_DEAD_AT_POP_RETURN); ++ BTreeSet::new() + } + + /// VCR-DEC-001 **increment 3** — the AAPCS register contract of a CALL, as a diff --git a/scripts/repro/vcr_ver_004_instrument_independence.py b/scripts/repro/vcr_ver_004_instrument_independence.py new file mode 100644 index 00000000..73659a05 --- /dev/null +++ b/scripts/repro/vcr_ver_004_instrument_independence.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python3 +# ci-status: wired +"""VCR-VER-004 — INSTRUMENT INDEPENDENCE, proven by re-running v0.53's mutation. + +**The finding this responds to.** v0.53's VCR-DEC-001 lane proved BY MUTATION +that emptying `liveness::cfg_exit_observable` — the exit contract the join-aware +graph allocator and its own CFG validator SHARE — makes the compiler emit code +that leaves the function's return value in the WRONG REGISTER, and that BOTH +per-compilation validators accept it: + + * `validate_cfg_rewrite` (the pass's acceptance oracle) -> Ok + * `validate_final_allocation`(VCR-RA-003, whole-function) -> Consistent + +Only EXECUTION caught it. Two independent-*looking* instruments, one shared +blind spot — and a direct counterexample to the claim that per-compilation +validation is an independent check on the code generator. + +**What this script proves.** It re-applies v0.53's EXACT mutation (the committed +patch `mutations/v053_shared_exit_contract.patch` — not a reconstruction, not an +artificially constructed input), rebuilds, and asserts on the SAME compilation of +the SAME fixture: + + (1) `validate_cfg_rewrite` ACCEPTS the rewrite [the blind spot] + (2) VCR-RA-003 reports Consistent [the blind spot] + (3) VCR-VER-004 `validate_abi_contract` REJECTS it with a CONCRETE violation + naming the ABI result register [the new instrument] + (4) the miscompile is therefore NOT EMITTED: the function declines to the + shipping allocator. + +(1) is the load-bearing assertion. It is what makes (3) non-vacuous: because the +dataflow gate returned Ok, the pre-VCR-VER-004 compiler would have emitted this +rewrite. No opt-out flag is needed to show that, and deliberately none exists — +an env var that disables the instrument would be a footgun, not evidence. + +**Why the new check fails differently** (the point of the lane, in one line): +`validate_cfg_rewrite` is a BACKWARD must-analysis whose obligation set is a +VARIABLE seeded from the shared table, and the empty set is a fixpoint — so +emptying the seed makes it vacuously green. `validate_abi_contract` is a FORWARD +value analysis whose obligation is the AAPCS result registers, hard-named in its +own source; a forward evaluation always produces exactly one value for R0 at each +return, so there is always exactly one obligation per sink and there is no seed +to shrink. + +**Proven RED-FIRST, and the evidence is reproducible.** Change `abi_gate` in +`graph_alloc.rs` to treat `AbiContractVerdict::Violated` as an accept, rebuild, +and re-run with the mutation applied: the compiler prints +`whole-function colouring APPLIED (validated)` and EMITS the miscompile, so +assertions (3) and (4) both fail. With the gate intact it prints +`DECLINED → shipping reallocate_function`. The gate is load-bearing, not +decorative. + +Run (needs cargo; no emulator, no solver): + python3 scripts/repro/vcr_ver_004_instrument_independence.py +Exits nonzero if any of (1)-(4) does not hold. ALWAYS restores the tree. +""" + +import os +import re +import subprocess +import sys +from pathlib import Path + +REPO = Path(__file__).resolve().parents[2] +PATCH = REPO / "scripts/repro/mutations/v053_shared_exit_contract.patch" +FIXTURE = REPO / "scripts/repro/brif_outer_740.wat" +TOUCHED = [ + "crates/synth-synthesis/src/liveness.rs", + "crates/synth-synthesis/src/graph_alloc.rs", +] + +# The exact three verdict lines, as emitted by the compiler under +# SYNTH_GRAPH_ALLOC_STATS / SYNTH_RA003_VERBOSE. +ACCEPT_DATAFLOW = "[graph-alloc] join colouring ACCEPTED by validate_cfg_rewrite (dataflow)" +RA003_CONSISTENT = "VCR-RA-003: Consistent" +ABI_REJECT = re.compile( + r"\[graph-alloc\] REJECTED by the ABI observable contract \(VCR-VER-004\): " + r"Violated \{ sink: (\d+), reg: (R0|R1) \}" +) +DECLINED = "[graph-alloc] DECLINED → shipping reallocate_function" + + +def run(cmd, **kw): + return subprocess.run(cmd, cwd=REPO, capture_output=True, text=True, **kw) + + +def build(): + r = run(["cargo", "build", "--bin", "synth"]) + if r.returncode != 0: + print(r.stderr[-4000:], file=sys.stderr) + raise SystemExit("FATAL: cargo build failed") + # Resolve the binary the way cargo did (CARGO_TARGET_DIR may be redirected — + # the stale-./target/debug/synth trap). + meta = run(["cargo", "metadata", "--format-version", "1", "--no-deps"]) + import json + + target_dir = json.loads(meta.stdout)["target_directory"] + return str(Path(target_dir) / "debug" / "synth") + + +def compile_fixture(synth): + env = dict(os.environ) + env.update( + SYNTH_GRAPH_ALLOC="1", + SYNTH_GRAPH_ALLOC_STATS="1", + SYNTH_RA003_VERBOSE="1", + ) + r = subprocess.run( + [synth, "compile", str(FIXTURE), "--relocatable", "-o", os.devnull], + cwd=REPO, + capture_output=True, + text=True, + env=env, + ) + return r.stdout + r.stderr + + +def main(): + if not PATCH.is_file(): + raise SystemExit(f"FATAL: missing mutation patch {PATCH}") + dirty = run(["git", "diff", "--name-only", "--"] + TOUCHED).stdout.split() + if dirty: + raise SystemExit( + "FATAL: the files the mutation touches are already modified: " + + ", ".join(dirty) + ) + + problems = [] + + # ---- BASELINE: the unmutated compiler applies to this fixture ---------- + synth = build() + base = compile_fixture(synth) + if ACCEPT_DATAFLOW not in base: + problems.append( + "BASELINE: the join allocator does not reach the fixture — this " + "script would gate nothing. Re-pick the fixture." + ) + if ABI_REJECT.search(base): + problems.append( + "BASELINE: VCR-VER-004 rejects the UNMUTATED compiler — a FALSE " + "REJECTION. The instrument is broken, not the compiler." + ) + if problems: + for p in problems: + print("FAIL " + p) + return 1 + print("OK baseline: join colouring applies AND the ABI contract holds") + + # ---- MUTATED: v0.53's exact mutation, re-applied ----------------------- + r = run(["git", "apply", str(PATCH)]) + if r.returncode != 0: + print(r.stderr, file=sys.stderr) + raise SystemExit("FATAL: could not apply the mutation patch") + try: + synth = build() + out = compile_fixture(synth) + finally: + rev = run(["git", "apply", "-R", str(PATCH)]) + if rev.returncode != 0: + print(rev.stderr, file=sys.stderr) + raise SystemExit("FATAL: could not REVERT the mutation — tree dirty!") + + # (1) the pass's own dataflow oracle is GREEN on this rewrite + if ACCEPT_DATAFLOW in out: + print("OK (1) validate_cfg_rewrite ACCEPTS the mutated rewrite") + else: + problems.append( + "(1) validate_cfg_rewrite did NOT accept — the mutation no longer " + "reproduces the v0.53 blind spot, so (3) proves nothing" + ) + + # (2) VCR-RA-003 is GREEN on the same compilation + if RA003_CONSISTENT in out: + print("OK (2) VCR-RA-003 validate_final_allocation reports Consistent") + else: + problems.append("(2) VCR-RA-003 did not report Consistent") + + # (3) VCR-VER-004 REJECTS, concretely + m = ABI_REJECT.search(out) + if m: + print( + f"OK (3) VCR-VER-004 REJECTS: result register {m.group(2)} holds a " + f"different value at the return terminator (instr {m.group(1)})" + ) + else: + problems.append( + "(3) VCR-VER-004 did NOT reject the mutated rewrite — the static " + "check does not catch the class it exists for" + ) + + # (4) and therefore the miscompile is not emitted + if DECLINED in out: + print("OK (4) the function DECLINES to the shipping allocator — not emitted") + else: + problems.append("(4) the function did not decline; the rewrite was emitted") + + print() + print(f"VCR-VER-004-INDEPENDENCE ASSERTIONS={4 - len(problems)}/4") + if problems: + for p in problems: + print("FAIL " + p) + print("RESULT: FAIL") + return 1 + print("RESULT: PASS — the v0.53 mutation is now caught STATICALLY, by an") + print(" instrument that shares neither the exit contract nor the CFG") + print(" with the pass, while both dataflow validators stay green.") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/repro/vcr_ver_004_shipping_path_audit.py b/scripts/repro/vcr_ver_004_shipping_path_audit.py new file mode 100644 index 00000000..53ffbf74 --- /dev/null +++ b/scripts/repro/vcr_ver_004_shipping_path_audit.py @@ -0,0 +1,156 @@ +#!/usr/bin/env python3 +# ci-status: wired +"""VCR-VER-004 — the ABI observable contract on the SHIPPING allocator (#242). + +The sibling script `vcr_ver_004_instrument_independence.py` proves the new +instrument catches v0.53's mutation on the flag-off graph-colouring spike. That +spike is not what users compile with. THIS script asks the same question of the +DEFAULT path — `liveness::reallocate_function_post_exhaust`, the allocator every +`synth compile` runs — and turns the answer into an enforced floor. + +For every function in the ARM repro corpus (`--relocatable`, the label-form path +the checker can analyze) it collects `SYNTH_ABI_CONTRACT_AUDIT=1`'s per-function +verdict and asserts: + + (A) ZERO `Violated`. This is the real gate. A violation here means the SHIPPING + allocator moved a value out of an AAPCS result register — the exact class + v0.53's mutation produced and both dataflow validators missed. It is also + the FALSE-REJECTION alarm: the shipping allocator is known-good on this + corpus (frozen anchors + every execution differential), so a `Violated` + is far more likely to be a bug in the INSTRUMENT than in the compiler. + Either way it must not pass silently. + (B) a floor on `Holds`. Coverage is the honest weak point of a checker that + declines on calls and unmodeled ops, so it is PINNED: if a change makes the + instrument see less of the shipping path, that regression is visible rather + than absorbed. The floor is set below the measured value, not at it, so + normal corpus churn does not create noise. + +The audit hook is REPORT-ONLY inside the compiler, deliberately. Making it gate +the default path would mean hard-erroring a user's compile on a checker whose +false-positive rate is only measured, not proven — the honest sequence is +measure first, flip on evidence. This script is that measurement, held to a +floor. + +Measured at the time of writing (v0.54, 617 corpus functions, --relocatable): + Holds 422 · NotAttempted 195 · Violated 0 + declines: unmodeled-op 174, indirect-call-pseudo-op 11, + numeric-offset-branch 10 + +Before the AAPCS call model landed (VCR-DEC-001 increment 3, #896) this read +`Holds 376 · NotAttempted 241`, with `call 62` its second-largest decline. The +62 direct-call declines are GONE, not reclassified; `unmodeled-op` rose 159 -> +174 because functions that used to stop at the call now get further and reach an +FP / i64-pair op instead — the decline MOVED, it did not vanish. + +Proven RED-FIRST, by real exit code, in both directions: + * a stub `SYNTH` that emits a `Violated` line -> exit 1, naming the fixture; + * a stub that emits nothing at all -> exit 1 on the vacuity + assertion ("the audit hook produced NO verdicts"), so a stale binary or an + un-wired hook cannot make this job pass while gating nothing; + * the real binary -> exit 0. + +Run: SYNTH=./target/debug/synth python3 scripts/repro/vcr_ver_004_shipping_path_audit.py +Exits nonzero on any Violated, or if Holds falls below the floor. +""" + +import os +import re +import subprocess +import sys +from collections import Counter +from pathlib import Path + +REPO = Path(__file__).resolve().parents[2] +REPRO = REPO / "scripts/repro" +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") + +# Set below the measured 422 so ordinary corpus churn is not noise, but close +# enough that losing a whole construct class (a `reg_effect` arm, the AAPCS +# `call_effect`, the label-form CFG, the return-sink recognition) trips it. +# Raised from 340 when VCR-DEC-001 increment 3 (#896) made calls modelable: a +# floor left at the pre-call-model value would have silently absorbed losing the +# entire call model again. +HOLDS_FLOOR = 400 + +VERDICT = re.compile(r"\[abi-contract-audit\] (Holds|Violated|NotAttempted)(.*)") +REASON = re.compile(r'reason: "([a-z-]+)"') + + +def main(): + fixtures = sorted( + [p for p in REPRO.glob("*.wat")] + [p for p in REPRO.glob("*.wasm")] + ) + if not fixtures: + print("FAIL no corpus fixtures found") + return 1 + + env = dict(os.environ, SYNTH_ABI_CONTRACT_AUDIT="1") + verdicts = Counter() + reasons = Counter() + violations = [] + + for f in fixtures: + r = subprocess.run( + [SYNTH, "compile", str(f), "--relocatable", "-o", os.devnull], + cwd=REPO, + capture_output=True, + text=True, + env=env, + ) + for line in (r.stdout + r.stderr).splitlines(): + m = VERDICT.search(line) + if not m: + continue + kind, rest = m.group(1), m.group(2) + verdicts[kind] += 1 + if kind == "NotAttempted": + rm = REASON.search(rest) + reasons[rm.group(1) if rm else "?"] += 1 + elif kind == "Violated": + violations.append(f"{f.name}: {line.strip()}") + + total = sum(verdicts.values()) + print(f"functions audited (--relocatable) : {total}") + print(f" Holds : {verdicts['Holds']}") + print(f" NotAttempted : {verdicts['NotAttempted']}") + print(f" Violated : {verdicts['Violated']}") + if reasons: + print("decline reasons:") + for k, v in reasons.most_common(): + print(f" {k:<28} {v}") + + problems = [] + if total == 0: + problems.append( + "the audit hook produced NO verdicts — SYNTH_ABI_CONTRACT_AUDIT is " + "not wired, or the binary is stale. This run gated nothing." + ) + if verdicts["Violated"]: + for v in violations: + print("FAIL VIOLATION " + v) + problems.append( + f"{verdicts['Violated']} ABI observable-contract VIOLATION(s) on the " + "SHIPPING allocator" + ) + if verdicts["Holds"] < HOLDS_FLOOR: + problems.append( + f"coverage regression: Holds={verdicts['Holds']} < floor {HOLDS_FLOOR} " + "— the instrument now sees LESS of the shipping path" + ) + + print() + print( + f"VCR-VER-004-SHIPPING HOLDS={verdicts['Holds']} " + f"VIOLATED={verdicts['Violated']} TOTAL={total} FLOOR={HOLDS_FLOOR}" + ) + if problems: + for p in problems: + print("FAIL " + p) + print("RESULT: FAIL") + return 1 + print("RESULT: PASS") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/templates/feature_matrix.md.tmpl b/scripts/templates/feature_matrix.md.tmpl index 0c8585ba..918fdbaf 100644 --- a/scripts/templates/feature_matrix.md.tmpl +++ b/scripts/templates/feature_matrix.md.tmpl @@ -145,3 +145,31 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. by `validate_cfg_rewrite` AND VCR-RA-003 *both*, caught only by execution (VCR-DEC-001, flag-off). Two validators sharing a blind spot agree without adding evidence. +- **That second residual is now closed STATICALLY** (VCR-VER-004, v0.54): + `abi_contract::validate_abi_contract` is a FORWARD, value-level check whose + obligation is the AAPCS result registers hard-named in its own source and whose + CFG is re-derived from both instruction streams — it takes nothing from the + pass, so emptying the shared exit contract cannot empty it. Re-running v0.53's + exact mutation, the two dataflow validators stay green (`validate_cfg_rewrite` + → Ok, VCR-RA-003 → Consistent) while this one rejects with a concrete violation + naming `R0`, and the miscompile is not emitted. That is a CI job, not a claim. +- What VCR-VER-004 does **not** close, stated plainly: + - It is a **gate only on the flag-off** graph-colouring allocator. On the + DEFAULT path it is a report-only audit held to a CI floor — measured + `Holds 422 / NotAttempted 195 / Violated 0` over 617 corpus functions, so it + proves the observable return contract on ~68 % of the shipping path — + `bl`/`blx` calls included, via the shared AAPCS `liveness::call_effect` — and + declines (never guesses) on the rest. Making it gate the default path means + hard-erroring a user's compile on a checker whose false-positive rate is + measured, not proven; that flip is deliberately not taken here. + - **Memory is not in its obligation.** A mis-renamed store address that a later + load reads back is a false negative for this instrument (it is covered by + `validate_cfg_rewrite`'s use-equations when that seed is intact — the two are + complementary, which is what independence looks like, not redundancy). + - **The op model is still shared.** Def/use extraction runs through + `liveness::reg_effect`, so a *mismodeled op* remains a blind spot common to + all three instruments. VCR-VER-004 closes the shared-*contract* hole, not the + shared-*op-model* hole. `synth-verify`'s `ArmSemantics::encode_op` is a + genuinely second model of the same operations; pinning the two against each + other is the next rung, and until it is done "three independent validators" + would be an overclaim.