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

convert

s

𝑀,𝑁

(

𝑖

)

• Let

𝑗

be the

signed interpretation

of

𝑖

.

• Return

float

𝑁

(

𝑗

)

.

convert

s

𝑀,𝑁

(

𝑖

)

=

float

𝑁

(

signed

𝑀

(

𝑖

))

reinterpret

𝑡

1

,𝑡

2

(

𝑐

)

• Let

𝑑

*

be the bit sequence

bits

𝑡

1

(

𝑐

)

.

• Return the constant

𝑐

′

for which

bits

𝑡

2

(

𝑐

′

) =

𝑑

*

.

reinterpret

𝑡

1

,𝑡

2

(

𝑐

)

=

bits

−

1

𝑡

2

(

bits

𝑡

1

(

𝑐

))

narrow

s

𝑀,𝑁

(

𝑖

)

• Let

𝑗

be the

signed interpretation

of

𝑖

of size

𝑀

.

• Return

sat

s

𝑁

(

𝑗

)

.

narrow

s

𝑀,𝑁

(

𝑖

)

=

sat

s

𝑁

(

signed

𝑀

(

𝑖

))

narrow

u

𝑀,𝑁

(

𝑖

)

• Let

𝑗

be the

signed interpretation

of

𝑖

of size

𝑀

.

• Return

sat

u

𝑁

(

𝑗

)

.

narrow

u

𝑀,𝑁

(

𝑖

)

=

sat

u

𝑁

(

signed

𝑀

(

𝑖

))

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:

op

i

𝑁

(

𝑛

1

, . . . , 𝑛

𝑘

)

=

i

op

𝑁

(

𝑛

1

, . . . , 𝑛

𝑘

)

op

f

𝑁

(

𝑧

1

, . . . , 𝑧

𝑘

)

=

f

op

𝑁

(

𝑧

1

, . . . , 𝑧

𝑘

)

And for

conversion operators

:

cvtop

sx

?

𝑡

1

,𝑡

2

(

𝑐

)

=

cvtop

sx

?

|

𝑡

1

|

,

|

𝑡

2

|

(

𝑐

)

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

i32

.

add

applied to operands

𝑖

1

, 𝑖

2

invokes

add

i32

(

𝑖

1

, 𝑖

2

)

, which maps

to the generic

iadd

32

(

𝑖

1

, 𝑖

2

)

via the above definition. Similarly,

i64

.

trunc

_

f32

_

s

applied to

𝑧

invokes

trunc

s

f32

,

i64

(

𝑧

)

,

which maps to the generic

trunc

s

32

,

64

(

𝑧

)

.

4.4. Instructions

87

𝑡.

const

𝑐

1. Push the value

𝑡.

const

𝑐

to the stack.

Note:

No formal reduction rule is required for this instruction, since

const

instructions already are

values

.

𝑡.

unop

1. Assert: due to

validation

, a value of

value type

𝑡

is on the top of the stack.

2. Pop the value

𝑡.

const

𝑐

1

from the stack.

3. If

unop

𝑡

(

𝑐

1

)

is defined, then:

a. Let

𝑐

be a possible result of computing

unop

𝑡

(

𝑐

1

)

.

b. Push the value

𝑡.

const

𝑐

to the stack.

4. Else:

a. Trap.

(

𝑡.

const

𝑐

1

)

𝑡.

unop

˓

→

(

𝑡.

const

𝑐

)

(

if

𝑐

∈

unop

𝑡

(

𝑐

1

))

(

𝑡.

const

𝑐

1

)

𝑡.

unop

˓

→

trap

(

if

unop

𝑡

(

𝑐

1

) =

{}

)

𝑡.

binop

1. Assert: due to

validation

, two values of

value type

𝑡

are on the top of the stack.

2. Pop the value

𝑡.

const

𝑐

2

from the stack.

3. Pop the value

𝑡.

const

𝑐

1

from the stack.

4. If

binop

𝑡

(

𝑐

1

, 𝑐

2

)

is defined, then:

a. Let

𝑐

be a possible result of computing

binop

𝑡

(

𝑐

1

, 𝑐

2

)

.

b. Push the value

𝑡.

const

𝑐

to the stack.

5. Else:

a. Trap.

(

𝑡.

const

𝑐

1

) (

𝑡.

const

𝑐

2

)

𝑡.

binop

˓

→

(

𝑡.

const

𝑐

)

(

if

𝑐

∈

binop

𝑡

(

𝑐

1

, 𝑐

2

))

(

𝑡.

const

𝑐

1

) (

𝑡.

const

𝑐

2

)

𝑡.

binop

˓

→

trap

(

if

binop

𝑡

(

𝑐

1

, 𝑐

2) =

{}

)

𝑡.

testop

1. Assert: due to

validation

, a value of

value type

𝑡

is on the top of the stack.

2. Pop the value

𝑡.

const

𝑐

1

from the stack.

3. Let

𝑐

be the result of computing

testop

𝑡

(

𝑐

1

)

.

4. Push the value

i32

.

const

𝑐

to the stack.

(

𝑡.

const

𝑐

1

)

𝑡.

testop

˓

→

(

i32

.

const

𝑐

)

(

if

𝑐

=

testop

𝑡

(

𝑐

1

))

88

Chapter 4. Execution

𝑡.

relop

1. Assert: due to

validation

, two values of

value type

𝑡

are on the top of the stack.

2. Pop the value

𝑡.

const

𝑐

2

from the stack.

3. Pop the value

𝑡.

const

𝑐

1

from the stack.

4. Let

𝑐

be the result of computing

relop

𝑡

(

𝑐

1

, 𝑐

2

)

.

5. Push the value

i32

.

const

𝑐

to the stack.

(

𝑡.

const

𝑐

1

) (

𝑡.

const

𝑐

2

)

𝑡.

relop

˓

→

(

i32

.

const

𝑐

)

(

if

𝑐

=

relop

𝑡

(

𝑐

1

, 𝑐

2

))

𝑡

2

.

cvtop

_

𝑡

1

_

sx

?

1. Assert: due to

validation

, a value of

value type

𝑡

1

is on the top of the stack.

2. Pop the value

𝑡

1

.

const

𝑐

1

from the stack.

3. If

cvtop

sx

?

𝑡

1

,𝑡

2

(

𝑐

1

)

is defined:

a. Let

𝑐

2

be a possible result of computing

cvtop

sx

?

𝑡

1

,𝑡

2

(

𝑐

1

)

.

b. Push the value

𝑡

2

.

const

𝑐

2

to the stack.

4. Else:

a. Trap.

(

𝑡

1

.

const

𝑐

1

)

𝑡

2

.

cvtop

_

𝑡

1

_

sx

?

˓

→

(

𝑡

2

.

const

𝑐

2

)

(

if

𝑐

2

∈

cvtop

sx

?

𝑡

1

,𝑡

2

(

𝑐

1

))

(

𝑡

1

.

const

𝑐

1

)

𝑡

2

.

cvtop

_

𝑡

1

_

sx

?

˓

→

trap

(

if

cvtop

sx

?

𝑡

1

,𝑡

2

(

𝑐

1

) =

{}

)

4.4.2 Reference Instructions

ref

.

null

𝑡

1. Push the value

ref

.

null

𝑡

to the stack.

Note:

No formal reduction rule is required for this instruction, since the

ref

.

null

instruction is already a

value

.

ref

.

is

_

null

1. Assert: due to

validation

, a

reference value

is on the top of the stack.

2. Pop the value

val

from the stack.

3. If

val

is

ref

.

null

𝑡

, then:

a. Push the value

i32

.

const

1

to the stack.

4. Else:

a. Push the value

i32

.

const

0

to the stack.

val

ref

.

is

_

null

˓

→

i32

.

const

1

(

if

val

=

ref

.

null

𝑡

)

val

ref

.

is

_

null

˓

→

i32

.

const

0

(

otherwise

)

4.4. Instructions

89

ref

.

func

𝑥

1. Let

𝐹

be the

current frame

.

2. Assert: due to

validation

,

𝐹.

module

.

funcaddrs

[

𝑥

]

exists.

3. Let

𝑎

be the

function address

𝐹.

module

.

funcaddrs

[

𝑥

]

.

4. Push the value

ref

𝑎

to the stack.

𝐹

;

ref

.

func

𝑥

˓

→

𝐹

;

ref

𝑎

(

if

𝑎

=

𝐹.

module

.

funcaddrs

[

𝑥

])

4.4.3 Vector Instructions

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

shape

.

op

𝑡

x

𝑁

(

𝑛

1

, . . . , 𝑛

𝑘

)

=

lanes

−

1

𝑡

x

𝑁

(

𝑜𝑝

𝑡

(

lanes

𝑡

x

𝑁

(

𝑛

1

)

. . .

lanes

𝑡

x

𝑁

(

𝑛

𝑘

))

Note:

For example, the result of instruction

i32x4

.

add

applied to operands

𝑖

1

, 𝑖

2

invokes

add

i32x4

(

𝑖

1

, 𝑖

2

)

, which

maps to

lanes

−

1

i32x4

(

add

i32

(

𝑖

+
1

, 𝑖

+
2

))

, where

𝑖

+
1

and

𝑖

+
2

are sequences resulting from invoking

lanes

i32x4

(

𝑖

1

)

and

lanes

i32x4

(

𝑖

2

)

respectively.

v128

.

const

𝑐

1. Push the value

v128

.

const

𝑐

to the stack.

Note:

No formal reduction rule is required for this instruction, since

const

instructions coincide with

values

.

v128

.

vvunop

1. Assert: due to

validation

, a value of

value type

v128

is on the top of the stack.

2. Pop the value

v128

.

const

𝑐

1

from the stack.

3. Let

𝑐

be the result of computing

vvunop

i128

(

𝑐

1

)

.

4. Push the value

v128

.

const

𝑐

to the stack.

(

v128

.

const

𝑐

1

)

v128

.

vvunop

˓

→

(

v128

.

const

𝑐

)

(

if

𝑐

=

vvunop

i128

(

𝑐

1

))

v128

.

vvbinop

1. Assert: due to

validation

, two values of

value type

v128

are on the top of the stack.

2. Pop the value

v128

.

const

𝑐

2

from the stack.

3. Pop the value

v128

.

const

𝑐

1

from the stack.

4. Let

𝑐

be the result of computing

vvbinop

i128

(

𝑐

1

, 𝑐

2

)

.

5. Push the value

v128

.

const

𝑐

to the stack.

(

v128

.

const

𝑐

1

) (

v128

.

const

𝑐

2

)

v128

.

vvbinop

˓

→

(

v128

.

const

𝑐

)

(

if

𝑐

=

vvbinop

i128

(

𝑐

1

, 𝑐

2

))

90

Chapter 4. Execution

v128

.

vvternop

1. Assert: due to

validation

, three values of

value type

v128

are on the top of the stack.

2. Pop the value

v128

.

const

𝑐

3

from the stack.

3. Pop the value

v128

.

const

𝑐

2

from the stack.

4. Pop the value

v128

.

const

𝑐

1

from the stack.

5. Let

𝑐

be the result of computing

vvternop

i128

(

𝑐

1

, 𝑐

2

, 𝑐

3

)

.

6. Push the value

v128

.

const

𝑐

to the stack.

(

v128

.

const

𝑐

1

) (

v128

.

const

𝑐

2

) (

v128

.

const

𝑐

3

)

v128

.

vvternop

˓

→

(

v128

.

const

𝑐

)

(

if

𝑐

=

vvternop

i128

(

𝑐

1

, 𝑐

2

, 𝑐

3

))

v128

.

any

_

true

1. Assert: due to

validation

, a value of

value type

v128

is on the top of the stack.

2. Pop the value

v128

.

const

𝑐

1

from the stack.

3. Let

𝑖

be the result of computing

ine

128

(

𝑐

1

,

0)

.

4. Push the value

i32

.

const

𝑖

onto the stack.

(

v128

.

const

𝑐

1

)

v128

.

any

_

true

˓

→

(

i32

.

const

𝑖

)

(

if

𝑖

=

ine

128

(

𝑐

1

,

0))

i8x16

.

swizzle

1. Assert: due to

validation

, two values of

value type

v128

are on the top of the stack.

2. Pop the value

v128

.

const

𝑐

2

from the stack.

3. Let

𝑖

*

be the sequence

lanes

𝑖

8

𝑥

16

(

𝑐

2

)

.

4. Pop the value

v128

.

const

𝑐

1

from the stack.

5. Let

𝑗

*

be the sequence

lanes

𝑖

8

𝑥

16

(

𝑐

1

)

.

6. Let

𝑐

*

be the concatenation of the two sequences

𝑗

*

0

240

7. Let

𝑐

′

be the result of

lanes

−

1

𝑖

8

𝑥

16

(

𝑐

*

[

𝑖

*

[0]]

. . . 𝑐

*

[

𝑖

*

[15]])

.

8. Push the value

v128

.

const

𝑐

′

onto the stack.

(

v128

.

const

𝑐

1

) (

v128

.

const

𝑐

2

)

v128

.

swizzle

˓

→

(

v128

.

const

𝑐

′

)

(

if

𝑖

*

=

lanes

𝑖

8

𝑥

16

(

𝑐

2

)

∧

𝑐

*

=

lanes

𝑖

8

𝑥

16

(

𝑐

1

) 0

240

∧

𝑐

′

=

lanes

−

1

𝑖

8

𝑥

16

(

𝑐

*

[

𝑖

*

[0]]

. . . 𝑐

*

[

𝑖

*

[15]])

i8x16

.

shuffle

𝑥

*

1. Assert: due to

validation

, two values of

value type

v128

are on the top of the stack.

2. Assert: due to

validation

, for all

𝑥

𝑖

in

𝑥

*

it holds that

𝑥

𝑖

<

32

.

3. Pop the value

v128

.

const

𝑐

2

from the stack.

4. Let

𝑖

*

2

be the sequence

lanes

𝑖

8

𝑥

16

(

𝑐

2

)

.

5. Pop the value

v128

.

const

𝑐

1

from the stack.

6. Let

𝑖

*

1

be the sequence

lanes

𝑖

8

𝑥

16

(

𝑐

1

)

.

7. Let

𝑖

*

be the concatenation of the two sequences

𝑖

*

1

𝑖

*

2

.

8. Let

𝑐

be the result of

lanes

−

1

𝑖

8

𝑥

16

(

𝑖

*

[

𝑥

*

[0]]

. . . 𝑖

*

[

𝑥

*

[15]])

.

4.4. Instructions

91

9. Push the value

v128

.

const

𝑐

onto the stack.

(

v128

.

const

𝑐

1

) (

v128

.

const

𝑐

2

)

v128

.

shuffle

𝑥

*

˓

→

(

v128

.

const

𝑐

)

(

if

𝑖

*

=

lanes

𝑖

8

𝑥

16

(

𝑐

1

)

lanes

𝑖

8

𝑥

16

(

𝑐

2

)

∧

𝑐

=

lanes

−

1

𝑖

8

𝑥

16

(

𝑖

*

[

𝑥

*

[0]]

. . . 𝑖

*

[

𝑥

*

[15]])

shape

.

splat

1. Let

𝑡

be the type

unpacked

(

shape

)

.

2. Assert: due to

validation

, a value of

value type

𝑡

is on the top of the stack.

3. Pop the value

𝑡.

const

𝑐

1

from the stack.

4. Let

𝑁

be the integer

dim

(

shape

)

.

5. Let

𝑐

be the result of

lanes

−

1

shape

(

𝑐

𝑁

1

)

.

6. Push the value

v128

.

const

𝑐

to the stack.

(

𝑡.

const

𝑐

1

)

shape

.

splat

˓

→

(

v128

.

const

𝑐

)

(

if

𝑡

=

unpacked

(

shape

)

∧

𝑐

=

lanes

−

1

shape

(

𝑐

dim

(

shape

)

1

))

𝑡

1

x

𝑁.

extract

_

lane

_

sx

?

𝑥

1. Assert: due to

validation

,

𝑥 < 𝑁

.

2. Assert: due to

validation

, a value of

value type

v128

is on the top of the stack.

3. Pop the value

v128

.

const

𝑐

1

from the stack.

4. Let

𝑖

*

be the sequence

lanes

𝑡

1

x

𝑁

(

𝑐

1

)

.

5. Let

𝑡

2

be the type

unpacked

(

𝑡

1

x

𝑁

)

.

6. Let

𝑐

2

be the result of computing

extend

𝑠𝑥

?

𝑡

1

,𝑡

2

(

𝑖

*

[

𝑥

])

.

7. Push the value

𝑡

2

.

const

𝑐

2

to the stack.

(

v128

.

const

𝑐

1

)

𝑡

1

x

𝑁.

extract

_

lane

𝑥

˓

→

(

𝑡

2

.

const

𝑐

2

)

(

if

𝑡

2

=

unpacked

(

𝑡

1

x

𝑁

)

∧

𝑐

2

=

extend

𝑠𝑥

?

𝑡

1

,𝑡

2

(

lanes

𝑡

1

x

𝑁

(

𝑐

1

)[

𝑥

])

shape

.

replace

_

lane

𝑥

1. Assert: due to

validation

,

𝑥 <

dim

(

shape

)

.

2. Let

𝑡

1

be the type

unpacked

(

shape

)

.

3. Assert: due to

validation

, a value of

value type

𝑡

1

is on the top of the stack.

4. Pop the value

𝑡

1

.

const

𝑐

1

from the stack.

5. Assert: due to

validation

, a value of

value type

v128

is on the top of the stack.

6. Pop the value

v128

.

const

𝑐

2

from the stack.

7. Let

𝑖

*

be the sequence

lanes

shape

(

𝑐

2

)

.

8. Let

𝑐

be the result of computing

lanes

−

1

shape

(

𝑖

*

with

[

𝑥

] =

𝑐

1

)

9. Push

v128

.

const

𝑐

on the stack.

(

𝑡

1

.

const

𝑐

1

) (

v128

.

const

𝑐

2

)

shape

.

replace

_

lane

𝑥

˓

→

(

v128

.

const

𝑐

)

(

if

𝑖

*

=

lanes

shape

(

𝑐

2

))

∧

𝑐

=

lanes

−

1

shape

(

𝑖

*

with

[

𝑥

] =

𝑐

1

)

92

Chapter 4. Execution

shape

.

vunop

1. Assert: due to

validation

, a value of

value type

v128

is on the top of the stack.

2. Pop the value

v128

.

const

𝑐

1

from the stack.

3. Let

𝑐

be the result of computing

vunop

shape

(

𝑐

1

)

.

4. Push the value

v128

.

const

𝑐

to the stack.

(

v128

.

const

𝑐

1

)

v128

.

vunop

˓

→

(

v128

.

const

𝑐

)

(

if

𝑐

=

vunop

shape

(

𝑐

1

))

shape

.

vbinop

1. Assert: due to

validation

, two values of

value type

v128

are on the top of the stack.

2. Pop the value

v128

.

const

𝑐

2

from the stack.

3. Pop the value

v128

.

const

𝑐

1

from the stack.

4. If

vbinop

shape

(

𝑐

1

, 𝑐

2

)

is defined:

a. Let

𝑐

be a possible result of computing

vbinop

shape

(

𝑐

1

, 𝑐

2

)

.

b. Push the value

v128

.

const

𝑐

to the stack.

5. Else:

a. Trap.

(

v128

.

const

𝑐

1

) (

v128

.

const

𝑐

2

)

shape

.

vbinop

˓

→

(

v128

.

const

𝑐

)

(

if

𝑐

∈

vbinop

shape

(

𝑐

1

, 𝑐

2

))

(

v128

.

const

𝑐

1

) (

v128

.

const

𝑐

2

)

shape

.

vbinop

˓

→

trap

(

if

vbinop

shape

(

𝑐

1

, 𝑐

2

) =

{}

)

𝑡

x

𝑁.

vrelop

1. Assert: due to

validation

, two values of

value type

v128

are on the top of the stack.

2. Pop the value

v128

.

const

𝑐

2

from the stack.

3. Pop the value

v128

.

const

𝑐

1

from the stack.

4. Let

𝑖

*

be the sequence

lanes

𝑡

x

𝑁

(

𝑐

1

)

.

5. Let

𝑗

*

be the sequence

lanes

𝑡

x

𝑁

(

𝑐

2

)

.

6. Let

𝑐

be the result of computing

lanes

−

1

𝑡

x

𝑁

(

extend

s

1

,

|

𝑡

|

(

vrelop

𝑡

(

𝑖

*

, 𝑗

*

)))

.

7. Push the value

v128

.

const

𝑐

to the stack.

(

v128

.

const

𝑐

1

) (

v128

.

const

𝑐

2

)

𝑡

x

𝑁.

vrelop

˓

→

(

v128

.

const

𝑐

)

(

if

𝑐

=

lanes

−

1

𝑡

x

𝑁

(

extend

s

1

,

|

𝑡

|

(

vrelop

𝑡

(

lanes

𝑡

x

𝑁

(

𝑐

1

)

,

lanes

𝑡

x

𝑁

(

𝑐

2

)))))

𝑡

x

𝑁.

vishiftop

1. Assert: due to

validation

, a value of

value type

i32

is on the top of the stack.

2. Pop the value

i32

.

const

𝑠

from the stack.

3. Assert: due to

validation

, a value of

value type

v128

is on the top of the stack.

4. Pop the value

v128

.

const

𝑐

1

from the stack.

5. Let

𝑖

*

be the sequence

lanes

𝑡

x

𝑁

(

𝑐

1

)

.

6. Let

𝑐

be

lanes

−

1

𝑡

x

𝑁

(

vishiftop

𝑡

(

𝑖

*

, 𝑠

𝑁

))

.

7. Push the value

v128

.

const

𝑐

to the stack.

4.4. Instructions

93

(

v128

.

const

𝑐

1

) (

i32

.

const

𝑠

)

𝑡

x

𝑁.

vishiftop

˓

→

(

v128

.

const

𝑐

)

(

if

𝑖

*

=

lanes

𝑡

x

𝑁

(

𝑐

1

)

∧

𝑐

=

lanes

−

1

𝑡

x

𝑁

(

vishiftop

𝑡

(

𝑖

*

, 𝑠

𝑁

)))

shape

.

all

_

true

1. Assert: due to

validation

, a value of

value type

v128

is on the top of the stack.

2. Pop the value

v128

.

const

𝑐

1

from the stack.

3. Let

𝑖

*

1

be the sequence

lanes

shape

(

𝑐

1

)

4. Let

𝑖

be the result of computing

bool

(

⋀︀

(

𝑖

1

̸

= 0)

*

)

.

5. Push the value

i32

.

const

𝑖

onto the stack.

(

v128

.

const

𝑐

1

)

shape

.

all

_

true

˓

→

(

i32

.

const

𝑖

)

(

if

𝑖

*

1

=

lanes

shape

(

𝑐

)

∧

𝑖

=

bool

(

⋀︀

(

𝑖

1

̸

= 0)

*

)

𝑡

x

𝑁.

bitmask

1. Assert: due to

validation

, a value of

value type

v128

is on the top of the stack.

2. Pop the value

v128

.

const

𝑐

1

from the stack.

3. Let

𝑖

𝑁

1

be the sequence

lanes

𝑡

x

𝑁

(

𝑐

)

.

4. Let

𝐵

be the

bit width

|

𝑡

|

of

value type

𝑡

.

5. Let

𝑖

𝑁

2

be the sequence as a result of computing

ilt

_

s

𝐵

(

𝑖

𝑁

1

,

0

𝑁

)

.

6. Let

𝑐

be the integer

ibits

−

1

32

(

𝑖

𝑁

2

0

32

−

𝑁

)

.

7. Push the value

i32

.

const

𝑐

onto the stack.

(

v128

.

const

𝑐

1

)

𝑡

x

𝑁.

bitmask

˓

→

(

i32

.

const

𝑐

)

(

if

𝑐

=

ibits

−

1

32

(

ilt

_

s

|

𝑡

|

(

lanes

𝑡

x

𝑁

(

𝑐

)

,

0

𝑁

)))

𝑡

2

x

𝑁.

narrow

_

𝑡

1

x

𝑀

_

sx

1. Assert: due to

syntax

,

𝑁

= 2

·

𝑀

.

2. Assert: due to

validation

, two values of

value type

v128

are on the top of the stack.

3. Pop the value

v128

.

const

𝑐

2

from the stack.

4. Let

𝑑

𝑀

2

be the result of computing

narrow

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

lanes

𝑡

1

x

𝑀

(

𝑐

2

))

.

5. Pop the value

v128

.

const

𝑐

1

from the stack.

6. Let

𝑑

𝑀

1

be the result of computing

narrow

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

lanes

𝑡

1

x

𝑀

(

𝑐

1

))

.

7. Let

𝑐

be the result of

lanes

−

1

𝑡

2

x

𝑁

(

𝑑

𝑀

1

𝑑

𝑀

2

)

.

8. Push the value

v128

.

const

𝑐

onto the stack.

(

v128

.

const

𝑐

1

) (

v128

.

const

𝑐

2

)

𝑡

2

x

𝑁.

narrow

_

𝑡

1

x

𝑀

_

sx

˓

→

(

v128

.

const

𝑐

)

(

if

𝑑

𝑀

1

=

narrow

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

lanes

𝑡

1

x

𝑀

(

𝑐

1

))

∧

𝑑

𝑀

2

=

narrow

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

lanes

𝑡

1

x

𝑀

(

𝑐

2

))

∧

𝑐

=

lanes

−

1

𝑡

2

x

𝑁

(

𝑑

𝑀

1

𝑑

𝑀

2

)

94

Chapter 4. Execution

𝑡

2

x

𝑁.

vcvtop

_

𝑡

1

x

𝑀

_

sx

1. Assert: due to

validation

, a value of

value type

v128

is on the top of the stack.

2. Pop the value

v128

.

const

𝑐

1

from the stack.

3. Let

𝑖

*

be the sequence

lanes

𝑡

1

x

𝑀

(

𝑐

1

)

.

4. Let

𝑐

be the result of computing

lanes

−

1

𝑡

2

x

𝑁

(

vcvtop

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

𝑖

*

))

5. Push the value

v128

.

const

𝑐

onto the stack.

(

v128

.

const

𝑐

1

)

𝑡

2

x

𝑁.

vcvtop

_

𝑡

1

x

𝑀

_

sx

˓

→

(

v128

.

const

𝑐

)

(

if

𝑐

=

lanes

−

1

𝑡

2

x

𝑁

(

vcvtop

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

lanes

𝑡

1

x

𝑀

(

𝑐

1

)))

𝑡

2

x

𝑁.

vcvtop

_

half

_

𝑡

1

x

𝑀

_

sx

?

1. Assert: due to

validation

, a value of

value type

v128

is on the top of the stack.

2. Pop the value

v128

.

const

𝑐

1

from the stack.

3. If

half

is

low

, then:

a. Let

𝑖

*

be the sequence

lanes

𝑡

1

x

𝑀

(

𝑐

1

)[0

:

𝑁

]

.

4. Else:

a. Let

𝑖

*

be the sequence

lanes

𝑡

1

x

𝑀

(

𝑐

1

)[

𝑁

:

𝑁

]

.

5. Let

𝑗

*

be the result of computing

vcvtop

sx

?

|

𝑡

1

|

,

|

𝑡

2

|

(

𝑖

*

)

.

6. Let

𝑐

be the result of computing

lanes

−

1

𝑡

2

x

𝑁

(

𝑗

*

)

.

7. Push the value

v128

.

const

𝑐

onto the stack.

(

v128

.

const

𝑐

1

)

𝑡

2

x

𝑁.

vcvtop

_

half

_

𝑡

1

x

𝑀

_

sx

?

˓

→

(

v128

.

const

𝑐

)

(

if

𝑐

=

lanes

−

1

𝑡

2

x

𝑁

(

vcvtop

sx

?

|

𝑡

1

|

,

|

𝑡

2

|

(

lanes

𝑡

1

x

𝑀

(

𝑐

1

)[

half

(0

, 𝑁

)

:

𝑁

]))

where:

low

(

𝑥, 𝑦

)

=

𝑥

high

(

𝑥, 𝑦

)

=

𝑦

𝑡

2

x

𝑁.

vcvtop

_

𝑡

1

x

𝑀

_

sx

_

zero

1. Assert: due to

validation

, a value of

value type

v128

is on the top of the stack.

2. Pop the value

v128

.

const

𝑐

1

from the stack.

3. Let

𝑖

*

be the sequence

lanes

𝑡

1

x

𝑀

(

𝑐

1

)

.

4. Let

𝑗

*

be the result of computing

vcvtop

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

𝑖

*

)

concatenated with the vector

0

𝑀

.

5. Let

𝑐

be the result of computing

lanes

−

1

𝑡

2

x

𝑁

(

𝑗

*

)

.

6. Push the value

v128

.

const

𝑐

onto the stack.

(

v128

.

const

𝑐

1

)

𝑡

2

x

𝑁.

vcvtop

_

𝑡

1

x

𝑀

_

sx

_

zero

˓

→

(

v128

.

const

𝑐

)

(

if

𝑐

=

lanes

−

1

𝑡

2

x

𝑁

(

vcvtop

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

lanes

𝑡

1

x

𝑀

(

𝑐

1

)) 0

𝑀

)

4.4. Instructions

95

i32x4

.

dot

_

i16x8

_

s

1. Assert: due to

validation

, two values of

value type

v128

is on the top of the stack.

2. Pop the value

v128

.

const

𝑐

2

from the stack.

3. Pop the value

v128

.

const

𝑐

1

from the stack.

4. Let

(

𝑖

1

𝑖

2

)

*

be the result of computing

imul

32

(

extend

s

16

,

32

(

lanes

i16x8

(

𝑐

1

))

,

extend

s

16

,

32

(

lanes

i16x8

(

𝑐

2

)))

5. Let

𝑗

*

be the result of computing

iadd

32

(

𝑖

1

, 𝑖

2

)

*

.

6. Let

𝑐

be the result of computing

lanes

−

1

i32x4

(

𝑗

*

)

.

7. Push the value

v128

.

const

𝑐

onto the stack.

(

v128

.

const

𝑐

1

) (

v128

.

const

𝑐

2

)

i32x4

.

dot

_

i16x8

_

s

˓

→

(

v128

.

const

𝑐

)

(

if

(

𝑖

1

𝑖

2

)

*

=

imul

32

(

extend

s

16

,

32

(

lanes

i16x8

(

𝑐

1

))

,

extend

s

16

,

32

(

lanes

i16x8

(

𝑐

2

)))

∧

𝑗

*

=

iadd

32

(

𝑖

1

, 𝑖

2

)

*

∧

𝑐

=

lanes

−

1

i32x4

(

𝑗

*

)

𝑡

2

x

𝑁.

extmul

_

half

_

𝑡

1

x

𝑀

_

sx

1. Assert: due to

validation

, two values of

value type

v128

is on the top of the stack.

2. Pop the value

v128

.

const

𝑐

2

from the stack.

3. Pop the value

v128

.

const

𝑐

1

from the stack.

4. If

half

is

low

, then:

a. Let

𝑖

*

be the sequence

lanes

𝑡

1

x

𝑀

(

𝑐

1

)[0

:

𝑁

]

.

b. Let

𝑗

*

be the sequence

lanes

𝑡

1

x

𝑀

(

𝑐

2

)[0

:

𝑁

]

.

5. Else:

a. Let

𝑖

*

be the sequence

lanes

𝑡

1

x

𝑀

(

𝑐

1

)[

𝑁

:

𝑁

]

.

b. Let

𝑗

*

be the sequence

lanes

𝑡

1

x

𝑀

(

𝑐

2

)[

𝑁

:

𝑁

]

.

6. Let

𝑐

be the result of computing

lanes

−

1

𝑡

2

x

𝑁

(

imul

𝑡

2

x

𝑁

(

extend

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

𝑖

*

)

,

extend

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

𝑗

*

)))

