diff --git a/cpp/impl.cpp b/cpp/impl.cpp index 082df1d6..805da65e 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,17 +1276,48 @@ 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. - - // 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`. 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")) { @@ -1284,45 +1333,162 @@ 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(); + } } } } 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()); + + // 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`. + + // 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())); + + // 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))); + } - // 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`. + // + // 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(), 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/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 ebad446a..8cb2112f 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) @@ -71,3 +72,72 @@ 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; +} + +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)) +{ + s->x = s->x + 1; + return s->x < 10; +} + +/* 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) +{ + struct counter s = { .x = 0 }; + do + _do_while_first(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; +}