Verify backends, docs fixes, Z3 heap fix, coverage tooling

README.md

@@ -70,18 +70,29 @@ int abs(int x)
 
 Use `-fverify-contracts` on `clang++` so `pre` / `post` are keywords. `cpp-verify` enables that flag automatically.
 
+## Verification backends
+
+| Backend | CLI | Role |
+|---------|-----|------|
+| **Z3** (default) | `cpp-verify file.cpp` | Weakest-precondition VCs + Z3 |
+| **BMC** | `cpp-verify --backend=bmc --unroll=N file.cpp` | Bounded loop unrolling, then Z3 |
+| **Lean export** | `cpp-verify --backend=lean --lean-out=out.lean file.cpp` | Emit goals for manual proof |
+
 ## Commands
 
 | Command | Role |
-| -------- | ----- |
+|---------|------|
 | `cpp-verify file.cpp` | Verify only (Z3) |
 | `clang++ -fverify-contracts -c file.cpp` | Verify (parallel) + compile |
 | `clang++ -fverify-contracts -fno-verify -c file.cpp` | Contracts on; skip SMT |
 
 ```bash
-./build/bin/cpp-verify --dump-ir=1,2 file.cpp   # layers: 1=VCR 2=passive 3=VC 4=Z3
+./build/bin/cpp-verify --dump-ir=1,2,3,4 file.cpp   # VCR, passive, VC, Z3
 ```
 
