C#/Java: Range analysis: use ranked phi nodes

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

@@ -111,13 +111,6 @@ private predicate evenlyDivisibleExpr(Expr e, int factor) {
   )
 }
 
-/**
- * Holds if `rix` is the number of input edges to `phi`.
- */
-private predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
-  rix = max(int r | rankedPhiInput(phi, _, _, r))
-}
-
 /**
  * Gets the remainder of `val` modulo `mod`.
  *

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

@@ -43,37 +43,4 @@ module Private {
   predicate ssaUpdateStep = RU::ssaUpdateStep/3;
 
   Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode() }
-
-  private class PhiInputEdgeBlock extends BasicBlock {
-    PhiInputEdgeBlock() { this = any(SsaReadPositionPhiInputEdge edge).getOrigBlock() }
-  }
-
-  int getId(PhiInputEdgeBlock bb) {
-    exists(CfgImpl::ControlFlowTree::Range_ t | CfgImpl::ControlFlowTree::idOf(t, result) |
-      t = bb.getFirstNode().getElement()
-      or
-      t = bb.(CS::ControlFlow::BasicBlocks::EntryBlock).getCallable()
-    )
-  }
-
-  private string getSplitString(PhiInputEdgeBlock bb) {
-    result = bb.getFirstNode().(CS::ControlFlow::Nodes::ElementNode).getSplitsString()
-    or
-    not exists(bb.getFirstNode().(CS::ControlFlow::Nodes::ElementNode).getSplitsString()) and
-    result = ""
-  }
-
-  /**
-   * Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
-   * in an arbitrary 1-based numbering of the input edges to `phi`.
-   */
-  predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
-    edge.phiInput(phi, inp) and
-    edge =
-      rank[r](SsaReadPositionPhiInputEdge e |
-        e.phiInput(phi, _)
-      |
-        e order by getId(e.getOrigBlock()), getSplitString(e.getOrigBlock())
-      )
-  }
 }

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

@@ -3,6 +3,7 @@
  */
 
 private import SsaReadPositionSpecific
+import SsaReadPositionSpecific::Public
 
 private newtype TSsaReadPosition =
   TSsaReadPositionBlock(BasicBlock bb) { bb = getAReadBasicBlock(_) } or
@@ -55,3 +56,10 @@ class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiIn
 
   override string toString() { result = "edge" }
 }
+
+/**
+ * Holds if `rix` is the number of input edges to `phi`.
+ */
+predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
+  rix = max(int r | rankedPhiInput(phi, _, _, r))
+}

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

@@ -3,6 +3,8 @@
  */
 
 private import csharp
+private import SsaReadPositionCommon
+private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl as CfgImpl
 
 class SsaVariable = Ssa::Definition;
 
@@ -14,3 +16,41 @@ class BasicBlock = ControlFlow::BasicBlock;
 BasicBlock getAReadBasicBlock(SsaVariable v) {
   result = v.getARead().getAControlFlowNode().getBasicBlock()
 }
+
+private class PhiInputEdgeBlock extends BasicBlock {
+  PhiInputEdgeBlock() { this = any(SsaReadPositionPhiInputEdge edge).getOrigBlock() }
+}
+
+private int getId(PhiInputEdgeBlock bb) {
+  exists(CfgImpl::ControlFlowTree::Range_ t | CfgImpl::ControlFlowTree::idOf(t, result) |
+    t = bb.getFirstNode().getElement()
+    or
+    t = bb.(ControlFlow::BasicBlocks::EntryBlock).getCallable()
+  )
+}
+
+private string getSplitString(PhiInputEdgeBlock bb) {
+  result = bb.getFirstNode().(ControlFlow::Nodes::ElementNode).getSplitsString()
+  or
+  not exists(bb.getFirstNode().(ControlFlow::Nodes::ElementNode).getSplitsString()) and
+  result = ""
+}
+
+/**
+ * Declarations to be exposed to users of SsaReadPositionCommon.
+ */
+module Public {
+  /**
+   * Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
+   * in an arbitrary 1-based numbering of the input edges to `phi`.
+   */
+  predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
+    edge.phiInput(phi, inp) and
+    edge =
+      rank[r](SsaReadPositionPhiInputEdge e |
+        e.phiInput(phi, _)
+      |
+        e order by getId(e.getOrigBlock()), getSplitString(e.getOrigBlock())
+      )
+  }
+}

java/ql/lib/semmle/code/java/dataflow/ModulusAnalysis.qll

@@ -111,13 +111,6 @@ private predicate evenlyDivisibleExpr(Expr e, int factor) {
   )
 }
 
-/**
- * Holds if `rix` is the number of input edges to `phi`.
- */
-private predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
-  rix = max(int r | rankedPhiInput(phi, _, _, r))
-}
-
 /**
  * Gets the remainder of `val` modulo `mod`.
  *

java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll

@@ -725,6 +725,26 @@ private predicate boundedPhiCandValidForEdge(
   )
 }
 
+/**
+ * Holds if `b + delta` is a valid bound for `phi`'s `rix`th input edge.
+ * - `upper = true`  : `phi <= b + delta`
+ * - `upper = false` : `phi >= b + delta`
+ */
+private predicate boundedPhiStep(
+  SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
+  Reason reason, int rix
+) {
+  exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge |
+    rankedPhiInput(phi, inp, edge, rix) and
+    boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge) and
+    (
+      rix = 1
+      or
+      boundedPhiStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, rix - 1)
+    )
+  )
+}
+
 /**
  * Holds if `b + delta` is a valid bound for `phi`.
  * - `upper = true`  : `phi <= b + delta`
@@ -734,8 +754,9 @@ private predicate boundedPhi(
   SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
   Reason reason
 ) {
-  forex(SsaVariable inp, SsaReadPositionPhiInputEdge edge | edge.phiInput(phi, inp) |
-    boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
+  exists(int r |
+    boundedPhiStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, r) and
+    maxPhiInputRank(phi, r)
   )
 }
 

java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll

@@ -111,24 +111,4 @@ module Private {
   predicate ssaUpdateStep = RU::ssaUpdateStep/3;
 
   Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode() }
-
-  private predicate id(BasicBlock x, BasicBlock y) { x = y }
-
-  private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
-
-  private int getId(BasicBlock bb) { idOf(bb, result) }
-
-  /**
-   * Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
-   * in an arbitrary 1-based numbering of the input edges to `phi`.
-   */
-  predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
-    edge.phiInput(phi, inp) and
-    edge =
-      rank[r](SsaReadPositionPhiInputEdge e |
-        e.phiInput(phi, _)
-      |
-        e order by getId(e.getOrigBlock())
-      )
-  }
 }

java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll

@@ -3,6 +3,7 @@
  */
 
 private import SsaReadPositionSpecific
+import SsaReadPositionSpecific::Public
 
 private newtype TSsaReadPosition =
   TSsaReadPositionBlock(BasicBlock bb) { bb = getAReadBasicBlock(_) } or
@@ -55,3 +56,10 @@ class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiIn
 
   override string toString() { result = "edge" }
 }
+
+/**
+ * Holds if `rix` is the number of input edges to `phi`.
+ */
+predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
+  rix = max(int r | rankedPhiInput(phi, _, _, r))
+}

java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll

@@ -4,6 +4,7 @@
 
 private import semmle.code.java.dataflow.SSA as Ssa
 private import semmle.code.java.controlflow.BasicBlocks as BB
+private import SsaReadPositionCommon
 
 class SsaVariable = Ssa::SsaVariable;
 
@@ -13,3 +14,28 @@ class BasicBlock = BB::BasicBlock;
 
 /** Gets a basic block in which SSA variable `v` is read. */
 BasicBlock getAReadBasicBlock(SsaVariable v) { result = v.getAUse().getBasicBlock() }
+
+private predicate id(BasicBlock x, BasicBlock y) { x = y }
+
+private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
+
+private int getId(BasicBlock bb) { idOf(bb, result) }
+
+/**
+ * Declarations to be exposed to users of SsaReadPositionCommon
+ */
+module Public {
+  /**
+   * Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
+   * in an arbitrary 1-based numbering of the input edges to `phi`.
+   */
+  predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
+    edge.phiInput(phi, inp) and
+    edge =
+      rank[r](SsaReadPositionPhiInputEdge e |
+        e.phiInput(phi, _)
+      |
+        e order by getId(e.getOrigBlock())
+      )
+  }
+}