java: add ThreadSafe query (P3)

Co-authored-by: Raúl Pardo <raul.pardo@protonmail.com>
Co-authored-by: SimonJorgensenMancofi <simon.jorgensen@mancofi.dk>
Co-authored-by: Bjørnar Haugstad Jåtten <bjornjaat@hotmail.com>

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

@@ -0,0 +1,338 @@
+/**
+ * Provides classes and predicates for detecting conflicting accesses in the sense of the Java Memory Model.
+ */
+
+import java
+import Concurrency
+
+/**
+ * Holds if `t` is the type of a lock.
+ * Currently a crude test of the type name.
+ */
+pragma[inline]
+predicate isLockType(Type t) { t.getName().matches("%Lock%") }
+
+/**
+ * This module provides predicates, chiefly `locallyMonitors`, to check if a given expression is synchronized on a specific monitor.
+ */
+module Monitors {
+  /**
+   * A monitor is any object that is used to synchronize access to a shared resource.
+   * This includes locks as well as variables used in synchronized blocks (including `this`).
+   */
+  newtype TMonitor =
+    /** Either a lock or a variable used in a synchronized block. */
+    TVariableMonitor(Variable v) { isLockType(v.getType()) or locallySynchronizedOn(_, _, v) } or
+    /** An instance reference used as a monitor. */
+    TInstanceMonitor(RefType thisType) { locallySynchronizedOnThis(_, thisType) } or
+    /** A class used as a monitor. */
+    TClassMonitor(RefType classType) { locallySynchronizedOnClass(_, classType) }
+
+  /**
+   * A monitor is any object that is used to synchronize access to a shared resource.
+   * This includes locks as well as variables used in synchronized blocks (including `this`).
+   */
+  class Monitor extends TMonitor {
+    /** Gets the location of this monitor. */
+    abstract Location getLocation();
+
+    /** Gets a textual representation of this element. */
+    string toString() { result = "Monitor" }
+  }
+
+  /**
+   * A variable used as a monitor.
+   * The variable is either a lock or is used in a synchronized block.
+   * E.g `synchronized (m) { ... }` or `m.lock();`
+   */
+  class VariableMonitor extends Monitor, TVariableMonitor {
+    Variable v;
+
+    VariableMonitor() { this = TVariableMonitor(v) }
+
+    override Location getLocation() { result = v.getLocation() }
+
+    override string toString() { result = "VariableMonitor(" + v.toString() + ")" }
+
+    /** Gets the variable being used as a monitor. */
+    Variable getVariable() { result = v }
+  }
+
+  /**
+   * An instance reference used as a monitor.
+   * Either via `synchronized (this) { ... }` or by marking a non-static method as `synchronized`.
+   */
+  class InstanceMonitor extends Monitor, TInstanceMonitor {
+    RefType thisType;
+
+    InstanceMonitor() { this = TInstanceMonitor(thisType) }
+
+    override Location getLocation() { result = thisType.getLocation() }
+
+    override string toString() { result = "InstanceMonitor(" + thisType.toString() + ")" }
+
+    /** Gets the instance reference being used as a monitor. */
+    RefType getThisType() { result = thisType }
+  }
+
+  /**
+   * A class used as a monitor.
+   * This is achieved by marking a static method as `synchronized`.
+   */
+  class ClassMonitor extends Monitor, TClassMonitor {
+    RefType classType;
+
+    ClassMonitor() { this = TClassMonitor(classType) }
+
+    override Location getLocation() { result = classType.getLocation() }
+
+    override string toString() { result = "ClassMonitor(" + classType.toString() + ")" }
+
+    /** Gets the class being used as a monitor. */
+    RefType getClassType() { result = classType }
+  }
+
+  /** Holds if the expression `e` is synchronized on the monitor `m`. */
+  predicate locallyMonitors(Expr e, Monitor m) {
+    exists(Variable v | v = m.(VariableMonitor).getVariable() |
+      locallyLockedOn(e, v)
+      or
+      locallySynchronizedOn(e, _, v)
+    )
+    or
+    locallySynchronizedOnThis(e, m.(InstanceMonitor).getThisType())
+    or
+    locallySynchronizedOnClass(e, m.(ClassMonitor).getClassType())
+  }
+
+  /** Holds if `localLock` refers to `lock`. */
+  predicate represents(Field lock, Variable localLock) {
+    isLockType(lock.getType()) and
+    (
+      localLock = lock
+      or
+      localLock.getInitializer() = lock.getAnAccess()
+    )
+  }
+
+  /** Holds if `e` is synchronized on the `Lock` `lock` by a locking call. */
+  predicate locallyLockedOn(Expr e, Field lock) {
+    isLockType(lock.getType()) and
+    exists(Variable localLock, MethodCall lockCall, MethodCall unlockCall |
+      represents(lock, localLock) and
+      lockCall.getQualifier() = localLock.getAnAccess() and
+      lockCall.getMethod().getName() in ["lock", "lockInterruptibly", "tryLock"] and
+      unlockCall.getQualifier() = localLock.getAnAccess() and
+      unlockCall.getMethod().getName() = "unlock"
+    |
+      dominates(lockCall.getControlFlowNode(), unlockCall.getControlFlowNode()) and
+      dominates(lockCall.getControlFlowNode(), e.getControlFlowNode()) and
+      postDominates(unlockCall.getControlFlowNode(), e.getControlFlowNode())
+    )
+  }
+}
+
+/** Provides predicates, chiefly `isModifying`, to check if a given expression modifies a shared resource. */
+module Modification {
+  import semmle.code.java.dataflow.FlowSummary
+
+  /** Holds if the field access `a` modifies a shared resource. */
+  predicate isModifying(FieldAccess a) {
+    a.isVarWrite()
+    or
+    exists(Call c | c.(MethodCall).getQualifier() = a | isModifyingCall(c))
+    or
+    exists(ArrayAccess aa, Assignment asa | aa.getArray() = a | asa.getDest() = aa)
+  }
+
+  /** Holds if the call `c` modifies a shared resource. */
+  predicate isModifyingCall(Call c) {
+    exists(SummarizedCallable sc, string output, string prefix | sc.getACall() = c |
+      sc.propagatesFlow(_, output, _, _) and
+      prefix = "Argument[this]" and
+      output.prefix(prefix.length()) = prefix
+    )
+  }
+}
+
+/** Holds if the class is annotated as `@ThreadSafe`. */
+Class annotatedAsThreadSafe() { result.getAnAnnotation().getType().getName() = "ThreadSafe" }
+
+/** Holds if the type `t` is thread-safe. */
+predicate isThreadSafeType(Type t) {
+  t.getName().matches(["Atomic%", "Concurrent%"])
+  or
+  t.getName() in [
+      "CopyOnWriteArraySet", "BlockingQueue", "ThreadLocal",
+      // this is a method that returns a thread-safe version of the collection used as parameter
+      "synchronizedMap", "Executor", "ExecutorService", "CopyOnWriteArrayList",
+      "LinkedBlockingDeque", "LinkedBlockingQueue", "CompletableFuture"
+    ]
+  or
+  t = annotatedAsThreadSafe()
+}
+
+/**
+ * A field access that is exposed to potential data races.
+ * We require the field to be in a class that is annotated as `@ThreadSafe`.
+ */
+class ExposedFieldAccess extends FieldAccess {
+  ExposedFieldAccess() {
+    this.getField() = annotatedAsThreadSafe().getAField() and
+    not this.getField().isVolatile() and
+    // field is not a lock
+    not isLockType(this.getField().getType()) and
+    // field is not thread-safe
+    not isThreadSafeType(this.getField().getType()) and
+    not isThreadSafeType(this.getField().getInitializer().getType()) and
+    // access is not the initializer of the field
+    not this.(VarWrite).getASource() = this.getField().getInitializer() and
+    // access not in a constructor
+    not this.getEnclosingCallable() = this.getField().getDeclaringType().getAConstructor() and
+    // not a field on a local variable
+    not this.getQualifier+().(VarAccess).getVariable() instanceof LocalVariableDecl and
+    // not the variable mention in a synchronized statement
+    not this = any(SynchronizedStmt sync).getExpr()
+  }
+
+  // LHS of assignments are excluded from the control flow graph,
+  // so we use the control flow node for the assignment itself instead.
+  override ControlFlowNode getControlFlowNode() {
+    // this is the LHS of an assignment, use the control flow node for the assignment
+    exists(Assignment asgn | asgn.getDest() = this | result = asgn.getControlFlowNode())
+    or
+    // this is not the LHS of an assignment, use the default control flow node
+    not exists(Assignment asgn | asgn.getDest() = this) and
+    result = super.getControlFlowNode()
+  }
+}
+
+/** Holds if the location of `a` is strictly before the location of `b`. */
+pragma[inline]
+predicate orderedLocations(Location a, Location b) {
+  a.getStartLine() < b.getStartLine()
+  or
+  a.getStartLine() = b.getStartLine() and
+  a.getStartColumn() < b.getStartColumn()
+}
+
+/**
+ * A class annotated as `@ThreadSafe`.
+ * Provides predicates to check for concurrency issues.
+ */
+class ClassAnnotatedAsThreadSafe extends Class {
+  ClassAnnotatedAsThreadSafe() { this = annotatedAsThreadSafe() }
+
+  /** Holds if `a` and `b` are conflicting accesses to the same field and not monitored by the same monitor. */
+  predicate unsynchronised(ExposedFieldAccess a, ExposedFieldAccess b) {
+    this.conflicting(a, b) and
+    this.publicAccess(_, a) and
+    this.publicAccess(_, b) and
+    not exists(Monitors::Monitor m |
+      this.monitors(a, m) and
+      this.monitors(b, m)
+    )
+  }
+
+  /** Holds if `a` is the earliest write to its field that is unsynchronized with `b`. */
+  predicate unsynchronised_normalized(ExposedFieldAccess a, ExposedFieldAccess b) {
+    this.unsynchronised(a, b) and
+    // Eliminate double reporting by making `a` the earliest write to this field
+    // that is unsynchronized with `b`.
+    not exists(ExposedFieldAccess earlier_a |
+      earlier_a.getField() = a.getField() and
+      orderedLocations(earlier_a.getLocation(), a.getLocation())
+    |
+      this.unsynchronised(earlier_a, b)
+    )
+  }
+
+  /**
+   * Holds if `a` and `b` are unsynchronized and both publicly accessible
+   * as witnessed by `witness_a` and `witness_b`.
+   */
+  predicate witness(ExposedFieldAccess a, Expr witness_a, ExposedFieldAccess b, Expr witness_b) {
+    this.unsynchronised_normalized(a, b) and
+    this.publicAccess(witness_a, a) and
+    this.publicAccess(witness_b, b) and
+    // avoid double reporting
+    not exists(Expr better_witness_a | this.publicAccess(better_witness_a, a) |
+      orderedLocations(better_witness_a.getLocation(), witness_a.getLocation())
+    ) and
+    not exists(Expr better_witness_b | this.publicAccess(better_witness_b, b) |
+      orderedLocations(better_witness_b.getLocation(), witness_b.getLocation())
+    )
+  }
+
+  /**
+   * Actions `a` and `b` are conflicting iff
+   * they are field access operations on the same field and
+   * at least one of them is a write.
+   */
+  predicate conflicting(ExposedFieldAccess a, ExposedFieldAccess b) {
+    // We allow a = b, since they could be executed on different threads
+    // We are looking for two operations:
+    // - on the same non-volatile field
+    a.getField() = b.getField() and
+    // - on this class
+    a.getField() = this.getAField() and
+    // - where at least one is a write
+    //   wlog we assume that is `a`
+    //   We use a slightly more inclusive definition than simply `a.isVarWrite()`
+    Modification::isModifying(a) and
+    // Avoid reporting both `(a, b)` and `(b, a)` by choosing the tuple
+    // where `a` appears before `b` in the source code.
+    (
+      (
+        Modification::isModifying(b) and
+        a != b
+      )
+      implies
+      orderedLocations(a.getLocation(), b.getLocation())
+    )
+  }
+
+  /** Holds if `a` can be reached by a path from a public method, and all such paths are monitored by `monitor`. */
+  predicate monitors(ExposedFieldAccess a, Monitors::Monitor monitor) {
+    forex(Method m | this.providesAccess(m, _, a) and m.isPublic() |
+      this.monitorsVia(m, a, monitor)
+    )
+  }
+
+  /** 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. */
+  predicate publicAccess(Expr e, ExposedFieldAccess a) {
+    exists(Method m | m.isPublic() | this.providesAccess(m, e, a))
+  }
+
+  /**
+   * 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.
+   * `e` will either be `a` itself or a method call that leads to `a`.
+   */
+  predicate providesAccess(Method m, Expr e, ExposedFieldAccess a) {
+    m = this.getAMethod() and
+    (
+      a.getEnclosingCallable() = m and
+      e = a
+      or
+      exists(MethodCall c | c.getEnclosingCallable() = m |
+        this.providesAccess(c.getCallee(), _, a) and
+        e = c
+      )
+    )
+  }
+
+  /** Holds if all paths from `m` to `a` are monitored by `monitor`. */
+  predicate monitorsVia(Method m, ExposedFieldAccess a, Monitors::Monitor monitor) {
+    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)
+    |
+      Monitors::locallyMonitors(c, monitor)
+      or
+      this.monitorsVia(c.getCallee(), a, monitor)
+    )
+  }
+}

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

@@ -0,0 +1,33 @@
+<!DOCTYPE qhelp PUBLIC
+  "-//Semmle//qhelp//EN"
+  "qhelp.dtd">
+<qhelp>
+
+
+<overview>
+<p>
+In a thread-safe class, all field accesses that can be caused by calls to public methods must be properly synchronized.</p>
+
+</overview>
+<recommendation>
+
+<p>
+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>
+
+</recommendation>
+
+<references>
+
+
+<li>
+  Java Language Specification, chapter 17:
+  <a href="https://docs.oracle.com/javase/specs/jls/se8/html/jls-17.html#jls-17.4">Threads and Locks</a>.
+</li>
+<li>
+  Java concurrency package:
+  <a href="https://docs.oracle.com/javase/8/docs/api/java/util/concurrent/package-summary.html">java.util.concurrent</a>.
+</li>
+
+
+</references>
+</qhelp>

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

@@ -0,0 +1,26 @@
+/**
+ * @name Not thread-safe
+ * @description This class is not thread-safe. It is annotated as `@ThreadSafe`, but it has a
+ *              conflicting access to a field that is not synchronized with the same monitor.
+ * @kind problem
+ * @problem.severity warning
+ * @precision high
+ * @id java/not-threadsafe
+ * @tags quality
+ *       reliability
+ *       concurrency
+ */
+
+import java
+import semmle.code.java.ConflictingAccess
+
+from
+  ClassAnnotatedAsThreadSafe cls, FieldAccess modifyingAccess, Expr witness_modifyingAccess,
+  FieldAccess conflictingAccess, Expr witness_conflictingAccess
+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()

