malhar1995 updated this revision to Diff 99179.
malhar1995 added a comment.
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.
Repository:
rL LLVM
https://reviews.llvm.org/D32449
Files:
.DS_Store
lib/.DS_Store
lib/StaticAnalyzer/.DS_Store
lib/StaticAnalyzer/Checkers/.DS_Store
lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
Index: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
===================================================================
--- lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
+++ lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
@@ -25,30 +25,34 @@
namespace {
struct LockState {
- enum Kind { Destroyed, Locked, Unlocked } K;
+ enum Kind { Destroyed, Locked, Unlocked, SchrodingerLocked, SchrodingerUnlocked } 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 getSchrodingerLocked() { return LockState(SchrodingerLocked); }
+ static LockState getSchrodingerUnlocked() { return LockState(SchrodingerUnlocked); }
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 isSchrodingerLocked() const { return K == SchrodingerLocked; }
+ 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,21 +65,24 @@
};
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 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;
};
} // end anonymous namespace
// GDM Entry for tracking lock state.
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 {
@@ -120,16 +127,40 @@
InitLock(C, CE, state->getSVal(CE->getArg(0), LCtx));
}
+ProgramStateRef PthreadLockChecker::setAppropriateLockState(ProgramStateRef state, const MemRegion* lockR) const {
+ const SymbolRef* sym = state->get<DestroyRetVal>(lockR);
+ if(sym){
+ const LockState* lstate = state->get<LockMap>(lockR);
+ if(lstate){
+ ConstraintManager &CMgr = state->getConstraintManager();
+ ConditionTruthVal retZero = CMgr.isNull(state, *sym);
+ if(retZero.isConstrainedFalse()){
+ if(lstate->isSchrodingerLocked())
+ state = state->set<LockMap>(lockR, LockState::getLocked());
+ else if(lstate->isSchrodingerUnlocked())
+ state = state->set<LockMap>(lockR, LockState::getUnlocked());
+ }
+ else{
+ if(!lstate || lstate->isSchrodingerLocked() || 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();
+ state = setAppropriateLockState(state, lockR);
+
SVal X = state->getSVal(CE, C.getLocationContext());
if (X.isUnknownOrUndef())
return;
@@ -198,6 +229,8 @@
ProgramStateRef state = C.getState();
+ state = setAppropriateLockState(state, lockR);
+
if (const LockState *LState = state->get<LockMap>(lockR)) {
if (LState->isUnlocked()) {
if (!BT_doubleunlock)
@@ -253,9 +286,32 @@
ProgramStateRef State = C.getState();
+ State = setAppropriateLockState(State, LockR);
+
+ // CHECK THIS
const LockState *LState = State->get<LockMap>(LockR);
- if (!LState || LState->isUnlocked()) {
- State = State->set<LockMap>(LockR, LockState::getDestroyed());
+ if(!LState){
+ SVal X = State->getSVal(CE, C.getLocationContext());
+ if (X.isUnknownOrUndef()){
+ return;
+ }
+
+ DefinedSVal retVal = X.castAs<DefinedSVal>();
+ retVal.dump();
+ SymbolRef sym = retVal.getAsSymbol();
+ State = State->set<DestroyRetVal>(LockR, sym);
+ C.addTransition(State);
+ return;
+ }
+ if (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);
+ State = State->set<LockMap>(LockR, LockState::getSchrodingerUnlocked());
C.addTransition(State);
return;
}
@@ -327,6 +383,37 @@
Report->addRange(CE->getArg(0)->getSourceRange());
C.emitReport(std::move(Report));
}
+void PthreadLockChecker::checkDeadSymbols(SymbolReaper &SymReaper,
+ CheckerContext &C) const {
+ ProgramStateRef State = C.getState();
+ ConstraintManager &CMgr = State->getConstraintManager();
+
+ DestroyRetValTy TrackedSymbols = State->get<DestroyRetVal>();
+ for (DestroyRetValTy::iterator I = TrackedSymbols.begin(),
+ E = TrackedSymbols.end(); I != E; ++I) {
+ SymbolRef Sym = I->second;
+ const MemRegion* lockR = I->first;
+ bool IsSymDead = SymReaper.isDead(Sym);
+ const LockState* LState = State->get<LockMap>(lockR);
+ // Remove the dead symbol from the return value symbols map.
+ if (IsSymDead){
+ ConditionTruthVal retZero = CMgr.isNull(State, Sym);
+ if(retZero.isConstrainedFalse()){
+ if(LState && LState->isSchrodingerLocked())
+ State = State->set<LockMap>(lockR, LockState::getLocked());
+ else if(LState && LState->isSchrodingerUnlocked())
+ State = State->set<LockMap>(lockR, LockState::getUnlocked());
+ }
+ else{
+ // IS THIS CORRECT?
+ if(!LState || LState->isSchrodingerUnlocked() || LState->isSchrodingerLocked())
+ State = State->set<LockMap>(lockR, LockState::getDestroyed());
+ }
+ State = State->remove<DestroyRetVal>(lockR);
+ }
+ }
+ C.addTransition(State);
+}
void ento::registerPthreadLockChecker(CheckerManager &mgr) {
mgr.registerChecker<PthreadLockChecker>();
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
