java: rewrite conflict detection

- favour unary predicates over binary ones
(the natural "conflicting access" is binary)
- switch to a dual solution to trade recursion through forall for simple existentials.

Co-authored-by: Anders Schack-Mulligen <[email protected]>

Author: yoff

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

@@ -14,13 +14,43 @@
 import java
 import semmle.code.java.ConflictingAccess
 
+predicate unmonitored_access(
+  ClassAnnotatedAsThreadSafe cls, ExposedFieldAccess a, Expr entry, string msg, string entry_desc
+) {
+  exists(ExposedField f |
+    cls.unlocked_public_access(f, entry, _, a, true)
+    or
+    cls.unlocked_public_access(f, entry, _, a, false) and
+    cls.has_public_write_access(f)
+  ) and
+  msg =
+    "This field access (publicly accessible via $@) is not protected by any monitor, but the class is annotated as @ThreadSafe." and
+  entry_desc = "this expression"
+}
+
+predicate not_fully_monitored_field(
+  ClassAnnotatedAsThreadSafe cls, ExposedField f, string msg, string cls_name
+) {
+  (
+    // Technically there has to be a write access for a conflict to exist.
+    // But if you are locking your reads with different locks, you likely made a typo,
+    // so in this case we alert without requiring `cls.has_public_write_access(f)`
+    cls.single_monitor_mismatch(f)
+    or
+    cls.not_fully_monitored(f) and
+    cls.has_public_write_access(f)
+  ) and
+  msg =
+    "The field $@ is not properly synchronized in that no single monitor covers all accesses, but the class $@ is annotated as @ThreadSafe." and
+  cls_name = cls.getName()
+}
+
 from
-  ClassAnnotatedAsThreadSafe cls, FieldAccess modifyingAccess, Expr witness_modifyingAccess,
-  FieldAccess conflictingAccess, Expr witness_conflictingAccess
+  ClassAnnotatedAsThreadSafe cls, Top alert_element, Top alert_context, string alert_msg,
+  string context_desc
 where
-  cls.witness(modifyingAccess, witness_modifyingAccess, conflictingAccess, witness_conflictingAccess)
-select modifyingAccess,
-  "This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor.",
-  witness_modifyingAccess, "this expression", conflictingAccess, "this field access",
-  witness_conflictingAccess, "this expression"
-// select c, a.getField()
+  unmonitored_access(cls, alert_element, alert_context, alert_msg, context_desc)
+  or
+  not_fully_monitored_field(cls, alert_element, alert_msg, context_desc) and
+  alert_context = cls
+select alert_element, alert_msg, alert_context, context_desc

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

@@ -12,25 +12,25 @@ public class C {
 
     public void m() {
         this.y = 0; // $ Alert
-        this.y += 1;
-        this.y = this.y - 1;
+        this.y += 1; // $ Alert
+        this.y = this.y - 1; // $ Alert
     }
 
     public void n4() {
-        this.y = 0;
-        this.y += 1;
-        this.y = this.y - 1;
+        this.y = 0; // $ Alert
+        this.y += 1; // $ Alert
+        this.y = this.y - 1; // $ Alert
     }
 
     public void setY(int y) {
-        this.y = y;
+        this.y = y; // $ Alert
     }
 
     public void test() {
-        if (y == 0) {
+        if (y == 0) { // $ Alert
             lock.lock();
         }
-        y = 0;
+        y = 0; // $ Alert
         lock.unlock();
     }
 

java/ql/test/query-tests/ThreadSafe/ThreadSafe.expected

@@ -10,24 +10,24 @@ class FaultyTurnstileExample {
 
   public void inc() {
     lock.lock();
-    count++; // $ Alert
+    count++; // $ MISSING: Alert
     lock.unlock();
   }
 
   public void dec() {
-    count--;
+    count--; // $ Alert
   }
 }
 
 @ThreadSafe
 class FaultyTurnstileExample2 {
   private Lock lock1 = new ReentrantLock();
   private Lock lock2 = new ReentrantLock();
-  private int count = 0;
+  private int count = 0; // $ Alert
 
   public void inc() {
     lock1.lock();
-    count++; // $ Alert 
+    count++;
     lock1.unlock();
   }
 

java/ql/test/query-tests/ThreadSafe/examples/C.java

@@ -12,7 +12,7 @@ public FlawedSemaphore(int c) {
 
   public void acquire() {
     try {
-      while (state == capacity) {
+      while (state == capacity) { // $ Alert
         this.wait();
       }
       state++; // $ Alert

java/ql/test/query-tests/ThreadSafe/examples/FaultyTurnstileExample.java

@@ -15,14 +15,14 @@ public class LockExample {
   private Lock lock1 = new ReentrantLock();
   private Lock lock2 = new ReentrantLock();
 
-  private int length = 0;
-  private int notRelatedToOther = 10;
-  private int[] content  = new int[10];
+  private int length = 0; // $ Alert
+  private int notRelatedToOther = 10; // $ Alert
+  private int[] content  = new int[10]; // $ Alert
 
   public void add(int value) {
     lock1.lock();
-    length++; // $ Alert
-    content[length] = value; // $ Alert
+    length++;
+    content[length] = value;
     lock1.unlock();
   }
 
@@ -35,18 +35,18 @@ public void removeCorrect() {
 
   public void notTheSameLockAsAdd() { // use locks, but different ones
     lock2.lock();
-    length--; // $ Alert
-    content[length] = 0; // $ Alert
+    length--;
+    content[length] = 0;
     lock2.unlock();
   }
 
   public void noLock() { // no locks
-    length--;
-    content[length] = 0;
+    length--; // $ Alert
+    content[length] = 0; // $ Alert
   }
 
   public void fieldUpdatedOutsideOfLock() { // adjusts length without lock
-    length--;
+    length--; // $ Alert
 
     lock1.lock();
     content[length] = 0;
@@ -59,30 +59,30 @@ public synchronized void synchronizedLock() { // no locks, but with synchronized
   }
 
   public void onlyLocked() { // never unlocked, only locked
-    length--;
+    length--; // $ Alert
 
     lock1.lock();
-    content[length] = 0;
+    content[length] = 0; // $ Alert
   }
 
   public void onlyUnlocked() { // never locked, only unlocked
-    length--;
+    length--; // $ Alert
 
-    content[length] = 0;
+    content[length] = 0; // $ Alert
     lock1.unlock();
   }
 
   public void notSameLock() {
-    length--;
+    length--; // $ Alert
 
     lock2.lock();// Not the same lock
-    content[length] = 0;
+    content[length] = 0; // $ Alert
     lock1.unlock();
   }
 
   public void updateCount() {
     lock2.lock();
-    notRelatedToOther++; // $ Alert
+    notRelatedToOther++;
     lock2.unlock();
   }
 
@@ -91,7 +91,7 @@ public void updateCountTwiceCorrect() {
     notRelatedToOther++;
     lock2.unlock();
     lock1.lock();
-    notRelatedToOther++; // $ Alert
+    notRelatedToOther++;
     lock1.unlock();
   }
 
@@ -109,19 +109,19 @@ public void updateCountTwiceLock() {
     notRelatedToOther++;
     lock2.unlock();
     lock1.lock();
-    notRelatedToOther++;
+    notRelatedToOther++; // $ Alert
   }
 
   public void updateCountTwiceUnLock() {
     lock2.lock();
     notRelatedToOther++;
     lock2.unlock();
-    notRelatedToOther++;
+    notRelatedToOther++; // $ Alert
     lock1.unlock();
   }
 
   public void synchronizedNonRelatedOutside() {
-    notRelatedToOther++;
+    notRelatedToOther++; // $ Alert
 
     synchronized(this) {
       length++;
@@ -142,15 +142,15 @@ public void synchronizedNonRelatedOutside3() {
       length++;
     }
 
-    notRelatedToOther = 1;
+    notRelatedToOther = 1; // $ Alert
   }
 
   public void synchronizedNonRelatedOutside4() {
     synchronized(lock1) {
       length++;
     }
 
-    notRelatedToOther = 1;
+    notRelatedToOther = 1; // $ Alert
   }
 
 }

java/ql/test/query-tests/ThreadSafe/examples/FlawedSemaphore.java

@@ -37,11 +37,11 @@ public FaultySyncLstExample(List<T> lst) {
 
   public void add(T item) {
     lock.lock();
-    lst.add(item); // $ Alert
+    lst.add(item);
     lock.unlock();
   }
 
   public void remove(int i) {
-    lst.remove(i);
+    lst.remove(i); // $ Alert
   }
 }

java/ql/test/query-tests/ThreadSafe/examples/LockExample.java

@@ -29,11 +29,11 @@ class FaultySyncStackExample<T> {
 
   public void push(T item) {
     lock.lock();
-    stc.push(item); // $ Alert
+    stc.push(item);
     lock.unlock();
   }
 
   public void pop() {
-    stc.pop();
+    stc.pop(); // $ Alert
   }
 }

java/ql/test/query-tests/ThreadSafe/examples/SyncLstExample.java

@@ -7,11 +7,11 @@
 public class SynchronizedAndLock {
     private Lock lock = new ReentrantLock();
 
-    private int length = 0;
+    private int length = 0; // $ Alert
 
     public void add(int value) {
         lock.lock();
-        length++; // $ Alert
+        length++;
         lock.unlock();
     }