Consider the following test-case:
int retval = pthread_mutex_destroy(&mtx1);
if(retval == 0){
pthread_mutex_lock(&mtx1);
}
REGISTER_MAP_WITH_PROGRAMSTATE(RetValConstraint, const MemRegion *, SymbolRef)
I have added the following snippet for checkDeadSymbols:
void PthreadLockChecker::checkDeadSymbols(SymbolReaper &SymReaper,
CheckerContext &C) const {
// std::cout<<“Checking dead symbols\n”;
ProgramStateRef State = C.getState();
ConstraintManager &CMgr = State->getConstraintManager();
RetValConstraintTy TrackedSymbols = State->get();
// int counter = 0;
for (RetValConstraintTy::iterator I = TrackedSymbols.begin(),
E = TrackedSymbols.end(); I != E; ++I) {
// counter++;
// std::cout << "Counter: "<<counter<<std::endl;
SymbolRef Sym = I->second;
const MemRegion* lockR = I->first;
bool IsSymDead = SymReaper.isDead(Sym);
// Remove the dead symbol from the return value symbols map.
if (IsSymDead){
ConditionTruthVal retZero = CMgr.isNull(State, Sym);
if(retZero.isConstrainedFalse()){
std::cout<<“False\n”;
// Update LockMap
}
else if(retZero.isConstrainedTrue()){
std::cout<<“True\n”;
}
State = State->remove(lockR);
std::cout<<“Removed\n”;
}
}
}
Now, after the execution of PthreadLockChecker::DestroyLock(), checkDeadSymbols() is executed twice before PthreadLockChecker::AcquireLock() is executed.
When checkDeadSymbols is first executed, there is just one symbol in RetValConstraint(trivial). But, this symbol is constrained not 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.
Finally, PthreadLockChecker::AcquireLock() is executed.
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?
Thank you.
Regards,
Malhar