Lock every source lookup made while functions are verified at once

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<VerifyDiagnostic> 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<std::recursive_mutex> 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<std::recursive_mutex> 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<FunctionRun> 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<VerifyDiagnostic> &Diags = Run.Diags;
@@ -3783,6 +3786,7 @@ class Verifier {
       auto failureNotes = [&](const VFunction &F, const VerifyResult &Failure) {
         std::vector<std::string> Notes;
         auto at = [&](SourceLocation Loc) {
+          std::lock_guard<std::recursive_mutex> 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<std::mutex> 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

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

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