verify: Treat the contract constructs by their meaning in Clang's own analyses

.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: |

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:

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: {

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:

clang/lib/Analysis/CFG.cpp

@@ -2357,6 +2357,14 @@ CFGBlock *CFGBuilder::Visit(Stmt * S, AddStmtChoice asc,
     case Stmt::InitListExprClass:
       return VisitInitListExpr(cast<InitListExpr>(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<AttributedStmt>(S), asc);
 

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");

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.

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]

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 <class T> void test(int (&)[sizeof(cppverify::exists(k, 0, 3, k == T()), T())]) {} // mangle-error {{cannot yet mangle ExistsExpr expression}}
+template void test<int>(int (&)[sizeof(int)]);
+#endif

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;
 

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`)