Java: Adopt shared SSA library

java/ql/lib/semmle/code/java/dataflow/Nullness.qll

@@ -463,6 +463,21 @@ private predicate interestingCond(SsaSourceVariable npecand, ConditionBlock cond
   not cond.getCondition().(Expr).getAChildExpr*() = npecand.getAnAccess()
 }
 
+pragma[nomagic]
+private ConditionBlock ssaIntegerGuard(SsaVariable v, boolean branch, int k, boolean is_k) {
+  result.getCondition() = integerGuard(v.getAUse(), branch, k, is_k)
+}
+
+pragma[nomagic]
+private ConditionBlock ssaIntBoundGuard(SsaVariable v, boolean branch_with_lower_bound_k, int k) {
+  result.getCondition() = intBoundGuard(v.getAUse(), branch_with_lower_bound_k, k)
+}
+
+pragma[nomagic]
+private ConditionBlock ssaEnumConstEquality(SsaVariable v, boolean polarity, EnumConstant c) {
+  result.getCondition() = enumConstEquality(v.getAUse(), polarity, c)
+}
+
 /** A pair of correlated conditions for a given NPE candidate. */
 private predicate correlatedConditions(
   SsaSourceVariable npecand, ConditionBlock cond1, ConditionBlock cond2, boolean inverted
@@ -485,25 +500,23 @@ private predicate correlatedConditions(
       inverted = branch1.booleanXor(branch2)
     )
     or
-    exists(SsaVariable v, VarRead rv1, VarRead rv2, int k, boolean branch1, boolean branch2 |
-      rv1 = v.getAUse() and
-      rv2 = v.getAUse() and
-      cond1.getCondition() = integerGuard(rv1, branch1, k, true) and
-      cond1.getCondition() = integerGuard(rv1, branch1.booleanNot(), k, false) and
-      cond2.getCondition() = integerGuard(rv2, branch2, k, true) and
-      cond2.getCondition() = integerGuard(rv2, branch2.booleanNot(), k, false) and
+    exists(SsaVariable v, int k, boolean branch1, boolean branch2 |
+      cond1 = ssaIntegerGuard(v, branch1, k, true) and
+      cond1 = ssaIntegerGuard(v, branch1.booleanNot(), k, false) and
+      cond2 = ssaIntegerGuard(v, branch2, k, true) and
+      cond2 = ssaIntegerGuard(v, branch2.booleanNot(), k, false) and
       inverted = branch1.booleanXor(branch2)
     )
     or
     exists(SsaVariable v, int k, boolean branch1, boolean branch2 |
-      cond1.getCondition() = intBoundGuard(v.getAUse(), branch1, k) and
-      cond2.getCondition() = intBoundGuard(v.getAUse(), branch2, k) and
+      cond1 = ssaIntBoundGuard(v, branch1, k) and
+      cond2 = ssaIntBoundGuard(v, branch2, k) and
       inverted = branch1.booleanXor(branch2)
     )
     or
     exists(SsaVariable v, EnumConstant c, boolean pol1, boolean pol2 |
-      cond1.getCondition() = enumConstEquality(v.getAUse(), pol1, c) and
-      cond2.getCondition() = enumConstEquality(v.getAUse(), pol2, c) and
+      cond1 = ssaEnumConstEquality(v, pol1, c) and
+      cond2 = ssaEnumConstEquality(v, pol2, c) and
       inverted = pol1.booleanXor(pol2)
     )
     or

java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll

@@ -57,7 +57,7 @@ class BaseSsaSourceVariable extends TBaseSsaSourceVariable {
 }
 
 cached
-private module SsaImpl {
+private module BaseSsaImpl {
   /** Gets the destination variable of an update of a tracked variable. */
   cached
   BaseSsaSourceVariable getDestVar(VariableUpdate upd) {
@@ -440,7 +440,7 @@ private module SsaImpl {
   }
 }
 
-private import SsaImpl
+private import BaseSsaImpl
 private import SsaDefReaches
 import SsaPublic
 

java/ql/lib/semmle/code/java/dataflow/internal/DataFlowNodes.qll

@@ -10,6 +10,8 @@ private import FlowSummaryImpl as FlowSummaryImpl
 private import DataFlowImplCommon as DataFlowImplCommon
 private import semmle.code.java.controlflow.Guards
 private import semmle.code.java.dataflow.RangeUtils
+private import semmle.code.java.dataflow.SSA
+private import SsaImpl as SsaImpl
 
 /** Gets a string for approximating the name of a field. */
 string approximateFieldContent(FieldContent fc) { result = fc.getField().getName().prefix(1) }
@@ -21,8 +23,34 @@ private predicate deadcode(Expr e) {
   )
 }
 
+module SsaFlow {
+  module Impl = SsaImpl::DataFlowIntegration;
+
+  Impl::Node asNode(Node n) {
+    n = TSsaNode(result)
+    or
+    result.(Impl::ExprNode).getExpr() = n.asExpr()
+    or
+    result.(Impl::ExprPostUpdateNode).getExpr() = n.(PostUpdateNode).getPreUpdateNode().asExpr()
+    or
+    TExplicitParameterNode(result.(Impl::ParameterNode).getParameter()) = n
+  }
+
+  predicate localFlowStep(
+    SsaImpl::Impl::DefinitionExt def, Node nodeFrom, Node nodeTo, boolean isUseStep
+  ) {
+    Impl::localFlowStep(def, asNode(nodeFrom), asNode(nodeTo), isUseStep)
+  }
+
+  predicate localMustFlowStep(SsaImpl::Impl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
+    Impl::localMustFlowStep(def, asNode(nodeFrom), asNode(nodeTo))
+  }
+}
+
 cached
 private module Cached {
+  private import semmle.code.java.controlflow.internal.GuardsLogic as GuardsLogic
+
   cached
   newtype TNode =
     TExprNode(Expr e) {
@@ -31,6 +59,7 @@ private module Cached {
       not e.getType() instanceof VoidType and
       not e.getParent*() instanceof Annotation
     } or
+    TSsaNode(SsaFlow::Impl::SsaNode node) or
     TExplicitParameterNode(Parameter p) { exists(p.getCallable().getBody()) } or
     TImplicitVarargsArray(Call c) {
       c.getCallee().isVarargs() and
@@ -137,6 +166,8 @@ module Public {
       result = this.(FieldValueNode).getField().getType()
       or
       result instanceof TypeObject and this instanceof AdditionalNode
+      or
+      result = this.(SsaNode).getDefinitionExt().getSourceVariable().getType()
     }
 
     /** Gets the callable in which this node occurs. */
@@ -358,6 +389,18 @@ module Public {
 
 private import Public
 
+class SsaNode extends Node, TSsaNode {
+  private SsaFlow::Impl::SsaNode node;
+
+  SsaNode() { this = TSsaNode(node) }
+
+  SsaImpl::Impl::DefinitionExt getDefinitionExt() { result = node.getDefinitionExt() }
+
+  override Location getLocation() { result = node.getLocation() }
+
+  override string toString() { result = node.toString() }
+}
+
 private class NewExpr extends PostUpdateNode, TExprNode {
   NewExpr() { exists(ClassInstanceExpr cie | this = TExprNode(cie)) }
 
@@ -398,7 +441,8 @@ module Private {
     result.asSummarizedCallable() = n.(FlowSummaryNode).getSummarizedCallable() or
     result.asCallable() = n.(CaptureNode).getSynthesizedCaptureNode().getEnclosingCallable() or
     result.asFieldScope() = n.(FieldValueNode).getField() or
-    result.asCallable() = any(Expr e | n.(AdditionalNode).nodeAt(e, _)).getEnclosingCallable()
+    result.asCallable() = any(Expr e | n.(AdditionalNode).nodeAt(e, _)).getEnclosingCallable() or
+    result.asCallable() = n.(SsaNode).getDefinitionExt().getBasicBlock().getEnclosingCallable()
   }
 
   /** Holds if `p` is a `ParameterNode` of `c` with position `pos`. */

java/ql/lib/semmle/code/java/dataflow/internal/DataFlowPrivate.qll

@@ -581,7 +581,11 @@ predicate forceHighPrecision(Content c) {
 }
 
 /** Holds if `n` should be hidden from path explanations. */
-predicate nodeIsHidden(Node n) { n instanceof FlowSummaryNode }
+predicate nodeIsHidden(Node n) {
+  n instanceof FlowSummaryNode
+  or
+  n instanceof SsaNode
+}
 
 class LambdaCallKind = Method; // the "apply" method in the functional interface
 

java/ql/lib/semmle/code/java/dataflow/internal/DataFlowUtil.qll

@@ -10,6 +10,7 @@ private import semmle.code.java.dataflow.ExternalFlow
 private import semmle.code.java.dataflow.FlowSteps
 private import semmle.code.java.dataflow.FlowSummary
 private import semmle.code.java.dataflow.InstanceAccess
+private import semmle.code.java.dataflow.internal.SsaImpl as SsaImpl
 private import FlowSummaryImpl as FlowSummaryImpl
 private import TaintTrackingUtil as TaintTrackingUtil
 private import DataFlowNodes
@@ -101,6 +102,10 @@ predicate hasNonlocalValue(FieldRead fr) {
   )
 }
 
+private predicate capturedVariableRead(Node n) {
+  n.asExpr().(VarRead).getVariable() instanceof CapturedVariable
+}
+
 cached
 private module Cached {
   /**
@@ -110,7 +115,7 @@ private module Cached {
   predicate localFlowStep(Node node1, Node node2) {
     simpleLocalFlowStep0(node1, node2, _)
     or
-    adjacentUseUse(node1.asExpr(), node2.asExpr())
+    SsaFlow::localFlowStep(_, node1, node2, _)
     or
     // Simple flow through library code is included in the exposed local
     // step relation, even though flow is technically inter-procedural
@@ -127,6 +132,20 @@ private module Cached {
   predicate simpleLocalFlowStep(Node node1, Node node2, string model) {
     simpleLocalFlowStep0(node1, node2, model)
     or
+    exists(boolean isUseStep |
+      SsaFlow::localFlowStep(_, node1, node2, isUseStep) and
+      not capturedVariableRead(node2) and
+      model = ""
+    |
+      isUseStep = false
+      or
+      isUseStep = true and
+      not exists(FieldRead fr |
+        hasNonlocalValue(fr) and fr.getField().isStatic() and fr = node1.asExpr()
+      ) and
+      not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(node1, _)
+    )
+    or
     any(AdditionalValueStep a).step(node1, node2) and
     pragma[only_bind_out](node1.getEnclosingCallable()) =
       pragma[only_bind_out](node2.getEnclosingCallable()) and
@@ -149,14 +168,7 @@ predicate localMustFlowStep(Node node1, Node node2) {
       node2.(ImplicitInstanceAccess).getInstanceAccess().(OwnInstanceAccess).getEnclosingCallable()
   )
   or
-  exists(SsaImplicitInit init |
-    init.isParameterDefinition(node1.asParameter()) and init.getAUse() = node2.asExpr()
-  )
-  or
-  exists(SsaExplicitUpdate upd |
-    upd.getDefiningExpr().(VariableAssign).getSource() = node1.asExpr() and
-    upd.getAUse() = node2.asExpr()
-  )
+  SsaFlow::localMustFlowStep(_, node1, node2)
   or
   node2.asExpr().(CastingExpr).getExpr() = node1.asExpr()
   or
@@ -168,10 +180,6 @@ predicate localMustFlowStep(Node node1, Node node2) {
 
 import Cached
 
-private predicate capturedVariableRead(Node n) {
-  n.asExpr().(VarRead).getVariable() instanceof CapturedVariable
-}
-
 /**
  * Holds if there is a data flow step from `e1` to `e2` that only steps from
  * child to parent in the AST.
@@ -213,34 +221,8 @@ predicate simpleAstFlowStep(Expr e1, Expr e2) {
 private predicate simpleLocalFlowStep0(Node node1, Node node2, string model) {
   (
     TaintTrackingUtil::forceCachingInSameStage() and
-    // Variable flow steps through adjacent def-use and use-use pairs.
-    exists(SsaExplicitUpdate upd |
-      upd.getDefiningExpr().(VariableAssign).getSource() = node1.asExpr() or
-      upd.getDefiningExpr().(AssignOp) = node1.asExpr() or
-      upd.getDefiningExpr().(RecordBindingVariableExpr) = node1.asExpr()
-    |
-      node2.asExpr() = upd.getAFirstUse() and
-      not capturedVariableRead(node2)
-    )
-    or
-    exists(SsaImplicitInit init |
-      init.isParameterDefinition(node1.asParameter()) and
-      node2.asExpr() = init.getAFirstUse() and
-      not capturedVariableRead(node2)
-    )
-    or
-    adjacentUseUse(node1.asExpr(), node2.asExpr()) and
-    not exists(FieldRead fr |
-      hasNonlocalValue(fr) and fr.getField().isStatic() and fr = node1.asExpr()
-    ) and
-    not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(node1, _) and
-    not capturedVariableRead(node2)
-    or
     ThisFlow::adjacentThisRefs(node1, node2)
     or
-    adjacentUseUse(node1.(PostUpdateNode).getPreUpdateNode().asExpr(), node2.asExpr()) and
-    not capturedVariableRead(node2)
-    or
     ThisFlow::adjacentThisRefs(node1.(PostUpdateNode).getPreUpdateNode(), node2)
     or
     simpleAstFlowStep(node1.asExpr(), node2.asExpr())
@@ -404,11 +386,7 @@ signature predicate guardChecksSig(Guard g, Expr e, boolean branch);
 module BarrierGuard<guardChecksSig/3 guardChecks> {
   /** Gets a node that is safely guarded by the given guard check. */
   Node getABarrierNode() {
-    exists(Guard g, SsaVariable v, boolean branch, VarRead use |
-      guardChecks(g, v.getAUse(), branch) and
-      use = v.getAUse() and
-      g.controls(use.getBasicBlock(), branch) and
-      result.asExpr() = use
-    )
+    SsaFlow::asNode(result) =
+      SsaImpl::DataFlowIntegration::BarrierGuard<guardChecks/3>::getABarrierNode()
   }
 }

java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll

@@ -0,0 +1,745 @@
+import java
+private import codeql.ssa.Ssa as SsaImplCommon
+private import semmle.code.java.dataflow.SSA
+private import semmle.code.java.dispatch.VirtualDispatch
+private import semmle.code.java.dispatch.WrappedInvocation
+private import semmle.code.java.controlflow.Guards as Guards
+
+predicate fieldAccessInCallable(FieldAccess fa, Field f, Callable c) {
+  f = fa.getField() and
+  c = fa.getEnclosingCallable()
+}
+
+cached
+newtype TSsaSourceVariable =
+  TLocalVar(Callable c, LocalScopeVariable v) {
+    c = v.getCallable() or c = v.getAnAccess().getEnclosingCallable()
+  } or
+  TPlainField(Callable c, Field f) {
+    exists(FieldRead fr |
+      fieldAccessInCallable(fr, f, c) and
+      (fr.isOwnFieldAccess() or f.isStatic())
+    )
+  } or
+  TEnclosingField(Callable c, Field f, RefType t) {
+    exists(FieldRead fr | fieldAccessInCallable(fr, f, c) and fr.isEnclosingFieldAccess(t))
+  } or
+  TQualifiedField(Callable c, SsaSourceVariable q, InstanceField f) {
+    exists(FieldRead fr | fieldAccessInCallable(fr, f, c) and fr.getQualifier() = q.getAnAccess())
+  }
+
+private module TrackedVariablesImpl {
+  /** Gets the number of accesses of `f`. */
+  private int numberOfAccesses(SsaSourceField f) {
+    result = strictcount(FieldAccess fa | fa = f.getAnAccess())
+  }
+
+  /** Holds if `f` is accessed inside a loop. */
+  private predicate loopAccessed(SsaSourceField f) {
+    exists(LoopStmt l, FieldRead fr | fr = f.getAnAccess() |
+      l.getBody() = fr.getEnclosingStmt().getEnclosingStmt*() or
+      l.getCondition() = fr.getParent*() or
+      l.(ForStmt).getAnUpdate() = fr.getParent*()
+    )
+  }
+
+  /** Holds if `f` is accessed more than once or inside a loop. */
+  predicate multiAccessed(SsaSourceField f) { loopAccessed(f) or 1 < numberOfAccesses(f) }
+
+  /**
+   * Holds if `f` is a field that is interesting as a basis for SSA.
+   *
+   * - A field that is read twice is interesting as we want to know whether the
+   *   reads refer to the same value.
+   * - A field that is both written and read is interesting as we want to know
+   *   whether the read might get the written value.
+   * - A field that is read in a loop is interesting as we want to know whether
+   *   the value is the same in different iterations (that is, whether the SSA
+   *   definition can be placed outside the loop).
+   * - A volatile field is never interesting, since all reads must reread from
+   *   memory and we are forced to assume that the value can change at any point.
+   */
+  cached
+  predicate trackField(SsaSourceField f) { multiAccessed(f) and not f.isVolatile() }
+
+  /**
+   * The variables that form the basis of the non-trivial SSA construction.
+   * Fields that aren't tracked get a trivial SSA construction (a definition
+   * prior to every read).
+   */
+  class TrackedVar extends SsaSourceVariable {
+    TrackedVar() {
+      this = TLocalVar(_, _) or
+      trackField(this)
+    }
+  }
+
+  class TrackedField extends TrackedVar, SsaSourceField { }
+}
+
+private import TrackedVariablesImpl
+
+private predicate untrackedFieldWrite(BasicBlock bb, int i, SsaSourceVariable v) {
+  v =
+    any(SsaSourceField nf |
+      bb.getNode(i + 1) = nf.getAnAccess().(FieldRead).getControlFlowNode() and not trackField(nf)
+    )
+}
+
+/** Gets the definition point of a nested class in the parent scope. */
+private ControlFlowNode parentDef(NestedClass nc) {
+  nc.(AnonymousClass).getClassInstanceExpr().getControlFlowNode() = result or
+  nc.(LocalClass).getLocalTypeDeclStmt().getControlFlowNode() = result
+}
+
+/**
+ * Gets the enclosing type of a nested class.
+ *
+ * Differs from `RefType.getEnclosingType()` by including anonymous classes defined by lambdas.
+ */
+private RefType desugaredGetEnclosingType(NestedClass inner) {
+  exists(ControlFlowNode node |
+    node = parentDef(inner) and
+    node.getEnclosingCallable().getDeclaringType() = result
+  )
+}
+
+/**
+ * Gets the control flow node at which the variable is read to get the value for
+ * a `VarAccess` inside a closure. `capturedvar` is the variable in its defining
+ * scope, and `closurevar` is the variable in the closure.
+ */
+private ControlFlowNode captureNode(TrackedVar capturedvar, TrackedVar closurevar) {
+  exists(
+    LocalScopeVariable v, Callable inner, Callable outer, NestedClass innerclass, VarAccess va
+  |
+    va.getVariable() = v and
+    inner = va.getEnclosingCallable() and
+    outer = v.getCallable() and
+    inner != outer and
+    inner.getDeclaringType() = innerclass and
+    result = parentDef(desugaredGetEnclosingType*(innerclass)) and
+    result.getEnclosingStmt().getEnclosingCallable() = outer and
+    capturedvar = TLocalVar(outer, v) and
+    closurevar = TLocalVar(inner, v)
+  )
+}
+
+/** Holds if the value of `v` is captured in `b` at index `i`. */
+private predicate variableCapture(TrackedVar capturedvar, TrackedVar closurevar, BasicBlock b, int i) {
+  b.getNode(i) = captureNode(capturedvar, closurevar)
+}
+
+/** Holds if `n` must update the locally tracked variable `v`. */
+pragma[nomagic]
+private predicate certainVariableUpdate(TrackedVar v, ControlFlowNode n, BasicBlock b, int i) {
+  exists(VariableUpdate a | a.getControlFlowNode() = n | getDestVar(a) = v) and
+  b.getNode(i) = n and
+  hasDominanceInformation(b)
+  or
+  certainVariableUpdate(v.getQualifier(), n, b, i)
+}
+
+/** Holds if `v` has an implicit definition at the entry, `b`, of the callable. */
+pragma[nomagic]
+private predicate hasEntryDef(TrackedVar v, BasicBlock b) {
+  exists(LocalScopeVariable l, Callable c |
+    v = TLocalVar(c, l) and c.getBody().getControlFlowNode() = b
+  |
+    l instanceof Parameter or
+    l.getCallable() != c
+  )
+  or
+  v instanceof SsaSourceField and v.getEnclosingCallable().getBody().getControlFlowNode() = b
+}
+
+/** Holds if `n` might update the locally tracked variable `v`. */
+pragma[nomagic]
+private predicate uncertainVariableUpdate(TrackedVar v, ControlFlowNode n, BasicBlock b, int i) {
+  exists(Call c | c = n.asCall() | updatesNamedField(c, v, _)) and
+  b.getNode(i) = n and
+  hasDominanceInformation(b)
+  or
+  uncertainVariableUpdate(v.getQualifier(), n, b, i)
+}
+
+private module SsaInput implements SsaImplCommon::InputSig<Location> {
+  private import java as J
+  private import semmle.code.java.controlflow.Dominance as Dom
+
+  class BasicBlock = J::BasicBlock;
+
+  class ControlFlowNode = J::ControlFlowNode;
+
+  BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { Dom::bbIDominates(result, bb) }
+
+  BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getABBSuccessor() }
+
+  class ExitBasicBlock extends BasicBlock {
+    ExitBasicBlock() { not exists(this.getABBSuccessor()) }
+  }
+
+  class SourceVariable = SsaSourceVariable;
+
+  /**
+   * Holds if the `i`th node of basic block `bb` is a (potential) write to source
+   * variable `v`. The Boolean `certain` indicates whether the write is certain.
+   *
+   * This includes implicit writes via calls.
+   */
+  predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+    certainVariableUpdate(v, _, bb, i) and
+    certain = true
+    or
+    untrackedFieldWrite(bb, i, v) and
+    certain = true
+    or
+    hasEntryDef(v, bb) and
+    i = 0 and
+    certain = true
+    or
+    uncertainVariableUpdate(v, _, bb, i) and
+    certain = false
+  }
+
+  /**
+   * Holds if the `i`th of basic block `bb` reads source variable `v`.
+   *
+   * This includes implicit reads via calls.
+   */
+  predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
+    exists(VarRead use |
+      v.getAnAccess() = use and bb.getNode(i) = use.getControlFlowNode() and certain = true
+    )
+    or
+    variableCapture(v, _, bb, i) and
+    certain = false
+  }
+}
+
+import SsaImplCommon::Make<Location, SsaInput> as Impl
+
+final class Definition = Impl::Definition;
+
+final class WriteDefinition = Impl::WriteDefinition;
+
+final class UncertainWriteDefinition = Impl::UncertainWriteDefinition;
+
+final class PhiNode = Impl::PhiNode;
+
+class UntrackedDef extends Definition {
+  private VarRead read;
+
+  UntrackedDef() { ssaUntrackedDef(this, read) }
+
+  string toString() { result = read.toString() }
+
+  Location getLocation() { result = read.getLocation() }
+}
+
+cached
+private module Cached {
+  /** Gets the destination variable of an update of a tracked variable. */
+  cached
+  TrackedVar getDestVar(VariableUpdate upd) {
+    result.getAnAccess() = upd.(Assignment).getDest()
+    or
+    exists(LocalVariableDecl v | v = upd.(LocalVariableDeclExpr).getVariable() |
+      result = TLocalVar(v.getCallable(), v)
+    )
+    or
+    result.getAnAccess() = upd.(UnaryAssignExpr).getExpr()
+  }
+
+  cached
+  predicate ssaExplicitUpdate(SsaUpdate def, VariableUpdate upd) {
+    exists(SsaSourceVariable v, BasicBlock bb, int i |
+      def.definesAt(v, bb, i) and
+      certainVariableUpdate(v, upd.getControlFlowNode(), bb, i) and
+      getDestVar(upd) = def.getSourceVariable()
+    )
+  }
+
+  cached
+  predicate ssaUntrackedDef(Definition def, VarRead read) {
+    exists(SsaSourceVariable v, BasicBlock bb, int i |
+      def.definesAt(v, bb, i) and
+      untrackedFieldWrite(bb, i, v) and
+      read.getControlFlowNode() = bb.getNode(i + 1)
+    )
+  }
+
+  /*
+   * The SSA construction for a field `f` relies on implicit update nodes at
+   * every call site that conceivably could reach an update of the field.
+   *
+   * At a first approximation we need to find update paths of the form:
+   *   Callable --(callEdge)-->* Callable(setter of f)
+   *
+   * This can be improved by excluding paths ending in:
+   *   Constructor --(intraInstanceCallEdge)-->+ Method(setter of this.f)
+   * as these updates are guaranteed not to alias with the `f` under
+   * consideration.
+   *
+   * This set of paths can be expressed positively by noting that those
+   * that set `this.f` end in zero or more `intraInstanceCallEdge`s between
+   * methods, and before those is either the originating `Call` or a
+   * `crossInstanceCallEdge`.
+   */
+
+  /**
+   * Holds if `fw` is a field write that is not relevant as an implicit SSA
+   * update, since it is an initialization and therefore cannot alias.
+   */
+  private predicate init(FieldWrite fw) {
+    fw.getEnclosingCallable() instanceof InitializerMethod
+    or
+    fw.getEnclosingCallable() instanceof Constructor and fw.isOwnFieldAccess()
+    or
+    exists(LocalVariableDecl v |
+      v.getAnAccess() = fw.getQualifier() and
+      forex(VariableAssign va | va.getDestVar() = v and exists(va.getSource()) |
+        va.getSource() instanceof ClassInstanceExpr
+      )
+    )
+  }
+
+  /**
+   * Holds if `fw` is an update of `f` in `c` that is relevant for SSA construction.
+   */
+  cached
+  predicate relevantFieldUpdate(Callable c, Field f, FieldWrite fw) {
+    fw = f.getAnAccess() and
+    not init(fw) and
+    fw.getEnclosingCallable() = c and
+    exists(TrackedField nf | nf.getField() = f)
+  }
+
+  /** Holds if `c` can change the value of `this.f` and is relevant for SSA construction. */
+  private predicate setsOwnField(Method c, Field f) {
+    exists(FieldWrite fw | relevantFieldUpdate(c, f, fw) and fw.isOwnFieldAccess())
+  }
+
+  /**
+   * Holds if `c` can change the value of `f` and is relevant for SSA
+   * construction excluding those cases covered by `setsOwnField`.
+   */
+  private predicate setsOtherField(Callable c, Field f) {
+    exists(FieldWrite fw | relevantFieldUpdate(c, f, fw) and not fw.isOwnFieldAccess())
+  }
+
+  pragma[nomagic]
+  private predicate innerclassSupertypeStar(InnerClass t1, RefType t2) {
+    t1.getASourceSupertype*().getSourceDeclaration() = t2
+  }
+
+  /**
+   * Holds if `(c1,m2)` is a call edge to a method that does not change the value
+   * of `this`.
+   *
+   * Constructor-to-constructor calls can also be intra-instance, but are not
+   * included, as this does not affect whether a call chain ends in
+   *
+   * ```
+   *   Constructor --(intraInstanceCallEdge)-->+ Method(setter of this.f)
+   * ```
+   */
+  private predicate intraInstanceCallEdge(Callable c1, Method m2) {
+    exists(MethodCall ma, RefType t1 |
+      ma.getCaller() = c1 and
+      m2 = viableImpl_v2(ma) and
+      not m2.isStatic() and
+      (
+        not exists(ma.getQualifier()) or
+        ma.getQualifier() instanceof ThisAccess or
+        ma.getQualifier() instanceof SuperAccess
+      ) and
+      c1.getDeclaringType() = t1 and
+      if t1 instanceof InnerClass
+      then
+        innerclassSupertypeStar(t1, ma.getCallee().getSourceDeclaration().getDeclaringType()) and
+        not exists(ma.getQualifier().(ThisAccess).getQualifier()) and
+        not exists(ma.getQualifier().(SuperAccess).getQualifier())
+      else any()
+    )
+  }
+
+  private Callable tgt(Call c) {
+    result = viableImpl_v2(c)
+    or
+    result = getRunnerTarget(c)
+    or
+    c instanceof ConstructorCall and result = c.getCallee().getSourceDeclaration()
+  }
+
+  /** Holds if `(c1,c2)` is an edge in the call graph. */
+  private predicate callEdge(Callable c1, Callable c2) {
+    exists(Call c | c.getCaller() = c1 and c2 = tgt(c))
+  }
+
+  /** Holds if `(c1,c2)` is an edge in the call graph excluding `intraInstanceCallEdge`. */
+  private predicate crossInstanceCallEdge(Callable c1, Callable c2) {
+    callEdge(c1, c2) and not intraInstanceCallEdge(c1, c2)
+  }
+
+  /**
+   * Holds if `call` is relevant as a potential update of `f`. This requires the
+   * existence of an update to `f` somewhere.
+   */
+  private predicate relevantCall(Call call, TrackedField f) {
+    call.getEnclosingCallable() = f.getEnclosingCallable() and
+    relevantFieldUpdate(_, f.getField(), _)
+  }
+
+  private predicate source(Call call, TrackedField f, Field field, Callable c, boolean fresh) {
+    relevantCall(call, f) and
+    field = f.getField() and
+    c = tgt(call) and
+    if c instanceof Constructor then fresh = true else fresh = false
+  }
+
+  /**
+   * A callable in a potential call-chain between a source that cares about the
+   * value of some field `f` and a sink that may overwrite `f`. The boolean
+   * `fresh` indicates whether the instance `this` in `c` has been freshly
+   * allocated along the call-chain.
+   */
+  private newtype TCallableNode =
+    MkCallableNode(Callable c, boolean fresh) { source(_, _, _, c, fresh) or edge(_, c, fresh) }
+
+  private predicate edge(TCallableNode n, Callable c2, boolean f2) {
+    exists(Callable c1, boolean f1 | n = MkCallableNode(c1, f1) |
+      intraInstanceCallEdge(c1, c2) and f2 = f1
+      or
+      crossInstanceCallEdge(c1, c2) and
+      if c2 instanceof Constructor then f2 = true else f2 = false
+    )
+  }
+
+  private predicate edge(TCallableNode n1, TCallableNode n2) {
+    exists(Callable c2, boolean f2 |
+      edge(n1, c2, f2) and
+      n2 = MkCallableNode(c2, f2)
+    )
+  }
+
+  pragma[noinline]
+  private predicate source(Call call, TrackedField f, Field field, TCallableNode n) {
+    exists(Callable c, boolean fresh |
+      source(call, f, field, c, fresh) and
+      n = MkCallableNode(c, fresh)
+    )
+  }
+
+  private predicate sink(Callable c, Field f, TCallableNode n) {
+    setsOwnField(c, f) and n = MkCallableNode(c, false)
+    or
+    setsOtherField(c, f) and n = MkCallableNode(c, _)
+  }
+
+  private predicate prunedNode(TCallableNode n) {
+    sink(_, _, n)
+    or
+    exists(TCallableNode mid | edge(n, mid) and prunedNode(mid))
+  }
+
+  private predicate prunedEdge(TCallableNode n1, TCallableNode n2) {
+    prunedNode(n1) and
+    prunedNode(n2) and
+    edge(n1, n2)
+  }
+
+  private predicate edgePlus(TCallableNode c1, TCallableNode c2) = fastTC(prunedEdge/2)(c1, c2)
+
+  /**
+   * Holds if there exists a call-chain originating in `call` that can update `f` on some instance
+   * where `f` and `call` share the same enclosing callable in which a
+   * `FieldRead` of `f` is reachable from `call`.
+   */
+  pragma[noopt]
+  private predicate updatesNamedFieldImpl(Call call, TrackedField f, Callable setter) {
+    exists(TCallableNode src, TCallableNode sink, Field field |
+      source(call, f, field, src) and
+      sink(setter, field, sink) and
+      (src = sink or edgePlus(src, sink))
+    )
+  }
+
+  cached
+  predicate defUpdatesNamedField(SsaImplicitUpdate def, TrackedField f, Callable setter) {
+    f = def.getSourceVariable() and
+    updatesNamedField(def.getCfgNode().asCall(), f, setter)
+  }
+
+  cached
+  predicate ssaUncertainImplicitUpdate(SsaImplicitUpdate def) {
+    exists(SsaSourceVariable v, BasicBlock bb, int i |
+      def.definesAt(v, bb, i) and
+      uncertainVariableUpdate(v, _, bb, i)
+    )
+  }
+
+  cached
+  predicate ssaImplicitInit(WriteDefinition def) {
+    exists(SsaSourceVariable v, BasicBlock bb, int i |
+      def.definesAt(v, bb, i) and
+      hasEntryDef(v, bb) and
+      i = 0
+    )
+  }
+
+  pragma[nomagic]
+  private predicate captureDefReaches(Definition def, SsaInput::BasicBlock bb2, int i2) {
+    variableCapture(def.getSourceVariable(), _, _, _) and
+    exists(SsaInput::BasicBlock bb1, int i1 |
+      Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and
+      def.definesAt(_, bb1, i1)
+    )
+    or
+    exists(SsaInput::BasicBlock bb3, int i3 |
+      captureDefReaches(def, bb3, i3) and
+      SsaInput::variableRead(bb3, i3, _, _) and
+      Impl::adjacentDefRead(def, bb3, i3, bb2, i2)
+    )
+  }
+
+  /** Holds if `init` is a closure variable that captures the value of `capturedvar`. */
+  cached
+  predicate captures(SsaImplicitInit init, SsaVariable capturedvar) {
+    exists(BasicBlock bb, int i |
+      captureDefReaches(capturedvar, bb, i) and
+      variableCapture(capturedvar.getSourceVariable(), init.getSourceVariable(), bb, i)
+    )
+  }
+
+  /**
+   * Holds if the SSA definition of `v` at `def` reaches `redef` without crossing another
+   * SSA definition of `v`.
+   */
+  cached
+  predicate ssaDefReachesUncertainDef(TrackedSsaDef def, SsaUncertainImplicitUpdate redef) {
+    Impl::uncertainWriteDefinitionInput(redef, def)
+  }
+
+  pragma[nomagic]
+  private predicate defReaches(Definition def, DataFlowIntegration::Node node) {
+    exists(DataFlowIntegration::SsaDefinitionExtNode nodeFrom |
+      nodeFrom.getDefinitionExt() = def and
+      DataFlowIntegrationImpl::localFlowStep(_, nodeFrom, node, false)
+    )
+    or
+    exists(DataFlowIntegration::Node mid |
+      defReaches(def, mid) and
+      DataFlowIntegrationImpl::localFlowStep(_, mid, node, _)
+    |
+      // flow into phi input node
+      mid instanceof DataFlowIntegration::SsaInputNode
+      or
+      // flow into definition
+      mid instanceof DataFlowIntegration::SsaDefinitionExtNode
+    )
+  }
+
+  /**
+   * Holds if the value defined at `def` can reach `use` without passing through
+   * any other uses, but possibly through phi nodes and uncertain implicit updates.
+   */
+  cached
+  predicate firstUse(Definition def, VarRead use) {
+    exists(DataFlowIntegration::ExprNode nodeTo |
+      nodeTo.getExpr() = use and
+      defReaches(def, nodeTo)
+    )
+  }
+
+  cached
+  VarRead getAUse(Definition def) {
+    exists(SsaSourceVariable v, BasicBlock bb, int i |
+      Impl::ssaDefReachesRead(v, def, bb, i) and
+      result.getControlFlowNode() = bb.getNode(i) and
+      result = v.getAnAccess()
+    )
+  }
+
+  cached
+  predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def) {
+    Impl::ssaDefReachesEndOfBlock(bb, def, _)
+  }
+
+  cached
+  predicate phiHasInputFromBlock(PhiNode phi, Definition inp, BasicBlock bb) {
+    Impl::phiHasInputFromBlock(phi, inp, bb)
+  }
+
+  cached
+  module DataFlowIntegration {
+    import DataFlowIntegrationImpl
+
+    cached
+    predicate localFlowStep(Impl::DefinitionExt def, Node nodeFrom, Node nodeTo, boolean isUseStep) {
+      not def instanceof UntrackedDef and
+      DataFlowIntegrationImpl::localFlowStep(def, nodeFrom, nodeTo, isUseStep)
+    }
+
+    cached
+    predicate localMustFlowStep(Impl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
+      not def instanceof UntrackedDef and
+      DataFlowIntegrationImpl::localMustFlowStep(def, nodeFrom, nodeTo)
+    }
+
+    signature predicate guardChecksSig(Guards::Guard g, Expr e, boolean branch);
+
+    cached // nothing is actually cached
+    module BarrierGuard<guardChecksSig/3 guardChecks> {
+      private predicate guardChecksAdjTypes(
+        DataFlowIntegrationInput::Guard g, DataFlowIntegrationInput::Expr e, boolean branch
+      ) {
+        guardChecks(g, e, branch)
+      }
+
+      private Node getABarrierNodeImpl() {
+        result = DataFlowIntegrationImpl::BarrierGuard<guardChecksAdjTypes/3>::getABarrierNode()
+      }
+
+      predicate getABarrierNode = getABarrierNodeImpl/0;
+    }
+  }
+
+  cached
+  module SsaPublic {
+    pragma[nomagic]
+    private predicate useReaches(VarRead use, DataFlowIntegration::Node node, boolean sameVar) {
+      exists(DataFlowIntegration::ExprNode nodeFrom |
+        nodeFrom.getExpr() = use and
+        DataFlowIntegration::localFlowStep(_, nodeFrom, node, true) and
+        sameVar = true
+      )
+      or
+      exists(DataFlowIntegration::Node mid, boolean sameVarMid |
+        useReaches(use, mid, sameVarMid) and
+        DataFlowIntegration::localFlowStep(_, mid, node, _)
+      |
+        // flow into phi input node
+        mid instanceof DataFlowIntegration::SsaInputNode and
+        sameVar = false
+        or
+        // flow into definition
+        exists(Impl::DefinitionExt def |
+          def = mid.(DataFlowIntegration::SsaDefinitionExtNode).getDefinitionExt()
+        |
+          if def instanceof Impl::PhiReadNode then sameVar = sameVarMid else sameVar = false
+        )
+      )
+    }
+
+    /**
+     * Holds if `use1` and `use2` form an adjacent use-use-pair of the same SSA
+     * variable, that is, the value read in `use1` can reach `use2` without passing
+     * through any other use or any SSA definition of the variable.
+     */
+    cached
+    predicate adjacentUseUseSameVar(VarRead use1, VarRead use2) {
+      exists(DataFlowIntegration::ExprNode nodeTo |
+        nodeTo.getExpr() = use2 and
+        useReaches(use1, nodeTo, true)
+      )
+    }
+
+    /**
+     * Holds if `use1` and `use2` form an adjacent use-use-pair of the same
+     * `SsaSourceVariable`, that is, the value read in `use1` can reach `use2`
+     * without passing through any other use or any SSA definition of the variable
+     * except for phi nodes and uncertain implicit updates.
+     */
+    cached
+    predicate adjacentUseUse(VarRead use1, VarRead use2) {
+      exists(DataFlowIntegration::ExprNode nodeTo |
+        nodeTo.getExpr() = use2 and
+        useReaches(use1, nodeTo, _)
+      )
+    }
+  }
+
+  /**
+   * Provides internal implementation predicates that are not cached and should not
+   * be used outside of this file.
+   */
+  cached // needed to avoid compilation error; has no actual effect
+  module Internal {
+    predicate updatesNamedField = updatesNamedFieldImpl/3; // use alias to avoid caching
+  }
+}
+
+import Cached
+private import Internal
+
+/**
+ * An SSA definition excluding those variables that use a trivial SSA construction.
+ */
+private class TrackedSsaDef extends Definition {
+  TrackedSsaDef() { not this.getSourceVariable() = any(SsaSourceField f | not trackField(f)) }
+
+  /**
+   * Holds if this SSA definition occurs at the specified position.
+   * Phi nodes are placed at index -1.
+   */
+  predicate definesAt(TrackedVar v, BasicBlock b, int i) { super.definesAt(v, b, i) }
+}
+
+private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInputSig {
+  private import java as J
+
+  class Expr instanceof J::Expr {
+    string toString() { result = super.toString() }
+
+    Location getLocation() { result = super.getLocation() }
+
+    predicate hasCfgNode(BasicBlock bb, int i) {
+      super.getControlFlowNode() = bb.(J::BasicBlock).getNode(i)
+    }
+  }
+
+  Expr getARead(Definition def) { result = getAUse(def) }
+
+  class Parameter = J::Parameter;
+
+  predicate ssaDefAssigns(Impl::WriteDefinition def, Expr value) {
+    exists(VariableUpdate upd | upd = def.(SsaExplicitUpdate).getDefiningExpr() |
+      value = upd.(VariableAssign).getSource() or
+      value = upd.(AssignOp) or
+      value = upd.(RecordBindingVariableExpr)
+    )
+  }
+
+  predicate ssaDefInitializesParam(Impl::WriteDefinition def, Parameter p) {
+    def.(SsaImplicitInit).getSourceVariable() =
+      any(SsaSourceVariable v |
+        v.getVariable() = p and
+        v.getEnclosingCallable() = p.getCallable()
+      )
+  }
+
+  predicate allowFlowIntoUncertainDef(UncertainWriteDefinition def) {
+    def instanceof SsaUncertainImplicitUpdate
+  }
+
+  class Guard extends Guards::Guard {
+    predicate hasCfgNode(BasicBlock bb, int i) {
+      this = bb.getNode(i).asExpr()
+      or
+      this = bb.getNode(i).asStmt()
+    }
+  }
+
+  /** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */
+  predicate guardControlsBlock(Guard guard, BasicBlock bb, boolean branch) {
+    guard.controls(bb, branch)
+  }
+
+  /** Gets an immediate conditional successor of basic block `bb`, if any. */
+  BasicBlock getAConditionalBasicBlockSuccessor(BasicBlock bb, boolean branch) {
+    result = bb.(Guards::ConditionBlock).getTestSuccessor(branch)
+  }
+}
+
+private module DataFlowIntegrationImpl = Impl::DataFlowIntegration<DataFlowIntegrationInput>;