Merge pull request #4959 from hvitved/csharp/ssa/split

C#: Split up SSA implementation

Author: hvitved

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

@@ -3,6 +3,7 @@
  */
 
 import csharp
+private import semmle.code.csharp.dataflow.internal.SsaImpl as SsaImpl
 
 /**
  * An assignable, that is, an element that can be assigned to. Either a
@@ -83,7 +84,7 @@ class AssignableRead extends AssignableAccess {
 
   pragma[noinline]
   private ControlFlow::Node getAnAdjacentReadSameVar() {
-    Ssa::Internal::adjacentReadPairSameVar(_, this.getAControlFlowNode(), result)
+    SsaImpl::adjacentReadPairSameVar(_, this.getAControlFlowNode(), result)
   }
 
   /**

csharp/ql/src/semmle/code/csharp/commons/ConsistencyChecks.qll

@@ -46,7 +46,10 @@ module SsaChecks {
   }
 
   predicate notDominatedByDef(AssignableRead read, string m) {
-    exists(Definition def, BasicBlock bb, ControlFlow::Node rnode, ControlFlow::Node dnode, int i |
+    exists(
+      Definition def, ControlFlow::BasicBlock bb, ControlFlow::Node rnode, ControlFlow::Node dnode,
+      int i
+    |
       def.getAReadAtNode(rnode) = read
     |
       def.definesAt(_, bb, i) and

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

@@ -1723,6 +1723,7 @@ module Internal {
   cached
   private module Cached {
     private import semmle.code.csharp.Caching
+    private import semmle.code.csharp.dataflow.internal.SsaImpl as SsaImpl
 
     /**
      * Holds if basic block `bb` only is reached when guard `g` has abstract value `v`.
@@ -1775,9 +1776,9 @@ module Internal {
     private predicate adjacentReadPairSameVarUniquePredecessor(
       Ssa::Definition def, ControlFlow::Node cfn1, ControlFlow::Node cfn2
     ) {
-      Ssa::Internal::adjacentReadPairSameVar(def, cfn1, cfn2) and
+      SsaImpl::adjacentReadPairSameVar(def, cfn1, cfn2) and
       not exists(ControlFlow::Node other |
-        Ssa::Internal::adjacentReadPairSameVar(def, other, cfn2) and
+        SsaImpl::adjacentReadPairSameVar(def, other, cfn2) and
         other != cfn1 and
         other != cfn2
       )
@@ -1831,7 +1832,7 @@ module Internal {
     private predicate firstReadUniquePredecessor(Ssa::ExplicitDefinition def, ControlFlow::Node cfn) {
       exists(def.getAFirstReadAtNode(cfn)) and
       not exists(ControlFlow::Node other |
-        Ssa::Internal::adjacentReadPairSameVar(def, other, cfn) and
+        SsaImpl::adjacentReadPairSameVar(def, other, cfn) and
         other != cfn
       )
     }

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

@@ -23,6 +23,7 @@ private import internal.CallableReturns
 private import semmle.code.csharp.commons.Assertions
 private import semmle.code.csharp.controlflow.Guards as G
 private import semmle.code.csharp.controlflow.Guards::AbstractValues
+private import semmle.code.csharp.dataflow.internal.SsaImpl as SsaImpl
 private import semmle.code.csharp.frameworks.System
 private import semmle.code.csharp.frameworks.Test
 
@@ -177,7 +178,7 @@ private predicate defMaybeNull(Ssa::Definition def, string msg, Element reason)
     exists(G::DereferenceableExpr de | de = def.getARead() |
       reason = de.getANullCheck(_, true) and
       msg = "as suggested by $@ null check" and
-      not de = any(Ssa::PseudoDefinition pdef).getARead() and
+      not de = any(Ssa::PhiNode phi).getARead() and
       strictcount(Element e | e = any(Ssa::Definition def0 | de = def0.getARead()).getElement()) = 1 and
       // Don't use a check as reason if there is a `null` assignment
       // or argument
@@ -205,7 +206,7 @@ private predicate defMaybeNull(Ssa::Definition def, string msg, Element reason)
     // A variable of nullable type may be null
     exists(Dereference d | dereferenceAt(_, _, def, d) |
       d.hasNullableType() and
-      not def instanceof Ssa::PseudoDefinition and
+      not def instanceof Ssa::PhiNode and
       reason = def.getSourceVariable().getAssignable() and
       msg = "because it has a nullable type"
     )
@@ -236,13 +237,13 @@ private predicate defNullImpliesStep(
   Ssa::Definition def1, BasicBlock bb1, Ssa::Definition def2, BasicBlock bb2
 ) {
   exists(Ssa::SourceVariable v | defNullImpliesStep0(v, def1, bb1, bb2) |
-    def2.(Ssa::PseudoDefinition).getAnInput() = def1 and
+    def2.(Ssa::PhiNode).getAnInput() = def1 and
     bb2 = def2.getBasicBlock()
     or
     def2 = def1 and
-    not exists(Ssa::PseudoDefinition def |
-      def.getSourceVariable() = v and
-      bb2 = def.getBasicBlock()
+    not exists(Ssa::PhiNode phi |
+      phi.getSourceVariable() = v and
+      bb2 = phi.getBasicBlock()
     )
   ) and
   not exists(SuccessorTypes::ConditionalSuccessor s, NullValue nv |
@@ -426,14 +427,14 @@ module PathGraph {
 }
 
 private Ssa::Definition getAPseudoInput(Ssa::Definition def) {
-  result = def.(Ssa::PseudoDefinition).getAnInput()
+  result = def.(Ssa::PhiNode).getAnInput()
 }
 
 // `def.getAnUltimateDefinition()` includes inputs into uncertain
 // definitions, but we only want inputs into pseudo nodes
 private Ssa::Definition getAnUltimateDefinition(Ssa::Definition def) {
   result = getAPseudoInput*(def) and
-  not result instanceof Ssa::PseudoDefinition
+  not result instanceof Ssa::PhiNode
 }
 
 /**
@@ -446,7 +447,7 @@ private predicate defReaches(Ssa::Definition def, ControlFlow::Node cfn, boolean
   (always = true or always = false)
   or
   exists(ControlFlow::Node mid | defReaches(def, mid, always) |
-    Ssa::Internal::adjacentReadPairSameVar(_, mid, cfn) and
+    SsaImpl::adjacentReadPairSameVar(_, mid, cfn) and
     not mid =
       any(Dereference d |
         if always = true