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: | 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: 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: { 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: 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); 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"); 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. 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] 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..7482a69143 --- /dev/null +++ b/clang/test/Verify/contracts_in_clang_analyses.cpp @@ -0,0 +1,41 @@ +// 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. + +#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}} +#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}} +} + +// 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 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; diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index a206c89b61..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 @@ -1819,6 +1822,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`)