Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[interpreter] Add support for validation and evaluation for exceptions #175

Merged
merged 8 commits into from
Sep 15, 2021

Conversation

takikawa
Copy link
Collaborator

@takikawa takikawa commented Jul 15, 2021

This PR adds support for validation and evaluation of exception instructions in the reference interpreter.

I've split it into several commits to hopefully make it easier to review. The PR also expands the core tests to add more tests for validation, and to adjust some cases that I think were meant to be checking traps instead of throwing exceptions.

The PR was tested against V8 and SpiderMonkey to check that the test results agree, and as far as I can tell they all appear to for the core exceptions tests in the current test suite.

Some of the code here was based on existing code in https://github.com/effect-handlers/wasm-effect-handlers/tree/exception-handlers and it tries to follow the formal spec overview in #143.

The main differences from the formal spec have to do with how contexts are handled. Like how br is currently handled in the interpreter (with Breaking), administrative instructions like Throwing, Rethrowing, Delegating will "bubble up" until they traverse the appropriate context. This is particularly complicated for rethrow, because it needs to first unwind up to the appropriate context (to find the exception), and then re-install the original continuation to rethrow from the right place.

There are some small differences in the interpreter from the formal spec for validating try-delegate (already communicated these to @ioannad so we can sync the spec and interpreter):

  • Delegate contexts need to start checking 1 level further out (to avoid counting the immediate label around the delegate)
  • The label store also needs to track a body label in case try-delegate delegates to the function body

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.

This looks good at large! However, I'd strongly suggest removing the special handling of delegation to function bodies, since it does seem to contradict the design doc.

Yeah, the complication regarding the construction of rethrow contexts is a bit annoying. A simpler way in this setting would obviously be to duplicate the exceptions in the configuration or frame, but that wouldn't be as faithful a representation of the formal semantics.

interpreter/exec/eval.ml Outdated Show resolved Hide resolved
interpreter/runtime/tag.ml Outdated Show resolved Hide resolved
interpreter/exec/eval.ml Outdated Show resolved Hide resolved
interpreter/script/run.ml Outdated Show resolved Hide resolved
interpreter/valid/valid.ml Outdated Show resolved Hide resolved
interpreter/exec/eval.ml Outdated Show resolved Hide resolved
interpreter/exec/eval.ml Show resolved Hide resolved
interpreter/exec/eval.ml Outdated Show resolved Hide resolved
interpreter/exec/eval.ml Outdated Show resolved Hide resolved
interpreter/exec/eval.ml Outdated Show resolved Hide resolved
interpreter/valid/valid.ml Outdated Show resolved Hide resolved
interpreter/valid/valid.ml Outdated Show resolved Hide resolved
ioannad added a commit to ioannad/exception-handling that referenced this pull request Aug 25, 2021
The latter matches the interpreter implementation in PR WebAssembly#175
@takikawa
Copy link
Collaborator Author

takikawa commented Sep 2, 2021

I believe all the existing feedback on this PR has been addressed now. I pushed some minor changes (e.g., integrated the option 3 semantics into the validation commit and re-arranged commit history) and with #176 resolved, the interpreter should reflect the semantics we agree on now I think.

If anyone else has any additional feedback (@rossberg or @aheejin for example), would be happy to address it.

@rossberg
Copy link
Member

rossberg commented Sep 3, 2021

@takikawa, hm, in the future, please do not force-push to a PR branch that's already under review. Rewriting commit history breaks the review history and makes it impossible for reviewers to see the delta since their last comments. ;)

interpreter/exec/eval.ml Outdated Show resolved Hide resolved
Comment on lines +578 to +579
| Catch (n, cts, ca, (vs', {it = Delegating (0l, a, vs0); at} :: es')), vs ->
vs, [Catch (n, cts, ca, (vs', (Throwing (a, vs0) @@ at) :: es')) @@ e.at]
Copy link
Member

Choose a reason for hiding this comment

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

Since delegation always targets a label, this rule should be unnecessary.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

This rule seems needed as tests fail without it. I believe the issue is that since the label is outside the catch (when TryCatch is reduced to [Label (... [Catch ...])]), if we drop the Catch and let Delegating go up to the label, the handler that we were supposed to delegate to is gone.

Copy link
Member

Choose a reason for hiding this comment

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

I see. Hm, this is a bit unfortunate. Operationally, we could just switch around the nesting of Label and Catch to handle this naturally, but that would break the hack we use to type catch labels... Fine for now I guess, maybe I can come up with an idea later.

@ioannad, FYI, since @takikawa's observation likely applies to the formal reduction rules as well.

interpreter/valid/valid.ml Outdated Show resolved Hide resolved
@takikawa
Copy link
Collaborator Author

takikawa commented Sep 3, 2021

Whoops sorry for the loss of review history, I'll avoid editing the history now until it gets merged at the end.

@aheejin aheejin mentioned this pull request Sep 7, 2021
11 tasks
Comment on lines +578 to +579
| Catch (n, cts, ca, (vs', {it = Delegating (0l, a, vs0); at} :: es')), vs ->
vs, [Catch (n, cts, ca, (vs', (Throwing (a, vs0) @@ at) :: es')) @@ e.at]
Copy link
Member

Choose a reason for hiding this comment

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

I see. Hm, this is a bit unfortunate. Operationally, we could just switch around the nesting of Label and Catch to handle this naturally, but that would break the hack we use to type catch labels... Fine for now I guess, maybe I can come up with an idea later.

@ioannad, FYI, since @takikawa's observation likely applies to the formal reduction rules as well.

@takikawa
Copy link
Collaborator Author

takikawa commented Sep 8, 2021

Now that there's one review approval, is anyone else interested in reviewing or shall I merge this already? (@thibaudmichaud or @aheejin perhaps)

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.

Thanks! And sorry for the delayed reply. I don't have expertise to review the ML code so I only looked at the tests and they look good to me.

test/core/rethrow.wast Show resolved Hide resolved
@takikawa
Copy link
Collaborator Author

Thanks for the review approvals! I'll go ahead and merge this now as the CI is green except for the spec build (failing for unrelated reasons---I will try to fix this separately as it's confusing to have it continue to fail due to a build related issue).

@takikawa takikawa merged commit ea7f2c0 into WebAssembly:master Sep 15, 2021
@takikawa takikawa deleted the validation-and-execution branch September 15, 2021 20:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants