Skip to content

Conversation

@tlively
Copy link
Member

@tlively tlively commented Oct 22, 2025

Function references to imported functions must normally be inexact to
preserve soundness in the case where the dynamic type of the imported
function is a subtype of the import type. However, this difference
between imported and declared functions harms modularity by making it
possible for an instruction sequence to become invalid when a function
it references is replaced with an import.

To fix the modularity problem, introduce exact function imports that can
be referenced exactly, just as defined functions can.

Describe the problem and solution in the overview, and also update the
interpreter to make references to normal imported functions inexact and
to support exact function imports.

Fixes #57.

Function references to imported functions must normally be inexact to
preserve soundness in the case where the dynamic type of the imported
function is a subtype of the import type. However, this difference
between imported and declared functions harms modularity by making it
possible for an instruction sequence to become invalid when a function
it references is replaced with an import.

To fix the modularity problem, introduce exact function imports that can
be referenced exactly, just as defined functions can.

Describe the problem and solution in the overview, and also update the
interpreter to make references to normal imported functions inexact and
to support exact function imports.

Fixes #57.
@tlively
Copy link
Member Author

tlively commented Oct 22, 2025

Landing now to be able to use the tests downstream, but will happily address any feedback in a follow-up.

@tlively tlively merged commit e4a35de into main Oct 22, 2025
1 check passed
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.

Comment on lines +417 to 418
UseHT (Exact, Def (Lib.List32.nth dts y.it))) m.it.funcs in
ExternFuncT (Lib.List32.nth dts x.it)
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)


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.

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

tlively added a commit that referenced this pull request Oct 31, 2025
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Unsoundness bug: ref.func of imported function

3 participants