Java: Get rid of untracked SSA definitions.

Author: aschackmull

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

@@ -148,12 +148,10 @@ class SsaVariable extends Definition {
   /** Gets the `ControlFlowNode` at which this SSA variable is defined. */
   pragma[nomagic]
   ControlFlowNode getCfgNode() {
-    exists(BasicBlock bb, int i, int j |
+    exists(BasicBlock bb, int i |
       this.definesAt(_, bb, i) and
-      // untracked definitions are inserted just before reads
-      (if this instanceof UntrackedDef then j = i + 1 else j = i) and
       // phi nodes are inserted at position `-1`
-      result = bb.getNode(0.maximum(j))
+      result = bb.getNode(0.maximum(i))
     )
   }
 
@@ -246,8 +244,6 @@ class SsaImplicitUpdate extends SsaUpdate {
   }
 
   private string getKind() {
-    this instanceof UntrackedDef and result = "untracked"
-    or
     this.hasExplicitQualifierUpdate() and
     result = "explicit qualifier"
     or
@@ -280,8 +276,6 @@ class SsaImplicitUpdate extends SsaUpdate {
    * of its qualifiers is volatile.
    */
   predicate assignsUnknownValue() {
-    this instanceof UntrackedDef
-    or
     this.hasExplicitQualifierUpdate()
     or
     this.hasImplicitQualifierUpdate()

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

@@ -82,13 +82,6 @@ private module TrackedVariablesImpl {
 
 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
@@ -184,9 +177,6 @@ private module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock>
     certainVariableUpdate(v, _, bb, i) and
     certain = true
     or
-    untrackedFieldWrite(bb, i, v) and
-    certain = true
-    or
     hasEntryDef(v, bb) and
     i = -1 and
     certain = true
@@ -204,7 +194,10 @@ private module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock>
     hasDominanceInformation(bb) and
     (
       exists(VarRead use |
-        v.getAnAccess() = use and bb.getNode(i) = use.getControlFlowNode() and certain = true
+        v instanceof TrackedVar and
+        v.getAnAccess() = use and
+        bb.getNode(i) = use.getControlFlowNode() and
+        certain = true
       )
       or
       variableCapture(v, _, bb, i) and
@@ -223,16 +216,6 @@ 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. */
@@ -256,15 +239,6 @@ private module Cached {
     )
   }
 
-  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.