feat(verify): Adding lazy type_invariant support in cpp-verify - #11
Merged
Merged
Conversation
Add struct type_invariant clauses (parse + Sema field rewrite) and lazy injection into function preconditions when record fields are referenced. Include safe_fib flagship example, quantifier/SpecInline coverage tests, and lexer keyword coverage for type_invariant.
Owner
Author
|
SwayamInSync
changed the title
type_invariant support in cpp-verify
The default vendored path used add_subdirectory/FetchContent, which pulls Z3 into the LLVM CMake tree. Z3's z3_add_component(opt) declares a target named 'opt' that collides with LLVM's llvm/tools/opt (CMP0002 duplicate target), so the verifier could never configure with vendored Z3. Build vendored Z3 in an isolated ExternalProject sub-build instead (static libz3.a, consumed via an IMPORTED target); Z3's targets no longer share LLVM's namespace. Verify/CMakeLists.txt adds an explicit build-order dependency via the CPPVERIFY_Z3_EP_TARGET global property for the Makefiles generator. Also parallelize the setup.sh build with -j$(nproc).
Several node builders passed both std::move(p) and p->Ty as arguments to the same call, e.g. make_unique<VCastExpr>(std::move(Inner), Inner->Ty, ...). Function argument evaluation order is unspecified; under GCC the move is evaluated first, leaving the pointer null when ->Ty is read, which crashed the verifier on essentially every function (Clang's order happened to avoid it). Hoist the type read into a local before the move at all sites: Passivize.cpp (Assign, Return), SpecInline.cpp (two VConditionalExpr), ASTConverter.cpp (two VCastExpr, one VOldExpr).
The type_invariant interception compared Tok.getName() == "type_invariant". Token::getName() returns const char*, so this was a pointer comparison between string literals in different translation units (clangParse vs clangBasic) rather than a string compare, and was effectively never true. The hook was dead code and type_invariant(...) always failed to parse. Use Tok.is(tok::kw_type_invariant) at all three sites.
Two bugs made type_invariant a complete no-op even after it parsed: 1. The Sema rewrite turns an unqualified field in an invariant into this->field, which is an *arrow* MemberExpr (this is a pointer). convertExpr took the arrow branch and called convertExpr(CXXThisExpr) -> unhandled -> null -> bailed, before reaching the CXXThisExpr+FieldSubstPrefix substitution, which sat in the non-arrow path and was dead code. Move the substitution to the top of the MemberExpr handler so this->field maps to the 'param.field' variable. 2. isMutablePointerParam called getPointeeType() on a reference's referent (not a pointer), dereferencing a null QualType and aborting on any reference param. Check referent const-ness directly for references. Also let getRecordFromType see through references so const C&/C& params get injection (same 'param.field' lowering as by-value); pointers stay excluded since p->field lowers to a heap Load.
…nt test safe_fib's loop invariant was '1 <= i && i < n'. At loop exit the path condition becomes (i<n) && !(i<n) = false, so any postcondition verified vacuously (a deliberately wrong post still 'Verified'). Use '1 <= i && i <= n' so the exit state is i == n and the postcondition is proven non-vacuously; a wrong post now correctly fails. type_invariant_lazy only tested 'post(result == p.x)' returning p.x, which holds trivially without any injection. Replace with postconditions that are only provable from the injected invariant (bounded_x, sum_bounded). DESIGN.md showed type_invariant before the fields it names; the clause is parsed eagerly so the fields must be declared first. Reorder the example and note it.
- Drop the unused fnReferencesSpec/vexprHasSpecCall helpers (-Wunused-function). - Remove the redundant type_invariant interception in ParseCXXClassMemberDeclaration; the ParseCXXMemberSpecification loop handles it before member-decl parsing, which is the path that actually fires. - Use isa<FieldDecl> instead of an unused bound variable in the arrow MemberExpr branch (-Wunused-variable). - Drop a stray blank line in Parser.h.
Some queries (e.g. postconditions over old(*p) heap state) do not terminate under the vendored Z3, hanging the tool indefinitely. Set a per-query Z3 timeout (z3::params 'timeout'); on expiry the query returns Unknown, which is already reported honestly and yields a non-zero exit. Plumb a --timeout flag (default 10000 ms, 0 disables) through VerifyOptions and createVerifyBackend into Z3Encoder, covering the BMC backend too. Add a SIGKILL-based per-test wall-clock cap to run-verify-tests.sh (cpp-verify ignores SIGTERM via LLVM's signal handlers), overridable with CPPVERIFY_TEST_TIMEOUT.
emitCallStmt emitted the callee's preconditions as assume rather than assert, so a caller never had to establish them: f(-5) against a callee with pre(x > 0) verified. Per the modular protocol the caller must prove the precondition, so assert it. Postconditions and the modifies havoc are unchanged. This also makes injected type_invariants sound across calls: a caller passing an invariant-bearing argument must now establish the invariant.
When a contract clause failed to parse (e.g. result/old used outside a postcondition), the recovery loop skipped tokens with ConsumeToken(), which asserts the token is not special. An annotation token in the recovery stream tripped the assertion and aborted the compiler. Use ConsumeAnyToken(), the canonical skip-any-token primitive, so invalid input is diagnosed instead of crashing.
The verifier models free functions, not member functions (implicit this, member access), so a contract on an in-class method previously derailed parsing with a confusing 'expected ;' and blocked the rest of the class. Detect contract keywords after a member declarator, emit a clear -Wcontract-unsupported warning, and skip the clauses so the class parses and the method is treated as uncontracted. Full member-function verification remains future work.
exportLeanScratchPad created a default Z3VerifyBackend (no timeout), so the Lean backend's internal Z3 query could hang. Thread SolverTimeoutMs through LeanVerifyBackend and exportLeanScratchPad.
VCExprs are DAGs with shared sub-terms; printing them as a tree can re-expand shared nodes. Cap the number of emitted nodes so the Lean export always terminates, emitting an elision marker past the limit.
…ition Asserting callee preconditions (previous commit) regressed calls inside conditional branches: a call under 'if (c)' asserted its precondition unconditionally, so e.g. lemma_fibo_step's recursive call asserted i-1>=1 even on the i==1 base-case path. Track the path condition while passivizing branches and wrap branch-local precondition asserts as '(guards) ? pre : true', so they only must hold when the branch is taken. Top-level calls are unaffected and still prove their preconditions.
convertExpr did not handle CXXBoolLiteralExpr, so a contract such as pre(true) failed with 'unsupported expression in pre'. Lower true/false to a bool VLiteralExpr.
… eq) Two heap-model bugs made heap+old() postconditions either hang or verify unsoundly: 1. The heap was Array Int Int, but machine-mode programs use bit-vector values, so every load/store round-tripped through bv2int/int2bv. Arrays combined with int<->bv conversions land in a fragment Z3 cannot decide, so queries like post(*a == old(*a)+1) never terminated (on both Z3 4.8 and 4.13). Use Array Int BitVec32: integer addresses (exact, no mod-2^32 aliasing) with bit-vector cell values, eliminating the conversions. 2. arithOp encoded any operation with an array operand as the literal true, including Eq. The if-merge assume mem_k == ite(c, mem_then, mem_else) therefore left the merged heap unconstrained, so conditional stores verified unsoundly. Encode array Eq/Ne as real equality/disequality. Also fix cov_aliases_pair's postcondition: it only holds for n>0, and aliases() permits but does not force aliasing, so it must handle the n==0 (no-write) case.
The loop had no invariant, so after the loop the verifier only knows !(n > 0), i.e. n <= 0 — not enough to prove the postcondition result == 0. Add invariant(n >= 0); combined with the exit guard it gives n == 0.
Make explicit that contract syntax and -fverify-contracts only work with the shipped Clang/cpp-verify (stock GCC/upstream Clang reject both), while building the tool from source works with any standard host compiler.
Content (examples that did not actually verify): - abs with pre(true) overflows at INT_MIN (machine integers), so the quick-start on the home page, the README, ch11, and the ROADMAP item all failed. Bound the precondition to x >= -2147483647 (every int but INT_MIN). ch11 now uses this as a teaching moment for honest machine-integer semantics. - language/functions-loops: f returning x+1 with post(result > x) overflows at INT_MAX; bound to x < 1000. Accuracy / general: - language/tooling: document the new --timeout flag; add a "Supported compiler" note (contracts need the shipped clang; stock GCC/upstream clang reject them). - language/limitations: design notes live in docs/, not extras/docs/. - doxygen mainpage: drop the stale dir_llvm_project_* @ref anchors (this fork is not named llvm-project and modern Doxygen hashes directory IDs); list modules plainly instead. The Sphinx site builds clean (sphinx -n -W, 0 warnings) and every complete code example in the docs now verifies against cpp-verify.
Several working capabilities were missing or thin in the docs. Added, with every example verified against cpp-verify: Language reference: - syntax: complete the "full table" (was missing reveal_with_fuel, reveal, hide, forall, exists, old, result). - ghost-proofs: add hide/reveal, recommends (soft spec preconditions), spec opacity/fuel, and constexpr-as-spec. - new structs.rst: struct-field contracts, type_invariant (semantics + scope), view functions; linked into the reference toctree. Book: - Part I ch06: a conceptual "Opacity and fuel" section (recursive-spec matching loops, why reveal/hide/fuel exist). - Part II ch12: bounded quantifiers (forall/exists) worked example. - Part II ch13: constexpr-as-spec worked example with the single-source-of-truth framing (the Verus differentiator); complete reveal/hide; recommends. - Part II ch14: type_invariant section. Correctness: - DESIGN.md: decreases(a, b) lexicographic tuples are designed but NOT implemented (the parser treats them as a comma expression); document a single measure. Sphinx builds clean (sphinx -n -W, 0 warnings).
… contracts The CppVerify flags had two confusing problems: - a redundant positive run-flag -fverify (verification already runs by default once -fverify-contracts is on), whose generic name collided with upstream -fverify-intermediate-code / -verify; - -fno-verify alone did nothing useful, because the contract language was off. Now there are two clear axes: - -fverify-contracts / -fno-verify-contracts: the contract language (syntax + codegen stripping). Default off. - -fno-verify: skip the SMT step. Exposed as a lone negative (the verifier runs by default when contracts are on), and it now *implies* -fverify-contracts unless contracts were explicitly disabled — making it a standalone syntax/semantics-only 'light check' useful for fast tooling. -fverify is removed. Verified: -fverify-contracts (full verify), -fno-verify (light check, enables contracts, skips solver, still catches syntax/Sema errors), -fno-verify -fno-verify-contracts (off, explicit wins), -fverify (now an error).
Reflect the simplified flag design (drop -fverify; -fno-verify implies -fverify-contracts as a light check): - language/tooling: in-depth 'two axes' section + a quick-lookup table covering all flag combinations and their result. - ch15: rewrite Key flags as the two axes (language vs run-the-prover) and note -fno-verify's light-check / implication behaviour; add --timeout. - ch10: describe -fno-verify as a standalone syntax/semantics check. - workflow SVG + README: replace the removed -fverify with -fverify-contracts; README commands table simplified to a lone -fno-verify light check. Sphinx builds clean (-n -W, 0 warnings).
SwayamInSync
added a commit
that referenced
this pull request
Jul 27, 2026
…-mvp feat(verify): Adding lazy `type_invariant` support in cpp-verify
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
1 participant
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
type_invariant: struct clauses (type_invariant(expr);), Sema rewrite of fields tothis->, lazy injection into function preconditions when record fields are read.safe_fib: end-to-end spec/proof/loop example (lemma_fibo_step,reveal_with_fuel).cov_quantifier_multi.cpp,cov_spec_inline_if.cpp.type_invariantinverify_contracts_keywords.cpp.Tests
./build/bin/cpp-verifyon new suite files: all pass.Rebuild:
ninja -C build clangParse cpp-verify