fix: Added code to catch resolver exceptions if any. #2080
Conversation
MikaelMayer
changed the title
Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs
Outdated
Show resolved
Hide resolved
| visitor.Visit(symbolTable.CompilationUnit.Program); | ||
| return visitor.GhostDiagnostics; | ||
| } catch (Exception e) { | ||
| logger.LogDebug(e, "encountered an exception while getting ghost state diagnostics of {Name}", symbolTable.CompilationUnit.Name); |
There was a problem hiding this comment.
This will not be visible to users, right? Aren't these logs only written to disk in a somewhat hidden location?
There was a problem hiding this comment.
Yes they are written next to DafnyLanguageServer.dll, and only if an option is activated.
But this kind of error can happen if the language server recovered from problematic resolving, and leaving the program in a state that the Ghost Diagnostic Collector is not assuming, so that's why it's less important.
…olver.cs Co-authored-by: Clément Pit-Claudel <[email protected]>
|
Can we add tests by using dependency injection to inject a broken implementation? The reason I ask is because having a reliable language server is so important and without tests it seems easy to lose the functionality you added in this PR again. |
Yes you're right. |
|
|
||
| [TestMethod] | ||
| public void EnsureResilienceAgainstErrors() { | ||
| // Builtins is null to trigger an error. |
There was a problem hiding this comment.
It seems like this test relies on some badly defined API of DafnyPipeline.csproj, that it requires Builtins to be not null, to trigger the exception. I think it might be nicer if the test uses a more explicit API to trigger a failure, like mocking something from DafnyPipeline.csproj and letting the mock throw an Exception, but I imagine DafnyPipeline.csproj is not setup for being mocked.
There was a problem hiding this comment.
Yes you identified this test correctly.
I don't see either how to mock the DafnyPipeline, so I took the route of the minimum working test for now.
As a prevention measure for issues such as #2074
I added some code that catches exceptions coming from the Resolver so that it won't impact user experience in the IDE.
I also added some catching code for Ghost Diagnostics because they were impacted as well.
The result is a non-blocking diagnostic that does not crash the server anymore:
Moreover, it returns also all the other resolution errors so that users are not helpless:
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.