[clang] [clang][analyzer] Introduce MutexModeling checker (PR #111381)

Endre Fülöp via cfe-commits cfe-commits at lists.llvm.org
Mon Oct 7 07:43:53 PDT 2024


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

>From 4af2c63e4e65b1a8dd9947afdd09fe18362f5cfe 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/2] [clang][analyzer] 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 ++++
 7 files changed, 1457 insertions(+)
 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

>From 36039a46961fb2bbb273f08d859993a85c18f8b2 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 2/2] 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.
---
 clang/test/Analysis/analyzer-enabled-checkers.c                  | 1 +
 .../test/Analysis/std-c-library-functions-arg-enabled-checkers.c | 1 +
 2 files changed, 2 insertions(+)

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/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