<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><br class=""><div><blockquote type="cite" class=""><div class="">On Apr 15, 2017, at 3:52 AM, Malhar Thakkar <<a href="mailto:cs13b1031@iith.ac.in" class="">cs13b1031@iith.ac.in</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class=""><div class=""><font face="arial, helvetica, sans-serif" class="">Dear Dr. Devin,</font></div><div class=""><font face="arial, helvetica, sans-serif" class=""><br class=""></font></div><div class=""><font face="arial, helvetica, sans-serif" class="">I am storing the return value of pthread_mutex_destroy() (as a SymbolRef) and mapping it to the corresponding mutex's MemRegion. While trying to access this SymbolRef and checking for constraints on this SymbolRef, I am unable to produce the desired output. </font></div><div class=""><font face="arial, helvetica, sans-serif" class=""><br class=""></font></div><div class=""><font face="arial, helvetica, sans-serif" class="">The changes made are mentioned below.</font></div><div class=""><font face="arial, helvetica, sans-serif" class=""><br class=""></font></div><div style="font-family:monospace,monospace" class=""><br class=""></div><div style="font-family:monospace,monospace" class="">REGISTER_MAP_WITH_PROGRAMSTATE(RetValConstraint, const MemRegion *, SymbolRef) // Map to store SymbolRef corresponding to a mutex's MemRegion</div></div><div class=""><font face="monospace, monospace" class=""><br class=""></font></div><div class=""><font face="monospace, monospace" class="">PthreadLockChecker::AcquireLock(CheckerContext &C, const CallExpr *CE,</font></div><div class=""><font face="monospace, monospace" class=""> SVal lock, bool isTryLock,</font></div><div class=""><font face="monospace, monospace" class=""> enum LockingSemantics semantics) const {</font></div><div class=""><font face="monospace, monospace" class=""> const MemRegion *lockR = lock.getAsRegion();</font></div><div class=""><font face="monospace, monospace" class=""> if (!lockR)</font></div><div class=""><font face="monospace, monospace" class=""> return;</font></div><div class=""><font face="monospace, monospace" class=""><br class=""></font></div><div class=""><font face="monospace, monospace" class=""> ProgramStateRef state = C.getState();</font></div><div class=""><font face="monospace, monospace" class=""><br class=""></font></div><div class=""><font face="monospace, monospace" class=""> SVal X = state->getSVal(CE, C.getLocationContext());</font></div><div class=""><font face="monospace, monospace" class=""> if (X.isUnknownOrUndef())</font></div><div class=""><font face="monospace, monospace" class=""> return;</font></div><div class=""><font face="monospace, monospace" class=""><br class=""></font></div><div class=""><font face="monospace, monospace" class=""> DefinedSVal retVal = X.castAs<DefinedSVal>();</font></div><div class=""><font face="monospace, monospace" class=""><br class=""></font></div><div class=""><font face="monospace, monospace" class=""> ConstraintManager &CMgr = state->getConstraintManager();</font></div><div class=""><font face="monospace, monospace" class=""> const SymbolRef* sym = state->get<RetValConstraint>(lockR); </font></div><div class=""><font face="monospace, monospace" class=""> ConditionTruthVal retZero = CMgr.isNull(state, *sym); // Is this the correct way to check if the return value is zero or not? I also tried using isZeroConstant but neither seem to work.</font></div><div class=""><font face="monospace, monospace" class=""> ...</font></div><div class=""><font face="monospace, monospace" class="">}</font></div><div class=""><font face="monospace, monospace" class=""><br class=""></font></div><div class=""><font face="monospace, monospace" class=""><div class="">void PthreadLockChecker::DestroyLock(CheckerContext &C, const CallExpr *CE,</div><div class=""> SVal Lock) const {</div><div class=""> const LockState *LState = State->get<LockMap>(LockR);</div></font><div class=""><font face="monospace, monospace" class=""> if (!LState || LState->isUnlocked()) {</font></div><div class=""><font face="monospace, monospace" class=""> SVal X = State->getSVal(CE, C.getLocationContext()); // Added this</font></div><div class=""><font face="monospace, monospace" class=""> if (X.isUnknownOrUndef()) // Added this </font></div><div class=""><font face="monospace, monospace" class=""> return;</font></div><div class=""><font face="monospace, monospace" class=""><br class=""></font></div><div class=""><font face="monospace, monospace" class=""> DefinedSVal retVal = X.castAs<DefinedSVal>(); // Added this (Is this the correct way to get return value?)</font></div><div class=""><font face="monospace, monospace" class=""> SymbolRef sym = retVal.getAsSymbol(); // Added this</font></div><div class=""><font face="monospace, monospace" class=""><br class=""></font></div><div class=""><font face="monospace, monospace" class=""> State = State->set<LockMap>(LockR, LockState::getDestroyed());</font></div><div class=""><font face="monospace, monospace" class=""> State = State->set<RetValConstraint>(LockR, sym); // Added this</font></div><div class=""><font face="monospace, monospace" class=""> C.addTransition(State);</font></div><div class=""><font face="monospace, monospace" class=""> return;</font></div><div class=""><font face="monospace, monospace" class=""> }</font></div></div><div class=""><font face="monospace, monospace" class=""> ...</font></div><div class=""><font face="monospace, monospace" class="">}</font></div><div class=""><font face="monospace, monospace" class=""><br class=""></font></div><div class=""><br class=""></div><div class=""><font face="arial, helvetica, sans-serif" class="">I have been stuck on this for a while and haven't been able to find my way around it.</font></div></div></div></blockquote><div><br class=""></div><div>This is great progress!</div><div><br class=""></div><div>What is going on here is that the analyzer is very aggressive about pruning constraints on symbols for values that the program can’t refer to again. These constraints are very expensive to keep in the store, so it removes them as quickly as possible.</div><div><br class=""></div><div>So, for example, in</div><div><br class=""></div><div><div style="margin: 0px; font-size: 11px; line-height: normal; font-family: Menlo; background-color: rgb(255, 255, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> int result = pthread_mutex_destroy(&m);</span></div><div style="margin: 0px; font-size: 11px; line-height: normal; font-family: Menlo; background-color: rgb(255, 255, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> if (result != 0) { // (1)</span></div><div style="margin: 0px; font-size: 11px; line-height: normal; font-family: Menlo; background-color: rgb(255, 255, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> pthread_mutex_lock(&m);</span></div><div style="margin: 0px; font-size: 11px; line-height: normal; font-family: Menlo; background-color: rgb(255, 255, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> }</span></div></div><div><br class=""></div><div>The ‘result’ local variable is never referred in the code to after point (1). The analyzer sees this and removes the constraint on result discovered from the guard condition almost immediately after it is executed. Then, when you query for that symbol when analyzing the call to pthread_mutex_lock(), the analyze doesn’t have any constraints.</div><div><br class=""></div><div>For example, if you were to artificially extend the lifetime of ‘result’ in the above snippet:</div><div><div><div style="margin: 0px; font-size: 11px; line-height: normal; font-family: Menlo; background-color: rgb(255, 255, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures;" class=""> int result = pthread_mutex_destroy(&m);</span></div><div style="margin: 0px; font-size: 11px; line-height: normal; font-family: Menlo; background-color: rgb(255, 255, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures;" class=""> if (result != 0) { // (1)</span></div><div style="margin: 0px; font-size: 11px; line-height: normal; font-family: Menlo; background-color: rgb(255, 255, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures;" class=""> pthread_mutex_lock(&m);</span></div><div style="margin: 0px; font-size: 11px; line-height: normal; font-family: Menlo; background-color: rgb(255, 255, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures;" class=""> }</span></div><div style="margin: 0px; font-size: 11px; line-height: normal; font-family: Menlo; background-color: rgb(255, 255, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures;" class=""> (void)result; // This extends the life of 'result'.</span></div><div class=""><span style="font-variant-ligatures: no-common-ligatures;" class=""><br class=""></span></div></div></div><div>Your isNull() query would work as you expect because the symbol is still alive at the call to pthread_mutex_lock().</div><div><br class=""></div><div>Here is a suggested solution: you can add a checkDeadSymbols callback to the PthreadChecker. The analyzer calls this whenever it sees that a symbol became dead. In this callback you can iterate through the RetValConstraint symbols — if one of them becomes dead, you can query the constraint for the value then and update the LockMap appropriately. Don’t forget to also remove the dead symbol from RetValConstraint when it becomes dead. This way the analyzer won’t keep all those extra dead symbols in memory.</div><div><br class=""></div><div>There is an example of how the use the checkDeadSymbols callback in SimpleStreamChecker.cpp.</div><div><br class=""></div><div>Devin</div><div><br class=""></div></div></body></html>