1*53ee8cc1Swenshuai.xi/// Find double locks. False positives may occur when some paths cannot 2*53ee8cc1Swenshuai.xi/// occur at execution, due to the values of variables, and when there is 3*53ee8cc1Swenshuai.xi/// an intervening function call that releases the lock. 4*53ee8cc1Swenshuai.xi/// 5*53ee8cc1Swenshuai.xi// Confidence: Moderate 6*53ee8cc1Swenshuai.xi// Copyright: (C) 2010 Nicolas Palix, DIKU. GPLv2. 7*53ee8cc1Swenshuai.xi// Copyright: (C) 2010 Julia Lawall, DIKU. GPLv2. 8*53ee8cc1Swenshuai.xi// Copyright: (C) 2010 Gilles Muller, INRIA/LiP6. GPLv2. 9*53ee8cc1Swenshuai.xi// URL: http://coccinelle.lip6.fr/ 10*53ee8cc1Swenshuai.xi// Comments: 11*53ee8cc1Swenshuai.xi// Options: -no_includes -include_headers 12*53ee8cc1Swenshuai.xi 13*53ee8cc1Swenshuai.xivirtual org 14*53ee8cc1Swenshuai.xivirtual report 15*53ee8cc1Swenshuai.xi 16*53ee8cc1Swenshuai.xi@locked@ 17*53ee8cc1Swenshuai.xiposition p1; 18*53ee8cc1Swenshuai.xiexpression E1; 19*53ee8cc1Swenshuai.xiposition p; 20*53ee8cc1Swenshuai.xi@@ 21*53ee8cc1Swenshuai.xi 22*53ee8cc1Swenshuai.xi( 23*53ee8cc1Swenshuai.ximutex_lock@p1 24*53ee8cc1Swenshuai.xi| 25*53ee8cc1Swenshuai.ximutex_trylock@p1 26*53ee8cc1Swenshuai.xi| 27*53ee8cc1Swenshuai.xispin_lock@p1 28*53ee8cc1Swenshuai.xi| 29*53ee8cc1Swenshuai.xispin_trylock@p1 30*53ee8cc1Swenshuai.xi| 31*53ee8cc1Swenshuai.xiread_lock@p1 32*53ee8cc1Swenshuai.xi| 33*53ee8cc1Swenshuai.xiread_trylock@p1 34*53ee8cc1Swenshuai.xi| 35*53ee8cc1Swenshuai.xiwrite_lock@p1 36*53ee8cc1Swenshuai.xi| 37*53ee8cc1Swenshuai.xiwrite_trylock@p1 38*53ee8cc1Swenshuai.xi) (E1@p,...); 39*53ee8cc1Swenshuai.xi 40*53ee8cc1Swenshuai.xi@balanced@ 41*53ee8cc1Swenshuai.xiposition p1 != locked.p1; 42*53ee8cc1Swenshuai.xiposition locked.p; 43*53ee8cc1Swenshuai.xiidentifier lock,unlock; 44*53ee8cc1Swenshuai.xiexpression x <= locked.E1; 45*53ee8cc1Swenshuai.xiexpression E,locked.E1; 46*53ee8cc1Swenshuai.xiexpression E2; 47*53ee8cc1Swenshuai.xi@@ 48*53ee8cc1Swenshuai.xi 49*53ee8cc1Swenshuai.xiif (E) { 50*53ee8cc1Swenshuai.xi <+... when != E1 51*53ee8cc1Swenshuai.xi lock(E1@p,...) 52*53ee8cc1Swenshuai.xi ...+> 53*53ee8cc1Swenshuai.xi} 54*53ee8cc1Swenshuai.xi... when != E1 55*53ee8cc1Swenshuai.xi when != \(x = E2\|&x\) 56*53ee8cc1Swenshuai.xi when forall 57*53ee8cc1Swenshuai.xiif (E) { 58*53ee8cc1Swenshuai.xi <+... when != E1 59*53ee8cc1Swenshuai.xi unlock@p1(E1,...) 60*53ee8cc1Swenshuai.xi ...+> 61*53ee8cc1Swenshuai.xi} 62*53ee8cc1Swenshuai.xi 63*53ee8cc1Swenshuai.xi@r depends on !balanced exists@ 64*53ee8cc1Swenshuai.xiexpression x <= locked.E1; 65*53ee8cc1Swenshuai.xiexpression locked.E1; 66*53ee8cc1Swenshuai.xiexpression E2; 67*53ee8cc1Swenshuai.xiidentifier lock; 68*53ee8cc1Swenshuai.xiposition locked.p,p1,p2; 69*53ee8cc1Swenshuai.xi@@ 70*53ee8cc1Swenshuai.xi 71*53ee8cc1Swenshuai.xilock@p1 (E1@p,...); 72*53ee8cc1Swenshuai.xi... when != E1 73*53ee8cc1Swenshuai.xi when != \(x = E2\|&x\) 74*53ee8cc1Swenshuai.xilock@p2 (E1,...); 75*53ee8cc1Swenshuai.xi 76*53ee8cc1Swenshuai.xi@script:python depends on org@ 77*53ee8cc1Swenshuai.xip1 << r.p1; 78*53ee8cc1Swenshuai.xip2 << r.p2; 79*53ee8cc1Swenshuai.xilock << r.lock; 80*53ee8cc1Swenshuai.xi@@ 81*53ee8cc1Swenshuai.xi 82*53ee8cc1Swenshuai.xicocci.print_main(lock,p1) 83*53ee8cc1Swenshuai.xicocci.print_secs("second lock",p2) 84*53ee8cc1Swenshuai.xi 85*53ee8cc1Swenshuai.xi@script:python depends on report@ 86*53ee8cc1Swenshuai.xip1 << r.p1; 87*53ee8cc1Swenshuai.xip2 << r.p2; 88*53ee8cc1Swenshuai.xilock << r.lock; 89*53ee8cc1Swenshuai.xi@@ 90*53ee8cc1Swenshuai.xi 91*53ee8cc1Swenshuai.ximsg = "second lock on line %s" % (p2[0].line) 92*53ee8cc1Swenshuai.xicoccilib.report.print_report(p1[0],msg) 93