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