WebAssembly Specification

Release 2.0 + Threads (Draft 2023-10-10)
Editor: Andreas Rossberg

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 2.0 + Threads (Draft 2023-10-10) 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

A contraction of “WebAssembly”, not an acronym, hence not using all-caps.

2

No program can break WebAssembly’s memory model. Of course, it cannot guarantee that an unsafe language compiling to WebAssembly does not corrupt its own memory layout, e.g. inside WebAssembly’s linear memory.

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:

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 element type. It allows programs to select such values indirectly through a dynamic index operand. Currently, the only available element type is an untyped function reference or a reference to an external host value. Thereby, a program can call functions indirectly through a dynamic index into a table. For example, 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.

1

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” :

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. Reference Types

Reference types classify first-class references to objects in the runtime store.

The type denotes the infinite union of all references to functions, regardless of their function types.

The type denotes the infinite union of all references to objects owned by the embedder and that can be passed into WebAssembly under this type.

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. 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.

2.3.4.1. Conventions
  • The meta variable ranges over value types or subclasses thereof where clear from context.

2.3.5. Result Types

Result types classify the result of executing instructions or functions, which is a sequence of values, written with brackets.

2.3.6. 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.7. 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.8. 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. The memory type also determines whether this memory is shared.

2.3.9. 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.

Note

In future versions of WebAssembly, additional element types may be introduced.

2.3.10. Global Types

Global types classify global variables, which hold a value and can either be mutable or immutable.

2.3.11. External Types

External types classify imports and external values with their respective types.

2.3.11.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 bitwidth 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.

These instructions produce a null value, check for a null value, or produce a reference to a given function, respectively.

2.4.4. 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.5. 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.6. 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.7. Memory Instructions

Instructions in this group are concerned with linear memory.

Memory is accessed with and instructions for the different number types. They all take 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 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.

Note

Future versions of WebAssembly might provide memory instructions with 64 bit address ranges.

The instruction returns the current size of a memory. The instruction grows 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 to a given byte. The instruction copies data from a source memory region to a possibly overlapping destination region. 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.

Note

In the current version of WebAssembly, all memory instructions implicitly operate on memory index . This restriction may be lifted in future versions.

2.4.8. Atomic Memory Instructions

Instructions in this group are concerned with accessing linear memory atomically.

Memory is accessed atomically using the , , and instructions. All instructions take a memory immediate , just like their non-atomic equivalents. Unlike non-atomic memory access instructions, only integer value types can be used. Also unlike non-atomic memory access instructions, there are no sign extension modes; atomic memory accesses are always zero-extending.

The instructions are read-modify-write instructions. They each have an atomic operator, which specifies how memory will be modified. Each instruction returns the value read from memory before modification. The operator doesn’t use the read value, but instead stores its argument unmodified. The operator is similar, but only performs this action conditionally, if the read value is equal to a provided comparison argument. All other atomic operators have the same behavior as the binary operator of the same name.

The , , and instructions provide primitive synchronization between threads. The instructions atomically load a value from the calculated effective address and compare it to an expected value. If they are equal, the thread is then suspended until a given timeout expires or another thread wakes it. The instruction wakes threads that are waiting on a given address, up to a given maximum. The instruction takes no operands, and returns nothing. It is intended to preserve the synchronization guarantees of the fence operators of higher-level languages. Unlike other atomic operators, it does not target a particular linear memory.

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, terminated with, or separated by, or pseudo-instructions. As the grammar prescribes, they must be well-nested.

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, or as an optional value type inline, which is a shorthand for the function 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 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 calls a function indirectly through an operand indexing into a table that is denoted by a table index and must have type . 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.

2.4.10. Expressions

Function bodies, initialization values for globals, and offsets of element or 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, 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 and globals 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.

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 function types.

All function types used in a module must be defined in this component. They are referenced by type indices.

Note

Future versions of WebAssembly may add additional forms of type definitions.

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 a vector of opaque values of a particular reference type. 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 can be initialized through element segments.

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 .

Note

In the current version of WebAssembly, at most one memory may be defined or imported in a single module, and all constructs implicitly reference this memory . This restriction may be lifted in future versions.

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.7. 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.8. 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.9. 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.10. 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, and globals, which are referenced through a respective descriptor.

2.5.10.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.11. 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, and globals. 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:

  1. In prose, describing the meaning in intuitive form.

  2. 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. 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 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.

  • Element Segments: the list of element segments declared in the current module, represented by their element 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 value 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.2. 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.3. 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 local 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.

1

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.

2

For example: Benjamin Pierce. Types and Programming Languages. The MIT Press 2002

3.2. Types

Most types are universally valid. However, restrictions apply to limits, which must be checked during validation. Moreover, block types are converted to plain function types for ease of processing.

3.2.1. Limits

Limits must have meaningful bounds that are within a given range.

3.2.1.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.2. Block Types

Block types may be expressed in one of two forms, both of which are converted to plain function types by the following rules.

3.2.2.1.
3.2.2.2.

3.2.3. Function Types

Function types are always valid.

3.2.3.1.
  • The function type is valid.

3.2.4. Table Types

3.2.4.1.
  • The limits must be valid within range .

  • Then the table type is valid.

3.2.5. Memory Types

3.2.5.1.
  • The limits must be valid within range .

  • Then the memory type is valid.

3.2.6. Global Types

3.2.6.1.
  • The global type is valid.

3.2.7. External Types

3.2.7.1.
3.2.7.2.
3.2.7.3.
3.2.7.4.

3.2.8. Import Subtyping

When instantiating a module, external values must be provided whose types are matched against the respective external types classifying each import. In some cases, this allows for a simple form of subtyping (written “” formally), as defined here.

3.2.8.1. 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.2.8.2. Functions

An external type matches if and only if:

3.2.8.3. Tables

An external type matches if and only if:

3.2.8.4. Memories

An external type matches if and only if:

3.2.8.5. Globals

An external type matches if and only if:

3.3. Instructions

Instructions are classified by stack types that describe how instructions manipulate the operand stack.

The types describe the required input stack with operand types that an instruction pops off and the provided output stack with result values of types that it pushes back. Stack types are akin to function types, except that they allow individual operands to be classified as (bottom), indicating that the type is unconstrained. As an auxiliary notion, an operand type matches another operand type , if is either or equal to . This is extended to stack types in a point-wise manner.

Note

For example, the instruction has type , consuming two values and producing one.

Typing extends to instruction sequences . Such a sequence has a stack type if the accumulative effect of executing the instructions is consuming values of types off the operand stack and pushing new values of types .

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:

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 valid with type for any possible sequences of operand 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.3.1. Numeric Instructions

3.3.1.1.
  • The instruction is valid with type .

3.3.1.2.
  • The instruction is valid with type .

3.3.1.3.
  • The instruction is valid with type .

3.3.1.4.
  • The instruction is valid with type .

3.3.1.5.
  • The instruction is valid with type .

3.3.1.6.
  • The instruction is valid with type .

3.3.2. Reference Instructions

3.3.2.1.
  • The instruction is valid with type .

Note

In future versions of WebAssembly, there may be reference types for which no null reference is allowed.

3.3.2.2.
3.3.2.3.

3.3.3. 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.3.3.1.
  • The instruction is valid with type .

3.3.3.2.
3.3.3.3.
3.3.3.4.
3.3.3.5.
  • The instruction is valid with type .

3.3.3.6.
3.3.3.7.
3.3.3.8.
3.3.3.9.
3.3.3.10.
3.3.3.11.
3.3.3.12.
3.3.3.13.
3.3.3.14.
3.3.3.15.
  • The instruction is valid with type .

3.3.3.16.
3.3.3.17.
3.3.3.18.
  • The instruction is valid with type .

3.3.3.19.
3.3.3.20.
3.3.3.21.

3.3.4. Parametric Instructions

3.3.4.1.

Note

Both and without annotation are value-polymorphic instructions.

3.3.4.2.

Note

In future versions of WebAssembly, may allow more than one value per choice.

3.3.5. Variable Instructions

3.3.5.1.
  • The local must be defined in the context.

  • Let be the value type .

  • Then the instruction is valid with type .

3.3.5.2.
  • The local must be defined in the context.

  • Let be the value type .

  • Then the instruction is valid with type .

3.3.5.3.
  • The local must be defined in the context.

  • Let be the value type .

  • Then the instruction is valid with type .

3.3.5.4.
3.3.5.5.

3.3.6. Table Instructions

3.3.6.1.
3.3.6.2.
3.3.6.3.
  • The table must be defined in the context.

  • Then the instruction is valid with type .

3.3.6.4.
3.3.6.5.
3.3.6.6.
3.3.6.7.
3.3.6.8.
  • The element segment must be defined in the context.

  • Then the instruction is valid with type .

3.3.7. Memory Instructions

3.3.7.1.
  • The memory must be defined in the context.

  • The alignment must not be larger than the bit width of divided by .

  • Then the instruction is valid with type .

3.3.7.2.
  • The memory must be defined in the context.

  • The alignment must not be larger than .

  • Then the instruction is valid with type .

3.3.7.3.
  • The memory must be defined in the context.

  • The alignment must not be larger than the bit width of divided by .

  • Then the instruction is valid with type .

3.3.7.4.
  • The memory must be defined in the context.

  • The alignment must not be larger than .

  • Then the instruction is valid with type .

3.3.7.5.
  • The memory must be defined in the context.

  • The alignment must not be larger than .

  • Then the instruction is valid with type .

3.3.7.6.
  • The memory must be defined in the context.

  • The alignment must not be larger than .

  • Then the instruction is valid with type .

3.3.7.7.
  • The memory must be defined in the context.

  • The alignment must not be larger than .

  • Then the instruction is valid with type .

3.3.7.8.
  • The lane index must be smaller than .

  • The memory must be defined in the context.

  • The alignment must not be larger than .

  • Then the instruction is valid with type .

3.3.7.9.
  • The lane index must be smaller than .

  • The memory must be defined in the context.

  • The alignment must not be larger than .

  • Then the instruction is valid with type .

3.3.7.10.
  • The memory must be defined in the context.

  • Then the instruction is valid with type .

3.3.7.11.
  • The memory must be defined in the context.

  • Then the instruction is valid with type .

3.3.7.12.
  • The memory must be defined in the context.

  • Then the instruction is valid with type .

3.3.7.13.
  • The memory must be defined in the context.

  • Then the instruction is valid with type .

3.3.7.14.
  • The memory must be defined in the context.

  • The data segment must be defined in the context.

  • Then the instruction is valid with type .

3.3.7.15.
  • The data segment must be defined in the context.

  • Then the instruction is valid with type .

3.3.8. Atomic Memory Instructions

3.3.8.1.
  • The memory must be defined in the context.

  • The alignment must be equal to the width of divided by .

  • Then the instruction is valid with type .

3.3.8.2.
  • The memory must be defined in the context.

  • The alignment must be equal to .

  • Then the instruction is valid with type .

