From 40f369d319d8b24cc30894819d26dc8a51e20ea1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 19:53:57 +0530 Subject: [PATCH 1/6] verify: Follow the body of a choose in a spec's reads and postcondition checks. --- clang/lib/Verify/Transform/SpecInline.cpp | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/clang/lib/Verify/Transform/SpecInline.cpp b/clang/lib/Verify/Transform/SpecInline.cpp index 9873c6f760..c7a86ef342 100644 --- a/clang/lib/Verify/Transform/SpecInline.cpp +++ b/clang/lib/Verify/Transform/SpecInline.cpp @@ -2013,6 +2013,8 @@ struct SpecBodyCollector { const FunctionMap &FnMap; std::vector Sites; std::vector Returns; + /// The witness bodies of the choices walked, which sites point into. + std::vector> Witnesses; bool Unsupported = false; void site(BodySite Site, @@ -2043,9 +2045,21 @@ struct SpecBodyCollector { for (const auto &Arg : C->Args) Site.Args.push_back(substParamsInExpr(Arg.get(), Env)); Site.Loc = C->Loc; + const VFunction *Callee = Site.Callee; site(std::move(Site), Env, Guard, Quantifiers); for (const auto &A : C->Args) expr(A.get(), Env, Guard, Quantifiers); + // A choose is evaluated where it is written: the loads and + // applications of its body, at every value of its binder, are the + // caller's. + if (Callee && Callee->IsChoice) { + if (std::unique_ptr Witness = choiceWitness(*Callee, *C)) { + Witnesses.push_back(std::move(Witness)); + expr(Witnesses.back().get(), Env, Guard, Quantifiers); + } else { + Unsupported = true; + } + } return; } case VExpr::Load: { @@ -2286,6 +2300,9 @@ PassiveProgram verify::buildReadsChecks(const VFunction &Fn, for (BodySite &Site : Collector.Sites) { if (!Site.Address && !Site.Call->ReadsHeap) continue; + // The loads of a choice's body are sites of their own. + if (!Site.Address && Site.Callee && Site.Callee->IsChoice) + continue; if (!Site.Address && (!Site.Callee || Site.Callee->Reads.empty())) { if (Missing.empty()) Missing = Site.Call->Callee; From 08220cb8f0fdc025ab2c95ed5c650e0c7a2b8fda Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 19:53:58 +0530 Subject: [PATCH 2/6] test: A reads clause covers the cells a choose's body loads. --- clang/test/Verify/suite/choose_reads.cpp | 66 ++++++++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 clang/test/Verify/suite/choose_reads.cpp diff --git a/clang/test/Verify/suite/choose_reads.cpp b/clang/test/Verify/suite/choose_reads.cpp new file mode 100644 index 0000000000..aecf91d746 --- /dev/null +++ b/clang/test/Verify/suite/choose_reads.cpp @@ -0,0 +1,66 @@ +// RUN: not %cpp-verify %s -- 2>&1 | FileCheck %s --implicit-check-not=Verified: +// +// The reads check of a spec follows the loads in the body of a choose it +// applies, at every value of the choice's binder, as Dafny checks the reads +// of a let-such-that. The choice itself reads nothing else. + +namespace cv = cppverify; +using namespace cppverify; + +cv::spec int index_of(const int *a, int n, int x) + cv::reads(a, n) +{ + return cv::choose(k, 0, n, a[k] == x); +} +// CHECK-DAG: Verified: spec reads: index_of +// CHECK-DAG: Verified: spec axiom: index_of + +// a[n] lies outside the declared cells. +cv::spec int index_past(const int *a, int n, int x) + cv::reads(a, n) +{ + return cv::choose(k, 0, n + 1, a[k] == x); +} +// CHECK-DAG: error: spec reads failed: index_past [backend=z3] [reason=counterexample] +// CHECK-DAG: Verified: spec axiom: index_past + +// Once the reads clause holds, a write outside it keeps the value. +void set_other(const int *a, int n, int *b, int x) + cv::pre(valid(a, n) && n >= 1 && n <= 100 && valid(b, 1)) + cv::modifies(*b) + cv::post(index_of(a, n, x) == cv::old(index_of(a, n, x))) +{ + cv::hide(index_of); + *b = 5; +} +// CHECK-DAG: Verified: set_other [backend=z3] + +cv::spec int count_to(const int *a, int n, int x) + cv::reads(a, n) + cv::decreases(n) +{ + return n <= 0 ? 0 + : cv::choose(k, 0, 2, k == (a[n - 1] == x ? 1 : 0)) + + count_to(a, n - 1, x); +} +// CHECK-DAG: Verified: spec reads: count_to +// CHECK-DAG: Verified: spec decreases: count_to + +void set_other_rec(const int *a, int n, int *b, int x) + cv::pre(valid(a, n) && n >= 1 && n <= 100 && valid(b, 1)) + cv::modifies(*b) + cv::post(count_to(a, n, x) == cv::old(count_to(a, n, x))) +{ + *b = 5; +} +// CHECK-DAG: Verified: set_other_rec [backend=z3] + +// A write inside the cells may change it. +void set_inside(int *a, int n, int x) + cv::pre(valid(a, n) && n >= 1 && n <= 100) + cv::modifies(a[0]) + cv::post(count_to(a, n, x) == cv::old(count_to(a, n, x))) +{ + a[0] = x == 0 ? 1 : 0; +} +// CHECK-DAG: error: verification failed: set_inside [{{.*}}::postcondition@[[@LINE-4]]:30] From 0d4b9cbb08e30dae644c562a6f04bf8927e0dfaa Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 19:53:58 +0530 Subject: [PATCH 3/6] test: The induction hypothesis holds at a call inside a choose. --- clang/test/Verify/suite/choose_axioms.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/clang/test/Verify/suite/choose_axioms.cpp b/clang/test/Verify/suite/choose_axioms.cpp index 5f7415ffc1..01b001304e 100644 --- a/clang/test/Verify/suite/choose_axioms.cpp +++ b/clang/test/Verify/suite/choose_axioms.cpp @@ -161,15 +161,15 @@ cppverify::spec int bit_block(int n) } // CHECK-DAG: Verified: spec decreases and post: bit_block -// Without that hypothesis the claim is not proved, but no choice its axiom -// excludes refutes it. +// The hypothesis also holds at an application inside the body of a choose, +// so no proof block is needed. cppverify::spec int bit_unblocked(int n) cppverify::decreases(n) cppverify::post(n < 0 || cppverify::result == cppverify::choose(k, 0, 2, k == n % 2)) { return n <= 1 ? n : cppverify::choose(j, 0, 2, j == bit_unblocked(n - 2)); } -// CHECK-DAG: Unresolved: spec decreases and post unresolved: bit_unblocked +// CHECK-DAG: Verified: spec decreases and post: bit_unblocked // In the definition instances refinement gives, where only the check of the // model's choices sees them. From 5a23d0e4979d8b7e2dd0d96378ee687e87809055 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 23:17:38 +0530 Subject: [PATCH 4/6] docs: A reads check follows the loads of a choose, with a frame it misses. --- website/source/language/ghost-proofs.rst | 31 ++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/website/source/language/ghost-proofs.rst b/website/source/language/ghost-proofs.rst index c3a8be1eae..37464446a4 100644 --- a/website/source/language/ghost-proofs.rst +++ b/website/source/language/ghost-proofs.rst @@ -261,6 +261,37 @@ parameters do not alias), so the store lies outside the frame. A failed ``cppverify::reads`` check is reported as ``spec reads failed: f`` for a spec ``f``, and every proof that relied on the frame is ``Unresolved`` with reason ``spec.reads``. +The check follows a ``cppverify::choose`` too: a choice reads the cells its +body loads, at every value of its binder in its range. ``index_of`` chooses +among ``a[0]`` to ``a[n - 1]``, inside its frame; ``index_past`` also reads +``a[n]``, outside it: + +.. cppverify-example: fails index_past + +.. code-block:: cpp + + cv::spec int index_of(const int *a, int n, int x) + cv::reads(a, n) + { + return cv::choose(k, 0, n, a[k] == x); + } + + cv::spec int index_past(const int *a, int n, int x) + cv::reads(a, n) + { + return cv::choose(k, 0, n + 1, a[k] == x); + } + +.. code-block:: text + + Verified: spec reads: index_of + Verified: spec axiom: index_of + reads.cpp:10:34: error: spec reads failed: index_past [backend=z3] [reason=counterexample] (a [type=pointer] = 0, n [type=math-i32] = 0) + Verified: spec axiom: index_past + +The counterexample is the empty buffer: with ``n = 0``, ``index_past`` reads +``a[0]``, and ``cppverify::reads(a, 0)`` declares no cell. + Opacity and fuel ---------------- From 51c72fb564ab2bc298c2a0aa8307615457e9694c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 23:17:39 +0530 Subject: [PATCH 5/6] docs: The induction hypothesis holds at a call inside a choose, in ch13. --- .../part-ii/ch13-spec-and-proof-functions.rst | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/website/source/book/part-ii/ch13-spec-and-proof-functions.rst b/website/source/book/part-ii/ch13-spec-and-proof-functions.rst index 2b41863930..963b7221e2 100644 --- a/website/source/book/part-ii/ch13-spec-and-proof-functions.rst +++ b/website/source/book/part-ii/ch13-spec-and-proof-functions.rst @@ -188,6 +188,30 @@ contradiction, and a proof that used it could prove anything. Before 0.2 the call inside the choose was not seen as a recursive call: ``stuck`` was accepted, and ``forty_two`` verified although it returns ``0`` at ``x = 1``. +A choice's body counts where the choice is written in a spec's other checks +too: the applications inside a choose get the same facts as the others, so a +postcondition proved by induction may use the hypothesis at a call written +inside a choose: + +.. code-block:: cpp + + cv::spec int bit(int n) + cv::decreases(n) + cv::post(n < 0 || cv::result == cv::choose(k, 0, 2, k == n % 2)) + { + return n <= 1 ? n : cv::choose(j, 0, 2, j == bit(n - 2)); + } + +.. code-block:: text + + Verified: spec decreases and post: bit + +For ``n > 1``, the hypothesis at ``bit(n - 2)`` says that it is the parity of +``n - 2``, ``0`` or ``1``. So the outer choice has a witness and is that +value, which is also the parity of ``n``. A ``cppverify::reads`` check +follows the loads of a choose's body in the same way +(:doc:`../../language/ghost-proofs`). + Spec functions may call each other in a cycle when they share a measure of the same length and every call within the cycle lowers it; the termination proof treats all of them From 4580c3fff017ae45a0b1c2fc980a0669d478fce9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 23:17:39 +0530 Subject: [PATCH 6/6] docs: Reads clauses over a choice hold now, in the release notes. --- website/source/release-notes.rst | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index b8abf5d90b..2203197162 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -100,6 +100,13 @@ say that a function writes its parameter first (:doc:`language/pointers`). Every choice a counterexample uses is now checked against its body (:doc:`book/part-ii/ch13-spec-and-proof-functions`). +**Reads clauses over a choice.** A spec whose body applies ``cv::choose`` to +memory failed its ``cppverify::reads`` check (``calls choose, which reads the +heap without a reads clause``), although its frame held every cell the choice +reads. The check now follows the loads of the choice's body, and the facts a +spec's checks assume, its induction hypothesis included, reach the +applications inside a choice too (:doc:`language/ghost-proofs`). + **Vacuity findings of downgraded results.** A result that is ``Unresolved`` because a fact it relies on is not established could still be marked ``[vacuous]``, from that very fact, and whether it was depended on the