<div dir="ltr">Test-case:<div><br><div><div><font face="monospace, monospace">pthread_mutex_lock(&mtx1);</font></div><div><font face="monospace, monospace">pthread_mutex_unlock(&mtx1);</font></div><div><font face="monospace, monospace">int retval = pthread_mutex_destroy(&mtx1);</font></div><div><font face="monospace, monospace">if(retval != 0){</font></div><div><font face="monospace, monospace"><span class="gmail-Apple-tab-span" style="white-space:pre"> </span>pthread_mutex_destroy(&mtx1); (1)</font></div><div><font face="monospace, monospace">}</font></div><div><font face="monospace, monospace">else</font></div><div><font face="monospace, monospace"><span class="gmail-Apple-tab-span" style="white-space:pre"> </span>printf("Already destroyed\n");</font></div></div></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><br></font></div><div><font face="arial, helvetica, sans-serif">Regarding my previous query about reverting the LockState, how would I ensure that the LockState at (1) is Unlocked and not Destroyed?</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">Following is the code for checkDeadSymbols()</font></div><div><div><font face="monospace, monospace">void PthreadLockChecker::checkDeadSymbols(SymbolReaper &SymReaper,</font></div><div><font face="monospace, monospace"> CheckerContext &C) const {</font></div><div><font face="monospace, monospace"> ProgramStateRef State = C.getState();</font></div><div><font face="monospace, monospace"> ConstraintManager &CMgr = State->getConstraintManager();</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"> RetValConstraintTy TrackedSymbols = State->get<RetValConstraint>();</font></div><div><font face="monospace, monospace"> for (RetValConstraintTy::iterator I = TrackedSymbols.begin(),</font></div><div><font face="monospace, monospace"> E = TrackedSymbols.end(); I != E; ++I) {</font></div><div><font face="monospace, monospace"> SymbolRef Sym = I->second;</font></div><div><font face="monospace, monospace"> const MemRegion* lockR = I->first;</font></div><div><font face="monospace, monospace"> bool IsSymDead = SymReaper.isDead(Sym);</font></div><div><font face="monospace, monospace"> const LockState* LState = State->get<LockMap>(lockR); </font></div><div><font face="monospace, monospace"> // Remove the dead symbol from the return value symbols map.</font></div><div><font face="monospace, monospace"> if (IsSymDead){</font></div><div><font face="monospace, monospace"> ConditionTruthVal retZero = CMgr.isNull(State, Sym);</font></div><div><font face="monospace, monospace"> if(retZero.isConstrainedFalse()){</font></div><div><font face="monospace, monospace"> // Update LockMap</font></div><div><font face="monospace, monospace"> State = State->remove<LockMap>(lockR); // I know this is incorrect but even after removing this entry from the map, (1) raises a warning saying, "</font><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"><font face="monospace, monospace">This lock has already been destroyed</font></span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0);font-family:menlo;font-size:11px">".</span></div>
<div><font face="monospace, monospace"> }</font></div><div><font face="monospace, monospace"> State = State->remove<RetValConstraint>(lockR);</font></div><div><font face="monospace, monospace"> }</font></div><div><font face="monospace, monospace"> }</font></div><div><font face="monospace, monospace">}</font></div></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><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><br></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=03f99754-da79-48f5-9fa6-af9de507c264"><font color="#ffffff" size="1">ᐧ</font></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Apr 17, 2017 at 8:34 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><div><div class="h5"><blockquote type="cite"><div>On Apr 17, 2017, at 4:55 AM, Malhar Thakkar <<a href="mailto:cs13b1031@iith.ac.in" target="_blank">cs13b1031@iith.ac.in</a>> wrote:</div><br class="m_-7908023057935966487Apple-interchange-newline"><div><div dir="ltr">Consider the following test-case:<div><br></div><div><div><font face="monospace, monospace">int retval = pthread_mutex_destroy(&mtx1);</font></div><div><font face="monospace, monospace">if(retval == 0){</font></div><div><font face="monospace, monospace"><span class="m_-7908023057935966487gmail-Apple-tab-span" style="white-space:pre-wrap"> </span>pthread_mutex_lock(&mtx1);</font></div><div><font face="monospace, monospace">}</font></div></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">REGISTER_MAP_WITH_<wbr>PROGRAMSTATE(RetValConstraint, const MemRegion *, SymbolRef)<br></font></div><div><font face="monospace, monospace"><br></font></div><div><font face="arial, helvetica, sans-serif">I have added the following snippet for checkDeadSymbols:</font></div><div><div><font face="monospace, monospace">void PthreadLockChecker::<wbr>checkDeadSymbols(SymbolReaper &SymReaper,</font></div><div><font face="monospace, monospace"> CheckerContext &C) const {</font></div><div><font face="monospace, monospace"> // std::cout<<"Checking dead symbols\n";</font></div><div><font face="monospace, monospace"> ProgramStateRef State = C.getState();</font></div><div><font face="monospace, monospace"> ConstraintManager &CMgr = State->getConstraintManager();</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"> RetValConstraintTy TrackedSymbols = State->get<RetValConstraint>()<wbr>;</font></div><div><font face="monospace, monospace"> // int counter = 0;</font></div><div><font face="monospace, monospace"> for (RetValConstraintTy::iterator I = TrackedSymbols.begin(),</font></div><div><font face="monospace, monospace"> E = TrackedSymbols.end(); I != E; ++I) {</font></div><div><font face="monospace, monospace"> // counter++;</font></div><div><font face="monospace, monospace"> // std::cout << "Counter: "<<counter<<std::endl;</font></div><div><font face="monospace, monospace"> SymbolRef Sym = I->second;</font></div><div><font face="monospace, monospace"> const MemRegion* lockR = I->first;</font></div><div><font face="monospace, monospace"> bool IsSymDead = SymReaper.isDead(Sym);</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"> // Remove the dead symbol from the return value symbols map.</font></div><div><font face="monospace, monospace"> if (IsSymDead){</font></div><div><font face="monospace, monospace"> ConditionTruthVal retZero = CMgr.isNull(State, Sym);</font></div><div><font face="monospace, monospace"> if(retZero.isConstrainedFalse(<wbr>)){</font></div><div><font face="monospace, monospace"> std::cout<<"False\n";</font></div><div><font face="monospace, monospace"> // Update LockMap</font></div><div><font face="monospace, monospace"> }</font></div><div><font face="monospace, monospace"> else if(retZero.isConstrainedTrue()<wbr>){</font></div><div><font face="monospace, monospace"> std::cout<<"True\n";</font></div><div><font face="monospace, monospace"> }</font></div><div><font face="monospace, monospace"> State = State->remove<<wbr>RetValConstraint>(lockR);</font></div><div><font face="monospace, monospace"> std::cout<<"Removed\n";</font></div><div><font face="monospace, monospace"> }</font></div><div><font face="monospace, monospace"> }</font></div><div><font face="monospace, monospace">}</font></div></div><div><font face="monospace, monospace"><br></font></div><div><font face="arial, helvetica, sans-serif">Now, after the execution of PthreadLockChecker::<wbr>DestroyLock(), checkDeadSymbols() is executed twice before PthreadLockChecker::<wbr>AcquireLock() is executed.</font></div><div><br></div><div><font face="arial, helvetica, sans-serif">When checkDeadSymbols is first executed, there is just one symbol in RetValConstraint(trivial). But, this symbol is constrained <i>not </i>to be NULL. Then, the symbol is removed. During the execution of checkDeadSymbols for the second time, there is again one symbol in RetValConstraint(I don't understand this. Shouldn't this symbol have been destroyed during the previous execution?). Nevertheless, this time, this symbol is constrained to be NULL.</font></div></div></div></blockquote><div><br></div></div></div><div>The static analyzer performs a path-sensitive exploration of the program. This means that when it sees a branch it will explore both both sides of the branch independently (unless it can tell that one side is infeasible). In this case it means the analyzer will explore the path when retval is 0 and when it is not. If you haven’t read it yet, the “Debugging” section the the checker development manual describes some tricks for how to visualize the analyzer’s exploration. <<a href="https://clang-analyzer.llvm.org/checker_dev_manual.html#commands" target="_blank">https://clang-analyzer.llvm.<wbr>org/checker_dev_manual.html#<wbr>commands</a>>. I find the debug.ViewExplodedGraph checker particularly helpful.</div><span class=""><div><br></div><blockquote type="cite"><div><div dir="ltr"><div><span style="font-family:arial,helvetica,sans-serif">Also, I have one more query. After fixing the above mentioned issue, how do I update LockMap in the sense that I'll need to revert the change made to it if the symbol is constrained not to be NULL. Apart from keeping track of the previous LockState, is there any other way to do it?</span></div></div></div></blockquote><div><br></div></span><div>Since the analyzer keeps its representation of the program state per-path and explores paths independently, you shouldn’t need to do any reverting to undo the effects of simulating other paths to reaching a particular program point.</div><span class="HOEnZb"><font color="#888888"><div><br></div></font></span></div><span class="HOEnZb"><font color="#888888">Devin</font></span></div></blockquote></div><br></div>