3.3.8.3.
  • The memory must be defined in the context.

  • The alignment must be equal to the width of divided by .

  • Then the instruction is valid with type .

3.3.8.4.
  • The memory must be defined in the context.

  • The alignment must be equal to .

  • Then the instruction is valid with type .

3.3.8.5.
  • The memory must be defined in the context.

  • The alignment must be equal to the width of divided by .

  • Then the instruction is valid with type .

3.3.8.6.
  • The memory must be defined in the context.

  • The alignment must be equal to .

  • Then the instruction is valid with type .

3.3.8.7.
  • The memory must be defined in the context.

  • The alignment must be equal to the width of divided by .

  • Then the instruction is valid with type .

3.3.8.8.
  • The memory must be defined in the context.

  • The alignment must be equal to .

  • Then the instruction is valid with type .

3.3.8.9.
3.3.8.10.
3.3.8.11.
  • The instruction is valid with type .

Note

The instruction may occur in modules which declare no memory without causing a validation error.

3.3.9. Control Instructions

3.3.9.1.
  • The instruction is valid with type .

3.3.9.2.
  • The instruction is valid with type , for any sequences of operand types and .

Note

The instruction is stack-polymorphic.

3.3.9.3.
  • The block type must be valid as some function 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.3.9.4.
  • The block type must be valid as some function 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.3.9.5.
  • The block type must be valid as some function 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.3.9.6.
  • The label must be defined in the context.

  • Let be the result type .

  • Then the instruction is valid with type , for any sequences of operand types and .

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.

3.3.9.7.
  • 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 first, so that performs a relative lookup as expected.

3.3.9.8.
  • The label must be defined in the context.

  • For all in , the label must be defined in the context.

  • There must be a sequence of operand types, such that:

    • For each operand type in and corresponding type in , matches .

    • For all in , and for each operand type in and corresponding type in , matches .

  • Then the instruction is valid with type , for any sequences of operand types and .

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.

3.3.9.9.
  • The return type must not be absent in the context.

  • Let be the result type of .

  • Then the instruction is valid with type , for any sequences of operand types and .

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.3.9.10.
  • The function must be defined in the context.

  • Then the instruction is valid with type .

3.3.9.11.

3.3.10. Instruction Sequences

Typing of instruction sequences is defined recursively.

3.3.10.1. Empty Instruction Sequence:
  • The empty instruction sequence is valid with type , for any sequence of operand types .

3.3.10.2. Non-empty Instruction Sequence:
  • The instruction sequence must be valid with type , for some sequences of operand types and .

  • The instruction must be valid with type , for some sequences of operand types and .

  • There must be a sequence of operand types , such that where the type sequence is as long as .

  • For each operand type in and corresponding type in , matches .

  • Then the combined instruction sequence is valid with type .

3.3.11. Expressions

Expressions are classified by result types of the form .

3.3.11.1.
3.3.11.2. Constant Expressions

Note

Currently, constant expressions occurring in globals, element, or data segments are further constrained in that contained instructions are only allowed to 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.4. Modules

Modules are valid when all the components they contain are valid. Furthermore, most definitions are themselves classified with a suitable type.

3.4.1. Functions

Functions are classified by function types of the form .

3.4.1.1.
  • The type must be defined in the context.

  • Let be the function type .

  • Let be the same context as , but with:

  • Under the context , the expression must be valid with type .

  • Then the function definition is valid with type .

3.4.2. Tables

Tables are classified by table types.

3.4.2.1.

3.4.3. Memories

Memories are classified by memory types.

3.4.3.1.

3.4.4. Globals

Globals are classified by global types of the form .

3.4.4.1.

3.4.5. Element Segments

Element segments are classified by the reference type of their elements.

3.4.5.1.
3.4.5.2.
3.4.5.3.
3.4.5.4.

3.4.6. Data Segments

Data segments are not classified by any type but merely checked for well-formedness.

3.4.6.1.
  • The data mode must be valid.

  • Then the data segment is valid.

3.4.6.2.
  • The data mode is valid.

3.4.6.3.

3.4.7. Start Function

Start function declarations are not classified by any type.

3.4.7.1.
  • The function must be defined in the context.

  • The type of must be .

  • Then the start function is valid.

3.4.8. Exports

Exports and export descriptions are classified by their external type.

3.4.8.1.
3.4.8.2.
3.4.8.3.
3.4.8.4.
  • The memory must be defined in the context.

  • Then the export description is valid with external type .

3.4.8.5.

3.4.9. Imports

Imports and import descriptions are classified by external types.

3.4.9.1.
3.4.9.2.
  • The function must be defined in the context.

  • Let be the function type .

  • Then the import description is valid with type .

3.4.9.3.
3.4.9.4.
3.4.9.5.

3.4.10. 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.

Note

Most definitions in a module – particularly functions – 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 and not accessible within constant expressions when they are defined locally. The effect of defining the limited context for validating certain definitions is that they can only access functions and imported globals and nothing else.

Note

The restriction on the number of memories may be lifted in future versions of WebAssembly.

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:

  1. In prose, describing the execution in intuitive form.

  2. 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.

  • 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. Execution rules for each instruction have the following general form:

A configuration is a syntactic description of a program state. Each rule specifies one step of execution, resulting in an altered configuration. In addition, steps which involve operations related to shared memory concurrency may emit a number of actions which are used to specify relevant concurrent behaviours (for further details, see Events and the Relaxed Memory Model). 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 occurred.

Note

For example, the following instruction sequence,

terminates after three steps:

where and and .

1

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.

2

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 function references, pointing to a specific function address, or external references pointing to an uninterpreted form of extern address that can be defined by the embedder to represent its own objects.

Note

Future versions of WebAssembly may add additional forms of reference.

Each value type has an associated default value; it is the respective value for number types, for vector types, and null for reference types.

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 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, and globals, element segments, and data segments 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:

1

In practice, implementations may apply techniques like garbage collection 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, and global instances, element instances, and data 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.5. Time Stamps

In order to track the relative ordering in the execution of multiple threads and the occurrence of events, the semantics uses a notion of abstract time stamps.

Each time stamp denotes a discrete point in time, and is drawn from an infinite set. The shape of time stamps is not specified or observable.

Time stamps are associated with a total order – if a time stamp is totally ordered before time stamp , this is written as .

Time stamps are also associated with a happens before partial order – if a time stamp happens before , this is written as .

During the execution of WebAssembly code, time stamped events may be emitted which are related by one or both of these orderings, thus constraining the code’s observable behaviours according to WebAssembly’s relaxed memory model.

4.2.6. 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, and global 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.7. 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.

Note

Function instances are immutable, and their identity is not observable by WebAssembly code. However, the embedder might provide implicit or explicit means for distinguishing their addresses.

4.2.8. Table Instances

A table instance is the runtime representation of a table. It records its type and holds a vector 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 equal to the element type of . It also is an invariant that the length of the element vector never exceeds the maximum size of , if present.

4.2.9. Memory Instances

A memory instance is the runtime representation of a linear memory. It records its original memory type and takes one of two different shapes depending on whether that type is shared or not. It is an invariant of the semantics that the shape always matches the type.

The instance of a memory with unshared type holds a vector of bytes directly representing its state. The length of the vector 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.

For memories of shared type, no state is recorded in the instance itself.

4.2.10. 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 equal to the value type of .

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, 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. Stack

Besides the store, most instructions interact with an implicit stack. The stack contains three kinds of entries:

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.15.1. Values

Values are represented by themselves.

4.2.15.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.15.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:

The values of the locals are mutated by respective variable instructions.

4.2.15.4. Conventions
  • The meta variable ranges over labels where clear from context.

  • The meta variable ranges over frames where clear from context.

  • The following auxiliary definition takes a block type and looks up the function type that it denotes in the current frame:

4.2.16. Administrative Instructions

Note

This section is only relevant for the formal notation.

In order to express the reduction of traps, calls, 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 function reference values. Similarly, represents external references.

The instruction represents the imminent invocation of a function instance, identified by its address. It unifies the handling of different forms of calls.

The and instructions model labels and frames “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.

The instruction models a thread suspending further execution as the result of executing a instruction. If its argument is non-negative, execution may resume after at least nanoseconds. Otherwise, execution will only resume after is the target of a corresponding instruction.

The instruction is used to perform an action at a precise point in execution. These actions are used by the Relaxed Memory Model to determine the behaviours that are observable in a concurrent execution.

The instruction models the execution of the host environment.

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.16.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 targeted 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.17. Events

The interaction of a computation with the store is described through events. An event is a (possibly empty) set of actions, such as reads and writes, that are atomically performed by the execution of an individual instruction. Each event is annotated with two time stamps: the first records the time stamp of the event’s immediate predecessor while the second uniquely identifies the event.

The access of mutable shared state is performed through the , , and actions. Each action accesses an abstract location, which consists of an address of a shared memory instance, a symbolic field name in the respective object (either for the size or for the vector of bytes), and an offset index into the field.

In each case, read and write actions record the store value that has been read or written, which is either a regular value or a sequence of bytes, depending on the location accessed. An event, performing an atomic read-modify-write access, records both the store values read (first) and written (second); it is an invariant of the semantics that both are either regular values of the same type or byte sequences of the same length.

and events are further annotated by a memory ordering, which describes whether the access is unordered, as e.g. performed by a regular load or store instruction, or sequentially consistent, as e.g. performed by atomic memory instructions. A third ordering, initialisation, is used to record the initial value taken by the memory location upon its creation. A action always is sequentially consistent.

Note

Future versions of WebAssembly may introduce additional orderings.

Finally, a host action is an action performed outside of WebAssembly code. Its form and meaning is outside the scope of this specification.

Note

An embedder may define a custom set of host actions and respective ordering constraints to model other forms of interactions that are not expressible within WebAssembly, but whose ordering relative to WebAssembly events is relevant for the combined semantics.

4.2.17.1. Conventions
  • The actions and are abbreviated to just and when is .

  • A location may syntactically elide its offset in the case that it is 0.

The following auxiliary definition is used to classify whether an access will tear - that is, whether it will observably decompose into bytewise accesses when it participates in a data race.

Relations between time stamps are lifted to relations between events.

4.2.17.2. Configurations

A thread is a computation over instructions that operates relative to a current frame referring to the module instance in which the current computation runs. The thread is annotated with the time it was last active.

A global configuration consists of the current store and a list of executing threads.

A local configuration describes the state of a single executing thread.

A thread has terminated when its instruction sequence has been reduced to a result, that is, either a sequence of values or to a .

4.2.17.3. Convention
  • The meta variable ranges over threads where clear from context.

4.2.18. Reduction

Formally, WebAssembly computation is defined by two small-step reduction relations on global and local configurations that define how a single step of execution modifies these configurations, respectively.

4.2.18.1. Global Reduction

Global reduction is concerned with allocation in the global store and synchronization between multiple threads. It emits a (possibly empty) set of events that are produced by the corresponding step of computation. 2

Formally, global reduction is a relation

defined by inductive rewrite rules on global configurations.

