Skip to main content

Module wasm_stack_check

synth_core

Module wasm_stack_check 

Source
Expand description

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: control-flow ops (Block, Loop, If/Else, End, Br/BrIf/BrTable, Return, Call) have stack effects that depend on block types and function signatures we don’t have here. When the input contains any such op, validation gracefully bails out with Ok(()) rather than reporting a spurious underflow. This keeps the check conservative — it never rejects valid input — at the cost of catching only the underflow cases that don’t involve control flow.

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).