From 185d08555263a91bf2a84bb36b369cd5119b16d0 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 14:41:43 +0200 Subject: [PATCH 1/3] =?UTF-8?q?VCR-DEC-001=20increment=203:=20colour=20ACR?= =?UTF-8?q?OSS=20CALLS=20=E2=80=94=20AAPCS=20contract=20in=20pass=20AND=20?= =?UTF-8?q?validator=20(#242)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Increment 2's second-largest decline bucket was `call` / `call-indirect` (68 of the measured corpus): a `bl` had no modeled effect, so the join CFG builder refused the whole function. This increment models the AAPCS call boundary. ONE definition, TWO consumers — deliberately. `liveness::call_effect` states the contract once: defs = {R0,R1,R2,R3,R12,LR} (call-clobbered) uses = {R0,R1,R2,R3} + a `blx`'s target (arguments, conservatively all four — the callee signature is invisible here, and guessing an arity would silently corrupt a call whose argument we then recoloured) and it is consumed by BOTH `graph_alloc::joins` (liveness / interference / identity pins) AND `validate_cfg_rewrite`'s backward transfer. Modeling it in the pass alone would have been the #872 defect verbatim — the lane brief's own hazard: "a validator treating `bl` as effect-free would accept a non-identity equation across it", i.e. it would certify its own pass's "live value parked in call-clobbered scratch" miscompile. Before this commit `validate_cfg_rewrite` did exactly that (non-straight-line ops were required identical and then given NO effect). Deliberately NOT widening `reg_effect`: its `None`-on-call is load-bearing for the shipping pipeline (`body_uses_callee_saved`'s fail-safe prologue, `shrink_callee_saved_saves`' decline, VCR-RA-003 invariant 1), so widening it would move shipped bytes. `call_effect` is a separate, additive function. Pass side: `bl`/`blx` classify as FALL-THROUGH (interior, not a terminator); their webs are identity-pinned like a `Push`/`Pop` register list (#888) and the op is emitted VERBATIM with a re-check that both rename maps are the identity (`call-operand-recoloured` declines otherwise). Single-block functions containing a call are taken here too — increment 1 structurally cannot, since a call is not `is_straight_line`. Still declined by name: the HIGH-LEVEL `Call`/`CallIndirect` pseudo-ops (expanded downstream into a bounds guard + table load + result move, so the footprint here is not the one that ships). MEASURED (scripts/repro/vcr_dec_001_join_alloc_measure.py, ARM repro corpus): relocatable inc2 -46 B / -25 cyc, 275 applied -> inc3 -100 B / -33 cyc, 307 applied; 24 functions shrank (was 8), 0 cycle regressions self-contained inc2 -70 B / -9 cyc, 81 applied -> inc3 -120 B / -17 cyc, 108 applied; 27 shrank (was 10), 0 cycle regressions Decline histogram: `call` 57 -> 0 (taken); `call-indirect` 11 -> 11 (renamed `call-indirect-pseudo`, still out of scope). Flag stays OFF by default: frozen anchors 10/10 byte-identical, the flag-off path never enters this module. RED-FIRST, with the mutation that attributes the rejection to the call model: `cfg_validator_rejects_a_live_value_recoloured_across_a_call` shows R4->R2 across a `bl` is REJECTED (DefClobbersEquation) while the IDENTICAL rename over the IDENTICAL instructions with the `bl` DELETED is ACCEPTED — so the rejection comes from the call contract and nothing else. Plus: R4->R5 (callee-saved, both saved) accepted; a renamed call ARGUMENT rejected; the pass proven to colour a post-call temporary into scratch and to keep a cross-call value callee-saved. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-synthesis/src/graph_alloc.rs | 402 ++++++++++++++++++++-- crates/synth-synthesis/src/liveness.rs | 89 ++++- 2 files changed, 462 insertions(+), 29 deletions(-) diff --git a/crates/synth-synthesis/src/graph_alloc.rs b/crates/synth-synthesis/src/graph_alloc.rs index cd205eac..920bc86c 100644 --- a/crates/synth-synthesis/src/graph_alloc.rs +++ b/crates/synth-synthesis/src/graph_alloc.rs @@ -29,8 +29,23 @@ //! chains into cross-block *webs* (a reaching-def fixpoint), takes interference //! from CFG liveness and colours the whole branchy function at once — so two //! arms' values, never simultaneously live, share one register. See that module's -//! own docs for the scope (label-form branches; no calls; no pre-resolved numeric -//! branches) and for why each exclusion is a DECLINE rather than a guess. +//! own docs for the scope (label-form branches; no pre-resolved numeric branches) +//! and for why each exclusion is a DECLINE rather than a guess. +//! +//! **Increment 3 (v0.54) — colouring ACROSS CALLS.** Increment 2's biggest +//! decline bucket after unmodeled ops was `call` / `call-indirect` (68 of the +//! measured corpus): a `bl` had no modeled effect, so the CFG builder refused the +//! whole function. Increment 3 models the AAPCS call boundary — ONE definition, +//! [`crate::liveness::call_effect`], consumed by BOTH this pass (liveness, +//! interference, identity pins) and its oracle +//! ([`crate::liveness::validate_cfg_rewrite`]'s backward transfer). Modeling it +//! in the pass alone would have been the #872 defect verbatim: a validator that +//! treats `bl` as effect-free accepts a non-identity equation across it, i.e. it +//! certifies its own pass's "live value parked in call-clobbered scratch" +//! miscompile. Single-block functions containing a call are taken here too +//! (increment 1 structurally cannot, since a call is not `is_straight_line`). +//! Still declined, by name: the high-level `Call` / `CallIndirect` PSEUDO-ops +//! (expanded downstream, so their final register footprint is not this stream's). //! //! **The oracle IS the point (red-first).** A straight-line rewrite is proven //! semantics-preserving by [`crate::liveness::validate_segment_rewrite`] (the @@ -282,19 +297,32 @@ fn occurrence_costs(instrs: &[ArmInstruction]) -> Option> /// validator shares the CFG *shape* with the pass, so it is necessary, not /// sufficient — which is why RA-003 and unicorn execution both gate it. /// +/// **Calls (increment 3, v0.54).** A `bl`/`blx` is an interior instruction with +/// the AAPCS [`crate::liveness::call_effect`]: it DEFS `{R0..R3, R12, LR}` and +/// USES the argument registers `{R0..R3}` (conservatively all four — the callee's +/// signature is not visible here) plus a `blx`'s target register. Those defs make +/// every web live across the call interfere with the call-clobbered set, so the +/// colourer structurally CANNOT home a live value in caller-saved scratch; the +/// call's own webs are identity-pinned and the op is emitted verbatim. The SAME +/// `call_effect` drives [`validate_cfg_rewrite`]'s backward transfer, so the +/// oracle cannot be weaker than the pass on exactly the contract that matters — +/// the hazard this increment was briefed on ("a validator treating `bl` as +/// effect-free would accept a non-identity equation across it"). +/// /// **Bounded scope — declines, never hard-fails.** `None` (→ the shipping /// `reallocate_function`) on: numeric/pre-resolved branches (`BOffset`/ /// `BCondOffset` — their displacements are already baked, so a rename that /// changes a Thumb encoding width would silently overshoot; the label form is -/// resolved AFTER this pass), calls (`Bl`/`Blx`/`Call`/`CallIndirect` — the -/// AAPCS argument/clobber contract is a named follow-up), `BrTable`, computed +/// resolved AFTER this pass), the HIGH-LEVEL `Call`/`CallIndirect` pseudo-ops +/// (expanded downstream into a bounds guard + table load + result move, so the +/// register footprint here is not the one that ships), `BrTable`, computed /// `Bx`, duplicate/unknown labels, unreachable blocks, any op without a precise /// [`reg_effect`], any spill, and any validator rejection. mod joins { use super::*; use crate::liveness::{ - BasicBlock, RegEffect, cfg_exit_observable, is_straight_line, reg_effect, rewrite_op_maps, - validate_cfg_rewrite, + BasicBlock, RegEffect, call_effect, cfg_exit_observable, is_straight_line, reg_effect, + rewrite_op_maps, validate_cfg_rewrite, }; use crate::rules::ArmOp; @@ -355,12 +383,22 @@ mod joins { // would silently overshoot the target (#606). Re-resolving them is // the named next increment. BOffset { .. } | BCondOffset { .. } => Term::No("numeric-branch"), - // A call needs the AAPCS argument + caller-saved clobber contract - // modeled in BOTH the pass and the validator (a validator that - // treats `bl` as effect-free would accept a non-identity equation - // across it). Named follow-up. - Bl { .. } | Blx { .. } | Call { .. } => Term::No("call"), - CallIndirect { .. } => Term::No("call-indirect"), + // INCREMENT 3 (#242): a real machine call is MODELED, not declined. + // Its AAPCS argument + call-clobber contract comes from the single + // shared [`call_effect`] definition, which this pass feeds into its + // liveness / interference / pins AND `validate_cfg_rewrite` feeds + // into its backward transfer — the "model it in one and not the + // other and you build a validator that certifies its own pass's + // miscompile" hazard, closed by construction. A `bl`/`blx` FALLS + // THROUGH: it is an interior instruction, not a terminator. + Bl { .. } | Blx { .. } => Term::Fall, + // The HIGH-LEVEL call pseudo-ops stay out of scope: `Call` carries a + // result register and `CallIndirect` a table-index register, and both + // are EXPANDED downstream (bounds guard, table load, result move), so + // the register footprint this pass would colour is not the one that + // ships. Declined, with the reason named. + Call { .. } => Term::No("call-pseudo"), + CallIndirect { .. } => Term::No("call-indirect-pseudo"), BrTable { .. } => Term::No("br-table"), Bx { .. } => Term::No("computed-bx"), _ => Term::Fall, @@ -385,6 +423,10 @@ mod joins { if !matches!(ins.op, ArmOp::Label { .. }) && !matches!(ins.op, ArmOp::Bx { .. }) && reg_effect(&ins.op).is_none() + // INCREMENT 3: a call has no `reg_effect` (deliberately — + // the shipping pipeline depends on that `None`), but it + // DOES have a modeled AAPCS `call_effect`. + && call_effect(&ins.op).is_none() { return Err("unmodeled-op"); } @@ -500,7 +542,15 @@ mod joins { } } - /// Per-instruction effect (`None` for control flow / labels). + /// Per-instruction effect (`None` for pure control flow / labels). + /// + /// INCREMENT 3: a `bl`/`blx` is not straight-line but is NOT effect-free + /// either — it gets the AAPCS [`call_effect`], the SAME definition + /// `validate_cfg_rewrite` uses. That one line is what puts calls into this + /// pass's liveness, webs and interference: a web live across a call now + /// interferes with the call's `{R0..R3, R12, LR}` def webs (all + /// identity-pinned), so the colourer structurally cannot home a live value in + /// call-clobbered scratch. fn effects(instrs: &[ArmInstruction]) -> Vec> { instrs .iter() @@ -508,7 +558,7 @@ mod joins { if is_straight_line(&i.op) { reg_effect(&i.op) } else { - None + call_effect(&i.op) } }) .collect() @@ -869,8 +919,13 @@ mod joins { Err(why) => return decline(why), }; // A single-block function is increment 1's domain (tried first); this - // path exists for the branchy ones. - if blocks.len() < 2 { + // path exists for the branchy ones. EXCEPT when it contains a call: + // increment 1 requires every instruction to be `is_straight_line`, so it + // structurally declines a `bl` and would leave a straight-line CALLING + // function to the shipping pass forever. Increment 3 models calls, so a + // single-block function that has one is THIS path's job. + let has_call = instrs.iter().any(|i| call_effect(&i.op).is_some()); + if blocks.len() < 2 && !has_call { return decline("single-block"); } let eff = effects(instrs); @@ -989,14 +1044,26 @@ mod joins { } } } - // (c) ARCHITECTURAL REGISTER LISTS (#888): a `Push`/`Pop` register list - // is a bitmask whose stack layout is register-NUMBER order, matched - // pairwise between prologue and epilogue, and it carries the #490 - // callee-saved contract. Identity-pin every web a `Push` USES or a - // `Pop` DEFINES — recolouring one restores registers from a stack - // image laid out for different ones. + // (c) ARCHITECTURAL REGISTER OPERANDS. Two classes, one rule: these + // registers are fixed by the architecture or by the ABI, not chosen + // by the allocator, so every web feeding or produced by them is + // IDENTITY-pinned. + // + // * `Push`/`Pop` register lists (#888): a bitmask whose stack layout + // is register-NUMBER order, matched pairwise between prologue and + // epilogue, carrying the #490 callee-saved contract. Recolouring + // one restores registers from a stack image laid out for different + // ones — a real latent miscompile found in v0.53. + // * CALL operands (increment 3): the argument registers a `bl`/`blx` + // reads and the `{R0..R3, R12, LR}` it clobbers are the AAPCS + // contract. The call op itself is emitted VERBATIM (the apply phase + // below re-checks that), so its webs must land on their own + // registers — pinning them here is what makes that true rather than + // hoped for. for (i, ins) in instrs.iter().enumerate() { - if !matches!(&ins.op, ArmOp::Push { .. } | ArmOp::Pop { .. }) { + if !matches!(&ins.op, ArmOp::Push { .. } | ArmOp::Pop { .. }) + && call_effect(&ins.op).is_none() + { continue; } let Some(e) = &eff[i] else { return None }; @@ -1184,6 +1251,20 @@ mod joins { let w = webs.def_web[&(i, *d)]; def_map.insert(*d, *assignment.get(&w)?); } + // INCREMENT 3: a CALL is emitted VERBATIM — its operands are the + // AAPCS contract, not a colouring choice (and `validate_cfg_rewrite` + // requires non-straight-line ops to be identical on both sides). Pin + // (c) above already forces both maps to the identity here; re-check + // it rather than assume it, and DECLINE on any disagreement. A silent + // `rewrite_op_maps` on a call would be the miscompile this increment + // exists to make impossible. + if !is_straight_line(&ins.op) { + if use_map.iter().any(|(a, b)| a != b) || def_map.iter().any(|(a, b)| a != b) { + return decline("call-operand-recoloured"); + } + out.push(ins.clone()); + continue; + } out.push(ArmInstruction { op: rewrite_op_maps(&ins.op, &use_map, &def_map)?, source_line: ins.source_line, @@ -1625,7 +1706,7 @@ mod tests { /// that changes a Thumb encoding width would silently overshoot (#606). /// Out of scope by DECLINE, with the reason named. #[test] - fn declines_numeric_branches_and_calls() { + fn declines_numeric_branches() { let numeric = vec![ ins(ArmOp::Cmp { rn: Reg::R0, @@ -1642,14 +1723,279 @@ mod tests { ins(ArmOp::Bx { rm: Reg::LR }), ]; assert_eq!(joins::build_cfg(&numeric), Err("numeric-branch")); - let called = vec![ + assert!(reallocate(&numeric, &POOL).is_none()); + } + + // ================================================================ + // VCR-DEC-001 increment 3 — colouring ACROSS CALLS. + // ================================================================ + + /// A `push {r4-r8,lr}` / `pop {r4-r8,pc}`-framed body around one direct + /// call. The R4 value is born AFTER the call and dies before the return, so + /// whole-function liveness proves it never crosses the call boundary and it + /// may live in call-clobbered scratch — the recolouring increment 2 could + /// not even attempt, because the `bl` made the CFG builder decline the whole + /// function. + fn call_body() -> Vec { + vec![ + ins(ArmOp::Push { + regs: vec![Reg::R4, Reg::R5, Reg::R6, Reg::R7, Reg::R8, Reg::LR], + }), + ins(ArmOp::Bl { + label: "func_1".into(), + }), + ins(ArmOp::Movw { + rd: Reg::R4, + imm16: 7, + }), + ins(ArmOp::Add { + rd: Reg::R4, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R4), + }), + ins(ArmOp::Mov { + rd: Reg::R0, + op2: Operand2::Reg(Reg::R4), + }), + ins(ArmOp::Pop { + regs: vec![Reg::R4, Reg::R5, Reg::R6, Reg::R7, Reg::R8, Reg::PC], + }), + ] + } + + /// THE POINT OF INCREMENT 3. A function containing a call must be COLOURED, + /// not declined — and the value that provably never crosses the call must + /// leave its callee-saved register. A `None` here means the call model + /// regressed to increment 2's reach. + #[test] + fn colours_across_a_call() { + let body = call_body(); + let out = reallocate(&body, &POOL).expect("a call-containing function must colour"); + assert_eq!(out.len(), body.len()); + assert_ne!(out, body, "an identity rewrite gates nothing"); + // The post-call temporary moved OFF the callee-saved register... + assert!( + !matches!(out[2].op, ArmOp::Movw { rd: Reg::R4, .. }), + "the post-call temporary should have left R4: {:?}", + out[2].op + ); + // ...and onto a register the call boundary proves is free THERE (it is + // defined after the call and dead before the return, so R2/R3 — dead-out + // at a `pop {…,pc}` — are legal; R0/R1 are not, they are live). + let landed = match &out[2].op { + ArmOp::Movw { rd, .. } => *rd, + other => panic!("shape changed: {other:?}"), + }; + assert!( + matches!(landed, Reg::R2 | Reg::R3), + "expected the temporary in call-clobbered scratch, got {landed:?}" + ); + // The CALL is emitted verbatim and the architectural register lists are + // identity-pinned. + assert_eq!(out[1].op, body[1].op, "the call was rewritten"); + assert_eq!(out[0].op, body[0].op, "prologue push list recoloured"); + assert_eq!(out[5].op, body[5].op, "epilogue pop list recoloured"); + // And the rewrite is certified by the CFG-lifted oracle. + let blocks = joins::build_cfg(&body).expect("CFG"); + assert_eq!(validate_cfg_rewrite(&body, &out, &blocks), Ok(())); + } + + /// **RED-FIRST for the shared AAPCS contract — the hazard this increment was + /// briefed on.** A rewrite that moves a value LIVE ACROSS a call into a + /// call-clobbered register is a miscompile: the callee is contractually free + /// to destroy R0-R3/R12/LR, so the value read after the call is garbage. + /// + /// Before increment 3 `validate_cfg_rewrite` treated a `bl` as EFFECT-FREE + /// (a non-straight-line op was required to be identical and then given no + /// effect), so the equation `(R4, R2)` demanded after the call sailed + /// straight through it and was discharged by the `mov` above — the validator + /// would have ACCEPTED this exact rewrite. The MUTATION that proves the + /// rejection comes from the CALL MODEL and nothing else is in this same + /// test: the identical rename over the identical instructions with the `bl` + /// REMOVED is a legal re-colouring and must be ACCEPTED. + #[test] + fn cfg_validator_rejects_a_live_value_recoloured_across_a_call() { + // BOTH R4 and R5 are saved by the prologue, so a R4->R5 re-home is a + // legal choice for the allocator (an unsaved callee-saved register would + // be rejected for a DIFFERENT reason — clobbering the caller's value — + // and would muddy what this test attributes to the call). + let frame = |mid: Vec| { + let mut v = vec![ins(ArmOp::Push { + regs: vec![Reg::R4, Reg::R5, Reg::LR], + })]; + v.extend(mid); + v.push(ins(ArmOp::Pop { + regs: vec![Reg::R4, Reg::R5, Reg::PC], + })); + v + }; + // save an argument in R4 / call / consume the saved value after the call + let with_call = |home: Reg| { + frame(vec![ + ins(ArmOp::Mov { + rd: home, + op2: Operand2::Reg(Reg::R0), + }), + ins(ArmOp::Bl { + label: "func_1".into(), + }), + ins(ArmOp::Add { + rd: Reg::R0, + rn: Reg::R0, + op2: Operand2::Reg(home), + }), + ]) + }; + let orig = with_call(Reg::R4); + let blocks = joins::build_cfg(&orig).expect("a call-containing CFG is now built"); + // Non-vacuity: the identity rewrite is accepted. + assert_eq!(validate_cfg_rewrite(&orig, &orig, &blocks), Ok(())); + // A callee-saved -> callee-saved move across the call is legal. + assert_eq!( + validate_cfg_rewrite(&orig, &with_call(Reg::R5), &blocks), + Ok(()), + "R5 is callee-saved: the callee must preserve it, so this rename is legal" + ); + // THE RED: R2 is call-clobbered. The value does not survive the call. + assert!( + matches!( + validate_cfg_rewrite(&orig, &with_call(Reg::R2), &blocks), + Err(RewriteViolation::DefClobbersEquation { .. }) + ), + "a value live ACROSS a call must not be recoloured into call-clobbered \ + scratch, got {:?}", + validate_cfg_rewrite(&orig, &with_call(Reg::R2), &blocks) + ); + + // ---- The mutation that proves the CALL MODEL is doing the work ------- + // Same instructions, same rename, `bl` DELETED. Now nothing clobbers R2 + // between the definition and the use, so the rewrite is a legal + // re-colouring and MUST be accepted. A validator that rejected here would + // be rejecting for some unrelated reason and the RED above would prove + // nothing about calls. + let no_call = |home: Reg| { + frame(vec![ + ins(ArmOp::Mov { + rd: home, + op2: Operand2::Reg(Reg::R0), + }), + ins(ArmOp::Add { + rd: Reg::R0, + rn: Reg::R0, + op2: Operand2::Reg(home), + }), + ]) + }; + let orig_nc = no_call(Reg::R4); + let blocks_nc = joins::build_cfg(&orig_nc).expect("CFG"); + assert_eq!( + validate_cfg_rewrite(&orig_nc, &no_call(Reg::R2), &blocks_nc), + Ok(()), + "without the call the SAME rename is legal — so the rejection above \ + is attributable to the call model, not to anything else" + ); + } + + /// The other half of the AAPCS contract: a call READS its argument + /// registers. A rewrite that renames the definition feeding an argument + /// leaves the callee reading a stale register, and must be rejected — even + /// though the `bl` itself is byte-identical on both sides. + #[test] + fn cfg_validator_rejects_a_renamed_call_argument() { + let orig = vec![ + ins(ArmOp::Movw { + rd: Reg::R0, + imm16: 5, + }), ins(ArmOp::Bl { label: "func_1".into(), }), ins(ArmOp::Bx { rm: Reg::LR }), ]; - assert_eq!(joins::build_cfg(&called), Err("call")); - assert!(reallocate(&numeric, &POOL).is_none()); - assert!(reallocate(&called, &POOL).is_none()); + let blocks = joins::build_cfg(&orig).expect("CFG"); + assert_eq!(validate_cfg_rewrite(&orig, &orig, &blocks), Ok(())); + let mut bad = orig.clone(); + bad[0] = ins(ArmOp::Movw { + rd: Reg::R3, + imm16: 5, + }); + assert!( + validate_cfg_rewrite(&orig, &bad, &blocks).is_err(), + "staging the argument in R3 while the callee reads R0 must be rejected" + ); + } + + /// The pass never proposes what the previous test rejects: a value live + /// across the call keeps a callee-saved home, because the call's + /// identity-pinned `{R0..R3, R12, LR}` def webs interfere with everything + /// live after it. + #[test] + fn a_value_live_across_a_call_stays_callee_saved() { + let body = vec![ + ins(ArmOp::Push { + regs: vec![Reg::R4, Reg::LR], + }), + ins(ArmOp::Mov { + rd: Reg::R4, + op2: Operand2::Reg(Reg::R0), + }), + ins(ArmOp::Bl { + label: "func_1".into(), + }), + ins(ArmOp::Add { + rd: Reg::R0, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R4), + }), + ins(ArmOp::Pop { + regs: vec![Reg::R4, Reg::PC], + }), + ]; + // Either the pass declines (identity colouring) or it rewrites — but in + // NO case may the cross-call value land in call-clobbered scratch. + if let Some(out) = reallocate(&body, &POOL) { + let home = match &out[1].op { + ArmOp::Mov { rd, .. } => *rd, + other => panic!("shape changed: {other:?}"), + }; + assert!( + matches!(home, Reg::R4 | Reg::R5 | Reg::R6 | Reg::R7 | Reg::R8), + "a value live across a call must stay callee-saved, got {home:?}" + ); + assert_eq!(out[2].op, body[2].op, "the call was rewritten"); + } + } + + /// The HIGH-LEVEL call pseudo-ops stay out of scope: they carry a result / + /// table-index register and are EXPANDED downstream (bounds guard, table + /// load, result move), so the register footprint this pass would colour is + /// not the one that ships. Declined, with the reason named. + #[test] + fn declines_the_high_level_call_pseudo_ops() { + for (op, why) in [ + ( + ArmOp::Call { + rd: Reg::R0, + func_idx: 1, + }, + "call-pseudo", + ), + ( + ArmOp::CallIndirect { + rd: Reg::R0, + type_idx: 0, + table_index_reg: Reg::R1, + table_size: 4, + table_byte_offset: 0, + null_check: false, + type_check: None, + }, + "call-indirect-pseudo", + ), + ] { + let body = vec![ins(op), ins(ArmOp::Bx { rm: Reg::LR })]; + assert_eq!(joins::build_cfg(&body), Err(why)); + assert!(reallocate(&body, &POOL).is_none()); + } } } diff --git a/crates/synth-synthesis/src/liveness.rs b/crates/synth-synthesis/src/liveness.rs index 4a7a07a8..1652d738 100644 --- a/crates/synth-synthesis/src/liveness.rs +++ b/crates/synth-synthesis/src/liveness.rs @@ -3495,6 +3495,79 @@ pub fn cfg_exit_observable(terminator: &ArmOp) -> BTreeSet { .collect() } +/// VCR-DEC-001 **increment 3** — the AAPCS register contract of a CALL, as a +/// [`RegEffect`]. `None` for every op that is not a real machine call. +/// +/// **One definition, two consumers — deliberately.** The lane brief for this +/// increment named its own hazard: *"a validator that treats `bl` as effect-free +/// would accept a non-identity equation across it"*. That is not hypothetical — +/// it is what [`validate_cfg_rewrite`] did before increment 3, because a call is +/// not [`is_straight_line`] and non-straight-line ops were required to be +/// identical and then given NO effect. An equation `(R4, R2)` demanded after a +/// `bl` would sail straight through the call to the code above it, certifying a +/// rewrite that parks a live value in a register the callee is contractually +/// free to destroy. So the contract is stated ONCE, here, and consumed by BOTH +/// the pass ([`crate::graph_alloc`]'s liveness/interference/pins) and the oracle +/// ([`validate_cfg_rewrite`]'s backward transfer). Two hand-maintained copies +/// would be the VCR-ORACLE mirror-pinning failure mode; one shared definition +/// plus an EXECUTION differential (which is the only thing that can catch an +/// error in what pass and validator share — the #872 lesson) is the honest +/// layering. +/// +/// **The contract (AAPCS, core registers).** +/// * `defs` = `{R0, R1, R2, R3, R12, LR}` — the call-clobbered set. The callee +/// may write all of them; R0/R1 additionally carry the return value and LR the +/// return address. Modeling them as DEFS is what makes a web live across the +/// call interfere with them, so the colourer can never home a live value in +/// caller-saved scratch — and what lets the validator DISCHARGE an identity +/// equation `(r, r)` at the call (both sides call the same callee with the +/// same arguments, so both get the same junk) while REJECTING a non-identity +/// one. +/// * `uses` = `{R0, R1, R2, R3}` (plus the target register of a `Blx`) — the +/// argument registers. CONSERVATIVE: this pass cannot see the callee's +/// signature, so every core argument register is assumed read. The cost is +/// reach (an unused argument register stays live from its last definition to +/// the call and blocks that colour); the alternative — guessing an arity — +/// would silently corrupt a call whose argument we then recoloured. +/// +/// **Not `reg_effect`.** Deliberately a SEPARATE function: `reg_effect` +/// returning `None` on a call is load-bearing for the shipping pipeline +/// (`body_uses_callee_saved`'s fail-safe prologue, `eliminate_unread_frame_stores`, +/// `shrink_callee_saved_saves`' decline, [`validate_final_allocation`]'s +/// invariant 1 all treat `None` as "may do anything"). Widening `reg_effect` +/// would move the shipped bytes; this addition is inert until a caller asks for +/// it. +pub fn call_effect(op: &ArmOp) -> Option { + use Reg::*; + /// AAPCS core call-clobbered ("caller-saved") registers. + const CLOBBERED: [Reg; 6] = [R0, R1, R2, R3, R12, LR]; + /// AAPCS core argument registers — conservatively ALL read at a call. + const ARGS: [Reg; 4] = [R0, R1, R2, R3]; + match op { + ArmOp::Bl { .. } => Some(RegEffect { + defs: CLOBBERED.to_vec(), + uses: ARGS.to_vec(), + }), + // An indirect call additionally READS its target register. + ArmOp::Blx { rm } => { + let mut uses = ARGS.to_vec(); + if !uses.contains(rm) { + uses.push(*rm); + } + Some(RegEffect { + defs: CLOBBERED.to_vec(), + uses, + }) + } + // `Call` / `CallIndirect` are HIGH-LEVEL pseudo-ops carrying a result + // register and (for the indirect form) a table-index register; they are + // EXPANDED downstream into a bounds guard + table load + `blx` + result + // move, so the register footprint of the final code is not this stream's. + // Not modeled — callers decline. + _ => None, + } +} + /// VCR-DEC-001 increment 2 — the CFG-lifted translation validator: prove a /// renames-only rewrite of a WHOLE branchy function preserves its dataflow /// **across control-flow joins**. @@ -3587,7 +3660,21 @@ pub fn validate_cfg_rewrite( if o.op != r.op { return Err(RewriteViolation::ShapeMismatch { index: i }); } - effects.push(None); + // INCREMENT 3 (#242): a CALL is NOT effect-free. Both sides are the + // identical op here (checked just above — a register allocator never + // rewrites a call's architectural operands), so the pair is the same + // [`call_effect`] twice, and the backward transfer below then: + // * DISCHARGES an identity equation `(r, r)` on a clobbered + // register (both sides call the same callee with the same + // arguments, so both hold the same value after it); + // * REJECTS a non-identity equation touching one + // (`DefClobbersEquation`) — the "a live value was recoloured into + // caller-saved scratch across a call" miscompile; + // * GENERATES identity equations for the argument registers, so a + // rewrite that renames what feeds an argument is rejected too. + // Non-call control flow (`Label`/`B`/`Bcc`/`Bx`) keeps `None`: it is + // byte-identical on both sides and carries no register effect. + effects.push(call_effect(&o.op).map(|e| (e.clone(), e))); continue; } let (Some(eo), Some(er)) = (reg_effect(&o.op), reg_effect(&r.op)) else { From a5d00d94ab8e7a96b3c4a4e4dd3a77189f088c13 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 14:46:14 +0200 Subject: [PATCH 2/3] VCR-DEC-001 increment 3: EXECUTION-gate the call shapes + CI-wire the floor (#242) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The AAPCS call contract is SHARED by the pass and `validate_cfg_rewrite` on purpose (two hand-maintained copies would be the VCR-ORACLE mirror-pinning failure mode) — which means neither validator can catch an error IN the contract itself. Only execution can. So the join execution differential grows a CALL population covering both halves of the contract: CLOBBER half — a value live ACROSS a `bl` must not be homed in caller-saved scratch: local_promote_cross_call::cross_call and intra_module_callee_saved::a (both written precisely so a caller-saved home is observably wrong), plus stack_canary_687::recurse (self-recursion: every activation re-enters the same allocation). ARGUMENT half — the registers a call READS must still hold what the callee expects: call_5args::caller and call_6_7args::call6/call7, whose callees pack each argument into its own nibble, so ANY dropped/shifted/mis-assigned argument changes the result. Harness changes: * AAPCS argument passing: 0-3 in R0-R3 (was R0-R2), 4+ on an 8-byte-aligned stack with the fifth at [sp,#0]. Without this the 5/6/7-arg fixtures would look like miscompiles. * `contains_call()` verifies a case's `is_call_shape` DECLARATION against the emitted Thumb bytes (bl imm / blx reg). A fixture whose call got inlined away can no longer inflate the increment-3 population while testing nothing. * Its own non-vacuity FLOOR: <4 divergent call-containing functions FAILS, and the machine-readable summary line carries CALLSHAPES= so the CI awk pins the same floor (#890 — exit 0 alone is never trusted). Result: 56/56 checks, 19 engaged functions of which 6 are call shapes. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 56 ++++--- ...c_001_join_alloc_execution_differential.py | 137 ++++++++++++++---- 2 files changed, 147 insertions(+), 46 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 388a00b5..322b00aa 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -862,31 +862,45 @@ jobs: # ONLY (no unicorn/wasmtime). - name: Run VCR-DEC-001 graph-alloc spike differential (#242, thumb2) run: python scripts/repro/vcr_dec_001_graph_alloc_differential.py ./target/debug/synth - # VCR-DEC-001 increment 2 (#242): EXECUTION-gate the DIVERGENT bytes the - # join-aware colouring now produces. This is NOT redundant with the byte - # differential above: increment 1's correctness followed transitively from - # byte identity, and increment 2 broke that. `validate_cfg_rewrite` — the - # pass's own CFG-lifted trace-equality oracle — SHARES the CFG shape with - # the pass it validates, and #872 is the standing lesson that a validator - # can share its pass's blind spot, so the new bytes get EXECUTED: unicorn - # runs the flag-ON image and compares return value + linear-memory window - # against wasmtime, over every join shape the allocator reaches (real - # if/else, if-without-else, desugared block+br_if, early return, counted - # and data-dependent loops, two-level br_if). PROVEN non-vacuous by - # MUTATION: emptying `cfg_exit_observable` (the exit contract the pass and - # its validator SHARE) while removing the churn bias that masks it emits - # code leaving the return value in the wrong register — validate_cfg_rewrite - # AND VCR-RA-003 both ACCEPT it and only this gate catches it (16 wrong - # results). The grep asserts the NON-ZERO check count AND a non-zero - # engaged-function count from the machine-readable summary: exit 0 alone is - # not trusted, and a run where the allocator stopped changing bytes would - # pass every comparison while gating nothing. - - name: Run VCR-DEC-001 join-allocator execution differential (#242, thumb2) + # VCR-DEC-001 increments 2+3 (#242): EXECUTION-gate the DIVERGENT bytes the + # join- and call-aware colouring now produces. This is NOT redundant with + # the byte differential above: increment 1's correctness followed + # transitively from byte identity, and increment 2 broke that. + # `validate_cfg_rewrite` — the pass's own CFG-lifted trace-equality oracle + # — SHARES the CFG shape with the pass it validates, and #872 is the + # standing lesson that a validator can share its pass's blind spot, so the + # new bytes get EXECUTED: unicorn runs the flag-ON image and compares + # return value + linear-memory window against wasmtime, over every join + # shape the allocator reaches (real if/else, if-without-else, desugared + # block+br_if, early return, counted and data-dependent loops, two-level + # br_if). PROVEN non-vacuous by MUTATION: emptying `cfg_exit_observable` + # (the exit contract the pass and its validator SHARE) while removing the + # churn bias that masks it emits code leaving the return value in the wrong + # register — validate_cfg_rewrite AND VCR-RA-003 both ACCEPT it and only + # this gate catches it (16 wrong results). + # + # Increment 3 (v0.54) adds the CALL shapes and the same argument applies + # with MORE force: the AAPCS contract (`liveness::call_effect`) is SHARED + # by the pass and the validator on purpose (two hand-maintained copies + # would be the VCR-ORACLE mirror-pinning failure mode), so neither can + # catch an error IN the contract. Both halves are executed — the CLOBBER + # half (a value live across a `bl`, incl. self-recursion) and the ARGUMENT + # half (5/6/7-argument callees that pack each argument into its own nibble, + # register AND stack). Likewise proven non-vacuous by MUTATION: emptying + # `call_effect`'s clobber set makes the colourer home a cross-call value in + # R0-R3; `validate_cfg_rewrite` accepts it and only this gate fails it. + # + # The grep asserts the NON-ZERO check count, a non-zero engaged-function + # count AND the ≥4 engaged CALL-shape floor from the machine-readable + # summary: exit 0 alone is not trusted, and a run where the allocator + # stopped reaching call-containing functions would pass every comparison + # while leaving the whole increment-3 class ungated. + - name: Run VCR-DEC-001 join+call allocator execution differential (#242, thumb2) run: | set -o pipefail SYNTH=./target/debug/synth python scripts/repro/vcr_dec_001_join_alloc_execution_differential.py | tee ga_join.out grep -q "^VCR-DEC-001-JOIN CHECKS=" ga_join.out - awk -F'[=/ ]' '/^VCR-DEC-001-JOIN/ { if ($3+0 > 0 && $3 == $4 && $6+0 > 0) ok = 1 } END { exit ok ? 0 : 1 }' ga_join.out + awk -F'[=/ ]' '/^VCR-DEC-001-JOIN/ { if ($3+0 > 0 && $3 == $4 && $6+0 > 0 && $8+0 >= 4) ok = 1 } END { exit ok ? 0 : 1 }' ga_join.out # #798/#879: the RV32 active-data-segment FULL-BOOT oracle — found # un-wired in the same #879 audit as the gpio gate. clang+lld build a # bare-metal riscv32 firmware from synth's object + generated startup/ diff --git a/scripts/repro/vcr_dec_001_join_alloc_execution_differential.py b/scripts/repro/vcr_dec_001_join_alloc_execution_differential.py index 00be98d0..8bc1ab6a 100644 --- a/scripts/repro/vcr_dec_001_join_alloc_execution_differential.py +++ b/scripts/repro/vcr_dec_001_join_alloc_execution_differential.py @@ -1,6 +1,6 @@ #!/usr/bin/env python3 -"""VCR-DEC-001 increment 2 — EXECUTION differential for the join-aware -graph-colouring allocator (`SYNTH_GRAPH_ALLOC=1`, epic #242). +"""VCR-DEC-001 increments 2+3 — EXECUTION differential for the join- and +call-aware graph-colouring allocator (`SYNTH_GRAPH_ALLOC=1`, epic #242). **Why this exists.** Increment 1 (v0.50) could claim execution correctness TRANSITIVELY: on a whole straight-line function the spike and the shipping @@ -13,13 +13,28 @@ with the pass it validates (#872 is the standing lesson that a validator can share its pass's blind spot). So the new bytes get executed. +**Increment 3 (v0.54) makes that argument SHARPER, not weaker.** Colouring +across CALLS is driven by one shared AAPCS contract (`liveness::call_effect`), +consumed by the pass AND by `validate_cfg_rewrite`. Sharing is deliberate — two +hand-maintained copies would be the VCR-ORACLE mirror-pinning failure mode — but +it means NEITHER validator can catch an error IN the contract itself. Only +execution can. So the CALL SHAPES are gated here as their own population, with +their own non-vacuity floor: a run in which no call-containing function diverges +FAILS, because the increment-3 reach would then be gating nothing (#890). + What is gated, per fixture function: (E) ENGAGEMENT — the allocator must APPLY, and the flag-on `.text` must actually DIFFER from flag-off. Without both, the harness would be re-testing the shipping compiler and would pass vacuously; it FAILS - instead. + instead. A case DECLARED to be a call shape must additionally CONTAIN a + Thumb `bl`/`blx` in its emitted body — self-declaration verified against + bytes, so a fixture that stops containing a call (inlined away, shape + changed) fails loudly instead of silently degrading the population. (1) EXECUTION — unicorn runs the flag-ON image and its return value AND the compared linear-memory window must equal wasmtime's on every input. + Arguments follow AAPCS: 0-3 in R0-R3, 4+ on the stack (8-byte aligned), + which is what makes the 5/6/7-argument call fixtures test the argument + half of the contract and not just the clobber half. (2) VCR-RA-003 — `validate_final_allocation` must return Consistent for every applied function (observed via SYNTH_RA003_VERBOSE, not inferred from the exit code), and no violation may be reported. @@ -45,6 +60,7 @@ UC_ARM_REG_R0, UC_ARM_REG_R1, UC_ARM_REG_R2, + UC_ARM_REG_R3, UC_ARM_REG_R9, UC_ARM_REG_R10, UC_ARM_REG_R11, @@ -59,32 +75,52 @@ CODE = 0x0 SP_INIT = LIN + 0x2_0000 MEM_WINDOW = 0x100 -ARG_REGS = [UC_ARM_REG_R0, UC_ARM_REG_R1, UC_ARM_REG_R2] +# AAPCS core argument registers; arguments past the fourth go on the stack. +ARG_REGS = [UC_ARM_REG_R0, UC_ARM_REG_R1, UC_ARM_REG_R2, UC_ARM_REG_R3] -# (fixture, function, [arg tuples]). Chosen to cover every join shape the -# allocator now colours: real if/else, if-without-else, the desugared +# (fixture, function, [arg tuples], is_call_shape). +# +# JOIN shapes (increment 2): real if/else, if-without-else, the desugared # block+br_if form, an early (non-tail) return, counted and data-dependent # loops, and the two-level `br_if` exit — with inputs that take BOTH sides of # every branch (a one-sided input set would never execute the arm whose # register the colourer moved). +# +# CALL shapes (increment 3, `is_call_shape=True`): the AAPCS contract has two +# halves and both are covered. The CLOBBER half — a value live ACROSS a `bl` +# must not be homed in caller-saved scratch — is what `local_promote_cross_call` +# and `intra_module_callee_saved` were written for (their whole point is that a +# caller-saved home is observably wrong), plus a self-recursive `recurse` whose +# every activation re-enters the same allocation. The ARGUMENT half — the +# registers a call READS must still hold what the callee expects — is covered by +# the 5/6/7-argument fixtures, whose callees pack each argument into a distinct +# nibble, so ANY dropped, shifted or mis-assigned argument (register OR stack) +# changes the result. CASES = [ - ("cf_shapes_500.wat", "real_ifelse", [(0,), (1,), (7,)]), - ("cf_shapes_500.wat", "real_if", [(0,), (1,)]), - ("cf_shapes_500.wat", "br_func", [(0,), (1,)]), - ("cf_shapes_500.wat", "early_ret", [(0,), (1,)]), - ("provenance_branches_396.wat", "decide", [(0, 0), (5, 3), (3, 5), (100, 1)]), - ("aarch64_ctrlflow_851.wat", "count_sum", [(0,), (1,), (5,), (17,)]), - ("aarch64_ctrlflow_851.wat", "countdown", [(0,), (1,), (9,)]), + ("cf_shapes_500.wat", "real_ifelse", [(0,), (1,), (7,)], False), + ("cf_shapes_500.wat", "real_if", [(0,), (1,)], False), + ("cf_shapes_500.wat", "br_func", [(0,), (1,)], False), + ("cf_shapes_500.wat", "early_ret", [(0,), (1,)], False), + ("provenance_branches_396.wat", "decide", [(0, 0), (5, 3), (3, 5), (100, 1)], False), + ("aarch64_ctrlflow_851.wat", "count_sum", [(0,), (1,), (5,), (17,)], False), + ("aarch64_ctrlflow_851.wat", "countdown", [(0,), (1,), (9,)], False), # do_while_count(0) is deliberately absent: `n` starts at 0, so the # bottom-test loop runs 2**32 times before wrapping back to the exit. It # terminates in wasmtime (JIT) but not within any emulator instruction # budget, so it measures the budget, not the compiler. - ("aarch64_ctrlflow_851.wat", "do_while_count", [(1,), (6,), (23,)]), - ("loop_param_bound_663.wat", "sum_const", [(0, 0), (3, 4)]), - ("loop_param_bound_663.wat", "sum_below", [(0, 0), (1, 5), (4, 4), (2, 9)]), - ("if_else_result_343.wat", "pick", [(0,), (1,), (0xFFFFFFFF,)]), - ("if_else_result_343.wat", "pick2", [(0,), (1,)]), - ("brif_outer_740.wat", "poll", [(7, 0), (200, 0), (200, 1), (5, 3)]), + ("aarch64_ctrlflow_851.wat", "do_while_count", [(1,), (6,), (23,)], False), + ("loop_param_bound_663.wat", "sum_const", [(0, 0), (3, 4)], False), + ("loop_param_bound_663.wat", "sum_below", [(0, 0), (1, 5), (4, 4), (2, 9)], False), + ("if_else_result_343.wat", "pick", [(0,), (1,), (0xFFFFFFFF,)], False), + ("if_else_result_343.wat", "pick2", [(0,), (1,)], False), + ("brif_outer_740.wat", "poll", [(7, 0), (200, 0), (200, 1), (5, 3)], False), + # ---- increment 3: CALL shapes ------------------------------------------ + ("local_promote_cross_call.wat", "cross_call", [(0,), (5,), (100,), (0xFFFF,)], True), + ("intra_module_callee_saved.wat", "a", [(0,), (7,), (100,)], True), + ("stack_canary_687.wat", "recurse", [(0,), (1,), (5,), (12,)], True), + ("call_5args.wat", "caller", [(1, 2, 3, 4, 5), (0, 0, 0, 0, 9), (15, 1, 2, 4, 8)], True), + ("call_6_7args.wat", "call6", [(1, 2, 3, 4, 5, 6), (0, 0, 0, 0, 0, 7)], True), + ("call_6_7args.wat", "call7", [(1, 2, 3, 4, 5, 6, 7), (0, 0, 0, 0, 0, 0, 9)], True), ] CLEAR = [ @@ -145,6 +181,26 @@ def wasmtime_call(wat, func, args): return (None if r is None else r & 0xFFFFFFFF), window +def contains_call(body): + """True if the Thumb body contains a `bl ` or `blx `. + + Used to VERIFY a case's `is_call_shape` declaration against the emitted + bytes: a fixture whose call got inlined away (or whose shape drifted) would + otherwise keep inflating the increment-3 population while testing nothing. + bl : hw1 = 11110xxxxxxxxxxx, hw2 = 11x1xxxxxxxxxxx + blx : 010001111xxxx000 + """ + for i in range(0, len(body) - 1, 2): + hw = int.from_bytes(body[i:i + 2], "little") + if (hw & 0xFF87) == 0x4780: + return True + if (hw & 0xF800) == 0xF000 and i + 3 < len(body): + hw2 = int.from_bytes(body[i + 2:i + 4], "little") + if (hw2 & 0xD000) == 0xD000: + return True + return False + + def unicorn_call(text, lin_init, faddr, args): mu = Uc(UC_ARCH_ARM, UC_MODE_THUMB) mu.mem_map(CODE, 0x10000) @@ -155,7 +211,15 @@ def unicorn_call(text, lin_init, faddr, args): mu.reg_write(UC_ARM_REG_R9, LIN + LIN_SIZE) mu.reg_write(UC_ARM_REG_R10, LIN_SIZE) mu.reg_write(UC_ARM_REG_R11, LIN) - mu.reg_write(UC_ARM_REG_SP, SP_INIT) + # AAPCS: arguments 0-3 in R0-R3, 4+ on the stack with the FIFTH at [sp,#0] + # at the call boundary and SP 8-byte aligned. Getting this wrong would look + # exactly like a miscompile on the 5/6/7-argument fixtures, so it is done + # here rather than by pretending those functions take three arguments. + stack_args = [a & 0xFFFFFFFF for a in args[len(ARG_REGS):]] + sp = SP_INIT - ((len(stack_args) * 4 + 7) & ~7 if stack_args else 0) + for i, val in enumerate(stack_args): + mu.mem_write(sp + 4 * i, val.to_bytes(4, "little")) + mu.reg_write(UC_ARM_REG_SP, sp) ret = CODE + 0xFF00 mu.mem_write(ret, b"\x00\xbf\x00\xbf") mu.reg_write(UC_ARM_REG_LR, ret | 1) @@ -181,9 +245,10 @@ def main(): fails = 0 checks = 0 engaged_functions = 0 + engaged_call_functions = 0 by_fixture = {} - for wat, func, argsets in CASES: - by_fixture.setdefault(wat, []).append((func, argsets)) + for wat, func, argsets, is_call in CASES: + by_fixture.setdefault(wat, []).append((func, argsets, is_call)) for wat, entries in by_fixture.items(): off_elf = f"/tmp/ga_join_{Path(wat).stem}_off.elf" @@ -206,7 +271,7 @@ def main(): text_off, _, syms_off, sizes_off = load(off_elf) text_on, lin_init, syms_on, sizes_on = load(on_elf) - for func, argsets in entries: + for func, argsets, is_call in entries: if func not in syms_on: print(f"FAIL {wat}:{func} — symbol missing") fails += 1 @@ -222,7 +287,18 @@ def main(): f"it). Re-pick the fixture or fix the regression.") fails += 1 continue + # A declared CALL shape must really contain a call in the emitted + # body — self-declaration verified against the bytes, so an inlined + # -away call cannot silently inflate the increment-3 population. + if is_call and not contains_call(body_on): + print(f"FAIL {wat}:{func} — declared a CALL shape but the emitted " + f"body contains no bl/blx: it gates nothing about the AAPCS " + f"call contract.") + fails += 1 + continue engaged_functions += 1 + if is_call: + engaged_call_functions += 1 # ---- (1) EXECUTION ------------------------------------------- for args in argsets: @@ -246,16 +322,27 @@ def main(): # Non-vacuity: the whole harness is worthless if the allocator stopped # changing bytes anywhere. Require a real population. - print(f"\nengaged functions (flag-on bytes differ): {engaged_functions}") + print(f"\nengaged functions (flag-on bytes differ): {engaged_functions} " + f"(of which CALL shapes: {engaged_call_functions})") if engaged_functions < 10: print("VACUOUS: fewer than 10 functions have divergent flag-on bytes — " "the join allocator's reach regressed; this gate no longer gates.") fails += 1 + # Increment 3 gets its OWN floor. The AAPCS call contract is SHARED by the + # pass and `validate_cfg_rewrite`, so execution is the only thing that can + # catch an error in the contract itself — a run with no divergent + # call-containing function would leave that class entirely ungated while + # still reporting PASS (#890). + if engaged_call_functions < 4: + print("VACUOUS: fewer than 4 CALL-containing functions have divergent " + "flag-on bytes — increment 3's reach regressed and the AAPCS call " + "contract is no longer execution-gated.") + fails += 1 # Machine-readable summary the CI wiring greps for a NON-ZERO count: # exit 0 alone is not trusted (the "0 ops accepted PASS" lesson). print(f"VCR-DEC-001-JOIN CHECKS={checks - fails}/{checks} " - f"ENGAGED={engaged_functions}") + f"ENGAGED={engaged_functions} CALLSHAPES={engaged_call_functions}") print("RESULT:", "PASS" if not fails else f"FAIL ({fails} problem(s))") return 1 if fails else 0 From d2c2d7ac5f0da3c763b552a90f7970059330e8a9 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:03:35 +0200 Subject: [PATCH 3/3] VCR-DEC-001 increment 3: mutation matrix, sharpened argument test, CHANGELOG (#242) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit MUTATION MATRIX over the shared AAPCS contract (`liveness::call_effect`), run to find out what each half is actually buying: uses = [] KILLED by cfg_validator_rejects_a_renamed_call_argument (unit) and by the execution differential (5 wrong results: call6(1,2,3,4,5,6) -> 0x00651321 vs 0x00654321) once the churn bias is replaced by a churn-MAXIMISING one. Control: the churn-maximising bias ALONE, contract intact, gives 0 wrong results — so the failure is attributable to the contract, not to the bias. defs = [] SURVIVES. Documented, not papered over: with the conservative `uses` intact the two halves OVERLAP for the R0-R8 pool (a value live across a call must be defined above it, and the argument equation then collides with the rewritten definition). `defs`' independent duties today are the non-pool {R12,LR} and keeping the PASS from proposing colourings the oracle would only reject. The `call_effect` doc now warns that an arity-precise `uses` — the obvious next reach win — makes `defs` the SOLE soundness guard for R0-R3, so the two must be narrowed/tested together. both = [] (the pre-increment-3 effect-free `bl` — the briefed hazard) KILLED by three unit tests. `cfg_validator_rejects_a_renamed_call_argument` was sharpened after the matrix showed the original R0-staged/`bx lr` form was vacuous w.r.t. the call model: `bx lr`'s STRICT exit seed demanded R0 all by itself. It now stages R3 and renames to R2 inside a `pop {…,pc}` frame, where BOTH are dead-out per `cfg_exit_observable`, so only the argument use can reject it. Also: the measure script's docstring no longer claims the self-contained half "must be flat" (it is not, and was not in increment 2 either — 108 functions apply there now), and names the decline histogram as the actionable output that picks the next increment. Verification by REAL exit code: cargo fmt --check 0, clippy --workspace --all-targets -D warnings 0, cargo test --workspace 0 (frozen anchors 10/10), claim_check 34/34, byte differential 0, execution differential 0 (56/56, CALLSHAPES=6). Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CHANGELOG.md | 78 +++++++++++++++++++ crates/synth-synthesis/src/graph_alloc.rs | 50 ++++++++---- crates/synth-synthesis/src/liveness.rs | 17 ++++ .../repro/vcr_dec_001_join_alloc_measure.py | 28 ++++--- 4 files changed, 147 insertions(+), 26 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index bcd6fdcc..7198a91b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,84 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +### Added + +- **VCR-DEC-001 increment 3 (#242): the graph-colouring allocator colours ACROSS + CALLS.** Increment 2's second-largest decline bucket was `call` / + `call-indirect` — 68 of the measured corpus — because a `bl` had no modeled + effect and the join CFG builder refused the whole function. The AAPCS call + boundary is now modeled: `liveness::call_effect` states the contract ONCE + (`defs = {R0,R1,R2,R3,R12,LR}`, `uses = {R0..R3}` plus a `blx`'s target, + conservatively all four argument registers since the callee's signature is not + visible), and BOTH the pass (`graph_alloc::joins` — liveness, interference, + identity pins) and its acceptance oracle (`validate_cfg_rewrite`'s backward + transfer) consume that one definition. Modeling it in the pass alone would + have been the #872 defect verbatim: a validator that treats `bl` as + effect-free accepts a non-identity equation across it, i.e. it certifies its + own pass's *"live value parked in call-clobbered scratch"* miscompile — and + that is exactly what `validate_cfg_rewrite` did before this change. Calls are + emitted verbatim with both rename maps re-checked as the identity; + single-block functions containing a call are now taken too (increment 1 + structurally cannot, since a call is not `is_straight_line`). `reg_effect` is + deliberately NOT widened — its `None`-on-call is load-bearing for the shipping + pipeline (fail-safe prologue, `shrink_callee_saved_saves`' decline, VCR-RA-003 + invariant 1), so widening it would move shipped bytes. + + **Measured** (`scripts/repro/vcr_dec_001_join_alloc_measure.py`, ARM repro + corpus, ELF-symtab bytes + `--emit-wcet` sound bounds): + + | path | increment 2 | increment 3 | + |---|---|---| + | relocatable | −46 B (−0.11 %) / −25 cyc, 275 applied, 8 shrank / 1 grew | **−100 B (−0.24 %) / −33 cyc, 307 applied, 24 shrank / 5 grew** | + | self-contained | −70 B (−0.14 %) / −9 cyc, 81 applied, 10 shrank / 1 grew | **−120 B (−0.24 %) / −17 cyc, 108 applied, 27 shrank / 3 grew** | + + Zero WCET-bound regressions on either path (12 functions' bounds shrank, 0 + grew). Decline histogram: `call` 57 → **0** (taken); `call-indirect` 11 → 11 + (renamed `call-indirect-pseudo` — the high-level `Call`/`CallIndirect` + pseudo-ops are expanded downstream into a bounds guard + table load + result + move, so the register footprint here is not the one that ships, and they stay + declined by name). The residual buckets are `unmodeled-op` 174, `single-block` + 73, `identity-colouring` 31, `unreachable-block` 11, `call-indirect-pseudo` 11, + `numeric-branch` 10. + + Still **flag-off by default** (`SYNTH_GRAPH_ALLOC`): this is a measurement + spike, not a behaviour change. Frozen anchors byte-identical, 10/10. + + **Mutation evidence.** The AAPCS contract is shared by the pass and the + validator on purpose (two hand-maintained copies would be the VCR-ORACLE + mirror-pinning failure mode), so neither can catch an error *in* the contract — + only execution can. Emptying the ARGUMENT half (with the churn bias replaced by + a churn-maximising one, which otherwise masks it) makes the colourer re-home + argument staging and yields **5 wrong results** in + `vcr_dec_001_join_alloc_execution_differential.py` — `call6(1,2,3,4,5,6)` + returns `0x00651321` instead of `0x00654321` — while `validate_cfg_rewrite` + AND VCR-RA-003 both accept it; the churn-maximising bias *alone*, with the + contract intact, produces **0 wrong results**, so the failure is attributable + to the contract and nothing else. Emptying BOTH halves — the pre-increment-3 + effect-free `bl`, the briefed hazard — is killed by three unit tests. Emptying + the CLOBBER half alone is NOT caught, and that is documented on `call_effect` + rather than papered over: with the conservative `uses` intact the two halves + overlap for the R0-R8 pool, so `defs`' independent duties today are the + non-pool `{R12, LR}` and keeping the pass from proposing colourings the oracle + would reject. A future increment that makes the argument set arity-precise + makes `defs` the sole soundness guard for R0-R3 — narrow one and widen the + tests for the other in the same change. + +### Changed + +- `vcr_dec_001_join_alloc_execution_differential.py` gains an increment-3 CALL + population covering both halves of the contract: the CLOBBER half + (`local_promote_cross_call::cross_call`, `intra_module_callee_saved::a` — both + written so a caller-saved home is observably wrong — and the self-recursive + `stack_canary_687::recurse`) and the ARGUMENT half (`call_5args::caller`, + `call_6_7args::call6`/`call7`, whose callees pack each argument into its own + nibble). The harness now passes arguments per AAPCS (0-3 in R0-R3, 4+ on an + 8-byte-aligned stack), verifies each declared call shape really CONTAINS a + `bl`/`blx` in its emitted bytes, and enforces its own non-vacuity floor (≥4 + 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. + ## [0.53.0] - 2026-07-30 **"The last mile" — seven lanes.** falcon's VFP wall comes down, RISC-V compiles diff --git a/crates/synth-synthesis/src/graph_alloc.rs b/crates/synth-synthesis/src/graph_alloc.rs index 920bc86c..a62c6455 100644 --- a/crates/synth-synthesis/src/graph_alloc.rs +++ b/crates/synth-synthesis/src/graph_alloc.rs @@ -1900,28 +1900,44 @@ mod tests { /// registers. A rewrite that renames the definition feeding an argument /// leaves the callee reading a stale register, and must be rejected — even /// though the `bl` itself is byte-identical on both sides. + /// + /// The shape is chosen so the ARGUMENT USE is the ONLY thing that can + /// reject it: the staged register is R3 and the rewrite moves it to R2, and + /// BOTH are dead-out at a `pop {…, pc}` return + /// ([`crate::liveness::cfg_exit_observable`] exempts `{R2, R3, R12, LR}` + /// there). So the exit contract demands nothing about either, and the + /// rejection is attributable to `call_effect`'s `uses` alone — emptying them + /// turns this test green, which is how it is known not to be re-testing the + /// exit contract by accident (measured: with `uses` intact but the whole + /// call effect emptied, the R0-staged form this replaced still passed, + /// because `bx lr`'s STRICT exit seed demanded R0 all by itself). #[test] fn cfg_validator_rejects_a_renamed_call_argument() { - let orig = vec![ - ins(ArmOp::Movw { - rd: Reg::R0, - imm16: 5, - }), - ins(ArmOp::Bl { - label: "func_1".into(), - }), - ins(ArmOp::Bx { rm: Reg::LR }), - ]; + let staged = |arg: Reg| { + vec![ + ins(ArmOp::Push { + regs: vec![Reg::R4, Reg::LR], + }), + ins(ArmOp::Movw { rd: arg, imm16: 5 }), + ins(ArmOp::Bl { + label: "func_1".into(), + }), + ins(ArmOp::Pop { + regs: vec![Reg::R4, Reg::PC], + }), + ] + }; + let orig = staged(Reg::R3); let blocks = joins::build_cfg(&orig).expect("CFG"); assert_eq!(validate_cfg_rewrite(&orig, &orig, &blocks), Ok(())); - let mut bad = orig.clone(); - bad[0] = ins(ArmOp::Movw { - rd: Reg::R3, - imm16: 5, - }); assert!( - validate_cfg_rewrite(&orig, &bad, &blocks).is_err(), - "staging the argument in R3 while the callee reads R0 must be rejected" + matches!( + validate_cfg_rewrite(&orig, &staged(Reg::R2), &blocks), + Err(RewriteViolation::DefClobbersEquation { .. }) + ), + "staging the argument in R2 while the callee reads R3 must be rejected, \ + got {:?}", + validate_cfg_rewrite(&orig, &staged(Reg::R2), &blocks) ); } diff --git a/crates/synth-synthesis/src/liveness.rs b/crates/synth-synthesis/src/liveness.rs index 1652d738..0f6e67c8 100644 --- a/crates/synth-synthesis/src/liveness.rs +++ b/crates/synth-synthesis/src/liveness.rs @@ -3530,6 +3530,23 @@ pub fn cfg_exit_observable(terminator: &ArmOp) -> BTreeSet { /// the call and blocks that colour); the alternative — guessing an arity — /// would silently corrupt a call whose argument we then recoloured. /// +/// **Measured overlap — read before narrowing either half.** A mutation matrix +/// over the increment-3 unit suite found that emptying `defs` ALONE is not +/// caught: with the conservative `uses` intact, a pool value recoloured across a +/// call is already rejected by the ARGUMENT equation (the value must be defined +/// ABOVE the call to be live across it, and the `(r, r)` equation the call's use +/// generates then collides with the rewritten definition). So for the R0-R8 pool +/// the two halves currently OVERLAP, and `defs`' independent duties are (a) the +/// NON-pool `{R12, LR}`, and (b) keeping the PASS from proposing colourings the +/// oracle would only reject — reach, not soundness. **That changes the moment +/// `uses` is narrowed.** A future increment that makes the argument set precise +/// (per-callee arity, the obvious reach win — an unused argument register +/// currently stays live all the way back from the call and blocks that colour) +/// makes `defs` the SOLE soundness guard for R0-R3. Narrow `uses` and widen the +/// tests for `defs` in the same change, or the guard silently becomes the only +/// one and nothing is testing it. Emptying BOTH — i.e. the pre-increment-3 +/// effect-free `bl`, the briefed hazard — is caught by three tests. +/// /// **Not `reg_effect`.** Deliberately a SEPARATE function: `reg_effect` /// returning `None` on a call is load-bearing for the shipping pipeline /// (`body_uses_callee_saved`'s fail-safe prologue, `eliminate_unread_frame_stores`, diff --git a/scripts/repro/vcr_dec_001_join_alloc_measure.py b/scripts/repro/vcr_dec_001_join_alloc_measure.py index 86e582e1..3c5589ff 100644 --- a/scripts/repro/vcr_dec_001_join_alloc_measure.py +++ b/scripts/repro/vcr_dec_001_join_alloc_measure.py @@ -1,6 +1,7 @@ #!/usr/bin/env python3 -"""VCR-DEC-001 increment 2 — MEASURE the join-aware graph-colouring allocator -against the shipping greedy/segment allocator (epic #242, the North Star). +"""VCR-DEC-001 increments 2+3 — MEASURE the join- and call-aware graph-colouring +allocator against the shipping greedy/segment allocator (epic #242, the North +Star). This is the lane's DELIVERABLE, not a gate: a widened allocator with no comparative numbers says nothing about whether to flip it. For every function @@ -16,11 +17,19 @@ assumptions, not a hardware measurement. Functions whose bound DECLINES on either side are excluded from the cycle total and counted separately. -Both `--relocatable` (label-form branches — increment 2's scope) and the -default self-contained path (pre-resolved NUMERIC branches — out of scope, so -the allocator declines and the numbers must be flat) are measured, because the -flat half is itself evidence: it bounds how much of the corpus the increment -can reach today. +Both paths are measured, because the DIFFERENCE between them bounds how much of +the corpus each increment reaches: + * `--relocatable` — label-form branches, fully in scope; + * the default self-contained path — branches are PRE-RESOLVED to numeric + offsets, which the allocator still declines (`numeric-branch`), so only its + call-form and branch-free functions are reachable there. Increment 3 moved + this half from "mostly flat" to real: calls stay label-form on BOTH paths, + so modeling them reaches functions the numeric-branch decline had hidden. + +The per-run DECLINE HISTOGRAM is the actionable half of the output: each reason +names a construct the allocator refuses, and the largest bucket is the next +increment's target (that is how increment 3 was chosen — `call` + `call-indirect` +were 68 of increment 2's declines). Usage: python3 vcr_dec_001_join_alloc_measure.py [--json OUT] Exit 0 always unless a compile fails — this MEASURES, it does not judge. @@ -214,8 +223,9 @@ def main(): out_json = sys.argv[sys.argv.index("--json") + 1] summary = {} - for tag, reloc in (("relocatable / label-form branches (increment-2 scope)", True), - ("self-contained / pre-resolved numeric branches (out of scope)", False)): + for tag, reloc in (("relocatable / label-form branches (fully in scope)", True), + ("self-contained / pre-resolved numeric branches " + "(branches out of scope; calls in scope)", False)): rows, applied, declines, errors = measure(synth, reloc) summary["relocatable" if reloc else "self_contained"] = report( tag, rows, applied, declines, errors)