Merge pull request #47 from dhil/wasmfx-ref-interp

WasmFX reference interpreter and testsuite

.github/workflows/ci-interpreter.yml

@@ -33,4 +33,4 @@ jobs:
       - name: Run tests
         # TODO: reactiate node once it supports all of Wasm 3.0
         # run: cd interpreter && opam exec make JS=node ci
-        run: cd interpreter && opam exec make ci
+        run: cd interpreter && opam exec make test

document/core/appendix/embedding.rst

@@ -696,7 +696,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}
 
@@ -712,6 +712,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/valid/instructions.rst

@@ -2112,10 +2112,15 @@ Control Instructions
 
 * There must be a sequence :math:`t^\ast` of :ref:`value types <syntax-valtype>`, such that:
 
-  * The result type :math:`[t^\ast]` :ref:`matches <match-resulttype>` :math:`C.\CLABELS[l_N]`.
+  * The length of the sequence :math:`t^\ast` is the same as the length of the sequence :math:`C.\CLABELS[l_N]`.
 
-  * For all :math:`l_i` in :math:`l^\ast`,
-    the result type :math:`[t^\ast]` :ref:`matches <match-resulttype>` :math:`C.\CLABELS[l_i]`.
+  * For each :ref:`operand type <syntax-opdtype>` :math:`t_j` in :math:`t^\ast` and corresponding type :math:`t'_{Nj}` in :math:`C.\CLABELS[l_N]`, :math:`t_j` :ref:`matches <match-opdtype>` :math:`t'_{Nj}`.
+
+  * For each :ref:`label <syntax-label>` :math:`l_i` in :math:`l^\ast`:
+
+    * The length of the sequence :math:`t^\ast` is the same as the length of the sequence :math:`C.\CLABELS[l_i]`.
+
+    * For each :ref:`operand type <syntax-opdtype>` :math:`t_j` in :math:`t^\ast` and corresponding type :math:`t'_{ij}` in :math:`C.\CLABELS[l_i]`, :math:`t_j` :ref:`matches <match-opdtype>` :math:`t'_{ij}`.
 
 * Then the instruction is valid with any :ref:`valid <valid-instrtype>` type of the form :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`.
 

document/js-api/index.bs

@@ -1389,7 +1389,7 @@ The internal methods of an [=Exported GC Object=] use the following implementati
     1. Return keys.
 </div>
 
-<div algorithm>
+<div algorithm="gc">
   To create <dfn>a new Exported GC Object</dfn> from a WebAssembly [=object address=] |objectaddr| and a string |objectkind|, perform the following steps:
 
     1. Assert: |objectkind| is either "array" or "struct".

interpreter/binary/decode.ml

@@ -180,6 +180,7 @@ let heap_type s =
     (fun s -> VarHT (var_type s33 s));
     (fun s ->
       match s7 s with
+      | -0x0b -> NoContHT
       | -0x0c -> NoExnHT
       | -0x0d -> NoFuncHT
       | -0x0e -> NoExternHT
@@ -192,13 +193,15 @@ let heap_type s =
       | -0x15 -> StructHT
       | -0x16 -> ArrayHT
       | -0x17 -> ExnHT
+      | -0x18 -> ContHT
       | _ -> error s pos "malformed heap type"
     )
   ] s
 
 let ref_type s =
   let pos = pos s in
   match s7 s with
+  | -0x0b -> (Null, NoContHT)
   | -0x0c -> (Null, NoExnHT)
   | -0x0d -> (Null, NoFuncHT)
   | -0x0e -> (Null, NoExternHT)
@@ -211,6 +214,7 @@ let ref_type s =
   | -0x15 -> (Null, StructHT)
   | -0x16 -> (Null, ArrayHT)
   | -0x17 -> (Null, ExnHT)
+  | -0x18 -> (Null, ContHT)
   | -0x1c -> (NoNull, heap_type s)
   | -0x1d -> (Null, heap_type s)
   | _ -> error s pos "malformed reference type"
@@ -253,11 +257,15 @@ let func_type s =
   let ts2 = result_type s in
   FuncT (ts1, ts2)
 
+let cont_type s =
+  ContT (heap_type s)
+
 let str_type s =
   match s7 s with
   | -0x20 -> DefFuncT (func_type s)
   | -0x21 -> DefStructT (struct_type s)
   | -0x22 -> DefArrayT (array_type s)
+  | -0x23 -> DefContT (cont_type s) (* TODO(dhil): See comment in encode.ml *)
   | _ -> error s (pos s - 1) "malformed definition type"
 
 let sub_type s =
@@ -293,14 +301,16 @@ let memory_type s =
   let lim = limits u32 s in
   MemoryT lim
 
+let tag_type s =
+  zero s;
+  let et = heap_type s in
+  TagT et
+
 let global_type s =
   let t = val_type s in
   let mut = mutability s in
   GlobalT (mut, t)
 
-let tag_type s =
-  zero s; at var s
-
 
 (* Instructions *)
 
@@ -327,6 +337,11 @@ let block_type s =
     (fun s -> ValBlockType (Some (val_type s)));
   ] s
 
+let var_pair s =
+  let x = at var s in
+  let y = at var s in
+  x, y
+
 let local s =
   let n = u32 s in
   let t = at val_type s in
@@ -399,7 +414,10 @@ let rec instr s =
   | 0x14 -> call_ref (at var s)
   | 0x15 -> return_call_ref (at var s)
 
-  | 0x16 | 0x17 | 0x18 | 0x19 as b -> illegal s pos b
+  | (0x16 | 0x17) as b -> illegal s pos b
+
+  | 0x18 -> error s pos "misplaced DELEGATE opcode"
+  | 0x19 -> error s pos "misplaced CATCH_ALL opcode"
 
   | 0x1a -> drop
   | 0x1b -> select None
@@ -607,6 +625,27 @@ let rec instr s =
   | 0xd5 -> br_on_null (at var s)
   | 0xd6 -> br_on_non_null (at var s)
 
+  | 0xe0 -> cont_new (at var s)
+  | 0xe1 ->
+    let x = at var s in
+    let y = at var s in
+    cont_bind x y
+  | 0xe2 -> suspend (at var s)
+  | 0xe3 ->
+    let x = at var s in
+    let xls = vec var_pair s in
+    resume x xls
+  | 0xe4 ->
+    let x   = at var s in
+    let tag = at var s in
+    let xls = vec var_pair s in
+    resume_throw x tag xls
+  | 0xe5 ->
+    let bt = block_type s in
+    let es' = instr_block s in
+    end_ s;
+    barrier bt es'
+
   | 0xfb as b ->
     (match u32 s with
     | 0x00l -> struct_new (at var s)
@@ -971,11 +1010,11 @@ let rec instr s =
 and instr_block s = List.rev (instr_block' s [])
 and instr_block' s es =
   match peek s with
-  | None | Some (0x05 | 0x0b) -> es
+  | None | Some (0x05 | 0x07 | 0x0b | 0x19) -> es
   | _ ->
     let pos = pos s in
     let e' = instr s in
-    instr_block' s ((e' @@ region s pos pos) :: es)
+    instr_block' s (Source.(e' @@ region s pos pos) :: es)
 
 and catch s =
   match byte s with
@@ -1045,7 +1084,7 @@ let import_desc s =
   | 0x01 -> TableImport (table_type s)
   | 0x02 -> MemoryImport (memory_type s)
   | 0x03 -> GlobalImport (global_type s)
-  | 0x04 -> TagImport (tag_type s)
+  | 0x04 -> TagImport (at var s)
   | _ -> error s (pos s - 1) "malformed import kind"
 
 let import s =
@@ -1098,12 +1137,13 @@ let memory_section s =
 (* Tag section *)
 
 let tag s =
-  let tgtype = tag_type s in
-  {tgtype}
+  let tagtype = tag_type s in
+  {tagtype}
 
 let tag_section s =
   section `TagSection (vec (at tag)) [] s
 
