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

Author: backes

.github/workflows/ci-interpreter.yml

@@ -27,7 +27,7 @@ jobs:
       - name: Setup Node.js
         uses: actions/setup-node@v2
         with:
-          node-version: 19.x
+          node-version: 20.x
       - name: Build interpreter
         run: cd interpreter && opam exec make
       - name: Run tests

document/core/appendix/changes.rst

@@ -518,6 +518,48 @@ Added managed reference types. [#proposal-gc]_
   - |EXTERNCONVERTANY|
 
 
+.. index:: instruction, vector instruction, SIMD
+
+Relaxed Vector Instructions
+...........................
+
+Added new *relaxed* vector instructions,
+whose behaviour is non-deterministic and implementation-dependent. [#proposal-relaxed]_
+
+* New binary :ref:`vector instruction <syntax-instr-relaxed>`:
+
+  - :math:`\K{f}\!N\!\K{x}\!M\!\K{.relaxed\_min}`
+  - :math:`\K{f}\!N\!\K{x}\!M\!\K{.relaxed\_max}`
+  - :math:`\K{i16x8.relaxed\_q15mulr\_s}`
+  - :math:`\K{i16x8.relaxed\_dot\_i8x16\_i7x16\_s}`
+
+* New ternary :ref:`vector instruction <syntax-instr-relaxed>`:
+
+  - :math:`\K{f}\!N\!\K{x}\!M\!\K{.relaxed\_madd}`
+  - :math:`\K{f}\!N\!\K{x}\!M\!\K{.relaxed\_nmadd}`
+  - :math:`\K{i}\!N\!\K{x}\!M\!\K{.relaxed\_laneselect}`
+  - :math:`\K{i32x4.relaxed\_dot\_i8x16\_i7x16\_add\_s}`
+
+* New conversion :ref:`vector instructions <syntax-instr-relaxed>`:
+
+  - :math:`\K{i32x4.relaxed\_trunc\_f32x4\_}\sx`
+  - :math:`\K{i32x4.relaxed\_trunc\_f64x2\_}\sx\K{\_zero}`
+
+* New byte reordering :ref:`vector instruction <syntax-instr-relaxed>`:
+
+  - :math:`\K{i8x16.relaxed\_swizzle}`
+
+
+.. index:: determinism, non-determinism, profiles
+
+Profiles
+........
+
+Introduced the concept of :ref:`profile <profiles>` for specifying language subsets.
+
+* A new profile defining a :ref:`deterministic <profile-deterministic>` mode of execution.
+
+
 .. index:: text format, annotation, custom section, identifier, module, type, function, local, structure field
 
 Custom Annotations
@@ -542,7 +584,7 @@ mirroring the role of custom sections in the binary format. [#proposal-annot]_
 
 
 .. [#proposal-extconst]
-   https://github.com/WebAssembly/extended-const/blob/main/proposals/extended-const/
+   https://github.com/WebAssembly/spec/blob/main/proposals/extended-const/
 
 .. [#proposal-tailcall]
    https://github.com/WebAssembly/spec/tree/main/proposals/tail-call/
@@ -551,13 +593,16 @@ mirroring the role of custom sections in the binary format. [#proposal-annot]_
    https://github.com/WebAssembly/spec/tree/main/proposals/exception-handling/
 
 .. [#proposal-multimem]
-   https://github.com/WebAssembly/multi-memory/blob/main/proposals/multi-memory/
+   https://github.com/WebAssembly/spec/blob/main/proposals/multi-memory/
 
 .. [#proposal-typedref]
    https://github.com/WebAssembly/spec/tree/main/proposals/function-references/
 
 .. [#proposal-gc]
    https://github.com/WebAssembly/spec/tree/main/proposals/gc/
 
+.. [#proposal-relaxed]
+   https://github.com/WebAssembly/spec/tree/main/proposals/relaxed-simd/
+
 .. [#proposal-annot]
    https://github.com/WebAssembly/annotations/tree/main/proposals/annotations/

document/core/appendix/index-instructions.py

@@ -633,7 +633,26 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\I32X4.\VTRUNC\K{\_sat\_f64x2\_u\_zero}', r'\hex{FD}~~\hex{FD}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-trunc_sat_u'),
     Instruction(r'\F64X2.\VCONVERT\K{\_low\_i32x4\_s}', r'\hex{FD}~~\hex{FE}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-convert_s'),
     Instruction(r'\F64X2.\VCONVERT\K{\_low\_i32x4\_u}', r'\hex{FD}~~\hex{FF}~~\hex{01}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-convert_u'),
-    Instruction(None, r'\hex{FD}~\hex{00}~\hex{02} \dots'),
+    Instruction(r'\I8X16.\RELAXEDSWIZZLE', r'\hex{FD}~~\hex{80}~~\hex{02}', r'[\V128~\V128] \to [\V128]', r'valid-relaxed_swizzle', r'exec-relaxed_swizzle', r'op-irelaxed_swizzle'),
+    Instruction(r'\I32X4.\RELAXEDTRUNC\K{\_f32x4\_s}', r'\hex{FD}~~\hex{81}~~\hex{02}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-relaxed_trunc_s'),
+    Instruction(r'\I32X4.\RELAXEDTRUNC\K{\_f32x4\_u}', r'\hex{FD}~~\hex{82}~~\hex{02}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-relaxed_trunc_u'),
+    Instruction(r'\I32X4.\RELAXEDTRUNC\K{\_f64x2\_s}', r'\hex{FD}~~\hex{83}~~\hex{02}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-relaxed_trunc_s'),
+    Instruction(r'\I32X4.\RELAXEDTRUNC\K{\_f64x2\_u}', r'\hex{FD}~~\hex{84}~~\hex{02}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-relaxed_trunc_u'),
+    Instruction(r'\F32X4.\RELAXEDMADD', r'\hex{FD}~~\hex{85}~~\hex{02}', r'[\V128~\V128~\V128] \to [\V128]', r'valid-vternop', r'exec-vternop', r'op-frelaxed_madd'),
+    Instruction(r'\F32X4.\RELAXEDNMADD', r'\hex{FD}~~\hex{86}~~\hex{02}', r'[\V128~\V128~\V128] \to [\V128]', r'valid-vternop', r'exec-vternop', r'op-frelaxed_nmadd'),
+    Instruction(r'\F64X2.\RELAXEDMADD', r'\hex{FD}~~\hex{87}~~\hex{02}', r'[\V128~\V128~\V128] \to [\V128]', r'valid-vternop', r'exec-vternop', r'op-frelaxed_madd'),
+    Instruction(r'\F64X2.\RELAXEDNMADD', r'\hex{FD}~~\hex{88}~~\hex{02}', r'[\V128~\V128~\V128] \to [\V128]', r'valid-vternop', r'exec-vternop', r'op-frelaxed_nmadd'),
+    Instruction(r'\I8X16.\RELAXEDLANESELECT', r'\hex{FD}~~\hex{89}~~\hex{02}', r'[\V128~\V128~\V128] \to [\V128]', r'valid-relaxed_laneselect', r'exec-relaxed_laneselect', r'op-irelaxed_laneselect'),
+    Instruction(r'\I16X8.\RELAXEDLANESELECT', r'\hex{FD}~~\hex{8A}~~\hex{02}', r'[\V128~\V128~\V128] \to [\V128]', r'valid-relaxed_laneselect', r'exec-relaxed_laneselect', r'op-irelaxed_laneselect'),
+    Instruction(r'\I32X4.\RELAXEDLANESELECT', r'\hex{FD}~~\hex{8B}~~\hex{02}', r'[\V128~\V128~\V128] \to [\V128]', r'valid-relaxed_laneselect', r'exec-relaxed_laneselect', r'op-irelaxed_laneselect'),
+    Instruction(r'\I64X2.\RELAXEDLANESELECT', r'\hex{FD}~~\hex{8C}~~\hex{02}', r'[\V128~\V128~\V128] \to [\V128]', r'valid-relaxed_laneselect', r'exec-relaxed_laneselect', r'op-irelaxed_laneselect'),
+    Instruction(r'\F32X4.\RELAXEDMIN', r'\hex{FD}~~\hex{8D}~~\hex{02}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-frelaxed_min'),
+    Instruction(r'\F32X4.\RELAXEDMAX', r'\hex{FD}~~\hex{8E}~~\hex{02}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-frelaxed_max'),
+    Instruction(r'\F64X2.\RELAXEDMIN', r'\hex{FD}~~\hex{8F}~~\hex{02}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-frelaxed_min'),
+    Instruction(r'\F64X2.\RELAXEDMAX', r'\hex{FD}~~\hex{90}~~\hex{02}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-frelaxed_max'),
+    Instruction(r'\I16X8.\RELAXEDQ15MULRS', r'\hex{FD}~~\hex{91}~~\hex{02}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-irelaxed_q15mulr_s'),
+    Instruction(r'\I16X8.\RELAXEDDOT\K{\_i8x16\_i7x16\_s}', r'\hex{FD}~~\hex{92}~~\hex{02}', r'[\V128~\V128] \to [\V128]', r'valid-relaxed_dot', r'exec-relaxed_dot'),
+    Instruction(r'\I32X4.\RELAXEDDOT\K{\_i8x16\_i7x16\_add\_s}', r'\hex{FD}~~\hex{93}~~\hex{02}', r'[\V128~\V128~\V128] \to [\V128]', r'valid-relaxed_dot', r'exec-relaxed_dot'),
     Instruction(None, r'\hex{FE}'),
     Instruction(None, r'\hex{FF}'),
 ]

document/core/appendix/index.rst

@@ -7,6 +7,7 @@ Appendix
    :maxdepth: 2
 
    embedding
+   profiles
    implementation
    properties
    algorithm

document/core/appendix/profiles.rst

@@ -0,0 +1,131 @@
+.. index:: ! profile, abstract syntax, validation, execution, binary format, text format
+.. _profiles:
+
+Profiles
+--------
+
+To enable the use of WebAssembly in as many environments as possible, *profiles* specify coherent language subsets that fit constraints imposed by common classes of host environments.
+A host platform can thereby decide to support the language only under a restricted profile, or even the intersection of multiple profiles.
+
+
+Conventions
+~~~~~~~~~~~
+
+A profile modification is specified by decorating selected rules in the main body of this specification with a *profile annotation* that defines them as conditional on the choice of profile.
+
+For that purpose, every profile defines a *profile marker*, an alphanumeric short-hand like :math:`\profilename{ABC}`.
+A profile annotation of the form :math:`\exprofiles{\profile{ABC}~\profile{XYZ}}` on a rule indicates that this rule is *excluded* for either of the profiles whose marker is :math:`\profilename{ABC}` or :math:`\profilename{XYZ}`.
+
+There are two ways of subsetting the language in a profile:
+
+* *Syntactic*, by *omitting* a feature, in which case certain constructs are removed from the syntax altogether.
+
+* *Semantic*, by *restricting* a feature, in which case certain constructs are still present but some behaviours are ruled out.
+
+
+Syntax Annotations
+..................
+
+To omit a construct from a profile syntactically, respective productions in the grammar of the :ref:`abstract syntax <syntax>` are annotated with an associated profile marker.
+This is defined to have the following implications:
+
+1. Any production in the :ref:`binary <binary>` or :ref:`textual <text>` syntax that produces abstract syntax with a marked construct is omitted by extension.
+
+2. Any :ref:`validation <valid>` or :ref:`execution <exec>` rule that handles a marked construct is omitted by extension.
+
+The overall effect is that the respective construct is no longer part of the language under a respective profile.
+
+.. note::
+   For example, a "busy" profile marked :math:`\profilename{BUSY}` could rule out the |NOP| instruction by marking the production for it in the abstract syntax as follows:
+
+   .. math::
+      \begin{array}{llcl}
+      \production{instruction} & \instr &::=&
+        \dots \\
+      & \exprofiles{\profile{BUSY}} &|& \NOP \\
+      &                           &|& \UNREACHABLE \\
+      \end{array}
+
+   A rule may be annotated by multiple markers, which could be the case if a construct is in the intersection of multiple features.
+
+
+Semantics Annotations
+.....................
+
+To restrict certain behaviours in a profile, individual :ref:`validation <valid>` or :ref:`reduction <exec>` rules or auxiliary definitions are annotated with an associated marker.
+
+This has the consequence that the respective rule is no longer applicable under the given profile.
+
+.. note::
+   For example, an "infinite" profile marked :math:`\profilename{INF}` could define that growing memory never fails:
+
+   .. math::
+	   \begin{array}{llcl@{\qquad}l}
+	   & S; F; (\I32.\CONST~n)~\MEMORYGROW~x &\stepto& S'; F; (\I32.\CONST~\X{sz})
+	   \\&&&
+	     \begin{array}[t]{@{}r@{~}l@{}}
+	     (\iff & F.\AMODULE.\MIMEMS[x] = a \\
+	     \wedge & \X{sz} = |S.\SMEMS[a].\MIDATA|/64\,\F{Ki} \\
+	     \wedge & S' = S \with \SMEMS[a] = \growmem(S.\SMEMS[a], n)) \\[1ex]
+	     \end{array}
+	   \\[1ex]
+	   \exprofiles{\profile{INF}} & S; F; (\I32.\CONST~n)~\MEMORYGROW~x &\stepto& S; F; (\I32.\CONST~\signed_{32}^{-1}(-1))
+	   \end{array}
+
+
+Properties
+..........
+
+All profiles are defined such that the following properties are preserved:
+
+* All profiles represent syntactic and semantic subsets of the :ref:`full profile <profile-full>`, i.e., they do not *add* syntax or *alter* behaviour.
+
+* All profiles are mutually compatible, i.e., no two profiles subset semantic behaviour in inconsistent or ambiguous ways, and any intersection of profiles preserves the properties described here.
+
+* Profiles do not violate :ref:`soundness <soundness>`, i.e., all :ref:`configurations <syntax-config>` valid under that profile still have well-defined execution behaviour.
+
+.. note::
+   Tools are generally expected to handle and produce code for the full profile by default.
+   In particular, producers should not generate code that *depends* on specific profiles. Instead, all code should preserve correctness when executed under the full profile.
+
+   Moreover, profiles should be considered static and fixed for a given platform or ecosystem. Runtime conditioning on the "current" profile is not intended and should be avoided.
+
+
+
+Defined Profiles
+~~~~~~~~~~~~~~~~
+
+.. note::
+   The number of defined profiles is expected to remain small in the future. Profiles are intended for broad and permanent use cases only. In particular, profiles are not intended for language versioning.
+
+
+.. index:: full profile
+   single: profile; full
+.. _profile-full:
+
+Full Profile (:math:`{\small{\mathrm{FUL}}}`)
+.............................................
+
+The *full* profile contains the complete language and all possible behaviours.
+It imposes no restrictions, i.e., all rules and definitions are active.
+All other profiles define sub-languages of this profile.
+
+
+.. index:: determinism, non-determinism, deterministic profile
+   single: profile; deterministic
+.. _profile-deterministic:
+
+Deterministic Profile (:math:`{\small{\mathrm{DET}}}`)
+......................................................
+
+The *deterministic* profile excludes all rules marked :math:`\exprofiles{\PROFDET}`.
+It defines a sub-language that does not exhibit any incidental non-deterministic behaviour:
+
+* All :ref:`NaN <syntax-nan>` values :ref:`generated <aux-nans>` by :ref:`floating-point instructions <syntax-instr-numeric>` are canonical and positive.
+
+* All :ref:`relaxed vector instructions <syntax-instr-relaxed>` have a fixed behaviour that does not depend on the implementation.
+
+Even under this profile, the |MEMORYGROW| and |TABLEGROW| instructions technically remain :ref:`non-deterministic <exec-memory.grow>`, in order to be able to indicate resource exhaustion.
+
+.. note::
+   In future versions of WebAssembly, new non-deterministic behaviour may be added to the language, such that the deterministic profile will induce additional restrictions.

document/core/binary/instructions.rst

@@ -931,6 +931,31 @@ All other vector instructions are plain opcodes without any immediates.
      \hex{FD}~~95{:}\Bu32 &\Rightarrow& \F64X2.\VPROMOTE\K{\_low\_f32x4}\\
    \end{array}
 
+.. math::
+   \begin{array}{llclll}
+   \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{vechaslongerinstructionnames} \\[-2ex] &&|&
+     \hex{FD}~~256{:}\Bu32 &\Rightarrow& \I16X8.\RELAXEDSWIZZLE \\ &&|&
+     \hex{FD}~~257{:}\Bu32 &\Rightarrow& \I32X4.\RELAXEDTRUNC\K{\_f32x4\_s} \\ &&|&
+     \hex{FD}~~258{:}\Bu32 &\Rightarrow& \I32X4.\RELAXEDTRUNC\K{\_f32x4\_u} \\ &&|&
+     \hex{FD}~~259{:}\Bu32 &\Rightarrow& \I32X4.\RELAXEDTRUNC\K{\_f32x4\_s\_zero} \\ &&|&
+     \hex{FD}~~260{:}\Bu32 &\Rightarrow& \I32X4.\RELAXEDTRUNC\K{\_f32x4\_u\_zero} \\ &&|&
+     \hex{FD}~~261{:}\Bu32 &\Rightarrow& \F32X4.\RELAXEDMADD \\ &&|&
+     \hex{FD}~~262{:}\Bu32 &\Rightarrow& \F32X4.\RELAXEDNMADD \\ &&|&
+     \hex{FD}~~263{:}\Bu32 &\Rightarrow& \F64X2.\RELAXEDMADD \\ &&|&
+     \hex{FD}~~264{:}\Bu32 &\Rightarrow& \F64X2.\RELAXEDNMADD \\ &&|&
+     \hex{FD}~~265{:}\Bu32 &\Rightarrow& \I8X16.\RELAXEDLANESELECT \\ &&|&
+     \hex{FD}~~266{:}\Bu32 &\Rightarrow& \I16X8.\RELAXEDLANESELECT \\ &&|&
+     \hex{FD}~~267{:}\Bu32 &\Rightarrow& \I32X4.\RELAXEDLANESELECT \\ &&|&
+     \hex{FD}~~268{:}\Bu32 &\Rightarrow& \I64X2.\RELAXEDLANESELECT \\ &&|&
+     \hex{FD}~~269{:}\Bu32 &\Rightarrow& \F32X4.\RELAXEDMIN \\ &&|&
+     \hex{FD}~~270{:}\Bu32 &\Rightarrow& \F32X4.\RELAXEDMAX \\ &&|&
+     \hex{FD}~~271{:}\Bu32 &\Rightarrow& \F64X2.\RELAXEDMIN \\ &&|&
+     \hex{FD}~~272{:}\Bu32 &\Rightarrow& \F64X2.\RELAXEDMAX \\ &&|&
+     \hex{FD}~~273{:}\Bu32 &\Rightarrow& \I16X8.\RELAXEDQ15MULRS \\ &&|&
+     \hex{FD}~~274{:}\Bu32 &\Rightarrow& \I16X8.\RELAXEDDOT\K{\_i8x16\_i7x16\_s} \\ &&|&
+     \hex{FD}~~275{:}\Bu32 &\Rightarrow& \I16X8.\RELAXEDDOT\K{\_i8x16\_i7x16\_add\_s} \\
+   \end{array}
+
 
 .. index:: expression
    pair: binary format; expression