Skip to content

Commit 7a3d997

Browse files
yoffyoff
committed
java: add ThreadSafe query (P3)
1 parent dfbe08d commit 7a3d997

20 files changed

+1054
-0
lines changed

‎java/ql/lib/semmle/code/java/ConflictingAccess.qll

Lines changed: 278 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,278 @@
1+
import java
2+
import Concurrency
3+
4+
pragma[inline]
5+
predicate isLockType(Type t) { t.getName().matches("%Lock%") }
6+
7+
module Monitors {
8+
newtype TMonitor =
9+
TVariableMonitor(Variable v) { isLockType(v.getType()) or locallySynchronizedOn(_, _, v) } or
10+
TInstanceMonitor(RefType thisType) { locallySynchronizedOnThis(_, thisType) } or
11+
TClassMonitor(RefType classType) { locallySynchronizedOnClass(_, classType) }
12+
13+
class Monitor extends TMonitor {
14+
abstract Location getLocation();
15+
16+
string toString() { result = "Monitor" }
17+
}
18+
19+
class VariableMonitor extends Monitor, TVariableMonitor {
20+
Variable v;
21+
22+
VariableMonitor() { this = TVariableMonitor(v) }
23+
24+
override Location getLocation() { result = v.getLocation() }
25+
26+
override string toString() { result = "VariableMonitor(" + v.toString() + ")" }
27+
28+
Variable getVariable() { result = v }
29+
}
30+
31+
class InstanceMonitor extends Monitor, TInstanceMonitor {
32+
RefType thisType;
33+
34+
InstanceMonitor() { this = TInstanceMonitor(thisType) }
35+
36+
override Location getLocation() { result = thisType.getLocation() }
37+
38+
override string toString() { result = "InstanceMonitor(" + thisType.toString() + ")" }
39+
40+
RefType getThisType() { result = thisType }
41+
}
42+
43+
class ClassMonitor extends Monitor, TClassMonitor {
44+
RefType classType;
45+
46+
ClassMonitor() { this = TClassMonitor(classType) }
47+
48+
override Location getLocation() { result = classType.getLocation() }
49+
50+
override string toString() { result = "ClassMonitor(" + classType.toString() + ")" }
51+
52+
RefType getClassType() { result = classType }
53+
}
54+
55+
predicate locallyMonitors(Expr e, Monitor m) {
56+
exists(Variable v | v = m.(VariableMonitor).getVariable() |
57+
locallyLockedOn(e, v)
58+
or
59+
locallySynchronizedOn(e, _, v)
60+
)
61+
or
62+
locallySynchronizedOnThis(e, m.(InstanceMonitor).getThisType())
63+
or
64+
locallySynchronizedOnClass(e, m.(ClassMonitor).getClassType())
65+
}
66+
67+
/** Holds if `localLock` refers to `lock`. */
68+
predicate represents(Field lock, Variable localLock) {
69+
isLockType(lock.getType()) and
70+
(
71+
localLock = lock
72+
or
73+
localLock.getInitializer() = lock.getAnAccess()
74+
)
75+
}
76+
77+
/** Holds if `e` is synchronized on the `Lock` `lock` by a locking call. */
78+
predicate locallyLockedOn(Expr e, Field lock) {
79+
isLockType(lock.getType()) and
80+
exists(Variable localLock, MethodCall lockCall, MethodCall unlockCall |
81+
represents(lock, localLock) and
82+
lockCall.getQualifier() = localLock.getAnAccess() and
83+
lockCall.getMethod().getName() in ["lock", "lockInterruptibly", "tryLock"] and
84+
unlockCall.getQualifier() = localLock.getAnAccess() and
85+
unlockCall.getMethod().getName() = "unlock"
86+
|
87+
dominates(lockCall.getControlFlowNode(), unlockCall.getControlFlowNode()) and
88+
dominates(lockCall.getControlFlowNode(), e.getControlFlowNode()) and
89+
postDominates(unlockCall.getControlFlowNode(), e.getControlFlowNode())
90+
)
91+
}
92+
}
93+
94+
module Modification {
95+
import semmle.code.java.dataflow.FlowSummary
96+
97+
predicate isModifying(FieldAccess a) {
98+
a.isVarWrite()
99+
or
100+
exists(Call c | c.(MethodCall).getQualifier() = a | isModifyingCall(c))
101+
or
102+
exists(ArrayAccess aa, Assignment asa | aa.getArray() = a | asa.getDest() = aa)
103+
}
104+
105+
predicate isModifyingCall(Call c) {
106+
exists(SummarizedCallable sc, string output, string prefix | sc.getACall() = c |
107+
sc.propagatesFlow(_, output, _, _) and
108+
prefix = "Argument[this]" and
109+
output.prefix(prefix.length()) = prefix
110+
)
111+
}
112+
}
113+
114+
Class annotatedAsThreadSafe() { result.getAnAnnotation().getType().getName() = "ThreadSafe" }
115+
116+
predicate isThreadSafeType(Type t) {
117+
t.getName().matches(["Atomic%", "Concurrent%"])
118+
or
119+
t.getName() in [
120+
"CopyOnWriteArraySet", "BlockingQueue", "ThreadLocal",
121+
// this is a method that returns a thread-safe version of the collection used as parameter
122+
"synchronizedMap", "Executor", "ExecutorService", "CopyOnWriteArrayList",
123+
"LinkedBlockingDeque", "LinkedBlockingQueue", "CompletableFuture"
124+
]
125+
or
126+
t = annotatedAsThreadSafe()
127+
}
128+
129+
class ExposedFieldAccess extends FieldAccess {
130+
ExposedFieldAccess() {
131+
this.getField() = annotatedAsThreadSafe().getAField() and
132+
not this.getField().isVolatile() and
133+
// field is not a lock
134+
not isLockType(this.getField().getType()) and
135+
// field is not thread-safe
136+
not isThreadSafeType(this.getField().getType()) and
137+
not isThreadSafeType(this.getField().getInitializer().getType()) and
138+
// access is not the initializer of the field
139+
not this.(VarWrite).getASource() = this.getField().getInitializer() and
140+
// access not in a constructor
141+
not this.getEnclosingCallable() = this.getField().getDeclaringType().getAConstructor() and
142+
// not a field on a local variable
143+
not this.getQualifier+().(VarAccess).getVariable() instanceof LocalVariableDecl and
144+
// not the variable mention in a synchronized statement
145+
not this = any(SynchronizedStmt sync).getExpr()
146+
}
147+
148+
// LHS of assignments are excluded from the control flow graph,
149+
// so we use the control flow node for the assignment itself instead.
150+
override ControlFlowNode getControlFlowNode() {
151+
// this is the LHS of an assignment, use the control flow node for the assignment
152+
exists(Assignment asgn | asgn.getDest() = this | result = asgn.getControlFlowNode())
153+
or
154+
// this is not the LHS of an assignment, use the default control flow node
155+
not exists(Assignment asgn | asgn.getDest() = this) and
156+
result = super.getControlFlowNode()
157+
}
158+
}
159+
160+
pragma[inline]
161+
predicate orderedLocations(Location a, Location b) {
162+
a.getStartLine() < b.getStartLine()
163+
or
164+
a.getStartLine() = b.getStartLine() and
165+
a.getStartColumn() < b.getStartColumn()
166+
}
167+
168+
class ClassAnnotatedAsThreadSafe extends Class {
169+
ClassAnnotatedAsThreadSafe() { this = annotatedAsThreadSafe() }
170+
171+
predicate unsynchronised(ExposedFieldAccess a, ExposedFieldAccess b) {
172+
this.conflicting(a, b) and
173+
this.publicAccess(_, a) and
174+
this.publicAccess(_, b) and
175+
not exists(Monitors::Monitor m |
176+
this.monitors(a, m) and
177+
this.monitors(b, m)
178+
)
179+
}
180+
181+
/** Holds if `a` is the earliest write to its field that is unsynchronized with `b`. */
182+
predicate unsynchronised_normalized(ExposedFieldAccess a, ExposedFieldAccess b) {
183+
this.unsynchronised(a, b) and
184+
// Eliminate double reporting by making `a` the earliest write to this field
185+
// that is unsynchronized with `b`.
186+
not exists(ExposedFieldAccess earlier_a |
187+
earlier_a.getField() = a.getField() and
188+
orderedLocations(earlier_a.getLocation(), a.getLocation())
189+
|
190+
this.unsynchronised(earlier_a, b)
191+
)
192+
}
193+
194+
predicate witness(ExposedFieldAccess a, Expr witness_a, ExposedFieldAccess b, Expr witness_b) {
195+
this.unsynchronised_normalized(a, b) and
196+
this.publicAccess(witness_a, a) and
197+
this.publicAccess(witness_b, b) and
198+
// avoid double reporting
199+
not exists(Expr better_witness_a | this.publicAccess(better_witness_a, a) |
200+
orderedLocations(better_witness_a.getLocation(), witness_a.getLocation())
201+
) and
202+
not exists(Expr better_witness_b | this.publicAccess(better_witness_b, b) |
203+
orderedLocations(better_witness_b.getLocation(), witness_b.getLocation())
204+
)
205+
}
206+
207+
/**
208+
* Actions `a` and `b` are conflicting iff
209+
* they are field access operations on the same field and
210+
* at least one of them is a write.
211+
*/
212+
predicate conflicting(ExposedFieldAccess a, ExposedFieldAccess b) {
213+
// We allow a = b, since they could be executed on different threads
214+
// We are looking for two operations:
215+
// - on the same non-volatile field
216+
a.getField() = b.getField() and
217+
// - on this class
218+
a.getField() = this.getAField() and
219+
// - where at least one is a write
220+
// wlog we assume that is `a`
221+
// We use a slightly more inclusive definition than simply `a.isVarWrite()`
222+
Modification::isModifying(a) and
223+
// Avoid reporting both `(a, b)` and `(b, a)` by choosing the tuple
224+
// where `a` appears before `b` in the source code.
225+
(
226+
(
227+
Modification::isModifying(b) and
228+
a != b
229+
)
230+
implies
231+
orderedLocations(a.getLocation(), b.getLocation())
232+
)
233+
}
234+
235+
/** Holds if `a` can be reached by a path from a public method, and all such paths are monitored by `monitor`. */
236+
predicate monitors(ExposedFieldAccess a, Monitors::Monitor monitor) {
237+
forex(Method m | this.providesAccess(m, _, a) and m.isPublic() |
238+
this.monitorsVia(m, a, monitor)
239+
)
240+
}
241+
242+
/** 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. */
243+
predicate publicAccess(Expr e, ExposedFieldAccess a) {
244+
exists(Method m | m.isPublic() | this.providesAccess(m, e, a))
245+
}
246+
247+
/**
248+
* 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.
249+
* `e` will either be `a` itself or a method call that leads to `a`.
250+
*/
251+
predicate providesAccess(Method m, Expr e, ExposedFieldAccess a) {
252+
m = this.getAMethod() and
253+
(
254+
a.getEnclosingCallable() = m and
255+
e = a
256+
or
257+
exists(MethodCall c | c.getEnclosingCallable() = m |
258+
this.providesAccess(c.getCallee(), _, a) and
259+
e = c
260+
)
261+
)
262+
}
263+
264+
/** Holds if all paths from `m` to `a` are monitored by `monitor`. */
265+
predicate monitorsVia(Method m, ExposedFieldAccess a, Monitors::Monitor monitor) {
266+
m = this.getAMethod() and
267+
this.providesAccess(m, _, a) and
268+
(a.getEnclosingCallable() = m implies Monitors::locallyMonitors(a, monitor)) and
269+
forall(MethodCall c |
270+
c.getEnclosingCallable() = m and
271+
this.providesAccess(c.getCallee(), _, a)
272+
|
273+
Monitors::locallyMonitors(c, monitor)
274+
or
275+
this.monitorsVia(c.getCallee(), a, monitor)
276+
)
277+
}
278+
}

‎java/ql/src/Likely Bugs/Concurrency/ThreadSafe.qhelp

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
<!DOCTYPE qhelp PUBLIC
2+
"-//Semmle//qhelp//EN"
3+
"qhelp.dtd">
4+
<qhelp>
5+
6+
7+
<overview>
8+
<p>
9+
In a thread-safe class, all field accesses that can be caused by calls to public methods must be properly synchronized.</p>
10+
11+
</overview>
12+
<recommendation>
13+
14+
<p>
15+
Protect the field access with a lock. Alternatively mark the field as <code>volatile</code> 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 <code>final</code>.</p>
16+
17+
</recommendation>
18+
19+
<references>
20+
21+
22+
<li>
23+
Java Language Specification, chapter 17:
24+
<a href="https://docs.oracle.com/javase/specs/jls/se8/html/jls-17.html#jls-17.4">Threads and Locks</a>.
25+
</li>
26+
<li>
27+
Java concurrency package:
28+
<a href="https://docs.oracle.com/javase/8/docs/api/java/util/concurrent/package-summary.html">java.util.concurrent</a>.
29+
</li>
30+
31+
32+
</references>
33+
</qhelp>

‎java/ql/src/Likely Bugs/Concurrency/ThreadSafe.ql

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
/**
2+
* @id java/not-threadsafe
3+
* @name Not thread-safe
4+
* @description This class is not thread-safe. It is annotated as `@ThreadSafe`, but it has a
5+
* conflicting access to a field that is not synchronized with the same monitor.
6+
* @kind problem
7+
* @problem.severity warning
8+
*/
9+
10+
import java
11+
import semmle.code.java.ConflictingAccess
12+
13+
from
14+
ClassAnnotatedAsThreadSafe cls, FieldAccess modifyingAccess, Expr witness_modifyingAccess,
15+
FieldAccess conflictingAccess, Expr witness_conflictingAccess
16+
where
17+
cls.witness(modifyingAccess, witness_modifyingAccess, conflictingAccess, witness_conflictingAccess)
18+
select modifyingAccess,
19+
"This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor.",
20+
witness_modifyingAccess, "this expression", conflictingAccess, "this field access",
21+
witness_conflictingAccess, "this expression"
22+
// select c, a.getField()

0 commit comments

Comments
 (0)