Merge with WebAssembly/stack-switching

Author: dhil

document/core/appendix/changes.rst

@@ -462,6 +462,8 @@ Added more precise types for references. [#proposal-typedref]_
 
 * Refined typing of :ref:`local instructions <valid-instr-variable>` and :ref:`instruction sequences <valid-instr-seq>` to track the :ref:`initialization status <syntax-init>` of :ref:`locals <syntax-local>` with non-:ref:`defaultable <valid-defaultable>` type
 
+* Refined decoding of :ref:`active <syntax-elemmode>` :ref:`element segments <binary-elem>` with implicit element type and plain function indices (opcode :math:`0`) to produce :ref:`non-nullable <syntax-nullable>` :ref:`reference type <syntax-reftype>`.
+
 * Extended :ref:`table definitions <syntax-table>` with optional initializer expression
 
 

document/core/appendix/index-instructions.py

@@ -334,7 +334,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\STRUCTGETS~x~y', r'\hex{FB}~\hex{03}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'),
     Instruction(r'\STRUCTGETU~x~y', r'\hex{FB}~\hex{04}', r'[(\REF~\NULL~x)] \to [\I32]', r'valid-struct.get', r'exec-struct.get'),
     Instruction(r'\STRUCTSET~x~y', r'\hex{FB}~\hex{05}', r'[(\REF~\NULL~x)~t] \to []', r'valid-struct.set', r'exec-struct.set'),
-    Instruction(r'\ARRAYNEW~x', r'\hex{FB}~\hex{06}', r'[t] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'),
+    Instruction(r'\ARRAYNEW~x', r'\hex{FB}~\hex{06}', r'[t~\I32] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'),
     Instruction(r'\ARRAYNEWDEFAULT~x', r'\hex{FB}~\hex{07}', r'[\I32] \to [(\REF~x)]', r'valid-array.new', r'exec-array.new'),
     Instruction(r'\ARRAYNEWFIXED~x~n', r'\hex{FB}~\hex{08}', r'[t^n] \to [(\REF~x)]', r'valid-array.new_fixed', r'exec-array.new_fixed'),
     Instruction(r'\ARRAYNEWDATA~x~y', r'\hex{FB}~\hex{09}', r'[\I32~\I32] \to [(\REF~x)]', r'valid-array.new_data', r'exec-array.new_data'),

document/core/exec/instructions.rst

@@ -4753,7 +4753,7 @@ Control Instructions
      \begin{array}[t]{@{}r@{~}l@{}}
      (\iff & S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM[i] = \REFFUNCADDR~a \\
      \wedge & S.\SFUNCS[a] = f \\
-     \wedge & S \vdashdeftypematch F.\AMODULE.\MITYPES[y] \matchesdeftype f.\FITYPE)
+     \wedge & S \vdashdeftypematch f.\FITYPE \matchesdeftype F.\AMODULE.\MITYPES[y])
      \end{array}
    \\[1ex]
    \begin{array}{lcl@{\qquad}l}

document/core/exec/modules.rst

