WebAssembly Specification Release 1.1 (Draft 2021-12-18) - page 2

1.1.4 Dependencies

WebAssembly depends on two existing standards:

•

IEEE 754-2019

4

, for the representation of

floating-point data

and the semantics of respective

numeric oper-

ations

.

•

Unicode

5

, for the representation of import/export

names

and the

text format

.

However, to make this specification self-contained, relevant aspects of the aforementioned standards are defined

and formalized as part of this specification, such as the

binary representation

and

rounding

of floating-point values,

and the

value range

and

UTF-8 encoding

of Unicode characters.

Note:

The aforementioned standards are the authoritative source of all respective definitions. Formalizations

given in this specification are intended to match these definitions. Any discrepancy in the syntax or semantics

described is to be considered an error.

1.2 Overview

1.2.1 Concepts

WebAssembly encodes a low-level, assembly-like programming language. This language is structured around the

following concepts.

Values

WebAssembly provides only four basic

number types

. These are integers and

IEEE 754-2019

6

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

7

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

8

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.

4

https://ieeexplore.ieee.org/document/8766229

5

https://www.unicode.org/versions/latest/

6

https://ieeexplore.ieee.org/document/8766229

7

https://ieeexplore.ieee.org/document/8766229

8

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

3

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

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

, speci-

fying 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 environ-

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

4

Chapter 1. Introduction

CHAPTER

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:

i32

,

end

.

• Nonterminal symbols are written in italic font:

valtype

,

instr

.

•

𝐴

𝑛

is a sequence of

𝑛

≥

0

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

𝑛

≥

1

.)

•

𝐴

?

is an optional occurrence of

𝐴

. (This is a shorthand for

𝐴

𝑛

where

𝑛

≤

1

.)

• Productions are written

sym

::=

𝐴

1

|

. . .

|

𝐴

𝑛

.

• Large productions may be split into multiple definitions, indicated by ending the first one with explicit el-

lipses,

sym

::=

𝐴

1

|

. . .

, and starting continuations with ellipses,

sym

::=

. . .

|

𝐴

2

.

• Some productions are augmented with side conditions in parentheses, “

(

if

condition

)

”, that provide a short-

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

5

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

0

.

•

𝑠

[

𝑖

:

𝑛

]

denotes the sub-sequence

𝑠

[

𝑖

]

. . . 𝑠

[

𝑖

+

𝑛

−

1]

of a sequence

𝑠

.

•

𝑠

with

[

𝑖

] =

𝐴

denotes the same sequence as

𝑠

, except that the

𝑖

-th element is replaced with

𝐴

.

•

𝑠

with

[

𝑖

:

𝑛

] =

𝐴

𝑛

denotes the same sequence as

𝑠

, except that the sub-sequence

𝑠

[

𝑖

:

𝑛

]

is replaced with

𝐴

𝑛

.

•

concat

(

𝑠

*

)

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

(

𝐴

1

𝑥 𝐴

2

)

𝑛

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

field

𝑖

to “values”

𝐴

𝑖

,

respectively:

r

::=

{

field

1

𝐴

1

,

field

2

𝐴

2

, . . .

}

The following notation is adopted for manipulating such records:

•

𝑟.

field

denotes the contents of the

field

component of

𝑟

.

•

𝑟

with

field

=

𝐴

denotes the same record as

𝑟

, except that the contents of the

field

component is replaced

with

𝐴

.

•

𝑟

1

⊕

𝑟

2

denotes the composition of two records with the same fields of sequences by appending each sequence

point-wise:

{

field

1

𝐴

*

1

,

field

2

𝐴

*

2

, . . .

}

⊕

{

field

1

𝐵

*

1

,

field

2

𝐵

*

2

, . . .

}

=

{

field

1

𝐴

*

1

𝐵

*

1

,

field

2

𝐴

*

2

𝐵

*

2

, . . .

}

•

⨁︀

𝑟

*

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”

pth

::= ([

. . .

]

|

.

field

)

+

:

•

𝑠

with

[

𝑖

]

pth

=

𝐴

is short for

𝑠

with

[

𝑖

] = (

𝑠

[

𝑖

]

with

pth

=

𝐴

)

.

•

𝑟

with

field

pth

=

𝐴

is short for

𝑟

with

field

= (

𝑟.

field

with

pth

=

𝐴

)

.

where

𝑟

with

.

field

=

𝐴

is shortened to

𝑟

with

field

=

𝐴

.

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

2

32

−

1

elements.

vec

(

𝐴

)

::=

𝐴

𝑛

(

if

𝑛 <

2

32

)

6

Chapter 2. Structure

• Each

export instance

exportinst

𝑖

in

moduleinst

.

exports

must be

valid

.

• For each

export instance

exportinst

𝑖

in

moduleinst

.

exports

, the

name

exportinst

𝑖

.

name

must be different

from any other name occurring in

moduleinst

.

exports

.

• Let

functype

′*

be the concatenation of all

functype

′

𝑖

in order.

• Let

tabletype

*

be the concatenation of all

tabletype

𝑖

in order.

• Let

memtype

*

be the concatenation of all

memtype

𝑖

in order.

• Let

globaltype

*

be the concatenation of all

globaltype

𝑖

in order.

• Then the module instance is valid with

context

{

types

functype

*

,

funcs

functype

′*

,

tables

tabletype

*

,

mems

memtype

*

,

globals

globaltype

*

}

.

(

⊢

functype

ok

)

*

(

𝑆

⊢

func

funcaddr

:

func

functype

′

)

*

(

𝑆

⊢

table

tableaddr

:

table

tabletype

)

*

(

𝑆

⊢

mem

memaddr

:

mem

memtype

)

*

(

𝑆

⊢

global

globaladdr

:

global

globaltype

)

*

(

𝑆

⊢

𝑆.

elems

[

elemaddr

]

ok

)

*

(

𝑆

⊢

𝑆.

datas

[

dataaddr

]

ok

)

*

(

𝑆

⊢

exportinst

ok

)

*

(

exportinst

.

name

)

*

disjoint

𝑆

⊢

{

types

functype

*

,

funcaddrs

funcaddr

*

,

tableaddrs

tableaddr

*

,

memaddrs

memaddr

*

,

globaladdrs

globaladdr

*

,

elemaddrs

elemaddr

*

,

dataaddrs

dataaddr

*

,

exports

exportinst

*

}

:

{

types

functype

*

,

funcs

functype

′*

,

tables

tabletype

*

,

mems

memtype

*

,

globals

globaltype

*

}

7.5.3 Configuration Validity

To relate the WebAssembly

type system

to its

execution semantics

, the

typing rules for instructions

must be extended

to

configurations

𝑆

;

𝑇

, which relates the

store

to execution

threads

.

Configurations and threads are classified by their

result type

. In addition to the store

𝑆

, threads are typed under a

return type

resulttype

?

, which controls whether and with which type a

return

instruction is allowed. This type is

absent (

𝜖

) except for instruction sequences inside an administrative

frame

instruction.

Finally,

frames

are classified with

frame contexts

, which extend the

module contexts

of a frame’s associated

module

instance

with the

locals

that the frame contains.

Configurations

𝑆

;

𝑇

• The

store

𝑆

must be

valid

.

• Under no allowed return type, the

thread

𝑇

must be

valid

with some

result type

[

𝑡

*

]

.

• Then the configuration is valid with the

result type

[

𝑡

*

]

.

⊢

𝑆

ok

𝑆

;

𝜖

⊢

𝑇

: [

𝑡

*

]

⊢

𝑆

;

𝑇

: [

𝑡

*

]

Threads

𝐹

;

instr

*

• Let

resulttype

?

be the current allowed return type.

• The

frame

𝐹

must be

valid

with a

context

𝐶

.

• Let

𝐶

′

be the same

context

as

𝐶

, but with

return

set to

resulttype

?

.

• Under context

𝐶

′

, the instruction sequence

instr

*

must be

valid

with some type

[]

→

[

𝑡

*

]

.

• Then the thread is valid with the

result type

[

𝑡

*

]

.

𝑆

⊢

𝐹

:

𝐶

𝑆

;

𝐶,

return

resulttype

?

⊢

instr

*

: []

→

[

𝑡

*

]

𝑆

;

resulttype

?

⊢

𝐹

;

instr

*

: [

𝑡

*

]

Frames

{

locals

val

*

,

module

moduleinst

}

• The

module instance

moduleinst

must be

valid

with some

module context

𝐶

.

• Each

value

val

𝑖

in

val

*

must be

valid

with some

value type

𝑡

𝑖

.

• Let

𝑡

*

the concatenation of all

𝑡

𝑖

in order.

• Let

𝐶

′

be the same

context

as

𝐶

, but with the

value types

𝑡

*

prepended to the

locals

vector.

• Then the frame is valid with

frame context

𝐶

′

.

𝑆

⊢

moduleinst

:

𝐶

(

𝑆

⊢

val

:

𝑡

)

*

𝑆

⊢

{

locals

val

*

,

module

moduleinst

}

: (

𝐶,

locals

𝑡

*

)

7.5.4 Administrative Instructions

Typing rules for

administrative instructions

are specified as follows. In addition to the

context

𝐶

, typing of these

instructions is defined under a given

store

𝑆

. To that end, all previous typing judgements

𝐶

⊢

prop

are generalized

to include the store, as in

𝑆

;

𝐶

⊢

prop

, by implicitly adding

𝑆

to all rules –

𝑆

is never modified by the pre-existing

rules, but it is accessed in the extra rules for

administrative instructions

given below.

trap

• The instruction is valid with type

[

𝑡

*

1

]

→

[

𝑡

*

2

]

, for any sequences of

value types

𝑡

*

1

and

𝑡

*

2

.

𝑆

;

𝐶

⊢

trap

: [

𝑡

*

1

]

→

[

𝑡

*

2

]

ref

.

extern

externaddr

• The instruction is valid with type

[]

→

[

externref

]

.

𝑆

;

𝐶

⊢

ref

.

extern

externaddr

: []

→

[

externref

]

ref

funcaddr

• The

external function value

func

funcaddr

must be

valid

with

external function type

func

functype

.

• Then the instruction is valid with type

[]

→

[

funcref

]

.

𝑆

⊢

func

funcaddr

:

func

functype

𝑆

;

𝐶

⊢

ref

funcaddr

: []

→

[

funcref

]

invoke

funcaddr

• The

external function value

func

funcaddr

must be

valid

with

external function type

func

([

𝑡

*

1

]

→

[

𝑡

*

2

])

.

• Then the instruction is valid with type

[

𝑡

*

1

]

→

[

𝑡

*

2

]

.

𝑆

⊢

func

funcaddr

:

func

[

𝑡

*

1

]

→

[

𝑡

*

2

]

𝑆

;

𝐶

⊢

invoke

funcaddr

: [

𝑡

*

1

]

→

[

𝑡

*

2

]

label

𝑛

{

instr

*

0

}

instr

*

end

• The instruction sequence

instr

*

0

must be

valid

with some type

[

𝑡

𝑛

1

]

→

[

𝑡

*

2

]

.

• Let

𝐶

′

be the same

context

as

𝐶

, but with the

result type

[

𝑡

𝑛

1

]

prepended to the

labels

vector.

• Under context

𝐶

′

, the instruction sequence

instr

*

must be

valid

with type

[]

→

[

𝑡

*

2

]

.

• Then the compound instruction is valid with type

[]

→

[

𝑡

*

2

]

.

𝑆

;

𝐶

⊢

instr

*

0

: [

𝑡

𝑛

1

]

→

[

𝑡

*

2

]

𝑆

;

𝐶,

labels

[

𝑡

𝑛

1

]

⊢

instr

*

: []

→

[

𝑡

*

2

]

𝑆

;

𝐶

⊢

label

𝑛

{

instr

*

0

}

instr

*

end

: []

→

[

𝑡

*

2

]

frame

𝑛

{

𝐹

}

instr

*

end

• Under the return type

[

𝑡

𝑛

]

, the

thread

𝐹

;

instr

*

must be

valid

with

result type

[

𝑡

𝑛

]

.

• Then the compound instruction is valid with type

[]

→

[

𝑡

𝑛

]

.

𝑆

; [

𝑡

𝑛

]

⊢

𝐹

;

instr

*

: [

𝑡

𝑛

]

𝑆

;

𝐶

⊢

frame

𝑛

{

𝐹

}

instr

*

end

: []

→

[

𝑡

𝑛

]

7.5.5 Store Extension

Programs can mutate the

store

and its contained instances. Any such modification must respect certain invariants,

such as not removing allocated instances or changing immutable definitions. While these invariants are inherent

to the execution semantics of WebAssembly

instructions

and

modules

,

host functions

do not automatically adhere

to them. Consequently, the required invariants must be stated as explicit constraints on the

invocation

of host

functions. Soundness only holds when the

embedder

ensures these constraints.

The necessary constraints are codified by the notion of store

extension

: a store state

𝑆

′

extends state

𝑆

, written

𝑆

⪯

𝑆

′

, when the following rules hold.

Note:

Extension does not imply that the new store is valid, which is defined separately

above

.