From 18bb94f9f70e1c4665b4a454838d6d02b1d2611e Mon Sep 17 00:00:00 2001 From: yoff Date: Mon, 13 Jan 2025 21:46:00 +0100 Subject: [PATCH 1/8] 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 4a546d595d890073169274d4ac6ca586d8c8412d Mon Sep 17 00:00:00 2001 From: yoff Date: Thu, 15 May 2025 13:06:38 +0200 Subject: [PATCH 2/8] 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 aa5cc6d0d29e218e853ee22bce786e525c84c9af Mon Sep 17 00:00:00 2001 From: yoff Date: Thu, 15 May 2025 13:16:51 +0200 Subject: [PATCH 3/8] 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 c2374e57bc87af6c96ec9b140f77e68aba346498 Mon Sep 17 00:00:00 2001 From: yoff Date: Tue, 20 May 2025 14:12:45 +0200 Subject: [PATCH 4/8] 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 6240ae92d4ae67eec52df0c0e19c6b99c11092f2 Mon Sep 17 00:00:00 2001 From: yoff Date: Thu, 22 May 2025 14:44:24 +0200 Subject: [PATCH 5/8] 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 4af6a4dd5db2..3ab82a83ec4c 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 @@ -4,6 +4,9 @@ ql/java/ql/src/Likely Bugs/Comparison/IncomparableEquals.ql ql/java/ql/src/Likely Bugs/Comparison/InconsistentEqualsHashCode.ql ql/java/ql/src/Likely Bugs/Comparison/MissingInstanceofInEquals.ql ql/java/ql/src/Likely Bugs/Comparison/RefEqBoxed.ql +ql/java/ql/src/Likely Bugs/Concurrency/Escaping.ql +ql/java/ql/src/Likely Bugs/Concurrency/SafePublication.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/Likely Typos/ContradictoryTypeChecks.ql ql/java/ql/src/Likely Bugs/Likely Typos/SuspiciousDateFormat.ql From 6cbcc22dc999f4623a342fb8b1f6726b14209291 Mon Sep 17 00:00:00 2001 From: yoff Date: Tue, 27 May 2025 15:39:41 +0200 Subject: [PATCH 6/8] 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 53d4f608de6b7242860df3f1846accea6a40491b Mon Sep 17 00:00:00 2001 From: yoff Date: Mon, 9 Jun 2025 08:40:51 +0200 Subject: [PATCH 7/8] 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 02c26ce9ab0973a731dd1af31c9caa241fe1f272 Mon Sep 17 00:00:00 2001 From: yoff Date: Mon, 9 Jun 2025 09:18:02 +0200 Subject: [PATCH 8/8] 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) {