[cocci] Searching for questionable call pairs (with SmPL)?

[cocci] Searching for questionable call pairs (with SmPL)?

[Markus Elfring]

Hello,

I noticed another contribution.

I got into the mood to construct another script for the semantic patch language.


// See also:
// [PATCH v4] ALSA: usb-audio: qcom: Adjust mutex unlock order
// https://lore.kernel.org/linux-sound/20250721114554.1666104-1-karanja99erick@gmail.com/
@display@
expression x, y;
@@
*mutex_lock(x);
 ...
*mutex_lock(y);
 <+...
*mutex_unlock(x);
 ...
*mutex_unlock(y);
 ...+>


Questionable test result (by the software combination “Coccinelle 1.3.0” for example):
Markus_Elfring@Sonne:…/Projekte/Linux/next-analyses> git checkout next-20250722 && time /usr/bin/spatch --no-loops …/Projekte/Coccinelle/janitor/show_questionable_unlock_call_order.cocci sound/usb/qcom/qc_audio_offload.c
…
@@ -1580,7 +1576,6 @@ static void handle_uaudio_stream_req(str
                goto response;
        }
 
-       mutex_lock(&chip->mutex);
        if (req_msg->enable) {
                if (info_idx < 0 || chip->system_suspend || subs->opened) {
                        ret = -EBUSY;
@@ -1613,9 +1608,7 @@ static void handle_uaudio_stream_req(str
                        ret = prepare_qmi_response(subs, req_msg, &resp,
                                                   info_idx);
                if (ret < 0) {
-                       mutex_lock(&chip->mutex);
                        subs->opened = 0;
-                       mutex_unlock(&chip->mutex);
                }
        } else {
                info = &uadev[pcm_card_num].info[info_idx];
@@ -1646,9 +1639,7 @@ static void handle_uaudio_stream_req(str
                }
 
                disable_audio_stream(subs);
-               mutex_lock(&chip->mutex);
                subs->opened = 0;
-               mutex_unlock(&chip->mutex);
        }
 
 response:
@@ -1662,7 +1653,6 @@ response:
                if (atomic_read(&uadev[pcm_card_num].in_use))
                        kref_put(&uadev[pcm_card_num].kref,
                                 uaudio_dev_release);
-               mutex_unlock(&chip->mutex);
        }
        mutex_unlock(&qdev_mutex);
 
…
real    0m0,501s
user    0m0,460s
sys     0m0,035s


Now I wonder how these diff hunks fit to my source code search approach
for finding call pairs of known functions (or macros).
Will another clarification become more interesting?

Regards,
Markus

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Markus Elfring]

> Now I wonder how these diff hunks fit to my source code search approach
> for finding call pairs of known functions (or macros).
> Will another clarification become more interesting?

…
@@ -1613,9 +1608,7 @@ static void handle_uaudio_stream_req(str
                        ret = prepare_qmi_response(subs, req_msg, &resp,
                                                   info_idx);
                if (ret < 0) {
-                       mutex_lock(&chip->mutex);
                        subs->opened = 0;
-                       mutex_unlock(&chip->mutex);
                }
        } else {
                info = &uadev[pcm_card_num].info[info_idx];
…

* How can such a difference display happen at all when it is expected
  that the macro calls “mutex_lock(&qdev_mutex)” and “mutex_lock(&chip->mutex)”
  should be presented before?
  https://elixir.bootlin.com/linux/v6.16-rc7/source/sound/usb/qcom/qc_audio_offload.c#L1542-L1583

* The source code search pattern indicates an other unlock call order,
  doesn't it?


Regards,
Markus

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Julia Lawall]

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



On Wed, 23 Jul 2025, Markus Elfring wrote:

> Hello,
>
> I noticed another contribution.
>
> I got into the mood to construct another script for the semantic patch language.
>
>
> // See also:
> // [PATCH v4] ALSA: usb-audio: qcom: Adjust mutex unlock order
> // https://lore.kernel.org/linux-sound/20250721114554.1666104-1-karanja99erick@gmail.com/
> @display@
> expression x, y;
> @@
> *mutex_lock(x);
>  ...
> *mutex_lock(y);
>  <+...
> *mutex_unlock(x);
>  ...
> *mutex_unlock(y);
>  ...+>

* just highlights lines when there is a match.  Theer can be several
possible matches.  In that case, the union of the relevant lines will be
highlighted.

julia

>
>
> Questionable test result (by the software combination “Coccinelle 1.3.0” for example):
> Markus_Elfring@Sonne:…/Projekte/Linux/next-analyses> git checkout next-20250722 && time /usr/bin/spatch --no-loops …/Projekte/Coccinelle/janitor/show_questionable_unlock_call_order.cocci sound/usb/qcom/qc_audio_offload.c
> …
> @@ -1580,7 +1576,6 @@ static void handle_uaudio_stream_req(str
>                 goto response;
>         }
>
> -       mutex_lock(&chip->mutex);
>         if (req_msg->enable) {
>                 if (info_idx < 0 || chip->system_suspend || subs->opened) {
>                         ret = -EBUSY;
> @@ -1613,9 +1608,7 @@ static void handle_uaudio_stream_req(str
>                         ret = prepare_qmi_response(subs, req_msg, &resp,
>                                                    info_idx);
>                 if (ret < 0) {
> -                       mutex_lock(&chip->mutex);
>                         subs->opened = 0;
> -                       mutex_unlock(&chip->mutex);
>                 }
>         } else {
>                 info = &uadev[pcm_card_num].info[info_idx];
> @@ -1646,9 +1639,7 @@ static void handle_uaudio_stream_req(str
>                 }
>
>                 disable_audio_stream(subs);
> -               mutex_lock(&chip->mutex);
>                 subs->opened = 0;
> -               mutex_unlock(&chip->mutex);
>         }
>
>  response:
> @@ -1662,7 +1653,6 @@ response:
>                 if (atomic_read(&uadev[pcm_card_num].in_use))
>                         kref_put(&uadev[pcm_card_num].kref,
>                                  uaudio_dev_release);
> -               mutex_unlock(&chip->mutex);
>         }
>         mutex_unlock(&qdev_mutex);
>
> …
> real    0m0,501s
> user    0m0,460s
> sys     0m0,035s
>
>
> Now I wonder how these diff hunks fit to my source code search approach
> for finding call pairs of known functions (or macros).
> Will another clarification become more interesting?
>
> Regards,
> Markus
>

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Markus Elfring]

>> @display@
>> expression x, y;
>> @@
>> *mutex_lock(x);
>>  ...
>> *mutex_lock(y);
>>  <+...
>> *mutex_unlock(x);
>>  ...
>> *mutex_unlock(y);
>>  ...+>
> * just highlights lines when there is a match.  Theer can be several
> possible matches.

This is actually the case for a known source file.
https://elixir.bootlin.com/linux/v6.16-rc7/source/sound/usb/qcom/qc_audio_offload.c


>                    In that case, the union of the relevant lines will be highlighted.

I am still looking for further possibilities to avoid false positives.

* The source code search pattern can be simplified a bit
  by omitting two SmPL ellipses.
  (But the search approach should be more advanced, shouldn't it?)

* Why is the diff marking missing for the first lock call so far
  (within the implementation of the function “handle_uaudio_stream_req”)?


I would appreciate further advices.

Regards,
Markus

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Julia Lawall]

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



On Thu, 24 Jul 2025, Markus Elfring wrote:

> >> @display@
> >> expression x, y;
> >> @@
> >> *mutex_lock(x);
> >>  ...
> >> *mutex_lock(y);
> >>  <+...
> >> *mutex_unlock(x);
> >>  ...
> >> *mutex_unlock(y);
> >>  ...+>
> > * just highlights lines when there is a match.  Theer can be several
> > possible matches.
>
> This is actually the case for a known source file.
> https://elixir.bootlin.com/linux/v6.16-rc7/source/sound/usb/qcom/qc_audio_offload.c
>
>
> >                    In that case, the union of the relevant lines will be highlighted.
>
> I am still looking for further possibilities to avoid false positives.
>
> * The source code search pattern can be simplified a bit
>   by omitting two SmPL ellipses.
>   (But the search approach should be more advanced, shouldn't it?)
>
> * Why is the diff marking missing for the first lock call so far
>   (within the implementation of the function “handle_uaudio_stream_req”)?
>
>
> I would appreciate further advices.

I would think you should do:

@r exists@
expression x, y;
position p1,p2,p3,p4;
@@
mutex_lock(x);@p1
 ...
mutex_lock(y);@p2
...
mutex_unlock(x);@p3
 ...
mutex_unlock(y);@p4

And then use a python rule to print p1, p2, p3, p4.  That way you will keep
the different matches separated.

julia

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Markus Elfring]

>> * Why is the diff marking missing for the first lock call so far
>>   (within the implementation of the function “handle_uaudio_stream_req”)?
>>
>>
>> I would appreciate further advices.
> I would think you should do:
> 
> @r exists@
> expression x, y;
> position p1,p2,p3,p4;
> @@
> mutex_lock(x);@p1
>  ...
> mutex_lock(y);@p2
> ...
> mutex_unlock(x);@p3
>  ...
> mutex_unlock(y);@p4
> 
> And then use a python rule to print p1, p2, p3, p4.  That way you will keep
> the different matches separated.

I miss still a corresponding answer for my original question.


Can the Coccinelle software handle call orders correctly also according to
passed (different) expressions?

Regards,
Markus

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Julia Lawall]

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



On Thu, 24 Jul 2025, Markus Elfring wrote:

> >> * Why is the diff marking missing for the first lock call so far
> >>   (within the implementation of the function “handle_uaudio_stream_req”)?
> >>
> >>
> >> I would appreciate further advices.
> > I would think you should do:
> >
> > @r exists@
> > expression x, y;
> > position p1,p2,p3,p4;
> > @@
> > mutex_lock(x);@p1
> >  ...
> > mutex_lock(y);@p2
> > ...
> > mutex_unlock(x);@p3
> >  ...
> > mutex_unlock(y);@p4
> >
> > And then use a python rule to print p1, p2, p3, p4.  That way you will keep
> > the different matches separated.
>
> I miss still a corresponding answer for my original question.
>
>
> Can the Coccinelle software handle call orders correctly also according to
> passed (different) expressions?

I don't particularly understand the question, but Coccinelle knows about
the control flow, so it would seem that all is ok.

julia

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Markus Elfring]

>>>> * Why is the diff marking missing for the first lock call so far
>>>>   (within the implementation of the function “handle_uaudio_stream_req”)?
>>>>
>>>>
>>>> I would appreciate further advices.
>>> I would think you should do:
…

>>> And then use a python rule to print p1, p2, p3, p4.  That way you will keep
>>> the different matches separated.
>>
>> I miss still a corresponding answer for my original question.
>>
>>
>> Can the Coccinelle software handle call orders correctly also according to
>> passed (different) expressions?
> 
> I don't particularly understand the question,

Why does this happen again for this clarification approach?


>                                               but Coccinelle knows about
> the control flow, so it would seem that all is ok.

I got the impression that another implementation detail is broken so far
and is therefore improvable somehow.

Regards,
Markus

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Markus Elfring]

> I would think you should do:
> 
> @r exists@
> expression x, y;
> position p1,p2,p3,p4;
> @@
> mutex_lock(x);@p1
>  ...
> mutex_lock(y);@p2
> ...
> mutex_unlock(x);@p3
>  ...
> mutex_unlock(y);@p4
> 
> And then use a python rule to print p1, p2, p3, p4.  That way you will keep
> the different matches separated.

Will the following source code search approach trigger more helpful
development considerations?


@find@
expression x, y;
position l1, l2, ul1, ul2;
@@
 mutex_lock@l1(x);
 ...
 mutex_lock@l2(y);
 <+...
 mutex_unlock@ul1(x);
 ...
 mutex_unlock@ul2(y);
 ...+>

@display@
expression find.x, find.y;
position find.l1, find.l2;
@@
*mutex_lock@l1(x);
 ...
*mutex_lock@l2(y);


Questionable test result (by the software combination “Coccinelle 1.3.0” for example):
Markus_Elfring@Sonne:…/Projekte/Coccinelle/Probe> time /usr/bin/spatch --no-loops ../janitor/show_questionable_unlock_call_order3.cocci qc_audio_offload-handle_uaudio_stream_req-excerpt-20250722.c
…
@@ -70,7 +70,6 @@ static void handle_uaudio_stream_req(str
                goto response;
        }
 
-       mutex_lock(&chip->mutex);
        if (req_msg->enable) {
                if (info_idx < 0 || chip->system_suspend || subs->opened) {
                        ret = -EBUSY;
@@ -103,7 +102,6 @@ static void handle_uaudio_stream_req(str
                        ret = prepare_qmi_response(subs, req_msg, &resp,
                                                   info_idx);
                if (ret < 0) {
-                       mutex_lock(&chip->mutex);
                        subs->opened = 0;
                        mutex_unlock(&chip->mutex);
                }
@@ -136,7 +134,6 @@ static void handle_uaudio_stream_req(str
                }
 
                disable_audio_stream(subs);
-               mutex_lock(&chip->mutex);
                subs->opened = 0;
                mutex_unlock(&chip->mutex);
        }

real    0m0,197s
user    0m0,172s
sys     0m0,024s


Regards,
Markus

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Markus Elfring]

> Will another clarification become more interesting?

Another source code search approach can eventually help to provide further
insights into presented software development concerns.


// handle_uaudio_stream_req()
// https://elixir.bootlin.com/linux/v6.16-rc7/source/sound/usb/qcom/qc_audio_offload.c#L1508
@display@
expression x, y;
@@
 if (!svc->client_connected)
 {
    ...
 }

*mutex_lock(x);
 ...
*mutex_lock(y);
 <+...
*mutex_unlock(x);
 ...
*mutex_unlock(y);
 ...+>


Another test result (by the software combination “Coccinelle 1.3.0” for example):
Markus_Elfring@Sonne:…/Projekte/Coccinelle/Probe> time /usr/bin/spatch --no-loops ../janitor/show_questionable_unlock_call_order5.cocci qc_audio_offload-handle_uaudio_stream_req-excerpt-20250722.c
[no diff output]
…
real    0m0,103s
user    0m0,085s
sys     0m0,018s



Does the specification of additional context from the beginning of the discussed
function implementation influence the exclusion of a false positive?

Regards,
Markus

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Markus Elfring]

> Will another clarification become more interesting?

Another source code search approach can eventually help to influence
some software understanding into more desirable directions.


@display@
@@
(mutex_lock
|mutex_unlock
)(
*...
 );


Another test result (by the software combination “Coccinelle 1.3.0” for example):
Markus_Elfring@Sonne:…/Projekte/Linux/next-analyses> git checkout next-20250722 && /usr/bin/spatch --no-loops sound/usb/qcom/qc_audio_offload.c …/Projekte/Coccinelle/janitor/show_data_for_mutex_lock_and_unlock_calls.cocci | grep -E '^-\s+mutex_' | wc -l
… 
39

* Will such information trigger further collateral evolution?

* Would lock guards become applicable at more source code places?
  https://elixir.bootlin.com/linux/v6.16-rc7/source/include/linux/mutex.h#L225


Regards,
Markus

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Markus Elfring]

>> I would appreciate further advices.
> I would think you should do:

Would you like to add any insights why an additional qualification
would become relevant for the first SmPL ellipsis in the discussed
source code search pattern?
https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/922426fe0eeb860710a34e430e065cf33e990ca4/docs/manual/cocci_syntax.tex#L1007-1014


@display@
expression x, y;
@@
*mutex_lock(x);
 ... when forall
*mutex_lock(y);
 <+...
*mutex_unlock(x);
 ...
*mutex_unlock(y);
 ...+>


Regards,
Markus

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Markus Elfring]

> Would you like to add any insights why an additional qualification
> would become relevant for the first SmPL ellipsis in the discussed
> source code search pattern?

Would you get further development ideas if the source code search approach
(like the following for example) would be more general?


@display@
expression allocate, release, x, y;
@@
*allocate(x);
 ... when forall
*allocate(y);
 <+...
*release(x);
 ...
*release(y);
 ...+>


How do you think about to refine the selection of relevant
macro/function calls here?

Will any constraints become more interesting for usable call pairs?

Regards,
Markus

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Julia Lawall]

On Fri, 1 Aug 2025, Markus Elfring wrote:

> > Would you like to add any insights why an additional qualification
> > would become relevant for the first SmPL ellipsis in the discussed
> > source code search pattern?
>
> Would you get further development ideas if the source code search approach
> (like the following for example) would be more general?
>
>
> @display@
> expression allocate, release, x, y;
> @@
> *allocate(x);
>  ... when forall
> *allocate(y);
>  <+...
> *release(x);
>  ...
> *release(y);
>  ...+>

What is the goal of using <+... ...+> ?  The only way you should have
multiple releases is if there is a double lock error.  If you want to
search for double lock errors why do it only in the case where there are
two locks involved?

If you want to check for lock(a) lock(b) unlock(a) unlock(b), there is no
need for <+... ...+>.  Furthermore, you need to check that there is no
unlock of a between the lock(a) and lock(b), likewise no unlock(b) between
lock(b) and unlock (a).

julia

>
>
> How do you think about to refine the selection of relevant
> macro/function calls here?
>
> Will any constraints become more interesting for usable call pairs?
>
> Regards,
> Markus
>

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Markus Elfring]

>> Would you get further development ideas if the source code search approach
>> (like the following for example) would be more general?
>>
>>
>> @display@
>> expression allocate, release, x, y;
>> @@
>> *allocate(x);
>>  ... when forall
>> *allocate(y);
>>  <+...
>> *release(x);
>>  ...
>> *release(y);
>>  ...+>
> 
> What is the goal of using <+... ...+> ?  The only way you should have
> multiple releases is if there is a double lock error.

Really?

Would we become more concerned about any use-after-free here?
https://cwe.mitre.org/data/definitions/416.html
https://wiki.sei.cmu.edu/confluence/spaces/c/pages/87152153/MEM30-C.+Do+not+access+freed+memory


>                                                        If you want to
> search for double lock errors why do it only in the case where there are
> two locks involved?

The relative order of the searched release operations can be clarified better,
can't it?


> If you want to check for lock(a) lock(b) unlock(a) unlock(b), there is no
> need for <+... ...+>.  Furthermore, you need to check that there is no
> unlock of a between the lock(a) and lock(b), likewise no unlock(b) between
> lock(b) and unlock (a).

The source code search approach is obviously improvable in various ways.

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

> What is the goal of using <+... ...+> ?  The only way you should have
> multiple releases is if there is a double lock error.  If you want to
> search for double lock errors why do it only in the case where there are
> two locks involved?
> 
> If you want to check for lock(a) lock(b) unlock(a) unlock(b), there is no
> need for <+... ...+>.  Furthermore, you need to check that there is no
> unlock of a between the lock(a) and lock(b), likewise no unlock(b) between
> lock(b) and unlock (a).

Would you get into the mood to clarify data processing challenges better
for another source code search pattern (like the following)?


@display@
expression x, y;
@@
 action_lock(x);
 ... when != action_unlock(x);
*action_lock(y);
 <+... when != action_unlock(y);
*action_lock(y);
 ...+>


See also a corresponding source file example:
https://github.com/coccinelle/coccinelle/issues/404


Questionable test result (by the software combination “Coccinelle 1.3.0” for example):
Markus_Elfring@Sonne:…/Projekte/Coccinelle/Probe> time /usr/bin/spatch ../janitor/show_lock_calls_without_unlock2.cocci test-action_locks-20250725.c
[no diff output]

real    0m0,060s
user    0m0,051s
sys     0m0,009s


Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

> Would you get into the mood to clarify data processing challenges better
> for another source code search pattern (like the following)?

How reasonable would you find a test result for another source code search approach?


@display@
expression x, y;
@@
 action_lock(x);
 ... when != action_unlock(x);
*action_lock(y);


Markus_Elfring@Sonne:…/Projekte/Coccinelle/Probe> time /usr/bin/spatch ../janitor/show_second_lock_call_variant.cocci test-action_locks-20250725.c
…
@@ -2,13 +2,11 @@ void my_action_test(void)
 {
  action_lock(&blockage1);
  my_log("blocked 1");
- action_lock(&blockage2);
  my_log("blocked 2");
 
  if (my_surprise(123))
  {
   my_log("surprised!");
-  action_lock(&blockage2);
   my_log("blocked 2 once more");
   result = 99;
   action_unlock(&blockage2);

real    0m0,067s
user    0m0,045s
sys     0m0,021s


Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Julia Lawall]

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



On Sat, 2 Aug 2025, Markus Elfring wrote:

> > Would you get into the mood to clarify data processing challenges better
> > for another source code search pattern (like the following)?
>
> How reasonable would you find a test result for another source code search approach?

Completely reasonable.  You match pairs of subsequent locks, but you only
mark the second one in the pair.  So you match two pairs:

action_lock(&blockage1); and action_lock(&blockage2);

and

action_lock(&blockage2); and action_lock(&blockage2);

and you mark the second one in each case.

It would greatly help communication if you would also provide the answer
that you expect.

Please do not include the running time in every run, because that doesn't
seem to be related to the issue you are concerned about.

julia


>
>
> @display@
> expression x, y;
> @@
>  action_lock(x);
>  ... when != action_unlock(x);
> *action_lock(y);
>
>
> Markus_Elfring@Sonne:…/Projekte/Coccinelle/Probe> time /usr/bin/spatch ../janitor/show_second_lock_call_variant.cocci test-action_locks-20250725.c
> …
> @@ -2,13 +2,11 @@ void my_action_test(void)
>  {
>   action_lock(&blockage1);
>   my_log("blocked 1");
> - action_lock(&blockage2);
>   my_log("blocked 2");
>
>   if (my_surprise(123))
>   {
>    my_log("surprised!");
> -  action_lock(&blockage2);
>    my_log("blocked 2 once more");
>    result = 99;
>    action_unlock(&blockage2);
>
> real    0m0,067s
> user    0m0,045s
> sys     0m0,021s
>
>
> Regards,
> Markus
>

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

>>> Would you get into the mood to clarify data processing challenges better
>>> for another source code search pattern (like the following)?
>>
>> How reasonable would you find a test result for another source code search approach?
> 
> Completely reasonable.

I got an other understanding for the functionality of the Coccinelle software here
so far.


>                         You match pairs of subsequent locks, but you only
> mark the second one in the pair.  So you match two pairs:
> 
> action_lock(&blockage1); and action_lock(&blockage2);
> 
> and
> 
> action_lock(&blockage2); and action_lock(&blockage2);
> 
> and you mark the second one in each case.

It seems that our data processing expectations differ once more.


> It would greatly help communication if you would also provide the answer
> that you expect.

A “shortest path constraint” is mentioned for the usage of the SmPL ellipsis.
https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/3aa9a6ab3b035e31292be31399b99a8857480aef/docs/manual/cocci_syntax.tex#L1035-1043


…>> @display@
>> expression x, y;
>> @@
>>  action_lock(x);
>>  ... when != action_unlock(x);
>> *action_lock(y);

May I expect that only a single call should be marked for such a test case?

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Julia Lawall]

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



On Sat, 2 Aug 2025, Markus Elfring wrote:

> >>> Would you get into the mood to clarify data processing challenges better
> >>> for another source code search pattern (like the following)?
> >>
> >> How reasonable would you find a test result for another source code search approach?
> >
> > Completely reasonable.
>
> I got an other understanding for the functionality of the Coccinelle software here
> so far.
>
>
> >                         You match pairs of subsequent locks, but you only
> > mark the second one in the pair.  So you match two pairs:
> >
> > action_lock(&blockage1); and action_lock(&blockage2);
> >
> > and
> >
> > action_lock(&blockage2); and action_lock(&blockage2);
> >
> > and you mark the second one in each case.
>
> It seems that our data processing expectations differ once more.
>
>
> > It would greatly help communication if you would also provide the answer
> > that you expect.
>
> A “shortest path constraint” is mentioned for the usage of the SmPL ellipsis.
> https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/3aa9a6ab3b035e31292be31399b99a8857480aef/docs/manual/cocci_syntax.tex#L1035-1043
>
>
> …>> @display@
> >> expression x, y;
> >> @@
> >>  action_lock(x);
> >>  ... when != action_unlock(x);
> >> *action_lock(y);
>
> May I expect that only a single call should be marked for such a test case?

No, I already explained why two calls are marked.

The shortest path constraint is that for A ... B, the ... doesn't contain
A or B.  It doesn't mean that the rule can't match at multiple places in
the function.

julia

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

>> May I expect that only a single call should be marked for such a test case?
> 
> No, I already explained why two calls are marked.

I see further challenges with this explanation approach.


> The shortest path constraint is that for A ... B, the ... doesn't contain
> A or B.

This is generally fine.


>          It doesn't mean that the rule can't match at multiple places in
> the function.

I find that this information will need further clarifications.

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Julia Lawall]

On Sat, 2 Aug 2025, Markus Elfring wrote:

> >> May I expect that only a single call should be marked for such a test case?
> >
> > No, I already explained why two calls are marked.
>
> I see further challenges with this explanation approach.
>
>
> > The shortest path constraint is that for A ... B, the ... doesn't contain
> > A or B.
>
> This is generally fine.
>
>
> >          It doesn't mean that the rule can't match at multiple places in
> > the function.
>
> I find that this information will need further clarifications.

Coccinelle considers every node in the control-flow graph and checks
whether the pattern can be matched at that point.  Each mach is
independent.  There is no guarantee that one match will not cross another
one.  Furthermore, (just in case this is the concern) when you mentin two
different metavariables, there is no guarantee that they are not bound to
the same term.

julia

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

>>>> May I expect that only a single call should be marked for such a test case?
>>>
>>> No, I already explained why two calls are marked.
>>
>> I see further challenges with this explanation approach.
>>
>>
>>> The shortest path constraint is that for A ... B, the ... doesn't contain
>>> A or B.
>>
>> This is generally fine.

How does the “shortest path” fit to the statement “action_lock(&blockage2);”
from the if branch in your software view?

Can the path distance be determined anyhow?


>>>          It doesn't mean that the rule can't match at multiple places in
>>> the function.
>>
>> I find that this information will need further clarifications.
> 
> Coccinelle considers every node in the control-flow graph and checks
> whether the pattern can be matched at that point.  Each mach is
> independent.  There is no guarantee that one match will not cross another
> one.  Furthermore, (just in case this is the concern) when you mentin two
> different metavariables, there is no guarantee that they are not bound to
> the same term.

I am looking for further clarifications also according to such general information.
How will related technical details be represented in an improved software documentation?

Will it become more desirable to distinguish metavariable contents in an unique way?

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Julia Lawall]

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



On Sat, 2 Aug 2025, Markus Elfring wrote:

> >>>> May I expect that only a single call should be marked for such a test case?
> >>>
> >>> No, I already explained why two calls are marked.
> >>
> >> I see further challenges with this explanation approach.
> >>
> >>
> >>> The shortest path constraint is that for A ... B, the ... doesn't contain
> >>> A or B.
> >>
> >> This is generally fine.
>
> How does the “shortest path” fit to the statement “action_lock(&blockage2);”
> from the if branch in your software view?

I explained it already.  If you have A ... B, Coccinelle doe not allow A
or B to occur in the code matched by ...

A problem that you see to insist on causing is that by using * you have
no idea which matches involve which pieces of code.  If you would print
the line numbers of the involved calls then things would be clear.

>
> Can the path distance be determined anyhow?
>
>
> >>>          It doesn't mean that the rule can't match at multiple places in
> >>> the function.
> >>
> >> I find that this information will need further clarifications.
> >
> > Coccinelle considers every node in the control-flow graph and checks
> > whether the pattern can be matched at that point.  Each mach is
> > independent.  There is no guarantee that one match will not cross another
> > one.  Furthermore, (just in case this is the concern) when you mentin two
> > different metavariables, there is no guarantee that they are not bound to
> > the same term.
>
> I am looking for further clarifications also according to such general information.
> How will related technical details be represented in an improved software documentation?
>
> Will it become more desirable to distinguish metavariable contents in an
> unique way?

If you want something you have to express it in Coccinelle.

foo(A)
...
(
foo(A)
|
*foo(B)
)

ensures that the marked foo(B) involves a different argument than the
matched foo(A).

julia

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

>>>>>> May I expect that only a single call should be marked for such a test case?
>>>>>
>>>>> No, I already explained why two calls are marked.
>>>>
>>>> I see further challenges with this explanation approach.
>>>>
>>>>
>>>>> The shortest path constraint is that for A ... B, the ... doesn't contain
>>>>> A or B.
>>>>
>>>> This is generally fine.
>>
>> How does the “shortest path” fit to the statement “action_lock(&blockage2);”
>> from the if branch in your software view?
> 
> I explained it already.  If you have A ... B, Coccinelle doe not allow A
> or B to occur in the code matched by ...

