diff options
Diffstat (limited to 'scripts')
-rw-r--r-- | scripts/coccinelle/locks/double_lock.cocci | 92 |
1 files changed, 92 insertions, 0 deletions
diff --git a/scripts/coccinelle/locks/double_lock.cocci b/scripts/coccinelle/locks/double_lock.cocci new file mode 100644 index 000000000000..63b24e682fad --- /dev/null +++ b/scripts/coccinelle/locks/double_lock.cocci | |||
@@ -0,0 +1,92 @@ | |||
1 | /// Find double locks. False positives may occur when some paths cannot | ||
2 | /// occur at execution, due to the values of variables, and when there is | ||
3 | /// an intervening function call that releases the lock. | ||
4 | /// | ||
5 | // Confidence: Moderate | ||
6 | // Copyright: (C) 2010 Nicolas Palix, DIKU. GPLv2. | ||
7 | // Copyright: (C) 2010 Julia Lawall, DIKU. GPLv2. | ||
8 | // Copyright: (C) 2010 Gilles Muller, INRIA/LiP6. GPLv2. | ||
9 | // URL: http://coccinelle.lip6.fr/ | ||
10 | // Comments: | ||
11 | // Options: -no_includes -include_headers | ||
12 | |||
13 | virtual org | ||
14 | virtual report | ||
15 | |||
16 | @locked@ | ||
17 | position p1; | ||
18 | expression E1; | ||
19 | position p; | ||
20 | @@ | ||
21 | |||
22 | ( | ||
23 | mutex_lock@p1 | ||
24 | | | ||
25 | mutex_trylock@p1 | ||
26 | | | ||
27 | spin_lock@p1 | ||
28 | | | ||
29 | spin_trylock@p1 | ||
30 | | | ||
31 | read_lock@p1 | ||
32 | | | ||
33 | read_trylock@p1 | ||
34 | | | ||
35 | write_lock@p1 | ||
36 | | | ||
37 | write_trylock@p1 | ||
38 | ) (E1@p,...); | ||
39 | |||
40 | @balanced@ | ||
41 | position p1 != locked.p1; | ||
42 | position locked.p; | ||
43 | identifier lock,unlock; | ||
44 | expression x <= locked.E1; | ||
45 | expression E,locked.E1; | ||
46 | expression E2; | ||
47 | @@ | ||
48 | |||
49 | if (E) { | ||
50 | <+... when != E1 | ||
51 | lock(E1@p,...) | ||
52 | ...+> | ||
53 | } | ||
54 | ... when != E1 | ||
55 | when != \(x = E2\|&x\) | ||
56 | when forall | ||
57 | if (E) { | ||
58 | <+... when != E1 | ||
59 | unlock@p1(E1,...) | ||
60 | ...+> | ||
61 | } | ||
62 | |||
63 | @r depends on !balanced exists@ | ||
64 | expression x <= locked.E1; | ||
65 | expression locked.E1; | ||
66 | expression E2; | ||
67 | identifier lock; | ||
68 | position locked.p,p1,p2; | ||
69 | @@ | ||
70 | |||
71 | lock@p1 (E1@p,...); | ||
72 | ... when != E1 | ||
73 | when != \(x = E2\|&x\) | ||
74 | lock@p2 (E1,...); | ||
75 | |||
76 | @script:python depends on org@ | ||
77 | p1 << r.p1; | ||
78 | p2 << r.p2; | ||
79 | lock << r.lock; | ||
80 | @@ | ||
81 | |||
82 | cocci.print_main(lock,p1) | ||
83 | cocci.print_secs("second lock",p2) | ||
84 | |||
85 | @script:python depends on report@ | ||
86 | p1 << r.p1; | ||
87 | p2 << r.p2; | ||
88 | lock << r.lock; | ||
89 | @@ | ||
90 | |||
91 | msg = "second lock on line %s" % (p2[0].line) | ||
92 | coccilib.report.print_report(p1[0],msg) | ||