Merge with WebAssembly/spec (#19)

* [test] Adjust br_table length test to avoid wrong failure (WebAssembly#1715) * [spec] Fix extmul & extadd execution (WebAssembly#1716) * [interpreter] Add dune dependencies (WebAssembly#1717) * Revert "[interpreter] Add dune dependencies (WebAssembly#1717)" This reverts commit 44ed035. * [interpreter/test] Fix inconsistent use of float values in `spectest` (WebAssembly#1718) * [spec] Fix operand order in reduction of shape.replace_lane (WebAssembly#1721) * [spec] Fix sx to be sx? in reduction of vcvtop_zero (WebAssembly#1720) --------- Co-authored-by: Rod Vagg <[email protected]> Co-authored-by: 702fbtngus <[email protected]> Co-authored-by: Muqiu Han (韩暮秋) <[email protected]> Co-authored-by: Andreas Rossberg <[email protected]> Co-authored-by: Dongjun Youn / 윤동준 <[email protected]> Co-authored-by: Hoseong Lee <[email protected]>
wasmfx · Jan 25, 2024 · c49e324 · c49e324
1 parent a9ec313
commit c49e324
Show file tree

Hide file tree

Showing 6 changed files with 44 additions and 26 deletions.
diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst
@@ -1844,31 +1844,31 @@ Most other vector instructions are defined in terms of numeric operators that ar
 
 1. Assert: due to :ref:`validation <valid-vec-replace_lane>`, :math:`x < \dim(\shape)`.
 
-2. Let :math:`t_1` be the type :math:`\unpacked(\shape)`.
+2. Let :math:`t_2` be the type :math:`\unpacked(\shape)`.
 
 3. Assert: due to :ref:`validation <valid-vec-replace_lane>`, a value of :ref:`value type <syntax-valtype>` :math:`t_1` is on the top of the stack.
 
-4. Pop the value :math:`t_1.\CONST~c_1` from the stack.
+4. Pop the value :math:`t_2.\CONST~c_2` from the stack.
 
 5. Assert: due to :ref:`validation <valid-vec-replace_lane>`, a value of :ref:`value type <syntax-valtype>` |V128| is on the top of the stack.
 
-6. Pop the value :math:`\V128.\VCONST~c_2` from the stack.
+6. Pop the value :math:`\V128.\VCONST~c_1` from the stack.
 
-7. Let :math:`i^\ast` be the result of computing :math:`\lanes_{\shape}(c_2)`.
+7. Let :math:`i^\ast` be the result of computing :math:`\lanes_{\shape}(c_1)`.
 
-8. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\shape}(i^\ast \with [x] = c_1)`.
+8. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\shape}(i^\ast \with [x] = c_2)`.
 
 9. Push :math:`\V128.\VCONST~c` on the stack.
 
 .. math::
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   (t_1\K{.}\CONST~c_1)~(\V128\K{.}\VCONST~c_2)~(\shape\K{.}\REPLACELANE~x) &\stepto& (\V128\K{.}\VCONST~c)
+   (\V128\K{.}\VCONST~c_1)~(t_2\K{.}\CONST~c_2)~(\shape\K{.}\REPLACELANE~x) &\stepto& (\V128\K{.}\VCONST~c)
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
-      (\iff & i^\ast = \lanes_{\shape}(c_2) \\
-       \wedge & c = \lanes^{-1}_{\shape}(i^\ast \with [x] = c_1))
+      (\iff & i^\ast = \lanes_{\shape}(c_1) \\
+       \wedge & c = \lanes^{-1}_{\shape}(i^\ast \with [x] = c_2))
      \end{array}
    \end{array}
 
@@ -2168,8 +2168,8 @@ where:
    \end{array}
 
 
-:math:`t_2\K{x}N\K{.}\vcvtop\K{\_}t_1\K{x}M\K{\_}\sx\K{\_zero}`
-...............................................................
+:math:`t_2\K{x}N\K{.}\vcvtop\K{\_}t_1\K{x}M\K{\_}\sx^?\K{\_zero}`
+.................................................................
 
 1. Assert: due to :ref:`syntax <syntax-instr-vec>`, :math:`N = 2 \cdot M`.
 
@@ -2179,7 +2179,7 @@ where:
 
 4. Let :math:`i^\ast` be the result of computing :math:`\lanes_{t_1\K{x}M}(c_1)`.
 
-5. Let :math:`j^\ast` be the result of computing :math:`\vcvtop^{\sx}_{|t_1|,|t_2|}(i^\ast)`.
+5. Let :math:`j^\ast` be the result of computing :math:`\vcvtop^{\sx^?}_{|t_1|,|t_2|}(i^\ast)`.
 
 6. Let :math:`k^\ast` be the concatenation of the two sequences :math:`j^\ast` and :math:`0^M`.
 
@@ -2190,11 +2190,11 @@ where:
 .. math::
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   (\V128\K{.}\VCONST~c_1)~t_2\K{x}N\K{.}\vcvtop\K{\_}t_1\K{x}M\K{\_}\sx\K{\_zero} &\stepto& (\V128\K{.}\VCONST~c) \\
+   (\V128\K{.}\VCONST~c_1)~t_2\K{x}N\K{.}\vcvtop\K{\_}t_1\K{x}M\K{\_}\sx^?\K{\_zero} &\stepto& (\V128\K{.}\VCONST~c) \\
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
-     (\iff & c = \lanes^{-1}_{t_2\K{x}N}(\vcvtop^{\sx}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1))~0^M))
+     (\iff & c = \lanes^{-1}_{t_2\K{x}N}(\vcvtop^{\sx^?}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1))~0^M))
      \end{array}
    \end{array}
 
