Chapter 17 — Backends, modular calls, and debugging¶

CppVerify is not only a Z3-backed WP checker. The same front end and IR feed multiple backends and modular call lowering. This chapter ties those pieces to how you work day to day.

Verification backends¶

Backend	CLI	When to use it
Z3 (default)	`cpp-verify file.cpp`	General proofs: functions, pointers, spec/proof, loops via invariant/decreases (WP path).
cvc5	`cpp-verify --backend=cvc5 file.cpp`	Independent solving through a standalone SMT-LIB2 encoding. Requires an installed cvc5 or `--cvc5-path`.
Strict portfolio	`cpp-verify --backend=portfolio file.cpp`	Run Z3 and cvc5 over the same ordered canonical obligations. Use when a matching independent verdict is more important than accepting either solver alone.
Race	`cpp-verify --backend=race file.cpp`	Run Z3 and cvc5 at once and keep whichever settles a function first, as Frama-C’s prover list. Use when the solvers’ strengths differ, as with collections or nonlinear arithmetic, and either solver’s word is enough.
BMC	`cpp-verify --backend=bmc --unroll=N file.cpp`	Small bounded loops: grow the unrolling from zero through `N` and stop at the first decisive frontier. Good when loop structure is simple and bounds are tiny.
Lean	`cpp-verify --backend=lean --lean-project=proof file.cpp`	Generate editable source-attributed goals from the same canonical semantics. Initial generation is `Exported`; an admission-free pinned kernel build is `Certified`.

BMC does not replace loop contracts on the default path; it is an alternate pipeline stage that expands loops before passivization. You still write cppverify::invariant / cppverify::decreases for documentation and for the Z3 backend.

BMC’s result is also bounded explicitly. A counterexample inside the explored prefix is Failed. If safety holds but an unwinding assertion fails, the result is BoundedSafe(N), never an unbounded proof. It reports Verified only when both safety and complete unwinding are proved at an explored bound. Successful dependency-scoped prefix queries are reused in-process at later bounds; failed, unresolved, and unwinding-frontier queries are always solved. Text output lists the attempted bounds and reuse count, while JSON publishes explored_bounds and reused_queries. Numbered loop events such as iteration 2 reconstruct the counterexample depth at the original loop source.

A bounded result that no execution reaches says nothing, so BMC runs the same vacuity checks as Z3 on the program unrolled to the bound, as Kani reports an unreachable check. When every execution runs a loop past the bound, the result is BoundedSafe ... [vacuous] with warning: f: no execution finishes within 3 loop iterations, so its bounded safety covers no complete run; raise --unroll; an unsatisfiable precondition is reported as on the default path.

Strict portfolio mode never votes or silently trusts the primary solver. Two unsat verdicts are Verified; two sat verdicts are Failed and use Z3’s typed model/trace. Opposite verdicts, missing cvc5, unknown/timeout, malformed process output, and unsupported encoding are Unresolved. cvc5 is not vendored because it is an optional independent implementation; install it through the platform package manager or select an executable explicitly.

Race mode trusts each solver alone, which is sound: a proof is a proof, and a counterexample is reported only once the certifier has checked it against the true definitions, whichever solver found it. The first decisive answer stops the other solver. When neither settles a function, each obligation one of them proved counts as proved, since every obligation is a query of its own; the function is Verified with [backend=z3+cvc5] when together they cover all of them, and otherwise the unresolved ones are listed as for Z3. Two decisive answers that differ, which a sound pair cannot give, are backend.inconsistent-results.

Backend release fidelity¶

Contributors can run the repeatable cross-backend release gate as a lit test from the repository root:

./build/bin/llvm-lit -sv clang/test/Verify/suite/backend_fidelity_gate.test

It requires cvc5 and Lean 4.32.2. The gate checks every canonical feature family through Layer 3 and Z3/cvc5/portfolio/BMC, source-identical failures, deterministic parallel execution, canonical and bounded archive replay, Lean theorem/proof-module identity and generated-file compilation, and that cppverify::recommends warnings stay out of BMC and Lean replay artifacts. cvc5 may conservatively return unknown for designated valid quantified or inductive goals; every false matrix goal must remain decisive, and any solver disagreement fails the gate.

Parallel solving and persistent proofs¶

For a translation unit with several proof obligations:

cpp-verify --jobs=4 --proof-cache=.cppverify-cache file.cpp

--jobs=0 selects available physical cores. Each ordered obligation runs in its own Z3 context or cvc5 process, but results are published in source order. Frontend lowering, IR/archive output, Lean generation, and diagnostics remain serial, so changing the job count does not change the first reported failure.

