[SwayamInSync]

A failure whose counterexample passed through a loop looked like any other, though its state there came from the loop's invariants, and no execution need reach it. The plan's first example (R19) is the first loop most users write:

namespace cv = cppverify;

int count_up(int n)
  cv::pre(n >= 0 && n <= 5)
  cv::post(cv::result == n)
{
  int c = 0;
  while (c < n)
    cv::decreases(n - c)
  {
    c = c + 1;
  }
  return c;
}

On the base (#93) it fails with c = 0 after the loop and nothing more. Now:

count_up.cpp:5:23: error: verification failed: count_up [fn_...::postcondition@5:23] (counterexample: result [ssa=__result_1] [type=i32] = 1, c [ssa=c_1] [type=i32] = 0, c [ssa=c_2] [type=i32] = 1, c [ssa=c_3] [type=i32] = 1, n [ssa=n_0] [type=i32] = 0; trace: loop.entry@8:3 -> loop.exit@8:3 -> return.return@13:3 value=1) [backend=z3] [reason=counterexample]
note: the counterexample's state at the loop at 8:3 is any state its invariants allow, not necessarily one an execution reaches
note: no execution fails this check: every loop ends within 5 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof

and a failure an execution reaches says within how many iterations, with that execution (a division by 3 - c in the loop's body, n <= 5):

other.cpp:27:7: error: verification failed: divides [fn_...::division-by-zero@27:7] (counterexample: c [ssa=c_1] [type=i32] = 0, c [ssa=c_2] [type=i32] = 3, n [ssa=n_0] [type=i32] = 4, q [ssa=q_1] [type=i32] = 0; trace: loop.entry@23:3 -> loop.inductive iteration@23:3 condition=true) [backend=z3] [reason=counterexample]
note: the counterexample's state at the loop at 23:3 is any state its invariants allow, not necessarily one an execution reaches
note: an execution fails this check within 4 iterations of each loop (counterexample: c [ssa=c_1] [type=i32] = 0, c [ssa=c_2] [type=i32] = 1, c [ssa=c_3] [type=i32] = 2, c [ssa=c_4] [type=i32] = 3, n [ssa=n_0] [type=i32] = 4, q [ssa=q_1] [type=i32] = 0, q [ssa=q_2] [type=i32] = 3, q [ssa=q_3] [type=i32] = 5, q [ssa=q_4] [type=i32] = 10; trace: loop.iteration 1@23:3 -> loop.iteration 2@23:3 -> loop.iteration 3@23:3 -> loop.iteration 4@23:3)

A failure of a function whose loop has no cppverify::decreases also names that loop: with a proof the function would still be Unresolved (decreases.missing), which the base never said beside a failure.

Stacked on #93. Plan item E4, its first half (G5: the counterexample's kind and its confirmation by unrolling, and decreases.missing beside a failure); decision Q12 taken as recommended, (a): the verdict stays verification failed, and the notes carry the difference. The other half, every failing obligation reported (G6), follows.

Design

• Which failures. A certified counterexample (Z3, cvc5, the portfolio, the race) whose trace has an active loop event passed through the loop's havoc. Its note names the loop. BMC unrolls already, and Lean has no counterexamples.
• Confirmation by unrolling, of the same check. A copy of the function prepared as BMC prepares it (SpecInliner::prepareFunction, the UB checks), each bound from 0 to --confirm-bound (default 10, 0 skips) unrolled, passivized against the interface map, and solved obligation by obligation (Z3VerifyBackend::verifyObligations), as CBMC and Kani check unrolled programs (the plan's G5). The copies of the failed check are the obligations of its kind at its source location: one per iteration for a check in a loop's body. A failing copy is an execution within that many iterations (callees by their contracts), and its counterexample is noted; copies that hold where every loop's unwinding is proved hold for every execution; copies that hold short of that go on to the next bound; anything unresolved ends the search without a note. Unrolling keeps no loop invariant and no measure, so a failed invariant or measure has no copies and gets the first note only. The whole search gets one query timeout.
• Notes. VerifyDiagnostic::Notes, printed after the error (and after Clang's instantiation note, when there is one) as note: lines, and in JSON as notes.

Tests

suite/inductive_counterexamples.cpp (new), in order with -NEXT: a correct function whose loop lacks an invariant (unrolling proves the check), a reachable failure after one iteration, one no execution reaches within 10 iterations, a failure without a loop (no notes), an unmeasured loop (both notes, the failure reached with no iteration), a division by zero in the loop's body (its copy in the 4th iteration), a failed invariant (no confirmation), two assertions where the one after the loop fails sooner but is another check, a division whose division by zero fails an iteration before its reported overflow (copies are of the failed kind), a path that skips its loop (no notes), and a proof (no notes); --confirm-bound=0; the JSON notes; and --confirm-bound with BMC rejected. function_templates.cpp keeps Clang's instantiation note right after its error.

Each mutant below, applied alone, makes suite/inductive_counterexamples.cpp fail:

Mutant	Change
I1	no failure passes through a loop (no notes)
I3	no failure is confirmed
I4	the copies of the failed check are those of any kind at its place
I5	the copies are those of its kind anywhere
I6	copies that hold prove the check without the loops' unwinding
I7	an unmeasured loop is not named
I8	a failure with no iteration is noted as one within 0 iterations
I9	no failure within the bound is never noted
I10	a check unrolling does not keep (a failed invariant) is noted as passing within the bound
I11	JSON drops the notes
I12	the notes come before Clang's instantiation note
O1	--confirm-bound is accepted with BMC

I4 survived the first run, which had no check of another kind at the failed one's place; two_kinds (a division whose division by zero fails an iteration before its reported overflow) kills it.

Docs

• functions-loops.rst and book ch16: a failure after a loop, with a checked example. tooling.rst, book ch15: --confirm-bound and the notes, in text and JSON.
• release notes, DESIGN.md (the decision), ARCHITECTURE.md (the confirmation).

Checked

• lit of clang/test/Verify on this branch: 479 passed, 2 failed: function_templates.cpp, whose error was followed by the new notes before Clang's instantiation note (the notes now come after it), and docs_coverage.test, which asked for the new behavior in the documentation (added). Both pass now.
• Every example added to the documentation is checked by docs_examples.test, with the output shown.