Add project files with includes/excludes and options support

Source/DafnyCore/DafnyCore.csproj

@@ -27,10 +27,12 @@
   <ItemGroup>
       <PackageReference Include="JetBrains.Annotations" Version="2021.1.0" />
       <PackageReference Include="Microsoft.CodeAnalysis.CSharp" Version="3.7.0" />
+      <PackageReference Include="Microsoft.Extensions.FileSystemGlobbing" Version="5.0.0" />
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
       <PackageReference Include="Boogie.ExecutionEngine" Version="2.16.4" />
+      <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 
   <ItemGroup>

Source/DafnyCore/DafnyOptions.cs

@@ -35,7 +35,8 @@ public enum QuantifierSyntaxOptions {
   public record Options(IDictionary<Option, object> OptionArguments);
 
   public class DafnyOptions : Bpl.CommandLineOptions {
-
+    public static DafnyOptions Default = new DafnyOptions();
+    public ProjectFile ProjectFile { get; set; }
     public bool NonGhostsUseHeap => Allocated == 1 || Allocated == 2;
     public bool AlwaysUseHeap => Allocated == 2;
     public bool CommonHeapUse => Allocated >= 2;

Source/DafnyCore/Options/ICommandSpec.cs

@@ -15,7 +15,7 @@ public interface ICommandSpec {
   static ICommandSpec() {
     FilesArgument = new("file", r => {
       return r.Tokens.Where(t => !string.IsNullOrEmpty(t.Value)).Select(t => new FileInfo(t.Value)).ToList();
-    }, true, "input files");
+    }, true, "Dafny input files and/or a Dafny project file");
   }
 
   public static Argument<List<FileInfo>> FilesArgument { get; }

Source/DafnyCore/Options/ProjectFile.cs

@@ -0,0 +1,90 @@
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.CommandLine;
+using System.IO;
+using System.Linq;
+using System.Reflection.Metadata;
+using System.Runtime.Serialization;
+using System.Text.Json;
+using System.Text.RegularExpressions;
+using Microsoft.CodeAnalysis;
+using Microsoft.Extensions.FileSystemGlobbing;
+using Microsoft.Extensions.FileSystemGlobbing.Abstractions;
+using Tomlyn;
+
+namespace Microsoft.Dafny; 
+
+public class ProjectFile {
+  public const string FileName = "dfyconfig.toml";
+
+  [IgnoreDataMember]
+  public Uri Uri { get; set; }
+  public string[] Includes { get; set; }
+  public string[] Excludes { get; set; }
+  public Dictionary<string, object> Options { get; set; }
+
+  public static ProjectFile Open(Uri uri, TextWriter errorWriter) {
+    if (Path.GetFileName(uri.LocalPath) != FileName) {
+      Console.WriteLine($"Warning: only Dafny project files named {FileName} are recognised by the Dafny IDE.");
+    }
+    try {
+      var file = File.Open(uri.LocalPath, FileMode.Open);
+      var model = Toml.ToModel<ProjectFile>(new StreamReader(file).ReadToEnd(), null, new TomlModelOptions());
+      model.Uri = uri;
+      return model;
+
+    } catch (IOException e) {
+      errorWriter.WriteLine(e.Message);
+      return null;
+    } catch (TomlException tomlException) {
+      errorWriter.WriteLine($"The Dafny project file {uri.LocalPath} contains the following errors:");
+      var regex = new Regex(
+        @$"\((\d+),(\d+)\) : error : The property `(\w+)` was not found on object type {typeof(ProjectFile).FullName}");
+      var newMessage = regex.Replace(tomlException.Message,
+        match =>
+          $"({match.Groups[1].Value},{match.Groups[2].Value}): the property {match.Groups[3].Value} does not exist.");
+      errorWriter.WriteLine(newMessage);
+      return null;
+    }
+  }
+
+  public void AddFilesToOptions(DafnyOptions options) {
+    var matcher = new Matcher();
+    foreach (var includeGlob in Includes ?? new[] { "**/*.dfy" }) {
+      matcher.AddInclude(includeGlob);
+    }
+    foreach (var includeGlob in Excludes ?? Enumerable.Empty<string>()) {
+      matcher.AddExclude(includeGlob);
+    }
+
+    var root = Path.GetDirectoryName(Uri.LocalPath);
+    var result = matcher.Execute(new DirectoryInfoWrapper(new DirectoryInfo(root!)));
+    var files = result.Files.Select(f => Path.Combine(root, f.Path));
+    foreach (var file in files) {
+      options.AddFile(file);
+    }
+  }
+
+  public void Validate(IEnumerable<Option> possibleOptions) {
+    var possibleNames = possibleOptions.Select(o => o.Name).ToHashSet();
+    foreach (var optionThatDoesNotExist in Options.Where(option => !possibleNames.Contains(option.Key))) {
+      Console.WriteLine($"Warning: option '{optionThatDoesNotExist.Key}' that was specified in the project file, is not a valid Dafny option.");
+    }
+  }
+
+  public bool TryGetValue(Option option, TextWriter errorWriter, out object value) {
+    if (!Options.TryGetValue(option.Name, out value)) {
+      return false;
+    }
+
+    if (value.GetType() != option.ValueType) {
+      errorWriter.WriteLine(
+        $"Error: property '{option.Name}' is of type '{value.GetType().Name}' but should be of type '{option.ValueType.Name}'");
+      return false;
+    }
+
+    return true;
+
+  }
+}

Source/DafnyDriver/Commands/CommandRegistry.cs

@@ -37,13 +37,13 @@ static CommandRegistry() {
     AddCommand(new TranslateCommand());
     AddCommand(new FormatCommand());
     AddCommand(new MeasureComplexityCommand());
-    AddCommand(new ServerCommand());
+    AddCommand(ServerCommand.Instance);
     AddCommand(new TestCommand());
     AddCommand(new GenerateTestsCommand());
     AddCommand(new DeadCodeCommand());
     AddCommand(new AuditCommand());
 
-    FileArgument = new Argument<FileInfo>("file", "input file");
+    FileArgument = new Argument<FileInfo>("file", "Dafny input file or Dafny project file");
   }
 
   public static Argument<FileInfo> FileArgument { get; }
@@ -60,7 +60,7 @@ public static ParseArgumentResult Create(string[] arguments) {
     dafnyOptions.Environment = "Command-line arguments: " + string.Join(" ", arguments);
     dafnyOptions.Options = options;
 
-    foreach (var option in Commands.SelectMany(c => c.Options)) {
+    foreach (var option in AllOptions) {
       if (!allowHidden) {
         option.IsHidden = false;
       }
@@ -105,24 +105,36 @@ public static ParseArgumentResult Create(string[] arguments) {
       rootCommand.AddCommand(command);
     }
 
+    var failedToProcessFile = false;
     void CommandHandler(InvocationContext context) {
       wasInvoked = true;
       var command = context.ParseResult.CommandResult.Command;
       var commandSpec = commandToSpec[command];
 
       var singleFile = context.ParseResult.GetValueForArgument(FileArgument);
       if (singleFile != null) {
-        dafnyOptions.AddFile(singleFile.FullName);
+        if (!ProcessFile(dafnyOptions, singleFile)) {
+          failedToProcessFile = true;
+          return;
+        }
       }
       var files = context.ParseResult.GetValueForArgument(ICommandSpec.FilesArgument);
       if (files != null) {
         foreach (var file in files) {
-          dafnyOptions.AddFile(file.FullName);
+          if (!ProcessFile(dafnyOptions, file)) {
+            failedToProcessFile = true;
+            return;
+          }
         }
       }
 
       foreach (var option in command.Options) {
-        var value = context.ParseResult.GetValueForOption(option);
+        var result = context.ParseResult.FindResultFor(option);
+        object projectFileValue = null;
+        var hasProjectFileValue = dafnyOptions.ProjectFile?.TryGetValue(option, Console.Error, out projectFileValue) ?? false;
+        var value = result == null && hasProjectFileValue
+          ? projectFileValue
+          : context.ParseResult.GetValueForOption(option);
         options.OptionArguments[option] = value;
         dafnyOptions.ApplyBinding(option);
       }
@@ -137,6 +149,11 @@ void CommandHandler(InvocationContext context) {
 #pragma warning disable VSTHRD002
     var exitCode = builder.Build().InvokeAsync(arguments).Result;
 #pragma warning restore VSTHRD002
+
+    if (failedToProcessFile) {
+      return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR);
+    }
+
     if (!wasInvoked) {
       if (exitCode == 0) {
         return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.OK_EXIT_EARLY);
@@ -151,6 +168,34 @@ void CommandHandler(InvocationContext context) {
     return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR);
   }
 
+  private static bool ProcessFile(DafnyOptions dafnyOptions, FileInfo singleFile) {
+    if (Path.GetExtension(singleFile.FullName) == ".toml") {
+      if (dafnyOptions.ProjectFile != null) {
+        Console.Error.WriteLine($"Only one project file can be used at a time. Both {dafnyOptions.ProjectFile.Uri.LocalPath} and {singleFile.FullName} were specified");
+        return false;
+      }
+
+      if (!File.Exists(singleFile.FullName)) {
+        Console.Error.WriteLine($"Error: file {singleFile.FullName} not found");
+        return false;
+      }
+      var projectFile = ProjectFile.Open(new Uri(singleFile.FullName), Console.Error);
+      if (projectFile == null) {
+        return false;
+      }
+      projectFile.Validate(AllOptions);
+      dafnyOptions.ProjectFile = projectFile;
+      projectFile.AddFilesToOptions(dafnyOptions);
+    } else {
+      dafnyOptions.AddFile(singleFile.FullName);
+    }
+    return true;
+  }
+
+  private static IEnumerable<Option> AllOptions {
+    get { return Commands.SelectMany(c => c.Options); }
+  }
+
   private static CommandLineBuilder AddDeveloperHelp(RootCommand rootCommand, CommandLineBuilder builder) {
     var languageDeveloperHelp = new Option<bool>(ToolchainDebuggingHelpName,
       "Show help and usage information, including options designed for developing the Dafny language and toolchain.");

Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj

@@ -68,6 +68,21 @@
     <None Update="Various\TestFiles\includesAincludesB.dfy">
       <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
     </None>
+    <None Update="ProjectFiles\TestFiles\src\foo.dfy">
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </None>
+    <None Update="ProjectFiles\TestFiles\Nesting\dfyconfig.toml">
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </None>
+    <None Update="ProjectFiles\TestFiles\dfyconfig.toml">
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </None>
+    <None Update="ProjectFiles\TestFiles\noWarnShadowing.dfy">
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </None>
+    <None Update="ProjectFiles\TestFiles\Nesting\src\foo.dfy">
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </None>
   </ItemGroup>
 
   <ItemGroup>

Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs

@@ -84,12 +84,12 @@ void NewServerOptionsAction(LanguageServerOptions options) {
 
     private static void ApplyDefaultOptionValues(DafnyOptions dafnyOptions) {
       var testCommand = new System.CommandLine.Command("test");
-      foreach (var serverOption in new ServerCommand().Options) {
+      foreach (var serverOption in ServerCommand.Instance.Options) {
         testCommand.AddOption(serverOption);
       }
 
       var result = testCommand.Parse("test");
-      foreach (var option in new ServerCommand().Options) {
+      foreach (var option in ServerCommand.Instance.Options) {
         if (!dafnyOptions.Options.OptionArguments.ContainsKey(option)) {
           var value = result.GetValueForOption(option);
 

Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs

@@ -15,7 +15,7 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup {
   public class HoverTest : ClientBasedLanguageServerTest {
     protected override async Task SetUp(Action<DafnyOptions> modifyOptions = null) {
       void ModifyOptions(DafnyOptions options) {
-        options.ProverOptions.Add("-proverOpt:SOLVER=noop");
+        options.ProverOptions.Add("SOLVER=noop");
         modifyOptions?.Invoke(options);
       }
 

Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs

@@ -0,0 +1,33 @@
+using System.IO;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Xunit;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest; 
+
+public class ProjectFilesTest : ClientBasedLanguageServerTest {
+  [Fact]
+  public async Task ClosestProjectFileIsFound() {
+    var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/Nesting/src/foo.dfy");
+    var source = await File.ReadAllTextAsync(filePath);
+    var documentItem = CreateTestDocument(source, filePath);
+    await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+    var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken);
+
+    Assert.Single(diagnostics);
+    Assert.Equal("Shadowed local-variable name: x", diagnostics[0].Message);
+  }
+
+  [Fact]
+  public async Task ProjectFileOverridesOptions() {
+    await SetUp(options => options.WarnShadowing = true);
+    var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/noWarnShadowing.dfy");
+    var source = await File.ReadAllTextAsync(filePath);
+    var documentItem = CreateTestDocument(source, filePath);
+    await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+    var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken);
+
+    Assert.Empty(diagnostics);
+  }
+}

Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/dfyconfig.toml

@@ -0,0 +1,4 @@
+includes = ["src/**/*.dfy"]
+
+[options]
+warn-shadowing = true

Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/src/foo.dfy

@@ -0,0 +1,6 @@
+method Foo() {
+  var x := 3;
+  if (true) {
+    var x := 4;
+  }
+}

Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/dfyconfig.toml

@@ -0,0 +1,4 @@
+includes = ["**/*.dfy"]
+
+[options]
+warn-shadowing = false

Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/noWarnShadowing.dfy

@@ -0,0 +1,6 @@
+method Foo() {
+  var x := 3;
+  if (true) {
+    var x := 4;
+  }
+}

Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs

@@ -53,7 +53,7 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() {
       var source = new CancellationTokenSource();
       parser.Setup(p => p.Parse(It.IsAny<TextDocumentItem>(), It.IsAny<ErrorReporter>(), It.IsAny<CancellationToken>())).Callback(() => source.Cancel())
         .Throws<TaskCanceledException>();
-      var task = textDocumentLoader.LoadAsync(CreateTestDocument(), source.Token);
+      var task = textDocumentLoader.LoadAsync(DafnyOptions.Default, CreateTestDocument(), source.Token);
       try {
         await task;
         Assert.Fail("document load was not cancelled");
@@ -68,7 +68,7 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() {
     public async Task LoadReturnsFaultedTaskIfAnyExceptionOccured() {
       parser.Setup(p => p.Parse(It.IsAny<TextDocumentItem>(), It.IsAny<ErrorReporter>(), It.IsAny<CancellationToken>()))
         .Throws<InvalidOperationException>();
-      var task = textDocumentLoader.LoadAsync(CreateTestDocument(), default);
+      var task = textDocumentLoader.LoadAsync(DafnyOptions.Default, CreateTestDocument(), default);
       try {
         await task;
         Assert.Fail("document load did not fail");

Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs

@@ -123,11 +123,12 @@ public IdeState CreateUnloaded(DocumentTextBuffer textDocument, CancellationToke
       return loader.CreateUnloaded(textDocument, cancellationToken);
     }
 
-    public Task<DocumentAfterParsing> LoadAsync(DocumentTextBuffer textDocument, CancellationToken cancellationToken) {
+    public Task<DocumentAfterParsing> LoadAsync(DafnyOptions options, DocumentTextBuffer textDocument,
+      CancellationToken cancellationToken) {
       if (tests.CrashOnLoad) {
         throw new IOException("crash");
       }
-      return loader.LoadAsync(textDocument, cancellationToken);
+      return loader.LoadAsync(options, textDocument, cancellationToken);
     }
   }
 }

Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs

@@ -99,7 +99,7 @@ private ModuleSymbol ProcessModule(Symbol scope, ModuleDefinition moduleDefiniti
           case DatatypeDecl dataTypeDeclaration:
             return ProcessDataType(moduleSymbol, dataTypeDeclaration);
           default:
-            logger.LogDebug("encountered unknown top level declaration {Name} of type {Type}", topLevelDeclaration.Name, topLevelDeclaration.GetType());
+            logger.LogTrace("encountered unknown top level declaration {Name} of type {Type}", topLevelDeclaration.Name, topLevelDeclaration.GetType());
             return null;
         }
       }
@@ -276,7 +276,7 @@ public void Resolve(Expression bodyExpression) {
       }
 
       public override void VisitUnknown(object node, IToken token) {
-        logger.LogDebug("encountered unknown syntax node of type {NodeType} in {Filename}@({Line},{Column})",
+        logger.LogTrace("encountered unknown syntax node of type {NodeType} in {Filename}@({Line},{Column})",
           node.GetType(), token.GetDocumentFileName(), token.line, token.col);
       }