Modifying PthreadLockChecker.cpp to reduce false positives.

[malhar1995]

Summary

I am currently working on to avoid false positives which currently occur as the return values of mutex functions like pthread_mutex_destroy() are not taken into consideration.

The precise description of the bug can be found here: https://bugs.llvm.org/show_bug.cgi?id=32455

Dr. Devin and Dr. Artem have been guiding me to fix PthreadLockChecker to avoid such false positives. The patch I'm attaching is not 100% correct and hence I need your advice to proceed further.

Thank you.

[NoQ]

Uhm, i need to do something about this duplicate account. Sorry, I have completely forgotten that the review is already up...

[NoQ]

Thanks for uploading this to phabricator and sorry again that i was lost for a while.

As we already discussed in the mailing lists, i agree with your point that the locked-and-possibly-destroyed state should be removed, and we also had a thought of making it explicit that the patch only applies to posix thread semantics, not to XNU semantics - in other words, there should appear different branches of code depending on the lock's semantics.

Could you also upload the patch file with the "context" (eg. git diff -U999999 would include +/- 999999 unchanged lines around the changes in the patch file, and phabricator would use them fancily to make reviewing easier; otherwise i don't immediately see which callback you are changing in a particular spot).

Once the patch would reach completion, it'd need to be cleaned up for formatting/whitespace; we usually run clang-format over our changes with default settings and it does everything for us.

lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp

21

You don't need to include <iostream even for your own debugging, because we have this other facility:

llvm::errs() << "prpr " << RetVal << '\n';

(yeah, you can put SVal and some other objects into llvm::errs() directly (which would be equivalent to .dump()ing them), which is also handy).

145–151

This code gets duplicated multiple times - including the checkDeadSymbols callback as well; can we refactor it into a function?

154

I'd like you to consider various corner cases. Note that because we have the REGISTER_MAP_WITH_PROGRAMSTATE privately in this file, only code in this file can affect the contents of that program state trait. So we have complete knowledge of what can and cannot be in the program state.

For example, can it be that there's a symbol in the DestroyRetVal map, but lstate is not present for the same mutex region in the LockMap? Or does the code ensure that the former implies the latter? If we are sure that some invariants hold, then we should remove the respective if () and ideally replace it with an assert().

If you find invariants that always hold, it would be great to write these down in the comments inside the code.

[zaks.anna]

Thank you for the patch! Could you please re-submit the patch with context? Instructions on how to do that can be found here:
http://llvm.org/docs/Phabricator.html

[malhar1995]

Added context.
Also, I removed the inclusion of iostream and also added the repetitive code to the function setAppropriateLockState.
Currently working on finding various corner cases and invariants.

[malhar1995]

Cleaned up the previous patch.
Added checking of LockState before initializing a mutex as well.
Added separate branches of execution for PthreadSemantics and XNUSemantics.
Added assert in case of checkDeadSymbols as existence in DestroyRetVal ensures existence in LockMap.

[NoQ]

Thanks! Your code looks very clear now, and it seems correct to me.

One last thing we definitely should do here would be add regression tests for the new functionality. I guess you already have your tests, otherwise you wouldn't know if your code works, so you'd just need to append them to the patch, somewhere at the bottom of test/Analysis/pthreadlock.c, and make sure that make -j4 check-clang-analysis passes. Ideally, we should cover as many branches as possible.

A few ideas of what to test (you might have thought about most of them already, and i expect them to actually work by just looking at what your code accomplishes):

• What we can/cannot do with the mutex in the failed-to-be-destroyed state, depending on the state of the mutex before destruction was attempted.
• What we can/cannot do with the mutex in each of the "Schrodinger" states - in particular, do we display the double-destroy warning in such cases?
• How return-symbol death races against resolving success of the destroy operation: what if the programmer first tries to destroy mutex, then uses the mutex, then checks the return value?
• Are you sure we cannot assert(lstate) on line 137? - a test could be added that would cause such assertion to fail if someone tries to impose it.

Apart from that, i guess it'd be good to use more informative variable names in a few places (see inline comments), and fix the formatting, i.e. spaces and line breaks (should be easy with clang-format). Also you shouldn't add the .DS_Store files :) And then we'd accept and commit this patch.

lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp

28–34

