C#: Replace SSA classes with shared code.

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/semmle/code/csharp/Assignable.qll

@@ -488,16 +488,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()
-      )
-      or
-      exists(Ssa::ImplicitParameterDefinition def | result = def.getAFirstReadAtNode(cfn) |
-        this.(AssignableDefinitions::ImplicitParameterDefinition).getParameter() =
-          def.getParameter()
-      )
-    )
+    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::ImplicitParameterDefinition {
-    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::ImplicitParameterDefinition def, MaybeNullExpr arg) {
+private predicate isMaybeNullArgument(SsaParameterInit def, MaybeNullExpr arg) {
   exists(AssignableDefinitions::ImplicitParameterDefinition pdef, Parameter p |
     p = def.getParameter()
   |
@@ -181,7 +177,7 @@ private predicate hasMultipleParamsArguments(Call c) {
   )
 }
 
-private predicate isNullDefaultArgument(Ssa::ImplicitParameterDefinition def, AlwaysNullExpr arg) {
+private predicate isNullDefaultArgument(SsaParameterInit def, AlwaysNullExpr arg) {
   exists(AssignableDefinitions::ImplicitParameterDefinition pdef, Parameter p |
     p = def.getParameter()
   |
@@ -192,18 +188,18 @@ private predicate isNullDefaultArgument(Ssa::ImplicitParameterDefinition def, Al
 }
 
 /** 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
@@ -221,41 +217,41 @@ private predicate defMaybeNull(Ssa::Definition def, ControlFlowNode node, string
     msg = "because the parameter has a null default value"
     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
@@ -264,11 +260,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
     )
   }
@@ -281,11 +278,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)
   )
 }
@@ -336,10 +334,7 @@ class Dereference extends G::DereferenceableExpr {
         not p.getAnnotatedType().isNullableRefType()
         or
         p.fromSource() and
-        exists(
-          Ssa::ImplicitParameterDefinition def,
-          AssignableDefinitions::ImplicitParameterDefinition pdef
-        |
+        exists(SsaParameterInit def, AssignableDefinitions::ImplicitParameterDefinition pdef |
           p = def.getParameter()
         |
           p.getUnboundDeclaration() = pdef.getParameter() and
@@ -349,9 +344,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
@@ -367,7 +362,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