[Cocci] Inter-procedural analysis.

[Cocci] Inter-procedural analysis.

[Cyril Roelandt]

Hello!

I was trying to find cases of double mutex unlocks in the Hurd, and 
wrote a very simple semantic patch:

@exists@
expression E;
@@
* pthread_mutex_unlock(E);
... when != pthread_mutex_lock(E)
* pthread_mutex_unlock(E);

This works as expected with this snippet of C code:

static void
foo(void)
{
	pthread_mutex_lock(&lock);
	do_stg();
	pthread_mutex_unlock(&lock);
	if (some_condition)
		pthread_mutex_unlock(&lock);
}

--- x.c
+++ /tmp/cocci-output-4955-ff7d08-x.c
@@ -3,7 +3,5 @@ foo(void)
  {
  	pthread_mutex_lock(&lock);
  	do_stg();
-	pthread_mutex_unlock(&lock);
  	if (some_condition)
-		pthread_mutex_unlock(&lock);
  }

But it will report a false positive with this code:

static void
lock_it(pthread_mutex_t *lock)
{
	pthread_mutex_lock(lock);
}

static void
foo(void)
{
	pthread_mutex_lock(&lock);
	do_stg();
	pthread_mutex_unlock(&lock);
	lock_it(&lock);
	pthread_mutex_unlock(&lock);
}

It is perfectly fine to call pthread_mutex_unlock the second time, since 
LOCK has been re-acquired by lock_it(). Is there any way to do 
inter-procedural analysis in a semantic patch ?

Cyril Roelandt.

[Cocci] Inter-procedural analysis.

[Julia Lawall]

On Sat, 22 Dec 2012, Cyril Roelandt wrote:

> Hello!
>
> I was trying to find cases of double mutex unlocks in the Hurd, and wrote a
> very simple semantic patch:
>
> @exists@
> expression E;
> @@
> * pthread_mutex_unlock(E);
> ... when != pthread_mutex_lock(E)
> * pthread_mutex_unlock(E);
>
> This works as expected with this snippet of C code:
>
> static void
> foo(void)
> {
> 	pthread_mutex_lock(&lock);
> 	do_stg();
> 	pthread_mutex_unlock(&lock);
> 	if (some_condition)
> 		pthread_mutex_unlock(&lock);
> }
>
> --- x.c
> +++ /tmp/cocci-output-4955-ff7d08-x.c
> @@ -3,7 +3,5 @@ foo(void)
>  {
>  	pthread_mutex_lock(&lock);
>  	do_stg();
> -	pthread_mutex_unlock(&lock);
>  	if (some_condition)
> -		pthread_mutex_unlock(&lock);
>  }
>
> But it will report a false positive with this code:
>
> static void
> lock_it(pthread_mutex_t *lock)
> {
> 	pthread_mutex_lock(lock);
> }
>
> static void
> foo(void)
> {
> 	pthread_mutex_lock(&lock);
> 	do_stg();
> 	pthread_mutex_unlock(&lock);
> 	lock_it(&lock);
> 	pthread_mutex_unlock(&lock);
> }
>
> It is perfectly fine to call pthread_mutex_unlock the second time, since LOCK
> has been re-acquired by lock_it(). Is there any way to do inter-procedural
> analysis in a semantic patch ?

I'm not sure that I see anything that would be particularly pleasant.  If
this code is typical, perhaps you could just put when != E on the dots?

Does this happen a lot?

julia

[Cocci] Inter-procedural analysis.

[Cyril Roelandt]

On 12/22/2012 09:49 PM, Julia Lawall wrote:
> On Sat, 22 Dec 2012, Cyril Roelandt wrote:
>
>> Hello!
>>
>> I was trying to find cases of double mutex unlocks in the Hurd, and wrote a
>> very simple semantic patch:
>>
>> @exists@
>> expression E;
>> @@
>> * pthread_mutex_unlock(E);
>> ... when != pthread_mutex_lock(E)
>> * pthread_mutex_unlock(E);
>>
>> This works as expected with this snippet of C code:
>>
>> static void
>> foo(void)
>> {
>> 	pthread_mutex_lock(&lock);
>> 	do_stg();
>> 	pthread_mutex_unlock(&lock);
>> 	if (some_condition)
>> 		pthread_mutex_unlock(&lock);
>> }
>>
>> --- x.c
>> +++ /tmp/cocci-output-4955-ff7d08-x.c
>> @@ -3,7 +3,5 @@ foo(void)
>>   {
>>   	pthread_mutex_lock(&lock);
>>   	do_stg();
>> -	pthread_mutex_unlock(&lock);
>>   	if (some_condition)
>> -		pthread_mutex_unlock(&lock);
>>   }
>>
>> But it will report a false positive with this code:
>>
>> static void
>> lock_it(pthread_mutex_t *lock)
>> {
>> 	pthread_mutex_lock(lock);
>> }
>>
>> static void
>> foo(void)
>> {
>> 	pthread_mutex_lock(&lock);
>> 	do_stg();
>> 	pthread_mutex_unlock(&lock);
>> 	lock_it(&lock);
>> 	pthread_mutex_unlock(&lock);
>> }
>>
>> It is perfectly fine to call pthread_mutex_unlock the second time, since LOCK
>> has been re-acquired by lock_it(). Is there any way to do inter-procedural
>> analysis in a semantic patch ?
>
> I'm not sure that I see anything that would be particularly pleasant.  If
> this code is typical, perhaps you could just put when != E on the dots?
>

I could do this, but sometimes, things get a little bit more complicated:

struct foo {
	pthread_mutex_t *lock;
};

...

static void
bar(struct foo *f)
{
	pthread_mutex_unlock(f->lock);
	do_stg(f);
	pthread_mutex_unlock(f->lock);
}

