wasm_validate_code (wasm v0.1.0)
View SourceFunction body validation. Read this when a module you believe is well typed is being rejected.
This is the specification's abstract type-checking algorithm: an operand
stack of value types and a control stack of open blocks, with the operand
stack becoming polymorphic after unreachable or an unconditional branch.
The polymorphic rule is the part worth stating explicitly, because it is
where validators go wrong in both directions. After br, the rest of the
block is statically unreachable and may pop values that are not there:
(func (result i32) (unreachable) (i32.add)) ;; validi32.add pops two operands from an empty stack. Rejecting this wrongly
refuses legal modules that every real compiler emits. Conversely, treating
unreachable code as unchecked wrongly accepts modules whose reachable
continuation is ill-typed. The frame's height plus its unreachable flag
is what distinguishes the two: popping below the height yields unknown
(which unifies with anything) rather than either failing or being skipped.
Because the decoder produces a nested AST rather than a flat stream, blocks
recurse here instead of pushing and popping through end opcodes. The
typing rules are identical; only the traversal differs.
Summary
Functions
Validate a constant expression and check it yields Expected.
Validate one function body against its declared type, and return it annotated.
Direction, value type and natural alignment (log2 bytes) of an access.
Whether A is usable where B is expected.
Types
-type annotated() :: {Height :: non_neg_integer(), instr()} | {Height :: non_neg_integer(), Base :: non_neg_integer(), instr()}.
-type heaptype() :: func | extern | exn | any | eq | i31 | struct | array | nofunc | noextern | noexn | none | {type, typeidx()}.
-type numtype() :: i32 | i64 | f32 | f64.
-type reftype() :: {ref, null | nonull, heaptype()}.
-type typeidx() :: non_neg_integer().
-type vectype() :: v128.
Functions
-spec const_expr([instr()], valtype(), #ctx{types :: tuple(), canon :: tuple(), fields :: tuple(), kinds :: tuple(), supers :: tuple(), funcs :: tuple(), tables :: tuple(), mems :: tuple(), globals :: tuple(), tags :: tuple(), elems :: tuple(), n_datas :: non_neg_integer(), n_imported_globals :: non_neg_integer(), refs :: #{non_neg_integer() => true}, shared_globals :: #{non_neg_integer() => true}, shared_mems :: #{non_neg_integer() => true}, locals :: tuple(), results :: [valtype()]}) -> ok.
Validate a constant expression and check it yields Expected.
Constant expressions are a small pure sublanguage: literals, null and function references, reads of immutable globals already in scope, and (from the extended-const proposal, now part of the specification) integer add, sub and mul.
Two restrictions carry weight. global.get may only read an immutable
global that is already defined, which is what keeps initialisation order
unobservable and the result deterministic. And ref.func may only name a
declared function, so a module cannot fabricate a reference to a function
the embedder never exposed.
The caller controls which globals are in scope by passing a context whose global space is truncated to the visible prefix, so the same code serves global initialisers (which see only earlier globals) and segment offsets (which see all of them).
-spec function(#ctx{types :: tuple(), canon :: tuple(), fields :: tuple(), kinds :: tuple(), supers :: tuple(), funcs :: tuple(), tables :: tuple(), mems :: tuple(), globals :: tuple(), tags :: tuple(), elems :: tuple(), n_datas :: non_neg_integer(), n_imported_globals :: non_neg_integer(), refs :: #{non_neg_integer() => true}, shared_globals :: #{non_neg_integer() => true}, shared_mems :: #{non_neg_integer() => true}, locals :: tuple(), results :: [valtype()]}, #functype{params :: [valtype()], results :: [valtype()]}, #func{type :: typeidx(), locals :: [valtype()], body :: [instr()] | {validated, [annotated()]}}) -> [tuple()].
Validate one function body against its declared type, and return it annotated.
The validator already knows the operand-stack height at every instruction: it
is #vs.nopds, and the abstract stack machine cannot work without it. It used
to be computed and thrown away. It is returned instead, because a compiler that
wants to assign an operand to a slot rather than to a list needs exactly that
number, and recovering it afterwards means writing the abstract stack machine a
second time and keeping the two in step.
Every instruction is paired with the height on entry. The four that contain a
body carry their frame's base as well, because a branch slices the stack back
to the base of the frame it targets, and that is a property of the frame rather
than of any instruction inside it. See annotate/3 for the two shapes.
Direction, value type and natural alignment (log2 bytes) of an access.
-spec subtype(valtype(), valtype(), #ctx{types :: tuple(), canon :: tuple(), fields :: tuple(), kinds :: tuple(), supers :: tuple(), funcs :: tuple(), tables :: tuple(), mems :: tuple(), globals :: tuple(), tags :: tuple(), elems :: tuple(), n_datas :: non_neg_integer(), n_imported_globals :: non_neg_integer(), refs :: #{non_neg_integer() => true}, shared_globals :: #{non_neg_integer() => true}, shared_mems :: #{non_neg_integer() => true}, locals :: tuple(), results :: [valtype()]}) -> boolean().
Whether A is usable where B is expected.
Exported for the module-level checks in wasm_validate, which compare declared
types outside any operand stack.