+
 (* Global section *)
 
 let global s =
@@ -1329,7 +1369,6 @@ let module_ s =
   in { types; tables; memories; globals; tags; funcs;
        imports; exports; elems; datas; start }
 
-
 let decode name bs = at module_ (stream name bs)
 
 let all_custom tag s =

interpreter/binary/encode.ml

@@ -98,8 +98,6 @@ struct
   open Types
   open Source
 
-  let var x = u32 x.it
-
   let mutability = function
     | Cons -> byte 0
     | Var -> byte 1
@@ -130,6 +128,8 @@ struct
     | NoExnHT -> s7 (-0x0c)
     | ExternHT -> s7 (-0x11)
     | NoExternHT -> s7 (-0x0e)
+    | ContHT -> s7 (-0x18)
+    | NoContHT -> s7 (-0x0b)
     | VarHT x -> var_type s33 x
     | DefHT _ | BotHT -> assert false
 
@@ -150,6 +150,8 @@ struct
     | (Null, NoExnHT) -> s7 (-0x0c)
     | (Null, ExternHT) -> s7 (-0x11)
     | (Null, NoExternHT) -> s7 (-0x0e)
+    | (Null, ContHT) -> s7 (-0x18)
+    | (Null, NoContHT) -> s7 (-0x0b)
     | (Null, t) -> s7 (-0x1d); heap_type t
     | (NoNull, t) -> s7 (-0x1c); heap_type t
 
