[clang] [Clang] [Contracts] Design Doc (PR #229978)

via cfe-commits cfe-commits at lists.llvm.org
Sun Oct 25 15:11:39 PDT 2026


================
@@ -0,0 +1,943 @@
+# Introduction
+
+This is a high level design documentation for Contracts implementation in Clang.
+This summarized experiences from several implementors in seperate branches.
+
+This is also tend to be some developer policy/guide of contracts for how should clang
+developers continue working on this.
+
+## High Level Developing Style
+
+We plan to implement contracts in different small PRs. We don't want to implement
+contracts in a single PR. Smaller PR helps reviewers to understand the patch and give
+higher quality reviewers. Samller PR is also easier for testers to test and find the
+problems.
+
+The implementation contracts is marked as experimental before we announce it is 
+implemented completely.
+
+### ABI
+
+We'd like to keep ABI unstable during the experimental process. We all understand
+ABI's importance. But getting consensus for ABI needs a long time. We prefer to
+move faster instead of waiting the consensus for ABI consensus.
+
+For GCC/libstdc++ interoperability, we need to identify the ABI revision
+which a toolchain targets. We shouldn't assume that one experimental GCC ABI
+will remain unchanged.
+
+### Driver flags
+
+Before we think the support of contracts are minimal usable, users are unable
+to get access to contracts unless users pass `-Xclang` explicitly. 
+
+## AST structure
+
+### Contract Stmt
+
+```C++
+class Stmt {
+
+class ContractStmtBitfields {
+    unsigned Invalid : 1;
+};
+};
+
+class ContractStmtBase : public Stmt {
+  Expr *Predicate = nullptr;
+  SourceLocation KeywordLoc, LParenLoc, RParenLoc;
+  // llvm::ArrayRef<const Attr *> Attributes; // The design allows contracts to have attributes but none
+                                              // contracts attribute are presenting right now.
+};
+
+class ContractAssertStmt : public ContractStmtBase {};
+
+class ContractPreStmt : public ContractStmtBase {};
+
+class ContractPostStmt : public ContractStmtBase {
+  ResultNameDecl *ResultName = nullptr;
+};
+```
+
+Discussion:
+
+We though to use a simple struct to represent `pre` and `post` contracts. But we decided to put all of
+them into Stmt system. The major reason is that now the users can reuse components like 
+`TraverseStmt(...)` more easily.
+
+For attributes, as we don't have any attributes for contracts yet, we can save this on first implemenation.
+
+We split them into 3 Stmt kinds so we can save the bits for ResultName for other contracts types.
+
+For `ResultNameDecl`, see following sections.
+
+### FunctionDecl
+
+```C++
+class FunctionContractSequence final
+    : private llvm::TrailingObjects<FunctionContractSequence, ContractStmtBase *> {
+  friend llvm::TrailingObjects<FunctionContractSequence, ContractStmtBase *>;
+  unsigned NumContracts;
+
+  explicit FunctionContractSequence(unsigned N) : NumContracts(N) {}
+
+public:
+  static FunctionContractSequence *Create(
+      ASTContext &Ctx, llvm::ArrayRef<ContractStmtBase *> Contracts);
+
+  llvm::ArrayRef<ContractStmtBase *> contracts() const {
+    return {getTrailingObjects<ContractStmtBase *>(), NumContracts};
+  }
+};
+
+class FunctionDecl : /*...*/ {
+  /*...*/
+private:
+  // The actual contracts of the function.
+  // Even if it is not explicitly written.
+  FunctionContractSequence *Contracts = nullptr;
+
+public:
+  bool hasContracts() const {
+    return Contracts;
+  }
+
+  void setContracts(FunctionContractSequence *ContractsSeq) {
+    Contracts = ContractsSeq;
+  }
+
+  const FunctionContractSequence *getContracts() const {
+    return Contracts;
+  }
+};
+```
+
+Discussion:
+
+We need to use a single sequence for the contracts of a function. e.g.,
+
+```C++
+int f(int x)
+  pre(x > 0)
+  post(r: r > 0);
+
+int f(int x)
+  post(r: r > 0)
+  pre(x > 0); // Illegal
+```
+
+So that we can't use a sequence for `pre` and another sequence for `post`.
+
+Another problem is that we allow redeclarations without contracts, or
+with semantically equal contracts. So
+
+```C++
+int func(int lhs, int rhs) pre(lhs != rhs); // FD1
+int func(int lhs1, int rhs1) { return lhs1 == rhs1; } // FD2
+```
+
+we should think the function declaration `int func(int lhs1, int rhs1)`
+(FD2) have the same contracts as the first one.
+Then it is a problem that how should we store/access the contracts for
+`FD2`.
+
+Usually, as this is related to redeclarations, we might think we can
+get it by iterating redecls. e.g.,
+
+```C++
+for (auto *RD : this->redecls())
+  if (auto *ContractSeq = RD->getContracts())
+    return ContractSeq;
+```
+
+But if we follow this, the contracts we get for `FD2` will be the contracts
+of `FD1`, `pre(lhs != rhs)`. While this is semantically correct,
+`FD2` doesn't have `lhs` or `rhs`. It is not only they have
+different name but they are actually different AST nodes.
+So it will be problematic for code generation or static analysis
+if we simply store the contracts to the declaration
+which the contracts are written.
+
+The simplest solution is that Sema to put the corresponding
+contracts on every function redeclaration.
+
+This means, **Sema is responsible to construct a new contract
+sequence when it saw a redeclaration if the first function has
+contracts, no matter if the redeclaration has contracts written
+or not**.
+
----------------
EricWF wrote:

This is the main design choice I'd push back on.

Our branch started out doing this: a `TreeTransform`ed copy of the first declaration's contracts, rebound to the definition's parameters. But I ripped that out.

I think the correct approach is to re-map the parameters during constant evaluation and codegen rather than rebuilding every time.

We want to keep the real  source location and parameter names in the diagnostics produced. It would be confusing if we emitted diagnostics with the parameter names used in a declaration that doesn't contain the contract.

It also wastes Sema work and serialized AST space on every redeclaration.




https://github.com/llvm/llvm-project/pull/229978


More information about the cfe-commits mailing list