@@ -2273,7 +2273,7 @@ where:
 
 10. Let :math:`k_2^\ast` be the result of computing :math:`\extend^{\sx}_{|t_1|,|t_2|}(j_2^\ast)`.
 
-11. Let :math:`k^\ast` be the result of computing :math:`\imul_{t_2\K{x}N}(k_1^\ast, k_2^\ast)`.
+11. Let :math:`k^\ast` be the result of computing :math:`\imul_{|t_2|}(k_1^\ast, k_2^\ast)`.
 
 12. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{t_2\K{x}N}(k^\ast)`.
 
@@ -2287,7 +2287,7 @@ where:
      \begin{array}[t]{@{}r@{~}l@{}}
      (\iff & i^\ast = \lanes_{t_1\K{x}M}(c_1)[\half(0, N) \slice N] \\
      \wedge & j^\ast = \lanes_{t_1\K{x}M}(c_2)[\half(0, N) \slice N] \\
-     \wedge & c = \lanes^{-1}_{t_2\K{x}N}(\imul_{t_2\K{x}N}(\extend^{\sx}_{|t_1|,|t_2|}(i^\ast), \extend^{\sx}_{|t_1|,|t_2|}(j^\ast))))
+     \wedge & c = \lanes^{-1}_{t_2\K{x}N}(\imul_{|t_2|}(\extend^{\sx}_{|t_1|,|t_2|}(i^\ast), \extend^{\sx}_{|t_1|,|t_2|}(j^\ast))))
      \end{array}
 
 where:
@@ -2314,7 +2314,7 @@ where:
 
 5. Let :math:`(j_1~j_2)^\ast` be the result of computing :math:`\extend^{\sx}_{|t_1|,|t_2|}(i^\ast)`.
 
-6. Let :math:`k^\ast` be the result of computing :math:`\iadd_{N}(j_1, j_2)^\ast`.
+6. Let :math:`k^\ast` be the result of computing :math:`\iadd_{|t_2|}(j_1, j_2)^\ast`.
 
 7. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{t_2\K{x}N}(k^\ast)`.
 
@@ -2328,7 +2328,7 @@ where:
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
      (\iff & (i_1~i_2)^\ast = \extend^{\sx}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1)) \\
-     \wedge & j^\ast = \iadd_{N}(i_1, i_2)^\ast \\
+     \wedge & j^\ast = \iadd_{|t_2|}(i_1, i_2)^\ast \\
      \wedge & c = \lanes^{-1}_{t_2\K{x}N}(j^\ast))
      \end{array}
    \end{array}

diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml
@@ -33,8 +33,8 @@ let spectest = {
   print_f64: console.log.bind(console),
   global_i32: 666,
   global_i64: 666n,
-  global_f32: 666,
-  global_f64: 666,
+  global_f32: 666.6,
+  global_f64: 666.6,
   table: new WebAssembly.Table({initial: 10, maximum: 20, element: 'anyfunc'}),
   memory: new WebAssembly.Memory({initial: 1, maximum: 2})
 };

diff --git a/test/core/binary.wast b/test/core/binary.wast
@@ -1085,8 +1085,19 @@
 (assert_malformed
   (module binary
     "\00asm" "\01\00\00\00"
-    "\01\04\01"                             ;; type section
+    "\01\25\0c"                             ;; type section
     "\60\00\00"                             ;; type 0
+    "\60\00\00"                             ;; type 1
+    "\60\00\00"                             ;; type 2
+    "\60\00\00"                             ;; type 3
+    "\60\00\00"                             ;; type 4
+    "\60\00\00"                             ;; type 5
+    "\60\00\00"                             ;; type 6
+    "\60\00\00"                             ;; type 7
+    "\60\00\00"                             ;; type 8
+    "\60\00\00"                             ;; type 9
+    "\60\00\00"                             ;; type 10
+    "\60\00\00"                             ;; type 11
     "\03\02\01\00"                          ;; func section
     "\0a\13\01"                             ;; code section
     "\11\00"                                ;; func 0
@@ -1097,8 +1108,9 @@
     "\0e\01"                                ;; br_table with inconsistent target count (1 declared, 2 given)
     "\00"                                   ;; break depth 0
     "\01"                                   ;; break depth 1
-    "\02"                                   ;; break depth for default
-    "\0b\0b\0b"                             ;; end
+    "\02"                                   ;; break depth for default, interpreted as a block
+    "\0b"                                   ;; end, interpreted as type 11 for the block
+    "\0b\0b"                                ;; end
   )
   "unexpected end of section or function"
 )

diff --git a/test/core/imports.wast b/test/core/imports.wast
@@ -238,12 +238,18 @@
   (func (export "get-1") (result i32) (global.get 1))
   (func (export "get-x") (result i32) (global.get $x))
   (func (export "get-y") (result i32) (global.get $y))
+  (func (export "get-4") (result i64) (global.get 4))
+  (func (export "get-5") (result f32) (global.get 5))
+  (func (export "get-6") (result f64) (global.get 6))
 )
 
 (assert_return (invoke "get-0") (i32.const 666))
 (assert_return (invoke "get-1") (i32.const 666))
 (assert_return (invoke "get-x") (i32.const 666))
 (assert_return (invoke "get-y") (i32.const 666))
+(assert_return (invoke "get-4") (i64.const 666))
+(assert_return (invoke "get-5") (f32.const 666.6))
+(assert_return (invoke "get-6") (f64.const 666.6))
 
 (module (import "test" "global-i32" (global i32)))
 (module (import "test" "global-f32" (global f32)))

diff --git a/test/harness/async_index.js b/test/harness/async_index.js
@@ -100,8 +100,8 @@ function reinitializeRegistry() {
       print_f64: console.log.bind(console),
       global_i32: 666,
       global_i64: 666n,
-      global_f32: 666,
-      global_f64: 666,
+      global_f32: 666.6,
+      global_f64: 666.6,
       table: new WebAssembly.Table({
         initial: 10,
         maximum: 20,

diff --git a/test/harness/sync_index.js b/test/harness/sync_index.js
@@ -110,8 +110,8 @@ function reinitializeRegistry() {
         print_f64: console.log.bind(console),
         global_i32: 666,
         global_i64: 666n,
-        global_f32: 666,
-        global_f64: 666,
+        global_f32: 666.6,
+        global_f64: 666.6,
         table: new WebAssembly.Table({initial: 10, maximum: 20, element: 'anyfunc'}),
         memory: new WebAssembly.Memory({initial: 1, maximum: 2})
     };