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: http://coccinelle.lip6.fr/
11// Comments:
12// Options: --no-includes --include-headers
13
14virtual org
15virtual report
16
17@locked@
18position p1;
19expression E1;
20position p;
21@@
22
23(
24mutex_lock@p1
25|
26mutex_trylock@p1
27|
28spin_lock@p1
29|
30spin_trylock@p1
31|
32read_lock@p1
33|
34read_trylock@p1
35|
36write_lock@p1
37|
38write_trylock@p1
39) (E1@p,...);
40
41@balanced@
42position p1 != locked.p1;
43position locked.p;
44identifier lock,unlock;
45expression x <= locked.E1;
46expression E,locked.E1;
47expression E2;
48@@
49
50if (E) {
51 <+... when != E1
52 lock(E1@p,...)
53 ...+>
54}
55... when != E1
56    when != \(x = E2\|&x\)
57    when forall
58if (E) {
59 <+... when != E1
60 unlock@p1(E1,...)
61 ...+>
62}
63
64@r depends on !balanced exists@
65expression x <= locked.E1;
66expression locked.E1;
67expression E2;
68identifier lock;
69position locked.p,p1,p2;
70@@
71
72lock@p1 (E1@p,...);
73... when != E1
74    when != \(x = E2\|&x\)
75lock@p2 (E1,...);
76
77@script:python depends on org@
78p1 << r.p1;
79p2 << r.p2;
80lock << r.lock;
81@@
82
83cocci.print_main(lock,p1)
84cocci.print_secs("second lock",p2)
85
86@script:python depends on report@
87p1 << r.p1;
88p2 << r.p2;
89lock << r.lock;
90@@
91
92msg = "second lock on line %s" % (p2[0].line)
93coccilib.report.print_report(p1[0],msg)
94