From 9789e1758434c22d7366d18c6a6997571b129884 Mon Sep 17 00:00:00 2001 From: B Szilvasy Date: Wed, 26 Oct 2022 00:35:54 +0100 Subject: [PATCH 01/20] [test] Tweak binary-leb128 and simd_lane (#1555) --- test/core/binary-leb128.wast | 2 +- test/core/simd/simd_lane.wast | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/test/core/binary-leb128.wast b/test/core/binary-leb128.wast index 1d67219583..1b642261ae 100644 --- a/test/core/binary-leb128.wast +++ b/test/core/binary-leb128.wast @@ -290,7 +290,7 @@ (assert_malformed (module binary "\00asm" "\01\00\00\00" - "\01\08\01" ;; type section + "\01\0c\01" ;; type section "\60" ;; func type "\02" ;; num params "\7f\7e" ;; param type diff --git a/test/core/simd/simd_lane.wast b/test/core/simd/simd_lane.wast index 9d4b5fd729..9b66f53b1a 100644 --- a/test/core/simd/simd_lane.wast +++ b/test/core/simd/simd_lane.wast @@ -447,8 +447,8 @@ (assert_invalid (module (func (result v128) (i16x8.replace_lane 255 (v128.const i16x8 0 0 0 0 0 0 0 0) (i32.const 1)))) "invalid lane index") (assert_invalid (module (func (result v128) (i32x4.replace_lane 4 (v128.const i32x4 0 0 0 0) (i32.const 1)))) "invalid lane index") (assert_invalid (module (func (result v128) (i32x4.replace_lane 255 (v128.const i32x4 0 0 0 0) (i32.const 1)))) "invalid lane index") -(assert_invalid (module (func (result v128) (f32x4.replace_lane 4 (v128.const f32x4 0 0 0 0) (i32.const 1)))) "invalid lane index") -(assert_invalid (module (func (result v128) (f32x4.replace_lane 255 (v128.const f32x4 0 0 0 0) (i32.const 1)))) "invalid lane index") +(assert_invalid (module (func (result v128) (f32x4.replace_lane 4 (v128.const f32x4 0 0 0 0) (f32.const 1)))) "invalid lane index") +(assert_invalid (module (func (result v128) (f32x4.replace_lane 255 (v128.const f32x4 0 0 0 0) (f32.const 1)))) "invalid lane index") (assert_invalid (module (func (result i64) (i64x2.extract_lane 2 (v128.const i64x2 0 0)))) "invalid lane index") (assert_invalid (module (func (result i64) (i64x2.extract_lane 255 (v128.const i64x2 0 0)))) "invalid lane index") (assert_invalid (module (func (result f64) (f64x2.extract_lane 2 (v128.const f64x2 0 0)))) "invalid lane index") @@ -466,7 +466,7 @@ (assert_invalid (module (func (result i32) (f32x4.extract_lane 4 (v128.const i8x16 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)))) "invalid lane index") (assert_invalid (module (func (result v128) (i16x8.replace_lane 8 (v128.const i8x16 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0) (i32.const 1)))) "invalid lane index") (assert_invalid (module (func (result v128) (i32x4.replace_lane 4 (v128.const i8x16 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0) (i32.const 1)))) "invalid lane index") -(assert_invalid (module (func (result v128) (f32x4.replace_lane 4 (v128.const i8x16 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0) (i32.const 1)))) "invalid lane index") +(assert_invalid (module (func (result v128) (f32x4.replace_lane 4 (v128.const i8x16 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0) (f32.const 1)))) "invalid lane index") (assert_invalid (module (func (result i64) (i64x2.extract_lane 2 (v128.const i64x2 0 0)))) "invalid lane index") (assert_invalid (module (func (result f64) (f64x2.extract_lane 2 (v128.const f64x2 0 0)))) "invalid lane index") (assert_invalid (module (func (result v128) (i64x2.replace_lane 2 (v128.const i64x2 0 0) (i64.const 1)))) "invalid lane index") From 1831a38898f7b2a509cc8c4229ee315948fc679c Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Fri, 28 Oct 2022 00:26:35 -0500 Subject: [PATCH 02/20] [spec] Allow explicit keyword definitions (#1553) Rather than describing keyword tokens as always being defined implicitly by terminal symbols in syntactic productions, describe them as being defined implicitly or explicitly. This accounts for the explicit definitions of `offset` and `align` phrases, which are lexically keywords, later in the chapter. Fixes #1552. --- document/core/text/lexical.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/text/lexical.rst b/document/core/text/lexical.rst index 0c40a58d15..f466466622 100644 --- a/document/core/text/lexical.rst +++ b/document/core/text/lexical.rst @@ -58,7 +58,7 @@ That is, the next token always consists of the longest possible sequence of char Tokens can be separated by :ref:`white space `, but except for strings, they cannot themselves contain whitespace. -The set of *keyword* tokens is defined implicitly, by all occurrences of a :ref:`terminal symbol ` in literal form, such as :math:`\text{keyword}`, in a :ref:`syntactic ` production of this chapter. +*Keyword* tokens are defined either implicitly by an occurrence of a :ref:`terminal symbol ` in literal form, such as :math:`\text{keyword}`, in a :ref:`syntactic ` production of this chapter, or explicitly where they arise in this chapter. Any token that does not fall into any of the other categories is considered *reserved*, and cannot occur in source text. From f9b461a312426a60f2f81dcb19b39b66b90a5447 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Tue, 8 Nov 2022 11:50:50 -0800 Subject: [PATCH 03/20] [js-api] editorial: adjust link for v128 type --- document/js-api/index.bs | 1 + 1 file changed, 1 insertion(+) diff --git a/document/js-api/index.bs b/document/js-api/index.bs index fcfdbf8335..b22e825ca3 100644 --- a/document/js-api/index.bs +++ b/document/js-api/index.bs @@ -157,6 +157,7 @@ urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: df text: i64 text: f32 text: f64 + url: syntax/types.html#vector-types text: v128 url: syntax/types.html#syntax-reftype text: reftype From ff149b4c52c6bccd1c6a00eec984535c0e0d8a0b Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 5 Dec 2022 17:57:38 +0100 Subject: [PATCH 04/20] [spec] Add missing case for declarative elem segments Fixes #1562. --- document/core/exec/modules.rst | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 4242488dbd..16cd23fe2d 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -655,7 +655,7 @@ It is up to the :ref:`embedder ` to define how such conditions are rep 13. Push the frame :math:`F` to the stack. -14. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode ` is of the form :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{einstr}^\ast_i~\END \}`, do: +14. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode ` is either of the form :math:`\EDECLARATIVE` or :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{einstr}^\ast_i~\END \}`, do: a. Let :math:`n` be the length of the vector :math:`\elem_i.\EINIT`. @@ -685,15 +685,19 @@ It is up to the :ref:`embedder ` to define how such conditions are rep g. :ref:`Execute ` the instruction :math:`\DATADROP~i`. -16. If the :ref:`start function ` :math:`\module.\MSTART` is not empty, then: +16. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATAS` whose :ref:`mode ` is of the form :math:`\DDECLARATIVE`, do: + + a. :ref:`Execute ` the instruction :math:`\DATADROP~i`. + +17. If the :ref:`start function ` :math:`\module.\MSTART` is not empty, then: a. Let :math:`\start` be the :ref:`start function ` :math:`\module.\MSTART`. b. :ref:`Execute ` the instruction :math:`\CALL~\start.\SFUNC`. -17. Assert: due to :ref:`validation `, the frame :math:`F` is now on the top of the stack. +18. Assert: due to :ref:`validation `, the frame :math:`F` is now on the top of the stack. -18. Pop the frame :math:`F` from the stack. +19. Pop the frame :math:`F` from the stack. .. math:: From 11c4cc25df26182b56040b2b3c65fe03a0ff101b Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 5 Dec 2022 18:10:42 +0100 Subject: [PATCH 05/20] [spec] Hotfix last accidental commit --- document/core/exec/modules.rst | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 16cd23fe2d..4dfdb97351 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -655,7 +655,7 @@ It is up to the :ref:`embedder ` to define how such conditions are rep 13. Push the frame :math:`F` to the stack. -14. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode ` is either of the form :math:`\EDECLARATIVE` or :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{einstr}^\ast_i~\END \}`, do: +14. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode ` is of the form :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{einstr}^\ast_i~\END \}`, do: a. Let :math:`n` be the length of the vector :math:`\elem_i.\EINIT`. @@ -669,7 +669,11 @@ It is up to the :ref:`embedder ` to define how such conditions are rep f. :ref:`Execute ` the instruction :math:`\ELEMDROP~i`. -15. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATAS` whose :ref:`mode ` is of the form :math:`\DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{dinstr}^\ast_i~\END \}`, do: +15. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode ` is of the form :math:`\EDECLARATIVE`, do: + + a. :ref:`Execute ` the instruction :math:`\ELEMDROP~i`. + +16. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATAS` whose :ref:`mode ` is of the form :math:`\DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{dinstr}^\ast_i~\END \}`, do: a. Assert: :math:`\memidx_i` is :math:`0`. @@ -685,10 +689,6 @@ It is up to the :ref:`embedder ` to define how such conditions are rep g. :ref:`Execute ` the instruction :math:`\DATADROP~i`. -16. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATAS` whose :ref:`mode ` is of the form :math:`\DDECLARATIVE`, do: - - a. :ref:`Execute ` the instruction :math:`\DATADROP~i`. - 17. If the :ref:`start function ` :math:`\module.\MSTART` is not empty, then: a. Let :math:`\start` be the :ref:`start function ` :math:`\module.\MSTART`. From 6cc9fa15b4fee6d9e6ecc7bc7522802adef970d8 Mon Sep 17 00:00:00 2001 From: Michael Ficarra Date: Mon, 5 Dec 2022 10:10:57 -0800 Subject: [PATCH 06/20] [spec] Fix hyperref (#1563) --- document/core/exec/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index c7586d074c..c253a17eda 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2679,7 +2679,7 @@ Control Instructions :math:`\BRTABLE~l^\ast~l_N` ........................... -1. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +1. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. 2. Pop the value :math:`\I32.\CONST~i` from the stack. From 1fb0f3ea01e2afc8f61c04eb4665607a8bf359b4 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 5 Dec 2022 19:23:18 +0100 Subject: [PATCH 07/20] [spec] Bump sphinx version to fix Python problem --- .github/workflows/main.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 9a7a111a15..00b70e8f03 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -63,7 +63,7 @@ jobs: - run: pip install bikeshed && bikeshed update - run: pip install six - run: sudo apt-get update -y && sudo apt-get install -y latexmk texlive-latex-recommended texlive-latex-extra texlive-fonts-recommended - - run: pip install sphinx==4.0.0 + - run: pip install sphinx==5.1.0 - run: cd document/core && make all - uses: actions/upload-artifact@v2 with: From 62aa16e9085999dfd66d32b9a12f76f26605a7b8 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 7 Dec 2022 18:29:56 +0100 Subject: [PATCH 08/20] [spec] Fix minor errors and inconsistencies (#1564) --- document/core/appendix/properties.rst | 2 +- document/core/exec/instructions.rst | 46 ++++++++++--------- document/core/exec/runtime.rst | 66 +++++++++++++-------------- document/core/valid/instructions.rst | 2 +- 4 files changed, 59 insertions(+), 57 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index c378232192..d9b6a35487 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -237,7 +237,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co :ref:`Memory Instances ` :math:`\{ \MITYPE~\limits, \MIDATA~b^\ast \}` ...................................................................................... -* The :ref:`memory type ` :math:`\{\LMIN~n, \LMAX~m^?\}` must be :ref:`valid `. +* The :ref:`memory type ` :math:`\limits` must be :ref:`valid `. * The length of :math:`b^\ast` must equal :math:`\limits.\LMIN` multiplied by the :ref:`page size ` :math:`64\,\F{Ki}`. diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index c253a17eda..6b0280603c 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1256,7 +1256,7 @@ Table Instructions .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; \TABLESIZE~x &\stepto& S; F; (\I32.\CONST~\X{sz}) + S; F; (\TABLESIZE~x) &\stepto& S; F; (\I32.\CONST~\X{sz}) \end{array} \\ \qquad (\iff |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM| = \X{sz}) \\ @@ -1288,19 +1288,21 @@ Table Instructions 10. Pop the value :math:`\val` from the stack. -11. Either, try :ref:`growing ` :math:`\X{table}` by :math:`n` entries with initialization value :math:`\val`: +11. Let :math:`\X{err}` be the |i32| value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`. + +12. Either, try :ref:`growing ` :math:`\X{table}` by :math:`n` entries with initialization value :math:`\val`: a. If it succeeds, push the value :math:`\I32.\CONST~\X{sz}` to the stack. - b. Else, push the value :math:`\I32.\CONST~(-1)` to the stack. + b. Else, push the value :math:`\I32.\CONST~\X{err}` to the stack. -12. Or, push the value :math:`\I32.\CONST~(-1)` to the stack. +13. Or, push the value :math:`\I32.\CONST~\X{err}` to the stack. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; \val~(\I32.\CONST~n)~\TABLEGROW~x &\stepto& S'; F; (\I32.\CONST~\X{sz}) + S; F; \val~(\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S'; F; (\I32.\CONST~\X{sz}) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -1310,7 +1312,7 @@ Table Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~n)~\TABLEGROW~x &\stepto& S; F; (\I32.\CONST~{-1}) + S; F; (\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\I32.\CONST~\signed_{32}^{-1}(-1)) \end{array} \end{array} @@ -1511,7 +1513,7 @@ Table Instructions \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d+n-1)~(\I32.\CONST~s+n-1)~(\TABLEGET~y)~(\TABLESET~x) \\ + (\I32.\CONST~d+n)~(\I32.\CONST~s+n)~(\TABLEGET~y)~(\TABLESET~x) \\ (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLECOPY~x~y) \\ \end{array} \\ \qquad @@ -1722,7 +1724,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(t.\LOAD({N}\K{\_}\sx)^?~\memarg) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(t.\LOAD({N}\K{\_}\sx)^?~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -1783,7 +1785,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(\V128.\LOAD{M}\K{x}N\K{\_}\sx~\memarg) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(\V128.\LOAD{M}\K{x}N\K{\_}\sx~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -1840,7 +1842,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(\V128.\LOAD{N}\K{\_splat}~\memarg) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(\V128.\LOAD{N}\K{\_splat}~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -1895,7 +1897,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(\V128.\LOAD{N}\K{\_zero}~\memarg) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(\V128.\LOAD{N}\K{\_zero}~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -1957,7 +1959,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(\V128.\CONST~v)~(\V128.\LOAD{N}\K{\_lane}~\memarg~x) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(\V128.\CONST~v)~(\V128.\LOAD{N}\K{\_lane}~\memarg~x) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -2034,7 +2036,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(t.\CONST~c)~(t.\STORE{N}^?~\memarg) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(t.\CONST~c)~(t.\STORE{N}^?~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -2091,7 +2093,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~k)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~\memarg~x) &\stepto& S; F; \TRAP + S; F; (\I32.\CONST~i)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~\memarg~x) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -2368,8 +2370,8 @@ Memory Instructions \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d+n-1) \\ - (\I32.\CONST~s+n-1)~(\I32\K{.}\LOAD\K{8\_u}~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\I32.\CONST~d+n) \\ + (\I32.\CONST~s+n)~(\I32\K{.}\LOAD\K{8\_u}~\{ \OFFSET~0, \ALIGN~0 \}) \\ (\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\ (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~\MEMORYCOPY \\ \end{array} @@ -2679,7 +2681,7 @@ Control Instructions :math:`\BRTABLE~l^\ast~l_N` ........................... -1. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +1. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. 2. Pop the value :math:`\I32.\CONST~i` from the stack. @@ -2858,22 +2860,22 @@ Exiting :math:`\instr^\ast` with label :math:`L` When the end of a block is reached without a jump or trap aborting it, then the following steps are performed. -1. Let :math:`m` be the number of values on the top of the stack. +1. Let :math:`n` be the number of values on the top of the stack. -2. Pop the values :math:`\val^m` from the stack. +2. Pop the values :math:`\val^n` from the stack. -3. Assert: due to :ref:`validation `, the label :math:`L` is now on the top of the stack. +3. Assert: due to :ref:`validation `, the label :math:`L` is now on the top of the stack and has arity :math:`n`. 4. Pop the label from the stack. -5. Push :math:`\val^m` back to the stack. +5. Push :math:`\val^n` back to the stack. 6. Jump to the position after the |END| of the :ref:`structured control instruction ` associated with the label :math:`L`. .. math:: ~\\[-1ex] \begin{array}{lcl@{\qquad}l} - \LABEL_n\{\instr^\ast\}~\val^m~\END &\stepto& \val^m + \LABEL_n\{\instr^\ast\}~\val^n~\END &\stepto& \val^n \end{array} .. note:: diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 149a53a8be..9ee7eccc9c 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -30,18 +30,18 @@ or *external references* pointing to an uninterpreted form of :ref:`extern addre .. math:: \begin{array}{llcl} - \production{(number)} & \num &::=& + \production{number} & \num &::=& \I32.\CONST~\i32 \\&&|& \I64.\CONST~\i64 \\&&|& \F32.\CONST~\f32 \\&&|& \F64.\CONST~\f64 \\ - \production{(vector)} & \vecc &::=& + \production{vector} & \vecc &::=& \V128.\CONST~\i128 \\ - \production{(reference)} & \reff &::=& + \production{reference} & \reff &::=& \REFNULL~t \\&&|& \REFFUNCADDR~\funcaddr \\&&|& \REFEXTERNADDR~\externaddr \\ - \production{(value)} & \val &::=& + \production{value} & \val &::=& \num ~|~ \vecc ~|~ \reff \\ \end{array} @@ -79,7 +79,7 @@ It is either a sequence of :ref:`values ` or a :ref:`trap ` listing .. math:: \begin{array}{llll} - \production{(store)} & \store &::=& \{~ + \production{store} & \store &::=& \{~ \begin{array}[t]{l@{~}ll} \SFUNCS & \funcinst^\ast, \\ \STABLES & \tableinst^\ast, \\ @@ -157,21 +157,21 @@ In addition, an :ref:`embedder ` may supply an uninterpreted set of *h .. math:: \begin{array}{llll} - \production{(address)} & \addr &::=& + \production{address} & \addr &::=& 0 ~|~ 1 ~|~ 2 ~|~ \dots \\ - \production{(function address)} & \funcaddr &::=& + \production{function address} & \funcaddr &::=& \addr \\ - \production{(table address)} & \tableaddr &::=& + \production{table address} & \tableaddr &::=& \addr \\ - \production{(memory address)} & \memaddr &::=& + \production{memory address} & \memaddr &::=& \addr \\ - \production{(global address)} & \globaladdr &::=& + \production{global address} & \globaladdr &::=& \addr \\ - \production{(element address)} & \elemaddr &::=& + \production{element address} & \elemaddr &::=& \addr \\ - \production{(data address)} & \dataaddr &::=& + \production{data address} & \dataaddr &::=& \addr \\ - \production{(extern address)} & \externaddr &::=& + \production{extern address} & \externaddr &::=& \addr \\ \end{array} @@ -204,7 +204,7 @@ and collects runtime representations of all entities that are imported, defined, .. math:: \begin{array}{llll} - \production{(module instance)} & \moduleinst &::=& \{ + \production{module instance} & \moduleinst &::=& \{ \begin{array}[t]{l@{~}ll} \MITYPES & \functype^\ast, \\ \MIFUNCS & \funcaddr^\ast, \\ @@ -238,10 +238,10 @@ The module instance is used to resolve references to other definitions during ex .. math:: \begin{array}{llll} - \production{(function instance)} & \funcinst &::=& + \production{function instance} & \funcinst &::=& \{ \FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func \} \\ &&|& \{ \FITYPE~\functype, \FIHOSTCODE~\hostfunc \} \\ - \production{(host function)} & \hostfunc &::=& \dots \\ + \production{host function} & \hostfunc &::=& \dots \\ \end{array} A *host function* is a function expressed outside WebAssembly but passed to a :ref:`module ` as an :ref:`import `. @@ -268,7 +268,7 @@ It records its :ref:`type ` and holds a vector of :ref:`refere .. math:: \begin{array}{llll} - \production{(table instance)} & \tableinst &::=& + \production{table instance} & \tableinst &::=& \{ \TITYPE~\tabletype, \TIELEM~\vec(\reff) \} \\ \end{array} @@ -292,7 +292,7 @@ It records its :ref:`type ` and holds a vector of :ref:`bytes ` and holds an individual :ref:`val .. math:: \begin{array}{llll} - \production{(global instance)} & \globalinst &::=& + \production{global instance} & \globalinst &::=& \{ \GITYPE~\globaltype, \GIVALUE~\val \} \\ \end{array} @@ -338,7 +338,7 @@ It holds a vector of references and their common :ref:`type `. .. math:: \begin{array}{llll} - \production{(element instance)} & \eleminst &::=& + \production{element instance} & \eleminst &::=& \{ \EITYPE~\reftype, \EIELEM~\vec(\reff) \} \\ \end{array} @@ -356,7 +356,7 @@ It holds a vector of :ref:`bytes `. .. math:: \begin{array}{llll} - \production{(data instance)} & \datainst &::=& + \production{data instance} & \datainst &::=& \{ \DIDATA~\vec(\byte) \} \\ \end{array} @@ -374,7 +374,7 @@ It defines the export's :ref:`name ` and the associated :ref:`exter .. math:: \begin{array}{llll} - \production{(export instance)} & \exportinst &::=& + \production{export instance} & \exportinst &::=& \{ \EINAME~\name, \EIVALUE~\externval \} \\ \end{array} @@ -392,7 +392,7 @@ It is an :ref:`address ` denoting either a :ref:`function instance .. math:: \begin{array}{llcl} - \production{(external value)} & \externval &::=& + \production{external value} & \externval &::=& \EVFUNC~\funcaddr \\&&|& \EVTABLE~\tableaddr \\&&|& \EVMEM~\memaddr \\&&|& @@ -456,7 +456,7 @@ Labels carry an argument arity :math:`n` and their associated branch *target*, w .. math:: \begin{array}{llll} - \production{(label)} & \label &::=& + \production{label} & \label &::=& \LABEL_n\{\instr^\ast\} \\ \end{array} @@ -485,9 +485,9 @@ and a reference to the function's own :ref:`module instance ` .. math:: \begin{array}{llll} - \production{(activation)} & \X{activation} &::=& + \production{activation} & \X{activation} &::=& \FRAME_n\{\frame\} \\ - \production{(frame)} & \frame &::=& + \production{frame} & \frame &::=& \{ \ALOCALS~\val^\ast, \AMODULE~\moduleinst \} \\ \end{array} @@ -529,7 +529,7 @@ In order to express the reduction of :ref:`traps `, :ref:`calls `, the .. math:: \begin{array}{llll} - \production{(block contexts)} & \XB^0 &::=& + \production{block contexts} & \XB^0 &::=& \val^\ast~[\_]~\instr^\ast \\ - \production{(block contexts)} & \XB^{k+1} &::=& + \production{block contexts} & \XB^{k+1} &::=& \val^\ast~\LABEL_n\{\instr^\ast\}~\XB^k~\END~\instr^\ast \\ \end{array} @@ -624,9 +624,9 @@ that operates relative to a current :ref:`frame ` referring to the .. math:: \begin{array}{llcl} - \production{(configuration)} & \config &::=& + \production{configuration} & \config &::=& \store; \thread \\ - \production{(thread)} & \thread &::=& + \production{thread} & \thread &::=& \frame; \instr^\ast \\ \end{array} @@ -645,7 +645,7 @@ Finally, the following definition of *evaluation context* and associated structu .. math:: \begin{array}{llll} - \production{(evaluation contexts)} & E &::=& + \production{evaluation contexts} & E &::=& [\_] ~|~ \val^\ast~E~\instr^\ast ~|~ \LABEL_n\{\instr^\ast\}~E~\END \\ diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index b2d5fd13b8..afcda69c01 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1625,7 +1625,7 @@ Constant Expressions \qquad \frac{ }{ - C \vdashinstrconst \REFNULL \const + C \vdashinstrconst \REFNULL~t \const } \qquad \frac{ From 937fc7d63efb9e18f36334a9e761a8a040ac44b7 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 9 Dec 2022 17:20:54 +0100 Subject: [PATCH 09/20] [spec] Eps --- document/core/appendix/embedding.rst | 2 +- document/core/text/conventions.rst | 2 +- document/core/valid/conventions.rst | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index b2995f2f15..27aac4b319 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -33,7 +33,7 @@ Failure of an interface operation is indicated by an auxiliary syntactic class: .. math:: \begin{array}{llll} - \production{(error)} & \error &::=& \ERROR \\ + \production{error} & \error &::=& \ERROR \\ \end{array} In addition to the error conditions specified explicitly in this section, implementations may also return errors when specific :ref:`implementation limitations ` are reached. diff --git a/document/core/text/conventions.rst b/document/core/text/conventions.rst index 12c8b7dfc8..0bd32e0339 100644 --- a/document/core/text/conventions.rst +++ b/document/core/text/conventions.rst @@ -117,7 +117,7 @@ It is convenient to define identifier contexts as :ref:`records ` :math: .. math:: \begin{array}{llll} - \production{(context)} & C &::=& + \production{context} & C &::=& \begin{array}[t]{l@{~}ll} \{ & \CTYPES & \functype^\ast, \\ & \CFUNCS & \functype^\ast, \\ From ef01de5ef4e7d5cc772110af2e30cc4fb722784a Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 12 Dec 2022 23:37:45 +0100 Subject: [PATCH 10/20] [interpreter] Refactor parser to handle select & call_indirect correctly (#1567) --- interpreter/text/parser.mly | 100 +++++++++++------------------------ test/core/call_indirect.wast | 20 +++++++ test/core/select.wast | 17 ++++++ 3 files changed, 67 insertions(+), 70 deletions(-) diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 535a05d51e..7489acf72b 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -366,12 +366,16 @@ align_opt : /* Instructions & Expressions */ -instr : +instr_list : + | /* empty */ { fun c -> [] } + | instr1 instr_list { fun c -> $1 c @ $2 c } + | select_instr_instr_list { $1 } + | call_instr_instr_list { $1 } + +instr1 : | plain_instr { let at = at () in fun c -> [$1 c @@ at] } - | select_instr_instr { fun c -> let e, es = $1 c in e :: es } - | call_instr_instr { fun c -> let e, es = $1 c in e :: es } | block_instr { let at = at () in fun c -> [$1 c @@ at] } - | expr { $1 } /* Sugar */ + | expr { $1 } /* Sugar */ plain_instr : | UNREACHABLE { fun c -> unreachable } @@ -442,89 +446,51 @@ plain_instr : | VEC_REPLACE NAT { let at = at () in fun c -> $1 (vec_lane_index $2 at) } -select_instr : - | SELECT select_instr_results - { let at = at () in fun c -> let b, ts = $2 in - select (if b then (Some ts) else None) @@ at } - -select_instr_results : - | LPAR RESULT value_type_list RPAR select_instr_results - { let _, ts = $5 in true, $3 @ ts } - | /* empty */ - { false, [] } - -select_instr_instr : - | SELECT select_instr_results_instr +select_instr_instr_list : + | SELECT select_instr_results_instr_list { let at1 = ati 1 in fun c -> let b, ts, es = $2 c in - select (if b then (Some ts) else None) @@ at1, es } + (select (if b then (Some ts) else None) @@ at1) :: es } -select_instr_results_instr : - | LPAR RESULT value_type_list RPAR select_instr_results_instr +select_instr_results_instr_list : + | LPAR RESULT value_type_list RPAR select_instr_results_instr_list { fun c -> let _, ts, es = $5 c in true, $3 @ ts, es } - | instr + | instr_list { fun c -> false, [], $1 c } -call_instr : - | CALL_INDIRECT var call_instr_type - { let at = at () in fun c -> call_indirect ($2 c table) ($3 c) @@ at } - | CALL_INDIRECT call_instr_type /* Sugar */ - { let at = at () in fun c -> call_indirect (0l @@ at) ($2 c) @@ at } - -call_instr_type : - | type_use call_instr_params - { let at1 = ati 1 in - fun c -> - match $2 c with - | FuncType ([], []) -> $1 c type_ - | ft -> inline_type_explicit c ($1 c type_) ft at1 } - | call_instr_params - { let at = at () in fun c -> inline_type c ($1 c) at } - -call_instr_params : - | LPAR PARAM value_type_list RPAR call_instr_params - { fun c -> let FuncType (ts1, ts2) = $5 c in FuncType ($3 @ ts1, ts2) } - | call_instr_results - { fun c -> FuncType ([], $1 c) } - -call_instr_results : - | LPAR RESULT value_type_list RPAR call_instr_results - { fun c -> $3 @ $5 c } - | /* empty */ - { fun c -> [] } - - -call_instr_instr : - | CALL_INDIRECT var call_instr_type_instr +call_instr_instr_list : + | CALL_INDIRECT var call_instr_type_instr_list { let at1 = ati 1 in - fun c -> let x, es = $3 c in call_indirect ($2 c table) x @@ at1, es } - | CALL_INDIRECT call_instr_type_instr /* Sugar */ + fun c -> let x, es = $3 c in + (call_indirect ($2 c table) x @@ at1) :: es } + | CALL_INDIRECT call_instr_type_instr_list /* Sugar */ { let at1 = ati 1 in - fun c -> let x, es = $2 c in call_indirect (0l @@ at1) x @@ at1, es } + fun c -> let x, es = $2 c in + (call_indirect (0l @@ at1) x @@ at1) :: es } -call_instr_type_instr : - | type_use call_instr_params_instr +call_instr_type_instr_list : + | type_use call_instr_params_instr_list { let at1 = ati 1 in fun c -> match $2 c with | FuncType ([], []), es -> $1 c type_, es | ft, es -> inline_type_explicit c ($1 c type_) ft at1, es } - | call_instr_params_instr + | call_instr_params_instr_list { let at = at () in fun c -> let ft, es = $1 c in inline_type c ft at, es } -call_instr_params_instr : - | LPAR PARAM value_type_list RPAR call_instr_params_instr +call_instr_params_instr_list : + | LPAR PARAM value_type_list RPAR call_instr_params_instr_list { fun c -> let FuncType (ts1, ts2), es = $5 c in FuncType ($3 @ ts1, ts2), es } - | call_instr_results_instr + | call_instr_results_instr_list { fun c -> let ts, es = $1 c in FuncType ([], ts), es } -call_instr_results_instr : - | LPAR RESULT value_type_list RPAR call_instr_results_instr +call_instr_results_instr_list : + | LPAR RESULT value_type_list RPAR call_instr_results_instr_list { fun c -> let ts, es = $5 c in $3 @ ts, es } - | instr + | instr_list { fun c -> [], $1 c } @@ -657,12 +623,6 @@ if_ : | LPAR THEN instr_list RPAR /* Sugar */ { fun c c' -> [], $3 c', [] } -instr_list : - | /* empty */ { fun c -> [] } - | select_instr { fun c -> [$1 c] } - | call_instr { fun c -> [$1 c] } - | instr instr_list { fun c -> $1 c @ $2 c } - expr_list : | /* empty */ { fun c -> [] } | expr expr_list { fun c -> $1 c @ $2 c } diff --git a/test/core/call_indirect.wast b/test/core/call_indirect.wast index 1ecd9b7baf..79b8dc393e 100644 --- a/test/core/call_indirect.wast +++ b/test/core/call_indirect.wast @@ -1015,3 +1015,23 @@ (module (table funcref (elem 0 0))) "unknown function" ) + + + + +;; Flat syntax + +(module + (table 1 funcref) + (func unreachable call_indirect) + (func unreachable call_indirect nop) + (func unreachable call_indirect call_indirect) + (func unreachable call_indirect (call_indirect)) + (func unreachable call_indirect call_indirect call_indirect) + (func unreachable call_indirect (result)) + (func unreachable call_indirect (result) (result)) + (func unreachable call_indirect (result) (result) call_indirect) + (func unreachable call_indirect (result) (result) call_indirect (result)) + (func (result i32) unreachable call_indirect select) + (func (result i32) unreachable call_indirect select call_indirect) +) diff --git a/test/core/select.wast b/test/core/select.wast index 046e6fe2c2..673dcf478d 100644 --- a/test/core/select.wast +++ b/test/core/select.wast @@ -512,3 +512,20 @@ "type mismatch" ) + +;; Flat syntax + +(module + (table 1 funcref) + (func (result i32) unreachable select) + (func (result i32) unreachable select nop) + (func (result i32) unreachable select (select)) + (func (result i32) unreachable select select) + (func (result i32) unreachable select select select) + (func (result i32) unreachable select (result i32)) + (func (result i32) unreachable select (result i32) (result)) + (func (result i32) unreachable select (result i32) (result) select) + (func (result i32) unreachable select (result) (result i32) select (result i32)) + (func (result i32) unreachable select call_indirect) + (func (result i32) unreachable select call_indirect select) +) From a54a1d85400db3cf243717a0ab1cc2fb6098170f Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 15 Dec 2022 16:23:26 +0100 Subject: [PATCH 11/20] [spec] Remove dead piece of grammar --- document/core/exec/runtime.rst | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 9ee7eccc9c..6c53a4e965 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -476,8 +476,8 @@ Intuitively, :math:`\instr^\ast` is the *continuation* to execute when the branc When branching, the empty continuation ends the targeted block, such that execution can proceed with consecutive instructions. -Activations and Frames -...................... +Activation Frames +................. Activation frames carry the return arity :math:`n` of the respective function, hold the values of its :ref:`locals ` (including arguments) in the order corresponding to their static :ref:`local indices `, @@ -485,8 +485,6 @@ and a reference to the function's own :ref:`module instance ` .. math:: \begin{array}{llll} - \production{activation} & \X{activation} &::=& - \FRAME_n\{\frame\} \\ \production{frame} & \frame &::=& \{ \ALOCALS~\val^\ast, \AMODULE~\moduleinst \} \\ \end{array} From 1782235239ddebaf2cb079b00fdaa2d2c4dedba3 Mon Sep 17 00:00:00 2001 From: YAMAMOTO Takashi Date: Fri, 16 Dec 2022 00:24:54 +0900 Subject: [PATCH 12/20] [test] elem.wast: force to use exprs in a element (#1561) --- test/core/elem.wast | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/test/core/elem.wast b/test/core/elem.wast index 8dc04e6e49..5857ae8bd9 100644 --- a/test/core/elem.wast +++ b/test/core/elem.wast @@ -148,6 +148,25 @@ (assert_return (invoke "call-7") (i32.const 65)) (assert_return (invoke "call-9") (i32.const 66)) +;; Same as the above, but use ref.null to ensure the elements use exprs. +;; Note: some tools like wast2json avoid using exprs when possible. +(module + (type $out-i32 (func (result i32))) + (table 11 funcref) + (elem (i32.const 6) funcref (ref.null func) (ref.func $const-i32-a)) + (elem (i32.const 9) funcref (ref.func $const-i32-b) (ref.null func)) + (func $const-i32-a (type $out-i32) (i32.const 65)) + (func $const-i32-b (type $out-i32) (i32.const 66)) + (func (export "call-7") (type $out-i32) + (call_indirect (type $out-i32) (i32.const 7)) + ) + (func (export "call-9") (type $out-i32) + (call_indirect (type $out-i32) (i32.const 9)) + ) +) +(assert_return (invoke "call-7") (i32.const 65)) +(assert_return (invoke "call-9") (i32.const 66)) + (assert_invalid (module (table 1 funcref) (global i32 (i32.const 0)) (elem (global.get 0) $f) (func $f)) "unknown global" From ca1d792430e353a7de0f2f4948fbb02bb0b83a65 Mon Sep 17 00:00:00 2001 From: Ng Zhi An Date: Tue, 17 Jan 2023 23:47:06 +0000 Subject: [PATCH 13/20] Fix typos in SIMD exec/instructions --- document/core/exec/instructions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 6b0280603c..72893d64e8 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -394,7 +394,7 @@ Most vector instructions are defined in terms of generic numeric operators appli .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - (\V128\K{.}\VCONST~c_1)~(\V128\K{.}\VCONST~c_2)~\V128\K{.}\SWIZZLE &\stepto& (\V128\K{.}\VCONST~c') + (\V128\K{.}\VCONST~c_1)~(\V128\K{.}\VCONST~c_2)~\I8X16\K{.}\SWIZZLE &\stepto& (\V128\K{.}\VCONST~c') \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -431,7 +431,7 @@ Most vector instructions are defined in terms of generic numeric operators appli .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - (\V128\K{.}\VCONST~c_1)~(\V128\K{.}\VCONST~c_2)~\V128\K{.}\SHUFFLE~x^\ast &\stepto& (\V128\K{.}\VCONST~c) + (\V128\K{.}\VCONST~c_1)~(\V128\K{.}\VCONST~c_2)~\I8X16\K{.}\SHUFFLE~x^\ast &\stepto& (\V128\K{.}\VCONST~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} From 4c249c5a575e2b0e252e747af261bbb82f448dd4 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Wed, 18 Jan 2023 16:34:13 -0600 Subject: [PATCH 14/20] Update interpreter README (#1571) It previously stated that the formal spec did not exist, but the spec has existed for years now. --- interpreter/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/interpreter/README.md b/interpreter/README.md index 418b845011..18aa36c05e 100644 --- a/interpreter/README.md +++ b/interpreter/README.md @@ -1,6 +1,6 @@ # WebAssembly Reference Interpreter -This repository implements a interpreter for WebAssembly. It is written for clarity and simplicity, _not_ speed. It is intended as a playground for trying out ideas and a device for nailing down the exact semantics, and as a proxy for the (yet to be produced) formal specification of WebAssembly. For that purpose, the code is written in a fairly declarative, "speccy" way. +This repository implements an interpreter for WebAssembly. It is written for clarity and simplicity, _not_ speed. It is intended as a playground for trying out ideas and a device for nailing down their exact semantics. For that purpose, the code is written in a fairly declarative, "speccy" way. The interpreter can From f54b5b81a3649461b4c8be0363844301983868ab Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 24 Jan 2023 12:22:06 +0100 Subject: [PATCH 15/20] [spec] Remove an obsolete exec step (#1580) --- document/core/exec/instructions.rst | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 72893d64e8..cc66dbf2e0 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2912,15 +2912,13 @@ Invocation of :ref:`function address ` :math:`a` 7. Pop the values :math:`\val^n` from the stack. -8. Let :math:`\val_0^\ast` be the list of zero values of types :math:`t^\ast`. +8. Let :math:`F` be the :ref:`frame ` :math:`\{ \AMODULE~f.\FIMODULE, \ALOCALS~\val^n~(\default_t)^\ast \}`. -9. Let :math:`F` be the :ref:`frame ` :math:`\{ \AMODULE~f.\FIMODULE, \ALOCALS~\val^n~(\default_t)^\ast \}`. +9. Push the activation of :math:`F` with arity :math:`m` to the stack. -10. Push the activation of :math:`F` with arity :math:`m` to the stack. +10. Let :math:`L` be the :ref:`label ` whose arity is :math:`m` and whose continuation is the end of the function. -11. Let :math:`L` be the :ref:`label ` whose arity is :math:`m` and whose continuation is the end of the function. - -12. :ref:`Enter ` the instruction sequence :math:`\instr^\ast` with label :math:`L`. +11. :ref:`Enter ` the instruction sequence :math:`\instr^\ast` with label :math:`L`. .. math:: ~\\[-1ex] From 6798f054ad1b0493919f0b5244fa46682ccd3e69 Mon Sep 17 00:00:00 2001 From: Keith Winstein Date: Tue, 24 Jan 2023 04:32:02 -0800 Subject: [PATCH 16/20] [test] Optional tableidx for table.{get,set,size,grow,fill} (#1582) --- test/core/table_fill.wast | 6 +++++- test/core/table_get.wast | 2 +- test/core/table_grow.wast | 5 ++++- test/core/table_set.wast | 2 +- test/core/table_size.wast | 2 +- 5 files changed, 12 insertions(+), 5 deletions(-) diff --git a/test/core/table_fill.wast b/test/core/table_fill.wast index 3df64da1ab..a8e2225520 100644 --- a/test/core/table_fill.wast +++ b/test/core/table_fill.wast @@ -5,6 +5,10 @@ (table.fill $t (local.get $i) (local.get $r) (local.get $n)) ) + (func (export "fill-abbrev") (param $i i32) (param $r externref) (param $n i32) + (table.fill (local.get $i) (local.get $r) (local.get $n)) + ) + (func (export "get") (param $i i32) (result externref) (table.get $t (local.get $i)) ) @@ -39,7 +43,7 @@ (assert_return (invoke "get" (i32.const 8)) (ref.extern 4)) (assert_return (invoke "get" (i32.const 9)) (ref.extern 4)) -(assert_return (invoke "fill" (i32.const 9) (ref.null extern) (i32.const 1))) +(assert_return (invoke "fill-abbrev" (i32.const 9) (ref.null extern) (i32.const 1))) (assert_return (invoke "get" (i32.const 8)) (ref.extern 4)) (assert_return (invoke "get" (i32.const 9)) (ref.null extern)) diff --git a/test/core/table_get.wast b/test/core/table_get.wast index 5d57c31983..0dedb19f51 100644 --- a/test/core/table_get.wast +++ b/test/core/table_get.wast @@ -10,7 +10,7 @@ ) (func (export "get-externref") (param $i i32) (result externref) - (table.get $t2 (local.get $i)) + (table.get (local.get $i)) ) (func $f3 (export "get-funcref") (param $i i32) (result funcref) (table.get $t3 (local.get $i)) diff --git a/test/core/table_grow.wast b/test/core/table_grow.wast index 7d5b5630fc..9a931a7fa2 100644 --- a/test/core/table_grow.wast +++ b/test/core/table_grow.wast @@ -7,6 +7,9 @@ (func (export "grow") (param $sz i32) (param $init externref) (result i32) (table.grow $t (local.get $init) (local.get $sz)) ) + (func (export "grow-abbrev") (param $sz i32) (param $init externref) (result i32) + (table.grow (local.get $init) (local.get $sz)) + ) (func (export "size") (result i32) (table.size $t)) ) @@ -22,7 +25,7 @@ (assert_trap (invoke "set" (i32.const 1) (ref.extern 2)) "out of bounds table access") (assert_trap (invoke "get" (i32.const 1)) "out of bounds table access") -(assert_return (invoke "grow" (i32.const 4) (ref.extern 3)) (i32.const 1)) +(assert_return (invoke "grow-abbrev" (i32.const 4) (ref.extern 3)) (i32.const 1)) (assert_return (invoke "size") (i32.const 5)) (assert_return (invoke "get" (i32.const 0)) (ref.extern 2)) (assert_return (invoke "set" (i32.const 0) (ref.extern 2))) diff --git a/test/core/table_set.wast b/test/core/table_set.wast index 5a9cfa3715..3362f95673 100644 --- a/test/core/table_set.wast +++ b/test/core/table_set.wast @@ -12,7 +12,7 @@ ) (func (export "set-externref") (param $i i32) (param $r externref) - (table.set $t2 (local.get $i) (local.get $r)) + (table.set (local.get $i) (local.get $r)) ) (func (export "set-funcref") (param $i i32) (param $r funcref) (table.set $t3 (local.get $i) (local.get $r)) diff --git a/test/core/table_size.wast b/test/core/table_size.wast index ad293b5ee4..83fef02b33 100644 --- a/test/core/table_size.wast +++ b/test/core/table_size.wast @@ -4,7 +4,7 @@ (table $t2 0 2 externref) (table $t3 3 8 externref) - (func (export "size-t0") (result i32) (table.size $t0)) + (func (export "size-t0") (result i32) table.size) (func (export "size-t1") (result i32) (table.size $t1)) (func (export "size-t2") (result i32) (table.size $t2)) (func (export "size-t3") (result i32) (table.size $t3)) From 7d905dfa61b25ad58b71490eacfb13e70290b5ef Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 26 Jan 2023 17:03:14 +0100 Subject: [PATCH 17/20] [spec] Fix abstract grammar for const immediate (#1577) --- document/core/syntax/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index eae802cbd3..9c48736b0b 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -45,7 +45,7 @@ These operations closely match respective operations available in hardware. \production{signedness} & \sx &::=& \K{u} ~|~ \K{s} \\ \production{instruction} & \instr &::=& - \K{i}\X{nn}\K{.}\CONST~\xref{syntax/values}{syntax-int}{\iX{\X{nn}}} ~|~ + \K{i}\X{nn}\K{.}\CONST~\xref{syntax/values}{syntax-int}{\uX{\X{nn}}} ~|~ \K{f}\X{nn}\K{.}\CONST~\xref{syntax/values}{syntax-float}{\fX{\X{nn}}} \\&&|& \K{i}\X{nn}\K{.}\iunop ~|~ \K{f}\X{nn}\K{.}\funop \\&&|& From 0031ea49613c72522eeff11e0511d423cb64645f Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 26 Jan 2023 17:03:48 +0100 Subject: [PATCH 18/20] [spec] Fix context composition in text format (#1578) --- document/core/text/modules.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index fde59878a8..c34077326f 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -108,7 +108,7 @@ If inline declarations are given, then their types must match the referenced :re \end{array} \\ \end{array} -The synthesized attribute of a |Ttypeuse| is a pair consisting of both the used :ref:`type index ` and the updated :ref:`identifier context ` including possible parameter identifiers. +The synthesized attribute of a |Ttypeuse| is a pair consisting of both the used :ref:`type index ` and the local :ref:`identifier context ` containing possible parameter identifiers. The following auxiliary function extracts optional identifiers from parameters: .. math:: @@ -200,7 +200,7 @@ Function definitions can bind a symbolic :ref:`function identifier `, a \text{(}~\text{func}~~\Tid^?~~x,I'{:}\Ttypeuse_I~~ (t{:}\Tlocal)^\ast~~(\X{in}{:}\Tinstr_{I''})^\ast~\text{)} \\ &&& \qquad \Rightarrow\quad \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\X{in}^\ast~\END \} \\ &&& \qquad\qquad\qquad - (\iff I'' = I' \compose \{\ILOCALS~\F{id}(\Tlocal)^\ast\} \idcwellformed) \\[1ex] + (\iff I'' = I \compose I' \compose \{\ILOCALS~\F{id}(\Tlocal)^\ast\} \idcwellformed) \\[1ex] \production{local} & \Tlocal &::=& \text{(}~\text{local}~~\Tid^?~~t{:}\Tvaltype~\text{)} \quad\Rightarrow\quad t \\ From dcf4eaa08fe1b3f98e855e0581389bc29f5d496b Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 26 Jan 2023 17:04:44 +0100 Subject: [PATCH 19/20] [spec] Fix label shadowing (#1579) --- document/core/text/instructions.rst | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 348aa77335..e846ccb50b 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -34,6 +34,8 @@ The following grammar handles the corresponding update to the :ref:`identifier c \production{label} & \Tlabel_I &::=& v{:}\Tid &\Rightarrow& \{\ILABELS~v\} \compose I & (\iff v \notin I.\ILABELS) \\ &&|& + v{:}\Tid &\Rightarrow& \{\ILABELS~v\} \compose (I \with \ILABELS[i] = \epsilon) + & (\iff I.\ILABELS[i] = v) \\ &&|& \epsilon &\Rightarrow& \{\ILABELS~(\epsilon)\} \compose I \\ \end{array} @@ -42,6 +44,9 @@ The following grammar handles the corresponding update to the :ref:`identifier c This effectively shifts all existing labels up by one, mirroring the fact that control instructions are indexed relatively not absolutely. + If a label with the same name already exists, + then it is shadowed and the earlier label becomes inaccessible. + .. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, polymorphism pair: text format; instruction From 45f9845d4ecb92984dd573c93b7143ad42726bf8 Mon Sep 17 00:00:00 2001 From: candymate <31069474+candymate@users.noreply.github.com> Date: Tue, 31 Jan 2023 18:31:53 +0900 Subject: [PATCH 20/20] [spec] Fix typos in instruction index (#1584) --- document/core/appendix/gen-index-instructions.py | 8 ++++---- document/core/appendix/index-instructions.rst | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/document/core/appendix/gen-index-instructions.py b/document/core/appendix/gen-index-instructions.py index 65a9717155..fffa2b3292 100755 --- a/document/core/appendix/gen-index-instructions.py +++ b/document/core/appendix/gen-index-instructions.py @@ -427,10 +427,10 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\V128.\LOAD\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{55}', r'[\I32~\V128] \to [\V128]', r'valid-load-lane', r'exec-load-lane'), Instruction(r'\V128.\LOAD\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{56}', r'[\I32~\V128] \to [\V128]', r'valid-load-lane', r'exec-load-lane'), Instruction(r'\V128.\LOAD\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{57}', r'[\I32~\V128] \to [\V128]', r'valid-load-lane', r'exec-load-lane'), - Instruction(r'\V128.\STORE\K{8\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{58}', r'[\I32~\V128] \to [\V128]', r'valid-store-lane', r'exec-store-lane'), - Instruction(r'\V128.\STORE\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{59}', r'[\I32~\V128] \to [\V128]', r'valid-store-lane', r'exec-store-lane'), - Instruction(r'\V128.\STORE\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5A}', r'[\I32~\V128] \to [\V128]', r'valid-store-lane', r'exec-store-lane'), - Instruction(r'\V128.\STORE\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5B}', r'[\I32~\V128] \to [\V128]', r'valid-store-lane', r'exec-store-lane'), + Instruction(r'\V128.\STORE\K{8\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{58}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'), + Instruction(r'\V128.\STORE\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{59}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'), + Instruction(r'\V128.\STORE\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5A}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'), + Instruction(r'\V128.\STORE\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5B}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'), Instruction(r'\V128.\LOAD\K{32\_zero}~\memarg~\laneidx', r'\hex{FD}~~\hex{5C}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'), Instruction(r'\V128.\LOAD\K{64\_zero}~\memarg~\laneidx', r'\hex{FD}~~\hex{5D}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'), Instruction(r'\F32X4.\VDEMOTE\K{\_f64x2\_zero}', r'\hex{FD}~~\hex{5E}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-demote'), diff --git a/document/core/appendix/index-instructions.rst b/document/core/appendix/index-instructions.rst index 84055a9fa2..977c21fb33 100644 --- a/document/core/appendix/index-instructions.rst +++ b/document/core/appendix/index-instructions.rst @@ -367,10 +367,10 @@ Instruction Binary Opcode :math:`\V128.\LOAD\K{16\_lane}~\memarg~\laneidx` :math:`\hex{FD}~~\hex{55}` :math:`[\I32~\V128] \to [\V128]` :ref:`validation ` :ref:`execution ` :math:`\V128.\LOAD\K{32\_lane}~\memarg~\laneidx` :math:`\hex{FD}~~\hex{56}` :math:`[\I32~\V128] \to [\V128]` :ref:`validation ` :ref:`execution ` :math:`\V128.\LOAD\K{64\_lane}~\memarg~\laneidx` :math:`\hex{FD}~~\hex{57}` :math:`[\I32~\V128] \to [\V128]` :ref:`validation ` :ref:`execution ` -:math:`\V128.\STORE\K{8\_lane}~\memarg~\laneidx` :math:`\hex{FD}~~\hex{58}` :math:`[\I32~\V128] \to [\V128]` :ref:`validation ` :ref:`execution ` -:math:`\V128.\STORE\K{16\_lane}~\memarg~\laneidx` :math:`\hex{FD}~~\hex{59}` :math:`[\I32~\V128] \to [\V128]` :ref:`validation ` :ref:`execution ` -:math:`\V128.\STORE\K{32\_lane}~\memarg~\laneidx` :math:`\hex{FD}~~\hex{5A}` :math:`[\I32~\V128] \to [\V128]` :ref:`validation ` :ref:`execution ` -:math:`\V128.\STORE\K{64\_lane}~\memarg~\laneidx` :math:`\hex{FD}~~\hex{5B}` :math:`[\I32~\V128] \to [\V128]` :ref:`validation ` :ref:`execution ` +:math:`\V128.\STORE\K{8\_lane}~\memarg~\laneidx` :math:`\hex{FD}~~\hex{58}` :math:`[\I32~\V128] \to []` :ref:`validation ` :ref:`execution ` +:math:`\V128.\STORE\K{16\_lane}~\memarg~\laneidx` :math:`\hex{FD}~~\hex{59}` :math:`[\I32~\V128] \to []` :ref:`validation ` :ref:`execution ` +:math:`\V128.\STORE\K{32\_lane}~\memarg~\laneidx` :math:`\hex{FD}~~\hex{5A}` :math:`[\I32~\V128] \to []` :ref:`validation ` :ref:`execution ` +:math:`\V128.\STORE\K{64\_lane}~\memarg~\laneidx` :math:`\hex{FD}~~\hex{5B}` :math:`[\I32~\V128] \to []` :ref:`validation ` :ref:`execution ` :math:`\V128.\LOAD\K{32\_zero}~\memarg~\laneidx` :math:`\hex{FD}~~\hex{5C}` :math:`[\I32] \to [\V128]` :ref:`validation ` :ref:`execution ` :math:`\V128.\LOAD\K{64\_zero}~\memarg~\laneidx` :math:`\hex{FD}~~\hex{5D}` :math:`[\I32] \to [\V128]` :ref:`validation ` :ref:`execution ` :math:`\F32X4.\VDEMOTE\K{\_f64x2\_zero}` :math:`\hex{FD}~~\hex{5E}` :math:`[\V128] \to [\V128]` :ref:`validation ` :ref:`execution `, :ref:`operator `