Member operators, own-object returns, and class invariants at reference and pointer parameters

clang/lib/Verify/Frontend/ASTConverter.h

@@ -89,6 +89,12 @@ class ASTConverter {
   /// address parameter, by the synthetic parameter of the field's entry value
   /// (VFunction::FieldParams).
   std::map<const Expr *, std::string> FieldExtentParameters;
+  /// Converting a clause where an extent marker states nothing (a class
+  /// invariant at exit): each marker is true.
+  bool DropExtentMarkers = false;
+  /// The object `this` stands for while a class invariant is instantiated
+  /// for a parameter: the pointer or reference that addresses it.
+  const VExpr *ThisSubstitute = nullptr;
   std::set<const VarDecl *> GhostLocals;
   unsigned DynamicProvenanceId = 0;
   unsigned DynamicPointerAssignmentId = 0;
@@ -231,6 +237,18 @@ class ASTConverter {
                                   const VExpr *Base, uint64_t Offset,
                                   SourceLocation Loc,
                                   std::vector<std::unique_ptr<VStmt>> &Out);
+  /// The member initializers of a constructor, in the order they run, on
+  /// the object at Base + Offset.
+  bool appendMemberInitializers(const CXXConstructorDecl *Ctor,
+                                const VExpr *Base, uint64_t Offset,
+                                SourceLocation Loc,
+                                std::vector<std::unique_ptr<VStmt>> &Out);
+  /// Runs a constructor on the object at Base + Offset: a call of one the
+  /// class provides, else its members' initializers.
+  bool appendConstruction(const CXXConstructExpr *Construct, QualType Ty,
+                          const VExpr *Base, uint64_t Offset,
+                          SourceLocation Loc,
+                          std::vector<std::unique_ptr<VStmt>> &Out);
   bool appendObjectZeroInitialization(QualType Ty, const VExpr *Base,
                                       uint64_t Offset, SourceLocation Loc,
                                       std::vector<std::unique_ptr<VStmt>> &Out);
@@ -286,6 +304,13 @@ class ASTConverter {
                                                 std::string Provenance = "");
   bool appendRecordCallArgument(const Expr *E, const ParmVarDecl *Formal,
                                 std::vector<std::unique_ptr<VExpr>> &Args);
+  /// The fields of a record value that is kept in memory, a local object or
+  /// one a pointer or reference addresses, each read where it is: nothing
+  /// when E is no such record, false after an error.
+  std::optional<bool> recordFieldsInMemory(
+      const Expr *E, SourceLocation Loc,
+      std::vector<std::pair<const FieldDecl *, std::unique_ptr<VExpr>>>
+          &Fields);
   std::unique_ptr<VExpr>
   convertAssignmentValue(const BinaryOperator *Assignment);
   void appendAssignment(const Expr *LHS, std::unique_ptr<VExpr> Value,
@@ -299,6 +324,9 @@ class ASTConverter {
   bool appendRecordCopy(const Expr *Source, const VarDecl *Target,
                         SourceLocation Loc,
                         std::vector<std::unique_ptr<VStmt>> &Out);
+  /// Reports a use of the reference a member function returns to its own
+  /// object, which is no value.
+  bool rejectOwnObjectUse(const Expr *E);
   bool appendRecordInitializer(const InitListExpr *Init, const VarDecl *Target,
                                SourceLocation Loc,
                                std::vector<std::unique_ptr<VStmt>> &Out);
@@ -351,8 +379,13 @@ class ASTConverter {
   /// of FCI's preconditions names a synthetic parameter for its entry value
   /// (VFunction::FieldParams), and returns them for the default
   /// separation.
-  std::vector<AddressEntry> collectFieldExtents(const FunctionContractInfo &FCI,
-                                                VFunction &Fn);
+  std::vector<AddressEntry>
+  collectFieldExtents(const FunctionContractInfo &FCI,
+                      llvm::ArrayRef<const Expr *> Invariants, VFunction &Fn);
+  std::vector<const Expr *> entryClassInvariants(const CXXMethodDecl *Method,
+                                                 bool Constructor) const;
+  std::vector<const Expr *> exitClassInvariants(const CXXMethodDecl *Method,
+                                                bool Constructor) const;
   void registerLayoutType(QualType QT, VFunction &Fn);
   void buildRecordLayout(QualType QT, VFunction &Fn);
   void buildArrayLayout(QualType QT, const ConstantArrayType *CAT,

clang/lib/Verify/IR/VStmt.cpp

@@ -199,6 +199,7 @@ VFunction verify::cloneVFunction(const VFunction &Fn) {
   Out.SourceVariables = Fn.SourceVariables;
   Out.ScalarReferenceParams = Fn.ScalarReferenceParams;
   Out.RecordParams = Fn.RecordParams;
+  Out.IsConstructor = Fn.IsConstructor;
   for (const auto &[Name, Field] : Fn.FieldParams)
     Out.FieldParams.emplace_back(Name, cloneVExpr(Field.get()));
   Out.ConstAddressParams = Fn.ConstAddressParams;

clang/lib/Verify/IR/VStmt.h

@@ -345,6 +345,9 @@ struct VFunction {
   /// [[cppverify::trusted]]: its contract is assumed and its body, if any,
   /// is not verified.
   bool IsTrusted = false;
+  /// A constructor: its object's lifetime begins at `this`, uninitialized,
+  /// and the body initializes every leaf of it.
+  bool IsConstructor = false;
   /// The declaration, for diagnostics about the function itself.
   SourceLocation DeclLoc;
   bool NeedsDecreasesCheck = false;

clang/lib/Verify/Transform/LoopUnroll.cpp

@@ -257,6 +257,7 @@ VFunction LoopUnroller::unroll(const VFunction &Fn, unsigned K) {
   Out.SourceVariables = Fn.SourceVariables;
   Out.ScalarReferenceParams = Fn.ScalarReferenceParams;
   Out.RecordParams = Fn.RecordParams;
+  Out.IsConstructor = Fn.IsConstructor;
   for (const auto &[Name, Field] : Fn.FieldParams)
     Out.FieldParams.emplace_back(Name, cloneVExpr(Field.get()));
   Out.ConstAddressParams = Fn.ConstAddressParams;