C#: Compute phi inputs in pre-SSA library

Logic is copied directly from the ordinary SSA library.

Author: hvitved

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

@@ -2516,8 +2516,12 @@ module ControlFlow {
           result = strictcount(getAnElement())
         }
 
+        predicate immediatelyDominates(PreBasicBlock bb) {
+          bbIDominates(this, bb)
+        }
+
         predicate strictlyDominates(PreBasicBlock bb) {
-          bbIDominates+(this, bb)
+          this.immediatelyDominates+(bb)
         }
 
         predicate dominates(PreBasicBlock bb) {
@@ -2584,8 +2588,6 @@ module ControlFlow {
         }
       }
 
-      private newtype SsaRefKind = SsaRead() or SsaDef()
-
       class Definition extends TPreSsaDef {
         string toString() {
           exists(AssignableDefinition def |
@@ -2626,12 +2628,25 @@ module ControlFlow {
           )
         }
 
+        PreBasicBlock getBasicBlock() {
+          this = TExplicitPreSsaDef(result, _, _, _) or
+          this = TPhiPreSsaDef(result, _)
+        }
+
         AssignableDefinition getDefinition() {
           this = TExplicitPreSsaDef(_, _, result, _)
         }
+
+        Definition getAPhiInput() {
+          exists(PreBasicBlock bb, PreBasicBlock phiPred, SimpleLocalScopeVariable v |
+            this = TPhiPreSsaDef(bb, v) |
+            bb.getAPredecessor() = phiPred and
+            ssaDefReachesEndOfBlock(phiPred, result, v)
+          )
+        }
       }
 
-      predicate assignableDefAt(PreBasicBlocks::PreBasicBlock bb, int i, AssignableDefinition def, SimpleLocalScopeVariable v) {
+      private predicate assignableDefAt(PreBasicBlocks::PreBasicBlock bb, int i, AssignableDefinition def, SimpleLocalScopeVariable v) {
         bb.getElement(i) = def.getExpr() and
         v = def.getTarget() and
         // In cases like `(x, x) = (0, 1)`, we discard the first (dead) definition of `x`
@@ -2650,16 +2665,82 @@ module ControlFlow {
         )
       }
 
+      private predicate readAt(PreBasicBlock bb, int i, LocalScopeVariableRead read, SimpleLocalScopeVariable v) {
+        read = bb.getElement(i) and
+        read.getTarget() = v
+      }
+
+      pragma[noinline]
+      private predicate exitBlock(PreBasicBlock bb, Callable c) {
+        exists(succExit(bb.getLastElement(), _)) and
+        c = bb.getEnclosingCallable()
+      }
+
+      private predicate outRefExitRead(PreBasicBlock bb, int i, SimpleLocalScopeVariable v) {
+        exitBlock(bb, v.getCallable()) and
+        i = bb.length() + 1 and
+        (v.isRef() or v.(Parameter).isOut())
+      }
+
+      private newtype RefKind =
+        Read()
+        or
+        Write(boolean certain) { certain = true or certain = false }
+
+      private predicate ref(PreBasicBlock bb, int i, SimpleLocalScopeVariable v, RefKind k) {
+        (readAt(bb, i, _, v) or outRefExitRead(bb, i, v)) and
+        k = Read()
+        or
+        exists(AssignableDefinition def, boolean certain |
+          assignableDefAt(bb, i, def, v) |
+          if def.getTargetAccess().isRefArgument() then certain = false else certain = true and
+          k = Write(certain)
+        )
+      }
+
+      private int refRank(PreBasicBlock bb, int i, SimpleLocalScopeVariable v, RefKind k) {
+        i = rank[result](int j | ref(bb, j, v, _)) and
+        ref(bb, i, v, k)
+      }
+
+      private int firstReadOrCertainWrite(PreBasicBlock bb, SimpleLocalScopeVariable v) {
+        result = min(int r, RefKind k |
+          r = refRank(bb, _, v, k) and
+          k != Write(false)
+          |
+          r
+        )
+      }
+
+      predicate liveAtEntry(PreBasicBlock bb, SimpleLocalScopeVariable v) {
+        refRank(bb, _, v, Read()) = firstReadOrCertainWrite(bb, v)
+        or
+        not exists(firstReadOrCertainWrite(bb, v)) and
+        liveAtExit(bb, v)
+      }
+
+      private predicate liveAtExit(PreBasicBlock bb, SimpleLocalScopeVariable v) {
+        liveAtEntry(bb.getASuccessor(), v)
+      }
+
+      predicate assignableDefAtLive(PreBasicBlocks::PreBasicBlock bb, int i, AssignableDefinition def, SimpleLocalScopeVariable v) {
+        assignableDefAt(bb, i, def, v) and
+        exists(int rnk |
+          rnk = refRank(bb, i, v, Write(_)) |
+          rnk + 1 = refRank(bb, _, v, Read())
+          or
+          rnk = max(refRank(bb, _, v, _)) and
+          liveAtExit(bb, v)
+        )
+      }
+
       predicate defAt(PreBasicBlock bb, int i, Definition def, SimpleLocalScopeVariable v) {
         def = TExplicitPreSsaDef(bb, i, _, v)
         or
         def = TPhiPreSsaDef(bb, v) and i = -1
       }
 
-      private predicate readAt(PreBasicBlock bb, int i, LocalScopeVariableRead read, SimpleLocalScopeVariable v) {
-        read = bb.getElement(i) and
-        read.getTarget() = v
-      }
+      private newtype SsaRefKind = SsaRead() or SsaDef()
 
       private predicate ssaRef(PreBasicBlock bb, int i, SimpleLocalScopeVariable v, SsaRefKind k) {
         readAt(bb, i, _, v) and
@@ -2756,6 +2837,22 @@ module ControlFlow {
           readAt(bb2, i2, read2, v)
         )
       }
+
+      predicate ssaDefReachesEndOfBlock(PreBasicBlock bb, Definition def, SimpleLocalScopeVariable v) {
+        liveAtExit(bb, v) and
+        (
+          exists(int last |
+            last = max(ssaRefRank(bb, _, v, _)) |
+            defReachesRank(bb, def, v, last)
+          )
+          or
+          exists(PreBasicBlock idom |
+            idom.immediatelyDominates(bb) |
+            ssaDefReachesEndOfBlock(idom, def, v) and
+            not exists(ssaRefRank(bb, _, v, SsaDef()))
+          )
+        )
+      }
     }
 
     /**
@@ -3847,10 +3944,11 @@ module ControlFlow {
       newtype TPreSsaDef =
         TExplicitPreSsaDef(PreBasicBlocks::PreBasicBlock bb, int i, AssignableDefinition def, LocalScopeVariable v) {
           Guards::Internal::CachedWithCFG::forceCachingInSameStage() and
-          PreSsa::assignableDefAt(bb, i, def, v)
+          PreSsa::assignableDefAtLive(bb, i, def, v)
         }
         or
         TPhiPreSsaDef(PreBasicBlocks::PreBasicBlock bb, LocalScopeVariable v) {
+          PreSsa::liveAtEntry(bb, v) and
           exists(PreBasicBlocks::PreBasicBlock def |
             def.inDominanceFrontier(bb) |
             PreSsa::defAt(def, _, _, v)

csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.expected

@@ -0,0 +1,3 @@
+defReadInconsistency
+readReadInconsistency
+phiInconsistency

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

@@ -1,11 +1,13 @@
 import csharp
 import ControlFlow::Internal
 
-predicate defReadInconsistency(AssignableRead ar, Expr e, boolean b) {
+query
+predicate defReadInconsistency(AssignableRead ar, Expr e, PreSsa::SimpleLocalScopeVariable v, boolean b) {
   exists(AssignableDefinition def |
     e = def.getExpr() |
     b = true and
     exists(PreSsa::Definition ssaDef |
+      ssaDef.getVariable() = v |
       PreSsa::firstReadSameVar(ssaDef, ar) and
       ssaDef.getDefinition() = def and
       not exists(Ssa::ExplicitDefinition edef |
@@ -18,7 +20,7 @@ predicate defReadInconsistency(AssignableRead ar, Expr e, boolean b) {
     exists(Ssa::ExplicitDefinition edef |
       edef.getADefinition() = def and
       edef.getAFirstRead() = ar and
-      def.getTarget() instanceof PreSsa::SimpleLocalScopeVariable and
+      def.getTarget() = v and
       not exists(PreSsa::Definition ssaDef |
         PreSsa::firstReadSameVar(ssaDef, ar) and
         ssaDef.getDefinition() = def
@@ -27,22 +29,48 @@ predicate defReadInconsistency(AssignableRead ar, Expr e, boolean b) {
   )
 }
 
-predicate readReadInconsistency(LocalScopeVariableRead read1, LocalScopeVariableRead read2, boolean b) {
+query
+predicate readReadInconsistency(LocalScopeVariableRead read1, LocalScopeVariableRead read2, PreSsa::SimpleLocalScopeVariable v, boolean b) {
   b = true and
+  v = read1.getTarget() and
   PreSsa::adjacentReadPairSameVar(read1, read2) and
   not Ssa::Internal::adjacentReadPairSameVar(read1, read2)
   or
   b = false and
+  v = read1.getTarget() and
   Ssa::Internal::adjacentReadPairSameVar(read1, read2) and
   read1.getTarget() instanceof PreSsa::SimpleLocalScopeVariable and
   not PreSsa::adjacentReadPairSameVar(read1, read2)
 }
 
-from Element e1, Element e2, boolean b, string s
-where
-  defReadInconsistency(e1, e2, b) and
-  s = "def-read inconsistency (" + b + ")"
-  or
-  readReadInconsistency(e1, e2, b) and
-  s = "read-read inconsistency (" + b + ")"
-select e1, e2, s
+query
+predicate phiInconsistency(ControlFlowElement cfe, Expr e, PreSsa::SimpleLocalScopeVariable v, boolean b) {
+  exists(AssignableDefinition adef |
+    e = adef.getExpr() |
+    b = true and
+    exists(PreSsa::Definition def |
+      v = def.getVariable() |
+      adef = def.getAPhiInput+().getDefinition() and
+      cfe = def.getBasicBlock().getFirstElement() and
+      not exists(Ssa::PhiNode phi, ControlFlow::BasicBlock bb, Ssa::ExplicitDefinition edef |
+        edef = phi.getAnUltimateDefinition() |
+        edef.getADefinition() = adef and
+        phi.definesAt(bb, _) and
+        cfe = bb.getFirstNode().getElement()
+      )
+    )
+    or
+    b = false and
+    exists(Ssa::PhiNode phi, ControlFlow::BasicBlock bb, Ssa::ExplicitDefinition edef |
+      v = phi.getSourceVariable().getAssignable() |
+      edef = phi.getAnUltimateDefinition() and
+      edef.getADefinition() = adef and
+      phi.definesAt(bb, _) and
+      cfe = bb.getFirstNode().getElement() and
+      not exists(PreSsa::Definition def |
+        adef = def.getAPhiInput+().getDefinition() and
+        cfe = def.getBasicBlock().getFirstElement()
+      )
+    )
+  )
+}