hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2025-12-16 16:53:25 +01:00
Code Issues Packages Projects Releases Wiki Activity

java: implement SCC contraction of the call graph

Browse Source 
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.
This commit is contained in:
yoff
2025-05-20 14:12:45 +02:00
parent 5b30153113
commit 096d5f2a56
3 changed files with 107 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files

111
java/ql/lib/semmle/code/java/ConflictingAccess.qll
View File

@@ -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)
)
}
}

2
java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected
View File

@@ -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 |

6
java/ql/test/query-tests/ThreadSafe/examples/LoopyCallGraph.java
View File

@@ -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() {