diff --git a/claims.yaml b/claims.yaml index 9df90286..5f120b69 100644 --- a/claims.yaml +++ b/claims.yaml @@ -752,9 +752,15 @@ claims: evidence: # The straight-line-expansion ceiling — bumped 4→5 after auditing a 3-reg # 16-bit PUSH/POP in I64Popcnt (1+3=4 cyc/halfword had zero margin). - # #946 re-audit: the priced I64Rotl/I64Rotr fixed-ABI wrappers emit a - # 4-register PUSH {R0-R3} (0xB40F), so 5 holds EXACTLY (1+4), not with - # margin — a 5+-register 16-bit PUSH/POP in a priced arm would exceed it. + # #946 re-audit (two lanes reached this independently): I64Popcnt's + # 3-reg push is NOT the widest one in a priced arm. + # `emit_i64_fixed_abi_entry` emits `0xB40F` = PUSH {R0-R3} (4 regs, + # 1+4 = 5 cyc in 1 halfword — EXACTLY the ceiling) and is reached by the + # PRICED I64Rotl/I64Rotr. So 5 is load-bearing, not merely comfortable: + # at 4 those two arms would have been under-counted. Because it holds + # exactly rather than with margin, a 5+-register 16-bit PUSH/POP in a + # priced arm would exceed it and forces a re-derivation. The pinned + # constant is unchanged; only this rationale was stale. - kind: count-eq pattern: 'const STRAIGHTLINE_CEIL_PER_HALFWORD: u64 = 5;' glob: ['crates/synth-backend/src/wcet.rs'] diff --git a/crates/synth-backend/src/wcet.rs b/crates/synth-backend/src/wcet.rs index 72f635d6..c93d9a96 100644 --- a/crates/synth-backend/src/wcet.rs +++ b/crates/synth-backend/src/wcet.rs @@ -76,22 +76,37 @@ const BL_BLX_CALL_OVERHEAD_CYCLES: u64 = 4; /// - a 32-bit (2-halfword) op — including UMULL/MLA (M3 worst ≈ 5) — is priced at /// 2×5 = 10 ≥ its worst; /// - a 16-bit `PUSH`/`POP` of up to 4 registers is 1+4 = 5 cycles → exactly ≤ 5. -/// The priced arms DO contain 4-register lists: the #610 fixed-ABI wrappers -/// around the priced `I64Rotl`/`I64Rotr` expansions emit `PUSH {R0-R3}` -/// (`0xB40F`, `emit_i64_fixed_abi_entry`) and the matching ≤4-register -/// restore, so the ceiling holds EXACTLY there, with no margin — the bound -/// is still sound, but any future 16-bit `PUSH`/`POP` of 5+ registers in a -/// priced arm would exceed it and must force a re-derivation. /// /// Hardware `SDIV`/`UDIV` (up to 12) do NOT appear in any priced expansion — the /// only i64 division is the looped-expansion decline (it also pushes 4 registers, /// but is never priced here) — so no single instruction /// exceeds the ceiling. 5 cycles/halfword is therefore a sound over-estimate of any /// priced straight-line block; the block executes exactly once in a loop-free -/// function, so summing the ceiling stays sound. Audited against `arm_encoder.rs` -/// (#778, re-audited #946): the 16-bit `PUSH`/`POP`s in priced arms are -/// I64Popcnt's 3-register `0xB438`/`0xBC38` and the I64Rotl/I64Rotr fixed-ABI -/// wrappers' 4-register `PUSH {R0-R3}`/restore. +/// function, so summing the ceiling stays sound. +/// +/// RE-AUDITED against `arm_encoder.rs` (#946), because the previous note was +/// STALE. It claimed "the audited expansions push at most 3 registers, so this +/// holds with margin; the i64 software div/rem, which pushes 4, is a +/// LoopedExpansion decline and is never priced here". The margin does not +/// exist. Enumerating every 16-bit `PUSH`/`POP` and its owning arm: +/// +/// - `I64Popcnt`: `0xB438`/`0xBC38`, 3 registers → 1+3 = 4 ≤ 5. PRICED. +/// - `I64DivU`: `0xB4F0`/`0xBCF0`, 4 registers. `LoopedExpansion` — not priced. +/// - `emit_i64_fixed_abi_entry`: `0xB40F` = `PUSH {R0-R3}`, **4 registers** → +/// 1+4 = 5, EXACTLY the ceiling for its 1 halfword, zero margin. Reached by +/// `I64Rotl` and `I64Rotr`, which ARE priced (`Cycles(straightline_expansion)`) +/// — so a 4-register push does occur in a priced arm, contrary to the old note. +/// Its paired pops (`emit_i64_fixed_abi_exit`) are single-register (2 cycles). +/// +/// The bound is unchanged and still sound — 5 ≥ 5 holds — and this is precisely +/// why the constant had to be 4→5: at 4 the priced `I64Rotl`/`I64Rotr` prologue +/// push would have been UNDER-counted, not merely tight. The claims.yaml pin +/// (`SYNTH-WCET-CYCLE-MODEL`) is on the constant, which does not move. +/// +/// FORWARD CONSTRAINT (kept from the #946 doc sweep, which reached the same +/// conclusion independently): because the ceiling now holds EXACTLY rather +/// than with margin, any future 16-bit `PUSH`/`POP` of 5+ registers in a +/// PRICED arm would exceed it and must force a re-derivation of this constant. const STRAIGHTLINE_CEIL_PER_HALFWORD: u64 = 5; /// Worst-case cycles for a straight-line multi-byte expansion, sized from the diff --git a/crates/synth-backend/src/wcet_loops.rs b/crates/synth-backend/src/wcet_loops.rs index a285813a..210c16df 100644 --- a/crates/synth-backend/src/wcet_loops.rs +++ b/crates/synth-backend/src/wcet_loops.rs @@ -233,8 +233,18 @@ impl WalkState { /// Read a word slot `[sp,#off]`: the value written during this walk, else /// the symbolic entry value `Slot{off,0}`. + /// + /// (#946) A NEGATIVE offset is never tracked. Everything at or above SP is + /// the function's own live frame; everything below is scratch that any + /// interrupt, or any multi-instruction encoder expansion that transiently + /// pushes, may overwrite. Refusing to mint a `Slot` identity below SP is + /// what lets `may_move_sp` answer `false` for the priced expansions that + /// wrap a fixed-register core in `PUSH`/`POP` (`I64Popcnt`, `I64Rotl`, + /// `I64Rotr`): their transient writes land strictly BELOW the incoming SP, + /// so they provably cannot alias any slot this walk tracks. Conservative in + /// one direction only — `Top` can cost a bound, never invent one. fn read_slot(&self, off: i64) -> Sym { - if off % 4 != 0 || self.tainted.contains(&off) { + if off < 0 || off % 4 != 0 || self.tainted.contains(&off) { return Sym::Top; } self.written @@ -244,7 +254,11 @@ impl WalkState { } fn write_slot_word(&mut self, off: i64, v: Sym) { - if off % 4 == 0 { + if off < 0 { + // Below SP — see `read_slot`. Record nothing; taint so a later + // re-base cannot resurrect a value written into scratch space. + self.taint_range(off, 4); + } else if off % 4 == 0 { // A full word store replaces the slot entirely — un-taint. self.tainted.remove(&off); self.written.insert(off, v); @@ -510,7 +524,7 @@ pub(crate) fn analyze_loops( return unproven(hints, &head_offsets); } op => { - if writes_sp(op) { + if may_move_sp(op) { return unproven(hints, &head_offsets); } // A dynamic or non-word-offset SP store inside a region is @@ -1031,15 +1045,44 @@ fn sym_add(a: Sym, b: Sym, sign: i64) -> Sym { } } -/// `writes_sp` — does this op define SP? (Loop regions refuse any SP motion; -/// the function-level walk re-bases on the immediate push/pop/add/sub forms and -/// gives up on anything else.) Exhaustive over every `rd`-carrying op the -/// priced instruction set can contain; multi-instruction encoder expansions -/// never target SP (audited: arithmetic scratch only, I64Popcnt's push/pop is -/// SP-net-zero and it is a whole-function `LoopedExpansion` decline anyway). -fn writes_sp(op: &ArmOp) -> bool { +/// `may_move_sp` — may executing this op change SP, or is its SP effect +/// UNAUDITED? Either way the answer is `true` and the caller gives up. +/// +/// Both call sites use this as a *give-up* predicate: loop regions refuse any SP +/// motion, and the function-level walk re-bases only on the immediate +/// push/pop/add/sub forms. So `true` is the SOUND direction — it can only cost a +/// bound, never invent one — and `false` is the direction that must be EARNED. +/// +/// (#946) EXHAUSTIVE — no wildcard, no bare-identifier catch-all. It previously +/// named 47 of `ArmOp`'s 222 variants and let a `_ => false` absorb the other +/// 175, i.e. it *claimed* exhaustiveness over the priced instruction set while +/// silently answering "does not touch SP" for 79 % of the enum — the same shape +/// as the #615 A32 silent-NOP class. Three of those 175 (`I64Popcnt`, +/// `I64Rotl`, `I64Rotr`) are PRICED by `op_cost`, so they really do reach here, +/// and their encoder expansions really do emit `PUSH`/`POP` — the wildcard's +/// `false` was an UNJUSTIFIED answer, not merely an absent one. It happened to +/// be the right answer, but only because of a property nothing enforced; that +/// property is now a `WalkState` invariant (see the net-zero group below), so +/// the same `false` is now EARNED and the bounds are kept. The wildcard's own +/// doc comment excused `I64Popcnt` as "a whole-function `LoopedExpansion` +/// decline anyway", which was FALSE: `op_cost` prices it `Cycles`. +/// Structurally pinned by `tests/wcet_sp_no_wildcard_946.rs`. +/// +/// REACHABILITY (why the `true` bucket below is behaviourally free): the sole +/// caller of [`analyze_loops`] is `wcet::function_wcet_intermediate`, which runs +/// `scan_for_decline` FIRST. That scan declines every op `op_cost` classifies +/// `Unmodeled` or `LoopedExpansion`, plus indirect/external calls and residual +/// label branches. So a stream that reaches this predicate contains ONLY +/// `OpCost::Cycles` ops and direct calls. The one variant NOT covered by that +/// argument is `ArmOp::Call`: `classify_call` returns `Direct` for it and +/// `continue`s, so it never reaches the `op_cost` check at all. It is +/// unreachable for a different reason — `encode_thumb` REFUSES it with a typed +/// `Err` (#615), so a compile carrying one has already failed. +#[allow(clippy::match_same_arms)] // grouped by REASON, not by answer +fn may_move_sp(op: &ArmOp) -> bool { use ArmOp::*; match op { + // ---- Defines a named destination register: SP iff that register is SP ---- Add { rd, .. } | Sub { rd, .. } | Adds { rd, .. } @@ -1085,8 +1128,253 @@ fn writes_sp(op: &ArmOp) -> bool { | SetCond { rd, .. } | SelectMove { rd, .. } => *rd == Reg::SP, Umull { rdlo, rdhi, .. } => *rdlo == Reg::SP || *rdhi == Reg::SP, + + // ---- PRICED i64 expansions with a register destination (#946) ---- + // Reachable (`op_cost` → `Cycles(straightline_expansion(..))`), so these + // get the SAME precise `rd == SP` test as their i32 counterparts above + // rather than the wildcard's unconditional `false`. `I64Const`/`I64Ldr` + // are the #936 ops: pricing them made them reachable here, where they + // silently inherited the wildcard. + I64SetCond { rd, .. } | I64SetCondZ { rd, .. } | I64Clz { rd, .. } | I64Ctz { rd, .. } => { + *rd == Reg::SP + } + I64Const { rdlo, rdhi, .. } + | I64Ldr { rdlo, rdhi, .. } + | I64Extend8S { rdlo, rdhi, .. } + | I64Extend16S { rdlo, rdhi, .. } + | I64Extend32S { rdlo, rdhi, .. } => *rdlo == Reg::SP || *rdhi == Reg::SP, + I64Mul { rd_lo, rd_hi, .. } + | I64Shl { rd_lo, rd_hi, .. } + | I64ShrU { rd_lo, rd_hi, .. } + | I64ShrS { rd_lo, rd_hi, .. } => *rd_lo == Reg::SP || *rd_hi == Reg::SP, + + // ---- Moves SP outright ---- Push { .. } | Pop { .. } => true, - _ => false, + + // ---- Expansions that transiently PUSH/POP, net-zero — EARNED `false` ---- + // Each of these expands (arm_encoder.rs) to a fixed-register core + // wrapped in a `PUSH`/`POP` pair: `I64Popcnt`'s `0xB438`/`0xBC38`, and + // `I64Rotl`/`I64Rotr`/`I64Div*`/`I64Rem*` via + // `emit_i64_fixed_abi_entry`/`_exit` (`PUSH {R0-R3}` + `STR src,[SP,#-4]!` + // marshalling, then a matching pop/`ADD SP,#4` for all four words). + // + // TWO facts make `false` sound, both checked rather than assumed: + // 1. NET-ZERO: SP is restored exactly before the next op, so no + // tracked offset needs re-basing (verified by reading each arm: + // entry −16−12+12 = −16, exit +16). + // 2. NO ALIASING: the transient writes land strictly BELOW the + // incoming SP, and `read_slot`/`write_slot_word`/`shift_slots` + // refuse to track ANY slot at a negative offset (#946), so nothing + // the walk believes can live in the region these ops scribble on. + // + // Fact 2 used to be an unenforced premise — the walk took `addr.offset` + // raw and signed. It is now an invariant of `WalkState`, which is why + // this arm answers `false` (keeping the bound) instead of declining. + // Weaken those three guards and this answer stops being earned. + I64Popcnt { .. } + | I64Rotl { .. } + | I64Rotr { .. } + | I64DivS { .. } + | I64DivU { .. } + | I64RemS { .. } + | I64RemU { .. } => false, + + // ---- Reachable and provably NOT an SP definition ---- + // Each of these is PRICED, so it really does reach here, and `true` + // would be a live regression: the proven counter lives in an SP-relative + // slot written by `Str`, the exit predicate is `Cmp`, and the region + // closers/exits are `BOffset`/`BCondOffset` — declining any of them + // would decline EVERY proven loop. + // + // - `Cmp`/`Cmn` write flags only, no register. + // - `Str`/`Strb`/`Strh`/`I64Str`: `rd` (`rdlo`/`rdhi`) is the stored + // VALUE, a SOURCE. `MemAddr` has base/offset/offset_reg and NO + // writeback field, so the base register is never updated either. + // - `Label`/`Nop` have no register effect (`op_cost` prices both 0). + // - `Udf` traps. + // - `Bx`/`Bl`/`BOffset`/`BCondOffset` write PC (and `Bl` also LR); an + // AAPCS callee restores SP before returning. NOTE: `Bx` MUST stay + // `false` — `resolve_toplevel_inits` matches its `may_move_sp` guard + // arm BEFORE its `ArmOp::Bx` arm, so a `true` here would silently + // shadow the return handling (no unreachable-pattern warning). + Cmp { .. } + | Cmn { .. } + | Str { .. } + | Strb { .. } + | Strh { .. } + | I64Str { .. } + | Label { .. } + | Nop + | Udf { .. } + | Bx { .. } + | Bl { .. } + | BOffset { .. } + | BCondOffset { .. } => false, + + // ---- Not reachable here — answered `true` (give up), not `false` ---- + // `op_cost` classifies every variant below `Unmodeled` (VFP scalar, MVE + // vector, the i64 pseudo binops/compares/extends, and the off-path + // pseudo-ops `encode_thumb` REFUSES with a typed `Err`) or, for the + // indirect calls and residual label branches, `scan_for_decline` + // declines them outright. `Call` is the one exception to that chain — + // `classify_call` calls it `Direct` and skips the `op_cost` check — but + // `encode_thumb` refuses it too, so it is equally unreachable. Per the + // REACHABILITY note on this function, none can appear in a stream that + // reaches here. They answer `true` rather than `false` deliberately: + // + // 1. SOUNDNESS: `true` is the give-up direction at both call sites, so + // an unaudited op can only cost a bound, never fabricate one. + // 2. FUTURE-PROOFING: #936 priced `I64Const`/`I64Ldr`/`I64Str` and they + // instantly became reachable here, inheriting the wildcard's + // unaudited `false` with nobody revisiting this function. With + // `true` as the default, pricing an op produces a LOUD decline until + // its SP behaviour is consciously audited and moved to a group above. + // 3. TRIPWIRE POTENCY: a re-added `_ => false` flips all 142 of these + // answers, so the #946 behavioural pins can actually fail. A bucket + // of `false`s would make the wildcard behaviourally identical and + // the tripwire vacuous. + MemorySize { .. } + | MemoryGrow { .. } + | B { .. } + | Bhs { .. } + | Blo { .. } + | Bcc { .. } + | Blx { .. } + | Select { .. } + | LocalGet { .. } + | LocalSet { .. } + | LocalTee { .. } + | GlobalGet { .. } + | GlobalSet { .. } + | BrTable { .. } + | Call { .. } + | CallIndirect { .. } + | I64Add { .. } + | I64Sub { .. } + | I64And { .. } + | I64Or { .. } + | I64Xor { .. } + | I64Eqz { .. } + | I64Eq { .. } + | I64Ne { .. } + | I64LtS { .. } + | I64LtU { .. } + | I64LeS { .. } + | I64LeU { .. } + | I64GtS { .. } + | I64GtU { .. } + | I64GeS { .. } + | I64GeU { .. } + | I64ExtendI32S { .. } + | I64ExtendI32U { .. } + | I32WrapI64 { .. } + | F32Add { .. } + | F32Sub { .. } + | F32Mul { .. } + | F32Div { .. } + | F32Abs { .. } + | F32Neg { .. } + | F32Sqrt { .. } + | F32Ceil { .. } + | F32Floor { .. } + | F32Trunc { .. } + | F32Nearest { .. } + | F32Min { .. } + | F32Max { .. } + | F32Copysign { .. } + | F32Eq { .. } + | F32Ne { .. } + | F32Lt { .. } + | F32Le { .. } + | F32Gt { .. } + | F32Ge { .. } + | F32Const { .. } + | F32Load { .. } + | F32Store { .. } + | F32ConvertI32S { .. } + | F32ConvertI32U { .. } + | F32ConvertI64S { .. } + | F32ConvertI64U { .. } + | F32ReinterpretI32 { .. } + | I32ReinterpretF32 { .. } + | I32TruncF32S { .. } + | I32TruncF32U { .. } + | F64Add { .. } + | F64Sub { .. } + | F64Mul { .. } + | F64Div { .. } + | F64Abs { .. } + | F64Neg { .. } + | F64Sqrt { .. } + | F64Ceil { .. } + | F64Floor { .. } + | F64Trunc { .. } + | F64Nearest { .. } + | F64Min { .. } + | F64Max { .. } + | F64Copysign { .. } + | F64Eq { .. } + | F64Ne { .. } + | F64Lt { .. } + | F64Le { .. } + | F64Gt { .. } + | F64Ge { .. } + | F64Const { .. } + | F64Load { .. } + | F64Store { .. } + | F64ConvertI32S { .. } + | F64ConvertI32U { .. } + | F64ConvertI64S { .. } + | F64ConvertI64U { .. } + | F64PromoteF32 { .. } + | F32DemoteF64 { .. } + | F64ReinterpretI64 { .. } + | I64ReinterpretF64 { .. } + | I64TruncF64S { .. } + | I64TruncF64U { .. } + | I32TruncF64S { .. } + | I32TruncF64U { .. } + | MveLoad { .. } + | MveStore { .. } + | MveConst { .. } + | MveAnd { .. } + | MveOrr { .. } + | MveEor { .. } + | MveMvn { .. } + | MveBic { .. } + | MveAddI { .. } + | MveSubI { .. } + | MveMulI { .. } + | MveNegI { .. } + | MveCmpEqI { .. } + | MveCmpNeI { .. } + | MveCmpLtS { .. } + | MveCmpLtU { .. } + | MveCmpGtS { .. } + | MveCmpGtU { .. } + | MveCmpLeS { .. } + | MveCmpLeU { .. } + | MveCmpGeS { .. } + | MveCmpGeU { .. } + | MveDup { .. } + | MveExtractLane { .. } + | MveInsertLane { .. } + | MveAddF32 { .. } + | MveSubF32 { .. } + | MveMulF32 { .. } + | MveNegF32 { .. } + | MveAbsF32 { .. } + | MveCmpEqF32 { .. } + | MveCmpNeF32 { .. } + | MveCmpLtF32 { .. } + | MveCmpLeF32 { .. } + | MveCmpGtF32 { .. } + | MveCmpGeF32 { .. } + | MveDupF32 { .. } + | MveExtractLaneF32 { .. } + | MveReplaceLaneF32 { .. } + | MveDivF32 { .. } + | MveSqrtF32 { .. } => true, } } @@ -1159,7 +1447,10 @@ fn resolve_toplevel_inits(regions: &mut [Region], instrs: &[ArmInstruction]) -> _ => return false, } } - op if writes_sp(op) => return false, // any other SP write — give up + // NOTE: this guard arm is matched BEFORE the `ArmOp::Bx` arm below, + // so `may_move_sp(Bx) == false` is load-bearing — a `true` there + // would shadow the return handling with no compiler warning (#946). + op if may_move_sp(op) => return false, // any other SP motion — give up ArmOp::Bx { .. } => { // A return: nothing after it can be reached by fallthrough, and // all remaining region heads (if any) would be unreachable — @@ -1189,6 +1480,18 @@ fn shift_slots(st: &mut WalkState, delta: i64) { .map(|(&off, &v)| (off + delta, v)) .collect(); st.tainted = st.tainted.iter().map(|&off| off + delta).collect(); + // (#946) A re-base can push a tracked offset BELOW the new SP — an epilogue + // `pop {r4-r7}` shifts by −16. Those words are scratch from here on, so + // drop the remembered value and taint the slot rather than keep believing + // it. This is what makes `read_slot`'s "nothing below SP is ever tracked" + // invariant hold for the WHOLE walk, not just at the moment of the store — + // and it is the invariant `may_move_sp` relies on to answer `false` for the + // priced PUSH/POP-wrapping expansions. Conservative in one direction only. + let below: Vec = st.written.keys().copied().filter(|&o| o < 0).collect(); + for off in below { + st.written.remove(&off); + st.tainted.insert(off); + } // Symbolic Slot{off} identities in registers refer to pre-shift offsets — // drop them (registers holding loaded values stay valid as Const/Top, but a // Slot identity is offset-relative). @@ -1401,6 +1704,226 @@ mod tests { assert_eq!(exit_index(0, 2, &pred(Rel::Eq, 9, 0)), None); } + // ----------------------------------------------------------------------- + // #946 — `may_move_sp` behavioural pins. + // + // The STRUCTURAL half of the tripwire (no wildcard may regrow, every one of + // the 222 `ArmOp` variants must be named) lives in + // `tests/wcet_sp_no_wildcard_946.rs`. These pins are the BEHAVIOURAL half: + // they fix the answers a re-added `_ => false` would change, and the + // reachable answers a careless `_ => true` would change. Both directions + // matter — `true` is the sound/give-up direction, but on a REACHABLE op it + // is a live regression (declining `Str`/`Cmp`/`BOffset` would decline every + // proven loop, since those are what a canonical counted loop is built from). + // ----------------------------------------------------------------------- + + use synth_synthesis::{MemAddr, QReg, VfpReg}; + + /// Ops whose answer is `true` but which a `_ => false` wildcard would have + /// answered `false`. NON-VACUITY: this list must be non-empty, otherwise the + /// wildcard is behaviourally identical to the explicit arms and the tripwire + /// cannot fail. (`Push`/`Pop` are excluded — they were already explicit.) + fn true_but_absorbed_by_a_false_wildcard() -> Vec { + vec![ + // Pre-declined families — `true` is the decline-honest default so a + // future pricing change (cf. #936) gets a loud decline, not a + // silently inherited `false`. + ArmOp::I64Add { + rdlo: Reg::R0, + rdhi: Reg::R1, + rnlo: Reg::R2, + rnhi: Reg::R3, + rmlo: Reg::R4, + rmhi: Reg::R5, + }, + ArmOp::F64Add { + dd: VfpReg::D0, + dn: VfpReg::D1, + dm: VfpReg::D2, + }, + ArmOp::MveAddF32 { + qd: QReg::Q0, + qn: QReg::Q1, + qm: QReg::Q2, + }, + ArmOp::Select { + rd: Reg::R0, + rval1: Reg::R1, + rval2: Reg::R2, + rcond: Reg::R3, + }, + ArmOp::B { + label: "L".to_string(), + }, + ] + } + + #[test] + fn may_move_sp_true_answers_are_not_reproducible_by_a_false_wildcard() { + let ops = true_but_absorbed_by_a_false_wildcard(); + assert!( + !ops.is_empty(), + "non-vacuity: with an empty list a re-added `_ => false` would be \ + behaviourally identical and this tripwire could never fail" + ); + for op in &ops { + assert!( + may_move_sp(op), + "{op:?}: must answer `true`; a `_ => false` wildcard would say `false`" + ); + } + } + + #[test] + fn may_move_sp_true_on_real_sp_definitions() { + // The unconditional stack ops. + assert!(may_move_sp(&ArmOp::Push { + regs: vec![Reg::R4] + })); + assert!(may_move_sp(&ArmOp::Pop { + regs: vec![Reg::R4] + })); + // A destination register that IS SP, across every destination shape. + assert!(may_move_sp(&ArmOp::Add { + rd: Reg::SP, + rn: Reg::SP, + op2: Operand2::Imm(8) + })); + assert!(may_move_sp(&ArmOp::Umull { + rdlo: Reg::SP, + rdhi: Reg::R1, + rn: Reg::R2, + rm: Reg::R3 + })); + // #946: the i64 destination shapes the wildcard used to absorb. + assert!(may_move_sp(&ArmOp::I64Const { + rdlo: Reg::R0, + rdhi: Reg::SP, + value: 1 + })); + assert!(may_move_sp(&ArmOp::I64Mul { + rd_lo: Reg::SP, + rd_hi: Reg::R1, + rn_lo: Reg::R2, + rn_hi: Reg::R3, + rm_lo: Reg::R4, + rm_hi: Reg::R5 + })); + assert!(may_move_sp(&ArmOp::I64Clz { + rd: Reg::SP, + rnlo: Reg::R1, + rnhi: Reg::R2 + })); + } + + #[test] + fn may_move_sp_false_on_the_reachable_counted_loop_vocabulary() { + // These are exactly the ops a canonical counted loop is built from. A + // `true` here would decline EVERY proven loop — the regression a + // blanket "be conservative" sweep would have caused. + let must_be_false = vec![ + // The counter's slot store (`rd` is the stored VALUE, a source; and + // `MemAddr` has no writeback so the SP base is never updated). + ArmOp::Str { + rd: Reg::R0, + addr: MemAddr::imm(Reg::SP, 4), + }, + ArmOp::I64Str { + rdlo: Reg::R0, + rdhi: Reg::R1, + addr: MemAddr::imm(Reg::SP, 8), + }, + // The exit predicate. + ArmOp::Cmp { + rn: Reg::R0, + op2: Operand2::Imm(10), + }, + // The region closer and its exit branch. + ArmOp::BOffset { offset: -6 }, + ArmOp::BCondOffset { + cond: Condition::GE, + offset: 4, + }, + // `Bx` MUST be false: `resolve_toplevel_inits` matches the + // `may_move_sp` guard arm BEFORE its `ArmOp::Bx` arm, so a `true` + // would silently shadow the return handling. + ArmOp::Bx { rm: Reg::LR }, + ArmOp::Bl { + label: "func_1".to_string(), + }, + ArmOp::Label { + name: "L".to_string(), + }, + ArmOp::Nop, + ArmOp::Udf { imm: 0 }, + // A non-SP destination still answers false. + ArmOp::Add { + rd: Reg::R0, + rn: Reg::R1, + op2: Operand2::Imm(1), + }, + ArmOp::I64Const { + rdlo: Reg::R0, + rdhi: Reg::R1, + value: 1, + }, + // The net-zero PUSH/POP group. `false` here is EARNED by the + // `WalkState` non-negative-slot invariant (`read_slot`, + // `write_slot_word`, `shift_slots`), not assumed — see the arm's + // comment. Weaken those guards and this answer must go back to + // `true`, costing the `rot`/`pc` bounds in `wcet_bound_gate.rs`. + ArmOp::I64Popcnt { + rd: Reg::R0, + rnlo: Reg::R1, + rnhi: Reg::R2, + }, + ArmOp::I64Rotl { + rdlo: Reg::R0, + rdhi: Reg::R1, + rnlo: Reg::R2, + rnhi: Reg::R3, + shift: Reg::R4, + }, + ]; + for op in &must_be_false { + assert!( + !may_move_sp(op), + "{op:?}: must answer `false` — it is PRICED (so it really reaches \ + this predicate) and declining it would decline proven loops" + ); + } + } + + /// (#946) The invariant that EARNS `may_move_sp(I64Rotl) == false`: nothing + /// below SP is ever tracked, at store time or after a re-base. Without it, + /// the transient `PUSH {R0-R3}` inside those expansions could alias a slot + /// the walk believes it knows. + #[test] + fn walk_state_never_tracks_a_slot_below_sp() { + let mut st = WalkState::fresh(); + + // A store below SP is not remembered, and reads there are opaque. + st.write_slot_word(-4, Sym::Const(7)); + assert_eq!(st.read_slot(-4), Sym::Top, "a slot below SP must not track"); + assert!(!st.written.contains_key(&-4)); + // ...and no `Slot` identity is ever minted below SP, so it can never + // become a counter candidate. + assert_eq!(st.read_slot(-8), Sym::Top); + + // A normal frame slot tracks as before. + st.write_slot_word(8, Sym::Const(3)); + assert_eq!(st.read_slot(8), Sym::Const(3)); + + // A re-base that pushes it below SP (an epilogue `pop {r4-r7}`) drops + // the remembered value rather than carrying it into scratch space. + shift_slots(&mut st, -16); + assert!( + !st.written.contains_key(&-8), + "a re-based slot that fell below SP must be dropped, not believed" + ); + assert_eq!(st.read_slot(-8), Sym::Top); + } + #[test] fn overflow_wraps_decline() { // init MAX−1, step 2, exit when v ≥ MAX: the walk goes MAX−1 → MAX+1, diff --git a/crates/synth-backend/tests/wcet_sp_no_wildcard_946.rs b/crates/synth-backend/tests/wcet_sp_no_wildcard_946.rs new file mode 100644 index 00000000..60e73657 --- /dev/null +++ b/crates/synth-backend/tests/wcet_sp_no_wildcard_946.rs @@ -0,0 +1,376 @@ +//! #946 tripwire — no catch-all arm regrows in `wcet_loops::may_move_sp`. +//! +//! History of the class: a function that CLAIMS to enumerate a space while a +//! wildcard silently absorbs most of it. #615 was the same shape in the A32 +//! encoder ("encode as NOP for now" arms that became user-reachable silent +//! miscompiles). Here it was `writes_sp`, whose doc asserted it was +//! "exhaustive over every `rd`-carrying op the priced instruction set can +//! contain" while a single `_ => false` answered for **175 of `ArmOp`'s 222 +//! variants** — including three (`I64Popcnt`, `I64Rotl`, `I64Rotr`) that +//! `op_cost` PRICES and whose encoder expansions really do emit `PUSH`/`POP`. +//! Their `false` was right, but for a reason nothing checked; #946 turned that +//! reason into a `WalkState` invariant instead of deleting the bound. +//! +//! `may_move_sp` is a GIVE-UP predicate: `true` declines, `false` lets the +//! analysis proceed. So `false` is the unsound direction, and a wildcard +//! `_ => false` is the worst possible default. +//! +//! This test stops the class from regrowing, structurally: +//! +//! 1. `may_move_sp` is an exhaustive `match` over `ArmOp` with NO wildcard and +//! NO bare-identifier binding arm — a new `ArmOp` variant fails compilation +//! of `wcet_loops.rs` until the author states how SP is affected. +//! 2. Every one of the [`ARM_OP_VARIANT_COUNT`] variant names must appear +//! inside the function body (so an author cannot satisfy (1) by folding +//! variants into a catch-all under a different spelling). +//! 3. The REACHABILITY premise that makes the `true` bucket behaviourally free +//! is pinned too: `op_cost` has no wildcard, `scan_for_decline` runs BEFORE +//! `analyze_loops`, and `analyze_loops` has exactly one call site. +//! +//! The BEHAVIOURAL half (which answers a re-added `_ => false` would flip) +//! lives in `wcet_loops.rs`'s own `#[cfg(test)] mod tests` — `may_move_sp` is +//! private, and it should stay that way. + +/// Bump when adding an `ArmOp` variant — and name it in `may_move_sp`. +/// Deliberately the SAME number the #615 tripwire pins +/// (`a32_no_silent_nop_615.rs`'s `ARM_OP_VARIANT_COUNT`); the two are +/// independent readings of one enum, so they disagree only if one went stale. +const ARM_OP_VARIANT_COUNT: usize = 222; + +const RULES_SRC: &str = include_str!("../../synth-synthesis/src/rules.rs"); +const WCET_LOOPS_SRC: &str = include_str!("../src/wcet_loops.rs"); +const WCET_SRC: &str = include_str!("../src/wcet.rs"); +const WCET_COMPOSE_SRC: &str = include_str!("../src/wcet_compose.rs"); +const WCET_RECURSION_SRC: &str = include_str!("../src/wcet_recursion.rs"); + +// --------------------------------------------------------------------------- +// Source-scanning helpers +// --------------------------------------------------------------------------- + +/// Drop `//`-comments so brace matching and identifier scanning see only code. +/// (Neither scanned region contains a string literal with `//` in it; the +/// `body_is_really_there` assertions below catch it if that ever changes.) +fn without_comments(src: &str) -> String { + src.lines() + .map(|l| l.split("//").next().unwrap_or(l)) + .collect::>() + .join("\n") +} + +/// The full text of the item introduced by `header`, brace-matched. +fn item_after(src: &str, header: &str) -> String { + let start = src + .find(header) + .unwrap_or_else(|| panic!("source scan found no `{header}` — was it renamed? (#946)")); + let rest = &src[start..]; + let (mut depth, mut opened, mut end) = (0i32, false, 0usize); + for (i, c) in rest.char_indices() { + match c { + '{' => { + depth += 1; + opened = true; + } + '}' => { + depth -= 1; + if opened && depth == 0 { + end = i + 1; + break; + } + } + _ => {} + } + } + assert!(end > 0, "unbalanced braces after `{header}` (#946)"); + rest[..end].to_string() +} + +/// Is this trimmed line the head of a match arm that matches ANYTHING — +/// either the `_` wildcard or a bare identifier binding (guarded or not)? +fn is_catch_all_arm(trimmed: &str) -> bool { + let Some((head, _)) = trimmed.split_once("=>") else { + return false; + }; + // Strip a match guard: `op if pred(op) =>` binds everything just as + // `op =>` does, and is how a wildcard usually sneaks back in. + let head = head.split(" if ").next().unwrap_or(head).trim(); + if head == "_" { + return true; + } + !head.is_empty() + && head.chars().all(|c| c.is_ascii_alphanumeric() || c == '_') + && head + .chars() + .next() + .is_some_and(|c| c.is_ascii_lowercase() || c == '_') +} + +/// Every catch-all arm at the TOP level of the `match` opened by `match_header`. +fn catch_all_arms(item: &str, match_header: &str) -> Vec { + let at = item + .find(match_header) + .unwrap_or_else(|| panic!("no `{match_header}` in the scanned item (#946)")); + let rest = &item[at + match_header.len()..]; + let mut depth = 0i32; + let mut found = Vec::new(); + for line in rest.lines() { + let trimmed = line.trim(); + if depth == 0 && is_catch_all_arm(trimmed) { + found.push(trimmed.to_string()); + } + depth += line.matches('{').count() as i32; + depth -= line.matches('}').count() as i32; + if depth < 0 { + break; // closed the match block + } + } + found +} + +/// `needle` occurring as a whole identifier, not as a substring of a longer one +/// (`Add` must not be satisfied by `I64Add` or `F32Add`). +fn contains_ident(hay: &str, needle: &str) -> bool { + let bytes = hay.as_bytes(); + let mut from = 0usize; + while let Some(rel) = hay[from..].find(needle) { + let s = from + rel; + let e = s + needle.len(); + let before_ok = s == 0 || !is_ident_byte(bytes[s - 1]); + let after_ok = e == bytes.len() || !is_ident_byte(bytes[e]); + if before_ok && after_ok { + return true; + } + from = s + 1; + } + false +} + +fn is_ident_byte(b: u8) -> bool { + b.is_ascii_alphanumeric() || b == b'_' +} + +/// Every top-level variant name of `pub enum ArmOp`, read from the real source. +fn arm_op_variants() -> Vec { + let src = without_comments(RULES_SRC); + let body = item_after(&src, "pub enum ArmOp {"); + let inner = &body[body.find('{').unwrap() + 1..]; + let mut depth = 0i32; + let mut names = Vec::new(); + for line in inner.lines() { + let trimmed = line.trim(); + if depth == 0 { + let ident: String = trimmed + .chars() + .take_while(|c| c.is_ascii_alphanumeric() || *c == '_') + .collect(); + if !ident.is_empty() + && ident.starts_with(|c: char| c.is_ascii_uppercase()) + && trimmed[ident.len()..] + .trim_start() + .starts_with(['{', '(', ',', '}']) + { + names.push(ident); + } + } + depth += line.matches('{').count() as i32; + depth -= line.matches('}').count() as i32; + if depth < 0 { + break; + } + } + names +} + +// --------------------------------------------------------------------------- +// Negative controls — prove the scanner can actually go red (gate potency). +// --------------------------------------------------------------------------- + +#[test] +fn scanner_flags_a_wildcard_arm() { + let synthetic = "fn may_move_sp(op: &ArmOp) -> bool {\n\ + \x20 match op {\n\ + \x20 Add { rd, .. } => *rd == Reg::SP,\n\ + \x20 Push { .. } | Pop { .. } => true,\n\ + \x20 _ => false,\n\ + \x20 }\n\ + }"; + let arms = catch_all_arms(synthetic, "match op {"); + assert_eq!( + arms, + vec!["_ => false,".to_string()], + "the scanner must flag a bare `_` arm — otherwise this whole test is vacuous" + ); +} + +#[test] +fn scanner_flags_a_bare_binding_arm() { + // The subtler regrowth: `op => …` and `op if pred(op) => …` bind EVERYTHING + // just as `_` does. `wcet_loops.rs` legitimately uses both shapes elsewhere + // (`resolve_toplevel_inits`), so a `_`-only scan would be bypassable. + let synthetic = "fn may_move_sp(op: &ArmOp) -> bool {\n\ + \x20 match op {\n\ + \x20 Add { rd, .. } => *rd == Reg::SP,\n\ + \x20 op if is_odd(op) => true,\n\ + \x20 op => false,\n\ + \x20 }\n\ + }"; + let arms = catch_all_arms(synthetic, "match op {"); + assert_eq!( + arms.len(), + 2, + "the scanner must flag bare-identifier bindings too, guarded or not; got {arms:?}" + ); +} + +#[test] +fn scanner_does_not_flag_real_variant_arms() { + let synthetic = "fn f(op: &ArmOp) -> bool {\n\ + \x20 match op {\n\ + \x20 Umull { rdlo, rdhi, .. } => *rdlo == Reg::SP || *rdhi == Reg::SP,\n\ + \x20 I64SetCond { rd, .. } | I64Clz { rd, .. } => {\n\ + \x20 *rd == Reg::SP\n\ + \x20 }\n\ + \x20 Cmp { .. } | Nop\n\ + \x20 | Bx { .. } => false,\n\ + \x20 }\n\ + }"; + assert!( + catch_all_arms(synthetic, "match op {").is_empty(), + "false positive: legitimate variant arms must not be read as catch-alls" + ); +} + +// --------------------------------------------------------------------------- +// The tripwire itself +// --------------------------------------------------------------------------- + +#[test] +fn arm_op_variant_count_is_pinned() { + let variants = arm_op_variants(); + let mut unique = variants.clone(); + unique.sort(); + unique.dedup(); + assert_eq!( + unique.len(), + variants.len(), + "duplicate variant names parsed out of `pub enum ArmOp` — the scanner is confused" + ); + assert_eq!( + variants.len(), + ARM_OP_VARIANT_COUNT, + "`ArmOp` variant count changed. Name the new variant(s) in \ + `wcet_loops::may_move_sp` (SP effect audited, not guessed) and bump \ + ARM_OP_VARIANT_COUNT here AND in a32_no_silent_nop_615.rs." + ); +} + +#[test] +fn may_move_sp_has_no_catch_all_arm() { + let src = without_comments(WCET_LOOPS_SRC); + let body = item_after(&src, "fn may_move_sp(op: &ArmOp) -> bool {"); + + // "Count the needle before AND after": a scan over nothing passes silently. + assert!( + body.contains("match op {"), + "extracted `may_move_sp` body has no `match op {{` — the scan found the \ + wrong thing and every assertion below would be vacuous" + ); + + let arms = catch_all_arms(&body, "match op {"); + assert!( + arms.is_empty(), + "#946: `may_move_sp` grew a catch-all arm: {arms:?}\n\ + It is a GIVE-UP predicate — a catch-all `false` silently claims \"this op \ + cannot move SP\" for every variant it absorbs, which is exactly the \ + 175-of-222 hole this tripwire exists to prevent. State the SP effect per \ + variant instead (see the grouped arms and their reasons)." + ); +} + +#[test] +fn may_move_sp_names_every_arm_op_variant() { + let src = without_comments(WCET_LOOPS_SRC); + let body = item_after(&src, "fn may_move_sp(op: &ArmOp) -> bool {"); + let variants = arm_op_variants(); + assert_eq!(variants.len(), ARM_OP_VARIANT_COUNT); + + let missing: Vec<&String> = variants + .iter() + .filter(|v| !contains_ident(&body, v)) + .collect(); + assert!( + missing.is_empty(), + "#946: {} `ArmOp` variant(s) are not named in `may_move_sp`: {:?}\n\ + Exhaustiveness must come from naming every variant, not from a catch-all.", + missing.len(), + missing + ); +} + +// --------------------------------------------------------------------------- +// The reachability premise `may_move_sp`'s `true` bucket rests on. +// +// 145 of the 175 formerly-absorbed variants answer `true` (give up). That is +// behaviourally free ONLY because `op_cost` pre-declines them before the loop +// analysis ever runs. These three pins keep that premise true. +// --------------------------------------------------------------------------- + +#[test] +fn op_cost_still_has_no_catch_all_arm() { + let src = without_comments(WCET_SRC); + let body = item_after(&src, "fn op_cost(op: &ArmOp) -> OpCost {"); + assert!(body.contains("match op {"), "op_cost scan found no match"); + let arms = catch_all_arms(&body, "match op {"); + assert!( + arms.is_empty(), + "`op_cost` grew a catch-all arm: {arms:?} — a new variant would then be \ + silently PRICED or silently declined, and `may_move_sp`'s reachability \ + argument (#946) would no longer hold." + ); +} + +#[test] +fn scan_for_decline_runs_before_analyze_loops() { + let src = without_comments(WCET_SRC); + let body = item_after(&src, "pub fn function_wcet_intermediate("); + let scan = body + .find("scan_for_decline(instrs)") + .expect("no `scan_for_decline(instrs)` call in function_wcet_intermediate (#946)"); + let loops = body + .find("analyze_loops(instrs") + .expect("no `analyze_loops(instrs` call in function_wcet_intermediate (#946)"); + assert!( + scan < loops, + "#946: `analyze_loops` now runs BEFORE `scan_for_decline`. That inverts the \ + premise `may_move_sp` documents: unpriced ops (VFP, MVE, the i64 pseudo \ + family, the off-path pseudo-ops) would reach the loop walk. They answer \ + `true` (decline), so the bound stays SOUND — but every float or vector \ + function silently stops being bounded. Re-audit `may_move_sp` before \ + reordering these." + ); +} + +#[test] +fn analyze_loops_has_exactly_one_call_site() { + let callers = [ + ("wcet.rs", WCET_SRC), + ("wcet_compose.rs", WCET_COMPOSE_SRC), + ("wcet_recursion.rs", WCET_RECURSION_SRC), + ]; + let sites: Vec<(&str, usize)> = callers + .iter() + .map(|(name, src)| { + ( + *name, + without_comments(src).matches("analyze_loops(").count(), + ) + }) + .filter(|(_, n)| *n > 0) + .collect(); + assert_eq!( + sites, + vec![("wcet.rs", 1)], + "#946: `analyze_loops` must have exactly ONE call site \ + (`wcet::function_wcet_intermediate`, gated by `scan_for_decline`). A second \ + entry point would let unpriced ops reach `may_move_sp`; found {sites:?}" + ); +} diff --git a/crates/synth-cli/tests/wcet_bound_gate.rs b/crates/synth-cli/tests/wcet_bound_gate.rs index 5a8773f1..09a3dcab 100644 --- a/crates/synth-cli/tests/wcet_bound_gate.rs +++ b/crates/synth-cli/tests/wcet_bound_gate.rs @@ -520,6 +520,130 @@ fn i64_div_declines_with_looped_expansion_reason() { assert_declined(&report, "d", "looped-expansion"); } +// --------------------------------------------------------------------------- +// #946 — a proven counted loop whose body TRANSIENTLY moves SP stays BOUNDED, +// and the bound is now earned rather than accidental. +// +// `wcet_loops::may_move_sp` (was `writes_sp`) is the predicate both the region +// check and the function-level walk use to refuse SP motion. It named 47 of +// `ArmOp`'s 222 variants and let `_ => false` answer for the other 175 — +// including `I64Popcnt`, `I64Rotl` and `I64Rotr`, which `op_cost` PRICES (so +// they really do reach the walk) and whose encoder expansions really do emit +// `PUSH`/`POP` (`0xB438`/`0xBC38`; `0xB40F` via `emit_i64_fixed_abi_entry`). +// These two fixtures are the shapes that reached the wildcard in practice. +// +// The wildcard's `false` produced the RIGHT numbers for the WRONG reason. The +// push/pop is net-zero across the expansion and writes strictly BELOW the +// incoming SP, so neither the trip count nor the cycle sum is corrupted — but +// that argument needed a premise nothing enforced: that no tracked counter slot +// ever lives at a NEGATIVE offset from SP (the walk took `addr.offset` raw and +// signed). #946 makes it a `WalkState` invariant instead — `read_slot`, +// `write_slot_word` and `shift_slots` all refuse to track below SP — so the +// same `false` is now derived from a checked property. +// +// These therefore pin the EXACT pre-existing bounds (3120 / 4702, trip 8, +// source `static`): the lane must not silently trade Track D coverage for a +// decline, in either direction. Flip `may_move_sp` for those ops, or weaken +// the non-negative-slot guards, and these go red. +// --------------------------------------------------------------------------- + +/// A canonical const-bound counted loop (trip 8) whose body contains an +/// `i64.rotl` — priced, and its expansion pushes `{R0-R3}` transiently. +#[test] +fn proven_loop_containing_i64_rotl_stays_bounded() { + let wat = r#" + (module + (func (export "rot") (param i64) (result i64) + (local i32) (local i64) + (block + (loop + local.get 1 i32.const 8 i32.lt_s i32.eqz br_if 1 + local.get 2 local.get 0 i64.const 3 i64.rotl i64.add local.set 2 + local.get 1 i32.const 1 i32.add local.set 1 + br 0)) + local.get 2)) + "#; + let report = compile_wcet(wat, "cortex-m4"); + assert_sp_motion_loop_bounded(&report, "rot", 3120); +} + +/// Same loop shape with `i64.popcnt` — expansion pushes `{R3,R4,R5}`. +#[test] +fn proven_loop_containing_i64_popcnt_stays_bounded() { + let wat = r#" + (module + (func (export "pc") (param i64) (result i64) + (local i32) (local i64) + (block + (loop + local.get 1 i32.const 8 i32.lt_s i32.eqz br_if 1 + local.get 2 local.get 0 i64.popcnt i64.add local.set 2 + local.get 1 i32.const 1 i32.add local.set 1 + br 0)) + local.get 2)) + "#; + let report = compile_wcet(wat, "cortex-m4"); + assert_sp_motion_loop_bounded(&report, "pc", 4702); +} + +/// CONTROL: the same loop shape with an i64 op whose expansion does NOT touch +/// SP (`i64.and`). It isolates the two fixtures above to SP motion specifically +/// — if all three were to change together, the cause is the loop prover, not +/// `may_move_sp`. +#[test] +fn proven_loop_containing_sp_free_i64_op_is_bounded() { + let wat = r#" + (module + (func (export "andloop") (param i64) (result i64) + (local i32) (local i64) + (block + (loop + local.get 1 i32.const 8 i32.lt_s i32.eqz br_if 1 + local.get 2 local.get 0 i64.const 3 i64.and i64.add local.set 2 + local.get 1 i32.const 1 i32.add local.set 1 + br 0)) + local.get 2)) + "#; + let report = compile_wcet(wat, "cortex-m4"); + let f = func(&report, "andloop"); + assert_eq!( + f.get("status").and_then(Value::as_str), + Some("bounded"), + "the SP-free control must be bounded: {f}" + ); +} + +/// Shared assertion for the two #946 fixtures: bounded, at exactly `cycles`, +/// with the loop statically proven at trip 8. +fn assert_sp_motion_loop_bounded(report: &Value, name: &str, cycles: u64) { + let f = func(report, name); + assert_eq!( + f.get("status").and_then(Value::as_str), + Some("bounded"), + "#946: {name} must stay BOUNDED — `may_move_sp` answers `false` for the \ + net-zero PUSH/POP expansions, earned by the WalkState non-negative-slot \ + invariant. A decline here means that invariant or that arm moved: {f}" + ); + assert_eq!( + f.get("cycles").and_then(Value::as_u64), + Some(cycles), + "#946: {name} bound changed (was {cycles}, the value main emitted before \ + the wildcard was expanded): {f}" + ); + let loops = f.get("loops").and_then(Value::as_array).expect("loops[]"); + assert_eq!(loops.len(), 1, "{name}: expected exactly one proven loop"); + assert_eq!( + loops[0].get("trip_count").and_then(Value::as_u64), + Some(8), + "{name}: trip count must still be the statically proven 8" + ); + assert_eq!( + loops[0].get("source").and_then(Value::as_str), + Some("static"), + "{name}: the trip must be proven statically, not via a hint" + ); +} + // --------------------------------------------------------------------------- // #936 — I64Const/I64Ldr/I64Str are PRICED, not declined. Gale ran // `--emit-wcet` over a real 31-function `gust:os` composite (0.55.0) and