diff --git a/document/core/appendix/changes.rst b/document/core/appendix/changes.rst index 56bb449202..b7b217da75 100644 --- a/document/core/appendix/changes.rst +++ b/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]_. diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index dc27f435b1..2adb12f5a0 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1341,47 +1341,43 @@ Where: 19. Assert: due to :ref:`validation `, the :ref:`array instance ` :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 `, the :ref:`field type ` :math:`\X{ft}` has a defined :ref:`bit width `. - a. Trap. - -21. Assert: due to :ref:`validation `, the :ref:`field type ` :math:`\X{ft}` has a defined :ref:`bit width `. +21. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :math:`\X{ft}` divided by eight. -22. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :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 ` sequence :math:`\datainst.\DIDATA[s \slice z]`. +24. Let :math:`b^\ast` be the :ref:`byte ` sequence :math:`\datainst.\DIDATA[s \slice z]`. -26. Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\X{ft})`. +25. Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\X{ft})`. -27. Assert: due to :ref:`validation `, :math:`\bytes_{\X{ft}}` is defined. +26. Assert: due to :ref:`validation `, :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 `, the :ref:`array instance ` :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 ` :math:`\eleminst.\EIELEM[s]`. +22. Let :math:`\reff'` be the :ref:`reference value ` :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] diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 895789ba23..9e73c97fe9 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -517,11 +517,9 @@ It is up to the :ref:`embedder ` to define how such conditions are rep .. _exec-initvals: -5. Let :math:`\moduleinst_{\F{init}}` be the auxiliary module :ref:`instance ` :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 ` :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 ` :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 ` initialization :ref:`values ` determined by :math:`\module` and :math:`\externval^n`. These may be calculated as follows. @@ -529,7 +527,7 @@ It is up to the :ref:`embedder ` to define how such conditions are rep i. Let :math:`\val_{\F{g}i}` be the result of :ref:`evaluating ` the initializer expression :math:`\global_i.\GINIT`. - b. Assert: due to :ref:`validation `, the frame :math:`F_{\F{init}}` is now on the top of the stack. + b. Assert: due to :ref:`validation `, 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 ` 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 `, the frame :math:`F_{\F{init}}` is now on the top of the stack. + b. Assert: due to :ref:`validation `, 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 ` 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 ` 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 ` :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 ` 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 ` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode ` is of the form :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{einstr}^\ast_i~\END \}`, do: +12. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode ` 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 ` to define how such conditions are rep f. :ref:`Execute ` the instruction :math:`\ELEMDROP~i`. -16. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode ` is of the form :math:`\EDECLARATIVE`, do: +13. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode ` is of the form :math:`\EDECLARATIVE`, do: a. :ref:`Execute ` the instruction :math:`\ELEMDROP~i`. -17. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATAS` whose :ref:`mode ` is of the form :math:`\DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{dinstr}^\ast_i~\END \}`, do: +14. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATAS` whose :ref:`mode ` 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 ` to define how such conditions are rep g. :ref:`Execute ` the instruction :math:`\DATADROP~i`. -18. If the :ref:`start function ` :math:`\module.\MSTART` is not empty, then: +15. If the :ref:`start function ` :math:`\module.\MSTART` is not empty, then: a. Let :math:`\start` be the :ref:`start function ` :math:`\module.\MSTART`. b. :ref:`Execute ` the instruction :math:`\CALL~\start.\SFUNC`. -19. Assert: due to :ref:`validation `, the frame :math:`F` is now on the top of the stack. +16. Assert: due to :ref:`validation `, 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 ` and the :ref:`evaluation ` of :ref:`global ` and :ref:`table ` initializers as well as :ref:`element segments ` are mutually recursive because the global initialization :ref:`values ` :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 ` beforehand by staging module allocation further such that first, the module's own :ref:`function instances ` 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 ` beforehand by staging module allocation such that first, the module's own :ref:`function instances ` 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 ` 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. diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst index 99614cffa9..0b160c2055 100644 --- a/document/core/valid/matching.rst +++ b/document/core/valid/matching.rst @@ -453,6 +453,11 @@ A :ref:`defined type ` :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: diff --git a/interpreter/text/parse.mli b/interpreter/text/parse.mli index e3d1e654fa..3a318683b6 100644 --- a/interpreter/text/parse.mli +++ b/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 diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 71ee2a929a..218a4c5c2b 100644 --- a/interpreter/text/parser.mly +++ b/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 } diff --git a/test/core/gc/array.wast b/test/core/gc/array.wast index f5888cb2d9..6ad95c0873 100644 --- a/test/core/gc/array.wast +++ b/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") diff --git a/test/core/gc/struct.wast b/test/core/gc/struct.wast index 7a3ce4fc89..6151fe100f 100644 --- a/test/core/gc/struct.wast +++ b/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