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