+Chained modular calls (e.g. `return inc(inc(x))`) are lowered to temporaries automatically.
+See [Chapter 17](https://swayaminsync.github.io/cpp-verify/book/part-ii/ch17-backends-modular-calls.html).
+
 Contract syntax, flags, and limitations: **[language reference](https://swayaminsync.github.io/cpp-verify/language/index.html)**.
 
 ## Documentation
@@ -105,9 +116,17 @@ Design notes: `docs/DESIGN.md`, `docs/ARCHITECTURE.md`.
 ## Tests
 
 ```bash
+./scripts/run-verify-tests.sh
 ./build/bin/llvm-lit clang/test/Verify
 ```
 
+Contributor coverage (instrument ``clangVerify`` only):
+
+```bash
+./scripts/coverage-sweep.sh       # after a normal build
+./scripts/coverage-verify.sh      # full instrumented rebuild (slow)
+```
+
 ## License
 
 LLVM components use the [LLVM License](https://llvm.org/LICENSE.txt). See file headers in the tree.

clang/include/clang/AST/RecursiveASTVisitor.h

@@ -2604,6 +2604,8 @@ DEF_TRAVERSE_STMT(ExistsExpr, { TRY_TO(TraverseDecl(S->getBoundVar())); })
 DEF_TRAVERSE_STMT(ForallExpr, { TRY_TO(TraverseDecl(S->getBoundVar())); })
 DEF_TRAVERSE_STMT(GhostBlockStmt, {})
 DEF_TRAVERSE_STMT(RevealWithFuelStmt, {})
+DEF_TRAVERSE_STMT(HideSpecStmt, {})
+DEF_TRAVERSE_STMT(RevealSpecStmt, {})
 DEF_TRAVERSE_STMT(OldExpr, {})
 DEF_TRAVERSE_STMT(ResultExpr, {})
 

clang/include/clang/AST/StmtContract.h

@@ -7,7 +7,8 @@
 //===----------------------------------------------------------------------===//
 //
 // This file defines AST nodes for CppVerify contract statements:
-//   ContractAssertStmt, GhostBlockStmt, RevealWithFuelStmt
+//   ContractAssertStmt, GhostBlockStmt, RevealWithFuelStmt,
+//   HideSpecStmt, RevealSpecStmt
 //
 //===----------------------------------------------------------------------===//
 
@@ -139,6 +140,70 @@ class RevealWithFuelStmt : public Stmt {
   }
 };
 
+/// HideSpecStmt - ghost { hide(fn); } — keep spec body opaque in this VC.
+class HideSpecStmt : public Stmt {
+  friend class ASTStmtReader;
+  SourceLocation Loc;
+  SourceLocation LParenLoc;
+  SourceLocation RParenLoc;
+  Stmt *Function;
+
+public:
+  HideSpecStmt(SourceLocation Loc, SourceLocation LParenLoc,
+               SourceLocation RParenLoc, Expr *Function)
+      : Stmt(HideSpecStmtClass), Loc(Loc), LParenLoc(LParenLoc),
+        RParenLoc(RParenLoc), Function(Function) {}
+
+  explicit HideSpecStmt(EmptyShell Empty)
+      : Stmt(HideSpecStmtClass), Function(nullptr) {}
+
+  Expr *getFunction() const { return cast<Expr>(Function); }
+  SourceLocation getLParenLoc() const { return LParenLoc; }
+  SourceLocation getBeginLoc() const LLVM_READONLY { return Loc; }
+  SourceLocation getEndLoc() const LLVM_READONLY { return RParenLoc; }
+
+  static bool classof(const Stmt *T) {
+    return T->getStmtClass() == HideSpecStmtClass;
+  }
+
+  child_range children() { return child_range(&Function, &Function + 1); }
+  const_child_range children() const {
+    return const_child_range(&Function, &Function + 1);
+  }
+};
+
+/// RevealSpecStmt - ghost { reveal(fn); } — inline spec body with default fuel.
+class RevealSpecStmt : public Stmt {
+  friend class ASTStmtReader;
+  SourceLocation Loc;
+  SourceLocation LParenLoc;
+  SourceLocation RParenLoc;
+  Stmt *Function;
+
+public:
+  RevealSpecStmt(SourceLocation Loc, SourceLocation LParenLoc,
+                 SourceLocation RParenLoc, Expr *Function)
+      : Stmt(RevealSpecStmtClass), Loc(Loc), LParenLoc(LParenLoc),
+        RParenLoc(RParenLoc), Function(Function) {}
+
+  explicit RevealSpecStmt(EmptyShell Empty)
+      : Stmt(RevealSpecStmtClass), Function(nullptr) {}
+
+  Expr *getFunction() const { return cast<Expr>(Function); }
+  SourceLocation getLParenLoc() const { return LParenLoc; }
+  SourceLocation getBeginLoc() const LLVM_READONLY { return Loc; }
+  SourceLocation getEndLoc() const LLVM_READONLY { return RParenLoc; }
+
+  static bool classof(const Stmt *T) {
+    return T->getStmtClass() == RevealSpecStmtClass;
+  }
+
+  child_range children() { return child_range(&Function, &Function + 1); }
+  const_child_range children() const {
+    return const_child_range(&Function, &Function + 1);
+  }
+};
+
 } // namespace clang
 
 #endif // LLVM_CLANG_AST_STMTCONTRACT_H

clang/include/clang/Basic/StmtNodes.td

@@ -342,6 +342,8 @@ def HLSLOutArgExpr : StmtNode<Expr>;
 def ContractAssertStmt : StmtNode<Stmt>;
 def GhostBlockStmt : StmtNode<Stmt>;
 def RevealWithFuelStmt : StmtNode<Stmt>;
+def HideSpecStmt : StmtNode<Stmt>;
+def RevealSpecStmt : StmtNode<Stmt>;
 def ForallExpr : StmtNode<Expr>;
 def ExistsExpr : StmtNode<Expr>;
 def OldExpr : StmtNode<Expr>;

clang/include/clang/Basic/TokenKinds.def

@@ -463,6 +463,8 @@ KEYWORD(modifies                      , KEYCONTRACT)
 KEYWORD(aliases                       , KEYCONTRACT)
 KEYWORD(recommends                    , KEYCONTRACT)
 KEYWORD(reveal_with_fuel              , KEYCONTRACT)
+KEYWORD(hide                          , KEYCONTRACT)
+KEYWORD(reveal                        , KEYCONTRACT)
 
 // ISO/IEC JTC1 SC22 WG14 N1169 Extension
 KEYWORD(_Accum                      , KEYFIXEDPOINT)

clang/include/clang/Parse/Parser.h

@@ -7465,6 +7465,8 @@ class Parser : public CodeCompletionHandler {
 
   /// Parse reveal_with_fuel(fn, depth);
   StmtResult ParseRevealWithFuel();
+  StmtResult ParseHideSpec();
+  StmtResult ParseRevealSpec();
 
   /// Parse forall(binder, lo, hi, body) or exists(binder, lo, hi, body).
   ExprResult ParseQuantifierExpr();

clang/include/clang/Serialization/ASTBitCodes.h

@@ -2070,6 +2070,8 @@ enum StmtCode {
   STMT_CONTRACT_ASSERT,
   STMT_GHOST_BLOCK,
   STMT_REVEAL_WITH_FUEL,
+  STMT_HIDE_SPEC,
+  STMT_REVEAL_SPEC,
   EXPR_FORALL,
   EXPR_EXISTS,
   EXPR_OLD,

clang/lib/AST/StmtPrinter.cpp

@@ -621,6 +621,18 @@ void StmtPrinter::VisitRevealWithFuelStmt(RevealWithFuelStmt *Node) {
   OS << ");\n";
 }
 
+void StmtPrinter::VisitHideSpecStmt(HideSpecStmt *Node) {
+  Indent() << "hide(";
+  PrintExpr(Node->getFunction());
+  OS << ");\n";
+}
+
+void StmtPrinter::VisitRevealSpecStmt(RevealSpecStmt *Node) {
+  Indent() << "reveal(";
+  PrintExpr(Node->getFunction());
+  OS << ");\n";
+}
+
 void StmtPrinter::VisitForallExpr(ForallExpr *Node) {
   OS << "forall(" << Node->getBoundVar()->getName() << ", ";
   PrintExpr(Node->getLo());

clang/lib/AST/StmtProfile.cpp

@@ -408,6 +408,10 @@ void StmtProfiler::VisitRevealWithFuelStmt(const RevealWithFuelStmt *S) {
   VisitStmt(S);
 }
 
+void StmtProfiler::VisitHideSpecStmt(const HideSpecStmt *S) { VisitStmt(S); }
+
+void StmtProfiler::VisitRevealSpecStmt(const RevealSpecStmt *S) { VisitStmt(S); }
+
 void StmtProfiler::VisitForallExpr(const ForallExpr *E) {
   VisitExpr(E);
 }

clang/lib/CodeGen/CGStmt.cpp

@@ -109,6 +109,8 @@ void CodeGenFunction::EmitStmt(const Stmt *S, ArrayRef<const Attr *> Attrs) {
   case Stmt::GhostBlockStmtClass:
   case Stmt::ContractAssertStmtClass:
   case Stmt::RevealWithFuelStmtClass:
+  case Stmt::HideSpecStmtClass:
+  case Stmt::RevealSpecStmtClass:
     break;
 
   case Stmt::NullStmtClass:

clang/lib/Parse/ParseStmt.cpp

@@ -296,6 +296,14 @@ StmtResult Parser::ParseStatementOrDeclarationAfterAttributes(
     Res = ParseRevealWithFuel();
     SemiError = "reveal_with_fuel";
     break;
+  case tok::kw_hide:
+    Res = ParseHideSpec();
+    SemiError = "hide";
+    break;
+  case tok::kw_reveal:
+    Res = ParseRevealSpec();
+    SemiError = "reveal";
+    break;
 
   case tok::kw_while:               // C99 6.8.5.1: while-statement
     return ParseWhileStatement(TrailingElseLoc, PrecedingLabel);
@@ -2896,3 +2904,51 @@ StmtResult Parser::ParseRevealWithFuel() {
   return new (Actions.getASTContext())
       RevealWithFuelStmt(Loc, LParenLoc, RParenLoc, Fn.get(), Fuel.get());
 }
+
+/// Parse hide(fn);
+StmtResult Parser::ParseHideSpec() {
+  assert(Tok.is(tok::kw_hide) && "Expected 'hide'");
+  SourceLocation Loc = ConsumeToken();
+  if (Tok.isNot(tok::l_paren)) {
+    Diag(Tok, diag::err_contract_expected_lparen) << "hide";
+    return StmtError();
+  }
+  SourceLocation LParenLoc = ConsumeParen();
+  ExprResult Fn = ParseAssignmentExpression();
+  if (Fn.isInvalid()) {
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return StmtError();
+  }
+  if (Tok.isNot(tok::r_paren)) {
+    Diag(Tok, diag::err_contract_expected_rparen) << "hide";
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return StmtError();
+  }
+  SourceLocation RParenLoc = ConsumeParen();
+  return new (Actions.getASTContext())
+      HideSpecStmt(Loc, LParenLoc, RParenLoc, Fn.get());
+}
+
+/// Parse reveal(fn);
+StmtResult Parser::ParseRevealSpec() {
+  assert(Tok.is(tok::kw_reveal) && "Expected 'reveal'");
+  SourceLocation Loc = ConsumeToken();
+  if (Tok.isNot(tok::l_paren)) {
+    Diag(Tok, diag::err_contract_expected_lparen) << "reveal";
+    return StmtError();
+  }
+  SourceLocation LParenLoc = ConsumeParen();
+  ExprResult Fn = ParseAssignmentExpression();
+  if (Fn.isInvalid()) {
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return StmtError();
+  }
+  if (Tok.isNot(tok::r_paren)) {
+    Diag(Tok, diag::err_contract_expected_rparen) << "reveal";
+    SkipUntil(tok::r_paren, StopAtSemi);
+    return StmtError();
+  }
+  SourceLocation RParenLoc = ConsumeParen();
+  return new (Actions.getASTContext())
+      RevealSpecStmt(Loc, LParenLoc, RParenLoc, Fn.get());
+}

clang/lib/Sema/TreeTransform.h

@@ -17949,6 +17949,28 @@ StmtResult TreeTransform<Derived>::TransformRevealWithFuelStmt(
                          Fn.getAs<Expr>(), Fuel.getAs<Expr>());
 }
 
+template <typename Derived>
+StmtResult TreeTransform<Derived>::TransformHideSpecStmt(HideSpecStmt *S) {
+  ExprResult Fn = getDerived().TransformExpr(S->getFunction());
+  if (Fn.isInvalid())
+    return StmtError();
+  if (!getDerived().AlwaysRebuild() && Fn.get() == S->getFunction())
+    return S;
+  return new (SemaRef.Context)
+      HideSpecStmt(S->getBeginLoc(), S->getLParenLoc(), S->getEndLoc(), Fn.get());
+}
+
+template <typename Derived>
+StmtResult TreeTransform<Derived>::TransformRevealSpecStmt(RevealSpecStmt *S) {
+  ExprResult Fn = getDerived().TransformExpr(S->getFunction());
+  if (Fn.isInvalid())
+    return StmtError();
+  if (!getDerived().AlwaysRebuild() && Fn.get() == S->getFunction())
+    return S;
+  return new (SemaRef.Context)
+      RevealSpecStmt(S->getBeginLoc(), S->getLParenLoc(), S->getEndLoc(), Fn.get());
+}
+
 template <typename Derived>
 ExprResult TreeTransform<Derived>::TransformForallExpr(ForallExpr *E) {
   ExprResult Lo = getDerived().TransformExpr(E->getLo());

clang/lib/Serialization/ASTReaderStmt.cpp

@@ -3017,6 +3017,22 @@ void ASTStmtReader::VisitRevealWithFuelStmt(RevealWithFuelStmt *S) {
   S->RParenLoc = readSourceLocation();
 }
 
+void ASTStmtReader::VisitHideSpecStmt(HideSpecStmt *S) {
+  VisitStmt(S);
+  S->Function = Record.readSubStmt();
+  S->Loc = readSourceLocation();
+  S->LParenLoc = readSourceLocation();
+  S->RParenLoc = readSourceLocation();
+}
+
+void ASTStmtReader::VisitRevealSpecStmt(RevealSpecStmt *S) {
+  VisitStmt(S);
+  S->Function = Record.readSubStmt();
+  S->Loc = readSourceLocation();
+  S->LParenLoc = readSourceLocation();
+  S->RParenLoc = readSourceLocation();
+}
+
 void ASTStmtReader::VisitForallExpr(ForallExpr *E) {
   VisitExpr(E);
   E->BoundVar = readDeclAs<VarDecl>();
@@ -4617,6 +4633,12 @@ Stmt *ASTReader::ReadStmtFromStream(ModuleFile &F) {
     case STMT_REVEAL_WITH_FUEL:
       S = new (Context) RevealWithFuelStmt(Empty);
       break;
+    case STMT_HIDE_SPEC:
+      S = new (Context) HideSpecStmt(Empty);
+      break;
+    case STMT_REVEAL_SPEC:
+      S = new (Context) RevealSpecStmt(Empty);
+      break;
     case EXPR_FORALL:
       S = new (Context) ForallExpr(Empty);
       break;

clang/lib/Serialization/ASTWriterStmt.cpp

@@ -3120,6 +3120,24 @@ void ASTStmtWriter::VisitRevealWithFuelStmt(RevealWithFuelStmt *S) {
   Code = serialization::STMT_REVEAL_WITH_FUEL;
 }
 
+void ASTStmtWriter::VisitHideSpecStmt(HideSpecStmt *S) {
+  VisitStmt(S);
+  Record.AddStmt(S->getFunction());
+  Record.AddSourceLocation(S->getBeginLoc());
+  Record.AddSourceLocation(S->getLParenLoc());
+  Record.AddSourceLocation(S->getEndLoc());
+  Code = serialization::STMT_HIDE_SPEC;
+}
+
+void ASTStmtWriter::VisitRevealSpecStmt(RevealSpecStmt *S) {
+  VisitStmt(S);
+  Record.AddStmt(S->getFunction());
+  Record.AddSourceLocation(S->getBeginLoc());
+  Record.AddSourceLocation(S->getLParenLoc());
+  Record.AddSourceLocation(S->getEndLoc());
+  Code = serialization::STMT_REVEAL_SPEC;
+}
+
 void ASTStmtWriter::VisitForallExpr(ForallExpr *E) {
   VisitExpr(E);
   Record.AddDeclRef(E->getBoundVar());