[interpreter] Syntax and validation for new instructions

interpreter/binary/decode.ml

@@ -179,7 +179,7 @@ let vectype s =
 let heaptype s =
   let pos = pos s in
   either [
-    (fun s -> UseHT (typeuse s33 s));
+    (fun s -> UseHT (Inexact, typeuse s33 s));
     (fun s ->
       match s7 s with
       | -0x0c -> NoExnHT
@@ -194,7 +194,7 @@ let heaptype s =
       | -0x15 -> StructHT
       | -0x16 -> ArrayHT
       | -0x17 -> ExnHT
-      | -0x1e -> ExactHT (typeuse s32 s)
+      | -0x1e -> UseHT (Exact, typeuse s32 s)
       | _ -> error s pos "malformed heap type"
     )
   ] s
@@ -652,13 +652,19 @@ let rec instr s =
     | 0x15l -> let ht = heaptype s in ref_test (Null, ht)
     | 0x16l -> let ht = heaptype s in ref_cast (NoNull, ht)
     | 0x17l -> let ht = heaptype s in ref_cast (Null, ht)
-    | 0x18l | 0x19l as opcode ->
+    | 0x18l | 0x19l | 0x25l | 0x26l as opcode ->
       let flags = byte s in
       require (flags land 0xfc = 0) s (pos + 2) "malformed br_on_cast flags";
       let x = at idx s in
       let rt1 = ((if bit 0 flags then Null else NoNull), heaptype s) in
       let rt2 = ((if bit 1 flags then Null else NoNull), heaptype s) in
-      (if opcode = 0x18l then br_on_cast else br_on_cast_fail) x rt1 rt2
+      (match opcode with
+      | 0x18l -> br_on_cast x rt1 rt2
+      | 0x19l -> br_on_cast_fail x rt1 rt2
+      | 0x25l -> br_on_cast_desc x rt1 rt2
+      | 0x26l -> br_on_cast_desc_fail x rt1 rt2
+      | _ -> assert false
+      )
 
     | 0x1al -> any_convert_extern
     | 0x1bl -> extern_convert_any
@@ -667,6 +673,10 @@ let rec instr s =
     | 0x1dl -> i31_get_s
     | 0x1el -> i31_get_u
 
+    | 0x22l -> let x = at idx s in ref_get_desc x
+    | 0x23l -> let ht = heaptype s in ref_cast_desc (NoNull, ht)
+    | 0x24l -> let ht = heaptype s in ref_cast_desc (Null, ht)
+
     | n -> illegal2 s pos b n
     )
 

interpreter/binary/encode.ml

@@ -131,8 +131,8 @@ struct
     | NoExnHT -> s7 (-0x0c)
     | ExternHT -> s7 (-0x11)
     | NoExternHT -> s7 (-0x0e)
-    | UseHT ut -> typeuse s33 ut
-    | ExactHT ut -> s7 (-0x1e); typeuse u32 ut
+    | UseHT (Inexact, ut) -> typeuse s33 ut
+    | UseHT (Exact, ut) -> s7 (-0x1e); typeuse u32 ut
     | BotHT -> assert false
 
   let reftype = function
@@ -276,6 +276,12 @@ struct
     | BrOnCastFail (x, (nul1, t1), (nul2, t2)) ->
       let flags = bit 0 (nul1 = Null) + bit 1 (nul2 = Null) in
       op 0xfb; op 0x19; byte flags; idx x; heaptype t1; heaptype t2
+    | BrOnCastDesc (x, (nul1, t1), (nul2, t2)) ->
+      let flags = bit 0 (nul1 = Null) + bit 1 (nul2 = Null) in
+      op 0xfb; op 0x25; byte flags; idx x; heaptype t1; heaptype t2
+    | BrOnCastDescFail (x, (nul1, t1), (nul2, t2)) ->
+      let flags = bit 0 (nul1 = Null) + bit 1 (nul2 = Null) in
+      op 0xfb; op 0x26; byte flags; idx x; heaptype t1; heaptype t2
     | Return -> op 0x0f
     | Call x -> op 0x10; idx x
     | CallRef x -> op 0x14; idx x
@@ -429,6 +435,10 @@ struct
     | RefTest (Null, t) -> op 0xfb; op 0x15; heaptype t
     | RefCast (NoNull, t) -> op 0xfb; op 0x16; heaptype t
     | RefCast (Null, t) -> op 0xfb; op 0x17; heaptype t
