verify: Compare a callee footprint with the caller's frame by its cells

clang/lib/Verify/Transform/Passivize.cpp

@@ -3342,6 +3342,10 @@ class PassivizerImpl {
         return makeEq(cloneVExpr(OuterPtr), cloneVExpr(InnerPtr), Loc);
       if (InnerIsRange && InnerBytes)
         return Empty(*InnerBytes);
+      // A region of one scalar object is one cell.
+      if (InnerIsRegion && InnerBytes && InnerBytes->Cell)
+        return makeEq(cloneVExpr(OuterPtr), cloneVExpr(InnerBytes->Lo.get()),
+                      Loc);
       return makeBoolLiteral(false, Loc);
     }
     if (!InnerIsRegion && !InnerIsRange)
@@ -5041,14 +5045,51 @@ class PassivizerImpl {
           if (CallerCounts[J])
             OuterBytes = rangeBytes(CallerLoad->Ptr.get(), CallerCounts[J].get(),
                                     Fn.Modifies[J].ElementSize, C.Loc);
+          const bool OuterIsRegion =
+              isRegionFootprint(Fn.Modifies[J], Fn.ReferenceParams);
           Allowed = makeOr(
               std::move(Allowed),
-              footprintWithin(CallerLoad->Ptr.get(),
-                              isRegionFootprint(Fn.Modifies[J],
-                                                Fn.ReferenceParams),
-                              OuterBytes, ActualLoad->Ptr.get(), ActualIsRegion,
+              footprintWithin(CallerLoad->Ptr.get(), OuterIsRegion, OuterBytes,
+                              ActualLoad->Ptr.get(), ActualIsRegion,
                               ActualCounts[I] != nullptr, InnerBytes, C.Loc),
               C.Loc);
+          // A region is its parameter's object, as for a store: a callee
+          // footprint through another pointer (a copy of a pointer into the
+          // object) is inside where its cells lie in that object.
+          const VExpr *OuterBase = pointerBase(CallerLoad->Ptr.get());
+          const VExpr *InnerBase = pointerBase(ActualLoad->Ptr.get());
+          const auto *DeclaredLoad =
+              Fn.Modifies[J].Target && Fn.Modifies[J].Target->K == VExpr::Load
+                  ? static_cast<const VLoadExpr *>(Fn.Modifies[J].Target.get())
+                  : nullptr;
+          const VExpr *Root =
+              DeclaredLoad ? addressRoot(DeclaredLoad->Ptr.get()) : nullptr;
+          const bool SameBase =
+              OuterBase && InnerBase && OuterBase->K == VExpr::Var &&
+              InnerBase->K == VExpr::Var &&
+              static_cast<const VVarExpr *>(OuterBase)->Name ==
+                  static_cast<const VVarExpr *>(InnerBase)->Name;
+          if (Fn.ObjectModel && OuterIsRegion && !SameBase && Root &&
+              Root->K == VExpr::Var)
+            if (auto Object =
+                    parameterRegion(static_cast<const VVarExpr *>(Root)->Name,
+                                    Renames, C.Loc)) {
+              Region Inner = InnerBytes
+                                 ? Region{cloneVExpr(InnerBytes->Lo.get()),
+                                          cloneVExpr(InnerBytes->Hi.get()),
+                                          InnerBytes->Cell}
+                                 : cellRegion(ActualLoad->Ptr.get(),
+                                              ActualLoad->Ty, C.Loc);
+              auto Inside =
+                  makeAnd(std::make_unique<VBinOpExpr>(
+                              VBinOp::Le, std::move(Object->Lo),
+                              std::move(Inner.Lo), VType::makeBool(), C.Loc),
+                          std::make_unique<VBinOpExpr>(
+                              VBinOp::Le, std::move(Inner.Hi),
+                              std::move(Object->Hi), VType::makeBool(), C.Loc),
+                          C.Loc);
+              Allowed = makeOr(std::move(Allowed), std::move(Inside), C.Loc);
+            }
         }
       }
       emitPassive(P, PassiveStmt::Assert, std::move(Allowed), nullptr, C.Loc,

clang/test/Verify/suite/frame_call_objects.cpp

@@ -0,0 +1,181 @@
+// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s
+//
+// A callee's footprint lies in the caller's frame when its cells do,
+// whichever pointer reaches them. Before, a callee region of one scalar
+// object never lay in a caller cell, and a region reached through a copy
+// (q = a + 2) never lay in the caller's region of a, so these calls failed
+// their frame check although they wrote only what the caller may write.
+
+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]
+
+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]
+
+// The callee's region is the one cell the caller may write.
+void cell_frame(int *p)
+  cppverify::pre(p != nullptr)
+  cppverify::modifies(p[0])
+  cppverify::post(*p == 5)
+{
+  set(p, 5);
+}
+// CHECK-DAG: Verified: cell_frame [backend=z3]
+
+void element_frame(int *a)
+  cppverify::pre(cppverify::valid(a, 4))
+  cppverify::modifies(a[2])
+  cppverify::post(a[2] == 5 && a[1] == cppverify::old(a[1]))
+{
+  set(a + 2, 5);
+}
+// CHECK-DAG: Verified: element_frame [backend=z3]
+
+// A copy of a pointer into the region's object.
+void copy_region(int *a)
+  cppverify::pre(cppverify::valid(a, 4))
+  cppverify::modifies(*a)
+  cppverify::post(a[2] == 5)
+{
+  int *q = a + 2;
+  set(q, 5);
+}
+// CHECK-DAG: Verified: copy_region [backend=z3]
+
+void copy_range(int *a)
+  cppverify::pre(cppverify::valid(a, 4))
+  cppverify::modifies(*a)
+  cppverify::post(a[2] == 0 && a[3] == 0)
+{
+  int *q = a + 2;
+  zero2(q, 2);
+}
+// CHECK-DAG: Verified: copy_range [backend=z3]
+
+void chosen_region(int *a, int *b, bool c)
+  cppverify::pre(cppverify::valid(a, 4) && cppverify::valid(b, 4))
+  cppverify::modifies(*a, *b)
+{
+  int *q = c ? a + 1 : b + 3;
+  set(q, 5);
+}
+// CHECK-DAG: Verified: chosen_region [backend=z3]
+
+void clear(int *p, int n)
+  cppverify::pre(cppverify::valid(p, n))
+  cppverify::modifies(p[0 : n])
+{
+  for (int i = 0; i < n; i = i + 1)
+    cppverify::invariant(0 <= i && i <= n)
+    cppverify::modifies(p[0 : n])
+    cppverify::decreases(n - i)
+  {
+    p[i] = 0;
+  }
+}
+// CHECK-DAG: Verified: clear [backend=z3]
+
+// An empty range writes nothing, wherever it starts.
+void empty_elsewhere(int *a, int *b)
+  cppverify::pre(cppverify::valid(a, 4) && cppverify::valid(b, 4))
+  cppverify::modifies(*a)
+{
+  int *q = b + 4;
+  clear(q, 0);
+}
+// CHECK-DAG: Verified: empty_elsewhere [backend=z3]
+
+// The neighbor of the cell the caller may write.
+void neighbor_cell(int *a)
+  cppverify::pre(cppverify::valid(a, 4))
+  cppverify::modifies(a[2])
+{
+  set(a + 3, 5);
+}
+// CHECK-DAG: error: verification failed: neighbor_cell [{{.*}}::frame@[[@LINE-2]]:3]
+
+// A copy into another parameter's object, outside the caller's region.
+void other_object(int *a, int *b)
+  cppverify::pre(cppverify::valid(a, 4) && cppverify::valid(b, 4))
+  cppverify::modifies(*a)
+{
+  int *q = b + 1;
+  set(q, 5);
+}
+// CHECK-DAG: error: verification failed: other_object [{{.*}}::frame@[[@LINE-2]]:3]
+
+// The copy starts inside a's object only if b lay below it.
+void other_object_above(int *a, int *b)
+  cppverify::pre(cppverify::valid(a, 4) && cppverify::valid(b, 4) && a + 4 <= b)
+  cppverify::modifies(*a)
+{
+  int *q = b + 1;
+  set(q, 5);
+}
+// CHECK-DAG: error: verification failed: other_object_above [{{.*}}::frame@[[@LINE-2]]:3]
+
+// A callee may name more cells than its extent: these run past a's object.
+void wide(int *p)
+  cppverify::pre(cppverify::valid(p, 1))
+  cppverify::modifies(p[0 : 3])
+{
+  p[0] = 1;
+}
+// CHECK-DAG: Verified: wide [backend=z3]
+
+void wide_past(int *a)
+  cppverify::pre(cppverify::valid(a, 4))
+  cppverify::modifies(*a)
+{
+  int *q = a + 3;
+  wide(q);
+}
+// CHECK-DAG: error: verification failed: wide_past [{{.*}}::frame@[[@LINE-2]]:3]
+
+// When c is false the cell is in b, which the caller may not write.
+void chosen_outside(int *a, int *b, bool c)
+  cppverify::pre(cppverify::valid(a, 4) && cppverify::valid(b, 4))
+  cppverify::modifies(*a)
+{
+  int *q = c ? a + 1 : b + 3;
+  set(q, 5);
+}
+// CHECK-DAG: error: verification failed: chosen_outside [{{.*}}::frame@[[@LINE-2]]:3] (counterexample: {{.*}}c [ssa=c_0] [type=bool] = false,
+
+// The cell before the object, where its end would still be inside.
+[[cppverify::trusted]] int *before(const int *a, int n)
+  cppverify::pre(cppverify::valid(a, n) && n >= 1)
+  cppverify::post(cppverify::result != nullptr && cppverify::result + 1 == a);
+// CHECK-DAG: Trusted: before
+
+void before_object(int *a)
+  cppverify::pre(cppverify::valid(a, 4))
+  cppverify::modifies(*a)
+{
+  int *q = before(a, 4);
+  set(q, 5);
+}
+// CHECK-DAG: error: verification failed: before_object [{{.*}}::frame@[[@LINE-2]]:3]
+
+// The range a[3 : 2] runs past the cell a[3] the caller may write.
+void range_past_cell(int *a)
+  cppverify::pre(cppverify::valid(a, 5))
+  cppverify::modifies(a[3])
+{
+  int *q = a + 3;
+  zero2(q, 2);
+}
+// CHECK-DAG: error: verification failed: range_past_cell [{{.*}}::frame@[[@LINE-2]]:3]

