From bd929baae75c1d24ca03ef0ad43ae622efa2ff06 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 14 Nov 2024 14:54:38 +0100 Subject: [PATCH 1/4] Enable isolating all return statements --- Source/DafnyCore/AST/Tokens.cs | 5 +++++ Source/DafnyCore/DafnyCore.csproj | 2 +- .../proofDivision/isolateAllAssertions.dfy | 14 ++++++++++---- .../proofDivision/isolateAllAssertions.dfy.expect | 12 +++++++++--- 4 files changed, 25 insertions(+), 8 deletions(-) diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs index fd5ad0c4d5..1fcc88a332 100644 --- a/Source/DafnyCore/AST/Tokens.cs +++ b/Source/DafnyCore/AST/Tokens.cs @@ -66,6 +66,7 @@ public Token(int linenum, int colnum) { this.val = ""; } + public bool IsSourceToken => this != NoToken; public int kind { get; set; } // Used by coco, so we can't rename it to Kind public string ActualFilename => Filepath; @@ -160,6 +161,8 @@ public bool IsValid { get { return WrappedToken.IsValid; } } + public virtual bool IsSourceToken => false; + public int kind { get { return WrappedToken.kind; } set { WrappedToken.kind = value; } @@ -305,6 +308,8 @@ public override IToken WithVal(string newVal) { throw new NotImplementedException(); } + public override bool IsSourceToken => this != NoToken; + public BoogieRangeToken ToToken() { return new BoogieRangeToken(StartToken, EndToken, null); } diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 7aaae0f4f6..6c65a128f2 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -34,7 +34,7 @@ - + diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy index f53d0332b7..2363f8d4ac 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy @@ -1,13 +1,19 @@ -// RUN: %verify --progress VerificationJobs --cores=1 %s &> %t.raw +// RUN: ! %verify --progress VerificationJobs --cores=1 %s &> %t.raw // RUN: %sed 's#\(time.*\)##g' %t.raw > %t // RUN: %diff "%s.expect" "%t" - - -method {:isolate_assertions} Foo() { +method {:isolate_assertions} Foo(x: int) returns (r: int) + ensures r > 3 + ensures r < 10 +{ assert true; assert true; + if (x == 3) { + return 7; + } else { + return 12; + } } method Bar() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy.expect index ce6205ddf2..fd31a2e4c9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy.expect @@ -1,7 +1,13 @@ Verified 0/2 symbols. Waiting for Foo to verify. -Verified 1/2 of Foo: assertion at line 9 - verified successfully -Verified 2/2 of Foo: assertion at line 10 - verified successfully +Verified 1/6 of Foo: remaining assertions, assertion at line 10 - verified successfully +Verified 2/6 of Foo: remaining assertions, assertion at line 11 - verified successfully +Verified 3/6 of Foo: return at line 15, assertion at line 7 - verified successfully +Verified 4/6 of Foo: return at line 15, assertion at line 8 - could not be verified +Verified 5/6 of Foo: return at line 13, assertion at line 7 - verified successfully +Verified 6/6 of Foo: return at line 13, assertion at line 8 - verified successfully +isolateAllAssertions.dfy(15,4): Error: a postcondition could not be proved on this return path +isolateAllAssertions.dfy(8,12): Related location: this is the postcondition that could not be proved Verified 1/2 symbols. Waiting for Bar to verify. Verified 1/1 of Bar: entire body - verified successfully -Dafny program verifier finished with 3 verified, 0 errors +Dafny program verifier finished with 6 verified, 1 error From 18543e8fdfa696a934b4aa5066a223992051055d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 15 Nov 2024 15:50:59 +0100 Subject: [PATCH 2/4] Improve messaging and update tests --- Source/DafnyDriver/CliCompilation.cs | 2 +- .../verification/outOfResourceAndIsolateAssertions.dfy | 6 +++--- .../proofDivision/isolateAllAssertions.dfy.expect | 4 ++-- .../LitTest/vstte2012/BreadthFirstSearch.dfy.expect | 2 +- .../TestFiles/LitTests/LitTest/vstte2012/Tree.dfy.expect | 2 +- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 3787e5d1ea..0daff1c5f6 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -198,7 +198,7 @@ string OriginDescription(IImplementationPartOrigin origin, bool outer) { var result = origin switch { PathOrigin pathOrigin => $"{OriginDescription(pathOrigin.Inner, false)}" + $"after executing lines {string.Join(", ", pathOrigin.BranchTokens.Select(b => b.line))}", - RemainingAssertionsOrigin remainingAssertions => $"{OriginDescription(remainingAssertions.Origin, false)}remaining assertions", + RemainingAssertionsOrigin remainingAssertions => OriginDescription(remainingAssertions.Origin, false) + (outer ? "remaining assertions" : ""), IsolatedAssertionOrigin isolateOrigin => $"{OriginDescription(isolateOrigin.Origin, false)}assertion at line {isolateOrigin.line}", JumpOrigin returnOrigin => $"{OriginDescription(returnOrigin.Origin, false)}{JumpOriginKind(returnOrigin)} at line {returnOrigin.line}", AfterSplitOrigin splitOrigin => $"{OriginDescription(splitOrigin.Inner, false)}assertions after split_here at line {splitOrigin.line}", diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy index fb7ceac5f2..34ab6377f3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy @@ -1,9 +1,9 @@ // RUN: ! %verify --isolate-assertions --cores=1 --progress VerificationJobs "%s" &> %t.raw // RUN: %sed 's#\(time.*\)##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)} - +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; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy.expect index fd31a2e4c9..9c0187038c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy.expect @@ -1,6 +1,6 @@ Verified 0/2 symbols. Waiting for Foo to verify. -Verified 1/6 of Foo: remaining assertions, assertion at line 10 - verified successfully -Verified 2/6 of Foo: remaining assertions, assertion at line 11 - verified successfully +Verified 1/6 of Foo: assertion at line 10 - verified successfully +Verified 2/6 of Foo: assertion at line 11 - verified successfully Verified 3/6 of Foo: return at line 15, assertion at line 7 - verified successfully Verified 4/6 of Foo: return at line 15, assertion at line 8 - could not be verified Verified 5/6 of Foo: return at line 13, assertion at line 7 - verified successfully diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy.expect index e352fc1053..6252fafc31 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 142 verified, 0 errors +Dafny program verifier finished with 148 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 3b71b05bfb..2f021147f0 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 55 verified, 0 errors +Dafny program verifier finished with 67 verified, 0 errors From a0e423b2f0bcf6793865c87ba0bb9bc7dffee59d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 15 Nov 2024 15:52:53 +0100 Subject: [PATCH 3/4] Add release note --- docs/dev/news/5917.feat | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/news/5917.feat diff --git a/docs/dev/news/5917.feat b/docs/dev/news/5917.feat new file mode 100644 index 0000000000..0303609187 --- /dev/null +++ b/docs/dev/news/5917.feat @@ -0,0 +1 @@ +When using `--isolate-assertions` or `{:isolate_assertions}`, a separate assertion batch will be generated per pair of return statement and ensures clause. \ No newline at end of file From e07c01b7229d7e9dc79485a13bc7a5d900cfbb06 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 15 Nov 2024 16:19:18 +0100 Subject: [PATCH 4/4] update customboogie.patch --- customBoogie.patch | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/customBoogie.patch b/customBoogie.patch index 67588e2f76..9023f27d39 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + + +