verify: Bound pointers into a record by the array, field, or record they point into

clang/lib/Verify/CMakeLists.txt

@@ -31,6 +31,7 @@ add_clang_library(clangVerify
   Transform/Ownership.cpp
   Transform/LoopUnroll.cpp
   Transform/SpecInline.cpp
+  Transform/SubobjectBounds.cpp
   Transform/UBChecks.cpp
   Backend/Certify.cpp
   Backend/Presburger.cpp

clang/lib/Verify/Frontend/ASTConverter.cpp

@@ -1,6 +1,7 @@
 //===--- ASTConverter.cpp -------------------------------------------------===//
 #include "ASTConverter.h"
 #include "../Transform/Inductive.h"
+#include "../Transform/SubobjectBounds.h"
 #include "clang/AST/ASTContext.h"
 #include "clang/AST/Decl.h"
 #include "clang/AST/DeclCXX.h"
@@ -1164,6 +1165,16 @@ ASTConverter::convertPointerDifferenceOperand(const Expr *E,
                                               uint64_t PointeeSize) {
   if (!E || PointeeSize == 0)
     return nullptr;
+  // A pointer into a member array, or to a subobject, of the object a
+  // pointer addresses.
+  const Expr *Peeled = E->IgnoreParens();
+  if (const auto *Decay = dyn_cast<ImplicitCastExpr>(Peeled);
+      Decay && Decay->getCastKind() == CK_ArrayToPointerDecay &&
+      pointeeRootPointer(Decay->getSubExpr()))
+    return convertExpr(Peeled);
+  if (const auto *U = dyn_cast<UnaryOperator>(Peeled);
+      U && U->getOpcode() == UO_AddrOf && pointeeRootPointer(U->getSubExpr()))
+    return convertExpr(Peeled);
   E = E->IgnoreParenImpCasts();
   if (const auto *DRE = dyn_cast<DeclRefExpr>(E))
     if (isa<VarDecl>(DRE->getDecl()) && E->getType()->isPointerType())
@@ -2940,6 +2951,8 @@ ASTConverter::convertFunction(const FunctionDecl *FD) {
     for (auto &S : convertStmt(Body))
       Fn->Body.push_back(std::move(S));
     TrackInitialization = false;
+    for (const auto &[Loc, Message] : propagateSubobjectBounds(*Fn))
+      error(SourceRange(Loc), Fn->Name + ": " + Message);
     if (!DynamicPointerProvenanceVariables.empty()) {
       std::vector<std::pair<std::string, SourceLocation>> InitialProvenance;
       InitialProvenance.reserve(DynamicPointerProvenanceVariables.size());
@@ -3425,10 +3438,6 @@ std::string ASTConverter::arrayDecayError(const Expr *Array) const {
   const auto *M = dyn_cast_or_null<MemberExpr>(peelObjectExpr(Array));
   const std::string Member =
       M ? M->getMemberDecl()->getNameAsString() : std::string();
-  if (M && pointeeRootPointer(M))
-    return "a pointer to the array member '" + Member +
-           "' is unsupported; index the member where it is used, as in '" +
-           Member + "[i]'";
   if (const VarDecl *Root = selectionRootVar(Array);
       Root && Root->hasGlobalStorage()) {
     const std::string Kind = Root->isStaticLocal() ? "static local" : "global";
@@ -3441,6 +3450,63 @@ std::string ASTConverter::arrayDecayError(const Expr *Array) const {
          "lexical lifetime and escape effects are modeled";
 }
 
+std::unique_ptr<VExpr> ASTConverter::subobjectPointer(const Expr *E,
+                                                      const Expr *Object,
+                                                      bool AddressOf) {
+  const SourceLocation Loc = E->getExprLoc();
+  auto Place = objectPlace(Object);
+  if (!Place)
+    return nullptr;
+  auto AccessCondition = Place->takeAccessCondition();
+  auto Address = Place->takeAddress();
+  const VType PointerType = VType::fromQualType(E->getType(), IntMode, Ctx);
+  Address->Ty = PointerType;
+  // The bytes the pointer may address: the array it decays from or whose
+  // element it addresses, else the field or record it addresses. An element
+  // of the objects a pointer addresses (&p[i], &*p) is bounded by them.
+  const Expr *Bounding = nullptr;
+  const Expr *Peeled = peelObjectExpr(Object);
+  if (!AddressOf || isa<MemberExpr>(Peeled)) {
+    Bounding = Object;
+  } else if (const auto *AS = dyn_cast<ArraySubscriptExpr>(Peeled)) {
+    const Expr *Base = peelObjectExpr(AS->getBase());
+    if (Base && Base->getType()->isArrayType())
+      Bounding = Base;
+  }
+  std::unique_ptr<VExpr> Lo;
+  if (Bounding == Object) {
+    Lo = cloneVExpr(Address.get());
+  } else if (Bounding) {
+    auto Enclosing = objectPlace(Bounding);
+    if (!Enclosing)
+      return nullptr;
+    Lo = Enclosing->takeAddress();
+  }
+  // Only a statement can check the pointer and give it bounds; elsewhere,
+  // as in a condition or a contract, it is a value nothing reads through.
+  if (!SubobjectSink)
+    return Address;
+  if (AccessCondition)
+    SubobjectSink->push_back(std::make_unique<VAssertStmt>(
+        std::move(AccessCondition), Loc, ProofObligationKind::Bounds));
+  appendReferenceBindingCheck(Object, Address.get(), Loc, *SubobjectSink);
+  if (!Bounding)
+    return Address;
+  const uint64_t Size =
+      Ctx.getTypeSizeInChars(Bounding->getType()).getQuantity();
+  auto Hi = objectLeafAddress(Lo.get(), Size, Loc);
+  const std::string Name =
+      FormedSubobjectPrefix + std::to_string(++SubobjectPointerId);
+  SubobjectSink->push_back(
+      std::make_unique<VAssignStmt>(Name, std::move(Address), Loc));
+  SubobjectSink->push_back(
+      std::make_unique<VAssignStmt>(lowerBoundName(Name), std::move(Lo), Loc));
+  SubobjectSink->push_back(
+      std::make_unique<VAssignStmt>(upperBoundName(Name), std::move(Hi), Loc));
+  CurrentFn->BoundedPointers.insert(Name);
+  return std::make_unique<VVarExpr>(Name, PointerType, Loc);
+}
+
 const Expr *ASTConverter::pointeeRootPointer(const Expr *E) const {
   while (true) {
     E = peelObjectExpr(E);
@@ -4424,6 +4490,8 @@ std::unique_ptr<VExpr> ASTConverter::convertExprImpl(const Expr *E) {
     return convertExpr(MTE->getSubExpr());
   if (const auto *Decay = dyn_cast<CastExpr>(E);
       Decay && Decay->getCastKind() == CK_ArrayToPointerDecay) {
+    if (pointeeRootPointer(Decay->getSubExpr()))
+      return subobjectPointer(E, Decay->getSubExpr(), /*AddressOf=*/false);
     error(CurrentFn->Name + ": " + arrayDecayError(Decay->getSubExpr()));
     return nullptr;
   }
@@ -4602,6 +4670,8 @@ std::unique_ptr<VExpr> ASTConverter::convertExprImpl(const Expr *E) {
   }
   if (const auto *U = dyn_cast<UnaryOperator>(E)) {
     if (U->getOpcode() == UO_AddrOf) {
+      if (pointeeRootPointer(U->getSubExpr()))
+        return subobjectPointer(E, U->getSubExpr(), /*AddressOf=*/true);
       error(CurrentFn->Name +
             ": raw address-of is unsupported until lexical lifetime and escape "
             "effects are modeled");
@@ -6049,6 +6119,14 @@ ASTConverter::convertStmtBody(const Stmt *S) {
     leaveAutomaticScope(Out, CS->getRBracLoc());
     return Out;
   }
+  // A pointer to a subobject formed by this statement is checked and bounded
+  // before it; a condition only compares one.
+  llvm::SaveAndRestore Sink(SubobjectSink,
+                            (isa<DeclStmt, ReturnStmt>(S) || isa<Expr>(S)) &&
+                                    !InGhost && !CurrentFn->IsSpec &&
+                                    !CurrentFn->IsProof
+                                ? &Out
+                                : nullptr);
   if (S->getStmtClass() == Stmt::ReturnStmtClass) {
     if (InGhost) {
       error(CurrentFn->Name +

clang/lib/Verify/Frontend/ASTConverter.h

@@ -28,6 +28,11 @@ class ASTConverter {
   std::string ResultName = "result";
   VFunction *CurrentFn = nullptr;
   unsigned NestedCallId = 0;
+  /// Where the statement being lowered puts what forming a pointer to a
+  /// subobject needs (its checks and its bounds); null where the pointer is
+  /// only a value, as in a condition or a contract.
+  std::vector<std::unique_ptr<VStmt>> *SubobjectSink = nullptr;
+  unsigned SubobjectPointerId = 0;
   std::vector<ConversionError> Errors;
   /// The innermost declaration, statement, or expression being converted,
   /// where an error is reported unless it names a place of its own.
@@ -166,6 +171,12 @@ class ASTConverter {
   /// Why the decay of \p Array to a pointer is unsupported, in the terms of
   /// what the array is.
   std::string arrayDecayError(const Expr *Array) const;
+  /// A pointer to \p Object, a subobject of the object a pointer addresses:
+  /// the array \p E decays (AddressOf false) or the lvalue \p E takes the
+  /// address of. Bounded by the array it decays from or whose element it
+  /// addresses, else by the field or record it addresses.
+  std::unique_ptr<VExpr> subobjectPointer(const Expr *E, const Expr *Object,
+                                          bool AddressOf);
   /// The exact byte-offset place of a subobject, reached by field and
   /// fixed-array element selections from a promoted local or from the
   /// object a pointer addresses; each fixed-array index is bounded by its

clang/lib/Verify/IR/VStmt.cpp

@@ -186,6 +186,7 @@ VFunction verify::cloneVFunction(const VFunction &Fn) {
   Out.SourceVariables = Fn.SourceVariables;
   Out.ReferenceParams = Fn.ReferenceParams;
   Out.ConstAddressParams = Fn.ConstAddressParams;
+  Out.BoundedPointers = Fn.BoundedPointers;
   Out.ReturnFields = Fn.ReturnFields;
   Out.ExplicitPreconditionCount = Fn.ExplicitPreconditionCount;
   for (const auto &P : Fn.Preconditions)

clang/lib/Verify/IR/VStmt.h

@@ -402,6 +402,10 @@ struct VFunction {
   /// Pointer and reference parameters to const objects: the function
   /// writes nothing through them.
   std::set<std::string> ConstAddressParams;
+  /// Pointer variables that may address a subobject (a member array, a
+  /// field): each has companions `name.__lo` and `name.__hi`, the bytes it
+  /// may address, which every access and step through it must stay in.
+  std::set<std::string> BoundedPointers;
   std::vector<std::pair<std::string, VType>> ReturnFields;
   /// Number of leading preconditions originating from explicit pre clauses.
   unsigned ExplicitPreconditionCount = 0;

clang/lib/Verify/Transform/LoopUnroll.cpp

@@ -256,6 +256,7 @@ VFunction LoopUnroller::unroll(const VFunction &Fn, unsigned K) {
   Out.SourceVariables = Fn.SourceVariables;
   Out.ReferenceParams = Fn.ReferenceParams;
   Out.ConstAddressParams = Fn.ConstAddressParams;
+  Out.BoundedPointers = Fn.BoundedPointers;
   Out.ReturnFields = Fn.ReturnFields;
   Out.ExplicitPreconditionCount = Fn.ExplicitPreconditionCount;
   for (const auto &P : Fn.Preconditions)

clang/lib/Verify/Transform/Origins.cpp

@@ -7,6 +7,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "Origins.h"
+#include "SubobjectBounds.h"
 #include "UBChecks.h"
 #include "llvm/ADT/APInt.h"
 #include "llvm/ADT/SmallString.h"
@@ -149,14 +150,8 @@ class OriginAnalysis {
     }
     case VExpr::BinOp: {
       const auto *B = static_cast<const VBinOpExpr *>(E);
-      if (B->Op != VBinOp::Add && B->Op != VBinOp::Sub)
-        return std::nullopt;
-      const bool Left = B->Lhs->Ty.Kind == VTypeKind::Ptr;
-      const bool Right = B->Rhs->Ty.Kind == VTypeKind::Ptr;
-      if (Left && !Right)
-        return originsOf(B->Lhs.get(), S);
-      if (Right && !Left && B->Op == VBinOp::Add)
-        return originsOf(B->Rhs.get(), S);
+      if (const VExpr *Pointer = steppedPointer(*B))
+        return originsOf(Pointer, S);
       return std::nullopt;
     }
     case VExpr::Conditional: {
@@ -215,8 +210,10 @@ class OriginAnalysis {
     case VStmt::Assign: {
       auto &A = static_cast<VAssignStmt &>(Stmt);
       annotateIn(A.Value.get(), S);
+      // A bound companion holds an address no access goes through.
       if (S)
-        (*S)[A.Target] = A.Value && A.Value->Ty.Kind == VTypeKind::Ptr
+        (*S)[A.Target] = A.Value && A.Value->Ty.Kind == VTypeKind::Ptr &&
+                                 !isBoundCompanion(A.Target)
                              ? originsOf(A.Value.get(), *S)
                              : std::nullopt;
       return S;
@@ -551,6 +548,24 @@ std::unique_ptr<VExpr> verify::originIdentity(const std::string &Origin,
                                         identityType(), Loc);
 }
 
+const VExpr *verify::steppedPointer(const VBinOpExpr &B) {
+  if (B.Op != VBinOp::Add && B.Op != VBinOp::Sub)
+    return nullptr;
+  bool Left = B.Lhs->Ty.Kind == VTypeKind::Ptr;
+  bool Right = B.Rhs->Ty.Kind == VTypeKind::Ptr;
+  // A field offset is a constant of pointer type: in a sum of two pointers
+  // the constant is the offset.
+  if (Left && Right) {
+    Left = B.Rhs->K == VExpr::Literal;
+    Right = !Left && B.Lhs->K == VExpr::Literal;
+  }
+  if (Left && !Right)
+    return B.Lhs.get();
+  if (Right && !Left && B.Op == VBinOp::Add)
+    return B.Rhs.get();
+  return nullptr;
+}
+
 std::optional<std::vector<std::string>> verify::pointerOrigins(const VExpr *E) {
   if (!E)
     return std::nullopt;
@@ -568,15 +583,9 @@ std::optional<std::vector<std::string>> verify::pointerOrigins(const VExpr *E) {
   case VExpr::Cast:
     return pointerOrigins(static_cast<const VCastExpr *>(E)->Inner.get());
   case VExpr::BinOp: {
-    const auto *B = static_cast<const VBinOpExpr *>(E);
-    if (B->Op != VBinOp::Add && B->Op != VBinOp::Sub)
-      return std::nullopt;
-    const bool Left = B->Lhs->Ty.Kind == VTypeKind::Ptr;
-    const bool Right = B->Rhs->Ty.Kind == VTypeKind::Ptr;
-    if (Left && !Right)
-      return pointerOrigins(B->Lhs.get());
-    if (Right && !Left && B->Op == VBinOp::Add)
-      return pointerOrigins(B->Rhs.get());
+    if (const VExpr *Pointer =
+            steppedPointer(*static_cast<const VBinOpExpr *>(E)))
+      return pointerOrigins(Pointer);
     return std::nullopt;
   }
   case VExpr::Conditional: {
@@ -622,15 +631,9 @@ std::unique_ptr<VExpr> verify::pointerOriginTerm(const VExpr *E) {
   case VExpr::Cast:
     return pointerOriginTerm(static_cast<const VCastExpr *>(E)->Inner.get());
   case VExpr::BinOp: {
-    const auto *B = static_cast<const VBinOpExpr *>(E);
-    if (B->Op != VBinOp::Add && B->Op != VBinOp::Sub)
-      return nullptr;
-    const bool Left = B->Lhs->Ty.Kind == VTypeKind::Ptr;
-    const bool Right = B->Rhs->Ty.Kind == VTypeKind::Ptr;
-    if (Left && !Right)
-      return pointerOriginTerm(B->Lhs.get());
-    if (Right && !Left && B->Op == VBinOp::Add)
-      return pointerOriginTerm(B->Rhs.get());
+    if (const VExpr *Pointer =
+            steppedPointer(*static_cast<const VBinOpExpr *>(E)))
+      return pointerOriginTerm(Pointer);
     return nullptr;
   }
   case VExpr::Conditional: {

clang/lib/Verify/Transform/Origins.h

@@ -25,6 +25,10 @@ namespace verify {
 /// companion keeps it among the possible origins by a generated invariant.
 void annotatePointerOrigins(VFunction &Fn);
 
+/// The pointer operand of a step `p + n`, `n + p`, or `p - n`; null for
+/// anything else, such as a difference of two pointers.
+const VExpr *steppedPointer(const VBinOpExpr &B);
+
 /// The origin term of a pointer expression in an annotated function: an
 /// identity equal for two pointers exactly when they have one origin. Null
 /// when the origin is not known.