Re: Suggested starter bug on clang analyzer codebase

classic Classic list List threaded Threaded
20 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev
Dear Dr. Devin,

Thank you for your response. 
Just to be clear, I think I'll have to query what is known about the symbol in PthreadLockChecker::ReleaseLock() instead of PthreadLockChecker::AcquireLock() as pthread_mutex_destroy() returns a non-zero value when a mutex is locked by another thread. 
So, in order to destroy that mutex, one would first need to unlock it and then destroy it.

The code snippet which produces a false positive in the current checker:

if(pthread_mutex_destroy(&(o->lock_mutex))!=0) {
   pthread_mutex_unlock(&(o->lock_mutex)); // It raises a warning here.
   pthread_mutex_destroy(&(o->lock_mutex));
}


Thank you.


Regards,
Malhar

On Wed, Apr 12, 2017 at 11:13 PM, Devin Coughlin <[hidden email]> wrote:

On Apr 12, 2017, at 3:32 AM, Malhar Thakkar <[hidden email]> wrote:

Hello Dr. Devin,

I have the following approach in mind.
Just like the Unix API stream checker (where the return value of fopen is checked), we can use the constraint manager to check if the return value of any function (for example: pthread_mutex_destroy) is zero or not.
If it is non-zero (which indicates failure), then we don't update the set & map which are used to keep track of the states all mutex variables.

Let me know your thoughts on this.

Malhar,

These sounds like the right approach to me, although I would focus only on pthread_mutex_destroy()’s return value for now.

One thing that makes this slightly tricky is that at the point of the return from the call to pthread_mutex_destroy() we don’t know anything about the return value — it is only later, when the programmer checks that value (in a if statement, for example) that the analyzer can discover whether the value returned was zero or not.

Here is an example:
    pthread_mutex_t m;
    pthread_mutex_init(&m, NULL);
    
    // … 

    int result = pthread_mutex_destroy(&m);
    // (1) At this point the analyzer doesn’t know value of result.
    // It tracks it as a symbol with no constraints

    if (result != 0) { // (2) At this point the analyzer constrains the symbol from (1) to be non-zero

// (3) At this point the checker should look at the at the symbol.
// If it is unknown or is definitely zero (meaning the destroy succeeded)
// it should emit a diagnostic. But if it is definitely non-zero then
// the analyzer should not report the diagnostic.
       pthread_mutex_lock(&m); 
    }

What this means is that you’ll need to modify PthreadLockChecker::DestroyLock() to keep track of the returned symbol from pthread_mutex_destroy() in the LockState and then query what is known about that symbol in PthreadLockChecker::AcquireLock().

Please don’t hesitate to ask if you more questions!

Devin

P.S. In the future you should CC the cfe-dev mailing on these kinds of questions so that the community can offer their own input and get a sense of what you are working on!




Thank you.


Regards,
Malhar

On Fri, Apr 7, 2017 at 2:26 AM, Devin Coughlin <[hidden email]> wrote:
Hi Malhar (+Michael, cc’d),

Here is a suggested starter bug on the clang static analyzer code base:

“False Positive PthreadLockChecker Use destroyed lock” <https://bugs.llvm.org/show_bug.cgi?id=32455>

The analyzer has a checker (PthreadLockChecker.cpp) that emits a diagnostic when the programmer tries to acquire a mutex twice or lock a mutex that has already been destroyed. Unfortunately, it has a false positive: if the programmer calls pthread_destroy_lock() and that call fails (returns a non-zero value) and then later tries to lock then the analyzer incorrectly warns that the mutex has been destroyed. There is an example of the false positive in the linked bugzilla URL above.

Fixing this false positive is a good starter bug to get you familiar with the checker side of the analyzer. If you haven’t seen it already, a good place to start would be the Checker Development Manual <https://clang-analyzer.llvm.org/checker_dev_manual.html>.

And please don’t hesitate to email if you have any questions or want to discuss approaches to fixing the bug!

Devin





_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev

On Apr 12, 2017, at 10:47 PM, Malhar Thakkar <[hidden email]> wrote:

Dear Dr. Devin,

Thank you for your response. 
Just to be clear, I think I'll have to query what is known about the symbol in PthreadLockChecker::ReleaseLock() instead of PthreadLockChecker::AcquireLock() as pthread_mutex_destroy() returns a non-zero value when a mutex is locked by another thread. 
So, in order to destroy that mutex, one would first need to unlock it and then destroy it. 

In general, unlocking a mutex that is held by another thread is undefined behavior, so the snippet below is not safe. It would be great to improve the diagnostic emitted for the snippet below explaining why it is not safe — but for now let’s focus on fixing the false positive I mentioned before.

The code snippet which produces a false positive in the current checker:

if(pthread_mutex_destroy(&(o->lock_mutex))!=0) {
   pthread_mutex_unlock(&(o->lock_mutex)); // It raises a warning here.
   pthread_mutex_destroy(&(o->lock_mutex));
}

Another example (in addition to the one I gave before) that it would be good to treat as safe is similar to what you have above, but without the unlock:

if (pthread_mutex_destroy(&m) != 0) {
pthread_mutex_destroy(&m); // Should not warn here
}

The fix for that would be exactly analogous to what I outlined before but you would query that symbol that is the result of the previous call to pthread_mutex_destroy() when deciding whether to diagnose on the second call to pthread_mutex_destroy()

Devin



Thank you.


Regards,
Malhar

On Wed, Apr 12, 2017 at 11:13 PM, Devin Coughlin <[hidden email]> wrote:

On Apr 12, 2017, at 3:32 AM, Malhar Thakkar <[hidden email]> wrote:

Hello Dr. Devin,

I have the following approach in mind.
Just like the Unix API stream checker (where the return value of fopen is checked), we can use the constraint manager to check if the return value of any function (for example: pthread_mutex_destroy) is zero or not.
If it is non-zero (which indicates failure), then we don't update the set & map which are used to keep track of the states all mutex variables.

Let me know your thoughts on this.

Malhar,

These sounds like the right approach to me, although I would focus only on pthread_mutex_destroy()’s return value for now.

One thing that makes this slightly tricky is that at the point of the return from the call to pthread_mutex_destroy() we don’t know anything about the return value — it is only later, when the programmer checks that value (in a if statement, for example) that the analyzer can discover whether the value returned was zero or not.

Here is an example:
    pthread_mutex_t m;
    pthread_mutex_init(&m, NULL);
    
    // … 

    int result = pthread_mutex_destroy(&m);
    // (1) At this point the analyzer doesn’t know value of result.
    // It tracks it as a symbol with no constraints

    if (result != 0) { // (2) At this point the analyzer constrains the symbol from (1) to be non-zero

// (3) At this point the checker should look at the at the symbol.
// If it is unknown or is definitely zero (meaning the destroy succeeded)
// it should emit a diagnostic. But if it is definitely non-zero then
// the analyzer should not report the diagnostic.
       pthread_mutex_lock(&m); 
    }

What this means is that you’ll need to modify PthreadLockChecker::DestroyLock() to keep track of the returned symbol from pthread_mutex_destroy() in the LockState and then query what is known about that symbol in PthreadLockChecker::AcquireLock().

Please don’t hesitate to ask if you more questions!

Devin

P.S. In the future you should CC the cfe-dev mailing on these kinds of questions so that the community can offer their own input and get a sense of what you are working on!




Thank you.


Regards,
Malhar

On Fri, Apr 7, 2017 at 2:26 AM, Devin Coughlin <[hidden email]> wrote:
Hi Malhar (+Michael, cc’d),

Here is a suggested starter bug on the clang static analyzer code base:

“False Positive PthreadLockChecker Use destroyed lock” <https://bugs.llvm.org/show_bug.cgi?id=32455>

The analyzer has a checker (PthreadLockChecker.cpp) that emits a diagnostic when the programmer tries to acquire a mutex twice or lock a mutex that has already been destroyed. Unfortunately, it has a false positive: if the programmer calls pthread_destroy_lock() and that call fails (returns a non-zero value) and then later tries to lock then the analyzer incorrectly warns that the mutex has been destroyed. There is an example of the false positive in the linked bugzilla URL above.

Fixing this false positive is a good starter bug to get you familiar with the checker side of the analyzer. If you haven’t seen it already, a good place to start would be the Checker Development Manual <https://clang-analyzer.llvm.org/checker_dev_manual.html>.

And please don’t hesitate to email if you have any questions or want to discuss approaches to fixing the bug!

Devin






_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev
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.

Regards,
Malhar

On Thu, Apr 13, 2017 at 11:48 AM, Devin Coughlin <[hidden email]> wrote:

On Apr 12, 2017, at 10:47 PM, Malhar Thakkar <[hidden email]> wrote:

Dear Dr. Devin,

Thank you for your response. 
Just to be clear, I think I'll have to query what is known about the symbol in PthreadLockChecker::ReleaseLock() instead of PthreadLockChecker::AcquireLock() as pthread_mutex_destroy() returns a non-zero value when a mutex is locked by another thread. 
So, in order to destroy that mutex, one would first need to unlock it and then destroy it. 

In general, unlocking a mutex that is held by another thread is undefined behavior, so the snippet below is not safe. It would be great to improve the diagnostic emitted for the snippet below explaining why it is not safe — but for now let’s focus on fixing the false positive I mentioned before.

The code snippet which produces a false positive in the current checker:

if(pthread_mutex_destroy(&(o->lock_mutex))!=0) {
   pthread_mutex_unlock(&(o->lock_mutex)); // It raises a warning here.
   pthread_mutex_destroy(&(o->lock_mutex));
}

Another example (in addition to the one I gave before) that it would be good to treat as safe is similar to what you have above, but without the unlock:

if (pthread_mutex_destroy(&m) != 0) {
pthread_mutex_destroy(&m); // Should not warn here
}

The fix for that would be exactly analogous to what I outlined before but you would query that symbol that is the result of the previous call to pthread_mutex_destroy() when deciding whether to diagnose on the second call to pthread_mutex_destroy()

Devin



Thank you.


Regards,
Malhar

On Wed, Apr 12, 2017 at 11:13 PM, Devin Coughlin <[hidden email]> wrote:

On Apr 12, 2017, at 3:32 AM, Malhar Thakkar <[hidden email]> wrote:

Hello Dr. Devin,

I have the following approach in mind.
Just like the Unix API stream checker (where the return value of fopen is checked), we can use the constraint manager to check if the return value of any function (for example: pthread_mutex_destroy) is zero or not.
If it is non-zero (which indicates failure), then we don't update the set & map which are used to keep track of the states all mutex variables.

Let me know your thoughts on this.

Malhar,

These sounds like the right approach to me, although I would focus only on pthread_mutex_destroy()’s return value for now.

One thing that makes this slightly tricky is that at the point of the return from the call to pthread_mutex_destroy() we don’t know anything about the return value — it is only later, when the programmer checks that value (in a if statement, for example) that the analyzer can discover whether the value returned was zero or not.

Here is an example:
    pthread_mutex_t m;
    pthread_mutex_init(&m, NULL);
    
    // … 

    int result = pthread_mutex_destroy(&m);
    // (1) At this point the analyzer doesn’t know value of result.
    // It tracks it as a symbol with no constraints

    if (result != 0) { // (2) At this point the analyzer constrains the symbol from (1) to be non-zero

// (3) At this point the checker should look at the at the symbol.
// If it is unknown or is definitely zero (meaning the destroy succeeded)
// it should emit a diagnostic. But if it is definitely non-zero then
// the analyzer should not report the diagnostic.
       pthread_mutex_lock(&m); 
    }

What this means is that you’ll need to modify PthreadLockChecker::DestroyLock() to keep track of the returned symbol from pthread_mutex_destroy() in the LockState and then query what is known about that symbol in PthreadLockChecker::AcquireLock().

Please don’t hesitate to ask if you more questions!

Devin

P.S. In the future you should CC the cfe-dev mailing on these kinds of questions so that the community can offer their own input and get a sense of what you are working on!




Thank you.


Regards,
Malhar

On Fri, Apr 7, 2017 at 2:26 AM, Devin Coughlin <[hidden email]> wrote:
Hi Malhar (+Michael, cc’d),

Here is a suggested starter bug on the clang static analyzer code base:

“False Positive PthreadLockChecker Use destroyed lock” <https://bugs.llvm.org/show_bug.cgi?id=32455>

The analyzer has a checker (PthreadLockChecker.cpp) that emits a diagnostic when the programmer tries to acquire a mutex twice or lock a mutex that has already been destroyed. Unfortunately, it has a false positive: if the programmer calls pthread_destroy_lock() and that call fails (returns a non-zero value) and then later tries to lock then the analyzer incorrectly warns that the mutex has been destroyed. There is an example of the false positive in the linked bugzilla URL above.

Fixing this false positive is a good starter bug to get you familiar with the checker side of the analyzer. If you haven’t seen it already, a good place to start would be the Checker Development Manual <https://clang-analyzer.llvm.org/checker_dev_manual.html>.

And please don’t hesitate to email if you have any questions or want to discuss approaches to fixing the bug!

Devin







_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev

On Apr 15, 2017, at 3:52 AM, Malhar Thakkar <[hidden email]> 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


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev
The other part of the "check if the return value was checked" is the
escape problem. For example, if we have:

   int result = pthread_mutex_destroy(&m);
   if (is_bad_result(result)) {
     pthread_mutex_lock(&m);
   }

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)

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.


On 4/15/17 7:14 PM, Devin Coughlin via cfe-dev wrote:

>
>> On Apr 15, 2017, at 3:52 AM, Malhar Thakkar <[hidden email]
>> <mailto:[hidden email]>> 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
>
>
>
> _______________________________________________
> cfe-dev mailing list
> [hidden email]
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev

> On Apr 15, 2017, at 10:15 AM, Artem Dergachev <[hidden email]> wrote:
>
> The other part of the "check if the return value was checked" is the escape problem. For example, if we have:
>
>  int result = pthread_mutex_destroy(&m);
>  if (is_bad_result(result)) {
>    pthread_mutex_lock(&m);
>  }
>
> 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)
>
> 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.

Artem makes a very good point — but I would suggest not tackling adding this new callback as part of the starter bug.

Devin



>
>
> On 4/15/17 7:14 PM, Devin Coughlin via cfe-dev wrote:
>>
>>> On Apr 15, 2017, at 3:52 AM, Malhar Thakkar <[hidden email] <mailto:[hidden email]>> 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
>>
>>
>>
>> _______________________________________________
>> cfe-dev mailing list
>> [hidden email]
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev


On 4/15/17 8:21 PM, Devin Coughlin wrote:

>> On Apr 15, 2017, at 10:15 AM, Artem Dergachev <[hidden email]> wrote:
>>
>> The other part of the "check if the return value was checked" is the escape problem. For example, if we have:
>>
>>   int result = pthread_mutex_destroy(&m);
>>   if (is_bad_result(result)) {
>>     pthread_mutex_lock(&m);
>>   }
>>
>> 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)
>>
>> 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.
> Artem makes a very good point — but I would suggest not tackling adding this new callback as part of the starter bug.
>
> Devin

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.

>>
>> On 4/15/17 7:14 PM, Devin Coughlin via cfe-dev wrote:
>>>> On Apr 15, 2017, at 3:52 AM, Malhar Thakkar <[hidden email] <mailto:[hidden email]>> 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
>>>
>>>
>>>
>>> _______________________________________________
>>> cfe-dev mailing list
>>> [hidden email]
>>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev
In reply to this post by Robinson, Paul via cfe-dev


On 4/15/17 8:21 PM, Devin Coughlin wrote:

>> On Apr 15, 2017, at 10:15 AM, Artem Dergachev <[hidden email]> wrote:
>>
>> The other part of the "check if the return value was checked" is the escape problem. For example, if we have:
>>
>>   int result = pthread_mutex_destroy(&m);
>>   if (is_bad_result(result)) {
>>     pthread_mutex_lock(&m);
>>   }
>>
>> 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)
>>
>> 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.
> Artem makes a very good point — but I would suggest not tackling adding this new callback as part of the starter bug.
>
> Devin

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.

>
>
>
>>
>> On 4/15/17 7:14 PM, Devin Coughlin via cfe-dev wrote:
>>>> On Apr 15, 2017, at 3:52 AM, Malhar Thakkar <[hidden email] <mailto:[hidden email]>> 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
>>>
>>>
>>>
>>> _______________________________________________
>>> cfe-dev mailing list
>>> [hidden email]
>>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev
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.

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

On Sat, Apr 15, 2017 at 11:34 PM, Artem Dergachev <[hidden email]> wrote:


On 4/15/17 8:21 PM, Devin Coughlin wrote:
On Apr 15, 2017, at 10:15 AM, Artem Dergachev <[hidden email]> wrote:

The other part of the "check if the return value was checked" is the escape problem. For example, if we have:

  int result = pthread_mutex_destroy(&m);
  if (is_bad_result(result)) {
    pthread_mutex_lock(&m);
  }

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)

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.
Artem makes a very good point — but I would suggest not tackling adding this new callback as part of the starter bug.

Devin

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.




On 4/15/17 7:14 PM, Devin Coughlin via cfe-dev wrote:
On Apr 15, 2017, at 3:52 AM, Malhar Thakkar <[hidden email] <mailto:[hidden email]>> 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



_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev



_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev

On Apr 17, 2017, at 4:55 AM, Malhar Thakkar <[hidden email]> 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
_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul 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 <[hidden email]> wrote:

On Apr 17, 2017, at 4:55 AM, Malhar Thakkar <[hidden email]> 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


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul 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 <[hidden email]
> <mailto:[hidden email]>> wrote:
>
>
>>     On Apr 17, 2017, at 4:55 AM, Malhar Thakkar <[hidden email]
>>     <mailto:[hidden email]>> 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
>
>

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev
Dear Dr. Artem,

Thank you for your response. After incorporating 'addTransition', I was able to suppress the double-destroy. But, when 'pthread_mutex_destroy' was called for the second time (i.e., inside the if branch), LockState was found to be NULL (which it should be according to my code) but ideally it should be in the Unlocked state. For, it to be in Unlocked state, I think state->set<LockMap>() should be executed inside checkDeadSymbols() instead of executing it inside AcquireLock(), ReleaseLock(), DestroyLock() and InitLock() as I am unable to find a way to do it otherwise.

Regards,
Malhar

On Tue, Apr 18, 2017 at 8:30 PM, Artem Dergachev <[hidden email]> wrote:
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 <[hidden email] <mailto:[hidden email]>> wrote:


    On Apr 17, 2017, at 4:55 AM, Malhar Thakkar <[hidden email]
    <mailto:[hidden email]>> 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





_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev
Yep!

You are right that simply unlocking the failed-to-be-destroyed mutex in
checkDeadSymbols is not enough. The reason for that is, the moment when
the symbol dies is quite unpredictable, and we don't know how many
things have happened to the mutex between the failed destroy and the
symbol death - it might have been locked and unlocked many times in between.

I'd propose that in order to maintain the correct mutex state you'd need
to check the destruction-return-value symbol in every operation as well.
For instance, when somebody tries to lock a mutex, see if it was
destroyed previously. If it was destroyed, look at the symbol:
* If the destruction was checked and failed on that execution path (as
you can find out by looking at the symbol's constraints in the program
state), then it's ok, remove that symbol from the program state and mark
the mutex as locked.
* If the destruction cannot be proven to have failed on this path, then
either it is known to have succeeded, or destruction wasn't checked for
failure properly on this path. It means we have a use-after-destroy, and
we report the warning accordingly.

At the same time, checkDeadSymbols is still necessary: if no mutex state
changes happen after destroy before symbol death, we need to collect the
information from the dying symbol. Because the symbol is dying, this
information will no longer ever be made more accurate (that is,
constraints wouldn't ever become more strict anymore), so it's as
accurate as possible. So we can be sure if the symbol should be truly
set to destroyed or reverted to the previous state.

Most path-sensitive checkers are kind of state machines (see also
"typestate"). They assign a state to an object, and then various events
(coming from checker callbacks) affect this state in one way or another.
You can draw the state diagram.

So my proposal is to have the following states: Initialized, Locked,
Unlocked, SchrödingerInitialized, SchrödingerLocked,
SchrödingerUnlocked, Destroyed. Schrödinger states indicate that we're
having a Schrödinger mutex that is alive and destroyed at the same time
on different execution paths. The mutex becomes a Schrödinger mutex
after pthread_mutex_destroy() and remains there until the box is
opened^W^W^W^W either we try to conduct more operations on the mutex, or
the return-symbol of pthread_mutex_destroy() is dead. At such moments we
collapse the mutex state to either the previous state (eg.
SchrödingerLocked -> Locked)  or to Destroyed. The easiest way to
represent Schrödinger states would be something like "still Locked, but
with destroy-return-symbol set present for this mutex"; upon collapse we
remove the return symbol.

On 4/19/17 8:54 AM, Malhar Thakkar wrote:

> Dear Dr. Artem,
>
> Thank you for your response. After incorporating 'addTransition', I
> was able to suppress the double-destroy. But, when
> 'pthread_mutex_destroy' was called for the second time (i.e., inside
> the if branch), LockState was found to be NULL (which it should be
> according to my code) but ideally it should be in the Unlocked state.
> For, it to be in Unlocked state, I think state->set<LockMap>() should
> be executed inside checkDeadSymbols() instead of executing it inside
> AcquireLock(), ReleaseLock(), DestroyLock() and InitLock() as I am
> unable to find a way to do it otherwise.
>
> Regards,
> Malhar
> ᐧ
>
> On Tue, Apr 18, 2017 at 8:30 PM, Artem Dergachev <[hidden email]
> <mailto:[hidden email]>> wrote:
>
>     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
>         <[hidden email] <mailto:[hidden email]>
>         <mailto:[hidden email] <mailto:[hidden email]>>> wrote:
>
>
>                 On Apr 17, 2017, at 4:55 AM, Malhar Thakkar
>             <[hidden email] <mailto:[hidden email]>
>                 <mailto:[hidden email]
>             <mailto:[hidden email]>>> 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>
>            
>         <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
>
>
>
>

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev
For completeness, i'd point out that there's a simpler alternative
approach to this: force the analyzer to split the state immediately on
pthread_mutex_destroy(): construct a state where the mutex is destroyed
and symbol is known-to-be-zero, construct a state where the mutex
remains the same and symbol is known-to-be-non-zero, and addTransition
to both of them. This forces the analyzer to investigate two concrete
states in parallel, rather than one "Schrödinger" state that would still
be split when the return value is checked.

However, that approach pays a huge price of doubling analysis time - the
time we would spend in the "Schrödinger" state in the original approach
would be doubled here (and if the return value is truly unchecked, that
may go on until the end of the analysis, because even after the symbol
dies the mutex state is still different, so the paths wouldn't be
merged). This is why we try to avoid state splits unless it is
definitely necessary.

On 4/19/17 9:22 AM, Artem Dergachev wrote:

> Yep!
>
> You are right that simply unlocking the failed-to-be-destroyed mutex
> in checkDeadSymbols is not enough. The reason for that is, the moment
> when the symbol dies is quite unpredictable, and we don't know how
> many things have happened to the mutex between the failed destroy and
> the symbol death - it might have been locked and unlocked many times
> in between.
>
> I'd propose that in order to maintain the correct mutex state you'd
> need to check the destruction-return-value symbol in every operation
> as well. For instance, when somebody tries to lock a mutex, see if it
> was destroyed previously. If it was destroyed, look at the symbol:
> * If the destruction was checked and failed on that execution path (as
> you can find out by looking at the symbol's constraints in the program
> state), then it's ok, remove that symbol from the program state and
> mark the mutex as locked.
> * If the destruction cannot be proven to have failed on this path,
> then either it is known to have succeeded, or destruction wasn't
> checked for failure properly on this path. It means we have a
> use-after-destroy, and we report the warning accordingly.
>
> At the same time, checkDeadSymbols is still necessary: if no mutex
> state changes happen after destroy before symbol death, we need to
> collect the information from the dying symbol. Because the symbol is
> dying, this information will no longer ever be made more accurate
> (that is, constraints wouldn't ever become more strict anymore), so
> it's as accurate as possible. So we can be sure if the symbol should
> be truly set to destroyed or reverted to the previous state.
>
> Most path-sensitive checkers are kind of state machines (see also
> "typestate"). They assign a state to an object, and then various
> events (coming from checker callbacks) affect this state in one way or
> another. You can draw the state diagram.
>
> So my proposal is to have the following states: Initialized, Locked,
> Unlocked, SchrödingerInitialized, SchrödingerLocked,
> SchrödingerUnlocked, Destroyed. Schrödinger states indicate that we're
> having a Schrödinger mutex that is alive and destroyed at the same
> time on different execution paths. The mutex becomes a Schrödinger
> mutex after pthread_mutex_destroy() and remains there until the box is
> opened^W^W^W^W either we try to conduct more operations on the mutex,
> or the return-symbol of pthread_mutex_destroy() is dead. At such
> moments we collapse the mutex state to either the previous state (eg.
> SchrödingerLocked -> Locked)  or to Destroyed. The easiest way to
> represent Schrödinger states would be something like "still Locked,
> but with destroy-return-symbol set present for this mutex"; upon
> collapse we remove the return symbol.
>
> On 4/19/17 8:54 AM, Malhar Thakkar wrote:
>> Dear Dr. Artem,
>>
>> Thank you for your response. After incorporating 'addTransition', I
>> was able to suppress the double-destroy. But, when
>> 'pthread_mutex_destroy' was called for the second time (i.e., inside
>> the if branch), LockState was found to be NULL (which it should be
>> according to my code) but ideally it should be in the Unlocked state.
>> For, it to be in Unlocked state, I think state->set<LockMap>() should
>> be executed inside checkDeadSymbols() instead of executing it inside
>> AcquireLock(), ReleaseLock(), DestroyLock() and InitLock() as I am
>> unable to find a way to do it otherwise.
>>
>> Regards,
>> Malhar
>> ᐧ
>>
>> On Tue, Apr 18, 2017 at 8:30 PM, Artem Dergachev <[hidden email]
>> <mailto:[hidden email]>> wrote:
>>
>>     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
>>         <[hidden email] <mailto:[hidden email]>
>>         <mailto:[hidden email] <mailto:[hidden email]>>>
>> wrote:
>>
>>
>>                 On Apr 17, 2017, at 4:55 AM, Malhar Thakkar
>>             <[hidden email] <mailto:[hidden email]>
>>                 <mailto:[hidden email]
>>             <mailto:[hidden email]>>> 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>
>> <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
>>
>>
>>
>>
>

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev
Dear Dr. Artem,

I have the following queries.
  • Will I ever require SchrodingerLocked? (As you mentioned, a mutex becomes a Schrodinger only when pthread_mutex_destroy() is called. Now, calling pthread_mutex_destroy() after pthread_mutex_lock() is anyway wrong. So, a warning should be raised in this case.)
  • SVal corresponding to lck_mtx_destroy() is Unknown or Undefined. Hence, I am not able to obtain a symbol for the return value of lck_mtx_destroy() which is leading to incorrect output on the testcase pthreadlock.c.
I'm also attaching the modified code.
I want you to check certain parts of the code. (I have added capitalized comments just before the parts which I want you to check.)

Thank you.


Regards,
Malhar

On Wed, Apr 19, 2017 at 12:11 PM, Artem Dergachev <[hidden email]> wrote:
For completeness, i'd point out that there's a simpler alternative approach to this: force the analyzer to split the state immediately on pthread_mutex_destroy(): construct a state where the mutex is destroyed and symbol is known-to-be-zero, construct a state where the mutex remains the same and symbol is known-to-be-non-zero, and addTransition to both of them. This forces the analyzer to investigate two concrete states in parallel, rather than one "Schrödinger" state that would still be split when the return value is checked.

However, that approach pays a huge price of doubling analysis time - the time we would spend in the "Schrödinger" state in the original approach would be doubled here (and if the return value is truly unchecked, that may go on until the end of the analysis, because even after the symbol dies the mutex state is still different, so the paths wouldn't be merged). This is why we try to avoid state splits unless it is definitely necessary.


On 4/19/17 9:22 AM, Artem Dergachev wrote:
Yep!

You are right that simply unlocking the failed-to-be-destroyed mutex in checkDeadSymbols is not enough. The reason for that is, the moment when the symbol dies is quite unpredictable, and we don't know how many things have happened to the mutex between the failed destroy and the symbol death - it might have been locked and unlocked many times in between.

I'd propose that in order to maintain the correct mutex state you'd need to check the destruction-return-value symbol in every operation as well. For instance, when somebody tries to lock a mutex, see if it was destroyed previously. If it was destroyed, look at the symbol:
* If the destruction was checked and failed on that execution path (as you can find out by looking at the symbol's constraints in the program state), then it's ok, remove that symbol from the program state and mark the mutex as locked.
* If the destruction cannot be proven to have failed on this path, then either it is known to have succeeded, or destruction wasn't checked for failure properly on this path. It means we have a use-after-destroy, and we report the warning accordingly.

At the same time, checkDeadSymbols is still necessary: if no mutex state changes happen after destroy before symbol death, we need to collect the information from the dying symbol. Because the symbol is dying, this information will no longer ever be made more accurate (that is, constraints wouldn't ever become more strict anymore), so it's as accurate as possible. So we can be sure if the symbol should be truly set to destroyed or reverted to the previous state.

Most path-sensitive checkers are kind of state machines (see also "typestate"). They assign a state to an object, and then various events (coming from checker callbacks) affect this state in one way or another. You can draw the state diagram.

So my proposal is to have the following states: Initialized, Locked, Unlocked, SchrödingerInitialized, SchrödingerLocked, SchrödingerUnlocked, Destroyed. Schrödinger states indicate that we're having a Schrödinger mutex that is alive and destroyed at the same time on different execution paths. The mutex becomes a Schrödinger mutex after pthread_mutex_destroy() and remains there until the box is opened^W^W^W^W either we try to conduct more operations on the mutex, or the return-symbol of pthread_mutex_destroy() is dead. At such moments we collapse the mutex state to either the previous state (eg. SchrödingerLocked -> Locked)  or to Destroyed. The easiest way to represent Schrödinger states would be something like "still Locked, but with destroy-return-symbol set present for this mutex"; upon collapse we remove the return symbol.

On 4/19/17 8:54 AM, Malhar Thakkar wrote:
Dear Dr. Artem,

Thank you for your response. After incorporating 'addTransition', I was able to suppress the double-destroy. But, when 'pthread_mutex_destroy' was called for the second time (i.e., inside the if branch), LockState was found to be NULL (which it should be according to my code) but ideally it should be in the Unlocked state. For, it to be in Unlocked state, I think state->set<LockMap>() should be executed inside checkDeadSymbols() instead of executing it inside AcquireLock(), ReleaseLock(), DestroyLock() and InitLock() as I am unable to find a way to do it otherwise.

Regards,
Malhar


On Tue, Apr 18, 2017 at 8:30 PM, Artem Dergachev <[hidden email] <mailto:[hidden email]>> wrote:

    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
        <[hidden email] <mailto:[hidden email]>
        <mailto:[hidden email] <mailto:[hidden email]>>> wrote:


                On Apr 17, 2017, at 4:55 AM, Malhar Thakkar
            <[hidden email] <mailto:[hidden email]>
                <mailto:[hidden email]
            <mailto:[hidden email]>>> 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>
<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








_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

PthreadLockChecker.cpp (21K) Download Attachment
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev
Yep, you're right, no need for SchrodingerLocked!

(we'd need to come up with better names, because "Shrodinger mutex" is
something i just came up with for explaining... Eg.,
UnlockedAndPossiblyDestroyed. Or just remove the new verbose enum values
for the new states and look at if the symbol is present in the
DestroyRetVal map instead). Note that when you have a DestroyRetVal
symbol for a mutex, then the mutex  *definitely* has a state, which is
one of the "Shrodinger" states, and vice versa; you can replace quite a
lot of your "else" branches with *assertions*, because that's entirely
within your checker's area of expertise to keep it that way. You may
also probably try to de-duplicate some code into auxiliary functions.

lck_mtx_destroy() is void. It doesn't have a return value. Seems that
it's good as is :) You can vary behavior depending on the
LockingSemantics argument (if it's XNUSemantics, skip stuff).

I'd probably also have a closer look tomorrow.




On 4/20/17 5:51 PM, Malhar Thakkar wrote:

> Dear Dr. Artem,
>
> I have the following queries.
>
>   * Will I ever require SchrodingerLocked? (As you mentioned, a mutex
>     becomes a Schrodinger only when pthread_mutex_destroy() is called.
>     Now, calling pthread_mutex_destroy() after pthread_mutex_lock() is
>     anyway wrong. So, a warning should be raised in this case.)
>   * SVal corresponding to lck_mtx_destroy() is Unknown or Undefined.
>     Hence, I am not able to obtain a symbol for the return value of
>     lck_mtx_destroy() which is leading to incorrect output on the
>     testcase pthreadlock.c.
>
> I'm also attaching the modified code.
> I want you to check certain parts of the code. (I have added
> capitalized comments just before the parts which I want you to check.)
>
> Thank you.
>
>
> Regards,
> Malhar
> ᐧ
>
> On Wed, Apr 19, 2017 at 12:11 PM, Artem Dergachev <[hidden email]
> <mailto:[hidden email]>> wrote:
>
>     For completeness, i'd point out that there's a simpler alternative
>     approach to this: force the analyzer to split the state
>     immediately on pthread_mutex_destroy(): construct a state where
>     the mutex is destroyed and symbol is known-to-be-zero, construct a
>     state where the mutex remains the same and symbol is
>     known-to-be-non-zero, and addTransition to both of them. This
>     forces the analyzer to investigate two concrete states in
>     parallel, rather than one "Schrödinger" state that would still be
>     split when the return value is checked.
>
>     However, that approach pays a huge price of doubling analysis time
>     - the time we would spend in the "Schrödinger" state in the
>     original approach would be doubled here (and if the return value
>     is truly unchecked, that may go on until the end of the analysis,
>     because even after the symbol dies the mutex state is still
>     different, so the paths wouldn't be merged). This is why we try to
>     avoid state splits unless it is definitely necessary.
>
>
>     On 4/19/17 9:22 AM, Artem Dergachev wrote:
>
>         Yep!
>
>         You are right that simply unlocking the failed-to-be-destroyed
>         mutex in checkDeadSymbols is not enough. The reason for that
>         is, the moment when the symbol dies is quite unpredictable,
>         and we don't know how many things have happened to the mutex
>         between the failed destroy and the symbol death - it might
>         have been locked and unlocked many times in between.
>
>         I'd propose that in order to maintain the correct mutex state
>         you'd need to check the destruction-return-value symbol in
>         every operation as well. For instance, when somebody tries to
>         lock a mutex, see if it was destroyed previously. If it was
>         destroyed, look at the symbol:
>         * If the destruction was checked and failed on that execution
>         path (as you can find out by looking at the symbol's
>         constraints in the program state), then it's ok, remove that
>         symbol from the program state and mark the mutex as locked.
>         * If the destruction cannot be proven to have failed on this
>         path, then either it is known to have succeeded, or
>         destruction wasn't checked for failure properly on this path.
>         It means we have a use-after-destroy, and we report the
>         warning accordingly.
>
>         At the same time, checkDeadSymbols is still necessary: if no
>         mutex state changes happen after destroy before symbol death,
>         we need to collect the information from the dying symbol.
>         Because the symbol is dying, this information will no longer
>         ever be made more accurate (that is, constraints wouldn't ever
>         become more strict anymore), so it's as accurate as possible.
>         So we can be sure if the symbol should be truly set to
>         destroyed or reverted to the previous state.
>
>         Most path-sensitive checkers are kind of state machines (see
>         also "typestate"). They assign a state to an object, and then
>         various events (coming from checker callbacks) affect this
>         state in one way or another. You can draw the state diagram.
>
>         So my proposal is to have the following states: Initialized,
>         Locked, Unlocked, SchrödingerInitialized, SchrödingerLocked,
>         SchrödingerUnlocked, Destroyed. Schrödinger states indicate
>         that we're having a Schrödinger mutex that is alive and
>         destroyed at the same time on different execution paths. The
>         mutex becomes a Schrödinger mutex after
>         pthread_mutex_destroy() and remains there until the box is
>         opened^W^W^W^W either we try to conduct more operations on the
>         mutex, or the return-symbol of pthread_mutex_destroy() is
>         dead. At such moments we collapse the mutex state to either
>         the previous state (eg. SchrödingerLocked -> Locked)  or to
>         Destroyed. The easiest way to represent Schrödinger states
>         would be something like "still Locked, but with
>         destroy-return-symbol set present for this mutex"; upon
>         collapse we remove the return symbol.
>
>         On 4/19/17 8:54 AM, Malhar Thakkar wrote:
>
>             Dear Dr. Artem,
>
>             Thank you for your response. After incorporating
>             'addTransition', I was able to suppress the
>             double-destroy. But, when 'pthread_mutex_destroy' was
>             called for the second time (i.e., inside the if branch),
>             LockState was found to be NULL (which it should be
>             according to my code) but ideally it should be in the
>             Unlocked state. For, it to be in Unlocked state, I think
>             state->set<LockMap>() should be executed inside
>             checkDeadSymbols() instead of executing it inside
>             AcquireLock(), ReleaseLock(), DestroyLock() and InitLock()
>             as I am unable to find a way to do it otherwise.
>
>             Regards,
>             Malhar
>             ᐧ
>
>             On Tue, Apr 18, 2017 at 8:30 PM, Artem Dergachev
>             <[hidden email] <mailto:[hidden email]>
>             <mailto:[hidden email] <mailto:[hidden email]>>>
>             wrote:
>
>                 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
>                     <[hidden email] <mailto:[hidden email]>
>             <mailto:[hidden email] <mailto:[hidden email]>>
>                     <mailto:[hidden email]
>             <mailto:[hidden email]> <mailto:[hidden email]
>             <mailto:[hidden email]>>>> wrote:
>
>
>                             On Apr 17, 2017, at 4:55 AM, Malhar Thakkar
>                         <[hidden email]
>             <mailto:[hidden email]> <mailto:[hidden email]
>             <mailto:[hidden email]>>
>                             <mailto:[hidden email]
>             <mailto:[hidden email]>
>                         <mailto:[hidden email]
>             <mailto:[hidden email]>>>> 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>
>             <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands
>             <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands>>
>             <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands
>             <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands>
>             <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
>
>
>
>
>
>
>

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev
Malhar,

It would be great if you could upload your diff to our Phabricator at http://reviews.llvm.org — this is the online tool we use for code reviews. We can comment on specific code (rather than the overall approach) there.

There are instructions for using Phabricator at http://llvm.org/docs/Phabricator.html

Devin


On Apr 20, 2017, at 9:16 AM, Artem Dergachev <[hidden email]> wrote:

Yep, you're right, no need for SchrodingerLocked!

(we'd need to come up with better names, because "Shrodinger mutex" is something i just came up with for explaining... Eg., UnlockedAndPossiblyDestroyed. Or just remove the new verbose enum values for the new states and look at if the symbol is present in the DestroyRetVal map instead). Note that when you have a DestroyRetVal symbol for a mutex, then the mutex  *definitely* has a state, which is one of the "Shrodinger" states, and vice versa; you can replace quite a lot of your "else" branches with *assertions*, because that's entirely within your checker's area of expertise to keep it that way. You may also probably try to de-duplicate some code into auxiliary functions.

lck_mtx_destroy() is void. It doesn't have a return value. Seems that it's good as is :) You can vary behavior depending on the LockingSemantics argument (if it's XNUSemantics, skip stuff).

I'd probably also have a closer look tomorrow.




On 4/20/17 5:51 PM, Malhar Thakkar wrote:
Dear Dr. Artem,

I have the following queries.

 * Will I ever require SchrodingerLocked? (As you mentioned, a mutex
   becomes a Schrodinger only when pthread_mutex_destroy() is called.
   Now, calling pthread_mutex_destroy() after pthread_mutex_lock() is
   anyway wrong. So, a warning should be raised in this case.)
 * SVal corresponding to lck_mtx_destroy() is Unknown or Undefined.
   Hence, I am not able to obtain a symbol for the return value of
   lck_mtx_destroy() which is leading to incorrect output on the
   testcase pthreadlock.c.

I'm also attaching the modified code.
I want you to check certain parts of the code. (I have added capitalized comments just before the parts which I want you to check.)

Thank you.


Regards,
Malhar


On Wed, Apr 19, 2017 at 12:11 PM, Artem Dergachev <[hidden email] <[hidden email]>> wrote:

   For completeness, i'd point out that there's a simpler alternative
   approach to this: force the analyzer to split the state
   immediately on pthread_mutex_destroy(): construct a state where
   the mutex is destroyed and symbol is known-to-be-zero, construct a
   state where the mutex remains the same and symbol is
   known-to-be-non-zero, and addTransition to both of them. This
   forces the analyzer to investigate two concrete states in
   parallel, rather than one "Schrödinger" state that would still be
   split when the return value is checked.

   However, that approach pays a huge price of doubling analysis time
   - the time we would spend in the "Schrödinger" state in the
   original approach would be doubled here (and if the return value
   is truly unchecked, that may go on until the end of the analysis,
   because even after the symbol dies the mutex state is still
   different, so the paths wouldn't be merged). This is why we try to
   avoid state splits unless it is definitely necessary.


   On 4/19/17 9:22 AM, Artem Dergachev wrote:

       Yep!

       You are right that simply unlocking the failed-to-be-destroyed
       mutex in checkDeadSymbols is not enough. The reason for that
       is, the moment when the symbol dies is quite unpredictable,
       and we don't know how many things have happened to the mutex
       between the failed destroy and the symbol death - it might
       have been locked and unlocked many times in between.

       I'd propose that in order to maintain the correct mutex state
       you'd need to check the destruction-return-value symbol in
       every operation as well. For instance, when somebody tries to
       lock a mutex, see if it was destroyed previously. If it was
       destroyed, look at the symbol:
       * If the destruction was checked and failed on that execution
       path (as you can find out by looking at the symbol's
       constraints in the program state), then it's ok, remove that
       symbol from the program state and mark the mutex as locked.
       * If the destruction cannot be proven to have failed on this
       path, then either it is known to have succeeded, or
       destruction wasn't checked for failure properly on this path.
       It means we have a use-after-destroy, and we report the
       warning accordingly.

       At the same time, checkDeadSymbols is still necessary: if no
       mutex state changes happen after destroy before symbol death,
       we need to collect the information from the dying symbol.
       Because the symbol is dying, this information will no longer
       ever be made more accurate (that is, constraints wouldn't ever
       become more strict anymore), so it's as accurate as possible.
       So we can be sure if the symbol should be truly set to
       destroyed or reverted to the previous state.

       Most path-sensitive checkers are kind of state machines (see
       also "typestate"). They assign a state to an object, and then
       various events (coming from checker callbacks) affect this
       state in one way or another. You can draw the state diagram.

       So my proposal is to have the following states: Initialized,
       Locked, Unlocked, SchrödingerInitialized, SchrödingerLocked,
       SchrödingerUnlocked, Destroyed. Schrödinger states indicate
       that we're having a Schrödinger mutex that is alive and
       destroyed at the same time on different execution paths. The
       mutex becomes a Schrödinger mutex after
       pthread_mutex_destroy() and remains there until the box is
       opened^W^W^W^W either we try to conduct more operations on the
       mutex, or the return-symbol of pthread_mutex_destroy() is
       dead. At such moments we collapse the mutex state to either
       the previous state (eg. SchrödingerLocked -> Locked)  or to
       Destroyed. The easiest way to represent Schrödinger states
       would be something like "still Locked, but with
       destroy-return-symbol set present for this mutex"; upon
       collapse we remove the return symbol.

       On 4/19/17 8:54 AM, Malhar Thakkar wrote:

           Dear Dr. Artem,

           Thank you for your response. After incorporating
           'addTransition', I was able to suppress the
           double-destroy. But, when 'pthread_mutex_destroy' was
           called for the second time (i.e., inside the if branch),
           LockState was found to be NULL (which it should be
           according to my code) but ideally it should be in the
           Unlocked state. For, it to be in Unlocked state, I think
           state->set<LockMap>() should be executed inside
           checkDeadSymbols() instead of executing it inside
           AcquireLock(), ReleaseLock(), DestroyLock() and InitLock()
           as I am unable to find a way to do it otherwise.

           Regards,
           Malhar
           ᐧ

           On Tue, Apr 18, 2017 at 8:30 PM, Artem Dergachev
           <[hidden email] <[hidden email]>
           <[hidden email] <[hidden email]>>>
           wrote:

               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
                   <[hidden email] <[hidden email]>
           <[hidden email] <[hidden email]>>
                   <[hidden email]
           <[hidden email]> <[hidden email]
           <[hidden email]>>>> wrote:


                           On Apr 17, 2017, at 4:55 AM, Malhar Thakkar
                       <[hidden email]
           <[hidden email]> <[hidden email]
           <[hidden email]>>
                           <[hidden email]
           <[hidden email]>
                       <[hidden email]
           <[hidden email]>>>> 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>
           <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands
           <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands>>
           <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands
           <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands>
           <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


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev
As I wanted to start afresh, I downloaded LLVM and clang source from their mirror repositories from GitHub and built them yesterday. Then, I modified PthreadLockChecker.cpp and then performed make clang and make install in the build directory. It built without any errors.

Then, I went to build/bin and performed

./clang -cc1 -analyzer-checker=alpha.unix.PthreadLock -verify ../../llvm/tools/clang/test/Analysis/pthreadlock.c

I encountered an error saying, 'warning' diagnostics expected but not seen: 

Also, the llvm::errs() statement that I added in PthreadLockChecker.cpp is not getting displayed on the terminal.

What do you think the problem is?



Thank you.



Regards,

Malhar


On Thu, Apr 20, 2017 at 11:28 PM, Devin Coughlin <[hidden email]> wrote:
Malhar,

It would be great if you could upload your diff to our Phabricator at http://reviews.llvm.org — this is the online tool we use for code reviews. We can comment on specific code (rather than the overall approach) there.

There are instructions for using Phabricator at http://llvm.org/docs/Phabricator.html

Devin


On Apr 20, 2017, at 9:16 AM, Artem Dergachev <[hidden email]> wrote:

Yep, you're right, no need for SchrodingerLocked!

(we'd need to come up with better names, because "Shrodinger mutex" is something i just came up with for explaining... Eg., UnlockedAndPossiblyDestroyed. Or just remove the new verbose enum values for the new states and look at if the symbol is present in the DestroyRetVal map instead). Note that when you have a DestroyRetVal symbol for a mutex, then the mutex  *definitely* has a state, which is one of the "Shrodinger" states, and vice versa; you can replace quite a lot of your "else" branches with *assertions*, because that's entirely within your checker's area of expertise to keep it that way. You may also probably try to de-duplicate some code into auxiliary functions.

lck_mtx_destroy() is void. It doesn't have a return value. Seems that it's good as is :) You can vary behavior depending on the LockingSemantics argument (if it's XNUSemantics, skip stuff).

I'd probably also have a closer look tomorrow.




On 4/20/17 5:51 PM, Malhar Thakkar wrote:
Dear Dr. Artem,

I have the following queries.

 * Will I ever require SchrodingerLocked? (As you mentioned, a mutex
   becomes a Schrodinger only when pthread_mutex_destroy() is called.
   Now, calling pthread_mutex_destroy() after pthread_mutex_lock() is
   anyway wrong. So, a warning should be raised in this case.)
 * SVal corresponding to lck_mtx_destroy() is Unknown or Undefined.
   Hence, I am not able to obtain a symbol for the return value of
   lck_mtx_destroy() which is leading to incorrect output on the
   testcase pthreadlock.c.

I'm also attaching the modified code.
I want you to check certain parts of the code. (I have added capitalized comments just before the parts which I want you to check.)

Thank you.


Regards,
Malhar


On Wed, Apr 19, 2017 at 12:11 PM, Artem Dergachev <[hidden email] <[hidden email]>> wrote:

   For completeness, i'd point out that there's a simpler alternative
   approach to this: force the analyzer to split the state
   immediately on pthread_mutex_destroy(): construct a state where
   the mutex is destroyed and symbol is known-to-be-zero, construct a
   state where the mutex remains the same and symbol is
   known-to-be-non-zero, and addTransition to both of them. This
   forces the analyzer to investigate two concrete states in
   parallel, rather than one "Schrödinger" state that would still be
   split when the return value is checked.

   However, that approach pays a huge price of doubling analysis time
   - the time we would spend in the "Schrödinger" state in the
   original approach would be doubled here (and if the return value
   is truly unchecked, that may go on until the end of the analysis,
   because even after the symbol dies the mutex state is still
   different, so the paths wouldn't be merged). This is why we try to
   avoid state splits unless it is definitely necessary.


   On 4/19/17 9:22 AM, Artem Dergachev wrote:

       Yep!

       You are right that simply unlocking the failed-to-be-destroyed
       mutex in checkDeadSymbols is not enough. The reason for that
       is, the moment when the symbol dies is quite unpredictable,
       and we don't know how many things have happened to the mutex
       between the failed destroy and the symbol death - it might
       have been locked and unlocked many times in between.

       I'd propose that in order to maintain the correct mutex state
       you'd need to check the destruction-return-value symbol in
       every operation as well. For instance, when somebody tries to
       lock a mutex, see if it was destroyed previously. If it was
       destroyed, look at the symbol:
       * If the destruction was checked and failed on that execution
       path (as you can find out by looking at the symbol's
       constraints in the program state), then it's ok, remove that
       symbol from the program state and mark the mutex as locked.
       * If the destruction cannot be proven to have failed on this
       path, then either it is known to have succeeded, or
       destruction wasn't checked for failure properly on this path.
       It means we have a use-after-destroy, and we report the
       warning accordingly.

       At the same time, checkDeadSymbols is still necessary: if no
       mutex state changes happen after destroy before symbol death,
       we need to collect the information from the dying symbol.
       Because the symbol is dying, this information will no longer
       ever be made more accurate (that is, constraints wouldn't ever
       become more strict anymore), so it's as accurate as possible.
       So we can be sure if the symbol should be truly set to
       destroyed or reverted to the previous state.

       Most path-sensitive checkers are kind of state machines (see
       also "typestate"). They assign a state to an object, and then
       various events (coming from checker callbacks) affect this
       state in one way or another. You can draw the state diagram.

       So my proposal is to have the following states: Initialized,
       Locked, Unlocked, SchrödingerInitialized, SchrödingerLocked,
       SchrödingerUnlocked, Destroyed. Schrödinger states indicate
       that we're having a Schrödinger mutex that is alive and
       destroyed at the same time on different execution paths. The
       mutex becomes a Schrödinger mutex after
       pthread_mutex_destroy() and remains there until the box is
       opened^W^W^W^W either we try to conduct more operations on the
       mutex, or the return-symbol of pthread_mutex_destroy() is
       dead. At such moments we collapse the mutex state to either
       the previous state (eg. SchrödingerLocked -> Locked)  or to
       Destroyed. The easiest way to represent Schrödinger states
       would be something like "still Locked, but with
       destroy-return-symbol set present for this mutex"; upon
       collapse we remove the return symbol.

       On 4/19/17 8:54 AM, Malhar Thakkar wrote:

           Dear Dr. Artem,

           Thank you for your response. After incorporating
           'addTransition', I was able to suppress the
           double-destroy. But, when 'pthread_mutex_destroy' was
           called for the second time (i.e., inside the if branch),
           LockState was found to be NULL (which it should be
           according to my code) but ideally it should be in the
           Unlocked state. For, it to be in Unlocked state, I think
           state->set<LockMap>() should be executed inside
           checkDeadSymbols() instead of executing it inside
           AcquireLock(), ReleaseLock(), DestroyLock() and InitLock()
           as I am unable to find a way to do it otherwise.

           Regards,
           Malhar
           ᐧ

           On Tue, Apr 18, 2017 at 8:30 PM, Artem Dergachev
           <[hidden email] <[hidden email]>
           <[hidden email] <[hidden email]>>>
           wrote:

               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
                   <[hidden email] <[hidden email]>
           <[hidden email] <[hidden email]>>
                   <[hidden email]
           <[hidden email]> <[hidden email]
           <[hidden email]>>>> wrote:


                           On Apr 17, 2017, at 4:55 AM, Malhar Thakkar
                       <[hidden email]
           <[hidden email]> <[hidden email]
           <[hidden email]>>
                           <[hidden email]
           <[hidden email]>
                       <[hidden email]
           <[hidden email]>>>> 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>
           <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands
           <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands>>
           <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands
           <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands>
           <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



_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Suggested starter bug on clang analyzer codebase

Robinson, Paul via cfe-dev
Never mind. I was using the wrong command.

Now, I'm using the following command
./clang -cc1 -analyze -analyzer-checker=alpha.unix.PthreadLock ../../llvm/tools/clang/test/Analysis/pthreadlock.c

Added -analyze and removed -verify.
Now, it's working as expected.

Thank you.

Regards,
Malhar Thakkar

On Wed, May 17, 2017 at 4:35 PM, Malhar Thakkar <[hidden email]> wrote:
As I wanted to start afresh, I downloaded LLVM and clang source from their mirror repositories from GitHub and built them yesterday. Then, I modified PthreadLockChecker.cpp and then performed make clang and make install in the build directory. It built without any errors.

Then, I went to build/bin and performed

./clang -cc1 -analyzer-checker=alpha.unix.PthreadLock -verify ../../llvm/tools/clang/test/Analysis/pthreadlock.c

I encountered an error saying, 'warning' diagnostics expected but not seen: 

Also, the llvm::errs() statement that I added in PthreadLockChecker.cpp is not getting displayed on the terminal.

What do you think the problem is?



Thank you.



Regards,

Malhar


On Thu, Apr 20, 2017 at 11:28 PM, Devin Coughlin <[hidden email]> wrote:
Malhar,

It would be great if you could upload your diff to our Phabricator at http://reviews.llvm.org — this is the online tool we use for code reviews. We can comment on specific code (rather than the overall approach) there.

There are instructions for using Phabricator at http://llvm.org/docs/Phabricator.html

Devin


On Apr 20, 2017, at 9:16 AM, Artem Dergachev <[hidden email]> wrote:

Yep, you're right, no need for SchrodingerLocked!

(we'd need to come up with better names, because "Shrodinger mutex" is something i just came up with for explaining... Eg., UnlockedAndPossiblyDestroyed. Or just remove the new verbose enum values for the new states and look at if the symbol is present in the DestroyRetVal map instead). Note that when you have a DestroyRetVal symbol for a mutex, then the mutex  *definitely* has a state, which is one of the "Shrodinger" states, and vice versa; you can replace quite a lot of your "else" branches with *assertions*, because that's entirely within your checker's area of expertise to keep it that way. You may also probably try to de-duplicate some code into auxiliary functions.

lck_mtx_destroy() is void. It doesn't have a return value. Seems that it's good as is :) You can vary behavior depending on the LockingSemantics argument (if it's XNUSemantics, skip stuff).

I'd probably also have a closer look tomorrow.




On 4/20/17 5:51 PM, Malhar Thakkar wrote:
Dear Dr. Artem,

I have the following queries.

 * Will I ever require SchrodingerLocked? (As you mentioned, a mutex
   becomes a Schrodinger only when pthread_mutex_destroy() is called.
   Now, calling pthread_mutex_destroy() after pthread_mutex_lock() is
   anyway wrong. So, a warning should be raised in this case.)
 * SVal corresponding to lck_mtx_destroy() is Unknown or Undefined.
   Hence, I am not able to obtain a symbol for the return value of
   lck_mtx_destroy() which is leading to incorrect output on the
   testcase pthreadlock.c.

I'm also attaching the modified code.
I want you to check certain parts of the code. (I have added capitalized comments just before the parts which I want you to check.)

Thank you.


Regards,
Malhar


On Wed, Apr 19, 2017 at 12:11 PM, Artem Dergachev <[hidden email] <[hidden email]>> wrote:

   For completeness, i'd point out that there's a simpler alternative
   approach to this: force the analyzer to split the state
   immediately on pthread_mutex_destroy(): construct a state where
   the mutex is destroyed and symbol is known-to-be-zero, construct a
   state where the mutex remains the same and symbol is
   known-to-be-non-zero, and addTransition to both of them. This
   forces the analyzer to investigate two concrete states in
   parallel, rather than one "Schrödinger" state that would still be
   split when the return value is checked.

   However, that approach pays a huge price of doubling analysis time
   - the time we would spend in the "Schrödinger" state in the
   original approach would be doubled here (and if the return value
   is truly unchecked, that may go on until the end of the analysis,
   because even after the symbol dies the mutex state is still
   different, so the paths wouldn't be merged). This is why we try to
   avoid state splits unless it is definitely necessary.


   On 4/19/17 9:22 AM, Artem Dergachev wrote:

       Yep!

       You are right that simply unlocking the failed-to-be-destroyed
       mutex in checkDeadSymbols is not enough. The reason for that
       is, the moment when the symbol dies is quite unpredictable,
       and we don't know how many things have happened to the mutex
       between the failed destroy and the symbol death - it might
       have been locked and unlocked many times in between.

       I'd propose that in order to maintain the correct mutex state
       you'd need to check the destruction-return-value symbol in
       every operation as well. For instance, when somebody tries to
       lock a mutex, see if it was destroyed previously. If it was
       destroyed, look at the symbol:
       * If the destruction was checked and failed on that execution
       path (as you can find out by looking at the symbol's
       constraints in the program state), then it's ok, remove that
       symbol from the program state and mark the mutex as locked.
       * If the destruction cannot be proven to have failed on this
       path, then either it is known to have succeeded, or
       destruction wasn't checked for failure properly on this path.
       It means we have a use-after-destroy, and we report the
       warning accordingly.

       At the same time, checkDeadSymbols is still necessary: if no
       mutex state changes happen after destroy before symbol death,
       we need to collect the information from the dying symbol.
       Because the symbol is dying, this information will no longer
       ever be made more accurate (that is, constraints wouldn't ever
       become more strict anymore), so it's as accurate as possible.
       So we can be sure if the symbol should be truly set to
       destroyed or reverted to the previous state.

       Most path-sensitive checkers are kind of state machines (see
       also "typestate"). They assign a state to an object, and then
       various events (coming from checker callbacks) affect this
       state in one way or another. You can draw the state diagram.

       So my proposal is to have the following states: Initialized,
       Locked, Unlocked, SchrödingerInitialized, SchrödingerLocked,
       SchrödingerUnlocked, Destroyed. Schrödinger states indicate
       that we're having a Schrödinger mutex that is alive and
       destroyed at the same time on different execution paths. The
       mutex becomes a Schrödinger mutex after
       pthread_mutex_destroy() and remains there until the box is
       opened^W^W^W^W either we try to conduct more operations on the
       mutex, or the return-symbol of pthread_mutex_destroy() is
       dead. At such moments we collapse the mutex state to either
       the previous state (eg. SchrödingerLocked -> Locked)  or to
       Destroyed. The easiest way to represent Schrödinger states
       would be something like "still Locked, but with
       destroy-return-symbol set present for this mutex"; upon
       collapse we remove the return symbol.

       On 4/19/17 8:54 AM, Malhar Thakkar wrote:

           Dear Dr. Artem,

           Thank you for your response. After incorporating
           'addTransition', I was able to suppress the
           double-destroy. But, when 'pthread_mutex_destroy' was
           called for the second time (i.e., inside the if branch),
           LockState was found to be NULL (which it should be
           according to my code) but ideally it should be in the
           Unlocked state. For, it to be in Unlocked state, I think
           state->set<LockMap>() should be executed inside
           checkDeadSymbols() instead of executing it inside
           AcquireLock(), ReleaseLock(), DestroyLock() and InitLock()
           as I am unable to find a way to do it otherwise.

           Regards,
           Malhar
           ᐧ

           On Tue, Apr 18, 2017 at 8:30 PM, Artem Dergachev
           <[hidden email] <[hidden email]>
           <[hidden email] <[hidden email]>>>
           wrote:

               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
                   <[hidden email] <[hidden email]>
           <[hidden email] <[hidden email]>>
                   <[hidden email]
           <[hidden email]> <[hidden email]
           <[hidden email]>>>> wrote:


                           On Apr 17, 2017, at 4:55 AM, Malhar Thakkar
                       <[hidden email]
           <[hidden email]> <[hidden email]
           <[hidden email]>>
                           <[hidden email]
           <[hidden email]>
                       <[hidden email]
           <[hidden email]>>>> 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>
           <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands
           <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands>>
           <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands
           <https://clang-analyzer.llvm.org/checker_dev_manual.html#commands>
           <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




_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Loading...