java: fix aliasing FP

reorganise code, adding `LockField`
This commit is contained in:
yoff
2025-10-27 14:30:25 +01:00
parent 531b994819
commit 406e48b3bb
3 changed files with 32 additions and 20 deletions

View File

@@ -184,16 +184,6 @@ module Monitors {
locallySynchronizedOnClass(e, m.(ClassMonitor).getClassType())
}
/** Holds if `localLock` refers to `lock`. */
predicate represents(Field lock, Variable localLock) {
lock.getType() instanceof LockType and
(
localLock = lock
or
localLock.getInitializer() = lock.getAnAccess()
)
}
/** Gets the control flow node that must dominate `e` when `e` is synchronized on a lock. */
ControlFlowNode getNodeToBeDominated(Expr e) {
// If `e` is the LHS of an assignment, use the control flow node for the assignment
@@ -204,15 +194,38 @@ module Monitors {
result = e.getControlFlowNode()
}
/** A field storing a lock. */
class LockField extends Field {
LockField() { this.getType() instanceof LockType }
/** Gets a call to a method locking the lock stored in this field. */
MethodCall getLockCall() {
result.getQualifier() = this.getRepresentative().getAnAccess() and
result = this.getType().(LockType).getLockAccess()
}
/** Gets a call to a method unlocking the lock stored in this field. */
MethodCall getUnlockCall() {
result.getQualifier() = this.getRepresentative().getAnAccess() and
result = this.getType().(LockType).getUnlockAccess()
}
/**
* Gets a variable representing this field.
* It can be the field itself or a local variable initialized to the field.
*/
private Variable getRepresentative() {
result = this
or
result.getInitializer() = this.getAnAccess()
}
}
/** Holds if `e` is synchronized on the `Lock` `lock` by a locking call. */
predicate locallyLockedOn(Expr e, Field lock) {
lock.getType() instanceof LockType and
exists(Variable localLock, MethodCall lockCall, MethodCall unlockCall |
represents(lock, localLock) and
lockCall.getQualifier() = localLock.getAnAccess() and
lockCall = lock.getType().(LockType).getLockAccess() and
unlockCall.getQualifier() = localLock.getAnAccess() and
unlockCall = lock.getType().(LockType).getUnlockAccess()
predicate locallyLockedOn(Expr e, LockField lock) {
exists(MethodCall lockCall, MethodCall unlockCall |
lockCall = lock.getLockCall() and
unlockCall = lock.getUnlockCall()
|
dominates(lockCall.getControlFlowNode(), unlockCall.getControlFlowNode()) and
dominates(lockCall.getControlFlowNode(), getNodeToBeDominated(e)) and

View File

@@ -1,4 +1,3 @@
| examples/Alias.java:16:13:16:13 | y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/Alias.java:16:13:16:13 | y | this expression |
| examples/C.java:14:9:14:14 | this.y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/C.java:14:9:14:14 | this.y | this expression |
| examples/C.java:15:9:15:14 | this.y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/C.java:15:9:15:14 | this.y | this expression |
| examples/C.java:16:9:16:14 | this.y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/C.java:16:9:16:14 | this.y | this expression |

View File

@@ -13,7 +13,7 @@ public class Alias {
final ReentrantLock lock = this.lock;
lock.lock();
try {
y = 42; // $ SPURIOUS: Alert
y = 42;
} finally {
this.lock.unlock();
}