From e33136dbd67c154b6b716c3237ab26670bde63f8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:10 +0530 Subject: [PATCH 01/21] verify: Record the pointers of a function that address a subobject. --- clang/lib/Verify/IR/VStmt.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/clang/lib/Verify/IR/VStmt.h b/clang/lib/Verify/IR/VStmt.h index c45936f66e..696ad79c21 100644 --- a/clang/lib/Verify/IR/VStmt.h +++ b/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 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 BoundedPointers; std::vector> ReturnFields; /// Number of leading preconditions originating from explicit pre clauses. unsigned ExplicitPreconditionCount = 0; From e797d091b4b4bbdb0e7d6da3f2b04c4db4f4c28b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:11 +0530 Subject: [PATCH 02/21] verify: Copy a function's bounded pointers when cloning it. --- clang/lib/Verify/IR/VStmt.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/lib/Verify/IR/VStmt.cpp b/clang/lib/Verify/IR/VStmt.cpp index 6b2dbdb952..c8d057d9d3 100644 --- a/clang/lib/Verify/IR/VStmt.cpp +++ b/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) From 997e0e20b17c676fe78356bbc99934d4574751af Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:11 +0530 Subject: [PATCH 03/21] verify: Keep a function's bounded pointers when unrolling its loops. --- clang/lib/Verify/Transform/LoopUnroll.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/lib/Verify/Transform/LoopUnroll.cpp b/clang/lib/Verify/Transform/LoopUnroll.cpp index a363e2c2a7..0acff9045b 100644 --- a/clang/lib/Verify/Transform/LoopUnroll.cpp +++ b/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) From 583f5f44f56f50a466f929036ab957bc8855fa23 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:12 +0530 Subject: [PATCH 04/21] verify: Declare the bounds of pointers to subobjects. --- clang/lib/Verify/Transform/SubobjectBounds.h | 55 ++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 clang/lib/Verify/Transform/SubobjectBounds.h diff --git a/clang/lib/Verify/Transform/SubobjectBounds.h b/clang/lib/Verify/Transform/SubobjectBounds.h new file mode 100644 index 0000000000..4a77572f0e --- /dev/null +++ b/clang/lib/Verify/Transform/SubobjectBounds.h @@ -0,0 +1,55 @@ +//===--- SubobjectBounds.h - Bounds of subobject pointers -------*- C++ -*-===// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// + +#ifndef LLVM_CLANG_VERIFY_TRANSFORM_SUBOBJECTBOUNDS_H +#define LLVM_CLANG_VERIFY_TRANSFORM_SUBOBJECTBOUNDS_H + +#include "../IR/VStmt.h" +#include +#include +#include + +namespace clang { +namespace verify { + +/// The companions holding the first byte and the end of the bytes a bounded +/// pointer may address. +std::string lowerBoundName(const std::string &Pointer); +std::string upperBoundName(const std::string &Pointer); +bool isBoundCompanion(const std::string &Name); + +/// Whether a pointer value is rooted, through steps, casts, and +/// conditionals, at a pointer in Bounded. +bool hasBoundedRoot(const VExpr *Value, const std::set &Bounded); + +/// The first byte (or, with Upper, the end) a pointer value may address, as +/// its bounded roots' companions say: through steps and casts, and selected +/// like the value by a conditional. A root that is not bounded may address +/// any byte. Null when the value has no bounded root. +std::unique_ptr pointerBound(const VExpr *Value, bool Upper, + const std::set &Bounded); + +/// Gives every pointer variable assigned a value rooted at a bounded pointer +/// (Fn.BoundedPointers, which the converter forms with their companions) the +/// value's bounds, and starts every bounded variable that is not a formed +/// subobject pointer with bounds that admit any byte. A step keeps the +/// bounds. Returns the statements that would lose a pointer's bounds: +/// storing it in memory or returning it. +std::vector> +propagateSubobjectBounds(VFunction &Fn); + +/// Whether a variable is a subobject pointer the converter formed. +bool isFormedSubobjectPointer(const std::string &Name); + +/// The prefix of the subobject pointers the converter forms. +extern const char FormedSubobjectPrefix[]; + +} // namespace verify +} // namespace clang + +#endif From 3763cb2a695dcd35ff22b8256e18853cb749b7cf Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:12 +0530 Subject: [PATCH 05/21] verify: Give every pointer assigned a pointer into a subobject the bounds of that subobject. --- .../lib/Verify/Transform/SubobjectBounds.cpp | 332 ++++++++++++++++++ 1 file changed, 332 insertions(+) create mode 100644 clang/lib/Verify/Transform/SubobjectBounds.cpp diff --git a/clang/lib/Verify/Transform/SubobjectBounds.cpp b/clang/lib/Verify/Transform/SubobjectBounds.cpp new file mode 100644 index 0000000000..7c211a33f8 --- /dev/null +++ b/clang/lib/Verify/Transform/SubobjectBounds.cpp @@ -0,0 +1,332 @@ +//===--- SubobjectBounds.cpp - Bounds of subobject pointers ---------------===// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// + +#include "SubobjectBounds.h" +#include "Origins.h" +#include "llvm/ADT/StringRef.h" +#include + +using namespace clang; +using namespace verify; + +const char verify::FormedSubobjectPrefix[] = "__subobject_"; + +std::string verify::lowerBoundName(const std::string &Pointer) { + return Pointer + ".__lo"; +} + +std::string verify::upperBoundName(const std::string &Pointer) { + return Pointer + ".__hi"; +} + +bool verify::isBoundCompanion(const std::string &Name) { + llvm::StringRef Ref(Name); + return Ref.ends_with(".__lo") || Ref.ends_with(".__hi"); +} + +bool verify::isFormedSubobjectPointer(const std::string &Name) { + return llvm::StringRef(Name).starts_with(FormedSubobjectPrefix); +} + +namespace { + +/// The pointer operand a step or cast keeps the bounds of. +const VExpr *steppedOperand(const VExpr *E) { + if (E->K == VExpr::Cast) { + const auto *C = static_cast(E); + return C->Inner->Ty.Kind == VTypeKind::Ptr ? C->Inner.get() : nullptr; + } + if (E->K == VExpr::BinOp) + return steppedPointer(*static_cast(E)); + return nullptr; +} + +std::unique_ptr anyByte(bool Upper, SourceLocation Loc) { + // Every object lies below 2^64. + return std::make_unique( + std::string(Upper ? "18446744073709551616" : "0"), VType::makePtr(), Loc); +} + +/// Whether Value is Pointer stepped: a step keeps its bounds. +bool isStepOf(const VExpr *Value, const std::string &Pointer) { + while (Value) { + if (Value->K == VExpr::Var) + return static_cast(Value)->Name == Pointer; + Value = steppedOperand(Value); + } + return false; +} + +class Propagation { +public: + explicit Propagation(VFunction &Fn) : Fn(Fn) {} + + std::vector> run() { + // Bounded variables: the formed pointers and, to a fixpoint, every + // pointer variable assigned a value rooted at one. + for (bool Changed = true; Changed;) { + Changed = false; + collect(Fn.Body, Changed); + } + if (Fn.BoundedPointers.empty()) + return {}; + rewrite(Fn.Body); + std::vector> Entry; + for (const std::string &Name : Fn.BoundedPointers) + if (!isFormedSubobjectPointer(Name)) + appendAnyByte(Name, Fn.DeclLoc, Entry); + Fn.Body.insert(Fn.Body.begin(), std::make_move_iterator(Entry.begin()), + std::make_move_iterator(Entry.end())); + return std::move(Lost); + } + +private: + VFunction &Fn; + std::vector> Lost; + + void collect(const std::vector> &Stmts, + bool &Changed) { + for (const auto &S : Stmts) + collect(*S, Changed); + } + + void collect(const VStmt &S, bool &Changed) { + switch (S.K) { + case VStmt::Assign: { + const auto &A = static_cast(S); + if (A.Value && A.Value->Ty.Kind == VTypeKind::Ptr && + hasBoundedRoot(A.Value.get(), Fn.BoundedPointers)) + Changed |= Fn.BoundedPointers.insert(A.Target).second; + return; + } + case VStmt::If: { + const auto &I = static_cast(S); + collect(I.Then, Changed); + collect(I.Else, Changed); + return; + } + case VStmt::While: + collect(static_cast(S).Body, Changed); + return; + case VStmt::Seq: + collect(static_cast(S).Stmts, Changed); + return; + case VStmt::GhostBlock: + collect(static_cast(S).Body, Changed); + return; + default: + return; + } + } + + void appendAnyByte(const std::string &Name, SourceLocation Loc, + std::vector> &Out) { + Out.push_back(std::make_unique(lowerBoundName(Name), + anyByte(false, Loc), Loc)); + Out.push_back(std::make_unique(upperBoundName(Name), + anyByte(true, Loc), Loc)); + } + + bool bounded(const std::string &Name) const { + return Fn.BoundedPointers.count(Name); + } + + /// The bounded pointers Stmts assign, with their element sizes. + void assignedPointers(const std::vector> &Stmts, + std::map &Out) const { + for (const auto &S : Stmts) { + switch (S->K) { + case VStmt::Assign: { + const auto &A = static_cast(*S); + if (bounded(A.Target) && A.Value && + A.Value->Ty.Kind == VTypeKind::Ptr && + A.Value->Ty.PointeeSizeBytes != 0) + Out[A.Target] = A.Value->Ty.PointeeSizeBytes; + break; + } + case VStmt::If: + assignedPointers(static_cast(*S).Then, Out); + assignedPointers(static_cast(*S).Else, Out); + break; + case VStmt::While: + assignedPointers(static_cast(*S).Body, Out); + break; + case VStmt::Seq: + assignedPointers(static_cast(*S).Stmts, Out); + break; + case VStmt::GhostBlock: + assignedPointers(static_cast(*S).Body, Out); + break; + default: + break; + } + } + } + + /// A bounded pointer a loop moves stays a whole number of elements from + /// its lower bound (or has none): it starts at an element of its array or + /// at its field, and steps move by whole elements. A generated invariant, + /// so it is proved, not assumed. + void addAlignment(VWhileStmt &W) const { + std::map Moved; + assignedPointers(W.Body, Moved); + const SourceLocation Loc = W.Loc; + for (const auto &[Name, Stride] : Moved) { + const VType Pointer = VType::makePtr(Stride); + auto remainder = [&](std::unique_ptr P) { + return std::make_unique( + VBinOp::Rem, std::move(P), + std::make_unique(std::to_string(Stride), Pointer, + Loc), + Pointer, Loc); + }; + auto isZero = [&](std::string Variable) { + return std::make_unique( + VBinOp::Eq, std::make_unique(Variable, Pointer, Loc), + std::make_unique(0, VType::makePtr(), Loc), + VType::makeBool(), Loc); + }; + auto Aligned = std::make_unique( + VBinOp::Eq, remainder(std::make_unique(Name, Pointer, Loc)), + remainder( + std::make_unique(lowerBoundName(Name), Pointer, Loc)), + VType::makeBool(), Loc); + W.Invariants.push_back(std::make_unique( + VBinOp::Or, + std::make_unique(VBinOp::Or, isZero(Name), + isZero(lowerBoundName(Name)), + VType::makeBool(), Loc), + std::move(Aligned), VType::makeBool(), Loc)); + } + } + + void rewrite(std::vector> &Stmts) { + std::vector> Out; + for (auto &S : Stmts) { + switch (S->K) { + case VStmt::Assign: { + auto &A = static_cast(*S); + // The companions take the value's bounds before the assignment, + // in the state its value is computed in. + if (bounded(A.Target) && !isFormedSubobjectPointer(A.Target) && + !isStepOf(A.Value.get(), A.Target)) { + for (bool Upper : {false, true}) { + auto Bound = pointerBound(A.Value.get(), Upper, Fn.BoundedPointers); + Out.push_back(std::make_unique( + Upper ? upperBoundName(A.Target) : lowerBoundName(A.Target), + Bound ? std::move(Bound) : anyByte(Upper, A.Loc), A.Loc)); + } + } + break; + } + case VStmt::Store: { + const auto &St = static_cast(*S); + if (St.Value && St.Value->Ty.Kind == VTypeKind::Ptr && + hasBoundedRoot(St.Value.get(), Fn.BoundedPointers)) + Lost.emplace_back(St.Loc, "a pointer into a member array or field " + "cannot be stored in memory yet"); + break; + } + case VStmt::Allocate: { + const auto &A = static_cast(*S); + if (A.Initializer && A.Initializer->Ty.Kind == VTypeKind::Ptr && + hasBoundedRoot(A.Initializer.get(), Fn.BoundedPointers)) + Lost.emplace_back(A.Loc, "a pointer into a member array or field " + "cannot be stored in memory yet"); + break; + } + case VStmt::Return: { + const auto &R = static_cast(*S); + if (R.Value && R.Value->Ty.Kind == VTypeKind::Ptr && + hasBoundedRoot(R.Value.get(), Fn.BoundedPointers)) + Lost.emplace_back(R.Loc, "returning a pointer into a member array " + "or field is unsupported"); + break; + } + case VStmt::If: { + auto &I = static_cast(*S); + rewrite(I.Then); + rewrite(I.Else); + break; + } + case VStmt::While: { + auto &W = static_cast(*S); + rewrite(W.Body); + addAlignment(W); + break; + } + case VStmt::Seq: + rewrite(static_cast(*S).Stmts); + break; + case VStmt::GhostBlock: + rewrite(static_cast(*S).Body); + break; + default: + break; + } + // A result or a forgotten value may address anything. + std::string Reset; + if (S->K == VStmt::Call) + Reset = static_cast(*S).ResultTarget; + else if (S->K == VStmt::Havoc) + Reset = static_cast(*S).Target; + else if (S->K == VStmt::Allocate) + Reset = static_cast(*S).Target; + const SourceLocation Loc = S->Loc; + Out.push_back(std::move(S)); + if (!Reset.empty() && bounded(Reset)) + appendAnyByte(Reset, Loc, Out); + } + Stmts = std::move(Out); + } +}; + +} // namespace + +bool verify::hasBoundedRoot(const VExpr *Value, + const std::set &Bounded) { + if (!Value) + return false; + if (Value->K == VExpr::Var) + return Bounded.count(static_cast(Value)->Name); + if (Value->K == VExpr::Conditional) { + const auto *C = static_cast(Value); + return hasBoundedRoot(C->Then.get(), Bounded) || + hasBoundedRoot(C->Else.get(), Bounded); + } + return hasBoundedRoot(steppedOperand(Value), Bounded); +} + +std::unique_ptr +verify::pointerBound(const VExpr *Value, bool Upper, + const std::set &Bounded) { + if (!hasBoundedRoot(Value, Bounded)) + return nullptr; + if (Value->K == VExpr::Var) { + const std::string &Name = static_cast(Value)->Name; + return std::make_unique(Upper ? upperBoundName(Name) + : lowerBoundName(Name), + VType::makePtr(), Value->Loc); + } + if (Value->K == VExpr::Conditional) { + const auto *C = static_cast(Value); + auto Then = pointerBound(C->Then.get(), Upper, Bounded); + auto Else = pointerBound(C->Else.get(), Upper, Bounded); + return std::make_unique( + cloneVExpr(C->Cond.get()), + Then ? std::move(Then) : anyByte(Upper, C->Loc), + Else ? std::move(Else) : anyByte(Upper, C->Loc), VType::makePtr(), + C->Loc); + } + return pointerBound(steppedOperand(Value), Upper, Bounded); +} + +std::vector> +verify::propagateSubobjectBounds(VFunction &Fn) { + return Propagation(Fn).run(); +} From 0195c3cc9a6e2545a08c639c0195a597db559982 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:12 +0530 Subject: [PATCH 06/21] verify: Build the subobject bounds pass. --- clang/lib/Verify/CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/lib/Verify/CMakeLists.txt b/clang/lib/Verify/CMakeLists.txt index d13eed30f3..870d29c22c 100644 --- a/clang/lib/Verify/CMakeLists.txt +++ b/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 From 82b36f906fef60643b4142205579cc00c1cb26a6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:13 +0530 Subject: [PATCH 07/21] verify: Declare the pointer operand of a step. --- clang/lib/Verify/Transform/Origins.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/clang/lib/Verify/Transform/Origins.h b/clang/lib/Verify/Transform/Origins.h index 4e7f038171..31a2968f96 100644 --- a/clang/lib/Verify/Transform/Origins.h +++ b/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. From 58fc32aa37988d249527b3febf348e3ae221f8de Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:13 +0530 Subject: [PATCH 08/21] verify: Read a pointer-typed constant in a sum of pointers as a field offset, and keep bound companions out of origins. --- clang/lib/Verify/Transform/Origins.cpp | 57 ++++++++++++++------------ 1 file changed, 30 insertions(+), 27 deletions(-) diff --git a/clang/lib/Verify/Transform/Origins.cpp b/clang/lib/Verify/Transform/Origins.cpp index f87444308a..c9129e202c 100644 --- a/clang/lib/Verify/Transform/Origins.cpp +++ b/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(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(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 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> verify::pointerOrigins(const VExpr *E) { if (!E) return std::nullopt; @@ -568,15 +583,9 @@ std::optional> verify::pointerOrigins(const VExpr *E) { case VExpr::Cast: return pointerOrigins(static_cast(E)->Inner.get()); case VExpr::BinOp: { - const auto *B = static_cast(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(E))) + return pointerOrigins(Pointer); return std::nullopt; } case VExpr::Conditional: { @@ -622,15 +631,9 @@ std::unique_ptr verify::pointerOriginTerm(const VExpr *E) { case VExpr::Cast: return pointerOriginTerm(static_cast(E)->Inner.get()); case VExpr::BinOp: { - const auto *B = static_cast(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(E))) + return pointerOriginTerm(Pointer); return nullptr; } case VExpr::Conditional: { From 5757a929d67a9698de0c565aff4bcb0d8119c8df Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:13 +0530 Subject: [PATCH 09/21] verify: Declare forming pointers to subobjects of a pointee. --- clang/lib/Verify/Frontend/ASTConverter.h | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index 111754d205..34e1be9c97 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/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> *SubobjectSink = nullptr; + unsigned SubobjectPointerId = 0; std::vector 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 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 From a328596373c21be11c107b01bc011cf86b00e6ee Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:14 +0530 Subject: [PATCH 10/21] verify: Form pointers to member arrays, elements, fields, and nested records of a pointee with their bounds. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 86 +++++++++++++++++++++- 1 file changed, 82 insertions(+), 4 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index ab16c97f53..81f6567ff7 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/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(Peeled); + Decay && Decay->getCastKind() == CK_ArrayToPointerDecay && + pointeeRootPointer(Decay->getSubExpr())) + return convertExpr(Peeled); + if (const auto *U = dyn_cast(Peeled); + U && U->getOpcode() == UO_AddrOf && pointeeRootPointer(U->getSubExpr())) + return convertExpr(Peeled); E = E->IgnoreParenImpCasts(); if (const auto *DRE = dyn_cast(E)) if (isa(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> InitialProvenance; InitialProvenance.reserve(DynamicPointerProvenanceVariables.size()); @@ -3425,10 +3438,6 @@ std::string ASTConverter::arrayDecayError(const Expr *Array) const { const auto *M = dyn_cast_or_null(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 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(Peeled)) { + Bounding = Object; + } else if (const auto *AS = dyn_cast(Peeled)) { + const Expr *Base = peelObjectExpr(AS->getBase()); + if (Base && Base->getType()->isArrayType()) + Bounding = Base; + } + std::unique_ptr 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( + 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(Name, std::move(Address), Loc)); + SubobjectSink->push_back( + std::make_unique(lowerBoundName(Name), std::move(Lo), Loc)); + SubobjectSink->push_back( + std::make_unique(upperBoundName(Name), std::move(Hi), Loc)); + CurrentFn->BoundedPointers.insert(Name); + return std::make_unique(Name, PointerType, Loc); +} + const Expr *ASTConverter::pointeeRootPointer(const Expr *E) const { while (true) { E = peelObjectExpr(E); @@ -4424,6 +4490,8 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { return convertExpr(MTE->getSubExpr()); if (const auto *Decay = dyn_cast(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 ASTConverter::convertExprImpl(const Expr *E) { } if (const auto *U = dyn_cast(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(S) || isa(S)) && + !InGhost && !CurrentFn->IsSpec && + !CurrentFn->IsProof + ? &Out + : nullptr); if (S->getStmtClass() == Stmt::ReturnStmtClass) { if (InGhost) { error(CurrentFn->Name + From 075fe2321fa58414d7897c71e51ffd73087cf8d5 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:14 +0530 Subject: [PATCH 11/21] verify: Keep accesses, steps, and differences through a subobject pointer inside its bounds. --- clang/lib/Verify/Transform/UBChecks.cpp | 66 ++++++++++++++++++++++++- 1 file changed, 65 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/Transform/UBChecks.cpp b/clang/lib/Verify/Transform/UBChecks.cpp index afb633e415..6e5540555b 100644 --- a/clang/lib/Verify/Transform/UBChecks.cpp +++ b/clang/lib/Verify/Transform/UBChecks.cpp @@ -2,6 +2,7 @@ #include "UBChecks.h" #include "../IR/VExpr.h" #include "Origins.h" +#include "SubobjectBounds.h" #include "llvm/ADT/STLExtras.h" #include #include @@ -253,6 +254,47 @@ struct UBInstrumenter { // Parameters the body assigns, whose current value may address another // object than their entry value. std::set Reassigned; + // Pointers to subobjects, which address only their companions' bytes. + std::set Bounded; + + // Other lies in the closed bounds of Bounded, a pointer into a subobject. + std::unique_ptr sameSubobject(const VExpr *Bounded, + const VExpr *Other) const { + if (!ObjectModel) + return nullptr; + auto Lo = pointerBound(Bounded, /*Upper=*/false, this->Bounded); + auto Hi = pointerBound(Bounded, /*Upper=*/true, this->Bounded); + if (!Lo || !Hi) + return nullptr; + const SourceLocation Loc = Other->Loc; + return std::make_unique( + VBinOp::And, + std::make_unique(VBinOp::Le, std::move(Lo), + cloneVExpr(Other), VType::makeBool(), Loc), + std::make_unique(VBinOp::Le, cloneVExpr(Other), + std::move(Hi), VType::makeBool(), Loc), + VType::makeBool(), Loc); + } + + // A pointer to a subobject addresses only the bytes [lo, hi) its bounds + // name: an access lies there, a step in their closure. + std::unique_ptr subobjectObligation(const VExpr *Addr, + bool Closed) const { + if (!ObjectModel || !Addr || Addr->Ty.Kind != VTypeKind::Ptr) + return nullptr; + auto Lo = pointerBound(Addr, /*Upper=*/false, Bounded); + auto Hi = pointerBound(Addr, /*Upper=*/true, Bounded); + if (!Lo || !Hi) + return nullptr; + const SourceLocation Loc = Addr->Loc; + auto Low = std::make_unique( + VBinOp::Le, std::move(Lo), cloneVExpr(Addr), VType::makeBool(), Loc); + auto High = std::make_unique(Closed ? VBinOp::Le : VBinOp::Lt, + cloneVExpr(Addr), std::move(Hi), + VType::makeBool(), Loc); + return std::make_unique( + VBinOp::And, std::move(Low), std::move(High), VType::makeBool(), Loc); + } // The object of a parameter that keeps its entry value, when Root is one. const AbstractObject *parameterObject(const VExpr *Root) const { @@ -719,10 +761,23 @@ struct UBInstrumenter { switch (E->K) { case VExpr::BinOp: { const auto *B = static_cast(E); - if (E != AccessAddress) + if (E != AccessAddress) { if (auto Arithmetic = arithmeticObligation(B)) appendObligation(ProofObligationKind::Bounds, std::move(Arithmetic), Guard, Out); + if (auto Within = subobjectObligation(B, /*Closed=*/true)) + appendObligation(ProofObligationKind::Bounds, std::move(Within), + Guard, Out); + } + // Pointers into a subobject differ only from pointers into the same + // array ([expr.add]): each lies in the other's bounds. + if (B->Op == VBinOp::Sub && B->Lhs->Ty.Kind == VTypeKind::Ptr && + B->Rhs->Ty.Kind == VTypeKind::Ptr) + for (auto [Bounded, Other] : {std::pair{B->Lhs.get(), B->Rhs.get()}, + std::pair{B->Rhs.get(), B->Lhs.get()}}) + if (auto Within = sameSubobject(Bounded, Other)) + appendObligation(ProofObligationKind::PointerDifference, + std::move(Within), Guard, Out); collectObligations(B->Lhs.get(), Out, Guard); if (B->Op == VBinOp::And || B->Op == VBinOp::Or) { std::unique_ptr RhsCondition = cloneVExpr(B->Lhs.get()); @@ -771,6 +826,9 @@ struct UBInstrumenter { if (auto Access = accessObligation(L->Ptr.get())) appendObligation(ProofObligationKind::Bounds, std::move(Access), Guard, Out); + if (auto Within = subobjectObligation(L->Ptr.get(), /*Closed=*/false)) + appendObligation(ProofObligationKind::Bounds, std::move(Within), Guard, + Out); break; } case VExpr::FieldAccess: @@ -822,6 +880,11 @@ struct UBInstrumenter { New.push_back(std::make_unique( std::move(Access), L, ProofObligationKind::Bounds)); } + if (auto Within = subobjectObligation(St.Ptr.get(), /*Closed=*/false)) { + SourceLocation L = Within->Loc; + New.push_back(std::make_unique( + std::move(Within), L, ProofObligationKind::Bounds)); + } const VExpr *SavedAccess = AccessAddress; AccessAddress = St.Ptr.get(); emitObsInto(New, St.Ptr.get()); @@ -1194,6 +1257,7 @@ std::optional verify::instrumentUBChecks(VFunction &Fn) { UB.ObjectModel = true; UB.Objects = abstractObjects(Fn); UB.Reassigned = assignedNames(Fn.Body); + UB.Bounded = Fn.BoundedPointers; UB.dropSingleObjectValidity(Fn); } UB.instrumentStmts(Fn.Body); From 5454452d82fa6fbe702da3388845bc352c12f9c0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:14 +0530 Subject: [PATCH 12/21] verify: Bound call arguments formed from subobject pointers, and measure an origin in its own elements. --- clang/lib/Verify/Transform/Passivize.cpp | 82 +++++++++++++++++++++--- 1 file changed, 74 insertions(+), 8 deletions(-) diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index 2625dfe8ba..26e5e2e7c3 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/clang/lib/Verify/Transform/Passivize.cpp @@ -2,6 +2,7 @@ #include "Passivize.h" #include "Origins.h" #include "SpecInline.h" +#include "SubobjectBounds.h" #include "UBChecks.h" #include "llvm/ADT/APInt.h" #include "llvm/ADT/STLExtras.h" @@ -862,8 +863,9 @@ scaledExtent(const VExpr *Length, uint64_t PointeeSize, SourceLocation Loc) { } /// Pointer lies in the closed byte range of the object its origin names: -/// a parameter's entry object (its declared extent, else one element) or a -/// global. Null when an origin is not such an object. +/// a parameter's entry object (its declared extent, else one object of its +/// pointee type, an entry with no length in Extents) or a global. Null when +/// an origin is not such an object. static std::unique_ptr originPositionSafety(const VExpr *Pointer, const std::vector &Extents, @@ -894,12 +896,17 @@ originPositionSafety(const VExpr *Pointer, for (const VValidExtent &Candidate : Extents) if (Candidate.Base == Origin) Extent = &Candidate; - if (Extent && Extent->PointerType.PointeeSizeBytes != Stride) - return nullptr; - if (Extent) { + // The object is measured in its own elements: a pointer into a + // subobject (a member array) has a smaller type than its origin's. + const uint64_t ObjectStride = + Extent ? Extent->PointerType.PointeeSizeBytes : Stride; + if (Extent && Extent->Length) { VOldExpr Length(cloneVExpr(Extent->Length.get()), Extent->Length->Ty, Loc); - Bytes = scaledExtent(&Length, Stride, Loc); + Bytes = scaledExtent(&Length, ObjectStride, Loc); + } else if (Extent && ObjectStride > 0) { + Bytes = std::make_unique(std::to_string(ObjectStride), + pointerOffsetType(), Loc); } else { Bytes = std::make_unique(std::to_string(Stride), pointerOffsetType(), Loc); @@ -3253,6 +3260,10 @@ class PassivizerImpl { std::vector ActiveValidExtents; std::set PointerParameterNames; std::set SourcePointerParameterNames; + /// The objects of the pointer parameters, for origins: the declared + /// extents, and one object of its pointee type (no length) for a + /// parameter without one. + std::vector OriginObjects; std::set RepresentedAllocationPointers; std::vector StoredPointerCells; std::set HeapBases; @@ -4211,7 +4222,7 @@ class PassivizerImpl { SafetySource ? SafetySource : E, &FnMap, SafetySource ? &Fn.ValidExtents : &ActiveValidExtents, SafetySource ? &SourcePointerParameterNames : &PointerParameterNames, - Checks, Fn.ObjectModel, SafetySource ? &Fn.ValidExtents : nullptr); + Checks, Fn.ObjectModel, SafetySource ? &OriginObjects : nullptr); groupByKind(Checks); CloneCtx Ctx{Renames, OldState, false}; for (const SafetyCheck &Check : Checks) @@ -4530,6 +4541,15 @@ class PassivizerImpl { SourcePointerParameterNames.insert(Param.first); } } + for (const VValidExtent &Extent : Fn.ValidExtents) + OriginObjects.emplace_back(Extent.Base, Extent.PointerType, + cloneVExpr(Extent.Length.get())); + for (const auto &[Name, Ty] : Fn.Params) + if (Ty.Kind == VTypeKind::Ptr && + llvm::none_of(Fn.ValidExtents, [&, &Name = Name](const auto &E) { + return E.Base == Name; + })) + OriginObjects.emplace_back(Name, Ty, nullptr); CloneCtx EntryCtx{Renames, OldState, true}; for (const VValidExtent &Extent : Fn.ValidExtents) ActiveValidExtents.emplace_back(stateVariableName(EntryCtx, Extent.Base), @@ -4613,7 +4633,7 @@ class PassivizerImpl { SafetyChecks Checks; collectSafety(Post, &FnMap, &Fn.ValidExtents, &SourcePointerParameterNames, Checks, Fn.ObjectModel, - &Fn.ValidExtents); + &OriginObjects); groupByKind(Checks); for (const SafetyCheck &Check : Checks) { if (Fn.TotalExpressions && isDefinedness(Check.Kind)) @@ -4856,6 +4876,52 @@ class PassivizerImpl { C.Loc); } + // An argument that addresses a subobject passes only the bytes its + // bounds name: the callee's extent, or its one object, lies in them. + if (Fn.ObjectModel) + for (unsigned I = 0; I < Callee->Params.size() && I < C.Args.size(); + ++I) { + const auto &[Name, Ty] = Callee->Params[I]; + const VExpr *Arg = C.Args[I].get(); + if (Ty.Kind != VTypeKind::Ptr || + !hasBoundedRoot(Arg, Fn.BoundedPointers)) + continue; + std::unique_ptr Bytes; + for (const VValidExtent &Extent : Callee->ValidExtents) + if (Extent.Base == Name) { + auto Length = + substParams(Extent.Length.get(), ParamMap, Ctx, EntryHeap); + Bytes = scaledExtent(Length.get(), + Extent.PointerType.PointeeSizeBytes, C.Loc); + } + if (!Bytes && Ty.PointeeSizeBytes > 0) + Bytes = std::make_unique( + std::to_string(Ty.PointeeSizeBytes), pointerOffsetType(), C.Loc); + if (!Bytes) + continue; + auto Lo = cloneExpr( + pointerBound(Arg, /*Upper=*/false, Fn.BoundedPointers).get(), Ctx); + auto Hi = cloneExpr( + pointerBound(Arg, /*Upper=*/true, Fn.BoundedPointers).get(), Ctx); + const VExpr *Actual = ParamMap[Name].get(); + auto Within = + makeAnd(std::make_unique(VBinOp::Le, std::move(Lo), + cloneVExpr(Actual), + VType::makeBool(), C.Loc), + std::make_unique( + VBinOp::Le, + addBytes(cloneVExpr(Actual), std::move(Bytes), C.Loc), + std::move(Hi), VType::makeBool(), C.Loc), + C.Loc); + emitPassive(P, PassiveStmt::Assert, + makeOr(makeEq(cloneVExpr(Actual), + std::make_unique( + 0, VType::makePtr(), C.Loc), + C.Loc), + std::move(Within), C.Loc), + nullptr, C.Loc, ProofObligationKind::Bounds); + } + std::vector> ActualModifies; std::vector> ActualCounts; for (const VFootprint &M : Callee->Modifies) { From 057431ac14c4308b1132e389cb0aab4170ee3da1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:15 +0530 Subject: [PATCH 13/21] test: Cover pointers into member arrays, fields, and nested records. --- .../test/Verify/suite/subobject_pointers.cpp | 427 ++++++++++++++++++ 1 file changed, 427 insertions(+) create mode 100644 clang/test/Verify/suite/subobject_pointers.cpp diff --git a/clang/test/Verify/suite/subobject_pointers.cpp b/clang/test/Verify/suite/subobject_pointers.cpp new file mode 100644 index 0000000000..e197ee112b --- /dev/null +++ b/clang/test/Verify/suite/subobject_pointers.cpp @@ -0,0 +1,427 @@ +// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s +// RUN: %cpp-verify --lower-only --no-check-ub --dump-ir=1 %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=VCR +// RUN: not %cpp-verify --jobs=1 %s -- -DESCAPE 2>&1 \ +// RUN: | FileCheck %s --check-prefix=ESCAPE +// +// A pointer to a subobject of the object a pointer addresses (a member array +// it decays from, an element of one, a field, a nested record) addresses only +// that subobject's bytes: the array, or the field or record. Every access and +// step through it, and every argument formed from it, stays there, as CHERI's +// subobject bounds do in hardware. The address of a byte one past an array is +// the next field, inside the object, and is still out of bounds. + +struct Inner { + int x; + int y; + int arr[3]; +}; + +struct Item { + int v; + int w; +}; + +struct Ring { + int buf[8]; + int head; + Inner inner; + int grid[3][4]; + Item items[4]; + int other[2]; +}; + +#ifndef ESCAPE +int first(const int *p, int n) + cppverify::pre(cppverify::valid(p, n) && n >= 1) + cppverify::post(cppverify::result == p[0]) +{ + return p[0]; +} +// CHECK-DAG: Verified: first [backend=z3] + +int get(const int *p) + cppverify::pre(p != nullptr) + cppverify::post(cppverify::result == *p) +{ + return *p; +} +// CHECK-DAG: Verified: get [backend=z3] + +void set(int *p, int v) + cppverify::pre(p != nullptr) + cppverify::modifies(*p) + cppverify::post(*p == v) +{ + *p = v; +} +// CHECK-DAG: Verified: set [backend=z3] + +int inner_x(const Inner *p) + cppverify::pre(p != nullptr) + cppverify::post(cppverify::result == p->x) +{ + return p->x; +} +// CHECK-DAG: Verified: inner_x [backend=z3] + +// The member array passed as a buffer, whole and from an element on. +int pass_member(const Ring *r) + cppverify::pre(r != nullptr) + cppverify::post(cppverify::result == r->buf[0]) +{ + return first(r->buf, 8); +} +// CHECK-DAG: Verified: pass_member [backend=z3] +// VCR-LABEL: fn pass_member +// VCR: assign __subobject_1 +// VCR-NEXT: + +// VCR-NEXT: r +// VCR-NEXT: 0 +// VCR-NEXT: assign __subobject_1.__lo +// VCR-NEXT: + +// VCR-NEXT: r +// VCR-NEXT: 0 +// VCR-NEXT: assign __subobject_1.__hi +// VCR-NEXT: + +// VCR-NEXT: + +// VCR-NEXT: r +// VCR-NEXT: 0 +// VCR-NEXT: 32 +// VCR-NEXT: call first +// VCR-NEXT: __subobject_1 + +int pass_tail(const Ring *r) + cppverify::pre(r != nullptr) + cppverify::post(cppverify::result == r->buf[5]) +{ + return first(r->buf + 5, 3); +} +// CHECK-DAG: Verified: pass_tail [backend=z3] + +// A local pointer keeps the bounds of the array it comes from. +int local_walk(const Ring *r) + cppverify::pre(r != nullptr) + cppverify::post(cppverify::result == r->buf[7]) +{ + const int *q = r->buf; + return q[7]; +} +// CHECK-DAG: Verified: local_walk [backend=z3] +// VCR-LABEL: fn local_walk +// VCR: assign q.__lo +// VCR-NEXT: 0 +// VCR-NEXT: assign q.__hi +// VCR-NEXT: 18446744073709551616 +// VCR: assign q.__lo +// VCR-NEXT: __subobject_{{[0-9]+}}.__lo +// VCR-NEXT: assign q.__hi +// VCR-NEXT: __subobject_{{[0-9]+}}.__hi +// VCR-NEXT: assign q +// VCR-NEXT: __subobject_{{[0-9]+}} + +int element_address(const Ring *r) + cppverify::pre(r != nullptr) + cppverify::post(cppverify::result == r->buf[0]) +{ + const int *q = &r->buf[2]; + return q[-2]; +} +// CHECK-DAG: Verified: element_address [backend=z3] + +void field_address(Ring *r) + cppverify::pre(r != nullptr) + cppverify::modifies(r->head) + cppverify::post(r->head == 5) +{ + set(&r->head, 5); +} +// CHECK-DAG: Verified: field_address [backend=z3] + +int record_address(const Ring *r) + cppverify::pre(r != nullptr) + cppverify::post(cppverify::result == r->inner.x) +{ + return inner_x(&r->inner); +} +// CHECK-DAG: Verified: record_address [backend=z3] + +int nested_member(const Ring *r) + cppverify::pre(r != nullptr) + cppverify::post(cppverify::result == r->inner.arr[2]) +{ + const Inner *in = &r->inner; + return in->arr[2]; +} +// CHECK-DAG: Verified: nested_member [backend=z3] + +int row(const Ring *r, int i) + cppverify::pre(r != nullptr && 0 <= i && i < 3) + cppverify::post(cppverify::result == r->grid[i][3]) +{ + const int *q = r->grid[i]; + return q[3]; +} +// CHECK-DAG: Verified: row [backend=z3] + +int item_field(const Ring *r, int k) + cppverify::pre(r != nullptr && 0 <= k && k < 4) + cppverify::post(cppverify::result == r->items[k].w) +{ + const Item *it = &r->items[k]; + return it->w; +} +// CHECK-DAG: Verified: item_field [backend=z3] + +// The address of an element of a parameter's own buffer. +int param_element(const int *a, int n) + cppverify::pre(cppverify::valid(a, n) && n >= 4) + cppverify::post(cppverify::result == a[2]) +{ + return get(&a[2]); +} +// CHECK-DAG: Verified: param_element [backend=z3] + +// A pointer stepped through the member, compared with its end, and measured +// by a pointer difference. +int sum8(const Ring *r) + cppverify::pre(r != nullptr) + cppverify::pre(cppverify::forall(k, 0, 8, 0 <= r->buf[k] && r->buf[k] <= 100)) + cppverify::post(cppverify::result >= 0) +{ + int s = 0; + const int *q = r->buf; + int i = 0; + while (i < 8) + cppverify::invariant(0 <= i && i <= 8 && q == r->buf + i) + cppverify::invariant(0 <= s && s <= 100 * i) + cppverify::decreases(8 - i) + { + s = s + *q; + q = q + 1; + i = i + 1; + } + return s; +} +// CHECK-DAG: Verified: sum8 [backend=z3] + +int count8(const Ring *r) + cppverify::pre(r != nullptr) + cppverify::post(cppverify::result == 8) +{ + int n = 0; + for (const int *q = r->buf; q != r->buf + 8; q = q + 1) + cppverify::invariant(r->buf <= q && q <= r->buf + 8 && n == q - r->buf) + cppverify::decreases(r->buf + 8 - q) + { + n = n + 1; + } + return n; +} +// CHECK-DAG: Verified: count8 [backend=z3] + +int distance(const Ring *r, int i) + cppverify::pre(r != nullptr && 0 <= i && i <= 8) + cppverify::post(cppverify::result == i) +{ + const int *q = r->buf + i; + return q - r->buf; +} +// CHECK-DAG: Verified: distance [backend=z3] + +int chosen(const Ring *r, bool c) + cppverify::pre(r != nullptr) + cppverify::post(cppverify::result == (c ? r->buf[1] : r->other[1])) +{ + const int *q = c ? r->buf : r->other; + return q[1]; +} +// CHECK-DAG: Verified: chosen [backend=z3] + +// A pointer assigned another value takes that value's bounds. +int reassigned(const Ring *r, const int *p) + cppverify::pre(r != nullptr && p != nullptr) + cppverify::post(cppverify::result == *p) +{ + const int *q = r->buf; + q = p; + return q[0]; +} +// CHECK-DAG: Verified: reassigned [backend=z3] + +void write_through(Ring *r, int i) + cppverify::pre(r != nullptr && 0 <= i && i < 8) + cppverify::modifies(r->buf[0 : 8]) + cppverify::post(r->buf[i] == 7 && r->head == cppverify::old(r->head)) +{ + int *q = r->buf; + q[i] = 7; +} +// CHECK-DAG: Verified: write_through [backend=z3] + +int checked(const Ring *r) + cppverify::pre(r != nullptr) + cppverify::post(cppverify::result == r->buf[3]) +{ + const int *q = r->buf; + cppverify::check(q[3] == r->buf[3]); + return q[3]; +} +// CHECK-DAG: Verified: checked [backend=z3] + +// Nine elements from buf run into head. +int pass_too_long(const Ring *r) + cppverify::pre(r != nullptr) +{ + return first(r->buf, 9); +} +// CHECK-DAG: error: verification failed: pass_too_long [{{.*}}::bounds@[[@LINE-2]]:3#2] (counterexample: r [ssa=r_0] [type=pointer] = {{[0-9]+}} + +int pass_tail_too_long(const Ring *r) + cppverify::pre(r != nullptr) +{ + return first(r->buf + 5, 4); +} +// CHECK-DAG: error: verification failed: pass_tail_too_long [{{.*}}::bounds@[[@LINE-2]]:3#2] + +// The end of buf is a pointer, but get reads the element there: r->head. +int pass_end(const Ring *r) + cppverify::pre(r != nullptr) +{ + const int *q = r->buf + 8; + return get(q); +} +// CHECK-DAG: error: verification failed: pass_end [{{.*}}::bounds@[[@LINE-2]]:3] + +// q[-1] is r->items[3].w, inside *r but before other. +int before_member(const Ring *r) + cppverify::pre(r != nullptr) +{ + const int *q = r->other; + return q[-1]; +} +// CHECK-DAG: error: verification failed: before_member [{{.*}}::bounds@[[@LINE-2]]:10#2] + +// q[8] is r->head. +int local_past(const Ring *r) + cppverify::pre(r != nullptr) +{ + const int *q = r->buf; + return q[8]; +} +// CHECK-DAG: error: verification failed: local_past [{{.*}}::bounds@[[@LINE-2]]:10#2] + +int element_past(const Ring *r) + cppverify::pre(r != nullptr) +{ + const int *q = &r->buf[2]; + return q[6]; +} +// CHECK-DAG: error: verification failed: element_past [{{.*}}::bounds@[[@LINE-2]]:10#2] + +// q[1] is r->inner.x, next to head. +void field_neighbor(Ring *r) + cppverify::pre(r != nullptr) + cppverify::modifies(*r) +{ + int *q = &r->head; + q[1] = 0; +} +// CHECK-DAG: error: verification failed: field_neighbor [{{.*}}::bounds@[[@LINE-2]]:3#2] + +// q[4] is grid[i + 1][0]. +int row_past(const Ring *r, int i) + cppverify::pre(r != nullptr && 0 <= i && i < 2) +{ + const int *q = r->grid[i]; + return q[4]; +} +// CHECK-DAG: error: verification failed: row_past [{{.*}}::bounds@[[@LINE-2]]:10#2] + +// it[1] is past items, at r->other. +int item_past(const Ring *r) + cppverify::pre(r != nullptr) +{ + const Item *it = &r->items[3]; + return it[1].v; +} +// CHECK-DAG: error: verification failed: item_past [{{.*}}::bounds@[[@LINE-2]]:16#2] + +// When c is false, q addresses other, of two elements. +int chosen_past(const Ring *r, bool c) + cppverify::pre(r != nullptr) +{ + const int *q = c ? r->buf : r->other; + return q[2]; +} +// CHECK-DAG: error: verification failed: chosen_past [{{.*}}::bounds@[[@LINE-2]]:10] (counterexample: c [ssa=c_0] [type=bool] = false, + +int walk_past(const Ring *r) + cppverify::pre(r != nullptr) +{ + int s = 0; + for (const int *q = r->buf; q != r->buf + 9; q = q + 1) + cppverify::invariant(r->buf <= q && q <= r->buf + 9) + cppverify::decreases(r->buf + 9 - q) + { + s = *q; + } + return s; +} +// CHECK-DAG: error: verification failed: walk_past [{{.*}}::bounds@[[@LINE-4]]:10#2] + +// Forming the address of an element is reading nothing, but the element +// must exist: buf[8] does not. +int element_one_past(const Ring *r, int i) + cppverify::pre(r != nullptr && i == 8) +{ + const int *q = &r->buf[i]; + return 0; +} +// CHECK-DAG: error: verification failed: element_one_past [{{.*}}::bounds@[[@LINE-3]]:18] (counterexample: i [ssa=i_0] [type=i32] = 8, + +int null_root(const Ring *r) + cppverify::post(cppverify::result == 0) +{ + const int *q = r->buf; + return 0; +} +// CHECK-DAG: error: verification failed: null_root [{{.*}}::dereference@[[@LINE-3]]:18] (counterexample: r [ssa=r_0] [type=pointer] = 0) + +// Pointers into different members differ by nothing C++ defines. +int across_members(const Ring *r) + cppverify::pre(r != nullptr) +{ + return &r->head - r->buf; +} +// CHECK-DAG: error: verification failed: across_members [{{.*}}::pointer-difference@[[@LINE-2]]:21] + +void write_frame(Ring *r) + cppverify::pre(r != nullptr) + cppverify::modifies(r->buf[0 : 8]) +{ + int *q = r->other; + q[0] = 7; +} +// CHECK-DAG: error: verification failed: write_frame [{{.*}}::frame@[[@LINE-2]]:8] +#else +// A pointer that left the function would lose its bounds. +struct Holder { + const int *p; +}; + +void stored(Ring *r, Holder *h) + cppverify::pre(r != nullptr && h != nullptr) + cppverify::modifies(h->p) +{ + h->p = r->buf; +} +// ESCAPE-DAG: subobject_pointers.cpp:[[@LINE-2]]:8: error: stored: a pointer into a member array or field cannot be stored in memory yet + +const int *returned(const Ring *r) + cppverify::pre(r != nullptr) +{ + return &r->buf[2]; +} +// ESCAPE-DAG: subobject_pointers.cpp:[[@LINE-2]]:3: error: returned: returning a pointer into a member array or field is unsupported +#endif From d204329cd2af51c40b1747d921b921ebdb76b8eb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:15 +0530 Subject: [PATCH 14/21] test: Drop the member array decay that is supported now. --- clang/test/Verify/suite/pointer_subobjects.cpp | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/clang/test/Verify/suite/pointer_subobjects.cpp b/clang/test/Verify/suite/pointer_subobjects.cpp index 17d1cc186e..40b778c243 100644 --- a/clang/test/Verify/suite/pointer_subobjects.cpp +++ b/clang/test/Verify/suite/pointer_subobjects.cpp @@ -284,16 +284,6 @@ void nested_write_wrong(Outer *p) } // CHECK-DAG: error: verification failed: nested_write_wrong [{{.*}}::postcondition@[[@LINE-4]]:30] #else -// A pointer to a member array would be bounded by that array, which only an -// access that indexes it shows. -int decayed(const Ring *r) - cppverify::pre(r != nullptr) -{ - const int *q = r->buf; - return 0; -} -// DECAY-DAG: pointer_subobjects.cpp:[[@LINE-3]]:18: error: decayed: a pointer to the array member 'buf' is unsupported; index the member where it is used, as in 'buf[i]' - // Arrays in global storage are not modeled; the message names the global. Ring global_ring; int global_table[4]; From f3daa1aa88809154b99d38a555621da154df2586 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:15 +0530 Subject: [PATCH 15/21] docs: Document pointers into a record. --- website/source/language/structs.rst | 92 +++++++++++++++++++++++++---- 1 file changed, 82 insertions(+), 10 deletions(-) diff --git a/website/source/language/structs.rst b/website/source/language/structs.rst index cefe176650..4b33605a57 100644 --- a/website/source/language/structs.rst +++ b/website/source/language/structs.rst @@ -69,13 +69,23 @@ hold, so ``grid[0][4]`` is rejected even though it has the address of the body, and in postconditions and assertions, where a division by zero is checked too. -Two forms are not supported yet. Reading a whole record or array through a -pointer (``Ring copy = *r;``) is an error; read its fields instead. Forming a -pointer to an array member, as passing ``r->buf`` to a buffer parameter does, -is also an error, because the pointer would have to carry the member's -bounds; index the member where it is used: +Reading a whole record or array through a pointer (``Ring copy = *r;``) is +not supported yet; read its fields instead. -.. cppverify-example: rejects +Pointers into a record +---------------------- + +A pointer can also point into the object a pointer addresses. A member array +decays to a pointer to its first element (``r->buf``), and ``&`` gives the +address of an element, a field, or a nested record (``&r->buf[2]``, +``&r->head``, ``&r->inner``). Such a pointer may address only that +subobject: the array it comes from, or else the field or record. Every access +and step through it must stay there, however the pointer is copied, chosen, +or stepped, and so must the elements of every argument formed from it. +``q[8]`` below has the address of ``r->head``, inside ``*r``, and is still out +of bounds: + +.. cppverify-example: fails past .. code-block:: cpp @@ -94,15 +104,76 @@ bounds; index the member where it is used: int oldest(const Ring *r) cv::pre(r != nullptr) + cv::post(cv::result == r->buf[0]) { return first(r->buf, 8); } + int total(const Ring *r) + cv::pre(r != nullptr) + cv::pre(cv::forall(k, 0, 8, 0 <= r->buf[k] && r->buf[k] <= 100)) + cv::post(cv::result >= 0 && cv::result <= 800) + { + int s = 0; + for (const int *q = r->buf; q != r->buf + 8; q = q + 1) + cv::invariant(r->buf <= q && q <= r->buf + 8) + cv::invariant(0 <= s && s <= 100 * (q - r->buf)) + cv::decreases(r->buf + 8 - q) + { + s = s + *q; + } + return s; + } + + int past(const Ring *r) + cv::pre(r != nullptr) + { + const int *q = r->buf; + return q[8]; + } + +.. code-block:: text + + Verified: first [backend=z3] + Verified: oldest [backend=z3] + Verified: total [backend=z3] + ring.cpp:41:10: error: verification failed: past [...::bounds@41:10#2] (counterexample: q [ssa=q_1] [type=pointer] = 1, r [ssa=r_0] [type=pointer] = 1) [backend=z3] [reason=counterexample] + +The rules follow C++: + +- forming the pointer requires the object it points into: ``r`` non-null, and + each index inside its array, so ``&r->buf[i]`` with ``i == 8`` is an error + even though ``r->buf + 8`` is not; +- a step may reach one past the end of the array, and an access may not; +- a pointer difference such as ``q - r->buf`` requires both pointers in one + array, so ``&r->head - r->buf`` is an error; +- as a bare value, in a condition or a contract (``q != r->buf + 8``), the + pointer only compares. + +Such a pointer cannot yet leave the function, because the bounds it carries +would be lost there: returning it, or storing it in memory, is an error. + +.. cppverify-example: rejects + +.. code-block:: cpp + + struct Ring { + int buf[8]; + int head; + int count; + }; + + const int *slot(const Ring *r, int i) + cv::pre(r != nullptr && 0 <= i && i < 8) + { + return &r->buf[i]; + } + .. code-block:: text - ring.cpp:17:16: error: oldest: a pointer to the array member 'buf' is unsupported; index the member where it is used, as in 'buf[i]' - 17 | return first(r->buf, 8); - | ^~~~~~ + ring.cpp:10:3: error: slot: returning a pointer into a member array or field is unsupported + 10 | return &r->buf[i]; + | ^~~~~~ ``cppverify::type_invariant`` ----------------------------- @@ -162,6 +233,7 @@ fields. A local object whose address is needed (it holds a fixed array, or a reference binds to one of its members) is promoted to an automatic object and may also have nested record, pointer, and fixed-array members. A record reached through a pointer may have the same members, and its scalar fields and -elements are reached one at a time (see `Records through pointers`_). Reference +elements are reached one at a time (see `Records through pointers`_), or +through a pointer into it (see `Pointers into a record`_). Reference members, unions, bases, virtual dispatch, and non-trivial construction/destruction are rejected rather than approximated. From bbbb9fadc0bc8f89bb2ee0c3c5c47555d627990e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:16 +0530 Subject: [PATCH 16/21] docs: Relate pointers into a record to origins. --- website/source/language/pointers.rst | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/website/source/language/pointers.rst b/website/source/language/pointers.rst index ae9f4256d1..ef80228b84 100644 --- a/website/source/language/pointers.rst +++ b/website/source/language/pointers.rst @@ -717,6 +717,12 @@ from ``a`` and moved one past its end is rejected there even when another object happens to start at that address, as C++ requires. A pointer difference needs one origin, and a loop writes only its stores' origins. +A pointer into a record, such as ``r->buf`` or ``&r->head``, has the +record's origin and, in addition, the bounds of the array, field, or nested +record it points into. Its accesses, steps, and differences must stay inside +those bounds, so ``q = r->buf; q[8]`` is rejected although it lies in ``*r`` +(see :doc:`structs`). + Inside a loop, the verifier proves two facts for you: a pointer the loop moves stays a whole number of elements from its origin's start, and a pointer that may have either of two origins keeps one of them. An invariant still From 90b5aecdc25891864913d3f4c985cd5cbf9f5aec Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:16 +0530 Subject: [PATCH 17/21] docs: Move pointers into records into the supported subset. --- website/source/language/limitations.rst | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 3a3e29c69c..8841fa298c 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -89,7 +89,9 @@ The most mature current fragment includes: - fixed local arrays and promoted trivial local records with nested record, pointer, and fixed-array members; - the fields and fixed-array elements of a record a pointer addresses, at any - depth (``p->buf[i]``, ``p->inner.arr[j]``, ``p[k].items[i].v``); + depth (``p->buf[i]``, ``p->inner.arr[j]``, ``p[k].items[i].v``), and + pointers into them, each bounded by the array, field, or record it points + into; - one-level typed pointers, abstract indexed buffers, and heap framing; - constrained direct scalar ``new``/``delete`` with liveness, initialization, and provenance. @@ -127,10 +129,12 @@ C++ feature boundaries local arrays (including arrays of records and multidimensional arrays) modelled as byte-addressed automatic objects up to 256 bytes, and the fixed-array members of a record a pointer addresses, each index - checked against its own array. + checked against its own array, and pointers into them + (``int *q = p->buf;``, ``&p->buf[i]``), bounded by the array. - Array parameters/fields carried by value, array references, ``new[]``/``delete[]``, loop-local arrays, and raw pointers derived from - a local array or from an array member (``int *q = p->buf;``). + a local array; a pointer into a record a pointer addresses that leaves + the function (returned or stored in memory). * - Records - Flat trivial standard-layout values with scalar fields; trivial standard-layout records with nested record, pointer, and fixed-array From 8a5e6d7a957efd7050419f48cd0e8edf0b9ae77f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:17 +0530 Subject: [PATCH 18/21] docs: Walk a member array with a pointer in the pointers chapter. --- .../part-ii/ch14-pointers-frames-modifies.rst | 58 +++++++++++++++++-- 1 file changed, 54 insertions(+), 4 deletions(-) diff --git a/website/source/book/part-ii/ch14-pointers-frames-modifies.rst b/website/source/book/part-ii/ch14-pointers-frames-modifies.rst index 390d3a304e..c5cd6bbc02 100644 --- a/website/source/book/part-ii/ch14-pointers-frames-modifies.rst +++ b/website/source/book/part-ii/ch14-pointers-frames-modifies.rst @@ -273,10 +273,60 @@ the object alone would accept it. Each index is checked against its own array, as Frama-C's RTE guards are, and the counterexample is the full stack: the store's address is 65, which is ``s + 16 * 4`` with ``s = 1``. -A pointer to the member array itself (``int *q = s->items;``) is not -supported yet, because the pointer would have to carry the array's bounds. -Index the member where it is used. :doc:`../../language/structs` lists the -forms that are supported. +A pointer into the member array can also walk it. The pointer may address +only the array it comes from: ``s->items``, not the whole record, so a walk +that runs one element too far reads ``s->size`` and fails: + +.. cppverify-example: fails count_past + +.. code-block:: cpp + + struct Stack { + int items[16]; + int size; + }; + + int count_zero(const Stack *s) + cv::pre(s != nullptr && 0 <= s->size && s->size <= 16) + cv::post(0 <= cv::result && cv::result <= s->size) + { + int n = 0; + for (const int *q = s->items; q != s->items + s->size; q = q + 1) + cv::invariant(s->items <= q && q <= s->items + s->size) + cv::invariant(0 <= n && n <= q - s->items) + cv::decreases(s->items + s->size - q) + { + if (*q == 0) + n = n + 1; + } + return n; + } + + int count_past(const Stack *s) + cv::pre(s != nullptr && 0 <= s->size && s->size <= 16) + { + int n = 0; + for (const int *q = s->items; q != s->items + s->size + 1; q = q + 1) + cv::invariant(s->items <= q && q <= s->items + s->size + 1) + cv::invariant(0 <= n && n <= q - s->items) + cv::decreases(s->items + s->size + 1 - q) + { + if (*q == 0) + n = n + 1; + } + return n; + } + +.. code-block:: text + + Verified: count_zero [backend=z3] + stack.cpp:31:10: error: verification failed: count_past [...::bounds@31:10#2] (counterexample: n [ssa=n_1] [type=i32] = 0, n [ssa=n_2] [type=i32] = 0, q [ssa=q_1] [type=pointer] = 1, q [ssa=q_2] [type=pointer] = 65, s [ssa=s_0] [type=pointer] = 1; trace: loop.entry@26:3 -> loop.inductive iteration@26:3 condition=true) [backend=z3] [reason=counterexample] + +In ``count_past`` the solver chooses a full stack, and ``q`` reaches 65, the +address of ``s->size`` with ``s`` at 1. The verifier itself states that a +pointer stepped through the array stays a whole number of elements from its +start, as a generated invariant it proves, so the walk never lands between +elements. :doc:`../../language/structs` lists the forms that are supported. Declaring a checked extent -------------------------- From f800822dbdc0baeaf70cf30147afa63c95cc9084 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:17 +0530 Subject: [PATCH 19/21] docs: Note pointers into records in the release notes. --- website/source/release-notes.rst | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index b7ecf2b822..6e39ebc465 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -169,6 +169,17 @@ name it, and a reference can bind to it. Each index is checked against its own array, so ``r->buf[8]``, which has the address of the next field, is still an error (:doc:`language/structs`). +**Pointers into records.** A pointer into the object a pointer addresses was an +error: a member array passed to a buffer function (``first(r->buf, 8)``), a +pointer walking it (``for (const int *q = r->buf; q != r->buf + 8; ++q)``), +and the address of an element, a field, or a nested record (``&r->buf[i]``, +``&r->head``, ``&r->inner``). The address of an element of a parameter's own +buffer (``&a[2]``) was an error too. These are supported now. A pointer into +a record may address only the array, field, or record it points into: +accesses, steps, pointer differences, and call arguments through it are +checked against that subobject, so ``q[8]`` past ``r->buf`` is an error, +though it lies in ``*r`` (:doc:`language/structs`). + Running cpp-verify ~~~~~~~~~~~~~~~~~~ From d1704bd2a85c65740cd637fa5927dceb321906d3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:17 +0530 Subject: [PATCH 20/21] docs: Describe pointers into records in the design. --- docs/DESIGN.md | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 7f988388bc..16e7bea499 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1109,11 +1109,22 @@ void put(Ring *r, int v) rejects `r->buf[8]`, whose address is `r->head`, inside `*r`; in `p->grid[i][j]` it bounds `j` by the row, so `grid[0][4]` is rejected although it is `grid[1][0]` in memory. -- A whole record or array read through a pointer (`Ring copy = *r;`) and a - pointer to an array member (`const int *q = r->buf;`) are rejected. Such a - pointer would have to carry the member's extent, as a Rust slice carries - its length: the planned design gives a decayed member array an origin - whose object is the member, so its accesses are bounded by the array. +- A whole record or array read through a pointer (`Ring copy = *r;`) is + rejected. +- A pointer into the object, a decayed member array (`r->buf`) or the + address of an element, a field, or a nested record (`&r->buf[i]`, + `&r->head`, `&r->inner`), addresses only that subobject: the array it comes + from, else the field or record, as CHERI narrows a capability to a + subobject and as a Rust slice carries its length. Forming it requires the + object it points into (non-null root, every index of its path inside its + array, strictly). Every access through it lies in the subobject, every + step in its closure, a pointer difference needs both operands in one + subobject, and a callee's extent or object formed from it lies in it. + The bounds are proved, not checked at run time: two ghost companions of + the pointer hold the subobject's first byte and end, assigned where it is + formed and wherever a pointer variable takes its value, kept by steps. + Returning such a pointer or storing it in memory would lose the bounds + and is rejected. ### 4. `cppverify::modifies(...)` frame condition From 827c9833b3b92d02ac39fcdb3d3973b1e3a39a5b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 19:10:18 +0530 Subject: [PATCH 21/21] docs: Describe subobject pointers and their bounds in the architecture. --- docs/ARCHITECTURE.md | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 1a2480d2f5..aa41ad316a 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -176,6 +176,32 @@ whose own access UB instrumentation checks against the pointer's extent or object as before. `p->buf[i]` therefore has both checks, and the array's is what rejects `p->buf[8]`, the address of the next field. +**Pointers into objects:** `ASTConverter::subobjectPointer` lowers a decayed +member array of a pointee and the address of a pointee's element, field, or +nested record. In a statement (`SubobjectSink`) it asserts the place's access +condition and its accessibility (`appendReferenceBindingCheck`) and binds the +address to a fresh pointer `__subobject_N` with two companions, +`__subobject_N.__lo` and `.__hi`, the bytes of the array it comes from or +else of the field or record; elsewhere, as in a condition or a contract, it +is the address alone. `VFunction::BoundedPointers` names the pointers with +companions. `propagateSubobjectBounds` (`Transform/SubobjectBounds.cpp`) runs +on the converted body: every pointer variable assigned a value rooted at a +bounded pointer (through steps, casts, and conditionals, `pointerBound`) is +bounded too; before each such assignment its companions take the value's +bounds (a root without bounds may address any byte, `[0, 2^64)`), a step +keeps them, every bounded variable starts with any byte at entry, and a loop +that moves one gets the generated invariant `q == 0 || q.__lo == 0 || +q % S == q.__lo % S`. Storing a bounded value in memory or returning it is a +conversion error. UB instrumentation (`subobjectObligation`, `sameSubobject`) +adds `lo <= addr < hi` at each access, `lo <= p <= hi` at each step, and each +operand in the other's closed bounds at a pointer difference; a call asserts +that the bytes a callee's extent or object takes from a bounded argument lie +in its bounds. Origins treat the companions as no pointers, and a constant of +pointer type in a sum of two pointers is the field offset +(`steppedPointer`). Pointer-difference positions measure an origin's object +in its own elements (`PassivizerImpl::OriginObjects`), since a pointer into a +member has a smaller type than its origin. + **Quantifiers, triggers, choices, collections:** a quantifier without bounds ranges over all mathematical integers. A `cppverify::trigger(term)` mark is an identity `Cast` flagged `IsTrigger` around the term. Each `cppverify::choose` is lifted to a