On Thu, 6 Dec 2018, Johannes Thumshirn wrote:
> On 05/12/2018 15:46, Julia Lawall wrote:
> [...]
> >> +@r_patch depends on !context && patch && !org && !report@
> >> +expression E;
> >> +type T;
> >> +@@
> >> +
> >> +(
> >> +- E & ~PAGE_MASK
> >> ++ offset_in_page(E)
> >> +|
> >> +- E & (PAGE_SIZE - 1)
> >> ++ offset_in_page(E)
> >
> > The two lines above should be subsumed by the two lines below. When there
> > is a type metavariable that has no other dependencies, an isomorphism will
> > consider that it is either present or absent.
>
> Oh OK, I'm sorry I'm not really into cocinelle so I guessed it might
> take some iterations.
>
> Do you have an example for this?
Expanation 1:
Coccinelle as a file standard.iso that shows the isomorphisms (rewrite
rules) that may be applied to semantic patches. One of the rules is:
Expression
@ not_ptr1 @
expression *X;
@@
!X => X == NULL
So if you have a pointer typed expression X and you write a transformation
on !X, it will also apply to occurrences of X == NULL in the source code.
In this way, you don't have to write so many variants.
Likewise there is an isomorphism:
Expression
@ drop_cast @
expression E;
pure type T;
@@
(T)E => E
That is, if you have a semantic patch with (T)X, then it will also apply
to code that matches just X, without the cast. The word pure means that
this isomorphism metavariable has to match a semantic patch term that is a
metavariable and this metavariable can't be used elsewhere. If you wrote
- (char)x
Then you would probably not want that to apply without the (char) cast.
But if you have just
- (T)x
for some randome unbound metavariable T, then perhaps you don't case about
the cast to T. If you actually do, then you can put disable drop_cast in
the header of your rule.
Explanation 2:
To see what your semantic patch is really doing, you can run
spatch --parse-cocci sp.cocci
Here is what I get for your patch rule, with some annotations added:
@@
expression E;
type T;
@@
(
-E
>>> offset_in_page(E)
-& -~-PAGE_MASK
|
-~
>>> offset_in_page(E)
-PAGE_MASK -& -E
|
// the following come from
// - E & (PAGE_SIZE - 1)
// + offset_in_page(E)
-E // 1
>>> offset_in_page(E)
-& -(-PAGE_SIZE -- -1-)
|
-E // 2
>>> offset_in_page(E)
-& -PAGE_SIZE -- -1
|
-( // 3
>>> offset_in_page(E)
-PAGE_SIZE -- -1-) -& -E
|
-PAGE_SIZE // 4
>>> offset_in_page(E)
-- -1 -& -E
|
// the following come from:
// - E & ((T)PAGE_SIZE - 1)
// + offset_in_page(E)
-E
>>> offset_in_page(E)
-& -(-(-T -)-PAGE_SIZE -- -1-)
|
-E // same as 1
>>> offset_in_page(E)
-& -(-PAGE_SIZE -- -1-)
|
-E
>>> offset_in_page(E)
-& -(-T -)-PAGE_SIZE -- -1
|
-E // same as 2
>>> offset_in_page(E)
-& -PAGE_SIZE -- -1
|
-(
>>> offset_in_page(E)
-(-T -)-PAGE_SIZE -- -1-) -& -E
|
-( // same as 3
>>> offset_in_page(E)
-PAGE_SIZE -- -1-) -& -E
|
-(
>>> offset_in_page(E)
-T -)-PAGE_SIZE -- -1 -& -E
|
-PAGE_SIZE // same as 4
>>> offset_in_page(E)
-- -1 -& -E
)
So all the transformation generated by
- E & (PAGE_SIZE - 1)
+ offset_in_page(E)
are also generated by
- E & ((T)PAGE_SIZE - 1)
+ offset_in_page(E)
I hope that is helpful.
julia
