Current core formal spec for WebAssembly Exception Handling #121

ioannad · 2020-06-18T00:17:41Z

The rendered spec of this PR can be seen here: https://ioannad.github.io/exception-handling

Included in this PR:

Detailed core formal spec additions aiming to fully implement:
- the "informal formal" core spec laid out by Andreas @rossberg here: Any formal execution definition of exception handling? #87 (comment) and
- the core spec outlined in the proposal overview, 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.

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 Any formal execution definition of exception handling? #87, are added here. I plan to add these separately.
No JS-api/WebIDL changes.

Side comments:

In document/core/text/types.rst: 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.

This adds: - the informal formal core spec laid out by Andreas Rossberg: WebAssembly#87 (comment) 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. I also updated the README.md to: - remove mention to multi-value which is now part of the main spec, and - add a build status icon for the exception-handling modified spec.

rossberg

Great stuff! Looks pretty good.

Apart from my comments, I wonder at this point if it's really worth having all the extra verbosity of defining "events" as a possible generalisation of exceptions already. It creates a lot of extra hoops, and we don't know when we will have the generalisation. I think it would totally suffice if the spec removed any mention of events and just spoke of exceptions, merely leaving the extension point in the binary format (the attribute 0-byte) for now. That would make the spec considerably simpler and more uniform (there is just one concept). But that's best left for a follow-up.

document/core/appendix/algorithm.rst

document/core/appendix/properties.rst

document/core/valid/modules.rst

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

ioannad · 2020-06-22T19:09:25Z

Thank you for your careful and clarifying review @rossberg. I applied your suggestions and will address the rest of your comments in a separate commit.