java/ql/src/change-notes/2025-06-22-query-not-thread-safe.md

@@ -0,0 +1,4 @@
+---
+category: newQuery
+---
+* Added a new query, `java/not-threadsafe`, to detect data races in classes marked as `@ThreadSafe`.

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

@@ -0,0 +1,74 @@
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:14:9:14:14 | this.y | this field access | examples/C.java:14:9:14:14 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:15:9:15:14 | this.y | this field access | examples/C.java:15:9:15:14 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:16:9:16:14 | this.y | this field access | examples/C.java:16:9:16:14 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:16:18:16:23 | this.y | this field access | examples/C.java:16:18:16:23 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:20:9:20:14 | this.y | this field access | examples/C.java:20:9:20:14 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:21:9:21:14 | this.y | this field access | examples/C.java:21:9:21:14 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:22:9:22:14 | this.y | this field access | examples/C.java:22:9:22:14 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:22:18:22:23 | this.y | this field access | examples/C.java:22:18:22:23 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:26:9:26:14 | this.y | this field access | examples/C.java:26:9:26:14 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:30:13:30:13 | y | this field access | examples/C.java:30:13:30:13 | y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:33:9:33:9 | y | this field access | examples/C.java:33:9:33:9 | y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:39:9:39:14 | this.y | this field access | examples/C.java:39:9:39:14 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:40:9:40:14 | this.y | this field access | examples/C.java:40:9:40:14 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:41:9:41:14 | this.y | this field access | examples/C.java:41:9:41:14 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:41:18:41:23 | this.y | this field access | examples/C.java:41:18:41:23 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:53:9:53:14 | this.y | this field access | examples/C.java:53:9:53:14 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:54:9:54:14 | this.y | this field access | examples/C.java:54:9:54:14 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:55:9:55:14 | this.y | this field access | examples/C.java:55:9:55:14 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:55:18:55:23 | this.y | this field access | examples/C.java:55:18:55:23 | this.y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:61:9:61:9 | y | this field access | examples/C.java:61:9:61:9 | y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:62:9:62:9 | y | this field access | examples/C.java:62:9:62:9 | y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:63:9:63:9 | y | this field access | examples/C.java:63:9:63:9 | y | this expression |
+| examples/C.java:14:9:14:14 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/C.java:14:9:14:14 | this.y | this expression | examples/C.java:63:13:63:13 | y | this field access | examples/C.java:63:13:63:13 | y | this expression |
+| examples/FaultyTurnstileExample.java:13:5:13: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/FaultyTurnstileExample.java:13:5:13:9 | count | this expression | examples/FaultyTurnstileExample.java:18:5:18:9 | count | this field access | examples/FaultyTurnstileExample.java:18:5:18:9 | count | this expression |
+| examples/FaultyTurnstileExample.java:30:5:30: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/FaultyTurnstileExample.java:30:5:30:9 | count | this expression | examples/FaultyTurnstileExample.java:36:5:36:9 | count | this field access | examples/FaultyTurnstileExample.java:36:5:36:9 | count | this expression |
+| examples/FlawedSemaphore.java:18:7:18:11 | state | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression | examples/FlawedSemaphore.java:15:14:15:18 | state | this field access | examples/FlawedSemaphore.java:15:14:15:18 | state | this expression |
+| examples/FlawedSemaphore.java:18:7:18:11 | state | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression | examples/FlawedSemaphore.java:18:7:18:11 | state | this field access | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression |
+| examples/FlawedSemaphore.java:18:7:18:11 | state | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/FlawedSemaphore.java:18:7:18:11 | state | this expression | examples/FlawedSemaphore.java:26:7:26:11 | state | this field access | examples/FlawedSemaphore.java:26:7:26:11 | state | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:38:5:38:10 | length | this field access | examples/LockExample.java:38:5:38:10 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:39:13:39:18 | length | this field access | examples/LockExample.java:39:13:39:18 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:44:5:44:10 | length | this field access | examples/LockExample.java:44:5:44:10 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:45:13:45:18 | length | this field access | examples/LockExample.java:45:13:45:18 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:49:5:49:10 | length | this field access | examples/LockExample.java:49:5:49:10 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:57:5:57:10 | length | this field access | examples/LockExample.java:57:5:57:10 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:58:13:58:18 | length | this field access | examples/LockExample.java:58:13:58:18 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:62:5:62:10 | length | this field access | examples/LockExample.java:62:5:62:10 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:65:13:65:18 | length | this field access | examples/LockExample.java:65:13:65:18 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:69:5:69:10 | length | this field access | examples/LockExample.java:69:5:69:10 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:71:13:71:18 | length | this field access | examples/LockExample.java:71:13:71:18 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:76:5:76:10 | length | this field access | examples/LockExample.java:76:5:76:10 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:79:13:79:18 | length | this field access | examples/LockExample.java:79:13:79:18 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:127:7:127:12 | length | this field access | examples/LockExample.java:127:7:127:12 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:136:7:136:12 | length | this field access | examples/LockExample.java:136:7:136:12 | length | this expression |
+| examples/LockExample.java:24:5:24:10 | length | 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:24:5:24:10 | length | this expression | examples/LockExample.java:142:7:142:12 | length | this field access | examples/LockExample.java:142:7:142:12 | length | this expression |
+| examples/LockExample.java:25:5:25:11 | content | 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:25:5:25:11 | content | this expression | examples/LockExample.java:39:5:39:11 | content | this field access | examples/LockExample.java:39:5:39:11 | content | this expression |
+| examples/LockExample.java:25:5:25:11 | content | 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:25:5:25:11 | content | this expression | examples/LockExample.java:45:5:45:11 | content | this field access | examples/LockExample.java:45:5:45:11 | content | this expression |
+| examples/LockExample.java:25:5:25:11 | content | 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:25:5:25:11 | content | this expression | examples/LockExample.java:58:5:58:11 | content | this field access | examples/LockExample.java:58:5:58:11 | content | this expression |
+| examples/LockExample.java:25:5:25:11 | content | 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:25:5:25:11 | content | this expression | examples/LockExample.java:65:5:65:11 | content | this field access | examples/LockExample.java:65:5:65:11 | content | this expression |
+| examples/LockExample.java:25:5:25:11 | content | 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:25:5:25:11 | content | this expression | examples/LockExample.java:71:5:71:11 | content | this field access | examples/LockExample.java:71:5:71:11 | content | this expression |
+| examples/LockExample.java:25:5:25:11 | content | 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:25:5:25:11 | content | this expression | examples/LockExample.java:79:5:79:11 | content | this field access | examples/LockExample.java:79:5:79:11 | content | this expression |
+| examples/LockExample.java:38:5:38:10 | length | 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:38:5:38:10 | length | this expression | examples/LockExample.java:25:13:25:18 | length | this field access | examples/LockExample.java:25:13:25:18 | length | this expression |
+| examples/LockExample.java:38:5:38:10 | length | 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:38:5:38:10 | length | this expression | examples/LockExample.java:32:13:32:18 | length | this field access | examples/LockExample.java:32:13:32:18 | length | this expression |
+| examples/LockExample.java:38:5:38:10 | length | 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:38:5:38:10 | length | this expression | examples/LockExample.java:52:13:52:18 | length | this field access | examples/LockExample.java:52:13:52:18 | length | this expression |
+| examples/LockExample.java:38:5:38:10 | length | 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:38:5:38:10 | length | this expression | examples/LockExample.java:150:7:150:12 | length | this field access | examples/LockExample.java:150:7:150:12 | length | this expression |
+| examples/LockExample.java:39:5:39:11 | content | 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:39:5:39:11 | content | this expression | examples/LockExample.java:52:5:52:11 | content | this field access | examples/LockExample.java:52:5:52:11 | content | this expression |
+| examples/LockExample.java:85:5:85: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:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this field access | examples/LockExample.java:94:5:94:21 | notRelatedToOther | this expression |
+| examples/LockExample.java:85:5:85: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:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:112:5:112:21 | notRelatedToOther | this field access | examples/LockExample.java:112:5:112:21 | notRelatedToOther | this expression |
+| examples/LockExample.java:85:5:85: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:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:119:5:119:21 | notRelatedToOther | this field access | examples/LockExample.java:119:5:119:21 | notRelatedToOther | this expression |
+| examples/LockExample.java:85:5:85: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:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:124:5:124:21 | notRelatedToOther | this field access | examples/LockExample.java:124:5:124:21 | notRelatedToOther | this expression |
+| examples/LockExample.java:85:5:85: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:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:145:5:145:21 | notRelatedToOther | this field access | examples/LockExample.java:145:5:145:21 | notRelatedToOther | this expression |
+| examples/LockExample.java:85:5:85: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:85:5:85:21 | notRelatedToOther | this expression | examples/LockExample.java:153:5:153:21 | notRelatedToOther | this field access | examples/LockExample.java:153:5:153: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:100:5:100:21 | notRelatedToOther | this field access | examples/LockExample.java:100:5:100: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: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 |
+| examples/Test.java:43:5:43:10 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/Test.java:43:5:43:10 | this.y | this expression | examples/Test.java:52:5:52:10 | this.y | this field access | examples/Test.java:24:5:24:18 | setYPrivate(...) | this expression |
+| examples/Test.java:43:5:43:10 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/Test.java:43:5:43:10 | this.y | this expression | examples/Test.java:60:5:60:10 | this.y | this field access | examples/Test.java:60:5:60:10 | this.y | this expression |
+| examples/Test.java:43:5:43:10 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/Test.java:43:5:43:10 | this.y | this expression | examples/Test.java:74:5:74:10 | this.y | this field access | examples/Test.java:74:5:74:10 | this.y | this expression |
+| examples/Test.java:43:5:43:10 | this.y | This modifying field access (publicly accessible via $@) is conflicting with $@ (publicly accessible via $@) because they are not synchronized with the same monitor. | examples/Test.java:43:5:43:10 | this.y | this expression | examples/Test.java:74:14:74:14 | y | this field access | examples/Test.java:74:14:74:14 | y | this expression |

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

@@ -0,0 +1,2 @@
+query: Likely Bugs/Concurrency/ThreadSafe.ql
+postprocess: utils/test/InlineExpectationsTestQuery.ql

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

@@ -0,0 +1,14 @@
+/*
+ * This Java source file was generated by the Gradle 'init' task.
+ */
+package examples;
+
+public class App {
+    public String getGreeting() {
+        return "Hello World!";
+    }
+
+    public static void main(String[] args) {
+        System.out.println(new App().getGreeting());
+    }
+}

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

@@ -0,0 +1,72 @@
+package examples;
+
+import java.util.concurrent.locks.Lock;
+import java.util.concurrent.locks.ReentrantLock;
+
+@ThreadSafe
+public class C {
+
+    private int y;
+    private Lock lock = new ReentrantLock();
+    private Lock lock2 = new ReentrantLock();
+
+    public void m() {
+        this.y = 0; // $ Alert
+        this.y += 1;
+        this.y = this.y - 1;
+    }
+
+    public void n4() {
+        this.y = 0;
+        this.y += 1;
+        this.y = this.y - 1;
+    }
+
+    public void setY(int y) {
+        this.y = y;
+    }
+
+    public void test() {
+        if (y == 0) {
+            lock.lock();
+        }
+        y = 0;
+        lock.unlock();
+    }
+
+    public void n() {
+        this.lock.lock();
+        this.y = 0;
+        this.y += 1;
+        this.y = this.y - 1;
+        this.lock.unlock();
+    }
+
+    public void callTestLock2() {
+        lock2.lock();
+        setY(1);
+        lock2.unlock();
+    }
+
+    public void n2() {
+        lock.lock();
+        this.y = 0;
+        this.y += 1;
+        this.y = this.y - 1;
+        lock.unlock();
+    }
+
+    public void n3() {
+        lock.lock();
+        y = 0;
+        y += 1;
+        y = y - 1;
+        lock.unlock(); 
+    }
+
+    public void callTest() {
+        lock.lock();
+        setY(1);
+        lock.unlock();
+    }
+}

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

@@ -0,0 +1,40 @@
+package examples;
+
+import java.util.concurrent.locks.Lock;
+import java.util.concurrent.locks.ReentrantLock;
+
+@ThreadSafe
+class FaultyTurnstileExample {
+  private Lock lock = new ReentrantLock();
+  private int count = 0;
+
+  public void inc() {
+    lock.lock();
+    count++; // $ Alert
+    lock.unlock();
+  }
+
+  public void dec() {
+    count--;
+  }
+}
+
+@ThreadSafe
+class FaultyTurnstileExample2 {
+  private Lock lock1 = new ReentrantLock();
+  private Lock lock2 = new ReentrantLock();
+  private int count = 0;
+
+  public void inc() {
+    lock1.lock();
+    count++; // $ Alert 
+    lock1.unlock();
+  }
+
+  public void dec() {
+    lock2.lock();
+    count--;
+    lock2.unlock();
+  }
+}
+

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

@@ -0,0 +1,30 @@
+package examples;
+
+@ThreadSafe
+public class FlawedSemaphore {
+  private final int capacity;
+  private int state;
+
+  public FlawedSemaphore(int c) {
+    capacity = c;
+    state = 0;
+  }
+
+  public void acquire() {
+    try {
+      while (state == capacity) {
+        this.wait();
+      }
+      state++; // $ Alert
+    } catch (InterruptedException e) {
+      e.printStackTrace();
+    }
+  }
+
+  public void release() {
+    synchronized (this) {
+      state--; // State can become negative
+      this.notifyAll();
+    }
+  }
+}

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

@@ -0,0 +1,51 @@
+package examples;
+
+import java.util.concurrent.locks.Lock;
+import java.util.concurrent.locks.ReentrantLock;
+
+@ThreadSafe
+public class LockCorrect {
+  private Lock lock1 = new ReentrantLock();
+
+  private int length = 0;
+  private int notRelatedToOther = 10;
+  private int[] content  = new int[10];
+  private int thisSynchronized = 0;
+
+  public void add(int value) {
+    lock1.lock();
+    length++;
+    content[length] = value;
+    lock1.unlock();
+  }
+
+  public void removeCorrect() {
+    lock1.lock();
+    content[length] = 0;
+    length--;
+    lock1.unlock();
+  }
+
+  public void synchronizedOnLock1() {
+    synchronized(lock1) {
+      notRelatedToOther++;
+    }
+  }
+
+  public void synchronizedOnLock12() {
+    synchronized(lock1) {
+      notRelatedToOther++;
+    }
+  }
+
+  public synchronized void x() {
+    thisSynchronized++;
+  }
+
+  public void x1() {
+    synchronized(this) {
+      thisSynchronized++;
+    }
+  }
+
+}

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

@@ -0,0 +1,156 @@
+// This example shows that we only get one alert "per concurrency problem":
+// For each problematic variable, we get one alert at the earliest conflicting write.
+// If the variable is involved in several different monitors, we get an alert for each monitor that
+// is not correctly used.
+// A single alert can have many related locations, since each conflicting access which is not
+// prpoerly synchronized is a related location.
+// This leads to many lines in the .expected file.
+package examples;
+
+import java.util.concurrent.locks.Lock;
+import java.util.concurrent.locks.ReentrantLock;
+
+@ThreadSafe
+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];
+
+  public void add(int value) {
+    lock1.lock();
+    length++; // $ Alert
+    content[length] = value; // $ Alert
+    lock1.unlock();
+  }
+
+  public void removeCorrect() {
+    lock1.lock();
+    length--;
+    content[length] = 0;
+    lock1.unlock();
+  }
+
+  public void notTheSameLockAsAdd() { // use locks, but different ones
+    lock2.lock();
+    length--; // $ Alert
+    content[length] = 0; // $ Alert
+    lock2.unlock();
+  }
+
+  public void noLock() { // no locks
+    length--;
+    content[length] = 0;
+  }
+
+  public void fieldUpdatedOutsideOfLock() { // adjusts length without lock
+    length--;
+
+    lock1.lock();
+    content[length] = 0;
+    lock1.unlock();
+  }
+
+  public synchronized void synchronizedLock() { // no locks, but with synchronized
+    length--;
+    content[length] = 0;
+  }
+
+  public void onlyLocked() { // never unlocked, only locked
+    length--;
+
+    lock1.lock();
+    content[length] = 0;
+  }
+
+  public void onlyUnlocked() { // never locked, only unlocked
+    length--;
+
+    content[length] = 0;
+    lock1.unlock();
+  }
+
+  public void notSameLock() {
+    length--;
+
+    lock2.lock();// Not the same lock
+    content[length] = 0;
+    lock1.unlock();
+  }
+
+  public void updateCount() {
+    lock2.lock();
+    notRelatedToOther++; // $ Alert
+    lock2.unlock();
+  }
+
+  public void updateCountTwiceCorrect() {
+    lock2.lock();
+    notRelatedToOther++;
+    lock2.unlock();
+    lock1.lock();
+    notRelatedToOther++; // $ Alert
+    lock1.unlock();
+  }
+
+  public void updateCountTwiceDifferentLocks() {
+    lock2.lock();
+    notRelatedToOther++;
+    lock2.unlock();
+    lock1.lock();
+    notRelatedToOther++;
+    lock2.unlock();
+  }
+
+  public void updateCountTwiceLock() {
+    lock2.lock();
+    notRelatedToOther++;
+    lock2.unlock();
+    lock1.lock();
+    notRelatedToOther++;
+  }
+
+  public void updateCountTwiceUnLock() {
+    lock2.lock();
+    notRelatedToOther++;
+    lock2.unlock();
+    notRelatedToOther++;
+    lock1.unlock();
+  }
+
+  public void synchronizedNonRelatedOutside() {
+    notRelatedToOther++;
+
+    synchronized(this) {
+      length++;
+    }
+  }
+
+  public void synchronizedNonRelatedOutside2() {
+    int x = 0;
+    x++;
+
+    synchronized(this) {
+      length++;
+    }
+  }
+
+  public void synchronizedNonRelatedOutside3() {
+    synchronized(this) {
+      length++;
+    }
+
+    notRelatedToOther = 1;
+  }
+
+  public void synchronizedNonRelatedOutside4() {
+    synchronized(lock1) {
+      length++;
+    }
+
+    notRelatedToOther = 1;
+  }
+
+}

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

@@ -0,0 +1,33 @@
+package examples;
+
+import java.util.Random;
+import java.util.concurrent.locks.Lock;
+import java.util.concurrent.locks.ReentrantLock;
+
+@ThreadSafe
+public class LoopyCallGraph {
+  private Lock lock = new ReentrantLock();
+  private int count = 0;
+  private Random random = new Random();
+
+  public void entry() {
+    if (random.nextBoolean()) {
+      increase();  // this looks like an unprotected path to a call to dec()
+    } else {
+      lock.lock();
+      dec();
+      lock.unlock();
+    }
+  }
+
+  private void increase() {
+    lock.lock();
+    count = 10;  //$ SPURIOUS: Alert
+    lock.unlock();
+    entry();  // this looks like an unprotected path to a call to dec()
+  }
+
+  private void dec() {
+    count--;
+  }
+}

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

@@ -0,0 +1,47 @@
+package examples;
+
+import java.util.List;
+import java.util.concurrent.locks.Lock;
+import java.util.concurrent.locks.ReentrantLock;
+
+@ThreadSafe
+public class SyncLstExample<T> {
+  private Lock lock = new ReentrantLock();
+  private List<T> lst;
+
+  public SyncLstExample(List<T> lst) {
+    this.lst = lst;
+  }
+
+  public void add(T item) {
+    lock.lock();
+    lst.add(item);
+    lock.unlock();
+  }
+
+  public void remove(int i) {
+    lock.lock();
+    lst.remove(i);
+    lock.unlock();
+  }
+}
+
+@ThreadSafe
+class FaultySyncLstExample<T> {
+  private Lock lock = new ReentrantLock();
+  private List<T> lst;
+
+  public FaultySyncLstExample(List<T> lst) {
+    this.lst = lst;
+  }
+
+  public void add(T item) {
+    lock.lock();
+    lst.add(item); // $ Alert
+    lock.unlock();
+  }
+
+  public void remove(int i) {
+    lst.remove(i);
+  }
+}

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

