[clang] [clang][analyzer][WIP] Introduce modeling for threading related checkers (PR #109636)

Endre Fülöp via cfe-commits cfe-commits at lists.llvm.org
Sun Oct 6 17:17:32 PDT 2024


https://github.com/gamesh411 updated https://github.com/llvm/llvm-project/pull/109636

>From ed662eeccc0f8b53d431b88bf86ae2a17fe20078 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Endre=20F=C3=BCl=C3=B6p?= <endre.fulop at sigmatechnology.com>
Date: Thu, 3 Oct 2024 18:24:17 +0200
Subject: [PATCH 1/5] Introduce MutexModeling checker

This patch introduces the basic structure for the MutexModeling checker.
It adds the checker definition, creates the MutexModeling.cpp file,
supporting header files, and updates the necessary build files. The
MutexModeling checker will be responsible for modeling mutexlock and
unlock events, removing duplication in BlockInCriticalSectionChecker and
PthreadLockChecker.
---
 .../clang/StaticAnalyzer/Checkers/Checkers.td |   5 +
 .../StaticAnalyzer/Checkers/CMakeLists.txt    |   1 +
 .../StaticAnalyzer/Checkers/MutexModeling.cpp | 773 ++++++++++++++++++
 .../Checkers/MutexModeling/MutexModelingAPI.h | 244 ++++++
 .../MutexModeling/MutexModelingDomain.h       | 126 +++
 .../Checkers/MutexModeling/MutexModelingGDM.h | 169 ++++
 .../MutexModeling/MutexRegionExtractor.h      | 139 ++++
 .../Checkers/PthreadLockChecker.cpp           |   4 +-
 8 files changed, 1460 insertions(+), 1 deletion(-)
 create mode 100644 clang/lib/StaticAnalyzer/Checkers/MutexModeling.cpp
 create mode 100644 clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexModelingAPI.h
 create mode 100644 clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexModelingDomain.h
 create mode 100644 clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexModelingGDM.h
 create mode 100644 clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexRegionExtractor.h

diff --git a/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td b/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
index 349040c15eeb83..fb31011dde84ff 100644
--- a/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
+++ b/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
@@ -219,6 +219,11 @@ def DereferenceChecker : Checker<"NullDereference">,
   ]>,
   Documentation<HasDocumentation>;
 
+def MutexModeling : Checker<"MutexModeling">,
+  HelpText<"Model mutexes lock and unlock events">,
+  Documentation<NotDocumented>,
+  Hidden;
+
 def NonNullParamChecker : Checker<"NonNullParamChecker">,
   HelpText<"Check for null pointers passed as arguments to a function whose "
            "arguments are references or marked with the 'nonnull' attribute">,
diff --git a/clang/lib/StaticAnalyzer/Checkers/CMakeLists.txt b/clang/lib/StaticAnalyzer/Checkers/CMakeLists.txt
index 6da3665ab9a4df..c3987ba76529db 100644
--- a/clang/lib/StaticAnalyzer/Checkers/CMakeLists.txt
+++ b/clang/lib/StaticAnalyzer/Checkers/CMakeLists.txt
@@ -68,6 +68,7 @@ add_clang_library(clangStaticAnalyzerCheckers
   MmapWriteExecChecker.cpp
   MIGChecker.cpp
   MoveChecker.cpp
+  MutexModeling.cpp
   MPI-Checker/MPIBugReporter.cpp
   MPI-Checker/MPIChecker.cpp
   MPI-Checker/MPIFunctionClassifier.cpp
diff --git a/clang/lib/StaticAnalyzer/Checkers/MutexModeling.cpp b/clang/lib/StaticAnalyzer/Checkers/MutexModeling.cpp
new file mode 100644
index 00000000000000..f0e13c5c95e432
--- /dev/null
+++ b/clang/lib/StaticAnalyzer/Checkers/MutexModeling.cpp
@@ -0,0 +1,773 @@
+//===--- MutexModeling.cpp - Modeling of mutexes --------------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// Defines modeling checker for tracking mutex states.
+//
+//===----------------------------------------------------------------------===//
+
+#include "MutexModeling/MutexModelingAPI.h"
+#include "MutexModeling/MutexModelingDomain.h"
+#include "MutexModeling/MutexRegionExtractor.h"
+
+#include "clang/StaticAnalyzer/Core/Checker.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerHelpers.h"
+#include "clang/StaticAnalyzer/Frontend/CheckerRegistry.h"
+#include <memory>
+
+using namespace clang;
+using namespace ento;
+using namespace mutex_modeling;
+
+namespace {
+
+// When a lock is destroyed, in some semantics(like PthreadSemantics) we are not
+// sure if the destroy call has succeeded or failed, and the lock enters one of
+// the 'possibly destroyed' state. There is a short time frame for the
+// programmer to check the return value to see if the lock was successfully
+// destroyed. Before we model the next operation over that lock, we call this
+// function to see if the return value was checked by now and set the lock state
+// - either to destroyed state or back to its previous state.
+
+// In PthreadSemantics, pthread_mutex_destroy() returns zero if the lock is
+// successfully destroyed and it returns a non-zero value otherwise.
+ProgramStateRef resolvePossiblyDestroyedMutex(ProgramStateRef State,
+                                              const MemRegion *LockReg,
+                                              const SymbolRef *LockReturnSym) {
+  const LockStateKind *LockState = State->get<LockStates>(LockReg);
+  // Existence in DestroyRetVal ensures existence in LockMap.
+  // Existence in Destroyed also ensures that the lock state for lockR is either
+  // UntouchedAndPossiblyDestroyed or UnlockedAndPossiblyDestroyed.
+  assert(LockState);
+  assert(*LockState == LockStateKind::UntouchedAndPossiblyDestroyed ||
+         *LockState == LockStateKind::UnlockedAndPossiblyDestroyed);
+
+  ConstraintManager &CMgr = State->getConstraintManager();
+  ConditionTruthVal RetZero = CMgr.isNull(State, *LockReturnSym);
+  if (RetZero.isConstrainedFalse()) {
+    switch (*LockState) {
+    case LockStateKind::UntouchedAndPossiblyDestroyed: {
+      State = State->remove<LockStates>(LockReg);
+      break;
+    }
+    case LockStateKind::UnlockedAndPossiblyDestroyed: {
+      State = State->set<LockStates>(LockReg, LockStateKind::Unlocked);
+      break;
+    }
+    default:
+      llvm_unreachable("Unknown lock state for a lock inside DestroyRetVal");
+    }
+  } else {
+    State = State->set<LockStates>(LockReg, LockStateKind::Destroyed);
+  }
+
+  // Removing the map entry (LockReg, sym) from DestroyRetVal as the lock
+  // state is now resolved.
+  return State->remove<DestroyedRetVals>(LockReg);
+}
+
+ProgramStateRef doResolvePossiblyDestroyedMutex(ProgramStateRef State,
+                                                const MemRegion *MTX) {
+  assert(MTX && "should only be called with a mutex region");
+
+  if (const SymbolRef *Sym = State->get<DestroyedRetVals>(MTX))
+    return resolvePossiblyDestroyedMutex(State, MTX, Sym);
+  return State;
+}
+
+class MutexModeling : public Checker<check::PostCall, check::DeadSymbols,
+                                     check::RegionChanges> {
+public:
+  void checkPostCall(const CallEvent &Call, CheckerContext &C) const;
+
+  void checkDeadSymbols(SymbolReaper &SymReaper, CheckerContext &C) const;
+
+  ProgramStateRef
+  checkRegionChanges(ProgramStateRef State, const InvalidatedSymbols *Symbols,
+                     ArrayRef<const MemRegion *> ExplicitRegions,
+                     ArrayRef<const MemRegion *> Regions,
+                     const LocationContext *LCtx, const CallEvent *Call) const;
+
+private:
+  mutable std::unique_ptr<BugType> BT_initlock;
+
+  // When handling events, NoteTags can be placed on ProgramPoints. This struct
+  // supports returning both the resulting ProgramState and a NoteTag.
+  struct ModelingResult {
+    ProgramStateRef State;
+    const NoteTag *Note = nullptr;
+  };
+
+  ModelingResult handleInit(const EventDescriptor &Event, const MemRegion *MTX,
+                            const CallEvent &Call, ProgramStateRef State,
+                            CheckerContext &C) const;
+  ModelingResult onSuccessfulAcquire(const MemRegion *MTX,
+                                     const CallEvent &Call,
+                                     ProgramStateRef State,
+                                     CheckerContext &C) const;
+  ModelingResult markCritSection(ModelingResult InputState,
+                                 const MemRegion *MTX, const CallEvent &Call,
+                                 CheckerContext &C) const;
+  ModelingResult handleAcquire(const EventDescriptor &Event,
+                               const MemRegion *MTX, const CallEvent &Call,
+                               ProgramStateRef State, CheckerContext &C) const;
+  ModelingResult handleTryAcquire(const EventDescriptor &Event,
+                                  const MemRegion *MTX, const CallEvent &Call,
+                                  ProgramStateRef State,
+                                  CheckerContext &C) const;
+  ModelingResult handleRelease(const EventDescriptor &Event,
+                               const MemRegion *MTX, const CallEvent &Call,
+                               ProgramStateRef State, CheckerContext &C) const;
+  ModelingResult handleDestroy(const EventDescriptor &Event,
+                               const MemRegion *MTX, const CallEvent &Call,
+                               ProgramStateRef State, CheckerContext &C) const;
+  ModelingResult handleEvent(const EventDescriptor &Event, const MemRegion *MTX,
+                             const CallEvent &Call, ProgramStateRef State,
+                             CheckerContext &C) const;
+};
+
+} // namespace
+
+MutexModeling::ModelingResult
+MutexModeling::handleInit(const EventDescriptor &Event, const MemRegion *MTX,
+                          const CallEvent &Call, ProgramStateRef State,
+                          CheckerContext &C) const {
+  ModelingResult Result{State->set<LockStates>(MTX, LockStateKind::Unlocked)};
+
+  const LockStateKind *LockState = State->get<LockStates>(MTX);
+
+  if (!LockState)
+    return Result;
+
+  switch (*LockState) {
+  case (LockStateKind::Destroyed): {
+    Result.State = State->set<LockStates>(MTX, LockStateKind::Unlocked);
+    break;
+  }
+  case (LockStateKind::Locked): {
+    Result.State =
+        State->set<LockStates>(MTX, LockStateKind::Error_DoubleInitWhileLocked);
+    break;
+  }
+  default: {
+    Result.State = State->set<LockStates>(MTX, LockStateKind::Error_DoubleInit);
+    break;
+  }
+  }
+
+  return Result;
+}
+
+MutexModeling::ModelingResult
+MutexModeling::markCritSection(MutexModeling::ModelingResult InputState,
+                               const MemRegion *MTX, const CallEvent &Call,
+                               CheckerContext &C) const {
+  const CritSectionMarker MarkToAdd{Call.getOriginExpr(), MTX};
+  return {InputState.State->add<CritSections>(MarkToAdd),
+          CreateMutexCritSectionNote(MarkToAdd, C)};
+}
+
+MutexModeling::ModelingResult
+MutexModeling::onSuccessfulAcquire(const MemRegion *MTX, const CallEvent &Call,
+                                   ProgramStateRef State,
+                                   CheckerContext &C) const {
+  ModelingResult Result{State};
+
+  const LockStateKind *LockState = State->get<LockStates>(MTX);
+
+  if (!LockState) {
+    Result.State = Result.State->set<LockStates>(MTX, LockStateKind::Locked);
+  } else {
+    switch (*LockState) {
+    case LockStateKind::Unlocked:
+      Result.State = Result.State->set<LockStates>(MTX, LockStateKind::Locked);
+      break;
+    case LockStateKind::Locked:
+      Result.State =
+          Result.State->set<LockStates>(MTX, LockStateKind::Error_DoubleLock);
+      break;
+    case LockStateKind::Destroyed:
+      Result.State = Result.State->set<LockStates>(
+          MTX, LockStateKind::Error_LockDestroyed);
+      break;
+    default:
+      break;
+    }
+  }
+
+  Result = markCritSection(Result, MTX, Call, C);
+  return Result;
+}
+
+MutexModeling::ModelingResult
+MutexModeling::handleAcquire(const EventDescriptor &Event, const MemRegion *MTX,
+                             const CallEvent &Call, ProgramStateRef State,
+                             CheckerContext &C) const {
+
+  switch (Event.Semantics) {
+  case SemanticsKind::PthreadSemantics: {
+    // Assume that the return value was 0.
+    SVal RetVal = Call.getReturnValue();
+    if (auto DefinedRetVal = RetVal.getAs<DefinedSVal>()) {
+      // FIXME: If the lock function was inlined and returned true,
+      // we need to behave sanely - at least generate sink.
+      State = State->assume(*DefinedRetVal, false);
+      assert(State);
+    }
+    // We might want to handle the case when the mutex lock function was
+    // inlined and returned an Unknown or Undefined value.
+    break;
+  }
+  case SemanticsKind::XNUSemantics:
+    // XNU semantics return void on non-try locks.
+    break;
+  default:
+    llvm_unreachable(
+        "Acquire events should have either Pthread or XNU semantics");
+  }
+
+  return onSuccessfulAcquire(MTX, Call, State, C);
+}
+
+MutexModeling::ModelingResult MutexModeling::handleTryAcquire(
+    const EventDescriptor &Event, const MemRegion *MTX, const CallEvent &Call,
+    ProgramStateRef State, CheckerContext &C) const {
+
+  ProgramStateRef LockSucc{State};
+  // Bifurcate the state, and allow a mode where the lock acquisition fails.
+  SVal RetVal = Call.getReturnValue();
+  std::optional<DefinedSVal> DefinedRetVal = RetVal.getAs<DefinedSVal>();
+  // Bifurcating the state is only meaningful if the call was not inlined, but
+  // we can still reason about the return value.
+  if (!C.wasInlined && DefinedRetVal) {
+    ProgramStateRef LockFail;
+    switch (Event.Semantics) {
+    case SemanticsKind::PthreadSemantics:
+      // For PthreadSemantics, a non-zero return value indicates success
+      std::tie(LockFail, LockSucc) = State->assume(*DefinedRetVal);
+      break;
+    case SemanticsKind::XNUSemantics:
+      // For XNUSemantics, a zero return value indicates success
+      std::tie(LockSucc, LockFail) = State->assume(*DefinedRetVal);
+      break;
+    default:
+      llvm_unreachable("Unknown TryLock locking semantics");
+    }
+
+    // This is the bifurcation point in the ExplodedGraph, we do not need to
+    // return the new ExplodedGraph node because we do not plan on building this
+    // lock-failed case path in this checker.
+    C.addTransition(LockFail);
+  }
+
+  if (!LockSucc)
+    LockSucc = State;
+
+  // Pass the state where the locking succeeded onwards.
+  return onSuccessfulAcquire(MTX, Call, LockSucc, C);
+}
+
+MutexModeling::ModelingResult
+MutexModeling::handleRelease(const EventDescriptor &Event, const MemRegion *MTX,
+                             const CallEvent &Call, ProgramStateRef State,
+                             CheckerContext &C) const {
+
+  ModelingResult Result{State};
+
+  const LockStateKind *LockState = Result.State->get<LockStates>(MTX);
+
+  if (!LockState) {
+    Result.State = Result.State->set<LockStates>(MTX, LockStateKind::Unlocked);
+    return Result;
+  }
+
+  if (*LockState == LockStateKind::Unlocked) {
+    Result.State =
+        State->set<LockStates>(MTX, LockStateKind::Error_DoubleUnlock);
+    return Result;
+  }
+
+  if (*LockState == LockStateKind::Destroyed) {
+    Result.State =
+        State->set<LockStates>(MTX, LockStateKind::Error_UnlockDestroyed);
+    return Result;
+  }
+
+  const auto ActiveSections = State->get<CritSections>();
+  const auto MostRecentLockForMTX =
+      llvm::find_if(ActiveSections,
+                    [MTX](auto &&Marker) { return Marker.MutexRegion == MTX; });
+
+  // In a non-empty critical section list, if the most recent lock is for
+  // another mutex, then there is a lock reversal.
+  bool IsLockInversion = MostRecentLockForMTX != ActiveSections.begin();
+
+  // NOTE: IsLockInversion -> !ActiveSections.isEmpty()
+  assert((!IsLockInversion || !ActiveSections.isEmpty()) &&
+         "The existence of an inversion implies that the list is not empty");
+
+  if (IsLockInversion) {
+    Result.State =
+        State->set<LockStates>(MTX, LockStateKind::Error_LockReversal);
+    // Build a new ImmutableList without this element.
+    auto &Factory = Result.State->get_context<CritSections>();
+    llvm::ImmutableList<CritSectionMarker> WithoutThisLock =
+        Factory.getEmptyList();
+    for (auto It = ActiveSections.begin(), End = ActiveSections.end();
+         It != End; ++It) {
+      if (It != MostRecentLockForMTX)
+        WithoutThisLock = Factory.add(*It, WithoutThisLock);
+    }
+    Result.State = Result.State->set<CritSections>(WithoutThisLock);
+    return Result;
+  }
+
+  Result.State = Result.State->set<LockStates>(MTX, LockStateKind::Unlocked);
+  // If there is no lock inversion, we can just remove the last crit section.
+  // NOTE: It should be safe to call getTail on an empty list
+  Result.State = Result.State->set<CritSections>(ActiveSections.getTail());
+
+  return Result;
+}
+
+MutexModeling::ModelingResult
+MutexModeling::handleDestroy(const EventDescriptor &Event, const MemRegion *MTX,
+                             const CallEvent &Call, ProgramStateRef State,
+                             CheckerContext &C) const {
+  ModelingResult Result{State};
+
+  const LockStateKind *LockState = Result.State->get<LockStates>(MTX);
+
+  // PthreadSemantics handles destroy differently due to its return value
+  // semantics
+  if (Event.Semantics == SemanticsKind::PthreadSemantics) {
+    if (!LockState || *LockState == LockStateKind::Unlocked) {
+      SymbolRef Sym = Call.getReturnValue().getAsSymbol();
+      if (!Sym) {
+        Result.State = Result.State->remove<LockStates>(MTX);
+        return Result;
+      }
+      Result.State = Result.State->set<DestroyedRetVals>(MTX, Sym);
+      Result.State = Result.State->set<LockStates>(
+          MTX, LockState && *LockState == LockStateKind::Unlocked
+                   ? LockStateKind::UnlockedAndPossiblyDestroyed
+                   : LockStateKind::UntouchedAndPossiblyDestroyed);
+      return Result;
+    }
+  } else {
+    // For non-PthreadSemantics, we assume destroy always succeeds
+    if (!LockState || *LockState == LockStateKind::Unlocked) {
+      Result.State =
+          Result.State->set<LockStates>(MTX, LockStateKind::Destroyed);
+      return Result;
+    }
+  }
+
+  if (*LockState == LockStateKind::Locked) {
+    Result.State =
+        Result.State->set<LockStates>(MTX, LockStateKind::Error_DestroyLocked);
+    return Result;
+  }
+
+  if (*LockState == LockStateKind::Destroyed) {
+    Result.State =
+        Result.State->set<LockStates>(MTX, LockStateKind::Error_DoubleDestroy);
+    return Result;
+  }
+
+  assert(LockState && *LockState != LockStateKind::Unlocked &&
+         *LockState != LockStateKind::Locked &&
+         *LockState != LockStateKind::Destroyed &&
+         "We can only get here if we came from an error-state to begin with");
+
+  return Result;
+}
+
+MutexModeling::ModelingResult
+MutexModeling::handleEvent(const EventDescriptor &Event, const MemRegion *MTX,
+                           const CallEvent &Call, ProgramStateRef State,
+                           CheckerContext &C) const {
+  assert(MTX && "should only be called with a mutex region");
+
+  State = State->add<MutexEvents>(
+      EventMarker{Event.Kind, Event.Semantics, Event.Library,
+                  Call.getCalleeIdentifier(), Call.getOriginExpr(), MTX});
+
+  switch (Event.Kind) {
+  case EventKind::Init:
+    return handleInit(Event, MTX, Call, State, C);
+  case EventKind::Acquire:
+    return handleAcquire(Event, MTX, Call, State, C);
+  case EventKind::TryAcquire:
+    return handleTryAcquire(Event, MTX, Call, State, C);
+  case EventKind::Release:
+    return handleRelease(Event, MTX, Call, State, C);
+  case EventKind::Destroy:
+    return handleDestroy(Event, MTX, Call, State, C);
+  default:
+    llvm_unreachable("Unknown event kind");
+  }
+}
+
+static const MemRegion *skipStdBaseClassRegion(const MemRegion *Reg) {
+  while (Reg) {
+    const auto *BaseClassRegion = dyn_cast<CXXBaseObjectRegion>(Reg);
+    if (!BaseClassRegion || !isWithinStdNamespace(BaseClassRegion->getDecl()))
+      break;
+    Reg = BaseClassRegion->getSuperRegion();
+  }
+  return Reg;
+}
+
+void MutexModeling::checkPostCall(const CallEvent &Call,
+                                  CheckerContext &C) const {
+  ProgramStateRef State = C.getState();
+  for (auto &&Event : RegisteredEvents) {
+    if (matches(Event.Trigger, Call)) {
+      // Apply skipStdBaseClassRegion to canonicalize the mutex region
+      const MemRegion *MTX =
+          skipStdBaseClassRegion(getRegion(Event.Trigger, Call));
+      if (!MTX)
+        continue;
+      State = doResolvePossiblyDestroyedMutex(State, MTX);
+      ModelingResult Result = handleEvent(Event, MTX, Call, State, C);
+      C.addTransition(Result.State, Result.Note);
+    }
+  }
+}
+
+void MutexModeling::checkDeadSymbols(SymbolReaper &SymReaper,
+                                     CheckerContext &C) const {
+  ProgramStateRef State = C.getState();
+
+  for (auto I : State->get<DestroyedRetVals>()) {
+    // Once the return value symbol dies, no more checks can be performed
+    // against it. See if the return value was checked before this point.
+    // This would remove the symbol from the map as well.
+    if (SymReaper.isDead(I.second))
+      State = resolvePossiblyDestroyedMutex(State, I.first, &I.second);
+  }
+
+  for (auto I : State->get<LockStates>()) {
+    // Stop tracking dead mutex regions as well.
+    if (!SymReaper.isLiveRegion(I.first)) {
+      State = State->remove<LockStates>(I.first);
+      State = State->remove<DestroyedRetVals>(I.first);
+    }
+  }
+
+  // TODO: We probably need to clean up the lock stack as well.
+  // It is tricky though: even if the mutex cannot be unlocked anymore,
+  // it can still participate in lock order reversal resolution.
+
+  C.addTransition(State);
+}
+
+ProgramStateRef MutexModeling::checkRegionChanges(
+    ProgramStateRef State, const InvalidatedSymbols *Symbols,
+    ArrayRef<const MemRegion *> ExplicitRegions,
+    ArrayRef<const MemRegion *> Regions, const LocationContext *LCtx,
+    const CallEvent *Call) const {
+
+  bool IsLibraryFunction = false;
+  if (Call) {
+    // Avoid invalidating mutex state when a known supported function is
+    // called.
+    for (auto &&Event : RegisteredEvents) {
+      if (matches(Event.Trigger, *Call)) {
+        return State;
+      }
+    }
+
+    if (Call->isInSystemHeader())
+      IsLibraryFunction = true;
+  }
+
+  for (auto R : Regions) {
+    // We treat system library functions differently because we assume they
+    // won't modify mutex state unless the mutex is explicitly passed as an
+    // argument
+    if (IsLibraryFunction && !llvm::is_contained(ExplicitRegions, R))
+      continue;
+
+    State = State->remove<LockStates>(R);
+    State = State->remove<DestroyedRetVals>(R);
+
+    // TODO: We need to invalidate the lock stack as well. This is tricky
+    // to implement correctly and efficiently though, because the effects
+    // of mutex escapes on lock order may be fairly varied.
+  }
+
+  return State;
+}
+
+namespace clang {
+namespace ento {
+// Checker registration
+void registerMutexModeling(CheckerManager &CM) {
+  CM.registerChecker<MutexModeling>();
+
+  // The following RegisterEvent calls set up the checker to recognize various
+  // mutex-related function calls across different libraries and semantics.
+  // Each RegisterEvent associates a specific function with an event type
+  // (Init, Acquire, TryAcquire, Release, Destroy) and specifies how to
+  // extract the mutex argument from the function call.
+
+  // clang-format off
+  // Pthread-related events
+  // Init
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor(
+      {"pthread_mutex_init"}, 2),
+      EventKind::Init,
+      LibraryKind::Pthread
+  });
+
+  // Acquire
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor(
+      {"pthread_mutex_lock"}),
+      EventKind::Acquire,
+      LibraryKind::Pthread,
+      SemanticsKind::PthreadSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"pthread_rwlock_rdlock"}),
+    EventKind::Acquire,
+    LibraryKind::Pthread,
+    SemanticsKind::PthreadSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"pthread_rwlock_wrlock"}),
+    EventKind::Acquire,
+    LibraryKind::Pthread,
+    SemanticsKind::PthreadSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"lck_mtx_lock"}),
+    EventKind::Acquire,
+    LibraryKind::Pthread,
+    SemanticsKind::XNUSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"lck_rw_lock_exclusive"}),
+    EventKind::Acquire,
+    LibraryKind::Pthread,
+    SemanticsKind::XNUSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"lck_rw_lock_shared"}),
+    EventKind::Acquire,
+    LibraryKind::Pthread,
+    SemanticsKind::XNUSemantics
+  });
+
+  // TryAcquire
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"pthread_mutex_trylock"}),
+    EventKind::TryAcquire,
+    LibraryKind::Pthread,
+    SemanticsKind::PthreadSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"pthread_rwlock_tryrdlock"}),
+    EventKind::TryAcquire,
+    LibraryKind::Pthread,
+    SemanticsKind::PthreadSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"pthread_rwlock_trywrlock"}),
+    EventKind::TryAcquire,
+    LibraryKind::Pthread,
+    SemanticsKind::PthreadSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"lck_mtx_try_lock"}),
+    EventKind::TryAcquire,
+    LibraryKind::Pthread,
+    SemanticsKind::XNUSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"lck_rw_try_lock_exclusive"}),
+    EventKind::TryAcquire,
+    LibraryKind::Pthread,
+    SemanticsKind::XNUSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"lck_rw_try_lock_shared"}),
+    EventKind::TryAcquire,
+    LibraryKind::Pthread,
+    SemanticsKind::XNUSemantics
+  });
+
+  // Release
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"pthread_mutex_unlock"}),
+    EventKind::Release,
+    LibraryKind::Pthread
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"pthread_rwlock_unlock"}),
+    EventKind::Release,
+    LibraryKind::Pthread
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"lck_mtx_unlock"}),
+    EventKind::Release,
+    LibraryKind::Pthread
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"lck_rw_unlock_exclusive"}),
+    EventKind::Release,
+    LibraryKind::Pthread
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"lck_rw_unlock_shared"}),
+    EventKind::Release,
+    LibraryKind::Pthread
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"lck_rw_done"}),
+    EventKind::Release,
+    LibraryKind::Pthread
+  });
+
+  // Destroy
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"pthread_mutex_destroy"}),
+    EventKind::Destroy,
+    LibraryKind::Pthread,
+    SemanticsKind::PthreadSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"lck_mtx_destroy"}, 2),
+    EventKind::Destroy,
+    LibraryKind::Pthread,
+    SemanticsKind::XNUSemantics
+  });
+
+  // Fuchsia-related events
+  // Init
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"spin_lock_init"}),
+    EventKind::Init,
+    LibraryKind::Fuchsia
+  });
+
+  // Acquire
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"spin_lock"}),
+    EventKind::Acquire,
+    LibraryKind::Fuchsia,
+    SemanticsKind::PthreadSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"spin_lock_save"}, 3),
+    EventKind::Acquire,
+    LibraryKind::Fuchsia,
+    SemanticsKind::PthreadSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"sync_mutex_lock"}),
+    EventKind::Acquire,
+    LibraryKind::Fuchsia,
+    SemanticsKind::PthreadSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"sync_mutex_lock_with_waiter"}),
+    EventKind::Acquire,
+    LibraryKind::Fuchsia,
+    SemanticsKind::PthreadSemantics
+  });
+
+  // TryAcquire
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"spin_trylock"}),
+    EventKind::TryAcquire,
+    LibraryKind::Fuchsia,
+    SemanticsKind::PthreadSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"sync_mutex_trylock"}),
+    EventKind::TryAcquire,
+    LibraryKind::Fuchsia,
+    SemanticsKind::PthreadSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"sync_mutex_timedlock"}, 2),
+    EventKind::TryAcquire,
+    LibraryKind::Fuchsia,
+    SemanticsKind::PthreadSemantics
+  });
+
+  // Release
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"spin_unlock"}),
+    EventKind::Release,
+    LibraryKind::Fuchsia
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"spin_unlock_restore"}, 3),
+    EventKind::Release,
+    LibraryKind::Fuchsia
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"sync_mutex_unlock"}),
+    EventKind::Release,
+    LibraryKind::Fuchsia
+  });
+
+  // C11-related events
+  // Init
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"mtx_init"}, 2),
+    EventKind::Init,
+    LibraryKind::C11
+  });
+
+  // Acquire
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"mtx_lock"}),
+    EventKind::Acquire,
+    LibraryKind::C11,
+    SemanticsKind::PthreadSemantics
+  });
+
+  // TryAcquire
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"mtx_trylock"}),
+    EventKind::TryAcquire,
+    LibraryKind::C11,
+    SemanticsKind::PthreadSemantics
+  });
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"mtx_timedlock"}, 2),
+    EventKind::TryAcquire,
+    LibraryKind::C11,
+    SemanticsKind::PthreadSemantics
+  });
+
+  // Release
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"mtx_unlock"}),
+    EventKind::Release,
+    LibraryKind::C11
+  });
+
+  // Destroy
+  RegisterEvent(EventDescriptor{
+    MakeFirstArgExtractor({"mtx_destroy"}),
+    EventKind::Destroy,
+    LibraryKind::C11,
+    SemanticsKind::PthreadSemantics
+  });
+  // clang-format on
+}
+bool shouldRegisterMutexModeling(const CheckerManager &) { return true; }
+} // namespace ento
+} // namespace clang
diff --git a/clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexModelingAPI.h b/clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexModelingAPI.h
new file mode 100644
index 00000000000000..83ae83d23ee77b
--- /dev/null
+++ b/clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexModelingAPI.h
@@ -0,0 +1,244 @@
+//===--- MutexModelingAPI.h - API for modeling mutexes --------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// Defines inter-checker API for tracking and manipulating the
+// modeled state of locked mutexes in the GDM.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_LIB_STATICANALYZER_CHECKERS_MUTEXMODELINGAPI_H
+#define LLVM_CLANG_LIB_STATICANALYZER_CHECKERS_MUTEXMODELINGAPI_H
+
+#include "MutexModelingDomain.h"
+#include "MutexModelingGDM.h"
+#include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/SmallSet.h"
+#include "llvm/ADT/StringExtras.h"
+
+namespace clang {
+
+namespace ento {
+class BugType;
+namespace mutex_modeling {
+
+// Set of registered bug types for mutex modeling
+inline llvm::SmallSet<const BugType *, 0> RegisteredBugTypes{};
+
+// Register a bug type for mutex modeling
+inline void RegisterBugTypeForMutexModeling(const BugType *BT) {
+  RegisteredBugTypes.insert(BT);
+}
+
+// Check if a bug type is registered for mutex modeling
+inline bool IsBugTypeRegisteredForMutexModeling(const BugType *BT) {
+  return RegisteredBugTypes.contains(BT);
+}
+
+// Vector of registered event descriptors
+inline llvm::SmallVector<EventDescriptor, 0> RegisteredEvents{};
+
+// Register an event descriptor
+inline auto RegisterEvent(EventDescriptor Event) {
+  RegisteredEvents.push_back(Event);
+}
+
+// Helper functions to create common types of mutex extractors
+inline auto
+MakeFirstArgExtractor(ArrayRef<StringRef> NameParts, int NumArgsRequired = 1,
+                      CallDescription::Mode MatchAs = CDM::CLibrary) {
+  return FirstArgMutexExtractor{
+      CallDescription{MatchAs, NameParts, NumArgsRequired}};
+}
+
+inline auto
+MakeMemberExtractor(ArrayRef<StringRef> NameParts, int NumArgsRequired = 0,
+                    CallDescription::Mode MatchAs = CDM::CXXMethod) {
+  return MemberMutexExtractor{
+      CallDescription{MatchAs, NameParts, NumArgsRequired}};
+}
+
+inline auto MakeRAIILockExtractor(StringRef GuardObjectName) {
+  return RAIILockExtractor{GuardObjectName};
+}
+
+inline auto MakeRAIIReleaseExtractor(StringRef GuardObjectName) {
+  return RAIIReleaseExtractor{GuardObjectName};
+}
+
+// Check if any critical sections are currently active
+inline bool AreAnyCritsectionsActive(CheckerContext &C) {
+  return !C.getState()->get<CritSections>().isEmpty();
+}
+
+// Create a note tag for a mutex critical section
+inline const NoteTag *CreateMutexCritSectionNote(CritSectionMarker M,
+                                                 CheckerContext &C) {
+  return C.getNoteTag([M](const PathSensitiveBugReport &BR,
+                          llvm::raw_ostream &OS) {
+    if (!IsBugTypeRegisteredForMutexModeling(&BR.getBugType()))
+      return;
+    const auto CritSectionBegins =
+        BR.getErrorNode()->getState()->get<CritSections>();
+    llvm::SmallVector<CritSectionMarker, 4> LocksForMutex;
+    llvm::copy_if(CritSectionBegins, std::back_inserter(LocksForMutex),
+                  [M](const auto &Marker) {
+                    return Marker.MutexRegion == M.MutexRegion;
+                  });
+    if (LocksForMutex.empty())
+      return;
+
+    // As the ImmutableList builds the locks by prepending them, we
+    // reverse the list to get the correct order.
+    std::reverse(LocksForMutex.begin(), LocksForMutex.end());
+
+    // Find the index of the lock expression in the list of all locks for a
+    // given mutex (in acquisition order).
+    const CritSectionMarker *const Position =
+        llvm::find_if(std::as_const(LocksForMutex), [M](const auto &Marker) {
+          return Marker.BeginExpr == M.BeginExpr;
+        });
+    if (Position == LocksForMutex.end())
+      return;
+
+    // If there is only one lock event, we don't need to specify how many times
+    // the critical section was entered.
+    if (LocksForMutex.size() == 1) {
+      OS << "Entering critical section here";
+      return;
+    }
+
+    const auto IndexOfLock =
+        std::distance(std::as_const(LocksForMutex).begin(), Position);
+
+    const auto OrdinalOfLock = IndexOfLock + 1;
+    OS << "Entering critical section for the " << OrdinalOfLock
+       << llvm::getOrdinalSuffix(OrdinalOfLock) << " time here";
+  });
+}
+
+// Print the current state of mutex events, lock states, and destroyed return
+// values
+inline void printState(raw_ostream &Out, ProgramStateRef State, const char *NL,
+                       const char *Sep) {
+
+  const MutexEventsTy &ME = State->get<MutexEvents>();
+  if (!ME.isEmpty()) {
+    Out << Sep << "Mutex event:" << NL;
+    for (auto I : ME) {
+      Out << Sep << "Kind: " << ": ";
+      switch (I.Kind) {
+      case (EventKind::Init):
+        Out << "Init";
+        break;
+      case (EventKind::Acquire):
+        Out << "Acquire";
+        break;
+      case (EventKind::TryAcquire):
+        Out << "TryAcquire";
+        break;
+      case (EventKind::Release):
+        Out << "Release";
+        break;
+      case (EventKind::Destroy):
+        Out << "Destroy";
+        break;
+      }
+      Out << NL;
+      Out << Sep << "Semantics: ";
+      switch (I.Semantics) {
+      case (SemanticsKind::NotApplicable):
+        Out << "NotApplicable";
+        break;
+      case (SemanticsKind::PthreadSemantics):
+        Out << "PthreadSemantics";
+        break;
+      case (SemanticsKind::XNUSemantics):
+        Out << "XNUSemantics";
+        break;
+      }
+      Out << NL;
+      Out << Sep << "Library: ";
+      switch (I.Library) {
+      case (LibraryKind::NotApplicable):
+        Out << "NotApplicable";
+        break;
+      case (LibraryKind::Pthread):
+        Out << "Pthread";
+        break;
+      case (LibraryKind::Fuchsia):
+        Out << "Fuchsia";
+        break;
+      case (LibraryKind::C11):
+        Out << "C11";
+        break;
+      default:
+        llvm_unreachable("Unknown library");
+      }
+      Out << NL;
+
+      // Omit MutexExpr and EventExpr
+
+      Out << Sep << "Mutex region: ";
+      I.MutexRegion->dumpToStream(Out);
+      Out << NL;
+    }
+
+    const LockStatesTy &LM = State->get<LockStates>();
+    if (!LM.isEmpty()) {
+      Out << Sep << "Mutex states:" << NL;
+      for (auto I : LM) {
+        I.first->dumpToStream(Out);
+        switch (I.second) {
+        case (LockStateKind::Locked):
+          Out << ": locked";
+          break;
+        case (LockStateKind::Unlocked):
+          Out << ": unlocked";
+          break;
+        case (LockStateKind::Destroyed):
+          Out << ": destroyed";
+          break;
+        case (LockStateKind::UntouchedAndPossiblyDestroyed):
+          Out << ": not tracked, possibly destroyed";
+          break;
+        case (LockStateKind::UnlockedAndPossiblyDestroyed):
+          Out << ": unlocked, possibly destroyed";
+          break;
+        case (LockStateKind::Error_DoubleInit):
+          Out << ": error: double init";
+          break;
+        case (LockStateKind::Error_DoubleInitWhileLocked):
+          Out << ": error: double init while locked";
+          break;
+        default:
+          llvm_unreachable("Unknown lock state");
+        }
+        Out << NL;
+      }
+    }
+
+    const DestroyedRetValsTy &DRV = State->get<DestroyedRetVals>();
+    if (!DRV.isEmpty()) {
+      Out << Sep << "Mutexes in unresolved possibly destroyed state:" << NL;
+      for (auto I : DRV) {
+        I.first->dumpToStream(Out);
+        Out << ": ";
+        I.second->dumpToStream(Out);
+        Out << NL;
+      }
+    }
+  }
+}
+
+} // namespace mutex_modeling
+} // namespace ento
+} // namespace clang
+
+#endif
diff --git a/clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexModelingDomain.h b/clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexModelingDomain.h
new file mode 100644
index 00000000000000..b4e1fdf2f1108e
--- /dev/null
+++ b/clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexModelingDomain.h
@@ -0,0 +1,126 @@
+//===--- MutexModelingDomain.h - Common vocabulary for modeling mutexes ---===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// Defines common types and related functions used in the mutex modeling domain.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_LIB_STATICANALYZER_CHECKERS_MUTEXMODELINGDOMAIN_H
+#define LLVM_CLANG_LIB_STATICANALYZER_CHECKERS_MUTEXMODELINGDOMAIN_H
+
+#include "MutexRegionExtractor.h"
+
+// Forward declarations.
+namespace clang {
+class Expr;
+class IdentifierInfo;
+namespace ento {
+class MemRegion;
+} // namespace ento
+} // namespace clang
+
+namespace clang::ento::mutex_modeling {
+
+// Represents different kinds of mutex-related events
+enum class EventKind { Init, Acquire, TryAcquire, Release, Destroy };
+
+// TODO: Ideally the modeling should not know about which checkers consume the
+// modeling information. This enum is here to make a correspondence between the
+// checked mutex event the library that event came from. In order to keep the
+// external API of multiple distinct checkers (PthreadLockChecker,
+// FuchsiaLockChecker and C11LockChecker), this mapping is done here, but if
+// more consumers of this modeling arise, adding all of them here may not be
+// feasible and we may need to make this modeling more flexible.
+enum class LibraryKind { NotApplicable = 0, Pthread, Fuchsia, C11 };
+
+// Represents different mutex operation semantics
+enum class SemanticsKind { NotApplicable = 0, PthreadSemantics, XNUSemantics };
+
+// Represents different states a mutex can be in, including error states
+enum class LockStateKind {
+  Unlocked,
+  Locked,
+  Destroyed,
+  UntouchedAndPossiblyDestroyed,
+  UnlockedAndPossiblyDestroyed,
+  Error_DoubleInit,            // Mutex initialized twice
+  Error_DoubleInitWhileLocked, // Mutex initialized while already locked
+  Error_DoubleLock,            // Mutex locked twice without unlocking
+  Error_LockDestroyed,         // Attempt to lock a destroyed mutex
+  Error_DoubleUnlock,          // Mutex unlocked twice without locking
+  Error_UnlockDestroyed,       // Attempt to unlock a destroyed mutex
+  Error_LockReversal,          // Locks acquired in incorrect order
+  Error_DestroyLocked,         // Attempt to destroy a locked mutex
+  Error_DoubleDestroy          // Mutex destroyed twice
+};
+
+/// This class is intended for describing the list of events to detect.
+/// This list of events is the configuration of the MutexModeling checker.
+struct EventDescriptor {
+  MutexRegionExtractor Trigger;
+  EventKind Kind{};
+  LibraryKind Library{};
+  SemanticsKind Semantics{};
+
+  // TODO: Modernize to spaceship when C++20 is available.
+  [[nodiscard]] bool operator!=(const EventDescriptor &Other) const noexcept {
+    return !(Trigger == Other.Trigger) || Library != Other.Library ||
+           Kind != Other.Kind || Semantics != Other.Semantics;
+  }
+  [[nodiscard]] bool operator==(const EventDescriptor &Other) const noexcept {
+    return !(*this != Other);
+  }
+};
+
+/// This class is used in the GDM to describe the events that were detected.
+/// As instances of this class can appear many times in the ExplodedGraph, it
+/// best to keep it as simple and small as possible.
+struct EventMarker {
+  EventKind Kind{};
+  SemanticsKind Semantics{};
+  LibraryKind Library{};
+  const IdentifierInfo *EventII;
+  const clang::Expr *EventExpr{};
+  const clang::ento::MemRegion *MutexRegion{};
+
+  // TODO: Modernize to spaceship when C++20 is available.
+  [[nodiscard]] constexpr bool
+  operator!=(const EventMarker &Other) const noexcept {
+    return EventII != Other.EventII || Kind != Other.Kind ||
+           Semantics != Other.Semantics || Library != Other.Library ||
+           EventExpr != Other.EventExpr || MutexRegion != Other.MutexRegion;
+  }
+  [[nodiscard]] constexpr bool
+  operator==(const EventMarker &Other) const noexcept {
+    return !(*this != Other);
+  }
+};
+
+// Represents a critical section in the code, marked by a mutex lock
+struct CritSectionMarker {
+  const clang::Expr *BeginExpr;
+  const clang::ento::MemRegion *MutexRegion;
+
+  explicit CritSectionMarker(const clang::Expr *BeginExpr,
+                             const clang::ento::MemRegion *MutexRegion)
+      : BeginExpr(BeginExpr), MutexRegion(MutexRegion) {}
+
+  // TODO: Modernize to spaceship when C++20 is available.
+  [[nodiscard]] constexpr bool
+  operator!=(const CritSectionMarker &Other) const noexcept {
+    return BeginExpr != Other.BeginExpr || MutexRegion != Other.MutexRegion;
+  }
+  [[nodiscard]] constexpr bool
+  operator==(const CritSectionMarker &Other) const noexcept {
+    return !(*this != Other);
+  }
+};
+
+} // namespace clang::ento::mutex_modeling
+
+#endif
diff --git a/clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexModelingGDM.h b/clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexModelingGDM.h
new file mode 100644
index 00000000000000..d9f9549645f607
--- /dev/null
+++ b/clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexModelingGDM.h
@@ -0,0 +1,169 @@
+//===--- MutexModelingGDM.h - Modeling of mutexes in GDM ------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// Defines the GDM definitions for tracking mutex states.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_LIB_STATICANALYZER_CHECKERS_MUTEXMODELINGGDM_H
+#define LLVM_CLANG_LIB_STATICANALYZER_CHECKERS_MUTEXMODELINGGDM_H
+
+#include "MutexModelingDomain.h"
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
+#include "llvm/ADT/FoldingSet.h"
+
+// GDM-related handle-types for tracking mutex states.
+namespace clang {
+namespace ento {
+namespace mutex_modeling {
+
+// Raw data of the mutex events.
+class MutexEvents {};
+using MutexEventsTy = llvm::ImmutableList<EventMarker>;
+
+// Aggregated data structures for tracking critical sections.
+class CritSections {};
+using CritSectionsTy = llvm::ImmutableList<CritSectionMarker>;
+
+// Aggregated data structures for tracking mutex states.
+class LockStates {};
+using LockStatesTy = llvm::ImmutableMap<const MemRegion *, LockStateKind>;
+
+// Tracks return values of destroy operations for potentially destroyed mutexes
+class DestroyedRetVals {};
+using DestroyedRetValsTy = llvm::ImmutableMap<const MemRegion *, SymbolRef>;
+
+} // namespace mutex_modeling
+} // namespace ento
+} // namespace clang
+
+// Enable usage of mutex modeling data structures in llvm::FoldingSet.
+namespace llvm {
+// Specialization for EventMarker to allow its use in FoldingSet
+template <> struct FoldingSetTrait<clang::ento::mutex_modeling::EventMarker> {
+  static void Profile(const clang::ento::mutex_modeling::EventMarker &EM,
+                      llvm::FoldingSetNodeID &ID) {
+    ID.Add(EM.Kind);
+    ID.Add(EM.Library);
+    ID.Add(EM.Semantics);
+    ID.Add(EM.EventII);
+    ID.Add(EM.EventExpr);
+    ID.Add(EM.MutexRegion);
+  }
+};
+
+// Specialization for CritSectionMarker to allow its use in FoldingSet
+template <>
+struct FoldingSetTrait<clang::ento::mutex_modeling::CritSectionMarker> {
+  static void Profile(const clang::ento::mutex_modeling::CritSectionMarker &CSM,
+                      llvm::FoldingSetNodeID &ID) {
+    ID.Add(CSM.BeginExpr);
+    ID.Add(CSM.MutexRegion);
+  }
+};
+} // namespace llvm
+
+// Iterator traits for ImmutableList and ImmutableMap data structures
+// that enable the use of STL algorithms.
+namespace std {
+// These specializations allow the use of STL algorithms with our custom data
+// structures
+// TODO: Move these to llvm::ImmutableList when overhauling immutable data
+// structures for proper iterator concept support.
+template <>
+struct iterator_traits<typename llvm::ImmutableList<
+    clang::ento::mutex_modeling::EventMarker>::iterator> {
+  using iterator_category = std::forward_iterator_tag;
+  using value_type = clang::ento::mutex_modeling::EventMarker;
+  using difference_type = std::ptrdiff_t;
+  using reference = clang::ento::mutex_modeling::EventMarker &;
+  using pointer = clang::ento::mutex_modeling::EventMarker *;
+};
+template <>
+struct iterator_traits<typename llvm::ImmutableList<
+    clang::ento::mutex_modeling::CritSectionMarker>::iterator> {
+  using iterator_category = std::forward_iterator_tag;
+  using value_type = clang::ento::mutex_modeling::CritSectionMarker;
+  using difference_type = std::ptrdiff_t;
+  using reference = clang::ento::mutex_modeling::CritSectionMarker &;
+  using pointer = clang::ento::mutex_modeling::CritSectionMarker *;
+};
+template <>
+struct iterator_traits<typename llvm::ImmutableMap<
+    const clang::ento::MemRegion *,
+    clang::ento::mutex_modeling::LockStateKind>::iterator> {
+  using iterator_category = std::forward_iterator_tag;
+  using value_type = std::pair<const clang::ento::MemRegion *,
+                               clang::ento::mutex_modeling::LockStateKind>;
+  using difference_type = std::ptrdiff_t;
+  using reference = std::pair<const clang::ento::MemRegion *,
+                              clang::ento::mutex_modeling::LockStateKind> &;
+  using pointer = std::pair<const clang::ento::MemRegion *,
+                            clang::ento::mutex_modeling::LockStateKind> *;
+};
+template <>
+struct iterator_traits<typename llvm::ImmutableMap<
+    const clang::ento::MemRegion *, clang::ento::SymbolRef>::iterator> {
+  using iterator_category = std::forward_iterator_tag;
+  using value_type =
+      std::pair<const clang::ento::MemRegion *, clang::ento::SymbolRef>;
+  using difference_type = std::ptrdiff_t;
+  using reference =
+      std::pair<const clang::ento::MemRegion *, clang::ento::SymbolRef> &;
+  using pointer =
+      std::pair<const clang::ento::MemRegion *, clang::ento::SymbolRef> *;
+};
+} // namespace std
+
+// NOTE: ProgramState macros are not used here, because the visibility of these
+// GDM entries must span multiple translation units (multiple checkers).
+// TODO: check if this is still true after finishing the implementation.
+namespace clang {
+namespace ento {
+template <>
+struct ProgramStateTrait<clang::ento::mutex_modeling::MutexEvents>
+    : public ProgramStatePartialTrait<
+          clang::ento::mutex_modeling::MutexEventsTy> {
+  static void *GDMIndex() {
+    static int Index;
+    return &Index;
+  }
+};
+template <>
+struct ProgramStateTrait<clang::ento::mutex_modeling::CritSections>
+    : public ProgramStatePartialTrait<
+          clang::ento::mutex_modeling::CritSectionsTy> {
+  static void *GDMIndex() {
+    static int Index;
+    return &Index;
+  }
+};
+template <>
+struct ProgramStateTrait<clang::ento::mutex_modeling::LockStates>
+    : public ProgramStatePartialTrait<
+          clang::ento::mutex_modeling::LockStatesTy> {
+  static void *GDMIndex() {
+    static int Index;
+    return &Index;
+  }
+};
+template <>
+struct ProgramStateTrait<clang::ento::mutex_modeling::DestroyedRetVals>
+    : public ProgramStatePartialTrait<
+          clang::ento::mutex_modeling::DestroyedRetValsTy> {
+  static void *GDMIndex() {
+    static int Index;
+    return &Index;
+  }
+};
+} // namespace ento
+} // namespace clang
+
+#endif
diff --git a/clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexRegionExtractor.h b/clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexRegionExtractor.h
new file mode 100644
index 00000000000000..e31665ba68dee5
--- /dev/null
+++ b/clang/lib/StaticAnalyzer/Checkers/MutexModeling/MutexRegionExtractor.h
@@ -0,0 +1,139 @@
+//===--- MutexRegionExtractor.h - Modeling of mutexes ---------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// Defines modeling checker for tracking mutex states.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_LIB_STATICANALYZER_CHECKERS_MUTEXMODELING_MUTEXREGIONEXTRACTOR_H
+#define LLVM_CLANG_LIB_STATICANALYZER_CHECKERS_MUTEXMODELING_MUTEXREGIONEXTRACTOR_H
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/CallDescription.h"
+#include <variant>
+
+namespace clang::ento::mutex_modeling {
+
+// Extracts the mutex region from the first argument of a function call
+class FirstArgMutexExtractor {
+  CallDescription CD;
+
+public:
+  template <typename T>
+  FirstArgMutexExtractor(T &&CD) : CD(std::forward<T>(CD)) {}
+
+  [[nodiscard]] bool matches(const CallEvent &Call) const {
+    return CD.matches(Call);
+  }
+
+  [[nodiscard]] const MemRegion *getRegion(const CallEvent &Call) const {
+    return Call.getArgSVal(0).getAsRegion();
+  }
+};
+
+// Extracts the mutex region from the 'this' pointer of a member function call
+class MemberMutexExtractor {
+  CallDescription CD;
+
+public:
+  template <typename T>
+  MemberMutexExtractor(T &&CD) : CD(std::forward<T>(CD)) {}
+
+  [[nodiscard]] bool matches(const CallEvent &Call) const {
+    return CD.matches(Call);
+  }
+
+  [[nodiscard]] const MemRegion *getRegion(const CallEvent &Call) const {
+    return llvm::cast<CXXMemberCall>(Call).getCXXThisVal().getAsRegion();
+  }
+};
+
+// Template class for extracting mutex regions from RAII-style lock/unlock
+// operations
+template <bool IsLock> class RAIIMutexExtractor {
+  mutable const clang::IdentifierInfo *Guard{};
+  mutable bool IdentifierInfoInitialized{};
+  mutable llvm::SmallString<32> GuardName{};
+
+  void initIdentifierInfo(const CallEvent &Call) const {
+    if (!IdentifierInfoInitialized) {
+      // In case of checking C code, or when the corresponding headers are not
+      // included, we might end up query the identifier table every time when
+      // this function is called instead of early returning it. To avoid this,
+      // a bool variable (IdentifierInfoInitialized) is used and the function
+      // will be run only once.
+      const auto &ASTCtx = Call.getState()->getStateManager().getContext();
+      Guard = &ASTCtx.Idents.get(GuardName);
+    }
+  }
+
+  template <typename T> bool matchesImpl(const CallEvent &Call) const {
+    const T *C = llvm::dyn_cast<T>(&Call);
+    if (!C)
+      return false;
+    const clang::IdentifierInfo *II =
+        llvm::cast<clang::CXXRecordDecl>(C->getDecl()->getParent())
+            ->getIdentifier();
+    return II == Guard;
+  }
+
+public:
+  RAIIMutexExtractor(llvm::StringRef GuardName) : GuardName(GuardName) {}
+  [[nodiscard]] bool matches(const CallEvent &Call) const {
+    initIdentifierInfo(Call);
+    if constexpr (IsLock) {
+      return matchesImpl<CXXConstructorCall>(Call);
+    } else {
+      return matchesImpl<CXXDestructorCall>(Call);
+    }
+  }
+  [[nodiscard]] const MemRegion *getRegion(const CallEvent &Call) const {
+    const MemRegion *MutexRegion = nullptr;
+    if constexpr (IsLock) {
+      if (std::optional<SVal> Object = Call.getReturnValueUnderConstruction()) {
+        MutexRegion = Object->getAsRegion();
+      }
+    } else {
+      MutexRegion =
+          llvm::cast<CXXDestructorCall>(Call).getCXXThisVal().getAsRegion();
+    }
+    return MutexRegion;
+  }
+};
+
+// Specializations for RAII-style lock and release operations
+using RAIILockExtractor = RAIIMutexExtractor<true>;
+using RAIIReleaseExtractor = RAIIMutexExtractor<false>;
+
+// Variant type that can hold any of the mutex region extractor types
+using MutexRegionExtractor =
+    std::variant<FirstArgMutexExtractor, MemberMutexExtractor,
+                 RAIILockExtractor, RAIIReleaseExtractor>;
+
+// Helper functions for working with MutexRegionExtractor variant
+inline const MemRegion *getRegion(const MutexRegionExtractor &Extractor,
+                                  const CallEvent &Call) {
+  return std::visit(
+      [&Call](auto &&Descriptor) { return Descriptor.getRegion(Call); },
+      Extractor);
+}
+
+inline bool operator==(const MutexRegionExtractor &LHS,
+                       const MutexRegionExtractor &RHS) {
+  return std::visit([](auto &&LHS, auto &&RHS) { return LHS == RHS; }, LHS,
+                    RHS);
+}
+
+inline bool matches(const MutexRegionExtractor &Extractor,
+                    const CallEvent &Call) {
+  return std::visit(
+      [&Call](auto &&Extractor) { return Extractor.matches(Call); }, Extractor);
+}
+
+} // namespace clang::ento::mutex_modeling
+
+#endif
diff --git a/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
index 86530086ff1b27..d6a034f1fdee80 100644
--- a/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
+++ b/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
@@ -730,7 +730,9 @@ void ento::registerPthreadLockBase(CheckerManager &mgr) {
   mgr.registerChecker<PthreadLockChecker>();
 }
 
