[cocci] Finding functions that do not unlock mutex in the same function

[cocci] Finding functions that do not unlock mutex in the same function

[Martin Schröder]

[-- Attachment #1: Type: text/plain, Size: 2231 bytes --]

How can I adjust the following code to find all cases where a function
locks a mutex but does not call unlock in the same function:

```
virtual report
virtual patch

@ r exists @
identifier f;
expression l;
expression r, e;
position p;
@@
f@p(...){
... when != k_mutex_lock(...)
r = k_mutex_lock(l, ...)
... when != e = r
if(e){
... when != k_mutex_unlock(l)
    when any
    when strict
when exists
}
(
return ...;
)
}

@ script:python depends on r@
p << r.p;
f << r.f;
@@

// This Python script runs if a locked mutex is not unlocked in all code
paths.
msg = "In function '%s', there's a path without unlocking the mutex. Ensure
that the mutex is always unlocked before returning or exiting the
function." % f
coccilib.report.print_report(p[0], msg)
```
It catches some cases but I'm still not able to make it catch everything
but the first error checking if statement:

```
int invalid_a(int a1, int a2){
int r = k_mutex_lock(mutex, K_MSEC(200));
if(0 != r){
return 0;
}
if(1){
return 1;
}
return 0;
}

int invalid_b(int a1, int a2){
int r = k_mutex_lock(mutex, K_MSEC(200));
if(0 != r){
return 0;
}
return 0;
}


int valid_b(int a1, int a2){
int r = k_mutex_lock(mutex, K_MSEC(200));
if(0 != r){
return 0;
}
k_mutex_unlock(&mutex);
return 0;
}

int invalid_c(int a1, int a2){
int r = k_mutex_lock(mutex, K_MSEC(200));
int b = foo;
if(0 != r){
return 0;
}
if(0 != b){
return 0;
}
k_mutex_unlock(&mutex);
return 0;
}
```

Result:
tests/coccinelle/mutex_lock_unlock.c:1:4-13: In function 'invalid_a',
there's a path without unlocking the mutex. Ensure that the mutex is always
unlocked before returning or exiting the function.
tests/coccinelle/mutex_lock_unlock.c:12:4-13: In function 'invalid_b',
there's a path without unlocking the mutex. Ensure that the mutex is always
unlocked before returning or exiting the function.

Invalid_c is not detected.

-- 
Best regards,

Martin Schröder
*Embedded Firmware Consultant*
Connect on LinkedIn <https://www.linkedin.com/in/martinschroder/>
*Book online meeting <https://calendly.com/martinschroder/call>*

Swedish Embedded Consulting Group AB
W. https://swedishembedded.com

[-- Attachment #2: Type: text/html, Size: 3732 bytes --]

Re: [cocci] Finding functions that do not unlock mutex in the same function

[Julia Lawall]

[-- Attachment #1: Type: text/plain, Size: 2589 bytes --]



On Fri, 20 Oct 2023, Martin Schröder wrote:

> How can I adjust the following code to find all cases where a function locks a mutex but does not call unlock in the same function:
>
> ```
> virtual report
> virtual patch
>
> @ r exists @
> identifier f;
> expression l;
> expression r, e;
> position p;
> @@
> f@p(...){
> ... when != k_mutex_lock(...)

Drop the above two lines.

> r = k_mutex_lock(l, ...)
> ... when != e = r
> if(e){
> ... when != k_mutex_unlock(l)
>     when any
>     when strict
>     when exists

when exists is not needed here, since you have that already.

> }

I think you could just put

... when any
    when !=  k_mutex_unlock(l)

and drop the rest.

> (
> return ...;
> )
> }

Does that work the way you wanted?

julia


>
> @ script:python depends on r@
> p << r.p;
> f << r.f;
> @@
>
> // This Python script runs if a locked mutex is not unlocked in all code paths.
> msg = "In function '%s', there's a path without unlocking the mutex. Ensure that the mutex is always unlocked before returning or exiting the function." % f
> coccilib.report.print_report(p[0], msg)
> ```
> It catches some cases but I'm still not able to make it catch everything but the first error checking if statement:
>
> ```
> int invalid_a(int a1, int a2){
> int r = k_mutex_lock(mutex, K_MSEC(200));
> if(0 != r){
> return 0;
> }
> if(1){
> return 1;
> }
> return 0;
> }
>
> int invalid_b(int a1, int a2){
> int r = k_mutex_lock(mutex, K_MSEC(200));
> if(0 != r){
> return 0;
> }
> return 0;
> }
>
>
> int valid_b(int a1, int a2){
> int r = k_mutex_lock(mutex, K_MSEC(200));
> if(0 != r){
> return 0;
> }
> k_mutex_unlock(&mutex);
> return 0;
> }
>
> int invalid_c(int a1, int a2){
> int r = k_mutex_lock(mutex, K_MSEC(200));
> int b = foo;
> if(0 != r){
> return 0;
> }
> if(0 != b){
> return 0;
> }
> k_mutex_unlock(&mutex);
> return 0;
> }
> ```
>
> Result:
> tests/coccinelle/mutex_lock_unlock.c:1:4-13: In function 'invalid_a', there's a path without unlocking the mutex. Ensure that the mutex is always unlocked before returning or exiting the function.
> tests/coccinelle/mutex_lock_unlock.c:12:4-13: In function 'invalid_b', there's a path without unlocking the mutex. Ensure that the mutex is always unlocked before returning or exiting the function.
>
> Invalid_c is not detected.
>
> --
> Best regards,
>
> [AIorK4wH6aPZe4eYWheYhio282OdbmPN-eMyvcew6PbeQLd1K_qGuSNTnBuq0VT6bSD79PDVrzgSr5c]
> Martin Schröder
> Embedded Firmware Consultant
> Connect on LinkedIn
> Book online meeting
>
> Swedish Embedded Consulting Group AB
> W. https://swedishembedded.com
>
>
>
>

Re: [cocci] Finding functions that do not unlock mutex in the same function

[Markus Elfring]

> I think you could just put
>
> ... when any
>     when !=  k_mutex_unlock(l)
>
> and drop the rest.

How do you think about to check the desired consistency of lock scopes
in more detail?

Will any software extensions become helpful for further source code analyses?

Regards,
Markus

Re: [cocci] Finding functions that do not unlock mutex in the same function

[Martin Schröder]

[-- Attachment #1: Type: text/plain, Size: 1772 bytes --]

Thanks Julia.

My final script that seems to work looks like this:

virtual report
virtual patch

@ r exists @
expression l;
identifier r, e;
position p;
@@
r = k_mutex_lock(l, ...)
... when any
if(r){ ... }
... when != e = r
when any
if(e){
... when any
when != k_mutex_unlock(l)
return@p ...;
}

First I match k_mutex_lock. Then there can be any statements between that
and the first check.

If locking fails then in the first check it is valid to return. Not sure
how to capture that this first if statement must return in that case.

Then there can follow additional if statements and in all of them there
must be an unlock if there is also a return.

The sample code looks like this:

struct k_mutex lock;

int function(){

int r = k_mutex_lock(&lock, K_FOREVER);
if(r){

return -ETIMEDOUT; // valid to not unlock here

}
r = produce_something();
if(r){

k_mutex_unlock(&lock);

return -EIO;

}
r = produce_something();
if(r){

return -EINVAL; // here an unlock is missing

}
k_mutex_unlock(&lock);
return 0;

}

On Fri, 20 Oct 2023 at 17:01, Markus Elfring <Markus.Elfring@web.de> wrote:

> > I think you could just put
> >
> > ... when any
> >     when !=  k_mutex_unlock(l)
> >
> > and drop the rest.
>
> How do you think about to check the desired consistency of lock scopes
> in more detail?
>
> Will any software extensions become helpful for further source code
> analyses?
>
> Regards,
> Markus
>


-- 
Best regards,

Martin Schröder
*Embedded Firmware Consultant*
Connect on LinkedIn <https://www.linkedin.com/in/martinschroder/>
*Book online meeting <https://calendly.com/martinschroder/call>*

Swedish Embedded Consulting Group AB
W. https://swedishembedded.com

[-- Attachment #2: Type: text/html, Size: 3763 bytes --]

Re: [cocci] Finding functions that do not unlock mutex in the same function

[Markus Elfring]

> My final script that seems to work looks like this:
>
> virtual report
> virtual patch
>
> @ r exists @
> expression l;
> identifier r, e;
> position p;
> @@
> r = k_mutex_lock(l, ...)
> ... when any
> if(r){ ... }
> ... when != e = r
> when any
> if(e){
> ... when any
> when != k_mutex_unlock(l)
> return@p ...;
> }
>
> First I match k_mutex_lock. Then there can be any statements between that and the first check.

I suggest to take further case distinctions better into account
also for such a source code analysis approach.

I imagine that you would like to restrict the code which may be used
between a function call and a corresponding return value check.
Should the (compound) statement be restricted also for the corresponding if branch?


> If locking fails then in the first check it is valid to return.

Such a control flow possibility is reasonable.


> Not sure how to capture that this first if statement must return in that case.

How do you think about to add any SmPL disjunctions and to adjust the usage
of SmPL ellipses?


> Then there can follow additional if statements and in all of them there must be an unlock if there is also a return.

* Why do you try to exclude the assignment of the item “r” to other items?

* Would you occasionally like to support (lock) scopes which would be distributed over
  multiple function implementations?

Regards,
Markus

Re: [cocci] Finding functions that do not unlock mutex in the same function

[Martin Schröder]

[-- Attachment #1: Type: text/plain, Size: 2575 bytes --]

I explicitly want to disallow lock scopes that are distributed over
multiple functions. Instead, semaphore should be used in such cases. I want
to create a rule that ensures that 1. proper unlocking takes place across
all exit paths and 2. that both locking and unlocking happen in the same
function.

Markus, how would you recommend using disjunctions?

Here is my slightly updated rule:

@ r exists @
expression l;
identifier r, e;
position p;
@@
r = k_mutex_lock(l, ...)
... when any
if(r){ ... }
... when != e = r
when any
if(e){
... when any
when != k_mutex_unlock(l)
return@p ...;
}
... when != k_mutex_unlock(l)
k_mutex_unlock(l);



On Sun, 22 Oct 2023 at 10:44, Markus Elfring <Markus.Elfring@web.de> wrote:

> > My final script that seems to work looks like this:
> >
> > virtual report
> > virtual patch
> >
> > @ r exists @
> > expression l;
> > identifier r, e;
> > position p;
> > @@
> > r = k_mutex_lock(l, ...)
> > ... when any
> > if(r){ ... }
> > ... when != e = r
> > when any
> > if(e){
> > ... when any
> > when != k_mutex_unlock(l)
> > return@p ...;
> > }
> >
> > First I match k_mutex_lock. Then there can be any statements between
> that and the first check.
>
> I suggest to take further case distinctions better into account
> also for such a source code analysis approach.
>
> I imagine that you would like to restrict the code which may be used
> between a function call and a corresponding return value check.
> Should the (compound) statement be restricted also for the corresponding
> if branch?
>
>
> > If locking fails then in the first check it is valid to return.
>
> Such a control flow possibility is reasonable.
>
>
> > Not sure how to capture that this first if statement must return in that
> case.
>
> How do you think about to add any SmPL disjunctions and to adjust the usage
> of SmPL ellipses?
>
>
> > Then there can follow additional if statements and in all of them there
> must be an unlock if there is also a return.
>
> * Why do you try to exclude the assignment of the item “r” to other items?
>
> * Would you occasionally like to support (lock) scopes which would be
> distributed over
>   multiple function implementations?
>
> Regards,
> Markus
>


-- 
Best regards,

Martin Schröder
*Embedded Firmware Consultant*
Connect on LinkedIn <https://www.linkedin.com/in/martinschroder/>
*Book online meeting <https://calendly.com/martinschroder/call>*

Swedish Embedded Consulting Group AB
W. https://swedishembedded.com

[-- Attachment #2: Type: text/html, Size: 4250 bytes --]

Re: [cocci] Finding functions that do not unlock mutex in the same function

[Markus Elfring]

> I explicitly want to disallow lock scopes that are distributed over multiple functions.
> Instead, semaphore should be used in such cases.

Have you got any special preferences for locking primitives?


Did you get the impression that the proper handling of various scopes triggers
further development challenges also for the safe application of the semantic patch language
(Coccinelle software)?
https://en.wikipedia.org/wiki/Scope_(computer_science)


> Markus, how would you recommend using disjunctions? 

Please take another look at known information sources.
Do any SmPL script examples indicate how desirable case distinctions can be achieved with them?


> Here is my slightly updated rule:

I would appreciate further answers for presented questions.

Regards,
Markus

Re: [cocci] Finding functions that do not unlock mutex in the same function

[Markus Elfring]

> I explicitly want to disallow lock scopes that are distributed over multiple functions.

It seems that you are trying to restrict the desired control flow analysis
to intra-procedural means.


> Here is my slightly updated rule:

You would like to achieve something with a single SmPL rule so far.
I suggest to take additional software design options into account
for possible solution approaches.
How do you think about to work with more data processing steps?

The source code positions can be determined for lock and unlock function calls.

* Would you like to perform any advanced data processing by the means
  of supported programming languages?
  + OCaml
  + Python

* Can a corresponding report show how consistent the expected lock scopes would be?

Regards,
Markus

Re: [cocci] Finding functions that do not unlock mutex in the same function

[Julia Lawall]

[-- Attachment #1: Type: text/plain, Size: 2230 bytes --]



On Sat, 21 Oct 2023, Martin Schröder wrote:

> Thanks Julia.
> My final script that seems to work looks like this:
>
> virtual report
> virtual patch
>
> @ r exists @
> expression l;
> identifier r, e;
> position p;
> @@
> r = k_mutex_lock(l, ...)
> ... when any
> if(r){ ... }

Put a return ...; after the ... to require the branch to return.  This
will cover the case where there is a goto that leads to the return.

> ... when != e = r
> when any

I would consider it to be more readable to line up the when lines.

julia

> if(e){
> ... when any
> when != k_mutex_unlock(l)
> return@p ...;
> }
>
> First I match k_mutex_lock. Then there can be any statements between that and the first check.
>
> If locking fails then in the first check it is valid to return. Not sure how to capture that this first if statement must return in that case. 
>
> Then there can follow additional if statements and in all of them there must be an unlock if there is also a return.
>
> The sample code looks like this:
>
> struct k_mutex lock;
>
> int function(){
>       int r = k_mutex_lock(&lock, K_FOREVER);
>       if(r){
>             return -ETIMEDOUT; // valid to not unlock here
>
>       }
>       r = produce_something();
>       if(r){
>             k_mutex_unlock(&lock);
>
>             return -EIO;
>
>       }
>       r = produce_something();
>       if(r){
>             return -EINVAL; // here an unlock is missing
>
>       }
>       k_mutex_unlock(&lock);
>       return 0;
>
> }
>
> On Fri, 20 Oct 2023 at 17:01, Markus Elfring <Markus.Elfring@web.de> wrote:
>       > I think you could just put
>       >
>       > ... when any
>       >     when !=  k_mutex_unlock(l)
>       >
>       > and drop the rest.
>
>       How do you think about to check the desired consistency of lock scopes
>       in more detail?
>
>       Will any software extensions become helpful for further source code analyses?
>
>       Regards,
>       Markus
>
>
>
> --
> Best regards,
>
> [AIorK4wH6aPZe4eYWheYhio282OdbmPN-eMyvcew6PbeQLd1K_qGuSNTnBuq0VT6bSD79PDVrzgSr5c]
> Martin Schröder
> Embedded Firmware Consultant
> Connect on LinkedIn
> Book online meeting
>
> Swedish Embedded Consulting Group AB
> W. https://swedishembedded.com
>
>
>
>

Re: [cocci] Dependencies between key words “goto” and “return”?

[Markus Elfring]

>> if(r){ ... }
>
> Put a return ...; after the ... to require the branch to return.

Can any more restrictions become relevant for such SmPL code?


> This will cover the case where there is a goto that leads to the return.

Would you like to explain this information a bit more?

Regards,
Markus

Re: [cocci] Dependencies between key words “goto” and “return”?

[Julia Lawall]

On Wed, 25 Oct 2023, Markus Elfring wrote:

> >> if(r){ ... }
> >
> > Put a return ...; after the ... to require the branch to return.
>
> Can any more restrictions become relevant for such SmPL code?
>
>
> > This will cover the case where there is a goto that leads to the return.
>
> Would you like to explain this information a bit more?

The ... follows the control-flow patch over the goto until it reaches a
return.

julia

Re: [cocci] Dependencies between key words “goto” and “return”?

[Markus Elfring]

>>>> if(r){ ... }
…
>>> This will cover the case where there is a goto that leads to the return.
>>
>> Would you like to explain this information a bit more?
>
> The ... follows the control-flow patch over the goto until it reaches a return.

* Would you like to refer to “code paths” here?

* Goto statements can occasionally jump to source code places
  that would be connected to other items than a return statement.

Regards,
Markus