1 // SPDX-License-Identifier: GPL-2.0-only
2 /// Find double locks. False positives may occur when some paths cannot
3 /// occur at execution, due to the values of variables, and when there is
4 /// an intervening function call that releases the lock.
5 ///
6 // Confidence: Moderate
7 // Copyright: (C) 2010 Nicolas Palix, DIKU.
8 // Copyright: (C) 2010 Julia Lawall, DIKU.
9 // Copyright: (C) 2010 Gilles Muller, INRIA/LiP6.
10 // URL: https://coccinelle.gitlabpages.inria.fr/website
11 // Comments:
12 // Options: --no-includes --include-headers
13
14 virtual org
15 virtual report
16
17 @locked@
18 position p1;
19 expression E1;
20 position p;
21 @@
22
23 (
24 mutex_lock@p1
25 |
26 mutex_trylock@p1
27 |
28 spin_lock@p1
29 |
30 spin_trylock@p1
31 |
32 read_lock@p1
33 |
34 read_trylock@p1
35 |
36 write_lock@p1
37 |
38 write_trylock@p1
39 ) (E1@p,...);
40
41 @balanced@
42 position p1 != locked.p1;
43 position locked.p;
44 identifier lock,unlock;
45 expression x <= locked.E1;
46 expression E,locked.E1;
47 expression E2;
48 @@
49
50 if (E) {
51 <+... when != E1
52 lock(E1@p,...)
53 ...+>
54 }
55 ... when != E1
56 when != \(x = E2\|&x\)
57 when forall
58 if (E) {
59 <+... when != E1
60 unlock@p1(E1,...)
61 ...+>
62 }
63
64 @r depends on !balanced exists@
65 expression x <= locked.E1;
66 expression locked.E1;
67 expression E2;
68 identifier lock;
69 position locked.p,p1,p2;
70 @@
71
72 lock@p1 (E1@p,...);
73 ... when != E1
74 when != \(x = E2\|&x\)
75 lock@p2 (E1,...);
76
77 @script:python depends on org@
78 p1 << r.p1;
79 p2 << r.p2;
80 lock << r.lock;
81 @@
82
83 cocci.print_main(lock,p1)
84 cocci.print_secs("second lock",p2)
85
86 @script:python depends on report@
87 p1 << r.p1;
88 p2 << r.p2;
89 lock << r.lock;
90 @@
91
92 msg = "second lock on line %s" % (p2[0].line)
93 coccilib.report.print_report(p1[0],msg)
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.