# Validation Algorithm¶

The specification of WebAssembly validation is purely *declarative*.
It describes the constraints that must be met by a module or instruction sequence to be valid.

This section sketches the skeleton of a sound and complete *algorithm* for effectively validating code, i.e., sequences of instructions.
(Other aspects of validation are straightforward to implement.)

In fact, the algorithm is expressed over the flat sequence of opcodes as occurring in the binary format, and performs only a single pass over it. Consequently, it can be integrated directly into a decoder.

The algorithm is expressed in typed pseudo code whose semantics is intended to be self-explanatory.

## Data Structures¶

### Types¶

Value types are representable as sets of enumerations:

```
type num_type = I32 | I64 | F32 | F64
type vec_type = V128
type heap_type =
Any | Eq | I31 | Struct | Array | None |
Func | Nofunc | Extern | Noextern | Bot |
Def(def : def_type)
type ref_type = Ref(heap : heap_type, null : bool)
type val_type = num_type | vec_type | ref_type | Bot
func is_num(t : val_type) : bool =
return t = I32 || t = I64 || t = F32 || t = F64 || t = Bot
func is_vec(t : val_type) : bool =
return t = V128 || t = Bot
func is_ref(t : val_type) : bool =
return not (is_num t || is_vec t) || t = Bot
```

Similarly, defined types `def_type`

can be represented:

```
type packed_type = I8 | I16
type field_type = Field(val : val_type | packed_type, mut : bool)
type struct_type = Struct(fields : list(field_type))
type array_type = Array(fields : field_type)
type func_type = Func(params : list(val_type), results : list(val_type))
type comp_type = struct_type | array_type | func_type
type sub_type = Sub(super : list(def_type), body : comp_type, final : bool)
type rec_type = Rec(types : list(sub_type))
type def_type = Def(rec : rec_type, proj : int32)
func unpack_field(t : field_type) : val_type =
if (it = I8 || t = I16) return I32
return t
func expand_def(t : def_type) : comp_type =
return t.rec.types[t.proj].body
```

These representations assume that all types have been closed by substituting all type indices (in concrete heap types and in sub types) with their respective defined types.
This includes *recursive* references to enclosing defined types,
such that type representations form graphs and may be *cyclic* for recursive types.

We assume that all types have been *canonicalized*, such that equality on two type representations holds if and only if their closures are syntactically equivalent, making it a constant-time check.

Note

For the purpose of type canonicalization, recursive references from a heap type to an enclosing recursive type (i.e., forward edges in the graph that form a cycle) need to be distinguished from references to previously defined types. However, this distinction does not otherwise affect validation, so is ignored here. In the graph representation, all recursive types are effectively infinitely unrolled.

We further assume that validation and subtyping checks are defined on value types, as well as a few auxiliary functions on composite types:

```
func validate_val_type(t : val_type)
func validate_ref_type(t : ref_type)
func matches_val(t1 : val_type, t2 : val_type) : bool
func matches_ref(t1 : val_type, t2 : val_type) : bool
func is_func(t : comp_type) : bool
func is_struct(t : comp_type) : bool
func is_array(t : comp_type) : bool
```

Finally, the following function computes the least precise supertype of a given heap type (its corresponding top type):

```
func top_heap_type(t : heap_type) : heap_type =
switch (t)
case (Any | Eq | I31 | Struct | Array | None)
return Any
case (Func | Nofunc)
return Func
case (Extern | Noextern)
return Extern
case (Def(dt))
switch (dt.rec.types[dt.proj].body)
case (Struct(_) | Array(_))
return Any
case (Func(_))
return Func
case (Bot)
raise CannotOccurInSource
```

### Context¶

Validation requires a context for checking uses of indices. For the purpose of presenting the algorithm, it is maintained in a set of global variables:

```
var return_type : list(val_type)
var types : array(def_type)
var locals : array(val_type)
var locals_init : array(bool)
var globals : array(global_type)
var funcs : array(func_type)
var tables : array(table_type)
var mems : array(mem_type)
```

This assumes suitable representations for the various types besides `val_type`

, which are omitted here.

For locals, there is an additional array recording the initialization status of each local.

### Stacks¶

The algorithm uses three separate stacks: the *value stack*, the *control stack*, and the *initialization stack*.
The value stack tracks the types of operand values on the stack.
The control stack tracks surrounding structured control instructions and their associated blocks.
The initialization stack records all locals that have been initialized since the beginning of the function.

```
type val_stack = stack(val_type)
type init_stack = stack(u32)
type ctrl_stack = stack(ctrl_frame)
type ctrl_frame = {
opcode : opcode
start_types : list(val_type)
end_types : list(val_type)
val_height : nat
init_height : nat
unreachable : bool
}
```

For each entered block, the control stack records a *control frame* with the originating opcode, the types on the top of the operand stack at the start and end of the block (used to check its result as well as branches), the height of the operand stack at the start of the block (used to check that operands do not underflow the current block), the height of the initialization stack at the start of the block (used to reset initialization status at the end of the block), and a flag recording whether the remainder of the block is unreachable (used to handle stack-polymorphic typing after branches).

For the purpose of presenting the algorithm, these stacks are simply maintained as global variables:

```
var vals : val_stack
var inits : init_stack
var ctrls : ctrl_stack
```

However, these variables are not manipulated directly by the main checking function, but through a set of auxiliary functions:

```
func push_val(type : val_type) =
vals.push(type)
func pop_val() : val_type =
if (vals.size() = ctrls[0].height && ctrls[0].unreachable) return Bot
error_if(vals.size() = ctrls[0].height)
return vals.pop()
func pop_val(expect : val_type) : val_type =
let actual = pop_val()
error_if(not matches_val(actual, expect))
return actual
func pop_num() : num_type | Bot =
let actual = pop_val()
error_if(not is_num(actual))
return actual
func pop_ref() : ref_type =
let actual = pop_val()
error_if(not is_ref(actual))
if (actual = Bot) return Ref(Bot, false)
return actual
func push_vals(types : list(val_type)) = foreach (t in types) push_val(t)
func pop_vals(types : list(val_type)) : list(val_type) =
var popped := []
foreach (t in reverse(types)) popped.prepend(pop_val(t))
return popped
```

Pushing an operand value simply pushes the respective type to the value stack.

Popping an operand value checks that the value stack does not underflow the current block and then removes one type.
But first, a special case is handled where the block contains no known values, but has been marked as unreachable.
That can occur after an unconditional branch, when the stack is typed polymorphically.
In that case, the `Bot`

type is returned, because that is a *principal* choice trivially satisfying all use constraints.

A second function for popping an operand value takes an expected type, which the actual operand type is checked against.
The types may differ by subtyping, including the case where the actual type is `Bot`

, and thereby matches unconditionally.
The function returns the actual type popped from the stack.

Finally, there are accumulative functions for pushing or popping multiple operand types.

Note

The notation `stack[i]`

is meant to index the stack from the top,
so that, e.g., `ctrls[0]`

accesses the element pushed last.

The initialization stack and the initialization status of locals is manipulated through the following functions:

```
func get_local(idx : u32) =
error_if(not locals_init[idx])
func set_local(idx : u32) =
if (not locals_init[idx])
inits.push(idx)
locals_init[idx] := true
func reset_locals(height : nat) =
while (inits.size() > height)
locals_init[inits.pop()] := false
```

Getting a local verifies that it is known to be initialized. When a local is set that was not set already, then its initialization status is updated and the change is recorded in the initialization stack. Thus, the initialization status of all locals can be reset to a previous state by denoting a specific height in the initialization stack.

The size of the initialization stack is bounded by the number of (non-defaultable) locals in a function, so can be preallocated by an algorithm.

The control stack is likewise manipulated through auxiliary functions:

```
func push_ctrl(opcode : opcode, in : list(val_type), out : list(val_type)) =
let frame = ctrl_frame(opcode, in, out, vals.size(), inits.size(), false)
ctrls.push(frame)
push_vals(in)
func pop_ctrl() : ctrl_frame =
error_if(ctrls.is_empty())
let frame = ctrls[0]
pop_vals(frame.end_types)
error_if(vals.size() =/= frame.val_height)
reset_locals(frame.init_height)
ctrls.pop()
return frame
func label_types(frame : ctrl_frame) : list(val_types) =
return (if (frame.opcode = loop) frame.start_types else frame.end_types)
func unreachable() =
vals.resize(ctrls[0].height)
ctrls[0].unreachable := true
```

Pushing a control frame takes the types of the label and result values. It allocates a new frame record recording them along with the current height of the operand stack and marks the block as reachable.

Popping a frame first checks that the control stack is not empty. It then verifies that the operand stack contains the right types of values expected at the end of the exited block and pops them off the operand stack. Afterwards, it checks that the stack has shrunk back to its initial height. Finally, it undoes all changes to the initialization status of locals that happend inside the block.

The type of the label associated with a control frame is either that of the stack at the start or the end of the frame, determined by the opcode that it originates from.

Finally, the current frame can be marked as unreachable.
In that case, all existing operand types are purged from the value stack, in order to allow for the stack-polymorphism logic in `pop_val`

to take effect.
Because every function has an implicit outermost label that corresponds to an implicit block frame,
it is an invariant of the validation algorithm that there always is at least one frame on the control stack when validating an instruction, and hence, ctrls[0] is always defined.

