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.

Author: yoff

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

@@ -261,18 +261,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)
     )
   }
 }

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 |

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