Skip to content

Commit

Permalink
Java: add 'variableLockCheck' predicate
Browse files Browse the repository at this point in the history
  • Loading branch information
Jami Cogswell authored and Jami Cogswell committed Feb 28, 2025
1 parent 96f61ac commit 5882526
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 42 deletions.
28 changes: 22 additions & 6 deletions java/ql/src/Likely Bugs/Concurrency/UnreleasedLock.ql
Original file line number Diff line number Diff line change
Expand Up @@ -112,11 +112,26 @@ predicate failedLock(LockType t, BasicBlock lockblock, BasicBlock exblock) {
predicate heldByCurrentThreadCheck(LockType t, BasicBlock checkblock, BasicBlock falsesucc) {
exists(ConditionBlock conditionBlock |
conditionBlock.getCondition() = t.getIsHeldByCurrentThreadAccess()
or
// Assume that a boolean variable condition check that controls an unlock call
// is checking the lock state similar to `isHeldByCurrentThread`.
conditionBlock.getCondition() = any(VarAccess v | v.getType() instanceof BooleanType) and
conditionBlock.controls(t.getUnlockAccess().getBasicBlock(), true)
|
conditionBlock.getBasicBlock() = checkblock and
conditionBlock.getTestSuccessor(false) = falsesucc
)
}

/**
* A variable access in `checkblock` that has `falsesucc` as the false successor.
*
* The variable access must have an assigned value that is a lock access on `t`, and
* the true successor of `checkblock` must contain an unlock access.
*/

Check warning

Code scanning / CodeQL

Predicate QLDoc style. Warning

The QLDoc for a predicate without a result should start with 'Holds'.
predicate variableLockCheck(LockType t, BasicBlock checkblock, BasicBlock falsesucc) {
exists(ConditionBlock conditionBlock, VarAccess v |
v.getType() instanceof BooleanType and
// Ensure that a lock access is assigned to the variable
v.getVariable().getAnAssignedValue() = t.getLockAccess() and
// Ensure that the `true` successor of the condition block contains an unlock access
conditionBlock.getTestSuccessor(true) = t.getUnlockAccess().getBasicBlock() and
conditionBlock.getCondition() = v
|
conditionBlock.getBasicBlock() = checkblock and
conditionBlock.getTestSuccessor(false) = falsesucc
Expand All @@ -136,8 +151,9 @@ predicate blockIsLocked(LockType t, BasicBlock src, BasicBlock b, int locks) {
// The number of net locks from the `src` block to the predecessor block `pred` is `predlocks`.
blockIsLocked(t, src, pred, predlocks) and
// The recursive call ensures that at least one lock is held, so do not consider the false
// successor of the `isHeldByCurrentThread()` check.
// successor of the `isHeldByCurrentThread()` check and of `variableLockCheck`.
not heldByCurrentThreadCheck(t, pred, b) and
not variableLockCheck(t, pred, b) and
// Count a failed lock as an unlock so the net is zero.
(if failedLock(t, pred, b) then failedlock = 1 else failedlock = 0) and
(
Expand Down
38 changes: 2 additions & 36 deletions java/ql/test/query-tests/UnreleasedLock/UnreleasedLock.java
Original file line number Diff line number Diff line change
Expand Up @@ -96,9 +96,7 @@ void good8() {
}
}

// * New testing

void good9() { // * PASSES
void good9() {
boolean locked = mylock.tryLock();
if (!locked) { return; }
try {
Expand All @@ -110,7 +108,7 @@ void good9() { // * PASSES
}
}

void good10() { // ! FAILS
void good10() {
boolean locked = false;
try {
locked = mylock.tryLock();
Expand All @@ -119,38 +117,6 @@ void good10() { // ! FAILS
if (locked) {
mylock.unlock();
}
// else { // * PASSES when add this
// mylock.unlock();
// }
}
}

void good11() { // * PASSES
boolean locked = false;
try {
locked = mylock.tryLock();
if (!locked) { return; }
} finally {
mylock.unlock();
}
}

void good12() { // * PASSES
boolean locked = mylock.tryLock();
if (locked){
try {
f();
} finally {
mylock.unlock();
}
}
}

void good13() { // * PASSES
try {
mylock.lock();
} finally {
mylock.unlock();
}
}
}

0 comments on commit 5882526

Please # to comment.