-bool ento::shouldRegisterPthreadLockBase(const CheckerManager &mgr) { return true; }
+bool ento::shouldRegisterPthreadLockBase(const CheckerManager &mgr) {
+  return true;
+}
 
 #define REGISTER_CHECKER(name)                                                 \
   void ento::register##name(CheckerManager &mgr) {                             \

>From e62416585ebf4ef70e2168dae78901b2bac1f9be Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Endre=20F=C3=BCl=C3=B6p?= <endre.fulop at sigmatechnology.com>
Date: Thu, 3 Oct 2024 18:25:35 +0200
Subject: [PATCH 2/5] Update checker dependencies for MutexModeling

This patch updates the dependencies of existing checkers to use the
newMutexModeling checker. Specifically, it modifies the
PthreadLockBase,BlockInCriticalSectionChecker, and PthreadLockChecker to
depend onMutexModeling.
---
 clang/include/clang/StaticAnalyzer/Checkers/Checkers.td | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td b/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
index fb31011dde84ff..b41580dcfba575 100644
--- a/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
+++ b/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
@@ -312,6 +312,7 @@ def StackAddrAsyncEscapeChecker : Checker<"StackAddressAsyncEscape">,
 
 def PthreadLockBase : Checker<"PthreadLockBase">,
   HelpText<"Helper registering multiple checks.">,
+  Dependencies<[MutexModeling]>,
   Documentation<NotDocumented>,
   Hidden;
 
@@ -510,6 +511,7 @@ def UnixAPIMisuseChecker : Checker<"API">,
 
 def BlockInCriticalSectionChecker : Checker<"BlockInCriticalSection">,
   HelpText<"Check for calls to blocking functions inside a critical section">,
+  Dependencies<[MutexModeling]>,
   Documentation<HasDocumentation>;
 
 def DynamicMemoryModeling: Checker<"DynamicMemoryModeling">,
@@ -615,7 +617,7 @@ def ChrootChecker : Checker<"Chroot">,
 
 def PthreadLockChecker : Checker<"PthreadLock">,
   HelpText<"Simple lock -> unlock checker">,
-  Dependencies<[PthreadLockBase]>,
+  Dependencies<[PthreadLockBase, MutexModeling]>,
   Documentation<HasDocumentation>;
 
 def SimpleStreamChecker : Checker<"SimpleStream">,

>From fe30b8153980383f008aa491a65144b58420ddd3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Endre=20F=C3=BCl=C3=B6p?= <endre.fulop at sigmatechnology.com>
Date: Thu, 3 Oct 2024 18:26:29 +0200
Subject: [PATCH 3/5] Update BlockInCriticalSectionChecker for MutexModeling

This patch updates the BlockInCriticalSectionChecker to use the
newMutexModeling API. It removes the old mutex modeling logic and
replacesit with calls to the new API.
---
 .../BlockInCriticalSectionChecker.cpp         | 373 +++---------------
 1 file changed, 55 insertions(+), 318 deletions(-)

diff --git a/clang/lib/StaticAnalyzer/Checkers/BlockInCriticalSectionChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/BlockInCriticalSectionChecker.cpp
index 7460781799d08a..e5be2dfc19ff42 100644
--- a/clang/lib/StaticAnalyzer/Checkers/BlockInCriticalSectionChecker.cpp
+++ b/clang/lib/StaticAnalyzer/Checkers/BlockInCriticalSectionChecker.cpp
@@ -14,165 +14,24 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include "MutexModeling/MutexModelingAPI.h"
+
 #include "clang/StaticAnalyzer/Checkers/BuiltinCheckerRegistration.h"
 #include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
 #include "clang/StaticAnalyzer/Core/Checker.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CallDescription.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerHelpers.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
-#include "llvm/ADT/STLExtras.h"
-#include "llvm/ADT/SmallString.h"
-#include "llvm/ADT/StringExtras.h"
 
-#include <iterator>
 #include <utility>
-#include <variant>
 
 using namespace clang;
 using namespace ento;
+using namespace mutex_modeling;
 
 namespace {
-
-struct CritSectionMarker {
-  const Expr *LockExpr{};
-  const MemRegion *LockReg{};
-
-  void Profile(llvm::FoldingSetNodeID &ID) const {
-    ID.Add(LockExpr);
-    ID.Add(LockReg);
-  }
-
-  [[nodiscard]] constexpr bool
-  operator==(const CritSectionMarker &Other) const noexcept {
-    return LockExpr == Other.LockExpr && LockReg == Other.LockReg;
-  }
-  [[nodiscard]] constexpr bool
-  operator!=(const CritSectionMarker &Other) const noexcept {
-    return !(*this == Other);
-  }
-};
-
-class CallDescriptionBasedMatcher {
-  CallDescription LockFn;
-  CallDescription UnlockFn;
-
-public:
-  CallDescriptionBasedMatcher(CallDescription &&LockFn,
-                              CallDescription &&UnlockFn)
-      : LockFn(std::move(LockFn)), UnlockFn(std::move(UnlockFn)) {}
-  [[nodiscard]] bool matches(const CallEvent &Call, bool IsLock) const {
-    if (IsLock) {
-      return LockFn.matches(Call);
-    }
-    return UnlockFn.matches(Call);
-  }
-};
-
-class FirstArgMutexDescriptor : public CallDescriptionBasedMatcher {
-public:
-  FirstArgMutexDescriptor(CallDescription &&LockFn, CallDescription &&UnlockFn)
-      : CallDescriptionBasedMatcher(std::move(LockFn), std::move(UnlockFn)) {}
-
-  [[nodiscard]] const MemRegion *getRegion(const CallEvent &Call, bool) const {
-    return Call.getArgSVal(0).getAsRegion();
-  }
-};
-
-class MemberMutexDescriptor : public CallDescriptionBasedMatcher {
-public:
-  MemberMutexDescriptor(CallDescription &&LockFn, CallDescription &&UnlockFn)
-      : CallDescriptionBasedMatcher(std::move(LockFn), std::move(UnlockFn)) {}
-
-  [[nodiscard]] const MemRegion *getRegion(const CallEvent &Call, bool) const {
-    return cast<CXXMemberCall>(Call).getCXXThisVal().getAsRegion();
-  }
-};
-
-class RAIIMutexDescriptor {
-  mutable const IdentifierInfo *Guard{};
-  mutable bool IdentifierInfoInitialized{};
-  mutable llvm::SmallString<32> GuardName{};
-
-  void initIdentifierInfo(const CallEvent &Call) const {
-    if (!IdentifierInfoInitialized) {
-      // In case of checking C code, or when the corresponding headers are not
-      // included, we might end up query the identifier table every time when
-      // this function is called instead of early returning it. To avoid this, a
-      // bool variable (IdentifierInfoInitialized) is used and the function will
-      // be run only once.
-      const auto &ASTCtx = Call.getState()->getStateManager().getContext();
-      Guard = &ASTCtx.Idents.get(GuardName);
-    }
-  }
-
-  template <typename T> bool matchesImpl(const CallEvent &Call) const {
-    const T *C = dyn_cast<T>(&Call);
-    if (!C)
-      return false;
-    const IdentifierInfo *II =
-        cast<CXXRecordDecl>(C->getDecl()->getParent())->getIdentifier();
-    return II == Guard;
-  }
-
-public:
-  RAIIMutexDescriptor(StringRef GuardName) : GuardName(GuardName) {}
-  [[nodiscard]] bool matches(const CallEvent &Call, bool IsLock) const {
-    initIdentifierInfo(Call);
-    if (IsLock) {
-      return matchesImpl<CXXConstructorCall>(Call);
-    }
-    return matchesImpl<CXXDestructorCall>(Call);
-  }
-  [[nodiscard]] const MemRegion *getRegion(const CallEvent &Call,
-                                           bool IsLock) const {
-    const MemRegion *LockRegion = nullptr;
-    if (IsLock) {
-      if (std::optional<SVal> Object = Call.getReturnValueUnderConstruction()) {
-        LockRegion = Object->getAsRegion();
-      }
-    } else {
-      LockRegion = cast<CXXDestructorCall>(Call).getCXXThisVal().getAsRegion();
-    }
-    return LockRegion;
-  }
-};
-
-using MutexDescriptor =
-    std::variant<FirstArgMutexDescriptor, MemberMutexDescriptor,
-                 RAIIMutexDescriptor>;
-
 class BlockInCriticalSectionChecker : public Checker<check::PostCall> {
 private:
-  const std::array<MutexDescriptor, 8> MutexDescriptors{
-      // NOTE: There are standard library implementations where some methods
-      // of `std::mutex` are inherited from an implementation detail base
-      // class, and those aren't matched by the name specification {"std",
-      // "mutex", "lock"}.
-      // As a workaround here we omit the class name and only require the
-      // presence of the name parts "std" and "lock"/"unlock".
-      // TODO: Ensure that CallDescription understands inherited methods.
-      MemberMutexDescriptor(
-          {/*MatchAs=*/CDM::CXXMethod,
-           /*QualifiedName=*/{"std", /*"mutex",*/ "lock"},
-           /*RequiredArgs=*/0},
-          {CDM::CXXMethod, {"std", /*"mutex",*/ "unlock"}, 0}),
-      FirstArgMutexDescriptor({CDM::CLibrary, {"pthread_mutex_lock"}, 1},
-                              {CDM::CLibrary, {"pthread_mutex_unlock"}, 1}),
-      FirstArgMutexDescriptor({CDM::CLibrary, {"mtx_lock"}, 1},
-                              {CDM::CLibrary, {"mtx_unlock"}, 1}),
-      FirstArgMutexDescriptor({CDM::CLibrary, {"pthread_mutex_trylock"}, 1},
-                              {CDM::CLibrary, {"pthread_mutex_unlock"}, 1}),
-      FirstArgMutexDescriptor({CDM::CLibrary, {"mtx_trylock"}, 1},
-                              {CDM::CLibrary, {"mtx_unlock"}, 1}),
-      FirstArgMutexDescriptor({CDM::CLibrary, {"mtx_timedlock"}, 1},
-                              {CDM::CLibrary, {"mtx_unlock"}, 1}),
-      RAIIMutexDescriptor("lock_guard"),
-      RAIIMutexDescriptor("unique_lock")};
-
   const CallDescriptionSet BlockingFunctions{{CDM::CLibrary, {"sleep"}},
                                              {CDM::CLibrary, {"getc"}},
                                              {CDM::CLibrary, {"fgets"}},
@@ -182,147 +41,25 @@ class BlockInCriticalSectionChecker : public Checker<check::PostCall> {
   const BugType BlockInCritSectionBugType{
       this, "Call to blocking function in critical section", "Blocking Error"};
 
-  void reportBlockInCritSection(const CallEvent &call, CheckerContext &C) const;
-
-  [[nodiscard]] const NoteTag *createCritSectionNote(CritSectionMarker M,
-                                                     CheckerContext &C) const;
-
-  [[nodiscard]] std::optional<MutexDescriptor>
-  checkDescriptorMatch(const CallEvent &Call, CheckerContext &C,
-                       bool IsLock) const;
-
-  void handleLock(const MutexDescriptor &Mutex, const CallEvent &Call,
-                  CheckerContext &C) const;
-
-  void handleUnlock(const MutexDescriptor &Mutex, const CallEvent &Call,
-                    CheckerContext &C) const;
-
   [[nodiscard]] bool isBlockingInCritSection(const CallEvent &Call,
                                              CheckerContext &C) const;
 
+  void reportBlockInCritSection(const CallEvent &call, CheckerContext &C) const;
+
 public:
-  /// Process unlock.
-  /// Process lock.
-  /// Process blocking functions (sleep, getc, fgets, read, recv)
+  BlockInCriticalSectionChecker();
   void checkPostCall(const CallEvent &Call, CheckerContext &C) const;
 };
 
 } // end anonymous namespace
 
-REGISTER_LIST_WITH_PROGRAMSTATE(ActiveCritSections, CritSectionMarker)
-
-// Iterator traits for ImmutableList data structure
-// that enable the use of STL algorithms.
-// TODO: Move these to llvm::ImmutableList when overhauling immutable data
-// structures for proper iterator concept support.
-template <>
-struct std::iterator_traits<
-    typename llvm::ImmutableList<CritSectionMarker>::iterator> {
-  using iterator_category = std::forward_iterator_tag;
-  using value_type = CritSectionMarker;
-  using difference_type = std::ptrdiff_t;
-  using reference = CritSectionMarker &;
-  using pointer = CritSectionMarker *;
-};
-
-std::optional<MutexDescriptor>
-BlockInCriticalSectionChecker::checkDescriptorMatch(const CallEvent &Call,
-                                                    CheckerContext &C,
-                                                    bool IsLock) const {
-  const auto Descriptor =
-      llvm::find_if(MutexDescriptors, [&Call, IsLock](auto &&Descriptor) {
-        return std::visit(
-            [&Call, IsLock](auto &&DescriptorImpl) {
-              return DescriptorImpl.matches(Call, IsLock);
-            },
-            Descriptor);
-      });
-  if (Descriptor != MutexDescriptors.end())
-    return *Descriptor;
-  return std::nullopt;
-}
-
-static const MemRegion *skipStdBaseClassRegion(const MemRegion *Reg) {
-  while (Reg) {
-    const auto *BaseClassRegion = dyn_cast<CXXBaseObjectRegion>(Reg);
-    if (!BaseClassRegion || !isWithinStdNamespace(BaseClassRegion->getDecl()))
-      break;
-    Reg = BaseClassRegion->getSuperRegion();
-  }
-  return Reg;
-}
-
-static const MemRegion *getRegion(const CallEvent &Call,
-                                  const MutexDescriptor &Descriptor,
-                                  bool IsLock) {
-  return std::visit(
-      [&Call, IsLock](auto &Descr) -> const MemRegion * {
-        return skipStdBaseClassRegion(Descr.getRegion(Call, IsLock));
-      },
-      Descriptor);
-}
-
-void BlockInCriticalSectionChecker::handleLock(
-    const MutexDescriptor &LockDescriptor, const CallEvent &Call,
-    CheckerContext &C) const {
-  const MemRegion *MutexRegion =
-      getRegion(Call, LockDescriptor, /*IsLock=*/true);
-  if (!MutexRegion)
-    return;
-
-  const CritSectionMarker MarkToAdd{Call.getOriginExpr(), MutexRegion};
-  ProgramStateRef StateWithLockEvent =
-      C.getState()->add<ActiveCritSections>(MarkToAdd);
-  C.addTransition(StateWithLockEvent, createCritSectionNote(MarkToAdd, C));
-}
-
-void BlockInCriticalSectionChecker::handleUnlock(
-    const MutexDescriptor &UnlockDescriptor, const CallEvent &Call,
-    CheckerContext &C) const {
-  const MemRegion *MutexRegion =
-      getRegion(Call, UnlockDescriptor, /*IsLock=*/false);
-  if (!MutexRegion)
-    return;
-
-  ProgramStateRef State = C.getState();
-  const auto ActiveSections = State->get<ActiveCritSections>();
-  const auto MostRecentLock =
-      llvm::find_if(ActiveSections, [MutexRegion](auto &&Marker) {
-        return Marker.LockReg == MutexRegion;
-      });
-  if (MostRecentLock == ActiveSections.end())
-    return;
-
-  // Build a new ImmutableList without this element.
-  auto &Factory = State->get_context<ActiveCritSections>();
-  llvm::ImmutableList<CritSectionMarker> NewList = Factory.getEmptyList();
-  for (auto It = ActiveSections.begin(), End = ActiveSections.end(); It != End;
-       ++It) {
-    if (It != MostRecentLock)
-      NewList = Factory.add(*It, NewList);
-  }
-
-  State = State->set<ActiveCritSections>(NewList);
-  C.addTransition(State);
+BlockInCriticalSectionChecker::BlockInCriticalSectionChecker() {
+  RegisterBugTypeForMutexModeling(&BlockInCritSectionBugType);
 }
 
 bool BlockInCriticalSectionChecker::isBlockingInCritSection(
     const CallEvent &Call, CheckerContext &C) const {
-  return BlockingFunctions.contains(Call) &&
-         !C.getState()->get<ActiveCritSections>().isEmpty();
-}
-
-void BlockInCriticalSectionChecker::checkPostCall(const CallEvent &Call,
-                                                  CheckerContext &C) const {
-  if (isBlockingInCritSection(Call, C)) {
-    reportBlockInCritSection(Call, C);
-  } else if (std::optional<MutexDescriptor> LockDesc =
-                 checkDescriptorMatch(Call, C, /*IsLock=*/true)) {
-    handleLock(*LockDesc, Call, C);
-  } else if (std::optional<MutexDescriptor> UnlockDesc =
-                 checkDescriptorMatch(Call, C, /*IsLock=*/false)) {
-    handleUnlock(*UnlockDesc, Call, C);
-  }
+  return BlockingFunctions.contains(Call) && AreAnyCritsectionsActive(C);
 }
 
 void BlockInCriticalSectionChecker::reportBlockInCritSection(
@@ -342,56 +79,56 @@ void BlockInCriticalSectionChecker::reportBlockInCritSection(
   C.emitReport(std::move(R));
 }
 
-const NoteTag *
-BlockInCriticalSectionChecker::createCritSectionNote(CritSectionMarker M,
-                                                     CheckerContext &C) const {
-  const BugType *BT = &this->BlockInCritSectionBugType;
-  return C.getNoteTag([M, BT](PathSensitiveBugReport &BR,
-                              llvm::raw_ostream &OS) {
-    if (&BR.getBugType() != BT)
-      return;
-
-    // Get the lock events for the mutex of the current line's lock event.
-    const auto CritSectionBegins =
-        BR.getErrorNode()->getState()->get<ActiveCritSections>();
-    llvm::SmallVector<CritSectionMarker, 4> LocksForMutex;
-    llvm::copy_if(
-        CritSectionBegins, std::back_inserter(LocksForMutex),
-        [M](const auto &Marker) { return Marker.LockReg == M.LockReg; });
-    if (LocksForMutex.empty())
-      return;
-
-    // As the ImmutableList builds the locks by prepending them, we
-    // reverse the list to get the correct order.
-    std::reverse(LocksForMutex.begin(), LocksForMutex.end());
-
-    // Find the index of the lock expression in the list of all locks for a
-    // given mutex (in acquisition order).
-    const auto Position =
-        llvm::find_if(std::as_const(LocksForMutex), [M](const auto &Marker) {
-          return Marker.LockExpr == M.LockExpr;
-        });
-    if (Position == LocksForMutex.end())
-      return;
-
-    // If there is only one lock event, we don't need to specify how many times
-    // the critical section was entered.
-    if (LocksForMutex.size() == 1) {
-      OS << "Entering critical section here";
-      return;
-    }
-
-    const auto IndexOfLock =
-        std::distance(std::as_const(LocksForMutex).begin(), Position);
-
-    const auto OrdinalOfLock = IndexOfLock + 1;
-    OS << "Entering critical section for the " << OrdinalOfLock
-       << llvm::getOrdinalSuffix(OrdinalOfLock) << " time here";
-  });
+void BlockInCriticalSectionChecker::checkPostCall(const CallEvent &Call,
+                                                  CheckerContext &C) const {
+  if (!isBlockingInCritSection(Call, C))
+    return;
+  reportBlockInCritSection(Call, C);
 }
 
+// Checker registration
 void ento::registerBlockInCriticalSectionChecker(CheckerManager &mgr) {
   mgr.registerChecker<BlockInCriticalSectionChecker>();
+
+  // Register events for std::mutex lock and unlock
+  // NOTE: There are standard library implementations where some methods
+  // of `std::mutex` are inherited from an implementation detail base
+  // class, and those aren't matched by the name specification {"std",
+  // "mutex", "lock"}.
+  // As a workaround here we omit the class name and only require the
+  // presence of the name parts "std" and "lock"/"unlock".
+  // TODO: Ensure that CallDescription understands inherited methods.
+  RegisterEvent(EventDescriptor{
+      mutex_modeling::MakeMemberExtractor({"std", /*"mutex"*/ "lock"}),
+      EventKind::Acquire, LibraryKind::NotApplicable,
+      SemanticsKind::XNUSemantics});
+  RegisterEvent(EventDescriptor{
+      mutex_modeling::MakeMemberExtractor({"std", /*"mutex"*/ "unlock"}),
+      EventKind::Release});
+
+  // Register events for std::lock_guard
+  RegisterEvent(EventDescriptor{
+      mutex_modeling::MakeRAIILockExtractor("lock_guard"), EventKind::Acquire,
+      LibraryKind::NotApplicable, SemanticsKind::XNUSemantics});
+  RegisterEvent(
+      EventDescriptor{mutex_modeling::MakeRAIIReleaseExtractor("lock_guard"),
+                      EventKind::Release});
+
+  // Register events for std::unique_lock
+  RegisterEvent(EventDescriptor{
+      mutex_modeling::MakeRAIILockExtractor("unique_lock"), EventKind::Acquire,
+      LibraryKind::NotApplicable, SemanticsKind::XNUSemantics});
+  RegisterEvent(
+      EventDescriptor{mutex_modeling::MakeRAIIReleaseExtractor("unique_lock"),
+                      EventKind::Release});
+
+  // Register events for std::scoped_lock
+  RegisterEvent(EventDescriptor{
+      mutex_modeling::MakeRAIILockExtractor("scoped_lock"), EventKind::Acquire,
+      LibraryKind::NotApplicable, SemanticsKind::XNUSemantics});
+  RegisterEvent(
+      EventDescriptor{mutex_modeling::MakeRAIIReleaseExtractor("scoped_lock"),
+                      EventKind::Release});
 }
 
 bool ento::shouldRegisterBlockInCriticalSectionChecker(

>From 9595f3797181500f52025627160c5afa7666a732 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Endre=20F=C3=BCl=C3=B6p?= <endre.fulop at sigmatechnology.com>
Date: Thu, 3 Oct 2024 18:26:55 +0200
Subject: [PATCH 4/5] Update PthreadLockChecker for MutexModeling

This patch updates the PthreadLockChecker to use the new MutexModeling
API.It removes the old mutex modeling logic and replaces it with calls
to thenew API. The checker now handles mutex events through the
centralizedMutexModeling system.
---
 .../Checkers/PthreadLockChecker.cpp           | 755 ++++--------------
 1 file changed, 146 insertions(+), 609 deletions(-)

diff --git a/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
index d6a034f1fdee80..d9e2a0435cf8d6 100644
--- a/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
+++ b/clang/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
@@ -21,248 +21,50 @@
 #include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
 #include "clang/StaticAnalyzer/Core/Checker.h"
 #include "clang/StaticAnalyzer/Core/CheckerManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/CallDescription.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
 
+#include "MutexModeling/MutexModelingAPI.h"
+
 using namespace clang;
 using namespace ento;
+using namespace mutex_modeling;
 
 namespace {
 
-struct LockState {
-  enum Kind {
-    Destroyed,
-    Locked,
-    Unlocked,
-    UntouchedAndPossiblyDestroyed,
-    UnlockedAndPossiblyDestroyed
-  } K;
-
-private:
-  LockState(Kind K) : K(K) {}
-
+class PthreadLockChecker : public Checker<check::PostCall> {
 public:
-  static LockState getLocked() { return LockState(Locked); }
-  static LockState getUnlocked() { return LockState(Unlocked); }
-  static LockState getDestroyed() { return LockState(Destroyed); }
-  static LockState getUntouchedAndPossiblyDestroyed() {
-    return LockState(UntouchedAndPossiblyDestroyed);
-  }
-  static LockState getUnlockedAndPossiblyDestroyed() {
-    return LockState(UnlockedAndPossiblyDestroyed);
-  }
-
-  bool operator==(const LockState &X) const { return K == X.K; }
-
-  bool isLocked() const { return K == Locked; }
-  bool isUnlocked() const { return K == Unlocked; }
-  bool isDestroyed() const { return K == Destroyed; }
-  bool isUntouchedAndPossiblyDestroyed() const {
-    return K == UntouchedAndPossiblyDestroyed;
-  }
-  bool isUnlockedAndPossiblyDestroyed() const {
-    return K == UnlockedAndPossiblyDestroyed;
-  }
-
-  void Profile(llvm::FoldingSetNodeID &ID) const { ID.AddInteger(K); }
-};
-
-class PthreadLockChecker : public Checker<check::PostCall, check::DeadSymbols,
-                                          check::RegionChanges> {
-public:
-  enum LockingSemantics { NotApplicable = 0, PthreadSemantics, XNUSemantics };
+  // Enum to represent different types of lock checkers
   enum CheckerKind {
     CK_PthreadLockChecker,
     CK_FuchsiaLockChecker,
     CK_C11LockChecker,
     CK_NumCheckKinds
   };
+
   bool ChecksEnabled[CK_NumCheckKinds] = {false};
   CheckerNameRef CheckNames[CK_NumCheckKinds];
 
 private:
-  typedef void (PthreadLockChecker::*FnCheck)(const CallEvent &Call,
-                                              CheckerContext &C,
-                                              CheckerKind CheckKind) const;
-  CallDescriptionMap<FnCheck> PThreadCallbacks = {
-      // Init.
-      {{CDM::CLibrary, {"pthread_mutex_init"}, 2},
-       &PthreadLockChecker::InitAnyLock},
-      // TODO: pthread_rwlock_init(2 arguments).
-      // TODO: lck_mtx_init(3 arguments).
-      // TODO: lck_mtx_alloc_init(2 arguments) => returns the mutex.
-      // TODO: lck_rw_init(3 arguments).
-      // TODO: lck_rw_alloc_init(2 arguments) => returns the mutex.
-
-      // Acquire.
-      {{CDM::CLibrary, {"pthread_mutex_lock"}, 1},
-       &PthreadLockChecker::AcquirePthreadLock},
-      {{CDM::CLibrary, {"pthread_rwlock_rdlock"}, 1},
-       &PthreadLockChecker::AcquirePthreadLock},
-      {{CDM::CLibrary, {"pthread_rwlock_wrlock"}, 1},
-       &PthreadLockChecker::AcquirePthreadLock},
-      {{CDM::CLibrary, {"lck_mtx_lock"}, 1},
-       &PthreadLockChecker::AcquireXNULock},
-      {{CDM::CLibrary, {"lck_rw_lock_exclusive"}, 1},
-       &PthreadLockChecker::AcquireXNULock},
-      {{CDM::CLibrary, {"lck_rw_lock_shared"}, 1},
-       &PthreadLockChecker::AcquireXNULock},
-
-      // Try.
-      {{CDM::CLibrary, {"pthread_mutex_trylock"}, 1},
-       &PthreadLockChecker::TryPthreadLock},
-      {{CDM::CLibrary, {"pthread_rwlock_tryrdlock"}, 1},
-       &PthreadLockChecker::TryPthreadLock},
-      {{CDM::CLibrary, {"pthread_rwlock_trywrlock"}, 1},
-       &PthreadLockChecker::TryPthreadLock},
-      {{CDM::CLibrary, {"lck_mtx_try_lock"}, 1},
-       &PthreadLockChecker::TryXNULock},
-      {{CDM::CLibrary, {"lck_rw_try_lock_exclusive"}, 1},
-       &PthreadLockChecker::TryXNULock},
-      {{CDM::CLibrary, {"lck_rw_try_lock_shared"}, 1},
-       &PthreadLockChecker::TryXNULock},
-
-      // Release.
-      {{CDM::CLibrary, {"pthread_mutex_unlock"}, 1},
-       &PthreadLockChecker::ReleaseAnyLock},
-      {{CDM::CLibrary, {"pthread_rwlock_unlock"}, 1},
-       &PthreadLockChecker::ReleaseAnyLock},
-      {{CDM::CLibrary, {"lck_mtx_unlock"}, 1},
-       &PthreadLockChecker::ReleaseAnyLock},
-      {{CDM::CLibrary, {"lck_rw_unlock_exclusive"}, 1},
-       &PthreadLockChecker::ReleaseAnyLock},
-      {{CDM::CLibrary, {"lck_rw_unlock_shared"}, 1},
-       &PthreadLockChecker::ReleaseAnyLock},
-      {{CDM::CLibrary, {"lck_rw_done"}, 1},
-       &PthreadLockChecker::ReleaseAnyLock},
-
-      // Destroy.
-      {{CDM::CLibrary, {"pthread_mutex_destroy"}, 1},
-       &PthreadLockChecker::DestroyPthreadLock},
-      {{CDM::CLibrary, {"lck_mtx_destroy"}, 2},
-       &PthreadLockChecker::DestroyXNULock},
-      // TODO: pthread_rwlock_destroy(1 argument).
-      // TODO: lck_rw_destroy(2 arguments).
-  };
-
-  CallDescriptionMap<FnCheck> FuchsiaCallbacks = {
-      // Init.
-      {{CDM::CLibrary, {"spin_lock_init"}, 1},
-       &PthreadLockChecker::InitAnyLock},
-
-      // Acquire.
-      {{CDM::CLibrary, {"spin_lock"}, 1},
-       &PthreadLockChecker::AcquirePthreadLock},
-      {{CDM::CLibrary, {"spin_lock_save"}, 3},
-       &PthreadLockChecker::AcquirePthreadLock},
-      {{CDM::CLibrary, {"sync_mutex_lock"}, 1},
-       &PthreadLockChecker::AcquirePthreadLock},
-      {{CDM::CLibrary, {"sync_mutex_lock_with_waiter"}, 1},
-       &PthreadLockChecker::AcquirePthreadLock},
-
-      // Try.
-      {{CDM::CLibrary, {"spin_trylock"}, 1},
-       &PthreadLockChecker::TryFuchsiaLock},
-      {{CDM::CLibrary, {"sync_mutex_trylock"}, 1},
-       &PthreadLockChecker::TryFuchsiaLock},
-      {{CDM::CLibrary, {"sync_mutex_timedlock"}, 2},
-       &PthreadLockChecker::TryFuchsiaLock},
-
-      // Release.
-      {{CDM::CLibrary, {"spin_unlock"}, 1},
-       &PthreadLockChecker::ReleaseAnyLock},
-      {{CDM::CLibrary, {"spin_unlock_restore"}, 3},
-       &PthreadLockChecker::ReleaseAnyLock},
-      {{CDM::CLibrary, {"sync_mutex_unlock"}, 1},
-       &PthreadLockChecker::ReleaseAnyLock},
-  };
-
-  CallDescriptionMap<FnCheck> C11Callbacks = {
-      // Init.
-      {{CDM::CLibrary, {"mtx_init"}, 2}, &PthreadLockChecker::InitAnyLock},
-
-      // Acquire.
-      {{CDM::CLibrary, {"mtx_lock"}, 1},
-       &PthreadLockChecker::AcquirePthreadLock},
-
-      // Try.
-      {{CDM::CLibrary, {"mtx_trylock"}, 1}, &PthreadLockChecker::TryC11Lock},
-      {{CDM::CLibrary, {"mtx_timedlock"}, 2}, &PthreadLockChecker::TryC11Lock},
-
-      // Release.
-      {{CDM::CLibrary, {"mtx_unlock"}, 1}, &PthreadLockChecker::ReleaseAnyLock},
-
-      // Destroy
-      {{CDM::CLibrary, {"mtx_destroy"}, 1},
-       &PthreadLockChecker::DestroyPthreadLock},
-  };
-
-  ProgramStateRef resolvePossiblyDestroyedMutex(ProgramStateRef state,
-                                                const MemRegion *lockR,
-                                                const SymbolRef *sym) const;
   void reportBug(CheckerContext &C, std::unique_ptr<BugType> BT[],
                  const Expr *MtxExpr, CheckerKind CheckKind,
                  StringRef Desc) const;
 
-  // Init.
-  void InitAnyLock(const CallEvent &Call, CheckerContext &C,
-                   CheckerKind CheckKind) const;
-  void InitLockAux(const CallEvent &Call, CheckerContext &C,
-                   const Expr *MtxExpr, SVal MtxVal,
-                   CheckerKind CheckKind) const;
-
-  // Lock, Try-lock.
-  void AcquirePthreadLock(const CallEvent &Call, CheckerContext &C,
-                          CheckerKind CheckKind) const;
-  void AcquireXNULock(const CallEvent &Call, CheckerContext &C,
-                      CheckerKind CheckKind) const;
-  void TryPthreadLock(const CallEvent &Call, CheckerContext &C,
-                      CheckerKind CheckKind) const;
-  void TryXNULock(const CallEvent &Call, CheckerContext &C,
-                  CheckerKind CheckKind) const;
-  void TryFuchsiaLock(const CallEvent &Call, CheckerContext &C,
-                      CheckerKind CheckKind) const;
-  void TryC11Lock(const CallEvent &Call, CheckerContext &C,
-                  CheckerKind CheckKind) const;
-  void AcquireLockAux(const CallEvent &Call, CheckerContext &C,
-                      const Expr *MtxExpr, SVal MtxVal, bool IsTryLock,
-                      LockingSemantics Semantics, CheckerKind CheckKind) const;
-
-  // Release.
-  void ReleaseAnyLock(const CallEvent &Call, CheckerContext &C,
-                      CheckerKind CheckKind) const;
-  void ReleaseLockAux(const CallEvent &Call, CheckerContext &C,
-                      const Expr *MtxExpr, SVal MtxVal,
-                      CheckerKind CheckKind) const;
-
-  // Destroy.
-  void DestroyPthreadLock(const CallEvent &Call, CheckerContext &C,
-                          CheckerKind CheckKind) const;
-  void DestroyXNULock(const CallEvent &Call, CheckerContext &C,
-                      CheckerKind CheckKind) const;
-  void DestroyLockAux(const CallEvent &Call, CheckerContext &C,
-                      const Expr *MtxExpr, SVal MtxVal,
-                      LockingSemantics Semantics, CheckerKind CheckKind) const;
-
 public:
   void checkPostCall(const CallEvent &Call, CheckerContext &C) const;
-  void checkDeadSymbols(SymbolReaper &SymReaper, CheckerContext &C) const;
-  ProgramStateRef
-  checkRegionChanges(ProgramStateRef State, const InvalidatedSymbols *Symbols,
-                     ArrayRef<const MemRegion *> ExplicitRegions,
-                     ArrayRef<const MemRegion *> Regions,
-                     const LocationContext *LCtx, const CallEvent *Call) const;
   void printState(raw_ostream &Out, ProgramStateRef State, const char *NL,
                   const char *Sep) const override;
 
 private:
+  // Bug types for different lock-related issues
   mutable std::unique_ptr<BugType> BT_doublelock[CK_NumCheckKinds];
   mutable std::unique_ptr<BugType> BT_doubleunlock[CK_NumCheckKinds];
   mutable std::unique_ptr<BugType> BT_destroylock[CK_NumCheckKinds];
   mutable std::unique_ptr<BugType> BT_initlock[CK_NumCheckKinds];
+  mutable std::unique_ptr<BugType> BT_initlockPthread;
   mutable std::unique_ptr<BugType> BT_lor[CK_NumCheckKinds];
 
+  // Initialize bug types for a specific checker kind
   void initBugType(CheckerKind CheckKind) const {
     if (BT_doublelock[CheckKind])
       return;
@@ -277,377 +79,150 @@ class PthreadLockChecker : public Checker<check::PostCall, check::DeadSymbols,
     BT_lor[CheckKind].reset(new BugType{CheckNames[CheckKind],
                                         "Lock order reversal", "Lock checker"});
   }
-};
-} // end anonymous namespace
-
-// A stack of locks for tracking lock-unlock order.
-REGISTER_LIST_WITH_PROGRAMSTATE(LockSet, const MemRegion *)
-
-// An entry for tracking lock states.
-REGISTER_MAP_WITH_PROGRAMSTATE(LockMap, const MemRegion *, LockState)
-
-// Return values for unresolved calls to pthread_mutex_destroy().
-REGISTER_MAP_WITH_PROGRAMSTATE(DestroyRetVal, const MemRegion *, SymbolRef)
-
-void PthreadLockChecker::checkPostCall(const CallEvent &Call,
-                                       CheckerContext &C) const {
-  // FIXME: Try to handle cases when the implementation was inlined rather
-  // than just giving up.
-  if (C.wasInlined)
-    return;
-
-  if (const FnCheck *Callback = PThreadCallbacks.lookup(Call))
-    (this->**Callback)(Call, C, CK_PthreadLockChecker);
-  else if (const FnCheck *Callback = FuchsiaCallbacks.lookup(Call))
-    (this->**Callback)(Call, C, CK_FuchsiaLockChecker);
-  else if (const FnCheck *Callback = C11Callbacks.lookup(Call))
-    (this->**Callback)(Call, C, CK_C11LockChecker);
-}
-
-// When a lock is destroyed, in some semantics(like PthreadSemantics) we are not
-// sure if the destroy call has succeeded or failed, and the lock enters one of
-// the 'possibly destroyed' state. There is a short time frame for the
-// programmer to check the return value to see if the lock was successfully
-// destroyed. Before we model the next operation over that lock, we call this
-// function to see if the return value was checked by now and set the lock state
-// - either to destroyed state or back to its previous state.
-
-// In PthreadSemantics, pthread_mutex_destroy() returns zero if the lock is
-// successfully destroyed and it returns a non-zero value otherwise.
-ProgramStateRef PthreadLockChecker::resolvePossiblyDestroyedMutex(
-    ProgramStateRef state, const MemRegion *lockR, const SymbolRef *sym) const {
-  const LockState *lstate = state->get<LockMap>(lockR);
-  // Existence in DestroyRetVal ensures existence in LockMap.
-  // Existence in Destroyed also ensures that the lock state for lockR is either
-  // UntouchedAndPossiblyDestroyed or UnlockedAndPossiblyDestroyed.
-  assert(lstate);
-  assert(lstate->isUntouchedAndPossiblyDestroyed() ||
-         lstate->isUnlockedAndPossiblyDestroyed());
-
-  ConstraintManager &CMgr = state->getConstraintManager();
-  ConditionTruthVal retZero = CMgr.isNull(state, *sym);
-  if (retZero.isConstrainedFalse()) {
-    if (lstate->isUntouchedAndPossiblyDestroyed())
-      state = state->remove<LockMap>(lockR);
-    else if (lstate->isUnlockedAndPossiblyDestroyed())
-      state = state->set<LockMap>(lockR, LockState::getUnlocked());
-  } else
-    state = state->set<LockMap>(lockR, LockState::getDestroyed());
-
-  // Removing the map entry (lockR, sym) from DestroyRetVal as the lock state is
-  // now resolved.
-  state = state->remove<DestroyRetVal>(lockR);
-  return state;
-}
-
-void PthreadLockChecker::printState(raw_ostream &Out, ProgramStateRef State,
-                                    const char *NL, const char *Sep) const {
-  LockMapTy LM = State->get<LockMap>();
-  if (!LM.isEmpty()) {
-    Out << Sep << "Mutex states:" << NL;
-    for (auto I : LM) {
-      I.first->dumpToStream(Out);
-      if (I.second.isLocked())
-        Out << ": locked";
-      else if (I.second.isUnlocked())
-        Out << ": unlocked";
-      else if (I.second.isDestroyed())
-        Out << ": destroyed";
-      else if (I.second.isUntouchedAndPossiblyDestroyed())
-        Out << ": not tracked, possibly destroyed";
-      else if (I.second.isUnlockedAndPossiblyDestroyed())
-        Out << ": unlocked, possibly destroyed";
-      Out << NL;
-    }
-  }
-
-  LockSetTy LS = State->get<LockSet>();
-  if (!LS.isEmpty()) {
-    Out << Sep << "Mutex lock order:" << NL;
-    for (auto I : LS) {
-      I->dumpToStream(Out);
-      Out << NL;
-    }
-  }
 
-  DestroyRetValTy DRV = State->get<DestroyRetVal>();
-  if (!DRV.isEmpty()) {
-    Out << Sep << "Mutexes in unresolved possibly destroyed state:" << NL;
-    for (auto I : DRV) {
-      I.first->dumpToStream(Out);
-      Out << ": ";
-      I.second->dumpToStream(Out);
-      Out << NL;
+  // Detect which checker kind should be used based on the event
+  [[nodiscard]] constexpr std::optional<PthreadLockChecker::CheckerKind>
+  detectCheckerKind(mutex_modeling::EventMarker EV) const noexcept {
+    switch (EV.Library) {
+    default:
+      return std::nullopt;
+    case mutex_modeling::LibraryKind::Pthread:
+      return {PthreadLockChecker::CK_PthreadLockChecker};
+    case mutex_modeling::LibraryKind::Fuchsia:
+      return {PthreadLockChecker::CK_FuchsiaLockChecker};
+    case mutex_modeling::LibraryKind::C11:
+      return {PthreadLockChecker::CK_C11LockChecker};
     }
   }
-}
-
-void PthreadLockChecker::AcquirePthreadLock(const CallEvent &Call,
-                                            CheckerContext &C,
-                                            CheckerKind CheckKind) const {
-  AcquireLockAux(Call, C, Call.getArgExpr(0), Call.getArgSVal(0), false,
-                 PthreadSemantics, CheckKind);
-}
 
-void PthreadLockChecker::AcquireXNULock(const CallEvent &Call,
-                                        CheckerContext &C,
-                                        CheckerKind CheckKind) const {
-  AcquireLockAux(Call, C, Call.getArgExpr(0), Call.getArgSVal(0), false,
-                 XNUSemantics, CheckKind);
-}
-
-void PthreadLockChecker::TryPthreadLock(const CallEvent &Call,
-                                        CheckerContext &C,
-                                        CheckerKind CheckKind) const {
-  AcquireLockAux(Call, C, Call.getArgExpr(0), Call.getArgSVal(0), true,
-                 PthreadSemantics, CheckKind);
-}
-
-void PthreadLockChecker::TryXNULock(const CallEvent &Call, CheckerContext &C,
-                                    CheckerKind CheckKind) const {
-  AcquireLockAux(Call, C, Call.getArgExpr(0), Call.getArgSVal(0), true,
-                 PthreadSemantics, CheckKind);
-}
-
-void PthreadLockChecker::TryFuchsiaLock(const CallEvent &Call,
-                                        CheckerContext &C,
-                                        CheckerKind CheckKind) const {
-  AcquireLockAux(Call, C, Call.getArgExpr(0), Call.getArgSVal(0), true,
-                 PthreadSemantics, CheckKind);
-}
+  // Check methods for different types of lock events
+  void checkInitEvent(const EventMarker &LastEvent, CheckerKind Checker,
+                      CheckerContext &C) const;
+  void checkAcquireEvent(const EventMarker &LastEvent, CheckerKind Checker,
+                         CheckerContext &C) const;
+  void checkReleaseEvent(const EventMarker &LastEvent, CheckerKind Checker,
+                         CheckerContext &C) const;
+  void checkDestroyEvent(const EventMarker &LastEvent, CheckerKind Checker,
+                         CheckerContext &C) const;
+};
+} // end anonymous namespace
 
-void PthreadLockChecker::TryC11Lock(const CallEvent &Call, CheckerContext &C,
-                                    CheckerKind CheckKind) const {
-  AcquireLockAux(Call, C, Call.getArgExpr(0), Call.getArgSVal(0), true,
-                 PthreadSemantics, CheckKind);
-}
+void PthreadLockChecker::checkInitEvent(const EventMarker &LastEvent,
+                                        CheckerKind Checker,
+                                        CheckerContext &C) const {
+  ProgramStateRef State = C.getState();
 
-void PthreadLockChecker::AcquireLockAux(const CallEvent &Call,
-                                        CheckerContext &C, const Expr *MtxExpr,
-                                        SVal MtxVal, bool IsTryLock,
-                                        enum LockingSemantics Semantics,
-                                        CheckerKind CheckKind) const {
-  if (!ChecksEnabled[CheckKind])
-    return;
+  const LockStateKind *const LockState =
+      State->get<LockStates>(LastEvent.MutexRegion);
 
-  const MemRegion *lockR = MtxVal.getAsRegion();
-  if (!lockR)
+  if (!LockState) {
     return;
-
-  ProgramStateRef state = C.getState();
-  const SymbolRef *sym = state->get<DestroyRetVal>(lockR);
-  if (sym)
-    state = resolvePossiblyDestroyedMutex(state, lockR, sym);
-
-  if (const LockState *LState = state->get<LockMap>(lockR)) {
-    if (LState->isLocked()) {
-      reportBug(C, BT_doublelock, MtxExpr, CheckKind,
-                "This lock has already been acquired");
-      return;
-    } else if (LState->isDestroyed()) {
-      reportBug(C, BT_destroylock, MtxExpr, CheckKind,
-                "This lock has already been destroyed");
-      return;
-    }
   }
 
-  ProgramStateRef lockSucc = state;
-  if (IsTryLock) {
-    // Bifurcate the state, and allow a mode where the lock acquisition fails.
-    SVal RetVal = Call.getReturnValue();
-    if (auto DefinedRetVal = RetVal.getAs<DefinedSVal>()) {
-      ProgramStateRef lockFail;
-      switch (Semantics) {
-      case PthreadSemantics:
-        std::tie(lockFail, lockSucc) = state->assume(*DefinedRetVal);
-        break;
-      case XNUSemantics:
-        std::tie(lockSucc, lockFail) = state->assume(*DefinedRetVal);
-        break;
-      default:
-        llvm_unreachable("Unknown tryLock locking semantics");
-      }
-      assert(lockFail && lockSucc);
-      C.addTransition(lockFail);
-    }
-    // We might want to handle the case when the mutex lock function was inlined
-    // and returned an Unknown or Undefined value.
-  } else if (Semantics == PthreadSemantics) {
-    // Assume that the return value was 0.
-    SVal RetVal = Call.getReturnValue();
-    if (auto DefinedRetVal = RetVal.getAs<DefinedSVal>()) {
-      // FIXME: If the lock function was inlined and returned true,
-      // we need to behave sanely - at least generate sink.
-      lockSucc = state->assume(*DefinedRetVal, false);
-      assert(lockSucc);
-    }
-    // We might want to handle the case when the mutex lock function was inlined
-    // and returned an Unknown or Undefined value.
-  } else {
-    // XNU locking semantics return void on non-try locks
-    assert((Semantics == XNUSemantics) && "Unknown locking semantics");
-    lockSucc = state;
+  if (*LockState == LockStateKind::Error_DoubleInit) {
+    reportBug(C, BT_initlock, LastEvent.EventExpr, Checker,
+              "This lock has already been initialized");
+  } else if (*LockState == LockStateKind::Error_DoubleInitWhileLocked) {
+    reportBug(C, BT_initlock, LastEvent.EventExpr, Checker,
+              "This lock is still being held");
   }
-
-  // Record that the lock was acquired.
-  lockSucc = lockSucc->add<LockSet>(lockR);
-  lockSucc = lockSucc->set<LockMap>(lockR, LockState::getLocked());
-  C.addTransition(lockSucc);
 }
 
-void PthreadLockChecker::ReleaseAnyLock(const CallEvent &Call,
-                                        CheckerContext &C,
-                                        CheckerKind CheckKind) const {
-  ReleaseLockAux(Call, C, Call.getArgExpr(0), Call.getArgSVal(0), CheckKind);
-}
+void PthreadLockChecker::checkAcquireEvent(const EventMarker &LastEvent,
+                                           CheckerKind Checker,
+                                           CheckerContext &C) const {
+  ProgramStateRef State = C.getState();
 
-void PthreadLockChecker::ReleaseLockAux(const CallEvent &Call,
-                                        CheckerContext &C, const Expr *MtxExpr,
-                                        SVal MtxVal,
-                                        CheckerKind CheckKind) const {
-  if (!ChecksEnabled[CheckKind])
-    return;
+  const LockStateKind *const LockState =
+      State->get<LockStates>(LastEvent.MutexRegion);
 
-  const MemRegion *lockR = MtxVal.getAsRegion();
-  if (!lockR)
+  if (!LockState)
     return;
 
-  ProgramStateRef state = C.getState();
-  const SymbolRef *sym = state->get<DestroyRetVal>(lockR);
-  if (sym)
-    state = resolvePossiblyDestroyedMutex(state, lockR, sym);
-
-  if (const LockState *LState = state->get<LockMap>(lockR)) {
-    if (LState->isUnlocked()) {
-      reportBug(C, BT_doubleunlock, MtxExpr, CheckKind,
-                "This lock has already been unlocked");
-      return;
-    } else if (LState->isDestroyed()) {
-      reportBug(C, BT_destroylock, MtxExpr, CheckKind,
-                "This lock has already been destroyed");
-      return;
-    }
-  }
-
-  LockSetTy LS = state->get<LockSet>();
-
-  if (!LS.isEmpty()) {
-    const MemRegion *firstLockR = LS.getHead();
-    if (firstLockR != lockR) {
-      reportBug(C, BT_lor, MtxExpr, CheckKind,
-                "This was not the most recently acquired lock. Possible lock "
-                "order reversal");
-      return;
-    }
-    // Record that the lock was released.
-    state = state->set<LockSet>(LS.getTail());
+  if (*LockState == LockStateKind::Error_DoubleLock) {
+    reportBug(C, BT_doublelock, LastEvent.EventExpr, Checker,
+              "This lock has already been acquired");
+  } else if (*LockState == LockStateKind::Error_LockDestroyed) {
+    reportBug(C, BT_destroylock, LastEvent.EventExpr, Checker,
+              "This lock has already been destroyed");
   }
-
-  state = state->set<LockMap>(lockR, LockState::getUnlocked());
-  C.addTransition(state);
 }
 
-void PthreadLockChecker::DestroyPthreadLock(const CallEvent &Call,
-                                            CheckerContext &C,
-                                            CheckerKind CheckKind) const {
-  DestroyLockAux(Call, C, Call.getArgExpr(0), Call.getArgSVal(0),
-                 PthreadSemantics, CheckKind);
-}
+void PthreadLockChecker::checkReleaseEvent(const EventMarker &LastEvent,
+                                           CheckerKind Checker,
+                                           CheckerContext &C) const {
+  ProgramStateRef State = C.getState();
 
-void PthreadLockChecker::DestroyXNULock(const CallEvent &Call,
-                                        CheckerContext &C,
-                                        CheckerKind CheckKind) const {
-  DestroyLockAux(Call, C, Call.getArgExpr(0), Call.getArgSVal(0), XNUSemantics,
-                 CheckKind);
-}
+  const LockStateKind *const LockState =
+      State->get<LockStates>(LastEvent.MutexRegion);
 
-void PthreadLockChecker::DestroyLockAux(const CallEvent &Call,
-                                        CheckerContext &C, const Expr *MtxExpr,
-                                        SVal MtxVal,
-                                        enum LockingSemantics Semantics,
-                                        CheckerKind CheckKind) const {
-  if (!ChecksEnabled[CheckKind])
+  if (!LockState)
     return;
 
-  const MemRegion *LockR = MtxVal.getAsRegion();
-  if (!LockR)
-    return;
+  if (*LockState == LockStateKind::Error_DoubleUnlock) {
+    reportBug(C, BT_doubleunlock, LastEvent.EventExpr, Checker,
+              "This lock has already been unlocked");
+  } else if (*LockState == LockStateKind::Error_UnlockDestroyed) {
+    reportBug(C, BT_destroylock, LastEvent.EventExpr, Checker,
+              "This lock has already been destroyed");
+  } else if (*LockState == LockStateKind::Error_LockReversal) {
+    reportBug(C, BT_lor, LastEvent.EventExpr, Checker,
+              "This was not the most recently acquired lock. Possible lock "
+              "order reversal");
+  }
+}
 
+void PthreadLockChecker::checkDestroyEvent(const EventMarker &LastEvent,
+                                           CheckerKind Checker,
+                                           CheckerContext &C) const {
   ProgramStateRef State = C.getState();
 
-  const SymbolRef *sym = State->get<DestroyRetVal>(LockR);
-  if (sym)
-    State = resolvePossiblyDestroyedMutex(State, LockR, sym);
-
-  const LockState *LState = State->get<LockMap>(LockR);
-  // Checking the return value of the destroy method only in the case of
-  // PthreadSemantics
-  if (Semantics == PthreadSemantics) {
-    if (!LState || LState->isUnlocked()) {
-      SymbolRef sym = Call.getReturnValue().getAsSymbol();
-      if (!sym) {
-        State = State->remove<LockMap>(LockR);
-        C.addTransition(State);
-        return;
-      }
-      State = State->set<DestroyRetVal>(LockR, sym);
-      if (LState && LState->isUnlocked())
-        State = State->set<LockMap>(
-            LockR, LockState::getUnlockedAndPossiblyDestroyed());
-      else
-        State = State->set<LockMap>(
-            LockR, LockState::getUntouchedAndPossiblyDestroyed());
-      C.addTransition(State);
-      return;
-    }
-  } else {
-    if (!LState || LState->isUnlocked()) {
-      State = State->set<LockMap>(LockR, LockState::getDestroyed());
-      C.addTransition(State);
-      return;
-    }
-  }
+  const LockStateKind *const LockState =
+      State->get<LockStates>(LastEvent.MutexRegion);
 
-  StringRef Message = LState->isLocked()
-                          ? "This lock is still locked"
-                          : "This lock has already been destroyed";
+  if (!LockState || *LockState == LockStateKind::Destroyed)
+    return;
 
-  reportBug(C, BT_destroylock, MtxExpr, CheckKind, Message);
+  if (*LockState == LockStateKind::Error_DestroyLocked) {
+    reportBug(C, BT_destroylock, LastEvent.EventExpr, Checker,
+              "This lock is still locked");
+  } else if (*LockState == LockStateKind::Error_DoubleDestroy)
+    reportBug(C, BT_destroylock, LastEvent.EventExpr, Checker,
+              "This lock has already been destroyed");
 }
 
-void PthreadLockChecker::InitAnyLock(const CallEvent &Call, CheckerContext &C,
-                                     CheckerKind CheckKind) const {
-  InitLockAux(Call, C, Call.getArgExpr(0), Call.getArgSVal(0), CheckKind);
-}
+void PthreadLockChecker::checkPostCall(const CallEvent &Call,
+                                       CheckerContext &C) const {
 
-void PthreadLockChecker::InitLockAux(const CallEvent &Call, CheckerContext &C,
-                                     const Expr *MtxExpr, SVal MtxVal,
-                                     CheckerKind CheckKind) const {
-  if (!ChecksEnabled[CheckKind])
-    return;
+  ProgramStateRef State = C.getState();
+
+  const auto &MTXEvents = State->get<MutexEvents>();
 
-  const MemRegion *LockR = MtxVal.getAsRegion();
-  if (!LockR)
+  if (MTXEvents.isEmpty())
     return;
 
-  ProgramStateRef State = C.getState();
+  const auto &LastEvent = MTXEvents.getHead();
 
-  const SymbolRef *sym = State->get<DestroyRetVal>(LockR);
-  if (sym)
-    State = resolvePossiblyDestroyedMutex(State, LockR, sym);
+  std::optional<CheckerKind> Checker = detectCheckerKind(LastEvent);
 
-  const struct LockState *LState = State->get<LockMap>(LockR);
-  if (!LState || LState->isDestroyed()) {
-    State = State->set<LockMap>(LockR, LockState::getUnlocked());
-    C.addTransition(State);
+  if (!Checker || !ChecksEnabled[*Checker])
     return;
-  }
 
-  StringRef Message = LState->isLocked()
-                          ? "This lock is still being held"
-                          : "This lock has already been initialized";
-
-  reportBug(C, BT_initlock, MtxExpr, CheckKind, Message);
+  switch (LastEvent.Kind) {
+  case EventKind::Init:
+    checkInitEvent(LastEvent, *Checker, C);
+    break;
+  case EventKind::Acquire:
+  case EventKind::TryAcquire:
+    checkAcquireEvent(LastEvent, *Checker, C);
+    break;
+  case EventKind::Release:
+    checkReleaseEvent(LastEvent, *Checker, C);
+    break;
+  case EventKind::Destroy:
+    checkDestroyEvent(LastEvent, *Checker, C);
+    break;
+  }
 }
 
 void PthreadLockChecker::reportBug(CheckerContext &C,
@@ -664,86 +239,48 @@ void PthreadLockChecker::reportBug(CheckerContext &C,
   C.emitReport(std::move(Report));
 }
 
-void PthreadLockChecker::checkDeadSymbols(SymbolReaper &SymReaper,
-                                          CheckerContext &C) const {
-  ProgramStateRef State = C.getState();
-
-  for (auto I : State->get<DestroyRetVal>()) {
-    // Once the return value symbol dies, no more checks can be performed
-    // against it. See if the return value was checked before this point.
-    // This would remove the symbol from the map as well.
-    if (SymReaper.isDead(I.second))
-      State = resolvePossiblyDestroyedMutex(State, I.first, &I.second);
-  }
-
-  for (auto I : State->get<LockMap>()) {
-    // Stop tracking dead mutex regions as well.
-    if (!SymReaper.isLiveRegion(I.first)) {
-      State = State->remove<LockMap>(I.first);
-      State = State->remove<DestroyRetVal>(I.first);
-    }
-  }
-
-  // TODO: We probably need to clean up the lock stack as well.
-  // It is tricky though: even if the mutex cannot be unlocked anymore,
-  // it can still participate in lock order reversal resolution.
+void PthreadLockChecker::printState(raw_ostream &Out, ProgramStateRef State,
+                                    const char *NL, const char *Sep) const {
+  mutex_modeling::printState(Out, State, NL, Sep);
+}
 
-  C.addTransition(State);
+void ento::registerPthreadLockBase(CheckerManager &mgr) {
+  mgr.registerChecker<PthreadLockChecker>();
 }
 
-ProgramStateRef PthreadLockChecker::checkRegionChanges(
-    ProgramStateRef State, const InvalidatedSymbols *Symbols,
-    ArrayRef<const MemRegion *> ExplicitRegions,
-    ArrayRef<const MemRegion *> Regions, const LocationContext *LCtx,
-    const CallEvent *Call) const {
-
-  bool IsLibraryFunction = false;
-  if (Call && Call->isGlobalCFunction()) {
-    // Avoid invalidating mutex state when a known supported function is called.
-    if (PThreadCallbacks.lookup(*Call) || FuchsiaCallbacks.lookup(*Call) ||
-        C11Callbacks.lookup(*Call))
-      return State;
-
-    if (Call->isInSystemHeader())
-      IsLibraryFunction = true;
-  }
+bool ento::shouldRegisterPthreadLockBase(const CheckerManager &mgr) {
+  return true;
+}
 
-  for (auto R : Regions) {
-    // We assume that system library function wouldn't touch the mutex unless
-    // it takes the mutex explicitly as an argument.
-    // FIXME: This is a bit quadratic.
-    if (IsLibraryFunction && !llvm::is_contained(ExplicitRegions, R))
-      continue;
+void ento::registerPthreadLockChecker(CheckerManager &CM) {
+  PthreadLockChecker *ImplChecker = CM.getChecker<PthreadLockChecker>();
+  ImplChecker->ChecksEnabled[PthreadLockChecker::CK_PthreadLockChecker] = true;
+  ImplChecker->CheckNames[PthreadLockChecker::CK_PthreadLockChecker] =
+      CM.getCurrentCheckerName();
+}
 
-    State = State->remove<LockMap>(R);
-    State = State->remove<DestroyRetVal>(R);
+bool ento::shouldRegisterPthreadLockChecker(const CheckerManager &CM) {
+  return true;
+}
 
-    // TODO: We need to invalidate the lock stack as well. This is tricky
-    // to implement correctly and efficiently though, because the effects
-    // of mutex escapes on lock order may be fairly varied.
-  }
+void ento::registerFuchsiaLockChecker(CheckerManager &CM) {
+  PthreadLockChecker *ImplChecker = CM.getChecker<PthreadLockChecker>();
+  ImplChecker->ChecksEnabled[PthreadLockChecker::CK_FuchsiaLockChecker] = true;
+  ImplChecker->CheckNames[PthreadLockChecker::CK_FuchsiaLockChecker] =
+      CM.getCurrentCheckerName();
+}
 
-  return State;
+bool ento::shouldRegisterFuchsiaLockChecker(const CheckerManager &CM) {
+  return true;
 }
 
-void ento::registerPthreadLockBase(CheckerManager &mgr) {
-  mgr.registerChecker<PthreadLockChecker>();
+void ento::registerC11LockChecker(CheckerManager &CM) {
+  PthreadLockChecker *ImplChecker = CM.getChecker<PthreadLockChecker>();
+  ImplChecker->ChecksEnabled[PthreadLockChecker::CK_C11LockChecker] = true;
+  ImplChecker->CheckNames[PthreadLockChecker::CK_C11LockChecker] =
+      CM.getCurrentCheckerName();
 }
 
-bool ento::shouldRegisterPthreadLockBase(const CheckerManager &mgr) {
+bool ento::shouldRegisterC11LockChecker(const CheckerManager &CM) {
   return true;
 }
-
-#define REGISTER_CHECKER(name)                                                 \
-  void ento::register##name(CheckerManager &mgr) {                             \
-    PthreadLockChecker *checker = mgr.getChecker<PthreadLockChecker>();        \
-    checker->ChecksEnabled[PthreadLockChecker::CK_##name] = true;              \
-    checker->CheckNames[PthreadLockChecker::CK_##name] =                       \
-        mgr.getCurrentCheckerName();                                           \
-  }                                                                            \
-                                                                               \
-  bool ento::shouldRegister##name(const CheckerManager &mgr) { return true; }
-
-REGISTER_CHECKER(PthreadLockChecker)
-REGISTER_CHECKER(FuchsiaLockChecker)
-REGISTER_CHECKER(C11LockChecker)

>From 5f80c4a04cd77cae5b9af14eca8b134c582557e5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Endre=20F=C3=BCl=C3=B6p?= <endre.fulop at sigmatechnology.com>
Date: Thu, 3 Oct 2024 18:27:56 +0200
Subject: [PATCH 5/5] Update tests for MutexModeling

This patch updates the existing tests to reflect the changes made to
themutex modeling system. It modifies the expected output for various
testcases to match the new MutexModeling API and the updated checker
behavior.
---
 .../test/Analysis/analyzer-enabled-checkers.c |  1 +
 .../Analysis/block-in-critical-section.cpp    | 21 +++-----
 clang/test/Analysis/pthreadlock_state.c       | 53 +++++++++++++++++--
 .../Analysis/pthreadlock_state_nottracked.c   |  5 ++
 ...c-library-functions-arg-enabled-checkers.c |  1 +
 5 files changed, 63 insertions(+), 18 deletions(-)

diff --git a/clang/test/Analysis/analyzer-enabled-checkers.c b/clang/test/Analysis/analyzer-enabled-checkers.c
index e605c62a66ad0e..d02e88def01457 100644
--- a/clang/test/Analysis/analyzer-enabled-checkers.c
+++ b/clang/test/Analysis/analyzer-enabled-checkers.c
@@ -16,6 +16,7 @@
 // CHECK-NEXT: core.CallAndMessage
 // CHECK-NEXT: core.DivideZero
 // CHECK-NEXT: core.DynamicTypePropagation
+// CHECK-NEXT: core.MutexModeling
 // CHECK-NEXT: core.NonNullParamChecker
 // CHECK-NEXT: core.NonnilStringConstants
 // CHECK-NEXT: core.NullDereference
diff --git a/clang/test/Analysis/block-in-critical-section.cpp b/clang/test/Analysis/block-in-critical-section.cpp
index ee9a708f231a86..cd5fa1edcbea71 100644
--- a/clang/test/Analysis/block-in-critical-section.cpp
+++ b/clang/test/Analysis/block-in-critical-section.cpp
@@ -41,8 +41,9 @@ int pthread_mutex_trylock(pthread_mutex_t *mutex);
 int pthread_mutex_unlock(pthread_mutex_t *mutex);
 
 struct mtx_t;
+struct timespec;
 int mtx_lock(mtx_t *mutex);
-int mtx_timedlock(mtx_t *mutex);
+int mtx_timedlock(mtx_t *mutex, const struct timespec *ts);
 int mtx_trylock(mtx_t *mutex);
 int mtx_unlock(mtx_t *mutex);
 
@@ -100,7 +101,7 @@ void testBlockInCriticalSectionWithPthreadMutex(pthread_mutex_t *mutex) {
   pthread_mutex_unlock(mutex);
 }
 
-void testBlockInCriticalSectionC11Locks(mtx_t *mutex) {
+void testBlockInCriticalSectionC11Locks(mtx_t *mutex, timespec *ts) {
   mtx_lock(mutex); // expected-note 5{{Entering critical section here}}
   sleep(3); // expected-warning {{Call to blocking function 'sleep' inside of critical section}}
             // expected-note at -1 {{Call to blocking function 'sleep' inside of critical section}}
@@ -114,7 +115,7 @@ void testBlockInCriticalSectionC11Locks(mtx_t *mutex) {
           // expected-note at -1 {{Call to blocking function 'recv' inside of critical section}}
   mtx_unlock(mutex);
 
-  mtx_timedlock(mutex); // expected-note 5{{Entering critical section here}}
+  mtx_timedlock(mutex, ts); // expected-note 5{{Entering critical section here}}
   sleep(3); // expected-warning {{Call to blocking function 'sleep' inside of critical section}}
             // expected-note at -1 {{Call to blocking function 'sleep' inside of critical section}}
   getc(stream); // expected-warning {{Call to blocking function 'getc' inside of critical section}}
@@ -293,19 +294,13 @@ void testBlockInCriticalSectionUniqueLockNested() {
   sleep(1); // no-warning
 }
 
-void testTrylockCurrentlyFalsePositive(pthread_mutex_t *m) {
-                                       // expected-note at +4 {{Assuming the condition is true}}
-                                       // expected-note at +3 {{Taking true branch}}
-                                       // expected-note at +2 {{Assuming the condition is false}}
-                                       // expected-note at +1 {{Taking false branch}}
-  if (pthread_mutex_trylock(m) == 0) { // expected-note 2 {{Entering critical section here}}
-                                       // FIXME: we are entering the critical section only in the true branch
+void testTrylockStateSplitting(pthread_mutex_t *m) {
+                                       // expected-note at +1 {{Taking true branch}}
+  if (pthread_mutex_trylock(m) == 0) { // expected-note {{Entering critical section here}}
     sleep(10); // expected-warning {{Call to blocking function 'sleep' inside of critical section}}
                // expected-note at -1 {{Call to blocking function 'sleep' inside of critical section}}
     pthread_mutex_unlock(m);
   } else {
-    sleep(10); // expected-warning {{Call to blocking function 'sleep' inside of critical section}}
-               // expected-note at -1 {{Call to blocking function 'sleep' inside of critical section}}
-               // FIXME: this is a false positive, the lock was not acquired
+    sleep(10); // no-warning
   }
 }
diff --git a/clang/test/Analysis/pthreadlock_state.c b/clang/test/Analysis/pthreadlock_state.c
index ffbb33f6beaf7a..eab1b468aceeb9 100644
--- a/clang/test/Analysis/pthreadlock_state.c
+++ b/clang/test/Analysis/pthreadlock_state.c
@@ -15,24 +15,49 @@ void test(void) {
   pthread_mutex_init(&mtx, NULL);
   clang_analyzer_printState();
   // CHECK:    { "checker": "alpha.core.PthreadLockBase", "messages": [
-  // CHECK-NEXT:      "Mutex states:",
-  // CHECK-NEXT:      "mtx: unlocked",
+  // CHECK-NEXT:      "Mutex event:", 
+  // CHECK-NEXT:      "Kind: : Init", 
+  // CHECK-NEXT:      "Semantics: NotApplicable", 
+  // CHECK-NEXT:      "Library: Pthread", 
+  // CHECK-NEXT:      "Mutex region: mtx", 
+  // CHECK-NEXT:      "Mutex states:", 
+  // CHECK-NEXT:      "mtx: unlocked", 
   // CHECK-NEXT:      ""
   // CHECK-NEXT:    ]}
 
   pthread_mutex_lock(&mtx);
   clang_analyzer_printState();
   // CHECK:    { "checker": "alpha.core.PthreadLockBase", "messages": [
+  // CHECK-NEXT:      "Mutex event:", 
+  // CHECK-NEXT:      "Kind: : Acquire", 
+  // CHECK-NEXT:      "Semantics: PthreadSemantics", 
+  // CHECK-NEXT:      "Library: Pthread", 
+  // CHECK-NEXT:      "Mutex region: mtx", 
+  // CHECK-NEXT:      "Kind: : Init", 
+  // CHECK-NEXT:      "Semantics: NotApplicable", 
+  // CHECK-NEXT:      "Library: Pthread", 
+  // CHECK-NEXT:      "Mutex region: mtx", 
   // CHECK-NEXT:      "Mutex states:",
   // CHECK-NEXT:      "mtx: locked",
-  // CHECK-NEXT:      "Mutex lock order:",
-  // CHECK-NEXT:      "mtx",
   // CHECK-NEXT:      ""
   // CHECK-NEXT:    ]}
 
   pthread_mutex_unlock(&mtx);
   clang_analyzer_printState();
   // CHECK:    { "checker": "alpha.core.PthreadLockBase", "messages": [
+  // CHECK-NEXT:      "Mutex event:", 
+  // CHECK-NEXT:      "Kind: : Release", 
+  // CHECK-NEXT:      "Semantics: NotApplicable",
+  // CHECK-NEXT:      "Library: Pthread", 
+  // CHECK-NEXT:      "Mutex region: mtx", 
+  // CHECK-NEXT:      "Kind: : Acquire", 
+  // CHECK-NEXT:      "Semantics: PthreadSemantics", 
+  // CHECK-NEXT:      "Library: Pthread", 
+  // CHECK-NEXT:      "Mutex region: mtx", 
+  // CHECK-NEXT:      "Kind: : Init", 
+  // CHECK-NEXT:      "Semantics: NotApplicable", 
+  // CHECK-NEXT:      "Library: Pthread", 
+  // CHECK-NEXT:      "Mutex region: mtx", 
   // CHECK-NEXT:      "Mutex states:",
   // CHECK-NEXT:      "mtx: unlocked",
   // CHECK-NEXT:      ""
@@ -41,6 +66,23 @@ void test(void) {
   int ret = pthread_mutex_destroy(&mtx);
   clang_analyzer_printState();
   // CHECK:    { "checker": "alpha.core.PthreadLockBase", "messages": [
+  // CHECK-NEXT:      "Mutex event:", 
+  // CHECK-NEXT:      "Kind: : Destroy", 
+  // CHECK-NEXT:      "Semantics: PthreadSemantics",
+  // CHECK-NEXT:      "Library: Pthread", 
+  // CHECK-NEXT:      "Mutex region: mtx", 
+  // CHECK-NEXT:      "Kind: : Release", 
+  // CHECK-NEXT:      "Semantics: NotApplicable",
+  // CHECK-NEXT:      "Library: Pthread", 
+  // CHECK-NEXT:      "Mutex region: mtx", 
+  // CHECK-NEXT:      "Kind: : Acquire", 
+  // CHECK-NEXT:      "Semantics: PthreadSemantics", 
+  // CHECK-NEXT:      "Library: Pthread", 
+  // CHECK-NEXT:      "Mutex region: mtx", 
+  // CHECK-NEXT:      "Kind: : Init", 
+  // CHECK-NEXT:      "Semantics: NotApplicable", 
+  // CHECK-NEXT:      "Library: Pthread", 
+  // CHECK-NEXT:      "Mutex region: mtx", 
   // CHECK-NEXT:      "Mutex states:",
   // CHECK-NEXT:      "mtx: unlocked, possibly destroyed",
   // CHECK-NEXT:      "Mutexes in unresolved possibly destroyed state:",
@@ -51,9 +93,10 @@ void test(void) {
   if (ret)
     return;
 
+  // Assert that the 'possibly destroyed' state is now resolved to 'destroyed'.
   clang_analyzer_printState();
   // CHECK:    { "checker": "alpha.core.PthreadLockBase", "messages": [
-  // CHECK-NEXT:      "Mutex states:",
+  // CHECK:           "Mutex states:",
   // CHECK-NEXT:      "mtx: destroyed",
   // CHECK-NEXT:      ""
   // CHECK-NEXT:    ]}
diff --git a/clang/test/Analysis/pthreadlock_state_nottracked.c b/clang/test/Analysis/pthreadlock_state_nottracked.c
index 44023e7fc15c47..7788377069eb88 100644
--- a/clang/test/Analysis/pthreadlock_state_nottracked.c
+++ b/clang/test/Analysis/pthreadlock_state_nottracked.c
@@ -10,6 +10,11 @@ void test(pthread_mutex_t *mtx) {
   int ret = pthread_mutex_destroy(mtx);
   clang_analyzer_printState();
   // CHECK:    { "checker": "alpha.core.PthreadLockBase", "messages": [
+  // CHECK-NEXT:      "Mutex event:", 
+  // CHECK-NEXT:      "Kind: : Destroy", 
+  // CHECK-NEXT:      "Semantics: PthreadSemantics", 
+  // CHECK-NEXT:      "Library: Pthread", 
+  // CHECK-NEXT:      "Mutex region: SymRegion{reg_$[[REG:[0-9]+]]<pthread_mutex_t * mtx>}", 
   // CHECK-NEXT:      "Mutex states:",
   // CHECK-NEXT:      "SymRegion{reg_$[[REG:[0-9]+]]<pthread_mutex_t * mtx>}: not tracked, possibly destroyed",
   // CHECK-NEXT:      "Mutexes in unresolved possibly destroyed state:",
diff --git a/clang/test/Analysis/std-c-library-functions-arg-enabled-checkers.c b/clang/test/Analysis/std-c-library-functions-arg-enabled-checkers.c
index 345a4e8f44efd1..711567671613b3 100644
--- a/clang/test/Analysis/std-c-library-functions-arg-enabled-checkers.c
+++ b/clang/test/Analysis/std-c-library-functions-arg-enabled-checkers.c
@@ -24,6 +24,7 @@
 // CHECK-NEXT: core.CallAndMessage
 // CHECK-NEXT: core.DivideZero
 // CHECK-NEXT: core.DynamicTypePropagation
+// CHECK-NEXT: core.MutexModeling
 // CHECK-NEXT: core.NonNullParamChecker
 // CHECK-NEXT: core.NonnilStringConstants
 // CHECK-NEXT: core.NullDereference



More information about the cfe-commits mailing list