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

[Malhar Thakkar via cfe-dev]

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> wrote:

>
> On Apr 17, 2017, at 4:55 AM, Malhar Thakkar <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>. 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20170418/38b3bcbc/attachment.html>