Merge branch 'upstream'

Author: rossberg

.github/workflows/main.yml

@@ -19,7 +19,11 @@ jobs:
         with:
           ocaml-compiler: 4.12.x
       - run: opam install --yes ocamlbuild.0.14.0
-      - run: cd interpreter && opam exec make all
+      - name: Setup Node.js
+        uses: actions/setup-node@v1
+        with:
+          node-version: 19.x
+      - run: cd interpreter && opam exec make JS=node all
 
   ref-interpreter-js-library:
     runs-on: ubuntu-latest
@@ -60,6 +64,9 @@ jobs:
       - uses: actions/checkout@v2
         with:
           submodules: "recursive"
+      - uses: actions/setup-node@v3
+        with:
+          node-version: 16
       - run: pip install bikeshed && bikeshed update
       - run: pip install six
       - run: sudo apt-get update -y && sudo apt-get install -y latexmk texlive-latex-recommended texlive-latex-extra texlive-fonts-recommended

document/core/appendix/gen-index-instructions.py

@@ -427,10 +427,10 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\V128.\LOAD\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{55}', r'[\I32~\V128] \to [\V128]', r'valid-load-lane', r'exec-load-lane'),
     Instruction(r'\V128.\LOAD\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{56}', r'[\I32~\V128] \to [\V128]', r'valid-load-lane', r'exec-load-lane'),
     Instruction(r'\V128.\LOAD\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{57}', r'[\I32~\V128] \to [\V128]', r'valid-load-lane', r'exec-load-lane'),
-    Instruction(r'\V128.\STORE\K{8\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{58}', r'[\I32~\V128] \to [\V128]', r'valid-store-lane', r'exec-store-lane'),
-    Instruction(r'\V128.\STORE\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{59}', r'[\I32~\V128] \to [\V128]', r'valid-store-lane', r'exec-store-lane'),
-    Instruction(r'\V128.\STORE\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5A}', r'[\I32~\V128] \to [\V128]', r'valid-store-lane', r'exec-store-lane'),
-    Instruction(r'\V128.\STORE\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5B}', r'[\I32~\V128] \to [\V128]', r'valid-store-lane', r'exec-store-lane'),
+    Instruction(r'\V128.\STORE\K{8\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{58}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'),
+    Instruction(r'\V128.\STORE\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{59}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'),
+    Instruction(r'\V128.\STORE\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5A}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'),
+    Instruction(r'\V128.\STORE\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5B}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'),
     Instruction(r'\V128.\LOAD\K{32\_zero}~\memarg~\laneidx', r'\hex{FD}~~\hex{5C}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'),
     Instruction(r'\V128.\LOAD\K{64\_zero}~\memarg~\laneidx', r'\hex{FD}~~\hex{5D}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'),
     Instruction(r'\F32X4.\VDEMOTE\K{\_f64x2\_zero}', r'\hex{FD}~~\hex{5E}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-demote'),

document/core/appendix/index-instructions.rst

@@ -367,10 +367,10 @@ Instruction                                        Binary Opcode
 :math:`\V128.\LOAD\K{16\_lane}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{55}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-load-lane>`             :ref:`execution <exec-load-lane>`                                 
 :math:`\V128.\LOAD\K{32\_lane}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{56}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-load-lane>`             :ref:`execution <exec-load-lane>`                                 
 :math:`\V128.\LOAD\K{64\_lane}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{57}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-load-lane>`             :ref:`execution <exec-load-lane>`                                 
