[spec] Add call_addr and throw_addr as admin instructions

document/core/appendix/implementation.rst

@@ -110,7 +110,7 @@ For a module given in :ref:`text format <text>`, additional limitations may be i
 Validation
 ~~~~~~~~~~
 
-An implementation may defer :ref:`validation <valid>` of individual :ref:`functions <syntax-func>` until they are first :ref:`invoked <exec-invoke>`.
+An implementation may defer :ref:`validation <valid>` of individual :ref:`functions <syntax-func>` until they are first :ref:`called <exec-call_addr>`.
 
 If a function turns out to be invalid, then the invocation, and every consecutive call to the same function, results in a :ref:`trap <trap>`.
 

document/core/exec/instructions.rst

@@ -141,29 +141,9 @@ $${rule: {Step_read/call}}
 
 .. _exec-call_ref:
 
-:math:`\CALLREF~x`
-..................
+$${rule-prose: Step_read/call_ref}
 
-.. todo:: (*) Prose not spliced, for the prose merges the two cases of null and non-null references.
-
-1. Assert: due to :ref:`validation <valid-call_ref>`, a null or :ref:`function reference <syntax-ref>` is on the top of the stack.
-
-2. Pop the reference value :math:`r` from the stack.
-
-3. If :math:`r` is :math:`\REFNULL~\X{ht}`, then:
-
-    a. Trap.
-
-4. Assert: due to :ref:`validation <valid-call_ref>`, :math:`r` is a :ref:`function reference <syntax-ref>`.
-
-5. Let :math:`\REFFUNCADDR~a` be the reference :math:`r`.
-
-6. :ref:`Invoke <exec-invoke>` the function instance at address :math:`a`.
-
-$${rule: {Step_read/call_ref-null}}
-
-.. note::
-   The formal rule for calling a non-null function reference is described :ref:`below <exec-invoke>`.
+$${rule: {Step_read/call_ref-*}}
 
 
 .. _exec-call_indirect:
@@ -272,18 +252,19 @@ $${rule: Step_pure/label-vals}
 Exception Handling
 ~~~~~~~~~~~~~~~~~~
 
-The following auxiliary rules define the semantics of entering and exiting ${:TRY_TABLE} blocks.
+The following auxiliary rules define the semantics of entering and exiting ${:TRY_TABLE} blocks,
+and of throwing exceptions.
 
 .. _exec-handler-enter:
 
 Entering :math:`\instr^\ast` with label :math:`L` and exception handler :math:`H`
 .................................................................................
 
-1. Push :math:`H` to the stack.
+1. Push ${:H} to the stack.
 
-2. Push :math:`L` onto the stack.
+2. Push ${:L} onto the stack.
 
-3. Jump to the start of the instruction sequence :math:`\instr^\ast`.
+3. Jump to the start of the instruction sequence ${:instr*}.
 
 .. note::
    No formal reduction rule is needed for entering an exception :ref:`handler <syntax-handler>`
@@ -298,23 +279,33 @@ Exiting an exception handler
 
 When the end of a ${:TRY_TABLE} block is reached without a jump, :ref:`exception <exception>`, or :ref:`trap <trap>`, then the following steps are performed.
 
-1. Let :math:`m` be the number of values on the top of the stack.
+1. Let ${:m} be the number of values on the top of the stack.
 
-2. Pop the values :math:`\val^m` from the stack.
+2. Pop the values ${:val^m} from the stack.
 
 3. Assert: due to :ref:`validation <valid-instrs>`, a handler and a label are now on the top of the stack.
 
 4. Pop the label from the stack.
 
-5. Pop the handler :math:`H` from the stack.
+5. Pop the handler ${:H} from the stack.
 
-6. Push :math:`\val^m` back to the stack.
+6. Push ${:val^m} back to the stack.
 
-7. Jump to the position after the end of the administrative instruction associated with the handler :math:`H`.
+7. Jump to the position after the end of the administrative instruction associated with the handler ${:H}.
 
 $${rule: Step_pure/handler-vals}
 
 
+.. _exec-throw_addr:
+
+Throwing an exception
+.....................
+
+$${rule-prose: Step_read/throw_addr}
+
+$${rule: Step_read/throw_addr-*}
+
+
 .. index:: ! call, function, function instance, label, frame
 
 Function Calls
