Added concurrent tests

Source/DafnyLanguageServer.Test/Diagnostics/ConcurrentLinearVerificationDiagnosticTester.cs

@@ -0,0 +1,74 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text.RegularExpressions;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
+using Microsoft.VisualStudio.TestTools.UnitTesting;
+using OmniSharp.Extensions.JsonRpc;
+using OmniSharp.Extensions.LanguageServer.Protocol.Document;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics;
+
+[TestClass]
+public class ConcurrentLinearVerificationDiagnosticTester : LinearVerificationDiagnosticTester {
+ private const int MaxSimultaneousVerificationTasks = 3;
+
+ protected DiagnosticsReceiver[] diagnosticsReceivers = new DiagnosticsReceiver[MaxSimultaneousVerificationTasks];
+ protected TestNotificationReceiver<VerificationStatusGutter>[] verificationDiagnosticsReceivers =
+ new TestNotificationReceiver<VerificationStatusGutter>[MaxSimultaneousVerificationTasks];
+
+ private void NotifyAllDiagnosticsReceivers(PublishDiagnosticsParams request) {
+ foreach (var receiver in diagnosticsReceivers) {
+ receiver.NotificationReceived(request);
+ }
+ }
+
+ private void NotifyAllVerificationDiagnosticsReceivers(VerificationStatusGutter request) {
+ foreach (var receiver in verificationDiagnosticsReceivers) {
+ receiver.NotificationReceived(request);
+ }
+ }
+
+ [TestInitialize]
+ public override async Task SetUp() {
+ for (var i = 0; i < diagnosticsReceivers.Length; i++) {
+ diagnosticsReceivers[i] = new();
+ verificationDiagnosticsReceivers[i] = new();
+ }
+ verificationDiagnosticsReceiver = new();
+ client = await InitializeClient(options =>
+ options
+ .OnPublishDiagnostics(NotifyAllDiagnosticsReceivers)
+ .AddHandler(DafnyRequestNames.VerificationStatusGutter,
+ NotificationHandler.For<VerificationStatusGutter>(NotifyAllVerificationDiagnosticsReceivers))
+ );
+ }
+
+ [TestMethod/*, Timeout(MaxTestExecutionTimeMs)*/]
+ public async Task EnsuresManyDocumentsCanBeVerifiedAtOnce() {
+ var result = new List<Task>();
+ for (var i = 0; i < MaxSimultaneousVerificationTasks; i++) {
+ result.Add(VerifyTrace(@"
+ . | | | I | | :predicate F(i: int) {
+ . | | | I | | : false // Should not be highlighted in gutter.
+ . | | | I | | :}
+ | | | I | | :
+ . S [S][ ][I][S][ ]:method H()
+ . S [=][=][-][~][O]: ensures F(1)
+ . S [=][=][-][~][=]:{//Next: { assert false;
+ . S [S][ ][I][S][ ]:}", $"testfile{i}.dfy", diagnosticsReceivers[i], verificationDiagnosticsReceivers[i]));
+ }
+
+ for (var i = 0; i < MaxSimultaneousVerificationTasks; i++) {
+ await result[i];
+ }
+
+ //await Task.WhenAll(result.ToArray());
+ }
+
+}

Source/DafnyLanguageServer.Test/Diagnostics/LinearVerificationDiagnosticTester.cs

@@ -17,16 +17,16 @@
 namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics;
 
 public abstract class LinearVerificationDiagnosticTester : ClientBasedLanguageServerTest {
- protected TestNotificationReceiver<VerificationStatusGutter> VerificationDiagnosticReceiver;
+ protected TestNotificationReceiver<VerificationStatusGutter> verificationDiagnosticsReceiver;
  [TestInitialize]
  public override async Task SetUp() {
- diagnosticReceiver = new();
- VerificationDiagnosticReceiver = new();
+ diagnosticsReceiver = new();
+ verificationDiagnosticsReceiver = new();
  client = await InitializeClient(options =>
  options
- .OnPublishDiagnostics(diagnosticReceiver.NotificationReceived)
+ .OnPublishDiagnostics(diagnosticsReceiver.NotificationReceived)
  .AddHandler(DafnyRequestNames.VerificationStatusGutter,
- NotificationHandler.For<VerificationStatusGutter>(VerificationDiagnosticReceiver.NotificationReceived))
+ NotificationHandler.For<VerificationStatusGutter>(verificationDiagnosticsReceiver.NotificationReceived))
  );
  }
 
@@ -108,7 +108,11 @@ public static string ExtractCode(string tracesAndCode) {
 
  protected List<LineVerificationStatus[]> previousTraces = null;
 
- protected async Task<List<LineVerificationStatus[]>> GetAllLineVerificationDiagnostics(TextDocumentItem documentItem) {
+ protected async Task<List<LineVerificationStatus[]>> GetAllLineVerificationDiagnostics(
+ TextDocumentItem documentItem,
+ DiagnosticsReceiver diagnosticReceiver,
+ TestNotificationReceiver<VerificationStatusGutter> VerificationDiagnosticReceiver
+ ) {
  var traces = new List<LineVerificationStatus[]>();
  var maximumNumberOfTraces = 50;
  var previousPerLineDiagnostics
@@ -117,8 +121,7 @@ var previousPerLineDiagnostics
  var nextDiagnostic = await diagnosticReceiver.AwaitNextNotificationAsync(CancellationToken);
  for (; maximumNumberOfTraces > 0; maximumNumberOfTraces--) {
  var verificationDiagnosticReport = await VerificationDiagnosticReceiver.AwaitNextNotificationAsync(CancellationToken);
- Assert.AreEqual(documentItem.Uri, verificationDiagnosticReport.Uri);
- if (documentItem.Version != verificationDiagnosticReport.Version) {
+ if (documentItem.Uri != verificationDiagnosticReport.Uri || documentItem.Version != verificationDiagnosticReport.Version) {
  continue;
  }
  var newPerLineDiagnostics = verificationDiagnosticReport.PerLineStatus.ToList();
@@ -218,19 +221,26 @@ Position IndexToPosition(int index) {
  return new Tuple<string, List<Tuple<Range, string>>>(originalCode, changes);
  }
 
- public async Task VerifyTrace(string codeAndTrace) {
+ public async Task VerifyTrace(string codeAndTrace, string fileName = null,
+ DiagnosticsReceiver diagnosticsReceiver = null,
+ TestNotificationReceiver<VerificationStatusGutter> verificationDiagnosticsReceiver = null
+ ) {
+ if (diagnosticsReceiver == null || verificationDiagnosticsReceiver == null) {
+ diagnosticsReceiver = this.diagnosticsReceiver;
+ verificationDiagnosticsReceiver = this.verificationDiagnosticsReceiver;
+ }
  codeAndTrace = codeAndTrace[0] == '\n' ? codeAndTrace.Substring(1) :
  codeAndTrace.Substring(0, 2) == "\r\n" ? codeAndTrace.Substring(2) :
  codeAndTrace;
  var codeAndChanges = ExtractCode(codeAndTrace);
  var (code, changes) = ExtractCodeAndChanges(codeAndChanges);
- var documentItem = CreateTestDocument(code);
- await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+ var documentItem = CreateTestDocument(code, fileName);
+ client.OpenDocument(documentItem);
  var traces = new List<LineVerificationStatus[]>();
- traces.AddRange(await GetAllLineVerificationDiagnostics(documentItem));
+ traces.AddRange(await GetAllLineVerificationDiagnostics(documentItem, diagnosticsReceiver, verificationDiagnosticsReceiver));
  foreach (var (range, inserted) in changes) {
  ApplyChange(ref documentItem, range, inserted);
- traces.AddRange(await GetAllLineVerificationDiagnostics(documentItem));
+ traces.AddRange(await GetAllLineVerificationDiagnostics(documentItem, diagnosticsReceiver, verificationDiagnosticsReceiver));
  }
  var traceObtained = RenderTrace(traces, code);
  var ignoreQuestionMarks = AcceptQuestionMarks(traceObtained, codeAndTrace);