Skip to content

[spec] Add call_addr and throw_addr as admin instructions #2189

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
rossberg wants to merge 7 commits into
base: main
Choose a base branch
from
Open

[spec] Add call_addr and throw_addr as admin instructions #2189

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
a9e0f5e
[spec] Make call_addr and throw_addr into admin instructions
rossberg Jun 16, 2026
fd8bce0
Fix typing rules
rossberg Jun 17, 2026
17afb46
Fix throw_ref rule
rossberg Jun 17, 2026
130563f
Fix throw_addr to signal unhandled exception
f52985 Jun 29, 2026
e580051
Adjust spec doc
rossberg Jun 19, 2026
b3a31da
Merge branch 'main' into call_addr
rossberg Jul 15, 2026
dd1c61a
Tweak doc
rossberg Jul 15, 2026
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
10 changes: 9 additions & 1 deletion document/core/exec/runtime.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ Results
~~~~~~~

A *result* is the outcome of a computation.
It is either a sequence of :ref:`values <syntax-val>`, a thrown :ref:`exception <exec-throw_ref>`, or a :ref:`trap <syntax-trap>`.
It is either a sequence of :ref:`values <syntax-val>`, a thrown :ref:`exception <exec-throw_addr>`, or a :ref:`trap <syntax-trap>`.

$${syntax: result}

Expand Down Expand Up @@ -578,6 +578,9 @@ Conventions
.. index:: ! administrative instructions, function, function instance, function address, label, frame, instruction, trap, call, memory, memory instance, table, table instance, element, data, segment, tag, tag instance, tag address, exception, reftype, handler, caught, caught exception
pair:: abstract syntax; administrative instruction
.. _syntax-trap:
.. _syntax-throw_addr:
.. _syntax-call_addr:
.. _syntax-return_call_addr:
.. _syntax-instr-admin:

Administrative Instructions
Expand All @@ -595,6 +598,11 @@ A :ref:`reference <syntax-ref>` represents a :ref:`reference <syntax-ref>` value
The ${:LABEL}, ${:FRAME}, and ${:HANDLER} instructions model :ref:`labels <syntax-label>`, :ref:`frames <syntax-frame>`, and active :ref:`exception handlers <syntax-handler>`, respectively, :ref:`"on the stack" <exec-notation>`.
Moreover, the administrative syntax maintains the nesting structure of the original :ref:`structured control instruction <syntax-instr-control>` or :ref:`function body <syntax-func>` and their :ref:`instruction sequences <syntax-instrs>`.

The variants of the ${:CALL} and ${:RETURN_CALL} instructions with a :ref:`function address <syntax-funcaddr>` represent an imminent call to a specific target function.

Similarly, the variant of the ${:THROW} instruction with an :ref:`exception address <syntax-exnaddr>` represents an exception that is being thrown.
Such exceptions are propagated through nested instruction sequences until a matching handler is found.

The ${:TRAP} instruction represents the occurrence of a trap.
Traps are bubbled up through nested instruction sequences, ultimately reducing the entire program to a single ${:TRAP} instruction, signalling abrupt termination.

Expand Down
3 changes: 3 additions & 0 deletions document/core/util/macros.def
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1542,6 +1542,9 @@
.. |REFEXNADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}exn}}
.. |REFHOSTADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}host}}
.. |REFEXTERN| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}extern}}
.. |CALLADDR| mathdef:: \xref{exec/runtime}{syntax-call_addr}{\K{call}}
.. |RETURNCALLADDR| mathdef:: \xref{exec/runtime}{syntax-return_call_addr}{\K{return_call}}
.. |THROWADDR| mathdef:: \xref{exec/runtime}{syntax-throw_addr}{\K{throw}}
.. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}}


Expand Down
20 changes: 10 additions & 10 deletions specification/wasm-3.0/1.3-syntax.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -241,12 +241,12 @@ syntax instr/br hint(desc "branch instruction") = ...

syntax instr/call hint(desc "function instruction") = ...
| CALL funcidx
| CALL_REF typeuse
| CALL_INDIRECT tableidx typeuse
| CALL_REF typeidx
| CALL_INDIRECT tableidx typeidx
| RETURN
| RETURN_CALL funcidx
| RETURN_CALL_REF typeuse
| RETURN_CALL_INDIRECT tableidx typeuse
| RETURN_CALL_REF typeidx
| RETURN_CALL_INDIRECT tableidx typeidx
| ...

