Skip to content

Commit e22ec22

Browse files
brendandahlbrendandahl
authored
[spec/interpreter] Fix i32x4.relaxed_dot_i8x16_i7x16_add_s (#2312)
1 parent 0148af7 commit e22ec22

13 files changed

Lines changed: 186 additions & 96 deletions

File tree

‎document/core/exec/numerics.rst‎

Lines changed: 14 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2244,14 +2244,21 @@ where :math:`f`, :math:`\sx_1`, :math:`\sx_2`, :math:`h`, and :math:`k` are inst
22442244
\VRELAXEDDOTADD{\K\_}\S_{\K{i}N_1\K{x}M_1, \K{i}N_2\K{x}M_2}(c_1, c_2, c_3) &=& c
22452245
& (
22462246
\begin{array}[t]{@{}l}
2247-
\iff N = 2\cdot N_1 \\
2248-
\land~M = 2\cdot M_2 \\
2249-
\land~c' = \VRELAXEDDOT{\K\_}\S_{\K{i}N_1\K{x}M_1, \K{i}N\K{x}M}(c_1, c_2) \\
2250-
\land~c'' = \VEXTADDPAIRWISE{\K\_}\S_{\K{i}N\K{x}M, \K{i}N_2\K{x}M_2}(c') \\
2251-
\land~c \in \VADD_{\K{i}N_2\K{x}M_2}(c'', c_3) \\
2247+
\iff N = \relaxed(R_{\F{idot\_add}})[2\cdot N_1, N_2] \\
2248+
\land~i_1^\ast = \lanes_{\K{i}N_1\K{x}M_1}(c_1) \\
2249+
\land~i_2^\ast = \lanes_{\K{i}N_1\K{x}M_1}(c_2) \\
2250+
\land~{i'_1}^\ast = \extend^{\S}_{N_1, N}(i_1)^\ast \\
2251+
\land~{i'_2}^\ast = \extend^{\relaxed(R_{\F{idot}})[\S, \U]}_{N_1, N}(i_2)^\ast \\
2252+
\land~j^\ast = \ivrelaxeddot_N({i'_1}^\ast, {i'_2}^\ast) \\
2253+
\land~{j'}^\ast = \extend^{\S}_{N, N_2}(j)^\ast \\
2254+
\land~c' = \lanes^{-1}_{\K{i}N_2\K{x}M_2}(\ivaddpairwise_{N_2}({j'}^\ast)) \\
2255+
\land~c \in \VADD_{\K{i}N_2\K{x}M_2}(c', c_3) \\
22522256
\end{array}
22532257
\end{array}
22542258
2259+
.. note::
2260+
Relaxed operations and the parameters :math:`R_{\F{idot}}` and :math:`R_{\F{idot\_add}}` are introduced :ref:`below <relaxed-ops>`.
2261+
22552262

22562263
.. _op-vnarrow:
22572264

@@ -2546,7 +2553,8 @@ where:
25462553
...........................................
25472554

25482555
The implementation-specific behaviour of this operation is determined by the global parameter :math:`R_{\F{idot}} \in \{0, 1\}`.
2549-
It also affects the behaviour of :math:`\VRELAXEDDOT` and :math:`\VRELAXEDDOTADD` specified :ref:`above <op-vextbinop>`.
2556+
It also affects the behaviour of :math:`\VRELAXEDDOT` specified :ref:`above <op-vextbinop>`,
2557+
and of :math:`\VRELAXEDDOTADD` specified :ref:`above <op-vextternop>`, which additionally depends on the global parameter :math:`R_{\F{idot\_add}} \in \{0, 1\}`.
25502558

25512559
* Return :math:`\relaxed(R_{\F{idot}})[ \ivdot_N(i_1^{2m}, i_2^{2m}), \ivdotsat_N(i_1^{2m}, i_2^{2m}) ]`.
25522560

‎interpreter/exec/v128.ml‎

Lines changed: 3 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -425,20 +425,6 @@ struct
425425
| _, _ -> assert false
426426
in I32x4.of_lanes (dot xs ys)
427427

428-
let dot_add_s x y z =
429-
let xs = List.map Convert.I16_.extend_i8_s (I8x16.to_lanes x) in
430-
let ys = List.map Convert.I16_.extend_i8_s (I8x16.to_lanes y) in
431-
let rec dot xs ys =
432-
match xs, ys with
433-
| x1::x2::x3::x4::xs', y1::y2::y3::y4::ys' ->
434-
Int32.(add
435-
(Convert.I32_.extend_i16_s (I16.(add_sat_s (mul x1 y1) (mul x2 y2))))
436-
(Convert.I32_.extend_i16_s (I16.(add_sat_s (mul x3 y3) (mul x4 y4))))
437-
) :: dot xs' ys'
438-
| [], [] -> []
439-
| _, _ -> assert false
440-
in I32x4.add (I32x4.of_lanes (dot xs ys)) z
441-
442428
let extmul_low_s x y = I32x4.mul (extend_low_s x) (extend_low_s y)
443429
let extmul_high_s x y = I32x4.mul (extend_high_s x) (extend_high_s y)
444430
let extmul_low_u x y = I32x4.mul (extend_low_u x) (extend_low_u y)
@@ -449,6 +435,9 @@ struct
449435
I32x4.of_lanes (Lib.List.map_pairwise (extadd Convert.I32_.extend_i16_s) (I16x8.to_lanes x))
450436
let extadd_pairwise_u x =
451437
I32x4.of_lanes (Lib.List.map_pairwise (extadd Convert.I32_.extend_i16_u) (I16x8.to_lanes x))
438+
439+
let dot_add_s x y z =
440+
I32x4.add (extadd_pairwise_s (I16x8_convert.dot_s x y)) z
452441
end
453442

454443
module I64x2_convert =

‎specification/wasm-3.0/3.0-numerics.relaxed.spectec‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,9 @@ def $R_fmadd : relaxed2 hint(builtin)
1919
def $R_fmin : relaxed4 hint(builtin)
2020
def $R_fmax : relaxed4 hint(builtin)
2121
def $R_idot : relaxed2 hint(builtin)
22+
def $R_idot_add : relaxed2 hint(show $R_(idot__add)) hint(builtin)
2223
def $R_iq15mulr : relaxed2 hint(builtin)
23-
def $R_trunc_u : relaxed2 hint(builtin)
24-
def $R_trunc_s : relaxed2 hint(builtin)
24+
def $R_trunc_u : relaxed2 hint(show $R_(trunc__u)) hint(builtin)
25+
def $R_trunc_s : relaxed2 hint(show $R_(trunc__s)) hint(builtin)
2526
def $R_swizzle : relaxed2 hint(builtin)
2627
def $R_laneselect : relaxed2 hint(builtin)

‎specification/wasm-3.0/3.2-numerics.vector.spectec‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -399,8 +399,12 @@ def $vextternop__(Jnn_1 X M_1, Jnn_2 X M_2, RELAXED_DOT_ADD S, c_1, c_2, c_3) =
399399
;)
400400

401401
def $vextternop__(Jnn_1 X M_1, Jnn_2 X M_2, RELAXED_DOT_ADD S, c_1, c_2, c_3) = c
402-
-- if $jsizenn(Jnn) = $(2*$lsizenn1(Jnn_1))
403-
-- if M = $(2*M_2)
404-
-- if c' = $vextbinop__(Jnn_1 X M_1, Jnn X M, RELAXED_DOT S, c_1, c_2)
405-
-- if c'' = $vextunop__(Jnn X M, Jnn_2 X M_2, EXTADD_PAIRWISE S, c')
406-
-- if c <- $vbinop_(Jnn_2 X M_2, ADD, c'', c_3)
402+
-- if N = $relaxed2($R_idot_add, nat, $(2*$lsizenn1(Jnn_1)), $lsizenn2(Jnn_2))
403+
-- if ci_1* = $lanes_(Jnn_1 X M_1, c_1)
404+
-- if ci_2* = $lanes_(Jnn_1 X M_1, c_2)
405+
-- if ci'_1* = $extend__($lsizenn1(Jnn_1), N, S, ci_1)*
406+
-- if ci'_2* = $extend__($lsizenn1(Jnn_1), N, $relaxed2($R_idot, sx, S, U), ci_2)*
407+
-- if ci* = $ivrelaxed_dot_(N, ci'_1*, ci'_2*)
408+
-- if ci'* = $extend__(N, $lsizenn2(Jnn_2), S, ci)*
409+
-- if c' = $inv_lanes_(Jnn_2 X M_2, $ivadd_pairwise_($lsizenn2(Jnn_2), ci'*))
410+
-- if c <- $vbinop_(Jnn_2 X M_2, ADD, c', c_3)

‎specification/wasm-latest/3.0-numerics.relaxed.spectec‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,9 @@ def $R_fmadd : relaxed2 hint(builtin)
1919
def $R_fmin : relaxed4 hint(builtin)
2020
def $R_fmax : relaxed4 hint(builtin)
2121
def $R_idot : relaxed2 hint(builtin)
22+
def $R_idot_add : relaxed2 hint(show $R_(idot__add)) hint(builtin)
2223
def $R_iq15mulr : relaxed2 hint(builtin)
23-
def $R_trunc_u : relaxed2 hint(builtin)
24-
def $R_trunc_s : relaxed2 hint(builtin)
24+
def $R_trunc_u : relaxed2 hint(show $R_(trunc__u)) hint(builtin)
25+
def $R_trunc_s : relaxed2 hint(show $R_(trunc__s)) hint(builtin)
2526
def $R_swizzle : relaxed2 hint(builtin)
2627
def $R_laneselect : relaxed2 hint(builtin)

‎specification/wasm-latest/3.2-numerics.vector.spectec‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -399,8 +399,12 @@ def $vextternop__(Jnn_1 X M_1, Jnn_2 X M_2, RELAXED_DOT_ADD S, c_1, c_2, c_3) =
399399
;)
400400

401401
def $vextternop__(Jnn_1 X M_1, Jnn_2 X M_2, RELAXED_DOT_ADD S, c_1, c_2, c_3) = c
402-
-- if $jsizenn(Jnn) = $(2*$lsizenn1(Jnn_1))
403-
-- if M = $(2*M_2)
404-
-- if c' = $vextbinop__(Jnn_1 X M_1, Jnn X M, RELAXED_DOT S, c_1, c_2)
405-
-- if c'' = $vextunop__(Jnn X M, Jnn_2 X M_2, EXTADD_PAIRWISE S, c')
406-
-- if c <- $vbinop_(Jnn_2 X M_2, ADD, c'', c_3)
402+
-- if N = $relaxed2($R_idot_add, nat, $(2*$lsizenn1(Jnn_1)), $lsizenn2(Jnn_2))
403+
-- if ci_1* = $lanes_(Jnn_1 X M_1, c_1)
404+
-- if ci_2* = $lanes_(Jnn_1 X M_1, c_2)
405+
-- if ci'_1* = $extend__($lsizenn1(Jnn_1), N, S, ci_1)*
406+
-- if ci'_2* = $extend__($lsizenn1(Jnn_1), N, $relaxed2($R_idot, sx, S, U), ci_2)*
407+
-- if ci* = $ivrelaxed_dot_(N, ci'_1*, ci'_2*)
408+
-- if ci'* = $extend__(N, $lsizenn2(Jnn_2), S, ci)*
409+
-- if c' = $inv_lanes_(Jnn_2 X M_2, $ivadd_pairwise_($lsizenn2(Jnn_2), ci'*))
410+
-- if c <- $vbinop_(Jnn_2 X M_2, ADD, c', c_3)

‎spectec/src/backend-interpreter/numerics.ml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,7 @@ let r_fmadd = relaxed "R_fmadd" 0
6464
let r_fmin = relaxed "R_fmin" 0
6565
let r_fmax = relaxed "R_fmax" 0
6666
let r_idot = relaxed "R_idot" 0
67+
let r_idot_add = relaxed "R_idot_add" 0
6768
let r_iq15mulr = relaxed "R_iq15mulr" 0
6869
let r_trunc_u = relaxed "R_trunc_u" 0
6970
let r_trunc_s = relaxed "R_trunc_s" 0
@@ -1081,6 +1082,7 @@ let numerics_list : numerics list = [
10811082
r_fmin;
10821083
r_fmax;
10831084
r_idot;
1085+
r_idot_add;
10841086
r_iq15mulr;
10851087
r_trunc_u;
10861088
r_trunc_s;

‎spectec/test-frontend/TEST.md‎

Lines changed: 13 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4842,6 +4842,9 @@ def $R_fmax : relaxed4
48424842
;; ../../../../specification/wasm-latest/3.0-numerics.relaxed.spectec
48434843
def $R_idot : relaxed2
48444844

4845+
;; ../../../../specification/wasm-latest/3.0-numerics.relaxed.spectec
4846+
def $R_idot_add : relaxed2
4847+
48454848
;; ../../../../specification/wasm-latest/3.0-numerics.relaxed.spectec
48464849
def $R_iq15mulr : relaxed2
48474850

@@ -5894,12 +5897,16 @@ def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__
58945897
;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec
58955898
def $vextternop__(ishape_1 : ishape, ishape_2 : ishape, vextternop__ : vextternop__(ishape_1, ishape_2), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn)
58965899
;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec
5897-
def $vextternop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, c_1 : vec_(V128_Vnn), c_2 : vec_(V128_Vnn), c_3 : vec_(V128_Vnn), c : vec_(V128_Vnn), Jnn : Jnn, M : M, c' : vec_(V128_Vnn), c'' : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOT_ADDS_vextternop__, c_1, c_2, c_3) = c
5898-
-- if ($jsizenn(Jnn) = (2 * $lsizenn1((Jnn_1 : Jnn <: lanetype))))
5899-
-- if (M!`%`_M.0 = (2 * M_2!`%`_M.0))
5900-
-- if (c' = $vextbinop__(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn : Jnn <: lanetype), M),), RELAXED_DOTS_vextbinop__, c_1, c_2))
5901-
-- if (c'' = $vextunop__(`%`_ishape(`%X%`_shape((Jnn : Jnn <: lanetype), M),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), EXTADD_PAIRWISE_vextunop__(S_sx), c'))
5902-
-- if (c <- $vbinop_(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), ADD_vbinop_, c'', c_3))
5900+
def $vextternop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, c_1 : vec_(V128_Vnn), c_2 : vec_(V128_Vnn), c_3 : vec_(V128_Vnn), c : vec_(V128_Vnn), N : N, `ci_1*` : lane_($lanetype(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1)))*, `ci_2*` : lane_($lanetype(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1)))*, `ci'_1*` : iN(N)*, `ci'_2*` : iN(N)*, `ci*` : iN(N)*, `ci'*` : iN($lsizenn2((Jnn_2 : Jnn <: lanetype)))*, c' : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOT_ADDS_vextternop__, c_1, c_2, c_3) = c
5901+
-- if (N = $relaxed2($R_idot_add, syntax nat, (2 * $lsizenn1((Jnn_1 : Jnn <: lanetype))), $lsizenn2((Jnn_2 : Jnn <: lanetype))))
5902+
-- if (ci_1*{ci_1 <- `ci_1*`} = $lanes_(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), c_1))
5903+
-- if (ci_2*{ci_2 <- `ci_2*`} = $lanes_(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), c_2))
5904+
-- if (ci'_1*{ci'_1 <- `ci'_1*`} = $extend__($lsizenn1((Jnn_1 : Jnn <: lanetype)), N, S_sx, ci_1)*{ci_1 <- `ci_1*`})
5905+
-- if (ci'_2*{ci'_2 <- `ci'_2*`} = $extend__($lsizenn1((Jnn_1 : Jnn <: lanetype)), N, $relaxed2($R_idot, syntax sx, S_sx, U_sx), ci_2)*{ci_2 <- `ci_2*`})
5906+
-- if (ci*{ci <- `ci*`} = $ivrelaxed_dot_(N, ci'_1*{ci'_1 <- `ci'_1*`}, ci'_2*{ci'_2 <- `ci'_2*`}))
5907+
-- if (ci'*{ci' <- `ci'*`} = $extend__(N, $lsizenn2((Jnn_2 : Jnn <: lanetype)), S_sx, ci)*{ci <- `ci*`})
5908+
-- if (c' = $inv_lanes_(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), $ivadd_pairwise_($lsizenn2((Jnn_2 : Jnn <: lanetype)), ci'*{ci' <- `ci'*`})))
5909+
-- if (c <- $vbinop_(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), ADD_vbinop_, c', c_3))
59035910

59045911
;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec
59055912
syntax num =

‎spectec/test-latex/TEST.md‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -9013,11 +9013,15 @@ $$
90139013
\begin{array}[t]{@{}lcl@{}l@{}}
90149014
{{\mathsf{relaxed\_dot\_add}}{\mathsf{\_}}{\mathsf{s}}}{{}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}(c_1, c_2, c_3)} & = & c & \quad
90159015
\begin{array}[t]{@{}l@{}}
9016-
\mbox{if}~ N = 2 \cdot N_1 \\
9017-
{\land}~ M = 2 \, M_2 \\
9018-
{\land}~ {c'} = {{\mathsf{relaxed\_dot}}{\mathsf{\_}}{\mathsf{s}}}{{}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{\mathsf{i}}{N}}{\mathsf{x}}{M}}(c_1, c_2)} \\
9019-
{\land}~ {c''} = {{\mathsf{extadd\_pairwise}}{\mathsf{\_}}{\mathsf{s}}}{{}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}({c'})} \\
9020-
{\land}~ c \in {\mathsf{add}}{{}_{{{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}({c''}, c_3)} \\
9016+
\mbox{if}~ N = {{\mathrm{relaxed}}({{\mathrm{R}}}_{{\mathit{idot\_add}}})}{{}[ 2 \cdot N_1, N_2 ]} \\
9017+
{\land}~ {{\mathit{ci}}_1^\ast} = {{\mathrm{lanes}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}}(c_1) \\
9018+
{\land}~ {{\mathit{ci}}_2^\ast} = {{\mathrm{lanes}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}}(c_2) \\
9019+
{\land}~ {{\mathit{ci}'}_1^\ast} = {{{{{\mathrm{extend}}}_{N_1, N}^{\mathsf{s}}}}{({\mathit{ci}}_1)}^\ast} \\
9020+
{\land}~ {{\mathit{ci}'}_2^\ast} = {{{{{\mathrm{extend}}}_{N_1, N}^{{{\mathrm{relaxed}}({\mathrm{R}}_{\mathit{idot}})}{{}[ \mathsf{s}, \mathsf{u} ]}}}}{({\mathit{ci}}_2)}^\ast} \\
9021+
{\land}~ {{\mathit{ci}}^\ast} = {{\mathrm{ivrelaxed\_dot}}}_{N}({{\mathit{ci}'}_1^\ast}, {{\mathit{ci}'}_2^\ast}) \\
9022+
{\land}~ {{\mathit{ci}'}^\ast} = {{{{{\mathrm{extend}}}_{N, N_2}^{\mathsf{s}}}}{({\mathit{ci}})}^\ast} \\
9023+
{\land}~ {c'} = {{{{\mathrm{lanes}}}_{{{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}^{{-1}}}}{({{\mathrm{ivadd\_pairwise}}}_{N_2}({{\mathit{ci}'}^\ast}))} \\
9024+
{\land}~ c \in {\mathsf{add}}{{}_{{{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}({c'}, c_3)} \\
90219025
\end{array} \\
90229026
\end{array}
90239027
$$

0 commit comments

Comments
 (0)