// ****************************************************************************
// Prelude 
// ****************************************************************************

// Note: the order of the rules has some importance. As we don't do a fixpoint,
// changing the order may impact the result. For instance, if we have
//
//  iso1 = x+y <=> y+x   
//  iso2 = i++ <=> i=i+1; 
//
// and if 
//   in SP we have i++; 
//   in C  we have i=1+i;
//
// Does the SP matches the C ? 
//  - Yes if iso2 precedes iso1 in this file, 
//  - No otherwise.

// ****************************************************************************
// Standard C isomorphisms
// ****************************************************************************

// ---------------------------------------------------------------------------
// Spacing (include comments) isomorphisms
// ---------------------------------------------------------------------------
// They are handled at lex time.

// ---------------------------------------------------------------------------
// Dataflow isomorphisms (copy propagation, assignments)
// ---------------------------------------------------------------------------
// They are handled in engine (TODO).

// ---------------------------------------------------------------------------
// Iso-by-absence (optional qualifier, storage, sign, cast) isomorphisms
// ---------------------------------------------------------------------------
// Some of them are handled in cocci_vs_c. Some of them handled here.


// We would like that 
//      chip = (ak4117_t *)snd_magic_kcalloc(ak4117_t, 0, GFP_KERNEL);
//  also matches 
//      X = snd_magic_kcalloc(T, 0, C)
//
// For the moment because the iso is (T) E => E and not <=>, it forces
// us to rewrite the SP as  X = (T) snd_magic_kcalloc(T, 0, C)

Expression
@ drop_cast @
expression E;
pure type T;
@@

// in the following, the space at the beginning of the line is very important!
 (T)E => E

Type
@ add_signed @ 
@@
int => signed int

Type
@ add_int1 @ 
@@
unsigned => unsigned int

Type
@ add_int2 @ 
@@
signed => signed int


// ---------------------------------------------------------------------------
// Field isomorphisms
// ---------------------------------------------------------------------------
// Dereferences


// Those iso were introduced for the 'generic program matching' paper, 
// with sgrep. The idea is that when we want to detect bugs, 
// we want to detect something like  free(X) ... *X  
// meaning that you try to access something that have been freed. 
// But *X is not the only way to deference X, there is also 
// X->fld,  hence those iso. 

// The following don't see like a good idea, because eg fld could be
// instantiated in different ways in different places, meaning that the
// two occurrences of "*E" would not refer to the same thing at all.
// This could be addressed by making E pure, but then I think it would
// have no purpose.

// Expression
// @@
// expression E;
// identifier fld;
// @@
// 
// *E => E->fld
// 
// Expression
// @@
// expression E;
// identifier fld;
// @@
// 
// *E => (E)->fld
// 
// Expression
// @@
// expression E,E1;
// @@
// 
// *E => E[E1]

// ---------------------------------------------------------------------------
// Typedef isomorphisms
// ---------------------------------------------------------------------------
// They are handled in engine.


// ---------------------------------------------------------------------------
// Boolean isomorphisms
// ---------------------------------------------------------------------------

// the space at the beginning of the line is very important!
Expression
@ not_int1 @ 
int X; 
@@
 !X => 0 == X

// the space at the beginning of the line is very important!
Expression
@ not_int2 @ 
int X; 
@@
 !X => X == 0

Expression
@ is_zero @ 
expression X; 
@@
X == 0 <=> 0 == X => !X

Expression
@ isnt_zero @ 
expression X; 
@@
X != 0 <=> 0 != X => X

Expression
@ or_comm @ 
expression X,Y; 
@@
X | Y => Y | X

// ---------------------------------------------------------------------------
// Arithmetic isomorphisms
// ---------------------------------------------------------------------------
//todo: require check side-effect free expression

Expression
@ plus_comm @ 
expression X, Y; 
@@
X + Y => Y + X


// needed in kcalloc CE, where have a -kzalloc(c * sizeof(T), E)
Expression
@ mult_comm @ 
expression X, Y; 
@@
X * Y => Y * X

// ---------------------------------------------------------------------------
// Relational isomorphisms
// ---------------------------------------------------------------------------

Expression
@ gtr_lss @ 
expression X, Y; 
@@
X < Y <=> Y > X

// ---------------------------------------------------------------------------
// Increment isomorphisms
// ---------------------------------------------------------------------------

// equivalences between i++, +=1, etc.
// note: there is an addition in this SP.
Statement
@ inc @ 
identifier i; 
@@
i++; <=> ++i; <=> i+=1; <=> i=i+1;

// I would like to avoid the following rule, but we cant transform a ++i
// in i++ everywhere. We can do it only when the instruction is alone,
// such as when there is not stuff around it (not as in x = i++) That's why in
// the previous iso, we have explicitely force the i++ do be alone with
// the ';'. But unfortunately in the last expression of the for there is
// no ';' so the previous rule cannot be applied, hence this special
// case.

Statement
@ for_inc @ 
expression X, Y; 
statement S; 
identifier i; 
@@
for(X;Y;i++) S <=> for(X;Y;++i) S


// ---------------------------------------------------------------------------
// Pointer isomorphisms
// ---------------------------------------------------------------------------

// the space at the beginning of the line is very important!
Expression
@ not_ptr1 @ 
expression *X; 
@@
 !X => NULL == X

// the space at the beginning of the line is very important!
Expression
@ not_ptr2 @ 
expression *X; 
@@
 !X => X == NULL

Expression
@ is_null @ 
expression X; 
@@
X == NULL <=> NULL == X => !X

Expression
@ isnt_zero @ 
expression X; 
@@
X != NULL <=> NULL != X => X

// pointer arithmetic equivalences


// ---------------------------------------------------------------------------
// Statement isomorphisms
// ---------------------------------------------------------------------------

// ----------------
// If
// ----------------

Statement
@ int_if_test1 @
int X;
statement S1, S2;
@@
if (X) S1 else S2 => if (X != 0) S1 else S2 <=> if (0 != X) S1 else S2

Statement
@ int_if_test2 @
int X;
statement S;
@@
if (X) S => if (X != 0) S <=> if (0 != X) S

Statement
@ ptr_if_test1 @
expression *X;
statement S1, S2;
@@
if (X) S1 else S2 => if (X != NULL) S1 else S2 => if (NULL != X) S1 else S2

Statement
@ ptr_if_test2 @
expression *X;
statement S;
@@
if (X) S => if (X != NULL) S <=> if (NULL != X) S


Statement
@ neg_if @
expression X;
statement S1, S2;
@@
if (X) S1 else S2 <=> if (!X) S2 else S1

Statement
@ drop_else @
expression E;
statement S1;
pure statement S2;
@@

if (E) S1 else S2 => if (E) S1


// if (X) Y else Z <=> X ? Y : Z  sometimes.

// ----------------
// Loops
// ----------------

// ---------------------------------------------------------------------------
// Optional initializers
// ---------------------------------------------------------------------------
Declaration
@ decl_init @
type T;
identifier Z;
@@
T Z; => T Z = ...;

// ---------------------------------------------------------------------------
// Branch (or compound) isomorphisms
// ---------------------------------------------------------------------------
// maybe a cocci patch should require something that looks like what is on
// the left above to occur in a if or while

// could worry that this has to be a simple statement, but this should work
// better as it allows + code on S
Statement
@ braces1 @ 
statement S; 
@@
{ ... S } => S

Statement
@ braces2 @ 
statement S; 
@@
{ ... S ... } => S

Statement
@ braces3 @ 
statement S; 
@@
{ S ... } => S

Statement
@ braces4 @ 
statement S; 
@@
{ S } => S

Statement
@ ret @ 
@@
return ...; => return;


// ---------------------------------------------------------------------------
// Declaration isomorphisms
// ---------------------------------------------------------------------------
// They are handled in engine (TODO) 

// int i,j,k; <=> int i; int j; int k;
 

// ---------------------------------------------------------------------------
// Affectation/initialisation isomorphism
// ---------------------------------------------------------------------------
// 'X = Y'  should also match  'type X = Y';  (TODO)

// ---------------------------------------------------------------------------
// Parenthesis isomorphisms
// ---------------------------------------------------------------------------
//Expression
//@@ expression E; @@
// E => (E)
//// E => ((E))

// todo: isomorphism avec les () around ? cf sizeof 3.
// (E) => E    with some conditions.


// ---------------------------------------------------------------------------
// Pointer/Array isomorphisms
// ---------------------------------------------------------------------------

// pointer arithmetic equivalences
// a + x <=> a[x]

// ---------------------------------------------------------------------------
// Pointer/Field isomorphisms
// ---------------------------------------------------------------------------

Expression
@ ptr_to_array @
expression E1, E2; // was pure, not sure why that's needed, not good for rule27
identifier fld;
@@

E1->fld => E1[E2].fld



TopLevel
@ mkinit @
type T;
context T E;
identifier I;
identifier fld;
expression E1;
@@

E.fld = E1; => T I = { .fld = E1, };

// ---------------------------------------------------------------------------
// more pointer field iso
// ---------------------------------------------------------------------------

// pure means that either the whole field reference expression is dropped,
// or E is context code and has no attached + code
// not really... pure means matches a unitary unplussed metavariable
// but this rule doesn't work anyway

Expression
@ fld_to_ptr @
type T;
pure T E;
pure T *E1;
identifier fld;
@@

E.fld => E1->fld


// ---------------------------------------------------------------------------
// sizeof isomorphisms
// ---------------------------------------------------------------------------

Expression
@ sizeof_parens @
expression E;
@@

sizeof(E) => sizeof E


Expression
@ sizeof_type_expr @
type T;
T E;
@@

sizeof(T) => sizeof(E)


// ****************************************************************************
// gcc specific isomorphisms 
// ****************************************************************************

// likely and unlikely are used to give hints to gcc to improve performance.

Expression
@ unlikely @ 
expression E; 
@@

unlikely(E) => E

Expression
@ likely @ 
expression E; 
@@

likely(E) => E


// ****************************************************************************
// Linux specific isomorphisms 
// ****************************************************************************

// Examples: many functions are equivalent/related, and one SP modifying
// such a function should also modify the equivalent/related one.


// ---------------------------------------------------------------------------
// in rule18, needed ? 
// ---------------------------------------------------------------------------
// (
// -   test_and_set_bit(ev, &bcs->event);
// |
// -   set_bit(ev, &bcs->event);
// |
// -   bcs->event |= 1 << ev; // the only case that is used


// ****************************************************************************
// Everything that is required to be in last position, for ugly reasons ...
// ****************************************************************************