Update exact function imports (#75)

tlively · web-flow · commit 9477928d646f · 2025-11-05T06:21:40.000-08:00
Address feedback from #72, including by using (exact, deftype) pairs instead of full heaptypes where possible in the interpreter. Update the overview accordingly. Also fix #74 by introducing a new externtype binary encoding for exact function imports rather than using an s33 in the existing function import variant.
diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml
@@ -320,11 +320,12 @@ let tabletype s =
 
 let externtype s =
   match byte s with
-  | 0x00 -> ExternFuncT (heaptype s)
+  | 0x00 -> ExternFuncT (Inexact, typeuse idx s)
   | 0x01 -> ExternTableT (tabletype s)
   | 0x02 -> ExternMemoryT (memorytype s)
   | 0x03 -> ExternGlobalT (globaltype s)
   | 0x04 -> ExternTagT (tagtype s)
+  | 0x20 -> ExternFuncT (Exact, typeuse idx s)
   | _ -> error s (pos s - 1) "malformed import kind"
 
 
diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml
@@ -207,7 +207,8 @@ struct
     | TableT (at, lim, t) -> reftype t; limits at lim
 
   let externtype = function
-    | ExternFuncT ht -> byte 0x00; heaptype ht
+    | ExternFuncT (Inexact, ut) -> byte 0x00; typeuse u32 ut
+    | ExternFuncT (Exact, ut) -> byte 0x20; typeuse u32 ut
     | ExternTableT tt -> byte 0x01; tabletype tt
     | ExternMemoryT mt -> byte 0x02; memorytype mt
     | ExternGlobalT gt -> byte 0x03; globaltype gt
diff --git a/interpreter/host/env.ml b/interpreter/host/env.ml
@@ -42,8 +42,8 @@ let exit vs =
 
 let lookup name et =
   match Utf8.encode name, et with
-  | "abort", ExternFuncT (UseHT (_exact, ut)) ->
+  | "abort", ExternFuncT (_exact, ut) ->
     ExternFunc (Func.alloc_host (deftype_of_typeuse ut) abort)
-  | "exit", ExternFuncT (UseHT (_exact, ut)) ->
+  | "exit", ExternFuncT (_exact, ut) ->
     ExternFunc (Func.alloc_host (deftype_of_typeuse ut) exit)
   | _ -> raise Not_found
diff --git a/interpreter/runtime/instance.ml b/interpreter/runtime/instance.ml
@@ -75,7 +75,7 @@ let externtype_of c = function
   | ExternGlobal glob -> ExternGlobalT (Global.type_of glob)
   | ExternMemory mem -> ExternMemoryT (Memory.type_of mem)
   | ExternTable tab -> ExternTableT (Table.type_of tab)
-  | ExternFunc func -> ExternFuncT (UseHT (Exact, Def (Func.type_of func)))
+  | ExternFunc func -> ExternFuncT (Exact, Def (Func.type_of func))
 
 let export inst name =
   try Some (List.assoc name inst.exports) with Not_found -> None
diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml
@@ -424,7 +424,7 @@ let invoke dt vs at =
   let rts0 = Lib.List32.init subject_type_idx (fun i -> dummy, (dummy, i)) in
   let rts, i = statify_deftype rts0 dt in
   List.map (fun (_, (rt, _)) -> rt @@ at) (Lib.List32.drop subject_type_idx rts),
-  ExternFuncT (UseHT (Inexact, (Idx i))),
+  ExternFuncT (Inexact, Idx i),
   List.concat (List.map value vs) @ [Call (subject_idx @@ at) @@ at]
 
 let get t at =
@@ -606,9 +606,9 @@ let wrap item_name wrap_action wrap_assertion at =
   let imports =
     [ Import (Utf8.decode "module", item_name, idesc) @@ at;
       Import (Utf8.decode "spectest", Utf8.decode "hostref",
-        ExternFuncT (UseHT (Inexact, (Idx 1l)))) @@ at;
+        ExternFuncT (Inexact, Idx 1l)) @@ at;
       Import (Utf8.decode "spectest", Utf8.decode "eq_ref",
-        ExternFuncT (UseHT (Inexact, (Idx 2l)))) @@ at;
+        ExternFuncT (Inexact, Idx 2l)) @@ at;
     ]
   in
   let item =
