Skip to content

Commit 9c9af57

Browse files
ioannadioannad
committed
Current core formal spec for WebAssembly Exception Handling (WebAssembly#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: WebAssembly#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 WebAssembly#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.
1 parent 29e010d commit 9c9af57

28 files changed

+1252
-226
lines changed

‎README.md‎

Lines changed: 4 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -1,42 +1,15 @@
1-
[![Build Status](https://travis-ci.org/WebAssembly/spec.svg?branch=master)](https://travis-ci.org/WebAssembly/spec)
1+
[![Build Status](https://travis-ci.org/WebAssembly/exception-handling.svg?branch=master)](https://travis-ci.org/WebAssembly/exception-handling)
22

3-
# Exception handling
3+
# Exception Handling Proposal for WebAssembly
44

55
This repository
66
holds a
77
[proposal](https://github.com/WebAssembly/exception-handling/blob/master/proposals/Exceptions.md) for
88
adding exception handling to WebAssembly.
99

10-
The exception handling proposal depends on the [reference-types](https://github.com/WebAssembly/reference-types) proposal
11-
and on the [multi-value](https://github.com/WebAssembly/multi-value) proposal.
12-
13-
The repository is a clone
14-
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).
15-
16-
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).
17-
>>>>>>> Dependencies in proposal (#99)
18-
19-
# Reference Types Proposal for WebAssembly
20-
21-
This repository is a clone of [github.com/WebAssembly/spec/](https://github.com/WebAssembly/spec/).
22-
It is meant for discussion, prototype specification and implementation of a proposal to add support for basic reference types to WebAssembly.
23-
24-
* See the [overview](https://github.com/WebAssembly/reference-types/blob/master/proposals/reference-types/Overview.md) for a summary of the proposal.
25-
26-
* See the [modified spec](https://webassembly.github.io/reference-types/) for details.
27-
28-
# Multi-value Proposal for WebAssembly
29-
30-
[![Build Status](https://travis-ci.org/WebAssembly/multi-value.svg?branch=master)](https://travis-ci.org/WebAssembly/multi-value)
31-
32-
This repository is a clone of [github.com/WebAssembly/spec/](https://github.com/WebAssembly/spec/).
33-
It is meant for discussion, prototype specification and implementation of a proposal to add support for returning multiple values to WebAssembly.
34-
35-
* See the [overview](https://github.com/WebAssembly/multi-value/blob/master/proposals/multi-value/Overview.md) for a summary of the proposal.
36-
37-
* See the [modified spec](https://webassembly.github.io/multi-value/) for details.
10+
* See the [proposal overview](proposals/Exceptions.md) for a summary of the proposal.
3811

39-
The repository is now based on the [bulk operations proposal](proposals/bulk-memory-operations/Overview.md) and includes all respective changes.
12+
The repository is now based on the [reference types proposal](proposals/reference-types/Overview.md) and includes all respective changes.
4013

4114
Original README from upstream repository follows...
4215

‎document/core/appendix/algorithm.rst‎

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,13 +25,13 @@ Types are representable as an enumeration.
2525

2626
.. code-block:: pseudo
2727
28-
type val_type = I32 | I64 | F32 | F64 | Funcref | Externref
28+
type val_type = I32 | I64 | F32 | F64 | Funcref | Exnref | Externref
2929
3030
func is_num(t : val_type | Unknown) : bool =
3131
return t = I32 || t = I64 || t = F32 || t = F64 || t = Unknown
3232
3333
func is_ref(t : val_type | Unknown) : bool =
34-
return t = Funcref || t = Externref || t = Unknown
34+
return t = Funcref || t = Exnref || t = Externref || t = Unknown
3535
3636
The algorithm uses two separate stacks: the *value stack* and the *control stack*.
3737
The former tracks the :ref:`types <syntax-valtype>` of operand values on the :ref:`stack <stack>`,
@@ -209,6 +209,15 @@ Other instructions are checked in a similar manner.
209209
error_if(frame.opcode =/= if)
210210
push_ctrl(else, frame.start_types, frame.end_types)
211211
212+
case (try t1*->t2*)
213+
pop_vals([t1*])
214+
push_ctrl(try, [t1*], [t2*])
215+
216+
case (catch)
217+
let frame = pop_ctrl()
218+
error_if(frame.opcode =/= try)
219+
push_ctrl(catch, [exnref], frame.end_types)
220+
212221
case (br n)
213222
     error_if(ctrls.size() < n)
214223
      pop_vals(label_types(ctrls[n]))

‎document/core/appendix/embedding.rst‎

Lines changed: 23 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,7 @@ Store
7676

7777
.. math::
7878
\begin{array}{lclll}
79-
\F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\
79+
\F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon, ~\SEXNS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\
8080
\end{array}
8181
8282
@@ -539,6 +539,28 @@ Memories
539539
\end{array}
540540
541541
542+
.. index:: exception, exception address, store, exception instance, exception type, function type
543+
.. _embed-exn:
544+
545+
Exceptions
546+
~~~~~~~~~~
547+
548+
.. _embedd-exn-alloc:
549+
550+
:math:`\F{exn\_alloc}(\store, \exntype) : (\store, \exnaddr)`
551+
.............................................................
552+
553+
1. Pre-condition: :math:`exntype` is :ref:`valid <valid-exntype>`.
554+
555+
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`.
556+
557+
3. Return the new store paired with :math:`\exnaddr`.
558+
559+
.. math::
560+
\begin{array}{lclll}
561+
\F{exn\_alloc}(S, \X{et}) &=& (S', \X{a}) && (\iff \allocexn(S, \X{et}) = S', \X{a}) \\
562+
\end{array}
563+
542564
543565
.. index:: global, global address, store, global instance, global type, value
544566
.. _embed-global:

‎document/core/appendix/implementation.rst‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ An implementation may impose restrictions on the following dimensions of a modul
3636
* the number of :ref:`functions <syntax-func>` in a :ref:`module <syntax-module>`, including imports
3737
* the number of :ref:`tables <syntax-table>` in a :ref:`module <syntax-module>`, including imports
3838
* the number of :ref:`memories <syntax-mem>` in a :ref:`module <syntax-module>`, including imports
39+
* the number of :ref:`exceptions <syntax-exn>` in a :ref:`module <syntax-module>`, including imports
3940
* the number of :ref:`globals <syntax-global>` in a :ref:`module <syntax-module>`, including imports
4041
* the number of :ref:`element segments <syntax-elem>` in a :ref:`module <syntax-module>`
4142
* 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 <
123124
* the number of allocated :ref:`function instances <syntax-funcinst>`
124125
* the number of allocated :ref:`table instances <syntax-tableinst>`
125126
* the number of allocated :ref:`memory instances <syntax-meminst>`
127+
* the number of allocated :ref:`exception instances <syntax-exninst>`
126128
* the number of allocated :ref:`global instances <syntax-globalinst>`
127129
* the size of a :ref:`table instance <syntax-tableinst>`
128130
* the size of a :ref:`memory instance <syntax-meminst>`

‎document/core/appendix/index-instructions.rst‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,11 +15,11 @@ Instruction Binary Opcode Type
1515
:math:`\LOOP~\X{bt}` :math:`\hex{03}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation <valid-loop>` :ref:`execution <exec-loop>`
1616
:math:`\IF~\X{bt}` :math:`\hex{04}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation <valid-if>` :ref:`execution <exec-if>`
1717
:math:`\ELSE` :math:`\hex{05}`
18-
(reserved) :math:`\hex{06}`
19-
(reserved) :math:`\hex{07}`
20-
(reserved) :math:`\hex{08}`
21-
(reserved) :math:`\hex{09}`
22-
(reserved) :math:`\hex{0A}`
18+
:math:`\TRY~\X{bt}` :math:`\hex{06}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation <valid-try>` :ref:`execution <exec-try>`
19+
:math:`\CATCH` :math:`\hex{07}`
20+
:math:`\THROW~x` :math:`\hex{08}` :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]` :ref:`validation <valid-throw>` :ref:`execution <exec-throw>`
21+
:math:`\RETHROW` :math:`\hex{09}` :math:`[t_1^\ast~\EXNREF] \to [t_2^\ast]` :ref:`validation <valid-rethrow>` :ref:`execution <exec-rethrow>`
22+
:math:`\BRONEXN~l~x` :math:`\hex{0A}` :math:`[\EXNREF] \to [\EXNREF]` :ref:`validation <valid-br_on_exn>` :ref:`execution <exec-br_on_exn>`
2323
:math:`\END` :math:`\hex{0B}`
2424
:math:`\BR~l` :math:`\hex{0C}` :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]` :ref:`validation <valid-br>` :ref:`execution <exec-br>`
2525
: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‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Construct Judgement
1818
:ref:`Block type <valid-blocktype>` :math:`\vdashblocktype \blocktype \ok`
1919
:ref:`Table type <valid-tabletype>` :math:`\vdashtabletype \tabletype \ok`
2020
:ref:`Memory type <valid-memtype>` :math:`\vdashmemtype \memtype \ok`
21+
:ref:`Exception type <valid-exntype>` :math:`\vdashexntype \exntype \ok`
2122
:ref:`Global type <valid-globaltype>` :math:`\vdashglobaltype \globaltype \ok`
2223
:ref:`External type <valid-externtype>` :math:`\vdashexterntype \externtype \ok`
2324
:ref:`Instruction <valid-instr>` :math:`S;C \vdashinstr \instr : \stacktype`
@@ -26,6 +27,7 @@ Construct Judgement
2627
:ref:`Function <valid-func>` :math:`C \vdashfunc \func : \functype`
2728
:ref:`Table <valid-table>` :math:`C \vdashtable \table : \tabletype`
2829
:ref:`Memory <valid-mem>` :math:`C \vdashmem \mem : \memtype`
30+
:ref:`Exception <valid-exn>` :math:`C \vdashexn \exn : \exntype`
2931
:ref:`Global <valid-global>` :math:`C \vdashglobal \global : \globaltype`
3032
:ref:`Element segment <valid-elem>` :math:`C \vdashelem \elem : \reftype`
3133
:ref:`Element mode <valid-elemmode>` :math:`C \vdashelemmode \elemmode : \reftype`
@@ -54,6 +56,7 @@ Construct Judgement
5456
:ref:`Function instance <valid-funcinst>` :math:`S \vdashfuncinst \funcinst : \functype`
5557
:ref:`Table instance <valid-tableinst>` :math:`S \vdashtableinst \tableinst : \tabletype`
5658
:ref:`Memory instance <valid-meminst>` :math:`S \vdashmeminst \meminst : \memtype`
59+
:ref:`Exception instance <valid-exninst>` :math:`S \vdashexninst \exninst : \exntype`
5760
:ref:`Global instance <valid-globalinst>` :math:`S \vdashglobalinst \globalinst : \globaltype`
5861
:ref:`Element instance <valid-eleminst>` :math:`S \vdasheleminst \eleminst \ok`
5962
:ref:`Data instance <valid-datainst>` :math:`S \vdashdatainst \datainst \ok`
@@ -97,6 +100,7 @@ Construct Judgement
97100
:ref:`Function instance <extend-funcinst>` :math:`\vdashfuncinstextends \funcinst_1 \extendsto \funcinst_2`
98101
:ref:`Table instance <extend-tableinst>` :math:`\vdashtableinstextends \tableinst_1 \extendsto \tableinst_2`
99102
:ref:`Memory instance <extend-meminst>` :math:`\vdashmeminstextends \meminst_1 \extendsto \meminst_2`
103+
:ref:`Exception instance <extend-exninst>` :math:`\vdashexninstextends \exninst_1 \extendsto \exninst_2`
100104
:ref:`Global instance <extend-globalinst>` :math:`\vdashglobalinstextends \globalinst_1 \extendsto \globalinst_2`
101105
:ref:`Element instance <extend-eleminst>` :math:`\vdasheleminstextends \eleminst_1 \extendsto \eleminst_2`
102106
:ref:`Data instance <extend-datainst>` :math:`\vdashdatainstextends \datainst_1 \extendsto \datainst_2`

‎document/core/appendix/index-types.rst‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,11 +15,13 @@ Category Constructor
1515
(reserved) :math:`\hex{7B}` .. :math:`\hex{71}`
1616
:ref:`Reference type <syntax-reftype>` |FUNCREF| :math:`\hex{70}` (-16 as |Bs7|)
1717
:ref:`Reference type <syntax-reftype>` |EXTERNREF| :math:`\hex{6F}` (-17 as |Bs7|)
18-
(reserved) :math:`\hex{6E}` .. :math:`\hex{61}`
18+
:ref:`Reference type <syntax-reftype>` |EXNREF| :math:`\hex{68}` (-18 as |Bs7|)
19+
(reserved) :math:`\hex{6D}` .. :math:`\hex{61}`
1920
:ref:`Function type <syntax-functype>` :math:`[\valtype^\ast] \to [\valtype^\ast]` :math:`\hex{60}` (-32 as |Bs7|)
2021
(reserved) :math:`\hex{5F}` .. :math:`\hex{41}`
2122
:ref:`Result type <syntax-resulttype>` :math:`[\epsilon]` :math:`\hex{40}` (-64 as |Bs7|)
2223
:ref:`Table type <syntax-tabletype>` :math:`\limits~\reftype` (none)
2324
:ref:`Memory type <syntax-memtype>` :math:`\limits` (none)
25+
:ref:`Exception type <syntax-exntype>` :math:`\functype` (none)
2426
:ref:`Global type <syntax-globaltype>` :math:`\mut~\valtype` (none)
2527
======================================== =========================================== ===============================================================================

0 commit comments

Comments
 (0)