Add --find-project option (#5568)

### Description
- Add `--find-project` option, which allows selecting a project file by
traversing up from a certain path. This is useful when working in a
particular file and wanting to to a Dafny CLI call that uses the project
for that file.

### How has this been tested?
- Extended the existing CLI test `projectFile.dfy`

<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/DafnyFile.cs

@@ -29,7 +29,7 @@ public class DafnyFile {
   private static readonly Dictionary<Uri, Uri> ExternallyVisibleEmbeddedFiles = new();
 
   static DafnyFile() {
-    DooFile.RegisterLibraryCheck(UnsafeDependencies, OptionCompatibility.OptionLibraryImpliesLocalError);
+    DooFile.RegisterLibraryCheck(DoNotVerifyDependencies, OptionCompatibility.OptionLibraryImpliesLocalError);
   }
 
   public static Uri ExposeInternalUri(string externalName, Uri internalUri) {
@@ -108,7 +108,7 @@ public static async IAsyncEnumerable<DafnyFile> CreateAndValidate(IFileSystem fi
     }
   }
 
-  public static readonly Option<bool> UnsafeDependencies = new("--dont-verify-dependencies",
+  public static readonly Option<bool> DoNotVerifyDependencies = new("--dont-verify-dependencies",
     "Allows Dafny to accept dependencies that may not have been previously verified, which can be useful during development.");
 
   public static DafnyFile? HandleDafnyFile(IFileSystem fileSystem,
@@ -141,7 +141,7 @@ public static async IAsyncEnumerable<DafnyFile> CreateAndValidate(IFileSystem fi
       return null;
     }
 
-    if (!options.Get(UnsafeDependencies) && asLibrary && warnLibrary) {
+    if (!options.Get(DoNotVerifyDependencies) && asLibrary && warnLibrary) {
       reporter.Warning(MessageSource.Project, "", origin,
         $"The file '{options.GetPrintPath(filePath)}' was passed to --library. " +
         $"Verification for that file might have used options incompatible with the current ones, or might have been skipped entirely. " +

Source/DafnyCore/Options/DafnyCommands.cs

@@ -107,6 +107,7 @@ static DafnyCommands() {
     CommonOptionBag.WarnMissingConstructorParenthesis,
     PrintStmt.TrackPrintEffectsOption,
     CommonOptionBag.AllowAxioms,
-    MethodOrFunction.AllowExternalContracts
+    MethodOrFunction.AllowExternalContracts,
+    DafnyProject.FindProjectOption
   }).Concat(ParserOptions).ToList();
 }

Source/DafnyCore/Options/DafnyProject.cs

@@ -8,6 +8,7 @@
 using System.Linq;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using DafnyCore;
 using DafnyCore.Options;
 using Microsoft.Extensions.FileSystemGlobbing;
 using Tomlyn;
@@ -16,6 +17,13 @@
 namespace Microsoft.Dafny;
 
 public class DafnyProject : IEquatable<DafnyProject> {
+  public static Option<FileInfo> FindProjectOption = new("--find-project",
+    "Given a filesystem path, search for a project file by traversing up the file tree.");
+
+  static DafnyProject() {
+    DooFile.RegisterNoChecksNeeded(FindProjectOption, false);
+  }
+
   public const string Extension = ".toml";
   public const string FileName = "dfyconfig" + Extension;
 
@@ -48,7 +56,7 @@ public DafnyProject(Uri uri, Uri? @base, ISet<string> includes, ISet<string>? ex
     Options = options ?? new Dictionary<string, object>();
   }
 
-  public static async Task<DafnyProject> Open(IFileSystem fileSystem, DafnyOptions dafnyOptions, Uri uri, IToken uriOrigin,
+  public static async Task<DafnyProject> Open(IFileSystem fileSystem, Uri uri, IToken uriOrigin,
     bool defaultIncludes = true, bool serverNameCheck = true) {
 
     var emptyProject = new DafnyProject(uri, null, new HashSet<string>(), new HashSet<string>(),
@@ -67,7 +75,7 @@ public static async Task<DafnyProject> Open(IFileSystem fileSystem, DafnyOptions
         model.Options ?? new Dictionary<string, object>());
 
       if (result.Base != null) {
-        var baseProject = await Open(fileSystem, dafnyOptions, result.Base, new Token {
+        var baseProject = await Open(fileSystem, result.Base, new Token {
           Uri = uri,
           line = 1,
           col = 1

Source/DafnyCore/Options/ProjectFileOpener.cs

@@ -0,0 +1,48 @@
+#nullable enable
+using System;
+using System.IO;
+using System.Threading.Tasks;
+using Microsoft.Dafny;
+
+public class ProjectFileOpener {
+  private readonly IFileSystem fileSystem;
+  private readonly IToken origin;
+
+  public ProjectFileOpener(IFileSystem fileSystem, IToken origin) {
+    this.fileSystem = fileSystem;
+    this.origin = origin;
+  }
+
+  public async Task<DafnyProject?> TryFindProject(Uri uri) {
+    return uri.LocalPath.EndsWith(DafnyProject.FileName)
+      ? await DafnyProject.Open(fileSystem, uri, origin)
+      : await FindProjectFile(uri);
+  }
+
+  private async Task<DafnyProject?> FindProjectFile(Uri sourceUri) {
+    DafnyProject? projectFile = null;
+
+    var folder = Path.GetDirectoryName(sourceUri.LocalPath);
+    while (!string.IsNullOrEmpty(folder) && projectFile == null) {
+      projectFile = await OpenProjectInFolder(folder);
+
+      if (projectFile != null && projectFile.Uri != sourceUri &&
+          !(projectFile.Errors.HasErrors || projectFile.ContainsSourceFile(sourceUri))) {
+        projectFile = null;
+      }
+
+      folder = Path.GetDirectoryName(folder);
+    }
+
+    return projectFile;
+  }
+
+  protected virtual Task<DafnyProject?> OpenProjectInFolder(string folderPath) {
+    var configFileUri = new Uri(Path.Combine(folderPath, DafnyProject.FileName));
+    if (!fileSystem.Exists(configFileUri)) {
+      return Task.FromResult<DafnyProject?>(null);
+    }
+
+    return DafnyProject.Open(fileSystem, configFileUri, origin)!;
+  }
+}

Source/DafnyDriver/Commands/ResolveCommand.cs

@@ -13,7 +13,7 @@ public static Command Create() {
       result.AddOption(option);
     }
     DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, async (options, _) => {
-      options.Set(DafnyFile.UnsafeDependencies, true);
+      options.Set(DafnyFile.DoNotVerifyDependencies, true);
       var compilation = CliCompilation.Create(options);
       compilation.Start();
       await compilation.Resolution;

Source/DafnyDriver/Commands/ServerCommand.cs

@@ -32,7 +32,7 @@ private static Command Create() {
       result.Add(option);
     }
     DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, async (options, context) => {
-      options.Set(DafnyFile.UnsafeDependencies, true);
+      options.Set(DafnyFile.DoNotVerifyDependencies, true);
       LanguageServer.ConfigureDafnyOptionsForServer(options);
       await LanguageServer.Start(options);
       return 0;

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -42,7 +42,7 @@ public static Command Create() {
     new Option[] {
         FilterSymbol,
         FilterPosition,
-        DafnyFile.UnsafeDependencies
+        DafnyFile.DoNotVerifyDependencies
       }.Concat(DafnyCommands.VerificationOptions).
       Concat(DafnyCommands.ConsoleOutputOptions).
       Concat(DafnyCommands.ResolverOptions);

Source/DafnyDriver/DafnyNewCli.cs

@@ -20,6 +20,7 @@
 using Microsoft.Boogie;
 using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.LanguageServer;
+using Microsoft.Dafny.LanguageServer.Workspace;
 
 namespace Microsoft.Dafny;
 
@@ -108,12 +109,23 @@ async Task Handle(InvocationContext context) {
           }
         }
       }
+
+      ProcessOption(context, DafnyProject.FindProjectOption, dafnyOptions);
+      var findProjectPath = dafnyOptions.Get(DafnyProject.FindProjectOption);
+      if (dafnyOptions.DafnyProject == null && findProjectPath != null) {
+        var opener = new ProjectFileOpener(OnDiskFileSystem.Instance, Token.Cli);
+        var project = await opener.TryFindProject(new Uri(findProjectPath.FullName));
+        project?.Validate(dafnyOptions.OutputWriter, AllOptions);
+        dafnyOptions.DafnyProject = project;
+      }
+
       foreach (var option in command.Options) {
-        if (option == CommonOptionBag.UseBaseFileName) {
+        if (option == CommonOptionBag.UseBaseFileName || option == DafnyProject.FindProjectOption) {
           continue;
         }
         ProcessOption(context, option, dafnyOptions);
       }
+
       foreach (var option in command.Options) {
         try {
           dafnyOptions.ApplyBinding(option);
@@ -219,7 +231,7 @@ private static async Task<bool> ProcessProjectFile(DafnyOptions dafnyOptions, Ur
       await dafnyOptions.ErrorWriter.WriteLineAsync($"Error: file {dafnyOptions.GetPrintPath(file.LocalPath)} not found");
       return false;
     }
-    var projectFile = await DafnyProject.Open(OnDiskFileSystem.Instance, dafnyOptions, file, Token.Cli);
+    var projectFile = await DafnyProject.Open(OnDiskFileSystem.Instance, file, Token.Cli);
 
     projectFile.Validate(dafnyOptions.OutputWriter, AllOptions);
     dafnyOptions.DafnyProject = projectFile;
@@ -271,14 +283,14 @@ private static async IAsyncEnumerable<DafnyFile> HandleDafnyProject(IFileSystem
       yield break;
     }
 
-    var dependencyProject = await DafnyProject.Open(fileSystem, options, uri, uriOrigin);
+    var dependencyProject = await DafnyProject.Open(fileSystem, uri, uriOrigin);
     var dependencyOptions =
       DooFile.CheckAndGetLibraryOptions(reporter, uri, options, uriOrigin, dependencyProject.Options);
     if (dependencyOptions == null) {
       yield break;
     }
 
-    if (options.Get(DafnyFile.UnsafeDependencies) || !options.Verify) {
+    if (options.Get(DafnyFile.DoNotVerifyDependencies) || !options.Verify) {
       foreach (var libraryRootSetFile in dependencyProject.GetRootSourceUris(fileSystem)) {
         var file = DafnyFile.HandleDafnyFile(fileSystem, reporter, dependencyOptions, libraryRootSetFile,
           dependencyProject.StartingToken, true, false);
@@ -301,7 +313,7 @@ private static async IAsyncEnumerable<DafnyFile> HandleDafnyProject(IFileSystem
       dependencyOptions.Compile = true;
       dependencyOptions.RunAfterCompile = false;
       var exitCode = await SynchronousCliCompilation.Run(dependencyOptions);
-      if (exitCode == 0) {
+      if (exitCode == 0 && libraryBackend.DooPath != null) {
         var dooUri = new Uri(libraryBackend.DooPath);
         await foreach (var dooResult in DafnyFile.HandleDooFile(fileSystem, reporter, options, dooUri, uriOrigin, true)) {
           yield return dooResult;

Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs

@@ -105,7 +105,7 @@ public AnonymousDisposable(Action action) {
     private Action<LanguageServerOptions> GetServerOptionsAction(Action<DafnyOptions> modifyOptions) {
       var dafnyOptions = DafnyOptions.CreateUsingOldParser(output);
       dafnyOptions.Set(ProjectManager.UpdateThrottling, 0);
-      dafnyOptions.Set(ProjectManagerDatabase.ProjectFileCacheExpiry, 0);
+      dafnyOptions.Set(CachingProjectFileOpener.ProjectFileCacheExpiry, 0);
       modifyOptions?.Invoke(dafnyOptions);
       dafnyOptions.UsingNewCli = true;
       LanguageServer.ConfigureDafnyOptionsForServer(dafnyOptions);

Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs

@@ -92,7 +92,7 @@ public async Task ProjectFileChangesArePickedUpAfterCacheExpiration() {
     const int cacheExpiry = 1000;
     await SetUp(options => {
       options.WarnShadowing = false;
-      options.Set(ProjectManagerDatabase.ProjectFileCacheExpiry, cacheExpiry);
+      options.Set(CachingProjectFileOpener.ProjectFileCacheExpiry, cacheExpiry);
     });
     var tempDirectory = GetFreshTempPath();
     Directory.CreateDirectory(tempDirectory);

Source/DafnyLanguageServer/LanguageServer.cs

@@ -27,7 +27,7 @@ public class LanguageServer {
         VerifySnapshots,
         DafnyLangSymbolResolver.UseCaching,
         ProjectManager.UpdateThrottling,
-        ProjectManagerDatabase.ProjectFileCacheExpiry,
+        CachingProjectFileOpener.ProjectFileCacheExpiry,
         DeveloperOptionBag.BoogiePrint,
         CommonOptionBag.EnforceDeterminism,
         InternalDocstringRewritersPluginConfiguration.UseJavadocLikeDocstringRewriterOption,

Source/DafnyLanguageServer/Workspace/CachingProjectFileOpener.cs

@@ -0,0 +1,45 @@
+using System;
+using System.CommandLine;
+using System.Runtime.Caching;
+using System.Threading.Tasks;
+using DafnyCore;
+using Microsoft.Dafny;
+
+public class CachingProjectFileOpener : ProjectFileOpener {
+  public const int DefaultProjectFileCacheExpiryTime = 100;
+  private readonly object nullRepresentative = new(); // Needed because you can't store null in the MemoryCache, but that's a value we want to cache.
+  private readonly DafnyOptions serverOptions;
+  private readonly MemoryCache projectFilePerFolderCache = new("projectFiles");
+
+
+  static CachingProjectFileOpener() {
+    DooFile.RegisterNoChecksNeeded(ProjectFileCacheExpiry, false);
+  }
+
+  public CachingProjectFileOpener(IFileSystem fileSystem, DafnyOptions serverOptions, IToken origin) : base(fileSystem, origin) {
+    this.serverOptions = serverOptions;
+  }
+
+  public static readonly Option<int> ProjectFileCacheExpiry = new("--project-file-cache-expiry", () => DefaultProjectFileCacheExpiryTime,
+    @"How many milliseconds the server will cache project file contents".TrimStart()) {
+    IsHidden = true
+  };
+
+  protected override async Task<DafnyProject?> OpenProjectInFolder(string folderPath) {
+    var cacheExpiry = serverOptions.Get(ProjectFileCacheExpiry);
+    if (cacheExpiry == 0) {
+      return await base.OpenProjectInFolder(folderPath);
+    }
+
+    var cachedResult = projectFilePerFolderCache.Get(folderPath);
+    if (cachedResult != null) {
+      return cachedResult == nullRepresentative ? null : ((DafnyProject?)cachedResult)?.Clone();
+    }
+
+    var result = await base.OpenProjectInFolder(folderPath);
+    projectFilePerFolderCache.Set(new CacheItem(folderPath, (object?)result ?? nullRepresentative), new CacheItemPolicy {
+      AbsoluteExpiration = new DateTimeOffset(DateTime.Now.Add(TimeSpan.FromMilliseconds(cacheExpiry)))
+    });
+    return result?.Clone();
+  }
+}