[Cocci] Checking redundant variable initialisations with SmPL?

[Cocci] Checking redundant variable initialisations with SmPL?

[Markus Elfring]

Hello,

A patch on a topic like “[next] lkdtm: remove redundant initialization of ret”
caught also my software development attention.
https://lkml.org/lkml/2019/6/14/265
https://lore.kernel.org/patchwork/patch/1088971/
https://lore.kernel.org/lkml/20190614094311.24024-1-colin.king@canonical.com/


I hoped that the following script for the semantic patch language can point
such an update candidate also out.

@display@
binary operator bo;
expression e1, e2, e3;
identifier var, work;
statement is, es;
type t;
@@
*t var = e1;
 ... when != if (var bo e2) is else es
*var =
(      work(...)
|      e3
)


elfring@Sonne:~/Projekte/Linux/next-patched> spatch ~/Projekte/Coccinelle/janitor/show_questionable_variable_initialisation1.cocci drivers/misc/lkdtm/core.c
…
exn while in timeout_function
Fatal error: exception Coccinelle_modules.Common.Impossible(56)


How do you think about the software situation?

Regards,
Markus
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Julia Lawall]

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



On Thu, 20 Jun 2019, Markus Elfring wrote:

> Hello,
>
> A patch on a topic like “[next] lkdtm: remove redundant initialization of ret”
> caught also my software development attention.
> https://lkml.org/lkml/2019/6/14/265
> https://lore.kernel.org/patchwork/patch/1088971/
> https://lore.kernel.org/lkml/20190614094311.24024-1-colin.king@canonical.com/
>
>
> I hoped that the following script for the semantic patch language can point
> such an update candidate also out.
>
> @display@
> binary operator bo;
> expression e1, e2, e3;
> identifier var, work;
> statement is, es;
> type t;
> @@
> *t var = e1;
>  ... when != if (var bo e2) is else es
> *var =
> (      work(...)
> |      e3
> )
>
>
> elfring@Sonne:~/Projekte/Linux/next-patched> spatch ~/Projekte/Coccinelle/janitor/show_questionable_variable_initialisation1.cocci drivers/misc/lkdtm/core.c
> …
> exn while in timeout_function
> Fatal error: exception Coccinelle_modules.Common.Impossible(56)
>
>
> How do you think about the software situation?

This problem is now fixed.  Thank you for the report.

julia

[-- Attachment #2: Type: text/plain, Size: 136 bytes --]

_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Markus Elfring]

>> elfring@Sonne:~/Projekte/Linux/next-patched> spatch ~/Projekte/Coccinelle/janitor/show_questionable_variable_initialisation1.cocci drivers/misc/lkdtm/core.c
>> …
>> exn while in timeout_function
>> Fatal error: exception Coccinelle_modules.Common.Impossible(56)
>>
>>
>> How do you think about the software situation?
>
> This problem is now fixed.

Another aspect was improved also for the Coccinelle software.

The following SmPL script variant can point source code places out for
further considerations.

@display@
binary operator bo;
expression e1, e2, e3, call;
identifier var;
statement is, es;
type t;
@@
*t var = e1;
 ... when != if ( \( var bo e2 \| var \) ) is else es
     when != call(..., var, ...)
     when exists
*var = e3


But it seems that data flow analysis would be needed to exclude remaining
false positives for such a source code search pattern.

Regards,
Markus
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Julia Lawall]

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



On Sat, 22 Jun 2019, Markus Elfring wrote:

> >> elfring@Sonne:~/Projekte/Linux/next-patched> spatch ~/Projekte/Coccinelle/janitor/show_questionable_variable_initialisation1.cocci drivers/misc/lkdtm/core.c
> >> …
> >> exn while in timeout_function
> >> Fatal error: exception Coccinelle_modules.Common.Impossible(56)
> >>
> >>
> >> How do you think about the software situation?
> >
> > This problem is now fixed.
>
> Another aspect was improved also for the Coccinelle software.
>
> The following SmPL script variant can point source code places out for
> further considerations.
>
> @display@
> binary operator bo;
> expression e1, e2, e3, call;
> identifier var;
> statement is, es;
> type t;
> @@
> *t var = e1;
>  ... when != if ( \( var bo e2 \| var \) ) is else es
>      when != call(..., var, ...)
>      when exists
> *var = e3

It could be helpful to replace the last line by:

(
  e3 = <+...var...+>
|
* var = e3
)

In that case, it would also be beneficial to remove the * on the variable
declaration because that will be activated regardless of which branch
matches in the disjunction.

julia

>
>
> But it seems that data flow analysis would be needed to exclude remaining
> false positives for such a source code search pattern.
>
> Regards,
> Markus
>

[-- Attachment #2: Type: text/plain, Size: 136 bytes --]

_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Markus Elfring]

> It could be helpful to replace the last line by:
>
> (
>   e3 = <+...var...+>

Can this SmPL specification make sense as another when constraint?


> |
> * var = e3
> )
>
> In that case, it would also be beneficial to remove the *

I find the asterisk required here


> on the variable declaration

so that a potentially unused value is marked for the discussed
variable initialisation.


> because that will be activated regardless of which branch matches
> in the disjunction.

Will further data flow analysis influence such a view any more?

Regards,
Markus
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Julia Lawall]

On Sat, 22 Jun 2019, Markus Elfring wrote:

> > It could be helpful to replace the last line by:
> >
> > (
> >   e3 = <+...var...+>
>
> Can this SmPL specification make sense as another when constraint?

No.  When is about the code between the code that matches what is before
or after.  If you put when, you will get a false positives for var = var +
1.

>
>
> > |
> > * var = e3
> > )
> >
> > In that case, it would also be beneficial to remove the *
>
> I find the asterisk required here

Yu can do whatever you want, but you will get lotsof false positives if
you keep it.  If you really want a star on the declaration then you need
to make two rules.  The first that finds the positions of the places that
match and the second that only puts a * when there is both a matched
declaration and a matched reinitialization.  But I wold imagine that from
the reinitialization, it would be easy to find the declaration, so it
doesn't seem worth further complicating the rule.

julia
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Markus Elfring]

>>> In that case, it would also be beneficial to remove the *
>>
>> I find the asterisk required here
>
> Yu can do whatever you want, but you will get lotsof false positives if
> you keep it.  If you really want a star on the declaration

I would prefer to use a minus character for the specification
that an unused value should be deleted if corresponding change confidence
can be achieved for the discussed source code analysis pattern
also by the means of the semantic patch language.


> then you need to make two rules.  The first that finds the positions of the places
> that match and the second that only puts a * when there is both a matched
> declaration and a matched reinitialization.  But I wold imagine that from
> the reinitialization, it would be easy to find the declaration, so it
> doesn't seem worth further complicating the rule.

This explanation sounds promising.

Regards,
Markus
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Markus Elfring]

>>> It could be helpful to replace the last line by:
>>>
>>> (
>>>   e3 = <+...var...+>
>>
>> Can this SmPL specification make sense as another when constraint?
>
> No.

I imagine that a few extensions like the following can become safer.

     when != do ds while( \( var bo e3 \| var \) );
     when != switch(var) { ... default: ... }


Unfortunately, the software combination “Coccinelle 1.0.7-00211-geaa13d59 (OCaml 4.07.1)”
does not like such an approach at the moment.

…
minus: parse error:
  File "/home/elfring/Projekte/Coccinelle/janitor/show_questionable_variable_initialisation3.cocci", line 12, column 27, charpos = 295
  around = '...',
…


If I try the specification “when != switch(var) { default: ... }” out,
the information “not supported” is provided.


> When is about the code between the code that matches what is before
> or after.  If you put when, you will get a false positives for var = var + 1.

It seems that more analysis constraints should be taken into account finally.
I find also that it should be ensured then that metavariables like “e3” and “var”
will refer to different source code.

Regards,
Markus
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Markus Elfring]

> Yu can do whatever you want, but you will get lotsof false positives if
> you keep it.  If you really want a star on the declaration then you need
> to make two rules.  The first that finds the positions of the places that
> match and the second that only puts a * when there is both a matched
> declaration and a matched reinitialization.

I hoped that the following SmPL script variant can be another approximation
for the desired solution on the discussed source code search pattern.


@display@
binary operator bo1, bo2;
expression action, e1, e2 != e1, e3, e4, e5;
identifier var;
statement es1, is2, es2, is3, es3;
type t;
@@
(
 t var = e1;
 <+...
 if (...)
 {
    var = e2;
    ...
 }
 else
    es1
 ...+>
 if ( \( var \| var bo1 e3 \) )
    is2
 else
    es2
|
 t var
*      = e1
 ;
 ... when != if ( \( var \| var bo2 e4 \) ) is3 else es3
     when != action(..., var, ...)
     when != switch (var) { default: ... }
     when exists
(
*e5 = <+... var ...+>
|
*var = e5
)
)


But I stumble on the following error message.

elfring@Sonne:~/Projekte/Linux/next-patched> git checkout next-20190620 && spatch drivers/misc/lkdtm/core.c ~/Projekte/Coccinelle/janitor/show_questionable_variable_initialisation5.cocci
…
minus: parse error:
  File "/home/elfring/Projekte/Coccinelle/janitor/show_questionable_variable_initialisation5.cocci", line 36, column 0, charpos = 492
  around = ')',
  whole content = )


I observed then that each of the two main branches in the shown SmPL disjunction
can work as expected. So I wonder even more why the combination can not be parsed
by the software “Coccinelle 1.0.7-00211-geaa13d59 (OCaml 4.07.1)” so far.

Regards,
Markus
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Julia Lawall]

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



On Sun, 23 Jun 2019, Markus Elfring wrote:

> > Yu can do whatever you want, but you will get lotsof false positives if
> > you keep it.  If you really want a star on the declaration then you need
> > to make two rules.  The first that finds the positions of the places that
> > match and the second that only puts a * when there is both a matched
> > declaration and a matched reinitialization.
>
> I hoped that the following SmPL script variant can be another approximation
> for the desired solution on the discussed source code search pattern.
>
>
> @display@
> binary operator bo1, bo2;
> expression action, e1, e2 != e1, e3, e4, e5;
> identifier var;
> statement es1, is2, es2, is3, es3;
> type t;
> @@
> (
>  t var = e1;
>  <+...
>  if (...)
>  {
>     var = e2;
>     ...
>  }
>  else
>     es1
>  ...+>
>  if ( \( var \| var bo1 e3 \) )
>     is2
>  else
>     es2
> |
>  t var
> *      = e1
>  ;
>  ... when != if ( \( var \| var bo2 e4 \) ) is3 else es3
>      when != action(..., var, ...)
>      when != switch (var) { default: ... }
>      when exists
> (
> *e5 = <+... var ...+>
> |
> *var = e5
> )
> )
>
>
> But I stumble on the following error message.
>
> elfring@Sonne:~/Projekte/Linux/next-patched> git checkout next-20190620 && spatch drivers/misc/lkdtm/core.c ~/Projekte/Coccinelle/janitor/show_questionable_variable_initialisation5.cocci
> …
> minus: parse error:
>   File "/home/elfring/Projekte/Coccinelle/janitor/show_questionable_variable_initialisation5.cocci", line 36, column 0, charpos = 492
>   around = ')',
>   whole content = )
>
>
> I observed then that each of the two main branches in the shown SmPL disjunction
> can work as expected. So I wonder even more why the combination can not be parsed
> by the software “Coccinelle 1.0.7-00211-geaa13d59 (OCaml 4.07.1)” so far.

Try

... when any

just before the final ).  In some circumstaces the parser doesn't accept
an expression at the end of a sequence like you have here.

julia

[-- Attachment #2: Type: text/plain, Size: 136 bytes --]

_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Markus Elfring]

> Try
>
> ... when any
>
> just before the final ).  In some circumstaces the parser doesn't accept
> an expression at the end of a sequence like you have here.

Thanks for your quick response.

The addition of such a SmPL ellipsis helps somehow.
But I am still not pleased with the generated transformation result.
So I am curious on how this software clarification will evolve further.

Regards,
Markus
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Julia Lawall]

On Sun, 23 Jun 2019, Markus Elfring wrote:

> > Try
> >
> > ... when any
> >
> > just before the final ).  In some circumstaces the parser doesn't accept
> > an expression at the end of a sequence like you have here.
>
> Thanks for your quick response.
>
> The addition of such a SmPL ellipsis helps somehow.
> But I am still not pleased with the generated transformation result.
> So I am curious on how this software clarification will evolve further.

I am not pleased is not especially descriptive.  If you have a question
about something, provide the semantic patch and the code on which you get
an undesired result.

I believe that you put a * on an assignment with var on the right hand
side, which at least doesn't correspond to my understanding of what you
are trying to do, so perhaps that is the problem.

julia
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Markus Elfring]

Am 23.06.19 um 15:13 schrieb Julia Lawall:
>
>
> On Sun, 23 Jun 2019, Markus Elfring wrote:
>
>>> Try
>>>
>>> ... when any
>>>
>>> just before the final ).  In some circumstaces the parser doesn't accept
>>> an expression at the end of a sequence like you have here.
>>
>> Thanks for your quick response.
>>
>> The addition of such a SmPL ellipsis helps somehow.
>> But I am still not pleased with the generated transformation result.
>> So I am curious on how this software clarification will evolve further.
>
> I am not pleased is not especially descriptive.

Partly, yes.


> If you have a question about something, provide the semantic patch

The discussed SmPL script “variant show_questionable_variable_initialisation5.cocci”
(which is another work in progress):

@display@
binary operator bo1, bo2;
expression action, e1, e2 != e1, e3, e4, e5;
identifier var;
statement es1, is2, es2, is3, es3;
type t;
@@
(
 t var = e1;
 <+...
 if (...)
 {
    var = e2;
    ...
 }
 else
    es1
 ...+>
 if ( \( var \| var bo1 e3 \) )
    is2
 else
    es2
|
 t var
*      = e1
 ;
 ... when != if ( \( var \| var bo2 e4 \) ) is3 else es3
     when != action(..., var, ...)
     when != switch (var) { default: ... }
     when exists
(
*e5 = <+... var ...+>
|
*var = e5
)
 ... when any
)