The following structural rule for global reduction delegates to local reduction for single thread execution:

The following rule for global reduction describes the creation of a new thread by the host:

Note

The time stamp indicates the point in time at which the computation step takes place, marking both the emitted atomic event and the updated time of the thread. This time stamp is chosen non-deterministically in the rule. However, the second side condition ensures that the time of the last activity of the thread happened before , thereby imposing program order for any events originating from the same thread.

4.2.18.2. Local Reduction

Local reduction defines the execution of individual instructions. Each execution step can perform a (possibly empty) set of actions.

Formally, this is described by a labelled relation

To avoid unnecessary clutter, the following conventions are employed in the notation for local reduction rules:

  • The configuration’s store is omitted from rules that do not touch it.

  • The configuration’s frame is omitted from rules that do not touch it.

4.2.18.3. 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 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.

2

The semantics of global configurations is derived from the following article: Conrad Watt, Andreas Rossberg, Jean Pichon-Pharabod. Weakening WebAssembly. Proceedings of the ACM on Programming Languages (OOPSLA 2019). ACM 2019.

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:

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 have the same underlying representation as an . They can also be interpreted as a sequence of numeric values packed into a with a particular .

These functions are bijections, so they are 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 .

Note

This operator is partial.

As long as both operators are defined, it holds that .

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 .

Note

This operator is partial.

As long as both operators are defined, it holds that .

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.
4.3.2.28.
  • Return if is greater than , otherwise.

4.3.2.29.
4.3.2.30.
  • Return if is less than or equal to , otherwise.

4.3.2.31.
4.3.2.32.
  • Return if is greater than or equal to , otherwise.

4.3.2.33.
4.3.2.34.
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 .

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 .

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 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.

This 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.
  • 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.8.
  • 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.9.
  • If and have the same sign, then return .

  • Else return with negated sign.

4.3.3.10.
  • 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.11.
  • 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.12.
  • 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.13.
  • 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.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 greater than but smaller than , then return positive zero.

  • Else return the largest integral value that is not larger 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 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.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 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.17.
  • 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.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 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.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 larger 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 smaller than or equal to , 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 is less than then return .

  • Else return .

4.3.3.24.
  • 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 .

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.
4.3.4.11.
4.3.4.12.
  • Let be the bit sequence .

  • Return the constant for which .

4.3.4.13.
4.3.4.14.

4.4. Instructions

WebAssembly computation is performed by executing individual instructions.

4.4.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.4.1.1.
  1. Push the value to the stack.

Note

No formal reduction rule is required for this instruction, since instructions already are values.

4.4.1.2.
  1. Assert: due to validation, a value of value type is on the top of the stack.

  2. Pop the value from the stack.

  3. If is defined, then:

    1. Let be a possible result of computing .

    2. Push the value to the stack.

  4. Else:

    1. Trap.

4.4.1.3.
  1. Assert: due to validation, two values of value type are on the top of the stack.

  2. Pop the value from the stack.

  3. Pop the value from the stack.

  4. If is defined, then:

    1. Let be a possible result of computing .

    2. Push the value to the stack.

  5. Else:

    1. Trap.

4.4.1.4.
  1. Assert: due to validation, a value of value type is on the top of the stack.

  2. Pop the value from the stack.

  3. Let be the result of computing .

  4. Push the value to the stack.

4.4.1.5.
  1. Assert: due to validation, two values of value type are on the top of the stack.

  2. Pop the value from the stack.

  3. Pop the value from the stack.

  4. Let be the result of computing .

  5. Push the value to the stack.

4.4.1.6.
  1. Assert: due to validation, a value of value type is on the top of the stack.

  2. Pop the value from the stack.

  3. If is defined:

    1. Let be a possible result of computing .

    2. Push the value to the stack.

  4. Else:

    1. Trap.

4.4.2. Reference Instructions

4.4.2.1.
  1. Push the value to the stack.

Note

No formal reduction rule is required for this instruction, since the instruction is already a value.

4.4.2.2.
  1. Assert: due to validation, a reference value is on the top of the stack.

  2. Pop the value from the stack.

  3. If is , then:

    1. Push the value to the stack.

  4. Else:

    1. Push the value to the stack.

4.4.2.3.
  1. Let be the current frame.

  2. Assert: due to validation, exists.

  3. Let be the function address .

  4. Push the value to the stack.

4.4.3. Vector Instructions

Most vector instructions are defined in terms of generic numeric operators applied lane-wise based on the shape.

Note

For example, the result of instruction applied to operands invokes , which maps to , where and are sequences resulting from invoking and respectively.

4.4.3.1.
  1. Push the value to the stack.

Note

No formal reduction rule is required for this instruction, since instructions coincide with values.

4.4.3.2.
  1. Assert: due to validation, a value of value type is on the top of the stack.

  2. Pop the value from the stack.

  3. Let be the result of computing .

  4. Push the value to the stack.

4.4.3.3.
  1. Assert: due to validation, two values of value type are on the top of the stack.

  2. Pop the value from the stack.

  3. Pop the value from the stack.

  4. Let be the result of computing .

  5. Push the value to the stack.

4.4.3.4.
  1. Assert: due to validation, three values of value type are on the top of the stack.

  2. Pop the value from the stack.

  3. Pop the value from the stack.

  4. Pop the value from the stack.

  5. Let be the result of computing .

  6. Push the value to the stack.

4.4.3.5.
  1. Assert: due to validation, a value of value type is on the top of the stack.

  2. Pop the value from the stack.

  3. Let be the result of computing .

  4. Push the value onto the stack.

4.4.3.6.
  1. Assert: due to validation, two values of value type are on the top of the stack.

  2. Pop the value from the stack.

  3. Let be the result of computing .

  4. Pop the value from the stack.

  5. Let be the result of computing .

  6. Let be the concatenation of the two sequences and .

  7. Let be the result of computing .

  8. Push the value onto the stack.

4.4.3.7.
  1. Assert: due to validation, two values of value type are on the top of the stack.

  2. Assert: due to validation, for all in it holds that .

  3. Pop the value from the stack.

  4. Let be the result of computing .

  5. Pop the value from the stack.

  6. Let be the result of computing .

  7. Let be the concatenation of the two sequences and .

  8. Let be the result of computing .

  9. Push the value onto the stack.

4.4.3.8.
  1. Let be the type .

  2. Assert: due to validation, a value of value type is on the top of the stack.

  3. Pop the value from the stack.

  4. Let be the integer .

  5. Let be the result of computing .

  6. Push the value to the stack.

4.4.3.9.
  1. Assert: due to validation, .

  2. Assert: due to validation, a value of value type is on the top of the stack.

  3. Pop the value from the stack.

  4. Let be the result of computing .

  5. Let be the type .

  6. Let be the result of computing .

  7. Push the value to the stack.

4.4.3.10.
  1. Assert: due to validation, .

  2. Let be the type .

  3. Assert: due to validation, a value of value type is on the top of the stack.

  4. Pop the value from the stack.

  5. Assert: due to validation, a value of value type is on the top of the stack.

  6. Pop the value from the stack.

  7. Let be the result of computing .

  8. Let be the result of computing .

  9. Push on the stack.

4.4.3.11.
  1. Assert: due to validation, a value of value type is on the top of the stack.

  2. Pop the value from the stack.

  3. Let be the result of computing .

  4. Push the value to the stack.

4.4.3.12.
  1. Assert: due to validation, two values of value type are on the top of the stack.

  2. Pop the value from the stack.

  3. Pop the value from the stack.

  4. If is defined:

    1. Let be a possible result of computing .

    2. Push the value to the stack.

  5. Else:

    1. Trap.

4.4.3.13.
  1. Assert: due to validation, two values of value type are on the top of the stack.

  2. Pop the value from the stack.

  3. Pop the value from the stack.

  4. Let be the result of computing .

  5. Let be the result of computing .

  6. Let be the result of computing .

  7. Let be the result of computing .

  8. Let be the result of computing .

  9. Push the value to the stack.

4.4.3.14.
  1. Assert: due to validation, a value of value type is on the top of the stack.

  2. Pop the value from the stack.

  3. Assert: due to validation, a value of value type is on the top of the stack.

  4. Pop the value from the stack.

  5. Let be the result of computing .

  6. Let be the result of computing .

  7. Let be the result of computing .

  8. Push the value to the stack.

4.4.3.15.
  1. Assert: due to validation, a value of value type is on the top of the stack.

  2. Pop the value from the stack.

  3. Let be the result of computing .

  4. Let be the result of computing .

  5. Push the value onto the stack.

4.4.3.16.
  1. Assert: due to validation, a value of value type is on the top of the stack.

  2. Pop the value from the stack.

  3. Let be the result of computing .

  4. Let be the bit width of value type .

  5. Let be the result of computing .

  6. Let be the concatenation of the two sequences and .

  7. Let be the result of computing .

  8. Push the value onto the stack.

4.4.3.17.
  1. Assert: due to syntax, .

  2. Assert: due to validation, two values of value type are on the top of the stack.

  3. Pop the value from the stack.

  4. Let be the result of computing .

  5. Let be the result of computing .

  6. Pop the value from the stack.

  7. Let be the result of computing .

  8. Let be the result of computing .

  9. Let be the concatenation of the two sequences and .

  10. Let be the result of computing .

  11. Push the value onto the stack.

4.4.3.18.
  1. Assert: due to syntax, .

  2. Assert: due to validation, a value of value type is on the top of the stack.

  3. Pop the value from the stack.

  4. Let be the result of computing .

  5. Let be the result of computing .

  6. Let be the result of computing .

  7. Push the value onto the stack.

4.4.3.19.
  1. Assert: due to syntax, .

  2. Assert: due to validation, a value of value type is on the top of the stack.

  3. Pop the value from the stack.

  4. Let be the result of computing .

  5. If is , then:

    1. Let be the sequence .

  6. Else:

    1. Let be the sequence .

  7. Let be the result of computing .

  8. Let be the result of computing .

  9. Push the value onto the stack.

where:

4.4.3.20.
  1. Assert: due to syntax, .

  2. Assert: due to validation, a value of value type is on the top of the stack.

  3. Pop the value from the stack.

  4. Let be the result of computing .

  5. Let be the result of computing .

  6. Let be the concatenation of the two sequences and .

  7. Let be the result of computing .

  8. Push the value onto the stack.

4.4.3.21.
  1. Assert: due to validation, two values of value type are on the top of the stack.

  2. Pop the value from the stack.

  3. Pop the value from the stack.

  4. Let be the result of computing .

  5. Let be the result of computing .

  6. Let be the result of computing .

  7. Let be the result of computing .

  8. Let be the result of computing .

  9. Let be the result of computing .

  10. Let be the result of computing .

  11. Push the value onto the stack.

4.4.3.22.
  1. Assert: due to syntax, .

  2. Assert: due to validation, two values of value type are on the top of the stack.

  3. Pop the value from the stack.

  4. Pop the value from the stack.

  5. Let be the result of computing .

  6. Let be the result of computing .

  7. If is , then:

    1. Let be the sequence .

    2. Let be the sequence .

  8. Else:

    1. Let be the sequence .

    2. Let be the sequence .

  9. Let be the result of computing .

  10. Let be the result of computing .

  11. Let be the result of computing .

  12. Let be the result of computing .

  13. Push the value onto the stack.

where:

4.4.3.23.
  1. Assert: due to syntax, .

  2. Assert: due to validation, a value of value type is on the top of the stack.

  3. Pop the value from the stack.

  4. Let be the result of computing .

  5. Let be the result of computing .

  6. Let be the result of computing .

  7. Let be the result of computing .

  8. Push the value to the stack.

4.4.4. Parametric Instructions

4.4.4.1.
  1. Assert: due to validation, a value is on the top of the stack.

  2. Pop the value from the stack.

4.4.4.2.
  1. Assert: due to validation, a value of value type is on the top of the stack.

  2. Pop the value from the stack.

  3. Assert: due to validation, two more values (of the same value type) are on the top of the stack.

  4. Pop the value from the stack.

  5. Pop the value from the stack.

  6. If is not , then:

    1. Push the value back to the stack.

  7. Else:

    1. Push the value back to the stack.

Note

In future versions of WebAssembly, may allow more than one value per choice.

4.4.5. Variable Instructions

4.4.5.1.
  1. Let be the current frame.

  2. Assert: due to validation, exists.

  3. Let be the value .

  4. Push the value to the stack.

4.4.5.2.
  1. Let be the current frame.

  2. Assert: due to validation, exists.

  3. Assert: due to validation, a value is on the top of the stack.

  4. Pop the value from the stack.

  5. Replace with the value .

4.4.5.3.
  1. Assert: due to validation, a value is on the top of the stack.

  2. Pop the value from the stack.

  3. Push the value to the stack.

  4. Push the value to the stack.

  5. Execute the instruction .

4.4.5.4.
  1. Let be the current frame.

  2. Assert: due to validation, exists.

  3. Let be the global address .

  4. Assert: due to validation, exists.

  5. Let be the global instance .

  6. Let be the value .

  7. Push the value to the stack.

4.4.5.5.
  1. Let be the current frame.

  2. Assert: due to validation, exists.

  3. Let be the global address .

  4. Assert: due to validation, exists.

  5. Let be the global instance .

  6. Assert: due to validation, a value is on the top of the stack.

  7. Pop the value from the stack.

  8. Replace with the value .

Note

Validation ensures that the global is, in fact, marked as mutable.

4.4.6. Table Instructions

4.4.6.1.
  1. Let be the current frame.

  2. Assert: due to validation, exists.

  3. Let be the table address .

  4. Assert: due to validation, exists.

  5. Let be the table instance .

  6. Assert: due to validation, a value of value type is on the top of the stack.

  7. Pop the value from the stack.

  8. If is not smaller than the length of , then:

    1. Trap.

  9. Let be the value .

  10. Push the value to the stack.

4.4.6.2.
  1. Let be the current frame.

  2. Assert: due to validation, exists.

  3. Let be the table address .

  4. Assert: due to validation, exists.

  5. Let be the table instance .

  6. Assert: due to validation, a reference value is on the top of the stack.

  7. Pop the value from the stack.

  8. Assert: due to validation, a value of value type is on the top of the stack.

  9. Pop the value from the stack.

  10. If is not smaller than the length of , then:

    1. Trap.

  11. Replace the element with .

4.4.6.3.
  1. Let be the current frame.

  2. Assert: due to validation, exists.

  3. Let be the table address .

  4. Assert: due to validation, exists.

  5. Let be the table instance .

  6. Let be the length of .

  7. Push the value to the stack.

4.4.6.4.
  1. Let be the current frame.

  2. Assert: due to validation, exists.

  3. Let be the table address .

  4. Assert: due to validation, exists.

  5. Let be the table instance .

  6. Let be the length of .

  7. Assert: due to validation, a value of value type is on the top of the stack.

  8. Pop the value from the stack.

  9. Assert: due to validation, a reference value is on the top of the stack.

  10. Pop the value from the stack.

  11. Let be the value , for which is .

  12. Either:

  1. If growing by entries with initialization value succeeds, then:

    1. Push the value to the stack.

  2. Else:

    1. Push the value to the stack.

  1. Or:

  1. 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.4.6.5.
  1. Let be the current frame.

  2. Assert: due to validation, exists.

  3. Let be the table address .

  4. Assert: due to validation, exists.

  5. Let be the table instance .

  6. Assert: due to validation, a value of value type is on the top of the stack.

  7. Pop the value from the stack.

  8. Assert: due to validation, a reference value is on the top of the stack.

  9. Pop the value from the stack.

  10. Assert: due to validation, a value of value type is on the top of the stack.

  11. Pop the value from the stack.

  12. If is larger than the length of , then:

    1. Trap.

  1. If is , then:

    1. Return.

  2. Push the value to the stack.

  3. Push the value to the stack.

  4. Execute the instruction .

  5. Push the value to the stack.

  6. Push the value to the stack.

  7. Push the value to the stack.

  8. Execute the instruction .

