verify: Reject valid(p, n) outside a precondition

clang/lib/Verify/Driver/Verifier.cpp

@@ -2157,6 +2157,8 @@ class Verifier {
             UnrolledFn = LoopUnroller::unroll(*PreparedFn, Opts.BMCUnroll);
             WorkFn = &*UnrolledFn;
           }
+        } else if (Opts.CheckUB && !Fn->IsBuiltin) {
+          UBError = misplacedValidMarker(*Fn);
         }
 
         if (UBError) {

clang/lib/Verify/Transform/UBChecks.cpp

@@ -1069,15 +1069,112 @@ bool verify::hasRepresentedRoot(const VExpr *E) {
 }
 
 bool verify::usesValidMarker(const VFunction &Fn) {
-  if (Fn.IsSpec)
-    return false;
   for (const auto &Pre : Fn.Preconditions)
     if (containsValidCall(Pre.get()))
       return true;
-  for (const auto &Post : Fn.Postconditions)
-    if (containsValidCall(Post.get()))
-      return true;
-  return false;
+  return misplacedValidMarker(Fn).has_value();
+}
+
+namespace {
+/// Finds the first valid(p, n) outside the preconditions, where it would be a
+/// spec whose body is `true`.
+struct MisplacedValidFinder {
+  const char *Where = nullptr;
+
+  void expr(const VExpr *E, const char *Position) {
+    if (!Where && containsValidCall(E))
+      Where = Position;
+  }
+
+  void stmts(const std::vector<std::unique_ptr<VStmt>> &Stmts, bool Ghost) {
+    for (const auto &S : Stmts) {
+      const char *Code = Ghost ? "ghost code" : "a function body";
+      switch (S->K) {
+      case VStmt::Assign:
+        expr(static_cast<const VAssignStmt &>(*S).Value.get(), Code);
+        break;
+      case VStmt::Store: {
+        const auto &St = static_cast<const VStoreStmt &>(*S);
+        expr(St.Ptr.get(), Code);
+        expr(St.Value.get(), Code);
+        break;
+      }
+      case VStmt::If: {
+        const auto &I = static_cast<const VIfStmt &>(*S);
+        expr(I.Cond.get(), Code);
+        stmts(I.Then, Ghost);
+        stmts(I.Else, Ghost);
+        break;
+      }
+      case VStmt::Assert:
+        expr(static_cast<const VAssertStmt &>(*S).Cond.get(),
+             "a cppverify::check");
+        break;
+      case VStmt::Assume:
+        expr(static_cast<const VAssumeStmt &>(*S).Cond.get(), Code);
+        break;
+      case VStmt::ContractAssert:
+        expr(static_cast<const VContractAssertStmt &>(*S).Cond.get(),
+             "a cppverify::check");
+        break;
+      case VStmt::Return:
+        expr(static_cast<const VReturnStmt &>(*S).Value.get(), Code);
+        break;
+      case VStmt::While: {
+        const auto &W = static_cast<const VWhileStmt &>(*S);
+        expr(W.Cond.get(), Code);
+        for (const auto &Inv : W.Invariants)
+          expr(Inv.get(), "a loop invariant");
+        for (const auto &Dec : W.Decreases)
+          expr(Dec.get(), "a cppverify::decreases");
+        for (const VFootprint &F : W.Modifies) {
+          expr(F.Target.get(), "a cppverify::modifies");
+          expr(F.Count.get(), "a cppverify::modifies");
+        }
+        stmts(W.Body, Ghost);
+        break;
+      }
+      case VStmt::Call:
+        for (const auto &Arg : static_cast<const VCallStmt &>(*S).Args)
+          expr(Arg.get(), Code);
+        break;
+      case VStmt::Seq:
+        stmts(static_cast<const VSeqStmt &>(*S).Stmts, Ghost);
+        break;
+      case VStmt::GhostBlock:
+        stmts(static_cast<const VGhostBlockStmt &>(*S).Body, true);
+        break;
+      default:
+        break;
+      }
+    }
+  }
+
+  void function(const VFunction &Fn) {
+    for (const auto &Post : Fn.Postconditions)
+      expr(Post.get(), "a postcondition");
+    for (const auto &Rec : Fn.Recommends)
+      expr(Rec.get(), "a cppverify::recommends");
+    for (const auto &Dec : Fn.Decreases)
+      expr(Dec.get(), "a cppverify::decreases");
+    expr(Fn.Domain.get(), "a cppverify::when");
+    for (const VFunction::ClauseProof &Proof : Fn.ClauseProofs)
+      stmts(Proof.Body, true);
+    stmts(Fn.Body, Fn.IsSpec || Fn.IsProof);
+    if (Fn.IsSpec && Where)
+      Where = "a spec function";
+  }
+};
+} // namespace
+
+std::optional<std::string> verify::misplacedValidMarker(const VFunction &Fn) {
+  MisplacedValidFinder Finder;
+  Finder.function(Fn);
+  if (!Finder.Where)
+    return std::nullopt;
+  return std::string("valid(p, n) declares an extent only as a top-level "
+                     "condition of a cppverify::pre, and has no meaning in ") +
+         Finder.Where;
 }
 
 std::optional<std::string> verify::instrumentUBChecks(VFunction &Fn) {
@@ -1088,6 +1185,8 @@ std::optional<std::string> verify::instrumentUBChecks(VFunction &Fn) {
     UB.scanValid(Pre.get());
   if (UB.Error)
     return UB.Error;
+  if (auto Misplaced = misplacedValidMarker(Fn))
+    return Misplaced;
   UB.appendValidSemantics(Fn);
   UB.appendExtentSeparation(Fn);
   if (!Fn.IsProof) {

clang/lib/Verify/Transform/UBChecks.h

@@ -70,6 +70,11 @@ bool hasRepresentedRoot(const VExpr *Address);
 /// The driver uses this to warn instead of letting that happen silently.
 bool usesValidMarker(const VFunction &Fn);
 
+/// An error when valid(p, n) occurs anywhere but a precondition, where it is
+/// a spec whose body is `true`: a postcondition, a loop invariant, a check,
+/// ghost code, or a spec function.
+std::optional<std::string> misplacedValidMarker(const VFunction &Fn);
+
 } // namespace verify
 } // namespace clang
 

clang/test/Verify/suite/valid_outside_precondition.cpp

@@ -0,0 +1,67 @@
+// RUN: not %cpp-verify %s -- 2>&1 | FileCheck %s
+// RUN: not %cpp-verify --no-check-ub %s -- 2>&1 | FileCheck %s --check-prefix=NOUB
+//
+// cppverify::valid(p, n) declares an extent only as a top-level condition of a
+// precondition. Anywhere else it would be a spec whose body is true, so a
+// claim written with it would hold without meaning anything: it is an error
+// for that function, and the other functions are still verified.
+
+namespace cv = cppverify;
+using namespace cppverify;
+
+int *in_post(int n)
+  cv::pre(n == 4)
+  cv::post(valid(cv::result, n))
+{
+  return nullptr;
+}
+// CHECK: error: in_post: valid(p, n) declares an extent only as a top-level condition of a cppverify::pre, and has no meaning in a postcondition
+
+int in_invariant(const int *a, int n)
+  cv::pre(valid(a, n) && n >= 0)
+  cv::post(cv::result == n)
+{
+  int i = 0;
+  while (i < n)
+    cv::invariant(0 <= i && i <= n && valid(a, n))
+    cv::decreases(n - i)
+  {
+    i = i + 1;
+  }
+  return i;
+}
+// CHECK: error: in_invariant: {{.*}} has no meaning in a loop invariant
+
+int in_check(const int *a, int n)
+  cv::pre(valid(a, n) && n > 0)
+  cv::post(cv::result == a[0])
+{
+  cv::check(valid(a, n));
+  return a[0];
+}
+// CHECK: error: in_check: {{.*}} has no meaning in a cppverify::check
+
+int in_ghost(const int *a, int n)
+  cv::pre(n > 0)
+  cv::post(cv::result == n)
+{
+  cv::ghost { bool v = valid(a, n); }
+  return n;
+}
+// CHECK: error: in_ghost: {{.*}} has no meaning in ghost code
+
+cv::spec bool in_spec(const int *a, int n) { return valid(a, n) && n > 0; }
+// CHECK: error: in_spec: {{.*}} has no meaning in a spec function
+
+int fine(const int *a, int n)
+  cv::pre(valid(a, n) && n > 0)
+  cv::post(cv::result == a[0])
+{
+  return a[0];
+}
+// CHECK: Verified: fine
+
+// Without memory checks every marker folds to true, as the warning says.
+// NOUB: warning: contract of in_post uses the valid(p, n) extent marker, but memory checking is disabled (--no-check-ub)
+// NOUB: Verified: in_post
+// NOUB: warning: contract of in_check uses the valid(p, n) extent marker

docs/ARCHITECTURE.md

@@ -173,7 +173,9 @@ operation is a `SpecCall` whose identity is `__cppverify.<op>`, such as
 `cppverify::valid(p, n)` becomes a call of the synthesized builtin spec
 `__cppverify_valid(p, n)` (body `true`, marked `IsBuiltin` and never
 reported), so the extent marker scan treats it exactly like a user-declared
-`valid`.
+`valid`. A function that applies either anywhere but as a top-level condition
+of a precondition, where it would mean `true`, is rejected under `--check-ub`
+(`misplacedValidMarker`, `Transform/UBChecks.cpp`).
 
 **Mathematical values in ghost and proof code:** a spec result or a
 collection length, element, or count keeps its mathematical type wherever

docs/DESIGN.md

@@ -986,7 +986,10 @@ relate it to the condition that chose, as in `s ? q == a + i : q == b + i`.
 The marker must be a positive top-level conjunction clause on a bare pointer to
 a complete object type. At most one marker may describe each pointer. Shifted,
 disjunctive, conditional, or duplicate markers fail closed rather than creating
-unconditional extent assumptions.
+unconditional extent assumptions. Anywhere else (a postcondition, a loop
+invariant, a `cppverify::check`, ghost code, a spec function) the marker is its
+builtin spec, whose body is `true`, so a claim made with it would hold without
+meaning anything: under `--check-ub` it is an error for that function.
 
 ### 2. Implicit non-aliasing default
 

website/source/language/limitations.rst

@@ -209,7 +209,9 @@ precondition declares an abstract extent. It remains a caller promise rather tha
 derived from a concrete caller allocation; it does not supply general lifetime,
 alignment, provenance, or initialization. Bounds follow exact conditional and
 short-circuit evaluation, and fresh represented storage is kept disjoint from
-the complete declared incoming extent.
+the complete declared incoming extent. Outside a precondition the marker
+means nothing and is rejected (:doc:`pointers`), so an extent cannot yet be
+stated for a returned pointer.
 
 For pairs involving mutable pointees, CppVerify adds a generated
 complete-object disjointness precondition. ``cppverify::aliases(p, q)`` opts a pair into

website/source/language/pointers.rst

@@ -539,6 +539,90 @@ top-level conjunction clause of a ``cppverify::pre`` with a bare complete-object
 and each pointer may have only one marker; ambiguous forms (under ``||``,
 ``!``, or a conditional, or a second marker for one pointer) fail closed.
 
+Where the marker may appear
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+``valid(p, n)`` is not a condition that a state satisfies or violates. In a
+precondition it declares the extent the caller provides, and the verifier
+checks every access against that extent; that is its whole meaning. Written
+anywhere else (a ``cppverify::post``, a loop invariant, a ``cppverify::check``,
+ghost code, or a spec function) it would be a condition that always holds, so
+a claim made with it would verify without saying anything. That is an error
+for the function, which is then not verified; the other functions of the file
+still are:
+
+.. cppverify-example: rejects
+
+.. code-block:: cpp
+
+   int *start_of(int *buf)
+     cv::pre(valid(buf, 4))
+     cv::post(valid(cv::result, 4))
+   {
+     return buf;
+   }
+
+.. code-block:: text
+
+   error: start_of: valid(p, n) declares an extent only as a top-level condition of a cppverify::pre, and has no meaning in a postcondition
+
+The message ends with the place it found the marker: a postcondition, a loop
+invariant, a ``cppverify::check``, ghost code, or a spec function. The same
+holds for a marker you declare yourself as a spec named ``valid``.
+
+To tell callers where a result points, relate it to a parameter whose extent
+they know; their own precondition then covers the accesses through it:
+
+.. code-block:: cpp
+
+   int *start_of(int *buf)
+     cv::pre(valid(buf, 4))
+     cv::post(cv::result == buf)
+   {
+     return buf;
+   }
+
+   int fourth(int *a)
+     cv::pre(valid(a, 4) && a[3] == 7)
+     cv::post(cv::result == 7)
+   {
+     int *q = start_of(a);
+     return q[3];
+   }
+
+.. code-block:: text
+
+   Verified: start_of [backend=z3]
+   Verified: fourth [backend=z3]
+
+An extent declared by the precondition holds for the whole function, so a
+loop invariant does not repeat it. The invariant bounds the index, and each
+access is checked against the extent:
+
+.. code-block:: cpp
+
+   int sum4(const int *a, int n)
+     cv::pre(valid(a, n) && n >= 0 && n <= 4)
+     cv::pre(cv::forall(k, 0, n, 0 <= a[k] && a[k] <= 100))
+     cv::post(0 <= cv::result && cv::result <= 100 * n)
+   {
+     int s = 0;
+     for (int i = 0; i < n; i = i + 1)
+       cv::invariant(0 <= i && i <= n && 0 <= s && s <= 100 * i)
+       cv::decreases(n - i)
+     {
+       s = s + a[i];
+     }
+     return s;
+   }
+
+.. code-block:: text
+
+   Verified: sum4 [backend=z3]
+
+With ``--no-check-ub`` every marker, in a precondition too, folds to ``true``
+with a warning, and a misplaced one is not an error.
+
 ``valid`` exists only for verification, like the spec collections of the same
 header; Sema rejects it in executable code. Write ``cppverify::valid`` or add
 ``using cppverify::valid;``. Programs written before the header may declare

website/source/language/syntax.rst

@@ -189,5 +189,5 @@ Full table:
      - ``<cppverify.h>``, included implicitly
      - Spec collections
    * - ``cppverify::valid(p, n)``
-     - In ``cppverify::pre``
+     - A top-level condition of ``cppverify::pre``; an error anywhere else
      - ``p`` points to ``n`` objects

website/source/release-notes.rst

@@ -57,6 +57,13 @@ already was (:doc:`language/expressions`).
 generic lambda compiled, and the program failed to link. It is now reported
 where it is written (:doc:`language/ghost-proofs`).
 
+**Extent markers outside a precondition are errors.** ``valid(p, n)`` declares
+an extent only as a top-level condition of a precondition. Anywhere else it
+meant ``true``, so ``cv::post(valid(cv::result, 4))`` verified for a function
+that returns ``nullptr``. In a postcondition, a loop invariant, a
+``cppverify::check``, ghost code, or a spec function it is now an error for
+that function (:doc:`language/pointers`).
+
 **Clang's own analyses.** ``noexcept`` of a contract expression crashed or hung
 the compiler, as did a contract expression in a C++98 constant; the static
 analyzer reported nothing after a ghost block; libclang hid the constructs;