[SwayamInSync]

Plan item E15, its first part (F31 of the plan's findings): a failure points at the part of its check that fails, not at the whole clause or the start of the statement, and a failure at a call shows the callee's clause that does not hold. This PR is stacked on #111 (H5).

What a failure looks like

namespace cv = cppverify;

int half(int x)
  cv::pre(0 <= x && x % 2 == 0)
  cv::post(cv::result * 2 == x)
{
  return x / 2;
}

int odd_half(int y)
  cv::pre(0 <= y && y <= 100)
{
  return half(2 * y + 1);
}

int area(int w, int h)
  cv::pre(0 <= w && 0 <= h)
{
  int a = w * h + 1;
  return a;
}

On the base:

half.cpp:13:3: error: verification failed: odd_half [precondition] [backend=z3] [reason=counterexample]
   13 |   return half(2 * y + 1);
      |   ^
half.cpp:13:3: note: counterexample: y = 0
half.cpp:13:3: note: calls half(1)
half.cpp:19:3: error: verification failed: area [overflow] [backend=z3] [reason=counterexample]
   19 |   int a = w * h + 1;
      |   ^
half.cpp:19:3: note: counterexample: w = 1, h = 2147483647

With this PR:

half.cpp:13:10: error: verification failed: odd_half [precondition] [backend=z3] [reason=counterexample]
   13 |   return half(2 * y + 1);
      |          ^~~~~~~~~~~~~~~
half.cpp:13:10: note: counterexample: y = 0
half.cpp:4:27: note: this precondition does not hold at the call
    4 |   cv::pre(0 <= x && x % 2 == 0)
      |                     ~~~~~~^~~~
half.cpp:13:10: note: calls half(1)
   13 |   return half(2 * y + 1);
      |          ^
half.cpp:19:17: error: verification failed: area [overflow] [backend=z3] [reason=counterexample]
   19 |   int a = w * h + 1;
      |           ~~~~~~^~~
half.cpp:19:17: note: counterexample: w = 1, h = 2147483647

At w = 1 the product fits and the sum overflows, so the caret is at +. In cv::post(0 <= cv::result && cv::result <= 50) with a result of 51 the error is at cv::result <= 50; a disjunction, which fails only when all of it does, is shown whole.

JSON gives the callee's clause as related (message and source), SARIF as a related location, and a GitHub annotation as a line of its message.

Design, from the references

• Dafny splits each clause into one assertion per conjunct before solving (TrSplitExpr), so an error is at its conjunct. At a call it reports "a precondition for this call could not be proved", with the conjunct as a related location: "this is the precondition that could not be proved".
• Verus reports "precondition not satisfied" at the call and labels the callee's requires clause "failed precondition".
• Frama-C's WP splits conjunctions into goals of their own on request (-wp-split).

Splitting before solving multiplies the queries and changes what an obligation is. Here a failure already has a certified counterexample, so the part that fails is found from it, after solving:

• Passivization records, with each check, what it checks in the source apart from the path condition around it (PassiveStmt::Focus). For a callee's precondition, it records the call expression (VCallStmt::CallSite) and the callee's clause (PassiveStmt::Clause). A definedness check made at an operation's operator spans the operation.
• failingPlace (Driver/Counterexample.cpp) finds the checked condition in the goal under its assumptions and evaluates its parts at the counterexample's values, with the certifier's evaluator:
  • a conjunction fails at its first false conjunct;
  • a definedness check, which the verifier builds, also fails at the check under a short-circuit guard whose left side holds;
  • a disjunction the user wrote fails as a whole.
• Only a part the values make false is shown, so the place is as faithful as the counterexample. When the values decide no part, the failure stays where it was.

What it took besides:

• A comparison's lowered terms. A comparison of a machine and a mathematical operand is lowered to a conjunction (the value in range, then the comparison). Its terms took an operand's location, so cv::post(cv::result == n + 1) was "narrowed" to cv::result. They now take the comparison's location and span (asWritten): the terms built for one construct carry its place, so its parts are shown as the comparison. A first version instead split only the conjunctions whose parts lie on either side of their &&; with the terms placed, that rule changed no place, and its mutant survived, so it is gone.
• Lifted helpers. A check inside a lifted constexpr helper would have moved into the helper's body. A focus outside the verified function's own source (VFunction::Extent) is dropped when the module's sources are annotated, so such a check stays at the statement that calls the helper, as before.
• Confirmation. Unrolling (--confirm-bound) looks for copies of a failed check by its anchor, so its notes are computed before the failure is placed.
• Replay. Archive schema v6 keeps each obligation's focus and clause sources (diagnostics only, not hashed). Replay places a failure as a run from source does, matching the archived sources of the goal's terms; the backend fidelity gate checks that a replayed failure's source equals the source run's. A record of v5 or earlier is still read, and its failures are shown at their anchors.
• Spec substitution keeps the span of each node it rebuilds (substParams, substParamsInExpr), so a callee's clause instantiated at a call still spans its source.
• Obligation IDs keep their anchors, so a check's ID does not change; only where it is shown does.

Each mutant below, applied alone and rebuilt, is caught by failing_place.cpp, inductive_counterexamples.cpp, assertions.cpp, failure_notes.cpp, obligation_archive.test, max_failures.cpp, or pointer_subobjects.cpp (17 of 17):

Mutant	Change
P1	no check records its focus
P2	a call's own checks keep the statement
P3	no callee clause is recorded
P4	a call's step stays at the statement
P5	a definedness check spans only its operator
P6	a cloned call drops its call site
C1	a path condition is taken for the condition
C2	no conjunction is split
C4	no short-circuit guard of a definedness check is passed
O1	a split comparison's terms take its operands' locations
V1	a focus outside the function (a lifted helper's) is kept
V2	unrolling's notes come from the placed failure
V3	no JSON related
V4	no related line in GitHub annotations
V5	failures are not placed
A1	archives keep empty places
M1	replay places nothing

Tests

• suite/failing_place.cpp (new):
  • a conjunct of a postcondition; a disjunction, whole; a loop invariant's conjunct;
  • an assertion in a branch, at its condition;
  • an overflowing operation in a declaration; the one of two operations in an expression that overflows; one under the left side of &&; one in a branch;
  • an access out of bounds;
  • a callee's precondition: at the call, with the note at the callee's conjunct; at the second of two calls, with the clause, whole, of two cv::pre clauses; a member function's; an inner call that is an argument of another;
  • a lifted helper's check, which stays at its statement;
  • the JSON related record, SARIF's related location, and the GitHub annotation;
  • archive replay (the same places) and a record of schema v5 (anchors, no clause note).
• 22 tests whose expectations pinned the old places, each updated after checking that the new place is the part that fails. Three of them found what a first version got wrong: inductive_counterexamples.cpp the comparison's lowered terms and the confirmation's notes, assertions.cpp the lifted helper.
• obligation_archive.test and its archive mutator read schema v6, write v5 records, and check that a version 7 is refused.

On the base failing_place.cpp fails at its first check: clamp is reported at the clause's top-level &&.

On a release build of this branch the whole Verify suite passes (503 tests, one unsupported), the docs check passes (268 examples, 0 failed), and so do the unit tests (63, one skipped). After the conjunction rule was removed, the 29 tests that pin places and the docs check were run again and pass.

Docs

• Tooling: what a failure shows, with a worked example and its exact output; JSON related; SARIF; GitHub annotations; a check's ID and its caret; archive schema v6 and replay.
• Chapter 16: the part that fails.
• The outputs of 23 examples on 11 pages whose places moved, rerun.
• Release notes, ARCHITECTURE, DESIGN.

Not done

• A lifted helper's check could show the call with a note in the helper, as a precondition does now.
• A bounds check shows a caret at the access but no range.
• A function whose argument is not addressable prints its conversion error twice (self: reference arguments require ...); that is on the base too.

Stacked on #111.