Merge pull request #339 from WebAssembly/final

Add `final` attribute

Author: rossberg

.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:

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

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

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

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 =

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

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

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
 
@@ -176,7 +177,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 ^ ")"
 
@@ -241,9 +246,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
@@ -355,7 +361,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)
@@ -413,7 +419,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 *)

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])

interpreter/text/lexer.mll

@@ -175,6 +175,7 @@ rule token = parse
       | "field" -> FIELD
       | "mut" -> MUT
       | "sub" -> SUB
+      | "final" -> FINAL
       | "rec" -> REC
 
       | "nop" -> NOP

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) }

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
 

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
 

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 <typeidx>* <strtype>`
-  - the preexisting syntax with no `sub` clause is redefined to be a shorthand for a `sub` clause with empty `typeidx` list: `<strtype> == sub () <strtype>`
+  - `subtype ::= sub final? <typeidx>* <strtype>`
+  - the preexisting syntax with no `sub` clause is redefined to be a shorthand for a `sub` clause with empty `typeidx` list: `<strtype> == sub final () <strtype>`
   - 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(<ctxtype>)`  iff `$t = <ctxtype>`
-  - `expand(<ctxtype>) = <strtype>`
-    - where `unroll(<ctxttype>) = sub x* <strtype>`
+  - `expand(<ctxtype>)          = <strtype>`
+    - where `unroll(<ctxttype>) = sub final? x* <strtype>`
+
+* Finality of a type just checks the flag
+  - `final($t)                  = final(<ctxtype>)`  iff `$t = <ctxtype>`
+  - `final(<ctxtype>)           = final? =/= empty`
+    - where `unroll(<ctxttype>) = sub final? x* <strtype>`
 
 
 #### External Types
@@ -189,10 +194,11 @@ Some of the rules define a type as `ok` for a certain index, written `ok(x)`. Th
     - iff `<subtype0> ok($t)`
     - and `<subtype>* 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* <strtype> 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* <strtype> ok($t')`
     - iff `<strtype> ok`
     - and `(<strtype> <: 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 `(<subtype> == <subtype'>)*`
   - 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* <strtype>) == (sub $t'* <strtype'>)`
+* notably, two subtypes are equivalent if their structure is equivalent, they have equivalent supertypes, and their finality flag matches
+  - `(sub final1? $t* <strtype>) == (sub final2? $t'* <strtype'>)`
     - iff `<strtype> == <strtype'>`
     - 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 = <ctxtype>` and `$t' = <ctxtype'>` and `<ctxtype> == <ctxtype'>`
-    - 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))))
 ```
@@ -713,6 +720,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
 
@@ -722,6 +730,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
 
@@ -830,9 +839,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)
@@ -929,8 +939,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
@@ -942,9 +953,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'
 ```
 

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))))

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))))