[FEAT] Adding contracts parsing & diagnostics with basic type infomation

[SwayamInSync]

This pull request introduces foundational support for CppVerify contract-based verification in Clang's AST. It adds new AST node types for contract expressions and statements, manages contract metadata for functions and loops, and integrates contract parsing and diagnostics. The changes are organized into three main themes: AST node additions, contract metadata management, and parser/diagnostic enhancements.

AST Node Additions:

• Introduced new AST node classes in ExprContract.h and StmtContract.h for CppVerify contract constructs, including ForallExpr, ExistsExpr, OldExpr, ResultExpr, ContractAssertStmt, and GhostBlockStmt, enabling the representation of contract expressions and statements in the AST. [1] [2]
• Registered the new contract node types in StmtNodes.td so they are recognized as part of the AST hierarchy.

Contract Metadata Management:

• Added FunctionContractInfo and LoopContractInfo structures to ASTContext.h and implemented side tables in ASTContext for associating contract information (preconditions, postconditions, invariants, etc.) with functions and loops, along with accessor methods for retrieving and creating this metadata. [1] [2] [3] [4]

Parser and Diagnostic Enhancements:

• Extended the parser (Parser.h) with methods to parse contract clauses, contract statements, and contract expressions, and to track contract parsing context.
• Added new diagnostics for contract parsing and semantic errors in DiagnosticParseKinds.td and DiagnosticSemaKinds.td, providing user feedback for malformed contract constructs and misuse of contract features. [1] [2]

Integration and Build System:

• Updated includes throughout the AST and visitor infrastructure to recognize and traverse the new contract node types. [1] [2] [3] [4] [5] [6] [7] [8]
• Registered new source files for contract nodes in the build system (CMakeLists.txt). [1] [2]

[Copilot]

Pull request overview

This PR adds initial CppVerify contract support to Clang by introducing new AST nodes for contract expressions/statements, storing contract metadata in ASTContext side tables for functions/loops, and extending the parser (plus basic diagnostics) to recognize contract syntax.

Changes:

• Added new AST nodes for contract expressions (forall/exists/old/result) and statements (ghost, contract_assert) and integrated them into traversal/printing/profiling.
• Added FunctionContractInfo / LoopContractInfo side tables in ASTContext and hooked parser output into them.
• Extended parsing (and some CodeGen skipping behavior) to accept contract constructs under the VerifyContracts language option.

Reviewed changes

Copilot reviewed 31 out of 31 changed files in this pull request and generated 13 comments.

Show a summary per file

File	Description
clang/lib/Sema/SemaContract.cpp	Adds a placeholder TU for future contract-specific semantic checks.
clang/lib/Sema/CMakeLists.txt	Builds the new SemaContract.cpp.
clang/lib/Parse/ParseStmt.cpp	Parses ghost/contract_assert statements and loop contract clauses; stores loop contracts.
clang/lib/Parse/Parser.cpp	Parses function contract clauses (pre/post/decreases) and stores function contract info.
clang/lib/Parse/ParseExpr.cpp	Parses contract expressions (forall/exists/old/result) and constructs new AST nodes.
clang/lib/Parse/ParseDecl.cpp	Accepts spec/proof as declaration specifiers (currently mapped onto inline).
clang/lib/CodeGen/CGStmt.cpp	Skips emitting ghost/contract statements in generic statement emission.
clang/lib/CodeGen/CGExprScalar.cpp	Adds scalar emission hooks for contract expressions (currently returns poison).
clang/lib/AST/StmtProfile.cpp	Adds profiling visitor hooks for new contract nodes.
clang/lib/AST/StmtPrinter.cpp	Adds pretty-printing for new contract nodes.
clang/lib/AST/StmtContract.cpp	Adds a TU for contract statement nodes (currently header-only).
clang/lib/AST/Stmt.cpp	Pulls in contract node headers for AST infrastructure compilation units.
clang/lib/AST/ItaniumMangle.cpp	Includes contract headers (integration plumbing).
clang/lib/AST/ExprContract.cpp	Adds a TU for contract expression nodes (currently header-only).
clang/lib/AST/ExprConstant.cpp	Includes contract headers for constant evaluation plumbing.
clang/lib/AST/ExprClassification.cpp	Includes contract headers for expression classification plumbing.
clang/lib/AST/Expr.cpp	Includes contract headers for expression implementation plumbing.
clang/lib/AST/DynamicRecursiveASTVisitor.cpp	Includes contract headers for dynamic visitor plumbing.
clang/lib/AST/CMakeLists.txt	Builds the new ExprContract.cpp / StmtContract.cpp.
clang/lib/AST/ASTTypeTraits.cpp	Includes contract headers for type-traits / dyn-node plumbing.
clang/lib/AST/ASTStructuralEquivalence.cpp	Includes contract headers for structural equivalence plumbing.
clang/lib/AST/ASTContext.cpp	Implements side-table accessors for function/loop contract info.
clang/include/clang/Parse/Parser.h	Declares contract parsing helpers + parser state (InContractPostcondition, CurrentContractFunction).
clang/include/clang/Basic/StmtNodes.td	Registers new contract node kinds in the AST node hierarchy.
clang/include/clang/Basic/DiagnosticSemaKinds.td	Adds new (currently mostly unused) contract-related semantic diagnostics.
clang/include/clang/Basic/DiagnosticParseKinds.td	Adds new contract parsing diagnostics (some currently unused).
clang/include/clang/AST/StmtVisitor.h	Includes contract headers so visitors see new node declarations.
clang/include/clang/AST/StmtContract.h	Introduces AST node definitions for ContractAssertStmt and GhostBlockStmt.
clang/include/clang/AST/RecursiveASTVisitor.h	Includes contract headers so RAV can see new node declarations.
clang/include/clang/AST/ExprContract.h	Introduces AST node definitions for ForallExpr, ExistsExpr, OldExpr, ResultExpr.
clang/include/clang/AST/ASTContext.h	Introduces side-table structs and ASTContext storage/accessors for contract metadata.

