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

𝑑

) (

𝑠

) (

𝑛

) (

𝑥 𝑦

)

𝑆

;

𝐹

(

𝑠

𝑛 >

𝑆.

𝐹.

𝑦

]]

∨

𝑑

𝑛 >

𝑆.

𝐹.

𝑥

]]

)

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

0) (

𝑥 𝑦

)

𝑆

;

𝐹

;

𝜖

(

otherwise

)

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

𝑛

+ 1) (

𝑥 𝑦

)

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

get

𝑦

) (

set

𝑥

)

𝑑

+ 1) (

𝑠

+ 1) (

𝑛

) (

𝑥 𝑦

)

(

otherwise

𝑑

≤

𝑠

)

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

𝑛

+ 1) (

𝑥 𝑦

)

𝑆

;

𝐹

; (

𝑑

𝑛

−

1) (

𝑠

𝑛

−

1) (

get

𝑦

) (

set

𝑥

)

𝑑

) (

𝑠

) (

𝑛

) (

𝑥 𝑦

)

(

otherwise

𝑑 > 𝑠

)

𝑥 𝑦

1. Let

𝐹

be the

2. Assert: due to

𝐹.

𝑥

]

exists.

3. Let

be the

𝐹.

𝑥

]

4. Assert: due to

𝑆.

]

exists.

5. Let

tab

be the

table instance

𝑆.

]

6. Assert: due to

𝐹.

𝑦

]

exists.

7. Let

be the

𝐹.

𝑦

]

8. Assert: due to

𝑆.

]

exists.

9. Let

elem

be the

element instance

𝑆.

]

10. Assert: due to

, a value of

is on the top of the stack.

11. Pop the value

𝑛

from the stack.

12. Assert: due to

, a value of

is on the top of the stack.

13. Pop the value

𝑠

from the stack.

14. Assert: due to

, a value of

is on the top of the stack.

15. Pop the value

𝑑

from the stack.

16. If

𝑠

𝑛

is larger than the length of

elem

𝑑

𝑛

is larger than the length of

tab

, then:

a. Trap.

17. If

𝑛

= 0

, then:

a. Return.

18. Let

be the

reference value

elem

𝑠

]

19. Push the value

𝑑

to the stack.

20. Push the value

to the stack.

21. Execute the instruction

set

𝑥

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

𝑑

+ 1

23. Push the value

(

𝑑

+ 1)

to the stack.

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

𝑠

+ 1

25. Push the value

(

𝑠

+ 1)

to the stack.

4.4. Instructions

103

26. Push the value

(

𝑛

−

to the stack.

27. Execute the instruction

𝑥 𝑦

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

𝑛

) (

𝑥 𝑦

)

𝑆

;

𝐹

(

𝑠

𝑛 >

𝑆.

𝐹.

𝑦

]]

∨

𝑑

𝑛 >

𝑆.

𝐹.

𝑥

]]

)

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

0) (

𝑥 𝑦

)

𝑆

;

𝐹

;

𝜖

(

otherwise

)

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

𝑛

+ 1) (

𝑥 𝑦

)

𝑆

;

𝐹

; (

𝑑

)

𝑥

)

𝑑

+ 1) (

𝑠

+ 1) (

𝑛

) (

𝑥 𝑦

)

(

otherwise

𝑆.

𝐹.

𝑦

]]

𝑠

])

𝑥

1. Let

𝐹

be the

2. Assert: due to

𝐹.

𝑥

]

exists.

3. Let

𝑎

be the

𝐹.

𝑥

]

4. Assert: due to

𝑆.

𝑎

]

exists.

5. Replace

𝑆.

𝑎

]

with the

element instance

𝜖

}

𝑆

;

𝐹

; (

𝑥

)

𝑆

′

;

𝐹

;

𝜖

(

𝑆

′

𝐹.

𝑥

]] =

𝜖

}

)

4.4.7 Memory Instructions

Note:

The alignment

align

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

mod 2

align

= 0

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

and

1. Let

𝐹

be the

2. Assert: due to

𝐹.

exists.

3. Let

𝑎

be the

𝐹.

4. Assert: due to

𝑆.

𝑎

]

exists.

5. Let

mem

be the

𝑆.

𝑎

]

6. Assert: due to

, a value of

is on the top of the stack.

7. Pop the value

𝑖

from the stack.

8. Let

be the integer

𝑖

9. If

𝑁

is not part of the instruction, then:

a. Let

𝑁

be the

bit width

𝑡

number type

𝑡

104

Chapter 4. Execution

10. If

𝑁/

is larger than the length of

mem

, then:

a. Trap.

11. Let

𝑏

be the byte sequence

mem

𝑁/

12. If

𝑁

and

are part of the instruction, then:

a. Let

𝑛

be the integer for which

𝑛

) =

𝑏

b. Let

𝑐

be the result of computing

𝑁,

𝑡

(

𝑛

)

13. Else:

a. Let

𝑐

be the constant for which

𝑡

(

𝑐

) =

𝑏

14. Push the value

𝑐

to the stack.

𝑆

;

𝐹

; (

𝑖

) (

𝑆

;

𝐹

; (

𝑐

)

(

𝑖

∧

𝑡

≤ |

𝑆.

𝐹.

∧

(

𝑐

) =

𝑆.

𝐹.

𝑡

8])

𝑆

;

𝐹

; (

𝑖

) (

𝑆

;

𝐹

; (

𝑡

(

𝑛

))

(

𝑖

∧

𝑁/

≤ |

𝑆.

𝐹.

∧

𝑛

) =

𝑆.

𝐹.

𝑁/

8])

𝑆

;

𝐹

; (

𝑘

) (

𝑁

𝑆

;

𝐹

(

otherwise

)

𝑁

1. Let

𝐹

be the

2. Assert: due to

𝐹.

exists.

3. Let

𝑎

be the

𝐹.

4. Assert: due to

𝑆.

𝑎

]

exists.

5. Let

mem

be the

𝑆.

𝑎

]

6. Assert: due to

, a value of

is on the top of the stack.

7. Pop the value

𝑖

from the stack.

8. Let

be the integer

𝑖

9. If

𝑀

𝑁/

is larger than the length of

mem

, then:

a. Trap.

10. Let

𝑏

be the byte sequence

mem

𝑀

𝑁/

11. Let

𝑚

𝑘

be the integer for which

𝑀

𝑚

𝑘

) =

𝑏

[

𝑘

𝑀/

12. Let

𝑊

be the integer

𝑀

13. Let

𝑛

𝑘

be the result of

𝑀,𝑊

(

𝑚

𝑘

)

14. Let

𝑐

be the result of computing

𝑊

𝑁

(

𝑛

. . . 𝑛

𝑁

−

)

15. Push the value

𝑐

to the stack.

4.4. Instructions

105

𝑆

;

𝐹

; (

𝑖

) (

𝑁

𝑆

;

𝐹

; (

𝑐

)

(

𝑖

∧

𝑀

𝑁/

≤ |

𝑆.

𝐹.

∧

𝑚

𝑘

) =

𝑆.

𝐹.

𝑘

𝑀/

8])

∧

𝑊

𝑀

∧

𝑐

𝑊

𝑁

𝑀,𝑊

(

𝑚

)

. . .

𝑀,𝑊

(

𝑚

𝑁

−

))

𝑆

;

𝐹

; (

𝑘

) (

𝑁

𝑆

;

𝐹

(

otherwise

)

splat

1. Let

𝐹

be the

2. Assert: due to

𝐹.

exists.

3. Let

𝑎

be the

𝐹.

4. Assert: due to

𝑆.

𝑎

]

exists.

5. Let

mem

be the

𝑆.

𝑎

]

6. Assert: due to

, a value of

is on the top of the stack.

7. Pop the value

𝑖

from the stack.

8. Let

be the integer

𝑖

9. If

𝑁/

is larger than the length of

mem

, then:

a. Trap.

10. Let

𝑏

be the byte sequence

mem

𝑁/

11. Let

𝑛

be the integer for which

𝑛

) =

𝑏

12. Let

𝐿

be the integer

128

/𝑁

13. Let

𝑐

be the result of computing

𝐿

(

𝑛

𝐿

)

14. Push the value

𝑐

to the stack.

𝑆

;

𝐹

; (

𝑖

) (

splat

𝑆

;

𝐹

; (

𝑐

)

(

𝑖

∧

𝑁/

≤ |

𝑆.

𝐹.

∧

𝑛

) =

𝑆.

𝐹.

𝑁/

8])

∧

𝑐

𝐿

(

𝑛

𝐿

)

𝑆

;

𝐹

; (

𝑘

) (

splat

𝑆

;

𝐹

(

otherwise

)

zero

1. Let

𝐹

be the

2. Assert: due to

𝐹.

exists.

3. Let

𝑎

be the

𝐹.

4. Assert: due to

𝑆.

𝑎

]

exists.

5. Let

mem

be the

𝑆.

𝑎

]

6. Assert: due to

, a value of

is on the top of the stack.

7. Pop the value

𝑖

from the stack.

8. Let

be the integer

𝑖

106

Chapter 4. Execution

9. If

𝑁/

is larger than the length of

mem

, then:

a. Trap.

10. Let

𝑏

be the byte sequence

mem

𝑁/

11. Let

𝑛

be the integer for which

𝑛

) =

𝑏

12. Let

𝑐

be the result of

𝑁,

128

(

𝑛

)

13. Push the value

𝑐

to the stack.

𝑆

;

𝐹

; (

𝑖

) (

zero

𝑆

;

𝐹

; (

𝑐

)

(

𝑖

∧

𝑁/

≤ |

𝑆.

𝐹.

∧

𝑛

) =

𝑆.

𝐹.

𝑁/

8])

∧

𝑐

𝑁,

128

(

𝑛

)

𝑆

;

𝐹

; (

𝑘

) (

zero

𝑆

;

𝐹

(

otherwise

)

lane

𝑥

1. Let

𝐹

be the

2. Assert: due to

𝐹.

exists.

3. Let

𝑎

be the

𝐹.

4. Assert: due to

𝑆.

𝑎

]

exists.

5. Let

mem

be the

𝑆.

𝑎

]

6. Assert: due to

, a value of

is on the top of the stack.

7. Pop the value

𝑣

from the stack.

8. Assert: due to

, a value of

is on the top of the stack.

9. Pop the value

𝑖

from the stack.

10. Let

be the integer

𝑖

11. If

𝑁/

is larger than the length of

mem

, then:

a. Trap.

12. Let

𝑏

be the byte sequence

mem

𝑁/

13. Let

𝑟

be the constant for which

𝑟

) =

𝑏

14. Let

𝐿

128

/𝑁

15. Let

𝑐

be the result of computing

𝑁

𝐿

𝑁

𝐿

(

𝑣

)

with

[

𝑥

] =

𝑟

)

16. Push the value

𝑐

to the stack.

𝑆

;

𝐹

; (

𝑖

) (

𝑣

) (

lane

𝑥

)

𝑆

;

𝐹

; (

𝑐

)

(

𝑖

∧

𝑁/

≤ |

𝑆.

𝐹.

∧

𝑟

) =

𝑆.

𝐹.

𝑁/

8])

∧

𝐿

= 128

/𝑁

∧

𝑐

𝑁

𝐿

𝑁

𝐿

(

𝑣

)

with

[

𝑥

] =

𝑟

)

𝑆

;

𝐹

; (

𝑘

) (

𝑣

) (

lane

𝑥

)

𝑆

;

𝐹

(

otherwise

)

4.4. Instructions

107

and

1. Let

𝐹

be the

2. Assert: due to

𝐹.

exists.

3. Let

𝑎

be the

𝐹.

4. Assert: due to

𝑆.

𝑎

]

exists.

5. Let

mem

be the

𝑆.

𝑎

]

6. Assert: due to

, a value of

𝑡

is on the top of the stack.

7. Pop the value

𝑐

from the stack.

8. Assert: due to

, a value of

is on the top of the stack.

9. Pop the value

𝑖

from the stack.

10. Let

be the integer

𝑖

11. If

𝑁

is not part of the instruction, then:

a. Let

𝑁

be the

bit width

𝑡

number type

𝑡

12. If

𝑁/

is larger than the length of

