Merge branch 'upstream'

WebAssembly · Jul 3, 2024 · f3a075c · f3a075c
2 parents d6ea0c9 + d73ac32
commit f3a075c
Show file tree

Hide file tree

Showing 18 changed files with 289 additions and 161 deletions.
diff --git a/.github/workflows/mirror-to-master.yml b/.github/workflows/mirror-to-master.yml
diff --git a/.github/workflows/w3c-publish.yml b/.github/workflows/w3c-publish.yml
@@ -10,6 +10,7 @@ on:
 
 jobs:
   publish-to-w3c-TR:
+    if: github.repository == 'WebAssembly/spec'
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repo

diff --git a/document/core/Makefile b/document/core/Makefile
@@ -80,7 +80,7 @@ publish-main: clean main bikeshed-keep deploy
 all:	pdf html bikeshed
 
 .PHONY: main
-main:	pdf html
+main:	macrosok pdf html
 
 # Dirty hack to avoid rebuilding the Bikeshed version for every push.
 .PHONY: bikeshed-keep
@@ -97,6 +97,10 @@ GENERATED = appendix/index-instructions.rst
 %.rst: %.py
 	(cd `dirname $@`; ./`basename $^`)
 
+.PHONY: macrosok
+macrosok:	$(GENERATED)
+	sh util/check_macros.sh
+
 .PHONY: pdf
 pdf:	$(GENERATED) latexpdf
 	mkdir -p $(BUILDDIR)/html/$(DOWNLOADDIR)

diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst
@@ -360,7 +360,7 @@ It decodes into a vector of :ref:`element segments <syntax-elem>` that represent
 
 .. note::
    The initial integer can be interpreted as a bitfield.
-   Bit 0 indicates a passive or declarative segment,
+   Bit 0 distinguishes a passive or declarative segment from an active segment,
    bit 1 indicates the presence of an explicit table index for an active segment and otherwise distinguishes passive from declarative segments,
    bit 2 indicates the use of element type and element :ref:`expressions <binary-expr>` instead of element kind and element indices.
 

diff --git a/document/core/text/lexical.rst b/document/core/text/lexical.rst
@@ -71,8 +71,9 @@ Any token that does not fall into any of the other categories is considered *res
 
 .. index:: ! white space, character, ASCII
    single: text format; white space
-.. _text-format:
 .. _text-space:
+.. _text-format:
+.. _text-newline:
 
 White Space
 ~~~~~~~~~~~

diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst
@@ -569,7 +569,7 @@ As another abbreviation, element segments may also be specified inline with :ref
    single: data; segment
 .. _text-datastring:
 .. _text-data:
-.. _test-memuse:
+.. _text-memuse:
 
 Data Segments
 ~~~~~~~~~~~~~

diff --git a/document/core/util/check_macros.sh b/document/core/util/check_macros.sh
@@ -0,0 +1,32 @@
+#!/bin/sh
+
+cd `dirname $0`/..
+
+FILES=`ls */*.rst`
+ERRORS=0
+
+for XREF in `grep xref util/macros.def`; do
+  if echo $XREF | grep -q "[|]"; then
+    MACRO=`echo $XREF | sed 's/^[^|]*[|]//g' | sed 's/[|].*$//g'`
+  elif echo $XREF | grep -q xref; then
+    FILE=`echo $XREF | sed 's/^.*xref{//g' | sed 's/}.*$//g'`.rst
+    LABEL=`echo $XREF | sed 's/^[^}]*}{//g' | sed 's/}.*$//g'`
+    TARGET=".. _$LABEL:"
+    if ! [ -f $FILE ] || ! grep -q "$TARGET" $FILE; then
+      ERRORS=1
+      echo Undefined cross-reference $FILE:$LABEL in macro "|$MACRO|"
+      if ! [ -f $FILE ]; then
+        echo ...non-existent file $FILE
+      fi
+      if grep -q "$TARGET" $FILES; then
+        echo ...defined in `grep -l "$TARGET" $FILES`
+      fi
+    fi
+  fi
+done
+
+if [ $ERRORS -eq 0 ]; then
+  echo All cross-references okay.
+else
+  exit 1;
+fi
diff --git a/document/core/util/macros.def b/document/core/util/macros.def
@@ -177,8 +177,6 @@
 
 .. |to| mathdef:: \xref{syntax/types}{syntax-functype}{\rightarrow}
 
