Current core formal spec for WebAssembly Exception Handling

document/core/appendix/algorithm.rst

@@ -25,13 +25,13 @@ Types are representable as an enumeration.
 
 .. code-block:: pseudo
 
-   type val_type = I32 | I64 | F32 | F64 | Funcref | Externref | Exnref
+   type val_type = I32 | I64 | F32 | F64 | Funcref | Exnref | Externref
 
    func is_num(t : val_type) : bool =
      return t = I32 || t = I64 || t = F32 || t = F64
 
    func is_ref(t : val_type) : bool =
-     return t = Funcref || t = Externref || t = Exnref
+     return t = Funcref || t = Exnref || t = Externref
 
 The algorithm uses two separate stacks: the *value stack* and the *control stack*.
 The former tracks the :ref:`types <syntax-valtype>` of operand values on the :ref:`stack <stack>`,
@@ -212,12 +212,12 @@ Other instructions are checked in a similar manner.
 
        case (try t1*->t2*)
          pop_vals([t1*])
-	 push_ctrl(try, [t1*], [t2*])
+         push_ctrl(try, [t1*], [t2*])
 
        case (catch)
          let frame = pop_ctrl()
-	 error_if(frame.opcode =/= try)
-	 push_ctrl(catch, [exnref], frame.end_types)
+         error_if(frame.opcode =/= try)
+         push_ctrl(catch, [exnref], frame.end_types)
 
        case (br n)
          error_if(ctrls.size() < n)

document/core/appendix/properties.rst

@@ -262,8 +262,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 .. index:: event type, event instance, exception tag, function type
 .. _valid-eventinst:
 
-:ref:`Event Instances <syntax-eventinst>` :math:`\{ \EVIATTRIBUTE~\EXCEPTION, \EVITYPE~\functype \}`
-....................................................................................................
+:ref:`Event Instances <syntax-eventinst>` :math:`\{ \EVIATTR~\EXCEPTION, \EVITYPE~\functype \}`
+...............................................................................................
 
 * The :ref:`event type <syntax-eventtype>` :math:`\EXCEPTION~\functype` must be :ref:`valid <valid-eventtype>`.
 
@@ -273,7 +273,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
    \frac{
      \vdasheventtype \EXCEPTION~\functype \ok
    }{
-     S \vdasheventinst \{ \EVIATTRIBUTE~\EXCEPTION, \EVITYPE~\functype \} : \EXCEPTION~\functype
+     S \vdasheventinst \{ \EVIATTR~\EXCEPTION, \EVITYPE~\functype \} : \EXCEPTION~\functype
    }
 
 
@@ -388,12 +388,12 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 
 * Let :math:`\globaltype^\ast` be the concatenation of all :math:`\globaltype_i` in order.
 