mem

, then:

a. Trap.

13. If

𝑁

is part of the instruction, then:

a. Let

𝑛

be the result of computing

wrap

𝑡

,𝑁

(

𝑐

)

b. Let

𝑏

be the byte sequence

𝑛

)

14. Else:

a. Let

𝑏

be the byte sequence

𝑡

(

𝑐

)

15. Replace the bytes

mem

𝑁/

with

𝑏

𝑆

;

𝐹

; (

𝑖

) (

𝑐

) (

𝑆

′

;

𝐹

;

𝜖

(

𝑖

∧

𝑡

≤ |

𝑆.

𝐹.

∧

𝑆

′

𝐹.

𝑡

8] =

𝑡

(

𝑐

))

𝑆

;

𝐹

; (

𝑖

) (

𝑐

) (

𝑆

′

;

𝐹

;

𝜖

(

𝑖

∧

𝑁/

≤ |

𝑆.

𝐹.

∧

𝑆

′

𝐹.

𝑁/

8] =

𝑡

,𝑁

(

𝑐

))

𝑆

;

𝐹

; (

𝑘

) (

𝑐

) (

𝑆

;

𝐹

(

otherwise

)

lane

𝑥

1. Let

𝐹

be the

2. Assert: due to

𝐹.

exists.

3. Let

𝑎

be the

𝐹.

4. Assert: due to

𝑆.

𝑎

]

exists.

5. Let

mem

be the

𝑆.

𝑎

]

6. Assert: due to

, a value of

is on the top of the stack.

7. Pop the value

𝑐

from the stack.

108

Chapter 4. Execution

8. Assert: due to

, a value of

is on the top of the stack.

9. Pop the value

𝑖

from the stack.

10. Let

be the integer

𝑖

11. If

𝑁/

is larger than the length of

mem

, then:

a. Trap.

12. Let

𝐿

128

/𝑁

13. Let

𝑏

be the byte sequence

𝑁

𝐿

(

𝑐

)[

𝑥

])

14. Replace the bytes

mem

𝑁/

with

𝑏

𝑆

;

𝐹

; (

𝑖

) (

𝑐

) (

lane

𝑥

)

𝑆

′

;

𝐹

;

𝜖

(

𝑖

∧

𝑁

≤ |

𝑆.

𝐹.

∧

𝐿

= 128

/𝑁

∧

𝑆

′

𝐹.

𝑁/

8] =

𝑁

𝐿

(

𝑐

)[

𝑥

])

𝑆

;

𝐹

; (

𝑘

) (

𝑐

) (

lane

𝑥

)

𝑆

;

𝐹

(

otherwise

)

size

1. Let

𝐹

be the

2. Assert: due to

𝐹.

exists.

3. Let

𝑎

be the

𝐹.

4. Assert: due to

𝑆.

𝑎

]

exists.

5. Let

mem

be the

𝑆.

𝑎

]

6. Let

be the length of

mem

divided by the

7. Push the value

to the stack.

𝑆

;

𝐹

𝑆

;

𝐹

; (

)

(

𝑆.

𝐹.

64 Ki)

1. Let

𝐹

be the

2. Assert: due to

𝐹.

exists.

3. Let

𝑎

be the

𝐹.

4. Assert: due to

𝑆.

𝑎

]

exists.

5. Let

mem

be the

𝑆.

𝑎

]

6. Let

be the length of

𝑆.

𝑎

]

divided by the

7. Assert: due to

, a value of

is on the top of the stack.

8. Pop the value

𝑛

from the stack.

9. Let

err

be the

value

−

, for which

signed

(

err

)

−

10. Either, try

growing

mem

𝑛

pages

a. If it succeeds, push the value

to the stack.

b. Else, push the value

err

to the stack.

4.4. Instructions

109

11. Or, push the value

err

to the stack.

𝑆

;

𝐹

; (

𝑛

)

grow

𝑆

′

;

𝐹

; (

)

(

𝐹.

module

memaddrs

[0] =

𝑎

∧

𝑆.

𝑎

]

64 Ki

∧

𝑆

′

𝑎

] =

𝑆.

𝑎

]

, 𝑛

))

𝑆

