diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 60bfd8a0ddc..646ea176cb5 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -34,7 +34,7 @@ - + diff --git a/Source/DafnyCore/Generic/Util.cs b/Source/DafnyCore/Generic/Util.cs index 1c2fa8e08bd..6c76a5a0a02 100644 --- a/Source/DafnyCore/Generic/Util.cs +++ b/Source/DafnyCore/Generic/Util.cs @@ -26,6 +26,12 @@ public static ISet Empty() { public static class Util { + public static Task WaitForComplete(this IObservable observable) { + var result = new TaskCompletionSource(); + observable.Subscribe(_ => { }, e => result.SetException(e), () => result.SetResult()); + return result.Task; + } + public static string CapitaliseFirstLetter(this string input) { if (input.Length > 0) { return char.ToUpper(input[0]) + input.Substring(1); diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index 37b38cbe198..4310379c531 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -57,7 +57,7 @@ public DafnyDiagnostic[] GetDiagnosticsForUri(Uri uri) => private readonly ConcurrentDictionary verifyingOrVerifiedSymbols = new(); private readonly LazyConcurrentDictionary> tasksPerVerifiable = new(); - private DafnyOptions Options => Input.Options; + public DafnyOptions Options => Input.Options; public CompilationInput Input { get; } public DafnyProject Project => Input.Project; private readonly ExecutionEngine boogieEngine; @@ -225,8 +225,6 @@ private async Task ResolveAsync() { await ParsedProgram; var resolution = await documentLoader.ResolveAsync(this, transformedProgram!, cancellationSource.Token); - Options.ProcessSolverOptions(errorReporter, Options.DafnyProject.StartingToken); - updates.OnNext(new FinishedResolution( resolution, GetDiagnosticsCopy())); @@ -281,10 +279,11 @@ public async Task VerifyLocation(FilePosition verifiableLocation, bool onl return false; } - return await VerifyCanVerify(canVerify, _ => true, onlyPrepareVerificationForGutterTests); + return await VerifyCanVerify(canVerify, _ => true, null, onlyPrepareVerificationForGutterTests); } public async Task VerifyCanVerify(ICanVerify canVerify, Func taskFilter, + int? randomSeed = 0, bool onlyPrepareVerificationForGutterTests = false) { var resolution = await Resolution; @@ -293,23 +292,23 @@ public async Task VerifyCanVerify(ICanVerify canVerify, Func taskFilter) { + ResolutionResult resolution, Func taskFilter, int? randomSeed) { try { var ticket = verificationTickets.Dequeue(CancellationToken.None); @@ -345,7 +344,7 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT updated = true; return result; }); - if (updated) { + if (updated || randomSeed != null) { updates.OnNext(new CanVerifyPartsIdentified(canVerify, tasksPerVerifiable[canVerify].ToList())); } @@ -355,7 +354,8 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT if (!onlyPrepareVerificationForGutterTests) { foreach (var task in tasks.Where(taskFilter)) { - VerifyTask(canVerify, task); + var seededTask = randomSeed == null ? task : task.FromSeed(randomSeed.Value); + VerifyTask(canVerify, seededTask); } } diff --git a/Source/DafnyCore/Pipeline/IProgramVerifier.cs b/Source/DafnyCore/Pipeline/IProgramVerifier.cs index 7cdc359c6ff..e90746175e1 100644 --- a/Source/DafnyCore/Pipeline/IProgramVerifier.cs +++ b/Source/DafnyCore/Pipeline/IProgramVerifier.cs @@ -8,8 +8,6 @@ namespace Microsoft.Dafny { public record AssertionBatchResult(Implementation Implementation, VerificationRunResult Result); - public record ProgramVerificationTasks(IReadOnlyList Tasks); - /// /// Implementations of this interface are responsible to verify the correctness of a program. /// diff --git a/Source/DafnyCore/Pipeline/TextDocumentLoader.cs b/Source/DafnyCore/Pipeline/TextDocumentLoader.cs index dd243383240..f4165c016cc 100644 --- a/Source/DafnyCore/Pipeline/TextDocumentLoader.cs +++ b/Source/DafnyCore/Pipeline/TextDocumentLoader.cs @@ -52,6 +52,8 @@ private ResolutionResult ResolveInternal(Compilation compilation, Program progra symbolResolver.ResolveSymbols(compilation, program, cancellationToken); + compilation.Options.ProcessSolverOptions(compilation.Reporter, compilation.Options.DafnyProject.StartingToken); + List? verifiables; if (compilation.HasErrors) { verifiables = null; diff --git a/Source/DafnyDriver/CSVTestLogger.cs b/Source/DafnyDriver/CSVTestLogger.cs index 6db93b18fb1..2128ca936de 100644 --- a/Source/DafnyDriver/CSVTestLogger.cs +++ b/Source/DafnyDriver/CSVTestLogger.cs @@ -12,7 +12,7 @@ public class CSVTestLogger : ITestLoggerWithParameters { private readonly ConcurrentBag results = new(); private TextWriter writer; - private TextWriter logWriter; + private readonly TextWriter logWriter; private string writerFilename; public CSVTestLogger(TextWriter logWriter) { @@ -76,8 +76,9 @@ private void TestRunCompleteHandler(object sender, TestRunCompleteEventArgs e) { writer.WriteLine($"{result.TestCase.DisplayName},{result.Outcome},{result.Duration},{resCount}"); } - writer.Close(); + writer.Flush(); logWriter.WriteLine("Results File: " + Path.GetFullPath(writerFilename)); + logWriter.Flush(); } } } diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index f1449aaf8ea..02f56d684d9 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -2,6 +2,7 @@ using System; using System.Collections.Concurrent; using System.Collections.Generic; +using System.Diagnostics; using System.IO; using System.Linq; using System.Reactive.Subjects; @@ -21,20 +22,16 @@ namespace DafnyDriver.Commands; public record CanVerifyResult(ICanVerify CanVerify, IReadOnlyList Results); -public class CliCompilation : IDisposable { - private readonly DafnyOptions options; - - private Compilation Compilation { get; } +public class CliCompilation { + public Compilation Compilation { get; } private readonly ConcurrentDictionary errorsPerSource = new(); private int errorCount; - private bool verifiedAssertions; - - private readonly List disposables = new(); + public bool DidVerification { get; private set; } private CliCompilation( CreateCompilation createCompilation, DafnyOptions options) { - this.options = options; + Options = options; if (options.DafnyProject == null) { var firstFile = options.CliRootSourceUris.FirstOrDefault(); @@ -95,9 +92,9 @@ public void Start() { throw new InvalidOperationException("Compilation was already started"); } - ErrorReporter consoleReporter = options.DiagnosticsFormat switch { - DafnyOptions.DiagnosticsFormats.PlainText => new ConsoleErrorReporter(options), - DafnyOptions.DiagnosticsFormats.JSON => new JsonConsoleErrorReporter(options), + ErrorReporter consoleReporter = Options.DiagnosticsFormat switch { + DafnyOptions.DiagnosticsFormats.PlainText => new ConsoleErrorReporter(Options), + DafnyOptions.DiagnosticsFormats.JSON => new JsonConsoleErrorReporter(Options), _ => throw new ArgumentOutOfRangeException() }; @@ -115,14 +112,14 @@ public void Start() { } else if (ev is FinishedParsing finishedParsing) { if (errorCount > 0) { var programName = finishedParsing.Program.Name; - options.OutputWriter.WriteLine($"{errorCount} parse errors detected in {programName}"); + Options.OutputWriter.WriteLine($"{errorCount} parse errors detected in {programName}"); } } else if (ev is FinishedResolution finishedResolution) { - DafnyMain.MaybePrintProgram(finishedResolution.Result.ResolvedProgram, options.DafnyPrintResolvedFile, true); + DafnyMain.MaybePrintProgram(finishedResolution.Result.ResolvedProgram, Options.DafnyPrintResolvedFile, true); if (errorCount > 0) { var programName = finishedResolution.Result.ResolvedProgram.Name; - options.OutputWriter.WriteLine($"{errorCount} resolution/type errors detected in {programName}"); + Options.OutputWriter.WriteLine($"{errorCount} resolution/type errors detected in {programName}"); } } @@ -130,22 +127,13 @@ public void Start() { Compilation.Start(); } - public IObservable VerificationResults => verificationResults; - private readonly Subject verificationResults = new(); - private bool didVerification; - - public Task VerifyAll() { - var task = new TaskCompletionSource(); - verificationResults.Subscribe(_ => { }, e => - task.TrySetException(e), () => - task.TrySetResult()); - VerifyAllLazily().ToObservable().Subscribe(verificationResults); - return task.Task; - } + public DafnyOptions Options { get; } + + public bool VerifiedAssertions { get; private set; } - private async IAsyncEnumerable VerifyAllLazily() { + public async IAsyncEnumerable VerifyAllLazily(int? randomSeed) { var canVerifyResults = new Dictionary(); - Compilation.Updates.Subscribe(ev => { + using var subscription = Compilation.Updates.Subscribe(ev => { if (ev is CanVerifyPartsIdentified canVerifyPartsIdentified) { var canVerifyResult = canVerifyResults[canVerifyPartsIdentified.CanVerify]; @@ -181,20 +169,20 @@ private async IAsyncEnumerable VerifyAllLazily() { yield break; } - if (errorCount > 0) { + if (resolution.HasErrors) { yield break; } - didVerification = true; - var canVerifies = resolution.CanVerifies?.DistinctBy(v => v.Tok).ToList(); if (canVerifies == null) { yield break; } + DidVerification = true; + canVerifies = FilterCanVerifies(canVerifies, out var line); - verifiedAssertions = line != null; + VerifiedAssertions = line != null; var orderedCanVerifies = canVerifies.OrderBy(v => v.Tok.pos).ToList(); foreach (var canVerify in orderedCanVerifies) { @@ -204,13 +192,16 @@ private async IAsyncEnumerable VerifyAllLazily() { results.TaskFilter = t => KeepVerificationTask(t, line.Value); } - await Compilation.VerifyCanVerify(canVerify, results.TaskFilter); + var shouldVerify = await Compilation.VerifyCanVerify(canVerify, results.TaskFilter, randomSeed); + if (!shouldVerify) { + orderedCanVerifies.Remove(canVerify); + } } foreach (var canVerify in orderedCanVerifies) { var results = canVerifyResults[canVerify]; try { - var timeLimitSeconds = TimeSpan.FromSeconds(options.Get(BoogieOptionBag.VerificationTimeLimit)); + var timeLimitSeconds = TimeSpan.FromSeconds(Options.Get(BoogieOptionBag.VerificationTimeLimit)); var tasks = new List { results.Finished.Task }; if (timeLimitSeconds.Seconds != 0) { tasks.Add(Task.Delay(timeLimitSeconds)); @@ -226,7 +217,7 @@ private async IAsyncEnumerable VerifyAllLazily() { await results.Finished.Task; } catch (ProverException e) { Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, e.Message); - throw; + yield break; } catch (OperationCanceledException) { } catch (Exception e) { @@ -241,12 +232,12 @@ private async IAsyncEnumerable VerifyAllLazily() { } private List FilterCanVerifies(List canVerifies, out int? line) { - var symbolFilter = options.Get(VerifyCommand.FilterSymbol); + var symbolFilter = Options.Get(VerifyCommand.FilterSymbol); if (symbolFilter != null) { canVerifies = canVerifies.Where(canVerify => canVerify.FullDafnyName.Contains(symbolFilter)).ToList(); } - var filterPosition = options.Get(VerifyCommand.FilterPosition); + var filterPosition = Options.Get(VerifyCommand.FilterPosition); if (filterPosition == null) { line = null; return canVerifies; @@ -276,146 +267,6 @@ private List FilterCanVerifies(List canVerifies, out int private bool KeepVerificationTask(IVerificationTask task, int line) { return task.ScopeToken.line == line || task.Token.line == line; } - - public void ReportVerificationDiagnostics() { - VerificationResults.Subscribe(result => { - // We use an intermediate reporter so we can sort the diagnostics from all parts by token - var batchReporter = new BatchErrorReporter(options); - foreach (var completed in result.Results) { - Compilation.ReportDiagnosticsInResult(options, result.CanVerify.FullDafnyName, result.CanVerify.NameToken, - (uint)completed.Result.RunTime.Seconds, - completed.Result, batchReporter); - } - - foreach (var diagnostic in batchReporter.AllMessages.OrderBy(m => m.Token)) { - Compilation.Reporter.Message(diagnostic.Source, diagnostic.Level, diagnostic.ErrorId, diagnostic.Token, - diagnostic.Message); - } - }); - } - - public void ReportVerificationSummary() { - var statistics = new VerificationStatistics(); - - VerificationResults.Subscribe(result => { - foreach (var taskResult in result.Results) { - var runResult = taskResult.Result; - - switch (runResult.Outcome) { - case SolverOutcome.Valid: - case SolverOutcome.Bounded: - Interlocked.Increment(ref statistics.VerifiedSymbols); - Interlocked.Add(ref statistics.VerifiedAssertions, runResult.Asserts.Count); - break; - case SolverOutcome.Invalid: - var total = runResult.Asserts.Count; - var errors = runResult.CounterExamples.Count; - Interlocked.Add(ref statistics.VerifiedAssertions, total - errors); - Interlocked.Add(ref statistics.ErrorCount, errors); - break; - case SolverOutcome.TimeOut: - Interlocked.Increment(ref statistics.TimeoutCount); - break; - case SolverOutcome.OutOfMemory: - Interlocked.Increment(ref statistics.OutOfMemoryCount); - break; - case SolverOutcome.OutOfResource: - Interlocked.Increment(ref statistics.OutOfResourceCount); - break; - case SolverOutcome.Undetermined: - Interlocked.Increment(ref statistics.InconclusiveCount); - break; - default: - throw new ArgumentOutOfRangeException(); - } - } - }, e => { - Interlocked.Increment(ref statistics.SolverExceptionCount); - }, () => { - disposables.Add(WriteTrailer(options.OutputWriter, verifiedAssertions, statistics)); - }); - } - - private async Task WriteTrailer(TextWriter output, bool reportAssertions, VerificationStatistics statistics) { - if (options.Verbosity <= CoreOptions.VerbosityLevel.Quiet) { - return; - } - - if (!didVerification) { - return; - } - - await output.WriteLineAsync(); - - if (reportAssertions) { - await output.WriteAsync($"{options.DescriptiveToolName} finished with {statistics.VerifiedAssertions} assertions verified, {statistics.ErrorCount} error{Util.Plural(statistics.ErrorCount)}"); - - } else { - await output.WriteAsync($"{options.DescriptiveToolName} finished with {statistics.VerifiedSymbols} verified, {statistics.ErrorCount} error{Util.Plural(statistics.ErrorCount)}"); - }; - if (statistics.InconclusiveCount != 0) { - await output.WriteAsync($", {statistics.InconclusiveCount} inconclusive{Util.Plural(statistics.InconclusiveCount)}"); - } - - if (statistics.TimeoutCount != 0) { - await output.WriteAsync($", {statistics.TimeoutCount} time out{Util.Plural(statistics.TimeoutCount)}"); - } - - if (statistics.OutOfMemoryCount != 0) { - await output.WriteAsync($", {statistics.OutOfMemoryCount} out of memory"); - } - - if (statistics.OutOfResourceCount != 0) { - await output.WriteAsync($", {statistics.OutOfResourceCount} out of resource"); - } - - if (statistics.SolverExceptionCount != 0) { - await output.WriteAsync($", {statistics.SolverExceptionCount} solver exceptions"); - } - - await output.WriteLineAsync(); - await output.FlushAsync(); - } - - public void RecordProofDependencies(ResolutionResult resolution) { - var usedDependencies = new HashSet(); - var proofDependencyManager = resolution.ResolvedProgram.ProofDependencyManager; - VerificationResultLogger? verificationResultLogger = null; - try { - verificationResultLogger = new VerificationResultLogger(options, proofDependencyManager); - } catch (ArgumentException e) { - Compilation.Reporter.Error(MessageSource.Verifier, Compilation.Project.StartingToken, e.Message); - } - - verificationResults.Subscribe(result => { - ProofDependencyWarnings.ReportSuspiciousDependencies(options, result.Results, - resolution.ResolvedProgram.Reporter, resolution.ResolvedProgram.ProofDependencyManager); - - verificationResultLogger?.Report(result); - - foreach (var used in result.Results.SelectMany(part => part.Result.CoveredElements)) { - usedDependencies.Add(used); - } - }, - e => { }, - () => { - verificationResultLogger?.Finish(); - - var coverageReportDir = options.Get(CommonOptionBag.VerificationCoverageReport); - if (coverageReportDir != null) { - new CoverageReporter(options).SerializeVerificationCoverageReport( - proofDependencyManager, resolution.ResolvedProgram, - usedDependencies, - coverageReportDir); - } - }); - } - - public void Dispose() { - foreach (var disposable in disposables) { - disposable.Dispose(); - } - } } record VerificationStatistics { diff --git a/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs b/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs index 6a18263b17f..bb2d4015322 100644 --- a/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs +++ b/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs @@ -1,8 +1,9 @@ using System; using System.Collections.Generic; using System.CommandLine; -using System.CommandLine.Invocation; using System.Linq; +using System.Reactive.Subjects; +using System.Threading.Tasks; using DafnyCore; using DafnyDriver.Commands; @@ -39,7 +40,58 @@ public static Command Create() { foreach (var option in Options) { result.AddOption(option); } - DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => VerifyCommand.HandleVerification(options)); + DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => Execute(options)); return result; } + + private static async Task Execute(DafnyOptions options) { + if (options.Get(CommonOptionBag.VerificationCoverageReport) != null) { + options.TrackVerificationCoverage = true; + } + + var compilation = CliCompilation.Create(options); + compilation.Start(); + + try { + var resolution = await compilation.Resolution; + + Subject verificationResults = new(); + + // We should redesign the output of this command + // It should start out with a summary that reports how many proofs are brittle, and shows statistical data, + // such as averages and standard-deviations. + // For error diagnostics, we should group duplicates and say how often they occur. + // 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 verificationResultsLogged = VerifyCommand.LogVerificationResults(compilation, resolution, verificationResults); + + await RunVerificationIterations(options, compilation, verificationResults); + await summaryReported; + await verificationResultsLogged; + } catch (TaskCanceledException) { + } + + return compilation.ExitCode; + } + + private static async Task RunVerificationIterations(DafnyOptions options, CliCompilation compilation, + IObserver verificationResultsObserver) { + int iterationSeed = (int)options.Get(RandomSeed); + var random = new Random(iterationSeed); + foreach (var iteration in Enumerable.Range(0, (int)options.Get(Iterations))) { + await options.OutputWriter.WriteLineAsync( + $"Starting verification of iteration {iteration} with seed {iterationSeed}"); + try { + await foreach (var result in compilation.VerifyAllLazily(iterationSeed)) { + verificationResultsObserver.OnNext(result); + } + } catch (Exception e) { + verificationResultsObserver.OnError(e); + } + iterationSeed = random.Next(); + } + verificationResultsObserver.OnCompleted(); + } } diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs index 78d569bc50c..65173a59896 100644 --- a/Source/DafnyDriver/Commands/VerifyCommand.cs +++ b/Source/DafnyDriver/Commands/VerifyCommand.cs @@ -1,8 +1,17 @@ +#nullable enable +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; using DafnyDriver.Commands; +using Microsoft.Boogie; namespace Microsoft.Dafny; @@ -22,39 +31,198 @@ static VerifyCommand() { public static Command Create() { var result = new Command("verify", "Verify the program."); result.AddArgument(DafnyCommands.FilesArgument); - foreach (var option in Options) { + foreach (var option in VerifyOptions) { result.AddOption(option); } - DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, async (options, _) => await HandleVerification(options)); + DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => HandleVerification(options)); return result; } + private static IReadOnlyList