diff --git a/java/ql/lib/semmle/code/java/ConflictingAccess.qll b/java/ql/lib/semmle/code/java/ConflictingAccess.qll index 0d92438ae0f..75845044d27 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 72d0bbb1a3a..d25b09260ee 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 595aea014f2..caea22ac851 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 class LoopyCallGraph { 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() {