Implement Wasm Validation: Type-Check a Module Before Execution

Topic Overview

Validating Wasm Modules

Browsers refuse to instantiate invalid modules. Validation is a static type and stack check over every function body before execution, catching bad stacks and type mismatches early.

Type and Stack Checking

The validator tracks:

• Operand stack depth and types at each instruction
• Function types against the type section
• Branch targets with matching stack polymorphism rules

Rules mirror the spec: \`i32.add\` requires two \`i32\` values; \`call\` must target a function with compatible params; \`end\` must leave the stack matching the enclosing block signature.

For example, \`i32.add\` with only one \`i32\` on the stack is a validation error, not a runtime surprise.

\`\`\` error: type mismatch at i32.add stack: [i32] (expected [i32 i32]) \`\`\`

Design Notes

Validate before execute on every untrusted module. Browsers depend on this pass for safety; your interpreter should refuse modules that fail stack typing rather than corrupting memory at runtime.

For This Exercise

This exercise asks you to implement a validator for a Wasm subset before your interpreter runs code. You will type-check function bodies and reject modules with impossible stack states.

You will use the same mental model here when reading production interpreter source later in the track. Sketch one concrete input on paper, predict the outcome, then confirm with code. That discipline catches logic errors early and makes debugging far faster when you extend the implementation in follow-on tasks.

Your Task

Implement WebAssembly validation: type-check each function body before it may run, using the algorithm from the spec's appendix. Keep an operand stack of types and a stack of control frames. Each frame records its kind, its result type, the operand-stack height at entry, and whether the rest of the frame is unreachable. After unreachable, br or return, the stack becomes polymorphic: popping below the frame's height yields "any" instead of an error.

Input

;; starts a comment.

cCopy
Loading…

The function's last end closes its body. Instructions:

• Constants: i32.const i64.const (the argument is ignored).
• i32: i32.add sub mul (i32 i32 → i32), i32.eq lt_s (→ i32), i32.eqz (i32 → i32).
• i64: i64.add sub mul (i64 i64 → i64), i64.eq lt_s (i64 i64 → i32), i64.eqz (i64 → i32).
• Conversions: i32.wrap_i64, i64.extend_i32_s.
• Locals: local.get/set/tee I.
• Stack: drop; select (i32 condition, then two operands of the same type).
• Control: nop unreachable block [T] loop [T] if [T] else end br L br_if L return call NAME (calls may refer to later functions).

Rules

• pop(expected): at the frame's height, it yields "any" if the frame is unreachable, or fails with expected T, found nothing. Otherwise it pops, and a mismatch fails with expected T, found U.
• Branches: a branch to a block/if carries its result type, and a branch to a loop carries nothing.
  • br L pops the label's type, then makes the frame unreachable.
  • br_if L pops an i32, pops the label's type, and pushes it back.
  • return pops the function result and makes the frame unreachable.
• unreachable: truncates to the frame's height and marks the frame unreachable.
• block/loop/if T: if first pops an i32. Then a frame opens at the current height.
• else: the then-part must end with exactly its result on the frame. A new frame for the else-part then starts.
• end: pop the frame's result. The stack must be back at the frame's height (N extra value(s) on the stack at end). An if with a result but no else fails with if without else cannot produce a value. The result is then pushed onto the enclosing frame.
• Other errors:
  • unknown local I, unknown label L, unknown function X, unknown instruction X, bad block type X
  • else without matching if, N extra value(s) on the stack at else
  • instructions after the function's end, missing end

Output

One line per function, in order, then a summary:

cCopy
Loading…

The position is the instruction index within the function, starting at 0, followed by the instruction and its argument. Only the first error in each function is reported. Loader messages: line N: bad func, line N: bad func header word X, line N: outside a func.

Example

Input:

cCopy
Loading…

Output:

cCopy
Loading…

Requirements

1. Implement pop with the unreachable rule exactly. Code after unreachable or br must type-check against any operand.
2. Validation is a single pass with no execution. Every decision depends only on the types.

Hidden tests cover if/else with results (and the missing-else case), a mismatched else-branch, polymorphic stacks after unreachable and br, br_if carrying a value, branches with the wrong type, loop labels, unknown labels, forward calls, argument mismatches, select mismatches, and structural errors.