From 038cccfc3f39de35d6a1d3802a0564c44b27291d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 17:24:20 +0530 Subject: [PATCH 01/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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/86] 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 4606ed3303a2dd866ed1a6ba38e407f0cc7799db Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:29 +0530 Subject: [PATCH 29/86] verify: Add BackendTimes, where the backends of one function count their time. --- clang/lib/Verify/Backend/Timing.h | 44 +++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 clang/lib/Verify/Backend/Timing.h diff --git a/clang/lib/Verify/Backend/Timing.h b/clang/lib/Verify/Backend/Timing.h new file mode 100644 index 0000000000..72e2c37b25 --- /dev/null +++ b/clang/lib/Verify/Backend/Timing.h @@ -0,0 +1,44 @@ +//===--- Timing.h - Where a function's verification spends its time -----===// +#ifndef LLVM_CLANG_VERIFY_BACKEND_TIMING_H +#define LLVM_CLANG_VERIFY_BACKEND_TIMING_H + +#include +#include +#include + +namespace clang { +namespace verify { + +/// The time the backends of one function's verification spend, in +/// nanoseconds: solving is the wall time in VerifyBackend::verify, induction +/// the part of it spent on inductions, and certification the time of the +/// counterexample checks, summed over checks that may run at once. +struct BackendTimes { + std::atomic Solving{0}; + std::atomic Induction{0}; + std::atomic Certification{0}; +}; + +/// Adds the time from its construction to its destruction to a counter, if +/// there is one. +class TimeInto { + std::atomic *Counter; + std::chrono::steady_clock::time_point Start; + +public: + explicit TimeInto(std::atomic *Counter) + : Counter(Counter), Start(std::chrono::steady_clock::now()) {} + TimeInto(const TimeInto &) = delete; + TimeInto &operator=(const TimeInto &) = delete; + ~TimeInto() { + if (Counter) + Counter->fetch_add(std::chrono::duration_cast( + std::chrono::steady_clock::now() - Start) + .count()); + } +}; + +} // namespace verify +} // namespace clang + +#endif From ac67bd1a69a9012505da5e09d71c66672e93d3d5 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:29 +0530 Subject: [PATCH 30/86] verify: Count the time of each counterexample check into the limits' time sink. --- clang/lib/Verify/Backend/Certify.cpp | 1 + clang/lib/Verify/Backend/Certify.h | 2 ++ 2 files changed, 3 insertions(+) diff --git a/clang/lib/Verify/Backend/Certify.cpp b/clang/lib/Verify/Backend/Certify.cpp index 9562568603..66a8254347 100644 --- a/clang/lib/Verify/Backend/Certify.cpp +++ b/clang/lib/Verify/Backend/Certify.cpp @@ -3744,6 +3744,7 @@ CertifyResult verify::certifyCounterexample(const ObligationModule &Module, const LogicExpr &Query, CandidateModel &Model, const CertifyLimits &Limits) { + TimeInto Checking(Limits.Times ? &Limits.Times->Certification : nullptr); CertifyResult Result; auto Run = [&] { Evaluator Definitions(Module, Model, Limits, View::Definitions); diff --git a/clang/lib/Verify/Backend/Certify.h b/clang/lib/Verify/Backend/Certify.h index 9c8a95c665..807761b552 100644 --- a/clang/lib/Verify/Backend/Certify.h +++ b/clang/lib/Verify/Backend/Certify.h @@ -154,6 +154,8 @@ struct CertifyLimits { /// Set when Deadline is the time one counterexample check may take, not /// the query's: the message then says so. std::optional CheckTimeoutMs; + /// Where the checks' time is counted, for --time-report. + BackendTimes *Times = nullptr; }; /// A logical application at concrete arguments whose model value differs from From 38aa1fe49360a6199b54c355152c7dd5f80ec0ca Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:30 +0530 Subject: [PATCH 31/86] verify: Count a backend's solving and induction time, and forward its sink to a composite's solvers. --- clang/lib/Verify/Backend/VerifyBackend.cpp | 16 ++++++++++++++++ clang/lib/Verify/Backend/VerifyBackend.h | 7 +++++++ 2 files changed, 23 insertions(+) diff --git a/clang/lib/Verify/Backend/VerifyBackend.cpp b/clang/lib/Verify/Backend/VerifyBackend.cpp index 8a7a52238c..b61a3852be 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.cpp +++ b/clang/lib/Verify/Backend/VerifyBackend.cpp @@ -59,6 +59,10 @@ class BMCVerifyBackend : public VerifyBackend { /*ReuseVerifiedQueries=*/true)), MaxUnrollBound(UnrollBound) {} llvm::StringRef getName() const override { return "bmc"; } + void setTimes(std::shared_ptr T) override { + Z3->setTimes(T); + VerifyBackend::setTimes(std::move(T)); + } std::optional queryTimeoutMs(const ObligationModule &Module) const override { return Z3->queryTimeoutMs(Module); @@ -232,6 +236,11 @@ class PortfolioVerifyBackend : public VerifyBackend { MaxQueryNodes(Execution.MaxQueryNodes) {} llvm::StringRef getName() const override { return "portfolio"; } + void setTimes(std::shared_ptr T) override { + Z3->setTimes(T); + CVC5->setTimes(T); + VerifyBackend::setTimes(std::move(T)); + } std::optional queryTimeoutMs(const ObligationModule &Module) const override { return Z3->queryTimeoutMs(Module); @@ -488,6 +497,7 @@ void verify::requestInterrupt() { InterruptFlag.store(true); } bool verify::interruptRequested() { return InterruptFlag.load(); } VerifyResult VerifyBackend::verify(const ObligationModule &Module) { + TimeInto Solving(Times ? &Times->Solving : nullptr); VerifyResult Result = verifyDirect(Module); if (Module.Attempt != ModuleAttempt::Primary || Result.Status != VerifyStatus::Unresolved || @@ -511,6 +521,7 @@ VerifyResult VerifyBackend::verify(const ObligationModule &Module) { } setDeadline(Until); llvm::scope_exit Restore([&] { setDeadline(Saved); }); + TimeInto Inducting(Times ? &Times->Induction : nullptr); std::vector Tried; for (const InductionScheme &Scheme : inductionSchemes(Module)) { if (Until && std::chrono::steady_clock::now() >= *Until) @@ -678,6 +689,11 @@ class RaceVerifyBackend : public VerifyBackend { MaxQueryNodes(Execution.MaxQueryNodes) {} llvm::StringRef getName() const override { return "race"; } + void setTimes(std::shared_ptr T) override { + Z3->setTimes(T); + CVC5->setTimes(T); + VerifyBackend::setTimes(std::move(T)); + } std::optional queryTimeoutMs(const ObligationModule &Module) const override { return Z3->queryTimeoutMs(Module); diff --git a/clang/lib/Verify/Backend/VerifyBackend.h b/clang/lib/Verify/Backend/VerifyBackend.h index 2c2c8b2396..fe41b6428e 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.h +++ b/clang/lib/Verify/Backend/VerifyBackend.h @@ -3,6 +3,7 @@ #define LLVM_CLANG_VERIFY_BACKEND_VERIFYBACKEND_H #include "Obligation.h" +#include "Timing.h" #include "llvm/ADT/StringRef.h" #include "llvm/Support/ThreadPool.h" #include @@ -212,6 +213,10 @@ class VerifyBackend { FunctionDeadline = D; applyDeadline(D); } + /// Counts the time this backend spends into \p T, for --time-report. + virtual void setTimes(std::shared_ptr T) { + Times = std::move(T); + } /// Stops the work in progress, from any thread: queries running end /// unresolved and no further one starts, until resume(). virtual void cancel() {} @@ -227,9 +232,11 @@ class VerifyBackend { /// Limits the queries that start from now on to \p D. virtual void applyDeadline(std::optional D) {} + BackendTimes *times() const { return Times.get(); } private: std::optional FunctionDeadline; + std::shared_ptr Times; }; /// Race: Z3 and cvc5 at once, the first proof or certified counterexample From d480b8ec4fe09b4a9ccae38cddbbd1996d2c3d5d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:48 +0530 Subject: [PATCH 32/86] 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 c7ea7db908c204863de6273566733c61ab5d5962 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:30 +0530 Subject: [PATCH 33/86] verify: Give each Z3 query, and the passes nested in it, the backend's time sink. --- clang/lib/Verify/Backend/Z3Encode.cpp | 4 ++++ clang/lib/Verify/Backend/Z3Encode.h | 3 +++ 2 files changed, 7 insertions(+) diff --git a/clang/lib/Verify/Backend/Z3Encode.cpp b/clang/lib/Verify/Backend/Z3Encode.cpp index 41e868970c..fd2483b947 100644 --- a/clang/lib/Verify/Backend/Z3Encode.cpp +++ b/clang/lib/Verify/Backend/Z3Encode.cpp @@ -1779,6 +1779,8 @@ void Z3Encoder::resume() { Z3Encoder::PassScope::PassScope(Z3Encoder &Outer, Z3Encoder &Inner) : Outer(Outer) { + // The inner pass's checks are the outer query's. + Inner.Times = Outer.Times; std::lock_guard Guard(Outer.CheckLock); Outer.Pass = &Inner; if (Outer.Stopped) @@ -2230,6 +2232,7 @@ z3::expr Z3Encoder::evaluated(const z3::model &Model, const z3::expr &E, } CertifyLimits Z3Encoder::checkLimits(CertifyLimits Limits) const { + Limits.Times = Times; // One check may not spend the whole query: a slow one leaves time for the // others and for the later stages. const unsigned CapMs = CertifyTimeoutMs ? *CertifyTimeoutMs : TimeoutMs / 2; @@ -3726,6 +3729,7 @@ VerifyResult Z3VerifyBackend::solveQuery( ? std::optional(TimeoutMs / 2) : CertifyTimeoutMs); Encoder.setSearchSlice(Slice); + Encoder.setTimes(times()); Encoder.setIntegerEncoding(IntegerEncoding); Encoder.setProfileQuantifiers(ProfileQuantifiers && Facts); Encoder.setSequenceFacts(Facts); diff --git a/clang/lib/Verify/Backend/Z3Encode.h b/clang/lib/Verify/Backend/Z3Encode.h index 2185f4b88c..f1a12838b0 100644 --- a/clang/lib/Verify/Backend/Z3Encode.h +++ b/clang/lib/Verify/Backend/Z3Encode.h @@ -65,6 +65,7 @@ class Z3Encoder { std::optional TraceEventCount); std::chrono::steady_clock::time_point QueryStart; std::optional CertifyTimeoutMs; + BackendTimes *Times = nullptr; bool SearchSlice = false; bool QuantifiedQuery = false; z3::solver freshSolver(); @@ -290,6 +291,8 @@ class Z3Encoder { void setCertifyTimeoutMs(std::optional Ms) { CertifyTimeoutMs = Ms; } + /// Where the counterexample checks' time is counted. + void setTimes(BackendTimes *T) { Times = T; } /// The timeout is a slice of the query's time, for the search only: a model /// found is checked with the check's own time, not what is left of it. void setSearchSlice(bool Slice) { SearchSlice = Slice; } From 75785f812e5f80e3c266f516a6035afac356fab6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 18:22:48 +0530 Subject: [PATCH 34/86] 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 ec79bc931f48493a29f85248f17734c8888bdd57 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:31 +0530 Subject: [PATCH 35/86] verify: Give cvc5's counterexample checks the backend's time sink. --- clang/lib/Verify/Backend/CVC5Backend.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/lib/Verify/Backend/CVC5Backend.cpp b/clang/lib/Verify/Backend/CVC5Backend.cpp index 859c316d72..0ecff37ad3 100644 --- a/clang/lib/Verify/Backend/CVC5Backend.cpp +++ b/clang/lib/Verify/Backend/CVC5Backend.cpp @@ -2671,6 +2671,7 @@ CVC5VerifyBackend::verifyQuery(const ObligationModule &Module, // One check may not spend the whole query. auto checkLimits = [&] { CertifyLimits Limits; + Limits.Times = times(); Limits.Deadline = QueryDeadline; const unsigned CapMs = CertifyTimeoutMs ? *CertifyTimeoutMs : TimeoutMs / 2; if (CapMs > 0) { From af968e10e1141aa8fb2bb161d3ecd5e6e8231ba0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:31 +0530 Subject: [PATCH 36/86] verify: Report where the run and each function spent their time, and count the functions done on a terminal. --- clang/lib/Verify/Driver/Verifier.cpp | 172 ++++++++++++++++++++++++++- clang/lib/Verify/Driver/Verifier.h | 5 + 2 files changed, 174 insertions(+), 3 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 61d51814b1..d70a8780e6 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -44,6 +44,7 @@ #include "llvm/Support/MathExtras.h" #include "llvm/Support/MemoryBuffer.h" #include "llvm/Support/Path.h" +#include "llvm/Support/Process.h" #include "llvm/Support/Program.h" #include "llvm/Support/SHA256.h" #include "llvm/Support/ThreadPool.h" @@ -1110,6 +1111,12 @@ struct VerifyDiagnostic { bool Additional = false; }; +static uint64_t nanosecondsSince(std::chrono::steady_clock::time_point Start) { + return std::chrono::duration_cast( + std::chrono::steady_clock::now() - Start) + .count(); +} + static std::string backendSuffix(const VerifyResult &Result) { std::string Suffix; if (!Result.BackendName.empty()) { @@ -2801,6 +2808,21 @@ class Verifier { std::vector Diags; /// What --list-functions prints: each function's location and kind. std::vector> Listing; + /// Where the verification of each reported function spent its time, in + /// nanoseconds, and of the run, for --time-report. + struct FunctionTime { + std::string Name; + uint64_t Total = 0; + uint64_t Solving = 0; + uint64_t Induction = 0; + uint64_t Certification = 0; + uint64_t Confirmation = 0; + }; + std::vector Timings; + std::chrono::steady_clock::time_point RunStart = + std::chrono::steady_clock::now(); + std::optional Converted, Verified, + Settled; std::optional Lean; /// Where each template specialization verified is instantiated, and what /// it is, by its function's name. @@ -3169,6 +3191,7 @@ class Verifier { {VerifyDiagnostic::Warning, "no verifiable functions found"}); return true; } + Converted = std::chrono::steady_clock::now(); // 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. @@ -3427,6 +3450,8 @@ class Verifier { const VFunction *Fn; std::string Label; BackendKind Kind; + /// The function whose verification proposed it. + size_t Function; }; std::vector Confirmations; /// Certified failures a fallback project shows in Lean: each one's @@ -3446,6 +3471,13 @@ class Verifier { std::string Archive; /// Ctrl-C came before the verification ended. bool Interrupted = false; + /// Where the verification spent its time (--time-report), in + /// nanoseconds: the task, its backends, the notes of its failures, + /// and the confirmations by proof after every task. + std::shared_ptr Times; + uint64_t Task = 0; + uint64_t Notes = 0; + uint64_t Confirmed = 0; }; std::vector Runs(Functions.size()); // The source manager caches its last line lookup. @@ -3473,7 +3505,7 @@ class Verifier { Run.Confirmations.push_back({Diags.size(), std::make_shared( copyObligationModule(Checked)), - R, &In, Label, Kind}); + R, &In, Label, Kind, Index}); explainUnsettled(R, In, Checked); }; llvm::raw_string_ostream DumpStream(Run.Dump); @@ -3505,6 +3537,13 @@ class Verifier { } auto SmokeBackend = createVerifyBackend(BackendKind::Z3, nullptr, 0, SmokeExecution, nullptr); + if (Opts.TimeReport) { + Run.Times = std::make_shared(); + Backend->setTimes(Run.Times); + if (OwnSpecBackend) + OwnSpecBackend->setTimes(Run.Times); + SmokeBackend->setTimes(Run.Times); + } // 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 @@ -3537,6 +3576,9 @@ class Verifier { "execution reaches"); if (Opts.ConfirmBound == 0 || !Failure.ObligationType) return Notes; + const auto UnrollStart = std::chrono::steady_clock::now(); + llvm::scope_exit CountUnrolling( + [&] { Run.Notes += nanosecondsSince(UnrollStart); }); VFunction Bounded = cloneVFunction(F); annotatePointerOrigins(Bounded); if (Opts.CheckUB && !F.TotalExpressions && instrumentUBChecks(Bounded)) @@ -4907,15 +4949,34 @@ class Verifier { for (size_t I = 0; I != Functions.size(); ++I) if (Scheduled[I]) Batch.push_back(I); + // On a terminal, a line on standard error says how many functions are + // done; the results follow once every verdict is settled. + const bool ShowProgress = + Opts.Progress.value_or(llvm::sys::Process::StandardErrIsDisplayed()) && + Opts.Diagnostics != DiagnosticFormat::Json; + std::mutex ProgressLock; + size_t Done = 0; + size_t Queued = Batch.size(); + auto runFunction = [&](size_t I) { + const auto Start = std::chrono::steady_clock::now(); + verifyFunction(I); + Runs[I].Task = nanosecondsSince(Start); + if (!ShowProgress) + return; + std::lock_guard Lock(ProgressLock); + llvm::errs() << "\r\x1b[K[" << ++Done << "/" << Queued << "] " + << Functions[I]->Name; + llvm::errs().flush(); + }; while (!Batch.empty()) { if (Parallel) { TaskGroup Group(*Pool); for (size_t I : Batch) - Group.async([&verifyFunction, I] { verifyFunction(I); }); + Group.async([&runFunction, I] { runFunction(I); }); Group.wait(); } else { for (size_t I : Batch) - verifyFunction(I); + runFunction(I); } std::vector Next; auto need = [&](const std::string &Identity) { @@ -4935,7 +4996,32 @@ class Verifier { } llvm::sort(Next); Batch = std::move(Next); + Queued += Batch.size(); } + if (ShowProgress && Done != 0) + llvm::errs() << "\r\x1b[K"; + Verified = std::chrono::steady_clock::now(); + // The report lists the functions reported, as a run of the whole file + // would, with the time of the confirmations below. + llvm::scope_exit ReportTimes([&] { + if (!Opts.TimeReport) + return; + for (size_t I = 0; I != Functions.size(); ++I) { + const FunctionRun &Run = Runs[I]; + const VFunction &Fn = *Functions[I]; + if (!Scheduled[I] || !Selected[I] || !Run.Times || Fn.IsBuiltin || + Fn.IsChoice) + continue; + FunctionTime Time; + Time.Name = Fn.Name; + Time.Total = Run.Task + Run.Confirmed; + Time.Solving = Run.Times->Solving; + Time.Induction = Run.Times->Induction; + Time.Certification = Run.Times->Certification; + Time.Confirmation = Run.Notes + Run.Confirmed; + Timings.push_back(std::move(Time)); + } + }); // A function whose verification Ctrl-C cut short is reported by one // line. Its verdicts stay, hidden, for what they establish: a query the // interrupt stopped left its verdict unresolved, and a proof found @@ -5579,6 +5665,7 @@ class Verifier { Lemmas.emplace(Functions[I]->Identity, Runs[I].Contract); std::vector> Outcomes(Confirmations.size()); std::vector CutShort(Confirmations.size()); + std::vector ConfirmationTimes(Confirmations.size()); auto confirm = [&](size_t I) { const FunctionRun::Confirmation &Pending = Confirmations[I]; const VerifyDiagnostic &Verdict = Diags[Pending.Index]; @@ -5601,10 +5688,12 @@ class Verifier { CutShort[I] = true; return; } + const auto Start = std::chrono::steady_clock::now(); std::unique_ptr By = createVerifyBackend( Pending.Kind, nullptr, Opts.BMCUnroll, Execution, nullptr); Outcomes[I] = confirmCounterexample( Checked, Pending.Result, InterfaceMap, *Pending.Fn, Lemmas, *By); + ConfirmationTimes[I] = nanosecondsSince(Start); CutShort[I] = !Outcomes[I] && interruptRequested(); }; if (Parallel) { @@ -5616,6 +5705,8 @@ class Verifier { for (size_t I = 0; I != Confirmations.size(); ++I) confirm(I); } + for (size_t I = 0; I != Confirmations.size(); ++I) + Runs[Confirmations[I].Function].Confirmed += ConfirmationTimes[I]; for (size_t I = 0; I != Confirmations.size(); ++I) { if (CutShort[I]) { VerifyDiagnostic &Verdict = Diags[Confirmations[I].Index]; @@ -6095,6 +6186,78 @@ class Verifier { } } + /// The time the run took to settle the verdicts after verifying. + void settled() { Settled = std::chrono::steady_clock::now(); } + + /// Where the run spent its time: converting, verifying the functions (at + /// once, with several jobs), and settling the verdicts; and each reported + /// function, the busiest first. A function's solving includes its + /// inductions and certification; certification is summed over checks that + /// may run at once. + void printTimeReport(llvm::raw_ostream &OS) const { + if (!Converted || !Verified || !Settled) + return; + auto seconds = [](uint64_t Nanoseconds) { + return static_cast(Nanoseconds) / 1e9; + }; + auto between = [&](std::chrono::steady_clock::time_point From, + std::chrono::steady_clock::time_point To) { + return seconds( + std::chrono::duration_cast(To - From) + .count()); + }; + std::vector Busiest; + for (const FunctionTime &Time : Timings) + Busiest.push_back(&Time); + llvm::stable_sort(Busiest, + [](const FunctionTime *A, const FunctionTime *B) { + return A->Total > B->Total; + }); + auto lowering = [](const FunctionTime &Time) { + const uint64_t Rest = Time.Solving + Time.Confirmation; + return Time.Total > Rest ? Time.Total - Rest : 0; + }; + if (Opts.Diagnostics == DiagnosticFormat::Json) { + llvm::json::Object Run; + Run["schema"] = "cppverify.time/1"; + Run["seconds"] = + llvm::json::Object{{"conversion", between(RunStart, *Converted)}, + {"verification", between(*Converted, *Verified)}, + {"settling", between(*Verified, *Settled)}}; + OS << llvm::json::Value(std::move(Run)) << "\n"; + for (const FunctionTime *Time : Busiest) { + llvm::json::Object Record; + Record["schema"] = "cppverify.time/1"; + Record["function"] = Time->Name; + Record["seconds"] = + llvm::json::Object{{"total", seconds(Time->Total)}, + {"lowering", seconds(lowering(*Time))}, + {"solving", seconds(Time->Solving)}, + {"induction", seconds(Time->Induction)}, + {"certification", seconds(Time->Certification)}, + {"confirmation", seconds(Time->Confirmation)}}; + OS << llvm::json::Value(std::move(Record)) << "\n"; + } + return; + } + OS << llvm::formatv("Time report (seconds): conversion {0:F3}, " + "verification {1:F3}, settling {2:F3}\n", + between(RunStart, *Converted), + between(*Converted, *Verified), + between(*Verified, *Settled)); + if (Busiest.empty()) + return; + OS << " total lowering solving induction certification " + "confirmation function\n"; + for (const FunctionTime *Time : Busiest) + OS << llvm::formatv("{0,10:F3}{1,10:F3}{2,10:F3}{3,11:F3}{4,15:F3}" + "{5,14:F3} {6}\n", + seconds(Time->Total), seconds(lowering(*Time)), + seconds(Time->Solving), seconds(Time->Induction), + seconds(Time->Certification), + seconds(Time->Confirmation), Time->Name); + } + void printDiagnostics(llvm::raw_ostream &OS) const { for (const auto &[Loc, Line] : Listing) { PresumedLoc PLoc = Ctx.getSourceManager().getPresumedLoc(Loc); @@ -6215,7 +6378,10 @@ bool verify::verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS, const VerifyOptions &Opts) { Verifier V(Ctx, Opts, OS); bool Ok = V.run(); + V.settled(); V.printDiagnostics(OS); + if (Opts.TimeReport) + V.printTimeReport(OS); return Ok; } diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h index 7483d82571..91670b5bc8 100644 --- a/clang/lib/Verify/Driver/Verifier.h +++ b/clang/lib/Verify/Driver/Verifier.h @@ -109,6 +109,11 @@ struct VerifyOptions { bool Verbose = false; /// List the functions the run would verify, and verify none. bool ListFunctions = false; + /// Report where each function's verification spent its time. + bool TimeReport = false; + /// Show which functions are done on standard error as they finish; unset, + /// when standard error is a terminal. + std::optional Progress; /// How many failing obligations of a function are reported, each with its /// own counterexample (Z3 only); 0 reports every one. unsigned MaxFailures = 1; From 382bb840f22b6d612f17961dd8694fbf3f61b3c4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:31 +0530 Subject: [PATCH 37/86] verify: Add --time-report and --progress. --- clang/tools/cpp-verify/Main.cpp | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index f4e8e94bd3..a43fc8cd71 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -303,6 +303,18 @@ static cl::opt ListFunctions( "locations, and verify none"), cl::cat(CppVerifyCategory)); +static cl::opt TimeReport( + "time-report", + cl::desc("Report where the run and each function spent their time: " + "lowering, solving, induction, certification, confirmation"), + cl::cat(CppVerifyCategory)); + +static cl::opt Progress( + "progress", + cl::desc("Show on standard error how many functions are done (default: " + "when standard error is a terminal)"), + cl::cat(CppVerifyCategory)); + namespace { static int gVerifyFailures = 0; @@ -456,6 +468,9 @@ class VerifyConsumer : public ASTConsumer { VOpts.Quiet = Quiet.getValue(); VOpts.Verbose = Verbose.getValue(); VOpts.ListFunctions = ListFunctions.getValue(); + VOpts.TimeReport = TimeReport.getValue(); + if (Progress != cl::boolOrDefault::BOU_UNSET) + VOpts.Progress = Progress == cl::boolOrDefault::BOU_TRUE; VOpts.MaxFailures = MaxFailures.getValue(); VOpts.FunctionPatterns.assign(FunctionPatterns.begin(), FunctionPatterns.end()); @@ -717,6 +732,8 @@ static bool resolveOptions(bool Replay) { else if ((given(CheckUB) || given(NoCheckUB)) && Replay) Error = "--check-ub and --no-check-ub apply to source verification; an " "archive keeps the checks it was written with"; + else if (given(TimeReport) && Replay) + Error = "--time-report requires source verification"; if (Error.empty()) return true; llvm::errs() << "error: " << Error << "\n"; From 6b09406a29cdc21b15ee4f8d60aa24561ab111aa Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:32 +0530 Subject: [PATCH 38/86] test: Add a checker of which phases of a time report took time. --- .../Verify/suite/Inputs/time_report_phases.py | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/time_report_phases.py diff --git a/clang/test/Verify/suite/Inputs/time_report_phases.py b/clang/test/Verify/suite/Inputs/time_report_phases.py new file mode 100644 index 0000000000..57d2ecf311 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/time_report_phases.py @@ -0,0 +1,29 @@ +"""Reads the JSON Lines of a run with --time-report and prints, for each +function, which phases took any time, and whether its times add up: the +total is lowering, solving, and confirmation; induction is part of solving; +and with one job, so is certification. Then whether the functions come +busiest first.""" +import json +import sys + +totals = [] +for line in sys.stdin: + record = json.loads(line) + if record.get("schema") != "cppverify.time/1": + continue + seconds = record["seconds"] + if "function" not in record: + print("run " + " ".join(sorted(seconds))) + continue + totals.append(seconds["total"]) + parts = seconds["lowering"] + seconds["solving"] + seconds["confirmation"] + adds_up = (abs(seconds["total"] - parts) < 1e-6 and + seconds["lowering"] >= 0 and + seconds["induction"] <= seconds["solving"] and + seconds["certification"] <= seconds["solving"]) + print("%s solving=%d induction=%d certification=%d confirmation=%d %s" % ( + record["function"], seconds["solving"] > 0, seconds["induction"] > 0, + seconds["certification"] > 0, seconds["confirmation"] > 0, + "adds up" if adds_up else "does not add up: %r" % seconds)) +print("busiest first" if totals == sorted(totals, reverse=True) + else "not busiest first: %r" % totals) From 5ad39064f61920ca6f30ea193bcfc14f48a8f06a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:32 +0530 Subject: [PATCH 39/86] test: Add a failing function and a recursive spec for the time report's backend runs. --- .../test/Verify/suite/Inputs/time_report_wrong.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/time_report_wrong.cpp diff --git a/clang/test/Verify/suite/Inputs/time_report_wrong.cpp b/clang/test/Verify/suite/Inputs/time_report_wrong.cpp new file mode 100644 index 0000000000..eb9a22cb46 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/time_report_wrong.cpp @@ -0,0 +1,14 @@ +namespace cv = cppverify; + +int wrong(int x) + cv::pre(x < 100) + cv::post(cv::result == x) +{ + return x + 1; +} + +cv::spec int count(int n) + cv::decreases(n) +{ + return n <= 0 ? 0 : count(n - 1) + 1; +} From 43c059e4c68034a03f69c9fffcb494583ae4e220 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:33 +0530 Subject: [PATCH 40/86] test: --time-report shows the phases that took time, with times that add up, the busiest function first. --- clang/test/Verify/suite/time_report.cpp | 104 ++++++++++++++++++++++++ 1 file changed, 104 insertions(+) create mode 100644 clang/test/Verify/suite/time_report.cpp diff --git a/clang/test/Verify/suite/time_report.cpp b/clang/test/Verify/suite/time_report.cpp new file mode 100644 index 0000000000..b1f4ff7847 --- /dev/null +++ b/clang/test/Verify/suite/time_report.cpp @@ -0,0 +1,104 @@ +// RUN: not %cpp-verify --jobs=1 --timeout=1000 --time-report %s -- 2>&1 | FileCheck %s --check-prefix=TEXT +// RUN: not %cpp-verify --jobs=1 --timeout=1000 --time-report --diagnostics-format=json %s -- 2>/dev/null \ +// RUN: | %python %S/Inputs/time_report_phases.py | FileCheck %s --check-prefix=PHASES +// RUN: not %cpp-verify --backend=bmc --time-report --diagnostics-format=json %S/Inputs/time_report_wrong.cpp -- 2>/dev/null \ +// RUN: | %python %S/Inputs/time_report_phases.py | FileCheck %s --check-prefix=BMC +// RUN: %cpp-verify --jobs=1 --time-report --function=proved %s -- 2>&1 | FileCheck %s --check-prefix=FILTER --implicit-check-not=after_loop --implicit-check-not=fibo +// RUN: not %cpp-verify --jobs=1 --timeout=1000 --progress %s -- 2>&1 >/dev/null | FileCheck %s --check-prefix=PROGRESS +// RUN: not %cpp-verify --jobs=1 --timeout=1000 %s -- 2>&1 >/dev/null | count 0 +// RUN: not %cpp-verify --obligation-in=%t.none --time-report 2>&1 | FileCheck %s --check-prefix=REPLAY +// +// --time-report says where a run and each function spent their time: the +// lowering, the solving (with the inductions and the counterexample checks +// within it), and the confirmations after a failure, the busiest function +// first. --progress counts the functions done on standard error, which is +// the default only on a terminal. + +namespace cv = cppverify; + +// Solved, with no induction and nothing to confirm. +int proved(int x) + cv::pre(x < 100) + cv::post(cv::result == x + 1) +{ + return x + 1; +} + +// Its failure passes through the loop, which unrolling confirms. +int after_loop(int n) + cv::pre(n >= 0 && n <= 3) + cv::post(cv::result == n) +{ + int c = 0; + while (c < n) + cv::decreases(n - c) + { + c = c + 1; + } + return c; +} + +cv::spec int fibo(int n) + cv::decreases(n) + cv::post(cv::result >= 0) +{ + if (n <= 0) return 0; + if (n == 1) return 1; + return fibo(n - 2) + fibo(n - 1); +} + +// Proved by induction. +cv::proof void grows(int n) + cv::pre(n >= 3) + cv::post(fibo(n) >= n - 1) +{ +} + +cv::spec int pow2(int n) + cv::decreases(n) + cv::post(cv::result >= n + 1) +{ + return n <= 0 ? 1 : 2 * pow2(n - 1); +} + +// Inductions are tried, and the counterexample is confirmed by a proof +// after every function is verified. +cv::proof void small_power(int n) + cv::pre(n >= 1000000000) + cv::post(pow2(n) < 1000) +{ +} + +// TEXT: Time report (seconds): conversion {{[0-9]+\.[0-9][0-9][0-9]}}, verification {{[0-9]+\.[0-9][0-9][0-9]}}, settling {{[0-9]+\.[0-9][0-9][0-9]}} +// TEXT-NEXT: {{^}} total lowering solving induction certification confirmation function{{$}} +// TEXT-DAG: {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}} proved{{$}} +// TEXT-DAG: {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}} after_loop{{$}} +// TEXT-DAG: {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}} fibo{{$}} +// TEXT-DAG: {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}} grows{{$}} +// TEXT-DAG: {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}} pow2{{$}} +// TEXT-DAG: {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}} small_power{{$}} +// TEXT: Summary: 4 verified, 2 failed + +// Which phases took time, and that the times add up. +// PHASES: run conversion settling verification +// PHASES-DAG: proved solving=1 induction=0 certification=1 confirmation=0 adds up +// PHASES-DAG: after_loop solving=1 induction=0 certification=1 confirmation=1 adds up +// PHASES-DAG: grows solving=1 induction=1 certification=1 confirmation=0 adds up +// PHASES-DAG: small_power solving=1 induction=1 certification=1 confirmation=1 adds up +// PHASES-DAG: fibo solving=1 induction=0 certification=0 confirmation=0 adds up +// PHASES: {{^}}busiest first{{$}} + +// Under BMC too; a failure without a loop has nothing to confirm. +// BMC-DAG: wrong solving=1 induction=0 certification=1 confirmation=0 adds up +// BMC-DAG: count solving=1 induction=0 certification=0 confirmation=0 adds up + +// Only the functions reported are listed. +// FILTER: Verified: proved +// FILTER-NEXT: Time report (seconds): +// FILTER-NEXT: total +// FILTER-NEXT: {{^ +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9] +[0-9]+\.[0-9][0-9][0-9]}} proved{{$}} +// FILTER-NEXT: Summary: 1 verified + +// PROGRESS: [1/6] proved{{.*}}[2/6] after_loop{{.*}}[6/6] small_power + +// REPLAY: error: --time-report requires source verification From 8334673a17774b7299571503875ccecc54738b92 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:33 +0530 Subject: [PATCH 41/86] test: Every backend counts its counterexample checks for --time-report. --- clang/test/Verify/suite/time_report_backends.test | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 clang/test/Verify/suite/time_report_backends.test diff --git a/clang/test/Verify/suite/time_report_backends.test b/clang/test/Verify/suite/time_report_backends.test new file mode 100644 index 0000000000..cc2582c551 --- /dev/null +++ b/clang/test/Verify/suite/time_report_backends.test @@ -0,0 +1,10 @@ +# REQUIRES: cvc5 +# The solvers of every backend count their counterexample checks for +# --time-report, through a portfolio's and a race's components too. +# RUN: not %cpp-verify --backend=cvc5 --time-report --diagnostics-format=json %S/Inputs/time_report_wrong.cpp -- 2>/dev/null \ +# RUN: | %python %S/Inputs/time_report_phases.py | FileCheck %s +# RUN: not %cpp-verify --backend=portfolio --time-report --diagnostics-format=json %S/Inputs/time_report_wrong.cpp -- 2>/dev/null \ +# RUN: | %python %S/Inputs/time_report_phases.py | FileCheck %s +# RUN: not %cpp-verify --backend=race --time-report --diagnostics-format=json %S/Inputs/time_report_wrong.cpp -- 2>/dev/null \ +# RUN: | %python %S/Inputs/time_report_phases.py | FileCheck %s +# CHECK: wrong solving=1 induction=0 certification=1 confirmation=0 adds up From 9bbfb8557d2187fd5c45a2872a225d592170fb99 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:33 +0530 Subject: [PATCH 42/86] docs: Describe --time-report and the progress line. --- website/source/language/tooling.rst | 56 +++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index e8e468120c..9b49b4be69 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -12,6 +12,7 @@ Standalone verifier cpp-verify --verbose file.cpp cpp-verify --list-functions file.cpp cpp-verify --function='parse_*' --function=encode file.cpp + cpp-verify --time-report file.cpp cpp-verify file.cpp -- -I include -DNDEBUG cpp-verify --backend=z3 file.cpp cpp-verify --backend=cvc5 file.cpp @@ -231,6 +232,61 @@ 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. +``--time-report`` adds, after a file's verdicts, where its run spent its time, +then each function it reported, the busiest first. Here ``small_power``'s +counterexample is confirmed by a proof after inductions are tried, ``grows`` +is proved by induction, and ``after_loop`` fails after a loop that +unrolling then checks: + +.. code-block:: text + + $ cpp-verify --time-report file.cpp + ... + Time report (seconds): conversion 0.001, verification 4.412, settling 0.151 + total lowering solving induction certification confirmation function + 4.559 0.001 4.408 3.917 7.577 0.150 small_power + 1.767 0.001 1.766 0.014 3.292 0.000 grows + 0.062 0.002 0.022 0.000 0.000 0.038 after_loop + 0.027 0.001 0.026 0.000 0.000 0.000 fibo + 0.026 0.001 0.025 0.000 0.000 0.000 proved + 0.022 0.001 0.021 0.000 0.000 0.000 pow2 + Summary: 4 verified, 2 failed in 4.6 s + +For the run: + +- **conversion**: from the parsed file to the functions the verifier + verifies (Clang's parsing comes before it; the summary's time covers it); +- **verification**: verifying every function, at once with several jobs; +- **settling**: what follows: the verdicts that rest on other functions' + contracts and on spec facts, confirmations by proof, Lean certification. + +For a function: + +- **total**: its verification, and the confirmations of its counterexamples + by proof that run after every function is verified; +- **lowering**: preparing its checks, and passivizing and lowering them to + obligations; +- **solving**: in the backends: encoding, solving, checking counterexamples, + inductions, and a proof's vacuity checks; +- **induction**: the part of solving spent on automatic inductions; +- **certification**: checking the solvers' counterexamples against the true + definitions, summed over the checks; with several jobs they run at once, + so it can exceed solving; +- **confirmation**: unrolling the loops after a failure (``--confirm-bound``) + and confirming a counterexample by proof. + +A function's total is its lowering, solving, and confirmation. With +``--diagnostics-format=json`` the report is records of the schema +``cppverify.time/1``: one for the run, whose ``seconds`` has +``conversion``, ``verification``, and ``settling``, then one per function, +with ``function`` and the six ``seconds`` of its row. The report needs source +verification (not ``--obligation-in``). + +On a terminal, a line on standard error counts the functions done as they +finish (``[12/40] parse_header``); the results follow once every verdict is +settled. ``--progress`` shows the line anywhere, and ``--progress=false`` +hides it. + ``cpp-verify --help`` shows each time limit's default (``--timeout``, 30000 ms). From 4e619c11ebb62618d823eea93ccdc2dcad4ae1eb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:34 +0530 Subject: [PATCH 43/86] docs: List --time-report 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 b182e540a9..0117644477 100644 --- a/website/source/book/part-ii/ch15-toolchain-and-flags.rst +++ b/website/source/book/part-ii/ch15-toolchain-and-flags.rst @@ -47,6 +47,10 @@ Other flags - ``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 --time-report`` — after the verdicts, where the run and each + function spent their time (lowering, solving, induction, certification, + confirmation), the busiest function first; on a terminal a progress line + counts the functions done (``--progress`` shows it anywhere) - ``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 5fba9a6b51abb6190263977f1c73b5c808844b63 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:34 +0530 Subject: [PATCH 44/86] docs: Note --time-report and the progress line 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 6bf63e0390..e5c28d72fc 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -509,7 +509,9 @@ 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, ``--function=PATTERN`` reports only the functions a glob pattern matches, -with the verdicts a whole run gives, and +with the verdicts a whole run gives, ``--time-report`` says where the run and +each function spent their time, a line on a terminal counts the functions +done, 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 bd27ee07f5f87c95b68c62b7b85efd92f8ca4cab Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:10:34 +0530 Subject: [PATCH 45/86] docs: Describe what --time-report measures where. --- docs/ARCHITECTURE.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 369e765434..6651545b35 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -2423,6 +2423,19 @@ selected stay, hidden, for what they establish. A text run ends with a summary l 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. +`--time-report` measures where that time goes. Each function's task gives +its backends one `BackendTimes` (`Backend/Timing.h`, `VerifyBackend::setTimes`, +which a portfolio, a race, and BMC forward to their solvers): the wall time +in `VerifyBackend::verify` is solving and its induction loop induction, and +`certifyCounterexample` adds each check's time through `CertifyLimits::Times` +(summed, so with several jobs it may exceed solving). The driver times the +task, the unrolling of `failureNotes`, and each confirmation by proof (added +to the function that proposed it, `Confirmation::Function`); lowering is the +task's time outside the backends and the unrolling. The run's conversion, +verification, and settling are the times between `Verifier`'s construction, +the converted functions, the end of the tasks, and the report. Backends +without a sink (the unroller, those of the confirmations by proof and of the +`cppverify::recommends` pass) count nothing, so no time is counted twice. Its message names the construct as C++ does (`unsupportedConstruct` for the statements and expressions without a site of their own; Clang's class name only in parentheses for those it has no name for), and each error is raised From 9eb28c3ecf62d4f62dac486e2d3f694f3bb4fb72 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:59:41 +0530 Subject: [PATCH 46/86] verify: Verify a definition whose trusted mark it only inherits from a declaration. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index f4a41723d3..10b013a2b4 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -3271,10 +3271,20 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { } Fn->ReadsHeap = FCI->IsSpec && specReadsHeap(FD); Fn->DeclLoc = FD->getLocation(); - Fn->IsTrusted = llvm::any_of(FD->redecls(), [](const FunctionDecl *D) { - return D->hasAttr(); - }); - if (Fn->IsTrusted && Fn->IsSpec) { + // [[cppverify::trusted]] on a definition leaves its body unverified; on a + // declaration it says that callers which see no definition assume the + // contract, so a definition that only inherits it is verified. + const bool AnyTrusted = + llvm::any_of(FD->redecls(), [](const FunctionDecl *D) { + return D->hasAttr(); + }); + if (const FunctionDecl *Definition = FD->getDefinition()) { + const auto *Trusted = Definition->getAttr(); + Fn->IsTrusted = Trusted && !Trusted->isInherited(); + } else { + Fn->IsTrusted = AnyTrusted; + } + if (AnyTrusted && Fn->IsSpec) { error(Fn->Name + ": [[cppverify::trusted]] does not apply to a " "spec function, whose definition is its " "meaning"); From f563bca25822ff254c223c625dbb2e25371dc7f3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 19:59:41 +0530 Subject: [PATCH 47/86] test: A trusted declaration's definition is verified, and a trusted definition is not. --- .../Verify/suite/trusted_declarations.cpp | 59 +++++++++++++++++++ 1 file changed, 59 insertions(+) create mode 100644 clang/test/Verify/suite/trusted_declarations.cpp diff --git a/clang/test/Verify/suite/trusted_declarations.cpp b/clang/test/Verify/suite/trusted_declarations.cpp new file mode 100644 index 0000000000..8440c5a3ce --- /dev/null +++ b/clang/test/Verify/suite/trusted_declarations.cpp @@ -0,0 +1,59 @@ +// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s +// RUN: not %cpp-verify --jobs=1 %s -- -DSPEC 2>&1 | FileCheck %s --check-prefix=SPEC +// +// [[cppverify::trusted]] on a declaration says that callers which see no +// definition assume the contract. A definition that only inherits the mark +// from such a declaration is verified, so a wrong body is found; on a +// definition itself, the mark leaves the body unverified. + +namespace cv = cppverify; + +// As a header declares it. +[[cppverify::trusted]] int clamp100(int x) + cv::post(cv::result >= 0 && cv::result <= 100); + +int clamp100(int x) +{ + if (x < 0) + return 0; + if (x > 100) + return 101; + return x; +} + +int scaled(int x) + cv::post(cv::result >= 0 && cv::result <= 200) +{ + return 2 * clamp100(x); +} + +[[cppverify::trusted]] int halved(int x) + cv::pre(x >= 0) + cv::post(cv::result >= 0) +{ + return x - 1; +} + +[[cppverify::trusted]] int above(int x) + cv::post(cv::result > x); + +int uses_above(int x) + cv::pre(x < 100) + cv::post(cv::result > x) +{ + return above(x); +} + +// CHECK: trusted_declarations.cpp:13:28: error: verification failed: clamp100 [{{.*}}::postcondition@13:28] (counterexample: {{.*}}result [ssa={{.*}}] [type=i32] = 101 +// CHECK: Unresolved: scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which is not established) +// CHECK: Trusted: halved (contract assumed, not verified) +// CHECK: Trusted: above (contract assumed, not verified) +// CHECK: Verified: uses_above [backend=z3] [trusts=above] + +// A spec cannot be trusted, on any of its declarations. +#ifdef SPEC +[[cppverify::trusted]] cv::spec int twice(int x); + +cv::spec int twice(int x) { return 2 * x; } +#endif +// SPEC: error: twice: {{\[\[cppverify::trusted\]\]}} does not apply to a spec function, whose definition is its meaning From 87e2def98bcf33e04f67e726df839d8a1e2b25f4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:19 +0530 Subject: [PATCH 48/86] verify: Record each contracted function's contract as written. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 33 ++++++++++++++++++++++ clang/lib/Verify/Frontend/ASTConverter.h | 8 ++++++ 2 files changed, 41 insertions(+) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 10b013a2b4..7da19f9b3e 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -977,6 +977,38 @@ static std::string functionName(const FunctionDecl *FD, return Name; } +std::string ASTConverter::contractText(const FunctionContractInfo &FCI) const { + std::string Text; + llvm::raw_string_ostream OS(Text); + const PrintingPolicy Policy(Ctx.getLangOpts()); + auto clause = [&](llvm::StringRef Kind, const Expr *E) { + OS << Kind << '('; + if (E) + E->printPretty(OS, nullptr, Policy); + OS << ')'; + }; + for (const Expr *Pre : FCI.Preconditions) + clause("pre", Pre); + for (const Expr *Post : FCI.Postconditions) + clause("post", Post); + for (const Expr *Footprint : FCI.Modifies) + clause("modifies", Footprint); + for (const auto &[First, Second] : FCI.Aliases) { + clause("aliases", First); + clause("with", Second); + } + for (const Expr *Measure : FCI.Decreases) + clause("decreases", Measure); + if (FCI.MayDiverge.isValid()) + OS << "decreases(*)"; + for (const auto &[Name, Assumes] : FCI.Behaviors) + clause(std::string("behavior ") + (Name ? Name->getName().str() : ""), + Assumes); + for (const Expr *Check : FCI.BehaviorChecks) + clause("behaviors", Check); + return Text; +} + std::string ASTConverter::functionIdentity(const FunctionDecl *FD) { if (!FD) return {}; @@ -3263,6 +3295,7 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { Fn->IsConstructor = Constructor != nullptr; Fn->Name = functionName(FD, /*Qualified=*/Method != nullptr); Fn->Identity = functionIdentity(FD); + ContractTexts[Fn->Identity] = contractText(*FCI); Fn->IsSpec = FCI->IsSpec; Fn->IsProof = FCI->IsProof; if (FCI->MayDiverge.isValid() && !FCI->IsSpec && !FCI->IsProof) { diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index d83dc0a171..dfc350c871 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -93,6 +93,7 @@ class ASTConverter { void nameParameters(const FunctionDecl *ContractDecl, const FunctionDecl *FD); unsigned BoundValueId = 0; std::map FunctionIdentities; + std::map ContractTexts; std::map SpecHeapReads; /// Uncontracted constexpr functions the lowered code calls or names. std::set UsedConstexprSpecs; @@ -175,6 +176,11 @@ class ASTConverter { getInstantiationPoints() const { return InstantiationPoints; } + /// For each contracted function, by its identity: its contract as written, + /// which another file's declaration of it must state the same. + const std::map &getContractTexts() const { + return ContractTexts; + } private: /// Contract arithmetic is mathematical, as in ACSL and Verus spec code: an @@ -472,6 +478,8 @@ class ASTConverter { bool calleeReturnsFreshOwned(const FunctionDecl *FD); VIntMode specCallIntMode(const FunctionDecl *FD) const; std::string functionIdentity(const FunctionDecl *FD); + /// The clauses of a contract as written, each kind tagged. + std::string contractText(const FunctionContractInfo &FCI) const; std::string specIdentityFromExpr(const Expr *E); void injectTypeInvariants(const FunctionDecl *FD, VFunction &Fn); std::unique_ptr convertTypeInvariantExpr(const Expr *E); From 9e1dcaa458cca20a306a586b5f9ff93f12888cad Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:20 +0530 Subject: [PATCH 49/86] verify: Declare CrossFileRun, which settles the contracts of the files of one run. --- clang/lib/Verify/Driver/Verifier.h | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h index 91670b5bc8..25d9212d15 100644 --- a/clang/lib/Verify/Driver/Verifier.h +++ b/clang/lib/Verify/Driver/Verifier.h @@ -5,6 +5,7 @@ #include "../Backend/VerifyBackend.h" #include "llvm/Support/raw_ostream.h" #include +#include #include namespace clang { @@ -126,8 +127,37 @@ struct VerifyOptions { unsigned ConfirmBound = 10; /// Where the run counts the verdicts it prints, if anywhere. VerifySummary *Summary = nullptr; + /// A run over several files, which holds each file's results until every + /// file is verified (see CrossFileRun), or null. + class CrossFileRun *CrossFile = nullptr; }; +/// One run over several files. A contract that a file declares without a +/// definition may be defined and verified in another file of the run, so a +/// proof that rests on it waits: each file's results are kept, and once +/// every file is verified, a proof stands where every such contract it rests +/// on is established by its definition's verification, and is otherwise +/// unresolved (callee.contract), as within one file. +class CrossFileRun { +public: + CrossFileRun(); + ~CrossFileRun(); + CrossFileRun(const CrossFileRun &) = delete; + CrossFileRun &operator=(const CrossFileRun &) = delete; + + /// Settles the contracts the files assume against those they verify, + /// prints each file's results in the order the files were verified, and + /// counts them into \p Summary when it is given. Returns how many files + /// do not succeed. + unsigned finish(llvm::raw_ostream &OS, VerifySummary *Summary); + + struct Impl; + std::unique_ptr State; +}; + +/// Verifies the translation unit. In a run over several files +/// (Opts.CrossFile), the results wait for CrossFileRun::finish, and the +/// result is the file's as far as it alone decides. bool verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS, const VerifyOptions &Opts = VerifyOptions()); From 7b6e2f591dc366dcfab073753eb9b72be5a1e714 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:20 +0530 Subject: [PATCH 50/86] verify: Settle a contract a file declares without a definition against its verification in another file of the run. --- clang/lib/Verify/Driver/Verifier.cpp | 512 ++++++++++++++++++++++----- 1 file changed, 414 insertions(+), 98 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index d70a8780e6..853d54300a 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -61,6 +61,66 @@ using namespace clang; using namespace verify; +/// One printed result of a file of a run over several files, as verified +/// and, for a proof that rests on contracts the file declares without a +/// definition, as unresolved for want of one of them (the contract's +/// description in place of ContractPlaceholder); with what each counts. +struct CrossFileLine { + std::string Text; + std::string Demoted; + VerifySummary Counts; + VerifySummary DemotedCounts; + /// The keys of the contracts the proof rests on; empty for any other line. + std::set Assumes; + /// A finding about a proof (its line), and whether it holds for the entry + /// state alone, which no callee contract enters. + std::optional FindingOf; + bool FoundAtEntry = false; + /// A warning shown only when no file of the run defines this contract. + std::string UnlessDefined; +}; + +/// A contract a file verifies, offered to the other files. +struct CrossFileContract { + std::string Name; + std::string File; + bool Established = false; + std::set Assumes; +}; + +struct CrossFileReport { + std::vector Lines; + /// Printed after the lines (the time report). + std::string Trailer; + bool Ok = true; + std::map Defined; + /// The names of the contracts the lines rest on, by key. + std::map Names; +}; + +static constexpr llvm::StringLiteral ContractPlaceholder = + "@@cppverify-contract@@"; + +static void addSummary(VerifySummary &To, const VerifySummary &From) { + To.Verified += From.Verified; + To.Failed += From.Failed; + To.Unresolved += From.Unresolved; + To.BoundedSafe += From.BoundedSafe; + To.Trusted += From.Trusted; + To.Lowered += From.Lowered; + To.Exported += From.Exported; + To.Interrupted += From.Interrupted; + for (const auto &[Reason, Count] : From.Reasons) + To.Reasons[Reason] += Count; +} + +struct CrossFileRun::Impl { + std::vector Files; +}; + +CrossFileRun::CrossFileRun() : State(std::make_unique()) {} +CrossFileRun::~CrossFileRun() = default; + namespace { /// How deep the driver unfolds inductive predicates in a function, one @@ -1109,6 +1169,9 @@ struct VerifyDiagnostic { /// A failing obligation after the one a function's verdict reports: no /// verdict of its own. bool Additional = false; + /// In a run over several files: a warning that the contract of this + /// function has no definition, shown only if no file of the run has one. + std::string UnlessDefined; }; static uint64_t nanosecondsSince(std::chrono::steady_clock::time_point Start) { @@ -2808,6 +2871,21 @@ class Verifier { std::vector Diags; /// What --list-functions prints: each function's location and kind. std::vector> Listing; + /// Each contracted function's contract as written, by its identity. + std::map ContractTexts; + /// In a run over several files: the contracts declared here without a + /// definition, which another file may verify, by identity, with their + /// names; for each proof (its place in Diags), those it rests on, through + /// the contracts verified here; and each contract verified here, whether + /// this file establishes it and on which of the others it rests. + std::map Externals; + std::map> ExternalOf; + struct DefinedContract { + std::string Name; + bool Established = false; + std::set Assumes; + }; + std::map DefinedContracts; /// Where the verification of each reported function spent its time, in /// nanoseconds, and of the run, for --time-report. struct FunctionTime { @@ -3133,6 +3211,7 @@ class Verifier { for (const auto &[Loc, Message] : Converter.getWarnings()) Diags.push_back({VerifyDiagnostic::Warning, Message, Loc}); InstantiationPoints = Converter.getInstantiationPoints(); + ContractTexts = Converter.getContractTexts(); // A construct the verifier does not represent costs its function alone: // the function is Unresolved, its first error carrying the verdict, and // the rest of the translation unit is verified. An error outside every @@ -3898,13 +3977,16 @@ class Verifier { Diags.push_back({VerifyDiagnostic::Trusted, Fn->Name + " (contract assumed, not verified)", Fn->DeclLoc, Fn->Name}); - else if (!Fn->UnsupportedConstruct) + else if (!Fn->UnsupportedConstruct) { Diags.push_back( {VerifyDiagnostic::Warning, Fn->Name + " has a contract but no definition, so its callers " "are not verified; mark the declaration " "[[cppverify::trusted]] to assume the contract", Fn->DeclLoc, Fn->Name}); + if (Opts.CrossFile) + Diags.back().UnlessDefined = Fn->Identity; + } if (auto Error = InterfaceErrors.find(Fn->Identity); Error != InterfaceErrors.end()) { AllOk = false; @@ -5283,9 +5365,18 @@ class Verifier { // a demoted function no longer its contract, and an inductive predicate // whose rule proofs are not all established has no unfolding. std::set Unestablished; - for (const auto &Fn : Functions) - if (!Fn->IsSpec && !Fn->Uninterpreted && !Fn->IsTrusted) - Unestablished.insert(Fn->Identity); + for (const auto &Fn : Functions) { + if (Fn->IsSpec || Fn->Uninterpreted || Fn->IsTrusted) + continue; + // In a run over several files, a contract declared here without a + // definition holds for now: another file may verify it. + if (Opts.CrossFile && Fn->IsExternalContract && + !Fn->UnsupportedConstruct && !Fn->IsProof) { + Externals.emplace(Fn->Identity, Fn->Name); + continue; + } + Unestablished.insert(Fn->Identity); + } auto settled = [&](size_t Index) { return Diags[Index].isProof(); }; for (const auto &[Index, Identity, Callees] : CallDependencies) if (settled(Index)) @@ -5652,6 +5743,43 @@ class Verifier { Demoted = true; } } + // In a run over several files, each proof rests on the contracts + // declared here without a definition that its callees' contracts rest + // on, through the contracts verified here; each contract verified here + // is offered to the other files with what it rests on. + if (Opts.CrossFile) { + std::map> VerdictsOf; + for (const auto &[Index, Identity, Callees] : CallDependencies) + VerdictsOf[Identity].push_back(Index); + for (bool Changed = true; Changed;) { + Changed = false; + for (const auto &[Index, Identity, Callees] : CallDependencies) { + std::set Rests; + for (const std::string &Callee : Callees) { + if (Externals.count(Callee)) + Rests.insert(Callee); + for (size_t Verdict : VerdictsOf[Callee]) + if (auto It = ExternalOf.find(Verdict); It != ExternalOf.end()) + Rests.insert(It->second.begin(), It->second.end()); + } + std::set &Mine = ExternalOf[Index]; + const size_t Before = Mine.size(); + Mine.insert(Rests.begin(), Rests.end()); + Changed |= Mine.size() != Before; + } + } + for (const auto &Fn : Functions) { + if (Fn->IsSpec || Fn->IsProof || Fn->IsExternalContract || + Fn->Uninterpreted || !ContractTexts.count(Fn->Identity)) + continue; + DefinedContract &Defined = DefinedContracts[Fn->Identity]; + Defined.Name = Fn->Name; + Defined.Established = !Unestablished.count(Fn->Identity); + for (size_t Verdict : VerdictsOf[Fn->Identity]) + if (auto It = ExternalOf.find(Verdict); It != ExternalOf.end()) + Defined.Assumes.insert(It->second.begin(), It->second.end()); + } + } // Counterexamples their checks could not evaluate are confirmed by proof // now that it is known which contracts are established: a confirmation // rests only on those, and only where the spec facts its query assumes @@ -6258,6 +6386,21 @@ class Verifier { seconds(Time->Confirmation), Time->Name); } + /// Whether \p D is reported, and so counted: a hidden one is not, nor a + /// generated proof that holds. + static bool reported(const VerifyDiagnostic &D) { + return !D.Hidden && !(D.Quiet && (D.K == VerifyDiagnostic::Verified || + D.K == VerifyDiagnostic::Certified || + D.K == VerifyDiagnostic::Exported)); + } + + /// Whether --quiet leaves \p D out: what needs no attention. + bool quieted(const VerifyDiagnostic &D) const { + return Opts.Quiet && (D.isProof() || D.K == VerifyDiagnostic::Lowered || + D.K == VerifyDiagnostic::Exported || + D.K == VerifyDiagnostic::Trusted); + } + void printDiagnostics(llvm::raw_ostream &OS) const { for (const auto &[Loc, Line] : Listing) { PresumedLoc PLoc = Ctx.getSourceManager().getPresumedLoc(Loc); @@ -6267,108 +6410,174 @@ class Verifier { OS << Line << "\n"; } for (const auto &D : Diags) { - if (D.Hidden) - continue; - // A generated proof is reported only if it is not a proof. - if (D.Quiet && (D.K == VerifyDiagnostic::Verified || - D.K == VerifyDiagnostic::Certified || - D.K == VerifyDiagnostic::Exported)) + if (!reported(D)) continue; if (Opts.Summary) count(D, *Opts.Summary); - // --quiet leaves out what needs no attention. - if (Opts.Quiet && (D.isProof() || D.K == VerifyDiagnostic::Lowered || - D.K == VerifyDiagnostic::Exported || - D.K == VerifyDiagnostic::Trusted)) - continue; - if (Opts.Diagnostics == DiagnosticFormat::Json) { - printJSONDiagnostic(D, OS); + if (!quieted(D)) + printDiagnostic(D, OS); + } + } + + /// In a run over several files, this file's results as they wait for every + /// file to be verified: each reported diagnostic as printed and counted, + /// and a proof that rests on contracts declared here without a definition + /// also as unresolved for want of one, as demote() makes it, with + /// ContractPlaceholder for the contract. + CrossFileReport renderReport(bool Ok) const { + CrossFileReport Report; + Report.Ok = Ok; + auto key = [&](const std::string &Identity) { + auto It = ContractTexts.find(Identity); + return Identity + "\n" + (It != ContractTexts.end() ? It->second : ""); + }; + for (const auto &[Identity, Defined] : DefinedContracts) { + CrossFileContract &Contract = Report.Defined[key(Identity)]; + Contract.Name = Defined.Name; + Contract.File = std::string( + Ctx.getSourceManager() + .getFileEntryRefForID(Ctx.getSourceManager().getMainFileID()) + ->getName()); + Contract.Established = Defined.Established; + for (const std::string &Assumed : Defined.Assumes) + Contract.Assumes.insert(key(Assumed)); + } + for (const auto &[Identity, Name] : Externals) + Report.Names[key(Identity)] = Name; + std::map LineOf; + for (size_t Index = 0; Index != Diags.size(); ++Index) { + const VerifyDiagnostic &D = Diags[Index]; + if (!reported(D)) continue; + LineOf[Index] = Report.Lines.size(); + CrossFileLine &Line = Report.Lines.emplace_back(); + count(D, Line.Counts); + llvm::raw_string_ostream Text(Line.Text); + if (!quieted(D)) + printDiagnostic(D, Text); + if (!D.UnlessDefined.empty()) + Line.UnlessDefined = key(D.UnlessDefined); + if (D.FindingOf) { + if (auto It = LineOf.find(*D.FindingOf); It != LineOf.end()) + Line.FindingOf = It->second; + Line.FoundAtEntry = D.FoundAtEntry; } - const std::pair *Instantiation = - instantiationOf(D); - const std::string InstantiationNote = - Instantiation ? "in instantiation of " + Instantiation->second + - " '" + D.FunctionName + "' requested here" - : std::string(); - if (D.K == VerifyDiagnostic::Error && D.Span.isValid()) { - DiagnosticOptions DiagOpts; - DiagOpts.ShowPresumedLoc = true; - TextDiagnostic Text(OS, Ctx.getLangOpts(), DiagOpts); - Text.emitDiagnostic( - FullSourceLoc(D.Span.getBegin(), Ctx.getSourceManager()), - DiagnosticsEngine::Error, D.Message, - CharSourceRange::getTokenRange(D.Span), {}); - if (Instantiation) - Text.emitDiagnostic( - FullSourceLoc(Instantiation->first, Ctx.getSourceManager()), - DiagnosticsEngine::Note, InstantiationNote, {}, {}); + auto Rests = ExternalOf.find(Index); + if (!D.isProof() || Rests == ExternalOf.end() || Rests->second.empty()) continue; + for (const std::string &Assumed : Rests->second) + Line.Assumes.insert(key(Assumed)); + VerifyDiagnostic Demoted = D; + Demoted.K = VerifyDiagnostic::Unresolved; + // A callee contract enters only after the entry state. + if (Demoted.Vacuous && !Demoted.VacuousAtEntry) { + Demoted.Vacuous = false; + if (size_t At = Demoted.Message.find(" [vacuous]"); + At != std::string::npos) + Demoted.Message.erase(At, std::strlen(" [vacuous]")); } - if (D.Loc.isValid()) { - PresumedLoc PLoc = Ctx.getSourceManager().getPresumedLoc(D.Loc); - if (PLoc.isValid()) - OS << PLoc.getFilename() << ":" << PLoc.getLine() << ":" - << PLoc.getColumn() << ": "; - } - switch (D.K) { - case VerifyDiagnostic::Lowered: - OS << "Lowered: " << D.Message << "\n"; - break; - case VerifyDiagnostic::Verified: - OS << "Verified: " << D.Message << "\n"; - break; - case VerifyDiagnostic::Error: - OS << "error: " << D.Message << "\n"; - break; - case VerifyDiagnostic::Unresolved: - OS << "Unresolved: " << D.Message << "\n"; - if (D.Result) - for (const QuantifierProfileEntry &Entry : D.Result->QuantifierProfile) - OS << "note: the quantifier at " << Entry.Line << ":" - << Entry.Column << " was instantiated " << Entry.Instances - << " times, up to generation " << Entry.MaxGeneration << "\n"; - break; - case VerifyDiagnostic::Interrupted: - OS << "Interrupted: " << D.Message << "\n"; - break; - case VerifyDiagnostic::BoundedSafe: - OS << "BoundedSafe: " << D.Message << "\n"; - break; - case VerifyDiagnostic::Exported: - OS << "Exported: " << D.Message; - if (D.LeanAutomatic && D.Result) - OS << " (cppverify_auto proved " << D.LeanAutomatic << " of " - << std::set(D.Result->LeanGoals.begin(), - D.Result->LeanGoals.end()) - .size() - << " goals)"; - OS << "\n"; - break; - case VerifyDiagnostic::Certified: - OS << "Certified: " << D.Message << "\n"; - break; - case VerifyDiagnostic::MixedProof: - OS << "Proved (" << D.Result->BackendName << "): " << D.Message << "\n"; - break; - case VerifyDiagnostic::Trusted: - OS << "Trusted: " << D.Message << "\n"; - break; - case VerifyDiagnostic::Warning: - OS << "warning: " << D.Message << "\n"; - break; - } - if (Instantiation) { - PresumedLoc PLoc = - Ctx.getSourceManager().getPresumedLoc(Instantiation->first); - if (PLoc.isValid()) - OS << PLoc.getFilename() << ":" << PLoc.getLine() << ":" - << PLoc.getColumn() << ": "; - OS << "note: " << InstantiationNote << "\n"; - } - for (const std::string &Note : D.Notes) - OS << "note: " << Note << "\n"; + Demoted.Message += + " [reason=" + verifyReasonCode(VerifyReason::CalleeContract).str() + + "] (relies on " + ContractPlaceholder.str() + ")"; + if (!Demoted.Result) + Demoted.Result.emplace(); + Demoted.Result->Status = VerifyStatus::Unresolved; + Demoted.Result->Reason = VerifyReason::CalleeContract; + count(Demoted, Line.DemotedCounts); + llvm::raw_string_ostream DemotedText(Line.Demoted); + printDiagnostic(Demoted, DemotedText); + } + return Report; + } + + void printDiagnostic(const VerifyDiagnostic &D, llvm::raw_ostream &OS) const { + if (Opts.Diagnostics == DiagnosticFormat::Json) { + printJSONDiagnostic(D, OS); + return; + } + const std::pair *Instantiation = + instantiationOf(D); + const std::string InstantiationNote = + Instantiation ? "in instantiation of " + Instantiation->second + " '" + + D.FunctionName + "' requested here" + : std::string(); + if (D.K == VerifyDiagnostic::Error && D.Span.isValid()) { + DiagnosticOptions DiagOpts; + DiagOpts.ShowPresumedLoc = true; + TextDiagnostic Text(OS, Ctx.getLangOpts(), DiagOpts); + Text.emitDiagnostic( + FullSourceLoc(D.Span.getBegin(), Ctx.getSourceManager()), + DiagnosticsEngine::Error, D.Message, + CharSourceRange::getTokenRange(D.Span), {}); + if (Instantiation) + Text.emitDiagnostic( + FullSourceLoc(Instantiation->first, Ctx.getSourceManager()), + DiagnosticsEngine::Note, InstantiationNote, {}, {}); + return; + } + if (D.Loc.isValid()) { + PresumedLoc PLoc = Ctx.getSourceManager().getPresumedLoc(D.Loc); + if (PLoc.isValid()) + OS << PLoc.getFilename() << ":" << PLoc.getLine() << ":" + << PLoc.getColumn() << ": "; + } + switch (D.K) { + case VerifyDiagnostic::Lowered: + OS << "Lowered: " << D.Message << "\n"; + break; + case VerifyDiagnostic::Verified: + OS << "Verified: " << D.Message << "\n"; + break; + case VerifyDiagnostic::Error: + OS << "error: " << D.Message << "\n"; + break; + case VerifyDiagnostic::Unresolved: + OS << "Unresolved: " << D.Message << "\n"; + if (D.Result) + for (const QuantifierProfileEntry &Entry : D.Result->QuantifierProfile) + OS << "note: the quantifier at " << Entry.Line << ":" << Entry.Column + << " was instantiated " << Entry.Instances + << " times, up to generation " << Entry.MaxGeneration << "\n"; + break; + case VerifyDiagnostic::Interrupted: + OS << "Interrupted: " << D.Message << "\n"; + break; + case VerifyDiagnostic::BoundedSafe: + OS << "BoundedSafe: " << D.Message << "\n"; + break; + case VerifyDiagnostic::Exported: + OS << "Exported: " << D.Message; + if (D.LeanAutomatic && D.Result) + OS << " (cppverify_auto proved " << D.LeanAutomatic << " of " + << std::set(D.Result->LeanGoals.begin(), + D.Result->LeanGoals.end()) + .size() + << " goals)"; + OS << "\n"; + break; + case VerifyDiagnostic::Certified: + OS << "Certified: " << D.Message << "\n"; + break; + case VerifyDiagnostic::MixedProof: + OS << "Proved (" << D.Result->BackendName << "): " << D.Message << "\n"; + break; + case VerifyDiagnostic::Trusted: + OS << "Trusted: " << D.Message << "\n"; + break; + case VerifyDiagnostic::Warning: + OS << "warning: " << D.Message << "\n"; + break; } + if (Instantiation) { + PresumedLoc PLoc = + Ctx.getSourceManager().getPresumedLoc(Instantiation->first); + if (PLoc.isValid()) + OS << PLoc.getFilename() << ":" << PLoc.getLine() << ":" + << PLoc.getColumn() << ": "; + OS << "note: " << InstantiationNote << "\n"; + } + for (const std::string &Note : D.Notes) + OS << "note: " << Note << "\n"; } }; @@ -6379,12 +6588,119 @@ bool verify::verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS, Verifier V(Ctx, Opts, OS); bool Ok = V.run(); V.settled(); + if (Opts.CrossFile) { + CrossFileReport Report = V.renderReport(Ok); + llvm::raw_string_ostream Trailer(Report.Trailer); + if (Opts.TimeReport) + V.printTimeReport(Trailer); + Opts.CrossFile->State->Files.push_back(std::move(Report)); + return Ok; + } V.printDiagnostics(OS); if (Opts.TimeReport) V.printTimeReport(OS); return Ok; } +unsigned CrossFileRun::finish(llvm::raw_ostream &OS, VerifySummary *Summary) { + // A contract is established by its definitions' proofs once the contracts + // they rest on are, starting from none: one that rests on itself through + // other files is not. A contract defined in several files (inline in a + // header) must hold in each. + std::map> Definitions; + for (const CrossFileReport &File : State->Files) + for (const auto &[Key, Contract] : File.Defined) + Definitions[Key].push_back(&Contract); + std::set Established; + for (bool Changed = true; Changed;) { + Changed = false; + for (const auto &[Key, Contracts] : Definitions) + if (!Established.count(Key) && + llvm::all_of(Contracts, [&](const CrossFileContract *Contract) { + return Contract->Established && + llvm::all_of(Contract->Assumes, [&](const std::string &K) { + return Established.count(K) != 0; + }); + })) { + Established.insert(Key); + Changed = true; + } + } + auto describe = [&](const CrossFileReport &File, const std::string &Key) { + auto Name = File.Names.find(Key); + std::string Text = + "the contract of " + (Name != File.Names.end() + ? Name->second + : Key.substr(0, Key.find('\n'))); + auto Defined = Definitions.find(Key); + if (Defined == Definitions.end()) { + // A definition verified against another contract does not match. + const std::string Identity = Key.substr(0, Key.find('\n') + 1); + for (const auto &[Other, Contracts] : Definitions) + if (llvm::StringRef(Other).starts_with(Identity)) + return Text + ", which is not established: its definition in " + + Contracts.front()->File + + " is verified against another contract"; + return Text + " (no definition; mark it [[cppverify::trusted]] to " + "assume it), which is not established"; + } + for (const CrossFileContract *Contract : Defined->second) + if (!Contract->Established) + return Text + ", which its verification in " + Contract->File + + " does not establish"; + return Text + ", whose proof in " + Defined->second.front()->File + + " rests in turn on contracts not established"; + }; + // Whether some file defines the function of a contract's key, whatever + // contract its definition is verified against. + auto defined = [&](const std::string &Key) { + const std::string Identity = Key.substr(0, Key.find('\n') + 1); + auto It = Definitions.lower_bound(Identity); + return It != Definitions.end() && + llvm::StringRef(It->first).starts_with(Identity); + }; + unsigned Failures = 0; + for (const CrossFileReport &File : State->Files) { + std::vector Demoted(File.Lines.size()); + for (size_t I = 0; I != File.Lines.size(); ++I) + for (const std::string &Key : File.Lines[I].Assumes) + if (!Established.count(Key)) { + Demoted[I] = true; + break; + } + bool Ok = File.Ok; + for (size_t I = 0; I != File.Lines.size(); ++I) { + const CrossFileLine &Line = File.Lines[I]; + if (!Line.UnlessDefined.empty() && defined(Line.UnlessDefined)) + continue; + // A finding rests on the facts of its query, as its proof does. + if (Line.FindingOf && Demoted[*Line.FindingOf] && !Line.FoundAtEntry) + continue; + if (!Demoted[I]) { + OS << Line.Text; + if (Summary) + addSummary(*Summary, Line.Counts); + continue; + } + Ok = false; + std::string Missing; + for (const std::string &Key : Line.Assumes) + if (!Established.count(Key)) + Missing += (Missing.empty() ? "" : "; ") + describe(File, Key); + std::string Text = Line.Demoted; + for (size_t At = Text.find(ContractPlaceholder); At != std::string::npos; + At = Text.find(ContractPlaceholder, At + Missing.size())) + Text.replace(At, ContractPlaceholder.size(), Missing); + OS << Text; + if (Summary) + addSummary(*Summary, Line.DemotedCounts); + } + OS << File.Trailer; + Failures += !Ok; + } + return Failures; +} + LeanProjectReplay verify::replayLeanProject(const std::vector &Modules, const VerifyOptions &Opts) { From 03162aac7e185f7361d262bee720b4f76c91d328 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:20 +0530 Subject: [PATCH 51/86] verify: Settle contracts across the files of one run. --- clang/tools/cpp-verify/Main.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index a43fc8cd71..891e8799e8 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -319,6 +319,9 @@ namespace { static int gVerifyFailures = 0; static verify::VerifySummary gSummary; +/// A run over several files settles the contracts each declares without a +/// definition against those the others verify, before printing. +static std::unique_ptr gCrossFile; /// One line for the run: how many verdicts of each kind it reported, the /// reasons of the unresolved ones, and the time it took. @@ -476,6 +479,7 @@ class VerifyConsumer : public ASTConsumer { FunctionPatterns.end()); VOpts.ConfirmBound = ConfirmBound.getValue(); VOpts.Summary = &gSummary; + VOpts.CrossFile = gCrossFile.get(); if (!verify::verifyTranslationUnit(Ctx, llvm::outs(), VOpts)) ++gVerifyFailures; } @@ -1168,7 +1172,13 @@ int main(int argc, const char **argv) { TextDiagnosticPrinter ArgumentDiagnostics(llvm::errs(), *ArgumentOptions); Tool.setDiagnosticConsumer(&ArgumentDiagnostics); VerifyActionFactory Factory(ArgumentDiagnostics); + // Lean exports and --list-functions have no verdicts to settle. + if (OptionsParser.getSourcePathList().size() > 1 && BackendOpt != "lean" && + LeanFallback.empty() && !ListFunctions) + gCrossFile = std::make_unique(); int RC = Tool.run(&Factory); + if (gCrossFile) + gVerifyFailures += gCrossFile->finish(llvm::outs(), &gSummary); if (DiagnosticsFormat == verify::DiagnosticFormat::Text && !ListFunctions) printSummary(Start); if (verify::interruptRequested()) From dc41ce8b3d39693a959cd79622c49784ab8ee11a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:21 +0530 Subject: [PATCH 52/86] test: Add a header declaring a contract for the cross-file tests. --- clang/test/Verify/suite/Inputs/across/include/mathx.h | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/across/include/mathx.h diff --git a/clang/test/Verify/suite/Inputs/across/include/mathx.h b/clang/test/Verify/suite/Inputs/across/include/mathx.h new file mode 100644 index 0000000000..d688ecc585 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/across/include/mathx.h @@ -0,0 +1,2 @@ +int clamp100(int x) + cppverify::post(cppverify::result >= 0 && cppverify::result <= 100); From 0d0cca61542e2cd03364c08e79d75bd9a9067417 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:21 +0530 Subject: [PATCH 53/86] test: Add the definition of the header's contract, right or wrong. --- clang/test/Verify/suite/Inputs/across/src/mathx.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/across/src/mathx.cpp diff --git a/clang/test/Verify/suite/Inputs/across/src/mathx.cpp b/clang/test/Verify/suite/Inputs/across/src/mathx.cpp new file mode 100644 index 0000000000..c00f5a85d5 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/across/src/mathx.cpp @@ -0,0 +1,11 @@ +#include "mathx.h" + +// BUG is 100, or 101 for a definition that breaks its contract. +int clamp100(int x) +{ + if (x < 0) + return 0; + if (x > 100) + return BUG; + return x; +} From a735afc2bbb518e4cefb77c235dce6e206f5b0b6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:21 +0530 Subject: [PATCH 54/86] test: Add callers of the header's contract. --- clang/test/Verify/suite/Inputs/across/src/a.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/across/src/a.cpp diff --git a/clang/test/Verify/suite/Inputs/across/src/a.cpp b/clang/test/Verify/suite/Inputs/across/src/a.cpp new file mode 100644 index 0000000000..ed53d64b88 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/across/src/a.cpp @@ -0,0 +1,13 @@ +#include "mathx.h" + +int scaled(int x) + cppverify::post(cppverify::result >= 0 && cppverify::result <= 200) +{ + return 2 * clamp100(x); +} + +int twice_scaled(int x) + cppverify::post(cppverify::result >= 0 && cppverify::result <= 400) +{ + return 2 * scaled(x); +} From a75cedcde633f01e3ba5eb2e9c57e60cfd0e097a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:22 +0530 Subject: [PATCH 55/86] test: Add a declaration that states another contract than the definition's. --- clang/test/Verify/suite/Inputs/across/src/other.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/across/src/other.cpp diff --git a/clang/test/Verify/suite/Inputs/across/src/other.cpp b/clang/test/Verify/suite/Inputs/across/src/other.cpp new file mode 100644 index 0000000000..854852ff92 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/across/src/other.cpp @@ -0,0 +1,10 @@ +// A declaration that states another contract than the one mathx.cpp's +// definition is verified against. +int clamp100(int x) + cppverify::post(cppverify::result >= 0 && cppverify::result <= 50); + +int halved(int x) + cppverify::post(cppverify::result >= 0 && cppverify::result <= 50) +{ + return clamp100(x); +} From d6faf0abe0dcc82bb421ab349f1034349ec39272 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:22 +0530 Subject: [PATCH 56/86] test: Add one of two files whose contracts rest on each other. --- clang/test/Verify/suite/Inputs/across/src/ping.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/across/src/ping.cpp diff --git a/clang/test/Verify/suite/Inputs/across/src/ping.cpp b/clang/test/Verify/suite/Inputs/across/src/ping.cpp new file mode 100644 index 0000000000..a248efe3bf --- /dev/null +++ b/clang/test/Verify/suite/Inputs/across/src/ping.cpp @@ -0,0 +1,10 @@ +int pong(int n) + cppverify::pre(n >= 0 && n < 1000) + cppverify::post(cppverify::result == 0); + +int ping(int n) + cppverify::pre(n >= 0 && n < 1000) + cppverify::post(cppverify::result == 0) +{ + return n == 0 ? 0 : pong(n - 1); +} From 85a6b983c5095596654fd6a7320635e6f766ffed Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:23 +0530 Subject: [PATCH 57/86] test: Add the other of two files whose contracts rest on each other. --- clang/test/Verify/suite/Inputs/across/src/pong.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/across/src/pong.cpp diff --git a/clang/test/Verify/suite/Inputs/across/src/pong.cpp b/clang/test/Verify/suite/Inputs/across/src/pong.cpp new file mode 100644 index 0000000000..2159e5b02a --- /dev/null +++ b/clang/test/Verify/suite/Inputs/across/src/pong.cpp @@ -0,0 +1,10 @@ +int ping(int n) + cppverify::pre(n >= 0 && n < 1000) + cppverify::post(cppverify::result == 0); + +int pong(int n) + cppverify::pre(n >= 0 && n < 1000) + cppverify::post(cppverify::result == 0) +{ + return n == 0 ? 0 : ping(n - 1); +} From d187b18c44242837aaca2cd3a6101d38068bec34 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:23 +0530 Subject: [PATCH 58/86] test: One run over several files settles the contracts they declare without a definition. --- .../Verify/suite/contracts_across_files.test | 55 +++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 clang/test/Verify/suite/contracts_across_files.test diff --git a/clang/test/Verify/suite/contracts_across_files.test b/clang/test/Verify/suite/contracts_across_files.test new file mode 100644 index 0000000000..05e410f9e0 --- /dev/null +++ b/clang/test/Verify/suite/contracts_across_files.test @@ -0,0 +1,55 @@ +# One run over several files settles a contract that a file declares without +# a definition against the verification of its definition in another file: +# a proof that rests on it stands where that verification establishes it, +# and is unresolved (callee.contract) where it does not, as within one file. +# +# RUN: %cpp-verify --jobs=1 %S/Inputs/across/src/a.cpp %S/Inputs/across/src/mathx.cpp \ +# RUN: -- -I%S/Inputs/across/include -DBUG=100 2>&1 \ +# RUN: | FileCheck %s --check-prefix=RIGHT --implicit-check-not=warning: +# RUN: not %cpp-verify --jobs=1 %S/Inputs/across/src/a.cpp %S/Inputs/across/src/mathx.cpp \ +# RUN: -- -I%S/Inputs/across/include -DBUG=101 2>&1 \ +# RUN: | FileCheck %s --check-prefix=WRONG --implicit-check-not=warning: +# RUN: not %cpp-verify --jobs=1 %S/Inputs/across/src/mathx.cpp %S/Inputs/across/src/a.cpp \ +# RUN: -- -I%S/Inputs/across/include -DBUG=101 2>&1 \ +# RUN: | FileCheck %s --check-prefix=ORDER +# RUN: not %cpp-verify --jobs=1 --diagnostics-format=json %S/Inputs/across/src/a.cpp \ +# RUN: %S/Inputs/across/src/mathx.cpp -- -I%S/Inputs/across/include -DBUG=101 \ +# RUN: 2>/dev/null | FileCheck %s --check-prefix=JSON +# RUN: not %cpp-verify --jobs=1 %S/Inputs/across/src/a.cpp -- -I%S/Inputs/across/include \ +# RUN: 2>&1 | FileCheck %s --check-prefix=ALONE +# RUN: not %cpp-verify --jobs=1 %S/Inputs/across/src/other.cpp %S/Inputs/across/src/mathx.cpp \ +# RUN: -- -I%S/Inputs/across/include -DBUG=100 2>&1 \ +# RUN: | FileCheck %s --check-prefix=OTHER --implicit-check-not=warning: +# RUN: not %cpp-verify --jobs=1 %S/Inputs/across/src/ping.cpp %S/Inputs/across/src/pong.cpp \ +# RUN: -- 2>&1 | FileCheck %s --check-prefix=CYCLE + +RIGHT: Verified: scaled [backend=z3] +RIGHT-NEXT: Verified: twice_scaled [backend=z3] +RIGHT-NEXT: Verified: clamp100 [backend=z3] +RIGHT-NEXT: Summary: 3 verified + +WRONG: Unresolved: scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which its verification in {{.*}}mathx.cpp does not establish) +WRONG-NEXT: Unresolved: twice_scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which its verification in {{.*}}mathx.cpp does not establish) +WRONG-NEXT: mathx.h:2:42: error: verification failed: clamp100 [{{.*}}::postcondition@2:42] (counterexample: {{.*}}result [ssa=__result_1] [type=i32] = 101 +WRONG: Summary: 1 failed, 2 unresolved (callee.contract 2) + +The files are printed in the order they are given, settled together. +ORDER: mathx.h:2:42: error: verification failed: clamp100 +ORDER: Unresolved: scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which its verification in {{.*}}mathx.cpp does not establish) +ORDER: Summary: 1 failed, 2 unresolved (callee.contract 2) + +JSON: {"backend":"z3","function":"scaled","message":"scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which its verification in {{.*}}mathx.cpp does not establish)","reason":"callee.contract",{{.*}}"status":"unresolved"} +JSON: "function":"clamp100","message":"verification failed: clamp100 + +A file alone is as before: the contract has no definition. +ALONE: mathx.h:1:5: warning: clamp100 has a contract but no definition, so its callers are not verified; mark the declaration {{\[\[cppverify::trusted\]\]}} to assume the contract +ALONE-NEXT: Unresolved: scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100 (no definition; mark it {{\[\[cppverify::trusted\]\]}} to assume it), which is not established) +ALONE-NEXT: Unresolved: twice_scaled [backend=z3] [reason=callee.contract] (relies on the contract of scaled, which is not established) + +A declaration that states another contract is not the definition's. +OTHER: Unresolved: halved [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which is not established: its definition in {{.*}}mathx.cpp is verified against another contract) +OTHER-NEXT: Verified: clamp100 [backend=z3] + +Contracts whose proofs rest on each other through files establish nothing. +CYCLE: Unresolved: ping [backend=z3] [reason=callee.contract] (relies on the contract of pong, whose proof in {{.*}}pong.cpp rests in turn on contracts not established) +CYCLE-NEXT: Unresolved: pong [backend=z3] [reason=callee.contract] (relies on the contract of ping, whose proof in {{.*}}ping.cpp rests in turn on contracts not established) From 539b11c855a9c928807f346cb327dd3ae3147705 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:23 +0530 Subject: [PATCH 59/86] docs: Describe trust on declarations and definitions, and contracts across files. --- website/source/language/functions-loops.rst | 76 +++++++++++++++++++-- 1 file changed, 70 insertions(+), 6 deletions(-) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index 2aabca3f6f..e49fea9826 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -89,9 +89,11 @@ outside the verified subset, or a lemma you decide to assume. trusted.cpp:16:39: Trusted: sq_nonnegative (contract assumed, not verified) Verified: sample [backend=z3] [trusts=clamp_byte,read_sensor,sq_nonnegative] -- On a declaration, the contract is assumed at every call; the preconditions - are still checked there. -- On a definition, the body is compiled but not verified. +- On a declaration, the contract is assumed at every call that sees no + definition; the preconditions are still checked there. +- On a definition, the body is compiled but not verified. A definition that + only inherits the mark from an earlier declaration (a header's, say) is + verified: to leave a body unverified, mark the definition itself. - On a proof function, the postcondition is an axiom. - A spec function cannot be trusted: its definition is its meaning, so there is nothing to assume. The attribute is an error there. @@ -101,9 +103,8 @@ outside the verified subset, or a lemma you decide to assume. ``[trusts=...]`` (JSON ``"trusts"``), transitively through verified callees: a caller of ``sample`` carries the same three names. -The mark may appear on any declaration of the function. Without it, a -contract with no definition is neither proved nor vouched for, so it proves -nothing: +Without the mark, a contract with no definition is neither proved nor +vouched for, so it proves nothing: .. code-block:: cpp @@ -129,6 +130,69 @@ that contradicts the state of a call (no result can satisfy it) would make everything after the call hold vacuously; CppVerify reports that case with ``[vacuous]`` and a warning at the call (see :doc:`tooling`). +Contracts across files +---------------------- + +Real code declares a function with its contract in a header and defines it +in one file. Verified alone, a file that sees only the declaration has no +definition, as above. Verified together in one run, the files settle it: a +proof that rests on the contract stands once the verification of its +definition establishes it, and is ``Unresolved`` with ``callee.contract`` +otherwise, as within one file. + +.. cppverify-example: fragment +.. code-block:: cpp + + // include/mathx.h + int clamp100(int x) + cv::post(cv::result >= 0 && cv::result <= 100); + + // src/mathx.cpp + #include "mathx.h" + + int clamp100(int x) + { + if (x < 0) + return 0; + if (x > 100) + return 101; + return x; + } + + // src/a.cpp + #include "mathx.h" + + int scaled(int x) + cv::post(cv::result >= 0 && cv::result <= 200) + { + return 2 * clamp100(x); + } + +.. code-block:: text + + $ cpp-verify src/a.cpp src/mathx.cpp -- -Iinclude + Unresolved: scaled [backend=z3] [reason=callee.contract] (relies on the contract of clamp100, which its verification in src/mathx.cpp does not establish) + include/mathx.h:2:42: error: verification failed: clamp100 [fn_...::postcondition@2:42] (counterexample: result [ssa=__result_1] [type=i32] = 101, x [ssa=x_0] [type=i32] = 101; ...) [backend=z3] [reason=counterexample] + Summary: 1 failed, 1 unresolved (callee.contract 1) in 0.0 s + +With ``return 100;`` both verify, and the warning that ``clamp100`` has no +definition is not printed. The results of each file are held until every +file is verified, then printed in the order the files are given. + +- A declaration matches a definition with the same function (its mangled + name) and the same contract as written. A file that states another + contract for the function does not match: its callers are unresolved, and + the message says that the definition is verified against another + contract. +- A contract whose proof rests on contracts of other files is established + only once they are. Two files whose proofs rest on each other's contracts + establish nothing, as proofs that rest on themselves never do. +- A trusted declaration stays an assumption, with ``[trusts=...]`` on what + relies on it; only its definition, where it is verified, can find a wrong + contract. +- Files verified in separate runs, as in a build that verifies each object, + do not settle their contracts yet. + An uncontracted, non-recursive, loop-free ``constexpr`` definition may be lifted for use in contract expressions; a recursive one used with symbolic arguments is rejected. It is lifted where verification uses it: in a contract, a From ec24d8ab9256d7b50929b494f779e4c09c70a9ee Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:24 +0530 Subject: [PATCH 60/86] docs: Describe a run over several files. --- website/source/language/tooling.rst | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index 9b49b4be69..a9fb5fd4b1 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -14,6 +14,7 @@ Standalone verifier cpp-verify --function='parse_*' --function=encode file.cpp cpp-verify --time-report file.cpp cpp-verify file.cpp -- -I include -DNDEBUG + cpp-verify src/a.cpp src/mathx.cpp -- -I include cpp-verify --backend=z3 file.cpp cpp-verify --backend=cvc5 file.cpp cpp-verify --backend=portfolio file.cpp @@ -43,6 +44,12 @@ flags of a listed neighbour. Without a database the file is compiled with those alone. Flags after ``--`` replace the database, and ``--extra-arg=FLAG`` adds one flag either way. +Several files given to one run are verified one after the other and +settled together: a contract one file declares without a definition holds +for a proof once its definition's verification in another file establishes +it (see :doc:`functions-loops`). Their results are printed once every file +is verified, in the order given. + Input files and compiler errors ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ From 6d5f849704dc962412f8573d96b9ee733090f8e7 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:24 +0530 Subject: [PATCH 61/86] docs: Note contracts across files in the limitations. --- website/source/language/limitations.rst | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index db8af88024..a3577b91de 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -672,7 +672,10 @@ CppVerify does not yet ship comprehensive libc or C++ standard-library models: of the standard library it knows ``std::min`` and ``std::max`` of two integers (:doc:`functions-loops`), and any other of its functions is an error naming it. An uncontracted call fails closed; a contract is assumed -only when it is marked ``[[cppverify::trusted]]``. Contracts are not saved in precompiled +only when it is marked ``[[cppverify::trusted]]``, or, in one run over +several files, once the verification of its definition in another of them +establishes it (:doc:`functions-loops`); files verified in separate runs do +not settle their contracts yet. Contracts are not saved in precompiled headers: a function declared in a PCH has no contract for the verifier, so a contracted function that calls it fails closed (``call to function without a verification contract``). From c022adbf3b0ef69933a62253b1cf20660081e5f1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:24 +0530 Subject: [PATCH 62/86] docs: Point to one run over several files in the book. --- .../source/book/part-ii/ch17-backends-modular-calls.rst | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst index 04fb031093..971f0301d3 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -1306,6 +1306,14 @@ are ``Unresolved`` with reason ``callee.contract``, and a warning points at the declaration. A forgotten definition therefore cannot silently turn into an axiom. +Where the definition is in another file, verify the files together: +``cpp-verify src/a.cpp src/mathx.cpp -- -Iinclude``. The run settles the +contract a header declares against the verification of its definition, so +``a.cpp``'s callers of ``clamp100`` are verified when ``mathx.cpp``'s body +meets the contract, and ``Unresolved`` when it does not. Mark a header's +declaration trusted only for a definition outside the program: on the +definition, which inherits the mark, the body is still verified. + The same boundary exists in other verifiers. Verus assumes the specification of a function marked ``#[verifier::external_body]``. Frama-C assumes the contract of a function without a body when it proves the callers. CppVerify From 1029ccbcfda430bae4246441f313e01bceaee7b1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:25 +0530 Subject: [PATCH 63/86] docs: Note contracts across files in the 0.2.0 release notes. --- website/source/release-notes.rst | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index e5c28d72fc..40c915bd02 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -497,6 +497,18 @@ check that fails. A failure of a function whose loop has no ``cppverify::decreases`` names that loop too (:doc:`language/functions-loops`). +**Contracts across files.** A contract declared in a header and defined in +another file left every caller ``Unresolved [callee.contract]``, even when +one run verified both files, and the warning's advice, +``[[cppverify::trusted]]`` on the declaration, also stopped the verification +of the definition, which inherited the mark, so a wrong body was never +checked. Now one run over several files settles such a contract: a proof +that rests on it stands once the verification of its definition in another +file establishes it, and is ``Unresolved`` with ``callee.contract`` +otherwise, naming the file. A definition is trusted only by a mark of its +own, so a trusted header declaration no longer hides it +(: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 From 84f27047e235fb18c58630397cfc71f02f3e8ffc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:25 +0530 Subject: [PATCH 64/86] docs: Design trust on definitions and the settlement of contracts across files. --- docs/DESIGN.md | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 608c8e4b9a..d98d67279f 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -139,15 +139,26 @@ it is `Unresolved` with reason `callee.contract`. `[[cppverify::trusted]]` (a standard C++ attribute, like Verus's `#[verifier::external_body]`) marks a contract as assumed: on a declaration -the contract holds at every call (whose preconditions are still checked); on -a definition the body is compiled but not verified; on a proof function the -postcondition is an axiom. A spec cannot be trusted, since its definition is +the contract holds at every call that sees no definition (whose +preconditions are still checked); on a definition the body is compiled but +not verified; on a proof function the postcondition is an axiom. A +definition that only inherits the mark from an earlier declaration, as +Clang's attribute inheritance gives it, is verified (decision Q13 of the 0.2 +plan): before 0.2 the mark on a header's declaration stopped the +verification of the definition, so a wrong body was never checked. A spec cannot be trusted, since its definition is its meaning. The mark is written on each function: `#pragma clang attribute` cannot apply it to a region. A trusted function reports `Trusted: f (contract assumed, not verified)`, and every verdict that relies on it, directly or through verified callees, carries `[trusts=f]`. A contract without a definition and without the mark is not assumed: a warning names it, and its callers are -`Unresolved` with reason `callee.contract`. A trusted contract writes only +`Unresolved` with reason `callee.contract`. In one run over several files, +such a contract is settled across them, as Frama-C settles a property's +status over the files of a project: a proof that rests on it, directly or +through the file's own contracts, stands once the verification of its +definition in another file establishes it (a contract established only +through other files' contracts once those are, starting from none), and is +`Unresolved` with `callee.contract` otherwise. A declaration matches a +definition with the same function and the same contract as written. A trusted contract writes only its `cppverify::modifies` footprints; without them it writes nothing through a pointer or reference to const, and is taken to write the whole heap through a mutable one (see `cppverify::modifies` below). From 2e878af0ef4a7c75edb4fc28564351d335761312 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:50:26 +0530 Subject: [PATCH 65/86] docs: Describe how a run over several files holds and settles its files. --- docs/ARCHITECTURE.md | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 6651545b35..d3b36bb28b 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -2479,7 +2479,29 @@ again where it is used. - a trusted function reports `Trusted`; an unmarked contract without a definition draws a warning, and every caller whose proof relies on it (or on any callee contract whose verification failed) is demoted to - `Unresolved` with reason `callee.contract`; + `Unresolved` with reason `callee.contract`. A function is trusted by + the mark on its definition, or on any declaration when it has none + (`ASTConverter::convertFunction`: an inherited mark does not count); + - in a run over several files (`VerifyOptions::CrossFile`, a + `CrossFileRun` the driver creates when given more than one file), an + unmarked contract without a definition is provisionally established + instead (`Verifier::Externals`). After the fixpoints below, each proof + records the external contracts it rests on, through the file's own + contracts' verdicts (`ExternalOf`), and each contract the file + verifies is offered with whether the file establishes it and on which + external contracts that rests (`DefinedContracts`), keyed by identity + and the contract as written (`ASTConverter::contractText`). The file's + results are rendered while its AST lives (`renderReport`): each line + as verified and, for a proof that rests on external contracts, as + `demote` would make it, with a placeholder for the contracts, both + counted for the summary. Once every file is verified, + `CrossFileRun::finish` establishes contracts by a least fixpoint over + the files (a contract once every definition of it is established in + its file and the external contracts that rests on are), prints each + file's lines with the demoted form where a contract a proof rests on is + not established, drops the warning of a contract some file defines and + the findings of a demoted proof (but those of the entry state), and + counts the files that do not succeed; - `[trusts=...]` lists the trusted contracts a proof uses, closed transitively over verified callees (JSON `"trusts"`); - one fixpoint settles the reasons: a verdict relying on a spec whose From 311e05c37e105b66e719cdd66a98177555908e2a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:48 +0530 Subject: [PATCH 66/86] verify: Add -fverify-contracts-out, where a compilation records its contracts. --- clang/include/clang/Options/Options.td | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/clang/include/clang/Options/Options.td b/clang/include/clang/Options/Options.td index d81b16ca14..9fe881f6d1 100644 --- a/clang/include/clang/Options/Options.td +++ b/clang/include/clang/Options/Options.td @@ -2531,6 +2531,12 @@ defm verify_contracts : BoolFOption<"verify-contracts", // default once contracts are enabled, and -fno-verify turns compilation into a // syntax/semantics-only "light check". It implies -fverify-contracts (handled in // the driver) because it is meaningless without the contract language. +def fverify_contracts_out_EQ : Joined<["-"], "fverify-contracts-out=">, + Group, Visibility<[ClangOption, CC1Option]>, + MetaVarName<"">, + HelpText<"Write the contracts CppVerify verifies in this file and those it " + "assumes from other files, for cpp-verify --check-contracts">, + MarshallingInfoString>; def fno_verify : Flag<["-"], "fno-verify">, Group, Visibility<[ClangOption, CC1Option]>, HelpText<"Check contract syntax and semantics but skip CppVerify SMT verification " From ddefb15d039c281328f510667888f1b5e6b25ca3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:48 +0530 Subject: [PATCH 67/86] verify: Hold the path of -fverify-contracts-out in the frontend options. --- clang/include/clang/Frontend/FrontendOptions.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/clang/include/clang/Frontend/FrontendOptions.h b/clang/include/clang/Frontend/FrontendOptions.h index 0f81ff3a7e..29244682db 100644 --- a/clang/include/clang/Frontend/FrontendOptions.h +++ b/clang/include/clang/Frontend/FrontendOptions.h @@ -525,6 +525,10 @@ class FrontendOptions { /// (in the format produced by -fdump-record-layouts). std::string OverrideRecordLayoutsFile; + /// Where CppVerify writes the contracts this file verifies and those it + /// assumes from other files, for cpp-verify --check-contracts. + std::string VerifyContractsOut; + /// Auxiliary triple for CUDA/HIP/SYCL compilation. std::string AuxTriple; From f677e84af8345fc3c8e8183db48c0077160825ba Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:49 +0530 Subject: [PATCH 68/86] verify: Pass -fverify-contracts-out on to the compiler. --- clang/lib/Driver/ToolChains/Clang.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/lib/Driver/ToolChains/Clang.cpp b/clang/lib/Driver/ToolChains/Clang.cpp index 69bf819504..116b559c6a 100644 --- a/clang/lib/Driver/ToolChains/Clang.cpp +++ b/clang/lib/Driver/ToolChains/Clang.cpp @@ -6698,6 +6698,7 @@ void Clang::ConstructJob(Compilation &C, const JobAction &JA, // -fno-verify skips the SMT step. It is meaningless without the contract // language, so when neither -f/-fno-verify-contracts was given it implies // -fverify-contracts, yielding a syntax/semantics-only "light check". + Args.AddLastArg(CmdArgs, options::OPT_fverify_contracts_out_EQ); if (Args.hasArg(options::OPT_fno_verify)) { CmdArgs.push_back("-fno-verify"); if (!Args.hasArg(options::OPT_fverify_contracts) && From 2add478435199eec3c006cf88e06d0ee9df7db3d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:49 +0530 Subject: [PATCH 69/86] verify: Record a compilation's contracts where -fverify-contracts-out says. --- clang/lib/CodeGen/CodeGenAction.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/clang/lib/CodeGen/CodeGenAction.cpp b/clang/lib/CodeGen/CodeGenAction.cpp index 20452cf44b..f83b6f58af 100644 --- a/clang/lib/CodeGen/CodeGenAction.cpp +++ b/clang/lib/CodeGen/CodeGenAction.cpp @@ -244,7 +244,8 @@ bool BackendConsumer::LinkInModules(llvm::Module *M) { void BackendConsumer::HandleTranslationUnit(ASTContext &C) { std::optional> VerifyFuture; if (verify::shouldRunCppVerify(CI)) - VerifyFuture = verify::startCppVerifyAsync(C); + VerifyFuture = + verify::startCppVerifyAsync(C, CI.getFrontendOpts().VerifyContractsOut); { llvm::TimeTraceScope TimeScope("Frontend"); From e2cd3998a4ad4abd3be1e6a338fb2112cf16f6db Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:50 +0530 Subject: [PATCH 70/86] verify: Let the compile-time verifier record the contracts of its file. --- clang/lib/Verify/Driver/CppVerifyIntegration.cpp | 8 +++++--- clang/lib/Verify/Driver/CppVerifyIntegration.h | 5 ++++- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/clang/lib/Verify/Driver/CppVerifyIntegration.cpp b/clang/lib/Verify/Driver/CppVerifyIntegration.cpp index c3c09897ab..497bcfe7c3 100644 --- a/clang/lib/Verify/Driver/CppVerifyIntegration.cpp +++ b/clang/lib/Verify/Driver/CppVerifyIntegration.cpp @@ -20,11 +20,13 @@ bool verify::shouldRunCppVerify(const CompilerInstance &CI) { } std::future -verify::startCppVerifyAsync(ASTContext &Ctx) { - return std::async(std::launch::async, [&Ctx]() { +verify::startCppVerifyAsync(ASTContext &Ctx, std::string ContractsOut) { + return std::async(std::launch::async, [&Ctx, ContractsOut]() { std::string Buffer; llvm::raw_string_ostream OS(Buffer); - bool Ok = verifyTranslationUnit(Ctx, OS, VerifyOptions{}); + VerifyOptions Opts; + Opts.ContractsOut = ContractsOut; + bool Ok = verifyTranslationUnit(Ctx, OS, Opts); OS.flush(); return CppVerifyAsyncResult{Ok, std::move(Buffer)}; }); diff --git a/clang/lib/Verify/Driver/CppVerifyIntegration.h b/clang/lib/Verify/Driver/CppVerifyIntegration.h index 6246a1b392..bfee19996e 100644 --- a/clang/lib/Verify/Driver/CppVerifyIntegration.h +++ b/clang/lib/Verify/Driver/CppVerifyIntegration.h @@ -19,7 +19,10 @@ bool shouldRunCppVerify(const CompilerInstance &CI); /// Start SMT verification on \p Ctx in a background thread. The AST must not be /// mutated while the future is pending (safe during codegen IR generation). -std::future startCppVerifyAsync(ASTContext &Ctx); +/// With \p ContractsOut, contracts declared without a definition are assumed +/// and recorded there with those verified, for cpp-verify --check-contracts. +std::future +startCppVerifyAsync(ASTContext &Ctx, std::string ContractsOut = ""); /// Join \p Future, print verifier output, and report diagnostics on failure. bool finishCppVerify(CompilerInstance &CI, std::future Future); From 8335a3db24c3bf5137004c664dcf7ddb5825e30d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:51 +0530 Subject: [PATCH 71/86] verify: Declare --contracts-out and the check of files verified apart. --- clang/lib/Verify/Driver/Verifier.h | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h index 25d9212d15..4144be1306 100644 --- a/clang/lib/Verify/Driver/Verifier.h +++ b/clang/lib/Verify/Driver/Verifier.h @@ -7,6 +7,7 @@ #include #include #include +#include namespace clang { class ASTContext; @@ -130,6 +131,11 @@ struct VerifyOptions { /// A run over several files, which holds each file's results until every /// file is verified (see CrossFileRun), or null. class CrossFileRun *CrossFile = nullptr; + /// Where to write the contracts this file verifies and those it assumes + /// from other files, for checkContracts. With it, a contract declared + /// without a definition holds for now, and a proof that rests on it says + /// so ([assumes=...]): the check of the files together settles it. + std::string ContractsOut; }; /// One run over several files. A contract that a file declares without a @@ -155,6 +161,13 @@ class CrossFileRun { std::unique_ptr State; }; +/// The check of files verified apart (their ContractsOut records): every +/// contract a file assumes must be established by the verification of its +/// definition in another file. Prints each proof that rests on one that is +/// not, and returns how many. +unsigned checkContracts(const std::vector &Paths, + llvm::raw_ostream &OS); + /// Verifies the translation unit. In a run over several files /// (Opts.CrossFile), the results wait for CrossFileRun::finish, and the /// result is the file's as far as it alone decides. From 0977359a5c81e5658f81b9fe8f8820075337f0c4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:51 +0530 Subject: [PATCH 72/86] verify: Record a file's contracts for the check of files verified apart, and check the records together. --- clang/lib/Verify/Driver/Verifier.cpp | 288 ++++++++++++++++++++++----- 1 file changed, 240 insertions(+), 48 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 853d54300a..5b4be1d8c7 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -2886,6 +2886,9 @@ class Verifier { std::set Assumes; }; std::map DefinedContracts; + /// Where each function is declared, by its name, for the records of + /// --contracts-out. + std::map DeclLocOf; /// Where the verification of each reported function spent its time, in /// nanoseconds, and of the run, for --time-report. struct FunctionTime { @@ -3977,7 +3980,7 @@ class Verifier { Diags.push_back({VerifyDiagnostic::Trusted, Fn->Name + " (contract assumed, not verified)", Fn->DeclLoc, Fn->Name}); - else if (!Fn->UnsupportedConstruct) { + else if (!Fn->UnsupportedConstruct && Opts.ContractsOut.empty()) { Diags.push_back( {VerifyDiagnostic::Warning, Fn->Name + " has a contract but no definition, so its callers " @@ -5370,7 +5373,7 @@ class Verifier { continue; // In a run over several files, a contract declared here without a // definition holds for now: another file may verify it. - if (Opts.CrossFile && Fn->IsExternalContract && + if (deferredContracts() && Fn->IsExternalContract && !Fn->UnsupportedConstruct && !Fn->IsProof) { Externals.emplace(Fn->Identity, Fn->Name); continue; @@ -5747,7 +5750,7 @@ class Verifier { // declared here without a definition that its callees' contracts rest // on, through the contracts verified here; each contract verified here // is offered to the other files with what it rests on. - if (Opts.CrossFile) { + if (deferredContracts()) { std::map> VerdictsOf; for (const auto &[Index, Identity, Callees] : CallDependencies) VerdictsOf[Identity].push_back(Index); @@ -5769,6 +5772,7 @@ class Verifier { } } for (const auto &Fn : Functions) { + DeclLocOf.emplace(Fn->Name, Fn->DeclLoc); if (Fn->IsSpec || Fn->IsProof || Fn->IsExternalContract || Fn->Uninterpreted || !ContractTexts.count(Fn->Identity)) continue; @@ -6394,6 +6398,76 @@ class Verifier { D.K == VerifyDiagnostic::Exported)); } + /// A contract declared without a definition waits for the files verified + /// with this one, in one run or by checkContracts. + bool deferredContracts() const { + return Opts.CrossFile || !Opts.ContractsOut.empty(); + } + + /// For checkContracts: tags each proof that rests on contracts declared + /// without a definition ([assumes=...]), and writes what this file + /// verifies and assumes to Opts.ContractsOut. + bool recordContracts() { + auto key = [&](const std::string &Identity) { + auto It = ContractTexts.find(Identity); + return Identity + "\n" + (It != ContractTexts.end() ? It->second : ""); + }; + const SourceManager &SM = Ctx.getSourceManager(); + const std::string File = + std::string(SM.getFileEntryRefForID(SM.getMainFileID())->getName()); + llvm::json::Array Defined; + for (const auto &[Identity, Contract] : DefinedContracts) { + llvm::json::Array Assumes; + for (const std::string &Assumed : Contract.Assumes) + Assumes.push_back(key(Assumed)); + Defined.push_back( + llvm::json::Object{{"key", key(Identity)}, + {"name", Contract.Name}, + {"established", Contract.Established}, + {"assumes", std::move(Assumes)}}); + } + llvm::json::Array Proofs; + for (const auto &[Index, Assumed] : ExternalOf) { + VerifyDiagnostic &D = Diags[Index]; + if (Assumed.empty() || !D.isProof()) + continue; + llvm::json::Array Assumes; + std::string Names; + for (const std::string &Identity : Assumed) { + Assumes.push_back(llvm::json::Object{{"key", key(Identity)}, + {"name", Externals.at(Identity)}}); + Names += (Names.empty() ? "" : ",") + Externals.at(Identity); + } + D.Message += " [assumes=" + Names + "]"; + std::string Location; + SourceLocation Loc = D.Loc; + if (Loc.isInvalid()) + if (auto It = DeclLocOf.find(D.FunctionName); It != DeclLocOf.end()) + Loc = It->second; + if (const PresumedLoc Where = SM.getPresumedLoc(Loc); Where.isValid()) + Location = std::string(Where.getFilename()) + ":" + + std::to_string(Where.getLine()) + ":" + + std::to_string(Where.getColumn()); + Proofs.push_back(llvm::json::Object{{"function", D.FunctionName}, + {"location", Location}, + {"assumes", std::move(Assumes)}}); + } + llvm::json::Object Record{{"schema", "cppverify.contracts/1"}, + {"file", File}, + {"defined", std::move(Defined)}, + {"proofs", std::move(Proofs)}}; + std::error_code EC; + llvm::raw_fd_ostream Out(Opts.ContractsOut, EC, llvm::sys::fs::OF_Text); + if (EC) { + Diags.push_back( + {VerifyDiagnostic::Error, + "cannot write " + Opts.ContractsOut + ": " + EC.message()}); + return false; + } + Out << llvm::json::Value(std::move(Record)) << "\n"; + return true; + } + /// Whether --quiet leaves \p D out: what needs no attention. bool quieted(const VerifyDiagnostic &D) const { return Opts.Quiet && (D.isProof() || D.K == VerifyDiagnostic::Lowered || @@ -6596,82 +6670,200 @@ bool verify::verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS, Opts.CrossFile->State->Files.push_back(std::move(Report)); return Ok; } + if (!Opts.ContractsOut.empty()) + Ok = V.recordContracts() && Ok; V.printDiagnostics(OS); if (Opts.TimeReport) V.printTimeReport(OS); return Ok; } -unsigned CrossFileRun::finish(llvm::raw_ostream &OS, VerifySummary *Summary) { - // A contract is established by its definitions' proofs once the contracts - // they rest on are, starting from none: one that rests on itself through - // other files is not. A contract defined in several files (inline in a - // header) must hold in each. - std::map> Definitions; - for (const CrossFileReport &File : State->Files) - for (const auto &[Key, Contract] : File.Defined) - Definitions[Key].push_back(&Contract); +/// The contracts verified in the files of a run, or in files verified apart, +/// settled together. A contract is established by its definitions' proofs +/// once the contracts they rest on are, starting from none, so one that rests +/// on itself through other files is not; a contract defined in several files +/// (inline in a header) must hold in each. +class ContractSettlement { + std::map> Definitions; std::set Established; - for (bool Changed = true; Changed;) { - Changed = false; - for (const auto &[Key, Contracts] : Definitions) - if (!Established.count(Key) && - llvm::all_of(Contracts, [&](const CrossFileContract *Contract) { - return Contract->Established && - llvm::all_of(Contract->Assumes, [&](const std::string &K) { - return Established.count(K) != 0; - }); - })) { - Established.insert(Key); - Changed = true; - } + + static std::string identityOf(const std::string &Key) { + return Key.substr(0, Key.find('\n') + 1); } - auto describe = [&](const CrossFileReport &File, const std::string &Key) { - auto Name = File.Names.find(Key); - std::string Text = - "the contract of " + (Name != File.Names.end() - ? Name->second - : Key.substr(0, Key.find('\n'))); + +public: + void define(const std::string &Key, const CrossFileContract &Contract) { + Definitions[Key].push_back(Contract); + } + + void settle() { + for (bool Changed = true; Changed;) { + Changed = false; + for (const auto &[Key, Contracts] : Definitions) + if (!Established.count(Key) && + llvm::all_of(Contracts, [&](const CrossFileContract &Contract) { + return Contract.Established && + llvm::all_of(Contract.Assumes, [&](const std::string &K) { + return Established.count(K) != 0; + }); + })) { + Established.insert(Key); + Changed = true; + } + } + } + + bool established(const std::string &Key) const { + return Established.count(Key) != 0; + } + + /// Whether some file defines the function of \p Key, whatever contract its + /// definition is verified against. + bool defined(const std::string &Key) const { + auto It = Definitions.lower_bound(identityOf(Key)); + return It != Definitions.end() && + llvm::StringRef(It->first).starts_with(identityOf(Key)); + } + + /// What a proof that rests on the contract of \p Key, the function \p Name, + /// relies on, when it is not established. + std::string describe(const std::string &Key, const std::string &Name) const { + const std::string Text = "the contract of " + Name; auto Defined = Definitions.find(Key); if (Defined == Definitions.end()) { // A definition verified against another contract does not match. - const std::string Identity = Key.substr(0, Key.find('\n') + 1); for (const auto &[Other, Contracts] : Definitions) - if (llvm::StringRef(Other).starts_with(Identity)) + if (llvm::StringRef(Other).starts_with(identityOf(Key))) return Text + ", which is not established: its definition in " + - Contracts.front()->File + + Contracts.front().File + " is verified against another contract"; return Text + " (no definition; mark it [[cppverify::trusted]] to " "assume it), which is not established"; } - for (const CrossFileContract *Contract : Defined->second) - if (!Contract->Established) - return Text + ", which its verification in " + Contract->File + + for (const CrossFileContract &Contract : Defined->second) + if (!Contract.Established) + return Text + ", which its verification in " + Contract.File + " does not establish"; - return Text + ", whose proof in " + Defined->second.front()->File + + return Text + ", whose proof in " + Defined->second.front().File + " rests in turn on contracts not established"; + } +}; + +unsigned verify::checkContracts(const std::vector &Paths, + llvm::raw_ostream &OS) { + struct Proof { + std::string Function; + std::string Location; + std::vector> Assumes; }; - // Whether some file defines the function of a contract's key, whatever - // contract its definition is verified against. - auto defined = [&](const std::string &Key) { - const std::string Identity = Key.substr(0, Key.find('\n') + 1); - auto It = Definitions.lower_bound(Identity); - return It != Definitions.end() && - llvm::StringRef(It->first).starts_with(Identity); + ContractSettlement Contracts; + std::vector Proofs; + unsigned Errors = 0; + auto strings = [](const llvm::json::Array *Array) { + std::set Strings; + if (Array) + for (const llvm::json::Value &Value : *Array) + if (std::optional String = Value.getAsString()) + Strings.insert(String->str()); + return Strings; + }; + for (const std::string &Path : Paths) { + auto Buffer = llvm::MemoryBuffer::getFile(Path); + if (!Buffer) { + OS << "error: cannot read " << Path << ": " << Buffer.getError().message() + << "\n"; + ++Errors; + continue; + } + llvm::Expected Parsed = + llvm::json::parse((*Buffer)->getBuffer()); + const llvm::json::Object *Record = Parsed ? Parsed->getAsObject() : nullptr; + if (!Record || Record->getString("schema") != "cppverify.contracts/1") { + if (!Parsed) + llvm::consumeError(Parsed.takeError()); + OS << "error: " << Path + << " is not a contracts record (cppverify.contracts/1)\n"; + ++Errors; + continue; + } + const std::string File = + Record->getString("file").value_or(llvm::StringRef(Path)).str(); + if (const llvm::json::Array *Defined = Record->getArray("defined")) + for (const llvm::json::Value &Value : *Defined) { + const llvm::json::Object *Entry = Value.getAsObject(); + if (!Entry || !Entry->getString("key")) + continue; + CrossFileContract Contract; + Contract.Name = Entry->getString("name").value_or("").str(); + Contract.File = File; + Contract.Established = Entry->getBoolean("established").value_or(false); + Contract.Assumes = strings(Entry->getArray("assumes")); + Contracts.define(Entry->getString("key")->str(), Contract); + } + if (const llvm::json::Array *Rests = Record->getArray("proofs")) + for (const llvm::json::Value &Value : *Rests) { + const llvm::json::Object *Entry = Value.getAsObject(); + if (!Entry) + continue; + Proof &P = Proofs.emplace_back(); + P.Function = Entry->getString("function").value_or("").str(); + P.Location = Entry->getString("location").value_or("").str(); + if (const llvm::json::Array *Assumes = Entry->getArray("assumes")) + for (const llvm::json::Value &Assumed : *Assumes) + if (const llvm::json::Object *Contract = Assumed.getAsObject()) + P.Assumes.emplace_back( + Contract->getString("key").value_or("").str(), + Contract->getString("name").value_or("").str()); + } + } + Contracts.settle(); + unsigned Unsettled = 0; + for (const Proof &P : Proofs) { + std::string Missing; + for (const auto &[Key, Name] : P.Assumes) + if (!Contracts.established(Key)) + Missing += + (Missing.empty() ? "" : "; ") + Contracts.describe(Key, Name); + if (Missing.empty()) + continue; + ++Unsettled; + if (!P.Location.empty()) + OS << P.Location << ": "; + OS << "error: the proof of " << P.Function << " relies on " << Missing + << "\n"; + } + OS << "Contracts: " << Proofs.size() + << (Proofs.size() == 1 ? " proof rests" : " proofs rest") + << " on contracts of other files, " << Unsettled << " on one not " + << "established\n"; + return Errors + Unsettled; +} + +unsigned CrossFileRun::finish(llvm::raw_ostream &OS, VerifySummary *Summary) { + ContractSettlement Contracts; + for (const CrossFileReport &File : State->Files) + for (const auto &[Key, Contract] : File.Defined) + Contracts.define(Key, Contract); + Contracts.settle(); + auto describe = [&](const CrossFileReport &File, const std::string &Key) { + auto Name = File.Names.find(Key); + return Contracts.describe(Key, Name != File.Names.end() + ? Name->second + : Key.substr(0, Key.find('\n'))); }; unsigned Failures = 0; for (const CrossFileReport &File : State->Files) { std::vector Demoted(File.Lines.size()); for (size_t I = 0; I != File.Lines.size(); ++I) for (const std::string &Key : File.Lines[I].Assumes) - if (!Established.count(Key)) { + if (!Contracts.established(Key)) { Demoted[I] = true; break; } bool Ok = File.Ok; for (size_t I = 0; I != File.Lines.size(); ++I) { const CrossFileLine &Line = File.Lines[I]; - if (!Line.UnlessDefined.empty() && defined(Line.UnlessDefined)) + if (!Line.UnlessDefined.empty() && Contracts.defined(Line.UnlessDefined)) continue; // A finding rests on the facts of its query, as its proof does. if (Line.FindingOf && Demoted[*Line.FindingOf] && !Line.FoundAtEntry) @@ -6685,7 +6877,7 @@ unsigned CrossFileRun::finish(llvm::raw_ostream &OS, VerifySummary *Summary) { Ok = false; std::string Missing; for (const std::string &Key : Line.Assumes) - if (!Established.count(Key)) + if (!Contracts.established(Key)) Missing += (Missing.empty() ? "" : "; ") + describe(File, Key); std::string Text = Line.Demoted; for (size_t At = Text.find(ContractPlaceholder); At != std::string::npos; From f3465ab3c0c66c048c0eef56ee086fa41f918e2c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:52 +0530 Subject: [PATCH 73/86] verify: Add --contracts-out and --check-contracts. --- clang/tools/cpp-verify/Main.cpp | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index 891e8799e8..50257ca374 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -303,6 +303,19 @@ static cl::opt ListFunctions( "locations, and verify none"), cl::cat(CppVerifyCategory)); +static cl::opt ContractsOut( + "contracts-out", + cl::desc("Write the contracts the file verifies and those it assumes from " + "other files, for --check-contracts"), + cl::value_desc("file"), cl::cat(CppVerifyCategory)); + +static cl::opt CheckContracts( + "check-contracts", + cl::desc("Check that the contracts the given records (--contracts-out, " + "-fverify-contracts-out) assume are established by the " + "verification of their definitions in others"), + cl::cat(CppVerifyCategory)); + static cl::opt TimeReport( "time-report", cl::desc("Report where the run and each function spent their time: " @@ -472,6 +485,7 @@ class VerifyConsumer : public ASTConsumer { VOpts.Verbose = Verbose.getValue(); VOpts.ListFunctions = ListFunctions.getValue(); VOpts.TimeReport = TimeReport.getValue(); + VOpts.ContractsOut = ContractsOut.getValue(); if (Progress != cl::boolOrDefault::BOU_UNSET) VOpts.Progress = Progress == cl::boolOrDefault::BOU_TRUE; VOpts.MaxFailures = MaxFailures.getValue(); @@ -1102,6 +1116,14 @@ int main(int argc, const char **argv) { CommonOptionsParser &OptionsParser = ExpectedParser.get(); if (!resolveOptions(!ObligationIn.empty())) return 1; + if (CheckContracts) + return verify::checkContracts(OptionsParser.getSourcePathList(), + llvm::outs()) != 0; + if (!ContractsOut.empty() && OptionsParser.getSourcePathList().size() != 1) { + llvm::errs() << "error: --contracts-out records one file; a run over " + "several files settles their contracts itself\n"; + return 1; + } if (!ObligationIn.empty()) { const std::vector &Sources = OptionsParser.getSourcePathList(); if (Sources.size() != 1 || Sources.front() != ReplayPlaceholder) { From 0ff770e4f02dbcac04b3783ec8267b1768ce0df9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:52 +0530 Subject: [PATCH 74/86] test: Files verified apart record their contracts, and the check settles the records. --- .../Verify/suite/contracts_link_check.test | 61 +++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 clang/test/Verify/suite/contracts_link_check.test diff --git a/clang/test/Verify/suite/contracts_link_check.test b/clang/test/Verify/suite/contracts_link_check.test new file mode 100644 index 0000000000..db269ac4ee --- /dev/null +++ b/clang/test/Verify/suite/contracts_link_check.test @@ -0,0 +1,61 @@ +# Files verified apart (separate cpp-verify runs, or clang++ compiling each +# object) record the contracts they verify and those they assume from other +# files; --check-contracts settles them together, as one run over the files +# does, and fails for each proof whose assumed contract is not established. +# +# RUN: rm -rf %t && mkdir -p %t +# RUN: %cpp-verify --jobs=1 --contracts-out=%t/a.json %S/Inputs/across/src/a.cpp \ +# RUN: -- -I%S/Inputs/across/include 2>&1 | FileCheck %s --check-prefix=APART --implicit-check-not=warning: +# RUN: not %cpp-verify --jobs=1 --contracts-out=%t/wrong.json %S/Inputs/across/src/mathx.cpp \ +# RUN: -- -I%S/Inputs/across/include -DBUG=101 > /dev/null 2>&1 +# RUN: %cpp-verify --jobs=1 --contracts-out=%t/right.json %S/Inputs/across/src/mathx.cpp \ +# RUN: -- -I%S/Inputs/across/include -DBUG=100 > /dev/null 2>&1 +# RUN: not %cpp-verify --check-contracts %t/a.json %t/wrong.json 2>&1 \ +# RUN: | FileCheck %s --check-prefix=WRONG +# RUN: %cpp-verify --check-contracts %t/a.json %t/right.json 2>&1 \ +# RUN: | FileCheck %s --check-prefix=RIGHT +# RUN: not %cpp-verify --check-contracts %t/a.json 2>&1 \ +# RUN: | FileCheck %s --check-prefix=MISSING +# +# Through the compiler, each object's record beside it. +# RUN: %clang -std=c++17 -fverify-contracts -fverify-contracts-out=%t/a.o.cppverify \ +# RUN: -c %S/Inputs/across/src/a.cpp -o %t/a.o -I%S/Inputs/across/include 2>&1 \ +# RUN: | FileCheck %s --check-prefix=APART +# RUN: %clang -std=c++17 -fverify-contracts -fverify-contracts-out=%t/m.o.cppverify \ +# RUN: -c %S/Inputs/across/src/mathx.cpp -o %t/m.o -I%S/Inputs/across/include -DBUG=100 +# RUN: %cpp-verify --check-contracts %t/a.o.cppverify %t/m.o.cppverify 2>&1 \ +# RUN: | FileCheck %s --check-prefix=RIGHT +# RUN: not %clang -std=c++17 -fverify-contracts -fverify-contracts-out=%t/w.o.cppverify \ +# RUN: -c %S/Inputs/across/src/mathx.cpp -o %t/w.o -I%S/Inputs/across/include -DBUG=101 > /dev/null 2>&1 +# RUN: not %cpp-verify --check-contracts %t/a.o.cppverify %t/w.o.cppverify 2>&1 \ +# RUN: | FileCheck %s --check-prefix=WRONG +# +# Contracts whose proofs rest on each other establish nothing. +# RUN: %cpp-verify --jobs=1 --contracts-out=%t/ping.json %S/Inputs/across/src/ping.cpp -- > /dev/null 2>&1 +# RUN: %cpp-verify --jobs=1 --contracts-out=%t/pong.json %S/Inputs/across/src/pong.cpp -- > /dev/null 2>&1 +# RUN: not %cpp-verify --check-contracts %t/ping.json %t/pong.json 2>&1 \ +# RUN: | FileCheck %s --check-prefix=CYCLE +# +# RUN: not %cpp-verify --check-contracts %S/Inputs/across/src/a.cpp 2>&1 \ +# RUN: | FileCheck %s --check-prefix=NOT-RECORD +# RUN: not %cpp-verify --contracts-out=%t/both.json %S/Inputs/across/src/a.cpp \ +# RUN: %S/Inputs/across/src/mathx.cpp -- 2>&1 | FileCheck %s --check-prefix=SEVERAL + +A proof that rests on a contract of another file says so. +APART: Verified: scaled [backend=z3] [assumes=clamp100] +APART-NEXT: Verified: twice_scaled [backend=z3] [assumes=clamp100] + +WRONG: a.cpp:3:5: error: the proof of scaled relies on the contract of clamp100, which its verification in {{.*}}mathx.cpp does not establish +WRONG-NEXT: a.cpp:9:5: error: the proof of twice_scaled relies on the contract of clamp100, which its verification in {{.*}}mathx.cpp does not establish +WRONG-NEXT: Contracts: 2 proofs rest on contracts of other files, 2 on one not established + +RIGHT: Contracts: 2 proofs rest on contracts of other files, 0 on one not established + +MISSING: a.cpp:3:5: error: the proof of scaled relies on the contract of clamp100 (no definition; mark it {{\[\[cppverify::trusted\]\]}} to assume it), which is not established + +CYCLE: ping.cpp:5:5: error: the proof of ping relies on the contract of pong, whose proof in {{.*}}pong.cpp rests in turn on contracts not established +CYCLE-NEXT: pong.cpp:5:5: error: the proof of pong relies on the contract of ping, whose proof in {{.*}}ping.cpp rests in turn on contracts not established + +NOT-RECORD: error: {{.*}}a.cpp is not a contracts record (cppverify.contracts/1) + +SEVERAL: error: --contracts-out records one file; a run over several files settles their contracts itself From 5bcad91b1a7e0c6cefcc1e36b24dde3bf178b3ff Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:53 +0530 Subject: [PATCH 75/86] docs: Describe the check of contracts across files verified apart. --- website/source/language/functions-loops.rst | 23 +++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index e49fea9826..f82e325f61 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -190,8 +190,27 @@ file is verified, then printed in the order the files are given. - A trusted declaration stays an assumption, with ``[trusts=...]`` on what relies on it; only its definition, where it is verified, can find a wrong contract. -- Files verified in separate runs, as in a build that verifies each object, - do not settle their contracts yet. + +Files verified apart, as a build verifies each object, settle their +contracts with a check: each file records what it verifies and what it +assumes, and ``cpp-verify --check-contracts`` settles the records as one run +does. A proof that rests on a contract of another file says so, as +``[assumes=clamp100]``, and the warning that the contract has no definition +is not printed: + +.. code-block:: text + + $ clang++ -fverify-contracts -fverify-contracts-out=a.o.cppverify -c src/a.cpp -o a.o -Iinclude + Verified: scaled [backend=z3] [assumes=clamp100] + $ clang++ -fverify-contracts -fverify-contracts-out=mathx.o.cppverify -c src/mathx.cpp -o mathx.o -Iinclude + include/mathx.h:2:42: error: verification failed: clamp100 [...] + $ cpp-verify --check-contracts a.o.cppverify mathx.o.cppverify + src/a.cpp:3:5: error: the proof of scaled relies on the contract of clamp100, which its verification in src/mathx.cpp does not establish + Contracts: 1 proof rests on contracts of other files, 1 on one not established + +``cpp-verify --contracts-out=FILE`` records one file the same way. The check +exits with a non-zero status when a proof relies on a contract not +established: run it as a build's last step, beside the link. An uncontracted, non-recursive, loop-free ``constexpr`` definition may be lifted for use in contract expressions; a recursive one used with symbolic From 14a1d388aad7a1c46c1016ea641407833525abf4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:53 +0530 Subject: [PATCH 76/86] docs: Describe --contracts-out and --check-contracts. --- website/source/language/tooling.rst | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index a9fb5fd4b1..9908336b77 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -15,6 +15,8 @@ Standalone verifier cpp-verify --time-report file.cpp cpp-verify file.cpp -- -I include -DNDEBUG cpp-verify src/a.cpp src/mathx.cpp -- -I include + cpp-verify --contracts-out=a.cppverify src/a.cpp -- -I include + cpp-verify --check-contracts a.cppverify mathx.cppverify cpp-verify --backend=z3 file.cpp cpp-verify --backend=cvc5 file.cpp cpp-verify --backend=portfolio file.cpp @@ -50,6 +52,17 @@ for a proof once its definition's verification in another file establishes it (see :doc:`functions-loops`). Their results are printed once every file is verified, in the order given. +Files verified apart record their contracts instead: +``--contracts-out=FILE`` (or ``clang++ -fverify-contracts +-fverify-contracts-out=FILE``) writes a ``cppverify.contracts/1`` record of +the contracts the file verifies, whether it establishes each and on which +contracts of other files that rests, and of its proofs that rest on +contracts of other files, which say so (``[assumes=f]``). +``cpp-verify --check-contracts RECORD...`` settles the records and prints +each proof that relies on a contract not established, at the proof's +function, then a line that counts them; its exit status is non-zero when +there is one. + Input files and compiler errors ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ From d3415add9e1aa040bafb46f58c1156e47945dcd6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:54 +0530 Subject: [PATCH 77/86] docs: Note the check of files verified apart in the limitations. --- website/source/language/limitations.rst | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index a3577b91de..4ee58a1948 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -674,8 +674,9 @@ integers (:doc:`functions-loops`), and any other of its functions is an error naming it. An uncontracted call fails closed; a contract is assumed only when it is marked ``[[cppverify::trusted]]``, or, in one run over several files, once the verification of its definition in another of them -establishes it (:doc:`functions-loops`); files verified in separate runs do -not settle their contracts yet. Contracts are not saved in precompiled +establishes it, and for files verified apart once +``cpp-verify --check-contracts`` finds it established +(:doc:`functions-loops`). Contracts are not saved in precompiled headers: a function declared in a PCH has no contract for the verifier, so a contracted function that calls it fails closed (``call to function without a verification contract``). From 6bbf01cd439bd9106c65919cf50a6e8d597b5cfd Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:54 +0530 Subject: [PATCH 78/86] docs: Note the contracts check in the 0.2.0 release notes. --- website/source/release-notes.rst | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 40c915bd02..bb81c0be47 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -505,7 +505,11 @@ of the definition, which inherited the mark, so a wrong body was never checked. Now one run over several files settles such a contract: a proof that rests on it stands once the verification of its definition in another file establishes it, and is ``Unresolved`` with ``callee.contract`` -otherwise, naming the file. A definition is trusted only by a mark of its +otherwise, naming the file. Files verified apart, as a build verifies each +object, record their contracts (``clang++ -fverify-contracts-out=FILE``, +``cpp-verify --contracts-out=FILE``), and ``cpp-verify --check-contracts`` +settles the records the same way, failing for each proof whose assumed +contract is not established. A definition is trusted only by a mark of its own, so a trusted header declaration no longer hides it (:doc:`language/functions-loops`). From a0ec72879f3c3bacc69d92d9fc8bf7783b63686c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:54 +0530 Subject: [PATCH 79/86] docs: Point to the contracts check in the book's modular calls. --- .../source/book/part-ii/ch17-backends-modular-calls.rst | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst index 971f0301d3..9d4ba95f2c 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -1310,9 +1310,11 @@ Where the definition is in another file, verify the files together: ``cpp-verify src/a.cpp src/mathx.cpp -- -Iinclude``. The run settles the contract a header declares against the verification of its definition, so ``a.cpp``'s callers of ``clamp100`` are verified when ``mathx.cpp``'s body -meets the contract, and ``Unresolved`` when it does not. Mark a header's -declaration trusted only for a definition outside the program: on the -definition, which inherits the mark, the body is still verified. +meets the contract, and ``Unresolved`` when it does not. A build that verifies each object +records them instead (``-fverify-contracts-out=FILE``) and checks the +records together at the end (``cpp-verify --check-contracts``). Mark a +header's declaration trusted only for a definition outside the program: on +the definition, which inherits the mark, the body is still verified. The same boundary exists in other verifiers. Verus assumes the specification of a function marked ``#[verifier::external_body]``. Frama-C assumes the From 7aac589c911bc1e33c8bb9dca4dc07d54242ad94 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:55 +0530 Subject: [PATCH 80/86] docs: List --contracts-out and --check-contracts 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 0117644477..377199a3ff 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 function spent their time (lowering, solving, induction, certification, confirmation), the busiest function first; on a terminal a progress line counts the functions done (``--progress`` shows it anywhere) +- ``cpp-verify --contracts-out=FILE`` and ``clang++ -fverify-contracts-out=FILE`` + — record the contracts a file verifies and those it assumes from other + files; ``cpp-verify --check-contracts RECORD...`` checks the records + together (see :doc:`ch17-backends-modular-calls`) - ``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 c1da9c734d9ec46cf3b13fa82edf7eaa43e0bd36 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:55 +0530 Subject: [PATCH 81/86] docs: Design the check of contracts across files verified apart. --- docs/DESIGN.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index d98d67279f..c128a9777d 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -158,7 +158,13 @@ through the file's own contracts, stands once the verification of its definition in another file establishes it (a contract established only through other files' contracts once those are, starting from none), and is `Unresolved` with `callee.contract` otherwise. A declaration matches a -definition with the same function and the same contract as written. A trusted contract writes only +definition with the same function and the same contract as written. Files +verified apart (a build verifying each object) record what they verify and +assume (`--contracts-out`, `-fverify-contracts-out`): such a contract holds +there for now, a proof that rests on it says so (`[assumes=f]`), and +`cpp-verify --check-contracts` settles the records as one run does, failing +for each proof whose assumed contract is not established, as the plan's +link check. A trusted contract writes only its `cppverify::modifies` footprints; without them it writes nothing through a pointer or reference to const, and is taken to write the whole heap through a mutable one (see `cppverify::modifies` below). From 8accc5a22ee6c88449b10788d8f97a69fe57a104 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 21:04:55 +0530 Subject: [PATCH 82/86] docs: Describe how files verified apart record and check their contracts. --- docs/ARCHITECTURE.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index d3b36bb28b..e4959d9b4b 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -2501,7 +2501,17 @@ again where it is used. file's lines with the demoted form where a contract a proof rests on is not established, drops the warning of a contract some file defines and the findings of a demoted proof (but those of the entry state), and - counts the files that do not succeed; + counts the files that do not succeed. The settlement is + `ContractSettlement`, shared with the check of files verified apart: + with `VerifyOptions::ContractsOut` (`--contracts-out`, and + `-fverify-contracts-out` through `startCppVerifyAsync` in the compile + path) a file's externals are provisional the same way, each proof that + rests on them gets `[assumes=f]`, and `recordContracts` writes a + `cppverify.contracts/1` JSON record of the contracts it verifies (key, + name, established, assumes) and of its proofs that rest on externals + (function, the location of its declaration, the contracts). + `checkContracts` (`--check-contracts`) reads the records, settles them, + and prints each proof whose assumed contract is not established; - `[trusts=...]` lists the trusted contracts a proof uses, closed transitively over verified callees (JSON `"trusts"`); - one fixpoint settles the reasons: a verdict relying on a spec whose From 20a8d3f5fd8b799697bdc7855b84238aa148c678 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 06:42:08 +0530 Subject: [PATCH 83/86] 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 84/86] 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 From f4f704b8ba9ff36e3484c0972786ac40db72a1dc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 06:42:54 +0530 Subject: [PATCH 85/86] test: Check that a failed invariant's search for an execution ends at once in confirmation_invariants.cpp. --- .../Verify/suite/confirmation_invariants.cpp | 32 +++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 clang/test/Verify/suite/confirmation_invariants.cpp diff --git a/clang/test/Verify/suite/confirmation_invariants.cpp b/clang/test/Verify/suite/confirmation_invariants.cpp new file mode 100644 index 0000000000..979a3b47ec --- /dev/null +++ b/clang/test/Verify/suite/confirmation_invariants.cpp @@ -0,0 +1,32 @@ +// RUN: not %cpp-verify --jobs=4 --timeout=5000 --time-report %s -- 2>&1 | FileCheck %s +// +// Unrolling drops the loops' invariants and measures, so a failure of one +// has no copy at any bound: once the loops are unrolled once and no copy +// has appeared, the search for an execution that fails it stops, instead of +// solving every check at every bound until its time runs out (6.5 s at +// --timeout=5000 for this function, 31 s at the default 30000). + +namespace cv = cppverify; + +cv::spec bool valid(const int *p, int n) { return true; } + +void reversed_copy(const int *a, int *out, int n) + cv::pre(n >= 0 && valid(a, n) && valid(out, n)) + cv::modifies(*out) + cv::post(cv::forall(i, 0, n, out[i] == a[i])) +{ + int i = 0; + while (i < n) + cv::invariant(0 <= i && i <= n) + cv::invariant(cv::forall(j, 0, i, out[j] == a[j])) + cv::decreases(n - i) + { + out[i] = a[n - 1 - i]; + i = i + 1; + } +} +// CHECK: verification failed: reversed_copy {{.*}}invariant-preserved +// CHECK: note: the counterexample's state at the loop at {{[0-9]+}}:3 is any state its invariants allow +// CHECK-NOT: fails this check +// CHECK: total lowering solving induction certification confirmation function +// CHECK-NEXT: {{ *[0-9.]+ +[0-9.]+ +[0-9.]+ +[0-9.]+ +[0-9.]+ +0\.[0-9]+}} reversed_copy From 7e9f394a64a038257240f36a6bfeeb9b4a883388 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 08:21:23 +0530 Subject: [PATCH 86/86] test: Fail confirmation_invariants.cpp's invariant at a bound the solver finds at once. --- .../Verify/suite/confirmation_invariants.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/clang/test/Verify/suite/confirmation_invariants.cpp b/clang/test/Verify/suite/confirmation_invariants.cpp index 979a3b47ec..6900c3ccc6 100644 --- a/clang/test/Verify/suite/confirmation_invariants.cpp +++ b/clang/test/Verify/suite/confirmation_invariants.cpp @@ -3,30 +3,32 @@ // Unrolling drops the loops' invariants and measures, so a failure of one // has no copy at any bound: once the loops are unrolled once and no copy // has appeared, the search for an execution that fails it stops, instead of -// solving every check at every bound until its time runs out (6.5 s at -// --timeout=5000 for this function, 31 s at the default 30000). +// solving every check at every bound until its time runs out (5.8 s at +// --timeout=5000 for this function, 30 s at the default 30000). namespace cv = cppverify; cv::spec bool valid(const int *p, int n) { return true; } -void reversed_copy(const int *a, int *out, int n) +// The copy is right; the first invariant's bound on i is not, and only an +// invariant states it. +void bounded_copy(const int *a, int *out, int n) cv::pre(n >= 0 && valid(a, n) && valid(out, n)) cv::modifies(*out) cv::post(cv::forall(i, 0, n, out[i] == a[i])) { int i = 0; while (i < n) - cv::invariant(0 <= i && i <= n) + cv::invariant(0 <= i && i <= n && i <= 8) cv::invariant(cv::forall(j, 0, i, out[j] == a[j])) cv::decreases(n - i) { - out[i] = a[n - 1 - i]; + out[i] = a[i]; i = i + 1; } } -// CHECK: verification failed: reversed_copy {{.*}}invariant-preserved +// CHECK: verification failed: bounded_copy {{.*}}invariant-preserved // CHECK: note: the counterexample's state at the loop at {{[0-9]+}}:3 is any state its invariants allow // CHECK-NOT: fails this check // CHECK: total lowering solving induction certification confirmation function -// CHECK-NEXT: {{ *[0-9.]+ +[0-9.]+ +[0-9.]+ +[0-9.]+ +[0-9.]+ +0\.[0-9]+}} reversed_copy +// CHECK-NEXT: {{ *[0-9.]+ +[0-9.]+ +[0-9.]+ +[0-9.]+ +[0-9.]+ +0\.[0-9]+}} bounded_copy