feat: continue statements

RELEASE_NOTES.md

@@ -6,8 +6,7 @@
 # 3.4.2
 
 - fix: No output when compiling to JavaScript on Windows (https://github.com/dafny-lang/dafny/pull/1824)
-- fix: CanCall assumptions for loop invariants (https://github.com/dafny-lang/dafny/pull/1813)
-- fix: Behavior of the C# runtime in a concurrent setting (https://github.com/dafny-lang/dafny/pull/1780)
+- feat: `continue` statements. Like Dafny's `break` statements, these come in two forms: one that uses a label to name the continue target and one that specifies the continue target by nesting level. See section 19.2 of the Reference Manual. (https://github.com/dafny-lang/dafny/pull/1839)
 
 
 # 3.4.1

Source/Dafny/AST/DafnyAst.cs

@@ -7187,28 +7187,40 @@ public static string SingleName(Expression e) {
     }
   }
 
+  /// <summary>
+  /// Class "BreakStmt" represents both "break" and "continue" statements.
+  /// </summary>
   public class BreakStmt : Statement {
     public readonly IToken TargetLabel;
-    public readonly int BreakCount;
-    public Statement TargetStmt;  // filled in during resolution
+    public readonly bool IsContinue;
+    public string Kind => IsContinue ? "continue" : "break";
+    public readonly int BreakAndContinueCount;
+    public Statement TargetStmt; // filled in during resolution
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(TargetLabel != null || 1 <= BreakCount);
+      Contract.Invariant(TargetLabel != null || 1 <= BreakAndContinueCount);
     }
 
-    public BreakStmt(IToken tok, IToken endTok, IToken targetLabel)
+    public BreakStmt(IToken tok, IToken endTok, IToken targetLabel, bool isContinue)
       : base(tok, endTok) {
       Contract.Requires(tok != null);
       Contract.Requires(endTok != null);
       Contract.Requires(targetLabel != null);
       this.TargetLabel = targetLabel;
+      this.IsContinue = isContinue;
     }
-    public BreakStmt(IToken tok, IToken endTok, int breakCount)
+
+    /// <summary>
+    /// For "isContinue == false", represents the statement "break ^breakAndContinueCount ;".
+    /// For "isContinue == true", represents the statement "break ^(breakAndContinueCount - 1) continue;".
+    /// </summary>
+    public BreakStmt(IToken tok, IToken endTok, int breakAndContinueCount, bool isContinue)
       : base(tok, endTok) {
       Contract.Requires(tok != null);
       Contract.Requires(endTok != null);
-      Contract.Requires(1 <= breakCount);
-      this.BreakCount = breakCount;
+      Contract.Requires(1 <= breakAndContinueCount);
+      this.BreakAndContinueCount = breakAndContinueCount;
+      this.IsContinue = isContinue;
     }
   }
 

Source/Dafny/AST/Printer.cs

@@ -1205,16 +1205,14 @@ public void PrintStatement(Statement stmt, int indent) {
         wr.Write(";");
 
       } else if (stmt is BreakStmt) {
-        BreakStmt s = (BreakStmt)stmt;
+        var s = (BreakStmt)stmt;
         if (s.TargetLabel != null) {
-          wr.Write("break {0};", s.TargetLabel);
+          wr.Write($"{s.Kind} {s.TargetLabel.val};");
         } else {
-          string sep = "";
-          for (int i = 0; i < s.BreakCount; i++) {
-            wr.Write("{0}break", sep);
-            sep = " ";
+          for (int i = 0; i < s.BreakAndContinueCount - 1; i++) {
+            wr.Write("break ");
           }
-          wr.Write(";");
+          wr.Write($"{s.Kind};");
         }
 
       } else if (stmt is ProduceStmt) {

Source/Dafny/Cloner.cs

@@ -578,9 +578,9 @@ public virtual Statement CloneStmt(Statement stmt) {
       } else if (stmt is BreakStmt) {
         var s = (BreakStmt)stmt;
         if (s.TargetLabel != null) {
-          r = new BreakStmt(Tok(s.Tok), Tok(s.EndTok), s.TargetLabel);
+          r = new BreakStmt(Tok(s.Tok), Tok(s.EndTok), s.TargetLabel, s.IsContinue);
         } else {
-          r = new BreakStmt(Tok(s.Tok), Tok(s.EndTok), s.BreakCount);
+          r = new BreakStmt(Tok(s.Tok), Tok(s.EndTok), s.BreakAndContinueCount, s.IsContinue);
         }
 
       } else if (stmt is ReturnStmt) {

Source/Dafny/Compilers/Compiler-Csharp.cs

@@ -1724,9 +1724,10 @@ protected override void EmitReturn(List<Formal> outParams, ConcreteSyntaxTree wr
       wr.WriteLine($"return {returnExpr};");
     }
 
-    protected override ConcreteSyntaxTree CreateLabeledCode(string label, ConcreteSyntaxTree wr) {
+    protected override ConcreteSyntaxTree CreateLabeledCode(string label, bool createContinueLabel, ConcreteSyntaxTree wr) {
       var w = wr.Fork();
-      wr.Fork(-1).WriteLine($"after_{label}: ;");
+      var prefix = createContinueLabel ? "continue_" : "after_";
+      wr.Fork(-1).WriteLine($"{prefix}{label}: ;");
       return w;
     }
 
@@ -1738,6 +1739,10 @@ protected override void EmitBreak(string/*?*/ label, ConcreteSyntaxTree wr) {
       }
     }
 
+    protected override void EmitContinue(string label, ConcreteSyntaxTree wr) {
+      wr.WriteLine("goto continue_{0};", label);
+    }
+
     protected override void EmitYield(ConcreteSyntaxTree wr) {
       wr.WriteLine("yield return null;");
     }
@@ -1760,7 +1765,7 @@ protected override void EmitHalt(Bpl.IToken tok, Expression/*?*/ messageExpr, Co
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(Bpl.IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
 
       wr.Write($"for ({TypeName(loopIndex.Type, wr, tok)} {loopIndex.CompileName} = ");
       var startWr = wr.Fork();
@@ -1775,6 +1780,7 @@ protected override ConcreteSyntaxTree EmitForStmt(Bpl.IToken tok, IVariable loop
         bodyWr = wr.NewBlock($"; )");
         bodyWr.WriteLine($"{loopIndex.CompileName}--;");
       }
+      bodyWr = EmitContinueLabel(labels, bodyWr);
       TrStmtList(body, bodyWr);
 
       return startWr;

Source/Dafny/Compilers/Compiler-cpp.cs

@@ -1233,9 +1233,10 @@ protected override void EmitReturn(List<Formal> outParams, ConcreteSyntaxTree wr
       }
     }
 
-    protected override ConcreteSyntaxTree CreateLabeledCode(string label, ConcreteSyntaxTree wr) {
+    protected override ConcreteSyntaxTree CreateLabeledCode(string label, bool createContinueLabel, ConcreteSyntaxTree wr) {
       var w = wr.Fork();
-      wr.Fork(-1).WriteLine("after_{0}: ;", label);
+      var prefix = createContinueLabel ? "continue_" : "after_";
+      wr.Fork(-1).WriteLine($"{prefix}{label}: ;");
       return w;
     }
 
@@ -1247,6 +1248,10 @@ protected override void EmitBreak(string/*?*/ label, ConcreteSyntaxTree wr) {
       }
     }
 
+    protected override void EmitContinue(string label, ConcreteSyntaxTree wr) {
+      wr.WriteLine("goto continue_{0};", label);
+    }
+
     protected override void EmitYield(ConcreteSyntaxTree wr) {
       throw NotSupported("EmitYield");
     }
@@ -1269,7 +1274,7 @@ protected override void EmitHalt(Bpl.IToken tok, Expression messageExpr, Concret
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(Bpl.IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
 
       throw new NotImplementedException("for loops have not yet been implemented");
     }
@@ -2376,7 +2381,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
       Contract.Assert(assemblyLocation != null);
       var codebase = System.IO.Path.GetDirectoryName(assemblyLocation);
       Contract.Assert(codebase != null);
-      var warnings = "-Wall -Wextra -Wpedantic -Wno-unused-variable -Wno-deprecated-copy";
+      var warnings = "-Wall -Wextra -Wpedantic -Wno-unused-variable -Wno-deprecated-copy -Wno-unused-label";
       if (RuntimeInformation.IsOSPlatform(OSPlatform.Linux) || RuntimeInformation.IsOSPlatform(OSPlatform.Windows)) {
         warnings += " -Wno-unused-but-set-variable";
       } else {

Source/Dafny/Compilers/Compiler-go.cs

@@ -1779,10 +1779,11 @@ protected void EmitReturnWithCoercions(List<Formal> outParams, List<Formal>/*?*/
       wr.WriteLine();
     }
 
-    protected override ConcreteSyntaxTree CreateLabeledCode(string label, ConcreteSyntaxTree wr) {
+    protected override ConcreteSyntaxTree CreateLabeledCode(string label, bool createContinueLabel, ConcreteSyntaxTree wr) {
       var w = wr.Fork();
-      wr.WriteLine("goto L{0};", label);
-      wr.Fork(-1).WriteLine("L{0}:", label);
+      var prefix = createContinueLabel ? "C" : "L";
+      wr.WriteLine($"goto {prefix}{label};");
+      wr.Fork(-1).WriteLine($"{prefix}{label}:");
       return w;
     }
 
@@ -1794,6 +1795,10 @@ protected override void EmitBreak(string/*?*/ label, ConcreteSyntaxTree wr) {
       }
     }
 
+    protected override void EmitContinue(string label, ConcreteSyntaxTree wr) {
+      wr.WriteLine("goto C{0};", label);
+    }
+
     protected override void EmitYield(ConcreteSyntaxTree wr) {
       wr.WriteLine("_yielded <- struct{}{}");
       wr.WriteLine("_, _ok = <- _cont");
@@ -1826,7 +1831,7 @@ protected override ConcreteSyntaxTree CreateWhileLoop(out ConcreteSyntaxTree gua
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(Bpl.IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
 
       wr.Write($"for {loopIndex.CompileName} := ");
       var startWr = wr.Fork();
@@ -1861,6 +1866,7 @@ protected override ConcreteSyntaxTree EmitForStmt(Bpl.IToken tok, IVariable loop
           bodyWr.WriteLine($"{loopIndex.CompileName}--");
         }
       }
+      bodyWr = EmitContinueLabel(labels, bodyWr);
       TrStmtList(body, bodyWr);
 
       return startWr;

Source/Dafny/Compilers/Compiler-java.cs

@@ -3348,14 +3348,19 @@ protected override string GetCollectionBuilder_Build(CollectionType ct, Bpl.ITok
       }
     }
 
-    protected override ConcreteSyntaxTree CreateLabeledCode(string label, ConcreteSyntaxTree wr) {
-      return wr.NewNamedBlock($"goto_{label}:");
+    protected override ConcreteSyntaxTree CreateLabeledCode(string label, bool createContinueLabel, ConcreteSyntaxTree wr) {
+      var prefix = createContinueLabel ? "continue_" : "goto_";
+      return wr.NewNamedBlock($"{prefix}{label}:");
     }
 
     protected override void EmitBreak(string label, ConcreteSyntaxTree wr) {
       wr.WriteLine(label == null ? "break;" : $"break goto_{label};");
     }
 
+    protected override void EmitContinue(string label, ConcreteSyntaxTree wr) {
+      wr.WriteLine($"break continue_{label};");
+    }
+
     protected override void EmitAbsurd(string message, ConcreteSyntaxTree wr) {
       if (message == null) {
         message = "unexpected control point";
@@ -3524,7 +3529,7 @@ protected override ConcreteSyntaxTree CreateForLoop(string indexVar, string boun
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(Bpl.IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
 
       var nativeType = AsNativeType(loopIndex.Type);
 
@@ -3565,6 +3570,7 @@ protected override ConcreteSyntaxTree EmitForStmt(Bpl.IToken tok, IVariable loop
           bodyWr.WriteLine($"{loopIndex.CompileName}--;");
         }
       }
+      bodyWr = EmitContinueLabel(labels, bodyWr);
       TrStmtList(body, bodyWr);
 
       return startWr;

Source/Dafny/Compilers/Compiler-js.cs

@@ -1103,8 +1103,9 @@ protected override void EmitReturn(List<Formal> outParams, ConcreteSyntaxTree wr
       }
     }
 
-    protected override ConcreteSyntaxTree CreateLabeledCode(string label, ConcreteSyntaxTree wr) {
-      return wr.NewNamedBlock("L{0}:", label);
+    protected override ConcreteSyntaxTree CreateLabeledCode(string label, bool createContinueLabel, ConcreteSyntaxTree wr) {
+      var prefix = createContinueLabel ? "C" : "L";
+      return wr.NewNamedBlock($"{prefix}{label}:");
     }
 
     protected override void EmitBreak(string/*?*/ label, ConcreteSyntaxTree wr) {
@@ -1115,6 +1116,10 @@ protected override void EmitBreak(string/*?*/ label, ConcreteSyntaxTree wr) {
       }
     }
 
+    protected override void EmitContinue(string label, ConcreteSyntaxTree wr) {
+      wr.WriteLine("break C{0};", label);
+    }
+
     protected override void EmitYield(ConcreteSyntaxTree wr) {
       wr.WriteLine("yield null;");
     }
@@ -1137,7 +1142,7 @@ protected override void EmitHalt(Bpl.IToken tok, Expression/*?*/ messageExpr, Co
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(Bpl.IToken tok, IVariable loopIndex, bool goingUp, string /*?*/ endVarName,
-      List<Statement> body, ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
 
       var nativeType = AsNativeType(loopIndex.Type);
 
@@ -1174,6 +1179,7 @@ protected override ConcreteSyntaxTree EmitForStmt(Bpl.IToken tok, IVariable loop
           bodyWr.WriteLine($"{loopIndex.CompileName}--;");
         }
       }
+      bodyWr = EmitContinueLabel(labels, bodyWr);
       TrStmtList(body, bodyWr);
 
       return startWr;

Source/Dafny/Compilers/Compiler-python.cs

@@ -289,14 +289,18 @@ protected override void EmitReturn(List<Formal> outParams, ConcreteSyntaxTree wr
       throw new NotImplementedException();
     }
 
-    protected override ConcreteSyntaxTree CreateLabeledCode(string label, ConcreteSyntaxTree wr) {
+    protected override ConcreteSyntaxTree CreateLabeledCode(string label, bool createContinueLabel, ConcreteSyntaxTree wr) {
       throw new NotImplementedException();
     }
 
     protected override void EmitBreak(string label, ConcreteSyntaxTree wr) {
       throw new NotImplementedException();
     }
 
+    protected override void EmitContinue(string label, ConcreteSyntaxTree wr) {
+      throw new NotImplementedException();
+    }
+
     protected override void EmitYield(ConcreteSyntaxTree wr) {
       throw new NotImplementedException();
     }
@@ -310,8 +314,7 @@ protected override void EmitHalt(IToken tok, Expression messageExpr, ConcreteSyn
     }
 
     protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopIndex, bool goingUp, string endVarName,
-      List<Statement> body,
-      ConcreteSyntaxTree wr) {
+      List<Statement> body, LList<Label> labels, ConcreteSyntaxTree wr) {
       throw new NotImplementedException();
     }