@@ -26,18 +26,28 @@ predicate correctlySynchronized(CollectionMember c, Expr access) {
2626 )
2727}
2828
29- ControlFlowNode unlockedReachable ( Callable a ) {
30- result = a .getEntryPoint ( )
29+ predicate firstLockingCallInBlock ( BasicBlock b , int i ) {
30+ i = min ( int j | b .getNode ( j ) .asExpr ( ) instanceof LockingCall )
31+ }
32+
33+ BasicBlock unlockedReachable ( Callable a ) {
34+ result = a .getEntryPoint ( ) .getBasicBlock ( )
3135 or
32- exists ( ControlFlowNode mid | mid = unlockedReachable ( a ) |
33- not mid . asExpr ( ) instanceof LockingCall and
36+ exists ( BasicBlock mid | mid = unlockedReachable ( a ) |
37+ not firstLockingCallInBlock ( mid , _ ) and
3438 result = mid .getASuccessor ( )
3539 )
3640}
3741
3842predicate unlockedCalls ( Callable a , Callable b ) {
39- exists ( Call call |
40- call .getAControlFlowNode ( ) = unlockedReachable ( a ) and
43+ exists ( Call call , BasicBlock callBlock , int j |
44+ call .getControlFlowNode ( ) = callBlock .getNode ( j ) and
45+ callBlock = unlockedReachable ( a ) and
46+ (
47+ exists ( int i | j <= i and firstLockingCallInBlock ( callBlock , i ) )
48+ or
49+ not firstLockingCallInBlock ( callBlock , _)
50+ ) and
4151 call .getARuntimeTarget ( ) = b and
4252 not call .getParent * ( ) instanceof LockStmt
4353 )
0 commit comments