Resolve a concurrency bug that could cause the IDE server not to send…

… updates for a particular version (dafny-lang#5299)

### Description
- Resolve a concurrency bug that could cause the IDE server not to send
updates. From the data I have, my theory is that this was caused by
UpdateDocument setting `latestIdeState` with an updated version, as it
should, but after that an old compilation would also set
`latestIdeState` with an old version, and the new compilation would pick
up this old version and keep using it. The notification publisher would
then not send any updates because it would consider them to be for an
old version. The old compilation being able to set `latestIdeState` when
it should not was caused by a call to `observerSubscription.Dispose();`
being done too late, and this PR resolves that.
- Refactor UpdateDocument and StartNewCompilation so they are easier to
read.

### How has this been tested?
I don't know how to reproduce the issue, but this PR should greatly
reduce the amount of random test failures

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/Pipeline/CompilationInput.cs

@@ -7,22 +7,12 @@ namespace Microsoft.Dafny {
   /// <summary>
   /// Contains all the inputs of a Compilation
   /// </summary>
-  public class CompilationInput {
+  public record CompilationInput(DafnyOptions Options, int Version, DafnyProject Project) {
 
     public override string ToString() {
       return $"URI: {Uri}, Version: {Version}";
     }
-
-    public int Version { get; }
-    public DafnyOptions Options { get; }
-    public DafnyProject Project { get; }
     public DocumentUri Uri => Project.Uri;
-
-    public CompilationInput(DafnyOptions options, int version, DafnyProject project) {
-      Options = options;
-      Version = version;
-      Project = project;
-    }
   }
 
   public record BufferLine(int LineNumber, int StartIndex, int EndIndex);

Source/DafnyLanguageServer/Workspace/IdeState.cs

@@ -31,7 +31,6 @@ public record IdeCanVerifyState(VerificationPreparationState PreparationProgress
 /// to provide the IDE with as much information as possible.
 /// </summary>
 public record IdeState(
-  int Version,
   ISet<Uri> OwnedUris,
   CompilationInput Input,
   CompilationStatus Status,
@@ -47,6 +46,7 @@ public record IdeState(
   ImmutableDictionary<Uri, DocumentVerificationTree> VerificationTrees
 ) {
   public Uri Uri => Input.Uri.ToUri();
+  public int Version => Input.Version;
 
   public static IEnumerable<Diagnostic> MarkDiagnosticsAsOutdated(IEnumerable<Diagnostic> diagnostics) {
     return diagnostics.Select(diagnostic => diagnostic with {
@@ -59,7 +59,7 @@ public static IEnumerable<Diagnostic> MarkDiagnosticsAsOutdated(IEnumerable<Diag
 
   public static IdeState InitialIdeState(CompilationInput input) {
     var program = new EmptyNode();
-    return new IdeState(input.Version, ImmutableHashSet<Uri>.Empty,
+    return new IdeState(ImmutableHashSet<Uri>.Empty,
       input,
       CompilationStatus.Parsing,
       program,
@@ -96,7 +96,9 @@ public IdeState Migrate(DafnyOptions options, Migrator migrator, int newVersion,
       oldDiagnostics = oldDiagnostics.Add(phase, diagnostics);
     }
     return this with {
-      Version = newVersion,
+      Input = Input with {
+        Version = newVersion
+      },
       OldDiagnostics = oldDiagnostics,
       NewDiagnostics = ImmutableDictionary<IPhase, ImmutableList<FileDiagnostic>>.Empty,
       Status = CompilationStatus.Parsing,

Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs

@@ -33,14 +33,17 @@ public IdeStateObserver(ILogger logger,
     this.notificationPublisher = notificationPublisher;
   }
 
-  public void OnCompleted() {
+  public void Clear() {
     var ideState = initialState with {
-      Version = LastPublishedState.Version + 1
+      Input = initialState.Input with { Version = LastPublishedState.Version + 1 }
     };
     notificationPublisher.PublishNotifications(LastPublishedState, ideState);
     telemetryPublisher.PublishUpdateComplete();
   }
 
+  public void OnCompleted() {
+  }
+
   public void OnError(Exception exception) {
   }
 

Source/DafnyLanguageServer/Workspace/ProjectManager.cs

@@ -118,26 +118,56 @@ public ProjectManager(
   private const int MaxRememberedChanges = 100;
 
   public void UpdateDocument(DidChangeTextDocumentParams documentChange) {
-    var migrator = createMigrator(documentChange, CancellationToken.None);
+    StartNewCompilation(documentChange.TextDocument.Uri.ToUri(), documentChange);
+  }
+
+  private void StartNewCompilation(Uri triggeringFile, DidChangeTextDocumentParams? changes) {
+    observerSubscription.Dispose();
+    version += 1;
+
+    Migrator? migrator = null;
+    if (changes != null) {
+      migrator = createMigrator(changes, CancellationToken.None);
+      // If we migrate the observer before accessing latestIdeState, we can be sure it's migrated before it receives new events.
+      observer.Migrate(options, migrator, version);
+      latestIdeState = latestIdeState.Migrate(options, migrator, version, false);
+    }
 
-    var upcomingVersion = version + 1;
-    // If we migrate the observer before accessing latestIdeState, we can be sure it's migrated before it receives new events.
-    observer.Migrate(options, migrator, upcomingVersion);
-    latestIdeState = latestIdeState.Migrate(options, migrator, upcomingVersion, false);
-    StartNewCompilation();
+    Compilation.Dispose();
+    var input = new CompilationInput(options, version, Project);
+    Compilation = createCompilation(boogieEngine, input);
+    var migratedUpdates = GetStates(Compilation);
+    states = new ReplaySubject<IdeState>(1);
+    var statesSubscription = observerSubscription =
+      migratedUpdates.Do(s => latestIdeState = s).Subscribe(states);
+
+    var throttleTime = options.Get(UpdateThrottling);
+    var throttledUpdates = throttleTime == 0 ? States : States.Sample(TimeSpan.FromMilliseconds(throttleTime));
+
+    var throttledSubscription = throttledUpdates.Subscribe(observer);
+    observerSubscription = new CompositeDisposable(statesSubscription, throttledSubscription);
+
+    Compilation.Start();
+
+    if (changes != null) {
+      UpdateRecentChanges(changes, migrator);
+    }
+    TriggerVerificationForFile(triggeringFile);
+  }
 
+  private void UpdateRecentChanges(DidChangeTextDocumentParams changes, Migrator? migrator) {
     lock (RecentChanges) {
-      var newChanges = documentChange.ContentChanges.Where(c => c.Range != null).
+      var newChanges = changes.ContentChanges.Where(c => c.Range != null).
         Select(contentChange => new Location {
           Range = contentChange.Range!,
-          Uri = documentChange.TextDocument.Uri
+          Uri = changes.TextDocument.Uri
         });
       var migratedChanges = RecentChanges.Select(location => {
-        if (location.Uri != documentChange.TextDocument.Uri) {
+        if (location.Uri != changes.TextDocument.Uri) {
           return location;
         }
 
-        var newRange = migrator.MigrateRange(location.Range);
+        var newRange = migrator!.MigrateRange(location.Range);
         if (newRange == null) {
           return null;
         }
@@ -148,30 +178,6 @@ public void UpdateDocument(DidChangeTextDocumentParams documentChange) {
       }).Where(r => r != null);
       RecentChanges = newChanges.Concat(migratedChanges).Take(MaxRememberedChanges).ToList()!;
     }
-    TriggerVerificationForFile(documentChange.TextDocument.Uri.ToUri());
-  }
-
-  private void StartNewCompilation() {
-    ++version;
-    logger.LogDebug("Clearing result for workCompletedForCurrentVersion");
-
-    observerSubscription.Dispose();
-
-    Compilation.Dispose();
-    var input = new CompilationInput(options, version, Project);
-    Compilation = createCompilation(boogieEngine, input);
-    var migratedUpdates = GetStates(Compilation);
-    states = new ReplaySubject<IdeState>(1);
-    var statesSubscription = observerSubscription =
-      migratedUpdates.Do(s => latestIdeState = s).Subscribe(states);
-
-    var throttleTime = options.Get(UpdateThrottling);
-    var throttledUpdates = throttleTime == 0 ? States : States.Sample(TimeSpan.FromMilliseconds(throttleTime));
-
-    var throttledSubscription = throttledUpdates.Subscribe(observer);
-    observerSubscription = new CompositeDisposable(statesSubscription, throttledSubscription);
-
-    Compilation.Start();
   }
 
   private IObservable<IdeState> GetStates(Compilation compilation) {
@@ -246,7 +252,7 @@ public bool CloseDocument(Uri uri) {
   public void CloseAsync() {
     Compilation.Dispose();
     try {
-      observer.OnCompleted();
+      observer.Clear();
     } catch (OperationCanceledException) {
     }
     Dispose();
@@ -343,8 +349,7 @@ public void OpenDocument(Uri uri, bool triggerCompilation) {
     openFiles.TryAdd(uri, 1);
 
     if (triggerCompilation) {
-      StartNewCompilation();
-      TriggerVerificationForFile(uri);
+      StartNewCompilation(uri, null);
     }
   }