The cache stores only Verified individual obligations. Keys include the goal’s dependency-scoped semantic hash, backend/adapter identity, and exact Z3 version. A portfolio cache entry covers only its namespace-separated Z3 component; cvc5 always reruns. Standalone cvc5 rejects the proof cache. A BMC cache entry is separate from an unbounded Z3 entry and retains its semantic unroll provenance. Counterexamples, unknown/resource-limited queries, and BoundedSafe results are never cached. Corrupt or unreadable entries produce Unresolved instead of being trusted or silently replaced. Use --proof-cache-max-mb and --proof-cache-max-entries to bound storage. Pruning runs once, after a run’s last lookup, and proceeds even when another cache operation fails; capacity errors evict an old record and retry once, and abandoned atomic-write files older than 24 hours are removed without disturbing newer concurrent writes. The opt-in directory is trusted local memoization, not a portable certificate; do not make it writable by untrusted users. Lean certification remains the independent kernel-checking path.

Solver work can also be bounded explicitly:

cpp-verify --timeout=30000 --solver-rlimit=500000 \
  --max-query-nodes=50000 file.cpp

Timeout, solver resource, and canonical query-size exhaustion remain non-success results with distinct machine-readable reason codes.

Editable Lean fallback¶

For an explicit interactive proof:

cpp-verify --backend=lean --lean-project=proof file.cpp
# complete proof/CppVerify/Proofs/*.lean; put shared lemmas in User.lean
cpp-verify --backend=lean --lean-project=proof --lean-certify file.cpp

Generated.lean and Check.lean are machine-owned. User.lean and existing per-obligation proof files are never overwritten. The project pins leanprover/lean4:v4.32.2. Certification compiles the user module and every active proof with admissions promoted to errors, checks the aggregate module, and rejects proof dependencies other than Lean’s documented foundational axioms.

The Lean backend does not yet translate the spec collections of <cppverify.h> (seq, set, multiset, map): a function whose obligations use one is Unresolved with reason logic.unsupported on it. Lean support for them is planned for a future release; until then such functions are verified with Z3 (the default) or cvc5.

To keep Z3 as the fast path and export only unresolved functions:

cpp-verify --lean-fallback=proof file.cpp
cpp-verify --lean-fallback=proof --lean-certify file.cpp

The first run still exits as unresolved. By default only the obligations the solver did not prove individually are exported, under the goal names they have in a complete export; each remaining obligation already has its own solver proof. When every exported goal kernel-checks the function is Proved (z3+lean), or Proved (portfolio+lean), and JSON reports "status":"mixed-proof" with the per-obligation split. Only --lean-fallback-scope=all, which exports every obligation, can make a fallback function Certified. SAT counterexamples are failures, not fallback candidates. Regeneration may leave old proof files on disk, but only the current source obligations are imported and certified; a stale active proof must type-check against the regenerated goal.

Portable obligation archives¶

The canonical backend boundary can be persisted and replayed:

cpp-verify --lower-only --obligation-out=goals.cpv file.cpp
cpp-verify --obligation-in=goals.cpv --backend=z3
cpp-verify --obligation-in=goals.cpv --backend=portfolio
cpp-verify --obligation-in=goals.cpv --lower-only --dump-ir=3,4
cpp-verify --obligation-in=goals.cpv --backend=lean --lean-out=goals.lean

Each cppverify.obligation/2 record uses stable wire tags, defensive bounds, portable source points, and path-independent SHA-256 semantic hashes. Replay revalidates every sort, expression, logical declaration, call signature, feature declaration, and identity before backend dispatch. Multiple records may be concatenated. Parsing has explicit depth/node/collection budgets and a 4096-bit integer-width ceiling; malformed terms, non-canonical payloads, ill-scoped variables, and contradictory complete/ordered goals fail closed. Different records may request different reveal fuel for one logical function, but its shared parameter/result signature must remain compatible.

Source-built and replayed records pass through the same conservative canonicalizer before hashing and dispatch. It folds only trivial Boolean structure and reflexive equality/inequality, removes transitively unreachable logical declarations, rebuilds exact ordered and complete queries plus feature metadata, and revalidates. It does not rewrite arithmetic, quantifiers, pointers, heaps, or assumptions. Canonicalization introduced semantic-hash format v2; format v3 removed diagnostic obligation identities from the preimage, and format v4 removes every obligation kind except unwinding. Schema v2 adds precise obligation kinds; schema v1 records remain readable.

BMC source verification archives only the terminal module for each function. Those records retain their exact explored unroll bound. Replay is fixed-bound and uses BMC unwinding aggregation, so an incomplete frontier remains BoundedSafe(N) rather than rerunning the incremental source strategy. BMC cannot be applied to an untransformed record because loop unrolling is a VCR transformation that occurs before canonical obligation construction. Lean scratch replay of bounded records is rejected until the generated theorem format carries the same transform provenance. Failure-only cppverify::recommends checks are not archived, so bytes do not depend on whether a prior solver run succeeded or failed. The dependency-scoped proof cache is shared by direct verification and replay, so identical canonical goals reuse proofs without trusting source paths or diagnostic identities.

