Merge remote-tracking branch 'gc/main' into wasm-3.0

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)

document/core/appendix/properties.rst

@@ -21,7 +21,7 @@ In order to state and prove soundness precisely, the typing rules must be extend
 
 
 .. index:: context, recursive type, recursive type index
-.. context-rec:
+.. _context-ext:
 
 Contexts
 ~~~~~~~~

document/core/exec/instructions.rst

@@ -1776,7 +1776,7 @@ Most other vector instructions are defined in terms of numeric operators that ar
 :math:`\shape\K{.}\SPLAT`
 .........................
 
-1. Let :math:`t` be the type :math:`\unpacked(\shape)`.
+1. Let :math:`t` be the type :math:`\unpackshape(\shape)`.
 
 2. Assert: due to :ref:`validation <valid-vec-splat>`, a value of :ref:`value type <syntax-valtype>` :math:`t` is on the top of the stack.
 
@@ -1791,7 +1791,7 @@ Most other vector instructions are defined in terms of numeric operators that ar
 .. math::
    \begin{array}{lcl@{\qquad}l}
    (t\K{.}\CONST~c_1)~\shape\K{.}\SPLAT &\stepto& (\V128\K{.}\VCONST~c)
-     & (\iff t = \unpacked(\shape)
+     & (\iff t = \unpackshape(\shape)
        \wedge c = \lanes^{-1}_{\shape}(c_1^{\dim(\shape)}))
      \\
    \end{array}
@@ -1810,7 +1810,7 @@ Most other vector instructions are defined in terms of numeric operators that ar
 
 4. Let :math:`i^\ast` be the result of computing :math:`\lanes_{t_1\K{x}N}(c_1)`.
 
-5. Let :math:`t_2` be the type :math:`\unpacked(t_1\K{x}N)`.
+5. Let :math:`t_2` be the type :math:`\unpackshape(t_1\K{x}N)`.
 
 6. Let :math:`c_2` be the result of computing :math:`\extend^{sx^?}_{t_1,t_2}(i^\ast[x])`.
 
@@ -1823,7 +1823,7 @@ Most other vector instructions are defined in terms of numeric operators that ar
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
-      (\iff & t_2 = \unpacked(t_1\K{x}N) \\
+      (\iff & t_2 = \unpackshape(t_1\K{x}N) \\
        \wedge & c_2 = \extend^{sx^?}_{t_1,t_2}(\lanes_{t_1\K{x}N}(c_1)[x]))
      \end{array}
    \end{array}
@@ -1836,7 +1836,7 @@ Most other vector instructions are defined in terms of numeric operators that ar
 
 1. Assert: due to :ref:`validation <valid-vec-replace_lane>`, :math:`x < \dim(\shape)`.
 
-2. Let :math:`t_2` be the type :math:`\unpacked(\shape)`.
+2. Let :math:`t_2` be the type :math:`\unpackshape(\shape)`.
 
 3. Assert: due to :ref:`validation <valid-vec-replace_lane>`, a value of :ref:`value type <syntax-valtype>` :math:`t_1` is on the top of the stack.
 

document/core/exec/runtime.rst

@@ -506,7 +506,7 @@ Conventions
   .. math::
      \begin{array}{@{}lcl}
      \packval_{\valtype}(\val) &=& \val \\
-     \packval_{\packedtype}(\I32.\CONST~i) &=& \packedtype.\PACK~(\wrap_{32,|\packtype|}(i))
+     \packval_{\packedtype}(\I32.\CONST~i) &=& \packedtype.\PACK~(\wrap_{32,|\packedtype|}(i))
      \end{array}
 
 * The inverse conversion of a :ref:`field value <syntax-fieldval>` to a regular :ref:`value <syntax-val>` is defined as follows:
@@ -622,6 +622,7 @@ Conventions
 .. _syntax-trap:
 .. _syntax-reffuncaddr:
 .. _syntax-invoke:
+.. _syntax-return_invoke:
 .. _syntax-instr-admin:
 
 Administrative Instructions

document/core/syntax/types.rst

@@ -82,6 +82,7 @@ Conventions
 .. _type-concrete:
 .. _syntax-i31:
 .. _syntax-heaptype:
+.. _syntax-absheaptype:
 
 Heap Types
 ~~~~~~~~~~
@@ -290,12 +291,21 @@ Structures are heterogeneous, but require static indexing, while arrays need to
    \end{array}
 
 .. _bitwidth-fieldtype:
+.. _aux-unpacktype:
 
 Conventions
 ...........
 
 * The notation :math:`|t|` for :ref:`bit width <bitwidth-valtype>` extends to packed types as well, that is, :math:`|\I8| = 8` and :math:`|\I16| = 16`.
 
+* The auxiliary function :math:`\unpacktype` maps a storage type to the :ref:`value type <syntax-valtype>` obtained when accessing a field:
+
+  .. math::
+     \begin{array}{lll}
+     \unpacktype(\valtype) &=& \valtype \\
+     \unpacktype(\packedtype) &=& \I32 \\
+     \end{array}
+
 
 .. index:: ! composite type, function type, aggreagate type, structure type, array type
    pair: abstract syntax; composite type

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
 ~~~~~~~~~~~

document/core/text/modules.rst

@@ -573,7 +573,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
 ~~~~~~~~~~~~~

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

document/core/util/macros.def

@@ -101,7 +101,7 @@
 
 .. Notation for Sequences & Records
 
-.. |subst| mathdef:: \xref{syntax/conventions}{notation-subst}{\mathrel{\mathbf{:=}}}
+.. |subst| mathdef:: \xref{valid/conventions}{notation-subst}{\mathrel{\mathbf{:=}}}
 .. |slice| mathdef:: \xref{syntax/conventions}{notation-slice}{\mathrel{\mathbf{:}}}
 .. |with| mathdef:: \xref{syntax/conventions}{notation-replace}{\mathrel{\mbox{with}}}
 .. |concat| mathdef:: \xref{syntax/conventions}{notation-concat}{\F{concat}}
@@ -178,13 +178,13 @@
 .. Types, terminals
 
 .. |toF| mathdef:: \xref{syntax/types}{syntax-functype}{\rightarrow}
-.. |to| mathdef:: \mathrel{\xref{syntax/types}{syntax-instrtype}{\rightarrow}}
+.. |to| mathdef:: \mathrel{\xref{valid/conventions}{syntax-instrtype}{\rightarrow}}
 
 .. |BOTH| mathdef:: \xref{valid/conventions}{syntax-heaptype-ext}{\K{bot}}
 .. |BOT| mathdef:: \xref{valid/conventions}{syntax-valtype-ext}{\K{bot}}
 
-.. |I8| mathdef:: \xref{syntax/runtime}{syntax-storagetype}{\K{i8}}
-.. |I16| mathdef:: \xref{syntax/runtime}{syntax-storagetype}{\K{i16}}
+.. |I8| mathdef:: \xref{syntax/types}{syntax-storagetype}{\K{i8}}
+.. |I16| mathdef:: \xref{syntax/types}{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}}
@@ -235,8 +235,8 @@
 .. |MVAR| mathdef:: \xref{syntax/types}{syntax-mut}{\K{var}}
 .. |MCONST| mathdef:: \xref{syntax/types}{syntax-mut}{\K{const}}
 
-.. |SET| mathdef:: \xref{syntax/types}{syntax-init}{\K{set}}
-.. |UNSET| mathdef:: \xref{syntax/types}{syntax-init}{\K{unset}}
+.. |SET| mathdef:: \xref{valid/conventions}{syntax-init}{\K{set}}
+.. |UNSET| mathdef:: \xref{valid/conventions}{syntax-init}{\K{unset}}
 
 .. |LMIN| mathdef:: \xref{syntax/types}{syntax-limits}{\K{min}}
 .. |LMAX| mathdef:: \xref{syntax/types}{syntax-limits}{\K{max}}
@@ -273,7 +273,7 @@
 
 .. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}}
 .. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mut}}