I still think these names, no matter if a good metaphor or not and no matter how much i enjoyed them, should be toned down :) Suggesting UntouchedAndPossiblyDestroyed and UnlockedAndPossiblyDestroyed.

86

I suggest renaming to something like "resolvePossiblyDestroyedMutex()".

Also, i'm for passing the symbol by value (with * dereference at most call sites) because it's less surprising/confusing to the reader.

I also suggest a comment explaining what the function does. Eg., "When a lock is destroyed, in some semantics 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."

92–100

Because there's only one comment per three traits, it'd be great to clean this up a bit together with commenting up your new trait:

// 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 destroy calls.
REGISTER_MAP_WITH_PROGRAMSTATE(DestroyRetVal, const MemRegion *, SymbolRef)

153–156

I think we can be certain that the lock is in one of these states, and assert that.

159–161

Assert the lock state here as well?

324–330

A bit shorter and more stylish:

SymbolRef RetSym = C.getSVal(CE).getAsSymbol();
if (!RetSym)
  return;

Also, we may want to see what happens when the value is not a symbol. This would be surprising, but it may happen if the body of pthread_mutex_destroy() is suddenly available in our translation unit and we modeled the call, or another checker has assisted with modeling it. In this case the return value may be a concrete integer (say 0 or 1) or an UnknownVal or an UndefinedVal. It may also be something completely weird such as a pointer or a structure if the user defines his own function that is called "pthread_mutex_destroy()" but does something completely different.

I suggest to stop tracking the lock region in case RetSym is null (remove LockR from the LockMap), because in the really weird case when this code actually gets triggered, we'd at least not say that the mutex is still locked later on the path.

Additionally, by adding the transition before that return, we ensure that setAppropriateLockState above has taken effect.

421

Could you add here a

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

That's not something you should instantly do, but it's definitely something that needs to be done for this checker some day.

[malhar1995]

In D32449#760141, @NoQ wrote:

Thanks! Your code looks very clear now, and it seems correct to me.

One last thing we definitely should do here would be add regression tests for the new functionality. I guess you already have your tests, otherwise you wouldn't know if your code works, so you'd just need to append them to the patch, somewhere at the bottom of test/Analysis/pthreadlock.c, and make sure that make -j4 check-clang-analysis passes. Ideally, we should cover as many branches as possible.

A few ideas of what to test (you might have thought about most of them already, and i expect them to actually work by just looking at what your code accomplishes):

• What we can/cannot do with the mutex in the failed-to-be-destroyed state, depending on the state of the mutex before destruction was attempted.
• What we can/cannot do with the mutex in each of the "Schrodinger" states - in particular, do we display the double-destroy warning in such cases?
• How return-symbol death races against resolving success of the destroy operation: what if the programmer first tries to destroy mutex, then uses the mutex, then checks the return value?
• Are you sure we cannot assert(lstate) on line 137? - a test could be added that would cause such assertion to fail if someone tries to impose it.

Apart from that, i guess it'd be good to use more informative variable names in a few places (see inline comments), and fix the formatting, i.e. spaces and line breaks (should be easy with clang-format). Also you shouldn't add the .DS_Store files :) And then we'd accept and commit this patch.

Dear Dr. Artem,

Thank you so much for such a detailed review. I'll work on addressing these comments ASAP and reach out to you in case I have any queries.

Regards,
Malhar Thakkar

[malhar1995]

lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp

153–156

We can be certain that the lock state will be either of the two only if I add the following statement before returning from this function.

state = state->remove<DestroyRetVal>(lockR);

If I don't add the above statement, a return value symbol for the region specified by lockR will still be in DestroyRetVal and it may have an actual lock state (locked, unlocked or destroyed).

[malhar1995]

Addressed previous comments (removed Schrodinger from lock state names, changed method name setAppropriateLockState to resolvePossiblyDestroyedMutex, added an assert in resolvePossiblyDestroyedMutex, formatted the code using clang-format and added some test-cases to test/Analysis/pthreadlock.c)

[NoQ]

Thanks, this is great! Two more things:

• You have touched other code, unrelated to your patch, with clang-format; we're usually trying to avoid that, because it creates merge conflicts out of nowhere, and because some of that code actually seems formatted by hand intentionally. It's better to revert these changes; you can use the git clang-format thing to format only actual changes.

