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

CHAPTER

Execution

4.1 Conventions

WebAssembly code is

executed

when

instantiating

a module or

invoking

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.

Note:

As with validation, the prose and formal rules are equivalent, so that understanding of the formal notation

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

ventions 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

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.

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.

https://dl.acm.org/citation.cfm?doid=3062341.3062363

• 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 instruc-

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

The formal execution rules use a standard approach for specifying operational semantics, rendering them into

reduction rules

. Every rule has the following general form:

configuration

→

configuration

configuration

is a syntactic description of a program state. Each rule specifies one

step

of execution. As long

as there is at most one reduction rule applicable to a given configuration, reduction – and thereby execution – is

deterministic

. WebAssembly has only very few exceptions to this, which are noted explicitly in this specification.

For WebAssembly, a configuration typically is a tuple

(

𝑆

;

𝐹

;

instr

)

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

const

instructions, and a sequence of

const

instructions can be interpreted as an operand “stack” that grows to the right.

Note:

For example, the

reduction rule

for the

i32

add

instruction can be given as follows:

(

i32

const

𝑛

) (

i32

const

𝑛

)

(

𝑛

) mod 2

)

Per this rule, two

const

instructions and the

add

instruction itself are removed from the instruction stream and

replaced with one new

const

instruction. This can be interpreted as popping two value off the stack and pushing

the result.
When no result is produced, an instruction reduces to the empty sequence:

𝜖

and

are similarly

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

const

instructions, which can be interpreted as the

values

of the resulting operand stack, or if a

trap

occurred.

For example: Benjamin Pierce.

Types and Programming Languages

. The MIT Press 2002

https://www.cis.upenn.edu/~bcpierce/tapl/

Chapter 4. Execution

Note:

For example, the following instruction sequence,

(

f64

const

𝑥

) (

f64

const

𝑥

)

𝑥

)

f64

add f64

mul

terminates after three steps:

(

f64

const

𝑥

) (

f64

const

𝑥

)

𝑥

)

𝑥

) (

f64

const

𝑥

) (

f64

const

𝑥

)

𝑥

) (

f64

const

𝑥

)

𝑥

)

where

𝑥

−

𝑥

and

𝑥

−

𝑥

and

𝑥

(

−

𝑥

)

4.2 Runtime Structure

Store

stack

, and other

runtime structure

forming the WebAssembly abstract machine, such as

values

module

instances

, are made precise in terms of additional auxiliary syntax.

4.2.1 Values

WebAssembly computations manipulate

values

of either the four basic

, i.e.,

and

of 32 or 64 bit width each, of

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

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.

::=

vec

::=

::=

𝑡

ref

extern

::=

vec

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

and null for

(

𝑡

𝑡

(

𝑡

reftype

)

4.2. Runtime Structure

Convention

• The meta variable

𝑟

ranges over reference values where clear from context.

4.2.2 Results

result

is the outcome of a computation. It is either a sequence of

or a

::=

Note:

In the current version of WebAssembly, a result can consist of at most one value.

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

, and

, and

that have been

during the life time of the abstract machine.

It is an invariant of the semantics that no element or data instance is

addressed

from anywhere else but the owning

module instances.
Syntactically, the store is defined as a

record

listing the existing instances of each category:

store

::=

{

}

Convention

• The meta variable

𝑆

ranges over stores where clear from context.

4.2.4 Addresses

, and

, and

in the

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

addr

::=

. . .

::=

::=

::=

::=

::=

::=

::=

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

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.

Chapter 4. Execution

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

memaddr

denotes the abstract

address

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 Module Instances

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.

moduleinst

::=

{

}

Each component references runtime instances corresponding to respective declarations from the original module

– whether imported or defined – in the order of their static

, and

are referenced with an indirection through their respective

addresses

in the

store

It is an invariant of the semantics that all

export instances

in a given module instance have different

names

4.2.6 Function Instances

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.

::=

::=

. . .

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

table instance

is the runtime representation of a

table

. It records its

type

and holds a vector of

::=

}

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

tabletype

. It also

is an invariant that the length of the element vector never exceeds the maximum size of

tabletype

, if present.

4.2. Runtime Structure

4.2.8 Memory Instances

memory instance

is the runtime representation of a linear

memory

. It records its

type

and holds a vector of

::=

}

The length of the vector always is a multiple of the WebAssembly

page size

, which is defined to be the constant

65536

– abbreviated

64 Ki

The bytes can be mutated through

memory instructions

, the execution of an active

data segment

, or by external

means provided by the

embedder

It is an invariant of the semantics that the length of the byte vector, divided by page size, never exceeds the maximum

size of

memtype

, if present.

4.2.9 Global Instances

global instance

is the runtime representation of a

global

variable. It records its

type

and holds an individual

::=

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

globaltype

4.2.10 Element Instances

element instance

is the runtime representation of an

element segment

. It holds a vector of references and their

common

::=

}

4.2.11 Data Instances

data instance

is the runtime representation of a

data segment

. It holds a vector of

::=

}

4.2.12 Export Instances

export instance

is the runtime representation of an

export

. It defines the export’s

and the associated

::=

Chapter 4. Execution

4.2.13 External Values

external value

is the runtime representation of an entity that can be imported or exported. It is an

denoting either a

, or

in the shared

::=

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

Besides the

store

, most

instructions

interact with an implicit

stack

. The stack contains three kinds of entries:

•

Values

: the

operands

of instructions.

•

Labels

: active

structured control instructions

that can be targeted by branches.

•

Activations

: the

call frames

of active

function

calls.

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.

Values

Values are represented by

themselves

Labels

Labels carry an argument arity

𝑛

and their associated branch

target

, which is expressed syntactically as an

sequence:

::=

}

Intuitively,

instr

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

. . .

4.2. Runtime Structure

When performing a branch to this label, this executes the loop, effectively restarting it from the beginning. Con-

versely, a simple block label has the form

label

𝑛

{

𝜖

}

When branching, the empty continuation ends the targeted block, such that execution can proceed with consecutive

instructions.

Activations and Frames

Activation frames carry the return arity

𝑛

of the respective function, hold the values of its

locals

(including ar-

guments) in the order corresponding to their static

local indices

, and a reference to the function’s own

module

instance

activation

::=

::=

The values of the locals are mutated by respective

variable instructions

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

instr

::=

. . .

trap

ref

funcaddr

ref

extern

}

The

instruction represents the occurrence of a trap. Traps are bubbled up through nested instruction sequences,

ultimately reducing the entire program to a single

trap

instruction, signalling abrupt termination.

The

ref

instruction represents

function reference values

. Similarly,

ref

extern

represents

external references

The

invoke

instruction represents the imminent invocation of a

function instance

, identified by its

address

. It unifies

the handling of different forms of calls.
The

label

and

frame

instructions model

labels

and

frames “on the stack”

. Moreover, the administrative syntax

maintains the nesting structure of the original

structured control instruction

function body

and their

instruction

Chapter 4. Execution

sequences

with an

end

marker. That way, the end of the inner instruction sequence is known when part of an outer

sequence.

Note:

For example, the

reduction rule

for

block

is:

block

[

𝑡

𝑛

]

{

𝜖

}

instr

end

This replaces the block with a label instruction, which can be interpreted as “pushing” the label on the stack. When

end

is reached, i.e., the inner instruction sequence has been reduced to the empty sequence – or rather, a sequence

𝑛

const

instructions representing the resulting values – then the

label

instruction is eliminated courtesy of its

own

}

This can be interpreted as removing the label from the stack and only leaving the locally accumulated operand

values.

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:

𝐵

::=

val

[

]

::=

}

This definition allows to index active labels surrounding a

branch

return

instruction.

Note:

For example, the

reduction

of a simple branch can be defined as follows:

}

𝑙

]

end

→

instr

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

label

instructions that must be hopped

over – which is exactly the count encoded in the index of a block context.

Configurations

configuration

consists of the current

store

and an executing

thread

A thread is a computation over

instructions

that operates relative to a current

frame

referring to the

module instance

in which the computation runs, i.e., where the current function originates from.

::=

::=

Note:

The current version of WebAssembly is single-threaded, but configurations with multiple threads may be

supported in the future.

4.2. Runtime Structure

Evaluation Contexts

Finally, the following definition of

evaluation context

and associated structural rules enable reduction inside in-

struction sequences and administrative forms as well as the propagation of traps:

𝐸

::=

[

]

𝐸

}

𝐸

end

𝑆

;

𝐹

;

𝐸

[

instr

]

→

𝑆

′

;

𝐹

′

;

𝐸

[

instr

′*

]

(

𝑆

;

𝐹

;

instr

→

𝑆

′

;

𝐹

′

;

instr

′*

)

𝑆

;

𝐹

;

frame

𝑛

{

𝐹

′

}

instr

end

→

𝑆

′

;

𝐹

;

frame

𝑛

{

𝐹

′′

}

instr

′*

end

(

𝑆

;

𝐹

′

;

instr

→

𝑆

′

;

𝐹

′′

;

instr

′*

)

𝑆

;

𝐹

;

𝐸

𝑆

;

𝐹

;

trap

(

𝐸

= [

])

𝑆

;

𝐹

;

frame

𝑛

{

𝐹

′

}

trap end

→

𝑆

;

𝐹

;

trap

Reduction terminates when a thread’s instruction sequence has been reduced to a

result

, that is, either a sequence

values

or to a

trap

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.

(

f64

const

𝑥

) (

f64

const

𝑥

)

𝑥

)

f64

add f64

mul

This can be decomposed into

𝐸

[(

f64

const

𝑥

)

f64

neg

]

where

𝐸

= (

f64

const

𝑥

) [

] (

f64

const

𝑥

)

f64

add f64

mul

Moreover, this is the

only

possible choice of evaluation context where the contents of the hole matches the left-hand

side of a reduction rule.

4.3 Numerics

Numeric primitives are defined in a generic manner, by operators indexed over a bit width

𝑁

Some operators are

non-deterministic

, because they can return one of several possible results (such as different

NaN

values). Technically, each operator thus returns a

set

of allowed values. For convenience, deterministic results are

expressed as plain values, which are assumed to be identified with a respective singleton set.
Some operators are

partial

, because they are not defined on certain inputs. Technically, an empty set of results is

returned for these inputs.
In formal notation, each operator is defined by equational clauses that apply in decreasing order of precedence.

That is, the first clause that is applicable to the given arguments defines the result. In some cases, similar clauses

are combined into one by using the notation

∓

. 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

fcopysign

operator is defined as follows:

fcopysign

𝑁

(

𝑝

)

𝑝

fcopysign

𝑁

(

𝑝

∓

𝑝

)

∓

𝑝

This definition is to be read as a shorthand for the following expansion of each clause into two separate ones:

fcopysign

𝑁

𝑝

)

𝑝

fcopysign

𝑁

(

−

𝑝

−

𝑝

)

−

𝑝

fcopysign

𝑁

𝑝

−

𝑝

)

−

𝑝

fcopysign

𝑁

(

−

𝑝

)

𝑝

Chapter 4. Execution

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.

𝑜𝑝

(

𝑐

𝑛

, . . . , 𝑐

𝑛
𝑘

)

𝑜𝑝

(

𝑐

𝑛

[0]

, . . . , 𝑐

𝑛
𝑘

[0])

. . . 𝑜𝑝

