From 4b98f81f471a3feb90bba3bf01601d18f09951ce Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 31 Jan 2024 12:06:03 +0100 Subject: [PATCH 01/40] Fix build errors for new Boogie version --- .gitmodules | 3 + Source/DafnyCore/DafnyConsolePrinter.cs | 22 ++--- Source/DafnyCore/Options/CommonOptionBag.cs | 1 - Source/DafnyCore/Pipeline/Compilation.cs | 96 +++++++++--------- .../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 | 2 +- Source/DafnyDriver/CliCanVerifyResults.cs | 4 +- Source/DafnyDriver/CliCompilation.cs | 25 +++-- Source/DafnyDriver/JsonVerificationLogger.cs | 6 +- .../DafnyDriver/SynchronousCliCompilation.cs | 2 +- Source/DafnyDriver/TextVerificationLogger.cs | 2 +- .../DafnyDriver/VerificationResultLogger.cs | 2 +- .../Various/ExceptionTests.cs | 2 +- .../Various/SlowVerifier.cs | 12 +-- .../AssertionBatchCompletedObserver.cs | 2 +- .../Language/DafnyProgramVerifier.cs | 4 +- ...rIconAndHoverVerificationDetailsManager.cs | 44 ++++----- .../DafnyLanguageServer/Workspace/IdeState.cs | 99 ++++++++++--------- .../LitTests/LitTest/verification/filter.dfy | 2 + boogie | 1 + 23 files changed, 178 insertions(+), 165 deletions(-) create mode 160000 boogie diff --git a/.gitmodules b/.gitmodules index aa94f844181..ff4c52587f4 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,6 @@ [submodule "Test/libraries"] path = Source/IntegrationTests/TestFiles/LitTests/LitTest/libraries url = https://github.com/dafny-lang/libraries.git +[submodule "boogie"] + path = boogie + url = git@github.com:boogie-org/boogie.git diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index c09d81c6661..a2bce350cc3 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/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index d916645fb30..64ad9f9ad7d 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 81f0a5b1df8..fbacf6f4030 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,6 +237,19 @@ private async Task ResolveAsync() { } } + public static string GetSplitName(ManualSplit split) { + return split.Implementation.Name; // TODO fix. + // var prefix = implementation.Name.Split(BoogieGenerator.NameSeparator)[0]; + // + // // 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) { + // prefix += "." + refinementToken.InheritingModule.Name; + // } + + //return prefix; + } + public static string GetImplementationName(Implementation implementation) { var prefix = implementation.Name.Split(BoogieGenerator.NameSeparator)[0]; @@ -302,13 +315,14 @@ public async Task VerifyCanVerify(ICanVerify canVerify, bool onlyPrepareVe } private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterTests, ICanVerify canVerify, - ResolutionResult resolution) { + ResolutionResult resolution) + { 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 +331,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,19 +342,19 @@ 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. @@ -358,16 +372,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 +407,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 +416,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 +469,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 +479,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 +492,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) { + private 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 419d9791286..d84cc8f5423 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 0514b3aa95e..03bc69f149f 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 296e20806e5..fca31082e28 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 bac2880a61f..d52cc8e8f3d 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(ManualSplit Split, 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 5f53c98e987..2a4d6c1e467 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -19,7 +19,7 @@ public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, Er public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, DafnyConsolePrinter.ImplementationLogEntry logEntry, DafnyConsolePrinter.VerificationResultLogEntry result) { - if (result.Outcome != ConditionGeneration.Outcome.Correct) { + if (result.Outcome != VcOutcome.Correct) { return; } diff --git a/Source/DafnyDriver/CliCanVerifyResults.cs b/Source/DafnyDriver/CliCanVerifyResults.cs index e5757e17ca3..069e18781b1 100644 --- a/Source/DafnyDriver/CliCanVerifyResults.cs +++ b/Source/DafnyDriver/CliCanVerifyResults.cs @@ -7,8 +7,8 @@ namespace DafnyDriver.Commands; struct CliCanVerifyResults { public readonly TaskCompletionSource Finished = new(); - public readonly ConcurrentBag<(IImplementationTask, Completed)> CompletedParts = new(); - public readonly ConcurrentBag Tasks = new(); + public readonly ConcurrentBag<(IVerificationTask Task, Completed Result)> CompletedParts = new(); + public readonly ConcurrentBag Tasks = new(); public CliCanVerifyResults() { } diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index b19e6c5b75c..98e9624659e 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -151,26 +151,27 @@ 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)); + // TODO first update this to record resolution of ICanVerify things. switch (completed.Result.Outcome) { - case ConditionGeneration.Outcome.Correct: - case ConditionGeneration.Outcome.ReachedBound: + case SolverOutcome.Valid: + case SolverOutcome.Bounded: Interlocked.Increment(ref statSum.VerifiedCount); break; - case ConditionGeneration.Outcome.Errors: - Interlocked.Add(ref statSum.ErrorCount, completed.Result.Errors.Count); + case SolverOutcome.Invalid: + Interlocked.Add(ref statSum.ErrorCount, completed.Result.CounterExamples.Count); break; - case ConditionGeneration.Outcome.TimedOut: + case SolverOutcome.TimeOut: Interlocked.Increment(ref statSum.TimeoutCount); break; - case ConditionGeneration.Outcome.OutOfMemory: + case SolverOutcome.OutOfMemory: Interlocked.Increment(ref statSum.OutOfMemoryCount); break; - case ConditionGeneration.Outcome.OutOfResource: + case SolverOutcome.OutOfResource: Interlocked.Increment(ref statSum.OutOfResourceCount); break; - case ConditionGeneration.Outcome.Inconclusive: + case SolverOutcome.Undetermined: Interlocked.Increment(ref statSum.InconclusiveCount); break; default: @@ -205,10 +206,8 @@ public async Task VerifyAllAndPrintSummary() { var results = canVerifyResults[canVerify]; try { 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); - } + foreach (var (task, completed) in results.CompletedParts.OrderBy(t => t.Task.Split.Token)) { + Compilation.ReportDiagnosticsInResult(options, task, completed.Result, Compilation.Reporter); ProofDependencyWarnings.WarnAboutSuspiciousDependenciesForImplementation(options, resolution.ResolvedProgram!.Reporter, diff --git a/Source/DafnyDriver/JsonVerificationLogger.cs b/Source/DafnyDriver/JsonVerificationLogger.cs index b9557a70656..58d56ad9608 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 e402fc765fe..70f12a922a5 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 6839b6008f4..7cb0c0fba35 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 ec7e4b0a103..433a598519b 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/Various/ExceptionTests.cs b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs index 511109f223f..d2660587b5e 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 c75033ea95e..8f46a6cc7fd 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,18 @@ 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 IObservable TryRun() { return source; diff --git a/Source/DafnyLanguageServer/Language/AssertionBatchCompletedObserver.cs b/Source/DafnyLanguageServer/Language/AssertionBatchCompletedObserver.cs index 7c0a54bbe1c..9b59bf09a73 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 ba413a3d657..71359c62e60 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 be118a92c25..8c3e1e9fbc6 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,7 @@ 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, ImplementationRunResult verificationResult) { var uri = ((IToken)implementation.tok).Uri; var tree = state.VerificationTrees[uri]; @@ -264,16 +260,16 @@ public void ReportEndVerifyImplementation(IdeState state, Implementation impleme implementationNode.Stop(); implementationNode.ResourceCount = verificationResult.ResourceCount; targetMethodNode.ResourceCount += verificationResult.ResourceCount; - var finalOutcome = verificationResult.Outcome switch { - ConditionGeneration.Outcome.Correct => GutterVerificationStatus.Verified, + var finalOutcome = verificationResult.VcOutcome 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 = verificationResult.VcOutcome switch { + VcOutcome.Correct => targetMethodNode.StatusVerification, _ => GutterVerificationStatus.Error }; } else { @@ -302,11 +298,11 @@ private void NoMethodNodeAtLogging(VerificationTree tree, string methodName, Ide /// Called when a split is finished to be verified /// public void ReportAssertionBatchResult(IdeState ideState, AssertionBatchResult batchResult) { - var uri = ((IToken)batchResult.Implementation.tok).Uri; + var uri = ((IToken)batchResult.Split.Token).Uri; var tree = ideState.VerificationTrees[uri]; lock (LockProcessing) { - var implementation = batchResult.Implementation; + var implementation = batchResult.Split.Implementation; var result = batchResult.Result; // While there is no error, just add successful nodes. var targetMethodNode = GetTargetMethodTree(tree, implementation, out var implementationNode); @@ -324,9 +320,9 @@ assertNode is AssertionVerificationTree assertionNode 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, @@ -435,15 +431,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 f75e6bfa665..0a3dd267f35 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -382,7 +382,7 @@ private IdeState UpdateFinishedParsing(FinishedParsing finishedParsing) { private IdeState UpdateCanVerifyPartsUpdated(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; @@ -391,7 +391,7 @@ private IdeState UpdateCanVerifyPartsUpdated(ILogger logger, CanVerifyPartsIdent var range = canVerifyPartsIdentified.CanVerify.NameToken.GetLspRange(); var previousImplementations = previousState.VerificationResults[uri][range].Implementations; - var names = canVerifyPartsIdentified.Parts.Select(t => Compilation.GetImplementationName(t.Implementation)); + var names = canVerifyPartsIdentified.Parts.Select(t => Compilation.GetSplitName(t.Split)); var verificationResult = new IdeVerificationResult(PreparationProgress: VerificationPreparationState.Done, Implementations: names.ToImmutableDictionary(k => k, k => { @@ -409,7 +409,7 @@ private IdeState UpdateCanVerifyPartsUpdated(ILogger logger, CanVerifyPartsIdent private IdeState UpdateBoogieException(BoogieException boogieException) { var previousState = this; - var name = Compilation.GetImplementationName(boogieException.Task.Implementation); + var name = Compilation.GetSplitName(boogieException.Task.Split); var uri = boogieException.CanVerify.Tok.Uri; var range = boogieException.CanVerify.NameToken.GetLspRange(); @@ -440,7 +440,7 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie var previousState = this; UpdateGutterIconTrees(boogieUpdate, options, logger); - var name = Compilation.GetImplementationName(boogieUpdate.ImplementationTask.Implementation); + var name = Compilation.GetSplitName(boogieUpdate.VerificationTask.Split); var status = StatusFromBoogieStatus(boogieUpdate.BoogieStatus); var uri = boogieUpdate.CanVerify.Tok.Uri; var range = boogieUpdate.CanVerify.NameToken.GetLspRange(); @@ -458,33 +458,37 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie 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 batchCompleted) { + counterExamples = counterExamples.Concat(batchCompleted.Result.CounterExamples); + hitErrorLimit |= batchCompleted.Result.MaxCounterExamples == batchCompleted.Result.CounterExamples.Count; var newDiagnostics = - Compilation.GetDiagnosticsFromResult(options, previousState.Uri, boogieUpdate.ImplementationTask, batchCompleted.VcResult).ToArray(); + Compilation.GetDiagnosticsFromResult(options, previousState.Uri, boogieUpdate.VerificationTask, batchCompleted.Result).ToArray(); diagnostics = diagnostics.Concat(newDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); logger.LogTrace( $"BatchCompleted received for {previousState.Input} and found #{newDiagnostics.Length} new diagnostics."); } - if (boogieUpdate.BoogieStatus is Completed completed) { - 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)); - } - - diagnostics = diagnostics.Concat(verificationCoverageDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); - } + // TODO Come up with a solution + // WarnContradictoryAssumptions should be executable based on a single assertion batch. + // WarnRedundantAssumptions is more like find references. It needs all the batches under in a verification scope. + // If we're saying that WarnRedundantAssumptions is critical, than verifying single assertions is crap. + // if (boogieUpdate.BoogieStatus is Completed completed) { + // 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.VerificationTask.Implementation.VerboseName, + // boogieUpdate.VerificationTask.Implementation.tok), + // DafnyConsolePrinter.DistillVerificationResult(completed.Result)); + // } + // + // diagnostics = diagnostics.Concat(verificationCoverageDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); + // } var view = new IdeImplementationView(range, status, diagnostics.ToList(), previousView.HitErrorLimit || hitErrorLimit); @@ -500,31 +504,33 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie private void UpdateGutterIconTrees(BoogieUpdate update, DafnyOptions options, ILogger logger) { var gutterIconManager = new GutterIconAndHoverVerificationDetailsManager(logger); if (update.BoogieStatus is Running) { - gutterIconManager.ReportVerifyImplementationRunning(this, update.ImplementationTask.Implementation); + // TODO remove duplication? + gutterIconManager.ReportVerifyImplementationRunning(this, update.VerificationTask.Split.Implementation); } - if (update.BoogieStatus is BatchCompleted batchCompleted) { + if (update.BoogieStatus is Completed batchCompleted) { gutterIconManager.ReportAssertionBatchResult(this, - new AssertionBatchResult(update.ImplementationTask.Implementation, batchCompleted.VcResult)); + new AssertionBatchResult(update.VerificationTask.Split, batchCompleted.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) { - logger.LogDebug( - $"Possibly duplicate reporting assertion batch {result.vcNum} as completed in {tokenString}, version {this.Version}"); - gutterIconManager.ReportAssertionBatchResult(this, - new AssertionBatchResult(update.ImplementationTask.Implementation, result)); - } - - gutterIconManager.ReportEndVerifyImplementation(this, update.ImplementationTask.Implementation, verificationResult); - } + // TODO switch to + // if (update.BoogieStatus is Completed completed) { + // var tokenString = BoogieGenerator.ToDafnyToken(true, update.VerificationTask.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) { + // logger.LogDebug( + // $"Possibly duplicate reporting assertion batch {result.vcNum} as completed in {tokenString}, version {this.Version}"); + // gutterIconManager.ReportAssertionBatchResult(this, + // new AssertionBatchResult(update.VerificationTask.Implementation, result)); + // } + // + // gutterIconManager.ReportEndVerifyImplementation(this, update.VerificationTask.Implementation, verificationResult); + // } } private static PublishedVerificationStatus StatusFromBoogieStatus(IVerificationStatus verificationStatus) { @@ -534,10 +540,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/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy index 70e2e1b8286..015d2554cbc 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy @@ -4,6 +4,7 @@ // RUN: ! %verify --filter-position='filter.dfy:14' %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: ! %verify --isolate-assertions --filter-position='filter.dfy:15' %s >> %t // RUN: %diff "%s.expect" "%t" method Succeeds() @@ -12,4 +13,5 @@ method Succeeds() method Fails() ensures false { + assert false; } diff --git a/boogie b/boogie new file mode 160000 index 00000000000..0efcb0bd03c --- /dev/null +++ b/boogie @@ -0,0 +1 @@ +Subproject commit 0efcb0bd03cca063189e909dba9f20355619317a From d225e31c0c791f627ab6e65046918e0e135206a3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 31 Jan 2024 12:16:14 +0100 Subject: [PATCH 02/40] Add Boogie as a submodule --- Source/Dafny.sln | 38 +++++++++++++++++++++++++++++++ Source/DafnyCore/DafnyCore.csproj | 12 +++++++++- boogie | 2 +- 3 files changed, 50 insertions(+), 2 deletions(-) diff --git a/Source/Dafny.sln b/Source/Dafny.sln index 23297b185ed..fc8e8b1fa49 100644 --- a/Source/Dafny.sln +++ b/Source/Dafny.sln @@ -43,6 +43,32 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}" EndProject +Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Boogie", "Boogie", "{60332269-9C5D-465E-8582-01F9B738BD90}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BaseTypes", "..\boogie\Source\BaseTypes\BaseTypes.csproj", "{68721962-0D91-4355-BC94-BE1CCBD30E47}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbstractInterpretation", "..\boogie\Source\AbstractInterpretation\AbstractInterpretation.csproj", "{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj", "{09662044-5640-4785-92E3-2F7CDBA4DDB2}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "..\boogie\Source\Concurrency\Concurrency.csproj", "{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "..\boogie\Source\Core\Core.csproj", "{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj", "{0145DC89-7243-41F8-AB3E-F716F04E9BFF}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "..\boogie\Source\Graph\Graph.csproj", "{05DE24BB-D639-40C4-894F-701652F51559}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "..\boogie\Source\Houdini\Houdini.csproj", "{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "..\boogie\Source\Model\Model.csproj", "{D97C23B6-FB4A-4450-930E-58EC83D308A0}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "..\boogie\Source\Provers\SMTLib\SMTLib.csproj", "{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "..\boogie\Source\VCExpr\VCExpr.csproj", "{E760E37E-0257-4C96-89C4-722F85BABDBB}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "..\boogie\Source\VCGeneration\VCGeneration.csproj", "{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}" +EndProject EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution @@ -138,5 +164,17 @@ Global SolutionGuid = {280F572B-D27A-4613-998F-00B6FFE01187} EndGlobalSection GlobalSection(NestedProjects) = preSolution + {68721962-0D91-4355-BC94-BE1CCBD30E47} = {60332269-9C5D-465E-8582-01F9B738BD90} + {2A6B36F4-9F15-459A-8EDB-5BAEED98FE17} = {60332269-9C5D-465E-8582-01F9B738BD90} + {09662044-5640-4785-92E3-2F7CDBA4DDB2} = {60332269-9C5D-465E-8582-01F9B738BD90} + {DA8A9BA8-9BBA-4C64-9736-FD967517DCA9} = {60332269-9C5D-465E-8582-01F9B738BD90} + {2BF5ECCA-24B2-4A4B-86B6-D0DB17331109} = {60332269-9C5D-465E-8582-01F9B738BD90} + {0145DC89-7243-41F8-AB3E-F716F04E9BFF} = {60332269-9C5D-465E-8582-01F9B738BD90} + {05DE24BB-D639-40C4-894F-701652F51559} = {60332269-9C5D-465E-8582-01F9B738BD90} + {51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6} = {60332269-9C5D-465E-8582-01F9B738BD90} + {D97C23B6-FB4A-4450-930E-58EC83D308A0} = {60332269-9C5D-465E-8582-01F9B738BD90} + {0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F} = {60332269-9C5D-465E-8582-01F9B738BD90} + {E760E37E-0257-4C96-89C4-722F85BABDBB} = {60332269-9C5D-465E-8582-01F9B738BD90} + {1EE372AA-4FF9-47FB-9C04-18CBF219F6E8} = {60332269-9C5D-465E-8582-01F9B738BD90} EndGlobalSection EndGlobal diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 136dd72f1ce..13ed0280f25 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -33,7 +33,17 @@ - + + + + + + + + + + + diff --git a/boogie b/boogie index 0efcb0bd03c..0988838c40e 160000 --- a/boogie +++ b/boogie @@ -1 +1 @@ -Subproject commit 0efcb0bd03cca063189e909dba9f20355619317a +Subproject commit 0988838c40e3536ab30262f1aee29a4c056881e8 From ea44d00c494c68a3a6eb82a72ab31f9178afc922 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 31 Jan 2024 12:17:51 +0100 Subject: [PATCH 03/40] Trying to get back to existing behavior --- Source/DafnyCore/Pipeline/Compilation.cs | 5 ++- Source/DafnyCore/ProofDependencyWarnings.cs | 32 +++++++++++++------ Source/DafnyDriver/CliCompilation.cs | 9 ++++-- .../Various/SlowVerifier.cs | 2 ++ 4 files changed, 32 insertions(+), 16 deletions(-) diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index fbacf6f4030..67e1b9dd837 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -249,7 +249,7 @@ public static string GetSplitName(ManualSplit split) { //return prefix; } - + public static string GetImplementationName(Implementation implementation) { var prefix = implementation.Name.Split(BoogieGenerator.NameSeparator)[0]; @@ -315,8 +315,7 @@ public async Task VerifyCanVerify(ICanVerify canVerify, bool onlyPrepareVe } private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterTests, ICanVerify canVerify, - ResolutionResult resolution) - { + ResolutionResult resolution) { try { var ticket = verificationTickets.Dequeue(CancellationToken.None); diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index 2a4d6c1e467..1bfae630398 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -1,5 +1,7 @@ +using System.Collections.Generic; using System.Linq; using DafnyCore.Verifier; +using Microsoft.Boogie; using Microsoft.Dafny.ProofObligationDescription; using VC; @@ -11,23 +13,33 @@ public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, Er 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 != VcOutcome.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,14 +51,14 @@ 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)) { + if (ShouldWarnVacuous(dafnyOptions, scopeName, obligation)) { reporter.Warning(MessageSource.Verifier, "", obligation.Range, $"proved using contradictory assumptions: {obligation.Description}"); } } 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/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 98e9624659e..c637079d352 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -209,13 +209,16 @@ public async Task VerifyAllAndPrintSummary() { foreach (var (task, completed) in results.CompletedParts.OrderBy(t => t.Task.Split.Token)) { Compilation.ReportDiagnosticsInResult(options, task, completed.Result, Compilation.Reporter); + } + + foreach (var resultsForScope in results.CompletedParts.GroupBy(p => p.Task.ScopeToken)) { ProofDependencyWarnings.WarnAboutSuspiciousDependenciesForImplementation(options, resolution.ResolvedProgram!.Reporter, resolution.ResolvedProgram.ProofDependencyManager, - new DafnyConsolePrinter.ImplementationLogEntry(task.Implementation.VerboseName, - task.Implementation.tok), - DafnyConsolePrinter.DistillVerificationResult(completed.Result)); + resultsForScope.Key.val, + resultsForScope.Select(p => p.Result.Result).ToList()); } + } catch (ProverException e) { Interlocked.Increment(ref statSum.SolverExceptionCount); Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, e.Message); diff --git a/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs b/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs index 8f46a6cc7fd..8dcc89e41e5 100644 --- a/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs +++ b/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs @@ -48,6 +48,8 @@ public NeverVerifiesImplementationTask(IVerificationTask original) { public IVerificationStatus CacheStatus => new Stale(); public ProcessedProgram ProcessedProgram => original.ProcessedProgram; public ManualSplit Split => original.Split; + public Boogie.IToken ScopeToken => original.ScopeToken; + public Boogie.IToken Token => original.Token; public IObservable TryRun() { return source; From d1389193d5c98b3038ca1a20699bb176da030bbf Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 31 Jan 2024 13:47:41 +0100 Subject: [PATCH 04/40] Exclude boogie folder in format command --- Makefile | 2 +- Source/DafnyDriver/CliCompilation.cs | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 7de9d5483db..5b490a319cf 100644 --- a/Makefile +++ b/Makefile @@ -62,7 +62,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/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index c637079d352..acef49dd508 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -208,7 +208,6 @@ public async Task VerifyAllAndPrintSummary() { await results.Finished.Task; foreach (var (task, completed) in results.CompletedParts.OrderBy(t => t.Task.Split.Token)) { Compilation.ReportDiagnosticsInResult(options, task, completed.Result, Compilation.Reporter); - } foreach (var resultsForScope in results.CompletedParts.GroupBy(p => p.Task.ScopeToken)) { From 5350dfa954237b9152dcba247992451c338fc003 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 31 Jan 2024 14:19:59 +0100 Subject: [PATCH 05/40] Fixes --- Source/DafnyCore/Pipeline/Compilation.cs | 22 +++---- .../Custom/DafnyCounterExampleHandler.cs | 2 +- .../DafnyLanguageServer/Workspace/IdeState.cs | 64 +++++++++---------- .../Workspace/NotificationPublisher.cs | 5 +- boogie | 2 +- 5 files changed, 48 insertions(+), 47 deletions(-) diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index 67e1b9dd837..45010c29002 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -237,17 +237,17 @@ private async Task ResolveAsync() { } } - public static string GetSplitName(ManualSplit split) { - return split.Implementation.Name; // TODO fix. - // var prefix = implementation.Name.Split(BoogieGenerator.NameSeparator)[0]; - // - // // 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) { - // prefix += "." + refinementToken.InheritingModule.Name; - // } - - //return prefix; + public static string GetTaskName(IVerificationTask split) { + var dafnyToken = BoogieGenerator.ToDafnyToken(false, split.Token); + var prefix = dafnyToken.line + "," + dafnyToken.col; + + // 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 (split.ScopeToken is RefinementToken refinementToken) { + prefix += "." + refinementToken.InheritingModule.Name; + } + + return prefix; } public static string GetImplementationName(Implementation implementation) { diff --git a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs index 3df1385be3f..b52ff04fc13 100644 --- a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs @@ -60,7 +60,7 @@ private static bool FinishedVerifyingUri(IdeState s, Uri uri) { return s.Status == CompilationStatus.ResolutionSucceeded && s.VerificationResults[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/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index 0a3dd267f35..2745a1dfbd8 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -17,11 +17,11 @@ namespace Microsoft.Dafny.LanguageServer.Workspace; -public record IdeImplementationView(Range Range, PublishedVerificationStatus Status, +public record IdeVerificationTaskState(Range Range, PublishedVerificationStatus Status, IReadOnlyList Diagnostics, bool HitErrorLimit); public enum VerificationPreparationState { NotStarted, InProgress, Done } -public record IdeVerificationResult(VerificationPreparationState PreparationProgress, ImmutableDictionary Implementations); +public record IdeVerificationResult(VerificationPreparationState PreparationProgress, ImmutableDictionary VerificationTasks); /// /// Contains information from the latest document, and from older documents if some information is missing, @@ -104,8 +104,8 @@ private 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,7 +115,7 @@ private ImmutableDictionary 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)); + return x.Value.VerificationTasks.Values.SelectMany(v => v.Diagnostics).Concat(GetErrorLimitDiagnostics(x)); }); return resolutionDiagnostics.Concat(verificationDiagnostics); } private static IEnumerable GetErrorLimitDiagnostics(KeyValuePair x) { - var anyImplementationHitErrorLimit = x.Value.Implementations.Values.Any(i => i.HitErrorLimit); + var anyImplementationHitErrorLimit = x.Value.VerificationTasks.Values.Any(i => i.HitErrorLimit); IEnumerable result; if (anyImplementationHitErrorLimit) { var diagnostic = new Diagnostic() { @@ -224,11 +224,11 @@ private IdeState UpdateScheduledVerification(ScheduledVerification scheduledVeri var uri = scheduledVerification.CanVerify.Tok.Uri; var range = scheduledVerification.CanVerify.NameToken.GetLspRange(); var previousVerificationResult = previousState.VerificationResults[uri][range]; - var previousImplementations = previousVerificationResult.Implementations; + 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 { + VerificationTasks: previousImplementations.ToImmutableDictionary(kv => kv.Key, kv => kv.Value with { Status = PublishedVerificationStatus.Stale, Diagnostics = IdeState.MarkDiagnosticsAsOutdated(kv.Value.Diagnostics).ToList() })); @@ -329,8 +329,8 @@ private IdeState UpdateFinishedResolution(DafnyOptions options, private static IdeVerificationResult MergeResults(IEnumerable results) { return results.Aggregate((a, b) => new IdeVerificationResult( MergeStates(a.PreparationProgress, b.PreparationProgress), - a.Implementations.ToImmutableDictionary().Merge(b.Implementations, - (aView, bView) => new IdeImplementationView( + a.VerificationTasks.ToImmutableDictionary().Merge(b.VerificationTasks, + (aView, bView) => new IdeVerificationTaskState( aView.Range, Combine(aView.Status, bView.Status), aView.Diagnostics.Concat(bView.Diagnostics).ToList(), aView.HitErrorLimit || bView.HitErrorLimit)))); @@ -347,10 +347,10 @@ private static PublishedVerificationStatus Combine(PublishedVerificationStatus f private static IdeVerificationResult MergeVerifiable(IdeState previousState, ICanVerify canVerify) { var range = canVerify.NameToken.GetLspRange(); var previousImplementations = - previousState.GetVerificationResults(canVerify.NameToken.Uri).GetValueOrDefault(range)?.Implementations ?? - ImmutableDictionary.Empty; + previousState.GetVerificationResults(canVerify.NameToken.Uri).GetValueOrDefault(range)?.VerificationTasks ?? + ImmutableDictionary.Empty; return new IdeVerificationResult(PreparationProgress: VerificationPreparationState.NotStarted, - Implementations: previousImplementations.ToImmutableDictionary(kv => kv.Key, kv => kv.Value with { + VerificationTasks: previousImplementations.ToImmutableDictionary(kv => kv.Key, kv => kv.Value with { Status = PublishedVerificationStatus.Stale, Diagnostics = IdeState.MarkDiagnosticsAsOutdated(kv.Value.Diagnostics).ToList() })); @@ -390,13 +390,13 @@ 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.GetSplitName(t.Split)); + var previousImplementations = previousState.VerificationResults[uri][range].VerificationTasks; + var names = canVerifyPartsIdentified.Parts.Select(Compilation.GetTaskName); var verificationResult = new IdeVerificationResult(PreparationProgress: VerificationPreparationState.Done, - Implementations: names.ToImmutableDictionary(k => k, + VerificationTasks: names.ToImmutableDictionary(k => k, k => { var previous = previousImplementations.GetValueOrDefault(k); - return new IdeImplementationView(range, PublishedVerificationStatus.Queued, + return new IdeVerificationTaskState(range, PublishedVerificationStatus.Queued, previous?.Diagnostics ?? Array.Empty(), previous?.HitErrorLimit ?? false); })); @@ -409,14 +409,14 @@ private IdeState UpdateCanVerifyPartsUpdated(ILogger logger, CanVerifyPartsIdent private IdeState UpdateBoogieException(BoogieException boogieException) { var previousState = this; - var name = Compilation.GetSplitName(boogieException.Task.Split); + 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 previousImplementations = previousVerificationResult.VerificationTasks; var previousView = previousImplementations.GetValueOrDefault(name) ?? - new IdeImplementationView(range, PublishedVerificationStatus.Error, Array.Empty(), false); + new IdeVerificationTaskState(range, PublishedVerificationStatus.Error, Array.Empty(), false); var diagnostics = previousView.Diagnostics; var internalErrorDiagnostic = new Diagnostic { @@ -426,12 +426,12 @@ 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(), previousView.HitErrorLimit); return previousState with { VerificationResults = previousState.VerificationResults.SetItem(uri, previousState.VerificationResults[uri].SetItem(range, previousVerificationResult with { - Implementations = previousVerificationResult.Implementations.SetItem(name, view) + VerificationTasks = previousVerificationResult.VerificationTasks.SetItem(name, view) })) }; } @@ -440,15 +440,15 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie var previousState = this; UpdateGutterIconTrees(boogieUpdate, options, logger); - var name = Compilation.GetSplitName(boogieUpdate.VerificationTask.Split); + 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 previousImplementations = previousVerificationResult.VerificationTasks; var previousView = previousImplementations.GetValueOrDefault(name) ?? - new IdeImplementationView(range, status, Array.Empty(), false); + new IdeVerificationTaskState(range, status, Array.Empty(), false); var counterExamples = previousState.Counterexamples; bool hitErrorLimit = previousView.HitErrorLimit; var diagnostics = previousView.Diagnostics; @@ -458,11 +458,11 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie hitErrorLimit = false; } - if (boogieUpdate.BoogieStatus is Completed batchCompleted) { - counterExamples = counterExamples.Concat(batchCompleted.Result.CounterExamples); - hitErrorLimit |= batchCompleted.Result.MaxCounterExamples == batchCompleted.Result.CounterExamples.Count; + if (boogieUpdate.BoogieStatus is Completed completed) { + counterExamples = counterExamples.Concat(completed.Result.CounterExamples); + hitErrorLimit |= completed.Result.MaxCounterExamples == completed.Result.CounterExamples.Count; var newDiagnostics = - Compilation.GetDiagnosticsFromResult(options, previousState.Uri, boogieUpdate.VerificationTask, batchCompleted.Result).ToArray(); + Compilation.GetDiagnosticsFromResult(options, previousState.Uri, boogieUpdate.VerificationTask, completed.Result).ToArray(); diagnostics = diagnostics.Concat(newDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); logger.LogTrace( $"BatchCompleted received for {previousState.Input} and found #{newDiagnostics.Length} new diagnostics."); @@ -490,13 +490,13 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie // diagnostics = diagnostics.Concat(verificationCoverageDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); // } - var view = new IdeImplementationView(range, status, diagnostics.ToList(), + var view = new IdeVerificationTaskState(range, status, diagnostics.ToList(), previousView.HitErrorLimit || hitErrorLimit); return previousState with { Counterexamples = counterExamples, VerificationResults = previousState.VerificationResults.SetItem(uri, previousState.VerificationResults[uri].SetItem(range, previousVerificationResult with { - Implementations = previousVerificationResult.Implementations.SetItem(name, view) + VerificationTasks = previousVerificationResult.VerificationTasks.SetItem(name, view) })) }; } diff --git a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs index 86e19303d91..684af10479f 100644 --- a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs +++ b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs @@ -102,7 +102,7 @@ private static NamedVerifiableStatus GetNamedVerifiableStatuses(Range canVerify, VerificationPreparationState.NotStarted => PublishedVerificationStatus.Stale, VerificationPreparationState.InProgress => PublishedVerificationStatus.Queued, VerificationPreparationState.Done => - result.Implementations.Values.Select(v => v.Status).Aggregate(nothingToVerifyStatus, Combine), + result.VerificationTasks.Values.Select(v => v.Status).Aggregate(nothingToVerifyStatus, Combine), _ => throw new ArgumentOutOfRangeException() }; @@ -112,7 +112,8 @@ 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; + var minMaxRunning = new [] { PublishedVerificationStatus.Running, min }.Max(); + return max >= PublishedVerificationStatus.Error ? minMaxRunning : max; } private readonly ConcurrentDictionary> publishedDiagnostics = new(); diff --git a/boogie b/boogie index 0988838c40e..2e8f775b749 160000 --- a/boogie +++ b/boogie @@ -1 +1 @@ -Subproject commit 0988838c40e3536ab30262f1aee29a4c056881e8 +Subproject commit 2e8f775b7498a113b7b6f22eb26cd049047e82d4 From 38745862fd4f7fe95983ebc3d643705fd3ef61c0 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 31 Jan 2024 14:24:51 +0100 Subject: [PATCH 06/40] Rename --- .../Custom/DafnyCounterExampleHandler.cs | 4 +- .../DafnyLanguageServer/Workspace/IdeState.cs | 69 ++++++++++--------- .../Workspace/NotificationPublisher.cs | 2 +- 3 files changed, 38 insertions(+), 37 deletions(-) diff --git a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs index b52ff04fc13..9e4d9996c10 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,7 +58,7 @@ 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.VerificationTasks.Values.All(v => v.Status >= PublishedVerificationStatus.Error)); } diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index 2745a1dfbd8..417c84f1328 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -21,7 +21,7 @@ public record IdeVerificationTaskState(Range Range, PublishedVerificationStatus IReadOnlyList Diagnostics, bool HitErrorLimit); public enum VerificationPreparationState { NotStarted, InProgress, Done } -public record IdeVerificationResult(VerificationPreparationState PreparationProgress, ImmutableDictionary VerificationTasks); +public record IdeCanVerifyState(VerificationPreparationState PreparationProgress, ImmutableDictionary VerificationTasks); /// /// Contains information from the latest document, and from older documents if some information is missing, @@ -37,7 +37,7 @@ public record IdeState( Node? ResolvedProgram, SymbolTable SymbolTable, LegacySignatureAndCompletionTable SignatureAndCompletionTable, - ImmutableDictionary> VerificationResults, + ImmutableDictionary> CanVerifyStates, IReadOnlyList Counterexamples, IReadOnlyDictionary> GhostRanges, ImmutableDictionary VerificationTrees @@ -62,7 +62,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,27 +77,27 @@ 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) { @@ -121,9 +121,9 @@ 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() { @@ -138,7 +138,7 @@ public IEnumerable GetDiagnosticsForUri(Uri uri) { return resolutionDiagnostics.Concat(verificationDiagnostics); } - private static IEnumerable GetErrorLimitDiagnostics(KeyValuePair x) { + private static IEnumerable GetErrorLimitDiagnostics(KeyValuePair x) { var anyImplementationHitErrorLimit = x.Value.VerificationTasks.Values.Any(i => i.HitErrorLimit); IEnumerable result; if (anyImplementationHitErrorLimit) { @@ -159,7 +159,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, @@ -223,18 +223,18 @@ private IdeState UpdateScheduledVerification(ScheduledVerification scheduledVeri var uri = scheduledVerification.CanVerify.Tok.Uri; var range = scheduledVerification.CanVerify.NameToken.GetLspRange(); - var previousVerificationResult = previousState.VerificationResults[uri][range]; + var previousVerificationResult = previousState.CanVerifyStates[uri][range]; var previousImplementations = previousVerificationResult.VerificationTasks; var preparationProgress = new[] { previousVerificationResult.PreparationProgress, VerificationPreparationState.InProgress }.Max(); - var verificationResult = new IdeVerificationResult(PreparationProgress: preparationProgress, + 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() })); 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)) }; } @@ -305,7 +305,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, @@ -321,13 +321,13 @@ private IdeState UpdateFinishedResolution(DafnyOptions options, 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.VerificationTasks.ToImmutableDictionary().Merge(b.VerificationTasks, (aView, bView) => new IdeVerificationTaskState( @@ -344,12 +344,12 @@ 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 previousImplementations = previousState.GetVerificationResults(canVerify.NameToken.Uri).GetValueOrDefault(range)?.VerificationTasks ?? ImmutableDictionary.Empty; - return new IdeVerificationResult(PreparationProgress: VerificationPreparationState.NotStarted, + 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() @@ -390,9 +390,9 @@ private IdeState UpdateCanVerifyPartsUpdated(ILogger logger, CanVerifyPartsIdent canVerifyPartsIdentified.CanVerify, implementations.ToArray()); var range = canVerifyPartsIdentified.CanVerify.NameToken.GetLspRange(); - var previousImplementations = previousState.VerificationResults[uri][range].VerificationTasks; + var previousImplementations = previousState.CanVerifyStates[uri][range].VerificationTasks; var names = canVerifyPartsIdentified.Parts.Select(Compilation.GetTaskName); - var verificationResult = new IdeVerificationResult(PreparationProgress: VerificationPreparationState.Done, + var verificationResult = new IdeCanVerifyState(PreparationProgress: VerificationPreparationState.Done, VerificationTasks: names.ToImmutableDictionary(k => k, k => { var previous = previousImplementations.GetValueOrDefault(k); @@ -401,8 +401,8 @@ private IdeState UpdateCanVerifyPartsUpdated(ILogger logger, CanVerifyPartsIdent previous?.HitErrorLimit ?? false); })); 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)) }; } @@ -413,7 +413,7 @@ private IdeState UpdateBoogieException(BoogieException boogieException) { var uri = boogieException.CanVerify.Tok.Uri; var range = boogieException.CanVerify.NameToken.GetLspRange(); - var previousVerificationResult = previousState.VerificationResults[uri][range]; + var previousVerificationResult = previousState.CanVerifyStates[uri][range]; var previousImplementations = previousVerificationResult.VerificationTasks; var previousView = previousImplementations.GetValueOrDefault(name) ?? new IdeVerificationTaskState(range, PublishedVerificationStatus.Error, Array.Empty(), false); @@ -429,8 +429,8 @@ private IdeState UpdateBoogieException(BoogieException boogieException) { var view = new IdeVerificationTaskState(range, PublishedVerificationStatus.Error, diagnostics.ToList(), previousView.HitErrorLimit); return previousState with { - VerificationResults = previousState.VerificationResults.SetItem(uri, - previousState.VerificationResults[uri].SetItem(range, previousVerificationResult with { + CanVerifyStates = previousState.CanVerifyStates.SetItem(uri, + previousState.CanVerifyStates[uri].SetItem(range, previousVerificationResult with { VerificationTasks = previousVerificationResult.VerificationTasks.SetItem(name, view) })) }; @@ -445,7 +445,7 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie var uri = boogieUpdate.CanVerify.Tok.Uri; var range = boogieUpdate.CanVerify.NameToken.GetLspRange(); - var previousVerificationResult = previousState.VerificationResults[uri][range]; + var previousVerificationResult = previousState.CanVerifyStates[uri][range]; var previousImplementations = previousVerificationResult.VerificationTasks; var previousView = previousImplementations.GetValueOrDefault(name) ?? new IdeVerificationTaskState(range, status, Array.Empty(), false); @@ -472,6 +472,7 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie // WarnContradictoryAssumptions should be executable based on a single assertion batch. // WarnRedundantAssumptions is more like find references. It needs all the batches under in a verification scope. // If we're saying that WarnRedundantAssumptions is critical, than verifying single assertions is crap. + // if (boogieUpdate.BoogieStatus is Completed completed) { // var errorReporter = new ObservableErrorReporter(options, uri); // List verificationCoverageDiagnostics = new(); @@ -494,8 +495,8 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie previousView.HitErrorLimit || hitErrorLimit); return previousState with { Counterexamples = counterExamples, - VerificationResults = previousState.VerificationResults.SetItem(uri, - previousState.VerificationResults[uri].SetItem(range, previousVerificationResult with { + CanVerifyStates = previousState.CanVerifyStates.SetItem(uri, + previousState.CanVerifyStates[uri].SetItem(range, previousVerificationResult with { VerificationTasks = previousVerificationResult.VerificationTasks.SetItem(name, view) })) }; diff --git a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs index 684af10479f..cd82932f64a 100644 --- a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs +++ b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs @@ -96,7 +96,7 @@ 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, From 87b22dd4fc6851cda3e7a9b5ea0016009c9ef05d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 31 Jan 2024 17:33:15 +0100 Subject: [PATCH 07/40] Step towards getting RedundantAssumptionsGetWarnings to work again --- Source/DafnyCore/ProofDependencyWarnings.cs | 15 ++++ .../Verifier/ProofDependencyManager.cs | 4 +- Source/DafnyDriver/CliCompilation.cs | 13 +-- .../DafnyLanguageServer/Workspace/IdeState.cs | 80 ++++++++++++------- 4 files changed, 69 insertions(+), 43 deletions(-) diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index 1bfae630398..ba7f5f595c1 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -1,3 +1,4 @@ +using System.Collections.Concurrent; using System.Collections.Generic; using System.Linq; using DafnyCore.Verifier; @@ -8,6 +9,20 @@ 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.ScopeToken)) { + WarnAboutSuspiciousDependenciesForImplementation(options, + reporter, + manager, + resultsForScope.Key.val, + 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 = diff --git a/Source/DafnyCore/Verifier/ProofDependencyManager.cs b/Source/DafnyCore/Verifier/ProofDependencyManager.cs index 0d5522e6ce0..b2daad8a22c 100644 --- a/Source/DafnyCore/Verifier/ProofDependencyManager.cs +++ b/Source/DafnyCore/Verifier/ProofDependencyManager.cs @@ -19,7 +19,7 @@ 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; @@ -44,7 +44,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/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index acef49dd508..067a6b10133 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -12,10 +12,7 @@ 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; namespace DafnyDriver.Commands; @@ -210,13 +207,9 @@ public async Task VerifyAllAndPrintSummary() { Compilation.ReportDiagnosticsInResult(options, task, completed.Result, Compilation.Reporter); } - foreach (var resultsForScope in results.CompletedParts.GroupBy(p => p.Task.ScopeToken)) { - ProofDependencyWarnings.WarnAboutSuspiciousDependenciesForImplementation(options, - resolution.ResolvedProgram!.Reporter, - resolution.ResolvedProgram.ProofDependencyManager, - resultsForScope.Key.val, - resultsForScope.Select(p => p.Result.Result).ToList()); - } + var parts = results.CompletedParts; + ProofDependencyWarnings.ReportSuspiciousDependencies(options, parts, + resolution.ResolvedProgram.Reporter, resolution.ResolvedProgram.ProofDependencyManager); } catch (ProverException e) { Interlocked.Increment(ref statSum.SolverExceptionCount); diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index 417c84f1328..03f91779381 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -18,10 +18,12 @@ namespace Microsoft.Dafny.LanguageServer.Workspace; public record IdeVerificationTaskState(Range Range, PublishedVerificationStatus Status, - IReadOnlyList Diagnostics, bool HitErrorLimit); + IReadOnlyList Diagnostics, bool HitErrorLimit, IVerificationTask Task, IVerificationStatus RawStatus); public enum VerificationPreparationState { NotStarted, InProgress, Done } -public record IdeCanVerifyState(VerificationPreparationState PreparationProgress, ImmutableDictionary VerificationTasks); +public record IdeCanVerifyState(VerificationPreparationState PreparationProgress, + ImmutableDictionary VerificationTasks, + IReadOnlyList Diagnostics); /// /// Contains information from the latest document, and from older documents if some information is missing, @@ -133,7 +135,8 @@ public IEnumerable GetAllDiagnostics() { public IEnumerable GetDiagnosticsForUri(Uri uri) { var resolutionDiagnostics = StaticDiagnostics.GetValueOrDefault(uri) ?? Enumerable.Empty(); var verificationDiagnostics = GetVerificationResults(uri).SelectMany(x => { - return x.Value.VerificationTasks.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); } @@ -230,8 +233,8 @@ private IdeState UpdateScheduledVerification(ScheduledVerification scheduledVeri 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 { CanVerifyStates = previousState.CanVerifyStates.SetItem(uri, previousState.CanVerifyStates[uri].SetItem(range, verificationResult)) @@ -330,10 +333,8 @@ private static IdeCanVerifyState MergeResults(IEnumerable res return results.Aggregate((a, b) => new IdeCanVerifyState( MergeStates(a.PreparationProgress, b.PreparationProgress), a.VerificationTasks.ToImmutableDictionary().Merge(b.VerificationTasks, - (aView, bView) => new IdeVerificationTaskState( - aView.Range, - Combine(aView.Status, bView.Status), - aView.Diagnostics.Concat(bView.Diagnostics).ToList(), aView.HitErrorLimit || bView.HitErrorLimit)))); + (aView, bView) => aView /* Merge should not occur */), + a.Diagnostics.Concat(b.Diagnostics))); } private static VerificationPreparationState MergeStates(VerificationPreparationState a, VerificationPreparationState b) { @@ -346,14 +347,15 @@ private static PublishedVerificationStatus Combine(PublishedVerificationStatus f 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)?.VerificationTasks ?? + 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) { @@ -393,13 +395,13 @@ private IdeState UpdateCanVerifyPartsUpdated(ILogger logger, CanVerifyPartsIdent var previousImplementations = previousState.CanVerifyStates[uri][range].VerificationTasks; var names = canVerifyPartsIdentified.Parts.Select(Compilation.GetTaskName); var verificationResult = new IdeCanVerifyState(PreparationProgress: VerificationPreparationState.Done, - VerificationTasks: names.ToImmutableDictionary(k => k, + VerificationTasks: canVerifyPartsIdentified.Parts.ToImmutableDictionary(Compilation.GetTaskName, k => { - var previous = previousImplementations.GetValueOrDefault(k); + 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 { CanVerifyStates = previousState.CanVerifyStates.SetItem(uri, previousState.CanVerifyStates[uri].SetItem(range, verificationResult)) @@ -415,9 +417,9 @@ private IdeState UpdateBoogieException(BoogieException boogieException) { var previousVerificationResult = previousState.CanVerifyStates[uri][range]; var previousImplementations = previousVerificationResult.VerificationTasks; - var previousView = previousImplementations.GetValueOrDefault(name) ?? - new IdeVerificationTaskState(range, PublishedVerificationStatus.Error, Array.Empty(), false); - var diagnostics = previousView.Diagnostics; + 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,7 +428,7 @@ private IdeState UpdateBoogieException(BoogieException boogieException) { }; diagnostics = diagnostics.Concat(new[] { internalErrorDiagnostic }).ToList(); - var view = new IdeVerificationTaskState(range, PublishedVerificationStatus.Error, diagnostics.ToList(), previousView.HitErrorLimit); + var view = new IdeVerificationTaskState(range, PublishedVerificationStatus.Error, diagnostics.ToList(), hitErrorLimit, boogieException.Task, new Stale()); return previousState with { CanVerifyStates = previousState.CanVerifyStates.SetItem(uri, @@ -447,11 +449,11 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie var previousVerificationResult = previousState.CanVerifyStates[uri][range]; var previousImplementations = previousVerificationResult.VerificationTasks; - var previousView = previousImplementations.GetValueOrDefault(name) ?? - new IdeVerificationTaskState(range, status, Array.Empty(), false); + 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(); @@ -459,13 +461,13 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie } if (boogieUpdate.BoogieStatus is Completed completed) { - counterExamples = counterExamples.Concat(completed.Result.CounterExamples); + counterExamples = completed.Result.CounterExamples; hitErrorLimit |= completed.Result.MaxCounterExamples == completed.Result.CounterExamples.Count; var newDiagnostics = - Compilation.GetDiagnosticsFromResult(options, previousState.Uri, boogieUpdate.VerificationTask, completed.Result).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."); } // TODO Come up with a solution @@ -491,13 +493,29 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie // diagnostics = diagnostics.Concat(verificationCoverageDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); // } - var view = new IdeVerificationTaskState(range, status, diagnostics.ToList(), - previousView.HitErrorLimit || hitErrorLimit); + var newCanVerifyDiagnostics = new List(); + var taskState = new IdeVerificationTaskState(range, status, diagnostics.ToList(), + hitErrorLimit, boogieUpdate.VerificationTask, rawStatus); + var newTaskStates = previousVerificationResult.VerificationTasks.SetItem(name, taskState); + if (newTaskStates.Values.All(s => s.Status >= PublishedVerificationStatus.Error)) { + + var errorReporter = new ObservableErrorReporter(options, uri); + List verificationCoverageDiagnostics = new(); + errorReporter.Updates.Subscribe(d => verificationCoverageDiagnostics.Add(d.Diagnostic)); + + ProofDependencyWarnings.ReportSuspiciousDependencies(options, + newTaskStates.Values.Select(s => (s.Task, (Completed)s.RawStatus)), + errorReporter, boogieUpdate.ProofDependencyManager); + + newCanVerifyDiagnostics = previousVerificationResult.Diagnostics.Concat(verificationCoverageDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); + } + return previousState with { Counterexamples = counterExamples, CanVerifyStates = previousState.CanVerifyStates.SetItem(uri, previousState.CanVerifyStates[uri].SetItem(range, previousVerificationResult with { - VerificationTasks = previousVerificationResult.VerificationTasks.SetItem(name, view) + VerificationTasks = newTaskStates, + Diagnostics = newCanVerifyDiagnostics })) }; } From 536b1c4fb5f257b8373beeaaa2fa6d7b80499c52 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 31 Jan 2024 17:42:48 +0100 Subject: [PATCH 08/40] RedundantAssumptionsGetWarnings works now --- Source/DafnyCore/ProofDependencyWarnings.cs | 4 ++-- Source/DafnyCore/Verifier/BoogieGenerator.cs | 2 +- Source/DafnyCore/Verifier/ProofDependencyManager.cs | 11 ++++------- .../DafnyLanguageServer.Test/Various/SlowVerifier.cs | 1 + boogie | 2 +- 5 files changed, 9 insertions(+), 11 deletions(-) diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index ba7f5f595c1..cd3233680f5 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -14,11 +14,11 @@ 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.ScopeToken)) { + foreach (var resultsForScope in parts.GroupBy(p => p.Task.ScopeId)) { WarnAboutSuspiciousDependenciesForImplementation(options, reporter, manager, - resultsForScope.Key.val, + resultsForScope.Key, resultsForScope.Select(p => p.Result.Result).ToList()); } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 18c4f0c2efa..d44e9acd79d 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 b2daad8a22c..52ec364eeb2 100644 --- a/Source/DafnyCore/Verifier/ProofDependencyManager.cs +++ b/Source/DafnyCore/Verifier/ProofDependencyManager.cs @@ -21,22 +21,19 @@ public class ProofDependencyManager { public Dictionary ProofDependenciesById { get; } = 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) { diff --git a/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs b/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs index 8dcc89e41e5..9674f8ef705 100644 --- a/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs +++ b/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs @@ -49,6 +49,7 @@ public NeverVerifiesImplementationTask(IVerificationTask original) { public ProcessedProgram ProcessedProgram => original.ProcessedProgram; 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() { diff --git a/boogie b/boogie index 2e8f775b749..a1871efd793 160000 --- a/boogie +++ b/boogie @@ -1 +1 @@ -Subproject commit 2e8f775b7498a113b7b6f22eb26cd049047e82d4 +Subproject commit a1871efd79340aa02b3f66d6d7b9bceaacd08433 From 178b85a735640ef1021da30efdabaafe85a1685c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 31 Jan 2024 18:47:34 +0100 Subject: [PATCH 09/40] Trigger CI From bed7a5d5eeaa59f0916ec96c0b71360132282039 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 1 Feb 2024 13:54:57 +0100 Subject: [PATCH 10/40] Enable --filter-position on individual assertions/ensures clauses, fix a crash and fix an output ordering bug --- .../DafnyCore/Generic/BatchErrorReporter.cs | 3 +- Source/DafnyCore/Pipeline/Compilation.cs | 25 ++++++------ Source/DafnyCore/ProofDependencyWarnings.cs | 9 ++--- Source/DafnyDriver/CliCanVerifyResults.cs | 7 ++-- Source/DafnyDriver/CliCompilation.cs | 39 ++++++++++++++----- .../DafnyLanguageServer/Workspace/IdeState.cs | 12 +++--- .../Workspace/NotificationPublisher.cs | 2 +- .../LitTests/LitTest/verification/filter.dfy | 9 +++-- .../LitTest/verification/filter.dfy.expect | 11 ++++-- 9 files changed, 69 insertions(+), 48 deletions(-) diff --git a/Source/DafnyCore/Generic/BatchErrorReporter.cs b/Source/DafnyCore/Generic/BatchErrorReporter.cs index e8dba15f7dd..ddb291c427d 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/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index 45010c29002..3b5211add5c 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -240,12 +240,12 @@ private async Task ResolveAsync() { public static string GetTaskName(IVerificationTask split) { var dafnyToken = BoogieGenerator.ToDafnyToken(false, split.Token); var prefix = dafnyToken.line + "," + dafnyToken.col; - - // 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 (split.ScopeToken is RefinementToken refinementToken) { - prefix += "." + refinementToken.InheritingModule.Name; - } + + // 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 (split.ScopeToken is RefinementToken refinementToken) { + prefix += "." + refinementToken.InheritingModule.Name; + } return prefix; } @@ -289,10 +289,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)) { @@ -306,16 +307,16 @@ 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); @@ -360,7 +361,7 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT await ticket; if (!onlyPrepareVerificationForGutterTests) { - foreach (var task in tasks) { + foreach (var task in tasks.Where(taskFilter)) { VerifyTask(canVerify, task); } } diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index d4a7b19fdfe..f978623dfa6 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -9,11 +9,10 @@ namespace Microsoft.Dafny; public class ProofDependencyWarnings { - - public static void ReportSuspiciousDependencies(DafnyOptions options, IEnumerable<(IVerificationTask Task, Completed Result)> parts, - ErrorReporter reporter, ProofDependencyManager manager) - { + + 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, @@ -22,7 +21,7 @@ public static void ReportSuspiciousDependencies(DafnyOptions options, IEnumerabl 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 = diff --git a/Source/DafnyDriver/CliCanVerifyResults.cs b/Source/DafnyDriver/CliCanVerifyResults.cs index 069e18781b1..1d0c19dadc2 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<(IVerificationTask Task, Completed Result)> CompletedParts = new(); public readonly ConcurrentBag Tasks = new(); - - public CliCanVerifyResults() { - } } \ No newline at end of file diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 067a6b10133..a2fef76cbcb 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -131,7 +131,7 @@ public async Task VerifyAllAndPrintSummary() { 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); } @@ -191,24 +191,35 @@ public async Task VerifyAllAndPrintSummary() { var canVerifies = resolution.CanVerifies?.DistinctBy(v => v.Tok).ToList(); if (canVerifies != null) { - canVerifies = FilterCanVerifies(canVerifies); + canVerifies = FilterCanVerifies(canVerifies, out var line); 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 { await results.Finished.Task; - foreach (var (task, completed) in results.CompletedParts.OrderBy(t => t.Task.Split.Token)) { - Compilation.ReportDiagnosticsInResult(options, task, completed.Result, Compilation.Reporter); + + // 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, + ProofDependencyWarnings.ReportSuspiciousDependencies(options, parts, resolution.ResolvedProgram.Reporter, resolution.ResolvedProgram.ProofDependencyManager); } catch (ProverException e) { @@ -229,9 +240,14 @@ public async Task VerifyAllAndPrintSummary() { } } - 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; } @@ -239,17 +255,20 @@ private List FilterCanVerifies(List canVerifies) { 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(); } } \ No newline at end of file diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index 03f91779381..1abe6250976 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -21,7 +21,7 @@ public record IdeVerificationTaskState(Range Range, PublishedVerificationStatus IReadOnlyList Diagnostics, bool HitErrorLimit, IVerificationTask Task, IVerificationStatus RawStatus); public enum VerificationPreparationState { NotStarted, InProgress, Done } -public record IdeCanVerifyState(VerificationPreparationState PreparationProgress, +public record IdeCanVerifyState(VerificationPreparationState PreparationProgress, ImmutableDictionary VerificationTasks, IReadOnlyList Diagnostics); @@ -333,7 +333,7 @@ private static IdeCanVerifyState MergeResults(IEnumerable res return results.Aggregate((a, b) => new IdeCanVerifyState( MergeStates(a.PreparationProgress, b.PreparationProgress), a.VerificationTasks.ToImmutableDictionary().Merge(b.VerificationTasks, - (aView, bView) => aView /* Merge should not occur */), + (aView, bView) => aView /* Merge should not occur */), a.Diagnostics.Concat(b.Diagnostics))); } @@ -474,7 +474,7 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie // WarnContradictoryAssumptions should be executable based on a single assertion batch. // WarnRedundantAssumptions is more like find references. It needs all the batches under in a verification scope. // If we're saying that WarnRedundantAssumptions is critical, than verifying single assertions is crap. - + // if (boogieUpdate.BoogieStatus is Completed completed) { // var errorReporter = new ObservableErrorReporter(options, uri); // List verificationCoverageDiagnostics = new(); @@ -498,7 +498,7 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie hitErrorLimit, boogieUpdate.VerificationTask, rawStatus); var newTaskStates = previousVerificationResult.VerificationTasks.SetItem(name, taskState); if (newTaskStates.Values.All(s => s.Status >= PublishedVerificationStatus.Error)) { - + var errorReporter = new ObservableErrorReporter(options, uri); List verificationCoverageDiagnostics = new(); errorReporter.Updates.Subscribe(d => verificationCoverageDiagnostics.Add(d.Diagnostic)); @@ -506,10 +506,10 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie ProofDependencyWarnings.ReportSuspiciousDependencies(options, newTaskStates.Values.Select(s => (s.Task, (Completed)s.RawStatus)), errorReporter, boogieUpdate.ProofDependencyManager); - + newCanVerifyDiagnostics = previousVerificationResult.Diagnostics.Concat(verificationCoverageDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); } - + return previousState with { Counterexamples = counterExamples, CanVerifyStates = previousState.CanVerifyStates.SetItem(uri, diff --git a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs index cd82932f64a..d896b99bede 100644 --- a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs +++ b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs @@ -112,7 +112,7 @@ 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(); - var minMaxRunning = new [] { PublishedVerificationStatus.Running, min }.Max(); + var minMaxRunning = new[] { PublishedVerificationStatus.Running, min }.Max(); return max >= PublishedVerificationStatus.Error ? minMaxRunning : max; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy index 015d2554cbc..3976ebe4b3b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy @@ -1,10 +1,11 @@ // 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='filter.dfy:15' %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: ! %verify --isolate-assertions --filter-position='filter.dfy:15' %s >> %t +// RUN: %verify --filter-position='src/source1.dfy:1' %S/Inputs/dfyconfig.toml >> %t +// RUN: %verify --isolate-assertions --filter-position='filter.dfy:16' %s >> %t +// RUN: ! %verify --isolate-assertions --filter-position='filter.dfy:17' %s >> %t // RUN: %diff "%s.expect" "%t" method Succeeds() @@ -14,4 +15,4 @@ method Succeeds() method Fails() ensures false { assert false; -} +} \ 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 e7fc9735c1b..7662fe88e32 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect @@ -2,12 +2,10 @@ Dafny program verifier finished with 0 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 +filter.dfy(17,9): 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 +filter.dfy(17,9): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error source1.dfy(6,16): Error: a postcondition could not be proved on this return path @@ -16,3 +14,8 @@ source1.dfy(6,10): Related location: this is the postcondition that could not be Dafny program verifier finished with 0 verified, 1 error Dafny program verifier finished with 1 verified, 0 errors + +Dafny program verifier finished with 1 verified, 0 errors +filter.dfy(17,9): Error: assertion might not hold + +Dafny program verifier finished with 0 verified, 1 error From cfe91fdba61fcd5f2901be8cb97af6845f3f3879 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 1 Feb 2024 14:25:09 +0100 Subject: [PATCH 11/40] Fixes --- Source/DafnyCore/Pipeline/Compilation.cs | 10 +-- Source/DafnyDriver/CliCompilation.cs | 2 +- .../Synchronization/VerificationStatusTest.cs | 2 + ...rIconAndHoverVerificationDetailsManager.cs | 12 ++-- .../DafnyLanguageServer/Workspace/IdeState.cs | 64 ++++++------------- 5 files changed, 34 insertions(+), 56 deletions(-) diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index 3b5211add5c..1b23c3c00d0 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -237,13 +237,13 @@ private async Task ResolveAsync() { } } - public static string GetTaskName(IVerificationTask split) { - var dafnyToken = BoogieGenerator.ToDafnyToken(false, split.Token); - var prefix = dafnyToken.line + "," + dafnyToken.col; + public static string GetTaskName(IVerificationTask task) { + var dafnyToken = BoogieGenerator.ToDafnyToken(false, task.Token); + var prefix = task.ScopeId + dafnyToken.line + "," + dafnyToken.col; // 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 (split.ScopeToken is RefinementToken refinementToken) { + if (task.ScopeToken is RefinementToken refinementToken) { prefix += "." + refinementToken.InheritingModule.Name; } @@ -498,7 +498,7 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, IVerification implementation.GetTimeLimit(options), result.CounterExamples); } - private static VcOutcome GetOutcome(SolverOutcome outcome) { + public static VcOutcome GetOutcome(SolverOutcome outcome) { switch (outcome) { case SolverOutcome.Valid: return VcOutcome.Correct; diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index a2fef76cbcb..c106a4016af 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -150,7 +150,7 @@ public async Task VerifyAllAndPrintSummary() { var canVerifyResult = canVerifyResults[boogieUpdate.CanVerify]; canVerifyResult.CompletedParts.Add((boogieUpdate.VerificationTask, completed)); - // TODO first update this to record resolution of ICanVerify things. + // TODO Different PR, update the completed X output so it looks at ICanVerify things. switch (completed.Result.Outcome) { case SolverOutcome.Valid: case SolverOutcome.Bounded: diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index 21fe1e30c24..5648a76d363 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/Workspace/GutterIconAndHoverVerificationDetailsManager.cs b/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs index 8c3e1e9fbc6..ac934372692 100644 --- a/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs +++ b/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs @@ -245,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, ImplementationRunResult verificationResult) { + public void ReportEndVerifyImplementation(IdeState state, Implementation implementation, + int implementationResourceCount, + VcOutcome implementationOutcome) { var uri = ((IToken)implementation.tok).Uri; var tree = state.VerificationTrees[uri]; @@ -258,9 +260,9 @@ public void ReportEndVerifyImplementation(IdeState state, Implementation impleme } else { lock (LockProcessing) { implementationNode.Stop(); - implementationNode.ResourceCount = verificationResult.ResourceCount; - targetMethodNode.ResourceCount += verificationResult.ResourceCount; - var finalOutcome = verificationResult.VcOutcome switch { + implementationNode.ResourceCount = implementationResourceCount; + targetMethodNode.ResourceCount += implementationResourceCount; + var finalOutcome = implementationOutcome switch { VcOutcome.Correct => GutterVerificationStatus.Verified, _ => GutterVerificationStatus.Error }; @@ -268,7 +270,7 @@ public void ReportEndVerifyImplementation(IdeState state, Implementation impleme implementationNode.StatusVerification = finalOutcome; // Will be only executed by the last instance. if (!targetMethodNode.Children.All(child => child.Finished)) { - targetMethodNode.StatusVerification = verificationResult.VcOutcome switch { + targetMethodNode.StatusVerification = implementationOutcome switch { VcOutcome.Correct => targetMethodNode.StatusVerification, _ => GutterVerificationStatus.Error }; diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index 1abe6250976..877e9cd92e7 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -440,7 +440,6 @@ private IdeState UpdateBoogieException(BoogieException boogieException) { private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, BoogieUpdate boogieUpdate) { var previousState = this; - UpdateGutterIconTrees(boogieUpdate, options, logger); var name = Compilation.GetTaskName(boogieUpdate.VerificationTask); var status = StatusFromBoogieStatus(boogieUpdate.BoogieStatus); @@ -461,6 +460,10 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie } 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 = completed.Result.CounterExamples; hitErrorLimit |= completed.Result.MaxCounterExamples == completed.Result.CounterExamples.Count; var newDiagnostics = @@ -470,34 +473,12 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie $"Completed received for {previousState.Input} and found #{diagnostics.Count} diagnostics."); } - // TODO Come up with a solution - // WarnContradictoryAssumptions should be executable based on a single assertion batch. - // WarnRedundantAssumptions is more like find references. It needs all the batches under in a verification scope. - // If we're saying that WarnRedundantAssumptions is critical, than verifying single assertions is crap. - - // if (boogieUpdate.BoogieStatus is Completed completed) { - // 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.VerificationTask.Implementation.VerboseName, - // boogieUpdate.VerificationTask.Implementation.tok), - // DafnyConsolePrinter.DistillVerificationResult(completed.Result)); - // } - // - // diagnostics = diagnostics.Concat(verificationCoverageDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); - // } - var newCanVerifyDiagnostics = new List(); var taskState = new IdeVerificationTaskState(range, status, diagnostics.ToList(), hitErrorLimit, boogieUpdate.VerificationTask, rawStatus); var newTaskStates = previousVerificationResult.VerificationTasks.SetItem(name, taskState); - if (newTaskStates.Values.All(s => s.Status >= PublishedVerificationStatus.Error)) { + var allTasksAreCompleted = newTaskStates.Values.All(s => s.Status >= PublishedVerificationStatus.Error); + if (allTasksAreCompleted) { var errorReporter = new ObservableErrorReporter(options, uri); List verificationCoverageDiagnostics = new(); @@ -509,7 +490,19 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie newCanVerifyDiagnostics = previousVerificationResult.Diagnostics.Concat(verificationCoverageDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); } - + UpdateGutterIconTrees(boogieUpdate, options, logger); + + // TODO move inside UpdateGutterIconTrees ? + if (allTasksAreCompleted) { + var results = newTaskStates.Values.Select(t => (t.Task, ((Completed)t.RawStatus).Result)); + foreach (var g in results.GroupBy(r => r.Task.ScopeId)) { + var gutterIconManager = new GutterIconAndHoverVerificationDetailsManager(logger); + var resourceCount = g.Sum(e => e.Result.ResourceCount); + var outcome = g.Select(e => Compilation.GetOutcome(e.Result.Outcome)).Max(); + gutterIconManager.ReportEndVerifyImplementation(this, g.First().Task.Split.Implementation, resourceCount, outcome); + } + } + return previousState with { Counterexamples = counterExamples, CanVerifyStates = previousState.CanVerifyStates.SetItem(uri, @@ -531,25 +524,6 @@ private void UpdateGutterIconTrees(BoogieUpdate update, DafnyOptions options, IL gutterIconManager.ReportAssertionBatchResult(this, new AssertionBatchResult(update.VerificationTask.Split, batchCompleted.Result)); } - - // TODO switch to - // if (update.BoogieStatus is Completed completed) { - // var tokenString = BoogieGenerator.ToDafnyToken(true, update.VerificationTask.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) { - // logger.LogDebug( - // $"Possibly duplicate reporting assertion batch {result.vcNum} as completed in {tokenString}, version {this.Version}"); - // gutterIconManager.ReportAssertionBatchResult(this, - // new AssertionBatchResult(update.VerificationTask.Implementation, result)); - // } - // - // gutterIconManager.ReportEndVerifyImplementation(this, update.VerificationTask.Implementation, verificationResult); - // } } private static PublishedVerificationStatus StatusFromBoogieStatus(IVerificationStatus verificationStatus) { From 775adbb061c8a4909a45878e72fafd50ec81989d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 1 Feb 2024 16:38:28 +0100 Subject: [PATCH 12/40] Update expect files --- Source/DafnyDriver/CliCompilation.cs | 1 - .../TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect | 2 +- .../LitTest/concurrency/09-CounterNoStateMachine.dfy.expect | 2 +- .../LitTest/concurrency/10-SequenceInvariant.dfy.expect | 2 +- .../LitTest/concurrency/12-MutexLifetime-short.dfy.expect | 2 +- .../TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect | 2 +- .../TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect | 2 +- .../TestFiles/LitTests/LitTest/dafny4/ACL2-extractor.dfy.expect | 2 +- .../LitTest/dafny4/SoftwareFoundations-Basics.dfy.expect | 2 +- .../LitTests/LitTest/git-issues/git-issue-1252.dfy.expect | 2 +- .../LitTests/LitTest/git-issues/git-issue-3855.dfy.expect | 2 +- .../TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy.expect | 2 +- .../LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect | 2 +- .../TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect | 2 +- 14 files changed, 13 insertions(+), 14 deletions(-) diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index c106a4016af..ef111707ebd 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -150,7 +150,6 @@ public async Task VerifyAllAndPrintSummary() { var canVerifyResult = canVerifyResults[boogieUpdate.CanVerify]; canVerifyResult.CompletedParts.Add((boogieUpdate.VerificationTask, completed)); - // TODO Different PR, update the completed X output so it looks at ICanVerify things. switch (completed.Result.Outcome) { case SolverOutcome.Valid: case SolverOutcome.Bounded: 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 94a42af27f3..ef71487de53 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 49c99f8b11b..4fd36a1d403 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 bd57f1956c5..f3e2b391bdf 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 5762072e289..c2bb304608c 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 04f996a5072..0230b318658 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/dafny1/MoreInduction.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect index 89ed8e1ed3c..638376bfd6c 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 e43bbd93c5f..023b0990012 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 79eca64e20a..35e54b59f6f 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 cfe97d5394e..7d00bd734ae 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 3de59550cba..5ff8e24f08a 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 9b96db8633f..caca1722291 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/vstte2012/BreadthFirstSearch.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect index 66ffe3665d5..5436a7e7dc4 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 ccc01c35f48..42324885fd1 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 From 7a1c3e64ad56c9a6f465f5940c04ac4e6defd98e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 12:39:12 +0100 Subject: [PATCH 13/40] Gutter icon fixes --- Source/DafnyCore/Pipeline/IProgramVerifier.cs | 2 +- ...pleLinearVerificationGutterStatusTester.cs | 160 +++++++++--------- ...rIconAndHoverVerificationDetailsManager.cs | 4 +- .../DafnyLanguageServer/Workspace/IdeState.cs | 50 +++--- 4 files changed, 111 insertions(+), 105 deletions(-) diff --git a/Source/DafnyCore/Pipeline/IProgramVerifier.cs b/Source/DafnyCore/Pipeline/IProgramVerifier.cs index d52cc8e8f3d..7cdc359c6ff 100644 --- a/Source/DafnyCore/Pipeline/IProgramVerifier.cs +++ b/Source/DafnyCore/Pipeline/IProgramVerifier.cs @@ -6,7 +6,7 @@ using VC; namespace Microsoft.Dafny { - public record AssertionBatchResult(ManualSplit Split, VerificationRunResult Result); + public record AssertionBatchResult(Implementation Implementation, VerificationRunResult Result); public record ProgramVerificationTasks(IReadOnlyList Tasks); diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs index 5f54eeb8e2e..915426559b5 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs @@ -101,23 +101,23 @@ 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() { @@ -136,26 +136,26 @@ await VerifyTrace(@" [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 +178,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/Workspace/GutterIconAndHoverVerificationDetailsManager.cs b/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs index ac934372692..84bf87b66b7 100644 --- a/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs +++ b/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs @@ -300,11 +300,11 @@ private void NoMethodNodeAtLogging(VerificationTree tree, string methodName, Ide /// Called when a split is finished to be verified /// public void ReportAssertionBatchResult(IdeState ideState, AssertionBatchResult batchResult) { - var uri = ((IToken)batchResult.Split.Token).Uri; + var uri = ((IToken)batchResult.Implementation.tok).Uri; var tree = ideState.VerificationTrees[uri]; lock (LockProcessing) { - var implementation = batchResult.Split.Implementation; + var implementation = batchResult.Implementation; var result = batchResult.Result; // While there is no error, just add successful nodes. var targetMethodNode = GetTargetMethodTree(tree, implementation, out var implementationNode); diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index 877e9cd92e7..c87204030b5 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -463,7 +463,7 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie // 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 = completed.Result.CounterExamples; hitErrorLimit |= completed.Result.MaxCounterExamples == completed.Result.CounterExamples.Count; var newDiagnostics = @@ -477,7 +477,9 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie var taskState = new IdeVerificationTaskState(range, status, diagnostics.ToList(), hitErrorLimit, boogieUpdate.VerificationTask, rawStatus); var newTaskStates = previousVerificationResult.VerificationTasks.SetItem(name, taskState); - var allTasksAreCompleted = newTaskStates.Values.All(s => s.Status >= PublishedVerificationStatus.Error); + + 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); @@ -485,24 +487,14 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie errorReporter.Updates.Subscribe(d => verificationCoverageDiagnostics.Add(d.Diagnostic)); ProofDependencyWarnings.ReportSuspiciousDependencies(options, - newTaskStates.Values.Select(s => (s.Task, (Completed)s.RawStatus)), + scopeGroup.Select(s => (s.Task, (Completed)s.RawStatus)), errorReporter, boogieUpdate.ProofDependencyManager); newCanVerifyDiagnostics = previousVerificationResult.Diagnostics.Concat(verificationCoverageDiagnostics.Select(d => d.ToLspDiagnostic())).ToList(); } - UpdateGutterIconTrees(boogieUpdate, options, logger); - - // TODO move inside UpdateGutterIconTrees ? - if (allTasksAreCompleted) { - var results = newTaskStates.Values.Select(t => (t.Task, ((Completed)t.RawStatus).Result)); - foreach (var g in results.GroupBy(r => r.Task.ScopeId)) { - var gutterIconManager = new GutterIconAndHoverVerificationDetailsManager(logger); - var resourceCount = g.Sum(e => e.Result.ResourceCount); - var outcome = g.Select(e => Compilation.GetOutcome(e.Result.Outcome)).Max(); - gutterIconManager.ReportEndVerifyImplementation(this, g.First().Task.Split.Implementation, resourceCount, outcome); - } - } - + + UpdateGutterIconTrees(logger, boogieUpdate, scopeGroup); + return previousState with { Counterexamples = counterExamples, CanVerifyStates = previousState.CanVerifyStates.SetItem(uri, @@ -513,16 +505,30 @@ private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, Boogie }; } - 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) { - // TODO remove duplication? - gutterIconManager.ReportVerifyImplementationRunning(this, update.VerificationTask.Split.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 Completed batchCompleted) { + if (boogieUpdate.BoogieStatus is Completed completed) { gutterIconManager.ReportAssertionBatchResult(this, - new AssertionBatchResult(update.VerificationTask.Split, batchCompleted.Result)); + new AssertionBatchResult(boogieUpdate.VerificationTask.Split.Implementation, completed.Result)); + } + + 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}, version {this.Version}"); + gutterIconManager.ReportAssertionBatchResult(this, + new AssertionBatchResult(boogieUpdate.VerificationTask.Split.Implementation, result)); + } + + 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); } } From 8b0f648777a6f8938374b7ebbd43843ba3721ea7 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 13:55:09 +0100 Subject: [PATCH 14/40] Fix gutter test --- Source/DafnyCore/AST/Tokens.cs | 11 ++++++ ...pleLinearVerificationGutterStatusTester.cs | 21 +++++----- .../Language/DafnyProgramVerifier.cs | 13 ++++++- .../DafnyLanguageServer/Workspace/IdeState.cs | 38 +++++++++---------- 4 files changed, 54 insertions(+), 29 deletions(-) diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs index 96810cae6b7..3e9eefa37dd 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/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs index 915426559b5..2ad64631be1 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) @@ -122,15 +125,15 @@ await VerifyTrace(@" [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] diff --git a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs index 71359c62e60..ee9f30b1b70 100644 --- a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs +++ b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs @@ -61,7 +61,18 @@ public async Task> GetVerificationTasksAsync(Ex ExecutionEngine.PrintBplFile(engine.Options, fileName, boogieProgram, false, false, engine.Options.PrettyPrint); } - return engine.GetVerificationTasks(boogieProgram); + var tasksFromBoogie = engine.GetVerificationTasks(boogieProgram); + + // Ordering is required to let gutter icon tests behave more deterministically + // In situations where there are multiple valid orders of execution + // In particular, GitIssue3821GutterIgnoredProblem fails without this + // We can consider turning off that test so we do not need this hack + // Better would be to compute gutter icons on the client + var ordered = tasksFromBoogie. + OrderBy(s => s.ScopeToken). + ThenByDescending(s => s.ScopeId). + ThenBy(s => s.Token).ToList(); + return ordered; } finally { mutex.Release(); diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index c87204030b5..f564c9aee4c 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -171,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). @@ -221,7 +221,7 @@ 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; @@ -241,7 +241,7 @@ private IdeState UpdateScheduledVerification(ScheduledVerification scheduledVeri }; } - private IdeState UpdateNewDiagnostic(NewDiagnostic newDiagnostic) { + private IdeState HandleNewDiagnostic(NewDiagnostic newDiagnostic) { var previousState = this; // Until resolution is finished, keep showing the old diagnostics. @@ -256,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 = @@ -273,7 +273,7 @@ private IdeState UpdateInternalCompilationException(InternalCompilationException }; } - private IdeState UpdateFinishedResolution(DafnyOptions options, + private IdeState HandleFinishedResolution(DafnyOptions options, ILogger logger, TelemetryPublisherBase telemetryPublisher, FinishedResolution finishedResolution) { @@ -358,7 +358,7 @@ private static IdeCanVerifyState MergeVerifiable(IdeState previousState, ICanVer }), 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) { @@ -382,7 +382,7 @@ 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.Split.Implementation).Distinct(); var gutterIconManager = new GutterIconAndHoverVerificationDetailsManager(logger); @@ -408,7 +408,7 @@ private IdeState UpdateCanVerifyPartsUpdated(ILogger logger, CanVerifyPartsIdent }; } - private IdeState UpdateBoogieException(BoogieException boogieException) { + private IdeState HandleBoogieException(BoogieException boogieException) { var previousState = this; var name = Compilation.GetTaskName(boogieException.Task); @@ -438,7 +438,7 @@ private IdeState UpdateBoogieException(BoogieException boogieException) { }; } - private IdeState UpdateBoogieUpdate(DafnyOptions options, ILogger logger, BoogieUpdate boogieUpdate) { + private IdeState HandleBoogieUpdate(DafnyOptions options, ILogger logger, BoogieUpdate boogieUpdate) { var previousState = this; var name = Compilation.GetTaskName(boogieUpdate.VerificationTask); @@ -521,7 +521,7 @@ private void UpdateGutterIconTrees(ILogger logger, BoogieUpdate boogieUpdate, IR foreach (var result in results) { logger.LogDebug( - $"Possibly duplicate reporting assertion batch {result.vcNum}, version {this.Version}"); + $"Possibly duplicate reporting assertion batch {result.vcNum}, version {Version}"); gutterIconManager.ReportAssertionBatchResult(this, new AssertionBatchResult(boogieUpdate.VerificationTask.Split.Implementation, result)); } From 31da8edd20152eb4cc223811eba70973f91c2fb8 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 13:55:33 +0100 Subject: [PATCH 15/40] Ran formatter --- Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs index ee9f30b1b70..30db8dfe02b 100644 --- a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs +++ b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs @@ -62,7 +62,7 @@ public async Task> GetVerificationTasksAsync(Ex } var tasksFromBoogie = engine.GetVerificationTasks(boogieProgram); - + // Ordering is required to let gutter icon tests behave more deterministically // In situations where there are multiple valid orders of execution // In particular, GitIssue3821GutterIgnoredProblem fails without this From cef25e0f1cb5ae8c2962bd475e9551c3cf36775b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 14:05:30 +0100 Subject: [PATCH 16/40] Fix bug --- Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs index d896b99bede..6278ed25416 100644 --- a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs +++ b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs @@ -112,7 +112,9 @@ 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(); - var minMaxRunning = new[] { PublishedVerificationStatus.Running, min }.Max(); + + // If one task is completed, we do not allowed queued as a status. + var minMaxRunning = min == PublishedVerificationStatus.Queued ? PublishedVerificationStatus.Running : min; return max >= PublishedVerificationStatus.Error ? minMaxRunning : max; } From 634921e1e5f86106d99079ca27e64a80d116c506 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 14:46:13 +0100 Subject: [PATCH 17/40] Use SplitIndex --- Source/DafnyCore/Pipeline/Compilation.cs | 3 +-- boogie | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index 1b23c3c00d0..77c7f4d87a3 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -238,8 +238,7 @@ private async Task ResolveAsync() { } public static string GetTaskName(IVerificationTask task) { - var dafnyToken = BoogieGenerator.ToDafnyToken(false, task.Token); - var prefix = task.ScopeId + dafnyToken.line + "," + dafnyToken.col; + 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. diff --git a/boogie b/boogie index a1871efd793..1f60bda9875 160000 --- a/boogie +++ b/boogie @@ -1 +1 @@ -Subproject commit a1871efd79340aa02b3f66d6d7b9bceaacd08433 +Subproject commit 1f60bda98754e0780c85433f50208ddf7bb7eda1 From 4337c01e4daaae469953fd66d16406fc2519ac8f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 15:04:11 +0100 Subject: [PATCH 18/40] Fix status bug and fix tests --- ...chedLinearVerificationGutterStatusTester.cs | 18 +++++++++--------- ...rentLinearVerificationGutterStatusTester.cs | 16 ++++++++-------- .../Workspace/NotificationPublisher.cs | 17 +++++++++++++---- .../Workspace/ProjectManager.cs | 6 +++--- 4 files changed, 33 insertions(+), 24 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs index 5a083df51ed..52338f307c7 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 28eb9969f58..d6430856cb1 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/Workspace/NotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs index 6278ed25416..544f909af3c 100644 --- a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs +++ b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs @@ -102,7 +102,9 @@ private static NamedVerifiableStatus GetNamedVerifiableStatuses(Range canVerify, VerificationPreparationState.NotStarted => PublishedVerificationStatus.Stale, VerificationPreparationState.InProgress => PublishedVerificationStatus.Queued, VerificationPreparationState.Done => - result.VerificationTasks.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() }; @@ -113,9 +115,16 @@ public static PublishedVerificationStatus Combine(PublishedVerificationStatus fi var max = new[] { first, second }.Max(); var min = new[] { first, second }.Min(); - // If one task is completed, we do not allowed queued as a status. - var minMaxRunning = min == PublishedVerificationStatus.Queued ? PublishedVerificationStatus.Running : min; - return max >= PublishedVerificationStatus.Error ? minMaxRunning : 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 fbd295f16e8..d3a9940062c 100644 --- a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs +++ b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs @@ -297,9 +297,9 @@ 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(); From 0ee78f54ba262309829a837953984f590bbe2eea Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 15:12:53 +0100 Subject: [PATCH 19/40] Fix counter example bug --- Source/DafnyLanguageServer/Workspace/IdeState.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index f564c9aee4c..b7e3237ca8a 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -464,7 +464,7 @@ private IdeState HandleBoogieUpdate(DafnyOptions options, ILogger logger, Boogie // 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 = completed.Result.CounterExamples; + counterExamples = counterExamples.Concat(completed.Result.CounterExamples); hitErrorLimit |= completed.Result.MaxCounterExamples == completed.Result.CounterExamples.Count; var newDiagnostics = Compilation.GetDiagnosticsFromResult(options, previousState.Uri, boogieUpdate.VerificationTask, completed.Result); From 90885ea644eae29e4fe040eaaf3c4da4b5623f41 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 15:14:19 +0100 Subject: [PATCH 20/40] Trigger CI From c12e426f8018097523b3b41444187846f9a22272 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 15:17:20 +0100 Subject: [PATCH 21/40] Refactoring --- Source/DafnyCore/Pipeline/Compilation.cs | 12 ------------ .../DafnyLanguageServer/Workspace/ProjectManager.cs | 5 +++-- 2 files changed, 3 insertions(+), 14 deletions(-) diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index 77c7f4d87a3..4f0df9761be 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -249,18 +249,6 @@ public static string GetTaskName(IVerificationTask task) { return prefix; } - public static string GetImplementationName(Implementation implementation) { - var prefix = implementation.Name.Split(BoogieGenerator.NameSeparator)[0]; - - // 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) { - prefix += "." + refinementToken.InheritingModule.Name; - } - - return prefix; - } - private int runningVerificationJobs; // When verifying a symbol, a ticket must be acquired before the SMT part of verification may start. diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs index d3a9940062c..f96d5b2cfb3 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) + var orderedVerifiables = canVerifies + .OrderByDescending(GetPriorityAttribute) .ThenBy(t => implementationOrder.GetOrDefault(t.Tok.GetFilePosition(), () => int.MaxValue)) - .ThenBy(TopToBottomPriority).ToList(); ; + .ThenBy(TopToBottomPriority).ToList(); logger.LogDebug($"Ordered verifiables: {string.Join(", ", orderedVerifiables.Select(v => v.NameToken.val))}"); var orderedVerifiableLocations = orderedVerifiables.Select(v => v.NameToken.GetFilePosition()).ToList(); From a3e9277fd3886d0ce002ef3935e4a203838bdaf9 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 15:56:48 +0100 Subject: [PATCH 22/40] Update expect file --- .../LitTests/LitTest/dafny0/Termination.dfy.refresh.expect | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 189a267e262..7cc2944f0b5 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 From a65dda066b94e9c3d6f97a79a6abb1c34862e966 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 19:17:12 +0100 Subject: [PATCH 23/40] Updato to latest Boogie --- Source/Dafny.sln | 38 ------------------- Source/DafnyCore/DafnyConsolePrinter.cs | 2 +- Source/DafnyCore/DafnyCore.csproj | 12 +----- .../Various/SlowVerifier.cs | 1 - ...rIconAndHoverVerificationDetailsManager.cs | 6 +-- .../DafnyLanguageServer/Workspace/IdeState.cs | 2 +- boogie | 1 - 7 files changed, 6 insertions(+), 56 deletions(-) delete mode 160000 boogie diff --git a/Source/Dafny.sln b/Source/Dafny.sln index fc8e8b1fa49..23297b185ed 100644 --- a/Source/Dafny.sln +++ b/Source/Dafny.sln @@ -43,32 +43,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}" EndProject -Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Boogie", "Boogie", "{60332269-9C5D-465E-8582-01F9B738BD90}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BaseTypes", "..\boogie\Source\BaseTypes\BaseTypes.csproj", "{68721962-0D91-4355-BC94-BE1CCBD30E47}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbstractInterpretation", "..\boogie\Source\AbstractInterpretation\AbstractInterpretation.csproj", "{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj", "{09662044-5640-4785-92E3-2F7CDBA4DDB2}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "..\boogie\Source\Concurrency\Concurrency.csproj", "{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "..\boogie\Source\Core\Core.csproj", "{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj", "{0145DC89-7243-41F8-AB3E-F716F04E9BFF}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "..\boogie\Source\Graph\Graph.csproj", "{05DE24BB-D639-40C4-894F-701652F51559}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "..\boogie\Source\Houdini\Houdini.csproj", "{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "..\boogie\Source\Model\Model.csproj", "{D97C23B6-FB4A-4450-930E-58EC83D308A0}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "..\boogie\Source\Provers\SMTLib\SMTLib.csproj", "{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "..\boogie\Source\VCExpr\VCExpr.csproj", "{E760E37E-0257-4C96-89C4-722F85BABDBB}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "..\boogie\Source\VCGeneration\VCGeneration.csproj", "{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}" -EndProject EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution @@ -164,17 +138,5 @@ Global SolutionGuid = {280F572B-D27A-4613-998F-00B6FFE01187} EndGlobalSection GlobalSection(NestedProjects) = preSolution - {68721962-0D91-4355-BC94-BE1CCBD30E47} = {60332269-9C5D-465E-8582-01F9B738BD90} - {2A6B36F4-9F15-459A-8EDB-5BAEED98FE17} = {60332269-9C5D-465E-8582-01F9B738BD90} - {09662044-5640-4785-92E3-2F7CDBA4DDB2} = {60332269-9C5D-465E-8582-01F9B738BD90} - {DA8A9BA8-9BBA-4C64-9736-FD967517DCA9} = {60332269-9C5D-465E-8582-01F9B738BD90} - {2BF5ECCA-24B2-4A4B-86B6-D0DB17331109} = {60332269-9C5D-465E-8582-01F9B738BD90} - {0145DC89-7243-41F8-AB3E-F716F04E9BFF} = {60332269-9C5D-465E-8582-01F9B738BD90} - {05DE24BB-D639-40C4-894F-701652F51559} = {60332269-9C5D-465E-8582-01F9B738BD90} - {51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6} = {60332269-9C5D-465E-8582-01F9B738BD90} - {D97C23B6-FB4A-4450-930E-58EC83D308A0} = {60332269-9C5D-465E-8582-01F9B738BD90} - {0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F} = {60332269-9C5D-465E-8582-01F9B738BD90} - {E760E37E-0257-4C96-89C4-722F85BABDBB} = {60332269-9C5D-465E-8582-01F9B738BD90} - {1EE372AA-4FF9-47FB-9C04-18CBF219F6E8} = {60332269-9C5D-465E-8582-01F9B738BD90} EndGlobalSection EndGlobal diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index a2bce350cc3..42d23a92464 100644 --- a/Source/DafnyCore/DafnyConsolePrinter.cs +++ b/Source/DafnyCore/DafnyConsolePrinter.cs @@ -48,7 +48,7 @@ public static VerificationResultLogEntry DistillVerificationResult(Implementatio } private static VCResultLogEntry DistillVCResult(VerificationRunResult r) { - return new VCResultLogEntry(r.vcNum, r.StartTime, r.RunTime, r.Outcome, + 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); } diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 13ed0280f25..ccb550f3063 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -33,17 +33,7 @@ - - - - - - - - - - - + diff --git a/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs b/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs index 9674f8ef705..e1edd559079 100644 --- a/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs +++ b/Source/DafnyLanguageServer.Test/Various/SlowVerifier.cs @@ -46,7 +46,6 @@ public NeverVerifiesImplementationTask(IVerificationTask original) { } public IVerificationStatus CacheStatus => new Stale(); - public ProcessedProgram ProcessedProgram => original.ProcessedProgram; public ManualSplit Split => original.Split; public Boogie.IToken ScopeToken => original.ScopeToken; public string ScopeId => original.ScopeId; diff --git a/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs b/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs index 84bf87b66b7..14f095438d2 100644 --- a/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs +++ b/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs @@ -315,7 +315,7 @@ 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; } @@ -324,7 +324,7 @@ assertNode is AssertionVerificationTree assertionNode var assertionBatchTime = (int)result.RunTime.TotalMilliseconds; var assertionBatchResourceCount = result.ResourceCount; - implementationNode.AddAssertionBatchMetrics(result.vcNum, assertionBatchTime, assertionBatchResourceCount, result.CoveredElements.ToList()); + implementationNode.AddAssertionBatchMetrics(result.VcNum, assertionBatchTime, assertionBatchResourceCount, result.CoveredElements.ToList()); // Attaches the trace void AddChildOutcome(Counterexample? counterexample, AssertCmd assertCmd, IToken token, @@ -352,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) diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index b7e3237ca8a..2a48ed080bc 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -521,7 +521,7 @@ private void UpdateGutterIconTrees(ILogger logger, BoogieUpdate boogieUpdate, IR foreach (var result in results) { logger.LogDebug( - $"Possibly duplicate reporting assertion batch {result.vcNum}, version {Version}"); + $"Possibly duplicate reporting assertion batch {result.VcNum}, version {Version}"); gutterIconManager.ReportAssertionBatchResult(this, new AssertionBatchResult(boogieUpdate.VerificationTask.Split.Implementation, result)); } diff --git a/boogie b/boogie deleted file mode 160000 index 1f60bda9875..00000000000 --- a/boogie +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 1f60bda98754e0780c85433f50208ddf7bb7eda1 From 53b042779ec880866d1b463e21d0f07a9c64b943 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 19:17:49 +0100 Subject: [PATCH 24/40] Remove submodule --- .gitmodules | 3 --- 1 file changed, 3 deletions(-) diff --git a/.gitmodules b/.gitmodules index ff4c52587f4..aa94f844181 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,3 @@ [submodule "Test/libraries"] path = Source/IntegrationTests/TestFiles/LitTests/LitTest/libraries url = https://github.com/dafny-lang/libraries.git -[submodule "boogie"] - path = boogie - url = git@github.com:boogie-org/boogie.git From cb1ddf54f6efe29a2e724384dd97b7b783765faf Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 5 Feb 2024 13:04:13 +0100 Subject: [PATCH 25/40] Add code to help debug problems --- Source/DafnyDriver/CliCompilation.cs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index ef111707ebd..d41005f5153 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -205,7 +205,17 @@ public async Task VerifyAllAndPrintSummary() { foreach (var canVerify in orderedCanVerifies) { var results = canVerifyResults[canVerify]; try { - await results.Finished.Task; + 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. Please report it at .\n"); + continue; + } // We use an intermediate reporter so we can sort the diagnostics from all parts by token var batchReporter = new BatchErrorReporter(options); From 28e5c3b1af1beab2d654260971b6ce08c6e7b4dd Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 5 Feb 2024 13:46:25 +0100 Subject: [PATCH 26/40] Fix missing exception --- Source/DafnyDriver/CliCompilation.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index d41005f5153..417abaea5a4 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -216,6 +216,7 @@ public async Task VerifyAllAndPrintSummary() { "Dafny encountered an internal error. Please report it at .\n"); continue; } + await results.Finished.Task; // We use an intermediate reporter so we can sort the diagnostics from all parts by token var batchReporter = new BatchErrorReporter(options); From 06cfe775f170f167505c9973f86d36df38b68d59 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 5 Feb 2024 13:47:04 +0100 Subject: [PATCH 27/40] Halt earlier: --- Source/DafnyDriver/CliCompilation.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 417abaea5a4..b5ee0ce873d 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -213,8 +213,8 @@ public async Task VerifyAllAndPrintSummary() { await Task.WhenAny(tasks); if (!results.Finished.Task.IsCompleted) { Compilation.Reporter.Error(MessageSource.Verifier, canVerify.Tok, - "Dafny encountered an internal error. Please report it at .\n"); - continue; + "Dafny encountered an internal error during verification. Please report it at .\n"); + break; } await results.Finished.Task; From 1f734dc6c6efdfb465f677be911b3cdef3861b7b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 5 Feb 2024 14:12:39 +0100 Subject: [PATCH 28/40] Add more tests to filter.dfy file --- .../LitTests/LitTest/verification/filter.dfy | 24 ++++++++++++++++--- .../LitTest/verification/filter.dfy.expect | 22 +++++++++++++---- 2 files changed, 38 insertions(+), 8 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy index 3976ebe4b3b..5e1878aef12 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy @@ -1,11 +1,16 @@ // 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:15' %s >> %t +// RUN: %verify --filter-position='filter.dfy:15' %s >> %t // RUN: ! %verify --filter-position='src/source1.dfy:5' %S/Inputs/dfyconfig.toml >> %t // RUN: %verify --filter-position='src/source1.dfy:1' %S/Inputs/dfyconfig.toml >> %t -// RUN: %verify --isolate-assertions --filter-position='filter.dfy:16' %s >> %t -// RUN: ! %verify --isolate-assertions --filter-position='filter.dfy:17' %s >> %t +// RUN: ! %verify --isolate-assertions --filter-position='filter.dfy:20' %s >> %t +// RUN: %verify --isolate-assertions --filter-position='filter.dfy:21' %s >> %t +// RUN: %verify --isolate-assertions --filter-position='filter.dfy:22' %s >> %t +// RUN: ! %verify --isolate-assertions --filter-position='filter.dfy:23' %s >> %t +// RUN: %verify --isolate-assertions --filter-position='filter.dfy:24' %s >> %t +// RUN: ! %verify --isolate-assertions --filter-position='filter.dfy:31' %s >> %t +// RUN: %verify --isolate-assertions --filter-position='filter.dfy:35' %s >> %t // RUN: %diff "%s.expect" "%t" method Succeeds() @@ -14,5 +19,18 @@ method Succeeds() method Fails() ensures false { + assert false by { + assert false; + assert false; + } +} + +method Loop() { + var b := true; + while(b) + invariant false + { + b := false; + } assert false; } \ 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 7662fe88e32..d8576b060f7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect @@ -2,20 +2,32 @@ Dafny program verifier finished with 0 verified, 0 errors Dafny program verifier finished with 0 verified, 0 errors -filter.dfy(17,9): Error: assertion might not hold +filter.dfy(23,11): Error: assertion might not hold +filter.dfy(31,14): Error: loop invariant violation -Dafny program verifier finished with 1 verified, 1 error -filter.dfy(17,9): Error: assertion might not hold +Dafny program verifier finished with 1 verified, 2 errors -Dafny program verifier finished with 0 verified, 1 error +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 verified, 1 error +Dafny program verifier finished with 1 verified, 0 errors +filter.dfy(23,11): Error: assertion might not hold + +Dafny program verifier finished with 4 verified, 1 error + Dafny program verifier finished with 1 verified, 0 errors Dafny program verifier finished with 1 verified, 0 errors -filter.dfy(17,9): Error: assertion might not hold +filter.dfy(23,11): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error + +Dafny program verifier finished with 1 verified, 0 errors +filter.dfy(31,14): Error: loop invariant violation + +Dafny program verifier finished with 0 verified, 1 error + +Dafny program verifier finished with 1 verified, 0 errors From 78b43329e53ce87b6a928cd5b6108d43d0d4d9ab Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 5 Feb 2024 14:29:01 +0100 Subject: [PATCH 29/40] Improve verification summary when using a line filter --- Source/DafnyDriver/CliCompilation.cs | 79 ++++++++++++++++--- .../verification/Inputs/dfyconfig.toml | 1 + .../verification/Inputs/single-file.dfy | 21 +++++ .../LitTests/LitTest/verification/filter.dfy | 46 +++-------- .../LitTest/verification/filter.dfy.expect | 39 ++++----- 5 files changed, 123 insertions(+), 63 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/single-file.dfy diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index b5ee0ce873d..5f9517f050f 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -14,6 +14,7 @@ using Microsoft.Dafny.LanguageServer.Workspace; using Microsoft.Extensions.Logging; using Token = Microsoft.Dafny.Token; +using Util = Microsoft.Dafny.Util; namespace DafnyDriver.Commands; @@ -124,7 +125,7 @@ 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 => { @@ -153,22 +154,26 @@ public async Task VerifyAllAndPrintSummary() { switch (completed.Result.Outcome) { case SolverOutcome.Valid: case SolverOutcome.Bounded: - Interlocked.Increment(ref statSum.VerifiedCount); + Interlocked.Increment(ref statistics.VerifiedSymbols); + Interlocked.Add(ref statistics.VerifiedAssertions, completed.Result.Asserts.Count); break; case SolverOutcome.Invalid: - Interlocked.Add(ref statSum.ErrorCount, completed.Result.CounterExamples.Count); + 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 SolverOutcome.TimeOut: - Interlocked.Increment(ref statSum.TimeoutCount); + Interlocked.Increment(ref statistics.TimeoutCount); break; case SolverOutcome.OutOfMemory: - Interlocked.Increment(ref statSum.OutOfMemoryCount); + Interlocked.Increment(ref statistics.OutOfMemoryCount); break; case SolverOutcome.OutOfResource: - Interlocked.Increment(ref statSum.OutOfResourceCount); + Interlocked.Increment(ref statistics.OutOfResourceCount); break; case SolverOutcome.Undetermined: - Interlocked.Increment(ref statSum.InconclusiveCount); + Interlocked.Increment(ref statistics.InconclusiveCount); break; default: throw new ArgumentOutOfRangeException(); @@ -189,8 +194,10 @@ public async Task VerifyAllAndPrintSummary() { var canVerifies = resolution.CanVerifies?.DistinctBy(v => v.Tok).ToList(); + var verifiedAssertions = false; if (canVerifies != null) { canVerifies = FilterCanVerifies(canVerifies, out var line); + verifiedAssertions = line != null; var orderedCanVerifies = canVerifies.OrderBy(v => v.Tok.pos).ToList(); foreach (var canVerify in orderedCanVerifies) { @@ -233,17 +240,17 @@ public async Task VerifyAllAndPrintSummary() { 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. @@ -281,4 +288,56 @@ private List FilterCanVerifies(List canVerifies, out int return fileFiltered.Where(c => 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/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/dfyconfig.toml b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/dfyconfig.toml index e69de29bb2d..bed17481d41 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 00000000000..c35a66d605d --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/single-file.dfy @@ -0,0 +1,21 @@ +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; +} \ 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 5e1878aef12..41c3d242a35 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy @@ -1,36 +1,14 @@ -// 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:15' %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:1' %S/Inputs/dfyconfig.toml >> %t -// RUN: ! %verify --isolate-assertions --filter-position='filter.dfy:20' %s >> %t -// RUN: %verify --isolate-assertions --filter-position='filter.dfy:21' %s >> %t -// RUN: %verify --isolate-assertions --filter-position='filter.dfy:22' %s >> %t -// RUN: ! %verify --isolate-assertions --filter-position='filter.dfy:23' %s >> %t -// RUN: %verify --isolate-assertions --filter-position='filter.dfy:24' %s >> %t -// RUN: ! %verify --isolate-assertions --filter-position='filter.dfy:31' %s >> %t -// RUN: %verify --isolate-assertions --filter-position='filter.dfy:35' %s >> %t -// RUN: %diff "%s.expect" "%t" - -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; -} \ No newline at end of file +// 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='e.dfy:20' %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 d8576b060f7..96ac88dd566 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect @@ -1,33 +1,34 @@ +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 verified, 0 errors -filter.dfy(23,11): Error: assertion might not hold -filter.dfy(31,14): Error: loop invariant violation +Dafny program verifier finished with 0 assertions verified, 1 error -Dafny program verifier finished with 1 verified, 2 errors +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 -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 1 verified, 2 errors -Dafny program verifier finished with 0 verified, 1 error +Dafny program verifier finished with 0 assertions verified, 0 errors -Dafny program verifier finished with 1 verified, 0 errors -filter.dfy(23,11): Error: assertion might not hold +Dafny program verifier finished with 0 verified, 0 errors +single-file.dfy(8,11): Error: assertion might not hold -Dafny program verifier finished with 4 verified, 1 error +Dafny program verifier finished with 3 assertions verified, 1 error -Dafny program verifier finished with 1 verified, 0 errors +Dafny program verifier finished with 1 assertions verified, 0 errors -Dafny program verifier finished with 1 verified, 0 errors -filter.dfy(23,11): Error: assertion might not hold +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 verified, 1 error +Dafny program verifier finished with 0 assertions verified, 1 error -Dafny program verifier finished with 1 verified, 0 errors -filter.dfy(31,14): Error: loop invariant violation +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 verified, 1 error +Dafny program verifier finished with 0 assertions verified, 1 error -Dafny program verifier finished with 1 verified, 0 errors +Dafny program verifier finished with 1 assertions verified, 0 errors From 797567e69e0156e610a979c9713ecd83b0e7262c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 5 Feb 2024 14:32:00 +0100 Subject: [PATCH 30/40] Fix customBoogie.patch --- customBoogie.patch | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/customBoogie.patch b/customBoogie.patch index 822a4e0f4f7..0760ea90e91 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + + + From b7bdfab15ee61248ddfd7c9038714a8f6cb2c06b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 5 Feb 2024 17:09:39 +0100 Subject: [PATCH 31/40] Add a timeout on the queue task --- Source/DafnyDriver/CliCompilation.cs | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 5f9517f050f..4b6513b8b84 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -206,7 +206,20 @@ public async Task VerifyAllAndPrintSummary() { if (line != null) { results.TaskFilter = t => KeepVerificationTask(t, line.Value); } - await Compilation.VerifyCanVerify(canVerify, results.TaskFilter); + + var queueVerificationTask = Compilation.VerifyCanVerify(canVerify, results.TaskFilter); + var tasks = new List() { queueVerificationTask }; + var timeLimitSeconds = TimeSpan.FromSeconds(options.Get(BoogieOptionBag.VerificationTimeLimit)); + if (timeLimitSeconds.Seconds != 0) { + tasks.Add(Task.Delay(timeLimitSeconds)); + } + await Task.WhenAny(tasks); + if (!queueVerificationTask.IsCompleted) { + Compilation.Reporter.Error(MessageSource.Verifier, canVerify.Tok, + "Dafny encountered an internal error during verification. Please report it at .\n"); + break; + } + await queueVerificationTask; } foreach (var canVerify in orderedCanVerifies) { From b65691a5f04b086f4ef7072033905bb75accc69d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 6 Feb 2024 10:32:15 +0100 Subject: [PATCH 32/40] Fix path --- .../LitTests/LitTest/verification/filter.dfy | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy index 41c3d242a35..656775d6d7a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy @@ -1,14 +1,14 @@ // 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: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='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='e.dfy:20' %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='e.dfy:20' %S/Inputs/single-file.dfy >> %t // RUN: %diff "%s.expect" "%t" \ No newline at end of file From c06af7ad8122068b661e0f3ff50da8dd9793f57d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 6 Feb 2024 10:42:50 +0100 Subject: [PATCH 33/40] Remove obsolete code --- .../Language/DafnyProgramVerifier.cs | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) diff --git a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs index 30db8dfe02b..71359c62e60 100644 --- a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs +++ b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs @@ -61,18 +61,7 @@ public async Task> GetVerificationTasksAsync(Ex ExecutionEngine.PrintBplFile(engine.Options, fileName, boogieProgram, false, false, engine.Options.PrettyPrint); } - var tasksFromBoogie = engine.GetVerificationTasks(boogieProgram); - - // Ordering is required to let gutter icon tests behave more deterministically - // In situations where there are multiple valid orders of execution - // In particular, GitIssue3821GutterIgnoredProblem fails without this - // We can consider turning off that test so we do not need this hack - // Better would be to compute gutter icons on the client - var ordered = tasksFromBoogie. - OrderBy(s => s.ScopeToken). - ThenByDescending(s => s.ScopeId). - ThenBy(s => s.Token).ToList(); - return ordered; + return engine.GetVerificationTasks(boogieProgram); } finally { mutex.Release(); From 07f5f10896e21a172dbd3082909edc7b45878def Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 6 Feb 2024 11:01:11 +0100 Subject: [PATCH 34/40] Add test-case and allow not specifying the filter position filename --- Source/DafnyDriver/CliCompilation.cs | 2 +- .../LitTests/LitTest/verification/Inputs/single-file.dfy | 4 ++++ .../TestFiles/LitTests/LitTest/verification/filter.dfy | 3 ++- .../LitTests/LitTest/verification/filter.dfy.expect | 8 +++++++- 4 files changed, 14 insertions(+), 3 deletions(-) diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 4b6513b8b84..3175412e17b 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -281,7 +281,7 @@ private List FilterCanVerifies(List canVerifies, out int 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"); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/single-file.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/single-file.dfy index c35a66d605d..24eb8c2507a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/single-file.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/single-file.dfy @@ -18,4 +18,8 @@ method Loop() { 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 656775d6d7a..47f4bbcca92 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy @@ -10,5 +10,6 @@ // 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='e.dfy:20' %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 96ac88dd566..af96cf314c4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy.expect @@ -9,8 +9,10 @@ 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, 2 errors +Dafny program verifier finished with 1 verified, 4 errors Dafny program verifier finished with 0 assertions verified, 0 errors @@ -32,3 +34,7 @@ single-file.dfy(16,14): Error: loop invariant violation Dafny program verifier finished with 0 assertions 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 0 assertions verified, 2 errors From b025fac11335123478c40e35064f7567a86ce3fb Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 6 Feb 2024 13:34:16 +0100 Subject: [PATCH 35/40] Add missing capital --- .../TestFiles/LitTests/LitTest/verification/filter.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy index 47f4bbcca92..0db23fb8333 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter.dfy @@ -3,7 +3,7 @@ // 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 --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 From db5561e183607dc3ab8a3bc51b035a0c08b83e5d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 6 Feb 2024 16:48:10 +0100 Subject: [PATCH 36/40] Configure test timeout --- Source/XUnitExtensions/Lit/LitTestCase.cs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Source/XUnitExtensions/Lit/LitTestCase.cs b/Source/XUnitExtensions/Lit/LitTestCase.cs index 18dcafde3a8..20bdbf205e8 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,8 @@ public static LitTestCase Read(string filePath, LitTestConfiguration config) { } public static void Run(string filePath, LitTestConfiguration config, ITestOutputHelper outputHelper) { - Read(filePath, config).Execute(outputHelper); + var task = Task.Run(() => Read(filePath, config).Execute(outputHelper)); + task.Wait(IndividualTestTimeout); } public LitTestCase(string filePath, IEnumerable commands, bool expectFailure) { From 5d2a74980f962c77696c4242f5f022e93dc946e1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 7 Feb 2024 14:19:57 +0100 Subject: [PATCH 37/40] Fixes --- Source/XUnitExtensions/Lit/LitTestCase.cs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Source/XUnitExtensions/Lit/LitTestCase.cs b/Source/XUnitExtensions/Lit/LitTestCase.cs index 20bdbf205e8..4fb09831803 100644 --- a/Source/XUnitExtensions/Lit/LitTestCase.cs +++ b/Source/XUnitExtensions/Lit/LitTestCase.cs @@ -56,7 +56,8 @@ public static LitTestCase Read(string filePath, LitTestConfiguration config) { } public static void Run(string filePath, LitTestConfiguration config, ITestOutputHelper outputHelper) { - var task = Task.Run(() => Read(filePath, config).Execute(outputHelper)); + var litTestCase = Read(filePath, config); + var task = Task.Run(() => litTestCase.Execute(outputHelper)); task.Wait(IndividualTestTimeout); } @@ -86,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; } } From f2f0c656abb63895854a26ab4ebb3a2f20f22191 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 7 Feb 2024 16:07:10 +0100 Subject: [PATCH 38/40] Remove duplication and make error message more specific --- Source/DafnyDriver/CliCompilation.cs | 16 ++-------------- 1 file changed, 2 insertions(+), 14 deletions(-) diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 3175412e17b..2bb07b3c550 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -207,19 +207,7 @@ public async Task VerifyAllAndPrintSummary() { results.TaskFilter = t => KeepVerificationTask(t, line.Value); } - var queueVerificationTask = Compilation.VerifyCanVerify(canVerify, results.TaskFilter); - var tasks = new List() { queueVerificationTask }; - var timeLimitSeconds = TimeSpan.FromSeconds(options.Get(BoogieOptionBag.VerificationTimeLimit)); - if (timeLimitSeconds.Seconds != 0) { - tasks.Add(Task.Delay(timeLimitSeconds)); - } - await Task.WhenAny(tasks); - if (!queueVerificationTask.IsCompleted) { - Compilation.Reporter.Error(MessageSource.Verifier, canVerify.Tok, - "Dafny encountered an internal error during verification. Please report it at .\n"); - break; - } - await queueVerificationTask; + await Compilation.VerifyCanVerify(canVerify, results.TaskFilter); } foreach (var canVerify in orderedCanVerifies) { @@ -233,7 +221,7 @@ public async Task VerifyAllAndPrintSummary() { await Task.WhenAny(tasks); if (!results.Finished.Task.IsCompleted) { Compilation.Reporter.Error(MessageSource.Verifier, canVerify.Tok, - "Dafny encountered an internal error during verification. Please report it at .\n"); + "Dafny encountered an internal error while waiting for this symbol to verify. Please report it at .\n"); break; } await results.Finished.Task; From 1683a4bb76d4db1f7e265923ac2a7995e0c846c1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 8 Feb 2024 13:58:47 +0100 Subject: [PATCH 39/40] Remove unused check --- Source/DafnyLanguageServer/DafnyLanguageServer.cs | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs index 4b9fea91407..bf9929968d4 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs @@ -67,20 +67,11 @@ private static void PublishSolverPath(ILanguageServer server) { private static void HandleZ3Version(DafnyOptions options, 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"; } /// From 201e4cade9d1e142660cc610738110c0ca55fa74 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 8 Feb 2024 15:49:21 +0100 Subject: [PATCH 40/40] Fix counterexample tracking --- Source/DafnyLanguageServer/DafnyLanguageServer.cs | 4 ++-- .../Handlers/Custom/CounterExampleItem.cs | 10 +--------- Source/DafnyLanguageServer/Workspace/IdeState.cs | 4 ++-- 3 files changed, 5 insertions(+), 13 deletions(-) diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs index bf9929968d4..0ef3ba91dff 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,7 +65,7 @@ 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) { return; diff --git a/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs b/Source/DafnyLanguageServer/Handlers/Custom/CounterExampleItem.cs index f50b1932b40..0ccca4b0bfc 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/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index 2a48ed080bc..83dab60a87b 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -320,6 +320,7 @@ private IdeState HandleFinishedResolution(DafnyOptions options, return previousState with { StaticDiagnostics = finishedResolution.Diagnostics, Status = status, + Counterexamples = Array.Empty(), ResolvedProgram = finishedResolution.Result.ResolvedProgram, SymbolTable = symbolTable ?? previousState.SymbolTable, SignatureAndCompletionTable = signatureAndCompletionTable, @@ -455,7 +456,6 @@ private IdeState HandleBoogieUpdate(DafnyOptions options, ILogger logger, Boogie var diagnostics = previousView?.Diagnostics ?? Array.Empty(); if (boogieUpdate.BoogieStatus is Running) { diagnostics = Array.Empty(); - counterExamples = Array.Empty(); hitErrorLimit = false; } @@ -470,7 +470,7 @@ private IdeState HandleBoogieUpdate(DafnyOptions options, ILogger logger, Boogie Compilation.GetDiagnosticsFromResult(options, previousState.Uri, boogieUpdate.VerificationTask, completed.Result); diagnostics = newDiagnostics.Select(d => d.ToLspDiagnostic()).ToList(); logger.LogTrace( - $"Completed received for {previousState.Input} and found #{diagnostics.Count} diagnostics."); + $"Completed received for {previousState.Input} and found #{diagnostics.Count} diagnostics and #{completed.Result.CounterExamples.Count} counterexamples."); } var newCanVerifyDiagnostics = new List();