diff --git a/LICENSE b/LICENSE index ce8035027..b70114b7a 100644 --- a/LICENSE +++ b/LICENSE @@ -2,9 +2,10 @@ Please see the LICENSE file in each top-level directory for the terms applicable The relevant directories and licenses are: -document/ - W3C Software and Document Notice and License -spectec/ - Apache License 2.0 -interpreter/ - Apache License 2.0 -test/ - Apache License 2.0 -proposals/ - Creative Commons Universal 1.0 International License (CC0) -papers/ - Creative Commons Attribution 4.0 International License (CC BY 4.0) +document/ - W3C Software and Document Notice and License +specification/ - W3C Software and Document Notice and License +spectec/ - Apache License 2.0 +interpreter/ - Apache License 2.0 +test/ - Apache License 2.0 +proposals/ - Creative Commons Universal 1.0 International License (CC0) +papers/ - Creative Commons Attribution 4.0 International License (CC BY 4.0) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 04c53f82d..a4da2bcc6 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1176,10 +1176,10 @@ Expressions An :ref:`expression ` is *evaluated* relative to a :ref:`current ` :ref:`frame ` pointing to its containing :ref:`module instance `. -$${rule-prose: Eval_expr} +$${rule-prose-ignore: Eval_expr} -$${rule: Eval_expr} +$${rule-ignore: Eval_expr} -.. note:: - Evaluation iterates this reduction rule until reaching a value. - Expressions constituting :ref:`function ` bodies are executed during function :ref:`invocation `. +Expression evaluation iterates single-step reduction until reaching a sequence of resulting :ref:`values `. + +Expressions constituting :ref:`function ` bodies are executed during function :ref:`invocation `. diff --git a/document/core/exec/numerics.rst b/document/core/exec/numerics.rst index d0180ab19..77762fd8d 100644 --- a/document/core/exec/numerics.rst +++ b/document/core/exec/numerics.rst @@ -1051,7 +1051,7 @@ then its sign is non-deterministic and the :ref:`payload ` is co * Otherwise the payload is picked non-deterministically among all :ref:`arithmetic NaNs `; that is, its most significant bit is :math:`1` and all others are unspecified. -* In the :ref:`deterministic profile `, however, a positive canonical NaNs is reliably produced in the latter case. +* In the :ref:`deterministic profile `, only positive canonical NaN outputs are produced. The non-deterministic result is expressed by the following auxiliary function producing a set of allowed outputs from a set of inputs: @@ -1059,9 +1059,9 @@ The non-deterministic result is expressed by the following auxiliary function pr \begin{array}{llcl@{\qquad}l} & \nans_N\{z^\ast\} &=& \{ + \NAN(\canon_N) \} \\ \exprofiles{\PROFDET} & \nans_N\{z^\ast\} &=& \{ + \NAN(n), - \NAN(n) ~|~ n = \canon_N \} - & (\iff \{z^\ast\} \subseteq \{ + \NAN(\canon_N), - \NAN(\canon_N) \} \\ + & (\iff \forall \,{\pm \NAN(n)} \in z^\ast,~ n = \canon_N) \\ \exprofiles{\PROFDET} & \nans_N\{z^\ast\} &=& \{ + \NAN(n), - \NAN(n) ~|~ n \geq \canon_N \} - & (\iff \{z^\ast\} \not\subseteq \{ + \NAN(\canon_N), - \NAN(\canon_N) \} \\ + & (\iff \exists \,{\pm \NAN(n)} \in z^\ast,~ n \neq \canon_N) \\ \end{array} @@ -2221,7 +2221,7 @@ where :math:`f`, :math:`\sx_1`, :math:`\sx_2`, :math:`h`, and :math:`k` are inst \VEXTMUL{\K\_}\LOW{\K\_}\sx & \ivmul & \sx & \sx & 0 & M_2 \\ \VEXTMUL{\K\_}\HIGH{\K\_}\sx & \ivmul & \sx & \sx & M_2 & M_2 \\ \VDOT{\K\_}\S & \ivdot & \S & \S & 0 & M_1 \\ - \VRELAXEDDOT{\K\_}\S & \ivdotsat & \S & \relaxed(R_{\F{idot}})[ \S, \U ] & 0 & M_1 \\ + \VRELAXEDDOT{\K\_}\S & \ivrelaxeddot & \S & \relaxed(R_{\F{idot}})[ \S, \U ] & 0 & M_1 \\ \end{array} .. note:: @@ -2533,16 +2533,21 @@ where: it behaves like regular :math:`\ivswizzle`. -.. _op-irelaxed_dot: +.. _op-ivrelaxed_dot: .. _op-irelaxed_dot_add: -:math:`\VRELAXEDDOT(i_1, i_2)` -.............................. +:math:`\ivrelaxeddot_N(i_1^{2m}, i_2^{2m})` +........................................... The implementation-specific behaviour of this operation is determined by the global parameter :math:`R_{\F{idot}} \in \{0, 1\}`. -It also affects the behaviour of :math:`\VRELAXEDDOTADD`. +It also affects the behaviour of :math:`\VRELAXEDDOT` and :math:`\VRELAXEDDOTADD` specified :ref:`above `. + +* Return :math:`\relaxed(R_{\F{idot}})[ \ivdot_N(i_1^{2m}, i_2^{2m}), \ivdotsat_N(i_1^{2m}, i_2^{2m}) ]`. -Its definition is part of the definition of :math:`\vextbinop` specified :ref:`above `. +.. math:: + \begin{array}{@{}lcll} + \ivrelaxeddot_N(i_1^{2m}, i_2^{2m}) &=& \relaxed(R_{\F{idot}})[ \ivdot_N(i_1^{2m}, i_2^{2m}), \ivdotsat_N(i_1^{2m}, i_2^{2m}) ] \\ + \end{array} .. note:: Relaxed dot product is implementation-dependent when the second operand is negative in a signed intepretation. diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst index 1253da807..05a035a6d 100644 --- a/document/core/syntax/modules.rst +++ b/document/core/syntax/modules.rst @@ -111,7 +111,7 @@ Conventions * For every index space ${-:abcidx}, the notation ${-:$abcidx(A)} denotes the set of indices from that index space occurring free in ${:A}. Sometimes this set is reinterpreted as the :ref:`list ` of its elements. .. note:: - For example, if ${:instr*} is ${instr*: (DATA.DROP 1) (MEMORY.INIT 2 3)}, then ${:$dataidx_instrs(instr*) = 1 3}, or equivalently, the set ${:`{1, 3}}. + For example, if ${:instr*} is ${instr*: (DATA.DROP 1) (MEMORY.INIT 2 3)}, then ${:$dataidx(instr*) = 1 3}, or equivalently, the set ${:`{1, 3}}. .. index:: ! type definition, type index, function type, aggregate type diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 44584df28..3732aa2b6 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -1711,7 +1711,7 @@ .. |frelaxedmin| mathdef:: \xref{exec/numerics}{op-frelaxed_min}{\F{frelaxed\_min}} .. |frelaxedmax| mathdef:: \xref{exec/numerics}{op-frelaxed_max}{\F{frelaxed\_max}} .. |irelaxedq15mulrs| mathdef:: \xref{exec/numerics}{op-irelaxed_q15mulr_s}{\F{irelaxed\_q15mulr\_s}} -.. |irelaxeddot| mathdef:: \xref{exec/numerics}{op-irelaxed_dot}{\F{irelaxed\_dot}} +.. |ivrelaxeddot| mathdef:: \xref{exec/numerics}{op-ivrelaxed_dot}{\F{ivrelaxed\_dot}} .. Numerics, meta functions diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 7c70bb580..4bef40ac0 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1364,8 +1364,6 @@ $${rule-prose: Instrs_ok} $${rule: Instrs_ok/empty} -$${rule: Instrs_ok/instr} - $${rule: Instrs_ok/seq} $${rule: Instrs_ok/sub} diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst index 0043063d9..b8a5c725d 100644 --- a/document/core/valid/matching.rst +++ b/document/core/valid/matching.rst @@ -131,7 +131,7 @@ Field Types $${rule-prose: Fieldtype_sub} -$${rule: {Fieldtype_sub/*}} +$${rule: {Fieldtype_sub/var}} $${rule-prose: Storagetype_sub} @@ -208,7 +208,7 @@ Global Types $${rule-prose: Globaltype_sub} -$${rule: {Globaltype_sub/*}} +$${rule: {Globaltype_sub/var}} .. index:: memory type, limits diff --git a/document/js-api/index.bs b/document/js-api/index.bs index 64dfd22f7..0348c193e 100644 --- a/document/js-api/index.bs +++ b/document/js-api/index.bs @@ -237,8 +237,11 @@ urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: df text: tag text: global type; url: syntax/types.html#syntax-globaltype url: syntax/types.html#syntax-mut - text: var - text: const + text: mut + url: syntax/types.html#syntax-comptype; for: comp-type + text: func + text: defined type; url: valid/conventions.html#syntax-deftype + text: expansion; url: valid/conventions.html#aux-expand-deftype text: address; url: exec/runtime.html#addresses text: signed_31; url: exec/numerics.html#aux-signed text: signed_32; url: exec/numerics.html#aux-signed @@ -256,6 +259,7 @@ urlPrefix: https://webidl.spec.whatwg.org/; spec: WebIDL text: [EnforceRange]; url: #EnforceRange text: unsigned long; url: #idl-unsigned-long text: js-unsigned-long; url: #js-unsigned-long + text: converted to a JavaScript value; url: #dfn-convert-idl-to-javascript-value urlPrefix: https://webassembly.github.io/js-types/js-api/; spec: WebAssembly JS API (JS Type Reflection) type: abstract-op; text: FromValueType; url: abstract-opdef-fromvaluetype urlPrefix: https://tc39.es/proposal-resizablearraybuffer/; spec: ResizableArrayBuffer proposal @@ -366,8 +370,8 @@ dictionary WebAssemblyInstantiatedSource { }; dictionary WebAssemblyCompileOptions { - USVString? importedStringConstants; - sequence<USVString> builtins; + USVString? importedStringConstants = null; + sequence<USVString> builtins = []; }; [Exposed=*] @@ -409,7 +413,7 @@ To validate builtins and imported string for a WebAssembly module fro 1. [=list/iterate|For each=] |import| of [=module_imports=](|module|), 1. If |importedStringModule| is not null and |import|[0] equals |importedStringModule|, 1. Let |importExternType| be |import|[2]. - 1. Let |stringExternType| be `global const (ref extern)`. + 1. Let |stringExternType| be [=external-type/global=] [=ref=] [=heap-type/extern=]. 1. If [=match_externtype=](|stringExternType|, |importExternType|) is false, return false 1. Else, 1. If [=validate an import for builtins|validating an import for builtins=] with |import| and |builtinSetNames| is false, return false. @@ -528,7 +532,7 @@ To instantiate imported strings with module |module| and |importedStr 1. Throw a {{LinkError}} exception. 1. Let |value| be [=ToWebAssemblyValue=](|v|, |valtype|). If this operation throws a {{TypeError}}, catch it, and throw a {{LinkError}} exception. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. - 1. Let (|store|, |globaladdr|) be [=global_alloc=](|store|, [=const=] |valtype|, |value|). + 1. Let (|store|, |globaladdr|) be [=global_alloc=](|store|, |valtype|, |value|). 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. 1. Let |externglobal| be [=external value/global=] |globaladdr|. 1. [=list/Append=] |externglobal| to |imports|. @@ -877,7 +881,7 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each 1. If |descriptor|["address"] [=map/exists=], let |addrtype| be [=ToValueType=](|descriptor|["address"]); otherwise, let |addrtype| be [=i32=]. 1. Let |initial| be [=?=] [=AddressValueToU64=](|descriptor|["initial"], |addrtype|). 1. If |descriptor|["maximum"] [=map/exists=], let |maximum| be [=?=] [=AddressValueToU64=](|descriptor|["maximum"], |addrtype|); otherwise, let |maximum| be empty. - 1. Let |memtype| be [=memory type=] |addrtype| { **min** |initial|, **max** |maximum| }. + 1. Let |memtype| be the [=memory type=] |addrtype| [|initial| .. |maximum|] page. 1. If |memtype| is not [=valid memtype|valid=], throw a {{RangeError}} exception. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let (|store|, |memaddr|) be [=mem_alloc=](|store|, |memtype|). If allocation fails, throw a {{RangeError}} exception. @@ -918,7 +922,7 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each The grow(|delta|) method, when invoked, performs the following steps: 1. Let |memaddr| be **this**.\[[Memory]]. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. - 1. Let |addrtype| be the [=address type=] in [=mem_type=](|store|, |memaddr|). + 1. Let (|addrtype|, limits) be [=mem_type=](|store|, |memaddr|). 1. Let |delta64| be [=?=] [=AddressValueToU64=](|delta|, |addrtype|). 1. Let |ret| be the result of [=grow the memory buffer|growing the memory buffer=] associated with |memaddr| by |delta64|. 1. Return [=U64ToAddressValue=](|ret|, |addrtype|). @@ -1044,7 +1048,7 @@ Each {{Table}} object has a \[[Table]] internal slot, which is a [=table address 1. If |descriptor|["address"] [=map/exists=], let |addrtype| be [=ToValueType=](|descriptor|["address"]); otherwise, let |addrtype| be [=i32=]. 1. Let |initial| be [=?=] [=AddressValueToU64=](|descriptor|["initial"], |addrtype|). 1. If |descriptor|["maximum"] [=map/exists=], let |maximum| be [=?=] [=AddressValueToU64=](|descriptor|["maximum"], |addrtype|); otherwise, let |maximum| be empty. - 1. Let |type| be the [=table type=] |addrtype| { [=limits|min=] |initial|, [=limits|max=] |maximum| } |elementtype|. + 1. Let |type| be the [=table type=] |addrtype| [|initial| .. |maximum|] |elementtype|. 1. If |type| is not [=valid tabletype|valid=], throw a {{RangeError}} exception. 1. If |value| is missing, 1. Let |ref| be [=DefaultValue=](|elementtype|). @@ -1082,7 +1086,7 @@ Each {{Table}} object has a \[[Table]] internal slot, which is a [=table address The getter of the length attribute of {{Table}}, when invoked, performs the following steps: 1. Let |tableaddr| be **this**.\[[Table]]. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. - 1. Let |addrtype| be the [=address type=] in [=table_type=](|store|, |tableaddr|). + 1. Let (|addrtype|, limits, elementtype) be [=table_type=](|store|, |tableaddr|). 1. Let |length64| be [=table_size=](|store|, |tableaddr|). 1. Return [=U64ToAddressValue=](|length64|, |addrtype|). @@ -1201,7 +1205,7 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each 1. Assert: |value| is not [=error=]. 1. Otherwise, 1. Let |value| be [=?=] [=ToWebAssemblyValue=](|v|, |valuetype|). - 1. If |mutable| is true, let |globaltype| be [=var=] |valuetype|; otherwise, let |globaltype| be [=const=] |valuetype|. + 1. If |mutable| is true, let |globaltype| be [=mut=] |valuetype|; otherwise, let |globaltype| be |valuetype|. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let (|store|, |globaladdr|) be [=global_alloc=](|store|, |globaltype|, |value|). 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. @@ -1229,7 +1233,7 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each 1. Let |globaladdr| be **this**.\[[Global]]. 1. Let |mut| |valuetype| be [=global_type=](|store|, |globaladdr|). 1. If |valuetype| [=matches/valtype|matches=] [=v128=] or [=exnref=], throw a {{TypeError}}. - 1. If |mut| is [=const=], throw a {{TypeError}}. + 1. If |mut| is empty, throw a {{TypeError}}. 1. Let |value| be [=?=] [=ToWebAssemblyValue=](**the given value**, |valuetype|). 1. Let |store| be [=global_write=](|store|, |globaladdr|, |value|). 1. If |store| is [=error=], throw a {{RangeError}} exception. @@ -1272,7 +1276,7 @@ This slot holds a [=function address=] relative to the [=surrounding agent=]'s [ 1. Let |realm| be the [=current Realm=]. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let |functype| be [=func_type=](|store|, |funcaddr|). - 1. Let [|paramTypes|] → [resultTypes] be |functype|. + 1. Let [=comp-type/func=] |paramTypes| → resultTypes be the [=expansion=] of |functype|. 1. Let |arity| be |paramTypes|'s [=list/size=]. 1. Let |name| be the [=name of the WebAssembly function=] |funcaddr|. 1. Let |function| be [$CreateBuiltinFunction$](|steps|, |arity|, |name|, « \[[FunctionAddress]] », |realm|). @@ -1286,7 +1290,7 @@ This slot holds a [=function address=] relative to the [=surrounding agent=]'s [ 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let |functype| be [=func_type=](|store|, |funcaddr|). - 1. Let [|parameters|] → [|results|] be |functype|. + 1. Let [=comp-type/func=] |parameters| → |results| be the [=expansion=] of |functype|. 1. If any type in |parameters| or |results| [=matches/valtype|matches=] [=v128=] or [=exnref=], throw a {{TypeError}}. Note: the above error is thrown each time the \[[Call]] method is invoked. @@ -1326,7 +1330,7 @@ Note: Exported Functions do not have a \[[Construct]] method and thus it is not
To run a host function from the JavaScript object |func|, type |functype|, and [=list=] of [=WebAssembly values=] |arguments|, perform the following steps: - 1. Let [|parameters|] → [|results|] be |functype|. + 1. Let [=comp-type/func=] |parameters| → |results| be the [=expansion=] of |functype|. 1. If any type in |parameters| or |results| [=matches/valtype|matches=] [=v128=] or [=exnref=], throw a {{TypeError}}. 1. Let |jsArguments| be « ». 1. [=list/iterate|For each=] |arg| of |arguments|, @@ -1487,19 +1491,23 @@ The algorithm ToWebAssemblyValue(|v|, |type|) coerces a JavaScript va
-The algorithm AddressValueToU64(|v|, |addrtype|) converts a JavaScript value to a WebAssembly [=u64=] for use in embedding operations. It is designed to act like [=[EnforceRange]=] [=unsigned long=] for {{AddressType}} "i32", and to extend these semantics to {{AddressType}} "i64", by performing the following steps: +The algorithm AddressValueToU64(|v|, |addrtype|) converts an IDL value to a WebAssembly [=u64=] for use in embedding operations. It is designed to act like [=[EnforceRange]=] [=unsigned long=] for {{AddressType}} "i32", and to extend these semantics to {{AddressType}} "i64", by performing the following steps: + +1. Let |jsValue| be |v|, [=converted to a JavaScript value=]. + Note: The IDL `any` type is a discriminated union, not a transparent wrapper around a JavaScript value. 1. If |addrtype| is [=i32=], - 1. Let |n| be [=?=] [$ConvertToInt$](|v|, 32, "unsigned"), where the destination type is associated with [=[EnforceRange]=]. + 1. Let |n| be [=?=] [$ConvertToInt$](|jsValue|, 32, "unsigned"), where the destination type is associated with [=[EnforceRange]=]. Note: This is equivalent to the [=js-unsigned-long|JS conversion rules=] for [=[EnforceRange]=] [=unsigned long=]. 1. Return [=ℝ=](|n|) as a WebAssembly [=u64=]. 1. If |addrtype| is [=i64=], - 1. Let |n| be [=?=] [$ToBigInt$](|v|). - 1. If |n| < 0 or |n| > 264 − 1, [=throw=] a {{TypeError}}. + 1. Let |n| be [=?=] [$ToBigInt$](|jsValue|). + 1. Let |r| be [=ℝ=](|n|). + 1. If |r| < 0 or |r| > 264 − 1, [=throw=] a {{TypeError}}. Note: This operation is designed to emulate [=[EnforceRange]=]. - 1. Return [=ℝ=](|n|) as a WebAssembly [=u64=]. + 1. Return |r| as a WebAssembly [=u64=]. 1. Assert: This step is not reached.
@@ -1561,8 +1569,9 @@ The new Tag(|type|) constructor 1. Let |wasmParameters| be «». 1. [=list/iterate|For each=] |paramType| of |parameters|, 1. [=list/Append=] [=ToValueType=](|paramType|) to |wasmParameters|. +1. Let |tagtype| be the [=defined type=] such that [=comp-type/func=] |wasmParameters| → « » is the [=expansion=] of |tagtype|. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. -1. Let (|store|, |tagAddress|) be [=tag_alloc=](|store|, |wasmParameters| → « »). +1. Let (|store|, |tagAddress|) be [=tag_alloc=](|store|, |tagtype|). 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. 1. [=initialize a Tag object|Initialize=] **this** from |tagAddress|. @@ -1732,7 +1741,7 @@ constructor steps are: 1. If |exceptionTag|.\[[Address]] is equal to |JSTagAddr|, 1. Throw a {{TypeError}}. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. -1. Let [|types|] → [] be [=tag_type=](|store|, |exceptionTag|.\[[Address]]). +1. Let [=comp-type/func=] |types| → « » be the [=expansion=] of [=tag_type=](|store|, |exceptionTag|.\[[Address]]). 1. If |types|'s [=list/size=] is not |payload|'s [=list/size=], 1. Throw a {{TypeError}}. 1. Let |wasmPayload| be « ». @@ -1761,7 +1770,7 @@ The getArg(|exceptionTag|, |index|) method ste 1. Assert: |tagaddr| is equal to **this**.\[[Type]]. 1. If |index| ≥ |payload|'s [=list/size=], 1. Throw a {{RangeError}}. -1. Let [|types|] → [] be [=tag_type=](|store|, |tagaddr|). +1. Let [=comp-type/func=] |types| → « » be the [=expansion=] of [=tag_type=](|store|, |tagaddr|). 1. If |types|[|index|] [=matches/valtype|matches=] [=v128=] or [=exnref=], 1. Throw a {{TypeError}}. 1. Return [=ToJSValue=](|payload|[|index|]). @@ -1799,8 +1808,9 @@ To get the JavaScript exception tag, perform the following steps: 1. If the [=surrounding agent=]'s associated [=JavaScript exception tag=] has been initialized, 1. return the [=surrounding agent=]'s associated [=JavaScript exception tag=] + 1. Let |tagtype| be the [=defined type=] such that [=comp-type/func=] « [=externref=] » → « » is the [=expansion=] of |tagtype|. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. - 1. Let (|store|, |tagAddress|) be [=tag_alloc=](|store|, « [=externref=] » → « »). + 1. Let (|store|, |tagAddress|) be [=tag_alloc=](|store|, |tagtype|). 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. 1. Set the [=surrounding agent=]'s associated [=JavaScript exception tag=] to |tagAddress|. 1. return |tagAddress|. diff --git a/specification/wasm-1.0/A-binary.spectec b/specification/wasm-1.0/A-binary.spectec index ce3ede9c7..552a61a56 100644 --- a/specification/wasm-1.0/A-binary.spectec +++ b/specification/wasm-1.0/A-binary.spectec @@ -52,7 +52,7 @@ var ch : char def $utf8(ch) = b -- if ch < U+0080 /\ ch = b def $utf8(ch) = b_1 b_2 -- if U+0080 <= ch < U+0800 /\ ch = $(2^6*(b_1 - 0xC0) + (b_2 - 0x80)) def $utf8(ch) = b_1 b_2 b_3 -- if (U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000) /\ ch = $(2^12*(b_1 - 0xE0) + 2^6*(b_2 - 0x80) + (b_3 - 0x80)) -def $utf8(ch) = b_1 b_2 b_3 b_4 -- if (U+10000 <= ch < U+11000) /\ ch = $(2^18*(b_1 - 0xF0) + 2^12*(b_2 - 0x80) + 2^6*(b_3 - 0x80) + (b_4 - 0x80)) +def $utf8(ch) = b_1 b_2 b_3 b_4 -- if (U+10000 <= ch < U+110000) /\ ch = $(2^18*(b_1 - 0xF0) + 2^12*(b_2 - 0x80) + 2^6*(b_3 - 0x80) + (b_4 - 0x80)) def $utf8(ch*) = $concat_(byte, $utf8(ch)*) grammar Bname : name = diff --git a/specification/wasm-2.0/A-binary.spectec b/specification/wasm-2.0/A-binary.spectec index 8570e0b2e..5935ad391 100644 --- a/specification/wasm-2.0/A-binary.spectec +++ b/specification/wasm-2.0/A-binary.spectec @@ -54,7 +54,7 @@ var ch : char def $utf8(ch) = b -- if ch < U+0080 /\ ch = b def $utf8(ch) = b_1 b_2 -- if U+0080 <= ch < U+0800 /\ ch = $(2^6*(b_1 - 0xC0) + (b_2 - 0x80)) def $utf8(ch) = b_1 b_2 b_3 -- if (U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000) /\ ch = $(2^12*(b_1 - 0xE0) + 2^6*(b_2 - 0x80) + (b_3 - 0x80)) -def $utf8(ch) = b_1 b_2 b_3 b_4 -- if (U+10000 <= ch < U+11000) /\ ch = $(2^18*(b_1 - 0xF0) + 2^12*(b_2 - 0x80) + 2^6*(b_3 - 0x80) + (b_4 - 0x80)) +def $utf8(ch) = b_1 b_2 b_3 b_4 -- if (U+10000 <= ch < U+110000) /\ ch = $(2^18*(b_1 - 0xF0) + 2^12*(b_2 - 0x80) + 2^6*(b_3 - 0x80) + (b_4 - 0x80)) def $utf8(ch*) = $concat_(byte, $utf8(ch)*) grammar Bname : name = diff --git a/specification/wasm-3.0/1.3-syntax.instructions.spectec b/specification/wasm-3.0/1.3-syntax.instructions.spectec index 8571df71d..ad9f67449 100644 --- a/specification/wasm-3.0/1.3-syntax.instructions.spectec +++ b/specification/wasm-3.0/1.3-syntax.instructions.spectec @@ -385,7 +385,7 @@ syntax instr/vec hint(desc "vector instruction") = ... | VCVTOP shape_1 shape_2 vcvtop__(shape_2, shape_1) hint(show ##%1.%3#_# ##%2) | VSPLAT shape hint(show ##%.SPLAT) hint(macro "VSPLAT") | VEXTRACT_LANE shape sx? laneidx hint(show ##%.EXTRACT_LANE %) hint(show ##%.EXTRACT_LANE#_#% %) hint(macro "VEXTRACT_LANE") - -- if sx? = eps <=> $lanetype(shape) <- I32 I64 F32 F64 + -- if sx? = eps <=> $lanetype(shape) = numtype | VREPLACE_LANE shape laneidx hint(show ##%.REPLACE_LANE %) hint(macro "VREPLACE_LANE") | ... diff --git a/specification/wasm-3.0/3.0-numerics.relaxed.spectec b/specification/wasm-3.0/3.0-numerics.relaxed.spectec index 212c948ba..0c574d706 100644 --- a/specification/wasm-3.0/3.0-numerics.relaxed.spectec +++ b/specification/wasm-3.0/3.0-numerics.relaxed.spectec @@ -20,7 +20,7 @@ def $R_fmin : relaxed4 hint(builtin) def $R_fmax : relaxed4 hint(builtin) def $R_idot : relaxed2 hint(builtin) def $R_iq15mulr : relaxed2 hint(builtin) -def $R_trunc_u : relaxed4 hint(builtin) +def $R_trunc_u : relaxed2 hint(builtin) def $R_trunc_s : relaxed2 hint(builtin) def $R_swizzle : relaxed2 hint(builtin) def $R_laneselect : relaxed2 hint(builtin) diff --git a/specification/wasm-3.0/3.1-numerics.scalar.spectec b/specification/wasm-3.0/3.1-numerics.scalar.spectec index 7ac9dad59..8176526d0 100644 --- a/specification/wasm-3.0/3.1-numerics.scalar.spectec +++ b/specification/wasm-3.0/3.1-numerics.scalar.spectec @@ -10,7 +10,7 @@ def $s33_to_u32(s33) : u32 hint(show %) ;; Representation def $ibits_(N, iN(N)) : bit* hint(show $bits_($IN(%),%)) hint(inverse $inv_ibits_) -def $fbits_(N, fN(N)) : bit* hint(show $bits_($FN(%),%)) hint(inverse $inv_ibits_) +def $fbits_(N, fN(N)) : bit* hint(show $bits_($FN(%),%)) hint(inverse $inv_fbits_) def $ibytes_(N, iN(N)) : byte* hint(show $bytes_($IN(%),%)) hint(inverse $inv_ibytes_) def $fbytes_(N, fN(N)) : byte* hint(show $bytes_($FN(%),%)) hint(inverse $inv_fbytes_) def $nbytes_(numtype, num_(numtype)) : byte* hint(show $bytes_(%,%)) hint(inverse $inv_nbytes_) diff --git a/specification/wasm-3.0/3.2-numerics.vector.spectec b/specification/wasm-3.0/3.2-numerics.vector.spectec index c88b9dadf..cbdee7701 100644 --- a/specification/wasm-3.0/3.2-numerics.vector.spectec +++ b/specification/wasm-3.0/3.2-numerics.vector.spectec @@ -368,6 +368,9 @@ def $ivdot_sat_(N, iN(N)*, iN(N)*) : iN(N)* hint(show $ivdot__sat_(%,%,%)) def $ivdot_sat_(N, i_1*, i_2*) = $iadd_sat_(N, S, j_1, j_2)* -- if $concat_(iN(N), (j_1 j_2)*) = $imul_(N, i_1, i_2)* +def $ivrelaxed_dot_(N, iN(N)*, iN(N)*) : iN(N)* hint(show $ivrelaxed__dot_(%,%,%)) +def $ivrelaxed_dot_(N, i_1*, i_2*) = $relaxed2($R_idot, iN(N)*, $ivdot_(N, i_1*, i_2*), $ivdot_sat_(N, i_1*, i_2*)) + def $vextunop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTADD_PAIRWISE sx, v_1) = $ivextunop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivadd_pairwise_, sx, v_1) @@ -376,7 +379,7 @@ def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTMUL half sx, v_1, v_2) = def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, DOT S, v_1, v_2) = $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivdot_, S, S, 0, M_1, v_1, v_2) def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, RELAXED_DOT S, v_1, v_2) = - $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivdot_sat_, S, $relaxed2($R_idot, sx, S, U), 0, M_1, v_1, v_2) + $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivrelaxed_dot_, S, $relaxed2($R_idot, sx, S, U), 0, M_1, v_1, v_2) (; ;; TODO(2, rossberg): this is obsolete, clean up diff --git a/specification/wasm-3.0/5.1-binary.values.spectec b/specification/wasm-3.0/5.1-binary.values.spectec index 6bb898de2..4034c015e 100644 --- a/specification/wasm-3.0/5.1-binary.values.spectec +++ b/specification/wasm-3.0/5.1-binary.values.spectec @@ -60,7 +60,7 @@ def $utf8(ch) = b_1 b_2 b_3 -- if U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000 -- if ch = $(2^12*(b_1 - 0xE0) + 2^6*$cont(b_2) + $cont(b_3)) def $utf8(ch) = b_1 b_2 b_3 b_4 - -- if U+10000 <= ch < U+11000 + -- if U+10000 <= ch < U+110000 -- if ch = $(2^18*(b_1 - 0xF0) + 2^12*$cont(b_2) + 2^6*$cont(b_3) + $cont(b_4)) grammar Bname : name = diff --git a/specification/wasm-latest/1.3-syntax.instructions.spectec b/specification/wasm-latest/1.3-syntax.instructions.spectec index 8571df71d..ad9f67449 100644 --- a/specification/wasm-latest/1.3-syntax.instructions.spectec +++ b/specification/wasm-latest/1.3-syntax.instructions.spectec @@ -385,7 +385,7 @@ syntax instr/vec hint(desc "vector instruction") = ... | VCVTOP shape_1 shape_2 vcvtop__(shape_2, shape_1) hint(show ##%1.%3#_# ##%2) | VSPLAT shape hint(show ##%.SPLAT) hint(macro "VSPLAT") | VEXTRACT_LANE shape sx? laneidx hint(show ##%.EXTRACT_LANE %) hint(show ##%.EXTRACT_LANE#_#% %) hint(macro "VEXTRACT_LANE") - -- if sx? = eps <=> $lanetype(shape) <- I32 I64 F32 F64 + -- if sx? = eps <=> $lanetype(shape) = numtype | VREPLACE_LANE shape laneidx hint(show ##%.REPLACE_LANE %) hint(macro "VREPLACE_LANE") | ... diff --git a/specification/wasm-latest/3.0-numerics.relaxed.spectec b/specification/wasm-latest/3.0-numerics.relaxed.spectec index 212c948ba..0c574d706 100644 --- a/specification/wasm-latest/3.0-numerics.relaxed.spectec +++ b/specification/wasm-latest/3.0-numerics.relaxed.spectec @@ -20,7 +20,7 @@ def $R_fmin : relaxed4 hint(builtin) def $R_fmax : relaxed4 hint(builtin) def $R_idot : relaxed2 hint(builtin) def $R_iq15mulr : relaxed2 hint(builtin) -def $R_trunc_u : relaxed4 hint(builtin) +def $R_trunc_u : relaxed2 hint(builtin) def $R_trunc_s : relaxed2 hint(builtin) def $R_swizzle : relaxed2 hint(builtin) def $R_laneselect : relaxed2 hint(builtin) diff --git a/specification/wasm-latest/3.1-numerics.scalar.spectec b/specification/wasm-latest/3.1-numerics.scalar.spectec index 7ac9dad59..8176526d0 100644 --- a/specification/wasm-latest/3.1-numerics.scalar.spectec +++ b/specification/wasm-latest/3.1-numerics.scalar.spectec @@ -10,7 +10,7 @@ def $s33_to_u32(s33) : u32 hint(show %) ;; Representation def $ibits_(N, iN(N)) : bit* hint(show $bits_($IN(%),%)) hint(inverse $inv_ibits_) -def $fbits_(N, fN(N)) : bit* hint(show $bits_($FN(%),%)) hint(inverse $inv_ibits_) +def $fbits_(N, fN(N)) : bit* hint(show $bits_($FN(%),%)) hint(inverse $inv_fbits_) def $ibytes_(N, iN(N)) : byte* hint(show $bytes_($IN(%),%)) hint(inverse $inv_ibytes_) def $fbytes_(N, fN(N)) : byte* hint(show $bytes_($FN(%),%)) hint(inverse $inv_fbytes_) def $nbytes_(numtype, num_(numtype)) : byte* hint(show $bytes_(%,%)) hint(inverse $inv_nbytes_) diff --git a/specification/wasm-latest/3.2-numerics.vector.spectec b/specification/wasm-latest/3.2-numerics.vector.spectec index c88b9dadf..cbdee7701 100644 --- a/specification/wasm-latest/3.2-numerics.vector.spectec +++ b/specification/wasm-latest/3.2-numerics.vector.spectec @@ -368,6 +368,9 @@ def $ivdot_sat_(N, iN(N)*, iN(N)*) : iN(N)* hint(show $ivdot__sat_(%,%,%)) def $ivdot_sat_(N, i_1*, i_2*) = $iadd_sat_(N, S, j_1, j_2)* -- if $concat_(iN(N), (j_1 j_2)*) = $imul_(N, i_1, i_2)* +def $ivrelaxed_dot_(N, iN(N)*, iN(N)*) : iN(N)* hint(show $ivrelaxed__dot_(%,%,%)) +def $ivrelaxed_dot_(N, i_1*, i_2*) = $relaxed2($R_idot, iN(N)*, $ivdot_(N, i_1*, i_2*), $ivdot_sat_(N, i_1*, i_2*)) + def $vextunop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTADD_PAIRWISE sx, v_1) = $ivextunop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivadd_pairwise_, sx, v_1) @@ -376,7 +379,7 @@ def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, EXTMUL half sx, v_1, v_2) = def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, DOT S, v_1, v_2) = $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivdot_, S, S, 0, M_1, v_1, v_2) def $vextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, RELAXED_DOT S, v_1, v_2) = - $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivdot_sat_, S, $relaxed2($R_idot, sx, S, U), 0, M_1, v_1, v_2) + $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivrelaxed_dot_, S, $relaxed2($R_idot, sx, S, U), 0, M_1, v_1, v_2) (; ;; TODO(2, rossberg): this is obsolete, clean up diff --git a/specification/wasm-latest/5.1-binary.values.spectec b/specification/wasm-latest/5.1-binary.values.spectec index 6bb898de2..4034c015e 100644 --- a/specification/wasm-latest/5.1-binary.values.spectec +++ b/specification/wasm-latest/5.1-binary.values.spectec @@ -60,7 +60,7 @@ def $utf8(ch) = b_1 b_2 b_3 -- if U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000 -- if ch = $(2^12*(b_1 - 0xE0) + 2^6*$cont(b_2) + $cont(b_3)) def $utf8(ch) = b_1 b_2 b_3 b_4 - -- if U+10000 <= ch < U+11000 + -- if U+10000 <= ch < U+110000 -- if ch = $(2^18*(b_1 - 0xF0) + 2^12*$cont(b_2) + 2^6*$cont(b_3) + $cont(b_4)) grammar Bname : name = diff --git a/spectec/README.md b/spectec/README.md index bf88b51f0..4ecee1f43 100644 --- a/spectec/README.md +++ b/spectec/README.md @@ -107,9 +107,9 @@ You will need `ocaml` installed with `dune`, `menhir`, `mdx`, and the `zarith` l $ opam init ``` -* Set `ocaml` as version 5.1.0 or higher. +* Set `ocaml` as version 5.4.0 or higher. ``` - $ opam switch create 5.1.0 + $ opam switch create 5.4.0 ``` * Install `dune` version 3.11.0, `menhir` version 20230608, `mdx` version 2.3.1, and `zarith` version 1.13, via `opam` diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml index fe1dc3ee5..8439dd4c9 100644 --- a/spectec/src/backend-latex/render.ml +++ b/spectec/src/backend-latex/render.ml @@ -1078,6 +1078,7 @@ Printf.eprintf "[render_atom %s @ %s] id=%s def=%s macros: %s (%s)\n%!" | GreaterEqual -> "\\geq" | Equiv | EquivSub -> "\\equiv" | Approx | ApproxSub -> "\\approx" + | Sim | SimSub -> "\\sim" | Arrow | ArrowSub -> "\\rightarrow" | Arrow2 | Arrow2Sub -> "\\Rightarrow" | Sub -> "\\leq" diff --git a/spectec/src/frontend/lexer.mll b/spectec/src/frontend/lexer.mll index c10765b6c..50605fec4 100644 --- a/spectec/src/frontend/lexer.mll +++ b/spectec/src/frontend/lexer.mll @@ -174,8 +174,8 @@ and token = parse | "=_" { EQSUB } | "==_" { EQUIVSUB } | "~~_" { APPROXSUB } - - | "~" { NOT } + | "~_" { SIMSUB } + | "~" { SIM } | "/\\" { AND } | "\\/" { OR } | "(/\\)" { BIGAND } diff --git a/spectec/src/frontend/parser.mly b/spectec/src/frontend/parser.mly index 94f5ab086..40d472113 100644 --- a/spectec/src/frontend/parser.mly +++ b/spectec/src/frontend/parser.mly @@ -176,7 +176,7 @@ and short_alt_prod' = function %token COLON SEMICOLON COMMA DOT DOTDOT DOTDOTDOT BAR BARBAR DASH COLONSUB %token BIGAND BIGOR BIGFORALL BIGEXISTS BIGADD BIGMUL BIGCAT %token COMMA_NL NL_BAR NL_NL NL_NL_NL -%token EQ NE LT GT LE GE APPROX EQUIV ASSIGN SUB SUP EQCAT EQSUB EQUIVSUB APPROXSUB +%token EQ NE LT GT LE GE APPROX SIM EQUIV ASSIGN SUB SUP EQCAT EQSUB EQUIVSUB APPROXSUB SIMSUB %token NOT AND OR IMPL DIMPL %token QUEST PLUS MINUS STAR SLASH BACKSLASH UP CAT PLUSMINUS MINUSPLUS %token ARROW ARROW2 ARROWSUB ARROW2SUB SQARROW SQARROWSUB SQARROWSTAR SQARROWSTARSUB @@ -201,7 +201,7 @@ and short_alt_prod' = function %nonassoc TURNSTILE TURNSTILESUB %nonassoc TILESTURN TILESTURNSUB %right SQARROW SQARROWSUB SQARROWSTAR SQARROWSTARSUB PREC SUCC PRECSUB SUCCSUB BIGAND BIGOR BIGFORALL BIGEXISTS BIGADD BIGMUL BIGCAT -%left COLON SUB SUP ASSIGN EQUIV APPROX COLONSUB EQUIVSUB APPROXSUB +%left COLON SUB SUP ASSIGN EQUIV APPROX SIM COLONSUB EQUIVSUB APPROXSUB SIMSUB %left COMMA COMMA_NL %right EQ NE LT GT LE GE MEM NOTMEM EQSUB %right ARROW ARROWSUB @@ -344,7 +344,7 @@ atom_escape : | TICK PLUSMINUS { Atom.PlusMinus } | TICK MINUSPLUS { Atom.MinusPlus } | TICK STAR { Atom.Times } - | TICK NOT { Atom.Not } + | TICK SIM { Atom.Not } | TICK AND { Atom.And } | TICK OR { Atom.Or } | TICK IMPL { Atom.Arrow2 } @@ -353,7 +353,7 @@ atom_escape : | TICK CAT { Atom.Cat } | TICK COMMA { Atom.Comma } | TICK infixop_ { $2 } - | TICK relop_ { $2 } + | TICK relop_prefix_ { $2 } | BOT { Atom.Bot } | TOP { Atom.Top } | INFINITY { Atom.Infinity } @@ -391,6 +391,7 @@ check_atom : %inline unop : | NOT { `NotOp } + | SIM { `NotOp } | PLUS { `PlusOp } | MINUS { `MinusOp } | PLUSMINUS { `PlusMinusOp } @@ -442,9 +443,9 @@ check_atom : | ARROWSUB { Atom.ArrowSub } | ARROW2SUB { Atom.Arrow2Sub } -%inline relop : - | relop_ { $1 $$ $sloc } -%inline relop_ : +%inline relop_prefix : + | relop_prefix_ { $1 $$ $sloc } +%inline relop_prefix_ : | COLON { Atom.Colon } | SUB { Atom.Sub } | SUP { Atom.Sup } @@ -458,9 +459,15 @@ check_atom : | TILESTURN { Atom.Tilesturn } | TURNSTILE { Atom.Turnstile } -%inline relopsub : - | relopsub_ { $1 $$ $sloc } -%inline relopsub_ : +%inline relop : + | relop_ { $1 $$ $sloc } +%inline relop_ : + | relop_prefix_ { $1 } + | SIM { Atom.Sim } + +%inline relopsub_prefix : + | relopsub_prefix_ { $1 $$ $sloc } +%inline relopsub_prefix_ : | EQSUB { Atom.EqualSub } | COLONSUB { Atom.ColonSub } | EQUIVSUB { Atom.EquivSub } @@ -472,6 +479,12 @@ check_atom : | TILESTURNSUB { Atom.TilesturnSub } | TURNSTILESUB { Atom.TurnstileSub } +%inline relopsub : + | relopsub_ { $1 $$ $sloc } +%inline relopsub_ : + | relopsub_prefix_ { $1 } + | SIMSUB { Atom.SimSub } + (* Iteration *) @@ -638,8 +651,8 @@ nottyp_bin_ : nottyp_rel : nottyp_rel_ { $1 $ $sloc } nottyp_rel_ : | nottyp_bin_ { $1 } - | relop nottyp_rel { InfixT (SeqT [] $ $loc($1), $1, $2) } - | relopsub nottyp_prim nottyp_rel + | relop_prefix nottyp_rel { InfixT (SeqT [] $ $loc($1), $1, $2) } + | relopsub_prefix nottyp_prim nottyp_rel { InfixT (SeqT [] $ $loc($1), $1, cat_seq_typ $2 $3) } | nottyp_rel relop nottyp_rel { InfixT ($1, $2, $3) } | nottyp_rel relopsub nottyp_prim nottyp_rel @@ -798,8 +811,8 @@ exp_bin_ : exp_rel : exp_rel_ { $1 $ $sloc } exp_rel_ : | exp_bin_ { $1 } - | relop exp_rel { InfixE (SeqE [] $ $loc($1), $1, $2) } - | relopsub exp_prim exp_rel + | relop_prefix exp_rel { InfixE (SeqE [] $ $loc($1), $1, $2) } + | relopsub_prefix exp_prim exp_rel { InfixE (SeqE [] $ $loc($1), $1, cat_seq_exp $2 $3) } | exp_rel relop exp_rel { InfixE ($1, $2, $3) } | exp_rel relopsub exp_prim exp_rel { InfixE ($1, $2, cat_seq_exp $3 $4) } @@ -808,8 +821,8 @@ exp_comma : exp_comma_ { $1 $ $sloc } exp_comma_ : | exp_bin_ { $1 } | comma(exp) exp_comma { CommaE (SeqE [] $ $loc($1), $2) } - | relop exp_comma { InfixE (SeqE [] $ $loc($1), $1, $2) } - | relopsub exp_prim exp_comma + | relop_prefix exp_comma { InfixE (SeqE [] $ $loc($1), $1, $2) } + | relopsub_prefix exp_prim exp_comma { InfixE (SeqE [] $ $loc($1), $1, cat_seq_exp $2 $3) } | exp_comma comma(exp) exp_comma { CommaE ($1, $3) } | exp_comma relop exp_comma { InfixE ($1, $2, $3) } diff --git a/spectec/src/il2al/preprocess.ml b/spectec/src/il2al/preprocess.ml index 8c44dc02a..ca13e5e6c 100644 --- a/spectec/src/il2al/preprocess.ml +++ b/spectec/src/il2al/preprocess.ml @@ -138,8 +138,8 @@ let rec preprocess_prem prem = when turnstile.it = Turnstile && colon.it = Colon -> typing_functions := id.it :: !typing_functions; Some (lhs, rhs) - (* `lhs` ~~ `rhs` *) - | [[]; [approx]; []], TupE [lhs; rhs] when approx.it = Approx -> Some (lhs, rhs) + (* `lhs` ~~ `rhs` or `lhs` ~ `rhs` *) + | [[]; [op]; []], TupE [lhs; rhs] when op.it = Approx || op.it = Sim -> Some (lhs, rhs) | _ -> None in (match lhs_rhs_opt with diff --git a/spectec/src/xl/atom.ml b/spectec/src/xl/atom.ml index 73920e7ca..2f1461a71 100644 --- a/spectec/src/xl/atom.ml +++ b/spectec/src/xl/atom.ml @@ -41,6 +41,8 @@ and atom' = | EquivSub (* `==_` *) | Approx (* `~~` *) | ApproxSub (* `~~_` *) + | Sim (* `~` *) + | SimSub (* `~_` *) | SqArrow (* `~>` *) | SqArrowSub (* `~>_` *) | SqArrowStar (* `~>*` *) @@ -85,7 +87,7 @@ let compare atom1 atom2 = let is_sub atom = match atom.it with | Atom id -> id <> "" && id.[String.length id - 1] = '_' - | ArrowSub | Arrow2Sub | ColonSub | EqualSub | EquivSub | ApproxSub + | ArrowSub | Arrow2Sub | ColonSub | EqualSub | EquivSub | ApproxSub | SimSub | SqArrowSub | SqArrowStarSub | PrecSub | SuccSub | TurnstileSub | TilesturnSub -> true | _ -> false @@ -99,6 +101,7 @@ let sub atom1 atom2 = | EqualSub, Equal | EquivSub, Equiv | ApproxSub, Approx + | SimSub, Sim | SqArrowSub, SqArrow | SqArrowStarSub, SqArrowStar | PrecSub, Prec @@ -143,6 +146,8 @@ let to_string atom = | EquivSub -> "==_" | Approx -> "~~" | ApproxSub -> "~~_" + | Sim -> "~" + | SimSub -> "~_" | SqArrow -> "~>" | SqArrowSub -> "~>_" | SqArrowStar -> "~>*" @@ -221,6 +226,8 @@ let name atom = | EquivSub -> "equiv_" | Approx -> "approx" | ApproxSub -> "approx_" + | Sim -> "sim" + | SimSub -> "sim_" | SqArrow -> "sqarrow" (* Latex: \hookrightarrow *) | SqArrowSub -> "sqarrow_" (* Latex: \hookrightarrow with subscript *) | SqArrowStar -> "sqarrowstar" (* Latex: \hookrightarrow^\ast *) diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index ac80b4f38..49bb3274c 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -801,7 +801,7 @@ def $utf8(char*) : byte* -- if (ch!`%`_char.0 = ((((2 ^ 12) * (((b_1!`%`_byte.0 : nat <:> int) - (224 : nat <:> int)) : int <:> nat)) + ((2 ^ 6) * $cont(b_2))) + $cont(b_3))) ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec:62.1-64.82 def $utf8{ch : char, b_1 : byte, b_2 : byte, b_3 : byte, b_4 : byte}([ch]) = [b_1 b_2 b_3 b_4] - -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 69632)) + -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 1114112)) -- if (ch!`%`_char.0 = (((((2 ^ 18) * (((b_1!`%`_byte.0 : nat <:> int) - (240 : nat <:> int)) : int <:> nat)) + ((2 ^ 12) * $cont(b_2))) + ((2 ^ 6) * $cont(b_3))) + $cont(b_4))) } @@ -2688,8 +2688,8 @@ syntax instr = -- if (($lsize($lanetype(ishape_2!`%`_ishape.0)) = (2 * $lsize($lanetype(ishape_1!`%`_ishape.0)))) /\ ((2 * $lsize($lanetype(ishape_1!`%`_ishape.0))) <= 32)) | VCVTOP(shape_1 : shape, shape_2 : shape, vcvtop__(shape_2, shape_1)) | VSPLAT(shape) - | VEXTRACT_LANE(shape : shape, `sx?` : sx?, laneidx : laneidx) - -- if ((sx?{sx <- `sx?`} = ?()) <=> ($lanetype(shape) <- [I32_lanetype I64_lanetype F32_lanetype F64_lanetype])) + | VEXTRACT_LANE(shape : shape, `sx?` : sx?, laneidx : laneidx) {numtype : numtype} + -- if ((sx?{sx <- `sx?`} = ?()) <=> ($lanetype(shape) = (numtype : numtype <: lanetype))) | VREPLACE_LANE(shape : shape, laneidx : laneidx) | `REF.I31_NUM`(u31) | `REF.NULL_ADDR` @@ -4924,7 +4924,7 @@ def $R_idot : relaxed2 def $R_iq15mulr : relaxed2 ;; ../../../../specification/wasm-latest/3.0-numerics.relaxed.spectec -def $R_trunc_u : relaxed4 +def $R_trunc_u : relaxed2 ;; ../../../../specification/wasm-latest/3.0-numerics.relaxed.spectec def $R_trunc_s : relaxed2 @@ -5934,12 +5934,6 @@ def $ivdot_(N : N, iN(N)*, iN(N)*) : iN(N)* def $ivdot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_(N, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) -;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec -def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} - -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivextbinop__(shape_1 : shape, shape_2 : shape, def $f_(N : N, iN(N)*, iN(N)*) : iN(N)*, sx : sx, sx : sx, laneidx : laneidx, laneidx : laneidx, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -5955,6 +5949,17 @@ def $ivmul_(N : N, iN(N)*, iN(N)*) : iN(N)* ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivmul_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`} +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} + -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) + +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivrelaxed_dot_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivrelaxed_dot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $relaxed2($R_idot, syntax iN(N)*, $ivdot_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}), $ivdot_sat_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`})) + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__(ishape_1, ishape_2), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -5962,7 +5967,7 @@ def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__ ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_, S_sx, S_sx, `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_sat_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) + def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivrelaxed_dot_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec 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) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index c8ffe3263..30daae604 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -763,6 +763,10 @@ $\boxed{C \vdash {\mathit{parent}} \leq {\mathit{parent}}}$ $\boxed{{\mathit{parent}} ; {\mathit{child}} \hookrightarrow {\mathit{parent}} ; {\mathit{child}}}$ +$\boxed{{\mathit{parent}} \sim {\mathit{child}}}$ + +$\boxed{{\mathit{parent}} \sim_{C} {\mathit{child}}}$ + $$ \begin{array}{@{}c@{}}\displaystyle \frac{ @@ -789,12 +793,28 @@ $$ \end{array} $$ +$$ +\begin{array}[t]{@{}lrcl@{}l@{}} +{[\textsc{\scriptsize Rsim}]} \quad & \mathsf{aa} & \sim & \mathsf{bbb} \\ +\end{array} +$$ + +$$ +\begin{array}[t]{@{}lrcl@{}l@{}} +{[\textsc{\scriptsize Rsimsub}]} \quad & \mathsf{aa} & {\sim}_{C} {} & \mathsf{bbb} \\ +\end{array} +$$ + $\boxed{C \vdash {\mathit{parent}} : \mathsf{ok}}$ $\boxed{C \vdash {\mathit{parent}} \leq {\mathit{parent}}}$ $\boxed{{\mathit{parent}} ; {\mathit{child}} \hookrightarrow {\mathit{parent}} ; {\mathit{child}}}$ +$\boxed{{\mathit{parent}} \sim {\mathit{child}}}$ + +$\boxed{{\mathit{parent}} \sim_{C} {\mathit{child}}}$ + $$ \begin{array}{@{}c@{}}\displaystyle \frac{ @@ -821,12 +841,28 @@ $$ \end{array} $$ +$$ +\begin{array}[t]{@{}lrcl@{}l@{}} +{[\textsc{\scriptsize Rsim\_macro}]} \quad & \mathsf{aa} & \sim & \mathsf{bbb} \\ +\end{array} +$$ + +$$ +\begin{array}[t]{@{}lrcl@{}l@{}} +{[\textsc{\scriptsize Rsimsub\_macro}]} \quad & \mathsf{aa} & {\sim}_{C} {} & \mathsf{bbb} \\ +\end{array} +$$ + $\boxed{C \vdash {\mathit{parent}} : \mathsf{ok}}$ $\boxed{C \vdash {\mathit{parent}} \leq {\mathit{parent}}}$ $\boxed{{\mathit{parent}} ; {\mathit{child}} \hookrightarrow {\mathit{parent}} ; {\mathit{child}}}$ +$\boxed{{\mathit{parent}} \sim {\mathit{child}}}$ + +$\boxed{{\mathit{parent}} \sim_{C} {\mathit{child}}}$ + $$ \begin{array}{@{}c@{}}\displaystyle \frac{ @@ -853,6 +889,18 @@ $$ \end{array} $$ +$$ +\begin{array}[t]{@{}lrcl@{}l@{}} +{[\textsc{\scriptsize Rsim\_nomacro}]} \quad & \mathsf{aa} & \sim & \mathsf{bbb} \\ +\end{array} +$$ + +$$ +\begin{array}[t]{@{}lrcl@{}l@{}} +{[\textsc{\scriptsize Rsimsub\_nomacro}]} \quad & \mathsf{aa} & {\sim}_{C} {} & \mathsf{bbb} \\ +\end{array} +$$ + \vspace{1ex} \vspace{1ex} @@ -1938,6 +1986,10 @@ $\boxed{{\C} \vdash {\parent} \leq {\parent}}$ $\boxed{{\parent} ; {\child} \hookrightarrow {\parent} ; {\child}}$ +$\boxed{{\parent} \sim {\child}}$ + +$\boxed{{\parent} \sim_{{\C}} {\child}}$ + $$ \begin{array}{@{}c@{}}\displaystyle \frac{ @@ -1964,12 +2016,28 @@ $$ \end{array} $$ +$$ +\begin{array}[t]{@{}lrcl@{}l@{}} +{[\textsc{\scriptsize Rsim}]} \quad & \AA & \sim & \BBB \\ +\end{array} +$$ + +$$ +\begin{array}[t]{@{}lrcl@{}l@{}} +{[\textsc{\scriptsize Rsimsub}]} \quad & \AA & {\sim}_{{\C}} {} & \BBB \\ +\end{array} +$$ + $\boxed{{\C} \vdashok {\parent} : \OKok}$ $\boxed{{\C} \vdashsub {\parent} \subsub {\parent}}$ $\boxed{{\parent} ; {\child} \sqarroweval {\parent} ; {\child}}$ +$\boxed{{\parent} \simsim {\child}}$ + +$\boxed{{\parent} \simsim_{{\C}} {\child}}$ + $$ \begin{array}{@{}c@{}}\displaystyle \frac{ @@ -1996,12 +2064,28 @@ $$ \end{array} $$ +$$ +\begin{array}[t]{@{}lrcl@{}l@{}} +{[\textsc{\scriptsize Rsim\_macro}]} \quad & \AA & \simsim & \BBB \\ +\end{array} +$$ + +$$ +\begin{array}[t]{@{}lrcl@{}l@{}} +{[\textsc{\scriptsize Rsimsub\_macro}]} \quad & \AA & {\simsim}_{{\C}} {} & \BBB \\ +\end{array} +$$ + $\boxed{{\C} \vdash {\parent} : \mathsf{ok}}$ $\boxed{{\C} \vdash {\parent} \leq {\parent}}$ $\boxed{{\parent} ; {\child} \hookrightarrow {\parent} ; {\child}}$ +$\boxed{{\parent} \sim {\child}}$ + +$\boxed{{\parent} \sim_{{\C}} {\child}}$ + $$ \begin{array}{@{}c@{}}\displaystyle \frac{ @@ -2028,6 +2112,18 @@ $$ \end{array} $$ +$$ +\begin{array}[t]{@{}lrcl@{}l@{}} +{[\textsc{\scriptsize Rsim\_nomacro}]} \quad & \AA & \sim & \BBB \\ +\end{array} +$$ + +$$ +\begin{array}[t]{@{}lrcl@{}l@{}} +{[\textsc{\scriptsize Rsimsub\_nomacro}]} \quad & \AA & {\sim}_{{\C}} {} & \BBB \\ +\end{array} +$$ + \vspace{1ex} \vspace{1ex} @@ -4003,7 +4099,7 @@ $$ & & | & {{\mathit{ishape}}_1{.}\mathsf{narrow}}{\mathsf{\_}}{{\mathit{ishape}}_2}{\mathsf{\_}}{{\mathit{sx}}} & \quad \mbox{if}~ {|{\mathrm{lanetype}}({\mathit{ishape}}_2)|} = 2 \cdot {|{\mathrm{lanetype}}({\mathit{ishape}}_1)|} \leq \mathsf{{\scriptstyle 32}} \\ & & | & {\mathit{shape}}_1 {.} {{{\mathit{vcvtop}}}_{{\mathit{shape}}_2, {\mathit{shape}}_1}}{\mathsf{\_}}{{\mathit{shape}}_2} \\ & & | & {\mathit{shape}}{.}\mathsf{splat} \\ -& & | & {{\mathit{shape}}{.}\mathsf{extract\_lane}}{\mathsf{\_}}{{{\mathit{sx}}^?}}~{\mathit{laneidx}} & \quad \mbox{if}~ {{\mathit{sx}}^?} = \epsilon \Leftrightarrow {\mathrm{lanetype}}({\mathit{shape}}) \in \mathsf{i{\scriptstyle 32}}~\mathsf{i{\scriptstyle 64}}~\mathsf{f{\scriptstyle 32}}~\mathsf{f{\scriptstyle 64}} \\ +& & | & {{\mathit{shape}}{.}\mathsf{extract\_lane}}{\mathsf{\_}}{{{\mathit{sx}}^?}}~{\mathit{laneidx}} & \quad \mbox{if}~ {{\mathit{sx}}^?} = \epsilon \Leftrightarrow {\mathrm{lanetype}}({\mathit{shape}}) = {\mathit{numtype}} \\ & & | & {\mathit{shape}}{.}\mathsf{replace\_lane}~{\mathit{laneidx}} \\ & & | & \dots \\ \end{array} @@ -8873,6 +8969,12 @@ $$ \end{array} $$ +$$ +\begin{array}[t]{@{}lcl@{}l@{}} +{{\mathrm{ivrelaxed\_dot}}}_{N}({i_1^\ast}, {i_2^\ast}) & = & {{\mathrm{relaxed}}({\mathrm{R}}_{\mathit{idot}})}{{}[ {{\mathrm{ivdot}}}_{N}({i_1^\ast}, {i_2^\ast}), {{\mathrm{ivdot\_sat}}}_{N}({i_1^\ast}, {i_2^\ast}) ]} \\ +\end{array} +$$ + $$ \begin{array}[t]{@{}lcl@{}l@{}} {{\mathsf{extadd\_pairwise}}{\mathsf{\_}}{{\mathit{sx}}}}{{}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}(v_1)} & = & & \\ @@ -8901,7 +9003,7 @@ $$ {{\mathsf{relaxed\_dot}}{\mathsf{\_}}{\mathsf{s}}}{{}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}(v_1, v_2)} & = & & \\ \multicolumn{4}{@{}l@{}}{\quad \begin{array}[t]{@{}l@{}} -{{\mathrm{ivextbinop}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}({\mathrm{ivdot}}_{{\mathit{sat}}}, \mathsf{s}, {{\mathrm{relaxed}}({\mathrm{R}}_{\mathit{idot}})}{{}[ \mathsf{s}, \mathsf{u} ]}, 0, M_1, v_1, v_2) \\ +{{\mathrm{ivextbinop}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}({\mathrm{ivrelaxed}}_{{\mathit{dot}}}, \mathsf{s}, {{\mathrm{relaxed}}({\mathrm{R}}_{\mathit{idot}})}{{}[ \mathsf{s}, \mathsf{u} ]}, 0, M_1, v_1, v_2) \\ \end{array} } \\ \end{array} @@ -11467,7 +11569,7 @@ $$ \end{array} \\ {\mathrm{utf{\kern-0.1em\scriptstyle 8}}}({\mathit{ch}}) & = & b_1~b_2~b_3~b_4 & \quad \begin{array}[t]{@{}l@{}} -\mbox{if}~ \mathrm{U{+}10000} \leq {\mathit{ch}} < \mathrm{U{+}11000} \\ +\mbox{if}~ \mathrm{U{+}10000} \leq {\mathit{ch}} < \mathrm{U{+}110000} \\ {\land}~ {\mathit{ch}} = {2^{18}} \cdot (b_1 - \mathtt{0xF0}) + {2^{12}} \cdot {\mathrm{cont}}(b_2) + {2^{6}} \cdot {\mathrm{cont}}(b_3) + {\mathrm{cont}}(b_4) \\ \end{array} \\ \end{array} diff --git a/spectec/test-latex/test.spectec b/spectec/test-latex/test.spectec index a5e323673..c1bd04f8e 100644 --- a/spectec/test-latex/test.spectec +++ b/spectec/test-latex/test.spectec @@ -597,26 +597,38 @@ syntax C = {} relation Rok: C |- parent : OK relation Rsub: C |- parent <: parent relation Reval: parent; child ~> parent; child hint(tabular) +relation Rsim: parent ~ child hint(tabular) +relation Rsimsub: parent ~_C child hint(tabular) rule Rok: C |- AA : OK rule Rsub: C |- parent <: AA rule Reval: parent; child ~> AA; BB +rule Rsim: AA ~ BB +rule Rsimsub: AA ~_C BB relation Rok_macro: C |- parent : OK hint(macro "%ok") relation Rsub_macro: C |- parent <: parent hint(macro "%sub") relation Reval_macro: parent; child ~> parent; child hint(macro "%eval") hint(tabular) +relation Rsim_macro: parent ~ child hint(macro "%sim") hint(tabular) +relation Rsimsub_macro: parent ~_C child hint(macro "%sim_") hint(tabular) rule Rok_macro: C |- AA : OK rule Rsub_macro: C |- parent <: AA rule Reval_macro: parent; child ~> AA; BB +rule Rsim_macro: AA ~ BB +rule Rsimsub_macro: AA ~_C BB relation Rok_nomacro: C |- parent : OK hint(macro none) relation Rsub_nomacro: C |- parent <: parent hint(macro none) relation Reval_nomacro: parent; child ~> parent; child hint(macro none) hint(tabular) +relation Rsim_nomacro: parent ~ child hint(macro none) hint(tabular) +relation Rsimsub_nomacro: parent ~_C child hint(macro none) hint(tabular) rule Rok_nomacro: C |- AA : OK rule Rsub_nomacro: C |- parent <: AA rule Reval_nomacro: parent; child ~> AA; BB +rule Rsim_nomacro: AA ~ BB +rule Rsimsub_nomacro: AA ~_C BB ;; diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 88ff0f196..a636e157c 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -324,7 +324,7 @@ def $utf8(char*) : byte* -- if (ch!`%`_char.0 = ((((2 ^ 12) * (((b_1!`%`_byte.0 : nat <:> int) - (224 : nat <:> int)) : int <:> nat)) + ((2 ^ 6) * $cont(b_2))) + $cont(b_3))) ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec:62.1-64.82 def $utf8{ch : char, b_1 : byte, b_2 : byte, b_3 : byte, b_4 : byte}([ch]) = [b_1 b_2 b_3 b_4] - -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 69632)) + -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 1114112)) -- if (ch!`%`_char.0 = (((((2 ^ 18) * (((b_1!`%`_byte.0 : nat <:> int) - (240 : nat <:> int)) : int <:> nat)) + ((2 ^ 12) * $cont(b_2))) + ((2 ^ 6) * $cont(b_3))) + $cont(b_4))) } @@ -2161,8 +2161,8 @@ syntax instr = -- if (($lsize($lanetype(ishape_2!`%`_ishape.0)) = (2 * $lsize($lanetype(ishape_1!`%`_ishape.0)))) /\ ((2 * $lsize($lanetype(ishape_1!`%`_ishape.0))) <= 32)) | VCVTOP(shape_1 : shape, shape_2 : shape, vcvtop__(shape_2, shape_1)) | VSPLAT(shape) - | VEXTRACT_LANE(shape : shape, `sx?` : sx?, laneidx : laneidx) - -- if ((sx?{sx <- `sx?`} = ?()) <=> ($lanetype(shape) <- [I32_lanetype I64_lanetype F32_lanetype F64_lanetype])) + | VEXTRACT_LANE(shape : shape, `sx?` : sx?, laneidx : laneidx) {numtype : numtype} + -- if ((sx?{sx <- `sx?`} = ?()) <=> ($lanetype(shape) = (numtype : numtype <: lanetype))) | VREPLACE_LANE(shape : shape, laneidx : laneidx) | `REF.I31_NUM`(u31) | `REF.NULL_ADDR` @@ -4370,7 +4370,7 @@ def $R_idot : relaxed2 def $R_iq15mulr : relaxed2 ;; ../../../../specification/wasm-latest/3.0-numerics.relaxed.spectec -def $R_trunc_u : relaxed4 +def $R_trunc_u : relaxed2 ;; ../../../../specification/wasm-latest/3.0-numerics.relaxed.spectec def $R_trunc_s : relaxed2 @@ -5380,12 +5380,6 @@ def $ivdot_(N : N, iN(N)*, iN(N)*) : iN(N)* def $ivdot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_(N, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) -;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec -def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} - -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivextbinop__(shape_1 : shape, shape_2 : shape, def $f_(N : N, iN(N)*, iN(N)*) : iN(N)*, sx : sx, sx : sx, laneidx : laneidx, laneidx : laneidx, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -5401,6 +5395,17 @@ def $ivmul_(N : N, iN(N)*, iN(N)*) : iN(N)* ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivmul_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`} +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} + -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) + +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivrelaxed_dot_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivrelaxed_dot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $relaxed2($R_idot, syntax iN(N)*, $ivdot_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}), $ivdot_sat_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`})) + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__(ishape_1, ishape_2), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -5408,7 +5413,7 @@ def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__ ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_, S_sx, S_sx, `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_sat_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) + def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivrelaxed_dot_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec 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) @@ -12226,7 +12231,7 @@ def $utf8(char*) : byte* -- if (ch!`%`_char.0 = ((((2 ^ 12) * (((b_1!`%`_byte.0 : nat <:> int) - (224 : nat <:> int)) : int <:> nat)) + ((2 ^ 6) * $cont(b_2))) + $cont(b_3))) ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec:62.1-64.82 def $utf8{ch : char, b_1 : byte, b_2 : byte, b_3 : byte, b_4 : byte}([ch]) = [b_1 b_2 b_3 b_4] - -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 69632)) + -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 1114112)) -- if (ch!`%`_char.0 = (((((2 ^ 18) * (((b_1!`%`_byte.0 : nat <:> int) - (240 : nat <:> int)) : int <:> nat)) + ((2 ^ 12) * $cont(b_2))) + ((2 ^ 6) * $cont(b_3))) + $cont(b_4))) } @@ -14070,8 +14075,8 @@ syntax instr = -- if (($lsize($lanetype(ishape_2!`%`_ishape.0)) = (2 * $lsize($lanetype(ishape_1!`%`_ishape.0)))) /\ ((2 * $lsize($lanetype(ishape_1!`%`_ishape.0))) <= 32)) | VCVTOP(shape_1 : shape, shape_2 : shape, vcvtop__(shape_2, shape_1)) | VSPLAT(shape) - | VEXTRACT_LANE(shape : shape, `sx?` : sx?, laneidx : laneidx) - -- if ((sx?{sx <- `sx?`} = ?()) <=> ($lanetype(shape) <- [I32_lanetype I64_lanetype F32_lanetype F64_lanetype])) + | VEXTRACT_LANE(shape : shape, `sx?` : sx?, laneidx : laneidx) {numtype : numtype} + -- if ((sx?{sx <- `sx?`} = ?()) <=> ($lanetype(shape) = (numtype : numtype <: lanetype))) | VREPLACE_LANE(shape : shape, laneidx : laneidx) | `REF.I31_NUM`(u31) | `REF.NULL_ADDR` @@ -16279,7 +16284,7 @@ def $R_idot : relaxed2 def $R_iq15mulr : relaxed2 ;; ../../../../specification/wasm-latest/3.0-numerics.relaxed.spectec -def $R_trunc_u : relaxed4 +def $R_trunc_u : relaxed2 ;; ../../../../specification/wasm-latest/3.0-numerics.relaxed.spectec def $R_trunc_s : relaxed2 @@ -17289,12 +17294,6 @@ def $ivdot_(N : N, iN(N)*, iN(N)*) : iN(N)* def $ivdot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_(N, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) -;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec -def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} - -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivextbinop__(shape_1 : shape, shape_2 : shape, def $f_(N : N, iN(N)*, iN(N)*) : iN(N)*, sx : sx, sx : sx, laneidx : laneidx, laneidx : laneidx, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -17310,6 +17309,17 @@ def $ivmul_(N : N, iN(N)*, iN(N)*) : iN(N)* ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivmul_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`} +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} + -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) + +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivrelaxed_dot_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivrelaxed_dot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $relaxed2($R_idot, syntax iN(N)*, $ivdot_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}), $ivdot_sat_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`})) + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__(ishape_1, ishape_2), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -17317,7 +17327,7 @@ def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__ ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_, S_sx, S_sx, `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_sat_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) + def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivrelaxed_dot_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec 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) @@ -24137,7 +24147,7 @@ def $utf8(char*) : byte* -- if (ch!`%`_char.0 = ((((2 ^ 12) * (((b_1!`%`_byte.0 : nat <:> int) - (224 : nat <:> int)) : int <:> nat)) + ((2 ^ 6) * $cont(b_2))) + $cont(b_3))) ;; ../../../../specification/wasm-latest/5.1-binary.values.spectec:62.1-64.82 def $utf8{ch : char, b_1 : byte, b_2 : byte, b_3 : byte, b_4 : byte}([ch]) = [b_1 b_2 b_3 b_4] - -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 69632)) + -- if ((65536 <= ch!`%`_char.0) /\ (ch!`%`_char.0 < 1114112)) -- if (ch!`%`_char.0 = (((((2 ^ 18) * (((b_1!`%`_byte.0 : nat <:> int) - (240 : nat <:> int)) : int <:> nat)) + ((2 ^ 12) * $cont(b_2))) + ((2 ^ 6) * $cont(b_3))) + $cont(b_4))) } @@ -25981,8 +25991,8 @@ syntax instr = -- if (($lsize($lanetype(ishape_2!`%`_ishape.0)) = (2 * $lsize($lanetype(ishape_1!`%`_ishape.0)))) /\ ((2 * $lsize($lanetype(ishape_1!`%`_ishape.0))) <= 32)) | VCVTOP(shape_1 : shape, shape_2 : shape, vcvtop__(shape_2, shape_1)) | VSPLAT(shape) - | VEXTRACT_LANE(shape : shape, `sx?` : sx?, laneidx : laneidx) - -- if ((sx?{sx <- `sx?`} = ?()) <=> ($lanetype(shape) <- [I32_lanetype I64_lanetype F32_lanetype F64_lanetype])) + | VEXTRACT_LANE(shape : shape, `sx?` : sx?, laneidx : laneidx) {numtype : numtype} + -- if ((sx?{sx <- `sx?`} = ?()) <=> ($lanetype(shape) = (numtype : numtype <: lanetype))) | VREPLACE_LANE(shape : shape, laneidx : laneidx) | `REF.I31_NUM`(u31) | `REF.NULL_ADDR` @@ -28317,7 +28327,7 @@ def $R_idot : relaxed2 def $R_iq15mulr : relaxed2 ;; ../../../../specification/wasm-latest/3.0-numerics.relaxed.spectec -def $R_trunc_u : relaxed4 +def $R_trunc_u : relaxed2 ;; ../../../../specification/wasm-latest/3.0-numerics.relaxed.spectec def $R_trunc_s : relaxed2 @@ -29327,12 +29337,6 @@ def $ivdot_(N : N, iN(N)*, iN(N)*) : iN(N)* def $ivdot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_(N, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) -;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec -def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} - -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) - ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivextbinop__(shape_1 : shape, shape_2 : shape, def $f_(N : N, iN(N)*, iN(N)*) : iN(N)*, sx : sx, sx : sx, laneidx : laneidx, laneidx : laneidx, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -29348,6 +29352,17 @@ def $ivmul_(N : N, iN(N)*, iN(N)*) : iN(N)* ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $ivmul_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`} +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivdot_sat_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivdot_sat_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*, `j_1*` : iN(N)*, `j_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $iadd_sat_(N, S_sx, j_1, j_2)*{j_1 <- `j_1*`, j_2 <- `j_2*`} + -- if ($concat_(syntax iN(N), [j_1 j_2]*{j_1 <- `j_1*`, j_2 <- `j_2*`}) = $imul_(N, i_1, i_2)*{i_1 <- `i_1*`, i_2 <- `i_2*`}) + +;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec +def $ivrelaxed_dot_(N : N, iN(N)*, iN(N)*) : iN(N)* + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec + def $ivrelaxed_dot_{N : N, `i_1*` : iN(N)*, `i_2*` : iN(N)*}(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}) = $relaxed2($R_idot, syntax iN(N)*, $ivdot_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`}), $ivdot_sat_(N, i_1*{i_1 <- `i_1*`}, i_2*{i_2 <- `i_2*`})) + ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__(ishape_1, ishape_2), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec @@ -29355,7 +29370,7 @@ def $vextbinop__(ishape_1 : ishape, ishape_2 : ishape, vextbinop__ : vextbinop__ ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_, S_sx, S_sx, `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec - def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivdot_sat_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) + def $vextbinop__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%`_ishape(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1),), `%`_ishape(`%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2),), RELAXED_DOTS_vextbinop__, v_1, v_2) = $ivextbinop__(`%X%`_shape((Jnn_1 : Jnn <: lanetype), M_1), `%X%`_shape((Jnn_2 : Jnn <: lanetype), M_2), def $ivrelaxed_dot_, S_sx, $relaxed2($R_idot, syntax sx, S_sx, U_sx), `%`_laneidx(0,), `%`_laneidx(M_1!`%`_M.0,), v_1, v_2) ;; ../../../../specification/wasm-latest/3.2-numerics.vector.spectec 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) diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index ff6159818..c7eec9f7d 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -26188,15 +26188,6 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i #. Return :math:`{{{\mathrm{iadd}}}_{N}(j_1, j_2)^\ast}`. -:math:`{{\mathrm{ivdot\_sat}}}_{N}({i_1^\ast}, {i_2^\ast})` -........................................................... - - -1. Let :math:`{j_1~j_2^\ast}` be the result for which the :ref:`concatenation ` of :math:`{j_1~j_2^\ast}` is :math:`{{{\mathrm{imul}}}_{N}(i_1, i_2)^\ast}`. - -#. Return :math:`{{{\mathrm{iadd\_sat}}}{\mathsf{s}}{{}_{N}(j_1, j_2)}^\ast}`. - - :math:`{{\mathrm{ivextbinop}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}({\mathrm{f}}, {\mathit{sx}}_1, {\mathit{sx}}_2, i, k, v_1, v_2)` ................................................................................................................................................................................ @@ -26233,6 +26224,22 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i 1. Return :math:`{{{\mathrm{imul}}}_{N}(i_1, i_2)^\ast}`. +:math:`{{\mathrm{ivdot\_sat}}}_{N}({i_1^\ast}, {i_2^\ast})` +........................................................... + + +1. Let :math:`{j_1~j_2^\ast}` be the result for which the :ref:`concatenation ` of :math:`{j_1~j_2^\ast}` is :math:`{{{\mathrm{imul}}}_{N}(i_1, i_2)^\ast}`. + +#. Return :math:`{{{\mathrm{iadd\_sat}}}{\mathsf{s}}{{}_{N}(j_1, j_2)}^\ast}`. + + +:math:`{{\mathrm{ivrelaxed\_dot}}}_{N}({i_1^\ast}, {i_2^\ast})` +............................................................... + + +1. Return :math:`{{\mathrm{relaxed}}({\mathrm{R}}_{\mathit{idot}})}{{}[ {{\mathrm{ivdot}}}_{N}({i_1^\ast}, {i_2^\ast}), {{\mathrm{ivdot\_sat}}}_{N}({i_1^\ast}, {i_2^\ast}) ]}`. + + :math:`{{\mathit{vextbinop}}}{{}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}(v_1, v_2)}` ............................................................................................................................. @@ -26249,7 +26256,7 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i #. Assert: Due to validation, :math:`{\mathit{vextbinop}} = `. -#. Return :math:`{{\mathrm{ivextbinop}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}({\mathrm{ivdot}}_{{\mathit{sat}}}, \mathsf{s}, {{\mathrm{relaxed}}({\mathrm{R}}_{\mathit{idot}})}{{}[ \mathsf{s}, \mathsf{u} ]}, 0, M_1, v_1, v_2)`. +#. Return :math:`{{\mathrm{ivextbinop}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}({\mathrm{ivrelaxed}}_{{\mathit{dot}}}, \mathsf{s}, {{\mathrm{relaxed}}({\mathrm{R}}_{\mathit{idot}})}{{}[ \mathsf{s}, \mathsf{u} ]}, 0, M_1, v_1, v_2)`. :math:`{}{{}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}}(c_1, c_2, c_3)}` @@ -33837,10 +33844,6 @@ ivdot_ N i_1* i_2* 1. Let [j_1, j_2]* be $concat__1^-1(`iN(N), $imul_(N, i_1, i_2)*). 2. Return $iadd_(N, j_1, j_2)*. -ivdot_sat_ N i_1* i_2* -1. Let [j_1, j_2]* be $concat__1^-1(`iN(N), $imul_(N, i_1, i_2)*). -2. Return $iadd_sat_(N, S, j_1, j_2)*. - ivextbinop__ Jnn_1 X M_1 Jnn_2 X M_2 $f_ sx_1 sx_2 i k v_1 v_2 1. Let c_1* be $lanes_(Jnn_1 X M_1, v_1)[i : k]. 2. Let c_2* be $lanes_(Jnn_1 X M_1, v_2)[i : k]. @@ -33858,6 +33861,13 @@ ivextbinop__ Jnn_1 X M_1 Jnn_2 X M_2 $f_ sx_1 sx_2 i k v_1 v_2 ivmul_ N i_1* i_2* 1. Return $imul_(N, i_1, i_2)*. +ivdot_sat_ N i_1* i_2* +1. Let [j_1, j_2]* be $concat__1^-1(`iN(N), $imul_(N, i_1, i_2)*). +2. Return $iadd_sat_(N, S, j_1, j_2)*. + +ivrelaxed_dot_ N i_1* i_2* +1. Return $relaxed2($R_idot(), `iN(N)*, $ivdot_(N, i_1*, i_2*), $ivdot_sat_(N, i_1*, i_2*)). + vextbinop__ Jnn_1 X M_1 Jnn_2 X M_2 vextbinop__ v_1 v_2 1. If vextbinop__ is some EXTMUL, then: a. Let (EXTMUL half sx) be vextbinop__. @@ -33865,7 +33875,7 @@ vextbinop__ Jnn_1 X M_1 Jnn_2 X M_2 vextbinop__ v_1 v_2 2. If (vextbinop__ = DOTS), then: a. Return $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivdot_, S, S, 0, M_1, v_1, v_2). 3. Assert: Due to validation, (vextbinop__ = RELAXED_DOTS). -4. Return $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivdot_sat_, S, $relaxed2($R_idot(), `sx, S, U), 0, M_1, v_1, v_2). +4. Return $ivextbinop__(Jnn_1 X M_1, Jnn_2 X M_2, $ivrelaxed_dot_, S, $relaxed2($R_idot(), `sx, S, U), 0, M_1, v_1, v_2). vextternop__ Jnn_1 X M_1 Jnn_2 X M_2 RELAXED_DOT_ADDS c_1 c_2 c_3 1. Let M be (2 * M_2). diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index 05fbca79d..94517f04c 100644 --- a/spectec/test-splice/TEST.md +++ b/spectec/test-splice/TEST.md @@ -1796,6 +1796,7 @@ warning: definition `ivdot_sat_` was never spliced warning: definition `ivextbinop__` was never spliced warning: definition `ivextunop__` was never spliced warning: definition `ivmul_` was never spliced +warning: definition `ivrelaxed_dot_` was never spliced warning: definition `ivrelop_` was never spliced warning: definition `ivrelopsx_` was never spliced warning: definition `ivshiftop_` was never spliced @@ -2662,6 +2663,7 @@ warning: definition prose `ivdot_sat_` was never spliced warning: definition prose `ivextbinop__` was never spliced warning: definition prose `ivextunop__` was never spliced warning: definition prose `ivmul_` was never spliced +warning: definition prose `ivrelaxed_dot_` was never spliced warning: definition prose `ivrelop_` was never spliced warning: definition prose `ivrelopsx_` was never spliced warning: definition prose `ivshiftop_` was never spliced diff --git a/test/core/relaxed-simd/relaxed_dot_product.wast b/test/core/relaxed-simd/relaxed_dot_product.wast index 41dee0afc..b04d1c4bf 100644 --- a/test/core/relaxed-simd/relaxed_dot_product.wast +++ b/test/core/relaxed-simd/relaxed_dot_product.wast @@ -37,6 +37,26 @@ (v128.const i16x8 32512 0 0 0 0 0 0 0) (v128.const i16x8 33024 0 0 0 0 0 0 0))) +;; Repeat 4 corner cases in both 64-bit halves (i16x8 lanes 0..3 and 4..7): +;; lanes 0, 4 (a = -128, b = -128 or 128): +;; signed * signed (wrapping) : -128 * -128 * 2 = 32,768 wrapped to -32,768 +;; signed * unsigned (saturating) : -128 * 128 * 2 = -32,768 saturated to -32,768 +;; lanes 1, 5 (a = -128, b = -127 or 129): +;; signed * signed (wrapping) : -128 * -127 * 2 = 32,512 +;; signed * unsigned (saturating) : -128 * 129 * 2 = -33,024 saturated to -32,768 +;; lanes 2, 6 (a = 127, b = -128 or 128): +;; signed * signed (wrapping) : 127 * -128 * 2 = -32,512 +;; signed * unsigned (saturating) : 127 * 128 * 2 = 32,512 +;; lanes 3, 7 (a = 127, b = -1 or 255): +;; signed * signed (wrapping) : 127 * -1 * 2 = -254 +;; signed * unsigned (saturating) : 127 * 255 * 2 = 64,770 saturated to 32,767 +(assert_return (invoke "i16x8.relaxed_dot_i8x16_i7x16_s" + (v128.const i8x16 -128 -128 -128 -128 127 127 127 127 -128 -128 -128 -128 127 127 127 127) + (v128.const i8x16 -128 -128 -127 -127 -128 -128 -1 -1 -128 -128 -127 -127 -128 -128 -1 -1)) + (either + (v128.const i16x8 -32768 32512 -32512 -254 -32768 32512 -32512 -254) ;; signed * signed, wrapping add (ARM NEON smull + smull2 + addp) + (v128.const i16x8 -32768 -32768 32512 32767 -32768 -32768 32512 32767))) ;; signed * unsigned, saturating add (x86-64 vpmaddubsw) + ;; Simple values to ensure things are functional. (assert_return (invoke "i32x4.relaxed_dot_i8x16_i7x16_add_s" (v128.const i8x16 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)