Modular function calls¶

Functions with cppverify::pre / cppverify::post are verified modularly: the caller must prove the callee’s precondition at the call site and may then assume its postcondition (and frame conditions) without re-analyzing the callee body.

Simple call:

int y = abs_val(x);

Chained calls in one expression are supported by lowering inner calls to temporaries first:

int inc(int x) cv::pre(x >= 0 && x < 100) cv::post(cv::result == x + 1) { return x + 1; }

int twice(int x)
  cv::pre(x >= 0 && x < 98)
  cv::post(cv::result == x + 2)
{
  return inc(inc(x));   // inner inc, then outer inc
}

The converter emits VCallStmt for each exec or proof call site; passivization substitutes callee contracts in order. A call to a proof function is therefore a modular contract call like an exec call: its precondition is asserted and its postcondition assumed. Spec functions are inlined or axiomatized. Neither spec nor proof functions are emitted at runtime.

Preconditions, cppverify::old(parameter), and a parameter named in a postcondition all denote the argument’s entry value, as in ACSL, even when the callee reassigns its by-value parameter; the caller substitutes its argument. A function that sets its parameter p to null and returns therefore does not prove cppverify::post(p == nullptr) for a non-null argument.

A call changes the caller’s heap only inside the callee’s cppverify::modifies footprints, instantiated with the arguments: a cell (p[i], p->field) or a range (p[lo : n]) is exactly those cells, and a region (*p) is the object the argument addresses, its valid extent or else one object. Every other cell keeps its value, and the postcondition then re-establishes whatever the caller may rely on inside the footprints. Each footprint must also lie within the caller’s own cppverify::modifies, read in the caller’s entry state. A callee without cppverify::modifies whose body (or a callee of it) may write is treated as writing the whole heap; a conservative body scan keeps the heap for verified, acyclic read-only callees. A function that allocates or deallocates storage is verified as a standalone body. A call to it is supported only when it is an inferred fresh-owned scalar factory (see “Returning fresh ownership” in Chapter 19 — Dynamic storage and lifetime); a call to a function that deallocates, or that has any other lifetime effect, fails closed (Unresolved with reason construct.unsupported).

valid(p, n) extents also cross calls as checked sub-slices. Passing p + offset to a valid(q, length) formal asserts one root, nonnegative offset and length, and offset + length <= n. Empty one-past slices, exact-cell writes, ranges cppverify::modifies(q[lo : n]), and whole-slice cppverify::modifies(*q) are supported; the call changes only the written cells of the slice.

A caller-owned dynamic scalar may be passed in the other direction to a verified, non-allocating executable callee. Its direct matching pointer parameter may be compared or dereferenced, including a write authorized by cppverify::modifies(*p). The call substitutes the caller’s lifetime identity into validity checks and accepts the footprint only after proving that identity is one of the caller’s live allocations. Acyclic direct-pointer forwarding, scalar-value executable/spec helpers, and direct/conditional/null pointer results are checked recursively. Pointer results receive a separate SSA provenance target and need a result-equality contract to recover owned alias authority. Offset/subscript access, pointer copies or rebinding, nested pointer-result calls, recursion cycles, ghost use, proof/external contracts, and allocation in the callee fail closed. Within the caller, address and identity remain a pair through local copies, assignments, branches, nullptr, and supported call results.

Where verification stops: trusted contracts¶

Modular verification proves each function against its callees’ contracts. At the edge of the program there are functions it cannot see into: a library compiled elsewhere, a system call, a routine written in assembly. Their contracts can only be assumed, and CppVerify assumes a contract only when you say so, with the standard attribute syntax:

[[cppverify::trusted]] int clamp_byte(int v)
  cv::post(0 <= cv::result && cv::result <= 255);

[[cppverify::trusted]] int read_sensor(int channel)
  cv::pre(channel >= 0 && channel < 4)
  cv::post(cv::result >= 0 && cv::result <= 1023)
{
  return channel * 300;   // stands for hardware access
}

int sample(int c)
  cv::pre(c >= 0 && c < 4)
  cv::post(0 <= cv::result && cv::result <= 255)
{
  int r = read_sensor(c);
  return clamp_byte(r);
}

int twice(int c)
  cv::pre(c >= 0 && c < 4)
  cv::post(0 <= cv::result && cv::result <= 510)
{
  int a = sample(c);
  int b = sample(c);
  return a + b;
}