4.4.6.6.
  1. Let be the current frame.

  2. Assert: due to validation, exists.

  3. Let be the table address .

  4. Assert: due to validation, exists.

  5. Let be the table instance .

  6. Assert: due to validation, exists.

  7. Let be the table address .

  8. Assert: due to validation, exists.

  9. Let be the table instance .

  10. Assert: due to validation, a value of value type is on the top of the stack.

  11. Pop the value from the stack.

  12. Assert: due to validation, a value of value type is on the top of the stack.

  13. Pop the value from the stack.

  14. Assert: due to validation, a value of value type is on the top of the stack.

  15. Pop the value from the stack.

  16. If is larger than the length of or is larger than the length of , then:

    1. Trap.

  17. If , then:

  1. Return.

  1. If , then:

  1. Push the value to the stack.

  2. Push the value to the stack.

  3. Execute the instruction .

  4. Execute the instruction .

  5. Assert: due to the earlier check against the table size, .

  6. Push the value to the stack.

  7. Assert: due to the earlier check against the table size, .

  8. Push the value to the stack.

  1. Else:

  1. Assert: due to the earlier check against the table size, .

  2. Push the value to the stack.

  3. Assert: due to the earlier check against the table size, .

  4. Push the value to the stack.

  1. Execute the instruction .

  1. Execute the instruction .

  2. Push the value to the stack.

  3. Push the value to the stack.

  1. Push the value to the stack.

  2. Execute the instruction .

4.4.6.7.
  1. Let be the current frame.

  2. Assert: due to validation, exists.

  3. Let be the table address .

  4. Assert: due to validation, exists.

  5. Let be the table instance .

  6. Assert: due to validation, exists.

  7. Let be the element address .

  8. Assert: due to validation, exists.

  9. Let be the element instance .

  10. Assert: due to validation, a value of value type is on the top of the stack.

  11. Pop the value from the stack.

  12. Assert: due to validation, a value of value type is on the top of the stack.

  13. Pop the value from the stack.

  14. Assert: due to validation, a value of value type is on the top of the stack.

  15. Pop the value from the stack.

  16. If is larger than the length of or is larger than the length of , then:

    1. Trap.

  17. If , then:

    1. Return.

  18. Let be the reference value .

  19. Push the value to the stack.

  20. Push the value to the stack.

  21. Execute the instruction .

  22. Assert: due to the earlier check against the table size, .

  23. Push the value to the stack.

  24. Assert: due to the earlier check against the segment size, .

  25. Push the value to the stack.

  26. Push the value to the stack.

  27. Execute the instruction .

4.4.6.8.
  1. Let be the current frame.

  2. Assert: due to validation, exists.

  3. Let be the element address .

  4. Assert: due to validation, exists.

  5. Replace with .

4.4.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.4.7.1. and
  1. Let be .

  2. Let be the current frame.

  3. Assert: due to validation, exists.

  4. Let be the memory address .

  5. Assert: due to validation, exists.

  6. Let be the memory instance .

  7. Assert: due to validation, a value of value type is on the top of the stack.

  8. Pop the value from the stack.

  9. Let be the integer .

  10. If is not part of the instruction, then:

  1. Let be the bit width of number type .

  1. If both is and modulo is not equal to , then:

  1. Trap.

  1. If is , then:

    1. If is larger than the length of , then:

      1. Trap.

    2. Let be the byte sequence .

  2. Else:

    1. Perform the action to read the length of the shared memory instance at memory address .

    2. If is larger than , then:

      1. Trap.

    3. Let be .

    4. Perform the action to read bytes from data offset of the shared memory instance at memory address .

  3. Let be the integer for which .

  4. Let be the result of computing .

  5. Push the value to the stack.

4.4.7.2.
  1. Let be .

  2. Let be the current frame.

  3. Assert: due to validation, exists.

  4. Let be the memory address .

  5. Assert: due to validation, exists.

  6. Let be the memory instance .

  7. Assert: due to validation, a value of value type is on the top of the stack.

  8. Pop the value from the stack.

  9. Let be the integer .

  10. If is , then:

  1. If is larger than the length of , then:

    1. Trap.

  2. Let be the byte sequence .

  1. Else:

    1. Perform the action to read the length of the shared memory instance at memory address .

    2. If is larger than , then:

      1. Trap.

    3. Perform the action to read bytes from data offset of the shared memory instance at memory address .

  2. Let be the integer for which .

  3. Let be the integer .

  4. Let be the result of computing .

  5. Let be the result of computing .

  6. Push the value to the stack.

4.4.7.3.
  1. Let be .

  2. Let be the current frame.

  3. Assert: due to validation, exists.

  4. Let be the memory address .

  5. Assert: due to validation, exists.

  6. Let be the memory instance .

  7. Assert: due to validation, a value of value type is on the top of the stack.

  8. Pop the value from the stack.

  9. Let be the integer .

  10. If is , then:

  1. If is larger than the length of , then:

    1. Trap.

  2. Let be the byte sequence .

  1. Else:

    1. Perform the action to read the length of the shared memory instance at memory address .

    2. If is larger than , then:

      1. Trap.

    3. Perform the action to read bytes from data offset of the shared memory instance at memory address .

  2. Let be the integer for which .

  3. Let be the integer .

  4. Let be the result of computing .

  5. Push the value to the stack.

4.4.7.4.
  1. Let be .

  2. Let be the current frame.

  3. Assert: due to validation, exists.

  4. Let be the memory address .

  5. Assert: due to validation, exists.

  6. Let be the memory instance .

  7. Assert: due to validation, a value of value type is on the top of the stack.

  8. Pop the value from the stack.

  9. Let be the integer .

  10. If is , then:

  1. If is larger than the length of , then:

    1. Trap.

  2. Let be the byte sequence .

  1. Else:

    1. Perform the action to read the length of the shared memory instance at memory address .

    2. If is larger than , then:

      1. Trap.

    3. Perform the action