-* Then the module instance is valid with :ref:`context <context>` :math:`\{\CTYPES~\functype^\ast, \CFUNCS~{\functype'}^\ast,` :math:`\CTABLES~\tabletype^\ast, \CMEMS~\memtype^\ast, \CEVENTS~\eventtype^\ast, \CGLOBALS~\globaltype^\ast\}`.
+* Then the module instance is valid with :ref:`context <context>` :math:`\{\CTYPES~\functype^\ast, \CFUNCS~{\functype'}^\ast, \CTABLES~\tabletype^\ast, \CMEMS~\memtype^\ast, \CEVENTS~\eventtype^\ast, \CGLOBALS~\globaltype^\ast\}`.
 
 .. math::
    ~\\[-1ex]
    \frac{
-     \begin{array}{rcl}
+     \begin{array}{@{}rcl@{}}
      (\vdashfunctype \functype \ok)^\ast & \quad &
      (S \vdashexternval \EVFUNC~\funcaddr : \ETFUNC~\functype')^\ast \\
      (S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\tabletype)^\ast   & \quad &
@@ -579,7 +579,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
 
 .. index:: event address, event type, function type, value type, exception attribute, exception tag
 
-:math:`\EXNREFADDR~\eventaddr~\val^\ast`
+:math:`\REFEXNADDR~\eventaddr~\val^\ast`
 ........................................
 
 * The :ref:`external event value <syntax-externval>` :math:`\EVEVENT~\eventaddr` must be :ref:`valid <valid-externval-event>` with :ref:`external event type <syntax-externtype>` :math:`\ETEVENT~\EXCEPTION~[t^\ast]\to[]`.
@@ -594,7 +594,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
      \qquad
      (S \vdashval \val : t)^\ast
    }{
-     S; C \vdashadmininstr \EXNREFADDR~\eventaddr~\val^\ast : [] \to [\EXNREF]
+     S; C \vdashadmininstr \REFEXNADDR~\eventaddr~\val^\ast : [] \to [\EXNREF]
    }
 
 
@@ -619,9 +619,9 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
 :math:`\CATCH_n\{ \instr_0^\ast \} \instr^\ast \END`
 ....................................................
 
-* The instruction sequence :math:`\instr_0^\ast` must be :ref:`valid <valid-instr-seq>` with type of the form :math:`[\EXNREF] \to [t^n]`.
+* The instruction sequence :math:`\instr_0^\ast` must be :ref:`valid <valid-instr-seq>` with a type of the form :math:`[\EXNREF] \to [t^n]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[\EXNREF]` prepended to the |CLABELS| vector.
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t^n]` prepended to the |CLABELS| vector.
 
 * Under context :math:`C'`,
   the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[] \to [t^n]`.
@@ -632,7 +632,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
    \frac{
      S; C \vdashinstrseq \instr_0^\ast : [\EXNREF] \to [t^n]
      \qquad
-     S; C,\CLABELS\,[\EXNREF] \vdashinstrseq \instr^\ast : [] \to [t^n]
+     S; C,\CLABELS\,[t^n] \vdashinstrseq \instr^\ast : [] \to [t^n]
    }{
      S; C \vdashadmininstr \CATCH_n\{\instr_0^\ast\}~\instr^\ast~\END : [] \to [t^n]
    }

document/core/binary/modules.rst

@@ -175,7 +175,7 @@ It decodes into a vector of :ref:`imports <syntax-import>` that represent the |M
      \hex{01}~~\X{tt}{:}\Btabletype &\Rightarrow& \IDTABLE~\X{tt} \\ &&|&
      \hex{02}~~\X{mt}{:}\Bmemtype &\Rightarrow& \IDMEM~\X{mt} \\ &&|&
      \hex{03}~~\X{gt}{:}\Bglobaltype &\Rightarrow& \IDGLOBAL~\X{gt} \\ &&|&
-     \hex{04}~~\X{ev}{:}\Bevent &\Rightarrow& \IDEVENT~\X{ev} \\
+     \hex{04}~~\X{evt}{:}\Bevent &\Rightarrow& \IDEVENT~\X{evt} \\
    \end{array}
 
 
@@ -482,7 +482,7 @@ It decodes into an optional :ref:`u32 <syntax-uint>` that represents the number
    instead of deferring validation.
 
 
-.. index:: ! event section, event, event type, attribute, function type index
+.. index:: ! event section, event, event type, event attribute, function type index
    pair: binary format; event
    pair: section; event
 .. _binary-event:
@@ -500,8 +500,8 @@ component of a :ref:`module <syntax-module>`.
    \production{event section} & \Beventsec &::=&
      \X{event}^\ast{:}\Bsection_{13}(\Bvec(\Bevent)) &\Rightarrow& \X{event}^\ast \\
    \production{event} & \Bevent &::=&
-     \X{a}{:}\Battribute~~\X{x}{:}\Btypeidx
-       &\Rightarrow& \{ \EVATTRIBUTE~\X{a}, \EVTYPE~\X{x} \} \\
+     \X{eventattr}{:}\Beventattr~~\X{x}{:}\Btypeidx
+       &\Rightarrow& \{ \EVATTR~\X{eventattr}, \EVTYPE~\X{x} \} \\
    \end{array}
 
 

document/core/binary/types.rst

@@ -42,8 +42,8 @@ Reference Types
    \begin{array}{llclll@{\qquad\qquad}l}
    \production{reference type} & \Breftype &::=&
      \hex{70} &\Rightarrow& \FUNCREF \\ &&|&
-     \hex{6F} &\Rightarrow& \EXTERNREF \\ &&|&
-     \hex{68} &\Rightarrow& \EXNREF \\
+     \hex{68} &\Rightarrow& \EXNREF \\ &&|&
+     \hex{6F} &\Rightarrow& \EXTERNREF \\
    \end{array}
 
 
@@ -173,24 +173,24 @@ Global Types
 
 .. index:: event type, exception attribute, function type
    pair: binary format; event type
-   pair: binary format; attribute
-.. _binary-attribute:
+   pair: binary format; event attribute
+.. _binary-eventattr:
 .. _binary-eventtype:
 
 Event Types
 ~~~~~~~~~~~
 
-:ref:`Event types <syntax-eventtype>` are encoded as function types with a preceding flag indicating their :ref:`attribute <syntax-attribute>`.
+:ref:`Event types <syntax-eventtype>` are encoded as function types with a preceding flag indicating their :ref:`attribute <syntax-eventattr>`.
 
 .. math::
    \begin{array}{llclll}
    \production{event type} & \Beventtype &::=&
-     a{:}\Battribute~~ft{:}\Bfunctype &\Rightarrow& a~ft \\
-   \production{attribute} & \Battribute &::=&
+     a{:}\Beventattr~~ft{:}\Bfunctype &\Rightarrow& a~ft \\
+   \production{eventattr} & \Beventattr &::=&
      \hex{00} &\Rightarrow& \EXCEPTION \\
    \end{array}
 
-|EXCEPTION| is the |attribute| of an exception, whose function type must have void result.
+|EXCEPTION| is the |eventattr| of an exception, whose function type must have void result.
 
 .. note::
    Currently events can only be exceptions.

document/core/exec/instructions.rst

@@ -1624,13 +1624,13 @@ Control Instructions
 
 2. Let :math:`[t_1^n] \to [t_2^m]` be the :ref:`function type <syntax-functype>` :math:`\expand_F(\blocktype)`.
 
-3. Assert: due to :ref:`validation <valid-if>`, there are at least :math:`n` values on the top of the stack.
+3. Assert: due to :ref:`validation <valid-try>`, there are at least :math:`n` values on the top of the stack.
 
 4. Pop the values :math:`\val^n` from the stack.
 
 5. Let :math:`L` be the label whose arity is :math:`m` and whose continuation is the end of the |TRY| instruction.
 
-4. Execute the administrative instruction :math:`\CATCHN_m` by :ref:`entering <exec-instr-seq-enter>` the block :math:`\instr_1^\ast` with label :math:`L`, and reducing the resulting :ref:`throw context <syntax-ctxt-throw>`.
+4. :ref:`Execute <exec-catchn>` the administrative instruction :math:`\CATCHN_m` by :ref:`entering <exec-instr-seq-enter>` the block :math:`\instr_1^\ast` with label :math:`L`.
 
 .. math::
    ~\\[-1ex]
@@ -1652,12 +1652,12 @@ Control Instructions
 
 3. Let :math:`a` be the :ref:`event address <syntax-eventaddr>` :math:`F.\AMODULE.\MIEVENTS[x]`.
 
-4. :ref:`Throw <syntax-throwaddr>` the :ref:`event address <syntax-eventaddr>` :math:`a`.
+4. :ref:`Throw <exec-throwaddr>` the :ref:`event address <syntax-eventaddr>` :math:`a`.
 
 .. math::
    ~\\[-1ex]
    \begin{array}{lclr@{\qquad}l}
-   \THROW~x &\stepto& \THROWADDR~a & (\iff F.\AMODULE.\MIEVENTS[x]=a) \\
+   \THROW~x &\stepto& \THROWADDR~a & (\iff F.\AMODULE.\MIEVENTS[x] = a) \\
    \end{array}
 
 
@@ -1674,17 +1674,17 @@ Control Instructions
 
    a. Trap.
 
-4. Else the :math:`\EXNREF` value is of the form :math:`(\EXNREFADDR~a~\val^\ast)`.
+4. Assert: :math:`\EXNREF` is of the form :math:`(\REFEXNADDR~a~\val^\ast)`.
 
 5. Put the values :math:`\val^\ast` on the stack.
 
-6. :ref:`Throw <syntax-throwaddr>` the :ref:`event address <syntax-eventaddr>` :math:`a`.
+6. :ref:`Throw <exec-throwaddr>` the :ref:`event address <syntax-eventaddr>` :math:`a`.
 
 .. math::
    ~\\[-1ex]
    \begin{array}{lclr@{\qquad}}
      (\REFNULL~\EXNREF)~\RETHROW &\stepto& \TRAP \\
-     (\EXNREFADDR~a~\val^\ast)~\RETHROW &\stepto& \val^\ast~(\THROWADDR~a) \\
+     (\REFEXNADDR~a~\val^\ast)~\RETHROW &\stepto& \val^\ast~(\THROWADDR~a) \\
    \end{array}
 
 
@@ -1701,7 +1701,7 @@ Control Instructions
 
    a. Trap.
 
-4. Else the :math:`\EXNREF` value is of the form :math:`(\EXNREFADDR~a~\val^\ast)`.
+4. Assert: :math:`\EXNREF` is of the form :math:`(\REFEXNADDR~a~\val^\ast)`.
 
 5. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
 
@@ -1715,14 +1715,14 @@ Control Instructions
 
 8. Else:
 
-   a. Put the value :math:`(\EXNREFADDR~a~\val^\ast)` back on the stack.
+   a. Put the value :math:`(\REFEXNADDR~a~\val^\ast)` back on the stack.
 
 .. math::
    ~\\[-1ex]
    \begin{array}{lclr@{\qquad}l}
      F; (\REFNULL~\EXNREF)~\BRONEXN~l~x &\stepto& F; \TRAP \\
-     F; (\EXNREFADDR~a~\val^\ast)~\BRONEXN~l~x &\stepto& F; \val^\ast~(\BR~l)     & (\iff F.\AMODULE.\MIEVENTS[x] = a) \\
-     F; (\EXNREFADDR~a~\val^\ast)~\BRONEXN~l~x &\stepto& F; (\EXNREFADDR~a~\val^\ast) & (\iff F.\AMODULE.\MIEVENTS[x] \neq a) \\
+     F; (\REFEXNADDR~a~\val^\ast)~\BRONEXN~l~x &\stepto& F; \val^\ast~(\BR~l)     & (\iff F.\AMODULE.\MIEVENTS[x] = a) \\
+     F; (\REFEXNADDR~a~\val^\ast)~\BRONEXN~l~x &\stepto& F; (\REFEXNADDR~a~\val^\ast) & (\iff F.\AMODULE.\MIEVENTS[x] \neq a) \\
    \end{array}
 
 
@@ -1996,6 +1996,28 @@ When the end of a block is reached without a jump or trap aborting it, then the
    Therefore, execution of a loop falls off the end, unless a backwards branch is performed explicitly.
 
 
+.. index:: exception handling, throw context
+   pair: handling; exception
+.. _exec-catchn:
+.. _exec-throwaddr:
+
+Exception Handling
+~~~~~~~~~~~~~~~~~~
+
+The following auxiliary rules define the semantics of handling thrown exceptions
+inside :ref:`throw contexts <syntax-ctxt-throw>`.
+
+*TODO: Add rules prose, which may involve having defined return values for unresolved throws.*
+
+.. math::
+   \begin{array}{rcl}
+   S;~F;~\CATCHN_m\{\instr^\ast\}~\val^m~\END &\stepto& S;~F;~\val^m \\
+   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.\SEVENTS[a]=\{\EVATTR~\EXCEPTION, \EVTYPE~[t^n]\to[]\}) \\
+   \end{array}
+
+
 .. index:: ! call, function, function instance, label, frame
 
 Function Calls

document/core/exec/modules.rst

@@ -78,12 +78,12 @@ The following auxiliary typing rules specify this typing relation relative to a
 
 * Let :math:`\functype` be the function type :math:`S.\SEVENTS[a].\EVITYPE`.
 
-* Then :math:`\EVEVENT~a` is valid with :ref:`external type <syntax-externtype>` :math:`\ETEVENT~S.\SEVENTS[a].\EVIATTRIBUTE~\functype`.
+* Then :math:`\EVEVENT~a` is valid with :ref:`external type <syntax-externtype>` :math:`\ETEVENT~S.\SEVENTS[a].\EVIATTR~\functype`.
 
 .. math::
    \frac{
    }{
-     S \vdashexternval \EVEVENT~a : \ETEVENT~(S.\SEVENTS[a].\EVIATTRIBUTE)~(S.\SEVENTS[a].\EVITYPE)
+     S \vdashexternval \EVEVENT~a : \ETEVENT~(S.\SEVENTS[a].\EVIATTR)~(S.\SEVENTS[a].\EVITYPE)
    }
 
 
@@ -169,7 +169,7 @@ The following auxiliary typing rules specify this typing relation relative to a
    }
 
 
-:ref:`Exception References <syntax-exnrefaddr>` :math:`\EXNREFADDR~a~\val^n`
+:ref:`Exception References <syntax-refexnaddr>` :math:`\REFEXNADDR~a~\val^n`
 ............................................................................
 
 * The external value :math:`\EVEVENT~a` must be valid with :ref:`event type <syntax-eventtype>` :math:`\EXCEPTION~[t^n]\to[]`.
@@ -184,7 +184,7 @@ The following auxiliary typing rules specify this typing relation relative to a
    \qquad
     (S \vdashval \val : t)^n
    }{
-     S \vdashval \EXNREFADDR~a~\val^n : \EXNREF
+     S \vdashval \REFEXNADDR~a~\val^n : \EXNREF
    }
 
 
@@ -328,7 +328,7 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei
 
 3. Let :math:`\functype` be the :ref:`function type <syntax-functype>` :math:`\module.\MTYPES[\event.\EVTYPE]`.
 
-4. Let :math:`\eventinst` be the :ref:`event instance <syntax-eventinst>` :math:`\{ \EVIATTRIBUTE~\event.\EVATTRIBUTE, \EVITYPE~\functype \}`. 
+4. Let :math:`\eventinst` be the :ref:`event instance <syntax-eventinst>` :math:`\{ \EVIATTR~\event.\EVATTR, \EVITYPE~\functype \}`.
 
 5. Append :math:`\eventinst` to the |SEVENTS| of :math:`S`.
 
@@ -339,7 +339,7 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei
    \allocevent(S, \event, \module) &=& S', \eventaddr \\[1ex]
    \mbox{where:} \hfill \\
    \eventaddr &=& |S.\SEVENTS| \\
-   \eventinst &=& \{ \EVIATTRIBUTE~\event.\EVATTRIBUTE, \EVITYPE~\functype \} \\
+   \eventinst &=& \{ \EVIATTR~\event.\EVATTR, \EVITYPE~\functype \} \\
    S' &=& S \compose \{\SEVENTS~\eventinst\} \\
    \end{array}