xref: /utopia/UTPA2-700.0.x/projects/build/scripts/coccinelle/locks/double_lock.cocci (revision 53ee8cc121a030b8d368113ac3e966b4705770ef)
1*53ee8cc1Swenshuai.xi/// Find double locks.  False positives may occur when some paths cannot
2*53ee8cc1Swenshuai.xi/// occur at execution, due to the values of variables, and when there is
3*53ee8cc1Swenshuai.xi/// an intervening function call that releases the lock.
4*53ee8cc1Swenshuai.xi///
5*53ee8cc1Swenshuai.xi// Confidence: Moderate
6*53ee8cc1Swenshuai.xi// Copyright: (C) 2010 Nicolas Palix, DIKU.  GPLv2.
7*53ee8cc1Swenshuai.xi// Copyright: (C) 2010 Julia Lawall, DIKU.  GPLv2.
8*53ee8cc1Swenshuai.xi// Copyright: (C) 2010 Gilles Muller, INRIA/LiP6.  GPLv2.
9*53ee8cc1Swenshuai.xi// URL: http://coccinelle.lip6.fr/
10*53ee8cc1Swenshuai.xi// Comments:
11*53ee8cc1Swenshuai.xi// Options: -no_includes -include_headers
12*53ee8cc1Swenshuai.xi
13*53ee8cc1Swenshuai.xivirtual org
14*53ee8cc1Swenshuai.xivirtual report
15*53ee8cc1Swenshuai.xi
16*53ee8cc1Swenshuai.xi@locked@
17*53ee8cc1Swenshuai.xiposition p1;
18*53ee8cc1Swenshuai.xiexpression E1;
19*53ee8cc1Swenshuai.xiposition p;
20*53ee8cc1Swenshuai.xi@@
21*53ee8cc1Swenshuai.xi
22*53ee8cc1Swenshuai.xi(
23*53ee8cc1Swenshuai.ximutex_lock@p1
24*53ee8cc1Swenshuai.xi|
25*53ee8cc1Swenshuai.ximutex_trylock@p1
26*53ee8cc1Swenshuai.xi|
27*53ee8cc1Swenshuai.xispin_lock@p1
28*53ee8cc1Swenshuai.xi|
29*53ee8cc1Swenshuai.xispin_trylock@p1
30*53ee8cc1Swenshuai.xi|
31*53ee8cc1Swenshuai.xiread_lock@p1
32*53ee8cc1Swenshuai.xi|
33*53ee8cc1Swenshuai.xiread_trylock@p1
34*53ee8cc1Swenshuai.xi|
35*53ee8cc1Swenshuai.xiwrite_lock@p1
36*53ee8cc1Swenshuai.xi|
37*53ee8cc1Swenshuai.xiwrite_trylock@p1
38*53ee8cc1Swenshuai.xi) (E1@p,...);
39*53ee8cc1Swenshuai.xi
40*53ee8cc1Swenshuai.xi@balanced@
41*53ee8cc1Swenshuai.xiposition p1 != locked.p1;
42*53ee8cc1Swenshuai.xiposition locked.p;
43*53ee8cc1Swenshuai.xiidentifier lock,unlock;
44*53ee8cc1Swenshuai.xiexpression x <= locked.E1;
45*53ee8cc1Swenshuai.xiexpression E,locked.E1;
46*53ee8cc1Swenshuai.xiexpression E2;
47*53ee8cc1Swenshuai.xi@@
48*53ee8cc1Swenshuai.xi
49*53ee8cc1Swenshuai.xiif (E) {
50*53ee8cc1Swenshuai.xi <+... when != E1
51*53ee8cc1Swenshuai.xi lock(E1@p,...)
52*53ee8cc1Swenshuai.xi ...+>
53*53ee8cc1Swenshuai.xi}
54*53ee8cc1Swenshuai.xi... when != E1
55*53ee8cc1Swenshuai.xi    when != \(x = E2\|&x\)
56*53ee8cc1Swenshuai.xi    when forall
57*53ee8cc1Swenshuai.xiif (E) {
58*53ee8cc1Swenshuai.xi <+... when != E1
59*53ee8cc1Swenshuai.xi unlock@p1(E1,...)
60*53ee8cc1Swenshuai.xi ...+>
61*53ee8cc1Swenshuai.xi}
62*53ee8cc1Swenshuai.xi
63*53ee8cc1Swenshuai.xi@r depends on !balanced exists@
64*53ee8cc1Swenshuai.xiexpression x <= locked.E1;
65*53ee8cc1Swenshuai.xiexpression locked.E1;
66*53ee8cc1Swenshuai.xiexpression E2;
67*53ee8cc1Swenshuai.xiidentifier lock;
68*53ee8cc1Swenshuai.xiposition locked.p,p1,p2;
69*53ee8cc1Swenshuai.xi@@
70*53ee8cc1Swenshuai.xi
71*53ee8cc1Swenshuai.xilock@p1 (E1@p,...);
72*53ee8cc1Swenshuai.xi... when != E1
73*53ee8cc1Swenshuai.xi    when != \(x = E2\|&x\)
74*53ee8cc1Swenshuai.xilock@p2 (E1,...);
75*53ee8cc1Swenshuai.xi
76*53ee8cc1Swenshuai.xi@script:python depends on org@
77*53ee8cc1Swenshuai.xip1 << r.p1;
78*53ee8cc1Swenshuai.xip2 << r.p2;
79*53ee8cc1Swenshuai.xilock << r.lock;
80*53ee8cc1Swenshuai.xi@@
81*53ee8cc1Swenshuai.xi
82*53ee8cc1Swenshuai.xicocci.print_main(lock,p1)
83*53ee8cc1Swenshuai.xicocci.print_secs("second lock",p2)
84*53ee8cc1Swenshuai.xi
85*53ee8cc1Swenshuai.xi@script:python depends on report@
86*53ee8cc1Swenshuai.xip1 << r.p1;
87*53ee8cc1Swenshuai.xip2 << r.p2;
88*53ee8cc1Swenshuai.xilock << r.lock;
89*53ee8cc1Swenshuai.xi@@
90*53ee8cc1Swenshuai.xi
91*53ee8cc1Swenshuai.ximsg = "second lock on line %s" % (p2[0].line)
92*53ee8cc1Swenshuai.xicoccilib.report.print_report(p1[0],msg)
93