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

fix: Fix parsing error and a crash with non-reference-trait base type #4956

Merged
merged 18 commits into from
Jan 19, 2024

Conversation

RustanLeino
Copy link
Collaborator

@RustanLeino RustanLeino commented Jan 9, 2024

This PR fixes three bugs.

One bug was that the new resolver didn't check that the base type of a subset type was determined.

Another bug was that, even after reporting the error in the first bug, the resolver could crash downstream.

The third bug was that, even with a properly formed x: BaseType, the verifier would crash when trying to construct a default witness (if the base type is a non-reference trait and there is no explicit witness clause).

Fixes #4946

Note: I previously (and erroneously) thought the bug was a problem in the parser. But we do allow the syntax with just one identifier before the | in a subset-type declaration. The problem was that the new resolver didn't check to see that the type of that identifier was properly inferred.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@RustanLeino RustanLeino marked this pull request as ready for review January 9, 2024 01:45
@RustanLeino RustanLeino enabled auto-merge (squash) January 9, 2024 01:45
keyboardDrummer
keyboardDrummer previously approved these changes Jan 9, 2024
ssomayyajula
ssomayyajula previously approved these changes Jan 9, 2024
Copy link
Contributor

@ssomayyajula ssomayyajula left a comment

Choose a reason for hiding this comment

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

LGTM!

ssomayyajula
ssomayyajula previously approved these changes Jan 11, 2024
@RustanLeino RustanLeino merged commit 79e4ffa into dafny-lang:master Jan 19, 2024
20 checks passed
@RustanLeino RustanLeino deleted the issue-4946 branch January 19, 2024 23:30
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.

Resolver crashes on possibly empty subset type of trait
4 participants