docs/ARCHITECTURE.md

@@ -464,8 +464,11 @@ assume(Q[Result := y, Old(params) := args]);
   Cell footprints become stores of fresh values (no quantifier). In the
   object model, ranges and regions (the actual's `valid` extent, else one
   object) become `HeapFrame(mem_k, mem_{k+1}, regions)`; each footprint of
-  the callee must lie inside the caller's own frame (index-based
-  containment).
+  the callee must lie inside the caller's own frame, by its cells
+  (`footprintWithin`): a region of one scalar object is one cell, and a
+  footprint through a pointer of another base than a caller region's lies in
+  it where its cells lie in the region parameter's entry object, the rule a
+  store already follows.
 - If `cppverify::modifies` is the conservative default (all reachable through mut params), the entire heap is havocked.
 - A `freshOwnedReturn` call is not a whole-heap havoc. It preserves every old
   cell, materializes one disjoint initialized scalar object, then assumes the

docs/DESIGN.md

@@ -1150,8 +1150,11 @@ void incr_first(int* a, int* b)
     scalar object is one cell.
 - Inside the callee every store must lie in a footprint, read in the entry
   state, so reassigning a pointer cannot widen the frame; a footprint of a
-  callee must lie within the caller's own frame (index-based containment of
-  ranges and extents).
+  callee must lie within the caller's own frame, cell by cell: a region of
+  one scalar object is one cell, ranges and extents compare by their cells,
+  and a footprint reached through another pointer than a caller region's
+  (a copy of a pointer into the object) lies in that region when its cells
+  lie in the region's object, as a store does.
 - At a call, the caller's heap changes only inside the callee's footprints
   instantiated with the arguments: a cell or range is exactly those cells, a
   region is the argument's extent (or one object). Every other cell keeps its