- Fixed indentation in document/core/appendix/algorithm.rst - Changed `attribute` to `eventattr` everywhere (and plain "attribute" in the index to "event attribute" - Changed `exnrefaddr` to `refexnaddr` everywhere - Changed occurrences of `ev` to `evt` when it is used as a metavariable for events. Note that this makes the part on import descriptors in document/core/text/modules.rst look a bit strange, but this will all change when events are renamed to exceptions, anyway. - Changed order of `externref`-`exnref` to `exnref`-`externref` also in document/core/binary/types.rst and in the prose in document/core/syntax/types.rst - Added section for the reduction of `catch_n`, with a TODO item to add the rules in prose, probably when return values for unresolved throws is added. In this section I moved the reductions from the throw contexts in document/core/exec/runtime.rst - Added link to the above section in the last rules of `try-catch` and `throw` - Removed mention of throw contexts in the last rule of `try-catch` - Removed superfluous explanation after the administrative instructions for references are introduced in document/core/exec/runtime.rst - Changed `_exception tag_` to `*exception tag*` in document/core/exec/runtime.rst - Removed superfluous text in the throw context example of document/core/exec/runtime.rst - Changed `Teventtype` to `Ttypeuse` in the abbreviation rule for exceptions, in document/core/text/modules.rst - Removed event types from document/core/text/types.rst and document/core/util/macros.def

ioannad · 2020-06-24T18:27:40Z

@rossberg I addressed all your comments, except the text format of br_on_exn. If that text format is br_on_exn l (exception x), wouldn't it be confusing that x is a typeidx instead of an eventidx (soon to be exnidx)?

The built spec is also updated to reflect all the changes: https://ioannad.github.io/exception-handling/core/

rossberg

Thanks! Can you rename event{idx,addr,instance,...} to exn{idx,addr,instance,...} as well? As far as I am concerned, there currently is no compelling reason to use the word event at all, since all we provide is exceptions. The redundant naming may be unnecessarily confusing.

rossberg · 2020-06-25T15:22:19Z

document/core/exec/instructions.rst


 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`.


The prose tries to avoid referring to administrative instructions, so I would express this a bit differently. I would phrase it as pushing and popping a handler on/off the stack, similar to how the prose describes function frames. That is, describe handlers as a new form of stack element in the Stack section (runtime.rst), and in the new auxiliary section Exception Handling have subsections for "installing" and exiting a handler, analogous to the ones for invoking functions.

rossberg · 2020-06-25T15:27:26Z

document/core/syntax/modules.rst

   \end{array}

-The event's :ref:`attribute <syntax-attribute>` may only specify the attribute |EXCEPTION|, meaning that the event is an exception.
+The :ref:`event attribute <syntax-eventattr>` may only specify the attribute |EXCEPTION|, meaning that the event is an exception.


As long as it basically carries no information (there is only one possible value), I'd completely remove event attributes from the abstract syntax for the time being. For future extensibility it suffices to have the zero byte in the binary format.

Sure, no problem at all to completely remove "event" everywhere (except the binary format byte you mentioned). I just thought that in your first comment you suggested to do this in a different PR, that is the reason why I didn't do that yet.

The next commit will remove all occurrences of event.

Just to make sure I understand correctly, I should also rename "event section" to "exception section", so really leave no trace of "event" except in that binary format bit, correct?

Ah, okay, I wasn't sure what the plan was, since I think there were some changes already. Anyway, I think we're on the same page, so I'm fine either way.

Yes, I'd rename the event section as well (for now).

rossberg · 2020-06-25T15:38:14Z

document/core/text/instructions.rst

@@ -106,6 +115,9 @@ All other control instruction are represented verbatim.
   \production{plain instruction} & \Tplaininstr_I &::=&
     \text{unreachable} &\Rightarrow& \UNREACHABLE \\ &&|&
     \text{nop} &\Rightarrow& \NOP \\ &&|&
+     \text{throw}~~x{:}\Teventidx_I &\Rightarrow& \THROW~x \\ &&|&
+     \text{rethrow} &\Rightarrow& \RETHROW \\ &&|&
+     \text{br\_on\_exn}~~l{:}\Tlabelidx_I~~x{:}\Teventidx_I &\Rightarrow& \BRONEXN~l~x \\ &&|&


Yeah, I'm fine addressing this separately, since it requires a change to what's currently implemented.

The idea is that in all cases where an instruction has an index that is not of the "primary" sort of the construct, the text format makes the kind explicit. We do that e.g. for call_indirect (type $x), data (memory $x), elem (table $x), etc., and there will probably be more in the future.

if that text format is br_on_exn l (exception x), wouldn't it be confusing that x is a typeidx instead of an eventidx?

Not sure I follow, x is an eventidx/exnidx, isn't it?

In particular: - Removed events everywhere: + renamed event to exception in prose and in names of attributes, + renamed event to exn in all macros and variable names, + removed event `attr`s completely, leaving a single mention to events in `document/core/binary/types.rst`, under "exception types" + renamed macros `EVTYPE` to `EXNTYPE` and `EVITYPE` to `EXNITYPE` + changed exception metavariables called `ev` to `exn` - In `document/core/exec/runtime.rst`: + added exception handlers as stack items, and + adjusted the prose in the throw context example. - In `document/core/exec/instructions.rst`: + changed prose of `try`, `throw`, and `rethrow` to not refer directly to administrative instructions, + extended the exception handling section as suggested, and + changed text format for `br_on_exn` and `throw` to include `(exception ... )` around the exception index. - In `proposals/Exceptions.md`: + changed the text format of `br_on_exn` and `throw` as above, and + removed events from the abstract syntax and text format.

ioannad · 2020-07-09T14:25:00Z

Sorry for the delay, @rossberg. I think the commit I just pushed should implement your latest comments and suggestions. Moreover, I made some changes to proposal/Exceptions.md which you didn't request, but which I thought would make sense after the discussion here. In particular, I removed "events" from the abstract syntax and text format, and changed the text format of br_on_exn, and additionally of throw. The commit message is fully detailed.

As before, I rebuilt the spec of my fork to include these changes: https://ioannad.github.io/exception-handling/core/

rossberg

Sorry for the delay, vacation. ;)

This looks pretty good! I have added a number of suggestions, most prominently for factoring out entering a block from entering a handler, which should make things slightly simpler.

document/core/binary/types.rst

rossberg · 2020-07-16T07:31:15Z

document/core/exec/instructions.rst

 The following auxiliary rules define the semantics of handling thrown exceptions
-inside :ref:`throw contexts <syntax-ctxt-throw>`.
+inside :ref:`throw contexts <syntax-ctxt-throw>`, such as installing, searching for,
+and exiting an :ref:`exception handler <syntax-handler>` :math:`\CATCHN_n`.


Suggested change

The following auxiliary rules define the semantics of handling thrown exceptions

inside :ref:`throw contexts <syntax-ctxt-throw>`.

inside :ref:`throw contexts <syntax-ctxt-throw>`, such as installing, searching for,

and exiting an :ref:`exception handler <syntax-handler>` :math:`\CATCHN_n`.

The following auxiliary rules define the semantics of entering and exiting exception handlers through :ref:`try <syntax-try>` instructions and handling thrown exceptions.

It seems I missed this suggestion, I am incorporating it in the next commit.

document/core/exec/instructions.rst

document/core/exec/runtime.rst

document/core/exec/instructions.rst

I think these are all the suggestions except from EXNITYPE-->EITYPE, because the latter is already used for the type of an element instance. In the next commit I will - fix the prose after valid/types.rst:157, - make an assertion in valid/types.rst:962, - move the "Because ..." of exec/runtime.rst:332 to syntax/types.rst, and - rebuild the fork spec to make sure everything looks and works ok. Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

- adjusted prose in validation of exception types - renamed EITYPE to EIELEMTYPE, EXNITYPE to EITYPE, ETYPE to EELEMTYPE, and EXNTYPE to ETYPE - fixed prose and indentation of qquad in the validation of br_on_exn - renamed "void" result to "empty" result (in several places, for exntypes) - moved justification for the type of exception instances from exec/runtime.rst to syntax/types.rst - adjusted new section references (e.g. <exec-handler-throwaddr> to <exec-throwaddr>) - fixed prose in the beginning of the exception handling section (exec/instructions.rst) as suggested - adjusted tags and prose in the last step of throw and of rethrow to match the latest changes in the above mentioned section Moreover: - fixed exn definition in binary/modules.rst (missing 0x00) - fixed hex value of exnref in appendix/index-types.rst

ioannad · 2020-07-16T14:06:45Z

@rossberg I think all the comments should be now implemented, and as usual, the rebuilt spec is here.

rossberg

Great, thanks! Below a few things I overlooked before.

One further thing I just noted is that the section on typing administrative instructions in appendix/properties is missing the new cases.

document/core/binary/types.rst

rossberg · 2020-07-16T16:25:49Z

document/core/exec/instructions.rst


-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.


I just noted that a similar language tweak is probably necessary to the intro sentences to the sections on exiting a block and returning from a function (including exceptions in the enumerations of possibilities).

rossberg · 2020-07-16T16:27:04Z

document/core/exec/runtime.rst

@@ -321,16 +321,14 @@ Exception Instances
 ~~~~~~~~~~~~~~~~~~~

 An *exception instance* is the runtime representation of an :ref:`exception <syntax-exn>` definition.
-It records the :ref:`function type <syntax-functype>` of its :ref:`type <syntax-exntype>`.
+It records type :ref:`type <syntax-exntype>` of the exception.


Suggested change

It records type :ref:`type <syntax-exntype>` of the exception.

It records the type :ref:`type <syntax-exntype>` of the exception.

I'll change that to

It records the :ref:type <syntax-exntype> of the exception.

document/core/exec/runtime.rst

rossberg · 2020-07-16T16:32:12Z

document/core/syntax/types.rst

+Because :ref:`exceptions <syntax-exn>` have a :ref:`valid <valid-exn>` |exntype|,
+it is an invariant of the semantics that the function type :math:`\functype` has empty result type.
 The parameters of |functype| define the list of values associated with the exception.


Suggested change

Because :ref:`exceptions <syntax-exn>` have a :ref:`valid <valid-exn>` |exntype|,

it is an invariant of the semantics that the function type :math:`\functype` has empty result type.

The parameters of |functype| define the list of values associated with the exception.

The parameters of |functype| define the list of values associated with the exception.

Furthermore, it is an invariant of the semantics that every |functype| in a :ref:`valid <valid-exntype>` exception type has an empty result type.

.. note::

Future versions of WebAssembly may allow non-empty result types in exceptions.

For some reason I can't add this to the batch, I'll make the change in the next commit.

rossberg · 2020-07-16T16:35:50Z

document/core/exec/instructions.rst

@@ -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:


Nit: _exec-catch (overlooked this one).

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

- exec-catchn is now exec-catch - exec/instructions.rst: added ", exception," to prose of exiting an instruction block and returning from a function - exec/runtime.rst: fixed prose in introduction of exception instances, fixed mentions of try-catch blocks (now try blocks) - syntax/types.rst: applied suggestion to fix prose in exception types

ioannad · 2020-07-17T10:45:44Z

@rossberg: I applied your latest suggestions and implemented the rest of the comments, and rebuilt the fork github page

rossberg

Looks very good. Bu have you seen my comment regarding the missing typing rules for the new administrative instructions?

rossberg · 2020-07-20T09:31:32Z

document/core/exec/instructions.rst

@@ -2027,7 +2027,7 @@ Entering an exception handler :math:`H`
 Exiting an exception handler
 ............................

-When the end of a :ref:`try <syntax-try>` instruction is reached without a jump, exception or trap, then the following steps are performed.
+When the end of a :ref:`try <syntax-try>` instruction is reached without a jump, exception, or trap, then the following steps are performed.


I think in this particular place you do not want to include exceptions. ;)

Ooops, slip of the hand. Thanks for spotting it! 😊

@rossberg: on a second look, these are the instructions for exiting the try without an exception being thrown. If an exception is thrown then we are in the case "Throwing an exception ...", right?

document/core/exec/runtime.rst

ioannad · 2020-07-21T15:48:33Z

Looks very good. Bu have you seen my comment regarding the missing typing rules for the new administrative instructions?

Oh, sorry I missed implementing that comment. On it!

ioannad · 2020-07-22T10:55:03Z

@rossberg please ignore my last comment, I was confused by the way github sometimes shows the PR additions after some rounds of reviews and extra commits.
It seems I included the typing rules already in the first commit of this PR: https://github.com/ioannad/exception-handling/blob/06d5b3ff9ae58d56b66a1b6129850f2e457b3309/document/core/appendix/properties.rst#administrative-instructions
Or did I misunderstand your comment and there is something else missing?

ioannad · 2020-07-22T11:07:21Z

document/core/appendix/properties.rst

@@ -554,6 +577,67 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
   }


+.. index:: exception address, exception type, function type, value type, exception tag


@rossberg : are these the typing rules you are referring to?

Ah, yes, sorry! Strange, I could have sworn that I did not find them when I looked, but I was probably looking at some wrong diff somehow.

The same happened to me when I looked the first time. :)

rossberg

Thanks for the great work! I stumbled over a couple more minor things, but I approved anyway, so you don't need to wait for me looking again.

document/core/appendix/properties.rst

rossberg · 2020-07-22T11:53:05Z

document/core/appendix/properties.rst

@@ -554,6 +577,67 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
   }


+.. index:: exception address, exception type, function type, value type, exception tag


Ah, yes, sorry! Strange, I could have sworn that I did not find them when I looked, but I was probably looking at some wrong diff somehow.

document/core/exec/modules.rst

rossberg · 2020-07-22T12:09:19Z

document/core/exec/modules.rst

+
+.. math::
+   \begin{array}{rlll}
+   \allocexn(S, \exn, \module) &=& S', \exnaddr \\[1ex]


This signature doesn't match its use in embedding.rst, which passes merely an exntype -- which is necessary, because that's outside any module. So I think this function needs to use that, and allocmodule needs adjusting.

Still TODO: - remove exceptions from first sentence of "Exiting an exception handler" - in document/core/exec/modules.rst:336-339 fix signature of allocexn and allocmodule later in that file - Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

In particular: - Fixes exception allocation (now matches the signature given in document/core/appendix/embedding.rst, using an exntype) - Fixes module allocation to reflect the above change. Moreover: - fixes a wrong syntax for the indexing in document/core/appendix/embedding.rst - fixes leftover line from a previous commit, in document/core/exec/instructions.rst:2031, replacing that line with a clarification of what to do when an exception is thrown while inside a try block.

ioannad · 2020-07-23T13:27:06Z

Ok, so now all the comments should be implemented, except the first two lines of "Exiting an exception handler" which now reads (first line is the same, second is a clarification):

When the end of a :ref:try <syntax-try> instruction is reached without a jump, exception, or trap, then the following steps are performed.
If an exception is thrown before the end of the |TRY| instruction, then we are in the case of :ref:throwing <exec-throwaddr> an exception.

ioannad · 2020-07-23T13:28:14Z

Thank you so much for all your comments and suggestions @rossberg! 🙏

rossberg · 2020-07-23T15:32:03Z

When the end of a :ref:try <syntax-try> instruction is reached without a jump, exception, or trap, then the following steps are performed.
If an exception is thrown before the end of the |TRY| instruction, then we are in the case of :ref:throwing <exec-throwaddr> an exception.

Hm, that doesn't sound quite right. The ~~instruction sequence is~~ steps are not performed when an exception occurred instead.

rossberg · 2020-07-23T15:39:56Z

Ah, sorry, I was misparsing. Scratch the previous comment.

rossberg · 2020-07-23T15:44:01Z

document/core/exec/instructions.rst

+............................
+
+When the end of a :ref:`try <syntax-try>` instruction is reached without a jump, exception, or trap, then the following steps are performed.
+If an exception is thrown before the end of the |TRY| instruction, then we are in the case of :ref:`throwing <exec-throwaddr>` an exception.


Suggested change

If an exception is thrown before the end of the |TRY| instruction, then we are in the case of :ref:`throwing <exec-throwaddr>` an exception.

If an exception is thrown before the end of the |TRY| instruction, then the case of :ref:`throwing <exec-throwaddr>` an exception applies.

Or perhaps just remove the sentence -- it's kind of redundant, and we don't have such a note for trap either.

sentence removed! :)

aheejin · 2020-07-28T19:25:01Z

Sorry, but given that we might have to change the spec significantly, is merging this now a good idea?

Ms2ger · 2020-07-29T12:21:42Z

I think it's better to have the current proposal merged so we can iterate on it. If we end up fundamentally changing everything about the proposal, we could still revert this change; if not, we at least have something to build on.

@rossberg

…bly#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.

@rossberg

…bly#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.

Ms2ger requested a review from rossberg June 18, 2020 06:40

rossberg reviewed Jun 22, 2020

View reviewed changes

Apply suggestions from code review

231e0aa

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

rossberg reviewed Jun 25, 2020

View reviewed changes

rossberg reviewed Jul 16, 2020

View reviewed changes

document/core/exec/instructions.rst Outdated Show resolved Hide resolved

rossberg reviewed Jul 16, 2020

View reviewed changes

document/core/exec/instructions.rst Show resolved Hide resolved

ioannad and others added 2 commits July 16, 2020 12:46

rossberg reviewed Jul 16, 2020

View reviewed changes

ioannad and others added 2 commits July 17, 2020 11:27

Apply suggestions from code review

6d51a93

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

rossberg reviewed Jul 20, 2020

View reviewed changes

ioannad mentioned this pull request Jul 21, 2020

Two-phase unwinding and its implications #123

Closed

ioannad commented Jul 22, 2020

View reviewed changes

rossberg approved these changes Jul 22, 2020

View reviewed changes

ioannad and others added 2 commits July 23, 2020 13:54

Apply suggestions from code review

396777c

Still TODO: - remove exceptions from first sentence of "Exiting an exception handler" - in document/core/exec/modules.rst:336-339 fix signature of allocexn and allocmodule later in that file - Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

rossberg reviewed Jul 23, 2020

View reviewed changes

removed redundant explanation from exiting a handler

36f1c50

Ms2ger merged commit 1648e00 into WebAssembly:master Jul 28, 2020

ioannad mentioned this pull request Apr 7, 2021

Details of the JS API for exception handling #150

Closed


		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.

	It records type :ref:`type <syntax-exntype>` of the exception.
	It records the type :ref:`type <syntax-exntype>` of the exception.

		@@ -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:

		@@ -554,6 +577,67 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
		}


		.. index:: exception address, exception type, function type, value type, exception tag

	If an exception is thrown before the end of the \|TRY\| instruction, then we are in the case of :ref:`throwing <exec-throwaddr>` an exception.
	If an exception is thrown before the end of the \|TRY\| instruction, then the case of :ref:`throwing <exec-throwaddr>` an exception applies.

Current core formal spec for WebAssembly Exception Handling #121

Current core formal spec for WebAssembly Exception Handling #121

Conversation

ioannad commented Jun 18, 2020 • edited Loading

rossberg left a comment

Choose a reason for hiding this comment

ioannad commented Jun 22, 2020

ioannad commented Jun 24, 2020 • edited Loading

rossberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ioannad commented Jul 9, 2020 • edited Loading

rossberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ioannad commented Jul 16, 2020

rossberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ioannad commented Jul 17, 2020

rossberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ioannad commented Jul 21, 2020

ioannad commented Jul 22, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

rossberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ioannad commented Jul 23, 2020

ioannad commented Jul 23, 2020

rossberg commented Jul 23, 2020 • edited Loading

rossberg commented Jul 23, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

aheejin commented Jul 28, 2020 • edited Loading

Ms2ger commented Jul 29, 2020

ioannad commented Jun 18, 2020 •

edited

Loading

ioannad commented Jun 24, 2020 •

edited

Loading

ioannad commented Jul 9, 2020 •

edited

Loading

ioannad commented Jul 22, 2020 •

edited

Loading

rossberg commented Jul 23, 2020 •

edited

Loading

aheejin commented Jul 28, 2020 •

edited

Loading