Modules¶
For modules, the execution semantics primarily defines instantiation, which allocates instances for a module and its contained definitions, initializes tables and memories from contained element and data segments, and invokes the start function if present. It also includes invocation of exported functions.
Instantiation depends on a number of auxiliary notions for type-checking imports and allocating instances.
External Typing¶
For the purpose of checking external values against imports,
such values are classified by external types.
The following auxiliary typing rules specify this typing relation relative to a store
¶
The store entry
must exist.Then
is valid with external type .
¶
The store entry
must exist.Then
is valid with external type .
¶
The store entry
must exist.Then
is valid with external type .
¶
The store entry
must exist.Then
is valid with external type .
Value Typing¶
For the purpose of checking argument values against the parameter types of exported functions,
values are classified by value types.
The following auxiliary typing rules specify this typing relation relative to a store
Numeric Values ¶
The value is valid with number type
.
Null References ¶
The value is valid with reference type
.
Function References ¶
The external value
must be valid.Then the value is valid with reference type
.
External References ¶
The value is valid with reference type
.
Allocation¶
New instances of functions, tables, memories, and globals are allocated in a store
Functions¶
Let
be the function to allocate and its module instance.Let
be the first free function address in .Let
be the function type .Let
be the function instance .Append
to the of .Return
.
Host Functions¶
Let
be the host function to allocate and its function type.Let
be the first free function address in .Let
be the function instance .Append
to the of .Return
.
Note
Host functions are never allocated by the WebAssembly semantics itself, but may be allocated by the embedder.
Tables¶
Let
be the table type to allocate and the initialization value.Let
be the structure of table type .Let
be the first free table address in .Let
be the table instance with elements set to .Append
to the of .Return
.
Memories¶
Let
be the memory type to allocate.Let
be the structure of memory type .Let
be the first free memory address in .Let
be the memory instance that contains pages of zeroed bytes.Append
to the of .Return
.
Globals¶
Let
be the global type to allocate and the value to initialize the global with.Let
be the first free global address in .Let
be the global instance .Append
to the of .Return
.
Element segments¶
Let
be the elements’ type and the vector of references to allocate.Let
be the first free element address in .Let
be the element instance .Append
to the of .Return
.
Data segments¶
Let
be the vector of bytes to allocate.Let
be the first free data address in .Let
be the data instance .Append
to the of .Return
.
Growing tables¶
Let
be the table instance to grow, the number of elements by which to grow it, and the initialization value.Let
be added to the length of .If
is larger than or equal to , then fail.Let
be the structure of table type .Let
be with updated to .If
is not valid, then fail.Append
to .Set
to the table type .
Growing memories¶
Let
be the memory instance to grow and the number of pages by which to grow it.Assert: The length of
is divisible by the page size .Let
be added to the length of divided by the page size .If
is larger than , then fail.Let
be the structure of memory type .Let
be with updated to .If
is not valid, then fail.Append
times bytes with value to .Set
to the memory type .
Modules¶
The allocation function for modules requires a suitable list of external values that are assumed to match the import vector of the module, a list of initialization values for the module’s globals, and list of reference vectors for the module’s element segments.
Let
be the module to allocate and the vector of external values providing the module’s imports, the initialization values of the module’s globals, and the reference vectors of the module’s element segments.For each function
in , do:Let
be the function address resulting from allocating for the module instance defined below.
For each table
in , do:Let
be the table type .Let
be the table address resulting from allocating with initialization value .
For each memory
in , do:Let
be the memory address resulting from allocating .
For each global
in , do:Let
be the global address resulting from allocating with initializer value .
For each element segment
in , do:Let
be the element address resulting from allocating an element instance of reference type with contents .
For each data segment
in , do:Let
be the data address resulting from allocating a data instance with contents .
Let
be the concatenation of the function addresses in index order.Let
be the concatenation of the table addresses in index order.Let
be the concatenation of the memory addresses in index order.Let
be the concatenation of the global addresses in index order.Let
be the concatenation of the element addresses in index order.Let
be the concatenation of the data addresses in index order.Let
be the list of function addresses extracted from , concatenated with .Let
be the list of table addresses extracted from , concatenated with .Let
be the list of memory addresses extracted from , concatenated with .Let
be the list of global addresses extracted from , concatenated with .For each export
in , do:If
is a function export for function index , then let be the external value .Else, if
is a table export for table index , then let be the external value .Else, if
is a memory export for memory index , then let be the external value .Else, if
is a global export for global index , then let be the external value .Let
be the export instance .
Let
be the concatenation of the export instances in index order.Let
be the module instance .Return
.
where:
Here, the notation
Moreover, if the dots
Note
The definition of module allocation is mutually recursive with the allocation of its associated functions, because the resulting module instance
Instantiation¶
Given a store
Instantiation checks that the module is valid and the provided imports match the declared types, and may fail with an error otherwise. Instantiation can also result in a trap from initializing a table or memory from an active segment or from executing the start function. It is up to the embedder to define how such conditions are reported.
If
is not valid, then:Fail.
Assert:
is valid with external types classifying its imports.If the number
of imports is not equal to the number of provided external values, then:Fail.
For each external value
in and external type in , do:If
is not valid with an external type in store , then:Fail.
If
does not match , then:Fail.
Let
be the auxiliary module instance that only consists of the imported globals and the imported and allocated functions from the final module instance , defined below.Let
be the auxiliary frame .Push the frame
to the stack.Let
be the vector of global initialization values determined by and . These may be calculated as follows.For each global
in , do:Let
be the result of evaluating the initializer expression .
Assert: due to validation, the frame
is now on the top of the stack.Let
be the concatenation of in index order.
Let
be the list of reference vectors determined by the element segments in . These may be calculated as follows.For each element segment
in , and for each element expression in , do:Let
be the result of evaluating the initializer expression .
Let
be the concatenation of function elements in order of index .Let
be the concatenation of function element vectors in order of index .
Pop the frame
from the stack.Let
be a new module instance allocated from in store with imports , global initializer values , and element segment contents , and let be the extended store produced by module allocation.Let
be the auxiliary frame .Push the frame
to the stack.For each element segment
in whose mode is of the form , do:For each element segment
in whose mode is of the form , do:Execute the instruction
.
For each data segment
in whose mode is of the form , do:If the start function
is not empty, then:Let
be the start function .Execute the instruction
.
Assert: due to validation, the frame
is now on the top of the stack.Pop the frame
from the stack.
where:
Note
Module allocation and the evaluation of global initializers and element segments are mutually recursive because the global initialization values
All failure conditions are checked before any observable mutation of the store takes place. Store mutation is not atomic; it happens in individual steps that may be interleaved with other threads.
Evaluation of constant expressions does not affect the store.
Invocation¶
Once a module has been instantiated, any exported function can be invoked externally via its function address
Invocation may fail with an error if the arguments do not fit the function type. Invocation can also result in a trap. It is up to the embedder to define how such conditions are reported.
Note
If the embedder API performs type checks itself, either statically or dynamically, before performing an invocation, then no failure other than traps can occur.
The following steps are performed:
Assert:
exists.Let
be the function instance .Let
be the function type .If the length
of the provided argument values is different from the number of expected arguments, then:Fail.
For each value type
in and corresponding value in , do:If
is not valid with value type , then:Fail.
Let
be the dummy frame .Push the frame
to the stack.Push the values
to the stack.Invoke the function instance at address
.
Once the function has returned, the following steps are executed:
Assert: due to validation,
values are on the top of the stack.Pop
from the stack.Assert: due to validation, the frame
is now on the top of the stack.Pop the frame
from the stack.
The values