From 038cccfc3f39de35d6a1d3802a0564c44b27291d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:24:20 +0530 Subject: [PATCH 01/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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 fac2e5095f9feac741cc9d05c91a039ac6f2c8a6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:44 +0530 Subject: [PATCH 17/32] verify: Carry the failures a module reports after its first, each with its counterexample and backend. --- clang/lib/Verify/Backend/VerifyBackend.cpp | 3 +++ clang/lib/Verify/Backend/VerifyBackend.h | 6 ++++++ 2 files changed, 9 insertions(+) diff --git a/clang/lib/Verify/Backend/VerifyBackend.cpp b/clang/lib/Verify/Backend/VerifyBackend.cpp index fac014a9f8..8a7a52238c 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.cpp +++ b/clang/lib/Verify/Backend/VerifyBackend.cpp @@ -603,6 +603,9 @@ VerifyResult VerifyBackend::verifyDirect(const ObligationModule &Module) { VerifyResult Result = verifyModule(Module); if (Result.BackendName.empty()) Result.BackendName = getName().str(); + for (VerifyResult &More : Result.MoreFailures) + if (More.BackendName.empty()) + More.BackendName = Result.BackendName; if (!Capabilities.ProducesVerificationVerdict && Result.Status != VerifyStatus::Exported && Result.Status != VerifyStatus::Unresolved) { diff --git a/clang/lib/Verify/Backend/VerifyBackend.h b/clang/lib/Verify/Backend/VerifyBackend.h index f006f4a5dc..2c2c8b2396 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.h +++ b/clang/lib/Verify/Backend/VerifyBackend.h @@ -138,6 +138,9 @@ struct VerifyResult { std::string Message; std::vector Model; std::vector Trace; + /// The failing obligations after this one, in order, each with its own + /// counterexample, as many as the run's MaxFailures allows. + std::vector MoreFailures; std::string ObligationId; std::optional ObligationType; /// For a certified counterexample: the value of every free variable of the @@ -269,6 +272,9 @@ struct BackendExecutionOptions { /// unresolved. Interactive fallback backends can consume those unresolved /// obligations without spending a second whole-module timeout budget. bool SkipWholeModuleRetry = false; + /// How many failing obligations of a module are reported, each with its + /// own counterexample; 0 reports every one. + unsigned MaxFailures = 1; /// Solve the whole-module query once, at the full budget, and report it: /// no per-obligation queries, refinement fallback, or induction. For small /// auxiliary questions such as the vacuity checks. From 68a5856eaf28f50c6741a688896032b2cfff6d34 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:44 +0530 Subject: [PATCH 18/32] verify: Report up to --max-failures failing obligations of a module, solving each after the first past the earlier failures. --- clang/lib/Verify/Backend/Z3Encode.cpp | 133 ++++++++++++++++++++------ clang/lib/Verify/Backend/Z3Encode.h | 28 ++++-- 2 files changed, 126 insertions(+), 35 deletions(-) diff --git a/clang/lib/Verify/Backend/Z3Encode.cpp b/clang/lib/Verify/Backend/Z3Encode.cpp index 93cc05b0f5..41e868970c 100644 --- a/clang/lib/Verify/Backend/Z3Encode.cpp +++ b/clang/lib/Verify/Backend/Z3Encode.cpp @@ -3544,8 +3544,8 @@ static VerifyResult finishZ3Result(VerifyResult Result) { std::vector Z3VerifyBackend::verifyObligations(const ObligationModule &Module, - bool StopAtFailure, Race *Racing, - unsigned TimeoutCapMs) { + std::optional ReportedFailures, + Race *Racing, unsigned TimeoutCapMs) { TimeoutMs = budget(moduleTimeoutMs(Module, SolverTimeoutMs, CollectionTimeoutMs)); if (TimeoutCapMs != 0) @@ -3575,13 +3575,31 @@ Z3VerifyBackend::verifyObligations(const ObligationModule &Module, auto IsReused = [&](size_t I) { return ReuseVerifiedQueries && VerifiedQueries.count(QueryHashes[I]) != 0; }; + // When failures are reported, each obligation after the first failure is + // solved in the executions that pass every earlier one that fails, as + // Boogie assumes an assertion after checking it: alone, its counterexample + // could start where an earlier check already fails, and fixing that one + // would remove it. A check not settled is not assumed, so a proof past + // the failures rests on no check that may not hold. + const unsigned StopAfterFailures = ReportedFailures.value_or(0); + std::vector Failing; + std::vector PastEarlier(Module.Obligations.size()); if (Jobs == 1 || Module.Obligations.size() < 2) { + unsigned Failures = 0; for (size_t I = 0; I != Module.Obligations.size(); ++I) { - Results.push_back(verifyObligation( - Module, Module.Obligations[I], - Cache ? llvm::StringRef(CacheHashes[I]) : llvm::StringRef(), - Cache ? &CacheLookups[I] : nullptr, IsReused(I), Racing)); - if (StopAtFailure && Results.back().Status == VerifyStatus::Failed) + PastEarlier[I] = ReportedFailures && Failures != 0; + Results.push_back( + PastEarlier[I] + ? verifyPastEarlier(Module, I, Failing, Racing) + : verifyObligation(Module, Module.Obligations[I], + Cache ? llvm::StringRef(CacheHashes[I]) + : llvm::StringRef(), + Cache ? &CacheLookups[I] : nullptr, + IsReused(I), Racing)); + if (Results.back().Status != VerifyStatus::Failed) + continue; + Failing.push_back(I); + if (++Failures == StopAfterFailures) break; } } else { @@ -3605,10 +3623,26 @@ Z3VerifyBackend::verifyObligations(const ObligationModule &Module, Group.wait(); for (std::shared_future &Future : Futures) Results.push_back(Future.get()); + // A failure after the first is solved again past the earlier checks; a + // proof or an unresolved result stays one there. + unsigned Failures = 0; + for (size_t I = 0; + ReportedFailures && I != Results.size() && + (StopAfterFailures == 0 || Failures < StopAfterFailures); + ++I) { + if (Failures != 0 && Results[I].Status == VerifyStatus::Failed) { + PastEarlier[I] = true; + Results[I] = verifyPastEarlier(Module, I, Failing, Racing); + } + if (Results[I].Status == VerifyStatus::Failed) { + Failing.push_back(I); + ++Failures; + } + } } if (ReuseVerifiedQueries) for (size_t I = 0; I != Results.size(); ++I) - if (Results[I].Status == VerifyStatus::Verified) + if (Results[I].Status == VerifyStatus::Verified && !PastEarlier[I]) VerifiedQueries.insert(QueryHashes[I]); return Results; } @@ -3620,7 +3654,8 @@ Z3VerifyBackend::Z3VerifyBackend(const BackendExecutionOptions &Execution, SolverTimeoutMs(Execution.SolverTimeoutMs), CollectionTimeoutMs(Execution.CollectionTimeoutMs), ResourceLimit(Execution.SolverResourceLimit), Jobs(Execution.Jobs), - Pool(Execution.Pool), MaxQueryNodes(Execution.MaxQueryNodes), + MaxFailures(Execution.MaxFailures), Pool(Execution.Pool), + MaxQueryNodes(Execution.MaxQueryNodes), IntegerEncoding(Execution.IntegerEncoding), SkipWholeModuleRetry(Execution.SkipWholeModuleRetry), SingleQuery(Execution.SingleQuery), @@ -3738,6 +3773,18 @@ VerifyResult Z3VerifyBackend::solveQuery( return WithFacts; } +/// \p Result as the result of obligation \p Item. +static VerifyResult attributed(VerifyResult Result, const Obligation &Item) { + Result.ObligationId = Item.StableId.empty() ? Item.Id : Item.StableId; + Result.ObligationType = Item.Kind; + Result.Location = Item.Loc; + Result.Source = Item.Source; + if (Result.Status == VerifyStatus::Unresolved) + Result.Message = "proof obligation " + Result.ObligationId + + (Result.Message.empty() ? "" : ": " + Result.Message); + return finishZ3Result(std::move(Result)); +} + VerifyResult Z3VerifyBackend::verifyObligation(const ObligationModule &Module, const Obligation &Item, llvm::StringRef SemanticHash, @@ -3785,14 +3832,31 @@ VerifyResult Z3VerifyBackend::verifyObligation(const ObligationModule &Module, } } - Result.ObligationId = Item.StableId.empty() ? Item.Id : Item.StableId; - Result.ObligationType = Item.Kind; - Result.Location = Item.Loc; - Result.Source = Item.Source; - if (Result.Status == VerifyStatus::Unresolved) - Result.Message = "proof obligation " + Result.ObligationId + - (Result.Message.empty() ? "" : ": " + Result.Message); - return finishZ3Result(std::move(Result)); + return attributed(std::move(Result), Item); +} + +VerifyResult +Z3VerifyBackend::verifyPastEarlier(const ObligationModule &Module, size_t I, + const std::vector &Earlier, + Race *Racing) { + const Obligation &Item = Module.Obligations[I]; + auto Query = cloneLogicExpr(Item.CounterexampleQuery.get()); + for (size_t J : Earlier) { + auto Conjunction = std::make_unique(LogicExpr::And); + Conjunction->Sort = LogicSort::boolSort(); + Conjunction->Loc = Query->Loc; + Conjunction->EndLoc = Query->EndLoc; + Conjunction->Source = Query->Source; + Conjunction->Children.push_back(std::move(Query)); + Conjunction->Children.push_back( + cloneLogicExpr(Module.Obligations[J].Goal.get())); + Query = std::move(Conjunction); + } + return attributed(spent() ? timeSpent() + : solveQuery(Module, Query.get(), + Item.TraceEventCount, + budget(TimeoutMs), Racing), + Item); } /// Internal IDs of the obligations that one-to-one Results did not prove. @@ -3808,6 +3872,17 @@ unprovedObligations(const ObligationModule &Module, return Unproved; } +VerifyResult +Z3VerifyBackend::withMoreFailures(std::vector &Results, + size_t First) { + VerifyResult Reported = std::move(Results[First]); + for (size_t I = First + 1; I != Results.size(); ++I) + if (Results[I].Status == VerifyStatus::Failed && + (MaxFailures == 0 || Reported.MoreFailures.size() + 1 < MaxFailures)) + Reported.MoreFailures.push_back(std::move(Results[I])); + return Reported; +} + VerifyResult Z3VerifyBackend::verifyModule(const ObligationModule &Module) { TimeoutMs = budget(moduleTimeoutMs(Module, SolverTimeoutMs, CollectionTimeoutMs)); @@ -3962,7 +4037,7 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) { Group.emplace(*Pool); Ordered = Group->async([this, &Module, &Rivals, &WholeRace] { std::vector Results = - verifyObligations(Module, /*StopAtFailure=*/true, &Rivals); + verifyObligations(Module, MaxFailures, &Rivals); // The obligations settle the module when they prove all of it or one // fails, and the whole query, or its retry, is then stopped. if (llvm::any_of(Results, @@ -4018,8 +4093,7 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) { if (Whole.Status == VerifyStatus::Verified) return finishZ3Result(std::move(Whole)); auto orderedResults = [&] { - return Racing ? Ordered.get() - : verifyObligations(Module, /*StopAtFailure=*/true); + return Racing ? Ordered.get() : verifyObligations(Module, MaxFailures); }; if (Whole.Status == VerifyStatus::Failed) { @@ -4032,18 +4106,18 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) { TimeoutMs = FullTimeout; UnitsCap = 0; }); - std::vector Results = verifyObligations( - Module, /*StopAtFailure=*/true, nullptr, WholeTimeout); + std::vector Results = + verifyObligations(Module, MaxFailures, nullptr, WholeTimeout); bool SawUnresolved = false; - for (VerifyResult &Result : Results) { - if (Result.Status == VerifyStatus::Verified) + for (size_t I = 0; I != Results.size(); ++I) { + if (Results[I].Status == VerifyStatus::Verified) continue; - if (Result.Status == VerifyStatus::Unresolved) { + if (Results[I].Status == VerifyStatus::Unresolved) { SawUnresolved = true; continue; } - if (Result.Status == VerifyStatus::Failed) - return std::move(Result); + if (Results[I].Status == VerifyStatus::Failed) + return withMoreFailures(Results, I); } if (SawUnresolved) return finishZ3Result(std::move(Whole)); @@ -4070,13 +4144,16 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) { std::optional> Unproved = unprovedObligations(Module, Results); std::optional FirstUnresolved; - for (VerifyResult &Result : Results) { + for (size_t I = 0; I != Results.size(); ++I) { + VerifyResult &Result = Results[I]; if (Result.Status != VerifyStatus::Verified) { if (Result.Status == VerifyStatus::Unresolved) { if (!FirstUnresolved) FirstUnresolved = std::move(Result); continue; } + if (Result.Status == VerifyStatus::Failed) + return withMoreFailures(Results, I); return std::move(Result); } } diff --git a/clang/lib/Verify/Backend/Z3Encode.h b/clang/lib/Verify/Backend/Z3Encode.h index 9fc483a24b..2185f4b88c 100644 --- a/clang/lib/Verify/Backend/Z3Encode.h +++ b/clang/lib/Verify/Backend/Z3Encode.h @@ -328,6 +328,8 @@ class Z3VerifyBackend : public VerifyBackend { /// of their queries may do: the work the complete query's probe had, or 0. unsigned UnitsCap = 0; unsigned Jobs; + /// How many failing obligations a module reports; 0: every one. + unsigned MaxFailures; llvm::StdThreadPool *Pool; uint64_t MaxQueryNodes; MachineIntegerEncoding IntegerEncoding; @@ -340,6 +342,10 @@ class Z3VerifyBackend : public VerifyBackend { std::optional Deadline; unsigned budget(unsigned Ms) const { return withinDeadline(Ms, Deadline); } + /// The failure at First of the results of verifyObligations, carrying the + /// failures after it, as many as MaxFailures allows. + VerifyResult withMoreFailures(std::vector &Results, + size_t First); /// The function's time is spent, so no further query starts. bool spent() const { return Cancellation.Cancelled || @@ -376,6 +382,12 @@ class Z3VerifyBackend : public VerifyBackend { llvm::StringRef SemanticHash = {}, const ProofCacheLookup *Lookup = nullptr, bool Reused = false, Race *Racing = nullptr); + /// Obligation \p I of \p Module in the executions that pass every one of + /// \p Earlier, failing obligations before it. No cache holds it, since it + /// asks less than the obligation. + VerifyResult verifyPastEarlier(const ObligationModule &Module, size_t I, + const std::vector &Earlier, + Race *Racing); public: explicit Z3VerifyBackend(const BackendExecutionOptions &Execution = {}, @@ -385,13 +397,15 @@ class Z3VerifyBackend : public VerifyBackend { BackendCapabilities getCapabilities() const override { return {allLogicFeatures(), true}; } - /// One result per obligation in order. With StopAtFailure a serial run ends - /// after the first failure, since later results cannot change it. A nonzero - /// TimeoutCapMs bounds every query's timeout. - std::vector verifyObligations(const ObligationModule &Module, - bool StopAtFailure = false, - Race *Racing = nullptr, - unsigned TimeoutCapMs = 0); + /// One result per obligation in order, each solved alone. With + /// ReportedFailures, a serial run ends after that many failures (0: never), + /// since later results are not reported, and each obligation after the + /// first failure is solved in the executions that pass every earlier one + /// that fails. A nonzero TimeoutCapMs bounds every query's timeout. + std::vector + verifyObligations(const ObligationModule &Module, + std::optional ReportedFailures = std::nullopt, + Race *Racing = nullptr, unsigned TimeoutCapMs = 0); void cancel() override { Cancellation.cancel(); } void resume() override { Cancellation.reset(); } std::optional From 42ec76201f4e8641693e02b888faa512cacbb18e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:44 +0530 Subject: [PATCH 19/32] verify: Print each failure a function reports with its notes, and confirm a failure after a loop past the checks that fail before it. --- clang/lib/Verify/Driver/Verifier.cpp | 79 ++++++++++++++++++++++------ clang/lib/Verify/Driver/Verifier.h | 3 ++ 2 files changed, 66 insertions(+), 16 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 68cf461e94..61d51814b1 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -1105,6 +1105,9 @@ struct VerifyDiagnostic { bool Axiom = false; /// What else the verifier found about the verdict, each printed as a note. std::vector Notes; + /// A failing obligation after the one a function's verdict reports: no + /// verdict of its own. + bool Additional = false; }; static std::string backendSuffix(const VerifyResult &Result) { @@ -3272,6 +3275,7 @@ class Verifier { Execution.MaxQueryNodes = Opts.MaxQueryNodes; Execution.IntegerEncoding = Opts.IntegerEncoding; Execution.SkipWholeModuleRetry = !Opts.LeanFallbackProjectPath.empty(); + Execution.MaxFailures = Opts.MaxFailures; Execution.CVC5Path = Opts.CVC5Path; Execution.ProfileQuantifiers = Opts.ProfileQuantifiers; Execution.ProofCachePath = Opts.ProofCachePath; @@ -3562,6 +3566,7 @@ class Verifier { Result.Source.File == Failure.Source.File; }; bool Unrolled = false; + std::string Earlier; for (unsigned Bound = 0; Bound <= Opts.ConfirmBound; ++Bound) { VFunction Copy = LoopUnroller::unroll(Bounded, Bound); Passivizer Unrolling; @@ -3582,7 +3587,29 @@ class Verifier { bool Copies = false; bool CopiesHold = true; bool Unwound = true; - for (VerifyResult &Result : Unroller.verifyObligations(Module)) { + // Every failure is reported, so a copy, or a loop's unwinding, is + // solved in the executions that pass the failing checks before it: + // one that fails an earlier check never reaches it. What holds + // past another check that fails says so. + std::vector Results = + Unroller.verifyObligations(Module, /*ReportedFailures=*/0); + size_t Last = 0; + for (size_t I = 0; I != Results.size(); ++I) + if (Results[I].ObligationType == ObligationKind::Unwinding || + copyOfFailure(Results[I])) + Last = I; + Earlier.clear(); + for (size_t I = 0; I != Last && Earlier.empty(); ++I) + if (Results[I].Status == VerifyStatus::Failed && + Results[I].ObligationType && + Results[I].ObligationType != ObligationKind::Unwinding && + !copyOfFailure(Results[I])) + Earlier = std::string(" (the ") + + obligationKindName(*Results[I].ObligationType) + + " check at " + std::to_string(Results[I].Source.Line) + + ":" + std::to_string(Results[I].Source.Column) + + " fails)"; + for (VerifyResult &Result : Results) { if (Result.ObligationType == ObligationKind::Unwinding) { Unwound &= Result.Status == VerifyStatus::Verified; continue; @@ -3609,16 +3636,27 @@ class Verifier { 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"); + Earlier.empty() + ? "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" + : "no execution fails this check without failing an " + "earlier one first" + + Earlier + + ": those that pass the checks before it end every " + "loop within " + + iterations(Bound) + ", and unrolling proves it there"); return Notes; } } if (Unrolled) Notes.push_back("no execution fails this check within " + - iterations(Opts.ConfirmBound) + " of each loop"); + iterations(Opts.ConfirmBound) + " of each loop" + + (Earlier.empty() + ? std::string() + : " without failing an earlier one first" + + Earlier)); return Notes; }; Passivizer P; @@ -4814,15 +4852,24 @@ class Verifier { Module, *Item, *R.Assignment, LeanModules.Specs, Pending.Why); Run.Refutations.push_back(std::move(Pending)); } - std::string Msg = "verification failed: " + Fn->Name; - if (!R.ObligationId.empty()) - Msg += " [" + R.ObligationId + "]"; - if (!R.Message.empty()) - Msg += " (counterexample: " + R.Message + ")"; - Msg += backendSuffix(R); - Diags.push_back( - {VerifyDiagnostic::Error, Msg, R.Location, Fn->Name, R}); - Diags.back().Notes = failureNotes(*Fn, R); + // The failure, and those after it --max-failures reports, each + // with its counterexample and notes. + auto failure = [&](const VerifyResult &Failure) { + std::string Msg = "verification failed: " + Fn->Name; + if (!Failure.ObligationId.empty()) + Msg += " [" + Failure.ObligationId + "]"; + if (!Failure.Message.empty()) + Msg += " (counterexample: " + Failure.Message + ")"; + Msg += backendSuffix(Failure); + Diags.push_back({VerifyDiagnostic::Error, Msg, Failure.Location, + Fn->Name, Failure}); + Diags.back().Notes = failureNotes(*Fn, Failure); + }; + failure(R); + for (const VerifyResult &More : R.MoreFailures) { + failure(More); + Diags.back().Additional = true; + } } else { const bool FallbackExported = R.Status == VerifyStatus::Unresolved && exportLeanFallback(Module, Fn->Name, R); @@ -6009,7 +6056,7 @@ class Verifier { /// verdict only when it carries one, as the first error of a function the /// verifier does not represent does. static void count(const VerifyDiagnostic &D, VerifySummary &Summary) { - if (D.Axiom) + if (D.Axiom || D.Additional) return; switch (D.K) { case VerifyDiagnostic::Verified: diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h index 4217da5f90..7483d82571 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; + /// How many failing obligations of a function are reported, each with its + /// own counterexample (Z3 only); 0 reports every one. + unsigned MaxFailures = 1; /// Glob patterns over function names: only the functions they match are /// reported. Empty: every function. std::vector FunctionPatterns; From f8bc5315e5f610733e3ef86d8ca63461107a4aa0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:45 +0530 Subject: [PATCH 20/32] verify: Add --max-failures. --- clang/tools/cpp-verify/Main.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index 5a63665c5a..f4e8e94bd3 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::opt MaxFailures( + "max-failures", + cl::desc("Report up to this many failing checks of a function, each with " + "its own counterexample (default 1, 0 = all; --backend=z3)"), + cl::init(1), cl::cat(CppVerifyCategory)); + static cl::list FunctionPatterns( "function", cl::desc("Report only the functions whose names match this glob pattern " @@ -450,6 +456,7 @@ class VerifyConsumer : public ASTConsumer { VOpts.Quiet = Quiet.getValue(); VOpts.Verbose = Verbose.getValue(); VOpts.ListFunctions = ListFunctions.getValue(); + VOpts.MaxFailures = MaxFailures.getValue(); VOpts.FunctionPatterns.assign(FunctionPatterns.begin(), FunctionPatterns.end()); VOpts.ConfirmBound = ConfirmBound.getValue(); @@ -687,6 +694,8 @@ static bool resolveOptions(bool Replay) { (Replay || Backend == "bmc" || Backend == "lean")) Error = "--confirm-bound requires source verification with --backend=z3, " "cvc5, portfolio, or race"; + else if (given(MaxFailures) && (Replay || Backend != "z3")) + Error = "--max-failures requires source verification with --backend=z3"; else if (given(LeanFallbackScope) && LeanFallback.empty()) Error = "--lean-fallback-scope requires --lean-fallback"; else if (given(LeanAutoTimeout) && LeanProject.empty() && From 693c1b0c2089b05d9beb311a599bcdc0ce544651 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:45 +0530 Subject: [PATCH 21/32] test: --max-failures reports each failing check that an execution passing the earlier failures reaches. --- clang/test/Verify/suite/max_failures.cpp | 103 +++++++++++++++++++++++ 1 file changed, 103 insertions(+) create mode 100644 clang/test/Verify/suite/max_failures.cpp diff --git a/clang/test/Verify/suite/max_failures.cpp b/clang/test/Verify/suite/max_failures.cpp new file mode 100644 index 0000000000..ee169ceb8d --- /dev/null +++ b/clang/test/Verify/suite/max_failures.cpp @@ -0,0 +1,103 @@ +// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s --check-prefix=ONE +// RUN: not %cpp-verify --jobs=1 --max-failures=2 %s -- 2>&1 | FileCheck %s --check-prefix=TWO +// RUN: not %cpp-verify --jobs=4 --max-failures=2 %s -- 2>&1 | FileCheck %s --check-prefix=TWO +// RUN: not %cpp-verify --jobs=1 --max-failures=0 %s -- 2>&1 | FileCheck %s --check-prefix=ALL +// RUN: not %cpp-verify --jobs=4 --max-failures=0 %s -- 2>&1 | FileCheck %s --check-prefix=ALL +// RUN: not %cpp-verify --jobs=1 --max-failures=0 --diagnostics-format=json %s -- 2>/dev/null | FileCheck %s --check-prefix=JSON +// RUN: not %cpp-verify --backend=cvc5 --max-failures=2 %s -- 2>&1 | FileCheck %s --check-prefix=OPTION +// +// A function reports the first check that fails, in the order an execution +// meets them; --max-failures=N reports the first N, and 0 every one, each +// with its own counterexample. A check after the first failure is solved in +// the executions that pass the failing checks before it, so its +// counterexample reaches it, and a check that fails only where an earlier +// one does is not reported. The summary still counts functions. + +namespace cv = cppverify; + +int three_bugs(int x, int y) + cv::pre(x < 1000 && y < 1000) + cv::post(cv::result > 0) + cv::post(cv::result < 100) +{ + int q = 10 / y; + int r = x + q; + return r; +} + +int one_bug(int x) + cv::pre(x < 100) + cv::post(cv::result == x) +{ + return x + 1; +} + +// The assertion fails only where the division divides by zero. +int dependent(int x) + cv::pre(x < 100) + cv::post(true) +{ + int q = 100 / x; + cv::check(x != 0); + return q; +} + +// Each failure has its notes: the first holds in every execution, which its +// loop's missing invariant hides, and the second fails at once. +int counted(int n) + cv::pre(n >= 0 && n <= 3) + cv::post(cv::result == n) + cv::post(cv::result == n + 1) +{ + int c = 0; + while (c < n) + cv::decreases(n - c) + { + c = c + 1; + } + return c; +} + +// ONE: max_failures.cpp:23:3: error: verification failed: three_bugs [{{.*}}::division-by-zero@23:3] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = 0{{.*}}) [backend=z3] [reason=counterexample] +// ONE-NEXT: max_failures.cpp:30:23: error: verification failed: one_bug [{{.*}}::postcondition@30:23] +// ONE-NEXT: max_failures.cpp:40:3: error: verification failed: dependent [{{.*}}::division-by-zero@40:3] +// ONE-NEXT: max_failures.cpp:49:23: error: verification failed: counted [{{.*}}::postcondition@49:23] +// ONE-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches +// ONE-NEXT: note: no execution fails this check: every loop ends within 3 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof +// ONE-NEXT: Summary: 4 failed + +// The overflow's counterexample divides by y, which is not zero. +// TWO: max_failures.cpp:23:3: error: verification failed: three_bugs [{{.*}}::division-by-zero@23:3] +// TWO-NEXT: max_failures.cpp:24:3: error: verification failed: three_bugs [{{.*}}::overflow@24:3] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = {{-?[1-9][0-9]*}}) [backend=z3] [reason=counterexample] +// TWO-NEXT: max_failures.cpp:30:23: error: verification failed: one_bug [{{.*}}::postcondition@30:23] +// TWO-NEXT: max_failures.cpp:40:3: error: verification failed: dependent [{{.*}}::division-by-zero@40:3] +// TWO-NEXT: max_failures.cpp:49:23: error: verification failed: counted [{{.*}}::postcondition@49:23] +// TWO-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches +// TWO-NEXT: note: no execution fails this check: every loop ends within 3 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof +// TWO-NEXT: max_failures.cpp:50:23: error: verification failed: counted [{{.*}}::postcondition@50:23] +// TWO-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches +// TWO-NEXT: note: an execution fails this check with no iteration of any loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 0{{.*}}) +// TWO-NEXT: Summary: 4 failed + +// ALL: max_failures.cpp:23:3: error: verification failed: three_bugs [{{.*}}::division-by-zero@23:3] +// ALL-NEXT: max_failures.cpp:24:3: error: verification failed: three_bugs [{{.*}}::overflow@24:3] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = {{-?[1-9][0-9]*}}) +// ALL-NEXT: max_failures.cpp:20:23: error: verification failed: three_bugs [{{.*}}::postcondition@20:23] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = {{-?[1-9][0-9]*}}; +// ALL-NEXT: max_failures.cpp:21:23: error: verification failed: three_bugs [{{.*}}::postcondition@21:23] (counterexample: {{.*}}y [ssa=y_0] [type=i32] = {{-?[1-9][0-9]*}}; +// ALL-NEXT: max_failures.cpp:30:23: error: verification failed: one_bug [{{.*}}::postcondition@30:23] +// ALL-NEXT: max_failures.cpp:40:3: error: verification failed: dependent [{{.*}}::division-by-zero@40:3] +// ALL-NEXT: max_failures.cpp:49:23: error: verification failed: counted [{{.*}}::postcondition@49:23] +// ALL-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches +// ALL-NEXT: note: no execution fails this check: every loop ends within 3 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof +// ALL-NEXT: max_failures.cpp:50:23: error: verification failed: counted [{{.*}}::postcondition@50:23] +// ALL-NEXT: note: the counterexample's state at the loop at 53:3 is any state its invariants allow, not necessarily one an execution reaches +// ALL-NEXT: note: an execution fails this check with no iteration of any loop (counterexample: {{.*}}n [ssa=n_0] [type=i32] = 0{{.*}}) +// ALL-NEXT: Summary: 4 failed + +// JSON-COUNT-4: "function":"three_bugs" +// JSON-NOT: "function":"three_bugs" +// JSON: "function":"one_bug" +// JSON-NEXT: "function":"dependent" +// JSON-COUNT-2: "function":"counted"{{.*}}"notes":[ +// JSON-NOT: "function" + +// OPTION: error: --max-failures requires source verification with --backend=z3 From 9736285ea740b1e45b2d2e988fd9219743c81535 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:49:39 +0530 Subject: [PATCH 22/32] 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 1553fe8794de975ce9f6c40a10af94e94c6a16c1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:45 +0530 Subject: [PATCH 23/32] test: A failure after a loop is confirmed past the checks that fail before it. --- .../suite/inductive_counterexamples.cpp | 40 +++++++++++++++---- 1 file changed, 33 insertions(+), 7 deletions(-) diff --git a/clang/test/Verify/suite/inductive_counterexamples.cpp b/clang/test/Verify/suite/inductive_counterexamples.cpp index 42421b805d..7ce2f26981 100644 --- a/clang/test/Verify/suite/inductive_counterexamples.cpp +++ b/clang/test/Verify/suite/inductive_counterexamples.cpp @@ -123,8 +123,10 @@ int two_checks(int n) return c; } -// 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. +// And those of its kind: the failed check is the overflow of INT_MIN / -1, +// and the division by zero at the same place fails one iteration sooner, in +// every execution that would reach it. A copy is solved in the executions +// that pass the failing checks before it, so none fails the overflow. int two_kinds(int a, int n) cv::pre(n >= 0 && n <= 5) cv::post(true) @@ -141,6 +143,27 @@ int two_kinds(int a, int n) return q; } +// The first division fails at c == k, and the second one iteration sooner +// when m == k - 1: the execution that fails the first within 2 iterations +// divides by zero in the second first. The one shown passes it. +int past_failure(int k, int m, int n) + cv::pre(n >= 0 && n <= 5) + cv::pre((k == 1 && m == 0) || (k == 3 && m == 100)) + cv::post(true) +{ + int c = 0; + int q = 0; + while (c < n) + cv::invariant(0 <= c && c <= n) + cv::decreases(n - c) + { + q = 100 / (k - c); + q = q + 100 / (m - c); + c = c + 1; + } + return q; +} + // A failure on a path that skips the loop has no loop to note. int skipped(int n) cv::pre(n >= 0 && n <= 5) @@ -195,12 +218,15 @@ int count_up_proved(int n) // 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: inductive_counterexamples.cpp:140:7: error: verification failed: two_kinds [{{.*}}::overflow@140:7] +// CHECK-NEXT: note: the counterexample's state at the loop at 136:3 is any state its invariants allow, not necessarily one an execution reaches +// CHECK-NEXT: note: no execution fails this check without failing an earlier one first (the division-by-zero check at 140:7 fails): those that pass the checks before it end every loop within 2 iterations, and unrolling proves it there +// CHECK-NEXT: inductive_counterexamples.cpp:160:7: error: verification failed: past_failure [{{.*}}::division-by-zero@160:7] +// CHECK-NEXT: note: the counterexample's state at the loop at 156: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: {{.*}}k [ssa=k_0] [type=i32] = 3, m [ssa=m_0] [type=i32] = 100{{.*}}) +// CHECK-NEXT: inductive_counterexamples.cpp:170:23: error: verification failed: skipped [{{.*}}::postcondition@170:23] // CHECK-NEXT: Verified: count_up_proved [backend=z3] -// CHECK-NEXT: Summary: 1 verified, 10 failed +// CHECK-NEXT: Summary: 1 verified, 11 failed // Without unrolling, a failure still says where its state comes from. // NONE: error: verification failed: count_up From 08334b1a77ccb406313717baf8eda21e84dccece Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:46 +0530 Subject: [PATCH 24/32] docs: Describe --max-failures. --- website/source/language/tooling.rst | 39 +++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index 070eee43b1..e8e468120c 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -26,6 +26,7 @@ Standalone verifier cpp-verify --profile-quantifiers file.cpp cpp-verify --timeout=20000 file.cpp cpp-verify --confirm-bound=4 file.cpp + cpp-verify --max-failures=0 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 @@ -804,6 +805,44 @@ 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`). +A function reports one failure: the first check that fails, in the order an +execution meets them. ``--max-failures=N`` reports the first ``N``, and +``--max-failures=0`` every one, each with its own counterexample and notes, +as Dafny reports every failing assertion of a method (only with +``--backend=z3``). A check after the first failure is solved in the +executions that pass the failing checks before it, as Boogie assumes an +assertion once it has checked it: its counterexample reaches it without +failing an earlier check, and a check that fails only where an earlier one +fails is not reported, since fixing that one fixes it. The summary still +counts each function once: + +.. cppverify-example: flags --max-failures=0 +.. code-block:: cpp + + namespace cv = cppverify; + + int three_bugs(int x, int y) + cv::pre(x < 1000 && y < 1000) + cv::post(cv::result > 0) + { + int q = 10 / y; + int r = x + q; + return r; + } + +.. code-block:: text + + $ cpp-verify --max-failures=0 three_bugs.cpp + three_bugs.cpp:7:3: error: verification failed: three_bugs [fn_...::division-by-zero@7:3] (counterexample: x [ssa=x_0] [type=i32] = 0, y [ssa=y_0] [type=i32] = 0) [backend=z3] [reason=counterexample] + three_bugs.cpp:8:3: error: verification failed: three_bugs [fn_...::overflow@8:3] (counterexample: q [ssa=q_1] [type=i32] = -1, x [ssa=x_0] [type=i32] = -2147483648, y [ssa=y_0] [type=i32] = -9) [backend=z3] [reason=counterexample] + three_bugs.cpp:5:23: error: verification failed: three_bugs [fn_...::postcondition@5:23] (counterexample: result [ssa=__result_1] [type=i32] = 0, q [ssa=q_1] [type=i32] = 0, r [ssa=r_1] [type=i32] = 0, x [ssa=x_0] [type=i32] = 0, y [ssa=y_0] [type=i32] = 11; trace: return.return@9:3 value=0) [backend=z3] [reason=counterexample] + Summary: 1 failed in 0.0 s + +Without the option only the first line is printed. The overflow's +counterexample divides by ``y = -9``, not by zero, and the postcondition's +returns from an execution with no undefined operation. In JSON each failure +is a record of its own. + 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 657de3f3d068fe99724f674d9a7525a2b1ae5006 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:46 +0530 Subject: [PATCH 25/32] docs: Describe the note on a check that fails only after an earlier one. --- website/source/language/functions-loops.rst | 41 +++++++++++++++++++-- 1 file changed, 38 insertions(+), 3 deletions(-) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index 783e4e62b3..2aabca3f6f 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -673,9 +673,44 @@ Here the loop has no invariant, so after it ``c`` may be anything; the fix is 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 +that no execution fails the check within that many iterations. The execution +a note gives passes the checks before this one that fail, since one that +fails an earlier check never reaches it. When the check holds in every +execution that passes them, the note says so and names an earlier check that +fails, the one to fix first (``--max-failures=0`` reports it with its own +counterexample, see :doc:`tooling`): + +.. code-block:: cpp + + namespace cv = cppverify; + + int divide(int a, int n) + cv::pre(n >= 0 && n <= 5) + cv::post(true) + { + 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; + } + +.. code-block:: text + + divide.cpp:13:7: error: verification failed: divide [fn_...::overflow@13:7] (counterexample: a [ssa=a_0] [type=i32] = -2147483648, c [ssa=c_1] [type=i32] = 0, c [ssa=c_2] [type=i32] = 2, n [ssa=n_0] [type=i32] = 3, q [ssa=q_1] [type=i32] = 0; trace: loop.entry@9:3 -> loop.inductive iteration@9:3 condition=true) [backend=z3] [reason=counterexample] + note: the counterexample's state at the loop at 9:3 is any state its invariants allow, not necessarily one an execution reaches + note: no execution fails this check without failing an earlier one first (the division-by-zero check at 13:7 fails): those that pass the checks before it end every loop within 2 iterations, and unrolling proves it there + +``INT_MIN / -1`` needs ``c == 2``, and every execution that gets there +divides by ``1 - 1`` one iteration sooner. + +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``). From 0dcdef4ff37529d6c19793d124d9f4e83bcbb4c7 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:47 +0530 Subject: [PATCH 26/32] docs: List --max-failures 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 f059a1b3d3..b182e540a9 100644 --- a/website/source/book/part-ii/ch15-toolchain-and-flags.rst +++ b/website/source/book/part-ii/ch15-toolchain-and-flags.rst @@ -51,6 +51,10 @@ Other flags 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 --max-failures=N`` — report the first ``N`` checks of a + function that fail (``0``: every one), each with its own counterexample, + instead of the first only; a check after a failure counts only when an + execution that passes the failing checks before it fails it - ``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 0aa81ecfffde297aa021e7ac1622c1a566dac5d8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:47 +0530 Subject: [PATCH 27/32] docs: Point to --max-failures and the note on an earlier failure in the book. --- .../source/book/part-ii/ch16-when-verification-fails.rst | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) 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 a64919f550..643302f323 100644 --- a/website/source/book/part-ii/ch16-when-verification-fails.rst +++ b/website/source/book/part-ii/ch16-when-verification-fails.rst @@ -62,7 +62,13 @@ is what unrolling the loop found about the same check (``--confirm-bound``, 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. +contract, not in the invariant. When the check fails only in executions that +fail an earlier check first, the note names that check: fix it first. + +A function reports its first failing check. To see every one, each with its +own counterexample, run ``cpp-verify --max-failures=0``: a check after a +failure is reported only when some execution that passes the earlier failing +checks fails it, so each line is a bug of its own. An undecided query is different from a counterexample. ``Unresolved`` with reason ``solver.timeout``, ``solver.resource-limit``, or ``solver.unknown`` From 53091096ab1d48fe1409fcba03d36ef56db45d83 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:47 +0530 Subject: [PATCH 28/32] docs: Note --max-failures in the 0.2.0 release notes. --- website/source/release-notes.rst | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 4dc149b3bc..6bf63e0390 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -490,9 +490,18 @@ 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`). +check (when unrolling proves it) or that none fails it within the bound. The +execution it gives passes the failing checks before this one, and a check +that holds in every execution that passes them is noted with an earlier +check that fails. A failure of a function whose loop has no +``cppverify::decreases`` names that loop too +(:doc:`language/functions-loops`). + +**Every failure of a function.** A function reported only its first failing +check. ``--max-failures=N`` reports the first ``N`` (``0``: every one), each +with its own counterexample and notes; a check after a failure is reported +only when an execution that passes the earlier failing checks fails it, as +Dafny reports every failing assertion (:doc:`language/tooling`). **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 From d480b8ec4fe09b4a9ccae38cddbbd1996d2c3d5d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:48 +0530 Subject: [PATCH 29/32] docs: Design how the failures after the first are reported. --- docs/DESIGN.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index d34d26e88b..608c8e4b9a 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1899,11 +1899,19 @@ int safe_fib(int n) cppverify::pre(...) cppverify::post(cppverify::result == fib 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 + proves the check, or that none fails it within the bound. The execution + passes every failing check before this one, and a check that holds in the + executions that pass them says so and names one that fails. 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. +- Several failures of one function (`--max-failures`): after the first, + a check is a failure only when an execution that passes the failing checks + before it fails it, as Boogie assumes an assertion once checked and Dafny + then reports each failing assertion. Each such failure is a bug of its + own: one that fails only after an earlier failure disappears with its fix, + and is not reported. Checks not settled are not assumed. - 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 75785f812e5f80e3c266f516a6035afac356fab6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:48 +0530 Subject: [PATCH 30/32] docs: Describe how the failures after the first are solved past the earlier ones. --- docs/ARCHITECTURE.md | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 566bfd31b4..369e765434 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -768,7 +768,13 @@ 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 +the next bound; anything unresolved ends the search without a note. Every +failure of the unrolled module is reported, so each copy, and each loop's +unwinding, is solved past the failing obligations before it (see +`--max-failures` below): the execution noted fails no earlier check, and a +copy that holds there, when another check fails before it, is noted as +holding in every execution that does not fail that check first, named by its +kind and place. 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 @@ -2612,6 +2618,24 @@ the whole query had refuted the function in milliseconds: model search over quantified heap queries depends on the solver's search order, and 16 of 40 random seeds took the full 30 s. +With `--max-failures=N` (`BackendExecutionOptions::MaxFailures`, Z3 only) +the obligations report up to `N` failures (0: all), and the result of the +first carries the others (`VerifyResult::MoreFailures`), which the driver +prints after it, each with its notes, as diagnostics marked `Additional` that +the summary does not count. `verifyObligations` given a number of failures to +report solves each obligation after the first failure in the executions that +pass every earlier failing one, as Boogie's subsumption assumes an assertion +after checking it (`verifyPastEarlier`: the obligation's counterexample query +conjoined with those obligations' goals, never cached): alone, its +counterexample could start where an earlier check already fails, and a check +that fails only there would be reported though fixing the earlier one fixes +it. Checks not settled are not assumed, so nothing proved past the failures +rests on a check that may not hold. A serial run stops after the `N`th +failure; a parallel one solves every obligation alone and then solves each +failure after the first again, in order. Without a number, every obligation +is solved alone, as the portfolio's comparison of Z3's and cvc5's results +needs. + The whole query of a module without logic functions is a probe of a fixed amount of work, `WholeProbeUnits` (6 million) Z3 resource units, with the module's timeout as its bound in time, so where it stops depends neither on From 20a8d3f5fd8b799697bdc7855b84238aa148c678 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 06:42:08 +0530 Subject: [PATCH 31/32] 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 32/32] 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