Merge with WebAssembly/gc

Author: dhil

document/core/appendix/changes.rst

@@ -168,7 +168,7 @@ Added more precise types for references [#proposal-typedref]_.
 .. index:: reference, reference type, heap type, field type, storage type, structure type, array type, composite type, sub type, recursive type
 
 Garbage Collection
-~~~~~~~~~~~~~~~~~~
+..................
 
 Added managed reference types [#proposal-gc]_.
 

document/core/exec/instructions.rst

@@ -1341,47 +1341,43 @@ Where:
 
 19. Assert: due to :ref:`validation <valid-array.init_data>`, the :ref:`array instance <syntax-arrayinst>` :math:`S.\SARRAYS[a]` exists.
 
-20. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then:
+20. Assert: due to :ref:`validation <valid-array.init_data>`, the :ref:`field type <syntax-fieldtype>` :math:`\X{ft}` has a defined :ref:`bit width <bitwidth-fieldtype>`.
 
-    a. Trap.
-
-21. Assert: due to :ref:`validation <valid-array.init_data>`, the :ref:`field type <syntax-fieldtype>` :math:`\X{ft}` has a defined :ref:`bit width <bitwidth-fieldtype>`.
+21. Let :math:`z` be the :ref:`bit width <bitwidth-fieldtype>` of :ref:`field type <syntax-fieldtype>` :math:`\X{ft}` divided by eight.
 
-22. Let :math:`z` be the :ref:`bit width <bitwidth-fieldtype>` of :ref:`field type <syntax-fieldtype>` :math:`\X{ft}` divided by eight.
-
-23. If the sum of :math:`s` and :math:`n` times :math:`z` is larger than the length of :math:`\datainst.\DIDATA`, then:
+22. If :math:`d + n` is larger than the length of :math:`S.\SARRAYS[a].\AIFIELDS`, or the sum of :math:`s` and :math:`n` times :math:`z` is larger than the length of :math:`\datainst.\DIDATA`, then:
 
     a. Trap.
 
-24. If :math:`n = 0`, then:
+23. If :math:`n = 0`, then:
 
     a. Return.
 
-25. Let :math:`b^\ast` be the :ref:`byte <syntax-byte>` sequence :math:`\datainst.\DIDATA[s \slice z]`.
+24. Let :math:`b^\ast` be the :ref:`byte <syntax-byte>` sequence :math:`\datainst.\DIDATA[s \slice z]`.
 
-26. Let :math:`t` be the :ref:`value type <syntax-valtype>` :math:`\unpacktype(\X{ft})`.
+25. Let :math:`t` be the :ref:`value type <syntax-valtype>` :math:`\unpacktype(\X{ft})`.
 
-27. Assert: due to :ref:`validation <valid-array.init_data>`, :math:`\bytes_{\X{ft}}` is defined.
+26. Assert: due to :ref:`validation <valid-array.init_data>`, :math:`\bytes_{\X{ft}}` is defined.
 
-28. Let :math:`c` be the constant for which :math:`\bytes_{\X{ft}}(c)` is :math:`b^\ast`.
+27. Let :math:`c` be the constant for which :math:`\bytes_{\X{ft}}(c)` is :math:`b^\ast`.
 
-29. Push the value :math:`\REFARRAYADDR~a` to the stack.
+28. Push the value :math:`\REFARRAYADDR~a` to the stack.
 
-30. Push the value :math:`\I32.\CONST~d` to the stack.
+29. Push the value :math:`\I32.\CONST~d` to the stack.
 
-31. Push the value :math:`t.\CONST~c` to the stack.
+30. Push the value :math:`t.\CONST~c` to the stack.
 
-32. Execute the instruction :math:`\ARRAYSET~x`.
+31. Execute the instruction :math:`\ARRAYSET~x`.
 
-33. Push the value :math:`\REFARRAYADDR~a` to the stack.
+32. Push the value :math:`\REFARRAYADDR~a` to the stack.
 
-34. Push the value :math:`\I32.\CONST~(d+1)` to the stack.
+33. Push the value :math:`\I32.\CONST~(d+1)` to the stack.
 
-35. Push the value :math:`\I32.\CONST~(s+z)` to the stack.
+34. Push the value :math:`\I32.\CONST~(s+z)` to the stack.
 
-36. Push the value :math:`\I32.\CONST~(n-1)` to the stack.
+35. Push the value :math:`\I32.\CONST~(n-1)` to the stack.
 
-37. Execute the instruction :math:`\ARRAYINITDATA~x~y`.
+36. Execute the instruction :math:`\ARRAYINITDATA~x~y`.
 
 .. math::
    ~\\[-1ex]
@@ -1462,37 +1458,33 @@ Where:
 
 19. Assert: due to :ref:`validation <valid-array.init_elem>`, the :ref:`array instance <syntax-arrayinst>` :math:`S.\SARRAYS[a]` exists.
 
-20. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then:
+20. If :math:`d + n` is larger than the length of :math:`S.\SARRAYS[a].\AIFIELDS`, or :math:`s + n` is larger than the length of :math:`\eleminst.\EIELEM`, then:
 
     a. Trap.
 
-21. If :math:`s + n` is larger than or equal to the length of :math:`\eleminst.\EIELEM`, then:
-
-    a. Trap.
-
-22. If :math:`n = 0`, then:
+21. If :math:`n = 0`, then:
 
     a. Return.
 
-23. Let :math:`\reff'` be the :ref:`reference value <syntax-ref>` :math:`\eleminst.\EIELEM[s]`.
+22. Let :math:`\reff'` be the :ref:`reference value <syntax-ref>` :math:`\eleminst.\EIELEM[s]`.
 
-24. Push the value :math:`\REFARRAYADDR~a` to the stack.
+23. Push the value :math:`\REFARRAYADDR~a` to the stack.
 
-25. Push the value :math:`\I32.\CONST~d` to the stack.
+24. Push the value :math:`\I32.\CONST~d` to the stack.
 
-26. Push the value :math:`\reff'` to the stack.
+25. Push the value :math:`\reff'` to the stack.
 
-27. Execute the instruction :math:`\ARRAYSET~x`.
+26. Execute the instruction :math:`\ARRAYSET~x`.
 
-28. Push the value :math:`\REFARRAYADDR~a` to the stack.
+27. Push the value :math:`\REFARRAYADDR~a` to the stack.
 
-29. Push the value :math:`\I32.\CONST~(d+1)` to the stack.
+28. Push the value :math:`\I32.\CONST~(d+1)` to the stack.
 
-30. Push the value :math:`\I32.\CONST~(s+1)` to the stack.
+29. Push the value :math:`\I32.\CONST~(s+1)` to the stack.
 
-31. Push the value :math:`\I32.\CONST~(n-1)` to the stack.
+30. Push the value :math:`\I32.\CONST~(n-1)` to the stack.
 
-32. Execute the instruction :math:`\ARRAYINITELEM~x~y`.
+31. Execute the instruction :math:`\ARRAYINITELEM~x~y`.
 
 .. math::
    ~\\[-1ex]

document/core/exec/modules.rst

@@ -517,19 +517,17 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
 
 .. _exec-initvals:
 
-5. Let :math:`\moduleinst_{\F{init}}` be the auxiliary module :ref:`instance <syntax-moduleinst>` :math:`\{\MIGLOBALS~\evglobals(\externval^n), \MIFUNCS~\moduleinst.\MIFUNCS\}` that only consists of the imported globals and the imported and allocated functions from the final module instance :math:`\moduleinst`, defined below.
+6. Let :math:`F` be the auxiliary :ref:`frame <syntax-frame>` :math:`\{ \AMODULE~\moduleinst, \ALOCALS~\epsilon \}`, that consists of the final module instance :math:`\moduleinst`, defined below.
 
-6. Let :math:`F_{\F{init}}` be the auxiliary :ref:`frame <syntax-frame>` :math:`\{ \AMODULE~\moduleinst_{\F{init}}, \ALOCALS~\epsilon \}`.
-
-7. Push the frame :math:`F_{\F{init}}` to the stack.
+7. Push the frame :math:`F` to the stack.
 
 8. Let :math:`\val_{\F{g}}^\ast` be the vector of :ref:`global <syntax-global>` initialization :ref:`values <syntax-val>` determined by :math:`\module` and :math:`\externval^n`. These may be calculated as follows.
 
    a. For each :ref:`global <syntax-global>` :math:`\global_i` in :math:`\module.\MGLOBALS`, do:
 
       i. Let :math:`\val_{\F{g}i}` be the result of :ref:`evaluating <exec-expr>` the initializer expression :math:`\global_i.\GINIT`.
 
-   b. Assert: due to :ref:`validation <valid-module>`, the frame :math:`F_{\F{init}}` is now on the top of the stack.
+   b. Assert: due to :ref:`validation <valid-module>`, the frame :math:`F` is now on the top of the stack.
 
    c. Let :math:`\val_{\F{g}}^\ast` be the concatenation of :math:`\val_{\F{g}i}` in index order.
 
@@ -543,7 +541,7 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
 
       iii. Let :math:`\reff_{\F{t}i}` be the reference :math:`\val_{\F{t}i}`.
 
-   b. Assert: due to :ref:`validation <valid-module>`, the frame :math:`F_{\F{init}}` is now on the top of the stack.
+   b. Assert: due to :ref:`validation <valid-module>`, the frame :math:`F` is now on the top of the stack.
 
    c. Let :math:`\reff_{\F{t}}^\ast` be the concatenation of :math:`\reff_{ti}` in index order.
 
@@ -557,15 +555,9 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
 
     c. Let :math:`(\reff_{\F{e}}^\ast)^\ast` be the concatenation of function element vectors :math:`\reff^\ast_i` in order of index :math:`i`.
 
-11. Pop the frame :math:`F_{\F{init}}` from the stack.
-
-12. Let :math:`\moduleinst` be a new module instance :ref:`allocated <alloc-module>` from :math:`\module` in store :math:`S` with imports :math:`\externval^n`, global initializer values :math:`\val_{\F{g}}^\ast`, table initializer values :math:`\reff_{\F{t}}^\ast`, and element segment contents :math:`(\reff_{\F{e}}^\ast)^\ast`, and let :math:`S'` be the extended store produced by module allocation.
-
-13. Let :math:`F` be the auxiliary :ref:`frame <syntax-frame>` :math:`\{ \AMODULE~\moduleinst, \ALOCALS~\epsilon \}`.
-
-14. Push the frame :math:`F` to the stack.
+11. Let :math:`\moduleinst` be a new module instance :ref:`allocated <alloc-module>` from :math:`\module` in store :math:`S` with imports :math:`\externval^n`, global initializer values :math:`\val_{\F{g}}^\ast`, table initializer values :math:`\reff_{\F{t}}^\ast`, and element segment contents :math:`(\reff_{\F{e}}^\ast)^\ast`, and let :math:`S'` be the extended store produced by module allocation.
 
-15. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode <syntax-elemmode>` is of the form :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{einstr}^\ast_i~\END \}`, do:
+12. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode <syntax-elemmode>` is of the form :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{einstr}^\ast_i~\END \}`, do:
 
     a. Let :math:`n` be the length of the vector :math:`\elem_i.\EINIT`.
 
@@ -579,11 +571,11 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
 
     f. :ref:`Execute <exec-elem.drop>` the instruction :math:`\ELEMDROP~i`.
 
-16. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode <syntax-elemmode>` is of the form :math:`\EDECLARATIVE`, do:
+13. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode <syntax-elemmode>` is of the form :math:`\EDECLARATIVE`, do:
 
     a. :ref:`Execute <exec-elem.drop>` the instruction :math:`\ELEMDROP~i`.
 
-17. For each :ref:`data segment <syntax-data>` :math:`\data_i` in :math:`\module.\MDATAS` whose :ref:`mode <syntax-datamode>` is of the form :math:`\DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{dinstr}^\ast_i~\END \}`, do:
+14. For each :ref:`data segment <syntax-data>` :math:`\data_i` in :math:`\module.\MDATAS` whose :ref:`mode <syntax-datamode>` is of the form :math:`\DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{dinstr}^\ast_i~\END \}`, do:
 
     a. Assert: :math:`\memidx_i` is :math:`0`.
 
@@ -599,15 +591,15 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
 
     g. :ref:`Execute <exec-data.drop>` the instruction :math:`\DATADROP~i`.
 
-18. If the :ref:`start function <syntax-start>` :math:`\module.\MSTART` is not empty, then:
+15. If the :ref:`start function <syntax-start>` :math:`\module.\MSTART` is not empty, then:
 
     a. Let :math:`\start` be the :ref:`start function <syntax-start>` :math:`\module.\MSTART`.
 
     b. :ref:`Execute <exec-call>` the instruction :math:`\CALL~\start.\SFUNC`.
 
-19. Assert: due to :ref:`validation <valid-module>`, the frame :math:`F` is now on the top of the stack.
+16. Assert: due to :ref:`validation <valid-module>`, the frame :math:`F` is now on the top of the stack.
 
-20. Pop the frame :math:`F` from the stack.
+17. Pop the frame :math:`F` from the stack.
 
 
 .. math::
@@ -658,7 +650,7 @@ where:
 
    Similarly, module :ref:`allocation <alloc-module>` and the :ref:`evaluation <exec-expr>` of :ref:`global <syntax-global>` and :ref:`table <syntax-table>` initializers as well as :ref:`element segments <syntax-elem>` are mutually recursive because the global initialization :ref:`values <syntax-val>` :math:`\val_{\F{g}}^\ast`, :math:`\reff_{\F{t}}`, and element segment contents :math:`(\reff^\ast)^\ast` are passed to the module allocator while depending on the module instance :math:`\moduleinst` and store :math:`S'` returned by allocation.
    Again, this recursion is just a specification device.
-   In practice, the initialization values can :ref:`be determined <exec-initvals>` beforehand by staging module allocation further such that first, the module's own :ref:`function instances <syntax-funcinst>` are pre-allocated in the store, then the initializer expressions are evaluated in order, allocating globals on the way, then the rest of the module instance is allocated, and finally the new function instances' :math:`\AMODULE` fields are set to that module instance.
+   In practice, the initialization values can :ref:`be determined <exec-initvals>` beforehand by staging module allocation such that first, the module's own :ref:`function instances <syntax-funcinst>` are pre-allocated in the store, then the initializer expressions are evaluated in order, allocating globals on the way, then the rest of the module instance is allocated, and finally the new function instances' :math:`\AMODULE` fields are set to that module instance.
    This is possible because :ref:`validation <valid-module>` ensures that initialization expressions cannot actually call a function, only take their reference.
 
    All failure conditions are checked before any observable mutation of the store takes place.

document/core/valid/matching.rst

@@ -453,6 +453,11 @@ A :ref:`defined type <syntax-deftype>` :math:`\deftype_1` matches a type :math:`
      C \vdashdeftypematch \deftype_1 \matchesdeftype \deftype_2
    }
 
+.. note::
+   Note that there is no explicit definition of type _equivalence_,
+   since it coincides with syntactic equality,
+   as used in the premise of the fomer rule above.
+
 
 .. index:: limits
 .. _match-limits:

interpreter/text/parse.mli

@@ -3,10 +3,10 @@ exception Syntax of Source.region * string
 module type S =
 sig
   type t
-  val parse : string -> Lexing.lexbuf -> t
-  val parse_file : string -> t
-  val parse_string : string -> t
-  val parse_channel : in_channel -> t
+  val parse : string -> Lexing.lexbuf -> t (* raises Syntax *)
+  val parse_file : string -> t (* raises Syntax *)
+  val parse_string : string -> t (* raises Syntax *)
+  val parse_channel : in_channel -> t (* raises Syntax *)
 end
 
 module Module : S with type t = Script.var option * Script.definition

interpreter/text/parser.mly

@@ -1504,13 +1504,14 @@ result :
   | LPAR REF_I31 RPAR { RefResult (RefTypePat I31HT) @@ at () }
   | LPAR REF_STRUCT RPAR { RefResult (RefTypePat StructHT) @@ at () }
   | LPAR REF_ARRAY RPAR { RefResult (RefTypePat ArrayHT) @@ at () }
-  | LPAR REF_NULL RPAR { RefResult NullPat @@ at () }
   | LPAR REF_FUNC RPAR { RefResult (RefTypePat FuncHT) @@ at () }
   | LPAR REF_EXTERN RPAR { RefResult (RefTypePat ExternHT) @@ at () }
+  | LPAR REF_NULL RPAR { RefResult NullPat @@ at () }
   | LPAR VEC_CONST VEC_SHAPE list(numpat) RPAR
     { if V128.num_lanes $3 <> List.length $4 then
         error (at ()) "wrong number of lane literals";
-      VecResult (VecPat (Value.V128 ($3, List.map (fun lit -> lit $3) $4))) @@ at () }
+      VecResult (VecPat
+        (Value.V128 ($3, List.map (fun lit -> lit $3) $4))) @@ at () }
 
 script :
   | list(cmd) EOF { $1 }

test/core/gc/array.wast

@@ -152,17 +152,24 @@
   (type $vec (array i8))
   (type $mvec (array (mut i8)))
 
-  (data $d "\00\01\02\03\04")
+  (data $d "\00\01\02\ff\04")
 
   (func $new (export "new") (result (ref $vec))
     (array.new_data $vec $d (i32.const 1) (i32.const 3))
   )
 
-  (func $get (param $i i32) (param $v (ref $vec)) (result i32)
+  (func $get_u (param $i i32) (param $v (ref $vec)) (result i32)
     (array.get_u $vec (local.get $v) (local.get $i))
   )
-  (func (export "get") (param $i i32) (result i32)
-    (call $get (local.get $i) (call $new))
+  (func (export "get_u") (param $i i32) (result i32)
+    (call $get_u (local.get $i) (call $new))
+  )
+
+  (func $get_s (param $i i32) (param $v (ref $vec)) (result i32)
+    (array.get_s $vec (local.get $v) (local.get $i))
+  )
+  (func (export "get_s") (param $i i32) (result i32)
+    (call $get_s (local.get $i) (call $new))
   )
 
   (func $set_get (param $i i32) (param $v (ref $mvec)) (param $y i32) (result i32)
@@ -186,11 +193,13 @@
 
 (assert_return (invoke "new") (ref.array))
 (assert_return (invoke "new") (ref.eq))
-(assert_return (invoke "get" (i32.const 0)) (i32.const 1))
+(assert_return (invoke "get_u" (i32.const 2)) (i32.const 0xff))
+(assert_return (invoke "get_s" (i32.const 2)) (i32.const -1))
 (assert_return (invoke "set_get" (i32.const 1) (i32.const 7)) (i32.const 7))
 (assert_return (invoke "len") (i32.const 3))
 
-(assert_trap (invoke "get" (i32.const 10)) "out of bounds array access")
+(assert_trap (invoke "get_u" (i32.const 10)) "out of bounds array access")
+(assert_trap (invoke "get_s" (i32.const 10)) "out of bounds array access")
 (assert_trap (invoke "set_get" (i32.const 10) (i32.const 7)) "out of bounds array access")
 
 (module
@@ -302,5 +311,5 @@
   )
 )
 
-(assert_trap (invoke "array.get-null") "null array")
-(assert_trap (invoke "array.set-null") "null array")
+(assert_trap (invoke "array.get-null") "null array reference")
+(assert_trap (invoke "array.set-null") "null array reference")

test/core/gc/struct.wast

@@ -152,8 +152,8 @@
   )
 )
 
-(assert_trap (invoke "struct.get-null") "null structure")
-(assert_trap (invoke "struct.set-null") "null structure")
+(assert_trap (invoke "struct.get-null") "null structure reference")
+(assert_trap (invoke "struct.set-null") "null structure reference")
 
 ;; Packed field instructions