From 038cccfc3f39de35d6a1d3802a0564c44b27291d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:24:20 +0530 Subject: [PATCH 01/19] verify: Note a counterexample's loop, confirm it by unrolling the loops, and name an unmeasured loop beside a failure. --- clang/lib/Verify/Driver/Verifier.cpp | 132 +++++++++++++++++++++++++++ clang/lib/Verify/Driver/Verifier.h | 4 + 2 files changed, 136 insertions(+) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 4583445424..69b91649ce 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -13,6 +13,7 @@ #include "../Backend/ProofCache.h" #include "../Backend/SpecAxioms.h" #include "../Backend/TaskGroup.h" +#include "../Backend/Z3Encode.h" #include "../Frontend/ASTConverter.h" #include "../IR/VStmt.h" #include "../Transform/LoopUnroll.h" @@ -1101,6 +1102,8 @@ struct VerifyDiagnostic { SourceRange Span; /// A spec function that needs no check, listed with --verbose: no verdict. bool Axiom = false; + /// What else the verifier found about the verdict, each printed as a note. + std::vector Notes; }; static std::string backendSuffix(const VerifyResult &Result) { @@ -3451,6 +3454,126 @@ class Verifier { } auto SmokeBackend = createVerifyBackend(BackendKind::Z3, nullptr, 0, SmokeExecution, nullptr); + // What else a failure shows. A counterexample that passes through a + // loop starts from any state the loop's invariants allow, which no + // execution need reach; unrolling the loops looks for an execution + // that fails, or proves that none does. + auto failureNotes = [&](const VFunction &F, const VerifyResult &Failure) { + std::vector Notes; + auto at = [&](SourceLocation Loc) { + const PresumedLoc Where = Ctx.getSourceManager().getPresumedLoc(Loc); + return Where.isValid() ? std::to_string(Where.getLine()) + ":" + + std::to_string(Where.getColumn()) + : std::string("?"); + }; + if (F.UnmeasuredLoop.isValid()) + Notes.push_back("the loop at " + at(F.UnmeasuredLoop) + + " has no cppverify::decreases: a proof would be " + "Unresolved (decreases.missing) until it has one"); + const auto Loop = llvm::find_if(Failure.Trace, [](const auto &Event) { + return Event.Kind == DiagnosticTraceKind::Loop && + Event.Active.value_or(false); + }); + if (Loop == Failure.Trace.end() || !isDeductiveBackend(Opts.Backend) || + Failure.Reason != VerifyReason::Counterexample) + return Notes; + Notes.push_back( + "the counterexample's state at the loop at " + + (Loop->Source.isValid() ? std::to_string(Loop->Source.Line) + ":" + + std::to_string(Loop->Source.Column) + : std::string("?")) + + " is any state its invariants allow, not necessarily one an " + "execution reaches"); + if (Opts.ConfirmBound == 0 || !Failure.ObligationType) + return Notes; + VFunction Bounded = cloneVFunction(F); + annotatePointerOrigins(Bounded); + if (Opts.CheckUB && !F.TotalExpressions && instrumentUBChecks(Bounded)) + return Notes; + SpecInliner(FnMap, Bounded.SpecFuel).prepareFunction(Bounded); + // The search after a failure takes at most one query's time. + Z3VerifyBackend Unroller(Execution, "bmc"); + std::optional Until = Deadline; + if (Opts.SolverTimeoutMs != 0) { + const auto Slice = std::chrono::steady_clock::now() + + std::chrono::milliseconds(Opts.SolverTimeoutMs); + if (!Until || Slice < *Until) + Until = Slice; + } + Unroller.setDeadline(Until); + auto iterations = [](unsigned Bound) { + return std::to_string(Bound) + + (Bound == 1 ? " iteration" : " iterations"); + }; + // Unrolling keeps the function's checks, each copied into every + // iteration it is in, but not the loops' invariants and measures: + // the copies of the failed check are those of its kind at its place. + auto copyOfFailure = [&](const VerifyResult &Result) { + return Result.ObligationType == Failure.ObligationType && + Result.Source.Line == Failure.Source.Line && + Result.Source.Column == Failure.Source.Column && + Result.Source.File == Failure.Source.File; + }; + bool Unrolled = false; + for (unsigned Bound = 0; Bound <= Opts.ConfirmBound; ++Bound) { + VFunction Copy = LoopUnroller::unroll(Bounded, Bound); + Passivizer Unrolling; + Unrolling.setFunctionMap(InterfaceMap); + auto Lowered = buildObligationModule(Unrolling.run(Copy)); + if (!Lowered) { + llvm::consumeError(Lowered.takeError()); + return Notes; + } + auto Simplified = simplifyObligationModule(std::move(*Lowered)); + if (!Simplified) { + llvm::consumeError(Simplified.takeError()); + return Notes; + } + ObligationModule Module = std::move(*Simplified); + Module.BMCTransform = BMCTransformProvenance{Bound}; + annotateObligationSources(Module); + bool Copies = false; + bool CopiesHold = true; + bool Unwound = true; + for (VerifyResult &Result : Unroller.verifyObligations(Module)) { + if (Result.ObligationType == ObligationKind::Unwinding) { + Unwound &= Result.Status == VerifyStatus::Verified; + continue; + } + if (!copyOfFailure(Result)) + continue; + Copies = true; + if (Result.Status == VerifyStatus::Failed && + Result.Reason == VerifyReason::Counterexample) { + Notes.push_back( + "an execution fails this check " + + (Bound == 0 + ? std::string("with no iteration of any loop") + : "within " + iterations(Bound) + " of each loop") + + (Result.Message.empty() + ? std::string() + : " (counterexample: " + Result.Message + ")")); + return Notes; + } + CopiesHold &= Result.Status == VerifyStatus::Verified; + } + Unrolled |= Copies; + if (!CopiesHold) + return Notes; + if (Copies && Unwound) { + Notes.push_back( + "no execution fails this check: every loop ends within " + + iterations(Bound) + + ", and unrolling proves it there; the " + "loops' invariants are too weak for an unbounded proof"); + return Notes; + } + } + if (Unrolled) + Notes.push_back("no execution fails this check within " + + iterations(Opts.ConfirmBound) + " of each loop"); + return Notes; + }; Passivizer P; P.setFunctionMap(InterfaceMap); auto proves = [&](PassiveProgram Smoke) { @@ -4652,6 +4775,7 @@ class Verifier { Msg += backendSuffix(R); Diags.push_back( {VerifyDiagnostic::Error, Msg, R.Location, Fn->Name, R}); + Diags.back().Notes = failureNotes(*Fn, R); } else { const bool FallbackExported = R.Status == VerifyStatus::Unresolved && exportLeanFallback(Module, Fn->Name, R); @@ -5585,6 +5709,12 @@ class Verifier { ? "error" : "note"; Record["message"] = jsonText(D.Message); + if (!D.Notes.empty()) { + llvm::json::Array Notes; + for (const std::string &Note : D.Notes) + Notes.push_back(jsonText(Note)); + Record["notes"] = std::move(Notes); + } if (!D.FunctionName.empty()) Record["function"] = jsonText(D.FunctionName); @@ -5931,6 +6061,8 @@ class Verifier { << PLoc.getColumn() << ": "; OS << "note: " << InstantiationNote << "\n"; } + for (const std::string &Note : D.Notes) + OS << "note: " << Note << "\n"; } } }; diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h index 2d77453436..a7c4803241 100644 --- a/clang/lib/Verify/Driver/Verifier.h +++ b/clang/lib/Verify/Driver/Verifier.h @@ -109,6 +109,10 @@ struct VerifyOptions { bool Verbose = false; /// List the functions the run would verify, and verify none. bool ListFunctions = false; + /// For a failure whose counterexample passes through a loop, the most + /// iterations of each loop that unrolling may try to find an execution + /// that fails (0: do not try). + unsigned ConfirmBound = 10; /// Where the run counts the verdicts it prints, if anywhere. VerifySummary *Summary = nullptr; }; From 4f19294514cf681906c20e575564b484d52baa8a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:24:21 +0530 Subject: [PATCH 02/19] verify: Add --confirm-bound, for the solver backends only. --- clang/tools/cpp-verify/Main.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index 1947b7920d..863e327449 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -278,6 +278,13 @@ static cl::opt "(spec axiom)"), cl::cat(CppVerifyCategory)); +static cl::opt ConfirmBound( + "confirm-bound", + cl::desc("For a failure whose counterexample passes through a loop, " + "unroll each loop up to this many iterations to look for an " + "execution that fails (default 10, 0 = do not look)"), + cl::init(10), cl::cat(CppVerifyCategory)); + static cl::opt ListFunctions( "list-functions", cl::desc("List the functions a run would verify, with their kinds and " @@ -437,6 +444,7 @@ class VerifyConsumer : public ASTConsumer { VOpts.Quiet = Quiet.getValue(); VOpts.Verbose = Verbose.getValue(); VOpts.ListFunctions = ListFunctions.getValue(); + VOpts.ConfirmBound = ConfirmBound.getValue(); VOpts.Summary = &gSummary; if (!verify::verifyTranslationUnit(Ctx, llvm::outs(), VOpts)) ++gVerifyFailures; @@ -667,6 +675,10 @@ static bool resolveOptions(bool Replay) { "--backend=race"; else if (given(BMCUnroll) && !Replay && Backend != "bmc") Error = "--unroll requires --backend=bmc"; + else if (given(ConfirmBound) && + (Replay || Backend == "bmc" || Backend == "lean")) + Error = "--confirm-bound requires source verification with --backend=z3, " + "cvc5, portfolio, or race"; else if (given(LeanFallbackScope) && LeanFallback.empty()) Error = "--lean-fallback-scope requires --lean-fallback"; else if (given(LeanAutoTimeout) && LeanProject.empty() && From 3552a2a838be4065bcc00dc0edf2063fc0a72332 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:24:21 +0530 Subject: [PATCH 03/19] test: Failures after a loop, reachable, unreachable within the bound, proved by unrolling, and beside an unmeasured loop. --- .../suite/inductive_counterexamples.cpp | 245 ++++++++++++++---- 1 file changed, 192 insertions(+), 53 deletions(-) diff --git a/clang/test/Verify/suite/inductive_counterexamples.cpp b/clang/test/Verify/suite/inductive_counterexamples.cpp index 4fb3d8c718..42421b805d 100644 --- a/clang/test/Verify/suite/inductive_counterexamples.cpp +++ b/clang/test/Verify/suite/inductive_counterexamples.cpp @@ -1,76 +1,215 @@ -// RUN: not %cpp-verify %s -- 2>&1 | FileCheck %s +// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s +// RUN: not %cpp-verify --jobs=1 --confirm-bound=0 %s -- 2>&1 | FileCheck %s --check-prefix=NONE +// RUN: not %cpp-verify --jobs=1 --diagnostics-format=json %s -- 2>/dev/null | FileCheck %s --check-prefix=JSON +// RUN: not %cpp-verify --backend=bmc --confirm-bound=3 %s -- 2>&1 | FileCheck %s --check-prefix=OPTION // -// A counterexample may need an inductive predicate to be false somewhere, -// which no derivation height shows. Its check decides that by the least -// fixpoint over the arguments the predicate's derivations reach, when they -// are finitely many, or by a proved postcondition; otherwise the message -// names the application it could not decide. +// A counterexample that passes through a loop starts the loop's next steps +// from any state its invariants allow, which no execution need reach. Its +// failure says so, and unrolling each loop looks for an execution that +// fails: one within the bound, none within it, or a proof that none fails at +// all. A loop without a measure is named beside a failure too. -#include -using cppverify::valid; +namespace cv = cppverify; -cppverify::spec bool edge(int a, int b) { return b == a + 2 || b == 2 * a; } +int count_up(int n) + cv::pre(n >= 0 && n <= 5) + cv::post(cv::result == n) +{ + int c = 0; + while (c < n) + cv::decreases(n - c) + { + c = c + 1; + } + return c; +} -// Finitely many arguments: every step goes up, and none above b counts. -cppverify::spec bool climb(int a, int b) cppverify::inductive { - return a == b || (a < b && cppverify::exists(c, edge(a, c) && climb(c, b))); +int sum_wrong(int n) + cv::pre(n >= 0 && n <= 5) + cv::post(cv::result == n) +{ + int s = 0; + for (int i = 0; i < n; i = i + 1) + cv::invariant(0 <= i && i <= n && s == 2 * i) + cv::decreases(n - i) + { + s = s + 2; + } + return s; } -cppverify::proof void climb_three_four() cppverify::post(climb(3, 4)) {} -// CHECK-DAG: error: verification failed: climb_three_four {{.*}}[reason=counterexample] +int far_wrong(int n) + cv::pre(n >= 0 && n <= 1000) + cv::post(cv::result < 100) +{ + int c = 0; + while (c < n) + cv::invariant(0 <= c && c <= n) + cv::decreases(n - c) + { + c = c + 1; + } + return c; +} -cppverify::proof void climb_one_four() cppverify::post(climb(1, 4)) { - cppverify::check(climb(4, 4)); - cppverify::check(climb(2, 4)); +int no_loop(int x) + cv::pre(x < 100) + cv::post(cv::result == x) +{ + return x + 1; } -// CHECK-DAG: Verified: climb_one_four -// Defined together, with finitely many arguments. -cppverify::spec bool ev(int n); -cppverify::spec bool od(int n) cppverify::inductive { return n == 1 || (n > 1 && ev(n - 1)); } -cppverify::spec bool ev(int n) cppverify::inductive { return n == 0 || (n > 0 && od(n - 1)); } +int unmeasured(int n) + cv::pre(n >= 0 && n <= 5) + cv::post(cv::result == n + 1) +{ + int c = 0; + while (c < n) + cv::invariant(0 <= c && c <= n) + { + c = c + 1; + } + return c; +} -cppverify::proof void four_is_odd() cppverify::post(od(4)) {} -// CHECK-DAG: error: verification failed: four_is_odd {{.*}}[reason=counterexample] +// Unrolling checks the copies of the failed check, here the division in +// each iteration, and finds the execution that divides by zero. +int divides(int n) + cv::pre(n >= 0 && n <= 5) + cv::post(cv::result >= -5) +{ + int c = 0; + int q = 0; + while (c < n) + cv::invariant(0 <= c && c <= n) + cv::decreases(n - c) + { + q = 10 / (3 - c); + c = c + 1; + } + return q - 5; +} + +// Unrolling keeps no invariant, so it cannot confirm a failed one. +int grows(int n) + cv::pre(n >= 0 && n <= 5) + cv::post(true) +{ + int c = 0; + while (c < n) + cv::invariant(c <= 2) + cv::decreases(n - c) + { + c = c + 1; + } + return c; +} -// Reading memory: a cycle that never reaches 5. -cppverify::spec bool linked(const int *next, int n, int i, int j) - cppverify::inductive - cppverify::reads(next, n) +// The copies of the failed check are those at its place: the check after +// the loop fails sooner, with n == 2, but it is another check. +int two_checks(int n) + cv::pre(n >= 0 && n <= 5) + cv::post(true) { - return i == j || (0 <= i && i < n && linked(next, n, next[i], j)); + int c = 0; + while (c < n) + cv::invariant(0 <= c && c <= n) + cv::decreases(n - c) + { + cv::check(c != 4); + c = c + 1; + } + cv::check(c != 2); + return c; } -void around(const int *next) - cppverify::pre(valid(next, 2) && next[0] == 1 && next[1] == 0) +// And those of its kind: the division by zero at the same place fails one +// iteration sooner, but the failed check is the overflow of INT_MIN / -1. +int two_kinds(int a, int n) + cv::pre(n >= 0 && n <= 5) + cv::post(true) { - cppverify::check(linked(next, 2, 0, 5)); + int c = 0; + int q = 0; + while (c < n) + cv::invariant(0 <= c && c <= n) + cv::decreases(n - c) + { + q = a / (1 - c); + c = c + 1; + } + return q; } -// CHECK-DAG: error: verification failed: around {{.*}}[reason=counterexample] -// Infinitely many arguments, but a proved postcondition decides it. -cppverify::spec bool even(int n) cppverify::inductive cppverify::post(!cppverify::result || (n >= 0 && n % 2 == 0)) { - return n == 0 || even(n - 2); +// A failure on a path that skips the loop has no loop to note. +int skipped(int n) + cv::pre(n >= 0 && n <= 5) + cv::post(cv::result >= 0) +{ + int c = 0; + if (n > 3) { + while (c < n) + cv::invariant(0 <= c && c <= n) + cv::decreases(n - c) + { + c = c + 1; + } + } + return c - 1; } -cppverify::proof void three_is_even() cppverify::post(even(3)) {} -// CHECK-DAG: error: verification failed: three_is_even {{.*}}[reason=counterexample] +// A proof gets no notes. +int count_up_proved(int n) + cv::pre(n >= 0 && n <= 5) + cv::post(cv::result == n) +{ + int c = 0; + while (c < n) + cv::invariant(0 <= c && c <= n) + cv::decreases(n - c) + { + c = c + 1; + } + return c; +} -// Neither: the message names the application. -cppverify::spec bool odd(int n) cppverify::inductive { return n == 1 || odd(n - 2); } +// CHECK: inductive_counterexamples.cpp:16:23: error: verification failed: count_up [{{.*}}::postcondition@16:23] {{.*}}trace: loop.entry@19:3 -> loop.exit@19:3 +// CHECK-NEXT: note: the counterexample's state at the loop at 19:3 is any state its invariants allow, not necessarily one an execution reaches +// CHECK-NEXT: note: no execution fails this check: every loop ends within 5 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof +// CHECK-NEXT: inductive_counterexamples.cpp:29:23: error: verification failed: sum_wrong [{{.*}}::postcondition@29:23] +// CHECK-NEXT: note: the counterexample's state at the loop at 32:3 is any state its invariants allow, not necessarily one an execution reaches +// CHECK-NEXT: note: an execution fails this check within 1 iteration of each loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 1{{.*}}) +// CHECK-NEXT: inductive_counterexamples.cpp:43:23: error: verification failed: far_wrong [{{.*}}::postcondition@43:23] +// CHECK-NEXT: note: the counterexample's state at the loop at 46:3 is any state its invariants allow, not necessarily one an execution reaches +// CHECK-NEXT: note: no execution fails this check within 10 iterations of each loop +// CHECK-NEXT: inductive_counterexamples.cpp:57:23: error: verification failed: no_loop [{{.*}}::postcondition@57:23] +// CHECK-NEXT: inductive_counterexamples.cpp:64:23: error: verification failed: unmeasured [{{.*}}::postcondition@64:23] +// CHECK-NEXT: note: the loop at 67:3 has no cppverify::decreases: a proof would be Unresolved (decreases.missing) until it has one +// CHECK-NEXT: note: the counterexample's state at the loop at 67:3 is any state its invariants allow, not necessarily one an execution reaches +// CHECK-NEXT: note: an execution fails this check with no iteration of any loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 0{{.*}}) +// CHECK-NEXT: inductive_counterexamples.cpp:87:7: error: verification failed: divides [{{.*}}::division-by-zero@87:7] +// CHECK-NEXT: note: the counterexample's state at the loop at 83:3 is any state its invariants allow, not necessarily one an execution reaches +// CHECK-NEXT: note: an execution fails this check within 4 iterations of each loop (counterexample: {{.*}}c [ssa=c_4] [type=i32] = 3{{.*}}) +// CHECK-NEXT: inductive_counterexamples.cpp:100:21: error: verification failed: grows [{{.*}}::invariant-preserved@100:21] +// CHECK-NEXT: note: the counterexample's state at the loop at 99:3 is any state its invariants allow, not necessarily one an execution reaches +// CHECK-NEXT: inductive_counterexamples.cpp:119:5: error: verification failed: two_checks [{{.*}}::assertion@119:5] +// CHECK-NEXT: note: the counterexample's state at the loop at 115:3 is any state its invariants allow, not necessarily one an execution reaches +// CHECK-NEXT: note: an execution fails this check within 5 iterations of each loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 5{{.*}}) +// CHECK-NEXT: inductive_counterexamples.cpp:138:7: error: verification failed: two_kinds [{{.*}}::overflow@138:7] +// CHECK-NEXT: note: the counterexample's state at the loop at 134:3 is any state its invariants allow, not necessarily one an execution reaches +// CHECK-NEXT: note: an execution fails this check within 3 iterations of each loop (counterexample: {{.*}}) +// CHECK-NEXT: inductive_counterexamples.cpp:147:23: error: verification failed: skipped [{{.*}}::postcondition@147:23] +// CHECK-NEXT: Verified: count_up_proved [backend=z3] +// CHECK-NEXT: Summary: 1 verified, 10 failed -cppverify::proof void four_is_odd_too() cppverify::post(odd(4)) {} -// CHECK-DAG: four_is_odd_too {{.*}}whether odd(4) holds: no derivation was found among the heights tried +// Without unrolling, a failure still says where its state comes from. +// NONE: error: verification failed: count_up +// NONE-NEXT: note: the counterexample's state at the loop at 19:3 is any state its invariants allow, not necessarily one an execution reaches +// NONE-NEXT: error: verification failed: sum_wrong -// A postcondition that is not established is no evidence: the -// counterexample that used it is not reported as one. ge(-5000) holds, by a -// derivation too tall to find, while the false postcondition says it -// cannot. -cppverify::spec bool ge(int n); -cppverify::spec bool ge(int n) cppverify::inductive cppverify::post(!cppverify::result || n > -1000) { - return n == 20 || ge(n + 1); -} -// CHECK-DAG: error: spec post by induction failed: ge +// JSON: "function":"count_up",{{.*}}"notes":["the counterexample's state at the loop at 19:3 is any state its invariants allow, not necessarily one an execution reaches","no execution fails this check: every loop ends within 5 iterations{{.*}}"] +// JSON: "function":"no_loop" +// JSON-NOT: "notes" +// JSON: "function":"unmeasured" -cppverify::proof void far() cppverify::post(ge(-5000)) {} -// CHECK-DAG: Unresolved: verification unresolved: far {{.*}}[reason=spec.post] (its counterexample is checked with the postcondition of ge, which is not established) +// OPTION: error: --confirm-bound requires source verification with --backend=z3, cvc5, portfolio, or race From 7539fcfd9230a34a32d5cae050efaacaf53348e2 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:24:21 +0530 Subject: [PATCH 04/19] docs: Describe how a failure after a loop is noted and confirmed. --- website/source/language/functions-loops.rst | 42 +++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index 4c69734279..783e4e62b3 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -638,6 +638,48 @@ rest of the loop, and a ``continue`` goes to the condition, where the invariant must first hold. ``cppverify::ghost`` code cannot leave an executable loop. +A failure is relative to the loop's invariants: after the loop, and at the +start of an iteration, the verifier knows only what they say, so a +counterexample there may start from a state no execution reaches. Such a +failure says so in a note, and the verifier then unrolls each loop, up to +``--confirm-bound`` iterations (10 by default, ``0`` to skip), to look for an +execution that fails the same check, with callees still by their contracts: + +.. code-block:: cpp + + namespace cv = cppverify; + + int count_up(int n) + cv::pre(n >= 0 && n <= 5) + cv::post(cv::result == n) + { + int c = 0; + while (c < n) + cv::decreases(n - c) + { + c = c + 1; + } + return c; + } + +.. code-block:: text + + count_up.cpp:5:23: error: verification failed: count_up [fn_...::postcondition@5:23] (counterexample: result [ssa=__result_1] [type=i32] = 1, c [ssa=c_1] [type=i32] = 0, c [ssa=c_2] [type=i32] = 1, c [ssa=c_3] [type=i32] = 1, n [ssa=n_0] [type=i32] = 0; trace: loop.entry@8:3 -> loop.exit@8:3 -> return.return@13:3 value=1) [backend=z3] [reason=counterexample] + note: the counterexample's state at the loop at 8:3 is any state its invariants allow, not necessarily one an execution reaches + note: no execution fails this check: every loop ends within 5 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +Here the loop has no invariant, so after it ``c`` may be anything; the fix is +``cv::invariant(0 <= c && c <= n)``. When unrolling finds an execution that +fails the check (in any iteration's copy of it, for a check in the loop's +body), the note says within how many iterations and gives that execution; +when it finds neither a failure nor a proof within the bound, the note says +that no execution fails the check within that many iterations. Unrolling +keeps no invariant and no measure, so a failed invariant or measure gets the +first note only. The verdict stays ``verification failed`` either way, since +the claim is not proved. A failure of a function +whose loop has no ``cppverify::decreases`` also notes that loop: with a +proof, the function would still be ``Unresolved`` (``decreases.missing``). + A range-based ``for`` loop over an array (a local array, an array member, a constant table) visits its elements in order. Its contract names the position, ``cppverify::index``, the number of elements before the current From eb69d2ba7e7873843fe71920ca42ea4fdd4e4452 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:24:22 +0530 Subject: [PATCH 05/19] docs: Describe --confirm-bound and the notes of a failure. --- website/source/language/tooling.rst | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index ce079e7dce..f6ed5d1ea6 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -24,6 +24,7 @@ Standalone verifier cpp-verify --no-check-ub file.cpp cpp-verify --profile-quantifiers file.cpp cpp-verify --timeout=20000 file.cpp + cpp-verify --confirm-bound=4 file.cpp cpp-verify --jobs=4 --proof-cache=.cppverify-cache file.cpp cpp-verify --solver-rlimit=500000 --max-query-nodes=50000 file.cpp cpp-verify --diagnostics-format=json file.cpp @@ -777,6 +778,15 @@ False guards are omitted; a guard the model does not determine is retained with JSON ``"active": null`` rather than an invented path choice. Archives preserve the same names, ranges, IDs, and trace data during replay. +A failure may carry notes, printed after it as ``note:`` lines and in JSON as +``notes``: a counterexample that passes through a loop starts from any state +the loop's invariants allow, and what unrolling each loop then finds about +the same check, within ``--confirm-bound`` iterations (default 10; ``0`` +skips it; only with the solver backends, since BMC unrolls already and Lean +runs no solver): an execution that fails it, a proof that none does, or no +failure within the bound. The search takes at most one query timeout. A loop without +``cppverify::decreases`` is noted too (see :doc:`functions-loops`). + Each non-success verification result also carries a stable reason code. Current codes include ``counterexample``, ``solver.timeout``, ``solver.unknown``, ``solver.resource-limit``, ``solver.unavailable``, From a4bca09eb84ed4bec0bae45b80c119988e32b6c8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:24:22 +0530 Subject: [PATCH 06/19] docs: A counterexample after a loop in the book. --- .../part-ii/ch16-when-verification-fails.rst | 35 +++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/website/source/book/part-ii/ch16-when-verification-fails.rst b/website/source/book/part-ii/ch16-when-verification-fails.rst index e349049fa1..a64919f550 100644 --- a/website/source/book/part-ii/ch16-when-verification-fails.rst +++ b/website/source/book/part-ii/ch16-when-verification-fails.rst @@ -29,6 +29,41 @@ text, and IR dumps intentionally make the stream mixed. Malformed display bytes are replaced with the Unicode replacement character, so JSON output remains valid UTF-8. +A counterexample after a loop is only as real as the loop's invariants. At +the loop, the verifier knows what the invariants say and nothing else, so a +loop with too weak an invariant fails a correct function: + +.. code-block:: cpp + + namespace cv = cppverify; + + int count_up(int n) + cv::pre(n >= 0 && n <= 5) + cv::post(cv::result == n) + { + int c = 0; + while (c < n) + cv::decreases(n - c) + { + c = c + 1; + } + return c; + } + +.. code-block:: text + + count_up.cpp:5:23: error: verification failed: count_up [fn_...::postcondition@5:23] (counterexample: result [ssa=__result_1] [type=i32] = 1, c [ssa=c_1] [type=i32] = 0, c [ssa=c_2] [type=i32] = 1, c [ssa=c_3] [type=i32] = 1, n [ssa=n_0] [type=i32] = 0; trace: loop.entry@8:3 -> loop.exit@8:3 -> return.return@13:3 value=1) [backend=z3] [reason=counterexample] + note: the counterexample's state at the loop at 8:3 is any state its invariants allow, not necessarily one an execution reaches + note: no execution fails this check: every loop ends within 5 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +The first note says where the counterexample's state comes from; the second +is what unrolling the loop found about the same check (``--confirm-bound``, +10 iterations by default): here, that every execution passes it, so the +invariant is what is missing (``cv::invariant(0 <= c && c <= n)``). When +unrolling finds an execution that fails the check, the note gives that +execution and the number of iterations, and the bug is in the code or the +contract, not in the invariant. + An undecided query is different from a counterexample. ``Unresolved`` with reason ``solver.timeout``, ``solver.resource-limit``, or ``solver.unknown`` means Z3 timed out, exhausted an explicit resource/query budget, or entered a From 615eb6cfe4008e612de6727d646d4ad9324acc0f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:24:23 +0530 Subject: [PATCH 07/19] docs: List --confirm-bound in the book. --- website/source/book/part-ii/ch15-toolchain-and-flags.rst | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/website/source/book/part-ii/ch15-toolchain-and-flags.rst b/website/source/book/part-ii/ch15-toolchain-and-flags.rst index a495f77f29..ed078e4bcd 100644 --- a/website/source/book/part-ii/ch15-toolchain-and-flags.rst +++ b/website/source/book/part-ii/ch15-toolchain-and-flags.rst @@ -44,6 +44,10 @@ Other flags check (``Verified: spec axiom: twice``), which the default leaves out - ``cpp-verify --list-functions`` — list the functions a run would verify, with their locations and kinds, and verify none +- ``cpp-verify --confirm-bound=N`` — for a failure whose counterexample passes + through a loop, unroll each loop up to ``N`` iterations (default 10, ``0`` + skips it) to find an execution that fails or prove that none does (see + :doc:`ch16-when-verification-fails`) - ``cpp-verify --backend={z3,cvc5,portfolio,race,bmc,lean}`` — verification engine: Z3 (the default), cvc5, both with agreement required (``portfolio``), both at once with the first proof or certified From 79038ec43c618f1d140880918ccd62020f7a5db9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:24:23 +0530 Subject: [PATCH 08/19] docs: Note counterexamples after a loop in the 0.2.0 release notes. --- website/source/release-notes.rst | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 6ab5290185..ba9dda204e 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -483,6 +483,17 @@ are errors at the statement (:doc:`language/functions-loops`). Running cpp-verify ~~~~~~~~~~~~~~~~~~ +**Counterexamples after a loop.** A failure whose counterexample passed +through a loop looked like any other, though its state there came from the +loop's invariants and no execution need reach it: the first loop most users +write, without an invariant, failed with ``c = 0`` after ``while (c < n)``. +Such a failure now says so in a note, and unrolling each loop then looks for +an execution that fails the same check within ``--confirm-bound`` iterations +(default 10): it gives that execution, or says that no execution fails the +check (when unrolling proves it) or that none fails it within the bound. A +failure of a function whose loop has no ``cppverify::decreases`` names that +loop too (:doc:`language/functions-loops`). + **A summary, and what to print.** A run now ends with one line that counts its verdicts by kind, with the reasons of the unresolved ones and the time it took (``Summary: 12 verified, 1 failed, 2 unresolved (spec.fuel 1, From 1472ec74019b23dfb7009736fb048c36df127de9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:24:23 +0530 Subject: [PATCH 09/19] docs: Design the notes and confirmation of a failure after a loop. --- docs/DESIGN.md | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 8bdb1cc29c..d34d26e88b 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1894,7 +1894,16 @@ int safe_fib(int n) cppverify::pre(...) cppverify::post(cppverify::result == fib - `Failed`: a counterexample that holds when every logical function is evaluated at its true definition. It is relative to the declared abstractions only: callee contracts, loop invariants, and `cppverify::modifies` - frames. + frames. A counterexample that passes through a loop starts from any state + the loop's invariants allow, so such a failure says so in a note, and the + verifier unrolls each loop up to `--confirm-bound` iterations (default 10) + to look for an execution that fails the same check, as G5 proposed with + CBMC's and Kani's unrolling: it reports that execution, or that unrolling + proves the check, or that none fails it within the bound. Unrolling keeps + no loop invariant and no measure, so their failures are not confirmed. The verdict stays `Failed` + (decision Q12 of the 0.2 plan): the claim is not proved, and the note + carries the difference. A failure of a function whose loop has no + `cppverify::decreases` names that loop too. - Anything else is `Unresolved` with a reason. `spec.fuel`: every counterexample found relies on a recursive spec beyond what refinement could unfold, the automatic inductions did not prove it, and no counterexample From 018fa6921e1d5db257d6ab60aa10361b776e8977 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:24:24 +0530 Subject: [PATCH 10/19] docs: Describe how a failure after a loop is confirmed by unrolling. --- docs/ARCHITECTURE.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 6471c56e45..8708707f9c 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -752,6 +752,25 @@ function as possibly divergent: its proof, and the proof of every caller, is reported `[partial]`. Calls within an executable or proof recursion cycle assert the decrease of the shared measure at the call site. +**Counterexamples after a loop.** A certified failure (on Z3, cvc5, the +portfolio, or the race) whose trace has an active loop event passed through +the loop's havoc, so its state there is any the invariants allow. The driver +notes that (`VerifyDiagnostic::Notes`, printed as `note:` lines and JSON +`notes`) and confirms it the way BMC verifies: a copy of the function +prepared for unrolling (`SpecInliner::prepareFunction`, the UB checks), each +bound from 0 to `--confirm-bound` unrolled (`LoopUnroller`), passivized +against the interface map, and solved obligation by obligation +(`Z3VerifyBackend::verifyObligations`) with one query timeout for all +bounds. The copies of the failed check are the obligations of its kind at +its source location: one per iteration for a check in a loop's body, none +for a loop's invariant or measure, which unrolling does not keep (then +nothing is noted). A copy that fails at bound `b` is an execution within `b` +iterations of each loop (callees still by their contracts), and its +counterexample is noted; copies that all hold where every loop's unwinding +is proved hold for every execution; copies that hold short of that go on to +the next bound; anything unresolved ends the search without a note. A function with an unmeasured loop (`UnmeasuredLoop`) also +gets a note naming it on any failure. + **Loop exits.** A `break` or `return` inside the body leaves from the inductive iteration: its path guard is recorded and the path ends. After the loop the continuation assumes `(¬choice ∧ ¬cond) ∨ break₁ ∨ … ∨ return₁ ∨ …`. From 5ee269f7c782fc6817c3796feb5603d77a9aff6c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:49:37 +0530 Subject: [PATCH 11/19] verify: Report only the functions --function selects, verifying what their verdicts rely on so that each is a whole run's verdict. --- clang/lib/Verify/Driver/Verifier.cpp | 113 ++++++++++++++++++++++++--- clang/lib/Verify/Driver/Verifier.h | 3 + 2 files changed, 107 insertions(+), 9 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 69b91649ce..68cf461e94 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -38,6 +38,7 @@ #include "llvm/Support/Error.h" #include "llvm/Support/FileSystem.h" #include "llvm/Support/FormatVariadic.h" +#include "llvm/Support/GlobPattern.h" #include "llvm/Support/JSON.h" #include "llvm/Support/MD5.h" #include "llvm/Support/MathExtras.h" @@ -3111,6 +3112,24 @@ class Verifier { // the function is Unresolved, its first error carrying the verdict, and // the rest of the translation unit is verified. An error outside every // function stops the run. + // --function: the functions the run reports, by their names. + std::vector Patterns; + for (const std::string &Text : Opts.FunctionPatterns) { + auto Pattern = llvm::GlobPattern::create(Text); + if (!Pattern) { + Diags.push_back( + {VerifyDiagnostic::Error, "--function=" + Text + ": " + + llvm::toString(Pattern.takeError())}); + return false; + } + Patterns.push_back(std::move(*Pattern)); + } + auto selects = [&](llvm::StringRef Name) { + return Patterns.empty() || + llvm::any_of(Patterns, [&](const llvm::GlobPattern &Pattern) { + return Pattern.match(Name); + }); + }; bool OutsideFunctions = false; std::map UnsupportedConstructs; for (const ConversionError &Err : Converter.getErrors()) { @@ -3121,6 +3140,7 @@ class Verifier { OutsideFunctions = true; else D.FunctionName = Err.FunctionName; + D.Hidden = !Err.Function.empty() && !selects(Err.FunctionName); if (!Err.Function.empty() && UnsupportedConstructs.emplace(Err.Function, Err.Message).second) { VerifyResult R; @@ -3146,10 +3166,37 @@ class Verifier { {VerifyDiagnostic::Warning, "no verifiable functions found"}); return true; } + // A function is selected by the name its verdicts print, which for an + // inductive predicate's step is the predicate's; the predicate's rule + // proofs are reported with it. + std::vector Selected(Functions.size()); + for (size_t I = 0; I != Functions.size(); ++I) { + const VFunction &Fn = *Functions[I]; + Selected[I] = + selects(Fn.InductiveStepOf.empty() ? Fn.Name : Fn.InductiveStepOf); + } + std::set SelectedIdentities; + for (size_t I = 0; I != Functions.size(); ++I) + if (Selected[I]) + SelectedIdentities.insert(Functions[I]->Identity); + for (size_t I = 0; I != Functions.size(); ++I) + Selected[I] = Selected[I] || + SelectedIdentities.count(Functions[I]->InductiveRuleOf); + if (!Patterns.empty() && + llvm::none_of(Selected, [](bool S) { return S; }) && + llvm::none_of(Converter.getErrors(), [&](const ConversionError &Err) { + return !Err.Function.empty() && selects(Err.FunctionName); + })) { + Diags.push_back({VerifyDiagnostic::Error, + "no function matches --function=" + + llvm::join(Opts.FunctionPatterns, ", --function=")}); + return false; + } if (Opts.ListFunctions) { - for (const auto &Fn : Functions) { + for (size_t I = 0; I != Functions.size(); ++I) { + const auto &Fn = Functions[I]; if (Fn->IsBuiltin || Fn->IsChoice || !Fn->InductiveStepOf.empty() || - !Fn->InductiveRuleOf.empty()) + !Fn->InductiveRuleOf.empty() || !Selected[I]) continue; const char *Kind = Fn->IsConstexprSpec ? "constexpr spec" : Fn->IsSpec ? "spec" @@ -4796,14 +4843,51 @@ class Verifier { } DumpStream.flush(); }; - if (Parallel) { - TaskGroup Group(*Pool); + // With --function, the executable functions run are the selected ones + // and, round by round, those whose contracts a verdict of the run relies + // on; specs, proof functions, and generated checks always run, since any + // verdict may rest on their facts. Every verdict reported is then the + // one a run of the whole file gives. + std::vector Scheduled(Functions.size(), true); + if (!Opts.FunctionPatterns.empty()) for (size_t I = 0; I != Functions.size(); ++I) - Group.async([&verifyFunction, I] { verifyFunction(I); }); - Group.wait(); - } else { - for (size_t I = 0; I != Functions.size(); ++I) - verifyFunction(I); + Scheduled[I] = + Selected[I] || Functions[I]->IsSpec || Functions[I]->IsProof; + std::map IndexOf; + for (size_t I = 0; I != Functions.size(); ++I) + IndexOf.emplace(Functions[I]->Identity, I); + std::vector Batch; + for (size_t I = 0; I != Functions.size(); ++I) + if (Scheduled[I]) + Batch.push_back(I); + while (!Batch.empty()) { + if (Parallel) { + TaskGroup Group(*Pool); + for (size_t I : Batch) + Group.async([&verifyFunction, I] { verifyFunction(I); }); + Group.wait(); + } else { + for (size_t I : Batch) + verifyFunction(I); + } + std::vector Next; + auto need = [&](const std::string &Identity) { + auto It = IndexOf.find(Identity); + if (It != IndexOf.end() && !Scheduled[It->second]) { + Scheduled[It->second] = true; + Next.push_back(It->second); + } + }; + for (size_t I : Batch) { + for (const auto &[Index, Identity, Callees] : Runs[I].CallDependencies) + for (const std::string &Callee : Callees) + need(Callee); + for (const SpecReliance &Reliance : Runs[I].ProofDependencies) + for (const std::string &Callee : Reliance.Callees) + need(Callee); + } + llvm::sort(Next); + Batch = std::move(Next); } // A function whose verification Ctrl-C cut short is reported by one // line. Its verdicts stay, hidden, for what they establish: a query the @@ -4834,6 +4918,9 @@ class Verifier { for (VerifyDiagnostic &D : Run.Diags) { if (D.FindingOf) *D.FindingOf += Base; + // What a function --function leaves out reports stays, hidden, for + // what it establishes. + D.Hidden |= !Selected[I]; Diags.push_back(std::move(D)); } AllOk &= Run.AllOk; @@ -5691,6 +5778,14 @@ class Verifier { } } + // A run --function narrows succeeds when what it reports does. + if (!Opts.FunctionPatterns.empty()) + return llvm::none_of(Diags, [](const VerifyDiagnostic &D) { + return !D.Hidden && (D.K == VerifyDiagnostic::Error || + D.K == VerifyDiagnostic::Unresolved || + D.K == VerifyDiagnostic::Interrupted || + D.K == VerifyDiagnostic::BoundedSafe); + }); return AllOk; } diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h index a7c4803241..4217da5f90 100644 --- a/clang/lib/Verify/Driver/Verifier.h +++ b/clang/lib/Verify/Driver/Verifier.h @@ -109,6 +109,9 @@ struct VerifyOptions { bool Verbose = false; /// List the functions the run would verify, and verify none. bool ListFunctions = false; + /// Glob patterns over function names: only the functions they match are + /// reported. Empty: every function. + std::vector FunctionPatterns; /// For a failure whose counterexample passes through a loop, the most /// iterations of each loop that unrolling may try to find an execution /// that fails (0: do not try). From 5875c2474ac4582bc7b0fa79cc61e05dd9da76ea Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:49:37 +0530 Subject: [PATCH 12/19] verify: Add --function, a repeatable glob over function names. --- clang/tools/cpp-verify/Main.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index 863e327449..5a63665c5a 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -285,6 +285,12 @@ static cl::opt ConfirmBound( "execution that fails (default 10, 0 = do not look)"), cl::init(10), cl::cat(CppVerifyCategory)); +static cl::list FunctionPatterns( + "function", + cl::desc("Report only the functions whose names match this glob pattern " + "(repeatable); what their verdicts rely on is verified too"), + cl::value_desc("pattern"), cl::cat(CppVerifyCategory)); + static cl::opt ListFunctions( "list-functions", cl::desc("List the functions a run would verify, with their kinds and " @@ -444,6 +450,8 @@ class VerifyConsumer : public ASTConsumer { VOpts.Quiet = Quiet.getValue(); VOpts.Verbose = Verbose.getValue(); VOpts.ListFunctions = ListFunctions.getValue(); + VOpts.FunctionPatterns.assign(FunctionPatterns.begin(), + FunctionPatterns.end()); VOpts.ConfirmBound = ConfirmBound.getValue(); VOpts.Summary = &gSummary; if (!verify::verifyTranslationUnit(Ctx, llvm::outs(), VOpts)) From 014b8c105529c7b3b4ad54ba1fe42b5aef6e248b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:49:38 +0530 Subject: [PATCH 13/19] test: --function keeps a whole run's verdicts and verifies nothing else that is executable. --- clang/test/Verify/suite/function_filter.cpp | 150 ++++++++++++++++++++ 1 file changed, 150 insertions(+) create mode 100644 clang/test/Verify/suite/function_filter.cpp diff --git a/clang/test/Verify/suite/function_filter.cpp b/clang/test/Verify/suite/function_filter.cpp new file mode 100644 index 0000000000..91da544d7e --- /dev/null +++ b/clang/test/Verify/suite/function_filter.cpp @@ -0,0 +1,150 @@ +// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s --check-prefix=ALL +// RUN: not %cpp-verify --jobs=1 --function=uses_wrong %s -- 2>&1 | FileCheck %s --check-prefix=ONE --implicit-check-not=Verified --implicit-check-not=error: +// RUN: %cpp-verify --jobs=1 --function='add_*' %s -- 2>&1 | FileCheck %s --check-prefix=GLOB --implicit-check-not=uses_ --implicit-check-not=error: +// RUN: rm -f %t.cpv +// RUN: not %cpp-verify --jobs=1 --function=uses_wrong --obligation-out=%t.cpv %s -- > /dev/null 2>&1 +// RUN: not %cpp-verify --obligation-in=%t.cpv 2>&1 | FileCheck %s --check-prefix=RAN --implicit-check-not=add_two +// RUN: %cpp-verify --jobs=1 --function=uses_add %s -- 2>&1 | FileCheck %s --check-prefix=CALLEE --implicit-check-not=Verified +// RUN: not %cpp-verify --jobs=1 --function=uses_bad %s -- 2>&1 | FileCheck %s --check-prefix=SPEC --implicit-check-not=error: +// RUN: %cpp-verify --jobs=1 --function=reach %s -- 2>&1 | FileCheck %s --check-prefix=PREDICATE --implicit-check-not=Verified +// RUN: not %cpp-verify --jobs=1 --function=climbs %s -- 2>&1 | FileCheck %s --check-prefix=STEP +// RUN: not %cpp-verify --jobs=1 --solver-rlimit=1 --function=reach %s -- 2>&1 | FileCheck %s --check-prefix=RULES +// RUN: not %cpp-verify --jobs=1 --function=nothing %s -- 2>&1 | FileCheck %s --check-prefix=NONE +// RUN: %cpp-verify --list-functions --function='add_*' %s -- 2>&1 | FileCheck %s --check-prefix=LIST --implicit-check-not=uses_ +// +// --function reports only the functions whose names match: a glob pattern, +// repeatable. What their verdicts rely on is verified too, so each verdict +// is the one a run of the whole file gives; what they do not rely on is not +// verified at all. + +namespace cv = cppverify; + +int add_one(int x) + cv::pre(x < 100) + cv::post(cv::result == x + 1) +{ + return x + 1; +} + +int add_two(int x) + cv::pre(x < 100) + cv::post(cv::result == x + 2) +{ + return x + 2; +} + +int wrong(int x) + cv::pre(x < 100) + cv::post(cv::result == x) +{ + return x + 1; +} + +int uses_wrong(int x) + cv::pre(x < 50) + cv::post(cv::result == x + 1) +{ + int y = wrong(x); + return y + 1; +} + +int uses_add(int x) + cv::pre(x < 50) + cv::post(cv::result == x + 2) +{ + int y = add_one(x); + return y + 1; +} + +// A spec whose termination fails has no definition, whoever is selected. +cv::spec int bad(int n) + cv::decreases(n) +{ + return n > 100 ? 0 : bad(n + 1); +} + +int uses_bad(int x) + cv::post(bad(x) == bad(x) + 0) +{ + return x; +} + +int jumps(int x) + cv::post(true) +{ + goto done; +done: + return x; +} + +cv::spec bool edge(int a, int b) { return b == a + 1; } + +cv::spec bool reach(int a, int b) + cv::inductive +{ + return a == b || cv::exists(c, edge(a, c) && reach(c, b)); +} + +// Its postcondition is false at a == b; the induction that refutes it is +// a generated function. +cv::spec bool climbs(int a, int b) + cv::inductive + cv::post(!cv::result || a < b) +{ + return a == b || cv::exists(c, edge(a, c) && climbs(c, b)); +} + +// ALL: Verified: add_one [backend=z3] +// ALL: Verified: add_two [backend=z3] +// ALL: error: verification failed: wrong +// ALL: Unresolved: uses_wrong [backend=z3] [reason=callee.contract] (relies on the contract of wrong, which is not established) +// ALL: Verified: uses_add [backend=z3] +// ALL: error: spec decreases failed: bad +// ALL: Unresolved: uses_bad [backend=z3] [reason=spec.termination] +// ALL: Verified: inductive predicate: reach +// ALL: Verified: inductive predicate: climbs +// ALL: Unresolved: spec post: climbs [reason=spec.post] +// ALL: error: spec post by induction failed: climbs +// ALL: Summary: 5 verified, 3 failed, 4 unresolved (callee.contract 1, construct.unsupported 1, spec.post 1, spec.termination 1) + +// The same verdict, alone: wrong is verified, and its failure demotes it. +// ONE: Unresolved: uses_wrong [backend=z3] [reason=callee.contract] (relies on the contract of wrong, which is not established) +// ONE-NEXT: Summary: 1 unresolved (callee.contract 1) + +// GLOB: Verified: add_one [backend=z3] +// GLOB-NEXT: Verified: add_two [backend=z3] +// GLOB-NEXT: Summary: 2 verified + +// Only uses_wrong and what it relies on were verified. +// RAN-DAG: wrong +// RAN-DAG: uses_wrong + +// A callee that verifies is verified, so its caller is. +// CALLEE: Verified: uses_add [backend=z3] +// CALLEE-NEXT: Summary: 1 verified + +// SPEC: Unresolved: uses_bad [backend=z3] [reason=spec.termination] (relies on the definition of bad, whose termination is not established) +// SPEC-NEXT: Summary: 1 unresolved (spec.termination 1) + +// An inductive predicate is reported with its rules. +// PREDICATE: Verified: inductive predicate: reach +// PREDICATE-NEXT: Summary: 1 verified + +// Its step and rule proofs are reported with it when they do not hold. +// RULES: Unresolved: inductive predicate: reach [reason=spec.inductive] (its rules are not established: monotonicity, case analysis, introduction) +// RULES-NEXT: function_filter.cpp:[[#]]:3: Unresolved: spec decreases unresolved: reach +// RULES-NEXT: function_filter.cpp:[[#]]:3: Unresolved: reach (monotonicity) +// RULES-NEXT: function_filter.cpp:[[#]]:3: Unresolved: reach (case analysis) +// RULES-NEXT: function_filter.cpp:[[#]]:3: Unresolved: reach (introduction) +// RULES-NEXT: Summary: 5 unresolved ({{.*}}spec.inductive 1) + +// The induction of a generated function is reported with its predicate. +// STEP: Verified: inductive predicate: climbs +// STEP-NEXT: Unresolved: spec post: climbs [reason=spec.post] (relies on the postcondition of climbs.step, which is not established) +// STEP-NEXT: function_filter.cpp:92:24: error: spec post by induction failed: climbs +// STEP-NEXT: Summary: 1 verified, 1 failed, 1 unresolved (spec.post 1) + +// NONE: error: no function matches --function=nothing + +// LIST: function_filter.cpp:22:5: function add_one +// LIST-NEXT: function_filter.cpp:29:5: function add_two From d169b2acee9290bf1a37559589169575ccd9e455 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:49:38 +0530 Subject: [PATCH 14/19] docs: Describe --function. --- website/source/language/tooling.rst | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index f6ed5d1ea6..070eee43b1 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -11,6 +11,7 @@ Standalone verifier cpp-verify --quiet file.cpp cpp-verify --verbose file.cpp cpp-verify --list-functions file.cpp + cpp-verify --function='parse_*' --function=encode file.cpp cpp-verify file.cpp -- -I include -DNDEBUG cpp-verify --backend=z3 file.cpp cpp-verify --backend=cvc5 file.cpp @@ -213,6 +214,22 @@ whole output, of ``--list-functions``, and of archive replay summary.cpp:5:5: function add_one summary.cpp:12:5: function add_two +``--function=PATTERN`` reports only the functions whose names match the glob +pattern (``*``, ``?``, ``[...]``; repeatable, a function matching any is +reported), as ``Verified`` and the other lines print the name: ``Ring::push``, +``total``; an inductive predicate is reported with the checks generated +for it (its step's termination and induction, its rule proofs). Every verdict +it reports is the one a run of the whole file gives: the functions whose +contracts those verdicts rely on are verified too, round by round, and so +are all spec and proof functions, whose facts any +proof may use; their results are not printed, and a selected function that +relies on a callee whose verification fails is ``Unresolved`` with +``callee.contract`` exactly as in a whole run. An executable function no +reported verdict relies on is not verified at all. The exit status follows +what is reported: 0 when every reported verdict is a proof. A pattern that +matches no function is an error. With ``--list-functions`` it narrows the +listing. + ``cpp-verify --help`` shows each time limit's default (``--timeout``, 30000 ms). From 02abd632bb5bce41d646802a0dc875e22dfb0441 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:49:38 +0530 Subject: [PATCH 15/19] docs: List --function in the book. --- website/source/book/part-ii/ch15-toolchain-and-flags.rst | 3 +++ 1 file changed, 3 insertions(+) diff --git a/website/source/book/part-ii/ch15-toolchain-and-flags.rst b/website/source/book/part-ii/ch15-toolchain-and-flags.rst index ed078e4bcd..f059a1b3d3 100644 --- a/website/source/book/part-ii/ch15-toolchain-and-flags.rst +++ b/website/source/book/part-ii/ch15-toolchain-and-flags.rst @@ -44,6 +44,9 @@ Other flags check (``Verified: spec axiom: twice``), which the default leaves out - ``cpp-verify --list-functions`` — list the functions a run would verify, with their locations and kinds, and verify none +- ``cpp-verify --function=PATTERN`` — report only the functions whose names + match a glob pattern (repeatable), with the same verdicts as a whole run: + what they rely on is verified too, and nothing else that is executable - ``cpp-verify --confirm-bound=N`` — for a failure whose counterexample passes through a loop, unroll each loop up to ``N`` iterations (default 10, ``0`` skips it) to find an execution that fails or prove that none does (see From 5d03561edb3df3c97292e8a5d0ffb9d09c4c8b61 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:49:39 +0530 Subject: [PATCH 16/19] docs: Note --function in the 0.2.0 release notes. --- website/source/release-notes.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index ba9dda204e..4dc149b3bc 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -498,7 +498,9 @@ loop too (:doc:`language/functions-loops`). its verdicts by kind, with the reasons of the unresolved ones and the time it took (``Summary: 12 verified, 1 failed, 2 unresolved (spec.fuel 1, solver.timeout 1) in 3.2 s``). ``--quiet`` prints only what needs attention, -``--list-functions`` lists what a run would verify without verifying it, and +``--list-functions`` lists what a run would verify without verifying it, +``--function=PATTERN`` reports only the functions a glob pattern matches, +with the verdicts a whole run gives, and the ``Verified: spec axiom: f`` line of a spec that needs no check is printed only with ``--verbose``. ``--help`` shows the default of ``--timeout`` (:doc:`language/tooling`). From 9736285ea740b1e45b2d2e988fd9219743c81535 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:49:39 +0530 Subject: [PATCH 17/19] docs: Describe how --function schedules what the reported verdicts rely on. --- docs/ARCHITECTURE.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 8708707f9c..566bfd31b4 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -2403,7 +2403,17 @@ expression being converted (`ASTConverter::CurrentRange`), unless the site names a place of its own, such as a function for the checks made after every function is converted. It is printed with Clang's `TextDiagnostic`, line and caret included, as a compiler error is, and its JSON record carries the range. -A text run ends with a summary line: `printDiagnostics` counts each verdict +`--function` filters what a run reports, not what its verdicts mean. A +function is selected by the name its verdicts print, which for an inductive +predicate's step (`InductiveStepOf`) is the predicate's, and a selected +predicate's rule proofs (`InductiveRuleOf`) with it. `Verifier::run` +schedules the selected functions, every spec and proof +function (any verdict may rest on their facts, and a confirmation by proof +on any established lemma), and then, round by round, each executable +function whose contract a run's verdicts call (`CallDependencies`, proof +blocks' `Callees`), until none is new. The fixpoints then run as for the +whole file over the verdicts there are; the diagnostics of functions not +selected stay, hidden, for what they establish. A text run ends with a summary line: `printDiagnostics` counts each verdict it prints into the run's `VerifySummary` (a first error that carries a verdict counts, a `--verbose` spec axiom line does not), and the driver prints the counts of every file of the run with its time. From 20a8d3f5fd8b799697bdc7855b84238aa148c678 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 06:42:08 +0530 Subject: [PATCH 18/19] verify: Stop looking for an execution that fails a check unrolling drops. --- clang/lib/Verify/Driver/Verifier.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 69b91649ce..8b9889edfe 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -3558,6 +3558,12 @@ class Verifier { CopiesHold &= Result.Status == VerifyStatus::Verified; } Unrolled |= Copies; + // Unrolled once, every loop body holds a copy of each of its + // checks, and a check after a loop has one from no iteration on; + // a failure without a copy by then is of an invariant or a + // measure, which unrolling drops at every bound. + if (Bound >= 1 && !Unrolled) + return Notes; if (!CopiesHold) return Notes; if (Copies && Unwound) { From 7f3c99a756bd8613f33d701751e4ab2eb6b80334 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 06:42:09 +0530 Subject: [PATCH 19/19] docs: Say a failed invariant or measure gets no unrolling search in tooling. --- website/source/language/tooling.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index f6ed5d1ea6..129c92cf10 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -784,7 +784,9 @@ the loop's invariants allow, and what unrolling each loop then finds about the same check, within ``--confirm-bound`` iterations (default 10; ``0`` skips it; only with the solver backends, since BMC unrolls already and Lean runs no solver): an execution that fails it, a proof that none does, or no -failure within the bound. The search takes at most one query timeout. A loop without +failure within the bound. The search takes at most one query timeout. Unrolling +drops the loops' invariants and measures, so a failure of one gets no +search: it would find no copy of the check at any bound. A loop without ``cppverify::decreases`` is noted too (see :doc:`functions-loops`). Each non-success verification result also carries a stable reason code. Current