(

𝑐

𝑛

[

𝑛

−

, . . . , 𝑐

𝑛
𝑘

[

𝑛

−

1])

Note:

For example, the unary operator

fabs

, when given a sequence of floating-point values, return a sequence of

floating-point results:

fabs

𝑁

(

𝑧

𝑛

)

fabs

𝑁

(

𝑧

[0])

. . .

fabs

𝑁

(

𝑧

[

𝑛

])

The binary operator

iadd

, when given two sequences of integers of the same length,

𝑛

, return a sequence of integer

results:

iadd

𝑁

(

𝑖

𝑛

, 𝑖

𝑛

)

iadd

𝑁

(

𝑖

[0]

, 𝑖

[0])

. . .

iadd

𝑁

(

𝑖

[

𝑛

]

, 𝑖

[

𝑛

])

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

nan

and

∞

• The meta variable

𝑞

is used to range over (signless)

rational

magnitudes

, excluding

nan

∞

• The notation

𝑓

−

denotes the inverse of a bijective function

𝑓

• Truncation of rational values is written

trunc

(

𝑞

)

, with the usual mathematical definition:

trunc

(

𝑞

)

𝑖

(

𝑖

∈

∧

𝑞

−

< 𝑖

≤

𝑞

)

• Saturation of integers is written

sat

𝑁

(

𝑖

)

and

sat

𝑁

(

𝑖

)

. The arguments to these two functions range over

arbitrary signed integers.

–

Unsigned saturation,

sat

𝑁

(

𝑖

)

clamps

𝑖

to between

and

𝑁

−

sat

𝑁

(

𝑖

)

𝑁

−

(

𝑖 >

𝑁

−

sat

𝑁

(

𝑖

)

(

𝑖 <

sat

𝑁

(

𝑖

)

𝑖

(

otherwise

)

–

Signed saturation,

sat

𝑁

(

𝑖

)

clamps

𝑖

to between

−

𝑁

−

and

𝑁

−

sat

𝑁

(

𝑖

)

signed

−

𝑁

(

−

𝑁

−

)

(

𝑖 <

−

𝑁

−

)

sat

𝑁

(

𝑖

)

signed

−

𝑁

−

(

𝑖 >

𝑁

−

sat

𝑁

(

𝑖

)

𝑖

(

otherwise

)

4.3.1 Representations

Numbers have an underlying binary representation as a sequence of bits:

bits

𝑁

(

𝑖

)

ibits

𝑁

(

𝑖

)

bits

𝑁

(

𝑧

)

fbits

𝑁

(

𝑧

)

Each of these functions is a bijection, hence they are invertible.

4.3. Numerics

Integers

Integers

are represented as base two unsigned numbers:

ibits

𝑁

(

𝑖

)

𝑑

𝑁

−

. . . 𝑑

(

𝑖

= 2

𝑁

−

𝑑

𝑁

−

· · ·

+ 2

𝑑

)

Boolean operators like

∧

∨

, or

are lifted to bit sequences of equal length by applying them pointwise.

Floating-Point

Floating-point values

are represented in the respective binary format defined by

IEEE 754-2019

(Section 3.4):

fbits

𝑁

(

(1 +

𝑚

−

𝑀

)

𝑒

)

)

(

𝑒

)

(

𝑚

)

fbits

𝑁

(

(0 +

𝑚

−

𝑀

)

𝑒

)

fsign

(

) (0)

𝐸

ibits

𝑀

(

𝑚

)

fbits

𝑁

(

±∞

)

fsign

(

) (1)

𝐸

(0)

𝑀

(

𝑛

))

fsign

(

) (1)

𝐸

ibits

𝑀

(

𝑛

)

fbias

𝑁

𝐸

−

−

)

where

𝑀

signif

(

𝑁

)

and

𝐸

expon

(

𝑁

)

Storage

When a number is stored into

memory

, it is converted into a sequence of

byte order:

(

𝑖

)

(

𝑖

))

littleendian

(

𝜖

)

𝜖

littleendian

(

𝑑

′*

)

littleendian

(

𝑑

′*

)

ibits

−

(

𝑑

)

Again these functions are invertable bijections.

Vectors

Numeric vectors have the same underlying representation as an

i128

. They can also be interpreted as a sequence

of numeric values packed into a

with a particular

𝑁

(

𝑐

)

𝑐

. . . 𝑐

𝑁

−

(

where

𝐵

𝑡

∧

𝑏

𝑏𝑦𝑡𝑒𝑠

i128

(

𝑐

)

∧

𝑐

𝑖

bytes

−

𝑡

(

𝑏

[

𝑖

𝐵

]))

These functions are bijections, so they are invertible.

4.3.2 Integer Operations

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

signed

𝑁

(

𝑖

)

𝑖

≤

𝑖 <

𝑁

−

)

signed

𝑁

(

𝑖

)

𝑖

−

𝑁

−

≤

𝑖 <

𝑁

)

This function is bijective, and hence invertible.

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

https://en.wikipedia.org/wiki/Endianness#Little-endian

Chapter 4. Execution

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

depending on a condition.

bool

(

𝐶

)

(

𝐶

)

bool

(

𝐶

)

(

otherwise

)

iadd

𝑁

(

𝑖

, 𝑖

)

• Return the result of adding

𝑖

and

𝑖

modulo

𝑁

iadd

𝑁

(

𝑖

, 𝑖

)

(

𝑖

) mod 2

𝑁

isub

𝑁

(

𝑖

, 𝑖

)

• Return the result of subtracting

𝑖

from

𝑖

modulo

𝑁

isub

𝑁

(

𝑖

, 𝑖

)

(

𝑖

−

𝑖

+ 2

𝑁

) mod 2

𝑁

imul

𝑁

(

𝑖

, 𝑖

)

• Return the result of multiplying

𝑖

and

𝑖

modulo

𝑁

imul

𝑁

(

𝑖

, 𝑖

)

(

𝑖

) mod 2

𝑁

idiv

𝑁

(

𝑖

, 𝑖

)

• If

𝑖

, then the result is undefined.

• Else, return the result of dividing

𝑖

, truncated toward zero.

idiv

𝑁

(

𝑖

{}

idiv

𝑁

(

𝑖

, 𝑖

)

trunc

(

𝑖

/𝑖

)

Note:

This operator is

partial

idiv

𝑁

(

𝑖

, 𝑖

)

• Let

𝑗

be the

signed interpretation

𝑖

• Let

𝑗

be the

signed interpretation

𝑖

• If

𝑗

, then the result is undefined.

• Else if

𝑗

divided by

𝑗

𝑁

−

, then the result is undefined.

• Else, return the result of dividing

𝑗

, truncated toward zero.

idiv

𝑁

(

𝑖

{}

idiv

𝑁

(

𝑖

, 𝑖

)

{}

(

signed

𝑁

(

𝑖

)

signed

𝑁

(

𝑖

) = 2

𝑁

−

)

idiv

𝑁

(

𝑖

, 𝑖

)

(

𝑖

)

signed

𝑁

(

𝑖

)))

Note:

This operator is

partial

. Besides division by

, the result of

(

−

𝑁

−

)

(

−

1) = +2

𝑁

−

is not representable

as an

𝑁

-bit signed integer.

4.3. Numerics

irem

𝑁

(

𝑖

, 𝑖

)

• If

𝑖

, then the result is undefined.

• Else, return the remainder of dividing

𝑖

irem

𝑁

(

𝑖

{}

irem

𝑁

(

𝑖

, 𝑖

)

𝑖

−

𝑖

trunc

(

𝑖

/𝑖

)

Note:

This operator is

partial

As long as both operators are defined, it holds that

𝑖

idiv

(

𝑖

, 𝑖

) +

irem

(

𝑖

, 𝑖

)

irem

𝑁

(

𝑖

, 𝑖

)

• Let

𝑗

be the

signed interpretation

𝑖

• Let

𝑗

be the

signed interpretation

𝑖

• If

𝑖

, then the result is undefined.

• Else, return the remainder of dividing

𝑗

, with the sign of the dividend

𝑗

irem

𝑁

(

𝑖

{}

irem

𝑁

(

𝑖

, 𝑖

)

signed

−

𝑁

(

𝑗

−

𝑗

trunc

(

𝑗

/𝑗

))

(

where

𝑗

signed

𝑁

(

𝑖

)

∧

𝑗

signed

𝑁

(

𝑖

))

Note:

This operator is

partial

As long as both operators are defined, it holds that

𝑖

idiv

(

𝑖

, 𝑖

) +

irem

(

𝑖

, 𝑖

)

inot

𝑁

(

𝑖

)

• Return the bitwise negation of

𝑖

inot

𝑁

(

𝑖

)

(

𝑖

)

ibits

𝑁

−

1))

iand

𝑁

(

𝑖

, 𝑖

)

• Return the bitwise conjunction of

𝑖

and

𝑖

iand

𝑁

(

𝑖

, 𝑖

)

(

𝑖

)

∧

ibits

𝑁

(

𝑖

))

iandnot

𝑁

(

𝑖

, 𝑖

)

• Return the bitwise conjunction of

𝑖

and the bitwise negation of

𝑖

iandnot

𝑁

(

𝑖

, 𝑖

)

iand

𝑁

(

𝑖

inot

𝑁

(

𝑖

2))

Chapter 4. Execution

ior

𝑁

(

𝑖

, 𝑖

)

• Return the bitwise disjunction of

𝑖

and

𝑖

ior

𝑁

(

𝑖

, 𝑖

)

(

𝑖

)

∨

ibits

𝑁

(

𝑖

))

ixor

𝑁

(

𝑖

, 𝑖

)

• Return the bitwise exclusive disjunction of

𝑖

and

𝑖

ixor

𝑁

(

𝑖

, 𝑖

)

(

𝑖

)

ibits

𝑁

(

𝑖

))

ishl

𝑁

(

𝑖

, 𝑖

)

• Let

𝑘

𝑖

modulo

𝑁

• Return the result of shifting

𝑖

left by

𝑘

bits, modulo

𝑁

ishl

𝑁

(

𝑖

, 𝑖

)

ibits

−

𝑁

(

𝑑

𝑁

−

𝑘

)

(

ibits

𝑁

(

𝑖

) =

𝑑

𝑘

𝑑

𝑁

−

𝑘

∧

𝑘

𝑖

mod

𝑁

)

ishr

𝑁

(

𝑖

, 𝑖

)

• Let

𝑘

𝑖

modulo

𝑁

• Return the result of shifting

𝑖

right by

𝑘

bits, extended with

bits.

ishr

𝑁

(

𝑖

, 𝑖

)

ibits

−

𝑁

𝑘

𝑑

𝑁

−

𝑘

)

(

ibits

𝑁

(

𝑖

) =

𝑑

𝑁

−

𝑘

𝑑

𝑘

∧

𝑘

𝑖

mod

𝑁

)

ishr

𝑁

(

𝑖

, 𝑖

)

• Let

𝑘

𝑖

modulo

𝑁

• Return the result of shifting

𝑖

right by

𝑘

bits, extended with the most significant bit of the original value.

ishr

𝑁

(

𝑖

, 𝑖

)

ibits

−

𝑁

(

𝑑

𝑘

𝑑

𝑁

−

𝑘

−

)

(

ibits

𝑁

(

𝑖

) =

𝑑

𝑁

−

𝑘

−

𝑑

𝑘

∧

𝑘

𝑖

mod

𝑁

)

irotl

𝑁

(

𝑖

, 𝑖

)

• Let

𝑘

𝑖

modulo

𝑁

• Return the result of rotating

𝑖

left by

𝑘

bits.

irotl

𝑁

(

𝑖

, 𝑖

)

ibits

−

𝑁

(

𝑑

𝑁

−

𝑘

𝑑

𝑘

)

(

ibits

𝑁

(

𝑖

) =

𝑑

𝑘

𝑑

𝑁

−

𝑘

∧

𝑘

𝑖

mod

𝑁

)

irotr

𝑁

(

𝑖

, 𝑖

)

• Let

𝑘

𝑖

modulo

𝑁

• Return the result of rotating

𝑖

right by

𝑘

bits.

irotr

𝑁

(

𝑖

, 𝑖

)

ibits

−

𝑁

(

𝑑

𝑘

𝑑

𝑁

−

𝑘

)

(

ibits

𝑁

(

𝑖

) =

𝑑

𝑁

−

𝑘

𝑑

𝑘

∧

𝑘

𝑖

mod

𝑁

)

4.3. Numerics

iclz

𝑁

(

𝑖

)

• Return the count of leading zero bits in

𝑖

; all bits are considered leading zeros if

𝑖

iclz

𝑁

(

𝑖

)

𝑘

(

ibits

𝑁

(

𝑖

) = 0

𝑘

𝑑

)

ictz

𝑁

(

𝑖

)

• Return the count of trailing zero bits in

𝑖

; all bits are considered trailing zeros if

𝑖

ictz

𝑁

(

𝑖

)

𝑘

(

ibits

𝑁

(

𝑖

) = (

𝑑

𝑘

)

ipopcnt

𝑁

(

𝑖

)

• Return the count of non-zero bits in

𝑖

ipopcnt

𝑁

(

𝑖

)

𝑘

(

ibits

𝑁

(

𝑖

) = (0

𝑘

)

ieqz

𝑁

(

𝑖

)

• Return

𝑖

is zero,

otherwise.

ieqz

𝑁

(

𝑖

)

bool

(

𝑖

= 0)

ieq

𝑁

(

𝑖

, 𝑖

)

• Return

𝑖

equals

𝑖

otherwise.

ieq

𝑁

(

𝑖

, 𝑖

)

bool

(

𝑖

)

ine

𝑁

(

𝑖

, 𝑖

)

• Return

𝑖

does not equal

𝑖

otherwise.

ine

𝑁

(

𝑖

, 𝑖

)

bool

(

𝑖

)

ilt

𝑁

(

𝑖

, 𝑖

)

• Return

𝑖

is less than

𝑖

otherwise.

ilt

𝑁

(

𝑖

, 𝑖

)

bool

(

𝑖

< 𝑖

)

ilt

𝑁

(

𝑖

, 𝑖

)

• Let

𝑗

be the

signed interpretation

𝑖

• Let

𝑗

be the

signed interpretation

𝑖

• Return

𝑗

is less than

𝑗

otherwise.

ilt

𝑁

(

𝑖

, 𝑖

)

(

𝑖

)

signed

𝑁

(

𝑖

))

Chapter 4. Execution

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