-
Notifications
You must be signed in to change notification settings - Fork 0
Extend clang lexer to support contract-keywords and gate behind -fverify-contracts
#2
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
2 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,44 +1,102 @@ | ||
| # The LLVM Compiler Infrastructure | ||
| # CppVerify - Extending C++ to support Program Verification using SMT solvers | ||
|
|
||
| [](https://securityscorecards.dev/viewer/?uri=github.com/llvm/llvm-project) | ||
| [](https://www.bestpractices.dev/projects/8273) | ||
| [](https://github.com/llvm/llvm-project/actions/workflows/libcxx-build-and-test.yaml?query=event%3Aschedule) | ||
| > [!CAUTION] | ||
| > **Work in progress** — only lexer support is implemented so far. The verifier is not yet functional. | ||
|
|
||
| Welcome to the LLVM project! | ||
| > This is a fork of [LLVM/Clang](https://github.com/llvm/llvm-project) (pinned to | ||
| > `llvmorg-22.1.3`) extended with **CppVerify**: a deductive verification system | ||
| > for C++ built directly into the Clang frontend. | ||
|
|
||
| This repository contains the source code for LLVM, a toolkit for the | ||
| construction of highly optimized compilers, optimizers, and run-time | ||
| environments. | ||
| CppVerify adds first-class contract syntax (`pre`, `post`, `invariant`, | ||
| `decreases`, `ghost`, `spec`, `proof`) to C++, type-checked by Clang Sema and | ||
| discharged by Z3 via a weakest-precondition calculus backend. It occupies an | ||
| entirely uncontested niche: the only deductive verifier for modern C++ built on | ||
| Clang, with native contract syntax rather than comments or macros. | ||
|
|
||
| The LLVM project has multiple components. The core of the project is | ||
| itself called "LLVM". This contains all of the tools, libraries, and header | ||
| files needed to process intermediate representations and convert them into | ||
| object files. Tools include an assembler, disassembler, bitcode analyzer, and | ||
| bitcode optimizer. | ||
| ## What it looks like | ||
|
|
||
| C-like languages use the [Clang](https://clang.llvm.org/) frontend. This | ||
| component compiles C, C++, Objective-C, and Objective-C++ code into LLVM bitcode | ||
| -- and from there into object files, using LLVM. | ||
| ```cpp | ||
| spec int fibo(int n) decreases(n) { | ||
| if (n <= 1) return n; | ||
| return fibo(n - 1) + fibo(n - 2); | ||
| } | ||
|
|
||
| Other components include: | ||
| the [libc++ C++ standard library](https://libcxx.llvm.org), | ||
| the [LLD linker](https://lld.llvm.org), and more. | ||
| int safe_fib(int n) | ||
| pre(n >= 0) | ||
| pre(n <= 45) | ||
| post(result == fibo(n)) | ||
| { | ||
| if (n <= 1) return n; | ||
| int a = 0, b = 1, i = 2; | ||
| while (i <= n) | ||
| invariant(2 <= i && i <= n + 1) | ||
| invariant(b == fibo(i - 1)) | ||
| decreases(n - i + 1) | ||
| { | ||
| int tmp = a + b; | ||
| a = b; | ||
| b = tmp; | ||
| i++; | ||
| } | ||
| return b; | ||
| } | ||
| ``` | ||
|
|
||
| ## Getting the Source Code and Building LLVM | ||
| ## Contract syntax reference | ||
|
|
||
| Consult the | ||
| [Getting Started with LLVM](https://llvm.org/docs/GettingStarted.html#getting-the-source-code-and-building-llvm) | ||
| page for information on building and running LLVM. | ||
| | Syntax | Where | Meaning | | ||
| | ------------------------- | --------------------------------- | -------------------------------------------------------------------- | | ||
| | `pre(expr)` | After function `)` | Precondition — caller must satisfy | | ||
| | `post(expr)` | After function `)` | Postcondition — callee must establish; may use `result` and `old(x)` | | ||
| | `invariant(expr)` | After `while`/`for` condition `)` | Loop invariant | | ||
| | `decreases(expr)` | After `while`/`for` condition `)` | Termination measure | | ||
| | `ghost { ... }` | Statement | Ghost block — proof steps, stripped by CodeGen | | ||
| | `contract_assert(expr)` | Statement | Verification condition (not a runtime check) | | ||
| | `spec T f(...)` | Declaration | Pure spec function — interpreted by verifier only | | ||
| | `proof void f(...)` | Declaration | Ghost proof function — establishes lemmas | | ||
| | `forall(i, lo, hi, expr)` | Expression | Bounded universal quantifier | | ||
| | `exists(i, lo, hi, expr)` | Expression | Bounded existential quantifier | | ||
| | `old(expr)` | Inside `post` | Value of `expr` at function entry | | ||
| | `result` | Inside `post` | Return value of the enclosing function | | ||
|
|
||
| For information on how to contribute to the LLVM project, please take a look at | ||
| the [Contributing to LLVM](https://llvm.org/docs/Contributing.html) guide. | ||
| 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. | ||
|
|
||
| ## Getting in touch | ||
| ## Architecture | ||
|
|
||
| Join the [LLVM Discourse forums](https://discourse.llvm.org/), [Discord | ||
| chat](https://discord.gg/xS7Z362), | ||
| [LLVM Office Hours](https://llvm.org/docs/GettingInvolved.html#office-hours) or | ||
| [Regular sync-ups](https://llvm.org/docs/GettingInvolved.html#online-sync-ups). | ||
| ``` | ||
| C++ source with contracts | ||
| │ | ||
| ▼ | ||
| Clang Frontend (modified Parser + Sema + AST) | ||
| │ Annotated AST with contract nodes | ||
| ▼ | ||
| ASTConverter (Clang AST → Layer 1 VCR IR) | ||
| │ Typed, control-flow-preserving IR | ||
| ▼ | ||
| Passivize (Layer 1 → Layer 2 SSA) | ||
| │ Havoc / assume / assert, no loops | ||
| ▼ | ||
| WP Calculus (weakest precondition, backward pass) | ||
| │ Verification conditions | ||
| ▼ | ||
| Z3 Encoding (VCs → Z3 formulas, check UNSAT) | ||
| │ sat / unsat / unknown | ||
| ▼ | ||
| Diagnostics (Clang-style errors + counterexamples) | ||
| ``` | ||
|
|
||
| The LLVM project has adopted a [code of conduct](https://llvm.org/docs/CodeOfConduct.html) for | ||
| participants to all modes of communication within the project. | ||
| Normal compilation skips everything after the frontend: CodeGen simply ignores | ||
| all ghost/contract AST nodes. | ||
|
|
||
| ## Competitive landscape | ||
|
|
||
| | Tool | Frontend | C++ support | Contract syntax | | ||
| | ------------- | --------------------- | -------------- | --------------- | | ||
| | Frama-C | Custom OCaml | Prototype only | ACSL comments | | ||
| | VCC | Custom | C only (dead) | Macros | | ||
| | VeriFast | Custom | No | Comments | | ||
| | CBMC | Custom goto-cc | Partial | Assertions only | | ||
| | Verus | Rust compiler | No (Rust only) | First-class | | ||
| | **CppVerify** | **Clang (this fork)** | **Native** | **First-class** | | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,18 @@ | ||
| // Test that -fverify-contracts is forwarded from the driver to cc1, and that | ||
| // the flag is absent by default (or when -fno-verify-contracts is given). | ||
|
|
||
| // RUN: %clang -### -std=c++20 -fverify-contracts %s 2>&1 \ | ||
| // RUN: | FileCheck %s --check-prefix=WITH | ||
|
|
||
| // RUN: %clang -### -std=c++20 %s 2>&1 \ | ||
| // RUN: | FileCheck %s --check-prefix=OFF | ||
|
|
||
| // RUN: %clang -### -std=c++20 -fno-verify-contracts %s 2>&1 \ | ||
| // RUN: | FileCheck %s --check-prefix=OFF | ||
|
|
||
| // -fverify-contracts must appear in the cc1 invocation. | ||
| // WITH: "-fverify-contracts" | ||
|
|
||
| // Without the flag (or with the explicit negation), neither form is forwarded. | ||
| // OFF-NOT: "-fverify-contracts" | ||
| // OFF-NOT: "-fno-verify-contracts" |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,114 @@ | ||
| // Verify that all 12 KEYCONTRACT keywords are lexed correctly. | ||
| // | ||
| // With -fverify-contracts: each name lexes as a keyword token. | ||
| // Without -fverify-contracts: each name lexes as an identifier (no conflict | ||
| // with existing C++ code). | ||
|
|
||
| // --- dump-tokens: WITH flag — expect keyword tokens --- | ||
| // RUN: %clang_cc1 -std=c++20 -fverify-contracts -dump-tokens %s 2>&1 \ | ||
| // RUN: | FileCheck %s --check-prefix=KW | ||
|
|
||
| // --- dump-tokens: WITHOUT flag — expect identifier tokens --- | ||
| // RUN: %clang_cc1 -std=c++20 -dump-tokens %s 2>&1 \ | ||
| // RUN: | FileCheck %s --check-prefix=ID | ||
|
|
||
| // --- __is_identifier: WITH flag (-DWITH_FLAG selects the right assertions) --- | ||
| // RUN: %clang_cc1 -std=c++20 -fverify-contracts -DWITH_FLAG -fsyntax-only %s | ||
|
|
||
| // --- __is_identifier: WITHOUT flag --- | ||
| // RUN: %clang_cc1 -std=c++20 -fsyntax-only %s | ||
|
|
||
| // ========================================================================== | ||
| // Section 1: FileCheck patterns for dump-tokens runs | ||
| // | ||
| // dump-tokens is lex-only; syntax does not matter. The tokens that satisfy | ||
| // these checks come from the variable declarations in Section 3, which are | ||
| // compiled by every dump-tokens run (neither run defines WITH_FLAG). | ||
| // | ||
| // KW-DAG checks that each name appears as a keyword token. | ||
| // ID-DAG checks that each name appears as an identifier token. | ||
| // ========================================================================== | ||
|
|
||
| // KW-DAG: pre 'pre' | ||
| // KW-DAG: post 'post' | ||
| // KW-DAG: invariant 'invariant' | ||
| // KW-DAG: decreases 'decreases' | ||
| // KW-DAG: ghost 'ghost' | ||
| // KW-DAG: spec 'spec' | ||
| // KW-DAG: proof 'proof' | ||
| // KW-DAG: contract_assert 'contract_assert' | ||
| // KW-DAG: forall 'forall' | ||
| // KW-DAG: exists 'exists' | ||
| // KW-DAG: old 'old' | ||
| // KW-DAG: result 'result' | ||
|
|
||
| // ID-DAG: identifier 'pre' | ||
| // ID-DAG: identifier 'post' | ||
| // ID-DAG: identifier 'invariant' | ||
| // ID-DAG: identifier 'decreases' | ||
| // ID-DAG: identifier 'ghost' | ||
| // ID-DAG: identifier 'spec' | ||
| // ID-DAG: identifier 'proof' | ||
| // ID-DAG: identifier 'contract_assert' | ||
| // ID-DAG: identifier 'forall' | ||
| // ID-DAG: identifier 'exists' | ||
| // ID-DAG: identifier 'old' | ||
| // ID-DAG: identifier 'result' | ||
|
|
||
| // ========================================================================== | ||
| // Section 2: __is_identifier() static assertions | ||
| // | ||
| // __is_identifier(X) is a preprocessor built-in: it expands to 0 or 1 | ||
| // *before* the C++ parser runs, so the parser never sees the keyword token | ||
| // inside the parens. The result is a pure integer literal. | ||
| // | ||
| // WITH_FLAG → -fverify-contracts active → all 12 are keywords → expect 0 | ||
| // !WITH_FLAG → flag absent → all 12 are identifiers → expect 1 | ||
| // ========================================================================== | ||
|
|
||
| #ifdef WITH_FLAG | ||
| static_assert(!__is_identifier(pre), "pre must be a keyword with -fverify-contracts"); | ||
| static_assert(!__is_identifier(post), "post must be a keyword with -fverify-contracts"); | ||
| static_assert(!__is_identifier(invariant), "invariant must be a keyword with -fverify-contracts"); | ||
| static_assert(!__is_identifier(decreases), "decreases must be a keyword with -fverify-contracts"); | ||
| static_assert(!__is_identifier(ghost), "ghost must be a keyword with -fverify-contracts"); | ||
| static_assert(!__is_identifier(spec), "spec must be a keyword with -fverify-contracts"); | ||
| static_assert(!__is_identifier(proof), "proof must be a keyword with -fverify-contracts"); | ||
| static_assert(!__is_identifier(contract_assert), "contract_assert must be a keyword with -fverify-contracts"); | ||
| static_assert(!__is_identifier(forall), "forall must be a keyword with -fverify-contracts"); | ||
| static_assert(!__is_identifier(exists), "exists must be a keyword with -fverify-contracts"); | ||
| static_assert(!__is_identifier(old), "old must be a keyword with -fverify-contracts"); | ||
| static_assert(!__is_identifier(result), "result must be a keyword with -fverify-contracts"); | ||
| #else | ||
| // ========================================================================== | ||
| // Section 3: identifier-mode checks + token source for dump-tokens runs | ||
| // | ||
| // This block is compiled by: | ||
| // - the two dump-tokens runs (no WITH_FLAG defined) | ||
| // - the fsyntax-only run WITHOUT -fverify-contracts | ||
| // | ||
| // The variable declarations give dump-tokens the tokens to match against. | ||
| // The static_assert lines verify backward compatibility. | ||
| // ========================================================================== | ||
|
|
||
| // Backward compatibility: all names remain valid C++ identifiers. | ||
| static_assert(__is_identifier(pre), "pre must be an identifier without -fverify-contracts"); | ||
| static_assert(__is_identifier(post), "post must be an identifier without -fverify-contracts"); | ||
| static_assert(__is_identifier(invariant), "invariant must be an identifier without -fverify-contracts"); | ||
| static_assert(__is_identifier(decreases), "decreases must be an identifier without -fverify-contracts"); | ||
| static_assert(__is_identifier(ghost), "ghost must be an identifier without -fverify-contracts"); | ||
| static_assert(__is_identifier(spec), "spec must be an identifier without -fverify-contracts"); | ||
| static_assert(__is_identifier(proof), "proof must be an identifier without -fverify-contracts"); | ||
| static_assert(__is_identifier(contract_assert), "contract_assert must be an identifier without -fverify-contracts"); | ||
| static_assert(__is_identifier(forall), "forall must be an identifier without -fverify-contracts"); | ||
| static_assert(__is_identifier(exists), "exists must be an identifier without -fverify-contracts"); | ||
| static_assert(__is_identifier(old), "old must be an identifier without -fverify-contracts"); | ||
| static_assert(__is_identifier(result), "result must be an identifier without -fverify-contracts"); | ||
|
|
||
| // Declarations whose names produce the keyword/identifier tokens that the | ||
| // dump-tokens FileCheck patterns match against. With -fverify-contracts each | ||
| // name lexes as its keyword token; without it, as an identifier token. | ||
| // (dump-tokens is lex-only so no parse error occurs in either case.) | ||
| int pre, post, invariant, decreases, ghost, spec, proof; | ||
| int contract_assert, forall, exists, old, result; | ||
| #endif |
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
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