diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 4f48aa1a37..a9161a3329 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/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) { diff --git a/clang/lib/Verify/Transform/UBChecks.cpp b/clang/lib/Verify/Transform/UBChecks.cpp index 82fb2b0d46..afb633e415 100644 --- a/clang/lib/Verify/Transform/UBChecks.cpp +++ b/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> &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(*S).Value.get(), Code); + break; + case VStmt::Store: { + const auto &St = static_cast(*S); + expr(St.Ptr.get(), Code); + expr(St.Value.get(), Code); + break; + } + case VStmt::If: { + const auto &I = static_cast(*S); + expr(I.Cond.get(), Code); + stmts(I.Then, Ghost); + stmts(I.Else, Ghost); + break; + } + case VStmt::Assert: + expr(static_cast(*S).Cond.get(), + "a cppverify::check"); + break; + case VStmt::Assume: + expr(static_cast(*S).Cond.get(), Code); + break; + case VStmt::ContractAssert: + expr(static_cast(*S).Cond.get(), + "a cppverify::check"); + break; + case VStmt::Return: + expr(static_cast(*S).Value.get(), Code); + break; + case VStmt::While: { + const auto &W = static_cast(*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(*S).Args) + expr(Arg.get(), Code); + break; + case VStmt::Seq: + stmts(static_cast(*S).Stmts, Ghost); + break; + case VStmt::GhostBlock: + stmts(static_cast(*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 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 verify::instrumentUBChecks(VFunction &Fn) { @@ -1088,6 +1185,8 @@ std::optional 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) { diff --git a/clang/lib/Verify/Transform/UBChecks.h b/clang/lib/Verify/Transform/UBChecks.h index cdb507eb3b..79e4082d0c 100644 --- a/clang/lib/Verify/Transform/UBChecks.h +++ b/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 misplacedValidMarker(const VFunction &Fn); + } // namespace verify } // namespace clang diff --git a/clang/test/Verify/suite/valid_outside_precondition.cpp b/clang/test/Verify/suite/valid_outside_precondition.cpp new file mode 100644 index 0000000000..480416c39a --- /dev/null +++ b/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 diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 58cd771142..acf48ef64e 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -173,7 +173,9 @@ operation is a `SpecCall` whose identity is `__cppverify.`, 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 diff --git a/docs/DESIGN.md b/docs/DESIGN.md index d08bbc23dd..ab4f6eed1c 100644 --- a/docs/DESIGN.md +++ b/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 diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 1228ac4332..2f5057c7d0 100644 --- a/website/source/language/limitations.rst +++ b/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 diff --git a/website/source/language/pointers.rst b/website/source/language/pointers.rst index 7cb5df657f..09f28a357d 100644 --- a/website/source/language/pointers.rst +++ b/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 diff --git a/website/source/language/syntax.rst b/website/source/language/syntax.rst index f6c128a580..6cbdaafb91 100644 --- a/website/source/language/syntax.rst +++ b/website/source/language/syntax.rst @@ -189,5 +189,5 @@ Full table: - ````, 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 diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index b8abf5d90b..d447174c00 100644 --- a/website/source/release-notes.rst +++ b/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;