Current core formal spec for WebAssembly Exception Handling

document/core/appendix/index-types.rst

@@ -15,7 +15,7 @@ Category                                  Constructor
 (reserved)                                                                             :math:`\hex{7B}` .. :math:`\hex{71}`
 :ref:`Reference type <syntax-reftype>`    |FUNCREF|                                    :math:`\hex{70}` (-16 as |Bs7|)
 :ref:`Reference type <syntax-reftype>`    |EXTERNREF|                                  :math:`\hex{6F}` (-17 as |Bs7|)
-:ref:`Reference type <syntax-reftype>`    |EXNREF|                                     :math:`\hex{6E}` (-18 as |Bs7|)
+:ref:`Reference type <syntax-reftype>`    |EXNREF|                                     :math:`\hex{68}` (-18 as |Bs7|)
 (reserved)                                                                             :math:`\hex{6D}` .. :math:`\hex{61}`
 :ref:`Function type <syntax-functype>`    :math:`[\valtype^\ast] \to [\valtype^\ast]`  :math:`\hex{60}` (-32 as |Bs7|)
 (reserved)                                                                             :math:`\hex{5F}` .. :math:`\hex{41}`

document/core/appendix/properties.rst

@@ -262,8 +262,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 .. index:: exception type, exception instance, exception tag, function type
 .. _valid-exninst:
 
-:ref:`Exception Instances <syntax-exninst>` :math:`\{ \EXNITYPE~\functype \}`
-.............................................................................
+:ref:`Exception Instances <syntax-exninst>` :math:`\{ \EITYPE~\functype \}`
+...........................................................................
 
 * The :ref:`exception type <syntax-exntype>` :math:`\functype` must be :ref:`valid <valid-exntype>`.
 
@@ -273,7 +273,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
    \frac{
      \vdashexntype \functype \ok
    }{
-     S \vdashexninst \{ \EXNITYPE~\functype \} : \functype
+     S \vdashexninst \{ \EITYPE~\functype \} : \functype
    }
 
 
@@ -315,7 +315,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
    \frac{
      (S \vdash \reff : t)^\ast
    }{
-     S \vdasheleminst \{ \EITYPE~t, \EIELEM~\reff^\ast \} \ok
+     S \vdasheleminst \{ \EIELEMTYPE~t, \EIELEM~\reff^\ast \} \ok
    }
 
 

document/core/binary/modules.rst

@@ -334,21 +334,21 @@ It decodes into a vector of :ref:`element segments <syntax-elem>` that represent
      \X{seg}^\ast{:}\Bsection_9(\Bvec(\Belem)) &\Rightarrow& \X{seg} \\
    \production{element segment} & \Belem &::=&
      \hex{00}~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx)
-       &\Rightarrow& \{ \ETYPE~\FUNCREF, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
+       &\Rightarrow& \{ \EELEMTYPE~\FUNCREF, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
      \hex{01}~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx)
-       &\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EPASSIVE \} \\ &&|&
+       &\Rightarrow& \{ \EELEMTYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EPASSIVE \} \\ &&|&
      \hex{02}~~x{:}\Btableidx~~e{:}\Bexpr~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx)
-       &\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|&
+       &\Rightarrow& \{ \EELEMTYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|&
      \hex{03}~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx)
-       &\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EDECLARATIVE \} \\ &&|&
+       &\Rightarrow& \{ \EELEMTYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EDECLARATIVE \} \\ &&|&
      \hex{04}~~e{:}\Bexpr~~\X{el}^\ast{:}\Bvec(\Bexpr)
-       &\Rightarrow& \{ \ETYPE~\FUNCREF, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
+       &\Rightarrow& \{ \EELEMTYPE~\FUNCREF, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
      \hex{05}~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr)
-       &\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EPASSIVE \} \\ &&|&
+       &\Rightarrow& \{ \EELEMTYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EPASSIVE \} \\ &&|&
      \hex{06}~~x{:}\Btableidx~~e{:}\Bexpr~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr)
-       &\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|&
+       &\Rightarrow& \{ \EELEMTYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|&
      \hex{07}~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr)
-       &\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EDECLARATIVE \} \\
+       &\Rightarrow& \{ \EELEMTYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EDECLARATIVE \} \\
    \production{element kind} & \Belemkind &::=&
      \hex{00} &\Rightarrow& \FUNCREF \\
    \end{array}
@@ -500,7 +500,7 @@ component of a :ref:`module <syntax-module>`.
    \production{exception section} & \Bexnsec &::=&
      \X{exception}^\ast{:}\Bsection_{13}(\Bvec(\Bexn)) &\Rightarrow& \X{exception}^\ast \\
    \production{exception} & \Bexn &::=&
-     \X{x}{:}\Btypeidx &\Rightarrow& \{ \EXNTYPE~\X{x} \} \\
+     \hex{00}~~\X{x}{:}\Btypeidx &\Rightarrow& \{ \ETYPE~\X{x} \} \\
    \end{array}
 
 

document/core/binary/types.rst

@@ -178,15 +178,16 @@ Global Types
 Exception Types
 ~~~~~~~~~~~~~~~
 
-:ref:`Exception types <syntax-exntype>` are encoded as function types with a preceding flag, reserving a bit for future extensions.
+:ref:`Exception types <syntax-exntype>` are encoded by their function type.
 
 .. math::
    \begin{array}{llclll}
    \production{exception type} & \Bexntype &::=&
-     ft{:}\Bfunctype &\Rightarrow& \hex{00}~ft \\
+     \hex{00}~~ft{:}\Bfunctype &\Rightarrow& ft \\
    \end{array}
 
-The |Bfunctype| of an exception must have void result.
+The |Bfunctype| of an exception must have empty result.
 
 .. note::
-   In future versions of WebAssembly the preceeding flag could take more values, generalising exceptions to events.
+   In future versions of WebAssembly,
+   the preceding zero byte may encode additional flags.

document/core/exec/instructions.rst

@@ -1632,7 +1632,9 @@ Control Instructions
 
 6. Let :math:`H` be the exception handler whose arity is :math:`m` and whose continuation is the beginning of :math:`\instr_2^\ast`.
 
-7. :ref:`Install <exec-install-handler>` the exception handler `H` for the block :math:`\val^n~\instr_1^\ast` with label :math:`L`.
+7. :ref:`Enter <exec-handler-enter>` the exception handler `H`.
+
+8. :ref:`Enter <exec-instr-seq-enter>` the block :math:`\val^n~\instr_1^\ast` with label :math:`L`.
 
 .. math::
    ~\\[-1ex]
@@ -1654,7 +1656,7 @@ Control Instructions
 
 3. Let :math:`a` be the :ref:`exception address <syntax-exnaddr>` :math:`F.\AMODULE.\MIEXNS[x]`.
 
-4. :ref:`Search <exec-search-handler>` for an exception handler for the :ref:`exception address <syntax-exnaddr>` :math:`a`.
+4. :ref:`Throw <exec-throwaddr>` an exception with :ref:`exception address <syntax-exnaddr>` :math:`a`.
 
 .. math::
    ~\\[-1ex]
@@ -1680,7 +1682,7 @@ Control Instructions
 
 5. Put the values :math:`\val^\ast` on the stack.
 
-6. :ref:`Search <exec-search-handler>`  for an exception handler for the :ref:`exception address <syntax-exnaddr>` :math:`a`.
+6. :ref:`Throw <exec-throwaddr>`  an exception with :ref:`exception address <syntax-exnaddr>` :math:`a`.
 
 .. math::
    ~\\[-1ex]
@@ -2002,49 +2004,43 @@ When the end of a block is reached without a jump or trap aborting it, then the
    pair: handling; exception
 
 .. _exec-catchn:
-.. _exec-exn-handling:
 
 Exception Handling
 ~~~~~~~~~~~~~~~~~~
 
-The following auxiliary rules define the semantics of handling thrown exceptions
-inside :ref:`throw contexts <syntax-ctxt-throw>`, such as installing, searching for,
-and exiting an :ref:`exception handler <syntax-handler>` :math:`\CATCHN_n`.
-
-.. _exec-install-handler:
+The following auxiliary rules define the semantics of entering and exiting exception handlers through :ref:`try <syntax-try>` instructions and handling thrown exceptions.
 
-Installing an exception handler :math:`H` for a block :math:`\instr^\ast` with label :math:`L`
-..............................................................................................
+.. _exec-handler-enter:
 
-1. Let :math:`H` be the exception handler :math:`\CATCHN_m{\instr'^\ast}`.
+Entering an exception handler :math:`H`
+.......................................
 
-2. Push :math:`H` on the stack.
-
-3. :ref:`Enter <exec-instr-seq-enter>` the block :math:`\instr^\ast` with label :math:`L`.
+1. Push :math:`H` onto the stack.
 
 .. note::
    No formal reduction rule is needed for installing an exception handler
    because it is an :ref:`administrative instruction <syntax-instr-admin>`
-   which exception throwing instructions will search for.
+   that the :ref:`try <syntax-try>` instruction reduced to directly.
 
+.. _exec-handler-exit:
 
-Exiting an exception handler with arity :math:`m` from a block with label :math:`L`
-...................................................................................
+Exiting an exception handler
+............................
 
-When the block is exited without a throw :ref:`triggering <exec-handle-exn>`
+When the end of a :ref:`try <syntax-try>` instruction is reached without a jump, exception or trap, then the following steps are performed.
 the exception handler, then the following steps are performed.
 
-1. Assert: due to validation, there are :math:`m` values on the top of the stack.
+1. Let :math:`m` be the number of values on the top of the stack.
 
 2. Pop the values :math:`\val^m` from the stack.
 
-3. Assert: due to :ref:`validation <valid-instr-seq>`, the exception handler :math:`H` is now on the top of the stack.
+3. Assert: due to :ref:`validation <valid-instr-seq>`, the handler :math:`H` is now on the top of the stack.
 
-4. Pop the exception handler from the stack.
+4. Pop the handler from the stack.
 
 5. Push :math:`\val^m` back to the stack.
 
-6. Jump to the position after the |END| of the originating |TRY| instruction associated with the label :math:`L`.
+6. Jump to the position after the |END| of the originating |TRY| instruction associated with the handler :math:`H`.
 
 .. math::
    ~\\[-1ex]
@@ -2053,41 +2049,40 @@ the exception handler, then the following steps are performed.
    \end{array}
 
 
-.. _exec-search-handler:
 .. _exec-throwaddr:
 
-Searching for an exception handler for the :ref:`exception address <syntax-exnaddr>` :math:`a`
-..............................................................................................
+Throwing an exception with :ref:`exception address <syntax-exnaddr>` :math:`a`
+..............................................................................
 
 When a throw or a rethrow occurs, labels and call frames are popped if necessary,
 until an exception handler is found on the top of the stack.
 
 1. Assert: due to validation, :math:`S.\SEXNS[a]` exists.
 
-2. Let :math:`[t^n] \to []` be the type of the exception instance :math:`S.\SEXNS[a]`.
+2. Let :math:`[t^n] \to [t'^m]` be the :ref:`exception type <syntax-exntype>` :math:`S.\SEXNS[a].\EITYPE`.
 
-3. Assert: due to validation, there are :math:`n` values on the top of the stack.
+3. Assert: due to :ref:`validation <valid-try>`, there are :math:`n` values on the top of the stack.
 
 4. Pop the :math:`n` values :math:`\val^n` from the stack.
 
 5. While the stack is not empty and the top of the stack is not an exception handler, do:
 
    a. Pop the top element from the stack.
 
-6. The stack is now either empty or there is an exception handler on the top.
+6. Assert: The stack is now either empty or there is an exception handler on the top.
 
-.. _exec-handle-exn:
 
 7. If there is an exception handler :math:`\CATCHN_m\{\instr^\ast\}` on the top of the stack, then:
 
-   a. Assert: the last element popped from the stack was the label :math:`L` whose continuation is the end of the originating |TRY| instruction.
+   a. Pop the exception handler from the stack.
 
-   b. Pop the exception handler from the stack.
+   b. Let :math:`L` be the label whose arity is :math:`m` and whose continuation is the end of the |TRY| instruction associated with the handler.
 
-   c. Put the label :math:`L` back on the stack.
+   c. Push the label :math:`L` on the stack.
 
-   d. Enter the block :math:`(\REFEXNADDR~a~\val^n) \instr^\ast` with label :math:`L`.
+   d. Enter the block :math:`\instr^\ast` with label :math:`L`.
 
+   e. Push the :ref:`exception reference <syntax-refexnaddr>` :math:`(\REFEXNADDR~a~\val^n)` to the stack.
 8. Else the stack is empty.
 
 9. *TODO: return TBA administrative instruction for the unresolved throw.*
@@ -2097,7 +2092,7 @@ until an exception handler is found on the top of the stack.
    \begin{array}{rcl}
    S;~F;~\CATCHN_m\{\instr^\ast\}~\XT[\val^n~(\THROWADDR~a)]~\END &\stepto&
       S;~F;~\LABEL_m\{\}~(\REFEXNADDR~a~\val^n)~{\instr}^\ast~\END \\
-   && \hspace{-12ex} (\iff S.\SEXNS[a]=\{\EXNTYPE~[t^n]\to[]\}) \\
+   && \hspace{-12ex} (\iff S.\SEXNS[a]=\{\ETYPE~[t^n]\to[]\}) \\
    %   S;\val^n~(\THROWADDR~a) & \stepto & TBA \\
    \end{array}
 

document/core/exec/modules.rst

@@ -76,14 +76,14 @@ The following auxiliary typing rules specify this typing relation relative to a
 
 * The store entry :math:`S.\SEXNS[a]` must exist.
 
-* Let :math:`\functype` be the function type :math:`S.\SEXNS[a].\EXNITYPE`.
+* Let :math:`\functype` be the function type :math:`S.\SEXNS[a].\EITYPE`.
 
 * Then :math:`\EVEXN~a` is valid with :ref:`external type <syntax-externtype>` :math:`\ETEXN~\functype`.
 
 .. math::
    \frac{
    }{
-     S \vdashexternval \EVEXN~a : \ETEXN~(S.\SEXNS[a].\EXNITYPE)
+     S \vdashexternval \EVEXN~a : \ETEXN~(S.\SEXNS[a].\EITYPE)
    }
 
 
@@ -326,9 +326,9 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei
 
 2. Let :math:`a` be the first free :ref:`exception address <syntax-exnaddr>` in :math:`S`.
 
-3. Let :math:`\functype` be the :ref:`function type <syntax-functype>` :math:`\module.\MTYPES[\exn.\EXNTYPE]`.
+3. Let :math:`\functype` be the :ref:`function type <syntax-functype>` :math:`\module.\MTYPES[\exn.\ETYPE]`.
 
-4. Let :math:`\exninst` be the :ref:`exception instance <syntax-exninst>` :math:`\{ \EXNITYPE~\functype \}`.
+4. Let :math:`\exninst` be the :ref:`exception instance <syntax-exninst>` :math:`\{ \EITYPE~\functype \}`.
 
 5. Append :math:`\exninst` to the |SEXNS| of :math:`S`.
 
@@ -339,7 +339,7 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei
    \allocexn(S, \exn, \module) &=& S', \exnaddr \\[1ex]
    \mbox{where:} \hfill \\
    \exnaddr &=& |S.\SEXNS| \\
-   \exninst &=& \{ \EXNITYPE~\functype \} \\
+   \exninst &=& \{ \EITYPE~\functype \} \\
    S' &=& S \compose \{\SEXNS~\exninst\} \\
    \end{array}
 
@@ -380,7 +380,7 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei
 
 2. Let :math:`a` be the first free :ref:`element address <syntax-elemaddr>` in :math:`S`.
 