[Copilot]

Pull request overview

Copilot reviewed 45 out of 46 changed files in this pull request and generated 7 comments.

Comments suppressed due to low confidence (1)

clang/include/clang/Sema/DeclSpec.h:658

• ClearFunctionSpecs() does not reset the newly added FS_spec_specified / FS_proof_specified bits. If a DeclSpec instance is reused/cleared between declarations, these flags can leak into subsequent declarations and incorrectly mark later functions as spec/proof. Update ClearFunctionSpecs() to also clear both flags (and any associated locations, if added later).

  void ClearFunctionSpecs() {
    FS_inline_specified = false;
    FS_inlineLoc = SourceLocation();
    FS_forceinline_specified = false;
    FS_forceinlineLoc = SourceLocation();
    FS_virtual_specified = false;
    FS_virtualLoc = SourceLocation();
    FS_explicit_specifier = ExplicitSpecifier();
    FS_explicitLoc = SourceLocation();
    FS_explicitCloseParenLoc = SourceLocation();
    FS_noreturn_specified = false;
    FS_noreturnLoc = SourceLocation();
  }

[Copilot]

VisitWhileStmt overrides the base dumper but never calls the base traversal, so regular while-statement children (condition/body) will not be dumped when an ASTContext is present, and while statements without contract info may disappear entirely from -ast-dump. Call the base VisitWhileStmt first (or unconditionally), then append side-table invariant/decreases nodes.

[Copilot]

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]

Postconditions are parsed before ActOnStartOfFunctionDef creates the FunctionDecl, but ParseResultExpr relies on CurrentContractFunction to determine the return type. This means 'result' in post(...) will currently get the fallback type (int), losing the intended basic type information for non-int return types. Consider setting the current function return type (or a temporary FunctionDecl/QualType) before parsing postconditions, or delaying postcondition parsing until after the FunctionDecl exists.

[Copilot]

CurrentContractFunction is set when storing function contract info but is never reset. This can leak the previous function into subsequent parsing, causing 'result' to pick up the wrong return type (or be accepted unexpectedly) outside of contract contexts. Save/restore this member (RAII) around the contract parsing / function body parse so it is cleared when leaving ParseFunctionDefinition.

[Copilot]

ParseOldExpr does not enforce the intended context restrictions (postconditions / proof bodies). With -fverify-contracts enabled, using 'old(...)' in normal code will still parse into an OldExpr, and CodeGen currently emits a poison value for it, potentially leading to miscompiles/UB instead of a diagnostic. Emit diag::err_old_outside_postcondition (and recover appropriately) when !InContractPostcondition (and not in any other explicitly-allowed context).

[Copilot]

ParseResultExpr does not enforce that 'result' is only valid in postconditions, and silently falls back to int when CurrentContractFunction is null. With -fverify-contracts, this allows 'result' in normal code and then CodeGen emits a poison value, which is unsafe. Diagnose (diag::err_result_outside_postcondition) when !InContractPostcondition and avoid the IntTy fallback by requiring a known return type.

[Copilot]

This RUN line writes output to /dev/null, which is not portable to Windows test bots. Use %t (or -o -) for the output path so the test is platform-independent.

[Copilot]

Pull request overview

Copilot reviewed 45 out of 46 changed files in this pull request and generated 6 comments.

[Copilot]

Pull request overview

Copilot reviewed 46 out of 47 changed files in this pull request and generated 8 comments.

Comments suppressed due to low confidence (1)

clang/include/clang/Sema/DeclSpec.h:658

• ClearFunctionSpecs() doesn’t reset the newly added FS_spec_specified / FS_proof_specified bits. DeclSpec instances get reused while parsing, so leaving these set can cause spec/proof to “leak” onto subsequent declarations (and also makes setFunctionSpecInline behavior surprising). Extend ClearFunctionSpecs() to clear both flags (and any associated locations if you later add them).

  void ClearFunctionSpecs() {
    FS_inline_specified = false;
    FS_inlineLoc = SourceLocation();
    FS_forceinline_specified = false;
    FS_forceinlineLoc = SourceLocation();
    FS_virtual_specified = false;
    FS_virtualLoc = SourceLocation();
    FS_explicit_specifier = ExplicitSpecifier();
    FS_explicitLoc = SourceLocation();
    FS_explicitCloseParenLoc = SourceLocation();
    FS_noreturn_specified = false;
    FS_noreturnLoc = SourceLocation();
  }