website/source/book/part-ii/ch14-pointers-frames-modifies.rst

@@ -106,7 +106,10 @@ There are three frame granularities:
 Inside the function, every store must lie in a footprint read in the entry
 state. At a modular call, the caller's heap changes only inside the callee's
 footprints instantiated with the arguments, and every other cell keeps its
-value. A callee footprint must lie within the caller's own frame.
+value. A callee footprint must lie within the caller's own frame, cell by
+cell, however its pointer was computed: a callee that writes its one object
+may receive a cell the caller may write, or a copy of a pointer into an
+object the caller may write.
 
 A pointer-taking callee with no explicit ``cppverify::modifies`` that may write memory is
 treated as writing the whole heap: a caller may lose a true fact about an

website/source/book/part-ii/ch17-backends-modular-calls.rst

@@ -291,7 +291,8 @@ the object the argument addresses, its ``valid`` extent or else one object.
 Every other cell keeps its value, and the postcondition then re-establishes
 whatever the caller may rely on inside the footprints. Each footprint must
 also lie within the caller's own ``cppverify::modifies``, read in the caller's entry
-state. A callee without ``cppverify::modifies`` whose body (or a callee of it) may write
+state: its cells must be cells the caller may write, whichever pointer reaches
+them. A callee without ``cppverify::modifies`` whose body (or a callee of it) may write
 is treated as writing the whole heap; a conservative body scan keeps the heap
 for verified, acyclic read-only callees.
 A function that allocates or deallocates storage is verified as a standalone