How does the second lock call fit to these criteria?


> A problem that you see to insist on causing is that by using * you have
> no idea which matches involve which pieces of code.

Partly, yes.

The source code search patterns can occasionally be constructed with more
unique context data.
I hope still that undesirable data processing confusion can be reduced further.


>                                                      If you would print
> the line numbers of the involved calls then things would be clear.

I hope still that a better consensus can be achieved also for safer applications
of the SmPL asterisk functionality.


>> Can the path distance be determined anyhow?

I would appreciate a more helpful answer here.


…>>> independent.  There is no guarantee that one match will not cross another
>>> one.  Furthermore, (just in case this is the concern) when you mentin two
>>> different metavariables, there is no guarantee that they are not bound to
>>> the same term.
…>> Will it become more desirable to distinguish metavariable contents in an
>> unique way?
> 
> If you want something you have to express it in Coccinelle.
> 
> foo(A)
> ...
> (
> foo(A)
> |
> *foo(B)
> )
> 
> ensures that the marked foo(B) involves a different argument than the
> matched foo(A).

Would you like to provide a “guarantee” here?

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Julia Lawall]

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



On Sat, 2 Aug 2025, Markus Elfring wrote:

> >>>>>> May I expect that only a single call should be marked for such a test case?
> >>>>>
> >>>>> No, I already explained why two calls are marked.
> >>>>
> >>>> I see further challenges with this explanation approach.
> >>>>
> >>>>
> >>>>> The shortest path constraint is that for A ... B, the ... doesn't contain
> >>>>> A or B.
> >>>>
> >>>> This is generally fine.
> >>
> >> How does the “shortest path” fit to the statement “action_lock(&blockage2);”
> >> from the if branch in your software view?
> >
> > I explained it already.  If you have A ... B, Coccinelle doe not allow A
> > or B to occur in the code matched by ...
>
> How does the second lock call fit to these criteria?

In the two matches I mentioned earlier there was no intermediate lock
call.

> > A problem that you see to insist on causing is that by using * you have
> > no idea which matches involve which pieces of code.
>
> Partly, yes.
>
> The source code search patterns can occasionally be constructed with more
> unique context data.
> I hope still that undesirable data processing confusion can be reduced further.
>
>
> >                                                      If you would print
> > the line numbers of the involved calls then things would be clear.
>
> I hope still that a better consensus can be achieved also for safer applications
> of the SmPL asterisk functionality.

I have no idea what is considered to be unsafe. In any case, * is only
intended as a convenience.  It works well with emacs to jump to the
affected region of code.  Then you can study it and see what you really
want to do.

>
>
> >> Can the path distance be determined anyhow?
>
> I would appreciate a more helpful answer here.

No idea what this means nor why exact path distance is relevant.  The
point is that there may be some longer paths that start and end with A and
B, but that also contain instances of A and/or B.  By default Coccinelle
doesn't return them.

But * doesn't reflect the result of a single match.  It reflects the
result of all possible matches.  So they can overlap.

>
>
> …>>> independent.  There is no guarantee that one match will not cross another
> >>> one.  Furthermore, (just in case this is the concern) when you mentin two
> >>> different metavariables, there is no guarantee that they are not bound to
> >>> the same term.
> …>> Will it become more desirable to distinguish metavariable contents in an
> >> unique way?
> >
> > If you want something you have to express it in Coccinelle.
> >
> > foo(A)
> > ...
> > (
> > foo(A)
> > |
> > *foo(B)
> > )
> >
> > ensures that the marked foo(B) involves a different argument than the
> > matched foo(A).
>
> Would you like to provide a “guarantee” here?

Sure, it is guaranteed.

julia

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

> In the two matches I mentioned earlier there was no intermediate lock call.

How does this feedback fit to the mentioned SmPL code?


@display@
expression x, y;
@@
 action_lock(x);
 ... when != action_unlock(x);
*action_lock(y);



>> I hope still that a better consensus can be achieved also for safer applications
>> of the SmPL asterisk functionality.
> 
> I have no idea what is considered to be unsafe. In any case, * is only
> intended as a convenience.

This is generally nice.

It seems that presented test results can point disagreements out
which are waiting on more pleasing solutions.


>                             It works well with emacs to jump to the
> affected region of code.  Then you can study it and see what you really
> want to do.

The probability for the presentation of false positives can hopefully
be adjusted better.


>>>> Can the path distance be determined anyhow?
>>
>> I would appreciate a more helpful answer here.
> 
> No idea what this means nor why exact path distance is relevant.

It seems that we represent different development views for the term “shortest path constraint”.


> The point is that there may be some longer paths that start and end with A and
> B, but that also contain instances of A and/or B.  By default Coccinelle
> doesn't return them.
> 
> But * doesn't reflect the result of a single match.  It reflects the
> result of all possible matches.  So they can overlap.

I imagine that this information can trigger data processing confusion.


>> …>>> independent.  There is no guarantee that one match will not cross another
>>>>> one.  Furthermore, (just in case this is the concern) when you mentin two
>>>>> different metavariables, there is no guarantee that they are not bound to
>>>>> the same term.
>> …>> Will it become more desirable to distinguish metavariable contents in an
>>>> unique way?
>>>
>>> If you want something you have to express it in Coccinelle.
>>>
>>> foo(A)
>>> ...
>>> (
>>> foo(A)
>>> |
>>> *foo(B)
>>> )
>>>
>>> ensures that the marked foo(B) involves a different argument than the
>>> matched foo(A).
>>
>> Would you like to provide a “guarantee” here?
> 
> Sure, it is guaranteed.

Does this feedback indicate a contradiction to your previous description?

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

>> How does the “shortest path” fit to the statement “action_lock(&blockage2);”
>> from the if branch in your software view?
> I explained it already.  If you have A ... B, Coccinelle doe not allow A
> or B to occur in the code matched by ...

How many lock calls are close enough for the searched first lock call?

Should the lock call from the if branch be excluded then
because another lock call was found before?

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Julia Lawall]

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



On Sat, 2 Aug 2025, Markus Elfring wrote:

> >> How does the “shortest path” fit to the statement “action_lock(&blockage2);”
> >> from the if branch in your software view?
> > I explained it already.  If you have A ... B, Coccinelle doe not allow A
> > or B to occur in the code matched by ...
>
> How many lock calls are close enough for the searched first lock call?
>
> Should the lock call from the if branch be excluded then
> because another lock call was found before?

No.  The one in the if is matching with the call closest to it, not the
call at the beginning of the function.  There are two matches at two
different places.  Each leads to highlighting a different lock call.

julia

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

>>>> How does the “shortest path” fit to the statement “action_lock(&blockage2);”
>>>> from the if branch in your software view?
>>> I explained it already.  If you have A ... B, Coccinelle doe not allow A
>>> or B to occur in the code matched by ...
>>
>> How many lock calls are close enough for the searched first lock call?
>>
>> Should the lock call from the if branch be excluded then
>> because another lock call was found before?
> 
> No.

I would like to resolve this data processing disagreement somehow.


>      The one in the if is matching with the call closest to it,

I interpret this hit as a false positive.
(The first call lock call in the if branch is not the relevant companion call
from the function implementation.)


>                                                                 not the
> call at the beginning of the function.

This is an essential requirement for the discussed source code search pattern,
isn't it?



