<div dir="ltr"><div><div><font face="arial, helvetica, sans-serif">Dear Dr. Devin,</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">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><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">The changes made are mentioned below.</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div style="font-family:monospace,monospace"><br></div><div style="font-family:monospace,monospace">REGISTER_MAP_WITH_PROGRAMSTATE(RetValConstraint, const MemRegion *, SymbolRef) // Map to store SymbolRef corresponding to a mutex's MemRegion</div></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">PthreadLockChecker::AcquireLock(CheckerContext &C, const CallExpr *CE,</font></div><div><font face="monospace, monospace"> SVal lock, bool isTryLock,</font></div><div><font face="monospace, monospace"> enum LockingSemantics semantics) const {</font></div><div><font face="monospace, monospace"> const MemRegion *lockR = lock.getAsRegion();</font></div><div><font face="monospace, monospace"> if (!lockR)</font></div><div><font face="monospace, monospace"> return;</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"> ProgramStateRef state = C.getState();</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"> SVal X = state->getSVal(CE, C.getLocationContext());</font></div><div><font face="monospace, monospace"> if (X.isUnknownOrUndef())</font></div><div><font face="monospace, monospace"> return;</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"> DefinedSVal retVal = X.castAs<DefinedSVal>();</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"> ConstraintManager &CMgr = state->getConstraintManager();</font></div><div><font face="monospace, monospace"> const SymbolRef* sym = state->get<RetValConstraint>(lockR); </font></div><div><font face="monospace, monospace"> 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><font face="monospace, monospace"> ...</font></div><div><font face="monospace, monospace">}</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><div>void PthreadLockChecker::DestroyLock(CheckerContext &C, const CallExpr *CE,</div><div> SVal Lock) const {</div><div> const LockState *LState = State->get<LockMap>(LockR);</div></font><div><font face="monospace, monospace"> if (!LState || LState->isUnlocked()) {</font></div><div><font face="monospace, monospace"> SVal X = State->getSVal(CE, C.getLocationContext()); // Added this</font></div><div><font face="monospace, monospace"> if (X.isUnknownOrUndef()) // Added this </font></div><div><font face="monospace, monospace"> return;</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"> DefinedSVal retVal = X.castAs<DefinedSVal>(); // Added this (Is this the correct way to get return value?)</font></div><div><font face="monospace, monospace"> SymbolRef sym = retVal.getAsSymbol(); // Added this</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"> State = State->set<LockMap>(LockR, LockState::getDestroyed());</font></div><div><font face="monospace, monospace"> State = State->set<RetValConstraint>(LockR, sym); // Added this</font></div><div><font face="monospace, monospace"> C.addTransition(State);</font></div><div><font face="monospace, monospace"> return;</font></div><div><font face="monospace, monospace"> }</font></div></div><div><font face="monospace, monospace"> ...</font></div><div><font face="monospace, monospace">}</font></div><div><font face="monospace, monospace"><br></font></div><div><br></div><div><font face="arial, helvetica, sans-serif">I have been stuck on this for a while and haven't been able to find my way around it.</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">Regards,</font></div><div><font face="arial, helvetica, sans-serif">Malhar</font></div></div><div hspace="streak-pt-mark" style="max-height:1px"><img alt="" style="width:0px;max-height:0px;overflow:hidden" src="https://mailfoogae.appspot.com/t?sender=aY3MxM2IxMDMxQGlpdGguYWMuaW4%3D&type=zerocontent&guid=dd7ccb94-c66e-4d17-8cad-7d5471cfa6bc"><font color="#ffffff" size="1">ᐧ</font></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Apr 13, 2017 at 11:48 AM, Devin Coughlin <span dir="ltr"><<a href="mailto:dcoughlin@apple.com" target="_blank">dcoughlin@apple.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><br><div><span class=""><blockquote type="cite"><div>On Apr 12, 2017, at 10:47 PM, Malhar Thakkar <<a href="mailto:cs13b1031@iith.ac.in" target="_blank">cs13b1031@iith.ac.in</a>> wrote:</div><br class="m_-3602678140077335570Apple-interchange-newline"><div><div dir="ltr">Dear Dr. Devin,<div><br></div><div>Thank you for your response. </div><div>Just to be clear, I think I'll have to query what is known about the symbol in PthreadLockChecker::<wbr>ReleaseLock() instead of PthreadLockChecker::<wbr>AcquireLock() as pthread_mutex_destroy() returns a non-zero value when a mutex is locked by another thread. </div><div>So, in order to destroy that mutex, one would first need to unlock it and then destroy it. </div></div></div></blockquote><div><br></div></span><div>In general, unlocking a mutex that is held by another thread is undefined behavior, so the snippet below is not safe. It would be great to improve the diagnostic emitted for the snippet below explaining why it is not safe — but for now let’s focus on fixing the false positive I mentioned before.</div><span class=""><div><br></div><blockquote type="cite"><div><div dir="ltr"><div>The code snippet which produces a false positive in the current checker:</div><div><br></div><div><div><font face="monospace, monospace">if(pthread_mutex_destroy(&(o-><wbr>lock_mutex))!=0) {</font></div><div><font face="monospace, monospace"> pthread_mutex_unlock(&(o-><wbr>lock_mutex)); // It raises a warning here.</font></div><div><font face="monospace, monospace"> pthread_mutex_destroy(&(o-><wbr>lock_mutex));</font></div><div><font face="monospace, monospace">}</font></div></div></div></div></blockquote><div><br></div></span><div>Another example (in addition to the one I gave before) that it would be good to treat as safe is similar to what you have above, but without the unlock:</div><div><br></div><div>if (pthread_mutex_destroy(&m) != 0) {</div><div><span class="m_-3602678140077335570Apple-tab-span" style="white-space:pre-wrap"> </span>pthread_mutex_destroy(&m); // Should not warn here</div><div>}</div><div><br></div><div>The fix for that would be exactly analogous to what I outlined before but you would query that symbol that is the result of the previous call to pthread_mutex_destroy() when deciding whether to diagnose on the second call to pthread_mutex_destroy()</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>Devin</div></font></span><div><div class="h5"><br><blockquote type="cite"><div><div dir="ltr"><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><br></font></div><div><font face="arial, helvetica, sans-serif">Thank you.</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">Regards,</font></div><div><font face="arial, helvetica, sans-serif">Malhar</font></div></div><div hspace="streak-pt-mark" style="max-height:1px"><img alt="" style="width:0px;max-height:0px;overflow:hidden" src="https://mailfoogae.appspot.com/t?sender=aY3MxM2IxMDMxQGlpdGguYWMuaW4%3D&type=zerocontent&guid=715c5098-5a4e-4582-9fc2-2420112455e8"><font color="#ffffff" size="1">ᐧ</font></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Apr 12, 2017 at 11:13 PM, Devin Coughlin <span dir="ltr"><<a href="mailto:dcoughlin@apple.com" target="_blank">dcoughlin@apple.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><br><div><span><blockquote type="cite"><div>On Apr 12, 2017, at 3:32 AM, Malhar Thakkar <<a href="mailto:cs13b1031@iith.ac.in" target="_blank">cs13b1031@iith.ac.in</a>> wrote:</div><br class="m_-3602678140077335570m_-2880835901772509220Apple-interchange-newline"><div><div dir="ltr">Hello Dr. Devin,<div><br></div><div>I have the following approach in mind.</div><div>Just like the Unix API stream checker (where the return value of fopen is checked), <span style="font-size:12.8px">we can use the constraint manager to check if the return value of any function (for example: pthread_mutex_destroy) is zero or not.</span></div><div style="font-size:12.8px">If it is non-zero (which indicates failure), then we don't update the set & map which are used to keep track of the states all mutex variables.</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">Let me know your thoughts on this.</div></div></div></blockquote><div><br></div></span><div>Malhar,</div><div><br></div><div>These sounds like the right approach to me, although I would focus only on pthread_mutex_destroy()’s return value for now.</div><div><br></div><div>One thing that makes this slightly tricky is that at the point of the return from the call to pthread_mutex_destroy() we don’t know anything about the return value — it is only later, when the programmer checks that value (in a if statement, for example) that the analyzer can discover whether the value returned was zero or not.</div><div><br></div><div>Here is an example:</div><div> pthread_mutex_t m;</div> pthread_mutex_init(&m, NULL)<wbr>;</div><div> </div><div> // … </div><div><br><div> int result = pthread_mutex_destroy(&m);<br> // (1) At this point the analyzer doesn’t know value of result.</div><div> // It tracks it as a symbol with no constraints<br><br> if (result != 0) { // (2) At this point the analyzer constrains the symbol from (1) to be non-zero</div><div><br></div><div><span class="m_-3602678140077335570m_-2880835901772509220Apple-tab-span" style="white-space:pre-wrap"> </span>// (3) At this point the checker should look at the at the symbol.</div><div><span class="m_-3602678140077335570m_-2880835901772509220Apple-tab-span" style="white-space:pre-wrap"> </span>// If it is unknown or is definitely zero (meaning the destroy succeeded)</div><div><span class="m_-3602678140077335570m_-2880835901772509220Apple-tab-span" style="white-space:pre-wrap"> </span>// it should emit a diagnostic. But if it is definitely non-zero then</div><div><span class="m_-3602678140077335570m_-2880835901772509220Apple-tab-span" style="white-space:pre-wrap"> </span>// the analyzer should not report the diagnostic.</div><div> pthread_mutex_lock(&m); <br></div><div> }</div><div><br></div><div>What this means is that you’ll need to modify PthreadLockChecker::DestroyLoc<wbr>k() to keep track of the returned symbol from pthread_mutex_destroy() in the LockState and then query what is known about that symbol in PthreadLockChecker::AcquireLoc<wbr>k().</div><div><br></div><div>Please don’t hesitate to ask if you more questions!</div><span class="m_-3602678140077335570HOEnZb"><font color="#888888"><div><br></div><div>Devin</div></font></span><div><br></div><div><div>P.S. In the future you should CC the cfe-dev mailing on these kinds of questions so that the community can offer their own input and get a sense of what you are working on!</div><div><br></div><div><br></div></div><span><br><blockquote type="cite"><div><div dir="ltr"><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">Thank you.</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">Regards,</div><div style="font-size:12.8px">Malhar</div></div><div hspace="streak-pt-mark" style="max-height:1px"><img alt="" style="width:0px;max-height:0px;overflow:hidden" src="https://mailfoogae.appspot.com/t?sender=aY3MxM2IxMDMxQGlpdGguYWMuaW4%3D&type=zerocontent&guid=0508328b-d425-4ea1-b7e8-a3e2635356ed"><font color="#ffffff" size="1">ᐧ</font></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Apr 7, 2017 at 2:26 AM, Devin Coughlin <span dir="ltr"><<a href="mailto:dcoughlin@apple.com" target="_blank">dcoughlin@apple.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Malhar (+Michael, cc’d),<br>
<br>
Here is a suggested starter bug on the clang static analyzer code base:<br>
<br>
“False Positive PthreadLockChecker Use destroyed lock” <<a href="https://bugs.llvm.org/show_bug.cgi?id=32455" rel="noreferrer" target="_blank">https://bugs.llvm.org/show_bu<wbr>g.cgi?id=32455</a>><br>
<br>
The analyzer has a checker (PthreadLockChecker.cpp) that emits a diagnostic when the programmer tries to acquire a mutex twice or lock a mutex that has already been destroyed. Unfortunately, it has a false positive: if the programmer calls pthread_destroy_lock() and that call fails (returns a non-zero value) and then later tries to lock then the analyzer incorrectly warns that the mutex has been destroyed. There is an example of the false positive in the linked bugzilla URL above.<br>
<br>
Fixing this false positive is a good starter bug to get you familiar with the checker side of the analyzer. If you haven’t seen it already, a good place to start would be the Checker Development Manual <<a href="https://clang-analyzer.llvm.org/checker_dev_manual.html" rel="noreferrer" target="_blank">https://clang-analyzer.llvm.o<wbr>rg/checker_dev_manual.html</a>>.<br>
<br>
And please don’t hesitate to email if you have any questions or want to discuss approaches to fixing the bug!<br>
<span class="m_-3602678140077335570m_-2880835901772509220HOEnZb"><font color="#888888"><br>
Devin<br>
<br>
</font></span></blockquote></div><br></div>
</div></blockquote></span></div><br></div></blockquote></div><br></div>
</div></blockquote></div></div></div><br></div></blockquote></div><br></div>