[spectext] Add i32x4.dot_i16x8_s (WebAssembly#475)

This instruction was added in WebAssembly#127.

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

document/core/appendix/gen-index-instructions.py

@@ -488,6 +488,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\I32X4.\VMIN\K{\_u}', r'\hex{FD}~~183', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-imin_u'),
     Instruction(r'\I32X4.\VMAX\K{\_s}', r'\hex{FD}~~184', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-imax_s'),
     Instruction(r'\I32X4.\VMAX\K{\_u}', r'\hex{FD}~~185', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-imax_u'),
+    Instruction(r'\I32X4.\DOT\K{\_i16x8\_s}', r'\hex{FD}~~186', r'[\V128~\V128] \to [\V128]', r'valid-simd-dot', r'exec-simd-dot'),
     Instruction(r'\I32X4.\EXTMUL\K{\_low\_i16x8\_s}', r'\hex{FD}~~187', r'[\V128~\V128] \to [\V128]', r'valid-simd-vextmul', r'exec-simd-vextmul'),
     Instruction(r'\I32X4.\EXTMUL\K{\_high\_i16x8\_s}', r'\hex{FD}~~189', r'[\V128~\V128] \to [\V128]', r'valid-simd-vextmul', r'exec-simd-vextmul'),
     Instruction(r'\I32X4.\EXTMUL\K{\_low\_i16x8\_u}', r'\hex{FD}~~190', r'[\V128~\V128] \to [\V128]', r'valid-simd-vextmul', r'exec-simd-vextmul'),

document/core/appendix/index-instructions.rst

@@ -436,6 +436,7 @@ Instruction                                        Binary Opcode          Type
 :math:`\I32X4.\VMIN\K{\_u}`                        :math:`\hex{FD}~~183`  :math:`[\V128~\V128] \to [\V128]`              :ref:`validation <valid-vbinop>`             :ref:`execution <exec-vbinop>`, :ref:`operator <op-imin_u>`       
 :math:`\I32X4.\VMAX\K{\_s}`                        :math:`\hex{FD}~~184`  :math:`[\V128~\V128] \to [\V128]`              :ref:`validation <valid-vbinop>`             :ref:`execution <exec-vbinop>`, :ref:`operator <op-imax_s>`       
 :math:`\I32X4.\VMAX\K{\_u}`                        :math:`\hex{FD}~~185`  :math:`[\V128~\V128] \to [\V128]`              :ref:`validation <valid-vbinop>`             :ref:`execution <exec-vbinop>`, :ref:`operator <op-imax_u>`       
+:math:`\I32X4.\DOT\K{\_i16x8\_s}`                  :math:`\hex{FD}~~186`  :math:`[\V128~\V128] \to [\V128]`              :ref:`validation <valid-simd-dot>`           :ref:`execution <exec-simd-dot>`                                  
 :math:`\I32X4.\EXTMUL\K{\_low\_i16x8\_s}`          :math:`\hex{FD}~~187`  :math:`[\V128~\V128] \to [\V128]`              :ref:`validation <valid-simd-vextmul>`       :ref:`execution <exec-simd-vextmul>`                              
 :math:`\I32X4.\EXTMUL\K{\_high\_i16x8\_s}`         :math:`\hex{FD}~~189`  :math:`[\V128~\V128] \to [\V128]`              :ref:`validation <valid-simd-vextmul>`       :ref:`execution <exec-simd-vextmul>`                              
 :math:`\I32X4.\EXTMUL\K{\_low\_i16x8\_u}`          :math:`\hex{FD}~~190`  :math:`[\V128~\V128] \to [\V128]`              :ref:`validation <valid-simd-vextmul>`       :ref:`execution <exec-simd-vextmul>`                              

document/core/binary/instructions.rst

@@ -687,6 +687,7 @@ All other SIMD instructions are plain opcodes without any immediates.
      \hex{FD}~~183{:}\Bu32 &\Rightarrow& \I32X4.\VMIN\K{\_u} \\ &&|&
      \hex{FD}~~184{:}\Bu32 &\Rightarrow& \I32X4.\VMAX\K{\_s} \\ &&|&
      \hex{FD}~~185{:}\Bu32 &\Rightarrow& \I32X4.\VMAX\K{\_u} \\ &&|&
+     \hex{FD}~~186{:}\Bu32 &\Rightarrow& \I32X4.\DOT\K{\_i16x8\_s}\\ &&|&
      \hex{FD}~~187{:}\Bu32 &\Rightarrow& \I32X4.\EXTMUL\K{\_low\_i16x8\_s}\\ &&|&
      \hex{FD}~~189{:}\Bu32 &\Rightarrow& \I32X4.\EXTMUL\K{\_high\_i16x8\_s}\\ &&|&
      \hex{FD}~~190{:}\Bu32 &\Rightarrow& \I32X4.\EXTMUL\K{\_low\_i16x8\_u}\\ &&|&

document/core/exec/instructions.rst

@@ -725,6 +725,39 @@ SIMD instructions are defined in terms of generic numeric operators applied lane
    \end{array}
 
 
+.. _exec-simd-dot:
+
+:math:`\K{i32x4.}\DOT\K{\_i16x8\_s}`
+....................................
+
+1. Assert: due to :ref:`validation <valid-vitestop>`, two values of :ref:`value type <syntax-valtype>` |V128| is on the top of the stack.
+
+2. Pop the value :math:`\V128.\VCONST~c_2` from the stack.
+
+3. Pop the value :math:`\V128.\VCONST~c_1` from the stack.
+
+4. Let :math:`(i_1~i_2)^\ast` be the result of computing :math:`\imul_{32}(\extend^s_{16,32}(\lanes_{\I16X8}(c_1)), \extend^s_{16,32}(\lanes_{\I16X8}(c_2)))`
+
+5. Let :math:`j^\ast` be the result of computing :math:`\iadd_{32}(i_1, i_2)^\ast`.
+
+6. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\I32X4}(j^\ast)`.
+
+8. Push the value :math:`\V128.\VCONST~c` onto the stack.
+
+.. math::
+   \begin{array}{l}
+   \begin{array}{lcl@{\qquad}l}
+   (\V128\K{.}\VCONST~c_1)~(\V128\K{.}\VCONST~c_2)~\K{i32x4.}\DOT\K{\_i16x8\_s} &\stepto& (\V128\K{.}\VCONST~c) \\
+   \end{array}
+   \\ \qquad
+     \begin{array}[t]{@{}r@{~}l@{}}
+     (\iff & (i_1~i_2)^\ast = \imul_{32}(\extend^s_{16,32}(\lanes_{\I16X8}(c_1)), \extend^s_{16,32}(\lanes_{\I16X8}(c_2))) \\
+     \wedge & j^\ast = \iadd_{32}(i_1, i_2)^\ast \\
+     \wedge & c = \lanes^{-1}_{\I32X4}(j^\ast)
+     \end{array}
+   \end{array}
+
+
 .. _exec-simd-vextmul:
 
 :math:`t_2\K{x}N\K{.}\EXTMUL\_\K{low}\_t_1\K{x}M\_\sx` and :math:`t_2\K{x}N\K{.}\EXTMUL\_\K{high}\_t_1\K{x}M\_\sx`

document/core/syntax/instructions.rst

@@ -237,6 +237,7 @@ SIMD instructions provide basic operations over :ref:`values <syntax-value>` of
      \K{i64x2.}\viunop \\&&|&
      \K{i8x16.}\VPOPCNT \\&&|&
      \K{i16x8.}\Q15MULRSAT\K{\_s} \\ &&|&
+     \K{i32x4.}\DOT\K{\_i16x8\_s} \\ &&|&
      \fshape\K{.}\vfunop \\&&|&
      \ishape\K{.}\vitestop \\ &&|&
      \ishape\K{.}\BITMASK \\ &&|&

document/core/text/instructions.rst

@@ -720,6 +720,7 @@ SIMD const instructions have a mandatory :ref:`shape <syntax-simd-shape>` descri
      \text{i32x4.min\_u} &\Rightarrow& \I32X4.\VMIN\K{\_u}\\ &&|&
      \text{i32x4.max\_s} &\Rightarrow& \I32X4.\VMAX\K{\_s}\\ &&|&
      \text{i32x4.max\_u} &\Rightarrow& \I32X4.\VMAX\K{\_u}\\ &&|&
+     \text{i32x4.dot\_i16x8\_s} &\Rightarrow& \I32X4.\DOT\K{\_i16x8\_s}\\ &&|&
      \text{i32x4.extmul\_low\_i16x8\_s} &\Rightarrow& \I32X4.\EXTMUL\K{\_low\_i16x8\_s}\\ &&|&
      \text{i32x4.extmul\_high\_i16x8\_s} &\Rightarrow& \I32X4.\EXTMUL\K{\_high\_i16x8\_s}\\ &&|&
      \text{i32x4.extmul\_low\_i16x8\_u} &\Rightarrow& \I32X4.\EXTMUL\K{\_low\_i16x8\_u}\\ &&|&

document/core/util/macros.def

@@ -425,6 +425,7 @@
 .. |NARROW| mathdef:: \xref{syntax/instructions}{syntax-instr-simd}{\K{narrow}}
 .. |VEXTEND| mathdef:: \xref{syntax/instructions}{syntax-instr-simd}{\K{extend}}
 .. |AVGR| mathdef:: \xref{syntax/instructions}{syntax-instr-simd}{\K{avgr}}
+.. |DOT| mathdef:: \xref{syntax/instructions}{syntax-instr-simd}{\K{dot}}
 .. |EXTMUL| mathdef:: \xref{syntax/instructions}{syntax-instr-simd}{\K{extmul}}
 .. |VTRUNC| mathdef:: \xref{syntax/instructions}{syntax-instr-simd}{\K{trunc}}
 .. |VCONVERT| mathdef:: \xref{syntax/instructions}{syntax-instr-simd}{\K{convert}}

document/core/valid/instructions.rst

@@ -450,6 +450,20 @@ We also define an auxiliary function to get number of packed numeric types in a
    }
 
 
+.. _valid-simd-dot:
+
+:math:`\K{i32x4.}\DOT\K{\_i16x8\_s}`
+....................................
+
+* The instruction is valid with type :math:`[\V128~\V128] \to [\V128]`.
+
+.. math::
+   \frac{
+   }{
+     C \vdashinstr \K{i32x4.}\DOT\K{\_i16x8\_s} : [\V128~\V128] \to [\V128]
+   }
+
+
 .. _valid-simd-vextmul:
 
 :math:`\ishape\K{.}\vextmul\K{\_}\ishape\K{\_}\sx`