Skip to content

Exact function imports #72

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Oct 22, 2025
Merged

Exact function imports #72

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion interpreter/binary/decode.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -320,7 +320,7 @@ let tabletype s =

let externtype s =
match byte s with
| 0x00 -> ExternFuncT (typeuse idx s)
| 0x00 -> ExternFuncT (heaptype s)
| 0x01 -> ExternTableT (tabletype s)
| 0x02 -> ExternMemoryT (memorytype s)
| 0x03 -> ExternGlobalT (globaltype s)
Expand Down
2 changes: 1 addition & 1 deletion interpreter/binary/encode.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -207,7 +207,7 @@ struct
| TableT (at, lim, t) -> reftype t; limits at lim

let externtype = function
| ExternFuncT ut -> byte 0x00; typeuse u32 ut
| ExternFuncT ht -> byte 0x00; heaptype ht
| ExternTableT tt -> byte 0x01; tabletype tt
| ExternMemoryT mt -> byte 0x02; memorytype mt
| ExternGlobalT gt -> byte 0x03; globaltype gt
Expand Down
4 changes: 2 additions & 2 deletions interpreter/host/env.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,8 @@ let exit vs =

let lookup name et =
match Utf8.encode name, et with
| "abort", ExternFuncT ut ->
| "abort", ExternFuncT (UseHT (_exact, ut)) ->
ExternFunc (Func.alloc_host (deftype_of_typeuse ut) abort)
| "exit", ExternFuncT ut ->
| "exit", ExternFuncT (UseHT (_exact, ut)) ->
ExternFunc (Func.alloc_host (deftype_of_typeuse ut) exit)
| _ -> raise Not_found
2 changes: 1 addition & 1 deletion interpreter/runtime/instance.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 (Def (Func.type_of func))
| ExternFunc func -> ExternFuncT (UseHT (Exact, Def (Func.type_of func)))

let export inst name =
try Some (List.assoc name inst.exports) with Not_found -> None
8 changes: 4 additions & 4 deletions interpreter/script/js.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -422,7 +422,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 (Idx i),
ExternFuncT (UseHT (Inexact, (Idx i))),
List.concat (List.map value vs) @ [Call (subject_idx @@ at) @@ at]

let get t at =
Expand Down Expand Up @@ -604,9 +604,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 (Idx 1l)) @@ at;
ExternFuncT (UseHT (Inexact, (Idx 1l)))) @@ at;
Import (Utf8.decode "spectest", Utf8.decode "eq_ref",
ExternFuncT (Idx 2l)) @@ at;
ExternFuncT (UseHT (Inexact, (Idx 2l)))) @@ at;
]
in
let item =
Expand Down Expand Up @@ -770,7 +770,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 (Def dt) ->
| ExternFuncT (UseHT (_exact, (Def dt))) ->
let (_, out) as ft = functype_of_comptype (expand_deftype dt) in
if is_js_functype ft then
None
Expand Down
3 changes: 2 additions & 1 deletion interpreter/syntax/ast.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -413,7 +413,8 @@ let exporttype_of (m : module_) (ex : export) : exporttype =
ExternTableT (Lib.List32.nth tts x.it)
| FuncX x ->
let dts = funcs xts @ List.map (fun f ->
let Func (y, _, _) = f.it in Def (Lib.List32.nth dts y.it)) m.it.funcs in
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)
Comment on lines +417 to 418
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit:

Suggested change
UseHT (Exact, Def (Lib.List32.nth dts y.it))) m.it.funcs in
ExternFuncT (Lib.List32.nth dts x.it)
UseHT (Exact, Def (Lib.List32.nth dts y.it))) m.it.funcs
in ExternFuncT (Lib.List32.nth dts x.it)

in ExportT (name, subst_externtype (subst_of dts) xt)

Expand Down
2 changes: 1 addition & 1 deletion interpreter/syntax/free.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ let externtype = function
| ExternGlobalT gt -> globaltype gt
| ExternMemoryT mt -> memorytype mt
| ExternTableT tt -> tabletype tt
| ExternFuncT ut -> typeuse ut
| ExternFuncT ht -> heaptype ht

let blocktype = function
| VarBlockType x -> types (idx x)
Expand Down
8 changes: 5 additions & 3 deletions interpreter/syntax/types.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ type externtype =
| ExternGlobalT of globaltype
| ExternMemoryT of memorytype
| ExternTableT of tabletype
| ExternFuncT of typeuse
| ExternFuncT of heaptype

type exporttype = ExportT of name * externtype
type importtype = ImportT of name * name * externtype
Expand Down Expand Up @@ -125,6 +125,8 @@ 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
Expand Down Expand Up @@ -235,7 +237,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 ut -> ExternFuncT (subst_typeuse s ut)
| ExternFuncT ht -> ExternFuncT (subst_heaptype s ht)


let subst_exporttype s = function
Expand Down Expand Up @@ -446,7 +448,7 @@ 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 ut -> "func " ^ string_of_typeuse ut
| ExternFuncT ht -> "func " ^ string_of_heaptype ht


let string_of_exporttype = function
Expand Down
7 changes: 6 additions & 1 deletion interpreter/text/arrange.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,11 @@ 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 final = function
| NoFinal -> ""
| Final -> " final"
Expand Down Expand Up @@ -708,7 +713,7 @@ 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 ut -> incr fx; Node ("func $" ^ nat (!fx - 1), [typeuse ut])
| ExternFuncT ht -> incr fx; Node ("func $" ^ nat (!fx - 1), [heaptypeuse ht])

let import fx tx mx ex gx im =
let Import (module_name, item_name, xt) = im.it in
Expand Down
30 changes: 22 additions & 8 deletions interpreter/text/parser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -449,6 +449,10 @@ functype_result :
| LPAR RESULT valtype_list RPAR functype_result
{ fun c -> snd $3 c @ $5 c }

heapfunctype :
| LPAR EXACT functype RPAR { fun c -> Exact, $3 c }
| functype { fun c -> Inexact, $1 c }

comptype :
| LPAR STRUCT structtype RPAR { fun c x -> StructT ($3 c x) }
| LPAR ARRAY arraytype RPAR { fun c x -> ArrayT ($3 c) }
Expand Down Expand Up @@ -488,6 +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) }
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the binary format syntactically allows arbitrary heaptypes, then the text format must, too, to stay equi-expressive. In particular, we should have tests for the invalid cases.


/* Immediates */

