diff --git a/Source/DafnyCore.Test/DooFileTest.cs b/Source/DafnyCore.Test/DooFileTest.cs index 00f43718901..904e2960d96 100644 --- 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(() => DooFile.ManifestData.Read(new StringReader(source))); } - private static Program ParseProgram(string dafnyProgramText, DafnyOptions options) { + private static async Task 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 index 606de13113d..0e892ca2f89 100644 --- 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 logger, IFileSystem fileSystem) { this.fileSystem = fileSystem; } - public virtual Program ParseFiles(string programName, IReadOnlyList files, + public virtual async Task ParseFiles(string programName, IReadOnlyList files, ErrorReporter errorReporter, CancellationToken cancellationToken) { var options = errorReporter.Options; @@ -54,7 +54,7 @@ public virtual Program ParseFiles(string programName, IReadOnlyList 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 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 TryParseIncludes( + public async Task> TryParseIncludes( IReadOnlyList files, IEnumerable 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 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 Parse(string source, Uri uri, ErrorReporter reporter) { var fs = new InMemoryFileSystem(ImmutableDictionary.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() : 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 index 41c0c9c4f76..b4b934a8c92 100644 --- 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 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,7 +108,7 @@ 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"); @@ -114,7 +116,7 @@ public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fi } 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 index bcbb1a0707d..a8d6c82a369 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -40,23 +40,23 @@ public static void MaybePrintProgram(Program program, string filename, bool afte /// /// Returns null on success, or an error string otherwise. /// - public static string ParseCheck(TextReader stdIn, IReadOnlyList /*!*/ files, string /*!*/ programName, - DafnyOptions options, out Program program) + public static async Task<(Program Program, string Error)> ParseCheck(TextReader stdIn, + IReadOnlyList /*!*/ 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 files, string programName, DafnyOptions options, - out Program program) { + public static async Task<(Program Program, string Error)> Parse(IReadOnlyList 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), @@ -64,12 +64,12 @@ public static string Parse(IReadOnlyList files, string programName, D _ => 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 index 71815f08d36..4922cde1cfc 100644 --- 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,24 +70,25 @@ 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 Read(string path) { using var archive = ZipFile.Open(path, ZipArchiveMode.Read); return Read(archive); } - public static DooFile Read(Stream stream) { + public static Task Read(Stream stream) { using var archive = new ZipArchive(stream); return Read(archive); } - private static DooFile Read(ZipArchive archive) { + private static async Task 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)); } @@ -94,9 +96,10 @@ private static DooFile Read(ZipArchive archive) { 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 index 4b9da9ca5e3..778d93c04cb 100644 --- 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? RootFiles { get; set; } + public Task> 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,11 +127,15 @@ private ImmutableList GetDiagnosticsCopyAndClear() { return result; } - private IReadOnlyList DetermineRootFiles() { + + + private async Task> DetermineRootFiles() { + await started.Task; + var result = new List(); 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); } @@ -140,7 +143,7 @@ private IReadOnlyList DetermineRootFiles() { 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 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 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 ParseAsync() { try { - await started.Task; + await RootFiles; if (HasErrors) { return null; } diff --git a/Source/DafnyCore/Pipeline/IDafnyParser.cs b/Source/DafnyCore/Pipeline/IDafnyParser.cs index 6ce4dfd5052..5258a1bb582 100644 --- a/Source/DafnyCore/Pipeline/IDafnyParser.cs +++ b/Source/DafnyCore/Pipeline/IDafnyParser.cs @@ -1,4 +1,5 @@ using System.Threading; +using System.Threading.Tasks; namespace Microsoft.Dafny { /// @@ -8,6 +9,6 @@ namespace Microsoft.Dafny { /// Any implementation has to guarantee thread-safety of its public members. /// public interface IDafnyParser { - Program Parse(Compilation compilation, CancellationToken cancellationToken); + Task Parse(Compilation compilation, CancellationToken cancellationToken); } } diff --git a/Source/DafnyCore/Pipeline/TextDocumentLoader.cs b/Source/DafnyCore/Pipeline/TextDocumentLoader.cs index a84cd1c379f..65b3f3ea5bd 100644 --- a/Source/DafnyCore/Pipeline/TextDocumentLoader.cs +++ b/Source/DafnyCore/Pipeline/TextDocumentLoader.cs @@ -31,7 +31,7 @@ public TextDocumentLoader( public async Task ParseAsync(Compilation compilation, CancellationToken cancellationToken) { #pragma warning disable CS1998 return await await DafnyMain.LargeStackFactory.StartNew( - async () => parser.Parse(compilation, cancellationToken), cancellationToken + () => parser.Parse(compilation, cancellationToken), cancellationToken #pragma warning restore CS1998 ); } diff --git a/Source/DafnyCore/Snippets.cs b/Source/DafnyCore/Snippets.cs index 67dfd460eb7..61a37afa9c5 100644 --- a/Source/DafnyCore/Snippets.cs +++ b/Source/DafnyCore/Snippets.cs @@ -47,7 +47,9 @@ private static string GetFileLine(DafnyOptions options, Uri uri, int lineIndex) try { // Note: This is not guaranteed to be the same file that Dafny parsed. To ensure that, Dafny should keep // an in-memory version of each file it parses. - var file = DafnyFile.CreateAndValidate(new ErrorReporterSink(options), OnDiskFileSystem.Instance, options, uri, Token.NoToken); +#pragma warning disable VSTHRD002 + var file = DafnyFile.CreateAndValidate(new ErrorReporterSink(options), OnDiskFileSystem.Instance, options, uri, Token.NoToken).Result; +#pragma warning restore VSTHRD002 using var reader = file.GetContent(); lines = Util.Lines(reader).ToList(); } catch (Exception) { diff --git a/Source/DafnyDriver/Commands/CoverageReportCommand.cs b/Source/DafnyDriver/Commands/CoverageReportCommand.cs index 3130b779387..a748d1b583f 100644 --- a/Source/DafnyDriver/Commands/CoverageReportCommand.cs +++ b/Source/DafnyDriver/Commands/CoverageReportCommand.cs @@ -43,11 +43,11 @@ public static Command Create() { result.AddOption(option); } - DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => { + DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, async (options, _) => { var coverageReporter = new CoverageReporter(options); - coverageReporter.Merge(options.Get(ReportsArgument).ConvertAll(fileInfo => fileInfo.FullName), + await coverageReporter.Merge(options.Get(ReportsArgument).ConvertAll(fileInfo => fileInfo.FullName), options.Get(OutDirArgument)); - return Task.FromResult(0); + return 0; }); return result; } diff --git a/Source/DafnyDriver/Commands/FormatCommand.cs b/Source/DafnyDriver/Commands/FormatCommand.cs index b6fe9bf4dbb..861bc6b7f3f 100644 --- a/Source/DafnyDriver/Commands/FormatCommand.cs +++ b/Source/DafnyDriver/Commands/FormatCommand.cs @@ -1,7 +1,6 @@ using System; using System.Collections.Generic; using System.CommandLine; -using System.CommandLine.Invocation; using System.Diagnostics.Contracts; using System.IO; using System.Linq; @@ -33,7 +32,7 @@ public static Command Create() { } public static async Task DoFormatting(DafnyOptions options) { - var code = SynchronousCliCompilation.GetDafnyFiles(options, out var dafnyFiles, out _); + var (code, dafnyFiles, _) = await SynchronousCliCompilation.GetDafnyFiles(options); if (code != 0) { return code; } @@ -43,7 +42,8 @@ public static async Task DoFormatting(DafnyOptions options) { var exitValue = ExitValue.SUCCESS; Contract.Assert(dafnyFiles.Count > 0 || options.SourceFolders.Count > 0); - dafnyFiles = dafnyFiles.Concat(options.SourceFolders.SelectMany(folderPath => GetFilesForFolder(options, folderPath))).ToList(); + var folderFiles = (await Task.WhenAll(options.SourceFolders.Select(folderPath => GetFilesForFolder(options, folderPath)))).SelectMany(x => x); + dafnyFiles = dafnyFiles.Concat(folderFiles).ToList(); var failedToParseFiles = new List(); var emptyFiles = new List(); @@ -68,7 +68,7 @@ public static async Task DoFormatting(DafnyOptions options) { if (dafnyFile.Uri.Scheme == "stdin") { tempFileName = Path.GetTempFileName() + ".dfy"; SynchronousCliCompilation.WriteFile(tempFileName, await Console.In.ReadToEndAsync()); - dafnyFile = DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), + dafnyFile = await DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), OnDiskFileSystem.Instance, options, new Uri(tempFileName), Token.NoToken); } @@ -77,7 +77,7 @@ public static async Task DoFormatting(DafnyOptions options) { content.Close(); // Manual closing because we want to overwrite dafnyFile.GetContent = () => new StringReader(originalText); // Might not be totally optimized but let's do that for now - var err = DafnyMain.Parse(new List { dafnyFile }, programName, options, out var dafnyProgram); + var (dafnyProgram, err) = await DafnyMain.Parse(new List { dafnyFile }, programName, options); if (err != null) { exitValue = ExitValue.DAFNY_ERROR; await errorWriter.WriteLineAsync(err); @@ -151,9 +151,9 @@ await options.OutputWriter.WriteLineAsync(neededFormatting > 0 return exitValue; } - public static IEnumerable GetFilesForFolder(DafnyOptions options, string folderPath) { - return Directory.GetFiles(folderPath, "*.dfy", SearchOption.AllDirectories) + public static Task GetFilesForFolder(DafnyOptions options, string folderPath) { + return Task.WhenAll(Directory.GetFiles(folderPath, "*.dfy", SearchOption.AllDirectories) .Select(name => DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), OnDiskFileSystem.Instance, - options, new Uri(name), Token.Cli)); + options, new Uri(name), Token.Cli))); } } diff --git a/Source/DafnyDriver/Commands/GenerateTestsCommand.cs b/Source/DafnyDriver/Commands/GenerateTestsCommand.cs index 0bf84a0b2c8..16ca047fa0d 100644 --- a/Source/DafnyDriver/Commands/GenerateTestsCommand.cs +++ b/Source/DafnyDriver/Commands/GenerateTestsCommand.cs @@ -73,7 +73,7 @@ public static Command Create() { } public static async Task GenerateTests(DafnyOptions options) { - var exitValue = SynchronousCliCompilation.GetDafnyFiles(options, out var dafnyFiles, out _); + var (exitValue, dafnyFiles, _) = await SynchronousCliCompilation.GetDafnyFiles(options); if (exitValue != ExitValue.SUCCESS) { return exitValue; } @@ -100,7 +100,7 @@ await options.OutputWriter.WriteLineAsync( } } if (options.TestGenOptions.CoverageReport != null) { - new CoverageReporter(options).SerializeCoverageReports(coverageReport, options.TestGenOptions.CoverageReport); + await new CoverageReporter(options).SerializeCoverageReports(coverageReport, options.TestGenOptions.CoverageReport); } if (TestGenerator.SetNonZeroExitCode) { exitValue = ExitValue.DAFNY_ERROR; diff --git a/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs b/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs index 3eb79d2a6e2..089225af908 100644 --- a/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs +++ b/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs @@ -63,12 +63,13 @@ private static async Task Execute(DafnyOptions options) { // Performance data of individual verification tasks (VCs) should be grouped by VcNum (the assertion batch). VerifyCommand.ReportVerificationDiagnostics(compilation, verificationResults); var summaryReported = VerifyCommand.ReportVerificationSummary(compilation, verificationResults); - VerifyCommand.ReportProofDependencies(compilation, resolution, verificationResults); + var proofDependenciesReported = VerifyCommand.ReportProofDependencies(compilation, resolution, verificationResults); var verificationResultsLogged = VerifyCommand.LogVerificationResults(compilation, resolution, verificationResults); await RunVerificationIterations(options, compilation, verificationResults); await summaryReported; await verificationResultsLogged; + await proofDependenciesReported; } return await compilation.GetAndReportExitCode(); diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs index d1270ebc7ab..4a0b2a9bcd2 100644 --- a/Source/DafnyDriver/Commands/VerifyCommand.cs +++ b/Source/DafnyDriver/Commands/VerifyCommand.cs @@ -2,11 +2,8 @@ using System; using System.Collections.Generic; using System.CommandLine; -using System.IO; using System.Linq; -using System.Reactive.Disposables; using System.Reactive.Subjects; -using System.Reactive.Threading.Tasks; using System.Threading; using System.Threading.Tasks; using DafnyCore; @@ -62,11 +59,12 @@ public static async Task HandleVerification(DafnyOptions options) { ReportVerificationDiagnostics(compilation, verificationResults); var verificationSummarized = ReportVerificationSummary(compilation, verificationResults); - ReportProofDependencies(compilation, resolution, verificationResults); + var proofDependenciesReported = ReportProofDependencies(compilation, resolution, verificationResults); var verificationResultsLogged = LogVerificationResults(compilation, resolution, verificationResults); compilation.VerifyAllLazily(0).ToObservable().Subscribe(verificationResults); await verificationSummarized; await verificationResultsLogged; + await proofDependenciesReported; } return await compilation.GetAndReportExitCode(); @@ -196,7 +194,7 @@ public static async Task LogVerificationResults(CliCompilation cliCompilation, R } } - public static void ReportProofDependencies( + public static async Task ReportProofDependencies( CliCompilation cliCompilation, ResolutionResult resolution, IObservable verificationResults) { @@ -210,16 +208,14 @@ public static void ReportProofDependencies( foreach (var used in result.Results.SelectMany(part => part.Result.CoveredElements)) { usedDependencies.Add(used); } - }, - e => { }, - () => { - var coverageReportDir = cliCompilation.Options.Get(CommonOptionBag.VerificationCoverageReport); - if (coverageReportDir != null) { - new CoverageReporter(cliCompilation.Options).SerializeVerificationCoverageReport( - proofDependencyManager, resolution.ResolvedProgram, - usedDependencies, - coverageReportDir); - } - }); + }, e => { }, () => { }); + await verificationResults.WaitForComplete(); + var coverageReportDir = cliCompilation.Options.Get(CommonOptionBag.VerificationCoverageReport); + if (coverageReportDir != null) { + await new CoverageReporter(cliCompilation.Options).SerializeVerificationCoverageReport( + proofDependencyManager, resolution.ResolvedProgram, + usedDependencies, + coverageReportDir); + } } } diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs index e0e03daa6d7..1e4dfc031d9 100644 --- a/Source/DafnyDriver/CoverageReporter.cs +++ b/Source/DafnyDriver/CoverageReporter.cs @@ -4,6 +4,7 @@ using System.Linq; using System.Text; using System.Text.RegularExpressions; +using System.Threading.Tasks; using DafnyCore.Verifier; using Microsoft.Boogie; @@ -57,7 +58,7 @@ public CoverageReporter(DafnyOptions options) { } - public void SerializeVerificationCoverageReport(ProofDependencyManager depManager, Program dafnyProgram, IEnumerable usedComponents, string coverageReportDir) { + public async Task SerializeVerificationCoverageReport(ProofDependencyManager depManager, Program dafnyProgram, IEnumerable usedComponents, string coverageReportDir) { var usedDependencies = usedComponents.Select(depManager.GetFullIdDependency).ToHashSet(); var allDependencies = @@ -75,10 +76,10 @@ public void SerializeVerificationCoverageReport(ProofDependencyManager depManage : CoverageLabel.NotCovered); } - SerializeCoverageReports(coverageReport, coverageReportDir); + await SerializeCoverageReports(coverageReport, coverageReportDir); } - public void Merge(List coverageReportsToMerge, string coverageReportOutDir) { + public async Task Merge(List coverageReportsToMerge, string coverageReportOutDir) { List reports = new(); var mergedReport = new CoverageReport("Combined Coverage Report", "Locations", "_combined", null); foreach (var reportDir in coverageReportsToMerge) { @@ -94,7 +95,7 @@ public void Merge(List coverageReportsToMerge, string coverageReportOutD continue; } var suffix = indexFileMatch.Groups[1].Value; - var index = new StreamReader(pathToIndexFile).ReadToEnd(); + var index = await new StreamReader(pathToIndexFile).ReadToEndAsync(); var name = TitleRegexInverse.Match(index)?.Groups?[1]?.Value ?? ""; var units = UnitsRegexInverse.Match(index)?.Groups?[1]?.Value ?? ""; reports.Add(ParseCoverageReport(reportDir, $"{name} ({Path.GetFileName(reportDir)})", units, suffix)); @@ -113,7 +114,7 @@ public void Merge(List coverageReportsToMerge, string coverageReportOutD } } reports.Add(mergedReport); - SerializeCoverageReports(reports, coverageReportOutDir); + await SerializeCoverageReports(reports, coverageReportOutDir); } /// @@ -160,15 +161,15 @@ private static CoverageReport ParseCoverageReport(string reportDir, string name, } /// Serialize a single coverage report to disk - public void SerializeCoverageReports(CoverageReport report, string directory) { - SerializeCoverageReports(new List { report }, directory); + public Task SerializeCoverageReports(CoverageReport report, string directory) { + return SerializeCoverageReports(new List { report }, directory); } /// /// Create a directory with HTML files to display a set of coverage reports for the same program. The reports /// will have links to each other to make comparison easier /// - private void SerializeCoverageReports(List reports, string reportsDirectory) { + private async Task SerializeCoverageReports(List reports, string reportsDirectory) { var sessionDirectory = reportsDirectory; if (!options.Get(CommonOptionBag.NoTimeStampForCoverageReport)) { var sessionName = DateTime.Now.ToString("yyyy-dd-M--HH-mm-ss"); @@ -198,9 +199,9 @@ private void SerializeCoverageReports(List reports, string repor Directory.CreateDirectory(directoryForFile); foreach (var report in reports) { var linksToOtherReports = GetHtmlLinksToOtherReports(report, fileName, reports); - var reportForFile = HtmlReportForFile(report, uri, pathToRoot, linksToOtherReports); + var reportForFile = await HtmlReportForFile(report, uri, pathToRoot, linksToOtherReports); var desiredPath = Path.Combine(directoryForFile, Path.GetFileName(fileName)) + $"{report.Suffix}.html"; - File.WriteAllText(GetPath(report, desiredPath), reportForFile); + await File.WriteAllTextAsync(GetPath(report, desiredPath), reportForFile); } } @@ -334,9 +335,9 @@ private void CopyStyleFiles(string baseDirectory) { } } - private string HtmlReportForFile(CoverageReport report, Uri uri, string baseDirectory, string linksToOtherReports) { - var dafnyFile = DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), OnDiskFileSystem.Instance, options, uri, Token.Cli); - var source = dafnyFile.GetContent().ReadToEnd(); + private async Task HtmlReportForFile(CoverageReport report, Uri uri, string baseDirectory, string linksToOtherReports) { + var dafnyFile = await DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), OnDiskFileSystem.Instance, options, uri, Token.Cli); + var source = await dafnyFile.GetContent().ReadToEndAsync(); var lines = source.Split(new[] { Environment.NewLine }, StringSplitOptions.None); var characterLabels = new CoverageLabel[lines.Length][]; for (int i = 0; i < lines.Length; i++) { @@ -380,7 +381,7 @@ private string HtmlReportForFile(CoverageReport report, Uri uri, string baseDire } labeledCodeBuilder.Append(CloseHtmlTag()); - var assembly = System.Reflection.Assembly.GetCallingAssembly(); + var assembly = System.Reflection.Assembly.GetAssembly(typeof(CoverageReporter))!; var templateStream = assembly.GetManifestResourceStream(CoverageReportTemplatePath); var labeledCode = labeledCodeBuilder.ToString(); if (templateStream is null) { @@ -388,7 +389,7 @@ private string HtmlReportForFile(CoverageReport report, Uri uri, string baseDire "Embedded HTML template for coverage report not found. Returning raw HTML."); return labeledCode; } - var templateText = new StreamReader(templateStream).ReadToEnd(); + var templateText = await new StreamReader(templateStream).ReadToEndAsync(); templateText = PathToRootRegex.Replace(templateText, baseDirectory); templateText = LinksToOtherReportsRegex.Replace(templateText, linksToOtherReports); templateText = IndexLinkRegex.Replace(templateText, Path.GetFileName(GetPath(report, Path.Combine(baseDirectory, $"index{report.Suffix}.html")))); diff --git a/Source/DafnyDriver/DafnyDoc.cs b/Source/DafnyDriver/DafnyDoc.cs index 5688801be13..f25c52712f0 100644 --- a/Source/DafnyDriver/DafnyDoc.cs +++ b/Source/DafnyDriver/DafnyDoc.cs @@ -45,7 +45,7 @@ class DafnyDoc { public static async Task DoDocumenting(DafnyOptions options) { var dafnyFolders = options.SourceFolders; - var code = SynchronousCliCompilation.GetDafnyFiles(options, out var dafnyFiles, out _); + var (code, dafnyFiles, _) = await SynchronousCliCompilation.GetDafnyFiles(options); if (code != 0) { return code; } @@ -59,8 +59,9 @@ public static async Task DoDocumenting(DafnyOptions options) { // Collect all the dafny files; dafnyFiles already includes files from a .toml project file var exitValue = ExitValue.SUCCESS; - dafnyFiles = dafnyFiles.Concat(dafnyFolders.SelectMany(folderPath => - FormatCommand.GetFilesForFolder(options, folderPath))).ToList(); + var folderFiles = (await Task.WhenAll(dafnyFolders.Select(folderPath => + FormatCommand.GetFilesForFolder(options, folderPath)))).SelectMany(x => x); + dafnyFiles = dafnyFiles.Concat(folderFiles).ToList(); await options.OutputWriter.WriteAsync($"Documenting {dafnyFiles.Count} files from {dafnyFolders.Count} folders\n"); if (dafnyFiles.Count == 0) { return exitValue; @@ -70,7 +71,7 @@ public static async Task DoDocumenting(DafnyOptions options) { string err = null; Program dafnyProgram = null; try { - err = DafnyMain.ParseCheck(options.Input, dafnyFiles, programName, options, out dafnyProgram); + (dafnyProgram, err) = await DafnyMain.ParseCheck(options.Input, dafnyFiles, programName, options); } catch (Exception e) { err = "Exception while parsing -- please report the error (use --verbose to see the call stack)"; if (options.Verbose) { diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs index 40aa4f8d7af..01aa430ab00 100644 --- a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs +++ b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs @@ -51,7 +51,7 @@ public static async Task Run(DafnyOptions options) { } options.Backend = backend; - var getFilesExitCode = GetDafnyFiles(options, out var dafnyFiles, out var otherFiles); + var (getFilesExitCode, dafnyFiles, otherFiles) = await GetDafnyFiles(options); if (getFilesExitCode != ExitValue.SUCCESS) { return (int)getFilesExitCode; } @@ -78,9 +78,9 @@ public static async Task Run(DafnyOptions options) { return (int)exitValue; } - public static ExitValue GetDafnyFiles(DafnyOptions options, - out List dafnyFiles, - out List otherFiles) { + public static async Task<(ExitValue ExitValue, + List DafnyFiles, + List OtherFiles)> GetDafnyFiles(DafnyOptions options) { if (options.Printer is NullPrinter) { options.Printer = new DafnyConsolePrinter(options); } @@ -91,27 +91,27 @@ public static ExitValue GetDafnyFiles(DafnyOptions options, } } - dafnyFiles = new List(); - otherFiles = new List(); + var dafnyFiles = new List(); + var otherFiles = new List(); var outputWriter = options.OutputWriter; if (options.UseStdin) { var uri = new Uri("stdin:///"); options.CliRootSourceUris.Add(uri); - dafnyFiles.Add(DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), OnDiskFileSystem.Instance, options, uri, Token.NoToken)); + dafnyFiles.Add(await DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), OnDiskFileSystem.Instance, options, uri, Token.NoToken)); } else if (options.CliRootSourceUris.Count == 0) { - options.ErrorWriter.WriteLine("*** Error: No input files were specified in command-line. " + options.Environment); - return ExitValue.PREPROCESSING_ERROR; + await options.ErrorWriter.WriteLineAsync("*** Error: No input files were specified in command-line. " + options.Environment); + return (ExitValue.PREPROCESSING_ERROR, dafnyFiles, otherFiles); } if (options.XmlSink != null) { string errMsg = options.XmlSink.Open(); if (errMsg != null) { - options.ErrorWriter.WriteLine("*** Error: " + errMsg); - return ExitValue.PREPROCESSING_ERROR; + await options.ErrorWriter.WriteLineAsync("*** Error: " + errMsg); + return (ExitValue.PREPROCESSING_ERROR, dafnyFiles, otherFiles); } } if (options.ShowEnv == ExecutionEngineOptions.ShowEnvironment.Always) { - outputWriter.WriteLine(options.Environment); + await outputWriter.WriteLineAsync(options.Environment); } ISet filesSeen = new HashSet(); @@ -128,10 +128,10 @@ public static ExitValue GetDafnyFiles(DafnyOptions options, : Path.GetRelativePath(Directory.GetCurrentDirectory(), file); try { var consoleErrorReporter = new ConsoleErrorReporter(options); - var df = DafnyFile.CreateAndValidate(consoleErrorReporter, OnDiskFileSystem.Instance, options, new Uri(Path.GetFullPath(file)), Token.Cli); + var df = await DafnyFile.CreateAndValidate(consoleErrorReporter, OnDiskFileSystem.Instance, options, new Uri(Path.GetFullPath(file)), Token.Cli); if (df == null) { if (consoleErrorReporter.FailCompilation) { - return ExitValue.PREPROCESSING_ERROR; + return (ExitValue.PREPROCESSING_ERROR, dafnyFiles, otherFiles); } } else { if (options.LibraryFiles.Contains(file)) { @@ -145,11 +145,11 @@ public static ExitValue GetDafnyFiles(DafnyOptions options, isDafnyFile = true; } } catch (ArgumentException) { - options.ErrorWriter.WriteLine("*** Error: {0}: ", nameToShow); - return ExitValue.PREPROCESSING_ERROR; + await options.ErrorWriter.WriteLineAsync($"*** Error: {nameToShow}: "); + return (ExitValue.PREPROCESSING_ERROR, dafnyFiles, otherFiles); } catch (Exception e) { - options.ErrorWriter.WriteLine("*** Error: {0}: {1}", nameToShow, e.Message); - return ExitValue.PREPROCESSING_ERROR; + await options.ErrorWriter.WriteLineAsync($"*** Error: {nameToShow}: {e.Message}"); + return (ExitValue.PREPROCESSING_ERROR, dafnyFiles, otherFiles); } var supportedExtensions = options.Backend.SupportedExtensions; @@ -160,7 +160,7 @@ public static ExitValue GetDafnyFiles(DafnyOptions options, otherFiles.Add(file); } else { options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {nameToShow} not found"); - return ExitValue.PREPROCESSING_ERROR; + return (ExitValue.PREPROCESSING_ERROR, dafnyFiles, otherFiles); } } else if (options.AllowSourceFolders && Directory.Exists(file)) { options.SourceFolders.Add(file); @@ -179,7 +179,7 @@ public static ExitValue GetDafnyFiles(DafnyOptions options, "*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be Dafny programs (.dfy) or supported auxiliary files ({2})", nameToShow, extension, string.Join(", ", supportedExtensions)); } - return ExitValue.PREPROCESSING_ERROR; + return (ExitValue.PREPROCESSING_ERROR, dafnyFiles, otherFiles); } } @@ -188,13 +188,13 @@ public static ExitValue GetDafnyFiles(DafnyOptions options, options.Printer.ErrorWriteLine(Console.Out, "*** Error: The command-line contains no .dfy files"); // TODO: With the test on CliRootUris.Count above, this code is no longer reachable options.Printer.ErrorWriteLine(options.OutputWriter, "*** Error: The command-line contains no .dfy files"); - return ExitValue.PREPROCESSING_ERROR; + return (ExitValue.PREPROCESSING_ERROR, dafnyFiles, otherFiles); } options.Printer.ErrorWriteLine(Console.Out, "*** Error: The command-line contains no .dfy files or folders"); //options.Printer.ErrorWriteLine(Console.Out, // "Usage:\ndafny format [--check] [--print] ...\nYou can use '.' for the current directory"); - return ExitValue.PREPROCESSING_ERROR; + return (ExitValue.PREPROCESSING_ERROR, dafnyFiles, otherFiles); } // Add standard library .doo files after explicitly provided source files, @@ -206,20 +206,20 @@ public static ExitValue GetDafnyFiles(DafnyOptions options, var targetName = options.CompilerName ?? "notarget"; var stdlibDooUri = DafnyMain.StandardLibrariesDooUriTarget[targetName]; options.CliRootSourceUris.Add(stdlibDooUri); - var targetSpecificFile = DafnyFile.CreateAndValidate(reporter, OnDiskFileSystem.Instance, options, stdlibDooUri, Token.Cli); + var targetSpecificFile = await DafnyFile.CreateAndValidate(reporter, OnDiskFileSystem.Instance, options, stdlibDooUri, Token.Cli); if (targetSpecificFile != null) { dafnyFiles.Add(targetSpecificFile); } } options.CliRootSourceUris.Add(DafnyMain.StandardLibrariesDooUri); - var targetAgnosticFile = DafnyFile.CreateAndValidate(reporter, OnDiskFileSystem.Instance, options, DafnyMain.StandardLibrariesDooUri, Token.Cli); + var targetAgnosticFile = await DafnyFile.CreateAndValidate(reporter, OnDiskFileSystem.Instance, options, DafnyMain.StandardLibrariesDooUri, Token.Cli); if (targetAgnosticFile != null) { dafnyFiles.Add(targetAgnosticFile); } } - return ExitValue.SUCCESS; + return (ExitValue.SUCCESS, dafnyFiles, otherFiles); } private static IExecutableBackend GetBackend(DafnyOptions options) { @@ -265,7 +265,7 @@ public async Task ProcessFilesAsync(IReadOnlyList/*!* var snapshots = new List(); foreach (var f in s) { var uri = new Uri(Path.GetFullPath(f)); - snapshots.Add(DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), OnDiskFileSystem.Instance, options, uri, Token.Cli)); + snapshots.Add(await DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), OnDiskFileSystem.Instance, options, uri, Token.Cli)); options.CliRootSourceUris.Add(uri); } var ev = await ProcessFilesAsync(snapshots, new List().AsReadOnly(), options, depManager, false, programId); @@ -277,7 +277,7 @@ public async Task ProcessFilesAsync(IReadOnlyList/*!* } string programName = dafnyFileNames.Count == 1 ? dafnyFileNames[0] : "the_program"; - var err = DafnyMain.ParseCheck(options.Input, dafnyFiles, programName, options, out var dafnyProgram); + var (dafnyProgram, err) = await DafnyMain.ParseCheck(options.Input, dafnyFiles, programName, options); if (err != null) { exitValue = ExitValue.DAFNY_ERROR; options.Printer.ErrorWriteLine(options.OutputWriter, err); @@ -296,7 +296,7 @@ public async Task ProcessFilesAsync(IReadOnlyList/*!* ProofDependencyWarnings.WarnAboutSuspiciousDependencies(options, dafnyProgram.Reporter, depManager); var coverageReportDir = options.Get(CommonOptionBag.VerificationCoverageReport); if (coverageReportDir != null) { - new CoverageReporter(options).SerializeVerificationCoverageReport( + await new CoverageReporter(options).SerializeVerificationCoverageReport( depManager, dafnyProgram, boogiePrograms.SelectMany(tp => tp.Item2.AllCoveredElements), coverageReportDir); @@ -342,7 +342,7 @@ public async Task ProcessFilesAsync(IReadOnlyList/*!* /// assertion and print it to the console /// private static void PrintCounterexample(DafnyOptions options) { - var firstCounterexample = (options.Printer as DafnyConsolePrinter).VerificationResults + var firstCounterexample = ((DafnyConsolePrinter)options.Printer).VerificationResults .Select(result => result.Result) .Where(result => result.Outcome == VcOutcome.Errors) .Select(result => result.Counterexamples) @@ -731,7 +731,7 @@ public static async Task CompileDafnyProgram(Program dafnyProgram, string if (coverageReportDir != null) { var coverageReport = new CoverageReport("Execution Coverage", "Branches", "_tests_actual", dafnyProgram); compiler.PopulateCoverageReport(coverageReport); - new CoverageReporter(options).SerializeCoverageReports(coverageReport, coverageReportDir); + await new CoverageReporter(options).SerializeCoverageReports(coverageReport, coverageReportDir); } } } else { diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs index 44e08868cdc..09111981114 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs @@ -41,7 +41,8 @@ import opened Producer var projectFile = await CreateOpenAndWaitForResolve(projectFileSource, Path.Combine(consumerDirectory, DafnyProject.FileName)); await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime); - await AssertNoDiagnosticsAreComing(CancellationToken); + var diagnostics = await GetLastDiagnostics(projectFile); + Assert.Single(diagnostics); } /// diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs index 9c9bd98f434..6047ac0a8d4 100644 --- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs @@ -4,6 +4,7 @@ using Moq; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System; +using System.Collections.Generic; using System.Collections.Immutable; using System.IO; using System.Threading; @@ -61,7 +62,7 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() { It.IsAny(), It.IsAny())).Callback(() => source.Cancel()) .Throws(); - var task = textDocumentLoader.ParseAsync(GetCompilation(), source.Token); + var task = textDocumentLoader.ParseAsync(await GetCompilation(), source.Token); try { await task; Assert.Fail("document load was not cancelled"); @@ -72,17 +73,17 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() { } } - private Compilation GetCompilation() { + private async Task GetCompilation() { var versionedTextDocumentIdentifier = CreateTestDocumentId(); var uri = versionedTextDocumentIdentifier.Uri.ToUri(); var fs = new InMemoryFileSystem(ImmutableDictionary.Empty.Add(uri, "")); - var file = DafnyFile.CreateAndValidate(new ErrorReporterSink(DafnyOptions.Default), fs, DafnyOptions.Default, uri, Token.NoToken); + var file = await DafnyFile.CreateAndValidate(new ErrorReporterSink(DafnyOptions.Default), fs, DafnyOptions.Default, uri, Token.NoToken); var input = new CompilationInput(DafnyOptions.Default, 0, ProjectManagerDatabase.ImplicitProject(uri)); var engine = new ExecutionEngine(DafnyOptions.Default, new VerificationResultCache(), CustomStackSizePoolTaskScheduler.Create(0, 0)); var compilation = new Compilation(new Mock>().Object, new Mock().Object, textDocumentLoader, new Mock().Object, engine, input); - compilation.RootFiles = new[] { file }; + compilation.RootFiles = Task.FromResult>(new[] { file }); return compilation; } @@ -91,7 +92,7 @@ public async Task LoadReturnsFaultedTaskIfAnyExceptionOccured() { parser.Setup(p => p.Parse(It.IsAny(), It.IsAny())) .Throws(); - var task = textDocumentLoader.ParseAsync(GetCompilation(), default); + var task = textDocumentLoader.ParseAsync(await GetCompilation(), default); try { await task; Assert.Fail("document load did not fail"); diff --git a/Source/DafnyLanguageServer/Language/CachingParser.cs b/Source/DafnyLanguageServer/Language/CachingParser.cs index f2263ab5646..d198dbe2e65 100644 --- a/Source/DafnyLanguageServer/Language/CachingParser.cs +++ b/Source/DafnyLanguageServer/Language/CachingParser.cs @@ -5,6 +5,7 @@ using System.Security.Cryptography; using System.Text; using System.Threading; +using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.Workspace; using Microsoft.Extensions.Logging; @@ -20,7 +21,8 @@ public CachingParser(ILogger logger, this.telemetryPublisher = telemetryPublisher; } - public override Program ParseFiles(string programName, IReadOnlyList files, ErrorReporter errorReporter, + public override Task ParseFiles(string programName, IReadOnlyList files, + ErrorReporter errorReporter, CancellationToken cancellationToken) { return parseCache.ProfileAndPruneCache(() => base.ParseFiles(programName, files, errorReporter, cancellationToken), diff --git a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs index 083e31d89ae..7e67b471122 100644 --- a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs +++ b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs @@ -3,6 +3,7 @@ using System.Collections.Generic; using System.IO; using System.Threading; +using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.Language.Symbols; using Microsoft.Dafny.LanguageServer.Workspace; @@ -34,12 +35,13 @@ public DafnyLangParser(DafnyOptions options, IFileSystem fileSystem, TelemetryPu : new ProgramParser(innerParserLogger, fileSystem); } - public Program Parse(Compilation compilation, CancellationToken cancellationToken) { - mutex.Wait(cancellationToken); + public async Task Parse(Compilation compilation, CancellationToken cancellationToken) { + await mutex.WaitAsync(cancellationToken); + var rootFiles = await compilation.RootFiles; var beforeParsing = DateTime.Now; try { - return programParser.ParseFiles(compilation.Project.ProjectName, compilation.RootFiles, compilation.Reporter, cancellationToken); + return await programParser.ParseFiles(compilation.Project.ProjectName, rootFiles, compilation.Reporter, cancellationToken); } finally { telemetryPublisher.PublishTime("Parse", compilation.Project.Uri.ToString(), DateTime.Now - beforeParsing); diff --git a/Source/DafnyPipeline.Test/DocstringTest.cs b/Source/DafnyPipeline.Test/DocstringTest.cs index fec1e8d864a..c73878fc743 100644 --- a/Source/DafnyPipeline.Test/DocstringTest.cs +++ b/Source/DafnyPipeline.Test/DocstringTest.cs @@ -4,10 +4,9 @@ using System.IO; using System.Linq; using System.Text.RegularExpressions; +using System.Threading.Tasks; using DafnyCore.Test; using DafnyTestGeneration; -using Bpl = Microsoft.Boogie; -using BplParser = Microsoft.Boogie.Parser; using Microsoft.Dafny; using Xunit; using Xunit.Abstractions; @@ -38,8 +37,8 @@ public DocstringTest(ITestOutputHelper output) { private Newlines currentNewlines; [Fact] - void DocstringWorksForPredicates() { - DocstringWorksFor(@" + async Task DocstringWorksForPredicates() { + await DocstringWorksFor(@" predicate p1() // Always true. Every time. ensures p1() == true @@ -60,8 +59,8 @@ predicate p3(): (y: bool) }); } [Fact] - public void DocstringWorksForFunctions() { - DocstringWorksFor(@" + public async Task DocstringWorksForFunctions() { + await DocstringWorksFor(@" function Test1(i: int): int // Test1 computes an int // It takes an int and adds 1 to it @@ -128,8 +127,8 @@ function Test11(i: int): int } [Fact] - public void DocstringWorksForPredicate() { - DocstringWorksFor(@" + public async Task DocstringWorksForPredicate() { + await DocstringWorksFor(@" class X { static predicate Test1(i: int) // Test1 checks if an int @@ -148,8 +147,8 @@ static predicate Test2(i: int) } [Fact] - public void DocstringWorksForMethodsAndLemmas() { - DocstringWorksFor(@" + public async Task DocstringWorksForMethodsAndLemmas() { + await DocstringWorksFor(@" /** ComputeThing prints something to the screen */ method ComputeThing(i: int) returns (j: int) { print i; } @@ -177,8 +176,8 @@ method ComputeThing4(i: int) }); } [Fact] - public void DocstringWorksForConst() { - DocstringWorksFor(@" + public async Task DocstringWorksForConst() { + await DocstringWorksFor(@" class X { const x2 := 29 // The biggest prime number less than 30 @@ -197,8 +196,8 @@ class X { } [Fact] - public void DocstringWorksForSubsetType() { - DocstringWorksFor(@" + public async Task DocstringWorksForSubsetType() { + await DocstringWorksFor(@" type Odd = x: int | x % 2 == 1 witness 1 // Type of numbers that are not divisible by 2 @@ -261,8 +260,8 @@ type AbstractType2 } [Fact] - public void DocstringWorksForDatatypes() { - DocstringWorksFor(@" + public async Task DocstringWorksForDatatypes() { + await DocstringWorksFor(@" // Unrelated comment datatype State = // A typical log message from a process monitoring @@ -294,8 +293,8 @@ public void DocstringWorksForDatatypes() { [Fact] - public void DocstringWorksForClassAndTraits() { - DocstringWorksFor(@" + public async Task DocstringWorksForClassAndTraits() { + await DocstringWorksFor(@" trait X // A typical base class {} @@ -328,8 +327,8 @@ class A2 extends T [Fact] - public void DocstringWorksForExport() { - DocstringWorksFor(@" + public async Task DocstringWorksForExport() { + await DocstringWorksFor(@" module Test { /** You only get the signatures of f and g */ export hidden provides f @@ -360,8 +359,8 @@ function f(): int { } [Fact] - public void DocstringWorksForModules() { - DocstringWorksFor(@" + public async Task DocstringWorksForModules() { + await DocstringWorksFor(@" // Unattached comment module A // A is the most interesting module @@ -384,8 +383,8 @@ abstract module C } [Fact] - public void DocstringWorksForIterators() { - DocstringWorksFor(@" + public async Task DocstringWorksForIterators() { + await DocstringWorksFor(@" /** Iter is interesting */ iterator Iter(x: int) yields (y: int) requires A: 0 <= x @@ -421,13 +420,13 @@ iterator Iter2(x: int) yields (y: int) } } - protected void DocstringWorksFor(string source, string nodeTokenValue, string? expectedDocstring) { - DocstringWorksFor(source, new List<(string nodeTokenValue, string? expectedDocstring)>() { + protected Task DocstringWorksFor(string source, string nodeTokenValue, string? expectedDocstring) { + return DocstringWorksFor(source, new List<(string nodeTokenValue, string? expectedDocstring)>() { (nodeTokenValue, expectedDocstring) }); } - protected void DocstringWorksFor(string source, List<(string nodeTokenValue, string? expectedDocstring)> tests) { + protected async Task DocstringWorksFor(string source, List<(string nodeTokenValue, string? expectedDocstring)> tests) { var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(output)); var newlineTypes = Enum.GetValues(typeof(Newlines)); foreach (Newlines newLinesType in newlineTypes) { @@ -437,7 +436,7 @@ protected void DocstringWorksFor(string source, List<(string nodeTokenValue, str var programString = AdjustNewlines(source); var reporter = new BatchErrorReporter(options); - var dafnyProgram = Utils.Parse(reporter, programString, false); + var dafnyProgram = await Utils.Parse(reporter, programString, false); if (reporter.HasErrors) { var error = reporter.AllMessagesByLevel[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs index 29b58aed2e7..3eaae257674 100644 --- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs +++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs @@ -4,6 +4,7 @@ using System.Collections.Immutable; using System.IO; using System.Text.RegularExpressions; +using System.Threading.Tasks; using DafnyCore.Test; using DafnyTestGeneration; using Bpl = Microsoft.Boogie; @@ -42,7 +43,7 @@ enum Newlines { private Newlines currentNewlines; - protected void FormatterWorksFor(string testCase, string? expectedProgramString = null, bool expectNoToken = false, + protected async Task FormatterWorksFor(string testCase, string? expectedProgramString = null, bool expectNoToken = false, bool reduceBlockiness = true) { var options = DafnyOptions.Create(output); options.DisallowIncludes = true; @@ -61,7 +62,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString var reporter = new BatchErrorReporter(options); Microsoft.Dafny.Type.ResetScopes(); - var dafnyProgram = new ProgramParser().Parse(programNotIndented, uri, reporter); + var dafnyProgram = await new ProgramParser().Parse(programNotIndented, uri, reporter); if (reporter.HasErrors) { var error = reporter.AllMessagesByLevel[ErrorLevel.Error][0]; @@ -79,7 +80,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString : programString; EnsureEveryTokenIsOwned(uri, programNotIndented, dafnyProgram); if (expectedProgram != reprinted) { - Console.Out.WriteLine("Formatting after parsing generates an error:"); + await Console.Out.WriteLineAsync("Formatting after parsing generates an error:"); Assert.Equal(expectedProgram, reprinted); } @@ -104,7 +105,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString : programString; EnsureEveryTokenIsOwned(uri, programNotIndented, dafnyProgram); if (expectedProgram != reprintedCloned) { - Console.Out.WriteLine("Formatting after parsing + cloning generates an error:"); + await Console.Out.WriteLineAsync("Formatting after parsing + cloning generates an error:"); Assert.Equal(expectedProgram, reprinted); } @@ -115,7 +116,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString IndentationFormatter.ForProgram(dafnyProgram, firstToken.Uri, reduceBlockiness)) : programString; if (expectedProgram != reprinted) { - options.ErrorWriter.WriteLine("Formatting after resolution generates an error:"); + await options.ErrorWriter.WriteLineAsync("Formatting after resolution generates an error:"); Assert.Equal(expectedProgram, reprinted); } @@ -124,8 +125,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString // Verify that the formatting is stable. Microsoft.Dafny.Type.ResetScopes(); var newReporter = new BatchErrorReporter(options); - dafnyProgram = new ProgramParser().Parse(reprinted, uri, newReporter); - ; + dafnyProgram = await new ProgramParser().Parse(reprinted, uri, newReporter); Assert.Equal(initErrorCount, reporter.ErrorCount + newReporter.ErrorCount); firstToken = dafnyProgram.GetFirstTokenForUri(uri); diff --git a/Source/DafnyPipeline.Test/FormatterComprehensions.cs b/Source/DafnyPipeline.Test/FormatterComprehensions.cs index 1795182fad9..de40d1e6636 100644 --- a/Source/DafnyPipeline.Test/FormatterComprehensions.cs +++ b/Source/DafnyPipeline.Test/FormatterComprehensions.cs @@ -1,4 +1,5 @@ -using JetBrains.Annotations; +using System.Threading.Tasks; +using JetBrains.Annotations; using Xunit; using Xunit.Abstractions; @@ -7,8 +8,8 @@ namespace DafnyPipeline.Test; [Collection("Singleton Test Collection - FormatterForComprehensions")] public class FormatterForComprehensions : FormatterBaseTest { [Fact] - public void FormatWorksForMatchExpression() { - FormatterWorksFor(@" + public async Task FormatWorksForMatchExpression() { + await FormatterWorksFor(@" predicate bad(e:Maybe) { forall i :: 0 <= i < 1 ==> @@ -27,8 +28,8 @@ predicate bad2(e:Maybe) } [Fact] - public void FormatWorksForComprehensions() { - FormatterWorksFor(@" + public async Task FormatWorksForComprehensions() { + await FormatterWorksFor(@" method comprehensions() { c := imap i: int | i % 9 == 0 @@ -71,7 +72,7 @@ method comprehensions() { := 17; } "); - FormatterWorksFor(@" + await FormatterWorksFor(@" method comprehensions() { var a := imap t: int :: t % 3 @@ -107,8 +108,8 @@ method comprehensions() { } [Fact] - public void FormatterWorksForVarsAndGhostVarsAndUnchanged() { - FormatterWorksFor(@" + public async Task FormatterWorksForVarsAndGhostVarsAndUnchanged() { + await FormatterWorksFor(@" twostate predicate BadVariations(c: Twostate, d: Twostate, e: Twostate, f: Twostate) { && unchanged( @@ -145,8 +146,8 @@ function Fu(): int } [Fact] - public void FormatterWorksForLinearFunctionBody() { - FormatterWorksFor(@" + public async Task FormatterWorksForLinearFunctionBody() { + await FormatterWorksFor(@" function test(): int { :- Need(u); :- Need(u); @@ -158,8 +159,8 @@ function test(): int { } [Fact] - public void FormatterWorksForComparisons() { - FormatterWorksFor(@" + public async Task FormatterWorksForComparisons() { + await FormatterWorksFor(@" function f(x: int): (y: int) ensures x == y @@ -179,8 +180,8 @@ ensures x "); } [Fact] - public void FormatterWorksForForallExpressions() { - FormatterWorksFor(@" + public async Task FormatterWorksForForallExpressions() { + await FormatterWorksFor(@" predicate GoodIdentifier(s: string) { && s != [] && (|| 'a' <= s[0] <= 'z' @@ -199,8 +200,8 @@ predicate BadIdentifier(s: string) { } [Fact] - public void FormatterWorksForSetComprehension() { - FormatterWorksFor(@" + public async Task FormatterWorksForSetComprehension() { + await FormatterWorksFor(@" function test(): int { | set i: nat | i < 10 diff --git a/Source/DafnyPipeline.Test/FormatterForApplySuffixRelated.cs b/Source/DafnyPipeline.Test/FormatterForApplySuffixRelated.cs index dc47cd7e198..9f622d6d704 100644 --- a/Source/DafnyPipeline.Test/FormatterForApplySuffixRelated.cs +++ b/Source/DafnyPipeline.Test/FormatterForApplySuffixRelated.cs @@ -1,4 +1,5 @@ -using JetBrains.Annotations; +using System.Threading.Tasks; +using JetBrains.Annotations; using Xunit; using Xunit.Abstractions; @@ -7,8 +8,8 @@ namespace DafnyPipeline.Test; [Collection("Singleton Test Collection - FormatterForApplySuffixRelated")] public class FormatterForApplySuffixRelated : FormatterBaseTest { [Fact] - public void FormatterWorksForArguments() { - FormatterWorksFor(@" + public async Task FormatterWorksForArguments() { + await FormatterWorksFor(@" method Test() { me(func(arg(5, diff --git a/Source/DafnyPipeline.Test/FormatterForAssignments.cs b/Source/DafnyPipeline.Test/FormatterForAssignments.cs index 25b53785b59..2af2a7388a8 100644 --- a/Source/DafnyPipeline.Test/FormatterForAssignments.cs +++ b/Source/DafnyPipeline.Test/FormatterForAssignments.cs @@ -1,4 +1,5 @@ -using JetBrains.Annotations; +using System.Threading.Tasks; +using JetBrains.Annotations; using Xunit; using Xunit.Abstractions; @@ -7,8 +8,8 @@ namespace DafnyPipeline.Test; [Collection("Singleton Test Collection - FormatterForAssignments")] public class FormatterForAssignments : FormatterBaseTest { [Fact] - public void FormatterWorksForAssignments() { - FormatterWorksFor(@"method test() { + public async Task FormatterWorksForAssignments() { + await FormatterWorksFor(@"method test() { var x := @@ -29,8 +30,8 @@ public void FormatterWorksForAssignments() { }"); } [Fact] - public void FormatterWorksForVarAssignments() { - FormatterWorksFor(@" + public async Task FormatterWorksForVarAssignments() { + await FormatterWorksFor(@" method Test() { var y, z @@ -79,8 +80,8 @@ var y } [Fact] - public void FormatterWorksForObjectCreation() { - FormatterWorksFor(@" + public async Task FormatterWorksForObjectCreation() { + await FormatterWorksFor(@" method Test() { g := new ClassName.ConstructorName( argument1b, @@ -148,8 +149,8 @@ method Test() { ", reduceBlockiness: true); } [Fact] - public void FormatterWorksForObjectCreationBlockly() { - FormatterWorksFor(@" + public async Task FormatterWorksForObjectCreationBlockly() { + await FormatterWorksFor(@" method Test() { :- Module.Need( arg3, diff --git a/Source/DafnyPipeline.Test/FormatterForCalcStmt.cs b/Source/DafnyPipeline.Test/FormatterForCalcStmt.cs index 16b74ec76d4..ab14147daca 100644 --- a/Source/DafnyPipeline.Test/FormatterForCalcStmt.cs +++ b/Source/DafnyPipeline.Test/FormatterForCalcStmt.cs @@ -1,4 +1,5 @@ -using JetBrains.Annotations; +using System.Threading.Tasks; +using JetBrains.Annotations; using Xunit; using Xunit.Abstractions; @@ -7,8 +8,8 @@ namespace DafnyPipeline.Test; [Collection("Singleton Test Collection - FormatterForCalcStmt")] public class FormatterForCalcStmt : FormatterBaseTest { [Fact] - public void FormatterWorksForHintsInCalcStatements() { - FormatterWorksFor(@" + public async Task FormatterWorksForHintsInCalcStatements() { + await FormatterWorksFor(@" class Test { ghost constructor CalcInInitializationPhase() { var c0 := new Cell; // fine here diff --git a/Source/DafnyPipeline.Test/FormatterForComments.cs b/Source/DafnyPipeline.Test/FormatterForComments.cs index b346ba1ba4d..47a4a730286 100644 --- a/Source/DafnyPipeline.Test/FormatterForComments.cs +++ b/Source/DafnyPipeline.Test/FormatterForComments.cs @@ -1,4 +1,5 @@ -using JetBrains.Annotations; +using System.Threading.Tasks; +using JetBrains.Annotations; using Xunit; using Xunit.Abstractions; @@ -7,8 +8,8 @@ namespace DafnyPipeline.Test; [Collection("Singleton Test Collection - FormatterForComments")] public class FormatterForComments : FormatterBaseTest { [Fact] - public void FormatterWorksForCommentsHoldingTogether() { - FormatterWorksFor(@" + public async Task FormatterWorksForCommentsHoldingTogether() { + await FormatterWorksFor(@" const x := 2; /* start of comment These words aligned: start */ @@ -18,7 +19,7 @@ public void FormatterWorksForCommentsHoldingTogether() { const y := 3;"); - FormatterWorksFor(@" + await FormatterWorksFor(@" const x := 4; /* start of comment end of comment @@ -30,7 +31,7 @@ end of comment should stay aligned*/ const y := 5;"); - FormatterWorksFor(@" + await FormatterWorksFor(@" const x := 6; /* start of comment @@ -47,8 +48,8 @@ should stay aligned*/ [Fact] - public void FormatterWorksForMultilineCommentsStartingWithRowOfStars() { - FormatterWorksFor(@" + public async Task FormatterWorksForMultilineCommentsStartingWithRowOfStars() { + await FormatterWorksFor(@" /*********** * These are test cases for monotonicity of the the _k parameter. However, monotonicity * does not appear to be useful in the test suite, and it is possible that the axioms @@ -60,7 +61,7 @@ function test(): int } [Fact] - public void FormatterWorksForConsecutiveComments() { + public async Task FormatterWorksForConsecutiveComments() { var testCase = @" abstract module M0 { /******* State *******/ @@ -90,12 +91,12 @@ function build(prog: Program, st: State, useCache: bool): Tuple) // This definition is not allowed because Dt appears in a non-strict/lax position @@ -113,8 +114,8 @@ method M4() { }"); } [Fact] - public void FormatterWorksForAdvancedClosures() { - FormatterWorksFor(@" + public async Task FormatterWorksForAdvancedClosures() { + await FormatterWorksFor(@" method LRead() { var o : object?; var f : Ref<() ~> bool>; @@ -169,8 +170,8 @@ decreases t0 } [Fact] - public void FormatterWorksForCommentAfterSubsetType() { - FormatterWorksFor(@" + public async Task FormatterWorksForCommentAfterSubsetType() { + await FormatterWorksFor(@" module R1 refines Q { type G = real // specify G // now, it is known how to initialize @@ -178,7 +179,7 @@ module R1 refines Q { } [Fact] - public void FormatterWorksForLongCommentsDocument() { + public async Task FormatterWorksForLongCommentsDocument() { var testCase = @" module R { /* Simple comment @@ -205,11 +206,11 @@ import opened LibA function g(): int { 4 } } "; - FormatterWorksFor(testCase, testCase); + await FormatterWorksFor(testCase, testCase); } [Fact] - public void FormatterWorksForTutorialStyle() { - FormatterWorksFor(@" + public async Task FormatterWorksForTutorialStyle() { + await FormatterWorksFor(@" /// Tutorial style abstract module C { @@ -225,7 +226,7 @@ abstract module C { "); } [Fact] - public void FormatterWorksForAlignedSingleLineTrailingComments() { + public async Task FormatterWorksForAlignedSingleLineTrailingComments() { var before = @" module RefinedF refines BaseF { function f(): bool { false } // OK. Local f preferred over imported f @@ -260,12 +261,12 @@ method DeclWithHavoc() // This comment should be on its own line } }"; - FormatterWorksFor(before, after); + await FormatterWorksFor(before, after); } [Fact] - public void FormatterWorksForUtf8InComment() { - FormatterWorksFor(@" + public async Task FormatterWorksForUtf8InComment() { + await FormatterWorksFor(@" // x ∈ a[..3] Dafny won’t prove, Wüstholz would, Mikaël doesn’t voilà Great job const x: int "); diff --git a/Source/DafnyPipeline.Test/FormatterForDatatypeDeclarationTest.cs b/Source/DafnyPipeline.Test/FormatterForDatatypeDeclarationTest.cs index aa9ca091f33..72676b368fc 100644 --- a/Source/DafnyPipeline.Test/FormatterForDatatypeDeclarationTest.cs +++ b/Source/DafnyPipeline.Test/FormatterForDatatypeDeclarationTest.cs @@ -1,4 +1,5 @@ -using JetBrains.Annotations; +using System.Threading.Tasks; +using JetBrains.Annotations; using Xunit; using Xunit.Abstractions; @@ -7,15 +8,15 @@ namespace DafnyPipeline.Test; [Collection("Singleton Test Collection - FormatterForDatatypeDeclaration")] public class FormatterForDatatypeDeclarationTest : FormatterBaseTest { [Fact] - public void FormatterWorksForFinalSpaceAfterDatatype() { - FormatterWorksFor(@" + public async Task FormatterWorksForFinalSpaceAfterDatatype() { + await FormatterWorksFor(@" datatype Maybe = None | Some(get: T) "); } [Fact] - public void FormatWorksForDataTypes() { - FormatterWorksFor(@" + public async Task FormatWorksForDataTypes() { + await FormatterWorksFor(@" include ""test1"" include ""test2"" @@ -66,8 +67,8 @@ datatype Color2 } [Fact] - public void FormatterWorksForUniversalPatternShiftDatatypeParens() { - FormatterWorksFor(@" + public async Task FormatterWorksForUniversalPatternShiftDatatypeParens() { + await FormatterWorksFor(@" newtype b17 = x | 0 <= x < (10 as bv8 << -1) as int newtype b18 = x | 0 <= x < (10 as bv8 >> -1) as int @@ -84,8 +85,8 @@ method UniversalPattern() { } [Fact] - public void FormatterWorksForIteratorsAfterDatatypes() { - FormatterWorksFor(@" + public async Task FormatterWorksForIteratorsAfterDatatypes() { + await FormatterWorksFor(@" datatype MG5 = MG5(ghost x: int, y: int := FG(x), ghost z: int := FC(x), w: int := FC(x)) // error: call to FC passes in a ghost expression iterator MG6( x: int, y: int := FG(x), ghost z: int := FC(x), w: int := FC(x)) iterator MG7(ghost x: int, y: int := FG(x), ghost z: int := FC(x), w: int := FC(x)) // error: call to FC passes in a ghost expression @@ -99,8 +100,8 @@ yield requires true [Fact] - public void FormatterWorksForDatatypeWithVerticalBarAfterwardsOrOneLine() { - FormatterWorksFor(@" + public async Task FormatterWorksForDatatypeWithVerticalBarAfterwardsOrOneLine() { + await FormatterWorksFor(@" datatype Single = SingleWithArguments(a: int) @@ -117,8 +118,8 @@ public void FormatterWorksForDatatypeWithVerticalBarAfterwardsOrOneLine() { } [Fact] - public void FormatterWorksForDoublecomment() { - FormatterWorksFor(@" + public async Task FormatterWorksForDoublecomment() { + await FormatterWorksFor(@" datatype Test = | Zero /* Zero */ @@ -131,14 +132,14 @@ public void FormatterWorksForDoublecomment() { "); } [Fact] - public void FormatterWorksForSingleDatatypeConstructor() { - FormatterWorksFor(@" + public async Task FormatterWorksForSingleDatatypeConstructor() { + await FormatterWorksFor(@" datatype C = C( arg1: int, arg2: int ) ", reduceBlockiness: true); - FormatterWorksFor(@" + await FormatterWorksFor(@" datatype C = C( arg1: int, arg2: int diff --git a/Source/DafnyPipeline.Test/FormatterForExpressions.cs b/Source/DafnyPipeline.Test/FormatterForExpressions.cs index 380062015cc..438c47572df 100644 --- a/Source/DafnyPipeline.Test/FormatterForExpressions.cs +++ b/Source/DafnyPipeline.Test/FormatterForExpressions.cs @@ -1,4 +1,5 @@ -using JetBrains.Annotations; +using System.Threading.Tasks; +using JetBrains.Annotations; using Xunit; using Xunit.Abstractions; @@ -7,8 +8,8 @@ namespace DafnyPipeline.Test; [Collection("Singleton Test Collection - FormatterForExpressions")] public class FormatterForExpressions : FormatterBaseTest { [Fact] - public void FormatterWorksForFunctionsIfExprAndMatchCases() { - FormatterWorksFor(@" + public async Task FormatterWorksForFunctionsIfExprAndMatchCases() { + await FormatterWorksFor(@" function Zipper2(a: List, b: List) : List decreases /* max(a,b) */ if a < b then b else a, @@ -51,8 +52,8 @@ match x } [Fact] - public void FormatterWorksForCaseComments() { - FormatterWorksFor(@" + public async Task FormatterWorksForCaseComments() { + await FormatterWorksFor(@" predicate SmallOdd(i: int) { match i // Case small odd @@ -85,8 +86,8 @@ match i } [Fact] - public void FormatterWorksForMatchStatementsAndExpressions() { - FormatterWorksFor(@" + public async Task FormatterWorksForMatchStatementsAndExpressions() { + await FormatterWorksFor(@" method Test(z: int) { match z { @@ -139,8 +140,8 @@ match z { } [Fact] - public void FormatWorksForChainedImplications() { - FormatterWorksFor(@" + public async Task FormatWorksForChainedImplications() { + await FormatterWorksFor(@" method Test() { assert (1 ==> 2 ==> @@ -158,8 +159,8 @@ method Test() { } [Fact] - public void FormatWorksForFirstNestedElephantAssignments() { - FormatterWorksFor(@" + public async Task FormatWorksForFirstNestedElephantAssignments() { + await FormatterWorksFor(@" function TestExpressionParsing(b: bool, n: nat, o1: NatOutcome, o2: NatOutcome): NatOutcome { var expr1: nat :- (var x := if b then o1 else o2; x); var use_expr1: nat := expr1; @@ -171,7 +172,7 @@ function TestExpressionParsing(b: bool, n: nat, o1: NatOutcome, o2: NatOutcome): } [Fact] - public void FormatterWorksForNestedIfElse() { + public async Task FormatterWorksForNestedIfElse() { var testCase = @" function test(): int { if a then @@ -182,12 +183,12 @@ function test(): int { e } "; - FormatterWorksFor(testCase, testCase); + await FormatterWorksFor(testCase, testCase); } [Fact] - public void FormatterWorksForNestedConstructors() { - FormatterWorksFor(@" + public async Task FormatterWorksForNestedConstructors() { + await FormatterWorksFor(@" function test(): int { assert X; Some(Result( @@ -198,8 +199,8 @@ function test(): int { "); } [Fact] - public void FormatterWorksForEqualPlus() { - FormatterWorksFor(@" + public async Task FormatterWorksForEqualPlus() { + await FormatterWorksFor(@" function test(a: int, b: int, c: int): int requires a == b + d + e + f + g + h @@ -208,8 +209,8 @@ function test(a: int, b: int, c: int): int } [Fact] - public void FormatterWorksForCommentBeforeElse() { - FormatterWorksFor(@" + public async Task FormatterWorksForCommentBeforeElse() { + await FormatterWorksFor(@" function test(i: int): int { if true then Class.StaticMethod(argument) @@ -221,8 +222,8 @@ function test(i: int): int { } [Fact] - public void FormatterWorksForElseWithComplexContent() { - FormatterWorksFor(@" + public async Task FormatterWorksForElseWithComplexContent() { + await FormatterWorksFor(@" function Test(value: string): bool { if value == """" then Constructor(arg) else if value == ""1"" then Constructor1(arg) @@ -235,8 +236,8 @@ function Test(value: string): bool { } [Fact] - public void FormatterWorksForAlignedOrVar() { - FormatterWorksFor(@" + public async Task FormatterWorksForAlignedOrVar() { + await FormatterWorksFor(@" predicate IsBinary(s: seq) { forall i | 0 <= i < |s| :: || s[i] == 0 @@ -245,8 +246,8 @@ predicate IsBinary(s: seq) { } [Fact] - public void FormatterWorksForAlignedAmpVar() { - FormatterWorksFor(@" + public async Task FormatterWorksForAlignedAmpVar() { + await FormatterWorksFor(@" method Test() ensures && P() @@ -268,8 +269,8 @@ match A } [Fact] - public void FormatterWorksForEqualityOnItsOwnLine() { - FormatterWorksFor(@" + public async Task FormatterWorksForEqualityOnItsOwnLine() { + await FormatterWorksFor(@" function Test(): int { if A then assert C(a1, b1, c1) @@ -296,8 +297,8 @@ assert A } [Fact] - public void FormatterWorksForMatchInMap() { - FormatterWorksFor(@" + public async Task FormatterWorksForMatchInMap() { + await FormatterWorksFor(@" method AlignMapComplex(a: int) returns (r: map) { return ComputeMap(map[ ""a"" := Compute( @@ -310,8 +311,8 @@ match a { } [Fact] - public void FormatterWorksForSeqSetMapDisplay() { - FormatterWorksFor(@" + public async Task FormatterWorksForSeqSetMapDisplay() { + await FormatterWorksFor(@" function AlignSeq(): seq> { [ [ 1, 2, 3 ], [ 4, @@ -344,8 +345,8 @@ function AlignSet(): set { [Fact] - public void FormatterWorksForChainingEquality() { - FormatterWorksFor(@" + public async Task FormatterWorksForChainingEquality() { + await FormatterWorksFor(@" lemma SeventeenIsNotEven() ensures !Even(N(17)) @@ -365,7 +366,7 @@ assert Even(N(17)) "); } [Fact] - public void FormatterWorksForAligningThenAndElseIfAligned() { + public async Task FormatterWorksForAligningThenAndElseIfAligned() { var testCase = @" predicate Valid() { @@ -376,7 +377,7 @@ predicate Valid() else data[start..] + data[..start+len-N] } "; - FormatterWorksFor(testCase, testCase); + await FormatterWorksFor(testCase, testCase); } public FormatterForExpressions([NotNull] ITestOutputHelper output) : base(output) { diff --git a/Source/DafnyPipeline.Test/FormatterForMembers.cs b/Source/DafnyPipeline.Test/FormatterForMembers.cs index 7caa40515a3..aa11489c488 100644 --- a/Source/DafnyPipeline.Test/FormatterForMembers.cs +++ b/Source/DafnyPipeline.Test/FormatterForMembers.cs @@ -1,4 +1,5 @@ -using JetBrains.Annotations; +using System.Threading.Tasks; +using JetBrains.Annotations; using Xunit; using Xunit.Abstractions; @@ -7,8 +8,8 @@ namespace DafnyPipeline.Test; [Collection("Singleton Test Collection - FormatterForMembers")] public class FormatterForMembers : FormatterBaseTest { [Fact] - public void FormatterWorksForMethodsInModule() { - FormatterWorksFor(@" + public async Task FormatterWorksForMethodsInModule() { + await FormatterWorksFor(@" import opened Test module Test { method f1(a: T, b: U) @@ -141,8 +142,8 @@ least lemma l2[nat } [Fact] - public void FormatWorksForFunctionMethods() { - FormatterWorksFor(@" + public async Task FormatWorksForFunctionMethods() { + await FormatterWorksFor(@" function Test(): int { 1 } by method { @@ -154,8 +155,8 @@ assert IsScriptForward(edits[..0], |s|) by { } [Fact] - public void FormatWorksForFunctionByMethods() { - FormatterWorksFor(@" + public async Task FormatWorksForFunctionByMethods() { + await FormatterWorksFor(@" function Fib(i: nat): nat { 1 } by method { @@ -171,8 +172,8 @@ function Fib(i: nat): nat { } [Fact] - public void FormatWorksConstant() { - FormatterWorksFor(@" + public async Task FormatWorksConstant() { + await FormatterWorksFor(@" class T { const x : int @@ -183,8 +184,8 @@ const x }"); } [Fact] - public void FormatterWorksForConstants() { - FormatterWorksFor(@" + public async Task FormatterWorksForConstants() { + await FormatterWorksFor(@" const c := 1111111111111111111111111111111111111111 const ASSIGNED_PLANES := [ @@ -206,8 +207,8 @@ public void FormatterWorksForConstants() { } [Fact] - public void FormatterWorksForExtremePredicates() { - FormatterWorksFor(@" + public async Task FormatterWorksForExtremePredicates() { + await FormatterWorksFor(@" lemma Lemma(k: ORDINAL, r: real) requires E.P(r) requires E.P#[k](r) @@ -215,8 +216,8 @@ requires E.P(r) } [Fact] - public void FormatterWorksForSmokeTest() { - FormatterWorksFor(@" + public async Task FormatterWorksForSmokeTest() { + await FormatterWorksFor(@" include ""../libraries/src/Wrappers.dfy"" import opened Wrappers diff --git a/Source/DafnyPipeline.Test/FormatterForSpecifications.cs b/Source/DafnyPipeline.Test/FormatterForSpecifications.cs index 91037888f1a..26cf459e5d4 100644 --- a/Source/DafnyPipeline.Test/FormatterForSpecifications.cs +++ b/Source/DafnyPipeline.Test/FormatterForSpecifications.cs @@ -1,4 +1,5 @@ -using JetBrains.Annotations; +using System.Threading.Tasks; +using JetBrains.Annotations; using Xunit; using Xunit.Abstractions; @@ -7,8 +8,8 @@ namespace DafnyPipeline.Test; [Collection("Singleton Test Collection - FormatterForSpecifications")] public class FormatterForSpecifications : FormatterBaseTest { [Fact] - public void FormatterWorksForModifyStatements() { - FormatterWorksFor(@" + public async Task FormatterWorksForModifyStatements() { + await FormatterWorksFor(@" method Test() { modify x { x := 2; @@ -32,8 +33,8 @@ modify x { } [Fact] - public void FormatterWorksForDecreasesInvariantComments() { - FormatterWorksFor(@" + public async Task FormatterWorksForDecreasesInvariantComments() { + await FormatterWorksFor(@" method Test() { while X decreases true || false @@ -47,8 +48,8 @@ invariant true || false } [Fact] - public void FormatterWorksForAssertAssumeExpectPrintReveal() { - FormatterWorksFor(@" + public async Task FormatterWorksForAssertAssumeExpectPrintReveal() { + await FormatterWorksFor(@" method Test(z: int) { assert z == 1; assert z == 1 @@ -100,8 +101,8 @@ reveal P3() } [Fact] - public void FormatterWorksForCommentsAndAlignmentAmpStatements() { - FormatterWorksFor(@" + public async Task FormatterWorksForCommentsAndAlignmentAmpStatements() { + await FormatterWorksFor(@" module Test { /** A comment * Followed by newline @@ -217,8 +218,8 @@ invariant true } [Fact] - public void FormatterWorksForMethodBeforeAClass() { - FormatterWorksFor(@" + public async Task FormatterWorksForMethodBeforeAClass() { + await FormatterWorksFor(@" method Test() ensures true || false // comment should be between ensures and not attached to true/false diff --git a/Source/DafnyPipeline.Test/FormatterForStatements.cs b/Source/DafnyPipeline.Test/FormatterForStatements.cs index c04ea0500d8..1e87eb9b227 100644 --- a/Source/DafnyPipeline.Test/FormatterForStatements.cs +++ b/Source/DafnyPipeline.Test/FormatterForStatements.cs @@ -1,4 +1,5 @@ -using JetBrains.Annotations; +using System.Threading.Tasks; +using JetBrains.Annotations; using Xunit; using Xunit.Abstractions; @@ -7,8 +8,8 @@ namespace DafnyPipeline.Test; [Collection("Singleton Test Collection - FormatterForStatements")] public class FormatterForStatements : FormatterBaseTest { [Fact] - public void FormatterWorksForWhileTests() { - FormatterWorksFor(@" + public async Task FormatterWorksForWhileTests() { + await FormatterWorksFor(@" method Test() { rs.Close(); ghost var qc := q.contents; @@ -56,8 +57,8 @@ invariant q !in wr.footprint } [Fact] - public void FormatterWorksForAlternatives() { - FormatterWorksFor(@" + public async Task FormatterWorksForAlternatives() { + await FormatterWorksFor(@" method AlternativeStmt() { if { @@ -97,8 +98,8 @@ method AlternativeLoopStmt() { } [Fact] - public void FormatterWorksForElephantOperatorWithoutLHS() { - FormatterWorksFor(@" + public async Task FormatterWorksForElephantOperatorWithoutLHS() { + await FormatterWorksFor(@" method {:test} PassingTestUsingNoLHSAssignOrHalt() { :- // Comment expect FailUnless(true); @@ -108,8 +109,8 @@ public void FormatterWorksForElephantOperatorWithoutLHS() { } [Fact] - public void FormatterWorksForPrintStmt() { - FormatterWorksFor(@" + public async Task FormatterWorksForPrintStmt() { + await FormatterWorksFor(@" // Sanity check method Main() { print FunctionMethodSyntax.CompiledFunction() @@ -127,8 +128,8 @@ print FunctionMethodSyntax.CompiledFunction() } [Fact] - public void FormatterWorksForIfCaseReturn() { - FormatterWorksFor(@" + public async Task FormatterWorksForIfCaseReturn() { + await FormatterWorksFor(@" method Test() { if case true => @@ -142,8 +143,8 @@ method Test() { [Fact] - public void FormatterWorksForElephantOperatorInMatch() { - FormatterWorksFor(@" + public async Task FormatterWorksForElephantOperatorInMatch() { + await FormatterWorksFor(@" method execute_external_method(n:nat, m:nat) returns (r:Status) { match n { // match statement is essential to reproduce the bug @@ -163,8 +164,8 @@ match m { } [Fact] - public void FormatterWorksForBraceAfterArrowAndSimilar() { - FormatterWorksFor(@" + public async Task FormatterWorksForBraceAfterArrowAndSimilar() { + await FormatterWorksFor(@" function Test(): int { match s case None => ( @@ -192,8 +193,8 @@ match s { } [Fact] - public void FormatterWorksForLabelsBeforeIf() { - FormatterWorksFor(@" + public async Task FormatterWorksForLabelsBeforeIf() { + await FormatterWorksFor(@" method TheBreaker_AllGood(M: int, N: int, O: int) { @@ -208,8 +209,8 @@ method TheBreaker_AllGood(M: int, N: int, O: int) } [Fact] - public void FormatterWorksForSkeletonStatement() { - FormatterWorksFor(@" + public async Task FormatterWorksForSkeletonStatement() { + await FormatterWorksFor(@" module ModifyStmtBreak1 refines ModifyStmtBreak0 { method W... { while true @@ -232,8 +233,8 @@ modify ... { } [Fact] - public void FormatterWorksForDividedBlockStmt() { - FormatterWorksFor(@" + public async Task FormatterWorksForDividedBlockStmt() { + await FormatterWorksFor(@" class X { constructor Init(x: nat) { @@ -246,8 +247,8 @@ constructor Init(x: nat) } [Fact] - public void FormatterWorksForControlFlow() { - FormatterWorksFor(@" + public async Task FormatterWorksForControlFlow() { + await FormatterWorksFor(@" method ControlFlowTest() { while decreases O - k; @@ -264,8 +265,8 @@ method ControlFlowTest() { "); } [Fact] - public void FormatterWorksForIfInLemma() { - FormatterWorksFor(@" + public async Task FormatterWorksForIfInLemma() { + await FormatterWorksFor(@" lemma AlltokenSpec(i: int) requires Valid() decreases |allTokens| @@ -281,8 +282,8 @@ requires Valid() } [Fact] - public void FormatterWorksForParticularCase() { - FormatterWorksFor(@" + public async Task FormatterWorksForParticularCase() { + await FormatterWorksFor(@" module Test { lemma ProveMeThis(i: nat) { @@ -312,8 +313,8 @@ lemma ProveMeThis(i: nat) "); } [Fact] - public void FormatterWorksForUsualMatchCasePatterns() { - FormatterWorksFor(@" + public async Task FormatterWorksForUsualMatchCasePatterns() { + await FormatterWorksFor(@" method test() { match x { case 1 => Bring( @@ -337,7 +338,7 @@ [ 1 }; } ", reduceBlockiness: true); - FormatterWorksFor(@" + await FormatterWorksFor(@" method test() { var longName := match x { case 1 => World( @@ -359,7 +360,7 @@ [ 1 ", reduceBlockiness: false); } [Fact] - public void FormatterWorksForLabels() { + public async Task FormatterWorksForLabels() { var test = @" method BreakLabels(s: seq) requires |s| == 1000 @@ -432,7 +433,7 @@ method Test() { } } "; - FormatterWorksFor(test, test); + await FormatterWorksFor(test, test); } public FormatterForStatements([NotNull] ITestOutputHelper output) : base(output) { diff --git a/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs b/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs index d5429cfed98..e8b59b3c345 100644 --- a/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs +++ b/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs @@ -1,4 +1,5 @@ -using JetBrains.Annotations; +using System.Threading.Tasks; +using JetBrains.Annotations; using Xunit; using Xunit.Abstractions; @@ -7,8 +8,8 @@ namespace DafnyPipeline.Test; [Collection("Singleton Test Collection - FormatterForTopLevelDeclarations")] public class FormatterForTopLevelDeclarations : FormatterBaseTest { [Fact] - public void FormatterWorksForEmptyDocument() { - FormatterWorksFor(@" + public async Task FormatterWorksForEmptyDocument() { + await FormatterWorksFor(@" /* module S0 refines R { // This module defines a local g(). It takes precedence over the g() that @@ -23,8 +24,8 @@ function g(): int { 2 } } [Fact] - public void FormatWorksForSingleInclude() { - FormatterWorksFor(@" + public async Task FormatWorksForSingleInclude() { + await FormatterWorksFor(@" // RUN include ""git-issue48-include.dfyi"" @@ -32,8 +33,8 @@ public void FormatWorksForSingleInclude() { "); } [Fact] - public void FormatterWorksForMultipleModules() { - FormatterWorksFor(@" + public async Task FormatterWorksForMultipleModules() { + await FormatterWorksFor(@" module Outer.A { import B import C @@ -42,8 +43,8 @@ import C } [Fact] - public void FormatterWorksForIteratorRequiresComment() { - FormatterWorksFor(@" + public async Task FormatterWorksForIteratorRequiresComment() { + await FormatterWorksFor(@" iterator Iter(x: int) yields (y: int) requires A: 0 <= x // yield requires B: 0 <= y // not allowed; won't parse @@ -53,8 +54,8 @@ iterator Iter(x: int) yields (y: int) } [Fact] - public void FormatWorksForTypes() { - FormatterWorksFor(@" + public async Task FormatWorksForTypes() { + await FormatterWorksFor(@" type NoWitness_EffectlessArrow = f: A ~> B // error: cannot find witness | forall a :: f.reads(a) == {} @@ -82,8 +83,8 @@ witness 2 } [Fact] - public void FormatWorksForNewTypes() { - FormatterWorksFor(@" + public async Task FormatWorksForNewTypes() { + await FormatterWorksFor(@" newtype X = i : int | || i == 2 @@ -104,8 +105,8 @@ newtype Y } [Fact] - public void FormatWorksForModules() { - FormatterWorksFor(@" + public async Task FormatWorksForModules() { + await FormatterWorksFor(@" module AM { class A {} class B {} } @@ -183,8 +184,8 @@ function X(): int } [Fact] - public void FormatWorksForSimpleIterator() { - FormatterWorksFor(@" + public async Task FormatWorksForSimpleIterator() { + await FormatterWorksFor(@" iterator Gen(start: int) yields (x: int) yield ensures |xs| <= 10 && x == start + |xs| - 1 { @@ -198,8 +199,8 @@ iterator Gen(start: int) yields (x: int) "); } [Fact] - public void FormatterWorksForModules() { - FormatterWorksFor(@" + public async Task FormatterWorksForModules() { + await FormatterWorksFor(@" module Tests { class C { function F(c: C, d: D): bool { true } @@ -217,8 +218,8 @@ method M(x: int) } [Fact] - public void FormatterWorksForClassExtend() { - FormatterWorksFor(@" + public async Task FormatterWorksForClassExtend() { + await FormatterWorksFor(@" class A extends B< C< @@ -254,8 +255,8 @@ class W extends AA2, "); } [Fact] - public void FormatterWorksForAbstractModuleDecl() { - FormatterWorksFor(@" + public async Task FormatterWorksForAbstractModuleDecl() { + await FormatterWorksFor(@" abstract module C { export Body provides AF reveals g @@ -264,8 +265,8 @@ export Body provides AF reveals g "); } [Fact] - public void FormatterWorksForNewtypeWithMember() { - FormatterWorksFor(@" + public async Task FormatterWorksForNewtypeWithMember() { + await FormatterWorksFor(@" newtype Even = x : int | x % 2 == 0 { method {:timeLimitMultiplier 4} NewtypeTest(y:int) { @@ -283,8 +284,8 @@ type Opaque< } [Fact] - public void FormatterWorksForCppExample() { - FormatterWorksFor(@" + public async Task FormatterWorksForCppExample() { + await FormatterWorksFor(@" // RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp ExternDefs.h ""%s"" > ""%t"" // RUN: %diff ""%s.expect"" ""%t"" @@ -338,8 +339,8 @@ method Main() { } [Fact] - public void FormatterWorksForRefinedMethod() { - FormatterWorksFor(@" + public async Task FormatterWorksForRefinedMethod() { + await FormatterWorksFor(@" method M... { if ... {} diff --git a/Source/DafnyPipeline.Test/FormatterIssues.cs b/Source/DafnyPipeline.Test/FormatterIssues.cs index 18bad05f7c8..64d61409885 100644 --- a/Source/DafnyPipeline.Test/FormatterIssues.cs +++ b/Source/DafnyPipeline.Test/FormatterIssues.cs @@ -1,5 +1,6 @@ using System; using System.IO; +using System.Threading.Tasks; using JetBrains.Annotations; using Xunit; using Xunit.Abstractions; @@ -9,8 +10,8 @@ namespace DafnyPipeline.Test; [Collection("Singleton Test Collection - FormatterForTopLevelDeclarations")] public class FormatterIssues : FormatterBaseTest { [Fact] - public void GitIssue4269FormatLemmaIde() { - FormatterWorksFor(@" + public async Task GitIssue4269FormatLemmaIde() { + await FormatterWorksFor(@" module Foo { lemma Bar(t: string) { @@ -21,8 +22,8 @@ lemma Bar(t: string) } [Fact] - public void GitIssue4269BFormatMapIde() { - FormatterWorksFor(@" + public async Task GitIssue4269BFormatMapIde() { + await FormatterWorksFor(@" module Foo { method Bar( a: map, @@ -34,8 +35,8 @@ method Bar( } [Fact] - public void GitIssue3912FormatterCollectionArrow() { - FormatterWorksFor(@" + public async Task GitIssue3912FormatterCollectionArrow() { + await FormatterWorksFor(@" const i := a in B + // Previously it was not indented @@ -48,8 +49,8 @@ b in } [Fact] - public void GitIssue3912FormatterCollectionArrowA() { - FormatterWorksFor(@" + public async Task GitIssue3912FormatterCollectionArrowA() { + await FormatterWorksFor(@" const newline := set i <- @@ -75,8 +76,8 @@ set i <- } [Fact] - public void GitIssue3912FormatterCollectionArrowB() { - FormatterWorksFor(@" + public async Task GitIssue3912FormatterCollectionArrowB() { + await FormatterWorksFor(@" const newlineOp := set i @@ -94,8 +95,8 @@ public void GitIssue3912FormatterCollectionArrowB() { } [Fact] - public void GitIssue3912FormatterCollectionArrowC() { - FormatterWorksFor(@" + public async Task GitIssue3912FormatterCollectionArrowC() { + await FormatterWorksFor(@" const sameLineOp := set i <- @@ -111,8 +112,8 @@ set i } [Fact] - public void GitIssue3960FormattingIssueForallStatements() { - FormatterWorksFor(@" + public async Task GitIssue3960FormattingIssueForallStatements() { + await FormatterWorksFor(@" lemma Lemma() { forall pd0: int @@ -126,8 +127,8 @@ ensures true { } [Fact] - public void GitIssue3944FormatterArgumentsDefaultValue() { - FormatterWorksFor(@" + public async Task GitIssue3944FormatterArgumentsDefaultValue() { + await FormatterWorksFor(@" function Example( newNames : map := map[], a: int @@ -139,8 +140,8 @@ function Example( } [Fact] - public void GitIssue3790DafnyFormatterProducesIncorrectIndentation() { - FormatterWorksFor(@" + public async Task GitIssue3790DafnyFormatterProducesIncorrectIndentation() { + await FormatterWorksFor(@" lemma Try(i: int) { match i { @@ -152,8 +153,8 @@ match i { } [Fact] - public void FormatterWorksForEmptyDocument() { - FormatterWorksFor(@" + public async Task FormatterWorksForEmptyDocument() { + await FormatterWorksFor(@" ", null, true); } diff --git a/Source/DafnyPipeline.Test/ImplicitAssertionTest.cs b/Source/DafnyPipeline.Test/ImplicitAssertionTest.cs index dd9f7b7cc03..35f46ca15ff 100644 --- a/Source/DafnyPipeline.Test/ImplicitAssertionTest.cs +++ b/Source/DafnyPipeline.Test/ImplicitAssertionTest.cs @@ -2,6 +2,7 @@ using System.Collections.Generic; using System.IO; using System.Linq; +using System.Threading.Tasks; using Bpl = Microsoft.Boogie; using Xunit; using Microsoft.Dafny; @@ -14,8 +15,8 @@ namespace DafnyPipeline.Test; [Collection("Dafny implicit assertion test")] public class ImplicitAssertionTest { [Fact] - public void GitIssue4016ExplicitAssertionPrintNested() { - ShouldHaveImplicitCode(@" + public async Task GitIssue4016ExplicitAssertionPrintNested() { + await ShouldHaveImplicitCode(@" datatype D = C(value: int) | N function Test(e: D, inputs: map): bool { @@ -28,8 +29,8 @@ match e } [Fact] - public void DivisionByZero() { - ShouldHaveImplicitCode(@" + public async Task DivisionByZero() { + await ShouldHaveImplicitCode(@" method Test(x: int, y: int) returns (z: int) { z := 2 / (x + y); // Here } @@ -37,8 +38,8 @@ method Test(x: int, y: int) returns (z: int) { } [Fact] - public void CompilableAssignSuchThat() { - ShouldHaveImplicitCode(@" + public async Task CompilableAssignSuchThat() { + await ShouldHaveImplicitCode(@" predicate P(x: int, c: int) function Test(x: int, z: int): int @@ -51,8 +52,8 @@ requires P(x, z) && x <= z } [Fact] - public void AssignmentSuchThatShouldExist() { - ShouldHaveImplicitCode(@" + public async Task AssignmentSuchThatShouldExist() { + await ShouldHaveImplicitCode(@" predicate P(x: int) lemma PUnique(a: int) @@ -68,8 +69,8 @@ function Test(x: int): int } [Fact] - public void SeqIndexOutOfRange() { - ShouldHaveImplicitCode(@" + public async Task SeqIndexOutOfRange() { + await ShouldHaveImplicitCode(@" method Test(a: int -> seq, i: int) { var b := a(2)[i + 3]; // Here } @@ -77,8 +78,8 @@ method Test(a: int -> seq, i: int) { } [Fact] - public void SeqIndexOutOfRangeUpdate() { - ShouldHaveImplicitCode(@" + public async Task SeqIndexOutOfRangeUpdate() { + await ShouldHaveImplicitCode(@" method Test(a: int -> seq, i: int) { var b := a(2)[i + 3 := 1]; // Here } @@ -86,8 +87,8 @@ method Test(a: int -> seq, i: int) { } [Fact] - public void SeqSliceLowerOutOfRange() { - ShouldHaveImplicitCode(@" + public async Task SeqSliceLowerOutOfRange() { + await ShouldHaveImplicitCode(@" method Test(a: int -> seq, i: int) { var b := a(2)[i + 3..]; // Here } @@ -95,8 +96,8 @@ method Test(a: int -> seq, i: int) { } [Fact] - public void SeqUpperOutOfRange() { - ShouldHaveImplicitCode(@" + public async Task SeqUpperOutOfRange() { + await ShouldHaveImplicitCode(@" method Test(a: int -> seq, i: int, j: int) { var b := a(2)[j..i + 3]; // Here } @@ -104,8 +105,8 @@ method Test(a: int -> seq, i: int, j: int) { } [Fact] - public void ArrayIndexOutOfRange() { - ShouldHaveImplicitCode(@" + public async Task ArrayIndexOutOfRange() { + await ShouldHaveImplicitCode(@" method Test(a: int -> array, i: int) { var b := a(2)[i + 3]; // Here } @@ -113,8 +114,8 @@ method Test(a: int -> array, i: int) { } [Fact] - public void ArrayIndex0OutOfRange() { - ShouldHaveImplicitCode(@" + public async Task ArrayIndex0OutOfRange() { + await ShouldHaveImplicitCode(@" method Test(a: int -> array2, i: int) { var b := a(2)[i + 3, i + 4]; // Here } @@ -122,8 +123,8 @@ method Test(a: int -> array2, i: int) { } [Fact] - public void ArrayIndex1OutOfRange() { - ShouldHaveImplicitCode(@" + public async Task ArrayIndex1OutOfRange() { + await ShouldHaveImplicitCode(@" method Test(a: int -> array2, i: int) { var b := a(2)[i + 3, i + 4]; // Here } @@ -131,8 +132,8 @@ method Test(a: int -> array2, i: int) { } [Fact] - public void ElementNotInDomain() { - ShouldHaveImplicitCode(@" + public async Task ElementNotInDomain() { + await ShouldHaveImplicitCode(@" method Test(m: map, x: int) { var b := m[x + 2]; // Here } @@ -141,7 +142,7 @@ method Test(m: map, x: int) { /** Look at the line containing "// Here", and for every assertion there, look if they contain an implicit assertion that, if printed, would generate the string "expected" */ - private void ShouldHaveImplicitCode(string program, string expected, DafnyOptions options = null) { + private async Task ShouldHaveImplicitCode(string program, string expected, DafnyOptions options = null) { if (program.IndexOf("// Here", StringComparison.Ordinal) == -1) { Assert.Fail("Test is missing // Here"); } @@ -150,7 +151,7 @@ private void ShouldHaveImplicitCode(string program, string expected, DafnyOption options = options ?? new DafnyOptions(TextReader.Null, TextWriter.Null, TextWriter.Null); var uri = new Uri("virtual:///virtual"); BatchErrorReporter reporter = new BatchErrorReporter(options); - var dafnyProgram = new ProgramParser().Parse(program, uri, reporter); + var dafnyProgram = await new ProgramParser().Parse(program, uri, reporter); if (reporter.HasErrors) { var error = reporter.AllMessagesByLevel[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); diff --git a/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs b/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs index f5181c6dd86..100572a982c 100644 --- a/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs +++ b/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs @@ -150,16 +150,16 @@ public IntraMethodVerificationStability(ITestOutputHelper testOutputHelper) { } [Fact] - public void NoUniqueLinesWhenConcatenatingUnrelatedPrograms() { + public async Task NoUniqueLinesWhenConcatenatingUnrelatedPrograms() { var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(testOutputHelper)); Regex idAttributeRegex = new Regex("{:id \".*\"}"); - var regularBoogie = GetBoogie(options, originalProgram).ToList(); - var renamedBoogie = GetBoogie(options, renamedProgram).ToList(); + var regularBoogie = await GetBoogie(options, originalProgram); + var renamedBoogie = await GetBoogie(options, renamedProgram); var regularBoogieText = idAttributeRegex.Replace(GetBoogieText(options, regularBoogie), ""); var renamedBoogieText = idAttributeRegex.Replace(GetBoogieText(options, renamedBoogie), ""); var separate = UniqueNonCommentLines(regularBoogieText + renamedBoogieText); - var combinedBoogie = idAttributeRegex.Replace(GetBoogieText(options, GetBoogie(options, originalProgram + renamedProgram)), ""); + var combinedBoogie = idAttributeRegex.Replace(GetBoogieText(options, await GetBoogie(options, originalProgram + renamedProgram)), ""); var together = UniqueNonCommentLines(combinedBoogie); var uniqueLines = separate.Union(together).Except(separate.Intersect(together)).ToList(); @@ -171,8 +171,8 @@ public async Task EqualProverLogWhenReorderingProgram() { var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(testOutputHelper)); options.ProcsToCheck.Add("SomeMethod*"); - var reorderedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, reorderedProgram)); - var regularProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, originalProgram)); + var reorderedProverLog = await GetProverLogForProgramAsync(options, await GetBoogie(options, reorderedProgram)); + var regularProverLog = await GetProverLogForProgramAsync(options, await GetBoogie(options, originalProgram)); Assert.Equal(regularProverLog, reorderedProverLog); } @@ -181,8 +181,8 @@ public async Task EqualProverLogWhenRenamingProgram() { var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(testOutputHelper)); options.ProcsToCheck.Add("*SomeMethod*"); - var renamedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, renamedProgram)); - var regularProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, originalProgram)); + var renamedProverLog = await GetProverLogForProgramAsync(options, await GetBoogie(options, renamedProgram)); + var regularProverLog = await GetProverLogForProgramAsync(options, await GetBoogie(options, originalProgram)); Assert.Equal(regularProverLog, renamedProverLog); } @@ -192,8 +192,8 @@ public async Task EqualProverLogWhenAddingUnrelatedProgram() { var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(testOutputHelper)); options.ProcsToCheck.Add("*SomeMethod *"); - var renamedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, renamedProgram + originalProgram)); - var regularProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, originalProgram)); + var renamedProverLog = await GetProverLogForProgramAsync(options, await GetBoogie(options, renamedProgram + originalProgram)); + var regularProverLog = await GetProverLogForProgramAsync(options, await GetBoogie(options, originalProgram)); Assert.Equal(regularProverLog, renamedProverLog); } @@ -238,9 +238,9 @@ string GetBoogieText(CoreOptions options, IEnumerable boogieProgr return string.Join('\n', boogieProgram.Select(x => PrintBoogie(options, x))); } - IEnumerable GetBoogie(DafnyOptions options, string dafnyProgramText) { + async Task> GetBoogie(DafnyOptions options, string dafnyProgramText) { var reporter = new BatchErrorReporter(options); - var dafnyProgram = Utils.Parse(reporter, dafnyProgramText, false); + var dafnyProgram = await Utils.Parse(reporter, dafnyProgramText, false); Assert.NotNull(dafnyProgram); DafnyMain.Resolve(dafnyProgram); Assert.Equal(0, reporter.ErrorCount); diff --git a/Source/DafnyPipeline.Test/Issue1355.cs b/Source/DafnyPipeline.Test/Issue1355.cs index 21fe7394386..e5e8c7f4c91 100644 --- a/Source/DafnyPipeline.Test/Issue1355.cs +++ b/Source/DafnyPipeline.Test/Issue1355.cs @@ -1,4 +1,5 @@ using System.IO; +using System.Threading.Tasks; using DafnyCore.Test; using DafnyTestGeneration; using Bpl = Microsoft.Boogie; @@ -19,12 +20,12 @@ public Issue1355(ITestOutputHelper output) { } [Fact] - public void Test() { + public async Task Test() { var options = DafnyOptions.Create(output); options.DafnyPrelude = "../../../../../Binaries/DafnyPrelude.bpl"; var programString = @"trait Trait { }"; - var dafnyProgram = Utils.Parse(new BatchErrorReporter(options), programString, false); + var dafnyProgram = await Utils.Parse(new BatchErrorReporter(options), programString, false); DafnyMain.Resolve(dafnyProgram); foreach (var prog in BoogieGenerator.Translate(dafnyProgram, dafnyProgram.Reporter)) { var writer = new StringWriter(); diff --git a/Source/DafnyPipeline.Test/PluginsTest.cs b/Source/DafnyPipeline.Test/PluginsTest.cs index f2ff51f1ac2..2b2d10703cd 100644 --- a/Source/DafnyPipeline.Test/PluginsTest.cs +++ b/Source/DafnyPipeline.Test/PluginsTest.cs @@ -2,6 +2,7 @@ using System.IO; using System.Linq; using System.Reflection; +using System.Threading.Tasks; using DafnyCore.Test; using DafnyTestGeneration; using Microsoft.CodeAnalysis; @@ -55,7 +56,7 @@ private string GetLibrary(string name) { } [Fact] - public void EnsurePluginIsExecuted() { + public async Task EnsurePluginIsExecuted() { var library = GetLibrary("rewriterPreventingVerificationWithArgument"); var options = DafnyOptions.Create(output); @@ -63,7 +64,7 @@ public void EnsurePluginIsExecuted() { var programString = "function test(): int { 1 }"; var reporter = new BatchErrorReporter(options); - var dafnyProgram = Utils.Parse(reporter, programString, false); + var dafnyProgram = await Utils.Parse(reporter, programString, false); DafnyMain.Resolve(dafnyProgram); Assert.Equal(1, reporter.Count(ErrorLevel.Error)); @@ -71,7 +72,7 @@ public void EnsurePluginIsExecuted() { } [Fact] - public void EnsurePluginIsExecutedEvenWithoutConfiguration() { + public async Task EnsurePluginIsExecutedEvenWithoutConfiguration() { var library = GetLibrary("rewriterPreventingVerification"); var options = DafnyOptions.Create(output); @@ -79,14 +80,14 @@ public void EnsurePluginIsExecutedEvenWithoutConfiguration() { var programString = "function test(): int { 1 }"; var reporter = new BatchErrorReporter(options); - var dafnyProgram = Utils.Parse(reporter, programString, false); + var dafnyProgram = await Utils.Parse(reporter, programString, false); DafnyMain.Resolve(dafnyProgram); Assert.Equal(1, reporter.ErrorCount); Assert.Equal("Impossible to continue", reporter.AllMessagesByLevel[ErrorLevel.Error][0].Message); } [Fact] - public void EnsurePluginIsExecutedAndAllowsVerification() { + public async Task EnsurePluginIsExecutedAndAllowsVerification() { var library = GetLibrary("rewriterAllowingVerification"); var options = DafnyOptions.Create(output); @@ -94,7 +95,7 @@ public void EnsurePluginIsExecutedAndAllowsVerification() { var programString = "function test(): int { 1 }"; var reporter = new BatchErrorReporter(options); - var dafnyProgram = Utils.Parse(reporter, programString, false); + var dafnyProgram = await Utils.Parse(reporter, programString, false); DafnyMain.Resolve(dafnyProgram); Assert.Equal(0, reporter.ErrorCountUntilResolver); Assert.Equal(1, reporter.ErrorCount); diff --git a/Source/DafnyPipeline.Test/ProverLogStability.cs b/Source/DafnyPipeline.Test/ProverLogStability.cs index b2f3ae56d14..f56369a0150 100644 --- a/Source/DafnyPipeline.Test/ProverLogStability.cs +++ b/Source/DafnyPipeline.Test/ProverLogStability.cs @@ -116,7 +116,7 @@ public async Task ProverLogRegression() { var filePath = Path.Combine(Directory.GetCurrentDirectory(), "expectedProverLog.smt2"); var expectation = await File.ReadAllTextAsync(filePath); expectation = expectation.Replace("\r", ""); - var regularProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, originalProgram)); + var regularProverLog = await GetProverLogForProgramAsync(options, await GetBoogie(options, originalProgram)); regularProverLog = regularProverLog.Replace("\r", ""); if (updateProverLog) { var path = Path.GetFullPath(filePath).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net6.0" + Path.DirectorySeparatorChar, ""); @@ -151,9 +151,9 @@ private async IAsyncEnumerable GetProverLogsForProgramAsync(DafnyOptions } } - IEnumerable GetBoogie(DafnyOptions options, string dafnyProgramText) { + async Task> GetBoogie(DafnyOptions options, string dafnyProgramText) { var reporter = new BatchErrorReporter(options); - var dafnyProgram = Utils.Parse(reporter, dafnyProgramText, false); + var dafnyProgram = await Utils.Parse(reporter, dafnyProgramText, false); Assert.NotNull(dafnyProgram); DafnyMain.Resolve(dafnyProgram); Assert.Equal(0, reporter.ErrorCount); diff --git a/Source/DafnyPipeline.Test/Trivia.cs b/Source/DafnyPipeline.Test/Trivia.cs index 2d641ddff7f..735198cec5d 100644 --- a/Source/DafnyPipeline.Test/Trivia.cs +++ b/Source/DafnyPipeline.Test/Trivia.cs @@ -3,6 +3,7 @@ using System.IO; using System.Linq; using System.Text.RegularExpressions; +using System.Threading.Tasks; using DafnyCore.Test; using DafnyTestGeneration; using Bpl = Microsoft.Boogie; @@ -26,7 +27,7 @@ enum Newlines { LF, CR, CRLF }; private Newlines currentNewlines; [Fact] - public void TriviaSplitWorksOnLinuxMacAndWindows() { + public async Task TriviaSplitWorksOnLinuxMacAndWindows() { var options = DafnyOptions.Create(output); foreach (Newlines newLinesType in Enum.GetValues(typeof(Newlines))) { currentNewlines = newLinesType; @@ -80,7 +81,7 @@ ensures true programString = AdjustNewlines(programString); var reporter = new BatchErrorReporter(options); - var dafnyProgram = Utils.Parse(reporter, programString, false); + var dafnyProgram = await Utils.Parse(reporter, programString, false); Assert.Equal(0, reporter.ErrorCount); var topLevelDecls = dafnyProgram.DefaultModuleDef.TopLevelDecls.ToList(); Assert.Equal(6, topLevelDecls.Count()); diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index cbeaef2d0d6..0dae8e20a00 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -9,10 +9,9 @@ using System.Runtime.Serialization.Json; using System.Text; using System.Threading; +using System.Threading.Tasks; using Microsoft.Boogie; using DafnyServer; -using Microsoft.Extensions.Logging; -using Microsoft.Extensions.Logging.Abstractions; using Bpl = Microsoft.Boogie; namespace Microsoft.Dafny { @@ -37,17 +36,17 @@ public DafnyHelper(DafnyOptions options, ExecutionEngine engine, string[] args, this.source = source; } - public bool Verify() { + public async Task Verify() { ServerUtils.ApplyArgs(args, options); - return Parse() && Resolve() && Translate() && Boogie(); + return await Parse() && Resolve() && Translate() && Boogie(); } - private bool Parse() { + private async Task Parse() { var uri = new Uri("transcript:///" + fname); reporter = new ConsoleErrorReporter(options); var fs = new InMemoryFileSystem(ImmutableDictionary.Empty.Add(uri, source)); - var file = DafnyFile.CreateAndValidate(reporter, fs, reporter.Options, uri, Token.NoToken); - var program = new ProgramParser().ParseFiles(fname, file == null ? Array.Empty() : new[] { file }, + var file = await DafnyFile.CreateAndValidate(reporter, fs, reporter.Options, uri, Token.NoToken); + var program = await new ProgramParser().ParseFiles(fname, file == null ? Array.Empty() : new[] { file }, reporter, CancellationToken.None); var success = !reporter.HasErrors; @@ -98,32 +97,32 @@ private bool Boogie() { return isVerified; } - public void Symbols() { + public async Task Symbols() { ServerUtils.ApplyArgs(args, options); - if (Parse() && Resolve()) { + if (await Parse() && Resolve()) { var symbolTable = new SuperLegacySymbolTable(dafnyProgram); var symbols = symbolTable.CalculateSymbols(); - options.OutputWriter.WriteLine("SYMBOLS_START " + ConvertToJson(symbols) + " SYMBOLS_END"); + await options.OutputWriter.WriteLineAsync("SYMBOLS_START " + ConvertToJson(symbols) + " SYMBOLS_END"); } else { - options.OutputWriter.WriteLine("SYMBOLS_START [] SYMBOLS_END"); + await options.OutputWriter.WriteLineAsync("SYMBOLS_START [] SYMBOLS_END"); } } - public void CounterExample() { + public async Task CounterExample() { var listArgs = args.ToList(); listArgs.Add("/mv:" + counterExampleProvider.ModelBvd); ServerUtils.ApplyArgs(listArgs.ToArray(), options); try { - if (Parse() && Resolve() && Translate()) { + if (await Parse() && Resolve() && Translate()) { foreach (var boogieProgram in boogiePrograms) { RemoveExistingModel(); BoogieOnce(boogieProgram.Item1, boogieProgram.Item2); var model = counterExampleProvider.LoadCounterModel(options); - options.OutputWriter.WriteLine("COUNTEREXAMPLE_START " + ConvertToJson(model) + " COUNTEREXAMPLE_END"); + await options.OutputWriter.WriteLineAsync("COUNTEREXAMPLE_START " + ConvertToJson(model) + " COUNTEREXAMPLE_END"); } } } catch (Exception e) { - options.OutputWriter.WriteLine("Error collection models: " + e.Message); + await options.OutputWriter.WriteLineAsync("Error collection models: " + e.Message); } } @@ -133,17 +132,16 @@ private void RemoveExistingModel() { } } - public void DotGraph() { + public async Task DotGraph() { ServerUtils.ApplyArgs(args, options); - if (Parse() && Resolve() && Translate()) { + if (await Parse() && Resolve() && Translate()) { foreach (var boogieProgram in boogiePrograms) { BoogieOnce(boogieProgram.Item1, boogieProgram.Item2); foreach (var impl in boogieProgram.Item2.Implementations) { - using (StreamWriter sw = new StreamWriter(fname + impl.Name + ".dot")) { - sw.Write(boogieProgram.Item2.ProcessLoops(engine.Options, impl).ToDot()); - } + await using var sw = new StreamWriter(fname + impl.Name + ".dot"); + await sw.WriteAsync(boogieProgram.Item2.ProcessLoops(engine.Options, impl).ToDot()); } } } diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index c47582e933f..1b02d5c8e47 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -15,8 +15,8 @@ public class Server : IDisposable { private readonly TextReader input; private readonly TextWriter outputWriter; - public static void Main(string[] args) { - _ = MainWithWriters(Console.Out, Console.Error, Console.In, args); + public static Task Main(string[] args) { + return MainWithWriters(Console.Out, Console.Error, Console.In, args); } public static async Task MainWithWriters(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, string[] args) { @@ -50,7 +50,7 @@ public static async Task MainWithWriters(TextWriter outputWriter, TextWrite } if (selftest) { - VerificationTask.SelfTest(options, engine); + await VerificationTask.SelfTest(options, engine); return 0; } @@ -70,7 +70,7 @@ public static async Task MainWithWriters(TextWriter outputWriter, TextWrite } else if (encode) { server.Encode(); } else { - server.Loop(options, plaintext); + await server.Loop(options, plaintext); } return 0; } @@ -95,8 +95,7 @@ bool EndOfPayload(out string line) { string ReadPayload(bool inputIsPlaintext) { StringBuilder buffer = new StringBuilder(); - string line = null; - while (!EndOfPayload(out line)) { + while (!EndOfPayload(out var line)) { buffer.Append(line); if (inputIsPlaintext) { buffer.Append("\n"); @@ -166,17 +165,17 @@ void WriteAcrossLines(string s, int width) { } } - void Loop(DafnyOptions options, bool inputIsPlaintext) { + async Task Loop(DafnyOptions options, bool inputIsPlaintext) { for (int cycle = 0; running; cycle++) { - var line = input.ReadLine() ?? "quit"; + var line = await input.ReadLineAsync() ?? "quit"; if (line != String.Empty && !line.StartsWith("#")) { var command = line.Split(); - Respond(options, command, inputIsPlaintext); + await Respond(options, command, inputIsPlaintext); } } } - void Respond(DafnyOptions options, string[] command, bool inputIsPlaintext) { + async Task Respond(DafnyOptions options, string[] command, bool inputIsPlaintext) { try { if (command.Length == 0) { throw new ServerException("Empty command"); @@ -187,19 +186,19 @@ void Respond(DafnyOptions options, string[] command, bool inputIsPlaintext) { if (verb == "verify") { ServerUtils.checkArgs(command, 0); var vt = ReadVerificationTask(inputIsPlaintext); - vt.Run(options, engine); + await vt.Run(options, engine); } else if (verb == "counterexample") { ServerUtils.checkArgs(command, 0); var vt = ReadVerificationTask(inputIsPlaintext); - vt.CounterExample(options, engine); + await vt.CounterExample(options, engine); } else if (verb == "dotgraph") { ServerUtils.checkArgs(command, 0); var vt = ReadVerificationTask(inputIsPlaintext); - vt.DotGraph(options, engine); + await vt.DotGraph(options, engine); } else if (verb == "symbols") { ServerUtils.checkArgs(command, 0); var vt = ReadVerificationTask(inputIsPlaintext); - vt.Symbols(options, engine); + await vt.Symbols(options, engine); } else if (verb == "version") { ServerUtils.checkArgs(command, 0); var _ = ReadVerificationTask(inputIsPlaintext); diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs index 611ae8ea7dc..e3cfeed4e87 100644 --- a/Source/DafnyServer/VerificationTask.cs +++ b/Source/DafnyServer/VerificationTask.cs @@ -6,6 +6,7 @@ using System.Runtime.Serialization; using System.Runtime.Serialization.Json; using System.Text; +using System.Threading.Tasks; using Microsoft.Boogie; namespace Microsoft.Dafny { @@ -45,30 +46,30 @@ internal static VerificationTask ReadTask(string b64Repr) { } } - internal static void SelfTest(DafnyOptions options, ExecutionEngine engine) { + internal static async Task SelfTest(DafnyOptions options, ExecutionEngine engine) { var task = new VerificationTask(new string[] { }, "", "method selftest() { assert true; }", false); try { - task.Run(options, engine); + await task.Run(options, engine); Interaction.Eom(options.OutputWriter, Interaction.SUCCESS, (string)null); } catch (Exception ex) { Interaction.Eom(options.OutputWriter, Interaction.FAILURE, ex); } } - internal void Run(DafnyOptions options, ExecutionEngine engine) { - new DafnyHelper(options, engine, args, filename, ProgramSource).Verify(); + internal Task Run(DafnyOptions options, ExecutionEngine engine) { + return new DafnyHelper(options, engine, args, filename, ProgramSource).Verify(); } - internal void Symbols(DafnyOptions options, ExecutionEngine engine) { - new DafnyHelper(options, engine, args, filename, ProgramSource).Symbols(); + internal Task Symbols(DafnyOptions options, ExecutionEngine engine) { + return new DafnyHelper(options, engine, args, filename, ProgramSource).Symbols(); } - public void CounterExample(DafnyOptions options, ExecutionEngine engine) { - new DafnyHelper(options, engine, args, filename, ProgramSource).CounterExample(); + public Task CounterExample(DafnyOptions options, ExecutionEngine engine) { + return new DafnyHelper(options, engine, args, filename, ProgramSource).CounterExample(); } - public void DotGraph(DafnyOptions options, ExecutionEngine engine) { - new DafnyHelper(options, engine, args, filename, ProgramSource).DotGraph(); + public Task DotGraph(DafnyOptions options, ExecutionEngine engine) { + return new DafnyHelper(options, engine, args, filename, ProgramSource).DotGraph(); } public string EncodeProgram(out string json) { diff --git a/Source/DafnyTestGeneration.Test/BasicTypes.cs b/Source/DafnyTestGeneration.Test/BasicTypes.cs index 11d80d063eb..57526d71c92 100644 --- a/Source/DafnyTestGeneration.Test/BasicTypes.cs +++ b/Source/DafnyTestGeneration.Test/BasicTypes.cs @@ -37,7 +37,7 @@ module SimpleTest { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(3 <= methods.Count); Assert.True(methods.All(m => @@ -67,7 +67,7 @@ module SimpleTest { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(2 <= methods.Count); Assert.True(methods.All(m => m.MethodName == "SimpleTest.checkIfTrue")); @@ -103,7 +103,7 @@ module SimpleTest { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(7 <= methods.Count); Assert.True( @@ -138,7 +138,7 @@ module SimpleTest { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(3 <= methods.Count); Assert.True( @@ -171,7 +171,7 @@ module SimpleTest { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(3 <= methods.Count); Assert.True(methods.All(m => m.MethodName == "SimpleTest.compareToB")); @@ -204,7 +204,7 @@ module SimpleTest { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(2 <= methods.Count); Assert.True(methods.All(m => m.MethodName == "SimpleTest.compareToB")); diff --git a/Source/DafnyTestGeneration.Test/Collections.cs b/Source/DafnyTestGeneration.Test/Collections.cs index 740010a0b07..dcbbf8288b6 100644 --- a/Source/DafnyTestGeneration.Test/Collections.cs +++ b/Source/DafnyTestGeneration.Test/Collections.cs @@ -40,7 +40,7 @@ module SimpleTest { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(3 <= methods.Count); Assert.True(methods.All(m => @@ -84,7 +84,7 @@ module C { ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(3 <= methods.Count); Assert.True(methods.All(m => diff --git a/Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs b/Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs index 9ee5ad8db65..fe691ad482b 100644 --- a/Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs +++ b/Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs @@ -7,6 +7,7 @@ using System.IO; using System.Linq; using System.Text.RegularExpressions; +using System.Threading.Tasks; using DafnyCore.Test; using DafnyTestGeneration.Inlining; using Microsoft.Dafny; @@ -30,11 +31,11 @@ private static string RemoveSpaces(string input) { /// /// Perform shared checks and return the target method for further testing on a case by case basis /// - private Method ShortCircuitRemovalTest(string source, string expected, bool isByMethod = true) { + private async Task ShortCircuitRemovalTest(string source, string expected, bool isByMethod = true) { // If the following assertion fails, rename the corresponding variables in expected output of each test Assert.Equal(RemoveShortCircuitingRewriter.TmpVarPrefix, "#tmp"); var options = GetDafnyOptions(new List>(), output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var success = InliningTranslator.TranslateForFutureInlining(program, options, out var boogieProgram); Assert.True(success); var method = program.DefaultModuleDef.Children @@ -53,18 +54,18 @@ private Method ShortCircuitRemovalTest(string source, string expected, bool isBy } [Fact] - public void FunctionToFunctionByMethod() { + public async Task FunctionToFunctionByMethod() { var source = @" function {:testEntry} Identity(i:int):int { i } ".TrimStart(); var expected = "{ return i; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void And() { + public async Task And() { var source = @" predicate {:testEntry} And(a:bool, b:bool) { a && b @@ -80,11 +81,11 @@ public void And() { #tmp0 := #tmp0; return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void Or() { + public async Task Or() { var source = @" predicate {:testEntry} Or(a:bool, b:bool) { a || b @@ -100,11 +101,11 @@ public void Or() { #tmp0 := #tmp0; return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void Imp() { + public async Task Imp() { var source = @" predicate {:testEntry} Imp(a:bool, b:bool) { a ==> b @@ -121,11 +122,11 @@ public void Imp() { #tmp0 := true; return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void Exp() { + public async Task Exp() { var source = @" predicate {:testEntry} Exp(a:bool, b:bool) { a <== b @@ -141,11 +142,11 @@ public void Exp() { #tmp0 := true; return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void IfThenElse() { + public async Task IfThenElse() { var source = @" function {:testEntry} IfThenElse(a:bool):int { if a then 1 else 2 @@ -160,11 +161,11 @@ public void IfThenElse() { #tmp0 := 2; return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void Let() { + public async Task Let() { var source = @" function {:testEntry} Let(a:bool):int { var a:int := 7; a @@ -179,11 +180,11 @@ public void Let() { } return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void NestedLet() { + public async Task NestedLet() { var source = @" function {:testEntry} NestedLet(a:bool):int { var a:real := 7.5; var a:int := 4; a @@ -202,11 +203,11 @@ public void NestedLet() { #tmp0 := #tmp1; } return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void IfInsideLet() { + public async Task IfInsideLet() { var source = @" function {:testEntry} Let(a:bool):int { var a := false; if a then 5 else 7 @@ -226,11 +227,11 @@ public void IfInsideLet() { } return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void InElseBranch() { + public async Task InElseBranch() { var source = @" function {:testEntry} NestedIfTheElse(a:bool, b:bool):int { if a then 5 else if b then 3 else 1 @@ -251,11 +252,11 @@ public void InElseBranch() { } return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void StmtExpression() { + public async Task StmtExpression() { var source = @" function {:testEntry} StmtExpression(a:int):int { if (var a := true; a) then 5 else 3 @@ -272,11 +273,11 @@ public void StmtExpression() { #tmp0 := 3; return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void Match() { + public async Task Match() { var source = @" datatype Option = None | Some function {:testEntry} IsNone(o: Option): bool { @@ -293,11 +294,11 @@ match o case {:split false} Some() => #tmp0 := false; return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void MatchWithDestructors() { + public async Task MatchWithDestructors() { var source = @" datatype Option = None | Some(val:int) function {:testEntry} UnBoxOrZero(o: Option): int { @@ -314,11 +315,11 @@ match o case {:split false} Some(r) => #tmp0 := r; return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void FunctionCall() { + public async Task FunctionCall() { var source = @" function {:testEntry} Max(a:int, b:int):int { -Min(-a, -b) @@ -331,11 +332,11 @@ public void FunctionCall() { #tmp0 := Min(-a, -b); return -#tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void NestedFunctionCall() { + public async Task NestedFunctionCall() { var source = @" function {:testEntry} Max(a:int, b:int):int { Negate(Min(Negate(a), Negate(b))) @@ -355,11 +356,11 @@ function Negate(a:int):int { -a } #tmp0 := Negate(#tmp1); return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void FunctionCallWithShortCircuitingArgs() { + public async Task FunctionCallWithShortCircuitingArgs() { var source = @" function {:testEntry} Arguments(a:bool, b:bool):bool { IsTrue(a || b) @@ -378,11 +379,11 @@ function IsTrue(a:bool):bool { a } #tmp0 := IsTrue(#tmp1); return #tmp0; }"; - ShortCircuitRemovalTest(source, expected); + await ShortCircuitRemovalTest(source, expected); } [Fact] - public void Constructor() { + public async Task Constructor() { var source = @" class C { var i:int @@ -409,11 +410,11 @@ class C { #tmp1 := 1; i := #tmp1; }"; - ShortCircuitRemovalTest(source, expected, isByMethod: false); + await ShortCircuitRemovalTest(source, expected, isByMethod: false); } [Fact] - public void While() { + public async Task While() { var source = @" method {:testEntry} Sum(n:int) returns (s:int) requires n >= 0 @@ -444,11 +445,11 @@ decreases n-i } return s; }"; - ShortCircuitRemovalTest(source, expected, false); + await ShortCircuitRemovalTest(source, expected, false); } [Fact] - public void LetOrFail() { + public async Task LetOrFail() { var source = @" datatype Result = Success(value:T) | Failure { predicate IsFailure() {true} @@ -468,7 +469,7 @@ function PropagateFailure():Result {this} } return #tmp0; }"; - var resultingMethod = ShortCircuitRemovalTest(source, expected); + var resultingMethod = await ShortCircuitRemovalTest(source, expected); Assert.True(resultingMethod.Body.Body[1] is BlockStmt); var blockStmt = resultingMethod.Body.Body[1] as BlockStmt; Assert.True(blockStmt.Body[0] is AssignOrReturnStmt); @@ -479,7 +480,7 @@ function PropagateFailure():Result {this} } [Fact] - public void LetOrFailWithAssignment() { + public async Task LetOrFailWithAssignment() { var source = @" datatype Result = Success(value:T) | Failure { predicate IsFailure() {true} @@ -500,7 +501,7 @@ function Extract():T requires !IsFailure() {value} } return #tmp0; }"; - var resultingMethod = ShortCircuitRemovalTest(source, expected); + var resultingMethod = await ShortCircuitRemovalTest(source, expected); Assert.True(resultingMethod.Body.Body[1] is BlockStmt); var blockStmt = resultingMethod.Body.Body[1] as BlockStmt; Assert.True(blockStmt.Body[0] is VarDeclStmt); @@ -511,7 +512,7 @@ function Extract():T requires !IsFailure() {value} } [Fact] - public void TypeRhs() { + public async Task TypeRhs() { var source = @" class A { constructor () {} @@ -524,11 +525,11 @@ class A { { var a := new A(); }"; - ShortCircuitRemovalTest(source, expected, false); + await ShortCircuitRemovalTest(source, expected, false); } [Fact] - public void Print() { + public async Task Print() { var source = @" method {:testEntry} Print(b:bool) { print if b then ['a', 'b', 'c'] else []; @@ -543,11 +544,11 @@ public void Print() { #tmp0 := []; print #tmp0; }"; - ShortCircuitRemovalTest(source, expected, false); + await ShortCircuitRemovalTest(source, expected, false); } [Fact] - public void ForLoop() { + public async Task ForLoop() { var source = @" method {:testEntry} Sum(n:int) returns (s:int) requires n >= 0 @@ -569,11 +570,11 @@ public void ForLoop() { } return s; }"; - ShortCircuitRemovalTest(source, expected, false); + await ShortCircuitRemovalTest(source, expected, false); } [Fact] - public void CallStmt() { + public async Task CallStmt() { var source = @" method callee(a:int) {} method {:testEntry} caller() { @@ -589,11 +590,11 @@ method callee(a:int) {} #tmp0 := 1; callee(#tmp0); }"; - ShortCircuitRemovalTest(source, expected, false); + await ShortCircuitRemovalTest(source, expected, false); } [Fact] - public void CallStmtWithUpdate() { + public async Task CallStmtWithUpdate() { var source = @" method callee(a:int) returns (i:int) { return a; } method {:testEntry} caller() { @@ -609,7 +610,7 @@ public void CallStmtWithUpdate() { #tmp0 := 1; var x := callee(#tmp0); }"; - ShortCircuitRemovalTest(source, expected, false); + await ShortCircuitRemovalTest(source, expected, false); } } diff --git a/Source/DafnyTestGeneration.Test/Various.cs b/Source/DafnyTestGeneration.Test/Various.cs index fd06e74a925..e502d0b1275 100644 --- a/Source/DafnyTestGeneration.Test/Various.cs +++ b/Source/DafnyTestGeneration.Test/Various.cs @@ -40,7 +40,7 @@ module M { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(3 <= methods.Count); Assert.True(2 <= methods.Count(m => m.MethodName == "M.b")); @@ -73,7 +73,7 @@ module M { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(methods.Count >= 2); Assert.True(methods.All(m => m.MethodName == "M.a")); @@ -102,7 +102,7 @@ module M { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(methods.Count >= 2); } @@ -124,7 +124,7 @@ function max (a:int, b:int):int { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.Single(methods); } @@ -143,7 +143,7 @@ module M { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(2 <= methods.Count); } @@ -170,7 +170,7 @@ decreases n } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(methods.Count >= 3); } @@ -197,7 +197,7 @@ decreases n } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(methods.Count < 3); } @@ -220,7 +220,7 @@ module Paths { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); options.TestGenOptions.Mode = TestGenerationOptions.Modes.Path; var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); @@ -261,7 +261,7 @@ module Paths { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); options.TestGenOptions.Mode = TestGenerationOptions.Modes.InlinedBlock; var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); @@ -300,7 +300,7 @@ module Paths { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(methods.Count is >= 1 and <= 2); Assert.True(methods.All(m => m.MethodName == "Paths.eightPaths")); @@ -343,7 +343,7 @@ class List { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(methods.Count >= 5); Assert.True(methods.All(m => @@ -408,7 +408,7 @@ class LoopingList { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.Single(methods); } @@ -433,7 +433,7 @@ class List { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(3 <= methods.Count); Assert.True(methods.All(m => @@ -470,7 +470,7 @@ class Value { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.Single(methods); var m = methods[0]; @@ -497,7 +497,7 @@ requires a > 0 } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); options.TestGenOptions.WarnDeadCode = true; var stats = await TestGenerator.GetDeadCodeStatistics(program, new Modifications(options)).ToListAsync(); Assert.Contains(stats, s => s.Contains("(6,14) is potentially unreachable.")); @@ -551,7 +551,7 @@ public async Task NoDeadCode(List> optionSettings) { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); options.TestGenOptions.WarnDeadCode = true; var stats = await TestGenerator.GetDeadCodeStatistics(program, new Modifications(options)).ToListAsync(); Assert.Single(stats); // the only line with stats @@ -573,7 +573,7 @@ module Test { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); options.TestGenOptions.SeqLengthLimit = 1; var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(2 <= methods.Count); @@ -601,7 +601,7 @@ module Math { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(2 <= methods.Count); Assert.True(methods.All(m => m.MethodName == "Math.Min")); @@ -629,7 +629,7 @@ module ShortCircuit { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(2 <= methods.Count); Assert.True(methods.All(m => m.MethodName == "ShortCircuit.Or")); @@ -659,7 +659,7 @@ module C { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(3, methods.Count); Assert.True(methods.Exists(m => m.MethodName == "A.m" && @@ -700,7 +700,7 @@ modifies this } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.Single(methods); Assert.True(methods.All(m => @@ -730,7 +730,7 @@ assert true by { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); } @@ -743,7 +743,7 @@ module M { } ".TrimStart(); var options = GetDafnyOptions(optionSettings, output); - var program = Utils.Parse(new BatchErrorReporter(options), source, false); + var program = await Utils.Parse(new BatchErrorReporter(options), source, false); var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync(); Assert.Single(methods); } diff --git a/Source/DafnyTestGeneration/FirstPass.cs b/Source/DafnyTestGeneration/FirstPass.cs index 245acaafd7a..d1120d4d309 100644 --- a/Source/DafnyTestGeneration/FirstPass.cs +++ b/Source/DafnyTestGeneration/FirstPass.cs @@ -6,6 +6,7 @@ using System; using System.Collections.Generic; using System.Linq; +using System.Threading.Tasks; using Microsoft.Dafny; using Type = Microsoft.Dafny.Type; @@ -44,9 +45,9 @@ public FirstPass(DafnyOptions options) { /// Return false, if test generation should preemptively terminated, /// i.e. if there are any errors or if there are warnings and the --ignore-warnings flag is not used /// - public bool IsOk(string source, Uri uri) { + public async Task IsOk(string source, Uri uri) { var errorReporter = new ConsoleErrorReporter(options); - var program = Utils.Parse(errorReporter, source, true, uri); + var program = await Utils.Parse(errorReporter, source, true, uri); diagnostics = new(); if (errorReporter.FailCompilation) { NonZeroExitCode = true; diff --git a/Source/DafnyTestGeneration/TestGenerator.cs b/Source/DafnyTestGeneration/TestGenerator.cs index 0b10ac2d7eb..94a1f1e5b6e 100644 --- a/Source/DafnyTestGeneration/TestGenerator.cs +++ b/Source/DafnyTestGeneration/TestGenerator.cs @@ -66,12 +66,12 @@ public static async IAsyncEnumerable GetDeadCodeStatistics(TextReader so options.PrintMode = PrintModes.Everything; var code = await source.ReadToEndAsync(); var firstPass = new FirstPass(options); - if (!firstPass.IsOk(code, uri)) { + if (!(await firstPass.IsOk(code, uri))) { SetNonZeroExitCode = true; yield break; } SetNonZeroExitCode = firstPass.NonZeroExitCode; - var program = Utils.Parse(new BatchErrorReporter(options), code, false, uri); + var program = await Utils.Parse(new BatchErrorReporter(options), code, false, uri); if (report != null) { report.RegisterFiles(program); // do this here prior to modifying the program } @@ -219,12 +219,12 @@ public static async IAsyncEnumerable GetTestClassForProgram(TextReader s options.PrintMode = PrintModes.Everything; var code = await source.ReadToEndAsync(); var firstPass = new FirstPass(options); - if (!firstPass.IsOk(code, uri)) { + if (!(await firstPass.IsOk(code, uri))) { SetNonZeroExitCode = true; yield break; } SetNonZeroExitCode = firstPass.NonZeroExitCode; - var program = Utils.Parse(new BatchErrorReporter(options), code, false, uri); + var program = await Utils.Parse(new BatchErrorReporter(options), code, false, uri); var rawName = Regex.Replace(uri?.AbsolutePath ?? "", "[^a-zA-Z0-9_]", ""); string EscapeDafnyStringLiteral(string str) { diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index f46fe690e89..e86777c0200 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -9,6 +9,7 @@ using System.Linq; using System.Text.RegularExpressions; using System.Threading; +using System.Threading.Tasks; using JetBrains.Annotations; using Microsoft.Boogie; using Microsoft.Dafny; @@ -26,7 +27,7 @@ public static class Utils { /// public static List Translate(Program program) { var ret = new List { }; - var thread = new System.Threading.Thread( + var thread = new Thread( () => { var oldPrintInstrumented = program.Reporter.Options.PrintInstrumented; program.Reporter.Options.PrintInstrumented = true; @@ -83,12 +84,13 @@ public static Type CopyWithReplacements(Type type, List from, List /// /// Parse a string read (from a certain file) to a Dafny Program /// - public static Program/*?*/ Parse(ErrorReporter reporter, string source, bool resolve = true, Uri uri = null) { + public static async Task /*?*/ Parse(ErrorReporter reporter, string source, bool resolve = true, Uri uri = null) { uri ??= new Uri(Path.Combine(Path.GetTempPath(), "parseUtils.dfy")); var fs = new InMemoryFileSystem(ImmutableDictionary.Empty.Add(uri, source)); - var program = new ProgramParser().ParseFiles(uri.LocalPath, - new[] { DafnyFile.CreateAndValidate(reporter, fs, reporter.Options, uri, Token.NoToken) }, reporter, CancellationToken.None); + var dafnyFile = await DafnyFile.CreateAndValidate(reporter, fs, reporter.Options, uri, Token.NoToken); + var program = await new ProgramParser().ParseFiles(uri.LocalPath, + new[] { dafnyFile }, reporter, CancellationToken.None); if (!resolve) { return program; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/libraryOption/libraryOption.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/libraryOption/libraryOption.dfy.expect index 8dc075b70ae..3b35a7bf7d2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/libraryOption/libraryOption.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/libraryOption/libraryOption.dfy.expect @@ -1,2 +1,3 @@ +CLI: Warning: The file 'brokenProducer.dfy' 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 brokenProducer.dfy(1,9): Error: Function body type mismatch (expected int, got bool) 1 resolution/type errors detected in libraryOption.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libraries/dfyconfig.toml b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libraries/dfyconfig.toml index e0964ef6199..03fd41d67f7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libraries/dfyconfig.toml +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libraries/dfyconfig.toml @@ -1,5 +1,4 @@ - -excludes = ["wrappersLib.dfy"] +includes = ["usesLibrary.dfy"] [options] library = [ diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libraries/usesLibrary.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libraries/usesLibrary.dfy index 7b7e80ab7b3..2e14c622981 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libraries/usesLibrary.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libraries/usesLibrary.dfy @@ -1,4 +1,4 @@ -// RUN: %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" > "%t" +// RUN: %resolve "%S/dfyconfig.toml" --allow-warnings > "%t" // RUN: %diff "%s.expect" "%t" module Consumer { @@ -8,5 +8,4 @@ module Consumer { function MaybeInt(): Option { Some(42) } - } \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libraries/usesLibrary.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libraries/usesLibrary.dfy.expect index f829807e3d5..fc50822baec 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libraries/usesLibrary.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libraries/usesLibrary.dfy.expect @@ -1,2 +1,3 @@ +dfyconfig.toml(1,0): Warning: The file 'wrappersLib.dfy' 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 Dafny program verifier did not attempt verification diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3294.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3294.dfy.expect index 53f65df4b6e..75ade2bda83 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3294.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3294.dfy.expect @@ -1,2 +1,3 @@ +CLI: Warning: The file 'git-issue-3294.dfy' 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 git-issue-3294.dfy(7,4): Error: member IsFailure does not exist in FailureRestrictedType, in :- statement 1 resolution/type errors detected in git-issue-3294.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3513/git-issue-3513.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3513/git-issue-3513.dfy index 2fdd65f2c73..b5445ebd542 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3513/git-issue-3513.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3513/git-issue-3513.dfy @@ -1,8 +1,8 @@ -// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename "%s" > "%t" -// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename --library:"%S/src/A.dfy" "%s" >> "%t" -// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename --library:"%S/src/A.dfy,%S/src/sub/B.dfy" "%s" >> "%t" -// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename --library:"%S/src/A.dfy , %S/src/sub/B.dfy" "%s" >> "%t" -// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename --library:"%S/src" "%s" >> "%t" +// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename --allow-warnings "%s" > "%t" +// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename --allow-warnings --library:"%S/src/A.dfy" "%s" >> "%t" +// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename --allow-warnings --library:"%S/src/A.dfy,%S/src/sub/B.dfy" "%s" >> "%t" +// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename --allow-warnings --library:"%S/src/A.dfy , %S/src/sub/B.dfy" "%s" >> "%t" +// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename --allow-warnings --library:"%S/src" "%s" >> "%t" // RUN: %diff "%s.expect" "%t" module M { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3513/git-issue-3513.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3513/git-issue-3513.dfy.expect index 14179a1b9ac..dddcfe2fca2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3513/git-issue-3513.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3513/git-issue-3513.dfy.expect @@ -1,10 +1,14 @@ git-issue-3513.dfy(9,9): Error: module A does not exist 1 resolution/type errors detected in git-issue-3513.dfy +CLI: Warning: The file 'A.dfy' 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 A.dfy(4,9): Error: module B does not exist 1 resolution/type errors detected in git-issue-3513.dfy +CLI: Warning: The file 'B.dfy' 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 Dafny program verifier did not attempt verification +CLI: Warning: The file 'B.dfy' 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 Dafny program verifier did not attempt verification +CLI: Warning: The file 'B.dfy' 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 Dafny program verifier did not attempt verification diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy index f4e9fcf4df6..895885e7ae6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy @@ -1,12 +1,12 @@ // NONUNIFORM: Not a compiler test // Verification coverage: // RUN: rm -rf "%t"/coverage_verification -// RUN: %baredafny verify --use-basename-for-filename --show-snippets false --allow-axioms --verify-included-files --no-timestamp-for-coverage-report --verification-coverage-report "%t/coverage_verification" %s +// RUN: %verify --allow-axioms --verify-included-files --no-timestamp-for-coverage-report --verification-coverage-report "%t/coverage_verification" %s // RUN: %sed 's/

"%t"/coverage_verification_actual.html // RUN: %diff "%S/ProofDependencies.dfy_verification.html.expect" "%t/coverage_verification_actual.html" // Expected test coverage: // RUN: rm -rf "%t"/coverage_testing -// RUN: %baredafny generate-tests Block --no-timestamp-for-coverage-report --expected-coverage-report "%t/coverage_testing" %s +// RUN: %baredafny generate-tests Block --allow-axioms --no-timestamp-for-coverage-report --expected-coverage-report "%t/coverage_testing" %s // RUN: %sed 's/

"%t"/coverage_testing_actual.html // RUN: %diff "%S/ProofDependencies.dfy_tests_expected.html.expect" "%t/coverage_testing_actual.html" // Combined coverage: diff --git a/docs/dev/news/5313.feat b/docs/dev/news/5313.feat new file mode 100644 index 00000000000..7ee380d96e0 --- /dev/null +++ b/docs/dev/news/5313.feat @@ -0,0 +1 @@ +- Warn when passing something other than a doo file to `--library` \ No newline at end of file