<div dir="ltr">Dear Dr. Artem,<div><br></div><div>Thank you for your response. After incorporating 'addTransition', I was able to suppress the double-destroy. But, when 'pthread_mutex_destroy' was called for the second time (i.e., inside the if branch), LockState was found to be NULL (which it should be according to my code) but ideally it should be in the Unlocked state. For, it to be in Unlocked state, I think <font face="monospace, monospace">state->set<LockMap>()</font> should be executed inside <font face="monospace, monospace">checkDeadSymbols()</font> instead of executing it inside <font face="monospace, monospace">AcquireLock()</font>, <font face="monospace, monospace">ReleaseLock()</font>, <font face="monospace, monospace">DestroyLock()</font> and <font face="monospace, monospace">InitLock() </font>as I am unable to find a way to do it otherwise.</div><div><br></div><div>Regards,</div><div>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=44c7f052-8c1a-41d9-8000-3c265d6705ac"><font color="#ffffff" size="1">ᐧ</font></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Apr 18, 2017 at 8:30 PM, Artem Dergachev <span dir="ltr"><<a href="mailto:noqnoqneo@gmail.com" target="_blank">noqnoqneo@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Before anything, please note that `State' is your local variable; assigning to `State' doesn't immediately affect analysis in any way. In order to make your changes to the program state take effect, you'd need to put the changed state back into the `CheckerContext' by calling its `addTransition' method, like other checker callbacks do.<br>
<br>
Otherwise, your code looks reasonable to me. If everything is implemented correctly, i believe that your code would already suppress the double-destroy warning on this branch.<div><div class="h5"><br>
<br>
On 4/18/17 5:53 PM, Malhar Thakkar wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
Test-case:<br>
<br>
pthread_mutex_lock(&mtx1);<br>
pthread_mutex_unlock(&mtx1);<br>
int retval = pthread_mutex_destroy(&mtx1);<br>
if(retval != 0){<br>
pthread_mutex_destroy(&mtx1); (1)<br>
}<br>
else<br>
printf("Already destroyed\n");<br>
<br>
<br>
Regarding my previous query about reverting the LockState, how would I ensure that the LockState at (1) is Unlocked and not Destroyed?<br>
<br>
Following is the code for checkDeadSymbols()<br>
void PthreadLockChecker::checkDeadS<wbr>ymbols(SymbolReaper &SymReaper,<br>
CheckerContext &C) const {<br>
ProgramStateRef State = C.getState();<br>
ConstraintManager &CMgr = State->getConstraintManager();<br>
<br>
RetValConstraintTy TrackedSymbols = State->get<RetValConstraint>()<wbr>;<br>
for (RetValConstraintTy::iterator I = TrackedSymbols.begin(),<br>
E = TrackedSymbols.end(); I != E; ++I) {<br>
SymbolRef Sym = I->second;<br>
const MemRegion* lockR = I->first;<br>
bool IsSymDead = SymReaper.isDead(Sym);<br>
const LockState* LState = State->get<LockMap>(lockR);<br>
// Remove the dead symbol from the return value symbols map.<br>
if (IsSymDead){<br>
ConditionTruthVal retZero = CMgr.isNull(State, Sym);<br>
if(retZero.isConstrainedFalse(<wbr>)){<br>
// Update LockMap<br>
State = State->remove<LockMap>(lockR); // I know this is incorrect but even after removing this entry from the map, (1) raises a warning saying, "This lock has already been destroyed".<br>
}<br>
State = State->remove<RetValConstraint<wbr>>(lockR);<br>
}<br>
}<br>
}<br>
<br>
Thank you.<br>
<br>
<br>
Regards,<br>
Malhar<br>
<br>
<br></div></div>
ᐧ<span class=""><br>
<br>
On Mon, Apr 17, 2017 at 8:34 PM, Devin Coughlin <<a href="mailto:dcoughlin@apple.com" target="_blank">dcoughlin@apple.com</a> <mailto:<a href="mailto:dcoughlin@apple.com" target="_blank">dcoughlin@apple.com</a>>> wrote:<br>
<br>
<br>
</span><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">
On Apr 17, 2017, at 4:55 AM, Malhar Thakkar <<a href="mailto:cs13b1031@iith.ac.in" target="_blank">cs13b1031@iith.ac.in</a><br></span><div><div class="h5">
<mailto:<a href="mailto:cs13b1031@iith.ac.in" target="_blank">cs13b1031@iith.ac.in</a>>> wrote:<br>
<br>
Consider the following test-case:<br>
<br>
int retval = pthread_mutex_destroy(&mtx1);<br>
if(retval == 0){<br>
pthread_mutex_lock(&mtx1);<br>
}<br>
<br>
<br>
REGISTER_MAP_WITH_PROGRAMSTATE<wbr>(RetValConstraint, const MemRegion<br>
*, SymbolRef)<br>
<br>
I have added the following snippet for checkDeadSymbols:<br>
void PthreadLockChecker::checkDeadS<wbr>ymbols(SymbolReaper &SymReaper,<br>
CheckerContext &C) const {<br>
// std::cout<<"Checking dead symbols\n";<br>
ProgramStateRef State = C.getState();<br>
ConstraintManager &CMgr = State->getConstraintManager();<br>
<br>
RetValConstraintTy TrackedSymbols = State->get<RetValConstraint>()<wbr>;<br>
// int counter = 0;<br>
for (RetValConstraintTy::iterator I = TrackedSymbols.begin(),<br>
E = TrackedSymbols.end(); I != E; ++I) {<br>
// counter++;<br>
// std::cout << "Counter: "<<counter<<std::endl;<br>
SymbolRef Sym = I->second;<br>
const MemRegion* lockR = I->first;<br>
bool IsSymDead = SymReaper.isDead(Sym);<br>
<br>
// Remove the dead symbol from the return value symbols map.<br>
if (IsSymDead){<br>
ConditionTruthVal retZero = CMgr.isNull(State, Sym);<br>
if(retZero.isConstrainedFalse(<wbr>)){<br>
std::cout<<"False\n";<br>
// Update LockMap<br>
}<br>
else if(retZero.isConstrainedTrue()<wbr>){<br>
std::cout<<"True\n";<br>
}<br>
State = State->remove<RetValConstraint<wbr>>(lockR);<br>
std::cout<<"Removed\n";<br>
}<br>
}<br>
}<br>
<br>
Now, after the execution of PthreadLockChecker::DestroyLoc<wbr>k(),<br>
checkDeadSymbols() is executed twice before<br>
PthreadLockChecker::AcquireLoc<wbr>k() is executed.<br>
<br>
When checkDeadSymbols is first executed, there is just one symbol<br>
in RetValConstraint(trivial). But, this symbol is constrained<br></div></div>
/not /to be NULL. Then, the symbol is removed. During the<div><div class="h5"><br>
execution of checkDeadSymbols for the second time, there is again<br>
one symbol in RetValConstraint(I don't understand this. Shouldn't<br>
this symbol have been destroyed during the previous execution?).<br>
Nevertheless, this time, this symbol is constrained to be NULL.<br>
</div></div></blockquote><div><div class="h5">
<br>
The static analyzer performs a path-sensitive exploration of the<br>
program. This means that when it sees a branch it will explore<br>
both both sides of the branch independently (unless it can tell<br>
that one side is infeasible). In this case it means the analyzer<br>
will explore the path when retval is 0 and when it is not. If you<br>
haven’t read it yet, the “Debugging” section the the checker<br>
development manual describes some tricks for how to visualize the<br>
analyzer’s exploration.<br>
<<a href="https://clang-analyzer.llvm.org/checker_dev_manual.html#commands" rel="noreferrer" target="_blank">https://clang-analyzer.llvm.o<wbr>rg/checker_dev_manual.html#com<wbr>mands</a><br>
<<a href="https://clang-analyzer.llvm.org/checker_dev_manual.html#commands" rel="noreferrer" target="_blank">https://clang-analyzer.llvm.o<wbr>rg/checker_dev_manual.html#com<wbr>mands</a>>>.<br>
I find the debug.ViewExplodedGraph checker particularly helpful.<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Also, I have one more query. After fixing the above mentioned<br>
issue, how do I update LockMap in the sense that I'll need to<br>
revert the change made to it if the symbol is constrained not to<br>
be NULL. Apart from keeping track of the previous LockState, is<br>
there any other way to do it?<br>
</blockquote>
<br>
Since the analyzer keeps its representation of the program state<br>
per-path and explores paths independently, you shouldn’t need to<br>
do any reverting to undo the effects of simulating other paths to<br>
reaching a particular program point.<br>
<br>
Devin<br>
<br>
<br>
</div></div></blockquote>
<br>
</blockquote></div><br></div>