Changes since last approval

.github/workflows/xunit-tests-reusable.yml

@@ -16,6 +16,7 @@ defaults:
 jobs:
  build:
  runs-on: ${{matrix.os}}
+ timeout-minutes: 60
  name: ${{matrix.suffix}}
  strategy:
  fail-fast: false

.gitignore

@@ -12,6 +12,7 @@
 
 .gradle/
 .idea/
+.vs/
 
 Binaries/*.dll
 Binaries/*.mdb

Source/DafnyCore/AST/Grammar/CustomDirectoryInfoWrapper.cs

@@ -59,7 +59,7 @@ public override IEnumerable<FileSystemInfoBase> EnumerateFileSystemInfos() {
  /// </remarks>
  /// <param name="name">The directory name</param>
  /// <returns>The directory</returns>
- public override DirectoryInfoBase? GetDirectory(string name) {
+ public override DirectoryInfoBase GetDirectory(string name) {
  bool isParentPath = string.Equals(name, "..", StringComparison.Ordinal);
 
  if (isParentPath) {
@@ -102,7 +102,7 @@ public override FileInfoBase GetFile(string name)
  /// <remarks>
  /// Equals the value of <seealso cref="System.IO.DirectoryInfo.Parent" />.
  /// </remarks>
- public override DirectoryInfoBase? ParentDirectory
+ public override DirectoryInfoBase ParentDirectory
  => new CustomDirectoryInfoWrapper(_directoryInfo.Parent!);
  }
 }

Source/DafnyCore/AST/Types/Types.cs

@@ -19,7 +19,7 @@ public abstract class Type : TokenNode {
  public static Type String() { return new UserDefinedType(Token.NoToken, "string", null); } // note, this returns an unresolved type
  public static readonly BigOrdinalType BigOrdinal = new BigOrdinalType();
 
- private static AsyncLocal<List<VisibilityScope>> _scopes = new();
+ private static ThreadLocal<List<VisibilityScope>> _scopes = new();
  private static List<VisibilityScope> Scopes => _scopes.Value ??= new();
 
  [ThreadStatic]

Source/DafnyCore/Options/DafnyProject.cs

@@ -6,6 +6,7 @@
 using System.Linq;
 using System.Runtime.Serialization;
 using System.Text.RegularExpressions;
+using System.Threading.Tasks;
 using DafnyCore.Options;
 using Microsoft.Extensions.FileSystemGlobbing;
 using Tomlyn;
@@ -26,12 +27,13 @@ public class DafnyProject : IEquatable<DafnyProject> {
  public string[] Excludes { get; set; }
  public Dictionary<string, object> Options { get; set; }
 
- public static DafnyProject Open(IFileSystem fileSystem, Uri uri, TextWriter outputWriter, TextWriter errorWriter) {
+ public static async Task<DafnyProject> Open(IFileSystem fileSystem, Uri uri, TextWriter outputWriter, TextWriter errorWriter) {
  if (Path.GetFileName(uri.LocalPath) != FileName) {
  outputWriter.WriteLine($"Warning: only Dafny project files named {FileName} are recognised by the Dafny IDE.");
  }
  try {
- var model = Toml.ToModel<DafnyProject>(fileSystem.ReadFile(uri).ReadToEnd(), null, new TomlModelOptions());
+ var text = await fileSystem.ReadFile(uri).ReadToEndAsync();
+ var model = Toml.ToModel<DafnyProject>(text, null, new TomlModelOptions());
  model.Uri = uri;
  return model;
 

Source/DafnyDriver/Commands/CommandRegistry.cs

@@ -11,6 +11,7 @@
 using System.IO;
 using System.Linq;
 using System.Reflection;
+using System.Threading.Tasks;
 using DafnyCore;
 using JetBrains.Annotations;
 using Microsoft.Boogie;
@@ -140,23 +141,23 @@ public static ParseArgumentResult Create(TextWriter outputWriter, TextWriter err
  }
 
  var errorOccurred = false;
- void CommandHandler(InvocationContext context) {
+ async Task CommandHandler(InvocationContext context) {
  wasInvoked = true;
  var command = context.ParseResult.CommandResult.Command;
  var commandSpec = commandToSpec[command];
  dafnyOptions.Command = command;
 
  var singleFile = context.ParseResult.GetValueForArgument(FileArgument);
  if (singleFile != null) {
- if (!ProcessFile(dafnyOptions, singleFile)) {
+ if (!await ProcessFile(dafnyOptions, singleFile)) {
  errorOccurred = true;
  return;
  }
  }
  var files = context.ParseResult.GetValueForArgument(ICommandSpec.FilesArgument);
  if (files != null) {
  foreach (var file in files) {
- if (!ProcessFile(dafnyOptions, file)) {
+ if (!await ProcessFile(dafnyOptions, file)) {
  errorOccurred = true;
  return;
  }
@@ -247,21 +248,21 @@ private static object GetValueForOption(ParseResult result, Option option) {
  return generic.Invoke(result, new object[] { option });
  }
 
- private static bool ProcessFile(DafnyOptions dafnyOptions, FileInfo singleFile) {
+ private static async Task<bool> ProcessFile(DafnyOptions dafnyOptions, FileInfo singleFile) {
  var filePathForErrors = dafnyOptions.UseBaseNameForFileName
  ? Path.GetFileName(singleFile.FullName)
  : singleFile.FullName;
  if (Path.GetExtension(singleFile.FullName) == ".toml") {
  if (dafnyOptions.DafnyProject != null) {
- dafnyOptions.ErrorWriter.WriteLine($"Only one project file can be used at a time. Both {dafnyOptions.DafnyProject.Uri.LocalPath} and {filePathForErrors} were specified");
+ await dafnyOptions.ErrorWriter.WriteLineAsync($"Only one project file can be used at a time. Both {dafnyOptions.DafnyProject.Uri.LocalPath} and {filePathForErrors} were specified");
  return false;
  }
 
  if (!File.Exists(singleFile.FullName)) {
- dafnyOptions.ErrorWriter.WriteLine($"Error: file {filePathForErrors} not found");
+ await dafnyOptions.ErrorWriter.WriteLineAsync($"Error: file {filePathForErrors} not found");
  return false;
  }
- var projectFile = DafnyProject.Open(OnDiskFileSystem.Instance, new Uri(singleFile.FullName), dafnyOptions.OutputWriter, dafnyOptions.ErrorWriter);
+ var projectFile = await DafnyProject.Open(OnDiskFileSystem.Instance, new Uri(singleFile.FullName), dafnyOptions.OutputWriter, dafnyOptions.ErrorWriter);
  if (projectFile == null) {
  return false;
  }

Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs

@@ -129,6 +129,8 @@ protected virtual ILanguageClient CreateClient(
  );
 
  Disposable.Add(client);
+ Disposable.Add(Server);
+ Disposable.Add((IDisposable)Server.Services); // Testing shows that the services are not disposed automatically when the server is disposed.
 
  return client;
  }
@@ -152,8 +154,6 @@ protected virtual ILanguageClient CreateClient(
  Server.Initialize(CancellationToken);
 #pragma warning restore VSTHRD110 // Observe result of async calls
 
- Disposable.Add(Server);
- Disposable.Add((IDisposable)Server.Services); // Testing shows that the services are not disposed automatically when the server is disposed.
  return (clientPipe.Reader.AsStream(), serverPipe.Writer.AsStream());
  }
 

Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs

@@ -26,7 +26,7 @@ public async Task ExplicitProjectToGoDefinitionWorks() {
 ".TrimStart();
 
  var directory = Path.GetRandomFileName();
- await CreateAndOpenTestDocument("", Path.Combine(directory, "dfyconfig.toml"));
+ await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName));
  var aFile = await CreateAndOpenTestDocument(sourceA, Path.Combine(directory, "A.dfy"));
  var bFile = await CreateAndOpenTestDocument(sourceB, Path.Combine(directory, "B.dfy"));
 

Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesTest.cs

@@ -40,7 +40,7 @@ method Produces() {}
  var producesDefinition1 = await RequestDefinition(consumer, new Position(1, 3));
  Assert.Empty(producesDefinition1);
 
- await File.WriteAllTextAsync(Path.Combine(directory, "dfyconfig.toml"), "includes = [\"*.dfy\"]");
+ await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), "includes = [\"*.dfy\"]");
  await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime);
 
  var producesDefinition2 = await RequestDefinition(consumer, new Position(1, 3));
@@ -66,7 +66,7 @@ method Produces() {}
  var producesDefinition1 = await RequestDefinition(consumer, new Position(1, 3));
  Assert.Empty(producesDefinition1);
 
- await CreateAndOpenTestDocument("", Path.Combine(directory, "dfyconfig.toml"));
+ await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName));
 
  await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime);
 
@@ -81,7 +81,7 @@ await SetUp(options => {
  });
 
  var directory = Path.GetRandomFileName();
- var projectFile = await CreateAndOpenTestDocument("", Path.Combine(directory, "dfyconfig.toml"));
+ var projectFile = await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName));
  var codeFile = await CreateAndOpenTestDocument("method Foo() {}", Path.Combine(directory, "firstFile.dfy"));
 
  Assert.NotEmpty(Projects.Managers);
@@ -116,15 +116,15 @@ method Produces() {}
 
  var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
  Directory.CreateDirectory(directory);
- await File.WriteAllTextAsync(Path.Combine(directory, "dfyconfig.toml"), projectFileSource);
+ await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), projectFileSource);
 
  var consumer = await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "firstFile.dfy"));
  var secondFile = await CreateAndOpenTestDocument(producer, Path.Combine(directory, "secondFile.dfy"));
 
  var producesDefinition1 = await RequestDefinition(consumer, new Position(1, 3));
  Assert.Empty(producesDefinition1);
 
- await File.WriteAllTextAsync(Path.Combine(directory, "dfyconfig.toml"),
+ await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName),
  @"includes = [""firstFile.dfy"", ""secondFile.dfy""]");
  await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime);
 
@@ -155,15 +155,15 @@ method Foo() {
 warn-shadowing = true
 "; // includes must come before [options], even if there is a blank line
  var directory = Path.GetRandomFileName();
- var projectFile = await CreateAndOpenTestDocument(projectFileSource, Path.Combine(directory, "dfyconfig.toml"));
+ var projectFile = await CreateAndOpenTestDocument(projectFileSource, Path.Combine(directory, DafnyProject.FileName));
  var sourceFile = await CreateAndOpenTestDocument(source, Path.Combine(directory, "src/file.dfy"));
 
  var diagnostics1 = await GetLastDiagnostics(sourceFile, CancellationToken);
  Assert.Equal(2, diagnostics1.Length);
  Assert.Contains(diagnostics1, s => s.Message.Contains("Shadowed"));
 
- ApplyChange(ref projectFile, new Range(1, 17, 1, 21), "false");
  await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime);
+ ApplyChange(ref projectFile, new Range(1, 17, 1, 21), "false");
 
  var resolutionDiagnostics2 = await diagnosticsReceiver.AwaitNextWarningOrErrorDiagnosticsAsync(CancellationToken);
  // The shadowed warning is no longer produced, and the verification error is not migrated. 
@@ -186,8 +186,8 @@ method Bar() {
  var projectFileSource = @"
 includes = [""src/**/*.dfy""]
 ";
- var directory = Directory.GetCurrentDirectory();
- var projectFile = await CreateAndOpenTestDocument(projectFileSource, Path.Combine(directory, "dfyconfig.toml"));
+ var directory = Path.GetRandomFileName();
+ var projectFile = await CreateAndOpenTestDocument(projectFileSource, Path.Combine(directory, DafnyProject.FileName));
  var producerItem = await CreateAndOpenTestDocument(producerSource, Path.Combine(directory, "src/producer.dfy"));
  var consumer = await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "src/consumer1.dfy"));
 

Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs

@@ -27,12 +27,14 @@ method Foo() {
  }
 }
 ";
- var documentItem = CreateTestDocument(source, Path.Combine(projectFilePath, "source.dfy"));
+ var documentItem = CreateTestDocument(source, Path.Combine(tempDirectory, "source.dfy"));
  await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
 
  var warnShadowingOn = @"
 [options]
 warn-shadowing = true";
+ // Wait to prevent an IOException because the file is already in use.
+ await Task.Delay(100);
  await File.WriteAllTextAsync(projectFilePath, warnShadowingOn);
  await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime);
  ApplyChange(ref documentItem, new Range(0, 0, 0, 0), "//touch comment\n");

Source/DafnyLanguageServer.Test/Synchronization/GhostDiagnosticsTest.cs

@@ -31,7 +31,7 @@ await SetUp(options => {
  });
 
  var directory = Path.GetRandomFileName();
- var projectFile = await CreateAndOpenTestDocument("", Path.Combine(directory, "dfyconfig.toml"));
+ var projectFile = await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName));
  var docA = await CreateAndOpenTestDocument(sourceA, Path.Combine(directory, "a.dfy"));
  var docB = await CreateAndOpenTestDocument(sourceB, Path.Combine(directory, "b.dfy"));
 

Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs

@@ -48,6 +48,18 @@ method Test() {
  Assert.Single(document.GetDiagnostics(documentItem.Uri.ToUri()));
  }
 
+ [Fact]
+ public async Task NonErrorDiagnosticDoesNotProduceAnError() {
+ var source = @"
+include ""./hasWarning.dfy""
+".TrimStart();
+ var warningSource = "const tooManySemiColons := 3;";
+ await CreateAndOpenTestDocument(warningSource, Path.Combine(TestFileDirectory, "hasWarning.dfy"));
+ await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken);
+ await CreateAndOpenTestDocument(source, TestFilePath);
+ await AssertNoDiagnosticsAreComing(CancellationToken);
+ }
+
  [Fact]
  public async Task DirectlyIncludedFileFails() {
  var source = @"

Source/DafnyLanguageServer.Test/Synchronization/VerificationOrder.cs

@@ -30,7 +30,7 @@ method Bar() {
 ".TrimStart();
 
  var directory = Path.GetRandomFileName();
- var projectFile = await CreateAndOpenTestDocument("", Path.Combine(directory, "dfyconfig.toml"));
+ var projectFile = await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName));
  var firstFile = await CreateAndOpenTestDocument(sourceA, Path.Combine(directory, "firstFile.dfy"));
  var secondFile = await CreateAndOpenTestDocument(sourceB, Path.Combine(directory, "secondFile.dfy"));
 

Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs

@@ -166,7 +166,7 @@ decreases y
 }".TrimStart();
  var loadingDocuments = new List<TextDocumentItem>();
  for (int i = 0; i < documentsToLoadConcurrently; i++) {
- var documentItem = CreateTestDocument(source, $"test_{i}.dfy");
+ var documentItem = CreateTestDocument(source, $"current_test_{i}.dfy");
  client.OpenDocument(documentItem);
  loadingDocuments.Add(documentItem);
  }

Source/DafnyLanguageServer/Handlers/DafnyTextDocumentHandler.cs

@@ -69,6 +69,9 @@ public override Task<Unit> Handle(DidOpenTextDocumentParams notification, Cancel
  return Unit.Task;
  }
 
+ /// <summary>
+ /// Can be called in parallel
+ /// </summary>
  public override async Task<Unit> Handle(DidCloseTextDocumentParams notification, CancellationToken cancellationToken) {
  logger.LogTrace("received close notification {DocumentUri}", notification.TextDocument.Uri);
  try {

Source/DafnyLanguageServer/Language/DafnyLangParser.cs

@@ -1,5 +1,7 @@
 using Microsoft.Extensions.Logging;
 using System;
+using System.Collections.Generic;
+using System.IO;
 using System.Linq;
 using System.Threading;
 using Microsoft.Dafny.LanguageServer.Workspace;
@@ -13,7 +15,7 @@ namespace Microsoft.Dafny.LanguageServer.Language {
  /// dafny-lang makes use of static members and assembly loading. Since thread-safety of this is not guaranteed,
  /// this parser serializes all invocations.
  /// </remarks>
- public sealed class DafnyLangParser : IDafnyParser, IDisposable {
+ public sealed class DafnyLangParser : IDafnyParser {
  private readonly DafnyOptions options;
  private readonly IFileSystem fileSystem;
  private readonly ITelemetryPublisher telemetryPublisher;
@@ -38,18 +40,21 @@ public static DafnyLangParser Create(DafnyOptions options, IFileSystem fileSyste
  return new DafnyLangParser(options, fileSystem, telemetryPublisher, loggerFactory);
  }
 
- public Program Parse(DafnyProject project, ErrorReporter reporter,
- CancellationToken cancellationToken) {
+ public Program Parse(DafnyProject project, ErrorReporter reporter, CancellationToken cancellationToken) {
  mutex.Wait(cancellationToken);
 
  var beforeParsing = DateTime.Now;
  try {
  var rootSourceUris = project.GetRootSourceUris(fileSystem, options).Concat(options.CliRootSourceUris);
- var result = cachingParser.ParseFiles(project.ProjectName,
- rootSourceUris.Select(uri =>
- new DafnyFile(reporter.Options, uri, fileSystem.ReadFile(uri))
- ).ToList(),
- reporter, cancellationToken);
+ List<DafnyFile> dafnyFiles = new();
+ foreach (var rootSourceUri in rootSourceUris) {
+ try {
+ dafnyFiles.Add(new DafnyFile(reporter.Options, rootSourceUri, fileSystem.ReadFile(rootSourceUri)));
+ } catch (FileNotFoundException e) {
+ logger.LogError($"Tried to parse file {rootSourceUri} that could not be found");
+ }
+ }
+ var result = cachingParser.ParseFiles(project.ProjectName, dafnyFiles, reporter, cancellationToken);
  cachingParser.Prune();
  return result;
  }
@@ -58,9 +63,5 @@ public Program Parse(DafnyProject project, ErrorReporter reporter,
  mutex.Release();
  }
  }
-
- public void Dispose() {
- mutex.Dispose();
- }
  }
 }