Runtime Structure
Store, stack, and other runtime structure forming the WebAssembly abstract machine, such as values or module instances, are made precise in terms of additional auxiliary syntax.
Values
WebAssembly computations manipulate values of either the four basic number types, i.e., integers and floating-point data of 32 or 64 bit width each, or vectors of 128 bit width, or of reference type.
In most places of the semantics, values of different types can occur.
In order to avoid ambiguities, values are therefore represented with an abstract syntax that makes their type explicit.
It is convenient to reuse the same notation as for the \(\mathsf{const}\) instructions and \(\mathsf{ref{.}null}\) producing them.
References other than null are represented with additional administrative instructions.
They either are scalar references, containing a 31-bit integer,
structure references, pointing to a specific structure address,
array references, pointing to a specific array address,
function references, pointing to a specific function address,
exception references, pointing to a specific exception address,
or host references pointing to an uninterpreted form of host address defined by the embedder.
Any of the aformentioned references can furthermore be wrapped up as an external reference.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-val}{\mathit{val}}} & ::= & {\href{../exec/runtime.html#syntax-num}{\mathit{num}}} ~|~ {\href{../exec/runtime.html#syntax-vec}{\mathit{vec}}} ~|~ {\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}} \\[0.8ex]
& {\href{../exec/runtime.html#syntax-num}{\mathit{num}}} & ::= & {\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~{{\href{../exec/runtime.html#syntax-num}{\mathit{num}}}}_{{\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}} \\[0.8ex]
& {\href{../exec/runtime.html#syntax-vec}{\mathit{vec}}} & ::= & {\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~{{\href{../exec/runtime.html#syntax-vec}{\mathit{vec}}}}_{{\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}} \\[0.8ex]
& {\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}} & ::= & {\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}} \\
& & | & \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~{\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}} \\[0.8ex]
& {\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}} & ::= & \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}i31}}~{\href{../syntax/values.html#syntax-int}{\mathit{u\scriptstyle\kern-0.1em31}}} \\
& & | & \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}struct}}~{\href{../exec/runtime.html#syntax-structaddr}{\mathit{structaddr}}} \\
& & | & \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}array}}~{\href{../exec/runtime.html#syntax-arrayaddr}{\mathit{arrayaddr}}} \\
& & | & \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}func}}~{\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}} \\
& & | & \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}exn}}~{\href{../exec/runtime.html#syntax-exnaddr}{\mathit{exnaddr}}} \\
& & | & \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}host}}~{\href{../exec/runtime.html#syntax-hostaddr}{\mathit{hostaddr}}} \\
& & | & \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}extern}}~{\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}} \\
\end{array}\end{split}\]
Note
Future versions of WebAssembly may add additional forms of values.
Value types can have an associated default value;
it is the respective value \(0\) for number types, \(0\) for vector types, and null for nullable reference types.
For other references, no default value is defined, \({{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{t}\) hence is an optional value \({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^?}\).
\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}}
{{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{{\mathsf{i}}{N}} & = & ({\mathsf{i}}{N}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0) \\
{{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{{\mathsf{f}}{N}} & = & ({\mathsf{f}}{N}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~{+0}) \\
{{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{{\mathsf{v}}{N}} & = & ({\mathsf{v}}{N}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~0) \\
{{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}}} & = & (\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~{\mathit{ht}}) \\
{{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{ht}}} & = & \epsilon \\
\end{array}\end{split}\]
Results
A result is the outcome of a computation.
It is either a sequence of values, an exception, or a trap.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-result}{\mathit{result}}} & ::= & {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast} ~|~ ( \href{../exec/runtime.html#syntax-ref}{\mathsf{ref{.}exn}}~{\href{../exec/runtime.html#syntax-exnaddr}{\mathit{exnaddr}}} )~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}} ~|~ \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\
\end{array}\end{split}\]
Store
The store represents all global state that can be manipulated by WebAssembly programs.
It consists of the runtime representation of all instances of
functions,
tables,
memories,
globals,
tags,
element segments,
data segments,
and
structures,
arrays or
exceptions
that have been allocated during the life time of the abstract machine.
It is an invariant of the semantics that no element or data instance is addressed from anywhere else but the owning module instances.
Syntactically, the store is defined as a record listing the existing instances of each category:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-store}{\mathit{store}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~{{\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}}^\ast} \\
\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}~{{\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}}^\ast} \\
\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}~{{\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}}^\ast} \\
\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}~{{\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}}^\ast} \\
\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}~{{\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}}^\ast} \\
\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}~{{\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}}^\ast} \\
\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}~{{\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}}^\ast} \\
\href{../exec/runtime.html#syntax-store}{\mathsf{structs}}~{{\href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}}^\ast} \\
\href{../exec/runtime.html#syntax-store}{\mathsf{arrays}}~{{\href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}}^\ast} \\
\href{../exec/runtime.html#syntax-store}{\mathsf{exns}}~{{\href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}}}^\ast} \} \\
\end{array} \\
\end{array}\end{split}\]
Addresses
Function instances,
table instances,
memory instances,
global instances,
tag instances,
element instances,
data instances
and
structure,
array instances or
exception instances
in the store are referenced with abstract addresses.
These are simply indices into the respective store component.
In addition, an embedder may supply an uninterpreted set of host addresses.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} & ::= & 0 ~|~ 1 ~|~ 2 ~|~ \dots \\
& {\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}} & ::= & {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\
& {\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}} & ::= & {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\
& {\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}} & ::= & {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\
& {\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}} & ::= & {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\
& {\href{../exec/runtime.html#syntax-tagaddr}{\mathit{tagaddr}}} & ::= & {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\
& {\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}} & ::= & {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\
& {\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}} & ::= & {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\
& {\href{../exec/runtime.html#syntax-structaddr}{\mathit{structaddr}}} & ::= & {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\
& {\href{../exec/runtime.html#syntax-arrayaddr}{\mathit{arrayaddr}}} & ::= & {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\
& {\href{../exec/runtime.html#syntax-hostaddr}{\mathit{hostaddr}}} & ::= & {\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}} \\
\end{array}\end{split}\]
An embedder may assign identity to exported store objects corresponding to their addresses,
even where this identity is not observable from within WebAssembly code itself
(such as for function instances or immutable globals).
Note
Addresses are dynamic, globally unique references to runtime objects,
in contrast to indices,
which are static, module-local references to their original definitions.
A memory address \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}\) denotes the abstract address of a memory instance in the store,
not an offset inside a memory instance.
There is no specific limit on the number of allocations of store objects,
hence logical addresses can be arbitrarily large natural numbers.
External Addresses
An external address is the runtime address of an entity that can be imported or exported.
It is an address denoting either a
function instance,
global instances,
table instance,
memory instance, or
tag instances
in the shared store.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}} & ::= & \href{../exec/runtime.html#syntax-externaddr}{\mathsf{func}}~{\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}} ~|~ \href{../exec/runtime.html#syntax-externaddr}{\mathsf{global}}~{\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}} ~|~ \href{../exec/runtime.html#syntax-externaddr}{\mathsf{table}}~{\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}} ~|~ \href{../exec/runtime.html#syntax-externaddr}{\mathsf{mem}}~{\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}} ~|~ \href{../exec/runtime.html#syntax-externaddr}{\mathsf{tag}}~{\href{../exec/runtime.html#syntax-tagaddr}{\mathit{tagaddr}}} \\
\end{array}\end{split}\]
Module Instances
A module instance is the runtime representation of a module.
It is created by instantiating a module,
and collects runtime representations of all entities that are imported, defined, or exported by the module.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}~{{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}^\ast} \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcs}}~{{\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}}^\ast} \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}~{{\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}}^\ast} \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tables}}~{{\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}}^\ast} \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{mems}}~{{\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}}^\ast} \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tags}}~{{\href{../exec/runtime.html#syntax-tagaddr}{\mathit{tagaddr}}}^\ast} \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elems}}~{{\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}}^\ast} \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{datas}}~{{\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}}^\ast} \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}~{{\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}}^\ast} \} \\
\end{array} \\
\end{array}\end{split}\]
Each component references runtime instances corresponding to respective declarations from the original module – whether imported or defined – in the order of their static indices.
Function instances,
table instances,
memory instances,
global instances, and
tag instances
are referenced with an indirection through their respective addresses in the store.
It is an invariant of the semantics that all export instances in a given module instance have different names.
Function Instances
A function instance is the runtime representation of a function.
It effectively is a closure of the original function over the runtime module instance of its originating module.
The module instance is used to resolve references to other definitions during execution of the function.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} \href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}} \href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}~{{\href{../exec/runtime.html#syntax-funcinst}{\mathit{code}}}} \} \\
\end{array} \\
& {{\href{../exec/runtime.html#syntax-funcinst}{\mathit{code}}}} & ::= & {\href{../syntax/modules.html#syntax-func}{\mathit{func}}} ~|~ {\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}} \\
\end{array}\end{split}\]
A host function is a function expressed outside WebAssembly but passed to a module as an import.
The definition and behavior of host functions are outside the scope of this specification.
For the purpose of this specification, it is assumed that when invoked,
a host function behaves non-deterministically,
but within certain constraints that ensure the integrity of the runtime.
Note
Function instances are immutable, and their identity is not observable by WebAssembly code.
However, the embedder might provide implicit or explicit means for distinguishing their addresses.
Table Instances
A table instance is the runtime representation of a table.
It records its type and holds a sequence of reference values.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}} \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~{{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}^\ast} \} \\
\end{array} \\
\end{array}\end{split}\]
Table elements can be mutated through table instructions, the execution of an active element segment, or by external means provided by the embedder.
It is an invariant of the semantics that all table elements have a type matching the element type of \({\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}\).
It also is an invariant that the length of the element sequence never exceeds the maximum size of \({\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}\), if present.
Memory Instances
A memory instance is the runtime representation of a linear memory.
It records its type and holds a sequence of bytes.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~{\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}} \href{../exec/runtime.html#syntax-meminst}{\mathsf{bytes}}~{{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast} \} \\
\end{array} \\
\end{array}\end{split}\]
The length of the sequence always is a multiple of the WebAssembly page size, which is defined to be the constant \(65536\) – abbreviated \({64^\ast}~{\mathrm{Ki}}\).
The bytes can be mutated through memory instructions, the execution of an active data segment, or by external means provided by the embedder.
It is an invariant of the semantics that the length of the byte sequence, divided by page size, never exceeds the maximum size of \({\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}}\).
Global Instances
A global instance is the runtime representation of a global variable.
It records its type and holds an individual value.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}} \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~{\href{../exec/runtime.html#syntax-val}{\mathit{val}}} \} \\
\end{array} \\
\end{array}\end{split}\]
The value of mutable globals can be mutated through variable instructions or by external means provided by the embedder.
It is an invariant of the semantics that the value has a type matching the value type of \({\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}\).
Tag Instances
A tag instance is the runtime representation of a tag definition.
It records the defined type of the tag.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-taginst}{\mathit{taginst}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-taginst}{\mathsf{type}}~{\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}} \} \\
\end{array} \\
\end{array}\end{split}\]
Element Instances
An element instance is the runtime representation of an element segment.
It holds a list of references and their common type.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~{\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}} \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~{{\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}}^\ast} \} \\
\end{array} \\
\end{array}\end{split}\]
Data Instances
An data instance is the runtime representation of a data segment.
It holds a list of bytes.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-datainst}{\mathsf{bytes}}~{{\href{../syntax/values.html#syntax-byte}{\mathit{byte}}}^\ast} \} \\
\end{array} \\
\end{array}\end{split}\]
Export Instances
An export instance is the runtime representation of an export.
It defines the export’s name and the associated external address.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}} \href{../exec/runtime.html#syntax-exportinst}{\mathsf{addr}}~{\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}} \} \\
\end{array} \\
\end{array}\end{split}\]
Conventions
The following auxiliary notation is defined for sequences of external addresses.
It filters out entries of a specific kind in an order-preserving fashion:
\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}}
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{funcs}}}(\epsilon) & = & \epsilon \\
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{funcs}}}((\href{../exec/runtime.html#syntax-externaddr}{\mathsf{func}}~a)~{{\mathit{xa}}^\ast}) & = & a~{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{funcs}}}({{\mathit{xa}}^\ast}) \\
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{funcs}}}({\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}~{{\mathit{xa}}^\ast}) & = & {\href{../exec/runtime.html#syntax-externaddr}{\mathrm{funcs}}}({{\mathit{xa}}^\ast}) & \mbox{otherwise} \\[0.8ex]
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tables}}}(\epsilon) & = & \epsilon \\
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tables}}}((\href{../exec/runtime.html#syntax-externaddr}{\mathsf{table}}~a)~{{\mathit{xa}}^\ast}) & = & a~{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tables}}}({{\mathit{xa}}^\ast}) \\
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tables}}}({\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}~{{\mathit{xa}}^\ast}) & = & {\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tables}}}({{\mathit{xa}}^\ast}) & \mbox{otherwise} \\[0.8ex]
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{mems}}}(\epsilon) & = & \epsilon \\
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{mems}}}((\href{../exec/runtime.html#syntax-externaddr}{\mathsf{mem}}~a)~{{\mathit{xa}}^\ast}) & = & a~{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{mems}}}({{\mathit{xa}}^\ast}) \\
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{mems}}}({\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}~{{\mathit{xa}}^\ast}) & = & {\href{../exec/runtime.html#syntax-externaddr}{\mathrm{mems}}}({{\mathit{xa}}^\ast}) & \mbox{otherwise} \\[0.8ex]
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{globals}}}(\epsilon) & = & \epsilon \\
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{globals}}}((\href{../exec/runtime.html#syntax-externaddr}{\mathsf{global}}~a)~{{\mathit{xa}}^\ast}) & = & a~{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{globals}}}({{\mathit{xa}}^\ast}) \\
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{globals}}}({\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}~{{\mathit{xa}}^\ast}) & = & {\href{../exec/runtime.html#syntax-externaddr}{\mathrm{globals}}}({{\mathit{xa}}^\ast}) & \mbox{otherwise} \\[0.8ex]
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tags}}}(\epsilon) & = & \epsilon \\
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tags}}}((\href{../exec/runtime.html#syntax-externaddr}{\mathsf{tag}}~a)~{{\mathit{xa}}^\ast}) & = & a~{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tags}}}({{\mathit{xa}}^\ast}) \\
{\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tags}}}({\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}}~{{\mathit{xa}}^\ast}) & = & {\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tags}}}({{\mathit{xa}}^\ast}) & \mbox{otherwise} \\
\end{array}\end{split}\]
Aggregate Instances
A structure instance is the runtime representation of a heap object allocated from a structure type.
Likewise, an array instance is the runtime representation of a heap object allocated from an array type.
Both record their respective defined type and hold a list of the values of their fields.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-structinst}{\mathit{structinst}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-structinst}{\mathsf{type}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} \href{../exec/runtime.html#syntax-structinst}{\mathsf{fields}}~{{\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}}^\ast} \} \\
\end{array} \\
& {\href{../exec/runtime.html#syntax-arrayinst}{\mathit{arrayinst}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-arrayinst}{\mathsf{type}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} \href{../exec/runtime.html#syntax-arrayinst}{\mathsf{fields}}~{{\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}}^\ast} \} \\
\end{array} \\
& {\href{../exec/runtime.html#syntax-fieldval}{\mathit{fieldval}}} & ::= & {\href{../exec/runtime.html#syntax-val}{\mathit{val}}} ~|~ {\href{../exec/runtime.html#syntax-packval}{\mathit{packval}}} \\
& {\href{../exec/runtime.html#syntax-packval}{\mathit{packval}}} & ::= & {\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}{.}\href{../exec/runtime.html#syntax-packval}{\mathsf{pack}}~{{\href{../syntax/values.html#syntax-int}{\mathit{i}\kern-0.1em}}}{N} \\
\end{array}\end{split}\]
Conventions
Conversion of a regular value to a field value is defined as follows:
\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}}
{{\href{../exec/runtime.html#aux-packfield}{\mathrm{pack}}}}_{{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}}({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}) & = & {\href{../exec/runtime.html#syntax-val}{\mathit{val}}} \\
{{\href{../exec/runtime.html#aux-packfield}{\mathrm{pack}}}}_{{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}}(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i) & = & {\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}{.}\href{../exec/runtime.html#syntax-packval}{\mathsf{pack}}~{{\href{../exec/numerics.html#op-wrap}{\mathrm{wrap}}}}_{32, {|{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}|}}(i) \\
\end{array}\end{split}\]
The inverse conversion of a field value to a regular value is defined as follows:
\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}}
{{{{\href{../exec/runtime.html#aux-unpackfield}{\mathrm{unpack}}}}_{{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}}^{\epsilon}}}{({\href{../exec/runtime.html#syntax-val}{\mathit{val}}})} & = & {\href{../exec/runtime.html#syntax-val}{\mathit{val}}} \\
{{{{\href{../exec/runtime.html#aux-unpackfield}{\mathrm{unpack}}}}_{{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}}^{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}}}}{({\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}{.}\href{../exec/runtime.html#syntax-packval}{\mathsf{pack}}~i)} & = & \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~{{{{\href{../exec/numerics.html#op-ext}{\mathrm{extend}}}}_{{|{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}|}, 32}^{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}}}}{(i)} \\
\end{array}\end{split}\]
Exception Instances
An exception instance is the runtime representation of an exception produced by a \(\mathsf{throw}\) instruction.
It holds the address of the respective tag and the argument values.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-exninst}{\mathit{exninst}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-exninst}{\mathsf{tag}}~{\href{../exec/runtime.html#syntax-tagaddr}{\mathit{tagaddr}}} \href{../exec/runtime.html#syntax-exninst}{\mathsf{fields}}~{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast} \} \\
\end{array} \\
\end{array}\end{split}\]
Stack
Besides the store, most instructions interact with an implicit stack.
The stack contains the following kinds of entries:
Values: the operands of instructions.
Labels: active structured control instructions that can be targeted by branches.
Frames: the call frames of active function calls.
Handlers: active exception handlers.
These entries can occur on the stack in any order during the execution of a program.
Stack entries are described by abstract syntax as follows.
Note
It is possible to model the WebAssembly semantics using separate stacks for operands, control constructs, and calls.
However, because the stacks are interdependent, additional book keeping about associated stack heights would be required.
For the purpose of this specification, an interleaved representation is simpler.
Labels
Labels carry an argument arity \(n\) and their associated branch target, which is expressed syntactically as an instruction sequence:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-label}{\mathit{label}}} & ::= & {{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{n}}{\{ {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \}} \\
\end{array}\end{split}\]
Intuitively, \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is the continuation to execute when the branch is taken, in place of the original control construct.
Note
For example, a loop label has the form
\[{{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{n}}{\{ (\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~{\mathit{bt}}~\dots) \}}\]
When performing a branch to this label, this executes the loop, effectively restarting it from the beginning.
Conversely, a simple block label has the form
\[{{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{n}}{\{ \epsilon \}}\]
When branching, the empty continuation ends the targeted block, such that execution can proceed with consecutive instructions.
Call Frames
Call frames carry the return arity \(n\) of the respective function,
hold the values of its locals (including arguments) in the order corresponding to their static local indices,
and a reference to the function’s own module instance:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-callframe}{\mathit{callframe}}} & ::= & {{\href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}}_{n}}{\{ {\href{../exec/runtime.html#syntax-frame}{\mathit{frame}}} \}} \\
& {\href{../exec/runtime.html#syntax-frame}{\mathit{frame}}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}}
\href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~{({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^?})^\ast} \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}} \} \\
\end{array} \\
\end{array}\end{split}\]
Locals may be uninitialized, in which case they are empty.
Locals are mutated by respective variable instructions.
Exception Handlers
Exception handlers are installed by \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try\_table}}\) instructions and record the corresponding list of catch clauses:
\[\begin{array}{llllll}
\def\mathdef2139#1{{}}\mathdef2139{handler} & \href{../exec/runtime.html#syntax-handler}{\mathit{handler}} &::=&
\href{../exec/runtime.html#syntax-handler}{\mathsf{handler}}_n\{\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast\}
\end{array}\]
The handlers on the stack are searched when an exception is thrown.
Conventions
The meta variable \(L\) ranges over labels where clear from context.
The meta variable \(f\) ranges over frame states where clear from context.
The meta variable \(H\) ranges over exception handlers where clear from context.
The following auxiliary definition takes a block type and looks up the instruction type that it denotes in the current frame:
\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}}
{{\href{../exec/runtime.html#aux-blocktype}{\mathrm{instrtype}}}}_{z}(x) & = & {\mathit{ft}} & \quad \mbox{if}~ z{.}\href{../exec/runtime.html#syntax-store}{\mathsf{types}}{}[x] \href{../valid/conventions.html#aux-expand-deftype}{\approx} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\mathit{ft}} \\
{{\href{../exec/runtime.html#aux-blocktype}{\mathrm{instrtype}}}}_{z}({t^?}) & = & \epsilon \href{../syntax/types.html#syntax-functype}{\rightarrow} {t^?} \\
\end{array}\end{split}\]
Administrative Instructions
In order to express the reduction of traps, calls, exception handling, and control instructions, the syntax of instructions is extended to include the following administrative instructions:
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}} & ::= & \dots \\
& & | & {\href{../exec/runtime.html#syntax-addrref}{\mathit{addrref}}} \\
& & | & {{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{n}}{\{ {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \\
& & | & {{\href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}}_{n}}{\{ {\href{../exec/runtime.html#syntax-frame}{\mathit{frame}}} \}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \\
& & | & {{\href{../exec/runtime.html#syntax-handler}{\mathsf{handler}}}_{n}}{\{ {{\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}}^\ast} \}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \\
& & | & \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\
\end{array}\end{split}\]
An address reference represents an allocated reference value of respective form “on the stack”.
The \(\mathsf{label}\), \(\mathsf{frame}\), and \(\mathsf{handler}\) instructions model labels, frames, and active exception handlers, respectively, “on the stack”.
Moreover, the administrative syntax maintains the nesting structure of the original structured control instruction or function body and their instruction sequences.
The \(\mathsf{trap}\) instruction represents the occurrence of a trap.
Traps are bubbled up through nested instruction sequences, ultimately reducing the entire program to a single \(\mathsf{trap}\) instruction, signalling abrupt termination.
Note
For example, the reduction rule for \(\mathsf{block}\) is:
\[(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}) \href{../exec/conventions.html#exec-notation}{\hookrightarrow} ({{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{n}}{\{ \epsilon \}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})\]
if the block type \({\mathit{bt}}\) denotes a function type \({t_1^{m}} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^{n}}\),
such that \(n\) is the block’s result arity.
This rule replaces the block with a label instruction,
which can be interpreted as “pushing” the label on the stack.
When its end is reached, i.e., the inner instruction sequence has been reduced to the empty sequence – or rather, a sequence of \(n\) values representing the results – then the \(\mathsf{label}\) instruction is eliminated courtesy of its own reduction rule:
\[({{\href{../exec/runtime.html#syntax-label}{\mathsf{label}}}_{n}}{\{ {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \}}~{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}) \href{../exec/conventions.html#exec-notation}{\hookrightarrow} {{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}\]
This can be interpreted as removing the label from the stack and only leaving the locally accumulated operand values.
Validation guarantees that \(n\) matches the number \({|{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}|}\) of resulting values at this point.
Configurations
A configuration describes the current computation.
It consists of the computations’s state and the sequence of instructions left to execute.
The state in turn consists of a global store and a current frame referring to the module instance in which the computation runs, i.e., where the current function originates from.
\[\begin{split}\begin{array}[t]{@{}l@{}rrl@{}l@{}}
& {\href{../exec/runtime.html#syntax-config}{\mathit{config}}} & ::= & {\href{../exec/runtime.html#syntax-state}{\mathit{state}}} ; {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} \\[0.8ex]
& {\href{../exec/runtime.html#syntax-state}{\mathit{state}}} & ::= & {\href{../exec/runtime.html#syntax-store}{\mathit{store}}} ; {\href{../exec/runtime.html#syntax-frame}{\mathit{frame}}} \\
\end{array}\end{split}\]
Note
The current version of WebAssembly is single-threaded,
but configurations with multiple threads may be supported in the future.
