1. Introduction
1.1. Introduction
WebAssembly (abbreviated Wasm [1]) is a safe, portable, low-level code format designed for efficient execution and compact representation. Its main goal is to enable high performance applications on the Web, but it does not make any Web-specific assumptions or provide Web-specific features, so it can be employed in other environments as well.
WebAssembly is an open standard developed by a W3C Community Group.
This document describes version 3.0 (Draft 2024-11-07) of the core WebAssembly standard. It is intended that it will be superseded by new incremental releases with additional features in the future.
1.1.1. Design Goals
The design goals of WebAssembly are the following:
-
Fast, safe, and portable semantics:
-
Fast: executes with near native code performance, taking advantage of capabilities common to all contemporary hardware.
-
Safe: code is validated and executes in a memory-safe [2], sandboxed environment preventing data corruption or security breaches.
-
Well-defined: fully and precisely defines valid programs and their behavior in a way that is easy to reason about informally and formally.
-
Hardware-independent: can be compiled on all modern architectures, desktop or mobile devices and embedded systems alike.
-
Language-independent: does not privilege any particular language, programming model, or object model.
-
Platform-independent: can be embedded in browsers, run as a stand-alone VM, or integrated in other environments.
-
Open: programs can interoperate with their environment in a simple and universal manner.
-
-
Efficient and portable representation:
-
Compact: has a binary format that is fast to transmit by being smaller than typical text or native code formats.
-
Modular: programs can be split up in smaller parts that can be transmitted, cached, and consumed separately.
-
Efficient: can be decoded, validated, and compiled in a fast single pass, equally with either just-in-time (JIT) or ahead-of-time (AOT) compilation.
-
Streamable: allows decoding, validation, and compilation to begin as soon as possible, before all data has been seen.
-
Parallelizable: allows decoding, validation, and compilation to be split into many independent parallel tasks.
-
Portable: makes no architectural assumptions that are not broadly supported across modern hardware.
-
WebAssembly code is also intended to be easy to inspect and debug, especially in environments like web browsers, but such features are beyond the scope of this specification.
1.1.2. Scope
At its core, WebAssembly is a virtual instruction set architecture (virtual ISA). As such, it has many use cases and can be embedded in many different environments. To encompass their variety and enable maximum reuse, the WebAssembly specification is split and layered into several documents.
This document is concerned with the core ISA layer of WebAssembly. It defines the instruction set, binary encoding, validation, and execution semantics, as well as a textual representation. It does not, however, define how WebAssembly programs can interact with a specific environment they execute in, nor how they are invoked from such an environment.
Instead, this specification is complemented by additional documents defining interfaces to specific embedding environments such as the Web. These will each define a WebAssembly application programming interface (API) suitable for a given environment.
1.1.3. Security Considerations
WebAssembly provides no ambient access to the computing environment in which code is executed. Any interaction with the environment, such as I/O, access to resources, or operating system calls, can only be performed by invoking functions provided by the embedder and imported into a WebAssembly module. An embedder can establish security policies suitable for a respective environment by controlling or limiting which functional capabilities it makes available for import. Such considerations are an embedder’s responsibility and the subject of API definitions for a specific environment.
Because WebAssembly is designed to be translated into machine code running directly on the host’s hardware, it is potentially vulnerable to side channel attacks on the hardware level. In environments where this is a concern, an embedder may have to put suitable mitigations into place to isolate WebAssembly computations.
1.1.4. Dependencies
WebAssembly depends on two existing standards:
-
[IEEE-754-2019], for the representation of floating-point data and the semantics of respective numeric operations.
-
[UNICODE], for the representation of import/export names and the text format.
However, to make this specification self-contained, relevant aspects of the aforementioned standards are defined and formalized as part of this specification, such as the binary representation and rounding of floating-point values, and the value range and UTF-8 encoding of Unicode characters.
Note
The aforementioned standards are the authoritative source of all respective definitions. Formalizations given in this specification are intended to match these definitions. Any discrepancy in the syntax or semantics described is to be considered an error.
1.2. Overview
1.2.1. Concepts
WebAssembly encodes a low-level, assembly-like programming language. This language is structured around the following concepts.
- Values
-
WebAssembly provides only four basic number types. These are integers and [IEEE-754-2019] numbers, each in 32 and 64 bit width. 32 bit integers also serve as Booleans and as memory addresses. The usual operations on these types are available, including the full matrix of conversions between them. There is no distinction between signed and unsigned integer types. Instead, integers are interpreted by respective operations as either unsigned or signed in two’s complement representation.
In addition to these basic number types, there is a single 128 bit wide vector type representing different types of packed data. The supported representations are 4 32-bit, or 2 64-bit [IEEE-754-2019] numbers, or different widths of packed integer values, specifically 2 64-bit integers, 4 32-bit integers, 8 16-bit integers, or 16 8-bit integers.
Finally, values can consist of opaque references that represent pointers towards different sorts of entities. Unlike with other types, their size or representation is not observable.
- Instructions
-
The computational model of WebAssembly is based on a stack machine. Code consists of sequences of instructions that are executed in order. Instructions manipulate values on an implicit operand stack [1] and fall into two main categories. Simple instructions perform basic operations on data. They pop arguments from the operand stack and push results back to it. Control instructions alter control flow. Control flow is structured, meaning it is expressed with well-nested constructs such as blocks, loops, and conditionals. Branches can only target such constructs.
- Traps
-
Under some conditions, certain instructions may produce a trap, which immediately aborts execution. Traps cannot be handled by WebAssembly code, but are reported to the outside environment, where they typically can be caught.
- Functions
-
Code is organized into separate functions. Each function takes a sequence of values as parameters and returns a sequence of values as results. Functions can call each other, including recursively, resulting in an implicit call stack that cannot be accessed directly. Functions may also declare mutable local variables that are usable as virtual registers.
- Tables
-
A table is an array of opaque values of a particular reference type. It allows programs to select such values indirectly through a dynamic index operand. Thereby, for example, a program can call functions indirectly through a dynamic index into a table. This allows emulating function pointers by way of table indices.
- Linear Memory
-
A linear memory is a contiguous, mutable array of raw bytes. Such a memory is created with an initial size but can be grown dynamically. A program can load and store values from/to a linear memory at any byte address (including unaligned). Integer loads and stores can specify a storage size which is smaller than the size of the respective value type. A trap occurs if an access is not within the bounds of the current memory size.
- Modules
-
A WebAssembly binary takes the form of a module that contains definitions for functions, tables, and linear memories, as well as mutable or immutable global variables. Definitions can also be imported, specifying a module/name pair and a suitable type. Each definition can optionally be exported under one or more names. In addition to definitions, modules can define initialization data for their memories or tables that takes the form of segments copied to given offsets. They can also define a start function that is automatically executed.
- Embedder
-
A WebAssembly implementation will typically be embedded into a host environment. This environment defines how loading of modules is initiated, how imports are provided (including host-side definitions), and how exports can be accessed. However, the details of any particular embedding are beyond the scope of this specification, and will instead be provided by complementary, environment-specific API definitions.
In practice, implementations need not maintain an actual operand stack. Instead, the stack can be viewed as a set of anonymous registers that are implicitly referenced by instructions. The type system ensures that the stack height, and thus any referenced register, is always known statically.
1.2.2. Semantic Phases
Conceptually, the semantics of WebAssembly is divided into three phases. For each part of the language, the specification specifies each of them.
- Decoding
-
WebAssembly modules are distributed in a binary format. Decoding processes that format and converts it into an internal representation of a module. In this specification, this representation is modelled by abstract syntax, but a real implementation could compile directly to machine code instead.
- Validation
-
A decoded module has to be valid. Validation checks a number of well-formedness conditions to guarantee that the module is meaningful and safe. In particular, it performs type checking of functions and the instruction sequences in their bodies, ensuring for example that the operand stack is used consistently.
- Execution
-
Finally, a valid module can be executed. Execution can be further divided into two phases:
Instantiation. A module instance is the dynamic representation of a module, complete with its own state and execution stack. Instantiation executes the module body itself, given definitions for all its imports. It initializes globals, memories and tables and invokes the module’s start function if defined. It returns the instances of the module’s exports.
Invocation. Once instantiated, further WebAssembly computations can be initiated by invoking an exported function on a module instance. Given the required arguments, that executes the respective function and returns its results.
Instantiation and invocation are operations within the embedding environment.
2. Structure
2.1. Conventions
WebAssembly is a programming language that has multiple concrete representations (its binary format and the text format). Both map to a common structure. For conciseness, this structure is described in the form of an abstract syntax. All parts of this specification are defined in terms of this abstract syntax.
2.1.1. Grammar Notation
The following conventions are adopted in defining grammar rules for abstract syntax.
-
Terminal symbols (atoms) are written in sans-serif font or in symbolic form: .
-
Nonterminal symbols are written in italic font: .
-
is a sequence of iterations of .
-
is a possibly empty sequence of iterations of . (This is a shorthand for used where is not relevant.)
-
is a non-empty sequence of iterations of . (This is a shorthand for where .)
-
is an optional occurrence of . (This is a shorthand for where .)
-
Productions are written .
-
Large productions may be split into multiple definitions, indicated by ending the first one with explicit ellipses, , and starting continuations with ellipses, .
-
Some productions are augmented with side conditions in parentheses, “”, that provide a shorthand for a combinatorial expansion of the production into many separate cases.
-
If the same meta variable or non-terminal symbol appears multiple times in a production, then all those occurrences must have the same instantiation. (This is a shorthand for a side condition requiring multiple different variables to be equal.)
2.1.2. Auxiliary Notation
When dealing with syntactic constructs the following notation is also used:
-
denotes the empty sequence.
-
denotes the length of a sequence .
-
denotes the -th element of a sequence , starting from .
-
denotes the sub-sequence of a sequence .
-
denotes the same sequence as , except that the -th element is replaced with .
-
denotes the same sequence as , except that the sub-sequence is replaced with .
-
denotes the flat sequence formed by concatenating all sequences in .
Moreover, the following conventions are employed:
-
The notation , where is a non-terminal symbol, is treated as a meta variable ranging over respective sequences of (similarly for , , ).
-
When given a sequence , then the occurrences of in a sequence written are assumed to be in point-wise correspondence with (similarly for , , ). This implicitly expresses a form of mapping syntactic constructions over a sequence.
Productions of the following form are interpreted as records that map a fixed set of fields to “values” , respectively:
The following notation is adopted for manipulating such records:
-
denotes the contents of the component of .
-
denotes the same record as , except that the contents of the component is replaced with .
-
denotes the composition of two records with the same fields of sequences by appending each sequence point-wise:
-
denotes the composition of a sequence of records, respectively; if the sequence is empty, then all fields of the resulting record are empty.
The update notation for sequences and records generalizes recursively to nested components accessed by “paths” :
-
is short for ,
-
is short for ,
where is shortened to .
2.1.3. Vectors
Vectors are bounded sequences of the form (or ), where the can either be values or complex constructions. A vector can have at most elements.
2.2. Values
WebAssembly programs operate on primitive numeric values. Moreover, in the definition of programs, immutable sequences of values occur to represent more complex data, such as text strings or other vectors.
2.2.1. Bytes
The simplest form of value are raw uninterpreted bytes. In the abstract syntax they are represented as hexadecimal literals.
2.2.1.1. Conventions
-
The meta variable ranges over bytes.
-
Bytes are sometimes interpreted as natural numbers .
2.2.2. Integers
Different classes of integers with different value ranges are distinguished by their bit width and by whether they are unsigned or signed.
The class defines uninterpreted integers, whose signedness interpretation can vary depending on context. In the abstract syntax, they are represented as unsigned values. However, some operations convert them to signed based on a two’s complement interpretation.
Note
The main integer types occurring in this specification are , , , , , , , . However, other sizes occur as auxiliary constructions, e.g., in the definition of floating-point numbers.
2.2.2.1. Conventions
-
The meta variables range over integers.
-
Numbers may be denoted by simple arithmetics, as in the grammar above. In order to distinguish arithmetics like from sequences like , the latter is distinguished with parentheses.
2.2.3. Floating-Point
Floating-point data represents 32 or 64 bit values that correspond to the respective binary formats of the [IEEE-754-2019] standard (Section 3.3).
Every value has a sign and a magnitude. Magnitudes can either be expressed as normal numbers of the form , where is the exponent and is the significand whose most significant bit is , or as a subnormal number where the exponent is fixed to the smallest possible value and is ; among the subnormals are positive and negative zero values. Since the significands are binary values, normals are represented in the form , where is the bit width of ; similarly for subnormals.
Possible magnitudes also include the special values (infinity) and (NaN, not a number). NaN values have a payload that describes the mantissa bits in the underlying binary representation. No distinction is made between signalling and quiet NaNs.
where and with
A canonical NaN is a floating-point value where is a payload whose most significant bit is while all others are :
An arithmetic NaN is a floating-point value with , such that the most significant bit is while all others are arbitrary.
Note
In the abstract syntax, subnormals are distinguished by the leading 0 of the significand. The exponent of subnormals has the same value as the smallest possible exponent of a normal number. Only in the binary representation the exponent of a subnormal is encoded differently than the exponent of any normal number.
The notion of canonical NaN defined here is unrelated to the notion of canonical NaN that the [IEEE-754-2019] standard (Section 3.5.2) defines for decimal interchange formats.
2.2.3.1. Conventions
-
The meta variable ranges over floating-point values where clear from context.
2.2.4. Vectors
Numeric vectors are 128-bit values that are processed by vector instructions (also known as SIMD instructions, single instruction multiple data). They are represented in the abstract syntax using . The interpretation of lane types (integer or floating-point numbers) and lane sizes are determined by the specific instruction operating on them.
2.2.5. Names
Names are sequences of characters, which are scalar values as defined by [UNICODE] (Section 2.4).
Due to the limitations of the binary format, the length of a name is bounded by the length of its UTF-8 encoding.
2.2.5.1. Convention
-
Characters (Unicode scalar values) are sometimes used interchangeably with natural numbers .
2.3. Types
Various entities in WebAssembly are classified by types. Types are checked during validation, instantiation, and possibly execution.
2.3.1. Number Types
Number types classify numeric values.
The types and classify 32 and 64 bit integers, respectively. Integers are not inherently signed or unsigned, their interpretation is determined by individual operations.
The types and classify 32 and 64 bit floating-point data, respectively. They correspond to the respective binary floating-point representations, also known as single and double precision, as defined by the [IEEE-754-2019] standard (Section 3.3).
Number types are transparent, meaning that their bit patterns can be observed. Values of number type can be stored in memories.
2.3.1.1. Conventions
-
The notation denotes the bit width of a number type . That is, and .
2.3.2. Vector Types
Vector types classify vectors of numeric values processed by vector instructions (also known as SIMD instructions, single instruction multiple data).
The type corresponds to a 128 bit vector of packed integer or floating-point data. The packed data can be interpreted as signed or unsigned integers, single or double precision floating-point values, or a single 128 bit type. The interpretation is determined by individual operations.
Vector types, like number types are transparent, meaning that their bit patterns can be observed. Values of vector type can be stored in memories.
2.3.2.1. Conventions
-
The notation for bit width extends to vector types as well, that is, .
2.3.3. Heap Types
Heap types classify objects in the runtime store. There are three disjoint hierarchies of heap types:
-
function types classify functions,
-
aggregate types classify dynamically allocated managed data, such as structures, arrays, or unboxed scalars,
-
external types classify external references possibly owned by the embedder.
The values from the latter two hierarchies are interconvertible by ways of the and instructions. That is, both type hierarchies are inhabited by an isomorphic set of values, but may have different, incompatible representations in practice.
A heap type is either abstract or concrete.
The abstract type denotes the common supertype of all function types, regardless of their concrete definition. Dually, the type denotes the common subtype of all function types, regardless of their concrete definition. This type has no values.
The abstract type denotes the type of all exception references. Dually, the type denotes the common subtype of all forms of exception references. This type has no values.
The abstract type denotes the common supertype of all external references received through the embedder. This type has no concrete subtypes. Dually, the type denotes the common subtype of all forms of external references. This type has no values.
The abstract type denotes the common supertype of all aggregate types, as well as possibly abstract values produced by internalizing an external reference of type . Dually, the type denotes the common subtype of all forms of aggregate types. This type has no values.
The abstract type is a subtype of that includes all types for which references can be compared, i.e., aggregate values and .
The abstract types and denote the common supertypes of all structure and array aggregates, respectively.
The abstract type denotes unboxed scalars, that is, integers injected into references. Their observable value range is limited to 31 bits.
Note
An is not actually allocated in the store, but represented in a way that allows them to be mixed with actual references into the store without ambiguity. Engines need to perform some form of pointer tagging to achieve this, which is why 1 bit is reserved.
Although the types , , , and are not inhabited by any values, they can be used to form the types of all null references in their respective hierarchy. For example, is the generic type of a null reference compatible with all function reference types.
A concrete heap type consists of a type index and classifies an object of the respective type defined in a module.
The syntax of heap types is extended with additional forms for the purpose of specifying validation and execution.
2.3.4. Reference Types
Reference types classify values that are first-class references to objects in the runtime store.
A reference type is characterised by the heap type it points to.
In addition, a reference type of the form is nullable, meaning that it can either be a proper reference to or null. Other references are non-null.
Reference types are opaque, meaning that neither their size nor their bit pattern can be observed. Values of reference type can be stored in tables.
2.3.4.1. Conventions
-
The reference type is an abbreviation for .
-
The reference type is an abbreviation for .
-
The reference type is an abbreviation for .
-
The reference type is an abbreviation for .
-
The reference type is an abbreviation for .
-
The reference type is an abbreviation for .
-
The reference type is an abbreviation for .
-
The reference type is an abbreviation for .
-
The reference type is an abbreviation for .
-
The reference type is an abbreviation for .
-
The reference type is an abbreviation for .
-
The reference type is an abbreviation for .
2.3.5. Value Types
Value types classify the individual values that WebAssembly code can compute with and the values that a variable accepts. They are either number types, vector types, or reference types.
The syntax of value types is extended with additional forms for the purpose of specifying validation.
2.3.5.1. Conventions
-
The meta variable ranges over value types or subclasses thereof where clear from context.
2.3.6. Result Types
Result types classify the result of executing instructions or functions, which is a sequence of values, written with brackets.
2.3.7. Function Types
Function types classify the signature of functions, mapping a vector of parameters to a vector of results. They are also used to classify the inputs and outputs of instructions.
2.3.8. Aggregate Types
Aggregate types describe compound objects consisting of multiple values. These are either structures or arrays, which both consist of a list of possibly mutable and possibly packed fields. Structures are heterogeneous, but require static indexing, while arrays need to be homogeneous, but allow dynamic indexing.
2.3.8.1. Conventions
-
The notation for bit width extends to packed types as well, that is, and .
-
The auxiliary function maps a storage type to the value type obtained when accessing a field:
2.3.9. Composite Types
Composite types are all types composed from simpler types, including function types and aggregate types.
2.3.10. Recursive Types
Recursive types denote a group of mutually recursive composite types, each of which can optionally declare a list of type indices of supertypes that it matches. Each type can also be declared final, preventing further subtyping.
In a module, each member of a recursive type is assigned a separate type index.
The syntax of sub types is generalized for the purpose of specifying validation and execution.
2.3.11. Address Type
Address types are a subset of number types that classify the values that can be used as offsets into memories and tables.
2.3.11.1. Conventions
The minimum of two address types is defined as the address type whose bit width is the minimum of the two.
2.3.12. Limits
Limits classify the size range of resizeable storage associated with memory types and table types.
If no maximum is given, the respective storage can grow to any size.
2.3.13. Memory Types
Memory types classify linear memories and their size range.
The limits constrain the minimum and optionally the maximum size of a memory. The limits are given in units of page size.
2.3.14. Table Types
Table types classify tables over elements of reference type within a size range.
Like memories, tables are constrained by limits for their minimum and optionally maximum size. The limits are given in numbers of entries.
2.3.15. Global Types
Global types classify global variables, which hold a value and can either be mutable or immutable.
2.3.16. Tag Types
Tag types classify the signature of tags with a function type.
Currently tags are only used for categorizing exceptions. The parameters of define the list of values associated with the exception thrown with this tag. Furthermore, it is an invariant of the semantics that every in a valid tag type for an exception has an empty result type.
Note
Future versions of WebAssembly may have additional uses for tags, and may allow non-empty result types in the function types of tags.
2.3.17. External Types
External types classify imports and external values with their respective types.
2.3.17.1. Conventions
The following auxiliary notation is defined for sequences of external types. It filters out entries of a specific kind in an order-preserving fashion:
2.4. Instructions
WebAssembly code consists of sequences of instructions. Its computational model is based on a stack machine in that instructions manipulate values on an implicit operand stack, consuming (popping) argument values and producing or returning (pushing) result values.
In addition to dynamic operands from the stack, some instructions also have static immediate arguments, typically indices or type annotations, which are part of the instruction itself.
Some instructions are structured in that they bracket nested sequences of instructions.
The following sections group instructions into a number of different categories.
2.4.1. Numeric Instructions
Numeric instructions provide basic operations over numeric values of specific type. These operations closely match respective operations available in hardware.
Numeric instructions are divided by number type. For each type, several subcategories can be distinguished:
-
Constants: return a static constant.
-
Unary Operations: consume one operand and produce one result of the respective type.
-
Binary Operations: consume two operands and produce one result of the respective type.
-
Tests: consume one operand of the respective type and produce a Boolean integer result.
-
Comparisons: consume two operands of the respective type and produce a Boolean integer result.
-
Conversions: consume a value of one type and produce a result of another (the source type of the conversion is the one after the “”).
Some integer instructions come in two flavors, where a signedness annotation distinguishes whether the operands are to be interpreted as unsigned or signed integers. For the other integer instructions, the use of two’s complement for the signed interpretation means that they behave the same regardless of signedness.
2.4.1.1. Conventions
Occasionally, it is convenient to group operators together according to the following grammar shorthands:
2.4.2. Vector Instructions
Vector instructions (also known as SIMD instructions, single instruction multiple data) provide basic operations over values of vector type.
Vector instructions have a naming convention involving a prefix that determines how their operands will be interpreted. This prefix describes the shape of the operand, written , and consisting of a packed numeric type and the number of lanes of that type. Operations are performed point-wise on the values of each lane.
Note
For example, the shape interprets the operand as four values, packed into an . The bit width of the numeric type times always is 128.
Instructions prefixed with do not involve a specific interpretation, and treat the as an value or a vector of 128 individual bits.
Vector instructions can be grouped into several subcategories:
-
Constants: return a static constant.
-
Unary Operations: consume one operand and produce one result.
-
Binary Operations: consume two operands and produce one result.
-
Ternary Operations: consume three operands and produce one result.
-
Tests: consume one operand and produce a Boolean integer result.
-
Shifts: consume a operand and a operand, producing one result.
-
Splats: consume a value of numeric type and produce a result of a specified shape.
-
Extract lanes: consume a operand and return the numeric value in a given lane.
-
Replace lanes: consume a operand and a numeric value for a given lane, and produce a result.
Some vector instructions have a signedness annotation which distinguishes whether the elements in the operands are to be interpreted as unsigned or signed integers. For the other vector instructions, the use of two’s complement for the signed interpretation means that they behave the same regardless of signedness.
2.4.2.1. Conventions
Occasionally, it is convenient to group operators together according to the following grammar shorthands:
2.4.3. Reference Instructions
Instructions in this group are concerned with accessing references.
The and instructions produce a null value or a reference to a given function, respectively.
The instruction checks for null, while converts a nullable to a non-null one, and traps if it encounters null.
The compares two references.
The instructions and test the dynamic type of a reference operand. The former merely returns the result of the test, while the latter performs a downcast and traps if the operand’s type does not match.
Note
The and instructions provides versions of the latter that branch depending on the success of the downcast instead of trapping.
2.4.4. Aggregate Instructions
Instructions in this group are concerned with creating and accessing references to aggregate types.
The instructions and allocate a new structure, initializing them either with operands or with default values. The remaining instructions on structs access individual fields, allowing for different sign extension modes in the case of packed storage types.
Similarly, arrays can be allocated either with an explicit initialization operand or a default value. Furthermore, allocates an array with statically fixed size, and and allocate an array and initialize it from a data or element segment, respectively. , , , and access individual slots, again allowing for different sign extension modes in the case of a packed storage type. produces the length of an array. fills a specified slice of an array with a given value and , , and copy elements to a specified slice of an array from a given array, data segment, or element segment, respectively.
The instructions and convert between type and an unboxed scalar.
The instructions and allow lossless conversion between references represented as type .
2.4.5. Parametric Instructions
Instructions in this group can operate on operands of any value type.
The instruction simply throws away a single operand.
The instruction selects one of its first two operands based on whether its third operand is zero or not. It may include a value type determining the type of these operands. If missing, the operands must be of numeric type.
Note
In future versions of WebAssembly, the type annotation on may allow for more than a single value being selected at the same time.
2.4.6. Variable Instructions
Variable instructions are concerned with access to local or global variables.
These instructions get or set the values of variables, respectively. The instruction is like but also returns its argument.
2.4.7. Table Instructions
Instructions in this group are concerned with tables table.
The and instructions load or store an element in a table, respectively.
The instruction returns the current size of a table. The instruction grows table by a given delta and returns the previous size, or if enough space cannot be allocated. It also takes an initialization value for the newly allocated entries.
The instruction sets all entries in a range to a given value.
The instruction copies elements from a source table region to a possibly overlapping destination region; the first index denotes the destination. The instruction copies elements from a passive element segment into a table. The instruction prevents further use of a passive element segment. This instruction is intended to be used as an optimization hint. After an element segment is dropped its elements can no longer be retrieved, so the memory used by this segment may be freed.
An additional instruction that accesses a table is the control instruction .
2.4.8. Memory Instructions
Instructions in this group are concerned with linear memory.
Memory is accessed with and instructions for the different number types and vector types. They all take a memory index and a memory immediate that contains an address offset and the expected alignment (expressed as the exponent of a power of 2).
Integer loads and stores can optionally specify a storage size that is smaller than the bit width of the respective value type. In the case of loads, a sign extension mode is then required to select appropriate behavior.
Vector loads can specify a shape that is half the bit width of . Each lane is half its usual size, and the sign extension mode then specifies how the smaller lane is extended to the larger lane. Alternatively, vector loads can perform a splat, such that only a single lane of the specified storage size is loaded, and the result is duplicated to all lanes.
The static address offset is added to the dynamic address operand, yielding a 33-bit or 65-bit effective address that is the zero-based index at which the memory is accessed. All values are read and written in little endian byte order. A trap results if any of the accessed memory bytes lies outside the address range implied by the memory’s current size.
The instruction returns the current size of a memory. The instruction grows a memory by a given delta and returns the previous size, or if enough memory cannot be allocated. Both instructions operate in units of page size. The instruction sets all values in a region of a memory to a given byte. The instruction copies data from a source memory region to a possibly overlapping destination region in another or the same memory; the first index denotes the destination. The instruction copies data from a passive data segment into a memory. The instruction prevents further use of a passive data segment. This instruction is intended to be used as an optimization hint. After a data segment is dropped its data can no longer be retrieved, so the memory used by this segment may be freed.
2.4.9. Control Instructions
Instructions in this group affect the flow of control.
The instruction does nothing.
The instruction causes an unconditional trap.
The , , , and instructions are structured instructions. They bracket nested sequences of instructions, called blocks, separated by the pseudo-instruction, and terminated with an pseudo-instruction. As the grammar prescribes, they must be well-nested.
The instructions , , and are concerned with exceptions. The instruction installs an exception handler that handles exceptions as specified by its catch clauses.. The and instructions raise and reraise an exception, respectively, and transfers control to the innermost enclosing exception handler that has a matching catch clause.
A structured instruction can consume input and produce output on the operand stack according to its annotated block type. It is given either as a type index that refers to a suitable function type reinterpreted as an instruction type, or as an optional value type inline, which is a shorthand for the instruction type .
Each structured control instruction introduces an implicit label. Labels are targets for branch instructions that reference them with label indices. Unlike with other index spaces, indexing of labels is relative by nesting depth, that is, label refers to the innermost structured control instruction enclosing the referring branch instruction, while increasing indices refer to those farther out. Consequently, labels can only be referenced from within the associated structured control instruction. This also implies that branches can only be directed outwards, “breaking” from the block of the control construct they target. The exact effect depends on that control construct. In case of or it is a forward jump, resuming execution after the matching . In case of it is a backward jump to the beginning of the loop.
Note
This enforces structured control flow. Intuitively, a branch targeting a or behaves like a statement in most C-like languages, while a branch targeting a behaves like a statement.
Branch instructions come in several flavors: performs an unconditional branch, performs a conditional branch, and performs an indirect branch through an operand indexing into the label vector that is an immediate to the instruction, or to a default target if the operand is out of bounds. The and instructions check whether a reference operand is null and branch if that is the case or not the case, respectively. Similarly, and attempt a downcast on a reference operand and branch if that succeeds, or fails, respectively.
The instruction is a shortcut for an unconditional branch to the outermost block, which implicitly is the body of the current function. Taking a branch unwinds the operand stack up to the height where the targeted structured control instruction was entered. However, branches may additionally consume operands themselves, which they push back on the operand stack after unwinding. Forward branches require operands according to the output of the targeted block’s type, i.e., represent the values produced by the terminated block. Backward branches require operands according to the input of the targeted block’s type, i.e., represent the values consumed by the restarted block.
The instruction invokes another function, consuming the necessary arguments from the stack and returning the result values of the call. The instruction invokes a function indirectly through a function reference operand. The instruction calls a function indirectly through an operand indexing into a table that is denoted by a table index and must contain function references. Since it may contain functions of heterogeneous type, the callee is dynamically checked against the function type indexed by the instruction’s second immediate, and the call is aborted with a trap if it does not match.
The , , and instructions are tail-call variants of the previous ones. That is, they first return from the current function before actually performing the respective call. It is guaranteed that no sequence of nested calls using only these instructions can cause resource exhaustion due to hitting an implementation’s limit on the number of active calls.
2.4.10. Expressions
Function bodies, initialization values for globals, elements and offsets of element segments, and offsets of data segments are given as expressions, which are sequences of instructions terminated by an marker.
In some places, validation restricts expressions to be constant, which limits the set of allowable instructions.
2.5. Modules
WebAssembly programs are organized into modules, which are the unit of deployment, loading, and compilation. A module collects definitions for types, functions, tables, memories, tags, and globals. In addition, it can declare imports and exports and provide initialization in the form of data and element segments, or a start function.
Each of the vectors – and thus the entire module – may be empty.
2.5.1. Indices
Definitions are referenced with zero-based indices. Each class of definition has its own index space, as distinguished by the following classes.
The index space for functions, tables, memories, globals, and tags includes respective imports declared in the same module. The indices of these imports precede the indices of other definitions in the same index space.
Element indices reference element segments and data indices reference data segments.
The index space for locals is only accessible inside a function and includes the parameters of that function, which precede the local variables.
Label indices reference structured control instructions inside an instruction sequence.
Each aggregate type provides an index space for its fields.
2.5.1.1. Conventions
-
The meta variable ranges over label indices.
-
The meta variables range over indices in any of the other index spaces.
-
The notation denotes the set of indices from index space occurring free in . Sometimes this set is reinterpreted as the vector of its elements.
Note
For example, if is , then , or equivalently, the vector .
2.5.2. Types
The component of a module defines a vector of recursive types, each of consisting of a list of sub types referenced by individual type indices. All function or aggregate types used in a module must be defined in this component.
2.5.3. Functions
The component of a module defines a vector of functions with the following structure:
The of a function declares its signature by reference to a type defined in the module. The parameters of the function are referenced through 0-based local indices in the function’s body; they are mutable.
The declare a vector of mutable local variables and their types. These variables are referenced through local indices in the function’s body. The index of the first local is the smallest index not referencing a parameter.
The is an instruction sequence that upon termination must produce a stack matching the function type’s result type.
Functions are referenced through function indices, starting with the smallest index not referencing a function import.
2.5.4. Tables
The component of a module defines a vector of tables described by their table type:
A table is an array of opaque values of a particular reference type. Moreover, each table slot is initialized with the value given by a constant initializer expression. Tables can further be initialized through element segments.
The size in the limits of the table type specifies the initial size of that table, while its , if present, restricts the size to which it can grow later.
Tables are referenced through table indices, starting with the smallest index not referencing a table import. Most constructs implicitly reference table index .
2.5.5. Memories
The component of a module defines a vector of linear memories (or memories for short) as described by their memory type:
A memory is a vector of raw uninterpreted bytes. The size in the limits of the memory type specifies the initial size of that memory, while its , if present, restricts the size to which it can grow later. Both are in units of page size.
Memories can be initialized through data segments.
Memories are referenced through memory indices, starting with the smallest index not referencing a memory import. Most constructs implicitly reference memory index .
2.5.6. Globals
The component of a module defines a vector of global variables (or globals for short):
Each global stores a single value of the given global type. Its also specifies whether a global is immutable or mutable. Moreover, each global is initialized with an value given by a constant initializer expression.
Globals are referenced through global indices, starting with the smallest index not referencing a global import.
2.5.8. Element Segments
The initial contents of a table is uninitialized. Element segments can be used to initialize a subrange of a table from a static vector of elements.
The component of a module defines a vector of element segments. Each element segment defines a reference type and a corresponding list of constant element expressions.
Element segments have a mode that identifies them as either passive, active, or declarative. A passive element segment’s elements can be copied to a table using the instruction. An active element segment copies its elements into a table during instantiation, as specified by a table index and a constant expression defining an offset into that table. A declarative element segment is not available at runtime but merely serves to forward-declare references that are formed in code with instructions like .
The is given by a constant expression.
Element segments are referenced through element indices.
2.5.9. Data Segments
The initial contents of a memory are zero bytes. Data segments can be used to initialize a range of memory from a static vector of bytes.
The component of a module defines a vector of data segments.
Like element segments, data segments have a mode that identifies them as either passive or active. A passive data segment’s contents can be copied into a memory using the instruction. An active data segment copies its contents into a memory during instantiation, as specified by a memory index and a constant expression defining an offset into that memory.
Data segments are referenced through data indices.
Note
In the current version of WebAssembly, at most one memory is allowed in a module. Consequently, the only valid is .
2.5.10. Start Function
The component of a module declares the function index of a start function that is automatically invoked when the module is instantiated, after tables and memories have been initialized.
Note
The start function is intended for initializing the state of a module. The module and its exports are not accessible externally before this initialization has completed.
2.5.11. Exports
The component of a module defines a set of exports that become accessible to the host environment once the module has been instantiated.
Each export is labeled by a unique name. Exportable definitions are functions, tables, memories, globals, and tags, which are referenced through a respective descriptor.
2.5.11.1. Conventions
The following auxiliary notation is defined for sequences of exports, filtering out indices of a specific kind in an order-preserving fashion:
2.5.12. Imports
The component of a module defines a set of imports that are required for instantiation.
Each import is labeled by a two-level name space, consisting of a name and a for an entity within that module. Importable definitions are functions, tables, memories, globals, and tags. Each import is specified by a descriptor with a respective type that a definition provided during instantiation is required to match.
Every import defines an index in the respective index space. In each index space, the indices of imports go before the first index of any definition contained in the module itself.
Note
Unlike export names, import names are not necessarily unique. It is possible to import the same / pair multiple times; such imports may even have different type descriptions, including different kinds of entities. A module with such imports can still be instantiated depending on the specifics of how an embedder allows resolving and supplying imports. However, embedders are not required to support such overloading, and a WebAssembly module itself cannot implement an overloaded name.
3. Validation
3.1. Conventions
Validation checks that a WebAssembly module is well-formed. Only valid modules can be instantiated.
Validity is defined by a type system over the abstract syntax of a module and its contents. For each piece of abstract syntax, there is a typing rule that specifies the constraints that apply to it. All rules are given in two equivalent forms:
-
In prose, describing the meaning in intuitive form.
-
In formal notation, describing the rule in mathematical form. [1]
Note
The prose and formal rules are equivalent, so that understanding of the formal notation is not required to read this specification. The formalism offers a more concise description in notation that is used widely in programming languages semantics and is readily amenable to mathematical proof.
In both cases, the rules are formulated in a declarative manner. That is, they only formulate the constraints, they do not define an algorithm. The skeleton of a sound and complete algorithm for type-checking instruction sequences according to this specification is provided in the appendix.
3.1.1. Types
To define the semantics, the definition of some sorts of types is extended to include additional forms. By virtue of not being representable in either the binary format or the text format, these forms cannot be used in a program; they only occur during validation or execution.
The unique value type is a bottom type that matches all value types. Similarly, is also used as a bottom type of all heap types.
Note
No validation rule uses bottom types explicitly, but various rules can pick any value or heap type, including bottom. This ensures the existence of principal types, and thus a validation algorithm without back tracking.
A concrete heap type can consist of a defined type directly. this occurs as the result of substituting a type index with its definition.
A concrete heap type may also be a recursive type index. Such an index refers to the -th component of a surrounding recursive type. It occurs as the result of rolling up the definition of a recursive type.
Finally, the representation of supertypes in a sub type is generalized from mere type indices to heap types. They occur as defined types or recursive type indices after substituting type indices or rolling up recursive types.
Note
It is an invariant of the semantics that sub types occur only in one of two forms: either as “syntactic” types as in a source module, where all supertypes are type indices, or as “semantic” types, where all supertypes are resolved to either defined types or recursive type indices.
A type of any form is closed when it does not contain a heap type that is a type index or a recursive type index without a surrounding recursive type, i.e., all type indices have been substituted with their defined type and all free recursive type indices have been unrolled.
Note
Recursive type indices are internal to a recursive type. They are distinguished from regular type indices and represented such that two closed types are syntactically equal if and only if they have the same recursive structure.
3.1.1.1. Convention
-
The difference between two reference types is defined as follows:
Note
This definition computes an approximation of the reference type that is inhabited by all values from except those from . Since the type system does not have general union types, the defnition only affects the presence of null and cannot express the absence of other values.
3.1.2. Defined Types
Defined types denote the individual types defined in a module. Each such type is represented as a projection from the recursive type group it originates from, indexed by its position in that group.
Defined types do not occur in the binary or text format, but are formed by rolling up the recursive types defined in a module.
It is hence an invariant of the semantics that all recursive types occurring in defined types are rolled up.
3.1.2.1. Conventions
-
denotes the parallel substitution of type indices with defined types in type , provided .
-
denotes the parallel substitution of recursive type indices with defined types in type , provided .
-
is shorthand for the substitution , where .
3.1.3. Rolling and Unrolling
In order to allow comparing recursive types for equivalence, their representation is changed such that all type indices internal to the same recursive type are replaced by recursive type indices.
Note
This representation is independent of the type index space, so that it is meaningful across module boundaries. Moreover, this representation ensures that types with equivalent recursive structure are also syntactically equal, hence allowing a simple equality check on (closed) types. It gives rise to an iso-recursive interpretation of types.
The representation change is performed by two auxiliary operations on the syntax of recursive types:
-
Rolling up a recursive type substitutes its internal type indices with corresponding recursive type indices.
-
Unrolling a recursive type substitutes its recursive type indices with the corresponding defined types.
These operations are extended to defined types and defined as follows:
In addition, the following auxiliary function denotes the expansion of a defined type:
3.1.4. Instruction Types
Instruction types classify the behaviour of instructions or instruction sequences, by describing how they manipulate the operand stack and the initialization status of locals:
An instruction type describes the required input stack with argument values of types that an instruction pops off and the provided output stack with result values of types that it pushes back. Moreover, it enumerates the indices of locals that have been set by the instruction or sequence.
Note
Instruction types are only used for validation, they do not occur in programs.
3.1.5. Local Types
Local types classify locals, by describing their value type as well as their initialization status:
Note
Local types are only used for validation, they do not occur in programs.
3.1.6. Contexts
Validity of an individual definition is specified relative to a context, which collects relevant information about the surrounding module and the definitions in scope:
-
Types: the list of types defined in the current module.
-
Functions: the list of functions declared in the current module, represented by a defined type that expands to their function type.
-
Tables: the list of tables declared in the current module, represented by their table type.
-
Memories: the list of memories declared in the current module, represented by their memory type.
-
Globals: the list of globals declared in the current module, represented by their global type.
-
Tags: the list of tags declared in the current module, represented by their tag type.
-
Element Segments: the list of element segments declared in the current module, represented by the elements’ reference type.
-
Data Segments: the list of data segments declared in the current module, each represented by an entry.
-
Locals: the list of locals declared in the current function (including parameters), represented by their local type.
-
Labels: the stack of labels accessible from the current position, represented by their result type.
-
Return: the return type of the current function, represented as an optional result type that is absent when no return is allowed, as in free-standing expressions.
-
References: the list of function indices that occur in the module outside functions and can hence be used to form references inside them.
In other words, a context contains a sequence of suitable types for each index space, describing each defined entry in that space. Locals, labels and return type are only used for validating instructions in function bodies, and are left empty elsewhere. The label stack is the only part of the context that changes as validation of an instruction sequence proceeds.
More concretely, contexts are defined as records with abstract syntax:
In addition to field access written the following notation is adopted for manipulating contexts:
-
When spelling out a context, empty fields are omitted.
-
denotes the same context as but with the elements prepended to its component sequence.
Note
Indexing notation like is used to look up indices in their respective index space in the context. Context extension notation is primarily used to locally extend relative index spaces, such as label indices. Accordingly, the notation is defined to append at the front of the respective sequence, introducing a new relative index and shifting the existing ones.
3.1.6.1. Convention
Any form of type can be closed to bring it into closed form relative to a context it is valid in by substituting each type index occurring in it with the corresponding defined type , after first closing the types in themselves.
3.1.7. Prose Notation
Validation is specified by stylised rules for each relevant part of the abstract syntax. The rules not only state constraints defining when a phrase is valid, they also classify it with a type. The following conventions are adopted in stating these rules.
-
A phrase is said to be “valid with type ” if and only if all constraints expressed by the respective rules are met. The form of depends on what is.
Note
For example, if is a function, then is a function type; for an that is a global, is a global type; and so on.
-
The rules implicitly assume a given context .
-
In some places, this context is locally extended to a context with additional entries. The formulation “Under context , … statement …” is adopted to express that the following statement must apply under the assumptions embodied in the extended context.
3.1.8. Formal Notation
Note
This section gives a brief explanation of the notation for specifying typing rules formally. For the interested reader, a more thorough introduction can be found in respective text books. [2]
The proposition that a phrase has a respective type is written . In general, however, typing is dependent on a context . To express this explicitly, the complete form is a judgement , which says that holds under the assumptions encoded in .
The formal typing rules use a standard approach for specifying type systems, rendering them into deduction rules. Every rule has the following general form:
Such a rule is read as a big implication: if all premises hold, then the conclusion holds. Some rules have no premises; they are axioms whose conclusion holds unconditionally. The conclusion always is a judgment , and there is one respective rule for each relevant construct of the abstract syntax.
Note
For example, the typing rule for the instruction can be given as an axiom:
The instruction is always valid with type (saying that it consumes two values and produces one), independent of any side conditions.
An instruction like can be typed as follows:
Here, the premise enforces that the immediate global index exists in the context. The instruction produces a value of its respective type (and does not consume any values). If does not exist then the premise does not hold, and the instruction is ill-typed.
Finally, a structured instruction requires a recursive rule, where the premise is itself a typing judgement:
A instruction is only valid when the instruction sequence in its body is. Moreover, the result type must match the block’s annotation . If so, then the instruction has the same type as the body. Inside the body an additional label of the corresponding result type is available, which is expressed by extending the context with the additional label information for the premise.
The semantics is derived from the following article: Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. Bringing the Web up to Speed with WebAssembly. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017.
For example: Benjamin Pierce. Types and Programming Languages. The MIT Press 2002
3.2. Types
Simple types, such as number types are universally valid. However, restrictions apply to most other types, such as reference types, function types, as well as the limits of table types and memory types, which must be checked during validation.
Moreover, block types are converted to plain function types for ease of processing.
3.2.1. Number Types
Number types are always valid.
3.2.2. Vector Types
Vector types are always valid.
3.2.3. Heap Types
Concrete heap types are only valid when the type index is, while abstract ones are vacuously valid.
3.2.3.1.
-
The heap type is valid.
3.2.3.2.
-
The type must be defined in the context.
-
Then the heap type is valid.
3.2.4. Reference Types
Reference types are valid when the referenced heap type is.
3.2.4.1.
-
The heap type must be valid.
-
Then the reference type is valid.
3.2.5. Value Types
Valid value types are either valid number types, valid vector types, or valid reference types.
3.2.6. Block Types
Block types may be expressed in one of two forms, both of which are converted to instruction types by the following rules.
3.2.6.1.
-
The type must be defined in the context.
-
The expansion of must be a function type .
-
Then the block type is valid as instruction type .
3.2.6.2.
-
The value type must either be absent, or valid.
-
Then the block type is valid as instruction type .
3.2.7. Result Types
3.2.7.1.
-
Each value type in the type sequence must be valid.
-
Then the result type is valid.
3.2.8. Instruction Types
3.2.8.1.
-
The result type must be valid.
-
The result type must be valid.
-
Each local index in must be defined in the context.
-
Then the instruction type is valid.
3.2.9. Function Types
3.2.9.1.
-
The result type must be valid.
-
The result type must be valid.
-
Then the function type is valid.
3.2.10. Composite Types
3.2.10.1.
-
The function type must be valid.
-
Then the composite type is valid.
3.2.10.2.
-
For each field type in :
-
The field type must be valid.
-
-
Then the composite type is valid.
3.2.10.3.
-
The field type must be valid.
-
Then the composite type is valid.
3.2.11. Field Types
3.2.11.1.
-
The storage type must be valid.
-
Then the field type is valid.
3.2.11.2.
-
The packed type is valid.
3.2.12. Recursive Types
Recursive types are validated for a specific type index that denotes the index of the type defined by the recursive group.
3.2.12.1.
-
Either the sequence is empty.
-
Or:
-
The first sub type of the sequence must be valid for the type index .
-
The remaining sequence must be valid for the type index .
-
-
Then the recursive type is valid for the type index .
3.2.12.2.
-
The composite type must be valid.
-
The sequence may be no longer than .
-
For every type index in :
-
The type index must be smaller than .
-
The type index must exist in the context .
-
Let be the unrolling of the defined type .
-
The sub type must not contain .
-
Let be the composite type in .
-
The composite type must match .
-
-
Then the sub type is valid for the type index .
Note
The side condition on the index ensures that a declared supertype is a previously defined types, preventing cyclic subtype hierarchies.
Future versions of WebAssembly may allow more than one supertype.
3.2.13. Defined Types
3.2.13.1.
-
The recursive type must be valid for some type index .
-
Let be the defined type .
-
The number must be smaller than the length of the sequence of sub types.
-
Then the defined type is valid.
3.2.14. Limits
Limits must have meaningful bounds that are within a given range.
3.2.14.1.
-
The value of must not be larger than .
-
If the maximum is not empty, then:
-
Its value must not be larger than .
-
Its value must not be smaller than .
-
-
Then the limit is valid within range .
3.2.15. Table Types
3.2.15.1.
-
The limits must be valid within range .
-
The reference type must be valid.
-
Then the table type is valid.
3.2.16. Memory Types
3.2.16.1.
-
The limits must be valid within range .
-
Then the memory type is valid.
3.2.17. Tag Types
3.2.17.1.
-
The function type must be valid.
-
The type sequence must be empty.
-
Then the tag type is valid.
3.2.18. Global Types
3.2.18.1.
-
The value type must be valid.
-
Then the global type is valid.
3.2.19. External Types
3.2.19.1.
-
The defined type must be valid.
-
The defined type must be a function type.
-
Then the external type is valid.
3.2.19.2.
-
The table type must be valid.
-
Then the external type is valid.
3.2.19.3.
-
The memory type must be valid.
-
Then the external type is valid.
3.2.19.4.
3.2.19.5.
-
The global type must be valid.
-
Then the external type is valid.
3.2.20. Defaultable Types
A type is defaultable if it has a default value for initialization.
3.2.20.1. Value Types
-
A defaultable value type must be:
-
either a number type,
-
or a vector type,
-
or a nullable reference type.
-
3.3. Matching
On most types, a notion of subtyping is defined that is applicable in validation rules, during module instantiation when checking the types of imports, or during execution, when performing casts.
3.3.1. Number Types
A number type matches a number type if and only if:
-
Both and are the same.
3.3.2. Vector Types
A vector type matches a vector type if and only if:
-
Both and are the same.
3.3.3. Heap Types
A heap type matches a heap type if and only if:
-
Either both and are the same.
-
Or there exists a valid heap type , such that matches and matches .
-
Or is and is .
-
Or is one of , , or and is .
-
Or is a defined type which expands to a structure type and is .
-
Or is a defined type which expands to an array type and is .
-
Or is a defined type which expands to a function type and is .
-
Or is a defined type and is a defined type , and matches .
-
Or is a type index , and the defined type matches .
-
Or is a type index , and matches the defined type .
-
Or is and matches .
-
Or is and matches .
-
Or is and matches .
-
Or is .
3.3.4. Reference Types
A reference type matches a reference type if and only if:
3.3.5. Value Types
A value type matches a value type if and only if:
-
Either both and are number types and matches .
-
Or both and are reference types and matches .
-
Or is .
3.3.6. Result Types
Subtyping is lifted to result types in a pointwise manner. That is, a result type matches a result type if and only if:
-
Every value type in matches the corresponding value type in .
3.3.7. Instruction Types
Subtyping is further lifted to instruction types. An instruction type matches a type if and only if:
-
There is a common sequence of value types such that equals and equals .
-
The result type matches .
-
The result type matches .
-
For every local index that is in but not in , the local type is for some value type .
Note
Instruction types are contravariant in their input and covariant in their output. Subtyping also incorporates a sort of “frame” condition, which allows adding arbitrary invariant stack elements on both sides in the super type.
Finally, the supertype may ignore variables from the init set . It may also add variables to the init set, provided these are already set in the context, i.e., are vacuously initialized.
3.3.8. Function Types
A function type matches a type if and only if:
-
The result type matches .
-
The result type matches .
3.3.9. Composite Types
A composite type matches a type if and only if:
-
Either the composite type is and is and:
-
The function type matches .
-
-
Or the composite type is and is and:
-
The arity is greater than or equal to .
-
For every field type in and corresponding in
-
The field type matches .
-
-
-
Or the composite type is and is and:
-
The field type matches .
-
3.3.10. Field Types
A field type matches a type if and only if:
-
Either both and are .
-
Or both and are and matches as well.
A storage type matches a type if and only if:
-
Either is a value type and is a value type and matches .
-
Or is a packed type and is a packed type and matches .
A packed type matches a type if and only if:
-
The packed type is the same as .
3.3.11. Defined Types
A defined type matches a type if and only if:
-
Either and are equal when closed under context .
-
Or:
Note
Note that there is no explicit definition of type _equivalence_, since it coincides with syntactic equality, as used in the premise of the former rule above.
3.3.12. Limits
Limits match limits if and only if:
-
is larger than or equal to .
-
Either:
-
is empty.
-
-
Or:
-
Both and are non-empty.
-
is smaller than or equal to .
-
3.3.13. Table Types
A table type matches if and only if:
-
Address types and are the same.
-
Limits match .
-
The reference type matches , and vice versa.
3.3.14. Memory Types
A memory type matches if and only if:
-
Address types and are the same.
-
Limits match .
3.3.15. Global Types
A global type matches if and only if:
3.3.16. Tag Types
A tag type matches if and only if they are the same.
3.3.17. External Types
3.3.17.1. Functions
An external type matches if and only if:
-
The defined type matches .
3.3.17.2. Tables
An external type matches if and only if:
-
Table type matches .
3.3.17.3. Memories
An external type matches if and only if:
-
Memory type matches .
3.3.17.4. Globals
An external type matches if and only if:
-
Global type matches .
3.4. Instructions
Instructions are classified by instruction types that describe how they manipulate the operand stack and initialize locals: A type describes the required input stack with argument values of types that an instruction pops off and the provided output stack with result values of types that it pushes back. Moreover, it enumerates the indices of locals that have been set by the instruction. In most cases, this is empty.
Note
For example, the instruction has type , consuming two values and producing one. The instruction has type , provided is the type declared for the local .
Typing extends to instruction sequences . Such a sequence has an instruction type if the accumulative effect of executing the instructions is consuming values of types off the operand stack, pushing new values of types , and setting all locals .
For some instructions, the typing rules do not fully constrain the type, and therefore allow for multiple types. Such instructions are called polymorphic. Two degrees of polymorphism can be distinguished:
-
value-polymorphic: the value type of one or several individual operands is unconstrained. That is the case for all parametric instructions like and .
-
stack-polymorphic: the entire (or most of the) instruction type of the instruction is unconstrained. That is the case for all control instructions that perform an unconditional control transfer, such as , , , and .
In both cases, the unconstrained types or type sequences can be chosen arbitrarily, as long as they meet the constraints imposed for the surrounding parts of the program.
Note
For example, the instruction is valid with type , for any possible number type . Consequently, both instruction sequences
and
are valid, with in the typing of being instantiated to or , respectively.
The instruction is stack-polymorphic, and hence valid with type for any possible sequences of value types and . Consequently,
is valid by assuming type for the instruction. In contrast,
is invalid, because there is no possible type to pick for the instruction that would make the sequence well-typed.
The Appendix describes a type checking algorithm that efficiently implements validation of instruction sequences as prescribed by the rules given here.
3.4.1. Numeric Instructions
3.4.1.1.
-
The instruction is valid with type .
3.4.1.2.
-
The instruction is valid with type .
3.4.1.3.
-
The instruction is valid with type .
3.4.1.4.
-
The instruction is valid with type .
3.4.1.5.
-
The instruction is valid with type .
3.4.1.6.
-
The instruction is valid with type .
3.4.2. Reference Instructions
3.4.2.1.
3.4.2.2.
-
The function must be defined in the context.
-
Let be the defined type .
-
The function index must be contained in .
-
The instruction is valid with type .
3.4.2.3.
3.4.2.4.
3.4.2.5.
-
The instruction is valid with type .
3.4.2.6.
-
The reference type must be valid.
-
Then the instruction is valid with type for any valid reference type for which matches .
Note
The liberty to pick a supertype allows typing the instruction with the least precise super type of as input, that is, the top type in the corresponding heap subtyping hierarchy.
3.4.2.7.
-
The reference type must be valid.
-
Then the instruction is valid with type for any valid reference type for which matches .
Note
The liberty to pick a supertype allows typing the instruction with the least precise super type of as input, that is, the top type in the corresponding heap subtyping hierarchy.
3.4.3. Aggregate Reference Instructions
3.4.3.1.
-
The defined type must exist.
-
The expansion of must be a structure type .
-
For each field type in :
-
Let be .
-
Let be the value type .
-
-
Let be the concatenation of all .
-
Then the instruction is valid with type .
3.4.3.2.
-
The defined type must exist.
-
The expansion of must be a structure type .
-
For each field type in :
-
Let be .
-
Let be the value type .
-
The type must be defaultable.
-
-
Let be the concatenation of all .
-
Then the instruction is valid with type .
3.4.3.3.
-
The defined type must exist.
-
The expansion of must be a structure type .
-
Let the field type be .
-
Let be the value type .
-
The extension must be present if and only if is a packed type.
-
Then the instruction is valid with type .
3.4.3.4.
-
The defined type must exist.
-
The expansion of must be a structure type .
-
Let the field type be .
-
The prefix must be .
-
Let be the value type .
-
Then the instruction is valid with type .
3.4.3.5.
-
The defined type must exist.
-
The expansion of must be an array type .
-
Let be .
-
Let be the value type .
-
Then the instruction is valid with type .
3.4.3.6.
-
The defined type must exist.
-
The expansion of must be an array type .
-
Let be .
-
Let be the value type .
-
The type must be defaultable.
-
Then the instruction is valid with type .
3.4.3.7.
-
The defined type must exist.
-
The expansion of must be an array type .
-
Let be .
-
Let be the value type .
-
Then the instruction is valid with type .
3.4.3.8.
-
The defined type must exist.
-
The expansion of must be an array type .
-
Let be .
-
The storage type must be a reference type .
-
The element segment must exist.
-
Let be the reference type .
-
The reference type must match .
-
Then the instruction is valid with type .
3.4.3.9.
-
The defined type must exist.
-
The expansion of must be an array type .
-
Let be .
-
Let be the value type .
-
The type must be a numeric type or a vector type.
-
The data segment must exist.
-
Then the instruction is valid with type .
3.4.3.10.
-
The defined type must exist.
-
The expansion of must be an array type .
-
Let the field type be .
-
Let be the value type .
-
The extension must be present if and only if is a packed type.
-
Then the instruction is valid with type .
3.4.3.11.
-
The defined type must exist.
-
The expansion of must be an array type .
-
Let the field type be .
-
The prefix must be .
-
Let be the value type .
-
Then the instruction is valid with type .
3.4.3.12.
-
The the instruction is valid with type .
3.4.3.13.
-
The defined type must exist.
-
The expansion of must be an array type .
-
Let the field type be .
-
The prefix must be .
-
Let be the value type .
-
Then the instruction is valid with type .
3.4.3.14.
-
The defined type must exist.
-
The expansion of must be an array type .
-
Let the field type be .
-
The prefix must be .
-
The defined type must exist.
-
The expansion of must be an array type .
-
Let the field type be .
-
The storage type must match .
-
Then the instruction is valid with type .
3.4.3.15.
-
The defined type must exist.
-
The expansion of must be an array type .
-
Let the field type be .
-
The prefix must be .
-
Let be the value type .
-
The value type must be a numeric type or a vector type.
-
The data segment must exist.
-
Then the instruction is valid with type .
3.4.3.16.
-
The defined type must exist.
-
The expansion of must be an array type .
-
Let the field type be .
-
The prefix must be .
-
The storage type must be a reference type .
-
The element segment must exist.
-
Let be the reference type .
-
The reference type must match .
-
Then the instruction is valid with type .
3.4.4. Scalar Reference Instructions
3.4.4.1.
-
The instruction is valid with type .
3.4.4.2.
-
The instruction is valid with type .
3.4.5. External Reference Instructions
3.4.5.1.
-
The instruction is valid with type for any that equals .
3.4.5.2.
-
The instruction is valid with type for any that equals .
3.4.6. Vector Instructions
Vector instructions can have a prefix to describe the shape of the operand. Packed numeric types, and , are not value types. An auxiliary function maps such packed type shapes to value types:
The following auxiliary function denotes the number of lanes in a vector shape, i.e., its dimension:
3.4.6.1.
-
The instruction is valid with type .
3.4.6.2.
-
The instruction is valid with type .
3.4.6.3.
-
The instruction is valid with type .
3.4.6.4.
-
The instruction is valid with type .
3.4.6.5.
-
The instruction is valid with type .
3.4.6.6.
-
The instruction is valid with type .
3.4.6.7.
-
The instruction is valid with type .
3.4.6.8.
-
For all , in , must be smaller than .
-
The instruction is valid with type .
3.4.6.9.
-
Let be .
-
The instruction is valid with type .
3.4.6.10.
-
The lane index must be smaller than .
-
The instruction is valid with type .
3.4.6.11.
-
The lane index must be smaller than .
-
Let be .
-
The instruction is valid with type .
3.4.6.12.
-
The instruction is valid with type .
3.4.6.13.
-
The instruction is valid with type .
3.4.6.14.
-
The instruction is valid with type .
3.4.6.15.
-
The instruction is valid with type .
3.4.6.16.
-
The instruction is valid with type .
3.4.6.17.
-
The instruction is valid with type .
3.4.6.18.
-
The instruction is valid with type .
3.4.6.19.
-
The instruction is valid with type .
3.4.6.20.
-
The instruction is valid with type .
3.4.6.21.
-
The instruction is valid with type .
3.4.6.22.
-
The instruction is valid with type .
3.4.6.23.
-
The instruction is valid with type .
3.4.6.24.
-
The instruction is valid with type .
3.4.6.25.
-
The instruction is valid with type .
3.4.6.26.
-
The instruction is valid with type .
3.4.7. Parametric Instructions
3.4.7.1.
-
The instruction is valid with type , for any valid value type .
Note
Both and without annotation are value-polymorphic instructions.
3.4.7.2.
-
If is present, then:
-
The result type must be valid.
-
The length of must be .
-
Then the instruction is valid with type .
-
-
Else:
-
The instruction is valid with type , for any valid value type that matches some number type or vector type.
-
Note
In future versions of WebAssembly, may allow more than one value per choice.
3.4.8. Variable Instructions
3.4.8.1.
-
The local must be defined in the context.
-
Let be the local type .
-
The initialization status must be .
-
Then the instruction is valid with type .
3.4.8.2.
-
The local must be defined in the context.
-
Let be the local type .
-
Then the instruction is valid with type .
3.4.8.3.
-
The local must be defined in the context.
-
Let be the local type .
-
Then the instruction is valid with type .
3.4.8.4.
-
The global must be defined in the context.
-
Let be the global type .
-
Then the instruction is valid with type .
3.4.8.5.
-
The global must be defined in the context.
-
Let be the global type .
-
The mutability must be .
-
Then the instruction is valid with type .
3.4.9. Table Instructions
3.4.9.1.
-
The table must be defined in the context.
-
Let be the table type .
-
Then the instruction is valid with type .
3.4.9.2.
-
The table must be defined in the context.
-
Let be the table type .
-
Then the instruction is valid with type .
3.4.9.3.
-
The table must be defined in the context.
-
Let be the table type .
-
Then the instruction is valid with type .
3.4.9.4.
-
The table must be defined in the context.
-
Let be the table type .
-
Then the instruction is valid with type .
3.4.9.5.
-
The table must be defined in the context.
-
Let be the table type .
-
Then the instruction is valid with type .
3.4.9.6.
-
The table must be defined in the context.
-
Let be the table type .
-
The table must be defined in the context.
-
Let be the table type .
-
The reference type must match .
-
Let be the minimum of and
-
Then the instruction is valid with type .
3.4.9.7.
-
The table must be defined in the context.
-
Let be the table type .
-
The element segment must be defined in the context.
-
Let be the reference type .
-
The reference type must match .
-
Then the instruction is valid with type .
3.4.9.8.
-
The element segment must be defined in the context.
-
Then the instruction is valid with type .
3.4.10. Memory Instructions
3.4.10.1.
-
The memory must be defined in the context.
-
Let be the memory type .
-
The offset must be less than .
-
The alignment must not be larger than the bit width of divided by .
-
Then the instruction is valid with type .
3.4.10.2.
-
The memory must be defined in the context.
-
Let be the memory type .
-
The offset must be less than .
-
The alignment must not be larger than .
-
Then the instruction is valid with type .
3.4.10.3.
-
The memory must be defined in the context.
-
Let be the memory type .
-
The offset must be less than .
-
The alignment must not be larger than the bit width of divided by .
-
Then the instruction is valid with type .
3.4.10.4.
-
The memory must be defined in the context.
-
Let be the memory type .
-
The offset must be less than .
-
The alignment must not be larger than .
-
Then the instruction is valid with type .
3.4.10.5.
-
The memory must be defined in the context.
-
Let be the memory type .
-
The offset must be less than .
-
The alignment must not be larger than .
-
Then the instruction is valid with type .
3.4.10.6.
-
The memory must be defined in the context.
-
Let be the memory type .
-
The offset must be less than .
-
The alignment must not be larger than .
-
Then the instruction is valid with type .
3.4.10.7.
-
The memory must be defined in the context.
-
Let be the memory type .
-
The offset must be less than .
-
The alignment must not be larger than .
-
Then the instruction is valid with type .
3.4.10.8.
-
The memory must be defined in the context.
-
Let be the memory type .
-
The offset must be less than .
-
The alignment must not be larger than .
-
The lane index must be smaller than .
-
Then the instruction is valid with type .
3.4.10.9.
-
The memory must be defined in the context.
-
Let be the memory type .
-
The offset must be less than .
-
The alignment must not be larger than .
-
The lane index must be smaller than .
-
Then the instruction is valid with type .
3.4.10.10.
-
The memory must be defined in the context.
-
Let be the memory type .
-
Then the instruction is valid with type .
3.4.10.11.
-
The memory must be defined in the context.
-
Let be the memory type .
-
Then the instruction is valid with type .
3.4.10.12.
-
The memory must be defined in the context.
-
Let be the memory type .
-
Then the instruction is valid with type .
3.4.10.13.
-
The memory must be defined in the context.
-
The memory must be defined in the context.
-
Let be the memory type .
-
Let be the memory type .
-
Let be the minimum of and
-
Then the instruction is valid with type .
3.4.10.14.
-
The memory must be defined in the context.
-
Let be the memory type .
-
The data segment must be defined in the context.
-
Then the instruction is valid with type .
3.4.10.15.
-
The data segment must be defined in the context.
-
Then the instruction is valid with type .
3.4.11. Control Instructions
3.4.11.1.
-
The instruction is valid with type .
3.4.11.2.
-
The instruction is valid with any valid type of the form .
Note
The instruction is stack-polymorphic.
3.4.11.3.
-
The block type must be valid as some instruction type .
-
Let be the same context as , but with the result type prepended to the vector.
-
Under context , the instruction sequence must be valid with type .
-
Then the compound instruction is valid with type .
Note
The notation inserts the new label type at index , shifting all others.
3.4.11.4.
-
The block type must be valid as some instruction type .
-
Let be the same context as , but with the result type prepended to the vector.
-
Under context , the instruction sequence must be valid with type .
-
Then the compound instruction is valid with type .
Note
The notation inserts the new label type at index , shifting all others.
3.4.11.5.
-
The block type must be valid as some instruction type .
-
Let be the same context as , but with the result type prepended to the vector.
-
Under context , the instruction sequence must be valid with type .
-
Under context , the instruction sequence must be valid with type .
-
Then the compound instruction is valid with type .
Note
The notation inserts the new label type at index , shifting all others.
3.4.11.6.
-
The block type must be valid as some function type .
-
For every catch clause in , must be valid.
-
Let be the same context as , but with the result type prepended to the vector.
-
Under context , the instruction sequence must be valid with type .
-
Then the compound instruction is valid with type .
Note
The notation inserts the new label type at index , shifting all others.
3.4.11.7.
-
The tag must be defined in the context.
-
The result type must be empty.
-
The label must be defined in the context.
-
The result type must be the same as .
-
Then the catch clause is valid.
3.4.11.8.
-
The tag must be defined in the context.
-
The result type must be empty.
-
The label must be defined in the context.
-
The result type must match .
-
Then the catch clause is valid.
3.4.11.9.
-
The label must be defined in the context.
-
The result type must be empty.
-
Then the catch clause is valid.
3.4.11.10.
-
The label must be defined in the context.
-
The result type must match .
-
Then the catch clause is valid.
3.4.11.11.
-
The label must be defined in the context.
-
Let be the result type .
-
Then the instruction is valid with any valid type of the form .
Note
The label index space in the context contains the most recent label type first, so that performs a relative lookup as expected.
The instruction is stack-polymorphic.
3.4.11.12.
-
The label must be defined in the context.
-
Let be the result type .
-
Then the instruction is valid with type .
Note
The label index space in the context contains the most recent label type first, so that performs a relative lookup as expected.
3.4.11.13.
-
The label must be defined in the context.
-
For each label in , the label must be defined in the context.
-
There must be a sequence of value types, such that:
-
Then the instruction is valid with any valid type of the form .
Note
The label index space in the context contains the most recent label first, so that performs a relative lookup as expected.
The instruction is stack-polymorphic.
Furthermore, the result type is also chosen non-deterministically in this rule. Although it may seem necessary to compute as the greatest lower bound of all label types in practice, a simple linear algorithm does not require this.
3.4.11.14.
-
The label must be defined in the context.
-
Let be the result type .
-
Then the instruction is valid with type for any valid heap type .
3.4.11.15.
-
The label must be defined in the context.
-
Let be the result type .
-
The result type must contain at least one type.
-
Let the value type be the last element in the sequence , and the remainder of the sequence preceding it.
-
The value type must be a reference type of the form .
-
Then the instruction is valid with type .
3.4.11.16.
-
The label must be defined in the context.
-
Let be the result type .
-
The type sequence must be of the form .
-
The reference type must be valid.
-
The reference type must be valid.
-
The reference type must match .
-
The reference type must match .
-
Let be the type difference between and .
-
Then the instruction is valid with type .
3.4.11.17.
-
The label must be defined in the context.
-
Let be the result type .
-
The type sequence must be of the form .
-
The reference type must be valid.
-
The reference type must be valid.
-
The reference type must match .
-
Let be the type difference between and .
-
The reference type must match .
-
Then the instruction is valid with type .
3.4.11.18.
-
The return type must not be absent in the context.
-
Let be the result type of .
-
Then the instruction is valid with any valid type of the form .
Note
The instruction is stack-polymorphic.
is absent (set to ) when validating an expression that is not a function body. This differs from it being set to the empty result type (), which is the case for functions not returning anything.
3.4.11.19.
-
The function must be defined in the context.
-
The expansion of must be a function type .
-
Then the instruction is valid with type .
3.4.11.20.
-
The type must be defined in the context.
-
The expansion of must be a function type .
-
Then the instruction is valid with type .
3.4.11.21.
-
The table must be defined in the context.
-
Let be the table type .
-
The reference type must match type .
-
The type must be defined in the context.
-
The expansion of must be a function type .
-
Then the instruction is valid with type .
3.4.11.22.
-
The return type must not be absent in the context.
-
The function must be defined in the context.
-
The expansion of must be a function type .
-
The result type must match .
-
Then the instruction is valid with any valid type .
Note
The instruction is stack-polymorphic.
3.4.11.23.
-
The type must be defined in the context.
-
The expansion of must be a function type .
-
The result type must match .
-
Then the instruction is valid with any valid type .
Note
The instruction is stack-polymorphic.
3.4.11.24.
-
The return type must not be empty in the context.
-
The table must be defined in the context.
-
Let be the table type .
-
The reference type must match type .
-
The type must be defined in the context.
-
The expansion of must be a function type .
-
The result type must match .
-
Then the instruction is valid with type , for any sequences of value types and .
Note
The instruction is stack-polymorphic.
3.4.11.25.
-
The tag must be defined in the context.
-
Let be the tag type .
-
The result type must be empty.
-
Then the instruction is valid with type , for any sequences of value types and .
Note
The instruction is stack-polymorphic.
3.4.11.26.
-
The instruction is valid with type , for any sequences of value types and .
Note
The instruction is stack-polymorphic.
3.4.12. Instruction Sequences
Typing of instruction sequences is defined recursively.
3.4.12.1. Empty Instruction Sequence:
-
The empty instruction sequence is valid with type .
3.4.12.2. Non-empty Instruction Sequence:
-
The instruction must be valid with some type .
-
Let be the same context as , but with:
-
the same as in C, except that for every local index in , the local type has been updated to initialization status .
-
-
Under the context , the instruction sequence must be valid with some type .
-
Then the combined instruction sequence is valid with type .
3.4.12.3. Subsumption for
-
The instruction sequence must be valid with some type .
-
The instruction type : must be a valid
-
The instruction type must match the type .
-
Then the instruction sequence is also valid with type .
Note
In combination with the previous rule, subsumption allows to compose instructions whose types would not directly fit otherwise. For example, consider the instruction sequence
To type this sequence, its subsequence needs to be valid with an intermediate type. But the direct type of is , not matching the two inputs expected by . The subsumption rule allows to weaken the type of to the supertype , such that it can be composed with and yields the intermediate type for the subsequence. That can in turn be composed with the first constant.
Furthermore, subsumption allows to drop init variables from the instruction type in a context where they are not needed, for example, at the end of the body of a block.
3.4.13. Expressions
Expressions are classified by result types of the form .
3.4.13.1.
-
Then the expression is valid with result type .
3.4.13.2. Constant Expressions
-
In a constant expression all instructions in must be constant.
-
A constant instruction must be:
-
either of the form ,
-
or of the form , where is limited to , , or .
-
or of the form ,
-
or of the form ,
-
or of the form ,
-
or of the form ,
-
or of the form ,
-
or of the form ,
-
or of the form ,
-
or of the form ,
-
or of the form ,
-
or of the form ,
-
or of the form , in which case must be a global type of the form .
-
Note
Currently, constant expressions occurring in globals are further constrained in that contained instructions are only allowed to refer to imported or previously defined globals. Constant expressions occurring in tables may only have instructions that refer to imported globals. This is enforced in the validation rule for modules by constraining the context accordingly.
The definition of constant expression may be extended in future versions of WebAssembly.
3.5. Modules
Modules are valid when all the components they contain are valid. Furthermore, most definitions are themselves classified with a suitable type.
3.5.1. Types
The sequence of types defined in a module is validated incrementally, yielding a suitable context.
3.5.1.1.
-
If the sequence is empty, then:
-
The context must be empty.
-
Then the type sequence is valid.
-
-
Otherwise:
-
Let the recursive type be the last element in the sequence.
-
The sequence without must be valid for some context .
-
Let the type index be the length of , i.e., the first type index free in .
-
Let the sequence of defined types be the result of rolling up into its sequence of defined types.
-
The recursive type must be valid under the context for type index .
-
The current context be the same as , but with appended to .
-
Then the type sequence is valid.
-
Note
Despite the appearance, the context is effectively an _output_ of this judgement.
3.5.2. Functions
Functions are classified by defined types that expand to function types of the form .
3.5.2.1.
-
The defined type must be a function type.
-
Let be the expansion of the defined type .
-
For each local declared by a value type in :
-
The local for type must be valid with local type .
-
-
Let be the concatenation of all .
-
Let be the same context as , but with:
-
set to the sequence of value types , concatenating parameters and locals,
-
set to the singular sequence containing only result type .
-
set to the result type .
-
-
Under the context , the expression must be valid with type .
-
Then the function definition is valid with type .
3.5.3. Locals
Locals are classified with local types.
3.5.3.1.
-
The value type must be valid.
-
If is defaultable, then:
-
The local is valid with local type .
-
-
Else:
-
The local is valid with local type .
-
Note
For cases where both rules are applicable, the former yields the more permissable type.
3.5.4. Tables
Tables are classified by table types.
3.5.4.1.
-
The table type must be valid.
-
Let be the element reference type of .
-
The expression must be valid with result type .
-
The expression must be constant.
-
Then the table definition is valid with type .
3.5.5. Memories
Memories are classified by memory types.
3.5.5.1.
-
The memory type must be valid.
-
Then the memory definition is valid with type .
3.5.6. Globals
Globals are classified by global types of the form .
Sequences of globals are handled incrementally, such that each definition has access to previous definitions.
3.5.6.1.
-
The global type must be valid.
-
The expression must be valid with result type .
-
The expression must be constant.
-
Then the global definition is valid with type .
3.5.6.2.
-
If the sequence is empty, then it is valid with the empty sequence of global types.
-
Else:
-
The first global definition must be valid with some type global type .
-
Let be the same context as , but with the global type apppended to the vector.
-
Under context , the remainder of the sequence must be valid with some sequence of global types.
-
Then the sequence is valid with the sequence of global types consisting of prepended to .
-
3.5.8. Element Segments
Element segments are classified by the reference type of their elements.
3.5.8.1.
-
The reference type must be valid.
-
For each in :
-
The expression must be valid with some result type .
-
The expression must be constant.
-
-
The element mode must be valid with some reference type .
-
The reference type must match the reference type .
-
Then the element segment is valid with reference type .
3.5.8.2.
-
The element mode is valid with any valid reference type.
3.5.8.3.
-
The table must be defined in the context.
-
Let be the table type .
-
The expression must be valid with result type .
-
The expression must be constant.
-
Then the element mode is valid with reference type .
3.5.8.4.
-
The element mode is valid with any valid reference type.
3.5.9. Data Segments
Data segments are not classified by any type but merely checked for well-formedness.
3.5.9.1.
-
The data mode must be valid.
-
Then the data segment is valid.
3.5.9.2.
-
The data mode is valid.
3.5.9.3.
-
The memory must be defined in the context.
-
The expression must be valid with result type .
-
The expression must be constant.
-
Then the data mode is valid.
3.5.10. Start Function
Start function declarations are not classified by any type.
3.5.10.1.
-
The function must be defined in the context.
-
The expansion of must be a function type .
-
Then the start function is valid.
3.5.11. Exports
Exports and export descriptions are classified by their external type.
3.5.11.1.
-
The export description must be valid with external type .
-
Then the export is valid with external type .
3.5.11.2.
-
The function must be defined in the context.
-
Let be the defined type .
-
Then the export description is valid with external type .
3.5.11.3.
-
The table must be defined in the context.
-
Then the export description is valid with external type .
3.5.11.4.
-
The memory must be defined in the context.
-
Then the export description is valid with external type .
3.5.11.5.
-
The global must be defined in the context.
-
Then the export description is valid with external type .
3.5.11.6.
-
The tag must be defined in the context.
-
Then the export description is valid with external type .
3.5.12. Imports
Imports and import descriptions are classified by external types.
3.5.12.1.
-
The import description must be valid with type .
-
Then the import is valid with type .
3.5.12.2.
-
The defined type must be a function type.
-
Then the import description is valid with type .
3.5.12.3.
-
The table type must be valid.
-
Then the import description is valid with type .
3.5.12.4.
-
The memory type must be valid.
-
Then the import description is valid with type .
3.5.12.5.
-
The global type must be valid.
-
Then the import description is valid with type .
3.5.12.6.
-
Let be the tag .
-
The type must be defined in the context.
-
The tag type must be a valid tag type.
-
Then the import description is valid with type .
3.5.13. Modules
Modules are classified by their mapping from the external types of their imports to those of their exports.
A module is entirely closed, that is, its components can only refer to definitions that appear in the module itself. Consequently, no initial context is required. Instead, the context for validation of the module’s content is constructed from the definitions in the module.
The external types classifying a module may contain free type indices that refer to types defined within the module.
-
Let be the module to validate.
-
Let be a context where:
-
is ,
-
is concatenated with , with the import’s external types and the internal defined types as determined below,
-
is concatenated with , with the import’s external types and the internal table types as determined below,
-
is concatenated with , with the import’s external types and the internal memory types as determined below,
-
is concatenated with , with the import’s external types and the internal global types as determined below,
-
is concatenated with , with the import’s external types and the internal tag types as determined below,
-
is as determined below,
-
is , where is the length of the vector ,
-
is empty,
-
is empty,
-
is empty.
-
is the set , i.e., the set of function indices occurring in the module, except in its functions or start function.
-
-
Let be the context where:
-
is the sequence ,
-
is the same as ,
-
is the same as ,
-
is the same as ,
-
is the same as ,
-
is the same as ,
-
all other fields are empty.
-
-
Under the context :
-
The sequence of globals must be valid with a sequence of global types.
-
For each in , the definition must be valid with a table type .
-
For each in , the definition must be valid with a memory type .
-
-
Under the context :
-
For each in , the definition must be valid with a defined type .
-
For each in , the definition must be valid with a tag type .
-
For each in , the segment must be valid with reference type .
-
For each in , the segment must be valid.
-
If is non-empty, then must be valid.
-
For each in , the segment must be valid with an external type .
-
For each in , the segment must be valid with external type .
-
-
Let be the concatenation of the internal function types , in index order.
-
Let be the concatenation of the internal table types , in index order.
-
Let be the concatenation of the internal memory types , in index order.
-
Let be the concatenation of the internal global types , in index order.
-
Let be the concatenation of the internal tag types , in index order.
-
Let be the concatenation of the reference types , in index order.
-
Let be the concatenation of external types of the imports, in index order.
-
Let be the concatenation of external types of the exports, in index order.
-
The length of must not be larger than .
-
All export names must be different.
-
Then the module is valid with external types .
Note
All functions in a module are mutually recursive. Consequently, the definition of the context in this rule is recursive: it depends on the outcome of validation of the function, table, memory, and global definitions contained in the module, which itself depends on . However, this recursion is just a specification device. All types needed to construct can easily be determined from a simple pre-pass over the module that does not perform any actual validation.
Globals, however, are not recursive but evaluated sequentially, such that each constant expressions only has access to imported or previously defined globals.
4. Execution
4.1. Conventions
WebAssembly code is executed when instantiating a module or invoking an exported function on the resulting module instance.
Execution behavior is defined in terms of an abstract machine that models the program state. It includes a stack, which records operand values and control constructs, and an abstract store containing global state.
For each instruction, there is a rule that specifies the effect of its execution on the program state. Furthermore, there are rules describing the instantiation of a module. As with validation, all rules are given in two equivalent forms:
-
In prose, describing the execution in intuitive form.
-
In formal notation, describing the rule in mathematical form. [1]
Note
As with validation, the prose and formal rules are equivalent, so that understanding of the formal notation is not required to read this specification. The formalism offers a more concise description in notation that is used widely in programming languages semantics and is readily amenable to mathematical proof.
4.1.1. Prose Notation
Execution is specified by stylised, step-wise rules for each instruction of the abstract syntax. The following conventions are adopted in stating these rules.
-
The execution rules implicitly assume a given store .
-
The execution rules also assume the presence of an implicit stack that is modified by pushing or popping values, labels, and frames.
-
Certain rules require the stack to contain at least one frame. The most recent frame is referred to as the current frame.
-
Both the store and the current frame are mutated by replacing some of their components. Such replacement is assumed to apply globally.
-
The execution of an instruction may trap, in which case the entire computation is aborted and no further modifications to the store are performed by it. (Other computations can still be initiated afterwards.)
-
The execution of an instruction may also end in a jump to a designated target, which defines the next instruction to execute.
-
Execution can enter and exit instruction sequences that form blocks.
-
Instruction sequences are implicitly executed in order, unless a trap or jump occurs, or an exception is thrown.
-
In various places the rules contain assertions expressing crucial invariants about the program state.
4.1.2. Formal Notation
Note
This section gives a brief explanation of the notation for specifying execution formally. For the interested reader, a more thorough introduction can be found in respective text books. [2]
The formal execution rules use a standard approach for specifying operational semantics, rendering them into reduction rules. Every rule has the following general form:
A configuration is a syntactic description of a program state. Each rule specifies one step of execution. As long as there is at most one reduction rule applicable to a given configuration, reduction – and thereby execution – is deterministic. WebAssembly has only very few exceptions to this, which are noted explicitly in this specification.
For WebAssembly, a configuration typically is a tuple consisting of the current store , the call frame of the current function, and the sequence of instructions that is to be executed. (A more precise definition is given later.)
To avoid unnecessary clutter, the store and the frame are omitted from reduction rules that do not touch them.
There is no separate representation of the stack. Instead, it is conveniently represented as part of the configuration’s instruction sequence. In particular, values are defined to coincide with instructions, and a sequence of instructions can be interpreted as an operand “stack” that grows to the right.
Note
For example, the reduction rule for the instruction can be given as follows:
Per this rule, two instructions and the instruction itself are removed from the instruction stream and replaced with one new instruction. This can be interpreted as popping two values off the stack and pushing the result.
When no result is produced, an instruction reduces to the empty sequence:
Labels and frames are similarly defined to be part of an instruction sequence.
The order of reduction is determined by the definition of an appropriate evaluation context.
Reduction terminates when no more reduction rules are applicable. Soundness of the WebAssembly type system guarantees that this is only the case when the original instruction sequence has either been reduced to a sequence of instructions, which can be interpreted as the values of the resulting operand stack, or if a trap or an uncaught exception occurred.
Note
For example, the following instruction sequence,
terminates after three steps:
where and and .
The semantics is derived from the following article: Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. Bringing the Web up to Speed with WebAssembly. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017.
For example: Benjamin Pierce. Types and Programming Languages. The MIT Press 2002
4.2. 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.
4.2.1. 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 instructions and 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.
Note
Future versions of WebAssembly may add additional forms of reference.
Value types can have an associated default value; it is the respective value for number types, for vector types, and null for nullable reference types. For other references, no default value is defined, hence is an optional value .
4.2.1.1. Convention
-
The meta variable ranges over reference values where clear from context.
4.2.2. Results
A result is the outcome of a computation. It is either a sequence of values, an uncaught exception, or a trap.
4.2.3. 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. [1]
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:
In practice, implementations may apply techniques like garbage collection or reference counting to remove objects from the store that are no longer referenced. However, such techniques are not semantically observable, and hence outside the scope of this specification.
4.2.3.1. Convention
-
The meta variable ranges over stores where clear from context.
4.2.4. 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.
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 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.
4.2.4.1. Conventions
-
The notation denotes the set of addresses from address space occurring free in . We sometimes reinterpret this set as the vector of its elements.
4.2.5. 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.
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.
4.2.6. 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.
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.
4.2.7. Table Instances
A table instance is the runtime representation of a table. It records its type and holds a sequence of reference values.
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 . It also is an invariant that the length of the element sequence never exceeds the maximum size of , if present.
4.2.8. Memory Instances
A memory instance is the runtime representation of a linear memory. It records its type and holds a sequence of bytes.
The length of the sequence always is a multiple of the WebAssembly page size, which is defined to be the constant – abbreviated .
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 vector, divided by page size, never exceeds the maximum size of , if present.
4.2.9. Global Instances
A global instance is the runtime representation of a global variable. It records its type and holds an individual value.
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 .
4.2.10. Tag Instances
A tag instance is the runtime representation of a tag definition. It records the type of the tag.
4.2.11. Element Instances
An element instance is the runtime representation of an element segment. It holds a vector of references and their common type.
4.2.12. Data Instances
An data instance is the runtime representation of a data segment. It holds a vector of bytes.
4.2.13. Export Instances
An export instance is the runtime representation of an export. It defines the export’s name and the associated external value.
4.2.14. External Values
An external value is the runtime representation of an entity that can be imported or exported. It is an address denoting either a function instance, table instance, memory instance, tag instances, or global instances in the shared store.
4.2.14.1. Conventions
The following auxiliary notation is defined for sequences of external values. It filters out entries of a specific kind in an order-preserving fashion:
4.2.15. 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 vector of the values of their fields.
4.2.15.1. Conventions
-
Conversion of a regular value to a field value is defined as follows:
-
The inverse conversion of a field value to a regular value is defined as follows:
4.2.16. Exception Instances
An exception instance is the runtime representation of an _exception_ produced by a instruction. It holds the address of the respective tag and the argument values.
4.2.17. 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.
-
Activations: 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.
4.2.17.1. Values
Values are represented by themselves.
4.2.17.2. Labels
Labels carry an argument arity and their associated branch target, which is expressed syntactically as an instruction sequence:
Intuitively, 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
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
When branching, the empty continuation ends the targeted block, such that execution can proceed with consecutive instructions.
4.2.17.3. Activation Frames
Activation frames carry the return arity 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:
Locals may be uninitialized, in which case they are empty. Locals are mutated by respective variable instructions.
4.2.17.4. Exception Handlers
Exception handlers are installed by instructions and record the corresponding list of catch clauses:
The handlers on the stack are searched when an exception is thrown.
4.2.17.5. Conventions
-
The meta variable ranges over labels where clear from context.
-
The meta variable ranges over frame states where clear from context.
-
The meta variable 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:
4.2.18. Administrative Instructions
Note
This section is only relevant for the formal notation.
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:
The instruction represents the occurrence of a trap. Traps are bubbled up through nested instruction sequences, ultimately reducing the entire program to a single instruction, signalling abrupt termination.
The instruction represents unboxed scalar reference values, and represent structure and array references, respectively, represents function references, and represents exception references. Similarly, represents host references and represents any externalized reference.
The instruction represents the imminent invocation of a function instance, identified by its address. It unifies the handling of different forms of calls. Analogously, represents the imminent tail invocation of a function instance.
The , , and 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 with an marker. That way, the end of the inner instruction sequence is known when part of an outer sequence.
Note
For example, the reduction rule for is:
This replaces the block with a label instruction, which can be interpreted as “pushing” the label on the stack. When is reached, i.e., the inner instruction sequence has been reduced to the empty sequence – or rather, a sequence of instructions representing the resulting values – then the instruction is eliminated courtesy of its own reduction rule:
This can be interpreted as removing the label from the stack and only leaving the locally accumulated operand values.
4.2.18.1. Block Contexts
In order to specify the reduction of branches, the following syntax of block contexts is defined, indexed by the count of labels surrounding a hole that marks the place where the next step of computation is taking place:
This definition allows to index active labels surrounding a branch or return instruction.
Note
For example, the reduction of a simple branch can be defined as follows:
Here, the hole of the context is instantiated with a branch instruction. When a branch occurs, this rule replaces the target label and associated instruction sequence with the label’s continuation. The selected label is identified through the label index , which corresponds to the number of surrounding instructions that must be hopped over – which is exactly the count encoded in the index of a block context.
4.2.18.2. Throw Contexts
In order to specify the reduction of blocks, the following syntax of throw contexts is defined, as well as associated structural rules:
Throw contexts allow matching the program context around a throw instruction up to the innermost enclosing exception handler, if one exists.
Note
Contrary to block contexts, throw contexts do not skip over handlers.
4.2.18.3. Configurations
A configuration consists of the current store and an executing thread.
A thread is a computation over instructions that operates relative to the state of a current frame referring to the module instance in which the computation runs, i.e., where the current function originates from.
Note
The current version of WebAssembly is single-threaded, but configurations with multiple threads may be supported in the future.
4.2.18.4. Evaluation Contexts
Finally, the following definition of evaluation context and associated structural rules enable reduction inside instruction sequences and administrative forms as well as the propagation of traps:
Reduction terminates when a thread’s instruction sequence has been reduced to a result, that is, either a sequence of values, to an uncaught exception, or to a .
Note
The restriction on evaluation contexts rules out contexts like and for which .
For an example of reduction under evaluation contexts, consider the following instruction sequence.
This can be decomposed into where
Moreover, this is the only possible choice of evaluation context where the contents of the hole matches the left-hand side of a reduction rule.
4.3. Numerics
Numeric primitives are defined in a generic manner, by operators indexed over a bit width .
Some operators are non-deterministic, because they can return one of several possible results (such as different NaN values). Technically, each operator thus returns a set of allowed values. For convenience, deterministic results are expressed as plain values, which are assumed to be identified with a respective singleton set.
Some operators are partial, because they are not defined on certain inputs. Technically, an empty set of results is returned for these inputs.
In formal notation, each operator is defined by equational clauses that apply in decreasing order of precedence. That is, the first clause that is applicable to the given arguments defines the result. In some cases, similar clauses are combined into one by using the notation or . When several of these placeholders occur in a single clause, then they must be resolved consistently: either the upper sign is chosen for all of them or the lower sign.
Note
For example, the operator is defined as follows:
This definition is to be read as a shorthand for the following expansion of each clause into two separate ones:
Numeric operators are lifted to input sequences by applying the operator element-wise, returning a sequence of results. When there are multiple inputs, they must be of equal length.
Note
For example, the unary operator , when given a sequence of floating-point values, return a sequence of floating-point results:
The binary operator , when given two sequences of integers of the same length, , return a sequence of integer results:
Conventions:
-
The meta variable is used to range over single bits.
-
The meta variable is used to range over (signless) magnitudes of floating-point values, including and .
-
The meta variable is used to range over (signless) rational magnitudes, excluding or .
-
The notation denotes the inverse of a bijective function .
-
Truncation of rational values is written , with the usual mathematical definition:
-
Saturation of integers is written and . The arguments to these two functions range over arbitrary signed integers.
-
Unsigned saturation, clamps to between and :
-
Signed saturation, clamps to between and :
-
4.3.1. Representations
Numbers and numeric vectors have an underlying binary representation as a sequence of bits:
The first case of these applies to representations of both integer value types and packed types.
Each of these functions is a bijection, hence they are invertible.
4.3.1.1. Integers
Integers are represented as base two unsigned numbers:
Boolean operators like , , or are lifted to bit sequences of equal length by applying them pointwise.
4.3.1.2. Floating-Point
Floating-point values are represented in the respective binary format defined by [IEEE-754-2019] (Section 3.4):
where and .
4.3.1.3. Vectors
Numeric vectors of type have the same underlying representation as an . They can also be interpreted as a sequence of numeric values packed into a with a particular , provided that .
This function is a bijection on , hence it is invertible.
4.3.1.4. Storage
When a number is stored into memory, it is converted into a sequence of bytes in little endian byte order:
Again these functions are invertible bijections.
4.3.2. Integer Operations
4.3.2.1. Sign Interpretation
Integer operators are defined on values. Operators that use a signed interpretation convert the value using the following definition, which takes the two’s complement when the value lies in the upper half of the value range (i.e., its most significant bit is ):
This function is bijective, and hence invertible.
4.3.2.2. Boolean Interpretation
The integer result of predicates – i.e., tests and relational operators – is defined with the help of the following auxiliary function producing the value or depending on a condition.
4.3.2.3.
-
Return the result of adding and modulo .
4.3.2.4.
-
Return the result of subtracting from modulo .
4.3.2.5.
-
Return the result of multiplying and modulo .
4.3.2.6.
-
If is , then the result is undefined.
-
Else, return the result of dividing by , truncated toward zero.
Note
This operator is partial.
4.3.2.7.
-
Let be the signed interpretation of .
-
Let be the signed interpretation of .
-
If is , then the result is undefined.
-
Else if divided by is , then the result is undefined.
-
Else, return the result of dividing by , truncated toward zero.
Note
This operator is partial. Besides division by , the result of is not representable as an -bit signed integer.
4.3.2.8.
-
If is , then the result is undefined.
-
Else, return the remainder of dividing by .
4.3.2.9.
-
Let be the signed interpretation of .
-
Let be the signed interpretation of .
-
If is , then the result is undefined.
-
Else, return the remainder of dividing by , with the sign of the dividend .
4.3.2.10.
-
Return the bitwise negation of .
4.3.2.11.
-
Return the bitwise conjunction of and .
4.3.2.12.
-
Return the bitwise conjunction of and the bitwise negation of .
4.3.2.13.
-
Return the bitwise disjunction of and .
4.3.2.14.
-
Return the bitwise exclusive disjunction of and .
4.3.2.15.
-
Let be modulo .
-
Return the result of shifting left by bits, modulo .
4.3.2.16.
-
Let be modulo .
-
Return the result of shifting right by bits, extended with bits.
4.3.2.17.
-
Let be modulo .
-
Return the result of shifting right by bits, extended with the most significant bit of the original value.
4.3.2.18.
-
Let be modulo .
-
Return the result of rotating left by bits.
4.3.2.19.
-
Let be modulo .
-
Return the result of rotating right by bits.
4.3.2.20.
-
Return the count of leading zero bits in ; all bits are considered leading zeros if is .
4.3.2.21.
-
Return the count of trailing zero bits in ; all bits are considered trailing zeros if is .
4.3.2.22.
-
Return the count of non-zero bits in .
4.3.2.23.
-
Return if is zero, otherwise.
4.3.2.24.
-
Return if equals , otherwise.
4.3.2.25.
-
Return if does not equal , otherwise.
4.3.2.26.
-
Return if is less than , otherwise.
4.3.2.27.
-
Let be the signed interpretation of .
-
Let be the signed interpretation of .
-
Return if is less than , otherwise.
4.3.2.28.
-
Return if is greater than , otherwise.
4.3.2.29.
-
Let be the signed interpretation of .
-
Let be the signed interpretation of .
-
Return if is greater than , otherwise.
4.3.2.30.
-
Return if is less than or equal to , otherwise.
4.3.2.31.
-
Let be the signed interpretation of .
-
Let be the signed interpretation of .
-
Return if is less than or equal to , otherwise.
4.3.2.32.
-
Return if is greater than or equal to , otherwise.
4.3.2.33.
-
Let be the signed interpretation of .
-
Let be the signed interpretation of .
-
Return if is greater than or equal to , otherwise.
4.3.2.34.
-
Let be the result of computing .
-
Return .
4.3.2.35.
-
Let be the bitwise conjunction of and .
-
Let be the bitwise negation of .
-
Let be the bitwise conjunction of and .
-
Return the bitwise disjunction of and .
4.3.2.36.
-
Let be the signed interpretation of .
-
If is greater than or equal to , then return .
-
Else return the negation of j, modulo .
4.3.2.37.
-
Return the result of negating , modulo .
4.3.2.38.
-
Return if is , return otherwise.
4.3.2.39.
-
Return if is , return otherwise.
4.3.2.40.
-
Return if is , return otherwise.
4.3.2.41.
-
Return if is , return otherwise.
4.3.2.42.
-
Let be the result of adding and .
-
Return .
4.3.2.43.
-
Let be the signed interpretation of
-
Let be the signed interpretation of
-
Let be the result of adding and .
-
Return the value whose signed interpretation is .
4.3.2.44.
-
Let be the result of subtracting from .
-
Return .
4.3.2.45.
-
Let be the signed interpretation of
-
Let be the signed interpretation of
-
Let be the result of subtracting from .
-
Return the value whose signed interpretation is .
4.3.2.46.
-
Let be the result of adding , , and .
-
Return the result of dividing by , truncated toward zero.
4.3.2.47.
-
Return the whose signed interpretation is the result of .
4.3.3. Floating-Point Operations
Floating-point arithmetic follows the [IEEE-754-2019] standard, with the following qualifications:
-
All operators use round-to-nearest ties-to-even, except where otherwise specified. Non-default directed rounding attributes are not supported.
-
Following the recommendation that operators propagate NaN payloads from their operands is permitted but not required.
-
All operators use “non-stop” mode, and floating-point exceptions are not otherwise observable. In particular, neither alternate floating-point exception handling attributes nor operators on status flags are supported. There is no observable difference between quiet and signalling NaNs.
Note
Some of these limitations may be lifted in future versions of WebAssembly.
4.3.3.1. Rounding
Rounding always is round-to-nearest ties-to-even, in correspondence with [IEEE-754-2019] (Section 4.3.1).
An exact floating-point number is a rational number that is exactly representable as a floating-point number of given bit width .
A limit number for a given floating-point bit width is a positive or negative number whose magnitude is the smallest power of that is not exactly representable as a floating-point number of width (that magnitude is for and for ).
A candidate number is either an exact floating-point number or a positive or negative limit number for the given bit width .
A candidate pair is a pair of candidate numbers, such that no candidate number exists that lies between the two.
A real number is converted to a floating-point value of bit width as follows:
-
If is , then return .
-
Else if is an exact floating-point number, then return .
-
Else if greater than or equal to the positive limit, then return .
-
Else if is less than or equal to the negative limit, then return .
-
Else if and are a candidate pair such that , then:
-
If , then let be .
-
Else if , then let be .
-
Else if and the significand of is even, then let be .
-
Else, let be .
-
-
If is , then:
-
If , then return .
-
Else, return .
-
-
Else if is a limit number, then:
-
If , then return .
-
Else, return .
-
-
Else, return .
where:
4.3.3.2. NaN Propagation
When the result of a floating-point operator other than , , or is a NaN, then its sign is non-deterministic and the payload is computed as follows:
-
If the payload of all NaN inputs to the operator is canonical (including the case that there are no NaN inputs), then the payload of the output is canonical as well.
-
Otherwise the payload is picked non-deterministically among all arithmetic NaNs; that is, its most significant bit is and all others are unspecified.
-
In the deterministic profile, however, a positive canonical NaNs is reliably produced in the latter case.
The non-deterministic result is expressed by the following auxiliary function producing a set of allowed outputs from a set of inputs:
4.3.3.3.
-
If either or is a NaN, then return an element of .
-
Else if both and are infinities of opposite signs, then return an element of .
-
Else if both and are infinities of equal sign, then return that infinity.
-
Else if either or is an infinity, then return that infinity.
-
Else if both and are zeroes of opposite sign, then return positive zero.
-
Else if both and are zeroes of equal sign, then return that zero.
-
Else if either or is a zero, then return the other operand.
-
Else if both and are values with the same magnitude but opposite signs, then return positive zero.
-
Else return the result of adding and , rounded to the nearest representable value.
4.3.3.4.
-
If either or is a NaN, then return an element of .
-
Else if both and are infinities of equal signs, then return an element of .
-
Else if both and are infinities of opposite sign, then return .
-
Else if is an infinity, then return that infinity.
-
Else if is an infinity, then return that infinity negated.
-
Else if both and are zeroes of equal sign, then return positive zero.
-
Else if both and are zeroes of opposite sign, then return .
-
Else if is a zero, then return .
-
Else if is a zero, then return negated.
-
Else if both and are the same value, then return positive zero.
-
Else return the result of subtracting from , rounded to the nearest representable value.
Note
Up to the non-determinism regarding NaNs, it always holds that .
4.3.3.5.
-
If either or is a NaN, then return an element of .
-
Else if one of and is a zero and the other an infinity, then return an element of .
-
Else if both and are infinities of equal sign, then return positive infinity.
-
Else if both and are infinities of opposite sign, then return negative infinity.
-
Else if either or is an infinity and the other a value with equal sign, then return positive infinity.
-
Else if either or is an infinity and the other a value with opposite sign, then return negative infinity.
-
Else if both and are zeroes of equal sign, then return positive zero.
-
Else if both and are zeroes of opposite sign, then return negative zero.
-
Else return the result of multiplying and , rounded to the nearest representable value.
4.3.3.6.
-
If either or is a NaN, then return an element of .
-
Else if both and are infinities, then return an element of .
-
Else if both and are zeroes, then return an element of .
-
Else if is an infinity and a value with equal sign, then return positive infinity.
-
Else if is an infinity and a value with opposite sign, then return negative infinity.
-
Else if is an infinity and a value with equal sign, then return positive zero.
-
Else if is an infinity and a value with opposite sign, then return negative zero.
-
Else if is a zero and a value with equal sign, then return positive zero.
-
Else if is a zero and a value with opposite sign, then return negative zero.
-
Else if is a zero and a value with equal sign, then return positive infinity.
-
Else if is a zero and a value with opposite sign, then return negative infinity.
-
Else return the result of dividing by , rounded to the nearest representable value.
4.3.3.7.
The function is the same as fusedMultiplyAdd defined by [IEEE-754-2019] (Section 5.4.1). It computes as if with unbounded range and precision, rounding only once for the final result.
-
If either or or is a NaN, return an element of .
-
Else if either or is a zero and the other is an infinity, then return an element of .
-
Else if both or are infinities of equal sign, and is a negative infinity, then return an element of .
-
Else if both or are infinities of opposite sign, and is a positive infinity, then return an element of .
-
Else if either or is an infinity and the other is a value of the same sign, and is a negative infinity, then return an element of .
-
Else if either or is an infinity and the other is a value of the opposite sign, and is a positive infinity, then return an element of .
-
Else if both and are zeroes of the same sign and is a zero, then return positive zero.
-
Else if both and are zeroes of the opposite sign and is a positive zero, then return positive zero.
-
Else if both and are zeroes of the opposite sign and is a negative zero, then return negative zero.
-
Else return the result of multiplying and , adding to the intermediate, and the final result ref:rounded <aux-ieee> to the nearest representable value.
4.3.3.8.
-
If either or is a NaN, then return an element of .
-
Else if either or is a negative infinity, then return negative infinity.
-
Else if either or is a positive infinity, then return the other value.
-
Else if both and are zeroes of opposite signs, then return negative zero.
-
Else return the smaller value of and .
4.3.3.9.
-
If either or is a NaN, then return an element of .
-
Else if either or is a positive infinity, then return positive infinity.
-
Else if either or is a negative infinity, then return the other value.
-
Else if both and are zeroes of opposite signs, then return positive zero.
-
Else return the larger value of and .
4.3.3.10.
-
If and have the same sign, then return .
-
Else return with negated sign.
4.3.3.11.
-
If is a NaN, then return with positive sign.
-
Else if is an infinity, then return positive infinity.
-
Else if is a zero, then return positive zero.
-
Else if is a positive value, then .
-
Else return negated.
4.3.3.12.
-
If is a NaN, then return with negated sign.
-
Else if is an infinity, then return that infinity negated.
-
Else if is a zero, then return that zero negated.
-
Else return negated.
4.3.3.13.
-
If is a NaN, then return an element of .
-
Else if is negative infinity, then return an element of .
-
Else if is positive infinity, then return positive infinity.
-
Else if is a zero, then return that zero.
-
Else if has a negative sign, then return an element of .
-
Else return the square root of .
4.3.3.14.
-
If is a NaN, then return an element of .
-
Else if is an infinity, then return .
-
Else if is a zero, then return .
-
Else if is smaller than but greater than , then return negative zero.
-
Else return the smallest integral value that is not smaller than .
4.3.3.15.
-
If is a NaN, then return an element of .
-
Else if is an infinity, then return .
-
Else if is a zero, then return .
-
Else if is greater than but smaller than , then return positive zero.
-
Else return the largest integral value that is not larger than .
4.3.3.16.
-
If is a NaN, then return an element of .
-
Else if is an infinity, then return .
-
Else if is a zero, then return .
-
Else if is greater than but smaller than , then return positive zero.
-
Else if is smaller than but greater than , then return negative zero.
-
Else return the integral value with the same sign as and the largest magnitude that is not larger than the magnitude of .
4.3.3.17.
-
If is a NaN, then return an element of .
-
Else if is an infinity, then return .
-
Else if is a zero, then return .
-
Else if is greater than but smaller than or equal to , then return positive zero.
-
Else if is smaller than but greater than or equal to , then return negative zero.
-
Else return the integral value that is nearest to ; if two values are equally near, return the even one.
4.3.3.18.
-
If either or is a NaN, then return .
-
Else if both and are zeroes, then return .
-
Else if both and are the same value, then return .
-
Else return .
4.3.3.19.
-
If either or is a NaN, then return .
-
Else if both and are zeroes, then return .
-
Else if both and are the same value, then return .
-
Else return .
4.3.3.20.
-
If either or is a NaN, then return .
-
Else if and are the same value, then return .
-
Else if is positive infinity, then return .
-
Else if is negative infinity, then return .
-
Else if is positive infinity, then return .
-
Else if is negative infinity, then return .
-
Else if both and are zeroes, then return .
-
Else if is smaller than , then return .
-
Else return .
4.3.3.21.
-
If either or is a NaN, then return .
-
Else if and are the same value, then return .
-
Else if is positive infinity, then return .
-
Else if is negative infinity, then return .
-
Else if is positive infinity, then return .
-
Else if is negative infinity, then return .
-
Else if both and are zeroes, then return .
-
Else if is larger than , then return .
-
Else return .
4.3.3.22.
-
If either or is a NaN, then return .
-
Else if and are the same value, then return .
-
Else if is positive infinity, then return .
-
Else if is negative infinity, then return .
-
Else if is positive infinity, then return .
-
Else if is negative infinity, then return .
-
Else if both and are zeroes, then return .
-
Else if is smaller than or equal to , then return .
-
Else return .
4.3.3.23.
-
If either or is a NaN, then return .
-
Else if and are the same value, then return .
-
Else if is positive infinity, then return .
-
Else if is negative infinity, then return .
-
Else if is positive infinity, then return .
-
Else if is negative infinity, then return .
-
Else if both and are zeroes, then return .
-
Else if is smaller than or equal to , then return .
-
Else return .
4.3.3.24.
-
If is less than then return .
-
Else return .
4.3.3.25.
-
If is less than then return .
-
Else return .
4.3.4. Conversions
4.3.4.1.
-
Return .
Note
In the abstract syntax, unsigned extension just reinterprets the same value.
4.3.4.2.
-
Let be the signed interpretation of of size .
-
Return the two’s complement of relative to size .
4.3.4.3.
-
Return modulo .
4.3.4.4.
-
If is a NaN, then the result is undefined.
-
Else if is an infinity, then the result is undefined.
-
Else if is a number and is a value within range of the target type, then return that value.
-
Else the result is undefined.
Note
This operator is partial. It is not defined for NaNs, infinities, or values for which the result is out of range.
4.3.4.5.
-
If is a NaN, then the result is undefined.
-
Else if is an infinity, then the result is undefined.
-
If is a number and is a value within range of the target type, then return that value.
-
Else the result is undefined.
Note
This operator is partial. It is not defined for NaNs, infinities, or values for which the result is out of range.
4.3.4.6.
-
If is a NaN, then return .
-
Else if is negative infinity, then return .
-
Else if is positive infinity, then return .
-
Else, return .
4.3.4.7.
-
If is a NaN, then return .
-
Else if is negative infinity, then return .
-
Else if is positive infinity, then return .
-
Else, return the value whose signed interpretation is .
4.3.4.8.
-
If is a canonical NaN, then return an element of (i.e., a canonical NaN of size ).
-
Else if is a NaN, then return an element of (i.e., any arithmetic NaN of size ).
-
Else, return .
4.3.4.9.
-
If is a canonical NaN, then return an element of (i.e., a canonical NaN of size ).
-
Else if is a NaN, then return an element of (i.e., any NaN of size ).
-
Else if is an infinity, then return that infinity.
-
Else if is a zero, then return that zero.
-
Else, return .
4.3.4.10.
-
Return .
4.3.4.11.
-
Let be the signed interpretation of .
-
Return .
4.3.4.12.
-
Let be the bit sequence .
-
Return the constant for which .
4.3.4.13.
-
Let be the signed interpretation of of size .
-
Return the value whose signed interpretation is .
4.3.4.14.
-
Let be the signed interpretation of of size .
-
Return .
4.3.5. Relaxed Operations
The result of relaxed operators are implementation-dependent, because the set of possible results may depend on properties of the host environment, such as its hardware. Technically, their behaviour is controlled by a set of global parameters to the semantics that an implementation can instantiate in different ways. These choices are fixed, that is, parameters are constant during the execution of any given program.
Every such parameter is an index into a sequence of possible sets of results and must be instantiated to a defined index. In the deterministic profile, every parameter is prescribed to be 0. This behaviour is expressed by the following auxiliary function, where is a global parameter selecting one of the allowed outcomes:
Note
Each parameter can be thought of as inducing a family of operations that is fixed to one particular choice by an implementation. The fixed operation itself can still be non-deterministic or partial.
Implementations are expexted to either choose the behaviour that is the most efficient on the underlying hardware, or the behaviour of the deterministic profile.
4.3.5.1.
The implementation-specific behaviour of this operation is determined by the global parameter .
-
Return or .
Note
Relaxed multiply-add allows for fused or unfused results, which leads to implementation-dependent rounding behaviour. In the deterministic profile, the unfused behaviour is used.
4.3.5.2.
-
Return .
Note
This operation is implementation-dependent because is implementation-dependent.
4.3.5.3.
The implementation-specific behaviour of this operation is determined by the global parameter .
-
If is a NaN, then return , NAN(n), z_2, z_2 ]`.
-
If is a NaN, then return , z_1, NAN(n), z_1 ]`.
-
If both and are zeroes of opposite sign, then return , pm 0, mp 0, -0 ]`.
-
Return .
Note
Relaxed minimum is implementation-dependent for NaNs and for zeroes with different signs. In the deterministic profile, it behaves like regular .
4.3.5.4.
The implementation-specific behaviour of this operation is determined by the global parameter .
-
If is a NaN, then return , NAN(n), z_2, z_2 ]`.
-
If is a NaN, then return , z_1, NAN(n), z_1 ]`.
-
If both and are zeroes of opposite sign, then return , pm 0, mp 0, +0 ]`.
-
Return .
Note
Relaxed maximum is implementation-dependent for NaNs and for zeroes with different signs. In the deterministic profile, it behaves like regular .
4.3.5.5.
This is an auxiliary operator for the specification of .
The implementation-specific behaviour of this operation is determined by the global parameter .
-
Return .
Note
Relaxed dot product is implementation-dependent when the second operand is negative in a signed intepretation. In the deterministic profile, it behaves like signed dot product.
4.3.5.6.
The implementation-specific behaviour of this operation is determined by the global parameter .
-
If both and equal , then return .
-
Return
Note
Relaxed Q15 multiplication is implementation-dependent when the result overflows. In the deterministic profile, it behaves like regular .
4.3.5.7.
The implementation-specific behaviour of this operation is determined by the global parameter .
-
If is normal or subnormal and is non-negative and less than , then return .
-
Else, return .
Note
Relaxed unsigned truncation is implementation-dependent for NaNs and out-of-range values. In the deterministic profile, it behaves like regular .
4.3.5.8.
The implementation-specific behaviour of this operation is determined by the global parameter .
-
If is normal or subnormal and is greater than or equal to and less than , then return .
-
Else, return .
Note
Relaxed signed truncation is implementation-dependent for NaNs and out-of-range values. In the deterministic profile, it behaves like regular .
4.3.5.9.
The implementation-specific behaviour of this operation is determined by the global parameter .
-
For each in , let be the value .
-
Let be the concatenation of all .
-
Return .
where:
Note
Relaxed swizzle is implementation-dependent if the signed interpretation of any of the 8-bit indices in is larger than or equal to 16. In the deterministic profile, it behaves like regular .
4.3.5.10.
The implementation-specific behaviour of this operation is determined by the global parameter .
-
If is smaller than , then let be the value , otherwise .
-
Let be .
-
Return .
Note
Relaxed lane selection is non-deterministic when the mask mixes set and cleared bits, since the value of the high bit may or may not be expanded to all bits. In the deterministic profile, it behaves like .
4.4. Types
Execution has to check and compare types in a few places, such as executing or instantiating modules.
It is an invariant of the semantics that all types occurring during execution are closed.
Note
Runtime type checks generally involve types from multiple modules or types not defined by a module at all, such that module-local type indices are not meaningful.
4.4.1. Instantiation
Any form of type can be instantiated into a closed type inside a module instance by substituting each type index occurring in it with the corresponding defined type .
Note
This is the runtime equivalent to type closure.
4.5. Values
4.5.1. 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 in which possibly referenced addresses live.
4.5.1.1. Numeric Values
-
The value is valid with number type .
4.5.1.2. Vector Values
-
The value is valid with vector type .
4.5.1.3. Null References
-
Then the value is valid with reference type , where the heap type is the least type that matches .
Note
A null reference is typed with the least type in its respective hierarchy. That ensures that it is compatible with any nullable type in that hierarchy.
4.5.1.4. Scalar References
-
The value is valid with reference type .
4.5.1.5. Structure References
-
The structure address must exist in the store.
-
Let be the structure instance .
-
Let be the defined type .
-
The expansion of must be a struct type.
-
Then the value is valid with reference type .
4.5.1.6. Array References
-
The array address must exist in the store.
-
Let be the array instance .
-
Let be the defined type .
-
The expansion of must be an array type.
-
Then the value is valid with reference type .
4.5.1.7. Exception References
-
The store entry must exist.
-
Then the value is valid with reference type .
4.5.1.8. Function References
-
The function address must exist in the store.
-
Let be the function instance .
-
Let be the defined type .
-
The expansion of must be a function type.
-
Then the value is valid with reference type .
4.5.1.9. Host References
-
The value is valid with reference type .
Note
A host reference is considered internalized by this rule.
4.5.1.10. External References
-
The reference value must be valid with some reference type .
-
Then the value is valid with reference type .
4.5.1.11. Subsumption
-
The value must be valid with some value type .
-
Then the value is valid with type .
4.5.2. 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 in which the referenced instances live.
4.5.2.1.
-
The store entry must exist.
-
Then is valid with external type .
4.5.2.2.
-
The store entry must exist.
-
Then is valid with external type .
4.5.2.3.
-
The store entry must exist.
-
Then is valid with external type .
4.5.2.4.
-
The store entry must exist.
-
Then is valid with external type .
4.5.2.5.
-
The store entry must exist.
-
Let be the function type .
-
Then is valid with external type .
4.5.2.6. Subsumption
-
The external value must be valid with some external type .
-
Then the external value is valid with type .
4.6. Instructions
WebAssembly computation is performed by executing individual instructions.
4.6.1. 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 applied to operands invokes , which maps to the generic via the above definition. Similarly, applied to invokes , which maps to the generic .
4.6.1.1.
-
Push the value to the stack.
Note
No formal reduction rule is required for this instruction, since instructions already are values.
4.6.1.2.
-
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.
-
4.6.1.3.
-
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.
-
4.6.1.4.
-
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.
4.6.1.5.
-
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.
4.6.1.6.
-
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.
-
4.6.2. Reference Instructions
4.6.2.1.
-
Assert: due to validation, the defined type exists.
-
Let be the defined type .
-
Push the value to the stack.
Note
No formal reduction rule is required for the case , since the instruction form is already a value.
4.6.2.2.
-
Assert: due to validation, exists.
-
Let be the function address .
-
Push the value to the stack.
4.6.2.3.
-
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.
-
4.6.2.4.
-
Assert: due to validation, a reference value is on the top of the stack.
-
Pop the value from the stack.
-
If is , then:
-
Trap.
-
-
Push the value back to the stack.
4.6.2.5.
-
Assert: due to validation, two reference values are on the top of the stack.
-
Pop the value from the stack.
-
Pop the value from the stack.
-
If is the same as , then:
-
Push the value to the stack.
-
-
Else:
-
Push the value to the stack.
-
4.6.2.6.
-
Let be the reference type .
-
Assert: due to validation, is closed.
-
Assert: due to validation, a reference value is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, the reference value is valid with some reference type.
-
Let be the reference type of .
-
If the reference type matches , then:
-
Push the value to the stack.
-
-
Else:
-
Push the value to the stack.
-
4.6.2.7.
-
Let be the reference type .
-
Assert: due to validation, is closed.
-
Assert: due to validation, a reference value is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, the reference value is valid with some reference type.
-
Let be the reference type of .
-
If the reference type matches , then:
-
Push the value back to the stack.
-
-
Else:
-
Trap.
-
4.6.2.8.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
Let be the result of computing .
-
Push the reference value to the stack.
4.6.2.9.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
If is , then:
-
Trap.
-
-
Assert: due to validation, a is a scalar reference.
-
Let be the reference value .
-
Let be the result of computing .
-
Push the value to the stack.
4.6.2.10.
-
Assert: due to validation, the defined type exists.
-
Let be the defined type .
-
Assert: due to validation, the expansion of is a structure type.
-
Let be the expanded structure type of .
-
Let be the length of the field type sequence .
-
Assert: due to validation, values are on the top of the stack.
-
Pop the values from the stack.
-
For every value in and corresponding field type in :
-
Let be the result of computing .
-
-
Let the concatenation of all field values .
-
Let be the structure instance .
-
Let be the length of .
-
Append to .
-
Push the structure reference to the stack.
4.6.2.11.
-
Assert: due to validation, the defined type exists.
-
Let be the defined type .
-
Assert: due to validation, the expansion of is a structure type.
-
Let be the expanded structure type of .
-
Let be the length of the field type sequence .
-
For every field type in :
-
Let be the value type .
-
Assert: due to validation, is defined.
-
Push the value to the stack.
-
-
Execute the instruction .
4.6.2.12.
-
Assert: due to validation, the defined type exists.
-
Let be the defined type .
-
Assert: due to validation, the expansion of is a structure type with at least fields.
-
Let be the expanded structure type of .
-
Let be the -th field type of .
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
If is , then:
-
Trap.
-
-
Assert: due to validation, a is a structure reference.
-
Let be the reference value .
-
Assert: due to validation, the structure instance exists and has at least fields.
-
Let be the field value .
-
Let be the result of computing .
-
Push the value to the stack.
4.6.2.13.
-
Assert: due to validation, the defined type exists.
-
Let be the defined type .
-
Assert: due to validation, the expansion of is a structure type with at least fields.
-
Let be the expanded structure type of .
-
Let be the -th field type of .
-
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 type is on the top of the stack.
-
Pop the value from the stack.
-
If is , then:
Trap.
-
Assert: due to validation, a is a structure reference.
-
Let be the reference value .
-
Assert: due to validation, the structure instance exists and has at least fields.
-
Let be the result of computing .
-
Replace the field value with .
4.6.2.14.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
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 times.
-
Execute the instruction .
4.6.2.15.
-
Assert: due to validation, the defined type exists.
-
Let be the defined type .
-
Assert: due to validation, the expansion of is an array type.
-
Let be the expanded array type of .
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
Let be the value type .
-
Assert: due to validation, is defined.
-
Push the value to the stack times.
-
Execute the instruction .
4.6.2.16.
-
Assert: due to validation, the defined type exists.
-
Let be the defined type .
-
Assert: due to validation, the expansion of is a array type.
-
Let be the expanded array type of .
-
Assert: due to validation, values are on the top of the stack.
-
Pop the values from the stack.
-
For every value in :
-
Let be the result of computing .
-
-
Let be the concatenation of all field values .
-
Let be the array instance .
-
Let be the length of .
-
Append to .
-
Push the array reference to the stack.
4.6.2.17.
-
Assert: due to validation, the defined type exists.
-
Let be the defined type .
-
Assert: due to validation, the expansion of is an array type.
-
Let be the expanded array type of .
-
Assert: due to validation, the data address exists.
-
Let be the data address .
-
Assert: due to validation, the data instance exists.
-
Let be the data instance .
-
Assert: due to validation, two values of type are on the top of the stack.
-
Pop the value from the stack.
-
Pop the value from the stack.
-
Assert: due to validation, the field type has a defined bit width.
-
Let be the bit width of field type divided by eight.
-
If the sum of and times is larger than the length of , then:
-
Trap.
-
-
Let be the byte sequence .
-
Let be the value type .
-
For each of the consecutive subsequences of :
-
Assert: due to validation, is defined.
-
Let be the constant for which is .
-
Push the value to the stack.
-
-
Execute the instruction .
4.6.2.18.
-
Assert: due to validation, the element address exists.
-
Let be the element address .
-
Assert: due to validation, the element instance exists.
-
Let be the element instance .
-
Assert: due to validation, two values of type are on the top of the stack.
-
Pop the value from the stack.
-
Pop the value from the stack.
-
If the sum of and is larger than the length of , then:
-
Trap.
-
-
Let be the reference sequence .
-
Push the references to the stack.
-
Execute the instruction .
4.6.2.19.
-
Assert: due to validation, the defined type exists.
-
Let be the defined type .
-
Assert: due to validation, the expansion of is an array type.
-
Let be the expanded array type of .
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
If is , then:
Trap.
-
Assert: due to validation, is an array reference.
-
Let be the reference value .
-
Assert: due to validation, the array instance exists.
-
If is larger than or equal to the length of , then:
-
Trap.
-
-
Let be the field value .
-
Let be the result of computing .
-
Push the value to the stack.
4.6.2.20.
-
Assert: due to validation, the defined type exists.
-
Let be the defined type .
-
Assert: due to validation, the expansion of is an array type.
-
Let be the expanded array type of .
-
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 type is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
If is , then:
Trap.
-
Assert: due to validation, is an array reference.
-
Let be the reference value .
-
Assert: due to validation, the array instance exists.
-
If is larger than or equal to the length of , then:
-
Trap.
-
-
Let be the result of computing .
-
Replace the field value with .
4.6.2.21.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
If is , then:
-
Trap.
-
-
Assert: due to validation, is an array reference.
-
Let be the reference value .
-
Assert: due to validation, the array instance exists.
-
Let be the length of .
-
Push the value to the stack.
4.6.2.22.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
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 type is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
If is , then:
-
Trap.
-
-
Assert: due to validation, is an array reference.
-
Let be the reference value .
-
Assert: due to validation, the array instance exists.
-
If is larger than the length of , then:
-
Trap.
-
-
If , then:
-
Return.
-
-
Push the value to the stack.
-
Push the value to the stack.
-
Push the value to the stack.
-
Execute the instruction .
-
Push the value to the stack.
-
Assert: due to the earlier check against the array size, .
-
Push the value to the stack.
-
Push the value to the stack.
-
Push the value to the stack.
-
Execute the instruction .
4.6.2.23.
-
Assert: due to validation, the defined type exists.
-
Let be the defined type .
-
Assert: due to validation, the expansion of is an array type.
-
Let be the expanded array type .
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
If is , then:
Trap.
-
Assert: due to validation, is an array reference.
-
Let be the reference value .
-
If is , then:
Trap.
-
Assert: due to validation, is an array reference.
-
Let be the reference value .
-
Assert: due to validation, the array instance exists.
-
Assert: due to validation, the array instance exists.
-
If is larger than the length of , then:
-
Trap.
-
-
If 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.
-
Push the value to the stack.
-
Push the value to the stack.
-
Execute .
-
Execute the instruction .
-
Push the value to the stack.
-
Assert: due to the earlier check against the array size, .
-
Push the value to the stack.
-
Push the value to the stack.
-
Assert: due to the earlier check against the array size, .
-
Push the value to the stack.
-
-
Else:
-
Push the value to the stack.
-
Assert: due to the earlier check against the array size, .
-
Push the value to the stack.
-
Push the value to the stack.
-
Assert: due to the earlier check against the array size, .
-
Push the value to the stack.
-
Execute .
-
Execute the instruction .
-
Push the value to the stack.
-
Push the value to the stack.
-
Push the value to the stack.
-
Push the value to the stack.
-
-
Push the value to the stack.
-
Execute the instruction .
Where:
4.6.2.24.
-
Assert: due to validation, the defined type exists.
-
Let be the defined type .
-
Assert: due to validation, the expansion of is an array type.
-
Let be the expanded array type .
-
Assert: due to validation, the data address exists.
-
Let be the data address .
-
Assert: due to validation, the data instance exists.
-
Let be the data instance .
-
Assert: due to validation, three values of 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.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
If is , then:
Trap.
-
Assert: due to validation, is an array reference.
-
Let be the reference value .
-
Assert: due to validation, the array instance exists.
-
Assert: due to validation, the field type has a defined bit width.
-
Let be the bit width of field type divided by eight.
-
If is larger than the length of , or the sum of and times is larger than the length of , then:
-
Trap.
-
-
If , then:
-
Return.
-
-
Let be the byte sequence .
-
Let be the value type .
-
Assert: due to validation, is defined.
-
Let be the constant for which is .
-
Push the value to the stack.
-
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.
-
Push the value to the stack.
-
Execute the instruction .
4.6.2.25.
-
Assert: due to validation, the defined type exists.
-
Let be the defined type .
-
Assert: due to validation, the expansion of is an array type.
-
Let be the expanded array type .
-
Assert: due to validation, the element address exists.
-
Let be the element address .
-
Assert: due to validation, the element instance exists.
-
Let be the element instance .
-
Assert: due to validation, three values of 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.
-
Assert: due to validation, a value of type is on the top of the stack.
-
Pop the value from the stack.
-
If is , then:
Trap.
-
Assert: due to validation, is an array reference.
-
Let be the reference value .
-
Assert: due to validation, the array instance exists.
-
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.
-
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.
-
Push the value to the stack.
-
Execute the instruction .
4.6.2.26.
-
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 reference value to the stack.
-
-
Else:
-
Assert: due to validation, a is an external reference.
-
Let be the reference value .
-
Push the reference value to the stack.
-
4.6.2.27.
-
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 reference value to the stack.
-
-
Else:
-
Let be the reference value .
-
Push the reference value to the stack.
-
4.6.3. 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 applied to operands invokes , which maps to , where and are sequences resulting from invoking and respectively.
For non-deterministic operators this definition is generalized to sets:
where transforms a sequence of sets of values into a set of sequences of values by computing the set product:
4.6.3.1.
-
Push the value to the stack.
Note
No formal reduction rule is required for this instruction, since instructions coincide with values.
4.6.3.2.
-
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.
4.6.3.3.
-
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.
4.6.3.4.
-
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.
4.6.3.5.
-
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.
4.6.3.6.
-
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.
4.6.3.7.
-
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 onto the stack.
4.6.3.8.
-
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.
4.6.3.9.
-
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.
4.6.3.10.
-
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.
4.6.3.11.
-
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.
4.6.3.12.
-
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.
4.6.3.13.
-
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.
-
4.6.3.14.
-
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.
4.6.3.15.
-
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 bit width of value type .
-
Let be the result of computing .
-
Push the value to the stack.
4.6.3.16.
-
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.
4.6.3.17.
-
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.
4.6.3.18.
-
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.
4.6.3.19.
-
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.
4.6.3.20.
-
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.
4.6.3.21.
-
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.
4.6.3.22.
-
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:
4.6.3.23.
-
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.
4.6.3.24.
-
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.
4.6.3.25.
-
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 .
-
Push the value onto the stack.
4.6.3.26.
-
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
-
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.
4.6.3.27.
-
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:
4.6.3.28.
-
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.
4.6.4. Parametric Instructions
4.6.4.1.
-
Assert: due to validation, a value is on the top of the stack.
-
Pop the value from the stack.
4.6.4.2.
-
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, may allow more than one value per choice.
4.6.5. Variable Instructions
4.6.5.1.
-
Assert: due to validation, exists and is non-empty.
-
Let be the value .
-
Push the value to the stack.
4.6.5.2.
-
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 .
4.6.5.3.
-
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 .
4.6.5.4.
-
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.
4.6.5.5.
-
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.
4.6.6. Table Instructions
4.6.6.1.
-
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 some address 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.
4.6.6.2.
-
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 some address 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 .
4.6.6.3.
-
Assert: due to validation, exists.
-
Let be the table address .
-
Assert: due to validation, exists.
-
Let be the table instance .
-
Let be the table type .
-
Let be the length of .
-
Push the value to the stack.
4.6.6.4.
-
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 some address 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 instruction is non-deterministic. It may either succeed, returning the old table size , or fail, returning . Failure must occur if the referenced table instance has a maximum size defined that would be exceeded. However, failure can occur in other cases as well. In practice, the choice depends on the resources available to the embedder.
4.6.6.5.
-
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 some address 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 address 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 .
4.6.6.6.
-
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 some address type is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, a value of some address type is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, a value of some address 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 .
4.6.6.7.
-
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 some address 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 .
4.6.6.8.
-
Assert: due to validation, exists.
-
Let be the element address .
-
Assert: due to validation, exists.
-
Replace with .
4.6.7. Memory Instructions
Note
The alignment in load and store instructions does not affect the semantics. It is an indication that the offset at which the memory is accessed is intended to satisfy the property . A WebAssembly implementation can use this hint to optimize for the intended use. Unaligned access violating that property is still allowed and must succeed regardless of the annotation. However, it may be substantially slower on some hardware.
4.6.7.1. 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 some address 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.
4.6.7.2.
-
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 some address 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.
4.6.7.3.
-
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 some address 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.
4.6.7.4.
-
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 some address 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.
4.6.7.5.
-
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 some address 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.
4.6.7.6. 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 some address 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 .
4.6.7.7.
-
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 some address 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 .
4.6.7.8.
-
Assert: due to validation, exists.
-
Let be the memory address .
-
Assert: due to validation, exists.
-
Let be the memory instance .
-
Let be the memory type .
-
Let be the length of divided by the page size.
-
Push the value to the stack.
4.6.7.9.
-
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 some address 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 instruction is non-deterministic. It may either succeed, returning the old memory size , or fail, returning . Failure must occur if the referenced memory instance has a maximum size defined that would be exceeded. However, failure can occur in other cases as well. In practice, the choice depends on the resources available to the embedder.
4.6.7.10.
-
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 some address type is on the top of the stack.
-
Pop the value from the stack.
-
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 address 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 .
4.6.7.11.
-
Assert: due to validation, exists.
-
Assert: due to validation, exists.
-
Let be the memory address .
-
Let be the memory address .
-
Assert: due to validation, exists.
-
Assert: due to validation, exists.
-
Let be the memory instance .
-
Let be the memory instance .
-
Assert: due to validation, a value of some address type is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, a value of some address type is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, a value of some address 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 .
4.6.7.12.
-
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 some address 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 .
4.6.7.13.
-
Assert: due to validation, exists.
-
Let be the data address .
-
Assert: due to validation, exists.
-
Replace with the data instance .
4.6.8. Control Instructions
4.6.8.1.
-
Do nothing.
4.6.8.2.
-
Trap.
4.6.8.3.
-
Assert: due to validation, is defined.
-
Let be the instruction 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 .
4.6.8.4.
-
Assert: due to validation, is defined.
-
Let be the instruction 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 .
4.6.8.5.
-
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 .
-
4.6.8.6.
-
Assert: due to validation, exists.
-
Let be the tag address .
-
Assert: due to validation, exists.
-
Let be the tag instance .
-
Let be the tag type .
-
Assert: due to validation, there are at least values on the top of the stack.
-
Pop the values from the stack.
-
Let be the exception address resulting from allocating an exception instance with tag address and initializer values .
-
Let be
-
Push the value to the stack.
-
Execute the instruction .
4.6.8.7.
-
Assert: due to validation, a reference is on the top of the stack.
-
Pop the reference from the stack.
-
If is , then:
-
Trap.
-
-
Assert: due to validation, is an exception reference.
-
Let be .
-
Assert: due to validation, exists.
-
Let be the exception instance .
-
Let be the tag address .
-
While the stack is not empty and the top of the stack is not an exception handler, do:
-
Pop the top element from the stack.
-
-
Assert: the stack is now either empty, or there is an exception handler on the top of the stack.
-
If the stack is empty, then:
Return the exception as a result.
-
Assert: there is an exception handler on the top of the stack.
-
Pop the exception handler from the stack.
-
If is empty, then:
-
Push the exception reference back to the stack.
-
Execute the instruction again.
-
-
Else:
-
Let be the first catch clause in and the remaining clauses.
-
If is of the form and the tag address equals , then:
-
Push the values to the stack.
-
Execute the instruction .
-
-
Else if is of the form and the tag address equals , then:
-
Push the values to the stack.
-
Push the exception reference to the stack.
-
Execute the instruction .
-
-
Else if is of the form , then:
-
Execute the instruction .
-
-
Else if is of the form , then:
-
Push the exception reference to the stack.
-
Execute the instruction .
-
-
Else:
-
Push the modified handler back to the stack.
-
Push the exception reference back to the stack.
-
Execute the instruction again.
-
4.6.8.8.
-
Assert: due to validation, is defined.
-
Let be the instruction type .
-
Assert: due to validation, there are at least values on the top of the stack.
-
Pop the values from the stack.
-
Let be the label whose arity is and whose continuation is the end of the instruction.
-
Enter the block with label and exception handler .
4.6.8.9.
-
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 or a handler, do:
-
Pop the value or handler 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 .
4.6.8.10.
-
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.
-
4.6.8.11.
-
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 .
-
4.6.8.12.
-
Assert: due to validation, a reference value is on the top of the stack.
-
Pop the value from the stack.
-
If is , then:
-
Execute the instruction .
-
-
Else:
-
Push the value back to the stack.
-
4.6.8.13.
-
Assert: due to validation, a reference value is on the top of the stack.
-
Pop the value from the stack.
-
If is , then:
-
Do nothing.
-
-
Else:
-
Push the value back to the stack.
-
Execute the instruction .
-
4.6.8.14.
-
Let be the reference type .
-
Assert: due to validation, is closed.
-
Assert: due to validation, a reference value is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, the reference value is valid with some reference type.
-
Let be the reference type of .
-
Push the value back to the stack.
-
If the reference type matches , then:
-
Execute the instruction .
-
4.6.8.15.
-
Let be the reference type .
-
Assert: due to validation, is closed.
-
Assert: due to validation, a reference value is on the top of the stack.
-
Pop the value from the stack.
-
Assert: due to validation, the reference value is valid with some reference type.
-
Let be the reference type of .
-
Push the value back to the stack.
-
If the reference type does not match , then:
-
Execute the instruction .
-
4.6.8.16.
-
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.
4.6.8.17.
-
Assert: due to validation, exists.
-
Let be the function address .
-
Invoke the function instance at address .
4.6.8.18.
-
Assert: due to validation, a null or function reference is on the top of the stack.
-
Pop the reference value from the stack.
-
If is , then:
-
Trap.
-
-
Assert: due to validation, is a function reference.
-
Let be the reference .
-
Invoke the function instance at address .
4.6.8.19.
-
Assert: due to validation, exists.
-
Let be the table address .
-
Assert: due to validation, exists.
-
Let be the table instance .
-
Assert: due to validation, is defined.
-
Let be the defined 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 defined type .
-
If does not match , then:
-
Trap.
-
-
Invoke the function instance at address .
4.6.8.20.
-
Assert: due to validation, exists.
-
Let be the function address .
-
Tail-invoke the function instance at address .
4.6.8.21.
-
Assert: due to validation, a function reference is on the top of the stack.
-
Pop the reference value from the stack.
-
If is , then:
-
Trap.
-
-
Assert: due to validation, is a function reference.
-
Let be the reference .
-
Tail-invoke the function instance at address .
4.6.8.22.
-
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 defined 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.
-
-
If is uninitialized, then:
-
Trap.
-
-
Let be the function address .
-
Assert: due to validation, exists.
-
Let be the function instance .
-
Let be the defined type .
-
If does not match , then:
-
Trap.
-
-
Tail-invoke the function instance at address .
4.6.9. Blocks
The following auxiliary rules define the semantics of executing an instruction sequence that forms a block.
4.6.9.1. 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 is embedded in the administrative instruction that structured control instructions reduce to directly.
4.6.9.2. Exiting with label
When the end of a block is reached without a jump, exception, 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 instruction. Therefore, execution of a loop falls off the end, unless a backwards branch is performed explicitly.
4.6.10. Exception Handling
The following auxiliary rules define the semantics of entering and exiting blocks.
4.6.10.1. Entering with label and exception handler
-
Push to the stack.
-
Push onto the stack.
-
Jump to the start of the instruction sequence .
Note
No formal reduction rule is needed for entering an exception handler because it is an administrative instruction that the instruction reduces to directly.
4.6.10.2. Exiting an exception handler
When the end of a block is reached without a jump, exception, or trap, then the following steps are performed.
-
Let be the number of values on the top of the stack.
-
Pop the values from the stack.
-
Assert: due to validation, a handler and a label are now on the top of the stack.
-
Pop the label from the stack.
-
Pop the handler from the stack.
-
Push back to the stack.
-
Jump to the position after the of the administrative instruction associated with the handler .
4.6.11. Function Calls
The following auxiliary rules define the semantics of invoking a function instance through one of the call instructions and returning from it.
4.6.11.1. Invocation of function address
-
Assert: due to validation, exists.
-
Let be the function instance, .
-
Let be the composite type .
-
Let be the list of locals .
-
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 .
Note
For non-defaultable types, the respective local is left uninitialized by these rules.
4.6.11.2. Tail-invocation of function address
-
Assert: due to validation, exists.
-
Let be the composite type .
-
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 a frame.
-
Pop the frame from the stack.
-
Push to the stack.
-
Invoke the function instance at address .
4.6.11.3. Returning from a function
When the end of a function is reached without a jump (including through ), or an exception or trap aborting it, then the following steps are performed.
-
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.
4.6.11.4. Host Functions
Invoking a host function has non-deterministic behavior. It may either terminate with a trap, an exception, 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, denotes the implementation-defined execution of host function in current store with arguments . It yields a set of possible outcomes, where each element is either a pair of a modified store and a result or the special value indicating divergence. A host function is non-deterministic if there is at least one argument for which the set of outcomes is not singular.
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 , and given arguments matching the ascribed parameter types , executing the host function must yield a non-empty set of possible outcomes each of which is either divergence or consists of a valid store that is an extension of and a result matching the ascribed return types . All these notions are made precise in the Appendix.
4.6.12. 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 is the result of the evaluation.
Note
Evaluation iterates this reduction rule until reaching a value. Expressions constituting function bodies are executed during function invocation.
4.7. 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.
4.7.1. Allocation
New instances of functions, tables, memories, globals, tags, element segments, and data segments, as well as dynamic data types like structures, arrays, or exceptions, are allocated in a store , as defined by the following auxiliary functions.
4.7.1.1. Functions
-
Let be the function to allocate and its module instance.
-
Let be the defined type .
-
Let be the first free function address in .
-
Let be the function instance .
-
Append to the of .
-
Return .
4.7.1.2. Host Functions
-
Let be the host function to allocate and its defined 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.
4.7.1.3. Tables
-
Let be the table type of the table 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 .
4.7.1.4. Memories
-
Let be the memory type of the memory 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 .
4.7.1.6. Exceptions
-
Let be the tag address associated with the exception to allocate and be the values to initialize the exception with.
-
Let be the first free exception address in .
-
Let be the exception instance .
-
Append to the of .
-
Return .
4.7.1.7. Globals
-
Let be the global type of the global to allocate and its initialization value.
-
Let be the first free global address in .
-
Let be the global instance .
-
Append to the of .
-
Return .
4.7.1.8. 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 .
4.7.1.9. 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 .
4.7.1.10. 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 .
-
Let be the structure of table type .
-
Let be with updated to .
-
If the table type is not valid, then fail.
-
Append to .
-
Set to the table type .
4.7.1.11. 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 .
-
Let be the structure of memory type .
-
Let be with updated to .
-
If the memory type is not valid, then fail.
-
Append times bytes with value to .
-
Set to the memory type .
4.7.1.12. Modules
Todo
update prose for types
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, the initializer reference of the module’s tables, and the reference vectors of the module’s element segments.
-
For each defined type in , do:
-
Let be the instantiation in defined below.
-
-
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 obtained by instantiating in defined below.
-
Let be the table address resulting from allocating with initialization value .
-
-
For each memory in , do:
-
Let be the memory type obtained by insantiating in defined below.
-
Let be the memory address resulting from allocating .
-
-
For each global in , do:
-
Let be the global type obtained by instantiating in defined below.
-
Let be the global address resulting from allocating with initializer value .
-
-
For each tag in , do:
-
Let be the tag type .
-
Let be the tag address resulting from allocating .
-
-
For each element segment in , do:
-
Let be the element reference type obtained by instantiating <type-inst> in defined below.
-
Let be the element address resulting from allocating a 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 defined types in index order.
-
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 tag 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 .
-
Let be the list of tag 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 .
-
Else, if is a tag export for tag 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 is shorthand for multiple allocations of object kind , defined as follows:
Moreover, if the dots are a sequence (as for globals or tables), then the elements of this sequence are passed to the allocation function pointwise.
For types, however, allocation is defined in terms of rolling and substitution of all preceding types to produce a list of closed defined types:
Note
The definition of module allocation is mutually recursive with the allocation of its associated functions, because the resulting module instance is passed to the allocators as an argument, in order to form the necessary closures. In an implementation, this recursion is easily unraveled by mutating one or the other in a secondary step.
4.7.2. Instantiation
Given a store , a module is instantiated with a list of external values supplying the required imports as follows.
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 an exception or trap when initializing a table or memory from an active segment or when 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.
-
-
Let be the external type obtained by instantiating in defined below.
-
If does not match , then:
-
Fail.
-
-
-
Let be the auxiliary frame , that consists of the final module instance , defined below.
-
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 vector of table initialization references determined by and . These may be calculated as follows.
-
For each table in , do:
-
Let be the result of evaluating the initializer expression .
-
Assert: due to validation, is a reference.
-
Let be the reference .
-
-
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 .
-
-
Let be a new module instance allocated from in store with imports , global initializer values , table initializer values , and element segment contents , and let be the extended store produced by module allocation.
-
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
Checking import types assumes that the module instance has already been allocated to compute the respective closed defined types. However, this forward reference merely is a way to simplify the specification. In practice, implementations will likely allocate or canonicalize types beforehand, when compiling a module, in a stage before instantiation and before imports are checked.
Similarly, module allocation and the evaluation of global and table initializers as well as element segments are mutually recursive because the global initialization values , , and element segment contents are passed to the module allocator while depending on the module instance and store returned by allocation. Again, this recursion is just a specification device. In practice, the initialization values can be determined beforehand by staging module allocation such that first, the module’s own function instances are pre-allocated in the store, then the initializer expressions are evaluated in order, allocating globals on the way, then the rest of the module instance is allocated, and finally the new function instances’ fields are set to that module instance. This is possible because validation ensures that initialization expressions cannot actually call a function, only take their reference.
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.
4.7.3. Invocation
Once a module has been instantiated, any exported function can be invoked externally via its function address in the store and an appropriate list of argument values.
Invocation may fail with an error if the arguments do not fit the function type. Invocation can also result in an exception or 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 or exceptions can occur.
The following steps are performed:
-
Assert: exists.
-
Let be the function instance .
-
Let be the composite 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 are returned as the results of the invocation.
5. Binary Format
5.1. Conventions
The binary format for WebAssembly modules is a dense linear encoding of their abstract syntax. [1]
The format is defined by an attribute grammar whose only terminal symbols are bytes. A byte sequence is a well-formed encoding of a module if and only if it is generated by the grammar.
Each production of this grammar has exactly one synthesized attribute: the abstract syntax that the respective byte sequence encodes. Thus, the attribute grammar implicitly defines a decoding function (i.e., a parsing function for the binary format).
Except for a few exceptions, the binary grammar closely mirrors the grammar of the abstract syntax.
Note
Some phrases of abstract syntax have multiple possible encodings in the binary format. For example, numbers may be encoded as if they had optional leading zeros. Implementations of decoders must support all possible alternatives; implementations of encoders can pick any allowed encoding.
The recommended extension for files containing WebAssembly modules in binary format is “” and the recommended Media Type is “”.
Additional encoding layers – for example, introducing compression – may be defined on top of the basic representation defined here. However, such layers are outside the scope of the current specification.
5.1.1. Grammar
The following conventions are adopted in defining grammar rules for the binary format. They mirror the conventions used for abstract syntax. In order to distinguish symbols of the binary syntax from symbols of the abstract syntax, font is adopted for the former.
-
Terminal symbols are bytes expressed in hexadecimal notation: .
-
Nonterminal symbols are written in typewriter font: .
-
is a sequence of iterations of .
-
is a possibly empty sequence of iterations of . (This is a shorthand for used where is not relevant.)
-
is an optional occurrence of . (This is a shorthand for where .)
-
denotes the same language as the nonterminal , but also binds the variable to the attribute synthesized for . A pattern may also be used instead of a variable, e.g., .
-
Productions are written , where each is the attribute that is synthesized for in the given case, usually from attribute variables bound in .
-
Some productions are augmented by side conditions in parentheses, which restrict the applicability of the production. They provide a shorthand for a combinatorial expansion of the production into many separate cases.
-
If the same meta variable or non-terminal symbol appears multiple times in a production (in the syntax or in an attribute), then all those occurrences must have the same instantiation. (This is a shorthand for a side condition requiring multiple different variables to be equal.)
Note
For example, the binary grammar for number types is given as follows:
Consequently, the byte encodes the type , encodes the type , and so forth. No other byte value is allowed as the encoding of a number type.
The binary grammar for limits is defined as follows:
That is, a limits pair is encoded as either the byte followed by the encoding of a value, or the byte followed by two such encodings. The variables and name the attributes of the respective nonterminals, which in this case are the actual unsigned integers those decode into. The attribute of the complete production then is the abstract syntax for the limit, expressed in terms of the former values.
5.1.2. Auxiliary Notation
When dealing with binary encodings the following notation is also used:
-
denotes the empty byte sequence.
-
is the length of the byte sequence generated from the production in a derivation.
5.1.3. Vectors
Vectors are encoded with their length followed by the encoding of their element sequence.
5.2. Values
5.2.1. Bytes
Bytes encode themselves.
5.2.2. Integers
All integers are encoded using the LEB128 variable-length integer encoding, in either unsigned or signed variant.
Unsigned integers are encoded in unsigned LEB128 format. As an additional constraint, the total number of bytes encoding a value of type must not exceed bytes.
Signed integers are encoded in signed LEB128 format, which uses a two’s complement representation. As an additional constraint, the total number of bytes encoding a value of type must not exceed bytes.
Uninterpreted integers are encoded as signed integers.
Note
The side conditions in the productions for non-terminal bytes of the and encodings restrict the encoding’s length. However, “trailing zeros” are still allowed within these bounds. For example, and are both well-formed encodings for the value as a . Similarly, either of and and are well-formed encodings of the value as a .
The side conditions on the value of terminal bytes further enforce that any unused bits in these bytes must be for positive values and for negative ones. For example, is malformed as a encoding. Similarly, both and are malformed as encodings.
5.2.3. Floating-Point
Floating-point values are encoded directly by their [IEEE-754-2019] (Section 3.4) bit pattern in little endian byte order:
5.2.4. Names
Names are encoded as a vector of bytes containing the [UNICODE] (Section 3.9) UTF-8 encoding of the name’s character sequence.
The auxiliary function expressing this encoding is defined as follows:
Note
Unlike in some other formats, name strings are not 0-terminated.
5.3. Types
Note
In some places, possible types include both type constructors or types denoted by type indices. Thus, the binary format for type constructors corresponds to the encodings of small negative values, such that they can unambiguously occur in the same place as (positive) type indices.
5.3.1. Number Types
Number types are encoded by a single byte.
5.3.2. Vector Types
Vector types are also encoded by a single byte.
5.3.3. Heap Types
Heap types are encoded as either a single byte, or as a type index encoded as a positive signed integer.
5.3.4. Reference Types
Reference types are either encoded by a single byte followed by a heap type, or, as a short form, directly as an abstract heap type.
5.3.5. Value Types
Value types are encoded with their respective encoding as a number type, vector type, or reference type.
Note
The type cannot occur in a module.
Value types can occur in contexts where type indices are also allowed, such as in the case of block types. Thus, the binary format for types corresponds to the signed LEB128 encoding of small negative values, so that they can coexist with (positive) type indices in the future.
5.3.6. Result Types
Result types are encoded by the respective vectors of value types.
5.3.7. Function Types
Function types are encoded by the respective vectors of parameter and result types.
5.3.8. Aggregate Types
Aggregate types are encoded with their respective field types.
5.3.9. Composite Types
Composite types are encoded by a distinct byte followed by a type encoding of the respective form.
5.3.10. Recursive Types
Recursive types are encoded by the byte followed by a vector of sub types. Additional shorthands are recognized for unary recursions and sub types without super types.
5.3.11. Limits
Limits are encoded with a preceding flag indicating whether a maximum is present, and a flag for the address type.
5.3.12. Memory Types
Memory types are encoded with their limits.
5.3.13. Table Types
Table types are encoded with their limits and the encoding of their element reference type.
5.3.14. Global Types
Global types are encoded by their value type and a flag for their mutability.
5.3.15. Tag Types
Tag types are encoded by a type index denoting a function type.
Note
In future versions of WebAssembly, the preceding zero byte may encode additional flags.
5.4. Instructions
Instructions are encoded by opcodes. Each opcode is represented by a single byte, and is followed by the instruction’s immediate arguments, where present. The only exception are structured control instructions, which consist of several opcodes bracketing their nested instruction sequences.
Note
Gaps in the byte code ranges for encoding instructions are reserved for future extensions.
5.4.1. Control Instructions
Control instructions have varying encodings. For structured instructions, the instruction sequences forming nested blocks are delimited with explicit opcodes for and .
Block types are encoded in special compressed form, by either the byte indicating the empty type, as a single value type, or as a type index encoded as a positive signed integer.
Note
The opcode in the encoding of an instruction can be omitted if the following instruction sequence is empty.
Unlike any other occurrence, the type index in a block type is encoded as a positive signed integer, so that its signed LEB128 bit pattern cannot collide with the encoding of value types or the special code , which correspond to the LEB128 encoding of negative integers. To avoid any loss in the range of allowed indices, it is treated as a 33 bit signed integer.
5.4.2. Reference Instructions
Generic reference instructions are represented by single byte codes, others use prefixes and type operands.
5.4.3. Parametric Instructions
Parametric instructions are represented by single byte codes, possibly followed by a type annotation.
5.4.4. Variable Instructions
Variable instructions are represented by byte codes followed by the encoding of the respective index.
5.4.5. Table Instructions
Table instructions are represented either by a single byte or a one byte prefix followed by a variable-length unsigned integer.
5.4.6. Memory Instructions
Each variant of memory instruction is encoded with a different byte code. Loads and stores are followed by the encoding of their immediate, which includes the memory index if bit 6 of the flags field containing alignment is set; the memory index defaults to 0 otherwise.
5.4.7. Numeric Instructions
All variants of numeric instructions are represented by separate byte codes.
The instructions are followed by the respective literal.
All other numeric instructions are plain opcodes without any immediates.
The saturating truncation instructions all have a one byte prefix, whereas the actual opcode is encoded by a variable-length unsigned integer.
5.4.8. Vector Instructions
All variants of vector instructions are represented by separate byte codes. They all have a one byte prefix, whereas the actual opcode is encoded by a variable-length unsigned integer.
Vector loads and stores are followed by the encoding of their immediate.
The instruction is followed by 16 immediate bytes, which are converted into a in byte order:
The instruction is also followed by the encoding of 16 immediates.
and instructions are followed by the encoding of a immediate.
All other vector instructions are plain opcodes without any immediates.
5.4.9. Expressions
Expressions are encoded by their instruction sequence terminated with an explicit opcode for .
5.5. Modules
The binary encoding of modules is organized into sections. Most sections correspond to one component of a module record, except that function definitions are split into two sections, separating their type declarations in the function section from their bodies in the code section.
Note
This separation enables parallel and streaming compilation of the functions in a module.
5.5.1. Indices
All indices are encoded with their respective value.
5.5.2. Sections
Each section consists of
-
a one-byte section id,
-
the size of the contents, in bytes,
-
the actual contents, whose structure is dependent on the section id.
Every section is optional; an omitted section is equivalent to the section being present with empty contents.
The following parameterized grammar rule defines the generic structure of a section with id and contents described by the grammar .
For most sections, the contents encodes a vector. In these cases, the empty result is interpreted as the empty vector.
Note
Other than for unknown custom sections, the is not required for decoding, but can be used to skip sections when navigating through a binary. The module is malformed if the size does not match the length of the binary contents .
The following section ids are used:
Id |
Section |
---|---|
0 | |
1 | |
2 | |
3 | |
4 | |
5 | |
6 | |
7 | |
8 | |
9 | |
10 | |
11 | |
12 | |
13 |
Note
Section ids do not always correspond to the order of sections in the encoding of a module.
5.5.3. Custom Section
Custom sections have the id 0. They are intended to be used for debugging information or third-party extensions, and are ignored by the WebAssembly semantics. Their contents consist of a name further identifying the custom section, followed by an uninterpreted sequence of bytes for custom use.
Note
If an implementation interprets the data of a custom section, then errors in that data, or the placement of the section, must not invalidate the module.
5.5.4. Type Section
The type section has the id 1. It decodes into a vector of recursive types that represent the component of a module.
5.5.5. Import Section
The import section has the id 2. It decodes into a vector of imports that represent the component of a module.
5.5.6. Function Section
The function section has the id 3. It decodes into a vector of type indices that represent the fields of the functions in the component of a module. The and fields of the respective functions are encoded separately in the code section.
5.5.7. Table Section
The table section has the id 4. It decodes into a vector of tables that represent the component of a module.
Note
The encoding of a table type cannot start with byte , hence decoding is unambiguous. The zero byte following it is reserved for future extensions.
5.5.8. Memory Section
The memory section has the id 5. It decodes into a vector of memories that represent the component of a module.
5.5.9. Global Section
The global section has the id 6. It decodes into a vector of globals that represent the component of a module.
5.5.10. Export Section
The export section has the id 7. It decodes into a vector of exports that represent the component of a module.
5.5.11. Start Section
The start section has the id 8. It decodes into an optional start function that represents the component of a module.
5.5.12. Element Section
The element section has the id 9. It decodes into a vector of element segments that represent the component of a module.
Note
The initial integer can be interpreted as a bitfield. Bit 0 distinguishes a passive or declarative segment from an active segment, bit 1 indicates the presence of an explicit table index for an active segment and otherwise distinguishes passive from declarative segments, bit 2 indicates the use of element type and element expressions instead of element kind and element indices.
Additional element kinds may be added in future versions of WebAssembly.
5.5.13. Code Section
The code section has the id 10. It decodes into a vector of code entries that are pairs of value type vectors and expressions. They represent the and field of the functions in the component of a module. The fields of the respective functions are encoded separately in the function section.
The encoding of each code entry consists of
-
the size of the function code in bytes,
-
the actual function code, which in turn consists of
-
the declaration of locals,
-
the function body as an expression.
-
Local declarations are compressed into a vector whose entries consist of
-
a count,
-
a value type,
denoting count locals of the same value type.
Here, ranges over pairs . The meta function concatenates all sequences in . Any code for which the length of the resulting sequence is out of bounds of the maximum size of a vector is malformed.
Note
Like with sections, the code is not needed for decoding, but can be used to skip functions when navigating through a binary. The module is malformed if a size does not match the length of the respective function code.
5.5.14. Data Section
The data section has the id 11. It decodes into a vector of data segments that represent the component of a module.
Note
The initial integer can be interpreted as a bitfield. Bit 0 indicates a passive segment, bit 1 indicates the presence of an explicit memory index for an active segment.
In the current version of WebAssembly, at most one memory may be defined or imported in a single module, so all valid active data segments have a value of .
5.5.15. Data Count Section
The data count section has the id 12. It decodes into an optional u32 that represents the number of data segments in the data section. If this count does not match the length of the data segment vector, the module is malformed.
Note
The data count section is used to simplify single-pass validation. Since the data section occurs after the code section, the and instructions would not be able to check whether the data segment index is valid until the data section is read. The data count section occurs before the code section, so a single-pass validator can use this count instead of deferring validation.
5.5.16. Tag Section
The tag section has the id 13. It decodes into a vector of tags that represent the component of a module.
5.5.17. Modules
The encoding of a module starts with a preamble containing a 4-byte magic number (the string ) and a version field. The current version of the WebAssembly binary format is 1.
The preamble is followed by a sequence of sections. Custom sections may be inserted at any place in this sequence, while other sections must occur at most once and in the prescribed order. All sections can be empty.
The lengths of vectors produced by the (possibly empty) function and code section must match up.
Similarly, the optional data count must match the length of the data segment vector. Furthermore, it must be present if any data index occurs in the code section.
where for each in ,
Note
The version of the WebAssembly binary format may increase in the future if backward-incompatible changes have to be made to the format. However, such changes are expected to occur very infrequently, if ever. The binary format is intended to be forward-compatible, such that future extensions can be made without incrementing its version.
6. Text Format
6.1. Conventions
The textual format for WebAssembly modules is a rendering of their abstract syntax into S-expressions.
Like the binary format, the text format is defined by an attribute grammar. A text string is a well-formed description of a module if and only if it is generated by the grammar. Each production of this grammar has at most one synthesized attribute: the abstract syntax that the respective character sequence expresses. Thus, the attribute grammar implicitly defines a parsing function. Some productions also take a context as an inherited attribute that records bound identifiers.
Except for a few exceptions, the core of the text grammar closely mirrors the grammar of the abstract syntax. However, it also defines a number of abbreviations that are “syntactic sugar” over the core syntax.
The recommended extension for files containing WebAssembly modules in text format is “”. Files with this extension are assumed to be encoded in UTF-8, as per [UNICODE] (Section 2.5).
6.1.1. Grammar
The following conventions are adopted in defining grammar rules of the text format. They mirror the conventions used for abstract syntax and for the binary format. In order to distinguish symbols of the textual syntax from symbols of the abstract syntax, font is adopted for the former.
-
Terminal symbols are either literal strings of characters enclosed in quotes or expressed as [UNICODE] scalar values: , . (All characters written literally are unambiguously drawn from the 7-bit ASCII subset of Unicode.)
-
Nonterminal symbols are written in typewriter font: .
-
is a sequence of iterations of .
-
is a possibly empty sequence of iterations of . (This is a shorthand for used where is not relevant.)
-
is a sequence of one or more iterations of . (This is a shorthand for where .)
-
is an optional occurrence of . (This is a shorthand for where .)
-
denotes the same language as the nonterminal , but also binds the variable to the attribute synthesized for . A pattern may also be used instead of a variable, e.g., .
-
Productions are written , where each is the attribute that is synthesized for in the given case, usually from attribute variables bound in .
-
Some productions are augmented by side conditions in parentheses, which restrict the applicability of the production. They provide a shorthand for a combinatorial expansion of the production into many separate cases.
-
If the same meta variable or non-terminal symbol appears multiple times in a production (in the syntax or in an attribute), then all those occurrences must have the same instantiation.
-
A distinction is made between lexical and syntactic productions. For the latter, arbitrary white space is allowed in any place where the grammar contains spaces. The productions defining lexical syntax and the syntax of values are considered lexical, all others are syntactic.
Note
For example, the textual grammar for number types is given as follows:
The textual grammar for limits is defined as follows:
The variables and name the attributes of the respective nonterminals, which in this case are the actual unsigned integers those parse into. The attribute of the complete production then is the abstract syntax for the limit, expressed in terms of the former values.
6.1.2. Abbreviations
In addition to the core grammar, which corresponds directly to the abstract syntax, the textual syntax also defines a number of abbreviations that can be used for convenience and readability.
Abbreviations are defined by rewrite rules specifying their expansion into the core syntax:
These expansions are assumed to be applied, recursively and in order of appearance, before applying the core grammar rules to construct the abstract syntax.
6.1.3. Contexts
The text format allows the use of symbolic identifiers in place of indices. To resolve these identifiers into concrete indices, some grammar productions are indexed by an identifier context as a synthesized attribute that records the declared identifiers in each index space. In addition, the context records the types defined in the module, so that parameter indices can be computed for functions.
It is convenient to define identifier contexts as records with abstract syntax as follows:
For each index space, such a context contains the list of names assigned to the defined indices, which were denoted by the corresponding identifiers. Unnamed indices are associated with empty () entries in these lists. Fields have dependent name spaces, and hence a separate list of field identifiers per type.
An identifier context is well-formed if no index space contains duplicate identifiers. For fields, names need only be unique within a single type.
6.1.3.1. Conventions
To avoid unnecessary clutter, empty components are omitted when writing out identifier contexts. For example, the record is shorthand for an identifier context whose components are all empty.
6.1.4. Vectors
Vectors are written as plain sequences, but with a restriction on the length of these sequence.
6.2. Lexical Format
6.2.1. Characters
The text format assigns meaning to source text, which consists of a sequence of characters. Characters are assumed to be represented as valid [UNICODE] (Section 2.4) scalar values.
6.2.2. Tokens
The character stream in the source text is divided, from left to right, into a sequence of tokens, as defined by the following grammar.
Tokens are formed from the input character stream according to the longest match rule. That is, the next token always consists of the longest possible sequence of characters that is recognized by the above lexical grammar. Tokens can be separated by white space, but except for strings, they cannot themselves contain whitespace.
Keyword tokens are defined either implicitly by an occurrence of a terminal symbol in literal form, such as , in a syntactic production of this chapter, or explicitly where they arise in this chapter.
Any token that does not fall into any of the other categories is considered reserved, and cannot occur in source text.
Note
The effect of defining the set of reserved tokens is that all tokens must be separated by either parentheses, white space, or comments. For example, is a single reserved token, as is . Consequently, they are not recognized as two separate tokens and , or and , respectively, but instead disallowed. This property of tokenization is not affected by the fact that the definition of reserved tokens overlaps with other token classes.
6.2.3. White Space
White space is any sequence of literal space characters, formatting characters, comments, or annotations. The allowed formatting characters correspond to a subset of the ASCII format effectors, namely, horizontal tabulation (), line feed (), and carriage return ().
The only relevance of white space is to separate tokens. It is otherwise ignored.
6.2.5. Annotations
An annotation is a bracketed token sequence headed by an annotation id of the form or . No space is allowed between the opening parenthesis and this id. Annotations are intended to be used for third-party extensions; they can appear anywhere in a program but are ignored by the WebAssembly semantics itself, which treats them as white space.
Annotations can contain other parenthesized token sequences (including nested annotations), as long as they are well-nested. String literals and comments occurring in an annotation must also be properly nested and closed.
Note
The annotation id is meant to be an identifier categorising the extension, and plays a role similar to the name of a custom section. By convention, annotations corresponding to a custom section should use the custom section’s name as an id.
Implementations are expected to ignore annotations with ids that they do not recognize. On the other hand, they may impose restrictions on annotations that they do recognize, e.g., requiring a specific structure by superimposing a more concrete grammar. It is up to an implementation how it deals with errors in such annotations.
6.3. Values
The grammar productions in this section define lexical syntax, hence no white space is allowed.
6.3.1. Integers
All integers can be written in either decimal or hexadecimal notation. In both cases, digits can optionally be separated by underscores.
The allowed syntax for integer literals depends on size and signedness. Moreover, their value must lie within the range of the respective type.
Uninterpreted integers can be written as either signed or unsigned, and are normalized to unsigned in the abstract syntax.
6.3.2. Floating-Point
Floating-point values can be represented in either decimal or hexadecimal notation.
The value of a literal must not lie outside the representable range of the corresponding [IEEE-754-2019] type (that is, a numeric value must not overflow to ), but it may be rounded to the nearest representable value.
Note
Rounding can be prevented by using hexadecimal notation with no more significant bits than supported by the required type.
Floating-point values may also be written as constants for infinity or canonical NaN (not a number). Furthermore, arbitrary NaN values may be expressed by providing an explicit payload value.
6.3.3. Strings
Strings denote sequences of bytes that can represent both textual and binary data. They are enclosed in quotation marks and may contain any character other than ASCII control characters, quotation marks (), or backslash (), except when expressed with an escape sequence.
Each character in a string literal represents the byte sequence corresponding to its UTF-8 [UNICODE] (Section 2.5) encoding, except for hexadecimal escape sequences , which represent raw bytes of the respective value.
6.3.4. Names
Names are strings denoting a literal character sequence. A name string must form a valid UTF-8 encoding as defined by [UNICODE] (Section 2.5) and is interpreted as a string of Unicode scalar values.
Note
Presuming the source text is itself encoded correctly, strings that do not contain any uses of hexadecimal byte escapes are always valid names.
6.3.5. Identifiers
Indices can be given in both numeric and symbolic form. Symbolic identifiers that stand in lieu of indices start with , followed by eiter a sequence of printable ASCII characters that does not contain a space, quotation mark, comma, semicolon, or bracket, or by a quoted name.
Note
The value of an identifier character is the Unicode codepoint denoting it.
6.3.5.1. Conventions
The expansion rules of some abbreviations require insertion of a fresh identifier. That may be any syntactically valid identifier that does not already occur in the given source text.
6.4. Types
6.4.1. Number Types
6.4.2. Vector Types
6.4.3. Heap Types
6.4.4. Reference Types
6.4.4.1. Abbreviations
There are shorthands for references to abstract heap types.
6.4.5. Value Types
6.4.6. Function Types
Note
The optional identifier names for parameters in a function type only have documentation purpose. They cannot be referenced from anywhere.
6.4.6.1. Abbreviations
Multiple anonymous parameters or results may be combined into a single declaration:
6.4.7. Aggregate Types
6.4.7.1. Abbreviations
Multiple anonymous structure fields may be combined into a single declaration:
6.4.8. Composite Types
6.4.9. Recursive Types
6.4.9.1. Abbreviations
Singular recursive types can omit the keyword:
Similarly, final sub types with no super-types can omit the keyword and arguments:
6.4.10. Address Types
6.4.10.1. Abbreviations
The address type can be omited, in which case it defaults :
6.4.11. Limits
6.4.12. Memory Types
6.4.13. Table Types
6.4.14. Global Types
6.5. Instructions
Instructions are syntactically distinguished into plain and structured instructions.
In addition, as a syntactic abbreviation, instructions can be written as S-expressions in folded form, to group them visually.
6.5.1. Labels
Structured control instructions can be annotated with a symbolic label identifier. They are the only symbolic identifiers that can be bound locally in an instruction sequence. The following grammar handles the corresponding update to the identifier context by composing the context with an additional label entry.
Note
The new label entry is inserted at the beginning of the label list in the identifier context. This effectively shifts all existing labels up by one, mirroring the fact that control instructions are indexed relatively not absolutely.
If a label with the same name already exists, then it is shadowed and the earlier label becomes inaccessible.
6.5.2. Control Instructions
Structured control instructions can bind an optional symbolic label identifier. The same label identifier may optionally be repeated after the corresponding or keywords, to indicate the matching delimiters.
Their block type is given as a type use, analogous to the type of functions. However, the special case of a type use that is syntactically empty or consists of only a single result is not regarded as an abbreviation for an inline function type, but is parsed directly into an optional value type.
Note
The side condition stating that the identifier context must only contain unnamed entries in the rule for block types enforces that no identifier can be bound in any declaration for a block type.
All other control instruction are represented verbatim.
Note
The side condition stating that the identifier context must only contain unnamed entries in the rule for enforces that no identifier can be bound in any declaration appearing in the type annotation.
6.5.2.1. Abbreviations
The keyword of an instruction can be omitted if the following instruction sequence is empty.
Also, for backwards compatibility, the table index to and can be omitted, defaulting to .
6.5.3. Reference Instructions
6.5.4. Parametric Instructions
6.5.5. Variable Instructions
6.5.6. Table Instructions
6.5.6.1. Abbreviations
For backwards compatibility, all table indices may be omitted from table instructions, defaulting to .
6.5.7. Memory Instructions
The offset and alignment immediates to memory instructions are optional. The offset defaults to , the alignment to the storage size of the respective memory access, which is its natural alignment. Lexically, an or phrase is considered a single keyword token, so no white space is allowed around the .
6.5.7.1. Abbreviations
As an abbreviation, the memory index can be omitted in all memory instructions, defaulting to .
6.5.8. Numeric Instructions
6.5.9. Vector Instructions
Vector constant instructions have a mandatory shape descriptor, which determines how the following values are parsed.
6.5.10. Folded Instructions
Instructions can be written as S-expressions by grouping them into folded form. In that notation, an instruction is wrapped in parentheses and optionally includes nested folded instructions to indicate its operands.
In the case of block instructions, the folded form omits the delimiter. For instructions, both branches have to be wrapped into nested S-expressions, headed by the keywords and .
The set of all phrases defined by the following abbreviations recursively forms the auxiliary syntactic class . Such a folded instruction can appear anywhere a regular instruction can.
Note
For example, the instruction sequence
can be folded into
Folded instructions are solely syntactic sugar, no additional syntactic or type-based checking is implied.
6.5.11. Expressions
Expressions are written as instruction sequences. No explicit keyword is included, since they only occur in bracketed positions.
6.6. Modules
6.6.1. Indices
Indices can be given either in raw numeric form or as symbolic identifiers when bound by a respective construct. Such identifiers are looked up in the suitable space of the identifier context .
6.6.2. Type Uses
A type use is a reference to a function type definition. It may optionally be augmented by explicit inlined parameter and result declarations. That allows binding symbolic identifiers to name the local indices of parameters. If inline declarations are given, then their types must match the referenced function type.
Note
If inline declarations are given, their types must be syntactically equal to the types from the indexed definition; possible type substitutions from other definitions that might make them equal are not taken into account. This is to simplify syntactic pre-processing.
The synthesized attribute of a is a pair consisting of both the used type index and the local identifier context containing possible parameter identifiers. The following auxiliary function extracts optional identifiers from parameters:
Note
Both productions overlap for the case that the function type is . However, in that case, they also produce the same results, so that the choice is immaterial.
The well-formedness condition on ensures that the parameters do not contain duplicate identifiers.
6.6.2.1. Abbreviations
A may also be replaced entirely by inline parameter and result declarations. In that case, a type index is automatically inserted:
where is the smallest existing type index whose recursive type definition in the current module is of the form
If no such index exists, then a new recursive type of the same form is inserted at the end of the module.
Abbreviations are expanded in the order they appear, such that previously inserted type definitions are reused by consecutive expansions.
6.6.3. Imports
The descriptors in imports can bind a symbolic function, table, memory, tag, or global identifier.
6.6.3.1. Abbreviations
As an abbreviation, imports may also be specified inline with function, table, memory, global, or tag definitions; see the respective sections.
6.6.4. Functions
Function definitions can bind a symbolic function identifier, and local identifiers for its parameters and locals.
The definition of the local identifier context uses the following auxiliary function to extract optional identifiers from locals:
Note
The well-formedness condition on ensures that parameters and locals do not contain duplicate identifiers.
6.6.4.1. Abbreviations
Multiple anonymous locals may be combined into a single declaration:
Functions can be defined as imports or exports inline:
Note
The latter abbreviation can be applied repeatedly, if “” contains additional export clauses. Consequently, a function declaration can contain any number of exports, possibly followed by an import.
6.6.5. Tables
Table definitions can bind a symbolic table identifier.
6.6.5.1. Abbreviations
A table’s initialization expression can be omitted, in which case it defaults to :
An element segment can be given inline with a table definition, in which case its offset is and the limits of the table type are inferred from the length of the given segment:
Tables can be defined as imports or exports inline:
Note
The latter abbreviation can be applied repeatedly, if “” contains additional export clauses. Consequently, a table declaration can contain any number of exports, possibly followed by an import.
6.6.6. Memories
Memory definitions can bind a symbolic memory identifier.
6.6.6.1. Abbreviations
A data segment can be given inline with a memory definition, in which case its offset is and the limits of the memory type are inferred from the length of the data, rounded up to page size:
Memories can be defined as imports or exports inline:
Note
The latter abbreviation can be applied repeatedly, if “” contains additional export clauses. Consequently, a memory declaration can contain any number of exports, possibly followed by an import.
6.6.7. Globals
Global definitions can bind a symbolic global identifier.
6.6.7.1. Abbreviations
Globals can be defined as imports or exports inline:
Note
The latter abbreviation can be applied repeatedly, if “” contains additional export clauses. Consequently, a global declaration can contain any number of exports, possibly followed by an import.
6.6.9. Exports
The syntax for exports mirrors their abstract syntax directly.
6.6.9.1. Abbreviations
As an abbreviation, exports may also be specified inline with function, table, memory, global, or tag definitions; see the respective sections.
6.6.10. Start Function
A start function is defined in terms of its index.
Note
At most one start function may occur in a module, which is ensured by a suitable side condition on the grammar.
6.6.11. Element Segments
Element segments allow for an optional table index to identify the table to initialize.
6.6.11.1. Abbreviations
As an abbreviation, a single instruction may occur in place of the offset of an active element segment or as an element expression:
Also, the element list may be written as just a sequence of function indices:
A table use can be omitted, defaulting to . Furthermore, for backwards compatibility with earlier versions of WebAssembly, if the table use is omitted, the keyword can be omitted as well.
As another abbreviation, element segments may also be specified inline with table definitions; see the respective section.
6.6.12. Data Segments
Data segments allow for an optional memory index to identify the memory to initialize. The data is written as a string, which may be split up into a possibly empty sequence of individual string literals.
Note
In the current version of WebAssembly, the only valid memory index is 0 or a symbolic memory identifier resolving to the same value.
6.6.12.1. Abbreviations
As an abbreviation, a single instruction may occur in place of the offset of an active data segment:
Also, a memory use can be omitted, defaulting to .
As another abbreviation, data segments may also be specified inline with memory definitions; see the respective section.
6.6.13. Modules
A module consists of a sequence of fields that can occur in any order. All definitions and their respective bound identifiers scope over the entire module, including the text preceding them.
A module may optionally bind an identifier that names the module. The name serves a documentary role only.
Note
Tools may include the module name in the name section of the binary format.
The following restrictions are imposed on the composition of modules: is defined if and only if
Note
The first condition ensures that there is at most one start function. The second condition enforces that all imports must occur before any regular definition of a function, table, memory, global, or tag, thereby maintaining the ordering of the respective index spaces.
The well-formedness condition on in the grammar for ensures that no namespace contains duplicate identifiers.
The definition of the initial identifier context uses the following auxiliary definition which maps each relevant definition to a singular context with one (possibly empty) identifier:
6.6.13.1. Abbreviations
In a source file, the toplevel surrounding the module body may be omitted.
A Appendix
A.1 Embedding
A WebAssembly implementation will typically be embedded into a host environment. An embedder implements the connection between such a host environment and the WebAssembly semantics as defined in the main body of this specification. An embedder is expected to interact with the semantics in well-defined ways.
This section defines a suitable interface to the WebAssembly semantics in the form of entry points through which an embedder can access it. The interface is intended to be complete, in the sense that an embedder does not need to reference other functional parts of the WebAssembly specification directly.
Note
On the other hand, an embedder does not need to provide the host environment with access to all functionality defined in this interface. For example, an implementation may not support parsing of the text format.
Types
In the description of the embedder interface, syntactic classes from the abstract syntax and the runtime’s abstract machine are used as names for variables that range over the possible objects from that class. Hence, these syntactic classes can also be interpreted as types.
For numeric parameters, notation like is used to specify a symbolic name in addition to the respective value range.
Booleans
Interface operation that are predicates return Boolean values:
Exceptions and Errors
Invoking an exported function may throw or propagate exceptions, expressed by an auxiliary syntactic class:
The exception address identifies the exception thrown.
Failure of an interface operation is also indicated by an auxiliary syntactic class:
In addition to the error conditions specified explicitly in this section, such as invalid arguments or exceptions and traps resulting from execution, implementations may also return errors when specific implementation limitations are reached.
Note
Errors are abstract and unspecific with this definition. Implementations can refine it to carry suitable classifications and diagnostic messages.
Pre- and Post-Conditions
Some operations state pre-conditions about their arguments or post-conditions about their results. It is the embedder’s responsibility to meet the pre-conditions. If it does, the post conditions are guaranteed by the semantics.
In addition to pre- and post-conditions explicitly stated with each operation, the specification adopts the following conventions for runtime objects (, , , addresses):
-
Every runtime object passed as a parameter must be valid per an implicit pre-condition.
-
Every runtime object returned as a result is valid per an implicit post-condition.
Note
As long as an embedder treats runtime objects as abstract and only creates and manipulates them through the interface defined here, all implicit pre-conditions are automatically met.
Store
-
Return the empty store.
Modules
-
If there exists a derivation for the byte sequence as a according to the binary grammar for modules, yielding a module , then return .
-
Else, return .
-
If there exists a derivation for the source as a according to the text grammar for modules, yielding a module , then return .
-
Else, return .
-
If is valid, then return nothing.
-
Else, return .
-
Try instantiating in with external values as imports:
If it succeeds with a module instance , then let be .
Else, let be .
-
Return the new store paired with .
Note
The store may be modified even in case of an error.
-
Pre-condition: is valid with the external import types and external export types .
-
Let be the imports .
-
Assert: the length of equals the length of .
-
For each in and corresponding in , do:
Let be the triple .
-
Return the concatenation of all , in index order.
-
Pre-condition: is valid with the external import types and external export types .
-
Let be the exports .
-
Assert: the length of equals the length of .
-
For each in and corresponding in , do:
Let be the pair .
-
Return the concatenation of all , in index order.
Module Instances
-
Assert: due to validity of the module instance , all its export names are different.
-
If there exists an in such that name equals , then:
-
Return the external value .
-
-
Else, return .
Functions
-
Let be the result of allocating a host function in with function type and host function code .
-
Return the new store paired with .
Note
This operation assumes that satisfies the pre- and post-conditions required for a function instance with type .
Regular (non-host) function instances can only be created indirectly through module instantiation.
-
Let be the function type .
-
Return .
-
Post-condition: the returned function type is valid.
-
Return the new store paired with .
Note
The store may be modified even in case of an error.
Tables
-
Let be the result of allocating a table in with table type and initialization value .
-
Return the new store paired with .
-
Return .
-
Post-condition: the returned table type is valid under the empty context.
-
Let be the table instance .
-
If is larger than or equal to the length of , then return .
-
Else, return the reference value .
-
Let be the table instance .
-
If is larger than or equal to the length of , then return .
-
Replace with the reference value .
-
Return the updated store.
-
Return the length of .
-
Try growing the table instance by elements with initialization value :
-
If it succeeds, return the updated store.
-
Else, return .
-
Memories
-
Let be the result of allocating a memory in with memory type .
-
Return the new store paired with .
-
Return .
-
Post-condition: the returned memory type is valid under the empty context.
-
Let be the memory instance .
-
If is larger than or equal to the length of , then return .
-
Else, return the byte .
-
Let be the memory instance .
-
If is larger than or equal to the length of , then return .
-
Replace with .
-
Return the updated store.
-
Return the length of divided by the page size.
-
Try growing the memory instance by pages:
-
If it succeeds, return the updated store.
-
Else, return .
-
Exceptions
-
Pre-condition: is an allocated tag address.
-
Let be the result of allocating an exception instance in with tag address and initialization values .
-
Return the new store paired with .
-
Let be the exception instance .
-
Return the tag address .
-
Let be the exception instance .
-
Return the values .
Globals
-
Let be the result of allocating a global in with global type and initialization value .
-
Return the new store paired with .
-
Return .
-
Post-condition: the returned global type is valid under the empty context.
-
Let be the global instance .
-
Return the value .
-
Let be the global instance .
-
Let be the structure of the global type .
-
If is not , then return .
-
Replace with the value .
-
Return the updated store.
Values
-
Return the reference type with which is valid.
-
Post-condition: the returned reference type is valid under the empty context.
Note
In future versions of WebAssembly, not all references may carry precise type information at run time. In such cases, this function may return a less precise supertype.
-
If is not defined, then return .
-
Else, return the value .
Matching
-
Pre-condition: the value types and are valid under the empty context.
-
If matches , then return .
-
Else, return .
-
Pre-condition: the extern types and are valid under the empty context.
-
If matches , then return .
-
Else, return .
A.2 Profiles
To enable the use of WebAssembly in as many environments as possible, profiles specify coherent language subsets that fit constraints imposed by common classes of host environments. A host platform can thereby decide to support the language only under a restricted profile, or even the intersection of multiple profiles.
Conventions
A profile modification is specified by decorating selected rules in the main body of this specification with a profile annotation that defines them as conditional on the choice of profile.
For that purpose, every profile defines a profile marker, an alphanumeric short-hand like . A profile annotation of the form on a rule indicates that this rule is excluded for either of the profiles whose marker is or .
There are two ways of subsetting the language in a profile:
-
Syntactic, by omitting a feature, in which case certain constructs are removed from the syntax altogether.
-
Semantic, by restricting a feature, in which case certain constructs are still present but some behaviours are ruled out.
Syntax Annotations
To omit a construct from a profile syntactically, respective productions in the grammar of the abstract syntax are annotated with an associated profile marker. This is defined to have the following implications:
-
Any production in the binary or textual syntax that produces abstract syntax with a marked construct is omitted by extension.
-
Any validation or execution rule that handles a marked construct is omitted by extension.
The overall effect is that the respective construct is no longer part of the language under a respective profile.
Note
For example, a “busy” profile marked could rule out the instruction by marking the production for it in the abstract syntax as follows:
A rule may be annotated by multiple markers, which could be the case if a construct is in the intersection of multiple features.
Semantics Annotations
To restrict certain behaviours in a profile, individual validation or reduction rules or auxiliary definitions are annotated with an associated marker.
This has the consequence that the respective rule is no longer applicable under the given profile.
Note
For example, an “infinite” profile marked could define that growing memory never fails:
Properties
All profiles are defined such that the following properties are preserved:
-
All profiles represent syntactic and semantic subsets of the full profile, i.e., they do not add syntax or alter behaviour.
-
All profiles are mutually compatible, i.e., no two profiles subset semantic behaviour in inconsistent or ambiguous ways, and any intersection of profiles preserves the properties described here.
-
Profiles do not violate soundness, i.e., all configurations valid under that profile still have well-defined execution behaviour.
Note
Tools are generally expected to handle and produce code for the full profile by default. In particular, producers should not generate code that depends on specific profiles. Instead, all code should preserve correctness when executed under the full profile.
Moreover, profiles should be considered static and fixed for a given platform or ecosystem. Runtime conditioning on the “current” profile is not intended and should be avoided.
Defined Profiles
Note
The number of defined profiles is expected to remain small in the future. Profiles are intended for broad and permanent use cases only. In particular, profiles are not intended for language versioning.
Full Profile ()
The full profile contains the complete language and all possible behaviours. It imposes no restrictions, i.e., all rules and definitions are active. All other profiles define sub-languages of this profile.
Deterministic Profile ()
The deterministic profile excludes all rules marked . It defines a sub-language that does not exhibit any incidental non-deterministic behaviour:
-
All NaN values generated by floating-point instructions are canonical and positive.
-
All relaxed vector instructions have a fixed behaviour that does not depend on the implementation.
Even under this profile, the and instructions technically remain non-deterministic, in order to be able to indicate resource exhaustion.
Note
In future versions of WebAssembly, new non-deterministic behaviour may be added to the language, such that the deterministic profile will induce additional restrictions.
A.3 Implementation Limitations
Implementations typically impose additional restrictions on a number of aspects of a WebAssembly module or execution. These may stem from:
-
physical resource limits,
-
constraints imposed by the embedder or its environment,
-
limitations of selected implementation strategies.
This section lists allowed limitations. Where restrictions take the form of numeric limits, no minimum requirements are given, nor are the limits assumed to be concrete, fixed numbers. However, it is expected that all implementations have “reasonably” large limits to enable common applications.
Note
A conforming implementation is not allowed to leave out individual features. However, designated subsets of WebAssembly may be specified in the future.
Syntactic Limits
Structure
An implementation may impose restrictions on the following dimensions of a module:
-
the number of element segments in a module
-
the number of data segments in a module
-
the number of sub types in a recursive type
-
the subtyping depth of a sub type
-
the number of fields in a structure type
-
the number of parameters in a function type
-
the number of results in a function type
-
the number of parameters in a block type
-
the number of results in a block type
-
the number of instructions in a function body
-
the number of instructions in a structured control instruction
-
the number of structured control instructions in a function
-
the nesting depth of structured control instructions
-
the number of label indices in a instruction
-
the number of instructions in a constant expression
-
the length of the array in a instruction
-
the length of an element segment
-
the length of a data segment
-
the length of a name
-
the range of characters in a name
If the limits of an implementation are exceeded for a given module, then the implementation may reject the validation, compilation, or instantiation of that module with an embedder-specific error.
Binary Format
For a module given in binary format, additional limitations may be imposed on the following dimensions:
-
the size of a module
-
the size of any section
-
the size of a structured control instruction
-
the size of an individual constant expression’s instruction sequence
-
the number of sections
Text Format
For a module given in text format, additional limitations may be imposed on the following dimensions:
-
the size of the source text
-
the size of any syntactic element
-
the size of an individual token
-
the nesting depth of folded instructions
-
the length of symbolic identifiers
-
the range of literal characters allowed in the source text
Validation
An implementation may defer validation of individual functions until they are first invoked.
If a function turns out to be invalid, then the invocation, and every consecutive call to the same function, results in a trap.
Note
This is to allow implementations to use interpretation or just-in-time compilation for functions. The function must still be fully validated before execution of its body begins.
Execution
Restrictions on the following dimensions may be imposed during execution of a WebAssembly program:
-
the number of allocated module instances
-
the number of allocated function instances
-
the number of allocated table instances
-
the number of allocated memory instances
-
the number of allocated global instances
-
the number of allocated tag instances
-
the number of allocated structure instances
-
the number of allocated array instances
-
the number of allocated exception instances
-
the size of a table instance
-
the size of a memory instance
-
the size of an array instance
If the runtime limits of an implementation are exceeded during execution of a computation, then it may terminate that computation and report an embedder-specific error to the invoking code.
Some of the above limits may already be verified during instantiation, in which case an implementation may report exceedance in the same manner as for syntactic limits.
Note
Concrete limits are usually not fixed but may be dependent on specifics, interdependent, vary over time, or depend on other implementation- or embedder-specific situations or events.
Type Soundness
The type system of WebAssembly is sound, implying both type safety and memory safety with respect to the WebAssembly semantics. For example:
-
All types declared and derived during validation are respected at run time; e.g., every local or global variable will only contain type-correct values, every instruction will only be applied to operands of the expected type, and every function invocation always evaluates to a result of the right type (if it does not diverge, throw an exception, or trap).
-
No memory location will be read or written except those explicitly defined by the program, i.e., as a local, a global, an element in a table, or a location within a linear memory.
-
There is no undefined behavior, i.e., the execution rules cover all possible cases that can occur in a valid program, and the rules are mutually consistent.
Soundness also is instrumental in ensuring additional properties, most notably, encapsulation of function and module scopes: no locals can be accessed outside their own function and no module components can be accessed outside their own module unless they are explicitly exported or imported.
The typing rules defining WebAssembly validation only cover the static components of a WebAssembly program. In order to state and prove soundness precisely, the typing rules must be extended to the dynamic components of the abstract runtime, that is, the store, configurations, and administrative instructions. [1]
Contexts
In order to check rolled up recursive types, the context is locally extended with an additional component that records the sub type corresponding to each recursive type index within the current recursive type:
Types
Well-formedness for extended type forms is defined as follows.
Heap Type
-
The heap type is valid.
Heap Type
-
The recursive type index must exist in .
-
Then the heap type is valid.
Value Type
-
The value type is valid.
Recursive Types
-
Let be the current context , but where is .
-
There must be a type index , such that for each sub type in :
-
Under the context , the sub type must be valid for type index and recursive type index .
-
-
Then the recursive type is valid for the type index .
Note
These rules are a generalisation of the ones previously given.
Sub types
-
The composite type must be valid.
-
The sequence may be no longer than .
-
For every heap type in :
-
The heap type must be ordered before a type index and recursive type index a , meaning:
-
Either is a defined type.
-
Or is a type index that is smaller than .
-
Or is a recursive type index where is smaller than .
-
-
Let sub type be the unrolling of the heap type , meaning:
-
Either is a defined type , then must be the unrolling of .
-
Or is a type index , then must be the unrolling of the defined type .
-
Or is a recursive type index , then must be .
-
-
The sub type must not contain .
-
Let be the composite type in .
-
The composite type must match .
-
-
Then the sub type is valid for the type index and recursive type index .
where:
Note
This rule is a generalisation of the ones previously given, which only allowed type indices as supertypes.
Subtyping
In a rolled-up recursive type, a recursive type indices matches another heap type if:
-
Let be the sub type .
-
The heap type is contained in .
Note
This rule is only invoked when checking validity of rolled-up recursive types.
Results
Results can be classified by result types as follows.
Results
-
For each value in :
-
The value is valid with some value type .
-
-
Let be the concatenation of all .
-
Then the result is valid with result type .
Results
-
The value must be valid.
-
Then the result is valid with result type , for any sequence of value types.
Results
-
The result is valid with result type , for any valid closed result types.
Store Validity
The following typing rules specify when a runtime store is valid. A valid store must consist of function, table, memory, global, tag, element, data, structure, array, exception, and module instances that are themselves valid, relative to .
To that end, each kind of instance is classified by a respective function, table, memory, global, tag, element, or data type, or just in the case of structures, arrays, or exceptions. Module instances are classified by module contexts, which are regular contexts repurposed as module types describing the index spaces defined by a module.
Store
-
Each function instance in must be valid with some function type .
-
Each table instance in must be valid with some table type .
-
Each memory instance in must be valid with some memory type .
-
Each global instance in must be valid with some global type .
-
Each tag instance in must be valid with some tag type .
-
Each element instance in must be valid with some reference type .
-
Each data instance in must be valid.
-
Each structure instance in must be valid.
-
Each array instance in must be valid.
-
Each exception instance in must be valid.
-
No reference to a bound structure address must be reachable from itself through a path consisting only of indirections through immutable structure, or array fields or fields of exception instances.
-
No reference to a bound array address must be reachable from itself through a path consisting only of indirections through immutable structure or array fields or fields of exception instances.
-
No reference to a bound exception address must be reachable from itself through a path consisting only of indirections through immutable structure or array fields or fields of exception instances.
-
Then the store is valid.
where denotes the transitive closure of the following immutable reachability relation on values:
Note
The constraint on reachability through immutable fields prevents the presence of cyclic data structures that can not be constructed in the language. Cycles can only be formed using mutation.
Function Instances
-
The function type must be valid under an empty context.
-
The module instance must be valid with some context .
-
Under context :
-
The function must be valid with some function type .
-
The function type must match .
-
-
Then the function instance is valid with function type .
Host Function Instances
-
The function type must be valid under an empty context.
-
Let be the function type .
-
For every valid store extending and every sequence of values whose types coincide with :
-
Then the function instance is valid with function type .
Note
This rule states that, if appropriate pre-conditions about store and arguments are satisfied, then executing the host function must satisfy appropriate post-conditions about store and results. The post-conditions match the ones in the execution rule for invoking host functions.
Any store under which the function is invoked is assumed to be an extension of the current store. That way, the function itself is able to make sufficient assumptions about future stores.
Table Instances
-
The table type must be valid under the empty context.
-
The length of must equal .
-
For each reference in the table’s elements :
-
The reference must be valid with some reference type .
-
The reference type must match the reference type .
-
-
Then the table instance is valid with table type .
Memory Instances
-
The memory type must be valid under the empty context.
-
The length of must equal multiplied by the page size .
-
Then the memory instance is valid with memory type .
Global Instances
-
The global type must be valid under the empty context.
-
The value must be valid with some value type .
-
The value type must match the value type .
-
Then the global instance is valid with global type .
Tag Instances
Element Instances
-
The reference type must be valid under the empty context.
-
For each reference in the elements :
-
The reference must be valid with some reference type .
-
The reference type must match the reference type .
-
-
Then the element instance is valid with reference type .
Data Instances
-
The data instance is valid.
Structure Instances
-
The defined type must be valid under the empty context.
-
The expansion of must be a structure type .
-
The length of the sequence of field values must be the same as the length of the sequence of field types .
-
For each field value in and corresponding field type in :
-
Let be .
-
The field value must be valid with storage type .
-
-
Then the structure instance is valid.
Array Instances
-
The defined type must be valid under the empty context.
-
The expansion of must be an array type .
-
Let be .
-
For each field value in :
-
The field value must be valid with storage type .
-
-
Then the array instance is valid.
Field Values
-
If is a value , then:
-
The value must be valid with value type .
-
Then the field value is valid with value type .
-
-
Else, is a packed value :
-
Let be the field value .
-
Then the field value is valid with packed type .
-
Exception Instances
-
The store entry must exist.
-
Let be the tag type .
-
The result type must be empty.
-
The sequence of values must have the same length as the sequence of value types.
-
For each value in and corresponding value type in , the value must be valid with type .
-
Then the exception instance is valid.
Export Instances
-
The external value must be valid with some external type .
-
Then the export instance is valid.
Module Instances
-
Each defined type in must be valid under the empty context.
-
For each function address in , the external value must be valid with some external type .
-
For each table address in , the external value must be valid with some external type .
-
For each memory address in , the external value must be valid with some external type .
-
For each global address in , the external value must be valid with some external type .
-
For each tag address in , the external value must be valid with some external type .
-
For each element address in , the element instance must be valid with some reference type .
-
For each data address in , the data instance must be valid.
-
Each export instance in must be valid.
-
For each export instance in , the name must be different from any other name occurring in .
-
Let be the concatenation of all in order.
-
Let be the concatenation of all in order.
-
Let be the concatenation of all in order.
-
Let be the concatenation of all in order.
-
Let be the concatenation of all in order.
-
Let be the concatenation of all in order.
-
Let be the concatenation of all in order.
-
Let be the length of .
-
Let be the length of .
-
Let be the sequence of function indices from to .
-
Then the module instance is valid with context CTAGS~tagtype^ast, .
Configuration Validity
To relate the WebAssembly type system to its execution semantics, the typing rules for instructions must be extended to configurations , which relates the store to execution threads.
Configurations and threads are classified by their result type. In addition to the store , threads are typed under a return type , which controls whether and with which type a instruction is allowed. This type is absent () except for instruction sequences inside an administrative instruction.
Finally, frames are classified with frame contexts, which extend the module contexts of a frame’s associated module instance with the locals that the frame contains.
Configurations
-
Under no allowed return type, the thread must be valid with some result type .
-
Then the configuration is valid with the result type .
Threads
-
Let be the current allowed return type.
-
Let be the same context as , but with set to .
-
Under context , the instruction sequence must be valid with some type .
-
Then the thread is valid with the result type .
Frames
-
The module instance must be valid with some module context .
-
Each value in must be valid with some value type .
-
Let be the concatenation of all in order.
-
Let be the same context as , but with the value types prepended to the vector.
-
Then the frame is valid with frame context .
Administrative Instructions
Typing rules for administrative instructions are specified as follows. In addition to the context , typing of these instructions is defined under a given store .
To that end, all previous typing judgements are generalized to include the store, as in , by implicitly adding to all rules – is never modified by the pre-existing rules, but it is accessed in the extra rules for administrative instructions given below.
-
The instruction is valid with any valid instruction type of the form .
-
The value must be valid with value type .
-
Then it is valid as an instruction with type .
-
The external function value must be valid with external function type .
-
Let be the function type .
-
Then the instruction is valid with type .
-
The instruction sequence must be valid with some type .
-
Let be the same context as , but with the result type prepended to the vector.
-
Under context , the instruction sequence must be valid with type .
-
Then the compound instruction is valid with type .
-
For every catch clause in , must be valid.
-
The instruction sequence must be valid with some type .
-
Then the compound instruction is valid with type .
-
Under the valid return type , the thread must be valid with result type .
-
Then the compound instruction is valid with type .
Store Extension
Programs can mutate the store and its contained instances. Any such modification must respect certain invariants, such as not removing allocated instances or changing immutable definitions. While these invariants are inherent to the execution semantics of WebAssembly instructions and modules, host functions do not automatically adhere to them. Consequently, the required invariants must be stated as explicit constraints on the invocation of host functions. Soundness only holds when the embedder ensures these constraints.
The necessary constraints are codified by the notion of store extension: a store state extends state , written , when the following rules hold.
Note
Extension does not imply that the new store is valid, which is defined separately above.
Store
-
The length of must not shrink.
-
The length of must not shrink.
-
The length of must not shrink.
-
The length of must not shrink.
-
The length of must not shrink.
-
The length of must not shrink.
-
The length of must not shrink.
-
The length of must not shrink.
-
The length of must not shrink.
-
The length of must not shrink.
-
For each function instance in the original , the new function instance must be an extension of the old.
-
For each table instance in the original , the new table instance must be an extension of the old.
-
For each memory instance in the original , the new memory instance must be an extension of the old.
-
For each global instance in the original , the new global instance must be an extension of the old.
-
For each tag instance in the original , the new tag instance must be an extension of the old.
-
For each element instance in the original , the new element instance must be an extension of the old.
-
For each data instance in the original , the new data instance must be an extension of the old.
-
For each structure instance in the original , the new structure instance must be an extension of the old.
-
For each array instance in the original , the new array instance must be an extension of the old.
-
For each exception instance in the original , the new exception instance must be an extension of the old.
Function Instance
-
A function instance must remain unchanged.
Table Instance
-
The table type must remain unchanged.
-
The length of must not shrink.
Memory Instance
-
The memory type must remain unchanged.
-
The length of must not shrink.
Global Instance
-
The global type must remain unchanged.
-
Let be the structure of .
-
If is , then the value must remain unchanged.
Tag Instance
-
A tag instance must remain unchanged.
Element Instance
-
The reference type must remain unchanged.
-
The vector must:
-
either remain unchanged,
-
or shrink to length .
-
Data Instance
-
The vector must:
-
either remain unchanged,
-
or shrink to length .
-
Structure Instance
-
The defined type must remain unchanged.
-
Assert: due to store well-formedness, the expansion of is a structure type.
-
Let be the expansion of .
-
The length of the vector must remain unchanged.
-
Assert: due to store well-formedness, the length of is the same as the length of .
-
For each field value in and corresponding field type in :
-
Let be the structure of .
-
If is , then the field value must remain unchanged.
-
Array Instance
-
The defined type must remain unchanged.
-
Assert: due to store well-formedness, the expansion of is an array type.
-
Let be the expansion of .
-
The length of the vector must remain unchanged.
-
Let be the structure of .
-
If is , then the sequence of field values must remain unchanged.
Exception Instance
-
An exception instance must remain unchanged.
Theorems
Given the definition of valid configurations, the standard soundness theorems hold. [2] [3]
Theorem (Preservation). If a configuration is valid with result type (i.e., ), and steps to (i.e., ), then is a valid configuration with the same result type (i.e., ). Furthermore, is an extension of (i.e., ).
A terminal thread is one whose sequence of instructions is a result. A terminal configuration is a configuration whose thread is terminal.
Theorem (Progress). If a configuration is valid (i.e., for some result type ), then either it is terminal, or it can step to some configuration (i.e., ).
From Preservation and Progress the soundness of the WebAssembly type system follows directly.
Corollary (Soundness). If a configuration is valid (i.e., for some result type ), then it either diverges or takes a finite number of steps to reach a terminal configuration (i.e., ) that is valid with the same result type (i.e., ) and where is an extension of (i.e., ).
In other words, every thread in a valid configuration either runs forever, traps, throws an exception, or terminates with a result that has the expected type. Consequently, given a valid store, no computation defined by instantiation or invocation of a valid module can “crash” or otherwise (mis)behave in ways not covered by the execution semantics given in this specification.
The formalization and theorems are derived from the following article: Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. Bringing the Web up to Speed with WebAssembly. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017.
A machine-verified version of the formalization and soundness proof of the PLDI 2017 paper is described in the following article: Conrad Watt. Mechanising and Verifying the WebAssembly Specification. Proceedings of the 7th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2018). ACM 2018.
Machine-verified formalizations and soundness proofs of the semantics from the official specification are described in the following article: Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner. Two Mechanisations of WebAssembly 1.0. Proceedings of the 24th International Symposium on Formal Methods (FM 2021). Springer 2021.
Type System Properties
Principal Types
The type system of WebAssembly features both subtyping and simple forms of polymorphism for instruction types. That has the effect that every instruction or instruction sequence can be classified with multiple different instruction types.
However, the typing rules still allow deriving principal types for instruction sequences. That is, every valid instruction sequence has one particular type scheme, possibly containing some unconstrained place holder type variables, that is a subtype of all its valid instruction types, after substituting its type variables with suitable specific types.
Moreover, when deriving an instruction type in a “forward” manner, i.e., the input of the instruction sequence is already fixed to specific types, then it has a principal output type expressible without type variables, up to a possibly polymorphic stack bottom representable with one single variable. In other words, “forward” principal types are effectively closed.
Note
For example, in isolation, the instruction has the type for any choice of valid heap type . Moreover, if the input type is already determined, i.e., a specific is given, then the output type is fully determined as well.
The implication of the latter property is that a validator for complete instruction sequences (as they occur in valid modules) can be implemented with a simple left-to-right algorithm that does not require the introduction of type variables.
A typing algorithm capable of handling partial instruction sequences (as might be considered for program analysis or program manipulation) needs to introduce type variables and perform substitutions, but it does not need to perform backtracking or record any non-syntactic constraints on these type variables.
Technically, the syntax of heap, value, and result types can be enriched with type variables as follows:
where each ranges over a set of type variables for syntactic class , respectively. The special class is defined as , and is only needed to handle unannotated instructions.
A type is closed when it does not contain any type variables, and open otherwise. A type substitution is a finite mapping from type variables to closed types of the respective syntactic class. When applied to an open type, it replaces the type variables from its domain with the respective .
Theorem (Principal Types). If an instruction sequence is valid with some closed instruction type (i.e., ), then it is also valid with a possibly open instruction type (i.e., ), such that for every closed type with which is valid (i.e., for all ), there exists a substitution , such that is a subtype of (i.e., ). Furthermore, is unique up to the choice of type variables.
Theorem (Closed Principal Forward Types). If closed input type is given and the instruction sequence is valid with instruction type (i.e., ), then it is also valid with instruction type (i.e., ), where all are closed, such that for every closed result type with which is valid (i.e., for all ), there exists a substitution , such that .
Type Lattice
The Principal Types property depends on the existence of a greatest lower bound for any pair of types.
Theorem (Greatest Lower Bounds for Value Types). For any two value types and that are valid (i.e., and ), there exists a valid value type that is a subtype of both and (i.e., and and ), such that every valid value type that also is a subtype of both and (i.e., for all and and ), is a subtype of (i.e., ).
Note
The greatest lower bound of two types may be .
Theorem (Conditional Least Upper Bounds for Value Types). Any two value types and that are valid (i.e., and ) either have no common supertype, or there exists a valid value type that is a supertype of both and (i.e., and and ), such that every valid value type that also is a supertype of both and (i.e., for all and and ), is a supertype of (i.e., ).
Note
If a top type was added to the type system, a least upper bound would exist for any two types.
Corollary (Type Lattice). Assuming the addition of a provisional top type, value types form a lattice with respect to their subtype relation.
Finally, value types can be partitioned into multiple disjoint hierarchies that are not related by subtyping, except through .
Theorem (Disjoint Subtype Hierarchies). The greatest lower bound of two value types is or if and only if they do not have a least upper bound.
In other words, types that do not have common supertypes, do not have common subtypes either (other than or ), and vice versa.
Note
Types from disjoint hierarchies can safely be represented in mutually incompatible ways in an implementation, because their values can never flow to the same place.
Compositionality
Valid instruction sequences can be freely composed, as long as their types match up.
Theorem (Composition). If two instruction sequences and are valid with types and , respectively (i.e., and ), then the concatenated instruction sequence is valid with type (i.e., ).
Note
More generally, instead of a shared type , it suffices if the output type of is a subtype of the input type of , since the subtype can always be weakened to its supertype by subsumption.
Inversely, valid instruction sequences can also freely be decomposed, that is, splitting them anywhere produces two instruction sequences that are both valid.
Theorem (Decomposition). If an instruction sequence that is valid with type (i.e., ) is split into two instruction sequences and at any point (i.e., ), then these are separately valid with some types and , respectively (i.e., and ), where .
Note
This property holds because validation is required even for unreachable code. Without that, might not be valid in isolation.
A.4 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 | F64type vec_type = V128
type heap_type =
Any | Eq | I31 | Struct | Array | None |
Func | Nofunc | Exn | Noexn | 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 | I16type 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_stackvar 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 .
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]))
case (throw x)
pop_vals(tags[x].type.params)
unreachable()
case (try_table t1*->t2* handler*)
pop_vals([t1*])
foreach (handler in handler*)
error_if(ctrls.size() < handler.label)
push_ctrl(catch, [], label_types(ctrls[handler.label]))
switch (handler.clause)
case (catch x)
push_vals(tags[x].type.params)
case (catch_ref x)
push_vals(tags[x].type.params)
push_val(Exnref)
case (catch_all)
skip
case (catch_all_ref)
push_val(Exnref)
pop_ctrl()
push_ctrl(try_table, [t1*], [t2*])
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.
Custom Sections and Annotations
This appendix defines dedicated custom sections for WebAssembly’s binary format and annotations for the text format. Such sections or annotations do not contribute to, or otherwise affect, the WebAssembly semantics, and may be ignored by an implementation. However, they provide useful meta data that implementations can make use of to improve user experience or take compilation hints.
Name Section
The name section is a custom section whose name string is itself . The name section should appear only once in a module, and only after the data section.
The purpose of this section is to attach printable names to definitions in a module, which e.g. can be used by a debugger or when parts of the module are to be rendered in text form.
Subsections
The data of a name section consists of a sequence of subsections. Each subsection consists of a
-
a one-byte subsection id,
-
the size of the contents, in bytes,
-
the actual contents, whose structure is dependent on the subsection id.
The following subsection ids are used:
Id |
Subsection |
---|---|
0 | |
1 | |
2 | |
4 | |
10 | |
11 |
Each subsection may occur at most once, and in order of increasing id.
Name Maps
A name map assigns names to indices in a given index space. It consists of a vector of index/name pairs in order of increasing index value. Each index must be unique, but the assigned names need not be.
An indirect name map assigns names to a two-dimensional index space, where secondary indices are grouped by primary indices. It consists of a vector of primary index/name map pairs in order of increasing index value, where each name map in turn maps secondary indices to names. Each primary index must be unique, and likewise each secondary index per individual name map.
Module Names
The module name subsection has the id 0. It simply consists of a single name that is assigned to the module itself.
Function Names
The function name subsection has the id 1. It consists of a name map assigning function names to function indices.
Local Names
The local name subsection has the id 2. It consists of an indirect name map assigning local names to local indices grouped by function indices.
Type Names
The type name subsection has the id 4. It consists of a name map assigning type names to type indices.
Field Names
The field name subsection has the id 10. It consists of an indirect name map assigning field names to field indices grouped by the type indices of their respective structure types.
Tag Names
The tag name subsection has the id 11. It consists of a name map assigning tag names to tag indices.
Name Annotations
Name annotations are the textual analogue to the name section and provide a textual representation for it. Consequently, their id is .
Analogous to the name section, name annotations are allowed on modules, functions, and locals (including parameters). They can be placed where the text format allows binding occurrences of respective identifiers. If both an identifier and a name annotation are given, the annotation is expected after the identifier. In that case, the annotation takes precedence over the identifier as a textual representation of the binding’s name. At most one name annotation may be given per binding.
All name annotations have the following format:
Note
All name annotations can be arbitrary UTF-8 strings. Names need not be unique.
Module Names
A module name annotation must be placed on a module definition, directly after the keyword, or if present, after the following module identifier.
Function Names
A function name annotation must be placed on a function definition or function import, directly after the keyword, or if present, after the following function identifier or.
Parameter Names
A parameter name annotation must be placed on a parameter declaration, directly after the keyword, or if present, after the following parameter identifier. It may only be placed on a declaration that declares exactly one parameter.
Local Names
A local name annotation must be placed on a local declaration, directly after the keyword, or if present, after the following local identifier. It may only be placed on a declaration that declares exactly one local.
Type Names
A type name annotation must be placed on a type declaration, directly after the keyword, or if present, after the following type identifier.
Field Names
A field name annotation must be placed on the field of a structure type, directly after the keyword, or if present, after the following field identifier. It may only be placed on a declaration that declares exactly one field.
Tag Names
A tag name annotation must be placed on a tag declaration or tag import, directly after the keyword, or if present, after the following tag identifier.
Custom Annotations
Custom annotations are a generic textual representation for any custom section. Their id is . By generating custom annotations, tools converting between binary format and text format can maintain and round-trip the content of custom sections even when they do not recognize them.
Custom annotations must be placed inside a module definition. They must occur anywhere after the keyword, or if present, after the following module identifier. They must not be nested into other constructs.
The first string in a custom annotation denotes the name of the custom section it represents. The remaining strings collectively represent the section’s payload data, written as a data string, which can be split up into a possibly empty sequence of individual string literals (similar to data segments).
An arbitrary number of custom annotations (even of the same name) may occur in a module, each defining a separate custom section when converting to binary format. Placement of the sections in the binary can be customized via explicit placement directives, that position them either directly before or directly after a known section. That section must exist and be non-empty in the binary encoding of the annotated module. The placements and denote virtual sections before the first and after the last known section, respectively. When the placement directive is omitted, it defaults to .
If multiple placement directives appear for the same position, then the sections are all placed there, in order of their appearance in the text. For this purpose, the position a section is considered different from the position the consecutive section, and the former occurs before the latter.
Note
Future versions of WebAssembly may introduce additional sections between others or at the beginning or end of a module. Using and guarantees that placement will still go before or after any future section, respectively.
If a custom section with a specific section id is given as well as annotations representing the same custom section (e.g., annotations as well as a annotation for a section), then two sections are assumed to be created. Their relative placement will depend on the placement directive given for the annotation as well as the implicit placement requirements of the custom section, which are applied to the other annotation.
Note
For example, the following module,
(module (@custom "A" "aaa")
(type $t (func))
(@custom "B" (after func) "bbb")
(@custom "C" (before func) "ccc")
(@custom "D" (after last) "ddd")
(table 10 funcref)
(func (type $t))
(@custom "E" (after import) "eee")
(@custom "F" (before type) "fff")
(@custom "G" (after data) "ggg")
(@custom "H" (after code) "hhh")
(@custom "I" (after func) "iii")
(@custom "J" (before func) "jjj")
(@custom "K" (before first) "kkk")
)
will result in the following section ordering:
custom section "K"custom section "F"
type section
custom section "E"
custom section "C"
custom section "J"
function section
custom section "B"
custom section "I"
table section
code section
custom section "H"
custom section "G"
custom section "A"
custom section "D"
Change History
Since the original release 1.0 of the WebAssembly specification, a number of proposals for extensions have been integrated. The following sections provide an overview of what has changed.
Release 2.0
Sign Extension Instructions
Added new numeric instructions for performing sign extension within integer representations. [1]
-
New numeric instructions:
-
Non-trapping Float-to-Int Conversions
Added new conversion instructions that avoid trapping when converting a floating-point number to an integer. [2]
-
New numeric instructions:
-
Multiple Values
Generalized the result type of blocks and functions to allow for multiple values; in addition, introduced the ability to have block parameters. [3]
-
Function types allow more than one result
-
Block types can be arbitrary function types
Reference Types
Added and as new value types and respective instructions. [4]
-
New reference value types:
-
-
-
-
Extended parametric instruction:
-
with optional type immediate
-
-
New declarative form of element segment
Table Instructions
Added instructions to directly access and modify tables. [4]
-
Table types allow any reference type as element type
-
New table instructions:
-
Multiple Tables
Added the ability to use multiple tables per module. [4]
-
Modules may
-
Table instructions take a table index immediate:
-
-
Element segments take a table index
Bulk Memory and Table Instructions
Added instructions that modify ranges of memory or table entries. [4] [5]
-
New memory instructions:
-
-
New table instructions:
-
-
New passive form of data segment
-
New passive form of element segment
-
New data count section in binary format
-
Active data and element segments boundaries are no longer checked at compile time but may trap instead
Vector Instructions
Added vector type and instructions that manipulate multiple numeric values in parallel (also known as SIMD, single instruction multiple data) [6]
-
New value type:
-
-
New memory instructions:
-
-
New constant vector instruction:
-
-
New unary vector instructions:
-
-
New binary vector instructions:
-
-
New ternary vector instruction:
-
-
New test vector instructions:
-
-
New relational vector instructions:
-
-
New conversion vector instructions:
-
-
New lane access vector instructions:
-
-
New lane splitting/combining vector instructions:
-
-
New byte reordering vector instructions:
-
-
New injection/projection vector instructions:
-
https://github.com/WebAssembly/spec/tree/main/proposals/sign-extension-ops/
https://github.com/WebAssembly/spec/tree/main/proposals/nontrapping-float-to-int-conversion/
https://github.com/WebAssembly/spec/tree/main/proposals/multi-value/
https://github.com/WebAssembly/spec/tree/main/proposals/reference-types/
https://github.com/WebAssembly/spec/tree/main/proposals/bulk-memory-operations/
https://github.com/WebAssembly/spec/tree/main/proposals/simd/
Release 3.0
Extended Constant Expressions
Allowed basic numeric computations in constant expressions. [7]
-
Extended set of constant instructions with:
-
-
-
-
for any previously declared immutable global
-
Note
The garbage collection added further constant instructions.
Tail Calls
Added instructions to perform tail calls. [8]
-
New control instructions:
-
Exception Handling
Added tag definitions, imports, and exports, and instructions to throw and catch exceptions [9]
-
Modules may
-
New heap types:
-
-
New reference type short-hands:
-
-
New control instructions:
-
-
New tag section in binary format.
Multiple Memories
Added the ability to use multiple memories per module. [10]
-
Modules may
-
Memory instructions take a memory index immediate:
-
-
Data segments take a memory index
64-bit Address Space
Added the ability to declare an address type for tables and memories. [11]
-
Address types denote a subset of the integral number types
-
Table types include an address type
-
Memory types include an address type
-
Operand types of table and memory instructions now depend on the subject’s declared address type:
-
Typeful References
Added more precise types for references. [12]
-
New generalised form of reference types:
-
-
New class of heap types:
-
-
-
-
New control instruction:
-
-
Refined typing of reference instruction:
-
with more precise result type
-
-
Refined typing of local instructions and instruction sequences to track the initialization status of locals with non-defaultable type
-
Extended table definitions with optional initializer expression
Garbage Collection
Added managed reference types. [13]
-
New forms of heap types:
-
-
New reference type short-hands:
-
-
New forms of type definitions:
-
Enriched subtyping based on explicitly declared sub types and the new heap types
-
New generic reference instructions:
-
-
New reference instructions for unboxed scalars:
-
-
New reference instructions for structure types:
-
-
New reference instructions for array types:
-
-
New reference instructions for converting external types:
-
-
Extended set of constant instructions with:
-
Relaxed Vector Instructions
Added new relaxed vector instructions, whose behaviour is non-deterministic and implementation-dependent. [14]
-
New binary vector instruction:
-
-
New ternary vector instruction:
-
-
New conversion vector instructions:
-
-
New byte reordering vector instruction:
-
Profiles
Introduced the concept of profile for specifying language subsets.
-
A new profile defining a deterministic mode of execution.
Custom Annotations
Added generic syntax for custom annotations in the text format, mirroring the role of custom sections in the binary format. [15]
-
Annotations of the form are allowed anywhere in the text format
-
Identifiers can be escaped as with arbitrary names
-
Defined name annotations for:
-
Defined custom annotation to represent arbitrary custom sections in the text format
https://github.com/WebAssembly/spec/blob/main/proposals/extended-const/
https://github.com/WebAssembly/spec/tree/main/proposals/tail-call/
https://github.com/WebAssembly/spec/tree/main/proposals/exception-handling/
https://github.com/WebAssembly/spec/blob/main/proposals/multi-memory/
https://github.com/WebAssembly/spec/blob/main/proposals/memory64/
https://github.com/WebAssembly/spec/tree/main/proposals/function-references/
https://github.com/WebAssembly/spec/tree/main/proposals/relaxed-simd/
https://github.com/WebAssembly/annotations/tree/main/proposals/annotations/
A.8 Index of Types
Category |
Constructor |
Binary Opcode |
---|---|---|
|
(positive number as or ) | |
|
(-1 as ) | |
|
(-2 as ) | |
|
(-3 as ) | |
|
(-4 as ) | |
|
(-5 as ) | |
(reserved) |
.. | |
|
(-8 as ) | |
|
(-9 as ) | |
(reserved) |
.. | |
|
(-14 as ) | |
|
(-13 as ) | |
|
(-14 as ) | |
|
(-15 as ) | |
|
(-16 as ) | |
|
(-17 as ) | |
|
(-18 as ) | |
|
(-19 as ) | |
|
(-20 as ) | |
|
(-21 as ) | |
|
(-22 as ) | |
|
(-23 as ) | |
(reserved) |
.. | |
|
(-28 as ) | |
|
(-29 as ) | |
(reserved) |
.. | |
|
(-32 as ) | |
|
(-33 as ) | |
|
(-34 as ) | |
(reserved) |
.. | |
|
(-48 as ) | |
|
(-49 as ) | |
|
(-50 as ) | |
(reserved) |
.. | |
|
(-64 as ) | |
|
(none) | |
|
(none) | |
|
(none) | |
|
(none) |
A.9 Index of Instructions
Instruction |
Binary Opcode |
Type |
Validation |
Execution |
---|---|---|---|---|
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
| |||
(reserved) |
| |||
(reserved) |
| |||
|
|
| ||
(reserved) |
| |||
|
|
| ||
|
| |||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
(reserved) |
| |||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
|
|
| ||
|
|
| ||
(reserved) |
| |||
(reserved) |
| |||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
(reserved) |
| |||
|
|
| ||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
|
|
| ||
|
|
| ||
(reserved) |
| |||
(reserved) |
| |||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
(reserved) |
| |||
|
|
| ||
(reserved) |
| |||
(reserved) |
| |||
(reserved) |
| |||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
|
|
| ||
(reserved) |
| |||
(reserved) |
|
Note
Multi-byte opcodes are given with the shortest possible encoding in the table. However, what is following the first byte is actually a u32 with variable-length encoding and consequently has multiple possible representations.
A.10 Index of Semantic Rules
Well-formedness of Types
Construct |
Judgement |
---|---|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
|
Typing of Static Constructs
Construct |
Judgement |
---|---|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
|
Typing of Runtime Constructs
Construct |
Judgement |
---|---|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
|
Defaultability
Construct |
Judgement |
---|---|
|
Constantness
Construct |
Judgement |
---|---|
| |
|
Matching
Construct |
Judgement |
---|---|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
|
Store Extension
Construct |
Judgement |
---|---|
| |
| |
| |
| |
| |
| |
| |
| |
| |
|
Execution
Construct |
Judgement |
---|---|
| |
|
6.2.4. Comments
A comment can either be a line comment, started with a double semicolon ‘;;’ and extending to the end of the line, or a block comment, enclosed in delimiters ‘(;’…‘;)’. Block comments can be nested.
Here, the pseudo token eof indicates the end of the input. The look-ahead restrictions on the productions for blockchar disambiguate the grammar such that only well-bracketed uses of block comment delimiters are allowed.
Note
Any formatting and control characters are allowed inside comments.