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

Author: rossberg

document/core/appendix/embedding.rst

@@ -630,11 +630,12 @@ Globals
    \end{array}
 
 
-.. index:: reference, reference type
+.. index:: reference, reference type, value type, value
 .. _embed-ref-type:
+.. _embed-val-default:
 
-References
-~~~~~~~~~~
+Values
+~~~~~~
 
 :math:`\F{ref\_type}(\store, \reff) : \reftype`
 ...............................................
@@ -656,6 +657,20 @@ References
    In such cases, this function may return a less precise supertype.
 
 
+:math:`\F{val\_default}(\valtype) : \val`
+...............................................
+
+1. If :math:`\default_{valtype}` is not defined, then return :math:`\ERROR`.
+
+1. Else, return the :ref:`value <syntax-val>` :math:`\default_{valtype}`.
+
+.. math::
+   \begin{array}{lclll}
+   \F{val\_default}(t) &=& v && (\iff \default_t = v) \\
+   \F{val\_default}(t) &=& \ERROR && (\iff \default_t = \epsilon) \\
+   \end{array}
+
+
 .. index:: value type, external type, subtyping
 .. _embed-match-valtype:
 .. _embed-match-externtype:
@@ -674,7 +689,7 @@ Matching
 
 .. math::
    \begin{array}{lclll}
-   \F{match\_reftype}(t_1, t_2) &=& \TRUE && (\iff \vdashvaltypematch t_1 \matchesvaltype t_2) \\
+   \F{match\_reftype}(t_1, t_2) &=& \TRUE && (\iff {} \vdashvaltypematch t_1 \matchesvaltype t_2) \\
    \F{match\_reftype}(t_1, t_2) &=& \FALSE && (\otherwise) \\
    \end{array}
 
@@ -690,6 +705,6 @@ Matching
 
 .. math::
    \begin{array}{lclll}
-   \F{match\_externtype}(\X{et}_1, \X{et}_2) &=& \TRUE && (\iff \vdashexterntypematch \X{et}_1 \matchesexterntype \X{et}_2) \\
+   \F{match\_externtype}(\X{et}_1, \X{et}_2) &=& \TRUE && (\iff {} \vdashexterntypematch \X{et}_1 \matchesexterntype \X{et}_2) \\
    \F{match\_externtype}(\X{et}_1, \X{et}_2) &=& \FALSE && (\otherwise) \\
    \end{array}

document/core/appendix/index-instructions.py

@@ -347,7 +347,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\BRONCASTFAIL~t_1~t_2', r'\hex{FB}~\hex{19}', r'[t_1] \to [t_2]', r'valid-br_on_cast_fail', r'exec-br_on_cast_fail'),
     Instruction(r'\ANYCONVERTEXTERN', r'\hex{FB}~\hex{1A}', r'[(\REF~\NULL~\EXTERN)] \to [(\REF~\NULL~\ANY)]', r'valid-any.convert_extern', r'exec-any.convert_extern'),
     Instruction(r'\EXTERNCONVERTANY', r'\hex{FB}~\hex{1B}', r'[(\REF~\NULL~\ANY)] \to [(\REF~\NULL~\EXTERN)]', r'valid-extern.convert_any', r'exec-extern.convert_any'),
-    Instruction(r'\REFI31', r'\hex{FB}~\hex{1C}', r'[\I32] \to [\I31REF]', r'valid-ref.i31', r'exec-ref.i31'),
+    Instruction(r'\REFI31', r'\hex{FB}~\hex{1C}', r'[\I32] \to [(\REF~\I31)]', r'valid-ref.i31', r'exec-ref.i31'),
     Instruction(r'\I31GETS', r'\hex{FB}~\hex{1D}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'),
     Instruction(r'\I31GETU', r'\hex{FB}~\hex{1E}', r'[\I31REF] \to [\I32]', r'valid-i31.get_sx', r'exec-i31.get_sx'),
     Instruction(None, r'\hex{FB}~\hex{1E} \dots'),

document/core/binary/modules.rst

