[SwayamInSync]

Nothing in CI checked a verdict against the program it is about. The soundness investigation of the 0.2 plan did, by hand: it ran 484 contracted functions natively under UBSan and compared the runs with cpp-verify's verdicts, which is how it found the wrong verdicts F38 to F42. Exit criterion 1 requires that check in CI. This is plan item T2.

The investigation's framework is now clang/utils/cppverify-differential, and CI runs it every night.

What it does

For each case, a contracted C++ function with its pre- and postcondition restated in Python, the tool:

• verifies the function in each configuration its suite lists: Z3 in the auto, bitvector, and integer encodings and cvc5, or BMC at bounds 6 and 10;
• compiles the same source with the product's own clang++ -fverify-contracts -fno-verify (contracts emit no code) and -fsanitize=undefined -fsanitize-trap=undefined;
• runs it on every input of small parameter types (up to 70,000 combinations), otherwise on boundary values and samples seeded by the function's name. Each buffer ends at a PROT_NONE page and then starts after one, and each run has an alarm;
• judges every run whose input the precondition admits with the Python restatement, over mathematical integers as contract arithmetic is.

It reports three kinds of problem, and exits with 1 when there is one:

• UNSOUND: the function is Verified, or BoundedSafe for an input within the bound, yet an admitted input has undefined behavior or breaks the postcondition.
• BADCEX: a counterexample whose input the precondition rejects, or on which the function runs without UB and meets its postcondition.
• DISAGREE: two configurations decide differently.

A failure is evidence relative to the contracts it uses, so the tool does not expect every counterexample to reproduce. These are classified rather than reported:

• a counterexample that passes a call or an arbitrary loop iteration and does not reproduce (as m_weak_post, whose callee promises less than it does);
• a kind that a run cannot show: a check, an invariant, a measure, a frame, a callee's precondition, or an uninitialized read, which UBSan does not detect;
• a contract that is undefined at the input, since only the body runs.

Changes from the investigation's framework

• The harness is the verified source. It was a copy with the contracts removed by a regex, compiled by the system's clang. It is now compiled by the build's own clang with -fverify-contracts -fno-verify, which also exercises the compile path.
• Only admitted inputs run. Inputs the precondition rejects ran too. Some of them loop for their whole alarm: c_old_param_loop took over 8 minutes and was still running. The whole set now takes 344 s with 32 jobs.
• Deterministic samples. Samples were seeded with Python's hash(), which differs from process to process. They are now seeded with the CRC-32 of the name.
• Counterexample classification. A failed verdict whose counterexample did not reproduce was always reported, which today gives 17 false alarms:
  • c_spec_u_ret: the oracle was written before explicit specs became mathematical. u(x) is x, so post(u(x) >= 0) is false for negative x, and the oracle now says so;
  • m_weak_post, st_pass_by_value (callee contracts), l_mul_acc_overflow (an inductive iteration): relative to an abstraction;
  • l_decreases_wrong_sign (termination), m_conv_arg_pre_violated (a callee's precondition): not observable by a run;
  • c_cast_contract_narrow_math: its postcondition (int)(x + 1) == x + 1 || x == 2147483647 is undefined at INT_MAX, since an explicit cast in a contract is checked and the left operand comes first.
• Cases that never ran.
  • Nine _BitInt(65) cases stated their modulus as the literal 36893488147419103232 (2^65), which no C++ integer type holds, so cpp-verify and clang rejected the file. They now write ((__int128)1 << 65). All 15 65-bit cases verify or fail consistently with execution.
  • p_struct_swap, which has no inputs, is verified without a harness.
• A cvc5 counterexample has no values. Its JSON record carries no model, so it is not replayed. The investigation's script filled in zeros there, and the port first did too, which reported (0, 0) as a bad counterexample.

Results

On main plus #101 and #100 (a release build), every case in every configuration has no problem: 518 cases, 0 problems, 344 s with 32 jobs on 64 cores. That is 484 cases, plus the 34 pointer cases rerun under BMC.

Out of 1,982 verdicts:

Verdict	Count
verified	1,212
failed	541
unresolved	212
bounded-safe	17

How each counterexample was classified:

Classification	Count
confirmed by undefined behavior	178
confirmed by a broken postcondition	72
contract undefined at the input	83
not observable by a run	50
relative to a callee's contract or a loop invariant	8
no values (cvc5, and pointer functions)	150

On suites 1, 2, and 4, which the investigation's framework also finished, 154 of 155 cases have the same verdicts in every configuration. The other one, shl_assign_i8_20 with --int-encoding=integer, went from verified to solver.timeout under load.

CI

.github/workflows/cppverify-differential.yml runs nightly and on demand. It builds clang and cpp-verify (release, from the release CI cache), installs cvc5 1.4.2, runs every case, and uploads the JSON report.

clang/test/Verify/differential.test runs the tool's own seven cases on every change. Two of them state their contract wrongly in Python on purpose, so that a right verdict reads as UNSOUND and a right counterexample as BADCEX. One reads past its buffer, which the guard page must trap, and one has a contract undefined at an input.

Each mutant below, applied alone, fails differential.test:

Mutant	Change
T1	a verified function is never unsound
T2	a counterexample that runs fine is accepted
T3	undefined behavior does not confirm a counterexample
T4	rejected inputs run too
T5	every counterexample is relative to an abstraction
T6	postconditions are not observable
T7	the contract has no lines
T8	the harness runs without UBSan
T9	buffers never end at a guard page
T10	an undefined run counts as a normal one

Docs

• Book ch17: a section "Differential execution", with an example that docs_examples.test checks.
• ARCHITECTURE.md: a section on the tool and what it checks.
• REPO_LAYOUT.md: the tool's directory.
• limitations.rst: the nightly check, and the gap it leaves (classes, templates, dynamic storage).
• Release notes: a "Testing" entry.

Checked

• differential.test, docs_examples.test, and docs_coverage.test pass.
• The full run above, with the results shown.

A follow-up for the plan: cvc5 failures print no counterexample values (verification failed: u16mul [...] [backend=cvc5] [reason=counterexample]), in text or JSON.