Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -85,3 +85,7 @@ pythonenv*
/clang/utils/analyzer/projects/*/RefScanBuildResults
# automodapi puts generated documentation files here.
/lldb/docs/python_api/


# custom
docs/
25 changes: 25 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,31 @@ All contract syntax is gated behind `-fverify-contracts`. Without the flag,
none of these names are reserved — existing C++ that uses `pre`, `post`, etc.
as identifiers compiles unchanged.

## Build the cpp-verify clang compiler

```bash
cmake -S llvm -B build -G Ninja \
-DCMAKE_BUILD_TYPE=Release \
-DLLVM_ENABLE_PROJECTS="clang" \
-DLLVM_TARGETS_TO_BUILD="X86,AArch64" \
-DCMAKE_EXPORT_COMPILE_COMMANDS=ON

# Symlink compile_commands.json for clangd / IDE integration
ln -sf build/compile_commands.json compile_commands.json

ninja -C build clang -j$(nproc)
```

## Usage

```bash
# Identifying tokens and dumping the output
./build/bin/clang++ -cc1 -fverify-contracts -dump-tokens samples/test1.cpp

# Parsing AST with contracts and dumping the output
./build/bin/clang++ -cc1 -fverify-contracts -ast-dump samples/test1.cpp
```

## Architecture

```
Expand Down
32 changes: 32 additions & 0 deletions clang/include/clang/AST/ASTContext.h
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,21 @@ class AtomicExpr;
class BlockExpr;
struct BlockVarCopyInit;
class BuiltinTemplateDecl;

/// Contract information attached to a FunctionDecl via side table.
struct FunctionContractInfo {
SmallVector<Expr *, 2> Preconditions;
SmallVector<Expr *, 2> Postconditions;
Expr *Decreases = nullptr;
bool IsSpec = false;
bool IsProof = false;
};

/// Contract information attached to a WhileStmt/ForStmt via side table.
struct LoopContractInfo {
SmallVector<Expr *, 2> Invariants;
Expr *Decreases = nullptr;
};
class CharUnits;
class ConceptDecl;
class CXXABI;
Expand Down Expand Up @@ -351,6 +366,13 @@ class ASTContext : public RefCountedBase<ASTContext> {
/// Mapping from __block VarDecls to BlockVarCopyInit.
llvm::DenseMap<const VarDecl *, BlockVarCopyInit> BlockVarCopyInits;

/// CppVerify: contract info for functions (pre/post/decreases/spec/proof).
llvm::DenseMap<const FunctionDecl *, FunctionContractInfo *>
FunctionContracts;

/// CppVerify: contract info for loops (invariant/decreases).
llvm::DenseMap<const Stmt *, LoopContractInfo *> LoopContracts;

/// Mapping from GUIDs to the corresponding MSGuidDecl.
mutable llvm::FoldingSet<MSGuidDecl> MSGuidDecls;

Expand Down Expand Up @@ -3422,6 +3444,16 @@ class ASTContext : public RefCountedBase<ASTContext> {
/// nullptr if none exists.
BlockVarCopyInit getBlockVarCopyInit(const VarDecl* VD) const;

/// CppVerify: get or create contract info for a function.
FunctionContractInfo &getOrCreateFunctionContract(const FunctionDecl *FD);
/// CppVerify: get contract info for a function, or nullptr if none.
const FunctionContractInfo *getFunctionContract(const FunctionDecl *FD) const;

/// CppVerify: get or create contract info for a loop statement.
LoopContractInfo &getOrCreateLoopContract(const Stmt *S);
/// CppVerify: get contract info for a loop, or nullptr if none.
const LoopContractInfo *getLoopContract(const Stmt *S) const;

/// Allocate an uninitialized TypeSourceInfo.
///
/// The caller should initialize the memory held by TypeSourceInfo using
Expand Down
10 changes: 9 additions & 1 deletion clang/include/clang/AST/ASTDumper.h
Original file line number Diff line number Diff line change
Expand Up @@ -23,9 +23,12 @@ class ASTDumper : public ASTNodeTraverser<ASTDumper, TextNodeDumper> {

const bool ShowColors;

const ASTContext *Ctx = nullptr;

public:
ASTDumper(raw_ostream &OS, const ASTContext &Context, bool ShowColors)
: NodeDumper(OS, Context, ShowColors), OS(OS), ShowColors(ShowColors) {}
: NodeDumper(OS, Context, ShowColors), OS(OS), ShowColors(ShowColors),
Ctx(&Context) {}

ASTDumper(raw_ostream &OS, bool ShowColors)
: NodeDumper(OS, ShowColors), OS(OS), ShowColors(ShowColors) {}
Expand All @@ -44,6 +47,11 @@ class ASTDumper : public ASTNodeTraverser<ASTDumper, TextNodeDumper> {
void VisitFunctionTemplateDecl(const FunctionTemplateDecl *D);
void VisitClassTemplateDecl(const ClassTemplateDecl *D);
void VisitVarTemplateDecl(const VarTemplateDecl *D);

// CppVerify: dump contract side-table entries as child nodes.
void VisitFunctionDecl(const FunctionDecl *D);
void VisitWhileStmt(const WhileStmt *S);

Copilot AI Apr 9, 2026

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Parser stores loop contract metadata for both while and for statements, but ASTDumper only adds side-table children for WhileStmt. As a result, -ast-dump will omit invariants/decreases for for-loops even when present. Consider adding a VisitForStmt override (and any other loop kinds you support) to dump LoopContractInfo consistently.

Suggested change
void VisitWhileStmt(const WhileStmt *S);
void VisitWhileStmt(const WhileStmt *S);
void VisitForStmt(const ForStmt *S);

Copilot uses AI. Check for mistakes.
void VisitForStmt(const ForStmt *S);
};

} // namespace clang
Expand Down
197 changes: 197 additions & 0 deletions clang/include/clang/AST/ExprContract.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,197 @@
//===--- ExprContract.h - Contract expression AST nodes ---------*- C++ -*-===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//
//
// This file defines AST nodes for CppVerify contract expressions:
// ForallExpr, ExistsExpr, OldExpr, ResultExpr
//
//===----------------------------------------------------------------------===//

#ifndef LLVM_CLANG_AST_EXPRCONTRACT_H
#define LLVM_CLANG_AST_EXPRCONTRACT_H

#include "clang/AST/Decl.h"
#include "clang/AST/Expr.h"
#include "clang/AST/Type.h"

namespace clang {

// Forward declaration for serialization friend access.
class ASTStmtReader;

/// ForallExpr - Represents a bounded universal quantifier:
/// forall(binder, lo, hi, body)
/// means: for all binder in [lo, hi), body holds.
class ForallExpr : public Expr {
friend class ASTStmtReader;
SourceLocation ForallLoc;
SourceLocation LParenLoc;
SourceLocation RParenLoc;
VarDecl *BoundVar;
enum { LO, HI, BODY, NUM_SUBEXPRS };
Stmt *SubExprs[NUM_SUBEXPRS];

public:
ForallExpr(SourceLocation ForallLoc, SourceLocation LParenLoc,
SourceLocation RParenLoc, VarDecl *BoundVar, Expr *Lo, Expr *Hi,
Expr *Body, QualType BoolTy)
: Expr(ForallExprClass, BoolTy, VK_PRValue, OK_Ordinary),
ForallLoc(ForallLoc), LParenLoc(LParenLoc), RParenLoc(RParenLoc),
BoundVar(BoundVar) {
SubExprs[LO] = Lo;
SubExprs[HI] = Hi;
SubExprs[BODY] = Body;
setDependence(ExprDependence::None);
Comment thread
SwayamInSync marked this conversation as resolved.
Comment thread
SwayamInSync marked this conversation as resolved.
}

explicit ForallExpr(EmptyShell Empty) : Expr(ForallExprClass, Empty) {}

VarDecl *getBoundVar() const { return BoundVar; }
Expr *getLo() const { return cast<Expr>(SubExprs[LO]); }
Expr *getHi() const { return cast<Expr>(SubExprs[HI]); }
Expr *getBody() const { return cast<Expr>(SubExprs[BODY]); }

SourceLocation getForallLoc() const { return ForallLoc; }
SourceLocation getLParenLoc() const { return LParenLoc; }
SourceLocation getRParenLoc() const { return RParenLoc; }
SourceLocation getBeginLoc() const LLVM_READONLY { return ForallLoc; }
SourceLocation getEndLoc() const LLVM_READONLY { return RParenLoc; }

static bool classof(const Stmt *T) {
return T->getStmtClass() == ForallExprClass;
}

child_range children() {
return child_range(&SubExprs[0], &SubExprs[NUM_SUBEXPRS]);
}
const_child_range children() const {
return const_child_range(&SubExprs[0], &SubExprs[NUM_SUBEXPRS]);
}
};

/// ExistsExpr - Represents a bounded existential quantifier:
/// exists(binder, lo, hi, body)
/// means: there exists binder in [lo, hi) such that body holds.
class ExistsExpr : public Expr {
friend class ASTStmtReader;
SourceLocation ExistsLoc;
SourceLocation LParenLoc;
SourceLocation RParenLoc;
VarDecl *BoundVar;
enum { LO, HI, BODY, NUM_SUBEXPRS };
Stmt *SubExprs[NUM_SUBEXPRS];

public:
ExistsExpr(SourceLocation ExistsLoc, SourceLocation LParenLoc,
SourceLocation RParenLoc, VarDecl *BoundVar, Expr *Lo, Expr *Hi,
Expr *Body, QualType BoolTy)
: Expr(ExistsExprClass, BoolTy, VK_PRValue, OK_Ordinary),
ExistsLoc(ExistsLoc), LParenLoc(LParenLoc), RParenLoc(RParenLoc),
BoundVar(BoundVar) {
SubExprs[LO] = Lo;
SubExprs[HI] = Hi;
SubExprs[BODY] = Body;
setDependence(ExprDependence::None);
}

explicit ExistsExpr(EmptyShell Empty) : Expr(ExistsExprClass, Empty) {}

VarDecl *getBoundVar() const { return BoundVar; }
Expr *getLo() const { return cast<Expr>(SubExprs[LO]); }
Expr *getHi() const { return cast<Expr>(SubExprs[HI]); }
Expr *getBody() const { return cast<Expr>(SubExprs[BODY]); }

SourceLocation getExistsLoc() const { return ExistsLoc; }
SourceLocation getLParenLoc() const { return LParenLoc; }
SourceLocation getRParenLoc() const { return RParenLoc; }
SourceLocation getBeginLoc() const LLVM_READONLY { return ExistsLoc; }
SourceLocation getEndLoc() const LLVM_READONLY { return RParenLoc; }

static bool classof(const Stmt *T) {
return T->getStmtClass() == ExistsExprClass;
}

child_range children() {
return child_range(&SubExprs[0], &SubExprs[NUM_SUBEXPRS]);
}
const_child_range children() const {
return const_child_range(&SubExprs[0], &SubExprs[NUM_SUBEXPRS]);
}
};

/// OldExpr - Represents old(expr), referring to the value of expr at
/// function entry. Only valid in postconditions and proof function bodies.
class OldExpr : public Expr {
friend class ASTStmtReader;
SourceLocation OldLoc;
SourceLocation LParenLoc;
SourceLocation RParenLoc;
Stmt *Inner;

public:
OldExpr(SourceLocation OldLoc, SourceLocation LParenLoc,
SourceLocation RParenLoc, Expr *Inner)
: Expr(OldExprClass, Inner->getType(), VK_PRValue, OK_Ordinary),
OldLoc(OldLoc), LParenLoc(LParenLoc), RParenLoc(RParenLoc),
Inner(Inner) {
setDependence(ExprDependence::None);
}
Comment thread
SwayamInSync marked this conversation as resolved.

explicit OldExpr(EmptyShell Empty) : Expr(OldExprClass, Empty) {}

Expr *getInner() const { return cast<Expr>(Inner); }

SourceLocation getOldLoc() const { return OldLoc; }
SourceLocation getLParenLoc() const { return LParenLoc; }
SourceLocation getRParenLoc() const { return RParenLoc; }
SourceLocation getBeginLoc() const LLVM_READONLY { return OldLoc; }
SourceLocation getEndLoc() const LLVM_READONLY { return RParenLoc; }

static bool classof(const Stmt *T) {
return T->getStmtClass() == OldExprClass;
}

child_range children() { return child_range(&Inner, &Inner + 1); }
const_child_range children() const {
return const_child_range(&Inner, &Inner + 1);
}
};

/// ResultExpr - Represents 'result' in postconditions, referring to the
/// return value of the enclosing function.
class ResultExpr : public Expr {
friend class ASTStmtReader;
SourceLocation ResultLoc;

public:
ResultExpr(SourceLocation ResultLoc, QualType ReturnType)
: Expr(ResultExprClass, ReturnType, VK_PRValue, OK_Ordinary),
ResultLoc(ResultLoc) {
setDependence(ExprDependence::None);
}

explicit ResultExpr(EmptyShell Empty) : Expr(ResultExprClass, Empty) {}

SourceLocation getResultLoc() const { return ResultLoc; }
SourceLocation getBeginLoc() const LLVM_READONLY { return ResultLoc; }
SourceLocation getEndLoc() const LLVM_READONLY { return ResultLoc; }

static bool classof(const Stmt *T) {
return T->getStmtClass() == ResultExprClass;
}

child_range children() {
return child_range(child_iterator(), child_iterator());
}
const_child_range children() const {
return const_child_range(const_child_iterator(), const_child_iterator());
}
};

} // namespace clang

#endif // LLVM_CLANG_AST_EXPRCONTRACT_H
10 changes: 10 additions & 0 deletions clang/include/clang/AST/RecursiveASTVisitor.h
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@
#include "clang/AST/Expr.h"
#include "clang/AST/ExprCXX.h"
#include "clang/AST/ExprConcepts.h"
#include "clang/AST/ExprContract.h"
#include "clang/AST/ExprObjC.h"
#include "clang/AST/ExprOpenMP.h"
#include "clang/AST/LambdaCapture.h"
Expand All @@ -35,6 +36,7 @@
#include "clang/AST/OpenMPClause.h"
#include "clang/AST/Stmt.h"
#include "clang/AST/StmtCXX.h"
#include "clang/AST/StmtContract.h"
#include "clang/AST/StmtObjC.h"
#include "clang/AST/StmtOpenACC.h"
#include "clang/AST/StmtOpenMP.h"
Expand Down Expand Up @@ -2596,6 +2598,14 @@ DEF_TRAVERSE_STMT(ReturnStmt, {})
DEF_TRAVERSE_STMT(SwitchStmt, {})
DEF_TRAVERSE_STMT(WhileStmt, {})

// CppVerify contract nodes.
DEF_TRAVERSE_STMT(ContractAssertStmt, {})
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(OldExpr, {})
DEF_TRAVERSE_STMT(ResultExpr, {})

DEF_TRAVERSE_STMT(ConstantExpr, {})

DEF_TRAVERSE_STMT(CXXDependentScopeMemberExpr, {
Expand Down
Loading