Index: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
===================================================================
--- lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
+++ lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
@@ -25,7 +25,7 @@
 namespace {
 
 struct LockState {
-  enum Kind { Destroyed, Locked, Unlocked } K;
+  enum Kind { Destroyed, Locked, Unlocked, SchrodingerUntouched, SchrodingerUnlocked } K;
 
 private:
   LockState(Kind K) : K(K) {}
@@ -34,6 +34,8 @@
   static LockState getLocked() { return LockState(Locked); }
   static LockState getUnlocked() { return LockState(Unlocked); }
   static LockState getDestroyed() { return LockState(Destroyed); }
+  static LockState getSchrodingerUntouched() { return LockState(SchrodingerUntouched); }
+  static LockState getSchrodingerUnlocked() { return LockState(SchrodingerUnlocked); }
 
   bool operator==(const LockState &X) const {
     return K == X.K;
@@ -42,13 +44,15 @@
   bool isLocked() const { return K == Locked; }
   bool isUnlocked() const { return K == Unlocked; }
   bool isDestroyed() const { return K == Destroyed; }
+  bool isSchrodingerUntouched() const { return K == SchrodingerUntouched; }
+  bool isSchrodingerUnlocked() const { return K == SchrodingerUnlocked; }
 
   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;
@@ -61,14 +65,16 @@
   };
 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 setAppropriateLockState(ProgramStateRef state, const MemRegion* lockR, const SymbolRef* sym, bool fromCheckDeadSymbols) const;
 };
 } // end anonymous namespace
 
@@ -76,6 +82,7 @@
 REGISTER_LIST_WITH_PROGRAMSTATE(LockSet, const MemRegion *)
 
 REGISTER_MAP_WITH_PROGRAMSTATE(LockMap, const MemRegion *, LockState)
+REGISTER_MAP_WITH_PROGRAMSTATE(DestroyRetVal, const MemRegion *, SymbolRef)
 
 void PthreadLockChecker::checkPostStmt(const CallExpr *CE,
                                        CheckerContext &C) const {
@@ -113,22 +120,50 @@
            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));
 }
 
+ProgramStateRef PthreadLockChecker::setAppropriateLockState(ProgramStateRef state, const MemRegion* lockR, const SymbolRef* sym, bool fromCheckDeadSymbols) const {
+  const LockState* lstate = state->get<LockMap>(lockR);
+  // Existence in DestroyRetVal ensures existence in LockMap.
+  if(fromCheckDeadSymbols)
+    assert(lstate);
+  else{
+    if(!lstate)
+      return state;
+  }
+  ConstraintManager &CMgr = state->getConstraintManager();
+  ConditionTruthVal retZero = CMgr.isNull(state, *sym);
+  if(retZero.isConstrainedFalse()){
+    if(lstate->isSchrodingerUntouched())
+      state = state->remove<LockMap>(lockR);
+    else if(lstate->isSchrodingerUnlocked())
+      state = state->set<LockMap>(lockR, LockState::getUnlocked());
+  }
+  else{
+    if(lstate->isSchrodingerUntouched() || lstate->isSchrodingerUnlocked()){
+      state = state->set<LockMap>(lockR, LockState::getDestroyed());
+    }
+  }
+  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;
+    return; 
 
   ProgramStateRef state = C.getState();
+  const SymbolRef* sym = state->get<DestroyRetVal>(lockR);
+  if(sym)
+    state = setAppropriateLockState(state, lockR, sym, false);
 
   SVal X = state->getSVal(CE, C.getLocationContext());
   if (X.isUnknownOrUndef())
@@ -197,6 +232,9 @@
     return;
 
   ProgramStateRef state = C.getState();
+  const SymbolRef* sym = state->get<DestroyRetVal>(lockR);
+  if(sym)
+    state = setAppropriateLockState(state, lockR, sym, false);
 
   if (const LockState *LState = state->get<LockMap>(lockR)) {
     if (LState->isUnlocked()) {
@@ -245,7 +283,7 @@
 }
 
 void PthreadLockChecker::DestroyLock(CheckerContext &C, const CallExpr *CE,
-                                     SVal Lock) const {
+                                     SVal Lock, enum LockingSemantics semantics) const {
 
   const MemRegion *LockR = Lock.getAsRegion();
   if (!LockR)
@@ -253,13 +291,37 @@
 
   ProgramStateRef State = C.getState();
 
+  const SymbolRef* sym = State->get<DestroyRetVal>(LockR);
+  if(sym)
+    State = setAppropriateLockState(State, LockR, sym, false);
+
   const LockState *LState = State->get<LockMap>(LockR);
-  if (!LState || LState->isUnlocked()) {
-    State = State->set<LockMap>(LockR, LockState::getDestroyed());
-    C.addTransition(State);
-    return;
+  // Checking the return value of the destroy method only in the case of PthreadSemantics
+  if(semantics==PthreadSemantics){
+    if(!LState || LState->isUnlocked()){
+      SVal X = State->getSVal(CE, C.getLocationContext());
+      if (X.isUnknownOrUndef()){
+        return;
+      }
+
+      DefinedSVal retVal = X.castAs<DefinedSVal>();
+      SymbolRef sym = retVal.getAsSymbol();
+      State = State->set<DestroyRetVal>(LockR, sym);
+      if(LState && LState->isUnlocked())
+        State = State->set<LockMap>(LockR, LockState::getSchrodingerUnlocked());
+      else
+        State = State->set<LockMap>(LockR, LockState::getSchrodingerUntouched());
+      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()) {
@@ -288,6 +350,10 @@
 
   ProgramStateRef State = C.getState();
 
+  const SymbolRef* sym = State->get<DestroyRetVal>(LockR);
+  if(sym)
+    State = setAppropriateLockState(State, LockR, sym, false);
+
   const struct LockState *LState = State->get<LockMap>(LockR);
   if (!LState || LState->isDestroyed()) {
     State = State->set<LockMap>(LockR, LockState::getUnlocked());
@@ -327,6 +393,24 @@
   Report->addRange(CE->getArg(0)->getSourceRange());
   C.emitReport(std::move(Report));
 }
+void PthreadLockChecker::checkDeadSymbols(SymbolReaper &SymReaper,
+                                           CheckerContext &C) const {
+  ProgramStateRef State = C.getState();
+
+  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 = setAppropriateLockState(State, lockR, &Sym, true); 
+      State = State->remove<DestroyRetVal>(lockR);
+    }
+  }
+  C.addTransition(State);
+}
 
 void ento::registerPthreadLockChecker(CheckerManager &mgr) {
   mgr.registerChecker<PthreadLockChecker>();