verify: Contain a slice argument through the objects it may address

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<VExpr> objectContainment(
+      const VExpr *Arg, const VExpr *Actual, std::unique_ptr<VExpr> Bytes,
+      const std::map<std::string, std::string> &Renames, SourceLocation Loc) {
+    std::vector<Region> 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<VLiteralExpr>(Address, VType::makePtr(), Loc);
+          auto End =
+              addBytes(cloneVExpr(Start.get()),
+                       std::make_unique<VLiteralExpr>(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<VExpr> Any = makeBoolLiteral(false, Loc);
+    for (Region &Object : Objects)
+      Any = makeOr(std::move(Any),
+                   makeAnd(std::make_unique<VBinOpExpr>(
+                               VBinOp::Le, std::move(Object.Lo),
+                               cloneVExpr(Actual), VType::makeBool(), Loc),
+                           std::make_unique<VBinOpExpr>(
+                               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<Region>
@@ -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<VBinOpExpr>(
+                VBinOp::Ge, std::move(NonNegative),
+                std::make_unique<VLiteralExpr>(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<std::string> 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<std::string> 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<const VVarExpr *>(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);

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]

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`

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.
 

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:

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.

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``.

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.