Add TypeOf as a kind of heap_type (which, given a function id returns its type)

Author: hra687261

src/concrete/concrete_ref.ml

@@ -22,7 +22,11 @@ let pp fmt = function
   | Extern _ -> pf fmt "externref"
   | Func _ -> pf fmt "funcref"
 
-let null = function Text.Func_ht -> Func None | Extern_ht -> Extern None
+(* TODO: Is this the same as Symbolic_ref.null? *)
+let null = function
+  | Text.Func_ht -> Func None
+  | Extern_ht -> Extern None
+  | TypeOf _ -> (* TODO: Func None? *) assert false
 
 let func (f : Kind.func) = Func (Some f)
 

src/ir/binary_encoder.ml

@@ -69,10 +69,26 @@ let write_char_indice buf c idx =
   Buffer.add_char buf c;
   write_indice buf idx
 
-let write_reftype buf ht =
-  match ht with
-  | Text.Func_ht -> Buffer.add_char buf '\x70'
-  | Extern_ht -> Buffer.add_char buf '\x6F'
+let write_reftype buf nullable ht =
+  match nullable with
+  | Text.Null -> begin
+    match ht with
+    | Text.Extern_ht -> Buffer.add_char buf '\x6F'
+    | Func_ht -> Buffer.add_char buf '\x70'
+    | TypeOf (Raw id) -> write_char_indice buf '\x63' id
+    | TypeOf _ -> assert false
+  end
+  | No_null -> begin
+    Buffer.add_char buf '\x64';
+    match ht with
+    | Text.Func_ht -> Buffer.add_char buf '\x70'
+    | Extern_ht -> Buffer.add_char buf '\x6F'
+    | TypeOf (Raw id) -> write_indice buf id
+    | TypeOf _ -> assert false
+  end
+(* TODO: TypeOf (Text id) Unreachable because there are no text ids in binary
+  format, the proper way to do it is by redefining ref_type and heap_type for
+  the binary format but it requires lots of changes. *)
 
 let get_char_valtype = function
   | Text.Num_type I32 -> '\x7F'
@@ -159,12 +175,12 @@ let write_memory_import buf
   write_limits buf limits
 
 let write_table_import buf
-  ({ modul_name; name; typ = limits, (_nullable, heaptype); _ } :
+  ({ modul_name; name; typ = limits, (nullable, heaptype); _ } :
     Text.Table.Type.t Origin.imported ) =
   write_string buf modul_name;
   write_string buf name;
   Buffer.add_char buf '\x01';
-  write_reftype buf heaptype;
+  write_reftype buf nullable heaptype;
   write_limits buf limits
 
 let write_func_import buf
@@ -441,7 +457,7 @@ let rec write_instr buf instr =
   | I64_extend32_s -> add_char '\xC4'
   | Ref_null rt ->
     add_char '\xD0';
-    write_reftype buf rt
+    write_reftype buf Text.Null rt
   | Ref_is_null -> add_char '\xD1'
   | Ref_func idx -> write_char_indice buf '\xD2' idx
   | I_trunc_sat_f (S32, S32, S) -> write_fc buf 0
@@ -509,16 +525,16 @@ and write_expr buf expr ~end_op_code =
   let end_op_code = Option.value end_op_code ~default:'\x0B' in
   Buffer.add_char buf end_op_code
 
-let write_table buf { Table.typ = limits, (_nullable, heaptype); init; _ } =
+let write_table buf { Table.typ = limits, (nullable, heaptype); init; _ } =
   match init with
   | Some e ->
     Buffer.add_char buf '\x40';
     Buffer.add_char buf '\x00';
-    write_reftype buf heaptype;
+    write_reftype buf nullable heaptype;
     write_limits buf limits;
     write_expr buf e ~end_op_code:None
   | None ->
-    write_reftype buf heaptype;
+    write_reftype buf nullable heaptype;
     write_limits buf limits
 
 let write_export buf cid ({ name; id } : Binary.Export.t) =
@@ -559,7 +575,7 @@ let write_locals buf locals =
       Buffer.add_char buf char )
     compressed
 
-let write_element buf ({ typ = _, ht; init; mode; _ } : Elem.t) =
+let write_element buf ({ typ = nullable, ht; init; mode; _ } : Elem.t) =
   let write_init buf init =
     let is_ref_func = ref true in
     encode_vector_list buf init (fun buf expr ->
@@ -581,7 +597,7 @@ let write_element buf ({ typ = _, ht; init; mode; _ } : Elem.t) =
     end
     else begin
       write_u32_of_int buf 5;
-      write_reftype buf ht;
+      write_reftype buf nullable ht;
       Buffer.add_buffer buf elem_buf
     end
   | Declarative ->
@@ -594,7 +610,7 @@ let write_element buf ({ typ = _, ht; init; mode; _ } : Elem.t) =
     end
     else begin
       write_u32_of_int buf 7;
-      write_reftype buf ht;
+      write_reftype buf nullable ht;
       Buffer.add_buffer buf elem_buf
     end
   | Active (Some 0, expr) ->
@@ -617,7 +633,7 @@ let write_element buf ({ typ = _, ht; init; mode; _ } : Elem.t) =
       write_u32_of_int buf 6;
       write_indice buf i;
       write_expr buf expr ~end_op_code:None;
-      write_reftype buf ht;
+      write_reftype buf nullable ht;
       Buffer.add_buffer buf elem_buf
     end
   | _ -> assert false

src/ir/text.ml

@@ -27,6 +27,13 @@ let pp_indice_not0 fmt = function
 
 let pp_indice_opt fmt = function None -> () | Some i -> pp_indice fmt i
 
+let compare_indice id1 id2 =
+  match (id1, id2) with
+  | Text s1, Text s2 -> String.compare s1 s2
+  | Raw i1, Raw i2 -> Int.compare i1 i2
+  | Text _, Raw _ -> 1
+  | Raw _, Text _ -> -1
+
 type nonrec num_type =
   | I32
   | I64
@@ -240,23 +247,32 @@ let pp_limits fmt { min; max } =
 (** Types *)
 
 type heap_type =
+  | TypeOf of indice
+  (* abs_heap_type *)
   | Func_ht
   | Extern_ht
 
 let pp_heap_type fmt = function
+  | TypeOf id -> pf fmt "%a" pp_indice id
   | Func_ht -> pf fmt "func"
   | Extern_ht -> pf fmt "extern"
 
 let heap_type_eq t1 t2 =
   (* TODO: this is wrong *)
   match (t1, t2) with
   | Func_ht, Func_ht | Extern_ht, Extern_ht -> true
+  | TypeOf id1, TypeOf id2 -> compare_indice id1 id2 = 0
   | _, _ -> false
 
 let compare_heap_type t1 t2 =
   (* TODO: this is wrong *)
-  let to_int = function Func_ht -> 0 | Extern_ht -> 1 in
-  Int.compare (to_int t1) (to_int t2)
+  match (t1, t2) with
+  | Func_ht, Func_ht | Extern_ht, Extern_ht -> 0
+  | TypeOf id1, TypeOf id2 -> compare_indice id1 id2
+  | TypeOf _, _ -> 1
+  | _, TypeOf _ -> -1
+  | Extern_ht, _ -> 1
+  | _, Extern_ht -> -1
 
 type nonrec ref_type = nullable * heap_type
 

src/ir/text.mli

@@ -18,6 +18,8 @@ val pp_indice : Format.formatter -> indice -> unit
 
 val pp_indice_opt : Format.formatter -> indice option -> unit
 
+val compare_indice : indice -> indice -> int
+
 type nonrec num_type =
   | I32
   | I64
@@ -160,6 +162,8 @@ val pp_limits : Format.formatter -> limits -> unit
 (** Types *)
 
 type heap_type =
+  | TypeOf of indice
+  (* abs_heap_type *)
   | Func_ht
   | Extern_ht
 

src/ir/wast.ml

@@ -53,13 +53,12 @@ type result =
   | Result_extern_ref
   | Result_func_ref
 
-let pp_result fmt = function
-  | Result_const c -> pf fmt "(%a)" pp_result_const c
-  | Result_func_ref | Result_extern_ref -> assert false
-
 let pp_result_bis fmt = function
   | Result_const c -> pf fmt "%a" pp_result_const c
-  | Result_extern_ref | Result_func_ref -> assert false
+  | Result_extern_ref -> pf fmt "ref.extern"
+  | Result_func_ref -> pf fmt "ref.func"
+
+let pp_result fmt r = Fmt.pf fmt "(%a)" pp_result_bis r
 
 let pp_results fmt r = list ~sep:sp pp_result_bis fmt r
 

src/owi.mli

@@ -230,6 +230,8 @@ module Text : sig
   (** Types *)
 
   type heap_type =
+    | TypeOf of indice
+    (* abs_heap_type *)
     | Func_ht
     | Extern_ht
 

src/parser/text_parser.mly

@@ -133,6 +133,7 @@ let null_opt ==
 let heap_type ==
   | FUNC; { Func_ht }
   | EXTERN; { Extern_ht }
+  | ~ = indice; <TypeOf>
 
 let ref_type ==
   | LPAR; REF; ~ = null_opt; ~ = heap_type; RPAR; <>

src/script/script.ml

@@ -112,6 +112,9 @@ let compare_result_const result (const : Concrete_value.t) =
   | Result_const (Nan_arith S64), F64 f ->
     let pos_nan = Float64.to_bits Float64.pos_nan in
     Int64.eq (Int64.logand (Float64.to_bits f) pos_nan) pos_nan
+  | Result_func_ref, Ref (Func (Some (Wasm _))) ->
+    (* TODO: FIX! This is probably unsound! *)
+    true
   | Result_const (Nan_arith _), _
   | Result_const (Nan_canon _), _
   | Result_const (Literal (Const_I32 _)), _
@@ -121,8 +124,10 @@ let compare_result_const result (const : Concrete_value.t) =
   | Result_const (Literal (Const_null _)), _
   | Result_const (Literal (Const_host _)), _ ->
     false
-  | _ ->
-    Log.err (fun m -> m "TODO: unimplemented Script.compare_result_const");
+  | _, _ ->
+    Log.err (fun m ->
+      m "TODO: unimplemented Script.compare_result_const %a %a" Wast.pp_result
+        result Concrete_value.pp const );
     assert false
 
 let value_of_const : Wast.const -> Concrete_value.t = function

src/symbolic/symbolic_ref.ml

@@ -22,7 +22,11 @@ let pp fmt = function
   | Extern _ -> pf fmt "externref"
   | Func _ -> pf fmt "funcref"
 
-let null = function Text.Func_ht -> Func None | Extern_ht -> Extern None
+let null = function
+  | Text.Func_ht -> Func None
+  | Extern_ht -> Extern None
+  | TypeOf _ -> assert false
+(* TODO: Should this be Func None? *)
 
 let func (f : Kind.func) = Func (Some f)
 

src/validate/binary_validate.ml

@@ -168,8 +168,11 @@ end = struct
     match (required, got) with
     | Text.Func_ht, Text.Func_ht -> true
     | Extern_ht, Extern_ht -> true
-    | Func_ht, Extern_ht -> false
-    | Extern_ht, Func_ht -> false
+    | TypeOf id1, TypeOf id2 ->
+      (* TODO: This should probably check the types of id1 and id2,
+        not the ids themselves *)
+      Text.compare_indice id1 id2 = 0
+    | _ -> false
 
   let match_types required got =
     match (required, got) with