;

𝐹

; (

𝑛

)

grow

𝑆

;

𝐹

; (

(

−

1))

Note:

The

grow

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

, or fail, returning

−

. Failure

must

occur if the referenced memory instance has a maximum size defined that

would be exceeded. However, failure

can

occur in other cases as well. In practice, the choice depends on the

available to the

1. Let

𝐹

be the

2. Assert: due to

𝐹.

exists.

3. Let

be the

𝐹.

4. Assert: due to

𝑆.

]

exists.

5. Let

mem

be the

𝑆.

]

6. Assert: due to

, a value of

is on the top of the stack.

7. Pop the value

𝑛

from the stack.

8. Assert: due to

, a value of

is on the top of the stack.

9. Pop the value

from the stack.

10. Assert: due to

, a value of

is on the top of the stack.

11. Pop the value

𝑑

from the stack.

12. If

𝑑

𝑛

is larger than the length of

mem

, then:

a. Trap.

13. If

𝑛

= 0

, then:

a. Return.

14. Push the value

𝑑

to the stack.

15. Push the value

to the stack.

16. Execute the instruction

}

17. Assert: due to the earlier check against the memory size,

𝑑

+ 1

18. Push the value

(

𝑑

+ 1)

to the stack.

19. Push the value

to the stack.

20. Push the value

(

𝑛

−

to the stack.

21. Execute the instruction

110

Chapter 4. Execution

𝑆

;

𝐹

; (

𝑑

)

𝑛

)

𝑆

;

𝐹

(

𝑑

𝑛 >

𝑆.

𝐹.

𝑥

]]

)

𝑆

;

𝐹

; (

𝑑

)

𝑆

;

𝐹

;

𝜖

(

otherwise

)

𝑆

;

𝐹

; (

𝑑

)

𝑛

+ 1)

𝑆

;

𝐹

; (

𝑑

)

}

)

𝑑

+ 1)

𝑛

)

(

otherwise

)

1. Let

𝐹

be the

2. Assert: due to

𝐹.

exists.

3. Let

be the

𝐹.

4. Assert: due to

𝑆.

]

exists.

5. Let

mem

be the

𝑆.

]

6. Assert: due to

, a value of

is on the top of the stack.

7. Pop the value

𝑛

from the stack.

8. Assert: due to

, a value of

is on the top of the stack.

9. Pop the value

𝑠

from the stack.

10. Assert: due to

, a value of

is on the top of the stack.

11. Pop the value

𝑑

from the stack.

12. If

𝑠

𝑛

is larger than the length of

mem

𝑑

𝑛

is larger than the length of

mem

, then:

a. Trap.

13. If

𝑛

= 0

, then:

a. Return.

14. If

𝑑

≤

𝑠

, then:

a. Push the value

𝑑

to the stack.

b. Push the value

𝑠

to the stack.

c. Execute the instruction

}

d. Execute the instruction

}

e. Assert: due to the earlier check against the memory size,

𝑑

+ 1

f. Push the value

(

𝑑

+ 1)

to the stack.

g. Assert: due to the earlier check against the memory size,

𝑠

+ 1

h. Push the value

(

𝑠

+ 1)

to the stack.

15. Else:

a. Assert: due to the earlier check against the memory size,

𝑑

𝑛

−

b. Push the value

(

𝑑

𝑛

−

to the stack.

c. Assert: due to the earlier check against the memory size,

𝑠

𝑛

−

d. Push the value

(

𝑠

𝑛

−

to the stack.

e. Execute the instruction

}

4.4. Instructions

111

f. Execute the instruction

}

g. Push the value

𝑑

to the stack.

h. Push the value

𝑠

to the stack.

16. Push the value

(

𝑛

−

to the stack.

17. Execute the instruction

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

𝑛

)

𝑆

;

𝐹

(

𝑠

𝑛 >

𝑆.

𝐹.

∨

𝑑

𝑛 >

𝑆.

𝐹.

)

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

𝑆

;

𝐹

;

𝜖

(

otherwise

)

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

𝑛

+ 1)

𝑆

;

𝐹

; (

𝑑

)

𝑠

) (

}

)

}

)

𝑑

