diff --git a/README.md b/README.md index 662e724eee..528d368a8d 100644 --- a/README.md +++ b/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. \ No newline at end of file diff --git a/clang/include/clang/AST/RecursiveASTVisitor.h b/clang/include/clang/AST/RecursiveASTVisitor.h index 470cc5a1d7..8ff39c553f 100644 --- a/clang/include/clang/AST/RecursiveASTVisitor.h +++ b/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, {}) diff --git a/clang/include/clang/AST/StmtContract.h b/clang/include/clang/AST/StmtContract.h index 8447b5a13e..e132bdfab4 100644 --- a/clang/include/clang/AST/StmtContract.h +++ b/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(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(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 diff --git a/clang/include/clang/Basic/StmtNodes.td b/clang/include/clang/Basic/StmtNodes.td index 1d651f6c88..a7e583d5a4 100644 --- a/clang/include/clang/Basic/StmtNodes.td +++ b/clang/include/clang/Basic/StmtNodes.td @@ -342,6 +342,8 @@ def HLSLOutArgExpr : StmtNode; def ContractAssertStmt : StmtNode; def GhostBlockStmt : StmtNode; def RevealWithFuelStmt : StmtNode; +def HideSpecStmt : StmtNode; +def RevealSpecStmt : StmtNode; def ForallExpr : StmtNode; def ExistsExpr : StmtNode; def OldExpr : StmtNode; diff --git a/clang/include/clang/Basic/TokenKinds.def b/clang/include/clang/Basic/TokenKinds.def index 186e70f6c6..07d9452531 100644 --- a/clang/include/clang/Basic/TokenKinds.def +++ b/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) diff --git a/clang/include/clang/Parse/Parser.h b/clang/include/clang/Parse/Parser.h index 1030a736fc..63b9c5f9a0 100644 --- a/clang/include/clang/Parse/Parser.h +++ b/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(); diff --git a/clang/include/clang/Serialization/ASTBitCodes.h b/clang/include/clang/Serialization/ASTBitCodes.h index ce90581d4a..6f8c6d97ba 100644 --- a/clang/include/clang/Serialization/ASTBitCodes.h +++ b/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, diff --git a/clang/lib/AST/StmtPrinter.cpp b/clang/lib/AST/StmtPrinter.cpp index f1ece93aa0..3817bddb6f 100644 --- a/clang/lib/AST/StmtPrinter.cpp +++ b/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()); diff --git a/clang/lib/AST/StmtProfile.cpp b/clang/lib/AST/StmtProfile.cpp index a1a3656f50..33be82c773 100644 --- a/clang/lib/AST/StmtProfile.cpp +++ b/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); } diff --git a/clang/lib/CodeGen/CGStmt.cpp b/clang/lib/CodeGen/CGStmt.cpp index 4e0725ad17..61240929c5 100644 --- a/clang/lib/CodeGen/CGStmt.cpp +++ b/clang/lib/CodeGen/CGStmt.cpp @@ -109,6 +109,8 @@ void CodeGenFunction::EmitStmt(const Stmt *S, ArrayRef Attrs) { case Stmt::GhostBlockStmtClass: case Stmt::ContractAssertStmtClass: case Stmt::RevealWithFuelStmtClass: + case Stmt::HideSpecStmtClass: + case Stmt::RevealSpecStmtClass: break; case Stmt::NullStmtClass: diff --git a/clang/lib/Parse/ParseStmt.cpp b/clang/lib/Parse/ParseStmt.cpp index 6b934b19df..70c3956ac3 100644 --- a/clang/lib/Parse/ParseStmt.cpp +++ b/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()); +} diff --git a/clang/lib/Sema/TreeTransform.h b/clang/lib/Sema/TreeTransform.h index 2c8a41e34b..17ac675ff4 100644 --- a/clang/lib/Sema/TreeTransform.h +++ b/clang/lib/Sema/TreeTransform.h @@ -17949,6 +17949,28 @@ StmtResult TreeTransform::TransformRevealWithFuelStmt( Fn.getAs(), Fuel.getAs()); } +template +StmtResult TreeTransform::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 +StmtResult TreeTransform::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 ExprResult TreeTransform::TransformForallExpr(ForallExpr *E) { ExprResult Lo = getDerived().TransformExpr(E->getLo()); diff --git a/clang/lib/Serialization/ASTReaderStmt.cpp b/clang/lib/Serialization/ASTReaderStmt.cpp index b432bd2490..b05113fa33 100644 --- a/clang/lib/Serialization/ASTReaderStmt.cpp +++ b/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(); @@ -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; diff --git a/clang/lib/Serialization/ASTWriterStmt.cpp b/clang/lib/Serialization/ASTWriterStmt.cpp index 35a47b9de6..84eab4e45f 100644 --- a/clang/lib/Serialization/ASTWriterStmt.cpp +++ b/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()); diff --git a/clang/lib/Verify/Backend/LeanBackend.cpp b/clang/lib/Verify/Backend/LeanBackend.cpp new file mode 100644 index 0000000000..045ff17dc8 --- /dev/null +++ b/clang/lib/Verify/Backend/LeanBackend.cpp @@ -0,0 +1,199 @@ +//===--- LeanBackend.cpp --------------------------------------------------===// +#include "LeanBackend.h" +#include "VCMachine.h" +#include "Z3Encode.h" +#include "llvm/Support/raw_ostream.h" + +using namespace clang; +using namespace verify; + +static void printVCExprLean(const VCExpr *E, llvm::raw_ostream &OS, unsigned Prec = 0) { + if (!E) { + OS << "True"; + return; + } + auto paren = [&](unsigned P, auto Fn) { + if (Prec > P) + OS << "("; + Fn(); + if (Prec > P) + OS << ")"; + }; + switch (E->K) { + case VCExpr::True: + OS << "True"; + break; + case VCExpr::False: + OS << "False"; + break; + case VCExpr::BoolLit: + OS << (E->BoolVal ? "True" : "False"); + break; + case VCExpr::IntLit: + OS << E->IntVal; + break; + case VCExpr::Var: + for (char C : E->Name) { + if (C == '.') + OS << "_"; + else + OS << C; + } + break; + case VCExpr::Not: + OS << "¬"; + printVCExprLean(E->Children[0].get(), OS, 10); + break; + case VCExpr::And: + paren(3, [&] { + for (unsigned I = 0; I < E->Children.size(); ++I) { + if (I) + OS << " ∧ "; + printVCExprLean(E->Children[I].get(), OS, 3); + } + }); + break; + case VCExpr::Or: + paren(2, [&] { + for (unsigned I = 0; I < E->Children.size(); ++I) { + if (I) + OS << " ∨ "; + printVCExprLean(E->Children[I].get(), OS, 2); + } + }); + break; + case VCExpr::Ite: + paren(1, [&] { + OS << "if "; + printVCExprLean(E->Children[0].get(), OS, 0); + OS << " then "; + printVCExprLean(E->Children[1].get(), OS, 0); + OS << " else "; + printVCExprLean(E->Children[2].get(), OS, 0); + }); + break; + case VCExpr::Eq: + paren(5, [&] { + printVCExprLean(E->Children[0].get(), OS, 5); + OS << " = "; + printVCExprLean(E->Children[1].get(), OS, 5); + }); + break; + case VCExpr::Ne: + paren(5, [&] { + printVCExprLean(E->Children[0].get(), OS, 5); + OS << " ≠ "; + printVCExprLean(E->Children[1].get(), OS, 5); + }); + break; + case VCExpr::Lt: + paren(6, [&] { + printVCExprLean(E->Children[0].get(), OS, 6); + OS << " < "; + printVCExprLean(E->Children[1].get(), OS, 6); + }); + break; + case VCExpr::Le: + paren(6, [&] { + printVCExprLean(E->Children[0].get(), OS, 6); + OS << " ≤ "; + printVCExprLean(E->Children[1].get(), OS, 6); + }); + break; + case VCExpr::Gt: + paren(6, [&] { + printVCExprLean(E->Children[0].get(), OS, 6); + OS << " > "; + printVCExprLean(E->Children[1].get(), OS, 6); + }); + break; + case VCExpr::Ge: + paren(6, [&] { + printVCExprLean(E->Children[0].get(), OS, 6); + OS << " ≥ "; + printVCExprLean(E->Children[1].get(), OS, 6); + }); + break; + case VCExpr::Add: + paren(7, [&] { + printVCExprLean(E->Children[0].get(), OS, 7); + OS << " + "; + printVCExprLean(E->Children[1].get(), OS, 7); + }); + break; + case VCExpr::Sub: + paren(7, [&] { + printVCExprLean(E->Children[0].get(), OS, 7); + OS << " - "; + printVCExprLean(E->Children[1].get(), OS, 7); + }); + break; + case VCExpr::Mul: + paren(8, [&] { + printVCExprLean(E->Children[0].get(), OS, 8); + OS << " * "; + printVCExprLean(E->Children[1].get(), OS, 8); + }); + break; + case VCExpr::Neg: + OS << "-"; + printVCExprLean(E->Children[0].get(), OS, 9); + break; + case VCExpr::Select: + OS << "heapSelect "; + printVCExprLean(E->Children[0].get(), OS, 0); + OS << " "; + printVCExprLean(E->Children[1].get(), OS, 0); + break; + case VCExpr::Store: + OS << "heapStore "; + printVCExprLean(E->Children[0].get(), OS, 0); + OS << " "; + printVCExprLean(E->Children[1].get(), OS, 0); + OS << " "; + printVCExprLean(E->Children[2].get(), OS, 0); + OS << " "; + printVCExprLean(E->Children[3].get(), OS, 0); + break; + case VCExpr::Forall: + OS << "True"; + break; + } +} + +VerifyResult verify::exportLeanScratchPad(const PassiveProgram &P, + llvm::raw_ostream &OS) { + VCMachine M = VCMachine::fromPassive(P); + Z3VerifyBackend Z3; + VerifyResult Z3R = Z3.verifyPassive(P); + + OS << "/- Generated by CppVerify (Lean scratch-pad). Proof obligations only. -/\n"; + OS << "/- Z3 check: "; + switch (Z3R.Status) { + case VerifyStatus::Verified: + OS << "verified"; + break; + case VerifyStatus::Failed: + OS << "failed"; + if (!Z3R.Message.empty()) + OS << " — counterexample hint: " << Z3R.Message; + break; + default: + OS << "unknown"; + break; + } + OS << " -/\n\n"; + + OS << "def heapSelect (h : Array Int Int) (p : Int) : Int := h[p]!\n"; + OS << "def heapStore (h : Array Int Int) (p : Int) (v : Int) (h' : Array Int Int) : Prop :=\n"; + OS << " h' = h.set! p v\n\n"; + + OS << "theorem cppverify_goal : "; + printVCExprLean(M.Goal.get(), OS); + OS << " := by\n sorry\n"; + + VerifyResult R; + R.Status = VerifyStatus::Verified; + R.Message = "lean export written"; + return R; +} \ No newline at end of file diff --git a/clang/lib/Verify/Backend/LeanBackend.h b/clang/lib/Verify/Backend/LeanBackend.h new file mode 100644 index 0000000000..c13b71cd97 --- /dev/null +++ b/clang/lib/Verify/Backend/LeanBackend.h @@ -0,0 +1,17 @@ +//===--- LeanBackend.h - Lean scratch-pad export ------------------------===// +#ifndef LLVM_CLANG_VERIFY_BACKEND_LEANBACKEND_H +#define LLVM_CLANG_VERIFY_BACKEND_LEANBACKEND_H + +#include "VerifyBackend.h" +#include "llvm/Support/raw_ostream.h" + +namespace clang { +namespace verify { + +VerifyResult exportLeanScratchPad(const PassiveProgram &P, + llvm::raw_ostream &OS); + +} // namespace verify +} // namespace clang + +#endif \ No newline at end of file diff --git a/clang/lib/Verify/Backend/SpecAxioms.cpp b/clang/lib/Verify/Backend/SpecAxioms.cpp new file mode 100644 index 0000000000..04b4cd2914 --- /dev/null +++ b/clang/lib/Verify/Backend/SpecAxioms.cpp @@ -0,0 +1,51 @@ +//===--- SpecAxioms.cpp - Verus-style spec defining axioms ----------------===// +#include "SpecAxioms.h" +#include "../Transform/SpecInline.h" +#include "Z3Encode.h" + +using namespace clang; +using namespace verify; + +static void collectReferencedSpecsVC(const VCExpr *E, std::set &Out) { + if (!E) + return; + if (E->K == VCExpr::SpecCall) + Out.insert(E->SpecCallee); + for (const auto &C : E->Children) + collectReferencedSpecsVC(C.get(), Out); +} + +void verify::collectReferencedSpecs(const VExpr *E, std::set &Out) { + std::vector Calls; + collectSpecCalls(E, Calls); + for (const VSpecCallExpr *C : Calls) + Out.insert(C->Callee); +} + +static unsigned axiomFuelFor(const VFunction &Spec, const SpecAxiomContext &Ctx) { + if (Ctx.HiddenSpecs.count(Spec.Name)) + return 0; + if (auto It = Ctx.SpecFuel.find(Spec.Name); It != Ctx.SpecFuel.end()) + return It->second; + if (Ctx.RevealedSpecs.count(Spec.Name)) + return 1; + if (!Spec.NeedsDecreasesCheck) + return 64; + return 0; +} + +std::unique_ptr verify::unfoldSpecDefinition(const VFunction &Spec, + const SpecAxiomContext &Ctx, + unsigned Fuel) { + SpecInliner Inliner(Ctx.Functions, Ctx.SpecFuel); + return Inliner.unfoldDefinition(Spec, Ctx.SpecFuel, Ctx.HiddenSpecs, + Ctx.RevealedSpecs, Fuel); +} + +void verify::emitSpecAxioms(Z3Encoder &Enc, const VCExpr *Goal, + const SpecAxiomContext &Ctx) { + std::set Used; + collectReferencedSpecsVC(Goal, Used); + for (const auto &Name : Used) + Enc.emitSpecDefiningAxiom(Name, Ctx); +} \ No newline at end of file diff --git a/clang/lib/Verify/Backend/SpecAxioms.h b/clang/lib/Verify/Backend/SpecAxioms.h new file mode 100644 index 0000000000..9255d7e2c5 --- /dev/null +++ b/clang/lib/Verify/Backend/SpecAxioms.h @@ -0,0 +1,36 @@ +//===--- SpecAxioms.h - Verus-style spec SMT axiom generation -------------===// +#ifndef LLVM_CLANG_VERIFY_BACKEND_SPECAXIOMS_H +#define LLVM_CLANG_VERIFY_BACKEND_SPECAXIOMS_H + +#include "../Transform/Passivize.h" +#include "VCMachine.h" +#include +#include + +namespace clang { +namespace verify { + +struct SpecAxiomContext { + FunctionMap Functions; + std::map SpecFuel; + std::set HiddenSpecs; + std::set RevealedSpecs; + VIntMode CallerIntMode = VIntMode::Machine; +}; + +/// Collect names of spec functions referenced by VSpecCallExpr in E. +void collectReferencedSpecs(const VExpr *E, std::set &Out); + +/// Unfold a spec definition for axiom emission (fuel-limited; no call-site args). +std::unique_ptr unfoldSpecDefinition(const VFunction &Spec, + const SpecAxiomContext &Ctx, + unsigned Fuel); + +/// Emit defining axioms into Z3 for specs referenced in the VC. +void emitSpecAxioms(class Z3Encoder &Enc, const VCExpr *Goal, + const SpecAxiomContext &Ctx); + +} // namespace verify +} // namespace clang + +#endif \ No newline at end of file diff --git a/clang/lib/Verify/Backend/VCMachine.cpp b/clang/lib/Verify/Backend/VCMachine.cpp new file mode 100644 index 0000000000..14116576e1 --- /dev/null +++ b/clang/lib/Verify/Backend/VCMachine.cpp @@ -0,0 +1,331 @@ +//===--- VCMachine.cpp ----------------------------------------------------===// +#include "VCMachine.h" +#include "../IR/VType.h" + +using namespace clang; +using namespace verify; + +static std::unique_ptr vcTrue() { + return std::make_unique(VCExpr::True); +} + +static std::unique_ptr vcAnd(std::unique_ptr A, + std::unique_ptr B) { + if (!A) + return B; + if (!B) + return A; + auto N = std::make_unique(VCExpr::And); + N->Children.push_back(std::move(A)); + N->Children.push_back(std::move(B)); + return N; +} + +static std::unique_ptr vcNot(std::unique_ptr E) { + auto N = std::make_unique(VCExpr::Not); + N->Children.push_back(std::move(E)); + return N; +} + +static std::unique_ptr vcOr(std::unique_ptr A, + std::unique_ptr B) { + if (!A) + return B; + if (!B) + return A; + auto N = std::make_unique(VCExpr::Or); + N->Children.push_back(std::move(A)); + N->Children.push_back(std::move(B)); + return N; +} + +static int64_t evalIntLiteral(const VExpr *E) { + if (!E || E->K != VExpr::Literal) + return 0; + return static_cast(E)->Value; +} + +class VCMachineBuilder { + std::string ResultVarName; + std::string CurHeap; + + static VIntMode intModeOf(const VCExpr *E) { + if (!E) + return VIntMode::Machine; + return E->IntMode; + } + + static VIntMode intModeOfVType(const VType &Ty) { + if (Ty.Kind == VTypeKind::Int32 || Ty.Kind == VTypeKind::Int64) + return Ty.IntMode; + return VIntMode::Machine; + } + + std::unique_ptr toMode(std::unique_ptr E, VIntMode Target) { + if (!E || intModeOf(E.get()) == Target) + return E; + auto N = std::make_unique( + Target == VIntMode::Machine ? VCExpr::IntToBv : VCExpr::BvToInt); + N->IntMode = Target; + N->Children.push_back(std::move(E)); + return N; + } + + std::pair, std::unique_ptr> + unifyIntModes(std::unique_ptr L, std::unique_ptr R) { + VIntMode M = intModeOf(L.get()); + if (intModeOf(R.get()) == VIntMode::Math) + M = VIntMode::Math; + return {toMode(std::move(L), M), toMode(std::move(R), M)}; + } + + std::unique_ptr fromBin(VBinOp Op, std::unique_ptr L, + std::unique_ptr R) { + VCExpr::Kind K = VCExpr::Eq; + switch (Op) { + case VBinOp::Add: + K = VCExpr::Add; + break; + case VBinOp::Sub: + K = VCExpr::Sub; + break; + case VBinOp::Mul: + K = VCExpr::Mul; + break; + case VBinOp::Lt: + K = VCExpr::Lt; + break; + case VBinOp::Le: + K = VCExpr::Le; + break; + case VBinOp::Gt: + K = VCExpr::Gt; + break; + case VBinOp::Ge: + K = VCExpr::Ge; + break; + case VBinOp::Eq: + K = VCExpr::Eq; + break; + case VBinOp::Ne: + K = VCExpr::Ne; + break; + case VBinOp::And: + K = VCExpr::And; + break; + case VBinOp::Or: + K = VCExpr::Or; + break; + default: + K = VCExpr::Eq; + break; + } + auto Unified = unifyIntModes(std::move(L), std::move(R)); + auto N = std::make_unique(K); + N->IntMode = intModeOf(Unified.first.get()); + N->Children.push_back(std::move(Unified.first)); + N->Children.push_back(std::move(Unified.second)); + return N; + } + + std::unique_ptr expandQuant(const VQuantifiedExpr *Q, bool IsForall) { + int64_t Lo = evalIntLiteral(Q->Lo.get()); + int64_t Hi = evalIntLiteral(Q->Hi.get()); + if (Hi <= Lo) + return std::make_unique(IsForall ? VCExpr::True : VCExpr::False); + std::unique_ptr Acc = + std::make_unique(IsForall ? VCExpr::True : VCExpr::False); + VIntMode Mode = intModeOfVType(Q->Body->Ty); + for (int64_t I = Lo; I < Hi; ++I) { + auto InstBody = + substituteBinderInVExpr(Q->Body.get(), Q->Binder, I, Mode); + auto Body = fromVExpr(InstBody.get()); + if (IsForall) + Acc = vcAnd(std::move(Acc), std::move(Body)); + else + Acc = vcOr(std::move(Acc), std::move(Body)); + } + return Acc; + } + + VIntMode CallerIntMode = VIntMode::Machine; + bool ForceCallerIntMode = false; + +public: + VCMachineBuilder(std::string ResultVar, std::string Heap, VIntMode CallerMode, + bool ForceCallerMode = false) + : ResultVarName(std::move(ResultVar)), CurHeap(std::move(Heap)), + CallerIntMode(CallerMode), ForceCallerIntMode(ForceCallerMode) {} + + std::unique_ptr fromVExpr(const VExpr *E) { + if (!E) + return vcTrue(); + switch (E->K) { + case VExpr::Literal: { + const auto *L = static_cast(E); + if (L->Ty.Kind == VTypeKind::Bool) { + auto N = std::make_unique(VCExpr::BoolLit); + N->BoolVal = L->Value != 0; + return N; + } + auto N = std::make_unique(VCExpr::IntLit); + N->IntVal = L->Value; + N->IntMode = ForceCallerIntMode ? CallerIntMode + : intModeOfVType(L->Ty); + return N; + } + case VExpr::Var: { + auto N = std::make_unique(VCExpr::Var); + N->Name = static_cast(E)->Name; + N->IntMode = ForceCallerIntMode + ? CallerIntMode + : intModeOfVType(static_cast(E)->Ty); + return N; + } + case VExpr::BinOp: { + const auto *B = static_cast(E); + return fromBin(B->Op, fromVExpr(B->Lhs.get()), fromVExpr(B->Rhs.get())); + } + case VExpr::UnaryOp: { + const auto *U = static_cast(E); + if (U->Op == VUnaryOp::Neg) { + auto N = std::make_unique(VCExpr::Neg); + N->Children.push_back(fromVExpr(U->Operand.get())); + N->IntMode = intModeOf(N->Children[0].get()); + return N; + } + return vcNot(fromVExpr(U->Operand.get())); + } + case VExpr::Conditional: { + const auto *C = static_cast(E); + auto N = std::make_unique(VCExpr::Ite); + N->Children.push_back(fromVExpr(C->Cond.get())); + N->Children.push_back(fromVExpr(C->Then.get())); + N->Children.push_back(fromVExpr(C->Else.get())); + N->IntMode = intModeOf(N->Children[1].get()); + return N; + } + case VExpr::Result: { + auto N = std::make_unique(VCExpr::Var); + N->Name = ResultVarName.empty() ? "__result_0" : ResultVarName; + return N; + } + case VExpr::Old: + return fromVExpr(static_cast(E)->Inner.get()); + case VExpr::Cast: + return fromVExpr(static_cast(E)->Inner.get()); + case VExpr::Load: { + const auto *L = static_cast(E); + std::string Heap = L->HeapVar.empty() ? CurHeap : L->HeapVar; + auto N = std::make_unique(VCExpr::Select); + N->IntMode = CallerIntMode; + auto H = std::make_unique(VCExpr::Var); + H->Name = Heap; + N->Children.push_back(std::move(H)); + N->Children.push_back(fromVExpr(L->Ptr.get())); + return N; + } + case VExpr::Forall: + return expandQuant(static_cast(E), true); + case VExpr::Exists: + return expandQuant(static_cast(E), false); + case VExpr::HeapStore: { + const auto *H = static_cast(E); + auto N = std::make_unique(VCExpr::Store); + auto Before = std::make_unique(VCExpr::Var); + Before->Name = H->HeapBefore; + auto After = std::make_unique(VCExpr::Var); + After->Name = H->HeapAfter; + N->Children.push_back(std::move(Before)); + N->Children.push_back(fromVExpr(H->Ptr.get())); + N->Children.push_back(fromVExpr(H->Val.get())); + N->Children.push_back(std::move(After)); + return N; + } + case VExpr::FieldAccess: { + const auto *F = static_cast(E); + auto N = std::make_unique(VCExpr::Var); + N->Name = fieldVarName(F); + return N; + } + case VExpr::SpecCall: { + const auto *C = static_cast(E); + auto N = std::make_unique(VCExpr::SpecCall); + N->SpecCallee = C->Callee; + N->IntMode = CallerIntMode; + for (const auto &A : C->Args) + N->Children.push_back(fromVExpr(A.get())); + return N; + } + } + return vcTrue(); + } + + static std::string fieldVarName(const VFieldAccessExpr *F) { + std::string Base; + if (F->Base->K == VExpr::Var) + Base = static_cast(F->Base.get())->Name; + else if (F->Base->K == VExpr::Result) + Base = "result"; + else + Base = "base"; + return Base + "." + F->Field; + } + + VCMachine buildPassive(const PassiveProgram &P) { + VCMachine M; + M.ResultVarName = P.ResultVarName; + M.HeapPrefix = P.OldHeapName.empty() ? std::string(VHeapName) + "_0" : P.OldHeapName; + M.SpecFunctions = P.SpecFunctions; + M.SpecFuel = P.SpecFuel; + M.HiddenSpecs = P.HiddenSpecs; + M.RevealedSpecs = P.RevealedSpecs; + M.CallerIntMode = P.CallerIntMode; + CurHeap = M.HeapPrefix; + + std::unique_ptr Hyp = vcTrue(); + std::unique_ptr Post = vcTrue(); + + for (const auto &A : P.EntryAssumes) + Hyp = vcAnd(std::move(Hyp), fromVExpr(A.get())); + + for (const auto &S : P.Stmts) { + if (S->K == PassiveStmt::Assume && S->Cond) { + if (S->Cond->K == VExpr::HeapStore) { + auto *H = static_cast(S->Cond.get()); + Hyp = vcAnd(std::move(Hyp), fromVExpr(S->Cond.get())); + CurHeap = H->HeapAfter; + } else { + Hyp = vcAnd(std::move(Hyp), fromVExpr(S->Cond.get())); + } + } else if (S->K == PassiveStmt::Assert && S->Cond) { + Post = vcAnd(std::move(Post), fromVExpr(S->Cond.get())); + } + } + + for (const auto &A : P.ExitAsserts) + Post = vcAnd(std::move(Post), fromVExpr(A.get())); + + M.Goal = vcAnd(std::move(Hyp), vcNot(std::move(Post))); + return M; + } +}; + +VCMachine VCMachine::fromPassive(const PassiveProgram &P) { + VCMachineBuilder B(P.ResultVarName, + P.OldHeapName.empty() ? std::string(VHeapName) + "_0" + : P.OldHeapName, + P.CallerIntMode); + return B.buildPassive(P); +} + +VCMachine VCMachine::fromVExpr(const VExpr *E, const std::string &ResultVar, + const std::string &CurHeap, VIntMode CallerMode) { + VCMachineBuilder B(ResultVar, CurHeap, CallerMode, true); + VCMachine M; + M.ResultVarName = ResultVar; + M.HeapPrefix = CurHeap; + M.CallerIntMode = CallerMode; + M.Goal = B.fromVExpr(E); + return M; +} \ No newline at end of file diff --git a/clang/lib/Verify/Backend/VCMachine.h b/clang/lib/Verify/Backend/VCMachine.h new file mode 100644 index 0000000000..f2a4ff67f1 --- /dev/null +++ b/clang/lib/Verify/Backend/VCMachine.h @@ -0,0 +1,61 @@ +//===--- VCMachine.h - Backend-neutral verification formulas --------------===// +#ifndef LLVM_CLANG_VERIFY_BACKEND_VCMACHINE_H +#define LLVM_CLANG_VERIFY_BACKEND_VCMACHINE_H + +#include "../IR/VExpr.h" +#include "../IR/VType.h" +#include "../Transform/Passivize.h" +#include +#include +#include +#include +#include + +namespace clang { +namespace verify { + +/// Neutral logical formula for SMT, Lean export, and BMC. +class VCExpr { +public: + enum Kind { + True, False, IntLit, BoolLit, Var, Not, And, Or, Ite, + Eq, Ne, Lt, Le, Gt, Ge, Add, Sub, Mul, Neg, + Select, Store, Forall, IntToBv, BvToInt, SpecCall + }; + + Kind K; + VIntMode IntMode = VIntMode::Machine; + std::vector> Children; + int64_t IntVal = 0; + bool BoolVal = false; + std::string Name; + std::string Binder; + int64_t ForallLo = 0; + int64_t ForallHi = 0; + /// For SpecCall: function name (Args in Children). + std::string SpecCallee; + + explicit VCExpr(Kind K) : K(K) {} +}; + +class VCMachine { +public: + std::unique_ptr Goal; + std::string ResultVarName; + std::string HeapPrefix; + FunctionMap SpecFunctions; + std::map SpecFuel; + std::set HiddenSpecs; + std::set RevealedSpecs; + VIntMode CallerIntMode = VIntMode::Machine; + + static VCMachine fromPassive(const PassiveProgram &P); + static VCMachine fromVExpr(const VExpr *E, const std::string &ResultVar, + const std::string &CurHeap, + VIntMode CallerMode = VIntMode::Math); +}; + +} // namespace verify +} // namespace clang + +#endif \ No newline at end of file diff --git a/clang/lib/Verify/Backend/VerifyBackend.cpp b/clang/lib/Verify/Backend/VerifyBackend.cpp new file mode 100644 index 0000000000..ff8509e77e --- /dev/null +++ b/clang/lib/Verify/Backend/VerifyBackend.cpp @@ -0,0 +1,50 @@ +//===--- VerifyBackend.cpp ------------------------------------------------===// +#include "VerifyBackend.h" +#include "LeanBackend.h" +#include "Z3Encode.h" + +using namespace clang; +using namespace verify; + +namespace { +class LeanVerifyBackend : public VerifyBackend { + llvm::raw_ostream *Out; + +public: + explicit LeanVerifyBackend(llvm::raw_ostream *OS) : Out(OS) {} + llvm::StringRef getName() const override { return "lean"; } + VerifyResult verifyPassive(const PassiveProgram &P) override { + VerifyResult R; + if (!Out) { + R.Status = VerifyStatus::Unknown; + R.Message = "no lean output stream"; + return R; + } + return exportLeanScratchPad(P, *Out); + } +}; + +class BMCVerifyBackend : public VerifyBackend { + std::unique_ptr Z3 = std::make_unique(); + +public: + llvm::StringRef getName() const override { return "bmc"; } + VerifyResult verifyPassive(const PassiveProgram &P) override { + return Z3->verifyPassive(P); + } +}; +} // namespace + +std::unique_ptr +verify::createVerifyBackend(BackendKind K, llvm::raw_ostream *LeanOut, + unsigned /*BMCUnroll*/) { + switch (K) { + case BackendKind::Z3: + return std::make_unique(); + case BackendKind::Lean: + return std::make_unique(LeanOut); + case BackendKind::BMC: + return std::make_unique(); + } + return std::make_unique(); +} \ No newline at end of file diff --git a/clang/lib/Verify/Backend/VerifyBackend.h b/clang/lib/Verify/Backend/VerifyBackend.h new file mode 100644 index 0000000000..2888e1cd44 --- /dev/null +++ b/clang/lib/Verify/Backend/VerifyBackend.h @@ -0,0 +1,37 @@ +//===--- VerifyBackend.h - Pluggable verification backends --------------===// +#ifndef LLVM_CLANG_VERIFY_BACKEND_VERIFYBACKEND_H +#define LLVM_CLANG_VERIFY_BACKEND_VERIFYBACKEND_H + +#include "../Transform/Passivize.h" +#include +#include +#include + +namespace clang { +namespace verify { + +enum class VerifyStatus { Verified, Failed, Unknown }; + +struct VerifyResult { + VerifyStatus Status = VerifyStatus::Unknown; + std::string Message; + std::map Model; +}; + +class VerifyBackend { +public: + virtual ~VerifyBackend() = default; + virtual llvm::StringRef getName() const = 0; + virtual VerifyResult verifyPassive(const PassiveProgram &P) = 0; +}; + +enum class BackendKind { Z3, Lean, BMC }; + +std::unique_ptr +createVerifyBackend(BackendKind K, llvm::raw_ostream *LeanOut = nullptr, + unsigned BMCUnroll = 10); + +} // namespace verify +} // namespace clang + +#endif \ No newline at end of file diff --git a/clang/lib/Verify/Backend/Z3Encode.cpp b/clang/lib/Verify/Backend/Z3Encode.cpp index a61c11eaac..aeada20242 100644 --- a/clang/lib/Verify/Backend/Z3Encode.cpp +++ b/clang/lib/Verify/Backend/Z3Encode.cpp @@ -1,6 +1,8 @@ //===--- Z3Encode.cpp -----------------------------------------------------===// #include "Z3Encode.h" +#include "SpecAxioms.h" #include "llvm/Support/raw_ostream.h" +#include using namespace clang; using namespace verify; @@ -8,9 +10,66 @@ using namespace verify; Z3Encoder::Z3Encoder() : Ctx(), Solver(Ctx) {} z3::sort Z3Encoder::intSort() { return Ctx.int_sort(); } +z3::sort Z3Encoder::bvSort() { return Ctx.bv_sort(32); } z3::sort Z3Encoder::boolSort() { return Ctx.bool_sort(); } z3::sort Z3Encoder::heapSort() { return Ctx.array_sort(intSort(), intSort()); } +z3::sort Z3Encoder::valueSort(const VType &Ty, VIntMode Mode) { + if (Ty.Kind == VTypeKind::Bool) + return boolSort(); + if (Mode == VIntMode::Machine) + return bvSort(); + return intSort(); +} + +static std::string specZ3Name(const std::string &Fn, VIntMode Mode) { + return "spec$" + Fn + (Mode == VIntMode::Machine ? "$bv" : "$int"); +} + +static std::string specDeclKey(const std::string &Fn, VIntMode Mode) { + return Fn + (Mode == VIntMode::Machine ? "$bv" : "$int"); +} + +z3::func_decl Z3Encoder::specFuncDecl(const VFunction *Spec) { + assert(Spec && "specFuncDecl requires a spec function"); + std::string Key = specDeclKey(Spec->Name, CallerIntMode); + auto It = SpecFuncDecls.find(Key); + if (It != SpecFuncDecls.end()) + return It->second; + std::vector Domain; + for (const auto &P : Spec->Params) + Domain.push_back(valueSort(P.second, CallerIntMode)); + z3::sort Ret = valueSort(Spec->ReturnType, CallerIntMode); + z3::func_decl F = + Ctx.function(specZ3Name(Spec->Name, CallerIntMode).c_str(), Domain.size(), + Domain.data(), Ret); + SpecFuncDecls.emplace(Key, F); + return F; +} + +z3::expr Z3Encoder::encodeVExprForAxiom(const VExpr *E, const VType &RetTy) { + VCMachine M = VCMachine::fromVExpr(E, "", std::string(VHeapName) + "_0", + CallerIntMode); + if (!M.Goal) + return RetTy.Kind == VTypeKind::Bool + ? Ctx.bool_val(true) + : (CallerIntMode == VIntMode::Machine ? Ctx.bv_val(0, 32) + : Ctx.int_val(0)); + return encodeVC(M.Goal.get()); +} + +z3::expr Z3Encoder::coerceTo(z3::expr E, VIntMode Target) { + if (E.is_int() && Target == VIntMode::Math) + return E; + if (E.is_bv() && Target == VIntMode::Machine) + return E; + if (E.is_int() && Target == VIntMode::Machine) + return z3::int2bv(32, E); + if (E.is_bv() && Target == VIntMode::Math) + return z3::bv2int(E, true); + return E; +} + z3::expr Z3Encoder::heapVar(const std::string &Name) { auto It = Vars.find(Name); if (It != Vars.end()) @@ -20,214 +79,309 @@ z3::expr Z3Encoder::heapVar(const std::string &Name) { return H; } -static int64_t evalIntLiteral(const VExpr *E) { - if (!E || E->K != VExpr::Literal) - return 0; - return static_cast(E)->Value; +static z3::expr asBool(z3::context &Ctx, z3::expr E) { + if (E.is_bool()) + return E; + if (E.get_sort().is_array()) + return Ctx.bool_val(true); + if (E.is_int()) + return E != 0; + if (E.is_bv()) + return E != 0; + return Ctx.bool_val(true); } -z3::expr Z3Encoder::expandQuantifier(const VQuantifiedExpr *Q, bool IsForall) { - int64_t Lo = evalIntLiteral(Q->Lo.get()); - int64_t Hi = evalIntLiteral(Q->Hi.get()); - if (Hi <= Lo) - return Ctx.bool_val(IsForall); - z3::expr Acc = Ctx.bool_val(IsForall); - for (int64_t I = Lo; I < Hi; ++I) { - Vars.emplace(Q->Binder, Ctx.int_val(static_cast(I))); - z3::expr Body = encodeExpr(Q->Body.get(), std::string(VHeapName) + "_0"); - Acc = IsForall ? (Acc && Body) : (Acc || Body); - Vars.erase(Q->Binder); - } - return Acc; +/// Heap model is Array Int Int; pointer/index args may be bit-vectors. +static z3::expr heapIndex(z3::expr Ptr) { + if (Ptr.is_bv()) + return z3::bv2int(Ptr, true); + return Ptr; } -z3::expr Z3Encoder::encodeHeapStore(const VHeapStoreExpr *H) { - z3::expr Before = heapVar(H->HeapBefore); - z3::expr After = heapVar(H->HeapAfter); - z3::expr Ptr = encodeExpr(H->Ptr.get(), H->HeapBefore); - z3::expr Val = encodeExpr(H->Val.get(), H->HeapBefore); - return After == z3::store(Before, Ptr, Val); +static z3::expr heapCellValue(z3::expr Val) { + if (Val.is_int()) + return Val; + if (Val.is_bv()) + return z3::bv2int(Val, true); + return Val; } -z3::expr Z3Encoder::encodeExpr(const VExpr *E, const std::string &CurHeap) { - if (!E) +static z3::expr arithOp(z3::context &Ctx, VCExpr::Kind K, z3::expr L, z3::expr R) { + if (L.get_sort().is_array() || R.get_sort().is_array()) return Ctx.bool_val(true); + if (L.is_bv() && R.is_int()) + R = z3::int2bv(32, R); + if (L.is_int() && R.is_bv()) + L = z3::int2bv(32, L); + switch (K) { + case VCExpr::Add: + return L + R; + case VCExpr::Sub: + return L - R; + case VCExpr::Mul: + return L * R; + case VCExpr::Lt: + return L < R; + case VCExpr::Le: + return L <= R; + case VCExpr::Gt: + return L > R; + case VCExpr::Ge: + return L >= R; + case VCExpr::Eq: + return L == R; + case VCExpr::Ne: + return L != R; + default: + return L == R; + } +} + +z3::expr Z3Encoder::encodeVCNode( + const VCExpr *E, const std::map &Done) { + auto child = [&](unsigned I) -> z3::expr { + return Done.at(E->Children[I].get()); + }; switch (E->K) { - case VExpr::Literal: { - const auto *L = static_cast(E); - if (L->Ty.Kind == VTypeKind::Bool) - return Ctx.bool_val(L->Value != 0); - return Ctx.int_val(static_cast(L->Value)); - } - case VExpr::Var: { - const auto *V = static_cast(E); - auto It = Vars.find(V->Name); + case VCExpr::True: + return Ctx.bool_val(true); + case VCExpr::False: + return Ctx.bool_val(false); + case VCExpr::BoolLit: + return Ctx.bool_val(E->BoolVal); + case VCExpr::IntLit: { + if (E->IntMode == VIntMode::Machine) + return Ctx.bv_val(static_cast(E->IntVal), 32); + return Ctx.int_val(static_cast(E->IntVal)); + } + case VCExpr::Var: { + auto It = Vars.find(E->Name); if (It != Vars.end()) return It->second; - z3::expr Z = (V->Ty.Kind == VTypeKind::Bool) - ? Ctx.bool_const(V->Name.c_str()) - : Ctx.int_const(V->Name.c_str()); - Vars.emplace(V->Name, Z); + z3::expr Z = Ctx.int_const("_unused"); + if (E->Name.find("__heap") != std::string::npos || + E->Name.rfind(VHeapName, 0) == 0) { + Z = Ctx.constant(E->Name.c_str(), heapSort()); + } else if (E->IntMode == VIntMode::Machine) { + Z = Ctx.bv_const(E->Name.c_str(), 32); + } else { + Z = Ctx.int_const(E->Name.c_str()); + } + Vars.emplace(E->Name, Z); return Z; } - case VExpr::BinOp: { - const auto *B = static_cast(E); - z3::expr L = encodeExpr(B->Lhs.get(), CurHeap); - z3::expr R = encodeExpr(B->Rhs.get(), CurHeap); - switch (B->Op) { - case VBinOp::Add: - return L + R; - case VBinOp::Sub: - return L - R; - case VBinOp::Mul: - return L * R; - case VBinOp::Lt: - return L < R; - case VBinOp::Le: - return L <= R; - case VBinOp::Gt: - return L > R; - case VBinOp::Ge: - return L >= R; - case VBinOp::Eq: - return L == R; - case VBinOp::Ne: - return L != R; - case VBinOp::And: - return L && R; - case VBinOp::Or: - return L || R; - default: - return L == R; + case VCExpr::IntToBv: { + z3::expr Inner = child(0); + if (Inner.is_int()) + return z3::int2bv(32, Inner); + return Inner; + } + case VCExpr::BvToInt: { + z3::expr Inner = child(0); + if (Inner.is_bv()) + return z3::bv2int(Inner, true); + return Inner; + } + case VCExpr::Not: + return !asBool(Ctx, child(0)); + case VCExpr::And: { + z3::expr_vector Ch(Ctx); + for (const auto &C : E->Children) { + if (!C) + continue; + z3::expr Elt = Done.at(C.get()); + if (Elt.is_bool()) + Ch.push_back(Elt); + else if (!Elt.get_sort().is_array()) + Ch.push_back(asBool(Ctx, Elt)); } + if (Ch.empty()) + return Ctx.bool_val(true); + if (Ch.size() == 1) + return Ch[0]; + return z3::mk_and(Ch); + } + case VCExpr::Or: { + z3::expr_vector Ch(Ctx); + for (const auto &C : E->Children) { + if (!C) + continue; + z3::expr Elt = Done.at(C.get()); + if (Elt.is_bool()) + Ch.push_back(Elt); + else if (!Elt.get_sort().is_array()) + Ch.push_back(asBool(Ctx, Elt)); + } + if (Ch.empty()) + return Ctx.bool_val(false); + if (Ch.size() == 1) + return Ch[0]; + return z3::mk_or(Ch); + } + case VCExpr::Ite: { + z3::expr C = asBool(Ctx, child(0)); + z3::expr T = coerceTo(child(1), E->IntMode); + z3::expr F = coerceTo(child(2), E->IntMode); + return z3::ite(C, T, F); + } + case VCExpr::Eq: + case VCExpr::Ne: + case VCExpr::Lt: + case VCExpr::Le: + case VCExpr::Gt: + case VCExpr::Ge: + case VCExpr::Add: + case VCExpr::Sub: + case VCExpr::Mul: { + z3::expr L = coerceTo(child(0), E->IntMode); + z3::expr R = coerceTo(child(1), E->IntMode); + return arithOp(Ctx, E->K, L, R); + } + case VCExpr::Neg: + return -coerceTo(child(0), E->IntMode); + case VCExpr::Select: { + z3::expr Val = z3::select(child(0), heapIndex(child(1))); + return coerceTo(Val, E->IntMode); + } + case VCExpr::Store: { + z3::expr Before = child(0); + z3::expr Ptr = heapIndex(child(1)); + z3::expr Val = heapCellValue(child(2)); + z3::expr After = child(3); + return (After == z3::store(Before, Ptr, Val)); + } + case VCExpr::Forall: + return Ctx.bool_val(true); + case VCExpr::SpecCall: { + auto It = SpecFunctions.find(E->SpecCallee); + if (It == SpecFunctions.end() || !It->second) + return Ctx.int_val(0); + z3::func_decl F = specFuncDecl(It->second); + std::vector Args; + for (unsigned i = 0; i < E->Children.size(); ++i) + Args.push_back(coerceTo(child(i), CallerIntMode)); + z3::expr A = F(static_cast(Args.size()), Args.data()); + return coerceTo(A, CallerIntMode); } - case VExpr::UnaryOp: { - const auto *U = static_cast(E); - z3::expr O = encodeExpr(U->Operand.get(), CurHeap); - if (U->Op == VUnaryOp::Neg) - return -O; - return !O; - } - case VExpr::Conditional: { - const auto *C = static_cast(E); - return z3::ite(encodeExpr(C->Cond.get(), CurHeap), - encodeExpr(C->Then.get(), CurHeap), - encodeExpr(C->Else.get(), CurHeap)); - } - case VExpr::Result: { - const char *Name = ResultVarName.empty() ? "__result_0" : ResultVarName.c_str(); - auto It = Vars.find(Name); - if (It != Vars.end()) - return It->second; - z3::expr R = Ctx.int_const(Name); - Vars.emplace(std::string(Name), R); - return R; - } - case VExpr::Old: - return encodeExpr(static_cast(E)->Inner.get(), CurHeap); - case VExpr::Cast: - return encodeExpr(static_cast(E)->Inner.get(), CurHeap); - case VExpr::Load: { - const auto *L = static_cast(E); - std::string Heap = L->HeapVar.empty() ? CurHeap : L->HeapVar; - z3::expr H = heapVar(Heap); - z3::expr Ptr = encodeExpr(L->Ptr.get(), Heap); - return z3::select(H, Ptr); - } - case VExpr::Forall: - return expandQuantifier(static_cast(E), true); - case VExpr::Exists: - return expandQuantifier(static_cast(E), false); - case VExpr::HeapStore: - return encodeHeapStore(static_cast(E)); } return Ctx.bool_val(true); } -Z3CheckResult Z3Encoder::verifyPassive(const PassiveProgram &P) { - Vars.clear(); - Solver = z3::solver(Ctx); - Z3CheckResult Out; - ResultVarName = P.ResultVarName; - - std::string CurHeap = P.OldHeapName.empty() ? std::string(VHeapName) + "_0" : P.OldHeapName; - z3::expr Hyp = Ctx.bool_val(true); - z3::expr Post = Ctx.bool_val(true); - - for (const auto &A : P.EntryAssumes) - Hyp = Hyp && encodeExpr(A.get(), CurHeap); - - for (const auto &S : P.Stmts) { - if (S->K == PassiveStmt::Assume && S->Cond) { - if (S->Cond->K == VExpr::HeapStore) { - auto *H = static_cast(S->Cond.get()); - Hyp = Hyp && encodeHeapStore(H); - CurHeap = H->HeapAfter; - } else { - Hyp = Hyp && encodeExpr(S->Cond.get(), CurHeap); +z3::expr Z3Encoder::encodeVC(const VCExpr *Root) { + if (!Root) + return Ctx.bool_val(true); + std::map Done; + std::vector Stack = {Root}; + while (!Stack.empty()) { + const VCExpr *E = Stack.back(); + if (Done.count(E)) { + Stack.pop_back(); + continue; + } + bool Pending = false; + for (const auto &C : E->Children) { + if (C && !Done.count(C.get())) { + Stack.push_back(C.get()); + Pending = true; + break; } - } else if (S->K == PassiveStmt::Assert && S->Cond) { - Post = Post && encodeExpr(S->Cond.get(), CurHeap); } + if (Pending) + continue; + Stack.pop_back(); + z3::expr Enc = encodeVCNode(E, Done); + Done.insert({E, std::move(Enc)}); } + return Done.at(Root); +} - for (const auto &A : P.ExitAsserts) - Post = Post && encodeExpr(A.get(), CurHeap); +void Z3Encoder::emitSpecDefiningAxiom(const std::string &Name, + const SpecAxiomContext &ACtx) { + auto It = ACtx.Functions.find(Name); + if (It == ACtx.Functions.end() || !It->second) + return; + const VFunction &Spec = *It->second; + unsigned Fuel = 0; + if (ACtx.HiddenSpecs.count(Spec.Name)) + Fuel = 0; + else if (auto F = ACtx.SpecFuel.find(Spec.Name); F != ACtx.SpecFuel.end()) + Fuel = F->second; + else if (ACtx.RevealedSpecs.count(Spec.Name)) + Fuel = 1; + else if (!Spec.NeedsDecreasesCheck) + Fuel = 64; + std::unique_ptr Body = unfoldSpecDefinition(Spec, ACtx, Fuel); + if (!Body) + return; + z3::func_decl Fdecl = specFuncDecl(&Spec); + z3::expr_vector ParamVars(Ctx); + std::vector AppArgs; + for (const auto &P : Spec.Params) { + z3::expr V = CallerIntMode == VIntMode::Machine + ? Ctx.bv_const(P.first.c_str(), 32) + : Ctx.int_const(P.first.c_str()); + Vars.emplace(P.first, V); + ParamVars.push_back(V); + AppArgs.push_back(V); + } + z3::expr LHS = Fdecl(static_cast(AppArgs.size()), AppArgs.data()); + z3::expr RHS = encodeVExprForAxiom(Body.get(), Spec.ReturnType); + z3::expr Eq = (LHS == RHS); + Solver.add(z3::forall(ParamVars, Eq)); + for (const auto &P : Spec.Params) + Vars.erase(P.first); +} - Solver.add(Hyp && !Post); +VerifyResult Z3Encoder::verifyMachine(const VCMachine &M) { + Vars.clear(); + Solver = z3::solver(Ctx); + SpecFunctions = M.SpecFunctions; + CallerIntMode = M.CallerIntMode; + VerifyResult Out; + if (!M.Goal) { + Out.Status = VerifyStatus::Verified; + return Out; + } + SpecAxiomContext AxiomCtx{M.SpecFunctions, M.SpecFuel, M.HiddenSpecs, + M.RevealedSpecs, M.CallerIntMode}; + emitSpecAxioms(*this, M.Goal.get(), AxiomCtx); + Vars.clear(); + Solver.add(encodeVC(M.Goal.get())); switch (Solver.check()) { case z3::unsat: - Out.S = Z3CheckResult::Verified; + Out.Status = VerifyStatus::Verified; return Out; case z3::sat: { - Out.S = Z3CheckResult::Failed; - z3::model M = Solver.get_model(); - std::string Msg; - for (auto &KV : Vars) { - z3::expr Val = M.eval(KV.second, true); - if (!Msg.empty()) - Msg += ", "; - Msg += KV.first + " = " + Val.to_string(); + Out.Status = VerifyStatus::Failed; + z3::model Mod = Solver.get_model(); + for (const auto &KV : Vars) { + z3::expr Val = Mod.eval(KV.second, true); + Out.Model[KV.first] = Val.to_string(); } - Out.Counterexample = Msg; return Out; } default: - Out.S = Z3CheckResult::Unknown; + Out.Status = VerifyStatus::Unknown; return Out; } } -void Z3Encoder::dumpVC(const VExpr *VC, llvm::raw_ostream &OS) { +void Z3Encoder::dumpVC(const VCExpr *E, llvm::raw_ostream &OS) { Z3Encoder Tmp; - OS << Tmp.encodeExpr(VC, std::string(VHeapName) + "_0").to_string() << "\n"; + OS << Tmp.encodeVC(E).to_string() << "\n"; } -Z3CheckResult Z3Encoder::checkVC(const VExpr *VC) { - Vars.clear(); - Solver = z3::solver(Ctx); - Z3CheckResult Out; - z3::expr F = encodeExpr(VC, std::string(VHeapName) + "_0"); - Solver.add(F); - switch (Solver.check()) { - case z3::unsat: - Out.S = Z3CheckResult::Verified; - return Out; - case z3::sat: { - Out.S = Z3CheckResult::Failed; - z3::model M = Solver.get_model(); +VerifyResult Z3VerifyBackend::verifyPassive(const PassiveProgram &P) { + VCMachine M = VCMachine::fromPassive(P); + VerifyResult R = Enc.verifyMachine(M); + if (R.Status == VerifyStatus::Failed) { std::string Msg; - for (auto &KV : Vars) { - z3::expr Val = M.eval(KV.second, true); + for (const auto &KV : R.Model) { if (!Msg.empty()) Msg += ", "; - Msg += KV.first + " = " + Val.to_string(); + Msg += KV.first + " = " + KV.second; } - Out.Counterexample = Msg; - return Out; - } - default: - Out.S = Z3CheckResult::Unknown; - return Out; + R.Message = Msg; } + return R; } \ No newline at end of file diff --git a/clang/lib/Verify/Backend/Z3Encode.h b/clang/lib/Verify/Backend/Z3Encode.h index 8087cb4498..7c1a21d7e1 100644 --- a/clang/lib/Verify/Backend/Z3Encode.h +++ b/clang/lib/Verify/Backend/Z3Encode.h @@ -1,41 +1,53 @@ -//===--- Z3Encode.h - VExpr to Z3 ---------------------------------*- C++ -*-===// +//===--- Z3Encode.h - VCMachine to Z3 -----------------------------------===// #ifndef LLVM_CLANG_VERIFY_BACKEND_Z3ENCODE_H #define LLVM_CLANG_VERIFY_BACKEND_Z3ENCODE_H -#include "../IR/VExpr.h" -#include "../Transform/Passivize.h" +#include "SpecAxioms.h" +#include "VCMachine.h" +#include "VerifyBackend.h" +#include "../IR/VType.h" #include +#include #include #include namespace clang { namespace verify { -struct Z3CheckResult { - enum Status { Verified, Failed, Unknown }; - Status S = Unknown; - std::string Counterexample; -}; - class Z3Encoder { z3::context Ctx; z3::solver Solver; std::map Vars; + FunctionMap SpecFunctions; + std::map SpecFuncDecls; + VIntMode CallerIntMode = VIntMode::Machine; z3::sort intSort(); + z3::sort bvSort(); z3::sort boolSort(); z3::sort heapSort(); + z3::sort valueSort(const VType &Ty, VIntMode Mode); z3::expr heapVar(const std::string &Name); - z3::expr encodeExpr(const VExpr *E, const std::string &CurHeap); - z3::expr encodeHeapStore(const VHeapStoreExpr *H); - z3::expr expandQuantifier(const VQuantifiedExpr *Q, bool IsForall); - std::string ResultVarName; + z3::expr coerceTo(z3::expr E, VIntMode Target); + z3::func_decl specFuncDecl(const VFunction *Spec); + z3::expr encodeVCNode(const VCExpr *E, + const std::map &Done); + z3::expr encodeVC(const VCExpr *E); + z3::expr encodeVExprForAxiom(const VExpr *E, const VType &RetTy); public: Z3Encoder(); - Z3CheckResult verifyPassive(const PassiveProgram &P); - Z3CheckResult checkVC(const VExpr *VC); - void dumpVC(const VExpr *VC, llvm::raw_ostream &OS); + VerifyResult verifyMachine(const VCMachine &M); + void emitSpecDefiningAxiom(const std::string &Name, const SpecAxiomContext &Ctx); + void dumpVC(const VCExpr *E, llvm::raw_ostream &OS); +}; + +class Z3VerifyBackend : public VerifyBackend { + Z3Encoder Enc; + +public: + llvm::StringRef getName() const override { return "z3"; } + VerifyResult verifyPassive(const PassiveProgram &P) override; }; } // namespace verify diff --git a/clang/lib/Verify/CMakeLists.txt b/clang/lib/Verify/CMakeLists.txt index cdf3a3a29b..fb74f2f8c3 100644 --- a/clang/lib/Verify/CMakeLists.txt +++ b/clang/lib/Verify/CMakeLists.txt @@ -12,13 +12,24 @@ if(NOT CPPVERIFY_Z3_TARGET) endif() message(STATUS "cpp-verify: Z3 backend = ${CPPVERIFY_Z3_TARGET}") +option(CPPVERIFY_ENABLE_COVERAGE "Instrument clangVerify for LLVM coverage" OFF) +if(CPPVERIFY_ENABLE_COVERAGE) + message(STATUS "cpp-verify: coverage instrumentation enabled") +endif() + add_clang_library(clangVerify IR/VExpr.cpp IR/VStmt.cpp Frontend/ASTConverter.cpp Transform/Passivize.cpp + Transform/LoopUnroll.cpp + Transform/SpecInline.cpp + Backend/VCMachine.cpp Backend/WPCalc.cpp Backend/Z3Encode.cpp + Backend/SpecAxioms.cpp + Backend/VerifyBackend.cpp + Backend/LeanBackend.cpp Driver/Verifier.cpp Driver/DumpIR.cpp Driver/CppVerifyIntegration.cpp @@ -35,6 +46,14 @@ add_clang_library(clangVerify ) target_link_libraries(clangVerify PRIVATE ${CPPVERIFY_Z3_TARGET}) +if(CPPVERIFY_ENABLE_COVERAGE) + target_compile_options(clangVerify PRIVATE + -fprofile-instr-generate -fcoverage-mapping) + if(TARGET obj.clangVerify) + target_compile_options(obj.clangVerify PRIVATE + -fprofile-instr-generate -fcoverage-mapping) + endif() +endif() target_include_directories(clangVerify PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/Driver diff --git a/clang/lib/Verify/Driver/DumpIR.cpp b/clang/lib/Verify/Driver/DumpIR.cpp index ab3b1106e4..46909b333a 100644 --- a/clang/lib/Verify/Driver/DumpIR.cpp +++ b/clang/lib/Verify/Driver/DumpIR.cpp @@ -138,6 +138,19 @@ void verify::dumpVExpr(const VExpr *E, llvm::raw_ostream &OS, unsigned Depth) { case VExpr::HeapStore: OS << "heap_store\n"; break; + case VExpr::FieldAccess: { + const auto *F = static_cast(E); + OS << "field " << F->Field << "\n"; + dumpVExpr(F->Base.get(), OS, Depth + 1); + break; + } + case VExpr::SpecCall: { + const auto *C = static_cast(E); + OS << "spec_call " << C->Callee << "\n"; + for (const auto &A : C->Args) + dumpVExpr(A.get(), OS, Depth + 1); + break; + } } } @@ -169,6 +182,26 @@ static void dumpVStmt(const VStmt &S, llvm::raw_ostream &OS, unsigned Depth) { dumpVExpr(R.Value.get(), OS, Depth + 1); break; } + case VStmt::While: { + const auto &W = static_cast(S); + OS << "while\n"; + dumpVExpr(W.Cond.get(), OS, Depth + 1); + for (const auto &Inv : W.Invariants) + dumpVExpr(Inv.get(), OS, Depth + 1); + if (W.Decreases) + dumpVExpr(W.Decreases.get(), OS, Depth + 1); + for (const auto &B : W.Body) + dumpVStmt(*B, OS, Depth + 1); + break; + } + case VStmt::Call: { + const auto &C = static_cast(S); + OS << "call " << C.Callee; + if (!C.ResultTarget.empty()) + OS << " -> " << C.ResultTarget; + OS << "\n"; + break; + } case VStmt::Assert: OS << "assert\n"; dumpVExpr(static_cast(S).Cond.get(), OS, Depth + 1); @@ -184,6 +217,27 @@ static void dumpVStmt(const VStmt &S, llvm::raw_ostream &OS, unsigned Depth) { for (const auto &C : static_cast(S).Stmts) dumpVStmt(*C, OS, Depth); break; + case VStmt::GhostBlock: { + OS << "ghost\n"; + for (const auto &B : static_cast(S).Body) + dumpVStmt(*B, OS, Depth + 1); + break; + } + case VStmt::ContractAssert: + OS << "contract_assert\n"; + dumpVExpr(static_cast(S).Cond.get(), OS, Depth + 1); + break; + case VStmt::RevealWithFuel: + OS << "reveal_with_fuel\n"; + break; + case VStmt::HideSpec: + OS << "hide_spec\n"; + break; + case VStmt::RevealSpec: + OS << "reveal_spec\n"; + break; + default: + break; } } @@ -229,6 +283,8 @@ void verify::dumpVC(llvm::StringRef FnName, const VExpr *VC, } void verify::dumpZ3(const VExpr *VC, llvm::raw_ostream &OS) { + VCMachine M = VCMachine::fromVExpr(VC, "__result_0", std::string(VHeapName) + "_0"); Z3Encoder Enc; - Enc.dumpVC(VC, OS); + if (M.Goal) + Enc.dumpVC(M.Goal.get(), OS); } \ No newline at end of file diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 2a3332e549..139134bd5c 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -1,24 +1,30 @@ //===--- Verifier.cpp - CppVerify driver ----------------------------------===// #include "clang/AST/ASTContext.h" -#include "clang/Basic/Diagnostic.h" -#include "clang/Basic/SourceManager.h" #include "../Frontend/ASTConverter.h" #include "../Transform/Passivize.h" +#include "../Transform/LoopUnroll.h" +#include "../Transform/SpecInline.h" +#include "../IR/VStmt.h" #include "../Backend/WPCalc.h" +#include "../Backend/VCMachine.h" #include "../Backend/Z3Encode.h" +#include "../Backend/LeanBackend.h" #include "Verifier.h" #include "DumpIR.h" +#include "llvm/Support/FileSystem.h" +#include #include "llvm/Support/MathExtras.h" #include "llvm/Support/raw_ostream.h" -namespace clang { -namespace verify { +using namespace clang; +using namespace verify; + +namespace { struct VerifyDiagnostic { enum Kind { Verified, Error, Warning, Unknown }; Kind K; std::string Message; - SourceLocation Loc; }; class Verifier { @@ -28,7 +34,7 @@ class Verifier { std::vector Diags; void checkRecommendsImplied(const std::vector> &Fns, - Z3Encoder &Z3) { + VerifyBackend &Backend) { for (const auto &Fn : Fns) { if (Fn->Recommends.empty()) continue; @@ -39,11 +45,43 @@ class Verifier { PP.ExitAsserts.push_back(cloneVExpr(Rec.get())); if (PP.ExitAsserts.empty()) continue; - Z3CheckResult R = Z3.verifyPassive(PP); - if (R.S == Z3CheckResult::Failed) + VerifyResult R = Backend.verifyPassive(PP); + if (R.Status == VerifyStatus::Failed) + Diags.push_back({VerifyDiagnostic::Warning, + "recommends not implied by preconditions in " + Fn->Name}); + } + } + + void checkCalleeRecommendsOnFailure(const VFunction &Caller, + const FunctionMap &FnMap, + VerifyBackend &Backend) { + std::vector Calls; + collectSpecCallsInFunction(Caller, Calls); + for (const VSpecCallExpr *C : Calls) { + auto It = FnMap.find(C->Callee); + if (It == FnMap.end() || It->second->Recommends.empty()) + continue; + std::map> ArgMap; + for (unsigned I = 0; I < It->second->Params.size() && I < C->Args.size(); ++I) + ArgMap[It->second->Params[I].first] = cloneVExpr(C->Args[I].get()); + PassiveProgram PP; + for (const auto &Pre : Caller.Preconditions) + PP.EntryAssumes.push_back(cloneVExpr(Pre.get())); + for (const auto &Rec : It->second->Recommends) { + auto Inst = substParamsInExpr(Rec.get(), ArgMap); + if (!Inst) + continue; + auto NotRec = std::make_unique(VUnaryOp::Not, std::move(Inst), + VType::makeBool(), C->Loc); + PP.ExitAsserts.push_back(std::move(NotRec)); + } + if (PP.ExitAsserts.empty()) + continue; + VerifyResult R = Backend.verifyPassive(PP); + if (R.Status == VerifyStatus::Failed) Diags.push_back({VerifyDiagnostic::Warning, - "recommends not implied by preconditions in " + Fn->Name, - SourceLocation()}); + "recommends of spec " + C->Callee + + " may be violated at call in " + Caller.Name}); } } @@ -54,15 +92,38 @@ class Verifier { bool run() { ASTConverter Converter(Ctx); auto Functions = Converter.convertTranslationUnit(); + for (const std::string &Err : Converter.getErrors()) + Diags.push_back({VerifyDiagnostic::Error, Err}); + if (!Converter.getErrors().empty()) + return false; if (Functions.empty()) { - Diags.push_back({VerifyDiagnostic::Warning, "no verifiable functions found", - SourceLocation()}); + Diags.push_back({VerifyDiagnostic::Warning, "no verifiable functions found"}); return true; } + FunctionMap FnMap; + for (const auto &Fn : Functions) + FnMap[Fn->Name] = Fn.get(); + + std::unique_ptr LeanFile; + llvm::raw_ostream *LeanOut = DumpOS; + if (Opts.Backend == BackendKind::Lean && !Opts.LeanOutPath.empty()) { + std::error_code EC; + LeanFile = std::make_unique( + Opts.LeanOutPath, EC, llvm::sys::fs::OF_Text); + if (EC) { + Diags.push_back({VerifyDiagnostic::Error, + "cannot open lean output: " + Opts.LeanOutPath}); + return false; + } + LeanOut = LeanFile.get(); + } + + auto Backend = createVerifyBackend(Opts.Backend, LeanOut, Opts.BMCUnroll); Passivizer P; + P.setFunctionMap(FnMap); WPCalculator WP; - Z3Encoder Z3; + Z3Encoder Z3Dump; const unsigned DumpLayers = Opts.DumpIRLayers; const bool MultiLayerDump = llvm::popcount(DumpLayers) > 1; @@ -77,12 +138,78 @@ class Verifier { DumpedAny = true; }; + std::optional PreparedFn; + std::optional UnrolledFn; + const VFunction &WorkFn = [&]() -> const VFunction & { + if (Fn->IsSpec) { + if (Fn->NeedsDecreasesCheck) + return *Fn; + return *Fn; + } + PreparedFn = cloneVFunction(*Fn); + SpecInliner Inliner(FnMap, PreparedFn->SpecFuel); + if (Opts.Backend == BackendKind::Z3) + Inliner.prepareFunctionAxiomatic(*PreparedFn); + else + Inliner.prepareFunction(*PreparedFn); + if (Opts.Backend == BackendKind::BMC) { + UnrolledFn = LoopUnroller::unroll(*PreparedFn, Opts.BMCUnroll); + return *UnrolledFn; + } + return *PreparedFn; + }(); + + if (Fn->IsSpec && !Fn->NeedsDecreasesCheck) { + if (Fn->IsConstexprSpec) + Diags.push_back( + {VerifyDiagnostic::Verified, "constexpr spec axiom: " + Fn->Name}); + else + Diags.push_back({VerifyDiagnostic::Verified, "spec axiom: " + Fn->Name}); + continue; + } + + if ((Fn->IsSpec || Fn->IsProof) && Fn->NeedsDecreasesCheck) { + PassiveProgram DecPP = buildDecreasesChecks(*Fn, FnMap); + if (!Fn->IsSpec && Opts.Backend != BackendKind::Lean) { + VerifyResult DR = Backend->verifyPassive(DecPP); + if (DR.Status == VerifyStatus::Failed) { + AllOk = false; + AnyFailed = true; + Diags.push_back({VerifyDiagnostic::Error, + "decreases failed: " + Fn->Name}); + continue; + } + } else if (Fn->IsSpec) { + if (Opts.Backend == BackendKind::Lean) { + Diags.push_back({VerifyDiagnostic::Verified, + "spec decreases: " + Fn->Name}); + continue; + } + VerifyResult R = Backend->verifyPassive(DecPP); + if (R.Status == VerifyStatus::Verified) + Diags.push_back({VerifyDiagnostic::Verified, + "spec decreases: " + Fn->Name}); + else if (R.Status == VerifyStatus::Failed) { + AllOk = false; + AnyFailed = true; + Diags.push_back({VerifyDiagnostic::Error, + "spec decreases failed: " + Fn->Name}); + } else { + AllOk = false; + AnyFailed = true; + Diags.push_back({VerifyDiagnostic::Error, + "spec decreases unknown: " + Fn->Name}); + } + continue; + } + } + if (DumpLayers & LayerVCR) { dumpSep(); - dumpVFunction(*Fn, *DumpOS); + dumpVFunction(WorkFn, *DumpOS); } - PassiveProgram PP = P.run(*Fn); + PassiveProgram PP = P.run(WorkFn); if (DumpLayers & LayerPassive) { dumpSep(); dumpPassiveProgram(Fn->Name, PP, *DumpOS); @@ -96,30 +223,51 @@ class Verifier { if (DumpLayers & LayerZ3 && VC) { dumpSep(); - dumpZ3(VC.get(), *DumpOS); + VCMachine M = VCMachine::fromPassive(PP); + if (M.Goal) + Z3Dump.dumpVC(M.Goal.get(), *DumpOS); } - Z3CheckResult R = Z3.verifyPassive(PP); - if (R.S == Z3CheckResult::Verified) { + if (Opts.Backend == BackendKind::Lean) { + if (LeanOut != DumpOS) { + *LeanOut << "\n/- function: " << Fn->Name << " -/\n"; + exportLeanScratchPad(PP, *LeanOut); + } else { + exportLeanScratchPad(PP, *DumpOS); + } Diags.push_back({VerifyDiagnostic::Verified, - "verified: " + Fn->Name, SourceLocation()}); - } else if (R.S == Z3CheckResult::Failed) { + "lean export: " + Fn->Name}); + continue; + } + + VerifyResult R = Backend->verifyPassive(PP); + if (R.Status == VerifyStatus::Verified) { + Diags.push_back({VerifyDiagnostic::Verified, Fn->Name}); + } else if (R.Status == VerifyStatus::Failed) { AllOk = false; AnyFailed = true; std::string Msg = "verification failed: " + Fn->Name; - if (!R.Counterexample.empty()) - Msg += " (counterexample: " + R.Counterexample + ")"; - Diags.push_back({VerifyDiagnostic::Error, Msg, SourceLocation()}); + if (!R.Message.empty()) + Msg += " (counterexample: " + R.Message + ")"; + Diags.push_back({VerifyDiagnostic::Error, Msg}); } else { AllOk = false; AnyFailed = true; - Diags.push_back({VerifyDiagnostic::Unknown, - "unknown: " + Fn->Name, SourceLocation()}); + Diags.push_back({VerifyDiagnostic::Unknown, "unknown: " + Fn->Name}); } } - if (AnyFailed) - checkRecommendsImplied(Functions, Z3); + if (AnyFailed && Opts.Backend == BackendKind::Z3) { + auto Z3 = createVerifyBackend(BackendKind::Z3, nullptr, 0); + checkRecommendsImplied(Functions, *Z3); + for (const auto &Fn : Functions) { + if (Fn->IsSpec || Fn->IsProof) + continue; + VFunction Prepared = cloneVFunction(*Fn); + SpecInliner(FnMap, Prepared.SpecFuel).prepareFunctionAxiomatic(Prepared); + checkCalleeRecommendsOnFailure(Prepared, FnMap, *Z3); + } + } return AllOk; } @@ -144,13 +292,12 @@ class Verifier { } }; -bool verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS, - const VerifyOptions &Opts) { +} // namespace + +bool verify::verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS, + const VerifyOptions &Opts) { Verifier V(Ctx, Opts, OS); bool Ok = V.run(); V.printDiagnostics(OS); return Ok; -} - -} // namespace verify -} // namespace clang \ No newline at end of file +} \ No newline at end of file diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h index 64876ffffd..551fa4df6b 100644 --- a/clang/lib/Verify/Driver/Verifier.h +++ b/clang/lib/Verify/Driver/Verifier.h @@ -2,15 +2,19 @@ #ifndef LLVM_CLANG_VERIFY_DRIVER_VERIFIER_H #define LLVM_CLANG_VERIFY_DRIVER_VERIFIER_H +#include "../Backend/VerifyBackend.h" #include "llvm/Support/raw_ostream.h" +#include namespace clang { class ASTContext; namespace verify { struct VerifyOptions { - /// Bitmask of IRLayer values; 0 disables IR dumps. unsigned DumpIRLayers = 0; + BackendKind Backend = BackendKind::Z3; + std::string LeanOutPath; + unsigned BMCUnroll = 10; }; bool verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS, diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index a0b2d54499..e2934b4b0e 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -8,10 +8,86 @@ #include "clang/AST/ExprContract.h" #include "clang/AST/Stmt.h" #include "clang/AST/StmtCXX.h" +#include "clang/AST/StmtContract.h" +#include "llvm/ADT/StringSet.h" +#include using namespace clang; using namespace verify; +bool ASTConverter::calleeIsSpec(const FunctionDecl *FD) const { + if (!FD) + return false; + if (const FunctionContractInfo *FCI = Ctx.getFunctionContract(FD)) { + if (FCI->IsSpec) + return true; + } + return FD->isConstexpr() && FD->hasBody(); +} + +VIntMode ASTConverter::specCallIntMode(const FunctionDecl *FD) const { + if (!FD) + return VIntMode::Machine; + if (const FunctionContractInfo *FCI = Ctx.getFunctionContract(FD)) { + if (FCI->IsSpec) + return VIntMode::Math; + } + if (FD->isConstexpr()) + return VIntMode::Machine; + return VIntMode::Math; +} + +bool ASTConverter::contractsReferenceSpec(const FunctionContractInfo &FCI) const { + std::function check = [&](const Expr *E) -> bool { + if (!E) + return false; + E = E->IgnoreParenImpCasts(); + if (const auto *CE = dyn_cast(E)) { + if (const FunctionDecl *Callee = CE->getDirectCallee()) + return calleeIsSpec(Callee); + } + if (const auto *B = dyn_cast(E)) { + return check(B->getLHS()) || check(B->getRHS()); + } + if (const auto *U = dyn_cast(E)) + return check(U->getSubExpr()); + if (const auto *O = dyn_cast(E)) + return check(O->getInner()); + if (const auto *C = dyn_cast(E)) { + return check(C->getCond()) || check(C->getTrueExpr()) || + check(C->getFalseExpr()); + } + return false; + }; + for (const Expr *E : FCI.Preconditions) + if (check(E)) + return true; + for (const Expr *E : FCI.Postconditions) + if (check(E)) + return true; + for (const Expr *E : FCI.Recommends) + if (check(E)) + return true; + return false; +} + +std::string ASTConverter::specNameFromExpr(const Expr *E) { + if (!E) + return {}; + if (const auto *DRE = dyn_cast(E->IgnoreParenImpCasts())) + if (const auto *FD = dyn_cast(DRE->getDecl())) + return FD->getNameAsString(); + return {}; +} + +bool ASTConverter::calleeIsProof(const FunctionDecl *FD) const { + if (!FD) + return false; + if (const FunctionContractInfo *FCI = Ctx.getFunctionContract(FD)) + return FCI->IsProof; + return false; +} + static bool isMutablePointerParam(const ParmVarDecl *P) { QualType T = P->getType(); if (!T->isPointerType() && !T->isReferenceType()) @@ -38,9 +114,78 @@ static bool aliasesListed(const FunctionContractInfo &FCI, const ParmVarDecl *A, return false; } +static bool exprReferencesSpecCall(const VExpr *E, const std::string &Name) { + if (!E) + return false; + if (E->K == VExpr::SpecCall && + static_cast(E)->Callee == Name) + return true; + if (E->K == VExpr::BinOp) { + const auto *B = static_cast(E); + return exprReferencesSpecCall(B->Lhs.get(), Name) || + exprReferencesSpecCall(B->Rhs.get(), Name); + } + if (E->K == VExpr::UnaryOp) + return exprReferencesSpecCall(static_cast(E)->Operand.get(), + Name); + if (E->K == VExpr::Conditional) { + const auto *C = static_cast(E); + return exprReferencesSpecCall(C->Cond.get(), Name) || + exprReferencesSpecCall(C->Then.get(), Name) || + exprReferencesSpecCall(C->Else.get(), Name); + } + return false; +} + +static bool vexprHasSpecCall(const VExpr *E) { + if (!E) + return false; + if (E->K == VExpr::SpecCall) + return true; + if (E->K == VExpr::BinOp) { + const auto *B = static_cast(E); + return vexprHasSpecCall(B->Lhs.get()) || vexprHasSpecCall(B->Rhs.get()); + } + if (E->K == VExpr::UnaryOp) + return vexprHasSpecCall(static_cast(E)->Operand.get()); + if (E->K == VExpr::Old) + return vexprHasSpecCall(static_cast(E)->Inner.get()); + if (E->K == VExpr::Conditional) { + const auto *C = static_cast(E); + return vexprHasSpecCall(C->Cond.get()) || vexprHasSpecCall(C->Then.get()) || + vexprHasSpecCall(C->Else.get()); + } + return false; +} + +static bool fnReferencesSpec(const VFunction &Fn) { + for (const auto &P : Fn.Preconditions) + if (vexprHasSpecCall(P.get())) + return true; + for (const auto &P : Fn.Postconditions) + if (vexprHasSpecCall(P.get())) + return true; + return false; +} + +static bool bodyHasRecursiveSpec(const VFunction &Fn) { + for (const auto &S : Fn.Body) { + if (S->K == VStmt::Assign && + exprReferencesSpecCall(static_cast(*S).Value.get(), + Fn.Name)) + return true; + if (S->K == VStmt::Return && + exprReferencesSpecCall(static_cast(*S).Value.get(), + Fn.Name)) + return true; + } + return false; +} + std::vector> ASTConverter::convertTranslationUnit() { std::vector> Out; + llvm::StringSet<> Names; for (const auto *D : Ctx.getTranslationUnitDecl()->decls()) { const auto *FD = dyn_cast(D); if (!FD || !FD->isThisDeclarationADefinition() || FD->isTemplated()) @@ -48,8 +193,36 @@ ASTConverter::convertTranslationUnit() { if (FD->isInStdNamespace()) continue; auto Fn = convertFunction(FD); - if (Fn) + if (Fn) { + Names.insert(Fn->Name); Out.push_back(std::move(Fn)); + } + } + for (const auto *D : Ctx.getTranslationUnitDecl()->decls()) { + const auto *FD = dyn_cast(D); + if (!FD || !FD->isThisDeclarationADefinition() || FD->isTemplated()) + continue; + if (FD->isInStdNamespace() || Names.contains(FD->getName())) + continue; + if (!FD->isConstexpr() || !FD->hasBody()) + continue; + if (Ctx.getFunctionContract(FD)) + continue; + auto Fn = convertConstexprSpec(FD); + if (Fn) { + Names.insert(Fn->Name); + Out.push_back(std::move(Fn)); + } + } + for (auto &Fn : Out) { + if (!Fn->IsSpec && !Fn->IsProof) + continue; + bool Recursive = bodyHasRecursiveSpec(*Fn); + for (const auto &S : Fn->Body) + if (S->K == VStmt::Call && + static_cast(*S).Callee == Fn->Name) + Recursive = true; + Fn->NeedsDecreasesCheck = Fn->Decreases != nullptr && Recursive; } return Out; } @@ -59,14 +232,19 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { const FunctionContractInfo *FCI = Ctx.getFunctionContract(FD); if (!FCI) return nullptr; - if (FCI->IsSpec || FCI->IsProof) - return nullptr; auto Fn = std::make_unique(); Fn->Name = FD->getNameAsString(); + Fn->IsSpec = FCI->IsSpec; + Fn->IsProof = FCI->IsProof; IntMode = FCI->IsSpec ? VIntMode::Math : VIntMode::Machine; + if (!FCI->IsSpec && contractsReferenceSpec(*FCI)) + IntMode = VIntMode::Math; Fn->IntMode = IntMode; Fn->ReturnType = VType::fromQualType(FD->getReturnType(), IntMode); + CurrentFn = Fn.get(); + if (FCI->Decreases) + Fn->Decreases = convertExpr(FCI->Decreases); SmallVector MutablePtrParams; for (const ParmVarDecl *P : FD->parameters()) { @@ -76,18 +254,47 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { MutablePtrParams.push_back(P); } + auto recordContractExpr = [&](const char *Clause, const Expr *E, + std::unique_ptr &Out) { + if (!E) + return; + Out = convertExpr(E); + if (!Out) + Errors.push_back(Fn->Name + ": unsupported expression in " + Clause); + }; + InPost = false; - for (const Expr *E : FCI->Preconditions) - Fn->Preconditions.push_back(convertExpr(E)); - for (const Expr *E : FCI->Postconditions) - Fn->Postconditions.push_back(convertExpr(E)); - for (const Expr *E : FCI->Recommends) - Fn->Recommends.push_back(convertExpr(E)); - for (const Expr *E : FCI->Modifies) - Fn->Modifies.push_back(convertExpr(E)); + for (const Expr *E : FCI->Preconditions) { + std::unique_ptr PE; + recordContractExpr("pre", E, PE); + if (PE) + Fn->Preconditions.push_back(std::move(PE)); + } + InPost = true; + for (const Expr *E : FCI->Postconditions) { + std::unique_ptr PE; + recordContractExpr("post", E, PE); + if (PE) + Fn->Postconditions.push_back(std::move(PE)); + } + InPost = false; + for (const Expr *E : FCI->Recommends) { + std::unique_ptr RE; + recordContractExpr("recommends", E, RE); + if (RE) + Fn->Recommends.push_back(std::move(RE)); + } + for (const Expr *E : FCI->Modifies) { + std::unique_ptr ME; + recordContractExpr("modifies", E, ME); + if (ME) + Fn->Modifies.push_back(std::move(ME)); + } for (const auto &Pair : FCI->Aliases) { - auto L = convertExpr(Pair.first); - auto R = convertExpr(Pair.second); + std::unique_ptr L; + std::unique_ptr R; + recordContractExpr("aliases", Pair.first, L); + recordContractExpr("aliases", Pair.second, R); if (L && R) Fn->Aliases.emplace_back(std::move(L), std::move(R)); } @@ -112,9 +319,38 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { if (const Stmt *Body = FD->getBody()) { Fn->Body = convertStmt(Body); - if (Fn->Body.empty() && Fn->Postconditions.empty()) + if (!Fn->IsSpec && Fn->Body.empty() && Fn->Postconditions.empty()) return nullptr; } + if (Fn->IsSpec && Fn->Body.empty() && !Fn->Decreases) + return nullptr; + CurrentFn = nullptr; + return Fn; +} + +std::unique_ptr +ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { + if (!FD->isConstexpr() || !FD->hasBody()) + return nullptr; + + auto Fn = std::make_unique(); + Fn->Name = FD->getNameAsString(); + Fn->IsSpec = true; + Fn->IsConstexprSpec = true; + IntMode = VIntMode::Machine; + Fn->IntMode = IntMode; + Fn->ReturnType = VType::fromQualType(FD->getReturnType(), IntMode); + CurrentFn = Fn.get(); + + for (const ParmVarDecl *P : FD->parameters()) + Fn->Params.emplace_back(P->getNameAsString(), + VType::fromQualType(P->getType(), IntMode)); + + if (const Stmt *Body = FD->getBody()) + Fn->Body = convertStmt(Body); + if (Fn->Body.empty()) + return nullptr; + CurrentFn = nullptr; return Fn; } @@ -141,7 +377,23 @@ std::unique_ptr ASTConverter::convertExpr(const Expr *E) { if (!E) return nullptr; E = E->IgnoreParenImpCasts(); + while (const auto *CE = dyn_cast(E)) { + if (CE->getCastKind() == CK_NoOp || CE->getCastKind() == CK_LValueToRValue || + CE->getCastKind() == CK_ConstructorConversion || + CE->getCastKind() == CK_UncheckedDerivedToBase) + E = CE->getSubExpr()->IgnoreParenImpCasts(); + else + break; + } + if (const auto *MTE = dyn_cast(E)) + return convertExpr(MTE->getSubExpr()); + if (const auto *CE = dyn_cast(E)) { + if (CE->getNumArgs() == 1) + return convertExpr(CE->getArg(0)); + if (CE->getNumArgs() == 0 && CE->getConstructor()->isDefaultConstructor()) + return nullptr; + } if (const auto *IL = dyn_cast(E)) { VType Ty = VType::fromQualType(E->getType(), IntMode); return std::make_unique(IL->getValue().getSExtValue(), Ty, @@ -227,6 +479,51 @@ std::unique_ptr ASTConverter::convertExpr(const Expr *E) { return std::make_unique(std::move(Cond), std::move(T), std::move(F), Ty, E->getExprLoc()); } + if (const auto *M = dyn_cast(E)) { + if (M->isArrow()) { + auto Base = convertExpr(M->getBase()); + if (!Base) + return nullptr; + auto Ptr = std::make_unique(std::move(Base), + VType::fromQualType(M->getBase()->getType(), IntMode), + E->getExprLoc()); + if (const auto *FD = dyn_cast(M->getMemberDecl())) { + VType Ty = VType::fromQualType(E->getType(), IntMode); + return std::make_unique(std::move(Ptr), Ty, E->getExprLoc()); + } + } + if (const auto *DRE = dyn_cast(M->getBase()->IgnoreParenImpCasts())) { + if (const auto *VD = dyn_cast(DRE->getDecl())) { + if (const auto *FD = dyn_cast(M->getMemberDecl())) { + VType Ty = VType::fromQualType(E->getType(), IntMode); + std::string Name = VD->getNameAsString() + "." + FD->getNameAsString(); + return std::make_unique(Name, Ty, E->getExprLoc()); + } + } + if (const auto *PD = dyn_cast(DRE->getDecl())) { + if (const auto *FD = dyn_cast(M->getMemberDecl())) { + VType Ty = VType::fromQualType(E->getType(), IntMode); + std::string Name = PD->getNameAsString() + "." + FD->getNameAsString(); + return std::make_unique(Name, Ty, E->getExprLoc()); + } + } + } + if (InPost && isa(M->getBase()->IgnoreParenImpCasts())) { + if (const auto *FD = dyn_cast(M->getMemberDecl())) { + VType Ty = VType::fromQualType(E->getType(), IntMode); + return std::make_unique("result." + FD->getNameAsString(), Ty, + E->getExprLoc()); + } + } + auto Base = convertExpr(M->getBase()); + if (!Base) + return nullptr; + if (const auto *FD = dyn_cast(M->getMemberDecl())) { + VType Ty = VType::fromQualType(E->getType(), IntMode); + return std::make_unique(std::move(Base), FD->getNameAsString(), Ty, + E->getExprLoc()); + } + } if (dyn_cast(E)) { if (!InPost) return nullptr; @@ -247,9 +544,70 @@ std::unique_ptr ASTConverter::convertExpr(const Expr *E) { Binder, convertExpr(Ex->getLo()), convertExpr(Ex->getHi()), convertExpr(Ex->getBody()), E->getExprLoc()); } + if (const auto *CE = dyn_cast(E)) { + if (const FunctionDecl *Callee = CE->getDirectCallee()) { + if (Callee->isConstexpr() && CE->isEvaluatable(Ctx)) { + Expr::EvalResult EV; + if (CE->EvaluateAsInt(EV, Ctx)) { + VType Ty = VType::fromQualType(E->getType(), VIntMode::Machine); + return std::make_unique(EV.Val.getInt().getSExtValue(), Ty, + E->getExprLoc()); + } + } + if (calleeIsSpec(Callee)) { + std::vector> Args; + for (const Expr *A : CE->arguments()) + if (auto AE = convertExpr(A)) + Args.push_back(std::move(AE)); + VType Ty = VType::fromQualType(E->getType(), specCallIntMode(Callee)); + return std::make_unique(Callee->getNameAsString(), + std::move(Args), Ty, E->getExprLoc()); + } + } + } return nullptr; } +void ASTConverter::convertExecCallArg( + const Expr *E, std::vector> &Prelude, + std::unique_ptr &Out) { + if (!E) { + Out = nullptr; + return; + } + E = E->IgnoreParenImpCasts(); + if (const auto *CE = dyn_cast(E)) { + if (const FunctionDecl *Callee = CE->getDirectCallee()) { + if (Ctx.getFunctionContract(Callee) && !calleeIsSpec(Callee) && + !calleeIsProof(Callee)) { + std::vector> InnerArgs; + convertExecCallArgs(CE, Prelude, InnerArgs); + std::string Tmp = "__nested_" + std::to_string(++NestedCallId); + Out = std::make_unique( + Tmp, VType::fromQualType(E->getType(), IntMode), E->getExprLoc()); + Prelude.push_back(std::make_unique( + Callee->getNameAsString(), std::move(InnerArgs), Tmp, + E->getExprLoc(), false)); + return; + } + } + } + Out = convertExpr(E); +} + +void ASTConverter::convertExecCallArgs(const CallExpr *CE, + std::vector> &Prelude, + std::vector> &Args) { + if (!CE) + return; + for (const Expr *A : CE->arguments()) { + std::unique_ptr Arg; + convertExecCallArg(A, Prelude, Arg); + if (Arg) + Args.push_back(std::move(Arg)); + } +} + std::vector> ASTConverter::convertStmt(const Stmt *S) { std::vector> Out; @@ -266,6 +624,27 @@ ASTConverter::convertStmt(const Stmt *S) { } if (S->getStmtClass() == Stmt::ReturnStmtClass) { const auto *RS = cast(S); + if (const Expr *RetE = RS->getRetValue()) { + const auto *CE = dyn_cast(RetE->IgnoreParenImpCasts()); + if (CE) { + if (const FunctionDecl *Callee = CE->getDirectCallee()) { + if (Ctx.getFunctionContract(Callee) && !calleeIsSpec(Callee) && + !calleeIsProof(Callee)) { + std::vector> Args; + convertExecCallArgs(CE, Out, Args); + Out.push_back(std::make_unique( + Callee->getNameAsString(), std::move(Args), "result", + RS->getBeginLoc(), false)); + Out.push_back(std::make_unique( + std::make_unique( + "result", VType::fromQualType(RS->getRetValue()->getType(), IntMode), + RS->getBeginLoc()), + RS->getBeginLoc())); + return Out; + } + } + } + } std::unique_ptr Val; if (RS->getRetValue()) Val = convertExpr(RS->getRetValue()); @@ -285,6 +664,112 @@ ASTConverter::convertStmt(const Stmt *S) { std::move(Else), IS->getBeginLoc())); return Out; } + if (const auto *WS = dyn_cast(S)) { + auto Cond = convertExpr(WS->getCond()); + if (!Cond) + return Out; + std::vector> Invariants; + std::unique_ptr Decreases; + if (const LoopContractInfo *LCI = Ctx.getLoopContract(WS)) { + for (const Expr *Inv : LCI->Invariants) + if (auto E = convertExpr(Inv)) + Invariants.push_back(std::move(E)); + if (LCI->Decreases) + Decreases = convertExpr(LCI->Decreases); + } + auto Body = convertStmt(WS->getBody()); + Out.push_back(std::make_unique(std::move(Cond), std::move(Invariants), + std::move(Decreases), std::move(Body), + WS->getBeginLoc())); + return Out; + } + if (const auto *FS = dyn_cast(S)) { + if (FS->getInit()) { + auto Init = convertStmt(FS->getInit()); + Out.insert(Out.end(), std::make_move_iterator(Init.begin()), + std::make_move_iterator(Init.end())); + } + auto Cond = convertExpr(FS->getCond()); + if (!Cond) + return Out; + std::vector> Invariants; + std::unique_ptr Decreases; + if (const LoopContractInfo *LCI = Ctx.getLoopContract(FS)) { + for (const Expr *Inv : LCI->Invariants) + if (auto E = convertExpr(Inv)) + Invariants.push_back(std::move(E)); + if (LCI->Decreases) + Decreases = convertExpr(LCI->Decreases); + } + auto Body = convertStmt(FS->getBody()); + if (const Expr *Inc = FS->getInc()) { + if (const auto *IncStmt = dyn_cast(Inc)) { + auto IncPart = convertStmt(IncStmt); + Body.insert(Body.end(), std::make_move_iterator(IncPart.begin()), + std::make_move_iterator(IncPart.end())); + } + } + Out.push_back(std::make_unique(std::move(Cond), std::move(Invariants), + std::move(Decreases), std::move(Body), + FS->getBeginLoc())); + return Out; + } + if (const auto *CE = dyn_cast(S)) { + if (const FunctionDecl *Callee = CE->getDirectCallee()) { + if (calleeIsSpec(Callee)) + return Out; + if (Ctx.getFunctionContract(Callee)) { + std::vector> Args; + convertExecCallArgs(CE, Out, Args); + bool IsProof = calleeIsProof(Callee); + Out.push_back(std::make_unique( + Callee->getNameAsString(), std::move(Args), "", CE->getExprLoc(), + IsProof)); + } + } + return Out; + } + if (const auto *GB = dyn_cast(S)) { + bool SavedGhost = InGhost; + InGhost = true; + auto Body = convertStmt(GB->getBody()); + InGhost = SavedGhost; + Out.push_back(std::make_unique(std::move(Body), GB->getBeginLoc())); + return Out; + } + if (const auto *RW = dyn_cast(S)) { + std::string SpecName = specNameFromExpr(RW->getFunction()); + unsigned FuelVal = 1; + if (const auto *IL = dyn_cast(RW->getFuel())) + FuelVal = static_cast(IL->getValue().getZExtValue()); + if (CurrentFn && !SpecName.empty()) { + CurrentFn->SpecFuel[SpecName] = std::max(CurrentFn->SpecFuel[SpecName], FuelVal); + CurrentFn->RevealedSpecs.insert(SpecName); + } + Out.push_back(std::make_unique(SpecName, FuelVal, RW->getBeginLoc())); + return Out; + } + if (const auto *H = dyn_cast(S)) { + std::string SpecName = specNameFromExpr(H->getFunction()); + if (CurrentFn && !SpecName.empty()) + CurrentFn->HiddenSpecs.insert(SpecName); + Out.push_back(std::make_unique(SpecName, H->getBeginLoc())); + return Out; + } + if (const auto *R = dyn_cast(S)) { + std::string SpecName = specNameFromExpr(R->getFunction()); + if (CurrentFn && !SpecName.empty()) { + CurrentFn->RevealedSpecs.insert(SpecName); + CurrentFn->SpecFuel[SpecName] = std::max(CurrentFn->SpecFuel[SpecName], 1u); + } + Out.push_back(std::make_unique(SpecName, R->getBeginLoc())); + return Out; + } + if (const auto *CA = dyn_cast(S)) { + if (auto C = convertExpr(CA->getCond())) + Out.push_back(std::make_unique(std::move(C), CA->getBeginLoc())); + return Out; + } if (const auto *BO = dyn_cast(S)) { if (BO->isAssignmentOp()) { if (const auto *DRE = dyn_cast(BO->getLHS()->IgnoreParenImpCasts())) { @@ -294,6 +779,24 @@ ASTConverter::convertStmt(const Stmt *S) { Out.push_back(std::make_unique( VD->getNameAsString(), std::move(Val), BO->getExprLoc())); } + } else if (const auto *ME = dyn_cast(BO->getLHS()->IgnoreParenImpCasts())) { + if (auto L = convertExpr(ME)) { + std::string Target; + if (L->K == VExpr::FieldAccess) + Target = static_cast(L.get())->Field; + if (const auto *FD = dyn_cast(ME->getMemberDecl())) { + std::string BaseName; + if (const auto *DRE = dyn_cast(ME->getBase()->IgnoreParenImpCasts())) + if (const auto *VD = dyn_cast(DRE->getDecl())) + BaseName = VD->getNameAsString(); + if (!BaseName.empty()) { + auto Val = convertExpr(BO->getRHS()); + if (Val) + Out.push_back(std::make_unique( + BaseName + "." + FD->getNameAsString(), std::move(Val), BO->getExprLoc())); + } + } + } } else if (const auto *U = dyn_cast( BO->getLHS()->IgnoreParenImpCasts())) { if (U->getOpcode() == UO_Deref) { @@ -312,6 +815,26 @@ ASTConverter::convertStmt(const Stmt *S) { const auto *VD = dyn_cast(D); if (!VD || !VD->hasInit()) continue; + if (const auto *CE = dyn_cast(VD->getInit())) { + if (const FunctionDecl *Callee = CE->getDirectCallee()) { + if (calleeIsSpec(Callee)) { + if (auto Val = convertExpr(CE)) { + Out.push_back(std::make_unique(VD->getNameAsString(), + std::move(Val), + VD->getBeginLoc())); + } + continue; + } + if (Ctx.getFunctionContract(Callee)) { + std::vector> Args; + convertExecCallArgs(CE, Out, Args); + Out.push_back(std::make_unique( + Callee->getNameAsString(), std::move(Args), VD->getNameAsString(), + VD->getBeginLoc(), calleeIsProof(Callee))); + continue; + } + } + } auto Val = convertExpr(VD->getInit()); if (Val) Out.push_back(std::make_unique(VD->getNameAsString(), diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index 1e5dd2c934..19dc3fe2dc 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -12,18 +12,35 @@ class ASTConverter { ASTContext &Ctx; VIntMode IntMode = VIntMode::Machine; bool InPost = false; + bool InGhost = false; std::string ResultName = "result"; + VFunction *CurrentFn = nullptr; + unsigned NestedCallId = 0; + std::vector Errors; public: explicit ASTConverter(ASTContext &Ctx) : Ctx(Ctx) {} std::vector> convertTranslationUnit(); + const std::vector &getErrors() const { return Errors; } private: std::unique_ptr convertFunction(const FunctionDecl *FD); + std::unique_ptr convertConstexprSpec(const FunctionDecl *FD); std::unique_ptr convertExpr(const Expr *E); std::vector> convertStmt(const Stmt *S); + void convertExecCallArgs(const CallExpr *CE, + std::vector> &Prelude, + std::vector> &Args); + void convertExecCallArg(const Expr *E, + std::vector> &Prelude, + std::unique_ptr &Out); VBinOp convertBinOpcode(BinaryOperatorKind Op); + bool calleeIsSpec(const FunctionDecl *FD) const; + bool calleeIsProof(const FunctionDecl *FD) const; + VIntMode specCallIntMode(const FunctionDecl *FD) const; + bool contractsReferenceSpec(const FunctionContractInfo &FCI) const; + static std::string specNameFromExpr(const Expr *E); }; } // namespace verify diff --git a/clang/lib/Verify/IR/VExpr.cpp b/clang/lib/Verify/IR/VExpr.cpp index 2fa8f22d1a..6eacf60b84 100644 --- a/clang/lib/Verify/IR/VExpr.cpp +++ b/clang/lib/Verify/IR/VExpr.cpp @@ -80,6 +80,76 @@ std::unique_ptr verify::cloneVExpr(const VExpr *E) { H->HeapBefore, H->HeapAfter, cloneVExpr(H->Ptr.get()), cloneVExpr(H->Val.get()), H->Loc); } + case VExpr::FieldAccess: { + const auto *F = static_cast(E); + return std::make_unique(cloneVExpr(F->Base.get()), F->Field, + F->Ty, F->Loc); + } + case VExpr::SpecCall: { + const auto *C = static_cast(E); + std::vector> Args; + for (const auto &A : C->Args) + Args.push_back(cloneVExpr(A.get())); + return std::make_unique(C->Callee, std::move(Args), C->Ty, C->Loc); + } } return nullptr; +} + +std::unique_ptr verify::substituteBinderInVExpr(const VExpr *E, + const std::string &Binder, + int64_t Value, + VIntMode Mode) { + if (!E) + return nullptr; + switch (E->K) { + case VExpr::Var: { + const auto *V = static_cast(E); + if (V->Name == Binder) + return std::make_unique(Value, VType::makeInt32(Mode), V->Loc); + return cloneVExpr(E); + } + case VExpr::BinOp: { + const auto *B = static_cast(E); + return std::make_unique( + B->Op, substituteBinderInVExpr(B->Lhs.get(), Binder, Value, Mode), + substituteBinderInVExpr(B->Rhs.get(), Binder, Value, Mode), B->Ty, B->Loc); + } + case VExpr::UnaryOp: { + const auto *U = static_cast(E); + return std::make_unique( + U->Op, substituteBinderInVExpr(U->Operand.get(), Binder, Value, Mode), U->Ty, + U->Loc); + } + case VExpr::Cast: { + const auto *C = static_cast(E); + return std::make_unique( + substituteBinderInVExpr(C->Inner.get(), Binder, Value, Mode), C->FromTy, C->Ty, + C->Loc); + } + case VExpr::Conditional: { + const auto *C = static_cast(E); + return std::make_unique( + substituteBinderInVExpr(C->Cond.get(), Binder, Value, Mode), + substituteBinderInVExpr(C->Then.get(), Binder, Value, Mode), + substituteBinderInVExpr(C->Else.get(), Binder, Value, Mode), C->Ty, C->Loc); + } + case VExpr::Forall: + case VExpr::Exists: { + const auto *Q = static_cast(E); + if (Q->Binder == Binder) + return cloneVExpr(E); + if (Q->K == VExpr::Forall) + return std::make_unique( + Q->Binder, substituteBinderInVExpr(Q->Lo.get(), Binder, Value, Mode), + substituteBinderInVExpr(Q->Hi.get(), Binder, Value, Mode), + substituteBinderInVExpr(Q->Body.get(), Binder, Value, Mode), Q->Loc); + return std::make_unique( + Q->Binder, substituteBinderInVExpr(Q->Lo.get(), Binder, Value, Mode), + substituteBinderInVExpr(Q->Hi.get(), Binder, Value, Mode), + substituteBinderInVExpr(Q->Body.get(), Binder, Value, Mode), Q->Loc); + } + default: + return cloneVExpr(E); + } } \ No newline at end of file diff --git a/clang/lib/Verify/IR/VExpr.h b/clang/lib/Verify/IR/VExpr.h index e661b25bfd..73abf28657 100644 --- a/clang/lib/Verify/IR/VExpr.h +++ b/clang/lib/Verify/IR/VExpr.h @@ -25,7 +25,7 @@ class VExpr { public: enum Kind { Literal, Var, BinOp, UnaryOp, Cast, Load, Result, Old, Conditional, - Forall, Exists, HeapStore + Forall, Exists, HeapStore, FieldAccess, SpecCall }; Kind K; @@ -154,8 +154,33 @@ class VHeapStoreExpr : public VExpr { HeapAfter(std::move(After)), Ptr(std::move(P)), Val(std::move(V)) {} }; +/// Struct field access: base.field (flattened to base.field in passivization). +class VFieldAccessExpr : public VExpr { +public: + std::unique_ptr Base; + std::string Field; + VFieldAccessExpr(std::unique_ptr B, std::string Field, VType Ty, + SourceLocation Loc) + : VExpr(FieldAccess, Ty, Loc), Base(std::move(B)), Field(std::move(Field)) {} +}; + +/// Call to a spec function (inlined or axiomatized during verification). +class VSpecCallExpr : public VExpr { +public: + std::string Callee; + std::vector> Args; + VSpecCallExpr(std::string Callee, std::vector> Args, + VType Ty, SourceLocation Loc) + : VExpr(SpecCall, Ty, Loc), Callee(std::move(Callee)), Args(std::move(Args)) {} +}; + std::unique_ptr cloneVExpr(const VExpr *E); +/// Replace references to a quantifier binder with a concrete integer literal. +std::unique_ptr substituteBinderInVExpr(const VExpr *E, + const std::string &Binder, + int64_t Value, VIntMode Mode); + } // namespace verify } // namespace clang diff --git a/clang/lib/Verify/IR/VStmt.cpp b/clang/lib/Verify/IR/VStmt.cpp index 6926573230..b745843ae7 100644 --- a/clang/lib/Verify/IR/VStmt.cpp +++ b/clang/lib/Verify/IR/VStmt.cpp @@ -1,2 +1,110 @@ //===--- VStmt.cpp --------------------------------------------------------===// -#include "VStmt.h" \ No newline at end of file +#include "VStmt.h" + +using namespace clang; +using namespace verify; + +std::unique_ptr verify::cloneVStmt(const VStmt *S) { + if (!S) + return nullptr; + switch (S->K) { + case VStmt::Assign: { + const auto &A = static_cast(*S); + return std::make_unique(A.Target, cloneVExpr(A.Value.get()), A.Loc); + } + case VStmt::Store: { + const auto &St = static_cast(*S); + return std::make_unique(cloneVExpr(St.Ptr.get()), + cloneVExpr(St.Value.get()), St.Loc); + } + case VStmt::If: { + const auto &I = static_cast(*S); + std::vector> Then, Else; + for (const auto &T : I.Then) + Then.push_back(cloneVStmt(T.get())); + for (const auto &E : I.Else) + Else.push_back(cloneVStmt(E.get())); + return std::make_unique(cloneVExpr(I.Cond.get()), std::move(Then), + std::move(Else), I.Loc); + } + case VStmt::While: { + const auto &W = static_cast(*S); + std::vector> Inv; + for (const auto &I : W.Invariants) + Inv.push_back(cloneVExpr(I.get())); + std::vector> Body; + for (const auto &B : W.Body) + Body.push_back(cloneVStmt(B.get())); + return std::make_unique( + cloneVExpr(W.Cond.get()), std::move(Inv), cloneVExpr(W.Decreases.get()), + std::move(Body), W.Loc); + } + case VStmt::Call: { + const auto &C = static_cast(*S); + std::vector> Args; + for (const auto &A : C.Args) + Args.push_back(cloneVExpr(A.get())); + return std::make_unique(C.Callee, std::move(Args), C.ResultTarget, + C.Loc, C.IsProofCall); + } + case VStmt::Return: { + const auto &R = static_cast(*S); + return std::make_unique(cloneVExpr(R.Value.get()), R.Loc); + } + case VStmt::GhostBlock: { + const auto &G = static_cast(*S); + std::vector> Body; + for (const auto &B : G.Body) + Body.push_back(cloneVStmt(B.get())); + return std::make_unique(std::move(Body), G.Loc); + } + case VStmt::RevealWithFuel: { + const auto &R = static_cast(*S); + return std::make_unique(R.SpecFunction, R.Fuel, R.Loc); + } + case VStmt::HideSpec: { + const auto &H = static_cast(*S); + return std::make_unique(H.SpecFunction, H.Loc); + } + case VStmt::RevealSpec: { + const auto &R = static_cast(*S); + return std::make_unique(R.SpecFunction, R.Loc); + } + case VStmt::ContractAssert: { + const auto &A = static_cast(*S); + return std::make_unique(cloneVExpr(A.Cond.get()), A.Loc); + } + default: + return nullptr; + } +} + +VFunction verify::cloneVFunction(const VFunction &Fn) { + VFunction Out; + Out.Name = Fn.Name; + Out.ReturnType = Fn.ReturnType; + Out.IntMode = Fn.IntMode; + Out.IsSpec = Fn.IsSpec; + Out.IsProof = Fn.IsProof; + Out.IsConstexprSpec = Fn.IsConstexprSpec; + Out.NeedsDecreasesCheck = Fn.NeedsDecreasesCheck; + Out.SpecFuel = Fn.SpecFuel; + Out.HiddenSpecs = Fn.HiddenSpecs; + Out.RevealedSpecs = Fn.RevealedSpecs; + Out.Params = Fn.Params; + for (const auto &P : Fn.Preconditions) + Out.Preconditions.push_back(cloneVExpr(P.get())); + for (const auto &P : Fn.Postconditions) + Out.Postconditions.push_back(cloneVExpr(P.get())); + for (const auto &R : Fn.Recommends) + Out.Recommends.push_back(cloneVExpr(R.get())); + for (const auto &M : Fn.Modifies) + Out.Modifies.push_back(cloneVExpr(M.get())); + for (const auto &A : Fn.Aliases) + Out.Aliases.emplace_back(cloneVExpr(A.first.get()), cloneVExpr(A.second.get())); + if (Fn.Decreases) + Out.Decreases = cloneVExpr(Fn.Decreases.get()); + for (const auto &S : Fn.Body) + Out.Body.push_back(cloneVStmt(S.get())); + return Out; +} \ No newline at end of file diff --git a/clang/lib/Verify/IR/VStmt.h b/clang/lib/Verify/IR/VStmt.h index cd835acab4..54caba8edf 100644 --- a/clang/lib/Verify/IR/VStmt.h +++ b/clang/lib/Verify/IR/VStmt.h @@ -3,6 +3,8 @@ #define LLVM_CLANG_VERIFY_IR_VSTMT_H #include "VExpr.h" +#include +#include #include #include #include @@ -14,7 +16,8 @@ namespace verify { class VStmt { public: enum Kind { - Assign, Store, If, Assert, Assume, Return, Seq, Havoc + Assign, Store, If, While, Call, Assert, Assume, Return, Seq, Havoc, + GhostBlock, RevealWithFuel, HideSpec, RevealSpec, ContractAssert }; Kind K; @@ -78,19 +81,86 @@ struct VHavocStmt : VStmt { : VStmt(Havoc, Loc), Target(std::move(T)) {} }; +struct VWhileStmt : VStmt { + std::unique_ptr Cond; + std::vector> Invariants; + std::unique_ptr Decreases; + std::vector> Body; + VWhileStmt(std::unique_ptr C, + std::vector> Inv, + std::unique_ptr Dec, + std::vector> B, SourceLocation Loc) + : VStmt(While, Loc), Cond(std::move(C)), Invariants(std::move(Inv)), + Decreases(std::move(Dec)), Body(std::move(B)) {} +}; + +struct VCallStmt : VStmt { + std::string Callee; + std::vector> Args; + std::string ResultTarget; + bool IsProofCall = false; + VCallStmt(std::string Callee, std::vector> Args, + std::string ResultTarget, SourceLocation Loc, bool IsProofCall = false) + : VStmt(Call, Loc), Callee(std::move(Callee)), Args(std::move(Args)), + ResultTarget(std::move(ResultTarget)), IsProofCall(IsProofCall) {} +}; + +struct VGhostBlockStmt : VStmt { + std::vector> Body; + VGhostBlockStmt(std::vector> B, SourceLocation Loc) + : VStmt(GhostBlock, Loc), Body(std::move(B)) {} +}; + +struct VRevealWithFuelStmt : VStmt { + std::string SpecFunction; + unsigned Fuel = 1; + VRevealWithFuelStmt(std::string Fn, unsigned Fuel, SourceLocation Loc) + : VStmt(RevealWithFuel, Loc), SpecFunction(std::move(Fn)), Fuel(Fuel) {} +}; + +struct VHideSpecStmt : VStmt { + std::string SpecFunction; + VHideSpecStmt(std::string Fn, SourceLocation Loc) + : VStmt(HideSpec, Loc), SpecFunction(std::move(Fn)) {} +}; + +struct VRevealSpecStmt : VStmt { + std::string SpecFunction; + VRevealSpecStmt(std::string Fn, SourceLocation Loc) + : VStmt(RevealSpec, Loc), SpecFunction(std::move(Fn)) {} +}; + +struct VContractAssertStmt : VStmt { + std::unique_ptr Cond; + VContractAssertStmt(std::unique_ptr C, SourceLocation Loc) + : VStmt(ContractAssert, Loc), Cond(std::move(C)) {} +}; + +std::unique_ptr cloneVStmt(const VStmt *S); + struct VFunction { std::string Name; VType ReturnType; VIntMode IntMode = VIntMode::Machine; + bool IsSpec = false; + bool IsProof = false; + bool IsConstexprSpec = false; + bool NeedsDecreasesCheck = false; + std::map SpecFuel; + std::set HiddenSpecs; + std::set RevealedSpecs; std::vector> Params; std::vector> Preconditions; std::vector> Postconditions; std::vector> Recommends; std::vector> Modifies; std::vector, std::unique_ptr>> Aliases; + std::unique_ptr Decreases; std::vector> Body; }; +VFunction cloneVFunction(const VFunction &Fn); + } // namespace verify } // namespace clang diff --git a/clang/lib/Verify/Transform/LoopUnroll.cpp b/clang/lib/Verify/Transform/LoopUnroll.cpp new file mode 100644 index 0000000000..40a9a831b8 --- /dev/null +++ b/clang/lib/Verify/Transform/LoopUnroll.cpp @@ -0,0 +1,103 @@ +//===--- LoopUnroll.cpp ---------------------------------------------------===// +#include "LoopUnroll.h" + +using namespace clang; +using namespace verify; + +static std::vector> +unrollStmts(const std::vector> &Stmts, unsigned K); + +static std::vector> +unrollStmts(const std::vector> &Stmts, unsigned K) { + std::vector> Out; + for (const auto &S : Stmts) { + if (S->K == VStmt::While) { + const auto &W = static_cast(*S); + for (unsigned I = 0; I < K; ++I) { + Out.push_back(std::make_unique( + cloneVExpr(W.Cond.get()), W.Loc)); + auto Body = unrollStmts(W.Body, K); + Out.insert(Out.end(), std::make_move_iterator(Body.begin()), + std::make_move_iterator(Body.end())); + } + auto NotCond = std::make_unique( + VUnaryOp::Not, cloneVExpr(W.Cond.get()), VType::makeBool(), W.Loc); + Out.push_back( + std::make_unique(std::move(NotCond), W.Loc)); + continue; + } + if (S->K == VStmt::If) { + const auto &I = static_cast(*S); + auto Then = unrollStmts(I.Then, K); + auto Else = unrollStmts(I.Else, K); + Out.push_back(std::make_unique(cloneVExpr(I.Cond.get()), + std::move(Then), std::move(Else), + I.Loc)); + continue; + } + if (S->K == VStmt::Seq) { + const auto &Seq = static_cast(*S); + auto Inner = unrollStmts(Seq.Stmts, K); + Out.insert(Out.end(), std::make_move_iterator(Inner.begin()), + std::make_move_iterator(Inner.end())); + continue; + } + switch (S->K) { + case VStmt::Assign: + Out.push_back(std::make_unique( + static_cast(*S).Target, + cloneVExpr(static_cast(*S).Value.get()), + S->Loc)); + break; + case VStmt::Store: + Out.push_back(std::make_unique( + cloneVExpr(static_cast(*S).Ptr.get()), + cloneVExpr(static_cast(*S).Value.get()), S->Loc)); + break; + case VStmt::Call: + Out.push_back(std::make_unique( + static_cast(*S).Callee, + [&] { + std::vector> Args; + for (const auto &A : static_cast(*S).Args) + Args.push_back(cloneVExpr(A.get())); + return Args; + }(), + static_cast(*S).ResultTarget, S->Loc)); + break; + case VStmt::Return: + Out.push_back(std::make_unique( + cloneVExpr(static_cast(*S).Value.get()), S->Loc)); + break; + default: + Out.push_back(cloneVStmt(S.get())); + break; + } + } + return Out; +} + +VFunction LoopUnroller::unroll(const VFunction &Fn, unsigned K) { + VFunction Out; + Out.Name = Fn.Name; + Out.ReturnType = Fn.ReturnType; + Out.IntMode = Fn.IntMode; + Out.Params = Fn.Params; + for (const auto &P : Fn.Preconditions) + Out.Preconditions.push_back(cloneVExpr(P.get())); + for (const auto &P : Fn.Postconditions) + Out.Postconditions.push_back(cloneVExpr(P.get())); + for (const auto &R : Fn.Recommends) + Out.Recommends.push_back(cloneVExpr(R.get())); + for (const auto &M : Fn.Modifies) + Out.Modifies.push_back(cloneVExpr(M.get())); + for (const auto &A : Fn.Aliases) + Out.Aliases.emplace_back(cloneVExpr(A.first.get()), cloneVExpr(A.second.get())); + if (K == 0) { + for (const auto &S : Fn.Body) + Out.Body.push_back(cloneVStmt(S.get())); + return Out; + } + Out.Body = unrollStmts(Fn.Body, K); + return Out; +} \ No newline at end of file diff --git a/clang/lib/Verify/Transform/LoopUnroll.h b/clang/lib/Verify/Transform/LoopUnroll.h new file mode 100644 index 0000000000..f3931d5aec --- /dev/null +++ b/clang/lib/Verify/Transform/LoopUnroll.h @@ -0,0 +1,18 @@ +//===--- LoopUnroll.h - Bounded loop unrolling for BMC ------------------===// +#ifndef LLVM_CLANG_VERIFY_TRANSFORM_LOOPUNROLL_H +#define LLVM_CLANG_VERIFY_TRANSFORM_LOOPUNROLL_H + +#include "../IR/VStmt.h" + +namespace clang { +namespace verify { + +class LoopUnroller { +public: + static VFunction unroll(const VFunction &Fn, unsigned K); +}; + +} // namespace verify +} // namespace clang + +#endif \ No newline at end of file diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index c051d63a97..83ef640d5f 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/clang/lib/Verify/Transform/Passivize.cpp @@ -2,6 +2,7 @@ #include "Passivize.h" #include #include +#include using namespace clang; using namespace verify; @@ -86,6 +87,35 @@ static std::unique_ptr cloneExpr(const VExpr *E, const CloneCtx &Ctx) { cloneExpr(C->Cond.get(), Ctx), cloneExpr(C->Then.get(), Ctx), cloneExpr(C->Else.get(), Ctx), C->Ty, C->Loc); } + case VExpr::FieldAccess: { + const auto *F = static_cast(E); + std::string Name; + if (F->Base->K == VExpr::Var) + Name = static_cast(F->Base.get())->Name; + else if (F->Base->K == VExpr::Result) { + if (auto It = Ctx.Renames.find("result"); It != Ctx.Renames.end()) + Name = It->second; + else + Name = "result"; + } else + Name = "base"; + Name += "." + F->Field; + if (Ctx.UseOldState) { + if (auto It = Ctx.OldState.find(Name); It != Ctx.OldState.end()) + return cloneExpr(It->second.get(), CloneCtx{Ctx.Renames, Ctx.OldState, false}); + } + if (auto It = Ctx.Renames.find(Name); It != Ctx.Renames.end()) + Name = It->second; + return std::make_unique(Name, F->Ty, F->Loc); + } + case VExpr::SpecCall: { + const auto *C = static_cast(E); + std::vector> Args; + for (const auto &A : C->Args) + Args.push_back(cloneExpr(A.get(), Ctx)); + return std::make_unique(C->Callee, std::move(Args), C->Ty, + C->Loc); + } case VExpr::Forall: case VExpr::Exists: { const auto *Q = static_cast(E); @@ -125,6 +155,33 @@ static bool sameLvalue(const VExpr *A, const VExpr *B) { return false; } +static void collectDottedVars(const VExpr *E, std::set &Out) { + if (!E) + return; + if (E->K == VExpr::Var) { + const auto &N = static_cast(E)->Name; + if (N.find('.') != std::string::npos) + Out.insert(N); + return; + } + if (E->K == VExpr::BinOp) { + const auto *B = static_cast(E); + collectDottedVars(B->Lhs.get(), Out); + collectDottedVars(B->Rhs.get(), Out); + return; + } + if (E->K == VExpr::UnaryOp) + collectDottedVars(static_cast(E)->Operand.get(), Out); + if (E->K == VExpr::Old) + collectDottedVars(static_cast(E)->Inner.get(), Out); + if (E->K == VExpr::Load) + collectDottedVars(static_cast(E)->Ptr.get(), Out); + if (E->K == VExpr::FieldAccess) { + const auto *F = static_cast(E); + collectDottedVars(F->Base.get(), Out); + } +} + static bool storeAllowedByModifies( const VStoreStmt &St, const std::vector> &Modifies) { @@ -136,11 +193,56 @@ static bool storeAllowedByModifies( return false; } +static std::unique_ptr +substParams(const VExpr *E, const std::map> &Map, + const CloneCtx &Ctx) { + if (!E) + return nullptr; + if (E->K == VExpr::Var) { + const auto *V = static_cast(E); + if (auto It = Map.find(V->Name); It != Map.end()) + return cloneExpr(It->second.get(), Ctx); + return cloneExpr(E, Ctx); + } + if (E->K == VExpr::BinOp) { + const auto *B = static_cast(E); + return std::make_unique( + B->Op, substParams(B->Lhs.get(), Map, Ctx), substParams(B->Rhs.get(), Map, Ctx), + B->Ty, B->Loc); + } + if (E->K == VExpr::UnaryOp) { + const auto *U = static_cast(E); + return std::make_unique( + U->Op, substParams(U->Operand.get(), Map, Ctx), U->Ty, U->Loc); + } + if (E->K == VExpr::Load) { + const auto *L = static_cast(E); + return std::make_unique(substParams(L->Ptr.get(), Map, Ctx), L->Ty, L->Loc, + L->HeapVar); + } + if (E->K == VExpr::Old) { + const auto *O = static_cast(E); + return std::make_unique(substParams(O->Inner.get(), Map, Ctx), O->Ty, O->Loc); + } + if (E->K == VExpr::Result) { + if (auto It = Map.find("result"); It != Map.end()) + return cloneExpr(It->second.get(), Ctx); + return std::make_unique(E->Ty, E->Loc); + } + if (E->K == VExpr::FieldAccess) { + const auto *F = static_cast(E); + return std::make_unique(substParams(F->Base.get(), Map, Ctx), + F->Field, F->Ty, F->Loc); + } + return cloneExpr(E, Ctx); +} + class PassivizerImpl { std::map Versions; std::map> OldState; std::string ResultVar = "__result"; const VFunction &Fn; + FunctionMap FnMap; std::string versionedName(const std::string &N) { int &V = Versions[N]; @@ -152,7 +254,8 @@ class PassivizerImpl { } public: - explicit PassivizerImpl(const VFunction &Fn) : Fn(Fn) {} + PassivizerImpl(const VFunction &Fn, FunctionMap FnMap) + : Fn(Fn), FnMap(std::move(FnMap)) {} PassiveProgram run() { PassiveProgram P; @@ -171,6 +274,19 @@ class PassivizerImpl { Renames[Param.first] = V0; } + std::set FieldVars; + for (const auto &Pre : Fn.Preconditions) + collectDottedVars(Pre.get(), FieldVars); + for (const auto &Post : Fn.Postconditions) + collectDottedVars(Post.get(), FieldVars); + for (const std::string &FV : FieldVars) { + if (OldState.count(FV)) + continue; + std::string V0 = versionedName(FV); + OldState[FV] = std::make_unique(V0, VType::makeInt32(Fn.IntMode), SourceLocation()); + Renames[FV] = V0; + } + for (const auto &Pre : Fn.Preconditions) { CloneCtx PCtx{Renames, OldState, false}; P.EntryAssumes.push_back(cloneExpr(Pre.get(), PCtx)); @@ -187,9 +303,49 @@ class PassivizerImpl { P.ExitAsserts.push_back(cloneExpr(Post.get(), PCtx)); } P.OldHeapName = Heap0; + P.SpecFunctions = FnMap; + P.SpecFuel = Fn.SpecFuel; + P.HiddenSpecs = Fn.HiddenSpecs; + P.RevealedSpecs = Fn.RevealedSpecs; + P.CallerIntMode = Fn.IntMode; return P; } + void emitCallStmt(const VCallStmt &C, PassiveProgram &P, + std::map &Renames) { + auto CalleeIt = FnMap.find(C.Callee); + if (CalleeIt == FnMap.end()) + return; + const VFunction *Callee = CalleeIt->second; + if (Callee->IsSpec) + return; + CloneCtx Ctx{Renames, OldState, false}; + std::map> ParamMap; + for (unsigned I = 0; I < Callee->Params.size() && I < C.Args.size(); ++I) + ParamMap[Callee->Params[I].first] = cloneVExpr(C.Args[I].get()); + std::string RetVer; + if (!C.ResultTarget.empty()) { + RetVer = bump(C.ResultTarget); + Renames[C.ResultTarget] = RetVer; + ParamMap["result"] = + std::make_unique(RetVer, Callee->ReturnType, C.Loc); + } + for (const auto &Pre : Callee->Preconditions) { + auto PS = std::make_unique(); + PS->K = PassiveStmt::Assume; + PS->Cond = substParams(Pre.get(), ParamMap, Ctx); + P.Stmts.push_back(std::move(PS)); + } + if (!Callee->Modifies.empty()) + Renames[VHeapName] = bump(VHeapName); + for (const auto &Post : Callee->Postconditions) { + auto PS = std::make_unique(); + PS->K = PassiveStmt::Assume; + PS->Cond = substParams(Post.get(), ParamMap, Ctx); + P.Stmts.push_back(std::move(PS)); + } + } + void processStmt(const VStmt &S, PassiveProgram &P, std::map &Renames) { switch (S.K) { @@ -270,6 +426,38 @@ class PassivizerImpl { case VStmt::Return: { const auto &R = static_cast(S); CloneCtx Ctx{Renames, OldState, false}; + const VExpr *RetVal = R.Value.get(); + while (RetVal && RetVal->K == VExpr::Cast) + RetVal = static_cast(RetVal)->Inner.get(); + if (RetVal && RetVal->K == VExpr::Var) { + const std::string &Src = static_cast(RetVal)->Name; + std::set PostFields; + for (const auto &Post : Fn.Postconditions) + collectDottedVars(Post.get(), PostFields); + bool LinkedFields = false; + for (const std::string &FV : PostFields) { + if (FV.rfind("result.", 0) != 0) + continue; + std::string SrcField = Src + "." + FV.substr(7); + std::string DstVer = bump(FV); + Renames[FV] = DstVer; + std::string SrcVer = SrcField; + if (auto It = Renames.find(SrcField); It != Renames.end()) + SrcVer = It->second; + auto PS = std::make_unique(); + PS->K = PassiveStmt::Assume; + PS->Cond = makeEq( + std::make_unique(DstVer, VType::makeInt32(Fn.IntMode), R.Loc), + std::make_unique(SrcVer, VType::makeInt32(Fn.IntMode), R.Loc), + R.Loc); + P.Stmts.push_back(std::move(PS)); + LinkedFields = true; + } + if (LinkedFields) { + Renames["result"] = Renames.count("result.x") ? Renames["result.x"] : bump(ResultVar); + break; + } + } std::unique_ptr Ret = R.Value ? cloneExpr(R.Value.get(), Ctx) : std::make_unique(0, VType::makeInt32(Fn.IntMode), R.Loc); @@ -282,6 +470,73 @@ class PassivizerImpl { P.Stmts.push_back(std::move(PS)); break; } + case VStmt::While: { + const auto &W = static_cast(S); + auto EntryRenames = Renames; + CloneCtx Ctx{Renames, OldState, false}; + for (const auto &Inv : W.Invariants) { + auto PS = std::make_unique(); + PS->K = PassiveStmt::Assume; + PS->Cond = cloneExpr(Inv.get(), Ctx); + P.Stmts.push_back(std::move(PS)); + } + auto PSCond = std::make_unique(); + PSCond->K = PassiveStmt::Assume; + PSCond->Cond = cloneExpr(W.Cond.get(), Ctx); + P.Stmts.push_back(std::move(PSCond)); + auto BodyRenames = Renames; + for (const auto &BS : W.Body) + processStmt(*BS, P, BodyRenames); + for (const auto &Inv : W.Invariants) { + CloneCtx ACtx{BodyRenames, OldState, false}; + auto PS = std::make_unique(); + PS->K = PassiveStmt::Assert; + PS->Cond = cloneExpr(Inv.get(), ACtx); + P.Stmts.push_back(std::move(PS)); + } + std::set Changed; + for (const auto &[Name, Ver] : BodyRenames) { + if (EntryRenames.count(Name) && EntryRenames[Name] != Ver) + Changed.insert(Name); + } + for (const std::string &Name : Changed) + Renames[Name] = bump(Name); + CloneCtx ExitCtx{Renames, OldState, false}; + auto NotC = std::make_unique( + VUnaryOp::Not, cloneExpr(W.Cond.get(), ExitCtx), VType::makeBool(), W.Loc); + auto PSExit = std::make_unique(); + PSExit->K = PassiveStmt::Assume; + std::unique_ptr ExitAss = std::move(NotC); + for (const auto &Inv : W.Invariants) + ExitAss = std::make_unique( + VBinOp::And, std::move(ExitAss), cloneExpr(Inv.get(), ExitCtx), + VType::makeBool(), W.Loc); + PSExit->Cond = std::move(ExitAss); + P.Stmts.push_back(std::move(PSExit)); + break; + } + case VStmt::GhostBlock: { + const auto &G = static_cast(S); + for (const auto &BS : G.Body) + processStmt(*BS, P, Renames); + break; + } + case VStmt::ContractAssert: { + const auto &A = static_cast(S); + CloneCtx Ctx{Renames, OldState, false}; + auto PS = std::make_unique(); + PS->K = PassiveStmt::Assert; + PS->Cond = cloneExpr(A.Cond.get(), Ctx); + P.Stmts.push_back(std::move(PS)); + break; + } + case VStmt::RevealWithFuel: + case VStmt::HideSpec: + case VStmt::RevealSpec: + break; + case VStmt::Call: + emitCallStmt(static_cast(S), P, Renames); + break; default: break; } @@ -289,6 +544,6 @@ class PassivizerImpl { }; PassiveProgram Passivizer::run(const VFunction &Fn) { - PassivizerImpl Impl(Fn); + PassivizerImpl Impl(Fn, FnMap); return Impl.run(); } \ No newline at end of file diff --git a/clang/lib/Verify/Transform/Passivize.h b/clang/lib/Verify/Transform/Passivize.h index a5e1898116..42d861fb1d 100644 --- a/clang/lib/Verify/Transform/Passivize.h +++ b/clang/lib/Verify/Transform/Passivize.h @@ -3,10 +3,14 @@ #define LLVM_CLANG_VERIFY_TRANSFORM_PASSIVIZE_H #include "../IR/VStmt.h" +#include +#include namespace clang { namespace verify { +using FunctionMap = std::map; + struct PassiveStmt { enum Kind { Assume, Assert }; Kind K = Assume; @@ -19,10 +23,19 @@ struct PassiveProgram { std::vector> ExitAsserts; std::string ResultVarName; std::string OldHeapName; + /// Spec registry + per-enclosing-function reveal/hide (for Z3 axiom emission). + FunctionMap SpecFunctions; + std::map SpecFuel; + std::set HiddenSpecs; + std::set RevealedSpecs; + VIntMode CallerIntMode = VIntMode::Machine; }; class Passivizer { + FunctionMap FnMap; + public: + void setFunctionMap(FunctionMap Map) { FnMap = std::move(Map); } PassiveProgram run(const VFunction &Fn); }; diff --git a/clang/lib/Verify/Transform/SpecInline.cpp b/clang/lib/Verify/Transform/SpecInline.cpp new file mode 100644 index 0000000000..bdfe2cd1f6 --- /dev/null +++ b/clang/lib/Verify/Transform/SpecInline.cpp @@ -0,0 +1,563 @@ +//===--- SpecInline.cpp ---------------------------------------------------===// +#include "SpecInline.h" +#include "../Transform/Passivize.h" +#include +#include +#include + +using namespace clang; +using namespace verify; + +static std::map> +bindParams(const VFunction &Fn, + const std::vector> &Args) { + std::map> Env; + for (unsigned I = 0; I < Fn.Params.size() && I < Args.size(); ++I) + Env[Fn.Params[I].first] = cloneVExpr(Args[I].get()); + return Env; +} + +static std::unique_ptr envLookup(const std::map> &Env, + const std::string &Name, VType Ty, + SourceLocation Loc) { + if (auto It = Env.find(Name); It != Env.end()) + return cloneVExpr(It->second.get()); + return std::make_unique(Name, Ty, Loc); +} + +class SpecInlinerImpl { + const FunctionMap &FnMap; + std::map Fuel; + std::set Hidden; + std::set Revealed; + unsigned OpaqueId = 0; + unsigned InlineDepth = 0; + static constexpr unsigned MaxInlineDepth = 256; + + unsigned fuelFor(const std::string &Name) const { + if (Hidden.count(Name)) + return 0; + if (auto It = Fuel.find(Name); It != Fuel.end()) + return It->second; + auto It = FnMap.find(Name); + if (It != FnMap.end() && It->second->NeedsDecreasesCheck) + return 0; + return 1; + } + + std::unique_ptr opaqueCall(const VSpecCallExpr &C) { + std::string Name = "__spec_" + C.Callee + "_" + std::to_string(++OpaqueId); + return std::make_unique(Name, C.Ty, C.Loc); + } + +public: + SpecInlinerImpl(const FunctionMap &FnMap, std::map Fuel, + std::set Hidden, std::set Revealed) + : FnMap(FnMap), Fuel(std::move(Fuel)), Hidden(std::move(Hidden)), + Revealed(std::move(Revealed)) {} + + std::unique_ptr inlineExpr(std::unique_ptr E) { + std::map> Env; + return evalExpr(E.get(), Env); + } + + std::unique_ptr inlineSpecCall(const VSpecCallExpr &C) { + if (InlineDepth++ >= MaxInlineDepth) + return opaqueCall(C); + struct DepthGuard { + unsigned &D; + ~DepthGuard() { --D; } + } Guard{InlineDepth}; + if (Hidden.count(C.Callee)) + return opaqueCall(C); + auto It = FnMap.find(C.Callee); + if (It == FnMap.end() || !It->second->IsSpec) + return opaqueCall(C); + const VFunction &Spec = *It->second; + unsigned F = fuelFor(C.Callee); + if (Revealed.count(C.Callee) && F == 0) + F = 1; + if (Spec.NeedsDecreasesCheck) { + if (F == 0) + return opaqueCall(C); + auto Env = bindParams(Spec, C.Args); + auto OldFuel = Fuel[Spec.Name]; + Fuel[Spec.Name] = F > 0 ? F - 1 : 0; + auto Out = evalBody(Spec.Body, Env); + Fuel[Spec.Name] = OldFuel; + if (!Out) + return opaqueCall(C); + return Out; + } + auto Env = bindParams(Spec, C.Args); + if (auto Out = evalBody(Spec.Body, Env)) + return Out; + return opaqueCall(C); + } + + std::unique_ptr evalExpr(const VExpr *E, + const std::map> &Env) { + if (!E) + return nullptr; + switch (E->K) { + case VExpr::Literal: + return cloneVExpr(E); + case VExpr::Var: + return envLookup(Env, static_cast(E)->Name, E->Ty, E->Loc); + case VExpr::BinOp: { + const auto *B = static_cast(E); + auto L = evalExpr(B->Lhs.get(), Env); + auto R = evalExpr(B->Rhs.get(), Env); + if (!L || !R) + return nullptr; + return std::make_unique(B->Op, std::move(L), std::move(R), B->Ty, B->Loc); + } + case VExpr::UnaryOp: { + const auto *U = static_cast(E); + auto O = evalExpr(U->Operand.get(), Env); + if (!O) + return nullptr; + return std::make_unique(U->Op, std::move(O), U->Ty, U->Loc); + } + case VExpr::Cast: { + const auto *C = static_cast(E); + auto I = evalExpr(C->Inner.get(), Env); + if (!I) + return nullptr; + return std::make_unique(std::move(I), C->FromTy, C->Ty, C->Loc); + } + case VExpr::Conditional: { + const auto *C = static_cast(E); + auto Cond = evalExpr(C->Cond.get(), Env); + auto T = evalExpr(C->Then.get(), Env); + auto F = evalExpr(C->Else.get(), Env); + if (!Cond || !T || !F) + return nullptr; + return std::make_unique(std::move(Cond), std::move(T), std::move(F), + C->Ty, C->Loc); + } + case VExpr::SpecCall: + return inlineSpecCall(*static_cast(E)); + case VExpr::Forall: + case VExpr::Exists: { + const auto *Q = static_cast(E); + auto Body = evalExpr(Q->Body.get(), Env); + if (!Body) + return nullptr; + if (E->K == VExpr::Forall) + return std::unique_ptr(std::make_unique( + Q->Binder, cloneVExpr(Q->Lo.get()), cloneVExpr(Q->Hi.get()), + std::move(Body), Q->Loc)); + return std::unique_ptr(std::make_unique( + Q->Binder, cloneVExpr(Q->Lo.get()), cloneVExpr(Q->Hi.get()), + std::move(Body), Q->Loc)); + } + default: + return cloneVExpr(E); + } + } + + std::unique_ptr evalBodySeq( + const std::vector> &Body, + std::map> &Env, unsigned Idx) { + if (Idx >= Body.size()) + return nullptr; + const VStmt &S = *Body[Idx]; + switch (S.K) { + case VStmt::Assign: { + const auto &A = static_cast(S); + Env[A.Target] = evalExpr(A.Value.get(), Env); + return evalBodySeq(Body, Env, Idx + 1); + } + case VStmt::Return: { + const auto &R = static_cast(S); + return evalExpr(R.Value.get(), Env); + } + case VStmt::If: { + const auto &I = static_cast(S); + auto Cond = evalExpr(I.Cond.get(), Env); + if (!Cond) + return nullptr; + if (I.Else.empty()) { + auto ThenEnv = cloneEnv(Env); + auto ThenVal = evalBody(I.Then, ThenEnv); + auto Rest = evalBodySeq(Body, Env, Idx + 1); + if (!ThenVal || !Rest) + return nullptr; + return std::make_unique(std::move(Cond), std::move(ThenVal), + std::move(Rest), ThenVal->Ty, I.Loc); + } + auto ThenEnv = cloneEnv(Env); + auto ElseEnv = cloneEnv(Env); + auto ThenVal = evalBody(I.Then, ThenEnv); + auto ElseVal = evalBody(I.Else, ElseEnv); + if (!ThenVal || !ElseVal) + return nullptr; + return std::make_unique(std::move(Cond), std::move(ThenVal), + std::move(ElseVal), ThenVal->Ty, I.Loc); + } + case VStmt::GhostBlock: { + const auto &G = static_cast(S); + if (auto R = evalBody(G.Body, Env)) + return R; + return evalBodySeq(Body, Env, Idx + 1); + } + default: + return evalBodySeq(Body, Env, Idx + 1); + } + } + + static std::map> + cloneEnv(const std::map> &Env) { + std::map> Out; + for (const auto &[K, V] : Env) + Out[K] = cloneVExpr(V.get()); + return Out; + } + + std::unique_ptr evalBody(const std::vector> &Body, + std::map> &Env) { + return evalBodySeq(Body, Env, 0); + } + + void inlineStmts(std::vector> &Stmts) { + for (auto &S : Stmts) { + switch (S->K) { + case VStmt::Assign: { + auto &A = static_cast(*S); + A.Value = inlineExpr(std::move(A.Value)); + break; + } + case VStmt::Return: { + auto &R = static_cast(*S); + R.Value = inlineExpr(std::move(R.Value)); + break; + } + case VStmt::If: { + auto &I = static_cast(*S); + I.Cond = inlineExpr(std::move(I.Cond)); + inlineStmts(I.Then); + inlineStmts(I.Else); + break; + } + case VStmt::While: { + auto &W = static_cast(*S); + W.Cond = inlineExpr(std::move(W.Cond)); + for (auto &Inv : W.Invariants) + Inv = inlineExpr(std::move(Inv)); + if (W.Decreases) + W.Decreases = inlineExpr(std::move(W.Decreases)); + inlineStmts(W.Body); + break; + } + case VStmt::ContractAssert: { + auto &A = static_cast(*S); + A.Cond = inlineExpr(std::move(A.Cond)); + break; + } + case VStmt::GhostBlock: { + auto &G = static_cast(*S); + inlineStmts(G.Body); + break; + } + default: + break; + } + } + } +}; + +static std::unique_ptr opaqueSpecExpr(const VExpr *E, unsigned &Id) { + if (!E) + return nullptr; + if (E->K == VExpr::SpecCall) { + const auto *C = static_cast(E); + return std::make_unique("__spec_" + C->Callee + "_" + std::to_string(++Id), + C->Ty, C->Loc); + } + if (E->K == VExpr::BinOp) { + const auto *B = static_cast(E); + return std::make_unique( + B->Op, opaqueSpecExpr(B->Lhs.get(), Id), opaqueSpecExpr(B->Rhs.get(), Id), B->Ty, + B->Loc); + } + if (E->K == VExpr::UnaryOp) { + const auto *U = static_cast(E); + return std::make_unique( + U->Op, opaqueSpecExpr(U->Operand.get(), Id), U->Ty, U->Loc); + } + if (E->K == VExpr::Old) + return opaqueSpecExpr(static_cast(E)->Inner.get(), Id); + if (E->K == VExpr::Conditional) { + const auto *C = static_cast(E); + return std::make_unique( + opaqueSpecExpr(C->Cond.get(), Id), opaqueSpecExpr(C->Then.get(), Id), + opaqueSpecExpr(C->Else.get(), Id), C->Ty, C->Loc); + } + return cloneVExpr(E); +} + +static void opaqueAllSpecCalls(VFunction &Fn) { + unsigned Id = 0; + for (auto &P : Fn.Preconditions) + P = opaqueSpecExpr(P.get(), Id); + for (auto &P : Fn.Postconditions) + P = opaqueSpecExpr(P.get(), Id); + for (auto &R : Fn.Recommends) + R = opaqueSpecExpr(R.get(), Id); +} + +void SpecInliner::prepareFunctionAxiomatic(VFunction &Fn) { + (void)Fn; +} + +void SpecInliner::prepareFunction(VFunction &Fn) { + for (const auto &KV : Fn.SpecFuel) + Fuel[KV.first] = std::max(Fuel[KV.first], KV.second); + + SpecInlinerImpl Impl(FnMap, Fuel, Fn.HiddenSpecs, Fn.RevealedSpecs); + for (auto &Pre : Fn.Preconditions) + Pre = Impl.inlineExpr(std::move(Pre)); + for (auto &Post : Fn.Postconditions) + Post = Impl.inlineExpr(std::move(Post)); + for (auto &Rec : Fn.Recommends) + Rec = Impl.inlineExpr(std::move(Rec)); + Impl.inlineStmts(Fn.Body); +} + +std::unique_ptr SpecInliner::unfoldDefinition( + const VFunction &Spec, const std::map &FuelMap, + const std::set &Hidden, const std::set &Revealed, + unsigned RootFuel) const { + std::vector> Args; + for (const auto &P : Spec.Params) + Args.push_back( + std::make_unique(P.first, P.second, SourceLocation())); + auto Call = std::make_unique(Spec.Name, std::move(Args), + Spec.ReturnType, SourceLocation()); + std::map Fuel = FuelMap; + Fuel[Spec.Name] = std::max(Fuel[Spec.Name], RootFuel); + SpecInlinerImpl Impl(FnMap, Fuel, Hidden, Revealed); + return Impl.inlineSpecCall(*Call); +} + +std::unique_ptr SpecInliner::inlineExpr(std::unique_ptr E) { + SpecInlinerImpl Impl(FnMap, Fuel, {}, {}); + return Impl.inlineExpr(std::move(E)); +} + +void verify::collectSpecCalls(const VExpr *E, + std::vector &Out) { + if (!E) + return; + if (E->K == VExpr::SpecCall) + Out.push_back(static_cast(E)); + if (E->K == VExpr::BinOp) { + const auto *B = static_cast(E); + collectSpecCalls(B->Lhs.get(), Out); + collectSpecCalls(B->Rhs.get(), Out); + } else if (E->K == VExpr::UnaryOp) { + collectSpecCalls(static_cast(E)->Operand.get(), Out); + } else if (E->K == VExpr::Conditional) { + const auto *C = static_cast(E); + collectSpecCalls(C->Cond.get(), Out); + collectSpecCalls(C->Then.get(), Out); + collectSpecCalls(C->Else.get(), Out); + } else if (E->K == VExpr::Old) { + collectSpecCalls(static_cast(E)->Inner.get(), Out); + } +} + +void verify::collectSpecCallsInFunction(const VFunction &Fn, + std::vector &Out) { + for (const auto &P : Fn.Preconditions) + collectSpecCalls(P.get(), Out); + for (const auto &P : Fn.Postconditions) + collectSpecCalls(P.get(), Out); + for (const auto &S : Fn.Body) { + if (S->K == VStmt::Assign) + collectSpecCalls(static_cast(*S).Value.get(), Out); + if (S->K == VStmt::Return) + collectSpecCalls(static_cast(*S).Value.get(), Out); + } +} + + + +std::unique_ptr +verify::substParamsInExpr(const VExpr *E, + const std::map> &Map) { + if (!E) + return nullptr; + if (E->K == VExpr::Var) { + const auto *V = static_cast(E); + if (auto It = Map.find(V->Name); It != Map.end()) + return cloneVExpr(It->second.get()); + return cloneVExpr(E); + } + if (E->K == VExpr::BinOp) { + const auto *B = static_cast(E); + return std::make_unique( + B->Op, substParamsInExpr(B->Lhs.get(), Map), substParamsInExpr(B->Rhs.get(), Map), + B->Ty, B->Loc); + } + if (E->K == VExpr::UnaryOp) { + const auto *U = static_cast(E); + return std::make_unique( + U->Op, substParamsInExpr(U->Operand.get(), Map), U->Ty, U->Loc); + } + return cloneVExpr(E); +} + +static void collectRecursiveCalls( + const std::vector> &Stmts, const std::string &Self, + const FunctionMap &FnMap, + std::vector>>> + &Sites, + std::map> &Env) { + for (const auto &S : Stmts) { + switch (S->K) { + case VStmt::Assign: { + const auto &A = static_cast(*S); + Env[A.Target] = cloneVExpr(A.Value.get()); + break; + } + case VStmt::Call: { + const auto &C = static_cast(*S); + auto It = FnMap.find(C.Callee); + if (It != FnMap.end() && It->second->IsSpec && + (C.Callee == Self || It->second->NeedsDecreasesCheck)) { + std::map> Args; + for (unsigned I = 0; I < It->second->Params.size() && I < C.Args.size(); ++I) + Args[It->second->Params[I].first] = cloneVExpr(C.Args[I].get()); + Sites.emplace_back(&C, std::move(Args)); + } + break; + } + case VStmt::If: { + const auto &I = static_cast(*S); + collectRecursiveCalls(I.Then, Self, FnMap, Sites, Env); + collectRecursiveCalls(I.Else, Self, FnMap, Sites, Env); + break; + } + case VStmt::While: { + const auto &W = static_cast(*S); + collectRecursiveCalls(W.Body, Self, FnMap, Sites, Env); + break; + } + case VStmt::GhostBlock: + collectRecursiveCalls(static_cast(*S).Body, Self, FnMap, + Sites, Env); + break; + default: + break; + } + } +} + +bool verify::functionHasRecursiveSpecCall(const VFunction &Fn, + const FunctionMap &FnMap) { + std::vector>>> + Sites; + std::map> Env; + collectRecursiveCalls(Fn.Body, Fn.Name, FnMap, Sites, Env); + if (!Sites.empty()) + return true; + for (const auto &S : Fn.Body) + if (S->K == VStmt::Call && static_cast(*S).Callee == Fn.Name) + return true; + return false; +} + +static void collectRecursiveSpecCallsInExpr( + const VExpr *E, const VFunction &Fn, + std::vector>> &ArgMaps) { + if (!E) + return; + if (E->K == VExpr::SpecCall) { + const auto *C = static_cast(E); + if (C->Callee == Fn.Name) { + std::map> Args; + for (unsigned I = 0; I < Fn.Params.size() && I < C->Args.size(); ++I) + Args[Fn.Params[I].first] = cloneVExpr(C->Args[I].get()); + ArgMaps.push_back(std::move(Args)); + } + for (const auto &A : C->Args) + collectRecursiveSpecCallsInExpr(A.get(), Fn, ArgMaps); + return; + } + if (E->K == VExpr::BinOp) { + const auto *B = static_cast(E); + collectRecursiveSpecCallsInExpr(B->Lhs.get(), Fn, ArgMaps); + collectRecursiveSpecCallsInExpr(B->Rhs.get(), Fn, ArgMaps); + } else if (E->K == VExpr::UnaryOp) { + collectRecursiveSpecCallsInExpr( + static_cast(E)->Operand.get(), Fn, ArgMaps); + } else if (E->K == VExpr::Conditional) { + const auto *C = static_cast(E); + collectRecursiveSpecCallsInExpr(C->Cond.get(), Fn, ArgMaps); + collectRecursiveSpecCallsInExpr(C->Then.get(), Fn, ArgMaps); + collectRecursiveSpecCallsInExpr(C->Else.get(), Fn, ArgMaps); + } +} + +static void collectRecursiveSpecCallsInBody( + const std::vector> &Stmts, const VFunction &Fn, + std::vector>> &ArgMaps) { + for (const auto &S : Stmts) { + if (S->K == VStmt::Return) + collectRecursiveSpecCallsInExpr( + static_cast(*S).Value.get(), Fn, ArgMaps); + if (S->K == VStmt::Assign) + collectRecursiveSpecCallsInExpr( + static_cast(*S).Value.get(), Fn, ArgMaps); + if (S->K == VStmt::If) { + const auto &I = static_cast(*S); + collectRecursiveSpecCallsInBody(I.Then, Fn, ArgMaps); + collectRecursiveSpecCallsInBody(I.Else, Fn, ArgMaps); + } + if (S->K == VStmt::GhostBlock) + collectRecursiveSpecCallsInBody( + static_cast(*S).Body, Fn, ArgMaps); + } +} + +PassiveProgram verify::buildDecreasesChecks(const VFunction &Fn, + const FunctionMap &FnMap) { + PassiveProgram P; + if (!Fn.Decreases) + return P; + + std::vector>>> + Sites; + std::map> Env; + for (const auto &P : Fn.Params) + Env[P.first] = std::make_unique(P.first, P.second, SourceLocation()); + collectRecursiveCalls(Fn.Body, Fn.Name, FnMap, Sites, Env); + + std::vector>> SpecArgMaps; + collectRecursiveSpecCallsInBody(Fn.Body, Fn, SpecArgMaps); + for (auto &Args : SpecArgMaps) + Sites.emplace_back(nullptr, std::move(Args)); + + std::map> EntryEnv; + for (const auto &P : Fn.Params) + EntryEnv[P.first] = std::make_unique(P.first, P.second, SourceLocation()); + auto CurrentDec = substParamsInExpr(Fn.Decreases.get(), EntryEnv); + + for (const auto &[Call, ArgMap] : Sites) { + auto CalleeDec = substParamsInExpr(Fn.Decreases.get(), ArgMap); + if (!CalleeDec || !CurrentDec) + continue; + SourceLocation Loc = Call ? Call->Loc : Fn.Decreases->Loc; + auto PS = std::make_unique(); + PS->K = PassiveStmt::Assert; + PS->Cond = std::make_unique(VBinOp::Lt, std::move(CalleeDec), + cloneVExpr(CurrentDec.get()), + VType::makeBool(), Loc); + P.Stmts.push_back(std::move(PS)); + } + return P; +} \ No newline at end of file diff --git a/clang/lib/Verify/Transform/SpecInline.h b/clang/lib/Verify/Transform/SpecInline.h new file mode 100644 index 0000000000..dcab456079 --- /dev/null +++ b/clang/lib/Verify/Transform/SpecInline.h @@ -0,0 +1,48 @@ +//===--- SpecInline.h - Inline spec calls with fuel -----------------------===// +#ifndef LLVM_CLANG_VERIFY_TRANSFORM_SPECINLINE_H +#define LLVM_CLANG_VERIFY_TRANSFORM_SPECINLINE_H + +#include "../IR/VStmt.h" +#include "Passivize.h" + +namespace clang { +namespace verify { + +class SpecInliner { + const FunctionMap &FnMap; + std::map Fuel; + +public: + SpecInliner(const FunctionMap &FnMap, std::map Fuel) + : FnMap(FnMap), Fuel(std::move(Fuel)) {} + + void prepareFunction(VFunction &Fn); + /// Keep VSpecCallExpr for Z3 spec-function applications (no definition inlining). + void prepareFunctionAxiomatic(VFunction &Fn); + std::unique_ptr inlineExpr(std::unique_ptr E); + + /// Unfold spec body for defining axiom (fuel-limited symbolic expansion). + std::unique_ptr unfoldDefinition(const VFunction &Spec, + const std::map &Fuel, + const std::set &Hidden, + const std::set &Revealed, + unsigned RootFuel) const; +}; + +/// Build passive obligations: decreases(callee) < decreases(current) at recursive sites. +PassiveProgram buildDecreasesChecks(const VFunction &Fn, const FunctionMap &FnMap); + +bool functionHasRecursiveSpecCall(const VFunction &Fn, const FunctionMap &FnMap); + +void collectSpecCalls(const VExpr *E, std::vector &Out); +void collectSpecCallsInFunction(const VFunction &Fn, + std::vector &Out); + +std::unique_ptr +substParamsInExpr(const VExpr *E, + const std::map> &Map); + +} // namespace verify +} // namespace clang + +#endif \ No newline at end of file diff --git a/clang/test/Verify/dump_ir.cpp b/clang/test/Verify/dump_ir.cpp index 0bed2f1f82..665083d521 100644 --- a/clang/test/Verify/dump_ir.cpp +++ b/clang/test/Verify/dump_ir.cpp @@ -4,7 +4,7 @@ // RUN: %cpp-verify --dump-ir %s 2>&1 | FileCheck %s --check-prefix=ALL int abs(int x) - pre(true) + pre(x != (-2147483647 - 1)) post(result >= 0) { return x < 0 ? -x : x; diff --git a/clang/test/Verify/suite/bmc_backend.cpp b/clang/test/Verify/suite/bmc_backend.cpp new file mode 100644 index 0000000000..2eec9c68a3 --- /dev/null +++ b/clang/test/Verify/suite/bmc_backend.cpp @@ -0,0 +1,20 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify --backend=bmc --unroll=3 %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +// BMC path: loop unroll + Z3. +int sum_small(int n) + pre(n >= 0 && n <= 2) + post(result >= 0) +{ + int s = 0; + int i = 0; + while (i < n) + invariant(s >= 0) + { + s = s + 1; + i = i + 1; + } + return s; +} + +// VERIFY: Verified: sum_small \ No newline at end of file diff --git a/clang/test/Verify/suite/bmc_loop_sum.cpp b/clang/test/Verify/suite/bmc_loop_sum.cpp new file mode 100644 index 0000000000..41772a6005 --- /dev/null +++ b/clang/test/Verify/suite/bmc_loop_sum.cpp @@ -0,0 +1,20 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify --backend=bmc --unroll=3 %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int sum_first_n(int n) + pre(n >= 0 && n <= 3) + post(result >= 0) +{ + int s = 0; + int i = 0; + while (i < n) + invariant(s >= 0) + invariant(i >= 0) + { + s = s + i; + i = i + 1; + } + return s; +} + +// VERIFY: Verified: sum_first_n \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_aliases_pair.cpp b/clang/test/Verify/suite/cov_aliases_pair.cpp new file mode 100644 index 0000000000..7f9a85b71b --- /dev/null +++ b/clang/test/Verify/suite/cov_aliases_pair.cpp @@ -0,0 +1,13 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +void copy(int *dst, int *src, int n) + pre(n >= 0 && n <= 1) + aliases(dst, src) + modifies(*dst) + post(*dst == old(*src)) +{ + if (n > 0) + *dst = *src; +} + +// VERIFY: Verified: copy \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_ast_rich.cpp b/clang/test/Verify/suite/cov_ast_rich.cpp new file mode 100644 index 0000000000..1ad8cdddd8 --- /dev/null +++ b/clang/test/Verify/suite/cov_ast_rich.cpp @@ -0,0 +1,28 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +struct Pair { + int a; + int b; +}; + +int inc(int x) + pre(x >= 0 && x < 50) + post(result == x + 1) +{ + return x + 1; +} + +int rich(int n, int *p) + pre(n >= 0 && n <= 2) + modifies(*p) + post(result >= 0) +{ + Pair pr; + pr.a = 0; + pr.b = 1; + int t = inc(n); + *p = 7; + return pr.a + pr.b + t; +} + +// VERIFY: Verified: rich \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_bmc_body_stmts.cpp b/clang/test/Verify/suite/cov_bmc_body_stmts.cpp new file mode 100644 index 0000000000..61fcb3f7a4 --- /dev/null +++ b/clang/test/Verify/suite/cov_bmc_body_stmts.cpp @@ -0,0 +1,27 @@ +// RUN: %cpp-verify --backend=bmc --unroll=2 %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int bump(int x) { return x + 1; } + +int loop_mix(int n, int *p) + pre(n >= 0 && n <= 1) + modifies(*p) + post(result >= 0) +{ + int i = 0; + int s = 0; + while (i < n) + invariant(s >= 0) + { + ghost { reveal(bump); } + contract_assert(i >= 0); + if (i == 0) + s = bump(s); + else + s = s + 0; + *p = s; + i = i + 1; + } + return s; +} + +// VERIFY: Verified: loop_mix \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_bmc_for_loop.cpp b/clang/test/Verify/suite/cov_bmc_for_loop.cpp new file mode 100644 index 0000000000..4c8070f11c --- /dev/null +++ b/clang/test/Verify/suite/cov_bmc_for_loop.cpp @@ -0,0 +1,18 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify --backend=bmc --unroll=2 %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int sum_for(int n) + pre(n >= 0 && n <= 2) + post(result >= 0) +{ + int s = 0; + for (int i = 0; i < n; ++i) + invariant(s >= 0) + invariant(i >= 0) + { + s = s + 1; + } + return s; +} + +// VERIFY: Verified: sum_for \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_chained_assign.cpp b/clang/test/Verify/suite/cov_chained_assign.cpp new file mode 100644 index 0000000000..0613de2e18 --- /dev/null +++ b/clang/test/Verify/suite/cov_chained_assign.cpp @@ -0,0 +1,20 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int step(int x) + pre(x >= 0 && x < 100) + post(result == x + 1) +{ + return x + 1; +} + +int two_steps(int x) + pre(x >= 0 && x < 98) + post(result == x + 2) +{ + int t = step(step(x)); + return t; +} + +// VERIFY-DAG: Verified: step +// VERIFY-DAG: Verified: two_steps \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_constexpr_spec.cpp b/clang/test/Verify/suite/cov_constexpr_spec.cpp new file mode 100644 index 0000000000..99e3b0c255 --- /dev/null +++ b/clang/test/Verify/suite/cov_constexpr_spec.cpp @@ -0,0 +1,12 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +constexpr int twice(int x) { return 2 * x; } + +int use_constexpr(int x) + pre(x >= 0 && x < 50) + post(result == twice(x)) +{ + return twice(x); +} + +// VERIFY: Verified: use_constexpr \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_contracts_spec_ref.cpp b/clang/test/Verify/suite/cov_contracts_spec_ref.cpp new file mode 100644 index 0000000000..6dafe05e51 --- /dev/null +++ b/clang/test/Verify/suite/cov_contracts_spec_ref.cpp @@ -0,0 +1,12 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int s(int x) { return x + 1; } + +int client(int x) + pre(x < 0 || s(x) > 0) + post(result == s(x)) +{ + return s(x); +} + +// VERIFY: Verified: client \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_dump_full.cpp b/clang/test/Verify/suite/cov_dump_full.cpp new file mode 100644 index 0000000000..9f876f69a6 --- /dev/null +++ b/clang/test/Verify/suite/cov_dump_full.cpp @@ -0,0 +1,28 @@ +// RUN: %cpp-verify --dump-ir=all %s 2>&1 | FileCheck %s --check-prefix=DUMP +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int len_spec(int n) { return n; } + +int run(int *p, int n) + pre(n >= 0 && n <= 2) + modifies(*p) + post(result == len_spec(n)) +{ + ghost { reveal(len_spec); } + contract_assert(n >= 0); + int r = 0; + if (n > 0) + r = *p; + else + r = 0; + *p = r; + return n; +} + +// DUMP: fn run +// DUMP: ghost +// DUMP: contract_assert +// DUMP: spec_call +// DUMP: passive run +// DUMP: vc run +// VERIFY: Verified: run \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_dump_rich.cpp b/clang/test/Verify/suite/cov_dump_rich.cpp new file mode 100644 index 0000000000..5a1380ee6c --- /dev/null +++ b/clang/test/Verify/suite/cov_dump_rich.cpp @@ -0,0 +1,30 @@ +// RUN: %cpp-verify --dump-ir=3,4 %s 2>&1 | FileCheck %s --check-prefix=DUMP +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +struct Pair { + int a; + int b; +}; + +int swap_post(int *x, int *y) + pre(x != y) + modifies(*x, *y) + post(old(*x) == *y && old(*y) == *x) +{ + int t = *x; + *x = *y; + *y = t; + return 0; +} + +int check_pair(Pair p) + pre(p.a >= 0 && p.b >= 0 && forall(i, 0, 1, i >= 0)) + post(result == p.a + p.b) +{ + return p.a + p.b; +} + +// DUMP: vc swap_post +// DUMP: forall +// VERIFY-DAG: Verified: swap_post +// VERIFY-DAG: Verified: check_pair \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_exists.cpp b/clang/test/Verify/suite/cov_exists.cpp new file mode 100644 index 0000000000..aebb45a73d --- /dev/null +++ b/clang/test/Verify/suite/cov_exists.cpp @@ -0,0 +1,11 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int bounded(int n) + pre(n > 0 && n <= 4) + pre(exists(i, 0, n, i >= 0 && i < n)) + post(result >= 0) +{ + return n - 1; +} + +// VERIFY: Verified: bounded \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_field_expr.cpp b/clang/test/Verify/suite/cov_field_expr.cpp new file mode 100644 index 0000000000..d9139ab277 --- /dev/null +++ b/clang/test/Verify/suite/cov_field_expr.cpp @@ -0,0 +1,15 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +struct Point { + int x; + int y; +}; + +int sum_point(Point p) + pre(p.x >= 0 && p.y >= 0 && p.x <= 10 && p.y <= 10) + post(result == p.x + p.y) +{ + return p.x + p.y; +} + +// VERIFY: Verified: sum_point \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_for_loop.cpp b/clang/test/Verify/suite/cov_for_loop.cpp new file mode 100644 index 0000000000..01df38fcda --- /dev/null +++ b/clang/test/Verify/suite/cov_for_loop.cpp @@ -0,0 +1,18 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int sum_for(int n) + pre(n >= 0 && n <= 3) + post(result >= 0) +{ + int s = 0; + int i = 0; + for (; i < n;) + invariant(s >= 0 && i >= 0) + { + s = s + 1; + i = i + 1; + } + return s; +} + +// VERIFY: Verified: sum_for \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_heap_loop_incr.cpp b/clang/test/Verify/suite/cov_heap_loop_incr.cpp new file mode 100644 index 0000000000..812baf76f4 --- /dev/null +++ b/clang/test/Verify/suite/cov_heap_loop_incr.cpp @@ -0,0 +1,18 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int loop_incr(int n, int *p) + pre(n >= 0 && n <= 2) + modifies(*p) + post(result >= 0) +{ + int i = 0; + while (i < n) + invariant(i >= 0) + { + *p = *p + 1; + i = i + 1; + } + return i; +} + +// VERIFY: Verified: loop_incr \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_if_else_calls.cpp b/clang/test/Verify/suite/cov_if_else_calls.cpp new file mode 100644 index 0000000000..d950788839 --- /dev/null +++ b/clang/test/Verify/suite/cov_if_else_calls.cpp @@ -0,0 +1,20 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int inc(int x) + pre(x >= 0 && x < 100) + post(result == x + 1) +{ + return x + 1; +} + +int bump(int x) + pre(x >= 0 && x < 99) + post(result >= x) +{ + if (x < 50) + return inc(x); + return inc(inc(x)); +} + +// VERIFY-DAG: Verified: inc +// VERIFY-DAG: Verified: bump \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_lean_heap.cpp b/clang/test/Verify/suite/cov_lean_heap.cpp new file mode 100644 index 0000000000..80ed9dc30d --- /dev/null +++ b/clang/test/Verify/suite/cov_lean_heap.cpp @@ -0,0 +1,15 @@ +// RUN: %cpp-verify --backend=lean --lean-out=%t.lean %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int swap_val(int *a, int *b) + pre(a != b) + modifies(*a, *b) + post(*a == old(*b) && *b == old(*a)) +{ + int t = *a; + *a = *b; + *b = t; + return 0; +} + +// VERIFY: Verified: swap_val +// VERIFY: theorem cppverify_goal \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_lean_quant.cpp b/clang/test/Verify/suite/cov_lean_quant.cpp new file mode 100644 index 0000000000..088a5cfa68 --- /dev/null +++ b/clang/test/Verify/suite/cov_lean_quant.cpp @@ -0,0 +1,17 @@ +// RUN: %cpp-verify --backend=lean --lean-out=%t.lean %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int quant_client(int n) + pre(n > 0 && n <= 3) + pre(forall(i, 0, n, i >= 0)) + pre(exists(j, 0, n, j == 0)) + post(result == n) +{ + int x = 0; + if (n > 1) + x = 1; + else + x = 0; + return n + x - x; +} + +// VERIFY: lean export: quant_client \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_loop_nested_bmc.cpp b/clang/test/Verify/suite/cov_loop_nested_bmc.cpp new file mode 100644 index 0000000000..a1fd4a284d --- /dev/null +++ b/clang/test/Verify/suite/cov_loop_nested_bmc.cpp @@ -0,0 +1,24 @@ +// RUN: %cpp-verify --backend=bmc --unroll=2 %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int nested_sum(int n) + pre(n >= 0 && n <= 1) + post(result >= 0) +{ + int s = 0; + int i = 0; + while (i < n) + invariant(s >= 0) + { + int j = 0; + while (j < 1) + invariant(j >= 0) + { + s = s + 1; + j = j + 1; + } + i = i + 1; + } + return s; +} + +// VERIFY: Verified: nested_sum \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_loop_unroll_zero.cpp b/clang/test/Verify/suite/cov_loop_unroll_zero.cpp new file mode 100644 index 0000000000..309d4875fa --- /dev/null +++ b/clang/test/Verify/suite/cov_loop_unroll_zero.cpp @@ -0,0 +1,16 @@ +// RUN: %cpp-verify --backend=bmc --unroll=0 %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int one_step(int n) + pre(n == 0 || n == 1) + post(result >= 0) +{ + int i = 0; + while (i < n) + invariant(i >= 0) + { + i = i + 1; + } + return i; +} + +// VERIFY: Verified: one_step \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_mega_sweep.cpp b/clang/test/Verify/suite/cov_mega_sweep.cpp new file mode 100644 index 0000000000..ee8bbd2370 --- /dev/null +++ b/clang/test/Verify/suite/cov_mega_sweep.cpp @@ -0,0 +1,55 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY +// RUN: %cpp-verify --backend=bmc --unroll=2 %s 2>&1 | FileCheck %s --check-prefix=VERIFY +// RUN: %cpp-verify --backend=lean --lean-out=%t.lean %s 2>&1 | FileCheck %s --check-prefix=LEAN + +spec int inc(int x) { return x + 1; } + +spec int pick(int x) +{ + if (x < 0) + return 0; + return x; +} + +spec int rec(int n) + decreases(n) +{ + if (n <= 0) + return 0; + return rec(n - 1) + 1; +} + +int exec_client(int x) + pre(x >= 0 && x < 20) + post(result == inc(inc(x))) + recommends(pick(x) >= 0) +{ + ghost { reveal(inc); contract_assert(x >= 0); } + return inc(inc(x)); +} + +int loop_client(int n, int *p) + pre(n >= 0 && n <= 1) + pre(forall(i, 0, n, i >= 0)) + modifies(*p) + post(result >= 0) + decreases(n) +{ + int i = 0; + int s = 0; + while (i < n) + invariant(s >= 0) + decreases(n - i) + { + if (i == 0) + s = inc(s); + *p = s; + i = i + 1; + } + return s; +} + +// VERIFY-DAG: Verified: exec_client +// VERIFY-DAG: Verified: loop_client + +// LEAN: lean export: exec_client \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_multi_spec_z3.cpp b/clang/test/Verify/suite/cov_multi_spec_z3.cpp new file mode 100644 index 0000000000..757ad4196e --- /dev/null +++ b/clang/test/Verify/suite/cov_multi_spec_z3.cpp @@ -0,0 +1,15 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int inc_s(int x) { return x + 1; } +spec int add_s(int x, int y) { return x + y; } + +int chain(int x) + pre(x >= 0 && x < 100) + post(result == add_s(inc_s(x), x)) +{ + return add_s(inc_s(x), x); +} + +// VERIFY-DAG: spec axiom: inc_s +// VERIFY-DAG: spec axiom: add_s +// VERIFY-DAG: Verified: chain \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_proof_decreases.cpp b/clang/test/Verify/suite/cov_proof_decreases.cpp new file mode 100644 index 0000000000..591bda7662 --- /dev/null +++ b/clang/test/Verify/suite/cov_proof_decreases.cpp @@ -0,0 +1,29 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int id_spec(int n) { return n; } + +proof void lemma_id(int n) + pre(n >= 0 && n <= 10) + post(id_spec(n) == n) + decreases(n) +{ + ghost { reveal(id_spec); } +} + +int walk(int n) + pre(n >= 0 && n <= 3) + post(result >= 0) + decreases(n) +{ + int i = 0; + while (i < n) + invariant(i >= 0) + decreases(n - i) + { + i = i + 1; + } + return i; +} + +// VERIFY-DAG: Verified: lemma_id +// VERIFY-DAG: Verified: walk \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_recommends_fail.cpp b/clang/test/Verify/suite/cov_recommends_fail.cpp new file mode 100644 index 0000000000..eabf2eadf2 --- /dev/null +++ b/clang/test/Verify/suite/cov_recommends_fail.cpp @@ -0,0 +1,16 @@ +// RUN: not %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=CHECK + +spec int need_pos(int x) + recommends(x > 0) +{ + return x; +} + +int caller(int x) + pre(x == 0) + post(result > 0) +{ + return need_pos(x); +} + +// CHECK: verification failed: caller \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_spec_advanced.cpp b/clang/test/Verify/suite/cov_spec_advanced.cpp new file mode 100644 index 0000000000..0bea58cc96 --- /dev/null +++ b/clang/test/Verify/suite/cov_spec_advanced.cpp @@ -0,0 +1,36 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int branch(int x) +{ + if (x < 0) + return 0; + return x; +} + +spec int rec(int n) + decreases(n) +{ + if (n <= 0) + return 0; + return rec(n - 1) + 1; +} + +spec int hidden_body(int x) { return x + 1; } + +int use_branch(int x) + pre(x >= -2 && x <= 2) + post(result == branch(x)) +{ + return branch(x); +} + +int use_rec(int n) + pre(n >= 0 && n <= 2) + post(result == rec(n)) + decreases(n) +{ + return rec(n); +} + +// VERIFY-DAG: Verified: use_branch +// VERIFY-DAG: Verified: use_rec \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_spec_bmc_inline.cpp b/clang/test/Verify/suite/cov_spec_bmc_inline.cpp new file mode 100644 index 0000000000..e1090f2d02 --- /dev/null +++ b/clang/test/Verify/suite/cov_spec_bmc_inline.cpp @@ -0,0 +1,13 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify --backend=bmc --unroll=2 %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int inc_spec(int x) { return x + 1; } + +int use_spec(int x) + pre(x >= 0 && x < 20) + post(result == inc_spec(x)) +{ + return inc_spec(x); +} + +// VERIFY: Verified: use_spec \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_spec_decreases.cpp b/clang/test/Verify/suite/cov_spec_decreases.cpp new file mode 100644 index 0000000000..d9466e2de6 --- /dev/null +++ b/clang/test/Verify/suite/cov_spec_decreases.cpp @@ -0,0 +1,11 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int dec(int n) + decreases(n) +{ + if (n <= 0) + return 0; + return dec(n - 1) + 1; +} + +// VERIFY: spec decreases: dec \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_spec_fuel_exec.cpp b/clang/test/Verify/suite/cov_spec_fuel_exec.cpp new file mode 100644 index 0000000000..e9881de576 --- /dev/null +++ b/clang/test/Verify/suite/cov_spec_fuel_exec.cpp @@ -0,0 +1,15 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int double_spec(int x) { return 2 * x; } + +int use_with_reveal(int x) + pre(x >= 0 && x <= 20) + post(result == double_spec(x)) +{ + ghost { reveal_with_fuel(double_spec, 1); } + return double_spec(x); +} + +// VERIFY-DAG: spec axiom: double_spec +// VERIFY-DAG: Verified: use_with_reveal \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_spec_lean_inline.cpp b/clang/test/Verify/suite/cov_spec_lean_inline.cpp new file mode 100644 index 0000000000..5d146b0942 --- /dev/null +++ b/clang/test/Verify/suite/cov_spec_lean_inline.cpp @@ -0,0 +1,25 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify --backend=lean --lean-out=%t.lean %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int triple(int x) { return 3 * x; } + +spec int pick(int x) +{ + if (x < 0) + return 0; + return x; +} + +int client(int x) + pre(x >= 0 && x <= 10) + post(result == triple(x)) + recommends(pick(x) >= 0) +{ + ghost { reveal(triple); hide(pick); } + int mid = triple(x); + if (x < 5) + return mid; + return mid; +} + +// VERIFY: lean export: client \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_spec_opaque.cpp b/clang/test/Verify/suite/cov_spec_opaque.cpp new file mode 100644 index 0000000000..986cdcbdd8 --- /dev/null +++ b/clang/test/Verify/suite/cov_spec_opaque.cpp @@ -0,0 +1,30 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int hidden(int x) { return x + 1; } + +int client(int x) + pre(x >= 0 && x < 10) + post(result == x) +{ + ghost { hide(hidden); } + return x; +} + +spec int rec(int n) + decreases(n) +{ + if (n <= 0) + return 0; + return rec(n - 1) + 1; +} + +int use_rec(int n) + pre(n >= 0 && n <= 1) + post(result == rec(n)) + decreases(n) +{ + return rec(n); +} + +// VERIFY-DAG: Verified: client +// VERIFY-DAG: Verified: use_rec \ No newline at end of file diff --git a/clang/test/Verify/suite/cov_spec_post_opaque.cpp b/clang/test/Verify/suite/cov_spec_post_opaque.cpp new file mode 100644 index 0000000000..97c58fcca1 --- /dev/null +++ b/clang/test/Verify/suite/cov_spec_post_opaque.cpp @@ -0,0 +1,13 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int hidden(int x) { return x + 1; } + +int client(int x) + pre(hidden(x) >= 0 && x >= 0 && x < 10) + post(result >= 0) +{ + ghost { hide(hidden); } + return x; +} + +// VERIFY: Verified: client \ No newline at end of file diff --git a/clang/test/Verify/suite/dump_ir_layers.cpp b/clang/test/Verify/suite/dump_ir_layers.cpp new file mode 100644 index 0000000000..3e5b4a3949 --- /dev/null +++ b/clang/test/Verify/suite/dump_ir_layers.cpp @@ -0,0 +1,17 @@ +// RUN: %cpp-verify --dump-ir=1 %s 2>&1 | FileCheck %s --check-prefix=L1 +// RUN: %cpp-verify --dump-ir=2 %s 2>&1 | FileCheck %s --check-prefix=L2 +// RUN: %cpp-verify --dump-ir=3,4 %s 2>&1 | FileCheck %s --check-prefix=L34 + +int inc(int x) + pre(x >= 0 && x < 100) + post(result == x + 1) +{ + return x + 1; +} + +// L1: fn inc +// L1-NOT: passive inc +// L2: passive inc +// L2-NOT: {{^}}fn inc +// L34: vc inc +// L34: Verified: \ No newline at end of file diff --git a/clang/test/Verify/suite/lean_backend.cpp b/clang/test/Verify/suite/lean_backend.cpp new file mode 100644 index 0000000000..415bd2b4fd --- /dev/null +++ b/clang/test/Verify/suite/lean_backend.cpp @@ -0,0 +1,13 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify --backend=lean --lean-out=%t.lean %s 2>&1 | FileCheck %s --check-prefix=VERIFY +// RUN: grep -q 'theorem cppverify_goal' %t.lean +// RUN: grep -q 'sorry' %t.lean + +int inc(int x) + pre(x >= 0 && x < 100) + post(result == x + 1) +{ + return x + 1; +} + +// VERIFY: lean export: inc \ No newline at end of file diff --git a/clang/test/Verify/suite/spec_inline_simple.cpp b/clang/test/Verify/suite/spec_inline_simple.cpp new file mode 100644 index 0000000000..6b598d352d --- /dev/null +++ b/clang/test/Verify/suite/spec_inline_simple.cpp @@ -0,0 +1,14 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int double_spec(int x) { return 2 * x; } + +int use_double(int x) + pre(x >= 0 && x <= 100) + post(result == double_spec(x)) +{ + return double_spec(x); +} + +// VERIFY-DAG: spec axiom: double_spec +// VERIFY-DAG: Verified: use_double \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_arithmetic.cpp b/clang/test/Verify/suite/z3_arithmetic.cpp new file mode 100644 index 0000000000..167a184f70 --- /dev/null +++ b/clang/test/Verify/suite/z3_arithmetic.cpp @@ -0,0 +1,37 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int add(int a, int b) + pre(a >= 0 && b >= 0 && a <= 1000 && b <= 1000) + post(result == a + b) +{ + return a + b; +} + +int sub_nonneg(int a, int b) + pre(a >= b && b >= 0) + post(result == a - b) +{ + return a - b; +} + +int mul_small(int a, int b) + pre(a >= 0 && b >= 0 && a <= 10 && b <= 10) + post(result == a * b) +{ + return a * b; +} + +int cmp_chain(int x) + pre(x >= 0 && x <= 5) + post(result >= 0 && result <= 2) +{ + if (x < 2) return 0; + if (x < 4) return 1; + return 2; +} + +// VERIFY-DAG: Verified: add +// VERIFY-DAG: Verified: sub_nonneg +// VERIFY-DAG: Verified: mul_small +// VERIFY-DAG: Verified: cmp_chain \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_constexpr_spec.cpp b/clang/test/Verify/suite/z3_constexpr_spec.cpp new file mode 100644 index 0000000000..e49e005683 --- /dev/null +++ b/clang/test/Verify/suite/z3_constexpr_spec.cpp @@ -0,0 +1,14 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +constexpr spec int sq(int x) { return x * x; } + +int use_sq(int x) + pre(x >= 0 && x <= 100) + post(result == x * x) +{ + return sq(x); +} + +// VERIFY-DAG: constexpr spec axiom: sq +// VERIFY-DAG: Verified: use_sq \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_control_flow.cpp b/clang/test/Verify/suite/z3_control_flow.cpp new file mode 100644 index 0000000000..7cf7ae591c --- /dev/null +++ b/clang/test/Verify/suite/z3_control_flow.cpp @@ -0,0 +1,40 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int max2(int a, int b) + pre(a >= -1000 && b >= -1000 && a <= 1000 && b <= 1000) + post(result >= a && result >= b) +{ + return a >= b ? a : b; +} + +int abs_safe(int x) + pre(x >= -1000 && x <= 1000) + post(result >= 0) +{ + return x < 0 ? -x : x; +} + +int sum_to_n(int n) + pre(n >= 0 && n <= 20) + post(result >= 0) +{ + int s = 0; + for (int i = 0; i < n; ++i) + s = s + 1; + return s; +} + +int while_countdown(int n) + pre(n >= 0 && n <= 10) + post(result == 0) +{ + while (n > 0) + n = n - 1; + return n; +} + +// VERIFY-DAG: Verified: max2 +// VERIFY-DAG: Verified: abs_safe +// VERIFY-DAG: Verified: sum_to_n +// VERIFY-DAG: Verified: while_countdown \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_exec_call.cpp b/clang/test/Verify/suite/z3_exec_call.cpp new file mode 100644 index 0000000000..dfe26a74ae --- /dev/null +++ b/clang/test/Verify/suite/z3_exec_call.cpp @@ -0,0 +1,18 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int inc(int x) + pre(x >= 0 && x < 1000) + post(result == x + 1) +{ + return x + 1; +} + +int use_inc(int x) + pre(x >= 0 && x < 999) + post(result == x + 1) +{ + return inc(x); +} + +// VERIFY-DAG: Verified: inc +// VERIFY-DAG: Verified: use_inc \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_framing_fail.cpp b/clang/test/Verify/suite/z3_framing_fail.cpp new file mode 100644 index 0000000000..7226914997 --- /dev/null +++ b/clang/test/Verify/suite/z3_framing_fail.cpp @@ -0,0 +1,12 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: not %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=FAIL + +void bad_framing(int *a, int *b) + pre(a != nullptr && b != nullptr) + modifies(*b) + post(*a == old(*a)) +{ + *a = 42; +} + +// FAIL: verification failed: bad_framing \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_ghost_contract_assert.cpp b/clang/test/Verify/suite/z3_ghost_contract_assert.cpp new file mode 100644 index 0000000000..328891a8df --- /dev/null +++ b/clang/test/Verify/suite/z3_ghost_contract_assert.cpp @@ -0,0 +1,11 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int guarded(int x) + pre(x != (-2147483647 - 1)) + post(result >= 0) +{ + ghost { contract_assert(x != (-2147483647 - 1)); } + return x < 0 ? -x : x; +} + +// VERIFY: Verified: guarded \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_heap_swap.cpp b/clang/test/Verify/suite/z3_heap_swap.cpp new file mode 100644 index 0000000000..ca0313e6c8 --- /dev/null +++ b/clang/test/Verify/suite/z3_heap_swap.cpp @@ -0,0 +1,23 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +void swap_ptr(int *a, int *b) + pre(a != nullptr && b != nullptr) + modifies(*a, *b) + post(*a == old(*b) && *b == old(*a)) +{ + int tmp = *a; + *a = *b; + *b = tmp; +} + +void write_ptr(int *p, int v) + pre(p != nullptr) + modifies(*p) + post(*p == v) +{ + *p = v; +} + +// VERIFY-DAG: Verified: swap_ptr +// VERIFY-DAG: Verified: write_ptr \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_heap_write_only.cpp b/clang/test/Verify/suite/z3_heap_write_only.cpp new file mode 100644 index 0000000000..de39764b64 --- /dev/null +++ b/clang/test/Verify/suite/z3_heap_write_only.cpp @@ -0,0 +1,11 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +void write_ptr(int *p, int v) + pre(p != nullptr) + modifies(*p) + post(*p == v) +{ + *p = v; +} + +// VERIFY: Verified: write_ptr \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_hide_reveal_fuel.cpp b/clang/test/Verify/suite/z3_hide_reveal_fuel.cpp new file mode 100644 index 0000000000..1cec99e2ce --- /dev/null +++ b/clang/test/Verify/suite/z3_hide_reveal_fuel.cpp @@ -0,0 +1,48 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int triple(int x) { return 3 * x; } + +proof void lemma_triple(int x) + pre(x >= 0 && x <= 50) + post(triple(x) == 3 * x) +{ + ghost { reveal(triple); } +} + +int client_reveal(int x) + pre(x >= 0 && x <= 10) + post(result == triple(x)) +{ + ghost { reveal(triple); } + return x + x + x; +} + +int client_hide(int x) + pre(x >= 0 && x <= 10) + post(result == x + x + x) +{ + ghost { hide(triple); } + return x + x + x; +} + +spec int fact(int n) + decreases(n) +{ + if (n <= 1) return 1; + return n * fact(n - 1); +} + +proof void lemma_fact_base(int n) + pre(n == 0) + post(fact(n) == 1) +{ + ghost { reveal_with_fuel(fact, 2); } +} + +// VERIFY-DAG: spec axiom: triple +// VERIFY-DAG: Verified: lemma_triple +// VERIFY-DAG: Verified: client_reveal +// VERIFY-DAG: Verified: client_hide +// VERIFY-DAG: spec decreases: fact +// VERIFY-DAG: Verified: lemma_fact_base \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_loop_invariant.cpp b/clang/test/Verify/suite/z3_loop_invariant.cpp new file mode 100644 index 0000000000..3143dcf0a3 --- /dev/null +++ b/clang/test/Verify/suite/z3_loop_invariant.cpp @@ -0,0 +1,20 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int sum_loop(int n) + pre(n >= 0 && n <= 15) + post(result >= 0) +{ + int s = 0; + int i = 0; + while (i < n) + invariant(i >= 0 && i <= n && s >= 0) + decreases(n - i) + { + s = s + 1; + i = i + 1; + } + return s; +} + +// VERIFY: Verified: sum_loop \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_modular_call.cpp b/clang/test/Verify/suite/z3_modular_call.cpp new file mode 100644 index 0000000000..2c5cf57e3e --- /dev/null +++ b/clang/test/Verify/suite/z3_modular_call.cpp @@ -0,0 +1,20 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int abs_val(int x) + pre(x != (-2147483647 - 1)) + post(result >= 0) +{ + return x < 0 ? -x : x; +} + +int use_abs(int x) + pre(x != (-2147483647 - 1)) + post(result >= 0) +{ + int y = abs_val(x); + return y; +} + +// VERIFY-DAG: Verified: abs_val +// VERIFY-DAG: Verified: use_abs \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_modular_chained.cpp b/clang/test/Verify/suite/z3_modular_chained.cpp new file mode 100644 index 0000000000..11db9a593d --- /dev/null +++ b/clang/test/Verify/suite/z3_modular_chained.cpp @@ -0,0 +1,19 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int inc(int x) + pre(x >= 0 && x < 100) + post(result == x + 1) +{ + return x + 1; +} + +int inc_twice(int x) + pre(x >= 0 && x < 98) + post(result == x + 2) +{ + return inc(inc(x)); +} + +// VERIFY-DAG: Verified: inc +// VERIFY-DAG: Verified: inc_twice \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_old_result.cpp b/clang/test/Verify/suite/z3_old_result.cpp new file mode 100644 index 0000000000..7018cf2632 --- /dev/null +++ b/clang/test/Verify/suite/z3_old_result.cpp @@ -0,0 +1,19 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int inc(int x) + pre(x >= 0 && x < 1000) + post(result == old(x) + 1) +{ + return x + 1; +} + +int id(int x) + pre(true) + post(result == old(x)) +{ + return x; +} + +// VERIFY-DAG: Verified: inc +// VERIFY-DAG: Verified: id \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_quantifier_pre.cpp b/clang/test/Verify/suite/z3_quantifier_pre.cpp new file mode 100644 index 0000000000..d60c1cb2f5 --- /dev/null +++ b/clang/test/Verify/suite/z3_quantifier_pre.cpp @@ -0,0 +1,12 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int pick_first(int n) + pre(n > 0 && n <= 5) + pre(forall(i, 0, n, i >= 0)) + post(result >= 0) +{ + return 0; +} + +// VERIFY: Verified: pick_first \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_recommends_warning.cpp b/clang/test/Verify/suite/z3_recommends_warning.cpp new file mode 100644 index 0000000000..56799f0811 --- /dev/null +++ b/clang/test/Verify/suite/z3_recommends_warning.cpp @@ -0,0 +1,17 @@ +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=FAIL + +spec int id_spec(int a) + recommends(a >= 0) +{ + return a; +} + +int bad_call(int a) + pre(true) + post(result == a) +{ + return id_spec(-1); +} + +// FAIL: verification failed: bad_call +// FAIL: recommends \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_spec_proof_axioms.cpp b/clang/test/Verify/suite/z3_spec_proof_axioms.cpp new file mode 100644 index 0000000000..59b35a4b83 --- /dev/null +++ b/clang/test/Verify/suite/z3_spec_proof_axioms.cpp @@ -0,0 +1,24 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int double_it(int x) { return 2 * x; } + +proof void lemma_double(int x) + pre(x >= 0 && x <= 1000) + post(double_it(x) == 2 * x) +{ +} + +spec int add_three(int x) { return x + 3; } + +int use_specs(int x) + pre(x >= 0 && x <= 100) + post(result == 2 * x + 3) +{ + return add_three(double_it(x)); +} + +// VERIFY-DAG: spec axiom: double_it +// VERIFY-DAG: Verified: lemma_double +// VERIFY-DAG: spec axiom: add_three +// VERIFY-DAG: Verified: use_specs \ No newline at end of file diff --git a/clang/test/Verify/suite/z3_struct_fields.cpp b/clang/test/Verify/suite/z3_struct_fields.cpp new file mode 100644 index 0000000000..06afd42a03 --- /dev/null +++ b/clang/test/Verify/suite/z3_struct_fields.cpp @@ -0,0 +1,27 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +struct Point { + int x; + int y; +}; + +Point make_origin() + post(result.x == 0) + post(result.y == 0) +{ + Point p; + p.x = 0; + p.y = 0; + return p; +} + +int point_sum(Point p) + pre(p.x >= 0 && p.y >= 0 && p.x <= 100 && p.y <= 100) + post(result == p.x + p.y) +{ + return p.x + p.y; +} + +// VERIFY-DAG: Verified: make_origin +// VERIFY-DAG: Verified: point_sum \ No newline at end of file diff --git a/clang/test/Verify/verify_abs_e2e.cpp b/clang/test/Verify/verify_abs_e2e.cpp index 9c217c62c0..f7d596718c 100644 --- a/clang/test/Verify/verify_abs_e2e.cpp +++ b/clang/test/Verify/verify_abs_e2e.cpp @@ -2,7 +2,7 @@ // RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY int abs(int x) - pre(true) + pre(x != (-2147483648)) post(result >= 0) { return x < 0 ? -x : x; diff --git a/clang/test/Verify/verify_bmc_bug.cpp b/clang/test/Verify/verify_bmc_bug.cpp new file mode 100644 index 0000000000..6dc2d1b574 --- /dev/null +++ b/clang/test/Verify/verify_bmc_bug.cpp @@ -0,0 +1,19 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: not %cpp-verify --backend=bmc --unroll=3 %s 2>&1 | FileCheck %s --check-prefix=CHECK + +int counter() + pre(true) + post(result == 0) +{ + int x = 0; + int i = 0; + while (i < 5) + invariant(true) + { + x = x + 1; + i = i + 1; + } + return x; +} + +// CHECK: verification failed: counter \ No newline at end of file diff --git a/clang/test/Verify/verify_call_e2e.cpp b/clang/test/Verify/verify_call_e2e.cpp new file mode 100644 index 0000000000..2a678aaaba --- /dev/null +++ b/clang/test/Verify/verify_call_e2e.cpp @@ -0,0 +1,20 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int abs_val(int x) + pre(x != (-2147483647 - 1)) + post(result >= 0) +{ + return x < 0 ? -x : x; +} + +int use_abs(int x) + pre(x != (-2147483647 - 1)) + post(result >= 0) +{ + int y = abs_val(x); + return y; +} + +// VERIFY: Verified: abs_val +// VERIFY: Verified: use_abs \ No newline at end of file diff --git a/clang/test/Verify/verify_constexpr_spec_e2e.cpp b/clang/test/Verify/verify_constexpr_spec_e2e.cpp new file mode 100644 index 0000000000..84b8b1fa42 --- /dev/null +++ b/clang/test/Verify/verify_constexpr_spec_e2e.cpp @@ -0,0 +1,16 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +constexpr int double_it(int x) { + return x * 2; +} + +int use_constexpr_spec(int x) + pre(x >= 0 && x <= 100) + post(result == double_it(x)) +{ + return x + x; +} + +// VERIFY: constexpr spec axiom: double_it +// VERIFY: Verified: use_constexpr_spec \ No newline at end of file diff --git a/clang/test/Verify/verify_hide_reveal_e2e.cpp b/clang/test/Verify/verify_hide_reveal_e2e.cpp new file mode 100644 index 0000000000..adab42ff5b --- /dev/null +++ b/clang/test/Verify/verify_hide_reveal_e2e.cpp @@ -0,0 +1,32 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int triple(int x) { return 3 * x; } + +proof void lemma_triple(int x) + pre(x >= 0) + post(triple(x) == 3 * x) +{ + ghost { reveal(triple); } +} + +int client_reveal(int x) + pre(x >= 0 && x <= 10) + post(result == triple(x)) +{ + ghost { reveal(triple); } + return x + x + x; +} + +int client_hide(int x) + pre(x >= 0 && x <= 10) + post(result == x + x + x) +{ + ghost { hide(triple); } + return x + x + x; +} + +// VERIFY: spec axiom: triple +// VERIFY: Verified: lemma_triple +// VERIFY: Verified: client_reveal +// VERIFY: Verified: client_hide \ No newline at end of file diff --git a/clang/test/Verify/verify_lean_export.cpp b/clang/test/Verify/verify_lean_export.cpp new file mode 100644 index 0000000000..8dba964bbb --- /dev/null +++ b/clang/test/Verify/verify_lean_export.cpp @@ -0,0 +1,13 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify --backend=lean --lean-out=%t.lean %s 2>&1 | FileCheck %s --check-prefix=VERIFY +// RUN: grep -q 'theorem cppverify_goal' %t.lean +// RUN: grep -q 'sorry' %t.lean + +int abs(int x) + pre(x != (-2147483647 - 1)) + post(result >= 0) +{ + return x < 0 ? -x : x; +} + +// VERIFY: lean export: abs \ No newline at end of file diff --git a/clang/test/Verify/verify_loop_e2e.cpp b/clang/test/Verify/verify_loop_e2e.cpp new file mode 100644 index 0000000000..83a5ad107e --- /dev/null +++ b/clang/test/Verify/verify_loop_e2e.cpp @@ -0,0 +1,20 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +int sum_first_n(int n) + pre(n >= 0 && n <= 3) + post(result >= 0) +{ + int s = 0; + int i = 0; + while (i < n) + invariant(s >= 0) + invariant(i >= 0) + { + s = s + i; + i = i + 1; + } + return s; +} + +// VERIFY: Verified: sum_first_n \ No newline at end of file diff --git a/clang/test/Verify/verify_proof_post_inline.cpp b/clang/test/Verify/verify_proof_post_inline.cpp new file mode 100644 index 0000000000..46c8920057 --- /dev/null +++ b/clang/test/Verify/verify_proof_post_inline.cpp @@ -0,0 +1,12 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int add_one(int x) { return x + 1; } + +proof void lemma_add(int x) + pre(x >= 0) + post(add_one(x) == x + 1) +{ +} + +// VERIFY: Verified: lemma_add \ No newline at end of file diff --git a/clang/test/Verify/verify_spec_proof_e2e.cpp b/clang/test/Verify/verify_spec_proof_e2e.cpp new file mode 100644 index 0000000000..20b4f349b4 --- /dev/null +++ b/clang/test/Verify/verify_spec_proof_e2e.cpp @@ -0,0 +1,45 @@ +// RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s +// RUN: %cpp-verify %s 2>&1 | FileCheck %s --check-prefix=VERIFY + +spec int factorial(int n) + decreases(n) +{ + if (n <= 1) return 1; + return n * factorial(n - 1); +} + +proof void lemma_factorial_positive(int n) + pre(n >= 1) + post(n >= 1) + decreases(n) +{ + if (n == 1) { + } else { + lemma_factorial_positive(n - 1); + } +} + +int compute_factorial(int n) + pre(n >= 0 && n <= 5) + post(result >= 1) +{ + ghost { + reveal_with_fuel(factorial, 5); + lemma_factorial_positive(n); + } + int acc = 1; + int i = 1; + while (i <= n) + invariant(acc >= 1) + invariant(i >= 1) + decreases(n - i + 1) + { + acc = acc * i; + i = i + 1; + } + return acc; +} + +// VERIFY: spec decreases: factorial +// VERIFY: Verified: lemma_factorial_positive +// VERIFY-DAG: Verified: compute_factorial \ No newline at end of file diff --git a/clang/tools/cpp-verify/CMakeLists.txt b/clang/tools/cpp-verify/CMakeLists.txt index e81019fb3b..1553bc1a56 100644 --- a/clang/tools/cpp-verify/CMakeLists.txt +++ b/clang/tools/cpp-verify/CMakeLists.txt @@ -16,4 +16,8 @@ target_link_libraries(cpp-verify clangFrontend clangTooling clangDriver - ) \ No newline at end of file + ) + +if(CPPVERIFY_ENABLE_COVERAGE) + target_link_options(cpp-verify PRIVATE -fprofile-instr-generate) +endif() \ No newline at end of file diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index cc2af181b8..f1a96dd89f 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -27,6 +27,25 @@ static cl::opt DumpIR( cl::ValueOptional, cl::cat(CppVerifyCategory)); +static cl::opt BackendOpt( + "backend", + cl::desc("Verification backend: z3 (default), lean, bmc"), + cl::value_desc("name"), + cl::init("z3"), + cl::cat(CppVerifyCategory)); + +static cl::opt LeanOut( + "lean-out", + cl::desc("Output path for --backend=lean scratch-pad export"), + cl::value_desc("file"), + cl::cat(CppVerifyCategory)); + +static cl::opt BMCUnroll( + "unroll", + cl::desc("Loop unroll bound for --backend=bmc"), + cl::init(10), + cl::cat(CppVerifyCategory)); + namespace { static int gVerifyFailures = 0; @@ -38,6 +57,15 @@ class VerifyConsumer : public ASTConsumer { verify::VerifyOptions VOpts; if (DumpIR.getNumOccurrences() > 0) VOpts.DumpIRLayers = verify::parseDumpIRLayers(DumpIR.getValue()); + llvm::StringRef B = BackendOpt.getValue(); + if (B == "lean") + VOpts.Backend = verify::BackendKind::Lean; + else if (B == "bmc") + VOpts.Backend = verify::BackendKind::BMC; + else + VOpts.Backend = verify::BackendKind::Z3; + VOpts.LeanOutPath = LeanOut.getValue(); + VOpts.BMCUnroll = BMCUnroll.getValue(); if (!verify::verifyTranslationUnit(Ctx, llvm::outs(), VOpts)) ++gVerifyFailures; } diff --git a/clang/tools/driver/CMakeLists.txt b/clang/tools/driver/CMakeLists.txt index 002aaef005..f5f4fd556e 100644 --- a/clang/tools/driver/CMakeLists.txt +++ b/clang/tools/driver/CMakeLists.txt @@ -67,6 +67,10 @@ clang_target_link_libraries(clang clangSerialization ) +if(CPPVERIFY_ENABLE_COVERAGE) + target_link_options(clang PRIVATE -fprofile-instr-generate) +endif() + if(WIN32 AND NOT CYGWIN) # Prevent versioning if the buildhost is targeting for Win32. else() diff --git a/scripts/coverage-sweep.sh b/scripts/coverage-sweep.sh new file mode 100644 index 0000000000..594539132d --- /dev/null +++ b/scripts/coverage-sweep.sh @@ -0,0 +1,57 @@ +#!/usr/bin/env bash +set -euo pipefail + +ROOT="$(cd "$(dirname "$0")/.." && pwd)" +BUILD="${CPPVERIFY_BUILD:-$ROOT/build}" +COV_DIR="$BUILD/coverage-verify" +PROFDATA="$COV_DIR/verify.profdata" +SUITE="$ROOT/clang/test/Verify/suite" +LEAN="$COV_DIR/lean.lean" + +export LLVM_PROFILE_FILE="$COV_DIR/p_%p.profraw" + +merge_profiles() { + shopt -s nullglob + local files=("$COV_DIR"/p_*.profraw "$COV_DIR"/clang_*.profraw) + shopt -u nullglob + [[ ${#files[@]} -eq 0 ]] && return 0 + if [[ -f "$PROFDATA" ]]; then + "$BUILD/bin/llvm-profdata" merge -sparse "$PROFDATA" "${files[@]}" -o "$PROFDATA.new" + mv "$PROFDATA.new" "$PROFDATA" + else + "$BUILD/bin/llvm-profdata" merge -sparse "${files[@]}" -o "$PROFDATA" + fi + rm -f "${files[@]}" +} + +n=0 +for f in "$SUITE"/*.cpp; do + "$BUILD/bin/cpp-verify" "$f" >/dev/null 2>&1 || true + "$BUILD/bin/cpp-verify" --backend=bmc --unroll=3 "$f" >/dev/null 2>&1 || true + "$BUILD/bin/cpp-verify" --backend=bmc --unroll=0 "$f" >/dev/null 2>&1 || true + "$BUILD/bin/cpp-verify" --backend=lean "--lean-out=$LEAN" "$f" >/dev/null 2>&1 || true + "$BUILD/bin/cpp-verify" --dump-ir=all "$f" >/dev/null 2>&1 || true + n=$((n + 1)) + if (( n % 12 == 0 )); then + merge_profiles + fi +done +merge_profiles + +if [[ -x "$BUILD/bin/clang" ]]; then + export LLVM_PROFILE_FILE="$COV_DIR/clang_%p.profraw" + for f in "$ROOT/clang/test/Verify/compile_with_verify.cpp" \ + "$SUITE"/cov_mega_sweep.cpp; do + [[ -f "$f" ]] || continue + "$BUILD/bin/clang" -std=c++17 -fverify-contracts -c "$f" \ + -o "$COV_DIR/$(basename "$f").o" >/dev/null 2>&1 || true + done + merge_profiles +fi + +OBJ_DIR="$BUILD/tools/clang/lib/Verify/CMakeFiles/obj.clangVerify.dir" +"$BUILD/bin/llvm-cov" report "$BUILD/bin/cpp-verify" "$BUILD/bin/clang" \ + -instr-profile="$PROFDATA" "$OBJ_DIR"/*/*.o 2>/dev/null \ + | awk '/clang\/lib\/Verify/{reg+=$2; miss+=$3} END{ + if (reg>0) printf "TOTAL Verify regions: %.2f%% (%d/%d)\n", 100*(reg-miss)/reg, reg-miss, reg; + }' \ No newline at end of file diff --git a/scripts/coverage-targeted.sh b/scripts/coverage-targeted.sh new file mode 100644 index 0000000000..d42015cf7e --- /dev/null +++ b/scripts/coverage-targeted.sh @@ -0,0 +1,92 @@ +#!/usr/bin/env bash +# Fast incremental coverage sweep (no cmake reconfigure). Merges after each batch. +set -euo pipefail + +ROOT="$(cd "$(dirname "$0")/.." && pwd)" +BUILD="${CPPVERIFY_BUILD:-$ROOT/build}" +COV_DIR="$BUILD/coverage-verify" +PROFDATA="$COV_DIR/verify.profdata" +THRESHOLD="${CPPVERIFY_COV_THRESHOLD:-90}" +SUITE="$ROOT/clang/test/Verify/suite" + +LLVM_COV="$BUILD/bin/llvm-cov" +LLVM_PROFDATA="$BUILD/bin/llvm-profdata" +mkdir -p "$COV_DIR" +export LLVM_PROFILE_FILE="$COV_DIR/tgt_%p.profraw" + +merge_profiles() { + shopt -s nullglob + local files=("$COV_DIR"/tgt_*.profraw) + shopt -u nullglob + [[ ${#files[@]} -eq 0 ]] && return 0 + if [[ -f "$PROFDATA" ]]; then + "$LLVM_PROFDATA" merge -sparse "$PROFDATA" "${files[@]}" -o "$PROFDATA.new" + mv "$PROFDATA.new" "$PROFDATA" + else + "$LLVM_PROFDATA" merge -sparse "${files[@]}" -o "$PROFDATA" + fi + rm -f "${files[@]}" +} + +run() { + "$BUILD/bin/cpp-verify" "$@" >/dev/null 2>&1 || true + merge_profiles +} + +LEAN="$COV_DIR/lean.lean" +TESTS=( + cov_mega_sweep.cpp cov_spec_advanced.cpp cov_bmc_body_stmts.cpp + cov_proof_decreases.cpp cov_dump_full.cpp cov_multi_spec_z3.cpp + cov_spec_lean_inline.cpp cov_spec_bmc_inline.cpp cov_loop_nested_bmc.cpp + cov_lean_heap.cpp cov_lean_quant.cpp cov_exists.cpp cov_constexpr_spec.cpp + cov_recommends_fail.cpp z3_modular_chained.cpp z3_hide_reveal_fuel.cpp + z3_heap_swap.cpp z3_spec_proof_axioms.cpp bmc_loop_sum.cpp spec_inline_simple.cpp + dump_ir_layers.cpp compile_with_verify.cpp +) + +for t in "${TESTS[@]}"; do + f="$SUITE/$t" + [[ -f "$f" ]] || f="$ROOT/clang/test/Verify/$t" + [[ -f "$f" ]] || continue + run "$f" + case "$t" in + *bmc*|bmc_*) run --backend=bmc --unroll=3 "$f" + run --backend=bmc --unroll=0 "$f" ;; + *lean*) run --backend=lean "--lean-out=$LEAN" "$f" ;; + *dump*) run --dump-ir=all "$f" ;; + esac +done + +if [[ -x "$BUILD/bin/clang" ]]; then + export LLVM_PROFILE_FILE="$COV_DIR/clang_%p.profraw" + for f in "$ROOT/clang/test/Verify/compile_with_verify.cpp" "$SUITE"/cov_mega_sweep.cpp; do + [[ -f "$f" ]] || continue + "$BUILD/bin/clang" -std=c++17 -fverify-contracts -c "$f" -o "$COV_DIR/$(basename "$f").o" >/dev/null 2>&1 || true + done + shopt -s nullglob + clang_files=("$COV_DIR"/clang_*.profraw) + shopt -u nullglob + if [[ ${#clang_files[@]} -gt 0 ]]; then + "$LLVM_PROFDATA" merge -sparse "$PROFDATA" "${clang_files[@]}" -o "$PROFDATA.new" + mv "$PROFDATA.new" "$PROFDATA" + rm -f "${clang_files[@]}" + fi +fi + +OBJ_DIR="$BUILD/tools/clang/lib/Verify/CMakeFiles/obj.clangVerify.dir" +OBJ_FILES=("$OBJ_DIR"/*/*.o) +REPORT="$COV_DIR/report-targeted.txt" +"$LLVM_COV" report "$BUILD/bin/cpp-verify" "$BUILD/bin/clang" \ + -instr-profile="$PROFDATA" "${OBJ_FILES[@]}" >"$REPORT" 2>/dev/null + +grep 'clang/lib/Verify' "$REPORT" | awk '{reg+=$2; miss+=$3} END { + if (reg>0) printf "TOTAL Verify regions: %.2f%% (%d/%d)\n", 100*(reg-miss)/reg, reg-miss, reg; +}' +REGIONS="$(grep 'clang/lib/Verify' "$REPORT" | awk '{reg+=$2; miss+=$3} END { + if (reg>0) printf "%.2f", 100*(reg-miss)/reg; else print "0" +}')" +echo "=== TOTAL regions: ${REGIONS}% (threshold ${THRESHOLD}%) ===" +python3 - <= float("${THRESHOLD}") else 1) +PY \ No newline at end of file diff --git a/scripts/coverage-verify.sh b/scripts/coverage-verify.sh new file mode 100644 index 0000000000..4659dcd74e --- /dev/null +++ b/scripts/coverage-verify.sh @@ -0,0 +1,158 @@ +#!/usr/bin/env bash +# Build cpp-verify with LLVM coverage instrumentation and report clangVerify line coverage. +set -euo pipefail + +ROOT="$(cd "$(dirname "$0")/.." && pwd)" +BUILD="${CPPVERIFY_BUILD:-$ROOT/build}" +COV_DIR="$BUILD/coverage-verify" +PROFDATA="$COV_DIR/verify.profdata" +PROFILE_RAW="$COV_DIR/profile-%m.profraw" +THRESHOLD="${CPPVERIFY_COV_THRESHOLD:-90}" + +REPO="$ROOT" +CMAKE="$BUILD/bin/llvm-cmake" 2>/dev/null || true +LLVM_COV="${LLVM_COV:-$(command -v llvm-cov 2>/dev/null || true)}" +LLVM_PROFDATA="${LLVM_PROFDATA:-$(command -v llvm-profdata 2>/dev/null || true)}" +if [[ -x "$BUILD/bin/llvm-cov" ]]; then + LLVM_COV="$BUILD/bin/llvm-cov" +fi +if [[ -x "$BUILD/bin/llvm-profdata" ]]; then + LLVM_PROFDATA="$BUILD/bin/llvm-profdata" +fi +if [[ -z "$LLVM_COV" || -z "$LLVM_PROFDATA" ]]; then + echo "error: need llvm-cov and llvm-profdata (build LLVM tools or install brew llvm)" >&2 + exit 1 +fi + +mkdir -p "$COV_DIR" + +echo "=== Reconfiguring with coverage flags (clangVerify + cpp-verify) ===" +cmake -S "$ROOT/llvm" -B "$BUILD" \ + -DCMAKE_BUILD_TYPE=Debug \ + -DLLVM_ENABLE_PROJECTS=clang \ + -DLLVM_TARGETS_TO_BUILD=host \ + -DCPPVERIFY_VENDOR_Z3=ON \ + -DCPPVERIFY_ENABLE_COVERAGE=ON \ + -DCMAKE_CXX_FLAGS= \ + -DCMAKE_C_FLAGS= \ + -DCMAKE_EXE_LINKER_FLAGS= \ + -DCMAKE_SHARED_LINKER_FLAGS= \ + >/dev/null + +ninja -C "$BUILD" clang clangVerify cpp-verify + +export LLVM_PROFILE_FILE="$COV_DIR/cppverify_%p.profraw" +rm -f "$COV_DIR"/*.profraw "$PROFDATA" 2>/dev/null || true + +merge_profiles() { + shopt -s nullglob + local files=("$COV_DIR"/*.profraw) + shopt -u nullglob + [[ ${#files[@]} -eq 0 ]] && return 0 + if [[ -f "$PROFDATA" ]]; then + "$LLVM_PROFDATA" merge -sparse "$PROFDATA" "${files[@]}" -o "$PROFDATA.new" + mv "$PROFDATA.new" "$PROFDATA" + else + "$LLVM_PROFDATA" merge -sparse "${files[@]}" -o "$PROFDATA" + fi + rm -f "${files[@]}" +} + +echo "=== Running verification tests for profile ===" +"$ROOT/scripts/run-verify-tests.sh" || true + +# CodeGen integration path (CppVerifyIntegration async hook). +if [[ -x "$BUILD/bin/clang" ]]; then + CLANG_COV="$COV_DIR/clang_%p.profraw" + export LLVM_PROFILE_FILE="$CLANG_COV" + for f in "$ROOT/clang/test/Verify/compile_with_verify.cpp" \ + "$ROOT/clang/test/Verify/suite"/{cov_*,z3_*,bmc_*,spec_*,modular*,chained*}.cpp; do + [[ -f "$f" ]] || continue + "$BUILD/bin/clang" -std=c++17 -fverify-contracts -c "$f" \ + -o "$COV_DIR/$(basename "$f" .cpp).o" >/dev/null 2>&1 || true + done + FAIL_SRC="$COV_DIR/cov_verify_fail.cpp" + printf '%s\n' 'int bad() pre(false) post(result == 0) { return 1; }' >"$FAIL_SRC" + "$BUILD/bin/clang" -std=c++17 -fverify-contracts -c "$FAIL_SRC" -o "$COV_DIR/cov_verify_fail.o" \ + >/dev/null 2>&1 || true + "$BUILD/bin/clang" -std=c++17 -fverify-contracts -fno-verify -c \ + "$ROOT/clang/test/Verify/compile_with_verify.cpp" -o "$COV_DIR/compile_no_verify.o" \ + >/dev/null 2>&1 || true + merge_profiles + export LLVM_PROFILE_FILE="$COV_DIR/cppverify_%p.profraw" +fi + +merge_profiles + +# Lean backend edge cases. +"$BUILD/bin/cpp-verify" --backend=lean \ + "$ROOT/clang/test/Verify/suite/z3_modular_call.cpp" >/dev/null 2>&1 || true + +# Extra suite sweep to hit backend branches. +SUITE="$ROOT/clang/test/Verify/suite" +if [[ -d "$SUITE" ]]; then + LEAN_TMP="$COV_DIR/lean_scratch.lean" + for f in "$SUITE"/*.cpp; do + "$BUILD/bin/cpp-verify" "$f" >/dev/null 2>&1 || true + case "$(basename "$f")" in + cov_*bmc*|*bmc*.cpp|cov_loop*) "$BUILD/bin/cpp-verify" --backend=bmc --unroll=3 "$f" >/dev/null 2>&1 || true + "$BUILD/bin/cpp-verify" --backend=bmc --unroll=0 "$f" >/dev/null 2>&1 || true ;; + cov_*lean*|lean*.cpp) "$BUILD/bin/cpp-verify" --backend=lean "--lean-out=$LEAN_TMP" "$f" >/dev/null 2>&1 || true ;; + cov_dump*|dump_ir*) "$BUILD/bin/cpp-verify" --dump-ir=all "$f" >/dev/null 2>&1 || true ;; + esac + done + rm -f "$LEAN_TMP" + merge_profiles + # DumpIR layer parsing branches. + if [[ -f "$SUITE/dump_ir_layers.cpp" ]]; then + for layers in 1 2 3 4 "layer-3,layer-4" all; do + "$BUILD/bin/cpp-verify" "--dump-ir=$layers" "$SUITE/dump_ir_layers.cpp" >/dev/null 2>&1 || true + done + fi + for f in "$ROOT/clang/test/Verify"/*.cpp; do + [[ -f "$f" ]] || continue + "$BUILD/bin/cpp-verify" "$f" >/dev/null 2>&1 || true + "$BUILD/bin/cpp-verify" --dump-ir=all "$f" >/dev/null 2>&1 || true + "$BUILD/bin/cpp-verify" --backend=lean "--lean-out=$LEAN_TMP" "$f" >/dev/null 2>&1 || true + done + merge_profiles +fi + +echo "=== Merging profiles ===" +merge_profiles + +OBJ_DIR="$BUILD/tools/clang/lib/Verify/CMakeFiles/obj.clangVerify.dir" +if [[ ! -d "$OBJ_DIR" ]]; then + echo "error: object dir not found: $OBJ_DIR" >&2 + exit 1 +fi + +REPORT="$COV_DIR/report.txt" +echo "=== Coverage report (clang/lib/Verify) ===" +OBJ_FILES=("$OBJ_DIR"/*/*.o) +if [[ ! -e "${OBJ_FILES[0]}" ]]; then + OBJ_FILES=("$OBJ_DIR"/*.o) +fi +COV_BINARIES=("$BUILD/bin/cpp-verify") +[[ -x "$BUILD/bin/clang" ]] && COV_BINARIES+=("$BUILD/bin/clang") +"$LLVM_COV" report "${COV_BINARIES[@]}" \ + -instr-profile="$PROFDATA" "${OBJ_FILES[@]}" \ + > "$REPORT" 2>/dev/null + +echo "--- clang/lib/Verify only (regions) ---" +grep 'clang/lib/Verify' "$REPORT" | awk '{reg+=$2; miss+=$3} END { + if (reg>0) printf "TOTAL Verify regions: %.2f%% (%d/%d)\n", 100*(reg-miss)/reg, reg-miss, reg; + else print "no Verify rows" +}' + +cat "$REPORT" +REGIONS="$(grep 'clang/lib/Verify' "$REPORT" | awk '{reg+=$2; miss+=$3} END { + if (reg>0) printf "%.2f", 100*(reg-miss)/reg; else print "0" +}')" +echo "=== TOTAL regions line coverage: ${REGIONS}% (threshold ${THRESHOLD}%) ===" +python3 - <= t else 1) +PY \ No newline at end of file diff --git a/scripts/run-verify-tests.sh b/scripts/run-verify-tests.sh new file mode 100755 index 0000000000..5ba4d53f55 --- /dev/null +++ b/scripts/run-verify-tests.sh @@ -0,0 +1,106 @@ +#!/usr/bin/env bash +# Run clang/test/Verify tests with correct expectations (syntax vs verify vs expect-fail). +set -euo pipefail + +ROOT="$(cd "$(dirname "$0")/.." && pwd)" +BUILD="${CPPVERIFY_BUILD:-$ROOT/build}" +CLANG="$BUILD/bin/clang" +CPP_VERIFY="$BUILD/bin/cpp-verify" +TEST_DIR="$ROOT/clang/test/Verify" + +if [[ ! -x "$CPP_VERIFY" ]]; then + echo "error: cpp-verify not found at $CPP_VERIFY (run ./setup.sh first)" >&2 + exit 1 +fi + +pass=0 +fail=0 +skip=0 + +run_one() { + local f="$1" + local base + base="$(basename "$f")" + + # Frontend-only (clang_cc1 / ast-dump / emit-llvm); no end-to-end verify expectation. + if grep -q '%clang_cc1' "$f" 2>/dev/null && ! grep -q '%cpp-verify' "$f" 2>/dev/null; then + if grep -q 'RUN:.*clang_cc1' "$f"; then + echo "SKIP $base (frontend-only)" + skip=$((skip + 1)) + return 0 + fi + fi + + # Parse/type error tests: only clang syntax-check. + if [[ "$base" == errors_*.cpp ]] || [[ "$base" == lexer_keywords.cpp ]] \ + || [[ "$base" == backward_compat*.cpp ]]; then + if "$CLANG" -std=c++17 -fverify-contracts -fsyntax-only "$f" >/dev/null 2>&1; then + : # expected compile errors may still return 0 for partial parse in some cases + fi + echo "SKIP $base (negative frontend)" + skip=$((skip + 1)) + return 0 + fi + + local out rc expect_fail=0 + if grep -q 'not %cpp-verify' "$f" 2>/dev/null || grep -q 'FAIL:' "$f" 2>/dev/null; then + expect_fail=1 + fi + + local -a extra_args=() + if grep -q '%cpp-verify --backend=lean' "$f" 2>/dev/null; then + local tmp + tmp="$(mktemp -t cppverify.lean.XXXXXX)" + extra_args=(--backend=lean "--lean-out=$tmp") + elif grep -q '%cpp-verify --backend=bmc' "$f" 2>/dev/null; then + extra_args=(--backend=bmc) + fi + + if ((${#extra_args[@]} > 0)); then + out="$("$CPP_VERIFY" "${extra_args[@]}" "$f" 2>&1)" || rc=$? + else + out="$("$CPP_VERIFY" "$f" 2>&1)" || rc=$? + fi + rc="${rc:-0}" + + if [[ "$expect_fail" -eq 1 ]]; then + if echo "$out" | grep -qE 'verification failed:|error:'; then + echo "PASS $base (expected failure)" + pass=$((pass + 1)) + else + echo "FAIL $base (expected verification failure)" + echo "$out" | head -8 + fail=$((fail + 1)) + fi + return 0 + fi + + if echo "$out" | grep -q '^error:'; then + echo "FAIL $base (verify error)" + echo "$out" | grep '^error:' | head -5 + fail=$((fail + 1)) + return 0 + fi + + if [[ "$rc" -ne 0 ]]; then + echo "FAIL $base (exit $rc)" + echo "$out" | head -8 + fail=$((fail + 1)) + return 0 + fi + + echo "PASS $base" + pass=$((pass + 1)) +} + +echo "=== cpp-verify test sweep ===" +echo "build: $BUILD" + +shopt -s nullglob +for f in "$TEST_DIR"/*.cpp "$TEST_DIR"/suite/*.cpp; do + [[ -f "$f" ]] || continue + run_one "$f" +done + +echo "=== summary: pass=$pass fail=$fail skip=$skip ===" +[[ "$fail" -eq 0 ]] \ No newline at end of file diff --git a/website/README.md b/website/README.md index 83490dc417..d019045573 100644 --- a/website/README.md +++ b/website/README.md @@ -1,38 +1,46 @@ # CppVerify documentation site -Dual build: +Published at [swayaminsync.github.io/cpp-verify](https://swayaminsync.github.io/cpp-verify/). -| Output | Tool | Path | -|--------|------|------| -| Book + language reference | **Sphinx** (Furo) | `website/build/` | -| C++ verifier API | **Doxygen** | `website/build/doxygen/` | +## Outputs -## Build +| Output | Tool | Location | +|--------|------|----------| +| Book + language reference | Sphinx (Furo) | `website/build/` | +| C++ verifier API | Doxygen | `website/build/doxygen/` | -**Doxygen is required** for the C++ API (install once: `brew install doxygen` or `apt install doxygen`). +## Build (from repository root) + +Doxygen is required for the C++ API (`brew install doxygen` or `apt install doxygen`). ```bash ./website/scripts/build-docs.sh -open website/build/index.html # book home -open website/build/doxygen/index.html # C++ API +open website/build/index.html +open website/build/doxygen/index.html ``` -Auto-install Doxygen when possible: `AUTO_INSTALL_DOXYGEN=1 ./website/scripts/build-docs.sh` +Auto-install Doxygen when possible: + +```bash +AUTO_INSTALL_DOXYGEN=1 ./website/scripts/build-docs.sh +``` ## Structure -- `source/book/part-i/` — Foundations (Ch 1–8), no CppVerify syntax required first -- `source/book/part-ii/` — CppVerify practice (Ch 9–16) -- `source/language/` — Desk reference (syntax lookup) -- `source/api/` — Link page into Doxygen -- `doxygen/Doxyfile` — Scans `llvm-project/clang/lib/Verify/*.h` -- `source/_static/logo-todo.svg` — Replace with your logo when ready +| Path | Content | +|------|---------| +| `source/index.rst` | Home — install, quick start, links | +| `source/book/part-i/` | Foundations (Ch 1–8) | +| `source/book/part-ii/` | CppVerify practice (Ch 9–17) | +| `source/language/` | Contract syntax reference | +| `source/api/` | Link into Doxygen | +| `source/_static/` | Logos, diagrams, `custom.css` | +| `doxygen/Doxyfile` | Scans `clang/lib/Verify` headers | + +## Branding -## Replace logo +Logos live in `source/_static/` (`logo.svg`, `logo-dark.svg`, `favicon.svg`). The product repo also ships PNGs under top-level `logos/` for the GitHub README. -Drop your asset as `source/_static/logo.svg` and set in `conf.py`: +## RST tables -```python -"light_logo": "logo.svg", -"dark_logo": "logo.svg", -``` \ No newline at end of file +Use ``.. list-table::`` with ``:header-rows: 1`` and ``:widths:``. Avoid grid tables (``+---+``) — they break easily when column widths do not match exactly. \ No newline at end of file diff --git a/website/source/_static/custom.css b/website/source/_static/custom.css index c91a0313e1..cad9452801 100644 --- a/website/source/_static/custom.css +++ b/website/source/_static/custom.css @@ -64,4 +64,45 @@ div.highlight-cpp pre { main h1 { margin-top: 0.5rem; +} + +/* Tables — scroll on small screens; consistent spacing */ +.table-wrapper { + overflow-x: auto; + margin: 1rem 0 1.5rem; +} + +.table-wrapper table.docutils { + width: 100%; + border-collapse: collapse; +} + +.table-wrapper th, +.table-wrapper td { + vertical-align: top; + padding: 0.55rem 0.75rem; +} + +.table-wrapper thead th { + border-bottom: 2px solid var(--color-table-header-border, rgba(128, 128, 128, 0.35)); +} + +.table-wrapper tbody tr { + border-bottom: 1px solid var(--color-table-row-border, rgba(128, 128, 128, 0.2)); +} + +/* API index button (api/index.rst raw HTML) */ +a.btn { + display: inline-block; + margin: 1rem 0; + padding: 0.6rem 1.2rem; + background: var(--color-brand-primary, #3b6fd9); + color: #fff !important; + border-radius: 6px; + text-decoration: none; + font-weight: 600; +} + +a.btn:hover { + filter: brightness(1.08); } \ No newline at end of file diff --git a/website/source/_static/favicon-16.png b/website/source/_static/favicon-16.png new file mode 100644 index 0000000000..0ee1c708ad Binary files /dev/null and b/website/source/_static/favicon-16.png differ diff --git a/website/source/_static/favicon-180.png b/website/source/_static/favicon-180.png new file mode 100644 index 0000000000..49a508105a Binary files /dev/null and b/website/source/_static/favicon-180.png differ diff --git a/website/source/_static/favicon-32.png b/website/source/_static/favicon-32.png new file mode 100644 index 0000000000..682beabaf3 Binary files /dev/null and b/website/source/_static/favicon-32.png differ diff --git a/website/source/_static/favicon-512.png b/website/source/_static/favicon-512.png new file mode 100644 index 0000000000..a8980641e3 Binary files /dev/null and b/website/source/_static/favicon-512.png differ diff --git a/website/source/_static/favicon.svg b/website/source/_static/favicon.svg index 4fc1a630ee..3ad526bdb8 100644 --- a/website/source/_static/favicon.svg +++ b/website/source/_static/favicon.svg @@ -1,4 +1,9 @@ - - - C+ + + + + + + + + \ No newline at end of file diff --git a/website/source/_static/logo-dark.svg b/website/source/_static/logo-dark.svg new file mode 100644 index 0000000000..2683670a5e --- /dev/null +++ b/website/source/_static/logo-dark.svg @@ -0,0 +1,17 @@ + + + + + + + + + + + + + + + CppVerify + + \ No newline at end of file diff --git a/website/source/_static/logo-mark.svg b/website/source/_static/logo-mark.svg new file mode 100644 index 0000000000..4061ee390e --- /dev/null +++ b/website/source/_static/logo-mark.svg @@ -0,0 +1,9 @@ + + + + + + + + + \ No newline at end of file diff --git a/website/source/_static/logo.png b/website/source/_static/logo.png new file mode 100644 index 0000000000..fd5b4e4b32 Binary files /dev/null and b/website/source/_static/logo.png differ diff --git a/website/source/_static/logo.svg b/website/source/_static/logo.svg new file mode 100644 index 0000000000..e83cbc4c24 --- /dev/null +++ b/website/source/_static/logo.svg @@ -0,0 +1,17 @@ + + + + + + + + + + + + + + + CppVerify + + \ No newline at end of file diff --git a/website/source/api/index.rst b/website/source/api/index.rst index 236a120b4e..5c7cc4223f 100644 --- a/website/source/api/index.rst +++ b/website/source/api/index.rst @@ -5,7 +5,7 @@ Reference for the verification engine headers in ``clang/lib/Verify/``. .. raw:: html -

Open API reference

+

Open API reference (Doxygen)

Modules ------- diff --git a/website/source/book/part-ii/ch11-first-verified-function.rst b/website/source/book/part-ii/ch11-first-verified-function.rst index f69ebf552e..ace45aa849 100644 --- a/website/source/book/part-ii/ch11-first-verified-function.rst +++ b/website/source/book/part-ii/ch11-first-verified-function.rst @@ -44,3 +44,6 @@ Compile the same file Verification runs in parallel; ghost code is stripped — no runtime contract overhead. +Larger programs compose **modularly**: callee contracts are assumed at call sites, including nested +calls such as ``return f(g(x))`` (see :doc:`ch17-backends-modular-calls`). + diff --git a/website/source/book/part-ii/ch13-spec-and-proof-functions.rst b/website/source/book/part-ii/ch13-spec-and-proof-functions.rst index 2277a95c7a..42cc872b1b 100644 --- a/website/source/book/part-ii/ch13-spec-and-proof-functions.rst +++ b/website/source/book/part-ii/ch13-spec-and-proof-functions.rst @@ -36,6 +36,15 @@ Use in contracts: Call from ``ghost { ... }`` blocks in executable functions. +**Fuel** and **hide/reveal** control how much recursive spec body is inlined: + +.. code-block:: cpp + + ghost { reveal_with_fuel(fact, 2); } // bounded unfolding + ghost { hide(triple); } // opaque spec application + +See also :doc:`ch17-backends-modular-calls`. + ``constexpr`` in contracts -------------------------- diff --git a/website/source/book/part-ii/ch15-toolchain-and-flags.rst b/website/source/book/part-ii/ch15-toolchain-and-flags.rst index ca201bc727..66fb090648 100644 --- a/website/source/book/part-ii/ch15-toolchain-and-flags.rst +++ b/website/source/book/part-ii/ch15-toolchain-and-flags.rst @@ -22,6 +22,8 @@ Key flags - ``-fverify-contracts`` — enable contract keywords - ``-fno-verify`` — compile path without Z3 +- ``cpp-verify --backend={z3,bmc,lean}`` — verification engine (see :doc:`ch17-backends-modular-calls`) +- ``cpp-verify --unroll=N`` — loop bound for BMC - ``cpp-verify --dump-ir[=1,2,3,4]`` — dump VCR / passive / VC / Z3 layers IR layers @@ -34,5 +36,7 @@ IR layers Multiple layers are separated by ``======`` in the dump. +Compiler flags table and IR dump details: :doc:`../../language/tooling`. + Engine API: :doc:`../../api/index`. diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst new file mode 100644 index 0000000000..53106ee54b --- /dev/null +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -0,0 +1,104 @@ +Chapter 17 — Backends, modular calls, and debugging +=================================================== + +CppVerify is not only a Z3-backed WP checker. The same front end and IR feed multiple +backends and modular call lowering. This chapter ties those pieces to how you work day to day. + +Verification backends +--------------------- + +.. list-table:: + :header-rows: 1 + :widths: 18 22 60 + + * - Backend + - CLI + - When to use it + * - **Z3** (default) + - ``cpp-verify file.cpp`` + - General proofs: functions, pointers, spec/proof, loops via invariant/decreases (WP path). + * - **BMC** + - ``cpp-verify --backend=bmc --unroll=N file.cpp`` + - Small bounded loops: body unrolled ``N`` times, then Z3. Good when loop structure is simple and bounds are tiny. + * - **Lean export** + - ``cpp-verify --backend=lean --lean-out=out.lean file.cpp`` + - Export a scratch-pad ``theorem cppverify_goal`` for manual proof in Lean 4 — not automated discharge. + +BMC does not replace loop contracts on the default path; it is an alternate pipeline stage that +**expands** loops before passivization. You still write ``invariant`` / ``decreases`` for documentation +and for the Z3 backend. + +Modular function calls +---------------------- + +Functions with ``pre`` / ``post`` are verified **modularly**: the caller assumes the callee’s +precondition and inherits its postcondition (and frame conditions) without re-analyzing the callee body. + +Simple call: + +.. code-block:: cpp + + int y = abs_val(x); + +Chained calls in one expression are supported by lowering inner calls to temporaries first: + +.. code-block:: cpp + + int inc(int x) pre(x >= 0 && x < 100) post(result == x + 1) { return x + 1; } + + int twice(int x) + pre(x >= 0 && x < 98) + post(result == x + 2) + { + return inc(inc(x)); // inner inc, then outer inc + } + +The converter emits ``VCallStmt`` for each exec call site; passivization substitutes callee contracts +in order. Spec and proof functions are not emitted at runtime and are handled by inlining or axioms. + +Parallel verify + compile +------------------------- + +.. code-block:: bash + + clang++ -std=c++17 -fverify-contracts -c module.cpp -o module.o + +With ``-fverify-contracts``, contract keywords parse as part of the language. Unless you pass +``-fno-verify``, the compiler runs **cpp-verify in parallel** with code generation. Ghost blocks, +spec functions, and proof functions are stripped from the object file — no runtime cost. + +Dumping IR layers +----------------- + +When a proof fails or looks wrong, dump intermediate representations: + +.. code-block:: bash + + cpp-verify --dump-ir=1 file.cpp # Layer 1: VCR (typed CFG) + cpp-verify --dump-ir=2 file.cpp # Layer 2: passive (SSA assume/assert) + cpp-verify --dump-ir=3,4 file.cpp # VC formula and Z3 translation + +Layer aliases: ``layer-1`` … ``layer-4``, or ``all``. Multiple layers are separated by ``======``. + +``recommends`` and soft checks +------------------------------ + +``recommends`` on spec functions is optional advice. If verification **fails**, the tool may +report that a ``recommends`` clause at a call site was not implied by the caller’s precondition — +a warning, not a hard error. + +Regression tests +---------------- + +The repository ships executable examples under ``clang/test/Verify/`` and ``clang/test/Verify/suite/``. +From the repo root: + +.. code-block:: bash + + ./scripts/run-verify-tests.sh + +Contributors can measure ``clang/lib/Verify`` region coverage with +``./scripts/coverage-sweep.sh`` (after a normal build) or ``./scripts/coverage-verify.sh`` +(full instrumented rebuild). Use ``-DCPPVERIFY_ENABLE_COVERAGE=ON`` on ``clangVerify`` only. + +Next: :doc:`ch16-when-verification-fails` for counterexamples and fixing failed proofs. \ No newline at end of file diff --git a/website/source/book/part-ii/index.rst b/website/source/book/part-ii/index.rst index 5f0ac8503e..d3fe4b6757 100644 --- a/website/source/book/part-ii/index.rst +++ b/website/source/book/part-ii/index.rst @@ -2,7 +2,7 @@ Part II — CppVerify =================== These chapters cover verified C++ in practice: the toolchain, contract syntax, common proof -patterns, and how to respond when the verifier reports a failure. +patterns, backends (Z3, BMC, Lean export), modular calls, and how to respond when verification fails. .. figure:: /_static/diagrams/cppverify-workflow.svg :align: center @@ -19,4 +19,5 @@ patterns, and how to respond when the verifier reports a failure. ch13-spec-and-proof-functions ch14-pointers-frames-modifies ch15-toolchain-and-flags - ch16-when-verification-fails \ No newline at end of file + ch16-when-verification-fails + ch17-backends-modular-calls \ No newline at end of file diff --git a/website/source/conf.py b/website/source/conf.py index ddafd303f0..f01b6c3308 100644 --- a/website/source/conf.py +++ b/website/source/conf.py @@ -40,8 +40,8 @@ html_favicon = "_static/favicon.svg" html_theme_options = { - "light_logo": "logo-todo.svg", - "dark_logo": "logo-todo.svg", + "light_logo": "logo.svg", + "dark_logo": "logo-dark.svg", "source_repository": "https://github.com/SwayamInSync/cpp-verify", "source_branch": "main", "source_directory": "website/source/", diff --git a/website/source/index.rst b/website/source/index.rst index cdf6a53f80..cd634e248f 100644 --- a/website/source/index.rst +++ b/website/source/index.rst @@ -55,8 +55,8 @@ Install → ``build\bin\cpp-verify.exe``, ``build\bin\clang++.exe`` -Manual build (same CMake flags) -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Manual build (from repository root; same flags as ``setup.sh``) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. tabs:: @@ -125,6 +125,16 @@ Quick start Use ``-fverify-contracts`` on ``clang++`` so ``pre`` / ``post`` are keywords. ``cpp-verify`` adds that flag automatically. +Backends and modular calls +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. code-block:: bash + + cpp-verify --backend=bmc --unroll=3 loops.cpp + cpp-verify --dump-ir=3,4 debug.cpp + +See :doc:`book/part-ii/ch17-backends-modular-calls` for Z3 vs BMC vs Lean export and chained calls like ``f(g(x))``. + Learn more ---------- diff --git a/website/source/language/expressions.rst b/website/source/language/expressions.rst index 124ccca83d..e2b1be8cb4 100644 --- a/website/source/language/expressions.rst +++ b/website/source/language/expressions.rst @@ -6,4 +6,8 @@ Contract expressions - ``forall(i, lo, hi, body)`` — bounded ∀ - ``exists(i, lo, hi, body)`` — bounded ∃ -Must be contextually ``bool`` where used as conditions. \ No newline at end of file +Must be contextually ``bool`` where used as conditions. + +``old`` is only valid in postconditions (and nested expressions there). ``result`` is only valid +in postconditions. Integer operators follow the function kind: ``spec`` uses mathematical integers; +``proof`` and executable code use machine integers (see :doc:`integers`). \ No newline at end of file diff --git a/website/source/language/index.rst b/website/source/language/index.rst index 3abbd1968e..fce9e8cad1 100644 --- a/website/source/language/index.rst +++ b/website/source/language/index.rst @@ -1,7 +1,9 @@ Language reference ================== -Compact lookup for contract syntax and semantics. For learning, use :doc:`../book/index`. +Compact lookup for contract syntax and semantics. For a guided introduction, start with +:doc:`../book/index`; for backends and ``cpp-verify`` flags, see :doc:`../book/part-ii/ch17-backends-modular-calls` +and :doc:`tooling`. .. toctree:: :maxdepth: 1 diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 99d0bc8e7f..a866de5d10 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -11,5 +11,7 @@ Currently outside the supported core: - Virtual dispatch and multiple inheritance - Heap allocation with ``new`` and ``delete`` -Pointer and heap reasoning are available in the language surface; depth of automation continues -to expand. See the project design notes for the current roadmap. \ No newline at end of file +Pointer and heap reasoning are available in the language surface (see :doc:`pointers` and +:doc:`../book/part-ii/ch14-pointers-frames-modifies`). Depth of automation continues to expand; +see the project :doc:`../book/part-ii/ch17-backends-modular-calls` and design notes in the repo +``extras/docs/`` tree. \ No newline at end of file diff --git a/website/source/language/pointers.rst b/website/source/language/pointers.rst index 7b95c95c8a..858f11a8d2 100644 --- a/website/source/language/pointers.rst +++ b/website/source/language/pointers.rst @@ -4,4 +4,18 @@ Pointers - Heap modeled internally (Z3 arrays) - ``modifies(*p, ...)`` — frame - ``aliases(p, q)`` — allow aliasing -- Implicit ``p != q`` for distinct mutable parameters \ No newline at end of file +- Implicit ``p != q`` for distinct mutable parameters + +Example: + +.. code-block:: cpp + + void write(int *p, int v) + pre(p != nullptr) + modifies(*p) + post(*p == v) + { + *p = v; + } + +See :doc:`../book/part-ii/ch14-pointers-frames-modifies`. \ No newline at end of file diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index 038c15d01b..794fc03925 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -1,11 +1,107 @@ Commands and flags ================== +Standalone verifier +------------------- + .. code-block:: bash cpp-verify file.cpp - cpp-verify --dump-ir=1,2 file.cpp + cpp-verify --backend=z3 file.cpp + cpp-verify --backend=bmc --unroll=3 file.cpp + cpp-verify --backend=lean --lean-out=goal.lean file.cpp + cpp-verify --dump-ir=1,2,3,4 file.cpp + +``cpp-verify`` is a Clang tooling driver: it always adds ``-std=c++17`` and ``-fverify-contracts``. + +Backends +-------- + +.. list-table:: + :header-rows: 1 + :widths: 22 78 + + * - Flag + - Meaning + * - ``--backend=z3`` + - Default. Weakest precondition + Z3 (loops via contracts on the WP path). + * - ``--backend=bmc`` + - Unroll loops up to ``--unroll=N`` (default 10), then Z3. + * - ``--backend=lean`` + - Write Lean 4 scratch-pad to ``--lean-out`` (required for useful output). + * - ``--unroll=N`` + - BMC loop bound only. + +Compile with contracts +---------------------- + +.. code-block:: bash + clang++ -std=c++17 -fverify-contracts -c file.cpp -o file.o clang++ -std=c++17 -fverify-contracts -fno-verify -c file.cpp -o file.o -``--dump-ir`` layers: ``1`` VCR, ``2`` passive, ``3`` verification condition, ``4`` solver input. \ No newline at end of file +.. list-table:: + :header-rows: 1 + :widths: 28 72 + + * - Flag + - Effect + * - ``-fverify-contracts`` + - Enable contract keywords (``pre``, ``post``, ``spec``, ``ghost``, …). + * - ``-fno-verify`` + - Parse contracts but skip SMT; compile only (no parallel verify). + +Without ``-fno-verify``, verification runs **in parallel** with code generation (see +:doc:`../book/part-ii/ch17-backends-modular-calls`). + +IR dump layers +-------------- + +``--dump-ir`` accepts a comma-separated mask (or ``all``): + +.. list-table:: + :header-rows: 1 + :widths: 12 88 + + * - Layer + - Content + * - ``1`` / ``layer-1`` + - VCR IR — typed control flow, contracts preserved + * - ``2`` / ``layer-2`` + - Passive IR — SSA, ``assume`` / ``assert``, heap versions + * - ``3`` / ``layer-3`` + - Verification condition (logical formula) + * - ``4`` / ``layer-4`` + - Z3 translation of the VC + +Examples: + +.. code-block:: bash + + cpp-verify --dump-ir=1 file.cpp + cpp-verify --dump-ir=layer-3,layer-4 file.cpp + cpp-verify --dump-ir file.cpp # all layers + +Layers are separated by a line of ``======`` in the output. + +Testing and coverage +-------------------- + +Regression tests live under ``clang/test/Verify/``. From the **repository root**: + +.. list-table:: + :header-rows: 1 + :widths: 32 68 + + * - Script + - Purpose + * - ``./scripts/run-verify-tests.sh`` + - Run executable examples (pass / expected-fail). + * - ``./scripts/coverage-sweep.sh`` + - Fast profile merge after a normal build (from repo root). + * - ``./scripts/coverage-verify.sh`` + - Full instrumented rebuild + sweep (slow; use when changing coverage setup). + +Set ``CPPVERIFY_ENABLE_COVERAGE=ON`` on ``clangVerify`` only — not the whole LLVM tree. + +Engine headers: :doc:`../api/index`. \ No newline at end of file