[SwayamInSync]

A function reported only its first failing check, so each fix showed the next bug one run later. --max-failures=N now reports the first N failing checks of each function (0: every one), each with its own counterexample and notes:

namespace cv = cppverify;

int three_bugs(int x, int y)
  cv::pre(x < 1000 && y < 1000)
  cv::post(cv::result > 0)
{
  int q = 10 / y;
  int r = x + q;
  return r;
}

$ cpp-verify --max-failures=0 three_bugs.cpp
three_bugs.cpp:7:3: error: verification failed: three_bugs [fn_...::division-by-zero@7:3] (counterexample: x [ssa=x_0] [type=i32] = 0, y [ssa=y_0] [type=i32] = 0) [backend=z3] [reason=counterexample]
three_bugs.cpp:8:3: error: verification failed: three_bugs [fn_...::overflow@8:3] (counterexample: q [ssa=q_1] [type=i32] = -1, x [ssa=x_0] [type=i32] = -2147483648, y [ssa=y_0] [type=i32] = -9) [backend=z3] [reason=counterexample]
three_bugs.cpp:5:23: error: verification failed: three_bugs [fn_...::postcondition@5:23] (counterexample: result [ssa=__result_1] [type=i32] = 0, q [ssa=q_1] [type=i32] = 0, r [ssa=r_1] [type=i32] = 0, x [ssa=x_0] [type=i32] = 0, y [ssa=y_0] [type=i32] = 11; trace: return.return@9:3 value=0) [backend=z3] [reason=counterexample]
Summary: 1 failed in 0.0 s

On the base (#95), --max-failures is an unknown option.

A check after a failure is reported only when an execution that passes the failing checks before it fails it. This is Boogie's subsumption, which assumes an assertion once it has checked it, and it is why Dafny's list of failing assertions has no duplicates. Solved alone, the overflow above divided by y = 0, an execution that never reaches the addition. A check that fails only where an earlier one fails is a consequence of that bug, and fixing it fixes both.

The confirmation of a failure after a loop (#94) solves its unrolled copies the same way. That corrects a note #94 got wrong:

int divide(int a, int n)
  cv::pre(n >= 0 && n <= 5)
  cv::post(true)
{
  int c = 0;
  int q = 0;
  while (c < n)
    cv::invariant(0 <= c && c <= n)
    cv::decreases(n - c)
  {
    q = a / (1 - c);
    c = c + 1;
  }
  return q;
}

The failed check is the overflow of INT_MIN / -1, at c == 2. On the base, the note said that an execution fails it within 3 iterations, but that execution divides by 1 - 1 in iteration 2. Now:

divide.cpp:13:7: error: verification failed: divide [fn_...::overflow@13:7] (...) [backend=z3] [reason=counterexample]
note: the counterexample's state at the loop at 9:3 is any state its invariants allow, not necessarily one an execution reaches
note: no execution fails this check without failing an earlier one first (the division-by-zero check at 13:7 fails): those that pass the checks before it end every loop within 2 iterations, and unrolling proves it there

Stacked on #95. This is the second half of plan item E4 (G6: every failing obligation reported).

Design

• Which failures. Z3 solves a module's obligations in order, as before. When verifyObligations is given a number of failures to report, it solves each obligation after the first failure in the executions that pass every earlier obligation that fails. verifyPastEarlier does this: it conjoins the obligation's counterexample query with the goals of those obligations, and caches nothing, since that query asks less than the obligation.
  • Unsettled checks are not assumed, so nothing proved past the failures rests on a check that may not hold.
  • A serial run stops after the Nth failure. A parallel run solves every obligation alone, then solves each failure after the first again, in order.
  • Without a number, every obligation is solved alone, as before. The portfolio needs that, because it compares Z3's per-obligation results with cvc5's.
• Reporting. The result of the first failure carries the others (VerifyResult::MoreFailures, with the module's backend name). The driver prints each one after it with its own notes, including the loop notes and the confirmation, because a later failure through a loop has the same caveat as the first. These diagnostics are marked Additional, and the summary does not count them: it still counts functions. JSON has one record per failure.
• Confirmation. The unrolled module's obligations are solved the same way, so each copy of the failed check, and each loop's unwinding, is solved past the failing checks before it.
  • A copy that fails gives an execution that fails no earlier check.
  • When copies hold where another check fails before them, the note names that check (its kind and place), since that check is the one to fix.
• Backends. The option needs --backend=z3, the default, and source verification. It is an error with the other backends and with archive replay.

Tests

suite/max_failures.cpp (new):

• the default, one failure per function;
• --max-failures=2 and 0, each with one job and with four: three failures of one function in the order an execution meets them, with every counterexample after the division dividing by a y that is not zero;
• an assertion that fails only where an earlier division by zero does, which is not reported;
• a function with two failures through a loop, each with its own notes (unrolling proves the first, and an execution with no iteration fails the second);
• one JSON record per failure, with notes;
• the option rejected with cvc5.

suite/inductive_counterexamples.cpp:

• two_kinds now gets the note that names the division by zero;
• past_failure has a copy that fails within 4 iterations, past a second division that fails in the first iteration. Solved alone, the copy failed within 2 iterations through that division.

Each mutant below, applied alone, makes one of the two tests fail:

Mutant	Change
X1	the option does not reach the backend
X2	every failure is reported, whatever the cap
X3	no failure after the first is kept
X4	a serial run solves the obligations after a failure alone
X5	a parallel run does not solve the failures after the first again
X6	the earlier failures are not assumed
X7	the confirmation solves the copies alone
X8	a copy that holds past another failure is noted as holding in every execution
X9	the additional failures count in the summary
X10	the additional failures name no backend
X11	the additional failures are not printed
X12	the option is accepted with any backend
X13	the additional failures have no notes

X2 survived the first run. A serial run stops after N failures, so only a parallel run reaches the cap, and the test now runs --max-failures=2 with four jobs.

Docs

• tooling.rst: --max-failures, with a checked example.
• functions-loops.rst: the note on a check that fails only after an earlier one, with an example.
• Book ch15, ch16.
• Release notes.
• DESIGN.md: the decision.
• ARCHITECTURE.md: how the failures after the first are solved, in a run and in a confirmation.

Checked

• lit of clang/test/Verify on this branch: 482 passed, 1 unsupported (darwin only), and 1 failure, max_failures.cpp, which was extended during the run. On the final build it passes, as do inductive_counterexamples.cpp, function_filter.cpp, inductive_rules.cpp, command_line.cpp, docs_examples.test, and docs_coverage.test.
• Every branch below this one builds and passes its own tests after the fixes above were folded into it.