+ 1) (

𝑠

+ 1) (

𝑛

)

(

otherwise

𝑑

≤

𝑠

)

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

𝑛

+ 1)

𝑆

;

𝐹

; (

𝑑

𝑛

−

𝑠

𝑛

−

1) (

}

)

}

)

𝑑

) (

𝑠

) (

𝑛

)

(

otherwise

𝑑 > 𝑠

)

𝑥

1. Let

𝐹

be the

2. Assert: due to

𝐹.

exists.

3. Let

be the

𝐹.

4. Assert: due to

𝑆.

]

exists.

5. Let

mem

be the

𝑆.

]

6. Assert: due to

𝐹.

𝑥

]

exists.

7. Let

be the

𝐹.

𝑥

]

8. Assert: due to

𝑆.

]

exists.

9. Let

data

be the

data instance

𝑆.

]

10. Assert: due to

, a value of

is on the top of the stack.

11. Pop the value

𝑛

from the stack.

12. Assert: due to

, a value of

is on the top of the stack.

13. Pop the value

𝑠

from the stack.

14. Assert: due to

, a value of

is on the top of the stack.

15. Pop the value

𝑑

from the stack.

16. If

𝑠

𝑛

is larger than the length of

data

𝑑

𝑛

is larger than the length of

mem

, then:

a. Trap.

17. If

𝑛

= 0

, then:

a. Return.

112

Chapter 4. Execution

18. Let

𝑏

be the byte

data

𝑠

]

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 memory size,

𝑑

+ 1

23. Push the value

(

𝑑

+ 1)

to the stack.

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

𝑠

+ 1

25. Push the value

(

𝑠

+ 1)

to the stack.

26. Push the value

(

𝑛

−

to the stack.

27. Execute the instruction

𝑥

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

𝑛

) (

𝑥

)

𝑆

;

𝐹

(

𝑠

𝑛 >

𝑆.

𝐹.

𝑥

]]

∨

𝑑

𝑛 >

𝑆.

𝐹.

𝑥

]]

)

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

0) (

𝑥

)

𝑆

;

𝐹

;

𝜖

(

otherwise

)

𝑆

;

𝐹

; (

𝑑

) (

𝑠

) (

𝑛

+ 1) (

𝑥

)

𝑆

;

𝐹

; (

𝑑

) (

𝑏

) (

}

)

𝑑

+ 1) (

𝑠

+ 1) (

𝑛

) (

𝑥

)

(

otherwise

𝑏

𝑆.

𝐹.

𝑥

]]

𝑠

])

𝑥

1. Let

𝐹

be the

2. Assert: due to

𝐹.

𝑥

]

exists.

3. Let

𝑎

be the

𝐹.

𝑥

]

4. Assert: due to

𝑆.

𝑎

]

exists.

5. Replace

𝑆.

𝑎

]

with the

data instance

𝜖

}

𝑆

;

𝐹

; (

𝑥

)

𝑆

′

;

𝐹

;

𝜖

(

𝑆

′

𝐹.

𝑥

]] =

𝜖

}

)

4.4.8 Control Instructions

nop

1. Do nothing.

nop

𝜖

4.4. Instructions

113

1. Trap.

1. Assert: due to

is defined.

2. Let