@@ -325,32 +316,11 @@ through one of the :ref:`call instructions <exec-instr-control>`
 and returning from it.
 
 
-.. _exec-invoke:
-
-Invocation of :ref:`function reference <syntax-ref.func>` :math:`(\REFFUNCADDR~a)`
-..................................................................................
-
-1. Assert: due to :ref:`validation <valid-call>`, :math:`S.\SFUNCS[a]` exists.
-
-2. Let :math:`f` be the :ref:`function instance <syntax-funcinst>`, :math:`S.\SFUNCS[a]`.
-
-3. Let :math:`\TFUNC~[t_1^n] \Tarrow [t_2^m]` be the :ref:`composite type <syntax-comptype>` :math:`\expanddt(\X{f}.\FITYPE)`.
-
-4. Let :math:`\FUNC~x~\local^\ast~\instr^\ast` be the :ref:`function <syntax-func>` :math:`f.\FICODE`.
-
-5. Assert: due to :ref:`validation <valid-call>`, :math:`n` values are on the top of the stack.
-
-6. Pop the values :math:`\val^n` from the stack.
-
-7. Let :math:`F` be the :ref:`frame <syntax-frame>` :math:`\{ \AMODULE~F.\FIMODULE, \ALOCALS~\val^n~(\default_t)^\ast \}`.
-
-8. Push the activation of :math:`f` with arity :math:`m` to the stack.
-
-9. Let :math:`L` be the :ref:`label <syntax-label>` whose arity is :math:`m` and whose continuation is the end of the function.
+.. _exec-call_addr:
 
-10. :ref:`Enter <exec-instrs-enter>` the instruction sequence :math:`\instr^\ast` with label :math:`L` and no values.
+$${rule-prose: Step_read/call_addr}
 
-$${rule: {Step_read/call_ref-func}}
+$${rule: {Step_read/call_addr}}
 
 .. note::
    For non-defaultable types, the respective local is left uninitialized by these rules.
@@ -363,19 +333,19 @@ Returning from a function
 
 When the end of a function is reached without a jump (including through |RETURN|), or an :ref:`exception <exception>` or :ref:`trap <trap>` aborting it, then the following steps are performed.
 
-1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
+1. Let ${:F} be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
 
-2. Let :math:`n` be the arity of the activation of :math:`F`.
+2. Let ${:n} be the arity of the activation of ${:F}.
 
-3. Assert: due to :ref:`validation <valid-instrs>`, there are :math:`n` values on the top of the stack.
+3. Assert: due to :ref:`validation <valid-instrs>`, there are ${:n} values on the top of the stack.
 
-4. Pop the results :math:`\val^n` from the stack.
+4. Pop the results ${:val^n} from the stack.
 
-5. Assert: due to :ref:`validation <valid-func>`, the frame :math:`F` is now on the top of the stack.
+5. Assert: due to :ref:`validation <valid-func>`, the frame ${:F} is now on the top of the stack.
 
 6. Pop the frame from the stack.
 
-7. Push :math:`\val^n` back to the stack.
+7. Push ${:val^n} back to the stack.
 
 8. Jump to the instruction after the original call.
 
@@ -1183,4 +1153,4 @@ $${rule: Eval_expr}
 
 .. note::
    Evaluation iterates this reduction rule until reaching a value.
-   Expressions constituting :ref:`function <syntax-func>` bodies are executed during function :ref:`invocation <exec-invoke>`.
+   Expressions constituting :ref:`function <syntax-func>` bodies are executed during function :ref:`calls <exec-call_addr>`.

document/core/exec/runtime.rst

@@ -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}
 
@@ -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
@@ -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.
 

document/core/util/macros.def

@@ -1543,6 +1543,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}}
 
 

specification/wasm-3.0/1.3-syntax.instructions.spectec

@@ -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") = ...
@@ -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) = {}

specification/wasm-3.0/2.3-validation.instructions.spectec

@@ -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*
@@ -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)
   ----

specification/wasm-3.0/4.0-execution.configurations.spectec

@@ -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
@@ -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