C#: Remove ImplicitUntrackedDefinition

2026-04-30 19:26:02 +02:00 · 2020-12-21 15:25:26 +01:00
parent 7db5a999e9
commit 8d77f4bac9
11 changed files with 124 additions and 244 deletions
--- a/csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll
+++ b/csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll
@@ -621,8 +621,7 @@ private Ssa::Definition getAnSsaQualifier(Expr e, ControlFlow::Node cfn) {
 }

 private AssignableAccess getATrackedAccess(Ssa::Definition def, ControlFlow::Node cfn) {
-  result = def.getAReadAtNode(cfn) and
-  not def instanceof Ssa::ImplicitUntrackedDefinition
+  result = def.getAReadAtNode(cfn)
  or
  result = def.(Ssa::ExplicitDefinition).getADefinition().getTargetAccess() and
  cfn = def.getControlFlowNode()
--- a/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll
@@ -17,6 +17,12 @@ module Ssa {
        or
        this instanceof Property
      }
+
+      /**
+       * Holds if the this field or any of the fields part of the qualifier
+       * are volatile.
+       */
+      predicate isVolatile() { this.(Field).isVolatile() }
    }

    /** An instance field or property. */
@@ -43,10 +49,12 @@ module Ssa {
          c = v.getAnAccess().getEnclosingCallable()
        } or
        TPlainFieldOrProp(Callable c, FieldOrProp f) {
-          exists(FieldOrPropRead fr | isPlainFieldOrPropAccess(fr, f, c))
+          exists(FieldOrPropRead fr | isPlainFieldOrPropAccess(fr, f, c)) and
+          trackFieldOrProp(f)
        } or
        TQualifiedFieldOrProp(Callable c, SourceVariable q, InstanceFieldOrProp f) {
-          exists(FieldOrPropRead fr | isQualifiedFieldOrPropAccess(fr, f, c, q))
+          exists(FieldOrPropRead fr | isQualifiedFieldOrPropAccess(fr, f, c, q)) and
+          trackFieldOrProp(f)
        }

      /** Gets an access to source variable `v`. */
@@ -70,9 +78,9 @@ module Ssa {

      cached
      AssignableDefinition getADefinition(ExplicitDefinition def) {
-        exists(TrackedVar tv, AssignableDefinition ad | def = TSsaExplicitDef(tv, ad, _, _) |
+        exists(SourceVariable sv, AssignableDefinition ad | def = TSsaExplicitDef(sv, ad, _, _) |
          result = ad or
-          result = getASameOutRefDefAfter(tv, ad)
+          result = getASameOutRefDefAfter(sv, ad)
        )
      }
    }
@@ -360,6 +368,23 @@ module Ssa {
    predicate liveAfterWrite(BasicBlock bb, int i, SourceVariable v, ReadKind rk) {
      exists(int rnk | rnk = refRank(bb, i, v, Write(_)) | liveAtRank(bb, i, v, rnk, rk))
    }
+
+    /**
+     * Holds if `fp` is a field or a property that is interesting as a basis for SSA.
+     *
+     * - 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.
+     * - A property is only interesting if it is "field-like", that is, it is a
+     *   non-overridable trivial property.
+     */
+    predicate trackFieldOrProp(FieldOrProp fp) {
+      not fp.isVolatile() and
+      (
+        fp instanceof Field
+        or
+        fp = any(TrivialProperty p | not p.isOverridableOrImplementable())
+      )
+    }
  }

  private import SourceVariableImpl
@@ -460,15 +485,6 @@ module Ssa {
      }

      override Location getLocation() { result = getFirstAccess().getLocation() }
-
-      /**
-       * Holds if the this field or any of the fields part of the qualifier
-       * are volatile.
-       */
-      predicate isVolatile() {
-        this.getAssignable().(Field).isVolatile() or
-        this.getQualifier().(FieldOrPropSourceVariable).isVolatile()
-      }
    }

    /** A plain field or property. */