• Updating .gitignore sounds like the right thing to do (llvm's .gitignore already has this), but i guess we'd better make a separate commit for that.

lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp

153–156

Yep, that's a great thing to do. I didn't notice this.

Generally, it's great to keep the program state free from stuff that would no longer be necessary.

[malhar1995]

In D32449#761303, @NoQ wrote:

Thanks, this is great! Two more things:

• You have touched other code, unrelated to your patch, with clang-format; we're usually trying to avoid that, because it creates merge conflicts out of nowhere, and because some of that code actually seems formatted by hand intentionally. It's better to revert these changes; you can use the git clang-format thing to format only actual changes.

I did not apply clang-format to any file except for PthreadLockChecker.cpp. Do you think the merge conflict is due to me not applying clang-format to test/Analysis/pthreadlock.c? The only files I changed were .gitignore, PthreadLockChecker.cpp and test/Analysis/pthreadlock.c.
Also, when you asked me to revert the changes, did you mean revert the changes made by clang-format? If yes, how do I do that?
I apologize for asking such silly questions. The thing is I'm new to all this and I don't really know how to proceed further.

• Updating .gitignore sounds like the right thing to do (llvm's .gitignore already has this), but i guess we'd better make a separate commit for that.

[NoQ]

No-no, all i was trying to say is that there's code in PthreadLockChecker.cpp that you haven't changed, but accidentally reformatted - and this is something we normally try to avoid. Like, for example, changing enum LockingSemantics {...} from vertical to horizontal - that wasn't your intention, it just accidentally happened because you auto-reformatted the whole file. I don't mind these changes, and i didn't mean they introduce any merge conflicts for now, though they tend to do so in the future for other people working on the same code, as we have a few downstream users, and magenta guys who are working on this checker as part of D26342), so most of the time it's better not to introduce unnecessary changes.

I'm not sure if you can easily revert the style-only changes via git clang-format, but you should be able to find them with the help of git reflog if you made a local commit before running clang-format (even if it was later discarded or amended), otherwise only manually i guess.

[malhar1995]

Applied clang-format only to the changed lines in the final code.

[NoQ]

I'd commit your patch without the .gitignore change, as it deserves a separate commit and more attention; will have a look at it myself - llvm's and clang's .gitignores have diverged quite a bit.

Thanks for taking this up!~

.gitignore

 #==============================================================================#
 # This file specifies intentionally untracked files that git should ignore.
 # See: http://www.kernel.org/pub/software/scm/git/docs/gitignore.html
 #
 # This file is intentionally different from the output of `git svn show-ignore`,
 # as most of those are useless.
 #==============================================================================#
+.DS_Store
 
 #==============================================================================#
 # File extensions to be ignored anywhere in the tree.
 #==============================================================================#
 # Temp files created by most text editors.
 *~
 # Merge files created by git.
 *.orig

lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp

 //===----------------------------------------------------------------------===//
 
 #include "ClangSACheckers.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 } K;
+  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); }
-
-  bool operator==(const LockState &X) const {
-    return K == X.K;
+  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; }
-
-  void Profile(llvm::FoldingSetNodeID &ID) const {
-    ID.AddInteger(K);
+  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> > {
+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
-  };
+  enum LockingSemantics { NotApplicable = 0, PthreadSemantics, XNUSemantics };
+
 public:
   void checkPostStmt(const CallExpr *CE, CheckerContext &C) const;
+  void checkDeadSymbols(SymbolReaper &SymReaper, CheckerContext &C) const;
 
   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) 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
 
-// GDM Entry for tracking lock state.
+// 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 {
   ProgramStateRef state = C.getState();
   const LocationContext *LCtx = C.getLocationContext();
   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" ||
+  if (FName == "pthread_mutex_lock" || FName == "pthread_rwlock_rdlock" ||
       FName == "pthread_rwlock_wrlock")
