[cocci] [PATCH v4] coccinelle: Extend address test from ifaddr semantic patch to test expressions

[cocci] [PATCH v4] coccinelle: Extend address test from ifaddr semantic patch to test expressions

[Jérémy LEFAURE]

The test of an expression's address does not necessarily represent the
whole condition, it may only be a part of it. Also, an expression's
address is likely to be non-zero in every test expression, not only in
if statements.

This change aims at detecting an address test in more complex conditions
for every test expression.

Signed-off-by: Jérémy Lefaure <jeremy.lefaure@netatmo.com>
---
v3 -> v4: Improve patch subject
v2 -> v3: Apply Julia's suggestion to have a more generic solution + adapt
commit message and file name to this new solution.
v1 -> v2: Moved disjunction on the condition itself instead of being on the
if statements.

 scripts/coccinelle/misc/{ifaddr.cocci => test_addr.cocci} | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)
 rename scripts/coccinelle/misc/{ifaddr.cocci => test_addr.cocci} (94%)

diff --git a/scripts/coccinelle/misc/ifaddr.cocci b/scripts/coccinelle/misc/test_addr.cocci
similarity index 94%
rename from scripts/coccinelle/misc/ifaddr.cocci
rename to scripts/coccinelle/misc/test_addr.cocci
index fc92e8fcbfcb..2d0ec86d1701 100644
--- a/scripts/coccinelle/misc/ifaddr.cocci
+++ b/scripts/coccinelle/misc/test_addr.cocci
@@ -14,12 +14,10 @@ virtual context
 
 @r@
 expression x;
-statement S1,S2;
 position p;
 @@
 
-*if@p (&x)
- S1 else S2
+*&x@p || ...
 
 @script:python depends on org@
 p << r.p;
-- 
2.25.1

Re: [cocci] [PATCH v4] coccinelle: Extend address test from ifaddr semantic patch to test expressions

[Markus Elfring]

> This change aims at detecting an address test in more complex conditions
> for every test expression.
>
> Signed-off-by: Jérémy Lefaure <jeremy.lefaure@netatmo.com>
> ---
> v3 -> v4: Improve patch subject
> v2 -> v3: Apply Julia's suggestion to have a more generic solution + adapt
> commit message and file name to this new solution.
> v1 -> v2: Moved disjunction on the condition itself instead of being on the
> if statements.
>
>  scripts/coccinelle/misc/{ifaddr.cocci => test_addr.cocci} | 4 +---


The affected software components can be improved further, can't they?


Regards,
Markus

Re: [cocci] [PATCH v4] coccinelle: Extend address test from ifaddr semantic patch to test expressions

[Jérémy LEFAURE]

> -*if@p (&x)
> - S1 else S2
> +*&x@p || ...

I did additional tests and this version does not match explicit check
for NULL in if conditions such as `if (&my_var == NULL)`. But it matches
explicit check for non-NULL such as `if (&my_var != NULL)`. I don't know
why the `==` and `!=` cases are different. Do you have any idea Julia?

This limitation could be avoided with an explicit test to NULL in the
semantic patch:
*\(&x@p || ... \| &x == NULL@p || ... \)

Would it be the best solution?

Thank you,
Jérémy

________________________________________
From: Jérémy LEFAURE
Sent: Thursday, June 23, 2022 18:42
To: Julia Lawall; Nicolas Palix
Cc: Markus Elfring; cocci@inria.fr
Subject: [PATCH v4] coccinelle: Extend address test from ifaddr semantic patch to test expressions

The test of an expression's address does not necessarily represent the
whole condition, it may only be a part of it. Also, an expression's
address is likely to be non-zero in every test expression, not only in
if statements.

This change aims at detecting an address test in more complex conditions
for every test expression.

Signed-off-by: Jérémy Lefaure <jeremy.lefaure@netatmo.com>
---
v3 -> v4: Improve patch subject
v2 -> v3: Apply Julia's suggestion to have a more generic solution + adapt
commit message and file name to this new solution.
v1 -> v2: Moved disjunction on the condition itself instead of being on the
if statements.

 scripts/coccinelle/misc/{ifaddr.cocci => test_addr.cocci} | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)
 rename scripts/coccinelle/misc/{ifaddr.cocci => test_addr.cocci} (94%)

diff --git a/scripts/coccinelle/misc/ifaddr.cocci b/scripts/coccinelle/misc/test_addr.cocci
similarity index 94%
rename from scripts/coccinelle/misc/ifaddr.cocci
rename to scripts/coccinelle/misc/test_addr.cocci
index fc92e8fcbfcb..2d0ec86d1701 100644
--- a/scripts/coccinelle/misc/ifaddr.cocci
+++ b/scripts/coccinelle/misc/test_addr.cocci
@@ -14,12 +14,10 @@ virtual context

 @r@
 expression x;
-statement S1,S2;
 position p;
 @@

-*if@p (&x)
- S1 else S2
+*&x@p || ...

 @script:python depends on org@
 p << r.p;
--
2.25.1

Re: [cocci] [PATCH v4] coccinelle: Extend address test from ifaddr semantic patch to test expressions

[Julia Lawall]

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



On Tue, 28 Jun 2022, Jérémy LEFAURE wrote:

> > -*if@p (&x)
> > - S1 else S2
> > +*&x@p || ...
>
> I did additional tests and this version does not match explicit check
> for NULL in if conditions such as `if (&my_var == NULL)`. But it matches
> explicit check for non-NULL such as `if (&my_var != NULL)`. I don't know
> why the `==` and `!=` cases are different. Do you have any idea Julia?
>
> This limitation could be avoided with an explicit test to NULL in the
> semantic patch:
> *\(&x@p || ... \| &x == NULL@p || ... \)

No.  Just put the == NULL case.  The &x case will already be covered by an
isomorphism.  You can see this with spatch --parse-cocci file.cocci

julia

>
> Would it be the best solution?
>
> Thank you,
> Jérémy
>
> ________________________________________
> From: Jérémy LEFAURE
> Sent: Thursday, June 23, 2022 18:42
> To: Julia Lawall; Nicolas Palix
> Cc: Markus Elfring; cocci@inria.fr
> Subject: [PATCH v4] coccinelle: Extend address test from ifaddr semantic patch to test expressions
>
> The test of an expression's address does not necessarily represent the
> whole condition, it may only be a part of it. Also, an expression's
> address is likely to be non-zero in every test expression, not only in
> if statements.
>
> This change aims at detecting an address test in more complex conditions
> for every test expression.
>
> Signed-off-by: Jérémy Lefaure <jeremy.lefaure@netatmo.com>
> ---
> v3 -> v4: Improve patch subject
> v2 -> v3: Apply Julia's suggestion to have a more generic solution + adapt
> commit message and file name to this new solution.
> v1 -> v2: Moved disjunction on the condition itself instead of being on the
> if statements.
>
>  scripts/coccinelle/misc/{ifaddr.cocci => test_addr.cocci} | 4 +---
>  1 file changed, 1 insertion(+), 3 deletions(-)
>  rename scripts/coccinelle/misc/{ifaddr.cocci => test_addr.cocci} (94%)
>
> diff --git a/scripts/coccinelle/misc/ifaddr.cocci b/scripts/coccinelle/misc/test_addr.cocci
> similarity index 94%
> rename from scripts/coccinelle/misc/ifaddr.cocci
> rename to scripts/coccinelle/misc/test_addr.cocci
> index fc92e8fcbfcb..2d0ec86d1701 100644
> --- a/scripts/coccinelle/misc/ifaddr.cocci
> +++ b/scripts/coccinelle/misc/test_addr.cocci
> @@ -14,12 +14,10 @@ virtual context
>
>  @r@
>  expression x;
> -statement S1,S2;
>  position p;
>  @@
>
> -*if@p (&x)
> - S1 else S2
> +*&x@p || ...
>
>  @script:python depends on org@
>  p << r.p;
> --
> 2.25.1
>

Re: [cocci] [PATCH v4] coccinelle: Extend address test from ifaddr semantic patch to test expressions

[Jérémy LEFAURE]

> > This limitation could be avoided with an explicit test to NULL in the
> > semantic patch:
> > *\(&x@p || ... \| &x == NULL@p || ... \)
>
> No.  Just put the == NULL case.  The &x case will already be covered by an
> isomorphism.  You can see this with spatch --parse-cocci file.cocci

