From 2be6ebcae3dee77274d1d63c29b55d6d8a3294c7 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 07:33:12 +0530 Subject: [PATCH 01/13] verify: A contract expression or ghost statement cannot throw. --- clang/lib/Sema/SemaExceptionSpec.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/clang/lib/Sema/SemaExceptionSpec.cpp b/clang/lib/Sema/SemaExceptionSpec.cpp index 0ed5c35c40..aab3232a1d 100644 --- a/clang/lib/Sema/SemaExceptionSpec.cpp +++ b/clang/lib/Sema/SemaExceptionSpec.cpp @@ -1433,6 +1433,20 @@ CanThrowResult Sema::canThrow(const Stmt *S) { // These expressions can never throw. return CT_Cannot; + // cpp-verify: contract expressions are never evaluated, and ghost + // statements emit no code. + case Expr::ForallExprClass: + case Expr::ExistsExprClass: + case Expr::ContractChooseExprClass: + case Expr::OldExprClass: + case Expr::ResultExprClass: + case Stmt::ContractAssertStmtClass: + case Stmt::GhostBlockStmtClass: + case Stmt::RevealWithFuelStmtClass: + case Stmt::HideSpecStmtClass: + case Stmt::RevealSpecStmtClass: + return CT_Cannot; + case Expr::MSPropertyRefExprClass: case Expr::MSPropertySubscriptExprClass: llvm_unreachable("Invalid class for expression"); From 8c86a9b6086167d606ad53f0cb019d1d2f423835 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 07:33:12 +0530 Subject: [PATCH 02/13] verify: A contract expression is not an integral constant expression. --- clang/lib/AST/ExprConstant.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/clang/lib/AST/ExprConstant.cpp b/clang/lib/AST/ExprConstant.cpp index 993e7f99a9..6d04581716 100644 --- a/clang/lib/AST/ExprConstant.cpp +++ b/clang/lib/AST/ExprConstant.cpp @@ -22209,6 +22209,12 @@ static ICEDiag CheckICE(const Expr* E, const ASTContext &Ctx) { case Expr::CXXParenListInitExprClass: case Expr::HLSLOutArgExprClass: case Expr::CXXExpansionSelectExprClass: + // cpp-verify: contract expressions have no value at run time. + case Expr::ForallExprClass: + case Expr::ExistsExprClass: + case Expr::ContractChooseExprClass: + case Expr::OldExprClass: + case Expr::ResultExprClass: return ICEDiag(IK_NotICE, E->getBeginLoc()); case Expr::MemberExprClass: { From 6fb6446a9ccc25d772b1ff4e539028fd4d88a401 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 07:33:13 +0530 Subject: [PATCH 03/13] verify: A contract expression has its operands' side effects. --- clang/lib/AST/Expr.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/clang/lib/AST/Expr.cpp b/clang/lib/AST/Expr.cpp index cf0001f509..097447e43a 100644 --- a/clang/lib/AST/Expr.cpp +++ b/clang/lib/AST/Expr.cpp @@ -3822,6 +3822,13 @@ bool Expr::HasSideEffects(const ASTContext &Ctx, return true; break; + // cpp-verify: a contract expression has its operands' effects, as if it + // were evaluated. + case ForallExprClass: + case ExistsExprClass: + case ContractChooseExprClass: + case OldExprClass: + case ResultExprClass: case ParenExprClass: case ArraySubscriptExprClass: case MatrixSingleSubscriptExprClass: From 9289b4cf0c0beb591160370d1bdd73ea7defd042 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 07:33:13 +0530 Subject: [PATCH 04/13] verify: Report a contract expression in a mangled name as not yet mangled. --- clang/lib/AST/ItaniumMangle.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/clang/lib/AST/ItaniumMangle.cpp b/clang/lib/AST/ItaniumMangle.cpp index 3c6e7940bf..6a014f3fd6 100644 --- a/clang/lib/AST/ItaniumMangle.cpp +++ b/clang/lib/AST/ItaniumMangle.cpp @@ -5023,6 +5023,11 @@ void CXXNameMangler::mangleExpression(const Expr *E, unsigned Arity, } // FIXME: invent manglings for all these. + case Expr::ForallExprClass: + case Expr::ExistsExprClass: + case Expr::ContractChooseExprClass: + case Expr::OldExprClass: + case Expr::ResultExprClass: case Expr::BlockExprClass: case Expr::ChooseExprClass: case Expr::CompoundLiteralExprClass: From f3a2078feae6e9ac94be3db5e29fa0ab8ff5c6e5 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 07:33:13 +0530 Subject: [PATCH 05/13] verify: Leave ghost code and contract statements out of the CFG. --- clang/lib/Analysis/CFG.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/clang/lib/Analysis/CFG.cpp b/clang/lib/Analysis/CFG.cpp index bb8e98a894..f9fb4b83c0 100644 --- a/clang/lib/Analysis/CFG.cpp +++ b/clang/lib/Analysis/CFG.cpp @@ -2357,6 +2357,14 @@ CFGBlock *CFGBuilder::Visit(Stmt * S, AddStmtChoice asc, case Stmt::InitListExprClass: return VisitInitListExpr(cast(S), asc); + // cpp-verify: ghost code and contract statements emit no code. + case Stmt::ContractAssertStmtClass: + case Stmt::GhostBlockStmtClass: + case Stmt::RevealWithFuelStmtClass: + case Stmt::HideSpecStmtClass: + case Stmt::RevealSpecStmtClass: + return Block; + case Stmt::AttributedStmtClass: return VisitAttributedStmt(cast(S), asc); From 2127581e2b1ef6c1ee587abb088595dfdb418229 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 07:33:14 +0530 Subject: [PATCH 06/13] verify: List the contract classes the analyzer never evaluates. --- clang/lib/StaticAnalyzer/Core/ExprEngine.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/clang/lib/StaticAnalyzer/Core/ExprEngine.cpp b/clang/lib/StaticAnalyzer/Core/ExprEngine.cpp index 678b07ebba..2dda47acd0 100644 --- a/clang/lib/StaticAnalyzer/Core/ExprEngine.cpp +++ b/clang/lib/StaticAnalyzer/Core/ExprEngine.cpp @@ -1846,6 +1846,18 @@ void ExprEngine::Visit(const Stmt *S, ExplodedNode *Pred, case Stmt::WhileStmtClass: case Stmt::DeferStmtClass: case Expr::MSDependentExistsStmtClass: + // cpp-verify: the CFG omits ghost code and contract statements, and + // contract expressions occur only inside those or in contract clauses. + case Stmt::ContractAssertStmtClass: + case Stmt::GhostBlockStmtClass: + case Stmt::RevealWithFuelStmtClass: + case Stmt::HideSpecStmtClass: + case Stmt::RevealSpecStmtClass: + case Expr::ForallExprClass: + case Expr::ExistsExprClass: + case Expr::ContractChooseExprClass: + case Expr::OldExprClass: + case Expr::ResultExprClass: llvm_unreachable("Stmt should not be in analyzer evaluation loop"); case Stmt::ImplicitValueInitExprClass: // These nodes are shared in the CFG and would case caching out. From 84d3bddbbb4dfcc5c215e5790e9f395464a5ba2b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 07:33:14 +0530 Subject: [PATCH 07/13] test: Clang's analyses meet the contract constructs by their meaning. --- .../Verify/contracts_in_clang_analyses.cpp | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 clang/test/Verify/contracts_in_clang_analyses.cpp diff --git a/clang/test/Verify/contracts_in_clang_analyses.cpp b/clang/test/Verify/contracts_in_clang_analyses.cpp new file mode 100644 index 0000000000..c3a9e4b6a7 --- /dev/null +++ b/clang/test/Verify/contracts_in_clang_analyses.cpp @@ -0,0 +1,33 @@ +// RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -verify=cxx17 %s +// RUN: %clang_cc1 -std=c++98 -fverify-contracts -fno-verify -verify=cxx98 %s +// RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -analyze -analyzer-checker=core -DANALYZE -verify=analyzer %s + +// Clang's own analyses meet the contract constructs by their meaning: a +// contract expression is never evaluated, and ghost code emits no code. + +#ifndef ANALYZE +#if __cplusplus >= 201103L +static_assert(noexcept(cppverify::exists(k, 0, 3, k == 1)), ""); +void declared() noexcept(cppverify::forall(k, 0, 3, k >= 0)); // cxx17-error {{noexcept specifier argument is not a constant expression}} +#else +enum { Constant = cppverify::exists(k, 0, 3, k == 1) }; // cxx98-error {{expression is not an integral constant expression}} +#endif +#endif + +// The analyzer goes on after ghost code. + +int after_ghost(int x) + cppverify::pre(x > 0) +{ + cppverify::ghost { int g = x; } + int *p = 0; + return *p; // analyzer-warning {{Dereference of null pointer}} +} + +int after_check(int x) + cppverify::pre(x > 0) +{ + cppverify::check(x > 0); + int *p = 0; + return *p; // analyzer-warning {{Dereference of null pointer}} +} From a6955805f295f93a666f3496ca3a4addfffd21e6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 07:33:14 +0530 Subject: [PATCH 08/13] verify: Fail CI when a switch over statement classes misses a contract class. --- .github/workflows/cppverify-ci.yml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/.github/workflows/cppverify-ci.yml b/.github/workflows/cppverify-ci.yml index 342c48c3bf..f95b95a2b6 100644 --- a/.github/workflows/cppverify-ci.yml +++ b/.github/workflows/cppverify-ci.yml @@ -81,7 +81,15 @@ jobs: -DLLVM_CCACHE_BUILD=ON - name: Build - run: ninja -C build clang-test-depends + run: | + set -o pipefail + ninja -C build clang-test-depends 2>&1 | tee build.log + + - name: Check that every switch over statement classes handles the contract classes + run: | + if grep -E "enumeration value '((Forall|Exists|Old|Result|ContractChoose)Expr|(ContractAssert|GhostBlock|HideSpec|RevealSpec|RevealWithFuel)Stmt)Class' not handled in switch" build.log; then + exit 1 + fi - name: Report the versions run: | From 99bec8a0767360855d3c65472fcc6ed2f006ab01 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 07:33:30 +0530 Subject: [PATCH 09/13] docs: Describe how Clang's analyses treat the contract constructs in ARCHITECTURE. --- docs/ARCHITECTURE.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index a206c89b61..259a069aac 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1819,6 +1819,13 @@ code: its own line, the body's brace below. In a clause, the colon of a range footprint `p[lo : n]` is a range separator (`TT_ArraySectionColon`), never an Objective-C message's. +- Clang's own analyses meet the constructs by their meaning. The CFG leaves + out ghost code and contract statements, which emit no code, so the static + analyzer and the CFG-based warnings continue past them. A contract + expression cannot throw (`noexcept`), is not an integral constant + expression, has its operands' side effects, and is reported as not yet + mangled where a mangled name would contain it. CI fails when a `switch` over + statement classes misses one of the contract classes. ## IR Debugging (`--dump-ir`) From 1e0cb4f62a2204880d9ffb64571505018ba89b77 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 16 Oct 2026 16:12:05 +0530 Subject: [PATCH 10/13] verify: Expose the contract constructs in libclang as unexposed expressions and statements. --- clang/tools/libclang/CXCursor.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/clang/tools/libclang/CXCursor.cpp b/clang/tools/libclang/CXCursor.cpp index fb0b3c1502..eba327e6bb 100644 --- a/clang/tools/libclang/CXCursor.cpp +++ b/clang/tools/libclang/CXCursor.cpp @@ -229,6 +229,14 @@ CXCursor cxcursor::MakeCXCursor(const Stmt *S, const Decl *Parent, K = CXCursor_UnexposedStmt; break; + case Stmt::ContractAssertStmtClass: + case Stmt::GhostBlockStmtClass: + case Stmt::HideSpecStmtClass: + case Stmt::RevealSpecStmtClass: + case Stmt::RevealWithFuelStmtClass: + K = CXCursor_UnexposedStmt; + break; + case Stmt::GCCAsmStmtClass: K = CXCursor_GCCAsmStmt; break; @@ -348,6 +356,11 @@ CXCursor cxcursor::MakeCXCursor(const Stmt *S, const Decl *Parent, case Stmt::HLSLOutArgExprClass: case Stmt::OpenACCAsteriskSizeExprClass: case Stmt::CXXExpansionSelectExprClass: + case Stmt::ForallExprClass: + case Stmt::ExistsExprClass: + case Stmt::ContractChooseExprClass: + case Stmt::OldExprClass: + case Stmt::ResultExprClass: K = CXCursor_UnexposedExpr; break; From 59d44f3b03354faa1bf31302800b77e1dceeebab Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 16 Oct 2026 16:12:06 +0530 Subject: [PATCH 11/13] test: libclang shows each contract construct and its operands as cursors. --- clang/test/Index/cppverify-cursors.cpp | 37 ++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 clang/test/Index/cppverify-cursors.cpp diff --git a/clang/test/Index/cppverify-cursors.cpp b/clang/test/Index/cppverify-cursors.cpp new file mode 100644 index 0000000000..da1d9117cf --- /dev/null +++ b/clang/test/Index/cppverify-cursors.cpp @@ -0,0 +1,37 @@ +// RUN: c-index-test -test-load-source all %s -std=c++17 -fverify-contracts -fno-verify -isystem %resource_dir | FileCheck %s +// +// libclang exposes each contract construct as an unexposed expression or +// statement, with its operands as children. + +cppverify::spec int down(int x) cppverify::decreases(x) { return x <= 0 ? 0 : down(x - 1); } + +int f(int n) + cppverify::pre(cppverify::forall(k, 0, n, k >= 0)) + cppverify::post(cppverify::result >= cppverify::old(n)) +{ + cppverify::ghost { int g = cppverify::choose(j, 0, 2, j == 1); } + cppverify::check(cppverify::exists(k, 0, 1, k == 0)); + cppverify::hide(down); + cppverify::reveal(down); + cppverify::reveal_with_fuel(down, 2); + return n; +} + +// CHECK: cppverify-cursors.cpp:9:18: UnexposedExpr= Extent=[9:18 - 9:52] +// CHECK: cppverify-cursors.cpp:9:45: BinaryOperator=>= Extent=[9:45 - 9:51] +// CHECK: cppverify-cursors.cpp:10:19: UnexposedExpr= Extent=[10:19 - 10:36] +// CHECK: cppverify-cursors.cpp:10:40: UnexposedExpr= Extent=[10:40 - 10:57] +// CHECK: cppverify-cursors.cpp:10:55: DeclRefExpr=n:8:11 Extent=[10:55 - 10:56] +// CHECK: cppverify-cursors.cpp:12:3: UnexposedStmt= Extent=[12:3 - 12:67] +// CHECK: cppverify-cursors.cpp:12:30: UnexposedExpr= Extent=[12:30 - 12:64] +// CHECK: cppverify-cursors.cpp:12:57: BinaryOperator=== Extent=[12:57 - 12:63] +// CHECK: cppverify-cursors.cpp:13:3: UnexposedStmt= Extent=[13:3 - 13:55] +// CHECK: cppverify-cursors.cpp:13:20: UnexposedExpr= Extent=[13:20 - 13:54] +// CHECK: cppverify-cursors.cpp:13:47: BinaryOperator=== Extent=[13:47 - 13:53] +// CHECK: cppverify-cursors.cpp:14:3: UnexposedStmt= Extent=[14:3 - 14:24] +// CHECK: cppverify-cursors.cpp:14:19: DeclRefExpr=down:6:21 Extent=[14:19 - 14:23] +// CHECK: cppverify-cursors.cpp:15:3: UnexposedStmt= Extent=[15:3 - 15:26] +// CHECK: cppverify-cursors.cpp:15:21: DeclRefExpr=down:6:21 Extent=[15:21 - 15:25] +// CHECK: cppverify-cursors.cpp:16:3: UnexposedStmt= Extent=[16:3 - 16:39] +// CHECK: cppverify-cursors.cpp:16:31: DeclRefExpr=down:6:21 Extent=[16:31 - 16:35] +// CHECK: cppverify-cursors.cpp:16:37: IntegerLiteral= Extent=[16:37 - 16:38] From 105dc2631883e83ec752ec65a10f6ad808e7d590 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 16 Oct 2026 16:12:13 +0530 Subject: [PATCH 12/13] docs: Say in ARCHITECTURE how libclang shows the contract constructs. --- docs/ARCHITECTURE.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 259a069aac..73952b5c82 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1804,7 +1804,10 @@ code: - libIndex indexes the contract expressions and construct references of each function and record, and loop contracts inside bodies, which gives clangd's find references, cross-file rename, and call hierarchy. -- libclang exposes them as child cursors of the function and the loop. +- libclang exposes them as child cursors of the function and the loop: + each construct is an unexposed expression or statement + (`CXCursor_UnexposedExpr`, `CXCursor_UnexposedStmt`) with its operands as + children. - `DeclPrinter` prints a function's clauses, one per line, after its declarator, and `cppverify::spec`/`cppverify::proof` as its specifier; `StmtPrinter` prints loop clauses and the constructs qualified. clangd's From 9c72d10142c599312671ee70794fc12bd6479090 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sun, 18 Oct 2026 19:30:57 +0530 Subject: [PATCH 13/13] test: A contract expression in a mangled name is reported as not yet mangled. --- clang/test/Verify/contracts_in_clang_analyses.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/clang/test/Verify/contracts_in_clang_analyses.cpp b/clang/test/Verify/contracts_in_clang_analyses.cpp index c3a9e4b6a7..7482a69143 100644 --- a/clang/test/Verify/contracts_in_clang_analyses.cpp +++ b/clang/test/Verify/contracts_in_clang_analyses.cpp @@ -1,11 +1,12 @@ // RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -verify=cxx17 %s // RUN: %clang_cc1 -std=c++98 -fverify-contracts -fno-verify -verify=cxx98 %s // RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -analyze -analyzer-checker=core -DANALYZE -verify=analyzer %s +// RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -emit-llvm -o /dev/null -DMANGLE -verify=mangle %s // Clang's own analyses meet the contract constructs by their meaning: a // contract expression is never evaluated, and ghost code emits no code. -#ifndef ANALYZE +#if !defined(ANALYZE) && !defined(MANGLE) #if __cplusplus >= 201103L static_assert(noexcept(cppverify::exists(k, 0, 3, k == 1)), ""); void declared() noexcept(cppverify::forall(k, 0, 3, k >= 0)); // cxx17-error {{noexcept specifier argument is not a constant expression}} @@ -31,3 +32,10 @@ int after_check(int x) int *p = 0; return *p; // analyzer-warning {{Dereference of null pointer}} } + +// A contract expression in a mangled name has no mangling yet. + +#ifdef MANGLE +template void test(int (&)[sizeof(cppverify::exists(k, 0, 3, k == T()), T())]) {} // mangle-error {{cannot yet mangle ExistsExpr expression}} +template void test(int (&)[sizeof(int)]); +#endif