clamp_byte has no definition here; read_sensor has one, which is compiled but not verified. Each reports Trusted: ... (contract assumed, not verified), and every proof that relies on either names it, through any number of verified callers:

trusted.cpp:1:28: Trusted: clamp_byte (contract assumed, not verified)
trusted.cpp:4:28: Trusted: read_sensor (contract assumed, not verified)
Verified: sample [backend=z3] [trusts=clamp_byte,read_sensor]
Verified: twice [backend=z3] [trusts=clamp_byte,read_sensor]

The [trusts=...] list is the trusted computing base of that one proof: the verdict is exactly as reliable as those contracts. Keep it short. A trusted contract should state what the function guarantees and nothing more, and a function whose body is in the verified subset should be verified instead.

On a cppverify::proof function the mark makes an axiom: its postcondition is assumed for every argument that meets its precondition. That is occasionally the right tool, for a mathematical fact that the solver cannot prove and that you would rather cite than prove. It is also the easiest way to make every proof true, so an axiom that a call cannot satisfy is reported as [vacuous] (see Chapter 16 — When verification fails).

A contract with neither a definition nor the mark is not assumed: its callers are Unresolved with reason callee.contract, and a warning points at the declaration. A forgotten definition therefore cannot silently turn into an axiom.

The same boundary exists in other verifiers. Verus assumes the specification of a function marked #[verifier::external_body]. Frama-C assumes the contract of a function without a body when it proves the callers. CppVerify makes the assumption an explicit mark on the declaration and carries it into every verdict that depends on it.

Z3 result discipline¶

Passive SSA is lowered once into a typed, source-attributed ObligationModule. Layer 3 dumps this exact module and all backends consume it. It contains one complete counterexample query plus equivalent ordered queries with deterministic internal IDs, a precise kind per obligation (for example precondition, overflow, or bounds), source-anchored public IDs/ranges, original-name typed model metadata, and guarded trace events. Display-only diagnostic metadata persists through archives but is excluded from semantic hashes, including both positional and source-anchored obligation IDs. With one job and no proof cache, the backend submits the complete query first, then the ordered queries if it does not settle the module. With more than one job (the default uses the available physical cores) and more than one obligation, the ordered queries run beside the complete query, and a proof by either interrupts the other. With a proof cache, only the ordered queries run, since the cache holds proofs of single obligations. unsat means verified. A sat model is reported as a counterexample only once the certifier has checked it against the true definitions; otherwise the function is Unresolved with a reason, such as counterexample.unchecked. When the complete query ends unknown or with an unchecked model, the ordered queries check the module-owned assertions separately in source order, using only entry facts and assumptions that precede each obligation. They do not rebuild a second VC. This helps quantified heap programs without letting a later assumption prove an earlier assertion. If they still cannot discharge every obligation, the function is Unresolved and is not certified unless the user opted into the Lean fallback and its current project passes the admission-free kernel check.

Model extraction never uses Z3 model completion. Undetermined values and path guards stay explicitly unknown. When a complete-query model makes a particular ordered counterexample query true, CppVerify attributes the failure and its trace to that narrow obligation rather than reporting an anonymous whole-query counterexample.

Parallel verify + compile¶

clang++ -std=c++17 -fverify-contracts -c module.cpp -o module.o

With -fverify-contracts, the contract constructs parse as part of the language. Unless you pass -fno-verify, the compiler runs cpp-verify in parallel with code generation. Ghost blocks, spec functions, and proof functions are stripped from the object file — no runtime cost.

Dumping IR layers¶

When a proof fails or looks wrong, dump intermediate representations:

cpp-verify --dump-ir=1 file.cpp      # Layer 1: VCR (typed CFG)
cpp-verify --dump-ir=2 file.cpp      # Layer 2: passive (SSA assume/assert)
cpp-verify --dump-ir=3,4 file.cpp   # canonical Obligation IR and Z3 translation

Layer aliases: layer-1 … layer-4, or all. Multiple layers are separated by ======.

`cppverify::recommends` and soft checks¶

cppverify::recommends on spec functions is optional advice. If verification fails, the tool may report that a cppverify::recommends clause at a call site was not implied by the caller’s precondition — a warning, not a hard error.

Regression tests¶

The repository ships executable examples under clang/test/Verify/ and clang/test/Verify/suite/. From the repo root:

./scripts/run-verify-tests.sh

Contributors can measure clang/lib/Verify region coverage with ./scripts/coverage-sweep.sh (after a normal build) or ./scripts/coverage-verify.sh (full instrumented rebuild). Use -DCPPVERIFY_ENABLE_COVERAGE=ON on clangVerify only.

Next: Chapter 18 — Undefined behavior for proving freedom from undefined behavior.