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

[Artem Dergachev via cfe-dev]

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.

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.

On 4/18/17 5:53 PM, Malhar Thakkar wrote:
> Test-case:
>
> pthread_mutex_lock(&mtx1);
> pthread_mutex_unlock(&mtx1);
> int retval = pthread_mutex_destroy(&mtx1);
> if(retval != 0){
> pthread_mutex_destroy(&mtx1); (1)
> }
> else
> printf("Already destroyed\n");
>
>
> Regarding my previous query about reverting the LockState, how would I 
> ensure that the LockState at (1) is Unlocked and not Destroyed?
>
> Following is the code for checkDeadSymbols()
> void PthreadLockChecker::checkDeadSymbols(SymbolReaper &SymReaper,
>                    CheckerContext &C) const {
>   ProgramStateRef State = C.getState();
>   ConstraintManager &CMgr = State->getConstraintManager();
>
>   RetValConstraintTy TrackedSymbols = State->get<RetValConstraint>();
>   for (RetValConstraintTy::iterator I = TrackedSymbols.begin(),
>      E = TrackedSymbols.end(); I != E; ++I) {
>     SymbolRef Sym = I->second;
>     const MemRegion* lockR = I->first;
>     bool IsSymDead = SymReaper.isDead(Sym);
>     const LockState* LState = State->get<LockMap>(lockR);
>     // Remove the dead symbol from the return value symbols map.
>     if (IsSymDead){
>       ConditionTruthVal retZero = CMgr.isNull(State, Sym);
> if(retZero.isConstrainedFalse()){
>         // Update LockMap
>         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".
>       }
>       State = State->remove<RetValConstraint>(lockR);
>     }
>   }
> }
>
> Thank you.
>
>
> Regards,
> Malhar
>
>
> ᐧ
>
> On Mon, Apr 17, 2017 at 8:34 PM, Devin Coughlin <dcoughlin at apple.com 
> <mailto:dcoughlin at apple.com>> wrote:
>
>
>>     On Apr 17, 2017, at 4:55 AM, Malhar Thakkar <cs13b1031 at iith.ac.in
>>     <mailto:cs13b1031 at iith.ac.in>> wrote:
>>
>>     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<RetValConstraint>();
>>       // 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<RetValConstraint>(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.
>
>     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.
>     <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands
>     <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands>>.
>     I find the debug.ViewExplodedGraph checker particularly helpful.
>
>>     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?
>
>     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.
>
>     Devin
>
>