[cfe-dev] Suggested starter bug on clang analyzer codebase

[Devin Coughlin via cfe-dev]

> On Apr 15, 2017, at 3:52 AM, Malhar Thakkar <cs13b1031 at iith.ac.in> wrote:
> 
> Dear Dr. Devin,
> 
> 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. 
> 
> The changes made are mentioned below.
> 
> 
> REGISTER_MAP_WITH_PROGRAMSTATE(RetValConstraint, const MemRegion *, SymbolRef) // Map to store SymbolRef                                                                                 corresponding to a mutex's MemRegion
> 
> PthreadLockChecker::AcquireLock(CheckerContext &C, const CallExpr *CE,
>                                      SVal lock, bool isTryLock,
>                                      enum LockingSemantics semantics) const {
>   const MemRegion *lockR = lock.getAsRegion();
>   if (!lockR)
>     return;
> 
>   ProgramStateRef state = C.getState();
> 
>   SVal X = state->getSVal(CE, C.getLocationContext());
>   if (X.isUnknownOrUndef())
>     return;
> 
>   DefinedSVal retVal = X.castAs<DefinedSVal>();
> 
>   ConstraintManager &CMgr = state->getConstraintManager();
>   const SymbolRef* sym = state->get<RetValConstraint>(lockR); 
>   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.
>   ...
> }
> 
> void PthreadLockChecker::DestroyLock(CheckerContext &C, const CallExpr *CE,
>                                      SVal Lock) const {
>   const LockState *LState = State->get<LockMap>(LockR);
>   if (!LState || LState->isUnlocked()) {
>     SVal X = State->getSVal(CE, C.getLocationContext());  // Added this
>     if (X.isUnknownOrUndef())                             // Added this 
>       return;
> 
>     DefinedSVal retVal = X.castAs<DefinedSVal>();         // Added this (Is this the correct way to get return                                                                value?)
>     SymbolRef sym = retVal.getAsSymbol();                 // Added this
> 
>     State = State->set<LockMap>(LockR, LockState::getDestroyed());
>     State = State->set<RetValConstraint>(LockR, sym);              // Added this
>     C.addTransition(State);
>     return;
>   }
>   ...
> }
> 
> 
> I have been stuck on this for a while and haven't been able to find my way around it.

This is great progress!

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.

So, for example, in

  int result = pthread_mutex_destroy(&m);
  if (result != 0) { // (1)
    pthread_mutex_lock(&m);
  }

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.

For example, if you were to artificially extend the lifetime of ‘result’ in the above snippet:
  int result = pthread_mutex_destroy(&m);
  if (result != 0) { // (1)
    pthread_mutex_lock(&m);
  }
  (void)result; // This extends the life of 'result'.

Your isNull() query would work as you expect because the symbol is still alive at the call to pthread_mutex_lock().

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.

There is an example of how the use the checkDeadSymbols callback in SimpleStreamChecker.cpp.

Devin

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20170415/4c5ca8ad/attachment.html>