Expand Down Expand Up @@ -991,16 +998,20 @@ 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 typeuse func_fields_import /* Sugar */
| inline_import heaptypeuse func_fields_import /* Sugar */
{ fun c x loc ->
let y = inline_functype_explicit c ($2 c) ($3 c) in
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
[],
[Import (fst $1, snd $1, ExternFuncT (Idx y.it)) @@ loc ], [] }
[Import (fst $1, snd $1, ExternFuncT (UseHT (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 (Idx y.it)) @@ loc ], [] }
[Import (fst $1, snd $1, ExternFuncT (UseHT (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 }
Expand Down Expand Up @@ -1242,9 +1253,9 @@ table_fields :
/* Imports & Exports */

externtype :
| LPAR FUNC bindidx_opt typeuse RPAR
| LPAR FUNC bindidx_opt heaptypeuse RPAR
{ fun c -> ignore ($3 c anon_func bind_func);
fun () -> ExternFuncT (Idx ($4 c).it) }
fun () -> ExternFuncT ($4 c) }
| LPAR TAG bindidx_opt typeuse RPAR
{ fun c -> ignore ($3 c anon_tag bind_tag);
fun () -> ExternTagT (TagT (Idx ($4 c).it)) }
Expand All @@ -1260,9 +1271,12 @@ externtype :
| LPAR TABLE bindidx_opt tabletype RPAR
{ fun c -> ignore ($3 c anon_table bind_table);
fun () -> ExternTableT ($4 c) }
| LPAR FUNC bindidx_opt functype RPAR /* Sugar */
| LPAR FUNC bindidx_opt heapfunctype RPAR /* Sugar */
{ fun c -> ignore ($3 c anon_func bind_func);
fun () -> ExternFuncT (Idx (inline_functype c ($4 c) $loc($4)).it) }
fun () ->
let exact, ft = $4 c in
let y = inline_functype c ft $loc($4) in
ExternFuncT (UseHT (exact, Idx y.it)) }

import :
| LPAR IMPORT name name externtype RPAR
Expand Down
2 changes: 1 addition & 1 deletion interpreter/valid/match.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -184,5 +184,5 @@ 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 (Def dt1), ExternFuncT (Def dt2) -> match_deftype c dt1 dt2
| ExternFuncT ht1, ExternFuncT ht2 -> match_heaptype c ht1 ht2
| _, _ -> false
29 changes: 18 additions & 11 deletions interpreter/valid/valid.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ type context =
globals : globaltype list;
memories : memorytype list;
tables : tabletype list;
funcs : deftype list;
funcs : heaptype list;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think this should be that general. If it's limited to (exact * deftype), the use sites become simpler, too.

datas : unit list;
elems : reftype list;
locals : localtype list;
Expand Down Expand Up @@ -235,8 +235,13 @@ let check_externtype (c : context) (xt : externtype) at =
check_memorytype c mt at
| ExternTableT tt ->
check_tabletype c tt at
| ExternFuncT ut ->
| ExternFuncT (UseHT (_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)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit: Remove extra empty line



let diff_reftype (nul1, ht1) (nul2, ht2) =
Expand Down Expand Up @@ -586,7 +591,8 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
c.results -->... [], []

| Call x ->
let (ts1, ts2) = functype_of_comptype (expand_deftype (func c x)) in
let dt = deftype_of_typeuse (typeuse_of_heaptype (func c x)) in
let (ts1, ts2) = functype_of_comptype (expand_deftype dt) in
ts1 --> ts2, []

| CallRef x ->
Expand All @@ -602,7 +608,8 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
(ts1 @ [NumT (numtype_of_addrtype at)]) --> ts2, []

| ReturnCall x ->
let (ts1, ts2) = functype_of_comptype (expand_deftype (func c x)) in
let dt = deftype_of_typeuse (typeuse_of_heaptype (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 " ^
string_of_resulttype c.results ^
Expand Down Expand Up @@ -777,10 +784,9 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
[] --> [RefT (Null, ht)], []

| RefFunc x ->
let dt = func c x in
let ht = func c x in
refer_func c x;
(* TODO: Exact function references *)
[] --> [RefT (NoNull, UseHT (Inexact, Def dt))], []
[] --> [RefT (NoNull, ht)], []

| RefIsNull ->
let (_nul, ht) = peek_ref 0 s e.at in
Expand Down Expand Up @@ -1098,7 +1104,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 @ [type_ c x]}
{c with funcs = c.funcs @ [UseHT (Exact, Def (type_ c x))]}

let check_func_body (c : context) (f : func) =
let Func (x, ls, es) = f.it in
Expand Down Expand Up @@ -1194,7 +1200,8 @@ let check_type (c : context) (t : type_) : context =

let check_start (c : context) (start : start) =
let Start x = start.it in
let ft = functype_of_comptype (expand_deftype (func c x)) in
let dt = deftype_of_typeuse (typeuse_of_heaptype (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"

Expand All @@ -1206,7 +1213,7 @@ 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 ut -> {c with funcs = c.funcs @ [deftype_of_typeuse ut]}
| ExternFuncT ht -> {c with funcs = c.funcs @ [ht]}

module NameSet = Set.Make(struct type t = Ast.name let compare = compare end)

Expand All @@ -1218,7 +1225,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 (Def (func c x))
| FuncX x -> ExternFuncT (func c x)
in ExportT (name, xt)

let check_list f xs (c : context) : context =
Expand Down
Loading