Skip to content

fix(#288): wire trap_gate onto the runtime path (additive trap backstop) #289

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
avrabe wants to merge 1 commit into
base: main
Choose a base branch
from
Open

fix(#288): wire trap_gate onto the runtime path (additive trap backstop) #289

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
128 changes: 128 additions & 0 deletions loom-core/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down
212 changes: 212 additions & 0 deletions loom-core/src/trap_backstop.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 `<const> <const> <div/rem>` 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 `<const> <const> <div/rem>` 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
}
Loading
Loading