@@ -0,0 +1,39 @@
+package examples;
+
+import java.util.Stack;
+import java.util.concurrent.locks.Lock;
+import java.util.concurrent.locks.ReentrantLock;
+
+@ThreadSafe
+public class SyncStackExample<T> {
+  private Lock lock = new ReentrantLock();
+  private Stack<T> stc = new Stack<T>();
+
+  public void push(T item) {
+    lock.lock();
+    stc.push(item);
+    lock.unlock();
+  }
+
+  public void pop() {
+    lock.lock();
+    stc.pop();
+    lock.unlock();
+  }
+}
+
+@ThreadSafe
+class FaultySyncStackExample<T> {
+  private Lock lock = new ReentrantLock();
+  private Stack<T> stc = new Stack<T>();
+
+  public void push(T item) {
+    lock.lock();
+    stc.push(item); // $ Alert
+    lock.unlock();
+  }
+
+  public void pop() {
+    stc.pop();
+  }
+}

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

@@ -0,0 +1,21 @@
+package examples;
+
+import java.util.concurrent.locks.Lock;
+import java.util.concurrent.locks.ReentrantLock;
+
+@ThreadSafe
+public class SynchronizedAndLock {
+    private Lock lock = new ReentrantLock();
+
+    private int length = 0;
+
+    public void add(int value) {
+        lock.lock();
+        length++; // $ Alert
+        lock.unlock();
+    }
+
+    public synchronized void subtract() {
+        length--;
+    }
+}

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

@@ -0,0 +1,76 @@
+package examples;
+import java.util.concurrent.locks.Lock;
+import java.util.concurrent.locks.ReentrantLock;
+
+@ThreadSafe
+public class Test {
+  /**
+   * Escaping field due to public visuability.
+   */
+  int publicField;
+  
+  private int y;
+  final int immutableField = 1;
+
+  // As of the below examples with synchronized as well. Except the incorretly placed lock.
+
+  private Lock lock = new ReentrantLock();
+
+  /**
+   * Calls the a method where y field escapes.
+   * @param y
+   */
+  public void setYAgainInCorrect(int t) {
+    setYPrivate(t);
+  }
+
+  /**
+   * Locks the method where y field escapes.
+   * @param y
+   */
+  public void setYAgainCorrect(int y) {
+    lock.lock();
+    setYPrivate(y);
+    lock.unlock();
+  }
+
+  /**
+   * No escaping y field. Locks the y before assignment.
+   * @param y
+   */
+  public void setYCorrect(int y) {
+    lock.lock();
+    this.y = y; // $ Alert
+    lock.unlock();
+  }
+
+  /**
+   * No direct escaping, since it method is private. Only escaping if another public method uses this.
+   * @param y
+   */
+  private void setYPrivate(int y) {
+    this.y = y;
+  }
+
+  /**
+   * Incorretly locks y.
+   * @param y
+   */
+  public void setYWrongLock(int y) {
+    this.y = y;
+    lock.lock();
+    lock.unlock();
+  }
+
+  public synchronized int getImmutableField() {
+    return immutableField;
+  }
+
+  public synchronized int getImmutableField2() {
+    return immutableField;
+  }
+
+  public void testMethod() {
+    this.y = y + 2;
+  }
+}

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

@@ -0,0 +1,22 @@
+package examples;
+
+import java.util.ArrayList;
+
+// Note: Not marked as thread-safe
+// We inherit from this in Test3Super.java
+public class Test2 {
+  int x;
+  protected ArrayList<String> lst = new ArrayList<>();
+
+  public Test2() {
+    this.x = 0;
+  }
+
+  public void changeX() {
+    this.x = x + 1;
+  }
+
+  public void changeLst() {
+    lst.add("Hello");
+  }
+}

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

@@ -0,0 +1,17 @@
+package examples;
+
+@ThreadSafe
+public class Test3Super extends Test2 {  // We might want an alert here for the inherited unsafe methods.
+
+  public Test3Super() {
+    super.x = 0;
+  }
+
+  public void y() {
+    super.x = 0;  //$ MISSING: Alert
+  }
+
+  public void yLst() {
+    super.lst.add("Hello!");  //$ MISSING: Alert
+  }
+}

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

@@ -0,0 +1,4 @@
+package examples;
+
+public @interface ThreadSafe {
+}

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

@@ -0,0 +1,23 @@
+package examples;
+
+import java.util.concurrent.locks.Lock;
+import java.util.concurrent.locks.ReentrantLock;
+
+@ThreadSafe
+public class TurnstileExample {
+  private Lock lock = new ReentrantLock();
+  private int count = 0;
+
+  public void inc() {
+    Lock l = lock;
+    l.lock();
+    count++;
+    l.unlock();
+  }
+
+  public void dec() {
+    lock.lock();
+    count--;
+    lock.unlock();
+  }
+}