Current core formal spec for the WebAssembly Exception Handling Propo…

…sal.

This adds the [informal formal core spec](WebAssembly#87 (comment))
laid out by Andreas Rossberg, and the core spec outlined in the
[proposal overview](https://github.com/WebAssembly/exception-handling/blob/master/proposals/Exceptions.md).

I have aimed for this to be as complete as possible for the above
"informal formal spec" and proposal overview, meaning I added prose
for all the relevant parts in syntax, validation, execution, binary
format, text format, and the appendix, as well as an example for
throw contexts.

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
+   type val_type = I32 | I64 | F32 | F64 | Funcref | Externref | Exnref
 
    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
+     return t = Funcref || t = Externref || t = Exnref
 
 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>`,
@@ -210,6 +210,15 @@ Other instructions are checked in a similar manner.
          error_if(frame.opcode =/= if)
          push_ctrl(else, frame.start_types, frame.end_types)
 
+       case (try t1*->t2*)
+         pop_vals([t1*])
+	 push_ctrl(try, [t1*], [t2*])
+
+       case (catch)
+         let frame = pop_ctrl()
+	 error_if(frame.opcode =/= try)
+	 push_ctrl(catch, [exnref], frame.end_types)
+
        case (br n)
          error_if(ctrls.size() < n)
          pop_vals(label_types(ctrls[n]))

document/core/appendix/embedding.rst

@@ -76,7 +76,7 @@ Store
 
 .. math::
    \begin{array}{lclll}
-   \F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\
+   \F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon, ~\SEVENTS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\
    \end{array}
 
 
@@ -539,6 +539,28 @@ Memories
    \end{array}
 
 
+.. index: event, event address, store, event instance, event type, exception attribute, function type
+.. _embed-event:
+
+Events
+~~~~~~
+
+.. _embedd-event-alloc:
+
+:math:`\F{event\_alloc}(\store, \eventtype) : (\store, \eventaddr)`
+...................................................................
+
+1. Pre-condition: :math:`eventtype` is :ref:`valid <valid-eventtype>`.
+
+2. Let :math:`\eventaddr` be the result of :ref:`allocating an event <alloc-event>` in :math:`\store` with :ref:`event type <syntax-eventtype>` :math:`\eventtype`.
+
+3. Return the new store paired with :math:`\eventaddr`.
+
+.. math::
+   \begin{array}{lclll}
+   \F{event\_alloc}(S, \X{et}) &=& (S', \X{a}) && (\iff \allocevent(S, \X{et}) = S', \X{a}) \\
+   \end{array}
+
 
 .. index:: global, global address, store, global instance, global type, value
 .. _embed-global:

document/core/appendix/implementation.rst

@@ -36,6 +36,7 @@ An implementation may impose restrictions on the following dimensions of a modul
 * the number of :ref:`functions <syntax-func>` in a :ref:`module <syntax-module>`, including imports
 * the number of :ref:`tables <syntax-table>` in a :ref:`module <syntax-module>`, including imports
 * the number of :ref:`memories <syntax-mem>` in a :ref:`module <syntax-module>`, including imports
+* the number of :ref:`events <syntax-event>` in a :ref:`module <syntax-module>`, including imports
 * the number of :ref:`globals <syntax-global>` in a :ref:`module <syntax-module>`, including imports
 * the number of :ref:`element segments <syntax-elem>` in a :ref:`module <syntax-module>`
 * the number of :ref:`data segments <syntax-data>` in a :ref:`module <syntax-module>`
@@ -123,6 +124,7 @@ Restrictions on the following dimensions may be imposed during :ref:`execution <
 * the number of allocated :ref:`function instances <syntax-funcinst>`
 * the number of allocated :ref:`table instances <syntax-tableinst>`
 * the number of allocated :ref:`memory instances <syntax-meminst>`
+* the number of allocated :ref:`event instances <syntax-eventinst>`
 * the number of allocated :ref:`global instances <syntax-globalinst>`
 * the size of a :ref:`table instance <syntax-tableinst>`
 * the size of a :ref:`memory instance <syntax-meminst>`

document/core/appendix/index-instructions.rst

@@ -13,11 +13,11 @@ Instruction                                Binary Opcode              Type
 :math:`\LOOP~\X{bt}`                       :math:`\hex{03}`           :math:`[t_1^\ast] \to [t_2^\ast]`              :ref:`validation <valid-loop>`            :ref:`execution <exec-loop>`
 :math:`\IF~\X{bt}`                         :math:`\hex{04}`           :math:`[t_1^\ast] \to [t_2^\ast]`              :ref:`validation <valid-if>`              :ref:`execution <exec-if>`
 :math:`\ELSE`                              :math:`\hex{05}`
-(reserved)                                 :math:`\hex{06}`
-(reserved)                                 :math:`\hex{07}`
-(reserved)                                 :math:`\hex{08}`
-(reserved)                                 :math:`\hex{09}`
-(reserved)                                 :math:`\hex{0A}`
+:math:`\TRY~\X{bt}`                        :math:`\hex{06}`           :math:`[t_1^\ast] \to [t_2^\ast]`              :ref:`validation <valid-try>`             :ref:`execution <exec-try>`
+:math:`\CATCH`                             :math:`\hex{07}`
+:math:`\THROW~x`                           :math:`\hex{08}`           :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`       :ref:`validation <valid-throw>`           :ref:`execution <exec-throw>`
+:math:`\RETHROW`                           :math:`\hex{09}`           :math:`[t_1^\ast~\EXNREF] \to [t_2^\ast]`      :ref:`validation <valid-rethrow>`         :ref:`execution <exec-rethrow>`
+:math:`\BRONEXN~l~x`                       :math:`\hex{0A}`           :math:`[\EXNREF] \to [\EXNREF]`                :ref:`validation <valid-br_on_exn>`       :ref:`execution <exec-br_on_exn>`
 :math:`\END`                               :math:`\hex{0B}`
 :math:`\BR~l`                              :math:`\hex{0C}`           :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`       :ref:`validation <valid-br>`              :ref:`execution <exec-br>`
 :math:`\BRIF~l`                            :math:`\hex{0D}`           :math:`[t^\ast~\I32] \to [t^\ast]`             :ref:`validation <valid-br_if>`           :ref:`execution <exec-br_if>`

document/core/appendix/index-rules.rst

@@ -18,6 +18,7 @@ Construct                                        Judgement
 :ref:`Block type <valid-blocktype>`              :math:`\vdashblocktype \blocktype \ok`
 :ref:`Table type <valid-tabletype>`              :math:`\vdashtabletype \tabletype \ok`
 :ref:`Memory type <valid-memtype>`               :math:`\vdashmemtype \memtype \ok`
+:ref:`Event type <valid-eventtype>`              :math:`\vdasheventtype \eventtype \ok`
 :ref:`Global type <valid-globaltype>`            :math:`\vdashglobaltype \globaltype \ok`
 :ref:`External type <valid-externtype>`          :math:`\vdashexterntype \externtype \ok`
 :ref:`Instruction <valid-instr>`                 :math:`S;C \vdashinstr \instr : \functype`
@@ -26,6 +27,7 @@ Construct                                        Judgement
 :ref:`Function <valid-func>`                     :math:`C \vdashfunc \func : \functype`
 :ref:`Table <valid-table>`                       :math:`C \vdashtable \table : \tabletype`
 :ref:`Memory <valid-mem>`                        :math:`C \vdashmem \mem : \memtype`
+:ref:`Event <valid-event>`                       :math:`C \vdashevent \event : \eventtype`
 :ref:`Global <valid-global>`                     :math:`C \vdashglobal \global : \globaltype`
 :ref:`Element segment <valid-elem>`              :math:`C \vdashelem \elem : \reftype`
 :ref:`Element mode <valid-elemmode>`             :math:`C \vdashelemmode \elemmode : \reftype`
@@ -54,6 +56,7 @@ Construct                                        Judgement
 :ref:`Function instance <valid-funcinst>`        :math:`S \vdashfuncinst \funcinst : \functype`
 :ref:`Table instance <valid-tableinst>`          :math:`S \vdashtableinst \tableinst : \tabletype`
 :ref:`Memory instance <valid-meminst>`           :math:`S \vdashmeminst \meminst : \memtype`
+:ref:`Event instance <valid-eventinst>`          :math:`S \vdasheventinst \eventinst : \eventtype`
 :ref:`Global instance <valid-globalinst>`        :math:`S \vdashglobalinst \globalinst : \globaltype`
 :ref:`Element instance <valid-eleminst>`         :math:`S \vdasheleminst \eleminst \ok`
 :ref:`Data instance <valid-datainst>`            :math:`S \vdashdatainst \datainst \ok`
@@ -97,6 +100,7 @@ Construct                                        Judgement
 :ref:`Function instance <extend-funcinst>`       :math:`\vdashfuncinstextends \funcinst_1 \extendsto \funcinst_2`
 :ref:`Table instance <extend-tableinst>`         :math:`\vdashtableinstextends \tableinst_1 \extendsto \tableinst_2`
 :ref:`Memory instance <extend-meminst>`          :math:`\vdashmeminstextends \meminst_1 \extendsto \meminst_2`
+:ref:`Event instance <extend-eventinst>`          :math:`\vdasheventinstextends \eventinst_1 \extendsto \eventinst_2`
 :ref:`Global instance <extend-globalinst>`       :math:`\vdashglobalinstextends \globalinst_1 \extendsto \globalinst_2`
 :ref:`Element instance <extend-eleminst>`         :math:`\vdasheleminstextends \eleminst_1 \extendsto \eleminst_2`
 :ref:`Data instance <extend-datainst>`           :math:`\vdashdatainstextends \datainst_1 \extendsto \datainst_2`

document/core/appendix/index-types.rst

@@ -15,11 +15,13 @@ 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|)
-(reserved)                                                                             :math:`\hex{6E}` .. :math:`\hex{61}`
+:ref:`Reference type <syntax-reftype>`    |EXNREF|                                     :math:`\hex{6E}` (-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}`
 :ref:`Result type <syntax-resulttype>`    :math:`[\epsilon]`                             :math:`\hex{40}` (-64 as |Bs7|)
 :ref:`Table type <syntax-tabletype>`      :math:`\limits~\reftype`                     (none)
 :ref:`Memory type <syntax-memtype>`       :math:`\limits`                              (none)
+:ref:`Event type <syntax-eventtype>`      :math:`\EXCEPTION~\functype`                 (none)
 :ref:`Global type <syntax-globaltype>`    :math:`\mut~\valtype`                        (none)
 ========================================  ===========================================  ===============================================================================