+    | RefCastDesc (NoNull, t) -> op 0xfb; op 0x23; heaptype t
+    | RefCastDesc (Null, t) -> op 0xfb; op 0x24; heaptype t
+
+    | RefGetDesc x -> op 0xfb; op 0x22; idx x
 
     | RefI31 -> op 0xfb; op 0x1c
     | I31Get S -> op 0xfb; op 0x1d

interpreter/runtime/aggr.ml

@@ -58,8 +58,8 @@ let type_of_array (Array (dt, _)) = dt
 let () =
   let type_of_ref' = !Value.type_of_ref' in
   Value.type_of_ref' := function
-    | StructRef s -> UseHT (Def (type_of_struct s))
-    | ArrayRef a -> UseHT (Def (type_of_array a))
+    | StructRef s -> UseHT (Exact, Def (type_of_struct s))
+    | ArrayRef a -> UseHT (Exact, Def (type_of_array a))
     | r -> type_of_ref' r
 
 let string_of_field = function

interpreter/runtime/exn.ml

@@ -28,7 +28,7 @@ let () =
 let () =
   let type_of_ref' = !Value.type_of_ref' in
   Value.type_of_ref' := function
-    | ExnRef e -> UseHT (Def (type_of e))
+    | ExnRef e -> UseHT (Exact, (Def (type_of e)))
     | r -> type_of_ref' r
 
 let () =

interpreter/runtime/instance.ml

@@ -45,7 +45,7 @@ let () =
 let () =
   let type_of_ref' = !Value.type_of_ref' in
   Value.type_of_ref' := function
-    | FuncRef f -> UseHT (Def (Func.type_of f))
+    | FuncRef f -> UseHT (Exact, (Def (Func.type_of f)))
     | r -> type_of_ref' r
 
 let () =

interpreter/script/js.ml

@@ -298,9 +298,9 @@ let rec statify_typeuse rts = function
   | ht -> rts, ht
 
 and statify_heaptype rts = function
-  | UseHT ut ->
+  | UseHT (exact, ut) ->
     let rts', ut' = statify_typeuse rts ut in
-    rts', UseHT ut'
+    rts', UseHT (exact, ut')
   | ht -> rts, ht
 
 and statify_reftype rts = function

interpreter/syntax/ast.ml

@@ -181,6 +181,8 @@ and instr' =
   | BrOnNonNull of labelidx              (* break on type inverted *)
   | BrOnCast of labelidx * reftype * reftype     (* break on type *)
   | BrOnCastFail of labelidx * reftype * reftype (* break on type inverted *)
+  | BrOnCastDesc of labelidx * reftype * reftype (* break on descriptor cast *)
+  | BrOnCastDescFail of labelidx * reftype * reftype (* break on descriptor cast inverted *)
   | Return                               (* break from function body *)
   | Call of funcidx                      (* call function *)
   | CallRef of typeidx                   (* call function through reference *)
@@ -222,6 +224,8 @@ and instr' =
   | RefAsNonNull                         (* type cast *)
   | RefTest of reftype                   (* type test *)
   | RefCast of reftype                   (* type cast *)
+  | RefCastDesc of reftype               (* descriptor type cast *)
+  | RefGetDesc of typeidx                (* read descriptor *)
   | RefEq                                (* reference equality *)
   | RefI31                               (* scalar reference *)
   | I31Get of sx                         (* read scalar *)

interpreter/syntax/free.ml

@@ -82,8 +82,7 @@ and heaptype = function
   | FuncHT | NoFuncHT -> empty
   | ExnHT | NoExnHT -> empty
   | ExternHT | NoExternHT -> empty
-  | UseHT x -> typeuse x
-  | ExactHT x -> typeuse x
+  | UseHT (_, x) -> typeuse x
   | BotHT -> empty
 
 and reftype = function
@@ -143,7 +142,8 @@ let rec instr (e : instr) =
   | Block (bt, es) | Loop (bt, es) -> blocktype bt ++ block es
   | If (bt, es1, es2) -> blocktype bt ++ block es1 ++ block es2
   | Br x | BrIf x | BrOnNull x | BrOnNonNull x -> labels (idx x)
-  | BrOnCast (x, t1, t2) | BrOnCastFail (x, t1, t2) ->
+  | BrOnCast (x, t1, t2) | BrOnCastFail (x, t1, t2)
+  | BrOnCastDesc (x, t1, t2) | BrOnCastDescFail (x, t1, t2) ->
     labels (idx x) ++ reftype t1 ++ reftype t2
   | BrTable (xs, x) -> list (fun x -> labels (idx x)) (x::xs)
   | Return -> empty
@@ -169,7 +169,8 @@ let rec instr (e : instr) =
   | MemoryInit (x, y) -> memories (idx x) ++ datas (idx y)
   | DataDrop x -> datas (idx x)
   | RefIsNull | RefAsNonNull -> empty
-  | RefTest t | RefCast t -> reftype t
+  | RefTest t | RefCast t | RefCastDesc t -> reftype t
+  | RefGetDesc x -> types (idx x)
   | RefEq -> empty
   | RefNull t -> heaptype t
   | RefFunc x -> funcs (idx x)

interpreter/syntax/mnemonics.ml

@@ -35,6 +35,8 @@ let br_on_null x = BrOnNull x
 let br_on_non_null x = BrOnNonNull x
 let br_on_cast x t1 t2 = BrOnCast (x, t1, t2)
 let br_on_cast_fail x t1 t2 = BrOnCastFail (x, t1, t2)
+let br_on_cast_desc x t1 t2 = BrOnCastDesc (x, t1, t2)
+let br_on_cast_desc_fail x t1 t2 = BrOnCastDescFail (x, t1, t2)
 
 let catch x1 x2 = Catch (x1, x2)
 let catch_ref x1 x2 = CatchRef (x1, x2)
@@ -173,6 +175,8 @@ let ref_is_null = RefIsNull
 let ref_as_non_null = RefAsNonNull  
 let ref_test t = RefTest t
 let ref_cast t = RefCast t
+let ref_cast_desc t = RefCastDesc t
+let ref_get_desc x = RefGetDesc x
 let ref_eq = RefEq
 
 let ref_i31 = RefI31

interpreter/syntax/types.ml

@@ -5,6 +5,7 @@ type localidx = int32
 type name = Utf8.unicode
 
 type null = NoNull | Null
+type exact = Exact | Inexact
 type mut = Cons | Var
 type init = Set | Unset
 type final = NoFinal | Final
@@ -18,7 +19,7 @@ and vectype = V128T
 and heaptype =
   | AnyHT | NoneHT | EqHT | I31HT | StructHT | ArrayHT
   | FuncHT | NoFuncHT | ExnHT | NoExnHT | ExternHT | NoExternHT
-  | UseHT of typeuse | ExactHT of typeuse | BotHT
+  | UseHT of exact * typeuse | BotHT
 and reftype = null * heaptype
 and valtype = NumT of numtype | VecT of vectype | RefT of reftype | BotT
 
@@ -173,8 +174,7 @@ and subst_heaptype s = function
   | NoExnHT -> NoExnHT
   | ExternHT -> ExternHT
   | NoExternHT -> NoExternHT
-  | UseHT t -> UseHT (subst_typeuse s t)
-  | ExactHT t -> ExactHT (subst_typeuse s t)
+  | UseHT (exact, t) -> UseHT (exact, subst_typeuse s t)
   | BotHT -> BotHT
 
 and subst_reftype s = function
@@ -282,9 +282,12 @@ let unroll_deftype (dt : deftype) : subtype =
   let RecT sts = unroll_rectype rt in
   Lib.List32.nth sts i
 
-(* TODO: consider returning a desctype here. *)
+let expand_deftype_to_desctype (dt : deftype) : desctype =
+  let SubT (_, _, dt) = unroll_deftype dt in
+  dt
+
 let expand_deftype (dt : deftype) : comptype =
-  let SubT (_, _, DescT (_, _, st)) = unroll_deftype dt in
+  let DescT (_, _, st) = expand_deftype_to_desctype dt in
   st
 
 
@@ -350,8 +353,8 @@ and string_of_heaptype = function
   | NoExnHT -> "noexn"
   | ExternHT -> "extern"
   | NoExternHT -> "noextern"
-  | UseHT ut -> string_of_typeuse ut
-  | ExactHT ut -> "(exact " ^ (string_of_typeuse ut) ^ ")"
+  | UseHT (Inexact, ut) -> string_of_typeuse ut
+  | UseHT (Exact, ut) -> "(exact " ^ (string_of_typeuse ut) ^ ")"
   | BotHT -> "something"
 
 and string_of_reftype = function

interpreter/text/arrange.ml

@@ -513,6 +513,10 @@ let rec instr e =
       "br_on_cast " ^ idx x, [Atom (reftype t1); Atom (reftype t2)]
     | BrOnCastFail (x, t1, t2) ->
       "br_on_cast_fail " ^ idx x, [Atom (reftype t1); Atom (reftype t2)]
+    | BrOnCastDesc (x, t1, t2) ->
+      "br_on_cast_desc " ^ idx x, [Atom (reftype t1); Atom (reftype t2)]
+    | BrOnCastDescFail (x, t1, t2) ->
+      "br_on_cast_desc_fail " ^ idx x, [Atom (reftype t1); Atom (reftype t2)]
     | Return -> "return", []
     | Call x -> "call " ^ idx x, []
     | CallRef x -> "call_ref " ^ idx x, []
@@ -557,6 +561,8 @@ let rec instr e =
     | RefAsNonNull -> "ref.as_non_null", []
     | RefTest t -> "ref.test", [Atom (reftype t)]
     | RefCast t -> "ref.cast", [Atom (reftype t)]
+    | RefCastDesc t -> "ref.cast_desc", [Atom (reftype t)]
+    | RefGetDesc x -> "ref.get_desc " ^ idx x, []
     | RefEq -> "ref.eq", []
     | RefI31 -> "ref.i31", []
     | I31Get sx -> "i31.get" ^ ext sx, []

interpreter/text/lexer.mll

@@ -204,6 +204,8 @@ rule token = parse
       | "br_on_non_null" -> BR_ON_NULL br_on_non_null
       | "br_on_cast" -> BR_ON_CAST br_on_cast
       | "br_on_cast_fail" -> BR_ON_CAST br_on_cast_fail
+      | "br_on_cast_desc" -> BR_ON_CAST br_on_cast_desc
+      | "br_on_cast_desc_fail" -> BR_ON_CAST br_on_cast_desc_fail
       | "return" -> RETURN
       | "if" -> IF
       | "then" -> THEN
@@ -338,6 +340,8 @@ rule token = parse
       | "ref.as_non_null" -> REF_AS_NON_NULL
       | "ref.test" -> REF_TEST
       | "ref.cast" -> REF_CAST
+      | "ref.cast_desc" -> REF_CAST_DESC
+      | "ref.get_desc" -> REF_GET_DESC
       | "ref.eq" -> REF_EQ
 
       | "ref.i31" -> REF_I31

interpreter/text/parser.mly

@@ -304,7 +304,7 @@ let parse_annots (m : module_) : Custom.section list =
 %token<string Source.phrase -> Ast.instr' * Value.num> CONST
 %token<Ast.instr'> UNARY BINARY TEST COMPARE CONVERT
 %token REF_NULL REF_FUNC REF_I31 REF_STRUCT REF_ARRAY REF_EXN REF_EXTERN REF_HOST
-%token REF_EQ REF_IS_NULL REF_AS_NON_NULL REF_TEST REF_CAST
+%token REF_EQ REF_IS_NULL REF_AS_NON_NULL REF_TEST REF_CAST REF_CAST_DESC REF_GET_DESC
 %token<Ast.instr'> I31_GET
 %token<Ast.idx -> Ast.instr'> STRUCT_NEW ARRAY_NEW ARRAY_GET
 %token STRUCT_SET
@@ -376,8 +376,8 @@ heaptype :
   | NOEXN { fun c -> NoExnHT }
   | EXTERN { fun c -> ExternHT }
   | NOEXTERN { fun c -> NoExternHT }
-  | idx { fun c -> UseHT (Idx ($1 c type_).it) }
-  | LPAR EXACT idx RPAR { fun c -> ExactHT (Idx ($3 c type_).it) }
+  | idx { fun c -> UseHT (Inexact, Idx ($1 c type_).it) }
+  | LPAR EXACT idx RPAR { fun c -> UseHT (Exact, Idx ($3 c type_).it) }
 
 reftype :
   | LPAR REF null_opt heaptype RPAR { fun c -> ($3, $4 c) }
@@ -633,6 +633,8 @@ plaininstr :
   | REF_AS_NON_NULL { fun c -> ref_as_non_null }
   | REF_TEST reftype { fun c -> ref_test ($2 c) }
   | REF_CAST reftype { fun c -> ref_cast ($2 c) }
+  | REF_CAST_DESC reftype { fun c -> ref_cast_desc ($2 c) }
+  | REF_GET_DESC idx { fun c -> ref_get_desc ($2 c type_) }
   | REF_EQ { fun c -> ref_eq }
   | REF_I31 { fun c -> ref_i31 }
   | I31_GET { fun c -> $1 }