-    AcquireLock(C, CE, state->getSVal(CE->getArg(0), LCtx),
-                false, PthreadSemantics);
-  else if (FName == "lck_mtx_lock" ||
-           FName == "lck_rw_lock_exclusive" ||
+    AcquireLock(C, CE, state->getSVal(CE->getArg(0), LCtx), false,
+                PthreadSemantics);
+  else if (FName == "lck_mtx_lock" || FName == "lck_rw_lock_exclusive" ||
            FName == "lck_rw_lock_shared")
-    AcquireLock(C, CE, state->getSVal(CE->getArg(0), LCtx),
-                false, XNUSemantics);
+    AcquireLock(C, CE, state->getSVal(CE->getArg(0), LCtx), false,
+                XNUSemantics);
   else if (FName == "pthread_mutex_trylock" ||
            FName == "pthread_rwlock_tryrdlock" ||
            FName == "pthread_rwlock_trywrlock")
-    AcquireLock(C, CE, state->getSVal(CE->getArg(0), LCtx),
-                true, PthreadSemantics);
+    AcquireLock(C, CE, state->getSVal(CE->getArg(0), LCtx), true,
+                PthreadSemantics);
   else if (FName == "lck_mtx_try_lock" ||
            FName == "lck_rw_try_lock_exclusive" ||
            FName == "lck_rw_try_lock_shared")
-    AcquireLock(C, CE, state->getSVal(CE->getArg(0), LCtx),
-                true, XNUSemantics);
+    AcquireLock(C, CE, state->getSVal(CE->getArg(0), LCtx), true, XNUSemantics);
   else if (FName == "pthread_mutex_unlock" ||
-           FName == "pthread_rwlock_unlock" ||
-           FName == "lck_mtx_unlock" ||
+           FName == "pthread_rwlock_unlock" || FName == "lck_mtx_unlock" ||
            FName == "lck_rw_done")
     ReleaseLock(C, CE, state->getSVal(CE->getArg(0), LCtx));
-  else if (FName == "pthread_mutex_destroy" ||
-           FName == "lck_mtx_destroy")
-    DestroyLock(C, CE, state->getSVal(CE->getArg(0), LCtx));
+  else if (FName == "pthread_mutex_destroy")
+    DestroyLock(C, CE, state->getSVal(CE->getArg(0), LCtx), PthreadSemantics);
+  else if (FName == "lck_mtx_destroy")
+    DestroyLock(C, CE, state->getSVal(CE->getArg(0), LCtx), XNUSemantics);
   else if (FName == "pthread_mutex_init")
     InitLock(C, CE, state->getSVal(CE->getArg(0), LCtx));
 }
 
+// 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::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 = state->getSVal(CE, C.getLocationContext());
   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"));
+        BT_doublelock.reset(
+            new BugType(this, "Double locking", "Lock checker"));
       ExplodedNode *N = C.generateErrorNode();
       if (!N)
         return;
       auto report = llvm::make_unique<BugReport>(
           *BT_doublelock, "This lock has already been acquired", N);
       report->addRange(CE->getArg(0)->getSourceRange());
       C.emitReport(std::move(report));
       return;
