Skip to content

Extend clang lexer to support contract-keywords and gate behind -fverify-contracts - #2

Merged
SwayamInSync merged 2 commits into
mainfrom
contract-keywords
Apr 9, 2026
Merged

SwayamInSync merged 2 commits into
mainfrom
contract-keywords

Conversation

@SwayamInSync

Copy link
Copy Markdown
Owner

Summary

Extends Clang with first-class contract syntax keywords for deductive verification, gated behind the -fverify-contracts flag.

Changes

  • Add new keywords to TokenKinds.def: pre, post, invariant, decreases, ghost, spec_fn, proof_fn
  • Gate keywords with KEYCONTRACT flag, only active when -fverify-contracts is passed
  • Add -fverify-contracts / -fno-verify-contracts driver and CC1 flags
  • Add VerifyContracts to LangOptions
  • Update IdentifierTable to handle contract keyword registration
  • Add driver test (verify_contracts.cpp) and lexer test (verify_contracts_keywords.cpp)

Design

Keywords are invisible to normal compilation — they remain plain identifiers unless -fverify-contracts is explicitly passed. This ensures zero impact on existing C++ code.

@SwayamInSync SwayamInSync changed the title Add contract keywords and gate behind -fverify-contracts Extend clang lexer to support contract-keywords and gate behind -fverify-contracts Apr 9, 2026
@SwayamInSync
SwayamInSync requested a review from Copilot April 9, 2026 07:48

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Pull request overview

Extends Clang’s lexer/identifier handling to recognize a set of “contract” keywords only when -fverify-contracts is enabled, and wires the new flag through the driver/cc1 along with targeted tests.

Changes:

  • Add KEYCONTRACT gating and register new contract keywords in TokenKinds.def.
  • Introduce LangOptions::VerifyContracts and connect keyword enablement to it via IdentifierTable.
  • Add -fverify-contracts driver forwarding plus new driver/lexer tests.

Reviewed changes

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

Show a summary per file
File Description
clang/test/Lexer/verify_contracts_keywords.cpp Verifies keyword-vs-identifier lexing behavior with and without -fverify-contracts.
clang/test/Driver/verify_contracts.cpp Ensures -fverify-contracts is forwarded to cc1 and is absent by default.
clang/lib/Driver/ToolChains/Clang.cpp Forwards -fverify-contracts to cc1 using opt-in flag handling.
clang/lib/Basic/IdentifierTable.cpp Enables/disables KEYCONTRACT keywords based on LangOptions::VerifyContracts.
clang/include/clang/Options/Options.td Defines -fverify-contracts and maps it to LangOptions::VerifyContracts.
clang/include/clang/Basic/TokenKinds.def Adds KEYCONTRACT and the contract keyword list.
clang/include/clang/Basic/LangOptions.def Introduces the VerifyContracts language option.
clang/include/clang/Basic/IdentifierTable.h Adds the KEYCONTRACT token key bit and updates KEYMAX.

Comment thread clang/include/clang/Basic/TokenKinds.def
Comment thread clang/include/clang/Options/Options.td
Comment thread README.md
```

## Getting the Source Code and Building LLVM
## Contract syntax reference

Copy link
Copy Markdown
Owner Author

Choose a reason for hiding this comment

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

We could've also added the build instructions but since the scope is limited of this PR (just lexer support) so to avoid confusion those can be happen at later mature stages

@SwayamInSync
SwayamInSync merged commit ba14ff9 into main Apr 9, 2026
6 checks passed
@SwayamInSync

Copy link
Copy Markdown
Owner Author

Also in a follow-up, it might be better to rename ghost {...} block to something like proof block?

@SwayamInSync
SwayamInSync deleted the contract-keywords branch April 14, 2026 07:37
SwayamInSync added a commit that referenced this pull request Jul 27, 2026
Extend clang lexer to support contract-keywords and gate behind `-fverify-contracts`
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants