Merge pull request #21762 from aschackmull/csharp/ssa2

C#: Replace SSA classes with shared code.

Author: aschackmull

csharp/ql/consistency-queries/SsaConsistency.ql

@@ -7,8 +7,8 @@ query predicate localDeclWithSsaDef(LocalVariableDeclExpr d) {
   // Local variables in C# must be initialized before every use, so uninitialized
   // local variables should not have an SSA definition, as that would imply that
   // the declaration is live (can reach a use without passing through a definition)
-  exists(ExplicitDefinition def |
-    d = def.getADefinition().(AssignableDefinitions::LocalVariableDefinition).getDeclaration()
+  exists(SsaExplicitWrite def |
+    d = def.getDefinition().(AssignableDefinitions::LocalVariableDefinition).getDeclaration()
   |
     not d = any(ForeachStmt fs).getVariableDeclExpr() and
     not d = any(SpecificCatchClause scc).getVariableDeclExpr() and

csharp/ql/lib/change-notes/2026-05-01-ssa-replacement.md

@@ -0,0 +1,4 @@
+---
+category: deprecated
+---
+* The QL classes in the C# SSA library have been renamed to improve consistency between languages. Any custom QL code that makes use of SSA needs to be updated. The old classes have been deprecated and include more detailed migration instructions in their qldoc.

csharp/ql/lib/semmle/code/csharp/Assignable.qll

@@ -500,11 +500,7 @@ 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(SsaExplicitWrite def | result = Ssa::ssaGetAFirstUse(def) | this = def.getDefinition())
   }
 
   /** Gets a textual representation of this assignable definition. */

csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowReachability.qll

@@ -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;
 

csharp/ql/lib/semmle/code/csharp/controlflow/Guards.qll

@@ -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`
@@ -586,30 +570,30 @@ class AccessOrCallExpr extends Expr {
    * An expression can have more than one SSA qualifier in the presence
    * of control flow splitting.
    */
-  Ssa::Definition getAnSsaQualifier(ControlFlowNode cfn) { result = getAnSsaQualifier(this, cfn) }
+  SsaDefinition getAnSsaQualifier(ControlFlowNode cfn) { result = getAnSsaQualifier(this, cfn) }
 }
 
 private Declaration getDeclarationTarget(Expr e) {
   e = any(AssignableAccess aa | result = aa.getTarget()) or
   result = e.(Call).getTarget()
 }
 
-private Ssa::Definition getAnSsaQualifier(Expr e, ControlFlowNode cfn) {
+private SsaDefinition getAnSsaQualifier(Expr e, ControlFlowNode cfn) {
   e = getATrackedAccess(result, cfn)
   or
   not e = getATrackedAccess(_, _) and
   result = getAnSsaQualifier(e.(QualifiableExpr).getQualifier(), cfn)
 }
 
-private AssignableAccess getATrackedAccess(Ssa::Definition def, ControlFlowNode cfn) {
-  result = def.getAReadAtNode(cfn)
+private AssignableAccess getATrackedAccess(SsaDefinition def, ControlFlowNode cfn) {
+  result = def.getARead() and cfn = result.getControlFlowNode()
   or
-  result = def.(Ssa::ExplicitDefinition).getADefinition().getTargetAccess() and
+  result = def.(SsaExplicitWrite).getDefinition().getTargetAccess() and
   cfn = def.getControlFlowNode()
 }
 
 private predicate ssaMustHaveValue(Expr e, GuardValue v) {
-  exists(Ssa::Definition def, BasicBlock bb |
+  exists(SsaDefinition def, BasicBlock bb |
     e = def.getARead() and
     e.getBasicBlock() = bb and
     Guards::ssaControls(def, bb, v)
@@ -841,29 +825,25 @@ module Internal {
     )
     or
     e =
-      any(Ssa::Definition def |
-        forex(Ssa::Definition u | u = def.getAnUltimateDefinition() | nullDef(u))
+      any(SsaDefinition def |
+        forex(SsaDefinition u | u = def.getAnUltimateDefinition() | nullDef(u))
       ).getARead()
   }
 
-  private predicate nullDef(Ssa::ExplicitDefinition def) {
-    nullValueImplied(def.getADefinition().getSource())
-  }
+  private predicate nullDef(SsaExplicitWrite def) { nullValueImplied(def.getValue()) }
 
   predicate nonNullValueImplied(Expr e) {
     nonNullValue(e)
     or
     exists(Expr e1 | nonNullValueImplied(e1) and nonNullValueImpliedUnary(e1, e))
     or
     e =
-      any(Ssa::Definition def |
-        forex(Ssa::Definition u | u = def.getAnUltimateDefinition() | nonNullDef(u))
+      any(SsaDefinition def |
+        forex(SsaDefinition u | u = def.getAnUltimateDefinition() | nonNullDef(u))
       ).getARead()
   }
 
-  private predicate nonNullDef(Ssa::ExplicitDefinition def) {
-    nonNullValueImplied(def.getADefinition().getSource())
-  }
+  private predicate nonNullDef(SsaExplicitWrite def) { nonNullValueImplied(def.getValue()) }
 
   /** A callable that always returns a non-`null` value. */
   private class NonNullCallable extends Callable {
@@ -1120,7 +1100,7 @@ module Internal {
     private predicate nodeIsGuardedBySameSubExprSsaDef0(
       ControlFlowNode cfn, BasicBlock guardedBB, AccessOrCallExpr guarded, Guard g,
       ControlFlowNode subCfn, BasicBlock subCfnBB, AccessOrCallExpr sub, GuardValue v,
-      Ssa::Definition def
+      SsaDefinition def
     ) {
       nodeIsGuardedBySameSubExpr(cfn, guardedBB, guarded, g, sub, v) and
       def = sub.getAnSsaQualifier(subCfn) and
@@ -1130,7 +1110,7 @@ module Internal {
     pragma[nomagic]
     private predicate nodeIsGuardedBySameSubExprSsaDef(
       ControlFlowNode guardedCfn, AccessOrCallExpr guarded, Guard g, ControlFlowNode subCfn,
-      AccessOrCallExpr sub, GuardValue v, Ssa::Definition def
+      AccessOrCallExpr sub, GuardValue v, SsaDefinition def
     ) {
       exists(BasicBlock guardedBB, BasicBlock subCfnBB |
         nodeIsGuardedBySameSubExprSsaDef0(guardedCfn, guardedBB, guarded, g, subCfn, subCfnBB, sub,
@@ -1149,7 +1129,7 @@ module Internal {
     cached
     predicate isGuardedByExpr(AccessOrCallExpr guarded, Guard g, AccessOrCallExpr sub, GuardValue v) {
       isGuardedByExpr0(guarded, g, sub, v) and
-      forall(ControlFlowNode subCfn, Ssa::Definition def |
+      forall(ControlFlowNode subCfn, SsaDefinition def |
         nodeIsGuardedBySameSubExprSsaDef(_, guarded, g, subCfn, sub, v, def)
       |
         def = guarded.getAnSsaQualifier(_)
@@ -1161,7 +1141,7 @@ module Internal {
       ControlFlowNodes::ElementNode guarded, Guard g, AccessOrCallExpr sub, GuardValue v
     ) {
       nodeIsGuardedBySameSubExpr(guarded, _, _, g, sub, v) and
-      forall(ControlFlowNode subCfn, Ssa::Definition def |
+      forall(ControlFlowNode subCfn, SsaDefinition def |
         nodeIsGuardedBySameSubExprSsaDef(guarded, _, g, subCfn, sub, v, def)
       |
         def =

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

@@ -67,8 +67,8 @@ class AlwaysNullExpr extends Expr {
     exists(AlwaysNullExpr e1, AlwaysNullExpr e2 | G::Internal::nullValueImpliedBinary(e1, e2, this))
     or
     this =
-      any(Ssa::Definition def |
-        forex(Ssa::Definition u | u = def.getAnUltimateDefinition() | nullDef(u))
+      any(SsaDefinition def |
+        forex(SsaDefinition u | u = def.getAnUltimateDefinition() | nullDef(u))
       ).getARead()
     or
     exists(Callable target |
@@ -80,9 +80,7 @@ class AlwaysNullExpr extends Expr {
 }
 
 /** Holds if SSA definition `def` is always `null`. */
-private predicate nullDef(Ssa::ExplicitDefinition def) {
-  def.getADefinition().getSource() instanceof AlwaysNullExpr
-}
+private predicate nullDef(SsaExplicitWrite def) { def.getValue() instanceof AlwaysNullExpr }
 
 /** An expression that is never `null`. */
 class NonNullExpr extends Expr {
@@ -94,8 +92,8 @@ class NonNullExpr extends Expr {
     this instanceof G::NullGuardedExpr
     or
     this =
-      any(Ssa::Definition def |
-        forex(Ssa::Definition u | u = def.getAnUltimateDefinition() | nonNullDef(u))
+      any(SsaDefinition def |
+        forex(SsaDefinition u | u = def.getAnUltimateDefinition() | nonNullDef(u))
       ).getARead()
     or
     exists(Callable target |
@@ -108,10 +106,10 @@ class NonNullExpr extends Expr {
 }
 
 /** Holds if SSA definition `def` is never `null`. */
-private predicate nonNullDef(Ssa::ExplicitDefinition def) {
-  def.getADefinition().getSource() instanceof NonNullExpr
+private predicate nonNullDef(SsaExplicitWrite def) {
+  def.getValue() instanceof NonNullExpr
   or
-  exists(AssignableDefinition ad | ad = def.getADefinition() |
+  exists(AssignableDefinition ad | ad = def.getDefinition() |
     ad instanceof AssignableDefinitions::PatternDefinition
     or
     ad =
@@ -124,13 +122,11 @@ private predicate nonNullDef(Ssa::ExplicitDefinition def) {
 }
 
 /**
- * Holds if `node` is a dereference `d` of SSA definition `def`.
+ * Holds if `d` is a dereference of SSA definition `def`.
  */
-private predicate dereferenceAt(ControlFlowNode node, Ssa::Definition def, Dereference d) {
-  d = def.getAReadAtNode(node)
-}
+private predicate dereferenceAt(SsaDefinition def, Dereference d) { d = def.getARead() }
 
-private predicate isMaybeNullArgument(Ssa::ParameterDefinition def, MaybeNullExpr arg) {
+private predicate isMaybeNullArgument(SsaParameterInit def, MaybeNullExpr arg) {
   exists(AssignableDefinitions::ImplicitParameterDefinition pdef, Parameter p |
     p = def.getParameter()
   |
@@ -182,18 +178,18 @@ private predicate hasMultipleParamsArguments(Call c) {
 }
 
 /** Holds if `def` is an SSA definition that may be `null`. */
-private predicate defMaybeNull(Ssa::Definition def, ControlFlowNode node, string msg, Element reason) {
+private predicate defMaybeNull(SsaDefinition def, ControlFlowNode node, string msg, Element reason) {
   not nonNullDef(def) and
   (
     // A variable compared to `null` might be `null`
     exists(G::DereferenceableExpr de | de = def.getARead() |
       de.guardSuggestsMaybeNull(reason) and
       msg = "as suggested by $@ null check" and
       node = def.getControlFlowNode() and
-      not de = any(Ssa::PhiNode phi).getARead() and
+      not de = any(SsaPhiDefinition phi).getARead() and
       // Don't use a check as reason if there is a `null` assignment
       // or argument
-      not def.(Ssa::ExplicitDefinition).getADefinition().getSource() instanceof MaybeNullExpr and
+      not def.(SsaExplicitWrite).getValue() instanceof MaybeNullExpr and
       not isMaybeNullArgument(def, _)
     )
     or
@@ -207,41 +203,41 @@ private predicate defMaybeNull(Ssa::Definition def, ControlFlowNode node, string
     )
     or
     // If the source of a variable is `null` then the variable may be `null`
-    exists(AssignableDefinition adef | adef = def.(Ssa::ExplicitDefinition).getADefinition() |
+    exists(AssignableDefinition adef | adef = def.(SsaExplicitWrite).getDefinition() |
       adef.getSource() = maybeNullExpr(node.asExpr()) and
       reason = adef.getExpr() and
       msg = "because of $@ assignment"
     )
     or
     // A variable of nullable type may be null
-    exists(Dereference d | dereferenceAt(_, def, d) |
+    exists(Dereference d | dereferenceAt(def, d) |
       node = def.getControlFlowNode() and
       d.hasNullableType() and
-      not def instanceof Ssa::PhiNode and
+      not def instanceof SsaPhiDefinition and
       reason = def.getSourceVariable().getAssignable() and
       msg = "because it has a nullable type"
     )
   )
 }
 
-private Ssa::Definition getAPseudoInput(Ssa::Definition def) {
-  result = def.(Ssa::PhiNode).getAnInput()
+private SsaDefinition getAPseudoInput(SsaDefinition def) {
+  result = def.(SsaPhiDefinition).getAnInput()
 }
 
 // `def.getAnUltimateDefinition()` includes inputs into uncertain
 // definitions, but we only want inputs into pseudo nodes
-private Ssa::Definition getAnUltimateDefinition(Ssa::Definition def) {
+private SsaDefinition getAnUltimateDefinition(SsaDefinition def) {
   result = getAPseudoInput*(def) and
-  not result instanceof Ssa::PhiNode
+  not result instanceof SsaPhiDefinition
 }
 
 /**
  * Holds if SSA definition `def` can reach a read at `cfn`, without passing
  * through an intermediate dereference that always throws a null reference
  * exception.
  */
-private predicate defReaches(Ssa::Definition def, ControlFlowNode cfn) {
-  exists(def.getAFirstReadAtNode(cfn))
+private predicate defReaches(SsaDefinition def, ControlFlowNode cfn) {
+  Ssa::ssaGetAFirstUse(def).getControlFlowNode() = cfn
   or
   exists(ControlFlowNode mid | defReaches(def, mid) |
     SsaImpl::adjacentReadPairSameVar(_, mid, cfn) and
@@ -250,11 +246,12 @@ 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
+      dereferenceAt(def, d) and
+      node = d.getControlFlowNode() and
       not d instanceof NonNullExpr
     )
   }
@@ -267,11 +264,12 @@ private module NullnessConfig implements ControlFlowReachability::ConfigSig {
 private module NullnessFlow = ControlFlowReachability::Flow<NullnessConfig>;
 
 predicate maybeNullDeref(Dereference d, Ssa::SourceVariable v, string msg, Element reason) {
-  exists(Ssa::Definition origin, Ssa::Definition ssa, ControlFlowNode src, ControlFlowNode sink |
+  exists(SsaDefinition origin, SsaDefinition ssa, ControlFlowNode src, ControlFlowNode sink |
     defMaybeNull(origin, src, msg, reason) and
     NullnessFlow::flow(src, origin, sink, ssa) and
     ssa.getSourceVariable() = v and
-    dereferenceAt(sink, ssa, d) and
+    dereferenceAt(ssa, d) and
+    sink = d.getControlFlowNode() and
     not d.isAlwaysNull(v)
   )
 }
@@ -322,9 +320,7 @@ class Dereference extends G::DereferenceableExpr {
         not p.getAnnotatedType().isNullableRefType()
         or
         p.fromSource() and
-        exists(
-          Ssa::ParameterDefinition def, AssignableDefinitions::ImplicitParameterDefinition pdef
-        |
+        exists(SsaParameterInit def, AssignableDefinitions::ImplicitParameterDefinition pdef |
           p = def.getParameter()
         |
           p.getUnboundDeclaration() = pdef.getParameter() and
@@ -334,9 +330,9 @@ class Dereference extends G::DereferenceableExpr {
     )
   }
 
-  private predicate isAlwaysNull0(Ssa::Definition def) {
-    forall(Ssa::Definition input | input = getAnUltimateDefinition(def) |
-      input.(Ssa::ExplicitDefinition).getADefinition().getSource() instanceof AlwaysNullExpr
+  private predicate isAlwaysNull0(SsaDefinition def) {
+    forall(SsaDefinition input | input = getAnUltimateDefinition(def) |
+      input.(SsaExplicitWrite).getValue() instanceof AlwaysNullExpr
     ) and
     not nonNullDef(def) and
     this = def.getARead() and
@@ -352,7 +348,7 @@ class Dereference extends G::DereferenceableExpr {
     // Exclude fields and properties, as they may not have an accurate SSA representation
     v.getAssignable() instanceof LocalScopeVariable and
     (
-      forex(Ssa::Definition def0 | this = def0.getARead() | this.isAlwaysNull0(def0))
+      forex(SsaDefinition def0 | this = def0.getARead() | this.isAlwaysNull0(def0))
       or
       exists(G::GuardValue nv |
         this.(G::GuardedExpr).mustHaveValue(nv) and