diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index d3b17f4d20..ab16c97f53 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -3303,8 +3303,25 @@ std::optional ASTConverter::subscriptPlace(const ArraySubscriptExpr *AS) { if (!AS) return std::nullopt; - if (promotedRootLocal(AS)) - return promotedObjectPlace(AS); + // An element of a fixed array inside a represented object: a promoted + // local, or the object a pointer addresses (r->buf[i], p[k].grid[i][j]). + if (promotedRootLocal(AS) || pointeeRootPointer(AS->getBase())) + return objectPlace(AS); + return pointerElementPlace(AS); +} + +std::optional ASTConverter::pointeePlace(const Expr *PointerExpr, + SourceLocation Loc) { + if (isDynamicAddress(PointerExpr)) { + error(CurrentFn->Name + + ": dynamic-storage pointers cannot select record fields"); + return std::nullopt; + } + return derefPlace(PointerExpr, Loc); +} + +std::optional +ASTConverter::pointerElementPlace(const ArraySubscriptExpr *AS) { if (isDynamicAddress(AS->getBase())) { error(CurrentFn->Name + ": subscripting dynamic-storage pointers is unsupported"); @@ -3373,7 +3390,9 @@ static const Expr *peelObjectExpr(const Expr *E) { return E; } -const VarDecl *ASTConverter::promotedRootLocal(const Expr *E) const { +/// The variable a chain of dot member and fixed-array element selections +/// starts at (a in a.b[i].c), or null. +static const VarDecl *selectionRootVar(const Expr *E) { while (true) { E = peelObjectExpr(E); if (!E) @@ -3394,10 +3413,61 @@ const VarDecl *ASTConverter::promotedRootLocal(const Expr *E) const { break; } const auto *DRE = dyn_cast(E); - const auto *VD = DRE ? dyn_cast(DRE->getDecl()) : nullptr; + return DRE ? dyn_cast(DRE->getDecl()) : nullptr; +} + +const VarDecl *ASTConverter::promotedRootLocal(const Expr *E) const { + const VarDecl *VD = selectionRootVar(E); return VD && AddressableLocals.count(VD) ? VD : nullptr; } +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"; + const std::string Name = "'" + Root->getNameAsString() + "'"; + return M ? "the array member '" + Member + "' of the " + Kind + " " + Name + + " is unsupported" + : "the " + Kind + " array " + Name + " is unsupported"; + } + return "array-to-pointer decay of automatic storage is unsupported until " + "lexical lifetime and escape effects are modeled"; +} + +const Expr *ASTConverter::pointeeRootPointer(const Expr *E) const { + while (true) { + E = peelObjectExpr(E); + if (!E) + return nullptr; + if (const auto *M = dyn_cast(E)) { + if (M->isArrow()) + return M->getBase(); + E = M->getBase(); + continue; + } + if (const auto *AS = dyn_cast(E)) { + const Expr *Base = peelObjectExpr(AS->getBase()); + if (Base && Base->getType()->isArrayType()) { + E = Base; + continue; + } + return AS->getBase()->getType()->isPointerType() ? AS->getBase() + : nullptr; + } + if (const auto *U = dyn_cast(E); + U && U->getOpcode() == UO_Deref) + return U->getSubExpr(); + return nullptr; + } +} + std::optional ASTConverter::recordFieldOffset(const FieldDecl *FD) const { if (!FD || FD->isBitField()) @@ -3455,8 +3525,7 @@ ASTConverter::recordFixedArrayBoundsCheck(const Expr *Index, return Bound; } -std::optional -ASTConverter::promotedObjectPlace(const Expr *E) { +std::optional ASTConverter::objectPlace(const Expr *E) { E = peelObjectExpr(E); if (!E) return std::nullopt; @@ -3468,17 +3537,19 @@ ASTConverter::promotedObjectPlace(const Expr *E) { return automaticLocalPlace(VD, E->getExprLoc()); } + if (const auto *U = dyn_cast(E); + U && U->getOpcode() == UO_Deref) + return pointeePlace(U->getSubExpr(), E->getExprLoc()); + if (const auto *M = dyn_cast(E)) { - if (M->isArrow()) - return std::nullopt; const auto *FD = dyn_cast(M->getMemberDecl()); auto Offset = recordFieldOffset(FD); - auto Base = promotedObjectPlace(M->getBase()); + auto Base = M->isArrow() ? pointeePlace(M->getBase(), M->getExprLoc()) + : objectPlace(M->getBase()); if (!Base) return std::nullopt; if (!Offset) { - error(CurrentFn->Name + - ": unsupported field selection on an automatic object"); + error(CurrentFn->Name + ": unsupported field selection"); return std::nullopt; } Base->applyField(FD->getNameAsString(), *Offset, M->getExprLoc()); @@ -3491,11 +3562,14 @@ ASTConverter::promotedObjectPlace(const Expr *E) { const Expr *ArrayExpr = peelObjectExpr(AS->getBase()); const ConstantArrayType *CAT = ArrayExpr ? Ctx.getAsConstantArrayType(ArrayExpr->getType()) : nullptr; - auto Base = promotedObjectPlace(ArrayExpr); + // p[k] selects an element of the objects p addresses. + if (!CAT && AS->getBase()->getType()->isPointerType()) + return pointerElementPlace(AS); + auto Base = objectPlace(ArrayExpr); if (!Base) return std::nullopt; if (!CAT) { - error(CurrentFn->Name + ": unsupported indexing of an automatic object"); + error(CurrentFn->Name + ": unsupported indexing"); return std::nullopt; } const uint64_t Count = CAT->getSize().getZExtValue(); @@ -3742,7 +3816,7 @@ std::optional ASTConverter::lvaluePlace(const Expr *E) { // A promoted local has exactly one representation: every subobject lvalue // rooted in it is an exact byte offset from its single automatic object. if (promotedRootLocal(E)) - return promotedObjectPlace(E); + return objectPlace(E); if (const auto *DRE = dyn_cast(E)) { const auto *VD = dyn_cast(DRE->getDecl()); @@ -3789,33 +3863,16 @@ std::optional ASTConverter::lvaluePlace(const Expr *E) { return derefPlace(U->getSubExpr(), E->getExprLoc()); } - if (const auto *M = dyn_cast(E)) { - const Expr *Pointer = nullptr; - if (M->isArrow()) { - Pointer = M->getBase(); - } else if (const auto *Deref = - dyn_cast(M->getBase()->IgnoreParenImpCasts()); - Deref && Deref->getOpcode() == UO_Deref) { - Pointer = Deref->getSubExpr(); - } - const auto *PointerRef = - Pointer ? dyn_cast(Pointer->IgnoreParenImpCasts()) - : nullptr; - const auto *PointerVar = - PointerRef ? dyn_cast(PointerRef->getDecl()) : nullptr; - if (!PointerVar || !PointerVar->getType()->isPointerType()) - return std::nullopt; - return arrowFieldPlace(M); - } - - if (const auto *AS = dyn_cast(E)) { + // A subobject of the object a pointer variable addresses: p->f, p[i], + // p->inner.x, p->buf[i], p[k].grid[i][j]. + if (const Expr *Pointer = pointeeRootPointer(E)) { const auto *PointerRef = - dyn_cast(AS->getBase()->IgnoreParenImpCasts()); + dyn_cast(Pointer->IgnoreParenImpCasts()); const auto *PointerVar = PointerRef ? dyn_cast(PointerRef->getDecl()) : nullptr; if (!PointerVar || !PointerVar->getType()->isPointerType()) return std::nullopt; - return subscriptPlace(AS); + return objectPlace(E); } return std::nullopt; @@ -4367,9 +4424,7 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { return convertExpr(MTE->getSubExpr()); if (const auto *Decay = dyn_cast(E); Decay && Decay->getCastKind() == CK_ArrayToPointerDecay) { - error(CurrentFn->Name + - ": array-to-pointer decay of automatic storage is unsupported until " - "lexical lifetime and escape effects are modeled"); + error(CurrentFn->Name + ": " + arrayDecayError(Decay->getSubExpr())); return nullptr; } if (isa(E)) { @@ -4844,14 +4899,18 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { return std::make_unique(std::move(Address), Ty, E->getExprLoc()); } - if (!M->isArrow() && promotedRootLocal(M)) { + if (!M->isArrow() && (promotedRootLocal(M) || pointeeRootPointer(M))) { VType Ty = VType::fromQualType(E->getType(), IntMode, Ctx); if (Ty.isAggregate() || Ty.Kind == VTypeKind::Unsupported) { - error(CurrentFn->Name + ": aggregate value use of an automatic object " - "subobject is unsupported"); + error(CurrentFn->Name + + (promotedRootLocal(M) + ? ": aggregate value use of an automatic object " + "subobject is unsupported" + : ": a record or array read as a whole through a " + "pointer is unsupported; read its fields")); return nullptr; } - auto Place = promotedObjectPlace(M); + auto Place = objectPlace(M); if (!Place) return nullptr; return std::make_unique(Place->takeAddress(), Ty, @@ -5375,7 +5434,7 @@ void ASTConverter::appendAssignment(const Expr *LHS, return; } const size_t ErrorCount = Errors.size(); - auto Place = promotedObjectPlace(LHS); + auto Place = objectPlace(LHS); if (!Place) { if (Errors.size() == ErrorCount) error(CurrentFn->Name + ": unsupported assignment target"); @@ -5462,6 +5521,11 @@ void ASTConverter::appendAssignment(const Expr *LHS, std::move(Value), Loc)); return; } + // A field inside the object a pointer addresses: p->inner.x, p[k].f. + if (!ME->isArrow() && pointeeRootPointer(ME)) { + appendPointeeStore(LHS, std::move(Value), Loc, Out); + return; + } const auto *FD = dyn_cast(ME->getMemberDecl()); const auto *DRE = dyn_cast(ME->getBase()->IgnoreParenImpCasts()); @@ -5512,6 +5576,10 @@ void ASTConverter::appendAssignment(const Expr *LHS, ": proof functions cannot modify executable memory"); return; } + if (pointeeRootPointer(AS->getBase())) { + appendPointeeStore(LHS, std::move(Value), Loc, Out); + return; + } const size_t ErrorCount = Errors.size(); if (auto Address = convertSubscriptAddress(AS)) { Out.push_back(std::make_unique(std::move(Address), @@ -5525,6 +5593,31 @@ void ASTConverter::appendAssignment(const Expr *LHS, error(CurrentFn->Name + ": unsupported assignment target"); } +void ASTConverter::appendPointeeStore( + const Expr *LHS, std::unique_ptr Value, SourceLocation Loc, + std::vector> &Out) { + if (CurrentFn->IsProof) { + error(CurrentFn->Name + + ": proof functions cannot modify executable memory"); + return; + } + if (Value->Ty.isAggregate() || + isPromotableAggregateType(LHS->getType(), Ctx)) { + error(CurrentFn->Name + ": aggregate assignment is unsupported"); + return; + } + const size_t ErrorCount = Errors.size(); + auto Place = objectPlace(LHS); + if (!Place) { + if (Errors.size() == ErrorCount) + error(CurrentFn->Name + ": unsupported assignment target"); + return; + } + Out.push_back(std::make_unique(Place->takeAddress(), + std::move(Value), Loc, + Place->takeAccessCondition())); +} + bool ASTConverter::appendRecordCopy(const Expr *Source, const VarDecl *Target, SourceLocation Loc, std::vector> &Out) { @@ -5546,7 +5639,7 @@ bool ASTConverter::appendRecordCopy(const Expr *Source, const VarDecl *Target, if (promotedRootLocal(Source) && Target->isLocalVarDeclOrParm() && TargetRecord && TargetRecord->getDefinition() && Ctx.hasSameUnqualifiedType(Target->getType(), Source->getType())) { - auto SourcePlace = promotedObjectPlace(Source); + auto SourcePlace = objectPlace(Source); if (!SourcePlace) return true; if (auto AccessCondition = SourcePlace->takeAccessCondition()) @@ -5663,7 +5756,7 @@ bool ASTConverter::appendObjectCopy(const Expr *Source, QualType Ty, // Copy from another promoted object: read every leaf out of its storage. if (promotedRootLocal(Lvalue)) { - auto SourcePlace = promotedObjectPlace(Lvalue); + auto SourcePlace = objectPlace(Lvalue); if (!SourcePlace) return false; if (auto AccessCondition = SourcePlace->takeAccessCondition()) @@ -6324,7 +6417,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { ": proof functions cannot modify executable memory"); return Out; } - auto Place = promotedObjectPlace(TargetExpr); + auto Place = objectPlace(TargetExpr); if (!Place) return Out; if (auto AccessCondition = Place->takeAccessCondition()) diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index 5adbc638ea..111754d205 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -149,13 +149,28 @@ class ASTConverter { std::optional derefPlace(const Expr *PointerExpr, SourceLocation Loc); std::optional arrowFieldPlace(const MemberExpr *M); std::optional subscriptPlace(const ArraySubscriptExpr *AS); + /// The object \p PointerExpr addresses, as the root of a selection. + std::optional pointeePlace(const Expr *PointerExpr, + SourceLocation Loc); + /// p[k]: the element of the objects p addresses, bounded by their extent. + std::optional pointerElementPlace(const ArraySubscriptExpr *AS); /// Root-object discovery: peel no-op casts, array-to-pointer decays, dot /// member chains and fixed-array subscripts down to the enclosing local /// object. Returns the root only when it was promoted to one automatic /// byte-addressed object. const VarDecl *promotedRootLocal(const Expr *E) const; - /// Build the exact byte-offset place of a subobject of a promoted local. - std::optional promotedObjectPlace(const Expr *E); + /// The pointer whose pointee a chain of field and fixed-array element + /// selections starts at (p in *p, p->m, p[k], (*p).a.b[i]); null when the + /// chain does not start at a pointee. + const Expr *pointeeRootPointer(const Expr *E) const; + /// 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; + /// 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 + /// array in the place's access condition. + std::optional objectPlace(const Expr *E); std::optional recordFieldOffset(const FieldDecl *FD) const; /// Visit every scalar/pointer leaf of a promoted object type in offset order. bool forEachObjectLeaf(QualType Ty, uint64_t Offset, @@ -226,6 +241,11 @@ class ASTConverter { void appendAssignment(const Expr *LHS, std::unique_ptr Value, SourceLocation Loc, std::vector> &Out); + /// A store to a field or fixed-array element inside the object a pointer + /// addresses, with the element bounds of the place. + void appendPointeeStore(const Expr *LHS, std::unique_ptr Value, + SourceLocation Loc, + std::vector> &Out); bool appendRecordCopy(const Expr *Source, const VarDecl *Target, SourceLocation Loc, std::vector> &Out); diff --git a/clang/test/Verify/suite/dynamic_loaded_values.cpp b/clang/test/Verify/suite/dynamic_loaded_values.cpp index 535862cb25..3be1a2bfd4 100644 --- a/clang/test/Verify/suite/dynamic_loaded_values.cpp +++ b/clang/test/Verify/suite/dynamic_loaded_values.cpp @@ -94,5 +94,5 @@ int global_index(int a) delete p; return r; } -// GLOBAL: error: global_index: array-to-pointer decay +// GLOBAL: error: global_index: the global array 'table' is unsupported #endif diff --git a/clang/test/Verify/suite/pointer_subobjects.cpp b/clang/test/Verify/suite/pointer_subobjects.cpp new file mode 100644 index 0000000000..17d1cc186e --- /dev/null +++ b/clang/test/Verify/suite/pointer_subobjects.cpp @@ -0,0 +1,314 @@ +// 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 -- -DDECAY 2>&1 \ +// RUN: | FileCheck %s --check-prefix=DECAY +// +// Fields and fixed-array elements inside the object a pointer addresses, at +// any depth. Each index is bounded by its own array, so an index one past an +// array fails though its address is still inside the object. + +struct Inner { + int x; + int y; + int arr[4]; +}; + +struct Item { + int v; + int w; +}; + +struct Outer { + int buf[8]; + Inner inner; + int grid[3][4]; + Item items[5]; +}; + +struct Ring { + int buf[8]; + int head; + int count; +}; + +#ifndef DECAY +int peek(const Ring *r) + cppverify::pre(r != nullptr && 0 <= r->head && r->head < 8) + cppverify::post(cppverify::result == r->buf[r->head]) +{ + return r->buf[r->head]; +} +// CHECK-DAG: Verified: peek [backend=z3] +// VCR-LABEL: fn peek +// VCR: return +// VCR-NEXT: load +// VCR-NEXT: + +// VCR-NEXT: + +// VCR-NEXT: r +// VCR-NEXT: 0 +// VCR-NEXT: * +// VCR-NEXT: cast +// VCR-NEXT: load +// VCR-NEXT: + +// VCR-NEXT: r +// VCR-NEXT: 32 +// VCR-NEXT: 4 +// VCR-NEXT: access_condition +// VCR-NEXT: && +// VCR-NEXT: >= +// VCR: < +// VCR: 32 +// VCR-NEXT: 8 + +void put(Ring *r, int v) + cppverify::pre(r != nullptr && 0 <= r->head && r->head < 8) + cppverify::modifies(r->buf[r->head]) + cppverify::post(r->buf[r->head] == v) + cppverify::post(r->head == cppverify::old(r->head)) + cppverify::post(r->count == cppverify::old(r->count)) +{ + r->buf[r->head] = v; +} +// CHECK-DAG: Verified: put [backend=z3] + +// A reference bound to an element, and an element passed by reference. +void put_ref(Ring *r, int v) + cppverify::pre(r != nullptr && 0 <= r->head && r->head < 8) + cppverify::modifies(r->buf[r->head]) + cppverify::post(r->buf[r->head] == v) +{ + int &slot = r->buf[r->head]; + slot = v; +} +// CHECK-DAG: Verified: put_ref [backend=z3] + +void bump(int &x) + cppverify::pre(x < 100) + cppverify::modifies(x) + cppverify::post(x == cppverify::old(x) + 1) +{ + x = x + 1; +} +// CHECK-DAG: Verified: bump [backend=z3] + +void bump_slot(Ring *r, int i) + cppverify::pre(r != nullptr && 0 <= i && i < 8 && r->buf[i] < 100) + cppverify::modifies(r->buf[i]) + cppverify::post(r->buf[i] == cppverify::old(r->buf[i]) + 1) + cppverify::post(r->head == cppverify::old(r->head)) +{ + bump(r->buf[i]); +} +// CHECK-DAG: Verified: bump_slot [backend=z3] + +int nested(const Outer *p, int i, int j, int k) + cppverify::pre(p != nullptr && 0 <= i && i < 3 && 0 <= j && j < 4) + cppverify::pre(0 <= k && k < 5) + cppverify::pre(0 <= p->inner.y && p->inner.y < 1000) + cppverify::pre(0 <= p->inner.arr[j] && p->inner.arr[j] < 1000) + cppverify::pre(0 <= p->grid[i][j] && p->grid[i][j] < 1000) + cppverify::pre(0 <= p->items[k].v && p->items[k].v < 1000) + cppverify::post(cppverify::result == p->inner.y + p->inner.arr[j] + + p->grid[i][j] + p->items[k].v) +{ + return p->inner.y + p->inner.arr[j] + p->grid[i][j] + (*p).items[k].v; +} +// CHECK-DAG: Verified: nested [backend=z3] + +// p[k] is an element of the extent; buf[i] an element of its array. +int element_of_extent(const Outer *p, int n, int k, int i) + cppverify::pre(cppverify::valid(p, n) && 0 <= k && k < n) + cppverify::pre(0 <= i && i < 8) + cppverify::post(cppverify::result == p[k].buf[i]) +{ + return p[k].buf[i]; +} +// CHECK-DAG: Verified: element_of_extent [backend=z3] + +void nested_write(Outer *p) + cppverify::pre(p != nullptr) + cppverify::modifies(p->inner.y) + cppverify::post(p->inner.y == 3 && p->inner.x == cppverify::old(p->inner.x)) +{ + p->inner.y = 3; +} +// CHECK-DAG: Verified: nested_write [backend=z3] + +void write_keeps_others(Outer *p, int i, int j) + cppverify::pre(p != nullptr && 0 <= i && i < 8 && 0 <= j && j < 8 && i != j) + cppverify::modifies(p->buf[i]) + cppverify::post(p->buf[j] == cppverify::old(p->buf[j])) + cppverify::post(p->inner.x == cppverify::old(p->inner.x)) +{ + p->buf[i] = 5; +} +// CHECK-DAG: Verified: write_keeps_others [backend=z3] + +void clear(Outer *p) + cppverify::pre(p != nullptr) + cppverify::modifies(p->buf[0 : 8]) + cppverify::post(cppverify::forall(k, 0, 8, p->buf[k] == 0)) + cppverify::post(p->inner.y == cppverify::old(p->inner.y)) +{ + for (int i = 0; i < 8; i = i + 1) + cppverify::invariant(0 <= i && i <= 8) + cppverify::invariant(cppverify::forall(k, 0, i, p->buf[k] == 0)) + cppverify::modifies(p->buf[0 : 8]) + cppverify::decreases(8 - i) + { + p->buf[i] = 0; + } +} +// CHECK-DAG: Verified: clear [backend=z3] + +int clear_then_read(Outer *p) + cppverify::pre(p != nullptr) + cppverify::modifies(p->buf[0 : 8]) + cppverify::post(cppverify::result == 0) +{ + int before = p->inner.y; + clear(p); + cppverify::check(p->inner.y == before); + return p->buf[3]; +} +// CHECK-DAG: Verified: clear_then_read [backend=z3] + +// A spec reads the elements through the pointer, in the state of each call. +cppverify::spec int total(const Ring *r, int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : total(r, n - 1) + r->buf[n - 1]; +} +// CHECK-DAG: Verified: spec decreases: total + +int first_two(const Ring *r) + cppverify::pre(r != nullptr && 0 <= r->buf[0] && r->buf[0] < 1000) + cppverify::pre(0 <= r->buf[1] && r->buf[1] < 1000) + cppverify::post(cppverify::result == total(r, 2)) +{ + return r->buf[0] + r->buf[1]; +} +// CHECK-DAG: Verified: first_two [backend=z3] + +void set_first(Ring *r) + cppverify::pre(r != nullptr) + cppverify::modifies(r->buf[0]) + cppverify::post(total(r, 1) == 5) +{ + r->buf[0] = 5; +} +// CHECK-DAG: Verified: set_first [backend=z3] + +// One past the array: the address is p->inner.x, inside *p. +int past_end(const Outer *p, int i) + cppverify::pre(p != nullptr && 0 <= i && i <= 8) +{ + return p->buf[i]; +} +// CHECK-DAG: error: verification failed: past_end [{{.*}}::bounds@[[@LINE-2]]:3] (counterexample: i [ssa=i_0] [type=i32] = 8, + +int below_zero(const Outer *p, int i) + cppverify::pre(p != nullptr && -1 <= i && i < 8) +{ + return p->buf[i]; +} +// CHECK-DAG: error: verification failed: below_zero [{{.*}}::bounds@[[@LINE-2]]:10] (counterexample: i [ssa=i_0] [type=i32] = -1, + +// A postcondition's reads are checked like the body's. +int post_past_end(const Ring *r, int i) + cppverify::pre(r != nullptr && 0 <= i && i <= 8) + cppverify::post(r->buf[i] >= cppverify::result || r->buf[i] < cppverify::result) +{ + return 0; +} +// CHECK-DAG: error: verification failed: post_past_end [{{.*}}::bounds@[[@LINE-4]]:50] (counterexample: {{.*}}i [ssa=i_0] [type=i32] = 8, + +// grid[i][4] is grid[i + 1][0] in memory, but j indexes a row of 4. +int row_overflow(const Outer *p, int i, int j) + cppverify::pre(p != nullptr && 0 <= i && i < 3 && 0 <= j && j <= 4) +{ + return p->grid[i][j]; +} +// CHECK-DAG: error: verification failed: row_overflow [{{.*}}::bounds@[[@LINE-2]]:3] (counterexample: i [ssa=i_0] [type=i32] = {{[0-2]}}, j [ssa=j_0] [type=i32] = 4, + +void store_past_end(Outer *p, int i) + cppverify::pre(p != nullptr && 0 <= i && i <= 8) + cppverify::modifies(*p) +{ + p->buf[i] = 0; +} +// CHECK-DAG: error: verification failed: store_past_end [{{.*}}::bounds@[[@LINE-2]]:13] (counterexample: i [ssa=i_0] [type=i32] = 8, + +void slot_past_end(Ring *r, int i) + cppverify::pre(r != nullptr && 0 <= i && i <= 8) + cppverify::modifies(*r) +{ + int &slot = r->buf[i]; + slot = 0; +} +// CHECK-DAG: error: verification failed: slot_past_end [{{.*}}::bounds@[[@LINE-3]]:3] (counterexample: i [ssa=i_0] [type=i32] = 8, + +void bump_past_end(Ring *r, int i) + cppverify::pre(r != nullptr && 0 <= i && i <= 8 && r->head < 100) + cppverify::modifies(*r) +{ + bump(r->buf[i]); +} +// CHECK-DAG: error: verification failed: bump_past_end [{{.*}}::bounds@[[@LINE-2]]:8] (counterexample: i [ssa=i_0] [type=i32] = 8, + +// A write to buf[i] may be the read of buf[j]. +void write_keeps_all(Outer *p, int i, int j) + cppverify::pre(p != nullptr && 0 <= i && i < 8 && 0 <= j && j < 8) + cppverify::modifies(p->buf[i]) + cppverify::post(p->buf[j] == cppverify::old(p->buf[j])) +{ + p->buf[i] = 7; +} +// CHECK-DAG: error: verification failed: write_keeps_all [{{.*}}::postcondition@[[@LINE-4]]:29] (counterexample: i [ssa=i_0] [type=i32] = [[I:[0-7]]], j [ssa=j_0] [type=i32] = [[I]], + +void outside_frame(Outer *p, int i) + cppverify::pre(p != nullptr && 0 <= i && i < 8) + cppverify::modifies(p->inner.x) +{ + p->buf[i] = 0; +} +// CHECK-DAG: error: verification failed: outside_frame [{{.*}}::frame@[[@LINE-2]]:13] + +void nested_write_wrong(Outer *p) + cppverify::pre(p != nullptr) + cppverify::modifies(p->inner.y) + cppverify::post(p->inner.y == cppverify::old(p->inner.y)) +{ + p->inner.y = 3; +} +// 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]; + +int global_member(int i) + cppverify::pre(0 <= i && i < 8) +{ + return global_ring.buf[i]; +} +// DECAY-DAG: pointer_subobjects.cpp:[[@LINE-2]]:10: error: global_member: the array member 'buf' of the global 'global_ring' is unsupported + +int global_array(int i) + cppverify::pre(0 <= i && i < 4) +{ + return global_table[i]; +} +// DECAY-DAG: pointer_subobjects.cpp:[[@LINE-2]]:10: error: global_array: the global array 'global_table' is unsupported +#endif diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 0f8c06e74f..e021844d19 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -142,7 +142,7 @@ VExpr = | InitializedPtr(ptr, initializationHeap?) | Cast(inner: VExpr, fromType: VType, toType: VType) | FieldAccess(base: VExpr, field: string, type) - | Load(ptr: VExpr, type) // *p in an expression context + | Load(ptr: VExpr, type, accessCondition?) // *p in an expression context | HeapStore(before, after, ptr, value) // passive heap relation | HeapFrame(before, after, [(lo, hi)]) // passive frame relation | SpecCall(identity, args: [VExpr], type) @@ -163,6 +163,19 @@ All carry `SourceLocation` for diagnostics. `(select mem p)`. For `p[i]`, the selected address is `p + mathematical_value(i) * pointeeSizeBytes`. +**Places inside objects:** a field or fixed-array element inside an object is +a `VPlace`: the object's address plus Clang's layout offset for each field and +`index * stride` for each element, at any depth, with an access condition, +the conjunction of `0 <= index < count` over the fixed-array indices of the +path. A `Load` or `Store` of the place carries the condition, and +passivization asserts it, kind `bounds`, where the access is evaluated. The +object is a promoted local (`ASTConverter::objectPlace` on its allocation) or +the object a pointer addresses: `pointeeRootPointer` walks the place down to +`p->`, `(*p).`, or `p[k].`, and `pointeePlace` takes that pointer as the base, +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. + **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 @@ -196,7 +209,7 @@ every address outside the half-open regions. VStmt = | VarDecl(name, type, init: VExpr?) | Assign(target, value: VExpr) // local variable - | Store(ptr: VExpr, value: VExpr) // *p = value + | Store(ptr: VExpr, value: VExpr, accessCondition?) // *p = value | Allocate(target, allocatedType, init?, sizeBytes, alignBytes) | Free(ptr: VExpr) | If(cond: VExpr, then: [VStmt], else: [VStmt]) @@ -1724,7 +1737,8 @@ lexical closing brace and on each supported early return in reverse construction order, after materializing any heap-reading return value. Scalar references may bind fields and fixed-array elements with access-local nested bounds. General escape, raw array decay/address-taking, aggregate references, and addressable -declarations inside loops remain fail-closed. Automatic metadata transitions +declarations inside loops remain fail-closed; so does the decay of an array +member through a pointer (`ASTConverter::arrayDecayError` names which). Automatic metadata transitions are private and a modular caller may frame them away. Local reference declarations snapshot their VCR address in a marked diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 030e261ba3..c6d0feab6d 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1078,6 +1078,39 @@ loop. Recursive executable bodies may store through pointer and reference parameters and use automatic objects; recursion through a function that allocates or frees storage is `Unresolved` (`construct.unsupported`). +### 3b. Records through pointers + +```cpp +struct Ring { int buf[8]; int head; int count; }; + +void put(Ring *r, int v) + cppverify::pre(r != nullptr && 0 <= r->head && r->head < 8) + cppverify::modifies(r->buf[r->head]) + cppverify::post(r->buf[r->head] == v && r->count == cppverify::old(r->count)) +{ + r->buf[r->head] = v; +} +``` + +- A field or fixed-array element of the object a pointer addresses, at any + depth (`p->f`, `p->inner.arr[j]`, `p->grid[i][j]`, `(*p).items[k].v`, + `p[k].buf[i]`), is one heap cell: the pointer plus the record layout's + byte offsets and each index times its element size. Reads, writes, + contracts, `cppverify::modifies` footprints, reference bindings, and + reference arguments use it like any other cell. +- Each access has two checks, as Frama-C's RTE plugin generates + `index_bound` beside `\valid`: every fixed-array index lies in its own + array (`0 <= i < 8`, kind `bounds`), and the address lies in the pointer's + object, its `valid(p, n)` extent or one object (`--check-ub`). The first + 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. + ### 4. `cppverify::modifies(...)` frame condition ```cpp @@ -1102,9 +1135,12 @@ void incr_first(int* a, int* b) `cppverify::modifies` cannot call it, and a caller without one forgets every cell. With a `valid` extent on such a callee the call is not supported. - Footprints: - - a cell: scalar `ref`, `p->field`, or `p[i]`, at its exact address; + - a cell: scalar `ref`, `p->field`, `p[i]`, or a field or array element + inside the record `p` addresses (`p->inner.x`, `p->buf[i]`), at its exact + address; - a range `p[lo : n]`: the `n` elements from `p[lo]`, half-open - `[lo, lo + n)` (Clang's array-section syntax); + `[lo, lo + n)` (Clang's array-section syntax), and likewise + `p->buf[lo : n]` for an array member; - a region `*p`: the object `p` addresses, which is its `valid(p, n)` extent when it has one and otherwise one object. A region of a single scalar object is one cell. @@ -1255,9 +1291,12 @@ Interval shift(Interval r, int d) - No new syntax. `cppverify::spec` functions named `view()`, `elem()`, `size()`, etc. are a documented convention. - The verifier treats these spec function bodies as axioms (definitions), not as code to execute. - This is Verus's main abstraction idiom and the recommended style for non-trivial data structures. -- Records are passed by value with scalar fields; a record holding an array - or a pointer is not yet in the verified subset, so a view of a buffer is a - spec over the pointer and its length (`cppverify::spec int sum(const int *p, int n)`). +- A record passed by value has scalar fields. One that holds an array is + reached through a pointer, field by field and element by element, so its + view is a spec over that pointer + (`cppverify::spec int total(const Ring *r, int n)` reading `r->buf[n - 1]`), + as a view of a buffer is a spec over the pointer and its length + (`cppverify::spec int sum(const int *p, int n)`). ## Integer Semantics — summary @@ -1868,7 +1907,8 @@ Subsequent bounded lifetime checkpoints added scalar `new`/`delete`, initialized-storage checks, aligned disjoint allocation, use-after-delete/double-delete rejection, first-class local provenance, and inferred fresh-owned scalar factory returns. Bounded promoted local objects, -fixed arrays, scalar subobject references, modular slices, and general +fixed arrays, scalar subobject references, the fields and fixed-array +elements of a record a pointer addresses, modular slices, and general same-array pointer difference under `valid(p, n)` are also supported. Provenance across ownership-taking or recursive interfaces, pointer reinterpretation/cross-object arithmetic, aggregate/rvalue references, 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 9ad39675fb..cf3f98896f 100644 --- a/website/source/book/part-ii/ch14-pointers-frames-modifies.rst +++ b/website/source/book/part-ii/ch14-pointers-frames-modifies.rst @@ -201,6 +201,80 @@ which the verifier derives from the non-overlap as plain integer arithmetic (``d + j < d + n <= s <= s + i``), because addresses are modeled as mathematical integers rather than wrapping machine words. +Records through pointers +------------------------ + +A record often holds its storage inline: a fixed-capacity stack keeps its +items in an array member next to its size. Through a pointer to such a +record, every field and every array element is a heap cell of its own, at +the address the record layout gives it. Code reads and writes it, contracts +and footprints name it, and the same frame reasoning as for a buffer applies: + +.. cppverify-example: fails push_full + +.. code-block:: cpp + + struct Stack { + int items[16]; + int size; + }; + + void push(Stack *s, int v) + cv::pre(s != nullptr && 0 <= s->size && s->size < 16) + cv::modifies(s->items[s->size], s->size) + cv::post(s->size == cv::old(s->size) + 1) + cv::post(s->items[cv::old(s->size)] == v) + cv::post(cv::forall(k, 0, cv::old(s->size), s->items[k] == cv::old(s->items[k]))) + { + s->items[s->size] = v; + s->size = s->size + 1; + } + + void clear(Stack *s) + cv::pre(s != nullptr) + cv::modifies(s->items[0 : 16], s->size) + cv::post(s->size == 0 && cv::forall(k, 0, 16, s->items[k] == 0)) + { + for (int i = 0; i < 16; i = i + 1) + cv::invariant(0 <= i && i <= 16 && cv::forall(k, 0, i, s->items[k] == 0)) + cv::modifies(s->items[0 : 16]) + cv::decreases(16 - i) + { + s->items[i] = 0; + } + s->size = 0; + } + + void push_full(Stack *s, int v) + cv::pre(s != nullptr && 0 <= s->size && s->size <= 16) + cv::modifies(*s) + { + s->items[s->size] = v; + s->size = s->size + 1; + } + +.. code-block:: text + + Verified: push [backend=z3] + Verified: clear [backend=z3] + stack.cpp:36:21: error: verification failed: push_full [...::bounds@36:21] (counterexample: s [ssa=s_0] [type=pointer] = 1; trace: heap-write.store@36:21 address=65 value=) [backend=z3] [reason=counterexample] + +``push`` writes exactly two cells, so its postcondition can promise that every +item below the old size is unchanged. ``clear`` writes a range of the member +array and the size; ``s->items[0 : 16]`` is a range footprint like +``p[0 : n]``. + +``push_full`` admits a full stack. The store ``s->items[16]`` would land on +``s->size``, which is inside ``*s`` and inside the frame, so a check against +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. + Declaring a checked extent -------------------------- @@ -326,6 +400,7 @@ parameters — a frame condition on *values* rather than memory. Declare it afte It is injected as a precondition at the first use of an invariant field for supported by-value flat records, so callers must establish it. Record references are not yet in the verified subset; current references have scalar -referents only. See :doc:`../../language/structs`. +referents only, such as a field or an element reached through a pointer. See +:doc:`../../language/structs`. See :doc:`../../language/limitations` for the supported pointer and heap feature set. diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index ad12d3275e..971fb87a00 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -88,6 +88,8 @@ The most mature current fragment includes: - flat trivial standard-layout records with scalar fields; - 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``); - one-level typed pointers, abstract indexed buffers, and heap framing; - constrained direct scalar ``new``/``delete`` with liveness, initialization, and provenance. @@ -115,23 +117,28 @@ C++ feature boundaries functions, initialized ordinary scalar local actuals, local aliases for boolean, integral, and enum referents, and bindings to a field or fixed array element of a promoted local object, or to a field or element of - a parameter's buffer (``int &alias = p->second;``, ``p[i]``). + a parameter's buffer or of a record a pointer addresses + (``int &alias = p->second;``, ``p[i]``, ``p->buf[i]``). - Conditional bindings, reference returns, non-scalar referents, rvalue references, temporaries/lifetime extension, reference members, and forwarding. * - Arrays - - Pointer-parameter indexing, quantified abstract buffers, and fixed + - Pointer-parameter indexing, quantified abstract buffers, fixed local arrays (including arrays of records and multidimensional arrays) - modelled as byte-addressed automatic objects up to 256 bytes. + 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. - Array parameters/fields carried by value, array references, ``new[]``/``delete[]``, loop-local arrays, and raw pointers derived from - a local array. + a local array or from an array member (``int *q = p->buf;``). * - Records - Flat trivial standard-layout values with scalar fields; trivial standard-layout records with nested record, pointer, and fixed-array - members as promoted local objects. - - Non-trivial, inherited, polymorphic, union, and bit-field records, and - nested/pointer/array-bearing records used by value. + members as promoted local objects, and through pointers, where each + scalar field and element is a heap cell. + - Non-trivial, inherited, polymorphic, union, and bit-field records, + nested/pointer/array-bearing records used by value, and a whole record + or array read through a pointer (``Ring copy = *r;``). * - Functions - Free functions, overloads, namespaces, contracts, direct calls, and direct and mutual recursion, also through stores to pointer and diff --git a/website/source/language/pointers.rst b/website/source/language/pointers.rst index e9b0c758e5..73ec27234d 100644 --- a/website/source/language/pointers.rst +++ b/website/source/language/pointers.rst @@ -243,9 +243,12 @@ a *different* base pointer that is not in ``cppverify::modifies`` is still rejec A ``cppverify::modifies`` footprint is one of: -- a **cell**: ``p[i]``, ``p->field``, or a reference, at its exact address; +- a **cell**: ``p[i]``, ``p->field``, a field or array element inside the + record ``p`` addresses (``p->inner.x``, ``p->buf[i]``), or a reference, at + its exact address; - a **range** ``p[lo : n]``: the ``n`` elements from ``p[lo]``, half-open - ``[lo, lo + n)`` (Clang's array-section syntax); + ``[lo, lo + n)`` (Clang's array-section syntax), and likewise + ``p->buf[lo : n]`` for an array member (:doc:`structs`); - a **region** ``*p``: the object ``p`` addresses, which is its ``valid(p, n)`` extent when it has one and otherwise one object. diff --git a/website/source/language/structs.rst b/website/source/language/structs.rst index c9017c0aa9..cefe176650 100644 --- a/website/source/language/structs.rst +++ b/website/source/language/structs.rst @@ -13,6 +13,97 @@ member syntax: cv::post(cv::result >= 0) { return r.w * r.h; } +Records through pointers +------------------------ + +Through a pointer, every field and every element of a fixed array is +reachable, at any depth: ``p->f``, ``p->buf[i]``, ``p->inner.arr[j]``, +``p->grid[i][j]``, ``p->items[k].v``, ``(*p).buf[i]``, and ``p[k].buf[i]`` +for an element of a ``valid(p, n)`` extent. Each one is a single heap cell. +Code can read and write it, name it in a contract or a ``cppverify::modifies`` +footprint, bind a reference to it, and pass it to a reference parameter. + +.. cppverify-example: fails slot + +.. code-block:: cpp + + struct Ring { + int buf[8]; + int head; + int count; + }; + + int peek(const Ring *r) + cv::pre(r != nullptr && 0 <= r->head && r->head < 8) + cv::post(cv::result == r->buf[r->head]) + { + return r->buf[r->head]; + } + + void put(Ring *r, int v) + cv::pre(r != nullptr && 0 <= r->head && r->head < 8) + cv::modifies(r->buf[r->head]) + cv::post(r->buf[r->head] == v && r->count == cv::old(r->count)) + { + r->buf[r->head] = v; + } + + int slot(const Ring *r, int i) + cv::pre(r != nullptr && 0 <= i && i <= 8) + { + return r->buf[i]; + } + +.. code-block:: text + + Verified: peek [backend=z3] + Verified: put [backend=z3] + ring.cpp:25:3: error: verification failed: slot [...::bounds@25:3] (counterexample: i [ssa=i_0] [type=i32] = 8, r [ssa=r_0] [type=pointer] = 1; ...) [backend=z3] [reason=counterexample] + +Each index is checked against its own array, as Frama-C's RTE guards are, +and not only against the object. ``r->buf[8]`` has the address of +``r->head``, which lies inside ``*r``, and it is still an error. In +``p->grid[i][j]`` with ``int grid[3][4]``, both ``i < 3`` and ``j < 4`` must +hold, so ``grid[0][4]`` is rejected even though it has the address of +``grid[1][0]``. The check applies wherever an element is read or written: in +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: + +.. cppverify-example: rejects + +.. code-block:: cpp + + struct Ring { + int buf[8]; + int head; + int count; + }; + + int first(const int *p, int n) + cv::pre(cv::valid(p, n) && n >= 1) + cv::post(cv::result == p[0]) + { + return p[0]; + } + + int oldest(const Ring *r) + cv::pre(r != nullptr) + { + return first(r->buf, 8); + } + +.. 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); + | ^~~~~~ + ``cppverify::type_invariant`` ----------------------------- @@ -69,6 +160,8 @@ The current aggregate model is intentionally narrow. A record passed or returned by value must be trivial, standard-layout, and flat, with scalar 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. Reference +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 members, unions, bases, virtual dispatch, and non-trivial construction/destruction are rejected rather than approximated. diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 5a14924728..abac54c010 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -128,6 +128,16 @@ it into ``error: expected unqualified-id``. ``-fverify-contracts`` now defines targets unless the command line defines it, so the header defines only its ``__Check``, ``__Require``, and ``__Verify`` names (:doc:`language/syntax`). +**Records through pointers.** Through a pointer, 0.1.1 reached only a record's +direct fields (``p->x``). A nested field (``p->inner.y``), a field of an +element (``p[k].x``), and an element of an array member (``r->buf[i]``) were +errors, so a ring buffer, a fixed-capacity stack, or any record that holds its +storage inline could not be verified. Each of them is now a heap cell, at any +depth: code can read and write it, contracts and ``cppverify::modifies`` can +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`). + Running cpp-verify ~~~~~~~~~~~~~~~~~~