docs: Document every change since 0.1.1 with checked examples

website/scripts/check-doc-examples.py

@@ -4,7 +4,8 @@
 Every ``.. code-block:: cpp`` block (a ```` ```cpp ```` fence in Markdown) must
 compile with cpp-verify, and when the next code block on the page is a
 ``text`` block that shows verdicts, verifying the example must give those
-verdicts. A comment right before a block changes how it is checked; several
+verdicts. The errors and warnings that block shows must be among those the
+verifier prints, apart from the location before each. A comment right before a block changes how it is checked; several
 may be stacked (in Markdown, ``<!-- cppverify-example: ... -->``):
 
     .. cppverify-example: fragment         part of a larger program: not run
@@ -17,6 +18,8 @@
                                            counterexample
     .. cppverify-example: unresolved NAME ...
                                            these stay unresolved
+    .. cppverify-example: rejects          the example is an error: cpp-verify
+                                           reports one and exits non-zero
 
 An example whose page shows no verdicts is verified too: every function
 must verify, unless a comment says it fails or stays unresolved. Comments
@@ -44,6 +47,8 @@
     r" (.+?)(?=\s+\[|\s+\(|$)")
 FAILED = re.compile(r"error: (verification failed|spec [\w ]+? failed): "
                     r"(.+?)(?=\s+\[|\s+\(|$)")
+LOCATION = re.compile(r"^\S+\.(?:cpp|h):\d+:\d+: ")
+DIAGNOSTIC = re.compile(r"^(?:error|warning): ")
 
 
 class Block:
@@ -119,10 +124,28 @@ def blocks(page):
     return found
 
 
+def diagnostics(text):
+    """The errors and warnings a text block shows, without their locations;
+    failures are compared as verdicts."""
+    shown = []
+    for line in text.splitlines():
+        line = LOCATION.sub("", line.strip())
+        if DIAGNOSTIC.match(line) and not FAILED.match(line):
+            shown.append(" ".join(line.split()))
+    return shown
+
+
+def missing_diagnostics(shown, output):
+    printed = [" ".join(LOCATION.sub("", line.strip()).split())
+               for line in output.splitlines()]
+    return [line for line in shown
+            if not any(line in candidate for candidate in printed)]
+
+
 def verdicts(text):
     shown = set()
     for line in text.splitlines():
-        line = re.sub(r"^\S+\.cpp:\d+:\d+: ", "", line.strip())
+        line = LOCATION.sub("", line.strip())
         match = VERDICT.match(line)
         if match:
             shown.add((match.group(1), match.group(2).strip()))
@@ -169,8 +192,19 @@ def check(cpp_verify, job):
     """Returns None, or a failure message and whether every mismatch is a
     function left unresolved where a proof was expected, which only the
     wall-clock budgets of a loaded machine can cause."""
-    block, source, arguments, expected, fails, unresolved = job
+    block, source, arguments, expected, fails, unresolved, shown, rejects = job
     where = f"{block.page}:{block.line}"
+    if rejects:
+        code, output = run(cpp_verify, source, arguments, 300)
+        if code is None or code == 0 or "error:" not in output:
+            return (f"{where}: the example should be an error, but cpp-verify "
+                    f"accepts it:\n{(output or '').strip()[:1500]}"), False
+        missing = missing_diagnostics(shown, output)
+        if missing:
+            return (f"{where}: the page shows diagnostics cpp-verify does not "
+                    f"print:\n" + "\n".join(f"  {line}" for line in missing) +
+                    f"\nactual output:\n{output.strip()[:2500]}"), False
+        return None
     code, output = run(cpp_verify, source, ["--lower-only", *arguments], 300)
     if code is None or code != 0 or "error:" in output:
         return f"{where}: the example does not compile:\n{output.strip()[:1500]}", False
@@ -180,6 +214,10 @@ def check(cpp_verify, job):
         return f"{where}: verifying the example timed out", False
     given = verdicts(output)
     unproved = {name_of(verdict) for verdict in given if verdict[0] == "Unresolved"}
+    if missing := missing_diagnostics(shown, output):
+        return (f"{where}: the page shows diagnostics cpp-verify does not "
+                f"print:\n" + "\n".join(f"  {line}" for line in missing) +
+                f"\nactual output:\n{output.strip()[:2500]}"), False
     if not expected:
         wrong = []
         for verdict in sorted(given):
@@ -237,17 +275,21 @@ def main():
                     print(f"{page}:{block.line}: unknown example label {name}")
                     return 1
                 context.append(labels[name])
-            text = "".join(context) + block.text
+            # Locations in messages count from the block's first line.
+            text = "".join(context) + "#line 1\n" + block.text
             for name in modes.get("label", []):
                 labels[name] = block.text
             compiled.append(block.text)
             expected = set()
+            shown = []
             following = page_blocks[position + 1:position + 2]
             if following and following[0].language == "text":
                 expected = verdicts(following[0].text)
+                shown = diagnostics(following[0].text)
             jobs.append((block, PRELUDE + text, modes.get("flags", []),
                          expected, set(modes.get("fails", [])),
-                         set(modes.get("unresolved", []))))
+                         set(modes.get("unresolved", [])), shown,
+                         "rejects" in modes))
 
     failures = []
     alone = []
@@ -271,7 +313,7 @@ def main():
             failures.append(result[0])
     for failure in failures:
         print(failure, end="\n\n")
-    shown = sum(1 for job in jobs if job[3])
+    shown = sum(1 for job in jobs if job[3] or job[6])
     print(f"{len(jobs)} examples checked ({shown} against the verdicts their "
           f"pages show), {len(failures)} failed")
     return 1 if failures else 0

website/source/book/part-ii/ch13-spec-and-proof-functions.rst

@@ -154,7 +154,41 @@ measure whatever the spec's other calls return:
    }
 
 A recursive call inside ``cppverify::forall``, ``cppverify::exists``, or ``cppverify::choose`` must
-decrease the measure for every value of the bound variable. Spec functions may
+decrease the measure for every value of the bound variable. A call in the body
+of a ``cppverify::choose`` is a call of the function the choose is written in, so it
+is checked like any other:
+
+.. cppverify-example: fails stuck
+.. cppverify-example: unresolved forty_two
+
+.. code-block:: cpp
+
+   cv::spec int stuck(int n)
+     cv::decreases(n)
+   {
+     return n <= 0 ? 0 : cv::choose(k, k == stuck(n) + 1);
+   }
+
+   int forty_two(int x)
+     cv::post(cv::result == 42)
+   {
+     cv::check(stuck(x) >= 0 || stuck(x) < 0);
+     if (x == 1)
+       return 0;
+     return 42;
+   }
+
+.. code-block:: text
+
+   stuck.cpp:4:42: error: spec decreases failed: stuck [backend=z3] [reason=counterexample] (n [type=math-i32] = 1)
+   Unresolved: forty_two [backend=z3] [reason=spec.termination] (relies on the definition of stuck, whose termination is not established)
+
+At ``n = 1`` the definition says that ``stuck(1)`` equals ``stuck(1) + 1``, a
+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``.
+
+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
 as opaque:

website/source/book/part-ii/ch16-when-verification-fails.rst

@@ -311,6 +311,44 @@ problem, and those are exactly the places checked above: a verified callee
 returns, so ordinary calls cannot cut paths (a callee with
 ``cppverify::decreases(*)`` may not, and its callers are reported ``[partial]``).
 
+A finding that no execution reaches a claim rests on the facts its query
+uses, as a proof does. When a result is ``Unresolved`` because one of those
+facts is not established, the finding is dropped where the missing fact may
+be its cause:
+
+.. cppverify-example: fails contradictory
+.. cppverify-example: unresolved relies_on_it
+
+.. code-block:: cpp
+
+   int contradictory(int x)
+     cv::post(cv::result == x && cv::result == x + 1)   // no result satisfies this
+   {
+     return x;
+   }
+
+   int relies_on_it(int x)
+     cv::post(cv::result == 7)
+   {
+     return contradictory(x);
+   }
+
+.. code-block:: text
+
+   vacuity.cpp:2:28: error: verification failed: contradictory [...::postcondition@2:28] (...) [backend=z3] [reason=counterexample]
+   Unresolved: relies_on_it [backend=z3] [reason=callee.contract] (relies on the contract of contradictory, which is not established)
+
+``relies_on_it`` proves its postcondition only because the contract of
+``contradictory`` cannot hold, which is the problem to fix, and the reason
+names it. Whether no execution reaches its end is a question about that
+contract too, so it is not reported. A spec whose termination fails can
+contradict itself the same way, and whether the solver notices is not a fact
+about the program. A finding about the entry state alone is kept when what is
+missing is a callee's contract, since no callee contract enters the entry
+state: an unsatisfiable precondition is still reported, with ``[vacuous]``.
+Before 0.2, ``relies_on_it`` was also reported ``[vacuous]``, with the warning
+that no execution reaches its end.
+
 Quantifiers that run away
 -------------------------
 

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

@@ -215,7 +215,8 @@ uses, ``[partial]``, and the vacuity checks. Where the source run reports
 ``Verified``, replay therefore reports ``Proved obligations: f (dependencies
 not checked in replay)``, with JSON status ``proved-obligations``. A
 counterexample is checked against the definitions alone and is still a
-failure.
+failure. The archive section of :doc:`../../language/tooling` shows a source run
+and its replay side by side.
 
 Source-built and replayed records pass through the same conservative
 canonicalizer before hashing and dispatch. It folds only trivial Boolean

website/source/language/dynamic-storage.rst

@@ -282,7 +282,41 @@ type permits, compared for equality, converted to ``bool``, deleted, passed
 through the checked verified scalar interfaces above, or returned by the
 inferred fresh-owned factory boundary. These limits apply to the pointer, not
 to the value read through it: ``*p + 1``, ``*p < 50``, ``*p + *q``, and
-``sq(*p)`` in a spec call are ordinary integer expressions.
+``sq(*p)`` in a spec call are ordinary integer expressions. Both functions
+below verify:
+
+.. code-block:: cpp
+
+   cv::spec int sq(int x) { return x * x; }
+
+   int next_value(int v)
+     cv::pre(v < 100)
+     cv::post(cv::result == v + 1)
+   {
+     int *p = new int(v);
+     int r = *p + 1;
+     delete p;
+     return r;
+   }
+
+   int square_stored(int v)
+     cv::pre(0 <= v && v <= 100)
+     cv::post(cv::result == sq(v))
+   {
+     int *p = new int(v);
+     int *q = new int(v);
+     int r = *p * *q;
+     cv::check(r == sq(*p));
+     delete p;
+     delete q;
+     return r;
+   }
+
+Before 0.2, such expressions were rejected as if they computed with the
+pointer itself, and the file stopped: ``error: next_value: arithmetic on
+dynamic-storage pointers is unsupported``, and for the spec call ``error:
+square_stored: dynamic-storage pointers cannot cross a function-call
+boundary``.
 
 Type-erasing or indirect copies, ownership-taking pointer parameters,
 arithmetic-derived ownership, uninitialized/freed/multiple/escaped results,

website/source/language/expressions.rst

@@ -12,9 +12,75 @@ Contract expressions
 - collection operations of ``<cppverify.h>`` (``s.len()``, ``s[i]``,
   ``a.contains(x)``, ``m[k]``, ...)
 
-Must be contextually ``bool`` where used as conditions. They exist only for
-verification: a quantifier or a ``cppverify::choose`` in executable code is an
-error, outside an unevaluated operand such as ``sizeof``.
+Must be contextually ``bool`` where used as conditions.
+
+Quantifiers exist only for verification
+---------------------------------------
+
+A quantifier or a ``cppverify::choose`` has no value at run time: the compiler
+cannot evaluate ``cv::forall(k, 0, n, a[k] >= 0)`` without running a loop the
+program never wrote. So these expressions may appear only where the verifier
+reads them and the compiler does not: in a contract clause, a
+``cv::check``, a ghost block or ghost variable, a spec or proof function, and
+an unevaluated operand such as ``sizeof``. Every use below is allowed:
+
+.. code-block:: cpp
+
+   bool first_is_zero(const int *a, int n)
+     cv::pre(valid(a, n) && n > 0)
+     cv::post(cv::result == (a[0] == 0))
+     cv::post(!cv::result || cv::exists(k, 0, n, a[k] == 0))
+   {
+     cv::check(cv::forall(k, 0, 1, k == 0));
+     cv::ghost { bool any_zero = cv::exists(k, 0, n, a[k] == 0); }
+     return a[0] == 0;
+   }
+
+In executable code (a function body outside a ghost block, an initializer, a
+default argument that a call uses, a lambda, or a template's body) the same
+expression is an error, reported once where it is written, for the outermost
+quantifier:
+
+.. cppverify-example: rejects
+
+.. code-block:: cpp
+
+   bool all_nonnegative(const int *a, int n)
+     cv::pre(valid(a, n))
+   {
+     return cv::forall(k, 0, n, a[k] >= 0);
+   }
+
+.. code-block:: text
+
+   quantifiers.cpp:4:10: error: cppverify::forall exists only for verification and cannot be used in executable code; use it in a contract, ghost block, or spec or proof function
+       4 |   return cv::forall(k, 0, n, a[k] >= 0);
+         |          ^
+
+To compute such a value at run time, write the loop, and state what it
+computes in the postcondition with the quantifier:
+
+.. code-block:: cpp
+
+   bool all_nonnegative(const int *a, int n)
+     cv::pre(valid(a, n) && n >= 0)
+     cv::post(cv::result == cv::forall(k, 0, n, a[k] >= 0))
+   {
+     for (int i = 0; i < n; i = i + 1)
+       cv::invariant(0 <= i && i <= n)
+       cv::invariant(cv::forall(k, 0, i, a[k] >= 0))
+       cv::decreases(n - i)
+     {
+       if (a[i] < 0)
+         return false;
+     }
+     return true;
+   }
+
+Before 0.2, ``cv::forall`` and ``cv::exists`` in executable code compiled
+without a diagnostic to an undefined value (LLVM's ``poison``), while the
+verifier read them as quantifiers, so a function could verify and still
+behave arbitrarily when run. ``cv::choose`` was already rejected there.
 
 The range ``[lo, hi)`` may be **symbolic** (e.g. ``cppverify::forall(i, 0, n, ...)``).
 A bounded quantifier reaches the solver as a quantifier, whatever its range: