From c6dfe384b02126355542fb58736ae551795382ef Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 29 Oct 2026 14:34:06 +0530 Subject: [PATCH 1/4] verify: Take the source lock in every source lookup made while functions are verified at once. --- clang/lib/Verify/Driver/Verifier.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 2b32533561..e176a6849b 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -2881,6 +2881,9 @@ class Verifier { ASTContext &Ctx; VerifyOptions Opts; llvm::raw_ostream *DumpOS = nullptr; + /// The source manager caches its last lookups, so every lookup that + /// functions verified at once make holds this lock. + mutable std::recursive_mutex SourceLock; std::vector Diags; /// Each function's source and that of the helpers inlined into it, by /// identity (VFunction::Extent, InlinedExtents). @@ -3014,6 +3017,7 @@ class Verifier { /// when Loc has none. ObligationSource sourceOf(SourceLocation Loc, SourceLocation BeginLoc, SourceLocation EndLoc) const { + std::lock_guard Guard(SourceLock); const SourceManager &SourceMgr = Ctx.getSourceManager(); ObligationSource Found; if (!Loc.isValid()) @@ -3070,6 +3074,7 @@ class Verifier { } void annotateObligationSources(ObligationModule &Module) { + std::lock_guard Guard(SourceLock); auto annotateSource = [&](SourceLocation Loc, SourceLocation BeginLoc, SourceLocation EndLoc, ObligationSource &Source) { ObligationSource Found = sourceOf(Loc, BeginLoc, EndLoc); @@ -3689,8 +3694,6 @@ class Verifier { uint64_t Confirmed = 0; }; std::vector Runs(Functions.size()); - // The source manager caches its last line lookup. - std::mutex SourceLock; auto verifyFunction = [&](size_t Index) { FunctionRun &Run = Runs[Index]; std::vector &Diags = Run.Diags; @@ -3783,6 +3786,7 @@ class Verifier { auto failureNotes = [&](const VFunction &F, const VerifyResult &Failure) { std::vector Notes; auto at = [&](SourceLocation Loc) { + std::lock_guard Guard(SourceLock); const PresumedLoc Where = Ctx.getSourceManager().getPresumedLoc( Ctx.getSourceManager().getFileLoc(Loc)); return Where.isValid() ? std::to_string(Where.getLine()) + ":" + @@ -4011,10 +4015,6 @@ class Verifier { Run.Archive += *Record; return llvm::Error::success(); }; - auto annotateObligationSources = [&](ObligationModule &Module) { - std::lock_guard Guard(SourceLock); - this->annotateObligationSources(Module); - }; // A contract must be defined where it is evaluated (Dafny's // well-formedness check): its preconditions in order, and the // postconditions of a function whose body is not verified in every From aec8b8043d974228e5dd0221f453b4c1ed5bc44d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 29 Oct 2026 14:34:07 +0530 Subject: [PATCH 2/4] test: Fail sixteen functions at once through loops, so their failure notes look up sources together. --- .../Verify/suite/parallel_failure_notes.cpp | 314 ++++++++++++++++++ 1 file changed, 314 insertions(+) create mode 100644 clang/test/Verify/suite/parallel_failure_notes.cpp diff --git a/clang/test/Verify/suite/parallel_failure_notes.cpp b/clang/test/Verify/suite/parallel_failure_notes.cpp new file mode 100644 index 0000000000..5fe0b11ac2 --- /dev/null +++ b/clang/test/Verify/suite/parallel_failure_notes.cpp @@ -0,0 +1,314 @@ +// RUN: not %cpp-verify --jobs=4 %s -- 2>&1 | FileCheck %s +// +// Functions verified at once each fail with a counterexample through a loop +// whose invariant is too weak, so the notes of each failure unroll its loop +// bound by bound, each bound's module annotated with its sources, beside the +// other functions' lookups. Every lookup takes the verifier's source lock: +// the source manager caches its last lookups, and these raced on that cache. +// Under ThreadSanitizer, without the lock, most runs report the race. + +namespace cv = cppverify; + +int steps_of_1(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 1) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 1) + cv::decreases(n - i) + { + i = i + 1; + s = s + 1; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_1 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_2(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 2) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 2) + cv::decreases(n - i) + { + i = i + 1; + s = s + 2; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_2 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_3(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 3) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 3) + cv::decreases(n - i) + { + i = i + 1; + s = s + 3; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_3 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_4(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 4) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 4) + cv::decreases(n - i) + { + i = i + 1; + s = s + 4; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_4 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_5(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 5) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 5) + cv::decreases(n - i) + { + i = i + 1; + s = s + 5; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_5 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_6(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 6) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 6) + cv::decreases(n - i) + { + i = i + 1; + s = s + 6; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_6 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_7(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 7) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 7) + cv::decreases(n - i) + { + i = i + 1; + s = s + 7; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_7 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_8(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 8) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 8) + cv::decreases(n - i) + { + i = i + 1; + s = s + 8; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_8 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_9(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 9) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 9) + cv::decreases(n - i) + { + i = i + 1; + s = s + 9; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_9 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_10(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 10) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 10) + cv::decreases(n - i) + { + i = i + 1; + s = s + 10; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_10 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_11(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 11) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 11) + cv::decreases(n - i) + { + i = i + 1; + s = s + 11; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_11 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_12(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 12) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 12) + cv::decreases(n - i) + { + i = i + 1; + s = s + 12; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_12 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_13(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 13) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 13) + cv::decreases(n - i) + { + i = i + 1; + s = s + 13; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_13 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_14(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 14) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 14) + cv::decreases(n - i) + { + i = i + 1; + s = s + 14; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_14 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_15(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 15) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 15) + cv::decreases(n - i) + { + i = i + 1; + s = s + 15; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_15 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof + +int steps_of_16(int n) + cv::pre(0 <= n && n <= 9) + cv::post(cv::result == n * 16) +{ + int i = 0; + int s = 0; + while (i < n) + cv::invariant(0 <= i && s == i * 16) + cv::decreases(n - i) + { + i = i + 1; + s = s + 16; + } + return s; +} +// CHECK: parallel_failure_notes.cpp:[[@LINE-13]]:23: error: verification failed: steps_of_16 [postcondition] +// CHECK: note: the counterexample's state at the loop at [[@LINE-10]]: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 9 iterations, and unrolling proves it there; the loops' invariants are too weak for an unbounded proof From 9dd2ea44f1567d9eeeaf361e1a481738db85df5e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 29 Oct 2026 14:34:07 +0530 Subject: [PATCH 3/4] docs: Say which source lookups take the source lock in ARCHITECTURE.md. --- docs/ARCHITECTURE.md | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index c45ba8c436..25b10fec87 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -3051,9 +3051,14 @@ interrupt function. Every solver is created with Z3's `ctrl_c` parameter off: otherwise each check swaps Z3's own SIGINT handler in, Z3 keeps the handlers of concurrent checks in one unsynchronized stack, and Ctrl-C ran the handler of a finished check (a crash report, then a run that went on). -Source-location annotation takes a lock, since -the source manager caches its last lookup. Lean stays serial, and the -compile-time verifier keeps a single job. +Every source lookup made while functions are verified at once takes one +lock, `Verifier::SourceLock`, in `sourceOf`, `annotateObligationSources`, and +the notes of a failure, since the source manager caches its last lookups: +before 0.2 the notes of a failure whose counterexample passes through a loop, +which unroll the loop and annotate each bound's module, and the fallback of +a failure's place looked up sources without it, a data race that +ThreadSanitizer found (`suite/parallel_failure_notes.cpp`). Lean stays +serial, and the compile-time verifier keeps a single job. cvc5 execution resolves an explicit `--cvc5-path` or searches `PATH`, writes one bounded temporary SMT-LIB2 query, invokes the executable without a shell under From b1c58df3098d82c614abc398d8803723caff72f1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 29 Oct 2026 14:34:07 +0530 Subject: [PATCH 4/4] docs: Add the source lookups of parallel failures to the release notes. --- website/source/release-notes.rst | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index a40d93294d..186e81a758 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -544,6 +544,15 @@ are errors at the statement (:doc:`language/functions-loops`). Running cpp-verify ~~~~~~~~~~~~~~~~~~ +**Source lookups from parallel failures.** With more than one job, a failure +whose counterexample passes through a loop gets notes from unrolling the +loop, and those looked up source lines without the lock that the other +lookups take, while other functions looked up theirs; so did a failure's +place when its source was not recorded. The source manager caches its last +lookup, so this was a data race on that cache, which ThreadSanitizer found +and which could misplace a note or a check. Every lookup made while functions +are verified at once now takes the lock. + **Induction for lemmas that time out.** The automatic inductions ran only when unfolding a recursive spec could not settle a claim, so a lemma such as "an order on adjacent elements is an order on all of them" ended