Skip to content

Commit 18bb94f

Browse files
yoffraulpardoSimonJorgensenMancofibjornarjatten
committed
java: add ThreadSafe query (P3)
Co-authored-by: Raúl Pardo <[email protected]> Co-authored-by: SimonJorgensenMancofi <[email protected]> Co-authored-by: Bjørnar Haugstad Jåtten <[email protected]>
1 parent 9202a1b commit 18bb94f

21 files changed

+1122
-0
lines changed
Lines changed: 338 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,338 @@
1+
/**
2+
* Provides classes and predicates for detecting conflicting accesses in the sense of the Java Memory Model.
3+
*/
4+
5+
import java
6+
import Concurrency
7+
8+
/**
9+
* Holds if `t` is the type of a lock.
10+
* Currently a crude test of the type name.
11+
*/
12+
pragma[inline]
13+
predicate isLockType(Type t) { t.getName().matches("%Lock%") }
14+
15+
/**
16+
* This module provides predicates, chiefly `locallyMonitors`, to check if a given expression is synchronized on a specific monitor.
17+
*/
18+
module Monitors {
19+
/**
20+
* A monitor is any object that is used to synchronize access to a shared resource.
21+
* This includes locks as well as variables used in synchronized blocks (including `this`).
22+
*/
23+
newtype TMonitor =
24+
/** Either a lock or a variable used in a synchronized block. */
25+
TVariableMonitor(Variable v) { isLockType(v.getType()) or locallySynchronizedOn(_, _, v) } or
26+
/** An instance reference used as a monitor. */
27+
TInstanceMonitor(RefType thisType) { locallySynchronizedOnThis(_, thisType) } or
28+
/** A class used as a monitor. */
29+
TClassMonitor(RefType classType) { locallySynchronizedOnClass(_, classType) }
30+
31+
/**
32+
* A monitor is any object that is used to synchronize access to a shared resource.
33+
* This includes locks as well as variables used in synchronized blocks (including `this`).
34+
*/
35+
class Monitor extends TMonitor {
36+
/** Gets the location of this monitor. */
37+
abstract Location getLocation();
38+
39+
/** Gets a textual representation of this element. */
40+
string toString() { result = "Monitor" }
41+
}
42+
43+
/**
44+
* A variable used as a monitor.
45+
* The variable is either a lock or is used in a synchronized block.
46+
* E.g `synchronized (m) { ... }` or `m.lock();`
47+
*/
48+
class VariableMonitor extends Monitor, TVariableMonitor {
49+
Variable v;
50+
51+
VariableMonitor() { this = TVariableMonitor(v) }
52+
53+
override Location getLocation() { result = v.getLocation() }
54+
55+
override string toString() { result = "VariableMonitor(" + v.toString() + ")" }
56+
57+
/** Gets the variable being used as a monitor. */
58+
Variable getVariable() { result = v }
59+
}
60+
61+
/**
62+
* An instance reference used as a monitor.
63+
* Either via `synchronized (this) { ... }` or by marking a non-static method as `synchronized`.
64+
*/
65+
class InstanceMonitor extends Monitor, TInstanceMonitor {
66+
RefType thisType;
67+
68+
InstanceMonitor() { this = TInstanceMonitor(thisType) }
69+
70+
override Location getLocation() { result = thisType.getLocation() }
71+
72+
override string toString() { result = "InstanceMonitor(" + thisType.toString() + ")" }
73+
74+
/** Gets the instance reference being used as a monitor. */
75+
RefType getThisType() { result = thisType }
76+
}
77+
78+
/**
79+
* A class used as a monitor.
80+
* This is achieved by marking a static method as `synchronized`.
81+
*/
82+
class ClassMonitor extends Monitor, TClassMonitor {
83+
RefType classType;
84+
85+
ClassMonitor() { this = TClassMonitor(classType) }
86+
87+
override Location getLocation() { result = classType.getLocation() }
88+
89+
override string toString() { result = "ClassMonitor(" + classType.toString() + ")" }
90+
91+
/** Gets the class being used as a monitor. */
92+
RefType getClassType() { result = classType }
93+
}
94+
95+
/** Holds if the expression `e` is synchronized on the monitor `m`. */
96+
predicate locallyMonitors(Expr e, Monitor m) {
97+
exists(Variable v | v = m.(VariableMonitor).getVariable() |
98+
locallyLockedOn(e, v)
99+
or
100+
locallySynchronizedOn(e, _, v)
101+
)
102+
or
103+
locallySynchronizedOnThis(e, m.(InstanceMonitor).getThisType())
104+
or
105+
locallySynchronizedOnClass(e, m.(ClassMonitor).getClassType())
106+
}
107+
108+
/** Holds if `localLock` refers to `lock`. */
109+
predicate represents(Field lock, Variable localLock) {
110+
isLockType(lock.getType()) and
111+
(
112+
localLock = lock
113+
or
114+
localLock.getInitializer() = lock.getAnAccess()
115+
)
116+
}
117+
118+
/** Holds if `e` is synchronized on the `Lock` `lock` by a locking call. */
119+
predicate locallyLockedOn(Expr e, Field lock) {
120+
isLockType(lock.getType()) and
121+
exists(Variable localLock, MethodCall lockCall, MethodCall unlockCall |
122+
represents(lock, localLock) and
123+
lockCall.getQualifier() = localLock.getAnAccess() and
124+
lockCall.getMethod().getName() in ["lock", "lockInterruptibly", "tryLock"] and
125+
unlockCall.getQualifier() = localLock.getAnAccess() and
126+
unlockCall.getMethod().getName() = "unlock"
127+
|
128+
dominates(lockCall.getControlFlowNode(), unlockCall.getControlFlowNode()) and
129+
dominates(lockCall.getControlFlowNode(), e.getControlFlowNode()) and
130+
postDominates(unlockCall.getControlFlowNode(), e.getControlFlowNode())
131+
)
132+
}
133+
}
134+
135+
/** Provides predicates, chiefly `isModifying`, to check if a given expression modifies a shared resource. */
136+
module Modification {
137+
import semmle.code.java.dataflow.FlowSummary
138+
139+
/** Holds if the field access `a` modifies a shared resource. */
140+
predicate isModifying(FieldAccess a) {
141+
a.isVarWrite()
142+
or
143+
exists(Call c | c.(MethodCall).getQualifier() = a | isModifyingCall(c))
144+
or
145+
exists(ArrayAccess aa, Assignment asa | aa.getArray() = a | asa.getDest() = aa)
146+
}
147+
148+
/** Holds if the call `c` modifies a shared resource. */
149+
predicate isModifyingCall(Call c) {
150+
exists(SummarizedCallable sc, string output, string prefix | sc.getACall() = c |
151+
sc.propagatesFlow(_, output, _, _) and
152+
prefix = "Argument[this]" and
153+
output.prefix(prefix.length()) = prefix
154+
)
155+
}
156+
}
157+
158+
/** Holds if the class is annotated as `@ThreadSafe`. */
159+
Class annotatedAsThreadSafe() { result.getAnAnnotation().getType().getName() = "ThreadSafe" }
160+
161+
/** Holds if the type `t` is thread-safe. */
162+
predicate isThreadSafeType(Type t) {
163+
t.getName().matches(["Atomic%", "Concurrent%"])
164+
or
165+
t.getName() in [
166+
"CopyOnWriteArraySet", "BlockingQueue", "ThreadLocal",
167+
// this is a method that returns a thread-safe version of the collection used as parameter
168+
"synchronizedMap", "Executor", "ExecutorService", "CopyOnWriteArrayList",
169+
"LinkedBlockingDeque", "LinkedBlockingQueue", "CompletableFuture"
170+
]
171+
or
172+
t = annotatedAsThreadSafe()
173+
}
174+
175+
/**
176+
* A field access that is exposed to potential data races.
177+
* We require the field to be in a class that is annotated as `@ThreadSafe`.
178+
*/
179+
class ExposedFieldAccess extends FieldAccess {
180+
ExposedFieldAccess() {
181+
this.getField() = annotatedAsThreadSafe().getAField() and
182+
not this.getField().isVolatile() and
183+
// field is not a lock
184+
not isLockType(this.getField().getType()) and
185+
// field is not thread-safe
186+
not isThreadSafeType(this.getField().getType()) and
187+
not isThreadSafeType(this.getField().getInitializer().getType()) and
188+
// access is not the initializer of the field
189+
not this.(VarWrite).getASource() = this.getField().getInitializer() and
190+
// access not in a constructor
191+
not this.getEnclosingCallable() = this.getField().getDeclaringType().getAConstructor() and
192+
// not a field on a local variable
193+
not this.getQualifier+().(VarAccess).getVariable() instanceof LocalVariableDecl and
194+
// not the variable mention in a synchronized statement
195+
not this = any(SynchronizedStmt sync).getExpr()
196+
}
197+
198+
// LHS of assignments are excluded from the control flow graph,
199+
// so we use the control flow node for the assignment itself instead.
200+
override ControlFlowNode getControlFlowNode() {
201+
// this is the LHS of an assignment, use the control flow node for the assignment
202+
exists(Assignment asgn | asgn.getDest() = this | result = asgn.getControlFlowNode())
203+
or
204+
// this is not the LHS of an assignment, use the default control flow node
205+
not exists(Assignment asgn | asgn.getDest() = this) and
206+
result = super.getControlFlowNode()
207+
}
208+
}
209+
210+
/** Holds if the location of `a` is strictly before the location of `b`. */
211+
pragma[inline]
212+
predicate orderedLocations(Location a, Location b) {
213+
a.getStartLine() < b.getStartLine()
214+
or
215+
a.getStartLine() = b.getStartLine() and
216+
a.getStartColumn() < b.getStartColumn()
217+
}
218+
219+
/**
220+
* A class annotated as `@ThreadSafe`.
221+
* Provides predicates to check for concurrency issues.
222+
*/
223+
class ClassAnnotatedAsThreadSafe extends Class {
224+
ClassAnnotatedAsThreadSafe() { this = annotatedAsThreadSafe() }
225+
226+
/** Holds if `a` and `b` are conflicting accesses to the same field and not monitored by the same monitor. */
227+
predicate unsynchronised(ExposedFieldAccess a, ExposedFieldAccess b) {
228+
this.conflicting(a, b) and
229+
this.publicAccess(_, a) and
230+
this.publicAccess(_, b) and
231+
not exists(Monitors::Monitor m |
232+
this.monitors(a, m) and
233+
this.monitors(b, m)
234+
)
235+
}
236+
237+
/** Holds if `a` is the earliest write to its field that is unsynchronized with `b`. */
238+
predicate unsynchronised_normalized(ExposedFieldAccess a, ExposedFieldAccess b) {
239+
this.unsynchronised(a, b) and
240+
// Eliminate double reporting by making `a` the earliest write to this field
241+
// that is unsynchronized with `b`.
242+
not exists(ExposedFieldAccess earlier_a |
243+
earlier_a.getField() = a.getField() and
244+
orderedLocations(earlier_a.getLocation(), a.getLocation())
245+
|
246+
this.unsynchronised(earlier_a, b)
247+
)
248+
}
249+
250+
/**
251+
* Holds if `a` and `b` are unsynchronized and both publicly accessible
252+
* as witnessed by `witness_a` and `witness_b`.
253+
*/
254+
predicate witness(ExposedFieldAccess a, Expr witness_a, ExposedFieldAccess b, Expr witness_b) {
255+
this.unsynchronised_normalized(a, b) and
256+
this.publicAccess(witness_a, a) and
257+
this.publicAccess(witness_b, b) and
258+
// avoid double reporting
259+
not exists(Expr better_witness_a | this.publicAccess(better_witness_a, a) |
260+
orderedLocations(better_witness_a.getLocation(), witness_a.getLocation())
261+
) and
262+
not exists(Expr better_witness_b | this.publicAccess(better_witness_b, b) |
263+
orderedLocations(better_witness_b.getLocation(), witness_b.getLocation())
264+
)
265+
}
266+
267+
/**
268+
* Actions `a` and `b` are conflicting iff
269+
* they are field access operations on the same field and
270+
* at least one of them is a write.
271+
*/
272+
predicate conflicting(ExposedFieldAccess a, ExposedFieldAccess b) {
273+
// We allow a = b, since they could be executed on different threads
274+
// We are looking for two operations:
275+
// - on the same non-volatile field
276+
a.getField() = b.getField() and
277+
// - on this class
278+
a.getField() = this.getAField() and
279+
// - where at least one is a write
280+
// wlog we assume that is `a`
281+
// We use a slightly more inclusive definition than simply `a.isVarWrite()`
282+
Modification::isModifying(a) and
283+
// Avoid reporting both `(a, b)` and `(b, a)` by choosing the tuple
284+
// where `a` appears before `b` in the source code.
285+
(
286+
(
287+
Modification::isModifying(b) and
288+
a != b
289+
)
290+
implies
291+
orderedLocations(a.getLocation(), b.getLocation())
292+
)
293+
}
294+
295+
/** Holds if `a` can be reached by a path from a public method, and all such paths are monitored by `monitor`. */
296+
predicate monitors(ExposedFieldAccess a, Monitors::Monitor monitor) {
297+
forex(Method m | this.providesAccess(m, _, a) and m.isPublic() |
298+
this.monitorsVia(m, a, monitor)
299+
)
300+
}
301+
302+
/** 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. */
303+
predicate publicAccess(Expr e, ExposedFieldAccess a) {
304+
exists(Method m | m.isPublic() | this.providesAccess(m, e, a))
305+
}
306+
307+
/**
308+
* 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.
309+
* `e` will either be `a` itself or a method call that leads to `a`.
310+
*/
311+
predicate providesAccess(Method m, Expr e, ExposedFieldAccess a) {
312+
m = this.getAMethod() and
313+
(
314+
a.getEnclosingCallable() = m and
315+
e = a
316+
or
317+
exists(MethodCall c | c.getEnclosingCallable() = m |
318+
this.providesAccess(c.getCallee(), _, a) and
319+
e = c
320+
)
321+
)
322+
}
323+
324+
/** Holds if all paths from `m` to `a` are monitored by `monitor`. */
325+
predicate monitorsVia(Method m, ExposedFieldAccess a, Monitors::Monitor monitor) {
326+
m = this.getAMethod() and
327+
this.providesAccess(m, _, a) and
328+
(a.getEnclosingCallable() = m implies Monitors::locallyMonitors(a, monitor)) and
329+
forall(MethodCall c |
330+
c.getEnclosingCallable() = m and
331+
this.providesAccess(c.getCallee(), _, a)
332+
|
333+
Monitors::locallyMonitors(c, monitor)
334+
or
335+
this.monitorsVia(c.getCallee(), a, monitor)
336+
)
337+
}
338+
}
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>
Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
/**
2+
* @name Not thread-safe
3+
* @description This class is not thread-safe. It is annotated as `@ThreadSafe`, but it has a
4+
* conflicting access to a field that is not synchronized with the same monitor.
5+
* @kind problem
6+
* @problem.severity warning
7+
* @precision high
8+
* @id java/not-threadsafe
9+
* @tags quality
10+
* reliability
11+
* concurrency
12+
*/
13+
14+
import java
15+
import semmle.code.java.ConflictingAccess
16+
17+
from
18+
ClassAnnotatedAsThreadSafe cls, FieldAccess modifyingAccess, Expr witness_modifyingAccess,
19+
FieldAccess conflictingAccess, Expr witness_conflictingAccess
20+
where
21+
cls.witness(modifyingAccess, witness_modifyingAccess, conflictingAccess, witness_conflictingAccess)
22+
select modifyingAccess,
23+
"This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor.",
24+
witness_modifyingAccess, "this expression", conflictingAccess, "this field access",
25+
witness_conflictingAccess, "this expression"
26+
// select c, a.getField()

0 commit comments

Comments
 (0)