Instructions¶
WebAssembly computation is performed by executing individual instructions.
Numeric Instructions¶
Numeric instructions are defined in terms of the generic numeric operators. The mapping of numeric instructions to their underlying operators is expressed by the following definition:
And for conversion operators:
Where the underlying operators are partial, the corresponding instruction will trap when the result is not defined. Where the underlying operators are non-deterministic, because they may return one of multiple possible NaN values, so are the corresponding instructions.
Note
For example, the result of instruction
¶
Push the value
to the stack.
Note
No formal reduction rule is required for this instruction, since
¶
Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.If
is defined, then:Let
be a possible result of computing .Push the value
to the stack.
Else:
Trap.
¶
Assert: due to validation, two values of value type
are on the top of the stack.Pop the value
from the stack.Pop the value
from the stack.If
is defined, then:Let
be a possible result of computing .Push the value
to the stack.
Else:
Trap.
¶
Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Push the value
to the stack.
¶
Assert: due to validation, two values of value type
are on the top of the stack.Pop the value
from the stack.Pop the value
from the stack.Let
be the result of computing .Push the value
to the stack.
¶
Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.If
is defined:Let
be a possible result of computing .Push the value
to the stack.
Else:
Trap.
¶
Assert: due to validation, four values of value type
are on the top of the stack.Pop the value
from the stack.Pop the value
from the stack.Pop the value
from the stack.Pop the value
from the stack.Let
be the result of computingLet
be the result of computingLet
be the result of computingLet
be the result of computingPush the value
to the stack.Push the value
to the stack.
¶
Assert: due to validation, two values of value type
are on the top of the stack.Pop the value
from the stack.Pop the value
from the stack.Let
be the result of computingLet
be the result of computing
Let
be the result of computingLet
be the result of computingPush the value
to the stack.Push the value
to the stack.
Reference Instructions¶
¶
Push the value
to the stack.
Note
No formal reduction rule is required for this instruction, since the
¶
Assert: due to validation, a reference value is on the top of the stack.
Pop the value
from the stack.If
is , then:Push the value
to the stack.
Else:
Push the value
to the stack.
¶
Assert: due to validation,
exists.Let
be the function address .Push the value
to the stack.
Vector Instructions¶
Vector instructions that operate bitwise are handled as integer operations of respective width.
Most other vector instructions are defined in terms of numeric operators that are applied lane-wise according to the given shape.
Note
For example, the result of instruction
¶
Push the value
to the stack.
Note
No formal reduction rule is required for this instruction, since
¶
Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Push the value
to the stack.
¶
Assert: due to validation, two values of value type
are on the top of the stack.Pop the value
from the stack.Pop the value
from the stack.Let
be the result of computing .Push the value
to the stack.
¶
Assert: due to validation, three values of value type
are on the top of the stack.Pop the value
from the stack.Pop the value
from the stack.Pop the value
from the stack.Let
be the result of computing .Push the value
to the stack.
¶
Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Push the value
onto the stack.
¶
Assert: due to validation, two values of value type
are on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Pop the value
from the stack.Let
be the result of computing .Let
be the concatenation of the two sequences and .Let
be the result of computing .Push the value
onto the stack.
¶
Assert: due to validation, two values of value type
are on the top of the stack.Assert: due to validation, for all
in it holds that .Pop the value
from the stack.Let
be the result of computing .Pop the value
from the stack.Let
be the result of computing .Let
be the concatenation of the two sequences and .Let
be the result of computing .Push the value
onto the stack.
¶
Let
be the type .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the integer .Let
be the result of computing .Push the value
to the stack.
¶
Assert: due to validation,
.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Let
be the type .Let
be the result of computing .Push the value
to the stack.
¶
Assert: due to validation,
.Let
be the type .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Let
be the result of computing .Push
on the stack.
¶
Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Push the value
to the stack.
¶
Assert: due to validation, two values of value type
are on the top of the stack.Pop the value
from the stack.Pop the value
from the stack.If
is defined:Let
be a possible result of computing .Push the value
to the stack.
Else:
Trap.
¶
Assert: due to validation, two values of value type
are on the top of the stack.Pop the value
from the stack.Pop the value
from the stack.Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Push the value
to the stack.
¶
Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Push the value
to the stack.
¶
Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Let
be the result of computing .Push the value
onto the stack.
¶
Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Let
be the bit width of value type .Let
be the result of computing .Let
be the concatenation of the two sequences and .Let
be the result of computing .Push the value
onto the stack.
¶
Assert: due to syntax,
.Assert: due to validation, two values of value type
are on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Let
be the result of computing .Pop the value
from the stack.Let
be the result of computing .Let
be the result of computing .Let
be the concatenation of the two sequences and .Let
be the result of computing .Push the value
onto the stack.
¶
Assert: due to syntax,
.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Push the value
onto the stack.
¶
Assert: due to syntax,
.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the result of computing .If
is , then:Let
be the sequence .
Else:
Let
be the sequence .
Let
be the result of computing .Let
be the result of computing .Push the value
onto the stack.
where:
¶
Assert: due to syntax,
.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Let
be the result of computing .Let
be the concatenation of the two sequences and .Let
be the result of computing .Push the value
onto the stack.
¶
Assert: due to validation, two values of value type
are on the top of the stack.Pop the value
from the stack.Pop the value
from the stack.Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Push the value
onto the stack.
¶
Assert: due to syntax,
.Assert: due to validation, two values of value type
are on the top of the stack.Pop the value
from the stack.Pop the value
from the stack.Let
be the result of computing .Let
be the result of computing .If
is , then:Let
be the sequence .Let
be the sequence .
Else:
Let
be the sequence .Let
be the sequence .
Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Push the value
onto the stack.
where:
¶
Assert: due to syntax,
.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Let
be the result of computing .Push the value
to the stack.
Parametric Instructions¶
¶
Assert: due to validation, a value is on the top of the stack.
Pop the value
from the stack.
¶
Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, two more values (of the same value type) are on the top of the stack.
Pop the value
from the stack.Pop the value
from the stack.If
is not , then:Push the value
back to the stack.
Else:
Push the value
back to the stack.
Note
In future versions of WebAssembly,
Variable Instructions¶
¶
Assert: due to validation,
exists.Let
be the value .Push the value
to the stack.
¶
Assert: due to validation,
exists.Assert: due to validation, a value is on the top of the stack.
Pop the value
from the stack.Replace
with the value .
¶
Assert: due to validation, a value is on the top of the stack.
Pop the value
from the stack.Push the value
to the stack.Push the value
to the stack.Execute the instruction
.
¶
Assert: due to validation,
exists.Let
be the global address .Assert: due to validation,
exists.Let
be the global instance .Let
be the value .Push the value
to the stack.
¶
Assert: due to validation,
exists.Let
be the global address .Assert: due to validation,
exists.Let
be the global instance .Assert: due to validation, a value is on the top of the stack.
Pop the value
from the stack.Replace
with the value .
Note
Validation ensures that the global is, in fact, marked as mutable.
Table Instructions¶
¶
Assert: due to validation,
exists.Let
be the table address .Assert: due to validation,
exists.Let
be the table instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.If
is not smaller than the length of , then:Trap.
Let
be the value .Push the value
to the stack.
¶
Assert: due to validation,
exists.Let
be the table address .Assert: due to validation,
exists.Let
be the table instance .Assert: due to validation, a reference value is on the top of the stack.
Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.If
is not smaller than the length of , then:Trap.
Replace the element
with .
¶
Assert: due to validation,
exists.Let
be the table address .Assert: due to validation,
exists.Let
be the table instance .Let
be the length of .Push the value
to the stack.
¶
Assert: due to validation,
exists.Let
be the table address .Assert: due to validation,
exists.Let
be the table instance .Let
be the length of .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a reference value is on the top of the stack.
Pop the value
from the stack.Let
be the value , for which is .Either:
If growing
by entries with initialization value succeeds, then:
Push the value
to the stack. Else:
Push the value
to the stack.
Or:
push the value
to the stack.
Note
The
¶
Assert: due to validation,
exists.Let
be the table address .Assert: due to validation,
exists.Let
be the table instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a reference value is on the top of the stack.
Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.If
is larger than the length of , then:Trap.
If
is , then:Return.
Push the value
to the stack.Push the value
to the stack.Execute the instruction
.Push the value
to the stack.Push the value
to the stack.Push the value
to the stack.Execute the instruction
.
¶
Assert: due to validation,
exists.Let
be the table address .Assert: due to validation,
exists.Let
be the table instance .Assert: due to validation,
exists.Let
be the table address .Assert: due to validation,
exists.Let
be the table instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.If
is larger than the length of or is larger than the length of , then:Trap.
If
, then:
Return.
If
, then:
Push the value
to the stack. Push the value
to the stack. Execute the instruction
. Execute the instruction
. Assert: due to the earlier check against the table size,
. Push the value
to the stack. Assert: due to the earlier check against the table size,
. Push the value
to the stack.
Else:
Assert: due to the earlier check against the table size,
. Push the value
to the stack. Assert: due to the earlier check against the table size,
. Push the value
to the stack.
Execute the instruction
.
Execute the instruction
. Push the value
to the stack. Push the value
to the stack.
Push the value
to the stack.Execute the instruction
.
¶
Assert: due to validation,
exists.Let
be the table address .Assert: due to validation,
exists.Let
be the table instance .Assert: due to validation,
exists.Let
be the element address .Assert: due to validation,
exists.Let
be the element instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.If
is larger than the length of or is larger than the length of , then:Trap.
If
, then:Return.
Let
be the reference value .Push the value
to the stack.Push the value
to the stack.Execute the instruction
.Assert: due to the earlier check against the table size,
.Push the value
to the stack.Assert: due to the earlier check against the segment size,
.Push the value
to the stack.Push the value
to the stack.Execute the instruction
.
¶
Assert: due to validation,
exists.Let
be the element address .Assert: due to validation,
exists.Replace
with .
Memory Instructions¶
Note
The alignment
and ¶
Assert: due to validation,
exists.Let
be the memory address .Assert: due to validation,
exists.Let
be the memory instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the integer .If
is not part of the instruction, then:Let
be the bit width of number type .
If
is larger than the length of , then:Trap.
Let
be the byte sequence .If
and are part of the instruction, then:Let
be the integer for which .Let
be the result of computing .
Else:
Let
be the constant for which .
Push the value
to the stack.
¶
Assert: due to validation,
exists.Let
be the memory address .Assert: due to validation,
exists.Let
be the memory instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the integer .If
is larger than the length of , then:Trap.
Let
be the byte sequence .Let
be the integer for which .Let
be the integer .Let
be the result of computing .Let
be the result of computing .Push the value
to the stack.
¶
Assert: due to validation,
exists.Let
be the memory address .Assert: due to validation,
exists.Let
be the memory instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the integer .If
is larger than the length of , then:Trap.
Let
be the byte sequence .Let
be the integer for which .Let
be the integer .Let
be the result of computing .Push the value
to the stack.
¶
Assert: due to validation,
exists.Let
be the memory address .Assert: due to validation,
exists.Let
be the memory instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the integer .If
is larger than the length of , then:Trap.
Let
be the byte sequence .Let
be the integer for which .Let
be the result of computing .Push the value
to the stack.
¶
Assert: due to validation,
exists.Let
be the memory address .Assert: due to validation,
exists.Let
be the memory instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the integer .If
is larger than the length of , then:Trap.
Let
be the byte sequence .Let
be the constant for which .Let
be .Let
be the result of computing .Let
be the result of computing .Push the value
to the stack.
and ¶
Assert: due to validation,
exists.Let
be the memory address .Assert: due to validation,
exists.Let
be the memory instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the integer .If
is not part of the instruction, then:Let
be the bit width of number type .
If
is larger than the length of , then:Trap.
If
is part of the instruction, then:Let
be the result of computing .Let
be the byte sequence .
Else:
Let
be the byte sequence .
Replace the bytes
with .
¶
Assert: due to validation,
exists.Let
be the memory address .Assert: due to validation,
exists.Let
be the memory instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the integer .If
is larger than the length of , then:Trap.
Let
be .Let
be the result of computing .Let
be the result of computing .Replace the bytes
with .
¶
Assert: due to validation,
exists.Let
be the memory address .Assert: due to validation,
exists.Let
be the memory instance .Let
be the length of divided by the page size.Push the value
to the stack.
¶
Assert: due to validation,
exists.Let
be the memory address .Assert: due to validation,
exists.Let
be the memory instance .Let
be the length of divided by the page size.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Let
be the value , for which is .Either:
Or:
Push the value
to the stack.
Note
The
¶
Assert: due to validation,
exists.Let
be the memory address .Assert: due to validation,
exists.Let
be the memory instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.If
is larger than the length of , then:Trap.
If
, then:Return.
Push the value
to the stack.Push the value
to the stack.Execute the instruction
.Assert: due to the earlier check against the memory size,
.Push the value
to the stack.Push the value
to the stack.Push the value
to the stack.Execute the instruction
.
¶
Assert: due to validation,
exists.Let
be the memory address .Assert: due to validation,
exists.Let
be the memory instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.If
is larger than the length of or is larger than the length of , then:Trap.
If
, then:
Return.
If
, then:
Push the value
to the stack. Push the value
to the stack. Execute the instruction
. Execute the instruction
. Assert: due to the earlier check against the memory size,
. Push the value
to the stack. Assert: due to the earlier check against the memory size,
. Push the value
to the stack.
Else:
Assert: due to the earlier check against the memory size,
. Push the value
to the stack. Assert: due to the earlier check against the memory size,
. Push the value
to the stack. Execute the instruction
. Execute the instruction
. Push the value
to the stack. Push the value
to the stack.
Push the value
to the stack.Execute the instruction
.
¶
Assert: due to validation,
exists.Let
be the memory address .Assert: due to validation,
exists.Let
be the memory instance .Assert: due to validation,
exists.Let
be the data address .Assert: due to validation,
exists.Let
be the data instance .Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.If
is larger than the length of or is larger than the length of , then:Trap.
If
, then:Return.
Let
be the byte .Push the value
to the stack.Push the value
to the stack.Execute the instruction
.Assert: due to the earlier check against the memory size,
.Push the value
to the stack.Assert: due to the earlier check against the memory size,
.Push the value
to the stack.Push the value
to the stack.Execute the instruction
.
¶
Assert: due to validation,
exists.Let
be the data address .Assert: due to validation,
exists.Replace
with the data instance .
Control Instructions¶
¶
Do nothing.
¶
Trap.
¶
Assert: due to validation,
is defined.Let
be the function type .Let
be the label whose arity is and whose continuation is the end of the block.Assert: due to validation, there are at least
values on the top of the stack.Pop the values
from the stack.Enter the block
with label .
¶
Assert: due to validation,
is defined.Let
be the function type .Let
be the label whose arity is and whose continuation is the start of the loop.Assert: due to validation, there are at least
values on the top of the stack.Pop the values
from the stack.Enter the block
with label .
¶
Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.If
is non-zero, then:Execute the block instruction
.
Else:
Execute the block instruction
.
¶
Assert: due to validation, the stack contains at least
labels.Let
be the -th label appearing on the stack, starting from the top and counting from zero.Let
be the arity of .Assert: due to validation, there are at least
values on the top of the stack.Pop the values
from the stack.Repeat
times:While the top of the stack is a value, do:
Pop the value from the stack.
Assert: due to validation, the top of the stack now is a label.
Pop the label from the stack.
Push the values
to the stack.Jump to the continuation of
.
¶
Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.If
is non-zero, then:Execute the instruction
.
Else:
Do nothing.
¶
Assert: due to validation, a value of value type
is on the top of the stack.Pop the value
from the stack.If
is smaller than the length of , then:Let
be the label .Execute the instruction
.
Else:
Execute the instruction
.
¶
Let
be the arity of .Assert: due to validation, there are at least
values on the top of the stack.Pop the results
from the stack.Assert: due to validation, the stack contains at least one frame.
While the top of the stack is not a frame, do:
Pop the top element from the stack.
Assert: the top of the stack is the frame
.Pop the frame from the stack.
Push
to the stack.Jump to the instruction after the original call that pushed the frame.
¶
Assert: due to validation,
exists.Let
be the function address .Invoke the function instance at address
.
¶
Assert: due to validation,
exists.Let
be the table address .Assert: due to validation,
exists.Let
be the table instance .Assert: due to validation,
exists.Let
be the function type .Assert: due to validation, a value with value type
is on the top of the stack.Pop the value
from the stack.If
is not smaller than the length of , then:Trap.
Let
be the reference .If
is , then:Trap.
Assert: due to validation of table mutation,
is a function reference.Let
be the function reference .Assert: due to validation of table mutation,
exists.Let
be the function instance .Let
be the function type .If
and differ, then:Trap.
Invoke the function instance at address
.
Blocks¶
The following auxiliary rules define the semantics of executing an instruction sequence that forms a block.
Entering with label ¶
Push
to the stack.Jump to the start of the instruction sequence
.
Note
No formal reduction rule is needed for entering an instruction sequence,
because the label
Exiting with label ¶
When the end of a block is reached without a jump or trap aborting it, then the following steps are performed.
Pop all values
from the top of the stack.Assert: due to validation, the label
is now on the top of the stack.Pop the label from the stack.
Push
back to the stack.Jump to the position after the
of the structured control instruction associated with the label .
Note
This semantics also applies to the instruction sequence contained in a
Function Calls¶
The following auxiliary rules define the semantics of invoking a function instance through one of the call instructions and returning from it.
Invocation of function address ¶
Assert: due to validation,
exists.Let
be the function instance, .Let
be the function type .Let
be the list of value types .Let
be the expression .Assert: due to validation,
values are on the top of the stack.Pop the values
from the stack.Let
be the frame .Push the activation of
with arity to the stack.Let
be the label whose arity is and whose continuation is the end of the function.Enter the instruction sequence
with label .
Returning from a function¶
When the end of a function is reached without a jump (i.e.,
Let
be the arity of the activation of .Assert: due to validation, there are
values on the top of the stack.Pop the results
from the stack.Assert: due to validation, the frame
is now on the top of the stack.Pop the frame from the stack.
Push
back to the stack.Jump to the instruction after the original call.
Host Functions¶
Invoking a host function has non-deterministic behavior. It may either terminate with a trap or return regularly. However, in the latter case, it must consume and produce the right number and types of WebAssembly values on the stack, according to its function type.
A host function may also modify the store. However, all store modifications must result in an extension of the original store, i.e., they must only modify mutable contents and must not have instances removed. Furthermore, the resulting store must be valid, i.e., all data and code in it is well-typed.
Here,
For a WebAssembly implementation to be sound in the presence of host functions,
every host function instance must be valid,
which means that it adheres to suitable pre- and post-conditions:
under a valid store
Expressions¶
An expression is evaluated relative to a current frame pointing to its containing module instance.
Jump to the start of the instruction sequence
of the expression.Execute the instruction sequence.
Assert: due to validation, the top of the stack contains a value.
Pop the value
from the stack.
The value
Note
Evaluation iterates this reduction rule until reaching a value. Expressions constituting function bodies are executed during function invocation.