From fef4b6fcd41f299dcccd1ce6e71fa4e7b824654a Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 16:17:19 +0200 Subject: [PATCH 1/5] =?UTF-8?q?feat(#242):=20VCR-RA-003=20phase=202=20?= =?UTF-8?q?=E2=80=94=20across-CALL=20+=20across-JOIN=20allocation=20valida?= =?UTF-8?q?tion?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extend the unconditional per-compilation register-allocation validator past straight-line to WHOLE-FUNCTION control flow: - Invariant 3 (across-CALL): a caller-saved reg R2/R3/R12 live across a bl/blx/call (defined before, read after, no intervening redef) is flagged — the AAPCS boundary destroys it. Anchored on the ABI contract at the call, not inferred value-identity (the v0.48 vacuity lesson). R0/R1 excluded (return value). Does NOT touch the shared reg_effect (whose None-on-call meaning the phase-1 fail-safe depends on). - Invariant 4 (across-JOIN): a reg live-in to a CF join (>=2 preds) must be available (must-defined on every incoming path, or an entry live-in). Forward MUST/intersection availability fixpoint (UNIVERSE-init, not empty) over a dedicated join CFG that admits bx-lr returns (sink) and calls (fall-through with a caller-saved def-set). Entry seed = R0-R3, SP, LR, and the RESERVED regs R9/R10/R11/R12 (linmem base etc. — resident by construction). - RaFinalVerdict gains NotAttempted { reason } (loud honest decline when the join CFG can't be built: numeric branch, BrTable, computed Bx, dup label). NON-FATAL at the arm_backend call site; only Violation hard-errors. Vacuity-in-practice verified: invariant 4 fires on real branchy codegen (if_else_result_343, cf_shapes_500, block_brif_483 joins all Consistent). Caught + fixed a real false positive (block_brif nested: R11 linmem base defined nowhere in-stream) by seeding the reserved regs. 130-fixture sweep: 0 false positives. Frozen 10/10 byte-identical. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend/src/arm_backend.rs | 62 ++- crates/synth-synthesis/src/liveness.rs | 562 +++++++++++++++++++++++- 2 files changed, 593 insertions(+), 31 deletions(-) diff --git a/crates/synth-backend/src/arm_backend.rs b/crates/synth-backend/src/arm_backend.rs index 095a28e3..a954c39f 100644 --- a/crates/synth-backend/src/arm_backend.rs +++ b/crates/synth-backend/src/arm_backend.rs @@ -1360,28 +1360,46 @@ fn compile_wasm_to_arm( // VCR-RA-003 (epic #242): UNCONDITIONAL per-compilation register-allocation // validation. The register allocator is the last major unverified codegen - // component; this single-stream backward-dataflow checker proves — by - // construction, on the EXACT emitted stream about to be encoded — that the - // allocation preserves the two invariants whose reference lives in the - // stream: callee-saved preservation (#490) and spill-slot non-aliasing - // (#331). It runs on every ARM compile in the DEFAULT shipping build (NOT - // behind `--features verify`; a verify-gated check would be dormant in - // exactly the build that ships — the #757 / VCR-VER-003 lesson) and - // hard-errors the compile on a violation. Branches / CF joins and unmodeled - // ops (calls, i64-pair, FP) are the named PHASE-2 boundary: the spill check - // segments at them (never reasoning across a join), so this is honest — it - // never claims coherence it cannot prove. Frozen-safe: it emits nothing, so - // `.text` is byte-identical (proven by the frozen suite). - if let synth_synthesis::liveness::RaFinalVerdict::Violation(v) = - synth_synthesis::liveness::validate_final_allocation(&arm_instrs) - { - return Err(format!( - "VCR-RA-003: register-allocation validation FAILED — {v:?}. \ - The emitted stream violates a register-allocation invariant \ - (callee-saved preservation #490 / spill-slot non-aliasing #331); \ - this is a compiler bug, not a program error. Refusing to emit a \ - miscompiled object." - )); + // component; this whole-function checker proves — by construction, on the + // EXACT emitted stream about to be encoded — that the allocation preserves + // FOUR invariants whose reference lives in the stream (or the ABI): (1) + // callee-saved preservation (#490), (2) spill-slot non-aliasing (#331), and + // — PHASE 2 (#49), extending past straight-line — (3) caller-saved + // preservation across calls (a value in R2/R3/R12 live across a `bl` the + // AAPCS boundary destroys), and (4) value availability across control-flow + // joins (a live-in to a join must be defined on every incoming edge). It runs + // on every ARM compile in the DEFAULT shipping build (NOT behind + // `--features verify`; a verify-gated check would be dormant in exactly the + // build that ships — the #757 / VCR-VER-003 lesson) and hard-errors the + // compile on a VIOLATION. A `NotAttempted` verdict (the join check declines + // on an unmodeled-CF function: numeric branch, `BrTable`, etc.) is NON-FATAL + // — the compile proceeds; the other three invariants were still checked and + // held. This is the decline>guess doctrine applied to the checker itself: it + // never claims join coherence it cannot prove, but it also never blocks a + // correct compile for a construct it simply doesn't model yet. Frozen-safe: + // it emits nothing, so `.text` is byte-identical (proven by the frozen suite). + match synth_synthesis::liveness::validate_final_allocation(&arm_instrs) { + synth_synthesis::liveness::RaFinalVerdict::Violation(v) => { + return Err(format!( + "VCR-RA-003: register-allocation validation FAILED — {v:?}. \ + The emitted stream violates a register-allocation invariant \ + (callee-saved preservation #490 / spill-slot non-aliasing #331 \ + / caller-saved-across-call / join-value-availability); this is a \ + compiler bug, not a program error. Refusing to emit a \ + miscompiled object." + )); + } + // Loud honest decline (join reasoning skipped for an unmodeled-CF + // function). Non-fatal — surface it so the boundary is observable, but + // do NOT stop the compile. + synth_synthesis::liveness::RaFinalVerdict::NotAttempted { reason } => { + eprintln!( + "VCR-RA-003: across-join validation NOT ATTEMPTED ({reason}) — \ + straight-line / callee-saved / across-call invariants held; \ + join-availability reasoning declined on this control-flow shape." + ); + } + synth_synthesis::liveness::RaFinalVerdict::Consistent => {} } // Encode to binary — use Thumb-2 for Cortex-M targets diff --git a/crates/synth-synthesis/src/liveness.rs b/crates/synth-synthesis/src/liveness.rs index 382e77c6..f3c054bf 100644 --- a/crates/synth-synthesis/src/liveness.rs +++ b/crates/synth-synthesis/src/liveness.rs @@ -3577,6 +3577,30 @@ pub enum RaFinalViolation { overwriting_store: usize, stale_reload: usize, }, + /// PHASE 2 (across-CALL): a caller-saved register `reg` ∈ {R2, R3, R12} is + /// LIVE ACROSS a `bl`/`blx`/`call` — it holds a value defined before the + /// call and read after it, with no intervening redefinition — yet the AAPCS + /// call boundary DESTROYS caller-saved registers. The callee is free to + /// clobber R2/R3/R12, so the value the post-call read consumes is garbage. + /// A correct allocator either homes such a value in a callee-saved register + /// (R4-R8, preserved by the callee) or spills it to the frame across the + /// call. `call_index` is the index of the offending call instruction. + /// R0/R1 are DELIBERATELY excluded: a call DEFINES them (return value), so a + /// live R0/R1 across a call is the ubiquitous "use the return value" pattern, + /// not a clobber (documented phase-2 false-negative boundary — we cannot know + /// the callee's return arity, so FN < FP here). + CallerSavedLiveAcrossCall { reg: Reg, call_index: usize }, + /// PHASE 2 (across-JOIN): register `reg` is LIVE-IN to a control-flow join + /// block (≥2 predecessors) but is NOT AVAILABLE (must-defined) on every path + /// reaching the join — some predecessor path never defines it. The value the + /// join consumes is defined on one incoming edge but undefined (stale / + /// wrong) on another: the allocation does not preserve value flow across the + /// merge. `join_block` is the CFG block index of the join. Anchored on the + /// join's own read (a live-in = read-before-write), so it keys on a real + /// in-stream reference, not inferred value-identity (the v0.48 vacuity + /// lesson). Params/SP/LR are seeded available at entry, so a join reading a + /// param is never flagged (documented boundary). + JoinValueNotAvailable { reg: Reg, join_block: usize }, } /// The verdict of the UNCONDITIONAL final register-allocation validator @@ -3594,6 +3618,19 @@ pub enum RaFinalVerdict { Consistent, /// A checked invariant is violated — the compile must hard-error. Violation(RaFinalViolation), + /// PHASE 2 (loud honest decline): a CONSTRUCT is present that the + /// whole-function CF checks cannot model (a numeric-offset branch, a + /// computed/return branch, `BrTable`, a duplicate label, or any op the CFG + /// builder declines) — so the across-JOIN availability check was NOT + /// attempted for this function. The straight-line + callee-saved + across- + /// CALL invariants were still checked (they returned Consistent, else this + /// would be a `Violation`); only the join-availability reasoning is skipped. + /// This is the decline>guess doctrine applied to the checker itself: a false + /// `Consistent` on a join it could not analyze is worse than a loud "not + /// attempted". NON-FATAL at the call site (the compile proceeds) — it names + /// the construct so the boundary is visible, never silently passed. + /// `reason` is a static machine-readable tag. + NotAttempted { reason: &'static str }, } /// VCR-RA-003 UNCONDITIONAL single-stream register-allocation validator (epic @@ -3624,15 +3661,46 @@ pub enum RaFinalVerdict { /// ⇒ [`RaFinalViolation::SpillSlotAliased`]. Tracked with the same holder /// model [`forward_stack_reloads`] uses. /// -/// **Phase-2 boundary (loud, never a false pass).** Control-flow joins and ops -/// [`reg_effect`] cannot model (calls, i64-pair, FP, `BrTable`) end the current -/// spill segment; the callee-saved check still spans the whole function -/// (structural, FAIL-SAFE on `None` — an unmodeled op is treated as a possible -/// callee-saved clobber, so a no-prologue body containing one is flagged). The -/// spill check simply does not reason ACROSS a segment boundary — it never -/// claims a cross-join slot is coherent. The result is always -/// [`RaFinalVerdict::Consistent`] or a concrete `Violation`; there is no silent -/// pass on an unmodeled shape. +/// **Phase 2 (#242, this lane) — WHOLE-FUNCTION across CALLS and JOINS.** Two +/// more invariants extend the checker past straight-line, each anchored on a +/// reference that lives OUTSIDE inferred value-identity (the v0.48 vacuity +/// lesson: generic GP-liveness on one stream cannot tell a clobber from a +/// redefinition): +/// +/// 3. **Caller-saved preservation across a call (across-CALL).** The AAPCS call +/// boundary DESTROYS the caller-saved registers R2/R3/R12. A value in one of +/// them that is defined before a `bl`/`blx`/`call` and read after it (with no +/// redefinition between) crossed a boundary the ABI is contractually allowed +/// to clobber ⇒ [`RaFinalViolation::CallerSavedLiveAcrossCall`]. The +/// reference is the ABI contract at the call, not an inferred value — so the +/// check is non-vacuous. R0/R1 are excluded (a call DEFINES them: the return +/// value), a documented false-negative boundary. Computed locally at the call +/// site with a backward last-read scan; it does NOT modify the shared +/// [`reg_effect`] (whose `None`-on-call meaning the phase-1 callee-saved +/// fail-safe and [`eliminate_unread_frame_stores`] both depend on). +/// +/// 4. **Value availability across a join (across-JOIN).** A register live-in to +/// a CF join (a block with ≥2 predecessors) must be AVAILABLE — must-defined +/// on EVERY path reaching the join (or an entry live-in: a param R0-R3, SP, +/// or LR). A value defined on one incoming edge but undefined on another is +/// consumed stale on the second edge ⇒ +/// [`RaFinalViolation::JoinValueNotAvailable`]. The reference is the join's +/// own read (a live-in = read-before-write in the join block), a real +/// in-stream anchor. Solved by a forward MUST (intersection) availability +/// fixpoint over the label-form CFG ([`cfg_liveness`] supplies the blocks + +/// succ + per-block live-in). +/// +/// **Loud honest decline (never a false pass).** The across-JOIN check needs a +/// complete label-form CFG; a function containing a numeric-offset branch, a +/// computed/return branch, a call, `BrTable`, or a duplicate label makes +/// [`cfg_liveness`] return `None`, and this validator returns +/// [`RaFinalVerdict::NotAttempted`] for the JOIN reasoning (the other three +/// invariants having already passed) rather than silently claiming join +/// coherence it cannot prove. The spill check still segments at every barrier +/// (never reasoning across a join). The result is [`RaFinalVerdict::Consistent`] +/// (all attempted invariants hold), a concrete [`RaFinalVerdict::Violation`], or +/// a loud [`RaFinalVerdict::NotAttempted`] naming the unmodeled construct — there +/// is no silent pass on a shape the checker cannot analyze. pub fn validate_final_allocation(instrs: &[ArmInstruction]) -> RaFinalVerdict { use ArmOp::*; const CALLEE_SAVED: [Reg; 5] = [Reg::R4, Reg::R5, Reg::R6, Reg::R7, Reg::R8]; @@ -3850,9 +3918,485 @@ pub fn validate_final_allocation(instrs: &[ArmInstruction]) -> RaFinalVerdict { } } + // ---- Invariant 3: caller-saved preservation across a call (phase 2) ---- + if let Some(v) = check_caller_saved_across_calls(instrs) { + return RaFinalVerdict::Violation(v); + } + + // ---- Invariant 4: value availability across a join (phase 2) ---- + match check_join_availability(instrs) { + JoinCheck::Consistent => {} + JoinCheck::Violation(v) => return RaFinalVerdict::Violation(v), + JoinCheck::NotAttempted { reason } => { + // The straight-line, callee-saved, and across-call invariants all + // passed; only the join-availability reasoning is skipped for this + // (unmodeled-CF) function. Loud honest decline, non-fatal upstream. + return RaFinalVerdict::NotAttempted { reason }; + } + } + RaFinalVerdict::Consistent } +/// Across-CALL check (VCR-RA-003 phase 2, invariant 3). Returns `Some(violation)` +/// iff some caller-saved register R2/R3/R12 is LIVE ACROSS a `bl`/`blx`/`call`: +/// defined (or a live-in) before the call and read after it with no intervening +/// redefinition. The AAPCS boundary destroys R2/R3/R12, so such a value is +/// consumed garbage after the call. +/// +/// **Non-vacuity anchor.** The clobber is the ABI CONTRACT at the call site, not +/// an inferred redefinition — so a live-across-a-known-clobber is a real bug, +/// distinguishable without value-identity reasoning (the v0.48 lesson). +/// +/// R0/R1 are EXCLUDED (a call defines them: the return value; a live R0/R1 across +/// a call is the "use the return value" pattern). We cannot know callee return +/// arity, so this is a documented false-NEGATIVE boundary (FN < FP). The check +/// does NOT model the call in the shared [`reg_effect`] — it reasons locally, +/// keeping `reg_effect(call) == None` intact for the phase-1 fail-safe. +/// +/// Local liveness definition (backward, register-precise, over the LINEAR +/// stream): a register `c` is "read after the call" iff, scanning forward from +/// just after the call, some instruction USES `c` before any instruction DEFINES +/// `c`. It is "held across the call" iff it was USED-or-DEFINED at some point +/// before the call in the same linear prefix (i.e. it carries a value, not an +/// uninitialised register). We flag when both hold. To stay SOUND across the +/// intervening control flow, a caller-saved reg read after the call with no +/// visible redefinition on the fall-through IS the miscompile the allocator must +/// avoid — a conservative linear scan over-approximates "read after" (it may see +/// a read on a not-taken path), which is the false-POSITIVE-safe direction ONLY +/// if we also require a pre-call producer; both conditions together are the +/// tight signal. Because a false positive here would break frozen, we take the +/// STRICTER route: require the post-call read to be reached with NO intervening +/// def AND on the straight-line fall-through (we stop the forward scan at the +/// first branch/label/call), so we never invent a cross-CF read. +fn check_caller_saved_across_calls(instrs: &[ArmInstruction]) -> Option { + use ArmOp::*; + const CALLER_SAVED: [Reg; 3] = [Reg::R2, Reg::R3, Reg::R12]; + + let is_call = |op: &ArmOp| matches!(op, Bl { .. } | Blx { .. } | Call { .. }); + + for (ci, ins) in instrs.iter().enumerate() { + if !is_call(&ins.op) { + continue; + } + for &c in &CALLER_SAVED { + // (a) pre-call producer: c was defined somewhere in the straight- + // line prefix ending at the call, with no barrier in between + // (so the value is genuinely resident in c at the call). Scan + // backward from just before the call, stop at the first barrier. + let mut has_producer = false; + for prev in instrs[..ci].iter().rev() { + if !is_straight_line(&prev.op) { + break; // barrier: cannot prove c resident from before it + } + if let Some(e) = reg_effect(&prev.op) { + if e.defs.contains(&c) { + has_producer = true; + break; + } + } else { + break; // unmodeled op in prefix: stop conservatively + } + } + if !has_producer { + continue; + } + // (b) post-call consumer on the straight-line fall-through: scan + // forward from just after the call; a USE of c before any DEF of + // c (and before any barrier) proves c is read across the call. + let mut read_after = false; + for next in &instrs[ci + 1..] { + if !is_straight_line(&next.op) { + break; // stop at first branch/label/call — no cross-CF read + } + match reg_effect(&next.op) { + Some(e) => { + if e.uses.contains(&c) { + read_after = true; + break; + } + if e.defs.contains(&c) { + break; // redefined before read → value re-established + } + } + None => break, // unmodeled op: stop conservatively + } + } + if read_after { + return Some(RaFinalViolation::CallerSavedLiveAcrossCall { + reg: c, + call_index: ci, + }); + } + } + } + None +} + +/// Result of the across-JOIN availability check. +enum JoinCheck { + Consistent, + Violation(RaFinalViolation), + NotAttempted { reason: &'static str }, +} + +/// Across-JOIN check (VCR-RA-003 phase 2, invariant 4). A register LIVE-IN to a +/// join block (≥2 predecessors) must be AVAILABLE (must-defined on every path +/// reaching the join, or an entry live-in). Solved by a forward MUST +/// (intersection) availability fixpoint over the label-form CFG. +/// +/// **Non-vacuity anchor.** The reference is the join block's own READ (a live-in +/// = read-before-write) — a real in-stream fact — and the violation is +/// "unavailable on some incoming edge". A value defined in a common dominator IS +/// available on all edges, so a proper availability fixpoint stays SILENT on it +/// (no false positive on real code); only a value missing on some path fires. +/// +/// **Init is UNIVERSE, not empty (MUST/intersection analysis).** `avail_out` of +/// every non-entry block is initialised to the full register set and SHRINKS; +/// the entry's `avail_in` is seeded with the AAPCS entry-live set (R0-R3 params, +/// SP, LR). Initialising to empty (the liveness template's MAY/union init) would +/// wrongly drop dominator-defined values at loop headers → false positive. +/// +/// Declines to [`JoinCheck::NotAttempted`] whenever the CFG cannot be built in +/// complete label-form (numeric-offset branch, `BrTable`, computed `Bx` to a +/// non-`LR` register, duplicate label) — never a guessed CFG. Unlike the shared +/// [`cfg_liveness`] (whose `classify` marks a call / `bx lr` `Unsupported` +/// because other analyses need that), the JOIN CFG admits: +/// - `Bx {LR}` as a no-successor RETURN terminator (a function sink); +/// - `Bl`/`Blx`/`Call` as FALL-THROUGH (a call returns to the next +/// instruction), contributing a DEF of the caller-saved set (R0-R3, R12 — +/// all get new values across the call). Defining the caller-saved set is the +/// false-positive-SAFE (over-approximate availability) direction: a call +/// that returns a value into a join must not spuriously drop it (the latent +/// `bl foo → join → use r0` false positive). +fn check_join_availability(instrs: &[ArmInstruction]) -> JoinCheck { + let Some((blocks, live_in, def_b)) = build_join_cfg(instrs) else { + return JoinCheck::NotAttempted { + reason: "cfg-unmodeled-construct", + }; + }; + let nb = blocks.len(); + if nb == 0 { + return JoinCheck::Consistent; + } + + // Entry-live seed: AAPCS argument registers (R0-R3), SP, LR, AND the four + // RESERVED registers (R9=globals, R10=mem_size, R11=mem_base, R12) — see + // `contracts::regalloc::RESERVED_REGS`. The reserved registers are NEVER + // allocated by the register allocator: the runtime/prologue establishes them + // (R11 = linear-memory base) and every function assumes them resident, so + // they are available function-wide BY CONSTRUCTION, exactly like SP/LR. A + // `str [r11,#off]` in a join block reads R11 without a per-function def; NOT + // seeding them false-positives on every memory-touching branchy function + // (the block_brif_483 `nested` case — R11 defined nowhere in the stream). + // Over-seeding causes only false NEGATIVES; under-seeding would + // false-POSITIVE on real code — so seed generously. + let entry_seed: BTreeSet = [ + Reg::R0, + Reg::R1, + Reg::R2, + Reg::R3, + Reg::R9, + Reg::R10, + Reg::R11, + Reg::R12, + Reg::SP, + Reg::LR, + ] + .into_iter() + .collect(); + + // `def_b` (per-block must-def) and `live_in` are supplied by `build_join_cfg` + // (which models calls' caller-saved def-set — a detail `block_use_def` alone + // would miss, planting the `bl foo → join → use r0` false positive). + + // Predecessors: invert the successor edges. + let mut preds: Vec> = vec![Vec::new(); nb]; + for (b, blk) in blocks.iter().enumerate() { + for &s in &blk.succ { + preds[s].push(b); + } + } + + // The full register universe (any register the stream could define). Using + // the concrete GP + SP/LR set is sufficient: availability only ever tests + // membership for registers that are live-in somewhere, and those are drawn + // from `reg_effect` uses (a subset of this universe). + let universe: BTreeSet = [ + Reg::R0, + Reg::R1, + Reg::R2, + Reg::R3, + Reg::R4, + Reg::R5, + Reg::R6, + Reg::R7, + Reg::R8, + Reg::R9, + Reg::R10, + Reg::R11, + Reg::R12, + Reg::SP, + Reg::LR, + Reg::PC, + ] + .into_iter() + .collect(); + + // Forward MUST (intersection) fixpoint. Init: block 0's `avail_in` is the + // entry seed; every other block's `avail_out` starts at UNIVERSE and shrinks. + let mut avail_in: Vec> = vec![universe.clone(); nb]; + let mut avail_out: Vec> = vec![universe.clone(); nb]; + avail_in[0] = entry_seed.clone(); + + let mut changed = true; + while changed { + changed = false; + for b in 0..nb { + // avail_in[b] = entry_seed (b == 0) else ∩ preds avail_out. + let new_in: BTreeSet = if b == 0 { + entry_seed.clone() + } else if preds[b].is_empty() { + // Unreachable block (no predecessors, not entry): treat as + // universe (vacuously available) — it constrains nothing. + universe.clone() + } else { + let mut it = preds[b].iter(); + let first = *it.next().unwrap(); + let mut acc = avail_out[first].clone(); + for &p in it { + acc = acc.intersection(&avail_out[p]).copied().collect(); + } + acc + }; + // avail_out[b] = avail_in[b] ∪ def_b[b]. + let new_out: BTreeSet = new_in.union(&def_b[b]).copied().collect(); + if new_in != avail_in[b] { + avail_in[b] = new_in; + changed = true; + } + if new_out != avail_out[b] { + avail_out[b] = new_out; + changed = true; + } + } + } + + // Check every JOIN (≥2 preds): each live-in register must be available. + for b in 0..nb { + if preds[b].len() < 2 { + continue; + } + for &r in &live_in[b] { + if !avail_in[b].contains(&r) { + return JoinCheck::Violation(RaFinalViolation::JoinValueNotAvailable { + reg: r, + join_block: b, + }); + } + } + } + + JoinCheck::Consistent +} + +/// Build the JOIN-check CFG: `(blocks, live_in, def_b)`, or `None` (decline) if +/// the stream contains a construct the join analysis cannot model in complete +/// label form. See [`check_join_availability`] for how it differs from the shared +/// [`cfg_liveness`]: `Bx {LR}` is a return SINK and `Bl`/`Blx`/`Call` are +/// FALL-THROUGH with a caller-saved def-set. Everything else that is not a +/// label-form branch (`BOffset`/`BCondOffset`, `BrTable`, computed `Bx`, and any +/// op with no [`reg_effect`] that is not one of the admitted terminators) makes +/// this decline — never a partial/guessed CFG. +#[allow(clippy::type_complexity)] +fn build_join_cfg( + instrs: &[ArmInstruction], +) -> Option<(Vec, Vec>, Vec>)> { + use ArmOp::*; + // Caller-saved registers a call defines (all get fresh values across it). + const CALL_DEFS: [Reg; 5] = [Reg::R0, Reg::R1, Reg::R2, Reg::R3, Reg::R12]; + + // How the JOIN CFG classifies a terminator. Distinct from `classify`: a + // `bx lr` return is a SINK (no successors, not a decline) and a call is + // FALL-THROUGH (returns to next), so branchy functions with calls / returns + // remain analyzable instead of wholesale-declining. + enum JTerm<'a> { + Uncond(&'a str), + Cond(&'a str), + Fall, + Return, // bx lr — no successor + Unsupported, + } + fn jclassify(op: &ArmOp) -> JTerm<'_> { + use ArmOp::*; + match op { + B { label } => JTerm::Uncond(label), + Bhs { label } | Blo { label } | Bcc { label, .. } => JTerm::Cond(label), + Bx { rm: Reg::LR } => JTerm::Return, + // A call returns to the next instruction: fall-through. + Bl { .. } | Blx { .. } | Call { .. } => JTerm::Fall, + // Genuinely unmodeled control flow. + BOffset { .. } | BCondOffset { .. } | Bx { .. } | BrTable { .. } | CallIndirect { .. } => { + JTerm::Unsupported + } + _ => JTerm::Fall, + } + } + let n = instrs.len(); + if n == 0 { + return Some((vec![], vec![], vec![])); + } + + // 1. Admission: every instruction is a modeled label-form branch, an + // admitted terminator (return/call), a Label, or a precise-effect op. + let mut labels_seen: BTreeSet<&str> = BTreeSet::new(); + for ins in instrs { + match jclassify(&ins.op) { + JTerm::Unsupported => return None, + JTerm::Uncond(_) | JTerm::Cond(_) | JTerm::Return => {} + JTerm::Fall => { + // A call is admitted (its def-set is synthesized below); any + // other Fall op must be a Label or have a precise reg_effect. + let is_call = matches!(ins.op, Bl { .. } | Blx { .. } | Call { .. }); + if !is_call + && !matches!(ins.op, Label { .. }) + && reg_effect(&ins.op).is_none() + { + return None; + } + } + } + if let Label { name } = &ins.op + && !labels_seen.insert(name.as_str()) + { + return None; // duplicate label: ambiguous CFG + } + } + + // 2. Leaders: instr 0, every Label, and the instruction after any branch or + // return (a return ends a block; its follower — if any — is a leader). + let mut is_leader = vec![false; n]; + is_leader[0] = true; + for i in 0..n { + if matches!(instrs[i].op, Label { .. }) { + is_leader[i] = true; + } + if matches!( + jclassify(&instrs[i].op), + JTerm::Uncond(_) | JTerm::Cond(_) | JTerm::Return + ) && i + 1 < n + { + is_leader[i + 1] = true; + } + } + let leaders: Vec = (0..n).filter(|&i| is_leader[i]).collect(); + + // 3. Blocks span [leader, next_leader). + let mut blocks: Vec = leaders + .iter() + .enumerate() + .map(|(bi, &start)| BasicBlock { + start, + end: leaders.get(bi + 1).copied().unwrap_or(n), + succ: vec![], + }) + .collect(); + let block_of_start: BTreeMap = + blocks.iter().enumerate().map(|(bi, b)| (b.start, bi)).collect(); + let mut block_of_label: BTreeMap<&str, usize> = BTreeMap::new(); + for (bi, b) in blocks.iter().enumerate() { + if let Label { name } = &instrs[b.start].op { + block_of_label.insert(name.as_str(), bi); + } + } + + // 4. Successors. + let mut succs: Vec> = Vec::with_capacity(blocks.len()); + for b in &blocks { + let last = b.end - 1; + let fallthrough = block_of_start.get(&b.end).copied(); + let succ = match jclassify(&instrs[last].op) { + JTerm::Uncond(label) => vec![*block_of_label.get(label)?], + JTerm::Cond(label) => { + let t = *block_of_label.get(label)?; + let mut s = vec![t]; + if let Some(f) = fallthrough + && f != t + { + s.push(f); + } + s + } + JTerm::Return => vec![], // sink + JTerm::Fall => fallthrough.into_iter().collect(), + JTerm::Unsupported => return None, + }; + succs.push(succ); + } + for (b, succ) in blocks.iter_mut().zip(succs) { + b.succ = succ; + } + + // 5. Per-block use/def and live-in, with the call def-set folded in. We + // compute use/def locally (mirroring `block_use_def`) so a call inside a + // block contributes CALL_DEFS to `def` and — critically for live-in — a + // read of a caller-saved reg BEFORE the call in the same block is a + // genuine use, while a read AFTER the call is satisfied by the call def. + let nb = blocks.len(); + let mut use_b = vec![BTreeSet::::new(); nb]; + let mut def_b = vec![BTreeSet::::new(); nb]; + for (bi, b) in blocks.iter().enumerate() { + let mut used = BTreeSet::new(); + let mut defined = BTreeSet::new(); + for ins in &instrs[b.start..b.end] { + let is_call = matches!(ins.op, Bl { .. } | Blx { .. } | Call { .. }); + let eff = reg_effect(&ins.op).unwrap_or_default(); + for u in &eff.uses { + if !defined.contains(u) { + used.insert(*u); + } + } + for d in &eff.defs { + defined.insert(*d); + } + if is_call { + // A call defines the whole caller-saved set (return + clobbers). + for d in CALL_DEFS { + defined.insert(d); + } + } + } + use_b[bi] = used; + def_b[bi] = defined; + } + + // 6. Backward liveness fixpoint (same shape as `cfg_liveness` step 5). + let mut live_in = vec![BTreeSet::::new(); nb]; + let mut live_out = vec![BTreeSet::::new(); nb]; + let mut changed = true; + while changed { + changed = false; + for bi in (0..nb).rev() { + let mut out = BTreeSet::new(); + for &s in &blocks[bi].succ { + out.extend(live_in[s].iter().copied()); + } + let mut in_ = use_b[bi].clone(); + in_.extend(out.difference(&def_b[bi]).copied()); + if out != live_out[bi] { + live_out[bi] = out; + changed = true; + } + if in_ != live_in[bi] { + live_in[bi] = in_; + changed = true; + } + } + } + + Some((blocks, live_in, def_b)) +} + /// Defense-in-depth: before accepting a segment's rewrite, every interference /// edge is re-checked against the final assignment (independent of the /// colourer), mirroring `verify_allocation`. From 90c09bb2bec009a1b6123481c8c4854d290b6715 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 16:24:48 +0200 Subject: [PATCH 2/5] =?UTF-8?q?test(#242):=20VCR-RA-003=20phase-2=20red-fi?= =?UTF-8?q?rst=20=E2=80=94=20across-CALL=20+=20across-JOIN=20gate?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Six new ra003_ tests prove the phase-2 checks are NON-VACUOUS: - ra003_red_caller_saved_live_across_call_is_caught: R2 defined, bl, R2 read → CallerSavedLiveAcrossCall (asserts the SPECIFIC violation, not Violation|*). - ra003_green_return_value_used_after_call: bl defines R0, R0 read → Consistent (the "use the return value" pattern is not a clobber). - ra003_green_callee_saved_value_across_call: R4 (callee-saved) across bl → clean. - ra003_red_across_join_clobber_is_caught: R4 defined on then-path, R5 (not R4) on else-path, join reads R4 → JoinValueNotAvailable{R4} (specific). - ra003_green_across_join_both_paths_define / _dominator_defined: correct diamonds stay Consistent (no false positive on both-paths-define or dominator-def). - ra003_join_declines_on_unmodeled_control_flow: BrTable → NotAttempted (loud honest decline, never a silent Consistent). Full workspace green (synth-synthesis lib 641), clippy -D clean, fmt clean. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-synthesis/src/liveness.rs | 252 ++++++++++++++++++++++++- 1 file changed, 243 insertions(+), 9 deletions(-) diff --git a/crates/synth-synthesis/src/liveness.rs b/crates/synth-synthesis/src/liveness.rs index f3c054bf..24dcb11c 100644 --- a/crates/synth-synthesis/src/liveness.rs +++ b/crates/synth-synthesis/src/liveness.rs @@ -4236,9 +4236,11 @@ fn build_join_cfg( // A call returns to the next instruction: fall-through. Bl { .. } | Blx { .. } | Call { .. } => JTerm::Fall, // Genuinely unmodeled control flow. - BOffset { .. } | BCondOffset { .. } | Bx { .. } | BrTable { .. } | CallIndirect { .. } => { - JTerm::Unsupported - } + BOffset { .. } + | BCondOffset { .. } + | Bx { .. } + | BrTable { .. } + | CallIndirect { .. } => JTerm::Unsupported, _ => JTerm::Fall, } } @@ -4258,10 +4260,7 @@ fn build_join_cfg( // A call is admitted (its def-set is synthesized below); any // other Fall op must be a Label or have a precise reg_effect. let is_call = matches!(ins.op, Bl { .. } | Blx { .. } | Call { .. }); - if !is_call - && !matches!(ins.op, Label { .. }) - && reg_effect(&ins.op).is_none() - { + if !is_call && !matches!(ins.op, Label { .. }) && reg_effect(&ins.op).is_none() { return None; } } @@ -4301,8 +4300,11 @@ fn build_join_cfg( succ: vec![], }) .collect(); - let block_of_start: BTreeMap = - blocks.iter().enumerate().map(|(bi, b)| (b.start, bi)).collect(); + let block_of_start: BTreeMap = blocks + .iter() + .enumerate() + .map(|(bi, b)| (b.start, bi)) + .collect(); let mut block_of_label: BTreeMap<&str, usize> = BTreeMap::new(); for (bi, b) in blocks.iter().enumerate() { if let Label { name } = &instrs[b.start].op { @@ -14199,4 +14201,236 @@ mod tests { ]; assert_eq!(validate_final_allocation(&body), RaFinalVerdict::Consistent); } + + // ================================================================ + // VCR-RA-003 PHASE 2 (#242): across-CALL + across-JOIN red-first gate. + // ================================================================ + + fn label(name: &str) -> ArmInstruction { + ins(ArmOp::Label { + name: name.to_string(), + }) + } + fn bcc(cond: Condition, name: &str) -> ArmInstruction { + ins(ArmOp::Bcc { + cond, + label: name.to_string(), + }) + } + fn b(name: &str) -> ArmInstruction { + ins(ArmOp::B { + label: name.to_string(), + }) + } + fn bl(name: &str) -> ArmInstruction { + ins(ArmOp::Bl { + label: name.to_string(), + }) + } + fn add_rr(rd: Reg, rn: Reg, rm: Reg) -> ArmInstruction { + ins(ArmOp::Add { + rd, + rn, + op2: Operand2::Reg(rm), + }) + } + // ---- across-CALL: RED (a caller-saved value live across a bl) ---- + #[test] + fn ra003_red_caller_saved_live_across_call_is_caught() { + // R2 holds a value (movw), a `bl` runs (the AAPCS boundary DESTROYS R2), + // then R2 is read after the call — the callee was free to clobber it, so + // the post-call read consumes garbage. The allocator should have homed + // the value in a callee-saved reg or spilled it across the call. + let body = vec![ + push_prologue(vec![Reg::R4, Reg::LR]), + movi(Reg::R2, 0x55), // define R2 (caller-saved)… + bl("func_1"), // …AAPCS boundary destroys R2… + add_rr(Reg::R0, Reg::R2, Reg::R2), // …but R2 is read after → clobber + pop_epilogue(vec![Reg::R4, Reg::PC]), + ]; + let verdict = validate_final_allocation(&body); + assert!( + matches!( + verdict, + RaFinalVerdict::Violation(RaFinalViolation::CallerSavedLiveAcrossCall { + reg: Reg::R2, + .. + }) + ), + "a caller-saved value live across a call MUST be caught, got {verdict:?}" + ); + } + + // ---- across-CALL: GREEN (return value used after call is NOT a clobber) -- + #[test] + fn ra003_green_return_value_used_after_call_is_consistent() { + // The ubiquitous "use the return value" pattern: `bl` defines R0, then R0 + // is read. A call DEFINES R0/R1 (return), so this is not a clobber — the + // documented R0/R1 false-negative boundary. Must be Consistent, not a + // false positive (else every call-returning function stops compiling). + let body = vec![ + push_prologue(vec![Reg::R4, Reg::LR]), + bl("func_1"), // defines R0 (return value) + add_rr(Reg::R1, Reg::R0, Reg::R0), // read the return value — legal + pop_epilogue(vec![Reg::R4, Reg::PC]), + ]; + assert_eq!( + validate_final_allocation(&body), + RaFinalVerdict::Consistent, + "using a call's return value must not be flagged as a clobber" + ); + } + + // ---- across-CALL: GREEN (callee-saved value survives a call) ---- + #[test] + fn ra003_green_callee_saved_value_across_call_is_consistent() { + // The CORRECT allocation of the red case: home the live value in R4 + // (callee-saved — the callee preserves it), so reading it after the call + // is sound. The prologue saves R4. Must be Consistent. + let body = vec![ + push_prologue(vec![Reg::R4, Reg::LR]), + movi(Reg::R4, 0x55), // define R4 (callee-saved, preserved by callee) + bl("func_1"), + add_rr(Reg::R0, Reg::R4, Reg::R4), // read R4 after call — sound + pop_epilogue(vec![Reg::R4, Reg::PC]), + ]; + assert_eq!( + validate_final_allocation(&body), + RaFinalVerdict::Consistent, + "a callee-saved value read across a call must validate clean" + ); + } + + // ---- across-JOIN: RED (a value in different locations on two paths) ---- + #[test] + fn ra003_red_across_join_clobber_is_caught() { + // The across-join clobber: the value flowing into the join is placed in + // R4 on the then-path but the else-path defines R5 (NOT R4). The join + // block READS R4 (live-in), but R4 is not available on the else edge — + // the join consumes a stale/undefined R4 on that path. On R4-R8 (not a + // param) so the entry seed does not mask it. + // + // entry: push {r4,r5,lr} ; cmp r0,#0 ; beq .else + // then: movw r4,#7 ; b .join (R4 defined) + // else: movw r5,#9 (R5 defined, R4 is NOT) + // join: add r0,r4,r4 ; pop {r4,r5,pc} (reads R4 — unavailable on else) + // The prologue saves R4/R5 so invariant 1 (callee-saved) passes and the + // join check is the one that fires — proving invariant 4 non-vacuous. + let body = vec![ + push_prologue(vec![Reg::R4, Reg::R5, Reg::LR]), + ins(ArmOp::Cmp { + rn: Reg::R0, + op2: Operand2::Imm(0), + }), + bcc(Condition::EQ, ".else"), + // then-path + movi(Reg::R4, 7), + b(".join"), + // else-path + label(".else"), + movi(Reg::R5, 9), // defines R5, NOT R4 + // join + label(".join"), + add_rr(Reg::R0, Reg::R4, Reg::R4), // reads R4 — not available on else + pop_epilogue(vec![Reg::R4, Reg::R5, Reg::PC]), + ]; + let verdict = validate_final_allocation(&body); + assert!( + matches!( + verdict, + RaFinalVerdict::Violation(RaFinalViolation::JoinValueNotAvailable { + reg: Reg::R4, + .. + }) + ), + "a value live into a join but undefined on one path MUST be caught, got {verdict:?}" + ); + } + + // ---- across-JOIN: GREEN (value defined on BOTH paths is consistent) ---- + #[test] + fn ra003_green_across_join_both_paths_define_is_consistent() { + // The CORRECT allocation: BOTH paths place the join value in R4, so R4 is + // available on every incoming edge. Must be Consistent — a false positive + // here would break every real diamond that merges a value. + let body = vec![ + push_prologue(vec![Reg::R4, Reg::LR]), + ins(ArmOp::Cmp { + rn: Reg::R0, + op2: Operand2::Imm(0), + }), + bcc(Condition::EQ, ".else"), + movi(Reg::R4, 7), // then defines R4 + b(".join"), + label(".else"), + movi(Reg::R4, 9), // else ALSO defines R4 + label(".join"), + add_rr(Reg::R0, Reg::R4, Reg::R4), // reads R4 — available on both + pop_epilogue(vec![Reg::R4, Reg::PC]), + ]; + assert_eq!( + validate_final_allocation(&body), + RaFinalVerdict::Consistent, + "a value defined on both incoming edges must validate clean" + ); + } + + // ---- across-JOIN: GREEN (dominator-defined value survives the merge) ---- + #[test] + fn ra003_green_dominator_defined_value_across_join_is_consistent() { + // A value defined in the common dominator (entry block) before the split + // is available on ALL paths — the availability fixpoint must stay SILENT + // on it (the "no false positive on dominator-defined" property). + let body = vec![ + push_prologue(vec![Reg::R4, Reg::R5, Reg::R6, Reg::LR]), + movi(Reg::R4, 42), // dominator-defines R4, before the split + ins(ArmOp::Cmp { + rn: Reg::R0, + op2: Operand2::Imm(0), + }), + bcc(Condition::EQ, ".else"), + movi(Reg::R5, 1), // then touches an unrelated reg + b(".join"), + label(".else"), + movi(Reg::R6, 2), // else touches another unrelated reg + label(".join"), + add_rr(Reg::R0, Reg::R4, Reg::R4), // reads the dominator R4 — sound + pop_epilogue(vec![Reg::R4, Reg::R5, Reg::R6, Reg::PC]), + ]; + assert_eq!( + validate_final_allocation(&body), + RaFinalVerdict::Consistent, + "a dominator-defined value must not be flagged at a join" + ); + } + + // ---- across-JOIN: honest decline (unmodeled CF → NotAttempted) ---- + #[test] + fn ra003_join_declines_on_unmodeled_control_flow() { + // A `BrTable` (real multi-way divergence) is outside the modeled label- + // form CFG. The join check must LOUD-decline (NotAttempted), never a + // silent Consistent claiming coherence it cannot prove. The callee-saved + // + across-call invariants still ran (they held) — only the join + // reasoning is skipped. + let body = vec![ + push_prologue(vec![Reg::R4, Reg::LR]), + movi(Reg::R0, 1), + ins(ArmOp::BrTable { + rd: Reg::R1, + index_reg: Reg::R0, + targets: vec![0, 1], + default: 0, + }), + label("a"), + label("b"), + pop_epilogue(vec![Reg::R4, Reg::PC]), + ]; + assert!( + matches!( + validate_final_allocation(&body), + RaFinalVerdict::NotAttempted { .. } + ), + "an unmodeled-CF function must LOUD-decline the join check, not pass silently" + ); + } } From aae9b41f98affb882b02b74bd0d839056703b7e3 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 16:27:36 +0200 Subject: [PATCH 3/5] ci+docs(#242): wire VCR-RA-003 phase-2 gate + repro + roadmap note - ci.yml: append a third step to vcr-ra-003-alloc-validator-gate running scripts/repro/vcr_ra_003_phase2_join_call.py over branchy/mem/call fixtures (silent-on-real-branchy-codegen; the R11-linmem-base false-positive guard). Existing red-first (ra003_) + frozen steps untouched. - scripts/repro/vcr_ra_003_phase2_join_call.py: compiles 7 CF-join / memory / call fixtures through the unconditional validator, asserts 0 false positives. - artifacts/verified-codegen-roadmap.yaml: VCR-RA-003 phase-2 note (invariants 3+4, the NotAttempted honest decline, the reserved-reg seed fix, vacuity-in- practice evidence). Zero new rivet errors (52/102 identical to origin/main). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 34 ++++-- artifacts/verified-codegen-roadmap.yaml | 50 ++++++++- scripts/repro/vcr_ra_003_phase2_join_call.py | 112 +++++++++++++++++++ 3 files changed, 184 insertions(+), 12 deletions(-) create mode 100644 scripts/repro/vcr_ra_003_phase2_join_call.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e578fa56..a17c74bb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1636,23 +1636,33 @@ jobs: vcr-ra-003-alloc-validator-gate: name: "VCR-RA-003 register-allocation validator (red-first + frozen)" - # VCR-RA-003 (#242): the UNCONDITIONAL, single-stream backward-dataflow - # register-allocation validator (synth_synthesis::liveness:: - # validate_final_allocation) runs on every ARM compile in the default build - # and hard-errors on a callee-saved-preservation (#490) or spill-slot - # non-aliasing (#331) violation. This job pins the gate's TWO halves as an - # explicit, self-describing red so a regression is visible on its own name: + # VCR-RA-003 (#242): the UNCONDITIONAL register-allocation validator + # (synth_synthesis::liveness::validate_final_allocation) runs on every ARM + # compile in the default build and hard-errors on a violation of FOUR + # invariants: (1) callee-saved preservation (#490), (2) spill-slot + # non-aliasing (#331), and — PHASE 2 (#49), whole-function past straight-line + # — (3) caller-saved preservation across a call and (4) value availability + # across a control-flow join. This job pins the gate's halves as an explicit, + # self-describing red so a regression is visible on its own name: # (1) RED-FIRST non-vacuity: the ra003_red_* unit tests synthetically - # revert a known-fixed clobber and assert the validator CATCHES it - # (revert #490 prologue -> CalleeSavedNotSaved; drop epilogue restore + # revert / construct a known clobber and assert the validator CATCHES + # it (revert #490 prologue -> CalleeSavedNotSaved; drop epilogue restore # -> CalleeSavedNotRestored; alias two live values on one slot -> - # SpillSlotAliased). The ra003_green_* tests assert it is SILENT on - # correct code (the Consistent half). + # SpillSlotAliased; a caller-saved value live across a bl -> + # CallerSavedLiveAcrossCall; a value in R4 on one join path but not the + # other -> JoinValueNotAvailable; a BrTable -> NotAttempted loud + # decline). The ra003_green_* tests assert it is SILENT on correct code. # (2) SILENT-ON-REAL-CODEGEN: the frozen suite compiles the whole ARM # fixture set THROUGH the unconditional validator; if it false-positived # on any real function that fixture would fail to compile, so 10/10 green # (control_step 0x00210A55, flight_algo 0x07FDF307 byte-identical) is the # validator's "Consistent on every real function" proof. + # (3) PHASE-2 SILENT + FIRES ON REAL BRANCHY CODEGEN: the phase-2 repro + # compiles branchy / memory-touching / call-bearing fixtures (real CF + # joins the availability check reasons about) and asserts ZERO false + # positives — the guard against the R11-linmem-base regression this lane + # found (a join reading the reserved base register, defined nowhere in + # the stream, must be seeded available not flagged). runs-on: ubuntu-latest steps: - uses: actions/checkout@v7 @@ -1671,3 +1681,7 @@ jobs: run: cargo test -p synth-synthesis --lib ra003_ - name: Silent-on-real-codegen (frozen suite through the unconditional gate) run: cargo test -p synth-cli --test frozen_codegen_bytes + - name: PHASE-2 silent-on-real-branchy-codegen (across-CALL + across-JOIN) + run: | + cargo build -p synth-cli + python3 scripts/repro/vcr_ra_003_phase2_join_call.py ./target/debug/synth diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 133e1dc2..12428bef 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -1898,8 +1898,54 @@ artifacts: in synth-synthesis (not synth-core) because ArmOp/Reg live there and the register-assigned stream is consumed in arm_backend before main.rs. ARM-scoped this increment; RV32 / AArch64 get their own arms later - (per-backend, like VCR-VER-003). v2 (Rocq-mechanized soundness of the - straight-line fragment) remains the open step. + (per-backend, like VCR-VER-003). + PHASE 2 (v0.49, #49) — WHOLE-FUNCTION across CALLS and JOINS: the named + phase-2 boundary is now extended past straight-line with two more + invariants, each anchored on a reference OUTSIDE inferred value-identity + (the v0.48 vacuity lesson: generic GP-liveness on one stream cannot tell + a clobber from a redefinition). (3) CALLER-SAVED PRESERVATION ACROSS A + CALL: a value in R2/R3/R12 defined before a bl/blx/call and read after it + with no intervening redef crossed a boundary the AAPCS is contractually + allowed to clobber -> `CallerSavedLiveAcrossCall`; the reference is the + ABI contract at the call, not an inferred value. R0/R1 are EXCLUDED (a + call DEFINES them: the return value) - a documented false-NEGATIVE + boundary (FN < FP). Reasoned locally at the call site; does NOT modify the + shared `reg_effect` (whose None-on-call meaning the phase-1 callee-saved + fail-safe and `eliminate_unread_frame_stores` both depend on). (4) VALUE + AVAILABILITY ACROSS A JOIN: a register live-in to a CF join (>=2 preds) + must be AVAILABLE - must-defined on EVERY incoming path, or an entry + live-in -> else `JoinValueNotAvailable`. Solved by a forward MUST + (intersection) availability fixpoint (UNIVERSE-init, not empty - it is a + must-analysis) over a DEDICATED join CFG (`build_join_cfg`) that admits + `bx lr` returns (sinks) and calls (fall-through with a caller-saved + def-set), so branchy functions with calls/returns remain analyzable + instead of wholesale-declining. Entry seed = params R0-R3, SP, LR, AND the + RESERVED registers R9/R10/R11/R12 (`contracts::regalloc::RESERVED_REGS` - + R11 = linmem base etc., never allocated, resident by construction); + seeding them is REQUIRED to avoid a false positive on every + memory-touching branchy function (the block_brif_483 `nested` case: a + `str [r11,#off]` at a join, R11 defined nowhere in the stream - this lane + FOUND + FIXED that regression). RaFinalVerdict gains `NotAttempted { + reason }` - a LOUD honest decline when the join CFG cannot be built + (numeric branch, BrTable, computed Bx, duplicate label); NON-FATAL at the + arm_backend call site (only Violation hard-errors), so a construct the + checker cannot model never blocks a correct compile but is also never + silently passed. RED-FIRST non-vacuity extended (17 `ra003_*` tests): +2 + RED assert the SPECIFIC violation (a caller-saved value live across a bl + -> CallerSavedLiveAcrossCall; a value in R4 on one join path but not the + other -> JoinValueNotAvailable), +4 GREEN (return-value-after-call, + callee-saved-across-call, both-paths-define, dominator-defined at a join), + +1 NotAttempted (BrTable -> loud decline). Vacuity-in-practice VERIFIED: + invariant 4 FIRES on real branchy codegen (if_else_result_343 / + cf_shapes_500 / block_brif_483 joins all Consistent, incl. a real R11 + availability check) - not unit-tested-but-dead-in-shipping. 130-fixture + sweep: 0 false positives. CI-gated: the third + `vcr-ra-003-alloc-validator-gate` step runs + `scripts/repro/vcr_ra_003_phase2_join_call.py` over branchy/mem/call + fixtures (silent-on-real-branchy-codegen). Frozen-safe (emits nothing; + control_step 0x00210A55 / flight_algo 0x07FDF307 byte-identical, 10/10). + v2 (Rocq-mechanized soundness of the straight-line fragment) remains the + open step. - id: VCR-RA-004 type: sw-req diff --git a/scripts/repro/vcr_ra_003_phase2_join_call.py b/scripts/repro/vcr_ra_003_phase2_join_call.py new file mode 100644 index 00000000..e70c9dfd --- /dev/null +++ b/scripts/repro/vcr_ra_003_phase2_join_call.py @@ -0,0 +1,112 @@ +#!/usr/bin/env python3 +"""VCR-RA-003 phase 2 (#242) repro — across-CALL + across-JOIN allocation validation. + +The v0.48 validator (`validate_final_allocation`) was BOUNDED to straight-line +segments + callee-saved/spill discipline. Phase 2 extends it to WHOLE-FUNCTION +control flow: + + Invariant 3 (across-CALL): a caller-saved register R2/R3/R12 held live across a + bl/blx/call is flagged (the AAPCS boundary destroys it). R0/R1 excluded + (return value). Anchored on the ABI contract, not inferred value-identity. + + Invariant 4 (across-JOIN): a register live-in to a control-flow join (>=2 + predecessors) must be AVAILABLE (must-defined on every incoming path, or an + entry live-in). Forward MUST/intersection availability fixpoint over a + dedicated join CFG (bx-lr returns = sinks, calls = fall-through with a + caller-saved def-set; reserved R9/R10/R11/R12 + params/SP/LR seeded). + +This script is the SILENT-ON-REAL-CODEGEN half of the gate: it compiles a set of +branchy + memory-touching + call-bearing repro fixtures through the UNCONDITIONAL +validator and asserts ZERO false positives (no `VCR-RA-003 ... FAILED`). If the +across-JOIN check false-positived (e.g. the R11 linmem-base regression this lane +found + fixed by seeding the reserved registers), one of these would decline to +compile and this gate would go red. + +The RED (non-vacuity) half lives in the `ra003_red_*` unit tests +(`cargo test -p synth-synthesis --lib ra003_`), which assert the validator +CATCHES a synthetic across-CALL clobber and across-JOIN clobber. + +Usage: python3 scripts/repro/vcr_ra_003_phase2_join_call.py [path/to/synth] +Exit 0 iff every branchy fixture compiles clean (validator silent on real code). +""" +import subprocess +import sys +import tempfile +from pathlib import Path + +REPO = Path(__file__).resolve().parents[2] +REPRO = REPO / "scripts" / "repro" + +# Fixtures with real control-flow joins (br/br_if/block/loop/if) and/or memory +# stores through the reserved R11 base — the shapes invariant 4 reasons about. +BRANCHY_FIXTURES = [ + "block_brif_483.wat", # forward block + br_if; nested br 1 (the R11 case) + "if_else_result_343.wat", # if/else merging a value at the join + "cf_shapes_500.wat", # assorted CF shapes, promoted-local + R11 joins + "br_value_509.wat", # br carrying a value + "brif_outer_740.wat", # br_if to an outer block + "loop_param_bound_663.wat", # counted loop (loop-header join) + "base_cse_branch.wat", # base-CSE across a branch (R11 base at a join) +] + + +def synth_bin() -> str: + if len(sys.argv) > 1: + return sys.argv[1] + # Prefer an env-redirected target dir, else the workspace default. + import os + tgt = os.environ.get("CARGO_TARGET_DIR", str(REPO / "target")) + return str(Path(tgt) / "debug" / "synth") + + +def main() -> int: + binp = synth_bin() + if not Path(binp).exists(): + print(f"error: synth binary not found at {binp}", file=sys.stderr) + print("build first: cargo build -p synth-cli", file=sys.stderr) + return 2 + + failures = [] + checked = 0 + for fx in BRANCHY_FIXTURES: + path = REPRO / fx + if not path.exists(): + print(f"warn: fixture missing, skipping: {fx}", file=sys.stderr) + continue + checked += 1 + with tempfile.NamedTemporaryFile(suffix=".elf") as out: + proc = subprocess.run( + [binp, "compile", str(path), "-o", out.name, "--relocatable"], + capture_output=True, + text=True, + ) + combined = proc.stdout + proc.stderr + if "VCR-RA-003" in combined and "FAILED" in combined: + # Extract the offending line for the report. + line = next( + (l for l in combined.splitlines() if "FAILED" in l and "VCR-RA-003" in l), + "", + ) + failures.append((fx, line.strip())) + print(f"FAIL {fx}: validator false-positived on real codegen") + print(f" {line.strip()}") + else: + print(f"ok {fx}: validator silent (Consistent / NotAttempted)") + + print(f"\nchecked {checked} branchy fixtures; {len(failures)} false-positives") + if failures: + print( + "\nVCR-RA-003 phase-2 across-JOIN/across-CALL check FALSE-POSITIVED on " + "real codegen — the availability seed or the join CFG is wrong.", + file=sys.stderr, + ) + return 1 + print( + "VCR-RA-003 phase 2 SILENT on real branchy codegen — the whole-function " + "across-CALL + across-JOIN checks pass every real fixture." + ) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) From ad934f6e3778530171d1166d857e4dab750be819 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 16:34:38 +0200 Subject: [PATCH 4/5] fix(#242): VCR-RA-003 phase-2 default-path coverage + gate the decline eprintln MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Advisor caught: all phase-2 verification was --relocatable only; the DEFAULT optimized path (what the control_step differential actually compiles) had never run through invariants 3/4. - Verified the default path: control_step + 7 branchy fixtures × {relocatable, default} = 16 pairs, 0 false-positive Violations; full 130-fixture default-path sweep also 0 violations. No blocking issue. - HONEST SCOPE: on the default path branches are pre-resolved to NUMERIC offsets, so invariant 4 declines to NotAttempted there (invariants 1-3 still run). It FIRES on the label-form/relocatable path. Numeric-branch CFG = named follow-up. - Gate the NotAttempted eprintln behind SYNTH_RA003_VERBOSE: the decline is the COMMON default-path case (~41/130 fixtures) — unconditional it would spam every branchy production compile (noise phase 1 never produced). Verdict stays observable on demand; the repro greps FAILED so it's unaffected. - repro now sweeps BOTH paths + control_step.wasm; roadmap states the path scope. Frozen 10/10 byte-identical, clippy 0, control_step default-path clean. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- artifacts/verified-codegen-roadmap.yaml | 29 +++++++--- crates/synth-backend/src/arm_backend.rs | 23 +++++--- scripts/repro/vcr_ra_003_phase2_join_call.py | 60 +++++++++++--------- 3 files changed, 71 insertions(+), 41 deletions(-) diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 12428bef..bbc05bb1 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -1938,14 +1938,27 @@ artifacts: +1 NotAttempted (BrTable -> loud decline). Vacuity-in-practice VERIFIED: invariant 4 FIRES on real branchy codegen (if_else_result_343 / cf_shapes_500 / block_brif_483 joins all Consistent, incl. a real R11 - availability check) - not unit-tested-but-dead-in-shipping. 130-fixture - sweep: 0 false positives. CI-gated: the third - `vcr-ra-003-alloc-validator-gate` step runs - `scripts/repro/vcr_ra_003_phase2_join_call.py` over branchy/mem/call - fixtures (silent-on-real-branchy-codegen). Frozen-safe (emits nothing; - control_step 0x00210A55 / flight_algo 0x07FDF307 byte-identical, 10/10). - v2 (Rocq-mechanized soundness of the straight-line fragment) remains the - open step. + availability check) - not unit-tested-but-dead-in-shipping. + HONEST PATH SCOPE: invariant 4 FIRES (analyzable label-form CFG) on the + RELOCATABLE / direct-selector path; on the DEFAULT optimized path branches + are already resolved to NUMERIC offsets (BOffset/BCondOffset) before the + validator runs, so the join CFG cannot be built and invariant 4 declines + to NotAttempted THERE (invariants 1-3 still run on both paths - a + false-positive Violation on either would hard-error the compile). Verified + BOTH paths: control_step on the DEFAULT path (the control_step + differential's own input) + 7 branchy fixtures × {relocatable, default} = + 16 pairs, 0 false positives; the full 130-fixture default-path sweep is + also 0 violations. The NotAttempted decline is COMMON on the default path + (~41/130 fixtures), so its diagnostic eprintln is gated behind + `SYNTH_RA003_VERBOSE` (a production compile stays quiet; the verdict is + observable on demand). Extending invariant 4 to the numeric-branch + optimized path (a resolved-offset CFG builder, the #606 geometry) is a + NAMED follow-up. CI-gated: the third `vcr-ra-003-alloc-validator-gate` + step runs `scripts/repro/vcr_ra_003_phase2_join_call.py` over + branchy/mem/call fixtures on BOTH paths (silent-on-real-branchy-codegen). + Frozen-safe (emits nothing; control_step 0x00210A55 / flight_algo + 0x07FDF307 byte-identical, 10/10). v2 (Rocq-mechanized soundness of the + straight-line fragment) remains the open step. - id: VCR-RA-004 type: sw-req diff --git a/crates/synth-backend/src/arm_backend.rs b/crates/synth-backend/src/arm_backend.rs index a954c39f..3bcb4871 100644 --- a/crates/synth-backend/src/arm_backend.rs +++ b/crates/synth-backend/src/arm_backend.rs @@ -1390,14 +1390,23 @@ fn compile_wasm_to_arm( )); } // Loud honest decline (join reasoning skipped for an unmodeled-CF - // function). Non-fatal — surface it so the boundary is observable, but - // do NOT stop the compile. + // function). Non-fatal — the straight-line / callee-saved / across-call + // invariants still ran and held; only the across-JOIN availability + // reasoning is skipped (the optimized path pre-resolves branches to + // NUMERIC offsets, outside the label-form CFG the join check needs, so + // this is the COMMON case on the default path — ~41/130 repro fixtures). + // Surfaced only under `SYNTH_RA003_VERBOSE` so a production compile stays + // quiet: emitting it unconditionally would print on every branchy + // optimized-path compile (new stderr noise phase 1 never produced), yet + // it must remain observable on demand for the honest-scope audit. synth_synthesis::liveness::RaFinalVerdict::NotAttempted { reason } => { - eprintln!( - "VCR-RA-003: across-join validation NOT ATTEMPTED ({reason}) — \ - straight-line / callee-saved / across-call invariants held; \ - join-availability reasoning declined on this control-flow shape." - ); + if std::env::var_os("SYNTH_RA003_VERBOSE").is_some() { + eprintln!( + "VCR-RA-003: across-join validation NOT ATTEMPTED ({reason}) — \ + straight-line / callee-saved / across-call invariants held; \ + join-availability reasoning declined on this control-flow shape." + ); + } } synth_synthesis::liveness::RaFinalVerdict::Consistent => {} } diff --git a/scripts/repro/vcr_ra_003_phase2_join_call.py b/scripts/repro/vcr_ra_003_phase2_join_call.py index e70c9dfd..1956073d 100644 --- a/scripts/repro/vcr_ra_003_phase2_join_call.py +++ b/scripts/repro/vcr_ra_003_phase2_join_call.py @@ -40,6 +40,7 @@ # Fixtures with real control-flow joins (br/br_if/block/loop/if) and/or memory # stores through the reserved R11 base — the shapes invariant 4 reasons about. BRANCHY_FIXTURES = [ + "control_step.wasm", # the control_step differential's own input (default path) "block_brif_483.wat", # forward block + br_if; nested br 1 (the R11 case) "if_else_result_343.wat", # if/else merging a value at the join "cf_shapes_500.wat", # assorted CF shapes, promoted-local + R11 joins @@ -68,32 +69,39 @@ def main() -> int: failures = [] checked = 0 - for fx in BRANCHY_FIXTURES: - path = REPRO / fx - if not path.exists(): - print(f"warn: fixture missing, skipping: {fx}", file=sys.stderr) - continue - checked += 1 - with tempfile.NamedTemporaryFile(suffix=".elf") as out: - proc = subprocess.run( - [binp, "compile", str(path), "-o", out.name, "--relocatable"], - capture_output=True, - text=True, - ) - combined = proc.stdout + proc.stderr - if "VCR-RA-003" in combined and "FAILED" in combined: - # Extract the offending line for the report. - line = next( - (l for l in combined.splitlines() if "FAILED" in l and "VCR-RA-003" in l), - "", - ) - failures.append((fx, line.strip())) - print(f"FAIL {fx}: validator false-positived on real codegen") - print(f" {line.strip()}") - else: - print(f"ok {fx}: validator silent (Consistent / NotAttempted)") - - print(f"\nchecked {checked} branchy fixtures; {len(failures)} false-positives") + # Sweep BOTH the label-form/relocatable path (where invariant 4 FIRES: + # label branches → an analyzable CFG) AND the DEFAULT optimized path (the + # SHIPPING path the control_step differential compiles: pre-resolved numeric + # branches → invariant 4 declines to NotAttempted, but invariants 1-3 still + # run and a false-positive Violation would hard-error the compile). A false + # positive on EITHER path reds this gate. + for path_name, extra_args in (("relocatable", ["--relocatable"]), ("default", [])): + for fx in BRANCHY_FIXTURES: + path = REPRO / fx + if not path.exists(): + if path_name == "relocatable": + print(f"warn: fixture missing, skipping: {fx}", file=sys.stderr) + continue + checked += 1 + with tempfile.NamedTemporaryFile(suffix=".elf") as out: + proc = subprocess.run( + [binp, "compile", str(path), "-o", out.name, *extra_args], + capture_output=True, + text=True, + ) + combined = proc.stdout + proc.stderr + if "VCR-RA-003" in combined and "FAILED" in combined: + line = next( + (l for l in combined.splitlines() if "FAILED" in l and "VCR-RA-003" in l), + "", + ) + failures.append((fx, path_name, line.strip())) + print(f"FAIL [{path_name}] {fx}: validator false-positived on real codegen") + print(f" {line.strip()}") + else: + print(f"ok [{path_name}] {fx}: validator silent (Consistent / NotAttempted)") + + print(f"\nchecked {checked} (fixture, path) pairs; {len(failures)} false-positives") if failures: print( "\nVCR-RA-003 phase-2 across-JOIN/across-CALL check FALSE-POSITIVED on " From 0199f6a5e8f977ff2e96fcdaf3fd4d54bf5cba9c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 16:46:36 +0200 Subject: [PATCH 5/5] =?UTF-8?q?test(#242):=20VCR-RA-003=20phase-2=20?= =?UTF-8?q?=E2=80=94=20durable=20loop=20back-edge=20guard=20for=20universe?= =?UTF-8?q?-init?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Advisor caught: universe-init (the load-bearing MUST/intersection fixpoint correction) had zero CONFIRMED exercise as a Consistent-via-fixpoint result on a real back-edge — all prior evidence was forward diamonds. loop_param_bound_663 traces Consistent on the relocatable path, but the sweep conflated Consistent/NotAttempted. ra003_green_loop_back_edge_preserves_availability: a value (R4) defined before a loop and read in the body; the loop header is a join of preheader + back-edge. Verified NON-VACUOUS: flipping avail_out init from universe to empty makes this test FAIL (a false positive — the back-edge starts empty and the intersection drops the dominator-defined R4), so it durably guards the universe-init choice. 18 ra003_ tests pass; frozen 10/10 (test-only, byte-identical); clippy 0; fmt clean. Confirmed ci.yml line-75 PyYAML/actionlint parse note is PRE-EXISTING on origin/main (a `space::` scalar), not this lane's merge resolution. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-synthesis/src/liveness.rs | 45 ++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/crates/synth-synthesis/src/liveness.rs b/crates/synth-synthesis/src/liveness.rs index 24dcb11c..7daf4992 100644 --- a/crates/synth-synthesis/src/liveness.rs +++ b/crates/synth-synthesis/src/liveness.rs @@ -14433,4 +14433,49 @@ mod tests { "an unmodeled-CF function must LOUD-decline the join check, not pass silently" ); } + + // ---- across-JOIN: GREEN back-edge (the UNIVERSE-init correctness case) --- + #[test] + fn ra003_green_loop_back_edge_preserves_availability() { + // A LOOP: a value (R4) is defined BEFORE the loop and read INSIDE the + // body. The loop header is a join whose predecessors are the preheader + // AND the back-edge (body-tail). This is the exact case the forward + // MUST/intersection fixpoint's UNIVERSE-init protects: if the back-edge + // block were initialised to EMPTY (the liveness template's MAY/union + // init), the header's avail_in = avail_out[preheader] ∩ avail_out[back] + // would drop R4 on the first iteration and false-positive. With + // universe-init the back-edge starts full and shrinks only to what it + // genuinely lacks, so R4 (dominator-defined) stays available across the + // merge → Consistent. + // + // push {r4,r5,lr} + // movw r4,#7 ; R4 defined before the loop (dominator) + // movw r5,#0 ; counter + // .head: ; loop header — JOIN of preheader + back-edge + // add r0,r4,r4 ; reads R4 inside the body (live-in to header) + // add r5,r5,r5 ; mutate counter + // cmp r5,#0 + // bne .head ; back-edge to the header + // pop {r4,r5,pc} + let body = vec![ + push_prologue(vec![Reg::R4, Reg::R5, Reg::LR]), + movi(Reg::R4, 7), // dominator-defines R4 before the loop + movi(Reg::R5, 0), + label(".head"), + add_rr(Reg::R0, Reg::R4, Reg::R4), // reads R4 in the body + add_rr(Reg::R5, Reg::R5, Reg::R5), + ins(ArmOp::Cmp { + rn: Reg::R5, + op2: Operand2::Imm(0), + }), + bcc(Condition::NE, ".head"), // back-edge to the header (join) + pop_epilogue(vec![Reg::R4, Reg::R5, Reg::PC]), + ]; + assert_eq!( + validate_final_allocation(&body), + RaFinalVerdict::Consistent, + "a dominator-defined value read across a loop back-edge must stay \ + available (the universe-init correctness case) — got a false positive" + ); + } }