void PthreadLockChecker::AcquireLock(CheckerContext &C, const CallExpr *CE,
   // 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"));
+        BT_doubleunlock.reset(
+            new BugType(this, "Double unlocking", "Lock checker"));
       ExplodedNode *N = C.generateErrorNode();
       if (!N)
         return;
       auto Report = llvm::make_unique<BugReport>(
           *BT_doubleunlock, "This lock has already been unlocked", N);
       Report->addRange(CE->getArg(0)->getSourceRange());
       C.emitReport(std::move(Report));
       return;
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 = llvm::make_unique<BugReport>(
-          *BT_lor, "This was not the most recently acquired lock. Possible "
-                   "lock order reversal", N);
+          *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) const {
-
+                                     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"));
+    BT_destroylock.reset(
+        new BugType(this, "Destroy invalid lock", "Lock checker"));
   ExplodedNode *N = C.generateErrorNode();
   if (!N)
     return;
   auto Report = llvm::make_unique<BugReport>(*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"));
+    BT_initlock.reset(new BugType(this, "Init invalid lock", "Lock checker"));
   ExplodedNode *N = C.generateErrorNode();
   if (!N)
     return;
   auto Report = llvm::make_unique<BugReport>(*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"));
+    BT_destroylock.reset(
+        new BugType(this, "Use destroyed lock", "Lock checker"));
   ExplodedNode *N = C.generateErrorNode();
   if (!N)
     return;
   auto Report = llvm::make_unique<BugReport>(
       *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);
+
+    if (IsSymDead)
+      State = resolvePossiblyDestroyedMutex(State, lockR, &Sym);
+  }
+  C.addTransition(State);
+}
+
 void ento::registerPthreadLockChecker(CheckerManager &mgr) {
   mgr.registerChecker<PthreadLockChecker>();
 }

test/Analysis/pthreadlock.c

 void
 ok22(void) {
   pthread_mutex_lock(pmtx);    // no-warning
   pthread_mutex_unlock(pmtx);  // no-warning
   pthread_mutex_lock(pmtx);    // no-warning
   pthread_mutex_unlock(pmtx);  // no-warning
 }
 
+void
+ok23(void) {
+  if(pthread_mutex_destroy(&mtx1) != 0)  // no-warning
+    pthread_mutex_destroy(&mtx1); // no-warning
+}
+
+void
+ok24(void) {
+  if(pthread_mutex_destroy(&mtx1) != 0)  // no-warning
+    pthread_mutex_lock(&mtx1);  // no-warning
+}
+
+void
+ok25(void) {
+  if(pthread_mutex_destroy(&mtx1) != 0)  // no-warning
+    pthread_mutex_unlock(&mtx1);  // no-warning
+}
+
+void
+ok26(void) {
+  pthread_mutex_unlock(&mtx1);  // no-warning
+  if(pthread_mutex_destroy(&mtx1) != 0)  // no-warning
+    pthread_mutex_lock(&mtx1);  // no-warning
+}
+
+void
+ok27(void) {
+  pthread_mutex_unlock(&mtx1);  // no-warning
+  if(pthread_mutex_destroy(&mtx1) != 0)  // no-warning
+    pthread_mutex_lock(&mtx1);  // no-warning
+  else
+    pthread_mutex_init(&mtx1, NULL);  // no-warning
+}
+
+void
+ok28() {
+  if(pthread_mutex_destroy(&mtx1)!=0) {  // no-warning
+    pthread_mutex_lock(&mtx1);  // no-warning
+    pthread_mutex_unlock(&mtx1);  // no-warning
+    pthread_mutex_destroy(&mtx1); // no-warning
+  }
+}
+
 
 void
 bad1(void)
 {
   pthread_mutex_lock(&mtx1);  // no-warning
   pthread_mutex_lock(&mtx1);  // expected-warning{{This lock has already been acquired}}
 }
 

 }
 
 void
 bad26(void)
 {
   pthread_mutex_unlock(&mtx1);    // no-warning
   pthread_mutex_init(&mtx1, NULL);  // expected-warning{{This lock has already been initialized}}
 }
+
+void
+bad27(void)
+{
+  pthread_mutex_unlock(&mtx1);  // no-warning
+  int ret = pthread_mutex_destroy(&mtx1);  // no-warning
+  if(ret != 0)  // no-warning
+    pthread_mutex_lock(&mtx1);  // no-warning
+  else
+    pthread_mutex_unlock(&mtx1);  // expected-warning{{This lock has already been destroyed}}
+}
+
+void
+bad28(void)
+{
+  pthread_mutex_unlock(&mtx1);  // no-warning
+  int ret = pthread_mutex_destroy(&mtx1);  // no-warning
+  if(ret != 0)  // no-warning
+    pthread_mutex_lock(&mtx1);  // no-warning
+  else
+    pthread_mutex_lock(&mtx1);  // expected-warning{{This lock has already been destroyed}}
+}
+
+void
+bad29()
+{
+  pthread_mutex_lock(&mtx1);  // no-warning
+  pthread_mutex_unlock(&mtx1);  // no-warning
+  if(pthread_mutex_destroy(&mtx1) != 0)  // no-warning
+    pthread_mutex_init(&mtx1, NULL);  // expected-warning{{This lock has already been initialized}}
+  else
+    pthread_mutex_init(&mtx1, NULL);  // no-warning
+}
+
+void
+bad30()
+{
+  pthread_mutex_lock(&mtx1);  // no-warning
+  pthread_mutex_unlock(&mtx1);  // no-warning
+  if(pthread_mutex_destroy(&mtx1) != 0)  // no-warning
+    pthread_mutex_init(&mtx1, NULL);  // expected-warning{{This lock has already been initialized}}
+  else
+    pthread_mutex_destroy(&mtx1); // expected-warning{{This lock has already been destroyed}}
+}
+
+void 
+bad31()
+{
+  int ret = pthread_mutex_destroy(&mtx1);  // no-warning
+  pthread_mutex_lock(&mtx1);  // expected-warning{{This lock has already been destroyed}}
+  if(ret != 0)
+    pthread_mutex_lock(&mtx1);
+}