Skip to main content

synth_core/
wasm_stack_check.rs

1//! Pre-flight wasm value-stack underflow detector.
2//!
3//! Real wasm input is validated by the decoder (wasmparser). This module is
4//! a safety net for *direct callers* of the lowering pipeline that feed in
5//! raw `Vec<WasmOp>` without going through the validator — most notably the
6//! fuzz harnesses, which intentionally generate malformed sequences to
7//! prove the contract that lowering returns `Err`, not panics.
8//!
9//! The check is best-effort and, above all, *sound* — it never rejects valid
10//! wasm. Stack effects that depend on data we don't have here (block-result
11//! arities, callee signatures) are handled conservatively:
12//!
13//! * `Call` and unmodeled ops (SIMD, etc.) bail out with `Ok(())` — their
14//!   effect is signature/type dependent.
15//! * The stack-polymorphic terminators `unreachable`/`return`/`br`/`br_table`
16//!   also bail with `Ok(())`: everything after them (up to the enclosing
17//!   `end`) is unreachable and, per the wasm spec, type-checks against an
18//!   infinite-depth polymorphic stack, so depth-only reasoning would produce
19//!   *false* underflows there (issue #329).
20//! * `Block`/`Loop`/`If`/`Else`/`End` are modeled as stack-neutral. In
21//!   reachable code the depth counter can then only ever *over*-count (it
22//!   never pops the `if` condition and never resets at `else`/`end`), so it
23//!   cannot invent an underflow — it just catches fewer of them past a block.
24//!
25//! The net effect: the check reliably rejects the control-flow-free underflow
26//! shapes (the fuzz-harness bug class below) and never false-rejects a
27//! `wasm-tools`-valid module.
28//!
29//! The bug this was written for ([PR #113 fuzz harness wasm_ops_lower_or_error,
30//! input `[I32DivS]` with empty initial stack]) sits squarely inside the
31//! modeled subset, which is the common case.
32//!
33//! ## Scope
34//!
35//! The validator does *not* enforce wasm type checking — it only tracks
36//! stack *depth*. So `i32.const ; i64.add` will pass even though it's
37//! type-invalid. Type errors fall to the lowering pipeline, which now
38//! raises them as `Err` (per PR #117 — the same audit pass).
39//!
40//! ## Why not just call wasmparser?
41//!
42//! Two reasons:
43//! * The lowering pipeline accepts `Vec<WasmOp>` (its own enum), not raw
44//!   wasm bytes. Threading wasmparser back would require a re-encoder.
45//! * The harnesses *want* to feed malformed input. We want a cheap local
46//!   check that returns Err rather than panics, not full re-validation.
47//!
48//! See PR #117 for the original fuzz crash that motivated this module.
49//!
50//! Note: `Select` is modeled as `pop 3, push 1` — wasm's `select` consumes
51//! two values and a condition. `MemoryGrow` pops a page count and pushes
52//! the previous size (or -1). `MemorySize` is a pure push.
53
54use crate::Error;
55use crate::wasm_op::WasmOp;
56
57/// Pre-flight check: returns `Err(Error::validation(...))` if any modeled
58/// op would underflow the wasm value stack. If the sequence contains
59/// control-flow ops we don't model, returns `Ok(())` (bails conservatively).
60pub fn check_no_underflow(wasm_ops: &[WasmOp]) -> crate::Result<()> {
61    let mut depth: i64 = 0;
62    for (idx, op) in wasm_ops.iter().enumerate() {
63        match stack_effect_or_bail(op) {
64            StackEffect::Modeled { pops, pushes } => {
65                if depth < pops as i64 {
66                    return Err(Error::validation(format!(
67                        "wasm value-stack underflow at op {idx} ({op:?}): \
68                         would pop {pops} from depth {depth}"
69                    )));
70                }
71                depth -= pops as i64;
72                depth += pushes as i64;
73            }
74            StackEffect::Bail => return Ok(()),
75        }
76    }
77    Ok(())
78}
79
80enum StackEffect {
81    Modeled { pops: u32, pushes: u32 },
82    Bail,
83}
84
85fn modeled(pops: u32, pushes: u32) -> StackEffect {
86    StackEffect::Modeled { pops, pushes }
87}
88
89#[allow(clippy::too_many_lines)]
90fn stack_effect_or_bail(op: &WasmOp) -> StackEffect {
91    use WasmOp::*;
92    match op {
93        // ---- pushes (constants, reads) -----------------------------------
94        I32Const(_) | I64Const(_) | F32Const(_) | F64Const(_) | V128Const(_) | LocalGet(_)
95        | GlobalGet(_) | MemorySize(_) => modeled(0, 1),
96
97        // ---- i32 binary (pop 2, push 1) ----------------------------------
98        I32Add | I32Sub | I32Mul | I32DivS | I32DivU | I32RemS | I32RemU | I32And | I32Or
99        | I32Xor | I32Shl | I32ShrS | I32ShrU | I32Rotl | I32Rotr | I32Eq | I32Ne | I32LtS
100        | I32LtU | I32LeS | I32LeU | I32GtS | I32GtU | I32GeS | I32GeU => modeled(2, 1),
101
102        // ---- i32 unary (pop 1, push 1) -----------------------------------
103        I32Clz | I32Ctz | I32Popcnt | I32Eqz | I32Extend8S | I32Extend16S | I32WrapI64 => {
104            modeled(1, 1)
105        }
106
107        // ---- i64 binary (pop 2, push 1) ----------------------------------
108        I64Add | I64Sub | I64Mul | I64DivS | I64DivU | I64RemS | I64RemU | I64And | I64Or
109        | I64Xor | I64Shl | I64ShrS | I64ShrU | I64Rotl | I64Rotr | I64Eq | I64Ne | I64LtS
110        | I64LtU | I64LeS | I64LeU | I64GtS | I64GtU | I64GeS | I64GeU => modeled(2, 1),
111
112        // ---- i64 unary (pop 1, push 1) -----------------------------------
113        I64Clz | I64Ctz | I64Popcnt | I64Eqz | I64Extend8S | I64Extend16S | I64Extend32S
114        | I64ExtendI32S | I64ExtendI32U => modeled(1, 1),
115
116        // ---- f32 binary --------------------------------------------------
117        F32Add | F32Sub | F32Mul | F32Div | F32Eq | F32Ne | F32Lt | F32Le | F32Gt | F32Ge
118        | F32Min | F32Max | F32Copysign => modeled(2, 1),
119
120        // ---- f32 unary ---------------------------------------------------
121        F32Abs | F32Neg | F32Ceil | F32Floor | F32Trunc | F32Nearest | F32Sqrt => modeled(1, 1),
122
123        // ---- f64 binary --------------------------------------------------
124        F64Add | F64Sub | F64Mul | F64Div | F64Eq | F64Ne | F64Lt | F64Le | F64Gt | F64Ge
125        | F64Min | F64Max | F64Copysign => modeled(2, 1),
126
127        // ---- f64 unary ---------------------------------------------------
128        F64Abs | F64Neg | F64Ceil | F64Floor | F64Trunc | F64Nearest | F64Sqrt => modeled(1, 1),
129
130        // ---- f32 ↔ f64 / int conversions (pop 1, push 1) -----------------
131        F32ConvertI32S | F32ConvertI32U | F32ConvertI64S | F32ConvertI64U | F32DemoteF64
132        | F32ReinterpretI32 | I32ReinterpretF32 | I32TruncF32S | I32TruncF32U | F64ConvertI32S
133        | F64ConvertI32U | F64ConvertI64S | F64ConvertI64U | F64PromoteF32 | F64ReinterpretI64
134        | I64ReinterpretF64 | I64TruncF64S | I64TruncF64U | I32TruncF64S | I32TruncF64U => {
135            modeled(1, 1)
136        }
137
138        // ---- pop-only ----------------------------------------------------
139        LocalSet(_) | GlobalSet(_) | Drop => modeled(1, 0),
140
141        // ---- pop-modify-push (peek-write) --------------------------------
142        LocalTee(_) => modeled(1, 1),
143
144        // ---- memory ------------------------------------------------------
145        // load: pops address, pushes value
146        I32Load { .. }
147        | I32Load8S { .. }
148        | I32Load8U { .. }
149        | I32Load16S { .. }
150        | I32Load16U { .. }
151        | I64Load { .. }
152        | I64Load8S { .. }
153        | I64Load8U { .. }
154        | I64Load16S { .. }
155        | I64Load16U { .. }
156        | I64Load32S { .. }
157        | I64Load32U { .. }
158        | F32Load { .. }
159        | F64Load { .. } => modeled(1, 1),
160        // store: pops value, pops address
161        I32Store { .. }
162        | I32Store8 { .. }
163        | I32Store16 { .. }
164        | I64Store { .. }
165        | I64Store8 { .. }
166        | I64Store16 { .. }
167        | I64Store32 { .. }
168        | F32Store { .. }
169        | F64Store { .. } => modeled(2, 0),
170        // memory.grow: pops page count, pushes previous size or -1
171        MemoryGrow(_) => modeled(1, 1),
172
173        // ---- bulk memory (#374) -----------------------------------------
174        // memory.copy(dst, src, len) and memory.fill(dst, val, len) each pop
175        // three i32 operands and push nothing.
176        MemoryCopy | MemoryFill => modeled(3, 0),
177
178        // ---- select / nop -----------------------------------------------
179        // select: pops two values and a condition (i32), pushes one value
180        Select => modeled(3, 1),
181        Nop => modeled(0, 0),
182
183        // ---- stack-polymorphic terminators (#329) ------------------------
184        // `unreachable`, `return`, `br`, and `br_table` unconditionally
185        // transfer control, so every op *after* one of them (up to the
186        // enclosing `end`) is unreachable and, per the wasm spec, type-checks
187        // against an infinite-depth *polymorphic* stack. A
188        // `drop`/`select`/`local.set`/binary op in that dead region is
189        // perfectly valid wasm even at depth 0 — but our finite depth counter
190        // keeps decrementing and reports a *false* underflow (issue #329).
191        //
192        // (Note: falcon's original `func_30`/`func_39` underflows were a
193        // *different* root cause — the old #369 silent float-op decoder drop,
194        // which dropped pushes and starved the abstract stack; that was fixed
195        // by #369's loud-skip. This arm closes the remaining, latent
196        // dead-code-after-terminator false-positive in the same model.)
197        //
198        // Note the model can only ever *over*-count in reachable code (it
199        // never pops the `if` condition, never resets at `else`/`end`), so a
200        // false underflow is impossible there. Dead code after a polymorphic
201        // terminator is the sole false-reject class — and without block-result
202        // arities we cannot tell where reachable code resumes after the
203        // matching `end`. So we BAIL to `Ok(())` at the terminator: this keeps
204        // the check SOUND (it can only miss a genuine underflow, never invent
205        // one) and matches the module's documented "accept when unsure" intent.
206        //
207        // This does NOT reintroduce the PR #117 fuzz crashes. Those were
208        // panics deep in `wasm_to_ir`/`ir_to_arm` on shapes like
209        // `[Unreachable, I32GeS]`; the panic sites were since converted to
210        // typed `Err` (issue #93 / PR #101 `get_arm_reg`, issue #121
211        // `slot_stack`, and the `Unreachable`/`Return` handlers in
212        // `wasm_to_ir`). The fuzz contract is *no panic* — `Ok` or `Err` both
213        // pass — and those downstream changes, not this pre-flight, guarantee
214        // it. See the `*_does_not_panic_*` regression tests in synth-synthesis.
215        Unreachable | Return | Br(_) | BrTable { .. } => StackEffect::Bail,
216        // BrIf pops the condition (i32) but does NOT terminate — the
217        // fall-through path keeps executing reachable code. After it the stack
218        // lost the condition, so a genuine depth-0 `br_if` still underflows
219        // (kept as a real-underflow anchor).
220        BrIf(_) => modeled(1, 0),
221        // Block / Loop / If / Else / End — control region delimiters. Their
222        // stack effect depends on block type, which we don't have. Treat as
223        // stack-neutral; if a real underflow lurks past one of these, we
224        // accept it (matches the pre-flight's "best-effort safety net" intent).
225        Block | Loop | If | Else | End => modeled(0, 0),
226        // Call — pops N args, pushes M results. Without the callee's
227        // signature we can't compute this. Yield to upstream validation.
228        Call(_) => StackEffect::Bail,
229
230        // ---- SIMD lane ops, etc. — bail ---------------------------------
231        // The selector doesn't fully support these yet; their stack effects
232        // are well-defined but we don't enumerate them here. Bail.
233        _ => StackEffect::Bail,
234    }
235}
236
237#[cfg(test)]
238mod tests {
239    use super::*;
240
241    #[test]
242    fn binary_op_at_empty_stack_is_underflow() {
243        // This is the exact crash input from PR #113's fuzz harness:
244        // FuzzInput { num_params: 1, ops: [I32DivS] }
245        let err = check_no_underflow(&[WasmOp::I32DivS]).unwrap_err();
246        assert!(matches!(err, Error::ValidationError(_)), "got: {err:?}");
247        let msg = format!("{err}");
248        assert!(msg.contains("underflow"));
249        assert!(msg.contains("I32DivS"));
250    }
251
252    #[test]
253    fn well_formed_add_passes() {
254        let ops = vec![WasmOp::I32Const(1), WasmOp::I32Const(2), WasmOp::I32Add];
255        assert!(check_no_underflow(&ops).is_ok());
256    }
257
258    #[test]
259    fn unary_op_at_empty_stack_is_underflow() {
260        let err = check_no_underflow(&[WasmOp::I32Eqz]).unwrap_err();
261        assert!(matches!(err, Error::ValidationError(_)));
262    }
263
264    #[test]
265    fn drop_at_empty_stack_is_underflow() {
266        let err = check_no_underflow(&[WasmOp::Drop]).unwrap_err();
267        assert!(matches!(err, Error::ValidationError(_)));
268    }
269
270    #[test]
271    fn bulk_memory_pops_three_374() {
272        // memory.copy / memory.fill pop 3, push 0: three pushed operands then the
273        // op must balance to depth 0.
274        for op in [WasmOp::MemoryCopy, WasmOp::MemoryFill] {
275            let ok = vec![
276                WasmOp::I32Const(0),
277                WasmOp::I32Const(0),
278                WasmOp::I32Const(0),
279                op.clone(),
280            ];
281            assert!(check_no_underflow(&ok).is_ok(), "{op:?} with 3 operands");
282            // only two operands -> underflow
283            let bad = vec![WasmOp::I32Const(0), WasmOp::I32Const(0), op.clone()];
284            assert!(
285                matches!(
286                    check_no_underflow(&bad).unwrap_err(),
287                    Error::ValidationError(_)
288                ),
289                "{op:?} with 2 operands must underflow"
290            );
291        }
292    }
293
294    #[test]
295    fn store_at_empty_stack_is_underflow() {
296        let err = check_no_underflow(&[WasmOp::I32Store {
297            offset: 0,
298            align: 2,
299        }])
300        .unwrap_err();
301        assert!(matches!(err, Error::ValidationError(_)));
302    }
303
304    #[test]
305    fn select_needs_three_operands() {
306        // select with only 2 operands underflows.
307        let ops = vec![WasmOp::I32Const(1), WasmOp::I32Const(2), WasmOp::Select];
308        let err = check_no_underflow(&ops).unwrap_err();
309        assert!(matches!(err, Error::ValidationError(_)));
310    }
311
312    #[test]
313    fn select_with_three_operands_passes() {
314        let ops = vec![
315            WasmOp::I32Const(1),
316            WasmOp::I32Const(2),
317            WasmOp::I32Const(0),
318            WasmOp::Select,
319        ];
320        assert!(check_no_underflow(&ops).is_ok());
321    }
322
323    #[test]
324    fn call_bails_conservatively() {
325        // Call(_) has a callee-signature-dependent stack effect we can't
326        // compute here, so we bail (accept). Upstream wasm validation
327        // catches real signature mismatches.
328        let ops = vec![WasmOp::Call(0), WasmOp::I32Add];
329        assert!(check_no_underflow(&ops).is_ok());
330    }
331
332    #[test]
333    fn return_then_binary_op_is_accepted_dead_code_329() {
334        // #329: after `return`, the rest of the block is unreachable and
335        // type-checks against a polymorphic (infinite-depth) stack in wasm, so
336        // `[Return, I64Eqz]` is VALID wasm — the pre-flight must not invent an
337        // underflow. (It previously did, modeling `Return` as stack-neutral.)
338        // The downstream `wasm_to_ir` panic-safety this used to stand in for is
339        // now guaranteed by the `slot_stack`/`get_arm_reg` Err conversions —
340        // see the synth-synthesis `*_does_not_panic_*` regression tests.
341        let ops = vec![WasmOp::Return, WasmOp::I64Eqz];
342        assert!(check_no_underflow(&ops).is_ok());
343    }
344
345    #[test]
346    fn br_then_binary_op_is_accepted_dead_code_329() {
347        // Mirror of the Return case for unconditional branch: code after `br`
348        // is unreachable/polymorphic, hence accepted.
349        let ops = vec![WasmOp::Br(0), WasmOp::I32Add];
350        assert!(check_no_underflow(&ops).is_ok());
351    }
352
353    #[test]
354    fn br_table_then_pop_is_accepted_dead_code_329() {
355        // br_table is also a stack-polymorphic terminator.
356        let ops = vec![
357            WasmOp::BrTable {
358                targets: vec![0],
359                default: 0,
360            },
361            WasmOp::Select,
362        ];
363        assert!(check_no_underflow(&ops).is_ok());
364    }
365
366    #[test]
367    fn br_if_pops_condition() {
368        // BrIf pops one (the i32 condition). At depth 0, the BrIf itself
369        // underflows.
370        let ops = vec![WasmOp::BrIf(0)];
371        let err = check_no_underflow(&ops).unwrap_err();
372        assert!(matches!(err, Error::ValidationError(_)));
373    }
374
375    #[test]
376    fn br_if_with_condition_then_op_is_ok() {
377        // BrIf pops 1 (the condition), then I32Const pushes 1, then
378        // I32Eqz pops 1 / pushes 1 — no underflow.
379        let ops = vec![
380            WasmOp::I32Const(1),
381            WasmOp::BrIf(0),
382            WasmOp::I32Const(0),
383            WasmOp::I32Eqz,
384        ];
385        assert!(check_no_underflow(&ops).is_ok());
386    }
387
388    #[test]
389    fn unreachable_then_binary_op_is_accepted_dead_code_329() {
390        // `[Unreachable, I32GeS]` is VALID wasm: after `unreachable` the stack
391        // is polymorphic, so i32.ge_s type-checks. The pre-flight must accept
392        // it (it previously reported a false underflow). The `wasm_to_ir`
393        // no-panic guarantee this used to proxy for now lives downstream.
394        let ops = vec![WasmOp::Unreachable, WasmOp::I32GeS];
395        assert!(check_no_underflow(&ops).is_ok());
396    }
397
398    #[test]
399    fn unreachable_then_consts_then_binary_op_is_ok() {
400        // Also valid — and accepted whether or not the consts re-push (we bail
401        // at the `unreachable`).
402        let ops = vec![
403            WasmOp::Unreachable,
404            WasmOp::I32Const(1),
405            WasmOp::I32Const(2),
406            WasmOp::I32GeS,
407        ];
408        assert!(check_no_underflow(&ops).is_ok());
409    }
410
411    #[test]
412    fn unreachable_then_drop_is_accepted_329() {
413        // Minimal #329 repro shape: `(unreachable) (drop)` — wasm-tools valid,
414        // previously rejected with "would pop 1 from depth 0".
415        let ops = vec![WasmOp::Unreachable, WasmOp::Drop];
416        assert!(check_no_underflow(&ops).is_ok());
417    }
418
419    #[test]
420    fn return_then_select_is_accepted_329() {
421        // The #329 `func_39` Select shape: a select in dead code after a
422        // terminator. Previously "would pop 3 from depth N".
423        let ops = vec![WasmOp::I32Const(0), WasmOp::Return, WasmOp::Select];
424        assert!(check_no_underflow(&ops).is_ok());
425    }
426
427    #[test]
428    fn return_then_local_set_is_accepted_329() {
429        // The #329 `func_30` LocalSet shape: a local.set in dead code.
430        // Previously "would pop 1 from depth 0".
431        let ops = vec![WasmOp::Return, WasmOp::LocalSet(0)];
432        assert!(check_no_underflow(&ops).is_ok());
433    }
434
435    #[test]
436    fn reachable_select_with_block_result_operand_is_ok_329() {
437        // A reachable select whose operands include a block result stays
438        // accepted — the depth counter over-counts across the block markers,
439        // so it never false-rejects. (Sanity that we didn't over-loosen away
440        // from reachable control flow.)
441        let ops = vec![
442            WasmOp::Block,
443            WasmOp::I32Const(5),
444            WasmOp::End,
445            WasmOp::LocalGet(0),
446            WasmOp::LocalGet(1),
447            WasmOp::Select,
448        ];
449        assert!(check_no_underflow(&ops).is_ok());
450    }
451
452    #[test]
453    fn reachable_binary_op_underflow_still_caught_after_block() {
454        // Bounded-loosening anchor: a genuine underflow that does NOT sit in a
455        // dead region is still caught. `Block` is stack-neutral, then I32Add at
456        // depth 0 underflows.
457        let ops = vec![WasmOp::Block, WasmOp::I32Add];
458        let err = check_no_underflow(&ops).unwrap_err();
459        assert!(matches!(err, Error::ValidationError(_)));
460    }
461
462    #[test]
463    fn const_then_unary_then_binary() {
464        // const → eqz → const → const → add — last add needs 2, has 3.
465        let ops = vec![
466            WasmOp::I32Const(0),
467            WasmOp::I32Eqz,
468            WasmOp::I32Const(1),
469            WasmOp::I32Const(2),
470            WasmOp::I32Add,
471        ];
472        assert!(check_no_underflow(&ops).is_ok());
473    }
474
475    #[test]
476    fn empty_input_is_ok() {
477        assert!(check_no_underflow(&[]).is_ok());
478    }
479}