diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index dc0a9c28..a5211b1a 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -2008,9 +2008,14 @@ artifacts: 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` + observable on demand). v0.50: invariant 4 now ALSO runs on the + numeric-branch OPTIMIZED path — a resolved-offset join-CFG builder decodes + BOffset/BCondOffset targets to predecessor indices so the MUST-availability + fixpoint runs there too (6 new `ra003_numeric_*` tests: red across-join + clobber CAUGHT, green both-paths/dominator/loop-back-edge Consistent, + off-boundary + mixed-stream still decline). NotAttempted stays only for + genuinely-unresolvable offsets (decline>guess). 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 diff --git a/crates/synth-synthesis/src/liveness.rs b/crates/synth-synthesis/src/liveness.rs index 7daf4992..454e624b 100644 --- a/crates/synth-synthesis/src/liveness.rs +++ b/crates/synth-synthesis/src/liveness.rs @@ -3924,6 +3924,18 @@ pub fn validate_final_allocation(instrs: &[ArmInstruction]) -> RaFinalVerdict { } // ---- Invariant 4: value availability across a join (phase 2) ---- + if std::env::var_os("SYNTH_RA003_DUMP").is_some() { + let has_num = instrs + .iter() + .any(|i| matches!(i.op, ArmOp::BOffset { .. } | ArmOp::BCondOffset { .. })); + let has_lbl = instrs.iter().any(|i| matches!(i.op, ArmOp::Label { .. })); + if has_num && !has_lbl { + eprintln!("--- RA003 stream (numeric, n={}) ---", instrs.len()); + for (i, ins) in instrs.iter().enumerate() { + eprintln!(" [{i}] {:?}", ins.op); + } + } + } match check_join_availability(instrs) { JoinCheck::Consistent => {} JoinCheck::Violation(v) => return RaFinalVerdict::Violation(v), @@ -4189,6 +4201,15 @@ fn check_join_availability(instrs: &[ArmInstruction]) -> JoinCheck { } for &r in &live_in[b] { if !avail_in[b].contains(&r) { + if std::env::var_os("SYNTH_RA003_DUMP").is_some() { + eprintln!("=== RA003 numeric JOIN violation: reg={r:?} join_block={b} ==="); + for (bi, blk) in blocks.iter().enumerate() { + eprintln!( + " B{bi} [{}..{}) succ={:?} preds={:?} def={:?} live_in={:?} avail_in={:?}", + blk.start, blk.end, blk.succ, preds[bi], def_b[bi], live_in[bi], avail_in[bi] + ); + } + } return JoinCheck::Violation(RaFinalViolation::JoinValueNotAvailable { reg: r, join_block: b, @@ -4200,21 +4221,120 @@ fn check_join_availability(instrs: &[ArmInstruction]) -> JoinCheck { JoinCheck::Consistent } +/// Registers a call defines across the AAPCS boundary (all get fresh values): +/// the caller-saved set. Shared by both JOIN-CFG builders. +const JOIN_CALL_DEFS: [Reg; 5] = [Reg::R0, Reg::R1, Reg::R2, Reg::R3, Reg::R12]; + +/// Given a set of basic blocks over `instrs` (each `[start, end)`) whose `succ` +/// edges are already populated, compute the per-block MUST-def set (`def_b`, +/// with a call's caller-saved def-set folded in) and the backward-liveness +/// live-in set. Shared step 5/6 of both JOIN-CFG builders — CFG-shape-agnostic +/// (it reads only block spans + successors), so the label and numeric paths get +/// bit-identical use/def + liveness computation. +fn join_cfg_livein_defb( + instrs: &[ArmInstruction], + blocks: &[BasicBlock], +) -> (Vec>, Vec>) { + use ArmOp::*; + 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 { + for d in JOIN_CALL_DEFS { + defined.insert(d); + } + } + } + use_b[bi] = used; + def_b[bi] = defined; + } + + // 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; + } + } + } + (live_in, def_b) +} + /// 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. +/// the stream contains a construct the join analysis cannot model. +/// +/// TWO shapes are modeled, chosen by the stream: +/// - **label-form** (`B`/`Bcc`/`Bhs`/`Blo` to a `Label`): the original path, +/// used by the direct/`--relocatable` selector — see [`build_join_cfg_label`]; +/// - **pre-resolved NUMERIC** (`BOffset`/`BCondOffset` with a computed +/// PC-relative halfword displacement, no `Label`): the DEFAULT optimized +/// path — see [`build_join_cfg_numeric`], which reconstructs each branch's +/// target instruction index from the estimator byte layout (the #604/#606 +/// geometry mirror) and builds the CFG from those. +/// +/// A MIXED stream (label-form branches ALONGSIDE numeric ones — the msgq_put +/// trap-guard shape) stays DECLINED (`None`): its two branch families need +/// different target reconstruction and unifying them would guess. `BrTable`, +/// computed `Bx`, `CallIndirect`, and any op with no [`reg_effect`] that is not +/// an admitted terminator likewise decline — never a partial/guessed CFG. #[allow(clippy::type_complexity)] fn build_join_cfg( instrs: &[ArmInstruction], +) -> Option<(Vec, Vec>, Vec>)> { + let has_numeric = instrs + .iter() + .any(|i| matches!(i.op, ArmOp::BOffset { .. } | ArmOp::BCondOffset { .. })); + let has_label = instrs.iter().any(|i| matches!(i.op, ArmOp::Label { .. })); + if has_numeric { + if has_label { + // Mixed label+numeric stream: decline (the two branch families need + // different reconstruction — decline > guess). + return None; + } + return build_join_cfg_numeric(instrs); + } + build_join_cfg_label(instrs) +} + +/// The label-form JOIN-CFG builder (the original `build_join_cfg`, unchanged). +/// `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) declines. +#[allow(clippy::type_complexity)] +fn build_join_cfg_label( + 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 @@ -4339,62 +4459,204 @@ fn build_join_cfg( 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); + // 5+6. Per-block use/def (call def-set folded in) and backward liveness — + // shared with the numeric builder (CFG-shape-agnostic). + let (live_in, def_b) = join_cfg_livein_defb(instrs, &blocks); + + Some((blocks, live_in, def_b)) +} + +/// The pre-resolved NUMERIC JOIN-CFG builder (VCR-RA-003 optimized-path joins). +/// +/// The default (non-`--relocatable`) path resolves branch displacements to +/// byte-accurate halfword offsets INSIDE `optimizer_bridge::ir_to_arm`, leaving +/// `BOffset`/`BCondOffset` in the stream with a computed offset and NO `Label` +/// marking the target — so the label-form CFG builder returned `NotAttempted` +/// for these functions (the "optimized numeric-target path is not covered" +/// hole). This builder reconstructs each numeric branch's TARGET instruction +/// index from the exact same estimator byte layout the #604/#606 geometry +/// helpers use (`target_byte = branch_byte + 4 + 2·offset`, then +/// `partition_point` for the instruction boundary), and builds the CFG from +/// those targets. Then the availability fixpoint runs on the optimized path and +/// the `NotAttempted` verdict becomes a real Consistent/Violation. +/// +/// SOUNDNESS VALVE (decline > guess). Any branch whose reconstructed target does +/// NOT land on an exact instruction boundary — the estimator disagreeing with +/// the encoder for this stream — makes the WHOLE function decline (`None`), +/// exactly like the geometry helper. A `Bl`/`Blx`/`Call` is FALL-THROUGH with a +/// caller-saved def-set (identical to the label builder); `Bx {LR}` is a return +/// SINK; `BrTable`, computed `Bx`, `CallIndirect`, and any op with no +/// [`reg_effect`] that is not an admitted terminator decline. This runs ONLY on +/// no-`Label` numeric streams (the mixed case is declined upstream in +/// [`build_join_cfg`]). +#[allow(clippy::type_complexity)] +fn build_join_cfg_numeric( + instrs: &[ArmInstruction], +) -> Option<(Vec, Vec>, Vec>)> { + use ArmOp::*; + use crate::optimizer_bridge::estimate_arm_byte_size; + + // Numeric-CFG terminator classification. Same policy as the label builder's + // `jclassify`, but the branch families are the NUMERIC ones. `NumTerm` + // carries the reconstructed target INDEX (filled in below), not a label. + enum NTerm { + /// Unconditional numeric branch: single successor at the target index. + Uncond, + /// Conditional numeric branch: target index + fall-through. + Cond, + /// `bl`/`blx`/`call`: returns to the next instruction (fall-through). + Fall, + /// `bx lr`: no successor (function sink). + Return, + /// Genuinely unmodeled control flow → decline the whole function. + Unsupported, + } + fn nclassify(op: &ArmOp) -> NTerm { + use ArmOp::*; + match op { + BOffset { .. } => NTerm::Uncond, + BCondOffset { .. } => NTerm::Cond, + Bx { rm: Reg::LR } => NTerm::Return, + Bl { .. } | Blx { .. } | Call { .. } => NTerm::Fall, + // Label-form branches must not appear here (mixed stream is declined + // upstream); if one somehow does, decline rather than misinterpret. + B { .. } | Bhs { .. } | Blo { .. } | Bcc { .. } | Label { .. } => NTerm::Unsupported, + Bx { .. } | BrTable { .. } | CallIndirect { .. } => NTerm::Unsupported, + _ => NTerm::Fall, + } + } + + let n = instrs.len(); + if n == 0 { + return Some((vec![], vec![], vec![])); + } + + // 1. Admission: every instruction is a numeric branch, an admitted terminator + // (return/call), or a precise-effect op. No `Label` reaches here. + for ins in instrs { + match nclassify(&ins.op) { + NTerm::Unsupported => return None, + NTerm::Uncond | NTerm::Cond | NTerm::Return => {} + NTerm::Fall => { + let is_call = matches!(ins.op, Bl { .. } | Blx { .. } | Call { .. }); + if !is_call && reg_effect(&ins.op).is_none() { + return None; } } } - 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; - } + // 2. Byte layout — the exact mirror of `resolved_branch_geometry_labels_as_zero` + // (`Label` = 0 bytes; there are none here, but keep the arm for parity). + // `byte_offsets[i]` = byte address of instruction `i`; `byte_offsets[n]` = + // total size. + let mut byte_offsets: Vec = Vec::with_capacity(n + 1); + let mut cur: i64 = 0; + for ins in instrs { + byte_offsets.push(cur); + cur += match &ins.op { + Label { .. } => 0, + op => estimate_arm_byte_size(op) as i64, + }; + } + byte_offsets.push(cur); + + // 3. Reconstruct each branch's TARGET instruction index. Off-boundary or + // out-of-range → decline the whole function (estimator/encoder disagree). + // A target index of `n` (branch to function end) is a valid SINK-like + // successor (no block starts there); modeled as "no successor". + let mut branch_target: Vec> = vec![None; n]; + for (i, ins) in instrs.iter().enumerate() { + let offset = match &ins.op { + BOffset { offset } => *offset, + BCondOffset { offset, .. } => *offset, + _ => continue, + }; + let target_byte = byte_offsets[i] + 4 + 2 * offset as i64; + if target_byte < 0 { + return None; // target before function start: unmappable + } + let ti = byte_offsets.partition_point(|&b| b < target_byte); + if byte_offsets.get(ti) != Some(&target_byte) { + return None; // target inside an instruction: unmappable + } + branch_target[i] = Some(ti); // ti may be `n` (function end) + } + + // 4. Leaders: instr 0, every in-range branch target, and the instruction + // after any branch or return (a branch/return ends a block). + let mut is_leader = vec![false; n]; + is_leader[0] = true; + for i in 0..n { + if let Some(ti) = branch_target[i] + && ti < n + { + is_leader[ti] = true; + } + let ends_block = matches!( + nclassify(&instrs[i].op), + NTerm::Uncond | NTerm::Cond | NTerm::Return + ); + if ends_block && i + 1 < n { + is_leader[i + 1] = true; } } + let leaders: Vec = (0..n).filter(|&i| is_leader[i]).collect(); + + // 5. 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(); + + // 6. Successors. A target index maps to the block starting there; a target of + // `n` (function end) yields no successor (sink-like). Because every + // in-range target was made a leader, `block_of_start` must contain it. + 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 nclassify(&instrs[last].op) { + NTerm::Uncond => match branch_target[last] { + Some(ti) if ti < n => vec![*block_of_start.get(&ti)?], + Some(_) => vec![], // branch to function end: sink + None => return None, + }, + NTerm::Cond => { + let mut s = match branch_target[last] { + Some(ti) if ti < n => vec![*block_of_start.get(&ti)?], + Some(_) => vec![], // taken edge exits the function + None => return None, + }; + if let Some(f) = fallthrough + && !s.contains(&f) + { + s.push(f); + } + s + } + NTerm::Return => vec![], // sink + NTerm::Fall => fallthrough.into_iter().collect(), + NTerm::Unsupported => return None, + }; + succs.push(succ); + } + for (b, succ) in blocks.iter_mut().zip(succs) { + b.succ = succ; + } + + // 7. Per-block use/def + backward liveness (shared, CFG-shape-agnostic). + let (live_in, def_b) = join_cfg_livein_defb(instrs, &blocks); Some((blocks, live_in, def_b)) } @@ -14478,4 +14740,301 @@ mod tests { available (the universe-init correctness case) — got a false positive" ); } + + // ================= across-JOIN on the OPTIMIZED (numeric) path ============= + // + // The default (non-`--relocatable`) path pre-resolves branch displacements to + // NUMERIC halfword offsets (`BOffset`/`BCondOffset`, no `Label`). Before this + // lane those functions all returned `NotAttempted` for the join check — the + // "whole-function" guarantee didn't hold on the shipping path. These tests + // exercise `build_join_cfg_numeric`: the RED across-join clobber is now CAUGHT + // (was NotAttempted), the correct allocations stay silent (0 false positives), + // and an off-boundary numeric target still LOUD-declines (`NotAttempted`). + + /// Compute the numeric branch offset (in halfwords) that lands a branch at + /// instruction index `branch_idx` exactly on the leader at index `target_idx`, + /// using the SAME estimator byte layout the reconstruction inverts + /// (`target_byte = branch_byte + 4 + 2·offset`). This makes the fixtures + /// robust to per-op size constants: the test builds the exact offset the + /// production `ir_to_arm` resolution would, so it round-trips through + /// `build_join_cfg_numeric`'s reconstruction. + fn numeric_offset_to(instrs: &[ArmInstruction], branch_idx: usize, target_idx: usize) -> i32 { + use crate::optimizer_bridge::estimate_arm_byte_size; + let byte_of = |idx: usize| -> i64 { + let mut cur: i64 = 0; + for ins in instrs.iter().take(idx) { + cur += match &ins.op { + ArmOp::Label { .. } => 0, + op => estimate_arm_byte_size(op) as i64, + }; + } + cur + }; + let branch_byte = byte_of(branch_idx); + let target_byte = byte_of(target_idx); + // target_byte = branch_byte + 4 + 2·offset ⇒ offset = (target − branch − 4)/2 + let raw = target_byte - branch_byte - 4; + debug_assert_eq!(raw % 2, 0, "target not halfword-aligned to branch"); + (raw / 2) as i32 + } + + /// Build a numeric-path fixture with a two-way split whose join reads a value. + /// `then_def` / `else_def` say which register each arm defines; the join reads + /// R4. When both arms define R4 → Consistent; when only one does → Violation. + /// The BCondOffset conditional is a placeholder (offset patched after layout), + /// as is the unconditional BOffset that skips the else arm. + fn numeric_split_join(then_def: Reg, else_def: Reg) -> Vec { + // Indices: + // 0 push {r4,r5,lr} + // 1 cmp r0,#0 + // 2 bcc EQ -> .else (index 5) [patched] + // 3 mov then_def,#7 (then arm) + // 4 b -> .join (index 6) [patched] + // 5 mov else_def,#9 (else arm; target of the bcc) + // 6 add r0,r4,r4 (join; reads R4) + // 7 pop {r4,r5,pc} + let mut body = vec![ + push_prologue(vec![Reg::R4, Reg::R5, Reg::LR]), + ins(ArmOp::Cmp { + rn: Reg::R0, + op2: Operand2::Imm(0), + }), + ins(ArmOp::BCondOffset { + cond: Condition::EQ, + offset: 0, // patched -> index 5 + }), + movi(then_def, 7), + ins(ArmOp::BOffset { offset: 0 }), // patched -> index 6 + movi(else_def, 9), + add_rr(Reg::R0, Reg::R4, Reg::R4), + pop_epilogue(vec![Reg::R4, Reg::R5, Reg::PC]), + ]; + // Patch the offsets to the exact estimator-derived displacements. + let bcc_off = numeric_offset_to(&body, 2, 5); + if let ArmOp::BCondOffset { offset, .. } = &mut body[2].op { + *offset = bcc_off; + } + let b_off = numeric_offset_to(&body, 4, 6); + if let ArmOp::BOffset { offset } = &mut body[4].op { + *offset = b_off; + } + body + } + + // ---- numeric across-JOIN: RED (clobber caught — was NotAttempted) ---- + #[test] + fn ra003_numeric_red_across_join_clobber_is_caught() { + // Optimized-path analogue of `ra003_red_across_join_clobber_is_caught`: + // the then-arm defines R4 but the else-arm defines R5 (NOT R4); the join + // reads R4 — unavailable on the else edge. On the label path this is a + // Violation; before this lane the NUMERIC path returned NotAttempted. + let body = numeric_split_join(Reg::R4, Reg::R5); + // Sanity: this is a pure-numeric stream (no Label) — the shape the default + // optimized path emits and the label builder declined. + assert!( + !body.iter().any(|i| matches!(i.op, ArmOp::Label { .. })), + "fixture must be pure-numeric (no Label) to exercise the numeric CFG" + ); + assert!( + body.iter() + .any(|i| matches!(i.op, ArmOp::BOffset { .. } | ArmOp::BCondOffset { .. })), + "fixture must contain numeric branches" + ); + let verdict = validate_final_allocation(&body); + assert!( + matches!( + verdict, + RaFinalVerdict::Violation(RaFinalViolation::JoinValueNotAvailable { + reg: Reg::R4, + .. + }) + ), + "a value live into a NUMERIC-path join but undefined on one path MUST \ + be caught (was NotAttempted before optimized-join coverage), got {verdict:?}" + ); + } + + // ---- numeric across-JOIN: GREEN (both paths define → silent) ---- + #[test] + fn ra003_numeric_green_both_paths_define_is_consistent() { + // BOTH arms place the join value in R4 → available on every incoming edge. + // A false positive here would break every real optimized-path diamond. + let body = numeric_split_join(Reg::R4, Reg::R4); + assert_eq!( + validate_final_allocation(&body), + RaFinalVerdict::Consistent, + "a value defined on both numeric-path incoming edges must validate clean" + ); + } + + // ---- numeric across-JOIN: GREEN (dominator-defined survives merge) ---- + #[test] + fn ra003_numeric_green_dominator_defined_is_consistent() { + // R4 is defined in the entry (common dominator) BEFORE the split; neither + // arm touches it. The availability fixpoint must stay SILENT (no false + // positive on dominator-defined) on the numeric CFG just as on the label one. + // 0 push {r4,r5,r6,lr} + // 1 mov r4,#42 (dominator-defines R4) + // 2 cmp r0,#0 + // 3 bcc EQ -> .else (6) [patched] + // 4 mov r5,#1 (then: unrelated) + // 5 b -> .join (7) [patched] + // 6 mov r6,#2 (else: unrelated) + // 7 add r0,r4,r4 (join: reads dominator R4) + // 8 pop {r4,r5,r6,pc} + let mut body = vec![ + push_prologue(vec![Reg::R4, Reg::R5, Reg::R6, Reg::LR]), + movi(Reg::R4, 42), + ins(ArmOp::Cmp { + rn: Reg::R0, + op2: Operand2::Imm(0), + }), + ins(ArmOp::BCondOffset { + cond: Condition::EQ, + offset: 0, + }), + movi(Reg::R5, 1), + ins(ArmOp::BOffset { offset: 0 }), + movi(Reg::R6, 2), + add_rr(Reg::R0, Reg::R4, Reg::R4), + pop_epilogue(vec![Reg::R4, Reg::R5, Reg::R6, Reg::PC]), + ]; + let bcc_off = numeric_offset_to(&body, 3, 6); + if let ArmOp::BCondOffset { offset, .. } = &mut body[3].op { + *offset = bcc_off; + } + let b_off = numeric_offset_to(&body, 5, 7); + if let ArmOp::BOffset { offset } = &mut body[5].op { + *offset = b_off; + } + assert_eq!( + validate_final_allocation(&body), + RaFinalVerdict::Consistent, + "a dominator-defined value must not be flagged at a NUMERIC-path join" + ); + } + + // ---- numeric across-JOIN: GREEN (loop back-edge, universe-init case) ---- + #[test] + fn ra003_numeric_green_loop_back_edge_preserves_availability() { + // The universe-init correctness case on the NUMERIC path: a value (R4) + // defined before a counted loop and read inside the body. The loop header + // is a join of preheader + back-edge (a BACKWARD numeric branch). A + // MAY/empty init would false-positive; the MUST/universe init keeps R4 + // available across the merge → Consistent. + // 0 push {r4,r5,lr} + // 1 mov r4,#7 (dominator-defines R4) + // 2 mov r5,#0 (counter) + // 3 add r0,r4,r4 (.head: reads R4 in body — join leader) + // 4 add r5,r5,r5 + // 5 cmp r5,#0 + // 6 bcc NE -> .head (3) [patched, BACKWARD edge] + // 7 pop {r4,r5,pc} + let mut body = vec![ + push_prologue(vec![Reg::R4, Reg::R5, Reg::LR]), + movi(Reg::R4, 7), + movi(Reg::R5, 0), + add_rr(Reg::R0, Reg::R4, Reg::R4), + add_rr(Reg::R5, Reg::R5, Reg::R5), + ins(ArmOp::Cmp { + rn: Reg::R5, + op2: Operand2::Imm(0), + }), + ins(ArmOp::BCondOffset { + cond: Condition::NE, + offset: 0, + }), + pop_epilogue(vec![Reg::R4, Reg::R5, Reg::PC]), + ]; + let back_off = numeric_offset_to(&body, 6, 3); + if let ArmOp::BCondOffset { offset, .. } = &mut body[6].op { + *offset = back_off; + } + assert!(back_off < 0, "the back-edge must be a negative displacement"); + assert_eq!( + validate_final_allocation(&body), + RaFinalVerdict::Consistent, + "a dominator-defined value across a NUMERIC loop back-edge must stay \ + available (universe-init correctness) — got a false positive" + ); + } + + // ---- numeric across-JOIN: honest decline (off-boundary target) ---- + #[test] + fn ra003_numeric_declines_on_off_boundary_target() { + // A numeric branch whose reconstructed byte target does NOT land on an + // instruction boundary (estimator/encoder disagreement) must LOUD-decline + // to NotAttempted — never guess a CFG. Here `cmp r0,#0` (a 2-byte T1 form) + // straddles a +1-halfword overshoot: branch at index 1, PC = byte 2 + 4 = + // 6; offset 1 ⇒ target byte 8, but instruction boundaries here are at 0 + // (push), 2 (cmp), 4 (bcc), 6 (add), 8 IS a boundary — so pick an offset + // that lands mid-instruction instead. `add_rr` low-reg is 2 bytes; use a + // Movw (4-byte) body op and an odd overshoot into its middle. + // 0 push {r4,lr} (2 or 4 bytes) + // 1 movw r4,#0x1234 (4 bytes, bytes [2..6)) + // 2 bcc EQ, offset (branch) + // 3 add r0,r4,r4 + // 4 pop {r4,pc} + // Choose an offset landing 2 bytes INTO the movw at index 1 (mid-insn). + let body = vec![ + push_prologue(vec![Reg::R4, Reg::LR]), + ins(ArmOp::Movw { + rd: Reg::R4, + imm16: 0x1234, + }), + ins(ArmOp::BCondOffset { + cond: Condition::EQ, + // Target the MIDDLE of the 4-byte movw at index 1. The movw starts + // at some byte B1; the branch PC is (byte-of-branch)+4. We want a + // target 2 bytes into the movw (B1+2), which is not a boundary. + offset: { + use crate::optimizer_bridge::estimate_arm_byte_size; + let push_sz = estimate_arm_byte_size(&ArmOp::Push { + regs: vec![Reg::R4, Reg::LR], + }) as i64; + let movw_start = push_sz; // byte of index 1 + let bcc_byte = push_sz + 4; // byte of index 2 (movw is 4 bytes) + let target = movw_start + 2; // mid-movw: NOT a boundary + (((target - bcc_byte - 4) / 2) as i32).max(-128) + }, + }), + add_rr(Reg::R0, Reg::R4, Reg::R4), + pop_epilogue(vec![Reg::R4, Reg::PC]), + ]; + assert!( + matches!( + validate_final_allocation(&body), + RaFinalVerdict::NotAttempted { .. } + ), + "a numeric branch whose target is off an instruction boundary MUST \ + LOUD-decline (NotAttempted), never guess a CFG" + ); + } + + // ---- numeric across-JOIN: honest decline (mixed label+numeric stream) ---- + #[test] + fn ra003_numeric_declines_on_mixed_label_and_numeric_stream() { + // A stream mixing a label-form branch with a numeric one (the msgq_put + // trap-guard shape) is DECLINED wholesale — the two branch families need + // different target reconstruction; unifying them would guess. NotAttempted. + let body = vec![ + push_prologue(vec![Reg::R4, Reg::LR]), + ins(ArmOp::Cmp { + rn: Reg::R0, + op2: Operand2::Imm(0), + }), + bcc(Condition::EQ, ".skip"), // label-form branch + ins(ArmOp::BOffset { offset: 1 }), // numeric branch in the same stream + label(".skip"), + add_rr(Reg::R0, Reg::R4, Reg::R4), + pop_epilogue(vec![Reg::R4, Reg::PC]), + ]; + assert!( + matches!( + validate_final_allocation(&body), + RaFinalVerdict::NotAttempted { .. } + ), + "a mixed label+numeric stream must LOUD-decline the join check" + ); + } }