diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index 71c0e14fc6..2625dfe8ba 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/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(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(OuterBase)->Name == + static_cast(InnerBase)->Name; + if (Fn.ObjectModel && OuterIsRegion && !SameBase && Root && + Root->K == VExpr::Var) + if (auto Object = + parameterRegion(static_cast(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( + VBinOp::Le, std::move(Object->Lo), + std::move(Inner.Lo), VType::makeBool(), C.Loc), + std::make_unique( + 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, diff --git a/clang/test/Verify/suite/frame_call_objects.cpp b/clang/test/Verify/suite/frame_call_objects.cpp new file mode 100644 index 0000000000..8de22ab475 --- /dev/null +++ b/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] diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index f9bfef4e1f..1a2480d2f5 100644 --- a/docs/ARCHITECTURE.md +++ b/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 diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 1513eb5d30..7f988388bc 100644 --- a/docs/DESIGN.md +++ b/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 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 65b2ff8303..390d3a304e 100644 --- a/website/source/book/part-ii/ch14-pointers-frames-modifies.rst +++ b/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 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 7adf91713f..d4b421cce7 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/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 diff --git a/website/source/language/pointers.rst b/website/source/language/pointers.rst index 41faee042b..ae9f4256d1 100644 --- a/website/source/language/pointers.rst +++ b/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 diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index be0e97ae37..11bb85acb9 100644 --- a/website/source/release-notes.rst +++ b/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 ~~~~~~~~~~~~~~~~~~~~~