@@ -364,7 +364,7 @@ and list of :ref:`reference <syntax-ref>` vectors for the module's :ref:`element
 
 8. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEMS`, do:
 
-   a. Let :math:`\reftype_i` be the element :ref:`reference type <syntax-reftype>` obtained by `instantiating <type-inst>` :math:`\elem_i.\ETYPE` in :math:`\moduleinst` defined below.
+   a. Let :math:`\reftype_i` be the element :ref:`reference type <syntax-reftype>` obtained by :ref:`instantiating <type-inst>` :math:`\elem_i.\ETYPE` in :math:`\moduleinst` defined below.
 
    b. Let :math:`\elemaddr_i` be the :ref:`element address <syntax-elemaddr>` resulting from :ref:`allocating <alloc-elem>` a :ref:`element instance <syntax-eleminst>` of :ref:`reference type <syntax-reftype>` :math:`\reftype_i` with contents :math:`(\reff_{\F{e}}^\ast)^\ast[i]`.
 

document/core/syntax/types.rst

@@ -483,11 +483,11 @@ Global Types
 Tag Types
 ~~~~~~~~~
 
-*Tag types* classify the signature of :ref:`tags <syntax-tag>` with a function type.
+*Tag types* classify the signature of :ref:`tags <syntax-tag>` with a defined type |deftype|, which expands to a function type |functype|.
 
 .. math::
    \begin{array}{llll}
-   \production{tag type} &\tagtype &::=& \functype \\
+   \production{tag type} &\tagtype &::=& \deftype \\
    \end{array}
 
 Currently tags are only used for categorizing exceptions.

document/core/valid/instructions.rst

@@ -2601,15 +2601,15 @@ Control Instructions
 
 * The tag :math:`C.\CTAGS[x]` must be defined in the context.
 
-* Let :math:`[t^\ast] \to [{t'}^\ast]` be the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x]`.
+* Let :math:`[t^\ast] \to [{t'}^\ast]` be the :ref:`expansion <aux-expand-deftype>` of the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x]`.
 
 * The :ref:`result type <syntax-resulttype>` :math:`[{t'}^\ast]` must be empty.
 
-* Then the instruction is valid with type :math:`[t_1^\ast t^\ast] \to [t_2^\ast]`, for any sequences of  :ref:`value types <syntax-valtype>` :math:`t_1^\ast` and :math:`t_2^\ast`.
+* Then the instruction is valid with type :math:`[t_1^\ast t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types <syntax-valtype>` :math:`t_1^\ast` and :math:`t_2^\ast`.
 
 .. math::
    \frac{
-     C.\CTAGS[x] = [t^\ast] \to []
+     \expanddt(C.\CTAGS[x]) = [t^\ast] \to []
    }{
      C \vdashinstr \THROW~x : [t_1^\ast~t^\ast] \to [t_2^\ast]
    }

document/core/valid/matching.rst

@@ -580,14 +580,22 @@ A :ref:`global type <syntax-globaltype>` :math:`(\mut_1~t_1)` matches :math:`(\m
 Tag Types
 ~~~~~~~~~
 
-A :ref:`tag type <syntax-tagtype>` :math:`\tagtype_1` matches :math:`\tagtype_2` if and only if they are the same.
+A :ref:`tag type <syntax-tagtype>` :math:`\deftype_1` matches :math:`\deftype_2` if and only if the :ref:`defined type <syntax-deftype>` :math:`\deftype_1` :ref:`matches <match-deftype>` :math:`\deftype_2`, and vice versa.
 
 .. math::
    \frac{
+     C \vdashdeftypematch \deftype_1 \matchesdeftype \deftype_2
+     \qquad
+     C \vdashdeftypematch \deftype_2 \matchesdeftype \deftype_1
    }{
-     C \vdashtagtypematch \tagtype \matchestagtype \tagtype
+     C \vdashtagtypematch \deftype_1 \matchestagtype \deftype_2
    }
 
+.. note::
+   Although the conclusion of this rule looks identical to its premise,
+   they in fact describe different relations:
+   the premise invokes subtyping on defined types,
+   while the conclusion defines it on tag types that happen to be expressed as defined types.
 
 .. index:: external type, function type, table type, memory type, global type
 .. _match-externtype:

document/core/valid/types.rst

@@ -551,19 +551,25 @@ Memory Types
 Tag Types
 ~~~~~~~~~
 
-:math:`[t_1^n] \to [t_2^m]`
-...........................
+:math:`\deftype`
+................
 
-* The :ref:`function type <syntax-functype>` :math:`[t_1^n] \to [t_2^m]` must be :ref:`valid <valid-functype>`.
+
+* The :ref:`defined type <syntax-deftype>` :math:`\deftype` must be :ref:`valid <valid-deftype>`.
+
+* The :ref:`expansion <aux-expand-deftype>` of :math:`\deftype` must be a :ref:`function type <syntax-functype>` :math:`\TFUNC~[t_1^n] \toF [t_2^m]`.
 
 * The type sequence :math:`t_2^m` must be empty.
 
 * Then the tag type is valid.
 
 .. math::
    \frac{
+     C \vdashdeftype \deftype \ok
+     \qquad
+     \expanddt(\deftype) = \TFUNC~[t^\ast] \to []
    }{
-     \vdashtagtype [t^\ast] \to [] \ok
+     C \vdashtagtype \deftype \ok
    }
 
 

interpreter/exec/eval.ml

@@ -72,8 +72,8 @@ and admin_instr' =
   | Label of int * instr list * code
   | Frame of int * frame * code
   | Handler of int * catch list * code
-  | Handle of handle_table * code
-  | Suspending of tag_inst * value stack * ref_ option * ctxt
+  | Prompt of handle_table * code
+  | Suspending of tag_inst * value stack * (int32 * ref_) option * ctxt
 
 and ctxt = code -> code
 and handle_table = (tag_inst * idx) list * tag_inst list
@@ -391,7 +391,7 @@ let rec step (c : config) : config =
         let hs = handle_table c xls in
         let args, vs' = i32_split n vs e.at in
         cont := None;
-        vs', [Handle (hs, ctxt (args, [])) @@ e.at]
+        vs', [Prompt (hs, ctxt (args, [])) @@ e.at]
 
       | ResumeThrow (x, y, xls), Ref (NullRef _) :: vs ->
         vs, [Trapping "null continuation reference" @@ e.at]
@@ -405,18 +405,21 @@ let rec step (c : config) : config =
         let hs = handle_table c xls in
         let args, vs' = i32_split (Lib.List32.length ts) vs e.at in
         cont := None;
-        vs', [Handle (hs, ctxt ([], [Throwing (tagt, args) @@ e.at])) @@ e.at]
+        vs', [Prompt (hs, ctxt ([], [Throwing (tagt, args) @@ e.at])) @@ e.at]
 
       | Switch (x, y), Ref (NullRef _) :: vs ->
          vs, [Trapping "null continuation reference" @@ e.at]
 
       | Switch (x, y), Ref (ContRef {contents = None}) :: vs ->
          vs, [Trapping "continuation already consumed" @@ e.at]
 
-      | Switch (x, y), Ref (ContRef {contents = Some (n, ctxt)} as cont) :: vs ->
+      | Switch (x, y), Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs ->
+         let FuncT (ts, _) = func_type_of_cont_type c.frame.inst (cont_type c.frame.inst x) in
+         let FuncT (ts', _) = as_cont_func_ref_type (Lib.List.last ts) in
+         let arity = Lib.List32.length ts' in
          let tagt = tag c.frame.inst y in
          let args, vs' = i32_split (Int32.sub n 1l) vs e.at in
-         vs', [Suspending (tagt, args, Some cont, fun code -> code) @@ e.at]
+         vs', [Suspending (tagt, args, Some (arity, ContRef cont), fun code -> code) @@ e.at]
 
       | ReturnCall x, vs ->
         (match (step {c with code = (vs, [Plain (Call x) @@ e.at])}).code with
@@ -1282,35 +1285,34 @@ let rec step (c : config) : config =
         with Crash (_, msg) -> Crash.error e.at msg)
       )
 
-    | Handle (hso, (vs', [])), vs ->
+    | Prompt (hso, (vs', [])), vs ->
       vs' @ vs, []
 
-    | Handle ((hs, _), (vs', {it = Suspending (tagt, vs1, None, ctxt); at} :: es')), vs
+    | Prompt ((hs, _), (vs', {it = Suspending (tagt, vs1, None, ctxt); at} :: es')), vs
       when List.mem_assq tagt hs ->
       let FuncT (_, ts) = func_type_of_tag_type c.frame.inst (Tag.type_of tagt) in
       let ctxt' code = compose (ctxt code) (vs', es') in
       [Ref (ContRef (ref (Some (Lib.List32.length ts, ctxt'))))] @ vs1 @ vs,
       [Plain (Br (List.assq tagt hs)) @@ e.at]
 
-    | Handle ((_, hs) as hso, (vs', {it = Suspending (tagt, vs1, Some (ContRef ({contents = Some (_, ctxt)} as cont)), ctxt'); at} :: es')), vs
+    | Prompt ((_, hs) as hso, (vs', {it = Suspending (tagt, vs1, Some (ar, ContRef ({contents = Some (_, ctxt)} as cont)), ctxt'); at} :: es')), vs
        when List.memq tagt hs ->
-       let FuncT (_, ts) = func_type_of_tag_type c.frame.inst (Tag.type_of tagt) in
        let ctxt'' code = compose (ctxt' code) (vs', es') in
-       let cont' = Ref (ContRef (ref (Some (Int32.add (Lib.List32.length ts) 1l, ctxt'')))) in
+       let cont' = Ref (ContRef (ref (Some (ar, ctxt'')))) in
        let args = cont' :: vs1 in
        cont := None;
-       vs' @ vs, [Handle (hso, ctxt (args, [])) @@ e.at]
+       vs' @ vs, [Prompt (hso, ctxt (args, [])) @@ e.at]
 
-    | Handle (hso, (vs', {it = Suspending (tagt, vs1, contref, ctxt); at} :: es')), vs ->
-      let ctxt' code = [], [Handle (hso, compose (ctxt code) (vs', es')) @@ e.at] in
+    | Prompt (hso, (vs', {it = Suspending (tagt, vs1, contref, ctxt); at} :: es')), vs ->
+      let ctxt' code = [], [Prompt (hso, compose (ctxt code) (vs', es')) @@ e.at] in
       vs, [Suspending (tagt, vs1, contref, ctxt') @@ at]
 
-    | Handle (hso, (vs', e' :: es')), vs when is_jumping e' ->
+    | Prompt (hso, (vs', e' :: es')), vs when is_jumping e' ->
       vs, [e']
 
-    | Handle (hso, code'), vs ->
+    | Prompt (hso, code'), vs ->
       let c' = step {c with code = code'} in
-      vs, [Handle (hso, c'.code) @@ e.at]
+      vs, [Prompt (hso, c'.code) @@ e.at]
 
     | Suspending (_, _, _, _), _ -> assert false
 

interpreter/syntax/types.ml

@@ -114,18 +114,6 @@ let defaultable = function
   | BotT -> assert false
 
 
-(* Conversions & Projections *)
-
-let num_type_of_addr_type = function
-  | I32AT -> I32T
-  | I64AT -> I64T
-
-let addr_type_of_num_type = function
-  | I32T -> I32AT
-  | I64T -> I64AT
-  | _ -> assert false
-
-
 (* Filters *)
 
 let funcs = List.filter_map (function ExternFuncT ft -> Some ft | _ -> None)
@@ -283,14 +271,29 @@ let expand_def_type (dt : def_type) : str_type =
   let SubT (_, _, st) = unroll_def_type dt in
   st
 
-(* Projections *)
+
+(* Conversions & Projections *)
+
+let num_type_of_addr_type = function
+  | I32AT -> I32T
+  | I64AT -> I64T
+
+let addr_type_of_num_type = function
+  | I32T -> I32AT
+  | I64T -> I64AT
+  | _ -> assert false
 
 let unpacked_storage_type = function
   | ValStorageT t -> t
   | PackStorageT _ -> NumT I32T
 
 let unpacked_field_type (FieldT (_mut, t)) = unpacked_storage_type t
 
+let as_def_heap_type (ht : heap_type) : def_type =
+  match ht with
+  | DefHT def -> def
+  | _ -> assert false
+
 let as_func_str_type (st : str_type) : func_type =
   match st with
   | DefFuncT ft -> ft
@@ -311,10 +314,18 @@ let as_array_str_type (st : str_type) : array_type =
   | DefArrayT at -> at
   | _ -> assert false
 
+let as_cont_func_heap_type (ht : heap_type) : func_type =
+  let ContT ht' = as_cont_str_type (expand_def_type (as_def_heap_type ht)) in
+  as_func_str_type (expand_def_type (as_def_heap_type ht'))
+
+let as_cont_func_ref_type (rt : val_type) : func_type =
+  match rt with
+  | RefT (_, ht) -> as_cont_func_heap_type ht
+  | _ -> assert false
+
 let extern_type_of_import_type (ImportT (et, _, _)) = et
 let extern_type_of_export_type (ExportT (et, _)) = et
 
-
 (* String conversion *)
 
 let string_of_idx x =