-:math:`\V128.\STORE\K{8\_lane}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{58}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-store-lane>`            :ref:`execution <exec-store-lane>`                                
-:math:`\V128.\STORE\K{16\_lane}~\memarg~\laneidx`  :math:`\hex{FD}~~\hex{59}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-store-lane>`            :ref:`execution <exec-store-lane>`                                
-:math:`\V128.\STORE\K{32\_lane}~\memarg~\laneidx`  :math:`\hex{FD}~~\hex{5A}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-store-lane>`            :ref:`execution <exec-store-lane>`                                
-:math:`\V128.\STORE\K{64\_lane}~\memarg~\laneidx`  :math:`\hex{FD}~~\hex{5B}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-store-lane>`            :ref:`execution <exec-store-lane>`                                
+:math:`\V128.\STORE\K{8\_lane}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{58}`            :math:`[\I32~\V128] \to []`                    :ref:`validation <valid-store-lane>`            :ref:`execution <exec-store-lane>`                                
+:math:`\V128.\STORE\K{16\_lane}~\memarg~\laneidx`  :math:`\hex{FD}~~\hex{59}`            :math:`[\I32~\V128] \to []`                    :ref:`validation <valid-store-lane>`            :ref:`execution <exec-store-lane>`                                
+:math:`\V128.\STORE\K{32\_lane}~\memarg~\laneidx`  :math:`\hex{FD}~~\hex{5A}`            :math:`[\I32~\V128] \to []`                    :ref:`validation <valid-store-lane>`            :ref:`execution <exec-store-lane>`                                
+:math:`\V128.\STORE\K{64\_lane}~\memarg~\laneidx`  :math:`\hex{FD}~~\hex{5B}`            :math:`[\I32~\V128] \to []`                    :ref:`validation <valid-store-lane>`            :ref:`execution <exec-store-lane>`                                
 :math:`\V128.\LOAD\K{32\_zero}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{5C}`            :math:`[\I32] \to [\V128]`                     :ref:`validation <valid-load-zero>`             :ref:`execution <exec-load-zero>`                                 
 :math:`\V128.\LOAD\K{64\_zero}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{5D}`            :math:`[\I32] \to [\V128]`                     :ref:`validation <valid-load-zero>`             :ref:`execution <exec-load-zero>`                                 
 :math:`\F32X4.\VDEMOTE\K{\_f64x2\_zero}`           :math:`\hex{FD}~~\hex{5E}`            :math:`[\V128] \to [\V128]`                    :ref:`validation <valid-vcvtop>`                :ref:`execution <exec-vcvtop>`, :ref:`operator <op-demote>`       

document/core/conf.py

@@ -297,7 +297,8 @@
   'pointsize': '10pt',
 
    # Additional stuff for the LaTeX preamble.
-   'preamble': '',
+   # Don't type-set cross references with emphasis.
+   'preamble': '\\renewcommand\\sphinxcrossref[1]{#1}\n',
 
    # Latex figure (float) alignment
   'figure_align': 'htbp',

document/core/exec/instructions.rst

@@ -1312,7 +1312,7 @@ Table Instructions
      \end{array}
    \\[1ex]
    \begin{array}{lcl@{\qquad}l}
-   S; F; (\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\I32.\CONST~\signed_{32}^{-1}(-1))
+   S; F; \val~(\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\I32.\CONST~\signed_{32}^{-1}(-1))
    \end{array}
    \end{array}
 
@@ -2244,7 +2244,7 @@ Memory Instructions
    S; F; (\I32.\CONST~d)~\val~(\I32.\CONST~n)~\MEMORYFILL
      \quad\stepto\quad S; F; \TRAP
      \\ \qquad
-     (\iff d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA|)
+     (\iff d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA|)
    \\[1ex]
    S; F; (\I32.\CONST~d)~\val~(\I32.\CONST~0)~\MEMORYFILL
      \quad\stepto\quad S; F; \epsilon
@@ -2451,7 +2451,7 @@ Memory Instructions
      \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
      (\iff & s + n > |S.\SDATAS[F.\AMODULE.\MIDATAS[x]].\DIDATA| \\
-      \vee & d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA|) \\[1ex]
+      \vee & d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA|) \\[1ex]
      \end{array}
    \\[1ex]
    S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\MEMORYINIT~x)
@@ -2938,22 +2938,20 @@ Exiting :math:`\instr^\ast` with label :math:`L`
 
 When the end of a block is reached without a jump or trap aborting it, then the following steps are performed.
 
-1. Let :math:`n` be the number of values on the top of the stack.
-
-2. Pop the values :math:`\val^n` from the stack.
+1. Pop all values :math:`\val^\ast` from the top of the stack.
 
-3. Assert: due to :ref:`validation <valid-instr-seq>`, the label :math:`L` is now on the top of the stack and has arity :math:`n`.
+2. Assert: due to :ref:`validation <valid-instr-seq>`, the label :math:`L` is now on the top of the stack.
 
-4. Pop the label from the stack.
+3. Pop the label from the stack.
 
-5. Push :math:`\val^n` back to the stack.
+4. Push :math:`\val^\ast` back to the stack.
 
-6. Jump to the position after the |END| of the :ref:`structured control instruction <syntax-instr-control>` associated with the label :math:`L`.
+5. Jump to the position after the |END| of the :ref:`structured control instruction <syntax-instr-control>` associated with the label :math:`L`.
 
 .. math::
    ~\\[-1ex]
    \begin{array}{lcl@{\qquad}l}
-   \LABEL_n\{\instr^\ast\}~\val^n~\END &\stepto& \val^n
+   \LABEL_n\{\instr^\ast\}~\val^\ast~\END &\stepto& \val^\ast
    \end{array}
 
 .. note::

document/core/exec/modules.rst

@@ -449,8 +449,7 @@ and list of :ref:`reference <syntax-ref>` vectors for the module's :ref:`element
 
    a. Let :math:`\limits_i~t_i` be the :ref:`table type <syntax-tabletype>` :math:`\table_i.\TTYPE`.
 
-   b. Let :math:`\tableaddr_i` be the :ref:`table address <syntax-tableaddr>` resulting from :ref:`allocating <alloc-table>` :math:`\table_i.\TTYPE`
-   with initialization value :math:`\REFNULL~t_i`.
+   b. Let :math:`\tableaddr_i` be the :ref:`table address <syntax-tableaddr>` resulting from :ref:`allocating <alloc-table>` :math:`\table_i.\TTYPE` with initialization value :math:`\REFNULL~t_i`.
 
 4. For each :ref:`memory <syntax-mem>` :math:`\mem_i` in :math:`\module.\MMEMS`, do:
 

document/core/static/custom.css

@@ -44,6 +44,8 @@ div.admonition p.admonition-title {
 div.math {
   background-color: #F0F0F0;
   padding: 3px 0 3px 0;
+  overflow-x: auto;
+  overflow-y: hidden;
 }
 
 div.relations {

document/core/syntax/conventions.rst

@@ -20,7 +20,7 @@ Grammar Notation
 
 The following conventions are adopted in defining grammar rules for abstract syntax.
 
-* Terminal symbols (atoms) are written in sans-serif font: :math:`\K{i32}, \K{end}`.
+* Terminal symbols (atoms) are written in sans-serif font or in symbolic form: :math:`\K{i32}, \K{end}, {\to}, [, ]`.
 
 * Nonterminal symbols are written in italic font: :math:`\X{valtype}, \X{instr}`.
 

document/core/syntax/values.rst

@@ -140,6 +140,8 @@ An *arithmetic NaN*  is a floating-point value :math:`\pm\NAN(n)` with :math:`n
 .. note::
    In the abstract syntax, subnormals are distinguished by the leading 0 of the significand. The exponent of subnormals has the same value as the smallest possible exponent of a normal number. Only in the :ref:`binary representation <binary-float>` the exponent of a subnormal is encoded differently than the exponent of any normal number.
 
+   The notion of canonical NaN defined here is unrelated to the notion of canonical NaN that the |IEEE754|_ standard (Section 3.5.2) defines for decimal interchange formats.
+
 Conventions
 ...........
 

document/core/text/instructions.rst

@@ -173,7 +173,7 @@ Reference Instructions
    \production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|&
      \text{ref.null}~~t{:}\Theaptype &\Rightarrow& \REFNULL~t \\ &&|&
      \text{ref.is\_null} &\Rightarrow& \REFISNULL \\ &&|&
-     \text{ref.func}~~x{:}\Tfuncidx &\Rightarrow& \REFFUNC~x \\ &&|&
+     \text{ref.func}~~x{:}\Tfuncidx &\Rightarrow& \REFFUNC~x \\
    \end{array}
 
 
@@ -899,7 +899,7 @@ Vector constant instructions have a mandatory :ref:`shape <syntax-vec-shape>` de
      \text{f64x2.convert\_low\_i32x4\_s} &\Rightarrow& \F64X2.\VCONVERT\K{\_low\_i32x4\_s}\\  &&|&
      \text{f64x2.convert\_low\_i32x4\_u} &\Rightarrow& \F64X2.\VCONVERT\K{\_low\_i32x4\_u}\\ &&|&
      \text{f32x4.demote\_f64x2\_zero} &\Rightarrow& \F32X4.\VDEMOTE\K{\_f64x2\_zero}\\ &&|&
-     \text{f64x2.promote\_low\_f32x4} &\Rightarrow& \F64X2.\VPROMOTE\K{\_low\_f32x4}\\ &&|&
+     \text{f64x2.promote\_low\_f32x4} &\Rightarrow& \F64X2.\VPROMOTE\K{\_low\_f32x4}\\
    \end{array}