diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index fcfabb5a96..71c0e14fc6 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/clang/lib/Verify/Transform/Passivize.cpp @@ -3435,6 +3435,51 @@ class PassivizerImpl { return std::nullopt; } + /// In the object model a slice argument is valid storage where its bytes + /// [Actual, Actual + Bytes] lie in one of the caller's objects: those its + /// origins name when they are known, else any of them. Arg is the + /// argument as written, which carries the origins. + std::unique_ptr objectContainment( + const VExpr *Arg, const VExpr *Actual, std::unique_ptr Bytes, + const std::map &Renames, SourceLocation Loc) { + std::vector Objects; + auto Origins = pointerOrigins(Arg); + if (Origins && !Origins->empty() && !hasPointerProvenance(Arg)) { + for (const std::string &Origin : *Origins) { + if (isGlobalOrigin(Origin)) { + auto [Address, Size] = globalOriginExtent(Origin); + auto Start = + std::make_unique(Address, VType::makePtr(), Loc); + auto End = + addBytes(cloneVExpr(Start.get()), + std::make_unique(std::to_string(Size), + pointerOffsetType(), Loc), + Loc); + Objects.push_back(Region{std::move(Start), std::move(End)}); + } else if (auto Object = entryObjectRegion(Origin, Renames, Loc)) { + Objects.push_back(std::move(*Object)); + } + } + } else if (!hasPointerProvenance(Arg)) { + for (const AbstractObject &Object : abstractObjects(Fn)) + if (auto Region = entryObjectRegion(Object.Name, Renames, Loc)) + Objects.push_back(std::move(*Region)); + } + auto End = addBytes(cloneVExpr(Actual), std::move(Bytes), Loc); + std::unique_ptr Any = makeBoolLiteral(false, Loc); + for (Region &Object : Objects) + Any = makeOr(std::move(Any), + makeAnd(std::make_unique( + VBinOp::Le, std::move(Object.Lo), + cloneVExpr(Actual), VType::makeBool(), Loc), + std::make_unique( + VBinOp::Le, cloneVExpr(End.get()), + std::move(Object.Hi), VType::makeBool(), Loc), + Loc), + Loc); + return Any; + } + /// The region a write rooted at Root may reach, or nullopt when it cannot /// be bounded: a parameter's object or a global's cell. std::optional @@ -4751,6 +4796,25 @@ class PassivizerImpl { auto Contained = sliceContainment(Actual->second.get(), Length.get(), Extent.PointerType.PointeeSizeBytes, CallerExtents, C.Loc); + // A slice argument the syntactic rule cannot place (a copy, a choice, + // a callee's result) is contained through the objects it may address. + const VExpr *Arg = nullptr; + for (unsigned I = 0; I < Callee->Params.size() && I < C.Args.size(); ++I) + if (Callee->Params[I].first == Extent.Base) + Arg = C.Args[I].get(); + auto Bytes = scaledExtent(Length.get(), + Extent.PointerType.PointeeSizeBytes, C.Loc); + auto NonNegative = asPointerOffset(Length.get()); + if (Fn.ObjectModel && Arg && Bytes && NonNegative && + isFalseLiteral(Contained.get())) + Contained = makeAnd( + std::make_unique( + VBinOp::Ge, std::move(NonNegative), + std::make_unique(0, pointerOffsetType(), C.Loc), + VType::makeBool(), C.Loc), + objectContainment(Arg, Actual->second.get(), std::move(Bytes), + Renames, C.Loc), + C.Loc); emitPassive(P, PassiveStmt::Assert, std::move(Contained), nullptr, C.Loc, ProofObligationKind::Bounds); // A region write through an extent is framed by the extent itself @@ -4852,6 +4916,21 @@ class PassivizerImpl { std::set ContainedPointerParams; for (const VValidExtent &Extent : Callee->ValidExtents) ContainedPointerParams.insert(Extent.Base); + // Extent arguments not written from one of the caller's parameters: their + // validity follows from their containment in the caller's objects, not + // from a parameter's validity at entry. + std::set ObjectContainedParams; + for (unsigned I = 0; I < Callee->Params.size() && I < C.Args.size(); ++I) { + const VExpr *Base = pointerBase(C.Args[I].get()); + const bool FromParameter = + Base && Base->K == VExpr::Var && + llvm::any_of(Fn.Params, [&](const auto &Param) { + return Param.first == static_cast(Base)->Name; + }); + if (ContainedPointerParams.count(Callee->Params[I].first) && + !FromParameter) + ObjectContainedParams.insert(Callee->Params[I].first); + } for (size_t I = 0; I != Callee->Preconditions.size(); ++I) { const VExpr *Pre = Callee->Preconditions[I].get(); auto BoundPre = substParams(Pre, ParamMap, Ctx, EntryHeap, "", {}, @@ -4862,7 +4941,11 @@ class PassivizerImpl { // validity, which that membership gives. if (Fn.ObjectModel && (!Callee->ObjectModel || - llvm::none_of(ContainedPointerParams, [&](const std::string &Name) { + llvm::none_of(ContainedPointerParams, + [&](const std::string &Name) { + return referencesVar(Pre, Name); + }) || + llvm::any_of(ObjectContainedParams, [&](const std::string &Name) { return referencesVar(Pre, Name); }))) BoundPre = abstractValidity(std::move(BoundPre), Renames); diff --git a/clang/test/Verify/suite/slice_argument_objects.cpp b/clang/test/Verify/suite/slice_argument_objects.cpp new file mode 100644 index 0000000000..933e3c87af --- /dev/null +++ b/clang/test/Verify/suite/slice_argument_objects.cpp @@ -0,0 +1,181 @@ +// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s +// +// A slice argument lies in valid storage when its elements lie in one of the +// caller's objects, however the pointer was computed: a copy, a choice, a +// pointer stepped in a loop, or a callee's result. Before, only a parameter +// plus an offset written at the call was contained, and every other argument +// failed with a counterexample although the program was correct. + +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 count(const int *p, int n) + cppverify::pre(cppverify::valid(p, n) && n >= 0) + cppverify::post(cppverify::result == n) +{ + return n; +} +// CHECK-DAG: Verified: count [backend=z3] + +void zero2(int *p, int n) + cppverify::pre(cppverify::valid(p, n) && n >= 2) + cppverify::modifies(p[0 : 2]) + cppverify::post(p[0] == 0 && p[1] == 0) +{ + p[0] = 0; + p[1] = 0; +} +// CHECK-DAG: Verified: zero2 [backend=z3] + +const int *next(const int *a, int n) + cppverify::pre(cppverify::valid(a, n) && n >= 2) + cppverify::post(cppverify::result == a + 1) +{ + return a + 1; +} +// CHECK-DAG: Verified: next [backend=z3] + +const int *somewhere(const int *a, int n) + cppverify::pre(cppverify::valid(a, n) && n >= 2) + cppverify::post(cppverify::result != nullptr) +{ + return a + 1; +} +// CHECK-DAG: Verified: somewhere [backend=z3] + +int copied(const int *a) + cppverify::pre(cppverify::valid(a, 4)) + cppverify::post(cppverify::result == a[1]) +{ + const int *q = a + 1; + return first(q, 3); +} +// CHECK-DAG: Verified: copied [backend=z3] + +void copied_write(int *a) + cppverify::pre(cppverify::valid(a, 4)) + cppverify::modifies(a[0 : 4]) + cppverify::post(a[1] == 0 && a[2] == 0 && a[3] == cppverify::old(a[3])) +{ + int *q = a + 1; + zero2(q, 3); +} +// CHECK-DAG: Verified: copied_write [backend=z3] + +void chosen(int *a, int *b, bool c) + cppverify::pre(cppverify::valid(a, 4) && cppverify::valid(b, 4)) + cppverify::modifies(a[0 : 4], b[0 : 4]) +{ + int *q = c ? a + 1 : b; + zero2(q, 3); +} +// CHECK-DAG: Verified: chosen [backend=z3] + +int from_result(const int *a) + cppverify::pre(cppverify::valid(a, 4)) + cppverify::post(cppverify::result == a[1]) +{ + const int *q = next(a, 4); + return first(q, 3); +} +// CHECK-DAG: Verified: from_result [backend=z3] + +int one_past_empty(const int *a) + cppverify::pre(cppverify::valid(a, 4)) + cppverify::post(cppverify::result == 0) +{ + const int *q = a + 4; + return count(q, 0); +} +// CHECK-DAG: Verified: one_past_empty [backend=z3] + +int walked(const int *a, int n) + cppverify::pre(cppverify::valid(a, n) && n >= 2 && n <= 100) + cppverify::post(cppverify::result == a[n - 1]) +{ + const int *q = a; + int i = 0; + while (i < n - 1) + cppverify::invariant(0 <= i && i <= n - 1 && q == a + i) + cppverify::decreases(n - 1 - i) + { + q = q + 1; + i = i + 1; + } + return first(q, 1); +} +// CHECK-DAG: Verified: walked [backend=z3] + +// Three elements from a + 2 run past a + 4. +int copied_past(const int *a) + cppverify::pre(cppverify::valid(a, 4)) +{ + const int *q = a + 2; + return first(q, 3); +} +// CHECK-DAG: error: verification failed: copied_past [{{.*}}::bounds@[[@LINE-2]]:3] (counterexample: a [ssa=a_0] [type=pointer] = {{[0-9]+}}, q [ssa=q_1] [type=pointer] = {{[0-9]+}}; + +void copied_write_past(int *a) + cppverify::pre(cppverify::valid(a, 4)) + cppverify::modifies(a[0 : 4]) +{ + int *q = a + 2; + zero2(q, 3); +} +// CHECK-DAG: error: verification failed: copied_write_past [{{.*}}::bounds@[[@LINE-2]]:3] + +// When c is true, a + 2 has two elements left; b has four. +void chosen_past(int *a, int *b, bool c) + cppverify::pre(cppverify::valid(a, 4) && cppverify::valid(b, 4)) + cppverify::modifies(a[0 : 4], b[0 : 4]) +{ + int *q = c ? a + 2 : b; + zero2(q, 3); +} +// CHECK-DAG: error: verification failed: chosen_past [{{.*}}::bounds@[[@LINE-2]]:3] (counterexample: {{.*}}c [ssa=c_0] [type=bool] = true, + +// The callee's contract does not say where its result points. +int from_unknown(const int *a) + cppverify::pre(cppverify::valid(a, 4)) +{ + const int *q = somewhere(a, 4); + return first(q, 3); +} +// CHECK-DAG: error: verification failed: from_unknown [{{.*}}::bounds@[[@LINE-2]]:3] + +// The elements must start inside the object too: this result is one element +// before a, and the slice would end inside it. +[[cppverify::trusted]] const int *before(const int *a, int n) + cppverify::pre(cppverify::valid(a, n) && n >= 1) + cppverify::post(cppverify::result + 1 == a); +// CHECK-DAG: Trusted: before + +int from_before(const int *a) + cppverify::pre(cppverify::valid(a, 4)) +{ + const int *q = before(a, 4); + return first(q, 2); +} +// CHECK-DAG: error: verification failed: from_before [{{.*}}::bounds@[[@LINE-2]]:3] (counterexample: a [ssa=a_0] [type=pointer] = {{[0-9]+}}, q [ssa=q_1] [type=pointer] = {{[0-9]+}}; + +// A shorter walk leaves fewer elements than the call needs. +int walked_past(const int *a, int n) + cppverify::pre(cppverify::valid(a, n) && n >= 2 && n <= 100) +{ + const int *q = a; + int i = 0; + while (i < n - 1) + cppverify::invariant(0 <= i && i <= n - 1 && q == a + i) + cppverify::decreases(n - 1 - i) + { + q = q + 1; + i = i + 1; + } + return first(q, 2); +} +// CHECK-DAG: error: verification failed: walked_past [{{.*}}::bounds@[[@LINE-2]]:3] diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 0f8c06e74f..ea5cf78ffb 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1778,8 +1778,14 @@ position must lie in its origin's entry object, one past the end included The driver builds a UB-instrumented interface map before passivization so callee `VValidExtent` summaries are available at call sites. A slice actual is -lowered only after proving structural same-origin containment, including -nonnegative offset/length and the one-past empty case. A conservative transitive +lowered only after proving containment, including nonnegative offset/length +and the one-past empty case: structurally when it is written as a caller +parameter plus an offset (`sliceContainment`), and otherwise, in the object +model, by `[actual, actual + n * S]` lying in an entry object its origins name, +or in any of the caller's objects when they are unknown +(`Passivizer::objectContainment`). The callee's validity precondition for such +an argument is then discharged by the same membership (`abstractValidity`) +instead of a parameter's validity at entry. A conservative transitive body scan distinguishes acyclic read-only callees from unknown, recursive, or writing effects. Exact-cell writes reuse ordinary frame substitution; writes to a symbolic range or a whole sub-slice are supported, framed by a `HeapFrame` diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 030e261ba3..8e77a48f78 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -859,8 +859,12 @@ memory (no known origin), subtraction inside explicit specs or lifted casts remain rejected. At modular calls, a callee `valid(q, length)` extent can be instantiated from -`q = p + offset` only after proving a same-root nonnegative subrange with -`offset + length <= n`. Empty one-past slices, acyclic read-only forwarding, +an argument only after proving that its `length` elements lie in one of the +caller's objects: for `q = p + offset`, a nonnegative subrange with +`offset + length <= n`. A copy, a choice, a pointer stepped in a loop, or a +callee's result is contained through the objects its origins name, or any +caller object when they are unknown; validity is a property of storage, so +any object containing the elements establishes it. Empty one-past slices, acyclic read-only forwarding, exact-cell slice writes, and writes to a whole sub-slice or a symbolic range are supported; the call frames every cell outside the written region. 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..8ce173ae16 100644 --- a/website/source/book/part-ii/ch14-pointers-frames-modifies.rst +++ b/website/source/book/part-ii/ch14-pointers-frames-modifies.rst @@ -246,9 +246,12 @@ may be one caller array, which contracts cannot state, so their difference is explicit specs or lifted ``constexpr`` functions remain fail-closed. Extents also compose at modular calls. If a callee requires -``valid(q, length)`` and receives ``p + offset``, the caller must prove one -origin and ``0 <= offset``, ``0 <= length``, and -``offset + length <= n``. Empty one-past slices are legal. Read-only slice +``valid(q, length)``, the caller must prove that the ``length`` elements from +its argument lie in one of its objects: for ``p + offset`` from +``valid(p, n)``, that ``0 <= offset``, ``0 <= length``, and +``offset + length <= n``. The argument may also be a local copy, a choice +between pointers, or a pointer stepped in a loop; its elements must then lie +in the objects it may address. Empty one-past slices are legal. Read-only slice chains preserve the heap, while exact-cell effects such as ``cppverify::modifies(q[0])`` update only the corresponding caller cell, and a range or a whole-slice ``cppverify::modifies(*q)`` updates only the slice: diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst index 0aa0028263..7adf91713f 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -300,9 +300,12 @@ factory (see "Returning fresh ownership" in :doc:`ch19-dynamic-storage`); a call to a function that deallocates, or that has any other lifetime effect, fails closed (``Unresolved`` with reason ``construct.unsupported``). -``valid(p, n)`` extents also cross calls as checked sub-slices. Passing -``p + offset`` to a ``valid(q, length)`` formal asserts one root, nonnegative -offset and length, and ``offset + length <= n``. Empty one-past slices, +``valid(p, n)`` extents also cross calls as checked sub-slices. Passing an +argument to a ``valid(q, length)`` formal asserts that its ``length`` +elements lie in one of the caller's objects: for ``p + offset``, a +nonnegative offset and length and ``offset + length <= n``. A copy, a choice, +or a pointer stepped in a loop is checked against the objects it may +address. Empty one-past slices, exact-cell writes, ranges ``cppverify::modifies(q[lo : n])``, and whole-slice ``cppverify::modifies(*q)`` are supported; the call changes only the written cells of the slice. diff --git a/website/source/book/part-ii/ch18-undefined-behavior.rst b/website/source/book/part-ii/ch18-undefined-behavior.rst index 3f32986342..c0ea86940b 100644 --- a/website/source/book/part-ii/ch18-undefined-behavior.rst +++ b/website/source/book/part-ii/ch18-undefined-behavior.rst @@ -164,9 +164,10 @@ clause, ``p`` must be the bare complete-object pointer, and each pointer may have only one marker. Shifted, disjunctive, conditional, or duplicate markers are rejected instead of being interpreted as unconditional extents. -At a modular call, a callee extent ``valid(q, length)`` may be instantiated by -``q = p + offset`` only after proving the subrange is nonnegative and contained -in the caller's extent. The same inclusive ``[0, n]`` position proof governs +At a modular call, a callee extent ``valid(q, length)`` is instantiated by an +argument only after proving that its ``length`` elements are contained in one +of the caller's objects; for ``q = p + offset``, that the subrange is +nonnegative and contained in the caller's extent. The same inclusive ``[0, n]`` position proof governs same-array pointer subtraction, while dereferences keep the half-open ``[0, n)`` access rule. Pointer differences additionally prove that the element distance is representable by target ``ptrdiff_t``. diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index ad12d3275e..01bcab6ab9 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -356,9 +356,11 @@ such as ``cppverify::modifies(p[i])`` and ``cppverify::modifies(p->field)``, ran that may write memory forgets the whole value heap, as does a region footprint under ``--no-check-ub``. -A callee ``valid(q, length)`` extent can be instantiated from a caller -``valid(p, n)`` extent only after proving a same-root, nonnegative subrange -contained in ``[0, n]``. Empty one-past slices, transitive read-only +A callee ``valid(q, length)`` extent can be instantiated from an argument +only after proving that its elements lie in one of the caller's objects, such +as a nonnegative subrange of a ``valid(p, n)`` extent contained in +``[0, n]``; the argument may be a copy, a choice, a stepped pointer, or a +callee's result whose contract places it. Empty one-past slices, transitive read-only forwarding, exact-cell and range writes, and region writes through a sub-slice are supported; every cell outside the written slice keeps its value. diff --git a/website/source/language/pointers.rst b/website/source/language/pointers.rst index e9b0c758e5..4882652e01 100644 --- a/website/source/language/pointers.rst +++ b/website/source/language/pointers.rst @@ -692,10 +692,49 @@ With only ``q == a + i || q == b + i``, the invariant would allow ``q`` one past the end of ``a`` at the start of ``b`` while it came from ``a``, and the store there would be rejected. -The same marker composes across modular calls. Passing ``p + offset`` to a -callee with ``valid(q, length)`` requires a same-root proof of +The same marker composes across modular calls. An argument for a parameter +with ``valid(q, length)`` must have its ``length`` elements in one of the +caller's objects: passing ``p + offset`` from ``valid(p, n)`` requires ``0 <= offset``, ``0 <= length``, and ``offset + length <= n``. An empty slice -may start at ``p + n``. Read-only slice calls preserve the heap, including +may start at ``p + n``. The argument may be computed in any way, as a copy, a +choice, a pointer stepped in a loop, or a callee's result whose contract says +where it points; the elements must lie in the objects it may address: + +.. cppverify-example: fails third + +.. code-block:: cpp + + 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 second(const int *a, const int *b, bool from_a) + cv::pre(cv::valid(a, 4) && cv::valid(b, 3)) + cv::post(cv::result == (from_a ? a[1] : b[0])) + { + const int *q = from_a ? a + 1 : b; + return first(q, 3); + } + + int third(const int *a) + cv::pre(cv::valid(a, 4)) + { + const int *q = a + 2; + return first(q, 3); + } + +.. code-block:: text + + Verified: first [backend=z3] + Verified: second [backend=z3] + slices.cpp:20:3: error: verification failed: third [...::bounds@20:3] (counterexample: a [ssa=a_0] [type=pointer] = 1, q [ssa=q_1] [type=pointer] = 9; trace: call.first@20:3 arg0=9 arg1=3) [backend=z3] [reason=counterexample] + +``third`` passes three elements from ``a + 2``, of which only two are in +``a``: with ``a`` at address 1, ``q`` is 9, and the call would read up to +address 21, past ``a``'s end at 17. Read-only slice calls preserve the heap, including acyclic chains of read-only callees; exact-cell effects such as ``cppverify::modifies(q[0])``, ranges, and a whole-slice ``cppverify::modifies(*q)`` are also supported, and frame every cell of ``p`` outside the slice. diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 5a14924728..de3230f2b4 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -113,6 +113,19 @@ because a fact it relies on is not established could still be marked solver's search. Such findings are now dropped (:doc:`book/part-ii/ch16-when-verification-fails`). +**Slices passed through a copy.** A function that requires ``valid(p, n)`` +accepted an argument only when it was written as a parameter plus an offset, +as in ``first(a + 1, 3)``. Other arguments failed with a counterexample, even +when the program was correct: + +- a copy of such a pointer (``const int *q = a + 1; first(q, 3);``); +- a choice between pointers (``c ? a + 1 : b``); +- a pointer stepped in a loop; +- a result whose contract says where it points. + +Such an argument is now accepted when its elements lie in one of the caller's +objects (:doc:`language/pointers`). + C++ that compiles now ~~~~~~~~~~~~~~~~~~~~~