-.. |I8| mathdef:: \xref{exec/runtime}{syntax-storagetype}{\K{i8}}
-.. |I16| mathdef:: \xref{exec/runtime}{syntax-storagetype}{\K{i16}}
 .. |I32| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{i32}}
 .. |I64| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{i64}}
 .. |F32| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f32}}
@@ -227,8 +225,8 @@
 
 .. |externtype| mathdef:: \xref{syntax/types}{syntax-externtype}{\X{externtype}}
 
-.. |stacktype| mathdef:: \xref{syntax/types}{syntax-stacktype}{\X{stacktype}}
-.. |opdtype| mathdef:: \xref{syntax/types}{syntax-opdtype}{\X{opdtype}}
+.. |stacktype| mathdef:: \xref{valid/instructions}{syntax-stacktype}{\X{stacktype}}
+.. |opdtype| mathdef:: \xref{valid/instructions}{syntax-opdtype}{\X{opdtype}}
 
 
 .. Types, meta functions
@@ -523,9 +521,7 @@
 .. |vunop| mathdef:: \xref{syntax/instructions}{syntax-vunop}{\X{vunop}}
 .. |vbinop| mathdef:: \xref{syntax/instructions}{syntax-vbinop}{\X{vbinop}}
 .. |vrelop| mathdef:: \xref{syntax/instructions}{syntax-vrelop}{\X{vrelop}}
-.. |vternop| mathdef:: \xref{syntax/instructions}{syntax-vternop}{\X{vternop}}
 .. |vcvtop| mathdef:: \xref{syntax/instructions}{syntax-vcvtop}{\X{vcvtop}}
-.. |vextmul| mathdef:: \xref{syntax/instructions}{syntax-vextmul}{\X{vextmul}}
 
 .. |laneidx| mathdef:: \xref{syntax/instructions}{syntax-laneidx}{\X{laneidx}}
 .. |vvunop| mathdef:: \xref{syntax/instructions}{syntax-vvunop}{\X{vvunop}}
@@ -801,19 +797,10 @@
 .. |Tlocalidx| mathdef:: \xref{text/modules}{text-localidx}{\T{localidx}}
 .. |Tlabelidx| mathdef:: \xref{text/modules}{text-labelidx}{\T{labelidx}}
 
-.. |Ttypebind| mathdef:: \xref{text/modules}{text-typebind}{\T{typebind}}
-.. |Tfuncbind| mathdef:: \xref{text/modules}{text-funcbind}{\T{funcbind}}
-.. |Ttablebind| mathdef:: \xref{text/modules}{text-tablebind}{\T{tablebind}}
-.. |Tmembind| mathdef:: \xref{text/modules}{text-membind}{\T{membind}}
-.. |Tglobalbind| mathdef:: \xref{text/modules}{text-globalbind}{\T{globalbind}}
-.. |Tlocalbind| mathdef:: \xref{text/modules}{text-localbind}{\T{localbind}}
-.. |Tlabelbind| mathdef:: \xref{text/modules}{text-labelbind}{\T{labelbind}}
-
 
 .. Modules, non-terminals
 
 .. |Tmodule| mathdef:: \xref{text/modules}{text-module}{\T{module}}
-.. |Tmodulebody| mathdef:: \xref{text/modules}{text-modulebody}{\T{modulebody}}
 .. |Tmodulefield| mathdef:: \xref{text/modules}{text-modulefield}{\T{modulefield}}
 .. |Ttype| mathdef:: \xref{text/modules}{text-typedef}{\T{type}}
 .. |Ttypeuse| mathdef:: \xref{text/modules}{text-typeuse}{\T{typeuse}}
