From 73671b6da3ac517159c9d3235e91cdfb5bea3d27 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Wed, 6 Dec 2023 15:55:26 +0100
Subject: [PATCH] Rangeanalysis: Refactor base bounds.

---
 .../codeql/rangeanalysis/RangeAnalysis.qll    | 37 +++++++++----------
 1 file changed, 18 insertions(+), 19 deletions(-)

diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
index 55c0e3b432e..9162d4254f2 100644
--- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
+++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
@@ -995,15 +995,23 @@ module RangeStage<
   }
 
   /**
-   * Holds if `e` has an upper (for `upper = true`) or lower
-   * (for `upper = false`) bound of `b`.
+   * Holds if `e` has an intrinsic upper (for `upper = true`) or lower
+   * (for `upper = false`) bound of `b + delta` as a base case for range analysis.
    */
-  private predicate baseBound(Sem::Expr e, D::Delta b, boolean upper) {
-    hasConstantBound(e, b, upper)
-    or
-    upper = false and
-    b = D::fromInt(0) and
-    semPositive(e.(Sem::BitAndExpr).getAnOperand())
+  private predicate baseBound(Sem::Expr e, SemBound b, D::Delta delta, boolean upper) {
+    includeBound(b) and
+    (
+      e = b.getExpr(delta) and
+      upper = [true, false]
+      or
+      hasConstantBound(e, delta, upper) and
+      b instanceof SemZeroBound
+      or
+      upper = false and
+      delta = D::fromInt(0) and
+      semPositive(e.(Sem::BitAndExpr).getAnOperand()) and
+      b instanceof SemZeroBound
+    )
   }
 
   /**
@@ -1129,19 +1137,10 @@ module RangeStage<
   ) {
     not ignoreExprBound(e) and
     (
-      e = b.getExpr(delta) and
-      (upper = true or upper = false) and
+      baseBound(e, b, delta, upper) and
       fromBackEdge = false and
       origdelta = delta and
-      reason = TSemNoReason() and
-      includeBound(b)
-      or
-      baseBound(e, delta, upper) and
-      b instanceof SemZeroBound and
-      fromBackEdge = false and
-      origdelta = delta and
-      reason = TSemNoReason() and
-      includeBound(b)
+      reason = TSemNoReason()
       or
       exists(Sem::SsaVariable v, SsaReadPositionBlock bb |
         boundedSsa(v, b, delta, bb, upper, fromBackEdge, origdelta, reason) and