Merge pull request #2 from SwayamInSync/contract-keywords

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

Author: SwayamInSync

README.md

@@ -1,44 +1,102 @@
-# The LLVM Compiler Infrastructure
+# CppVerify - Extending C++ to support Program Verification using SMT solvers
 
-[![OpenSSF Scorecard](https://api.securityscorecards.dev/projects/github.com/llvm/llvm-project/badge)](https://securityscorecards.dev/viewer/?uri=github.com/llvm/llvm-project)
-[![OpenSSF Best Practices](https://www.bestpractices.dev/projects/8273/badge)](https://www.bestpractices.dev/projects/8273)
-[![libc++](https://github.com/llvm/llvm-project/actions/workflows/libcxx-build-and-test.yaml/badge.svg?branch=main&event=schedule)](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** |

clang/include/clang/Basic/IdentifierTable.h

@@ -78,7 +78,8 @@ enum TokenKey : unsigned {
   KEYHLSL = 0x8000000,
   KEYFIXEDPOINT = 0x10000000,
   KEYDEFERTS = 0x20000000,
-  KEYMAX = KEYDEFERTS, // The maximum key
+  KEYCONTRACT = 0x40000000, // Keywords enabled by -fverify-contracts
+  KEYMAX = KEYCONTRACT, // The maximum key
   KEYALLCXX = KEYCXX | KEYCXX11 | KEYCXX20,
   KEYALL = (KEYMAX | (KEYMAX - 1)) & ~KEYNOMS18 & ~KEYNOOPENCL &
            ~KEYNOZOS // KEYNOMS18, KEYNOOPENCL, KEYNOZOS are excluded.

clang/include/clang/Basic/LangOptions.def

@@ -427,6 +427,8 @@ VALUE_LANGOPT(FunctionAlignment, 5, 0, Compatible, "Default alignment for functi
 VALUE_LANGOPT(LoopAlignment, 32, 0, Compatible, "Default alignment for loops")
 
 LANGOPT(FixedPoint, 1, 0, NotCompatible, "fixed point types")
+
+LANGOPT(VerifyContracts, 1, 0, NotCompatible, "CppVerify contract verification")
 LANGOPT(PaddingOnUnsignedFixedPoint, 1, 0, NotCompatible,
         "unsigned fixed point types having one extra padding bit")
 

clang/include/clang/Basic/TokenKinds.def

@@ -295,6 +295,7 @@ PUNCTUATOR(greatergreatergreater, ">>>")
 //                   extension.
 //   KEYDEFERTS - This is a keyword if the C '_Defer' TS is enabled
 //   KEYZOS - This is a keyword in C/C++ on z/OS
+//   KEYCONTRACT - This is a keyword if -fverify-contracts is enabled
 //
 KEYWORD(auto                        , KEYALL)
 KEYWORD(break                       , KEYALL)
@@ -445,6 +446,20 @@ C23_KEYWORD(typeof_unqual           , 0)
 // '_Defer' TS
 KEYWORD(_Defer                      , KEYDEFERTS)
 
+// CppVerify contract keywords (enabled by -fverify-contracts)
+KEYWORD(pre                         , KEYCONTRACT)
+KEYWORD(post                        , KEYCONTRACT)
+KEYWORD(invariant                   , KEYCONTRACT)
+KEYWORD(decreases                   , KEYCONTRACT)
+KEYWORD(ghost                       , KEYCONTRACT)
+KEYWORD(spec                        , KEYCONTRACT)
+KEYWORD(proof                       , KEYCONTRACT)
+KEYWORD(contract_assert             , KEYCONTRACT)
+KEYWORD(forall                      , KEYCONTRACT)
+KEYWORD(exists                      , KEYCONTRACT)
+KEYWORD(old                         , KEYCONTRACT)
+KEYWORD(result                      , KEYCONTRACT)
+
 // ISO/IEC JTC1 SC22 WG14 N1169 Extension
 KEYWORD(_Accum                      , KEYFIXEDPOINT)
 KEYWORD(_Fract                      , KEYFIXEDPOINT)

clang/include/clang/Options/Options.td

@@ -2366,6 +2366,13 @@ defm fixed_point : BoolFOption<"fixed-point",
   PosFlag<SetTrue, [], [ClangOption, CC1Option], "Enable">,
   NegFlag<SetFalse, [], [ClangOption], "Disable">,
   BothFlags<[], [ClangOption], " fixed point types">>;
+
+// CppVerify: deductive contract verification
+defm verify_contracts : BoolFOption<"verify-contracts",
+  LangOpts<"VerifyContracts">, DefaultFalse,
+  PosFlag<SetTrue, [], [ClangOption, CC1Option],
+          "Enable CppVerify contract syntax (pre/post/invariant/decreases/ghost/spec/proof)">,
+  NegFlag<SetFalse, [], [ClangOption], "Disable CppVerify contract syntax">>;
 def cxx_static_destructors_EQ : Joined<["-"], "fc++-static-destructors=">, Group<f_Group>,
   HelpText<"Controls which variables C++ static destructors are registered for">,
   Values<"all,thread-local,none">,

clang/lib/Basic/IdentifierTable.cpp

@@ -166,6 +166,8 @@ static KeywordStatus getKeywordStatusHelper(const LangOptions &LangOpts,
     return LangOpts.FixedPoint ? KS_Enabled : KS_Disabled;
   case KEYDEFERTS:
     return LangOpts.DeferTS ? KS_Enabled : KS_Disabled;
+  case KEYCONTRACT:
+    return LangOpts.VerifyContracts ? KS_Enabled : KS_Disabled;
   default:
     llvm_unreachable("Unknown KeywordStatus flag");
   }

clang/lib/Driver/ToolChains/Clang.cpp

@@ -6365,6 +6365,9 @@ void Clang::ConstructJob(Compilation &C, const JobAction &JA,
   Args.addOptInFlag(CmdArgs, options::OPT_ffixed_point,
                     options::OPT_fno_fixed_point);
 
+  Args.addOptInFlag(CmdArgs, options::OPT_fverify_contracts,
+                    options::OPT_fno_verify_contracts);
+
   if (Arg *A = Args.getLastArg(options::OPT_fcxx_abi_EQ))
     A->render(Args, CmdArgs);
 

clang/test/Driver/verify_contracts.cpp

@@ -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"

clang/test/Lexer/verify_contracts_keywords.cpp

@@ -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