[

𝑡

𝑚

[

𝑡

𝑛

]

be the

3. Let

𝐿

be the label whose arity is

𝑛

and whose continuation is the end of the block.

4. Assert: due to

, there are at least

𝑚

values on the top of the stack.

5. Pop the values

from the stack.

the block

with label

𝐿

𝐹

𝐹

{

𝜖

}

(

(

) = [

𝑡

𝑚

[

𝑡

𝑛

])

1. Assert: due to

is defined.

2. Let

[

𝑡

𝑚

[

𝑡

𝑛

]

be the

3. Let

𝐿

be the label whose arity is

𝑚

and whose continuation is the start of the loop.

4. Assert: due to

, there are at least

𝑚

values on the top of the stack.

5. Pop the values

from the stack.

the block

with label

𝐿

𝐹

𝐹

(

(

) = [

𝑡

𝑚

[

𝑡

𝑛

])

1. Assert: due to

is defined.

2. Let

[

𝑡

𝑚

[

𝑡

𝑛

]

be the

3. Let

𝐿

be the label whose arity is

𝑛

and whose continuation is the end of the

instruction.

4. Assert: due to

, a value of

is on the top of the stack.

5. Pop the value

𝑐

from the stack.

6. Assert: due to

, there are at least

𝑚

values on the top of the stack.

7. Pop the values

𝑚

from the stack.

8. If

𝑐

is non-zero, then:

the block

with label

𝐿

9. Else:

the block

with label

𝐿

114

Chapter 4. Execution

𝐹

𝑐

)

𝐹

{

𝜖

}

(

𝑐

= 0

∧

expand

𝐹

(

) = [

𝑡

𝑚

[

𝑡

𝑛

])

𝐹

𝑐

)

𝐹

{

𝜖

}

(

𝑐

= 0

∧

expand

𝐹

(

) = [

𝑡

𝑚

[

𝑡

𝑛

])

𝑙

1. Assert: due to

, the stack contains at least

𝑙

+ 1

labels.

2. Let

𝐿

be the

𝑙

-th label appearing on the stack, starting from the top and counting from zero.

3. Let

𝑛

be the arity of

𝐿

4. Assert: due to

, there are at least

𝑛

values on the top of the stack.

5. Pop the values

from the stack.

6. Repeat

𝑙

+ 1

times:

a. While the top of the stack is a value, do:

i. Pop the value from the stack.

b. Assert: due to

, the top of the stack now is a label.

c. Pop the label from the stack.

7. Push the values

to the stack.

8. Jump to the continuation of

𝐿

}

𝑙

)]

𝑙

1. Assert: due to

, a value of

is on the top of the stack.

2. Pop the value

𝑐

from the stack.

3. If

𝑐

is non-zero, then:

Execute

the instruction

𝑙

)

4. Else:

a. Do nothing.

𝑐

) (

𝑙

)

𝑙

)

(

𝑐

= 0)

𝑐

) (

𝑙

)

𝜖

(

𝑐

= 0)

𝑙

𝑁

1. Assert: due to

, a value of

is on the top of the stack.

2. Pop the value

𝑖

from the stack.

3. If

𝑖

is smaller than the length of

𝑙

, then:

a. Let

𝑙

𝑖

be the label

𝑙

[

𝑖

]

Execute

the instruction

𝑙

𝑖

)

4. Else:

Execute

the instruction

𝑙

𝑁

)

4.4. Instructions

115

𝑖

) (

𝑙

𝑁

)

𝑙

𝑖

)

(

𝑙

[

𝑖

] =

𝑙

𝑖

)

𝑖

) (

𝑙

𝑁

)

𝑙

𝑁

)

(

𝑙

| ≤

𝑖

)

return

1. Let

𝐹

be the

current frame

2. Let

𝑛

be the arity of

𝐹

3. Assert: due to

, there are at least

𝑛

values on the top of the stack.

4. Pop the results

from the stack.

5. Assert: due to

, the stack contains at least one

frame

6. While the top of the stack is not a frame, do:

a. Pop the top element from the stack.

7. Assert: the top of the stack is the frame

𝐹

8. Pop the frame from the stack.
9. Push

to the stack.

10. Jump to the instruction after the original call that pushed the frame.

frame

{

𝐹

}

𝑥

1. Let

𝐹

be the

2. Assert: due to

𝐹.

𝑥

]

exists.

3. Let

𝑎

be the

𝐹.

𝑥

]

Invoke

the function instance at address

𝑎

𝐹

; (

𝑥

)

𝐹

; (

invoke

𝑎

)

(

𝐹.

module

funcaddrs

𝑥

] =

𝑎

)

indirect

𝑥 𝑦

1. Let

𝐹

be the

2. Assert: due to

𝐹.

𝑥

]

exists.

3. Let

be the

𝐹.

𝑥

]

4. Assert: due to

𝑆.

]

exists.

5. Let

tab

be the

table instance

𝑆.

]

6. Assert: due to

𝐹.

𝑦

]

exists.

7. Let

expect

be the

𝐹.

𝑦

]

8. Assert: due to

, a value with

is on the top of the stack.

9. Pop the value

𝑖

from the stack.

10. If

𝑖

is not smaller than the length of

tab

, then:

a. Trap.

11. Let

𝑟

be the

reference

tab

validation of table mutation

𝑖

]

12. If

𝑟

ref

null

𝑡

, then:

116

Chapter 4. Execution

a. Trap.

13. Assert: due to

𝑟

is a

function reference

14. Let

ref

𝑎

be the

function reference

𝑟

15. Assert: due to

validation of table mutation

𝑆.

𝑎

]

exists.

16. Let

be the

function instance

𝑆.

𝑎

]

17. Let

actual

be the

function type

18. If

actual

and

expect

differ, then:

a. Trap.

19.

Invoke

the function instance at address

𝑎

𝑆

;

𝐹

; (

𝑖

) (

indirect

𝑥 𝑦

)

𝑆

;

𝐹

; (

invoke

𝑎

)

(

𝑆.

𝐹.

𝑥

]]

𝑖

] =

ref

𝑎

∧

𝑆.

𝑎

] =

𝑓

∧

𝐹.

module

types

𝑦

] =

𝑓.

)

𝑆

;

𝐹

; (

𝑖

) (

indirect

𝑥 𝑦

)

𝑆

;

𝐹

(

otherwise

)

4.4.9 Blocks

The following auxiliary rules define the semantics of executing an

instruction sequence

that forms a

block

Entering

with label

𝐿

1. Push

𝐿

to the stack.

2. Jump to the start of the instruction sequence

administrative instruction

Note:

No formal reduction rule is needed for entering an instruction sequence, because the label

𝐿

is embedded

in the

that structured control instructions reduce to directly.

Exiting

with label

𝐿

When the end of a block is reached without a jump or trap aborting it, then the following steps are performed.

1. Let

𝑚

be the number of values on the top of the stack.

2. Pop the values

𝑚

from the stack.

3. Assert: due to

, the label

𝐿

is now on the top of the stack.

4. Pop the label from the stack.
5. Push

structured control instruction

𝑚

back to the stack.

6. Jump to the position after the

end

of the

associated with the label

𝐿

}

Note:

This semantics also applies to the instruction sequence contained in a

loop

instruction. Therefore, execution

of a loop falls off the end, unless a backwards branch is performed explicitly.

4.4. Instructions

117

4.4.10 Function Calls

The following auxiliary rules define the semantics of invoking a

function instance

through one of the

call instruc-

tions

and returning from it.

Invocation of function address

𝑎

1. Assert: due to

𝑆.

𝑎

]

exists.

2. Let

𝑓

be the

function instance

𝑆.

𝑎

]

3. Let

[

𝑡

𝑛

[

𝑡

𝑚

]

be the

function type

𝑓.

4. Let

𝑡

be the list of

𝑓.

5. Let

be the

𝑓.

6. Assert: due to

𝑛

values are on the top of the stack.

7. Pop the values

from the stack.

8. Let

be the list of zero values of types

𝑡

9. Let

𝐹

be the

𝑓.

)

}

10. Push the activation of

𝐹

with arity

𝑚

to the stack.

11. Let

𝐿

be the

label

whose arity is

𝑚

and whose continuation is the end of the function.

12.

Enter

the instruction sequence

with label

𝐿

𝑆

𝑎

)

𝑆

{

𝐹

}

{}

(

𝑆.

𝑎

] =

𝑓

∧

𝑓.

= [

𝑡

𝑛

[

𝑡

𝑚

]

∧

𝑓.

𝑡

𝑘

∧

𝐹

𝑓.

)

𝑘

}

)

Returning from a function

When the end of a function is reached without a jump (i.e.,

return

) or trap aborting it, then the following steps are

performed.

1. Let

𝐹

be the

current frame

2. Let

𝑛

be the arity of the activation of

𝐹

3. Assert: due to

, there are

𝑛

values on the top of the stack.

4. Pop the results

from the stack.

5. Assert: due to

, the frame

𝐹

is now on the top of the stack.

6. Pop the frame from the stack.
7. Push

back to the stack.

8. Jump to the instruction after the original call.

frame