From 3b44de2879bc9a9bc4c9282a27a5796501363ce8 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 1 Apr 2024 13:11:52 +0200 Subject: [PATCH 1/6] Add test and update --progress behavior to include an outcome --- Source/DafnyDriver/CliCompilation.cs | 23 +++++++++++++++--- .../isolate-assertions.dfy.expect | 8 +++---- .../outOfResourceAndIsolateAssertions.dfy | 13 ++++++++++ ...tOfResourceAndIsolateAssertions.dfy.expect | 3 +++ .../LitTest/verification/progress.dfy.expect | 24 +++++++++---------- 5 files changed, 52 insertions(+), 19 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 8ef85d82403..6afcacefa3b 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -14,6 +14,7 @@ using Microsoft.Dafny.LanguageServer.Language.Symbols; using Microsoft.Dafny.LanguageServer.Workspace; using Microsoft.Extensions.Logging; +using VC; using Token = Microsoft.Dafny.Token; namespace DafnyDriver.Commands; @@ -181,10 +182,13 @@ public async IAsyncEnumerable VerifyAllLazily(int? randomSeed) if (Options.Get(CommonOptionBag.ProgressOption)) { var token = BoogieGenerator.ToDafnyToken(false, boogieUpdate.VerificationTask.Split.Token); + var runResult = completed.Result; + var resourcesUsed = runResult.ResourceCount.ToString("E1", CultureInfo.InvariantCulture); Options.OutputWriter.WriteLine( - $"Verified part {canVerifyResult.CompletedParts.Count}/{canVerifyResult.Tasks.Count} of {boogieUpdate.CanVerify.FullDafnyName}" + - $", on line {token.line} (time: {completed.Result.RunTime.Milliseconds}ms, " + - $"resource count: {completed.Result.ResourceCount.ToString("E1", CultureInfo.InvariantCulture)})"); + $"Verification part {canVerifyResult.CompletedParts.Count}/{canVerifyResult.Tasks.Count} of {boogieUpdate.CanVerify.FullDafnyName}" + + $", on line {token.line}, " + + $"{DescribeOutcome(Compilation.GetOutcome(runResult.Outcome))}" + + $", taking {runResult.RunTime.Milliseconds}ms and consuming {resourcesUsed} resources"); } if (canVerifyResult.CompletedParts.Count == canVerifyResult.Tasks.Count) { canVerifyResult.Finished.TrySetResult(); @@ -260,6 +264,19 @@ public async IAsyncEnumerable VerifyAllLazily(int? randomSeed) } } + public static string DescribeOutcome(VcOutcome outcome) { + return outcome switch { + VcOutcome.Correct => "verified successfully", + VcOutcome.Errors => "could not prove all assertions", + VcOutcome.Inconclusive => "was inconclusive", + VcOutcome.TimedOut => "timed out", + VcOutcome.OutOfResource => "ran out of resources", + VcOutcome.OutOfMemory => "ran out of memory", + VcOutcome.SolverException => "ran into a solver exception", + _ => throw new ArgumentOutOfRangeException(nameof(outcome), outcome, null) + }; + } + private List FilterCanVerifies(List canVerifies, out int? line) { var symbolFilter = Options.Get(VerifyCommand.FilterSymbol); if (symbolFilter != null) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy.expect index 524e0c4e9e8..d119b471288 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy.expect @@ -1,8 +1,8 @@ Verified 0/2 symbols. Waiting for Foo to verify. -Verified part 1/3 of Foo, on line 5 (redacted, resource count: 8.7E+002) -Verified part 2/3 of Foo, on line 6 (redacted, resource count: 3.1E+003) -Verified part 3/3 of Foo, on line 7 (redacted, resource count: 2.8E+003) +Verification part 1/3 of Foo, on line 5, verified successfully, taking 37ms and consuming 8.7E+002 resources +Verification part 2/3 of Foo, on line 6, verified successfully, taking 24ms and consuming 3.1E+003 resources +Verification part 3/3 of Foo, on line 7, verified successfully, taking 8ms and consuming 2.8E+003 resources Verified 1/2 symbols. Waiting for Bar to verify. -Verified part 1/1 of Bar, on line 10 (redacted, resource count: 3.1E+003) +Verification part 1/1 of Bar, on line 10, verified successfully, taking 9ms and consuming 3.1E+003 resources Dafny program verifier finished with 4 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy new file mode 100644 index 00000000000..0674f6c13b0 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy @@ -0,0 +1,13 @@ +// RUN: ! %verify --isolate-assertions --progress "%s" &> %t.raw +// RUN: %sed 's/time: \d*ms/redacted/g' %t.raw > %t +// RUN: %diff "%s.expect" %t + +ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)} + +lemma{:resource_limit 10000000} L() +{ + assert true; + assert f(10, 5) == 0; + assert true; + assert f(10, 6) == 0; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect new file mode 100644 index 00000000000..1a1f32ef221 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect @@ -0,0 +1,3 @@ +git-issue106.dfy(6,32): Error: Verification out of resource (L) + +Dafny program verifier finished with 1 verified, 0 errors, 1 out of resource diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy.expect index 9b3819de3c2..6b3559e299d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy.expect @@ -1,19 +1,19 @@ Verified 0/5 symbols. Waiting for Foo to verify. -Verified part 1/3 of Foo, on line 5 (redacted, resource count: 8.7E+002) -Verified part 2/3 of Foo, on line 7 (redacted, resource count: 3.1E+003) -Verified part 3/3 of Foo, on line 8 (redacted, resource count: 2.8E+003) +Verification part 1/3 of Foo, on line 5, verified successfully, taking 40ms and consuming 8.7E+002 resources +Verification part 2/3 of Foo, on line 7, verified successfully, taking 24ms and consuming 3.1E+003 resources +Verification part 3/3 of Foo, on line 8, verified successfully, taking 9ms and consuming 2.8E+003 resources Verified 1/5 symbols. Waiting for Faz to verify. -Verified part 1/2 of Faz, on line 11 (redacted, resource count: 8.7E+002) -Verified part 2/2 of Faz, on line 11 (redacted, resource count: 3.1E+003) +Verification part 1/2 of Faz, on line 11, verified successfully, taking 7ms and consuming 8.7E+002 resources +Verification part 2/2 of Faz, on line 11, verified successfully, taking 8ms and consuming 3.1E+003 resources Verified 2/5 symbols. Waiting for Fopple to verify. -Verified part 1/2 of Fopple, on line 13 (redacted, resource count: 8.7E+002) -Verified part 2/2 of Fopple, on line 13 (redacted, resource count: 3.1E+003) +Verification part 1/2 of Fopple, on line 13, verified successfully, taking 6ms and consuming 8.7E+002 resources +Verification part 2/2 of Fopple, on line 13, verified successfully, taking 8ms and consuming 3.1E+003 resources Verified 3/5 symbols. Waiting for Burp to verify. -Verified part 1/3 of Burp, on line 15 (redacted, resource count: 8.7E+002) -Verified part 2/3 of Burp, on line 17 (redacted, resource count: 3.1E+003) -Verified part 3/3 of Burp, on line 18 (redacted, resource count: 2.8E+003) +Verification part 1/3 of Burp, on line 15, verified successfully, taking 6ms and consuming 8.7E+002 resources +Verification part 2/3 of Burp, on line 17, verified successfully, taking 9ms and consuming 3.1E+003 resources +Verification part 3/3 of Burp, on line 18, verified successfully, taking 8ms and consuming 2.8E+003 resources Verified 4/5 symbols. Waiting for Blanc to verify. -Verified part 1/2 of Blanc, on line 21 (redacted, resource count: 8.7E+002) -Verified part 2/2 of Blanc, on line 21 (redacted, resource count: 3.1E+003) +Verification part 1/2 of Blanc, on line 21, verified successfully, taking 6ms and consuming 8.7E+002 resources +Verification part 2/2 of Blanc, on line 21, verified successfully, taking 9ms and consuming 3.1E+003 resources Dafny program verifier finished with 12 verified, 0 errors From ba83e0a6e1ada1c394a575867a0fe0e651f0386f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 1 Apr 2024 13:23:01 +0200 Subject: [PATCH 2/6] Make reported token when verification runs out of resources, more precise --- Source/DafnyCore/Pipeline/Compilation.cs | 2 +- Source/DafnyDriver/Commands/VerifyCommand.cs | 2 +- .../verification/isolate-assertions.dfy | 2 +- .../outOfResourceAndIsolateAssertions.dfy | 2 +- ...tOfResourceAndIsolateAssertions.dfy.expect | 38 ++++++++++++++++++- Source/XUnitExtensions/Lit/DiffCommand.cs | 2 +- 6 files changed, 41 insertions(+), 7 deletions(-) diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index 4b9da9ca5e3..bd94bad71b7 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -500,7 +500,7 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, string name, var dafnyCounterExampleModel = options.ExtractCounterexample ? new DafnyModel(counterExample.Model, options) : null; errorReporter.ReportBoogieError(errorInformation, dafnyCounterExampleModel); } - + // This reports problems that are not captured by counter-examples, like a time-out // 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(), diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs index 5913ead4e9c..d1270ebc7ab 100644 --- a/Source/DafnyDriver/Commands/VerifyCommand.cs +++ b/Source/DafnyDriver/Commands/VerifyCommand.cs @@ -163,7 +163,7 @@ public static void ReportVerificationDiagnostics(CliCompilation compilation, IOb // We use an intermediate reporter so we can sort the diagnostics from all parts by token var batchReporter = new BatchErrorReporter(compilation.Options); foreach (var completed in result.Results) { - Compilation.ReportDiagnosticsInResult(compilation.Options, result.CanVerify.FullDafnyName, result.CanVerify.NameToken, + Compilation.ReportDiagnosticsInResult(compilation.Options, result.CanVerify.FullDafnyName, completed.Task.Token, (uint)completed.Result.RunTime.Seconds, completed.Result, batchReporter); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy index 327bc1ea5b0..93f161582b3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy @@ -1,5 +1,5 @@ // RUN: %verify --progress --cores=1 %s &> %t.raw -// RUN: %sed 's/time: \d*ms/redacted/g' "%t".raw > %t +// RUN: %sed 's/taking: \d*ms and /redacted/g' %t.raw > %t // RUN: %diff "%s.expect" "%t" method {:isolate_assertions} Foo() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy index 0674f6c13b0..f2f99d97c0b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy @@ -1,5 +1,5 @@ // RUN: ! %verify --isolate-assertions --progress "%s" &> %t.raw -// RUN: %sed 's/time: \d*ms/redacted/g' %t.raw > %t +// RUN: %sed 's/taking: \d*ms and /redacted/g' %t.raw > %t // RUN: %diff "%s.expect" %t ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect index 1a1f32ef221..6d924d71232 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect @@ -1,3 +1,37 @@ -git-issue106.dfy(6,32): Error: Verification out of resource (L) +Verified 0/2 symbols. Waiting for f to verify. +Verification part 1/11 of f, on line 5, verified successfully, taking 40ms and consuming 9.5E+002 resources +Verification part 2/11 of f, on line 5, verified successfully, taking 66ms and consuming 6.2E+003 resources +Verification part 3/11 of f, on line 5, verified successfully, taking 16ms and consuming 6.7E+003 resources +Verification part 4/11 of f, on line 5, verified successfully, taking 11ms and consuming 6.7E+003 resources +Verification part 5/11 of f, on line 5, verified successfully, taking 13ms and consuming 5.8E+003 resources +Verification part 6/11 of f, on line 5, verified successfully, taking 11ms and consuming 5.9E+003 resources +Verification part 7/11 of f, on line 5, verified successfully, taking 10ms and consuming 5.9E+003 resources +Verification part 8/11 of f, on line 5, verified successfully, taking 11ms and consuming 7.8E+003 resources +Verification part 9/11 of f, on line 5, verified successfully, taking 10ms and consuming 6.0E+003 resources +VerifVerified 0/2 symbols. Waiting for f to verify. +Verification part 1/11 of f, on line 5, verified successfully, taking 40ms and consuming 9.5E+002 resources +Verification part 2/11 of f, on line 5, verified successfully, taking 66ms and consuming 6.2E+003 resources +Verification part 3/11 of f, on line 5, verified successfully, taking 16ms and consuming 6.7E+003 resources +Verification part 4/11 of f, on line 5, verified successfully, taking 11ms and consuming 6.7E+003 resources +Verification part 5/11 of f, on line 5, verified successfully, taking 13ms and consuming 5.8E+003 resources +Verification part 6/11 of f, on line 5, verified successfully, taking 11ms and consuming 5.9E+003 resources +Verification part 7/11 of f, on line 5, verified successfully, taking 10ms and consuming 5.9E+003 resources +Verification part 8/11 of f, on line 5, verified successfully, taking 11ms and consuming 7.8E+003 resources +Verification part 9/11 of f, on line 5, verified successfully, taking 10ms and consuming 6.0E+003 resources +Verification part 11/11 of f, on line 5, verified successfully, taking 10ms and consuming 6.0E+003 resources +ully, taking 40ms and consuming 9.5E+002 resources +Verification part 2/11 of f, on line 5, verified suc +Verification part 1/9 of L, on line 7, verified successfully, taking 7ms and consuming 8.7E+002 resources +Verified 1/2 symbols. Waiting for L to verify. +Verification part 2/9 of L, on line 9, verified successfully, taking 9ms and consuming 5.6E+003 resources +Verification part 3/9 of L, on line 10, verified successfully, taking 11ms and consuming 5.8E+003 resources +Verification part 4/9 of L, on line 10, verified successfully, taking 10ms and consuming 6.0E+003 resources +Verification part 5/9 of L, on line 11, verified successfully, taking 9ms and consuming 5.5E+003 resources +Verification part 6/9 of L, on line 12, verified successfully, taking 9ms and consuming 5.5E+003 resources +Verification part 7/9 of L, on line 12, verified successfully, taking 10ms and consuming 6.8E+003 resources +Verification part 8/9 of L, on line 10, ran out of resources, taking 906ms and consuming 1.0E+007 resources +Verification part 9/9 of L, on line 12, ran out of resources, taking 423ms and consuming 1.0E+007 resources +outOfResourceAndIsolateAssertions.dfy(10,18): Error: Verification out of resource (L) +outOfResourceAndIsolateAssertions.dfy(12,18): Error: Verification out of resource (L) -Dafny program verifier finished with 1 verified, 0 errors, 1 out of resource +Dafny program verifier finished with 18 verified, 0 errors, 2 out of resource diff --git a/Source/XUnitExtensions/Lit/DiffCommand.cs b/Source/XUnitExtensions/Lit/DiffCommand.cs index fbc0f868936..f5c10dbb874 100644 --- a/Source/XUnitExtensions/Lit/DiffCommand.cs +++ b/Source/XUnitExtensions/Lit/DiffCommand.cs @@ -11,7 +11,7 @@ namespace XUnitExtensions.Lit { /// because 'diff' does not exist on Windows. /// public class DiffCommand : ILitCommand { - public static readonly bool UpdateExpectFile = false; + public static readonly bool UpdateExpectFile = true; public string ExpectedPath { get; } public string ActualPath { get; } From fe70c24e362dcff2818a0a6585d38f385c156f63 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 1 Apr 2024 13:31:18 +0200 Subject: [PATCH 3/6] Fixes --- Source/DafnyCore/Pipeline/Compilation.cs | 2 +- .../verification/isolate-assertions.dfy | 2 +- .../isolate-assertions.dfy.expect | 8 +-- .../outOfResourceAndIsolateAssertions.dfy | 6 +-- ...tOfResourceAndIsolateAssertions.dfy.expect | 51 ++++++++----------- .../LitTest/verification/progress.dfy | 2 +- .../LitTest/verification/progress.dfy.expect | 24 ++++----- Source/XUnitExtensions/Lit/DiffCommand.cs | 2 +- 8 files changed, 43 insertions(+), 54 deletions(-) diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index bd94bad71b7..4b9da9ca5e3 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -500,7 +500,7 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, string name, var dafnyCounterExampleModel = options.ExtractCounterexample ? new DafnyModel(counterExample.Model, options) : null; errorReporter.ReportBoogieError(errorInformation, dafnyCounterExampleModel); } - + // This reports problems that are not captured by counter-examples, like a time-out // 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(), diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy index 93f161582b3..c992fcd4c28 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy @@ -1,5 +1,5 @@ // RUN: %verify --progress --cores=1 %s &> %t.raw -// RUN: %sed 's/taking: \d*ms and /redacted/g' %t.raw > %t +// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t // RUN: %diff "%s.expect" "%t" method {:isolate_assertions} Foo() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy.expect index d119b471288..66919320ee4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy.expect @@ -1,8 +1,8 @@ Verified 0/2 symbols. Waiting for Foo to verify. -Verification part 1/3 of Foo, on line 5, verified successfully, taking 37ms and consuming 8.7E+002 resources -Verification part 2/3 of Foo, on line 6, verified successfully, taking 24ms and consuming 3.1E+003 resources -Verification part 3/3 of Foo, on line 7, verified successfully, taking 8ms and consuming 2.8E+003 resources +Verification part 1/3 of Foo, on line 5, verified successfully, redacted and consuming 8.7E+002 resources +Verification part 2/3 of Foo, on line 6, verified successfully, redacted and consuming 3.1E+003 resources +Verification part 3/3 of Foo, on line 7, verified successfully, redacted and consuming 2.8E+003 resources Verified 1/2 symbols. Waiting for Bar to verify. -Verification part 1/1 of Bar, on line 10, verified successfully, taking 9ms and consuming 3.1E+003 resources +Verification part 1/1 of Bar, on line 10, verified successfully, redacted and consuming 3.1E+003 resources Dafny program verifier finished with 4 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy index f2f99d97c0b..376ae94651f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy @@ -1,5 +1,5 @@ // RUN: ! %verify --isolate-assertions --progress "%s" &> %t.raw -// RUN: %sed 's/taking: \d*ms and /redacted/g' %t.raw > %t +// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t // RUN: %diff "%s.expect" %t ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)} @@ -7,7 +7,7 @@ ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + lemma{:resource_limit 10000000} L() { assert true; - assert f(10, 5) == 0; + assert f(10, 5) == 0; // runs out of resources assert true; - assert f(10, 6) == 0; + assert f(10, 6) == 0; // runs out of resources } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect index 6d924d71232..91ecd5fb843 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect @@ -1,36 +1,25 @@ Verified 0/2 symbols. Waiting for f to verify. -Verification part 1/11 of f, on line 5, verified successfully, taking 40ms and consuming 9.5E+002 resources -Verification part 2/11 of f, on line 5, verified successfully, taking 66ms and consuming 6.2E+003 resources -Verification part 3/11 of f, on line 5, verified successfully, taking 16ms and consuming 6.7E+003 resources -Verification part 4/11 of f, on line 5, verified successfully, taking 11ms and consuming 6.7E+003 resources -Verification part 5/11 of f, on line 5, verified successfully, taking 13ms and consuming 5.8E+003 resources -Verification part 6/11 of f, on line 5, verified successfully, taking 11ms and consuming 5.9E+003 resources -Verification part 7/11 of f, on line 5, verified successfully, taking 10ms and consuming 5.9E+003 resources -Verification part 8/11 of f, on line 5, verified successfully, taking 11ms and consuming 7.8E+003 resources -Verification part 9/11 of f, on line 5, verified successfully, taking 10ms and consuming 6.0E+003 resources -VerifVerified 0/2 symbols. Waiting for f to verify. -Verification part 1/11 of f, on line 5, verified successfully, taking 40ms and consuming 9.5E+002 resources -Verification part 2/11 of f, on line 5, verified successfully, taking 66ms and consuming 6.2E+003 resources -Verification part 3/11 of f, on line 5, verified successfully, taking 16ms and consuming 6.7E+003 resources -Verification part 4/11 of f, on line 5, verified successfully, taking 11ms and consuming 6.7E+003 resources -Verification part 5/11 of f, on line 5, verified successfully, taking 13ms and consuming 5.8E+003 resources -Verification part 6/11 of f, on line 5, verified successfully, taking 11ms and consuming 5.9E+003 resources -Verification part 7/11 of f, on line 5, verified successfully, taking 10ms and consuming 5.9E+003 resources -Verification part 8/11 of f, on line 5, verified successfully, taking 11ms and consuming 7.8E+003 resources -Verification part 9/11 of f, on line 5, verified successfully, taking 10ms and consuming 6.0E+003 resources -Verification part 11/11 of f, on line 5, verified successfully, taking 10ms and consuming 6.0E+003 resources -ully, taking 40ms and consuming 9.5E+002 resources -Verification part 2/11 of f, on line 5, verified suc -Verification part 1/9 of L, on line 7, verified successfully, taking 7ms and consuming 8.7E+002 resources +Verification part 1/11 of f, on line 5, verified successfully, redacted and consuming 9.5E+002 resources +Verification part 2/11 of f, on line 5, verified successfully, redacted and consuming 6.2E+003 resources +Verification part 3/11 of f, on line 5, verified successfully, redacted and consuming 6.7E+003 resources +Verification part 4/11 of f, on line 5, verified successfully, redacted and consuming 6.7E+003 resources +Verification part 5/11 of f, on line 5, verified successfully, redacted and consuming 5.8E+003 resources +Verification part 6/11 of f, on line 5, verified successfully, redacted and consuming 5.9E+003 resources +Verification part 7/11 of f, on line 5, verified successfully, redacted and consuming 5.9E+003 resources +Verification part 8/11 of f, on line 5, verified successfully, redacted and consuming 7.8E+003 resources +Verification part 9/11 of f, on line 5, verified successfully, redacted and consuming 6.0E+003 resources +Verification part 10/11 of f, on line 5, verified successfully, redacted and consuming 6.0E+003 resources +Verification part 11/11 of f, on line 5, verified successfully, redacted and consuming 6.1E+003 resources +Verification part 1/9 of L, on line 7, verified successfully, redacted and consuming 8.7E+002 resources Verified 1/2 symbols. Waiting for L to verify. -Verification part 2/9 of L, on line 9, verified successfully, taking 9ms and consuming 5.6E+003 resources -Verification part 3/9 of L, on line 10, verified successfully, taking 11ms and consuming 5.8E+003 resources -Verification part 4/9 of L, on line 10, verified successfully, taking 10ms and consuming 6.0E+003 resources -Verification part 5/9 of L, on line 11, verified successfully, taking 9ms and consuming 5.5E+003 resources -Verification part 6/9 of L, on line 12, verified successfully, taking 9ms and consuming 5.5E+003 resources -Verification part 7/9 of L, on line 12, verified successfully, taking 10ms and consuming 6.8E+003 resources -Verification part 8/9 of L, on line 10, ran out of resources, taking 906ms and consuming 1.0E+007 resources -Verification part 9/9 of L, on line 12, ran out of resources, taking 423ms and consuming 1.0E+007 resources +Verification part 2/9 of L, on line 9, verified successfully, redacted and consuming 5.6E+003 resources +Verification part 3/9 of L, on line 10, verified successfully, redacted and consuming 5.8E+003 resources +Verification part 4/9 of L, on line 10, verified successfully, redacted and consuming 6.0E+003 resources +Verification part 5/9 of L, on line 11, verified successfully, redacted and consuming 5.5E+003 resources +Verification part 6/9 of L, on line 12, verified successfully, redacted and consuming 5.5E+003 resources +Verification part 7/9 of L, on line 12, verified successfully, redacted and consuming 6.8E+003 resources +Verification part 8/9 of L, on line 10, ran out of resources, redacted and consuming 1.0E+007 resources +Verification part 9/9 of L, on line 12, ran out of resources, redacted and consuming 1.0E+007 resources outOfResourceAndIsolateAssertions.dfy(10,18): Error: Verification out of resource (L) outOfResourceAndIsolateAssertions.dfy(12,18): Error: Verification out of resource (L) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy index c3badc8ec6f..90626b23cbd 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy @@ -1,5 +1,5 @@ // RUN: %verify --progress --isolate-assertions --cores=1 %s > %t.raw -// RUN: %sed 's/time: \d*ms/redacted/g' "%t".raw > %t +// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t // RUN: %diff "%s.expect" "%t" method Foo() diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy.expect index 6b3559e299d..3110aa5d723 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy.expect @@ -1,19 +1,19 @@ Verified 0/5 symbols. Waiting for Foo to verify. -Verification part 1/3 of Foo, on line 5, verified successfully, taking 40ms and consuming 8.7E+002 resources -Verification part 2/3 of Foo, on line 7, verified successfully, taking 24ms and consuming 3.1E+003 resources -Verification part 3/3 of Foo, on line 8, verified successfully, taking 9ms and consuming 2.8E+003 resources +Verification part 1/3 of Foo, on line 5, verified successfully, redacted and consuming 8.7E+002 resources +Verification part 2/3 of Foo, on line 7, verified successfully, redacted and consuming 3.1E+003 resources +Verification part 3/3 of Foo, on line 8, verified successfully, redacted and consuming 2.8E+003 resources Verified 1/5 symbols. Waiting for Faz to verify. -Verification part 1/2 of Faz, on line 11, verified successfully, taking 7ms and consuming 8.7E+002 resources -Verification part 2/2 of Faz, on line 11, verified successfully, taking 8ms and consuming 3.1E+003 resources +Verification part 1/2 of Faz, on line 11, verified successfully, redacted and consuming 8.7E+002 resources +Verification part 2/2 of Faz, on line 11, verified successfully, redacted and consuming 3.1E+003 resources Verified 2/5 symbols. Waiting for Fopple to verify. -Verification part 1/2 of Fopple, on line 13, verified successfully, taking 6ms and consuming 8.7E+002 resources -Verification part 2/2 of Fopple, on line 13, verified successfully, taking 8ms and consuming 3.1E+003 resources +Verification part 1/2 of Fopple, on line 13, verified successfully, redacted and consuming 8.7E+002 resources +Verification part 2/2 of Fopple, on line 13, verified successfully, redacted and consuming 3.1E+003 resources Verified 3/5 symbols. Waiting for Burp to verify. -Verification part 1/3 of Burp, on line 15, verified successfully, taking 6ms and consuming 8.7E+002 resources -Verification part 2/3 of Burp, on line 17, verified successfully, taking 9ms and consuming 3.1E+003 resources -Verification part 3/3 of Burp, on line 18, verified successfully, taking 8ms and consuming 2.8E+003 resources +Verification part 1/3 of Burp, on line 15, verified successfully, redacted and consuming 8.7E+002 resources +Verification part 2/3 of Burp, on line 17, verified successfully, redacted and consuming 3.1E+003 resources +Verification part 3/3 of Burp, on line 18, verified successfully, redacted and consuming 2.8E+003 resources Verified 4/5 symbols. Waiting for Blanc to verify. -Verification part 1/2 of Blanc, on line 21, verified successfully, taking 6ms and consuming 8.7E+002 resources -Verification part 2/2 of Blanc, on line 21, verified successfully, taking 9ms and consuming 3.1E+003 resources +Verification part 1/2 of Blanc, on line 21, verified successfully, redacted and consuming 8.7E+002 resources +Verification part 2/2 of Blanc, on line 21, verified successfully, redacted and consuming 3.1E+003 resources Dafny program verifier finished with 12 verified, 0 errors diff --git a/Source/XUnitExtensions/Lit/DiffCommand.cs b/Source/XUnitExtensions/Lit/DiffCommand.cs index f5c10dbb874..fbc0f868936 100644 --- a/Source/XUnitExtensions/Lit/DiffCommand.cs +++ b/Source/XUnitExtensions/Lit/DiffCommand.cs @@ -11,7 +11,7 @@ namespace XUnitExtensions.Lit { /// because 'diff' does not exist on Windows. /// public class DiffCommand : ILitCommand { - public static readonly bool UpdateExpectFile = true; + public static readonly bool UpdateExpectFile = false; public string ExpectedPath { get; } public string ActualPath { get; } From a05f0f76e07d48ace40ea4db8e9bebc910eccf5e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 1 Apr 2024 13:36:51 +0200 Subject: [PATCH 4/6] Add release note --- docs/dev/news/5281.feat | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/news/5281.feat diff --git a/docs/dev/news/5281.feat b/docs/dev/news/5281.feat new file mode 100644 index 00000000000..0257cbf7639 --- /dev/null +++ b/docs/dev/news/5281.feat @@ -0,0 +1 @@ +Improved error reporting when verification times out or runs out of resources, so that when using --isolate-assertions, the error message points to the problematic assertion. \ No newline at end of file From 1b16f7c42c90cc75fcfa13a98f1f66f972ad1e58 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 1 Apr 2024 23:17:41 +0200 Subject: [PATCH 5/6] Fix test instability --- .../verification/outOfResourceAndIsolateAssertions.dfy | 2 +- .../outOfResourceAndIsolateAssertions.dfy.expect | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy index 376ae94651f..099fea64ca0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy @@ -1,4 +1,4 @@ -// RUN: ! %verify --isolate-assertions --progress "%s" &> %t.raw +// RUN: ! %verify --isolate-assertions --cores=1 --progress "%s" &> %t.raw // RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t // RUN: %diff "%s.expect" %t diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect index 91ecd5fb843..ca669adae56 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect @@ -10,15 +10,15 @@ Verification part 8/11 of f, on line 5, verified successfully, redacted and cons Verification part 9/11 of f, on line 5, verified successfully, redacted and consuming 6.0E+003 resources Verification part 10/11 of f, on line 5, verified successfully, redacted and consuming 6.0E+003 resources Verification part 11/11 of f, on line 5, verified successfully, redacted and consuming 6.1E+003 resources -Verification part 1/9 of L, on line 7, verified successfully, redacted and consuming 8.7E+002 resources Verified 1/2 symbols. Waiting for L to verify. +Verification part 1/9 of L, on line 7, verified successfully, redacted and consuming 8.7E+002 resources Verification part 2/9 of L, on line 9, verified successfully, redacted and consuming 5.6E+003 resources Verification part 3/9 of L, on line 10, verified successfully, redacted and consuming 5.8E+003 resources Verification part 4/9 of L, on line 10, verified successfully, redacted and consuming 6.0E+003 resources -Verification part 5/9 of L, on line 11, verified successfully, redacted and consuming 5.5E+003 resources -Verification part 6/9 of L, on line 12, verified successfully, redacted and consuming 5.5E+003 resources -Verification part 7/9 of L, on line 12, verified successfully, redacted and consuming 6.8E+003 resources -Verification part 8/9 of L, on line 10, ran out of resources, redacted and consuming 1.0E+007 resources +Verification part 5/9 of L, on line 10, ran out of resources, redacted and consuming 1.0E+007 resources +Verification part 6/9 of L, on line 11, verified successfully, redacted and consuming 5.5E+003 resources +Verification part 7/9 of L, on line 12, verified successfully, redacted and consuming 5.5E+003 resources +Verification part 8/9 of L, on line 12, verified successfully, redacted and consuming 6.8E+003 resources Verification part 9/9 of L, on line 12, ran out of resources, redacted and consuming 1.0E+007 resources outOfResourceAndIsolateAssertions.dfy(10,18): Error: Verification out of resource (L) outOfResourceAndIsolateAssertions.dfy(12,18): Error: Verification out of resource (L) From 72a053d53ab0ca239ed75c113196bc50c483e420 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 1 Apr 2024 23:17:59 +0200 Subject: [PATCH 6/6] Update docs/dev/news/5281.feat MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Mikaël Mayer --- docs/dev/news/5281.feat | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/dev/news/5281.feat b/docs/dev/news/5281.feat index 0257cbf7639..1eacc1e7826 100644 --- a/docs/dev/news/5281.feat +++ b/docs/dev/news/5281.feat @@ -1 +1 @@ -Improved error reporting when verification times out or runs out of resources, so that when using --isolate-assertions, the error message points to the problematic assertion. \ No newline at end of file +Improved error reporting when verification times out or runs out of resources, so that when using `--isolate-assertions`, the error message points to the problematic assertion. \ No newline at end of file