Add support for isolate on continue statements

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;".
   /// </summary>
-  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;

Source/DafnyCore/Dafny.atg

@@ -2264,8 +2264,10 @@ BreakStmt<out Statement/*!*/ s>
      IToken start = Token.NoToken;
      IToken label = null;
      int breakAndContinueCount = 1;
+     Attributes attributes = null;
   .)
   ( "continue"              (. start = t; isContinue = true; .)
+    [ Attribute<ref attributes> ]
     [ LabelName<out label> ]
   | "break"                 (. start = t; .)
     ( LabelName<out label>
@@ -2280,7 +2282,7 @@ BreakStmt<out Statement/*!*/ s>
   (. 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);
   .)
   .
 

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<string> { 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<string> { 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.

Source/DafnyDriver/CliCompilation.cs

@@ -195,7 +195,7 @@ public async IAsyncEnumerable<CanVerifyResult> 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",

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;
     }