0001 // SPDX-License-Identifier: GPL-2.0-only
0002 /// Find double locks. False positives may occur when some paths cannot
0003 /// occur at execution, due to the values of variables, and when there is
0004 /// an intervening function call that releases the lock.
0005 ///
0006 // Confidence: Moderate
0007 // Copyright: (C) 2010 Nicolas Palix, DIKU.
0008 // Copyright: (C) 2010 Julia Lawall, DIKU.
0009 // Copyright: (C) 2010 Gilles Muller, INRIA/LiP6.
0010 // URL: https://coccinelle.gitlabpages.inria.fr/website
0011 // Comments:
0012 // Options: --no-includes --include-headers
0013
0014 virtual org
0015 virtual report
0016
0017 @locked@
0018 position p1;
0019 expression E1;
0020 position p;
0021 @@
0022
0023 (
0024 mutex_lock@p1
0025 |
0026 mutex_trylock@p1
0027 |
0028 spin_lock@p1
0029 |
0030 spin_trylock@p1
0031 |
0032 read_lock@p1
0033 |
0034 read_trylock@p1
0035 |
0036 write_lock@p1
0037 |
0038 write_trylock@p1
0039 ) (E1@p,...);
0040
0041 @balanced@
0042 position p1 != locked.p1;
0043 position locked.p;
0044 identifier lock,unlock;
0045 expression x <= locked.E1;
0046 expression E,locked.E1;
0047 expression E2;
0048 @@
0049
0050 if (E) {
0051 <+... when != E1
0052 lock(E1@p,...)
0053 ...+>
0054 }
0055 ... when != E1
0056 when != \(x = E2\|&x\)
0057 when forall
0058 if (E) {
0059 <+... when != E1
0060 unlock@p1(E1,...)
0061 ...+>
0062 }
0063
0064 @r depends on !balanced exists@
0065 expression x <= locked.E1;
0066 expression locked.E1;
0067 expression E2;
0068 identifier lock;
0069 position locked.p,p1,p2;
0070 @@
0071
0072 lock@p1 (E1@p,...);
0073 ... when != E1
0074 when != \(x = E2\|&x\)
0075 lock@p2 (E1,...);
0076
0077 @script:python depends on org@
0078 p1 << r.p1;
0079 p2 << r.p2;
0080 lock << r.lock;
0081 @@
0082
0083 cocci.print_main(lock,p1)
0084 cocci.print_secs("second lock",p2)
0085
0086 @script:python depends on report@
0087 p1 << r.p1;
0088 p2 << r.p2;
0089 lock << r.lock;
0090 @@
0091
0092 msg = "second lock on line %s" % (p2[0].line)
0093 coccilib.report.print_report(p1[0],msg)
