Skip to content

[spec] specify host functions in spectec #2210

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

Open
zilinc wants to merge 1 commit into
base: main
Choose a base branch
from
Open

[spec] specify host functions in spectec #2210

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
17 changes: 16 additions & 1 deletion specification/wasm-3.0/4.0-execution.configurations.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ var res : result

;; Instances

syntax hostfunc hint(desc "host function") hint(macro "%" "FI%") = `...
syntax hostfunc hint(desc "host function") hint(macro "%" "FI%") = _HOSTFUNC text
syntax funccode hint(show code) hint(macro "funccode") = func | hostfunc

syntax taginst hint(desc "tag instance") hint(macro "%" "HI%") =
Expand Down Expand Up @@ -329,3 +329,18 @@ def $growmem(meminst, n) = meminst'
-- if $(i' = |b*| / (64 * $Ki) + n)
-- (if i' <= j)?
-- if i' <= $(2^($size(at) - 16))


;; Host functions

syntax hostcallresult =
| RES store result hint(show %, %)
| BOT

def $hostcall(hostfunc, store, val*) : hostcallresult* hint(show %4 <- %1(%2, %3))
def $hostcall hint(builtin)

def $lift_result(result) : instr* hint(show %)
def $lift_result(_VALS val*) = val*
def $lift_result(`(REF.EXN_ADDR a) THROW_REF) = (REF.EXN_ADDR a) THROW_REF

@rossberg rossberg Jul 15, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Note that the representation of exception results changes in #2189.

def $lift_result(TRAP) = TRAP
23 changes: 19 additions & 4 deletions specification/wasm-3.0/4.3-execution.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -170,17 +170,32 @@ rule Step_read/call:
z; (CALL x) ~> (REF.FUNC_ADDR a) (CALL_REF $funcinst(z)[a].TYPE)
-- if $moduleinst(z).FUNCS[x] = a

rule Step_read/call_ref-null:
z; (REF.NULL_ADDR) (CALL_REF yy) ~> TRAP
rule Step/call_ref-null:
z; (REF.NULL_ADDR) (CALL_REF yy) ~> z; TRAP

rule Step_read/call_ref-func:
z; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> (FRAME_ m `{f} (LABEL_ m `{eps} instr*))
rule Step/call_ref-func:
z; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> z; (FRAME_ m `{f} (LABEL_ m `{eps} instr*))
----
-- if $funcinst(z)[a] = fi
-- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m
-- if fi.CODE = FUNC x (LOCAL t)* (instr*)
-- if f = {LOCALS val^n ($default_(t))*, MODULE fi.MODULE}

rule Step/call_ref-hostfunc-res:
s; f; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> s'; f; $lift_result(result)
----
-- if $funcinst((s; f))[a] = fi

@rossberg rossberg Jul 15, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Does it not work to use pattern matching here, like in the hand-written version?

@zilinc zilinc Jul 15, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

I think the reason was that there's a MODULE field in the record as well, so it has to appear in the pattern. But otherwise I don't see any problems. I can do it if it's preferred.

@rossberg rossberg Jul 15, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Ah, right. In that case leave it as is.

@zilinc zilinc Jul 15, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

I was wondering why I needed the parens around (s; f) in the $funcinst call. Maybe the reason is in the latex generation:

-\mbox{if}~ (s ; f){.}\mathsf{funcs}{}[a] = {\mathit{fi}} \\
+\mbox{if}~ s ; f{.}\mathsf{funcs}{}[a] = {\mathit{fi}} \\

@rossberg rossberg Jul 15, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Yes, exactly. Or more precisely, the show hint for $funcinst removes the call parens..

-- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m
-- if fi.CODE = _HOSTFUNC hf
-- if RES s' result <- $hostcall(_HOSTFUNC hf, s, val^n)

rule Step/call_ref-hostfunc-div:
s; f; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> s; f; (REF.FUNC_ADDR a) (CALL_REF yy)
----
-- if $funcinst((s; f))[a] = fi
-- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m
-- if fi.CODE = _HOSTFUNC hf
-- if BOT <- $hostcall(_HOSTFUNC hf, s, val^n)

rule Step_read/return_call:
z; (RETURN_CALL x) ~> (REF.FUNC_ADDR a) (RETURN_CALL_REF $funcinst(z)[a].TYPE)
Expand Down
17 changes: 16 additions & 1 deletion specification/wasm-latest/4.0-execution.configurations.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ var res : result

;; Instances

syntax hostfunc hint(desc "host function") hint(macro "%" "FI%") = `...
syntax hostfunc hint(desc "host function") hint(macro "%" "FI%") = _HOSTFUNC text
syntax funccode hint(show code) hint(macro "funccode") = func | hostfunc

syntax taginst hint(desc "tag instance") hint(macro "%" "HI%") =
Expand Down Expand Up @@ -329,3 +329,18 @@ def $growmem(meminst, n) = meminst'
-- if $(i' = |b*| / (64 * $Ki) + n)
-- (if i' <= j)?
-- if i' <= $(2^($size(at) - 16))


;; Host functions

syntax hostcallresult =
| RES store result hint(show %, %)
| BOT

def $hostcall(hostfunc, store, val*) : hostcallresult* hint(show %4 <- %1(%2, %3))
def $hostcall hint(builtin)

def $lift_result(result) : instr* hint(show %)
def $lift_result(_VALS val*) = val*
def $lift_result(`(REF.EXN_ADDR a) THROW_REF) = (REF.EXN_ADDR a) THROW_REF
def $lift_result(TRAP) = TRAP
23 changes: 19 additions & 4 deletions specification/wasm-latest/4.3-execution.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -170,17 +170,32 @@ rule Step_read/call:
z; (CALL x) ~> (REF.FUNC_ADDR a) (CALL_REF $funcinst(z)[a].TYPE)
-- if $moduleinst(z).FUNCS[x] = a

rule Step_read/call_ref-null:
z; (REF.NULL_ADDR) (CALL_REF yy) ~> TRAP
rule Step/call_ref-null:
z; (REF.NULL_ADDR) (CALL_REF yy) ~> z; TRAP

rule Step_read/call_ref-func:
z; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> (FRAME_ m `{f} (LABEL_ m `{eps} instr*))
rule Step/call_ref-func:
z; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> z; (FRAME_ m `{f} (LABEL_ m `{eps} instr*))
----
-- if $funcinst(z)[a] = fi
-- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m
-- if fi.CODE = FUNC x (LOCAL t)* (instr*)
-- if f = {LOCALS val^n ($default_(t))*, MODULE fi.MODULE}

rule Step/call_ref-hostfunc-res:
s; f; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> s'; f; $lift_result(result)
----
-- if $funcinst((s; f))[a] = fi
-- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m
-- if fi.CODE = _HOSTFUNC hf
-- if RES s' result <- $hostcall(_HOSTFUNC hf, s, val^n)

rule Step/call_ref-hostfunc-div:
s; f; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> s; f; (REF.FUNC_ADDR a) (CALL_REF yy)
----
-- if $funcinst((s; f))[a] = fi
-- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m
-- if fi.CODE = _HOSTFUNC hf
-- if BOT <- $hostcall(_HOSTFUNC hf, s, val^n)

rule Step_read/return_call:
z; (RETURN_CALL x) ~> (REF.FUNC_ADDR a) (RETURN_CALL_REF $funcinst(z)[a].TYPE)
Expand Down
Loading
Loading