-3. Let :math:`\eleminst` be the :ref:`element instance <syntax-eleminst>` :math:`\{ \EITYPE~t, \EIELEM~\reff^\ast \}`.
+3. Let :math:`\eleminst` be the :ref:`element instance <syntax-eleminst>` :math:`\{ \EIELEMTYPE~t, \EIELEM~\reff^\ast \}`.
 
 4. Append :math:`\eleminst` to the |SELEMS| of :math:`S`.
 
@@ -391,7 +391,7 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei
   \allocelem(S, \reftype, \reff^\ast) &=& S', \elemaddr \\[1ex]
   \mbox{where:} \hfill \\
   \elemaddr &=& |S.\SELEMS| \\
-  \eleminst &=& \{ \EITYPE~\reftype, \EIELEM~\reff^\ast \} \\
+  \eleminst &=& \{ \EIELEMTYPE~\reftype, \EIELEM~\reff^\ast \} \\
   S' &=& S \compose \{\SELEMS~\eleminst\} \\
   \end{array}
 
@@ -533,7 +533,7 @@ and list of :ref:`reference <syntax-ref>` vectors for the module's :ref:`element
 
 7. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEMS`, do:
 
-   a. Let :math:`\elemaddr_i` be the :ref:`element address <syntax-elemaddr>` resulting from :ref:`allocating <alloc-elem>` a :ref:`element instance <syntax-eleminst>` of :ref:`reference type <syntax-reftype>` :math:`\elem_i.\ETYPE` with contents :math:`(\reff^\ast)^\ast[i]`.
+   a. Let :math:`\elemaddr_i` be the :ref:`element address <syntax-elemaddr>` resulting from :ref:`allocating <alloc-elem>` a :ref:`element instance <syntax-eleminst>` of :ref:`reference type <syntax-reftype>` :math:`\elem_i.\EELEMTYPE` with contents :math:`(\reff^\ast)^\ast[i]`.
 
 8. For each :ref:`data segment <syntax-data>` :math:`\data_i` in :math:`\module.\MDATAS`, do:
 
@@ -616,7 +616,7 @@ where:
      \qquad\quad~ (\where \exn^\ast = \module.\MEXNS) \\
    S_5, \globaladdr^\ast &=& \allocglobal^\ast(S_4, (\global.\GTYPE)^\ast, \val^\ast)
      \qquad\quad~ (\where \global^\ast = \module.\MGLOBALS) \\
-   S_6, \elemaddr^\ast &=& \allocelem^\ast(S_5, (\elem.\ETYPE)^\ast, (\reff^\ast)^\ast) \\
+   S_6, \elemaddr^\ast &=& \allocelem^\ast(S_5, (\elem.\EELEMTYPE)^\ast, (\reff^\ast)^\ast) \\
      \qquad\quad~ (\where \elem^\ast = \module.\MELEMS) \\
    S', \dataaddr^\ast &=& \allocdata^\ast(S_6, (\data.\DINIT)^\ast)
      \qquad\qquad\qquad~ (\where \data^\ast = \module.\MDATAS) \\
@@ -813,10 +813,10 @@ where:
 
 .. math::
    \begin{array}{@{}l}
-   \F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EPASSIVE\}) \quad=\quad \epsilon \\
-   \F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EACTIVE \{\ETABLE~0, \EOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad
+   \F{runelem}_i(\{\EELEMTYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EPASSIVE\}) \quad=\quad \epsilon \\
+   \F{runelem}_i(\{\EELEMTYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EACTIVE \{\ETABLE~0, \EOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad
      \instr^\ast~(\I32.\CONST~0)~(\I32.\CONST~n)~(\TABLEINIT~i)~(\ELEMDROP~i) \\
-   \F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EDECLARATIVE\}) \quad=\\ \qquad
+   \F{runelem}_i(\{\EELEMTYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EDECLARATIVE\}) \quad=\\ \qquad
      (\ELEMDROP~i) \\[1ex]
    \F{rundata}_i(\{\DINIT~b^n, DMODE~\DPASSIVE\}) \quad=\quad \epsilon \\
    \F{rundata}_i(\{\DINIT~b^n, DMODE~\DACTIVE \{\DMEM~0, \DOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad