verify: Follow the body of a choose in a spec's reads and postcondition checks

clang/lib/Verify/Transform/SpecInline.cpp

@@ -2013,6 +2013,8 @@ struct SpecBodyCollector {
   const FunctionMap &FnMap;
   std::vector<BodySite> Sites;
   std::vector<BodyReturn> Returns;
+  /// The witness bodies of the choices walked, which sites point into.
+  std::vector<std::unique_ptr<VExpr>> 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<VExpr> 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;

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.

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]

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

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

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