github · aschackmull · May 4, 2026 · Apr 17, 2026 · Apr 17, 2026 · Apr 23, 2026
@@ -500,10 +500,8 @@ class AssignableDefinition extends TAssignableDefinition {
    */
   pragma[nomagic]
   AssignableRead getAFirstRead() {
-    exists(ControlFlowNode cfn | cfn = result.getControlFlowNode() |
-      exists(Ssa::ExplicitDefinition def | result = def.getAFirstReadAtNode(cfn) |
-        this = def.getADefinition()
-      )
+    exists(Ssa::ExplicitDefinition def | result = Ssa::ssaGetAFirstUse(def) |
+      this = def.getADefinition()
     )
   }
 

@@ -26,17 +26,7 @@ private module ControlFlowInput implements InputSig<Location, ControlFlowNode, B
 
   class Expr = CS::Expr;
 
-  class SourceVariable = Ssa::SourceVariable;
-
-  class SsaDefinition = Ssa::Definition;
-
-  class SsaExplicitWrite extends SsaDefinition instanceof Ssa::ExplicitDefinition {
-    Expr getValue() { result = super.getADefinition().getSource() }
-  }
-
-  class SsaPhiDefinition = Ssa::PhiNode;
-
-  class SsaUncertainWrite = Ssa::UncertainDefinition;
+  import Ssa
 
   class GuardValue = Guards::GuardValue;
 

@@ -191,23 +191,7 @@ private module GuardsImpl = SharedGuards::Make<Location, Cfg, GuardsInput>;
 class GuardValue = GuardsImpl::GuardValue;
 
 private module LogicInput implements GuardsImpl::LogicInputSig {
-  class SsaDefinition extends Ssa::Definition {
-    Expr getARead() { super.getARead() = result }
-  }
-
-  class SsaExplicitWrite extends SsaDefinition instanceof Ssa::ExplicitDefinition {
-    Expr getValue() { result = super.getADefinition().getSource() }
-  }
-
-  class SsaPhiDefinition extends SsaDefinition instanceof Ssa::PhiNode {
-    predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb) {
-      super.hasInputFromBlock(inp, bb)
-    }
-  }
-
-  class SsaParameterInit extends SsaDefinition instanceof Ssa::ParameterDefinition {
-    Parameter getParameter() { result = super.getParameter() }
-  }
+  import Ssa
 
   predicate additionalNullCheck(GuardsImpl::PreGuard guard, GuardValue val, Expr e, boolean isNull) {
     // Comparison with a non-`null` value, for example `x?.Length > 0`

@@ -241,7 +241,7 @@ private Ssa::Definition getAnUltimateDefinition(Ssa::Definition def) {
  * exception.
  */
 private predicate defReaches(Ssa::Definition def, ControlFlowNode cfn) {
-  exists(def.getAFirstReadAtNode(cfn))
+  Ssa::ssaGetAFirstUse(def).getControlFlowNode() = cfn
   or
   exists(ControlFlowNode mid | defReaches(def, mid) |
     SsaImpl::adjacentReadPairSameVar(_, mid, cfn) and
@@ -250,9 +250,9 @@ private predicate defReaches(Ssa::Definition def, ControlFlowNode cfn) {
 }
 
 private module NullnessConfig implements ControlFlowReachability::ConfigSig {
-  predicate source(ControlFlowNode node, Ssa::Definition def) { defMaybeNull(def, node, _, _) }
+  predicate source(ControlFlowNode node, SsaDefinition def) { defMaybeNull(def, node, _, _) }
 
-  predicate sink(ControlFlowNode node, Ssa::Definition def) {
+  predicate sink(ControlFlowNode node, SsaDefinition def) {
     exists(Dereference d |
       dereferenceAt(node, def, d) and
       not d instanceof NonNullExpr

@@ -3,12 +3,14 @@
  */
 
 import csharp
+private import internal.SsaImpl as SsaImpl
+import SsaImpl::Ssa_
 
 /**
  * Provides classes for working with static single assignment (SSA) form.
  */
 module Ssa {
-  private import internal.SsaImpl as SsaImpl
+  import SsaImpl::Ssa_
 
   pragma[nomagic]
   private predicate assignableDefinitionLocalScopeVariable(
@@ -147,6 +149,47 @@ module Ssa {
     }
   }
 
+  /**
+   * Gets a read of the source variable underlying the SSA definition `def`
+   * that can be reached from `def` without passing through any
+   * other SSA definition or read. Example:
+   *
+   * ```csharp
+   * int Field;
+   *
+   * void SetField(int i) {
+   *   this.Field = i;
+   *   Use(this.Field);
+   *   if (i > 0)
+   *     this.Field = i - 1;
+   *   else if (i < 0)
+   *     SetField(1);
+   *   Use(this.Field);
+   *   Use(this.Field);
+   * }
+   * ```
+   *
+   * - The read of `i` on line 4 can be reached from the explicit SSA
+   *   definition (wrapping an implicit entry definition) on line 3.
+   * - The reads of `i` on lines 6 and 7 are not the first reads of any SSA
+   *   definition.
+   * - The read of `this.Field` on line 5 can be reached from the explicit SSA
+   *   definition on line 4.
+   * - The read of `this.Field` on line 10 can be reached from the phi node
+   *   between lines 9 and 10.
+   * - The read of `this.Field` on line 11 is not the first read of any SSA
+   *   definition.
+   *
+   * Subsequent reads can be found by following the steps defined by
+   * `AssignableRead.getANextRead()`.
+   */
+  AssignableRead ssaGetAFirstUse(SsaDefinition def) {
+    exists(ControlFlowNode cfn |
+      SsaImpl::firstReadSameVar(def, cfn) and
+      result.getControlFlowNode() = cfn
+    )
+  }
+
   /**
    * A static single assignment (SSA) definition. Either an explicit variable
    * definition (`ExplicitDefinition`), an implicit variable definition
@@ -227,6 +270,8 @@ module Ssa {
     }
 
     /**
+     * DEPRECATED: Use `ssaGetAFirstUse` instead.
+     *
      * Gets a read of the source variable underlying this SSA definition that
      * can be reached from this SSA definition without passing through any
      * other SSA definition or read. Example:
@@ -260,9 +305,11 @@ module Ssa {
      * Subsequent reads can be found by following the steps defined by
      * `AssignableRead.getANextRead()`.
      */
-    final AssignableRead getAFirstRead() { result = this.getAFirstReadAtNode(_) }
+    deprecated final AssignableRead getAFirstRead() { result = this.getAFirstReadAtNode(_) }
 
     /**
+     * DEPRECATED: Use `ssaGetAFirstUse` instead.
+     *
      * Gets a read of the source variable underlying this SSA definition at
      * control flow node `cfn` that can be reached from this SSA definition
      * without passing through any other SSA definition or read. Example:
@@ -296,7 +343,7 @@ module Ssa {
      * Subsequent reads can be found by following the steps defined by
      * `AssignableRead.getANextRead()`.
      */
-    final AssignableRead getAFirstReadAtNode(ControlFlowNode cfn) {
+    deprecated final AssignableRead getAFirstReadAtNode(ControlFlowNode cfn) {
       SsaImpl::firstReadSameVar(this, cfn) and
       result.getControlFlowNode() = cfn
     }

@@ -1,9 +1,20 @@
-import csharp
+private import csharp as CS
 
 /**
  * Provides a simple SSA implementation for local scope variables.
  */
 module BaseSsa {
+  private import BaseSsaImpl
+
+  class SimpleLocalScopeVariable = BaseSsaImpl::SimpleLocalScopeVariable;
+
+  module Ssa = SsaImpl::MakeSsa<SsaInput>;
+
+  import Ssa
+}
+
+private module BaseSsaImpl {
+  private import CS
   private import AssignableDefinitions
   private import codeql.ssa.Ssa as SsaImplCommon
 
@@ -13,7 +24,7 @@ module BaseSsa {
     predicate ref() { any() }
 
     cached
-    predicate backref() { (exists(any(SsaDefinition def).getARead()) implies any()) }
+    predicate backref() { (exists(any(BaseSsa::SsaDefinition def).getARead()) implies any()) }
   }
 
   /**
@@ -112,11 +123,9 @@ module BaseSsa {
     }
   }
 
-  private module SsaImpl = SsaImplCommon::Make<Location, Cfg, SsaImplInput>;
-
-  private module SsaInput implements SsaImpl::SsaInputSig {
-    private import csharp as CS
+  module SsaImpl = SsaImplCommon::Make<Location, Cfg, SsaImplInput>;
 
+  module SsaInput implements SsaImpl::SsaInputSig {
     class Expr = CS::Expr;
 
     class Parameter = CS::Parameter;
@@ -139,8 +148,4 @@ module BaseSsa {
       w.isParameterInit(v)
     }
   }
-
-  module Ssa = SsaImpl::MakeSsa<SsaInput>;
-
-  import Ssa
 }
@@ -9,7 +9,7 @@ private import semmle.code.csharp.controlflow.Guards as Guards
 private import semmle.code.csharp.dataflow.internal.BaseSSA
 private import semmle.code.csharp.internal.Location
 
-private module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock> {
+private module SsaImplInput implements SsaImplCommon::InputSig<Location, BasicBlock> {
   class SourceVariable = Ssa::SourceVariable;
 
   /**
@@ -41,7 +41,40 @@ private module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock>
   }
 }
 
-import SsaImplCommon::Make<Location, Cfg, SsaInput> as Impl
+import SsaImplCommon::Make<Location, Cfg, SsaImplInput> as Impl
+
+private module SsaInput implements Impl::SsaInputSig {
+  private import csharp as CS
+
+  class Expr = CS::Expr;
+
+  class Parameter = CS::Parameter;
+
+  class VariableWrite extends AssignableDefinition {
+    Expr asExpr() { result = this.getExpr() }
+
+    Expr getValue() { result = this.getSource() }
+
+    predicate isParameterInit(Parameter p) { this.(ImplicitParameterDefinition).getParameter() = p }
+  }
+
+  predicate explicitWrite(VariableWrite w, BasicBlock bb, int i, SsaImplInput::SourceVariable v) {
+    exists(AssignableDefinition ad | variableDefinition(bb, i, v, ad) |
+      w = ad or
+      w = getASameOutRefDefAfter(v, ad)
+    )
+    or
+    exists(Parameter p |
+      implicitEntryDefinition(bb, v) and
+      i = -1 and
+      p = v.getAssignable() and
+      pragma[only_bind_out](p.getCallable()) = pragma[only_bind_out](v.getEnclosingCallable()) and
+      w.isParameterInit(p)
+    )
+  }
+}
+
+module Ssa_ = Impl::MakeSsa<SsaInput>;
 
 class Definition = Impl::Definition;
 
@@ -815,7 +848,7 @@ private module Cached {
   predicate variableWriteQualifier(
     BasicBlock bb, int i, QualifiedFieldOrPropSourceVariable v, boolean certain
   ) {
-    SsaInput::variableWrite(bb, i, v.getQualifier(), certain) and
+    SsaImplInput::variableWrite(bb, i, v.getQualifier(), certain) and
     // Eliminate corner case where a call definition can overlap with a
     // qualifier definition: if method `M` updates field `F`, then a call
     // to `M` is both an update of `x.M` and `x.M.M`, so the former call

@@ -42,9 +42,9 @@ private TLocalScopeVariableReadOrSsaDef getANextReadOrDef(TLocalScopeVariableRea
   )
   or
   exists(Ssa::Definition ssaDef | prev = TSsaDefinition(ssaDef) |
-    result = TLocalScopeVariableRead(ssaDef.getAFirstRead())
+    result = TLocalScopeVariableRead(Ssa::ssaGetAFirstUse(ssaDef))
     or
-    not exists(ssaDef.getAFirstRead()) and
+    not exists(Ssa::ssaGetAFirstUse(ssaDef)) and
     exists(Ssa::PhiNode phi |
       phi.getAnInput() = ssaDef and
       result = TSsaDefinition(phi)