Formal overview: add uncaught exceptions #221
Conversation
Based on this previous discussion: https://github.com/WebAssembly/exception-handling/pull/143/files#r761207853 Also: - fixed throw contexts to include situations where `val* T instr*` in general.
| ## TODO Uncaught Exceptions | ||
| ## Uncaught Exceptions | ||
|
|
||
| To describe uncaught exceptions we add a new terminal value. |
There was a problem hiding this comment.
@rossberg suggested we should avoid 'we': #180 (comment)
There was a problem hiding this comment.
Thank you, it seems to have slipped my mind!
There was a problem hiding this comment.
Fixed in the latest commit. By the way I noticed other usages of "we" in the formal overview, will fix those, including some other nits in an upcoming PR.
| To describe uncaught exceptions we add a new terminal value. | ||
|
|
||
| ``` | ||
| result ::= ... | T[val* (throw tagaddr)] |
There was a problem hiding this comment.
What result are we talking about? Can we expand ... if that's not too long?
There was a problem hiding this comment.
This refers to these result values. I now expanded ... and added this link in the document as well.
|
|
||
| ``` | ||
| result ::= val* | trap | ||
| | T[val* (throw tagaddr)] |
There was a problem hiding this comment.
- What @rossberg suggested was
val* T[throw e] instr*... Is this different fromT[val* (throw tagaddr)]? - How are the cases, which a throw context contains not only a
throwandvals but other things... such aslabel,caught, orframeas listed in the throw context section, covered?
There was a problem hiding this comment.
What @rossberg suggested was
val* T[throw e] instr*... Is this different fromT[val* (throw tagaddr)]?
They were different when @rossberg suggested the former formulation, but in this PR I also changed throw contexts from T ::= val* '[_]' instr* | ... to T ::= '[_]' | val* T instr* | ..., so now these two things val* T[throw e] instr* and T[val* (throw tagaddr)] are really the same.
How are the cases, which a throw context contains not only a throw and vals but other things... such as label, caught, or frame as listed in the throw context section, covered?
So now throw contexts surrounded by values and instructions are also throw contexts. Meaning that val* T instr* is a throw context too.
Based on this previous discussion:
https://github.com/WebAssembly/exception-handling/pull/143/files#r761207853
Also:
val* T instr*in general.