>                                         There are two matches at two
> different places.

I would expect that only one match should be appropriate here.


>                    Each leads to highlighting a different lock call.

The source file example “test-action_locks-20250725.c” contains only one lock call combination
with matching expressions, doesn't it?

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Julia Lawall]

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



On Sat, 2 Aug 2025, Markus Elfring wrote:

> >>>> How does the “shortest path” fit to the statement “action_lock(&blockage2);”
> >>>> from the if branch in your software view?
> >>> I explained it already.  If you have A ... B, Coccinelle doe not allow A
> >>> or B to occur in the code matched by ...
> >>
> >> How many lock calls are close enough for the searched first lock call?
> >>
> >> Should the lock call from the if branch be excluded then
> >> because another lock call was found before?
> >
> > No.
>
> I would like to resolve this data processing disagreement somehow.
>
>
> >      The one in the if is matching with the call closest to it,
>
> I interpret this hit as a false positive.
> (The first call lock call in the if branch is not the relevant companion call
> from the function implementation.)
>
>
> >                                                                 not the
> > call at the beginning of the function.
>
> This is an essential requirement for the discussed source code search pattern,
> isn't it?

No.  I don't understand why you think that.

julia


>
>
>
> >                                         There are two matches at two
> > different places.
>
> I would expect that only one match should be appropriate here.
>
>
> >                    Each leads to highlighting a different lock call.
>
> The source file example “test-action_locks-20250725.c” contains only one lock call combination
> with matching expressions, doesn't it?
>
> Regards,
> Markus
>

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

>>>      The one in the if is matching with the call closest to it,
>>
>> I interpret this hit as a false positive.
>> (The first lock call in the if branch is not the relevant companion call
>> from the function implementation.)
>>
>>
>>>                                                                 not the
>>> call at the beginning of the function.
>>
>> This is an essential requirement for the discussed source code search pattern,
>> isn't it?
> 
> No.

I hope still that a better common understanding can be achieved.


>      I don't understand why you think that.

The source code search pattern tries to find a pair of lock calls.
Is the passed expression determined for the metavariable “y” after the second
lock call was found at the beginning of the function implementation?

May these two calls be kept close together also in the desired search result?

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Julia Lawall]

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



On Sat, 2 Aug 2025, Markus Elfring wrote:

> >>>      The one in the if is matching with the call closest to it,
> >>
> >> I interpret this hit as a false positive.
> >> (The first lock call in the if branch is not the relevant companion call
> >> from the function implementation.)
> >>
> >>
> >>>                                                                 not the
> >>> call at the beginning of the function.
> >>
> >> This is an essential requirement for the discussed source code search pattern,
> >> isn't it?
> >
> > No.
>
> I hope still that a better common understanding can be achieved.
>
>
> >      I don't understand why you think that.
>
> The source code search pattern tries to find a pair of lock calls.
> Is the passed expression determined for the metavariable “y” after the second
> lock call was found at the beginning of the function implementation?

I don't understand this at all.  Coccinelle doesn't care about the
beginning of the function, unless you start the pattern with a function
header or a ...

In all cases, Coccinelle looks at every node of the control-flow graph and
tries to match the pattern there.  It doesn't care about beginning middle
or end.

julia

>
> May these two calls be kept close together also in the desired search result?
>
> Regards,
> Markus
>

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

>>>>>      The one in the if is matching with the call closest to it,
>>>>
>>>> I interpret this hit as a false positive.
>>>> (The first lock call in the if branch is not the relevant companion call
>>>> from the function implementation.)
>>>>
>>>>
>>>>>                                                                 not the
>>>>> call at the beginning of the function.
>>>>
>>>> This is an essential requirement for the discussed source code search pattern,
>>>> isn't it?
>>>
>>> No.
>>
>> I hope still that a better common understanding can be achieved.
>>
>>
>>>      I don't understand why you think that.
>>
>> The source code search pattern tries to find a pair of lock calls.
>> Is the passed expression determined for the metavariable “y” after the second
>> lock call was found at the beginning of the function implementation?
> 
> I don't understand this at all.

Does this feedback indicate another communication problem?


>                                  Coccinelle doesn't care about the
> beginning of the function, unless you start the pattern with a function
> header or a ...

Where does the statement “action_lock(&blockage1);” appear in the implementation
of the function “my_action_test”?


> In all cases, Coccinelle looks at every node of the control-flow graph and
> tries to match the pattern there.  It doesn't care about beginning middle
> or end.

But should the analysis tool care more for selected function call combinations?

Would it be possible to determine that special control flow from an if branch
would be inappropriate according to the mentioned SmPL code?

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Julia Lawall]

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



On Sat, 2 Aug 2025, Markus Elfring wrote:

> >>>>>      The one in the if is matching with the call closest to it,
> >>>>
> >>>> I interpret this hit as a false positive.
> >>>> (The first lock call in the if branch is not the relevant companion call
> >>>> from the function implementation.)
> >>>>
> >>>>
> >>>>>                                                                 not the
> >>>>> call at the beginning of the function.
> >>>>
> >>>> This is an essential requirement for the discussed source code search pattern,
> >>>> isn't it?
> >>>
> >>> No.
> >>
> >> I hope still that a better common understanding can be achieved.
> >>
> >>
> >>>      I don't understand why you think that.
> >>
> >> The source code search pattern tries to find a pair of lock calls.
> >> Is the passed expression determined for the metavariable “y” after the second
> >> lock call was found at the beginning of the function implementation?
> >
> > I don't understand this at all.
>
> Does this feedback indicate another communication problem?
>
>
> >                                  Coccinelle doesn't care about the
> > beginning of the function, unless you start the pattern with a function
> > header or a ...
>
> Where does the statement “action_lock(&blockage1);” appear in the implementation
> of the function “my_action_test”?

It is at the beginning of the function.  But that the fact that x matches
&blockage1 n one place doesn't mean that it can't match something else
when checking for a match at another place in the code.  If you hava a
function like

int f() {
  a(1);
  a(2);
  a(3);
}

and your semantic patch is:

@@
expression x;
@@

* a(x);

Then all calls to a will be marked, because the pattern can march in three
different places, with three different bindings of x.

>
>
> > In all cases, Coccinelle looks at every node of the control-flow graph and
> > tries to match the pattern there.  It doesn't care about beginning middle
> > or end.
>
> But should the analysis tool care more for selected function call combinations?
>
> Would it be possible to determine that special control flow from an if branch
> would be inappropriate according to the mentioned SmPL code?

If you don't want a match to go over an if, you have to add the if to the
pattern to specify that.

julia

> Regards,
> Markus
>

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

Am 02.08.25 um 19:38 schrieb Julia Lawall:
> 
> 
> On Sat, 2 Aug 2025, Markus Elfring wrote:
> 
>>>>>>>      The one in the if is matching with the call closest to it,
>>>>>>
>>>>>> I interpret this hit as a false positive.
>>>>>> (The first lock call in the if branch is not the relevant companion call
>>>>>> from the function implementation.)
>>>>>>
>>>>>>
>>>>>>>                                                                 not the
>>>>>>> call at the beginning of the function.
>>>>>>
>>>>>> This is an essential requirement for the discussed source code search pattern,
>>>>>> isn't it?
>>>>>
>>>>> No.
>>>>
>>>> I hope still that a better common understanding can be achieved.
>>>>
>>>>
>>>>>      I don't understand why you think that.
>>>>
>>>> The source code search pattern tries to find a pair of lock calls.
>>>> Is the passed expression determined for the metavariable “y” after the second
>>>> lock call was found at the beginning of the function implementation?
>>>
>>> I don't understand this at all.
>>
>> Does this feedback indicate another communication problem?
>>
>>
>>>                                  Coccinelle doesn't care about the
>>> beginning of the function, unless you start the pattern with a function
>>> header or a ...
>>
>> Where does the statement “action_lock(&blockage1);” appear in the implementation
>> of the function “my_action_test”?
> 
> It is at the beginning of the function.

