Current core formal spec for WebAssembly Exception Handling (#121)

Included in this PR:

- Detailed core formal spec additions aiming to fully implement:
  + the "informal formal" core spec laid out by Andreas @rossberg here: #87 (comment) and
  + the core spec outlined in the [proposal overview](https://github.com/WebAssembly/exception-handling/blob/master/proposals/Exceptions.md), while removing the mention of "events" everywhere but in the binary format ,
  + prose for the above in: syntax, validation, execution, binary format, text format, and the appendix, as well as an example for throw contexts.
- Travis-ci build status icon to `README.md`. The contents of this PR get built and deployed on my fork's github page successfully, using [the howto instructions](https://github.com/WebAssembly/proposals/blob/master/howto.md#setting-up-travis-and-github-page).

Not included in this PR:

- Neither the new values representing unresolved throw contexts, nor the additional rules for the execution contexts, which we discussed in #87, are added here. I plan to add these separately.
- No JS API/Web API changes.

Side comments:

- In [document/core/text/types.rst](https://ioannad.github.io/exception-handling/core/text/types.html#text-refedtype): I'm not sure whether `refedtype ::= ... | event ⇒ exnref` should have `event` there or something else (perhaps `exception`?) However, since currently the only events are exceptions, this is probably not really an issue.
- The "informal formal spec" defines the administrative instruction which represents an exception package as `exnref`, i.e.,  the same name as the type. I called this administrative instruction `ref.exn` instead for two reasons;  to match the style of `ref.null` and `ref.extern`, and to avoid ambiguity in the discussions.
- I removed multi-value mentions from `README.md` because multi-value is now part of the main spec. For the same reason I didn't add "multi-value" to the list of included proposals at the top of the core spec landing page.

Author: ioannad

README.md

@@ -1,43 +1,17 @@
-[![Build Status](https://travis-ci.org/WebAssembly/spec.svg?branch=master)](https://travis-ci.org/WebAssembly/spec)
+[![Build Status](https://travis-ci.org/WebAssembly/exception-handling.svg?branch=master)](https://travis-ci.org/WebAssembly/exception-handling)
 
-# Exception handling
+# Exception Handling Proposal for WebAssembly
 
 This repository
 holds a
 [proposal](https://github.com/WebAssembly/exception-handling/blob/master/proposals/Exceptions.md) for
 adding exception handling to WebAssembly.
 
-The exception handling proposal depends on the [reference-types](https://github.com/WebAssembly/reference-types) proposal
-and on the [multi-value](https://github.com/WebAssembly/multi-value) proposal.
+* See the [proposal overview](proposals/Exceptions.md) for a summary of the proposal.
 
-The repository is a clone
-of [WebAssembly/spec](https://github.com/WebAssembly/spec), first rebased on the spec of its dependency [reference-types](https://github.com/WebAssembly/reference-types), and then merged with the other dependency [multi-value](https://github.com/WebAssembly/multi-value). 
+The repository is now based on the [reference types proposal](proposals/reference-types/Overview.md) and includes all respective changes.
 
-The remainder of the document has contents of the two README files of the dependencies: [reference-types/README.md](https://github.com/WebAssembly/reference-types/blob/master/README.md) and [multi-value/README.md](https://github.com/WebAssembly/multi-value/blob/master/README.md).
-
-# Reference Types Proposal for WebAssembly
-
-[![Build Status](https://travis-ci.org/WebAssembly/reference-types.svg?branch=master)](https://travis-ci.org/WebAssembly/reference-types)
-
-This repository is a clone of [github.com/WebAssembly/spec/](https://github.com/WebAssembly/spec/).
-It is meant for discussion, prototype specification and implementation of a proposal to add support for basic reference types to WebAssembly.
-
-* See the [overview](https://github.com/WebAssembly/reference-types/blob/master/proposals/reference-types/Overview.md) for a summary of the proposal.
-
-* See the [modified spec](https://webassembly.github.io/reference-types/) for details.
-
-# Multi-value Proposal for WebAssembly
-
-[![Build Status](https://travis-ci.org/WebAssembly/multi-value.svg?branch=master)](https://travis-ci.org/WebAssembly/multi-value)
-
-This repository is a clone of [github.com/WebAssembly/spec/](https://github.com/WebAssembly/spec/).
-It is meant for discussion, prototype specification and implementation of a proposal to add support for returning multiple values to WebAssembly.
-
-* See the [overview](https://github.com/WebAssembly/multi-value/blob/master/proposals/multi-value/Overview.md) for a summary of the proposal.
-
-* See the [modified spec](https://webassembly.github.io/multi-value/) for details.
-
-Original `README` from upstream repository follows...
+Original README from upstream repository follows...
 
 # spec
 

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 | 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
+     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>`,
@@ -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, ~\SEXNS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\
    \end{array}
 
 
@@ -539,6 +539,28 @@ Memories
    \end{array}
 
 
+.. index:: exception, exception address, store, exception instance, exception type, function type
+.. _embed-exn:
+
+Exceptions
+~~~~~~~~~~
+
+.. _embedd-exn-alloc:
+
+:math:`\F{exn\_alloc}(\store, \exntype) : (\store, \exnaddr)`
+.............................................................
+
+1. Pre-condition: :math:`exntype` is :ref:`valid <valid-exntype>`.
+
+2. Let :math:`\exnaddr` be the result of :ref:`allocating an exception <alloc-exn>` in :math:`\store` with :ref:`exception type <syntax-exntype>` :math:`\exntype`.
+
+3. Return the new store paired with :math:`\exnaddr`.
+
+.. math::
+   \begin{array}{lclll}
+   \F{exn\_alloc}(S, \X{et}) &=& (S', \X{a}) && (\iff \allocexn(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:`exceptions <syntax-exn>` 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:`exception instances <syntax-exninst>`
 * 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:`Exception type <valid-exntype>`            :math:`\vdashexntype \exntype \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:`Exception <valid-exn>`                     :math:`C \vdashexn \exn : \exntype`
 :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:`Exception instance <valid-exninst>`        :math:`S \vdashexninst \exninst : \exntype`
 :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:`Exception instance <extend-exninst>`       :math:`\vdashexninstextends \exninst_1 \extendsto \exninst_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{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}`
 :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:`Exception type <syntax-exntype>`    :math:`\functype`                            (none)
 :ref:`Global type <syntax-globaltype>`    :math:`\mut~\valtype`                        (none)
 ========================================  ===========================================  ===============================================================================