From 385103dd9e77a329b04c45fef0c3ceee1ae6bb26 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 8 Feb 2024 17:54:41 +0100 Subject: [PATCH] Filter assertions (#5031) ### Description - Allow using `--filter-position` to only verify individual assertions. The implementation relies on a new version of Boogie, which changes the API so that Boogie returns not a list of implementations but instead of a list of 'verification tasks', which map to individual SMT executions or 'assertion batches'. When using `--isolate-assertions`, each assertion is given such as task, and it becomes easy to filter these tasks/assertions based on a file position. #### Background of some of the code changes This change in the Boogie API means Dafny is not longer updated when all the tasks for a particular Boogie implementation are finished, which effects a few things that rely on all tasks in a Boogie implementation to be done: - Computation of redundant assertions - Gutter icons (maybe it conceptually does not depend on Boogie implementations, I'm not sure, but the current implementation cares about Boogie implementations) There is no change in behavior for the above, but the code had to be updated so on the Dafny side we track whether everything for a particular implementation is done. ### How has this been tested? - Added new cases to the existing littish test `filter.dfy` - Some gutter icons tests have been updated, which is I think due to an improvement. The last batch completed + implementation completed steps are now combined, so two updates that would always immediately follow each other are now squashed together. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Makefile | 2 +- Source/DafnyCore/AST/Tokens.cs | 11 + Source/DafnyCore/DafnyConsolePrinter.cs | 22 +- Source/DafnyCore/DafnyCore.csproj | 2 +- .../DafnyCore/Generic/BatchErrorReporter.cs | 3 +- Source/DafnyCore/Options/CommonOptionBag.cs | 1 - Source/DafnyCore/Pipeline/Compilation.cs | 99 +++---- .../Pipeline/Events/BoogieException.cs | 2 +- .../DafnyCore/Pipeline/Events/BoogieUpdate.cs | 2 +- .../Events/CanVerifyPartsIdentified.cs | 2 +- Source/DafnyCore/Pipeline/IProgramVerifier.cs | 6 +- Source/DafnyCore/ProofDependencyWarnings.cs | 56 +++- Source/DafnyCore/Verifier/BoogieGenerator.cs | 2 +- .../Verifier/ProofDependencyManager.cs | 15 +- Source/DafnyDriver/CliCanVerifyResults.cs | 11 +- Source/DafnyDriver/CliCompilation.cs | 163 ++++++++--- Source/DafnyDriver/JsonVerificationLogger.cs | 6 +- .../DafnyDriver/SynchronousCliCompilation.cs | 2 +- Source/DafnyDriver/TextVerificationLogger.cs | 2 +- .../DafnyDriver/VerificationResultLogger.cs | 2 +- ...hedLinearVerificationGutterStatusTester.cs | 18 +- ...entLinearVerificationGutterStatusTester.cs | 16 +- ...pleLinearVerificationGutterStatusTester.cs | 181 ++++++------ .../Synchronization/VerificationStatusTest.cs | 2 + .../Various/ExceptionTests.cs | 2 +- .../Various/SlowVerifier.cs | 16 +- .../DafnyLanguageServer.cs | 15 +- .../Handlers/Custom/CounterExampleItem.cs | 10 +- .../Custom/DafnyCounterExampleHandler.cs | 6 +- .../AssertionBatchCompletedObserver.cs | 2 +- .../Language/DafnyProgramVerifier.cs | 4 +- ...rIconAndHoverVerificationDetailsManager.cs | 50 ++-- .../DafnyLanguageServer/Workspace/IdeState.cs | 272 +++++++++--------- .../Workspace/NotificationPublisher.cs | 18 +- .../Workspace/ProjectManager.cs | 7 +- .../LitTest/VSI-Benchmarks/b4.dfy.expect | 2 +- .../09-CounterNoStateMachine.dfy.expect | 2 +- .../10-SequenceInvariant.dfy.expect | 2 +- .../12-MutexLifetime-short.dfy.expect | 2 +- .../LitTest/dafny0/Termination.dfy.expect | 2 +- .../dafny0/Termination.dfy.refresh.expect | 2 +- .../LitTest/dafny1/MoreInduction.dfy.expect | 2 +- .../LitTest/dafny4/ACL2-extractor.dfy.expect | 2 +- .../SoftwareFoundations-Basics.dfy.expect | 2 +- .../git-issues/git-issue-1252.dfy.expect | 2 +- .../git-issues/git-issue-3855.dfy.expect | 2 +- .../LitTest/lambdas/MatrixAssoc.dfy.expect | 2 +- .../verification/Inputs/dfyconfig.toml | 1 + .../verification/Inputs/single-file.dfy | 25 ++ .../LitTests/LitTest/verification/filter.dfy | 28 +- .../LitTest/verification/filter.dfy.expect | 42 ++- .../vstte2012/BreadthFirstSearch.dfy.expect | 2 +- .../LitTest/vstte2012/Tree.dfy.expect | 2 +- Source/XUnitExtensions/Lit/LitTestCase.cs | 10 +- customBoogie.patch | 2 +- 55 files changed, 666 insertions(+), 500 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/single-file.dfy diff --git a/Makefile b/Makefile index b3cc398a13..d6256e00c2 100644 --- a/Makefile +++ b/Makefile @@ -73,7 +73,7 @@ z3-ubuntu: chmod +x ${DIR}/Binaries/z3/bin/z3-* format: - dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs + dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs clean: (cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin) diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs index 96810cae6b..3e9eefa37d 100644 --- a/Source/DafnyCore/AST/Tokens.cs +++ b/Source/DafnyCore/AST/Tokens.cs @@ -109,6 +109,13 @@ public IToken WithVal(string newVal) { }; } + public int CompareTo(Boogie.IToken other) { + if (line != other.line) { + return line.CompareTo(other.line); + } + return col.CompareTo(other.col); + } + public override int GetHashCode() { return pos; } @@ -189,6 +196,10 @@ public virtual IToken Prev { public int CompareTo(IToken other) { return WrappedToken.CompareTo(other); } + + public int CompareTo(Boogie.IToken other) { + return WrappedToken.CompareTo(other); + } } public static class TokenExtensions { diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index c09d81c666..42d23a9246 100644 --- a/Source/DafnyCore/DafnyConsolePrinter.cs +++ b/Source/DafnyCore/DafnyConsolePrinter.cs @@ -20,7 +20,7 @@ public class DafnyConsolePrinter : ConsolePrinter { } } - private readonly static ConditionalWeakTable>> fsCaches = new(); + private static readonly ConditionalWeakTable>> fsCaches = new(); private DafnyOptions options; @@ -29,28 +29,28 @@ public record VCResultLogEntry( int VCNum, DateTime StartTime, TimeSpan RunTime, - ProverInterface.Outcome Outcome, + SolverOutcome Outcome, List<(Boogie.IToken Tok, string Description)> Asserts, IEnumerable CoveredElements, int ResourceCount); public record VerificationResultLogEntry( - ConditionGeneration.Outcome Outcome, + VcOutcome Outcome, TimeSpan RunTime, int ResourceCount, List VCResults, List Counterexamples); public record ConsoleLogEntry(ImplementationLogEntry Implementation, VerificationResultLogEntry Result); - public static VerificationResultLogEntry DistillVerificationResult(VerificationResult verificationResult) { + public static VerificationResultLogEntry DistillVerificationResult(ImplementationRunResult verificationResult) { return new VerificationResultLogEntry( - verificationResult.Outcome, verificationResult.End - verificationResult.Start, - verificationResult.ResourceCount, verificationResult.VCResults.Select(DistillVCResult).ToList(), verificationResult.Errors); + verificationResult.VcOutcome, verificationResult.End - verificationResult.Start, + verificationResult.ResourceCount, verificationResult.RunResults.Select(DistillVCResult).ToList(), verificationResult.Errors); } - private static VCResultLogEntry DistillVCResult(VCResult r) { - return new VCResultLogEntry(r.vcNum, r.startTime, r.runTime, r.outcome, - r.asserts.Select(a => (a.tok, a.Description.SuccessDescription)).ToList(), r.coveredElements, - r.resourceCount); + private static VCResultLogEntry DistillVCResult(VerificationRunResult r) { + return new VCResultLogEntry(r.VcNum, r.StartTime, r.RunTime, r.Outcome, + r.Asserts.Select(a => (a.tok, a.Description.SuccessDescription)).ToList(), r.CoveredElements, + r.ResourceCount); } public ConcurrentBag VerificationResults { get; } = new(); @@ -153,7 +153,7 @@ public override void ReportBplError(Boogie.IToken tok, string message, bool erro } } - public override void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result) { + public override void ReportEndVerifyImplementation(Implementation implementation, ImplementationRunResult result) { var impl = new ImplementationLogEntry(implementation.VerboseName, implementation.tok); VerificationResults.Add(new ConsoleLogEntry(impl, DistillVerificationResult(result))); } diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 136dd72f1c..ccb550f306 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -33,7 +33,7 @@ - + diff --git a/Source/DafnyCore/Generic/BatchErrorReporter.cs b/Source/DafnyCore/Generic/BatchErrorReporter.cs index e8dba15f7d..ddb291c427 100644 --- a/Source/DafnyCore/Generic/BatchErrorReporter.cs +++ b/Source/DafnyCore/Generic/BatchErrorReporter.cs @@ -9,8 +9,7 @@ public class BatchErrorReporter : ErrorReporter { public void CopyDiagnostics(ErrorReporter intoReporter) { foreach (var diagnostic in AllMessages) { - intoReporter.Message(diagnostic.Source, diagnostic.Level, diagnostic.ErrorId, diagnostic.Token, - diagnostic.Message); + intoReporter.Message(diagnostic.Source, diagnostic.Level, diagnostic.ErrorId, diagnostic.Token, diagnostic.Message); } } diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index fadd24c1ed..1357bb043e 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -3,7 +3,6 @@ using System.IO; using System.Linq; using DafnyCore; -using Microsoft.Dafny.Compilers; namespace Microsoft.Dafny; diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index 81f0a5b1df..4f0df9761b 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -50,10 +50,10 @@ public DafnyDiagnostic[] GetDiagnosticsForUri(Uri uri) => /// FilePosition is required because the default module lives in multiple files /// private readonly LazyConcurrentDictionary>>> translatedModules = new(); + Task>>> translatedModules = new(); private readonly ConcurrentDictionary verifyingOrVerifiedSymbols = new(); - private readonly LazyConcurrentDictionary> implementationsPerVerifiable = new(); + private readonly LazyConcurrentDictionary> tasksPerVerifiable = new(); private DafnyOptions Options => Input.Options; public CompilationInput Input { get; } @@ -237,12 +237,12 @@ private async Task ResolveAsync() { } } - public static string GetImplementationName(Implementation implementation) { - var prefix = implementation.Name.Split(BoogieGenerator.NameSeparator)[0]; + public static string GetTaskName(IVerificationTask task) { + var prefix = task.ScopeId + task.Split.SplitIndex; // Refining declarations get the token of what they're refining, so to distinguish them we need to // add the refining module name to the prefix. - if (implementation.tok is RefinementToken refinementToken) { + if (task.ScopeToken is RefinementToken refinementToken) { prefix += "." + refinementToken.InheritingModule.Name; } @@ -276,10 +276,11 @@ public async Task VerifyLocation(FilePosition verifiableLocation, bool onl return false; } - return await VerifyCanVerify(canVerify, onlyPrepareVerificationForGutterTests); + return await VerifyCanVerify(canVerify, _ => true, onlyPrepareVerificationForGutterTests); } - public async Task VerifyCanVerify(ICanVerify canVerify, bool onlyPrepareVerificationForGutterTests) { + public async Task VerifyCanVerify(ICanVerify canVerify, Func taskFilter, + bool onlyPrepareVerificationForGutterTests = false) { var resolution = await Resolution; var containingModule = canVerify.ContainingModule; if (!containingModule.ShouldVerify(resolution.ResolvedProgram.Compilation)) { @@ -293,22 +294,22 @@ public async Task VerifyCanVerify(ICanVerify canVerify, bool onlyPrepareVe updates.OnNext(new ScheduledVerification(canVerify)); if (onlyPrepareVerificationForGutterTests) { - await VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution); + await VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution, taskFilter); return true; } - _ = VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution); + _ = VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution, taskFilter); return true; } private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterTests, ICanVerify canVerify, - ResolutionResult resolution) { + ResolutionResult resolution, Func taskFilter) { try { var ticket = verificationTickets.Dequeue(CancellationToken.None); var containingModule = canVerify.ContainingModule; - IReadOnlyDictionary> tasksForModule; + IReadOnlyDictionary> tasksForModule; try { tasksForModule = await translatedModules.GetOrAdd(containingModule, async () => { var result = await verifier.GetVerificationTasksAsync(boogieEngine, resolution, containingModule, @@ -317,9 +318,9 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT cancellationSource.Token.Register(task.Cancel); } - return result.GroupBy(t => ((IToken)t.Implementation.tok).GetFilePosition()).ToDictionary( + return result.GroupBy(t => ((IToken)t.ScopeToken).GetFilePosition()).ToDictionary( g => g.Key, - g => (IReadOnlyList)g.ToList()); + g => (IReadOnlyList)g.ToList()); }); } catch (OperationCanceledException) { throw; @@ -328,26 +329,26 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT throw; } - // For updated to be reliable, ImplementationsPerVerifiable must be Lazy + // For updated to be reliable, tasksPerVerifiable must be Lazy var updated = false; - var tasks = implementationsPerVerifiable.GetOrAdd(canVerify, () => { + var tasks = tasksPerVerifiable.GetOrAdd(canVerify, () => { var result = tasksForModule.GetValueOrDefault(canVerify.NameToken.GetFilePosition()) ?? - new List(0); + new List(0); updated = true; return result; }); if (updated) { updates.OnNext(new CanVerifyPartsIdentified(canVerify, - implementationsPerVerifiable[canVerify].ToList())); + tasksPerVerifiable[canVerify].ToList())); } // When multiple calls to VerifyUnverifiedSymbol are made, the order in which they pass this await matches the call order. await ticket; if (!onlyPrepareVerificationForGutterTests) { - foreach (var task in tasks) { + foreach (var task in tasks.Where(taskFilter)) { VerifyTask(canVerify, task); } } @@ -358,16 +359,10 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT } } - private void VerifyTask(ICanVerify canVerify, IImplementationTask task) { + private void VerifyTask(ICanVerify canVerify, IVerificationTask task) { var statusUpdates = task.TryRun(); if (statusUpdates == null) { if (task.CacheStatus is Completed completedCache) { - foreach (var result in completedCache.Result.VCResults) { -#pragma warning disable CS8625 // Cannot convert null literal to non-nullable reference type. - HandleStatusUpdate(canVerify, task, new BatchCompleted(null /* unused */, result)); -#pragma warning restore CS8625 // Cannot convert null literal to non-nullable reference type. - } - HandleStatusUpdate(canVerify, task, completedCache); } @@ -399,8 +394,8 @@ public async Task Cancel(FilePosition filePosition) { var resolution = await Resolution; var canVerify = resolution.ResolvedProgram.FindNode(filePosition.Uri, filePosition.Position.ToDafnyPosition()); if (canVerify != null) { - var implementations = implementationsPerVerifiable.TryGetValue(canVerify, out var implementationsPerName) - ? implementationsPerName! : Enumerable.Empty(); + var implementations = tasksPerVerifiable.TryGetValue(canVerify, out var implementationsPerName) + ? implementationsPerName! : Enumerable.Empty(); foreach (var view in implementations) { view.Cancel(); } @@ -408,12 +403,12 @@ public async Task Cancel(FilePosition filePosition) { } } - private void HandleStatusUpdate(ICanVerify canVerify, IImplementationTask implementationTask, IVerificationStatus boogieStatus) { - var tokenString = BoogieGenerator.ToDafnyToken(true, implementationTask.Implementation.tok).TokenToString(Options); + private void HandleStatusUpdate(ICanVerify canVerify, IVerificationTask verificationTask, IVerificationStatus boogieStatus) { + var tokenString = BoogieGenerator.ToDafnyToken(true, verificationTask.Split.Token).TokenToString(Options); logger.LogDebug($"Received Boogie status {boogieStatus} for {tokenString}, version {Input.Version}"); updates.OnNext(new BoogieUpdate(transformedProgram!.ProofDependencyManager, canVerify, - implementationTask, + verificationTask, boogieStatus)); } @@ -461,7 +456,7 @@ public void Dispose() { CancelPendingUpdates(); } - public static List GetDiagnosticsFromResult(DafnyOptions options, Uri uri, IImplementationTask task, VCResult result) { + public static List GetDiagnosticsFromResult(DafnyOptions options, Uri uri, IVerificationTask task, VerificationRunResult result) { var errorReporter = new ObservableErrorReporter(options, uri); List diagnostics = new(); errorReporter.Updates.Subscribe(d => diagnostics.Add(d.Diagnostic)); @@ -471,11 +466,11 @@ public static List GetDiagnosticsFromResult(DafnyOptions option return diagnostics.OrderBy(d => d.Token.GetLspPosition()).ToList(); } - public static void ReportDiagnosticsInResult(DafnyOptions options, IImplementationTask task, VCResult result, + public static void ReportDiagnosticsInResult(DafnyOptions options, IVerificationTask task, VerificationRunResult result, ErrorReporter errorReporter) { - var outcome = GetOutcome(result.outcome); - result.counterExamples.Sort(new CounterexampleComparer()); - foreach (var counterExample in result.counterExamples) //.OrderBy(d => d.GetLocation())) + var outcome = GetOutcome(result.Outcome); + result.CounterExamples.Sort(new CounterexampleComparer()); + foreach (var counterExample in result.CounterExamples) //.OrderBy(d => d.GetLocation())) { errorReporter.ReportBoogieError(counterExample.CreateErrorInformation(outcome, options.ForceBplErrors)); } @@ -484,28 +479,28 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, IImplementati // The Boogie API forces us to create a temporary engine here to report the outcome, even though it only uses the options. var boogieEngine = new ExecutionEngine(options, new VerificationResultCache(), CustomStackSizePoolTaskScheduler.Create(0, 0)); - var implementation = task.Implementation; + var implementation = task.Split.Implementation; boogieEngine.ReportOutcome(null, outcome, outcomeError => errorReporter.ReportBoogieError(outcomeError, false), implementation.VerboseName, implementation.tok, null, TextWriter.Null, - implementation.GetTimeLimit(options), result.counterExamples); + implementation.GetTimeLimit(options), result.CounterExamples); } - private static ConditionGeneration.Outcome GetOutcome(ProverInterface.Outcome outcome) { + public static VcOutcome GetOutcome(SolverOutcome outcome) { switch (outcome) { - case ProverInterface.Outcome.Valid: - return ConditionGeneration.Outcome.Correct; - case ProverInterface.Outcome.Invalid: - return ConditionGeneration.Outcome.Errors; - case ProverInterface.Outcome.TimeOut: - return ConditionGeneration.Outcome.TimedOut; - case ProverInterface.Outcome.OutOfMemory: - return ConditionGeneration.Outcome.OutOfMemory; - case ProverInterface.Outcome.OutOfResource: - return ConditionGeneration.Outcome.OutOfResource; - case ProverInterface.Outcome.Undetermined: - return ConditionGeneration.Outcome.Inconclusive; - case ProverInterface.Outcome.Bounded: - return ConditionGeneration.Outcome.ReachedBound; + case SolverOutcome.Valid: + return VcOutcome.Correct; + case SolverOutcome.Invalid: + return VcOutcome.Errors; + case SolverOutcome.TimeOut: + return VcOutcome.TimedOut; + case SolverOutcome.OutOfMemory: + return VcOutcome.OutOfMemory; + case SolverOutcome.OutOfResource: + return VcOutcome.OutOfResource; + case SolverOutcome.Undetermined: + return VcOutcome.Inconclusive; + case SolverOutcome.Bounded: + return VcOutcome.ReachedBound; default: throw new ArgumentOutOfRangeException(nameof(outcome), outcome, null); } diff --git a/Source/DafnyCore/Pipeline/Events/BoogieException.cs b/Source/DafnyCore/Pipeline/Events/BoogieException.cs index 419d979128..d84cc8f542 100644 --- a/Source/DafnyCore/Pipeline/Events/BoogieException.cs +++ b/Source/DafnyCore/Pipeline/Events/BoogieException.cs @@ -4,4 +4,4 @@ namespace Microsoft.Dafny; -public record BoogieException(ICanVerify CanVerify, IImplementationTask Task, Exception Exception) : ICompilationEvent; \ No newline at end of file +public record BoogieException(ICanVerify CanVerify, IVerificationTask Task, Exception Exception) : ICompilationEvent; \ No newline at end of file diff --git a/Source/DafnyCore/Pipeline/Events/BoogieUpdate.cs b/Source/DafnyCore/Pipeline/Events/BoogieUpdate.cs index 0514b3aa95..03bc69f149 100644 --- a/Source/DafnyCore/Pipeline/Events/BoogieUpdate.cs +++ b/Source/DafnyCore/Pipeline/Events/BoogieUpdate.cs @@ -3,7 +3,7 @@ namespace Microsoft.Dafny; public record BoogieUpdate(ProofDependencyManager ProofDependencyManager, - ICanVerify CanVerify, IImplementationTask ImplementationTask, IVerificationStatus BoogieStatus) + ICanVerify CanVerify, IVerificationTask VerificationTask, IVerificationStatus BoogieStatus) : ICompilationEvent { } \ No newline at end of file diff --git a/Source/DafnyCore/Pipeline/Events/CanVerifyPartsIdentified.cs b/Source/DafnyCore/Pipeline/Events/CanVerifyPartsIdentified.cs index 296e20806e..fca31082e2 100644 --- a/Source/DafnyCore/Pipeline/Events/CanVerifyPartsIdentified.cs +++ b/Source/DafnyCore/Pipeline/Events/CanVerifyPartsIdentified.cs @@ -3,5 +3,5 @@ namespace Microsoft.Dafny; -public record CanVerifyPartsIdentified(ICanVerify CanVerify, IReadOnlyList Parts) : ICompilationEvent { +public record CanVerifyPartsIdentified(ICanVerify CanVerify, IReadOnlyList Parts) : ICompilationEvent { } \ No newline at end of file diff --git a/Source/DafnyCore/Pipeline/IProgramVerifier.cs b/Source/DafnyCore/Pipeline/IProgramVerifier.cs index bac2880a61..7cdc359c6f 100644 --- a/Source/DafnyCore/Pipeline/IProgramVerifier.cs +++ b/Source/DafnyCore/Pipeline/IProgramVerifier.cs @@ -6,15 +6,15 @@ using VC; namespace Microsoft.Dafny { - public record AssertionBatchResult(Implementation Implementation, VCResult Result); + public record AssertionBatchResult(Implementation Implementation, VerificationRunResult Result); - public record ProgramVerificationTasks(IReadOnlyList Tasks); + public record ProgramVerificationTasks(IReadOnlyList Tasks); /// /// Implementations of this interface are responsible to verify the correctness of a program. /// public interface IProgramVerifier { - Task> GetVerificationTasksAsync(ExecutionEngine engine, + Task> GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken); diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index 3e3c616a9e..f978623dfa 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -1,33 +1,59 @@ +using System.Collections.Concurrent; +using System.Collections.Generic; using System.Linq; using DafnyCore.Verifier; +using Microsoft.Boogie; using Microsoft.Dafny.ProofObligationDescription; using VC; namespace Microsoft.Dafny; public class ProofDependencyWarnings { + + + public static void ReportSuspiciousDependencies(DafnyOptions options, IEnumerable<(IVerificationTask Task, Completed Result)> parts, + ErrorReporter reporter, ProofDependencyManager manager) { + foreach (var resultsForScope in parts.GroupBy(p => p.Task.ScopeId)) { + WarnAboutSuspiciousDependenciesForImplementation(options, + reporter, + manager, + resultsForScope.Key, + resultsForScope.Select(p => p.Result.Result).ToList()); + } + } + public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager) { var verificationResults = (dafnyOptions.Printer as DafnyConsolePrinter).VerificationResults.ToList(); var orderedResults = verificationResults.OrderBy(vr => (vr.Implementation.Tok.filename, vr.Implementation.Tok.line, vr.Implementation.Tok.col)); + foreach (var (implementation, result) in orderedResults) { - WarnAboutSuspiciousDependenciesForImplementation(dafnyOptions, reporter, depManager, implementation, result); + if (result.Outcome != VcOutcome.Correct) { + continue; + } + Warn(dafnyOptions, reporter, depManager, implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements)); } } public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions dafnyOptions, ErrorReporter reporter, - ProofDependencyManager depManager, DafnyConsolePrinter.ImplementationLogEntry logEntry, - DafnyConsolePrinter.VerificationResultLogEntry result) { - if (result.Outcome != ConditionGeneration.Outcome.Correct) { + ProofDependencyManager depManager, string name, + IReadOnlyList results) { + if (results.Any(r => r.Outcome != SolverOutcome.Valid)) { return; } - var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(logEntry.Name); + var coveredElements = results.SelectMany(r => r.CoveredElements); + + Warn(dafnyOptions, reporter, depManager, name, coveredElements); + } + + private static void Warn(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, + string scopeName, IEnumerable coveredElements) { + var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(scopeName); var usedDependencies = - result - .VCResults - .SelectMany(vcResult => vcResult.CoveredElements.Select(depManager.GetFullIdDependency)) + coveredElements + .Select(depManager.GetFullIdDependency) .OrderBy(dep => dep.Range) .ThenBy(dep => dep.Description); var unusedDependencies = @@ -39,17 +65,17 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions foreach (var unusedDependency in unusedDependencies) { if (dafnyOptions.Get(CommonOptionBag.WarnContradictoryAssumptions)) { if (unusedDependency is ProofObligationDependency obligation) { - if (ShouldWarnVacuous(dafnyOptions, logEntry.Name, obligation)) { - var msg = $"proved using contradictory assumptions: {obligation.Description}"; - var rest = obligation.ProofObligation is AssertStatementDescription - ? ". (Use the `{:contradiction}` attribute on the `assert` statement to silence.)" - : ""; - reporter.Warning(MessageSource.Verifier, "", obligation.Range, msg + rest); + if (ShouldWarnVacuous(dafnyOptions, scopeName, obligation)) { + var message = $"proved using contradictory assumptions: {obligation.Description}"; + if (obligation.ProofObligation is AssertStatementDescription) { + message += ". (Use the `{:contradiction}` attribute on the `assert` statement to silence.)"; + } + reporter.Warning(MessageSource.Verifier, "", obligation.Range, message); } } if (unusedDependency is EnsuresDependency ensures) { - if (ShouldWarnVacuous(dafnyOptions, logEntry.Name, ensures)) { + if (ShouldWarnVacuous(dafnyOptions, scopeName, ensures)) { reporter.Warning(MessageSource.Verifier, "", ensures.Range, $"ensures clause proved using contradictory assumptions"); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index b35e0c097e..82f2a38be2 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -2885,7 +2885,7 @@ Bpl.Function GetOrCreateFunction(Function f) { enum MethodTranslationKind { SpecWellformedness, Call, CoCall, Implementation, OverrideCheck } private static readonly Dictionary kindSanitizedPrefix = - new Dictionary() { + new() { {MethodTranslationKind.SpecWellformedness, "CheckWellFormed"}, {MethodTranslationKind.Call, "Call"}, {MethodTranslationKind.CoCall, "CoCall"}, diff --git a/Source/DafnyCore/Verifier/ProofDependencyManager.cs b/Source/DafnyCore/Verifier/ProofDependencyManager.cs index 0d5522e6ce..52ec364eeb 100644 --- a/Source/DafnyCore/Verifier/ProofDependencyManager.cs +++ b/Source/DafnyCore/Verifier/ProofDependencyManager.cs @@ -19,24 +19,21 @@ namespace Microsoft.Dafny { public class ProofDependencyManager { // proof dependency tracking state public Dictionary ProofDependenciesById { get; } = new(); - private Dictionary> idsByMemberName = new(); + private readonly Dictionary> idsByMemberName = new(); private UInt64 proofDependencyIdCount = 0; - private string currentDefinition = null; + private string currentDefinition; public string GetProofDependencyId(ProofDependency dep) { var idString = $"id{proofDependencyIdCount}"; ProofDependenciesById[idString] = dep; proofDependencyIdCount++; - if (!idsByMemberName.TryGetValue(currentDefinition, out var currentSet)) { - currentSet = new HashSet(); - idsByMemberName[currentDefinition] = currentSet; - } + var currentSet = idsByMemberName.GetOrCreate(currentDefinition, () => new HashSet()); currentSet.Add(dep); return idString; } - public void SetCurrentDefinition(string defName) { - currentDefinition = defName; + public void SetCurrentDefinition(string verificationScopeId) { + currentDefinition = verificationScopeId; } public IEnumerable GetPotentialDependenciesForDefinition(string defName) { @@ -44,7 +41,7 @@ public IEnumerable GetPotentialDependenciesForDefinition(string } public IEnumerable GetAllPotentialDependencies() { - return idsByMemberName.Values.SelectMany(deps => deps); + return idsByMemberName.Values.SelectMany(x => x); } // The "id" attribute on a Boogie AST node is used by Boogie to label diff --git a/Source/DafnyDriver/CliCanVerifyResults.cs b/Source/DafnyDriver/CliCanVerifyResults.cs index e5757e17ca..1d0c19dadc 100644 --- a/Source/DafnyDriver/CliCanVerifyResults.cs +++ b/Source/DafnyDriver/CliCanVerifyResults.cs @@ -1,3 +1,4 @@ +using System; using System.Collections.Concurrent; using System.Collections.Generic; using System.Threading.Tasks; @@ -5,11 +6,9 @@ namespace DafnyDriver.Commands; -struct CliCanVerifyResults { +record CliCanVerifyResults { + public Func TaskFilter = _ => true; public readonly TaskCompletionSource Finished = new(); - public readonly ConcurrentBag<(IImplementationTask, Completed)> CompletedParts = new(); - public readonly ConcurrentBag Tasks = new(); - - public CliCanVerifyResults() { - } + public readonly ConcurrentBag<(IVerificationTask Task, Completed Result)> CompletedParts = new(); + public readonly ConcurrentBag Tasks = new(); } \ No newline at end of file diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index b19e6c5b75..2bb07b3c55 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -12,11 +12,9 @@ using Microsoft.Dafny.LanguageServer.Language; using Microsoft.Dafny.LanguageServer.Language.Symbols; using Microsoft.Dafny.LanguageServer.Workspace; -using Microsoft.Extensions.FileSystemGlobbing; using Microsoft.Extensions.Logging; -using VC; -using IToken = Microsoft.Dafny.IToken; using Token = Microsoft.Dafny.Token; +using Util = Microsoft.Dafny.Util; namespace DafnyDriver.Commands; @@ -127,14 +125,14 @@ Compilation CreateCompilation(ExecutionEngine engine, CompilationInput input) => } public async Task VerifyAllAndPrintSummary() { - var statSum = new PipelineStatistics(); + var statistics = new VerificationStatistics(); var canVerifyResults = new Dictionary(); Compilation.Updates.Subscribe(ev => { if (ev is CanVerifyPartsIdentified canVerifyPartsIdentified) { var canVerifyResult = canVerifyResults[canVerifyPartsIdentified.CanVerify]; - foreach (var part in canVerifyPartsIdentified.Parts) { + foreach (var part in canVerifyPartsIdentified.Parts.Where(canVerifyResult.TaskFilter)) { canVerifyResult.Tasks.Add(part); } @@ -151,27 +149,31 @@ public async Task VerifyAllAndPrintSummary() { if (ev is BoogieUpdate boogieUpdate) { if (boogieUpdate.BoogieStatus is Completed completed) { var canVerifyResult = canVerifyResults[boogieUpdate.CanVerify]; - canVerifyResult.CompletedParts.Add((boogieUpdate.ImplementationTask, completed)); + canVerifyResult.CompletedParts.Add((boogieUpdate.VerificationTask, completed)); switch (completed.Result.Outcome) { - case ConditionGeneration.Outcome.Correct: - case ConditionGeneration.Outcome.ReachedBound: - Interlocked.Increment(ref statSum.VerifiedCount); + case SolverOutcome.Valid: + case SolverOutcome.Bounded: + Interlocked.Increment(ref statistics.VerifiedSymbols); + Interlocked.Add(ref statistics.VerifiedAssertions, completed.Result.Asserts.Count); break; - case ConditionGeneration.Outcome.Errors: - Interlocked.Add(ref statSum.ErrorCount, completed.Result.Errors.Count); + case SolverOutcome.Invalid: + var total = completed.Result.Asserts.Count; + var errors = completed.Result.CounterExamples.Count; + Interlocked.Add(ref statistics.VerifiedAssertions, total - errors); + Interlocked.Add(ref statistics.ErrorCount, errors); break; - case ConditionGeneration.Outcome.TimedOut: - Interlocked.Increment(ref statSum.TimeoutCount); + case SolverOutcome.TimeOut: + Interlocked.Increment(ref statistics.TimeoutCount); break; - case ConditionGeneration.Outcome.OutOfMemory: - Interlocked.Increment(ref statSum.OutOfMemoryCount); + case SolverOutcome.OutOfMemory: + Interlocked.Increment(ref statistics.OutOfMemoryCount); break; - case ConditionGeneration.Outcome.OutOfResource: - Interlocked.Increment(ref statSum.OutOfResourceCount); + case SolverOutcome.OutOfResource: + Interlocked.Increment(ref statistics.OutOfResourceCount); break; - case ConditionGeneration.Outcome.Inconclusive: - Interlocked.Increment(ref statSum.InconclusiveCount); + case SolverOutcome.Undetermined: + Interlocked.Increment(ref statistics.InconclusiveCount); break; default: throw new ArgumentOutOfRangeException(); @@ -192,70 +194,151 @@ public async Task VerifyAllAndPrintSummary() { var canVerifies = resolution.CanVerifies?.DistinctBy(v => v.Tok).ToList(); + var verifiedAssertions = false; if (canVerifies != null) { - canVerifies = FilterCanVerifies(canVerifies); + canVerifies = FilterCanVerifies(canVerifies, out var line); + verifiedAssertions = line != null; var orderedCanVerifies = canVerifies.OrderBy(v => v.Tok.pos).ToList(); foreach (var canVerify in orderedCanVerifies) { - canVerifyResults[canVerify] = new CliCanVerifyResults(); - await Compilation.VerifyCanVerify(canVerify, false); + var results = new CliCanVerifyResults(); + canVerifyResults[canVerify] = results; + if (line != null) { + results.TaskFilter = t => KeepVerificationTask(t, line.Value); + } + + await Compilation.VerifyCanVerify(canVerify, results.TaskFilter); } foreach (var canVerify in orderedCanVerifies) { var results = canVerifyResults[canVerify]; try { + var timeLimitSeconds = TimeSpan.FromSeconds(options.Get(BoogieOptionBag.VerificationTimeLimit)); + var tasks = new List() { results.Finished.Task }; + if (timeLimitSeconds.Seconds != 0) { + tasks.Add(Task.Delay(timeLimitSeconds)); + } + await Task.WhenAny(tasks); + if (!results.Finished.Task.IsCompleted) { + Compilation.Reporter.Error(MessageSource.Verifier, canVerify.Tok, + "Dafny encountered an internal error while waiting for this symbol to verify. Please report it at .\n"); + break; + } await results.Finished.Task; - foreach (var (task, completed) in results.CompletedParts.OrderBy(t => t.Item1.Implementation.Name)) { - foreach (var vcResult in completed.Result.VCResults) { - Compilation.ReportDiagnosticsInResult(options, task, vcResult, Compilation.Reporter); - } - - ProofDependencyWarnings.WarnAboutSuspiciousDependenciesForImplementation(options, - resolution.ResolvedProgram!.Reporter, - resolution.ResolvedProgram.ProofDependencyManager, - new DafnyConsolePrinter.ImplementationLogEntry(task.Implementation.VerboseName, - task.Implementation.tok), - DafnyConsolePrinter.DistillVerificationResult(completed.Result)); + + // We use an intermediate reporter so we can sort the diagnostics from all parts by token + var batchReporter = new BatchErrorReporter(options); + foreach (var (task, completed) in results.CompletedParts) { + Compilation.ReportDiagnosticsInResult(options, task, 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); } + + var parts = results.CompletedParts; + ProofDependencyWarnings.ReportSuspiciousDependencies(options, parts, + resolution.ResolvedProgram.Reporter, resolution.ResolvedProgram.ProofDependencyManager); + } catch (ProverException e) { - Interlocked.Increment(ref statSum.SolverExceptionCount); + Interlocked.Increment(ref statistics.SolverExceptionCount); Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, e.Message); } catch (Exception e) { - Interlocked.Increment(ref statSum.SolverExceptionCount); + Interlocked.Increment(ref statistics.SolverExceptionCount); Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, $"Internal error occurred during verification: {e.Message}\n{e.StackTrace}"); } } } - SynchronousCliCompilation.WriteTrailer(options, /* TODO ErrorWriter? */ options.OutputWriter, statSum); + WriteTrailer(options, /* TODO ErrorWriter? */ options.OutputWriter, verifiedAssertions, statistics); } catch (OperationCanceledException) { // Failed to resolve the program due to a user error. } } - private List FilterCanVerifies(List canVerifies) { + private bool KeepVerificationTask(IVerificationTask task, int line) { + return task.ScopeToken.line == line || task.Token.line == line; + } + + private List FilterCanVerifies(List canVerifies, out int? line) { var filterPosition = options.Get(VerifyCommand.FilterPosition); if (filterPosition == null) { + line = null; return canVerifies; } - var regex = new Regex(@"(.+)(?::(\d+))?", RegexOptions.RightToLeft); + var regex = new Regex(@"(.*)(?::(\d+))?", RegexOptions.RightToLeft); var result = regex.Match(filterPosition); if (result.Length != filterPosition.Length || !result.Success) { Compilation.Reporter.Error(MessageSource.Project, Token.Cli, "Could not parse value passed to --filter-position"); + line = null; return new List(); } var filePart = result.Groups[1].Value; string? linePart = result.Groups.Count > 2 ? result.Groups[2].Value : null; var fileFiltered = canVerifies.Where(c => c.Tok.Uri.ToString().EndsWith(filePart)).ToList(); if (string.IsNullOrEmpty(linePart)) { + line = null; return fileFiltered; } - var line = int.Parse(linePart); + var parsedLine = int.Parse(linePart); + line = parsedLine; return fileFiltered.Where(c => - c.RangeToken.StartToken.line <= line && line <= c.RangeToken.EndToken.line).ToList(); + c.RangeToken.StartToken.line <= parsedLine && parsedLine <= c.RangeToken.EndToken.line).ToList(); + } + + static void WriteTrailer(DafnyOptions options, TextWriter output, bool reportAssertions, VerificationStatistics statistics) { + if (options.Verbosity <= CoreOptions.VerbosityLevel.Quiet) { + return; + } + + output.WriteLine(); + + if (reportAssertions) { + output.Write("{0} finished with {1} assertions verified, {2} error{3}", options.DescriptiveToolName, + statistics.VerifiedAssertions, statistics.ErrorCount, + Util.Plural(statistics.ErrorCount)); + + } else { + output.Write("{0} finished with {1} verified, {2} error{3}", options.DescriptiveToolName, + statistics.VerifiedSymbols, statistics.ErrorCount, + Util.Plural(statistics.ErrorCount)); + }; + if (statistics.InconclusiveCount != 0) { + output.Write(", {0} inconclusive{1}", statistics.InconclusiveCount, Util.Plural(statistics.InconclusiveCount)); + } + + if (statistics.TimeoutCount != 0) { + output.Write(", {0} time out{1}", statistics.TimeoutCount, Util.Plural(statistics.TimeoutCount)); + } + + if (statistics.OutOfMemoryCount != 0) { + output.Write(", {0} out of memory", statistics.OutOfMemoryCount); + } + + if (statistics.OutOfResourceCount != 0) { + output.Write(", {0} out of resource", statistics.OutOfResourceCount); + } + + if (statistics.SolverExceptionCount != 0) { + output.Write(", {0} solver exceptions", statistics.SolverExceptionCount); + } + + output.WriteLine(); + output.Flush(); } +} + +record VerificationStatistics { + public int ErrorCount; + public int VerifiedAssertions; + public int VerifiedSymbols; + public int InconclusiveCount; + public int TimeoutCount; + public int OutOfResourceCount; + public int OutOfMemoryCount; + public int SolverExceptionCount; } \ No newline at end of file diff --git a/Source/DafnyDriver/JsonVerificationLogger.cs b/Source/DafnyDriver/JsonVerificationLogger.cs index b9557a7065..58d56ad960 100644 --- a/Source/DafnyDriver/JsonVerificationLogger.cs +++ b/Source/DafnyDriver/JsonVerificationLogger.cs @@ -67,17 +67,17 @@ private static JsonNode SerializeTimeSpan(TimeSpan timeSpan) { return timeSpan.ToString(); } - private static JsonNode SerializeOutcome(ProverInterface.Outcome outcome) { + private static JsonNode SerializeOutcome(SolverOutcome outcome) { return outcome.ToString(); } - private static JsonNode SerializeOutcome(ConditionGeneration.Outcome outcome) { + private static JsonNode SerializeOutcome(VcOutcome outcome) { return outcome.ToString(); } private JsonNode SerializeVerificationResult(DafnyConsolePrinter.ConsoleLogEntry logEntry) { var (impl, verificationResult) = logEntry; var trackProofDependencies = - verificationResult.Outcome == ConditionGeneration.Outcome.Correct && + verificationResult.Outcome == VcOutcome.Correct && verificationResult.VCResults.Any(vcResult => vcResult.CoveredElements.Any()); var potentialDependencies = trackProofDependencies ? depManager.GetPotentialDependenciesForDefinition(impl.Name) : null; diff --git a/Source/DafnyDriver/SynchronousCliCompilation.cs b/Source/DafnyDriver/SynchronousCliCompilation.cs index e402fc765f..70f12a922a 100644 --- a/Source/DafnyDriver/SynchronousCliCompilation.cs +++ b/Source/DafnyDriver/SynchronousCliCompilation.cs @@ -328,7 +328,7 @@ public async Task ProcessFilesAsync(IReadOnlyList/*!* private static void PrintCounterexample(DafnyOptions options) { var firstCounterexample = (options.Printer as DafnyConsolePrinter).VerificationResults .Select(result => result.Result) - .Where(result => result.Outcome == ConditionGeneration.Outcome.Errors) + .Where(result => result.Outcome == VcOutcome.Errors) .Select(result => result.Counterexamples) .Where(counterexampleList => counterexampleList != null) .Select(counterexampleList => counterexampleList.FirstOrDefault(counterexample => counterexample.Model != null)) diff --git a/Source/DafnyDriver/TextVerificationLogger.cs b/Source/DafnyDriver/TextVerificationLogger.cs index 6839b6008f..7cb0c0fba3 100644 --- a/Source/DafnyDriver/TextVerificationLogger.cs +++ b/Source/DafnyDriver/TextVerificationLogger.cs @@ -44,7 +44,7 @@ public void LogResults(IEnumerable verifica $" {cmd.Tok.filename}({cmd.Tok.line},{cmd.Tok.col}): {cmd.Description}"); } - if (vcResult.CoveredElements.Any() && vcResult.Outcome == ProverInterface.Outcome.Valid) { + if (vcResult.CoveredElements.Any() && vcResult.Outcome == SolverOutcome.Valid) { tw.WriteLine(""); tw.WriteLine(" Proof dependencies:"); var fullDependencies = depManager.GetOrderedFullDependencies(vcResult.CoveredElements); diff --git a/Source/DafnyDriver/VerificationResultLogger.cs b/Source/DafnyDriver/VerificationResultLogger.cs index ec7e4b0a10..433a598519 100644 --- a/Source/DafnyDriver/VerificationResultLogger.cs +++ b/Source/DafnyDriver/VerificationResultLogger.cs @@ -110,7 +110,7 @@ private static IEnumerable VerificationToTestResults(IEnumerable<(Da Duration = vcResult.RunTime }; testResult.SetPropertyValue(ResourceCountProperty, vcResult.ResourceCount); - if (vcResult.Outcome == ProverInterface.Outcome.Valid) { + if (vcResult.Outcome == SolverOutcome.Valid) { testResult.Outcome = TestOutcome.Passed; } else { testResult.Outcome = TestOutcome.Failed; diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs index 5a083df51e..52338f307c 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs @@ -25,10 +25,10 @@ await SetUp(options => { options.Set(LanguageServer.VerifySnapshots, 1U); }); await VerifyTrace(@" - . S S | I $ | :method test() { - . S | | I $ | : assert true; - . S S | I $ | : //Replace: - . S S | I $ | :}", true); + . S | I $ | :method test() { + . S | I $ | : assert true; + . S | I $ | : //Replace: + . S | I $ | :}", true); } [Fact] @@ -38,11 +38,11 @@ await SetUp(options => { options.Set(LanguageServer.VerifySnapshots, 1U); }); await VerifyTrace(@" - . S [S][ ][I][S][S][ ]:method test() { - . S [O][O][o][Q][O][O]: assert true; - . S [=][=][-][~][=][=]: assert false; - . S [S][ ][I][S][S][ ]: //Replace: - . S [S][ ][I][S][S][ ]:}", false, "ensureCachingDoesNotHideErrors.dfy"); + . S [ ][I][S][ ]:method test() { + . S [O][o][Q][O]: assert true; + . S [=][-][~][=]: assert false; + . S [ ][I][S][ ]: //Replace: + . S [ ][I][S][ ]:}", false, "ensureCachingDoesNotHideErrors.dfy"); } public CachedLinearVerificationGutterStatusTester(ITestOutputHelper output) : base(output) { diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs index 28eb9969f5..d6430856cb 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs @@ -45,14 +45,14 @@ public async Task EnsuresManyDocumentsCanBeVerifiedAtOnce() { // That way, it can rebuild the trace for every file independently. for (var i = 0; i < MaxSimultaneousVerificationTasks; i++) { result.Add(VerifyTrace(@" - . | | | | I | | | :predicate F(i: int) { - . | | | | I | | | : false // Should not be highlighted in gutter. - . | | | | I | | | :} - | | | | I | | | : - . . S [S][ ][I][I][S][ ]:method H() - . . S [=][=][-][-][~][O]: ensures F(1) - . . S [=][=][-][-][~][=]:{//Replace: { assert false; - . . S [S][ ][I][I][S][ ]:}", false, $"EnsuresManyDocumentsCanBeVerifiedAtOnce{i}.dfy", true, true, verificationStatusGutterReceivers[i])); + . | | | I | | | :predicate F(i: int) { + . | | | I | | | : false // Should not be highlighted in gutter. + . | | | I | | | :} + | | | I | | | : + . . S [ ][I][I][S][ ]:method H() + . . S [=][-][-][~][O]: ensures F(1) + . . S [=][-][-][~][=]:{//Replace: { assert false; + . . S [ ][I][I][S][ ]:}", false, $"EnsuresManyDocumentsCanBeVerifiedAtOnce{i}.dfy", true, true, verificationStatusGutterReceivers[i])); } for (var i = 0; i < MaxSimultaneousVerificationTasks; i++) { diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs index 5f54eeb8e2..2ad64631be 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs @@ -65,6 +65,9 @@ await VerifyTrace(@" [Fact] public async Task GitIssue3821GutterIgnoredProblem() { + await SetUp(options => { + options.Set(BoogieOptionBag.Cores, 1u); + }); await VerifyTrace(@" | :function fib(n: nat): nat { | : if n <= 1 then n else fib(n-1) + fib(n-2) @@ -101,61 +104,61 @@ await VerifyTrace(@" public async Task EnsureVerificationGutterStatusIsWorking() { await SetUp(o => o.Set(CommonOptionBag.RelaxDefiniteAssignment, true)); await VerifyTrace(@" - . | | | | | I I | | | | :predicate Ok() { - . | | | | | I I | | | | : true - . | | | | | I I | | | | :} - | | | | | I I | | | | : - . . . S [S][ ][I][I][I][I][S] | :method Test(x: bool) returns (i: int) - . . . S [=][=][-][-][-][-][~] | : ensures i == 2 - . . . S [S][ ][I][I][I][I][S] | :{ - . . . S [S][ ][I][I][I][I][S] | : if x { - . . . S [S][ ][I][I][I][I][S] | : i := 2; - . . . S [=][=][-][-][-][-][~] | : } else { - . . . S [S][ ]/!\[I][I][I][S] | : i := 1; //Replace1: i := /; //Replace2: i := 2; - . . . S [S][ ][I][I][I][I][S] | : } - . . . S [S][ ][I][I][I][I][S] | :} - | | | | I I I | | | : - . . | | | | I I I | | | :predicate OkBis() { - . . | | | | I I I | | | : false - . . | | | | I I I | | | :}", true); + . | | | | I I | | | | :predicate Ok() { + . | | | | I I | | | | : true + . | | | | I I | | | | :} + | | | | I I | | | | : + . . . S [ ][I][I][I][I][S] | :method Test(x: bool) returns (i: int) + . . . S [=][-][-][-][-][~] | : ensures i == 2 + . . . S [ ][I][I][I][I][S] | :{ + . . . S [ ][I][I][I][I][S] | : if x { + . . . S [ ][I][I][I][I][S] | : i := 2; + . . . S [=][-][-][-][-][~] | : } else { + . . . S [ ]/!\[I][I][I][S] | : i := 1; //Replace1: i := /; //Replace2: i := 2; + . . . S [ ][I][I][I][I][S] | : } + . . . S [ ][I][I][I][I][S] | :} + | | | I I I | | | : + . . | | | I I I | | | :predicate OkBis() { + . . | | | I I I | | | : false + . . | | | I I I | | | :}", true); } [Fact] public async Task EnsuresItWorksForSubsetTypes() { await VerifyTrace(@" - | | | | | I I | | | | | I I | | | | | :// The maximum Id - . | | | | | I I | | | | | I I | | | | | :ghost const maxId := 200; - | | | | | I I | | | | | I I | | | | | : - . . | | | | I I I | | | | I I I | | | | :ghost predicate isIssueIdValid(issueId: int) { - . . | | | | I I I | | | | I I I | | | | : 101 <= issueId < maxId - . . | | | | I I I | | | | I I I | | | | :} - | | | | I I I | | | | I I I | | | | : - . . . S S | I . . . S S [=] I . . . S S | :type IssueId = i : int | isIssueIdValid(i) - . . . S | | I . . . S | [=] I . . . S | | : witness 101 //Replace1: witness 99 //Replace2: witness 101 ", false, "EnsuresItWorksForSubsetTypes.dfy"); + | | | | I I | | | | I I | | | | :// The maximum Id + . | | | | I I | | | | I I | | | | :ghost const maxId := 200; + | | | | I I | | | | I I | | | | : + . . | | | I I I | | | I I I | | | :ghost predicate isIssueIdValid(issueId: int) { + . . | | | I I I | | | I I I | | | : 101 <= issueId < maxId + . . | | | I I I | | | I I I | | | :} + | | | I I I | | | I I I | | | : + . . . S | I . . . S [=] I . . . S | :type IssueId = i : int | isIssueIdValid(i) + . . . S | I . . . S [=] I . . . S | : witness 101 //Replace1: witness 99 //Replace2: witness 101 ", false, "EnsuresItWorksForSubsetTypes.dfy"); } [Fact] public async Task EnsureItWorksForPostconditionsRelatedOutside() { await VerifyTrace(@" - . | | | | :predicate F(i: int) { - . | | | | : false // Should not be highlighted in gutter. - . | | | | :} - | | | | : - . . S [S][ ]:method H() - . . S [=][=]: ensures F(1) - . . S [=][=]:{ - . . S [S][ ]:}", true); + . | | | :predicate F(i: int) { + . | | | : false // Should not be highlighted in gutter. + . | | | :} + | | | : + . . S [ ]:method H() + . . S [=]: ensures F(1) + . . S [=]:{ + . . S [ ]:}", true); } [Fact(Timeout = MaxTestExecutionTimeMs * 10)] public async Task EnsureNoAssertShowsVerified() { for (var i = 0; i < 10; i++) { await VerifyTrace(@" - . | | | | I I | :predicate P(x: int) - | | | | I I | : - . . S [S][ ][I] | | :method Main() { - . . S [=][=][I] | | : ghost var x :| P(x); //Replace: ghost var x := 1; - . . S [S][ ][I] | | :} - | | :// Comment to not trim this line", false, $"EnsureNoAssertShowsVerified{i}.dfy"); + . | | | I I | :predicate P(x: int) + | | | I I | : + . . S [ ][I] | | :method Main() { + . . S [=][I] | | : ghost var x :| P(x); //Replace: ghost var x := 1; + . . S [ ][I] | | :} + | | :// Comment to not trim this line", false, $"EnsureNoAssertShowsVerified{i}.dfy"); } } @@ -178,87 +181,87 @@ await VerifyTrace(@" [Fact/*(Timeout = MaxTestExecutionTimeMs)*/] public async Task EnsuresDefaultArgumentsShowsError() { await VerifyTrace(@" - . S [~][=]:datatype D = T(i: nat := -2)", true); + . S [=]:datatype D = T(i: nat := -2)", true); } [Fact/*(Timeout = MaxTestExecutionTimeMs)*/] public async Task TopLevelConstantsHaveToBeVerifiedAlso() { await VerifyTrace(@" - | | | | :// The following should trigger only one error - . | | | | :ghost const a := [1, 2]; - | | | | : - . . S [~][=]:ghost const b := a[-1];", false); + | | | :// The following should trigger only one error + . | | | :ghost const a := [1, 2]; + | | | : + . . S [=]:ghost const b := a[-1];", false); } [Fact/*(Timeout = MaxTestExecutionTimeMs)*/] public async Task EnsuresAddingNewlinesMigratesPositions() { await VerifyTrace(@" - . S [S][ ][I][S][ ][I][S][ ]:method f(x: int) { - . S [S][ ][I][S][ ][I][S][ ]: //Replace1:\n //Replace2:\\n - . S [=][=][I][S][ ][I][S][ ]: assert x == 2; } -############[-][~][=][I][S][ ]: -#####################[-][~][=]:", true, "EnsuresAddingNewlinesMigratesPositions.dfy"); + . S [ ][I][S][ ][I][S][ ]:method f(x: int) { + . S [ ][I][S][ ][I][S][ ]: //Replace1:\n //Replace2:\\n + . S [=][I][S][ ][I][S][ ]: assert x == 2; } +#########[-][~][=][I][S][ ]: +##################[-][~][=]:", true, "EnsuresAddingNewlinesMigratesPositions.dfy"); } [Fact/*(Timeout = MaxTestExecutionTimeMs)*/] public async Task EnsuresWorkWithInformationsAsWell() { await SetUp(o => o.Set(CommonOptionBag.RelaxDefiniteAssignment, true)); await VerifyTrace(@" - . S [S][ ][I][S][S][ ]:method f(x: int) returns (y: int) - . S [S][ ][I][S][S][ ]:ensures - . S [=][=][-][~][=][=]: x > 3 { y := x; - . S [S][ ][I][S][S][ ]: //Replace1:\n - . S [=][=][-][~][=][ ]: while(y <= 1) invariant y >= 2 { - . S [S][ ][-][~][~][=]: y := y + 1; - . S [S][ ][I][S][S][ ]: } - . S [S][ ][I][S][S][ ]:} -############[I][S][S][ ]:", false); + . S [ ][I][S][ ]:method f(x: int) returns (y: int) + . S [ ][I][S][ ]:ensures + . S [=][-][~][=]: x > 3 { y := x; + . S [ ][I][S][ ]: //Replace1:\n + . S [=][-][~][ ]: while(y <= 1) invariant y >= 2 { + . S [ ][-][~][=]: y := y + 1; + . S [ ][I][S][ ]: } + . S [ ][I][S][ ]:} +#########[I][S][ ]:", false); } [Fact] public async Task EnsureMultilineAssertIsCorreclyHandled() { await VerifyTrace(@" - . S [S][ ]:method x() { - . S [=][=]: assert false - . S [=][=]: || false; - . S [S][ ]:}", true); + . S [ ]:method x() { + . S [=]: assert false + . S [=]: || false; + . S [ ]:}", true); } [Fact] public async Task EnsureBodylessMethodsAreCovered() { await VerifyTrace(@" - . | | | | | :method test() { - . | | | | | :} - | | | | | : - . . . S [S][ ]:method {:extern} test3(a: nat, b: nat) - . . . S [S][ ]: ensures true - . . . S [=][=]: ensures test2(a - b) - . . . S [S][ ]: ensures true - . . . S [O][O]: ensures test2(a - b) - . . . S [S][ ]: ensures true - | | | | : - . . | | | | :predicate test2(x: nat) { - . . | | | | : true - . . | | | | :}", false); + . | | | | :method test() { + . | | | | :} + | | | | : + . . . S [ ]:method {:extern} test3(a: nat, b: nat) + . . . S [ ]: ensures true + . . . S [=]: ensures test2(a - b) + . . . S [ ]: ensures true + . . . S [O]: ensures test2(a - b) + . . . S [ ]: ensures true + | | | : + . . | | | :predicate test2(x: nat) { + . . | | | : true + . . | | | :}", false); } [Fact] public async Task EnsureBodylessFunctionsAreCovered() { await VerifyTrace(@" - . | | | | | :method test() { - . | | | | | :} - | | | | | : - . . . S [S][ ]:function {:extern} test4(a: nat, b: nat): nat - . . . S [S][ ]: ensures true - . . . S [=][=]: ensures test2(a - b) - . . . S [S][ ]: ensures true - . . . S [O][O]: ensures test2(a - b) - . . . S [S][ ]: ensures true - | | | | : - . . | | | | :predicate test2(x: nat) { - . . | | | | : true - . . | | | | :}", true); + . | | | | :method test() { + . | | | | :} + | | | | : + . . . S [ ]:function {:extern} test4(a: nat, b: nat): nat + . . . S [ ]: ensures true + . . . S [=]: ensures test2(a - b) + . . . S [ ]: ensures true + . . . S [O]: ensures test2(a - b) + . . . S [ ]: ensures true + | | | : + . . | | | :predicate test2(x: nat) { + . . | | | : true + . . | | | :}", true); } public SimpleLinearVerificationGutterStatusTester(ITestOutputHelper output) : base(output) { diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index 21fe1e30c2..5648a76d36 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -93,6 +93,7 @@ await SetUp(options => { _ = client.RunSymbolVerification(documentItem1, new Position(0, 7), CancellationToken); _ = client.RunSymbolVerification(documentItem1, new Position(4, 7), CancellationToken); while (true) { + CancellationToken.ThrowIfCancellationRequested(); var status = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); if (status.NamedVerifiables.Count(v => v.Status == PublishedVerificationStatus.Queued) == 2) { Assert.Contains(status.NamedVerifiables, v => v.Status == PublishedVerificationStatus.Stale); @@ -105,6 +106,7 @@ await SetUp(options => { } while (true) { + CancellationToken.ThrowIfCancellationRequested(); var status = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); if (status.NamedVerifiables.Count(v => v.Status == PublishedVerificationStatus.Stale) > 1) { Assert.Fail("May not become stale after both being queued. "); diff --git a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs index 511109f223..d2660587b5 100644 --- a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs +++ b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs @@ -93,7 +93,7 @@ public CrashingVerifier(ExceptionTests tests, IProgramVerifier verifier) { this.verifier = verifier; } - public Task> GetVerificationTasksAsync(ExecutionEngine engine, + public Task> GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken) { if (tests.CrashOnPrepareVerification) { diff --git a/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs b/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs index c75033ea95..e1edd55907 100644 --- a/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs +++ b/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs @@ -6,8 +6,8 @@ using System.Threading.Tasks; using Microsoft.Boogie; using Microsoft.Dafny.LanguageServer.Language; -using Microsoft.Dafny.LanguageServer.Workspace; using Microsoft.Extensions.Logging; +using VC; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; @@ -21,7 +21,7 @@ public SlowVerifier(ILogger logger) { private readonly DafnyProgramVerifier verifier; - public async Task> GetVerificationTasksAsync(ExecutionEngine engine, + public async Task> GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken) { var program = resolution.ResolvedProgram; var attributes = program.Modules().SelectMany(m => { @@ -36,18 +36,20 @@ public async Task> GetVerificationTasksAsync( return tasks; } - class NeverVerifiesImplementationTask : IImplementationTask { - private readonly IImplementationTask original; + class NeverVerifiesImplementationTask : IVerificationTask { + private readonly IVerificationTask original; private readonly Subject source; - public NeverVerifiesImplementationTask(IImplementationTask original) { + public NeverVerifiesImplementationTask(IVerificationTask original) { this.original = original; source = new(); } public IVerificationStatus CacheStatus => new Stale(); - public ProcessedProgram ProcessedProgram => original.ProcessedProgram; - public Implementation Implementation => original.Implementation; + public ManualSplit Split => original.Split; + public Boogie.IToken ScopeToken => original.ScopeToken; + public string ScopeId => original.ScopeId; + public Boogie.IToken Token => original.Token; public IObservable TryRun() { return source; diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs index 4b9fea9140..0ef3ba91df 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs @@ -57,7 +57,7 @@ private static void PublishSolverPath(ILanguageServer server) { var proverOptions = new SMTLibSolverOptions(options); proverOptions.Parse(options.ProverOptions); solverPath = proverOptions.ExecutablePath(); - HandleZ3Version(options, telemetryPublisher, proverOptions); + HandleZ3Version(telemetryPublisher, proverOptions); } catch (Exception e) { solverPath = $"Error while determining solver path: {e}"; } @@ -65,22 +65,13 @@ private static void PublishSolverPath(ILanguageServer server) { telemetryPublisher.PublishSolverPath(solverPath); } - private static void HandleZ3Version(DafnyOptions options, TelemetryPublisherBase telemetryPublisher, SMTLibSolverOptions proverOptions) { + private static void HandleZ3Version(TelemetryPublisherBase telemetryPublisher, SMTLibSolverOptions proverOptions) { var z3Version = DafnyOptions.GetZ3Version(proverOptions.ProverPath); - if (z3Version is null || z3Version < new Version(4, 8, 6)) { + if (z3Version is null) { return; } telemetryPublisher.PublishZ3Version($"Z3 version {z3Version}"); - - var toReplace = "O:model_compress=false"; - var i = options.ProverOptions.IndexOf(toReplace); - if (i == -1) { - telemetryPublisher.PublishUnhandledException(new Exception($"Z3 version is > 4.8.6 but I did not find {toReplace} in the prover options:" + string.Join(" ", options.ProverOptions))); - return; - } - - options.ProverOptions[i] = "O:model.compact=false"; } /// diff --git a/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs b/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs index f50b1932b4..0ccca4b0bf 100644 --- a/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs +++ b/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs @@ -2,13 +2,5 @@ using System.Collections.Generic; namespace Microsoft.Dafny.LanguageServer.Handlers.Custom { - public class CounterExampleItem { - public Position Position { get; } - public IDictionary Variables { get; } - - public CounterExampleItem(Position position, IDictionary variables) { - Position = position; - Variables = variables; - } - } + public record CounterExampleItem(Position Position, IDictionary Variables); } diff --git a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs index 3df1385be3..9e4d9996c1 100644 --- a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs @@ -38,7 +38,7 @@ public async Task Handle(CounterExampleParams request, Cance var state = await projectManager.States. Where(s => FinishedVerifyingUri(s, uri)).FirstAsync(); logger.LogDebug($"counter-example handler retrieved IDE state, " + - $"canVerify count: {state.VerificationResults[uri].Count}, " + + $"canVerify count: {state.CanVerifyStates[uri].Count}, " + $"counterExample count: {state.Counterexamples.Count}"); return new CounterExampleLoader(options, logger, state, request.CounterExampleDepth, cancellationToken).GetCounterExamples(); } @@ -58,9 +58,9 @@ public async Task Handle(CounterExampleParams request, Cance private static bool FinishedVerifyingUri(IdeState s, Uri uri) { return s.Status == CompilationStatus.ResolutionSucceeded && - s.VerificationResults[uri].Values.All(r => + s.CanVerifyStates[uri].Values.All(r => r.PreparationProgress == VerificationPreparationState.Done && - r.Implementations.Values.All(v => v.Status >= PublishedVerificationStatus.Error)); + r.VerificationTasks.Values.All(v => v.Status >= PublishedVerificationStatus.Error)); } private class CounterExampleLoader { diff --git a/Source/DafnyLanguageServer/Language/AssertionBatchCompletedObserver.cs b/Source/DafnyLanguageServer/Language/AssertionBatchCompletedObserver.cs index 7c0a54bbe1..9b59bf09a7 100644 --- a/Source/DafnyLanguageServer/Language/AssertionBatchCompletedObserver.cs +++ b/Source/DafnyLanguageServer/Language/AssertionBatchCompletedObserver.cs @@ -16,7 +16,7 @@ public OutputLogger(ILogger logger) { public void AdvisoryWriteLine(TextWriter writer, string format, params object[] args) { } - public void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result) { + public void ReportEndVerifyImplementation(Implementation implementation, ImplementationRunResult result) { } public ExecutionEngineOptions? Options { get; set; } diff --git a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs index ba413a3d65..71359c62e6 100644 --- a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs +++ b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs @@ -25,7 +25,7 @@ public DafnyProgramVerifier(ILogger logger) { this.logger = logger; } - public async Task> GetVerificationTasksAsync(ExecutionEngine engine, + public async Task> GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken) { @@ -61,7 +61,7 @@ public async Task> GetVerificationTasksAsync( ExecutionEngine.PrintBplFile(engine.Options, fileName, boogieProgram, false, false, engine.Options.PrettyPrint); } - return engine.GetImplementationTasks(boogieProgram); + return engine.GetVerificationTasks(boogieProgram); } finally { mutex.Release(); diff --git a/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs b/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs index be118a92c2..14f095438d 100644 --- a/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs +++ b/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs @@ -2,12 +2,10 @@ using System.CommandLine; using System.Linq; using Microsoft.Boogie; -using Microsoft.Dafny.LanguageServer.Language; using Microsoft.Dafny.LanguageServer.Workspace.Notifications; using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using VC; -using VerificationResult = Microsoft.Boogie.VerificationResult; namespace Microsoft.Dafny.LanguageServer.Workspace; @@ -177,11 +175,9 @@ public virtual void ReportImplementationsBeforeVerification(IdeState state, ICan canVerifyNode.ResetNewChildren(); - TopLevelDeclMemberVerificationTree? targetMethodNode; - ImplementationVerificationTree newImplementationNode; foreach (var implementation in implementations) { - targetMethodNode = GetTargetMethodTree(tree, implementation, out var oldImplementationNode, true); + var targetMethodNode = GetTargetMethodTree(tree, implementation, out var oldImplementationNode, true); if (targetMethodNode == null) { NoMethodNodeAtLogging(tree, "ReportImplementationsBeforeVerification", state, implementation); continue; @@ -189,7 +185,7 @@ public virtual void ReportImplementationsBeforeVerification(IdeState state, ICan var newDisplayName = targetMethodNode.DisplayName + " #" + (targetMethodNode.Children.Count + 1) + ":" + implementation.Name; - newImplementationNode = new ImplementationVerificationTree( + var newImplementationNode = new ImplementationVerificationTree( newDisplayName, implementation.VerboseName, implementation.Name, @@ -249,7 +245,9 @@ public void ReportVerifyImplementationRunning(IdeState state, Implementation imp /// /// Called when the verifier finished to visit an implementation /// - public void ReportEndVerifyImplementation(IdeState state, Implementation implementation, VerificationResult verificationResult) { + public void ReportEndVerifyImplementation(IdeState state, Implementation implementation, + int implementationResourceCount, + VcOutcome implementationOutcome) { var uri = ((IToken)implementation.tok).Uri; var tree = state.VerificationTrees[uri]; @@ -262,18 +260,18 @@ public void ReportEndVerifyImplementation(IdeState state, Implementation impleme } else { lock (LockProcessing) { implementationNode.Stop(); - implementationNode.ResourceCount = verificationResult.ResourceCount; - targetMethodNode.ResourceCount += verificationResult.ResourceCount; - var finalOutcome = verificationResult.Outcome switch { - ConditionGeneration.Outcome.Correct => GutterVerificationStatus.Verified, + implementationNode.ResourceCount = implementationResourceCount; + targetMethodNode.ResourceCount += implementationResourceCount; + var finalOutcome = implementationOutcome switch { + VcOutcome.Correct => GutterVerificationStatus.Verified, _ => GutterVerificationStatus.Error }; implementationNode.StatusVerification = finalOutcome; // Will be only executed by the last instance. if (!targetMethodNode.Children.All(child => child.Finished)) { - targetMethodNode.StatusVerification = verificationResult.Outcome switch { - ConditionGeneration.Outcome.Correct => targetMethodNode.StatusVerification, + targetMethodNode.StatusVerification = implementationOutcome switch { + VcOutcome.Correct => targetMethodNode.StatusVerification, _ => GutterVerificationStatus.Error }; } else { @@ -317,16 +315,16 @@ public void ReportAssertionBatchResult(IdeState ideState, AssertionBatchResult b } else { var wasAlreadyProcessed = implementationNode.NewChildren.Any(assertNode => assertNode is AssertionVerificationTree assertionNode - && assertionNode.AssertionBatchNum == result.vcNum); + && assertionNode.AssertionBatchNum == result.VcNum); if (wasAlreadyProcessed) { return; } result.ComputePerAssertOutcomes(out var perAssertOutcome, out var perAssertCounterExample); - var assertionBatchTime = (int)result.runTime.TotalMilliseconds; - var assertionBatchResourceCount = result.resourceCount; - implementationNode.AddAssertionBatchMetrics(result.vcNum, assertionBatchTime, assertionBatchResourceCount, result.coveredElements.ToList()); + var assertionBatchTime = (int)result.RunTime.TotalMilliseconds; + var assertionBatchResourceCount = result.ResourceCount; + implementationNode.AddAssertionBatchMetrics(result.VcNum, assertionBatchTime, assertionBatchResourceCount, result.CoveredElements.ToList()); // Attaches the trace void AddChildOutcome(Counterexample? counterexample, AssertCmd assertCmd, IToken token, @@ -354,7 +352,7 @@ void AddChildOutcome(Counterexample? counterexample, AssertCmd assertCmd, IToken ) { StatusVerification = status, StatusCurrent = CurrentStatus.Current, - AssertionBatchNum = result.vcNum, + AssertionBatchNum = result.VcNum, Started = true, Finished = true }.WithDuration(implementationNode.StartTime, assertionBatchTime) @@ -435,15 +433,15 @@ void AddChildOutcome(Counterexample? counterexample, AssertCmd assertCmd, IToken /// /// The outcome set by the split result /// The matching verification status - private static GutterVerificationStatus GetNodeStatus(ProverInterface.Outcome outcome) { + private static GutterVerificationStatus GetNodeStatus(SolverOutcome outcome) { return outcome switch { - ProverInterface.Outcome.Valid => GutterVerificationStatus.Verified, - ProverInterface.Outcome.Invalid => GutterVerificationStatus.Error, - ProverInterface.Outcome.Undetermined => GutterVerificationStatus.Inconclusive, - ProverInterface.Outcome.TimeOut => GutterVerificationStatus.Error, - ProverInterface.Outcome.OutOfMemory => GutterVerificationStatus.Error, - ProverInterface.Outcome.OutOfResource => GutterVerificationStatus.Error, - ProverInterface.Outcome.Bounded => GutterVerificationStatus.Error, + SolverOutcome.Valid => GutterVerificationStatus.Verified, + SolverOutcome.Invalid => GutterVerificationStatus.Error, + SolverOutcome.Undetermined => GutterVerificationStatus.Inconclusive, + SolverOutcome.TimeOut => GutterVerificationStatus.Error, + SolverOutcome.OutOfMemory => GutterVerificationStatus.Error, + SolverOutcome.OutOfResource => GutterVerificationStatus.Error, + SolverOutcome.Bounded => GutterVerificationStatus.Error, _ => GutterVerificationStatus.Error }; } diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index f75e6bfa66..83dab60a87 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -17,11 +17,13 @@ namespace Microsoft.Dafny.LanguageServer.Workspace; -public record IdeImplementationView(Range Range, PublishedVerificationStatus Status, - IReadOnlyList Diagnostics, bool HitErrorLimit); +public record IdeVerificationTaskState(Range Range, PublishedVerificationStatus Status, + IReadOnlyList Diagnostics, bool HitErrorLimit, IVerificationTask Task, IVerificationStatus RawStatus); public enum VerificationPreparationState { NotStarted, InProgress, Done } -public record IdeVerificationResult(VerificationPreparationState PreparationProgress, ImmutableDictionary Implementations); +public record IdeCanVerifyState(VerificationPreparationState PreparationProgress, + ImmutableDictionary VerificationTasks, + IReadOnlyList Diagnostics); /// /// Contains information from the latest document, and from older documents if some information is missing, @@ -37,7 +39,7 @@ public record IdeState( Node? ResolvedProgram, SymbolTable SymbolTable, LegacySignatureAndCompletionTable SignatureAndCompletionTable, - ImmutableDictionary> VerificationResults, + ImmutableDictionary> CanVerifyStates, IReadOnlyList Counterexamples, IReadOnlyDictionary> GhostRanges, ImmutableDictionary VerificationTrees @@ -62,7 +64,7 @@ public static IdeState InitialIdeState(CompilationInput input) { ImmutableDictionary>.Empty, program, SymbolTable.Empty(), - LegacySignatureAndCompletionTable.Empty(input.Options, input.Project), ImmutableDictionary>.Empty, + LegacySignatureAndCompletionTable.Empty(input.Options, input.Project), ImmutableDictionary>.Empty, Array.Empty(), ImmutableDictionary>.Empty, ImmutableDictionary.Empty @@ -77,35 +79,35 @@ public IdeState Migrate(DafnyOptions options, Migrator migrator, int newVersion, (DocumentVerificationTree)migrator.RelocateVerificationTree(kv.Value)); var verificationResults = clientSide - ? VerificationResults - : MigrateImplementationViews(migrator, VerificationResults); + ? CanVerifyStates + : MigrateImplementationViews(migrator, CanVerifyStates); return this with { Version = newVersion, Status = CompilationStatus.Parsing, - VerificationResults = verificationResults, + CanVerifyStates = verificationResults, SignatureAndCompletionTable = options.Get(LegacySignatureAndCompletionTable.MigrateSignatureAndCompletionTable) ? migrator.MigrateSymbolTable(SignatureAndCompletionTable) : LegacySignatureAndCompletionTable.Empty(options, Input.Project), VerificationTrees = migratedVerificationTrees }; } - private ImmutableDictionary> MigrateImplementationViews( + private ImmutableDictionary> MigrateImplementationViews( Migrator migrator, - ImmutableDictionary> oldVerificationDiagnostics) { + ImmutableDictionary> oldVerificationDiagnostics) { var uri = migrator.MigratedUri; var previous = oldVerificationDiagnostics.GetValueOrDefault(uri); if (previous == null) { return oldVerificationDiagnostics; } - var result = ImmutableDictionary.Empty; + var result = ImmutableDictionary.Empty; foreach (var entry in previous) { var newOuterRange = migrator.MigrateRange(entry.Key); if (newOuterRange == null) { continue; } - var newValue = ImmutableDictionary.Empty; - foreach (var innerEntry in entry.Value.Implementations) { + var newValue = ImmutableDictionary.Empty; + foreach (var innerEntry in entry.Value.VerificationTasks) { var newInnerRange = migrator.MigrateRange(innerEntry.Value.Range); if (newInnerRange != null) { newValue = newValue.Add(innerEntry.Key, innerEntry.Value with { @@ -115,15 +117,15 @@ private ImmutableDictionary GetVerificationResults(Uri uri) { - return VerificationResults.GetValueOrDefault(uri) ?? - ((IReadOnlyDictionary)ImmutableDictionary.Empty); + public IReadOnlyDictionary GetVerificationResults(Uri uri) { + return CanVerifyStates.GetValueOrDefault(uri) ?? + ((IReadOnlyDictionary)ImmutableDictionary.Empty); } public IEnumerable GetAllDiagnostics() { @@ -133,13 +135,14 @@ public IEnumerable GetAllDiagnostics() { public IEnumerable GetDiagnosticsForUri(Uri uri) { var resolutionDiagnostics = StaticDiagnostics.GetValueOrDefault(uri) ?? Enumerable.Empty(); var verificationDiagnostics = GetVerificationResults(uri).SelectMany(x => { - return x.Value.Implementations.Values.SelectMany(v => v.Diagnostics).Concat(GetErrorLimitDiagnostics(x)); + var taskDiagnostics = x.Value.VerificationTasks.Values.SelectMany(v => v.Diagnostics); + return x.Value.Diagnostics.Concat(taskDiagnostics.Concat(GetErrorLimitDiagnostics(x))); }); return resolutionDiagnostics.Concat(verificationDiagnostics); } - private static IEnumerable GetErrorLimitDiagnostics(KeyValuePair x) { - var anyImplementationHitErrorLimit = x.Value.Implementations.Values.Any(i => i.HitErrorLimit); + private static IEnumerable GetErrorLimitDiagnostics(KeyValuePair x) { + var anyImplementationHitErrorLimit = x.Value.VerificationTasks.Values.Any(i => i.HitErrorLimit); IEnumerable result; if (anyImplementationHitErrorLimit) { var diagnostic = new Diagnostic() { @@ -159,7 +162,7 @@ private static IEnumerable GetErrorLimitDiagnostics(KeyValuePair GetDiagnosticUris() { - return StaticDiagnostics.Keys.Concat(VerificationResults.Keys); + return StaticDiagnostics.Keys.Concat(CanVerifyStates.Keys); } public async Task UpdateState(DafnyOptions options, @@ -168,29 +171,29 @@ public async Task UpdateState(DafnyOptions options, IProjectDatabase projectDatabase, ICompilationEvent e) { switch (e) { case DeterminedRootFiles determinedRootFiles: - return await UpdateDeterminedRootFiles(options, logger, projectDatabase, determinedRootFiles); + return await HandleDeterminedRootFiles(options, logger, projectDatabase, determinedRootFiles); case BoogieUpdate boogieUpdate: - return UpdateBoogieUpdate(options, logger, boogieUpdate); + return HandleBoogieUpdate(options, logger, boogieUpdate); case CanVerifyPartsIdentified canVerifyPartsIdentified: - return UpdateCanVerifyPartsUpdated(logger, canVerifyPartsIdentified); + return HandleCanVerifyPartsUpdated(logger, canVerifyPartsIdentified); case FinishedParsing finishedParsing: - return UpdateFinishedParsing(finishedParsing); + return HandleFinishedParsing(finishedParsing); case FinishedResolution finishedResolution: - return UpdateFinishedResolution(options, logger, telemetryPublisher, finishedResolution); + return HandleFinishedResolution(options, logger, telemetryPublisher, finishedResolution); case InternalCompilationException internalCompilationException: - return UpdateInternalCompilationException(internalCompilationException); + return HandleInternalCompilationException(internalCompilationException); case BoogieException boogieException: - return UpdateBoogieException(boogieException); + return HandleBoogieException(boogieException); case NewDiagnostic newDiagnostic: - return UpdateNewDiagnostic(newDiagnostic); + return HandleNewDiagnostic(newDiagnostic); case ScheduledVerification scheduledVerification: - return UpdateScheduledVerification(scheduledVerification); + return HandleScheduledVerification(scheduledVerification); default: throw new ArgumentOutOfRangeException(nameof(e)); } } - private async Task UpdateDeterminedRootFiles(DafnyOptions options, ILogger logger, + private async Task HandleDeterminedRootFiles(DafnyOptions options, ILogger logger, IProjectDatabase projectDatabase, DeterminedRootFiles determinedRootFiles) { var errors = determinedRootFiles.Diagnostics.Values.SelectMany(x => x). @@ -218,27 +221,27 @@ private async Task UpdateDeterminedRootFiles(DafnyOptions options, ILo }; } - private IdeState UpdateScheduledVerification(ScheduledVerification scheduledVerification) { + private IdeState HandleScheduledVerification(ScheduledVerification scheduledVerification) { var previousState = this; var uri = scheduledVerification.CanVerify.Tok.Uri; var range = scheduledVerification.CanVerify.NameToken.GetLspRange(); - var previousVerificationResult = previousState.VerificationResults[uri][range]; - var previousImplementations = previousVerificationResult.Implementations; + var previousVerificationResult = previousState.CanVerifyStates[uri][range]; + var previousImplementations = previousVerificationResult.VerificationTasks; var preparationProgress = new[] { previousVerificationResult.PreparationProgress, VerificationPreparationState.InProgress }.Max(); - var verificationResult = new IdeVerificationResult(PreparationProgress: preparationProgress, - Implementations: previousImplementations.ToImmutableDictionary(kv => kv.Key, kv => kv.Value with { + var verificationResult = new IdeCanVerifyState(PreparationProgress: preparationProgress, + VerificationTasks: previousImplementations.ToImmutableDictionary(kv => kv.Key, kv => kv.Value with { Status = PublishedVerificationStatus.Stale, - Diagnostics = IdeState.MarkDiagnosticsAsOutdated(kv.Value.Diagnostics).ToList() - })); + Diagnostics = MarkDiagnosticsAsOutdated(kv.Value.Diagnostics).ToList() + }), previousVerificationResult.Diagnostics); return previousState with { - VerificationResults = previousState.VerificationResults.SetItem(uri, - previousState.VerificationResults[uri].SetItem(range, verificationResult)) + CanVerifyStates = previousState.CanVerifyStates.SetItem(uri, + previousState.CanVerifyStates[uri].SetItem(range, verificationResult)) }; } - private IdeState UpdateNewDiagnostic(NewDiagnostic newDiagnostic) { + private IdeState HandleNewDiagnostic(NewDiagnostic newDiagnostic) { var previousState = this; // Until resolution is finished, keep showing the old diagnostics. @@ -253,7 +256,7 @@ private IdeState UpdateNewDiagnostic(NewDiagnostic newDiagnostic) { return previousState; } - private IdeState UpdateInternalCompilationException(InternalCompilationException internalCompilationException) { + private IdeState HandleInternalCompilationException(InternalCompilationException internalCompilationException) { var previousState = this; var internalErrorDiagnostic = new Diagnostic { Message = @@ -270,7 +273,7 @@ private IdeState UpdateInternalCompilationException(InternalCompilationException }; } - private IdeState UpdateFinishedResolution(DafnyOptions options, + private IdeState HandleFinishedResolution(DafnyOptions options, ILogger logger, TelemetryPublisherBase telemetryPublisher, FinishedResolution finishedResolution) { @@ -305,7 +308,7 @@ private IdeState UpdateFinishedResolution(DafnyOptions options, } var verificationResults = finishedResolution.Result.CanVerifies == null - ? previousState.VerificationResults + ? previousState.CanVerifyStates : finishedResolution.Result.CanVerifies.GroupBy(l => l.NameToken.Uri).ToImmutableDictionary(k => k.Key, k => k.GroupBy(l => l.NameToken.GetLspRange()).ToImmutableDictionary( l => l.Key, @@ -317,23 +320,22 @@ private IdeState UpdateFinishedResolution(DafnyOptions options, return previousState with { StaticDiagnostics = finishedResolution.Diagnostics, Status = status, + Counterexamples = Array.Empty(), ResolvedProgram = finishedResolution.Result.ResolvedProgram, SymbolTable = symbolTable ?? previousState.SymbolTable, SignatureAndCompletionTable = signatureAndCompletionTable, GhostRanges = ghostRanges, - VerificationResults = verificationResults, + CanVerifyStates = verificationResults, VerificationTrees = trees }; } - private static IdeVerificationResult MergeResults(IEnumerable results) { - return results.Aggregate((a, b) => new IdeVerificationResult( + private static IdeCanVerifyState MergeResults(IEnumerable results) { + return results.Aggregate((a, b) => new IdeCanVerifyState( MergeStates(a.PreparationProgress, b.PreparationProgress), - a.Implementations.ToImmutableDictionary().Merge(b.Implementations, - (aView, bView) => new IdeImplementationView( - aView.Range, - Combine(aView.Status, bView.Status), - aView.Diagnostics.Concat(bView.Diagnostics).ToList(), aView.HitErrorLimit || bView.HitErrorLimit)))); + a.VerificationTasks.ToImmutableDictionary().Merge(b.VerificationTasks, + (aView, bView) => aView /* Merge should not occur */), + a.Diagnostics.Concat(b.Diagnostics))); } private static VerificationPreparationState MergeStates(VerificationPreparationState a, VerificationPreparationState b) { @@ -344,19 +346,20 @@ private static PublishedVerificationStatus Combine(PublishedVerificationStatus f return new[] { first, second }.Min(); } - private static IdeVerificationResult MergeVerifiable(IdeState previousState, ICanVerify canVerify) { + private static IdeCanVerifyState MergeVerifiable(IdeState previousState, ICanVerify canVerify) { var range = canVerify.NameToken.GetLspRange(); + var previousIdeCanVerifyState = previousState.GetVerificationResults(canVerify.NameToken.Uri).GetValueOrDefault(range); var previousImplementations = - previousState.GetVerificationResults(canVerify.NameToken.Uri).GetValueOrDefault(range)?.Implementations ?? - ImmutableDictionary.Empty; - return new IdeVerificationResult(PreparationProgress: VerificationPreparationState.NotStarted, - Implementations: previousImplementations.ToImmutableDictionary(kv => kv.Key, kv => kv.Value with { + previousIdeCanVerifyState?.VerificationTasks ?? + ImmutableDictionary.Empty; + return new IdeCanVerifyState(PreparationProgress: VerificationPreparationState.NotStarted, + VerificationTasks: previousImplementations.ToImmutableDictionary(kv => kv.Key, kv => kv.Value with { Status = PublishedVerificationStatus.Stale, - Diagnostics = IdeState.MarkDiagnosticsAsOutdated(kv.Value.Diagnostics).ToList() - })); + Diagnostics = MarkDiagnosticsAsOutdated(kv.Value.Diagnostics).ToList() + }), previousIdeCanVerifyState?.Diagnostics ?? new List()); } - private IdeState UpdateFinishedParsing(FinishedParsing finishedParsing) { + private IdeState HandleFinishedParsing(FinishedParsing finishedParsing) { var previousState = this; var trees = previousState.VerificationTrees; foreach (var uri in trees.Keys) { @@ -380,9 +383,9 @@ private IdeState UpdateFinishedParsing(FinishedParsing finishedParsing) { }; } - private IdeState UpdateCanVerifyPartsUpdated(ILogger logger, CanVerifyPartsIdentified canVerifyPartsIdentified) { + private IdeState HandleCanVerifyPartsUpdated(ILogger logger, CanVerifyPartsIdentified canVerifyPartsIdentified) { var previousState = this; - var implementations = canVerifyPartsIdentified.Parts.Select(t => t.Implementation); + var implementations = canVerifyPartsIdentified.Parts.Select(t => t.Split.Implementation).Distinct(); var gutterIconManager = new GutterIconAndHoverVerificationDetailsManager(logger); var uri = canVerifyPartsIdentified.CanVerify.Tok.Uri; @@ -390,34 +393,34 @@ private IdeState UpdateCanVerifyPartsUpdated(ILogger logger, CanVerifyPartsIdent canVerifyPartsIdentified.CanVerify, implementations.ToArray()); var range = canVerifyPartsIdentified.CanVerify.NameToken.GetLspRange(); - var previousImplementations = previousState.VerificationResults[uri][range].Implementations; - var names = canVerifyPartsIdentified.Parts.Select(t => Compilation.GetImplementationName(t.Implementation)); - var verificationResult = new IdeVerificationResult(PreparationProgress: VerificationPreparationState.Done, - Implementations: names.ToImmutableDictionary(k => k, + var previousImplementations = previousState.CanVerifyStates[uri][range].VerificationTasks; + var names = canVerifyPartsIdentified.Parts.Select(Compilation.GetTaskName); + var verificationResult = new IdeCanVerifyState(PreparationProgress: VerificationPreparationState.Done, + VerificationTasks: canVerifyPartsIdentified.Parts.ToImmutableDictionary(Compilation.GetTaskName, k => { - var previous = previousImplementations.GetValueOrDefault(k); - return new IdeImplementationView(range, PublishedVerificationStatus.Queued, + var previous = previousImplementations.GetValueOrDefault(Compilation.GetTaskName(k)); + return new IdeVerificationTaskState(range, PublishedVerificationStatus.Queued, previous?.Diagnostics ?? Array.Empty(), - previous?.HitErrorLimit ?? false); - })); + previous?.HitErrorLimit ?? false, k, new Stale()); + }), new List()); return previousState with { - VerificationResults = previousState.VerificationResults.SetItem(uri, - previousState.VerificationResults[uri].SetItem(range, verificationResult)) + CanVerifyStates = previousState.CanVerifyStates.SetItem(uri, + previousState.CanVerifyStates[uri].SetItem(range, verificationResult)) }; } - private IdeState UpdateBoogieException(BoogieException boogieException) { + private IdeState HandleBoogieException(BoogieException boogieException) { var previousState = this; - var name = Compilation.GetImplementationName(boogieException.Task.Implementation); + var name = Compilation.GetTaskName(boogieException.Task); var uri = boogieException.CanVerify.Tok.Uri; var range = boogieException.CanVerify.NameToken.GetLspRange(); - var previousVerificationResult = previousState.VerificationResults[uri][range]; - var previousImplementations = previousVerificationResult.Implementations; - var previousView = previousImplementations.GetValueOrDefault(name) ?? - new IdeImplementationView(range, PublishedVerificationStatus.Error, Array.Empty(), false); - var diagnostics = previousView.Diagnostics; + var previousVerificationResult = previousState.CanVerifyStates[uri][range]; + var previousImplementations = previousVerificationResult.VerificationTasks; + var previousView = previousImplementations.GetValueOrDefault(name); + var diagnostics = previousView?.Diagnostics ?? Array.Empty(); + var hitErrorLimit = previousView?.HitErrorLimit ?? false; var internalErrorDiagnostic = new Diagnostic { Message = boogieException.Exception.Message, @@ -426,104 +429,106 @@ private IdeState UpdateBoogieException(BoogieException boogieException) { }; diagnostics = diagnostics.Concat(new[] { internalErrorDiagnostic }).ToList(); - var view = new IdeImplementationView(range, PublishedVerificationStatus.Error, diagnostics.ToList(), previousView.HitErrorLimit); + var view = new IdeVerificationTaskState(range, PublishedVerificationStatus.Error, diagnostics.ToList(), hitErrorLimit, boogieException.Task, new Stale()); return previousState with { - VerificationResults = previousState.VerificationResults.SetItem(uri, - previousState.VerificationResults[uri].SetItem(range, previousVerificationResult with { - Implementations = previousVerificationResult.Implementations.SetItem(name, view) + CanVerifyStates = previousState.CanVerifyStates.SetItem(uri, + previousState.CanVerifyStates[uri].SetItem(range, previousVerificationResult with { + VerificationTasks = previousVerificationResult.VerificationTasks.SetItem(name, view) })) }; } - private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, BoogieUpdate boogieUpdate) { + private IdeState HandleBoogieUpdate(DafnyOptions options, ILogger logger, BoogieUpdate boogieUpdate) { var previousState = this; - UpdateGutterIconTrees(boogieUpdate, options, logger); - var name = Compilation.GetImplementationName(boogieUpdate.ImplementationTask.Implementation); + var name = Compilation.GetTaskName(boogieUpdate.VerificationTask); var status = StatusFromBoogieStatus(boogieUpdate.BoogieStatus); var uri = boogieUpdate.CanVerify.Tok.Uri; var range = boogieUpdate.CanVerify.NameToken.GetLspRange(); - var previousVerificationResult = previousState.VerificationResults[uri][range]; - var previousImplementations = previousVerificationResult.Implementations; - var previousView = previousImplementations.GetValueOrDefault(name) ?? - new IdeImplementationView(range, status, Array.Empty(), false); + var previousVerificationResult = previousState.CanVerifyStates[uri][range]; + var previousImplementations = previousVerificationResult.VerificationTasks; + var previousView = previousImplementations.GetValueOrDefault(name); var counterExamples = previousState.Counterexamples; - bool hitErrorLimit = previousView.HitErrorLimit; - var diagnostics = previousView.Diagnostics; + bool hitErrorLimit = previousView?.HitErrorLimit ?? false; + IVerificationStatus rawStatus = boogieUpdate.BoogieStatus; + var diagnostics = previousView?.Diagnostics ?? Array.Empty(); if (boogieUpdate.BoogieStatus is Running) { diagnostics = Array.Empty(); - counterExamples = Array.Empty(); hitErrorLimit = false; } - if (boogieUpdate.BoogieStatus is BatchCompleted batchCompleted) { - counterExamples = counterExamples.Concat(batchCompleted.VcResult.counterExamples); - hitErrorLimit |= batchCompleted.VcResult.maxCounterExamples == batchCompleted.VcResult.counterExamples.Count; + if (boogieUpdate.BoogieStatus is Completed completed) { + // WarnContradictoryAssumptions should be computable after completing a single assertion batch. + // And we should do this because it allows this warning to be shown when doing --filter-position on a single assertion + // https://github.com/dafny-lang/dafny/issues/5039 + + counterExamples = counterExamples.Concat(completed.Result.CounterExamples); + hitErrorLimit |= completed.Result.MaxCounterExamples == completed.Result.CounterExamples.Count; var newDiagnostics = - Compilation.GetDiagnosticsFromResult(options, previousState.Uri, boogieUpdate.ImplementationTask, batchCompleted.VcResult).ToArray(); - diagnostics = diagnostics.Concat(newDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); + Compilation.GetDiagnosticsFromResult(options, previousState.Uri, boogieUpdate.VerificationTask, completed.Result); + diagnostics = newDiagnostics.Select(d => d.ToLspDiagnostic()).ToList(); logger.LogTrace( - $"BatchCompleted received for {previousState.Input} and found #{newDiagnostics.Length} new diagnostics."); + $"Completed received for {previousState.Input} and found #{diagnostics.Count} diagnostics and #{completed.Result.CounterExamples.Count} counterexamples."); } - if (boogieUpdate.BoogieStatus is Completed completed) { + var newCanVerifyDiagnostics = new List(); + var taskState = new IdeVerificationTaskState(range, status, diagnostics.ToList(), + hitErrorLimit, boogieUpdate.VerificationTask, rawStatus); + var newTaskStates = previousVerificationResult.VerificationTasks.SetItem(name, taskState); + + var scopeGroup = newTaskStates.Values.Where(s => s.Task.ScopeId == boogieUpdate.VerificationTask.ScopeId).ToList(); + var allTasksAreCompleted = scopeGroup.All(s => s.Status >= PublishedVerificationStatus.Error); + if (allTasksAreCompleted) { + var errorReporter = new ObservableErrorReporter(options, uri); List verificationCoverageDiagnostics = new(); errorReporter.Updates.Subscribe(d => verificationCoverageDiagnostics.Add(d.Diagnostic)); - if (Input.Options.Get(CommonOptionBag.WarnContradictoryAssumptions) - || Input.Options.Get(CommonOptionBag.WarnRedundantAssumptions)) { - ProofDependencyWarnings.WarnAboutSuspiciousDependenciesForImplementation(Input.Options, - errorReporter, - boogieUpdate.ProofDependencyManager, - new DafnyConsolePrinter.ImplementationLogEntry(boogieUpdate.ImplementationTask.Implementation.VerboseName, - boogieUpdate.ImplementationTask.Implementation.tok), - DafnyConsolePrinter.DistillVerificationResult(completed.Result)); - } + ProofDependencyWarnings.ReportSuspiciousDependencies(options, + scopeGroup.Select(s => (s.Task, (Completed)s.RawStatus)), + errorReporter, boogieUpdate.ProofDependencyManager); - diagnostics = diagnostics.Concat(verificationCoverageDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); + newCanVerifyDiagnostics = previousVerificationResult.Diagnostics.Concat(verificationCoverageDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); } - var view = new IdeImplementationView(range, status, diagnostics.ToList(), - previousView.HitErrorLimit || hitErrorLimit); + UpdateGutterIconTrees(logger, boogieUpdate, scopeGroup); + return previousState with { Counterexamples = counterExamples, - VerificationResults = previousState.VerificationResults.SetItem(uri, - previousState.VerificationResults[uri].SetItem(range, previousVerificationResult with { - Implementations = previousVerificationResult.Implementations.SetItem(name, view) + CanVerifyStates = previousState.CanVerifyStates.SetItem(uri, + previousState.CanVerifyStates[uri].SetItem(range, previousVerificationResult with { + VerificationTasks = newTaskStates, + Diagnostics = newCanVerifyDiagnostics })) }; } - private void UpdateGutterIconTrees(BoogieUpdate update, DafnyOptions options, ILogger logger) { + private void UpdateGutterIconTrees(ILogger logger, BoogieUpdate boogieUpdate, IReadOnlyList scopeGroup) { var gutterIconManager = new GutterIconAndHoverVerificationDetailsManager(logger); - if (update.BoogieStatus is Running) { - gutterIconManager.ReportVerifyImplementationRunning(this, update.ImplementationTask.Implementation); + if (boogieUpdate.BoogieStatus is Running && scopeGroup.Count(e => e.Status == PublishedVerificationStatus.Running) == 1) { + gutterIconManager.ReportVerifyImplementationRunning(this, boogieUpdate.VerificationTask.Split.Implementation); } - if (update.BoogieStatus is BatchCompleted batchCompleted) { + if (boogieUpdate.BoogieStatus is Completed completed) { gutterIconManager.ReportAssertionBatchResult(this, - new AssertionBatchResult(update.ImplementationTask.Implementation, batchCompleted.VcResult)); + new AssertionBatchResult(boogieUpdate.VerificationTask.Split.Implementation, completed.Result)); } - if (update.BoogieStatus is Completed completed) { - var tokenString = BoogieGenerator.ToDafnyToken(true, update.ImplementationTask.Implementation.tok).TokenToString(options); - var verificationResult = completed.Result; - // Sometimes, the boogie status is set as Completed - // but the assertion batches were not reported yet. - // because they are on a different thread. - // This loop will ensure that every vc result has been dealt with - // before we report that the verification of the implementation is finished - foreach (var result in completed.Result.VCResults) { + if (scopeGroup.All(e => e.Status >= PublishedVerificationStatus.Error)) { + var results = scopeGroup.Select(e => e.RawStatus).OfType().Select(c => c.Result).ToList(); + + foreach (var result in results) { logger.LogDebug( - $"Possibly duplicate reporting assertion batch {result.vcNum} as completed in {tokenString}, version {this.Version}"); + $"Possibly duplicate reporting assertion batch {result.VcNum}, version {Version}"); gutterIconManager.ReportAssertionBatchResult(this, - new AssertionBatchResult(update.ImplementationTask.Implementation, result)); + new AssertionBatchResult(boogieUpdate.VerificationTask.Split.Implementation, result)); } - gutterIconManager.ReportEndVerifyImplementation(this, update.ImplementationTask.Implementation, verificationResult); + var resourceCount = results.Sum(e => e.ResourceCount); + var outcome = results.Select(e => Compilation.GetOutcome(e.Outcome)).Max(); + gutterIconManager.ReportEndVerifyImplementation(this, boogieUpdate.VerificationTask.Split.Implementation, resourceCount, outcome); } } @@ -534,10 +539,9 @@ private static PublishedVerificationStatus StatusFromBoogieStatus(IVerificationS case Queued: return PublishedVerificationStatus.Queued; case Running: - case BatchCompleted: return PublishedVerificationStatus.Running; case Completed completed: - return completed.Result.Outcome == ConditionGeneration.Outcome.Correct + return completed.Result.Outcome == SolverOutcome.Valid ? PublishedVerificationStatus.Correct : PublishedVerificationStatus.Error; default: diff --git a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs index 86e19303d9..544f909af3 100644 --- a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs +++ b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs @@ -96,13 +96,15 @@ private FileVerificationStatus GetFileVerificationStatus(IdeState state, Uri uri OrderBy(s => s.NameRange.Start).ToList()); } - private static NamedVerifiableStatus GetNamedVerifiableStatuses(Range canVerify, IdeVerificationResult result) { + private static NamedVerifiableStatus GetNamedVerifiableStatuses(Range canVerify, IdeCanVerifyState result) { const PublishedVerificationStatus nothingToVerifyStatus = PublishedVerificationStatus.Correct; var status = result.PreparationProgress switch { VerificationPreparationState.NotStarted => PublishedVerificationStatus.Stale, VerificationPreparationState.InProgress => PublishedVerificationStatus.Queued, VerificationPreparationState.Done => - result.Implementations.Values.Select(v => v.Status).Aggregate(nothingToVerifyStatus, Combine), + result.VerificationTasks.Values.Any() + ? result.VerificationTasks.Values.Select(v => v.Status).Aggregate(Combine) + : nothingToVerifyStatus, _ => throw new ArgumentOutOfRangeException() }; @@ -112,7 +114,17 @@ private static NamedVerifiableStatus GetNamedVerifiableStatuses(Range canVerify, public static PublishedVerificationStatus Combine(PublishedVerificationStatus first, PublishedVerificationStatus second) { var max = new[] { first, second }.Max(); var min = new[] { first, second }.Min(); - return max >= PublishedVerificationStatus.Error ? min : max; + + if (max >= PublishedVerificationStatus.Error) { + if (min == PublishedVerificationStatus.Queued) { + // If one task is completed, we do not allowed queued as a status. + return PublishedVerificationStatus.Running; + } + + return min; + } else { + return max; + } } private readonly ConcurrentDictionary> publishedDiagnostics = new(); diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs index fbd295f16e..f96d5b2cfb 100644 --- a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs +++ b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs @@ -297,9 +297,10 @@ int TopToBottomPriority(ISymbol symbol) { return symbol.Tok.pos; } var implementationOrder = changedVerifiables.Select((v, i) => (v, i)).ToDictionary(k => k.v, k => k.i); - var orderedVerifiables = canVerifies.OrderByDescending(GetPriorityAttribute).CreateOrderedEnumerable( - t => implementationOrder.GetOrDefault(t.Tok.GetFilePosition(), () => int.MaxValue), - null, false).CreateOrderedEnumerable(TopToBottomPriority, null, false).ToList(); + var orderedVerifiables = canVerifies + .OrderByDescending(GetPriorityAttribute) + .ThenBy(t => implementationOrder.GetOrDefault(t.Tok.GetFilePosition(), () => int.MaxValue)) + .ThenBy(TopToBottomPriority).ToList(); logger.LogDebug($"Ordered verifiables: {string.Join(", ", orderedVerifiables.Select(v => v.NameToken.val))}"); var orderedVerifiableLocations = orderedVerifiables.Select(v => v.NameToken.GetFilePosition()).ToList(); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect index 94a42af27f..ef71487de5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 21 verified, 0 errors +Dafny program verifier finished with 74 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect index 49c99f8b11..4fd36a1d40 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 165 verified, 0 errors +Dafny program verifier finished with 597 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect index bd57f1956c..f3e2b391bd 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 166 verified, 0 errors +Dafny program verifier finished with 491 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect index 5762072e28..c2bb304608 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 202 verified, 0 errors +Dafny program verifier finished with 444 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect index 04f996a507..0230b31865 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect @@ -23,4 +23,4 @@ Termination.dfy(806,2): Error: cannot prove termination; try supplying a decreas Termination.dfy(1178,2): Error: cannot prove termination; try supplying a decreases clause for the loop Termination.dfy(1194,2): Error: cannot prove termination; try supplying a decreases clause for the loop -Dafny program verifier finished with 96 verified, 23 errors +Dafny program verifier finished with 112 verified, 23 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect index 189a267e26..7cc2944f0b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect @@ -24,4 +24,4 @@ Termination.dfy(923,2): Error: cannot prove termination; try supplying a decreas Termination.dfy(1178,2): Error: cannot prove termination; try supplying a decreases clause for the loop Termination.dfy(1194,2): Error: cannot prove termination; try supplying a decreases clause for the loop -Dafny program verifier finished with 95 verified, 24 errors +Dafny program verifier finished with 111 verified, 24 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect index 89ed8e1ed3..638376bfd6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect @@ -7,4 +7,4 @@ MoreInduction.dfy(87,10): Related location: this is the postcondition that could MoreInduction.dfy(93,0): Error: a postcondition could not be proved on this return path MoreInduction.dfy(92,21): Related location: this is the postcondition that could not be proved -Dafny program verifier finished with 9 verified, 4 errors +Dafny program verifier finished with 28 verified, 4 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy.expect index e43bbd93c5..023b099001 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 22 verified, 0 errors +Dafny program verifier finished with 33 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect index 79eca64e20..35e54b59f6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect @@ -1,3 +1,3 @@ SoftwareFoundations-Basics.dfy(41,11): Error: assertion might not hold -Dafny program verifier finished with 42 verified, 1 error +Dafny program verifier finished with 53 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1252.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1252.dfy.expect index cfe97d5394..7d00bd734a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1252.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1252.dfy.expect @@ -8,9 +8,9 @@ git-issue-1252.dfy(70,15): Error: target object might be null git-issue-1252.dfy(81,15): Error: target object might be null git-issue-1252.dfy(87,13): Error: target object might be null git-issue-1252.dfy(93,13): Error: target object might be null -git-issue-1252.dfy(94,10): Error: target object might be null git-issue-1252.dfy(93,13): Error: target object might be null git-issue-1252.dfy(94,10): Error: target object might be null +git-issue-1252.dfy(94,10): Error: target object might be null git-issue-1252.dfy(100,25): Error: target object might be null git-issue-1252.dfy(106,21): Error: object might be null git-issue-1252.dfy(106,21): Error: object might not be allocated in the old-state of the 'unchanged' predicate diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect index 3de59550cb..5ff8e24f08 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect @@ -7,4 +7,4 @@ git-issue-3855.dfy(433,36): Related location: this is the precondition that coul git-issue-3855.dfy(1336,20): Error: a precondition for this call could not be proved git-issue-3855.dfy(433,36): Related location: this is the precondition that could not be proved -Dafny program verifier finished with 69 verified, 3 errors, 1 time out +Dafny program verifier finished with 101 verified, 3 errors, 1 time out diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy.expect index 9b96db8633..caca172229 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 17 verified, 0 errors +Dafny program verifier finished with 47 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/dfyconfig.toml b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/dfyconfig.toml index e69de29bb2..bed17481d4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/dfyconfig.toml +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/dfyconfig.toml @@ -0,0 +1 @@ +includes = ["src/**/*.dfy"] \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/single-file.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/single-file.dfy new file mode 100644 index 0000000000..24eb8c2507 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/single-file.dfy @@ -0,0 +1,25 @@ +method Succeeds() + ensures true { +} + +method Fails() + ensures false { + assert false by { + assert false; + assert false; + } +} + +method Loop() { + var b := true; + while(b) + invariant false + { + b := false; + } + assert false; +} + +method DoubleAssertOneLine(x: int) { + assert x > 2; assert x > 3; +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy index 70e2e1b828..0db23fb833 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy @@ -1,15 +1,15 @@ -// RUN: %verify --filter-position='blaergaerga' %s > %t -// RUN: %verify --filter-position='C:\windows\path.dfy' %s >> %t -// RUN: ! %verify --filter-position='filter.dfy' %s >> %t -// RUN: ! %verify --filter-position='filter.dfy:14' %s >> %t +// RUN: %verify --filter-position='C:\windows\path.dfy' %s > %t // RUN: ! %verify --filter-position='src/source1.dfy:5' %S/Inputs/dfyconfig.toml >> %t -// RUN: %verify --filter-position='src/source1.dfy:2' %S/Inputs/dfyconfig.toml >> %t -// RUN: %diff "%s.expect" "%t" - -method Succeeds() - ensures true { -} - -method Fails() - ensures false { -} +// RUN: %verify --filter-position='src/source1.dfy:1' %S/Inputs/dfyconfig.toml >> %t +// RUN: ! %verify --filter-position='e.dfy' %S/Inputs/single-file.dfy >> %t +// RUN: %verify --filter-position='e.dfy:2' %S/Inputs/single-file.dfy >> %t +// RUN: %verify --filter-position='blaergaerga' %S/Inputs/single-file.dfy >> %t +// RUN: ! %verify --isolate-assertions --filter-position='e.dfy:5' %S/Inputs/single-file.dfy >> %t +// RUN: %verify --isolate-assertions --filter-position='e.dfy:6' %S/Inputs/single-file.dfy >> %t +// RUN: %verify --isolate-assertions --filter-position='e.dfy:7' %S/Inputs/single-file.dfy >> %t +// RUN: ! %verify --isolate-assertions --filter-position='e.dfy:8' %S/Inputs/single-file.dfy >> %t +// RUN: %verify --isolate-assertions --filter-position='e.dfy:9' %S/Inputs/single-file.dfy >> %t +// RUN: ! %verify --isolate-assertions --filter-position='e.dfy:16' %S/Inputs/single-file.dfy >> %t +// RUN: %verify --isolate-assertions --filter-position='y:20' %S/Inputs/single-file.dfy >> %t +// RUN: ! %verify --isolate-assertions --filter-position=':24' %S/Inputs/single-file.dfy >> %t +// RUN: %diff "%s.expect" "%t" \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect index e7fc9735c1..af96cf314c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect @@ -1,18 +1,40 @@ +filter.dfy(1,0): Warning: File contains no code Dafny program verifier finished with 0 verified, 0 errors +source1.dfy(6,16): Error: a postcondition could not be proved on this return path +source1.dfy(6,10): Related location: this is the postcondition that could not be proved + +Dafny program verifier finished with 0 assertions verified, 1 error + +Dafny program verifier finished with 1 assertions verified, 0 errors +single-file.dfy(8,11): Error: assertion might not hold +single-file.dfy(16,14): Error: loop invariant violation +single-file.dfy(24,11): Error: assertion might not hold +single-file.dfy(24,25): Error: assertion might not hold + +Dafny program verifier finished with 1 verified, 4 errors + +Dafny program verifier finished with 0 assertions verified, 0 errors Dafny program verifier finished with 0 verified, 0 errors -filter.dfy(14,16): Error: a postcondition could not be proved on this return path -filter.dfy(14,10): Related location: this is the postcondition that could not be proved +single-file.dfy(8,11): Error: assertion might not hold -Dafny program verifier finished with 1 verified, 1 error -filter.dfy(14,16): Error: a postcondition could not be proved on this return path -filter.dfy(14,10): Related location: this is the postcondition that could not be proved +Dafny program verifier finished with 3 assertions verified, 1 error -Dafny program verifier finished with 0 verified, 1 error -source1.dfy(6,16): Error: a postcondition could not be proved on this return path -source1.dfy(6,10): Related location: this is the postcondition that could not be proved +Dafny program verifier finished with 1 assertions verified, 0 errors + +Dafny program verifier finished with 1 assertions verified, 0 errors +single-file.dfy(8,11): Error: assertion might not hold + +Dafny program verifier finished with 0 assertions verified, 1 error + +Dafny program verifier finished with 1 assertions verified, 0 errors +single-file.dfy(16,14): Error: loop invariant violation + +Dafny program verifier finished with 0 assertions verified, 1 error -Dafny program verifier finished with 0 verified, 1 error +Dafny program verifier finished with 1 assertions verified, 0 errors +single-file.dfy(24,11): Error: assertion might not hold +single-file.dfy(24,25): Error: assertion might not hold -Dafny program verifier finished with 1 verified, 0 errors +Dafny program verifier finished with 0 assertions verified, 2 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect index 66ffe3665d..5436a7e7dc 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 14 verified, 0 errors +Dafny program verifier finished with 164 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect index ccc01c35f4..42324885fd 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 11 verified, 0 errors +Dafny program verifier finished with 56 verified, 0 errors diff --git a/Source/XUnitExtensions/Lit/LitTestCase.cs b/Source/XUnitExtensions/Lit/LitTestCase.cs index 18dcafde3a..4fb0983180 100644 --- a/Source/XUnitExtensions/Lit/LitTestCase.cs +++ b/Source/XUnitExtensions/Lit/LitTestCase.cs @@ -3,11 +3,13 @@ using System.Collections.Generic; using System.IO; using System.Linq; +using System.Threading.Tasks; using Xunit; using Xunit.Abstractions; namespace XUnitExtensions.Lit { public class LitTestCase { + private static readonly TimeSpan IndividualTestTimeout = TimeSpan.FromMinutes(15); public string FilePath { get; } public IEnumerable Commands { get; } public bool ExpectFailure { get; } @@ -54,7 +56,9 @@ public static LitTestCase Read(string filePath, LitTestConfiguration config) { } public static void Run(string filePath, LitTestConfiguration config, ITestOutputHelper outputHelper) { - Read(filePath, config).Execute(outputHelper); + var litTestCase = Read(filePath, config); + var task = Task.Run(() => litTestCase.Execute(outputHelper)); + task.Wait(IndividualTestTimeout); } public LitTestCase(string filePath, IEnumerable commands, bool expectFailure) { @@ -83,8 +87,8 @@ public void Execute(ITestOutputHelper outputHelper) { if (ExpectFailure) { if (exitCode != 0) { - throw new SkipException( - $"Command returned non-zero exit code ({exitCode}): {command}\nOutput:\n{output + outputWriter}\nError:\n{error + errorWriter}"); + results.Add((output + outputWriter, error + errorWriter)); + return; } } diff --git a/customBoogie.patch b/customBoogie.patch index 822a4e0f4f..0760ea90e9 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + + +