Post-mortem/investigation on #2828

[robin-aws]

#2790 introduced a case (issue ref), where the resolver crashed on an invalid Dafny program. This kind of regression is especially disruptive for those using the VSCode extension, since it crashes the extension completely, and it often isn't obvious to users what part of their code is triggering the bug so it looks like the extension is 100% broken.

Let's look into a few questions:

1. Are there general mechanisms for making the extension and/or language server more robust on a program that can't be resolved without an exception?
2. Are there general testing strategies for catching such bugs in the first place? Perhaps we could leverage https://github.com/dafny-lang/xdsmith to fuzz test by generating invalid programs.
3. Could we make the extension automatically offer to revert back to a previous version of Dafny when this happens?

[MikaelMayer]

1. Back in July, there was a mechanism to ensure that every call to parser and resolver handled the exception if any. I know that @keyboardDrummer has modified the exception reporting mechanism since, but it's still there for the resolver and parser alltogether
2. I don't know of any current testing strategy
3. Everything is possible

[cpitclaudel]

One thing that happens often is that you have an error in your code, the default path after detecting that error in the resolver breaks an invariant (e.g. something ends up being null or a TypeProxy), and later the code crashes.

In these cases the CLI output shows the error before the crash. So, we should either:

• Tell the user to run on the CLI
• Warn about the crash but still display any accumulated errors.

The second option would be particularly nice, but how easy is it?

[keyboardDrummer]

Are there general mechanisms for making the extension and/or language server more robust on a program that can't be resolved without an exception?

Testing the IDE with the bug: it doesn’t recover if you remove the code that triggers the bug, even though it should. I'm guessing it fails to update the document state after you trigger the bug so it keeps working with the broken document.

Also, even though in the case of this bug the problem occurs both in the CLI and LSP server, I think we can do better to ensure uniformity between server and CLI. I think we should expose a small Dafny agnostic compiler API, something similar to LSP, that exposes enough for both the language server and CLI to operate on, so there is little room for differences between the CLI and language server. This would also mean we remove the duplication in compilation driving logic that exists between LSP server and CLI.

A coarse way to view this is that the CLI would run on top of the current LSP server back-end, which would move to DafnyPipeline : )

Also, PR related to this postmortem: #2949

[cpitclaudel]

I think we should expose a small Dafny agnostic compiler API, something similar to LSP, that exposes enough for both the language server and CLI to operate on, so there is little room for differences between the CLI and language server.

#2229 was a bit of that, but it wasn't complete (and we abandoned it because there was no identified use case at the time).

[keyboardDrummer]

Action item: #2945