Warn when using non doo file as a library (#5313)

### Changes - Warn when passing non-doo files to --library - Lots of code was made asynchronous. These locations are performing IO, so it's good that they're async now. ### How has this been tested? - Updated existing CLI tests <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> --------- Co-authored-by: Robin Salkeld <[email protected]>
dafny-lang · Apr 11, 2024 · 4e586b5 · 4e586b5
1 parent 62a00c7
commit 4e586b5
Show file tree

Hide file tree

Showing 60 changed files with 646 additions and 587 deletions.
diff --git a/Source/DafnyCore.Test/DooFileTest.cs b/Source/DafnyCore.Test/DooFileTest.cs
@@ -7,16 +7,16 @@ namespace DafnyCore.Test;
 
 public class DooFileTest {
   [Fact]
-  public void RoundTripCurrentVersion() {
+  public async Task RoundTripCurrentVersion() {
     var options = DafnyOptions.Default;
     options.ApplyDefaultOptionsWithoutSettingsDefault();
-    var program = ParseProgram("module MyModule { function TheAnswer(): int { 42 } }", options);
+    var program = await ParseProgram("module MyModule { function TheAnswer(): int { 42 } }", options);
     options.ProcessSolverOptions(program.Reporter, Token.Cli);
     var dooFile = new DooFile(program);
 
     var path = Path.GetTempFileName();
     dooFile.Write(path);
-    var loadedDooFile = DooFile.Read(path);
+    var loadedDooFile = await DooFile.Read(path);
 
     Assert.Equal(loadedDooFile.Manifest.DooFileVersion, DooFile.ManifestData.CurrentDooFileVersion);
     Assert.Equal(loadedDooFile.Manifest.DafnyVersion, options.VersionNumber);
@@ -31,12 +31,12 @@ public void UnknownManifestEntries() {
     Assert.Throws<TomlException>(() => DooFile.ManifestData.Read(new StringReader(source)));
   }
 
-  private static Program ParseProgram(string dafnyProgramText, DafnyOptions options) {
+  private static async Task<Program> ParseProgram(string dafnyProgramText, DafnyOptions options) {
     const string fullFilePath = "untitled:foo";
     var rootUri = new Uri(fullFilePath);
     Microsoft.Dafny.Type.ResetScopes();
     var errorReporter = new ConsoleErrorReporter(options);
-    var program = new ProgramParser().Parse(dafnyProgramText, rootUri, errorReporter);
+    var program = await new ProgramParser().Parse(dafnyProgramText, rootUri, errorReporter);
     Assert.Equal(0, errorReporter.ErrorCount);
     return program;
   }

diff --git a/Source/DafnyCore/AST/Grammar/ProgramParser.cs b/Source/DafnyCore/AST/Grammar/ProgramParser.cs
@@ -6,7 +6,7 @@
 using System.Linq;
 using System.Text;
 using System.Threading;
-using DafnyCore;
+using System.Threading.Tasks;
 using Microsoft.Dafny.Compilers;
 using Microsoft.Extensions.Logging;
 using Microsoft.Extensions.Logging.Abstractions;
@@ -32,7 +32,7 @@ public ProgramParser(ILogger<ProgramParser> logger, IFileSystem fileSystem) {
     this.fileSystem = fileSystem;
   }
 
-  public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> files,
+  public virtual async Task<Program> ParseFiles(string programName, IReadOnlyList<DafnyFile> files,
     ErrorReporter errorReporter,
     CancellationToken cancellationToken) {
     var options = errorReporter.Options;
@@ -54,7 +54,7 @@ public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> f
     foreach (var dafnyFile in files) {
       cancellationToken.ThrowIfCancellationRequested();
       if (options.Trace) {
-        options.OutputWriter.WriteLine("Parsing " + dafnyFile.FilePath);
+        await options.OutputWriter.WriteLineAsync("Parsing " + dafnyFile.FilePath);
       }
 
       if (options.XmlSink is { IsOpen: true } && dafnyFile.Uri.IsFile) {
@@ -75,7 +75,7 @@ public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> f
     }
 
     if (!(options.DisallowIncludes || options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate)) {
-      var includedModules = TryParseIncludes(files, defaultModule.Includes.ToList(),
+      var includedModules = await TryParseIncludes(files, defaultModule.Includes.ToList(),
         builtIns, errorReporter, cancellationToken);
 
       foreach (var module in includedModules) {
@@ -205,7 +205,7 @@ public static void MoveModuleContents(ModuleDefinition sourceModule, ModuleDefin
     }
   }
 
-  public IList<DfyParseResult> TryParseIncludes(
+  public async Task<IList<DfyParseResult>> TryParseIncludes(
     IReadOnlyList<DafnyFile> files,
     IEnumerable<Include> roots,
     SystemModuleManager systemModuleManager,
@@ -220,7 +220,7 @@ CancellationToken cancellationToken
     }
 
     foreach (var root in roots) {
-      var dafnyFile = IncludeToDafnyFile(systemModuleManager, errorReporter, root);
+      var dafnyFile = await IncludeToDafnyFile(systemModuleManager, errorReporter, root);
       if (dafnyFile != null) {
         stack.Push(dafnyFile);
       }
@@ -242,7 +242,7 @@ CancellationToken cancellationToken
       result.Add(parseIncludeResult);
 
       foreach (var include in parseIncludeResult.Module.Includes) {
-        var dafnyFile = IncludeToDafnyFile(systemModuleManager, errorReporter, include);
+        var dafnyFile = await IncludeToDafnyFile(systemModuleManager, errorReporter, include);
         if (dafnyFile != null) {
           stack.Push(dafnyFile);
         }
@@ -252,7 +252,7 @@ CancellationToken cancellationToken
     return result;
   }
 
-  private DafnyFile IncludeToDafnyFile(SystemModuleManager systemModuleManager, ErrorReporter errorReporter, Include include) {
+  private Task<DafnyFile> IncludeToDafnyFile(SystemModuleManager systemModuleManager, ErrorReporter errorReporter, Include include) {
     return DafnyFile.CreateAndValidate(errorReporter, fileSystem, systemModuleManager.Options, include.IncludedFilename, include.tok);
   }
 
@@ -307,10 +307,10 @@ private static Parser SetupParser(string s /*!*/, Uri uri /*!*/,
     return new Parser(errorReporter.Options, scanner, errors, cancellationToken);
   }
 
-  public Program Parse(string source, Uri uri, ErrorReporter reporter) {
+  public async Task<Program> Parse(string source, Uri uri, ErrorReporter reporter) {
     var fs = new InMemoryFileSystem(ImmutableDictionary<Uri, string>.Empty.Add(uri, source));
-    var file = DafnyFile.CreateAndValidate(reporter, fs, reporter.Options, uri, Token.NoToken);
+    var file = await DafnyFile.CreateAndValidate(reporter, fs, reporter.Options, uri, Token.NoToken);
     var files = file == null ? Array.Empty<DafnyFile>() : new[] { file };
-    return ParseFiles(uri.ToString(), files, reporter, CancellationToken.None);
+    return await ParseFiles(uri.ToString(), files, reporter, CancellationToken.None);
   }
 }
diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs
@@ -1,9 +1,11 @@
 using System;
 using System.Collections.Generic;
 using System.IO;
+using System.Linq;
 using System.Reflection;
 using System.Reflection.Metadata;
 using System.Reflection.PortableExecutable;
+using System.Threading.Tasks;
 using DafnyCore;
 using JetBrains.Annotations;
 
@@ -29,12 +31,12 @@ public static Uri ExposeInternalUri(string externalName, Uri internalUri) {
     return externalUri;
   }
 
-  public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fileSystem,
+  public static async Task<DafnyFile> CreateAndValidate(ErrorReporter reporter, IFileSystem fileSystem,
     DafnyOptions options, Uri uri, IToken origin, string errorOnNotRecognized = null) {
 
     var embeddedFile = ExternallyVisibleEmbeddedFiles.GetValueOrDefault(uri);
     if (embeddedFile != null) {
-      var result = CreateAndValidate(reporter, fileSystem, options, embeddedFile, origin, errorOnNotRecognized);
+      var result = await CreateAndValidate(reporter, fileSystem, options, embeddedFile, origin, errorOnNotRecognized);
       if (result != null) {
         result.Uri = uri;
       }
@@ -106,15 +108,15 @@ public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fi
           throw new Exception($"Cannot find embedded resource: {resourceName}");
         }
 
-        dooFile = DooFile.Read(stream);
+        dooFile = await DooFile.Read(stream);
       } else {
         if (!fileSystem.Exists(uri)) {
           reporter.Error(MessageSource.Project, origin, $"file {filePathForErrors} not found");
           return null;
         }
 
         try {
-          dooFile = DooFile.Read(filePath);
+          dooFile = await DooFile.Read(filePath);
         } catch (InvalidDataException) {
           reporter.Error(MessageSource.Project, origin, $"malformed doo file {options.GetPrintPath(filePath)}");
           return null;

diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs
@@ -40,36 +40,36 @@ public static void MaybePrintProgram(Program program, string filename, bool afte
     /// <summary>
     /// Returns null on success, or an error string otherwise.
     /// </summary>
-    public static string ParseCheck(TextReader stdIn, IReadOnlyList<DafnyFile /*!*/> /*!*/ files, string /*!*/ programName,
-        DafnyOptions options, out Program program)
+    public static async Task<(Program Program, string Error)> ParseCheck(TextReader stdIn,
+        IReadOnlyList<DafnyFile /*!*/> /*!*/ files, string /*!*/ programName,
+        DafnyOptions options)
     //modifies Bpl.options.XmlSink.*;
     {
-      string err = Parse(files, programName, options, out program);
+      var (program, err) = await Parse(files, programName, options);
       if (err != null) {
-        return err;
+        return (program, err);
       }
 
-      return Resolve(program);
+      return (program, Resolve(program));
     }
 
-    public static string Parse(IReadOnlyList<DafnyFile> files, string programName, DafnyOptions options,
-      out Program program) {
+    public static async Task<(Program Program, string Error)> Parse(IReadOnlyList<DafnyFile> files,
+      string programName, DafnyOptions options) {
       Contract.Requires(programName != null);
       Contract.Requires(files != null);
-      program = null;
 
       ErrorReporter reporter = options.DiagnosticsFormat switch {
         DafnyOptions.DiagnosticsFormats.PlainText => new ConsoleErrorReporter(options),
         DafnyOptions.DiagnosticsFormats.JSON => new JsonConsoleErrorReporter(options),
         _ => throw new ArgumentOutOfRangeException()
       };
 
-      program = new ProgramParser().ParseFiles(programName, files, reporter, CancellationToken.None);
+      var program = await new ProgramParser().ParseFiles(programName, files, reporter, CancellationToken.None);
       var errorCount = program.Reporter.ErrorCount;
       if (errorCount != 0) {
-        return $"{errorCount} parse errors detected in {program.Name}";
+        return (program, $"{errorCount} parse errors detected in {program.Name}");
       }
-      return null;
+      return (program, null);
     }
 
     public static readonly CustomStackSizePoolTaskScheduler LargeThreadScheduler =

diff --git a/Source/DafnyCore/DooFile.cs b/Source/DafnyCore/DooFile.cs
@@ -5,6 +5,7 @@
 using System.IO.Compression;
 using System.Linq;
 using System.Text;
+using System.Threading.Tasks;
 using DafnyCore.Generic;
 using Microsoft.Dafny;
 using Tomlyn;
@@ -69,34 +70,36 @@ public void Write(TextWriter writer) {
   // this must be configured to stay the same.
   private static DafnyOptions ProgramSerializationOptions => DafnyOptions.Default;
 
-  public static DooFile Read(string path) {
+  public static Task<DooFile> Read(string path) {
     using var archive = ZipFile.Open(path, ZipArchiveMode.Read);
     return Read(archive);
   }
 
-  public static DooFile Read(Stream stream) {
+  public static Task<DooFile> Read(Stream stream) {
     using var archive = new ZipArchive(stream);
     return Read(archive);
   }
 
-  private static DooFile Read(ZipArchive archive) {
+  private static async Task<DooFile> Read(ZipArchive archive) {
     var result = new DooFile();
 
     var manifestEntry = archive.GetEntry(ManifestFileEntry);
     if (manifestEntry == null) {
       throw new ArgumentException(".doo file missing manifest entry");
     }
-    using (var manifestStream = manifestEntry.Open()) {
+
+    await using (var manifestStream = manifestEntry.Open()) {
       result.Manifest = ManifestData.Read(new StreamReader(manifestStream, Encoding.UTF8));
     }
 
     var programTextEntry = archive.GetEntry(ProgramFileEntry);
     if (programTextEntry == null) {
       throw new ArgumentException(".doo file missing program text entry");
     }
-    using (var programTextStream = programTextEntry.Open()) {
+
+    await using (var programTextStream = programTextEntry.Open()) {
       var reader = new StreamReader(programTextStream, Encoding.UTF8);
-      result.ProgramText = reader.ReadToEnd();
+      result.ProgramText = await reader.ReadToEndAsync();
     }
 
     return result;

diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs
@@ -72,7 +72,7 @@ public class Compilation : IDisposable {
 
   public ErrorReporter Reporter => errorReporter;
 
-  public IReadOnlyList<DafnyFile>? RootFiles { get; set; }
+  public Task<IReadOnlyList<DafnyFile>> RootFiles { get; set; }
   public bool HasErrors { get; private set; }
 
   public Compilation(
@@ -105,6 +105,7 @@ CompilationInput input
 
     verificationTickets.Enqueue(Unit.Default);
 
+    RootFiles = DetermineRootFiles();
     ParsedProgram = ParseAsync();
     Resolution = ResolveAsync();
   }
@@ -115,9 +116,7 @@ public void Start() {
     }
 
     Project.Errors.CopyDiagnostics(errorReporter);
-    RootFiles = DetermineRootFiles();
 
-    updates.OnNext(new DeterminedRootFiles(Project, RootFiles!, GetDiagnosticsCopyAndClear()));
     started.TrySetResult();
   }
 
@@ -128,19 +127,23 @@ private ImmutableList<FileDiagnostic> GetDiagnosticsCopyAndClear() {
     return result;
   }
 
-  private IReadOnlyList<DafnyFile> DetermineRootFiles() {
+
+
+  private async Task<IReadOnlyList<DafnyFile>> DetermineRootFiles() {
+    await started.Task;
+
     var result = new List<DafnyFile>();
 
     foreach (var uri in Input.Project.GetRootSourceUris(fileSystem)) {
-      var file = DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Project.StartingToken);
+      var file = await DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Project.StartingToken);
       if (file != null) {
         result.Add(file);
       }
     }
 
     foreach (var uri in Options.CliRootSourceUris) {
       var shortPath = Path.GetRelativePath(Directory.GetCurrentDirectory(), uri.LocalPath);
-      var file = DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Token.Cli,
+      var file = await DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Token.Cli,
         $"command-line argument '{shortPath}' is neither a recognized option nor a Dafny input file (.dfy, .doo, or .toml).");
       if (file != null) {
         result.Add(file);
@@ -150,29 +153,46 @@ private IReadOnlyList<DafnyFile> DetermineRootFiles() {
     }
     if (Options.UseStdin) {
       var uri = new Uri("stdin:///");
-      result.Add(DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Token.Cli));
+      result.Add(await DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Token.Cli));
     }
 
     if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
       if (Options.CompilerName is null or "cs" or "java" or "go" or "py" or "js") {
         var targetName = Options.CompilerName ?? "notarget";
         var stdlibDooUri = DafnyMain.StandardLibrariesDooUriTarget[targetName];
-        result.Add(DafnyFile.CreateAndValidate(errorReporter, OnDiskFileSystem.Instance, Options, stdlibDooUri, Project.StartingToken));
+        var targetSpecificFile = await DafnyFile.CreateAndValidate(errorReporter, OnDiskFileSystem.Instance, Options, stdlibDooUri, Project.StartingToken);
+        if (targetSpecificFile != null) {
+          result.Add(targetSpecificFile);
+        }
       }
 
-      result.Add(DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, DafnyMain.StandardLibrariesDooUri, Project.StartingToken));
+      var file = await DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, DafnyMain.StandardLibrariesDooUri, Project.StartingToken);
+      if (file != null) {
+        result.Add(file);
+      }
     }
 
+    string? unverifiedLibrary = null;
     var libraryFiles = CommonOptionBag.SplitOptionValueIntoFiles(Options.Get(CommonOptionBag.Libraries).Select(f => f.FullName));
     foreach (var library in libraryFiles) {
-      var file = DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, new Uri(library), Project.StartingToken);
+      var file = await DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, new Uri(library), Project.StartingToken);
       if (file != null) {
+        if (!file.IsPreverified) {
+          unverifiedLibrary = library;
+        }
         file.IsPreverified = true;
         file.IsPrecompiled = true;
         result.Add(file);
       }
     }
 
+    if (unverifiedLibrary != null) {
+      errorReporter.Warning(MessageSource.Project, "", Project.StartingToken,
+        $"The file '{Options.GetPrintPath(unverifiedLibrary)}' was passed to --library. " +
+        $"Verification for that file might have used options incompatible with the current ones, or might have been skipped entirely. " +
+        $"Use a .doo file to enable Dafny to check that compatible options were used");
+    }
+
     var projectPath = Project.Uri.LocalPath;
     if (projectPath.EndsWith(DafnyProject.FileName)) {
       var projectDirectory = Path.GetDirectoryName(projectPath)!;
@@ -188,12 +208,15 @@ private IReadOnlyList<DafnyFile> DetermineRootFiles() {
     }
 
     // Allow specifying the same file twice on the CLI
-    return result.DistinctBy(d => d.Uri).ToList();
+    var distinctResults = result.DistinctBy(d => d.Uri).ToList();
+
+    updates.OnNext(new DeterminedRootFiles(Project, distinctResults, GetDiagnosticsCopyAndClear()));
+    return distinctResults;
   }
 
   private async Task<Program?> ParseAsync() {
     try {
-      await started.Task;
+      await RootFiles;
       if (HasErrors) {
         return null;
       }