[SwayamInSync]

A run said how long it took, but not where the time went: a slow file gave no hint of which function, or which stage of it, to look at. Nothing showed progress either, so a long run was silent until its last verdict was settled. Now:

$ cpp-verify --time-report file.cpp
...
Time report (seconds): conversion 0.001, verification 4.412, settling 0.151
     total  lowering   solving  induction  certification  confirmation  function
     4.559     0.001     4.408      3.917          7.577         0.150  small_power
     1.767     0.001     1.766      0.014          3.292         0.000  grows
     0.062     0.002     0.022      0.000          0.000         0.038  after_loop
     0.027     0.001     0.026      0.000          0.000         0.000  fibo
     0.026     0.001     0.025      0.000          0.000         0.000  proved
     0.022     0.001     0.021      0.000          0.000         0.000  pow2
Summary: 4 verified, 2 failed in 4.6 s

On the base (#96), --time-report and --progress are unknown options.

This finishes plan item E5, apart from results streamed as they become final. The summary, --quiet, --verbose, and --list-functions came in #93, and --function in #95. Streaming waits for a design of its own: a verdict is final only once the functions it rests on are settled, and today every fixpoint that settles them runs over the whole file. Until then, the progress line shows that the run moves.

Design

• What is measured. Each function's task gives its backends one BackendTimes (Backend/Timing.h, VerifyBackend::setTimes), which a portfolio, a race, and BMC forward to their solvers.
  • Solving is the wall time in VerifyBackend::verify: encoding, solving, checking counterexamples, inductions, and a proof's vacuity checks.
  • Induction is the part of solving spent in its induction loop.
  • Certification is the time of each counterexample check (certifyCounterexample, through CertifyLimits::Times), summed. With several jobs, checks run at once, so it can exceed solving.
  • Confirmation is the unrolling after a failure (failureNotes) plus each confirmation by proof. The driver times both, and adds a confirmation by proof to the function that proposed it.
  • Lowering is the rest of the task.
  • Total is the task plus its confirmations by proof, so a function's total is exactly its lowering, solving, and confirmation.
• Nothing counted twice. Backends without a sink count nothing: the unroller, the backends of the confirmations by proof, and the one of the cppverify::recommends pass.
• The run. Conversion, verification, and settling are the times between Verifier's construction, the converted functions, the end of the tasks, and the report.
• What is listed. The functions reported (as --function selects them), the busiest first, as Verus's --time-expanded lists its slowest functions. With JSON, the report is cppverify.time/1 records: one for the run, then one per function.
• Progress. The progress line goes to standard error, by default only when standard error is a terminal, and never with JSON. It counts the functions done out of those scheduled so far: --function schedules callees round by round. It is erased before the results print.

Tests

suite/time_report.cpp (new) has a proof, a failure after a loop, a lemma proved by induction, and a claim whose counterexample is confirmed by proof. It checks:

• the text report: one row per function, with six times;
• through the JSON records and Inputs/time_report_phases.py, which phases took time in each function, exactly: no induction where none ran, confirmation only where unrolling or a proof confirmed. In every row the times add up, induction and (with one job) certification are within solving, and the rows come busiest first;
• under BMC, with a spec, whose checks BMC gives a Z3 backend of their own;
• --function, which lists only what it reports;
• --progress, and no progress line on standard error by default under lit;
• the option rejected with archive replay.

suite/time_report_backends.test (new, requires cvc5) checks that certification is counted by cvc5, the portfolio, and the race.

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

Mutant	Change
T1	solving is not timed
T2	inductions are not timed
T3	counterexample checks are not timed
T4	a Z3 query has no sink
T7	cvc5 has no sink
T8	BMC forwards no sink to its solver
T9	a portfolio forwards no sink
T10	a race forwards no sink
T11	unrolling is not counted as confirmation
T12	confirmations by proof are not attributed to their function
T13	the total leaves out the confirmations by proof
T14	functions not reported are listed
T15	the functions keep source order
T16	the progress line shows without a terminal
T17	--progress is ignored
T18	the report is accepted with archive replay
T19	the spec backend of BMC has no sink
T20	the vacuity checks have no sink
T21	the JSON run record is missing

One mutant survives: T5, a pass nested in a Z3 query (the native-definitions pass, the integer pass after a bit-vector probe) without the query's sink. Its checks would then go uncounted, but the query's own checks already make certification non-zero, and no test can tell their sum apart. The sink now passes through PassScope, which already joins a nested pass to its query, rather than at each nested encoder.

T15 survived the first run, because the check busiest first also matched the checker's not busiest first; the check is now anchored. Certification first also counted the evaluation of spec applications at constant arguments, which every query does before solving, so every function had some and a mutant of the counterexample checks' timing could not be seen. That evaluation is part of solving now, and certification is only the checks.

Docs

• tooling.rst: --time-report (every column, the JSON schema) and the progress line.
• Book ch15.
• Release notes.
• ARCHITECTURE.md: what is measured where.

Checked

• lit of clang/test/Verify on this branch: 485 passed, 1 unsupported (darwin only), no failure. docs_examples.test and docs_coverage.test pass with the new section.
• The default output is unchanged: no lit test sees a progress line, and without --time-report the backends get no sink.