@@ -775,7 +775,7 @@ let of_action env act =
     "call(" ^ of_inst_opt env x_opt ^ ", " ^ of_name name ^ ", " ^
       "[" ^ String.concat ", " (List.map of_value vs) ^ "])",
     (match lookup_export env x_opt name act.at with
-    | ExternFuncT (UseHT (_exact, (Def dt))) ->
+    | ExternFuncT (_exact, Def dt) ->
       let (_, out) as ft = functype_of_comptype (expand_deftype dt) in
       if is_js_functype ft then
         None
diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml
@@ -414,8 +414,10 @@ let exporttype_of (m : module_) (ex : export) : exporttype =
     | FuncX x ->
       let dts = funcs xts @ List.map (fun f ->
         let Func (y, _, _) = f.it in
-        UseHT (Exact, Def (Lib.List32.nth dts y.it))) m.it.funcs in
-      ExternFuncT (Lib.List32.nth dts x.it)
+        (Exact, Def (Lib.List32.nth dts y.it))) m.it.funcs
+      in
+      let (exact, dt) = Lib.List32.nth dts x.it in
+      ExternFuncT (exact, dt)
   in ExportT (name, subst_externtype (subst_of dts) xt)
 
 let moduletype_of (m : module_) : moduletype =
diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml
@@ -129,7 +129,7 @@ let externtype = function
   | ExternGlobalT gt -> globaltype gt
   | ExternMemoryT mt -> memorytype mt
   | ExternTableT tt -> tabletype tt
-  | ExternFuncT ht -> heaptype ht
+  | ExternFuncT (_, ut) -> typeuse ut
 
 let blocktype = function
   | VarBlockType x -> types (idx x)
diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
@@ -49,7 +49,7 @@ type externtype =
   | ExternGlobalT of globaltype
   | ExternMemoryT of memorytype
   | ExternTableT of tabletype
-  | ExternFuncT of heaptype
+  | ExternFuncT of exact * typeuse
 
 type exporttype = ExportT of name * externtype
 type importtype = ImportT of name * name * externtype
@@ -125,8 +125,6 @@ let unpacked_fieldtype (FieldT (_mut, t)) = unpacked_storagetype t
 let idx_of_typeuse = function Idx x -> x | _ -> assert false
 let deftype_of_typeuse = function Def dt -> dt | _ -> assert false
 
-let typeuse_of_heaptype = function UseHT (_, ut) -> ut | _ -> assert false
-
 let structtype_of_comptype = function StructT fts -> fts | _ -> assert false
 let arraytype_of_comptype = function ArrayT ft -> ft | _ -> assert false
 let functype_of_comptype = function FuncT rt2 -> rt2 | _ -> assert false
@@ -141,7 +139,7 @@ let tags = List.filter_map (function ExternTagT tt -> Some tt | _ -> None)
 let globals = List.filter_map (function ExternGlobalT gt -> Some gt | _ -> None)
 let memories = List.filter_map (function ExternMemoryT mt -> Some mt | _ -> None)
 let tables = List.filter_map (function ExternTableT tt -> Some tt | _ -> None)
-let funcs = List.filter_map (function ExternFuncT ft -> Some ft | _ -> None)
+let funcs = List.filter_map (function ExternFuncT (exact, ut) -> Some (exact, ut) | _ -> None)
 
 
 (* Substitution *)
@@ -237,7 +235,7 @@ let subst_externtype s = function
   | ExternGlobalT gt -> ExternGlobalT (subst_globaltype s gt)
   | ExternMemoryT mt -> ExternMemoryT (subst_memorytype s mt)
   | ExternTableT tt -> ExternTableT (subst_tabletype s tt)
-  | ExternFuncT ht -> ExternFuncT (subst_heaptype s ht)
+  | ExternFuncT (exact, ut) -> ExternFuncT (exact, subst_typeuse s ut)
 
 
 let subst_exporttype s = function
@@ -448,8 +446,8 @@ let string_of_externtype = function
   | ExternGlobalT gt -> "global " ^ string_of_globaltype gt
   | ExternMemoryT mt -> "memory " ^ string_of_memorytype mt
   | ExternTableT tt -> "table " ^ string_of_tabletype tt
-  | ExternFuncT ht -> "func " ^ string_of_heaptype ht
-
+  | ExternFuncT (Inexact, ut) -> "func " ^ string_of_typeuse ut
+  | ExternFuncT (Exact, ut) -> "func exact " ^ string_of_typeuse ut
 
 let string_of_exporttype = function
   | ExportT (name, xt) ->
diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml
@@ -84,10 +84,9 @@ let heaptype t = string_of_heaptype t
 let valtype t = string_of_valtype t
 let storagetype t = string_of_storagetype t
 
-let heaptypeuse = function
-  | UseHT (Inexact, ut) -> typeuse ut
-  | UseHT (Exact, ut) -> Node ("exact", [typeuse ut])
-  | _ -> assert false
+let exacttypeuse = function
+  | (Inexact, ut) -> typeuse ut
+  | (Exact, ut) -> Node ("exact", [typeuse ut])
 
 let final = function
   | NoFinal -> ""
@@ -713,7 +712,8 @@ let importtype fx tx mx tgx gx = function
   | ExternGlobalT gt -> incr gx; Node ("global $" ^ nat (!gx - 1), globaltype gt)
   | ExternMemoryT mt -> incr mx; Node ("memory $" ^ nat (!mx - 1), memorytype mt)
   | ExternTableT tt -> incr tx; Node ("table $" ^ nat (!tx - 1), tabletype tt)
-  | ExternFuncT ht -> incr fx; Node ("func $" ^ nat (!fx - 1), [heaptypeuse ht])
+  | ExternFuncT (exact, ut) ->
+    incr fx; Node ("func $" ^ nat (!fx - 1), [exacttypeuse (exact, ut)])
 
 let import fx tx mx ex gx im =
   let Import (module_name, item_name, xt) = im.it in
diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly
@@ -492,9 +492,9 @@ limits :
 typeuse :
   | LPAR TYPE idx RPAR { fun c -> $3 c type_ }
 
-heaptypeuse :
-  | LPAR EXACT typeuse RPAR { fun c -> UseHT (Exact, Idx ($3 c).it) }
-  | typeuse { fun c -> UseHT (Inexact, Idx ($1 c).it) }
+exacttypeuse :
+  | LPAR EXACT typeuse RPAR { fun c -> (Exact, $3 c) }
+  | typeuse { fun c -> (Inexact, $1 c) }
 
 /* Immediates */
 
@@ -998,20 +998,17 @@ func_fields :
       let y = inline_functype c' (fst $1 c') loc in
       let Func (_, ls, es) = snd $1 c' in
       [Func (y, ls, es) @@ loc], [], [] }
-  | inline_import heaptypeuse func_fields_import  /* Sugar */
+  | inline_import exacttypeuse func_fields_import  /* Sugar */
     { fun c x loc ->
-      let exact, y = match ($2 c) with
-        | UseHT (exact, Idx y) -> exact, y
-        | _ -> assert false
-      in
-      let y = inline_functype_explicit c (y @@ loc) ($3 c) in
+      let exact, y = $2 c in
+      let y = inline_functype_explicit c y ($3 c) in
       [],
-      [Import (fst $1, snd $1, ExternFuncT (UseHT (exact, Idx y.it))) @@ loc ], [] }
+      [Import (fst $1, snd $1, ExternFuncT (exact, Idx y.it)) @@ loc ], [] }
   | inline_import func_fields_import  /* Sugar */
     { fun c x loc ->
       let y = inline_functype c ($2 c) loc in
       [],
-      [Import (fst $1, snd $1, ExternFuncT (UseHT (Inexact, Idx y.it))) @@ loc ], [] }
+      [Import (fst $1, snd $1, ExternFuncT (Inexact, Idx y.it)) @@ loc ], [] }
   | inline_export func_fields  /* Sugar */
     { fun c x loc ->
       let fns, ims, exs = $2 c x loc in fns, ims, $1 (FuncX x) c :: exs }
@@ -1253,9 +1250,9 @@ table_fields :
 /* Imports & Exports */
 
 externtype :
-  | LPAR FUNC bindidx_opt heaptypeuse RPAR
+  | LPAR FUNC bindidx_opt exacttypeuse RPAR
     { fun c -> ignore ($3 c anon_func bind_func);
-      fun () -> ExternFuncT ($4 c) }
+      fun () -> let exact, y = $4 c in ExternFuncT (exact, Idx y.it) }
   | LPAR TAG bindidx_opt typeuse RPAR
     { fun c -> ignore ($3 c anon_tag bind_tag);
       fun () -> ExternTagT (TagT (Idx ($4 c).it)) }
@@ -1276,7 +1273,7 @@ externtype :
       fun () ->
         let exact, ft = $4 c in
         let y = inline_functype c ft $loc($4) in
-        ExternFuncT (UseHT (exact, Idx y.it)) }
+        ExternFuncT (exact, Idx y.it) }
 
 import :
   | LPAR IMPORT name name externtype RPAR
diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml
@@ -187,5 +187,6 @@ let match_externtype c xt1 xt2 =
   | ExternGlobalT gt1, ExternGlobalT gt2 -> match_globaltype c gt1 gt2
   | ExternMemoryT mt1, ExternMemoryT mt2 -> match_memorytype c mt1 mt2
   | ExternTableT tt1, ExternTableT tt2 -> match_tabletype c tt1 tt2
-  | ExternFuncT ht1, ExternFuncT ht2 -> match_heaptype c ht1 ht2
+  | ExternFuncT (exact1, ut1), ExternFuncT (exact2, ut2) -> 
+    match_heaptype c (UseHT (exact1, ut1)) (UseHT (exact2, ut2))
   | _, _ -> false
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
@@ -22,7 +22,7 @@ type context =
   globals : globaltype list;
   memories : memorytype list;
   tables : tabletype list;
-  funcs : heaptype list;
+  funcs : (exact * deftype) list;
   datas : unit list;
   elems : reftype list;
   locals : localtype list;
@@ -243,7 +243,6 @@ let check_rectype (c : context) (rt : rectype) at : context =
     (fun i st -> check_subtype_sub c' st (Int32.add x i) at) sts;
   c'
 
-
 let check_tagtype (c : context) (tt : tagtype) at =
   let TagT ut = tt in
   let (ts1, ts2) = func_type c (idx_of_typeuse ut @@ at) in
@@ -283,14 +282,8 @@ let check_externtype (c : context) (xt : externtype) at =
     check_memorytype c mt at
   | ExternTableT tt ->
     check_tabletype c tt at
-  | ExternFuncT (UseHT (_exact, ut)) ->
+  | ExternFuncT (_exact, ut) ->
     let _ft = func_type c (idx_of_typeuse ut @@ at) in ()
-  | ExternFuncT ht ->
-    error at
-      ("external function type should have defined type, but has " ^
-       string_of_heaptype ht)
-
-
 
 let diff_reftype (nul1, ht1) (nul2, ht2) =
   match nul2 with
@@ -639,7 +632,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
     c.results -->... [], []
 
   | Call x ->
-    let dt = deftype_of_typeuse (typeuse_of_heaptype (func c x)) in
+    let (_, dt) = func c x in
     let (ts1, ts2) = functype_of_comptype (expand_deftype dt) in
     ts1 --> ts2, []
 
@@ -656,7 +649,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
     (ts1 @ [NumT (numtype_of_addrtype at)]) --> ts2, []
 
   | ReturnCall x ->
-    let dt = deftype_of_typeuse (typeuse_of_heaptype (func c x)) in
+    let (_, dt) = func c x in
     let (ts1, ts2) = functype_of_comptype (expand_deftype dt) in
     require (match_resulttype c.types ts2 c.results) e.at
       ("type mismatch: current function requires result type " ^
@@ -832,9 +825,9 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
     [] --> [RefT (Null, ht)], []
 
   | RefFunc x ->
-    let ht = func c x in
+    let (exact, dt) = func c x in
     refer_func c x;
-    [] --> [RefT (NoNull, ht)], []
+    [] --> [RefT (NoNull, UseHT (exact, Def dt))], []
 
   | RefIsNull ->
     let (_nul, ht) = peek_ref 0 s e.at in
@@ -1152,7 +1145,7 @@ let check_local (c : context) (loc : local) : localtype =
 let check_func (c : context) (f : func) : context =
   let Func (x, _ls, _es) = f.it in
   let _ft = func_type c x in
-  {c with funcs = c.funcs @ [UseHT (Exact, Def (type_ c x))]}
+  {c with funcs = c.funcs @ [(Exact, type_ c x)]}
 
 let check_func_body (c : context) (f : func) =
   let Func (x, ls, es) = f.it in
@@ -1248,7 +1241,7 @@ let check_type (c : context) (t : type_) : context =
 
 let check_start (c : context) (start : start) =
   let Start x = start.it in
-  let dt = deftype_of_typeuse (typeuse_of_heaptype (func c x)) in
+  let (_, dt) = func c x in
   let ft = functype_of_comptype (expand_deftype dt) in
   require (ft = ([], [])) start.at
     "start function must not have parameters or results"
@@ -1261,7 +1254,8 @@ let check_import (c : context) (im : import) : context =
   | ExternGlobalT gt -> {c with globals = c.globals @ [gt]}
   | ExternMemoryT mt -> {c with memories = c.memories @ [mt]}
   | ExternTableT tt -> {c with tables = c.tables @ [tt]}
-  | ExternFuncT ht -> {c with funcs = c.funcs @ [ht]}
+  | ExternFuncT (exact, ut) ->
+    {c with funcs = c.funcs @ [(exact, deftype_of_typeuse ut)]}
 
 module NameSet = Set.Make(struct type t = Ast.name let compare = compare end)
 
@@ -1273,7 +1267,7 @@ let check_export (c : context) (ex : export) : exporttype =
     | GlobalX x -> ExternGlobalT (global c x)
     | MemoryX x -> ExternMemoryT (memory c x)
     | TableX x -> ExternTableT (table c x)
-    | FuncX x -> ExternFuncT (func c x)
+    | FuncX x -> let exact, dt = func c x in ExternFuncT (exact, Def dt)
   in ExportT (name, xt)
 
 let check_list f xs (c : context) : context =
diff --git a/proposals/custom-descriptors/Overview.md b/proposals/custom-descriptors/Overview.md
@@ -387,26 +387,26 @@ Function imports already give a type for the imported function;
 we must now make it possible for that type to be exact.
 
 The external type of a function import is currently represented as a `typeuse`,
-but we can change that to `heaptype` to allow for exact types.
+so we can just make it a pair of `exact` and `typeuse`:
 
 ```
-externtype ::= ... | func heaptype
+externtype ::= ... | func exact? heaptype
 ```
 
 In the text format,
 function import types are given by `typeuse` and its associated sugar.
 We don't want to allow exactness everywhere `typeuse`
 appears in the text format,
 so instead of extending the syntax of `typeuse`,
-we introduce a new production, `heaptypeuse`.
+we introduce a new production, `exacttypeuse`.
 
 ```
-heaptypeuse ::= '(' 'exact' ut:typeuse ')' => exact ut
-              | ut:typeuse                 => inexact ut
+exacttypeuse ::= '(' 'exact' ut:typeuse ')' => exact ut
+               | ut:typeuse                 => inexact ut
 ```
 
-Function imports, including all their sytax sugars,
-are updated to use `heaptypeuse` in place of `typeuse`.
+Function imports, including all their syntax sugars,
+are updated to use `exacttypeuse` in place of `typeuse`.
 For example:
 
 ```wasm
@@ -941,6 +941,26 @@ heaptype :: ... | 0x62 x:u32 => exact x
 Note that the type index being encoded as a `u32` instead of an `s33`
 intentionally makes it impossible to encode an exact abstract heap type.
 
+### Exact Function Imports
+
+The `externtype` encoding is updated
+with a new variant for exact function imports:
+
+```
+externtype = 0x00 x:typeidx => func x
+             ...
+             0x20 x:typeidx => func exact x
+```
+
+> The intention is that bit 6 is reserved to indicate exactness of other kinds
+> of `externtype`s in the future.
+
+Note that exports do not need to separately declare exactness.
+Exported functions are exact if and only if
+the internal type of the function is exact
+(i.e. the function is imported exactly or defined in the module).
+An export section using 0x20 is malfomed.
+
 ### Instructions
 
 All existing instructions that take heap type immediates work without
diff --git a/test/core/binary-leb128.wast b/test/core/binary-leb128.wast
diff --git a/test/core/binary.wast b/test/core/binary.wast
diff --git a/test/core/custom-descriptors/exact-func-import.wast b/test/core/custom-descriptors/exact-func-import.wast
