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.

Sign up for GitHub

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

Jump to bottom

NullPointerException fixed in Parser #1683

Merged
merged 16 commits into from
Jan 11, 2022
Merged

NullPointerException fixed in Parser #1683

merged 16 commits into from
Jan 11, 2022

Conversation

MikaelMayer
Copy link
Member

@MikaelMayer MikaelMayer commented Jan 4, 2022 •
edited
Loading

This PR fixes one problem of #1682

I added a tests to ensure does not happen again for this particular case

#1694 fixes the two other problems

@MikaelMayer MikaelMayer self-assigned this Jan 4, 2022
@MikaelMayer MikaelMayer changed the title Fix for a parse error NullPointerException fixed in Parser, Parser exception recovery for Language Server Jan 4, 2022
@MikaelMayer MikaelMayer marked this pull request as ready for review January 4, 2022 18:30
@MikaelMayer MikaelMayer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) part: parser First phase of Dafny's pipeline labels Jan 4, 2022
atomb
atomb reviewed Jan 5, 2022
View reviewed changes
Source/Dafny/Dafny.atg Outdated
)
{ Attribute<ref attrs> } (. r.Attributes = attrs; .)
{ Attribute<ref attrs> } (. if(r != null) { r.Attributes = attrs; } .)
Copy link
Member

Choose a reason for hiding this comment

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

Is it possible that this can lead to some portion of the source code being silently ignored? And, if so, can we detect it and emit a useful error message?

Copy link
Member Author

Choose a reason for hiding this comment

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

I don't know to what extent it will ignore portions of the source code, because before it would actually crash. The new behavior is thus strictly better than the previous one, but again I can't guarantee the absence of null pointer exceptions.

Source/DafnyLanguageServer/Language/DafnyLangParser.cs Outdated Show resolved Hide resolved
camrein
camrein requested changes Jan 5, 2022
View reviewed changes
Copy link
Member

@camrein camrein left a comment

Choose a reason for hiding this comment

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

Looks good to improve the language server's stability.
I only request to change the way you log the exception.

Source/DafnyLanguageServer/Language/DafnyLangParser.cs Outdated Show resolved Hide resolved
Source/DafnyLanguageServer/Language/DafnyLangParser.cs Outdated Show resolved Hide resolved
fabiomadge
fabiomadge previously approved these changes Jan 5, 2022
View reviewed changes
@camrein
Copy link
Member

camrein commented Jan 6, 2022

Did you forget to push your last changes? I don't see any difference.

keyboardDrummer
keyboardDrummer reviewed Jan 6, 2022
View reviewed changes
Copy link
Member

@keyboardDrummer keyboardDrummer left a comment

Choose a reason for hiding this comment

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

This PR fixes all three problems of #1682

I'd prefer having separate PRs for issues that can solved separately. I know this PR is small, but having the DafnyLangParser change in a separate PR would for example make it easier to see whether there's a test change for this functional change.

@MikaelMayer
Copy link
Member Author

Did you forget to push your last changes? I don't see any difference.

Indeed, I must have been distracted or the push failed and I did not check it.

camrein
camrein previously approved these changes Jan 7, 2022
View reviewed changes
@MikaelMayer MikaelMayer mentioned this pull request Jan 7, 2022
Merged
@MikaelMayer
Copy link
Member Author

This PR fixes all three problems of #1682

I'd prefer having separate PRs for issues that can solved separately. I know this PR is small, but having the DafnyLangParser change in a separate PR would for example make it easier to see whether there's a test change for this functional change.

Here you are:
#1694

RustanLeino
RustanLeino reviewed Jan 7, 2022
View reviewed changes
Test/git-issues/git-issue-1682.dfy Outdated Show resolved Hide resolved
Source/Dafny/Dafny.atg Outdated Show resolved Hide resolved
@MikaelMayer MikaelMayer changed the title NullPointerException fixed in Parser, Parser exception recovery for Language Server NullPointerException fixed in Parser Jan 10, 2022
@MikaelMayer MikaelMayer enabled auto-merge (squash) January 10, 2022 17:47
@MikaelMayer MikaelMayer merged commit ef07877 into master Jan 11, 2022
@MikaelMayer MikaelMayer deleted the fix-1682 branch January 11, 2022 16:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@atomb atomb atomb approved these changes

@keyboardDrummer keyboardDrummer keyboardDrummer approved these changes

@fabiomadge fabiomadge fabiomadge left review comments

@RustanLeino RustanLeino Awaiting requested review from RustanLeino

@camrein camrein Awaiting requested review from camrein

Assignees

@MikaelMayer MikaelMayer

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) part: parser First phase of Dafny's pipeline
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@MikaelMayer @camrein @atomb @fabiomadge @keyboardDrummer @RustanLeino