feat: continue statements #1839

RustanLeino · 2022-02-18T04:10:14Z

This PR adds continue statements, in the two forms analogous to the two forms of break statements:

ContinueStmt ::=
  | "continue" LabelName ";"
  | { "break" } "continue" ";"

The statement continue L; causes control flow to jump to the very end of the current iteration of the enclosing loop labeled L. The statement break ... break continue; with n occurrences of break (where n is 0 or more) breaks out of n loops and then ends the current iteration.

For more details, see docs/DafnyRef/Statements.md.

Fixes #1738

By generating just “break;” rather than a labeled break/goto for `while *` loops.

MikaelMayer

Wonderful natural integration of continue in the Dafny language, with the break statement. Brilliant and useful.
A few comments to address, otherwise it looks good !

Source/Dafny/Compilers/Compiler.cs

MikaelMayer · 2022-02-18T15:58:02Z

Source/Dafny/Resolver.cs

 } else {
 s.TargetStmt = target;
 }
 } else {
 if (loopStack.Count < s.BreakCount) {
- reporter.Error(MessageSource.Resolver, s, "trying to break out of more loop levels than there are enclosing loops");
+ var jump = s.IsContinue && s.BreakCount != 1 ? "break/continue" : s.Kind;
+ reporter.Error(MessageSource.Resolver, s, $"trying to {jump} out of more loop levels than there are enclosing loops");


The sentence for 'continue' would be disturbing: "Trying to continue out of more loop levels than there are enclosing loops", since we don't usually "continue out of a loop".
Consider rephrasing it to more precise messages, depending on the value of loopStack and s.breakCount, such as the following

(loopStack.count, breakCount, isContinue) switch { (0, 0, true) => "continue statements are only allowed inside loops" (0, n, true) => "break ... continue statements are only allowed inside loops" (l, b, false) => "Expected at most {l} 'break' because there are {l} enclosing loops, but got {b} (l, b, true) => "Expected at most {l - 1} 'break' before 'continue' because there are {l} enclosing loops, but got {b} }

Also, I think that isContinue == 1 should add 1 to the number to test against loopStack.Count in the guard. Am I right?

If a non-labeled continue statement lists n occurrences of break before the
continue keyword, then the statement must be enclosed in at least n + 1 levels

Thanks. I improved the messages along the lines you suggested. See if you like them better now.

MikaelMayer · 2022-02-18T15:58:38Z

Source/Dafny/Verifier/Translator.TrStatement.cs

- foreach (var resolved in s.ResolvedStatements) {
- TrStmt(resolved, builder, locals, etran);
- }
+ TrStmtList(s.ResolvedStatements, builder, locals, etran);


Very good refactoring

And, in fact, fixing the code, too! It turns out that TrStmtList processes labels, whereas TrStmt does not.

MikaelMayer · 2022-02-18T16:07:08Z

docs/DafnyRef/Statements.md

+mentions the label must be _enclosed_ in the labeled statement.
+The label may also be used in an `old` expression ([Section 20.24](#sec-old-expression)). In this case, the label
+must have been encountered during the control flow en route to the `old`
+expression, which is to say the label must _dominate_ the use of the label.


which is to say the label must dominate the use of the label.

What about the following suggestion to clearly mention it's a definition:

We say in this case that the label "dominates" the use of the label

I'm a bit puzzled by the word "dominate" since I never saw it before in such a context. Would it be possible to replace it by "must lead"? Then, afterwards, you'd be able to talk about the "any leading label"

I improved the wording along your suggestion, and also tried to be more clear about "dominates".

The word "dominates" is used in the Dragon Book ("Compilers" by Aho et al.). A program point (or basic block) A dominates a program point (or basic block) B when the only way to get to B is via A.

MikaelMayer · 2022-02-18T16:15:32Z

docs/DafnyRef/Statements.md

 DoSomething(n);
 }
 ```
 is equivalent to
 ```dafny
 {
- var n: ReadNext();
+ var n := ReadNext();


Yay for fixing this typo

MikaelMayer · 2022-02-18T16:18:19Z

docs/DafnyRef/Statements.md

+ | "continue" LabelName ";"
+ | { "break" } "break" ";"
+ | { "break" } "continue" ";"
+ )


Can you mention somewhere that break, break continue and other variants will not be able to check the loop invariants? I think that could be useful.
It might also apply for "continue label".

Good suggestion.

RELEASE_NOTES.md

Co-authored-by: Fabio Madge <[email protected]>

…dafny into issue-1738-continue

MikaelMayer

Just a possible infinite loop to fix, otherwise we good to go !

MikaelMayer · 2022-02-18T21:54:49Z

Source/Dafny/Resolver.cs

- reporter.Error(MessageSource.Resolver, s, $"trying to {jump} out of more loop levels than there are enclosing loops");
+ var jumpStmt = s.BreakCount == 1 ?
+ $"a non-labeled '{s.Kind}' statement" :
+ $"a '{Util.Repeat(s.BreakCount - 1, "break ")}{s.Kind}' statement";


s.BreakCount might be zero at this stage, which could trigger an infinite loop. Consider either testing it or changing Repeat so that 0 or -1 are considered the same.

I disagree. There's an invariant in class BreakStmt that says

Contract.Invariant(TargetLabel != null || 1 <= BreakCount);

and the if statement surrounding the assignment to jumpStmt ensures that this code is used only when s.TargetLabel == null.

The count s.BreakCount include the final continue. So, the name of this field is not the best. Would BreakContinueCount or Levels be more readily understood?

Good argument. I can't see the surrounding block in GitHub because the file is too large, so I couldn't have had this assumption, I'm just watching over your shoulder :-)
However, while debugging Dafny, I have seen surprisingly many times invariants which did not hold but the code did not crash. It looks like the invariants are not checked (how odd), and I wouldn't be surprised if some refactoring down the road silently breaks such an invariant.
My not-so-strong opinion is that, until we migrate our codebase to Dafny, it is better not to rely on contracts. Changing a == 0 to a <= 0 seems like a very minor change that would it even more easily to reason locally.
If you prefer not to do that change, at least put a comment recalling the BreakStmt invariant on the else branch.

About the variable name, I think it would be better to have it meaning what it does, since It's a public API: breakCount looks instinctively like the number of times the word "break" appears. "level" might thus be more appropriate, but you could as well name it explicitly "SurroundingLoopLevelTarget".

Unfortunately, Contract.Invariant, Contract.Requires, and Contract.Ensures contracts are not checked at run time, so it happens they are out of date or that bugs in the code are missed. Still, they often express the intent, and in this case the intent can be checked manually at least back to the constructor. For the particular code in this PR, I added a Contract.Assert (which is checked at run time in our DEBUG build) at this source location. I also added a comment that describes why I expect the asserted condition to hold.

I renamed BreakCount to BreakAndContinueCount.

I'm happy with those changes.

# Conflicts: # RELEASE_NOTES.md

Source/Dafny/AST/DafnyAst.cs

MikaelMayer · 2022-02-22T17:03:27Z

Source/Dafny/Resolver.cs

- reporter.Error(MessageSource.Resolver, s, $"trying to {jump} out of more loop levels than there are enclosing loops");
+ var jumpStmt = s.BreakCount == 1 ?
+ $"a non-labeled '{s.Kind}' statement" :
+ $"a '{Util.Repeat(s.BreakCount - 1, "break ")}{s.Kind}' statement";


I'm happy with those changes.

MikaelMayer

I think we can remove the comment now since the variable is self-explaining.
Otherwise, looks good !

Co-authored-by: Mikaël Mayer <[email protected]>

RustanLeino added 10 commits February 16, 2022 22:00

Parse and print

d710d93

Resolve

db5dbf9

Verify

0bcfe24

fix: Labeled-statement regressions

d83bd68

Compile

c7810d6

Don’t warn about unused C++ labels

46e9549

Simplify target code

364d5ad

By generating just “break;” rather than a labeled break/goto for `while *` loops.

Document

bceb32a

Remove whitespace

a3b82fe

Merge branch 'master' into issue-1738-continue

1241fde

MikaelMayer requested changes Feb 18, 2022

View reviewed changes

Add release notes

22356c9

fabiomadge reviewed Feb 18, 2022

View reviewed changes

RELEASE_NOTES.md Outdated Show resolved Hide resolved

RustanLeino and others added 7 commits February 18, 2022 11:07

Improve error messages

cf43bd6

Improve wording in documentation

31a40ee

Explain that loop invariants are not checked at break/continue

e32af49

Update RELEASE_NOTES.md

617063e

Co-authored-by: Fabio Madge <[email protected]>

Merge branch 'issue-1738-continue' of https://github.com/RustanLeino/…

bed7e41

…dafny into issue-1738-continue

Fix whitespace

60a0846

Merge branch 'master' into issue-1738-continue

b563fab

MikaelMayer requested changes Feb 18, 2022

View reviewed changes

RustanLeino added 3 commits February 21, 2022 11:33

chore: Rename BreakCount to BreakAndContinueCount

62c6f70

Assert condition that should hold from class invariant

89e3227

Merge branch 'master' into issue-1738-continue

caaa60a

# Conflicts: # RELEASE_NOTES.md

RustanLeino enabled auto-merge (squash) February 21, 2022 19:43

MikaelMayer reviewed Feb 22, 2022

View reviewed changes

MikaelMayer previously approved these changes Feb 22, 2022

View reviewed changes

Update Source/Dafny/AST/DafnyAst.cs

e10fb7c

Co-authored-by: Mikaël Mayer <[email protected]>

RustanLeino dismissed MikaelMayer’s stale review via e10fb7c February 22, 2022 18:03

Merge branch 'master' into issue-1738-continue

a1e2430

MikaelMayer approved these changes Feb 22, 2022

View reviewed changes

RustanLeino merged commit 6c9e621 into dafny-lang:master Feb 22, 2022

RustanLeino deleted the issue-1738-continue branch February 22, 2022 20:08

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: continue statements #1839

feat: continue statements #1839

RustanLeino commented Feb 18, 2022

MikaelMayer left a comment

MikaelMayer Feb 18, 2022

RustanLeino Feb 18, 2022

MikaelMayer Feb 18, 2022

RustanLeino Feb 18, 2022

MikaelMayer Feb 18, 2022

RustanLeino Feb 18, 2022

MikaelMayer Feb 18, 2022

MikaelMayer Feb 18, 2022

RustanLeino Feb 18, 2022

MikaelMayer left a comment

MikaelMayer Feb 18, 2022

RustanLeino Feb 18, 2022

MikaelMayer Feb 21, 2022

MikaelMayer Feb 21, 2022

RustanLeino Feb 21, 2022

RustanLeino Feb 21, 2022

MikaelMayer Feb 22, 2022

MikaelMayer Feb 22, 2022

MikaelMayer left a comment

feat: continue statements #1839

feat: continue statements #1839

Conversation

RustanLeino commented Feb 18, 2022

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment