================
@@ -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**.
+
+#### Possible Later Changes
+
+If needed, we can add `IsWritten` information to `FunctionContractSequence`
+to indicate if this sequence is written in source or not.
+This may be helpful for toolings.
+
+But in the first version, we don't have to do that.
+
+### ResultNameDecl
+
+A post contract can introduce a name to represent the return value of the
+function. e.g.,
+
+```C++
+int f(int x) post(result: result > x);
+```
+
+We introduce a new `ValueDecl` for this name.
+
+```C++
+class ResultNameDecl final : public ValueDecl {
----------------
ChuanqiXu9 wrote:
I am going to use `ContractResultBindingDecl` in next revision.
https://github.com/llvm/llvm-project/pull/229978
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
