From e9cbf1a88a2877a2c73c4651c712beb36f72b80b Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 1 Oct 2024 15:15:41 +0200 Subject: [PATCH 1/4] [spec] Fix typo in relaxed formula --- document/core/exec/numerics.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/exec/numerics.rst b/document/core/exec/numerics.rst index cfbe1ae7..38b25449 100644 --- a/document/core/exec/numerics.rst +++ b/document/core/exec/numerics.rst @@ -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:: From 8e5f4eeaa1aaf407a21cf0f1268519dba8ee6b4e Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 3 Oct 2024 10:51:18 +0200 Subject: [PATCH 2/4] [spec] Various fixes to SIMD stuff --- document/core/exec/instructions.rst | 31 +++++++++++++++++++++-------- document/core/exec/numerics.rst | 30 ++++++++++++++-------------- 2 files changed, 38 insertions(+), 23 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index e5297742..24d73e24 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -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: @@ -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)`. @@ -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} @@ -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)`. @@ -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)) diff --git a/document/core/exec/numerics.rst b/document/core/exec/numerics.rst index 38b25449..44f823ee 100644 --- a/document/core/exec/numerics.rst +++ b/document/core/exec/numerics.rst @@ -88,8 +88,8 @@ 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} @@ -97,8 +97,8 @@ Conventions: .. 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} @@ -860,11 +860,11 @@ The integer result of predicates -- i.e., :ref:`tests ` 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} @@ -894,11 +894,11 @@ The integer result of predicates -- i.e., :ref:`tests ` 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} @@ -922,11 +922,11 @@ The integer result of predicates -- i.e., :ref:`tests ` 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} @@ -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} @@ -2006,11 +2006,11 @@ Conversions * Let :math:`j` be the :ref:`signed interpretation ` 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} @@ -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 `, - it behaves like regular :math:`\truncu`. + it behaves like regular :math:`\truncsatu`. .. _op-relaxed_trunc_s: @@ -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 `, - it behaves like regular :math:`\truncs`. + it behaves like regular :math:`\truncsats`. .. _op-irelaxed_swizzle: From 2a30893e2868adbe0831af3c277728203bc70e8d Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 8 Oct 2024 11:45:33 +0200 Subject: [PATCH 3/4] [interpreter] Fix JS module invocation (#1829) --- interpreter/script/js.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml index ca25ac3e..2e796f7e 100644 --- a/interpreter/script/js.ml +++ b/interpreter/script/js.ml @@ -614,13 +614,16 @@ let rec of_result res = | EitherResult ress -> "[" ^ String.concat ", " (List.map of_result ress) ^ "]" +let of_module bs = + "module(" ^ of_bytes bs ^ ")" + let rec of_definition def = match def.it with - | Textual (m, _) -> of_bytes (Encode.encode m) - | Encoded (_, bs) -> of_bytes bs.it + | Textual (m, _) -> of_module (Encode.encode m) + | Encoded (_, bs) -> of_module bs.it | Quoted (_, s) -> try of_definition (snd (Parse.Module.parse_string ~offset:s.at s.it)) - with Parse.Syntax _ | Custom.Syntax _ -> of_bytes "" + with Parse.Syntax _ | Custom.Syntax _ -> of_module "" let of_instance env x_opt = "instance(" ^ of_mod_opt env x_opt ^ ")" @@ -628,7 +631,7 @@ let of_instance 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 - "call(instance(module(" ^ of_bytes bs ^ "), " ^ + "call(instance(" ^ of_module bs ^ ", " ^ "exports(" ^ x ^ ")), " ^ " \"run\", [])" let of_action env act = From 29b1fd4d3771b08d6a505fdce4bb2b3373dd7d61 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 8 Oct 2024 15:41:38 +0200 Subject: [PATCH 4/4] [interpreter] Proper fix for JS conversion (#1832) --- interpreter/script/js.ml | 22 ++++++++-------------- 1 file changed, 8 insertions(+), 14 deletions(-) diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml index 2e796f7e..adc072cb 100644 --- a/interpreter/script/js.ml +++ b/interpreter/script/js.ml @@ -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 @@ -614,24 +614,18 @@ let rec of_result res = | EitherResult ress -> "[" ^ String.concat ", " (List.map of_result ress) ^ "]" -let of_module bs = - "module(" ^ of_bytes bs ^ ")" - let rec of_definition def = match def.it with - | Textual (m, _) -> of_module (Encode.encode m) - | Encoded (_, bs) -> of_module bs.it + | Textual (m, _) -> of_bytes (Encode.encode m) + | Encoded (_, bs) -> of_bytes bs.it | Quoted (_, s) -> try of_definition (snd (Parse.Module.parse_string ~offset:s.at s.it)) - with Parse.Syntax _ | Custom.Syntax _ -> of_module "" - -let of_instance env x_opt = - "instance(" ^ of_mod_opt env x_opt ^ ")" + with Parse.Syntax _ | Custom.Syntax _ -> of_bytes "" 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 - "call(instance(" ^ of_module bs ^ ", " ^ + "call(instance(module(" ^ of_bytes bs ^ "), " ^ "exports(" ^ x ^ ")), " ^ " \"run\", [])" let of_action env act = @@ -680,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)) @@ -705,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) ->