@@ -344,7 +344,7 @@ It decodes into a vector of :ref:`element segments <syntax-elem>` that represent
    \production{element segment} & \Belem &::=&
      0{:}\Bu32~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx)
        &\Rightarrow& \\&&&\quad
-       \{ \ETYPE~(\REF~\NULL~\FUNC), \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
+       \{ \ETYPE~(\REF~\FUNC), \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
      1{:}\Bu32~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx)
        &\Rightarrow& \\&&&\quad
        \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EPASSIVE \} \\ &&|&
@@ -356,7 +356,7 @@ It decodes into a vector of :ref:`element segments <syntax-elem>` that represent
        \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EDECLARATIVE \} \\ &&|&
      4{:}\Bu32~~e{:}\Bexpr~~\X{el}^\ast{:}\Bvec(\Bexpr)
        &\Rightarrow& \\&&&\quad
-       \{ \ETYPE~(\REF~\NULL~\FUNC), \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
+       \{ \ETYPE~(\REF~\FUNC), \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
      5{:}\Bu32~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr)
        &\Rightarrow& \\&&&\quad
        \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EPASSIVE \} \\ &&|&

document/core/exec/instructions.rst

@@ -819,14 +819,14 @@ Reference Instructions
    S; F; (\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYNEWDATA~x~y) &\stepto& \TRAP
      \\&&
      \begin{array}[t]{@{}r@{~}l@{}}
-      (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}^n \\
+      (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\
       \land & s + n\cdot|\X{ft}|/8 > |S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA|)
      \end{array} \\
    \\[1ex]
    S; F; (\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYNEWDATA~x~y) &\stepto& (t.\CONST~c)^n~(\ARRAYNEWFIXED~x~n)
      \\&&
      \begin{array}[t]{@{}r@{~}l@{}}
-      (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}^n \\
+      (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\
       \land & t = \unpacktype(\X{ft}) \\
       \land & \concat((\bytes_{\X{ft}}(c))^n) = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice n\cdot|\X{ft}|/8] \\
      \end{array} \\
@@ -1065,7 +1065,7 @@ Reference Instructions
 
 12. Assert: due to :ref:`validation <valid-array.fill>`, the :ref:`array instance <syntax-arrayinst>` :math:`S.\SARRAYS[a]` exists.
 
-13. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then:
+13. If :math:`d + n` is larger than the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then:
 
     a. Trap.
 
@@ -1102,13 +1102,13 @@ Reference Instructions
      (\iff d + n > |S.\SARRAYS[a].\AIFIELDS|)
    \\[1ex]
    S; (\REFARRAYADDR~a)~(\I32.\CONST~d)~\val~(\I32.\CONST~0)~(\ARRAYFILL~x)
-     \quad\stepto\quad S; \epsilon
+     \quad\stepto\quad \epsilon
      \\ \qquad
      (\otherwise)
    \\[1ex]
    S; (\REFARRAYADDR~a)~(\I32.\CONST~d)~\val~(\I32.\CONST~n+1)~(\ARRAYFILL~x)
      \quad\stepto
-     \\ \quad S;
+     \\ \quad
        \begin{array}[t]{@{}l@{}}
        (\REFARRAYADDR~a)~(\I32.\CONST~d)~\val~(\ARRAYSET~x) \\
        (\REFARRAYADDR~a)~(\I32.\CONST~d+1)~\val~(\I32.\CONST~n)~(\ARRAYFILL~x) \\
@@ -1175,11 +1175,11 @@ Reference Instructions
 
 23. Assert: due to :ref:`validation <valid-array.copy>`, the :ref:`array instance <syntax-arrayinst>` :math:`S.\SARRAYS[a_2]` exists.
 
-24. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then:
+24. If :math:`d + n` is larger than the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then:
 
     a. Trap.
 
-25. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then:
+25. If :math:`s + n` is larger than the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then:
 
     a. Trap.
 
@@ -1252,7 +1252,7 @@ Reference Instructions
      (\iff d + n > |S.\SARRAYS[a_1].\AIFIELDS| \vee s + n > |S.\SARRAYS[a_2].\AIFIELDS|)
    \\[1ex]
    S; F; (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\ARRAYCOPY~x~y)
-     \quad\stepto\quad S; \epsilon
+     \quad\stepto\quad \epsilon
      \\ \qquad
      (\otherwise)
    \\[1ex]
@@ -1391,13 +1391,13 @@ Where:
      \end{array}
    \\[1ex]
    S; F; (\REFARRAYADDR~a)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\ARRAYINITDATA~x~y)
-     \quad\stepto\quad S; F; \epsilon
+     \quad\stepto\quad \epsilon
      \\ \qquad
      (\otherwise)
    \\[1ex]
    S; F; (\REFARRAYADDR~a)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYINITDATA~x~y)
      \quad\stepto
-     \\ \quad S; F;
+     \\ \quad
      \begin{array}[t]{@{}l@{}}
      (\REFARRAYADDR~a)~(\I32.\CONST~d)~(t.\CONST~c)~(\ARRAYSET~x) \\
      (\REFARRAYADDR~a)~(\I32.\CONST~d+1)~(\I32.\CONST~s+|\X{ft}|/8)~(\I32.\CONST~n)~(\ARRAYINITDATA~x~y) \\
@@ -1497,13 +1497,13 @@ Where:
      \end{array}
    \\[1ex]
    S; F; (\REFARRAYADDR~a)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\ARRAYINITELEM~x~y)
-     \quad\stepto\quad S; F; \epsilon
+     \quad\stepto\quad \epsilon
      \\ \qquad
      (\otherwise)
    \\[1ex]
    S; F; (\REFARRAYADDR~a)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\ARRAYINITELEM~x~y)
      \quad\stepto
-     \\ \quad S; F;
+     \\ \quad
      \begin{array}[t]{@{}l@{}}
      (\REFARRAYADDR~a)~(\I32.\CONST~d)~\REF~(\ARRAYSET~x) \\
      (\REFARRAYADDR~a)~(\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\ARRAYINITELEM~x~y) \\
@@ -1538,7 +1538,7 @@ Where:
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   (\REFNULL \X{ht})~\ANYCONVERTEXTERN &\stepto& (\REFNULL~\ANY) \\
+   (\REFNULL~\X{ht})~\ANYCONVERTEXTERN &\stepto& (\REFNULL~\ANY) \\
    (\REFEXTERN~\reff)~\ANYCONVERTEXTERN &\stepto& \reff \\
    \end{array}
 
@@ -1564,8 +1564,8 @@ Where:
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   (\REFNULL \X{ht})~\EXTERNCONVERTANY &\stepto& (\REFNULL~\EXTERN) \\
-   \reff~\EXTERNCONVERTANY &\stepto& (\REFEXTERN~\reff) & (\iff \reff \neq (\REFNULL \X{ht})) \\
+   (\REFNULL~\X{ht})~\EXTERNCONVERTANY &\stepto& (\REFNULL~\EXTERN) \\
+   \reff~\EXTERNCONVERTANY &\stepto& (\REFEXTERN~\reff) & (\iff \reff \neq (\REFNULL~\X{ht})) \\
    \end{array}
 
 
@@ -4195,8 +4195,8 @@ Control Instructions
 .. math::
    \begin{array}{lcl@{\qquad}l}
    S; F; \reff~(\BRONCAST~l~\X{rt}_1~\X{rt}_2) &\stepto& \reff~(\BR~l)
-     & (\iff S \vdashval \reff : \X{rt}
-        \land \vdashreftypematch \X{rt} \matchesreftype \insttype_{F.\AMODULE}(\X{rt}_2)) \\
+     & (\iff S \vdashval \reff : \X{rt}}
+        \land {} \vdashreftypematch \X{rt} \matchesreftype \insttype_{F.\AMODULE}(\X{rt}_2)) \\
    S; F; \reff~(\BRONCAST~l~\X{rt}_1~\X{rt}_2) &\stepto& \reff
      & (\otherwise) \\
    \end{array}
@@ -4231,7 +4231,7 @@ Control Instructions
    \begin{array}{lcl@{\qquad}l}
    S; F; \reff~(\BRONCASTFAIL~l~\X{rt}_1~\X{rt}_2) &\stepto& \reff
      & (\iff S \vdashval \reff : \X{rt}
-        \land \vdashreftypematch \X{rt} \matchesreftype \insttype_{F.\AMODULE}(\X{rt}_2)) \\
+        \land {} \vdashreftypematch \X{rt} \matchesreftype \insttype_{F.\AMODULE}(\X{rt}_2)) \\
    S; F; \reff~(\BRONCASTFAIL~l~\X{rt}_1~\X{rt}_2) &\stepto& \reff~(\BR~l)
      & (\otherwise) \\
    \end{array}

document/core/exec/values.rst

@@ -48,7 +48,7 @@ The following auxiliary typing rules specify this typing relation relative to a
 
 * The :ref:`heap type <syntax-heaptype>` must be :ref:`valid <valid-heaptype>` under the empty :ref:`context <context>`.
 
-* Then value is valid with :ref:`reference type <syntax-reftype>` :math:`(\REF~\NULL~t')`, where the :ref:`heap type <syntax-heaptype>` :math:`t'` that is the least type that :ref:`matches <match-heaptype>` :math:`t`.
+* Then the value is valid with :ref:`reference type <syntax-reftype>` :math:`(\REF~\NULL~t')`, where the :ref:`heap type <syntax-heaptype>` :math:`t'` is the least type that :ref:`matches <match-heaptype>` :math:`t`.
 
 .. math::
    \frac{

document/core/valid/instructions.rst

@@ -379,7 +379,7 @@ Aggregate Reference Instructions
      \qquad
      \X{ft}^\ast[y] = \mut~\X{st}
      \qquad
-     \sx = \epsilon \Leftrightarrow \X{st} = \unpacktype(\X{st})
+     \sx^? = \epsilon \Leftrightarrow \X{st} = \unpacktype(\X{st})
    }{
      C \vdashinstr \STRUCTGET\K{\_}\sx^?~x~y : [(\REF~\NULL~x)] \to [\unpacktype(\X{st})]
    }
@@ -508,7 +508,7 @@ Aggregate Reference Instructions
      \qquad
      C \vdashreftypematch C.\CELEMS[y] \matchesreftype \X{rt}
    }{
-     C \vdashinstr \ARRAYNEWELEM~x~n : [\I32~\I32] \to [(\REF~x)]
+     C \vdashinstr \ARRAYNEWELEM~x~y : [\I32~\I32] \to [(\REF~x)]
    }
 
 
@@ -539,7 +539,7 @@ Aggregate Reference Instructions
      \qquad
      C.\CDATAS[y] = {\ok}
    }{
-     C \vdashinstr \ARRAYNEWDATA~x~n : [\I32~\I32] \to [(\REF~x)]
+     C \vdashinstr \ARRAYNEWDATA~x~y : [\I32~\I32] \to [(\REF~x)]
    }
 
 
@@ -566,7 +566,7 @@ Aggregate Reference Instructions
    \frac{
      \expanddt(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st})
      \qquad
-     \sx = \epsilon \Leftrightarrow \X{st} = \unpacktype(\X{st})
+     \sx^? = \epsilon \Leftrightarrow \X{st} = \unpacktype(\X{st})
    }{
      C \vdashinstr \ARRAYGET\K{\_}\sx^?~x : [(\REF~\NULL~x)~\I32] \to [\unpacktype(\X{st})]
    }

document/js-api/index.bs

@@ -118,6 +118,7 @@ urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: df
     text: global_read; url: appendix/embedding.html#embed-global-read
     text: global_write; url: appendix/embedding.html#embed-global-write
     text: ref_type; url: appendix/embedding.html#embed-ref-type
+    text: val_default; url: appendix/embedding.html#embed-val-default
     text: match_valtype; url: appendix/embedding.html#embed-match-valtype
     text: error; url: appendix/embedding.html#embed-error
     text: store; url: exec/runtime.html#syntax-store
@@ -380,7 +381,7 @@ A {{Module}} object represents a single WebAssembly module. Each {{Module}} obje
                     1. Throw a {{LinkError}} exception.
                 1. If |valtype| is [=v128=],
                     1. Throw a {{LinkError}} exception.
-                1. Let |value| be [=ToWebAssemblyValue=](|v|, |valtype|).
+                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. Set the [=surrounding agent=]'s [=associated store=] to |store|.
@@ -853,6 +854,7 @@ Each {{Table}} object has a \[[Table]] internal slot, which is a [=table address
     1. If |maximum| is not empty and |maximum| < |initial|, throw a {{RangeError}} exception.
     1. If |value| is missing,
         1. Let |ref| be [=DefaultValue=](|elementType|).
+        1. Assert: |ref| is not [=error=].
     1. Otherwise,
         1. Let |ref| be [=?=] [=ToWebAssemblyValue=](|value|, |elementType|).
     1. Let |type| be the [=table type=] {[=table type|min=] |initial|, [=table type|max=] |maximum|} |elementType|.
@@ -870,6 +872,7 @@ Each {{Table}} object has a \[[Table]] internal slot, which is a [=table address
     1. Let (<var ignore>limits</var>, |elementType|) be [=table_type=](|tableaddr|).
     1. If |value| is missing,
         1. Let |ref| be [=DefaultValue=](|elementType|).
+        1. If |ref| is [=error=], throw a {{TypeError}} exception.
     1. Otherwise,
         1. Let |ref| be [=?=] [=ToWebAssemblyValue=](|value|, |elementType|).
     1. Let |result| be [=table_grow=](|store|, |tableaddr|, |delta|, |ref|).
@@ -903,6 +906,7 @@ Each {{Table}} object has a \[[Table]] internal slot, which is a [=table address
     1. Let (<var ignore>limits</var>, |elementType|) be [=table_type=](|tableaddr|).
     1. If |value| is missing,
         1. Let |ref| be [=DefaultValue=](|elementType|).
+        1. If |ref| is [=error=], throw a {{TypeError}} exception.
     1. Otherwise,
         1. Let |ref| be [=?=] [=ToWebAssemblyValue=](|value|, |elementType|).
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
@@ -979,13 +983,8 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each
 
 <div algorithm>
     The algorithm <dfn>DefaultValue</dfn>(|valuetype|) performs the following steps:
-    1. If |valuetype| equals [=i32=], return [=i32.const=] 0.
-    1. If |valuetype| equals [=i64=], return [=i64.const=] 0.
-    1. If |valuetype| equals [=f32=], return [=f32.const=] 0.
-    1. If |valuetype| equals [=f64=], return [=f64.const=] 0.
-    1. If |valuetype| equals [=funcref=], return [=ref.null=] [=funcref=].
     1. If |valuetype| equals [=externref=], return [=ToWebAssemblyValue=](undefined, |valuetype|).
-    1. Assert: This step is not reached.
+    1. Return [=val_default=](|valuetype|).
 </div>
 
 <div algorithm>
@@ -996,6 +995,7 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each
         1. Throw a {{TypeError}} exception.
     1. If |v| is missing,
         1. Let |value| be [=DefaultValue=](|valuetype|).
+        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|.

proposals/gc/MVP.md

@@ -466,7 +466,7 @@ Then, `$rttA` would carry supertype vector `[$rttA]`, `$rttB` has `[$rttA, $rttB
 Now consider a function that casts a `$B` to a `$C`:
 ```
 (func $castBtoC (param $x (ref $B)) (result (ref $C))
-  (ref.cast $C (local.get $x))
+  (ref.cast (ref $C) (local.get $x))
 )
 ```
 This can compile to machine code that (1) reads the RTT from `$x`, (2) checks that the length of its supertype table is >= 3, and (3) pointer-compares table[2] against `$rttC`.