Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merge remote-tracking branch 'spec/wasm-3.0' #50

Merged
merged 5 commits into from
Oct 8, 2024
Merged

Merge remote-tracking branch 'spec/wasm-3.0' #50

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
e9cbf1a
[spec] Fix typo in relaxed formula
rossberg Oct 1, 2024
8e5f4ee
[spec] Various fixes to SIMD stuff
rossberg Oct 3, 2024
2a30893
[interpreter] Fix JS module invocation (#1829)
rossberg Oct 8, 2024
29b1fd4
[interpreter] Proper fix for JS conversion (#1832)
rossberg Oct 8, 2024
82d7113
Merge remote-tracking branch 'spec/wasm-3.0'
backes Oct 8, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 23 additions & 8 deletions document/core/exec/instructions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1601,6 +1601,21 @@ Most other vector instructions are defined in terms of numeric operators that ar
:math:`\lanes_{\K{i32x4}}(v_1)` and :math:`\lanes_{\K{i32x4}}(v_2)`
respectively.

For non-deterministic operators this definition is generalized to sets:

.. math::
\begin{array}{lll}
\X{op}_{t\K{x}N}(n_1,\dots,n_k) &=&
\{ \lanes^{-1}_{t\K{x}N}(i^\ast) ~|~ i^\ast \in \Large\times\xref{Step_pure/instructions}{exec-instr-numeric}{\X{op}}_t(i_1,\dots,i_k)^\ast \land i_1^\ast = \lanes_{t\K{x}N}(n_1) \land \dots \land i_k^\ast = \lanes_{t\K{x}N}(n_k) \} \\
\end{array}

where :math:`\Large\times \{x^\ast\}^N` transforms a sequence of :math:`N` sets of values into a set of sequences of :math:`N` values by computing the set product:

.. math::
\begin{array}{lll}
\Large\times (S_1 \dots S_N) &=& \{ x_1 \dots x_N ~|~ x_1 \in S_1 \land \dots \land x_N \in S_N \}
\end{array}


.. _exec-vconst:

Expand Down Expand Up @@ -2335,9 +2350,9 @@ where:

3. Pop the value :math:`\V128.\VCONST~c_1` from the stack.

4. Let :math:`(i_1~i_2)^8` be the result of computing :math:`\irelaxeddotmul_{8, 16}(\lanes_{\I8X16}(c_1), \lanes_{\I8X16}(c_2))`
4. Let :math:`(i_1~i_2)^8` be the result of computing :math:`\irelaxeddotmul_{8,16}(\lanes_{\I8X16}(c_1), \lanes_{\I8X16}(c_2))`

5. Let :math:`j^8` be the result of computing :math:`\sats_{16}(i_1 + i_2)^8`.
5. Let :math:`j^8` be the result of computing :math:`\iaddsats_{16}(i_1, i_2)^8`.

6. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\I16X8}(j^8)`.

Expand All @@ -2351,7 +2366,7 @@ where:
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\iff & (i_1~i_2)^8 = \irelaxeddotmul_{8,16}(\lanes_{\I8X16}(c_1), \lanes_{\I8X16}(c_2)) \\
\wedge & j^8 = \sats_{16}(i_1, i_2)^8 \\
\wedge & j^8 = \iaddsats_{16}(i_1, i_2)^8 \\
\wedge & c = \lanes^{-1}_{\I16X8}(j^8))
\end{array}
\end{array}
Expand All @@ -2370,11 +2385,11 @@ where:

4. Pop the value :math:`\V128.\VCONST~c_1` from the stack.

5. Let :math:`(i_1~i_2)^8` be the result of computing :math:`\irelaxeddotmul_{8, 16}(\lanes_{\I8X16}(c_1), \lanes_{\I8X16}(c_2))`
5. Let :math:`(i_1~i_2)^8` be the result of computing :math:`\irelaxeddotmul_{8,16}(\lanes_{\I8X16}(c_1), \lanes_{\I8X16}(c_2))`

6. Let :math:`(j_1~j_2)^4` be the result of computing :math:`\sats_{16}(i_1 + i_2)^8`.
6. Let :math:`(j_1~j_2)^4` be the result of computing :math:`\iaddsats_{16}(i_1, i_2)^8`.

7. Let :math:`j^4` be the result of computing :math:`\iadd_{32}(\extend^{s}_{16, 32}(j_1), \extend^{s}_{16, 32}(j_2))^4`.
7. Let :math:`j^4` be the result of computing :math:`\iadd_{32}(\extends_{16,32}(j_1), \extends_{16,32}(j_2))^4`.

8. Let :math:`k^4` be the result of computing :math:`\lanes_{\I32X4}(c_3)`.

Expand All @@ -2392,8 +2407,8 @@ where:
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\iff & (i_1~i_2)^8 = \irelaxeddotmul_{8,16}(\lanes_{\I8X16}(c_1), \lanes_{\I8X16}(c_2)) \\
\wedge & (j_1~j_2)^4 = \sats_{16}(i_1 + i_2)^8 \\
\wedge & j^4 = \iadd_{32}(\extend^{s}_{16, 32}(j_1), \extend^{s}_{16, 32}(j_2))^4 \\
\wedge & (j_1~j_2)^4 = \iaddsats_{16}(i_1, i_2)^8 \\
\wedge & j^4 = \iadd_{32}(\extends_{16,32}(j_1), \extends_{16,32}(j_2))^4 \\
\wedge & k^4 = \lanes_{\I32X4}(c_3) \\
\wedge & l^4 = \iadd_{32}(j, k)^4 \\
\wedge & c = \lanes^{-1}_{\I32X4}(l^4))
Expand Down
34 changes: 17 additions & 17 deletions document/core/exec/numerics.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,17 +88,17 @@ Conventions:

.. math::
\begin{array}{lll@{\qquad}l}
\satu_N(i) &=& 2^N-1 & (\iff i > 2^N-1)\\
\satu_N(i) &=& 0 & (\iff i < 0) \\
\satu_N(i) &=& 2^N-1 & (\iff i > 2^N-1)\\
\satu_N(i) &=& i & (\otherwise) \\
\end{array}

* Signed saturation, :math:`\sats_N(i)` clamps :math:`i` to between :math:`-2^{N-1}` and :math:`2^{N-1}-1`:

.. math::
\begin{array}{lll@{\qquad}l}
\sats_N(i) &=& \signed_N^{-1}(-2^{N-1}) & (\iff i < -2^{N-1})\\
\sats_N(i) &=& \signed_N^{-1}(2^{N-1}-1) & (\iff i > 2^{N-1}-1)\\
\sats_N(i) &=& -2^{N-1} & (\iff i < -2^{N-1})\\
\sats_N(i) &=& 2^{N-1}-1 & (\iff i > 2^{N-1}-1)\\
\sats_N(i) &=& i & (\otherwise)
\end{array}

Expand Down Expand Up @@ -860,11 +860,11 @@ The integer result of predicates -- i.e., :ref:`tests <syntax-testop>` and :ref:

* Let :math:`j` be the result of adding :math:`j_1` and :math:`j_2`.

* Return :math:`\sats_N(j)`.
* Return the value whose signed interpretation is :math:`\sats_N(j)`.

.. math::
\begin{array}{lll@{\qquad}l}
\iaddsats_N(i_1, i_2) &=& \sats_N(\signed_N(i_1) + \signed_N(i_2))
\iaddsats_N(i_1, i_2) &=& \signed_N^{-1}(\sats_N(\signed_N(i_1) + \signed_N(i_2)))
\end{array}


Expand Down Expand Up @@ -894,11 +894,11 @@ The integer result of predicates -- i.e., :ref:`tests <syntax-testop>` and :ref:

* Let :math:`j` be the result of subtracting :math:`j_2` from :math:`j_1`.

* Return :math:`\sats_N(j)`.
* Return the value whose signed interpretation is :math:`\sats_N(j)`.

.. math::
\begin{array}{lll@{\qquad}l}
\isubsats_N(i_1, i_2) &=& \sats_N(\signed_N(i_1) - \signed_N(i_2))
\isubsats_N(i_1, i_2) &=& \signed_N^{-1}(\sats_N(\signed_N(i_1) - \signed_N(i_2)))
\end{array}


Expand All @@ -922,11 +922,11 @@ The integer result of predicates -- i.e., :ref:`tests <syntax-testop>` and :ref:
:math:`\iq15mulrsats_N(i_1, i_2)`
.................................

* Return the result of :math:`\sats_N(\ishrs_N(i_1 \cdot i_2 + 2^{14}, 15))`.
* Return the whose signed interpretation is the result of :math:`\sats_N(\ishrs_N(i_1 \cdot i_2 + 2^{14}, 15))`.

.. math::
\begin{array}{lll@{\qquad}l}
\iq15mulrsats_N(i_1, i_2) &=& \sats_N(\ishrs_N(i_1 \cdot i_2 + 2^{14}, 15))
\iq15mulrsats_N(i_1, i_2) &=& \signed_N^{-1}(\sats_N(\ishrs_N(i_1 \cdot i_2 + 2^{14}, 15)))
\end{array}


Expand Down Expand Up @@ -1901,14 +1901,14 @@ Conversions

* Else if :math:`z` is positive infinity, then return :math:`2^{N-1} - 1`.

* Else, return :math:`\sats_N(\trunc(z))`.
* Else, return the value whose signed interpretation is :math:`\sats_N(\trunc(z))`.

.. math::
\begin{array}{lll@{\qquad}l}
\truncsats_{M,N}(\pm \NAN(n)) &=& 0 \\
\truncsats_{M,N}(- \infty) &=& -2^{N-1} \\
\truncsats_{M,N}(+ \infty) &=& 2^{N-1}-1 \\
\truncsats_{M,N}(z) &=& \sats_N(\trunc(z)) \\
\truncsats_{M,N}(z) &=& \signed_N^{-1}(\sats_N(\trunc(z))) \\
\end{array}


Expand Down Expand Up @@ -2006,11 +2006,11 @@ Conversions

* Let :math:`j` be the :ref:`signed interpretation <aux-signed>` of :math:`i` of size :math:`M`.

* Return :math:`\sats_N(j)`.
* Return the value whose signed interpretation is :math:`\sats_N(j)`.

.. math::
\begin{array}{lll@{\qquad}l}
\narrows_{M,N}(i) &=& \sats_N(\signed_M(i))
\narrows_{M,N}(i) &=& \signed_N^{-1}(\sats_N(\signed_M(i)))
\end{array}


Expand Down Expand Up @@ -2163,11 +2163,11 @@ This is an auxiliary operator for the specification of |RELAXEDDOT|.

The implementation-specific behaviour of this operation is determined by the global parameter :math:`R_{\F{idot}} \in \{0, 1\}`.

* Return :math:`\relaxed(R_{\F{idot}})[ \imul_N(\extends_{M,N}(i_1), extends_{M,N}), \imul_N(\extends_{M,N}(i_1), \extendu_{M,N}(i_2)) ]`.
* Return :math:`\relaxed(R_{\F{idot}})[ \imul_N(\extends_{M,N}(i_1), \extends_{M,N}(i_2)), \imul_N(\extends_{M,N}(i_1), \extendu_{M,N}(i_2)) ]`.

.. math::
\begin{array}{@{}lcll}
\irelaxeddotmul_{M,N}(i_1, i_2) &=& \relaxed(R_{\F{idot}})[ \imul_N(\extends_{M,N}(i_1), extends_{M,N}), \imul_N(\extends_{M,N}(i_1), \extendu_{M,N}(i_2)) ] \\
\irelaxeddotmul_{M,N}(i_1, i_2) &=& \relaxed(R_{\F{idot}})[ \imul_N(\extends_{M,N}(i_1), \extends_{M,N}(i_2)), \imul_N(\extends_{M,N}(i_1), \extendu_{M,N}(i_2)) ] \\
\end{array}

.. note::
Expand Down Expand Up @@ -2220,7 +2220,7 @@ The implementation-specific behaviour of this operation is determined by the glo
.. note::
Relaxed unsigned truncation is implementation-dependent for NaNs and out-of-range values.
In the :ref:`deterministic profile <profile-deterministic>`,
it behaves like regular :math:`\truncu`.
it behaves like regular :math:`\truncsatu`.


.. _op-relaxed_trunc_s:
Expand All @@ -2243,7 +2243,7 @@ The implementation-specific behaviour of this operation is determined by the glo
.. note::
Relaxed signed truncation is implementation-dependent for NaNs and out-of-range values.
In the :ref:`deterministic profile <profile-deterministic>`,
it behaves like regular :math:`\truncs`.
it behaves like regular :math:`\truncsats`.


.. _op-irelaxed_swizzle:
Expand Down
11 changes: 4 additions & 7 deletions interpreter/script/js.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -236,7 +236,7 @@ let env () : env =
let current_mod (env : env) = "$$" ^ string_of_int env.current_mod
let of_mod_opt (env : env) = function
| None -> current_mod env
| Some x -> x.it
| Some x -> "$" ^ x.it

let current_inst (env : env) = "$" ^ string_of_int env.current_inst
let of_inst_opt (env : env) = function
Expand Down Expand Up @@ -622,9 +622,6 @@ let rec of_definition def =
try of_definition (snd (Parse.Module.parse_string ~offset:s.at s.it))
with Parse.Syntax _ | Custom.Syntax _ -> of_bytes "<malformed quote>"

let of_instance env x_opt =
"instance(" ^ of_mod_opt env x_opt ^ ")"

let of_wrapper env x_opt name wrap_action wrap_assertion at =
let x = of_inst_opt env x_opt in
let bs = wrap name wrap_action wrap_assertion at in
Expand Down Expand Up @@ -677,9 +674,9 @@ let of_assertion env ass =
| AssertInvalidCustom (def, _) ->
"assert_invalid_custom(" ^ of_definition def ^ ");"
| AssertUnlinkable (x_opt, _) ->
"assert_unlinkable(" ^ of_instance env x_opt ^ ");"
"assert_unlinkable(" ^ of_mod_opt env x_opt ^ ");"
| AssertUninstantiable (x_opt, _) ->
"assert_uninstantiable(" ^ of_instance env x_opt ^ ");"
"assert_uninstantiable(" ^ of_mod_opt env x_opt ^ ");"
| AssertReturn (act, ress) ->
of_assertion' env act "assert_return" (List.map of_result ress)
(Some (assert_return ress))
Expand All @@ -702,7 +699,7 @@ let of_command env cmd =
| Quoted (_, s) ->
unquote (snd (Parse.Module.parse_string ~offset:s.at s.it))
in bind_mod env x_opt (unquote def);
"let " ^ current_mod env ^ " = " ^ of_definition def ^ ";\n" ^
"let " ^ current_mod env ^ " = module(" ^ of_definition def ^ ");\n" ^
(if x_opt = None then "" else
"let " ^ of_mod_opt env x_opt ^ " = " ^ current_mod env ^ ";\n")
| Instance (x1_opt, x2_opt) ->
Expand Down
Loading