lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp - clang - Git at Google

 //===--- PthreadLockChecker.cpp - Check for locking problems ---*- C++ -*--===//
 //
 // 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
 //
 //===----------------------------------------------------------------------===//
 //
 // This defines PthreadLockChecker, a simple lock -> unlock checker.
 // Also handles XNU locks, which behave similarly enough to share code.
 //
 //===----------------------------------------------------------------------===//

 #include "clang/StaticAnalyzer/Checkers/BuiltinCheckerRegistration.h"
 #include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
 #include "clang/StaticAnalyzer/Core/Checker.h"
 #include "clang/StaticAnalyzer/Core/CheckerManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"

 using namespace clang;
 using namespace ento;

 namespace {

 struct LockState {
   enum Kind {
     Destroyed,
     Locked,
     Unlocked,
     UntouchedAndPossiblyDestroyed,
     UnlockedAndPossiblyDestroyed
   } K;

 private:
   LockState(Kind K) : K(K) {}

 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::PostStmt<CallExpr>, check::DeadSymbols> {
   mutable std::unique_ptr<BugType> BT_doublelock;
   mutable std::unique_ptr<BugType> BT_doubleunlock;
   mutable std::unique_ptr<BugType> BT_destroylock;
   mutable std::unique_ptr<BugType> BT_initlock;
   mutable std::unique_ptr<BugType> BT_lor;
   enum LockingSemantics {
     NotApplicable = 0,
     PthreadSemantics,
     XNUSemantics
   };
 public:
   void checkPostStmt(const CallExpr *CE, CheckerContext &C) const;
   void checkDeadSymbols(SymbolReaper &SymReaper, CheckerContext &C) const;
   void printState(raw_ostream &Out, ProgramStateRef State,
                   const char *NL, const char *Sep) const override;

   void AcquireLock(CheckerContext &C, const CallExpr *CE, SVal lock,
                    bool isTryLock, enum LockingSemantics semantics) const;

   void ReleaseLock(CheckerContext &C, const CallExpr *CE, SVal lock) const;
   void DestroyLock(CheckerContext &C, const CallExpr *CE, SVal Lock,
                    enum LockingSemantics semantics) const;
   void InitLock(CheckerContext &C, const CallExpr *CE, SVal Lock) const;
   void reportUseDestroyedBug(CheckerContext &C, const CallExpr *CE) const;
   ProgramStateRef resolvePossiblyDestroyedMutex(ProgramStateRef state,
                                                 const MemRegion *lockR,
                                                 const SymbolRef *sym) const;
 };
 } // 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::checkPostStmt(const CallExpr *CE,
                                        CheckerContext &C) const {
   StringRef FName = C.getCalleeName(CE);
   if (FName.empty())
     return;

   if (CE->getNumArgs() != 1 && CE->getNumArgs() != 2)
     return;

   if (FName == "pthread_mutex_lock" ||
       FName == "pthread_rwlock_rdlock" ||
       FName == "pthread_rwlock_wrlock")
     AcquireLock(C, CE, C.getSVal(CE->getArg(0)), false, PthreadSemantics);
   else if (FName == "lck_mtx_lock" ||
            FName == "lck_rw_lock_exclusive" ||
            FName == "lck_rw_lock_shared")
     AcquireLock(C, CE, C.getSVal(CE->getArg(0)), false, XNUSemantics);
   else if (FName == "pthread_mutex_trylock" ||
            FName == "pthread_rwlock_tryrdlock" ||
            FName == "pthread_rwlock_trywrlock")
     AcquireLock(C, CE, C.getSVal(CE->getArg(0)),
                 true, PthreadSemantics);
   else if (FName == "lck_mtx_try_lock" ||
            FName == "lck_rw_try_lock_exclusive" ||
            FName == "lck_rw_try_lock_shared")
     AcquireLock(C, CE, C.getSVal(CE->getArg(0)), true, XNUSemantics);
   else if (FName == "pthread_mutex_unlock" ||
            FName == "pthread_rwlock_unlock" ||
            FName == "lck_mtx_unlock" ||
            FName == "lck_rw_done")
     ReleaseLock(C, CE, C.getSVal(CE->getArg(0)));
   else if (FName == "pthread_mutex_destroy")
     DestroyLock(C, CE, C.getSVal(CE->getArg(0)), PthreadSemantics);
   else if (FName == "lck_mtx_destroy")
     DestroyLock(C, CE, C.getSVal(CE->getArg(0)), XNUSemantics);
   else if (FName == "pthread_mutex_init")
     InitLock(C, CE, C.getSVal(CE->getArg(0)));
 }

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

   // TODO: Dump destroyed mutex symbols?
 }

 void PthreadLockChecker::AcquireLock(CheckerContext &C, const CallExpr *CE,
                                      SVal lock, bool isTryLock,
                                      enum LockingSemantics semantics) const {

   const MemRegion *lockR = lock.getAsRegion();
   if (!lockR)
     return;

   ProgramStateRef state = C.getState();
   const SymbolRef *sym = state->get<DestroyRetVal>(lockR);
   if (sym)
     state = resolvePossiblyDestroyedMutex(state, lockR, sym);

   SVal X = C.getSVal(CE);
   if (X.isUnknownOrUndef())
     return;

   DefinedSVal retVal = X.castAs<DefinedSVal>();

   if (const LockState *LState = state->get<LockMap>(lockR)) {
     if (LState->isLocked()) {
       if (!BT_doublelock)
         BT_doublelock.reset(new BugType(this, "Double locking",
                                         "Lock checker"));
       ExplodedNode *N = C.generateErrorNode();
       if (!N)
         return;
       auto report = std::make_unique<PathSensitiveBugReport>(
           *BT_doublelock, "This lock has already been acquired", N);
       report->addRange(CE->getArg(0)->getSourceRange());
       C.emitReport(std::move(report));
       return;
     } else if (LState->isDestroyed()) {
       reportUseDestroyedBug(C, CE);
       return;
     }
   }

   ProgramStateRef lockSucc = state;
   if (isTryLock) {
     // Bifurcate the state, and allow a mode where the lock acquisition fails.
     ProgramStateRef lockFail;
     switch (semantics) {
     case PthreadSemantics:
       std::tie(lockFail, lockSucc) = state->assume(retVal);
       break;
     case XNUSemantics:
       std::tie(lockSucc, lockFail) = state->assume(retVal);
       break;
     default:
       llvm_unreachable("Unknown tryLock locking semantics");
     }
     assert(lockFail && lockSucc);
     C.addTransition(lockFail);

   } else if (semantics == PthreadSemantics) {
     // Assume that the return value was 0.
     lockSucc = state->assume(retVal, false);
     assert(lockSucc);

   } else {
     // XNU locking semantics return void on non-try locks
     assert((semantics == XNUSemantics) && "Unknown locking semantics");
     lockSucc = state;
   }

   // Record that the lock was acquired.
   lockSucc = lockSucc->add<LockSet>(lockR);
   lockSucc = lockSucc->set<LockMap>(lockR, LockState::getLocked());
   C.addTransition(lockSucc);
 }

 void PthreadLockChecker::ReleaseLock(CheckerContext &C, const CallExpr *CE,
                                      SVal lock) const {

   const MemRegion *lockR = lock.getAsRegion();
   if (!lockR)
     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()) {
       if (!BT_doubleunlock)
         BT_doubleunlock.reset(new BugType(this, "Double unlocking",
                                           "Lock checker"));
       ExplodedNode *N = C.generateErrorNode();
       if (!N)
         return;
       auto Report = std::make_unique<PathSensitiveBugReport>(
           *BT_doubleunlock, "This lock has already been unlocked", N);
       Report->addRange(CE->getArg(0)->getSourceRange());
       C.emitReport(std::move(Report));
       return;
     } else if (LState->isDestroyed()) {
       reportUseDestroyedBug(C, CE);
       return;
     }
   }

   LockSetTy LS = state->get<LockSet>();

   // FIXME: Better analysis requires IPA for wrappers.

   if (!LS.isEmpty()) {
     const MemRegion *firstLockR = LS.getHead();
     if (firstLockR != lockR) {
       if (!BT_lor)
         BT_lor.reset(new BugType(this, "Lock order reversal", "Lock checker"));
       ExplodedNode *N = C.generateErrorNode();
       if (!N)
         return;
       auto report = std::make_unique<PathSensitiveBugReport>(
           *BT_lor, "This was not the most recently acquired lock. Possible "
                    "lock order reversal", N);
       report->addRange(CE->getArg(0)->getSourceRange());
       C.emitReport(std::move(report));
       return;
     }
     // Record that the lock was released.
     state = state->set<LockSet>(LS.getTail());
   }

   state = state->set<LockMap>(lockR, LockState::getUnlocked());
   C.addTransition(state);
 }

 void PthreadLockChecker::DestroyLock(CheckerContext &C, const CallExpr *CE,
                                      SVal Lock,
                                      enum LockingSemantics semantics) const {

   const MemRegion *LockR = Lock.getAsRegion();
   if (!LockR)
     return;

   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 = C.getSVal(CE).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;
     }
   }
   StringRef Message;

   if (LState->isLocked()) {
     Message = "This lock is still locked";
   } else {
     Message = "This lock has already been destroyed";
   }

   if (!BT_destroylock)
     BT_destroylock.reset(new BugType(this, "Destroy invalid lock",
                                      "Lock checker"));
   ExplodedNode *N = C.generateErrorNode();
   if (!N)
     return;
   auto Report =
       std::make_unique<PathSensitiveBugReport>(*BT_destroylock, Message, N);
   Report->addRange(CE->getArg(0)->getSourceRange());
   C.emitReport(std::move(Report));
 }

 void PthreadLockChecker::InitLock(CheckerContext &C, const CallExpr *CE,
                                   SVal Lock) const {

   const MemRegion *LockR = Lock.getAsRegion();
   if (!LockR)
     return;

   ProgramStateRef State = C.getState();

   const SymbolRef *sym = State->get<DestroyRetVal>(LockR);
   if (sym)
     State = resolvePossiblyDestroyedMutex(State, LockR, sym);

   const struct LockState *LState = State->get<LockMap>(LockR);
   if (!LState || LState->isDestroyed()) {
     State = State->set<LockMap>(LockR, LockState::getUnlocked());
     C.addTransition(State);
     return;
   }

   StringRef Message;

   if (LState->isLocked()) {
     Message = "This lock is still being held";
   } else {
     Message = "This lock has already been initialized";
   }

   if (!BT_initlock)
     BT_initlock.reset(new BugType(this, "Init invalid lock",
                                   "Lock checker"));
   ExplodedNode *N = C.generateErrorNode();
   if (!N)
     return;
   auto Report =
       std::make_unique<PathSensitiveBugReport>(*BT_initlock, Message, N);
   Report->addRange(CE->getArg(0)->getSourceRange());
   C.emitReport(std::move(Report));
 }

 void PthreadLockChecker::reportUseDestroyedBug(CheckerContext &C,
                                                const CallExpr *CE) const {
   if (!BT_destroylock)
     BT_destroylock.reset(new BugType(this, "Use destroyed lock",
                                      "Lock checker"));
   ExplodedNode *N = C.generateErrorNode();
   if (!N)
     return;
   auto Report = std::make_unique<PathSensitiveBugReport>(
       *BT_destroylock, "This lock has already been destroyed", N);
   Report->addRange(CE->getArg(0)->getSourceRange());
   C.emitReport(std::move(Report));
 }

 void PthreadLockChecker::checkDeadSymbols(SymbolReaper &SymReaper,
                                           CheckerContext &C) const {
   ProgramStateRef State = C.getState();

   // TODO: Clean LockMap when a mutex region dies.

   DestroyRetValTy TrackedSymbols = State->get<DestroyRetVal>();
   for (DestroyRetValTy::iterator I = TrackedSymbols.begin(),
                                  E = TrackedSymbols.end();
        I != E; ++I) {
     const SymbolRef Sym = I->second;
     const MemRegion *lockR = I->first;
     bool IsSymDead = SymReaper.isDead(Sym);
     // Remove the dead symbol from the return value symbols map.
     if (IsSymDead)
       State = resolvePossiblyDestroyedMutex(State, lockR, &Sym);
   }
   C.addTransition(State);
 }

 void ento::registerPthreadLockChecker(CheckerManager &mgr) {
   mgr.registerChecker<PthreadLockChecker>();
 }

 bool ento::shouldRegisterPthreadLockChecker(const LangOptions &LO) {
   return true;
 }
	//===--- PthreadLockChecker.cpp - Check for locking problems ---- C++ ---===//
	//
	// 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
	//
	//===----------------------------------------------------------------------===//
	//
	// This defines PthreadLockChecker, a simple lock -> unlock checker.
	// Also handles XNU locks, which behave similarly enough to share code.
	//
	//===----------------------------------------------------------------------===//

	#include "clang/StaticAnalyzer/Checkers/BuiltinCheckerRegistration.h"
	#include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
	#include "clang/StaticAnalyzer/Core/Checker.h"
	#include "clang/StaticAnalyzer/Core/CheckerManager.h"
	#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
	#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"

	using namespace clang;
	using namespace ento;

	namespace {

	struct LockState {
	enum Kind {
	Destroyed,
	Locked,
	Unlocked,
	UntouchedAndPossiblyDestroyed,
	UnlockedAndPossiblyDestroyed
	} K;

	private:
	LockState(Kind K) : K(K) {}

	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::PostStmt<CallExpr>, check::DeadSymbols> {
	mutable std::unique_ptr<BugType> BT_doublelock;
	mutable std::unique_ptr<BugType> BT_doubleunlock;
	mutable std::unique_ptr<BugType> BT_destroylock;
	mutable std::unique_ptr<BugType> BT_initlock;
	mutable std::unique_ptr<BugType> BT_lor;
	enum LockingSemantics {
	NotApplicable = 0,
	PthreadSemantics,
	XNUSemantics
	};
	public:
	void checkPostStmt(const CallExpr *CE, CheckerContext &C) const;
	void checkDeadSymbols(SymbolReaper &SymReaper, CheckerContext &C) const;
	void printState(raw_ostream &Out, ProgramStateRef State,
	const char NL, const char Sep) const override;

	void AcquireLock(CheckerContext &C, const CallExpr *CE, SVal lock,
	bool isTryLock, enum LockingSemantics semantics) const;

	void ReleaseLock(CheckerContext &C, const CallExpr *CE, SVal lock) const;
	void DestroyLock(CheckerContext &C, const CallExpr *CE, SVal Lock,
	enum LockingSemantics semantics) const;
	void InitLock(CheckerContext &C, const CallExpr *CE, SVal Lock) const;
	void reportUseDestroyedBug(CheckerContext &C, const CallExpr *CE) const;
	ProgramStateRef resolvePossiblyDestroyedMutex(ProgramStateRef state,
	const MemRegion *lockR,
	const SymbolRef *sym) const;
	};
	} // 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::checkPostStmt(const CallExpr *CE,
	CheckerContext &C) const {
	StringRef FName = C.getCalleeName(CE);
	if (FName.empty())
	return;

	if (CE->getNumArgs() != 1 && CE->getNumArgs() != 2)
	return;

	if (FName == "pthread_mutex_lock" \|\|
	FName == "pthread_rwlock_rdlock" \|\|
	FName == "pthread_rwlock_wrlock")
	AcquireLock(C, CE, C.getSVal(CE->getArg(0)), false, PthreadSemantics);
	else if (FName == "lck_mtx_lock" \|\|
	FName == "lck_rw_lock_exclusive" \|\|
	FName == "lck_rw_lock_shared")
	AcquireLock(C, CE, C.getSVal(CE->getArg(0)), false, XNUSemantics);
	else if (FName == "pthread_mutex_trylock" \|\|
	FName == "pthread_rwlock_tryrdlock" \|\|
	FName == "pthread_rwlock_trywrlock")
	AcquireLock(C, CE, C.getSVal(CE->getArg(0)),
	true, PthreadSemantics);
	else if (FName == "lck_mtx_try_lock" \|\|
	FName == "lck_rw_try_lock_exclusive" \|\|
	FName == "lck_rw_try_lock_shared")
	AcquireLock(C, CE, C.getSVal(CE->getArg(0)), true, XNUSemantics);
	else if (FName == "pthread_mutex_unlock" \|\|
	FName == "pthread_rwlock_unlock" \|\|
	FName == "lck_mtx_unlock" \|\|
	FName == "lck_rw_done")
	ReleaseLock(C, CE, C.getSVal(CE->getArg(0)));
	else if (FName == "pthread_mutex_destroy")
	DestroyLock(C, CE, C.getSVal(CE->getArg(0)), PthreadSemantics);
	else if (FName == "lck_mtx_destroy")
	DestroyLock(C, CE, C.getSVal(CE->getArg(0)), XNUSemantics);
	else if (FName == "pthread_mutex_init")
	InitLock(C, CE, C.getSVal(CE->getArg(0)));
	}

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

	// TODO: Dump destroyed mutex symbols?
	}

	void PthreadLockChecker::AcquireLock(CheckerContext &C, const CallExpr *CE,
	SVal lock, bool isTryLock,
	enum LockingSemantics semantics) const {

	const MemRegion *lockR = lock.getAsRegion();
	if (!lockR)
	return;

	ProgramStateRef state = C.getState();
	const SymbolRef *sym = state->get<DestroyRetVal>(lockR);
	if (sym)
	state = resolvePossiblyDestroyedMutex(state, lockR, sym);

	SVal X = C.getSVal(CE);
	if (X.isUnknownOrUndef())
	return;

	DefinedSVal retVal = X.castAs<DefinedSVal>();

	if (const LockState *LState = state->get<LockMap>(lockR)) {
	if (LState->isLocked()) {
	if (!BT_doublelock)
	BT_doublelock.reset(new BugType(this, "Double locking",
	"Lock checker"));
	ExplodedNode *N = C.generateErrorNode();
	if (!N)
	return;
	auto report = std::make_unique<PathSensitiveBugReport>(
	*BT_doublelock, "This lock has already been acquired", N);
	report->addRange(CE->getArg(0)->getSourceRange());
	C.emitReport(std::move(report));
	return;
	} else if (LState->isDestroyed()) {
	reportUseDestroyedBug(C, CE);
	return;
	}
	}

	ProgramStateRef lockSucc = state;
	if (isTryLock) {
	// Bifurcate the state, and allow a mode where the lock acquisition fails.
	ProgramStateRef lockFail;
	switch (semantics) {
	case PthreadSemantics:
	std::tie(lockFail, lockSucc) = state->assume(retVal);
	break;
	case XNUSemantics:
	std::tie(lockSucc, lockFail) = state->assume(retVal);
	break;
	default:
	llvm_unreachable("Unknown tryLock locking semantics");
	}
	assert(lockFail && lockSucc);
	C.addTransition(lockFail);

	} else if (semantics == PthreadSemantics) {
	// Assume that the return value was 0.
	lockSucc = state->assume(retVal, false);
	assert(lockSucc);

	} else {
	// XNU locking semantics return void on non-try locks
	assert((semantics == XNUSemantics) && "Unknown locking semantics");
	lockSucc = state;
	}

	// Record that the lock was acquired.
	lockSucc = lockSucc->add<LockSet>(lockR);
	lockSucc = lockSucc->set<LockMap>(lockR, LockState::getLocked());
	C.addTransition(lockSucc);
	}

	void PthreadLockChecker::ReleaseLock(CheckerContext &C, const CallExpr *CE,
	SVal lock) const {

	const MemRegion *lockR = lock.getAsRegion();
	if (!lockR)
	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()) {
	if (!BT_doubleunlock)
	BT_doubleunlock.reset(new BugType(this, "Double unlocking",
	"Lock checker"));
	ExplodedNode *N = C.generateErrorNode();
	if (!N)
	return;
	auto Report = std::make_unique<PathSensitiveBugReport>(
	*BT_doubleunlock, "This lock has already been unlocked", N);
	Report->addRange(CE->getArg(0)->getSourceRange());
	C.emitReport(std::move(Report));
	return;
	} else if (LState->isDestroyed()) {
	reportUseDestroyedBug(C, CE);
	return;
	}
	}

	LockSetTy LS = state->get<LockSet>();

	// FIXME: Better analysis requires IPA for wrappers.

	if (!LS.isEmpty()) {
	const MemRegion *firstLockR = LS.getHead();
	if (firstLockR != lockR) {
	if (!BT_lor)
	BT_lor.reset(new BugType(this, "Lock order reversal", "Lock checker"));
	ExplodedNode *N = C.generateErrorNode();
	if (!N)
	return;
	auto report = std::make_unique<PathSensitiveBugReport>(
	*BT_lor, "This was not the most recently acquired lock. Possible "
	"lock order reversal", N);
	report->addRange(CE->getArg(0)->getSourceRange());
	C.emitReport(std::move(report));
	return;
	}
	// Record that the lock was released.
	state = state->set<LockSet>(LS.getTail());
	}

	state = state->set<LockMap>(lockR, LockState::getUnlocked());
	C.addTransition(state);
	}

	void PthreadLockChecker::DestroyLock(CheckerContext &C, const CallExpr *CE,
	SVal Lock,
	enum LockingSemantics semantics) const {

	const MemRegion *LockR = Lock.getAsRegion();
	if (!LockR)
	return;

	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 = C.getSVal(CE).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;
	}
	}
	StringRef Message;

	if (LState->isLocked()) {
	Message = "This lock is still locked";
	} else {
	Message = "This lock has already been destroyed";
	}

	if (!BT_destroylock)
	BT_destroylock.reset(new BugType(this, "Destroy invalid lock",
	"Lock checker"));
	ExplodedNode *N = C.generateErrorNode();
	if (!N)
	return;
	auto Report =
	std::make_unique<PathSensitiveBugReport>(*BT_destroylock, Message, N);
	Report->addRange(CE->getArg(0)->getSourceRange());
	C.emitReport(std::move(Report));
	}

	void PthreadLockChecker::InitLock(CheckerContext &C, const CallExpr *CE,
	SVal Lock) const {

	const MemRegion *LockR = Lock.getAsRegion();
	if (!LockR)
	return;

	ProgramStateRef State = C.getState();

	const SymbolRef *sym = State->get<DestroyRetVal>(LockR);
	if (sym)
	State = resolvePossiblyDestroyedMutex(State, LockR, sym);

	const struct LockState *LState = State->get<LockMap>(LockR);
	if (!LState \|\| LState->isDestroyed()) {
	State = State->set<LockMap>(LockR, LockState::getUnlocked());
	C.addTransition(State);
	return;
	}

	StringRef Message;

	if (LState->isLocked()) {
	Message = "This lock is still being held";
	} else {
	Message = "This lock has already been initialized";
	}

	if (!BT_initlock)
	BT_initlock.reset(new BugType(this, "Init invalid lock",
	"Lock checker"));
	ExplodedNode *N = C.generateErrorNode();
	if (!N)
	return;
	auto Report =
	std::make_unique<PathSensitiveBugReport>(*BT_initlock, Message, N);
	Report->addRange(CE->getArg(0)->getSourceRange());
	C.emitReport(std::move(Report));
	}

	void PthreadLockChecker::reportUseDestroyedBug(CheckerContext &C,
	const CallExpr *CE) const {
	if (!BT_destroylock)
	BT_destroylock.reset(new BugType(this, "Use destroyed lock",
	"Lock checker"));
	ExplodedNode *N = C.generateErrorNode();
	if (!N)
	return;
	auto Report = std::make_unique<PathSensitiveBugReport>(
	*BT_destroylock, "This lock has already been destroyed", N);
	Report->addRange(CE->getArg(0)->getSourceRange());
	C.emitReport(std::move(Report));
	}

	void PthreadLockChecker::checkDeadSymbols(SymbolReaper &SymReaper,
	CheckerContext &C) const {
	ProgramStateRef State = C.getState();

	// TODO: Clean LockMap when a mutex region dies.

	DestroyRetValTy TrackedSymbols = State->get<DestroyRetVal>();
	for (DestroyRetValTy::iterator I = TrackedSymbols.begin(),
	E = TrackedSymbols.end();
	I != E; ++I) {
	const SymbolRef Sym = I->second;
	const MemRegion *lockR = I->first;
	bool IsSymDead = SymReaper.isDead(Sym);
	// Remove the dead symbol from the return value symbols map.
	if (IsSymDead)
	State = resolvePossiblyDestroyedMutex(State, lockR, &Sym);
	}
	C.addTransition(State);
	}

	void ento::registerPthreadLockChecker(CheckerManager &mgr) {
	mgr.registerChecker<PthreadLockChecker>();
	}

	bool ento::shouldRegisterPthreadLockChecker(const LangOptions &LO) {
	return true;
	}