interpreter/valid/match.ml

@@ -27,8 +27,7 @@ and top_of_heaptype c = function
   | FuncHT | NoFuncHT -> FuncHT
   | ExnHT | NoExnHT -> ExnHT
   | ExternHT | NoExternHT -> ExternHT
-  | UseHT ut -> top_of_typeuse c ut
-  | ExactHT ut -> top_of_typeuse c ut
+  | UseHT (_, ut) -> top_of_typeuse c ut
   | BotHT -> assert false
 
 let top_of_valtype c = function
@@ -50,8 +49,7 @@ and bot_of_heaptype c = function
   | FuncHT | NoFuncHT -> NoFuncHT
   | ExnHT | NoExnHT -> NoExnHT
   | ExternHT | NoExternHT -> NoExternHT
-  | UseHT ut -> bot_of_typeuse c ut
-  | ExactHT ut -> bot_of_typeuse c ut
+  | UseHT (_, ut) -> bot_of_typeuse c ut
   | BotHT -> assert false
 
 
@@ -89,10 +87,14 @@ let rec match_heaptype c t1 t2 =
   | NoFuncHT, t -> match_heaptype c t FuncHT
   | NoExnHT, t -> match_heaptype c t ExnHT
   | NoExternHT, t -> match_heaptype c t ExternHT
-  | UseHT (Idx x1), _ -> match_heaptype c (UseHT (Def (lookup c x1))) t2
-  | _, UseHT (Idx x2) -> match_heaptype c t1 (UseHT (Def (lookup c x2)))
-  | UseHT (Def dt1), UseHT (Def dt2) -> match_deftype c dt1 dt2
-  | UseHT (Def dt), t ->
+  | UseHT (exact, Idx x1), _ ->
+    match_heaptype c (UseHT (exact, Def (lookup c x1))) t2
+  | _, UseHT (exact, Idx x2) ->
+    match_heaptype c t1 (UseHT (exact, Def (lookup c x2)))
+  | UseHT (_, Def dt1), UseHT (Inexact, Def dt2) -> match_deftype c dt1 dt2
+  | UseHT (Exact, Def dt1), UseHT (Exact, Def dt2) ->
+    match_deftype c dt1 dt2 && match_deftype c dt2 dt1
+  | UseHT (_, Def dt), t ->
     (match expand_deftype dt, t with
     | StructT _, AnyHT -> true
     | StructT _, EqHT -> true
@@ -103,13 +105,6 @@ let rec match_heaptype c t1 t2 =
     | FuncT _, FuncHT -> true
     | _ -> false
     )
-  | ExactHT (Idx x1), _ ->
-    match_heaptype c (ExactHT (Def (lookup c x1))) t2
-  | _, ExactHT (Idx x2) ->
-    match_heaptype c t1 (ExactHT (Def (lookup c x2)))
-  | ExactHT (Def dt1), ExactHT (Def dt2) ->
-    match_deftype c dt1 dt2 && match_deftype c dt2 dt1
-  | ExactHT (Def dt1), _ -> match_heaptype c (UseHT (Def dt1)) t2
   | BotHT, _ -> true
   | _, _ -> t1 = t2
 
@@ -160,8 +155,10 @@ and match_comptype c ct1 ct2 =
 and match_deftype c dt1 dt2 =
   dt1 == dt2 ||  (* optimisation *)
   let s = subst_of c in subst_deftype s dt1 = subst_deftype s dt2 ||
-  let SubT (_fin, uts1, _st) = unroll_deftype dt1 in
-  List.exists (fun ut1 -> match_heaptype c (UseHT ut1) (UseHT (Def dt2))) uts1
+  let SubT (_fin, uts1, _dt) = unroll_deftype dt1 in
+  List.exists (fun ut1 ->
+    match_heaptype c (UseHT (Inexact, ut1)) (UseHT (Inexact, (Def dt2)))
+  ) uts1
 
 let match_tagtype c (TagT ut1) (TagT ut2) =
   match ut1, ut2 with

interpreter/valid/match.mli

@@ -18,6 +18,7 @@ val bot_of_comptype : context -> comptype -> heaptype
 (* Subtyping *)
 
 val match_numtype : context -> numtype -> numtype -> bool
+val match_heaptype : context -> heaptype -> heaptype -> bool
 val match_reftype : context -> reftype -> reftype -> bool
 val match_valtype : context -> valtype -> valtype -> bool