diff --git a/loom-core/src/lib.rs b/loom-core/src/lib.rs index 2466acf..1b33da5 100644 --- a/loom-core/src/lib.rs +++ b/loom-core/src/lib.rs @@ -7382,6 +7382,32 @@ pub mod optimize { } } + // #288 — TRAP BACKSTOP (additive; requires the `verification` feature). + // The Z3 translation validator below proves *value* equivalence over a + // TOTAL model — traps are unmodeled, so a div/rem → constant fold that + // dropped a mandatory ÷0 / signed-overflow trap looks value-equal and + // is waved through. The #273 static guard in `rewrite_pure` prevents + // that fold, but this backstop is the independent, certificate-checked + // authority: for every div/rem-on-constants fold that FIRED, ordeal + // must PROVE the op was trap-free. A non-accepted verdict reverts this + // function. This does NOT relax any static guard (behavior is + // unchanged when the guard holds); it only catches a fold the guard + // would have let slip. With `verification` off this block is absent. + #[cfg(feature = "verification")] + { + if !crate::trap_backstop::accept_div_const_folds( + &original_instructions, + &func.instructions, + ) { + eprintln!( + "constant_folding: reverting function (trap backstop rejected a \ + div/rem const-fold — mandatory trap would be dropped; #288/#273)" + ); + crate::stats::record_revert("constant_folding:trap-backstop"); + func.instructions = original_instructions.clone(); + } + } + // Z3 translation validation: prove semantic equivalence. // If verification fails for this function, revert to original // instructions and continue optimizing other functions. @@ -15611,6 +15637,15 @@ pub mod verify; /// hypothesis" machinery that #231 (proof-carrying facts) will reuse. pub mod trap_gate; +/// Runtime wiring of the [`trap_gate`] onto the optimization passes (issue #288). +/// +/// [`trap_gate`]'s transform-checking entry points had zero callers — this +/// module invokes the gate as an additive proof BACKSTOP at each trap-relevant +/// fold site (currently the div/rem → constant fold, #273 class). It sits +/// alongside, never replaces, the per-fold static guards. Compiled out entirely +/// with the `verification` feature off. +pub mod trap_backstop; + /// Swappable solver backend for algebraic rule verification (issue #277). /// /// Defines the backend-neutral term DSL and the `RuleSolver` trait that @@ -20059,6 +20094,99 @@ mod tests { assert!(has_five, "20/4 must fold to 5"); } + // --------------------------------------------------------------------- + // #288 — the trap gate must be ON THE RUNTIME PATH. + // + // These tests FAIL if `trap_backstop` is not wired into a pass: + // 1. A known-safe fold (20/4) still applies BECAUSE the gate ACCEPTS — + // and the gate observably saw exactly one fired fold. + // 2. A constructed trapping fold is BLOCKED by the gate — with the static + // guard bypassed here (we hand the backstop an "optimized" stream where + // the trapping div was folded away), proving the gate, not the static + // guard, is the authority on the runtime path. + // --------------------------------------------------------------------- + + #[cfg(feature = "verification")] + #[test] + fn test_288_backstop_observes_and_accepts_safe_div_fold() { + // The #273 safe-fold fixture: 20 / 4 → 5. The backstop must SEE the fold + // fire (observability) and ACCEPT it (trap-free), so the fold survives. + let original = vec![ + Instruction::I32Const(20), + Instruction::I32Const(4), + Instruction::I32DivS, + ]; + let optimized = vec![Instruction::I32Const(5)]; + + // Observability: the backstop actually saw a fold fire (not vacuous). + assert_eq!( + crate::trap_backstop::fired_div_const_fold_count(&original, &optimized), + 1, + "backstop must observe the 20/4 div fold firing" + ); + // And it ACCEPTS it, because ordeal proves 20/4 cannot trap. + assert!( + crate::trap_backstop::accept_div_const_folds(&original, &optimized), + "backstop must accept the trap-free 20/4 fold" + ); + } + + #[cfg(feature = "verification")] + #[test] + fn test_288_backstop_blocks_trapping_div_fold() { + // Construct the miscompile the static #273 guard is supposed to prevent: + // div_s(INT_MIN, -1) folded to a constant, dropping the overflow trap. + // We hand the backstop an "optimized" stream where the fold DID fire + // (bypassing the static guard, which lives upstream in rewrite_pure). + // The gate — the runtime authority — must REJECT it. + let original = vec![ + Instruction::I32Const(i32::MIN), + Instruction::I32Const(-1), + Instruction::I32DivS, + ]; + let optimized = vec![Instruction::I32Const(i32::MIN)]; // trap dropped! + + assert_eq!( + crate::trap_backstop::fired_div_const_fold_count(&original, &optimized), + 1, + "backstop must observe the trapping fold firing" + ); + assert!( + !crate::trap_backstop::accept_div_const_folds(&original, &optimized), + "backstop MUST block a div_s(INT_MIN,-1) → const fold (overflow trap dropped)" + ); + + // The ÷0 variant must be blocked too. + let div0_orig = vec![ + Instruction::I32Const(7), + Instruction::I32Const(0), + Instruction::I32DivU, + ]; + let div0_opt = vec![Instruction::I32Const(0)]; + assert!( + !crate::trap_backstop::accept_div_const_folds(&div0_orig, &div0_opt), + "backstop MUST block a div_u(7,0) → const fold (÷0 trap dropped)" + ); + } + + #[cfg(feature = "verification")] + #[test] + fn test_288_constant_folding_pass_keeps_safe_fold() { + // End-to-end: the whole `constant_folding` pass, with the backstop on + // its runtime path, still folds a trap-free const div. This is the + // regression guard that the backstop did not over-block. + let wat = r#"(module + (func (export "f") (result i32) + (i32.div_s (i32.const 20) (i32.const 4))))"#; + let mut module = parse::parse_wat(wat).expect("parse"); + optimize::constant_folding(&mut module).expect("fold"); + assert_eq!( + count_div_rem(&module.functions[0].instructions), + 0, + "trap-free const div must still fold with the #288 backstop live" + ); + } + #[test] fn test_273_rem_s_int_min_neg1_folds_to_zero() { // i32.rem_s(INT_MIN,-1) does NOT trap in wasm — the result is 0. diff --git a/loom-core/src/trap_backstop.rs b/loom-core/src/trap_backstop.rs new file mode 100644 index 0000000..b760af2 --- /dev/null +++ b/loom-core/src/trap_backstop.rs @@ -0,0 +1,212 @@ +//! Runtime wiring of the [`crate::trap_gate`] trap-equivalence gate onto the +//! optimization passes (issue #288). +//! +//! # Why this exists +//! +//! [`crate::trap_gate`] (issue #279/#284) is a certificate-checked +//! trap-equivalence oracle, but until #288 its transform-checking entry points +//! had **zero callers** — every trap-relevant fold was guarded only by a +//! hand-written static predicate (#273/#274/#276/#278/#281). Those static guards +//! remain the feature-independent floor and are NOT touched here. This module is +//! purely **additive**: it invokes the gate as a proof BACKSTOP at each +//! trap-relevant fold site, so a fold that slipped past a static guard (or a +//! future guard regression) is caught by a checked `Unsat` certificate before it +//! ships. +//! +//! # The contract +//! +//! Each entry point takes the ORIGINAL and OPTIMIZED instruction stream of one +//! function, detects the trap-relevant folds that FIRED, and returns `true` iff +//! **every** such fold is accepted by the gate (trap-and-value equivalence +//! proven, LRAT certificate re-checked). A `false` return means the pass MUST +//! revert this function to its original instructions. With the `verification` +//! feature OFF this module is compiled out entirely and passes behave exactly as +//! before (byte-identical). +//! +//! # Scope (honest coverage) +//! +//! Wired: the `div_s` / `div_u` / `rem_u` → **constant** fold (#273 class), which +//! is soundly and exactly modelable because the fold's operands are literal +//! constants — ordeal decides the trap condition with no symbolic slack. The gate +//! proves the folded op could not have trapped +//! ([`crate::trap_gate::check_div_discard`]). +//! +//! Documented remaining gaps (static guard is sole authority, see PR #288): +//! - `rem_s` is NOT routed: ordeal's `trap_div` over-approximates it (it shares +//! the `INT_MIN / -1` overflow disjunct with `div_s`, but WASM `rem_s(INT_MIN, +//! -1)` does not trap). Routing it would falsely REJECT a safe fold and revert +//! a valid optimization. Its exact static #273 guard remains sole authority. +//! See `div_meta` and the pinning test in `trap_gate`. +//! - The vacuum `load; drop` discard (#278) already never fires — `is_pure_pusher` +//! excludes loads — so there is no fired fold to back-check at that site; the +//! [`crate::trap_gate::check_mem_transform`] API is exercised by its own unit +//! tests but not on a live fold, because loom carries no symbolic memory bound +//! at the instruction layer to feed it soundly. +//! - The `select(const, a, b)` arm-discard (#281) fold lives in `loom-shared`'s +//! `rewrite_pure`, below the ordeal dependency boundary, and its discarded arm +//! is a *value term* whose trap condition loom does not reconstruct at the +//! instruction layer; modeling it soundly would require lifting arbitrary arm +//! expressions into `BvTerm`s, which is out of scope for this additive +//! backstop. Its static `is_no_trap_expr` guard remains sole authority. + +#![cfg(feature = "verification")] + +use crate::Instruction; +use crate::trap_gate::{DivKind, TrapVerdict, check_div_discard, constant}; + +/// Width + kind of a div/rem instruction, for the trap-gate query. +/// +/// `rem_s` is deliberately EXCLUDED (returns `None`): ordeal's `trap_div` shares +/// the `INT_MIN / -1` signed-overflow disjunct between `div_s` and `rem_s`, but +/// WASM `rem_s(INT_MIN, -1)` does NOT trap (result 0). Routing `rem_s` through +/// the gate would REJECT that genuinely-safe fold and revert a valid +/// optimization — a capability regression. So `rem_s` folds stay on their exact +/// static #273 guard (which folds `rem_s(INT_MIN,-1)` to 0). `div_s`, `div_u`, +/// and `rem_u` ARE modeled exactly by ordeal and are routed. See +/// `trap_gate::tests::rem_s_int_min_is_over_approximated_rejected`. +fn div_meta(instr: &Instruction) -> Option<(DivKind, u32)> { + use Instruction::*; + Some(match instr { + I32DivS => (DivKind::DivS, 32), + I32DivU => (DivKind::DivU, 32), + I32RemU => (DivKind::RemU, 32), + I64DivS => (DivKind::DivS, 64), + I64DivU => (DivKind::DivU, 64), + I64RemU => (DivKind::RemU, 64), + // I32RemS / I64RemS excluded — see doc comment (ordeal over-approximates). + _ => return None, + }) +} + +/// The unsigned bit pattern of an integer constant instruction (width-masked), +/// for feeding the trap-gate as an ordeal `constant`. +fn const_bits(instr: &Instruction) -> Option<(u128, u32)> { + match instr { + Instruction::I32Const(v) => Some(((*v as u32) as u128, 32)), + Instruction::I64Const(v) => Some(((*v as u64) as u128, 64)), + _ => None, + } +} + +/// Count the constant-operand div/rem fold CANDIDATES in a straight-line-or- +/// nested instruction stream: a `
` triple whose two +/// preceding pushers are both constants of the matching width. Recurses into +/// `Block`/`Loop`/`If` bodies. Returns one entry `(kind, width, a_bits, b_bits)` +/// per candidate; ordering is a stable pre-order so two streams can be compared +/// positionally. +fn div_const_fold_candidates(instrs: &[Instruction]) -> Vec<(DivKind, u32, u128, u128)> { + let mut out = Vec::new(); + collect_candidates(instrs, &mut out); + out +} + +fn collect_candidates(instrs: &[Instruction], out: &mut Vec<(DivKind, u32, u128, u128)>) { + for (i, instr) in instrs.iter().enumerate() { + match instr { + Instruction::Block { body, .. } | Instruction::Loop { body, .. } => { + collect_candidates(body, out); + } + Instruction::If { + then_body, + else_body, + .. + } => { + collect_candidates(then_body, out); + collect_candidates(else_body, out); + } + _ => { + if let Some((kind, width)) = div_meta(instr) { + // The two immediately-preceding instructions must be the + // constant operands (postfix order: a, b, op). + if i >= 2 { + if let (Some((a, aw)), Some((b, bw))) = + (const_bits(&instrs[i - 2]), const_bits(&instrs[i - 1])) + { + if aw == width && bw == width { + out.push((kind, width, a, b)); + } + } + } + } + } + } + } +} + +/// Back-check every div/rem → constant fold that FIRED between `original` and +/// `optimized`, using [`crate::trap_gate::check_div_discard`]. +/// +/// A fold is deemed to have FIRED when a `
` candidate +/// present in `original` is no longer present in `optimized` (the pure rewriter +/// replaced it with a single constant). For every such fired fold the gate must +/// prove the op was trap-free; if any is not accepted, this returns `false` and +/// the caller MUST revert the function. +/// +/// Candidates that survive into `optimized` were NOT folded (the static #273 +/// guard held the op in place) and need no proof — the op still traps correctly +/// at runtime. +/// +/// Returns `true` when every fired fold is proven trap-free (or none fired). +pub fn accept_div_const_folds(original: &[Instruction], optimized: &[Instruction]) -> bool { + use std::collections::HashMap; + + let before = div_const_fold_candidates(original); + if before.is_empty() { + return true; // no trap-relevant div/rem fold could have fired + } + let after = div_const_fold_candidates(optimized); + + // Multiset of surviving candidates — a candidate present in `after` was not + // folded. Anything in `before` beyond the `after` count is a FIRED fold. + let mut after_counts: HashMap<(DivKind, u32, u128, u128), usize> = HashMap::new(); + for cand in &after { + *after_counts.entry(*cand).or_insert(0) += 1; + } + + let mut before_counts: HashMap<(DivKind, u32, u128, u128), usize> = HashMap::new(); + for cand in &before { + *before_counts.entry(*cand).or_insert(0) += 1; + } + + for (cand, n_before) in &before_counts { + let n_after = after_counts.get(cand).copied().unwrap_or(0); + if *n_before > n_after { + // At least one instance of this candidate was folded away. PROVE the + // op is trap-free for these (constant) operands; if not, reject. + let (kind, width, a, b) = *cand; + let a_term = constant(a, width); + let b_term = constant(b, width); + let verdict: TrapVerdict = check_div_discard(kind, &a_term, &b_term, width); + if !verdict.is_accepted() { + return false; + } + } + } + true +} + +/// Test-only observability: how many div/rem → constant folds fired between the +/// two streams. Lets the anti-regression test assert the backstop was actually +/// consulted (a fold was seen and checked), not vacuously satisfied. +#[cfg(test)] +pub fn fired_div_const_fold_count(original: &[Instruction], optimized: &[Instruction]) -> usize { + use std::collections::HashMap; + let before = div_const_fold_candidates(original); + let after = div_const_fold_candidates(optimized); + let mut after_counts: HashMap<(DivKind, u32, u128, u128), usize> = HashMap::new(); + for c in &after { + *after_counts.entry(*c).or_insert(0) += 1; + } + let mut before_counts: HashMap<(DivKind, u32, u128, u128), usize> = HashMap::new(); + for c in &before { + *before_counts.entry(*c).or_insert(0) += 1; + } + let mut fired = 0; + for (c, nb) in &before_counts { + let na = after_counts.get(c).copied().unwrap_or(0); + if *nb > na { + fired += nb - na; + } + } + fired +} diff --git a/loom-core/src/trap_gate.rs b/loom-core/src/trap_gate.rs index 6e4fcee..05cb1f6 100644 --- a/loom-core/src/trap_gate.rs +++ b/loom-core/src/trap_gate.rs @@ -180,7 +180,7 @@ pub fn signed_rem_value(a: &BvTerm, b: &BvTerm, width: u32) -> BvTerm { /// The signedness/kind of a div/rem op, mapping loom instructions onto ordeal's /// [`DivOp`] plus the correct **value** builder. -#[derive(Clone, Copy, Debug)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] pub enum DivKind { /// `iN.div_u`. DivU, @@ -285,6 +285,24 @@ pub fn mem_bound_from_pages(pages: &BvTerm, width: u32) -> BvTerm { BvTerm::Mul(bx(pages.clone()), bx(constant(65536, width))) } +/// **Div-is-trap-free** gate for a div/rem → **constant** fold (issue #279 — +/// #273 class). Constant-folding `div_s/div_u/rem_s/rem_u` replaces the op with a +/// literal that carries NO trap, so the fold is sound **only** when the op +/// provably CANNOT trap for these operands. This proves exactly that obligation: +/// `orig.may_trap ⇔ false` — the `÷0` disjunct (all four kinds) and the +/// `INT_MIN / -1` overflow disjunct (signed kinds) are both unsatisfiable. +/// +/// `a`/`b` are the operand `BvTerm`s at the fold site. At a const-fold site they +/// are [`constant`] terms, so ordeal decides the trap condition exactly (no +/// symbolic slack). A folded `div_s(INT_MIN, -1)` (which the #273 static guard +/// already refuses) is caught here as `Sat` (the overflow disjunct holds); a +/// fold of `20 / 4` proves `Unsat` and is accepted. +pub fn check_div_discard(kind: DivKind, a: &BvTerm, b: &BvTerm, width: u32) -> TrapVerdict { + let orig_trap = trap::trap_div(kind.ordeal_op(), a, b, width); + let no_trap = BoolTerm::Ne(bx(constant(0, 8)), bx(constant(0, 8))); // false + verdict_of(prove_trap_condition_equivalence(&orig_trap, &no_trap)) +} + /// **Select-with-trapping-arm** gate (issue #279 — #281 class). WASM `select` is /// *eager*: both value arms are evaluated before the condition picks one, so /// folding `select(const_cond, a, b)` to the taken arm is sound **only** if the @@ -472,6 +490,84 @@ mod tests { } } + // ---- div → constant fold: check_div_discard (trap-free obligation, #273) ---- + + /// A non-trapping constant div (`20 / 4`) proves trap-free ⇒ the const-fold + /// is accepted. This is the ACCEPT half of the #273 backstop. + #[test] + fn div_discard_trap_free_const_is_accepted() { + let a = c(20, 32); + let b = c(4, 32); + let verdict = check_div_discard(DivKind::DivS, &a, &b, 32); + assert!( + verdict.is_accepted(), + "trap-free const div_s(20,4) fold must be accepted, got {verdict:?}" + ); + } + + /// #273: `div_s(INT_MIN, -1)` overflows — the trap is real, so folding it to + /// a constant drops a mandatory trap. `check_div_discard` must REJECT. + #[test] + fn div_discard_int_min_overflow_is_rejected() { + let int_min = c(0x8000_0000, 32); + let neg_one = c(0xFFFF_FFFF, 32); + let verdict = check_div_discard(DivKind::DivS, &int_min, &neg_one, 32); + assert!( + matches!(verdict, TrapVerdict::RejectCounterexample(_)), + "div_s(INT_MIN,-1) const-fold must be rejected (overflow trap), got {verdict:?}" + ); + } + + /// A ÷0 constant div traps — folding it to a constant drops the trap. + /// `check_div_discard` must REJECT. + #[test] + fn div_discard_div_by_zero_is_rejected() { + let a = c(7, 32); + let zero = c(0, 32); + let verdict = check_div_discard(DivKind::DivU, &a, &zero, 32); + assert!( + matches!(verdict, TrapVerdict::RejectCounterexample(_)), + "div_u(7,0) const-fold must be rejected (÷0 trap), got {verdict:?}" + ); + } + + /// `rem_u(7, 0)` traps (÷0) — folding it to a constant drops the trap, so it + /// must be REJECTED. `rem_u` is unsigned so ordeal's `trap_div` models it + /// exactly (÷0 only, no overflow disjunct). + #[test] + fn rem_u_div_by_zero_is_rejected() { + let a = c(7, 32); + let zero = c(0, 32); + let verdict = check_div_discard(DivKind::RemU, &a, &zero, 32); + assert!( + matches!(verdict, TrapVerdict::RejectCounterexample(_)), + "rem_u(7,0) const-fold must be rejected (÷0 trap), got {verdict:?}" + ); + } + + /// KNOWN OVER-APPROXIMATION (documented gap). Per the WASM spec, + /// `rem_s(INT_MIN, -1)` does NOT trap — the result is 0. But ordeal's + /// `trap_div(RemS, …)` shares the signed-overflow disjunct with `div_s`, so + /// it reports this case as TRAPPING. `check_div_discard(RemS, …)` therefore + /// (conservatively, but imprecisely) REJECTS a genuinely-safe `rem_s` + /// overflow fold. Because a REJECT here would revert a valid optimization + /// (a capability regression, not a soundness bug), the #288 backstop + /// deliberately does NOT route `RemS` folds — they stay on their exact + /// static #273 guard. This test PINS that over-approximation so a future + /// ordeal fix (dropping the overflow disjunct for `RemS`) is noticed here + /// and the backstop can then be extended to cover `RemS`. + #[test] + fn rem_s_int_min_is_over_approximated_rejected() { + let int_min = c(0x8000_0000, 32); + let neg_one = c(0xFFFF_FFFF, 32); + let verdict = check_div_discard(DivKind::RemS, &int_min, &neg_one, 32); + assert!( + matches!(verdict, TrapVerdict::RejectCounterexample(_)), + "ordeal over-approximates rem_s(INT_MIN,-1) as trapping (documented \ + gap; backstop must not route RemS), got {verdict:?}" + ); + } + // ---- REJECT: OOB load discard (zero-annihilation, #278) ---- #[test] diff --git a/safety/requirements/verification.yaml b/safety/requirements/verification.yaml index 8906f7f..cc38b95 100644 --- a/safety/requirements/verification.yaml +++ b/safety/requirements/verification.yaml @@ -402,3 +402,55 @@ artifacts: links: - type: verifies target: REQ-18 + + # ============================================================================ + # REQ-1 / REQ-6 — trap_gate must be ON THE RUNTIME PATH (issue #288) + # + # The systemic trap-equivalence gate (trap_gate, issue #279/#284) had ZERO + # callers — its transform-checking entry points were dead code, so trap + # soundness rested entirely on the per-fold STATIC guards. UCA-5 (ISLE folds + # a trapping op to a constant, suppressing the trap; mitigated by CC-4) and + # UCA-21 (Z3 encoding omits the trap condition; mitigated by CC-20) both + # describe exactly the failure the dead gate was meant to catch. #288 wires + # the gate onto the constant_folding runtime path as an additive proof + # BACKSTOP: for every div/rem-on-constants fold that FIRES, ordeal must prove + # the op was trap-free (certificate re-checked) or the fold is reverted. This + # test fails if the gate is not on the runtime path (observability + + # accept/block assertions), which is the whole point of #288. + # ============================================================================ + + - id: TEST-TRAP-GATE-RUNTIME-PATH + type: feature + title: trap_gate wired onto the constant-folding runtime path (#288 backstop) + description: > + Verifies that the trap-equivalence gate (trap_gate) is actually + INVOKED by the constant_folding pass — not dead code (#288). The + backstop (loom_core::trap_backstop) is consulted for every div/rem → + constant fold that fires: a known-safe fold (20/4) is observed AND + accepted by ordeal; a constructed trapping fold (div_s(INT_MIN,-1), + div_u(x,0)) is BLOCKED, with the static guard bypassed in-test so the + gate — not the static guard — is proven to be the runtime authority. + Additive only: no static guard is relaxed. Mitigates UCA-5 (CC-4) and + UCA-21 (CC-20). rem_s is a documented gap (ordeal over-approximates its + overflow trap); it stays on its exact static #273 guard. Runs under the + `verification` feature (default), which pulls in ordeal + Z3. + fields: + method: automated-test + steps: + - run: | + cargo test --release --lib -p loom-core --features verification -- test_288_ trap_gate::tests::div_discard trap_gate::tests::rem + status: verified + tags: [v122, verification, trap-gate, safety] + links: + - type: verifies + target: REQ-1 + - type: verifies + target: REQ-6 + - type: mitigates + target: UCA-5 + - type: mitigates + target: UCA-21 + - type: verifies + target: CC-4 + - type: verifies + target: CC-20