syntax instr/exn hint(desc "exception instructions") = ...
Expand Down Expand Up @@ -455,14 +455,14 @@ def $free_instr(BR_ON_CAST_FAIL labelidx reftype_1 reftype_2) =
$free_labelidx(labelidx) ++ $free_reftype(reftype_1) ++ $free_reftype(reftype_2)

def $free_instr(CALL funcidx) = $free_funcidx(funcidx)
def $free_instr(CALL_REF typeuse) = $free_typeuse(typeuse)
def $free_instr(CALL_INDIRECT tableidx typeuse) =
$free_tableidx(tableidx) ++ $free_typeuse(typeuse)
def $free_instr(CALL_REF typeidx) = $free_typeidx(typeidx)
def $free_instr(CALL_INDIRECT tableidx typeidx) =
$free_tableidx(tableidx) ++ $free_typeidx(typeidx)
def $free_instr(RETURN) = {}
def $free_instr(RETURN_CALL funcidx) = $free_funcidx(funcidx)
def $free_instr(RETURN_CALL_REF typeuse) = $free_typeuse(typeuse)
def $free_instr(RETURN_CALL_INDIRECT tableidx typeuse) =
$free_tableidx(tableidx) ++ $free_typeuse(typeuse)
def $free_instr(RETURN_CALL_REF typeidx) = $free_typeidx(typeidx)
def $free_instr(RETURN_CALL_INDIRECT tableidx typeidx) =
$free_tableidx(tableidx) ++ $free_typeidx(typeidx)

def $free_instr(THROW tagidx) = $free_tagidx(tagidx)
def $free_instr(THROW_REF) = {}
Expand Down
8 changes: 4 additions & 4 deletions specification/wasm-3.0/2.3-validation.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,11 +117,11 @@ rule Instr_ok/call:
-- Expand: C.FUNCS[x] ~~ FUNC t_1* -> t_2*

rule Instr_ok/call_ref:
C |- CALL_REF (_IDX x) : t_1* (REF NULL (_IDX x)) -> t_2*
C |- CALL_REF x : t_1* (REF NULL (_IDX x)) -> t_2*
-- Expand: C.TYPES[x] ~~ FUNC t_1* -> t_2*

rule Instr_ok/call_indirect:
C |- CALL_INDIRECT x (_IDX y) : t_1* at -> t_2*
C |- CALL_INDIRECT x y : t_1* at -> t_2*
-- if C.TABLES[x] = at lim rt
-- Reftype_sub: C |- rt <: (REF NULL FUNC)
-- Expand: C.TYPES[y] ~~ FUNC t_1* -> t_2*
Expand All @@ -141,15 +141,15 @@ rule Instr_ok/return_call:

;; TODO(3, rossberg): enable t_2* <: C.RETURN
rule Instr_ok/return_call_ref:
C |- RETURN_CALL_REF (_IDX x) : t_3* t_1* (REF NULL (_IDX x)) -> t_4*
C |- RETURN_CALL_REF x : t_3* t_1* (REF NULL (_IDX x)) -> t_4*
-- Expand: C.TYPES[x] ~~ FUNC t_1* -> t_2*
-- if C.RETURN = (t'_2*)
-- Resulttype_sub: C |- t_2* <: t'_2*
-- Instrtype_ok: C |- t_3* -> t_4* : OK

;; TODO(3, rossberg): enable t_2* <: C.RETURN
rule Instr_ok/return_call_indirect:
C |- RETURN_CALL_INDIRECT x (_IDX y) : t_3* t_1* at -> t_4*
C |- RETURN_CALL_INDIRECT x y : t_3* t_1* at -> t_4*
-- if C.TABLES[x] = at lim rt
-- Reftype_sub: C |- rt <: (REF NULL FUNC)
----
Expand Down
5 changes: 4 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 @@ -46,7 +46,7 @@ syntax val hint(desc "value") =
| num | vec | ref

syntax result hint(desc "result") =
| _VALS val* | `(REF.EXN_ADDR exnaddr) THROW_REF | TRAP
| _VALS val* | THROW_ADDR exnaddr | TRAP

var r : ref
var res : result
Expand Down Expand Up @@ -136,6 +136,9 @@ syntax instr/admin hint(desc "administrative instruction") =
| LABEL_ n `{instr*} instr* hint(show LABEL_%#% %%)
| FRAME_ n `{frame} instr* hint(show FRAME_%#% %%)
| HANDLER_ n `{catch*} instr* hint(show HANDLER_%#% %%)
| CALL_ADDR funcaddr
| RETURN_CALL_ADDR funcaddr
| THROW_ADDR exnaddr
| TRAP


Expand Down
76 changes: 43 additions & 33 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 @@ -167,14 +167,17 @@ rule Step_read/br_on_cast_fail-fail:
;; Function instructions

rule Step_read/call:
z; (CALL x) ~> (REF.FUNC_ADDR a) (CALL_REF $funcinst(z)[a].TYPE)
z; (CALL x) ~> (CALL_ADDR a)
-- if $moduleinst(z).FUNCS[x] = a

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

rule Step_read/call_ref-func:
z; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> (FRAME_ m `{f} (LABEL_ m `{eps} instr*))
z; (REF.FUNC_ADDR a) (CALL_REF x) ~> (CALL_ADDR a)

rule Step_read/call_addr:
z; val^n (CALL_ADDR a) ~> (FRAME_ m `{f} (LABEL_ m `{eps} instr*))
----
-- if $funcinst(z)[a] = fi
-- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m
Expand All @@ -183,30 +186,32 @@ rule Step_read/call_ref-func:


rule Step_read/return_call:
z; (RETURN_CALL x) ~> (REF.FUNC_ADDR a) (RETURN_CALL_REF $funcinst(z)[a].TYPE)
z; (RETURN_CALL x) ~> (RETURN_CALL_ADDR a)
-- if $moduleinst(z).FUNCS[x] = a

rule Step_read/return_call_ref-null:
z; (REF.NULL_ADDR) (RETURN_CALL_REF x) ~> TRAP

rule Step_read/return_call_ref-label:
z; (LABEL_ k `{instr'*} val* (RETURN_CALL_REF yy) instr*) ~> val* (RETURN_CALL_REF yy)
rule Step_read/return_call_ref-func:
z; (REF.FUNC_ADDR a) (RETURN_CALL_REF x) ~> (RETURN_CALL_ADDR a)

rule Step_read/return_call_ref-handler:
z; (HANDLER_ k `{catch*} val* (RETURN_CALL_REF yy) instr*) ~> val* (RETURN_CALL_REF yy)
rule Step_read/return_call_addr-label:
z; (LABEL_ k `{instr'*} val* (RETURN_CALL_ADDR a) instr*) ~> val* (RETURN_CALL_ADDR a)

rule Step_read/return_call_ref-frame-null:
z; (FRAME_ k `{f} val* (REF.NULL_ADDR) (RETURN_CALL_REF yy) instr*) ~> TRAP
rule Step_read/return_call_addr-handler:
z; (HANDLER_ k `{catch*} val* (RETURN_CALL_ADDR a) instr*) ~> val* (RETURN_CALL_ADDR a)

rule Step_read/return_call_ref-frame-addr:
z; (FRAME_ k `{f} val'* val^n (REF.FUNC_ADDR a) (RETURN_CALL_REF yy) instr*) ~> val^n (REF.FUNC_ADDR a) (CALL_REF yy)
rule Step_read/return_call_addr-frame:
z; (FRAME_ k `{f} val'* val^n (RETURN_CALL_ADDR a) instr*) ~> val^n (CALL_ADDR a)
----
-- Expand: $funcinst(z)[a].TYPE ~~ FUNC t_1^n -> t_2^m


rule Step_pure/call_indirect:
(CALL_INDIRECT x yy) ~> (TABLE.GET x) (REF.CAST (REF NULL yy)) (CALL_REF yy)
(CALL_INDIRECT x y) ~> (TABLE.GET x) (REF.CAST (REF NULL (_IDX y))) (CALL_REF y)

rule Step_pure/return_call_indirect:
(RETURN_CALL_INDIRECT x yy) ~> (TABLE.GET x) (REF.CAST (REF NULL yy)) (RETURN_CALL_REF yy)
(RETURN_CALL_INDIRECT x y) ~> (TABLE.GET x) (REF.CAST (REF NULL (_IDX y))) (RETURN_CALL_REF y)


rule Step_pure/frame-vals:
Expand All @@ -225,48 +230,53 @@ rule Step_pure/return-handler:
;; Exceptions

rule Step/throw:
z; val^n (THROW x) ~> $add_exninst(z, exn); (REF.EXN_ADDR a) THROW_REF
z; val^n (THROW x) ~> $add_exninst(z, exn); (THROW_ADDR a)
-- Expand: $as_deftype($tag(z, x).TYPE) ~~ FUNC t^n -> eps
-- if a = |$exninst(z)|
-- if exn = {TAG $tagaddr(z)[x], FIELDS val^n}

rule Step_read/throw_ref-null:
z; (REF.NULL_ADDR) THROW_REF ~> TRAP

rule Step_read/throw_ref-instrs:
z; val* (REF.EXN_ADDR a) THROW_REF instr* ~> (REF.EXN_ADDR a) THROW_REF
rule Step_read/throw_ref-addr:
z; val* (REF.EXN_ADDR a) THROW_REF instr* ~> (THROW_ADDR a)
----
-- if val* =/= eps \/ instr* =/= eps

rule Step_read/throw_addr-instrs:
z; val* (THROW_ADDR a) instr* ~> (THROW_ADDR a)
----
-- if val* =/= eps \/ instr* =/= eps

rule Step_read/throw_ref-label:
z; (LABEL_ n `{instr'*} (REF.EXN_ADDR a) THROW_REF) ~> (REF.EXN_ADDR a) THROW_REF
rule Step_read/throw_addr-label:
z; (LABEL_ n `{instr'*} (THROW_ADDR a)) ~> (THROW_ADDR a)

rule Step_read/throw_ref-frame:
z; (FRAME_ n `{f} (REF.EXN_ADDR a) THROW_REF) ~> (REF.EXN_ADDR a) THROW_REF
rule Step_read/throw_addr-frame:
z; (FRAME_ n `{f} (THROW_ADDR a)) ~> (THROW_ADDR a)

rule Step_read/throw_ref-handler-empty:
z; (HANDLER_ n `{eps} (REF.EXN_ADDR a) THROW_REF) ~> (REF.EXN_ADDR a) THROW_REF
rule Step_read/throw_addr-handler-empty:
z; (HANDLER_ n `{eps} (THROW_ADDR a)) ~> (THROW_ADDR a)

rule Step_read/throw_ref-handler-catch:
z; (HANDLER_ n `{(CATCH x l) catch'*} (REF.EXN_ADDR a) THROW_REF) ~> val* (BR l)
rule Step_read/throw_addr-handler-catch:
z; (HANDLER_ n `{(CATCH x l) catch'*} (THROW_ADDR a)) ~> val* (BR l)
----
-- if $exninst(z)[a].TAG = $tagaddr(z)[x]
-- if val* = $exninst(z)[a].FIELDS

rule Step_read/throw_ref-handler-catch_ref:
z; (HANDLER_ n `{(CATCH_REF x l) catch'*} (REF.EXN_ADDR a) THROW_REF) ~> val* (REF.EXN_ADDR a) (BR l)
rule Step_read/throw_addr-handler-catch_ref:
z; (HANDLER_ n `{(CATCH_REF x l) catch'*} (THROW_ADDR a)) ~> val* (REF.EXN_ADDR a) (BR l)
----
-- if $exninst(z)[a].TAG = $tagaddr(z)[x]
-- if val* = $exninst(z)[a].FIELDS

rule Step_read/throw_ref-handler-catch_all:
z; (HANDLER_ n `{(CATCH_ALL l) catch'*} (REF.EXN_ADDR a) THROW_REF) ~> (BR l)
rule Step_read/throw_addr-handler-catch_all:
z; (HANDLER_ n `{(CATCH_ALL l) catch'*} (THROW_ADDR a)) ~> (BR l)

rule Step_read/throw_ref-handler-catch_all_ref:
z; (HANDLER_ n `{(CATCH_ALL_REF l) catch'*} (REF.EXN_ADDR a) THROW_REF) ~> (REF.EXN_ADDR a) (BR l)
rule Step_read/throw_addr-handler-catch_all_ref:
z; (HANDLER_ n `{(CATCH_ALL_REF l) catch'*} (THROW_ADDR a)) ~> (REF.EXN_ADDR a) (BR l)

rule Step_read/throw_ref-handler-next:
z; (HANDLER_ n `{catch catch'*} (REF.EXN_ADDR a) THROW_REF) ~> (HANDLER_ n `{catch'*} (REF.EXN_ADDR a) THROW_REF)
rule Step_read/throw_addr-handler-next:
z; (HANDLER_ n `{catch catch'*} (THROW_ADDR a)) ~> (HANDLER_ n `{catch'*} (THROW_ADDR a))
----
-- otherwise

Expand Down
2 changes: 1 addition & 1 deletion specification/wasm-3.0/4.4-execution.modules.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -212,7 +212,7 @@ def $instantiate(s, module, externaddr*) = s''''; {MODULE moduleinst}; instr_E*
;; Invocation

def $invoke(store, funcaddr, val*) : config
def $invoke(s, funcaddr, val*) = s; {MODULE {}}; val* (REF.FUNC_ADDR funcaddr) (CALL_REF s.FUNCS[funcaddr].TYPE)
def $invoke(s, funcaddr, val*) = s; {MODULE {}}; val* (CALL_ADDR funcaddr)
----
-- Expand: s.FUNCS[funcaddr].TYPE ~~ FUNC t_1* -> t_2*
-- (Val_ok: s |- val : t_1)*
8 changes: 4 additions & 4 deletions specification/wasm-3.0/5.3-binary.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,11 +44,11 @@ grammar Binstr/control : instr = ...
| 0x0E l*:Blist(Blabelidx) l_n:Blabelidx => BR_TABLE l* l_n
| 0x0F => RETURN
| 0x10 x:Bfuncidx => CALL x
| 0x11 y:Btypeidx x:Btableidx => CALL_INDIRECT x (_IDX y)
| 0x11 y:Btypeidx x:Btableidx => CALL_INDIRECT x y
| 0x12 x:Bfuncidx => RETURN_CALL x
| 0x13 y:Btypeidx x:Btableidx => RETURN_CALL_INDIRECT x (_IDX y)
| 0x14 x:Btypeidx => CALL_REF (_IDX x)
| 0x15 x:Btypeidx => RETURN_CALL_REF (_IDX x)
| 0x13 y:Btypeidx x:Btableidx => RETURN_CALL_INDIRECT x y
| 0x14 x:Btypeidx => CALL_REF x
| 0x15 x:Btypeidx => RETURN_CALL_REF x
| 0x1F bt:Bblocktype c*:Blist(Bcatch) (in:Binstr)* 0x0B => TRY_TABLE bt c* in*
| 0xD5 l:Blabelidx => BR_ON_NULL l
| 0xD6 l:Blabelidx => BR_ON_NON_NULL l
Expand Down
8 changes: 4 additions & 4 deletions specification/wasm-3.0/6.3-text.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,13 +110,13 @@ grammar Tplaininstr_(I)/br : instr = ...

grammar Tplaininstr_(I)/func-plain : instr = ...
| "call" x:Tfuncidx_(I) => CALL x
| "call_ref" x:Ttypeidx_(I) => CALL_REF $($(_IDX x))
| "call_indirect" x:Ttableidx_(I) (y,I'):Ttypeuse_(I) => CALL_INDIRECT x $($(_IDX y))
| "call_ref" x:Ttypeidx_(I) => CALL_REF x
| "call_indirect" x:Ttableidx_(I) (y,I'):Ttypeuse_(I) => CALL_INDIRECT x y
-- if I' = {LOCALS (eps)*}
| "return" => RETURN
| "return_call" x:Tfuncidx_(I) => RETURN_CALL x
| "return_call_ref" x:Ttypeidx_(I) => RETURN_CALL_REF $($(_IDX x))
| "return_call_indirect" x:Ttableidx_(I) (y,I'):Ttypeuse_(I) => RETURN_CALL_INDIRECT x $($(_IDX y))
| "return_call_ref" x:Ttypeidx_(I) => RETURN_CALL_REF x
| "return_call_indirect" x:Ttableidx_(I) (y,I'):Ttypeuse_(I) => RETURN_CALL_INDIRECT x y
-- if I' = {LOCALS (eps)*}
| ...

Expand Down
33 changes: 19 additions & 14 deletions specification/wasm-3.0/7.1-soundness.configurations.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,20 +11,6 @@ rule Instr_ok2/plain:
s; C |- instr : t_1* ->_(x*) t_2*
-- Instr_ok: C |- instr : t_1* ->_(x*) t_2*

rule Instr_ok2/call_ref:
s; C |- CALL_REF yy : t_1* (REF NULL yy) -> t_2*
-- Typeuse_ok: C |- yy : OK
-- Expand_use: yy ~~_C FUNC t_1* -> t_2*

;; TODO(3, rossberg): enable t_2* <: C.RETURN
rule Instr_ok2/return_call_ref:
s; C |- RETURN_CALL_REF yy : t_3* t_1* (REF NULL yy) -> t_4*
-- Typeuse_ok: C |- yy : OK
-- Expand_use: yy ~~_C FUNC t_1* -> t_2*
-- if C.RETURN = (t'_2*)
-- Resulttype_sub: C |- t_2* <: t'_2*
-- Instrtype_ok: C |- t_3* -> t_4* : OK

rule Instr_ok2/ref:
s; C |- ref : eps -> rt
-- Ref_ok: s |- ref : rt
Expand All @@ -45,6 +31,25 @@ rule Instr_ok2/handler:
-- (Catch_ok: C |- catch : OK)*
-- Instrs_ok2: s; C |- instr* : eps ->_(x*) t*

rule Instr_ok2/call_addr:
s; C |- CALL_ADDR a : t_1* (REF NULL dt) -> t_2*

@raoxiaojia raoxiaojia Jun 17, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Hmm, I thought we would be able to drop the additional REF NULL dt here given that call_addr is now the dedicated invoke admin instruction (so it only resolves the lookup and invoke the function frame).

-- if s.FUNCS[a].TYPE = dt
-- Expand: dt ~~ FUNC t_1* -> t_2*

;; TODO(3, rossberg): enable t_2* <: C.RETURN
rule Instr_ok2/return_call_addr:
s; C |- RETURN_CALL_ADDR a : t_3* t_1* (REF NULL dt) -> t_4*

@raoxiaojia raoxiaojia Jun 17, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Same for the ref null dt here

-- if s.FUNCS[a].TYPE = dt
-- Expand: dt ~~ FUNC t_1* -> t_2*
-- if C.RETURN = (t'_2*)
-- Resulttype_sub: C |- t_2* <: t'_2*
-- Instrtype_ok: C |- t_3* -> t_4* : OK

rule Instr_ok2/throw_addr:
s; C |- THROW_ADDR a : t_1* t* -> t_2*

@raoxiaojia raoxiaojia Jun 17, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

t^* here looks to be droppable as well (same as the above 2)

-- Expand_use: s.TAGS[s.EXNS[a].TAG].TYPE ~~_C FUNC t* -> eps
-- Instrtype_ok: C |- t_1* -> t_2* : OK

rule Instr_ok2/trap:
s; C |- TRAP : t_1* -> t_2*
-- Instrtype_ok: C |- t_1* -> t_2* : OK
Expand Down
20 changes: 10 additions & 10 deletions specification/wasm-latest/1.3-syntax.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -241,12 +241,12 @@ syntax instr/br hint(desc "branch instruction") = ...

syntax instr/call hint(desc "function instruction") = ...
| CALL funcidx
| CALL_REF typeuse
| CALL_INDIRECT tableidx typeuse
| CALL_REF typeidx
| CALL_INDIRECT tableidx typeidx
| RETURN
| RETURN_CALL funcidx
| RETURN_CALL_REF typeuse
| RETURN_CALL_INDIRECT tableidx typeuse
| RETURN_CALL_REF typeidx
| RETURN_CALL_INDIRECT tableidx typeidx
| ...

syntax instr/exn hint(desc "exception instructions") = ...
Expand Down Expand Up @@ -455,14 +455,14 @@ def $free_instr(BR_ON_CAST_FAIL labelidx reftype_1 reftype_2) =
$free_labelidx(labelidx) ++ $free_reftype(reftype_1) ++ $free_reftype(reftype_2)

def $free_instr(CALL funcidx) = $free_funcidx(funcidx)
def $free_instr(CALL_REF typeuse) = $free_typeuse(typeuse)
def $free_instr(CALL_INDIRECT tableidx typeuse) =
$free_tableidx(tableidx) ++ $free_typeuse(typeuse)
def $free_instr(CALL_REF typeidx) = $free_typeidx(typeidx)
def $free_instr(CALL_INDIRECT tableidx typeidx) =
$free_tableidx(tableidx) ++ $free_typeidx(typeidx)
def $free_instr(RETURN) = {}
def $free_instr(RETURN_CALL funcidx) = $free_funcidx(funcidx)
def $free_instr(RETURN_CALL_REF typeuse) = $free_typeuse(typeuse)
def $free_instr(RETURN_CALL_INDIRECT tableidx typeuse) =
$free_tableidx(tableidx) ++ $free_typeuse(typeuse)
def $free_instr(RETURN_CALL_REF typeidx) = $free_typeidx(typeidx)
def $free_instr(RETURN_CALL_INDIRECT tableidx typeidx) =
$free_tableidx(tableidx) ++ $free_typeidx(typeidx)

def $free_instr(THROW tagidx) = $free_tagidx(tagidx)
def $free_instr(THROW_REF) = {}
Expand Down
Loading
Loading