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