Alternate translation of do-while-block to avoid or (||) short circuiting#158
Merged
Conversation
Contributor
|
Please rebase to main. Otherwise lgtm. |
Previously `do { body } while (cond)` was always desugared to
`bool first = true; while (first || cond) { first = false; body; }`.
This adds a cleaner desugaring used when the do-body contains no
top-level `continue` (continues inside a nested for/while/do-while are
excluded via hasTopLevelContinue, which treats loops as boundaries but
descends into if/switch/blocks/labels):
bool cont = true; bool first = true;
while (cont) { body; first = false; cont = cond; }
An internal `cont` flag drives the loop; a separate `first` flag (named
by _do_while_first) preserves first-iteration semantics for invariants.
To keep loops whose body relies on the loop condition verifiable, we
auto-inject the invariant `cont == (first || cond)` plus `_live(cont)`.
When a top-level `continue` is present, we fall back to the original
desugaring unchanged. Both paths now save/restore forLoopIncrement
around body translation.
Adds test/do_while_nested_continue exercising the new path with a
continue nested in an inner loop.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Move the nested-loop-continue example into test/do_while as a new `nested_continue` function instead of a standalone test folder, keeping all do-while desugaring cases together. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The clean do-while desugaring auto-injects `cont == (first || cond)` as a
`with_pure` loop invariant. When the guard `cond` has side effects (e.g.
`do { ... } while (f());` with a bool-returning function `f`), embedding
it in a pure invariant is rejected by F* (Error 228, "Cannot use ... in
impure spec").
Gate the linking invariant on `!cond->HasSideEffects(astCtx)`: for an
impure guard we omit it entirely. `cont` already holds the guard's most
recent value (assigned at the end of the body), which is all an impure
guard can convey; there is no pure fact to state.
Adds `f` + `g_loop` (function-call guard, empty body) to test/do_while,
ported from ../loopback-new/pal-tests/bool_call.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…an impure function in the guard
Contributor
|
Please fix the PR title and then feel free to merge! |
hei411
changed the title
hei411
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is a pull request making changes to the do-while loop. Changes and design choices are a bit subtle, which I describe below:
Originally a do while block of the form
do {body} while(cond)is translated tobool first = true; while (first || cond){ body; first = false; }.This is troublesome since
||does not support short-circuiting. F* also complains a lot whencondperforms external stateful function calls.Instead, we translate the do while block to
bool cont = true; bool first = true; while (cont) { body; cont = cond; first = false; }firstas before for backwards compatibility.continuein the top level. Otherwise, we fall back to the original translation._do_while_first, we add a PAL annotation_do_while_condto refer tocontfor defining invariantscont==first||condifcondis pure. This is also used to support backwards compatibility.