From f398122244f227070853d6295621b5284a168c91 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 13 Aug 2026 21:02:00 +0200 Subject: [PATCH 1/5] fix(#946): expand writes_sp's 175-variant wildcard into explicit arms MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `writes_sp` claimed exhaustiveness over the priced instruction set while a single `_ => false` absorbed 175 of `ArmOp`'s 222 variants — the #615 silent-NOP shape (a function that enumerates a space while a wildcard silently answers for most of it). Measured on origin/main: 222 variants, 47 named, 175 absorbed. Renamed to `may_move_sp` — both call sites use it as a GIVE-UP predicate, so `true` is the sound direction and `false` is what must be earned. The name `writes_sp` could not honestly cover the "unaudited" answers. Classification, by reason rather than by answer: - 30 of the 175 are PRICED by `op_cost`, so they really do reach here. `I64Popcnt`/`I64Rotl`/`I64Rotr` expand to a fixed-register core wrapped in PUSH/POP (`0xB438`/`0xBC38`, `emit_i64_fixed_abi_entry`/`_exit`) — the wildcard's `false` was a WRONG answer, not merely an absent one. They now answer `true`. The old doc comment excused them as "a whole-function LoopedExpansion decline anyway", which was FALSE: `op_cost` prices `I64Popcnt` as `Cycles`. - The i64 ops with a register destination get the same precise `rd == SP` test as their i32 counterparts (`I64Const`/`I64Ldr` are the #936 ops that became reachable here and silently inherited the wildcard). - The reachable counted-loop vocabulary (`Str`/`Cmp`/`BOffset`/ `BCondOffset`/`Bx`/`Bl`/`Label`/`Nop`/`Udf`/`I64Str`) stays `false` with the reason recorded — `true` there would decline EVERY proven loop. - The other 145 are pre-declined by `scan_for_decline` before `analyze_loops` ever runs. They answer `true` so that pricing one later yields a loud decline instead of a silently inherited `false`. Behavioural pins added, including an explicit non-vacuity list of ops whose `true` a re-added `_ => false` would flip. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend/src/wcet_loops.rs | 464 ++++++++++++++++++++++++- 1 file changed, 454 insertions(+), 10 deletions(-) diff --git a/crates/synth-backend/src/wcet_loops.rs b/crates/synth-backend/src/wcet_loops.rs index a285813a..ccb32bed 100644 --- a/crates/synth-backend/src/wcet_loops.rs +++ b/crates/synth-backend/src/wcet_loops.rs @@ -510,7 +510,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 +1031,37 @@ 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 a wrong answer, not merely an absent one. The wildcard's own +/// doc comment asserted `I64Popcnt` "is 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 `BL func_N`/`Call`. +#[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 +1107,241 @@ 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: real stack ops, and expansions that EMIT PUSH/POP ---- + // `Push`/`Pop` obviously. The i64 group is the #946 correction: 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). SP is restored + // net-zero across the whole expansion, but the transient region writes + // BELOW the incoming SP, and the walk tracks slots by raw signed + // `addr.offset` with no non-negativity constraint — so `false` would + // rest on an unenforced "synth never emits a negative SP offset" + // premise. `true` is the answer that needs no premise. The first three + // are PRICED (reachable); the four div/rem are `LoopedExpansion`. Push { .. } | Pop { .. } => true, - _ => false, + I64Popcnt { .. } + | I64Rotl { .. } + | I64Rotr { .. } + | I64DivS { .. } + | I64DivU { .. } + | I64RemS { .. } + | I64RemU { .. } => true, + + // ---- 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. 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 +1414,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 — @@ -1401,6 +1659,192 @@ 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![ + // PRICED (reachable) — expansions that really do emit PUSH/POP. + 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, + }, + // 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, + }, + ]; + 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" + ); + } + } + #[test] fn overflow_wraps_decline() { // init MAX−1, step 2, exit when v ≥ MAX: the walk goes MAX−1 → MAX+1, From 944cfe93987929f56799cacebd7f5626c4e2572c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 14 Aug 2026 06:01:38 +0200 Subject: [PATCH 2/5] test(#946): no-wildcard tripwire for may_move_sp, in the #615 style MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two halves, because either alone is bypassable: STRUCTURAL (tests/wcet_sp_no_wildcard_946.rs) — scans the real source and fails if `may_move_sp` grows a catch-all arm, or if any of the 222 `ArmOp` variants stops being named. The arm scanner rejects bare-identifier bindings (`op =>`, `op if pred(op) =>`) as well as `_ =>`: `wcet_loops.rs` uses both shapes legitimately elsewhere, so a `_`-only scan would be bypassable. ARM_OP_VARIANT_COUNT = 222 is deliberately the same number a32_no_silent_nop_615.rs pins — two independent readings of one enum. BEHAVIOURAL (wcet_loops.rs unit tests) — pins the answers, in both directions: the `true`s a re-added `_ => false` would flip, and the reachable counted-loop vocabulary (`Str`/`Cmp`/`BOffset`/`BCondOffset`/`Bx`) where a careless `_ => true` would decline every proven loop. GATE POTENCY, measured rather than assumed: replacing the 142-line unreachable-bucket arm with `_ => false,` in the real file turns `may_move_sp_has_no_catch_all_arm`, `may_move_sp_names_every_arm_op_variant` (naming all 142) and the non-vacuity behavioural pin RED; restoring it turns them green. The behavioural half only bites because that bucket answers `true` — had it answered `false` to match the old wildcard, the wildcard would be behaviourally identical and that half would be vacuous. Three synthetic negative controls prove the scanner itself can go red, and `may_move_sp_has_no_catch_all_arm` asserts the extracted body really contains `match op {` before scanning it — a scan over nothing passes silently. Also pins the REACHABILITY premise the `true` bucket rests on: `op_cost` has no catch-all, `scan_for_decline` runs before `analyze_loops`, and `analyze_loops` has exactly one call site. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../tests/wcet_sp_no_wildcard_946.rs | 374 ++++++++++++++++++ 1 file changed, 374 insertions(+) create mode 100644 crates/synth-backend/tests/wcet_sp_no_wildcard_946.rs 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..9390002f --- /dev/null +++ b/crates/synth-backend/tests/wcet_sp_no_wildcard_946.rs @@ -0,0 +1,374 @@ +//! #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`. +//! +//! `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:?}" + ); +} From fe0444e90f46ddb67a19e93b1b1be91ae9cce9ca Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 14 Aug 2026 06:03:28 +0200 Subject: [PATCH 3/5] docs(#946): correct a stale PUSH-width audit in the WCET ceiling rationale MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Found while auditing every SP-touching encoder emission for #946. `STRAIGHTLINE_CEIL_PER_HALFWORD`'s doc 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". Enumerating every 16-bit PUSH/POP in arm_encoder.rs and its owning arm: I64Popcnt 0xB438/0xBC38 3 regs PRICED I64DivU 0xB4F0/0xBCF0 4 regs LoopedExpansion (declined) emit_i64_fixed_abi_entry 0xB40F 4 regs PRICED via I64Rotl/I64Rotr So a 4-register push DOES occur in a priced arm: 1+4 = 5 cycles in one halfword, exactly the ceiling, zero margin. The bound is unchanged and still sound (5 >= 5), and the finding strengthens rather than weakens the model — it is precisely why the constant had to go 4->5, since at 4 the priced I64Rotl/I64Rotr prologue push would have been UNDER-counted. The claims.yaml pin is on the constant (`STRAIGHTLINE_CEIL_PER_HALFWORD = 5`), which does not move; only the rationale comment beside it was stale. Ledger still 43/43. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- claims.yaml | 6 ++++++ crates/synth-backend/src/wcet.rs | 28 +++++++++++++++++++++------- 2 files changed, 27 insertions(+), 7 deletions(-) diff --git a/claims.yaml b/claims.yaml index c16f2c1f..6b645777 100644 --- a/claims.yaml +++ b/claims.yaml @@ -752,6 +752,12 @@ 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: 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. 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 461b93c1..7c3e7577 100644 --- a/crates/synth-backend/src/wcet.rs +++ b/crates/synth-backend/src/wcet.rs @@ -75,18 +75,32 @@ const BL_BLX_CALL_OVERHEAD_CYCLES: u64 = 4; /// - a 16-bit (1-halfword) ALU/shift/mov/cmp/forward-branch is ≤ 3 cycles → ≤ 5; /// - 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 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). +/// - a 16-bit `PUSH`/`POP` of up to 4 registers is 1+4 = 5 cycles → exactly ≤ 5. /// /// Hardware `SDIV`/`UDIV` (up to 12) do NOT appear in any priced expansion — the /// only i64 division is the looped-expansion decline — 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): the only 16-bit `PUSH`/`POP` in a priced arm is I64Popcnt's 3-register -/// `0xB438`/`0xBC38`. +/// 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. const STRAIGHTLINE_CEIL_PER_HALFWORD: u64 = 5; /// Worst-case cycles for a straight-line multi-byte expansion, sized from the From 9295497258bd0efcbc4d30a3825336db0f9d7a55 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 14 Aug 2026 06:12:36 +0200 Subject: [PATCH 4/5] =?UTF-8?q?test(#946):=20pin=20the=20SP-motion=20loop?= =?UTF-8?q?=20decline=20=E2=80=94=20the=20LIVE=20half=20of=20the=20wildcar?= =?UTF-8?q?d=20hole?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The 175-variant wildcard was not purely latent. Measured, same two modules, same flags (-t cortex-m4 --emit-wcet), only wcet_loops.rs differing: i64.rotl in a trip-8 counted loop: main BOUNDED 3120 cyc -> now declines i64.popcnt in a trip-8 counted loop: main BOUNDED 4702 cyc -> now declines Both bodies contain a PRICED op whose encoder expansion emits PUSH/POP, and `writes_sp` answered `false` for it via the wildcard. So the misclassification was reachable and reached, on ordinary WASM. Honest about what that does and does not mean: those two bounds were not demonstrably WRONG. 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. They were accidentally sound — resting on an unenforced premise that no tracked counter slot lives at a negative SP offset (the walk tracks slots by raw signed `addr.offset` and never constrains the sign). The answer moved to the sound side rather than staying accidentally right. Coverage cost stated, not hidden: an i64 rotate/popcnt inside an otherwise provable counted loop is no longer bounded. Re-earning it means enforcing the non-negative-slot premise in the walk, not relaxing the predicate. Includes a NON-VACUITY control: the same loop shape with `i64.and` (an i64 op that does not touch SP) must stay BOUNDED, so the two decline assertions cannot be satisfied by a future change that declines every i64 loop. wcet_bound_gate: 44 -> 47 executed tests, all green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-cli/tests/wcet_bound_gate.rs | 94 +++++++++++++++++++++++ 1 file changed, 94 insertions(+) diff --git a/crates/synth-cli/tests/wcet_bound_gate.rs b/crates/synth-cli/tests/wcet_bound_gate.rs index 5a8773f1..44be0654 100644 --- a/crates/synth-cli/tests/wcet_bound_gate.rs +++ b/crates/synth-cli/tests/wcet_bound_gate.rs @@ -520,6 +520,100 @@ fn i64_div_declines_with_looped_expansion_reason() { assert_declined(&report, "d", "looped-expansion"); } +// --------------------------------------------------------------------------- +// #946 — a proven counted loop whose body MOVES SP declines `loop`. +// +// `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`). +// +// This is a LIVE behaviour change, deliberately taken. Before the fix both +// fixtures below came out BOUNDED (`rot` 3120 cyc, `pc` 4702 cyc, trip 8, +// source `static`). Those numbers were not demonstrably WRONG — 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 they rested +// on an unenforced premise: that no tracked counter slot ever lives at a +// NEGATIVE offset from SP (the walk tracks slots by raw signed `addr.offset` +// and does not constrain the sign). An accidentally-correct bound is exactly +// what the decline-honesty posture refuses to ship, so the answer moved to the +// sound side: these shapes now decline, loudly, with a machine reason. +// +// Coverage cost, stated rather than hidden: an i64 rotate or popcnt inside an +// otherwise-provable counted loop is no longer bounded. Re-earning it means +// enforcing the non-negative-slot premise in the walk, not relaxing this +// predicate. Named follow-up. +// --------------------------------------------------------------------------- + +/// A canonical const-bound counted loop (trip 8) whose body contains an +/// `i64.rotl` — priced, but its expansion pushes `{R0-R3}`. +#[test] +fn proven_loop_containing_i64_rotl_declines_on_sp_motion() { + 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_declined(&report, "rot", "loop"); +} + +/// Same loop shape with `i64.popcnt` — expansion pushes `{R3,R4,R5}`. +#[test] +fn proven_loop_containing_i64_popcnt_declines_on_sp_motion() { + 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_declined(&report, "pc", "loop"); +} + +/// NON-VACUITY for the two fixtures above: the SAME loop shape with an i64 op +/// whose expansion does NOT touch SP (`i64.and`) must still be BOUNDED. Without +/// this, a future change that declined every i64 loop — or every loop at all — +/// would leave the two decline assertions green and meaningless. +#[test] +fn proven_loop_containing_sp_free_i64_op_is_still_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 stay bounded, else the #946 decline fixtures \ + above prove nothing about SP specifically: {f}" + ); +} + // --------------------------------------------------------------------------- // #936 — I64Const/I64Ldr/I64Str are PRICED, not declined. Gale ran // `--emit-wcet` over a real 31-function `gust:os` composite (0.55.0) and From 029e5ebbf471aa020c05584da02227fda1be451c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 14 Aug 2026 06:22:21 +0200 Subject: [PATCH 5/5] fix(#946): earn the net-zero PUSH/POP `false` instead of paying for it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Follow-up to the classification commit. The three PRICED expansions that wrap a fixed-register core in PUSH/POP (I64Popcnt, I64Rotl, I64Rotr) were given the conservative `true`, which cost two real bounds. That was the wrong trade: the answer was not undeterminable, it was determinable-but-unenforced. The `false` argument has two parts. NET-ZERO was already verifiable by reading each arm (entry -16-12+12 = -16, exit +16). NO-ALIASING needed a premise the walk did not enforce: that nothing tracked lives at a negative SP offset. It now does — `read_slot` returns Top below SP, `write_slot_word` taints instead of recording, and `shift_slots` drops any entry a re-base pushed below SP (an epilogue `pop {r4-r7}` shifts by -16, so this case is real). All three are conservative in one direction only: Top and taint can cost a bound, never invent one. So the premise is now a WalkState invariant, `false` is derived rather than assumed, and the bounds come back: i64.rotl trip-8 loop: 3120 cycles (identical to main) i64.popcnt trip-8 loop: 4702 cycles (identical to main) Net effect of the lane on emitted bounds: none. The wildcard's answers were right; nothing justified them. Now something does. Gate fixtures rewritten from decline-assertions to EXACT bound pins (3120 / 4702, trip 8, source static) plus an SP-free `i64.and` control, so the lane cannot silently trade Track D coverage in either direction. New unit test `walk_state_never_tracks_a_slot_below_sp` pins the invariant directly. Also corrects the reachability comment: `Call` bypasses the `op_cost` check entirely (`classify_call` returns Direct and continues); it is unreachable because `encode_thumb` refuses it with a typed Err, not because op_cost declines it. The `true` answer is unchanged. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend/src/wcet_loops.rs | 147 ++++++++++++++---- .../tests/wcet_sp_no_wildcard_946.rs | 2 + crates/synth-cli/tests/wcet_bound_gate.rs | 84 ++++++---- 3 files changed, 172 insertions(+), 61 deletions(-) diff --git a/crates/synth-backend/src/wcet_loops.rs b/crates/synth-backend/src/wcet_loops.rs index ccb32bed..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); @@ -1046,8 +1060,11 @@ fn sym_add(a: Sym, b: Sym, sign: i64) -> Sym { /// 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 a wrong answer, not merely an absent one. The wildcard's own -/// doc comment asserted `I64Popcnt` "is a whole-function `LoopedExpansion` +/// `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`. /// @@ -1056,7 +1073,11 @@ fn sym_add(a: Sym, b: Sym, sign: i64) -> Sym { /// `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 `BL func_N`/`Call`. +/// `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::*; @@ -1127,26 +1148,36 @@ fn may_move_sp(op: &ArmOp) -> bool { | I64ShrU { rd_lo, rd_hi, .. } | I64ShrS { rd_lo, rd_hi, .. } => *rd_lo == Reg::SP || *rd_hi == Reg::SP, - // ---- Moves SP: real stack ops, and expansions that EMIT PUSH/POP ---- - // `Push`/`Pop` obviously. The i64 group is the #946 correction: 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). SP is restored - // net-zero across the whole expansion, but the transient region writes - // BELOW the incoming SP, and the walk tracks slots by raw signed - // `addr.offset` with no non-negativity constraint — so `false` would - // rest on an unenforced "synth never emits a negative SP offset" - // premise. `true` is the answer that needs no premise. The first three - // are PRICED (reachable); the four div/rem are `LoopedExpansion`. + // ---- Moves SP outright ---- Push { .. } | Pop { .. } => true, + + // ---- 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 { .. } => true, + | I64RemU { .. } => false, // ---- Reachable and provably NOT an SP definition ---- // Each of these is PRICED, so it really does reach here, and `true` @@ -1185,9 +1216,11 @@ fn may_move_sp(op: &ArmOp) -> bool { // 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. Per the REACHABILITY note on this function, - // none can appear in a stream that reaches here. They answer `true` - // rather than `false` deliberately: + // 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. @@ -1447,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). @@ -1680,19 +1725,6 @@ mod tests { /// cannot fail. (`Push`/`Pop` are excluded — they were already explicit.) fn true_but_absorbed_by_a_false_wildcard() -> Vec { vec![ - // PRICED (reachable) — expansions that really do emit PUSH/POP. - 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, - }, // 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`. @@ -1835,6 +1867,23 @@ mod tests { 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!( @@ -1845,6 +1894,36 @@ mod tests { } } + /// (#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 index 9390002f..60e73657 100644 --- a/crates/synth-backend/tests/wcet_sp_no_wildcard_946.rs +++ b/crates/synth-backend/tests/wcet_sp_no_wildcard_946.rs @@ -8,6 +8,8 @@ //! 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 diff --git a/crates/synth-cli/tests/wcet_bound_gate.rs b/crates/synth-cli/tests/wcet_bound_gate.rs index 44be0654..09a3dcab 100644 --- a/crates/synth-cli/tests/wcet_bound_gate.rs +++ b/crates/synth-cli/tests/wcet_bound_gate.rs @@ -521,7 +521,8 @@ fn i64_div_declines_with_looped_expansion_reason() { } // --------------------------------------------------------------------------- -// #946 — a proven counted loop whose body MOVES SP declines `loop`. +// #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 @@ -529,28 +530,27 @@ fn i64_div_declines_with_looped_expansion_reason() { // 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. // -// This is a LIVE behaviour change, deliberately taken. Before the fix both -// fixtures below came out BOUNDED (`rot` 3120 cyc, `pc` 4702 cyc, trip 8, -// source `static`). Those numbers were not demonstrably WRONG — 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 they rested -// on an unenforced premise: that no tracked counter slot ever lives at a -// NEGATIVE offset from SP (the walk tracks slots by raw signed `addr.offset` -// and does not constrain the sign). An accidentally-correct bound is exactly -// what the decline-honesty posture refuses to ship, so the answer moved to the -// sound side: these shapes now decline, loudly, with a machine reason. +// 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. // -// Coverage cost, stated rather than hidden: an i64 rotate or popcnt inside an -// otherwise-provable counted loop is no longer bounded. Re-earning it means -// enforcing the non-negative-slot premise in the walk, not relaxing this -// predicate. Named follow-up. +// 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, but its expansion pushes `{R0-R3}`. +/// `i64.rotl` — priced, and its expansion pushes `{R0-R3}` transiently. #[test] -fn proven_loop_containing_i64_rotl_declines_on_sp_motion() { +fn proven_loop_containing_i64_rotl_stays_bounded() { let wat = r#" (module (func (export "rot") (param i64) (result i64) @@ -564,12 +564,12 @@ fn proven_loop_containing_i64_rotl_declines_on_sp_motion() { local.get 2)) "#; let report = compile_wcet(wat, "cortex-m4"); - assert_declined(&report, "rot", "loop"); + 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_declines_on_sp_motion() { +fn proven_loop_containing_i64_popcnt_stays_bounded() { let wat = r#" (module (func (export "pc") (param i64) (result i64) @@ -583,15 +583,15 @@ fn proven_loop_containing_i64_popcnt_declines_on_sp_motion() { local.get 2)) "#; let report = compile_wcet(wat, "cortex-m4"); - assert_declined(&report, "pc", "loop"); + assert_sp_motion_loop_bounded(&report, "pc", 4702); } -/// NON-VACUITY for the two fixtures above: the SAME loop shape with an i64 op -/// whose expansion does NOT touch SP (`i64.and`) must still be BOUNDED. Without -/// this, a future change that declined every i64 loop — or every loop at all — -/// would leave the two decline assertions green and meaningless. +/// 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_still_bounded() { +fn proven_loop_containing_sp_free_i64_op_is_bounded() { let wat = r#" (module (func (export "andloop") (param i64) (result i64) @@ -609,8 +609,38 @@ fn proven_loop_containing_sp_free_i64_op_is_still_bounded() { assert_eq!( f.get("status").and_then(Value::as_str), Some("bounded"), - "the SP-free control must stay bounded, else the #946 decline fixtures \ - above prove nothing about SP specifically: {f}" + "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" ); }