From 0ff73c1a70bb1e35bf3c501efc42a5cfb6870a6b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 22 Oct 2024 15:32:27 +0200 Subject: [PATCH] Add support for isolate on continue statements --- .../AST/Statements/ControlFlow/BreakStmt.cs | 8 +++---- Source/DafnyCore/Dafny.atg | 4 +++- .../Statements/BoogieGenerator.TrStatement.cs | 22 ++++++++++++------- Source/DafnyDriver/CliCompilation.cs | 7 +++++- .../proofDivision/isolateAssertionOrJump.dfy | 10 ++++----- boogie | 2 +- 6 files changed, 33 insertions(+), 20 deletions(-) diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/BreakStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/BreakStmt.cs index 07d87acf39..84183cc683 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/BreakStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/BreakStmt.cs @@ -31,8 +31,8 @@ public BreakStmt(Cloner cloner, BreakStmt original) : base(cloner, original) { } } - public BreakStmt(RangeToken rangeToken, IToken targetLabel, bool isContinue) - : base(rangeToken) { + public BreakStmt(RangeToken rangeToken, IToken targetLabel, bool isContinue, Attributes attributes = null) + : base(rangeToken, attributes) { Contract.Requires(rangeToken != null); Contract.Requires(targetLabel != null); this.TargetLabel = targetLabel; @@ -43,8 +43,8 @@ public BreakStmt(RangeToken rangeToken, IToken targetLabel, bool isContinue) /// For "isContinue == false", represents the statement "break ^breakAndContinueCount ;". /// For "isContinue == true", represents the statement "break ^(breakAndContinueCount - 1) continue;". /// - public BreakStmt(RangeToken rangeToken, int breakAndContinueCount, bool isContinue) - : base(rangeToken) { + public BreakStmt(RangeToken rangeToken, int breakAndContinueCount, bool isContinue, Attributes attributes = null) + : base(rangeToken, attributes) { Contract.Requires(rangeToken != null); Contract.Requires(1 <= breakAndContinueCount); this.BreakAndContinueCount = breakAndContinueCount; diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 45d3a0967a..c8b2ba37b6 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -2264,8 +2264,10 @@ BreakStmt IToken start = Token.NoToken; IToken label = null; int breakAndContinueCount = 1; + Attributes attributes = null; .) ( "continue" (. start = t; isContinue = true; .) + [ Attribute ] [ LabelName ] | "break" (. start = t; .) ( LabelName @@ -2280,7 +2282,7 @@ BreakStmt (. Contract.Assert(label == null || breakAndContinueCount == 1); s = label != null ? new BreakStmt(new RangeToken(start, t), label, isContinue) : - new BreakStmt(new RangeToken(start, t), breakAndContinueCount, isContinue); + new BreakStmt(new RangeToken(start, t), breakAndContinueCount, isContinue, attributes); .) . diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs index 441ffefba8..ff27ec52f7 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs @@ -43,14 +43,8 @@ public void TrStmt(Statement stmt, BoogieStmtListBuilder builder, } else if (stmt is HideRevealStmt revealStmt) { TranslateRevealStmt(builder, locals, etran, revealStmt); - } else if (stmt is BreakStmt) { - var s = (BreakStmt)stmt; - AddComment(builder, stmt, $"{s.Kind} statement"); - foreach (var _ in Enumerable.Range(0, builder.Context.ScopeDepth - s.TargetStmt.ScopeDepth)) { - builder.Add(new ChangeScope(s.Tok, ChangeScope.Modes.Pop)); - } - var lbl = (s.IsContinue ? "continue_" : "after_") + s.TargetStmt.Labels.Data.AssignUniqueId(CurrentIdGenerator); - builder.Add(new GotoCmd(s.Tok, new List { lbl })); + } else if (stmt is BreakStmt breakStmt) { + TrBreakStmt(builder, etran, breakStmt); } else if (stmt is ReturnStmt returnStmt) { AddComment(builder, returnStmt, "return statement"); if (returnStmt.ReverifyPost) { @@ -410,6 +404,18 @@ void AddResultCommands(BoogieStmtListBuilder returnBuilder, Expression result) { } } + private void TrBreakStmt(BoogieStmtListBuilder builder, ExpressionTranslator etran, BreakStmt breakStmt) + { + AddComment(builder, breakStmt, $"{breakStmt.Kind} statement"); + foreach (var _ in Enumerable.Range(0, builder.Context.ScopeDepth - breakStmt.TargetStmt.ScopeDepth)) { + builder.Add(new ChangeScope(breakStmt.Tok, ChangeScope.Modes.Pop)); + } + var lbl = (breakStmt.IsContinue ? "continue_" : "after_") + breakStmt.TargetStmt.Labels.Data.AssignUniqueId(CurrentIdGenerator); + builder.Add(new GotoCmd(breakStmt.Tok, new List { lbl }) { + Attributes = etran.TrAttributes(breakStmt.Attributes) + }); + } + private void TrUpdateStmt(BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran, AssignStatement statement) { // This UpdateStmt can be single-target assignment, a multi-assignment, a call statement, or // an array-range update. Handle the multi-assignment here and handle the others as for .ResolvedStatements. diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 740f9d8845..98089bb513 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -195,7 +195,7 @@ public async IAsyncEnumerable VerifyAllLazily(int? randomSeed) PathOrigin pathOrigin => $"{pathOrigin.Inner.KindName} at line {pathOrigin.line}, " + $"through [{string.Join(",", pathOrigin.Branches.Select(b => b.tok.line))}]", IsolatedAssertionOrigin isolateOrigin => $"assertion at line {isolateOrigin.line}", - ReturnOrigin returnOrigin => $"return at line {returnOrigin.line}", + JumpOrigin returnOrigin => $"{JumpOriginKind(returnOrigin)} at line {returnOrigin.line}", _ => wellFormedness ? "contract well-formedness" : (hasParts ? "remaining body" : "body") }; @@ -279,6 +279,11 @@ await Options.OutputWriter.WriteLineAsync( } } + private static string JumpOriginKind(JumpOrigin returnOrigin) + { + return returnOrigin.IsolatedReturn is GotoCmd ? "continue" : "return"; + } + public static string DescribeOutcome(VcOutcome outcome) { return outcome switch { VcOutcome.Correct => "verified successfully", diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAssertionOrJump.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAssertionOrJump.dfy index 7eed47e9d9..182dfe15c2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAssertionOrJump.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAssertionOrJump.dfy @@ -1,12 +1,12 @@ -// RUN: ! %verify --progress --cores=1 %s &> %t +// RUN: ! %verify --progress VerificationJobs --cores=1 %s &> %t // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK:Verified 1/2 of Assertion: assertion at line 19, could not prove all assertions // CHECK:Verified 2/2 of Assertion: assertion at line 27, verified successfully -// CHECK:Verified 1/3 of Return: remaining body, could not prove all assertions +// CHECK:Verified 1/3 of Return: body, could not prove all assertions // CHECK:Verified 2/3 of Return: return at line 49, could not prove all assertions // CHECK:Verified 3/3 of Return: return at line 44, could not prove all assertions - - +// CHECK:Verified 1/2 of Continue: body, verified successfully +// CHECK:Verified 2/2 of Continue: continue at line 65, could not prove all assertions method Assertion(x: int, y: int) returns (r: int) { r := 0; if x > 0 @@ -62,7 +62,7 @@ method Continue() { i := i - 1; if (i == 2) { r := r + 2; - continue /*{:isolate}*/; + continue {:isolate}; } else { r := r + 1; } diff --git a/boogie b/boogie index ed1abc9356..ca07b3f8f5 160000 --- a/boogie +++ b/boogie @@ -1 +1 @@ -Subproject commit ed1abc93562dd97a781291d7fd5925cb77340a10 +Subproject commit ca07b3f8f5422375f85e3966de6d6eb1fc0f6a36