From fe487e8bf0a301fd718c4ffad0704ec5814f0719 Mon Sep 17 00:00:00 2001 From: yoff Date: Mon, 13 Jan 2025 21:46:00 +0100 Subject: [PATCH 01/25] java: add ThreadSafe query (P3) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Raúl Pardo Co-authored-by: SimonJorgensenMancofi Co-authored-by: Bjørnar Haugstad Jåtten --- .../semmle/code/java/ConflictingAccess.qll | 338 ++++++++++++++++++ .../Likely Bugs/Concurrency/ThreadSafe.qhelp | 33 ++ .../src/Likely Bugs/Concurrency/ThreadSafe.ql | 26 ++ .../2025-06-22-query-not-thread-safe.md | 4 + .../ThreadSafe/ThreadSafe.expected | 74 ++++ .../query-tests/ThreadSafe/ThreadSafe.qlref | 2 + .../query-tests/ThreadSafe/examples/App.java | 14 + .../query-tests/ThreadSafe/examples/C.java | 72 ++++ .../examples/FaultyTurnstileExample.java | 40 +++ .../ThreadSafe/examples/FlawedSemaphore.java | 30 ++ .../ThreadSafe/examples/LockCorrect.java | 51 +++ .../ThreadSafe/examples/LockExample.java | 156 ++++++++ .../ThreadSafe/examples/LoopyCallGraph.java | 33 ++ .../ThreadSafe/examples/SyncLstExample.java | 47 +++ .../ThreadSafe/examples/SyncStackExample.java | 39 ++ .../examples/SynchronizedAndLock.java | 21 ++ .../query-tests/ThreadSafe/examples/Test.java | 76 ++++ .../ThreadSafe/examples/Test2.java | 22 ++ .../ThreadSafe/examples/Test3Super.java | 17 + .../ThreadSafe/examples/ThreadSafe.java | 4 + .../ThreadSafe/examples/TurnstileExample.java | 23 ++ 21 files changed, 1122 insertions(+) create mode 100644 java/ql/lib/semmle/code/java/ConflictingAccess.qll create mode 100644 java/ql/src/Likely Bugs/Concurrency/ThreadSafe.qhelp create mode 100644 java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql create mode 100644 java/ql/src/change-notes/2025-06-22-query-not-thread-safe.md create mode 100644 java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected create mode 100644 java/ql/test/query-tests/ThreadSafe/ThreadSafe.qlref create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/App.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/C.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/FaultyTurnstileExample.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/FlawedSemaphore.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/LockCorrect.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/LockExample.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/LoopyCallGraph.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/SyncLstExample.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/SyncStackExample.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/SynchronizedAndLock.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/Test.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/Test2.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/Test3Super.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/ThreadSafe.java create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/TurnstileExample.java diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll new file mode 100644 index 000000000000..0d92438ae0f2 --- /dev/null +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -0,0 +1,338 @@ +/** + * Provides classes and predicates for detecting conflicting accesses in the sense of the Java Memory Model. + */ + +import java +import Concurrency + +/** + * Holds if `t` is the type of a lock. + * Currently a crude test of the type name. + */ +pragma[inline] +predicate isLockType(Type t) { t.getName().matches("%Lock%") } + +/** + * This module provides predicates, chiefly `locallyMonitors`, to check if a given expression is synchronized on a specific monitor. + */ +module Monitors { + /** + * A monitor is any object that is used to synchronize access to a shared resource. + * This includes locks as well as variables used in synchronized blocks (including `this`). + */ + newtype TMonitor = + /** Either a lock or a variable used in a synchronized block. */ + TVariableMonitor(Variable v) { isLockType(v.getType()) or locallySynchronizedOn(_, _, v) } or + /** An instance reference used as a monitor. */ + TInstanceMonitor(RefType thisType) { locallySynchronizedOnThis(_, thisType) } or + /** A class used as a monitor. */ + TClassMonitor(RefType classType) { locallySynchronizedOnClass(_, classType) } + + /** + * A monitor is any object that is used to synchronize access to a shared resource. + * This includes locks as well as variables used in synchronized blocks (including `this`). + */ + class Monitor extends TMonitor { + /** Gets the location of this monitor. */ + abstract Location getLocation(); + + /** Gets a textual representation of this element. */ + string toString() { result = "Monitor" } + } + + /** + * A variable used as a monitor. + * The variable is either a lock or is used in a synchronized block. + * E.g `synchronized (m) { ... }` or `m.lock();` + */ + class VariableMonitor extends Monitor, TVariableMonitor { + Variable v; + + VariableMonitor() { this = TVariableMonitor(v) } + + override Location getLocation() { result = v.getLocation() } + + override string toString() { result = "VariableMonitor(" + v.toString() + ")" } + + /** Gets the variable being used as a monitor. */ + Variable getVariable() { result = v } + } + + /** + * An instance reference used as a monitor. + * Either via `synchronized (this) { ... }` or by marking a non-static method as `synchronized`. + */ + class InstanceMonitor extends Monitor, TInstanceMonitor { + RefType thisType; + + InstanceMonitor() { this = TInstanceMonitor(thisType) } + + override Location getLocation() { result = thisType.getLocation() } + + override string toString() { result = "InstanceMonitor(" + thisType.toString() + ")" } + + /** Gets the instance reference being used as a monitor. */ + RefType getThisType() { result = thisType } + } + + /** + * A class used as a monitor. + * This is achieved by marking a static method as `synchronized`. + */ + class ClassMonitor extends Monitor, TClassMonitor { + RefType classType; + + ClassMonitor() { this = TClassMonitor(classType) } + + override Location getLocation() { result = classType.getLocation() } + + override string toString() { result = "ClassMonitor(" + classType.toString() + ")" } + + /** Gets the class being used as a monitor. */ + RefType getClassType() { result = classType } + } + + /** Holds if the expression `e` is synchronized on the monitor `m`. */ + predicate locallyMonitors(Expr e, Monitor m) { + exists(Variable v | v = m.(VariableMonitor).getVariable() | + locallyLockedOn(e, v) + or + locallySynchronizedOn(e, _, v) + ) + or + locallySynchronizedOnThis(e, m.(InstanceMonitor).getThisType()) + or + locallySynchronizedOnClass(e, m.(ClassMonitor).getClassType()) + } + + /** Holds if `localLock` refers to `lock`. */ + predicate represents(Field lock, Variable localLock) { + isLockType(lock.getType()) and + ( + localLock = lock + or + localLock.getInitializer() = lock.getAnAccess() + ) + } + + /** Holds if `e` is synchronized on the `Lock` `lock` by a locking call. */ + predicate locallyLockedOn(Expr e, Field lock) { + isLockType(lock.getType()) and + exists(Variable localLock, MethodCall lockCall, MethodCall unlockCall | + represents(lock, localLock) and + lockCall.getQualifier() = localLock.getAnAccess() and + lockCall.getMethod().getName() in ["lock", "lockInterruptibly", "tryLock"] and + unlockCall.getQualifier() = localLock.getAnAccess() and + unlockCall.getMethod().getName() = "unlock" + | + dominates(lockCall.getControlFlowNode(), unlockCall.getControlFlowNode()) and + dominates(lockCall.getControlFlowNode(), e.getControlFlowNode()) and + postDominates(unlockCall.getControlFlowNode(), e.getControlFlowNode()) + ) + } +} + +/** Provides predicates, chiefly `isModifying`, to check if a given expression modifies a shared resource. */ +module Modification { + import semmle.code.java.dataflow.FlowSummary + + /** Holds if the field access `a` modifies a shared resource. */ + predicate isModifying(FieldAccess a) { + a.isVarWrite() + or + exists(Call c | c.(MethodCall).getQualifier() = a | isModifyingCall(c)) + or + exists(ArrayAccess aa, Assignment asa | aa.getArray() = a | asa.getDest() = aa) + } + + /** Holds if the call `c` modifies a shared resource. */ + predicate isModifyingCall(Call c) { + exists(SummarizedCallable sc, string output, string prefix | sc.getACall() = c | + sc.propagatesFlow(_, output, _, _) and + prefix = "Argument[this]" and + output.prefix(prefix.length()) = prefix + ) + } +} + +/** Holds if the class is annotated as `@ThreadSafe`. */ +Class annotatedAsThreadSafe() { result.getAnAnnotation().getType().getName() = "ThreadSafe" } + +/** Holds if the type `t` is thread-safe. */ +predicate isThreadSafeType(Type t) { + t.getName().matches(["Atomic%", "Concurrent%"]) + or + t.getName() in [ + "CopyOnWriteArraySet", "BlockingQueue", "ThreadLocal", + // this is a method that returns a thread-safe version of the collection used as parameter + "synchronizedMap", "Executor", "ExecutorService", "CopyOnWriteArrayList", + "LinkedBlockingDeque", "LinkedBlockingQueue", "CompletableFuture" + ] + or + t = annotatedAsThreadSafe() +} + +/** + * A field access that is exposed to potential data races. + * We require the field to be in a class that is annotated as `@ThreadSafe`. + */ +class ExposedFieldAccess extends FieldAccess { + ExposedFieldAccess() { + this.getField() = annotatedAsThreadSafe().getAField() and + not this.getField().isVolatile() and + // field is not a lock + not isLockType(this.getField().getType()) and + // field is not thread-safe + not isThreadSafeType(this.getField().getType()) and + not isThreadSafeType(this.getField().getInitializer().getType()) and + // access is not the initializer of the field + not this.(VarWrite).getASource() = this.getField().getInitializer() and + // access not in a constructor + not this.getEnclosingCallable() = this.getField().getDeclaringType().getAConstructor() and + // not a field on a local variable + not this.getQualifier+().(VarAccess).getVariable() instanceof LocalVariableDecl and + // not the variable mention in a synchronized statement + not this = any(SynchronizedStmt sync).getExpr() + } + + // LHS of assignments are excluded from the control flow graph, + // so we use the control flow node for the assignment itself instead. + override ControlFlowNode getControlFlowNode() { + // this is the LHS of an assignment, use the control flow node for the assignment + exists(Assignment asgn | asgn.getDest() = this | result = asgn.getControlFlowNode()) + or + // this is not the LHS of an assignment, use the default control flow node + not exists(Assignment asgn | asgn.getDest() = this) and + result = super.getControlFlowNode() + } +} + +/** Holds if the location of `a` is strictly before the location of `b`. */ +pragma[inline] +predicate orderedLocations(Location a, Location b) { + a.getStartLine() < b.getStartLine() + or + a.getStartLine() = b.getStartLine() and + a.getStartColumn() < b.getStartColumn() +} + +/** + * A class annotated as `@ThreadSafe`. + * Provides predicates to check for concurrency issues. + */ +class ClassAnnotatedAsThreadSafe extends Class { + ClassAnnotatedAsThreadSafe() { this = annotatedAsThreadSafe() } + + /** Holds if `a` and `b` are conflicting accesses to the same field and not monitored by the same monitor. */ + predicate unsynchronised(ExposedFieldAccess a, ExposedFieldAccess b) { + this.conflicting(a, b) and + this.publicAccess(_, a) and + this.publicAccess(_, b) and + not exists(Monitors::Monitor m | + this.monitors(a, m) and + this.monitors(b, m) + ) + } + + /** Holds if `a` is the earliest write to its field that is unsynchronized with `b`. */ + predicate unsynchronised_normalized(ExposedFieldAccess a, ExposedFieldAccess b) { + this.unsynchronised(a, b) and + // Eliminate double reporting by making `a` the earliest write to this field + // that is unsynchronized with `b`. + not exists(ExposedFieldAccess earlier_a | + earlier_a.getField() = a.getField() and + orderedLocations(earlier_a.getLocation(), a.getLocation()) + | + this.unsynchronised(earlier_a, b) + ) + } + + /** + * Holds if `a` and `b` are unsynchronized and both publicly accessible + * as witnessed by `witness_a` and `witness_b`. + */ + predicate witness(ExposedFieldAccess a, Expr witness_a, ExposedFieldAccess b, Expr witness_b) { + this.unsynchronised_normalized(a, b) and + this.publicAccess(witness_a, a) and + this.publicAccess(witness_b, b) and + // avoid double reporting + not exists(Expr better_witness_a | this.publicAccess(better_witness_a, a) | + orderedLocations(better_witness_a.getLocation(), witness_a.getLocation()) + ) and + not exists(Expr better_witness_b | this.publicAccess(better_witness_b, b) | + orderedLocations(better_witness_b.getLocation(), witness_b.getLocation()) + ) + } + + /** + * Actions `a` and `b` are conflicting iff + * they are field access operations on the same field and + * at least one of them is a write. + */ + predicate conflicting(ExposedFieldAccess a, ExposedFieldAccess b) { + // We allow a = b, since they could be executed on different threads + // We are looking for two operations: + // - on the same non-volatile field + a.getField() = b.getField() and + // - on this class + a.getField() = this.getAField() and + // - where at least one is a write + // wlog we assume that is `a` + // We use a slightly more inclusive definition than simply `a.isVarWrite()` + Modification::isModifying(a) and + // Avoid reporting both `(a, b)` and `(b, a)` by choosing the tuple + // where `a` appears before `b` in the source code. + ( + ( + Modification::isModifying(b) and + a != b + ) + implies + orderedLocations(a.getLocation(), b.getLocation()) + ) + } + + /** Holds if `a` can be reached by a path from a public method, and all such paths are monitored by `monitor`. */ + predicate monitors(ExposedFieldAccess a, Monitors::Monitor monitor) { + forex(Method m | this.providesAccess(m, _, a) and m.isPublic() | + this.monitorsVia(m, a, monitor) + ) + } + + /** Holds if `a` can be reached by a path from a public method and `e` is the expression in that method that stsarts the path. */ + predicate publicAccess(Expr e, ExposedFieldAccess a) { + exists(Method m | m.isPublic() | this.providesAccess(m, e, a)) + } + + /** + * Holds if a call to method `m` can cause an access of `a` and `e` is the expression inside `m` that leads to that access. + * `e` will either be `a` itself or a method call that leads to `a`. + */ + predicate providesAccess(Method m, Expr e, ExposedFieldAccess a) { + m = this.getAMethod() and + ( + a.getEnclosingCallable() = m and + e = a + or + exists(MethodCall c | c.getEnclosingCallable() = m | + this.providesAccess(c.getCallee(), _, a) and + e = c + ) + ) + } + + /** Holds if all paths from `m` to `a` are monitored by `monitor`. */ + predicate monitorsVia(Method m, ExposedFieldAccess a, Monitors::Monitor monitor) { + m = this.getAMethod() and + this.providesAccess(m, _, a) and + (a.getEnclosingCallable() = m implies Monitors::locallyMonitors(a, monitor)) and + forall(MethodCall c | + c.getEnclosingCallable() = m and + this.providesAccess(c.getCallee(), _, a) + | + Monitors::locallyMonitors(c, monitor) + or + this.monitorsVia(c.getCallee(), a, monitor) + ) + } +} diff --git a/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.qhelp b/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.qhelp new file mode 100644 index 000000000000..cafcb3cdd799 --- /dev/null +++ b/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.qhelp @@ -0,0 +1,33 @@ + + + + + +

+In a thread-safe class, all field accesses that can be caused by calls to public methods must be properly synchronized.

+ + + + +

+Protect the field access with a lock. Alternatively mark the field as volatile if the write operation is atomic. You can also choose to use a data type that guarantees atomic access. If the field is immutable, mark it as final.

+ + + + + + +
  • + Java Language Specification, chapter 17: + Threads and Locks. +
    • +
  • + Java concurrency package: + java.util.concurrent. +
    • + + +     +     diff --git a/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql b/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql new file mode 100644 index 000000000000..1498274131e1 --- /dev/null +++ b/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql @@ -0,0 +1,26 @@ +/** + * @name Not thread-safe + * @description This class is not thread-safe. It is annotated as `@ThreadSafe`, but it has a + * conflicting access to a field that is not synchronized with the same monitor. + * @kind problem + * @problem.severity warning + * @precision high + * @id java/not-threadsafe + * @tags quality + * reliability + * concurrency + */ + +import java +import semmle.code.java.ConflictingAccess + +from + ClassAnnotatedAsThreadSafe cls, FieldAccess modifyingAccess, Expr witness_modifyingAccess, + FieldAccess conflictingAccess, Expr witness_conflictingAccess +where + cls.witness(modifyingAccess, witness_modifyingAccess, conflictingAccess, witness_conflictingAccess) +select modifyingAccess, + "This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor.", + witness_modifyingAccess, "this expression", conflictingAccess, "this field access", + witness_conflictingAccess, "this expression" +// select c, a.getField() diff --git a/java/ql/src/change-notes/2025-06-22-query-not-thread-safe.md b/java/ql/src/change-notes/2025-06-22-query-not-thread-safe.md new file mode 100644 index 000000000000..d5dd07446097 --- /dev/null +++ b/java/ql/src/change-notes/2025-06-22-query-not-thread-safe.md @@ -0,0 +1,4 @@ +--- +category: newQuery +--- +* Added a new query, `java/not-threadsafe`, to detect data races in classes marked as `@ThreadSafe`. \ No newline at end of file diff --git a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected new file mode 100644 index 000000000000..72d0bbb1a3a3 --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected @@ -0,0 +1,74 @@ +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:14:9:14:14 | this.y | this field access | examples/C.java:14:9:14:14 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:15:9:15:14 | this.y | this field access | examples/C.java:15:9:15:14 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:16:9:16:14 | this.y | this field access | examples/C.java:16:9:16:14 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:16:18:16:23 | this.y | this field access | examples/C.java:16:18:16:23 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:20:9:20:14 | this.y | this field access | examples/C.java:20:9:20:14 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:21:9:21:14 | this.y | this field access | examples/C.java:21:9:21:14 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:22:9:22:14 | this.y | this field access | examples/C.java:22:9:22:14 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:22:18:22:23 | this.y | this field access | examples/C.java:22:18:22:23 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:26:9:26:14 | this.y | this field access | examples/C.java:26:9:26:14 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:30:13:30:13 | y | this field access | examples/C.java:30:13:30:13 | y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:33:9:33:9 | y | this field access | examples/C.java:33:9:33:9 | y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:39:9:39:14 | this.y | this field access | examples/C.java:39:9:39:14 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:40:9:40:14 | this.y | this field access | examples/C.java:40:9:40:14 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:41:9:41:14 | this.y | this field access | examples/C.java:41:9:41:14 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:41:18:41:23 | this.y | this field access | examples/C.java:41:18:41:23 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:53:9:53:14 | this.y | this field access | examples/C.java:53:9:53:14 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:54:9:54:14 | this.y | this field access | examples/C.java:54:9:54:14 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:55:9:55:14 | this.y | this field access | examples/C.java:55:9:55:14 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:55:18:55:23 | this.y | this field access | examples/C.java:55:18:55:23 | this.y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:61:9:61:9 | y | this field access | examples/C.java:61:9:61:9 | y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:62:9:62:9 | y | this field access | examples/C.java:62:9:62:9 | y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:63:9:63:9 | y | this field access | examples/C.java:63:9:63:9 | y | this expression | +| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:63:13:63:13 | y | this field access | examples/C.java:63:13:63:13 | y | this expression | +| examples/FaultyTurnstileExample.java:13:5:13:9 | count | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/FaultyTurnstileExample.java:13:5:13:9 | count | this expression | examples/FaultyTurnstileExample.java:18:5:18:9 | count | this field access | examples/FaultyTurnstileExample.java:18:5:18:9 | count | this expression | +| examples/FaultyTurnstileExample.java:30:5:30:9 | count | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/FaultyTurnstileExample.java:30:5:30:9 | count | this expression | examples/FaultyTurnstileExample.java:36:5:36:9 | count | this field access | examples/FaultyTurnstileExample.java:36:5:36:9 | count | this expression | +| examples/FlawedSemaphore.java:18:7:18:11 | state | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression | examples/FlawedSemaphore.java:15:14:15:18 | state | this field access | examples/FlawedSemaphore.java:15:14:15:18 | state | this expression | +| examples/FlawedSemaphore.java:18:7:18:11 | state | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression | examples/FlawedSemaphore.java:18:7:18:11 | state | this field access | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression | +| examples/FlawedSemaphore.java:18:7:18:11 | state | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression | examples/FlawedSemaphore.java:26:7:26:11 | state | this field access | examples/FlawedSemaphore.java:26:7:26:11 | state | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:38:5:38:10 | length | this field access | examples/LockExample.java:38:5:38:10 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:39:13:39:18 | length | this field access | examples/LockExample.java:39:13:39:18 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:44:5:44:10 | length | this field access | examples/LockExample.java:44:5:44:10 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:45:13:45:18 | length | this field access | examples/LockExample.java:45:13:45:18 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:49:5:49:10 | length | this field access | examples/LockExample.java:49:5:49:10 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:57:5:57:10 | length | this field access | examples/LockExample.java:57:5:57:10 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:58:13:58:18 | length | this field access | examples/LockExample.java:58:13:58:18 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:62:5:62:10 | length | this field access | examples/LockExample.java:62:5:62:10 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:65:13:65:18 | length | this field access | examples/LockExample.java:65:13:65:18 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:69:5:69:10 | length | this field access | examples/LockExample.java:69:5:69:10 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:71:13:71:18 | length | this field access | examples/LockExample.java:71:13:71:18 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:76:5:76:10 | length | this field access | examples/LockExample.java:76:5:76:10 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:79:13:79:18 | length | this field access | examples/LockExample.java:79:13:79:18 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:127:7:127:12 | length | this field access | examples/LockExample.java:127:7:127:12 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:136:7:136:12 | length | this field access | examples/LockExample.java:136:7:136:12 | length | this expression | +| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:142:7:142:12 | length | this field access | examples/LockExample.java:142:7:142:12 | length | this expression | +| examples/LockExample.java:25:5:25:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:25:5:25:11 | content | this expression | examples/LockExample.java:39:5:39:11 | content | this field access | examples/LockExample.java:39:5:39:11 | content | this expression | +| examples/LockExample.java:25:5:25:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:25:5:25:11 | content | this expression | examples/LockExample.java:45:5:45:11 | content | this field access | examples/LockExample.java:45:5:45:11 | content | this expression | +| examples/LockExample.java:25:5:25:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:25:5:25:11 | content | this expression | examples/LockExample.java:58:5:58:11 | content | this field access | examples/LockExample.java:58:5:58:11 | content | this expression | +| examples/LockExample.java:25:5:25:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:25:5:25:11 | content | this expression | examples/LockExample.java:65:5:65:11 | content | this field access | examples/LockExample.java:65:5:65:11 | content | this expression | +| examples/LockExample.java:25:5:25:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:25:5:25:11 | content | this expression | examples/LockExample.java:71:5:71:11 | content | this field access | examples/LockExample.java:71:5:71:11 | content | this expression | +| examples/LockExample.java:25:5:25:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:25:5:25:11 | content | this expression | examples/LockExample.java:79:5:79:11 | content | this field access | examples/LockExample.java:79:5:79:11 | content | this expression | +| examples/LockExample.java:38:5:38:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:38:5:38:10 | length | this expression | examples/LockExample.java:25:13:25:18 | length | this field access | examples/LockExample.java:25:13:25:18 | length | this expression | +| examples/LockExample.java:38:5:38:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:38:5:38:10 | length | this expression | examples/LockExample.java:32:13:32:18 | length | this field access | examples/LockExample.java:32:13:32:18 | length | this expression | +| examples/LockExample.java:38:5:38:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:38:5:38:10 | length | this expression | examples/LockExample.java:52:13:52:18 | length | this field access | examples/LockExample.java:52:13:52:18 | length | this expression | +| examples/LockExample.java:38:5:38:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:38:5:38:10 | length | this expression | examples/LockExample.java:150:7:150:12 | length | this field access | examples/LockExample.java:150:7:150:12 | length | this expression | +| examples/LockExample.java:39:5:39:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:39:5:39:11 | content | this expression | examples/LockExample.java:52:5:52:11 | content | this field access | examples/LockExample.java:52:5:52:11 | content | this expression | +| examples/LockExample.java:85:5:85:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this field access | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression | +| examples/LockExample.java:85:5:85:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:112:5:112:21 | notRelatedToOther | this field access | examples/LockExample.java:112:5:112:21 | notRelatedToOther | this expression | +| examples/LockExample.java:85:5:85:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:119:5:119:21 | notRelatedToOther | this field access | examples/LockExample.java:119:5:119:21 | notRelatedToOther | this expression | +| examples/LockExample.java:85:5:85:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:124:5:124:21 | notRelatedToOther | this field access | examples/LockExample.java:124:5:124:21 | notRelatedToOther | this expression | +| examples/LockExample.java:85:5:85:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:145:5:145:21 | notRelatedToOther | this field access | examples/LockExample.java:145:5:145:21 | notRelatedToOther | this expression | +| examples/LockExample.java:85:5:85:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:153:5:153:21 | notRelatedToOther | this field access | examples/LockExample.java:153:5:153:21 | notRelatedToOther | this expression | +| examples/LockExample.java:94:5:94:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression | examples/LockExample.java:100:5:100:21 | notRelatedToOther | this field access | examples/LockExample.java:100:5:100:21 | notRelatedToOther | this expression | +| examples/LockExample.java:94:5:94:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression | examples/LockExample.java:103:5:103:21 | notRelatedToOther | this field access | examples/LockExample.java:103:5:103:21 | notRelatedToOther | this expression | +| examples/LockExample.java:94:5:94:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression | examples/LockExample.java:109:5:109:21 | notRelatedToOther | this field access | examples/LockExample.java:109:5:109:21 | notRelatedToOther | this expression | +| examples/LockExample.java:94:5:94:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression | examples/LockExample.java:117:5:117:21 | notRelatedToOther | this field access | examples/LockExample.java:117:5:117:21 | notRelatedToOther | this expression | +| examples/LoopyCallGraph.java:25:5:25:9 | count | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LoopyCallGraph.java:15:7:15:16 | increase(...) | this expression | examples/LoopyCallGraph.java:25:5:25:9 | count | this field access | examples/LoopyCallGraph.java:15:7:15:16 | increase(...) | this expression | +| examples/LoopyCallGraph.java:25:5:25:9 | count | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LoopyCallGraph.java:15:7:15:16 | increase(...) | this expression | examples/LoopyCallGraph.java:31:5:31:9 | count | this field access | examples/LoopyCallGraph.java:15:7:15:16 | increase(...) | this expression | +| examples/SyncLstExample.java:40:5:40:7 | lst | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/SyncLstExample.java:40:5:40:7 | lst | this expression | examples/SyncLstExample.java:45:5:45:7 | lst | this field access | examples/SyncLstExample.java:45:5:45:7 | lst | this expression | +| examples/SyncStackExample.java:32:5:32:7 | stc | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/SyncStackExample.java:32:5:32:7 | stc | this expression | examples/SyncStackExample.java:37:5:37:7 | stc | this field access | examples/SyncStackExample.java:37:5:37:7 | stc | this expression | +| examples/SynchronizedAndLock.java:14:9:14:14 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/SynchronizedAndLock.java:14:9:14:14 | length | this expression | examples/SynchronizedAndLock.java:19:9:19:14 | length | this field access | examples/SynchronizedAndLock.java:19:9:19:14 | length | this expression | +| examples/Test.java:43:5:43:10 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/Test.java:43:5:43:10 | this.y | this expression | examples/Test.java:52:5:52:10 | this.y | this field access | examples/Test.java:24:5:24:18 | setYPrivate(...) | this expression | +| examples/Test.java:43:5:43:10 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/Test.java:43:5:43:10 | this.y | this expression | examples/Test.java:60:5:60:10 | this.y | this field access | examples/Test.java:60:5:60:10 | this.y | this expression | +| examples/Test.java:43:5:43:10 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/Test.java:43:5:43:10 | this.y | this expression | examples/Test.java:74:5:74:10 | this.y | this field access | examples/Test.java:74:5:74:10 | this.y | this expression | +| examples/Test.java:43:5:43:10 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/Test.java:43:5:43:10 | this.y | this expression | examples/Test.java:74:14:74:14 | y | this field access | examples/Test.java:74:14:74:14 | y | this expression | diff --git a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.qlref b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.qlref new file mode 100644 index 000000000000..eba9a6745542 --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.qlref @@ -0,0 +1,2 @@ +query: Likely Bugs/Concurrency/ThreadSafe.ql +postprocess: utils/test/InlineExpectationsTestQuery.ql \ No newline at end of file diff --git a/java/ql/test/query-tests/ThreadSafe/examples/App.java b/java/ql/test/query-tests/ThreadSafe/examples/App.java new file mode 100644 index 000000000000..1c085ee6179a --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/App.java @@ -0,0 +1,14 @@ +/* + * This Java source file was generated by the Gradle 'init' task. + */ +package examples; + +public class App { + public String getGreeting() { + return "Hello World!"; + } + + public static void main(String[] args) { + System.out.println(new App().getGreeting()); + } +} diff --git a/java/ql/test/query-tests/ThreadSafe/examples/C.java b/java/ql/test/query-tests/ThreadSafe/examples/C.java new file mode 100644 index 000000000000..51201d4f6be3 --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/C.java @@ -0,0 +1,72 @@ +package examples; + +import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; + +@ThreadSafe +public class C { + + private int y; + private Lock lock = new ReentrantLock(); + private Lock lock2 = new ReentrantLock(); + + public void m() { + this.y = 0; // $ Alert + this.y += 1; + this.y = this.y - 1; + } + + public void n4() { + this.y = 0; + this.y += 1; + this.y = this.y - 1; + } + + public void setY(int y) { + this.y = y; + } + + public void test() { + if (y == 0) { + lock.lock(); + } + y = 0; + lock.unlock(); + } + + public void n() { + this.lock.lock(); + this.y = 0; + this.y += 1; + this.y = this.y - 1; + this.lock.unlock(); + } + + public void callTestLock2() { + lock2.lock(); + setY(1); + lock2.unlock(); + } + + public void n2() { + lock.lock(); + this.y = 0; + this.y += 1; + this.y = this.y - 1; + lock.unlock(); + } + + public void n3() { + lock.lock(); + y = 0; + y += 1; + y = y - 1; + lock.unlock(); + } + + public void callTest() { + lock.lock(); + setY(1); + lock.unlock(); + } +} \ No newline at end of file diff --git a/java/ql/test/query-tests/ThreadSafe/examples/FaultyTurnstileExample.java b/java/ql/test/query-tests/ThreadSafe/examples/FaultyTurnstileExample.java new file mode 100644 index 000000000000..adbd74473e41 --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/FaultyTurnstileExample.java @@ -0,0 +1,40 @@ +package examples; + +import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; + +@ThreadSafe +class FaultyTurnstileExample { + private Lock lock = new ReentrantLock(); + private int count = 0; + + public void inc() { + lock.lock(); + count++; // $ Alert + lock.unlock(); + } + + public void dec() { + count--; + } +} + +@ThreadSafe +class FaultyTurnstileExample2 { + private Lock lock1 = new ReentrantLock(); + private Lock lock2 = new ReentrantLock(); + private int count = 0; + + public void inc() { + lock1.lock(); + count++; // $ Alert + lock1.unlock(); + } + + public void dec() { + lock2.lock(); + count--; + lock2.unlock(); + } +} + diff --git a/java/ql/test/query-tests/ThreadSafe/examples/FlawedSemaphore.java b/java/ql/test/query-tests/ThreadSafe/examples/FlawedSemaphore.java new file mode 100644 index 000000000000..405edbe7058d --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/FlawedSemaphore.java @@ -0,0 +1,30 @@ +package examples; + +@ThreadSafe +public class FlawedSemaphore { + private final int capacity; + private int state; + + public FlawedSemaphore(int c) { + capacity = c; + state = 0; + } + + public void acquire() { + try { + while (state == capacity) { + this.wait(); + } + state++; // $ Alert + } catch (InterruptedException e) { + e.printStackTrace(); + } + } + + public void release() { + synchronized (this) { + state--; // State can become negative + this.notifyAll(); + } + } +} diff --git a/java/ql/test/query-tests/ThreadSafe/examples/LockCorrect.java b/java/ql/test/query-tests/ThreadSafe/examples/LockCorrect.java new file mode 100644 index 000000000000..9c6c5abce56d --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/LockCorrect.java @@ -0,0 +1,51 @@ +package examples; + +import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; + +@ThreadSafe +public class LockCorrect { + private Lock lock1 = new ReentrantLock(); + + private int length = 0; + private int notRelatedToOther = 10; + private int[] content = new int[10]; + private int thisSynchronized = 0; + + public void add(int value) { + lock1.lock(); + length++; + content[length] = value; + lock1.unlock(); + } + + public void removeCorrect() { + lock1.lock(); + content[length] = 0; + length--; + lock1.unlock(); + } + + public void synchronizedOnLock1() { + synchronized(lock1) { + notRelatedToOther++; + } + } + + public void synchronizedOnLock12() { + synchronized(lock1) { + notRelatedToOther++; + } + } + + public synchronized void x() { + thisSynchronized++; + } + + public void x1() { + synchronized(this) { + thisSynchronized++; + } + } + +} diff --git a/java/ql/test/query-tests/ThreadSafe/examples/LockExample.java b/java/ql/test/query-tests/ThreadSafe/examples/LockExample.java new file mode 100644 index 000000000000..92886bbb5ffb --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/LockExample.java @@ -0,0 +1,156 @@ +// This example shows that we only get one alert "per concurrency problem": +// For each problematic variable, we get one alert at the earliest conflicting write. +// If the variable is involved in several different monitors, we get an alert for each monitor that +// is not correctly used. +// A single alert can have many related locations, since each conflicting access which is not +// prpoerly synchronized is a related location. +// This leads to many lines in the .expected file. +package examples; + +import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; + +@ThreadSafe +public class LockExample { + private Lock lock1 = new ReentrantLock(); + private Lock lock2 = new ReentrantLock(); + + private int length = 0; + private int notRelatedToOther = 10; + private int[] content = new int[10]; + + public void add(int value) { + lock1.lock(); + length++; // $ Alert + content[length] = value; // $ Alert + lock1.unlock(); + } + + public void removeCorrect() { + lock1.lock(); + length--; + content[length] = 0; + lock1.unlock(); + } + + public void notTheSameLockAsAdd() { // use locks, but different ones + lock2.lock(); + length--; // $ Alert + content[length] = 0; // $ Alert + lock2.unlock(); + } + + public void noLock() { // no locks + length--; + content[length] = 0; + } + + public void fieldUpdatedOutsideOfLock() { // adjusts length without lock + length--; + + lock1.lock(); + content[length] = 0; + lock1.unlock(); + } + + public synchronized void synchronizedLock() { // no locks, but with synchronized + length--; + content[length] = 0; + } + + public void onlyLocked() { // never unlocked, only locked + length--; + + lock1.lock(); + content[length] = 0; + } + + public void onlyUnlocked() { // never locked, only unlocked + length--; + + content[length] = 0; + lock1.unlock(); + } + + public void notSameLock() { + length--; + + lock2.lock();// Not the same lock + content[length] = 0; + lock1.unlock(); + } + + public void updateCount() { + lock2.lock(); + notRelatedToOther++; // $ Alert + lock2.unlock(); + } + + public void updateCountTwiceCorrect() { + lock2.lock(); + notRelatedToOther++; + lock2.unlock(); + lock1.lock(); + notRelatedToOther++; // $ Alert + lock1.unlock(); + } + + public void updateCountTwiceDifferentLocks() { + lock2.lock(); + notRelatedToOther++; + lock2.unlock(); + lock1.lock(); + notRelatedToOther++; + lock2.unlock(); + } + + public void updateCountTwiceLock() { + lock2.lock(); + notRelatedToOther++; + lock2.unlock(); + lock1.lock(); + notRelatedToOther++; + } + + public void updateCountTwiceUnLock() { + lock2.lock(); + notRelatedToOther++; + lock2.unlock(); + notRelatedToOther++; + lock1.unlock(); + } + + public void synchronizedNonRelatedOutside() { + notRelatedToOther++; + + synchronized(this) { + length++; + } + } + + public void synchronizedNonRelatedOutside2() { + int x = 0; + x++; + + synchronized(this) { + length++; + } + } + + public void synchronizedNonRelatedOutside3() { + synchronized(this) { + length++; + } + + notRelatedToOther = 1; + } + + public void synchronizedNonRelatedOutside4() { + synchronized(lock1) { + length++; + } + + notRelatedToOther = 1; + } + +} diff --git a/java/ql/test/query-tests/ThreadSafe/examples/LoopyCallGraph.java b/java/ql/test/query-tests/ThreadSafe/examples/LoopyCallGraph.java new file mode 100644 index 000000000000..595aea014f25 --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/LoopyCallGraph.java @@ -0,0 +1,33 @@ +package examples; + +import java.util.Random; +import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; + +@ThreadSafe +public class LoopyCallGraph { + private Lock lock = new ReentrantLock(); + private int count = 0; + private Random random = new Random(); + + public void entry() { + if (random.nextBoolean()) { + increase(); // this looks like an unprotected path to a call to dec() + } else { + lock.lock(); + dec(); + lock.unlock(); + } + } + + private void increase() { + lock.lock(); + count = 10; //$ SPURIOUS: Alert + lock.unlock(); + entry(); // this looks like an unprotected path to a call to dec() + } + + private void dec() { + count--; + } +} \ No newline at end of file diff --git a/java/ql/test/query-tests/ThreadSafe/examples/SyncLstExample.java b/java/ql/test/query-tests/ThreadSafe/examples/SyncLstExample.java new file mode 100644 index 000000000000..63f6985840c1 --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/SyncLstExample.java @@ -0,0 +1,47 @@ +package examples; + +import java.util.List; +import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; + +@ThreadSafe +public class SyncLstExample { + private Lock lock = new ReentrantLock(); + private List lst; + + public SyncLstExample(List lst) { + this.lst = lst; + } + + public void add(T item) { + lock.lock(); + lst.add(item); + lock.unlock(); + } + + public void remove(int i) { + lock.lock(); + lst.remove(i); + lock.unlock(); + } +} + +@ThreadSafe +class FaultySyncLstExample { + private Lock lock = new ReentrantLock(); + private List lst; + + public FaultySyncLstExample(List lst) { + this.lst = lst; + } + + public void add(T item) { + lock.lock(); + lst.add(item); // $ Alert + lock.unlock(); + } + + public void remove(int i) { + lst.remove(i); + } +} diff --git a/java/ql/test/query-tests/ThreadSafe/examples/SyncStackExample.java b/java/ql/test/query-tests/ThreadSafe/examples/SyncStackExample.java new file mode 100644 index 000000000000..62eabde4b7d7 --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/SyncStackExample.java @@ -0,0 +1,39 @@ +package examples; + +import java.util.Stack; +import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; + +@ThreadSafe +public class SyncStackExample { + private Lock lock = new ReentrantLock(); + private Stack stc = new Stack(); + + public void push(T item) { + lock.lock(); + stc.push(item); + lock.unlock(); + } + + public void pop() { + lock.lock(); + stc.pop(); + lock.unlock(); + } +} + +@ThreadSafe +class FaultySyncStackExample { + private Lock lock = new ReentrantLock(); + private Stack stc = new Stack(); + + public void push(T item) { + lock.lock(); + stc.push(item); // $ Alert + lock.unlock(); + } + + public void pop() { + stc.pop(); + } +} diff --git a/java/ql/test/query-tests/ThreadSafe/examples/SynchronizedAndLock.java b/java/ql/test/query-tests/ThreadSafe/examples/SynchronizedAndLock.java new file mode 100644 index 000000000000..fc0aa038b0ee --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/SynchronizedAndLock.java @@ -0,0 +1,21 @@ +package examples; + +import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; + +@ThreadSafe +public class SynchronizedAndLock { + private Lock lock = new ReentrantLock(); + + private int length = 0; + + public void add(int value) { + lock.lock(); + length++; // $ Alert + lock.unlock(); + } + + public synchronized void subtract() { + length--; + } +} diff --git a/java/ql/test/query-tests/ThreadSafe/examples/Test.java b/java/ql/test/query-tests/ThreadSafe/examples/Test.java new file mode 100644 index 000000000000..55fef174fc54 --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/Test.java @@ -0,0 +1,76 @@ +package examples; +import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; + +@ThreadSafe +public class Test { + /** + * Escaping field due to public visuability. + */ + int publicField; + + private int y; + final int immutableField = 1; + + // As of the below examples with synchronized as well. Except the incorretly placed lock. + + private Lock lock = new ReentrantLock(); + + /** + * Calls the a method where y field escapes. + * @param y + */ + public void setYAgainInCorrect(int t) { + setYPrivate(t); + } + + /** + * Locks the method where y field escapes. + * @param y + */ + public void setYAgainCorrect(int y) { + lock.lock(); + setYPrivate(y); + lock.unlock(); + } + + /** + * No escaping y field. Locks the y before assignment. + * @param y + */ + public void setYCorrect(int y) { + lock.lock(); + this.y = y; // $ Alert + lock.unlock(); + } + + /** + * No direct escaping, since it method is private. Only escaping if another public method uses this. + * @param y + */ + private void setYPrivate(int y) { + this.y = y; + } + + /** + * Incorretly locks y. + * @param y + */ + public void setYWrongLock(int y) { + this.y = y; + lock.lock(); + lock.unlock(); + } + + public synchronized int getImmutableField() { + return immutableField; + } + + public synchronized int getImmutableField2() { + return immutableField; + } + + public void testMethod() { + this.y = y + 2; + } +} diff --git a/java/ql/test/query-tests/ThreadSafe/examples/Test2.java b/java/ql/test/query-tests/ThreadSafe/examples/Test2.java new file mode 100644 index 000000000000..731af5ecf679 --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/Test2.java @@ -0,0 +1,22 @@ +package examples; + +import java.util.ArrayList; + +// Note: Not marked as thread-safe +// We inherit from this in Test3Super.java +public class Test2 { + int x; + protected ArrayList lst = new ArrayList<>(); + + public Test2() { + this.x = 0; + } + + public void changeX() { + this.x = x + 1; + } + + public void changeLst() { + lst.add("Hello"); + } +} diff --git a/java/ql/test/query-tests/ThreadSafe/examples/Test3Super.java b/java/ql/test/query-tests/ThreadSafe/examples/Test3Super.java new file mode 100644 index 000000000000..5a48e20bc056 --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/Test3Super.java @@ -0,0 +1,17 @@ +package examples; + +@ThreadSafe +public class Test3Super extends Test2 { // We might want an alert here for the inherited unsafe methods. + + public Test3Super() { + super.x = 0; + } + + public void y() { + super.x = 0; //$ MISSING: Alert + } + + public void yLst() { + super.lst.add("Hello!"); //$ MISSING: Alert + } +} diff --git a/java/ql/test/query-tests/ThreadSafe/examples/ThreadSafe.java b/java/ql/test/query-tests/ThreadSafe/examples/ThreadSafe.java new file mode 100644 index 000000000000..fc0a645c442c --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/ThreadSafe.java @@ -0,0 +1,4 @@ +package examples; + +public @interface ThreadSafe { +} \ No newline at end of file diff --git a/java/ql/test/query-tests/ThreadSafe/examples/TurnstileExample.java b/java/ql/test/query-tests/ThreadSafe/examples/TurnstileExample.java new file mode 100644 index 000000000000..90ea98a77d9e --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/TurnstileExample.java @@ -0,0 +1,23 @@ +package examples; + +import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; + +@ThreadSafe +public class TurnstileExample { + private Lock lock = new ReentrantLock(); + private int count = 0; + + public void inc() { + Lock l = lock; + l.lock(); + count++; + l.unlock(); + } + + public void dec() { + lock.lock(); + count--; + lock.unlock(); + } +} \ No newline at end of file From 328b53576a67c1eff6aabf2afab7a1bb2d271fa0 Mon Sep 17 00:00:00 2001 From: yoff Date: Thu, 15 May 2025 13:06:38 +0200 Subject: [PATCH 02/25] java: add SafePublication query (P2) --- .../Concurrency/SafePublication.java | 11 +++ .../Concurrency/SafePublication.qhelp | 62 +++++++++++++ .../Concurrency/SafePublication.ql | 93 +++++++++++++++++++ .../Concurrency/UnsafePublication.java | 12 +++ .../2025-06-22-query-safe-publication.md | 4 + .../SafePublication/SafePublication.expected | 7 ++ .../SafePublication/SafePublication.java | 29 ++++++ .../SafePublication/SafePublication.qlref | 2 + .../SafePublication/ThreadSafe.java | 2 + 9 files changed, 222 insertions(+) create mode 100644 java/ql/src/Likely Bugs/Concurrency/SafePublication.java create mode 100644 java/ql/src/Likely Bugs/Concurrency/SafePublication.qhelp create mode 100644 java/ql/src/Likely Bugs/Concurrency/SafePublication.ql create mode 100644 java/ql/src/Likely Bugs/Concurrency/UnsafePublication.java create mode 100644 java/ql/src/change-notes/2025-06-22-query-safe-publication.md create mode 100644 java/ql/test/query-tests/SafePublication/SafePublication.expected create mode 100644 java/ql/test/query-tests/SafePublication/SafePublication.java create mode 100644 java/ql/test/query-tests/SafePublication/SafePublication.qlref create mode 100644 java/ql/test/query-tests/SafePublication/ThreadSafe.java diff --git a/java/ql/src/Likely Bugs/Concurrency/SafePublication.java b/java/ql/src/Likely Bugs/Concurrency/SafePublication.java new file mode 100644 index 000000000000..64341017890f --- /dev/null +++ b/java/ql/src/Likely Bugs/Concurrency/SafePublication.java @@ -0,0 +1,11 @@ +public class SafePublication { + private Object value; + + public synchronized void produce() { + value = new Object(); // Safely published using synchronization + } + + public synchronized Object getValue() { + return value; + } +} \ No newline at end of file diff --git a/java/ql/src/Likely Bugs/Concurrency/SafePublication.qhelp b/java/ql/src/Likely Bugs/Concurrency/SafePublication.qhelp new file mode 100644 index 000000000000..a24977e67301 --- /dev/null +++ b/java/ql/src/Likely Bugs/Concurrency/SafePublication.qhelp @@ -0,0 +1,62 @@ + + + + + +

    +In a thread-safe class, values must be published safely to avoid inconsistent or unexpected behavior caused by visibility issues between threads. If a value is not safely published, one thread may see a stale or partially constructed value written by another thread, leading to subtle concurrency bugs. +

    +

    +In particular, values of primitive types should not be initialised to anything but their default values (which for Object is null) unless this happens in a static context. +

    +

    +Techniques for safe publication include: +

    +
      +
    • Using synchronized blocks or methods to ensure that a value is fully constructed before it is published.
      • +
    • Using volatile fields to ensure visibility of changes across threads.
      • +
    • Using thread-safe collections or classes that provide built-in synchronization, such as are found in java.util.concurrent.
      • +
    • Using the final keyword to ensure that a reference to an object is safely published when the object is constructed.
      • +
    + +     + + +

    +Choose a safe publication technique that fits your use case. If the value only needs to be written once, say for a singleton, consider using the final keyword. If the value is mutable and needs to be shared across threads, consider using synchronized blocks or methods, or using a thread-safe collection from java.util.concurrent. +

    + +     + + +

    In the following example, the value of value is not safely published. The produce method + creates a new object and assigns it to the field value. However, the field is not + declared as volatile, and there are no synchronization mechanisms in place to ensure + that the value is fully constructed before it is published.

    + + + +

    To fix this example, declare the field value as volatile, or use + synchronized blocks or methods to ensure that the value is fully constructed before it is + published. We illustrate the latter with the following example:

    + + + +     + + + +
  • + Java Language Specification, chapter 17: + Threads and Locks. +
    • +
  • + Java concurrency package: + java.util.concurrent. +
    • + + +     +     diff --git a/java/ql/src/Likely Bugs/Concurrency/SafePublication.ql b/java/ql/src/Likely Bugs/Concurrency/SafePublication.ql new file mode 100644 index 000000000000..08cd3d5a5779 --- /dev/null +++ b/java/ql/src/Likely Bugs/Concurrency/SafePublication.ql @@ -0,0 +1,93 @@ +/** + * @name Safe publication + * @description A field of a thread-safe class is not safely published. + * @kind problem + * @problem.severity warning + * @precision high + * @id java/safe-publication + * @tags quality + * reliability + * concurrency + */ + +import java +import semmle.code.java.ConflictingAccess + +/** + * Holds if `v` should be the default value for the field `f`. + * That is, `v` is an initial (or constructor) assignment of `f`. + */ +predicate shouldBeDefaultValueFor(Field f, Expr v) { + v = f.getAnAssignedValue() and + ( + v = f.getInitializer() + or + v.getEnclosingCallable() = f.getDeclaringType().getAConstructor() + ) +} + +/** + * Gets the default value for the field `f`. + * See https://docs.oracle.com/javase/tutorial/java/nutsandbolts/datatypes.html + * for the default values of the primitive types. + * The default value for non-primitive types is null. + */ +bindingset[result] +Expr getDefaultValue(Field f) { + f.getType().hasName("byte") and result.(IntegerLiteral).getIntValue() = 0 + or + f.getType().hasName("short") and result.(IntegerLiteral).getIntValue() = 0 + or + f.getType().hasName("int") and result.(IntegerLiteral).getIntValue() = 0 + or + f.getType().hasName("long") and + ( + result.(LongLiteral).getValue() = "0" or + result.(IntegerLiteral).getValue() = "0" + ) + or + f.getType().hasName("float") and result.(FloatLiteral).getValue() = "0.0" + or + f.getType().hasName("double") and result.(DoubleLiteral).getValue() = "0.0" + or + f.getType().hasName("char") and result.(CharacterLiteral).getCodePointValue() = 0 + or + f.getType().hasName("boolean") and result.(BooleanLiteral).getBooleanValue() = false + or + not f.getType().getName() in [ + "byte", "short", "int", "long", "float", "double", "char", "boolean" + ] and + result instanceof NullLiteral +} + +/** + * Holds if all constructor or initial assignments (if any) are to the default value. + * That is, assignments by the declaration: + * int x = 0; OK + * int x = 3; not OK + * or inside a constructor: + * public c(a) { + * x = 0; OK + * x = 3; not OK + * x = a; not OK + * } + */ +predicate isAssignedDefaultValue(Field f) { + forall(Expr v | shouldBeDefaultValueFor(f, v) | v = getDefaultValue(f)) +} + +predicate isSafelyPublished(Field f) { + f.isFinal() or // TODO: Consider non-primitive types + f.isStatic() or + f.isVolatile() or + isThreadSafeType(f.getType()) or + isThreadSafeType(f.getInitializer().getType()) or + isAssignedDefaultValue(f) +} + +from Field f, ClassAnnotatedAsThreadSafe c +where + f = c.getAField() and + not isSafelyPublished(f) +select f, "The class $@ is marked as thread-safe, but this field is not safely published.", c, + c.getName() diff --git a/java/ql/src/Likely Bugs/Concurrency/UnsafePublication.java b/java/ql/src/Likely Bugs/Concurrency/UnsafePublication.java new file mode 100644 index 000000000000..ddf8c8b400f5 --- /dev/null +++ b/java/ql/src/Likely Bugs/Concurrency/UnsafePublication.java @@ -0,0 +1,12 @@ +@ThreadSafe +public class UnsafePublication { + private Object value; + + public void produce() { + value = new Object(); // Not safely published, other threads may see the default value null + } + + public Object getValue() { + return value; + } +} \ No newline at end of file diff --git a/java/ql/src/change-notes/2025-06-22-query-safe-publication.md b/java/ql/src/change-notes/2025-06-22-query-safe-publication.md new file mode 100644 index 000000000000..23b64c970b31 --- /dev/null +++ b/java/ql/src/change-notes/2025-06-22-query-safe-publication.md @@ -0,0 +1,4 @@ +--- +category: newQuery +--- +* Added a new query, `java/safe-publication`, to detect unsafe publication in classes marked as `@ThreadSafe`. \ No newline at end of file diff --git a/java/ql/test/query-tests/SafePublication/SafePublication.expected b/java/ql/test/query-tests/SafePublication/SafePublication.expected new file mode 100644 index 000000000000..fbb54ff7b8cc --- /dev/null +++ b/java/ql/test/query-tests/SafePublication/SafePublication.expected @@ -0,0 +1,7 @@ +| SafePublication.java:5:9:5:9 | z | The class $@ is marked as thread-safe, but this field is not safely published. | SafePublication.java:2:14:2:28 | SafePublication | SafePublication | +| SafePublication.java:6:9:6:9 | w | The class $@ is marked as thread-safe, but this field is not safely published. | SafePublication.java:2:14:2:28 | SafePublication | SafePublication | +| SafePublication.java:7:9:7:9 | u | The class $@ is marked as thread-safe, but this field is not safely published. | SafePublication.java:2:14:2:28 | SafePublication | SafePublication | +| SafePublication.java:11:10:11:10 | d | The class $@ is marked as thread-safe, but this field is not safely published. | SafePublication.java:2:14:2:28 | SafePublication | SafePublication | +| SafePublication.java:12:10:12:10 | e | The class $@ is marked as thread-safe, but this field is not safely published. | SafePublication.java:2:14:2:28 | SafePublication | SafePublication | +| SafePublication.java:14:11:14:13 | arr | The class $@ is marked as thread-safe, but this field is not safely published. | SafePublication.java:2:14:2:28 | SafePublication | SafePublication | +| SafePublication.java:17:10:17:11 | cc | The class $@ is marked as thread-safe, but this field is not safely published. | SafePublication.java:2:14:2:28 | SafePublication | SafePublication | diff --git a/java/ql/test/query-tests/SafePublication/SafePublication.java b/java/ql/test/query-tests/SafePublication/SafePublication.java new file mode 100644 index 000000000000..9c1d031987b0 --- /dev/null +++ b/java/ql/test/query-tests/SafePublication/SafePublication.java @@ -0,0 +1,29 @@ +@ThreadSafe +public class SafePublication { + int x; + int y = 0; + int z = 3; //$ Alert + int w; //$ Alert + int u; //$ Alert + long a; + long b = 0; + long c = 0L; + long d = 3; //$ Alert + long e = 3L; //$ Alert + + int[] arr = new int[3]; //$ Alert + float f = 0.0f; + double dd = 00.0d; + char cc = 'a'; //$ Alert + char ok = '\u0000'; + + public SafePublication(int a) { + x = 0; + w = 3; // not ok + u = a; // not ok + } + + public void methodLocal() { + int i; + } +} \ No newline at end of file diff --git a/java/ql/test/query-tests/SafePublication/SafePublication.qlref b/java/ql/test/query-tests/SafePublication/SafePublication.qlref new file mode 100644 index 000000000000..51bf2ced9660 --- /dev/null +++ b/java/ql/test/query-tests/SafePublication/SafePublication.qlref @@ -0,0 +1,2 @@ +query: Likely Bugs/Concurrency/SafePublication.ql +postprocess: utils/test/InlineExpectationsTestQuery.ql \ No newline at end of file diff --git a/java/ql/test/query-tests/SafePublication/ThreadSafe.java b/java/ql/test/query-tests/SafePublication/ThreadSafe.java new file mode 100644 index 000000000000..1a4534cc78f4 --- /dev/null +++ b/java/ql/test/query-tests/SafePublication/ThreadSafe.java @@ -0,0 +1,2 @@ +public @interface ThreadSafe { +} \ No newline at end of file From 5b301531135385eed02c23a63605d07afa07d696 Mon Sep 17 00:00:00 2001 From: yoff Date: Thu, 15 May 2025 13:16:51 +0200 Subject: [PATCH 03/25] java: add Escaping query (P1) --- .../Likely Bugs/Concurrency/Escaping.qhelp | 34 +++++++++++++++++++ .../src/Likely Bugs/Concurrency/Escaping.ql | 26 ++++++++++++++ .../change-notes/2025-06-22-query-escaping.md | 4 +++ .../query-tests/Escaping/Escaping.expected | 3 ++ .../test/query-tests/Escaping/Escaping.java | 17 ++++++++++ .../test/query-tests/Escaping/Escaping.qlref | 2 ++ .../test/query-tests/Escaping/ThreadSafe.java | 2 ++ 7 files changed, 88 insertions(+) create mode 100644 java/ql/src/Likely Bugs/Concurrency/Escaping.qhelp create mode 100644 java/ql/src/Likely Bugs/Concurrency/Escaping.ql create mode 100644 java/ql/src/change-notes/2025-06-22-query-escaping.md create mode 100644 java/ql/test/query-tests/Escaping/Escaping.expected create mode 100644 java/ql/test/query-tests/Escaping/Escaping.java create mode 100644 java/ql/test/query-tests/Escaping/Escaping.qlref create mode 100644 java/ql/test/query-tests/Escaping/ThreadSafe.java diff --git a/java/ql/src/Likely Bugs/Concurrency/Escaping.qhelp b/java/ql/src/Likely Bugs/Concurrency/Escaping.qhelp new file mode 100644 index 000000000000..a8a614dbe369 --- /dev/null +++ b/java/ql/src/Likely Bugs/Concurrency/Escaping.qhelp @@ -0,0 +1,34 @@ + + + + + +

    +In a thread-safe class, non-final fields should generally be private (or possibly volatile) to ensure that they cannot be accessed by other threads in an unsafe manner. +

    + +     + + +

    +If the field does not change, mark it as final. If the field is mutable, mark it as private and provide properly synchronized accessors.

    + +     + + + + +
  • + Java Language Specification, chapter 17: + Threads and Locks. +
    • +
  • + Java concurrency package: + java.util.concurrent. +
    • + + +     +     diff --git a/java/ql/src/Likely Bugs/Concurrency/Escaping.ql b/java/ql/src/Likely Bugs/Concurrency/Escaping.ql new file mode 100644 index 000000000000..a2f3e0f7b463 --- /dev/null +++ b/java/ql/src/Likely Bugs/Concurrency/Escaping.ql @@ -0,0 +1,26 @@ +/** + * @name Escaping + * @description In a thread-safe class, care should be taken to avoid exposing mutable state. + * @kind problem + * @problem.severity warning + * @precision high + * @id java/escaping + * @tags quality + * reliability + * concurrency + */ + +import java +import semmle.code.java.ConflictingAccess + +from Field f, ClassAnnotatedAsThreadSafe c +where + f = c.getAField() and + not f.isFinal() and // final fields do not change + not f.isPrivate() and + // We believe that protected fields are also dangerous + // Volatile fields cannot cause data races, but it is dubious to allow changes. + // For now, we ignore volatile fields, but there are likely bugs to be caught here. + not f.isVolatile() +select f, "The class $@ is marked as thread-safe, but this field is potentially escaping.", c, + c.getName() diff --git a/java/ql/src/change-notes/2025-06-22-query-escaping.md b/java/ql/src/change-notes/2025-06-22-query-escaping.md new file mode 100644 index 000000000000..f33de2e8556f --- /dev/null +++ b/java/ql/src/change-notes/2025-06-22-query-escaping.md @@ -0,0 +1,4 @@ +--- +category: newQuery +--- +* Added a new query, `java/escaping`, to detect values escaping from classes marked as `@ThreadSafe`. \ No newline at end of file diff --git a/java/ql/test/query-tests/Escaping/Escaping.expected b/java/ql/test/query-tests/Escaping/Escaping.expected new file mode 100644 index 000000000000..e066b29dae4f --- /dev/null +++ b/java/ql/test/query-tests/Escaping/Escaping.expected @@ -0,0 +1,3 @@ +| Escaping.java:3:7:3:7 | x | The class $@ is marked as thread-safe, but this field is potentially escaping. | Escaping.java:2:14:2:21 | Escaping | Escaping | +| Escaping.java:4:14:4:14 | y | The class $@ is marked as thread-safe, but this field is potentially escaping. | Escaping.java:2:14:2:21 | Escaping | Escaping | +| Escaping.java:9:18:9:18 | b | The class $@ is marked as thread-safe, but this field is potentially escaping. | Escaping.java:2:14:2:21 | Escaping | Escaping | diff --git a/java/ql/test/query-tests/Escaping/Escaping.java b/java/ql/test/query-tests/Escaping/Escaping.java new file mode 100644 index 000000000000..9d3b568369ad --- /dev/null +++ b/java/ql/test/query-tests/Escaping/Escaping.java @@ -0,0 +1,17 @@ +@ThreadSafe +public class Escaping { + int x; //$ Alert + public int y = 0; //$ Alert + private int z = 3; + final int w = 0; + public final int u = 4; + private final long a = 5; + protected long b = 0; //$ Alert + protected final long c = 0L; + volatile long d = 3; + protected volatile long e = 3L; + + public void methodLocal() { + int i; + } +} \ No newline at end of file diff --git a/java/ql/test/query-tests/Escaping/Escaping.qlref b/java/ql/test/query-tests/Escaping/Escaping.qlref new file mode 100644 index 000000000000..846d88a1e0aa --- /dev/null +++ b/java/ql/test/query-tests/Escaping/Escaping.qlref @@ -0,0 +1,2 @@ +query: Likely Bugs/Concurrency/Escaping.ql +postprocess: utils/test/InlineExpectationsTestQuery.ql \ No newline at end of file diff --git a/java/ql/test/query-tests/Escaping/ThreadSafe.java b/java/ql/test/query-tests/Escaping/ThreadSafe.java new file mode 100644 index 000000000000..1a4534cc78f4 --- /dev/null +++ b/java/ql/test/query-tests/Escaping/ThreadSafe.java @@ -0,0 +1,2 @@ +public @interface ThreadSafe { +} \ No newline at end of file From 096d5f2a56e1ab778eec98c74de39bd67705858a Mon Sep 17 00:00:00 2001 From: yoff Date: Tue, 20 May 2025 14:12:45 +0200 Subject: [PATCH 04/25] java: implement SCC contraction of the call graph Our monitor analysis would be fooled by cycles in the call graph, since it required all edges on a path to a conflicting access to be either - targetting a method where the access is monitored (recursively) or - monitored locally, that is the call is monitored in the calling method For access to be monitored (first case) all outgoing edges (towards an access) need to satisfy this property. For a loop, that is too strong, only edges out of the loop actually need to be protected. This led to FPs. --- .../semmle/code/java/ConflictingAccess.qll | 111 ++++++++++++++++-- .../ThreadSafe/ThreadSafe.expected | 2 - .../ThreadSafe/examples/LoopyCallGraph.java | 6 +- 3 files changed, 107 insertions(+), 12 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index 0d92438ae0f2..75845044d279 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -321,18 +321,115 @@ class ClassAnnotatedAsThreadSafe extends Class { ) } - /** Holds if all paths from `m` to `a` are monitored by `monitor`. */ - predicate monitorsVia(Method m, ExposedFieldAccess a, Monitors::Monitor monitor) { + // NOTE: + // In order to deal with loops in the call graph, we compute the strongly connected components (SCCs). + // We only wish to do this for the methods that can lead to exposed field accesses. + // Given a field access `a`, we can consider a "call graph of interest", a sub graph of the call graph + // that only contains methods that lead to an access of `a`. We call this "the call graph induced by `a`". + // We can then compute the SCCs of this graph, yielding the SCC graph induced by `a`. + // + /** + * Holds if a call to method `m` can cause an access of `a` by `m` calling `callee`. + * This is an edge in the call graph induced by `a`. + */ + predicate accessVia(Method m, ExposedFieldAccess a, Method callee) { + exists(MethodCall c | this.providesAccess(m, c, a) | callee = c.getCallee()) + } + + /** Holds if `m` can reach `reached` by a path in the call graph induced by `a`. */ + predicate accessReach(Method m, ExposedFieldAccess a, Method reached) { + m = this.getAMethod() and + reached = this.getAMethod() and + this.providesAccess(m, _, a) and + this.providesAccess(reached, _, a) and + ( + this.accessVia(m, a, reached) + or + exists(Method mid | this.accessReach(m, a, mid) | this.accessVia(mid, a, reached)) + ) + } + + /** + * Holds if `rep` is a representative of the SCC containing `m` in the call graph induced by `a`. + * This only assigns representatives to methods involved in loops. + * To get a representative of any method, use `repScc`. + */ + predicate repInLoopScc(Method rep, ExposedFieldAccess a, Method m) { + // `rep` and `m` are in the same SCC + this.accessReach(rep, a, m) and + this.accessReach(m, a, rep) and + // `rep` is the representative of the SCC + // that is, the earliest in the source code + forall(Method alt_rep | + rep != alt_rep and + this.accessReach(alt_rep, a, m) and + this.accessReach(m, a, alt_rep) + | + rep.getLocation().getStartLine() < alt_rep.getLocation().getStartLine() + ) + } + + /** Holds if `rep` is a representative of the SCC containing `m` in the call graph induced by `a`. */ + predicate repScc(Method rep, ExposedFieldAccess a, Method m) { + this.repInLoopScc(rep, a, m) + or + // If `m` is in the call graph induced by `a` and did not get a representative from `repInLoopScc`, + // it is represented by itself. m = this.getAMethod() and this.providesAccess(m, _, a) and - (a.getEnclosingCallable() = m implies Monitors::locallyMonitors(a, monitor)) and - forall(MethodCall c | - c.getEnclosingCallable() = m and - this.providesAccess(c.getCallee(), _, a) + not this.repInLoopScc(_, a, m) and + rep = m + } + + /** + * Holds if `c` is a call from the SCC represented by `callerRep` to the (different) SCC represented by `calleeRep`. + * This is an edge in the SCC graph induced by `a`. + */ + predicate callEdgeScc(Method callerRep, ExposedFieldAccess a, MethodCall c, Method calleeRep) { + callerRep != calleeRep and + exists(Method caller, Method callee | + this.repScc(callerRep, a, caller) and + this.repScc(calleeRep, a, callee) | + this.accessVia(caller, a, callee) and + c.getEnclosingCallable() = caller and + c.getCallee() = callee + ) + } + + /** + * Holds if the SCC represented by `rep` can cause an access to `a` and `e` is the expression that leads to that access. + * `e` will either be `a` itself or a method call that leads to `a` via a different SCC. + */ + predicate providesAccessScc(Method rep, Expr e, ExposedFieldAccess a) { + rep = this.getAMethod() and + exists(Method m | this.repScc(rep, a, m) | + a.getEnclosingCallable() = m and + e = a + or + exists(MethodCall c | this.callEdgeScc(rep, a, c, _) | e = c) + ) + } + + /** Holds if all paths from `rep` to `a` are monitored by `monitor`. */ + predicate monitorsViaScc(Method rep, ExposedFieldAccess a, Monitors::Monitor monitor) { + rep = this.getAMethod() and + this.providesAccessScc(rep, _, a) and + // If we are in an SCC that can access `a`, the access must be monitored locally + (this.repScc(rep, a, a.getEnclosingCallable()) implies Monitors::locallyMonitors(a, monitor)) and + // Any call towards `a` must either be monitored or guarantee that the access is monitored + forall(MethodCall c, Method calleeRep | this.callEdgeScc(rep, a, c, calleeRep) | Monitors::locallyMonitors(c, monitor) or - this.monitorsVia(c.getCallee(), a, monitor) + this.monitorsViaScc(calleeRep, a, monitor) + ) + } + + /** Holds if all paths from `m` to `a` are monitored by `monitor`. */ + predicate monitorsVia(Method m, ExposedFieldAccess a, Monitors::Monitor monitor) { + exists(Method rep | + this.repScc(rep, a, m) and + this.monitorsViaScc(rep, a, monitor) ) } } diff --git a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected index 72d0bbb1a3a3..d25b09260ee7 100644 --- a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected +++ b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected @@ -63,8 +63,6 @@ | examples/LockExample.java:94:5:94:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression | examples/LockExample.java:103:5:103:21 | notRelatedToOther | this field access | examples/LockExample.java:103:5:103:21 | notRelatedToOther | this expression | | examples/LockExample.java:94:5:94:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression | examples/LockExample.java:109:5:109:21 | notRelatedToOther | this field access | examples/LockExample.java:109:5:109:21 | notRelatedToOther | this expression | | examples/LockExample.java:94:5:94:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression | examples/LockExample.java:117:5:117:21 | notRelatedToOther | this field access | examples/LockExample.java:117:5:117:21 | notRelatedToOther | this expression | -| examples/LoopyCallGraph.java:25:5:25:9 | count | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LoopyCallGraph.java:15:7:15:16 | increase(...) | this expression | examples/LoopyCallGraph.java:25:5:25:9 | count | this field access | examples/LoopyCallGraph.java:15:7:15:16 | increase(...) | this expression | -| examples/LoopyCallGraph.java:25:5:25:9 | count | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LoopyCallGraph.java:15:7:15:16 | increase(...) | this expression | examples/LoopyCallGraph.java:31:5:31:9 | count | this field access | examples/LoopyCallGraph.java:15:7:15:16 | increase(...) | this expression | | examples/SyncLstExample.java:40:5:40:7 | lst | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/SyncLstExample.java:40:5:40:7 | lst | this expression | examples/SyncLstExample.java:45:5:45:7 | lst | this field access | examples/SyncLstExample.java:45:5:45:7 | lst | this expression | | examples/SyncStackExample.java:32:5:32:7 | stc | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/SyncStackExample.java:32:5:32:7 | stc | this expression | examples/SyncStackExample.java:37:5:37:7 | stc | this field access | examples/SyncStackExample.java:37:5:37:7 | stc | this expression | | examples/SynchronizedAndLock.java:14:9:14:14 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/SynchronizedAndLock.java:14:9:14:14 | length | this expression | examples/SynchronizedAndLock.java:19:9:19:14 | length | this field access | examples/SynchronizedAndLock.java:19:9:19:14 | length | this expression | diff --git a/java/ql/test/query-tests/ThreadSafe/examples/LoopyCallGraph.java b/java/ql/test/query-tests/ThreadSafe/examples/LoopyCallGraph.java index 595aea014f25..caea22ac8511 100644 --- a/java/ql/test/query-tests/ThreadSafe/examples/LoopyCallGraph.java +++ b/java/ql/test/query-tests/ThreadSafe/examples/LoopyCallGraph.java @@ -12,7 +12,7 @@ public class LoopyCallGraph { public void entry() { if (random.nextBoolean()) { - increase(); // this looks like an unprotected path to a call to dec() + increase(); // this could look like an unprotected path to a call to dec() } else { lock.lock(); dec(); @@ -22,9 +22,9 @@ public void entry() { private void increase() { lock.lock(); - count = 10; //$ SPURIOUS: Alert + count = 10; lock.unlock(); - entry(); // this looks like an unprotected path to a call to dec() + entry(); // this could look like an unprotected path to a call to dec() } private void dec() { From bf138693a3a7c56482b4c77ee084cdf82cb0502b Mon Sep 17 00:00:00 2001 From: yoff Date: Thu, 22 May 2025 14:44:24 +0200 Subject: [PATCH 05/25] java: update expectations for java-code-quality suite --- .../java/query-suite/java-code-quality.qls.expected | 3 +++ 1 file changed, 3 insertions(+) diff --git a/java/ql/integration-tests/java/query-suite/java-code-quality.qls.expected b/java/ql/integration-tests/java/query-suite/java-code-quality.qls.expected index eb502feb6bac..56e2daa58ce0 100644 --- a/java/ql/integration-tests/java/query-suite/java-code-quality.qls.expected +++ b/java/ql/integration-tests/java/query-suite/java-code-quality.qls.expected @@ -30,10 +30,13 @@ ql/java/ql/src/Likely Bugs/Comparison/WrongNanComparison.ql ql/java/ql/src/Likely Bugs/Concurrency/CallsToRunnableRun.ql ql/java/ql/src/Likely Bugs/Concurrency/DoubleCheckedLocking.ql ql/java/ql/src/Likely Bugs/Concurrency/DoubleCheckedLockingWithInitRace.ql +ql/java/ql/src/Likely Bugs/Concurrency/Escaping.ql ql/java/ql/src/Likely Bugs/Concurrency/NonSynchronizedOverride.ql +ql/java/ql/src/Likely Bugs/Concurrency/SafePublication.ql ql/java/ql/src/Likely Bugs/Concurrency/ScheduledThreadPoolExecutorZeroThread.ql ql/java/ql/src/Likely Bugs/Concurrency/SynchOnBoxedType.ql ql/java/ql/src/Likely Bugs/Concurrency/SynchSetUnsynchGet.ql +ql/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql ql/java/ql/src/Likely Bugs/Frameworks/JUnit/JUnit5MissingNestedAnnotation.ql ql/java/ql/src/Likely Bugs/Inheritance/NoNonFinalInConstructor.ql ql/java/ql/src/Likely Bugs/Likely Typos/ContainerSizeCmpZero.ql From 77734f83d5ea7281ef676df99f490274dd464432 Mon Sep 17 00:00:00 2001 From: yoff Date: Tue, 27 May 2025 15:39:41 +0200 Subject: [PATCH 06/25] java: better detection of thread safe fields. Identified by triage of DCA results. Previously, we did not use the erased type, so would not recgnize `CompletableFuture`. We now also recognize safe initializers. --- .../semmle/code/java/ConflictingAccess.qll | 20 ++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index 75845044d279..1a497566174a 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -160,18 +160,22 @@ Class annotatedAsThreadSafe() { result.getAnAnnotation().getType().getName() = " /** Holds if the type `t` is thread-safe. */ predicate isThreadSafeType(Type t) { - t.getName().matches(["Atomic%", "Concurrent%"]) + t.getErasure().getName().matches(["Atomic%", "Concurrent%"]) or - t.getName() in [ - "CopyOnWriteArraySet", "BlockingQueue", "ThreadLocal", - // this is a method that returns a thread-safe version of the collection used as parameter - "synchronizedMap", "Executor", "ExecutorService", "CopyOnWriteArrayList", - "LinkedBlockingDeque", "LinkedBlockingQueue", "CompletableFuture" - ] + t.getErasure().getName() in ["ThreadLocal"] + or + // Anything in `java.itul.concurrent` is thread safe. + // See https://docs.oracle.com/javase/8/docs/api/java/util/concurrent/package-summary.html#MemoryVisibility + t.getTypeDescriptor().matches("Ljava/util/concurrent/%;") or t = annotatedAsThreadSafe() } +/** Holds if the expression `e` is a thread-safe initializer. */ +predicate isThreadSafeInitializer(Expr e) { + e.(Call).getCallee().getQualifiedName().matches("java.util.Collections.synchronized%") +} + /** * A field access that is exposed to potential data races. * We require the field to be in a class that is annotated as `@ThreadSafe`. @@ -185,6 +189,8 @@ class ExposedFieldAccess extends FieldAccess { // field is not thread-safe not isThreadSafeType(this.getField().getType()) and not isThreadSafeType(this.getField().getInitializer().getType()) and + // the initializer guarantees thread safety + not isThreadSafeInitializer(this.getField().getInitializer()) and // access is not the initializer of the field not this.(VarWrite).getASource() = this.getField().getInitializer() and // access not in a constructor From 01ddc11fa7b6a2e964f28c0784738a9dae878b84 Mon Sep 17 00:00:00 2001 From: yoff Date: Mon, 9 Jun 2025 08:40:51 +0200 Subject: [PATCH 07/25] java: address some review comments --- .../semmle/code/java/ConflictingAccess.qll | 61 +++++++------------ 1 file changed, 23 insertions(+), 38 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index 1a497566174a..7ef2ca38dbda 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -37,7 +37,7 @@ module Monitors { abstract Location getLocation(); /** Gets a textual representation of this element. */ - string toString() { result = "Monitor" } + abstract string toString(); } /** @@ -46,16 +46,12 @@ module Monitors { * E.g `synchronized (m) { ... }` or `m.lock();` */ class VariableMonitor extends Monitor, TVariableMonitor { - Variable v; + override Location getLocation() { result = this.getVariable().getLocation() } - VariableMonitor() { this = TVariableMonitor(v) } - - override Location getLocation() { result = v.getLocation() } - - override string toString() { result = "VariableMonitor(" + v.toString() + ")" } + override string toString() { result = "VariableMonitor(" + this.getVariable().toString() + ")" } /** Gets the variable being used as a monitor. */ - Variable getVariable() { result = v } + Variable getVariable() { this = TVariableMonitor(result) } } /** @@ -63,16 +59,12 @@ module Monitors { * Either via `synchronized (this) { ... }` or by marking a non-static method as `synchronized`. */ class InstanceMonitor extends Monitor, TInstanceMonitor { - RefType thisType; - - InstanceMonitor() { this = TInstanceMonitor(thisType) } + override Location getLocation() { result = this.getThisType().getLocation() } - override Location getLocation() { result = thisType.getLocation() } - - override string toString() { result = "InstanceMonitor(" + thisType.toString() + ")" } + override string toString() { result = "InstanceMonitor(" + this.getThisType().toString() + ")" } /** Gets the instance reference being used as a monitor. */ - RefType getThisType() { result = thisType } + RefType getThisType() { this = TInstanceMonitor(result) } } /** @@ -80,16 +72,12 @@ module Monitors { * This is achieved by marking a static method as `synchronized`. */ class ClassMonitor extends Monitor, TClassMonitor { - RefType classType; - - ClassMonitor() { this = TClassMonitor(classType) } - - override Location getLocation() { result = classType.getLocation() } + override Location getLocation() { result = this.getClassType().getLocation() } - override string toString() { result = "ClassMonitor(" + classType.toString() + ")" } + override string toString() { result = "ClassMonitor(" + this.getClassType().toString() + ")" } /** Gets the class being used as a monitor. */ - RefType getClassType() { result = classType } + RefType getClassType() { this = TClassMonitor(result) } } /** Holds if the expression `e` is synchronized on the monitor `m`. */ @@ -115,6 +103,15 @@ module Monitors { ) } + ControlFlowNode getNodeToBeDominated(Expr e) { + // If `e` is the LHS of an assignment, use the control flow node for the assignment + exists(Assignment asgn | asgn.getDest() = e | result = asgn.getControlFlowNode()) + or + // if `e` is not the LHS of an assignment, use the default control flow node + not exists(Assignment asgn | asgn.getDest() = e) and + result = e.getControlFlowNode() + } + /** Holds if `e` is synchronized on the `Lock` `lock` by a locking call. */ predicate locallyLockedOn(Expr e, Field lock) { isLockType(lock.getType()) and @@ -126,8 +123,8 @@ module Monitors { unlockCall.getMethod().getName() = "unlock" | dominates(lockCall.getControlFlowNode(), unlockCall.getControlFlowNode()) and - dominates(lockCall.getControlFlowNode(), e.getControlFlowNode()) and - postDominates(unlockCall.getControlFlowNode(), e.getControlFlowNode()) + dominates(lockCall.getControlFlowNode(), getNodeToBeDominated(e)) and + postDominates(unlockCall.getControlFlowNode(), getNodeToBeDominated(e)) ) } } @@ -147,10 +144,9 @@ module Modification { /** Holds if the call `c` modifies a shared resource. */ predicate isModifyingCall(Call c) { - exists(SummarizedCallable sc, string output, string prefix | sc.getACall() = c | + exists(SummarizedCallable sc, string output | sc.getACall() = c | sc.propagatesFlow(_, output, _, _) and - prefix = "Argument[this]" and - output.prefix(prefix.length()) = prefix + output.matches("Argument[this]%") ) } } @@ -200,17 +196,6 @@ class ExposedFieldAccess extends FieldAccess { // not the variable mention in a synchronized statement not this = any(SynchronizedStmt sync).getExpr() } - - // LHS of assignments are excluded from the control flow graph, - // so we use the control flow node for the assignment itself instead. - override ControlFlowNode getControlFlowNode() { - // this is the LHS of an assignment, use the control flow node for the assignment - exists(Assignment asgn | asgn.getDest() = this | result = asgn.getControlFlowNode()) - or - // this is not the LHS of an assignment, use the default control flow node - not exists(Assignment asgn | asgn.getDest() = this) and - result = super.getControlFlowNode() - } } /** Holds if the location of `a` is strictly before the location of `b`. */ From 821b1de5b39041db4e3c17b82542967c29be4d02 Mon Sep 17 00:00:00 2001 From: yoff Date: Mon, 9 Jun 2025 09:18:02 +0200 Subject: [PATCH 08/25] java: inline char pred --- java/ql/lib/semmle/code/java/ConflictingAccess.qll | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index 7ef2ca38dbda..74ae148db398 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -151,9 +151,6 @@ module Modification { } } -/** Holds if the class is annotated as `@ThreadSafe`. */ -Class annotatedAsThreadSafe() { result.getAnAnnotation().getType().getName() = "ThreadSafe" } - /** Holds if the type `t` is thread-safe. */ predicate isThreadSafeType(Type t) { t.getErasure().getName().matches(["Atomic%", "Concurrent%"]) @@ -164,7 +161,7 @@ predicate isThreadSafeType(Type t) { // See https://docs.oracle.com/javase/8/docs/api/java/util/concurrent/package-summary.html#MemoryVisibility t.getTypeDescriptor().matches("Ljava/util/concurrent/%;") or - t = annotatedAsThreadSafe() + t instanceof ClassAnnotatedAsThreadSafe } /** Holds if the expression `e` is a thread-safe initializer. */ @@ -178,7 +175,7 @@ predicate isThreadSafeInitializer(Expr e) { */ class ExposedFieldAccess extends FieldAccess { ExposedFieldAccess() { - this.getField() = annotatedAsThreadSafe().getAField() and + this.getField() = any(ClassAnnotatedAsThreadSafe c).getAField() and not this.getField().isVolatile() and // field is not a lock not isLockType(this.getField().getType()) and @@ -212,7 +209,7 @@ predicate orderedLocations(Location a, Location b) { * Provides predicates to check for concurrency issues. */ class ClassAnnotatedAsThreadSafe extends Class { - ClassAnnotatedAsThreadSafe() { this = annotatedAsThreadSafe() } + ClassAnnotatedAsThreadSafe() { this.getAnAnnotation().getType().getName() = "ThreadSafe" } /** Holds if `a` and `b` are conflicting accesses to the same field and not monitored by the same monitor. */ predicate unsynchronised(ExposedFieldAccess a, ExposedFieldAccess b) { From a1671ea8af6d2661b32b379f27e6c875224e6d87 Mon Sep 17 00:00:00 2001 From: yoff Date: Thu, 9 Oct 2025 09:11:02 +0200 Subject: [PATCH 09/25] java: small cleanups - add missing qldoc - remove use of `getErasure` - remove use of `getTypeDescriptor` - define `ExposedField` --- .../semmle/code/java/ConflictingAccess.qll | 38 ++++++++++++------- 1 file changed, 25 insertions(+), 13 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index 74ae148db398..17890e1798fb 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -103,6 +103,7 @@ module Monitors { ) } + /** 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 exists(Assignment asgn | asgn.getDest() = e | result = asgn.getControlFlowNode()) @@ -153,13 +154,13 @@ module Modification { /** Holds if the type `t` is thread-safe. */ predicate isThreadSafeType(Type t) { - t.getErasure().getName().matches(["Atomic%", "Concurrent%"]) + t.(RefType).getSourceDeclaration().getName().matches(["Atomic%", "Concurrent%"]) or - t.getErasure().getName() in ["ThreadLocal"] + t.(RefType).getSourceDeclaration().getName() in ["ThreadLocal"] or // Anything in `java.itul.concurrent` is thread safe. // See https://docs.oracle.com/javase/8/docs/api/java/util/concurrent/package-summary.html#MemoryVisibility - t.getTypeDescriptor().matches("Ljava/util/concurrent/%;") + t.(RefType).getPackage().getName() = "java.util.concurrent" or t instanceof ClassAnnotatedAsThreadSafe } @@ -170,27 +171,38 @@ predicate isThreadSafeInitializer(Expr e) { } /** - * A field access that is exposed to potential data races. + * A field that is exposed to potential data races. * We require the field to be in a class that is annotated as `@ThreadSafe`. */ -class ExposedFieldAccess extends FieldAccess { - ExposedFieldAccess() { - this.getField() = any(ClassAnnotatedAsThreadSafe c).getAField() and - not this.getField().isVolatile() and +class ExposedField extends Field { + ExposedField() { + this.getDeclaringType() instanceof ClassAnnotatedAsThreadSafe and + not this.isVolatile() and // field is not a lock - not isLockType(this.getField().getType()) and + not isLockType(this.getType()) and // field is not thread-safe - not isThreadSafeType(this.getField().getType()) and - not isThreadSafeType(this.getField().getInitializer().getType()) and + not isThreadSafeType(this.getType()) and + not isThreadSafeType(this.getInitializer().getType()) and // the initializer guarantees thread safety - not isThreadSafeInitializer(this.getField().getInitializer()) and + not isThreadSafeInitializer(this.getInitializer()) + } +} + +/** + * A field access that is exposed to potential data races. + * We require the field to be in a class that is annotated as `@ThreadSafe`. + */ +class ExposedFieldAccess extends FieldAccess { + ExposedFieldAccess() { + // access is to an exposed field + this.getField() instanceof ExposedField and // access is not the initializer of the field not this.(VarWrite).getASource() = this.getField().getInitializer() and // access not in a constructor not this.getEnclosingCallable() = this.getField().getDeclaringType().getAConstructor() and // not a field on a local variable not this.getQualifier+().(VarAccess).getVariable() instanceof LocalVariableDecl and - // not the variable mention in a synchronized statement + // not the variable mentioned in a synchronized statement not this = any(SynchronizedStmt sync).getExpr() } } From 93fc287ef12768b571a22f2ce4a2b44d8a3f784b Mon Sep 17 00:00:00 2001 From: yoff Date: Thu, 9 Oct 2025 09:25:57 +0200 Subject: [PATCH 10/25] java: add auto-generated overlay annotations --- java/ql/lib/semmle/code/java/ConflictingAccess.qll | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index 17890e1798fb..39bd7f0d383f 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -1,6 +1,8 @@ /** * Provides classes and predicates for detecting conflicting accesses in the sense of the Java Memory Model. */ +overlay[local?] +module; import java import Concurrency @@ -9,6 +11,7 @@ import Concurrency * Holds if `t` is the type of a lock. * Currently a crude test of the type name. */ +overlay[caller?] pragma[inline] predicate isLockType(Type t) { t.getName().matches("%Lock%") } @@ -208,6 +211,7 @@ class ExposedFieldAccess extends FieldAccess { } /** Holds if the location of `a` is strictly before the location of `b`. */ +overlay[caller?] pragma[inline] predicate orderedLocations(Location a, Location b) { a.getStartLine() < b.getStartLine() From 830f02af1ff14968cae0c45e9f0c595d11a7831a Mon Sep 17 00:00:00 2001 From: yoff Date: Thu, 9 Oct 2025 09:37:31 +0200 Subject: [PATCH 11/25] java: fixes from the CI bots --- java/ql/lib/semmle/code/java/ConflictingAccess.qll | 6 +++--- java/ql/src/Likely Bugs/Concurrency/SafePublication.ql | 2 +- .../test/query-tests/ThreadSafe/examples/LockExample.java | 2 +- java/ql/test/query-tests/ThreadSafe/examples/Test.java | 6 +++--- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index 39bd7f0d383f..1243a94d6615 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -159,9 +159,9 @@ module Modification { predicate isThreadSafeType(Type t) { t.(RefType).getSourceDeclaration().getName().matches(["Atomic%", "Concurrent%"]) or - t.(RefType).getSourceDeclaration().getName() in ["ThreadLocal"] + t.(RefType).getSourceDeclaration().getName() = "ThreadLocal" or - // Anything in `java.itul.concurrent` is thread safe. + // Anything in `java.util.concurrent` is thread safe. // See https://docs.oracle.com/javase/8/docs/api/java/util/concurrent/package-summary.html#MemoryVisibility t.(RefType).getPackage().getName() = "java.util.concurrent" or @@ -303,7 +303,7 @@ class ClassAnnotatedAsThreadSafe extends Class { ) } - /** Holds if `a` can be reached by a path from a public method and `e` is the expression in that method that stsarts the path. */ + /** Holds if `a` can be reached by a path from a public method and `e` is the expression in that method that starts the path. */ predicate publicAccess(Expr e, ExposedFieldAccess a) { exists(Method m | m.isPublic() | this.providesAccess(m, e, a)) } diff --git a/java/ql/src/Likely Bugs/Concurrency/SafePublication.ql b/java/ql/src/Likely Bugs/Concurrency/SafePublication.ql index 08cd3d5a5779..5e2a89ce3721 100644 --- a/java/ql/src/Likely Bugs/Concurrency/SafePublication.ql +++ b/java/ql/src/Likely Bugs/Concurrency/SafePublication.ql @@ -77,7 +77,7 @@ predicate isAssignedDefaultValue(Field f) { } predicate isSafelyPublished(Field f) { - f.isFinal() or // TODO: Consider non-primitive types + f.isFinal() or // NOTE: For non-primitive types, 'final' alone does not guarantee safe publication unless the object is immutable or safely constructed. Consider reviewing the handling of non-primitive fields for safe publication. f.isStatic() or f.isVolatile() or isThreadSafeType(f.getType()) or diff --git a/java/ql/test/query-tests/ThreadSafe/examples/LockExample.java b/java/ql/test/query-tests/ThreadSafe/examples/LockExample.java index 92886bbb5ffb..8ce34922c5b6 100644 --- a/java/ql/test/query-tests/ThreadSafe/examples/LockExample.java +++ b/java/ql/test/query-tests/ThreadSafe/examples/LockExample.java @@ -3,7 +3,7 @@ // If the variable is involved in several different monitors, we get an alert for each monitor that // is not correctly used. // A single alert can have many related locations, since each conflicting access which is not -// prpoerly synchronized is a related location. +// properly synchronized is a related location. // This leads to many lines in the .expected file. package examples; diff --git a/java/ql/test/query-tests/ThreadSafe/examples/Test.java b/java/ql/test/query-tests/ThreadSafe/examples/Test.java index 55fef174fc54..b2e7ac46c0bf 100644 --- a/java/ql/test/query-tests/ThreadSafe/examples/Test.java +++ b/java/ql/test/query-tests/ThreadSafe/examples/Test.java @@ -5,14 +5,14 @@ @ThreadSafe public class Test { /** - * Escaping field due to public visuability. + * Escaping field due to public visibility. */ int publicField; private int y; final int immutableField = 1; - // As of the below examples with synchronized as well. Except the incorretly placed lock. + // As of the below examples with synchronized as well. Except the incorrectly placed lock. private Lock lock = new ReentrantLock(); @@ -53,7 +53,7 @@ private void setYPrivate(int y) { } /** - * Incorretly locks y. + * Incorrectly locks y. * @param y */ public void setYWrongLock(int y) { From 26c1b2f14316ccda78f8878769d84a3fc069cedc Mon Sep 17 00:00:00 2001 From: yoff Date: Thu, 9 Oct 2025 12:29:42 +0200 Subject: [PATCH 12/25] java: adjust test expectations; new queries are enabled in extended --- .../java/query-suite/java-code-quality-extended.qls.expected | 3 +++ 1 file changed, 3 insertions(+) diff --git a/java/ql/integration-tests/java/query-suite/java-code-quality-extended.qls.expected b/java/ql/integration-tests/java/query-suite/java-code-quality-extended.qls.expected index cdd6769ab46f..6d0319431d6f 100644 --- a/java/ql/integration-tests/java/query-suite/java-code-quality-extended.qls.expected +++ b/java/ql/integration-tests/java/query-suite/java-code-quality-extended.qls.expected @@ -67,15 +67,18 @@ ql/java/ql/src/Likely Bugs/Concurrency/CallsToRunnableRun.ql ql/java/ql/src/Likely Bugs/Concurrency/DateFormatThreadUnsafe.ql ql/java/ql/src/Likely Bugs/Concurrency/DoubleCheckedLocking.ql ql/java/ql/src/Likely Bugs/Concurrency/DoubleCheckedLockingWithInitRace.ql +ql/java/ql/src/Likely Bugs/Concurrency/Escaping.ql ql/java/ql/src/Likely Bugs/Concurrency/FutileSynchOnField.ql ql/java/ql/src/Likely Bugs/Concurrency/NonSynchronizedOverride.ql ql/java/ql/src/Likely Bugs/Concurrency/NotifyNotNotifyAll.ql +ql/java/ql/src/Likely Bugs/Concurrency/SafePublication.ql ql/java/ql/src/Likely Bugs/Concurrency/ScheduledThreadPoolExecutorZeroThread.ql ql/java/ql/src/Likely Bugs/Concurrency/SleepWithLock.ql ql/java/ql/src/Likely Bugs/Concurrency/StartInConstructor.ql ql/java/ql/src/Likely Bugs/Concurrency/SynchOnBoxedType.ql ql/java/ql/src/Likely Bugs/Concurrency/SynchSetUnsynchGet.ql ql/java/ql/src/Likely Bugs/Concurrency/SynchWriteObject.ql +ql/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql ql/java/ql/src/Likely Bugs/Finalization/NullifiedSuperFinalize.ql ql/java/ql/src/Likely Bugs/Frameworks/JUnit/BadSuiteMethod.ql ql/java/ql/src/Likely Bugs/Frameworks/JUnit/JUnit5MissingNestedAnnotation.ql From f90e9dbb5ebb51596536f9eb73093806491b0fc6 Mon Sep 17 00:00:00 2001 From: yoff Date: Thu, 9 Oct 2025 13:01:25 +0200 Subject: [PATCH 13/25] java: favour `inline_late` over `inline` This gives much greater control over the join-order --- java/ql/lib/semmle/code/java/ConflictingAccess.qll | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index 1243a94d6615..ae76e0fa46eb 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -11,8 +11,9 @@ import Concurrency * Holds if `t` is the type of a lock. * Currently a crude test of the type name. */ +bindingset[t] overlay[caller?] -pragma[inline] +pragma[inline_late] predicate isLockType(Type t) { t.getName().matches("%Lock%") } /** @@ -211,8 +212,9 @@ class ExposedFieldAccess extends FieldAccess { } /** Holds if the location of `a` is strictly before the location of `b`. */ +bindingset[a, b] overlay[caller?] -pragma[inline] +pragma[inline_late] predicate orderedLocations(Location a, Location b) { a.getStartLine() < b.getStartLine() or From 1ad239459f505f7da741ec13fa93fd054a1e1033 Mon Sep 17 00:00:00 2001 From: yoff Date: Thu, 9 Oct 2025 13:36:35 +0200 Subject: [PATCH 14/25] java: move shared code into `Concurrency.qll` --- java/ql/lib/semmle/code/java/Concurrency.qll | 161 ++++++++++++++++++ .../semmle/code/java/ConflictingAccess.qll | 129 +------------- .../Likely Bugs/Concurrency/UnreleasedLock.ql | 42 +---- 3 files changed, 163 insertions(+), 169 deletions(-) diff --git a/java/ql/lib/semmle/code/java/Concurrency.qll b/java/ql/lib/semmle/code/java/Concurrency.qll index 7322f16068c0..f32c7ee963cc 100644 --- a/java/ql/lib/semmle/code/java/Concurrency.qll +++ b/java/ql/lib/semmle/code/java/Concurrency.qll @@ -2,6 +2,47 @@ overlay[local?] module; import java +import semmle.code.java.frameworks.Mockito + +class LockType extends RefType { + LockType() { + this.getAMethod().hasName("lock") and + this.getAMethod().hasName("unlock") + } + + Method getLockMethod() { + result.getDeclaringType() = this and + result.hasName(["lock", "lockInterruptibly", "tryLock"]) + } + + Method getUnlockMethod() { + result.getDeclaringType() = this and + result.hasName("unlock") + } + + Method getIsHeldByCurrentThreadMethod() { + result.getDeclaringType() = this and + result.hasName("isHeldByCurrentThread") + } + + MethodCall getLockAccess() { + result.getMethod() = this.getLockMethod() and + // Not part of a Mockito verification call + not result instanceof MockitoVerifiedMethodCall + } + + MethodCall getUnlockAccess() { + result.getMethod() = this.getUnlockMethod() and + // Not part of a Mockito verification call + not result instanceof MockitoVerifiedMethodCall + } + + MethodCall getIsHeldByCurrentThreadAccess() { + result.getMethod() = this.getIsHeldByCurrentThreadMethod() and + // Not part of a Mockito verification call + not result instanceof MockitoVerifiedMethodCall + } +} /** * Holds if `e` is synchronized by a local synchronized statement `sync` on the variable `v`. @@ -49,3 +90,123 @@ class SynchronizedCallable extends Callable { ) } } + +/** + * This module provides predicates, chiefly `locallyMonitors`, to check if a given expression is synchronized on a specific monitor. + */ +module Monitors { + /** + * A monitor is any object that is used to synchronize access to a shared resource. + * This includes locks as well as variables used in synchronized blocks (including `this`). + */ + newtype TMonitor = + /** Either a lock or a variable used in a synchronized block. */ + TVariableMonitor(Variable v) { + v.getType() instanceof LockType or locallySynchronizedOn(_, _, v) + } or + /** An instance reference used as a monitor. */ + TInstanceMonitor(RefType thisType) { locallySynchronizedOnThis(_, thisType) } or + /** A class used as a monitor. */ + TClassMonitor(RefType classType) { locallySynchronizedOnClass(_, classType) } + + /** + * A monitor is any object that is used to synchronize access to a shared resource. + * This includes locks as well as variables used in synchronized blocks (including `this`). + */ + class Monitor extends TMonitor { + /** Gets the location of this monitor. */ + abstract Location getLocation(); + + /** Gets a textual representation of this element. */ + abstract string toString(); + } + + /** + * A variable used as a monitor. + * The variable is either a lock or is used in a synchronized block. + * E.g `synchronized (m) { ... }` or `m.lock();` + */ + class VariableMonitor extends Monitor, TVariableMonitor { + override Location getLocation() { result = this.getVariable().getLocation() } + + override string toString() { result = "VariableMonitor(" + this.getVariable().toString() + ")" } + + /** Gets the variable being used as a monitor. */ + Variable getVariable() { this = TVariableMonitor(result) } + } + + /** + * An instance reference used as a monitor. + * Either via `synchronized (this) { ... }` or by marking a non-static method as `synchronized`. + */ + class InstanceMonitor extends Monitor, TInstanceMonitor { + override Location getLocation() { result = this.getThisType().getLocation() } + + override string toString() { result = "InstanceMonitor(" + this.getThisType().toString() + ")" } + + /** Gets the instance reference being used as a monitor. */ + RefType getThisType() { this = TInstanceMonitor(result) } + } + + /** + * A class used as a monitor. + * This is achieved by marking a static method as `synchronized`. + */ + class ClassMonitor extends Monitor, TClassMonitor { + override Location getLocation() { result = this.getClassType().getLocation() } + + override string toString() { result = "ClassMonitor(" + this.getClassType().toString() + ")" } + + /** Gets the class being used as a monitor. */ + RefType getClassType() { this = TClassMonitor(result) } + } + + /** Holds if the expression `e` is synchronized on the monitor `m`. */ + predicate locallyMonitors(Expr e, Monitor m) { + exists(Variable v | v = m.(VariableMonitor).getVariable() | + locallyLockedOn(e, v) + or + locallySynchronizedOn(e, _, v) + ) + or + locallySynchronizedOnThis(e, m.(InstanceMonitor).getThisType()) + or + 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 + exists(Assignment asgn | asgn.getDest() = e | result = asgn.getControlFlowNode()) + or + // if `e` is not the LHS of an assignment, use the default control flow node + not exists(Assignment asgn | asgn.getDest() = e) and + result = e.getControlFlowNode() + } + + /** 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.getMethod() = lock.getType().(LockType).getLockMethod() and + unlockCall.getQualifier() = localLock.getAnAccess() and + unlockCall.getMethod() = lock.getType().(LockType).getUnlockMethod() + | + dominates(lockCall.getControlFlowNode(), unlockCall.getControlFlowNode()) and + dominates(lockCall.getControlFlowNode(), getNodeToBeDominated(e)) and + postDominates(unlockCall.getControlFlowNode(), getNodeToBeDominated(e)) + ) + } +} diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index ae76e0fa46eb..c98fb3bdf3bc 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -7,133 +7,6 @@ module; import java import Concurrency -/** - * Holds if `t` is the type of a lock. - * Currently a crude test of the type name. - */ -bindingset[t] -overlay[caller?] -pragma[inline_late] -predicate isLockType(Type t) { t.getName().matches("%Lock%") } - -/** - * This module provides predicates, chiefly `locallyMonitors`, to check if a given expression is synchronized on a specific monitor. - */ -module Monitors { - /** - * A monitor is any object that is used to synchronize access to a shared resource. - * This includes locks as well as variables used in synchronized blocks (including `this`). - */ - newtype TMonitor = - /** Either a lock or a variable used in a synchronized block. */ - TVariableMonitor(Variable v) { isLockType(v.getType()) or locallySynchronizedOn(_, _, v) } or - /** An instance reference used as a monitor. */ - TInstanceMonitor(RefType thisType) { locallySynchronizedOnThis(_, thisType) } or - /** A class used as a monitor. */ - TClassMonitor(RefType classType) { locallySynchronizedOnClass(_, classType) } - - /** - * A monitor is any object that is used to synchronize access to a shared resource. - * This includes locks as well as variables used in synchronized blocks (including `this`). - */ - class Monitor extends TMonitor { - /** Gets the location of this monitor. */ - abstract Location getLocation(); - - /** Gets a textual representation of this element. */ - abstract string toString(); - } - - /** - * A variable used as a monitor. - * The variable is either a lock or is used in a synchronized block. - * E.g `synchronized (m) { ... }` or `m.lock();` - */ - class VariableMonitor extends Monitor, TVariableMonitor { - override Location getLocation() { result = this.getVariable().getLocation() } - - override string toString() { result = "VariableMonitor(" + this.getVariable().toString() + ")" } - - /** Gets the variable being used as a monitor. */ - Variable getVariable() { this = TVariableMonitor(result) } - } - - /** - * An instance reference used as a monitor. - * Either via `synchronized (this) { ... }` or by marking a non-static method as `synchronized`. - */ - class InstanceMonitor extends Monitor, TInstanceMonitor { - override Location getLocation() { result = this.getThisType().getLocation() } - - override string toString() { result = "InstanceMonitor(" + this.getThisType().toString() + ")" } - - /** Gets the instance reference being used as a monitor. */ - RefType getThisType() { this = TInstanceMonitor(result) } - } - - /** - * A class used as a monitor. - * This is achieved by marking a static method as `synchronized`. - */ - class ClassMonitor extends Monitor, TClassMonitor { - override Location getLocation() { result = this.getClassType().getLocation() } - - override string toString() { result = "ClassMonitor(" + this.getClassType().toString() + ")" } - - /** Gets the class being used as a monitor. */ - RefType getClassType() { this = TClassMonitor(result) } - } - - /** Holds if the expression `e` is synchronized on the monitor `m`. */ - predicate locallyMonitors(Expr e, Monitor m) { - exists(Variable v | v = m.(VariableMonitor).getVariable() | - locallyLockedOn(e, v) - or - locallySynchronizedOn(e, _, v) - ) - or - locallySynchronizedOnThis(e, m.(InstanceMonitor).getThisType()) - or - locallySynchronizedOnClass(e, m.(ClassMonitor).getClassType()) - } - - /** Holds if `localLock` refers to `lock`. */ - predicate represents(Field lock, Variable localLock) { - isLockType(lock.getType()) 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 - exists(Assignment asgn | asgn.getDest() = e | result = asgn.getControlFlowNode()) - or - // if `e` is not the LHS of an assignment, use the default control flow node - not exists(Assignment asgn | asgn.getDest() = e) and - result = e.getControlFlowNode() - } - - /** Holds if `e` is synchronized on the `Lock` `lock` by a locking call. */ - predicate locallyLockedOn(Expr e, Field lock) { - isLockType(lock.getType()) and - exists(Variable localLock, MethodCall lockCall, MethodCall unlockCall | - represents(lock, localLock) and - lockCall.getQualifier() = localLock.getAnAccess() and - lockCall.getMethod().getName() in ["lock", "lockInterruptibly", "tryLock"] and - unlockCall.getQualifier() = localLock.getAnAccess() and - unlockCall.getMethod().getName() = "unlock" - | - dominates(lockCall.getControlFlowNode(), unlockCall.getControlFlowNode()) and - dominates(lockCall.getControlFlowNode(), getNodeToBeDominated(e)) and - postDominates(unlockCall.getControlFlowNode(), getNodeToBeDominated(e)) - ) - } -} - /** Provides predicates, chiefly `isModifying`, to check if a given expression modifies a shared resource. */ module Modification { import semmle.code.java.dataflow.FlowSummary @@ -183,7 +56,7 @@ class ExposedField extends Field { this.getDeclaringType() instanceof ClassAnnotatedAsThreadSafe and not this.isVolatile() and // field is not a lock - not isLockType(this.getType()) and + not this.getType() instanceof LockType and // field is not thread-safe not isThreadSafeType(this.getType()) and not isThreadSafeType(this.getInitializer().getType()) and diff --git a/java/ql/src/Likely Bugs/Concurrency/UnreleasedLock.ql b/java/ql/src/Likely Bugs/Concurrency/UnreleasedLock.ql index 118593e31fe8..c7d33eff4a99 100644 --- a/java/ql/src/Likely Bugs/Concurrency/UnreleasedLock.ql +++ b/java/ql/src/Likely Bugs/Concurrency/UnreleasedLock.ql @@ -16,47 +16,7 @@ import java import semmle.code.java.controlflow.Guards import semmle.code.java.dataflow.SSA -import semmle.code.java.frameworks.Mockito - -class LockType extends RefType { - LockType() { - this.getAMethod().hasName("lock") and - this.getAMethod().hasName("unlock") - } - - Method getLockMethod() { - result.getDeclaringType() = this and - (result.hasName("lock") or result.hasName("tryLock")) - } - - Method getUnlockMethod() { - result.getDeclaringType() = this and - result.hasName("unlock") - } - - Method getIsHeldByCurrentThreadMethod() { - result.getDeclaringType() = this and - result.hasName("isHeldByCurrentThread") - } - - MethodCall getLockAccess() { - result.getMethod() = this.getLockMethod() and - // Not part of a Mockito verification call - not result instanceof MockitoVerifiedMethodCall - } - - MethodCall getUnlockAccess() { - result.getMethod() = this.getUnlockMethod() and - // Not part of a Mockito verification call - not result instanceof MockitoVerifiedMethodCall - } - - MethodCall getIsHeldByCurrentThreadAccess() { - result.getMethod() = this.getIsHeldByCurrentThreadMethod() and - // Not part of a Mockito verification call - not result instanceof MockitoVerifiedMethodCall - } -} +import semmle.code.java.Concurrency predicate lockBlock(LockType t, BasicBlock b, int locks) { locks = strictcount(int i | b.getNode(i).asExpr() = t.getLockAccess()) From 5109babd928a0733782d398d421fce4301b8baa8 Mon Sep 17 00:00:00 2001 From: yoff Date: Thu, 9 Oct 2025 14:20:28 +0200 Subject: [PATCH 15/25] java: add qldoc These interfaces were previously in a .ql file. Also, use the XXAccess variants. --- java/ql/lib/semmle/code/java/Concurrency.qll | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/java/ql/lib/semmle/code/java/Concurrency.qll b/java/ql/lib/semmle/code/java/Concurrency.qll index f32c7ee963cc..7fbf0647b277 100644 --- a/java/ql/lib/semmle/code/java/Concurrency.qll +++ b/java/ql/lib/semmle/code/java/Concurrency.qll @@ -4,39 +4,49 @@ module; import java import semmle.code.java.frameworks.Mockito +/** + * A Java type representing a lock. + * We identify a lock type as one that has both `lock` and `unlock` methods. + */ class LockType extends RefType { LockType() { this.getAMethod().hasName("lock") and this.getAMethod().hasName("unlock") } + /** Gets a method that is locking this lock type. */ Method getLockMethod() { result.getDeclaringType() = this and result.hasName(["lock", "lockInterruptibly", "tryLock"]) } + /** Gets a method that is unlocking this lock type. */ Method getUnlockMethod() { result.getDeclaringType() = this and result.hasName("unlock") } + /** Gets an `isHeldByCurrentThread` method of this lock type. */ Method getIsHeldByCurrentThreadMethod() { result.getDeclaringType() = this and result.hasName("isHeldByCurrentThread") } + /** Gets a call to a method that is locking this lock type. */ MethodCall getLockAccess() { result.getMethod() = this.getLockMethod() and // Not part of a Mockito verification call not result instanceof MockitoVerifiedMethodCall } + /** Gets a call to a method that is unlocking this lock type. */ MethodCall getUnlockAccess() { result.getMethod() = this.getUnlockMethod() and // Not part of a Mockito verification call not result instanceof MockitoVerifiedMethodCall } + /** Gets a call to a method that checks if the lock is held by the current thread. */ MethodCall getIsHeldByCurrentThreadAccess() { result.getMethod() = this.getIsHeldByCurrentThreadMethod() and // Not part of a Mockito verification call @@ -200,9 +210,9 @@ module Monitors { exists(Variable localLock, MethodCall lockCall, MethodCall unlockCall | represents(lock, localLock) and lockCall.getQualifier() = localLock.getAnAccess() and - lockCall.getMethod() = lock.getType().(LockType).getLockMethod() and + lockCall = lock.getType().(LockType).getLockAccess() and unlockCall.getQualifier() = localLock.getAnAccess() and - unlockCall.getMethod() = lock.getType().(LockType).getUnlockMethod() + unlockCall = lock.getType().(LockType).getUnlockAccess() | dominates(lockCall.getControlFlowNode(), unlockCall.getControlFlowNode()) and dominates(lockCall.getControlFlowNode(), getNodeToBeDominated(e)) and From 61a3e9630f9e7579491894a99948632cb1e57404 Mon Sep 17 00:00:00 2001 From: yoff Date: Fri, 17 Oct 2025 01:39:29 +0200 Subject: [PATCH 16/25] java: rewrite conflict detection - favour unary predicates over binary ones (the natural "conflicting access" is binary) - switch to a dual solution to trade recursion through forall for simple existentials. Co-authored-by: Anders Schack-Mulligen --- .../semmle/code/java/ConflictingAccess.qll | 344 ++++++++---------- .../src/Likely Bugs/Concurrency/ThreadSafe.ql | 46 ++- .../ThreadSafe/ThreadSafe.expected | 115 +++--- .../query-tests/ThreadSafe/examples/C.java | 16 +- .../examples/FaultyTurnstileExample.java | 8 +- .../ThreadSafe/examples/FlawedSemaphore.java | 2 +- .../ThreadSafe/examples/LockExample.java | 46 +-- .../ThreadSafe/examples/SyncLstExample.java | 4 +- .../ThreadSafe/examples/SyncStackExample.java | 4 +- .../examples/SynchronizedAndLock.java | 4 +- .../query-tests/ThreadSafe/examples/Test.java | 8 +- 11 files changed, 285 insertions(+), 312 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index c98fb3bdf3bc..9373845d6bca 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -44,7 +44,11 @@ predicate isThreadSafeType(Type t) { /** Holds if the expression `e` is a thread-safe initializer. */ predicate isThreadSafeInitializer(Expr e) { - e.(Call).getCallee().getQualifiedName().matches("java.util.Collections.synchronized%") + e.(Call) + .getCallee() + .getSourceDeclaration() + .getQualifiedName() + .matches("java.util.Collections.synchronized%") } /** @@ -84,17 +88,6 @@ class ExposedFieldAccess extends FieldAccess { } } -/** Holds if the location of `a` is strictly before the location of `b`. */ -bindingset[a, b] -overlay[caller?] -pragma[inline_late] -predicate orderedLocations(Location a, Location b) { - a.getStartLine() < b.getStartLine() - or - a.getStartLine() = b.getStartLine() and - a.getStartColumn() < b.getStartColumn() -} - /** * A class annotated as `@ThreadSafe`. * Provides predicates to check for concurrency issues. @@ -102,213 +95,192 @@ predicate orderedLocations(Location a, Location b) { class ClassAnnotatedAsThreadSafe extends Class { ClassAnnotatedAsThreadSafe() { this.getAnAnnotation().getType().getName() = "ThreadSafe" } - /** Holds if `a` and `b` are conflicting accesses to the same field and not monitored by the same monitor. */ - predicate unsynchronised(ExposedFieldAccess a, ExposedFieldAccess b) { - this.conflicting(a, b) and - this.publicAccess(_, a) and - this.publicAccess(_, b) and - not exists(Monitors::Monitor m | - this.monitors(a, m) and - this.monitors(b, m) - ) - } - - /** Holds if `a` is the earliest write to its field that is unsynchronized with `b`. */ - predicate unsynchronised_normalized(ExposedFieldAccess a, ExposedFieldAccess b) { - this.unsynchronised(a, b) and - // Eliminate double reporting by making `a` the earliest write to this field - // that is unsynchronized with `b`. - not exists(ExposedFieldAccess earlier_a | - earlier_a.getField() = a.getField() and - orderedLocations(earlier_a.getLocation(), a.getLocation()) - | - this.unsynchronised(earlier_a, b) - ) - } - - /** - * Holds if `a` and `b` are unsynchronized and both publicly accessible - * as witnessed by `witness_a` and `witness_b`. - */ - predicate witness(ExposedFieldAccess a, Expr witness_a, ExposedFieldAccess b, Expr witness_b) { - this.unsynchronised_normalized(a, b) and - this.publicAccess(witness_a, a) and - this.publicAccess(witness_b, b) and - // avoid double reporting - not exists(Expr better_witness_a | this.publicAccess(better_witness_a, a) | - orderedLocations(better_witness_a.getLocation(), witness_a.getLocation()) - ) and - not exists(Expr better_witness_b | this.publicAccess(better_witness_b, b) | - orderedLocations(better_witness_b.getLocation(), witness_b.getLocation()) - ) - } - + // We wish to find conflicting accesses that are reachable from public methods + // and to know which monitors protect them. + // + // It is very easy and natural to write a predicate for conflicting accesses, + // but that would be binary, and hence not suited for reachability analysis. + // + // It is also easy to state that all accesses to a field are protected by a single monitor, + // but that would require a forall, which is not suited for recursion. + // (The recursion occurs for example as you traverse the access path and keep requiring that all tails are protected.) + // + // We therefore use a dual solution: + // - We write a unary recursive predicate for accesses that are not protected by any monitor. + // Any such write access, reachable from a public method, is conflicting with itself. + // And any such read will be conflicting with any publicly reachable write access (locked or not). + // + // - We project the above predicate down to fields, so we can find fields with unprotected accesses. + // - From this we can derive a unary recursive predicate for fields whose accesses are protected by exactly one monitor. + // The predicate tracks the monitor. + // If such a field has two accesses protected by different monitors, we have a concurrency issue. + // This can be determined by simple counting at the end of the recursion. + // Technically, we only have a concurrency issue if there is a write access, + // but if you are locking your reads with different locks, you likely made a typo. + // + // - From the above, we can derive a unary recursive predicate for fields whose accesses are protected by at least one monitor. + // This predicate tracks all the monitors that protect accesses to the field. + // This is combined with a predicate that checks if any access escapes a given monitor. + // If all the monitors that protect accesses to a field are escaped by at least one access, + // we have a concurrency issue. + // This can be determined by a single forall at the end of the recursion. + // + // With this formulation we avoid binary predicates and foralls in recursion. + // + // Cases where a field access is not protected by any monitor /** - * Actions `a` and `b` are conflicting iff - * they are field access operations on the same field and - * at least one of them is a write. + * Holds if the field access `a` to the field `f` is not protected by any monitor, and it can be reached via the expression `e` in the method `m`. + * We maintain the invariant that `m = e.getEnclosingCallable()`. */ - predicate conflicting(ExposedFieldAccess a, ExposedFieldAccess b) { - // We allow a = b, since they could be executed on different threads - // We are looking for two operations: - // - on the same non-volatile field - a.getField() = b.getField() and - // - on this class - a.getField() = this.getAField() and - // - where at least one is a write - // wlog we assume that is `a` - // We use a slightly more inclusive definition than simply `a.isVarWrite()` - Modification::isModifying(a) and - // Avoid reporting both `(a, b)` and `(b, a)` by choosing the tuple - // where `a` appears before `b` in the source code. + predicate unlocked_access(ExposedField f, Expr e, Method m, ExposedFieldAccess a, boolean write) { + m.getDeclaringType() = this and ( - ( - Modification::isModifying(b) and - a != b + // base case + f.getDeclaringType() = this and + m = e.getEnclosingCallable() and + a.getField() = f and + a = e and + (if Modification::isModifying(a) then write = true else write = false) + or + // recursive case + exists(MethodCall c, Expr e0, Method m0 | this.unlocked_access(f, e0, m0, a, write) | + m = c.getEnclosingCallable() and + not m0.isPublic() and + c.getCallee().getSourceDeclaration() = m0 and + c = e and + not Monitors::locallyMonitors(e0, _) ) - implies - orderedLocations(a.getLocation(), b.getLocation()) ) } - /** Holds if `a` can be reached by a path from a public method, and all such paths are monitored by `monitor`. */ - predicate monitors(ExposedFieldAccess a, Monitors::Monitor monitor) { - forex(Method m | this.providesAccess(m, _, a) and m.isPublic() | - this.monitorsVia(m, a, monitor) - ) + /** Holds if the class has an unlocked access to the field `f` via the expression `e` in the method `m`. */ + predicate has_unlocked_access(ExposedField f, Expr e, Method m, boolean write) { + this.unlocked_access(f, e, m, _, write) } - /** Holds if `a` can be reached by a path from a public method and `e` is the expression in that method that starts the path. */ - predicate publicAccess(Expr e, ExposedFieldAccess a) { - exists(Method m | m.isPublic() | this.providesAccess(m, e, a)) + /** Holds if the field access `a` to the field `f` is not protected by any monitor, and it can be reached via the expression `e` in the public method `m`. */ + predicate unlocked_public_access( + ExposedField f, Expr e, Method m, ExposedFieldAccess a, boolean write + ) { + this.unlocked_access(f, e, m, a, write) and + m.isPublic() and + not Monitors::locallyMonitors(e, _) } - /** - * Holds if a call to method `m` can cause an access of `a` and `e` is the expression inside `m` that leads to that access. - * `e` will either be `a` itself or a method call that leads to `a`. - */ - predicate providesAccess(Method m, Expr e, ExposedFieldAccess a) { - m = this.getAMethod() and - ( - a.getEnclosingCallable() = m and - e = a - or - exists(MethodCall c | c.getEnclosingCallable() = m | - this.providesAccess(c.getCallee(), _, a) and - e = c - ) - ) + /** Holds if the class has an unlocked access to the field `f` via the expression `e` in the public method `m`. */ + predicate has_unlocked_public_access(ExposedField f, Expr e, Method m, boolean write) { + this.unlocked_public_access(f, e, m, _, write) } - // NOTE: - // In order to deal with loops in the call graph, we compute the strongly connected components (SCCs). - // We only wish to do this for the methods that can lead to exposed field accesses. - // Given a field access `a`, we can consider a "call graph of interest", a sub graph of the call graph - // that only contains methods that lead to an access of `a`. We call this "the call graph induced by `a`". - // We can then compute the SCCs of this graph, yielding the SCC graph induced by `a`. + // Cases where all accesses to a field are protected by exactly one monitor // /** - * Holds if a call to method `m` can cause an access of `a` by `m` calling `callee`. - * This is an edge in the call graph induced by `a`. + * Holds if the class has an access, locked by exactly one monitor, to the field `f` via the expression `e` in the method `m`. */ - predicate accessVia(Method m, ExposedFieldAccess a, Method callee) { - exists(MethodCall c | this.providesAccess(m, c, a) | callee = c.getCallee()) - } - - /** Holds if `m` can reach `reached` by a path in the call graph induced by `a`. */ - predicate accessReach(Method m, ExposedFieldAccess a, Method reached) { - m = this.getAMethod() and - reached = this.getAMethod() and - this.providesAccess(m, _, a) and - this.providesAccess(reached, _, a) and - ( - this.accessVia(m, a, reached) - or - exists(Method mid | this.accessReach(m, a, mid) | this.accessVia(mid, a, reached)) + predicate has_onelocked_access( + ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor + ) { + //base + this.has_unlocked_access(f, e, m, write) and + Monitors::locallyMonitors(e, monitor) + or + // recursive case + exists(MethodCall c, Expr e0, Method m0 | this.has_onelocked_access(f, e0, m0, write, monitor) | + m = c.getEnclosingCallable() and + not m0.isPublic() and + c.getCallee().getSourceDeclaration() = m0 and + c = e and + // consider allowing idempotent monitors + not Monitors::locallyMonitors(e, _) and + m.getDeclaringType() = this ) } - /** - * Holds if `rep` is a representative of the SCC containing `m` in the call graph induced by `a`. - * This only assigns representatives to methods involved in loops. - * To get a representative of any method, use `repScc`. - */ - predicate repInLoopScc(Method rep, ExposedFieldAccess a, Method m) { - // `rep` and `m` are in the same SCC - this.accessReach(rep, a, m) and - this.accessReach(m, a, rep) and - // `rep` is the representative of the SCC - // that is, the earliest in the source code - forall(Method alt_rep | - rep != alt_rep and - this.accessReach(alt_rep, a, m) and - this.accessReach(m, a, alt_rep) - | - rep.getLocation().getStartLine() < alt_rep.getLocation().getStartLine() - ) + /** Holds if the class has an access, locked by exactly one monitor, to the field `f` via the expression `e` in the public method `m`. */ + predicate has_onelocked_public_access( + ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor + ) { + this.has_onelocked_access(f, e, m, write, monitor) and + m.isPublic() and + not this.has_unlocked_public_access(f, e, m, write) } - /** Holds if `rep` is a representative of the SCC containing `m` in the call graph induced by `a`. */ - predicate repScc(Method rep, ExposedFieldAccess a, Method m) { - this.repInLoopScc(rep, a, m) - or - // If `m` is in the call graph induced by `a` and did not get a representative from `repInLoopScc`, - // it is represented by itself. - m = this.getAMethod() and - this.providesAccess(m, _, a) and - not this.repInLoopScc(_, a, m) and - rep = m + /** Holds if the field `f` has more than one access, all locked by a single monitor, but different monitors are used. */ + predicate single_monitor_mismatch(ExposedField f) { + 2 <= + strictcount(Monitors::Monitor monitor | this.has_onelocked_public_access(f, _, _, _, monitor)) } - /** - * Holds if `c` is a call from the SCC represented by `callerRep` to the (different) SCC represented by `calleeRep`. - * This is an edge in the SCC graph induced by `a`. - */ - predicate callEdgeScc(Method callerRep, ExposedFieldAccess a, MethodCall c, Method calleeRep) { - callerRep != calleeRep and - exists(Method caller, Method callee | - this.repScc(callerRep, a, caller) and - this.repScc(calleeRep, a, callee) + // Cases where all accesses to a field are protected by at least one monitor + // + /** Holds if the class has an access, locked by at least one monitor, to the field `f` via the expression `e` in the method `m`. */ + predicate has_onepluslocked_access( + ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor + ) { + //base + this.has_onelocked_access(f, e, m, write, monitor) and + not this.single_monitor_mismatch(f) and + not this.has_unlocked_public_access(f, _, _, _) + or + // recursive case + exists(MethodCall c, Expr e0, Method m0, Monitors::Monitor monitor0 | + this.has_onepluslocked_access(f, e0, m0, write, monitor0) and + m = c.getEnclosingCallable() and + not m0.isPublic() and + c.getCallee().getSourceDeclaration() = m0 and + c = e and + m.getDeclaringType() = this | - this.accessVia(caller, a, callee) and - c.getEnclosingCallable() = caller and - c.getCallee() = callee + monitor = monitor0 + or + Monitors::locallyMonitors(e, monitor) ) } - /** - * Holds if the SCC represented by `rep` can cause an access to `a` and `e` is the expression that leads to that access. - * `e` will either be `a` itself or a method call that leads to `a` via a different SCC. - */ - predicate providesAccessScc(Method rep, Expr e, ExposedFieldAccess a) { - rep = this.getAMethod() and - exists(Method m | this.repScc(rep, a, m) | - a.getEnclosingCallable() = m and - e = a - or - exists(MethodCall c | this.callEdgeScc(rep, a, c, _) | e = c) + /** Holds if the class has a write access to the field `f` that can be reached via a public method. */ + predicate has_public_write_access(ExposedField f) { + this.has_unlocked_public_access(f, _, _, true) + or + this.has_onelocked_public_access(f, _, _, true, _) + or + exists(Method m | m.getDeclaringType() = this and m.isPublic() | + this.has_onepluslocked_access(f, _, m, true, _) ) } - /** Holds if all paths from `rep` to `a` are monitored by `monitor`. */ - predicate monitorsViaScc(Method rep, ExposedFieldAccess a, Monitors::Monitor monitor) { - rep = this.getAMethod() and - this.providesAccessScc(rep, _, a) and - // If we are in an SCC that can access `a`, the access must be monitored locally - (this.repScc(rep, a, a.getEnclosingCallable()) implies Monitors::locallyMonitors(a, monitor)) and - // Any call towards `a` must either be monitored or guarantee that the access is monitored - forall(MethodCall c, Method calleeRep | this.callEdgeScc(rep, a, c, calleeRep) | - Monitors::locallyMonitors(c, monitor) - or - this.monitorsViaScc(calleeRep, a, monitor) + /** Holds if the class has an access, not protected by the monitor `m`, to the field `f` via the expression `e` in the method `m`. */ + predicate escapes_monitor( + ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor + ) { + //base + this.has_onepluslocked_access(f, _, _, _, monitor) and + this.has_unlocked_access(f, e, m, write) and + not Monitors::locallyMonitors(e, monitor) + or + // recursive case + exists(MethodCall c, Expr e0, Method m0 | this.escapes_monitor(f, e0, m0, write, monitor) | + m = c.getEnclosingCallable() and + not m0.isPublic() and + c.getCallee().getSourceDeclaration() = m0 and + c = e and + // consider allowing idempotent monitors + not Monitors::locallyMonitors(e, monitor) and + m.getDeclaringType() = this ) } - /** Holds if all paths from `m` to `a` are monitored by `monitor`. */ - predicate monitorsVia(Method m, ExposedFieldAccess a, Monitors::Monitor monitor) { - exists(Method rep | - this.repScc(rep, a, m) and - this.monitorsViaScc(rep, a, monitor) + /** Holds if the class has an access, not protected by the monitor `m`, to the field `f` via the expression `e` in the public method `m`. */ + predicate escapes_monitor_public( + ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor + ) { + this.escapes_monitor(f, e, m, write, monitor) and + m.isPublic() + } + + /** Holds if no monitor protects all accesses to the field `f`. */ + predicate not_fully_monitored(ExposedField f) { + forex(Monitors::Monitor monitor | this.has_onepluslocked_access(f, _, _, _, monitor) | + this.escapes_monitor_public(f, _, _, _, monitor) ) } } diff --git a/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql b/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql index 1498274131e1..89e9cbdb169b 100644 --- a/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql +++ b/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql @@ -14,13 +14,43 @@ import java import semmle.code.java.ConflictingAccess +predicate unmonitored_access( + ClassAnnotatedAsThreadSafe cls, ExposedFieldAccess a, Expr entry, string msg, string entry_desc +) { + exists(ExposedField f | + cls.unlocked_public_access(f, entry, _, a, true) + or + cls.unlocked_public_access(f, entry, _, a, false) and + cls.has_public_write_access(f) + ) and + msg = + "This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe." and + entry_desc = "this expression" +} + +predicate not_fully_monitored_field( + ClassAnnotatedAsThreadSafe cls, ExposedField f, string msg, string cls_name +) { + ( + // Technically there has to be a write access for a conflict to exist. + // But if you are locking your reads with different locks, you likely made a typo, + // so in this case we alert without requiring `cls.has_public_write_access(f)` + cls.single_monitor_mismatch(f) + or + cls.not_fully_monitored(f) and + cls.has_public_write_access(f) + ) and + msg = + "The field $@ is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe." and + cls_name = cls.getName() +} + from - ClassAnnotatedAsThreadSafe cls, FieldAccess modifyingAccess, Expr witness_modifyingAccess, - FieldAccess conflictingAccess, Expr witness_conflictingAccess + ClassAnnotatedAsThreadSafe cls, Top alert_element, Top alert_context, string alert_msg, + string context_desc where - cls.witness(modifyingAccess, witness_modifyingAccess, conflictingAccess, witness_conflictingAccess) -select modifyingAccess, - "This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor.", - witness_modifyingAccess, "this expression", conflictingAccess, "this field access", - witness_conflictingAccess, "this expression" -// select c, a.getField() + unmonitored_access(cls, alert_element, alert_context, alert_msg, context_desc) + or + not_fully_monitored_field(cls, alert_element, alert_msg, context_desc) and + alert_context = cls +select alert_element, alert_msg, alert_context, context_desc diff --git a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected index d25b09260ee7..ae2bd4ea5c8a 100644 --- a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected +++ b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected @@ -1,72 +1,43 @@ -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:14:9:14:14 | this.y | this field access | examples/C.java:14:9:14:14 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:15:9:15:14 | this.y | this field access | examples/C.java:15:9:15:14 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:16:9:16:14 | this.y | this field access | examples/C.java:16:9:16:14 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:16:18:16:23 | this.y | this field access | examples/C.java:16:18:16:23 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:20:9:20:14 | this.y | this field access | examples/C.java:20:9:20:14 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:21:9:21:14 | this.y | this field access | examples/C.java:21:9:21:14 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:22:9:22:14 | this.y | this field access | examples/C.java:22:9:22:14 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:22:18:22:23 | this.y | this field access | examples/C.java:22:18:22:23 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:26:9:26:14 | this.y | this field access | examples/C.java:26:9:26:14 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:30:13:30:13 | y | this field access | examples/C.java:30:13:30:13 | y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:33:9:33:9 | y | this field access | examples/C.java:33:9:33:9 | y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:39:9:39:14 | this.y | this field access | examples/C.java:39:9:39:14 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:40:9:40:14 | this.y | this field access | examples/C.java:40:9:40:14 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:41:9:41:14 | this.y | this field access | examples/C.java:41:9:41:14 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:41:18:41:23 | this.y | this field access | examples/C.java:41:18:41:23 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:53:9:53:14 | this.y | this field access | examples/C.java:53:9:53:14 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:54:9:54:14 | this.y | this field access | examples/C.java:54:9:54:14 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:55:9:55:14 | this.y | this field access | examples/C.java:55:9:55:14 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:55:18:55:23 | this.y | this field access | examples/C.java:55:18:55:23 | this.y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:61:9:61:9 | y | this field access | examples/C.java:61:9:61:9 | y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:62:9:62:9 | y | this field access | examples/C.java:62:9:62:9 | y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:63:9:63:9 | y | this field access | examples/C.java:63:9:63:9 | y | this expression | -| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:63:13:63:13 | y | this field access | examples/C.java:63:13:63:13 | y | this expression | -| examples/FaultyTurnstileExample.java:13:5:13:9 | count | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/FaultyTurnstileExample.java:13:5:13:9 | count | this expression | examples/FaultyTurnstileExample.java:18:5:18:9 | count | this field access | examples/FaultyTurnstileExample.java:18:5:18:9 | count | this expression | -| examples/FaultyTurnstileExample.java:30:5:30:9 | count | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/FaultyTurnstileExample.java:30:5:30:9 | count | this expression | examples/FaultyTurnstileExample.java:36:5:36:9 | count | this field access | examples/FaultyTurnstileExample.java:36:5:36:9 | count | this expression | -| examples/FlawedSemaphore.java:18:7:18:11 | state | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression | examples/FlawedSemaphore.java:15:14:15:18 | state | this field access | examples/FlawedSemaphore.java:15:14:15:18 | state | this expression | -| examples/FlawedSemaphore.java:18:7:18:11 | state | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression | examples/FlawedSemaphore.java:18:7:18:11 | state | this field access | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression | -| examples/FlawedSemaphore.java:18:7:18:11 | state | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression | examples/FlawedSemaphore.java:26:7:26:11 | state | this field access | examples/FlawedSemaphore.java:26:7:26:11 | state | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:38:5:38:10 | length | this field access | examples/LockExample.java:38:5:38:10 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:39:13:39:18 | length | this field access | examples/LockExample.java:39:13:39:18 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:44:5:44:10 | length | this field access | examples/LockExample.java:44:5:44:10 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:45:13:45:18 | length | this field access | examples/LockExample.java:45:13:45:18 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:49:5:49:10 | length | this field access | examples/LockExample.java:49:5:49:10 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:57:5:57:10 | length | this field access | examples/LockExample.java:57:5:57:10 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:58:13:58:18 | length | this field access | examples/LockExample.java:58:13:58:18 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:62:5:62:10 | length | this field access | examples/LockExample.java:62:5:62:10 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:65:13:65:18 | length | this field access | examples/LockExample.java:65:13:65:18 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:69:5:69:10 | length | this field access | examples/LockExample.java:69:5:69:10 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:71:13:71:18 | length | this field access | examples/LockExample.java:71:13:71:18 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:76:5:76:10 | length | this field access | examples/LockExample.java:76:5:76:10 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:79:13:79:18 | length | this field access | examples/LockExample.java:79:13:79:18 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:127:7:127:12 | length | this field access | examples/LockExample.java:127:7:127:12 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:136:7:136:12 | length | this field access | examples/LockExample.java:136:7:136:12 | length | this expression | -| examples/LockExample.java:24:5:24:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:24:5:24:10 | length | this expression | examples/LockExample.java:142:7:142:12 | length | this field access | examples/LockExample.java:142:7:142:12 | length | this expression | -| examples/LockExample.java:25:5:25:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:25:5:25:11 | content | this expression | examples/LockExample.java:39:5:39:11 | content | this field access | examples/LockExample.java:39:5:39:11 | content | this expression | -| examples/LockExample.java:25:5:25:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:25:5:25:11 | content | this expression | examples/LockExample.java:45:5:45:11 | content | this field access | examples/LockExample.java:45:5:45:11 | content | this expression | -| examples/LockExample.java:25:5:25:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:25:5:25:11 | content | this expression | examples/LockExample.java:58:5:58:11 | content | this field access | examples/LockExample.java:58:5:58:11 | content | this expression | -| examples/LockExample.java:25:5:25:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:25:5:25:11 | content | this expression | examples/LockExample.java:65:5:65:11 | content | this field access | examples/LockExample.java:65:5:65:11 | content | this expression | -| examples/LockExample.java:25:5:25:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:25:5:25:11 | content | this expression | examples/LockExample.java:71:5:71:11 | content | this field access | examples/LockExample.java:71:5:71:11 | content | this expression | -| examples/LockExample.java:25:5:25:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:25:5:25:11 | content | this expression | examples/LockExample.java:79:5:79:11 | content | this field access | examples/LockExample.java:79:5:79:11 | content | this expression | -| examples/LockExample.java:38:5:38:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:38:5:38:10 | length | this expression | examples/LockExample.java:25:13:25:18 | length | this field access | examples/LockExample.java:25:13:25:18 | length | this expression | -| examples/LockExample.java:38:5:38:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:38:5:38:10 | length | this expression | examples/LockExample.java:32:13:32:18 | length | this field access | examples/LockExample.java:32:13:32:18 | length | this expression | -| examples/LockExample.java:38:5:38:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:38:5:38:10 | length | this expression | examples/LockExample.java:52:13:52:18 | length | this field access | examples/LockExample.java:52:13:52:18 | length | this expression | -| examples/LockExample.java:38:5:38:10 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:38:5:38:10 | length | this expression | examples/LockExample.java:150:7:150:12 | length | this field access | examples/LockExample.java:150:7:150:12 | length | this expression | -| examples/LockExample.java:39:5:39:11 | content | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:39:5:39:11 | content | this expression | examples/LockExample.java:52:5:52:11 | content | this field access | examples/LockExample.java:52:5:52:11 | content | this expression | -| examples/LockExample.java:85:5:85:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this field access | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression | -| examples/LockExample.java:85:5:85:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:112:5:112:21 | notRelatedToOther | this field access | examples/LockExample.java:112:5:112:21 | notRelatedToOther | this expression | -| examples/LockExample.java:85:5:85:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:119:5:119:21 | notRelatedToOther | this field access | examples/LockExample.java:119:5:119:21 | notRelatedToOther | this expression | -| examples/LockExample.java:85:5:85:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:124:5:124:21 | notRelatedToOther | this field access | examples/LockExample.java:124:5:124:21 | notRelatedToOther | this expression | -| examples/LockExample.java:85:5:85:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:145:5:145:21 | notRelatedToOther | this field access | examples/LockExample.java:145:5:145:21 | notRelatedToOther | this expression | -| examples/LockExample.java:85:5:85:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:153:5:153:21 | notRelatedToOther | this field access | examples/LockExample.java:153:5:153:21 | notRelatedToOther | this expression | -| examples/LockExample.java:94:5:94:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression | examples/LockExample.java:100:5:100:21 | notRelatedToOther | this field access | examples/LockExample.java:100:5:100:21 | notRelatedToOther | this expression | -| examples/LockExample.java:94:5:94:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression | examples/LockExample.java:103:5:103:21 | notRelatedToOther | this field access | examples/LockExample.java:103:5:103:21 | notRelatedToOther | this expression | -| examples/LockExample.java:94:5:94:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression | examples/LockExample.java:109:5:109:21 | notRelatedToOther | this field access | examples/LockExample.java:109:5:109:21 | notRelatedToOther | this expression | -| examples/LockExample.java:94:5:94:21 | notRelatedToOther | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression | examples/LockExample.java:117:5:117:21 | notRelatedToOther | this field access | examples/LockExample.java:117:5:117:21 | notRelatedToOther | this expression | -| examples/SyncLstExample.java:40:5:40:7 | lst | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/SyncLstExample.java:40:5:40:7 | lst | this expression | examples/SyncLstExample.java:45:5:45:7 | lst | this field access | examples/SyncLstExample.java:45:5:45:7 | lst | this expression | -| examples/SyncStackExample.java:32:5:32:7 | stc | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/SyncStackExample.java:32:5:32:7 | stc | this expression | examples/SyncStackExample.java:37:5:37:7 | stc | this field access | examples/SyncStackExample.java:37:5:37:7 | stc | this expression | -| examples/SynchronizedAndLock.java:14:9:14:14 | length | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/SynchronizedAndLock.java:14:9:14:14 | length | this expression | examples/SynchronizedAndLock.java:19:9:19:14 | length | this field access | examples/SynchronizedAndLock.java:19:9:19:14 | length | this expression | -| examples/Test.java:43:5:43:10 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/Test.java:43:5:43:10 | this.y | this expression | examples/Test.java:52:5:52:10 | this.y | this field access | examples/Test.java:24:5:24:18 | setYPrivate(...) | this expression | -| examples/Test.java:43:5:43:10 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/Test.java:43:5:43:10 | this.y | this expression | examples/Test.java:60:5:60:10 | this.y | this field access | examples/Test.java:60:5:60:10 | this.y | this expression | -| examples/Test.java:43:5:43:10 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/Test.java:43:5:43:10 | this.y | this expression | examples/Test.java:74:5:74:10 | this.y | this field access | examples/Test.java:74:5:74:10 | this.y | this expression | -| examples/Test.java:43:5:43:10 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/Test.java:43:5:43:10 | this.y | this expression | examples/Test.java:74:14:74:14 | y | this field access | examples/Test.java:74:14:74:14 | 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 | +| examples/C.java:16:18:16:23 | 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:18:16:23 | this.y | this expression | +| examples/C.java:20:9:20: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:20:9:20:14 | this.y | this expression | +| examples/C.java:21:9:21: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:21:9:21:14 | this.y | this expression | +| examples/C.java:22:9:22: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:22:9:22:14 | this.y | this expression | +| examples/C.java:22:18:22:23 | this.y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/C.java:22:18:22:23 | this.y | this expression | +| examples/C.java:26:9:26: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:26:9:26:14 | this.y | this expression | +| examples/C.java:30:13:30:13 | y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/C.java:30:13:30:13 | y | this expression | +| examples/C.java:33:9:33:9 | y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/C.java:33:9:33:9 | y | this expression | +| examples/FaultyTurnstileExample.java:18:5:18:9 | count | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/FaultyTurnstileExample.java:18:5:18:9 | count | this expression | +| examples/FaultyTurnstileExample.java:26:15:26:19 | count | The field $@ is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/FaultyTurnstileExample.java:23:7:23:29 | FaultyTurnstileExample2 | FaultyTurnstileExample2 | +| examples/FlawedSemaphore.java:15:14:15:18 | state | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/FlawedSemaphore.java:15:14:15:18 | state | this expression | +| examples/FlawedSemaphore.java:18:7:18:11 | state | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression | +| examples/LockExample.java:18:15:18:20 | length | The field $@ is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/LockExample.java:14:14:14:24 | LockExample | LockExample | +| examples/LockExample.java:19:15:19:31 | notRelatedToOther | The field $@ is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/LockExample.java:14:14:14:24 | LockExample | LockExample | +| examples/LockExample.java:20:17:20:23 | content | The field $@ is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/LockExample.java:14:14:14:24 | LockExample | LockExample | +| examples/LockExample.java:44:5:44:10 | length | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:44:5:44:10 | length | this expression | +| examples/LockExample.java:45:5:45:11 | content | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:45:5:45:11 | content | this expression | +| examples/LockExample.java:45:13:45:18 | length | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:45:13:45:18 | length | this expression | +| examples/LockExample.java:49:5:49:10 | length | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:49:5:49:10 | length | this expression | +| examples/LockExample.java:62:5:62:10 | length | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:62:5:62:10 | length | this expression | +| examples/LockExample.java:65:5:65:11 | content | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:65:5:65:11 | content | this expression | +| examples/LockExample.java:65:13:65:18 | length | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:65:13:65:18 | length | this expression | +| examples/LockExample.java:69:5:69:10 | length | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:69:5:69:10 | length | this expression | +| examples/LockExample.java:71:5:71:11 | content | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:71:5:71:11 | content | this expression | +| examples/LockExample.java:71:13:71:18 | length | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:71:13:71:18 | length | this expression | +| examples/LockExample.java:76:5:76:10 | length | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:76:5:76:10 | length | this expression | +| examples/LockExample.java:79:5:79:11 | content | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:79:5:79:11 | content | this expression | +| examples/LockExample.java:79:13:79:18 | length | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:79:13:79:18 | length | this expression | +| examples/LockExample.java:112:5:112:21 | notRelatedToOther | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:112:5:112:21 | notRelatedToOther | this expression | +| examples/LockExample.java:119:5:119:21 | notRelatedToOther | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:119:5:119:21 | notRelatedToOther | this expression | +| examples/LockExample.java:124:5:124:21 | notRelatedToOther | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:124:5:124:21 | notRelatedToOther | this expression | +| examples/LockExample.java:145:5:145:21 | notRelatedToOther | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:145:5:145:21 | notRelatedToOther | this expression | +| examples/LockExample.java:153:5:153:21 | notRelatedToOther | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:153:5:153:21 | notRelatedToOther | this expression | +| examples/SyncLstExample.java:45:5:45:7 | lst | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/SyncLstExample.java:45:5:45:7 | lst | this expression | +| examples/SyncStackExample.java:37:5:37:7 | stc | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/SyncStackExample.java:37:5:37:7 | stc | this expression | +| examples/SynchronizedAndLock.java:10:17:10:22 | length | The field $@ is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/SynchronizedAndLock.java:7:14:7:32 | SynchronizedAndLock | SynchronizedAndLock | +| examples/Test.java:52:5:52:10 | this.y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/Test.java:24:5:24:18 | setYPrivate(...) | this expression | +| examples/Test.java:60:5:60:10 | this.y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/Test.java:60:5:60:10 | this.y | this expression | +| examples/Test.java:74:5:74:10 | this.y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/Test.java:74:5:74:10 | this.y | this expression | +| examples/Test.java:74:14:74:14 | y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/Test.java:74:14:74:14 | y | this expression | diff --git a/java/ql/test/query-tests/ThreadSafe/examples/C.java b/java/ql/test/query-tests/ThreadSafe/examples/C.java index 51201d4f6be3..92c6b82800c3 100644 --- a/java/ql/test/query-tests/ThreadSafe/examples/C.java +++ b/java/ql/test/query-tests/ThreadSafe/examples/C.java @@ -12,25 +12,25 @@ public class C { public void m() { this.y = 0; // $ Alert - this.y += 1; - this.y = this.y - 1; + this.y += 1; // $ Alert + this.y = this.y - 1; // $ Alert } public void n4() { - this.y = 0; - this.y += 1; - this.y = this.y - 1; + this.y = 0; // $ Alert + this.y += 1; // $ Alert + this.y = this.y - 1; // $ Alert } public void setY(int y) { - this.y = y; + this.y = y; // $ Alert } public void test() { - if (y == 0) { + if (y == 0) { // $ Alert lock.lock(); } - y = 0; + y = 0; // $ Alert lock.unlock(); } diff --git a/java/ql/test/query-tests/ThreadSafe/examples/FaultyTurnstileExample.java b/java/ql/test/query-tests/ThreadSafe/examples/FaultyTurnstileExample.java index adbd74473e41..20b258135f6d 100644 --- a/java/ql/test/query-tests/ThreadSafe/examples/FaultyTurnstileExample.java +++ b/java/ql/test/query-tests/ThreadSafe/examples/FaultyTurnstileExample.java @@ -10,12 +10,12 @@ class FaultyTurnstileExample { public void inc() { lock.lock(); - count++; // $ Alert + count++; // $ MISSING: Alert lock.unlock(); } public void dec() { - count--; + count--; // $ Alert } } @@ -23,11 +23,11 @@ public void dec() { class FaultyTurnstileExample2 { private Lock lock1 = new ReentrantLock(); private Lock lock2 = new ReentrantLock(); - private int count = 0; + private int count = 0; // $ Alert public void inc() { lock1.lock(); - count++; // $ Alert + count++; lock1.unlock(); } diff --git a/java/ql/test/query-tests/ThreadSafe/examples/FlawedSemaphore.java b/java/ql/test/query-tests/ThreadSafe/examples/FlawedSemaphore.java index 405edbe7058d..a73b45e60ed6 100644 --- a/java/ql/test/query-tests/ThreadSafe/examples/FlawedSemaphore.java +++ b/java/ql/test/query-tests/ThreadSafe/examples/FlawedSemaphore.java @@ -12,7 +12,7 @@ public FlawedSemaphore(int c) { public void acquire() { try { - while (state == capacity) { + while (state == capacity) { // $ Alert this.wait(); } state++; // $ Alert diff --git a/java/ql/test/query-tests/ThreadSafe/examples/LockExample.java b/java/ql/test/query-tests/ThreadSafe/examples/LockExample.java index 8ce34922c5b6..1e1792d0d2e4 100644 --- a/java/ql/test/query-tests/ThreadSafe/examples/LockExample.java +++ b/java/ql/test/query-tests/ThreadSafe/examples/LockExample.java @@ -15,14 +15,14 @@ public class LockExample { private Lock lock1 = new ReentrantLock(); private Lock lock2 = new ReentrantLock(); - private int length = 0; - private int notRelatedToOther = 10; - private int[] content = new int[10]; + private int length = 0; // $ Alert + private int notRelatedToOther = 10; // $ Alert + private int[] content = new int[10]; // $ Alert public void add(int value) { lock1.lock(); - length++; // $ Alert - content[length] = value; // $ Alert + length++; + content[length] = value; lock1.unlock(); } @@ -35,18 +35,18 @@ public void removeCorrect() { public void notTheSameLockAsAdd() { // use locks, but different ones lock2.lock(); - length--; // $ Alert - content[length] = 0; // $ Alert + length--; + content[length] = 0; lock2.unlock(); } public void noLock() { // no locks - length--; - content[length] = 0; + length--; // $ Alert + content[length] = 0; // $ Alert } public void fieldUpdatedOutsideOfLock() { // adjusts length without lock - length--; + length--; // $ Alert lock1.lock(); content[length] = 0; @@ -59,30 +59,30 @@ public synchronized void synchronizedLock() { // no locks, but with synchronized } public void onlyLocked() { // never unlocked, only locked - length--; + length--; // $ Alert lock1.lock(); - content[length] = 0; + content[length] = 0; // $ Alert } public void onlyUnlocked() { // never locked, only unlocked - length--; + length--; // $ Alert - content[length] = 0; + content[length] = 0; // $ Alert lock1.unlock(); } public void notSameLock() { - length--; + length--; // $ Alert lock2.lock();// Not the same lock - content[length] = 0; + content[length] = 0; // $ Alert lock1.unlock(); } public void updateCount() { lock2.lock(); - notRelatedToOther++; // $ Alert + notRelatedToOther++; lock2.unlock(); } @@ -91,7 +91,7 @@ public void updateCountTwiceCorrect() { notRelatedToOther++; lock2.unlock(); lock1.lock(); - notRelatedToOther++; // $ Alert + notRelatedToOther++; lock1.unlock(); } @@ -109,19 +109,19 @@ public void updateCountTwiceLock() { notRelatedToOther++; lock2.unlock(); lock1.lock(); - notRelatedToOther++; + notRelatedToOther++; // $ Alert } public void updateCountTwiceUnLock() { lock2.lock(); notRelatedToOther++; lock2.unlock(); - notRelatedToOther++; + notRelatedToOther++; // $ Alert lock1.unlock(); } public void synchronizedNonRelatedOutside() { - notRelatedToOther++; + notRelatedToOther++; // $ Alert synchronized(this) { length++; @@ -142,7 +142,7 @@ public void synchronizedNonRelatedOutside3() { length++; } - notRelatedToOther = 1; + notRelatedToOther = 1; // $ Alert } public void synchronizedNonRelatedOutside4() { @@ -150,7 +150,7 @@ public void synchronizedNonRelatedOutside4() { length++; } - notRelatedToOther = 1; + notRelatedToOther = 1; // $ Alert } } diff --git a/java/ql/test/query-tests/ThreadSafe/examples/SyncLstExample.java b/java/ql/test/query-tests/ThreadSafe/examples/SyncLstExample.java index 63f6985840c1..04bc1c3c454b 100644 --- a/java/ql/test/query-tests/ThreadSafe/examples/SyncLstExample.java +++ b/java/ql/test/query-tests/ThreadSafe/examples/SyncLstExample.java @@ -37,11 +37,11 @@ public FaultySyncLstExample(List lst) { public void add(T item) { lock.lock(); - lst.add(item); // $ Alert + lst.add(item); lock.unlock(); } public void remove(int i) { - lst.remove(i); + lst.remove(i); // $ Alert } } diff --git a/java/ql/test/query-tests/ThreadSafe/examples/SyncStackExample.java b/java/ql/test/query-tests/ThreadSafe/examples/SyncStackExample.java index 62eabde4b7d7..31e8cebee3e7 100644 --- a/java/ql/test/query-tests/ThreadSafe/examples/SyncStackExample.java +++ b/java/ql/test/query-tests/ThreadSafe/examples/SyncStackExample.java @@ -29,11 +29,11 @@ class FaultySyncStackExample { public void push(T item) { lock.lock(); - stc.push(item); // $ Alert + stc.push(item); lock.unlock(); } public void pop() { - stc.pop(); + stc.pop(); // $ Alert } } diff --git a/java/ql/test/query-tests/ThreadSafe/examples/SynchronizedAndLock.java b/java/ql/test/query-tests/ThreadSafe/examples/SynchronizedAndLock.java index fc0aa038b0ee..52b35a84bb70 100644 --- a/java/ql/test/query-tests/ThreadSafe/examples/SynchronizedAndLock.java +++ b/java/ql/test/query-tests/ThreadSafe/examples/SynchronizedAndLock.java @@ -7,11 +7,11 @@ public class SynchronizedAndLock { private Lock lock = new ReentrantLock(); - private int length = 0; + private int length = 0; // $ Alert public void add(int value) { lock.lock(); - length++; // $ Alert + length++; lock.unlock(); } diff --git a/java/ql/test/query-tests/ThreadSafe/examples/Test.java b/java/ql/test/query-tests/ThreadSafe/examples/Test.java index b2e7ac46c0bf..e6b0567ef89b 100644 --- a/java/ql/test/query-tests/ThreadSafe/examples/Test.java +++ b/java/ql/test/query-tests/ThreadSafe/examples/Test.java @@ -40,7 +40,7 @@ public void setYAgainCorrect(int y) { */ public void setYCorrect(int y) { lock.lock(); - this.y = y; // $ Alert + this.y = y; lock.unlock(); } @@ -49,7 +49,7 @@ public void setYCorrect(int y) { * @param y */ private void setYPrivate(int y) { - this.y = y; + this.y = y; // $ Alert } /** @@ -57,7 +57,7 @@ private void setYPrivate(int y) { * @param y */ public void setYWrongLock(int y) { - this.y = y; + this.y = y; // $ Alert lock.lock(); lock.unlock(); } @@ -71,6 +71,6 @@ public synchronized int getImmutableField2() { } public void testMethod() { - this.y = y + 2; + this.y = y + 2; // $ Alert } } From 3a0a8999d5a7c1c76dfdbd2e2503cf7cd064a048 Mon Sep 17 00:00:00 2001 From: yoff Date: Fri, 17 Oct 2025 01:52:23 +0200 Subject: [PATCH 17/25] java: fix ql alerts --- java/ql/lib/semmle/code/java/ConflictingAccess.qll | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index 9373845d6bca..f075bb3d1989 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -185,7 +185,7 @@ class ClassAnnotatedAsThreadSafe extends Class { Monitors::locallyMonitors(e, monitor) or // recursive case - exists(MethodCall c, Expr e0, Method m0 | this.has_onelocked_access(f, e0, m0, write, monitor) | + exists(MethodCall c, Method m0 | this.has_onelocked_access(f, _, m0, write, monitor) | m = c.getEnclosingCallable() and not m0.isPublic() and c.getCallee().getSourceDeclaration() = m0 and @@ -223,8 +223,8 @@ class ClassAnnotatedAsThreadSafe extends Class { not this.has_unlocked_public_access(f, _, _, _) or // recursive case - exists(MethodCall c, Expr e0, Method m0, Monitors::Monitor monitor0 | - this.has_onepluslocked_access(f, e0, m0, write, monitor0) and + exists(MethodCall c, Method m0, Monitors::Monitor monitor0 | + this.has_onepluslocked_access(f, _, m0, write, monitor0) and m = c.getEnclosingCallable() and not m0.isPublic() and c.getCallee().getSourceDeclaration() = m0 and @@ -258,7 +258,7 @@ class ClassAnnotatedAsThreadSafe extends Class { not Monitors::locallyMonitors(e, monitor) or // recursive case - exists(MethodCall c, Expr e0, Method m0 | this.escapes_monitor(f, e0, m0, write, monitor) | + exists(MethodCall c, Method m0 | this.escapes_monitor(f, _, m0, write, monitor) | m = c.getEnclosingCallable() and not m0.isPublic() and c.getCallee().getSourceDeclaration() = m0 and From 715acefaccaf0711fbb9c85500cd46b76253d5de Mon Sep 17 00:00:00 2001 From: yoff Date: Tue, 21 Oct 2025 12:52:59 +0200 Subject: [PATCH 18/25] Apply suggestions from code review Co-authored-by: Anders Schack-Mulligen --- java/ql/lib/semmle/code/java/ConflictingAccess.qll | 1 - java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index f075bb3d1989..eb4f7c0f0b7e 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -263,7 +263,6 @@ class ClassAnnotatedAsThreadSafe extends Class { not m0.isPublic() and c.getCallee().getSourceDeclaration() = m0 and c = e and - // consider allowing idempotent monitors not Monitors::locallyMonitors(e, monitor) and m.getDeclaringType() = this ) diff --git a/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql b/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql index 89e9cbdb169b..bdb081ec4a6b 100644 --- a/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql +++ b/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql @@ -41,7 +41,7 @@ predicate not_fully_monitored_field( cls.has_public_write_access(f) ) and msg = - "The field $@ is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe." and + "This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe." and cls_name = cls.getName() } From de05bfbce3c703a6e5ef1e391819ee1c3125556f Mon Sep 17 00:00:00 2001 From: yoff Date: Tue, 21 Oct 2025 12:49:07 +0200 Subject: [PATCH 19/25] java: address review comments - do not use `getQualifiedName` - use camelCase - rework alert predicates --- .../semmle/code/java/ConflictingAccess.qll | 79 +++++++++---------- .../src/Likely Bugs/Concurrency/ThreadSafe.ql | 31 +++----- .../ThreadSafe/ThreadSafe.expected | 10 +-- 3 files changed, 57 insertions(+), 63 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index eb4f7c0f0b7e..39f8a5e1e9e8 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -44,11 +44,11 @@ predicate isThreadSafeType(Type t) { /** Holds if the expression `e` is a thread-safe initializer. */ predicate isThreadSafeInitializer(Expr e) { - e.(Call) - .getCallee() - .getSourceDeclaration() - .getQualifiedName() - .matches("java.util.Collections.synchronized%") + exists(string name | + e.(Call).getCallee().getSourceDeclaration().hasQualifiedName("java.util", "Collections", name) + | + name.matches("synchronized%") + ) } /** @@ -132,7 +132,7 @@ class ClassAnnotatedAsThreadSafe extends Class { * Holds if the field access `a` to the field `f` is not protected by any monitor, and it can be reached via the expression `e` in the method `m`. * We maintain the invariant that `m = e.getEnclosingCallable()`. */ - predicate unlocked_access(ExposedField f, Expr e, Method m, ExposedFieldAccess a, boolean write) { + predicate unlockedAccess(ExposedField f, Expr e, Method m, ExposedFieldAccess a, boolean write) { m.getDeclaringType() = this and ( // base case @@ -143,7 +143,7 @@ class ClassAnnotatedAsThreadSafe extends Class { (if Modification::isModifying(a) then write = true else write = false) or // recursive case - exists(MethodCall c, Expr e0, Method m0 | this.unlocked_access(f, e0, m0, a, write) | + exists(MethodCall c, Expr e0, Method m0 | this.unlockedAccess(f, e0, m0, a, write) | m = c.getEnclosingCallable() and not m0.isPublic() and c.getCallee().getSourceDeclaration() = m0 and @@ -154,22 +154,22 @@ class ClassAnnotatedAsThreadSafe extends Class { } /** Holds if the class has an unlocked access to the field `f` via the expression `e` in the method `m`. */ - predicate has_unlocked_access(ExposedField f, Expr e, Method m, boolean write) { - this.unlocked_access(f, e, m, _, write) + predicate hasUnlockedAccess(ExposedField f, Expr e, Method m, boolean write) { + this.unlockedAccess(f, e, m, _, write) } /** Holds if the field access `a` to the field `f` is not protected by any monitor, and it can be reached via the expression `e` in the public method `m`. */ - predicate unlocked_public_access( + predicate unlockedPublicAccess( ExposedField f, Expr e, Method m, ExposedFieldAccess a, boolean write ) { - this.unlocked_access(f, e, m, a, write) and + this.unlockedAccess(f, e, m, a, write) and m.isPublic() and not Monitors::locallyMonitors(e, _) } /** Holds if the class has an unlocked access to the field `f` via the expression `e` in the public method `m`. */ - predicate has_unlocked_public_access(ExposedField f, Expr e, Method m, boolean write) { - this.unlocked_public_access(f, e, m, _, write) + predicate hasUnlockedPublicAccess(ExposedField f, Expr e, Method m, boolean write) { + this.unlockedPublicAccess(f, e, m, _, write) } // Cases where all accesses to a field are protected by exactly one monitor @@ -177,15 +177,15 @@ class ClassAnnotatedAsThreadSafe extends Class { /** * Holds if the class has an access, locked by exactly one monitor, to the field `f` via the expression `e` in the method `m`. */ - predicate has_onelocked_access( + predicate hasOnelockedAccess( ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor ) { //base - this.has_unlocked_access(f, e, m, write) and + this.hasUnlockedAccess(f, e, m, write) and Monitors::locallyMonitors(e, monitor) or // recursive case - exists(MethodCall c, Method m0 | this.has_onelocked_access(f, _, m0, write, monitor) | + exists(MethodCall c, Method m0 | this.hasOnelockedAccess(f, _, m0, write, monitor) | m = c.getEnclosingCallable() and not m0.isPublic() and c.getCallee().getSourceDeclaration() = m0 and @@ -197,34 +197,33 @@ class ClassAnnotatedAsThreadSafe extends Class { } /** Holds if the class has an access, locked by exactly one monitor, to the field `f` via the expression `e` in the public method `m`. */ - predicate has_onelocked_public_access( + predicate hasOnelockedPublicAccess( ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor ) { - this.has_onelocked_access(f, e, m, write, monitor) and + this.hasOnelockedAccess(f, e, m, write, monitor) and m.isPublic() and - not this.has_unlocked_public_access(f, e, m, write) + not this.hasUnlockedPublicAccess(f, e, m, write) } /** Holds if the field `f` has more than one access, all locked by a single monitor, but different monitors are used. */ - predicate single_monitor_mismatch(ExposedField f) { - 2 <= - strictcount(Monitors::Monitor monitor | this.has_onelocked_public_access(f, _, _, _, monitor)) + predicate singleMonitorMismatch(ExposedField f) { + 2 <= strictcount(Monitors::Monitor monitor | this.hasOnelockedPublicAccess(f, _, _, _, monitor)) } // Cases where all accesses to a field are protected by at least one monitor // /** Holds if the class has an access, locked by at least one monitor, to the field `f` via the expression `e` in the method `m`. */ - predicate has_onepluslocked_access( + predicate hasOnepluslockedAccess( ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor ) { //base - this.has_onelocked_access(f, e, m, write, monitor) and - not this.single_monitor_mismatch(f) and - not this.has_unlocked_public_access(f, _, _, _) + this.hasOnelockedAccess(f, e, m, write, monitor) and + not this.singleMonitorMismatch(f) and + not this.hasUnlockedPublicAccess(f, _, _, _) or // recursive case exists(MethodCall c, Method m0, Monitors::Monitor monitor0 | - this.has_onepluslocked_access(f, _, m0, write, monitor0) and + this.hasOnepluslockedAccess(f, _, m0, write, monitor0) and m = c.getEnclosingCallable() and not m0.isPublic() and c.getCallee().getSourceDeclaration() = m0 and @@ -238,27 +237,27 @@ class ClassAnnotatedAsThreadSafe extends Class { } /** Holds if the class has a write access to the field `f` that can be reached via a public method. */ - predicate has_public_write_access(ExposedField f) { - this.has_unlocked_public_access(f, _, _, true) + predicate hasPublicWriteAccess(ExposedField f) { + this.hasUnlockedPublicAccess(f, _, _, true) or - this.has_onelocked_public_access(f, _, _, true, _) + this.hasOnelockedPublicAccess(f, _, _, true, _) or exists(Method m | m.getDeclaringType() = this and m.isPublic() | - this.has_onepluslocked_access(f, _, m, true, _) + this.hasOnepluslockedAccess(f, _, m, true, _) ) } /** Holds if the class has an access, not protected by the monitor `m`, to the field `f` via the expression `e` in the method `m`. */ - predicate escapes_monitor( + predicate escapesMonitor( ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor ) { //base - this.has_onepluslocked_access(f, _, _, _, monitor) and - this.has_unlocked_access(f, e, m, write) and + this.hasOnepluslockedAccess(f, _, _, _, monitor) and + this.hasUnlockedAccess(f, e, m, write) and not Monitors::locallyMonitors(e, monitor) or // recursive case - exists(MethodCall c, Method m0 | this.escapes_monitor(f, _, m0, write, monitor) | + exists(MethodCall c, Method m0 | this.escapesMonitor(f, _, m0, write, monitor) | m = c.getEnclosingCallable() and not m0.isPublic() and c.getCallee().getSourceDeclaration() = m0 and @@ -269,17 +268,17 @@ class ClassAnnotatedAsThreadSafe extends Class { } /** Holds if the class has an access, not protected by the monitor `m`, to the field `f` via the expression `e` in the public method `m`. */ - predicate escapes_monitor_public( + predicate escapesMonitorPublic( ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor ) { - this.escapes_monitor(f, e, m, write, monitor) and + this.escapesMonitor(f, e, m, write, monitor) and m.isPublic() } /** Holds if no monitor protects all accesses to the field `f`. */ - predicate not_fully_monitored(ExposedField f) { - forex(Monitors::Monitor monitor | this.has_onepluslocked_access(f, _, _, _, monitor) | - this.escapes_monitor_public(f, _, _, _, monitor) + predicate notFullyMonitored(ExposedField f) { + forex(Monitors::Monitor monitor | this.hasOnepluslockedAccess(f, _, _, _, monitor) | + this.escapesMonitorPublic(f, _, _, _, monitor) ) } } diff --git a/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql b/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql index bdb081ec4a6b..fafa4701ed22 100644 --- a/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql +++ b/java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql @@ -14,43 +14,38 @@ import java import semmle.code.java.ConflictingAccess -predicate unmonitored_access( - ClassAnnotatedAsThreadSafe cls, ExposedFieldAccess a, Expr entry, string msg, string entry_desc -) { - exists(ExposedField f | - cls.unlocked_public_access(f, entry, _, a, true) +predicate unmonitoredAccess(ExposedFieldAccess a, string msg, Expr entry, string entry_desc) { + exists(ClassAnnotatedAsThreadSafe cls, ExposedField f | + cls.unlockedPublicAccess(f, entry, _, a, true) or - cls.unlocked_public_access(f, entry, _, a, false) and - cls.has_public_write_access(f) + cls.unlockedPublicAccess(f, entry, _, a, false) and + cls.hasPublicWriteAccess(f) ) and msg = "This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe." and entry_desc = "this expression" } -predicate not_fully_monitored_field( - ClassAnnotatedAsThreadSafe cls, ExposedField f, string msg, string cls_name +predicate notFullyMonitoredField( + ExposedField f, string msg, ClassAnnotatedAsThreadSafe cls, string cls_name ) { ( // Technically there has to be a write access for a conflict to exist. // But if you are locking your reads with different locks, you likely made a typo, // so in this case we alert without requiring `cls.has_public_write_access(f)` - cls.single_monitor_mismatch(f) + cls.singleMonitorMismatch(f) or - cls.not_fully_monitored(f) and - cls.has_public_write_access(f) + cls.notFullyMonitored(f) and + cls.hasPublicWriteAccess(f) ) and msg = "This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe." and cls_name = cls.getName() } -from - ClassAnnotatedAsThreadSafe cls, Top alert_element, Top alert_context, string alert_msg, - string context_desc +from Top alert_element, Top alert_context, string alert_msg, string context_desc where - unmonitored_access(cls, alert_element, alert_context, alert_msg, context_desc) + unmonitoredAccess(alert_element, alert_msg, alert_context, context_desc) or - not_fully_monitored_field(cls, alert_element, alert_msg, context_desc) and - alert_context = cls + notFullyMonitoredField(alert_element, alert_msg, alert_context, context_desc) select alert_element, alert_msg, alert_context, context_desc diff --git a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected index ae2bd4ea5c8a..d6005400129a 100644 --- a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected +++ b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected @@ -10,12 +10,12 @@ | examples/C.java:30:13:30:13 | y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/C.java:30:13:30:13 | y | this expression | | examples/C.java:33:9:33:9 | y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/C.java:33:9:33:9 | y | this expression | | examples/FaultyTurnstileExample.java:18:5:18:9 | count | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/FaultyTurnstileExample.java:18:5:18:9 | count | this expression | -| examples/FaultyTurnstileExample.java:26:15:26:19 | count | The field $@ is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/FaultyTurnstileExample.java:23:7:23:29 | FaultyTurnstileExample2 | FaultyTurnstileExample2 | +| examples/FaultyTurnstileExample.java:26:15:26:19 | count | This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/FaultyTurnstileExample.java:23:7:23:29 | FaultyTurnstileExample2 | FaultyTurnstileExample2 | | examples/FlawedSemaphore.java:15:14:15:18 | state | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/FlawedSemaphore.java:15:14:15:18 | state | this expression | | examples/FlawedSemaphore.java:18:7:18:11 | state | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression | -| examples/LockExample.java:18:15:18:20 | length | The field $@ is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/LockExample.java:14:14:14:24 | LockExample | LockExample | -| examples/LockExample.java:19:15:19:31 | notRelatedToOther | The field $@ is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/LockExample.java:14:14:14:24 | LockExample | LockExample | -| examples/LockExample.java:20:17:20:23 | content | The field $@ is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/LockExample.java:14:14:14:24 | LockExample | LockExample | +| examples/LockExample.java:18:15:18:20 | length | This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/LockExample.java:14:14:14:24 | LockExample | LockExample | +| examples/LockExample.java:19:15:19:31 | notRelatedToOther | This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/LockExample.java:14:14:14:24 | LockExample | LockExample | +| examples/LockExample.java:20:17:20:23 | content | This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/LockExample.java:14:14:14:24 | LockExample | LockExample | | examples/LockExample.java:44:5:44:10 | length | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:44:5:44:10 | length | this expression | | examples/LockExample.java:45:5:45:11 | content | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:45:5:45:11 | content | this expression | | examples/LockExample.java:45:13:45:18 | length | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:45:13:45:18 | length | this expression | @@ -36,7 +36,7 @@ | examples/LockExample.java:153:5:153:21 | notRelatedToOther | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:153:5:153:21 | notRelatedToOther | this expression | | examples/SyncLstExample.java:45:5:45:7 | lst | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/SyncLstExample.java:45:5:45:7 | lst | this expression | | examples/SyncStackExample.java:37:5:37:7 | stc | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/SyncStackExample.java:37:5:37:7 | stc | this expression | -| examples/SynchronizedAndLock.java:10:17:10:22 | length | The field $@ is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/SynchronizedAndLock.java:7:14:7:32 | SynchronizedAndLock | SynchronizedAndLock | +| examples/SynchronizedAndLock.java:10:17:10:22 | length | This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/SynchronizedAndLock.java:7:14:7:32 | SynchronizedAndLock | SynchronizedAndLock | | examples/Test.java:52:5:52:10 | this.y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/Test.java:24:5:24:18 | setYPrivate(...) | this expression | | examples/Test.java:60:5:60:10 | this.y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/Test.java:60:5:60:10 | this.y | this expression | | examples/Test.java:74:5:74:10 | this.y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/Test.java:74:5:74:10 | this.y | this expression | From f4878b38069642b59389ee42c10fe72bfeb1c139 Mon Sep 17 00:00:00 2001 From: yoff Date: Tue, 21 Oct 2025 13:24:23 +0200 Subject: [PATCH 20/25] java: make as many predicates private as possible --- java/ql/lib/semmle/code/java/Concurrency.qll | 6 +++--- .../semmle/code/java/ConflictingAccess.qll | 20 ++++++++++--------- 2 files changed, 14 insertions(+), 12 deletions(-) diff --git a/java/ql/lib/semmle/code/java/Concurrency.qll b/java/ql/lib/semmle/code/java/Concurrency.qll index 7fbf0647b277..b16aa850c39b 100644 --- a/java/ql/lib/semmle/code/java/Concurrency.qll +++ b/java/ql/lib/semmle/code/java/Concurrency.qll @@ -15,19 +15,19 @@ class LockType extends RefType { } /** Gets a method that is locking this lock type. */ - Method getLockMethod() { + private Method getLockMethod() { result.getDeclaringType() = this and result.hasName(["lock", "lockInterruptibly", "tryLock"]) } /** Gets a method that is unlocking this lock type. */ - Method getUnlockMethod() { + private Method getUnlockMethod() { result.getDeclaringType() = this and result.hasName("unlock") } /** Gets an `isHeldByCurrentThread` method of this lock type. */ - Method getIsHeldByCurrentThreadMethod() { + private Method getIsHeldByCurrentThreadMethod() { result.getDeclaringType() = this and result.hasName("isHeldByCurrentThread") } diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index 39f8a5e1e9e8..ceff3e4ffa3a 100644 --- a/java/ql/lib/semmle/code/java/ConflictingAccess.qll +++ b/java/ql/lib/semmle/code/java/ConflictingAccess.qll @@ -43,7 +43,7 @@ predicate isThreadSafeType(Type t) { } /** Holds if the expression `e` is a thread-safe initializer. */ -predicate isThreadSafeInitializer(Expr e) { +private predicate isThreadSafeInitializer(Expr e) { exists(string name | e.(Call).getCallee().getSourceDeclaration().hasQualifiedName("java.util", "Collections", name) | @@ -132,7 +132,9 @@ class ClassAnnotatedAsThreadSafe extends Class { * Holds if the field access `a` to the field `f` is not protected by any monitor, and it can be reached via the expression `e` in the method `m`. * We maintain the invariant that `m = e.getEnclosingCallable()`. */ - predicate unlockedAccess(ExposedField f, Expr e, Method m, ExposedFieldAccess a, boolean write) { + private predicate unlockedAccess( + ExposedField f, Expr e, Method m, ExposedFieldAccess a, boolean write + ) { m.getDeclaringType() = this and ( // base case @@ -154,7 +156,7 @@ class ClassAnnotatedAsThreadSafe extends Class { } /** Holds if the class has an unlocked access to the field `f` via the expression `e` in the method `m`. */ - predicate hasUnlockedAccess(ExposedField f, Expr e, Method m, boolean write) { + private predicate hasUnlockedAccess(ExposedField f, Expr e, Method m, boolean write) { this.unlockedAccess(f, e, m, _, write) } @@ -168,7 +170,7 @@ class ClassAnnotatedAsThreadSafe extends Class { } /** Holds if the class has an unlocked access to the field `f` via the expression `e` in the public method `m`. */ - predicate hasUnlockedPublicAccess(ExposedField f, Expr e, Method m, boolean write) { + private predicate hasUnlockedPublicAccess(ExposedField f, Expr e, Method m, boolean write) { this.unlockedPublicAccess(f, e, m, _, write) } @@ -177,7 +179,7 @@ class ClassAnnotatedAsThreadSafe extends Class { /** * Holds if the class has an access, locked by exactly one monitor, to the field `f` via the expression `e` in the method `m`. */ - predicate hasOnelockedAccess( + private predicate hasOnelockedAccess( ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor ) { //base @@ -197,7 +199,7 @@ class ClassAnnotatedAsThreadSafe extends Class { } /** Holds if the class has an access, locked by exactly one monitor, to the field `f` via the expression `e` in the public method `m`. */ - predicate hasOnelockedPublicAccess( + private predicate hasOnelockedPublicAccess( ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor ) { this.hasOnelockedAccess(f, e, m, write, monitor) and @@ -213,7 +215,7 @@ class ClassAnnotatedAsThreadSafe extends Class { // Cases where all accesses to a field are protected by at least one monitor // /** Holds if the class has an access, locked by at least one monitor, to the field `f` via the expression `e` in the method `m`. */ - predicate hasOnepluslockedAccess( + private predicate hasOnepluslockedAccess( ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor ) { //base @@ -248,7 +250,7 @@ class ClassAnnotatedAsThreadSafe extends Class { } /** Holds if the class has an access, not protected by the monitor `m`, to the field `f` via the expression `e` in the method `m`. */ - predicate escapesMonitor( + private predicate escapesMonitor( ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor ) { //base @@ -268,7 +270,7 @@ class ClassAnnotatedAsThreadSafe extends Class { } /** Holds if the class has an access, not protected by the monitor `m`, to the field `f` via the expression `e` in the public method `m`. */ - predicate escapesMonitorPublic( + private predicate escapesMonitorPublic( ExposedField f, Expr e, Method m, boolean write, Monitors::Monitor monitor ) { this.escapesMonitor(f, e, m, write, monitor) and From f183a7223fd4d2676975e6e4089e8b369e7ab611 Mon Sep 17 00:00:00 2001 From: yoff Date: Tue, 21 Oct 2025 13:40:29 +0200 Subject: [PATCH 21/25] java: add test for `notFullyMonitored` --- .../ThreadSafe/ThreadSafe.expected | 1 + .../ThreadSafe/examples/ManyLocks.java | 37 +++++++++++++++++++ 2 files changed, 38 insertions(+) create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/ManyLocks.java diff --git a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected index d6005400129a..a4da07d7ac6d 100644 --- a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected +++ b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected @@ -34,6 +34,7 @@ | examples/LockExample.java:124:5:124:21 | notRelatedToOther | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:124:5:124:21 | notRelatedToOther | this expression | | examples/LockExample.java:145:5:145:21 | notRelatedToOther | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:145:5:145:21 | notRelatedToOther | this expression | | examples/LockExample.java:153:5:153:21 | notRelatedToOther | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:153:5:153:21 | notRelatedToOther | this expression | +| examples/ManyLocks.java:8:15:8:15 | y | This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/ManyLocks.java:7:14:7:22 | ManyLocks | ManyLocks | | examples/SyncLstExample.java:45:5:45:7 | lst | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/SyncLstExample.java:45:5:45:7 | lst | this expression | | examples/SyncStackExample.java:37:5:37:7 | stc | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/SyncStackExample.java:37:5:37:7 | stc | this expression | | examples/SynchronizedAndLock.java:10:17:10:22 | length | This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/SynchronizedAndLock.java:7:14:7:32 | SynchronizedAndLock | SynchronizedAndLock | diff --git a/java/ql/test/query-tests/ThreadSafe/examples/ManyLocks.java b/java/ql/test/query-tests/ThreadSafe/examples/ManyLocks.java new file mode 100644 index 000000000000..93557ecdafea --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/ManyLocks.java @@ -0,0 +1,37 @@ +package examples; + +import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; + +@ThreadSafe +public class ManyLocks { + private int y; // $ Alert + + private final Lock lock1 = new ReentrantLock(); + private final Lock lock2 = new ReentrantLock(); + private final Lock lock3 = new ReentrantLock(); + + public void inc() { + lock1.lock(); + lock2.lock(); + y++; + lock2.unlock(); + lock1.unlock(); + } + + public void dec() { + lock2.lock(); + lock3.lock(); + y--; + lock3.unlock(); + lock2.unlock(); + } + + public void reset() { + lock1.lock(); + lock3.lock(); + y = 0; + lock3.unlock(); + lock1.unlock(); + } +} \ No newline at end of file From 9e77e5b0468055aca55417569d3ab8831a1c103d Mon Sep 17 00:00:00 2001 From: yoff Date: Tue, 21 Oct 2025 14:02:36 +0200 Subject: [PATCH 22/25] java: add test with deeper paths also format test files --- .../ThreadSafe/ThreadSafe.expected | 3 +- .../ThreadSafe/examples/DeepPaths.java | 61 +++++++++++++++++++ .../ThreadSafe/examples/ManyLocks.java | 50 +++++++-------- 3 files changed, 88 insertions(+), 26 deletions(-) create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/DeepPaths.java diff --git a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected index a4da07d7ac6d..3d73caaffe56 100644 --- a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected +++ b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected @@ -9,6 +9,7 @@ | examples/C.java:26:9:26: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:26:9:26:14 | this.y | this expression | | examples/C.java:30:13:30:13 | y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/C.java:30:13:30:13 | y | this expression | | examples/C.java:33:9:33:9 | y | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/C.java:33:9:33:9 | y | this expression | +| examples/DeepPaths.java:8:17:8:17 | y | This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/DeepPaths.java:7:14:7:22 | DeepPaths | DeepPaths | | examples/FaultyTurnstileExample.java:18:5:18:9 | count | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/FaultyTurnstileExample.java:18:5:18:9 | count | this expression | | examples/FaultyTurnstileExample.java:26:15:26:19 | count | This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/FaultyTurnstileExample.java:23:7:23:29 | FaultyTurnstileExample2 | FaultyTurnstileExample2 | | examples/FlawedSemaphore.java:15:14:15:18 | state | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/FlawedSemaphore.java:15:14:15:18 | state | this expression | @@ -34,7 +35,7 @@ | examples/LockExample.java:124:5:124:21 | notRelatedToOther | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:124:5:124:21 | notRelatedToOther | this expression | | examples/LockExample.java:145:5:145:21 | notRelatedToOther | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:145:5:145:21 | notRelatedToOther | this expression | | examples/LockExample.java:153:5:153:21 | notRelatedToOther | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/LockExample.java:153:5:153:21 | notRelatedToOther | this expression | -| examples/ManyLocks.java:8:15:8:15 | y | This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/ManyLocks.java:7:14:7:22 | ManyLocks | ManyLocks | +| examples/ManyLocks.java:8:17:8:17 | y | This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/ManyLocks.java:7:14:7:22 | ManyLocks | ManyLocks | | examples/SyncLstExample.java:45:5:45:7 | lst | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/SyncLstExample.java:45:5:45:7 | lst | this expression | | examples/SyncStackExample.java:37:5:37:7 | stc | This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe. | examples/SyncStackExample.java:37:5:37:7 | stc | this expression | | examples/SynchronizedAndLock.java:10:17:10:22 | length | This field is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe. | examples/SynchronizedAndLock.java:7:14:7:32 | SynchronizedAndLock | SynchronizedAndLock | diff --git a/java/ql/test/query-tests/ThreadSafe/examples/DeepPaths.java b/java/ql/test/query-tests/ThreadSafe/examples/DeepPaths.java new file mode 100644 index 000000000000..095087a50182 --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/DeepPaths.java @@ -0,0 +1,61 @@ +package examples; + +import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; + +@ThreadSafe +public class DeepPaths { + private int y; // $ Alert + + private final Lock lock1 = new ReentrantLock(); + private final Lock lock2 = new ReentrantLock(); + private final Lock lock3 = new ReentrantLock(); + + public void layer1Locked() { + lock1.lock(); + this.layer2Locked(); + lock1.unlock(); + } + + private void layer2Locked() { + lock2.lock(); + this.layer3Unlocked(); + lock2.unlock(); + } + + private void layer3Locked() { + lock3.lock(); + y++; + lock3.unlock(); + } + + public void layer1Skip() { + lock2.lock(); + this.layer3Locked(); + lock2.unlock(); + } + + public void layer1Indirect() { + this.layer2(); + } + + private void layer2() { + this.layer2Locked(); + } + + public void layer1Unlocked() { + this.layer2Unlocked(); + } + + private void layer2Unlocked() { + this.layer3(); + } + + private void layer3() { + this.layer3Locked(); + } + + private void layer3Unlocked() { + y++; + } +} diff --git a/java/ql/test/query-tests/ThreadSafe/examples/ManyLocks.java b/java/ql/test/query-tests/ThreadSafe/examples/ManyLocks.java index 93557ecdafea..a7e19b3424bf 100644 --- a/java/ql/test/query-tests/ThreadSafe/examples/ManyLocks.java +++ b/java/ql/test/query-tests/ThreadSafe/examples/ManyLocks.java @@ -5,33 +5,33 @@ @ThreadSafe public class ManyLocks { - private int y; // $ Alert + private int y; // $ Alert - private final Lock lock1 = new ReentrantLock(); - private final Lock lock2 = new ReentrantLock(); - private final Lock lock3 = new ReentrantLock(); + private final Lock lock1 = new ReentrantLock(); + private final Lock lock2 = new ReentrantLock(); + private final Lock lock3 = new ReentrantLock(); - public void inc() { - lock1.lock(); - lock2.lock(); - y++; - lock2.unlock(); - lock1.unlock(); - } + public void inc() { + lock1.lock(); + lock2.lock(); + y++; + lock2.unlock(); + lock1.unlock(); + } - public void dec() { - lock2.lock(); - lock3.lock(); - y--; - lock3.unlock(); - lock2.unlock(); - } + public void dec() { + lock2.lock(); + lock3.lock(); + y--; + lock3.unlock(); + lock2.unlock(); + } - public void reset() { - lock1.lock(); - lock3.lock(); - y = 0; - lock3.unlock(); - lock1.unlock(); - } + public void reset() { + lock1.lock(); + lock3.lock(); + y = 0; + lock3.unlock(); + lock1.unlock(); + } } \ No newline at end of file From 83508ba661414c392c31916bf9f3a3dea4b70673 Mon Sep 17 00:00:00 2001 From: yoff Date: Mon, 27 Oct 2025 11:25:51 +0100 Subject: [PATCH 23/25] java: adjust qhelp and examples for SafePublication --- .../src/Likely Bugs/Concurrency/SafePublication.java | 12 +++++++++--- .../Likely Bugs/Concurrency/SafePublication.qhelp | 9 ++------- .../Likely Bugs/Concurrency/UnsafePublication.java | 9 +++++++-- 3 files changed, 18 insertions(+), 12 deletions(-) diff --git a/java/ql/src/Likely Bugs/Concurrency/SafePublication.java b/java/ql/src/Likely Bugs/Concurrency/SafePublication.java index 64341017890f..76980412e8cc 100644 --- a/java/ql/src/Likely Bugs/Concurrency/SafePublication.java +++ b/java/ql/src/Likely Bugs/Concurrency/SafePublication.java @@ -1,11 +1,17 @@ public class SafePublication { - private Object value; + private volatile Object value; + private final int server_id; - public synchronized void produce() { - value = new Object(); // Safely published using synchronization + public SafePublication() { + value = new Object(); // Safely published as volatile + server_id = 1; // Safely published as final } public synchronized Object getValue() { return value; } + + public int getServerId() { + return server_id; + } } \ No newline at end of file diff --git a/java/ql/src/Likely Bugs/Concurrency/SafePublication.qhelp b/java/ql/src/Likely Bugs/Concurrency/SafePublication.qhelp index a24977e67301..4b4225304111 100644 --- a/java/ql/src/Likely Bugs/Concurrency/SafePublication.qhelp +++ b/java/ql/src/Likely Bugs/Concurrency/SafePublication.qhelp @@ -31,16 +31,11 @@ Choose a safe publication technique that fits your use case. If the value only n -

    In the following example, the value of value is not safely published. The produce method - creates a new object and assigns it to the field value. However, the field is not - declared as volatile, and there are no synchronization mechanisms in place to ensure - that the value is fully constructed before it is published.

    +

    In the following example, the values of value and server_id are not safely published. The constructor creates a new object and assigns it to the field value. However, the field is not declared as volatile or final, and there are no synchronization mechanisms in place to ensure that the value is fully constructed before it is published. A different thread may see the default value null. Similarly, the field server_id may be observed to be 0.

    -

    To fix this example, declare the field value as volatile, or use - synchronized blocks or methods to ensure that the value is fully constructed before it is - published. We illustrate the latter with the following example:

    +

    To fix this example, we declare the field value as volatile. This will ensure that all changes to the field are visible to all threads. The field server_id is only meant to be written once, so we only need the write inside the constructor to be visible to other threads; declaring it final guarantees this:

    diff --git a/java/ql/src/Likely Bugs/Concurrency/UnsafePublication.java b/java/ql/src/Likely Bugs/Concurrency/UnsafePublication.java index ddf8c8b400f5..0b7ea3309815 100644 --- a/java/ql/src/Likely Bugs/Concurrency/UnsafePublication.java +++ b/java/ql/src/Likely Bugs/Concurrency/UnsafePublication.java @@ -1,12 +1,17 @@ -@ThreadSafe public class UnsafePublication { private Object value; + private int server_id; - public void produce() { + public UnsafePublication() { value = new Object(); // Not safely published, other threads may see the default value null + server_id = 1; // Not safely published, other threads may see the default value 0 } public Object getValue() { return value; } + + public int getServerId() { + return server_id; + } } \ No newline at end of file From 531b9948191504fa0004c34260794df06e6bd0e6 Mon Sep 17 00:00:00 2001 From: yoff Date: Mon, 27 Oct 2025 14:27:32 +0100 Subject: [PATCH 24/25] java: add test for aliasing found by triage --- .../ThreadSafe/ThreadSafe.expected | 1 + .../ThreadSafe/examples/Alias.java | 21 +++++++++++++++++++ 2 files changed, 22 insertions(+) create mode 100644 java/ql/test/query-tests/ThreadSafe/examples/Alias.java diff --git a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected index 3d73caaffe56..d09771f97c1c 100644 --- a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected +++ b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected @@ -1,3 +1,4 @@ +| 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 | diff --git a/java/ql/test/query-tests/ThreadSafe/examples/Alias.java b/java/ql/test/query-tests/ThreadSafe/examples/Alias.java new file mode 100644 index 000000000000..679e2c3366a7 --- /dev/null +++ b/java/ql/test/query-tests/ThreadSafe/examples/Alias.java @@ -0,0 +1,21 @@ +package examples; + +import java.util.concurrent.locks.Lock; +import java.util.concurrent.locks.ReentrantLock; + +@ThreadSafe +public class Alias { + private int y; + + private final ReentrantLock lock = new ReentrantLock(); + + public void notMismatch() { + final ReentrantLock lock = this.lock; + lock.lock(); + try { + y = 42; // $ SPURIOUS: Alert + } finally { + this.lock.unlock(); + } + } +} \ No newline at end of file From 406e48b3bb348c6e414355ab8e01a1cd8a774bfd Mon Sep 17 00:00:00 2001 From: yoff Date: Mon, 27 Oct 2025 14:30:25 +0100 Subject: [PATCH 25/25] java: fix aliasing FP reorganise code, adding `LockField` --- java/ql/lib/semmle/code/java/Concurrency.qll | 49 ++++++++++++------- .../ThreadSafe/ThreadSafe.expected | 1 - .../ThreadSafe/examples/Alias.java | 2 +- 3 files changed, 32 insertions(+), 20 deletions(-) diff --git a/java/ql/lib/semmle/code/java/Concurrency.qll b/java/ql/lib/semmle/code/java/Concurrency.qll index b16aa850c39b..da2783bc3080 100644 --- a/java/ql/lib/semmle/code/java/Concurrency.qll +++ b/java/ql/lib/semmle/code/java/Concurrency.qll @@ -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 diff --git a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected index d09771f97c1c..3d73caaffe56 100644 --- a/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected +++ b/java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected @@ -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 | diff --git a/java/ql/test/query-tests/ThreadSafe/examples/Alias.java b/java/ql/test/query-tests/ThreadSafe/examples/Alias.java index 679e2c3366a7..802bae2fbb35 100644 --- a/java/ql/test/query-tests/ThreadSafe/examples/Alias.java +++ b/java/ql/test/query-tests/ThreadSafe/examples/Alias.java @@ -13,7 +13,7 @@ public void notMismatch() { final ReentrantLock lock = this.lock; lock.lock(); try { - y = 42; // $ SPURIOUS: Alert + y = 42; } finally { this.lock.unlock(); }