From 9e863cef939257d055dd3774de27f286d4b3b9c5 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Tue, 6 Sep 2022 18:07:57 +0200 Subject: [PATCH 1/2] Formal overview: add uncaught exceptions 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. --- .../Exceptions-formal-overview.md | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 027a4720..345bf8ad 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -139,9 +139,10 @@ Throw contexts don't skip over handlers (administrative `catch` or `delegate` in Throw contexts are used to match a thrown exception with the innermost handler. ``` -T ::= val* '[_]' instr* | 'label'_n{instr*} T 'end' - | 'caught'{ tagaddr val^n } T 'end' - | 'frame'_n{F} T end +T ::= '[_]' | val* T instr* + | 'label'_n{instr*} T 'end' + | 'caught'{ tagaddr val* } T 'end' + | 'frame'_n{F} T 'end' ``` Note that because `catch` and `delegate` instructions are not included above, there is always a unique maximal throw context to match the reduction rules. Note that this basically means that `caught{..} instr* end` is not a potential catching block for exceptions thrown by `instr*`. The instruction sequence `instr*` is inside a `catch` or `catch_all` block. @@ -222,6 +223,11 @@ S;C, labels (catch [t*]) ⊢ instr* : []→[t*] S;C, labels [t*] ⊢ caught{a val^n} instr* end : []→[t*] ``` -## TODO Uncaught Exceptions +## Uncaught Exceptions + +To describe uncaught exceptions we add a new terminal value. + +``` +result ::= ... | T[val* (throw tagaddr)] +``` -We haven't yet described the formalism for an uncaught exception being the result of evaluation. From 3ac9af9b82933a0f1f42272c2c139d27140a5775 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 9 Sep 2022 16:41:05 +0200 Subject: [PATCH 2/2] Addressed review comments. --- proposals/exception-handling/Exceptions-formal-overview.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/proposals/exception-handling/Exceptions-formal-overview.md b/proposals/exception-handling/Exceptions-formal-overview.md index 345bf8ad..9d314bcd 100644 --- a/proposals/exception-handling/Exceptions-formal-overview.md +++ b/proposals/exception-handling/Exceptions-formal-overview.md @@ -225,9 +225,10 @@ S;C, labels [t*] ⊢ caught{a val^n} instr* end : []→[t*] ## Uncaught Exceptions -To describe uncaught exceptions we add a new terminal value. +A new [result](https://webassembly.github.io/spec/core/exec/runtime.html#syntax-result) value is added to describe uncaught exceptions. ``` -result ::= ... | T[val* (throw tagaddr)] +result ::= val* | trap + | T[val* (throw tagaddr)] ```