verify: Reject a quantifier in executable code

clang/include/clang/Basic/DiagnosticSemaKinds.td

@@ -14396,8 +14396,8 @@ def err_contract_range_no_length : Error<
   "a modifies range needs a length: p[start : length]">;
 def err_contract_range_use : Error<
   "a range p[start : length] is a whole modifies footprint, not an operand">;
-def err_choose_in_executable_code : Error<
-  "cppverify::choose exists only for verification and cannot be used in "
+def err_verification_construct_in_executable_code : Error<
+  "cppverify::%0 exists only for verification and cannot be used in "
   "executable code; use it in a contract, ghost block, or spec or proof "
   "function">;
 def err_ghost_variable_in_executable_code : Error<

clang/lib/Sema/SemaContract.cpp

@@ -190,10 +190,27 @@ class ExecutableSpecUseFinder
       S.Diag(Loc, diag::err_collection_in_executable_code) << 0 << D;
   }
 
-  bool VisitContractChooseExpr(ContractChooseExpr *E) {
-    if (!GhostDepth &&
-        S.DiagnosedSpecFunctionUses.insert(E->getExprLoc()).second)
-      S.Diag(E->getExprLoc(), diag::err_choose_in_executable_code);
+  // A quantifier or a choice has no value at run time: it is reported once,
+  // and what it contains with it.
+  bool TraverseForallExpr(ForallExpr *E) {
+    return diagnoseConstruct(E, "forall") || Base::TraverseForallExpr(E);
+  }
+  bool TraverseExistsExpr(ExistsExpr *E) {
+    return diagnoseConstruct(E, "exists") || Base::TraverseExistsExpr(E);
+  }
+  bool TraverseContractChooseExpr(ContractChooseExpr *E) {
+    return diagnoseConstruct(E, "choose") ||
+           Base::TraverseContractChooseExpr(E);
+  }
+
+  /// Whether \p E is in executable code, which is then reported.
+  bool diagnoseConstruct(Expr *E, llvm::StringRef Name) {
+    if (GhostDepth)
+      return false;
+    if (S.DiagnosedSpecFunctionUses.insert(E->getExprLoc()).second)
+      S.Diag(E->getExprLoc(),
+             diag::err_verification_construct_in_executable_code)
+          << Name;
     return true;
   }
 };

clang/test/Verify/errors_namespaced.cpp

@@ -28,7 +28,8 @@ int old_name(int x) {
 
 int with_using(int n) {
   using namespace cppverify;
-  return forall(k, 0, n, k >= 0); // expected-error {{'forall' is a cpp-verify construct only when qualified: write 'cppverify::forall'}}
+  cv::check(forall(k, 0, n, k >= 0)); // expected-error {{'forall' is a cpp-verify construct only when qualified: write 'cppverify::forall'}}
+  return n;
 }
 
 int clause_in_body(int x) {

clang/test/Verify/errors_quantifier_in_executable.cpp

@@ -0,0 +1,49 @@
+// RUN: %clang_cc1 -std=c++17 -fverify-contracts -verify %s
+// RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -DALLOWED_ONLY \
+// RUN:   -emit-llvm -o - %s | FileCheck %s --implicit-check-not=poison
+//
+// A quantifier has no value at run time, so executable code may not use one;
+// it once compiled to poison. Contracts, ghost code, and unevaluated operands
+// may.
+
+// CHECK: define {{.*}}allowed
+bool allowed(int n)
+  cppverify::pre(cppverify::forall(k, 0, n, k >= 0))
+  cppverify::post(cppverify::result == cppverify::exists(k, 0, n, k == 0))
+{
+  cppverify::check(cppverify::forall(k, 0, 1, k == 0));
+  cppverify::ghost { bool all = cppverify::forall(k, 0, n, k >= 0); }
+  unsigned long size = sizeof(cppverify::forall(k, 0, n, k >= 0));
+  return n > 0 && size == sizeof(bool);
+}
+
+#ifndef ALLOWED_ONLY
+bool returns_forall(int n) {
+  return cppverify::forall(k, 0, n, k >= 0); // expected-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}}
+}
+
+bool initializes_exists(int n) {
+  bool found = cppverify::exists(k, 0, n, k == 3); // expected-error {{cppverify::exists exists only for verification}}
+  return found;
+}
+
+// The inner quantifier is reported with the outer one.
+bool nested(int n) {
+  return cppverify::forall(i, 0, n, cppverify::exists(j, 0, n, i == j)); // expected-error {{cppverify::forall exists only for verification}}
+}
+
+bool global_quantifier = cppverify::exists(k, 0, 2, k == 1); // expected-error {{cppverify::exists exists only for verification}}
+
+// A template is reported where it is written, once, whether or not it is
+// instantiated.
+template <typename T>
+bool never_instantiated(T n) {
+  return cppverify::forall(k, 0, 3, k < n); // expected-error {{cppverify::forall exists only for verification}}
+}
+
+template <typename T>
+bool instantiated(T n) {
+  return cppverify::exists(k, 0, 3, k == n); // expected-error {{cppverify::exists exists only for verification}}
+}
+bool uses_template() { return instantiated(5) && instantiated(6L); }
+#endif

docs/DESIGN.md

@@ -761,6 +761,8 @@ cppverify::post(cppverify::forall(k, sq(k) >= 0))
 ```
 
 - `binder` is a fresh mathematical integer, scoped to `body`.
+- A quantifier exists only for verification: Sema rejects one in executable
+  code, as it rejects `cppverify::choose`, except as an unevaluated operand.
 - `lo` and `hi` must be integer; `body` must be bool.
 - Without bounds the quantifier ranges over all mathematical integers. A
   counterexample to one is certified exactly when its body depends on its
@@ -1597,8 +1599,8 @@ a one-line hook.
     `cppverify::spec` or `cppverify::proof` functions; executable code, including initializers and
     default arguments, may not reference one. Unevaluated operands
     (`sizeof`, `decltype`) are exempt.
-11. The same holds for ghost variables, `cppverify::choose`, and the `cppverify`
-    collections (their types as executable declarations, parameters, or
+11. The same holds for ghost variables, `cppverify::forall`, `cppverify::exists`,
+    `cppverify::choose`, and the `cppverify` collections (their types as executable declarations, parameters, or
     results, and every operation).
 12. A range `p[lo : n]` needs a pointer to a complete object type and
     integer bounds, and is valid only as a whole `cppverify::modifies` footprint.

website/source/language/expressions.rst

@@ -12,7 +12,9 @@ Contract expressions
 - collection operations of ``<cppverify.h>`` (``s.len()``, ``s[i]``,
   ``a.contains(x)``, ``m[k]``, ...)
 
-Must be contextually ``bool`` where used as conditions.
+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``.
 
 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: