Skip to content
This repository was archived by the owner on Apr 25, 2025. It is now read-only.

Dependencies in proposal #99

Merged
merged 7 commits into from
Mar 5, 2020

Conversation

ioannad
Copy link
Collaborator

@ioannad ioannad commented Feb 10, 2020

This PR adds the dependency to multi-value to the exception handling proposal text and to the README.

I wrote an explanation of this dependency on the proposal text, but it's easier to see this once the verification and execution steps of br_on_exn and of try blocks are written out, as done here by @rossberg :

Validation:

ft = t1* -> t2*
C, label t2* |- e1* : t1* -> t2*
C, label t2* |- e2* : exnref -> t2*
-----------------------------------
C |- try ft e1* catch e2* end : ft

C_label(l) = C_exn(x) = t*
-------------------------------------
C |- br_on_exn l x : exnref -> exnref

Execution:

v^n (try ft e1* catch e2* end)  -->  catch_m{e2*} (label_m{} v^n e1* end) end)
  (iff ft = t1^n -> t2^m)
S; F; catch_m{e*} T[v^n (throw a)] end  -->  S; F; label_m{} (exn a v^n) e* end
  (iff S_exn(a) = {typ t^n})

F; (exn a v*) (br_on_exn l x)  -->  F; v* (br l)
  (iff F_exn(x) = a)

Concerning the functionality of try-catch blocks, note especially the passing of v^n values into a label_m{}.
Concerning the functionality of br_on_exn, note especially the execution step resulting in a br instruction.

cc: @aheejin @Ms2ger @dhil

Copy link
Member

@aheejin aheejin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you! Sorry for the delayed reply.

@aheejin aheejin requested a review from rossberg February 17, 2020 03:43
Copy link
Member

@rossberg rossberg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM modulo @aheejin's comments.

@ioannad
Copy link
Collaborator Author

ioannad commented Mar 2, 2020

Sorry for the delayed action! I think I addressed all your comments, @aheejin. Thank you and @rossberg for the review.

@aheejin aheejin merged commit 4e8c37e into WebAssembly:master Mar 5, 2020
@ioannad ioannad deleted the dependencies-in-proposal branch March 5, 2020 09:07
ioannad pushed a commit to ioannad/exception-handling that referenced this pull request Jun 6, 2020
This PR adds the dependency to multi-value to the exception handling proposal text and to the README.

I wrote an explanation of this dependency on the proposal text, but it's easier to see this once the verification and execution steps of `br_on_exn` and of `try` blocks are written out, as done [here](WebAssembly#87 (comment)) by @rossberg :

Validation:

```
ft = t1* -> t2*
C, label t2* |- e1* : t1* -> t2*
C, label t2* |- e2* : exnref -> t2*
-----------------------------------
C |- try ft e1* catch e2* end : ft

C_label(l) = C_exn(x) = t*
-------------------------------------
C |- br_on_exn l x : exnref -> exnref
```

Execution:

```
v^n (try ft e1* catch e2* end)  -->  catch_m{e2*} (label_m{} v^n e1* end) end)
  (iff ft = t1^n -> t2^m)
S; F; catch_m{e*} T[v^n (throw a)] end  -->  S; F; label_m{} (exn a v^n) e* end
  (iff S_exn(a) = {typ t^n})

F; (exn a v*) (br_on_exn l x)  -->  F; v* (br l)
  (iff F_exn(x) = a)
```

Concerning the functionality of `try`-`catch` blocks, note especially the passing of `v^n` values into a `label_m{}`.
Concerning the functionality of `br_on_exn`, note especially the execution step resulting in a `br` instruction.
aheejin added a commit to aheejin/exception-handling that referenced this pull request Jun 12, 2020
This reverts commit 10d6c6c.

This reverts WebAssembly#96, which squashed all upstream commits into one, which
was not the recommended way in
https://github.com/WebAssembly/proposals/blob/master/howto.md#syncing-with-upstream-changes.

This leaves README.md untouched because WebAssembly#99 made significant changes on
top of the merged version already.
aheejin added a commit that referenced this pull request Jun 15, 2020
This reverts commit 10d6c6c.

This reverts #96, which squashed all upstream commits into one, which
was not the recommended way in
https://github.com/WebAssembly/proposals/blob/master/howto.md#syncing-with-upstream-changes.

This leaves README.md untouched because #99 made significant changes on
top of the merged version already.
ioannad pushed a commit to ioannad/exception-handling that referenced this pull request Feb 23, 2021
ioannad pushed a commit to ioannad/exception-handling that referenced this pull request Feb 23, 2021
This PR adds the dependency to multi-value to the exception handling proposal text and to the README. 

I wrote an explanation of this dependency on the proposal text, but it's easier to see this once the verification and execution steps of `br_on_exn` and of `try` blocks are written out, as done [here](WebAssembly#87 (comment)) by @rossberg :

Validation:

```
ft = t1* -> t2*
C, label t2* |- e1* : t1* -> t2*
C, label t2* |- e2* : exnref -> t2*
-----------------------------------
C |- try ft e1* catch e2* end : ft

C_label(l) = C_exn(x) = t*
-------------------------------------
C |- br_on_exn l x : exnref -> exnref
```

Execution: 

```
v^n (try ft e1* catch e2* end)  -->  catch_m{e2*} (label_m{} v^n e1* end) end)
  (iff ft = t1^n -> t2^m)
S; F; catch_m{e*} T[v^n (throw a)] end  -->  S; F; label_m{} (exn a v^n) e* end
  (iff S_exn(a) = {typ t^n})

F; (exn a v*) (br_on_exn l x)  -->  F; v* (br l)
  (iff F_exn(x) = a)
```

Concerning the functionality of `try`-`catch` blocks, note especially the passing of `v^n` values into a `label_m{}`.
Concerning the functionality of `br_on_exn`, note especially the execution step resulting in a `br` instruction.
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants