diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 25994a68a..214ba48d3 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -63,7 +63,7 @@ jobs: - run: pip install bikeshed && bikeshed update - run: pip install six - run: sudo apt-get update -y && sudo apt-get install -y latexmk texlive-latex-recommended texlive-latex-extra texlive-fonts-recommended - - run: pip install sphinx==4.0.0 + - run: pip install sphinx==5.1.0 - run: cd document/core && make all - uses: actions/upload-artifact@v2 with: diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 630af976c..11687069b 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -256,8 +256,12 @@ let sub_type s = | Some i when i = -0x30 land 0x7f -> skip 1 s; let xs = vec (var_type u32) s in - SubT (xs, str_type s) - | _ -> SubT ([], str_type s) + SubT (NoFinal, xs, str_type s) + | Some i when i = -0x32 land 0x7f -> + skip 1 s; + let xs = vec (var_type u32) s in + SubT (Final, xs, str_type s) + | _ -> SubT (Final, [], str_type s) let def_type s = match peek s with diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 0644cb6b6..93b9845dc 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -173,8 +173,9 @@ struct | DefFuncT ft -> s7 (-0x20); func_type ft let sub_type = function - | SubT ([], st) -> str_type st - | SubT (xs, st) -> s7 (-0x30); vec (var_type u32) xs; str_type st + | SubT (Final, [], st) -> str_type st + | SubT (Final, xs, st) -> s7 (-0x32); vec (var_type u32) xs; str_type st + | SubT (NoFinal, xs, st) -> s7 (-0x30); vec (var_type u32) xs; str_type st let def_type = function | RecT [st] -> sub_type st diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 90e486ee7..4e95592aa 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -244,7 +244,7 @@ let rec step (c : config) : config = | CallIndirect (x, y), Num (I32 i) :: vs -> let f = func_ref c.frame.inst x i e.at in if - Match.eq_var_type [] (DynX (type_ c.frame.inst y)) (DynX (Func.type_inst_of f)) + Match.match_var_type [] (DynX (Func.type_inst_of f)) (DynX (type_ c.frame.inst y)) then vs, [Invoke f @@ e.at] else diff --git a/interpreter/host/spectest.ml b/interpreter/host/spectest.ml index 252a17d01..be8e32f17 100644 --- a/interpreter/host/spectest.ml +++ b/interpreter/host/spectest.ml @@ -29,7 +29,7 @@ let memory = let func f ft = let x = Types.alloc_uninit () in - Types.init x (CtxT ([(DynX x, SubT ([], DefFuncT ft))], 0l)); + Types.init x (CtxT ([(DynX x, SubT (Final, [], DefFuncT ft))], 0l)); ExternFunc (Func.alloc_host x (f ft)) let print_value v = diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml index cd6ce21ad..c7c874b29 100644 --- a/interpreter/script/js.ml +++ b/interpreter/script/js.ml @@ -270,7 +270,7 @@ let value v = | Ref _ -> assert false let invoke ft vs at = - let dt = RecT [SubT ([], DefFuncT ft)] in + let dt = RecT [SubT (Final, [], DefFuncT ft)] in [dt @@ at], FuncImport (subject_type_idx @@ at) @@ at, List.concat (List.map value vs) @ [Call (subject_idx @@ at) @@ at] @@ -380,7 +380,8 @@ let assert_return ress ts at = let i32 = NumT I32T let anyref = RefT (Null, AnyHT) let eqref = RefT (Null, EqHT) -let func_def_type ts1 ts2 at = RecT [SubT ([], DefFuncT (FuncT (ts1, ts2)))] @@ at +let func_def_type ts1 ts2 at = + RecT [SubT (Final, [], DefFuncT (FuncT (ts1, ts2)))] @@ at let wrap item_name wrap_action wrap_assertion at = let itypes, idesc, action = wrap_action at in diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml index 3b980fc33..5ee8e712c 100644 --- a/interpreter/syntax/free.ml +++ b/interpreter/syntax/free.ml @@ -107,7 +107,7 @@ let str_type = function | DefFuncT ft -> func_type ft let sub_type = function - | SubT (xs, st) -> list var_type xs ++ str_type st + | SubT (_fin, xs, st) -> list var_type xs ++ str_type st let def_type = function | RecT sts -> list sub_type sts diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml index 6abb7cd61..bec9a2f2e 100644 --- a/interpreter/syntax/types.ml +++ b/interpreter/syntax/types.ml @@ -7,6 +7,7 @@ type name = Utf8.unicode type null = NoNull | Null type mut = Cons | Var type init = Set | Unset +type final = NoFinal | Final type 'a limits = {min : 'a; max : 'a option} type type_addr = .. @@ -38,7 +39,7 @@ type str_type = | DefArrayT of array_type | DefFuncT of func_type -type sub_type = SubT of var list * str_type +type sub_type = SubT of final * var list * str_type type def_type = RecT of sub_type list type ctx_type = CtxT of (var * sub_type) list * int32 @@ -180,7 +181,11 @@ let string_of_null = function | NoNull -> "" | Null -> "null " -and string_of_mut s = function +let string_of_final = function + | NoFinal -> "" + | Final -> " final" + +let string_of_mut s = function | Cons -> s | Var -> "(mut " ^ s ^ ")" @@ -245,9 +250,10 @@ let string_of_str_type = function | DefFuncT ft -> "func " ^ string_of_func_type ft let string_of_sub_type = function - | SubT ([], st) -> string_of_str_type st - | SubT (xs, st) -> - String.concat " " ("sub" :: List.map string_of_var xs) ^ + | SubT (Final, [], st) -> string_of_str_type st + | SubT (fin, xs, st) -> + String.concat " " + (("sub" ^ string_of_final fin) :: List.map string_of_var xs) ^ " (" ^ string_of_str_type st ^ ")" let string_of_def_type = function @@ -359,7 +365,7 @@ let subst_str_type s = function | DefFuncT ft -> DefFuncT (subst_func_type s ft) let subst_sub_type s = function - | SubT (xs, st) -> SubT (List.map s xs, subst_str_type s st) + | SubT (fin, xs, st) -> SubT (fin, List.map s xs, subst_str_type s st) let subst_def_type s = function | RecT sts -> RecT (List.map (subst_sub_type s) sts) @@ -417,7 +423,7 @@ let unroll_ctx_type (ct : ctx_type) : sub_type = let expand_ctx_type (ct : ctx_type) : str_type = match unroll_ctx_type ct with - | SubT (_, st) -> st + | SubT (_, _, st) -> st (* Dynamic Types *) diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index 379dd2801..980f90677 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -86,6 +86,10 @@ let null = function | NoNull -> "" | Null -> "null " +let final = function + | NoFinal -> "" + | Final -> " final" + let ref_type_raw (nul, t) = Atom (null nul ^ heap_type t) @@ -110,9 +114,10 @@ let str_type st = | DefFuncT ft -> func_type ft let sub_type = function - | SubT ([], st) -> str_type st - | SubT (xs, st) -> - Node (String.concat " " ("sub" :: List.map var_type xs), [str_type st]) + | SubT (Final, [], st) -> str_type st + | SubT (fin, xs, st) -> + Node (String.concat " " + (("sub" ^ final fin ):: List.map var_type xs), [str_type st]) let def_type i j st = Node ("type $" ^ nat (i + j), [sub_type st]) diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll index 78e9a0738..8110c897e 100644 --- a/interpreter/text/lexer.mll +++ b/interpreter/text/lexer.mll @@ -175,6 +175,7 @@ rule token = parse | "field" -> FIELD | "mut" -> MUT | "sub" -> SUB + | "final" -> FINAL | "rec" -> REC | "nop" -> NOP diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index ecb6218d8..2a26171ee 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -212,7 +212,7 @@ let anon_fields (c : context) n at = bind "field" c.fields n at let inline_func_type (c : context) ft at = - let st = SubT ([], DefFuncT ft) in + let st = SubT (Final, [], DefFuncT ft) in match Lib.List.index_where (function | CtxT ([(_, st')], 0l) -> st = st' @@ -248,7 +248,7 @@ let inline_func_type_explicit (c : context) x ft at = %token ANYREF NULLREF EQREF I31REF STRUCTREF ARRAYREF %token FUNCREF NULLFUNCREF EXTERNREF NULLEXTERNREF %token ANY NONE EQ I31 REF NOFUNC EXTERN NOEXTERN NULL -%token MUT FIELD STRUCT ARRAY SUB REC +%token MUT FIELD STRUCT ARRAY SUB FINAL REC %token UNREACHABLE NOP DROP SELECT %token BLOCK END IF THEN ELSE LOOP %token BR BR_IF BR_TABLE BR_ON_NULL BR_ON_NON_NULL BR_ON_CAST BR_ON_CAST_FAIL @@ -439,9 +439,11 @@ str_type : | LPAR FUNC func_type RPAR { fun c -> DefFuncT ($3 c) } sub_type : - | str_type { fun c -> SubT ([], $1 c) } + | str_type { fun c -> SubT (Final, [], $1 c) } | LPAR SUB var_list str_type RPAR - { fun c -> SubT (List.map (fun x -> StatX x.it) ($3 c type_), $4 c) } + { fun c -> SubT (NoFinal, List.map (fun x -> StatX x.it) ($3 c type_), $4 c) } + | LPAR SUB FINAL var_list str_type RPAR + { fun c -> SubT (Final, List.map (fun x -> StatX x.it) ($4 c type_), $5 c) } table_type : | limits ref_type { fun c -> TableT ($1, $2 c) } diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml index 733282e5b..1d812aa2b 100644 --- a/interpreter/valid/match.ml +++ b/interpreter/valid/match.ml @@ -127,8 +127,8 @@ and eq_str_type c dt1 dt2 = | DefFuncT ft1, DefFuncT ft2 -> eq_func_type c ft1 ft2 | _, _ -> false -and eq_sub_type c (SubT (xs1, st1)) (SubT (xs2, st2)) = - eq_list eq_var_type c xs1 xs2 && eq_str_type c st1 st2 +and eq_sub_type c (SubT (fin1, xs1, st1)) (SubT (fin2, xs2, st2)) = + fin1 = fin2 && eq_list eq_var_type c xs1 xs2 && eq_str_type c st1 st2 and eq_def_type c (RecT sts1) (RecT sts2) = eq_list eq_sub_type c sts1 sts2 @@ -261,10 +261,9 @@ and match_str_type c dt1 dt2 = and match_var_type c x1 x2 = eq_var x1 x2 || not (is_rec_var x1 || is_rec_var x2) && eq_ctx_type c (lookup c x1) (lookup c x2) || - let SubT (xs, _) = unroll_ctx_type (lookup c x1) in + let SubT (_fin, xs, _st) = unroll_ctx_type (lookup c x1) in List.exists (fun x -> match_var_type c x x2) xs - let match_table_type c (TableT (lim1, t1)) (TableT (lim2, t2)) = match_limits c lim1 lim2 && eq_ref_type c t1 t2 diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index bfc404242..2305b3471 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -170,13 +170,16 @@ let check_str_type (c : context) (st : str_type) at = | DefFuncT ft -> check_func_type c ft at let check_sub_type (c : context) (st : sub_type) x at = - let SubT (xs, st) = st in + let SubT (fin, xs, st) = st in check_str_type c st at; List.iter (fun xi -> let xi = as_stat_var xi in require (xi < x) at ("forward use of type " ^ I32.to_string_u xi ^ " in sub type definition"); - require (match_str_type c.types st (expand_ctx_type (type_ c (xi @@ at)))) at + let SubT (fini, _, sti) = unroll_ctx_type (type_ c (xi @@ at)) in + require (fini = NoFinal) at + ("sub type " ^ I32.to_string_u x ^ " has final super type " ^ I32.to_string_u xi); + require (match_str_type c.types st sti) at ("sub type " ^ I32.to_string_u x ^ " does not match super type " ^ I32.to_string_u xi) ) xs diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index 029ba4bd8..b443049c0 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -111,8 +111,8 @@ New abbreviations are introduced for reference types in binary and text format, - Note that the number of type section entries is now the number of recursion groups rather than the number of individual types. * `subtype` is a new category of type defining a single type, as a subtype of possible other types - - `subtype ::= sub * ` - - the preexisting syntax with no `sub` clause is redefined to be a shorthand for a `sub` clause with empty `typeidx` list: ` == sub () ` + - `subtype ::= sub final? * ` + - the preexisting syntax with no `sub` clause is redefined to be a shorthand for a `sub` clause with empty `typeidx` list: ` == sub final () ` - Note: This allows multiple supertypes. For the MVP, it is restricted to at most one supertype. * `strtype` is a new category of types covering the different forms of concrete structural reference types @@ -155,8 +155,13 @@ In the case of `C.funcs`, it is an invariant that all types [expand](#auxiliary- * Expanding a type definition unrolls it and returns its plain definition - `expand($t) = expand()` iff `$t = ` - - `expand() = ` - - where `unroll() = sub x* ` + - `expand() = ` + - where `unroll() = sub final? x* ` + +* Finality of a type just checks the flag + - `final($t) = final()` iff `$t = ` + - `final() = final? =/= empty` + - where `unroll() = sub final? x* ` #### External Types @@ -189,10 +194,11 @@ Some of the rules define a type as `ok` for a certain index, written `ok(x)`. Th - iff ` ok($t)` - and `* ok($t+1)` -* an individual subtype is valid if its definition is valid, matches every supertype, and no supertype has an index higher than its own - - `sub $t* ok($t')` +* an individual subtype is valid if its definition is valid, matches every supertype, and no supertype is final or has an index higher than its own + - `sub final? $t* ok($t')` - iff ` ok` - and `( <: expand($t))*` + - and `(not final($t))*` - and `($t < $t')*` - Note: the upper bound on the supertype indices ensures that subtyping hierarchies are never circular, because definitions need to be ordered. @@ -253,10 +259,11 @@ With that: - iff `( == )*` - Note: This rule is only used on types that have been tied, which prevents looping. -* notably, two subtypes are equivalent if their structure is equivalent and they have equivalent supertypes - - `(sub $t* ) == (sub $t'* )` +* notably, two subtypes are equivalent if their structure is equivalent, they have equivalent supertypes, and their finality flag matches + - `(sub final1? $t* ) == (sub final2? $t'* )` - iff ` == ` - and `($t == $t')*` + - and `final1? = final2?` Example: As explained above, the mutually recursive types ``` @@ -311,7 +318,7 @@ In the [existing rules](https://github.com/WebAssembly/function-references/propo * Type indices are subtypes if they either define [equivalent](#type-equivalence) types or a suitable (direct or indirect) subtype relation has been declared - `$t <: $t'` - if `$t = ` and `$t' = ` and ` == ` - - or `unroll($t) = sub $t1* $t'' $t2* strtype` and `$t'' <: $t'` + - or `unroll($t) = sub final? $t1* $t'' $t2* strtype` and `$t'' <: $t'` - Note: This rule climbs the supertype hierarchy until an equivalent type has been found. Effectively, this means that subtyping is "nominal" modulo type canonicalisation. @@ -446,7 +453,7 @@ Note: This assumes that there is at most one supertype. For hierarchies with mul Example: Consider three types and corresponding RTTs: ``` -(type $A (struct)) +(type $A (sub (struct))) (type $B (sub $A (struct (field i32)))) (type $C (sub $B (struct (field i32 i64)))) ``` @@ -716,6 +723,7 @@ The opcode for heap types is encoded as an `s33`. | -0x21 | `struct ft*` | `ft* : vec(fieldtype)` | shorthand | | -0x22 | `array ft` | `ft : fieldtype` | shorthand | | -0x30 | `sub $t* st` | `$t* : vec(typeidx)`, `st : strtype` | | +| -0x32 | `sub final $t* st` | `$t* : vec(typeidx)`, `st : strtype` | | #### Defined Types @@ -725,6 +733,7 @@ The opcode for heap types is encoded as an `s33`. | -0x22 | `array ft` | `ft : fieldtype` | shorthand | | -0x30 | `sub $t* st` | `$t* : vec(typeidx)`, `st : strtype` | shorthand | | -0x31 | `rec dt*` | `dt* : vec(subtype)` | | +| -0x32 | `sub final $t* st` | `$t* : vec(typeidx)`, `st : strtype` | shorthand | #### Field Types @@ -833,9 +842,10 @@ C |- array ft ok ``` C |- st ok (C |- st <: expand(C(x)))* +(not final(C(x)))* (x < x')* --------------------------- -C |- sub x* st ok(x') +---------------------------- +C |- sub final? x* st ok(x') C |- st ok(x) C |- st'* ok(x+1) @@ -932,8 +942,9 @@ C |- array ft == array ft' ``` (C |- x == x')* C |- st == st' ------------------------------ -C |- sub x* st == sub x'* st' +final1? = final2? +--------------------------------------------- +C |- sub final1? x* st == sub final2? x'* st' ``` ### Subtyping @@ -945,9 +956,9 @@ C |- x == x' ------------ C |- x <: x' -unroll(C(x)) = sub (x1* x'' x2*) st +unroll(C(x)) = sub final? (x1* x'' x2*) st C |- x'' <: x' ------------------------------------ +------------------------------------------ C |- x <: x' ``` diff --git a/test/core/gc/br_on_cast.wast b/test/core/gc/br_on_cast.wast index fd191dab6..67034fcef 100644 --- a/test/core/gc/br_on_cast.wast +++ b/test/core/gc/br_on_cast.wast @@ -86,7 +86,7 @@ ;; Concrete Types (module - (type $t0 (struct)) + (type $t0 (sub (struct))) (type $t1 (sub $t0 (struct (field i32)))) (type $t1' (sub $t0 (struct (field i32)))) (type $t2 (sub $t1 (struct (field i32 i32)))) diff --git a/test/core/gc/br_on_cast_fail.wast b/test/core/gc/br_on_cast_fail.wast index 5c5199ac8..4ae59e006 100644 --- a/test/core/gc/br_on_cast_fail.wast +++ b/test/core/gc/br_on_cast_fail.wast @@ -86,7 +86,7 @@ ;; Concrete Types (module - (type $t0 (struct)) + (type $t0 (sub (struct))) (type $t1 (sub $t0 (struct (field i32)))) (type $t1' (sub $t0 (struct (field i32)))) (type $t2 (sub $t1 (struct (field i32 i32)))) diff --git a/test/core/gc/ref_cast.wast b/test/core/gc/ref_cast.wast index bca221984..b5bb163fd 100644 --- a/test/core/gc/ref_cast.wast +++ b/test/core/gc/ref_cast.wast @@ -97,7 +97,7 @@ ;; Concrete Types (module - (type $t0 (struct)) + (type $t0 (sub (struct))) (type $t1 (sub $t0 (struct (field i32)))) (type $t1' (sub $t0 (struct (field i32)))) (type $t2 (sub $t1 (struct (field i32 i32)))) diff --git a/test/core/gc/ref_eq.wast b/test/core/gc/ref_eq.wast index d7f3a906a..c8e090442 100644 --- a/test/core/gc/ref_eq.wast +++ b/test/core/gc/ref_eq.wast @@ -1,6 +1,6 @@ (module - (type $st (struct)) - (type $st' (struct (field i32))) + (type $st (sub (struct))) + (type $st' (sub (struct (field i32)))) (type $at (array i8)) (type $st-sub1 (sub $st (struct))) (type $st-sub2 (sub $st (struct))) diff --git a/test/core/gc/ref_test.wast b/test/core/gc/ref_test.wast index 4370d1674..da769b35b 100644 --- a/test/core/gc/ref_test.wast +++ b/test/core/gc/ref_test.wast @@ -180,7 +180,7 @@ ;; Concrete Types (module - (type $t0 (struct)) + (type $t0 (sub (struct))) (type $t1 (sub $t0 (struct (field i32)))) (type $t1' (sub $t0 (struct (field i32)))) (type $t2 (sub $t1 (struct (field i32 i32)))) diff --git a/test/core/gc/type-subtyping.wast b/test/core/gc/type-subtyping.wast index 4941d5eea..fc5d3d6b3 100644 --- a/test/core/gc/type-subtyping.wast +++ b/test/core/gc/type-subtyping.wast @@ -1,19 +1,19 @@ ;; Definitions (module - (type $e0 (array i32)) + (type $e0 (sub (array i32))) (type $e1 (sub $e0 (array i32))) - (type $e2 (array anyref)) + (type $e2 (sub (array anyref))) (type $e3 (sub (array (ref null $e0)))) (type $e4 (sub (array (ref $e1)))) - (type $m1 (array (mut i32))) + (type $m1 (sub (array (mut i32)))) (type $m2 (sub $m1 (array (mut i32)))) ) (module - (type $e0 (struct)) + (type $e0 (sub (struct))) (type $e1 (sub $e0 (struct))) (type $e2 (sub $e1 (struct (field i32)))) (type $e3 (sub $e2 (struct (field i32 (ref null $e0))))) @@ -22,10 +22,10 @@ ) (module - (type $s (struct)) + (type $s (sub (struct))) (type $s' (sub $s (struct))) - (type $f1 (func (param (ref $s')) (result anyref))) + (type $f1 (sub (func (param (ref $s')) (result anyref)))) (type $f2 (sub $f1 (func (param (ref $s)) (result (ref any))))) (type $f3 (sub $f2 (func (param (ref null $s)) (result (ref $s))))) (type $f4 (sub $f3 (func (param (ref null struct)) (result (ref $s'))))) @@ -35,14 +35,14 @@ ;; Recursive definitions (module - (type $t (struct (field anyref))) + (type $t (sub (struct (field anyref)))) (rec (type $r (sub $t (struct (field (ref $r)))))) (type $t' (sub $r (struct (field (ref $r) i32)))) ) (module (rec - (type $r1 (struct (field i32 (ref $r1)))) + (type $r1 (sub (struct (field i32 (ref $r1))))) ) (rec (type $r2 (sub $r1 (struct (field i32 (ref $r3))))) @@ -52,8 +52,8 @@ (module (rec - (type $a1 (struct (field i32 (ref $a2)))) - (type $a2 (struct (field i64 (ref $a1)))) + (type $a1 (sub (struct (field i32 (ref $a2))))) + (type $a2 (sub (struct (field i64 (ref $a1))))) ) (rec (type $b1 (sub $a2 (struct (field i64 (ref $a1) i32)))) @@ -67,7 +67,7 @@ (module (rec - (type $t1 (func (param i32 (ref $t3)))) + (type $t1 (sub (func (param i32 (ref $t3))))) (type $t2 (sub $t1 (func (param i32 (ref $t2))))) (type $t3 (sub $t2 (func (param i32 (ref $t1))))) ) @@ -88,8 +88,8 @@ (module (rec - (type $t1 (func (result i32 (ref $u1)))) - (type $u1 (func (result f32 (ref $t1)))) + (type $t1 (sub (func (result i32 (ref $u1))))) + (type $u1 (sub (func (result f32 (ref $t1))))) ) (rec @@ -116,36 +116,222 @@ ;; Runtime types (module - (rec (type $t1 (func (result (ref null $t1))))) + (type $t0 (sub (func (result (ref null func))))) + (rec (type $t1 (sub $t0 (func (result (ref null $t1)))))) (rec (type $t2 (sub $t1 (func (result (ref null $t2)))))) + (func $f0 (type $t0) (ref.null func)) (func $f1 (type $t1) (ref.null $t1)) (func $f2 (type $t2) (ref.null $t2)) - (table funcref (elem $f1 $f2)) + (table funcref (elem $f0 $f1 $f2)) (func (export "run") - (block (result (ref null $t1)) (call_indirect (type $t1) (i32.const 0))) - (block (result (ref null $t2)) (call_indirect (type $t2) (i32.const 1))) - (block (result (ref null $t1)) (ref.cast $t1 (table.get (i32.const 0)))) + (block (result (ref null func)) (call_indirect (type $t0) (i32.const 0))) + (block (result (ref null func)) (call_indirect (type $t0) (i32.const 1))) + (block (result (ref null func)) (call_indirect (type $t0) (i32.const 2))) + (block (result (ref null $t1)) (call_indirect (type $t1) (i32.const 1))) + (block (result (ref null $t1)) (call_indirect (type $t1) (i32.const 2))) + (block (result (ref null $t2)) (call_indirect (type $t2) (i32.const 2))) + + (block (result (ref null $t0)) (ref.cast $t0 (table.get (i32.const 0)))) + (block (result (ref null $t0)) (ref.cast $t0 (table.get (i32.const 1)))) + (block (result (ref null $t0)) (ref.cast $t0 (table.get (i32.const 2)))) (block (result (ref null $t1)) (ref.cast $t1 (table.get (i32.const 1)))) - (block (result (ref null $t2)) (ref.cast $t2 (table.get (i32.const 1)))) + (block (result (ref null $t1)) (ref.cast $t1 (table.get (i32.const 2)))) + (block (result (ref null $t2)) (ref.cast $t2 (table.get (i32.const 2)))) (br 0) ) - (func (export "fail") - (block (result (ref null $t1)) (call_indirect (type $t1) (i32.const 1))) + (func (export "fail1") + (block (result (ref null $t1)) (call_indirect (type $t1) (i32.const 0))) + (br 0) + ) + (func (export "fail2") + (block (result (ref null $t1)) (call_indirect (type $t2) (i32.const 0))) + (br 0) + ) + (func (export "fail3") + (block (result (ref null $t1)) (call_indirect (type $t2) (i32.const 1))) + (br 0) + ) + + (func (export "fail4") + (ref.cast $t1 (table.get (i32.const 0))) + (br 0) + ) + (func (export "fail5") + (ref.cast $t2 (table.get (i32.const 0))) + (br 0) + ) + (func (export "fail6") + (ref.cast $t2 (table.get (i32.const 1))) (br 0) ) ) (assert_return (invoke "run")) -(assert_trap (invoke "fail") "indirect call") +(assert_trap (invoke "fail1") "indirect call") +(assert_trap (invoke "fail2") "indirect call") +(assert_trap (invoke "fail3") "indirect call") +(assert_trap (invoke "fail4") "cast") +(assert_trap (invoke "fail5") "cast") +(assert_trap (invoke "fail6") "cast") + +(module + (type $t1 (sub (func))) + (type $t2 (sub final (func))) + + (func $f1 (type $t1)) + (func $f2 (type $t2)) + (table funcref (elem $f1 $f2)) + + (func (export "fail1") + (block (call_indirect (type $t1) (i32.const 1))) + ) + (func (export "fail2") + (block (call_indirect (type $t2) (i32.const 0))) + ) + + (func (export "fail3") + (ref.cast $t1 (table.get (i32.const 1))) + (drop) + ) + (func (export "fail4") + (ref.cast $t2 (table.get (i32.const 0))) + (drop) + ) +) +(assert_trap (invoke "fail1") "indirect call") +(assert_trap (invoke "fail2") "indirect call") +(assert_trap (invoke "fail3") "cast") +(assert_trap (invoke "fail4") "cast") + + + +;; Linking + +(module + (type $t0 (sub (func (result (ref null func))))) + (rec (type $t1 (sub $t0 (func (result (ref null $t1)))))) + (rec (type $t2 (sub $t1 (func (result (ref null $t2)))))) + + (func (export "f0") (type $t0) (ref.null func)) + (func (export "f1") (type $t1) (ref.null $t1)) + (func (export "f2") (type $t2) (ref.null $t2)) +) +(register "M") + +(module + (type $t0 (sub (func (result (ref null func))))) + (rec (type $t1 (sub $t0 (func (result (ref null $t1)))))) + (rec (type $t2 (sub $t1 (func (result (ref null $t2)))))) + + (func (import "M" "f0") (type $t0)) + (func (import "M" "f1") (type $t0)) + (func (import "M" "f1") (type $t1)) + (func (import "M" "f2") (type $t0)) + (func (import "M" "f2") (type $t1)) + (func (import "M" "f2") (type $t2)) +) + +(assert_unlinkable + (module + (type $t0 (sub (func (result (ref null func))))) + (rec (type $t1 (sub $t0 (func (result (ref null $t1)))))) + (rec (type $t2 (sub $t1 (func (result (ref null $t2)))))) + (func (import "M" "f0") (type $t1)) + ) + "incompatible import type" +) + +(assert_unlinkable + (module + (type $t0 (sub (func (result (ref null func))))) + (rec (type $t1 (sub $t0 (func (result (ref null $t1)))))) + (rec (type $t2 (sub $t1 (func (result (ref null $t2)))))) + (func (import "M" "f0") (type $t2)) + ) + "incompatible import type" +) + +(assert_unlinkable + (module + (type $t0 (sub (func (result (ref null func))))) + (rec (type $t1 (sub $t0 (func (result (ref null $t1)))))) + (rec (type $t2 (sub $t1 (func (result (ref null $t2)))))) + (func (import "M" "f1") (type $t2)) + ) + "incompatible import type" +) + +(module + (type $t1 (sub (func))) + (type $t2 (sub final (func))) + (func (export "f1") (type $t1)) + (func (export "f2") (type $t2)) +) +(register "M2") + +(assert_unlinkable + (module + (type $t1 (sub (func))) + (type $t2 (sub final (func))) + (func (import "M2" "f1") (type $t2)) + ) + "incompatible import type" +) +(assert_unlinkable + (module + (type $t1 (sub (func))) + (type $t2 (sub final (func))) + (func (import "M2" "f2") (type $t1)) + ) + "incompatible import type" +) + + + +;; Finality violation + +(assert_invalid + (module + (type $t (func)) + (type $s (sub $t (func))) + ) + "sub type" +) + +(assert_invalid + (module + (type $t (struct)) + (type $s (sub $t (struct))) + ) + "sub type" +) + +(assert_invalid + (module + (type $t (sub final (func))) + (type $s (sub $t (func))) + ) + "sub type" +) + +(assert_invalid + (module + (type $t (sub (func))) + (type $s (sub final $t (func))) + (type $u (sub $s (func))) + ) + "sub type" +) + ;; Invalid subtyping definitions (assert_invalid (module - (type $a0 (array i32)) + (type $a0 (sub (array i32))) (type $s0 (sub $a0 (struct))) ) "sub type" @@ -153,7 +339,7 @@ (assert_invalid (module - (type $f0 (func (param i32) (result i32))) + (type $f0 (sub (func (param i32) (result i32)))) (type $s0 (sub $f0 (struct))) ) "sub type" @@ -161,7 +347,7 @@ (assert_invalid (module - (type $s0 (struct)) + (type $s0 (sub (struct))) (type $a0 (sub $s0 (array i32))) ) "sub type" @@ -169,7 +355,7 @@ (assert_invalid (module - (type $f0 (func (param i32) (result i32))) + (type $f0 (sub (func (param i32) (result i32)))) (type $a0 (sub $f0 (array i32))) ) "sub type" @@ -177,7 +363,7 @@ (assert_invalid (module - (type $s0 (struct)) + (type $s0 (sub (struct))) (type $f0 (sub $s0 (func (param i32) (result i32)))) ) "sub type" @@ -185,7 +371,7 @@ (assert_invalid (module - (type $a0 (array i32)) + (type $a0 (sub (array i32))) (type $f0 (sub $a0 (func (param i32) (result i32)))) ) "sub type" @@ -193,7 +379,7 @@ (assert_invalid (module - (type $a0 (array i32)) + (type $a0 (sub (array i32))) (type $a1 (sub $a0 (array i64))) ) "sub type" @@ -201,7 +387,7 @@ (assert_invalid (module - (type $s0 (struct (field i32))) + (type $s0 (sub (struct (field i32)))) (type $s1 (sub $s0 (struct (field i64)))) ) "sub type" @@ -209,7 +395,7 @@ (assert_invalid (module - (type $f0 (func)) + (type $f0 (sub (func))) (type $f1 (sub $f0 (func (param i32)))) ) "sub type"