Module wasm_stack_check 

Pre-flight wasm value-stack underflow detector.

Real wasm input is validated by the decoder (wasmparser). This module is a safety net for direct callers of the lowering pipeline that feed in raw Vec<WasmOp> without going through the validator — most notably the fuzz harnesses, which intentionally generate malformed sequences to prove the contract that lowering returns Err, not panics.

The check is best-effort and, above all, sound — it never rejects valid wasm. Stack effects that depend on data we don’t have here (block-result arities, callee signatures) are handled conservatively:

• Call and unmodeled ops (SIMD, etc.) bail out with Ok(()) — their effect is signature/type dependent.
• The stack-polymorphic terminators unreachable/return/br/br_table also bail with Ok(()): everything after them (up to the enclosing end) is unreachable and, per the wasm spec, type-checks against an infinite-depth polymorphic stack, so depth-only reasoning would produce false underflows there (issue #329).
• Block/Loop/If/Else/End are modeled as stack-neutral. In reachable code the depth counter can then only ever over-count (it never pops the if condition and never resets at else/end), so it cannot invent an underflow — it just catches fewer of them past a block.

The net effect: the check reliably rejects the control-flow-free underflow shapes (the fuzz-harness bug class below) and never false-rejects a wasm-tools-valid module.

The bug this was written for ([PR #113 fuzz harness wasm_ops_lower_or_error, input [I32DivS] with empty initial stack]) sits squarely inside the modeled subset, which is the common case.

Scope

The validator does not enforce wasm type checking — it only tracks stack depth. So i32.const ; i64.add will pass even though it’s type-invalid. Type errors fall to the lowering pipeline, which now raises them as Err (per PR #117 — the same audit pass).

Why not just call wasmparser?

Two reasons:

• The lowering pipeline accepts Vec<WasmOp> (its own enum), not raw wasm bytes. Threading wasmparser back would require a re-encoder.
• The harnesses want to feed malformed input. We want a cheap local check that returns Err rather than panics, not full re-validation.

See PR #117 for the original fuzz crash that motivated this module.

Note: Select is modeled as pop 3, push 1 — wasm’s select consumes two values and a condition. MemoryGrow pops a page count and pushes the previous size (or -1). MemorySize is a pure push.

Functions

check_no_underflow

Pre-flight check: returns Err(Error::validation(...)) if any modeled op would underflow the wasm value stack. If the sequence contains control-flow ops we don’t model, returns Ok(()) (bails conservatively).