@@ -112,11 +112,26 @@ predicate failedLock(LockType t, BasicBlock lockblock, BasicBlock exblock) {
112112predicate heldByCurrentThreadCheck ( LockType t , BasicBlock checkblock , BasicBlock falsesucc ) {
113113 exists ( ConditionBlock conditionBlock |
114114 conditionBlock .getCondition ( ) = t .getIsHeldByCurrentThreadAccess ( )
115- or
116- // Assume that a boolean variable condition check that controls an unlock call
117- // is checking the lock state similar to `isHeldByCurrentThread`.
118- conditionBlock .getCondition ( ) = any ( VarAccess v | v .getType ( ) instanceof BooleanType ) and
119- conditionBlock .controls ( t .getUnlockAccess ( ) .getBasicBlock ( ) , true )
115+ |
116+ conditionBlock .getBasicBlock ( ) = checkblock and
117+ conditionBlock .getTestSuccessor ( false ) = falsesucc
118+ )
119+ }
120+
121+ /**
122+ * A variable access in `checkblock` that has `falsesucc` as the false successor.
123+ *
124+ * The variable access must have an assigned value that is a lock access on `t`, and
125+ * the true successor of `checkblock` must contain an unlock access.
126+ */
127+ predicate variableLockCheck ( LockType t , BasicBlock checkblock , BasicBlock falsesucc ) {
128+ exists ( ConditionBlock conditionBlock , VarAccess v |
129+ v .getType ( ) instanceof BooleanType and
130+ // Ensure that a lock access is assigned to the variable
131+ v .getVariable ( ) .getAnAssignedValue ( ) = t .getLockAccess ( ) and
132+ // Ensure that the `true` successor of the condition block contains an unlock access
133+ conditionBlock .getTestSuccessor ( true ) = t .getUnlockAccess ( ) .getBasicBlock ( ) and
134+ conditionBlock .getCondition ( ) = v
120135 |
121136 conditionBlock .getBasicBlock ( ) = checkblock and
122137 conditionBlock .getTestSuccessor ( false ) = falsesucc
@@ -136,8 +151,9 @@ predicate blockIsLocked(LockType t, BasicBlock src, BasicBlock b, int locks) {
136151 // The number of net locks from the `src` block to the predecessor block `pred` is `predlocks`.
137152 blockIsLocked ( t , src , pred , predlocks ) and
138153 // The recursive call ensures that at least one lock is held, so do not consider the false
139- // successor of the `isHeldByCurrentThread()` check.
154+ // successor of the `isHeldByCurrentThread()` check and of `variableLockCheck` .
140155 not heldByCurrentThreadCheck ( t , pred , b ) and
156+ not variableLockCheck ( t , pred , b ) and
141157 // Count a failed lock as an unlock so the net is zero.
142158 ( if failedLock ( t , pred , b ) then failedlock = 1 else failedlock = 0 ) and
143159 (
0 commit comments