Merge with WebAssembly/gc

document/core/appendix/algorithm.rst

@@ -95,6 +95,28 @@ We further assume that :ref:`validation <valid-valtype>` and :ref:`subtyping <ma
    func is_struct(t : comp_type) : bool
    func is_array(t : comp_type) : bool
 
+Finally, the following function computes the least precise supertype of a given :ref:`heap type <syntax-heaptype>` (its corresponding top type):
+
+.. code-block:: pseudo
+
+   func top_heap_type(t : heap_type) : heap_type =
+     switch (t)
+       case (Any | Eq | I31 | Struct | Array | None)
+         return Any
+       case (Func | Nofunc)
+         return Func
+       case (Extern | Noextern)
+         return Extern
+       case (Def(dt))
+         switch (dt.rec.types[dt.proj].body)
+           case (Struct(_) | Array(_))
+             return Any
+           case (Func(_))
+             return Func
+       case (Bot)
+         raise CannotOccurInSource
+
+
 Context
 .......
 
@@ -312,6 +334,11 @@ Other instructions are checked in a similar manner.
          let rt = pop_ref()
          push_val(Ref(rt.heap, false))
 
+       case (ref.test rt)
+         validate_ref_type(rt)
+         pop_val(Ref(top_heap_type(rt), true))
+         push_val(I32)
+
        case (local.get x)
          get_local(x)
          push_val(locals[x])

document/core/appendix/index-instructions.py

@@ -87,7 +87,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\CALL~x', r'\hex{10}', r'[t_1^\ast] \to [t_2^\ast]', r'valid-call', r'exec-call'),
     Instruction(r'\CALLINDIRECT~x~y', r'\hex{11}', r'[t_1^\ast~\I32] \to [t_2^\ast]', r'valid-call_indirect', r'exec-call_indirect'),
     Instruction(r'\RETURNCALL~x', r'\hex{12}', r'[t_1^\ast] \to [t_2^\ast]', r'valid-return_call', r'exec-return_call'),
-    Instruction(r'\RETURNCALLINDIRECT~x', r'\hex{13}', r'[t_1^\ast~\I32] \to [t_2^\ast]', r'valid-return_call_indirect', r'exec-return_call_indirect'),
+    Instruction(r'\RETURNCALLINDIRECT~x~y', r'\hex{13}', r'[t_1^\ast~\I32] \to [t_2^\ast]', r'valid-return_call_indirect', r'exec-return_call_indirect'),
     Instruction(r'\CALLREF~x', r'\hex{14}', r'[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]', r'valid-call_ref', r'exec-call_ref'),
     Instruction(r'\RETURNCALLREF~x', r'\hex{15}', r'[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]', r'valid-return_call_ref', r'exec-return_call_ref'),
     Instruction(None, r'\hex{16}'),

document/core/binary/modules.rst

@@ -223,7 +223,7 @@ It decodes into a vector of :ref:`tables <syntax-table>` that represent the |MTA
 .. note::
    The encoding of a table type cannot start with byte :math:`\hex{40}`,
    hence decoding is unambiguous.
-   The zero byte following it is reserved for futre extensions.
+   The zero byte following it is reserved for future extensions.
 
 
 .. index:: ! memory section, memory, memory type

document/core/exec/instructions.rst

@@ -4432,22 +4432,22 @@ Control Instructions
 
 .. _exec-return_call_indirect:
 
-:math:`\RETURNCALLINDIRECT~x`
-.............................
+:math:`\RETURNCALLINDIRECT~x~y`
+...............................
 
 1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
 
-2. Assert: due to :ref:`validation <valid-call_indirect>`, :math:`F.\AMODULE.\MITABLES[0]` exists.
+2. Assert: due to :ref:`validation <valid-call_indirect>`, :math:`F.\AMODULE.\MITABLES[x]` exists.
 
-3. Let :math:`\X{ta}` be the :ref:`table address <syntax-tableaddr>` :math:`F.\AMODULE.\MITABLES[0]`.
+3. Let :math:`\X{ta}` be the :ref:`table address <syntax-tableaddr>` :math:`F.\AMODULE.\MITABLES[x]`.
 
 4. Assert: due to :ref:`validation <valid-call_indirect>`, :math:`S.\STABLES[\X{ta}]` exists.
 
 5. Let :math:`\X{tab}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\STABLES[\X{ta}]`.
 
-6. Assert: due to :ref:`validation <valid-call_indirect>`, :math:`F.\AMODULE.\MITYPES[x]` is defined.
+6. Assert: due to :ref:`validation <valid-call_indirect>`, :math:`F.\AMODULE.\MITYPES[y]` is defined.
 
-7. Let :math:`\X{dt}_{\F{expect}}` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[x]`.
+7. Let :math:`\X{dt}_{\F{expect}}` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[y]`.
 
 8. Assert: due to :ref:`validation <valid-call_indirect>`, a value with :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
 
@@ -4478,10 +4478,10 @@ Control Instructions
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   \val~(\RETURNCALLINDIRECT~x) &\stepto& (\RETURNINVOKE~a)
-     & (\iff \val~(\CALLINDIRECT~x) \stepto (\INVOKE~a)) \\
-   \val~(\RETURNCALLINDIRECT~x) &\stepto& \TRAP
-     & (\iff \val~(\CALLINDIRECT~x) \stepto \TRAP) \\
+   \val~(\RETURNCALLINDIRECT~x~y) &\stepto& (\RETURNINVOKE~a)
+     & (\iff \val~(\CALLINDIRECT~x~y) \stepto (\INVOKE~a)) \\
+   \val~(\RETURNCALLINDIRECT~x~y) &\stepto& \TRAP
+     & (\iff \val~(\CALLINDIRECT~x~y) \stepto \TRAP) \\
    \end{array}
 
 

document/core/valid/instructions.rst

@@ -265,6 +265,10 @@ Reference Instructions
      C \vdashinstr \REFTEST~\X{rt} : [\X{rt}'] \to [\I32]
    }
 
+.. note::
+   The liberty to pick a supertype :math:`\X{rt}'` allows typing the instruction with the least precise super type of :math:`\X{rt}` as input, that is, the top type in the corresponding heap subtyping hierarchy.
+
+
 .. _valid-ref.cast:
 
 :math:`\REFCAST~\X{rt}`
@@ -285,6 +289,9 @@ Reference Instructions
      C \vdashinstr \REFCAST~\X{rt} : [\X{rt}'] \to [\X{rt}]
    }
 
+.. note::
+   The liberty to pick a supertype :math:`\X{rt}'` allows typing the instruction with the least precise super type of :math:`\X{rt}` as input, that is, the top type in the corresponding heap subtyping hierarchy.
+
 
 .. index:: aggregate reference