Here, do_stg() may or may not acquire f->lock, but excluding uses of "f" 
between calls to pthread_mutex_unlock() would probably make us miss bugs.

> Does this happen a lot?

No, and anyway, locking issues are always quite complicated, so the 
patches must be reviewed, and it is not so bad to have a few false 
positives.

I was just curious, and wondering if it would be possible to have a 
bunch of pthread-related semantic patches "ready-to-use" for people who 
are not familiar with Coccinelle, in which case handling such cases 
would have been nice.


Cyril.

[Cocci] Inter-procedural analysis.

[Rene Rydhof Hansen]

[...]

One other thing you might consider is to first look for functions that
acquire the lock and store the (names of) these functions in a
hashtable, e.g., using the ocaml/python scripting capabilities of
Coccinelle, and then use this hashtable to at least reduce the number
of false positives.

It doesn't solve all problems, but it's quick and easy to do.



/rrh

-- 
Rene Rydhof Hansen
email: rrh at cs.aau.dk

[Cocci] Inter-procedural analysis.

[Julia Lawall]

On Sun, 23 Dec 2012, Rene Rydhof Hansen wrote:

> [...]
>
> One other thing you might consider is to first look for functions that
> acquire the lock and store the (names of) these functions in a
> hashtable, e.g., using the ocaml/python scripting capabilities of
> Coccinelle, and then use this hashtable to at least reduce the number
> of false positives.
>
> It doesn't solve all problems, but it's quick and easy to do.

Not so easy I think because there is no way to write a match that matches
any function that is stored in a hash table.  You would have to do
something like the following:

find unbalanced functions and store them in a hash table

find
   unlock at p1
   ... when any
       when != unlock
   f(...)
   ... when any
       when != unlock
   unlock at p

Look for f in the hash table.  If it is found, put p1,p2 in another hash
table.

find
   unlock at p1@p3
   ...
   unlock at p2@p4

Look up p1,p2 in the hash table.  If it is found, do
Coccilib.include_match false.

find
   unlock at p3
   ...
   unlock at p4

Report this as a bug.

But this is likely to be quite a bit slower to run than the previous
version, especially if there are a lot of function calls between locks.
And it only does one level of unfolding.

julia

[Cocci] Inter-procedural analysis.

[Julia Lawall]

On Sat, 22 Dec 2012, Cyril Roelandt wrote:

> On 12/22/2012 09:49 PM, Julia Lawall wrote:
> > On Sat, 22 Dec 2012, Cyril Roelandt wrote:
> >
> > > Hello!
> > >
> > > I was trying to find cases of double mutex unlocks in the Hurd, and wrote
> > > a
> > > very simple semantic patch:
> > >
> > > @exists@
> > > expression E;
> > > @@
> > > * pthread_mutex_unlock(E);
> > > ... when != pthread_mutex_lock(E)
> > > * pthread_mutex_unlock(E);
> > >
> > > This works as expected with this snippet of C code:
> > >
> > > static void
> > > foo(void)
> > > {
> > > 	pthread_mutex_lock(&lock);
> > > 	do_stg();
> > > 	pthread_mutex_unlock(&lock);
> > > 	if (some_condition)
> > > 		pthread_mutex_unlock(&lock);
> > > }
> > >
> > > --- x.c
> > > +++ /tmp/cocci-output-4955-ff7d08-x.c
> > > @@ -3,7 +3,5 @@ foo(void)
> > >   {
> > >   	pthread_mutex_lock(&lock);
> > >   	do_stg();
> > > -	pthread_mutex_unlock(&lock);
> > >   	if (some_condition)
> > > -		pthread_mutex_unlock(&lock);
> > >   }
> > >
> > > But it will report a false positive with this code:
> > >
> > > static void
> > > lock_it(pthread_mutex_t *lock)
> > > {
> > > 	pthread_mutex_lock(lock);
> > > }
> > >
> > > static void
> > > foo(void)
> > > {
> > > 	pthread_mutex_lock(&lock);
> > > 	do_stg();
> > > 	pthread_mutex_unlock(&lock);
> > > 	lock_it(&lock);
> > > 	pthread_mutex_unlock(&lock);
> > > }
> > >
> > > It is perfectly fine to call pthread_mutex_unlock the second time, since
> > > LOCK
> > > has been re-acquired by lock_it(). Is there any way to do inter-procedural
> > > analysis in a semantic patch ?
> >
> > I'm not sure that I see anything that would be particularly pleasant.  If
> > this code is typical, perhaps you could just put when != E on the dots?
> >
>
> I could do this, but sometimes, things get a little bit more complicated:
>
> struct foo {
> 	pthread_mutex_t *lock;
> };
>
> ...
>
> static void
> bar(struct foo *f)
> {
> 	pthread_mutex_unlock(f->lock);
> 	do_stg(f);
> 	pthread_mutex_unlock(f->lock);
> }
>
> Here, do_stg() may or may not acquire f->lock, but excluding uses of "f"
> between calls to pthread_mutex_unlock() would probably make us miss bugs.
>
> > Does this happen a lot?
>
> No, and anyway, locking issues are always quite complicated, so the patches
> must be reviewed, and it is not so bad to have a few false positives.
>
> I was just curious, and wondering if it would be possible to have a bunch of
> pthread-related semantic patches "ready-to-use" for people who are not
> familiar with Coccinelle, in which case handling such cases would have been
> nice.

The problem is that one doesn't know which function to unfold, or how
much.  It could go quite far.

On coccinellery.org there is the semantic patch o_lock_inconsistent.cocci,
which could be useful in general for locks.  It tries to find the case
where the lock is unlocked on some paths and not unlocked on others.  It
tries to take into account the case where both the lock and unlock are
under the same tests.

julia