-.. |init| mathdef:: \xref{syntax/types}{syntax-init}{\X{init}}
+.. |init| mathdef:: \xref{valid/conventions}{syntax-init}{\X{init}}
 
 .. |instrtype| mathdef:: \xref{valid/conventions}{syntax-instrtype}{\X{instrtype}}
 .. |localtype| mathdef:: \xref{valid/conventions}{syntax-localtype}{\X{localtype}}
@@ -291,7 +291,6 @@
 .. |expanddt| mathdef:: \xref{valid/conventions}{aux-expand-deftype}{\F{expand}}
 .. |unrollht| mathdef:: \xref{appendix/properties}{aux-unroll-heaptype}{\F{unroll}}
 
-.. |packtype| mathdef:: \xref{syntax/types}{aux-packtype}{\F{pack}}
 .. |unpacktype| mathdef:: \xref{syntax/types}{aux-unpacktype}{\F{unpack}}
 
 .. |etfuncs| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}}
@@ -496,10 +495,10 @@
 .. |ARRAYGETU| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array.get\_u}}
 .. |ARRAYSET| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array.set}}
 .. |ARRAYLEN| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array.len}}
-.. |ARRAYFILL| mathdef:: \xref{syntax/instructions}{syntax-instr-aray}{\K{array.fill}}
-.. |ARRAYCOPY| mathdef:: \xref{syntax/instructions}{syntax-instr-aray}{\K{array.copy}}
-.. |ARRAYINITDATA| mathdef:: \xref{syntax/instructions}{syntax-instr-aray}{\K{array.init\_data}}
-.. |ARRAYINITELEM| mathdef:: \xref{syntax/instructions}{syntax-instr-aray}{\K{array.init\_elem}}
+.. |ARRAYFILL| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array.fill}}
+.. |ARRAYCOPY| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array.copy}}
+.. |ARRAYINITDATA| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array.init\_data}}
+.. |ARRAYINITELEM| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array.init\_elem}}
 
 .. |REFI31| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{ref.i31}}
 .. |I31GET| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{i31.get}}
