@@ -118,6 +118,26 @@ predicate heldByCurrentThreadCheck(LockType t, BasicBlock checkblock, BasicBlock
118118 )
119119}
120120
121+ /**
122+ * Holds if there is 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 variableLockStateCheck ( 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
135+ |
136+ conditionBlock .getBasicBlock ( ) = checkblock and
137+ conditionBlock .getTestSuccessor ( false ) = falsesucc
138+ )
139+ }
140+
121141/**
122142 * A control flow path from a locking call in `src` to `b` such that the number of
123143 * locks minus the number of unlocks along the way is positive and equal to `locks`.
@@ -131,8 +151,9 @@ predicate blockIsLocked(LockType t, BasicBlock src, BasicBlock b, int locks) {
131151 // The number of net locks from the `src` block to the predecessor block `pred` is `predlocks`.
132152 blockIsLocked ( t , src , pred , predlocks ) and
133153 // The recursive call ensures that at least one lock is held, so do not consider the false
134- // successor of the `isHeldByCurrentThread()` check.
154+ // successor of the `isHeldByCurrentThread()` check or of `variableLockStateCheck` .
135155 not heldByCurrentThreadCheck ( t , pred , b ) and
156+ not variableLockStateCheck ( t , pred , b ) and
136157 // Count a failed lock as an unlock so the net is zero.
137158 ( if failedLock ( t , pred , b ) then failedlock = 1 else failedlock = 0 ) and
138159 (
0 commit comments