Thanks for another bit of positive feedback.


>                                          But that the fact that x matches
> &blockage1 n one place doesn't mean that it can't match something else
> when checking for a match at another place in the code.

This technical aspect can be usable for further source code search approaches.


>                                                          If you hava a
> function like
> 
> int f() {
>   a(1);
>   a(2);
>   a(3);
> }
> 
> and your semantic patch is:
> 
> @@
> expression x;
> @@
> 
> * a(x);
> 
> Then all calls to a will be marked, because the pattern can march in three
> different places, with three different bindings of x.

It seems that this software behaviour (according to the functionality “semantic match”)
was not officially documented so far.
https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/3aa9a6ab3b035e31292be31399b99a8857480aef/docs/manual/cocci_syntax.tex#L1214-1225

Would it be cleaner to use the SmPL construct “<+... … ...+>” accordingly?


>> Would it be possible to determine that special control flow from an if branch
>> would be inappropriate according to the mentioned SmPL code?
> 
> If you don't want a match to go over an if,

There are further constraints to consider.


>                                             you have to add the if to the
> pattern to specify that.

I do not like this suggestion.

It should be possible in a simpler way to point source code places out
which start with a selected function call combination.

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Julia Lawall]

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



On Sat, 2 Aug 2025, Markus Elfring wrote:

>
>
> Am 02.08.25 um 19:38 schrieb Julia Lawall:
> >
> >
> > On Sat, 2 Aug 2025, Markus Elfring wrote:
> >
> >>>>>>>      The one in the if is matching with the call closest to it,
> >>>>>>
> >>>>>> I interpret this hit as a false positive.
> >>>>>> (The first lock call in the if branch is not the relevant companion call
> >>>>>> from the function implementation.)
> >>>>>>
> >>>>>>
> >>>>>>>                                                                 not the
> >>>>>>> call at the beginning of the function.
> >>>>>>
> >>>>>> This is an essential requirement for the discussed source code search pattern,
> >>>>>> isn't it?
> >>>>>
> >>>>> No.
> >>>>
> >>>> I hope still that a better common understanding can be achieved.
> >>>>
> >>>>
> >>>>>      I don't understand why you think that.
> >>>>
> >>>> The source code search pattern tries to find a pair of lock calls.
> >>>> Is the passed expression determined for the metavariable “y” after the second
> >>>> lock call was found at the beginning of the function implementation?
> >>>
> >>> I don't understand this at all.
> >>
> >> Does this feedback indicate another communication problem?
> >>
> >>
> >>>                                  Coccinelle doesn't care about the
> >>> beginning of the function, unless you start the pattern with a function
> >>> header or a ...
> >>
> >> Where does the statement “action_lock(&blockage1);” appear in the implementation
> >> of the function “my_action_test”?
> >
> > It is at the beginning of the function.
>
> Thanks for another bit of positive feedback.
>
>
> >                                          But that the fact that x matches
> > &blockage1 n one place doesn't mean that it can't match something else
> > when checking for a match at another place in the code.
>
> This technical aspect can be usable for further source code search approaches.
>
>
> >                                                          If you hava a
> > function like
> >
> > int f() {
> >   a(1);
> >   a(2);
> >   a(3);
> > }
> >
> > and your semantic patch is:
> >
> > @@
> > expression x;
> > @@
> >
> > * a(x);
> >
> > Then all calls to a will be marked, because the pattern can march in three
> > different places, with three different bindings of x.
>
> It seems that this software behaviour (according to the functionality “semantic match”)
> was not officially documented so far.
> https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/3aa9a6ab3b035e31292be31399b99a8857480aef/docs/manual/cocci_syntax.tex#L1214-1225

The cited text seems totally irrelevant.

You do know that

@@
expression x;
@@

- a(x);

would remove all three calls. right?  Why do you expect * to do something
different?

julia

>
> Would it be cleaner to use the SmPL construct “<+... … ...+>” accordingly?
>
>
> >> Would it be possible to determine that special control flow from an if branch
> >> would be inappropriate according to the mentioned SmPL code?
> >
> > If you don't want a match to go over an if,
>
> There are further constraints to consider.
>
>
> >                                             you have to add the if to the
> > pattern to specify that.
>
> I do not like this suggestion.
>
> It should be possible in a simpler way to point source code places out
> which start with a selected function call combination.
>
> Regards,
> Markus
>

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

>> It seems that this software behaviour (according to the functionality “semantic match”)
>> was not officially documented so far.
>> https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/3aa9a6ab3b035e31292be31399b99a8857480aef/docs/manual/cocci_syntax.tex#L1214-1225
> 
> The cited text seems totally irrelevant.

I hope that the SmPL manual is relevant so far for the determination
of known (and mostly desirable) software behaviour.


> You do know that
> 
> @@
> expression x;
> @@
> 
> - a(x);
> 
> would remove all three calls. right?

The software behaviour might be unclear also according to
the modification incidence for this source code transformation.


>                                       Why do you expect * to do something different?

I am trying again to achieve more clarity for better software documentation.


>> It should be possible in a simpler way to point source code places out
>> which start with a selected function call combination.

Which development ideas will evolve for this use case?

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Julia Lawall]

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



On Sat, 2 Aug 2025, Markus Elfring wrote:

> >> It seems that this software behaviour (according to the functionality “semantic match”)
> >> was not officially documented so far.
> >> https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/3aa9a6ab3b035e31292be31399b99a8857480aef/docs/manual/cocci_syntax.tex#L1214-1225
> >
> > The cited text seems totally irrelevant.
>
> I hope that the SmPL manual is relevant so far for the determination
> of known (and mostly desirable) software behaviour.

The cited text describes what happens when a match occurs, It doesn't say
anything about where a match can occur, which is determined in the same
way for all other kinds of matches, except that for ... only the existence
of a path with the property is required by default rather than all paths
being required to have the property.

julia


>
>
> > You do know that
> >
> > @@
> > expression x;
> > @@
> >
> > - a(x);
> >
> > would remove all three calls. right?
>
> The software behaviour might be unclear also according to
> the modification incidence for this source code transformation.
>
>
> >                                       Why do you expect * to do something different?
>
> I am trying again to achieve more clarity for better software documentation.
>
>
> >> It should be possible in a simpler way to point source code places out
> >> which start with a selected function call combination.
>
> Which development ideas will evolve for this use case?
>
> Regards,
> Markus
>

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

>>>> It seems that this software behaviour (according to the functionality “semantic match”)
>>>> was not officially documented so far.
>>>> https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/3aa9a6ab3b035e31292be31399b99a8857480aef/docs/manual/cocci_syntax.tex#L1214-1225
>>>
>>> The cited text seems totally irrelevant.
>>
>> I hope that the SmPL manual is relevant so far for the determination
>> of known (and mostly desirable) software behaviour.
> 
> The cited text describes what happens when a match occurs,

Some information is provided.


>                                                            It doesn't say
> anything about where a match can occur, which is determined in the same
> way for all other kinds of matches, except that for ... only the existence
> of a path with the property is required by default rather than all paths
> being required to have the property.

Are there further clarification opportunities?

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Julia Lawall]

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



On Sat, 2 Aug 2025, Markus Elfring wrote:

> >>>> It seems that this software behaviour (according to the functionality “semantic match”)
> >>>> was not officially documented so far.
> >>>> https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/3aa9a6ab3b035e31292be31399b99a8857480aef/docs/manual/cocci_syntax.tex#L1214-1225
> >>>
> >>> The cited text seems totally irrelevant.
> >>
> >> I hope that the SmPL manual is relevant so far for the determination
> >> of known (and mostly desirable) software behaviour.
> >
> > The cited text describes what happens when a match occurs,
>
> Some information is provided.
>
>
> >                                                            It doesn't say
> > anything about where a match can occur, which is determined in the same
> > way for all other kinds of matches, except that for ... only the existence
> > of a path with the property is required by default rather than all paths
> > being required to have the property.
>
> Are there further clarification opportunities?

The paper from POPL 2009 explains everything.

julia

Re: [cocci] Evolution of software documentation?

[Markus Elfring]

>> Are there further clarification opportunities?
> 
> The paper from POPL 2009 explains everything.

I got an other impression.

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

> You do know that
> 
> @@
> expression x;
> @@
> 
> - a(x);
> 
> would remove all three calls. right?

We tend to adjust all affected source code places.



>                                       Why do you expect * to do something different?

One of the recurring source code analysis tasks can be to point the beginning
of a sequence out.
Thus there are corresponding case distinctions relevant.

* Presenting only the first hit

* Reconsidering subsequent repetitions


Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Julia Lawall]

On Sun, 3 Aug 2025, Markus Elfring wrote:

> > You do know that
> >
> > @@
> > expression x;
> > @@
> >
> > - a(x);
> >
> > would remove all three calls. right?
>
> We tend to adjust all affected source code places.
>
>
>
> >                                       Why do you expect * to do something different?
>
> One of the recurring source code analysis tasks can be to point the beginning
> of a sequence out.
> Thus there are corresponding case distinctions relevant.
>
> * Presenting only the first hit

Which one is th first one?  The first one it finds?  That seems
meaningless.  Coccinelle works bottom up.  It finds all nodes that match
some pattern, then all nodes that are connected to that one, etc.  There
is no notion of first one.

If you mean the first one that appears in the function, I already told you
that you can get that by putting ... at the top of the pattern.  It may
greatly degrade the execution time, though.

julia

>
> * Reconsidering subsequent repetitions
>
>
> Regards,
> Markus
>

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

>> One of the recurring source code analysis tasks can be to point the beginning
>> of a sequence out.
>> Thus there are corresponding case distinctions relevant.
>>
>> * Presenting only the first hit
> 
> Which one is th first one?

We tend to interpret the control flow in one direction ‒ from top to bottom,
don't we?


>                             The first one it finds?

Probably, yes.


>                                                      That seems meaningless.

Development views can evolve further.


>               Coccinelle works bottom up.  It finds all nodes that match
> some pattern, then all nodes that are connected to that one, etc.  There
> is no notion of first one.

Is another general concept helpful here?


> If you mean the first one that appears in the function, I already told you
> that you can get that by putting ... at the top of the pattern.  It may
> greatly degrade the execution time, though.

Thanks for such a reminder.

Sequence beginnings occur at several well-known places.

Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

>               Coccinelle works bottom up.  It finds all nodes that match
> some pattern, then all nodes that are connected to that one, etc.  There
> is no notion of first one.

Do you take care of data processing for sequences also together with
the means of computation tree logic (and linear temporal logic)?

Regards,
Markus

Re: [cocci] Searching for questionable call pairs (with SmPL)?

[Markus Elfring]

> What is the goal of using <+... ...+> ?  The only way you should have
> multiple releases is if there is a double lock error.  If you want to
> search for double lock errors why do it only in the case where there are
> two locks involved?
> 
> If you want to check for lock(a) lock(b) unlock(a) unlock(b), there is no
> need for <+... ...+>.  Furthermore, you need to check that there is no
> unlock of a between the lock(a) and lock(b), likewise no unlock(b) between
> lock(b) and unlock (a).

Would you get into the mood to clarify data processing challenges better
for another source code search pattern (like the following)?


@mark@
expression x;
@@
 action_lock(x);
 <+... when != action_unlock(x);
       when exists
-action_lock(x);
 ...+>


See also a corresponding source file example once more:
https://github.com/coccinelle/coccinelle/issues/404


Questionable test result (by the software combination “Coccinelle 1.3.0” for example):
Markus_Elfring@Sonne:…/Projekte/Coccinelle/Probe> /usr/bin/spatch ../janitor/show_lock_calls_without_unlock4.cocci test-action_locks-20250725.c
[no diff output]


Regards,
Markus

Re: [cocci] Searching for lock calls without unlocking (with SmPL)?

[Markus Elfring]

> @mark@
> expression x;
> @@
>  action_lock(x);
>  <+... when != action_unlock(x);
>        when exists
> -action_lock(x);
>  ...+>

May I expect a similar outcome as it happens for another source code search pattern
(like the following)?


@mark2@
expression x;
@@
 action_lock(x);
 ... when != action_unlock(x);
     when exists
-action_lock(x);


Another test result (by the software combination “Coccinelle 1.3.0” for example):
Markus_Elfring@Sonne:…/Projekte/Coccinelle/Probe> /usr/bin/spatch ../janitor/show_lock_calls_without_unlock5.cocci test-action_locks-20250725.c
…
@@ -8,7 +8,6 @@ void my_action_test(void)
  if (my_surprise(123))
  {
   my_log("surprised!");
-  action_lock(&blockage2);
   my_log("blocked 2 once more");
   result = 99;
   action_unlock(&blockage2);


Regards,
Markus

Re: [cocci] Searching for repeated actions (with SmPL)?

[Markus Elfring]

>> What is the goal of using <+... ...+> ? …

Another source file example:
void my_action_repetition(void)
{
 my_action();
 my_log("once more ...");
 my_action();
 my_log("repeated!");
}


Another SmPL script example:
@mark@
@@
 <+...
-my_action();
 ...+>


Probably expected test result:
Markus_Elfring@Sonne:…/Projekte/Coccinelle/Probe> /usr/bin/spatch ../janitor/show_repeated_actions3.cocci test-repeated_action-20250806.c
…
@@ -1,7 +1,5 @@
 void my_action_repetition(void)
 {
- my_action();
  my_log("once more ...");
- my_action();
  my_log("repeated!");
 }


> Would you get into the mood to clarify data processing challenges better
> for another source code search pattern (like the following)?

Another SmPL script variant:
@mark2@
@@
 my_action();
 <+...
-my_action();
 ...+>


Questionable test result (by the software combination “Coccinelle 1.3.0” for example):
Markus_Elfring@Sonne:…/Projekte/Coccinelle/Probe> /usr/bin/spatch ../janitor/show_repeated_actions6.cocci test-repeated_action-20250806.c
[no diff output]


How will clarification interests evolve further for this issue?

Regards,
Markus