<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="gmail-Apple-tab-span" style="white-space:pre"> </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_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::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>();</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()){</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()){</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<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::DestroyLock(), checkDeadSymbols() is executed twice before PthreadLockChecker::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><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">Finally, </font><span style="font-family:arial,helvetica,sans-serif">PthreadLockChecker::AcquireLock() is executed.</span></div><div><span style="font-family:arial,helvetica,sans-serif"><br></span></div><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><span style="font-family:arial,helvetica,sans-serif"><br></span></div><div><span style="font-family:arial,helvetica,sans-serif">Thank you.</span></div><div><span style="font-family:arial,helvetica,sans-serif"><br></span></div><div><span style="font-family:arial,helvetica,sans-serif"><br></span></div><div><span style="font-family:arial,helvetica,sans-serif"><br></span></div><div><span style="font-family:arial,helvetica,sans-serif">Regards,</span></div><div><span style="font-family:arial,helvetica,sans-serif">Malhar</span></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Apr 15, 2017 at 11:34 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"><span class=""><br>
<br>
On 4/15/17 8:21 PM, Devin Coughlin wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On Apr 15, 2017, at 10:15 AM, Artem Dergachev <<a href="mailto:noqnoqneo@gmail.com" target="_blank">noqnoqneo@gmail.com</a>> wrote:<br>
<br>
The other part of the "check if the return value was checked" is the escape problem. For example, if we have:<br>
<br>
int result = pthread_mutex_destroy(&m);<br>
if (is_bad_result(result)) {<br>
pthread_mutex_lock(&m);<br>
}<br>
<br>
and body of is_bad_result() is not modeled, then the return value symbol is dead and unconstrained, but we may still need to suppress the checker's warning. In this case, we say that the symbol "escapes" to an unknown function (it may also escape to a global variable, for example, or be passed into the function as part of a structure or an array)<br>
<br>
The real problem here is, we have a convenient checkPointerEscape callback that handles situations when a pointer "escapes" in any way, which we use to suppress memory leak reports for escaped pointers, but we don't have a similar callback for non-pointers. So it's not easy to track escapes in this case. I'm all for implementing such callback.<br>
</blockquote>
Artem makes a very good point — but I would suggest not tackling adding this new callback as part of the starter bug.<br>
<br>
Devin<br>
</blockquote>
<br></span><span class="">
Yep, i agree. The example i point out is unlikely; the only reasonable case i imagine is something like if (EXPECT(result)), but we model that in the builtin function checker. But generally, if we commit more effort into "unchecked return value" checks, we'd have to deal with this somehow.<br>
</span><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br><div><div class="h5">
On 4/15/17 7:14 PM, Devin Coughlin via cfe-dev wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On Apr 15, 2017, at 3:52 AM, Malhar Thakkar <<a href="mailto:cs13b1031@iith.ac.in" target="_blank">cs13b1031@iith.ac.in</a> <mailto:<a href="mailto:cs13b1031@iith.ac.in" target="_blank">cs13b1031@iith.ac.in</a>>> wrote:<br>
<br>
Dear Dr. Devin,<br>
<br>
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.<br>
<br>
The changes made are mentioned below.<br>
<br>
<br>
REGISTER_MAP_WITH_PROGRAMSTATE<wbr>(RetValConstraint, const MemRegion *, SymbolRef) // Map to store SymbolRef corresponding to a mutex's MemRegion<br>
<br>
PthreadLockChecker::AcquireLoc<wbr>k(CheckerContext &C, const CallExpr *CE,<br>
SVal lock, bool isTryLock,<br>
enum LockingSemantics semantics) const {<br>
const MemRegion *lockR = lock.getAsRegion();<br>
if (!lockR)<br>
return;<br>
<br>
ProgramStateRef state = C.getState();<br>
<br>
SVal X = state->getSVal(CE, C.getLocationContext());<br>
if (X.isUnknownOrUndef())<br>
return;<br>
<br>
DefinedSVal retVal = X.castAs<DefinedSVal>();<br>
<br>
ConstraintManager &CMgr = state->getConstraintManager();<br>
const SymbolRef* sym = state->get<RetValConstraint>(l<wbr>ockR);<br>
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.<br>
...<br>
}<br>
<br>
void PthreadLockChecker::DestroyLoc<wbr>k(CheckerContext &C, const CallExpr *CE,<br>
SVal Lock) const {<br>
const LockState *LState = State->get<LockMap>(LockR);<br>
if (!LState || LState->isUnlocked()) {<br>
SVal X = State->getSVal(CE, C.getLocationContext()); // Added this<br>
if (X.isUnknownOrUndef()) // Added this<br>
return;<br>
<br>
DefinedSVal retVal = X.castAs<DefinedSVal>(); // Added this (Is this the correct way to get return value?)<br>
SymbolRef sym = retVal.getAsSymbol(); // Added this<br>
<br>
State = State->set<LockMap>(LockR, LockState::getDestroyed());<br>
State = State->set<RetValConstraint>(L<wbr>ockR, sym); // Added this<br>
C.addTransition(State);<br>
return;<br>
}<br>
...<br>
}<br>
<br>
<br>
I have been stuck on this for a while and haven't been able to find my way around it.<br>
</blockquote>
This is great progress!<br>
<br>
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.<br>
<br>
So, for example, in<br>
<br>
int result = pthread_mutex_destroy(&m);<br>
if (result != 0) { // (1)<br>
pthread_mutex_lock(&m);<br>
}<br>
<br>
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.<br>
<br>
For example, if you were to artificially extend the lifetime of ‘result’ in the above snippet:<br>
int result = pthread_mutex_destroy(&m);<br>
if (result != 0) { // (1)<br>
pthread_mutex_lock(&m);<br>
}<br>
(void)result; // This extends the life of 'result'.<br>
<br>
Your isNull() query would work as you expect because the symbol is still alive at the call to pthread_mutex_lock().<br>
<br>
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.<br>
<br>
There is an example of how the use the checkDeadSymbols callback in SimpleStreamChecker.cpp.<br>
<br>
Devin<br>
<br>
<br>
<br>
______________________________<wbr>_________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br>
<a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/cfe-dev</a><br>
</blockquote></div></div></blockquote></blockquote>
<br>
</blockquote></div><br></div>