@@ -498,93 +514,9 @@ module Ssa {

  private import SourceVariables

-  private module TrackedVariablesImpl {
-    /** Gets the number of accesses of field or property `fp`. */
-    private int numberOfAccesses(FieldOrPropSourceVariable fp) {
-      result = strictcount(fp.getAnAccess())
-    }
-
-    /** Holds if field or property `fp` is accessed inside a loop. */
-    private predicate loopAccessed(FieldOrPropSourceVariable fp) {
-      exists(FieldOrPropRead fpr |
-        fpr = fp.getAnAccess() and
-        fpr.getAControlFlowNode().getBasicBlock().inLoop()
-      )
-    }
-
-    /** Holds if field or property `fp` is accessed more than once or inside a loop. */
-    private predicate multiAccessed(FieldOrPropSourceVariable fp) {
-      loopAccessed(fp) or 1 < numberOfAccesses(fp)
-    }
-
-    /**
-     * Holds if `fp` is a field or a property that is interesting as a basis for SSA.
-     *
-     * - A field or property that is read twice is interesting as we want to know whether
-     *   the reads refer to the same value.
-     * - A field or property that is both written and read is interesting as we want to
-     *   know whether the read might get the written value.
-     * - A field or property 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.
-     * - A property is only interesting if it is "field-like", that is, it is a
-     *   non-overridable trivial property.
-     */
-    predicate trackFieldOrProp(FieldOrPropSourceVariable fp) {
-      multiAccessed(fp) and
-      not fp.isVolatile() and
-      exists(Assignable a | a = fp.getAssignable() |
-        a instanceof Field
-        or
-        a = any(TrivialProperty p | not p.isOverridableOrImplementable())
-      )
-    }
-  }
-
-  private import TrackedVariablesImpl
-
-  /**
-   * A source variable that gets a non-trivial SSA construction.
-   */
-  private class TrackedVar extends SourceVariable {
-    TrackedVar() {
-      this instanceof LocalScopeSourceVariable or
-      trackFieldOrProp(this)
-    }
-  }
-
-  /**
-   * A field or property that gets a non-trivial SSA construction.
-   */
-  private class TrackedFieldOrProp extends TrackedVar, FieldOrPropSourceVariable { }
-
-  /**
-   * A source variable that gets a trivial SSA construction, that is a
-   * definition prior to every read.
-   */
-  private class UntrackedVar extends SourceVariable {
-    UntrackedVar() { not this instanceof TrackedVar }
-  }
-
  private module SsaDefReaches {
-    /** A non-trivial SSA definition. */
-    private class TrackedDefinition extends Definition {
-      TrackedDefinition() {
-        // Same as `not this instanceof ImplicitUntrackedDefinition` but
-        // avoids negative recursion
-        this instanceof ExplicitDefinition or
-        this instanceof ImplicitEntryDefinition or
-        this instanceof ImplicitCallDefinition or
-        this instanceof ImplicitQualifierDefinition or
-        this instanceof PseudoDefinition
-      }
-    }
-
    /**
-     * A classification of SSA variable references into reads and non-trivial
-     * SSA definitions.
+     * A classification of SSA variable references into reads definitions.
     */
    private newtype SsaRefKind =
      SsaRead() or
@@ -592,8 +524,8 @@ module Ssa {

    /**
     * Holds if the `i`th node of basic block `bb` is a reference to `v`,
-     * either a read (when `k` is `Read()`) or a non-trivial SSA definition
-     * (when `k` is `SsaDef()`).
+     * either a read (when `k` is `Read()`) or an SSA definition (when `k`
+     * is `SsaDef()`).
     */
    private predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
      exists(ReadKind rk | variableRead(bb, i, v, _, rk) |
@@ -601,7 +533,7 @@ module Ssa {
        k = SsaRead()
      )
      or
-      exists(TrackedDefinition def | definesAt(def, bb, i, v)) and
+      exists(Definition def | definesAt(def, bb, i, v)) and
      k = SsaDef()
    }

@@ -629,12 +561,10 @@ module Ssa {
    }

    /**
-     * Holds if the non-trivial SSA definition `def` reaches rank index `rankix`
-     * in its own basic block `bb`.
+     * Holds if the SSA definition `def` reaches rank index `rankix` in its own
+     * basic block `bb`.
     */
-    private predicate ssaDefReachesRank(
-      BasicBlock bb, TrackedDefinition def, int rankix, TrackedVar v
-    ) {
+    private predicate ssaDefReachesRank(BasicBlock bb, Definition def, int rankix, SourceVariable v) {
      exists(int i |
        rankix = ssaRefRank(bb, i, v, SsaDef()) and
        definesAt(def, bb, i, v)
@@ -645,12 +575,12 @@ module Ssa {
    }

    /**
-     * Holds if the non-trivial SSA definition of `v` at `def` reaches `read` in the
+     * Holds if the SSA definition of `v` at `def` reaches `read` in the
     * same basic block without crossing another SSA definition of `v`.
     * The read at `node` is of kind `rk`.
     */
    private predicate ssaDefReachesReadWithinBlock(
-      TrackedVar v, TrackedDefinition def, ControlFlow::Node read, ReadKind rk
+      SourceVariable v, Definition def, ControlFlow::Node read, ReadKind rk
    ) {
      exists(BasicBlock bb, int rankix, int i |
        ssaDefReachesRank(bb, def, rankix, v) and
@@ -660,12 +590,11 @@ module Ssa {
    }

    /**
-     * Holds if the non-trivial SSA definition of `v` at `def` reaches uncertain SSA
-     * definition `redef` in the same basic block, without crossing another SSA
-     * definition of `v`.
+     * Holds if the SSA definition of `v` at `def` reaches uncertain SSA definition
+     * `redef` in the same basic block, without crossing another SSA definition of `v`.
     */
    private predicate ssaDefReachesUncertainDefWithinBlock(
-      TrackedVar v, TrackedDefinition def, UncertainDefinition redef
+      SourceVariable v, Definition def, UncertainDefinition redef
    ) {
      exists(BasicBlock bb, int rankix, int i |
        ssaDefReachesRank(bb, def, rankix, v) and
@@ -678,7 +607,7 @@ module Ssa {
     * Same as `ssaRefRank()`, but restricted to actual reads of `def`, or
     * `def` itself.
     */
-    private int ssaDefRank(TrackedDefinition def, TrackedVar v, BasicBlock bb, int i) {
+    private int ssaDefRank(Definition def, SourceVariable v, BasicBlock bb, int i) {
      v = def.getSourceVariable() and
      result = ssaRefRank(bb, i, v, _) and
      (
@@ -688,12 +617,12 @@ module Ssa {
      )
    }

-    private int maxSsaDefRefRank(BasicBlock bb, TrackedVar v) {
+    private int maxSsaDefRefRank(BasicBlock bb, SourceVariable v) {
      result = ssaDefRank(_, v, bb, _) and
      not result + 1 = ssaDefRank(_, v, bb, _)
    }

-    private predicate varOccursInBlock(TrackedDefinition def, BasicBlock bb, TrackedVar v) {
+    private predicate varOccursInBlock(Definition def, BasicBlock bb, SourceVariable v) {
      exists(ssaDefRank(def, v, bb, _))
    }

@@ -710,7 +639,7 @@ module Ssa {
     * and the underlying variable for `def` is neither read nor written in any block
     * on the path between `bb1` and `bb2`.
     */
-    private predicate varBlockReaches(TrackedDefinition def, BasicBlock bb1, BasicBlock bb2) {
+    private predicate varBlockReaches(Definition def, BasicBlock bb1, BasicBlock bb2) {
      varOccursInBlock(def, bb1, _) and
      bb2 = bb1.getASuccessor()
      or
@@ -724,9 +653,7 @@ module Ssa {
     * `def` is read at `cfn`, `cfn` is in a transitive successor block of `bb1`,
     * and `def` is not read in any block on the path between `bb1` and `cfn`.
     */
-    private predicate varBlockReachesRead(
-      TrackedDefinition def, BasicBlock bb1, ControlFlow::Node cfn
-    ) {
+    private predicate varBlockReachesRead(Definition def, BasicBlock bb1, ControlFlow::Node cfn) {
      exists(BasicBlock bb2, int i2 |
        varBlockReaches(def, bb1, bb2) and
        ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1 and
@@ -739,9 +666,7 @@ module Ssa {
     * or a write), `def` is read at `cfn`, and there is a path between them without
     * any read of `def`.
     */
-    private predicate adjacentVarRead(
-      TrackedDefinition def, BasicBlock bb1, int i1, ControlFlow::Node cfn
-    ) {
+    private predicate adjacentVarRead(Definition def, BasicBlock bb1, int i1, ControlFlow::Node cfn) {
      exists(int rankix, int i2 |
        rankix = ssaDefRank(def, _, bb1, i1) and
        rankix + 1 = ssaDefRank(def, _, bb1, i2) and
@@ -755,14 +680,13 @@ module Ssa {
    cached
    private module Cached {
      /**
-       * Holds if `cfn` is a last read of the non-trivial SSA definition `def`.
-       * That is, `cfn` can reach the end of the enclosing callable, or another
-       * SSA definition for the underlying source variable, without passing through
-       * another read.
+       * Holds if `cfn` is a last read of the SSA definition `def`. That is, `cfn`
+       * can reach the end of the enclosing callable, or another SSA definition for
+       * the underlying source variable, without passing through another read.
       */
      cached
-      predicate lastRead(TrackedDefinition def, ControlFlow::Node cfn) {
-        exists(BasicBlock bb1, int i1, int rnk, TrackedVar v |
+      predicate lastRead(Definition def, ControlFlow::Node cfn) {
+        exists(BasicBlock bb1, int i1, int rnk, SourceVariable v |
          variableRead(bb1, i1, v, cfn, _) and
          rnk = ssaDefRank(def, v, bb1, i1)
        |
@@ -788,9 +712,7 @@ module Ssa {
      }

      pragma[noinline]
-      private predicate ssaDefReachesEndOfBlockRec(
-        BasicBlock bb, TrackedDefinition def, TrackedVar v
-      ) {
+      private predicate ssaDefReachesEndOfBlockRec(BasicBlock bb, Definition def, SourceVariable v) {
        exists(BasicBlock idom | ssaDefReachesEndOfBlock(idom, def, v) |
          // The construction of SSA form ensures that each read of a variable is
          // dominated by its definition. An SSA definition therefore reaches a
@@ -803,12 +725,12 @@ module Ssa {
      }

      /**
-       * Holds if the non-trivial SSA definition of `v` at `def` reaches the end of a
-       * basic block `bb`, at which point it is still live, without crossing another
+       * Holds if the SSA definition of `v` at `def` reaches the end of a basic
+       * block `bb`, at which point it is still live, without crossing another
       * SSA definition of `v`.
       */
      cached
-      predicate ssaDefReachesEndOfBlock(BasicBlock bb, TrackedDefinition def, TrackedVar v) {
+      predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) {
        exists(int last | last = maxSsaRefRank(bb, v) |
          ssaDefReachesRank(bb, def, last, v) and
          liveAtExit(bb, v, _)
@@ -820,13 +742,12 @@ module Ssa {
      }

      /**
-       * Holds if the non-trivial SSA definition of `v` at `def` reaches `read` without
-       * crossing another SSA definition of `v`.
-       * The read at `node` is of kind `rk`.
+       * Holds if the SSA definition of `v` at `def` reaches `read` without crossing
+       * another SSA definition of `v`. The read at `node` is of kind `rk`.
       */
      cached
      predicate ssaDefReachesRead(
-        TrackedVar v, TrackedDefinition def, ControlFlow::Node read, ReadKind rk
+        SourceVariable v, Definition def, ControlFlow::Node read, ReadKind rk
      ) {
        ssaDefReachesReadWithinBlock(v, def, read, rk)
        or
@@ -838,12 +759,12 @@ module Ssa {
      }

      /**
-       * Holds if the non-trivial SSA definition of `v` at `def` reaches uncertain SSA
-       * definition `redef` without crossing another SSA definition of `v`.
+       * Holds if the SSA definition of `v` at `def` reaches uncertain SSA definition
+       * `redef` without crossing another SSA definition of `v`.
       */
      cached
      predicate ssaDefReachesUncertainDef(
-        TrackedVar v, TrackedDefinition def, UncertainDefinition redef
+        SourceVariable v, Definition def, UncertainDefinition redef
      ) {
        ssaDefReachesUncertainDefWithinBlock(v, def, redef)
        or
@@ -855,11 +776,11 @@ module Ssa {
      }

      /**
-       * Holds if the value defined at non-trivial SSA definition `def` can reach a
-       * read at `cfn`, without passing through any other read.
+       * Holds if the value defined at SSA definition `def` can reach a read at `cfn`,
+       * without passing through any other read.
       */
      cached
-      predicate firstReadSameVar(TrackedDefinition def, ControlFlow::Node cfn) {
+      predicate firstReadSameVar(Definition def, ControlFlow::Node cfn) {
        exists(BasicBlock bb1, int i1 |
          definesAt(def, bb1, i1, _) and
          adjacentVarRead(def, bb1, i1, cfn)
@@ -873,7 +794,7 @@ module Ssa {
       */
      cached
      predicate adjacentReadPairSameVar(
-        TrackedDefinition def, ControlFlow::Node cfn1, ControlFlow::Node cfn2
+        Definition def, ControlFlow::Node cfn1, ControlFlow::Node cfn2
      ) {
        exists(BasicBlock bb1, int i1 |
          variableRead(bb1, i1, _, cfn1, _) and
@@ -981,7 +902,7 @@ module Ssa {
      fpdef.getTarget() = fp and
      not init(fpdef) and
      fpdef.getEnclosingCallable() = c and
-      exists(TrackedFieldOrProp tf | tf.getAssignable() = fp)
+      exists(FieldOrPropSourceVariable tf | tf.getAssignable() = fp)
    }

    /**
@@ -1173,7 +1094,7 @@ module Ssa {
     * an update somewhere, and `fp` is likely to be live in `bb` at index
     * `i`.
     */
-    private predicate updateCandidate(BasicBlock bb, int i, TrackedFieldOrProp fp, Call call) {
+    private predicate updateCandidate(BasicBlock bb, int i, FieldOrPropSourceVariable fp, Call call) {
      possiblyLiveAtAllNodes(bb, fp) and
      callAt(bb, i, call) and
      relevantDefinition(_, fp.getAssignable(), _) and
@@ -1181,11 +1102,11 @@ module Ssa {
    }

    private predicate source(
-      Call call, TrackedFieldOrProp tfp, FieldOrProp fp, Callable c, boolean fresh
+      Call call, FieldOrPropSourceVariable fps, FieldOrProp fp, Callable c, boolean fresh
    ) {
-      updateCandidate(_, _, tfp, call) and
+      updateCandidate(_, _, fps, call) and
      c = getARuntimeTarget(call, _) and
-      fp = tfp.getAssignable() and
+      fp = fps.getAssignable() and
      if c instanceof Constructor then fresh = true else fresh = false
    }

@@ -1259,13 +1180,13 @@ module Ssa {
    }

    private predicate updatesNamedFieldOrPropPossiblyLive(
-      BasicBlock bb, int i, TrackedFieldOrProp fp, Call call, Callable setter
+      BasicBlock bb, int i, FieldOrPropSourceVariable fp, Call call, Callable setter
    ) {
      updateCandidate(bb, i, fp, call) and
      updatesNamedFieldOrProp_(fp, call, setter)
    }

-    private int firstRefAfterCall(BasicBlock bb, int i, TrackedFieldOrProp fp) {
+    private int firstRefAfterCall(BasicBlock bb, int i, FieldOrPropSourceVariable fp) {
      updatesNamedFieldOrPropPossiblyLive(bb, i, fp, _, _) and
      result = min(int k | k > i and ref(bb, k, fp, _))
    }
@@ -1275,7 +1196,7 @@ module Ssa {
     * update occurs in `setter`.
     */
    cached
-    predicate updatesNamedFieldOrProp(Call c, TrackedFieldOrProp fp, Callable setter) {
+    predicate updatesNamedFieldOrProp(Call c, FieldOrPropSourceVariable fp, Callable setter) {
      forceCachingInSameStage() and
      exists(BasicBlock bb, int i | updatesNamedFieldOrPropPossiblyLive(bb, i, fp, c, setter) |
        not exists(firstRefAfterCall(bb, i, fp)) and
@@ -1784,16 +1705,14 @@ module Ssa {
     *      properties, or captured variables).
     *   4. Implicit indirect definitions of variables through qualifier definitions
     *      (fields or properties).
-     *   5. Implicit definitions of variables prior to all reads, for variables that
-     *      are not amenable to SSA analysis (`UntrackedVar`).
-     *   6. Phi nodes.
+     *   5. Phi nodes.
     *
     * SSA definitions are only introduced where necessary. That is, dead assignments
     * have no associated SSA definitions.
     */
    cached
    newtype TDefinition =
-      TSsaExplicitDef(TrackedVar v, AssignableDefinition def, BasicBlock bb, int i) {
+      TSsaExplicitDef(SourceVariable v, AssignableDefinition def, BasicBlock bb, int i) {
        variableDefinition(bb, i, v, def) and
        (
          exists(ReadKind rk | liveAfterWrite(bb, i, v, rk) |
@@ -1814,7 +1733,7 @@ module Ssa {
          liveAfterWriteCaptured(bb, i, v)
        )
      } or
-      TSsaImplicitEntryDef(TrackedVar v, ControlFlow::BasicBlocks::EntryBlock ebb) {
+      TSsaImplicitEntryDef(SourceVariable v, ControlFlow::BasicBlocks::EntryBlock ebb) {
        liveAtEntry(ebb, v, _) and
        exists(Callable c |
          c = ebb.getCallable() and
@@ -1828,10 +1747,10 @@ module Ssa {
          )
          or
          // Each tracked field and property has an implicit entry definition
-          v instanceof TrackedFieldOrProp
+          v instanceof FieldOrPropSourceVariable
        )
      } or
-      TSsaImplicitCallDef(TrackedVar v, Call c, BasicBlock bb, int i) {
+      TSsaImplicitCallDef(SourceVariable v, Call c, BasicBlock bb, int i) {
        bb.getNode(i) = c.getAControlFlowNode() and
        (
          // Liveness of `v` after `c` is guaranteed by `updatesNamedFieldOrProp`
@@ -1841,7 +1760,7 @@ module Ssa {
          updatesCapturedVariable(c, v, _, _)
        )
      } or
-      TSsaImplicitQualifierDef(TrackedVar v, Definition qdef) {
+      TSsaImplicitQualifierDef(SourceVariable v, Definition qdef) {
        exists(BasicBlock bb, int i |
          qdef.getSourceVariable() = v.getQualifier() and
          qdef.definesAt(bb, i) and
@@ -1854,17 +1773,13 @@ module Ssa {
          not exists(TSsaImplicitCallDef(v, _, bb, i))
        )
      } or
-      TSsaImplicitUntrackedDef(UntrackedVar v, BasicBlock bb, int i) {
-        // Insert a definition prior to every read for untracked variables
-        bb.getNode(i + 1) = v.getAnAccess().(AssignableRead).getAControlFlowNode()
-      } or
-      TPhiNode(TrackedVar v, ControlFlow::BasicBlocks::JoinBlock bb) {
+      TPhiNode(SourceVariable v, ControlFlow::BasicBlocks::JoinBlock bb) {
        phiNodeMaybeLive(bb, v) and
        liveAtEntry(bb, v, _)
      }

    pragma[noinline]
-    private predicate phiNodeMaybeLive(ControlFlow::BasicBlocks::JoinBlock bb, TrackedVar v) {
+    private predicate phiNodeMaybeLive(ControlFlow::BasicBlocks::JoinBlock bb, SourceVariable v) {
      exists(Definition def, BasicBlock bb1 | definesAt(def, bb1, _, v) |
        bb1.inDominanceFrontier(bb)
      )
@@ -1886,8 +1801,6 @@ module Ssa {
      or
      exists(Definition qdef | def = TSsaImplicitQualifierDef(v, qdef) | definesAt(qdef, bb, i, _))
      or
-      def = TSsaImplicitUntrackedDef(v, bb, i)
-      or
      def = TPhiNode(v, bb) and i = -1
    }

@@ -2256,10 +2169,10 @@ module Ssa {
   * An SSA definition that corresponds to an explicit assignable definition.
   */
  class ExplicitDefinition extends Definition, TSsaExplicitDef {
-    TrackedVar tv;
+    SourceVariable sv;
    AssignableDefinition ad;

-    ExplicitDefinition() { this = TSsaExplicitDef(tv, ad, _, _) }
+    ExplicitDefinition() { this = TSsaExplicitDef(sv, ad, _, _) }

    /**
     * Gets an underlying assignable definition. The result is always unique,
@@ -2337,16 +2250,14 @@ module Ssa {
   * An SSA definition that does not correspond to an explicit variable definition.
   * Either an implicit initialization of a variable at the beginning of a callable
   * (`ImplicitEntryDefinition`), an implicit definition via a call
-   * (`ImplicitCallDefinition`), an implicit definition where the qualifier is
-   * updated (`ImplicitQualifierDefinition`), or a definition for a field or
-   * property that is not amenable to SSA analysis (`ImplicitUntrackedDefinition`).
+   * (`ImplicitCallDefinition`), or an implicit definition where the qualifier is
+   * updated (`ImplicitQualifierDefinition`).
   */
  class ImplicitDefinition extends Definition {
    ImplicitDefinition() {
      this = TSsaImplicitEntryDef(_, _) or
      this = TSsaImplicitCallDef(_, _, _, _) or
-      this = TSsaImplicitQualifierDef(_, _) or
-      this = TSsaImplicitUntrackedDef(_, _, _)
+      this = TSsaImplicitQualifierDef(_, _)
    }
  }

@@ -2420,25 +2331,6 @@ module Ssa {
    override Location getLocation() { result = getQualifierDefinition().getLocation() }
  }

-  /**
-   * An SSA definition for a variable that is not amenable to SSA analysis. A definition
-   * is inserted prior to every read.
-   */
-  class ImplicitUntrackedDefinition extends ImplicitDefinition, TSsaImplicitUntrackedDef {
-    override AssignableRead getARead() {
-      exists(BasicBlock bb, int i, UntrackedVar v |
-        this = TSsaImplicitUntrackedDef(v, bb, i) and
-        result.getAControlFlowNode() = bb.getNode(i + 1)
-      )
-    }
-
-    override string toString() {
-      result = getToStringPrefix(this) + "SSA untracked def(" + getSourceVariable() + ")"
-    }
-
-    override Location getLocation() { result = this.getARead().getLocation() }
-  }
-
  /**
   * An SSA definition that has no actual semantics, but simply serves to
   * merge or filter data flow.
@@ -2483,7 +2375,7 @@ module Ssa {
     *   call definition on line 9 as inputs.
     */
    override Definition getAnInput() {
-      exists(BasicBlock bb, BasicBlock phiPred, TrackedVar v |
+      exists(BasicBlock bb, BasicBlock phiPred, SourceVariable v |
        definesAt(this, bb, _, v) and
        bb.getAPredecessor() = phiPred and
        ssaDefReachesEndOfBlock(phiPred, result, v)
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll
@@ -1691,8 +1691,6 @@ private class FieldOrPropertyRead extends FieldOrPropertyAccess, AssignableRead
   * SSA updates.
   */
  predicate hasNonlocalValue() {
-    this = any(Ssa::ImplicitUntrackedDefinition udef).getARead()
-    or
    exists(Ssa::Definition def, Ssa::ImplicitDefinition idef |
      def.getARead() = this and
      idef = def.getAnUltimateDefinition()
--- a/csharp/ql/test/library-tests/csharp7/LocalTaintFlow.expected
+++ b/csharp/ql/test/library-tests/csharp7/LocalTaintFlow.expected
@@ -4,6 +4,7 @@
 | CSharp7.cs:10:9:10:9 | this access | CSharp7.cs:11:9:11:9 | this access |
 | CSharp7.cs:16:9:16:13 | [post] this access | CSharp7.cs:25:39:25:43 | this access |
 | CSharp7.cs:16:9:16:13 | this access | CSharp7.cs:25:39:25:43 | this access |
+| CSharp7.cs:17:9:17:11 | SSA entry def(this.field) | CSharp7.cs:17:18:17:22 | access to field field |
 | CSharp7.cs:17:9:17:11 | this | CSharp7.cs:17:18:17:22 | this access |
 | CSharp7.cs:21:9:21:11 | this | CSharp7.cs:21:16:21:20 | this access |
 | CSharp7.cs:22:9:22:11 | this | CSharp7.cs:22:16:22:20 | this access |
@@ -67,6 +68,7 @@
 | CSharp7.cs:84:23:84:23 | 2 | CSharp7.cs:84:16:84:24 | (..., ...) |
 | CSharp7.cs:87:10:87:18 | this | CSharp7.cs:92:18:92:28 | this access |
 | CSharp7.cs:89:13:89:34 | SSA def(t1) | CSharp7.cs:90:28:90:29 | access to local variable t1 |
+| CSharp7.cs:89:13:89:34 | SSA qualifier def(t1.Item1) | CSharp7.cs:92:20:92:27 | access to field Item1 |
 | CSharp7.cs:89:18:89:34 | (..., ...) | CSharp7.cs:89:13:89:34 | SSA def(t1) |
 | CSharp7.cs:89:19:89:27 | "tainted" | CSharp7.cs:89:18:89:34 | (..., ...) |
 | CSharp7.cs:89:30:89:33 | "X2" | CSharp7.cs:89:18:89:34 | (..., ...) |
@@ -100,6 +102,7 @@
 | CSharp7.cs:112:31:112:32 | access to local variable m2 | CSharp7.cs:112:26:112:33 | (..., ...) |
 | CSharp7.cs:114:9:114:67 | SSA def(m9) | CSharp7.cs:115:19:115:20 | access to local variable m9 |
 | CSharp7.cs:114:38:114:67 | SSA def(m2) | CSharp7.cs:118:9:118:10 | access to local variable m2 |
+| CSharp7.cs:114:38:114:67 | SSA qualifier def(m2.Item1) | CSharp7.cs:119:19:119:26 | access to field Item1 |
 | CSharp7.cs:114:49:114:67 | (..., ...) | CSharp7.cs:114:38:114:67 | ... = ... |
 | CSharp7.cs:114:50:114:58 | "DefUse2" | CSharp7.cs:114:49:114:67 | (..., ...) |
 | CSharp7.cs:114:61:114:66 | (..., ...) | CSharp7.cs:114:38:114:67 | SSA def(m2) |
--- a/csharp/ql/test/library-tests/dataflow/local/DataFlowStep.expected
+++ b/csharp/ql/test/library-tests/dataflow/local/DataFlowStep.expected
@@ -325,6 +325,8 @@
 | LocalDataFlow.cs:243:9:243:17 | access to local variable nonSink10 | LocalDataFlow.cs:244:15:244:23 | access to local variable nonSink10 |
 | LocalDataFlow.cs:247:13:247:52 | SSA def(taintedDataContract) | LocalDataFlow.cs:248:22:248:40 | access to local variable taintedDataContract |
 | LocalDataFlow.cs:247:13:247:52 | SSA qualifier def(taintedDataContract.AList) | LocalDataFlow.cs:250:22:250:46 | access to property AList |
+| LocalDataFlow.cs:247:13:247:52 | SSA qualifier def(taintedDataContract.AString) | LocalDataFlow.cs:248:22:248:48 | access to property AString |
+| LocalDataFlow.cs:247:13:247:52 | SSA qualifier def(taintedDataContract.AnInt) | LocalDataFlow.cs:257:20:257:44 | access to property AnInt |
 | LocalDataFlow.cs:247:35:247:52 | object creation of type DataContract | LocalDataFlow.cs:247:13:247:52 | SSA def(taintedDataContract) |
 | LocalDataFlow.cs:248:13:248:48 | SSA def(sink53) | LocalDataFlow.cs:249:15:249:20 | access to local variable sink53 |
 | LocalDataFlow.cs:248:22:248:40 | [post] access to local variable taintedDataContract | LocalDataFlow.cs:250:22:250:40 | access to local variable taintedDataContract |
@@ -337,6 +339,7 @@
 | LocalDataFlow.cs:250:22:250:46 | access to property AList | LocalDataFlow.cs:259:20:259:44 | access to property AList |
 | LocalDataFlow.cs:250:22:250:57 | access to property AString | LocalDataFlow.cs:250:13:250:57 | SSA def(sink54) |
 | LocalDataFlow.cs:254:13:254:55 | SSA def(nonTaintedDataContract) | LocalDataFlow.cs:255:20:255:41 | access to local variable nonTaintedDataContract |
+| LocalDataFlow.cs:254:13:254:55 | SSA qualifier def(nonTaintedDataContract.AString) | LocalDataFlow.cs:255:20:255:49 | access to property AString |
 | LocalDataFlow.cs:254:38:254:55 | object creation of type DataContract | LocalDataFlow.cs:254:13:254:55 | SSA def(nonTaintedDataContract) |
 | LocalDataFlow.cs:255:9:255:49 | SSA def(nonSink0) | LocalDataFlow.cs:256:15:256:22 | access to local variable nonSink0 |
 | LocalDataFlow.cs:255:20:255:49 | access to property AString | LocalDataFlow.cs:255:9:255:49 | SSA def(nonSink0) |
@@ -347,10 +350,12 @@
 | LocalDataFlow.cs:259:9:259:53 | SSA def(nonSink2) | LocalDataFlow.cs:260:15:260:22 | access to local variable nonSink2 |
 | LocalDataFlow.cs:259:20:259:53 | access to property AnInt | LocalDataFlow.cs:259:9:259:53 | SSA def(nonSink2) |
 | LocalDataFlow.cs:263:17:263:37 | SSA def(taintedTextBox) | LocalDataFlow.cs:264:22:264:35 | access to local variable taintedTextBox |
+| LocalDataFlow.cs:263:17:263:37 | SSA qualifier def(taintedTextBox.Text) | LocalDataFlow.cs:264:22:264:40 | access to property Text |
 | LocalDataFlow.cs:263:34:263:37 | null | LocalDataFlow.cs:263:17:263:37 | SSA def(taintedTextBox) |
 | LocalDataFlow.cs:264:13:264:40 | SSA def(sink60) | LocalDataFlow.cs:265:15:265:20 | access to local variable sink60 |
 | LocalDataFlow.cs:264:22:264:40 | access to property Text | LocalDataFlow.cs:264:13:264:40 | SSA def(sink60) |
 | LocalDataFlow.cs:268:17:268:40 | SSA def(nonTaintedTextBox) | LocalDataFlow.cs:269:20:269:36 | access to local variable nonTaintedTextBox |
+| LocalDataFlow.cs:268:17:268:40 | SSA qualifier def(nonTaintedTextBox.Text) | LocalDataFlow.cs:269:20:269:41 | access to property Text |
 | LocalDataFlow.cs:268:37:268:40 | null | LocalDataFlow.cs:268:17:268:40 | SSA def(nonTaintedTextBox) |
 | LocalDataFlow.cs:269:9:269:41 | SSA def(nonSink0) | LocalDataFlow.cs:270:15:270:22 | access to local variable nonSink0 |
 | LocalDataFlow.cs:269:20:269:41 | access to property Text | LocalDataFlow.cs:269:9:269:41 | SSA def(nonSink0) |
@@ -396,6 +401,7 @@
 | LocalDataFlow.cs:314:22:314:26 | access to local variable sink0 | LocalDataFlow.cs:314:22:314:38 | ... ?? ... |
 | LocalDataFlow.cs:314:22:314:38 | ... ?? ... | LocalDataFlow.cs:314:13:314:38 | SSA def(sink74) |
 | LocalDataFlow.cs:314:31:314:38 | access to local variable nonSink0 | LocalDataFlow.cs:314:22:314:38 | ... ?? ... |
+| LocalDataFlow.cs:334:28:334:30 | SSA entry def(this.anInt) | LocalDataFlow.cs:334:41:334:45 | access to field anInt |
 | LocalDataFlow.cs:334:28:334:30 | this | LocalDataFlow.cs:334:41:334:45 | this access |
 | LocalDataFlow.cs:334:50:334:52 | this | LocalDataFlow.cs:334:56:334:60 | this access |
 | LocalDataFlow.cs:334:50:334:52 | value | LocalDataFlow.cs:334:64:334:68 | access to parameter value |
--- a/csharp/ql/test/library-tests/dataflow/local/TaintTrackingStep.expected
+++ b/csharp/ql/test/library-tests/dataflow/local/TaintTrackingStep.expected
@@ -421,6 +421,8 @@
 | LocalDataFlow.cs:243:30:243:37 | access to local variable nonSink0 | LocalDataFlow.cs:243:9:243:38 | call to method AppendLine |
 | LocalDataFlow.cs:247:13:247:52 | SSA def(taintedDataContract) | LocalDataFlow.cs:248:22:248:40 | access to local variable taintedDataContract |
 | LocalDataFlow.cs:247:13:247:52 | SSA qualifier def(taintedDataContract.AList) | LocalDataFlow.cs:250:22:250:46 | access to property AList |
+| LocalDataFlow.cs:247:13:247:52 | SSA qualifier def(taintedDataContract.AString) | LocalDataFlow.cs:248:22:248:48 | access to property AString |
+| LocalDataFlow.cs:247:13:247:52 | SSA qualifier def(taintedDataContract.AnInt) | LocalDataFlow.cs:257:20:257:44 | access to property AnInt |
 | LocalDataFlow.cs:247:35:247:52 | object creation of type DataContract | LocalDataFlow.cs:247:13:247:52 | SSA def(taintedDataContract) |
 | LocalDataFlow.cs:248:13:248:48 | SSA def(sink53) | LocalDataFlow.cs:249:15:249:20 | access to local variable sink53 |
 | LocalDataFlow.cs:248:22:248:40 | [post] access to local variable taintedDataContract | LocalDataFlow.cs:250:22:250:40 | access to local variable taintedDataContract |
@@ -437,6 +439,7 @@
 | LocalDataFlow.cs:250:22:250:49 | access to indexer | LocalDataFlow.cs:250:22:250:57 | access to property AString |
 | LocalDataFlow.cs:250:22:250:57 | access to property AString | LocalDataFlow.cs:250:13:250:57 | SSA def(sink54) |
 | LocalDataFlow.cs:254:13:254:55 | SSA def(nonTaintedDataContract) | LocalDataFlow.cs:255:20:255:41 | access to local variable nonTaintedDataContract |
+| LocalDataFlow.cs:254:13:254:55 | SSA qualifier def(nonTaintedDataContract.AString) | LocalDataFlow.cs:255:20:255:49 | access to property AString |
 | LocalDataFlow.cs:254:38:254:55 | object creation of type DataContract | LocalDataFlow.cs:254:13:254:55 | SSA def(nonTaintedDataContract) |
 | LocalDataFlow.cs:255:9:255:49 | SSA def(nonSink0) | LocalDataFlow.cs:256:15:256:22 | access to local variable nonSink0 |
 | LocalDataFlow.cs:255:20:255:41 | access to local variable nonTaintedDataContract | LocalDataFlow.cs:255:20:255:49 | access to property AString |
@@ -450,11 +453,13 @@
 | LocalDataFlow.cs:259:20:259:44 | access to property AList | LocalDataFlow.cs:259:20:259:47 | access to indexer |
 | LocalDataFlow.cs:259:20:259:53 | access to property AnInt | LocalDataFlow.cs:259:9:259:53 | SSA def(nonSink2) |
 | LocalDataFlow.cs:263:17:263:37 | SSA def(taintedTextBox) | LocalDataFlow.cs:264:22:264:35 | access to local variable taintedTextBox |
+| LocalDataFlow.cs:263:17:263:37 | SSA qualifier def(taintedTextBox.Text) | LocalDataFlow.cs:264:22:264:40 | access to property Text |
 | LocalDataFlow.cs:263:34:263:37 | null | LocalDataFlow.cs:263:17:263:37 | SSA def(taintedTextBox) |
 | LocalDataFlow.cs:264:13:264:40 | SSA def(sink60) | LocalDataFlow.cs:265:15:265:20 | access to local variable sink60 |
 | LocalDataFlow.cs:264:22:264:35 | access to local variable taintedTextBox | LocalDataFlow.cs:264:22:264:40 | access to property Text |
 | LocalDataFlow.cs:264:22:264:40 | access to property Text | LocalDataFlow.cs:264:13:264:40 | SSA def(sink60) |
 | LocalDataFlow.cs:268:17:268:40 | SSA def(nonTaintedTextBox) | LocalDataFlow.cs:269:20:269:36 | access to local variable nonTaintedTextBox |
+| LocalDataFlow.cs:268:17:268:40 | SSA qualifier def(nonTaintedTextBox.Text) | LocalDataFlow.cs:269:20:269:41 | access to property Text |
 | LocalDataFlow.cs:268:37:268:40 | null | LocalDataFlow.cs:268:17:268:40 | SSA def(nonTaintedTextBox) |
 | LocalDataFlow.cs:269:9:269:41 | SSA def(nonSink0) | LocalDataFlow.cs:270:15:270:22 | access to local variable nonSink0 |
 | LocalDataFlow.cs:269:20:269:36 | access to local variable nonTaintedTextBox | LocalDataFlow.cs:269:20:269:41 | access to property Text |
@@ -505,6 +510,7 @@
 | LocalDataFlow.cs:314:22:314:26 | access to local variable sink0 | LocalDataFlow.cs:314:22:314:38 | ... ?? ... |
 | LocalDataFlow.cs:314:22:314:38 | ... ?? ... | LocalDataFlow.cs:314:13:314:38 | SSA def(sink74) |
 | LocalDataFlow.cs:314:31:314:38 | access to local variable nonSink0 | LocalDataFlow.cs:314:22:314:38 | ... ?? ... |
+| LocalDataFlow.cs:334:28:334:30 | SSA entry def(this.anInt) | LocalDataFlow.cs:334:41:334:45 | access to field anInt |
 | LocalDataFlow.cs:334:28:334:30 | this | LocalDataFlow.cs:334:41:334:45 | this access |
 | LocalDataFlow.cs:334:50:334:52 | this | LocalDataFlow.cs:334:56:334:60 | this access |
 | LocalDataFlow.cs:334:50:334:52 | value | LocalDataFlow.cs:334:64:334:68 | access to parameter value |
--- a/csharp/ql/test/library-tests/dataflow/ssa/SsaDef.expected
+++ b/csharp/ql/test/library-tests/dataflow/ssa/SsaDef.expected
@@ -193,11 +193,9 @@
 | Fields.cs:33:19:33:22 | Fields.stat | Fields.cs:49:17:49:28 | SSA call def(Fields.stat) |
 | Fields.cs:33:19:33:22 | Fields.stat | Fields.cs:50:9:50:17 | SSA phi(Fields.stat) |
 | Fields.cs:33:19:33:22 | Fields.stat | Fields.cs:51:9:51:20 | SSA call def(Fields.stat) |
-| Fields.cs:63:16:63:28 | this.VolatileField | Fields.cs:63:16:63:28 | SSA untracked def(this.VolatileField) |
-| Fields.cs:63:16:63:28 | this.VolatileField | Fields.cs:69:21:69:33 | SSA untracked def(this.VolatileField) |
 | Fields.cs:65:24:65:32 | this.LoopField | Fields.cs:61:17:61:17 | SSA entry def(this.LoopField) |
-| Fields.cs:71:17:71:35 | this.SingleAccessedField | Fields.cs:71:17:71:35 | SSA untracked def(this.SingleAccessedField) |
-| Fields.cs:76:20:76:38 | this.SingleAccessedField | Fields.cs:76:20:76:38 | SSA untracked def(this.SingleAccessedField) |
+| Fields.cs:71:17:71:35 | this.SingleAccessedField | Fields.cs:61:17:61:17 | SSA entry def(this.SingleAccessedField) |
+| Fields.cs:76:20:76:38 | this.SingleAccessedField | Fields.cs:74:17:74:17 | SSA entry def(this.SingleAccessedField) |
 | Fields.cs:77:13:77:13 | f | Fields.cs:77:13:77:45 | SSA def(f) |
 | Fields.cs:77:13:77:13 | f | Fields.cs:78:27:78:54 | SSA capture def(f) |
 | Fields.cs:78:23:78:23 | a | Fields.cs:78:23:78:54 | SSA def(a) |
@@ -283,8 +281,8 @@
 | Properties.cs:61:23:61:23 | i | Properties.cs:63:16:63:16 | SSA phi(i) |
 | Properties.cs:61:23:61:23 | i | Properties.cs:63:16:63:18 | SSA def(i) |
 | Properties.cs:65:24:65:31 | this.LoopProp | Properties.cs:61:17:61:17 | SSA entry def(this.LoopProp) |
-| Properties.cs:67:21:67:38 | this.SingleAccessedProp | Properties.cs:67:21:67:38 | SSA untracked def(this.SingleAccessedProp) |
-| Properties.cs:72:20:72:37 | this.SingleAccessedProp | Properties.cs:72:20:72:37 | SSA untracked def(this.SingleAccessedProp) |
+| Properties.cs:67:21:67:38 | this.SingleAccessedProp | Properties.cs:61:17:61:17 | SSA entry def(this.SingleAccessedProp) |
+| Properties.cs:72:20:72:37 | this.SingleAccessedProp | Properties.cs:70:17:70:17 | SSA entry def(this.SingleAccessedProp) |
 | Properties.cs:73:13:73:13 | f | Properties.cs:73:13:73:32 | SSA def(f) |
 | Properties.cs:73:13:73:13 | f | Properties.cs:74:27:74:54 | SSA capture def(f) |
 | Properties.cs:74:23:74:23 | a | Properties.cs:74:23:74:54 | SSA def(a) |
@@ -298,11 +296,6 @@
 | Properties.cs:76:9:76:12 | f.xs | Properties.cs:84:9:84:25 | SSA def(f.xs) |
 | Properties.cs:78:9:78:15 | this.xs | Properties.cs:81:9:81:22 | SSA def(this.xs) |
 | Properties.cs:78:9:78:15 | this.xs | Properties.cs:83:9:83:22 | SSA def(this.xs) |
-| Properties.cs:94:9:94:27 | this.NonTrivialProp | Properties.cs:95:20:95:38 | SSA untracked def(this.NonTrivialProp) |
-| Properties.cs:97:9:97:24 | this.VirtualProp | Properties.cs:98:16:98:31 | SSA untracked def(this.VirtualProp) |
-| Properties.cs:100:9:100:26 | this.VolatileField | Properties.cs:100:9:100:26 | SSA untracked def(this.VolatileField) |
-| Properties.cs:100:9:100:26 | this.VolatileField | Properties.cs:101:21:101:38 | SSA untracked def(this.VolatileField) |
-| Properties.cs:100:9:100:29 | this.VolatileField.xs | Properties.cs:101:21:101:41 | SSA untracked def(this.VolatileField.xs) |
 | Properties.cs:106:37:106:37 | p | Properties.cs:106:37:106:37 | SSA param(p) |
 | Properties.cs:114:20:114:29 | this.Props | Properties.cs:108:10:108:10 | SSA entry def(this.Props) |
 | Properties.cs:114:20:114:29 | this.Props | Properties.cs:113:9:113:22 | SSA call def(this.Props) |
--- a/csharp/ql/test/library-tests/dataflow/ssa/SsaDefElement.expected
+++ b/csharp/ql/test/library-tests/dataflow/ssa/SsaDefElement.expected
@@ -183,10 +183,8 @@
 | Fields.cs:49:17:49:28 | SSA call def(Fields.stat) | Fields.cs:49:17:49:28 | object creation of type Fields |
 | Fields.cs:51:9:51:20 | SSA call def(Fields.stat) | Fields.cs:51:9:51:20 | object creation of type Fields |
 | Fields.cs:61:17:61:17 | SSA entry def(this.LoopField) | Fields.cs:61:17:61:17 | H |
-| Fields.cs:63:16:63:28 | SSA untracked def(this.VolatileField) | Fields.cs:63:16:63:28 | this access |
-| Fields.cs:69:21:69:33 | SSA untracked def(this.VolatileField) | Fields.cs:69:21:69:33 | this access |
-| Fields.cs:71:17:71:35 | SSA untracked def(this.SingleAccessedField) | Fields.cs:71:17:71:35 | this access |
-| Fields.cs:76:20:76:38 | SSA untracked def(this.SingleAccessedField) | Fields.cs:76:20:76:38 | this access |
+| Fields.cs:61:17:61:17 | SSA entry def(this.SingleAccessedField) | Fields.cs:61:17:61:17 | H |
+| Fields.cs:74:17:74:17 | SSA entry def(this.SingleAccessedField) | Fields.cs:74:17:74:17 | I |
 | Fields.cs:77:13:77:45 | SSA def(f) | Fields.cs:77:13:77:45 | Fields f = ... |
 | Fields.cs:78:23:78:54 | SSA def(a) | Fields.cs:78:23:78:54 | Action a = ... |
 | Fields.cs:78:27:78:54 | SSA capture def(f) | Fields.cs:78:27:78:54 | (...) => ... |
@@ -264,10 +262,10 @@
 | Properties.cs:49:17:49:32 | SSA call def(Properties.stat) | Properties.cs:49:17:49:32 | object creation of type Properties |
 | Properties.cs:51:9:51:24 | SSA call def(Properties.stat) | Properties.cs:51:9:51:24 | object creation of type Properties |
 | Properties.cs:61:17:61:17 | SSA entry def(this.LoopProp) | Properties.cs:61:17:61:17 | H |
+| Properties.cs:61:17:61:17 | SSA entry def(this.SingleAccessedProp) | Properties.cs:61:17:61:17 | H |
 | Properties.cs:61:23:61:23 | SSA param(i) | Properties.cs:61:23:61:23 | i |
 | Properties.cs:63:16:63:18 | SSA def(i) | Properties.cs:63:16:63:18 | ...-- |
-| Properties.cs:67:21:67:38 | SSA untracked def(this.SingleAccessedProp) | Properties.cs:67:21:67:38 | this access |
-| Properties.cs:72:20:72:37 | SSA untracked def(this.SingleAccessedProp) | Properties.cs:72:20:72:37 | this access |
+| Properties.cs:70:17:70:17 | SSA entry def(this.SingleAccessedProp) | Properties.cs:70:17:70:17 | I |
 | Properties.cs:73:13:73:32 | SSA def(f) | Properties.cs:73:13:73:32 | Properties f = ... |
 | Properties.cs:74:23:74:54 | SSA def(a) | Properties.cs:74:23:74:54 | Action a = ... |
 | Properties.cs:74:27:74:54 | SSA capture def(f) | Properties.cs:74:27:74:54 | (...) => ... |
@@ -281,11 +279,6 @@
 | Properties.cs:83:9:83:22 | SSA def(this.xs) | Properties.cs:83:9:83:22 | ... = ... |
 | Properties.cs:84:9:84:25 | SSA def(f.xs) | Properties.cs:84:9:84:25 | ... = ... |
 | Properties.cs:85:24:85:46 | SSA capture def(b) | Properties.cs:85:24:85:46 | (...) => ... |
-| Properties.cs:95:20:95:38 | SSA untracked def(this.NonTrivialProp) | Properties.cs:95:20:95:23 | this access |
-| Properties.cs:98:16:98:31 | SSA untracked def(this.VirtualProp) | Properties.cs:98:16:98:19 | this access |
-| Properties.cs:100:9:100:26 | SSA untracked def(this.VolatileField) | Properties.cs:100:9:100:12 | this access |
-| Properties.cs:101:21:101:38 | SSA untracked def(this.VolatileField) | Properties.cs:101:21:101:24 | this access |
-| Properties.cs:101:21:101:41 | SSA untracked def(this.VolatileField.xs) | Properties.cs:101:21:101:38 | access to field VolatileField |
 | Properties.cs:106:37:106:37 | SSA param(p) | Properties.cs:106:37:106:37 | p |
 | Properties.cs:108:10:108:10 | SSA entry def(this.Props) | Properties.cs:108:10:108:10 | K |
 | Properties.cs:108:10:108:10 | SSA entry def(this.Props.Props) | Properties.cs:108:10:108:10 | K |
--- a/csharp/ql/test/library-tests/dataflow/ssa/SsaDefLastRead.expected
+++ b/csharp/ql/test/library-tests/dataflow/ssa/SsaDefLastRead.expected
@@ -151,6 +151,8 @@
 | Fields.cs:33:19:33:22 | Fields.stat | Fields.cs:38:9:38:13 | SSA call def(Fields.stat) | Fields.cs:41:13:41:16 | access to field stat |
 | Fields.cs:33:19:33:22 | Fields.stat | Fields.cs:51:9:51:20 | SSA call def(Fields.stat) | Fields.cs:54:13:54:16 | access to field stat |
 | Fields.cs:65:24:65:32 | this.LoopField | Fields.cs:61:17:61:17 | SSA entry def(this.LoopField) | Fields.cs:65:24:65:32 | access to field LoopField |
+| Fields.cs:71:17:71:35 | this.SingleAccessedField | Fields.cs:61:17:61:17 | SSA entry def(this.SingleAccessedField) | Fields.cs:71:17:71:35 | access to field SingleAccessedField |
+| Fields.cs:76:20:76:38 | this.SingleAccessedField | Fields.cs:74:17:74:17 | SSA entry def(this.SingleAccessedField) | Fields.cs:76:20:76:38 | access to field SingleAccessedField |
 | Fields.cs:77:13:77:13 | f | Fields.cs:77:13:77:45 | SSA def(f) | Fields.cs:90:19:90:19 | access to local variable f |
 | Fields.cs:77:13:77:13 | f | Fields.cs:78:27:78:54 | SSA capture def(f) | Fields.cs:78:35:78:35 | access to local variable f |
 | Fields.cs:78:23:78:23 | a | Fields.cs:78:23:78:54 | SSA def(a) | Fields.cs:81:9:81:9 | access to local variable a |
@@ -219,6 +221,8 @@
 | Properties.cs:33:19:33:22 | Properties.stat | Properties.cs:51:9:51:24 | SSA call def(Properties.stat) | Properties.cs:54:13:54:16 | access to property stat |
 | Properties.cs:61:23:61:23 | i | Properties.cs:63:16:63:16 | SSA phi(i) | Properties.cs:63:16:63:16 | access to parameter i |
 | Properties.cs:65:24:65:31 | this.LoopProp | Properties.cs:61:17:61:17 | SSA entry def(this.LoopProp) | Properties.cs:65:24:65:31 | access to property LoopProp |
+| Properties.cs:67:21:67:38 | this.SingleAccessedProp | Properties.cs:61:17:61:17 | SSA entry def(this.SingleAccessedProp) | Properties.cs:67:21:67:38 | access to property SingleAccessedProp |
+| Properties.cs:72:20:72:37 | this.SingleAccessedProp | Properties.cs:70:17:70:17 | SSA entry def(this.SingleAccessedProp) | Properties.cs:72:20:72:37 | access to property SingleAccessedProp |
 | Properties.cs:73:13:73:13 | f | Properties.cs:73:13:73:32 | SSA def(f) | Properties.cs:86:19:86:19 | access to local variable f |
 | Properties.cs:73:13:73:13 | f | Properties.cs:74:27:74:54 | SSA capture def(f) | Properties.cs:74:35:74:35 | access to local variable f |
 | Properties.cs:74:23:74:23 | a | Properties.cs:74:23:74:54 | SSA def(a) | Properties.cs:77:9:77:9 | access to local variable a |
--- a/csharp/ql/test/library-tests/dataflow/ssa/SsaRead.expected
+++ b/csharp/ql/test/library-tests/dataflow/ssa/SsaRead.expected
@@ -185,11 +185,9 @@
 | Fields.cs:33:19:33:22 | Fields.stat | Fields.cs:34:9:34:16 | SSA call def(Fields.stat) | Fields.cs:37:13:37:16 | access to field stat |
 | Fields.cs:33:19:33:22 | Fields.stat | Fields.cs:38:9:38:13 | SSA call def(Fields.stat) | Fields.cs:41:13:41:16 | access to field stat |
 | Fields.cs:33:19:33:22 | Fields.stat | Fields.cs:51:9:51:20 | SSA call def(Fields.stat) | Fields.cs:54:13:54:16 | access to field stat |
-| Fields.cs:63:16:63:28 | this.VolatileField | Fields.cs:63:16:63:28 | SSA untracked def(this.VolatileField) | Fields.cs:63:16:63:28 | access to field VolatileField |
-| Fields.cs:63:16:63:28 | this.VolatileField | Fields.cs:69:21:69:33 | SSA untracked def(this.VolatileField) | Fields.cs:69:21:69:33 | access to field VolatileField |
 | Fields.cs:65:24:65:32 | this.LoopField | Fields.cs:61:17:61:17 | SSA entry def(this.LoopField) | Fields.cs:65:24:65:32 | access to field LoopField |
-| Fields.cs:71:17:71:35 | this.SingleAccessedField | Fields.cs:71:17:71:35 | SSA untracked def(this.SingleAccessedField) | Fields.cs:71:17:71:35 | access to field SingleAccessedField |
-| Fields.cs:76:20:76:38 | this.SingleAccessedField | Fields.cs:76:20:76:38 | SSA untracked def(this.SingleAccessedField) | Fields.cs:76:20:76:38 | access to field SingleAccessedField |
+| Fields.cs:71:17:71:35 | this.SingleAccessedField | Fields.cs:61:17:61:17 | SSA entry def(this.SingleAccessedField) | Fields.cs:71:17:71:35 | access to field SingleAccessedField |
+| Fields.cs:76:20:76:38 | this.SingleAccessedField | Fields.cs:74:17:74:17 | SSA entry def(this.SingleAccessedField) | Fields.cs:76:20:76:38 | access to field SingleAccessedField |
 | Fields.cs:77:13:77:13 | f | Fields.cs:77:13:77:45 | SSA def(f) | Fields.cs:80:9:80:9 | access to local variable f |
 | Fields.cs:77:13:77:13 | f | Fields.cs:77:13:77:45 | SSA def(f) | Fields.cs:82:19:82:19 | access to local variable f |
 | Fields.cs:77:13:77:13 | f | Fields.cs:77:13:77:45 | SSA def(f) | Fields.cs:83:9:83:9 | access to local variable f |
@@ -302,8 +300,8 @@
 | Properties.cs:33:19:33:22 | Properties.stat | Properties.cs:51:9:51:24 | SSA call def(Properties.stat) | Properties.cs:54:13:54:16 | access to property stat |
 | Properties.cs:61:23:61:23 | i | Properties.cs:63:16:63:16 | SSA phi(i) | Properties.cs:63:16:63:16 | access to parameter i |
 | Properties.cs:65:24:65:31 | this.LoopProp | Properties.cs:61:17:61:17 | SSA entry def(this.LoopProp) | Properties.cs:65:24:65:31 | access to property LoopProp |
-| Properties.cs:67:21:67:38 | this.SingleAccessedProp | Properties.cs:67:21:67:38 | SSA untracked def(this.SingleAccessedProp) | Properties.cs:67:21:67:38 | access to property SingleAccessedProp |
-| Properties.cs:72:20:72:37 | this.SingleAccessedProp | Properties.cs:72:20:72:37 | SSA untracked def(this.SingleAccessedProp) | Properties.cs:72:20:72:37 | access to property SingleAccessedProp |
+| Properties.cs:67:21:67:38 | this.SingleAccessedProp | Properties.cs:61:17:61:17 | SSA entry def(this.SingleAccessedProp) | Properties.cs:67:21:67:38 | access to property SingleAccessedProp |
+| Properties.cs:72:20:72:37 | this.SingleAccessedProp | Properties.cs:70:17:70:17 | SSA entry def(this.SingleAccessedProp) | Properties.cs:72:20:72:37 | access to property SingleAccessedProp |
 | Properties.cs:73:13:73:13 | f | Properties.cs:73:13:73:32 | SSA def(f) | Properties.cs:76:9:76:9 | access to local variable f |
 | Properties.cs:73:13:73:13 | f | Properties.cs:73:13:73:32 | SSA def(f) | Properties.cs:78:19:78:19 | access to local variable f |
 | Properties.cs:73:13:73:13 | f | Properties.cs:73:13:73:32 | SSA def(f) | Properties.cs:79:9:79:9 | access to local variable f |
@@ -322,11 +320,6 @@
 | Properties.cs:76:9:76:12 | f.xs | Properties.cs:84:9:84:25 | SSA def(f.xs) | Properties.cs:86:19:86:22 | access to property xs |
 | Properties.cs:78:9:78:15 | this.xs | Properties.cs:81:9:81:22 | SSA def(this.xs) | Properties.cs:82:9:82:15 | access to property xs |
 | Properties.cs:78:9:78:15 | this.xs | Properties.cs:83:9:83:22 | SSA def(this.xs) | Properties.cs:85:9:85:15 | access to property xs |
-| Properties.cs:94:9:94:27 | this.NonTrivialProp | Properties.cs:95:20:95:38 | SSA untracked def(this.NonTrivialProp) | Properties.cs:95:20:95:38 | access to property NonTrivialProp |
-| Properties.cs:97:9:97:24 | this.VirtualProp | Properties.cs:98:16:98:31 | SSA untracked def(this.VirtualProp) | Properties.cs:98:16:98:31 | access to property VirtualProp |
-| Properties.cs:100:9:100:26 | this.VolatileField | Properties.cs:100:9:100:26 | SSA untracked def(this.VolatileField) | Properties.cs:100:9:100:26 | access to field VolatileField |
-| Properties.cs:100:9:100:26 | this.VolatileField | Properties.cs:101:21:101:38 | SSA untracked def(this.VolatileField) | Properties.cs:101:21:101:38 | access to field VolatileField |
-| Properties.cs:100:9:100:29 | this.VolatileField.xs | Properties.cs:101:21:101:41 | SSA untracked def(this.VolatileField.xs) | Properties.cs:101:21:101:41 | access to property xs |
 | Properties.cs:106:37:106:37 | p | Properties.cs:106:37:106:37 | SSA param(p) | Properties.cs:106:42:106:42 | access to parameter p |
 | Properties.cs:114:20:114:29 | this.Props | Properties.cs:113:9:113:22 | SSA call def(this.Props) | Properties.cs:114:20:114:29 | access to field Props |
 | Properties.cs:114:20:114:29 | this.Props | Properties.cs:113:9:113:22 | SSA call def(this.Props) | Properties.cs:115:21:115:30 | access to field Props |
--- a/csharp/ql/test/library-tests/dataflow/ssa/SsaUltimateDef.expected
+++ b/csharp/ql/test/library-tests/dataflow/ssa/SsaUltimateDef.expected
@@ -247,11 +247,9 @@
 | Fields.cs:33:19:33:22 | Fields.stat | Fields.cs:51:9:51:20 | SSA call def(Fields.stat) | Fields.cs:38:9:38:13 | SSA call def(Fields.stat) |
 | Fields.cs:33:19:33:22 | Fields.stat | Fields.cs:51:9:51:20 | SSA call def(Fields.stat) | Fields.cs:49:17:49:28 | SSA call def(Fields.stat) |
 | Fields.cs:33:19:33:22 | Fields.stat | Fields.cs:51:9:51:20 | SSA call def(Fields.stat) | Fields.cs:51:9:51:20 | SSA call def(Fields.stat) |
-| Fields.cs:63:16:63:28 | this.VolatileField | Fields.cs:63:16:63:28 | SSA untracked def(this.VolatileField) | Fields.cs:63:16:63:28 | SSA untracked def(this.VolatileField) |
-| Fields.cs:63:16:63:28 | this.VolatileField | Fields.cs:69:21:69:33 | SSA untracked def(this.VolatileField) | Fields.cs:69:21:69:33 | SSA untracked def(this.VolatileField) |
 | Fields.cs:65:24:65:32 | this.LoopField | Fields.cs:61:17:61:17 | SSA entry def(this.LoopField) | Fields.cs:61:17:61:17 | SSA entry def(this.LoopField) |
-| Fields.cs:71:17:71:35 | this.SingleAccessedField | Fields.cs:71:17:71:35 | SSA untracked def(this.SingleAccessedField) | Fields.cs:71:17:71:35 | SSA untracked def(this.SingleAccessedField) |
-| Fields.cs:76:20:76:38 | this.SingleAccessedField | Fields.cs:76:20:76:38 | SSA untracked def(this.SingleAccessedField) | Fields.cs:76:20:76:38 | SSA untracked def(this.SingleAccessedField) |
+| Fields.cs:71:17:71:35 | this.SingleAccessedField | Fields.cs:61:17:61:17 | SSA entry def(this.SingleAccessedField) | Fields.cs:61:17:61:17 | SSA entry def(this.SingleAccessedField) |
+| Fields.cs:76:20:76:38 | this.SingleAccessedField | Fields.cs:74:17:74:17 | SSA entry def(this.SingleAccessedField) | Fields.cs:74:17:74:17 | SSA entry def(this.SingleAccessedField) |
 | Fields.cs:77:13:77:13 | f | Fields.cs:77:13:77:45 | SSA def(f) | Fields.cs:77:13:77:45 | SSA def(f) |
 | Fields.cs:77:13:77:13 | f | Fields.cs:78:27:78:54 | SSA capture def(f) | Fields.cs:78:27:78:54 | SSA capture def(f) |
 | Fields.cs:78:23:78:23 | a | Fields.cs:78:23:78:54 | SSA def(a) | Fields.cs:78:23:78:54 | SSA def(a) |
@@ -377,8 +375,8 @@
 | Properties.cs:61:23:61:23 | i | Properties.cs:63:16:63:16 | SSA phi(i) | Properties.cs:63:16:63:18 | SSA def(i) |
 | Properties.cs:61:23:61:23 | i | Properties.cs:63:16:63:18 | SSA def(i) | Properties.cs:63:16:63:18 | SSA def(i) |
 | Properties.cs:65:24:65:31 | this.LoopProp | Properties.cs:61:17:61:17 | SSA entry def(this.LoopProp) | Properties.cs:61:17:61:17 | SSA entry def(this.LoopProp) |
-| Properties.cs:67:21:67:38 | this.SingleAccessedProp | Properties.cs:67:21:67:38 | SSA untracked def(this.SingleAccessedProp) | Properties.cs:67:21:67:38 | SSA untracked def(this.SingleAccessedProp) |
-| Properties.cs:72:20:72:37 | this.SingleAccessedProp | Properties.cs:72:20:72:37 | SSA untracked def(this.SingleAccessedProp) | Properties.cs:72:20:72:37 | SSA untracked def(this.SingleAccessedProp) |
+| Properties.cs:67:21:67:38 | this.SingleAccessedProp | Properties.cs:61:17:61:17 | SSA entry def(this.SingleAccessedProp) | Properties.cs:61:17:61:17 | SSA entry def(this.SingleAccessedProp) |
+| Properties.cs:72:20:72:37 | this.SingleAccessedProp | Properties.cs:70:17:70:17 | SSA entry def(this.SingleAccessedProp) | Properties.cs:70:17:70:17 | SSA entry def(this.SingleAccessedProp) |
 | Properties.cs:73:13:73:13 | f | Properties.cs:73:13:73:32 | SSA def(f) | Properties.cs:73:13:73:32 | SSA def(f) |
 | Properties.cs:73:13:73:13 | f | Properties.cs:74:27:74:54 | SSA capture def(f) | Properties.cs:74:27:74:54 | SSA capture def(f) |
 | Properties.cs:74:23:74:23 | a | Properties.cs:74:23:74:54 | SSA def(a) | Properties.cs:74:23:74:54 | SSA def(a) |
@@ -394,11 +392,6 @@
 | Properties.cs:76:9:76:12 | f.xs | Properties.cs:84:9:84:25 | SSA def(f.xs) | Properties.cs:84:9:84:25 | SSA def(f.xs) |
 | Properties.cs:78:9:78:15 | this.xs | Properties.cs:81:9:81:22 | SSA def(this.xs) | Properties.cs:81:9:81:22 | SSA def(this.xs) |
 | Properties.cs:78:9:78:15 | this.xs | Properties.cs:83:9:83:22 | SSA def(this.xs) | Properties.cs:83:9:83:22 | SSA def(this.xs) |
-| Properties.cs:94:9:94:27 | this.NonTrivialProp | Properties.cs:95:20:95:38 | SSA untracked def(this.NonTrivialProp) | Properties.cs:95:20:95:38 | SSA untracked def(this.NonTrivialProp) |
-| Properties.cs:97:9:97:24 | this.VirtualProp | Properties.cs:98:16:98:31 | SSA untracked def(this.VirtualProp) | Properties.cs:98:16:98:31 | SSA untracked def(this.VirtualProp) |
-| Properties.cs:100:9:100:26 | this.VolatileField | Properties.cs:100:9:100:26 | SSA untracked def(this.VolatileField) | Properties.cs:100:9:100:26 | SSA untracked def(this.VolatileField) |
-| Properties.cs:100:9:100:26 | this.VolatileField | Properties.cs:101:21:101:38 | SSA untracked def(this.VolatileField) | Properties.cs:101:21:101:38 | SSA untracked def(this.VolatileField) |
-| Properties.cs:100:9:100:29 | this.VolatileField.xs | Properties.cs:101:21:101:41 | SSA untracked def(this.VolatileField.xs) | Properties.cs:101:21:101:41 | SSA untracked def(this.VolatileField.xs) |
 | Properties.cs:106:37:106:37 | p | Properties.cs:106:37:106:37 | SSA param(p) | Properties.cs:106:37:106:37 | SSA param(p) |
 | Properties.cs:114:20:114:29 | this.Props | Properties.cs:108:10:108:10 | SSA entry def(this.Props) | Properties.cs:108:10:108:10 | SSA entry def(this.Props) |
 | Properties.cs:114:20:114:29 | this.Props | Properties.cs:113:9:113:22 | SSA call def(this.Props) | Properties.cs:108:10:108:10 | SSA entry def(this.Props) |