@@ -180,10 +182,17 @@ struct
   let func_type = function
     | FuncT (ts1, ts2) -> vec val_type ts1; vec val_type ts2
 
+  let cont_type = function
+    | ContT ht -> heap_type ht
+
   let str_type = function
     | DefStructT st -> s7 (-0x21); struct_type st
     | DefArrayT at -> s7 (-0x22); array_type at
     | DefFuncT ft -> s7 (-0x20); func_type ft
+    | DefContT ct -> s7 (-0x23); cont_type ct
+    (* TODO(dhil): This might need to change again in the future as a
+       different proposal might claim this opcode! GC proposal claimed
+       the previous opcode we were using. *)
 
   let sub_type = function
     | SubT (Final, [], st) -> str_type st
@@ -206,9 +215,8 @@ struct
   let global_type = function
     | GlobalT (mut, t) -> val_type t; mutability mut
 
-  let tag_type x =
-    u32 0x00l; var x
-
+  let tag_type = function
+    | TagT ht -> byte 0x00; heap_type ht
 
   (* Expressions *)
 
@@ -222,6 +230,7 @@ struct
   let end_ () = op 0x0b
 
   let var x = u32 x.it
+  let var_pair (x, y) = var x; var y
 
   let memop x {align; offset; _} =
     let has_var = x.it <> 0l in
@@ -278,6 +287,13 @@ struct
     | ReturnCallRef x -> op 0x15; var x
     | ReturnCallIndirect (x, y) -> op 0x13; var y; var x
 
+    | ContNew x -> op 0xe0; var x
+    | ContBind (x, y) -> op 0xe1; var x; var y
+    | Suspend x -> op 0xe2; var x
+    | Resume (x, xls) -> op 0xe3; var x; vec var_pair xls
+    | ResumeThrow (x, y, xls) -> op 0xe4; var x; var y; vec var_pair xls
+    | Barrier (bt, es) -> op 0xe5; block_type bt; list instr es; end_ ()
+
     | Throw x -> op 0x08; var x
     | ThrowRef -> op 0x0a
 
@@ -925,7 +941,7 @@ struct
     | TableImport t -> byte 0x01; table_type t
     | MemoryImport t -> byte 0x02; memory_type t
     | GlobalImport t -> byte 0x03; global_type t
-    | TagImport t -> byte 0x04; tag_type t
+    | TagImport t -> byte 0x04; var t
 
   let import im =
     let {module_name; item_name; idesc} = im.it in
@@ -966,14 +982,6 @@ struct
     section 5 (vec memory) mems (mems <> [])
 
 
-  (* Tag section *)
-
-  let tag (t : tag) = byte 0x00; var t.it.tgtype
-
-  let tag_section ts =
-    section 13 (vec tag) ts (ts <> [])
-
-
   (* Global section *)
 
   let global g =
@@ -983,6 +991,12 @@ struct
   let global_section gs =
     section 6 (vec global) gs (gs <> [])
 
+  (* Tag section *)
+  let tag tag =
+    tag_type tag.it.tagtype
+
+  let tag_section ts =
+    section 13 (vec tag) ts (ts <> [])
 
   (* Export section *)