-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: continue statements #1839
feat: continue statements #1839
Conversation
By generating just “break;” rather than a labeled break/goto for `while *` loops.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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/Resolver.cs
Outdated
} 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"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 ofbreak
before the
continue
keyword, then the statement must be enclosed in at leastn + 1
levels
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks. I improved the messages along the lines you suggested. See if you like them better now.
foreach (var resolved in s.ResolvedStatements) { | ||
TrStmt(resolved, builder, locals, etran); | ||
} | ||
TrStmtList(s.ResolvedStatements, builder, locals, etran); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Very good refactoring
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
And, in fact, fixing the code, too! It turns out that TrStmtList
processes labels, whereas TrStmt
does not.
docs/DafnyRef/Statements.md
Outdated
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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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"
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
.
DoSomething(n); | ||
} | ||
``` | ||
is equivalent to | ||
```dafny | ||
{ | ||
var n: ReadNext(); | ||
var n := ReadNext(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yay for fixing this typo
| "continue" LabelName ";" | ||
| { "break" } "break" ";" | ||
| { "break" } "continue" ";" | ||
) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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".
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good suggestion.
Co-authored-by: Fabio Madge <fabio@madge.me>
…dafny into issue-1738-continue
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just a possible infinite loop to fix, otherwise we good to go !
Source/Dafny/Resolver.cs
Outdated
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"; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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".
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I renamed BreakCount
to BreakAndContinueCount
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm happy with those changes.
Source/Dafny/Resolver.cs
Outdated
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"; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm happy with those changes.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think we can remove the comment now since the variable is self-explaining.
Otherwise, looks good !
Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>
This PR adds
continue
statements, in the two forms analogous to the two forms ofbreak
statements:The statement
continue L;
causes control flow to jump to the very end of the current iteration of the enclosing loop labeledL
. The statementbreak ... break continue;
with n occurrences ofbreak
(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