C#: Replace Ssa::ExplicitDefinition with SsaExplicitWrite.

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

@@ -500,9 +500,7 @@ class AssignableDefinition extends TAssignableDefinition {
    */
   pragma[nomagic]
   AssignableRead getAFirstRead() {
-    exists(Ssa::ExplicitDefinition def | result = Ssa::ssaGetAFirstUse(def) |
-      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/Guards.qll

@@ -588,7 +588,7 @@ private SsaDefinition getAnSsaQualifier(Expr e, ControlFlowNode 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()
 }
 
@@ -830,9 +830,7 @@ module Internal {
       ).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)
@@ -845,9 +843,7 @@ module Internal {
       ).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 {

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

@@ -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 {
@@ -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 =
@@ -191,7 +189,7 @@ private predicate defMaybeNull(SsaDefinition def, ControlFlowNode node, string m
       not de = any(Ssa::PhiNode 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
@@ -205,7 +203,7 @@ private predicate defMaybeNull(SsaDefinition def, ControlFlowNode node, string m
     )
     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"
@@ -336,7 +334,7 @@ class Dereference extends G::DereferenceableExpr {
 
   private predicate isAlwaysNull0(SsaDefinition def) {
     forall(SsaDefinition input | input = getAnUltimateDefinition(def) |
-      input.(Ssa::ExplicitDefinition).getADefinition().getSource() instanceof AlwaysNullExpr
+      input.(SsaExplicitWrite).getValue() instanceof AlwaysNullExpr
     ) and
     not nonNullDef(def) and
     this = def.getARead() and

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

@@ -428,19 +428,25 @@ module Ssa {
   }
 
   /**
+   * DEPRECATED: Use `SsaExplicitWrite` instead.
+   *
    * An SSA definition that corresponds to an explicit assignable definition.
    */
-  class ExplicitDefinition extends Definition, SsaImpl::WriteDefinition {
+  deprecated class ExplicitDefinition extends Definition, SsaImpl::WriteDefinition {
     AssignableDefinition ad;
 
     ExplicitDefinition() { SsaImpl::explicitDefinition(this, _, ad) }
 
     /**
+     * DEPRECATED: Use `SsaExplicitWrite.getDefinition()` instead.
+     *
      * Gets an underlying assignable definition. The result is always unique,
      * except for pathological `out`/`ref` assignments like `M(out x, out x)`,
      * where there may be more than one underlying definition.
      */
-    final AssignableDefinition getADefinition() { result = SsaImpl::getADefinition(this) }
+    deprecated final AssignableDefinition getADefinition() {
+      result = SsaImpl::getADefinition(this)
+    }
 
     /**
      * DEPRECATED.

csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll

@@ -272,7 +272,7 @@ module VariableCapture {
     or
     exists(SsaDefinition def, AssignableDefinition adef |
       LocalFlow::defAssigns(adef, _, _, e1) and
-      def.getAnUltimateDefinition().(Ssa::ExplicitDefinition).getADefinition() = adef and
+      def.getAnUltimateDefinition().(SsaExplicitWrite).getDefinition() = adef and
       def.getARead().getControlFlowNode() = e2
     )
   }
@@ -600,8 +600,8 @@ module LocalFlow {
     or
     ThisFlow::adjacentThisRefs(nodeFrom.(PostUpdateNode).getPreUpdateNode(), nodeTo)
     or
-    exists(AssignableDefinition def, ControlFlowNode cfn, Ssa::ExplicitDefinition ssaDef |
-      ssaDef.getADefinition() = def and
+    exists(AssignableDefinition def, ControlFlowNode cfn, SsaExplicitWrite ssaDef |
+      ssaDef.getDefinition() = def and
       ssaDef.getControlFlowNode() = cfn and
       nodeFrom = TAssignableDefinitionNode(def, cfn) and
       nodeTo.(SsaDefinitionNode).getDefinition() = ssaDef
@@ -2220,12 +2220,11 @@ private predicate readContentStep(Node node1, Content c, Node node2) {
   c instanceof ElementContent
   or
   exists(
-    ForeachStmt fs, Ssa::ExplicitDefinition def,
-    AssignableDefinitions::LocalVariableDefinition defTo
+    ForeachStmt fs, SsaExplicitWrite def, AssignableDefinitions::LocalVariableDefinition defTo
   |
     node1.asExpr() = fs.getIterableExpr() and
     defTo.getDeclaration() = fs.getVariableDeclExpr() and
-    def.getADefinition() = defTo and
+    def.getDefinition() = defTo and
     node2.(SsaDefinitionNode).getDefinition() = def and
     c instanceof ElementContent
   )

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

@@ -825,7 +825,7 @@ private module Cached {
   }
 
   cached
-  AssignableDefinition getADefinition(Ssa::ExplicitDefinition def) {
+  deprecated AssignableDefinition getADefinition(Ssa::ExplicitDefinition def) {
     exists(Ssa::SourceVariable v, AssignableDefinition ad | explicitDefinition(def, v, ad) |
       result = ad or
       result = getASameOutRefDefAfter(v, ad)
@@ -858,7 +858,9 @@ private module Cached {
   }
 
   cached
-  predicate explicitDefinition(WriteDefinition def, Ssa::SourceVariable v, AssignableDefinition ad) {
+  deprecated predicate explicitDefinition(
+    WriteDefinition def, Ssa::SourceVariable v, AssignableDefinition ad
+  ) {
     exists(BasicBlock bb, int i |
       def.definesAt(v, bb, i) and
       variableDefinition(bb, i, v, ad)
@@ -1023,7 +1025,7 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
    * as we, conservatively, consider such definitions to be certain.
    */
   predicate allowFlowIntoUncertainDef(UncertainWriteDefinition def) {
-    def instanceof Ssa::ExplicitDefinition
+    def instanceof SsaExplicitWrite
     or
     def =
       any(Ssa::ImplicitQualifierDefinition qdef |

csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/RangeUtils.qll

@@ -19,7 +19,7 @@ private module Impl {
   }
 
   /** Holds if SSA definition `def` equals `e + delta`. */
-  predicate ssaUpdateStep(ExplicitDefinition def, ExprNode e, int delta) {
+  predicate ssaUpdateStep(SsaExplicitWrite def, ExprNode e, int delta) {
     exists(ControlFlowNode cfn | cfn = def.getControlFlowNode() |
       e = cfn.(ExprNode::Assignment).getRightOperand() and
       delta = 0 and

csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll

@@ -35,7 +35,7 @@ module Private {
 
   class Expr = CS::ControlFlowNodes::ExprNode;
 
-  class VariableUpdate = CS::Ssa::ExplicitDefinition;
+  class VariableUpdate = CS::SsaExplicitWrite;
 
   class Field = CS::Field;
 
@@ -122,37 +122,25 @@ private module Impl {
   }
 
   /** Returns the underlying variable update of the explicit SSA variable `v`. */
-  Ssa::ExplicitDefinition getExplicitSsaAssignment(Ssa::ExplicitDefinition v) { result = v }
+  SsaExplicitWrite getExplicitSsaAssignment(SsaExplicitWrite v) { result = v }
 
   /** Returns the assignment of the variable update `def`. */
-  ExprNode getExprFromSsaAssignment(Ssa::ExplicitDefinition def) {
-    exists(AssignableDefinition adef |
-      adef = def.getADefinition() and
-      hasChild(adef.getExpr(), adef.getSource(), def.getControlFlowNode(), result)
-    )
-    or
-    exists(AssignableDefinitions::AssignOperationDefinition adef |
-      adef = def.getADefinition() and
-      result.getExpr() = adef.getSource()
-    )
-  }
+  ExprNode getExprFromSsaAssignment(SsaExplicitWrite def) { result.getExpr() = def.getValue() }
 
   /** Holds if `def` can have any sign. */
-  predicate explicitSsaDefWithAnySign(Ssa::ExplicitDefinition def) {
-    not exists(def.getADefinition().getSource()) and
-    not def.getElement() instanceof MutatorOperation
+  predicate explicitSsaDefWithAnySign(SsaExplicitWrite def) {
+    not exists(def.getValue()) and
+    not def.getDefiningExpr() instanceof MutatorOperation
   }
 
   /** Returns the operand of the operation if `def` is a decrement. */
-  ExprNode getDecrementOperand(Ssa::ExplicitDefinition def) {
-    hasChild(def.getElement(), def.getElement().(DecrementOperation).getOperand(),
-      def.getControlFlowNode(), result)
+  ExprNode getDecrementOperand(SsaExplicitWrite def) {
+    result.getExpr() = def.getDefiningExpr().(DecrementOperation).getOperand()
   }
 
   /** Returns the operand of the operation if `def` is an increment. */
-  ExprNode getIncrementOperand(Ssa::ExplicitDefinition def) {
-    hasChild(def.getElement(), def.getElement().(IncrementOperation).getOperand(),
-      def.getControlFlowNode(), result)
+  ExprNode getIncrementOperand(SsaExplicitWrite def) {
+    result.getExpr() = def.getDefiningExpr().(IncrementOperation).getOperand()
   }
 
   /** Gets the variable underlying the implicit SSA variable `def`. */

csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaUtils.qll

@@ -17,9 +17,9 @@ class SsaVariable extends SsaDefinition {
 
 /** Gets a node that reads `src` via an SSA explicit definition. */
 ExprNode getAnExplicitDefinitionRead(ExprNode src) {
-  exists(ExplicitDefinition def |
+  exists(SsaExplicitWrite def |
     def.getARead().getControlFlowNode() = result and
-    hasChild(def.getElement(), def.getADefinition().getSource(), def.getControlFlowNode(), src)
+    hasChild(def.getDefiningExpr(), def.getValue(), def.getControlFlowNode(), src)
   )
 }
 
@@ -45,15 +45,15 @@ ExprNode ssaRead(SsaDefinition v, int delta) {
     delta = d1 + c.getIntValue()
   )
   or
-  v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PreIncrExpr) = result and delta = 0
+  v.(SsaExplicitWrite).getControlFlowNode().(ExprNode::PreIncrExpr) = result and delta = 0
   or
-  v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PreDecrExpr) = result and delta = 0
+  v.(SsaExplicitWrite).getControlFlowNode().(ExprNode::PreDecrExpr) = result and delta = 0
   or
-  v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PostIncrExpr) = result and delta = 1 // x++ === ++x - 1
+  v.(SsaExplicitWrite).getControlFlowNode().(ExprNode::PostIncrExpr) = result and delta = 1 // x++ === ++x - 1
   or
-  v.(ExplicitDefinition).getControlFlowNode().(ExprNode::PostDecrExpr) = result and delta = -1 // x-- === --x + 1
+  v.(SsaExplicitWrite).getControlFlowNode().(ExprNode::PostDecrExpr) = result and delta = -1 // x-- === --x + 1
   or
-  v.(ExplicitDefinition).getControlFlowNode().(ExprNode::Assignment) = result and delta = 0
+  v.(SsaExplicitWrite).getControlFlowNode().(ExprNode::Assignment) = result and delta = 0
   or
   result.(ExprNode::AssignExpr).getRightOperand() = ssaRead(v, delta)
 }

csharp/ql/src/Dead Code/DeadStoreOfLocal.ql

@@ -92,7 +92,7 @@ class RelevantDefinition extends AssignableDefinition {
   private predicate isMaybeLive() {
     exists(LocalVariable v | v = this.getTarget() |
       // SSA definitions are only created for live variables
-      this = any(Ssa::ExplicitDefinition ssaDef).getADefinition()
+      this = any(SsaExplicitWrite ssaDef).getDefinition()
       or
       mayEscape(v)
       or

csharp/ql/src/Likely Bugs/Dynamic/BadDynamicCall.ql

@@ -36,17 +36,16 @@ abstract class BadDynamicCall extends DynamicExpr {
   }
 
   private Type possibleTypeForRelevantSource(Variable v, int i, Expr source) {
-    exists(AssignableRead read, SsaDefinition ssaDef, Ssa::ExplicitDefinition ultimateSsaDef |
+    exists(AssignableRead read, SsaDefinition ssaDef, SsaExplicitWrite ultimateSsaDef |
       read = this.getARelevantVariableAccess(i) and
       v = read.getTarget() and
       result = source.getType() and
       read = ssaDef.getARead() and
       ultimateSsaDef = ssaDef.getAnUltimateDefinition()
     |
-      ultimateSsaDef.getADefinition() =
-        any(AssignableDefinition def | source = def.getSource().stripImplicit())
+      ultimateSsaDef.getValue().stripImplicit() = source
       or
-      ultimateSsaDef.getADefinition() =
+      ultimateSsaDef.getDefinition() =
         any(AssignableDefinitions::ImplicitParameterDefinition p |
           source = p.getParameter().getAnAssignedValue().stripImplicit()
         )

csharp/ql/test/library-tests/csharp7/DefUse.ql

@@ -3,11 +3,6 @@ import csharp
 from AssignableDefinition def, AssignableRead read, SsaDefinition ult, SsaDefinition ssaDef
 where
   ssaDef.getAnUltimateDefinition() = ult and
-  (
-    ult.(Ssa::ExplicitDefinition).getADefinition() = def
-    or
-    ult.(Ssa::ParameterDefinition).getParameter() =
-      def.(AssignableDefinitions::ImplicitParameterDefinition).getParameter()
-  ) and
+  ult.(SsaExplicitWrite).getDefinition() = def and
   read = ssaDef.getARead()
 select def, read

csharp/ql/test/library-tests/dataflow/callablereturnsarg/Common.qll

@@ -2,9 +2,9 @@ import csharp
 private import semmle.code.csharp.controlflow.Guards
 
 private predicate outRefDef(DataFlow::ExprNode ne, int outRef) {
-  exists(Ssa::ExplicitDefinition def, Parameter outRefParameter |
+  exists(SsaExplicitWrite def, Parameter outRefParameter |
     outRefParameter.isOutOrRef() and
-    ne.getExpr() = def.getADefinition().getSource() and
+    ne.getExpr() = def.getValue() and
     Ssa::isLiveOutRefParameterDefinition(def, outRefParameter) and
     outRef = outRefParameter.getPosition()
   )

csharp/ql/test/library-tests/dataflow/defuse/defUseEquivalence.ql

@@ -12,6 +12,10 @@ predicate defReaches(
       def.(AssignableDefinitions::ImplicitParameterDefinition).getParameter().getControlFlowNode()
     ].getASuccessor()
   or
+  def.getTarget() = v and
+  cfn =
+    def.(AssignableDefinitions::ImplicitParameterDefinition).getEnclosingCallable().getEntryPoint()
+  or
   exists(ControlFlowNode mid | defReaches(def, v, mid) |
     not mid =
       any(AssignableDefinition ad | ad.getTarget() = v and ad.isCertain())
@@ -30,7 +34,7 @@ predicate defUsePair(AssignableDefinition def, AssignableRead read) {
 
 private LocalScopeVariableRead getAReachableUncertainRead(AssignableDefinition def) {
   exists(SsaDefinition ssaDef |
-    def = ssaDef.getAnUltimateDefinition().(Ssa::ExplicitDefinition).getADefinition()
+    def = ssaDef.getAnUltimateDefinition().(SsaExplicitWrite).getDefinition()
   |
     result = ssaDef.getARead()
   )

csharp/ql/test/library-tests/dataflow/ssa-large/countssa.ql

@@ -2,6 +2,6 @@ import csharp
 
 from int uses, int live
 where
-  uses = strictcount(Ssa::ExplicitDefinition ssa, AssignableRead read | read = ssa.getARead()) and
-  live = strictcount(Ssa::ExplicitDefinition ssa, BasicBlock bb | ssa.isLiveAtEndOfBlock(bb))
+  uses = strictcount(SsaExplicitWrite ssa, AssignableRead read | read = ssa.getARead()) and
+  live = strictcount(SsaExplicitWrite ssa, BasicBlock bb | ssa.isLiveAtEndOfBlock(bb))
 select uses, live

csharp/ql/test/library-tests/dataflow/ssa/BaseSsaConsistency.ql

@@ -8,12 +8,8 @@ where
   ar = ssaDef.getARead() and
   def = ssaDef.getDefinition() and
   v = def.getTarget() and
-  not exists(Ssa::ExplicitDefinition edef |
-    edef.getADefinition() = def and
-    edef.getARead() = ar
-  ) and
-  not exists(Ssa::ParameterDefinition edef |
-    edef.getParameter() = def.(AssignableDefinitions::ImplicitParameterDefinition).getParameter() and
+  not exists(SsaExplicitWrite edef |
+    edef.getDefinition() = def and
     edef.getARead() = ar
   )
 select ar, def

csharp/ql/test/library-tests/dataflow/ssa/SsaExplicitDef.ql

@@ -1,5 +1,5 @@
 import csharp
 
-from Ssa::SourceVariable v, Ssa::ExplicitDefinition def
+from Ssa::SourceVariable v, SsaExplicitWrite def
 where v = def.getSourceVariable()
-select v, def, def.getADefinition()
+select v, def, def.getDefinition()