7. Push the value

v128

.

const

𝑐

onto the stack.

(

v128

.

const

𝑐

1

) (

v128

.

const

𝑐

2

)

𝑡

2

x

𝑁.

extmul

_

half

_

𝑡

1

x

𝑀

_

sx

˓

→

(

v128

.

const

𝑐

)

(

if

𝑖

*

=

lanes

𝑡

1

x

𝑀

(

𝑐

1

)[

half

(0

, 𝑁

)

:

𝑁

]

∧

𝑗

*

=

lanes

𝑡

1

x

𝑀

(

𝑐

2

)[

half

(0

, 𝑁

)

:

𝑁

]

∧

𝑐

=

lanes

−

1

𝑡

2

x

𝑁

(

imul

𝑡

2

x

𝑁

(

extend

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

𝑖

*

)

,

extend

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

𝑗

*

)))

where:

low

(

𝑥, 𝑦

)

=

𝑥

high

(

𝑥, 𝑦

)

=

𝑦

𝑡

2

x

𝑁.

extadd

_

pairwise

_

𝑡

1

x

𝑀

_

sx

1. Assert: due to

validation

, a value of

value type

v128

is on the top of the stack.

2. Pop the value

v128

.

const

𝑐

1

from the stack.

3. Let

(

𝑖

1

𝑖

2

)

*

be the sequence

extend

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

lanes

𝑡

1

x

𝑀

(

𝑐

1

))

.

4. Let

𝑗

*

be the result of computing

iadd

𝑁

(

𝑖

1

, 𝑖

2

)

*

.

5. Let

c

be the result of computing

lanes

−

1

𝑡

2

x

𝑁

(

𝑗

*

)

.

6. Push the value

v128

.

const

𝑐

to the stack.

96

Chapter 4. Execution

(

v128

.

const

𝑐

1

)

𝑡

2

x

𝑁.

extadd

_

pairwise

_

𝑡

1

x

𝑀

_

sx

˓

→

(

v128

.

const

𝑐

)

(

if

(

𝑖

1

𝑖

2

)

*

=

extend

sx

|

𝑡

1

|

,

|

𝑡

2

|

(

lanes

𝑡

1

x

𝑀

(

𝑐

1

))

∧

𝑗

*

=

iadd

𝑁

(

𝑖

1

, 𝑖

2

)

*

∧

𝑐

=

lanes

−

1

𝑡

2

x

𝑁

(

𝑗

*

)

4.4.4 Parametric Instructions

drop

1. Assert: due to

validation

, a value is on the top of the stack.

2. Pop the value

val

from the stack.

val

drop

˓

→

𝜖

select

(

𝑡

*

)

?

1. Assert: due to

validation

, a value of

value type

i32

is on the top of the stack.

2. Pop the value

i32

.

const

𝑐

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

val

2

from the stack.

5. Pop the value

val

1

from the stack.

6. If

𝑐

is not

0

, then:

a. Push the value

val

1

back to the stack.

7. Else:

a. Push the value

val

2

back to the stack.

val

1

val

2

(

i32

.

const

𝑐

)

select

𝑡

?

˓

→

val

1

(

if

𝑐

̸

= 0)

val

1

val

2

(

i32

.

const

𝑐

)

select

𝑡

?

˓

→

val

2

(

if

𝑐

= 0)

Note:

In future versions of WebAssembly,

select

may allow more than one value per choice.

4.4.5 Variable Instructions

local

.

get

𝑥

1. Let

𝐹

be the

current frame

.

2. Assert: due to

validation

,

𝐹.

locals

[

𝑥

]

exists.

3. Let

val

be the value

𝐹.

locals

[

𝑥

]

.

4. Push the value

val

to the stack.

𝐹

; (

local

.

get

𝑥

)

˓

→

𝐹

;

val

(

if

𝐹.

locals

[

𝑥

] =

val

)

4.4. Instructions

97

local

.

set

𝑥

1. Let

𝐹

be the

current frame

.

2. Assert: due to

validation

,

𝐹.

locals

[

𝑥

]

exists.

3. Assert: due to

validation

, a value is on the top of the stack.

4. Pop the value

val

from the stack.

5. Replace

𝐹.

locals

[

𝑥

]

with the value

val

.

𝐹

;

val

(

local

.

set

𝑥

)

˓

→

𝐹

′

;

𝜖

(

if

𝐹

′

=

𝐹

with

locals

[

𝑥

] =

val

)

local

.

tee

𝑥

1. Assert: due to

validation

, a value is on the top of the stack.

2. Pop the value

val

from the stack.

3. Push the value

val

to the stack.

4. Push the value

val

to the stack.

5.

Execute

the instruction

(

local

.

set

𝑥

)

.

val

(

local

.

tee

𝑥

)

˓

→

val val

(

local

.

set

𝑥

)

global

.

get

𝑥

1. Let

𝐹

be the

current frame

.

2. Assert: due to

validation

,

𝐹.

module

.

globaladdrs

[

𝑥

]

exists.

3. Let

𝑎

be the

global address

𝐹.

module

.

globaladdrs

[

𝑥

]

.

4. Assert: due to

validation

,

𝑆.

globals

[

𝑎

]

exists.

5. Let

glob

be the

global instance

𝑆.

globals

[

𝑎

]

.

6. Let

val

be the value

glob

.

value

.

7. Push the value

val

to the stack.

𝑆

;

𝐹

; (

global

.

get

𝑥

)

˓

→

𝑆

;

𝐹

;

val

(

if

𝑆.

globals

[

𝐹.

module

.

globaladdrs

[

𝑥

]]

.

value

=

val

)

global

.

set

𝑥

1. Let

𝐹

be the

current frame

.

2. Assert: due to

validation

,

𝐹.

module

.

globaladdrs

[

𝑥

]

exists.

3. Let

𝑎

be the

global address

𝐹.

module

.

globaladdrs

[

𝑥

]

.

4. Assert: due to

validation

,

𝑆.

globals

[

𝑎

]

exists.

5. Let

glob

be the

global instance

𝑆.

globals

[

𝑎

]

.

6. Assert: due to

validation

, a value is on the top of the stack.

7. Pop the value

val

from the stack.

8. Replace

glob

.

value

with the value

val

.

98

Chapter 4. Execution

𝑆

;

𝐹

;

val

(

global

.

set

𝑥

)

˓

→

𝑆

′

;

𝐹

;

𝜖

(

if

𝑆

′

=

𝑆

with

globals

[

𝐹.

module

.

globaladdrs

[

𝑥

]]

.

value

=

val

)

Note:

Validation

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

4.4.6 Table Instructions

table

.

get

𝑥

1. Let

𝐹

be the

current frame

.

2. Assert: due to

validation

,

𝐹.

module

.

tableaddrs

[

𝑥

]

exists.

3. Let

𝑎

be the

table address

𝐹.

module

.

tableaddrs

[

𝑥

]

.

4. Assert: due to

validation

,

𝑆.

tables

[

𝑎

]

exists.

5. Let

tab

be the

table instance

𝑆.

tables

[

𝑎

]

.

6. Assert: due to

validation

, a value of

value type

i32

is on the top of the stack.

7. Pop the value

i32

.

const

𝑖

from the stack.

8. If

𝑖

is not smaller than the length of

tab

.

elem

, then:

a. Trap.

9. Let

val

be the value

tab

.

elem

[

𝑖

]

.

10. Push the value

val

to the stack.

𝑆

;

𝐹

; (

i32

.

const

𝑖

) (

table

.

get

𝑥

)

˓

→

𝑆

;

𝐹

;

val

(

if

𝑆.

tables

[

𝐹.

module

.

tableaddrs

[

𝑥

]]

.

elem

[

𝑖

] =

val

)

𝑆

;

𝐹

; (

i32

.

const

𝑖

) (

table

.

get

𝑥

)

˓

→

𝑆

;

𝐹

;

trap

(

otherwise

)

table

.

set

1. Let

𝐹

be the

current frame

.

2. Assert: due to

validation

,

𝐹.

module

.

tableaddrs

[

𝑥

]

exists.

3. Let

𝑎

be the

table address

𝐹.

module

.

tableaddrs

[

𝑥

]

.

4. Assert: due to

validation

,

𝑆.

tables

[

𝑎

]

exists.

5. Let

tab

be the

table instance

𝑆.

tables

[

𝑎

]

.

6. Assert: due to

validation

, a

reference value

is on the top of the stack.

7. Pop the value

val

from the stack.

8. Assert: due to

validation

, a value of

value type

i32

is on the top of the stack.

9. Pop the value

i32

.

const

𝑖

from the stack.

10. If

𝑖

is not smaller than the length of

tab

.

elem

, then:

a. Trap.

11. Replace the element

tab

.

elem

[

𝑖

]

with

val

.

4.4. Instructions

99

𝑆

;

𝐹

; (

i32

.

const

𝑖

)

val

(

table

.

set

𝑥

)

˓

→

𝑆

′

;

𝐹

;

𝜖

(

if

𝑆

′

=

𝑆

with

tables

[

𝐹.

module

.

tableaddrs

[

𝑥

]]

.

elem

[

𝑖

] =

val

)

𝑆

;

𝐹

; (

i32

.

const

𝑖

)

val

(

table

.

set

𝑥

)

˓

→

𝑆

;

𝐹

;

trap

(

otherwise

)

table

.

size

𝑥

1. Let

𝐹

be the

current frame

.

2. Assert: due to

validation

,

𝐹.

module

.

tableaddrs

[

𝑥

]

exists.

3. Let

𝑎

be the

table address

𝐹.

module

.

tableaddrs

[

𝑥

]

.

4. Assert: due to

validation

,

𝑆.

tables

[

𝑎

]

exists.

5. Let

tab

be the

table instance

𝑆.

tables

[

𝑎

]

.

6. Let

sz

be the length of

tab

.

elem

.

7. Push the value

i32

.

const

sz

to the stack.

𝑆

;

𝐹

;

table

.

size

𝑥

˓

→

𝑆

;

𝐹

; (

i32

.

const

sz

)

(

if

|

𝑆.

tables

[

𝐹.

module

.

tableaddrs

[

𝑥

]]

.

elem

|

=

sz

)

table

.

grow

𝑥

1. Let

𝐹

be the

current frame

.

2. Assert: due to

validation

,

𝐹.

module

.

tableaddrs

[

𝑥

]

exists.

3. Let

𝑎

be the

table address

𝐹.

module

.

tableaddrs

[

𝑥

]

.

4. Assert: due to

validation

,

𝑆.

tables

[

𝑎

]

exists.

5. Let

tab

be the

table instance

𝑆.

tables

[

𝑎

]

.

6. Let

sz

be the length of

𝑆.

tables

[

𝑎

]

.

7. Assert: due to

validation

, a value of

value type

i32

is on the top of the stack.

8. Pop the value

i32

.

const

𝑛

from the stack.

9. Assert: due to

validation

, a

reference value

is on the top of the stack.

10. Pop the value

val

from the stack.

11. Either, try

growing

table

by

𝑛

entries with initialization value

val

:

a. If it succeeds, push the value

i32

.

const

sz

to the stack.

b. Else, push the value

i32

.

const

(

−

1)

to the stack.

12. Or, push the value

i32

.

const

(

−

1)

to the stack.

𝑆

;

𝐹

;

val

(

i32

.

const

𝑛

)

table

.

grow

𝑥

˓

→

𝑆

′

;

𝐹

; (

i32

.

const

sz

)

(

if

𝐹.

module

.

tableaddrs

[

𝑥

] =

𝑎

∧

sz

=

|

𝑆.

tables

[

𝑎

]

.

elem

|

∧

𝑆

′

=

𝑆

with

tables

[

𝑎

] =

growtable

(

𝑆.

tables

[

𝑎

]

, 𝑛,

val

))

𝑆

;

𝐹

; (

i32

.

const

𝑛

)

table

.

grow

𝑥

˓

→

𝑆

;

𝐹

; (

i32

.

const

−

1)

Note:

The

table

.

grow

instruction is non-deterministic. It may either succeed, returning the old table size

sz

,

or fail, returning

−

1

. 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

.

100

Chapter 4. Execution

table

.

fill

𝑥

1. Let

𝐹

be the

current frame

.

2. Assert: due to

validation

,

𝐹.

module

.

tableaddrs

[

𝑥

]

exists.

3. Let

ta

be the

table address

𝐹.

module

.

tableaddrs

[

𝑥

]

.

4. Assert: due to

validation

,

𝑆.

tables

[

ta

]

exists.

5. Let

tab

be the

table instance

𝑆.

tables

[

ta

]

.

6. Assert: due to

validation

, a value of

value type

i32

is on the top of the stack.

7. Pop the value

i32

.

const

𝑛

from the stack.

8. Assert: due to

validation

, a

reference value

is on the top of the stack.

9. Pop the value

val

from the stack.

10. Assert: due to

validation

, a value of

value type

i32

is on the top of the stack.

11. Pop the value

i32

.

const

𝑖

from the stack.

12. If

𝑖

+

𝑛

is larger than the length of

tab

.

elem

, then:

a. Trap.

12. If

𝑛

is

0

, then:

a. Return.

13. Push the value

i32

.

const

𝑖

to the stack.

14. Push the value

val

to the stack.

15. Execute the instruction

table

.

set

𝑥

.

16. Push the value

i32

.

const

(

𝑖

+ 1)

to the stack.

17. Push the value

val

to the stack.

18. Push the value

i32

.

const

(

𝑛

−

1)

to the stack.

19. Execute the instruction

table

.

fill

𝑥

.

𝑆

;

𝐹

; (

i32

.

const

𝑖

)

val

(

i32

.

const

𝑛

) (

table

.

fill

𝑥

)

˓

→

𝑆

;

𝐹

;

trap

(

if

𝑖

+

𝑛 >

|

𝑆.

tables

[

𝐹.

module

.

tableaddrs

[

𝑥

]]

.

elem

|

)

𝑆

;

𝐹

; (

i32

.

const

𝑖

)

val

(

i32

.

const

0) (

table

.

fill

𝑥

)

˓

→

𝑆

;

𝐹

;

𝜖

(

otherwise

)

𝑆

;

𝐹

; (

i32

.

const

𝑖

)

val

(

i32

.

const

𝑛

+ 1) (

table

.

fill

𝑥

)

˓

→

𝑆

;

𝐹

; (

i32

.

const

𝑖

)

val

(

table

.

set

𝑥

)

(

i32

.

const

𝑖

+ 1)

val

(

i32

.

const

𝑛

) (

table

.

fill

𝑥

)

(

otherwise

)

table

.

copy

𝑥 𝑦

1. Let

𝐹

be the

current frame

.

2. Assert: due to

validation

,

𝐹.

module

.

tableaddrs

[

𝑥

]

exists.

3. Let

ta

𝑥

be the

table address

𝐹.

module

.

tableaddrs

[

𝑥

]

.

4. Assert: due to

validation

,

𝑆.

tables

[

ta

𝑥

]

exists.

5. Let

tab

𝑥

be the

table instance

𝑆.

tables

[

ta

𝑥

]

.

6. Assert: due to

validation

,

𝐹.

module

.

tableaddrs

[

𝑦

]

exists.

7. Let

ta

𝑦

be the

table address

𝐹.

module

.

tableaddrs

[

𝑦

]

.

4.4. Instructions

101