website/source/language/pointers.rst

@@ -281,7 +281,56 @@ A callee writing a range or a whole slice frames the rest of the buffer:
      zero_middle(p, n, 1, 2);
    }
 
-Each callee footprint must lie within the caller's own frame. A pointer-taking
+Each callee footprint must lie within the caller's own frame, cell by cell,
+whichever pointer reaches it. A callee that writes its one object
+(``cv::modifies(*p)``) may be passed a cell the caller may write, or a copy of
+a pointer into an object the caller may write:
+
+.. cppverify-example: fails set_fourth
+
+.. code-block:: cpp
+
+   void put(int *p, int v)
+     cv::pre(p != nullptr)
+     cv::modifies(*p)
+     cv::post(*p == v)
+   {
+     *p = v;
+   }
+
+   void set_third(int *a)
+     cv::pre(cv::valid(a, 4))
+     cv::modifies(a[2])
+     cv::post(a[2] == 5 && a[1] == cv::old(a[1]))
+   {
+     put(a + 2, 5);
+   }
+
+   void set_through_copy(int *a)
+     cv::pre(cv::valid(a, 4))
+     cv::modifies(*a)
+     cv::post(a[2] == 5)
+   {
+     int *q = a + 2;
+     put(q, 5);
+   }
+
+   void set_fourth(int *a)
+     cv::pre(cv::valid(a, 4))
+     cv::modifies(a[2])
+   {
+     put(a + 3, 5);
+   }
+
+.. code-block:: text
+
+   Verified: put [backend=z3]
+   Verified: set_third [backend=z3]
+   Verified: set_through_copy [backend=z3]
+   frames.cpp:30:3: error: verification failed: set_fourth [...::frame@30:3] (counterexample: a [ssa=a_0] [type=pointer] = 1; trace: call.put@30:3 arg0=13 arg1=5) [backend=z3] [reason=counterexample]
+
+``set_fourth`` may write only ``a[2]``, at address 9 when ``a`` is 1, but
+passes ``a + 3``, address 13. A pointer-taking
 callee with no explicit ``cppverify::modifies`` that may write memory is treated as
 writing the whole heap, which cannot fit inside an explicit caller frame; an
 unframed caller may still call it. Under ``--no-check-ub`` a region footprint

website/source/release-notes.rst

@@ -126,6 +126,17 @@ when the program was correct:
 Such an argument is now accepted when its elements lie in one of the caller's
 objects (:doc:`language/pointers`).
 
+**Callee frames inside the caller's.** A call could fail its ``frame`` check
+although the callee writes only cells the caller may write, in two cases:
+
+- a callee that writes its one object (``modifies(*p)``) passed a cell the
+  caller may write, as in ``set(a + 2, 5)`` under ``modifies(a[2])``;
+- a pointer copied into an object the caller may write, as in
+  ``int *q = a + 2; set(q, 5);`` under ``modifies(*a)``.
+
+The callee's footprint is now compared with the caller's frame cell by cell
+(:doc:`language/pointers`).
+
 C++ that compiles now
 ~~~~~~~~~~~~~~~~~~~~~