@@ -632,9 +631,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}}
@@ -905,7 +902,7 @@
 .. |Tfunctype| mathdef:: \xref{text/types}{text-functype}{\T{functype}}
 .. |Tstructtype| mathdef:: \xref{text/types}{text-structtype}{\T{structtype}}
 .. |Tarraytype| mathdef:: \xref{text/types}{text-arraytype}{\T{arraytype}}
-.. |Taggrtype| mathdef:: \xref{text/types}{text-aggrype}{\T{aggrtype}}
+.. |Taggrtype| mathdef:: \xref{text/types}{text-aggrtype}{\T{aggrtype}}
 .. |Tfieldtype| mathdef:: \xref{text/types}{text-fieldtype}{\T{fieldtype}}
 .. |Tstoragetype| mathdef:: \xref{text/types}{text-storagetype}{\T{storagetype}}
 .. |Tpackedtype| mathdef:: \xref{text/types}{text-packedtype}{\T{packedtype}}
@@ -941,9 +938,8 @@
 .. 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}}
+.. |Ttype| mathdef:: \xref{text/types}{text-typedef}{\T{type}}
 .. |Ttypeuse| mathdef:: \xref{text/modules}{text-typeuse}{\T{typeuse}}
 .. |Tfunc| mathdef:: \xref{text/modules}{text-func}{\T{func}}
 .. |Ttable| mathdef:: \xref{text/modules}{text-table}{\T{table}}
@@ -957,7 +953,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}}
@@ -1043,7 +1038,7 @@
 
 .. Meta functions
 
-.. |clostype| mathdef:: \xref{valid/conventions}{closure}{\K{clos}}
+.. |clostype| mathdef:: \xref{valid/conventions}{aux-clostype}{\K{clos}}
 
 
 .. Contexts
@@ -1059,7 +1054,7 @@
 .. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}}
 .. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}}
 .. |CREFS| mathdef:: \xref{valid/conventions}{context}{\K{refs}}
-.. |CRECS| mathdef:: \xref{valid/matching}{context-rec}{\K{recs}}
+.. |CRECS| mathdef:: \xref{appendix/properties}{context-ext}{\K{recs}}
 
 
 .. Judgments
@@ -1136,7 +1131,7 @@
 .. |vdashimportdesc| mathdef:: \xref{valid/modules}{valid-importdesc}{\vdash}
 .. |vdashmodule| mathdef:: \xref{valid/modules}{valid-module}{\vdash}
 
-.. |unpacked| mathdef:: \xref{valid/instructions}{aux-unpacked}{\F{unpacked}}
+.. |unpackshape| mathdef:: \xref{valid/instructions}{aux-unpackshape}{\F{unpack}}
 .. |dim| mathdef:: \xref{valid/instructions}{aux-dim}{\F{dim}}
 
 
@@ -1145,7 +1140,7 @@
 
 .. Notation
 
-.. |stepto| mathdef:: \xref{exec/conventions}{formal-notation}{\hookrightarrow}
+.. |stepto| mathdef:: \xref{exec/conventions}{exec-notation}{\hookrightarrow}
 .. |extendsto| mathdef:: \xref{appendix/properties}{extend}{\preceq}
 
 
@@ -1183,12 +1178,12 @@
 
 .. Address, meta functions
 
-.. |freefuncaddr| mathdef:: \xref{syntax/modules}{syntax-funcaddr}{\F{funcaddr}}
-.. |freetableaddr| mathdef:: \xref{syntax/modules}{syntax-tableaddr}{\F{tableaddr}}
-.. |freememaddr| mathdef:: \xref{syntax/modules}{syntax-memaddr}{\F{memaddr}}
-.. |freeglobaladdr| mathdef:: \xref{syntax/modules}{syntax-globaladdr}{\F{globaladdr}}
-.. |freeelemaddr| mathdef:: \xref{syntax/modules}{syntax-elemaddr}{\F{elemaddr}}
-.. |freedataaddr| mathdef:: \xref{syntax/modules}{syntax-dataaddr}{\F{dataaddr}}
+.. |freefuncaddr| mathdef:: \xref{exec/runtime}{syntax-funcaddr}{\F{funcaddr}}
+.. |freetableaddr| mathdef:: \xref{exec/runtime}{syntax-tableaddr}{\F{tableaddr}}
+.. |freememaddr| mathdef:: \xref{exec/runtime}{syntax-memaddr}{\F{memaddr}}
+.. |freeglobaladdr| mathdef:: \xref{exec/runtime}{syntax-globaladdr}{\F{globaladdr}}
+.. |freeelemaddr| mathdef:: \xref{exec/runtime}{syntax-elemaddr}{\F{elemaddr}}
+.. |freedataaddr| mathdef:: \xref{exec/runtime}{syntax-dataaddr}{\F{dataaddr}}
 
 
 .. Instances, terminals
@@ -1236,8 +1231,8 @@
 .. |AIFIELDS| mathdef:: \xref{exec/runtime}{syntax-arrayinst}{\K{fields}}
 
 .. |PACK| mathdef:: \xref{exec/runtime}{syntax-packedval}{\K{pack}}
-.. |I8PACK| mathdef:: \xref{exec/runtime}{syntax-packval}{\K{i8.pack}}
-.. |I16PACK| mathdef:: \xref{exec/runtime}{syntax-packval}{\K{i16.pack}}
+.. |I8PACK| mathdef:: \xref{exec/runtime}{syntax-packedval}{\K{i8.pack}}
+.. |I16PACK| mathdef:: \xref{exec/runtime}{syntax-packedval}{\K{i16.pack}}
 
 
 .. Instances, non-terminals
@@ -1322,7 +1317,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}}
@@ -1391,10 +1386,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}}
 
@@ -1478,7 +1473,7 @@
 
 .. |vdashadmininstr| mathdef:: \xref{appendix/properties}{valid-instr-admin}{\vdash}
 
-.. |vdashval| mathdef:: \xref{appendix/properties}{valid-val}{\vdash}
+.. |vdashval| mathdef:: \xref{exec/values}{valid-val}{\vdash}
 .. |vdashresult| mathdef:: \xref{appendix/properties}{valid-result}{\vdash}
 .. |vdashfieldval| mathdef:: \xref{appendix/properties}{valid-fieldval}{\vdash}
 .. |vdashpackedval| mathdef:: \xref{appendix/properties}{valid-packedval}{\vdash}

document/core/valid/conventions.rst

@@ -301,6 +301,7 @@ In addition to field access written :math:`C.\K{field}` the following notation i
 
 .. index:: ! type closure
 .. _type-closure:
+.. _aux-clostype:
 
 Convention
 ..........