Note

Even with the unreachable flag set, consecutive operands are still pushed to and popped from the operand stack.
That is necessary to detect invalid examples like \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}})~\href{../syntax/types.html#syntax-valtype}{\mathsf{i64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}})\).
However, a polymorphic stack cannot underflow, but instead generates `Bot`

types as needed.

## Validation of Opcode Sequences¶

The following function shows the validation of a number of representative instructions that manipulate the stack. Other instructions are checked in a similar manner.

```
func validate(opcode) =
switch (opcode)
case (i32.add)
pop_val(I32)
pop_val(I32)
push_val(I32)
case (drop)
pop_val()
case (select)
pop_val(I32)
let t1 = pop_val()
let t2 = pop_val()
error_if(not (is_num(t1) && is_num(t2) || is_vec(t1) && is_vec(t2)))
error_if(t1 =/= t2 && t1 =/= Bot && t2 =/= Bot)
push_val(if (t1 = Bot) t2 else t1)
case (select t)
pop_val(I32)
pop_val(t)
pop_val(t)
push_val(t)
case (ref.is_null)
pop_ref()
push_val(I32)
case (ref.as_non_null)
let rt = pop_ref()
push_val(Ref(rt.heap, false))
case (ref.test rt)
validate_ref_type(rt)
pop_val(Ref(top_heap_type(rt), true))
push_val(I32)
case (local.get x)
get_local(x)
push_val(locals[x])
case (local.set x)
pop_val(locals[x])
set_local(x)
case (unreachable)
unreachable()
case (block t1*->t2*)
pop_vals([t1*])
push_ctrl(block, [t1*], [t2*])
case (loop t1*->t2*)
pop_vals([t1*])
push_ctrl(loop, [t1*], [t2*])
case (if t1*->t2*)
pop_val(I32)
pop_vals([t1*])
push_ctrl(if, [t1*], [t2*])
case (end)
let frame = pop_ctrl()
push_vals(frame.end_types)
case (else)
let frame = pop_ctrl()
error_if(frame.opcode =/= if)
push_ctrl(else, frame.start_types, frame.end_types)
case (br n)
error_if(ctrls.size() < n)
pop_vals(label_types(ctrls[n]))
unreachable()
case (br_if n)
error_if(ctrls.size() < n)
pop_val(I32)
pop_vals(label_types(ctrls[n]))
push_vals(label_types(ctrls[n]))
case (br_table n* m)
pop_val(I32)
error_if(ctrls.size() < m)
let arity = label_types(ctrls[m]).size()
foreach (n in n*)
error_if(ctrls.size() < n)
error_if(label_types(ctrls[n]).size() =/= arity)
push_vals(pop_vals(label_types(ctrls[n])))
pop_vals(label_types(ctrls[m]))
unreachable()
case (br_on_null n)
error_if(ctrls.size() < n)
let rt = pop_ref()
pop_vals(label_types(ctrls[n]))
push_vals(label_types(ctrls[n]))
push_val(Ref(rt.heap, false))
case (br_on_cast n rt1 rt2)
validate_ref_type(rt1)
validate_ref_type(rt2)
pop_val(rt1)
push_val(rt2)
pop_vals(label_types(ctrls[n]))
push_vals(label_types(ctrls[n]))
pop_val(rt2)
push_val(diff_ref_type(rt2, rt1))
case (return)
pop_vals(return_types)
unreachable()
case (call_ref x)
let t = expand_def(types[x])
error_if(not is_func(t))
pop_vals(t.params)
pop_val(Ref(Def(types[x])))
push_vals(t.results)
case (return_call_ref x)
let t = expand_def(types[x])
error_if(not is_func(t))
pop_vals(t.params)
pop_val(Ref(Def(types[x])))
error_if(t.results.len() =/= return_types.len())
push_vals(t.results)
pop_vals(return_types)
unreachable()
case (struct.new x)
let t = expand_def(types[x])
error_if(not is_struct(t))
for (ti in reverse(t.fields))
pop_val(unpack_field(ti))
push_val(Ref(Def(types[x])))
case (struct.set x n)
let t = expand_def(types[x])
error_if(not is_struct(t) || n >= t.fields.len())
pop_val(Ref(Def(types[x])))
pop_val(unpack_field(st.fields[n]))
```

Note

It is an invariant under the current WebAssembly instruction set that an operand of `Bot`

type is never duplicated on the stack.
This would change if the language were extended with stack instructions like `dup`

.
Under such an extension, the above algorithm would need to be refined by replacing the `Bot`

type with proper *type variables* to ensure that all uses are consistent.