I'm not sure to understand what you mean. I tried to have only:
*&x@p == NULL || ...

But it matches only negation of test addresses, something like
`if (&my_var)` is not matched. The --parse-cocci gives this output:

(
*&*x@p  *== *NULL *|| *...
|
*!*&*x@p  *|| *...
|
*NULL *== *&*x@p  *|| *...
)

I get that the &x allows to match the `!= NULL` case thanks to the
isomorphism `X => X != NULL` but I don't get how the `== NULL` case only
could match the test address without negation as the isomorphism is
`X == NULL => !X`.


Thank you for your help,
Jérémy

Re: [cocci] [PATCH v4] coccinelle: Extend address test from ifaddr semantic patch to test expressions

[Julia Lawall]

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



On Tue, 28 Jun 2022, Jérémy LEFAURE wrote:

> > > This limitation could be avoided with an explicit test to NULL in the
> > > semantic patch:
> > > *\(&x@p || ... \| &x == NULL@p || ... \)
> >
> > No.  Just put the == NULL case.  The &x case will already be covered by an
> > isomorphism.  You can see this with spatch --parse-cocci file.cocci
>
> I'm not sure to understand what you mean. I tried to have only:
> *&x@p == NULL || ...
>
> But it matches only negation of test addresses, something like
> `if (&my_var)` is not matched. The --parse-cocci gives this output:
>
> (
> *&*x@p  *== *NULL *|| *...
> |
> *!*&*x@p  *|| *...
> |
> *NULL *== *&*x@p  *|| *...
> )
>
> I get that the &x allows to match the `!= NULL` case thanks to the
> isomorphism `X => X != NULL` but I don't get how the `== NULL` case only
> could match the test address without negation as the isomorphism is
> `X == NULL => !X`.

I think you should have \(&x == NULL \| &x != NULL\)

If you have if (&x) S1 else S2 then it will consider the possibility of
exchanging the branches and negating the test.  But if you just have a
positive test expression by itself, it won't consider the possibility of
changing it into a negative one.

julia

Re: [cocci] [v4] coccinelle: Extend address test from ifaddr semantic patch to test expressions

[Markus Elfring]

>> I get that the &x allows to match the `!= NULL` case thanks to the
>> isomorphism `X => X != NULL` but I don't get how the `== NULL` case only
>> could match the test address without negation as the isomorphism is
>> `X == NULL => !X`.
> I think you should have \(&x == NULL \| &x != NULL\)


Does this suggestion express a questionable contradiction?



> If you have if (&x) S1 else S2 then it will consider the possibility of
> exchanging the branches and negating the test.  But if you just have a
> positive test expression by itself, it won't consider the possibility of
> changing it into a negative one.


How does this response fit to your proposal to reduce a SmPL search pattern?
* https://lore.kernel.org/cocci/alpine.DEB.2.22.394.2206072138160.2960@hadrien/
* https://sympa.inria.fr/sympa/arc/cocci/2022-06/msg00011.html


How do you think about to extend the documentation for the Coccinelle software
another bit also according to the mentioned use case?

Regards,
Markus

Re: [cocci] [v4] coccinelle: Extend address test from ifaddr semantic patch to test expressions

[Markus Elfring]

>> I get that the &x allows to match the `!= NULL` case thanks to the
>> isomorphism `X => X != NULL` but I don't get how the `== NULL` case only
>> could match the test address without negation as the isomorphism is
>> `X == NULL => !X`.
> I think you should have \(&x == NULL \| &x != NULL\)
>
> If you have if (&x) S1 else S2 then it will consider the possibility of
> exchanging the branches and negating the test.  But if you just have a
> positive test expression by itself, it won't consider the possibility of
> changing it into a negative one.


This information can be handled in another constructive way.


Changes are generally context-dependent.
Thus context data are accordingly required also for the usage of structure isomorphisms.
https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/02d51a763c8bcce054e065062e43b9b196840159/standard.iso#L421
https://github.com/coccinelle/coccinelle/blob/19ee1697bf152d37a78a20cefe148775bf4b0e0d/standard.iso#L421

How do you think about to extend the SmPL search pattern
so that more case distinctions will be taken better into account?

Regards,
Markus