Repository navigation
Verify backends, docs fixes, Z3 heap fix, coverage tooling - #9
Merged
Merged
Conversation
- Add Z3/BMC/Lean backends, spec inlining, loop unroll, modular chained calls - Fix Z3 encoding for *p = *p + 1 (heap select index vs bit-vector) - Extend DumpIR; LoopUnroll preserves non-loop stmts in BMC path - Add regression suite under clang/test/Verify/suite/ and cov_* tests - Add scripts: run-verify-tests.sh, coverage-sweep.sh, coverage-verify.sh - Fix website tables (list-table for compiler flags), update book ch15–17 - README: backends table, test/coverage commands Region coverage ~81% on clang/lib/Verify (target 90% is follow-up).
There was a problem hiding this comment.
Pull request overview
This PR is a broad update that extends the CppVerify verification engine with multiple backends (Z3/WP, BMC, Lean export), adds spec inlining/modular-call support, and ships new tests, coverage scripts, and documentation/website improvements to match the expanded functionality.
Changes:
- Add backend selection (
--backend={z3,bmc,lean}), Lean scratch export, and BMC loop unrolling; refactor VC handling to a backend-neutral “VCMachine”. - Implement spec call infrastructure (spec-call IR nodes, spec inlining/fuel, hide/reveal) and modular call passivization support.
- Add a large set of verification tests plus coverage tooling and documentation/branding updates.
Reviewed changes
Copilot reviewed 110 out of 119 changed files in this pull request and generated 8 comments.
Show a summary per file
| File | Description |
|---|---|
| website/source/language/tooling.rst | Expands CLI/flags documentation, IR dump layers, and testing/coverage references |
| website/source/language/pointers.rst | Adds pointer contract example and links into book chapter |
| website/source/language/limitations.rst | Updates limitations text with pointers/backends chapter links |
| website/source/language/index.rst | Adds links to tooling/backends docs from language reference index |
| website/source/language/expressions.rst | Clarifies old/result validity and integer-mode behavior |
| website/source/index.rst | Updates install/build/quick-start docs; adds backend examples |
| website/source/conf.py | Switches theme logos to new SVG assets |
| website/source/book/part-ii/index.rst | Adds new Chapter 17 to Part II and updates intro text |
| website/source/book/part-ii/ch17-backends-modular-calls.rst | New chapter describing backends, modular calls, IR dumps, recommends, tests |
| website/source/book/part-ii/ch15-toolchain-and-flags.rst | Adds backend/unroll flags and cross-links to tooling details |
| website/source/book/part-ii/ch13-spec-and-proof-functions.rst | Documents fuel and hide/reveal usage and links to Ch17 |
| website/source/book/part-ii/ch11-first-verified-function.rst | Adds modular-call note and link to Ch17 |
| website/source/api/index.rst | Simplifies API link markup to use shared CSS styling |
| website/source/_static/logo.svg | Adds new light logo SVG asset |
| website/source/_static/logo-mark.svg | Adds new logo mark SVG asset |
| website/source/_static/logo-dark.svg | Adds new dark logo SVG asset |
| website/source/_static/favicon.svg | Updates favicon SVG to match branding |
| website/source/_static/custom.css | Adds table wrapping and styles “btn” link class |
| website/README.md | Updates website build instructions, structure, and table guidance |
| scripts/run-verify-tests.sh | New script to run Verify tests with expected-fail/skip logic |
| scripts/coverage-verify.sh | New full instrumented rebuild + coverage report workflow |
| scripts/coverage-targeted.sh | New targeted/incremental coverage sweep helper |
| scripts/coverage-sweep.sh | New coverage sweep script for suite runs and report summary |
| README.md | Documents backends, chained modular calls, tests, and coverage scripts |
| clang/tools/driver/CMakeLists.txt | Adds conditional coverage link options for clang |
| clang/tools/cpp-verify/Main.cpp | Adds --backend, --lean-out, --unroll CLI flags and wires into VerifyOptions |
| clang/tools/cpp-verify/CMakeLists.txt | Adds conditional coverage link options for cpp-verify |
| clang/test/Verify/verify_spec_proof_e2e.cpp | New end-to-end test for spec/proof + decreases + fuel/reveal |
| clang/test/Verify/verify_proof_post_inline.cpp | New test for proof postcondition referencing a spec call |
| clang/test/Verify/verify_loop_e2e.cpp | New end-to-end loop test |
| clang/test/Verify/verify_lean_export.cpp | New end-to-end Lean export test |
| clang/test/Verify/verify_hide_reveal_e2e.cpp | New end-to-end hide/reveal test |
| clang/test/Verify/verify_constexpr_spec_e2e.cpp | New end-to-end constexpr-as-spec test |
| clang/test/Verify/verify_call_e2e.cpp | New end-to-end call/modular test |
| clang/test/Verify/verify_bmc_bug.cpp | New expected-failure BMC regression test |
| clang/test/Verify/verify_abs_e2e.cpp | Tightens abs precondition to avoid overflow |
| clang/test/Verify/suite/z3_struct_fields.cpp | New suite test for struct field postconditions |
| clang/test/Verify/suite/z3_spec_proof_axioms.cpp | New suite test for spec axioms + proof lemma |
| clang/test/Verify/suite/z3_recommends_warning.cpp | New suite test for recommends failure/warning behavior |
| clang/test/Verify/suite/z3_quantifier_pre.cpp | New suite test for bounded quantifier in preconditions |
| clang/test/Verify/suite/z3_old_result.cpp | New suite test for old + result usage |
| clang/test/Verify/suite/z3_modular_chained.cpp | New suite test for chained modular calls |
| clang/test/Verify/suite/z3_modular_call.cpp | New suite test for modular exec call |
| clang/test/Verify/suite/z3_loop_invariant.cpp | New suite test for loop invariants + decreases |
| clang/test/Verify/suite/z3_hide_reveal_fuel.cpp | New suite test for hide/reveal + fuel controls |
| clang/test/Verify/suite/z3_heap_write_only.cpp | New suite test for heap write with modifies |
| clang/test/Verify/suite/z3_heap_swap.cpp | New suite test for heap swap postconditions with old |
| clang/test/Verify/suite/z3_ghost_contract_assert.cpp | New suite test for ghost contract_assert |
| clang/test/Verify/suite/z3_framing_fail.cpp | New suite expected-failure framing test |
| clang/test/Verify/suite/z3_exec_call.cpp | New suite test for exec call verification |
| clang/test/Verify/suite/z3_control_flow.cpp | New suite test for if/for/while control-flow coverage |
| clang/test/Verify/suite/z3_constexpr_spec.cpp | New suite test for constexpr spec axiom handling |
| clang/test/Verify/suite/z3_arithmetic.cpp | New suite arithmetic coverage test |
| clang/test/Verify/suite/spec_inline_simple.cpp | New suite test for simple spec inlining/axioms |
| clang/test/Verify/suite/lean_backend.cpp | New suite Lean export test |
| clang/test/Verify/suite/dump_ir_layers.cpp | New suite test for per-layer IR dump filtering |
| clang/test/Verify/suite/cov_spec_post_opaque.cpp | New coverage-focused test for hiding specs in postconditions |
| clang/test/Verify/suite/cov_spec_opaque.cpp | New coverage-focused test for hidden spec bodies + recursion |
| clang/test/Verify/suite/cov_spec_lean_inline.cpp | New coverage-focused Lean path exercising spec/hide/reveal |
| clang/test/Verify/suite/cov_spec_fuel_exec.cpp | New coverage-focused test for reveal-with-fuel |
| clang/test/Verify/suite/cov_spec_decreases.cpp | New coverage-focused decreases check test |
| clang/test/Verify/suite/cov_spec_bmc_inline.cpp | New coverage-focused BMC path with spec usage |
| clang/test/Verify/suite/cov_spec_advanced.cpp | New coverage-focused spec branching + recursion |
| clang/test/Verify/suite/cov_recommends_fail.cpp | New coverage-focused recommends failure test |
| clang/test/Verify/suite/cov_proof_decreases.cpp | New coverage-focused proof decreases + loop decreases |
| clang/test/Verify/suite/cov_multi_spec_z3.cpp | New coverage-focused multi-spec chaining test |
| clang/test/Verify/suite/cov_mega_sweep.cpp | New broad coverage sweep test for backends and features |
| clang/test/Verify/suite/cov_loop_unroll_zero.cpp | New coverage test for BMC unroll=0 behavior |
| clang/test/Verify/suite/cov_loop_nested_bmc.cpp | New coverage test for nested loops in BMC |
| clang/test/Verify/suite/cov_lean_quant.cpp | New coverage test for Lean export with quantifiers |
| clang/test/Verify/suite/cov_lean_heap.cpp | New coverage test for Lean export with heap updates |
| clang/test/Verify/suite/cov_if_else_calls.cpp | New coverage test for call lowering in if/else paths |
| clang/test/Verify/suite/cov_heap_loop_incr.cpp | New coverage test for heap self-update in loops |
| clang/test/Verify/suite/cov_for_loop.cpp | New coverage test for for-loop lowering |
| clang/test/Verify/suite/cov_field_expr.cpp | New coverage test for struct field expressions |
| clang/test/Verify/suite/cov_exists.cpp | New coverage test for bounded exists |
| clang/test/Verify/suite/cov_dump_rich.cpp | New coverage test combining dump + quantifiers + heap |
| clang/test/Verify/suite/cov_dump_full.cpp | New coverage test for full IR dump and constructs |
| clang/test/Verify/suite/cov_contracts_spec_ref.cpp | New coverage test for spec references in contracts |
| clang/test/Verify/suite/cov_constexpr_spec.cpp | New coverage test for constexpr usage in contracts |
| clang/test/Verify/suite/cov_chained_assign.cpp | New coverage test for nested calls in assignments |
| clang/test/Verify/suite/cov_bmc_for_loop.cpp | New coverage test for BMC + for loop |
| clang/test/Verify/suite/cov_bmc_body_stmts.cpp | New coverage test for BMC body statements + ghost/assert |
| clang/test/Verify/suite/cov_ast_rich.cpp | New coverage test for AST richness incl. structs and heap |
| clang/test/Verify/suite/cov_aliases_pair.cpp | New coverage test for aliases + modifies |
| clang/test/Verify/suite/bmc_loop_sum.cpp | New BMC suite test |
| clang/test/Verify/suite/bmc_backend.cpp | New BMC suite smoke test |
| clang/test/Verify/dump_ir.cpp | Updates dump_ir abs precondition to avoid overflow |
| clang/lib/Verify/Transform/SpecInline.h | New spec inliner interface + decreases utilities |
| clang/lib/Verify/Transform/SpecInline.cpp | New spec inliner implementation and decreases checks |
| clang/lib/Verify/Transform/Passivize.h | Extends passive program with spec registry and caller int mode |
| clang/lib/Verify/Transform/Passivize.cpp | Adds support for loops, exec calls, ghost blocks, contract_assert, field vars |
| clang/lib/Verify/Transform/LoopUnroll.h | New bounded loop-unroll transform for BMC |
| clang/lib/Verify/Transform/LoopUnroll.cpp | Implements loop unrolling for BMC pipeline |
| clang/lib/Verify/IR/VStmt.h | Extends IR statements (while/call/ghost/hide/reveal/contract_assert) and function metadata |
| clang/lib/Verify/IR/VStmt.cpp | Implements cloning for new stmt kinds + function cloning |
| clang/lib/Verify/IR/VExpr.h | Extends IR expressions with field access and spec calls |
| clang/lib/Verify/IR/VExpr.cpp | Implements cloning for new expr kinds |
| clang/lib/Verify/Frontend/ASTConverter.h | Extends converter for constexpr specs, calls, ghost, hide/reveal/fuel |
| clang/lib/Verify/Frontend/ASTConverter.cpp | Implements new AST lowering for specs/proofs, loops, modular/nested calls, field access |
| clang/lib/Verify/Driver/Verifier.h | Adds backend selection, Lean output path, and BMC unroll options |
| clang/lib/Verify/Driver/Verifier.cpp | Wires backend creation, spec inlining/unroll pipeline, Lean export, recommends checks |
| clang/lib/Verify/Driver/DumpIR.cpp | Adds dumping for new IR nodes and adapts Z3 dump via VCMachine |
| clang/lib/Verify/CMakeLists.txt | Adds coverage option, new sources, and instrumentation flags |
| clang/lib/Verify/Backend/Z3Encode.h | Refactors Z3 encoding to operate on VCMachine and adds backend wrapper |
| clang/lib/Verify/Backend/Z3Encode.cpp | Implements VCMachine-to-Z3 encoding and spec axiom emission support |
| clang/lib/Verify/Backend/VerifyBackend.h | New backend abstraction and factory API |
| clang/lib/Verify/Backend/VerifyBackend.cpp | Implements Z3/Lean/BMC backend selection |
| clang/lib/Verify/Backend/VCMachine.h | New backend-neutral VC representation |
| clang/lib/Verify/Backend/VCMachine.cpp | Implements conversion from PassiveProgram/VExpr into VCMachine |
| clang/lib/Verify/Backend/SpecAxioms.h | New spec axiom collection/unfolding interfaces |
| clang/lib/Verify/Backend/SpecAxioms.cpp | Implements spec axiom emission via spec unfolding |
| clang/lib/Verify/Backend/LeanBackend.h | New Lean scratch-pad export interface |
| clang/lib/Verify/Backend/LeanBackend.cpp | Implements Lean scratch export and embeds Z3 hint output |
Comments suppressed due to low confidence (3)
website/source/index.rst:72
- The manual build instructions use
cmake -S llvm-project/llvm, but this repository layout hasllvm/at the repo root (nollvm-project/directory). As written, the command will fail when run from the repository root.
website/source/index.rst:84 - This Windows manual build command also points at
llvm-project/llvm, but the repository root containsllvm/. The source dir should match the actual checkout layout.
website/source/index.rst:96 - This Visual Studio manual build command uses
llvm-project/llvm, but the source tree in this repo isllvm/at the repository root. The current path will fail for contributors following the docs.
Comment on lines
+473
to
+508
| case VStmt::While: { | ||
| const auto &W = static_cast<const VWhileStmt &>(S); | ||
| CloneCtx Ctx{Renames, OldState, false}; | ||
| for (const auto &Inv : W.Invariants) { | ||
| auto PS = std::make_unique<PassiveStmt>(); | ||
| PS->K = PassiveStmt::Assume; | ||
| PS->Cond = cloneExpr(Inv.get(), Ctx); | ||
| P.Stmts.push_back(std::move(PS)); | ||
| } | ||
| auto PSCond = std::make_unique<PassiveStmt>(); | ||
| PSCond->K = PassiveStmt::Assume; | ||
| PSCond->Cond = cloneExpr(W.Cond.get(), Ctx); | ||
| P.Stmts.push_back(std::move(PSCond)); | ||
| auto BodyRenames = Renames; | ||
| for (const auto &BS : W.Body) | ||
| processStmt(*BS, P, BodyRenames); | ||
| for (const auto &Inv : W.Invariants) { | ||
| CloneCtx ACtx{BodyRenames, OldState, false}; | ||
| auto PS = std::make_unique<PassiveStmt>(); | ||
| PS->K = PassiveStmt::Assert; | ||
| PS->Cond = cloneExpr(Inv.get(), ACtx); | ||
| P.Stmts.push_back(std::move(PS)); | ||
| } | ||
| auto NotC = std::make_unique<VUnaryOpExpr>( | ||
| VUnaryOp::Not, cloneExpr(W.Cond.get(), Ctx), VType::makeBool(), W.Loc); | ||
| auto PSExit = std::make_unique<PassiveStmt>(); | ||
| PSExit->K = PassiveStmt::Assume; | ||
| std::unique_ptr<VExpr> ExitAss = std::move(NotC); | ||
| for (const auto &Inv : W.Invariants) | ||
| ExitAss = std::make_unique<VBinOpExpr>( | ||
| VBinOp::And, std::move(ExitAss), cloneExpr(Inv.get(), Ctx), | ||
| VType::makeBool(), W.Loc); | ||
| PSExit->Cond = std::move(ExitAss); | ||
| P.Stmts.push_back(std::move(PSExit)); | ||
| Renames = BodyRenames; | ||
| break; |
Comment on lines
+662
to
+679
| if (const auto *FS = dyn_cast<ForStmt>(S)) { | ||
| auto Cond = convertExpr(FS->getCond()); | ||
| if (!Cond) | ||
| return Out; | ||
| std::vector<std::unique_ptr<VExpr>> Invariants; | ||
| std::unique_ptr<VExpr> Decreases; | ||
| if (const LoopContractInfo *LCI = Ctx.getLoopContract(FS)) { | ||
| for (const Expr *Inv : LCI->Invariants) | ||
| if (auto E = convertExpr(Inv)) | ||
| Invariants.push_back(std::move(E)); | ||
| if (LCI->Decreases) | ||
| Decreases = convertExpr(LCI->Decreases); | ||
| } | ||
| auto Body = convertStmt(FS->getBody()); | ||
| Out.push_back(std::make_unique<VWhileStmt>(std::move(Cond), std::move(Invariants), | ||
| std::move(Decreases), std::move(Body), | ||
| FS->getBeginLoc())); | ||
| return Out; |
Comment on lines
257
to
270
| InPost = false; | ||
| for (const Expr *E : FCI->Preconditions) | ||
| Fn->Preconditions.push_back(convertExpr(E)); | ||
| if (auto PE = convertExpr(E)) | ||
| Fn->Preconditions.push_back(std::move(PE)); | ||
| InPost = true; | ||
| for (const Expr *E : FCI->Postconditions) | ||
| Fn->Postconditions.push_back(convertExpr(E)); | ||
| if (auto PE = convertExpr(E)) | ||
| Fn->Postconditions.push_back(std::move(PE)); | ||
| InPost = false; | ||
| for (const Expr *E : FCI->Recommends) | ||
| Fn->Recommends.push_back(convertExpr(E)); | ||
| if (auto RE = convertExpr(E)) | ||
| Fn->Recommends.push_back(std::move(RE)); | ||
| for (const Expr *E : FCI->Modifies) | ||
| Fn->Modifies.push_back(convertExpr(E)); |
Comment on lines
+131
to
+155
| std::unique_ptr<VCExpr> expandQuant(const VQuantifiedExpr *Q, bool IsForall) { | ||
| int64_t Lo = evalIntLiteral(Q->Lo.get()); | ||
| int64_t Hi = evalIntLiteral(Q->Hi.get()); | ||
| if (Hi <= Lo) | ||
| return std::make_unique<VCExpr>(IsForall ? VCExpr::True : VCExpr::False); | ||
| std::unique_ptr<VCExpr> Acc = | ||
| std::make_unique<VCExpr>(IsForall ? VCExpr::True : VCExpr::False); | ||
| for (int64_t I = Lo; I < Hi; ++I) { | ||
| auto Body = fromVExpr(Q->Body.get()); | ||
| auto Binder = std::make_unique<VCExpr>(VCExpr::IntLit); | ||
| Binder->IntVal = I; | ||
| auto Eq = std::make_unique<VCExpr>(VCExpr::Eq); | ||
| auto Var = std::make_unique<VCExpr>(VCExpr::Var); | ||
| Var->Name = Q->Binder; | ||
| Eq->Children.push_back(std::move(Var)); | ||
| Eq->Children.push_back(std::move(Binder)); | ||
| auto Inst = std::make_unique<VCExpr>(VCExpr::And); | ||
| Inst->Children.push_back(std::move(Eq)); | ||
| Inst->Children.push_back(std::move(Body)); | ||
| if (IsForall) | ||
| Acc = vcAnd(std::move(Acc), std::move(Inst)); | ||
| else | ||
| Acc = vcOr(std::move(Acc), std::move(Inst)); | ||
| } | ||
| return Acc; |
Comment on lines
+176
to
+194
| case VStmt::If: { | ||
| const auto &I = static_cast<const VIfStmt &>(S); | ||
| auto Cond = evalExpr(I.Cond.get(), Env); | ||
| if (!Cond) | ||
| return nullptr; | ||
| if (I.Else.empty()) { | ||
| auto ThenVal = evalBody(I.Then, Env); | ||
| auto Rest = evalBodySeq(Body, Env, Idx + 1); | ||
| if (!ThenVal || !Rest) | ||
| return nullptr; | ||
| return std::make_unique<VConditionalExpr>(std::move(Cond), std::move(ThenVal), | ||
| std::move(Rest), ThenVal->Ty, I.Loc); | ||
| } | ||
| auto ThenVal = evalBody(I.Then, Env); | ||
| auto ElseVal = evalBody(I.Else, Env); | ||
| if (!ThenVal || !ElseVal) | ||
| return nullptr; | ||
| return std::make_unique<VConditionalExpr>(std::move(Cond), std::move(ThenVal), | ||
| std::move(ElseVal), ThenVal->Ty, I.Loc); |
|
|
||
| VerifyResult R = Backend->verifyPassive(PP); | ||
| if (R.Status == VerifyStatus::Verified) { | ||
| Diags.push_back({VerifyDiagnostic::Verified, "verified: " + Fn->Name}); |
Comment on lines
+9
to
+10
| | Book + language reference | Sphinx (Furo) | `llvm-project/website/build/` | | ||
| | C++ verifier API | Doxygen | `llvm-project/website/build/doxygen/` | |
Comment on lines
+17
to
+19
| ./llvm-project/website/scripts/build-docs.sh | ||
| open llvm-project/website/build/index.html | ||
| open llvm-project/website/build/doxygen/index.html |
Review triage (Copilot on PR #9): - Legit: loop exit state (havoc modified vars, not body renames) - Legit: for-init/inc lowering into while body - Legit: quantifier expansion substitutes binder per index - Legit: spec-inline if branches use separate env copies - Legit: contract expr conversion errors fail TU (no silent drop) - Legit: Verified diagnostic prefix (tests updated) - Legit: website paths use llvm/ and website/ at repo root - False alarm: verified prefix did not break FileCheck (substring match) but UX was wrong; fixed anyway Also commit hide/reveal frontend keywords (parser + AST) already used by tests.
SwayamInSync
added a commit
that referenced
this pull request
Jul 27, 2026
Review triage (Copilot on PR #9): - Legit: loop exit state (havoc modified vars, not body renames) - Legit: for-init/inc lowering into while body - Legit: quantifier expansion substitutes binder per index - Legit: spec-inline if branches use separate env copies - Legit: contract expr conversion errors fail TU (no silent drop) - Legit: Verified diagnostic prefix (tests updated) - Legit: website paths use llvm/ and website/ at repo root - False alarm: verified prefix did not break FileCheck (substring match) but UX was wrong; fixed anyway Also commit hide/reveal frontend keywords (parser + AST) already used by tests.
SwayamInSync
added a commit
that referenced
this pull request
Jul 27, 2026
…p-fix Verify backends, docs fixes, Z3 heap fix, coverage tooling
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Large verifier + documentation update.
Verification engine
*p = *p + 1in loopsTests & tooling
clang/test/Verify/suite/(+ cov_* tests); 55 pass / 0 failclang/lib/VerifyWebsite
Not included: local WIP
hide/revealfrontend keywords.