Merge pull request #13035 from MathiasVP/ranked-phi-hack-for-bounded-phi

C++: Work around poor codegen for `forex` in IR-based range analysis

Author: Robert Marsh

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ModulusAnalysis.qll

@@ -120,13 +120,6 @@ module ModulusAnalysis<DeltaSig D, BoundSig<D> Bounds, UtilSig<D> U> {
     )
   }
 
-  /**
-   * Holds if `rix` is the number of input edges to `phi`.
-   */
-  private predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
-    rix = max(int r | rankedPhiInput(phi, _, _, r))
-  }
-
   /**
    * Gets the remainder of `val` modulo `mod`.
    *
@@ -322,20 +315,4 @@ module ModulusAnalysis<DeltaSig D, BoundSig<D> Bounds, UtilSig<D> U> {
       semExprModulus(rarg, b, val, mod) and isLeft = false
     )
   }
-
-  /**
-   * 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`.
-   */
-  private predicate rankedPhiInput(
-    SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
-  ) {
-    edge.phiInput(phi, inp) and
-    edge =
-      rank[r](SemSsaReadPositionPhiInputEdge e |
-        e.phiInput(phi, _)
-      |
-        e order by e.getOrigBlock().getUniqueId()
-      )
-  }
 }

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll

@@ -877,6 +877,22 @@ module RangeStage<
     )
   }
 
+  pragma[assume_small_delta]
+  pragma[nomagic]
+  private predicate boundedPhiRankStep(
+    SemSsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
+    D::Delta origdelta, SemReason reason, int rix
+  ) {
+    exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
+      Utils::rankedPhiInput(phi, inp, edge, rix) and
+      boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
+    |
+      if rix = 1
+      then any()
+      else boundedPhiRankStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, rix - 1)
+    )
+  }
+
   /**
    * Holds if `b + delta` is a valid bound for `phi`.
    * - `upper = true`  : `phi <= b + delta`
@@ -886,8 +902,9 @@ module RangeStage<
     SemSsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
     D::Delta origdelta, SemReason reason
   ) {
-    forex(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge | edge.phiInput(phi, inp) |
-      boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
+    exists(int r |
+      Utils::maxPhiInputRank(phi, r) and
+      boundedPhiRankStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, r)
     )
   }
 

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll

@@ -138,3 +138,26 @@ module RangeUtil<Range::DeltaSig D, Range::LangSig<D> Lang> implements Range::Ut
     not exists(Lang::getAlternateTypeForSsaVariable(var)) and result = var.getType()
   }
 }
+
+/**
+ * Holds if `rix` is the number of input edges to `phi`.
+ */
+predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
+  rix = max(int r | rankedPhiInput(phi, _, _, r))
+}
+
+/**
+ * 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(
+  SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
+) {
+  edge.phiInput(phi, inp) and
+  edge =
+    rank[r](SemSsaReadPositionPhiInputEdge e |
+      e.phiInput(phi, _)
+    |
+      e order by e.getOrigBlock().getUniqueId()
+    )
+}