From cbdef5ec93681a0f883a104dc2c6dc28db5a7ee3 Mon Sep 17 00:00:00 2001 From: Carter Snook Date: Sun, 12 Mar 2023 09:49:36 -0500 Subject: [PATCH 01/43] chore(doc): fix some typos --- proposals/function-references/Overview.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md index 57947c5a33..944f81fadf 100644 --- a/proposals/function-references/Overview.md +++ b/proposals/function-references/Overview.md @@ -2,13 +2,13 @@ ## Introduction -This proposal adds function references that are typed and can be called directly. Unlike `funcref` and the existing `call_indirect` instruction, typed function references need not be stored into a table to be called (though they can). A typed function reference can be formed from any function index. +This proposal adds function references that are typed and can be called directly. Unlike `funcref` and the existing `call_indirect` instruction, typed function references do not need to be stored in a table to be called (though they can). A typed function reference can be formed from any function index. The proposal distinguished regular and nullable function reference. The former cannot be null, and a call through them does not require any runtime check. The proposal has instructions for producing and consuming (calling) function references. It also includes instruction for testing and converting between regular and nullable references. -Typed references have no canonical default value, because they cannot be null. To enable storing them in locals, which so far depend on default values for initialisation, the proposal also tracks the initialisation status of locals during validation. +Typed references have no canonical default value, because they cannot be null. To enable storing them in locals, which so far depend on default values for initialization, the proposal also tracks the initialization status of locals during validation. ### Motivation @@ -24,7 +24,7 @@ Typed references have no canonical default value, because they cannot be null. T ### Summary -* This proposal is based on the [reference types proposal](https://github.com/WebAssembly/reference-types)) +* This proposal is based on the [reference types proposal](https://github.com/WebAssembly/reference-types) * Add a new form of *typed reference type* `ref $t` and a nullable variant `(ref null $t)`, where `$t` is a type index; can be used as both a value type or an element type for tables @@ -38,7 +38,7 @@ Typed references have no canonical default value, because they cannot be null. T * Track initialisation status of locals during validation and only allow `local.get` after a `local.set/tee` in the same or a surrounding block. -* Add an optional initialiser expression to table definitions, for element types that do not have an implicit default value. +* Add an optional initializer expression to table definitions, for element types that do not have an implicit default value. ### Examples @@ -64,7 +64,7 @@ It is also possible to create a typed function table: ```wasm (table 0 (ref $i32-i32)) ``` -Such a table can neither contain `null` entries nor functions of another type. Any use of `call_indirect` on this table does hence avoid all runtime checks beyond the basic bounds check. By using multiple tables, each one can be given a homogeneous type. The table can be initialised with an initializer or by growing it. +Such a table can neither contain `null` entries nor functions of another type. Any use of `call_indirect` on this table does hence avoid all runtime checks beyond the basic bounds check. By using multiple tables, each one can be given a homogeneous type. The table can be initialized with an initializer or by growing it. Typed function references are a subtype of `funcref`, so they can also be used as untyped references. All previous uses of `ref.func` remain valid: ```wasm @@ -165,7 +165,7 @@ The following rules, now defined in terms of heap types, replace and extend the * Function-level locals must have a type that is defaultable. -* Table definitions with a type that is not defaultable must have an initialiser value. (Imports are not affected.) +* Table definitions with a type that is not defaultable must have an initializer value. (Imports are not affected.) #### Local Types @@ -283,7 +283,7 @@ A subsumption rule allows to go to a supertype for any instruction: ### Tables -Table definitions have an initialiser value: +Table definitions have an initializer value: * `(table )` is an extended form of table definition - `(table ) ok` iff ` ok` and ` : ` @@ -363,9 +363,9 @@ In addition to the rules for basic reference types: #### `Table` -* The `Table` constructor gets an additional optional argument `init` that is used to initialise the table slots. It defaults to `null`. A `TypeError` is produced if the argument is omitted and the table's element type is not defaultable. +* The `Table` constructor gets an additional optional argument `init` that is used to initialize the table slots. It defaults to `null`. A `TypeError` is produced if the argument is omitted and the table's element type is not defaultable. -* The `Table` method `grow` gets an additional optional argument `init` that is used to initialise the new table slots. It defaults to `null`. A `TypeError` is produced if the argument is omitted and the table's element type is not defaultable. +* The `Table` method `grow` gets an additional optional argument `init` that is used to initialize the new table slots. It defaults to `null`. A `TypeError` is produced if the argument is omitted and the table's element type is not defaultable. ### Type Reflection From b3b6053b3a73e06c148adbcc5fc38f2e3cd307de Mon Sep 17 00:00:00 2001 From: YiYing He Date: Fri, 20 Oct 2023 20:19:47 +0800 Subject: [PATCH 02/43] [test] Prevent from module name conflict when registering in wast. Signed-off-by: YiYing He --- test/core/gc/type-subtyping.wast | 58 ++++++++++++++++---------------- test/core/type-equivalence.wast | 28 +++++++-------- 2 files changed, 43 insertions(+), 43 deletions(-) diff --git a/test/core/gc/type-subtyping.wast b/test/core/gc/type-subtyping.wast index 1346a91d5a..a9022fc334 100644 --- a/test/core/gc/type-subtyping.wast +++ b/test/core/gc/type-subtyping.wast @@ -540,11 +540,11 @@ (rec (type $g2 (sub $f2 (func))) (type (struct))) (func (export "g") (type $g2)) ) -(register "M") +(register "M3") (module (rec (type $f1 (sub (func))) (type (struct (field (ref $f1))))) (rec (type $g1 (sub $f1 (func))) (type (struct))) - (func (import "M" "g") (type $g1)) + (func (import "M3" "g") (type $g1)) ) (module @@ -556,7 +556,7 @@ ) (func (export "g") (type $g2)) ) -(register "M") +(register "M4") (module (rec (type $f1 (sub (func))) (type $s1 (sub (struct (field (ref $f1)))))) (rec (type $f2 (sub (func))) (type $s2 (sub (struct (field (ref $f2)))))) @@ -564,7 +564,7 @@ (type $g1 (sub $f1 (func))) (type (sub $s1 (struct (field (ref $f1) (ref $f1) (ref $f2) (ref $f2) (ref $g1))))) ) - (func (import "M" "g") (type $g1)) + (func (import "M4" "g") (type $g1)) ) (module @@ -573,12 +573,12 @@ (rec (type $g2 (sub $f2 (func))) (type (struct))) (func (export "g") (type $g2)) ) -(register "M") +(register "M5") (assert_unlinkable (module (rec (type $f1 (sub (func))) (type (struct (field (ref $f1))))) (rec (type $g1 (sub $f1 (func))) (type (struct))) - (func (import "M" "g") (type $g1)) + (func (import "M5" "g") (type $g1)) ) "incompatible import" ) @@ -589,12 +589,12 @@ (rec (type $g (sub $f1 (func))) (type (struct))) (func (export "g") (type $g)) ) -(register "M") +(register "M6") (module (rec (type $f1 (sub (func))) (type (struct (field (ref $f1))))) (rec (type $f2 (sub (func))) (type (struct (field (ref $f2))))) (rec (type $g (sub $f1 (func))) (type (struct))) - (func (import "M" "g") (type $f1)) + (func (import "M6" "g") (type $f1)) ) (module @@ -607,7 +607,7 @@ (rec (type $h (sub $g2 (func))) (type (struct))) (func (export "h") (type $h)) ) -(register "M") +(register "M7") (module (rec (type $f1 (sub (func))) (type $s1 (sub (struct (field (ref $f1)))))) (rec (type $f2 (sub (func))) (type $s2 (sub (struct (field (ref $f2)))))) @@ -616,8 +616,8 @@ (type (sub $s1 (struct (field (ref $f1) (ref $f1) (ref $f2) (ref $f2) (ref $g1))))) ) (rec (type $h (sub $g1 (func))) (type (struct))) - (func (import "M" "h") (type $f1)) - (func (import "M" "h") (type $g1)) + (func (import "M7" "h") (type $f1)) + (func (import "M7" "h") (type $g1)) ) @@ -627,14 +627,14 @@ (func (export "f11") (type $f11) (unreachable)) (func (export "f12") (type $f12) (unreachable)) ) -(register "M") +(register "M8") (module (rec (type $f11 (sub (func (result (ref func))))) (type $f12 (sub $f11 (func (result (ref $f11)))))) (rec (type $f21 (sub (func (result (ref func))))) (type $f22 (sub $f21 (func (result (ref $f21)))))) - (func (import "M" "f11") (type $f11)) - (func (import "M" "f11") (type $f21)) - (func (import "M" "f12") (type $f12)) - (func (import "M" "f12") (type $f22)) + (func (import "M8" "f11") (type $f11)) + (func (import "M8" "f11") (type $f21)) + (func (import "M8" "f12") (type $f12)) + (func (import "M8" "f12") (type $f22)) ) (module @@ -645,20 +645,20 @@ (func (export "g11") (type $g11) (unreachable)) (func (export "g12") (type $g12) (unreachable)) ) -(register "M") +(register "M9") (module (rec (type $f11 (sub (func (result (ref func))))) (type $f12 (sub $f11 (func (result (ref $f11)))))) (rec (type $f21 (sub (func (result (ref func))))) (type $f22 (sub $f21 (func (result (ref $f21)))))) (rec (type $g11 (sub $f11 (func (result (ref func))))) (type $g12 (sub $g11 (func (result (ref $g11)))))) (rec (type $g21 (sub $f21 (func (result (ref func))))) (type $g22 (sub $g21 (func (result (ref $g21)))))) - (func (import "M" "g11") (type $f11)) - (func (import "M" "g11") (type $f21)) - (func (import "M" "g12") (type $f11)) - (func (import "M" "g12") (type $f21)) - (func (import "M" "g11") (type $g11)) - (func (import "M" "g11") (type $g21)) - (func (import "M" "g12") (type $g12)) - (func (import "M" "g12") (type $g22)) + (func (import "M9" "g11") (type $f11)) + (func (import "M9" "g11") (type $f21)) + (func (import "M9" "g12") (type $f11)) + (func (import "M9" "g12") (type $f21)) + (func (import "M9" "g11") (type $g11)) + (func (import "M9" "g11") (type $g21)) + (func (import "M9" "g12") (type $g12)) + (func (import "M9" "g12") (type $g22)) ) (module @@ -666,11 +666,11 @@ (rec (type $f21 (sub (func))) (type $f22 (sub $f11 (func)))) (func (export "f") (type $f21)) ) -(register "M") +(register "M10") (assert_unlinkable (module (rec (type $f11 (sub (func))) (type $f12 (sub $f11 (func)))) - (func (import "M" "f") (type $f11)) + (func (import "M10" "f") (type $f11)) ) "incompatible import" ) @@ -681,12 +681,12 @@ (rec (type $f21 (sub (func))) (type $f22 (sub $f11 (func)))) (func (export "f") (type $f21)) ) -(register "M") +(register "M11") (assert_unlinkable (module (rec (type $f01 (sub (func))) (type $f02 (sub $f01 (func)))) (rec (type $f11 (sub (func))) (type $f12 (sub $f01 (func)))) - (func (import "M" "f") (type $f11)) + (func (import "M11" "f") (type $f11)) ) "incompatible import" ) diff --git a/test/core/type-equivalence.wast b/test/core/type-equivalence.wast index 8280779644..b3d1151d22 100644 --- a/test/core/type-equivalence.wast +++ b/test/core/type-equivalence.wast @@ -234,10 +234,10 @@ (rec (type $t1 (func (param i32 (ref $t1))))) (func (export "f") (param (ref $t1))) ) -(register "M") +(register "Mr1") (module (rec (type $t2 (func (param i32 (ref $t2))))) - (func (import "M" "f") (param (ref $t2))) + (func (import "Mr1" "f") (param (ref $t2))) ) @@ -253,16 +253,16 @@ (func (export "f2") (param (ref $t2))) (func (export "f3") (param (ref $t3))) ) -(register "M") +(register "Mr2") (module (rec (type $t1 (func (param i32 (ref $t1)))) (type $t2 (func (param i32 (ref $t3)))) (type $t3 (func (param i32 (ref $t2)))) ) - (func (import "M" "f1") (param (ref $t1))) - (func (import "M" "f2") (param (ref $t2))) - (func (import "M" "f3") (param (ref $t3))) + (func (import "Mr2" "f1") (param (ref $t1))) + (func (import "Mr2" "f2") (param (ref $t2))) + (func (import "Mr2" "f3") (param (ref $t3))) ) (module @@ -275,16 +275,16 @@ (func (export "f2") (param (ref $t2))) (func (export "f3") (param (ref $t3))) ) -(register "M") +(register "Mr3") (module (rec (type $t1 (func (param i32 (ref $t3)))) (type $t2 (func (param i32 (ref $t1)))) (type $t3 (func (param i32 (ref $t2)))) ) - (func (import "M" "f1") (param (ref $t1))) - (func (import "M" "f2") (param (ref $t2))) - (func (import "M" "f3") (param (ref $t3))) + (func (import "Mr3" "f1") (param (ref $t1))) + (func (import "Mr3" "f2") (param (ref $t2))) + (func (import "Mr3" "f3") (param (ref $t3))) ) (module @@ -304,7 +304,7 @@ (func (export "f2") (param (ref $t2))) (func (export "f3") (param (ref $t3))) ) -(register "M") +(register "Mr4") (module (rec (type $t1 (func (param i32 (ref $u1)))) @@ -318,7 +318,7 @@ (type $u3 (func (param f32 (ref $t2)))) ) - (func (import "M" "f1") (param (ref $t1))) - (func (import "M" "f2") (param (ref $t2))) - (func (import "M" "f3") (param (ref $t3))) + (func (import "Mr4" "f1") (param (ref $t1))) + (func (import "Mr4" "f2") (param (ref $t2))) + (func (import "Mr4" "f3") (param (ref $t3))) ) From b39baf7795a8a6d969ae713ce2088ef0fb8c8ebe Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 24 Oct 2023 18:11:01 +0200 Subject: [PATCH 03/43] [spec] Fix definition of iextend (#1696) --- document/core/exec/numerics.rst | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/document/core/exec/numerics.rst b/document/core/exec/numerics.rst index f9eae6b9d0..85d3dbd00c 100644 --- a/document/core/exec/numerics.rst +++ b/document/core/exec/numerics.rst @@ -715,11 +715,13 @@ The integer result of predicates -- i.e., :ref:`tests ` and :ref: :math:`\iextendMs_N(i)` ....................... -* Return :math:`\extends_{M,N}(i)`. +* Let :math:`j` be the result of computing :math:`\wrap_{N,M}(i)`. + +* Return :math:`\extends_{M,N}(j)`. .. math:: \begin{array}{lll@{\qquad}l} - \iextendMs_{N}(i) &=& \extends_{M,N}(i) \\ + \iextendMs_{N}(i) &=& \extends_{M,N}(\wrap_{N,M}(i)) \\ \end{array} From 43d405f5301adefb823b443c6fb9bb6093b1e1a7 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 25 Oct 2023 21:55:07 +0200 Subject: [PATCH 04/43] [spec/interpreter/test] Align definition of newline with Unicode recommendation (#1684) --- document/core/text/lexical.rst | 10 ++++++---- document/core/util/macros.def | 1 + interpreter/Makefile | 2 +- interpreter/text/lexer.mll | 24 +++++++++++++----------- test/core/comments.wast | Bin 772 -> 1316 bytes 5 files changed, 21 insertions(+), 16 deletions(-) diff --git a/document/core/text/lexical.rst b/document/core/text/lexical.rst index 1dd34c8635..4584b0c424 100644 --- a/document/core/text/lexical.rst +++ b/document/core/text/lexical.rst @@ -85,7 +85,9 @@ The allowed formatting characters correspond to a subset of the |ASCII|_ *format \production{white space} & \Tspace &::=& (\text{~~} ~|~ \Tformat ~|~ \Tcomment)^\ast \\ \production{format} & \Tformat &::=& - \unicode{09} ~|~ \unicode{0A} ~|~ \unicode{0D} \\ + \Tnewline ~|~ \unicode{09} \\ + \production{newline} & \Tnewline &::=& + \unicode{0A} ~|~ \unicode{0D} ~|~ \unicode{0D}~\unicode{0A} \\ \end{array} The only relevance of white space is to separate :ref:`tokens `. It is otherwise ignored. @@ -107,13 +109,13 @@ Block comments can be nested. \production{comment} & \Tcomment &::=& \Tlinecomment ~|~ \Tblockcomment \\ \production{line comment} & \Tlinecomment &::=& - \Tcommentd~~\Tlinechar^\ast~~(\unicode{0A} ~|~ \T{eof}) \\ + \Tcommentd~~\Tlinechar^\ast~~(\Tnewline ~|~ \T{eof}) \\ \production{line character} & \Tlinechar &::=& - c{:}\Tchar & (\iff c \neq \unicode{0A}) \\ + c{:}\Tchar & (\iff c \neq \unicode{0A} \land c \neq \unicode{0D}) \\ \production{block comment} & \Tblockcomment &::=& \Tcommentl~~\Tblockchar^\ast~~\Tcommentr \\ \production{block character} & \Tblockchar &::=& - c{:}\Tchar & (\iff c \neq \text{;} \wedge c \neq \text{(}) \\ &&|& + c{:}\Tchar & (\iff c \neq \text{;} \land c \neq \text{(}) \\ &&|& \text{;} & (\iff~\mbox{the next character is not}~\text{)}) \\ &&|& \text{(} & (\iff~\mbox{the next character is not}~\text{;}) \\ &&|& \Tblockcomment \\ diff --git a/document/core/util/macros.def b/document/core/util/macros.def index df4af62f83..5e7a4889b2 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -700,6 +700,7 @@ .. |Tchar| mathdef:: \xref{text/lexical}{text-char}{\T{char}} .. |Tspace| mathdef:: \xref{text/lexical}{text-space}{\T{space}} .. |Tformat| mathdef:: \xref{text/lexical}{text-format}{\T{format}} +.. |Tnewline| mathdef:: \xref{text/lexical}{text-newline}{\T{newline}} .. |Ttoken| mathdef:: \xref{text/lexical}{text-token}{\T{token}} .. |Tkeyword| mathdef:: \xref{text/lexical}{text-keyword}{\T{keyword}} diff --git a/interpreter/Makefile b/interpreter/Makefile index 5939f838ec..dfd9064bbf 100644 --- a/interpreter/Makefile +++ b/interpreter/Makefile @@ -33,7 +33,7 @@ zip: $(ZIP) # Building -.PHONY: $(NAME) $(JSLIB) +.PHONY: $(NAME) $(JSLIB) $(NAME): rm -f $@ diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll index d9a12b5d21..34099e849f 100644 --- a/interpreter/text/lexer.mll +++ b/interpreter/text/lexer.mll @@ -27,9 +27,9 @@ let string s = while !i < String.length s - 1 do let c = if s.[!i] <> '\\' then s.[!i] else match (incr i; s.[!i]) with - | 'n' -> '\n' - | 'r' -> '\r' - | 't' -> '\t' + | 'n' -> '\x0a' + | 'r' -> '\x0d' + | 't' -> '\x09' | '\\' -> '\\' | '\'' -> '\'' | '\"' -> '\"' @@ -61,10 +61,12 @@ let letter = ['a'-'z''A'-'Z'] let symbol = ['+''-''*''/''\\''^''~''=''<''>''!''?''@''#''$''%''&''|'':''`''.''\''] -let space = [' ''\t''\n''\r'] +let ascii_newline = ['\x0a''\x0d'] +let newline = ascii_newline | "\x0a\x0d" +let space = [' ''\x09''\x0a''\x0d'] let control = ['\x00'-'\x1f'] # space let ascii = ['\x00'-'\x7f'] -let ascii_no_nl = ascii # '\x0a' +let ascii_no_nl = ascii # ascii_newline let utf8cont = ['\x80'-'\xbf'] let utf8enc = ['\xc2'-'\xdf'] utf8cont @@ -127,8 +129,8 @@ rule token = parse | float as s { FLOAT s } | string as s { STRING (string s) } - | '"'character*('\n'|eof) { error lexbuf "unclosed string literal" } - | '"'character*['\x00'-'\x09''\x0b'-'\x1f''\x7f'] + | '"'character*(newline|eof) { error lexbuf "unclosed string literal" } + | '"'character*(control#ascii_newline) { error lexbuf "illegal control character in string literal" } | '"'character*'\\'_ { error_nest (Lexing.lexeme_end_p lexbuf) lexbuf "illegal escape" } @@ -698,11 +700,11 @@ rule token = parse | id as s { VAR s } | ";;"utf8_no_nl*eof { EOF } - | ";;"utf8_no_nl*'\n' { Lexing.new_line lexbuf; token lexbuf } + | ";;"utf8_no_nl*newline { Lexing.new_line lexbuf; token lexbuf } | ";;"utf8_no_nl* { token lexbuf (* causes error on following position *) } | "(;" { comment (Lexing.lexeme_start_p lexbuf) lexbuf; token lexbuf } - | space#'\n' { token lexbuf } - | '\n' { Lexing.new_line lexbuf; token lexbuf } + | space#ascii_newline { token lexbuf } + | newline { Lexing.new_line lexbuf; token lexbuf } | eof { EOF } | reserved { unknown lexbuf } @@ -713,7 +715,7 @@ rule token = parse and comment start = parse | ";)" { () } | "(;" { comment (Lexing.lexeme_start_p lexbuf) lexbuf; comment start lexbuf } - | '\n' { Lexing.new_line lexbuf; comment start lexbuf } + | newline { Lexing.new_line lexbuf; comment start lexbuf } | utf8_no_nl { comment start lexbuf } | eof { error_nest start lexbuf "unclosed comment" } | _ { error lexbuf "malformed UTF-8 encoding" } diff --git a/test/core/comments.wast b/test/core/comments.wast index c291370fa72141c02e627c6edf0442bd409129cf..5ef64a6c1e60e898c86f51a53dcb11201e5025f8 100644 GIT binary patch literal 1316 zcmbtTJ8u**5au0X5D?yPMqAkuhwf2OxI#z~X=p&AISE~MXNiT+2CtXoD*gi%qM_zL z(B%i^FEGBn_4@7<34#mnjOUy08_#&9gtu6E$nA8B#zQqTesaK=l#7#K#>E)WN@6^5 zrnaaxc0tjZ#32Gt*r3_DWQ>Os+80udv*N9~v6e+Hk1G%pndsIMd$#PYx^thZd-3Mw z&JOhZy}|ZVc)m@9r%sb0%wH*Vg#edq4I`wt#Idi>;TAf`-H zYu($Od4$qxZTGPNMNKW##G{_U?hMcrJzMtLUKgmS{|AyLWbsP6V`qu`)^seW&TY#(k{}g2UW? zFv=@yV$JZmwjQbSjF+{^f#bm^>pYCJaxl&WaEDc`J*d%8WC2EZB>P!z4gFe!_KZ{( z_ZaslEzY5@ok{US(Im8>##>V!o=~~?Z{^WRmD?Lpd;aR$Vf2%#Lg(K{y!m23B2eQ) S-@7JL(~idu{{cH%$NmAx5ppO1 delta 14 VcmZ3&)xx&HfRT}RvmxVUMgShv1K|Jw From 32b1643f94a66f082b6f28598c8ddc02fee8b62f Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Wed, 25 Oct 2023 14:11:54 -0700 Subject: [PATCH 05/43] [spec] fix table binary formatting --- document/core/binary/modules.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst index 9449f6f7fd..59c7c2540a 100644 --- a/document/core/binary/modules.rst +++ b/document/core/binary/modules.rst @@ -212,7 +212,7 @@ It decodes into a vector of :ref:`tables ` that represent the |MTA \production{table} & \Btable &::=& \X{tt}{:}\Btabletype &\Rightarrow& \{ \TTYPE~\X{tt}, \TINIT~(\REFNULL~\X{ht}) \} - \qquad \iff \X{tt} = \limits~(\REF~\NULL^?~\X{ht}) \\ + \qquad \iff \X{tt} = \limits~(\REF~\NULL^?~\X{ht}) \\ &&|& \hex{40}~~\hex{00}~~\X{tt}{:}\Btabletype~~e{:}\Bexpr &\Rightarrow& \{ \TTYPE~\X{tt}, \TINIT~e \} \\ \end{array} From 1fff7237974ef731c996032fc21fc6100eec40f6 Mon Sep 17 00:00:00 2001 From: DJ Date: Thu, 26 Oct 2023 14:02:15 +0900 Subject: [PATCH 06/43] [spec] Fix spec for execution of struct.new and array.new_fixed --- document/core/exec/instructions.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index a30c4388bf..d367a1b7dc 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -455,7 +455,7 @@ Reference Instructions 12. Append :math:`\X{si}` to :math:`S.\SSTRUCTS`. -13. Return the :ref:`structure reference ` :math:`\REFSTRUCTADDR~a`. +13. Push the :ref:`structure reference ` :math:`\REFSTRUCTADDR~a` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} @@ -724,14 +724,14 @@ Reference Instructions 11. Append :math:`\X{ai}` to :math:`S.\SARRAYS`. -12. Return the :ref:`array reference ` :math:`\REFARRAYADDR~a`. +12. Push the :ref:`array reference ` :math:`\REFARRAYADDR~a` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} S; F; \val^n~(\ARRAYNEWFIXED~x~n) &\stepto& S'; F; (\REFARRAYADDR~|S.\SARRAYS|) \\&& \begin{array}[t]{@{}r@{~}l@{}} - (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}^n \\ + (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ \land & \X{ai} = \{\AITYPE~F.\AMODULE.\MITYPES[x], \AIFIELDS~(\packval_{\X{ft}}(\val))^n\} \\ \land & S' = S \with \SARRAYS = S.\SARRAYS~\X{ai}) \end{array} \\ From 8d39c795d2770277db0b77dcd20ba21ba975e0d9 Mon Sep 17 00:00:00 2001 From: DJ Date: Thu, 26 Oct 2023 14:28:26 +0900 Subject: [PATCH 07/43] [spec] Fix typos in execution semantics of br_on_cast / br_on_cast_fail --- document/core/exec/instructions.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index d367a1b7dc..9f19a15eba 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -4139,10 +4139,10 @@ Control Instructions .. math:: \begin{array}{lcl@{\qquad}l} - S; \reff~(\BRONCAST~l~\X{rt}_1~X{rt}_2) &\stepto& \reff~(\BR~l) + S; F; \reff~(\BRONCAST~l~\X{rt}_1~\X{rt}_2) &\stepto& \reff~(\BR~l) & (\iff S \vdashval \reff : \X{rt} \land \vdashreftypematch \X{rt} \matchesreftype \insttype_{F.\AMODULE}(\X{rt}_2)) \\ - S; \reff~(\BRONCAST~l~\X{rt}_1~\X{rt}_2) &\stepto& \reff + S; F; \reff~(\BRONCAST~l~\X{rt}_1~\X{rt}_2) &\stepto& \reff & (\otherwise) \\ \end{array} @@ -4174,10 +4174,10 @@ Control Instructions .. math:: \begin{array}{lcl@{\qquad}l} - S; \reff~(\BRONCASTFAIL~l~\X{rt}_1~X{rt}_2) &\stepto& \reff + S; F; \reff~(\BRONCASTFAIL~l~\X{rt}_1~\X{rt}_2) &\stepto& \reff & (\iff S \vdashval \reff : \X{rt} \land \vdashreftypematch \X{rt} \matchesreftype \insttype_{F.\AMODULE}(\X{rt}_2)) \\ - S; \reff~(\BRONCASTFAIL~l~\X{rt}_1~\X{rt}_2) &\stepto& \reff~(\BR~l) + S; F; \reff~(\BRONCASTFAIL~l~\X{rt}_1~\X{rt}_2) &\stepto& \reff~(\BR~l) & (\otherwise) \\ \end{array} From 1fc73f40b9ba384181cc237dd51e8142dadda6ff Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sun, 29 Oct 2023 21:37:47 +0100 Subject: [PATCH 08/43] [spec] Fix typing of functions --- document/core/exec/values.rst | 40 ++++++++++++++++++++++++++++ document/core/syntax/types.rst | 2 +- document/core/valid/conventions.rst | 4 +-- document/core/valid/instructions.rst | 24 +++++++---------- document/core/valid/modules.rst | 36 ++++++++++++------------- 5 files changed, 70 insertions(+), 36 deletions(-) diff --git a/document/core/exec/values.rst b/document/core/exec/values.rst index 56e42b6043..6b19fcef38 100644 --- a/document/core/exec/values.rst +++ b/document/core/exec/values.rst @@ -186,6 +186,26 @@ The following auxiliary typing rules specify this typing relation relative to a S \vdashval \REFEXTERN~\reff : \REF~\NULL^?~\EXTERN } +Subsumption +........... + +* The value must be valid with some value type :math:`t`. + +* The value type :math:`t` :ref:`matches ` another :ref:`valid ` type :math:`t'`. + +* Then the value is valid with type :math:`t'`. + +.. math:: + \frac{ + S \vdashval \val : t + \qquad + \vdashvaltype t' \ok + \qquad + \vdashvaltypematch t \matchesvaltype t' + }{ + S \vdashval \val : t' + } + .. index:: external value, external type, validation, import, store .. _valid-externval: @@ -264,3 +284,23 @@ The following auxiliary typing rules specify this typing relation relative to a }{ S \vdashexternval \EVGLOBAL~a : \ETGLOBAL~S.\SGLOBALS[a].\GITYPE } + +Subsumption +........... + +* The external value must be valid with some external type :math:`\X{et}`. + +* The external type :math:`\X{et}` :ref:`matches ` another :ref:`valid ` type :math:`\X{et'}`. + +* Then the external value is valid with type :math:`\X{et'}`. + +.. math:: + \frac{ + S \vdashexternval \externval : \X{et} + \qquad + \vdashexterntype \X{et'} \ok + \qquad + \vdashexterntypematch \X{et} \matchesexterntype \X{et'} + }{ + S \vdashexternval \externval : \X{et'} + } diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index c2f6a4323b..13c2495a27 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -451,7 +451,7 @@ Conventions The following auxiliary notation is defined for sequences of external types. It filters out entries of a specific kind in an order-preserving fashion: -* :math:`\etfuncs(\externtype^\ast) = [\functype ~|~ (\ETFUNC~\functype) \in \externtype^\ast]` +* :math:`\etfuncs(\externtype^\ast) = [\deftype ~|~ (\ETFUNC~\deftype) \in \externtype^\ast]` * :math:`\ettables(\externtype^\ast) = [\tabletype ~|~ (\ETTABLE~\tabletype) \in \externtype^\ast]` diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index c39c8fc826..e86f1d661b 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -249,7 +249,7 @@ Validity of an individual definition is specified relative to a *context*, which collects relevant information about the surrounding :ref:`module ` and the definitions in scope: * *Types*: the list of :ref:`types ` defined in the current module. -* *Functions*: the list of :ref:`functions ` declared in the current module, represented by their :ref:`function type `. +* *Functions*: the list of :ref:`functions ` declared in the current module, represented by a :ref:`defined type ` that :ref:`expands ` to their :ref:`function type `. * *Tables*: the list of :ref:`tables ` declared in the current module, represented by their :ref:`table type `. * *Memories*: the list of :ref:`memories ` declared in the current module, represented by their :ref:`memory type `. * *Globals*: the list of :ref:`globals ` declared in the current module, represented by their :ref:`global type `. @@ -272,7 +272,7 @@ More concretely, contexts are defined as :ref:`records ` :math: \production{context} & C &::=& \begin{array}[t]{l@{~}ll} \{ & \CTYPES & \deftype^\ast, \\ - & \CFUNCS & \functype^\ast, \\ + & \CFUNCS & \deftype^\ast, \\ & \CTABLES & \tabletype^\ast, \\ & \CMEMS & \memtype^\ast, \\ & \CGLOBALS & \globaltype^\ast, \\ diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 2d76bf1a0a..f5ad69aa35 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -189,19 +189,19 @@ Reference Instructions * The function :math:`C.\CFUNCS[x]` must be defined in the context. -* Let :math:`y` be the :ref:`type index ` :math:`C.\CFUNCS[x]`. +* Let :math:`\X{dt}` be the :ref:`defined type ` :math:`C.\CFUNCS[x]`. * The :ref:`function index ` :math:`x` must be contained in :math:`C.\CREFS`. -* The instruction is valid with type :math:`[] \to [(\REF~y)]`. +* The instruction is valid with type :math:`[] \to [(\REF~\X{dt})]`. .. math:: \frac{ - C.\CFUNCS[x] = y + C.\CFUNCS[x] = \X{dt} \qquad x \in C.\CREFS }{ - C \vdashinstr \REFFUNC~x : [] \to [(\REF~y)] + C \vdashinstr \REFFUNC~x : [] \to [(\REF~\X{dt})] } .. _valid-ref.is_null: @@ -2166,17 +2166,13 @@ Control Instructions * The function :math:`C.\CFUNCS[x]` must be defined in the context. -* Let :math:`y` be the :ref:`type index ` :math:`C.\CFUNCS[x]`. - -* Assert: The type :math:`C.\CTYPES[y]` is defined in the context. - -* Let :math:`[t_1^\ast] \toF [t_2^\ast]` be the :ref:`function type ` :math:`C.\CTYPES[y]`. +* The :ref:`expansion ` of :math:`C.\CFUNCS[x]` must be a :ref:`function type ` :math:`\TFUNC~[t_1^\ast] \toF [t_2^\ast]`. * Then the instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`. .. math:: \frac{ - C.\CTYPES[C.\CFUNCS[x]] = [t_1^\ast] \toF [t_2^\ast] + \expanddt(C.\CFUNCS[x]) = \TFUNC~[t_1^\ast] \toF [t_2^\ast] }{ C \vdashinstr \CALL~x : [t_1^\ast] \to [t_2^\ast] } @@ -2189,13 +2185,13 @@ Control Instructions * The type :math:`C.\CTYPES[x]` must be defined in the context. -* Let :math:`[t_1^\ast] \toF [t_2^\ast]` be the :ref:`function type ` :math:`C.\CTYPES[x]`. +* The :ref:`expansion ` of :math:`C.\CFUNCS[x]` must be a :ref:`function type ` :math:`\TFUNC~[t_1^\ast] \toF [t_2^\ast]`. * Then the instruction is valid with type :math:`[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]`. .. math:: \frac{ - C.\CTYPES[x] = [t_1^\ast] \toF [t_2^\ast] + \expanddt(C.\CTYPES[x]) = \TFUNC~[t_1^\ast] \toF [t_2^\ast] }{ C \vdashinstr \CALLREF~x : [t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast] } @@ -2239,7 +2235,7 @@ Control Instructions * The function :math:`C.\CFUNCS[x]` must be defined in the context. -* Let :math:`[t_1^\ast] \toF [t_2^\ast]` be the :ref:`function type ` :math:`C.\CFUNCS[x]`. +* The :ref:`expansion ` of :math:`C.\CFUNCS[x]` must be a :ref:`function type ` :math:`\TFUNC~[t_1^\ast] \toF [t_2^\ast]`. * The :ref:`result type ` :math:`[t_2^\ast]` must :ref:`match ` :math:`C.\CRETURN`. @@ -2247,7 +2243,7 @@ Control Instructions .. math:: \frac{ - C.\CFUNCS[x] = [t_1^\ast] \toF [t_2^\ast] + \expanddt(C.\CFUNCS[x]) = \TFUNC~[t_1^\ast] \toF [t_2^\ast] \qquad C \vdashresulttypematch [t_2^\ast] \matchesresulttype C.\CRETURN }{ diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index d46704a56c..fd93a04738 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -70,7 +70,7 @@ The sequence of :ref:`types ` defined in a module is validated incr Functions ~~~~~~~~~ -Functions :math:`\func` are classified by :ref:`type indices ` referring to :ref:`function types ` of the form :math:`[t_1^\ast] \toF [t_2^\ast]`. +Functions :math:`\func` are classified by :ref:`defined types ` that :ref:`expand ` to :ref:`function types ` of the form :math:`\TFUNC~[t_1^\ast] \toF [t_2^\ast]`. :math:`\{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \}` @@ -98,7 +98,7 @@ Functions :math:`\func` are classified by :ref:`type indices ` r * Under the context :math:`C'`, the expression :math:`\expr` must be valid with type :math:`[t_2^\ast]`. -* Then the function definition is valid with type :math:`[t_1^\ast] \toF [t_2^\ast]`. +* Then the function definition is valid with type :math:`C.\CTYPES[x]`. .. math:: \frac{ @@ -108,7 +108,7 @@ Functions :math:`\func` are classified by :ref:`type indices ` r \qquad C,\CLOCALS\,(\SET~t_1)^\ast~(\init~t)^\ast,\CLABELS~[t_2^\ast],\CRETURN~[t_2^\ast] \vdashexpr \expr : [t_2^\ast] }{ - C \vdashfunc \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : x + C \vdashfunc \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : C.\CTYPES[x] } @@ -466,18 +466,14 @@ Start function declarations :math:`\start` are not classified by any type. * The function :math:`C.\CFUNCS[x]` must be defined in the context. -* Let :math:`y` be the :ref:`type index ` :math:`C.\CFUNCS[x]`. - -* Assert: The type :math:`C.\CTYPES[y]` is defined in the context. - -* The type :math:`C.\CTYPES[y]` must be the :ref:`function type ` :math:`\TFUNC~[] \toF []`. +* The :ref:`expansion ` of :math:`C.\CFUNCS[x]` must be a :ref:`function type ` :math:`\TFUNC~[] \toF []`. * Then the start function is valid. .. math:: \frac{ - C.\CTYPES[C.\CFUNCS[x]] = \TFUNC~[] \toF [] + \expanddt(C.\CFUNCS[x]) = \TFUNC~[] \toF [] }{ C \vdashstart \{ \SFUNC~x \} \ok } @@ -515,13 +511,15 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi * The function :math:`C.\CFUNCS[x]` must be defined in the context. -* Then the export description is valid with :ref:`external type ` :math:`\ETFUNC~C.\CFUNCS[x]`. +* Let :math:`\X{dt}` be the :ref:`defined type ` :math:`C.\CFUNCS[x]`. + +* Then the export description is valid with :ref:`external type ` :math:`\ETFUNC~\X{dt}`. .. math:: \frac{ - C.\CFUNCS[x] = \functype + C.\CFUNCS[x] = \X{dt} }{ - C \vdashexportdesc \EDFUNC~x : \ETFUNC~(\TFUNC~\functype) + C \vdashexportdesc \EDFUNC~x : \ETFUNC~\X{dt} } @@ -683,8 +681,8 @@ The :ref:`external types ` classifying a module may contain f * :math:`C.\CTYPES` is :math:`C_0.\CTYPES`, - * :math:`C.\CFUNCS` is :math:`\etfuncs(\X{it}^\ast)` concatenated with :math:`\X{ft}^\ast`, - with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :ref:`function types ` :math:`\X{ft}^\ast` as determined below, + * :math:`C.\CFUNCS` is :math:`\etfuncs(\X{it}^\ast)` concatenated with :math:`\X{dt}^\ast`, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :ref:`defined types ` :math:`\X{dt}^\ast` as determined below, * :math:`C.\CTABLES` is :math:`\ettables(\X{it}^\ast)` concatenated with :math:`\X{tt}^\ast`, with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :ref:`table types ` :math:`\X{tt}^\ast` as determined below, @@ -732,7 +730,7 @@ The :ref:`external types ` classifying a module may contain f * Under the context :math:`C`: * For each :math:`\func_i` in :math:`\module.\MFUNCS`, - the definition :math:`\func_i` must be :ref:`valid ` with a :ref:`function type ` :math:`\X{ft}_i`. + the definition :math:`\func_i` must be :ref:`valid ` with a :ref:`defined type ` :math:`\X{dt}_i`. * For each :math:`\elem_i` in :math:`\module.\MELEMS`, the segment :math:`\elem_i` must be :ref:`valid ` with :ref:`reference type ` :math:`\X{rt}_i`. @@ -749,7 +747,7 @@ The :ref:`external types ` classifying a module may contain f * For each :math:`\export_i` in :math:`\module.\MEXPORTS`, the segment :math:`\export_i` must be :ref:`valid ` with :ref:`external type ` :math:`\X{et}_i`. -* Let :math:`\X{ft}^\ast` be the concatenation of the internal :ref:`function types ` :math:`\X{ft}_i`, in index order. +* Let :math:`\X{dt}^\ast` be the concatenation of the internal :ref:`function types ` :math:`\X{dt}_i`, in index order. * Let :math:`\X{tt}^\ast` be the concatenation of the internal :ref:`table types ` :math:`\X{tt}_i`, in index order. @@ -778,7 +776,7 @@ The :ref:`external types ` classifying a module may contain f \quad (C' \vdashmem \mem : \X{mt})^\ast \quad - (C \vdashfunc \func : \X{ft})^\ast + (C \vdashfunc \func : \X{dt})^\ast \\ (C \vdashelem \elem : \X{rt})^\ast \quad @@ -790,7 +788,7 @@ The :ref:`external types ` classifying a module may contain f \quad (C \vdashexport \export : \X{et})^\ast \\ - \X{ift}^\ast = \etfuncs(\X{it}^\ast) + \X{idt}^\ast = \etfuncs(\X{it}^\ast) \qquad \X{itt}^\ast = \ettables(\X{it}^\ast) \qquad @@ -800,7 +798,7 @@ The :ref:`external types ` classifying a module may contain f \\ x^\ast = \freefuncidx(\module \with \MFUNCS = \epsilon \with \MSTART = \epsilon) \\ - C = \{ \CTYPES~C_0.\CTYPES, \CFUNCS~\X{ift}^\ast\,\X{ft}^\ast, \CTABLES~\X{itt}^\ast\,\X{tt}^\ast, \CMEMS~\X{imt}^\ast\,\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast\,\X{gt}^\ast, \CELEMS~\X{rt}^\ast, \CDATAS~{\ok}^n, \CREFS~x^\ast \} + C = \{ \CTYPES~C_0.\CTYPES, \CFUNCS~\X{idt}^\ast\,\X{dt}^\ast, \CTABLES~\X{itt}^\ast\,\X{tt}^\ast, \CMEMS~\X{imt}^\ast\,\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast\,\X{gt}^\ast, \CELEMS~\X{rt}^\ast, \CDATAS~{\ok}^n, \CREFS~x^\ast \} \\ C' = \{ \CTYPES~C_0.\CTYPES, \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \} \qquad From 673eaf58cce00e765b02f2a95d5f9ff3b3acee76 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 30 Oct 2023 09:07:18 +0100 Subject: [PATCH 09/43] [spec] Typo --- document/core/exec/modules.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index bc2e9bb965..a16e1ecc70 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -459,7 +459,7 @@ For types, however, allocation is defined in terms of :ref:`rolling Date: Mon, 30 Oct 2023 09:19:37 +0100 Subject: [PATCH 10/43] [spec] Fix prose for blocktype validation --- document/core/valid/types.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 9366e01154..39ab9601ed 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -130,7 +130,7 @@ Block Types * The type :math:`C.\CTYPES[\typeidx]` must be defined in the context. -* Let :math:`[t_1^\ast] \toF [t_2^\ast]` be the :ref:`function type ` :math:`C.\CTYPES[\typeidx]`. +* The :ref:`expansion ` of :math:`C.\CFUNCS[\typeidx]` must be a :ref:`function type ` :math:`\TFUNC~[t_1^\ast] \toF [t_2^\ast]`. * Then the block type is valid as :ref:`instruction type ` :math:`[t_1^\ast] \to [t_2^\ast]`. From 3a7f703d408ceb9fb742e519c0e3dfcfdc3fcab7 Mon Sep 17 00:00:00 2001 From: YiYing He Date: Tue, 31 Oct 2023 03:51:52 +0800 Subject: [PATCH 11/43] [spec] fix immediate of `array.set` instruction. Signed-off-by: YiYing He --- document/core/valid/instructions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index f5ad69aa35..655e5f79d8 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -566,8 +566,8 @@ Aggregate Reference Instructions .. _valid-array.set: -:math:`\ARRAYSET~x~i` -..................... +:math:`\ARRAYSET~x` +................... * The :ref:`defined type ` :math:`C.\CTYPES[x]` must exist. From 951bda8a93dcc5c2b537b819e26de3e90de9b89a Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Tue, 31 Oct 2023 11:12:31 -0700 Subject: [PATCH 12/43] [spec] Fix minor issues in local rules Add missing backslash on \LTYPE Local validation doesn't need `ok` Locals in a function have structure so need {type t} to match the valtype --- document/core/valid/modules.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 550d895778..e934d563e0 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -52,7 +52,7 @@ Functions :math:`\func` are classified by :ref:`type indices ` r \qquad C,\CLOCALS\,(\SET~t_1)^\ast~(\init~t)^\ast,\CLABELS~[t_2^\ast],\CRETURN~[t_2^\ast] \vdashexpr \expr : [t_2^\ast] }{ - C \vdashfunc \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : x + C \vdashfunc \{ \FTYPE~x, \FLOCALS \{\LTYPE~t\}^\ast, \FBODY~\expr \} : x } @@ -85,14 +85,14 @@ Locals \qquad C \vdashvaltypedefaultable t \defaultable }{ - C \vdashlocal \{ \LTYPE~t \} : \SET~t \ok + C \vdashlocal \{ \LTYPE~t \} : \SET~t } .. math:: \frac{ C \vdashvaltype t \ok }{ - C \vdashlocal \{ LTYPE~t \} : \UNSET~t \ok + C \vdashlocal \{ \LTYPE~t \} : \UNSET~t } .. note:: From 268b9c4964ba6565adc70cbde673caffdd260223 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Tue, 31 Oct 2023 12:23:07 -0700 Subject: [PATCH 13/43] Adjust locals PR based on feedback --- document/core/util/macros.def | 4 ++-- document/core/valid/modules.rst | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 81dc94de23..2427f77f0b 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -212,8 +212,8 @@ .. |MVAR| mathdef:: \xref{syntax/types}{syntax-mut}{\K{var}} .. |MCONST| mathdef:: \xref{syntax/types}{syntax-mut}{\K{const}} -.. |SET| mathdef:: \xref{syntax/types}{syntax-init}{\mathrel{\mbox{set}}} -.. |UNSET| mathdef:: \xref{syntax/types}{syntax-init}{\mathrel{\mbox{unset}}} +.. |SET| mathdef:: \xref{syntax/types}{syntax-init}{\K{set}} +.. |UNSET| mathdef:: \xref{syntax/types}{syntax-init}{\K{unset}} .. |LMIN| mathdef:: \xref{syntax/types}{syntax-limits}{\K{min}} .. |LMAX| mathdef:: \xref{syntax/types}{syntax-limits}{\K{max}} diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index e934d563e0..064f44f8e1 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -48,11 +48,11 @@ Functions :math:`\func` are classified by :ref:`type indices ` r \frac{ C.\CTYPES[x] = [t_1^\ast] \toF [t_2^\ast] \qquad - (C \vdashlocal t : \init~t)^\ast + (C \vdashlocal \{\LTYPE~t\} : \init~t)^\ast \qquad C,\CLOCALS\,(\SET~t_1)^\ast~(\init~t)^\ast,\CLABELS~[t_2^\ast],\CRETURN~[t_2^\ast] \vdashexpr \expr : [t_2^\ast] }{ - C \vdashfunc \{ \FTYPE~x, \FLOCALS \{\LTYPE~t\}^\ast, \FBODY~\expr \} : x + C \vdashfunc \{ \FTYPE~x, \FLOCALS~\{\LTYPE~t\}^\ast, \FBODY~\expr \} : x } From 92fbea708bf0bbaae1106cc111004843cd20c418 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 1 Nov 2023 06:54:47 +0100 Subject: [PATCH 14/43] [spec] Cleaner definition of frames (#1697) --- document/core/exec/runtime.rst | 11 +++++++---- document/core/util/macros.def | 1 + 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 6c53a4e965..c7a6b9819f 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -419,6 +419,7 @@ It filters out entries of a specific kind in an order-preserving fashion: pair: abstract syntax; frame pair: abstract syntax; label .. _syntax-frame: +.. _syntax-framestate: .. _syntax-label: .. _frame: .. _label: @@ -486,6 +487,8 @@ and a reference to the function's own :ref:`module instance ` .. math:: \begin{array}{llll} \production{frame} & \frame &::=& + \FRAME_n\{ \framestate \} \\ + \production{frame state} & \framestate &::=& \{ \ALOCALS~\val^\ast, \AMODULE~\moduleinst \} \\ \end{array} @@ -499,7 +502,7 @@ Conventions * The meta variable :math:`L` ranges over labels where clear from context. -* The meta variable :math:`F` ranges over frames where clear from context. +* The meta variable :math:`F` ranges over frame states where clear from context. * The following auxiliary definition takes a :ref:`block type ` and looks up the :ref:`function type ` that it denotes in the current frame: @@ -534,7 +537,7 @@ In order to express the reduction of :ref:`traps `, :ref:`calls ` and an executing *thread*. A thread is a computation over :ref:`instructions ` -that operates relative to a current :ref:`frame ` referring to the :ref:`module instance ` in which the computation runs, i.e., where the current function originates from. +that operates relative to the state of a current :ref:`frame ` referring to the :ref:`module instance ` in which the computation runs, i.e., where the current function originates from. .. math:: \begin{array}{llcl} \production{configuration} & \config &::=& \store; \thread \\ \production{thread} & \thread &::=& - \frame; \instr^\ast \\ + \framestate; \instr^\ast \\ \end{array} .. note:: diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 5e7a4889b2..2ae99bdee8 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -1056,6 +1056,7 @@ .. |label| mathdef:: \xref{exec/runtime}{syntax-label}{\X{label}} .. |frame| mathdef:: \xref{exec/runtime}{syntax-frame}{\X{frame}} +.. |framestate| mathdef:: \xref{exec/runtime}{syntax-framestate}{\X{framestate}} .. Stack, meta functions From 9b55765facce6cbe9c3c1c08b4b8385da7529abe Mon Sep 17 00:00:00 2001 From: Wonho Date: Fri, 3 Nov 2023 13:51:01 +0900 Subject: [PATCH 15/43] Pass index argument in `getfield` function --- document/core/exec/instructions.rst | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 9f19a15eba..b7085c7fc8 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1153,7 +1153,7 @@ Reference Instructions d. Push the value :math:`\I32.\CONST~s` to the stack. - e. Execute :math:`\getfield(\X{st})`. + e. Execute :math:`\getfield(\X{st}, x)`. f. Execute the instruction :math:`\ARRAYSET~x`. @@ -1183,7 +1183,7 @@ Reference Instructions f. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack. - g. Execute :math:`\getfield(\X{st})`. + g. Execute :math:`\getfield(\X{st}, x)`. h. Execute the instruction :math:`\ARRAYSET~x`. @@ -1217,7 +1217,7 @@ Reference Instructions \\ \quad \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~\getfield(\X{st}) \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~\getfield(\X{st}, x) \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d+1)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} @@ -1229,7 +1229,7 @@ Reference Instructions \\ \quad \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d+n) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~\getfield(\X{st}) \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~\getfield(\X{st}, x) \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} @@ -1247,8 +1247,8 @@ Where: .. math:: \begin{array}{lll} - \getfield(\valtype) &=& \ARRAYGET \\ - \getfield(\packedtype) &=& \ARRAYGETU \\ + \getfield(\valtype, x) &=& \ARRAYGET~x \\ + \getfield(\packedtype, x) &=& \ARRAYGETU~x \\ \end{array} From 13bb5d1886c3b193bd5a5609935b4d3c893ff266 Mon Sep 17 00:00:00 2001 From: Wonho Date: Fri, 3 Nov 2023 14:23:15 +0900 Subject: [PATCH 16/43] Fix `array.set/get` reduction rule --- document/core/exec/instructions.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 9f19a15eba..802d0c69c8 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -901,7 +901,7 @@ Reference Instructions (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ \land & \val = \unpackval^{\sx^?}_{\X{ft}}(S.\SARRAYS[a].\AIFIELDS[i])) \end{array} \\ - S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) &\stepto& \val + S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) &\stepto& \TRAP & (\otherwise) \\ S; F; (\REFNULL~t)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) &\stepto& \TRAP \end{array} @@ -958,6 +958,8 @@ Reference Instructions (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ \land & S' = S \with \SARRAYS[a].\AIFIELDS[i] = \packval_{\X{ft}}(\val)) \end{array} \\ + S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) &\stepto& \TRAP + & (\otherwise) \\ S; F; (\REFNULL~t)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) &\stepto& \TRAP \end{array} From b108440070907c485841745ac33331012de9caae Mon Sep 17 00:00:00 2001 From: Wonho Date: Fri, 3 Nov 2023 17:24:28 +0900 Subject: [PATCH 17/43] Fix OOB cases for `array.get/set` --- document/core/exec/instructions.rst | 40 +++++++++++++++++------------ 1 file changed, 24 insertions(+), 16 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 802d0c69c8..ec36a56467 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -894,16 +894,20 @@ Reference Instructions 16. Push the value :math:`\val` to the stack. .. math:: + ~\\[-1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) &\stepto& \val - & + S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) \stepto \TRAP + \\ \qquad + (\iff |\SARRAYS[a].\AIFIELDS| \leq i) + \\[1ex] + S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) \stepto \val + \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ - \land & \val = \unpackval^{\sx^?}_{\X{ft}}(S.\SARRAYS[a].\AIFIELDS[i])) - \end{array} \\ - S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) &\stepto& \TRAP - & (\otherwise) \\ - S; F; (\REFNULL~t)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) &\stepto& \TRAP + (\otherwise, \iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ + \land & \val = \unpackval^{\sx^?}_{\X{ft}}(S.\SARRAYS[a].\AIFIELDS[i])) \\ + \end{array} + \\[1ex] + S; F; (\REFNULL~t)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) \stepto \TRAP \end{array} @@ -951,16 +955,20 @@ Reference Instructions 17. Replace the :ref:`field value ` :math:`S.\SARRAYS[a].\AIFIELDS[i]` with :math:`\fieldval`. .. math:: + ~\\[-1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) &\stepto& S'; \epsilon - & + S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) \stepto \TRAP + \\ \qquad + (\iff |\SARRAYS[a].\AIFIELDS| \leq i) + \\[1ex] + S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) \stepto S'; \epsilon + \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ - \land & S' = S \with \SARRAYS[a].\AIFIELDS[i] = \packval_{\X{ft}}(\val)) - \end{array} \\ - S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) &\stepto& \TRAP - & (\otherwise) \\ - S; F; (\REFNULL~t)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) &\stepto& \TRAP + (\otherwise, \iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ + \land & S' = S \with \SARRAYS[a].\AIFIELDS[i] = \packval_{\X{ft}}(\val)) \\ + \end{array} + \\[1ex] + S; F; (\REFNULL~t)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) \stepto \TRAP \end{array} From da29215dd817477e0a5e75f0b9a496af3fc5c480 Mon Sep 17 00:00:00 2001 From: Wonho Date: Fri, 3 Nov 2023 17:35:35 +0900 Subject: [PATCH 18/43] Minor fix --- document/core/exec/instructions.rst | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index b7085c7fc8..16c9f4bef5 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1153,7 +1153,7 @@ Reference Instructions d. Push the value :math:`\I32.\CONST~s` to the stack. - e. Execute :math:`\getfield(\X{st}, x)`. + e. Execute :math:`\getfield(\X{st})`. f. Execute the instruction :math:`\ARRAYSET~x`. @@ -1183,7 +1183,7 @@ Reference Instructions f. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack. - g. Execute :math:`\getfield(\X{st}, x)`. + g. Execute :math:`\getfield(\X{st})`. h. Execute the instruction :math:`\ARRAYSET~x`. @@ -1217,7 +1217,7 @@ Reference Instructions \\ \quad \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~\getfield(\X{st}, x) \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s)~\getfield(\X{st}) \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d+1)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} @@ -1229,7 +1229,7 @@ Reference Instructions \\ \quad \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a_1)~(\I32.\CONST~d+n) \\ - (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~\getfield(\X{st}, x) \\ + (\REFARRAYADDR~a_2)~(\I32.\CONST~s+n)~\getfield(\X{st}) \\ (\ARRAYSET~x) \\ (\REFARRAYADDR~a_1)~(\I32.\CONST~d)~(\REFARRAYADDR~a_2)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYCOPY~x~y) \\ \end{array} @@ -1247,8 +1247,8 @@ Where: .. math:: \begin{array}{lll} - \getfield(\valtype, x) &=& \ARRAYGET~x \\ - \getfield(\packedtype, x) &=& \ARRAYGETU~x \\ + \getfield(\valtype) &=& \ARRAYGET~y \\ + \getfield(\packedtype) &=& \ARRAYGETU~y \\ \end{array} From 3c6f6ea9a30457ac98deefb87d1931e731e717ef Mon Sep 17 00:00:00 2001 From: ShinWonho <50018375+ShinWonho@users.noreply.github.com> Date: Fri, 3 Nov 2023 19:31:05 +0900 Subject: [PATCH 19/43] Update document/core/exec/instructions.rst Co-authored-by: Andreas Rossberg --- document/core/exec/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ec36a56467..ef92e20e98 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -898,7 +898,7 @@ Reference Instructions \begin{array}{lcl@{\qquad}l} S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) \stepto \TRAP \\ \qquad - (\iff |\SARRAYS[a].\AIFIELDS| \leq i) + (\iff i \geq |\SARRAYS[a].\AIFIELDS|) \\[1ex] S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) \stepto \val \\ \qquad From 6a9736a79c16fb55b7c9ef215258705c99849a56 Mon Sep 17 00:00:00 2001 From: ShinWonho <50018375+ShinWonho@users.noreply.github.com> Date: Fri, 3 Nov 2023 19:31:13 +0900 Subject: [PATCH 20/43] Update document/core/exec/instructions.rst Co-authored-by: Andreas Rossberg --- document/core/exec/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ef92e20e98..970ebffb14 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -959,7 +959,7 @@ Reference Instructions \begin{array}{lcl@{\qquad}l} S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) \stepto \TRAP \\ \qquad - (\iff |\SARRAYS[a].\AIFIELDS| \leq i) + (\iff i \geq |\SARRAYS[a].\AIFIELDS|) \\[1ex] S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) \stepto S'; \epsilon \\ \qquad From 26ba9e298cb2e55b1dee2d00b8e3a0dc6b651f38 Mon Sep 17 00:00:00 2001 From: Wonho Date: Fri, 3 Nov 2023 19:42:15 +0900 Subject: [PATCH 21/43] Remove otherwise --- document/core/exec/instructions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 970ebffb14..ef10d61468 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -903,7 +903,7 @@ Reference Instructions S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) \stepto \val \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\otherwise, \iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ + (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ \land & \val = \unpackval^{\sx^?}_{\X{ft}}(S.\SARRAYS[a].\AIFIELDS[i])) \\ \end{array} \\[1ex] @@ -964,7 +964,7 @@ Reference Instructions S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) \stepto S'; \epsilon \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\otherwise, \iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ + (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ \land & S' = S \with \SARRAYS[a].\AIFIELDS[i] = \packval_{\X{ft}}(\val)) \\ \end{array} \\[1ex] From c7b6fc38c1457c28e131c6e58b49fe9be79ff823 Mon Sep 17 00:00:00 2001 From: DJ Date: Fri, 3 Nov 2023 22:48:48 +0900 Subject: [PATCH 22/43] [test] Add `assert_return` --- test/core/gc/ref_test.wast | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/core/gc/ref_test.wast b/test/core/gc/ref_test.wast index 39c2def151..590b81b8a4 100644 --- a/test/core/gc/ref_test.wast +++ b/test/core/gc/ref_test.wast @@ -326,5 +326,5 @@ ) ) -(invoke "test-sub") -(invoke "test-canon") +(assert_return (invoke "test-sub")) +(assert_return (invoke "test-canon")) From 07969346e860e88dccaefd02649827cd3d4b0c2b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?J=C3=A9r=C3=B4me=20Vouillon?= Date: Sat, 4 Nov 2023 09:31:15 +0100 Subject: [PATCH 23/43] Update the 'read the imports' process --- document/js-api/index.bs | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/document/js-api/index.bs b/document/js-api/index.bs index 62957c2d51..60f562fb79 100644 --- a/document/js-api/index.bs +++ b/document/js-api/index.bs @@ -361,10 +361,12 @@ A {{Module}} object represents a single WebAssembly module. Each {{Module}} obje 1. Let |externfunc| be the [=external value=] [=external value|func=] |funcaddr|. 1. [=list/Append=] |externfunc| to |imports|. 1. If |externtype| is of the form [=global=] mut |valtype|, - 1. If [=Type=](|v|) is Number or BigInt, - 1. If |valtype| is [=i64=] and [=Type=](|v|) is Number, + 1. If |v| [=implements=] {{Global}}, + 1. Let |globaladdr| be |v|.\[[Global]]. + 1. Otherwise, + 1. If |valtype| is [=i64=] and [=Type=](|v|) is not BigInt, 1. Throw a {{LinkError}} exception. - 1. If |valtype| is not [=i64=] and [=Type=](|v|) is BigInt, + 1. If |valtype| is one of [=i32=], [=f32=] or [=f64=] and [=Type=](|v|) is not Number, 1. Throw a {{LinkError}} exception. 1. If |valtype| is [=v128=], 1. Throw a {{LinkError}} exception. @@ -372,10 +374,6 @@ A {{Module}} object represents a single WebAssembly module. Each {{Module}} obje 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let (|store|, |globaladdr|) be [=global_alloc=](|store|, [=const=] |valtype|, |value|). 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. - 1. Otherwise, if |v| [=implements=] {{Global}}, - 1. Let |globaladdr| be |v|.\[[Global]]. - 1. Otherwise, - 1. Throw a {{LinkError}} exception. 1. Let |externglobal| be [=external value|global=] |globaladdr|. 1. [=list/Append=] |externglobal| to |imports|. 1. If |externtype| is of the form [=mem=] memtype, From 1c187ea5e6ddf8d525ec760ad02db43e87ff3b11 Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Mon, 6 Nov 2023 15:24:43 +0100 Subject: [PATCH 24/43] fix display of administrative instructions --- document/core/exec/runtime.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 1ecc196c0b..681a4f89d7 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -639,7 +639,7 @@ In order to express the reduction of :ref:`traps `, :ref:`calls Date: Tue, 7 Nov 2023 02:02:23 +0100 Subject: [PATCH 25/43] [js-api] Document the new implementation limits (#471) The new limits were previously merged in #360, but apparently that PR was to another branch that itself was never merged. Reland that change with two additional fixes: - Add digit separators in the numbers to improve readability and match the formatting of other limits. - Add an explicit limit of 1,000,000 types per recursion group. This is not intended to be a functional change, but this limit was previously left implicit. --- document/js-api/index.bs | 7 ++++++- proposals/gc/MVP-JS.md | 13 +++++++++++++ proposals/gc/MVP.md | 3 +-- 3 files changed, 20 insertions(+), 3 deletions(-) diff --git a/document/js-api/index.bs b/document/js-api/index.bs index 60f562fb79..f8fc544362 100644 --- a/document/js-api/index.bs +++ b/document/js-api/index.bs @@ -1349,6 +1349,9 @@ In practice, an implementation may run out of resources for valid modules below
  • The maximum size of a module is 1,073,741,824 bytes (1 GiB).
  • The maximum number of types defined in the types section is 1,000,000.
    • +
  • The maximum number of recursion groups defined in the types sections is 1,000,000.
    • +
  • The maximum number of types defined in a recursion group is 1,000,000.
    • +
  • The maximum depth of a defined subtype hierarchy is 63 (where a type defined with no supertype has depth 0).
  • The maximum number of functions defined in a module is 1,000,000.
  • The maximum number of imports declared in a module is 100,000.
  • The maximum number of exports declared in a module is 100,000.
    • @@ -1356,7 +1359,7 @@ In practice, an implementation may run out of resources for valid modules below
  • The maximum number of data segments defined in a module is 100,000.
  • The maximum number of tables, including declared or imported tables, is 100,000.
    • -
  • The maximum size of a table is 10,000,000.
    • +
  • The maximum size of a table is 10000000.
  • The maximum number of table entries in any table initialization is 10,000,000.
  • The maximum number of memories, including declared or imported memories, is 1.
    • @@ -1364,6 +1367,8 @@ In practice, an implementation may run out of resources for valid modules below
  • The maximum number of return values for any function or block is 1,000.
  • The maximum size of a function body, including locals declarations, is 7,654,321 bytes.
  • The maximum number of locals declared in a function, including implicitly declared as parameters, is 50,000.
    • +
  • The maximum number of fields in a struct is 10,000.
    • +
  • The maximum number of operands to `array.new_fixed` is 10,000.
An implementation must throw a {{RuntimeError}} if one of the following limits is exceeded during runtime: diff --git a/proposals/gc/MVP-JS.md b/proposals/gc/MVP-JS.md index 11843c6fe5..455465bb55 100644 --- a/proposals/gc/MVP-JS.md +++ b/proposals/gc/MVP-JS.md @@ -69,3 +69,16 @@ internal reference value that is being externalized: _TODO: avoid having to patch the behavior of `extern.internalize` and `extern.internalize` by converting to/from JS numbers separately._ + +## Implementation-defined Limits + +The following limits will be added to the Implementation-defined Limits +[section](https://webassembly.github.io/spec/js-api/index.html#limits) of the JS +API. + + - The maximum number of recursion groups is 1000000. (The maximum number of + individual types remains unchanged and is also 1000000.) + - The maximum number of struct fields is 10000. + - The maximum number of operands to `array.new_fixed` is 10000. + - The maximum length of a supertype chain is 63. (A type declared with no + supertypes has a supertype chain of length 0) diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index 6d9589aca7..081dfc539e 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -848,8 +848,7 @@ Flag byte encoding for `br_on_cast(_fail)?`: ## JS API -See [GC JS API document](MVP-JS.md) . - +See [GC JS API document](MVP-JS.md). ## Questions From 51de001b99ef306044a3a3e91cd2be658f6d2ceb Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Mon, 6 Nov 2023 17:43:01 -0800 Subject: [PATCH 26/43] [js-api] Restore accidentally-deleted digit separators These were accidentally deleted in #471. --- document/js-api/index.bs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/js-api/index.bs b/document/js-api/index.bs index f8fc544362..d7657d9fe0 100644 --- a/document/js-api/index.bs +++ b/document/js-api/index.bs @@ -1359,7 +1359,7 @@ In practice, an implementation may run out of resources for valid modules below
  • The maximum number of data segments defined in a module is 100,000.
  • The maximum number of tables, including declared or imported tables, is 100,000.
    • -
  • The maximum size of a table is 10000000.
    • +
  • The maximum size of a table is 10,000,000.
  • The maximum number of table entries in any table initialization is 10,000,000.
  • The maximum number of memories, including declared or imported memories, is 1.
    • From 3be4c2fb1b44f5b48ccb43af1f314dc3dc8ca6ec Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 7 Nov 2023 07:20:40 +0100 Subject: [PATCH 27/43] [spec] Fix definition of lane ops + better xrefs (#1700) --- document/core/appendix/index-instructions.py | 3 +- document/core/exec/instructions.rst | 52 +++++++++++--------- document/core/exec/numerics.rst | 17 ++++--- document/core/util/macros.def | 6 +++ 4 files changed, 45 insertions(+), 33 deletions(-) diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index c3ffc2a324..8ffedcca31 100755 --- a/document/core/appendix/index-instructions.py +++ b/document/core/appendix/index-instructions.py @@ -54,8 +54,7 @@ def RefWrap(s, kind): def Instruction(name, opcode, type=None, validation=None, execution=None, operator=None): if operator: - execution_str = ', '.join([RefWrap(execution, 'execution'), - RefWrap(operator, 'operator')]) + execution_str = RefWrap(execution, 'execution') + ' (' + RefWrap(operator, 'operator') + ')' else: execution_str = RefWrap(execution, 'execution') diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ccb27bfd31..74802d6deb 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -20,16 +20,15 @@ The mapping of numeric instructions to their underlying operators is expressed b .. math:: \begin{array}{lll@{\qquad}l} - \X{op}_{\IN}(i_1,\dots,i_k) &=& \F{i}\X{op}_N(i_1,\dots,i_k) \\ - \X{op}_{\FN}(z_1,\dots,z_k) &=& \F{f}\X{op}_N(z_1,\dots,z_k) \\ - \X{op}_{\VN}(i_1,\dots,i_k) &=& \F{i}\X{op}_N(i_1,\dots,i_k) \\ + \X{op}_{\IN}(i_1,\dots,i_k) &=& \xref{exec/numerics}{int-ops}{\F{i}\X{op}}_N(i_1,\dots,i_k) \\ + \X{op}_{\FN}(z_1,\dots,z_k) &=& \xref{exec/numerics}{float-ops}{\F{f}\X{op}}_N(z_1,\dots,z_k) \\ \end{array} And for :ref:`conversion operators `: .. math:: \begin{array}{lll@{\qquad}l} - \X{cvtop}^{\sx^?}_{t_1,t_2}(c) &=& \X{cvtop}^{\sx^?}_{|t_1|,|t_2|}(c) \\ + \cvtop^{\sx^?}_{t_1,t_2}(c) &=& \xref{exec/numerics}{convert-ops}{\X{cvtop}}^{\sx^?}_{|t_1|,|t_2|}(c) \\ \end{array} Where the underlying operators are partial, the corresponding instruction will :ref:`trap ` when the result is not defined. @@ -64,9 +63,9 @@ Where the underlying operators are non-deterministic, because they may return on 2. Pop the value :math:`t.\CONST~c_1` from the stack. -3. If :math:`\unop_t(c_1)` is defined, then: +3. If :math:`\unopF_t(c_1)` is defined, then: - a. Let :math:`c` be a possible result of computing :math:`\unop_t(c_1)`. + a. Let :math:`c` be a possible result of computing :math:`\unopF_t(c_1)`. b. Push the value :math:`t.\CONST~c` to the stack. @@ -77,9 +76,9 @@ Where the underlying operators are non-deterministic, because they may return on .. math:: \begin{array}{lcl@{\qquad}l} (t\K{.}\CONST~c_1)~t\K{.}\unop &\stepto& (t\K{.}\CONST~c) - & (\iff c \in \unop_t(c_1)) \\ + & (\iff c \in \unopF_t(c_1)) \\ (t\K{.}\CONST~c_1)~t\K{.}\unop &\stepto& \TRAP - & (\iff \unop_{t}(c_1) = \{\}) + & (\iff \unopF_{t}(c_1) = \{\}) \end{array} @@ -94,9 +93,9 @@ Where the underlying operators are non-deterministic, because they may return on 3. Pop the value :math:`t.\CONST~c_1` from the stack. -4. If :math:`\binop_t(c_1, c_2)` is defined, then: +4. If :math:`\binopF_t(c_1, c_2)` is defined, then: - a. Let :math:`c` be a possible result of computing :math:`\binop_t(c_1, c_2)`. + a. Let :math:`c` be a possible result of computing :math:`\binopF_t(c_1, c_2)`. b. Push the value :math:`t.\CONST~c` to the stack. @@ -107,9 +106,9 @@ Where the underlying operators are non-deterministic, because they may return on .. math:: \begin{array}{lcl@{\qquad}l} (t\K{.}\CONST~c_1)~(t\K{.}\CONST~c_2)~t\K{.}\binop &\stepto& (t\K{.}\CONST~c) - & (\iff c \in \binop_t(c_1,c_2)) \\ + & (\iff c \in \binopF_t(c_1,c_2)) \\ (t\K{.}\CONST~c_1)~(t\K{.}\CONST~c_2)~t\K{.}\binop &\stepto& \TRAP - & (\iff \binop_{t}(c_1,c_2) = \{\}) + & (\iff \binopF_{t}(c_1,c_2) = \{\}) \end{array} @@ -122,14 +121,14 @@ Where the underlying operators are non-deterministic, because they may return on 2. Pop the value :math:`t.\CONST~c_1` from the stack. -3. Let :math:`c` be the result of computing :math:`\testop_t(c_1)`. +3. Let :math:`c` be the result of computing :math:`\testopF_t(c_1)`. 4. Push the value :math:`\I32.\CONST~c` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} (t\K{.}\CONST~c_1)~t\K{.}\testop &\stepto& (\I32\K{.}\CONST~c) - & (\iff c = \testop_t(c_1)) \\ + & (\iff c = \testopF_t(c_1)) \\ \end{array} @@ -144,14 +143,14 @@ Where the underlying operators are non-deterministic, because they may return on 3. Pop the value :math:`t.\CONST~c_1` from the stack. -4. Let :math:`c` be the result of computing :math:`\relop_t(c_1, c_2)`. +4. Let :math:`c` be the result of computing :math:`\relopF_t(c_1, c_2)`. 5. Push the value :math:`\I32.\CONST~c` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} (t\K{.}\CONST~c_1)~(t\K{.}\CONST~c_2)~t\K{.}\relop &\stepto& (\I32\K{.}\CONST~c) - & (\iff c = \relop_t(c_1,c_2)) \\ + & (\iff c = \relopF_t(c_1,c_2)) \\ \end{array} @@ -256,20 +255,27 @@ Reference Instructions Vector Instructions ~~~~~~~~~~~~~~~~~~~ -Most vector instructions are defined in terms of generic numeric operators applied lane-wise based on the :ref:`shape `. +Vector instructions that operate bitwise are handled as integer operations of respective width. .. math:: \begin{array}{lll@{\qquad}l} + \X{op}_{\VN}(i_1,\dots,i_k) &=& \xref{exec/numerics}{int-ops}{\F{i}\X{op}}_N(i_1,\dots,i_k) \\ + \end{array} + +Most other vector instructions are defined in terms of numeric operators that are applied lane-wise according to the given :ref:`shape `. + +.. math:: + \begin{array}{llll} \X{op}_{t\K{x}N}(n_1,\dots,n_k) &=& - \lanes^{-1}_{t\K{x}N}(op_t(\lanes_{t\K{x}N}(n_1) ~\dots~ \lanes_{t\K{x}N}(n_k)) + \lanes^{-1}_{t\K{x}N}(\xref{exec/instructions}{exec-instr-numeric}{\X{op}}_t(i_1,\dots,i_k)^\ast) & \qquad(\iff i_1^\ast = \lanes_{t\K{x}N}(n_1) \land \dots \land i_k^\ast = \lanes_{t\K{x}N}(n_k) \\ \end{array} .. note:: - For example, the result of instruction :math:`\K{i32x4}.\ADD` applied to operands :math:`i_1, i_2` - invokes :math:`\ADD_{\K{i32x4}}(i_1, i_2)`, which maps to - :math:`\lanes^{-1}_{\K{i32x4}}(\ADD_{\I32}(i_1^+, i_2^+))`, - where :math:`i_1^+` and :math:`i_2^+` are sequences resulting from invoking - :math:`\lanes_{\K{i32x4}}(i_1)` and :math:`\lanes_{\K{i32x4}}(i_2)` + For example, the result of instruction :math:`\K{i32x4}.\ADD` applied to operands :math:`v_1, v_2` + invokes :math:`\ADD_{\K{i32x4}}(v_1, v_2)`, which maps to + :math:`\lanes^{-1}_{\K{i32x4}}(\ADD_{\I32}(i_1, i_2)^\ast)`, + where :math:`i_1^\ast` and :math:`i_2^\ast` are sequences resulting from invoking + :math:`\lanes_{\K{i32x4}}(v_1)` and :math:`\lanes_{\K{i32x4}}(v_2)` respectively. diff --git a/document/core/exec/numerics.rst b/document/core/exec/numerics.rst index 85d3dbd00c..b76190f6f2 100644 --- a/document/core/exec/numerics.rst +++ b/document/core/exec/numerics.rst @@ -169,24 +169,25 @@ where :math:`M = \significand(N)` and :math:`E = \exponent(N)`. Vectors ....... -Numeric vectors have the same underlying representation as an |i128|. -They can also be interpreted as a sequence of numeric values packed into a |V128| with a particular |shape|. +Numeric vectors of type |VN| have the same underlying representation as an |IN|. +They can also be interpreted as a sequence of numeric values packed into a |VN| with a particular |shape| :math:`t\K{x}M`, +provided that :math:`N = |t|\cdot M`. .. math:: \begin{array}{l} \begin{array}{lll@{\qquad}l} - \lanes_{t\K{x}N}(c) &=& - c_0~\dots~c_{N-1} \\ + \lanes_{t\K{x}M}(c) &=& + c_0~\dots~c_{M-1} \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}l@{~}l@{~}l} - (\where & B &=& |t| / 8 \\ - \wedge & b^{16} &=& \bytes_{\i128}(c) \\ - \wedge & c_i &=& \bytes_{t}^{-1}(b^{16}[i \cdot B \slice B])) + (\where & w &=& |t| / 8 \\ + \wedge & b^\ast &=& \bytes_{\IN}(c) \\ + \wedge & c_i &=& \bytes_{t}^{-1}(b^\ast[i \cdot w \slice w])) \end{array} \end{array} -These functions are bijections, so they are invertible. +This function is a bijection on |IN|, hence it is invertible. .. index:: byte, little endian, memory diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 2ae99bdee8..1dcec42d2d 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -500,6 +500,12 @@ .. |relop| mathdef:: \xref{syntax/instructions}{syntax-relop}{\X{relop}} .. |cvtop| mathdef:: \xref{syntax/instructions}{syntax-cvtop}{\X{cvtop}} +.. |unopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{unop}} +.. |binopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{binop}} +.. |testopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{testop}} +.. |relopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{relop}} +.. |cvtopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{cvtop}} + .. |iunop| mathdef:: \xref{syntax/instructions}{syntax-iunop}{\X{iunop}} .. |ibinop| mathdef:: \xref{syntax/instructions}{syntax-ibinop}{\X{ibinop}} .. |itestop| mathdef:: \xref{syntax/instructions}{syntax-itestop}{\X{itestop}} From 29a76a392edad3feefaa7ac79d55e2a15285c808 Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Tue, 7 Nov 2023 17:36:47 +0100 Subject: [PATCH 28/43] fix rule for array.set --- document/core/exec/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 06871c1e98..c3ac550015 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -964,7 +964,7 @@ Reference Instructions S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) \stepto S'; \epsilon \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ + (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ \land & S' = S \with \SARRAYS[a].\AIFIELDS[i] = \packval_{\X{ft}}(\val)) \\ \end{array} \\[1ex] From 63ee3ee7b67272f32fec9dec85287166eada2e8e Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Wed, 8 Nov 2023 17:57:44 +0100 Subject: [PATCH 29/43] remove duplicated token definition in parser --- interpreter/text/parser.mly | 1 - 1 file changed, 1 deletion(-) diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 8e74493f8c..a445027c82 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -275,7 +275,6 @@ let inline_func_type_explicit (c : context) x ft at = %token UNARY BINARY TEST COMPARE CONVERT %token REF_NULL REF_FUNC REF_I31 REF_STRUCT REF_ARRAY REF_EXTERN REF_HOST %token REF_EQ REF_IS_NULL REF_AS_NON_NULL REF_TEST REF_CAST -%token REF_I31 %token I31_GET %token Ast.instr'> STRUCT_NEW ARRAY_NEW ARRAY_GET %token STRUCT_SET From 2f16867a6e47819d26c12adec496c0aba82aa761 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Thu, 9 Nov 2023 19:31:58 -0800 Subject: [PATCH 30/43] [spec] Fix formatting of any.convert_extern and extern.convert_any The underscore needs to be escaped. --- document/core/text/instructions.rst | 6 +++--- document/core/util/macros.def | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index cf84de104b..619761e4db 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -240,8 +240,8 @@ Reference Instructions \text{ref.i31} &\Rightarrow& \REFI31 \\ &&|& \text{i31.get\_u} &\Rightarrow& \I31GETU \\ &&|& \text{i31.get\_s} &\Rightarrow& \I31GETS \\ &&|& - \text{any.convert_extern} &\Rightarrow& \ANYCONVERTEXTERN \\ &&|& - \text{extern.convert_any} &\Rightarrow& \EXTERNCONVERTANY \\ + \text{any.convert\_extern} &\Rightarrow& \ANYCONVERTEXTERN \\ &&|& + \text{extern.convert\_any} &\Rightarrow& \EXTERNCONVERTANY \\ \end{array} @@ -989,7 +989,7 @@ Such a folded instruction can appear anywhere a regular instruction can. .. math:: \begin{array}{lllll} - \production{instruction} & + \production{instruction} & \text{(}~\Tplaininstr~~\Tfoldedinstr^\ast~\text{)} &\equiv\quad \Tfoldedinstr^\ast~~\Tplaininstr \\ & \text{(}~\text{block}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~\text{)} diff --git a/document/core/util/macros.def b/document/core/util/macros.def index b7499f0eca..602c4fb51a 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -506,8 +506,8 @@ .. |I31GETS| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{i31.get\_s}} .. |I31GETU| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{i31.get\_u}} -.. |ANYCONVERTEXTERN| mathdef:: \xref{syntax/instructions}{syntax-instr-extern}{\K{any.convert_extern}} -.. |EXTERNCONVERTANY| mathdef:: \xref{syntax/instructions}{syntax-instr-extern}{\K{extern.convert_any}} +.. |ANYCONVERTEXTERN| mathdef:: \xref{syntax/instructions}{syntax-instr-extern}{\K{any.convert\_extern}} +.. |EXTERNCONVERTANY| mathdef:: \xref{syntax/instructions}{syntax-instr-extern}{\K{extern.convert\_any}} .. |CONST| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{const}} .. |EQZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eqz}} From b431866e360d4eb75df4e506ba1fcdd24955082d Mon Sep 17 00:00:00 2001 From: Wonho Date: Fri, 10 Nov 2023 15:58:41 +0900 Subject: [PATCH 31/43] Minor changes on array.new_elem --- document/core/exec/instructions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 637b002d8a..73ec445584 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -827,13 +827,13 @@ Reference Instructions 8. If the sum of :math:`s` and :math:`n` is larger than the length of :math:`\eleminst.\EIELEM`, then: - a. Trap. + a. Trap. 9. Let :math:`\reff^\ast` be the :ref:`reference ` sequence :math:`\eleminst.\EIELEM[s \slice n]`. 10. Push the references :math:`\reff^\ast` to the stack. -15. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. +11. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. .. math:: ~\\[-1ex] From d3c8128fdf00198cfee2d57f78736b14a0562c3a Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 10 Nov 2023 11:28:18 +0100 Subject: [PATCH 32/43] [spec] Fix 476 --- document/core/exec/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 73ec445584..4a3b9fb0e6 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -801,7 +801,7 @@ Reference Instructions \begin{array}[t]{@{}r@{~}l@{}} (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}^n \\ \land & t = \unpacktype(\X{ft}) \\ - \land & (\bytes_{\X{ft}}(c))^n = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice n\cdot|\X{ft}|/8] \\ + \land & \concat((\bytes_{\X{ft}}(c))^n) = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice n\cdot|\X{ft}|/8] \\ \end{array} \\ \end{array} From f7884c2ccc1fafd9b84059c0f2be30db7f9f08e1 Mon Sep 17 00:00:00 2001 From: Dylan Thacker-Smith Date: Tue, 7 Nov 2023 14:56:37 -0500 Subject: [PATCH 33/43] Fix overview example --- proposals/gc/Overview.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/gc/Overview.md b/proposals/gc/Overview.md index 7655c206ee..3bdd4d80de 100644 --- a/proposals/gc/Overview.md +++ b/proposals/gc/Overview.md @@ -118,7 +118,7 @@ function g() { function h() { let b : nullable buf = {pos = 0, chars = "AAAA"} - b.buf[b.pos] + b.chars[b.pos] } ``` From 156239b6bc3b124ff11d21b89eea3586f4e4cacb Mon Sep 17 00:00:00 2001 From: Dylan Thacker-Smith Date: Tue, 7 Nov 2023 14:56:58 -0500 Subject: [PATCH 34/43] `optref` -> `ref null` `ref null` is currently how nullable references are specified in the typed references spec --- proposals/gc/Overview.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/proposals/gc/Overview.md b/proposals/gc/Overview.md index 3bdd4d80de..64f3924479 100644 --- a/proposals/gc/Overview.md +++ b/proposals/gc/Overview.md @@ -153,7 +153,7 @@ The above could map to ) (func $h - (local $b (optref $buf)) + (local $b (ref null $buf)) (local.set $b (struct.new $buf (i64.const 0) @@ -408,7 +408,7 @@ For example: ) ``` All accesses are type-checked at validation time. -The structure operand of `struct.get/set` may either be a `ref` or an `optref` for a structure type +The structure operand of `struct.get/set` may either be a `ref` or an `ref null` for a structure type In the latter case, the access involves a runtime null check that will trap upon failure. Structures are *allocated* with the `struct.new` instruction that accepts initialization values for each field. @@ -440,7 +440,7 @@ Elements are accessed with generic load/store instructions that take a reference ) ``` The element type of every access is checked at validation time. -The array operand of `array.get/set` may either be a `ref` or an `optref` for an array type +The array operand of `array.get/set` may either be a `ref` or an `ref null` for an array type In the latter case, the access involves a runtime null check that will trap upon failure. The index is checked against the array's length at execution time. A trap occurs if the index is out of bounds. @@ -505,7 +505,7 @@ These notions are already introduced by [typed function references](https://gith Plain references cannot be null, avoiding any runtime overhead for null checks when accessing a struct or array. -Nullable references are available as separate types called `optref`, as per the . +Nullable references are available as separate types called `ref null`, as per the . Most value types, including all numeric types and nullable references are *defaultable*, which means that they have 0 or null as a default value. Other reference types are not defaultable. From 48e610fdd9aa955d31a164092e915ee71e8ab347 Mon Sep 17 00:00:00 2001 From: Dylan Thacker-Smith Date: Wed, 8 Nov 2023 08:25:12 -0500 Subject: [PATCH 35/43] Reference the right local variable in example explanation. --- proposals/gc/Overview.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/gc/Overview.md b/proposals/gc/Overview.md index 64f3924479..b227bcefac 100644 --- a/proposals/gc/Overview.md +++ b/proposals/gc/Overview.md @@ -168,7 +168,7 @@ The above could map to ) ``` These functions `$f` and `$g` code introduces local with the `let` instruction (see the [typed function references proposal](https://github.com/WebAssembly/function-references/blob/master/proposals/function-references/Overview.md)) because the defined types cannot be null, such that locals of these types cannot be default-initialised. -In the case of `$h` the local is declared as nullable, however, mapping to an optional reference. +In the case of `$b` the local is declared as nullable, however, mapping to an optional reference. The respective access via `struct.get` may hence trap. From 6bdba3a7433df29a7a702cefbd9a4c18d6e29abe Mon Sep 17 00:00:00 2001 From: Dylan Thacker-Smith Date: Fri, 10 Nov 2023 09:53:01 -0500 Subject: [PATCH 36/43] Remove references to the `let` instruction that was removed That instruction as removed in https://github.com/WebAssembly/function-references/pull/63 --- proposals/gc/Overview.md | 59 +++++++++++++++++++++------------------- 1 file changed, 31 insertions(+), 28 deletions(-) diff --git a/proposals/gc/Overview.md b/proposals/gc/Overview.md index b227bcefac..150d089b1f 100644 --- a/proposals/gc/Overview.md +++ b/proposals/gc/Overview.md @@ -126,7 +126,7 @@ Needs: * user-defined structures and arrays as heap objects * references to those as first-class values -* let +* locals of these types The above could map to ``` @@ -136,20 +136,22 @@ The above could map to (type $buf (struct (field $pos (mut i64)) (field $chars (ref $char-array)))) (func $f - (struct.new $tup (i64.const 1) (i64.const 2) (i64.const 1)) - (let (local $t (ref $tup)) - (struct.get $tup 1 (local.get $t)) - (drop) + (local $t (ref $tup)) + (local.set $t + (struct.new $tup (i64.const 1) (i64.const 2) (i64.const 1)) ) + (struct.get $tup 1 (local.get $t)) + (drop) ) (func $g - (array.new $vec3d (f64.const 1) (i32.const 3)) - (let (local $v (ref $vec3d)) - (array.set $vec3d (local.get $v) (i32.const 2) (i32.const 5)) - (array.get $vec3d (local.get $v) (i32.const 1)) - (drop) + (local $v (ref $vec3d)) + (local.set $v + (array.new $vec3d (f64.const 1) (i32.const 3)) ) + (array.set $vec3d (local.get $v) (i32.const 2) (i32.const 5)) + (array.get $vec3d (local.get $v) (i32.const 1)) + (drop) ) (func $h @@ -167,7 +169,7 @@ The above could map to (drop) ) ``` -These functions `$f` and `$g` code introduces local with the `let` instruction (see the [typed function references proposal](https://github.com/WebAssembly/function-references/blob/master/proposals/function-references/Overview.md)) because the defined types cannot be null, such that locals of these types cannot be default-initialised. +These functions `$f` and `$g` code introduces locals which cannot be null, so they must be set before their first get (see the [typed function references proposal](https://github.com/WebAssembly/function-references/blob/master/proposals/function-references/Overview.md)). In the case of `$b` the local is declared as nullable, however, mapping to an optional reference. The respective access via `struct.get` may hence trap. @@ -217,10 +219,11 @@ To emulate the covariance of the `this` parameter, one down cast on `this` is ne For example, `D.g`: ``` (func $D.g (param $Cthis (ref $C)) - (ref.cast (local.get $Cthis) (rtt.get (ref $D))) - (let (local $this (ref $D)) - ... + (local $this (ref $D)) + (local.set $this + (ref.cast (local.get $Cthis) (rtt.get (ref $D))) ) + ... ) ``` The addition of [type fields](Post-MVP.md#type-parameters) may later avoid this cast. @@ -260,24 +263,24 @@ function caller() { ) (func $inner (param $clos (ref $clos-f64-f64)) (param $y f64) (result f64) - (ref.cast (local.get $clos) (rtt.get (ref $inner-clos))) - (let (result f64) (local $env (ref $inner-clos)) - (local.get $y) - (struct.get $inner-clos $a (local.get $env)) - (f64.add) - (struct.get $inner-clos $x (local.get $env)) - (f64.add) + (local $env (ref $inner-clos)) + (local.set $env + (ref.cast (local.get $clos) (rtt.get (ref $inner-clos))) ) + (local.get $y) + (struct.get $inner-clos $a (local.get $env)) + (f64.add) + (struct.get $inner-clos $x (local.get $env)) + (f64.add) ) (func $caller (result f64) - (call $outer (f64.const 1)) - (let (result f64) (local $clos (ref $clos-f64-f64)) - (call_ref - (local.get $clos) - (f64.const 2) - (struct.get $clos-f64-f64 $code (local.get $clos)) - ) + (local $clos (ref $clos-f64-f64)) + (local.set $clos (call $outer (f64.const 1))) + (call_ref + (local.get $clos) + (f64.const 2) + (struct.get $clos-f64-f64 $code (local.get $clos)) ) ) ``` From 30661978c0b3ef4993c60a5cbaedb010b45f9b55 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 10 Nov 2023 16:19:41 +0100 Subject: [PATCH 37/43] Update proposals/gc/Overview.md --- proposals/gc/Overview.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/gc/Overview.md b/proposals/gc/Overview.md index 150d089b1f..e6d4581609 100644 --- a/proposals/gc/Overview.md +++ b/proposals/gc/Overview.md @@ -411,7 +411,7 @@ For example: ) ``` All accesses are type-checked at validation time. -The structure operand of `struct.get/set` may either be a `ref` or an `ref null` for a structure type +The structure operand of `struct.get/set` may either be a `ref` or a `ref null` for a structure type In the latter case, the access involves a runtime null check that will trap upon failure. Structures are *allocated* with the `struct.new` instruction that accepts initialization values for each field. From 63802af91fd690175abcce370ef4c98288e2eb70 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 10 Nov 2023 16:19:48 +0100 Subject: [PATCH 38/43] Update proposals/gc/Overview.md --- proposals/gc/Overview.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/gc/Overview.md b/proposals/gc/Overview.md index e6d4581609..440769c40d 100644 --- a/proposals/gc/Overview.md +++ b/proposals/gc/Overview.md @@ -443,7 +443,7 @@ Elements are accessed with generic load/store instructions that take a reference ) ``` The element type of every access is checked at validation time. -The array operand of `array.get/set` may either be a `ref` or an `ref null` for an array type +The array operand of `array.get/set` may either be a `ref` or a `ref null` for an array type In the latter case, the access involves a runtime null check that will trap upon failure. The index is checked against the array's length at execution time. A trap occurs if the index is out of bounds. From 47d3f8bb241306b5b37a69abffcf817d84eba601 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 10 Nov 2023 16:19:53 +0100 Subject: [PATCH 39/43] Update proposals/gc/Overview.md --- proposals/gc/Overview.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/gc/Overview.md b/proposals/gc/Overview.md index 440769c40d..210c4e53be 100644 --- a/proposals/gc/Overview.md +++ b/proposals/gc/Overview.md @@ -508,7 +508,7 @@ These notions are already introduced by [typed function references](https://gith Plain references cannot be null, avoiding any runtime overhead for null checks when accessing a struct or array. -Nullable references are available as separate types called `ref null`, as per the . +Nullable references are available as separate types called `ref null`, as per the [typed function references proposal](https://github.com/WebAssembly/function-references/blob/master/proposals/function-references/Overview.md). Most value types, including all numeric types and nullable references are *defaultable*, which means that they have 0 or null as a default value. Other reference types are not defaultable. From 8339f47276d78af017e6f22dd2ebf9b5ec7484c8 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Fri, 10 Nov 2023 12:10:01 -0800 Subject: [PATCH 40/43] [spec] update note on constant expressions The global.get instruction can refer to previously defined globals in addition to imported ones now. Uses of global.get in data and element segments can refer to any global. --- document/core/valid/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 655e5f79d8..a965ff5201 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -2544,7 +2544,7 @@ Constant Expressions .. note:: - Currently, constant expressions occurring in :ref:`globals `, :ref:`element `, or :ref:`data ` segments are further constrained in that contained |GLOBALGET| instructions are only allowed to refer to *imported* globals. + Currently, constant expressions occurring in :ref:`globals ` are further constrained in that contained |GLOBALGET| instructions are only allowed to refer to *imported* or *previously defined* globals. This is enforced in the :ref:`validation rule for modules ` by constraining the context :math:`C` accordingly. The definition of constant expression may be extended in future versions of WebAssembly. From 3b34252b3e42bb62333841b811c894dc7e7f3dc2 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Fri, 10 Nov 2023 12:35:21 -0800 Subject: [PATCH 41/43] [spec] Also mention tables in constexpr note --- document/core/valid/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index a965ff5201..f3a57bd836 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -2544,7 +2544,7 @@ Constant Expressions .. note:: - Currently, constant expressions occurring in :ref:`globals ` are further constrained in that contained |GLOBALGET| instructions are only allowed to refer to *imported* or *previously defined* globals. + Currently, constant expressions occurring in :ref:`globals ` are further constrained in that contained |GLOBALGET| instructions are only allowed to refer to *imported* or *previously defined* globals. Constant expressions occurring in :ref:`tables ` may only have |GLOBALGET| instructions that refer to *imported* globals. This is enforced in the :ref:`validation rule for modules ` by constraining the context :math:`C` accordingly. The definition of constant expression may be extended in future versions of WebAssembly. From 8b512dd9d3fdfc54f94a099d4d03dfe3fb06284d Mon Sep 17 00:00:00 2001 From: Nick Fitzgerald Date: Fri, 10 Nov 2023 14:11:12 -0800 Subject: [PATCH 42/43] Fix off-by-one length in binary-gc.wast This avoids having two binary encoding errors which makes testing that a parser caught the expected error difficult. --- test/core/gc/binary-gc.wast | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/core/gc/binary-gc.wast b/test/core/gc/binary-gc.wast index 52cf02ace8..589573f2cc 100644 --- a/test/core/gc/binary-gc.wast +++ b/test/core/gc/binary-gc.wast @@ -2,7 +2,7 @@ (module binary "\00asm" "\01\00\00\00" "\01" ;; Type section id - "\05" ;; Type section length + "\04" ;; Type section length "\01" ;; Types vector length "\5e" ;; Array type, -0x22 "\78" ;; Storage type: i8 or -0x08 From 4ce065742b5a05c06c090a3b15189a5e7e799461 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Mon, 13 Nov 2023 08:59:39 +0100 Subject: [PATCH 43/43] Merge with spec, function-references, and gc