@@ -829,7 +816,6 @@
 .. |Telemlist| mathdef:: \xref{text/modules}{text-elemlist}{\T{elemlist}}
 .. |Telemexpr| mathdef:: \xref{text/modules}{text-elemexpr}{\T{elemexpr}}
 .. |Ttableuse| mathdef:: \xref{text/modules}{text-tableuse}{\T{tableuse}}
-.. |Tcode| mathdef:: \xref{text/modules}{text-code}{\T{code}}
 .. |Tlocal| mathdef:: \xref{text/modules}{text-local}{\T{local}}
 .. |Tlocals| mathdef:: \xref{text/modules}{text-local}{\T{locals}}
 .. |Tdata| mathdef:: \xref{text/modules}{text-data}{\T{data}}
@@ -944,10 +930,10 @@
 
 .. Notation
 
-.. |stepto| mathdef:: \xref{exec/conventions}{formal-notation}{\hookrightarrow}
+.. |stepto| mathdef:: \xref{exec/conventions}{exec-notation}{\hookrightarrow}
 .. |extendsto| mathdef:: \xref{appendix/properties}{extend}{\preceq}
-.. |matchesexterntype| mathdef:: \xref{exec/modules}{match-externtype}{\leq}
-.. |matcheslimits| mathdef:: \xref{exec/modules}{match-limits}{\leq}
+.. |matchesexterntype| mathdef:: \xref{valid/types}{match-externtype}{\leq}
+.. |matcheslimits| mathdef:: \xref{valid/types}{match-limits}{\leq}
 
 
 .. Allocation
@@ -1085,7 +1071,7 @@
 .. Values & Results, non-terminals
 
 .. |num| mathdef:: \xref{exec/runtime}{syntax-num}{\X{num}}
-.. |vecc| mathdef:: \xref{exec/runtime}{syntax-vec}{\X{vec}}
+.. |vecc| mathdef:: \xref{exec/runtime}{syntax-vecc}{\X{vec}}
 .. |reff| mathdef:: \xref{exec/runtime}{syntax-ref}{\X{ref}}
 .. |val| mathdef:: \xref{exec/runtime}{syntax-val}{\X{val}}
 .. |result| mathdef:: \xref{exec/runtime}{syntax-result}{\X{result}}
@@ -1148,10 +1134,10 @@
 .. |imins| mathdef:: \xref{exec/numerics}{op-imin_s}{\F{imin\_s}}
 .. |imaxu| mathdef:: \xref{exec/numerics}{op-imax_u}{\F{imax\_u}}
 .. |imaxs| mathdef:: \xref{exec/numerics}{op-imax_s}{\F{imax\_s}}
-.. |iaddsatu| mathdef:: \xref{exec/numerics}{op-iaddsat_u}{\F{iaddsat\_u}}
-.. |iaddsats| mathdef:: \xref{exec/numerics}{op-iaddsat_s}{\F{iaddsat\_s}}
-.. |isubsatu| mathdef:: \xref{exec/numerics}{op-isubsat_u}{\F{isubsat\_u}}
-.. |isubsats| mathdef:: \xref{exec/numerics}{op-isubsat_s}{\F{isubsat\_s}}
+.. |iaddsatu| mathdef:: \xref{exec/numerics}{op-iadd_sat_u}{\F{iadd\_sat\_u}}
+.. |iaddsats| mathdef:: \xref{exec/numerics}{op-iadd_sat_s}{\F{iadd\_sat\_s}}
+.. |isubsatu| mathdef:: \xref{exec/numerics}{op-isub_sat_u}{\F{isub\_sat\_u}}
+.. |isubsats| mathdef:: \xref{exec/numerics}{op-isub_sat_s}{\F{isub\_sat\_s}}
 .. |iavgru| mathdef:: \xref{exec/numerics}{op-iavgr_u}{\F{iavgr\_u}}
 .. |iq15mulrsats| mathdef:: \xref{exec/numerics}{op-iq15mulrsat_s}{\F{iq15mulrsat\_s}}
 
@@ -1227,8 +1213,8 @@
 
 .. |vdashexternval| mathdef:: \xref{exec/modules}{valid-externval}{\vdash}
 
-.. |vdashlimitsmatch| mathdef:: \xref{exec/modules}{match-limits}{\vdash}
-.. |vdashexterntypematch| mathdef:: \xref{exec/modules}{match-externtype}{\vdash}
+.. |vdashlimitsmatch| mathdef:: \xref{valid/types}{match-limits}{\vdash}
+.. |vdashexterntypematch| mathdef:: \xref{valid/types}{match-externtype}{\vdash}
 
 
 .. Soundness
@@ -1238,7 +1224,7 @@
 
 .. |vdashadmininstr| mathdef:: \xref{appendix/properties}{valid-instr-admin}{\vdash}
 
-.. |vdashval| mathdef:: \xref{appendix/properties}{valid-val}{\vdash}
+.. |vdashval| mathdef:: \xref{exec/modules}{valid-val}{\vdash}
 .. |vdashresult| mathdef:: \xref{appendix/properties}{valid-result}{\vdash}
 
 .. |vdashfuncinst| mathdef:: \xref{appendix/properties}{valid-funcinst}{\vdash}

diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst
@@ -1098,7 +1098,7 @@ Memory Instructions
      \qquad
      C.\CMEMS[0] = \memtype
      \qquad
-     2^{\memarg.\ALIGN} < N/8
+     2^{\memarg.\ALIGN} \leq N/8
    }{
      C \vdashinstr \K{v128.}\LOAD{N}\K{\_lane}~\memarg~\laneidx : [\I32~\V128] \to [\V128]
    }
@@ -1122,7 +1122,7 @@ Memory Instructions
      \qquad
      C.\CMEMS[0] = \memtype
      \qquad
-     2^{\memarg.\ALIGN} < N/8
+     2^{\memarg.\ALIGN} \leq N/8
    }{
      C \vdashinstr \K{v128.}\STORE{N}\K{\_lane}~\memarg~\laneidx : [\I32~\V128] \to []
    }

diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst
@@ -536,22 +536,27 @@ Instead, the context :math:`C` for validation of the module's content is constru
 
   * :math:`C.\CREFS` is the set :math:`\freefuncidx(\module \with \MFUNCS = \epsilon \with \MSTART = \epsilon)`, i.e., the set of :ref:`function indices <syntax-funcidx>` occurring in the module, except in its :ref:`functions <syntax-func>` or :ref:`start function <syntax-start>`.
 
-* Let :math:`C'` be the :ref:`context <context>` where:
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, except that :math:`C'.\CGLOBALS` is just the sequence :math:`\etglobals(\X{it}^\ast)`.
 
-  * :math:`C'.\CGLOBALS` is the sequence :math:`\etglobals(\X{it}^\ast)`,
+* For each :math:`\functype_i` in :math:`\module.\MTYPES`,
+  the :ref:`function type <syntax-functype>` :math:`\functype_i` must be :ref:`valid <valid-functype>`.
 
-  * :math:`C'.\CFUNCS` is the same as :math:`C.\CFUNCS`,
+* Under the context :math:`C'`:
 
-  * :math:`C'.\CTABLES` is the same as :math:`C.\CTABLES`,
+  * For each :math:`\table_i` in :math:`\module.\MTABLES`,
+    the definition :math:`\table_i` must be :ref:`valid <valid-table>` with a :ref:`table type <syntax-tabletype>` :math:`\X{tt}_i`.
 
-  * :math:`C'.\CMEMS` is the same as :math:`C.\CMEMS`,
+  * For each :math:`\mem_i` in :math:`\module.\MMEMS`,
+    the definition :math:`\mem_i` must be :ref:`valid <valid-mem>` with a :ref:`memory type <syntax-memtype>` :math:`\X{mt}_i`.
 
-  * :math:`C'.\CREFS` is the same as :math:`C.\CREFS`,
+  * For each :math:`\global_i` in :math:`\module.\MGLOBALS`,
+    the definition :math:`\global_i` must be :ref:`valid <valid-global>` with a :ref:`global type <syntax-globaltype>` :math:`\X{gt}_i`.
 
-  * all other fields are empty.
+  * For each :math:`\elem_i` in :math:`\module.\MELEMS`,
+    the segment :math:`\elem_i` must be :ref:`valid <valid-elem>` with :ref:`reference type <syntax-reftype>` :math:`\X{rt}_i`.
 
-* For each :math:`\functype_i` in :math:`\module.\MTYPES`,
-  the :ref:`function type <syntax-functype>` :math:`\functype_i` must be :ref:`valid <valid-functype>`.
+  * For each :math:`\data_i` in :math:`\module.\MDATAS`,
+    the segment :math:`\data_i` must be :ref:`valid <valid-data>`.
 
 * Under the context :math:`C`:
 
@@ -567,23 +572,6 @@ Instead, the context :math:`C` for validation of the module's content is constru
   * For each :math:`\export_i` in :math:`\module.\MEXPORTS`,
     the segment :math:`\export_i` must be :ref:`valid <valid-export>` with :ref:`external type <syntax-externtype>` :math:`\X{et}_i`.
 
-* Under the context :math:`C'`:
-
-  * For each :math:`\table_i` in :math:`\module.\MTABLES`,
-    the definition :math:`\table_i` must be :ref:`valid <valid-table>` with a :ref:`table type <syntax-tabletype>` :math:`\X{tt}_i`.
-
-  * For each :math:`\mem_i` in :math:`\module.\MMEMS`,
-    the definition :math:`\mem_i` must be :ref:`valid <valid-mem>` with a :ref:`memory type <syntax-memtype>` :math:`\X{mt}_i`.
-
-  * For each :math:`\global_i` in :math:`\module.\MGLOBALS`,
-    the definition :math:`\global_i` must be :ref:`valid <valid-global>` with a :ref:`global type <syntax-globaltype>` :math:`\X{gt}_i`.
-
-  * For each :math:`\elem_i` in :math:`\module.\MELEMS`,
-    the segment :math:`\elem_i` must be :ref:`valid <valid-elem>` with :ref:`reference type <syntax-reftype>` :math:`\X{rt}_i`.
-
-  * For each :math:`\data_i` in :math:`\module.\MDATAS`,
-    the segment :math:`\data_i` must be :ref:`valid <valid-data>`.
-
 * The length of :math:`C.\CMEMS` must not be larger than :math:`1`.
 
 * All export names :math:`\export_i.\ENAME` must be different.
@@ -639,7 +627,7 @@ Instead, the context :math:`C` for validation of the module's content is constru
      \\
      C = \{ \CTYPES~\type^\ast, \CFUNCS~\X{ift}^\ast\,\X{ft}^\ast, \CTABLES~\X{itt}^\ast\,\X{tt}^\ast, \CMEMS~\X{imt}^\ast\,\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast\,\X{gt}^\ast, \CELEMS~\X{rt}^\ast, \CDATAS~{\ok}^n, \CREFS~x^\ast \}
      \\
-     C' = \{ \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CTABLES~(C.\CTABLES), \CMEMS~(C.\CMEMS), \CREFS~(C.\CREFS) \}
+     C' = C \with \CGLOBALS = \X{igt}^\ast
      \qquad
      |C.\CMEMS| \leq 1
      \qquad

diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml
@@ -220,7 +220,7 @@ let zero s = expect 0x00 s "zero byte expected"
 
 let memop s =
   let align = u32 s in
-  require (I32.le_u align 32l) s (pos s - 1) "malformed memop flags";
+  require (I32.lt_u align 32l) s (pos s - 1) "malformed memop flags";
   let offset = u32 s in
   Int32.to_int align, offset