Coccinelle Archive on lore.kernel.org
 help / color / mirror / Atom feed
From: Julia Lawall <julia.lawall@inria.fr>
To: Denis Efremov <efremov@ispras.ru>
Cc: Coccinelle <cocci@systeme.lip6.fr>
Subject: Re: [Cocci] How to match a part of a rule expression (documentation)
Date: Wed, 3 Jun 2020 21:45:03 +0200 (CEST)	[thread overview]
Message-ID: <alpine.DEB.2.21.2006032128480.2548@hadrien> (raw)
In-Reply-To: <5149c7dd-2771-e592-c5da-f36cca725a4e@ispras.ru>



On Wed, 3 Jun 2020, Denis Efremov wrote:

> Hi,
>
> I'm trying to write a rule to match consecutive function calls. For example:
> @r@
> expression E, E1;
> @@
>
>   call_func(E);
>   ... when != E = E1
> * call_func(E);
>
> It works well, but not in case "E == p->f" and p is updated in between calls.
> So, I'm to understand how can I avoid these kind of pointers update.
>
> And fail case example:
>
> struct test {
> 	int a;
> };
>
> void call_func(int);
>
> void test(void)
> {
> 	struct test t[10];
> 	struct test *i;
> 	for(i = t; i < i + 10; ++i) {
> 		call_func(i->a);
> 	}
> }
>
>
> While I tried to figure it out, I faced some cocci constructions with no documentation.
> For example, what are rulekinds, "when strict", and "expression *r.E;", "expression E1 <= r.E;"?
>
> 1)
> main_grammar.pdf, page 2:
> rulekind ::= expression
>              identifier
>              type
>
> What is it and how it could be used? I see that it's used in deref_null.cocci, doublebitand.cocci.

Some times it is not clear what kind of term a semantic patch should
match.  For example, if the semantic patch is:

@@
@@

- x
+ y

should f.x be converted to f.y.  Actually, it will not.  By default a
semantic patch rule is parsed as a statement or an expression.  But x in
f.x is an identifier.  So if you really want to replace all the x's by y's
no matter what they are used for, you would put @identifier@ on the first
line of the semantic patch.  Putting expression can avoid some parsing
ambiguities.  I'm not sure that type is actually useful, because
Coccinelle should be able to figure out what is a type by itself, at least
with the typedef declaration.

>
> 2)
> What is "... when strict"? Is it negation of "... when any" and enabled by default?

When strict is unrelated to when any and it is not emabled by default.

In a transformation rule, by default A ... B requires that there is a B
after A on every control-flow path.  But that is not reasonable if between
A and B there is some code that checks for an error condition and if
one is found aborts the function.  So by default the condition of A always
followed by B does not require B on such error paths.  Sometimes, however,
eg for locks and unlocks, you want B to appear in error handling code too.
In that case you would put when strict, to be sure B really appears in all
paths.

When any has to do with the constraint that when you have A ... B you want
the A that is closest to B.  That is the default.  If you put when any,
you get any B that is after A.


> 3) What is "expression *r.E;" in ./null/deref_null.cocci, for example:
> 43:expression *E;
> 54:expression *ifm.E;
> 115:expression *ifm.E;
> 175:expression *ifm.E;
> 239:expression *E;
> 248:expression *ifm1.E;

Any expression that is a pointer.  You can also say expression struct.

> 4) What is "expression  <= " in ./null/deref_null.cocci?
> 53:expression subE <= ifm.E;
> 114:expression subE <= ifm.E;
> 174:expression subE <= ifm.E;
> 247:expression subE <= ifm1.E;

subE is a expressionof whatever expression was previously matched to E in
the rule ifm.  <= can only be used when the metavariable on the right side
is inherited from another rule.  Ths is probably what you want for your
problem.

julia


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

  reply	other threads:[~2020-06-03 19:45 UTC|newest]

Thread overview: 4+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-06-03 17:33 [Cocci] How to match a part of a rule expression (documentation) Denis Efremov
2020-06-03 19:45 ` Julia Lawall [this message]
2020-06-03 22:09   ` Denis Efremov
2020-06-04  7:31     ` Julia Lawall

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=alpine.DEB.2.21.2006032128480.2548@hadrien \
    --to=julia.lawall@inria.fr \
    --cc=cocci@systeme.lip6.fr \
    --cc=efremov@ispras.ru \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox