New visualization for counterexamples

[camrein]

With the merge of https://github.com/dafny-lang/dafny/pull/1336, counterexamples may now display values of reference types. This makes inline counterexamples hard to read.

As suggested by @Dargones, something like a debugger view might be suitable here. As a first PoC (see branch), I've created a tree-view that displays the variables and their values for the active line: Further improvements (e.g. nesting) will probably require changes to the language server.

[Dargones]

This looks great, thank you for doing this! I can make the necessary changes to the language server to make nesting display possible. What format would be the most intuitive? My understanding is that one would have to edit CounterExampleItem class to achieve this but I am wondering what is the correct way to make these changes to preserve compatibility across versions of the plugin\server. There is also the issue of CounterExampleProvider in the older DafnyServer code - I am not certain if it is still being used and\or should be supported.

[camrein]

I can make the necessary changes to the language server to make nesting display possible. What format would be the most intuitive?

I guess some tree structure makes sense since it's a TreeView (basically the same as the file explorer of VSCode).

My understanding is that one would have to edit CounterExampleItem class to achieve this but I am wondering what is the correct way to make these changes to preserve compatibility across versions of the plugin\server.

Correct, that will affect CounterExampleItem. But making changes to it will break compatibility to older VSCode versions. Since the next extension update requires a new release of the Dafny, we should preserve the backward compatibility for the moment. Therefore, creating a new API similar to the one we have now makes sense, allowing the recursive structure we need. Although I'd prefer to create a notification mechanism for this, I think we should stick to the request/response one we have now not to overload the TextDocumentLoader and DafnyDocument classes.

There is also the issue of CounterExampleProvider in the older DafnyServer code - I am not certain if it is still being used and\or should be supported.

I don't know of any uses either. I don't even know if it's still compatible with the legacy extension. However, I think we should not break its serialization API either.

[Dargones]

Thank you and apologies for the belated response! So, should I modify CounterExampleItem at this point? Or does preserving backward compatibility means that adding new functionality requires creating a completely new "EnhancedCounterExampleItem" along with a new request that would return it?

[camrein]

I'd opt for creating a dedicated EnhancedCounterExampleItem / CounterExampleItemV2 (or whatever name suits best) to avoid mixing the different representation formats within the same data classes. Since we'll be using a new endpoint, you'd have to create a new ICounterExampleHandler interface with a suitable method name (e.g., dafny/counterExampleV2). Since I believe most of the logic stays the same as before, you're probably fine with implementing the interface within the existing DafnyCounterExampleHandler. If that's not the case you may want to create a dedicated implementation for the new version.

[keyboardDrummer]

I'm curious whether we can use the VSCode debugger to display counterexamples.

Verification errors in the Dafny program would show a lightbulb action that would start a debug session for this error. In the debug session, users can step through the statements of the program both forwards and backwards, and using breakpoints and the run-to-line command. By default the debugger would stop at the point where an assertion failed. At each statement, users can inspect variables with deeply hierarchical values using the variables tree view.

Implementation

For the implementation, we'd let our language server implement the debug adapter protocol. The attach request would specify which method we want to debug. I think a debugger based on counterexample information shouldn't be too hard. The counterexample data defines which statements the program visits chronologically, so we don't need an actual interpreter or execution environment for Dafny to implement the stepping actions. We could implement "time traveling debugging" basically for free. A while loop would likely be considered a single statement since that's how counterexamples consider them.

[seebees]

Yes, I think this is an excellent idea! The only thing I would add is that we should let the user interact with the counter example. If we let the user constrain some aspect of the counter example, then the user can get a clearer picture of what is going on.

I suspect that it would be worth trying to toss together some images in paint or something just to make sure we are all seeing the same thing :)