From fbcc0d623792cbb83ddc06e06a95dedbff4f4964 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 10:07:46 +0530 Subject: [PATCH 1/7] verify: Name the construct in the error for a verification construct in executable code. --- clang/include/clang/Basic/DiagnosticSemaKinds.td | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/clang/include/clang/Basic/DiagnosticSemaKinds.td b/clang/include/clang/Basic/DiagnosticSemaKinds.td index f79efbeaee..050cb87f37 100644 --- a/clang/include/clang/Basic/DiagnosticSemaKinds.td +++ b/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< From 11d2424ee73f6e60b6d38a6dd847e6fc38c8bc5a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 10:07:46 +0530 Subject: [PATCH 2/7] verify: Reject a quantifier in executable code, as a choice is rejected. --- clang/lib/Sema/SemaContract.cpp | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/clang/lib/Sema/SemaContract.cpp b/clang/lib/Sema/SemaContract.cpp index f762a33551..8eef44eae8 100644 --- a/clang/lib/Sema/SemaContract.cpp +++ b/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; } }; From 05a65577cb7d9fe97a26319633b2d41d37f65ce1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 10:07:46 +0530 Subject: [PATCH 3/7] test: A quantifier in executable code is an error. --- .../errors_quantifier_in_executable.cpp | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 clang/test/Verify/errors_quantifier_in_executable.cpp diff --git a/clang/test/Verify/errors_quantifier_in_executable.cpp b/clang/test/Verify/errors_quantifier_in_executable.cpp new file mode 100644 index 0000000000..87ac186674 --- /dev/null +++ b/clang/test/Verify/errors_quantifier_in_executable.cpp @@ -0,0 +1,36 @@ +// 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}} +#endif From d0b26be8365904bafc66a96331c66b914dc2e851 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 10:07:47 +0530 Subject: [PATCH 4/7] docs: Say in DESIGN that executable code cannot use a quantifier. --- docs/DESIGN.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 236cf1d7e7..c9ff2e4019 100644 --- a/docs/DESIGN.md +++ b/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. From 1d64188264ddc6e7eb74b10bd4a835edb9293175 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 15 Oct 2026 10:07:47 +0530 Subject: [PATCH 5/7] docs: Say in the expressions guide that executable code cannot use a quantifier. --- website/source/language/expressions.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/website/source/language/expressions.rst b/website/source/language/expressions.rst index f20ffdf77e..a33b11410a 100644 --- a/website/source/language/expressions.rst +++ b/website/source/language/expressions.rst @@ -12,7 +12,9 @@ Contract expressions - collection operations of ```` (``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: From 1f1a8f65de604684a5c0a80150c192f259d6d2ed Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 16 Oct 2026 16:29:00 +0530 Subject: [PATCH 6/7] test: Write the bare quantifier of errors_namespaced.cpp in a check, where a quantifier belongs. --- clang/test/Verify/errors_namespaced.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/clang/test/Verify/errors_namespaced.cpp b/clang/test/Verify/errors_namespaced.cpp index 1df6046744..e01e0d8506 100644 --- a/clang/test/Verify/errors_namespaced.cpp +++ b/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) { From 39321933500767fb29f15709e51d9ee1d59d739b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sun, 18 Oct 2026 20:12:05 +0530 Subject: [PATCH 7/7] test: A quantifier in a template's executable code is reported once, instantiated or not. --- .../test/Verify/errors_quantifier_in_executable.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/clang/test/Verify/errors_quantifier_in_executable.cpp b/clang/test/Verify/errors_quantifier_in_executable.cpp index 87ac186674..80137732b0 100644 --- a/clang/test/Verify/errors_quantifier_in_executable.cpp +++ b/clang/test/Verify/errors_quantifier_in_executable.cpp @@ -33,4 +33,17 @@ bool nested(int n) { } 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 +bool never_instantiated(T n) { + return cppverify::forall(k, 0, 3, k < n); // expected-error {{cppverify::forall exists only for verification}} +} + +template +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