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 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