Crash of Language Server

[MikaelMayer]

A reproducible permanent crash of gutter icons that requires restarting VSCode

Just got this exception while editing the text, on the latest nightly (3.9.1 + all recent commits)

Code to reproduce on the language server

function bullspec(s:seq<nat>, u:seq<nat>): (r: nat)
  requires |s| > 0
  requires |u| > 0
  requires |s| == |u|
  ensures forall i | i < r :: s[i] != u[i]
  ensures r == |s| || s[r] == u[r]
{
  if |s| == 0 then 0 else
  if |s| == 1 then
    if s[0]==u[0] 
    then 1 else 0
  else
    if s[0] != u[0] 
    then bullspec(s[1..],u[1..])
    else 1+bullspec(s[1..],u[1..])
}

AFter this code verifies, select the following and delete it (with the first newline)

  if |s| == 1 then
    if s[0]==u[0] 
    then 1 else 0

Then, select the dangling else and remove it (with the space before).
I get the following exception:

Unhandled exception. System.ArgumentException: Offset and length were out of bounds for the array or count is greater than the number of elements from index to the end of the source collection.
   at System.Collections.Generic.List`1.GetRange(Int32 index, Int32 count)
   at Microsoft.Dafny.LanguageServer.Workspace.Notifications.VerificationTree.RenderInto(LineVerificationStatus[] perLineDiagnostics, Boolean contextHasErrors, Boolean contextIsPending, Range otherRange, Range contextRange) in dafny\Source\DafnyLanguageServer\Workspace\Notifications\VerificationDiagnosticsParams.cs:line 326
   at Microsoft.Dafny.LanguageServer.Workspace.Notifications.AssertionVerificationTree.RenderInto(LineVerificationStatus[] perLineDiagnostics, Boolean contextHasErrors, Boolean contextIsPending, Range otherRange, Range contextRange) in dafny\Source\DafnyLanguageServer\Workspace\Notifications\VerificationDiagnosticsParams.cs:line 617
   at Microsoft.Dafny.LanguageServer.Workspace.Notifications.VerificationTree.RenderInto(LineVerificationStatus[] perLineDiagnostics, Boolean contextHasErrors, Boolean contextIsPending, Range otherRange, Range contextRange) in dafny\Source\DafnyLanguageServer\Workspace\Notifications\VerificationDiagnosticsParams.cs:line 314
   at Microsoft.Dafny.LanguageServer.Workspace.Notifications.VerificationTree.RenderInto(LineVerificationStatus[] perLineDiagnostics, Boolean contextHasErrors, Boolean contextIsPending, Range otherRange, Range contextRange) in dafny\Source\DafnyLanguageServer\Workspace\Notifications\VerificationDiagnosticsParams.cs:line 314
   at Microsoft.Dafny.LanguageServer.Workspace.Notifications.VerificationStatusGutter.RenderPerLineDiagnostics(DocumentUri uri, VerificationTree[] verificationTrees, Int32 numberOfLines, Boolean verificationStarted, Container`1 parseAndResolutionErrors) in dafny\Source\DafnyLanguageServer\Workspace\Notifications\VerificationDiagnosticsParams.cs:line 60
   at Microsoft.Dafny.LanguageServer.Workspace.Notifications.VerificationStatusGutter.ComputeFrom(DocumentUri uri, Int32 version, VerificationTree[] verificationTrees, Container`1 resolutionErrors, Int32 linesCount, Boolean verificationStarted) in dafny\Source\DafnyLanguageServer\Workspace\Notifications\VerificationDiagnosticsParams.cs:line 36
   at Microsoft.Dafny.LanguageServer.Workspace.NotificationPublisher.PublishGutterIcons(IdeState state, Boolean verificationStarted) in dafny\Source\DafnyLanguageServer\Workspace\NotificationPublisher.cs:line 100
   at Microsoft.Dafny.LanguageServer.Workspace.VerificationProgressReporter.ReportRealtimeDiagnostics(Boolean verificationStarted, DocumentAfterResolution document) in dafny\Source\DafnyLanguageServer\Workspace\VerificationProgressReporter.cs:line 211
   at Microsoft.Dafny.LanguageServer.Workspace.VerificationProgressReporter.ReportAssertionBatchResult(AssertionBatchResult batchResult) in dafny\Source\DafnyLanguageServer\Workspace\VerificationProgressReporter.cs:line 369
   at System.Reactive.AnonymousSafeObserver`1.OnNext(T value) in /_/Rx.NET/Source/src/System.Reactive/AnonymousSafeObserver.cs:line 54
   at System.Reactive.ObserveOnObserverNew`1.DrainStep(ConcurrentQueue`1 q) in /_/Rx.NET/Source/src/System.Reactive/Internal/ScheduledObserver.cs:line 559
   at System.Reactive.ObserveOnObserverNew`1.DrainShortRunning(IScheduler recursiveScheduler) in /_/Rx.NET/Source/src/System.Reactive/Internal/ScheduledObserver.cs:line 513
   at System.Reactive.Concurrency.EventLoopScheduler.Run() in /_/Rx.NET/Source/src/System.Reactive/Concurrency/EventLoopScheduler.cs:line 356
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location ---
   at System.Runtime.ExceptionServices.ExceptionDispatchInfo.Throw()

It's worth noting that only gutter icons and status bar are affected; diagnostics are still correctly received and displayed.

Behavior on older versions of Dafny

• 3.9.1: Same as latest nightly
• 3.9.0 and 3.8.1: No apparent crash error message, but otherwise it's the same behavior.

[MikaelMayer]

@keyboardDrummer I just looked a bit into it. The error arise from there:

dafny/Source/DafnyLanguageServer/Workspace/DocumentManager.cs

Lines 109 to 118 in 4bd935f

	var migratedVerificationTree =
	relocator.RelocateVerificationTree(lastPublishedState.VerificationTree, updatedText.NumberOfLines, documentChange, CancellationToken.None);
	Compilation = new Compilation(
	services,
	verifierOptions,
	updatedText,
	// TODO do not pass this to CompilationManager but instead use it in FillMissingStateUsingLastPublishedDocument
	migratedVerificationTree
	);

As you see, we are not migrating the compilation.migratedVerificationTree, but the lastPublishedState.VerificationTree
The problem is that, with the second edit, lastPublishedState.VerificationTree was not modified after the parse error, so it contains assertions with lines numbers up to 14 when the file only has 13 lines.
The proper solution would be to replace lastPublishedState.VerificationTree by compilation.migratedVerificationTree,
or to ensure that lastPublishedState.VerificationTree surely contains the migrated version, even after a parse error.

[MikaelMayer]

@keyboardDrummer here is the PR that reproduces the issue without fixing it for now.

#3064