From 4f19c6c7b8919a3042ad689a6b23fac364568b16 Mon Sep 17 00:00:00 2001 From: t-heili Date: Wed, 1 Jul 2026 12:46:53 -0700 Subject: [PATCH 1/6] Add clean do-while desugaring when body has no top-level continue 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> --- cpp/impl.cpp | 133 +++++++++++++++--- test/do_while_nested_continue/Makefile | 1 + .../do_while_nested_continue.c | 32 +++++ .../fstar.fst.config.json | 1 + test/do_while_nested_continue/pal.config.json | 1 + test/do_while_nested_continue/pal.h | 1 + 6 files changed, 152 insertions(+), 17 deletions(-) create mode 120000 test/do_while_nested_continue/Makefile create mode 100644 test/do_while_nested_continue/do_while_nested_continue.c create mode 120000 test/do_while_nested_continue/fstar.fst.config.json create mode 120000 test/do_while_nested_continue/pal.config.json create mode 120000 test/do_while_nested_continue/pal.h diff --git a/cpp/impl.cpp b/cpp/impl.cpp index 082df1d6..b864ee5b 100644 --- a/cpp/impl.cpp +++ b/cpp/impl.cpp @@ -35,6 +35,24 @@ Ref toStr(std::string const &str) { return str_from_parts((uint8_t const *)str.data(), str.size()); } +// Returns true if `s` contains a `continue` that binds to the enclosing loop, +// i.e. a `continue` that is not nested inside another loop. Nested `for`, +// `while`, and `do-while` loops act as boundaries (their `continue` belongs to +// them), so we do not descend into them. A `switch` does NOT capture `continue` +// in C, so we descend into it (and into `if`, blocks, labels, etc.). +static bool hasTopLevelContinue(const Stmt *s) { + if (!s) + return false; + if (isa(s)) + return true; + if (isa(s) || isa(s) || isa(s)) + return false; + for (const Stmt *child : s->children()) + if (hasTopLevelContinue(child)) + return true; + return false; +} + using SnipMap = rust::pal::hauntedc::SnippetMap; using TargetIntWidths = rust::pal::hauntedc::TargetIntWidths; @@ -1258,10 +1276,15 @@ class PALConsumer : public ASTConsumer { std::move(invs), std::move(reqs), std::move(enss), std::move(bodyStmts))); } else if (auto *d = dyn_cast(stmt)) { - // Desugar: do { body } while (cond) - // --> bool flag = true; - // while (flag || cond) { flag = false; body; } - // If _do_while_first(name) is provided, use that name for the flag. + // Desugar `do { body } while (cond)`. If the body has no top-level + // `continue` we use the "clean" desugaring: + // --> bool cont = true; bool first = true; + // while (cont) { body; first = false; cont = cond; } + // Otherwise (a top-level `continue` would skip the trailing `cont = cond` + // update) we fall back to the legacy desugaring: + // --> bool first = true; + // while (first || cond) { first = false; body; } + // In both cases `_do_while_first(name)` names the first-iteration flag. // Extract annotations and check for _do_while_first auto body = d->getBody(); @@ -1290,39 +1313,115 @@ class PALConsumer : public ASTConsumer { body = attrBody->getSubStmt(); } - if (flagName.empty()) { + // First-iteration flag: named by _do_while_first, else auto-generated. + // Its + // `_live` invariant is auto-injected only when the name is auto-generated + // (a user-named flag is expected to be mentioned in the user's + // invariant). + bool firstIsAuto = flagName.empty(); + if (firstIsAuto) { static int doCounter = 0; flagName = "__do_first_" + std::to_string(doCounter++); } - auto flagId = ctx.mk_ident(toStr(flagName), loc.clone()); + auto firstId = ctx.mk_ident(toStr(flagName), loc.clone()); + + if (!hasTopLevelContinue(body)) { + // Clean desugaring: no top-level `continue`. + static int doContCounter = 0; + std::string contName = "__do_cont_" + std::to_string(doContCounter++); + auto contId = ctx.mk_ident(toStr(contName), loc.clone()); + + // bool cont; cont = true; + stmts.push(mk_var_decl(loc.clone(), contId.clone(), + mk_bool_type(loc.clone()))); + stmts.push(mk_assign(loc.clone(), + mk_lvalue_var(loc.clone(), contId.clone()), + mk_bool_lit(loc.clone(), true))); + // bool first; first = true; + stmts.push(mk_var_decl(loc.clone(), firstId.clone(), + mk_bool_type(loc.clone()))); + stmts.push(mk_assign(loc.clone(), + mk_lvalue_var(loc.clone(), firstId.clone()), + mk_bool_lit(loc.clone(), true))); + + // while condition: cont + auto whileCond = mk_rvalue_lvalue( + loc.clone(), mk_lvalue_var(loc.clone(), contId.clone())); + + // Always inject _live(cont) (internal flag), and _live(first) when the + // first flag was auto-generated. + invs.push( + mk_live(loc.clone(), mk_lvalue_var(loc.clone(), contId.clone()))); + if (firstIsAuto) { + invs.push(mk_live(loc.clone(), + mk_lvalue_var(loc.clone(), firstId.clone()))); + } + + // Link the internal `cont` flag to the loop condition so the body knows + // `cond` holds on re-entry (the guard `while (cont)` alone conveys + // nothing to the solver). We inject: + // cont == (first || cond) + { + auto firstRead = mk_rvalue_lvalue( + loc.clone(), mk_lvalue_var(loc.clone(), firstId.clone())); + auto contReadInv = mk_rvalue_lvalue( + loc.clone(), mk_lvalue_var(loc.clone(), contId.clone())); + auto firstOrCond = + mk_rvalue_binop(loc.clone(), ir::BinOp::LogOr(), + std::move(firstRead), trRValue(d->getCond())); + invs.push(mk_rvalue_binop(loc.clone(), ir::BinOp::Eq(), + std::move(contReadInv), + std::move(firstOrCond))); + } - // bool flag; flag = true; + // Build body: original_body; first = false; cont = cond; + auto bodyStmts = Vec>::new_(); + auto savedIncrement = forLoopIncrement; + forLoopIncrement = nullptr; + trStmt(bodyStmts, body); + forLoopIncrement = savedIncrement; + bodyStmts.push(mk_assign(loc.clone(), + mk_lvalue_var(loc.clone(), firstId.clone()), + mk_bool_lit(loc.clone(), false))); + bodyStmts.push(mk_assign(loc.clone(), + mk_lvalue_var(loc.clone(), contId.clone()), + trRValue(d->getCond()))); + + return stmts.push(mk_while(std::move(loc), std::move(whileCond), + std::move(invs), std::move(reqs), + std::move(enss), std::move(bodyStmts))); + } + + // Legacy desugaring: body has a top-level `continue`. + // bool first; first = true; stmts.push( - mk_var_decl(loc.clone(), flagId.clone(), mk_bool_type(loc.clone()))); + mk_var_decl(loc.clone(), firstId.clone(), mk_bool_type(loc.clone()))); stmts.push(mk_assign(loc.clone(), - mk_lvalue_var(loc.clone(), flagId.clone()), + mk_lvalue_var(loc.clone(), firstId.clone()), mk_bool_lit(loc.clone(), true))); - // while condition: flag || cond + // while condition: first || cond auto flagRead = mk_rvalue_lvalue( - loc.clone(), mk_lvalue_var(loc.clone(), flagId.clone())); + loc.clone(), mk_lvalue_var(loc.clone(), firstId.clone())); auto whileCond = mk_rvalue_binop(loc.clone(), ir::BinOp::LogOr(), std::move(flagRead), trRValue(d->getCond())); - // Add _live(flag) to invariants (skip if user provided _do_while_first, - // since user is expected to include it in their own invariant) - if (flagName.find("__do_first_") == 0) { + // Add _live(first) to invariants when the name is auto-generated. + if (firstIsAuto) { invs.push( - mk_live(loc.clone(), mk_lvalue_var(loc.clone(), flagId.clone()))); + mk_live(loc.clone(), mk_lvalue_var(loc.clone(), firstId.clone()))); } - // Build body: flag = false; original_body; + // Build body: first = false; original_body; auto bodyStmts = Vec>::new_(); bodyStmts.push(mk_assign(loc.clone(), - mk_lvalue_var(loc.clone(), flagId.clone()), + mk_lvalue_var(loc.clone(), firstId.clone()), mk_bool_lit(loc.clone(), false))); + auto savedIncrement = forLoopIncrement; + forLoopIncrement = nullptr; trStmt(bodyStmts, body); + forLoopIncrement = savedIncrement; return stmts.push(mk_while(std::move(loc), std::move(whileCond), std::move(invs), std::move(reqs), diff --git a/test/do_while_nested_continue/Makefile b/test/do_while_nested_continue/Makefile new file mode 120000 index 00000000..3febeb16 --- /dev/null +++ b/test/do_while_nested_continue/Makefile @@ -0,0 +1 @@ +../_templates/Makefile \ No newline at end of file diff --git a/test/do_while_nested_continue/do_while_nested_continue.c b/test/do_while_nested_continue/do_while_nested_continue.c new file mode 100644 index 00000000..db99ee51 --- /dev/null +++ b/test/do_while_nested_continue/do_while_nested_continue.c @@ -0,0 +1,32 @@ +#include "pal.h" +#include + +/* The `continue` here binds to the *inner* while loop, so the outer do-while + * body has no top-level `continue`. This exercises the clean do-while + * desugaring (`bool cont = true; while (cont) { body; first = false; + * cont = cond; }`) rather than the legacy fallback, while still proving that a + * nested-loop `continue` is correctly excluded by the top-level scan. */ +uint32_t nested_continue(uint32_t n) + _requires(n >= 1 && n <= 100) +{ + uint32_t i = 0; + do + _do_while_first(first) + _invariant(_live(i) && _live(n) && _live(first)) + _invariant(first ==> (_specint) i < n) + _invariant((_specint) i <= n) + { + uint32_t j = 0; + while (j < 3) + _invariant(_live(j)) + _invariant((_specint) j <= 3) + { + j = j + 1; + if (j == 2) { + continue; + } + } + i = i + 1; + } while (i < n); + return i; +} diff --git a/test/do_while_nested_continue/fstar.fst.config.json b/test/do_while_nested_continue/fstar.fst.config.json new file mode 120000 index 00000000..4100b019 --- /dev/null +++ b/test/do_while_nested_continue/fstar.fst.config.json @@ -0,0 +1 @@ +../_templates/fstar.fst.config.json \ No newline at end of file diff --git a/test/do_while_nested_continue/pal.config.json b/test/do_while_nested_continue/pal.config.json new file mode 120000 index 00000000..d59f1cfa --- /dev/null +++ b/test/do_while_nested_continue/pal.config.json @@ -0,0 +1 @@ +../_templates/pal.config.json \ No newline at end of file diff --git a/test/do_while_nested_continue/pal.h b/test/do_while_nested_continue/pal.h new file mode 120000 index 00000000..05ef83f9 --- /dev/null +++ b/test/do_while_nested_continue/pal.h @@ -0,0 +1 @@ +../pal.h \ No newline at end of file From f64270e7049d685f352e6b2a0cf6e1ee932b33a7 Mon Sep 17 00:00:00 2001 From: t-heili Date: Wed, 1 Jul 2026 12:50:12 -0700 Subject: [PATCH 2/6] Fold nested_continue case into do_while test 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> --- test/do_while/do_while.c | 30 +++++++++++++++++ test/do_while_nested_continue/Makefile | 1 - .../do_while_nested_continue.c | 32 ------------------- .../fstar.fst.config.json | 1 - test/do_while_nested_continue/pal.config.json | 1 - test/do_while_nested_continue/pal.h | 1 - 6 files changed, 30 insertions(+), 36 deletions(-) delete mode 120000 test/do_while_nested_continue/Makefile delete mode 100644 test/do_while_nested_continue/do_while_nested_continue.c delete mode 120000 test/do_while_nested_continue/fstar.fst.config.json delete mode 120000 test/do_while_nested_continue/pal.config.json delete mode 120000 test/do_while_nested_continue/pal.h diff --git a/test/do_while/do_while.c b/test/do_while/do_while.c index ebad446a..5068bd4c 100644 --- a/test/do_while/do_while.c +++ b/test/do_while/do_while.c @@ -71,3 +71,33 @@ uint32_t count_odd(uint32_t n) } while (i < n); return count; } + +/* do-while whose only `continue` binds to the *inner* while loop, so the outer + * do-while body has no top-level `continue`. This exercises the clean do-while + * desugaring (`bool cont = true; while (cont) { body; first = false; + * cont = cond; }`) rather than the legacy fallback, while still proving that a + * nested-loop `continue` is correctly excluded by the top-level scan. */ +uint32_t nested_continue(uint32_t n) + _requires(n >= 1 && n <= 100) +{ + uint32_t i = 0; + do + _do_while_first(first) + _invariant(_live(i) && _live(n) && _live(first)) + _invariant(first ==> (_specint) i < n) + _invariant((_specint) i <= n) + { + uint32_t j = 0; + while (j < 3) + _invariant(_live(j)) + _invariant((_specint) j <= 3) + { + j = j + 1; + if (j == 2) { + continue; + } + } + i = i + 1; + } while (i < n); + return i; +} diff --git a/test/do_while_nested_continue/Makefile b/test/do_while_nested_continue/Makefile deleted file mode 120000 index 3febeb16..00000000 --- a/test/do_while_nested_continue/Makefile +++ /dev/null @@ -1 +0,0 @@ -../_templates/Makefile \ No newline at end of file diff --git a/test/do_while_nested_continue/do_while_nested_continue.c b/test/do_while_nested_continue/do_while_nested_continue.c deleted file mode 100644 index db99ee51..00000000 --- a/test/do_while_nested_continue/do_while_nested_continue.c +++ /dev/null @@ -1,32 +0,0 @@ -#include "pal.h" -#include - -/* The `continue` here binds to the *inner* while loop, so the outer do-while - * body has no top-level `continue`. This exercises the clean do-while - * desugaring (`bool cont = true; while (cont) { body; first = false; - * cont = cond; }`) rather than the legacy fallback, while still proving that a - * nested-loop `continue` is correctly excluded by the top-level scan. */ -uint32_t nested_continue(uint32_t n) - _requires(n >= 1 && n <= 100) -{ - uint32_t i = 0; - do - _do_while_first(first) - _invariant(_live(i) && _live(n) && _live(first)) - _invariant(first ==> (_specint) i < n) - _invariant((_specint) i <= n) - { - uint32_t j = 0; - while (j < 3) - _invariant(_live(j)) - _invariant((_specint) j <= 3) - { - j = j + 1; - if (j == 2) { - continue; - } - } - i = i + 1; - } while (i < n); - return i; -} diff --git a/test/do_while_nested_continue/fstar.fst.config.json b/test/do_while_nested_continue/fstar.fst.config.json deleted file mode 120000 index 4100b019..00000000 --- a/test/do_while_nested_continue/fstar.fst.config.json +++ /dev/null @@ -1 +0,0 @@ -../_templates/fstar.fst.config.json \ No newline at end of file diff --git a/test/do_while_nested_continue/pal.config.json b/test/do_while_nested_continue/pal.config.json deleted file mode 120000 index d59f1cfa..00000000 --- a/test/do_while_nested_continue/pal.config.json +++ /dev/null @@ -1 +0,0 @@ -../_templates/pal.config.json \ No newline at end of file diff --git a/test/do_while_nested_continue/pal.h b/test/do_while_nested_continue/pal.h deleted file mode 120000 index 05ef83f9..00000000 --- a/test/do_while_nested_continue/pal.h +++ /dev/null @@ -1 +0,0 @@ -../pal.h \ No newline at end of file From 94c9a1ec01d5cdd3c54b2e820e3a475327a4ad32 Mon Sep 17 00:00:00 2001 From: t-heili Date: Wed, 1 Jul 2026 13:02:21 -0700 Subject: [PATCH 3/6] Omit do-while linking invariant for impure guards; add g_loop test 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> --- cpp/impl.cpp | 9 ++++++++- test/do_while/do_while.c | 26 ++++++++++++++++++++++++++ 2 files changed, 34 insertions(+), 1 deletion(-) diff --git a/cpp/impl.cpp b/cpp/impl.cpp index b864ee5b..74752678 100644 --- a/cpp/impl.cpp +++ b/cpp/impl.cpp @@ -1361,7 +1361,14 @@ class PALConsumer : public ASTConsumer { // `cond` holds on re-entry (the guard `while (cont)` alone conveys // nothing to the solver). We inject: // cont == (first || cond) - { + // + // This is only sound to emit when `cond` is a *pure* expression: the + // invariant is a `with_pure` proposition, so an impure guard (e.g. a + // function call like `while (f())`) cannot appear in it. When the guard + // has side effects we omit the linking invariant 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. + if (!d->getCond()->HasSideEffects(*astCtx)) { auto firstRead = mk_rvalue_lvalue( loc.clone(), mk_lvalue_var(loc.clone(), firstId.clone())); auto contReadInv = mk_rvalue_lvalue( diff --git a/test/do_while/do_while.c b/test/do_while/do_while.c index 5068bd4c..1b8a36c8 100644 --- a/test/do_while/do_while.c +++ b/test/do_while/do_while.c @@ -1,5 +1,6 @@ #include "pal.h" #include +#include /* do-while with user-named flag variable for first-iteration invariant */ uint32_t simple_do(uint32_t n) @@ -101,3 +102,28 @@ uint32_t nested_continue(uint32_t n) } while (i < n); return i; } + +/* f: a bool-returning function whose postcondition guarantees `return == true`. + */ +bool f(void) + _ensures(return == true) +{ + return true; +} + +/* g_loop: a do-while whose *guard is a function call* `f()`, with an empty + * body (so it takes the clean desugaring path). Because the guard has side + * effects, PAL omits the `cont == (first || cond)` linking invariant (a + * function call cannot appear in a pure `with_pure` invariant); `cont` simply + * carries the guard's value. Ported from ../loopback-new/pal-tests/bool_call. */ +int g_loop(void) +{ + int r = 0; + do + _do_while_first(first) + _invariant(_live(r) && _live(first)) + _invariant((_specint) r == 0) + { + } while (f()); + return r; +} From f045b1a34eac9a8c38071000a6539db95382ce28 Mon Sep 17 00:00:00 2001 From: t-heili Date: Wed, 1 Jul 2026 13:47:11 -0700 Subject: [PATCH 4/6] do while now extended to support impure cond --- cpp/impl.cpp | 110 +++++++++++++++++++++++++++++++-------- examples/pal.h | 2 + test/do_while/do_while.c | 47 +++++++++++------ 3 files changed, 120 insertions(+), 39 deletions(-) diff --git a/cpp/impl.cpp b/cpp/impl.cpp index 74752678..345e3742 100644 --- a/cpp/impl.cpp +++ b/cpp/impl.cpp @@ -1276,22 +1276,46 @@ class PALConsumer : public ASTConsumer { std::move(invs), std::move(reqs), std::move(enss), std::move(bodyStmts))); } else if (auto *d = dyn_cast(stmt)) { - // Desugar `do { body } while (cond)`. If the body has no top-level - // `continue` we use the "clean" desugaring: - // --> bool cont = true; bool first = true; - // while (cont) { body; first = false; cont = cond; } - // Otherwise (a top-level `continue` would skip the trailing `cont = cond` - // update) we fall back to the legacy desugaring: - // --> bool first = true; - // while (first || cond) { first = false; body; } - // In both cases `_do_while_first(name)` names the first-iteration flag. - - // Extract annotations and check for _do_while_first + // Desugar `do { body } while (cond)` into a `while` loop. There are two + // desugarings, and the presence of a *top-level* `continue` in the body + // selects between them: + // + // * Clean desugaring (no top-level `continue`): + // bool cont = true; bool first = true; + // while (cont) { body; first = false; cont = cond; } + // Here `cont` (the "continuation" flag) drives the loop: it is forced + // true so the body runs at least once (do-while semantics), then the + // guard is re-evaluated at the *end* of the body via `cont = cond`. + // + // * Legacy desugaring (a top-level `continue` is present): + // bool first = true; + // while (first || cond) { first = false; body; } + // We cannot use the clean form here: a top-level `continue` would + // jump past the trailing `cont = cond` update, so the guard would + // never be re-evaluated and the loop could spin forever. The legacy + // form keeps the guard `cond` in the `while` condition (re-evaluated + // on each iteration, side effects and all) where `continue` cannot + // skip it. + // + // `hasTopLevelContinue` decides which form to use. It treats a nested + // for/while/do-while as a boundary (a `continue` inside one binds to that + // inner loop, not to us) but descends into if/switch/blocks/labels, since + // a `continue` there does target this do-while. + // + // Annotations: + // * `_do_while_first(name)` names the first-iteration flag so the user + // can mention it in invariants (e.g. `first ==> i < n`). + // * `_do_while_cond(name)` names the continuation flag `cont`; see the + // clean-path comment on the linking invariant below for why this is + // needed for impure guards. + + // Extract annotations and check for _do_while_first / _do_while_cond auto body = d->getBody(); auto invs = Vec>::new_(); auto reqs = Vec>::new_(); auto enss = Vec>::new_(); std::string flagName; + std::string condName; if (auto attrBody = dyn_cast(body)) { for (auto attr : attrBody->getAttrs()) { if (auto inv = isUnaryAttrOf(attr, "pal-invariant")) { @@ -1307,6 +1331,12 @@ class PALConsumer : public ASTConsumer { if (auto *sl = dyn_cast(arg)) { flagName = sl->getString().str(); } + } else if (ann->getAnnotation() == "pal-do-while-cond" && + ann->args_size() == 1) { + auto *arg = (*ann->args_begin())->IgnoreParenImpCasts(); + if (auto *sl = dyn_cast(arg)) { + condName = sl->getString().str(); + } } } } @@ -1325,11 +1355,19 @@ class PALConsumer : public ASTConsumer { } auto firstId = ctx.mk_ident(toStr(flagName), loc.clone()); + // Continuation flag `cont`: named by _do_while_cond, else auto-generated. + // As with `first`, `_live(cont)` is auto-injected only when the name is + // auto-generated; a user-named `cont` is expected to appear (with its own + // `_live`) in the user's invariants. + bool condIsAuto = condName.empty(); + if (condIsAuto) { + static int doContCounter = 0; + condName = "__do_cont_" + std::to_string(doContCounter++); + } + auto contId = ctx.mk_ident(toStr(condName), loc.clone()); + if (!hasTopLevelContinue(body)) { // Clean desugaring: no top-level `continue`. - static int doContCounter = 0; - std::string contName = "__do_cont_" + std::to_string(doContCounter++); - auto contId = ctx.mk_ident(toStr(contName), loc.clone()); // bool cont; cont = true; stmts.push(mk_var_decl(loc.clone(), contId.clone(), @@ -1348,26 +1386,38 @@ class PALConsumer : public ASTConsumer { auto whileCond = mk_rvalue_lvalue( loc.clone(), mk_lvalue_var(loc.clone(), contId.clone())); - // Always inject _live(cont) (internal flag), and _live(first) when the - // first flag was auto-generated. - invs.push( - mk_live(loc.clone(), mk_lvalue_var(loc.clone(), contId.clone()))); + // Inject _live(cont) and _live(first) when the respective flag name was + // auto-generated (a user-named flag carries its own _live). + if (condIsAuto) { + invs.push( + mk_live(loc.clone(), mk_lvalue_var(loc.clone(), contId.clone()))); + } if (firstIsAuto) { invs.push(mk_live(loc.clone(), mk_lvalue_var(loc.clone(), firstId.clone()))); } // Link the internal `cont` flag to the loop condition so the body knows - // `cond` holds on re-entry (the guard `while (cont)` alone conveys - // nothing to the solver). We inject: + // `cond` holds on re-entry. The guard `while (cont)` alone conveys + // nothing to the solver about `cond`, yet many bodies rely on it (e.g. + // a body doing `i = i + 1` needs `i < n` to maintain `i <= n`). We + // inject: // cont == (first || cond) + // which, together with the guard `cont == true`, re-supplies exactly + // the `first || cond` fact the original do-while guard would have + // provided. // // This is only sound to emit when `cond` is a *pure* expression: the // invariant is a `with_pure` proposition, so an impure guard (e.g. a // function call like `while (f())`) cannot appear in it. When the guard - // has side effects we omit the linking invariant 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. + // has side effects we omit the linking invariant entirely. For such + // impure guards the user can instead name the flag with + // `_do_while_cond(cont)` and write their own *pure* linking invariant + // that relates `cont` to program state rather than to the call itself + // (e.g. `cont == (s.x < 10)`, justified by the callee's postcondition). + // That user-written invariant is what makes post-loop facts provable: + // at loop exit the solver knows `not cont`, and the invariant turns + // that into a fact about the state (e.g. `s.x >= 10`). if (!d->getCond()->HasSideEffects(*astCtx)) { auto firstRead = mk_rvalue_lvalue( loc.clone(), mk_lvalue_var(loc.clone(), firstId.clone())); @@ -1400,6 +1450,20 @@ class PALConsumer : public ASTConsumer { } // Legacy desugaring: body has a top-level `continue`. + // + // The `cont` flag plays no role here (the guard is `first || cond`), but + // if the user named it via `_do_while_cond(cont)` we still declare and + // initialize it. That way an invariant / `_live` referencing `cont` + // resolves to a real, initialized variable and the generated F* file does + // not break -- even though nothing in this desugaring reads `cont`. + if (!condIsAuto) { + stmts.push(mk_var_decl(loc.clone(), contId.clone(), + mk_bool_type(loc.clone()))); + stmts.push(mk_assign(loc.clone(), + mk_lvalue_var(loc.clone(), contId.clone()), + mk_bool_lit(loc.clone(), true))); + } + // bool first; first = true; stmts.push( mk_var_decl(loc.clone(), firstId.clone(), mk_bool_type(loc.clone()))); diff --git a/examples/pal.h b/examples/pal.h index c34f2476..180294c6 100644 --- a/examples/pal.h +++ b/examples/pal.h @@ -22,6 +22,7 @@ __attribute__((annotate("pal-pure"))) _Bool pal_c_assert_enabled(void); #define _refine_value(binding, pred) __attribute__((annotate("pal-refine-value", __capture_args(binding), __capture_args(pred)))) #define _invariant(p) __attribute__((annotate("pal-invariant", __capture_args(p)))) #define _do_while_first(name) __attribute__((annotate("pal-do-while-first", #name))) +#define _do_while_cond(name) __attribute__((annotate("pal-do-while-cond", #name))) #define _assert(p) ({ __attribute__((annotate("pal-assert", __capture_args(p)))) {} }) #define _ghost_stmt(args) ({ __attribute__((annotate("pal-ghost-stmt", __capture_args(args)))) {} }) @@ -63,6 +64,7 @@ __attribute__((annotate("pal-pure"))) _Bool pal_c_assert_enabled(void); #define _refine_value(binding, pred) #define _invariant(p) #define _do_while_first(name) +#define _do_while_cond(name) #define _assert(p) #define _ghost_stmt(args) diff --git a/test/do_while/do_while.c b/test/do_while/do_while.c index 1b8a36c8..410404c4 100644 --- a/test/do_while/do_while.c +++ b/test/do_while/do_while.c @@ -84,7 +84,8 @@ uint32_t nested_continue(uint32_t n) uint32_t i = 0; do _do_while_first(first) - _invariant(_live(i) && _live(n) && _live(first)) + _do_while_cond(cont) + _invariant(_live(i) && _live(n) && _live(first) && _live(cont)) _invariant(first ==> (_specint) i < n) _invariant((_specint) i <= n) { @@ -103,27 +104,41 @@ uint32_t nested_continue(uint32_t n) return i; } -/* f: a bool-returning function whose postcondition guarantees `return == true`. - */ -bool f(void) - _ensures(return == true) +struct counter { + int x; +}; + +/* f: increment the struct's field by 1 and return whether the new value is + * still < 10. Its postcondition pins both the mutation and the returned flag, + * which is what lets g_loop reason about the loop. */ +bool f(struct counter *s) + _requires(s->x >= 0 && s->x < 10) + _ensures(s->x == _old(s->x) + 1) + _ensures(return == (s->x < 10)) { - return true; + s->x = s->x + 1; + return s->x < 10; } -/* g_loop: a do-while whose *guard is a function call* `f()`, with an empty - * body (so it takes the clean desugaring path). Because the guard has side - * effects, PAL omits the `cont == (first || cond)` linking invariant (a - * function call cannot appear in a pure `with_pure` invariant); `cont` simply - * carries the guard's value. Ported from ../loopback-new/pal-tests/bool_call. */ +/* g_loop: a do-while whose guard is the impure call `f(&s)`, with an empty body + * (so it takes the clean desugaring path). Because the guard has side effects, + * PAL omits the auto `cont == (first || cond)` linking invariant. Instead we + * name the continuation flag with `_do_while_cond(cont)` and supply our own + * *pure* linking invariant `cont == (s.x < 10)` (justified by f's + * postcondition). At loop exit the solver knows `not cont`, which via that + * invariant gives `s.x >= 10`; combined with `s.x <= 10` this proves the + * struct's field is exactly 10 on termination. */ int g_loop(void) + _ensures(return == 10) { - int r = 0; + struct counter s = { .x = 0 }; do + _do_while_cond(cont) _do_while_first(first) - _invariant(_live(r) && _live(first)) - _invariant((_specint) r == 0) + _invariant(_live(s.x) && _live(cont) && _live(first)) + _invariant((_specint) s.x >= 0 && (_specint) s.x <= 10) + _invariant(cont == ((_specint) s.x < 10)) { - } while (f()); - return r; + } while (f(&s)); + return s.x; } From aaca7191e0070786c7511088ccde069c352713f0 Mon Sep 17 00:00:00 2001 From: t-heili Date: Wed, 1 Jul 2026 15:39:53 -0700 Subject: [PATCH 5/6] Revert changes. Tests do not all pass --- cpp/impl.cpp | 91 +++++++--------------------------------- examples/pal.h | 2 - test/do_while/do_while.c | 18 +++----- 3 files changed, 20 insertions(+), 91 deletions(-) diff --git a/cpp/impl.cpp b/cpp/impl.cpp index 345e3742..e404f6ea 100644 --- a/cpp/impl.cpp +++ b/cpp/impl.cpp @@ -1302,20 +1302,15 @@ class PALConsumer : public ASTConsumer { // inner loop, not to us) but descends into if/switch/blocks/labels, since // a `continue` there does target this do-while. // - // Annotations: - // * `_do_while_first(name)` names the first-iteration flag so the user - // can mention it in invariants (e.g. `first ==> i < n`). - // * `_do_while_cond(name)` names the continuation flag `cont`; see the - // clean-path comment on the linking invariant below for why this is - // needed for impure guards. - - // Extract annotations and check for _do_while_first / _do_while_cond + // The `_do_while_first(name)` annotation names the first-iteration flag + // so the user can mention it in invariants (e.g. `first ==> i < n`). + + // Extract annotations and check for _do_while_first auto body = d->getBody(); auto invs = Vec>::new_(); auto reqs = Vec>::new_(); auto enss = Vec>::new_(); std::string flagName; - std::string condName; if (auto attrBody = dyn_cast(body)) { for (auto attr : attrBody->getAttrs()) { if (auto inv = isUnaryAttrOf(attr, "pal-invariant")) { @@ -1331,12 +1326,6 @@ class PALConsumer : public ASTConsumer { if (auto *sl = dyn_cast(arg)) { flagName = sl->getString().str(); } - } else if (ann->getAnnotation() == "pal-do-while-cond" && - ann->args_size() == 1) { - auto *arg = (*ann->args_begin())->IgnoreParenImpCasts(); - if (auto *sl = dyn_cast(arg)) { - condName = sl->getString().str(); - } } } } @@ -1355,16 +1344,10 @@ class PALConsumer : public ASTConsumer { } auto firstId = ctx.mk_ident(toStr(flagName), loc.clone()); - // Continuation flag `cont`: named by _do_while_cond, else auto-generated. - // As with `first`, `_live(cont)` is auto-injected only when the name is - // auto-generated; a user-named `cont` is expected to appear (with its own - // `_live`) in the user's invariants. - bool condIsAuto = condName.empty(); - if (condIsAuto) { - static int doContCounter = 0; - condName = "__do_cont_" + std::to_string(doContCounter++); - } - auto contId = ctx.mk_ident(toStr(condName), loc.clone()); + // Continuation flag `cont`: always internal/auto-generated. + static int doContCounter = 0; + auto contId = ctx.mk_ident( + toStr("__do_cont_" + std::to_string(doContCounter++)), loc.clone()); if (!hasTopLevelContinue(body)) { // Clean desugaring: no top-level `continue`. @@ -1386,51 +1369,16 @@ class PALConsumer : public ASTConsumer { auto whileCond = mk_rvalue_lvalue( loc.clone(), mk_lvalue_var(loc.clone(), contId.clone())); - // Inject _live(cont) and _live(first) when the respective flag name was - // auto-generated (a user-named flag carries its own _live). - if (condIsAuto) { - invs.push( - mk_live(loc.clone(), mk_lvalue_var(loc.clone(), contId.clone()))); - } + // Inject _live(cont) (always auto-generated) and _live(first) when the + // first-flag name was auto-generated (a user-named flag carries its own + // _live). + invs.push( + mk_live(loc.clone(), mk_lvalue_var(loc.clone(), contId.clone()))); if (firstIsAuto) { invs.push(mk_live(loc.clone(), mk_lvalue_var(loc.clone(), firstId.clone()))); } - // Link the internal `cont` flag to the loop condition so the body knows - // `cond` holds on re-entry. The guard `while (cont)` alone conveys - // nothing to the solver about `cond`, yet many bodies rely on it (e.g. - // a body doing `i = i + 1` needs `i < n` to maintain `i <= n`). We - // inject: - // cont == (first || cond) - // which, together with the guard `cont == true`, re-supplies exactly - // the `first || cond` fact the original do-while guard would have - // provided. - // - // This is only sound to emit when `cond` is a *pure* expression: the - // invariant is a `with_pure` proposition, so an impure guard (e.g. a - // function call like `while (f())`) cannot appear in it. When the guard - // has side effects we omit the linking invariant entirely. For such - // impure guards the user can instead name the flag with - // `_do_while_cond(cont)` and write their own *pure* linking invariant - // that relates `cont` to program state rather than to the call itself - // (e.g. `cont == (s.x < 10)`, justified by the callee's postcondition). - // That user-written invariant is what makes post-loop facts provable: - // at loop exit the solver knows `not cont`, and the invariant turns - // that into a fact about the state (e.g. `s.x >= 10`). - if (!d->getCond()->HasSideEffects(*astCtx)) { - auto firstRead = mk_rvalue_lvalue( - loc.clone(), mk_lvalue_var(loc.clone(), firstId.clone())); - auto contReadInv = mk_rvalue_lvalue( - loc.clone(), mk_lvalue_var(loc.clone(), contId.clone())); - auto firstOrCond = - mk_rvalue_binop(loc.clone(), ir::BinOp::LogOr(), - std::move(firstRead), trRValue(d->getCond())); - invs.push(mk_rvalue_binop(loc.clone(), ir::BinOp::Eq(), - std::move(contReadInv), - std::move(firstOrCond))); - } - // Build body: original_body; first = false; cont = cond; auto bodyStmts = Vec>::new_(); auto savedIncrement = forLoopIncrement; @@ -1451,18 +1399,7 @@ class PALConsumer : public ASTConsumer { // Legacy desugaring: body has a top-level `continue`. // - // The `cont` flag plays no role here (the guard is `first || cond`), but - // if the user named it via `_do_while_cond(cont)` we still declare and - // initialize it. That way an invariant / `_live` referencing `cont` - // resolves to a real, initialized variable and the generated F* file does - // not break -- even though nothing in this desugaring reads `cont`. - if (!condIsAuto) { - stmts.push(mk_var_decl(loc.clone(), contId.clone(), - mk_bool_type(loc.clone()))); - stmts.push(mk_assign(loc.clone(), - mk_lvalue_var(loc.clone(), contId.clone()), - mk_bool_lit(loc.clone(), true))); - } + // The `cont` flag plays no role here (the guard is `first || cond`). // bool first; first = true; stmts.push( diff --git a/examples/pal.h b/examples/pal.h index 180294c6..c34f2476 100644 --- a/examples/pal.h +++ b/examples/pal.h @@ -22,7 +22,6 @@ __attribute__((annotate("pal-pure"))) _Bool pal_c_assert_enabled(void); #define _refine_value(binding, pred) __attribute__((annotate("pal-refine-value", __capture_args(binding), __capture_args(pred)))) #define _invariant(p) __attribute__((annotate("pal-invariant", __capture_args(p)))) #define _do_while_first(name) __attribute__((annotate("pal-do-while-first", #name))) -#define _do_while_cond(name) __attribute__((annotate("pal-do-while-cond", #name))) #define _assert(p) ({ __attribute__((annotate("pal-assert", __capture_args(p)))) {} }) #define _ghost_stmt(args) ({ __attribute__((annotate("pal-ghost-stmt", __capture_args(args)))) {} }) @@ -64,7 +63,6 @@ __attribute__((annotate("pal-pure"))) _Bool pal_c_assert_enabled(void); #define _refine_value(binding, pred) #define _invariant(p) #define _do_while_first(name) -#define _do_while_cond(name) #define _assert(p) #define _ghost_stmt(args) diff --git a/test/do_while/do_while.c b/test/do_while/do_while.c index 410404c4..a8e6725f 100644 --- a/test/do_while/do_while.c +++ b/test/do_while/do_while.c @@ -84,8 +84,7 @@ uint32_t nested_continue(uint32_t n) uint32_t i = 0; do _do_while_first(first) - _do_while_cond(cont) - _invariant(_live(i) && _live(n) && _live(first) && _live(cont)) + _invariant(_live(i) && _live(n) && _live(first)) _invariant(first ==> (_specint) i < n) _invariant((_specint) i <= n) { @@ -121,23 +120,18 @@ bool f(struct counter *s) } /* g_loop: a do-while whose guard is the impure call `f(&s)`, with an empty body - * (so it takes the clean desugaring path). Because the guard has side effects, - * PAL omits the auto `cont == (first || cond)` linking invariant. Instead we - * name the continuation flag with `_do_while_cond(cont)` and supply our own - * *pure* linking invariant `cont == (s.x < 10)` (justified by f's - * postcondition). At loop exit the solver knows `not cont`, which via that - * invariant gives `s.x >= 10`; combined with `s.x <= 10` this proves the - * struct's field is exactly 10 on termination. */ + * (so it takes the clean desugaring path). NOTE: with the auto-linking invariant + * and the `_do_while_cond` naming feature removed, there is no way to relate the + * internal continuation flag to `s.x`, so the `_ensures(return == 10)` + * postcondition can no longer be proved -- this test is expected to FAIL. */ int g_loop(void) _ensures(return == 10) { struct counter s = { .x = 0 }; do - _do_while_cond(cont) _do_while_first(first) - _invariant(_live(s.x) && _live(cont) && _live(first)) + _invariant(_live(s.x) && _live(first)) _invariant((_specint) s.x >= 0 && (_specint) s.x <= 10) - _invariant(cont == ((_specint) s.x < 10)) { } while (f(&s)); return s.x; From 082172b349c28ff7ee302756cc5253f9d25be6ff Mon Sep 17 00:00:00 2001 From: t-heili Date: Thu, 2 Jul 2026 10:01:46 -0700 Subject: [PATCH 6/6] Changse to do while: added a _do_while_cond and a test that utilizes an impure function in the guard --- cpp/impl.cpp | 87 +++++++++++++++++++++++++++++++++------- examples/pal.h | 2 + test/do_while/do_while.c | 15 ++++--- 3 files changed, 85 insertions(+), 19 deletions(-) diff --git a/cpp/impl.cpp b/cpp/impl.cpp index e404f6ea..805da65e 100644 --- a/cpp/impl.cpp +++ b/cpp/impl.cpp @@ -1302,15 +1302,22 @@ class PALConsumer : public ASTConsumer { // inner loop, not to us) but descends into if/switch/blocks/labels, since // a `continue` there does target this do-while. // - // The `_do_while_first(name)` annotation names the first-iteration flag - // so the user can mention it in invariants (e.g. `first ==> i < n`). - - // Extract annotations and check for _do_while_first + // Annotations: + // * `_do_while_first(name)` names the first-iteration flag so the user + // can mention it in invariants (e.g. `first ==> i < n`). + // * `_do_while_cond(name)` names the continuation flag `cont`. This is + // needed for impure guards: the auto-linking invariant (below) is + // omitted when the guard has side effects, so the user must name + // `cont` and supply their own *pure* linking invariant relating it to + // program state (e.g. `cont == (s.x < 10)`). + + // Extract annotations and check for _do_while_first / _do_while_cond auto body = d->getBody(); auto invs = Vec>::new_(); auto reqs = Vec>::new_(); auto enss = Vec>::new_(); std::string flagName; + std::string condName; if (auto attrBody = dyn_cast(body)) { for (auto attr : attrBody->getAttrs()) { if (auto inv = isUnaryAttrOf(attr, "pal-invariant")) { @@ -1326,6 +1333,12 @@ class PALConsumer : public ASTConsumer { if (auto *sl = dyn_cast(arg)) { flagName = sl->getString().str(); } + } else if (ann->getAnnotation() == "pal-do-while-cond" && + ann->args_size() == 1) { + auto *arg = (*ann->args_begin())->IgnoreParenImpCasts(); + if (auto *sl = dyn_cast(arg)) { + condName = sl->getString().str(); + } } } } @@ -1344,10 +1357,16 @@ class PALConsumer : public ASTConsumer { } auto firstId = ctx.mk_ident(toStr(flagName), loc.clone()); - // Continuation flag `cont`: always internal/auto-generated. - static int doContCounter = 0; - auto contId = ctx.mk_ident( - toStr("__do_cont_" + std::to_string(doContCounter++)), loc.clone()); + // Continuation flag `cont`: named by _do_while_cond, else auto-generated. + // As with `first`, `_live(cont)` is auto-injected only when the name is + // auto-generated; a user-named `cont` is expected to appear (with its own + // `_live`) in the user's invariants. + bool condIsAuto = condName.empty(); + if (condIsAuto) { + static int doContCounter = 0; + condName = "__do_cont_" + std::to_string(doContCounter++); + } + auto contId = ctx.mk_ident(toStr(condName), loc.clone()); if (!hasTopLevelContinue(body)) { // Clean desugaring: no top-level `continue`. @@ -1369,16 +1388,45 @@ class PALConsumer : public ASTConsumer { auto whileCond = mk_rvalue_lvalue( loc.clone(), mk_lvalue_var(loc.clone(), contId.clone())); - // Inject _live(cont) (always auto-generated) and _live(first) when the - // first-flag name was auto-generated (a user-named flag carries its own - // _live). - invs.push( - mk_live(loc.clone(), mk_lvalue_var(loc.clone(), contId.clone()))); + // Inject _live(cont) and _live(first) when the respective flag name was + // auto-generated (a user-named flag carries its own _live). + if (condIsAuto) { + invs.push( + mk_live(loc.clone(), mk_lvalue_var(loc.clone(), contId.clone()))); + } if (firstIsAuto) { invs.push(mk_live(loc.clone(), mk_lvalue_var(loc.clone(), firstId.clone()))); } + // Link the internal `cont` flag back to the loop condition so the body + // knows `cond` held on re-entry. The guard `while (cont)` alone conveys + // nothing to the solver about `cond`, yet many bodies rely on it (e.g. + // a body doing `i = i + 1` needs `i < n` to maintain `i <= n`). We + // inject: + // cont == (first || cond) + // which, together with the guard `cont == true`, re-supplies exactly + // the `first || cond` fact the original do-while guard would have + // provided. + // + // This is only sound when `cond` is a *pure* expression: the invariant + // is a `with_pure` proposition, so an impure guard (e.g. `while (f())`) + // cannot appear in it. When the guard has side effects we omit the + // linking invariant entirely (such loops must instead carry a + // user-written invariant relating program state to the guard's result). + if (!d->getCond()->HasSideEffects(*astCtx)) { + auto firstRead = mk_rvalue_lvalue( + loc.clone(), mk_lvalue_var(loc.clone(), firstId.clone())); + auto contReadInv = mk_rvalue_lvalue( + loc.clone(), mk_lvalue_var(loc.clone(), contId.clone())); + auto firstOrCond = + mk_rvalue_binop(loc.clone(), ir::BinOp::LogOr(), + std::move(firstRead), trRValue(d->getCond())); + invs.push(mk_rvalue_binop(loc.clone(), ir::BinOp::Eq(), + std::move(contReadInv), + std::move(firstOrCond))); + } + // Build body: original_body; first = false; cont = cond; auto bodyStmts = Vec>::new_(); auto savedIncrement = forLoopIncrement; @@ -1399,7 +1447,18 @@ class PALConsumer : public ASTConsumer { // Legacy desugaring: body has a top-level `continue`. // - // The `cont` flag plays no role here (the guard is `first || cond`). + // The `cont` flag plays no role here (the guard is `first || cond`), but + // if the user named it via `_do_while_cond(cont)` we still declare and + // initialize it. That way an invariant / `_live` referencing `cont` + // resolves to a real, initialized variable and the generated F* file does + // not break -- even though nothing in this desugaring reads `cont`. + if (!condIsAuto) { + stmts.push(mk_var_decl(loc.clone(), contId.clone(), + mk_bool_type(loc.clone()))); + stmts.push(mk_assign(loc.clone(), + mk_lvalue_var(loc.clone(), contId.clone()), + mk_bool_lit(loc.clone(), true))); + } // bool first; first = true; stmts.push( diff --git a/examples/pal.h b/examples/pal.h index c34f2476..180294c6 100644 --- a/examples/pal.h +++ b/examples/pal.h @@ -22,6 +22,7 @@ __attribute__((annotate("pal-pure"))) _Bool pal_c_assert_enabled(void); #define _refine_value(binding, pred) __attribute__((annotate("pal-refine-value", __capture_args(binding), __capture_args(pred)))) #define _invariant(p) __attribute__((annotate("pal-invariant", __capture_args(p)))) #define _do_while_first(name) __attribute__((annotate("pal-do-while-first", #name))) +#define _do_while_cond(name) __attribute__((annotate("pal-do-while-cond", #name))) #define _assert(p) ({ __attribute__((annotate("pal-assert", __capture_args(p)))) {} }) #define _ghost_stmt(args) ({ __attribute__((annotate("pal-ghost-stmt", __capture_args(args)))) {} }) @@ -63,6 +64,7 @@ __attribute__((annotate("pal-pure"))) _Bool pal_c_assert_enabled(void); #define _refine_value(binding, pred) #define _invariant(p) #define _do_while_first(name) +#define _do_while_cond(name) #define _assert(p) #define _ghost_stmt(args) diff --git a/test/do_while/do_while.c b/test/do_while/do_while.c index a8e6725f..8cb2112f 100644 --- a/test/do_while/do_while.c +++ b/test/do_while/do_while.c @@ -120,18 +120,23 @@ bool f(struct counter *s) } /* g_loop: a do-while whose guard is the impure call `f(&s)`, with an empty body - * (so it takes the clean desugaring path). NOTE: with the auto-linking invariant - * and the `_do_while_cond` naming feature removed, there is no way to relate the - * internal continuation flag to `s.x`, so the `_ensures(return == 10)` - * postcondition can no longer be proved -- this test is expected to FAIL. */ + * (so it takes the clean desugaring path). Because the guard has side effects, + * PAL omits the auto `cont == (first || cond)` linking invariant. Instead we + * name the continuation flag with `_do_while_cond(cont)` and supply our own + * *pure* linking invariant `cont == (s.x < 10)` (justified by f's + * postcondition). At loop exit the solver knows `not cont`, which via that + * invariant gives `s.x >= 10`; combined with `s.x <= 10` this proves the + * struct's field is exactly 10 on termination. */ int g_loop(void) _ensures(return == 10) { struct counter s = { .x = 0 }; do _do_while_first(first) - _invariant(_live(s.x) && _live(first)) + _do_while_cond(cont) + _invariant(_live(s.x) && _live(cont) && _live(first)) _invariant((_specint) s.x >= 0 && (_specint) s.x <= 10) + _invariant(cont == ((_specint) s.x < 10)) { } while (f(&s)); return s.x;