> and the code on which you get an undesired result.

We have got access to the original source file which is another update candidate.
https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/tree/drivers/misc/lkdtm/core.c?id=4b972a01a7da614b4796475f933094751a295a2f#n386
https://elixir.bootlin.com/linux/v5.2-rc6/source/drivers/misc/lkdtm/core.c#L386


Intermediate test result:

…
@@ -284,8 +284,6 @@ static ssize_t lkdtm_debugfs_entry(struc
 				   const char __user *user_buf,
 				   size_t count, loff_t *off)
 {
-	struct crashpoint *crashpoint = file_inode(f)->i_private;
-	const struct crashtype *crashtype = NULL;
 	char *buf;
 	int err;

@@ -303,13 +301,11 @@ static ssize_t lkdtm_debugfs_entry(struc
 	buf[count] = '\0';
 	strim(buf);

-	crashtype = find_crashtype(buf);
 	free_page((unsigned long)buf);

 	if (!crashtype)
 		return -EINVAL;

-	err = lkdtm_register_cpoint(crashpoint, crashtype);
 	if (err < 0)
 		return err;


> I believe that you put a * on an assignment with var on the right hand side,

I would like to stress the change possibility to delete a value
for a variable initialisation if it would be really unused in the
analysed function implementations.


> which at least doesn't correspond to my understanding of what you
> are trying to do, so perhaps that is the problem.

1. The patch hunk for the function “lkdtm_debugfs_entry” points out
   that the preprocessor symbol “NULL” could be omitted in this case.

2. Now I am missing the proposed deletion of the code “ = -EINVAL”
   for the function “lkdtm_module_init” (according to my SmPL patch attempt).

See also a patch on the topic “[next] lkdtm: remove redundant initialization of ret”:
https://lkml.org/lkml/2019/6/14/265
https://lore.kernel.org/patchwork/patch/1088971/
https://lore.kernel.org/lkml/20190614094311.24024-1-colin.king@canonical.com/


We hope still on software development progress for the issue
“Addition of do-while support for SmPL”.
https://systeme.lip6.fr/pipermail/cocci/2019-April/005786.html
https://lore.kernel.org/cocci/CAAGQS2ujUte9tX4Ai66auP8sy4zkryqEXZkbioy8+hKMvUgmMA@mail.gmail.com/

Regards,
Markus
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Markus Elfring]

> Try
>
> ... when any
>
> just before the final ).  In some circumstaces the parser doesn't accept
> an expression at the end of a sequence like you have here.

Thanks for your quick response.

The addition of such a SmPL ellipsis helps somehow.
But I am still not pleased with the generated transformation result.
So I am curious on how this software clarification will evolve further.

Regards,
Markus
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci

Re: [Cocci] Checking redundant variable initialisations with SmPL?

[Markus Elfring]

> Yu can do whatever you want, but you will get lotsof false positives if
> you keep it.  If you really want a star on the declaration then you need
> to make two rules.  The first that finds the positions of the places that
> match and the second that only puts a * when there is both a matched
> declaration and a matched reinitialization.

I hoped that the following SmPL script variant can be another approximation
for the desired solution on the discussed source code search pattern.


@display@
binary operator bo1, bo2;
expression action, e1, e2 != e1, e3, e4, e5;
identifier var;
statement es1, is2, es2, is3, es3;
type t;
@@
(
 t var = e1;
 <+...
 if (...)
 {
    var = e2;
    ...
 }
 else
    es1
 ...+>
 if ( \( var \| var bo1 e3 \) )
    is2
 else
    es2
|
 t var
*      = e1
 ;
 ... when != if ( \( var \| var bo2 e4 \) ) is3 else es3
     when != action(..., var, ...)
     when != switch (var) { default: ... }
     when exists
(
*e5 = <+... var ...+>
|
*var = e5
)
)


But I stumble on the following error message.

elfring@Sonne:~/Projekte/Linux/next-patched> git checkout next-20190620 && spatch drivers/misc/lkdtm/core.c ~/Projekte/Coccinelle/janitor/show_questionable_variable_initialisation5.cocci
…
minus: parse error:
  File "/home/elfring/Projekte/Coccinelle/janitor/show_questionable_variable_initialisation5.cocci", line 36, column 0, charpos = 492
  around = ')',
  whole content = )


I observed then that each of the two main branches in the shown SmPL disjunction
can work as expected. So I wonder even more why the combination can not be parsed
by the software “Coccinelle 1.0.7-00211-geaa13d59 (OCaml 4.07.1)” so far.

Regards,
Markus
_______________________________________________
Cocci mailing list
Cocci@systeme.lip6.fr
https://systeme.lip6.fr/mailman/listinfo/cocci