From aed830cf1b7775c3ca786e2c2d66f5bfd3a5d0b7 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Thu, 5 Oct 2023 13:42:09 +0200
Subject: [PATCH 01/14] Rangeanalysis: Make new qlpack

---
 shared/rangeanalysis/change-notes/2023-10-05-initial.md | 4 ++++
 shared/rangeanalysis/qlpack.yml                         | 7 +++++++
 2 files changed, 11 insertions(+)
 create mode 100644 shared/rangeanalysis/change-notes/2023-10-05-initial.md
 create mode 100644 shared/rangeanalysis/qlpack.yml

diff --git a/shared/rangeanalysis/change-notes/2023-10-05-initial.md b/shared/rangeanalysis/change-notes/2023-10-05-initial.md
new file mode 100644
index 000000000000..910b6962a932
--- /dev/null
+++ b/shared/rangeanalysis/change-notes/2023-10-05-initial.md
@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* Initial release. Moves the range analysis library into its own qlpack.
diff --git a/shared/rangeanalysis/qlpack.yml b/shared/rangeanalysis/qlpack.yml
new file mode 100644
index 000000000000..fbe05924c5a6
--- /dev/null
+++ b/shared/rangeanalysis/qlpack.yml
@@ -0,0 +1,7 @@
+name: codeql/rangeanalysis
+version: 0.0.1-dev
+groups: shared
+library: true
+dependencies:
+  codeql/util: ${workspace}
+warnOnImplicitThis: true

From 169ba037782fea40c936bb1ead5f7eb7eae5aba3 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Thu, 5 Oct 2023 13:42:44 +0200
Subject: [PATCH 02/14] Rangeanalysis: Copy C++ version verbatim.

---
 .../rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll          | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll => shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll (100%)

diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
similarity index 100%
rename from cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll
rename to shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

From 38274db205343942a231c488cd8421eefdc5e75f Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Mon, 9 Oct 2023 12:54:33 +0200
Subject: [PATCH 03/14] Rangeanalysis: Parameterise library.

---
 .../semantic/analysis/SignAnalysisCommon.qll  |  12 +
 .../codeql/rangeanalysis/RangeAnalysis.qll    | 529 +++++++++++-------
 2 files changed, 343 insertions(+), 198 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
index 9abcdc842abb..0de6c1aca6e8 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
@@ -507,4 +507,16 @@ module SignAnalysis<DeltaSig D, UtilSig<D> Utils> {
     not semExprSign(e) = TPos() and
     not semExprSign(e) = TZero()
   }
+
+  /**
+   * Holds if `e` may have positive values. This does not rule out the
+   * possibilty for negative values.
+   */
+  predicate semMayBePositive(SemExpr e) { semExprSign(e) = TPos() }
+
+  /**
+   * Holds if `e` may have negative values. This does not rule out the
+   * possibilty for positive values.
+   */
+  predicate semMayBeNegative(SemExpr e) { semExprSign(e) = TNeg() }
 }
diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
index 806dfffbec93..1f462c94f549 100644
--- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
+++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
@@ -63,33 +63,160 @@
  * back-edge as a precise bound might require traversing a loop once).
  */
 
-private import RangeUtils as Utils
-private import SignAnalysisCommon
-private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.ModulusAnalysis
-import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExpr
-import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticSSA
-import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticGuard
-import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticCFG
-import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticType
-import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticOpcode
-private import ConstantAnalysis
-private import Sign
-import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticLocation
+private import codeql.util.Location
 
-/**
- * Holds if `typ` is a small integral type with the given lower and upper bounds.
- */
-private predicate typeBound(SemIntegerType typ, float lowerbound, float upperbound) {
-  exists(int bitSize | bitSize = typ.getByteSize() * 8 |
-    if typ.isSigned()
-    then (
-      upperbound = 2.pow(bitSize - 1) - 1 and
-      lowerbound = -upperbound - 1
-    ) else (
-      lowerbound = 0 and
-      upperbound = 2.pow(bitSize) - 1
-    )
-  )
+signature module Semantic {
+  class Expr {
+    string toString();
+
+    BasicBlock getBasicBlock();
+  }
+
+  class ConstantIntegerExpr extends Expr {
+    int getIntValue();
+  }
+
+  class BinaryExpr extends Expr {
+    Expr getLeftOperand();
+
+    Expr getRightOperand();
+
+    Expr getAnOperand();
+
+    predicate hasOperands(Expr e1, Expr e2);
+  }
+
+  class AddExpr extends BinaryExpr;
+
+  class SubExpr extends BinaryExpr;
+
+  class MulExpr extends BinaryExpr;
+
+  class DivExpr extends BinaryExpr;
+
+  class RemExpr extends BinaryExpr;
+
+  class BitAndExpr extends BinaryExpr;
+
+  class BitOrExpr extends BinaryExpr;
+
+  class ShiftLeftExpr extends BinaryExpr;
+
+  class ShiftRightExpr extends BinaryExpr;
+
+  class ShiftRightUnsignedExpr extends BinaryExpr;
+
+  class RelationalExpr extends Expr {
+    Expr getLesserOperand();
+
+    Expr getGreaterOperand();
+
+    predicate isStrict();
+  }
+
+  class UnaryExpr extends Expr {
+    Expr getOperand();
+  }
+
+  class ConvertExpr extends UnaryExpr;
+
+  class BoxExpr extends UnaryExpr;
+
+  class UnboxExpr extends UnaryExpr;
+
+  class NegateExpr extends UnaryExpr;
+
+  class AddOneExpr extends UnaryExpr;
+
+  class SubOneExpr extends UnaryExpr;
+
+  class ConditionalExpr extends Expr {
+    Expr getBranchExpr(boolean branch);
+  }
+
+  class BasicBlock;
+
+  class Guard {
+    string toString();
+
+    BasicBlock getBasicBlock();
+
+    Expr asExpr();
+
+    predicate directlyControls(BasicBlock controlled, boolean branch);
+  }
+
+  predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2);
+
+  predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue);
+
+  class Type;
+
+  class IntegerType extends Type {
+    predicate isSigned();
+
+    int getByteSize();
+  }
+
+  class FloatingPointType extends Type;
+
+  class AddressType extends Type;
+
+  class SsaVariable {
+    Expr getAUse();
+  }
+
+  class SsaPhiNode extends SsaVariable;
+
+  class SsaExplicitUpdate extends SsaVariable;
+
+  class SsaReadPosition {
+    predicate hasReadOfVar(SsaVariable v);
+  }
+
+  class SsaReadPositionPhiInputEdge extends SsaReadPosition {
+    predicate phiInput(SsaPhiNode phi, SsaVariable inp);
+  }
+
+  class SsaReadPositionBlock extends SsaReadPosition {
+    BasicBlock getBlock();
+  }
+
+  predicate backEdge(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge);
+
+  predicate conversionCannotOverflow(Type fromType, Type toType);
+}
+
+signature module SignAnalysisSig<Semantic Sem> {
+  /** Holds if `e` can be positive and cannot be negative. */
+  predicate semPositive(Sem::Expr e);
+
+  /** Holds if `e` can be negative and cannot be positive. */
+  predicate semNegative(Sem::Expr e);
+
+  /** Holds if `e` is strictly positive. */
+  predicate semStrictlyPositive(Sem::Expr e);
+
+  /** Holds if `e` is strictly negative. */
+  predicate semStrictlyNegative(Sem::Expr e);
+
+  /**
+   * Holds if `e` may have positive values. This does not rule out the
+   * possibilty for negative values.
+   */
+  predicate semMayBePositive(Sem::Expr e);
+
+  /**
+   * Holds if `e` may have negative values. This does not rule out the
+   * possibilty for positive values.
+   */
+  predicate semMayBeNegative(Sem::Expr e);
+}
+
+signature module ModulusAnalysisSig<Semantic Sem> {
+  class ModBound;
+
+  predicate semExprModulus(Sem::Expr e, ModBound b, int val, int mod);
 }
 
 signature module DeltaSig {
@@ -112,24 +239,24 @@ signature module DeltaSig {
   Delta fromFloat(float f);
 }
 
-signature module LangSig<DeltaSig D> {
+signature module LangSig<Semantic Sem, DeltaSig D> {
   /**
    * Holds if the specified expression should be excluded from the result of `ssaRead()`.
    *
    * This predicate is to keep the results identical to the original Java implementation. It should be
    * removed once we have the new implementation matching the old results exactly.
    */
-  predicate ignoreSsaReadCopy(SemExpr e);
+  predicate ignoreSsaReadCopy(Sem::Expr e);
 
   /**
    * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
    */
-  predicate hasConstantBound(SemExpr e, D::Delta bound, boolean upper);
+  predicate hasConstantBound(Sem::Expr e, D::Delta bound, boolean upper);
 
   /**
    * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).
    */
-  predicate hasBound(SemExpr e, SemExpr bound, D::Delta delta, boolean upper);
+  predicate hasBound(Sem::Expr e, Sem::Expr bound, D::Delta delta, boolean upper);
 
   /**
    * Ignore the bound on this expression.
@@ -137,7 +264,7 @@ signature module LangSig<DeltaSig D> {
    * This predicate is to keep the results identical to the original Java implementation. It should be
    * removed once we have the new implementation matching the old results exactly.
    */
-  predicate ignoreExprBound(SemExpr e);
+  predicate ignoreExprBound(Sem::Expr e);
 
   /**
    * Ignore any inferred zero lower bound on this expression.
@@ -145,7 +272,7 @@ signature module LangSig<DeltaSig D> {
    * This predicate is to keep the results identical to the original Java implementation. It should be
    * removed once we have the new implementation matching the old results exactly.
    */
-  predicate ignoreZeroLowerBound(SemExpr e);
+  predicate ignoreZeroLowerBound(Sem::Expr e);
 
   /**
    * Holds if the specified expression should be excluded from the result of `ssaRead()`.
@@ -153,7 +280,7 @@ signature module LangSig<DeltaSig D> {
    * This predicate is to keep the results identical to the original Java implementation. It should be
    * removed once we have the new implementation matching the old results exactly.
    */
-  predicate ignoreSsaReadArithmeticExpr(SemExpr e);
+  predicate ignoreSsaReadArithmeticExpr(Sem::Expr e);
 
   /**
    * Holds if the specified variable should be excluded from the result of `ssaRead()`.
@@ -161,7 +288,7 @@ signature module LangSig<DeltaSig D> {
    * This predicate is to keep the results identical to the original Java implementation. It should be
    * removed once we have the new implementation matching the old results exactly.
    */
-  predicate ignoreSsaReadAssignment(SemSsaVariable v);
+  predicate ignoreSsaReadAssignment(Sem::SsaVariable v);
 
   /**
    * Adds additional results to `ssaRead()` that are specific to Java.
@@ -171,12 +298,12 @@ signature module LangSig<DeltaSig D> {
    * old one, we should remove this predicate and propagate deltas for all similar patterns, whether
    * or not they come from a post-increment/decrement expression.
    */
-  SemExpr specificSsaRead(SemSsaVariable v, D::Delta delta);
+  Sem::Expr specificSsaRead(Sem::SsaVariable v, D::Delta delta);
 
   /**
    * Holds if the value of `dest` is known to be `src + delta`.
    */
-  predicate additionalValueFlowStep(SemExpr dest, SemExpr src, D::Delta delta);
+  predicate additionalValueFlowStep(Sem::Expr dest, Sem::Expr src, D::Delta delta);
 
   /**
    * Gets the type that range analysis should use to track the result of the specified expression,
@@ -185,7 +312,7 @@ signature module LangSig<DeltaSig D> {
    * This predicate is commonly used in languages that support immutable "boxed" types that are
    * actually references but whose values can be tracked as the type contained in the box.
    */
-  SemType getAlternateType(SemExpr e);
+  Sem::Type getAlternateType(Sem::Expr e);
 
   /**
    * Gets the type that range analysis should use to track the result of the specified source
@@ -194,19 +321,19 @@ signature module LangSig<DeltaSig D> {
    * This predicate is commonly used in languages that support immutable "boxed" types that are
    * actually references but whose values can be tracked as the type contained in the box.
    */
-  SemType getAlternateTypeForSsaVariable(SemSsaVariable var);
+  Sem::Type getAlternateTypeForSsaVariable(Sem::SsaVariable var);
 }
 
-signature module UtilSig<DeltaSig DeltaParam> {
-  SemExpr semSsaRead(SemSsaVariable v, DeltaParam::Delta delta);
+signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> {
+  Sem::Expr semSsaRead(Sem::SsaVariable v, DeltaParam::Delta delta);
 
-  SemGuard semEqFlowCond(
-    SemSsaVariable v, SemExpr e, DeltaParam::Delta delta, boolean isEq, boolean testIsTrue
+  Sem::Guard semEqFlowCond(
+    Sem::SsaVariable v, Sem::Expr e, DeltaParam::Delta delta, boolean isEq, boolean testIsTrue
   );
 
-  predicate semSsaUpdateStep(SemSsaExplicitUpdate v, SemExpr e, DeltaParam::Delta delta);
+  predicate semSsaUpdateStep(Sem::SsaExplicitUpdate v, Sem::Expr e, DeltaParam::Delta delta);
 
-  predicate semValueFlowStep(SemExpr e2, SemExpr e1, DeltaParam::Delta delta);
+  predicate semValueFlowStep(Sem::Expr e2, Sem::Expr e1, DeltaParam::Delta delta);
 
   /**
    * Gets the type used to track the specified source variable's range information.
@@ -214,7 +341,7 @@ signature module UtilSig<DeltaSig DeltaParam> {
    * Usually, this just `e.getType()`, but the language can override this to track immutable boxed
    * primitive types as the underlying primitive type.
    */
-  SemType getTrackedTypeForSsaVariable(SemSsaVariable var);
+  Sem::Type getTrackedTypeForSsaVariable(Sem::SsaVariable var);
 
   /**
    * Gets the type used to track the specified expression's range information.
@@ -222,54 +349,86 @@ signature module UtilSig<DeltaSig DeltaParam> {
    * Usually, this just `e.getSemType()`, but the language can override this to track immutable boxed
    * primitive types as the underlying primitive type.
    */
-  SemType getTrackedType(SemExpr e);
+  Sem::Type getTrackedType(Sem::Expr e);
+
+  /**
+   * 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(
+    Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, int r
+  );
+
+  /**
+   * Holds if `rix` is the number of input edges to `phi`.
+   */
+  predicate maxPhiInputRank(Sem::SsaPhiNode phi, int rix);
 }
 
-signature module BoundSig<DeltaSig D> {
+signature module BoundSig<LocationSig Location, Semantic Sem, DeltaSig D> {
   class SemBound {
     string toString();
 
-    SemLocation getLocation();
+    Location getLocation();
 
-    SemExpr getExpr(D::Delta delta);
+    Sem::Expr getExpr(D::Delta delta);
   }
 
   class SemZeroBound extends SemBound;
 
   class SemSsaBound extends SemBound {
-    SemSsaVariable getAVariable();
+    Sem::SsaVariable getAVariable();
   }
 }
 
-signature module OverflowSig<DeltaSig D> {
-  predicate semExprDoesNotOverflow(boolean positively, SemExpr expr);
+signature module OverflowSig<Semantic Sem, DeltaSig D> {
+  predicate semExprDoesNotOverflow(boolean positively, Sem::Expr expr);
 }
 
 module RangeStage<
-  DeltaSig D, BoundSig<D> Bounds, OverflowSig<D> OverflowParam, LangSig<D> LangParam,
-  UtilSig<D> UtilParam>
+  LocationSig Location, Semantic Sem, DeltaSig D, BoundSig<Location, Sem, D> Bounds,
+  OverflowSig<Sem, D> OverflowParam, LangSig<Sem, D> LangParam, SignAnalysisSig<Sem> SignAnalysis,
+  ModulusAnalysisSig<Sem> ModulusAnalysis, UtilSig<Sem, D> UtilParam>
 {
   private import Bounds
   private import LangParam
   private import UtilParam
   private import D
   private import OverflowParam
+  private import SignAnalysis
+  private import ModulusAnalysis
 
   /**
    * An expression that does conversion, boxing, or unboxing
    */
-  private class ConvertOrBoxExpr instanceof SemUnaryExpr {
+  private class ConvertOrBoxExpr instanceof Sem::UnaryExpr {
     ConvertOrBoxExpr() {
-      this instanceof SemConvertExpr
+      this instanceof Sem::ConvertExpr
       or
-      this instanceof SemBoxExpr
+      this instanceof Sem::BoxExpr
       or
-      this instanceof SemUnboxExpr
+      this instanceof Sem::UnboxExpr
     }
 
     string toString() { result = super.toString() }
 
-    SemExpr getOperand() { result = super.getOperand() }
+    Sem::Expr getOperand() { result = super.getOperand() }
+  }
+
+  /**
+   * Holds if `typ` is a small integral type with the given lower and upper bounds.
+   */
+  private predicate typeBound(Sem::IntegerType typ, float lowerbound, float upperbound) {
+    exists(int bitSize | bitSize = typ.getByteSize() * 8 |
+      if typ.isSigned()
+      then (
+        upperbound = 2.pow(bitSize - 1) - 1 and
+        lowerbound = -upperbound - 1
+      ) else (
+        lowerbound = 0 and
+        upperbound = 2.pow(bitSize) - 1
+      )
+    )
   }
 
   /**
@@ -277,7 +436,7 @@ module RangeStage<
    */
   private class SafeCastExpr extends ConvertOrBoxExpr {
     SafeCastExpr() {
-      conversionCannotOverflow(getTrackedType(pragma[only_bind_into](this.getOperand())),
+      Sem::conversionCannotOverflow(getTrackedType(pragma[only_bind_into](this.getOperand())),
         pragma[only_bind_out](getTrackedType(this)))
     }
   }
@@ -298,14 +457,6 @@ module RangeStage<
     float getUpperBound() { typeBound(getTrackedType(this), _, result) }
   }
 
-  private module SignAnalysisInstantiated = SignAnalysis<D, UtilParam>; // TODO: will this cause reevaluation if it's instantiated with the same DeltaSig and UtilParam multiple times?
-
-  private import SignAnalysisInstantiated
-
-  private module ModulusAnalysisInstantiated = ModulusAnalysis<D, Bounds, UtilParam>; // TODO: will this cause reevaluation if it's instantiated with the same DeltaSig and UtilParam multiple times?
-
-  private import ModulusAnalysisInstantiated
-
   cached
   private module RangeAnalysisCache {
     cached
@@ -320,7 +471,7 @@ module RangeStage<
        * condition.
        */
       cached
-      predicate semBounded(SemExpr e, SemBound b, D::Delta delta, boolean upper, SemReason reason) {
+      predicate semBounded(Sem::Expr e, SemBound b, D::Delta delta, boolean upper, SemReason reason) {
         bounded(e, b, delta, upper, _, _, reason) and
         bestBound(e, b, delta, upper)
       }
@@ -330,7 +481,7 @@ module RangeStage<
      * Holds if `guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)`.
      */
     cached
-    predicate possibleReason(SemGuard guard) {
+    predicate possibleReason(Sem::Guard guard) {
       guard = boundFlowCond(_, _, _, _, _) or guard = semEqFlowCond(_, _, _, _, _)
     }
   }
@@ -343,7 +494,7 @@ module RangeStage<
    * - `upper = true`  : `e <= b + delta`
    * - `upper = false` : `e >= b + delta`
    */
-  private predicate bestBound(SemExpr e, SemBound b, D::Delta delta, boolean upper) {
+  private predicate bestBound(Sem::Expr e, SemBound b, D::Delta delta, boolean upper) {
     delta = min(D::Delta d | bounded(e, b, d, upper, _, _, _) | d order by D::toFloat(d)) and
     upper = true
     or
@@ -357,7 +508,7 @@ module RangeStage<
    * - `upper = false` : `v >= e + delta` or `v > e + delta`
    */
   private predicate boundCondition(
-    SemRelationalExpr comp, SemSsaVariable v, SemExpr e, D::Delta delta, boolean upper
+    Sem::RelationalExpr comp, Sem::SsaVariable v, Sem::Expr e, D::Delta delta, boolean upper
   ) {
     comp.getLesserOperand() = semSsaRead(v, delta) and
     e = comp.getGreaterOperand() and
@@ -367,7 +518,7 @@ module RangeStage<
     e = comp.getLesserOperand() and
     upper = false
     or
-    exists(SemSubExpr sub, SemConstantIntegerExpr c, D::Delta d |
+    exists(Sem::SubExpr sub, Sem::ConstantIntegerExpr c, D::Delta d |
       // (v - d) - e < c
       comp.getLesserOperand() = sub and
       comp.getGreaterOperand() = c and
@@ -407,9 +558,9 @@ module RangeStage<
    * fixed value modulo some `mod > 1`, such that the comparison can be
    * strengthened by `strengthen` when evaluating to `testIsTrue`.
    */
-  private predicate modulusComparison(SemRelationalExpr comp, boolean testIsTrue, int strengthen) {
+  private predicate modulusComparison(Sem::RelationalExpr comp, boolean testIsTrue, int strengthen) {
     exists(
-      SemBound b, int v1, int v2, int mod1, int mod2, int mod, boolean resultIsStrict, int d, int k
+      ModBound b, int v1, int v2, int mod1, int mod2, int mod, boolean resultIsStrict, int d, int k
     |
       // If `x <= y` and `x =(mod) b + v1` and `y =(mod) b + v2` then
       // `0 <= y - x =(mod) v2 - v1`. By choosing `k =(mod) v2 - v1` with
@@ -448,12 +599,12 @@ module RangeStage<
    * - `upper = true`  : `v <= e + delta`
    * - `upper = false` : `v >= e + delta`
    */
-  private SemGuard boundFlowCond(
-    SemSsaVariable v, SemExpr e, D::Delta delta, boolean upper, boolean testIsTrue
+  private Sem::Guard boundFlowCond(
+    Sem::SsaVariable v, Sem::Expr e, D::Delta delta, boolean upper, boolean testIsTrue
   ) {
     exists(
-      SemRelationalExpr comp, D::Delta d1, float d2, float d3, int strengthen, boolean compIsUpper,
-      boolean resultIsStrict
+      Sem::RelationalExpr comp, D::Delta d1, float d2, float d3, int strengthen,
+      boolean compIsUpper, boolean resultIsStrict
     |
       comp = result.asExpr() and
       boundCondition(comp, v, e, d1, compIsUpper) and
@@ -466,8 +617,8 @@ module RangeStage<
       ) and
       (
         if
-          getTrackedTypeForSsaVariable(v) instanceof SemIntegerType or
-          getTrackedTypeForSsaVariable(v) instanceof SemAddressType
+          getTrackedTypeForSsaVariable(v) instanceof Sem::IntegerType or
+          getTrackedTypeForSsaVariable(v) instanceof Sem::AddressType
         then
           upper = true and strengthen = -1
           or
@@ -489,7 +640,8 @@ module RangeStage<
     )
     or
     exists(boolean testIsTrue0 |
-      semImplies_v2(result, testIsTrue, boundFlowCond(v, e, delta, upper, testIsTrue0), testIsTrue0)
+      Sem::implies_v2(result, testIsTrue, boundFlowCond(v, e, delta, upper, testIsTrue0),
+        testIsTrue0)
     )
     or
     result = semEqFlowCond(v, e, delta, true, testIsTrue) and
@@ -498,7 +650,7 @@ module RangeStage<
     // guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
     // exists a guard `guardEq` such that `v = v2 - d1 + d2`.
     exists(
-      SemSsaVariable v2, SemGuard guardEq, boolean eqIsTrue, D::Delta d1, D::Delta d2,
+      Sem::SsaVariable v2, Sem::Guard guardEq, boolean eqIsTrue, D::Delta d1, D::Delta d2,
       D::Delta oldDelta
     |
       guardEq = semEqFlowCond(v, semSsaRead(pragma[only_bind_into](v2), d1), d2, true, eqIsTrue) and
@@ -511,7 +663,7 @@ module RangeStage<
 
   private newtype TSemReason =
     TSemNoReason() or
-    TSemCondReason(SemGuard guard) { possibleReason(guard) }
+    TSemCondReason(Sem::Guard guard) { possibleReason(guard) }
 
   /**
    * A reason for an inferred bound. This can either be `CondReason` if the bound
@@ -534,7 +686,7 @@ module RangeStage<
   /** A reason for an inferred bound pointing to a condition. */
   class SemCondReason extends SemReason, TSemCondReason {
     /** Gets the condition that is the reason for the bound. */
-    SemGuard getCond() { this = TSemCondReason(result) }
+    Sem::Guard getCond() { this = TSemCondReason(result) }
 
     override string toString() { result = this.getCond().toString() }
   }
@@ -545,7 +697,7 @@ module RangeStage<
    * - `upper = false` : `v >= e + delta`
    */
   private predicate boundFlowStepSsa(
-    SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, D::Delta delta, boolean upper,
+    Sem::SsaVariable v, Sem::SsaReadPosition pos, Sem::Expr e, D::Delta delta, boolean upper,
     SemReason reason
   ) {
     semSsaUpdateStep(v, e, delta) and
@@ -553,23 +705,23 @@ module RangeStage<
     (upper = true or upper = false) and
     reason = TSemNoReason()
     or
-    exists(SemGuard guard, boolean testIsTrue |
+    exists(Sem::Guard guard, boolean testIsTrue |
       pos.hasReadOfVar(v) and
       guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
-      semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
+      Sem::guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
       reason = TSemCondReason(guard)
     )
   }
 
   /** Holds if `v != e + delta` at `pos` and `v` is of integral type. */
   private predicate unequalFlowStepIntegralSsa(
-    SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, D::Delta delta, SemReason reason
+    Sem::SsaVariable v, Sem::SsaReadPosition pos, Sem::Expr e, D::Delta delta, SemReason reason
   ) {
-    getTrackedTypeForSsaVariable(v) instanceof SemIntegerType and
-    exists(SemGuard guard, boolean testIsTrue |
+    getTrackedTypeForSsaVariable(v) instanceof Sem::IntegerType and
+    exists(Sem::Guard guard, boolean testIsTrue |
       pos.hasReadOfVar(v) and
       guard = semEqFlowCond(v, e, delta, false, testIsTrue) and
-      semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
+      Sem::guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
       reason = TSemCondReason(guard)
     )
   }
@@ -579,7 +731,7 @@ module RangeStage<
    * - `upper = true`  : `e2 <= e1 + delta`
    * - `upper = false` : `e2 >= e1 + delta`
    */
-  private predicate boundFlowStep(SemExpr e2, SemExpr e1, D::Delta delta, boolean upper) {
+  private predicate boundFlowStep(Sem::Expr e2, Sem::Expr e1, D::Delta delta, boolean upper) {
     semValueFlowStep(e2, e1, delta) and
     (upper = true or upper = false)
     or
@@ -587,22 +739,22 @@ module RangeStage<
     delta = D::fromInt(0) and
     (upper = true or upper = false)
     or
-    e2.(SemRemExpr).getRightOperand() = e1 and
+    e2.(Sem::RemExpr).getRightOperand() = e1 and
     semPositive(e1) and
     delta = D::fromInt(-1) and
     upper = true
     or
-    e2.(SemRemExpr).getLeftOperand() = e1 and
+    e2.(Sem::RemExpr).getLeftOperand() = e1 and
     semPositive(e1) and
     delta = D::fromInt(0) and
     upper = true
     or
-    e2.(SemBitAndExpr).getAnOperand() = e1 and
+    e2.(Sem::BitAndExpr).getAnOperand() = e1 and
     semPositive(e1) and
     delta = D::fromInt(0) and
     upper = true
     or
-    e2.(SemBitOrExpr).getAnOperand() = e1 and
+    e2.(Sem::BitOrExpr).getAnOperand() = e1 and
     semPositive(e2) and
     delta = D::fromInt(0) and
     upper = false
@@ -611,11 +763,11 @@ module RangeStage<
   }
 
   /** Holds if `e2 = e1 * factor` and `factor > 0`. */
-  private predicate boundFlowStepMul(SemExpr e2, SemExpr e1, D::Delta factor) {
-    exists(SemConstantIntegerExpr c, int k | k = c.getIntValue() and k > 0 |
-      e2.(SemMulExpr).hasOperands(e1, c) and factor = D::fromInt(k)
+  private predicate boundFlowStepMul(Sem::Expr e2, Sem::Expr e1, D::Delta factor) {
+    exists(Sem::ConstantIntegerExpr c, int k | k = c.getIntValue() and k > 0 |
+      e2.(Sem::MulExpr).hasOperands(e1, c) and factor = D::fromInt(k)
       or
-      exists(SemShiftLeftExpr e |
+      exists(Sem::ShiftLeftExpr e |
         e = e2 and
         e.getLeftOperand() = e1 and
         e.getRightOperand() = c and
@@ -630,22 +782,22 @@ module RangeStage<
    * This conflates division, right shift, and unsigned right shift and is
    * therefore only valid for non-negative numbers.
    */
-  private predicate boundFlowStepDiv(SemExpr e2, SemExpr e1, D::Delta factor) {
-    exists(SemConstantIntegerExpr c, D::Delta k |
+  private predicate boundFlowStepDiv(Sem::Expr e2, Sem::Expr e1, D::Delta factor) {
+    exists(Sem::ConstantIntegerExpr c, D::Delta k |
       k = D::fromInt(c.getIntValue()) and D::toFloat(k) > 0
     |
-      exists(SemDivExpr e |
+      exists(Sem::DivExpr e |
         e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = k
       )
       or
-      exists(SemShiftRightExpr e |
+      exists(Sem::ShiftRightExpr e |
         e = e2 and
         e.getLeftOperand() = e1 and
         e.getRightOperand() = c and
         factor = D::fromInt(2.pow(D::toInt(k)))
       )
       or
-      exists(SemShiftRightUnsignedExpr e |
+      exists(Sem::ShiftRightUnsignedExpr e |
         e = e2 and
         e.getLeftOperand() = e1 and
         e.getRightOperand() = c and
@@ -660,10 +812,10 @@ module RangeStage<
    * - `upper = false` : `v >= b + delta`
    */
   private predicate boundedSsa(
-    SemSsaVariable v, SemBound b, D::Delta delta, SemSsaReadPosition pos, boolean upper,
+    Sem::SsaVariable v, SemBound b, D::Delta delta, Sem::SsaReadPosition pos, boolean upper,
     boolean fromBackEdge, D::Delta origdelta, SemReason reason
   ) {
-    exists(SemExpr mid, D::Delta d1, D::Delta d2, SemReason r1, SemReason r2 |
+    exists(Sem::Expr mid, D::Delta d1, D::Delta d2, SemReason r1, SemReason r2 |
       boundFlowStepSsa(v, pos, mid, d1, upper, r1) and
       bounded(mid, b, d2, upper, fromBackEdge, origdelta, r2) and
       // upper = true:  v <= mid + d1 <= b + d1 + d2 = b + delta
@@ -697,9 +849,9 @@ module RangeStage<
    * Holds if `v != b + delta` at `pos` and `v` is of integral type.
    */
   private predicate unequalIntegralSsa(
-    SemSsaVariable v, SemBound b, D::Delta delta, SemSsaReadPosition pos, SemReason reason
+    Sem::SsaVariable v, SemBound b, D::Delta delta, Sem::SsaReadPosition pos, SemReason reason
   ) {
-    exists(SemExpr e, D::Delta d1, D::Delta d2 |
+    exists(Sem::Expr e, D::Delta d1, D::Delta d2 |
       unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
       boundedUpper(e, b, d2) and
       boundedLower(e, b, d2) and
@@ -713,7 +865,7 @@ module RangeStage<
    * This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
    */
   pragma[nomagic]
-  private predicate boundedUpper(SemExpr e, SemBound b, D::Delta delta) {
+  private predicate boundedUpper(Sem::Expr e, SemBound b, D::Delta delta) {
     bounded(e, b, delta, true, _, _, _)
   }
 
@@ -723,7 +875,7 @@ module RangeStage<
    * This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
    */
   pragma[nomagic]
-  private predicate boundedLower(SemExpr e, SemBound b, D::Delta delta) {
+  private predicate boundedLower(Sem::Expr e, SemBound b, D::Delta delta) {
     bounded(e, b, delta, false, _, _, _)
   }
 
@@ -744,7 +896,7 @@ module RangeStage<
    * - `upper = false` : `inp >= b + delta`
    */
   private predicate boundedPhiInp(
-    SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, SemBound b,
+    Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, SemBound b,
     D::Delta delta, boolean upper, boolean fromBackEdge, D::Delta origdelta, SemReason reason
   ) {
     edge.phiInput(phi, inp) and
@@ -760,7 +912,7 @@ module RangeStage<
       origdelta = D::fromFloat(0) and
       reason = TSemNoReason()
     |
-      if semBackEdge(phi, inp, edge)
+      if Sem::backEdge(phi, inp, edge)
       then
         fromBackEdge = true and
         (
@@ -787,8 +939,8 @@ module RangeStage<
    */
   pragma[noinline]
   private predicate boundedPhiInp1(
-    SemSsaPhiNode phi, SemBound b, boolean upper, SemSsaVariable inp,
-    SemSsaReadPositionPhiInputEdge edge, D::Delta delta
+    Sem::SsaPhiNode phi, SemBound b, boolean upper, Sem::SsaVariable inp,
+    Sem::SsaReadPositionPhiInputEdge edge, D::Delta delta
   ) {
     boundedPhiInp(phi, inp, edge, b, delta, upper, _, _, _)
   }
@@ -800,7 +952,7 @@ module RangeStage<
    * - `upper = false` : `inp >= phi`
    */
   private predicate selfBoundedPhiInp(
-    SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, boolean upper
+    Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, boolean upper
   ) {
     exists(D::Delta d, SemSsaBound phibound |
       phibound.getAVariable() = phi and
@@ -821,7 +973,7 @@ module RangeStage<
    */
   pragma[noinline]
   private predicate boundedPhiCand(
-    SemSsaPhiNode phi, boolean upper, SemBound b, D::Delta delta, boolean fromBackEdge,
+    Sem::SsaPhiNode phi, boolean upper, SemBound b, D::Delta delta, boolean fromBackEdge,
     D::Delta origdelta, SemReason reason
   ) {
     boundedPhiInp(phi, _, _, b, delta, upper, fromBackEdge, origdelta, reason)
@@ -832,8 +984,9 @@ module RangeStage<
    * `inp` along `edge`.
    */
   private predicate boundedPhiCandValidForEdge(
-    SemSsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
-    D::Delta origdelta, SemReason reason, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge
+    Sem::SsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
+    D::Delta origdelta, SemReason reason, Sem::SsaVariable inp,
+    Sem::SsaReadPositionPhiInputEdge edge
   ) {
     boundedPhiCand(phi, upper, b, delta, fromBackEdge, origdelta, reason) and
     (
@@ -851,11 +1004,11 @@ module RangeStage<
 
   pragma[nomagic]
   private predicate boundedPhiRankStep(
-    SemSsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
+    Sem::SsaPhiNode 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
+    exists(Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge |
+      rankedPhiInput(phi, inp, edge, rix) and
       boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
     |
       if rix = 1
@@ -870,11 +1023,11 @@ module RangeStage<
    * - `upper = false` : `phi >= b + delta`
    */
   private predicate boundedPhi(
-    SemSsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
+    Sem::SsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
     D::Delta origdelta, SemReason reason
   ) {
     exists(int r |
-      Utils::maxPhiInputRank(phi, r) and
+      maxPhiInputRank(phi, r) and
       boundedPhiRankStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, r)
     )
   }
@@ -883,12 +1036,12 @@ module RangeStage<
    * Holds if `e` has an upper (for `upper = true`) or lower
    * (for `upper = false`) bound of `b`.
    */
-  private predicate baseBound(SemExpr e, D::Delta b, boolean upper) {
+  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.(SemBitAndExpr).getAnOperand()) and
+    semPositive(e.(Sem::BitAndExpr).getAnOperand()) and
     // REVIEW: We let the language opt out here to preserve original results.
     not ignoreZeroLowerBound(e)
   }
@@ -918,14 +1071,14 @@ module RangeStage<
   }
 
   pragma[nomagic]
-  private predicate initialBoundedUpper(SemExpr e) {
+  private predicate initialBoundedUpper(Sem::Expr e) {
     exists(D::Delta d |
       initialBounded(e, _, d, false, _, _, _) and
       D::toFloat(d) >= 0
     )
   }
 
-  private predicate noOverflow0(SemExpr e, boolean upper) {
+  private predicate noOverflow0(Sem::Expr e, boolean upper) {
     exists(boolean lower | lower = upper.booleanNot() |
       semExprDoesNotOverflow(lower, e)
       or
@@ -935,7 +1088,7 @@ module RangeStage<
   }
 
   pragma[nomagic]
-  private predicate initialBoundedLower(SemExpr e) {
+  private predicate initialBoundedLower(Sem::Expr e) {
     exists(D::Delta d |
       initialBounded(e, _, d, true, _, _, _) and
       D::toFloat(d) <= 0
@@ -943,7 +1096,7 @@ module RangeStage<
   }
 
   pragma[nomagic]
-  private predicate noOverflow(SemExpr e, boolean upper) {
+  private predicate noOverflow(Sem::Expr e, boolean upper) {
     noOverflow0(e, upper)
     or
     upper = true and initialBoundedUpper(e)
@@ -952,65 +1105,45 @@ module RangeStage<
   }
 
   predicate bounded(
-    SemExpr e, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge, D::Delta origdelta,
-    SemReason reason
+    Sem::Expr e, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
+    D::Delta origdelta, SemReason reason
   ) {
     initialBounded(e, b, delta, upper, fromBackEdge, origdelta, reason) and
     noOverflow(e, upper)
   }
 
-  predicate potentiallyOverflowingExpr(boolean positively, SemExpr expr) {
-    (
-      expr.getOpcode() instanceof Opcode::Add or
-      expr.getOpcode() instanceof Opcode::PointerAdd
-    ) and
-    (
-      positively = true and
-      (
-        pragma[only_bind_out](semExprSign(expr.(SemBinaryExpr).getLeftOperand())) = TPos() and
-        pragma[only_bind_out](semExprSign(expr.(SemBinaryExpr).getRightOperand())) = TPos()
-      )
-      or
-      positively = false and
-      (
-        pragma[only_bind_out](semExprSign(expr.(SemBinaryExpr).getLeftOperand())) = TNeg() and
-        pragma[only_bind_out](semExprSign(expr.(SemBinaryExpr).getRightOperand())) = TNeg()
-      )
-    )
+  predicate potentiallyOverflowingExpr(boolean positively, Sem::Expr expr) {
+    positively = true and
+    semMayBePositive(expr.(Sem::AddExpr).getLeftOperand()) and
+    semMayBePositive(expr.(Sem::AddExpr).getRightOperand())
     or
-    (
-      expr.getOpcode() instanceof Opcode::Sub or
-      expr.getOpcode() instanceof Opcode::PointerSub
-    ) and
-    (
-      positively = true and
-      (
-        pragma[only_bind_out](semExprSign(expr.(SemBinaryExpr).getLeftOperand())) = TPos() and
-        pragma[only_bind_out](semExprSign(expr.(SemBinaryExpr).getRightOperand())) = TNeg()
-      )
-      or
-      positively = false and
-      (
-        pragma[only_bind_out](semExprSign(expr.(SemBinaryExpr).getLeftOperand())) = TNeg() and
-        pragma[only_bind_out](semExprSign(expr.(SemBinaryExpr).getRightOperand())) = TPos()
-      )
-    )
+    positively = false and
+    semMayBeNegative(expr.(Sem::AddExpr).getLeftOperand()) and
+    semMayBeNegative(expr.(Sem::AddExpr).getRightOperand())
+    or
+    positively = true and
+    semMayBePositive(expr.(Sem::SubExpr).getLeftOperand()) and
+    semMayBeNegative(expr.(Sem::SubExpr).getRightOperand())
+    or
+    positively = false and
+    semMayBeNegative(expr.(Sem::SubExpr).getLeftOperand()) and
+    semMayBePositive(expr.(Sem::SubExpr).getRightOperand())
     or
     positively in [true, false] and
     (
-      expr.getOpcode() instanceof Opcode::Mul or
-      expr.getOpcode() instanceof Opcode::ShiftLeft
+      expr instanceof Sem::MulExpr or
+      expr instanceof Sem::ShiftLeftExpr
     )
     or
     positively = false and
     (
-      expr.getOpcode() instanceof Opcode::Negate or
-      expr.getOpcode() instanceof Opcode::SubOne or
-      expr.(SemDivExpr).getSemType() instanceof SemFloatingPointType
+      expr instanceof Sem::NegateExpr or
+      expr instanceof Sem::SubOneExpr or
+      getTrackedType(expr.(Sem::DivExpr)) instanceof Sem::FloatingPointType
     )
     or
     positively = true and
-    expr.getOpcode() instanceof Opcode::AddOne
+    expr instanceof Sem::AddOneExpr
   }
 
   /**
@@ -1028,8 +1161,8 @@ module RangeStage<
    * - `upper = false` : `e >= b + delta`
    */
   predicate initialBounded(
-    SemExpr e, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge, D::Delta origdelta,
-    SemReason reason
+    Sem::Expr e, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
+    D::Delta origdelta, SemReason reason
   ) {
     not ignoreExprBound(e) and
     (
@@ -1045,38 +1178,38 @@ module RangeStage<
       origdelta = delta and
       reason = TSemNoReason()
       or
-      exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
+      exists(Sem::SsaVariable v, Sem::SsaReadPositionBlock bb |
         boundedSsa(v, b, delta, bb, upper, fromBackEdge, origdelta, reason) and
         e = v.getAUse() and
         bb.getBlock() = e.getBasicBlock()
       )
       or
-      exists(SemExpr mid, D::Delta d1, D::Delta d2 |
+      exists(Sem::Expr mid, D::Delta d1, D::Delta d2 |
         boundFlowStep(e, mid, d1, upper) and
         // Constants have easy, base-case bounds, so let's not infer any recursive bounds.
-        not e instanceof SemConstantIntegerExpr and
+        not e instanceof Sem::ConstantIntegerExpr and
         bounded(mid, b, d2, upper, fromBackEdge, origdelta, reason) and
         // upper = true:  e <= mid + d1 <= b + d1 + d2 = b + delta
         // upper = false: e >= mid + d1 >= b + d1 + d2 = b + delta
         delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2))
       )
       or
-      exists(SemSsaPhiNode phi |
+      exists(Sem::SsaPhiNode phi |
         boundedPhi(phi, b, delta, upper, fromBackEdge, origdelta, reason) and
         e = phi.getAUse()
       )
       or
-      exists(SemExpr mid, D::Delta factor, D::Delta d |
+      exists(Sem::Expr mid, D::Delta factor, D::Delta d |
         boundFlowStepMul(e, mid, factor) and
-        not e instanceof SemConstantIntegerExpr and
+        not e instanceof Sem::ConstantIntegerExpr and
         bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
         b instanceof SemZeroBound and
         delta = D::fromFloat(D::toFloat(d) * D::toFloat(factor))
       )
       or
-      exists(SemExpr mid, D::Delta factor, D::Delta d |
+      exists(Sem::Expr mid, D::Delta factor, D::Delta d |
         boundFlowStepDiv(e, mid, factor) and
-        not e instanceof SemConstantIntegerExpr and
+        not e instanceof Sem::ConstantIntegerExpr and
         bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
         b instanceof SemZeroBound and
         D::toFloat(d) >= 0 and
@@ -1090,8 +1223,8 @@ module RangeStage<
       )
       or
       exists(
-        SemConditionalExpr cond, D::Delta d1, D::Delta d2, boolean fbe1, boolean fbe2, D::Delta od1,
-        D::Delta od2, SemReason r1, SemReason r2
+        Sem::ConditionalExpr cond, D::Delta d1, D::Delta d2, boolean fbe1, boolean fbe2,
+        D::Delta od1, D::Delta od2, SemReason r1, SemReason r2
       |
         cond = e and
         boundedConditionalExpr(cond, b, upper, true, d1, fbe1, od1, r1) and
@@ -1107,8 +1240,8 @@ module RangeStage<
         upper = false and delta = D::fromFloat(D::toFloat(d1).minimum(D::toFloat(d2)))
       )
       or
-      exists(SemExpr mid, D::Delta d, float f |
-        e.(SemNegateExpr).getOperand() = mid and
+      exists(Sem::Expr mid, D::Delta d, float f |
+        e.(Sem::NegateExpr).getOperand() = mid and
         b instanceof SemZeroBound and
         bounded(mid, b, d, upper.booleanNot(), fromBackEdge, origdelta, reason) and
         f = normalizeFloatUp(-D::toFloat(d)) and
@@ -1148,7 +1281,7 @@ module RangeStage<
       )
       or
       exists(
-        SemRemExpr rem, D::Delta d_max, D::Delta d1, D::Delta d2, boolean fbe1, boolean fbe2,
+        Sem::RemExpr rem, D::Delta d_max, D::Delta d1, D::Delta d2, boolean fbe1, boolean fbe2,
         D::Delta od1, D::Delta od2, SemReason r1, SemReason r2
       |
         rem = e and
@@ -1189,7 +1322,7 @@ module RangeStage<
 
   pragma[nomagic]
   private predicate boundedConditionalExpr(
-    SemConditionalExpr cond, SemBound b, boolean upper, boolean branch, D::Delta delta,
+    Sem::ConditionalExpr cond, SemBound b, boolean upper, boolean branch, D::Delta delta,
     boolean fromBackEdge, D::Delta origdelta, SemReason reason
   ) {
     bounded(cond.getBranchExpr(branch), b, delta, upper, fromBackEdge, origdelta, reason)
@@ -1197,8 +1330,8 @@ module RangeStage<
 
   pragma[nomagic]
   private predicate boundedAddOperand(
-    SemAddExpr add, boolean upper, SemBound b, boolean isLeft, D::Delta delta, boolean fromBackEdge,
-    D::Delta origdelta, SemReason reason
+    Sem::AddExpr add, boolean upper, SemBound b, boolean isLeft, D::Delta delta,
+    boolean fromBackEdge, D::Delta origdelta, SemReason reason
   ) {
     // `semValueFlowStep` already handles the case where one of the operands is a constant.
     not semValueFlowStep(add, _, _) and
@@ -1217,7 +1350,7 @@ module RangeStage<
    */
   pragma[nomagic]
   private predicate boundedSubOperandLeft(
-    SemSubExpr sub, boolean upper, SemBound b, D::Delta delta, boolean fromBackEdge,
+    Sem::SubExpr sub, boolean upper, SemBound b, D::Delta delta, boolean fromBackEdge,
     D::Delta origdelta, SemReason reason
   ) {
     // `semValueFlowStep` already handles the case where one of the operands is a constant.
@@ -1234,7 +1367,7 @@ module RangeStage<
    */
   pragma[nomagic]
   private predicate boundedSubOperandRight(
-    SemSubExpr sub, boolean upper, D::Delta delta, boolean fromBackEdge
+    Sem::SubExpr sub, boolean upper, D::Delta delta, boolean fromBackEdge
   ) {
     // `semValueFlowStep` already handles the case where one of the operands is a constant.
     not semValueFlowStep(sub, _, _) and
@@ -1244,7 +1377,7 @@ module RangeStage<
 
   pragma[nomagic]
   private predicate boundedRemExpr(
-    SemRemExpr rem, boolean upper, D::Delta delta, boolean fromBackEdge, D::Delta origdelta,
+    Sem::RemExpr rem, boolean upper, D::Delta delta, boolean fromBackEdge, D::Delta origdelta,
     SemReason reason
   ) {
     bounded(rem.getRightOperand(), any(SemZeroBound zb), delta, upper, fromBackEdge, origdelta,
@@ -1260,7 +1393,7 @@ module RangeStage<
    */
   pragma[nomagic]
   private predicate boundedMulOperandCand(
-    SemMulExpr mul, SemExpr left, SemExpr right, boolean upper, boolean upperLeft,
+    Sem::MulExpr mul, Sem::Expr left, Sem::Expr right, boolean upper, boolean upperLeft,
     boolean upperRight
   ) {
     not boundFlowStepMul(mul, _, _) and
@@ -1342,10 +1475,10 @@ module RangeStage<
    */
   pragma[nomagic]
   private predicate boundedMulOperand(
-    SemMulExpr mul, boolean upper, boolean isLeft, D::Delta delta, boolean fromBackEdge,
+    Sem::MulExpr mul, boolean upper, boolean isLeft, D::Delta delta, boolean fromBackEdge,
     D::Delta origdelta, SemReason reason
   ) {
-    exists(boolean upperLeft, boolean upperRight, SemExpr left, SemExpr right |
+    exists(boolean upperLeft, boolean upperRight, Sem::Expr left, Sem::Expr right |
       boundedMulOperandCand(mul, left, right, upper, upperLeft, upperRight)
     |
       isLeft = true and

From ec39de20d82f90a692d54612372058b5c2f59cad Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Mon, 9 Oct 2023 14:05:29 +0200
Subject: [PATCH 04/14] C++: Convert to qlpack version of core range analysis.

---
 cpp/ql/lib/qlpack.yml                         |   1 +
 .../internal/semantic/SemanticLocation.qll    |  12 ++
 .../internal/semantic/analysis/FloatDelta.qll |   6 +-
 .../internal/semantic/analysis/IntDelta.qll   |  29 ----
 .../semantic/analysis/ModulusAnalysis.qll     |   6 +-
 .../RangeAnalysisConstantSpecific.qll         |   5 +-
 .../semantic/analysis/RangeAnalysisImpl.qll   | 130 +++++++++++++++++-
 .../RangeAnalysisRelativeSpecific.qll         |   5 +-
 .../internal/semantic/analysis/RangeUtils.qll |  51 ++++---
 .../semantic/analysis/SignAnalysisCommon.qll  |   5 +-
 .../library-tests/ir/range-analysis/test.cpp  |   2 +-
 11 files changed, 182 insertions(+), 70 deletions(-)
 delete mode 100644 cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/IntDelta.qll

diff --git a/cpp/ql/lib/qlpack.yml b/cpp/ql/lib/qlpack.yml
index cb5488af594a..06ce6589b7b6 100644
--- a/cpp/ql/lib/qlpack.yml
+++ b/cpp/ql/lib/qlpack.yml
@@ -7,6 +7,7 @@ library: true
 upgrades: upgrades
 dependencies:
   codeql/dataflow: ${workspace}
+  codeql/rangeanalysis: ${workspace}
   codeql/ssa: ${workspace}
   codeql/tutorial: ${workspace}
   codeql/util: ${workspace}
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticLocation.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticLocation.qll
index 328f85151b58..0e801fb75c37 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticLocation.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticLocation.qll
@@ -8,6 +8,18 @@ class SemLocation instanceof Location {
    */
   string toString() { result = super.toString() }
 
+  /** Gets the 1-based line number (inclusive) where this location starts. */
+  int getStartLine() { result = super.getStartLine() }
+
+  /** Gets the 1-based column number (inclusive) where this location starts. */
+  int getStartColumn() { result = super.getStartColumn() }
+
+  /** Gets the 1-based line number (inclusive) where this location ends. */
+  int getEndLine() { result = super.getEndLine() }
+
+  /** Gets the 1-based column number (inclusive) where this location ends. */
+  int getEndColumn() { result = super.getEndColumn() }
+
   /**
    * Holds if this element is at the specified location.
    * The location spans column `startcolumn` of line `startline` to
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/FloatDelta.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/FloatDelta.qll
index 8767c53aa195..2cdeb9544ab7 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/FloatDelta.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/FloatDelta.qll
@@ -1,5 +1,7 @@
-private import RangeAnalysisStage
 private import RangeAnalysisImpl
+private import codeql.rangeanalysis.RangeAnalysis
+private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExpr
+private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticType
 
 module FloatDelta implements DeltaSig {
   class Delta = float;
@@ -20,7 +22,7 @@ module FloatDelta implements DeltaSig {
   Delta fromFloat(float f) { result = f }
 }
 
-module FloatOverflow implements OverflowSig<FloatDelta> {
+module FloatOverflow implements OverflowSig<Sem, FloatDelta> {
   predicate semExprDoesNotOverflow(boolean positively, SemExpr expr) {
     exists(float lb, float ub, float delta |
       typeBounds(expr.getSemType(), lb, ub) and
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/IntDelta.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/IntDelta.qll
deleted file mode 100644
index 83698b56229c..000000000000
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/IntDelta.qll
+++ /dev/null
@@ -1,29 +0,0 @@
-private import RangeAnalysisStage
-
-module IntDelta implements DeltaSig {
-  class Delta = int;
-
-  bindingset[d]
-  bindingset[result]
-  float toFloat(Delta d) { result = d }
-
-  bindingset[d]
-  bindingset[result]
-  int toInt(Delta d) { result = d }
-
-  bindingset[n]
-  bindingset[result]
-  Delta fromInt(int n) { result = n }
-
-  bindingset[f]
-  Delta fromFloat(float f) {
-    result =
-      min(float diff, float res |
-        diff = (res - f) and res = f.ceil()
-        or
-        diff = (f - res) and res = f.floor()
-      |
-        res order by diff
-      )
-  }
-}
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ModulusAnalysis.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ModulusAnalysis.qll
index 9b00aca362f1..c53b0b85eb2a 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ModulusAnalysis.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ModulusAnalysis.qll
@@ -12,11 +12,13 @@
 
 private import ModulusAnalysisSpecific::Private
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
+private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticLocation
 private import ConstantAnalysis
 private import RangeUtils
-private import RangeAnalysisStage
+private import codeql.rangeanalysis.RangeAnalysis
+private import RangeAnalysisImpl
 
-module ModulusAnalysis<DeltaSig D, BoundSig<D> Bounds, UtilSig<D> U> {
+module ModulusAnalysis<DeltaSig D, BoundSig<SemLocation, Sem, D> Bounds, UtilSig<Sem, D> U> {
   pragma[nomagic]
   private predicate valueFlowStepSsaEqFlowCond(
     SemSsaReadPosition pos, SemSsaVariable v, SemExpr e, int delta
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll
index 42edb904c3f4..fc729766d2da 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll
@@ -3,10 +3,11 @@
  */
 
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
-private import RangeAnalysisStage
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
+private import RangeAnalysisImpl
+private import codeql.rangeanalysis.RangeAnalysis
 
-module CppLangImplConstant implements LangSig<FloatDelta> {
+module CppLangImplConstant implements LangSig<Sem, FloatDelta> {
   /**
    * Holds if the specified expression should be excluded from the result of `ssaRead()`.
    *
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll
index 938857c0c2de..cbbd5d092bbb 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll
@@ -1,13 +1,104 @@
-private import RangeAnalysisStage
 private import RangeAnalysisConstantSpecific
 private import RangeAnalysisRelativeSpecific
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
 private import RangeUtils
+private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExpr
+private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticCFG
+private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticGuard
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticBound as SemanticBound
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticLocation
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticSSA
+private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticType as SemanticType
+private import SemanticType
+private import codeql.rangeanalysis.RangeAnalysis
+private import ConstantAnalysis as ConstantAnalysis
 
-module ConstantBounds implements BoundSig<FloatDelta> {
+module Sem implements Semantic {
+  class Expr = SemExpr;
+
+  class ConstantIntegerExpr = ConstantAnalysis::SemConstantIntegerExpr;
+
+  class BinaryExpr = SemBinaryExpr;
+
+  class AddExpr = SemAddExpr;
+
+  class SubExpr = SemSubExpr;
+
+  class MulExpr = SemMulExpr;
+
+  class DivExpr = SemDivExpr;
+
+  class RemExpr = SemRemExpr;
+
+  class BitAndExpr = SemBitAndExpr;
+
+  class BitOrExpr = SemBitOrExpr;
+
+  class ShiftLeftExpr = SemShiftLeftExpr;
+
+  class ShiftRightExpr = SemShiftRightExpr;
+
+  class ShiftRightUnsignedExpr = SemShiftRightUnsignedExpr;
+
+  class RelationalExpr = SemRelationalExpr;
+
+  class UnaryExpr = SemUnaryExpr;
+
+  class ConvertExpr = SemConvertExpr;
+
+  class BoxExpr = SemBoxExpr;
+
+  class UnboxExpr = SemUnboxExpr;
+
+  class NegateExpr = SemNegateExpr;
+
+  class AddOneExpr = SemAddOneExpr;
+
+  class SubOneExpr = SemSubOneExpr;
+
+  class ConditionalExpr = SemConditionalExpr;
+
+  class BasicBlock = SemBasicBlock;
+
+  class Guard = SemGuard;
+
+  predicate implies_v2 = semImplies_v2/4;
+
+  predicate guardDirectlyControlsSsaRead = semGuardDirectlyControlsSsaRead/3;
+
+  class Type = SemType;
+
+  class IntegerType = SemIntegerType;
+
+  class FloatingPointType = SemFloatingPointType;
+
+  class AddressType = SemAddressType;
+
+  class SsaVariable = SemSsaVariable;
+
+  class SsaPhiNode = SemSsaPhiNode;
+
+  class SsaExplicitUpdate = SemSsaExplicitUpdate;
+
+  class SsaReadPosition = SemSsaReadPosition;
+
+  class SsaReadPositionPhiInputEdge = SemSsaReadPositionPhiInputEdge;
+
+  class SsaReadPositionBlock = SemSsaReadPositionBlock;
+
+  predicate backEdge = semBackEdge/3;
+
+  predicate conversionCannotOverflow(Type fromType, Type toType) {
+    SemanticType::conversionCannotOverflow(fromType, toType)
+  }
+}
+
+module SignAnalysis implements SignAnalysisSig<Sem> {
+  private import SignAnalysisCommon as SA
+  import SA::SignAnalysis<FloatDelta, Util>
+}
+
+module ConstantBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
   class SemBound instanceof SemanticBound::SemBound {
     SemBound() {
       this instanceof SemanticBound::SemZeroBound
@@ -29,7 +120,7 @@ module ConstantBounds implements BoundSig<FloatDelta> {
   }
 }
 
-module RelativeBounds implements BoundSig<FloatDelta> {
+module RelativeBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
   class SemBound instanceof SemanticBound::SemBound {
     SemBound() { not this instanceof SemanticBound::SemZeroBound }
 
@@ -47,13 +138,38 @@ module RelativeBounds implements BoundSig<FloatDelta> {
   }
 }
 
+module AllBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
+  class SemBound instanceof SemanticBound::SemBound {
+    string toString() { result = super.toString() }
+
+    SemLocation getLocation() { result = super.getLocation() }
+
+    SemExpr getExpr(float delta) { result = super.getExpr(delta) }
+  }
+
+  class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { }
+
+  class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound {
+    SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
+  }
+}
+
+private module ModulusAnalysisInstantiated implements ModulusAnalysisSig<Sem> {
+  class ModBound = AllBounds::SemBound;
+
+  private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.ModulusAnalysis as MA
+  import MA::ModulusAnalysis<FloatDelta, AllBounds, Util>
+}
+
+module Util = RangeUtil<FloatDelta, CppLangImplConstant>;
+
 module ConstantStage =
-  RangeStage<FloatDelta, ConstantBounds, FloatOverflow, CppLangImplConstant,
-    RangeUtil<FloatDelta, CppLangImplConstant>>;
+  RangeStage<SemLocation, Sem, FloatDelta, ConstantBounds, FloatOverflow, CppLangImplConstant,
+    SignAnalysis, ModulusAnalysisInstantiated, Util>;
 
 module RelativeStage =
-  RangeStage<FloatDelta, RelativeBounds, FloatOverflow, CppLangImplRelative,
-    RangeUtil<FloatDelta, CppLangImplRelative>>;
+  RangeStage<SemLocation, Sem, FloatDelta, RelativeBounds, FloatOverflow, CppLangImplRelative,
+    SignAnalysis, ModulusAnalysisInstantiated, Util>;
 
 private newtype TSemReason =
   TSemNoReason() or
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll
index 7643c4aadb94..114219783860 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll
@@ -3,13 +3,12 @@
  */
 
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
-private import RangeAnalysisStage
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
-private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.IntDelta
 private import RangeAnalysisImpl
 private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
+private import codeql.rangeanalysis.RangeAnalysis
 
-module CppLangImplRelative implements LangSig<FloatDelta> {
+module CppLangImplRelative implements LangSig<Sem, FloatDelta> {
   /**
    * Holds if the specified expression should be excluded from the result of `ssaRead()`.
    *
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll
index 1b5da03feecf..e3798600f85d 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll
@@ -4,10 +4,11 @@
 
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
 private import RangeAnalysisRelativeSpecific
-private import RangeAnalysisStage as Range
+private import codeql.rangeanalysis.RangeAnalysis
+private import RangeAnalysisImpl
 private import ConstantAnalysis
 
-module RangeUtil<Range::DeltaSig D, Range::LangSig<D> Lang> implements Range::UtilSig<D> {
+module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
   /**
    * Gets an expression that equals `v - d`.
    */
@@ -138,27 +139,33 @@ module RangeUtil<Range::DeltaSig D, Range::LangSig<D> Lang> implements Range::Ut
     or
     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))
+  import Ranking
 }
 
-/**
- * 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()
-    )
+import Ranking
+
+module Ranking {
+  /**
+   * 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()
+      )
+  }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
index 0de6c1aca6e8..26e72d33e722 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
@@ -6,14 +6,15 @@
  * three-valued domain `{negative, zero, positive}`.
  */
 
-private import RangeAnalysisStage
+private import codeql.rangeanalysis.RangeAnalysis
+private import RangeAnalysisImpl
 private import SignAnalysisSpecific as Specific
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
 private import ConstantAnalysis
 private import RangeUtils
 private import Sign
 
-module SignAnalysis<DeltaSig D, UtilSig<D> Utils> {
+module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
   /**
    * An SSA definition for which the analysis can compute the sign.
    *
diff --git a/cpp/ql/test/library-tests/ir/range-analysis/test.cpp b/cpp/ql/test/library-tests/ir/range-analysis/test.cpp
index ff9acbfae1a4..0602088ba492 100644
--- a/cpp/ql/test/library-tests/ir/range-analysis/test.cpp
+++ b/cpp/ql/test/library-tests/ir/range-analysis/test.cpp
@@ -56,7 +56,7 @@
     while (f3_get(n)) n+=2;
 
     for (int i = 0; i < n; i += 2) {
-      range(i); // $ range=>=0 SPURIOUS: range="<=Phi: call to f3_get-1" range="<=Phi: call to f3_get-2"
+      range(i); // $ range=>=0 range="<=Phi: call to f3_get-2"
     }
   }
 

From 232c147f6b4cd29e6848bdee36a99a1060621679 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Thu, 12 Oct 2023 11:21:34 +0200
Subject: [PATCH 05/14] Rangeanalysis: Port join-order fix from Java version.

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

diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
index 1f462c94f549..e1f1fd4b331f 100644
--- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
+++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
@@ -649,15 +649,25 @@ module RangeStage<
     or
     // guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
     // exists a guard `guardEq` such that `v = v2 - d1 + d2`.
-    exists(
-      Sem::SsaVariable v2, Sem::Guard guardEq, boolean eqIsTrue, D::Delta d1, D::Delta d2,
-      D::Delta oldDelta
-    |
-      guardEq = semEqFlowCond(v, semSsaRead(pragma[only_bind_into](v2), d1), d2, true, eqIsTrue) and
+    exists(Sem::SsaVariable v2, D::Delta oldDelta, float d |
+      // equality needs to control guard
+      result.getBasicBlock() = eqSsaCondDirectlyControls(v, v2, d) and
       result = boundFlowCond(v2, e, oldDelta, upper, testIsTrue) and
-      // guardEq needs to control guard
-      guardEq.directlyControls(result.getBasicBlock(), eqIsTrue) and
-      delta = D::fromFloat(D::toFloat(oldDelta) - D::toFloat(d1) + D::toFloat(d2))
+      delta = D::fromFloat(D::toFloat(oldDelta) + d)
+    )
+  }
+
+  /**
+   * Gets a basic block in which `v1` equals `v2 + delta`.
+   */
+  pragma[nomagic]
+  private Sem::BasicBlock eqSsaCondDirectlyControls(
+    Sem::SsaVariable v1, Sem::SsaVariable v2, float delta
+  ) {
+    exists(Sem::Guard guardEq, D::Delta d1, D::Delta d2, boolean eqIsTrue |
+      guardEq = semEqFlowCond(v1, semSsaRead(v2, d1), d2, true, eqIsTrue) and
+      delta = D::toFloat(d2) - D::toFloat(d1) and
+      guardEq.directlyControls(result, eqIsTrue)
     )
   }
 

From 7b214a24df510fd47aee20fc037f7fad66a2935d Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Thu, 12 Oct 2023 11:25:55 +0200
Subject: [PATCH 06/14] C++: Add division test

---
 .../test/library-tests/ir/range-analysis/test.cpp   | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/cpp/ql/test/library-tests/ir/range-analysis/test.cpp b/cpp/ql/test/library-tests/ir/range-analysis/test.cpp
index 0602088ba492..df06b28e2972 100644
--- a/cpp/ql/test/library-tests/ir/range-analysis/test.cpp
+++ b/cpp/ql/test/library-tests/ir/range-analysis/test.cpp
@@ -117,3 +117,16 @@ void test_sub(int x, int y, int n) {
     }
   }
 }
+
+void test_div(int x) {
+  if (3 <= x && x <= 7) {
+    range(x / 2); // $ SPURIOUS: range=>=1.5 SPURIOUS: range=<=3.5
+    range(x / 3); // $ range=>=1 SPURIOUS: range=<=2.333333
+    range(x >> 2); // $ SPURIOUS: range=>=0.75 SPURIOUS: range=<=1.75
+  }
+  if (2 <= x && x <= 8) {
+    range(x / 2); // $ range=>=1 range=<=4
+    range(x / 3); // $ SPURIOUS: range=>=0.666667 SPURIOUS: range=<=2.666667
+    range(x >> 2); // $ SPURIOUS: range=>=0.5 range=<=2
+  }
+}

From 06fe10bbe9e5f6d53a539c8704d23a045ca3abba Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Thu, 12 Oct 2023 12:59:34 +0200
Subject: [PATCH 07/14] Rangeanalysis: Bugfix division with float
 representation.

---
 cpp/ql/test/library-tests/ir/range-analysis/test.cpp   | 10 +++++-----
 .../codeql/rangeanalysis/RangeAnalysis.qll             |  6 +++++-
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/cpp/ql/test/library-tests/ir/range-analysis/test.cpp b/cpp/ql/test/library-tests/ir/range-analysis/test.cpp
index df06b28e2972..61d171029483 100644
--- a/cpp/ql/test/library-tests/ir/range-analysis/test.cpp
+++ b/cpp/ql/test/library-tests/ir/range-analysis/test.cpp
@@ -120,13 +120,13 @@ void test_sub(int x, int y, int n) {
 
 void test_div(int x) {
   if (3 <= x && x <= 7) {
-    range(x / 2); // $ SPURIOUS: range=>=1.5 SPURIOUS: range=<=3.5
-    range(x / 3); // $ range=>=1 SPURIOUS: range=<=2.333333
-    range(x >> 2); // $ SPURIOUS: range=>=0.75 SPURIOUS: range=<=1.75
+    range(x / 2); // $ range=>=1 range=<=3
+    range(x / 3); // $ range=>=1 range=<=2
+    range(x >> 2); // $ range=>=0 range=<=1
   }
   if (2 <= x && x <= 8) {
     range(x / 2); // $ range=>=1 range=<=4
-    range(x / 3); // $ SPURIOUS: range=>=0.666667 SPURIOUS: range=<=2.666667
-    range(x >> 2); // $ SPURIOUS: range=>=0.5 range=<=2
+    range(x / 3); // $ range=>=0 range=<=2
+    range(x >> 2); // $ range=>=0 range=<=2
   }
 }
diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
index e1f1fd4b331f..ea11074ad12a 100644
--- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
+++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
@@ -793,6 +793,7 @@ module RangeStage<
    * therefore only valid for non-negative numbers.
    */
   private predicate boundFlowStepDiv(Sem::Expr e2, Sem::Expr e1, D::Delta factor) {
+    getTrackedType(e2) instanceof Sem::IntegerType and
     exists(Sem::ConstantIntegerExpr c, D::Delta k |
       k = D::fromInt(c.getIntValue()) and D::toFloat(k) > 0
     |
@@ -1165,6 +1166,9 @@ module RangeStage<
   bindingset[x]
   private float normalizeFloatUp(float x) { result = x + 0.0 }
 
+  bindingset[x, y]
+  private float truncatingDiv(float x, float y) { result = (x - (x % y)) / y }
+
   /**
    * Holds if `b + delta` is a valid bound for `e`.
    * - `upper = true`  : `e <= b + delta`
@@ -1223,7 +1227,7 @@ module RangeStage<
         bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
         b instanceof SemZeroBound and
         D::toFloat(d) >= 0 and
-        delta = D::fromFloat(D::toFloat(d) / D::toFloat(factor))
+        delta = D::fromFloat(truncatingDiv(D::toFloat(d), D::toFloat(factor)))
       )
       or
       exists(NarrowingCastExpr cast |

From cd44d675292ab94fda87f17f19e46b367247116e Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Wed, 18 Oct 2023 13:24:38 +0200
Subject: [PATCH 08/14] Rangeanalysis: Add temporary Java compatibility flag.

---
 .../codeql/rangeanalysis/RangeAnalysis.qll    | 38 +++++++++++++++++++
 1 file changed, 38 insertions(+)

diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
index ea11074ad12a..a136a6eabb16 100644
--- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
+++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
@@ -322,6 +322,8 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
    * actually references but whose values can be tracked as the type contained in the box.
    */
   Sem::Type getAlternateTypeForSsaVariable(Sem::SsaVariable var);
+
+  default predicate javaCompatibility() { none() }
 }
 
 signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> {
@@ -736,6 +738,16 @@ module RangeStage<
     )
   }
 
+  /** Holds if `e >= 1` as determined by sign analysis. */
+  private predicate strictlyPositiveIntegralExpr(Sem::Expr e) {
+    semStrictlyPositive(e) and getTrackedType(e) instanceof Sem::IntegerType
+  }
+
+  /** Holds if `e <= -1` as determined by sign analysis. */
+  private predicate strictlyNegativeIntegralExpr(Sem::Expr e) {
+    semStrictlyNegative(e) and getTrackedType(e) instanceof Sem::IntegerType
+  }
+
   /**
    * Holds if `e1 + delta` is a valid bound for `e2`.
    * - `upper = true`  : `e2 <= e1 + delta`
@@ -749,6 +761,28 @@ module RangeStage<
     delta = D::fromInt(0) and
     (upper = true or upper = false)
     or
+    javaCompatibility() and
+    exists(Sem::Expr x, Sem::SubExpr sub |
+      e2 = sub and
+      sub.getLeftOperand() = e1 and
+      sub.getRightOperand() = x
+    |
+      // `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
+      not x instanceof Sem::ConstantIntegerExpr and
+      if strictlyPositiveIntegralExpr(x)
+      then upper = true and delta = D::fromInt(-1)
+      else
+        if semPositive(x)
+        then upper = true and delta = D::fromInt(0)
+        else
+          if strictlyNegativeIntegralExpr(x)
+          then upper = false and delta = D::fromInt(1)
+          else
+            if semNegative(x)
+            then upper = false and delta = D::fromInt(0)
+            else none()
+    )
+    or
     e2.(Sem::RemExpr).getRightOperand() = e1 and
     semPositive(e1) and
     delta = D::fromInt(-1) and
@@ -1254,6 +1288,7 @@ module RangeStage<
         upper = false and delta = D::fromFloat(D::toFloat(d1).minimum(D::toFloat(d2)))
       )
       or
+      not javaCompatibility() and
       exists(Sem::Expr mid, D::Delta d, float f |
         e.(Sem::NegateExpr).getOperand() = mid and
         b instanceof SemZeroBound and
@@ -1277,6 +1312,7 @@ module RangeStage<
         b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
       )
       or
+      not javaCompatibility() and
       exists(D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight |
         boundedSubOperandLeft(e, upper, b, dLeft, fbeLeft, origdelta, reason) and
         boundedSubOperandRight(e, upper, dRight, fbeRight) and
@@ -1294,6 +1330,7 @@ module RangeStage<
         fromBackEdge = fbeLeft.booleanOr(fbeRight)
       )
       or
+      not javaCompatibility() and
       exists(
         Sem::RemExpr rem, D::Delta d_max, D::Delta d1, D::Delta d2, boolean fbe1, boolean fbe2,
         D::Delta od1, D::Delta od2, SemReason r1, SemReason r2
@@ -1318,6 +1355,7 @@ module RangeStage<
         upper = false and delta = D::fromFloat(-D::toFloat(d_max).abs() + 1)
       )
       or
+      not javaCompatibility() and
       exists(
         D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight, D::Delta odLeft,
         D::Delta odRight, SemReason rLeft, SemReason rRight

From c1c4a5bfcf6043589027b0b62d637adb60324536 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Wed, 18 Oct 2023 14:42:08 +0200
Subject: [PATCH 09/14] Rangeanalysis: Copy qldoc and simplification from Java.

---
 .../codeql/rangeanalysis/RangeAnalysis.qll            | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
index a136a6eabb16..b9ac86b3d3b0 100644
--- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
+++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
@@ -1047,6 +1047,11 @@ module RangeStage<
     )
   }
 
+  /**
+   * 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`
+   */
   pragma[nomagic]
   private predicate boundedPhiRankStep(
     Sem::SsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
@@ -1056,9 +1061,9 @@ module RangeStage<
       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)
+      rix = 1
+      or
+      boundedPhiRankStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, rix - 1)
     )
   }
 

From 36082808d3b99a5a514d00830ae40922cb387ffc Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Wed, 18 Oct 2023 15:04:36 +0200
Subject: [PATCH 10/14] Java: Implement shared range analysis signatures.

---
 java/ql/lib/qlpack.yml                        |   1 +
 java/ql/lib/semmle/code/java/Type.qll         |  24 ++
 .../lib/semmle/code/java/dataflow/Bound.qll   |  22 +-
 .../code/java/dataflow/RangeAnalysis.qll      | 385 +++++++++++++++++-
 .../semmle/code/java/dataflow/RangeUtils.qll  |   9 +-
 .../internal/rangeanalysis/BoundSpecific.qll  |   2 +
 6 files changed, 414 insertions(+), 29 deletions(-)

diff --git a/java/ql/lib/qlpack.yml b/java/ql/lib/qlpack.yml
index 98daf03df528..69273cccf55b 100644
--- a/java/ql/lib/qlpack.yml
+++ b/java/ql/lib/qlpack.yml
@@ -8,6 +8,7 @@ upgrades: upgrades
 dependencies:
   codeql/dataflow: ${workspace}
   codeql/mad: ${workspace}
+  codeql/rangeanalysis: ${workspace}
   codeql/regex: ${workspace}
   codeql/tutorial: ${workspace}
   codeql/typetracking: ${workspace}
diff --git a/java/ql/lib/semmle/code/java/Type.qll b/java/ql/lib/semmle/code/java/Type.qll
index 1b1cb83e4f85..afe78d522f2a 100644
--- a/java/ql/lib/semmle/code/java/Type.qll
+++ b/java/ql/lib/semmle/code/java/Type.qll
@@ -1090,6 +1090,24 @@ class PrimitiveType extends Type, @primitive {
   override string getAPrimaryQlClass() { result = "PrimitiveType" }
 }
 
+private int getByteSize(PrimitiveType t) {
+  t.hasName("boolean") and result = 1
+  or
+  t.hasName("byte") and result = 1
+  or
+  t.hasName("char") and result = 2
+  or
+  t.hasName("short") and result = 2
+  or
+  t.hasName("int") and result = 4
+  or
+  t.hasName("float") and result = 4
+  or
+  t.hasName("long") and result = 8
+  or
+  t.hasName("double") and result = 8
+}
+
 /** The type of the `null` literal. */
 class NullType extends Type, @primitive {
   NullType() { this.hasName("<nulltype>") }
@@ -1282,6 +1300,12 @@ class IntegralType extends Type {
       name = ["byte", "char", "short", "int", "long"]
     )
   }
+
+  /** Gets the size in bytes of this numeric type. */
+  final int getByteSize() {
+    result = getByteSize(this) or
+    result = getByteSize(this.(BoxedType).getPrimitiveType())
+  }
 }
 
 /** A boolean type, which may be either a primitive or a boxed type. */
diff --git a/java/ql/lib/semmle/code/java/dataflow/Bound.qll b/java/ql/lib/semmle/code/java/dataflow/Bound.qll
index b881161f66f5..08826b7ae8f1 100644
--- a/java/ql/lib/semmle/code/java/dataflow/Bound.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/Bound.qll
@@ -25,16 +25,8 @@ abstract class Bound extends TBound {
   /** Gets an expression that equals this bound. */
   Expr getExpr() { result = this.getExpr(0) }
 
-  /**
-   * Holds if this element is at the specified location.
-   * The location spans column `sc` of line `sl` to
-   * column `ec` of line `el` in file `path`.
-   * For more information, see
-   * [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
-   */
-  predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
-    path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
-  }
+  /** Gets the location of this bound. */
+  abstract Location getLocation();
 }
 
 /**
@@ -45,6 +37,8 @@ class ZeroBound extends Bound, TBoundZero {
   override string toString() { result = "0" }
 
   override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }
+
+  override Location getLocation() { result.hasLocationInfo("", 0, 0, 0, 0) }
 }
 
 /**
@@ -58,9 +52,7 @@ class SsaBound extends Bound, TBoundSsa {
 
   override Expr getExpr(int delta) { result = this.getSsa().getAUse() and delta = 0 }
 
-  override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
-    this.getSsa().getLocation().hasLocationInfo(path, sl, sc, el, ec)
-  }
+  override Location getLocation() { result = this.getSsa().getLocation() }
 }
 
 /**
@@ -72,7 +64,5 @@ class ExprBound extends Bound, TBoundExpr {
 
   override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }
 
-  override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
-    this.getExpr().getLocation().hasLocationInfo(path, sl, sc, el, ec)
-  }
+  override Location getLocation() { result = this.getExpr().getLocation() }
 }
diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
index dcbd39bf331c..b7630bccd5e8 100644
--- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
@@ -75,6 +75,354 @@ private import semmle.code.java.Reflection
 private import semmle.code.java.Collections
 private import semmle.code.java.Maps
 import Bound
+private import codeql.rangeanalysis.RangeAnalysis
+
+module Sem implements Semantic {
+  private import java as J
+  private import SSA as SSA
+  private import RangeUtils as RU
+  private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SSAReadPos
+  private import semmle.code.java.controlflow.internal.GuardsLogic as GL
+
+  class Expr = J::Expr;
+
+  class ConstantIntegerExpr = RU::ConstantIntegerExpr;
+
+  abstract class BinaryExpr extends Expr {
+    Expr getLeftOperand() {
+      result = this.(J::BinaryExpr).getLeftOperand() or result = this.(J::AssignOp).getDest()
+    }
+
+    Expr getRightOperand() {
+      result = this.(J::BinaryExpr).getRightOperand() or result = this.(J::AssignOp).getRhs()
+    }
+
+    final Expr getAnOperand() { result = this.getLeftOperand() or result = this.getRightOperand() }
+
+    final predicate hasOperands(Expr e1, Expr e2) {
+      this.getLeftOperand() = e1 and this.getRightOperand() = e2
+      or
+      this.getLeftOperand() = e2 and this.getRightOperand() = e1
+    }
+  }
+
+  class AddExpr extends BinaryExpr {
+    AddExpr() { this instanceof J::AddExpr or this instanceof J::AssignAddExpr }
+  }
+
+  class SubExpr extends BinaryExpr {
+    SubExpr() { this instanceof J::SubExpr or this instanceof J::AssignSubExpr }
+  }
+
+  class MulExpr extends BinaryExpr {
+    MulExpr() { this instanceof J::MulExpr or this instanceof J::AssignMulExpr }
+  }
+
+  class DivExpr extends BinaryExpr {
+    DivExpr() { this instanceof J::DivExpr or this instanceof J::AssignDivExpr }
+  }
+
+  class RemExpr extends BinaryExpr {
+    RemExpr() { this instanceof J::RemExpr or this instanceof J::AssignRemExpr }
+  }
+
+  class BitAndExpr extends BinaryExpr {
+    BitAndExpr() { this instanceof J::AndBitwiseExpr or this instanceof J::AssignAndExpr }
+  }
+
+  class BitOrExpr extends BinaryExpr {
+    BitOrExpr() { this instanceof J::OrBitwiseExpr or this instanceof J::AssignOrExpr }
+  }
+
+  class ShiftLeftExpr extends BinaryExpr {
+    ShiftLeftExpr() { this instanceof J::LeftShiftExpr or this instanceof J::AssignLeftShiftExpr }
+  }
+
+  class ShiftRightExpr extends BinaryExpr {
+    ShiftRightExpr() {
+      this instanceof J::RightShiftExpr or this instanceof J::AssignRightShiftExpr
+    }
+  }
+
+  class ShiftRightUnsignedExpr extends BinaryExpr {
+    ShiftRightUnsignedExpr() {
+      this instanceof J::UnsignedRightShiftExpr or this instanceof J::AssignUnsignedRightShiftExpr
+    }
+  }
+
+  class RelationalExpr = J::ComparisonExpr;
+
+  abstract class UnaryExpr extends Expr {
+    abstract Expr getOperand();
+  }
+
+  class ConvertExpr extends UnaryExpr instanceof CastingExpr {
+    override Expr getOperand() { result = super.getExpr() }
+  }
+
+  class BoxExpr extends UnaryExpr {
+    BoxExpr() { none() }
+
+    override Expr getOperand() { none() }
+  }
+
+  class UnboxExpr extends UnaryExpr {
+    UnboxExpr() { none() }
+
+    override Expr getOperand() { none() }
+  }
+
+  class NegateExpr extends UnaryExpr instanceof MinusExpr {
+    override Expr getOperand() { result = super.getExpr() }
+  }
+
+  // TODO: Implement once utils are properly shared
+  class AddOneExpr extends UnaryExpr {
+    AddOneExpr() { none() }
+
+    override Expr getOperand() { none() }
+  }
+
+  // TODO: Implement once utils are properly shared
+  class SubOneExpr extends UnaryExpr {
+    SubOneExpr() { none() }
+
+    override Expr getOperand() { none() }
+  }
+
+  class ConditionalExpr = J::ConditionalExpr;
+
+  class BasicBlock = J::BasicBlock;
+
+  class Guard extends GL::Guard {
+    Expr asExpr() { result = this }
+  }
+
+  predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
+    GL::implies_v2(g1, b1, g2, b2)
+  }
+
+  predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
+    RU::guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
+  }
+
+  class Type = J::Type;
+
+  class IntegerType extends J::IntegralType {
+    predicate isSigned() { not this instanceof CharacterType }
+  }
+
+  class FloatingPointType extends Type {
+    FloatingPointType() { none() }
+  }
+
+  class AddressType extends Type {
+    AddressType() { none() }
+  }
+
+  final private class FinalSsaVariable = SSA::SsaVariable;
+
+  class SsaVariable extends FinalSsaVariable {
+    Expr getAUse() { result = super.getAUse() }
+  }
+
+  class SsaPhiNode extends SsaVariable instanceof SSA::SsaPhiNode { }
+
+  class SsaExplicitUpdate extends SsaVariable instanceof SSA::SsaExplicitUpdate { }
+
+  final private class FinalSsaReadPosition = SSAReadPos::SsaReadPosition;
+
+  class SsaReadPosition extends FinalSsaReadPosition {
+    predicate hasReadOfVar(SsaVariable v) { super.hasReadOfVar(v) }
+  }
+
+  class SsaReadPositionPhiInputEdge extends SsaReadPosition instanceof SSAReadPos::SsaReadPositionPhiInputEdge
+  {
+    predicate phiInput(SsaPhiNode phi, SsaVariable inp) { super.phiInput(phi, inp) }
+  }
+
+  class SsaReadPositionBlock extends SsaReadPosition instanceof SSAReadPos::SsaReadPositionBlock {
+    BasicBlock getBlock() { result = super.getBlock() }
+  }
+
+  predicate backEdge(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge) {
+    RU::backEdge(phi, inp, edge)
+  }
+
+  predicate conversionCannotOverflow = safeCast/2;
+}
+
+module SignInp implements SignAnalysisSig<Sem> {
+  private import SignAnalysis
+  private import internal.rangeanalysis.Sign
+
+  predicate semPositive = positive/1;
+
+  predicate semNegative = negative/1;
+
+  predicate semStrictlyPositive = strictlyPositive/1;
+
+  predicate semStrictlyNegative = strictlyNegative/1;
+
+  predicate semMayBePositive(Sem::Expr e) { exprSign(e) = TPos() }
+
+  predicate semMayBeNegative(Sem::Expr e) { exprSign(e) = TNeg() }
+}
+
+module Modulus implements ModulusAnalysisSig<Sem> {
+  class ModBound = Bound;
+
+  predicate semExprModulus = exprModulus/4;
+}
+
+module IntDelta implements DeltaSig {
+  class Delta = int;
+
+  bindingset[d]
+  bindingset[result]
+  float toFloat(Delta d) { result = d }
+
+  bindingset[d]
+  bindingset[result]
+  int toInt(Delta d) { result = d }
+
+  bindingset[n]
+  bindingset[result]
+  Delta fromInt(int n) { result = n }
+
+  bindingset[f]
+  Delta fromFloat(float f) { result = f }
+}
+
+module JavaLangImpl implements LangSig<Sem, IntDelta> {
+  predicate ignoreSsaReadCopy(Sem::Expr e) { none() }
+
+  /**
+   * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
+   */
+  predicate hasConstantBound(Sem::Expr e, int bound, boolean upper) {
+    (
+      e.(MethodCall).getMethod() instanceof StringLengthMethod or
+      e.(MethodCall).getMethod() instanceof CollectionSizeMethod or
+      e.(MethodCall).getMethod() instanceof MapSizeMethod or
+      e.(FieldRead).getField() instanceof ArrayLengthField
+    ) and
+    bound = 0 and
+    upper = false
+    or
+    exists(Method read |
+      e.(MethodCall).getMethod().overrides*(read) and
+      read.getDeclaringType() instanceof TypeInputStream and
+      read.hasName("read") and
+      read.getNumberOfParameters() = 0
+    |
+      upper = true and bound = 255
+      or
+      upper = false and bound = -1
+    )
+  }
+
+  /**
+   * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`).
+   */
+  predicate hasBound(Sem::Expr e2, Sem::Expr e1, int delta, boolean upper) {
+    exists(RandomDataSource rds |
+      e2 = rds.getOutput() and
+      (
+        e1 = rds.getUpperBoundExpr() and
+        delta = -1 and
+        upper = true
+        or
+        e1 = rds.getLowerBoundExpr() and
+        delta = 0 and
+        upper = false
+      )
+    )
+    or
+    exists(MethodCall ma, Method m |
+      e2 = ma and
+      ma.getMethod() = m and
+      (
+        m.hasName("max") and upper = false
+        or
+        m.hasName("min") and upper = true
+      ) and
+      m.getDeclaringType().hasQualifiedName("java.lang", "Math") and
+      e1 = ma.getAnArgument() and
+      delta = 0
+    )
+  }
+
+  predicate ignoreExprBound(Sem::Expr e) { none() }
+
+  predicate ignoreZeroLowerBound(Sem::Expr e) { none() }
+
+  predicate ignoreSsaReadArithmeticExpr(Sem::Expr e) { none() }
+
+  predicate ignoreSsaReadAssignment(Sem::SsaVariable v) { none() }
+
+  Sem::Expr specificSsaRead(Sem::SsaVariable v, int delta) { none() }
+
+  predicate additionalValueFlowStep(Sem::Expr dest, Sem::Expr src, int delta) { none() }
+
+  Sem::Type getAlternateType(Sem::Expr e) { none() }
+
+  Sem::Type getAlternateTypeForSsaVariable(Sem::SsaVariable var) { none() }
+
+  predicate javaCompatibility() { any() }
+}
+
+module Utils implements UtilSig<Sem, IntDelta> {
+  private import RangeUtils as RU
+  private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SSAReadPos
+
+  Sem::Expr semSsaRead(Sem::SsaVariable v, int delta) { result = RU::ssaRead(v, delta) }
+
+  Sem::Guard semEqFlowCond(
+    Sem::SsaVariable v, Sem::Expr e, int delta, boolean isEq, boolean testIsTrue
+  ) {
+    result = RU::eqFlowCond(v, e, delta, isEq, testIsTrue)
+  }
+
+  predicate semSsaUpdateStep(Sem::SsaExplicitUpdate v, Sem::Expr e, int delta) {
+    RU::ssaUpdateStep(v, e, delta)
+  }
+
+  predicate semValueFlowStep = RU::valueFlowStep/3;
+
+  Sem::Type getTrackedTypeForSsaVariable(Sem::SsaVariable var) {
+    result = var.getSourceVariable().getType()
+  }
+
+  Sem::Type getTrackedType(Sem::Expr e) { result = e.getType() }
+
+  predicate rankedPhiInput(
+    Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, int r
+  ) {
+    SSAReadPos::rankedPhiInput(phi, inp, edge, r)
+  }
+
+  predicate maxPhiInputRank(Sem::SsaPhiNode phi, int rix) { SSAReadPos::maxPhiInputRank(phi, rix) }
+}
+
+module Bounds implements BoundSig<Location, Sem, IntDelta> {
+  class SemBound = Bound;
+
+  class SemZeroBound = ZeroBound;
+
+  class SemSsaBound extends SsaBound {
+    Sem::SsaVariable getAVariable() { result = super.getSsa() }
+  }
+}
+
+module Overflow implements OverflowSig<Sem, IntDelta> {
+  predicate semExprDoesNotOverflow(boolean positively, Sem::Expr expr) {
+    positively = [true, false] and exists(expr)
+  }
+}
+
+module Range =
+  RangeStage<Location, Sem, IntDelta, Bounds, Overflow, JavaLangImpl, SignInp, Modulus, Utils>;
 
 cached
 private module RangeAnalysisCache {
@@ -138,7 +486,8 @@ private predicate boundCondition(
     sub.getLeftOperand() = ssaRead(v, d) and
     sub.getRightOperand() = e and
     upper = true and
-    delta = d + c.getIntValue()
+    delta = d + c.getIntValue() and
+    okInt(d.(float) + c.getIntValue().(float))
     or
     // (v - d) - e > c
     comp.getGreaterOperand() = sub and
@@ -146,7 +495,8 @@ private predicate boundCondition(
     sub.getLeftOperand() = ssaRead(v, d) and
     sub.getRightOperand() = e and
     upper = false and
-    delta = d + c.getIntValue()
+    delta = d + c.getIntValue() and
+    okInt(d.(float) + c.getIntValue().(float))
     or
     // e - (v - d) < c
     comp.getLesserOperand() = sub and
@@ -154,7 +504,8 @@ private predicate boundCondition(
     sub.getLeftOperand() = e and
     sub.getRightOperand() = ssaRead(v, d) and
     upper = false and
-    delta = d - c.getIntValue()
+    delta = d - c.getIntValue() and
+    okInt(d.(float) - c.getIntValue().(float))
     or
     // e - (v - d) > c
     comp.getGreaterOperand() = sub and
@@ -162,7 +513,8 @@ private predicate boundCondition(
     sub.getLeftOperand() = e and
     sub.getRightOperand() = ssaRead(v, d) and
     upper = true and
-    delta = d - c.getIntValue()
+    delta = d - c.getIntValue() and
+    okInt(d.(float) - c.getIntValue().(float))
   )
 }
 
@@ -245,7 +597,8 @@ private Guard boundFlowCond(SsaVariable v, Expr e, int delta, boolean upper, boo
       or
       resultIsStrict = false and d3 = 0
     ) and
-    delta = d1 + d2 + d3
+    delta = d1 + d2 + d3 and
+    okInt(d1.(float) + d2.(float) + d3.(float))
   )
   or
   exists(boolean testIsTrue0 |
@@ -260,7 +613,8 @@ private Guard boundFlowCond(SsaVariable v, Expr e, int delta, boolean upper, boo
   exists(SsaVariable v2, int d |
     // equality needs to control guard
     result.getBasicBlock() = eqSsaCondDirectlyControls(v, v2, d) and
-    result = boundFlowCond(v2, e, delta - d, upper, testIsTrue)
+    result = boundFlowCond(v2, e, delta - d, upper, testIsTrue) and
+    okInt((delta - d).(float) + d.(float))
   )
 }
 
@@ -272,7 +626,8 @@ private BasicBlock eqSsaCondDirectlyControls(SsaVariable v1, SsaVariable v2, int
   exists(Guard guardEq, int d1, int d2, boolean eqIsTrue |
     guardEq = eqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
     delta = d2 - d1 and
-    guardEq.directlyControls(result, eqIsTrue)
+    guardEq.directlyControls(result, eqIsTrue) and
+    okInt(d2.(float) - d1.(float))
   )
 }
 
@@ -530,6 +885,7 @@ private predicate boundFlowStepMul(Expr e2, Expr e1, int factor) {
  * therefore only valid for non-negative numbers.
  */
 private predicate boundFlowStepDiv(Expr e2, Expr e1, int factor) {
+  e2.getType() instanceof IntegralType and
   exists(ConstantIntegerExpr c, int k | k = c.getIntValue() and k > 0 |
     exists(DivExpr e |
       e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = k
@@ -570,7 +926,8 @@ private predicate boundedSsa(
     // upper = true:  v <= mid + d1 <= b + d1 + d2 = b + delta
     // upper = false: v >= mid + d1 >= b + d1 + d2 = b + delta
     delta = d1 + d2 and
-    (if r1 instanceof NoReason then reason = r2 else reason = r1)
+    (if r1 instanceof NoReason then reason = r2 else reason = r1) and
+    okInt(d1.(float) + d2.(float))
   )
   or
   exists(int d, Reason r1, Reason r2 |
@@ -800,6 +1157,9 @@ private predicate boundedCastExpr(
   bounded(cast.getExpr(), b, delta, upper, fromBackEdge, origdelta, reason)
 }
 
+bindingset[f]
+private predicate okInt(float f) { -2.pow(31) <= f and f <= 2.pow(31) - 1 }
+
 /**
  * Holds if `b + delta` is a valid bound for `e`.
  * - `upper = true`  : `e <= b + delta`
@@ -833,7 +1193,8 @@ private predicate bounded(
     bounded(mid, b, d2, upper, fromBackEdge, origdelta, reason) and
     // upper = true:  e <= mid + d1 <= b + d1 + d2 = b + delta
     // upper = false: e >= mid + d1 >= b + d1 + d2 = b + delta
-    delta = d1 + d2
+    delta = d1 + d2 and
+    okInt(d1.(float) + d2.(float))
   )
   or
   exists(SsaPhiNode phi |
@@ -846,7 +1207,8 @@ private predicate bounded(
     not e instanceof ConstantIntegerExpr and
     bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
     b instanceof ZeroBound and
-    delta = d * factor
+    delta = d * factor and
+    okInt(d.(float) * factor.(float))
   )
   or
   exists(Expr mid, int factor, int d |
@@ -889,7 +1251,8 @@ private predicate bounded(
     boundedAddition(e, upper, b1, true, d1, fbe1, od1, r1) and
     boundedAddition(e, upper, b2, false, d2, fbe2, od2, r2) and
     delta = d1 + d2 and
-    fromBackEdge = fbe1.booleanOr(fbe2)
+    fromBackEdge = fbe1.booleanOr(fbe2) and
+    okInt(d1.(float) + d2.(float))
   |
     b = b1 and origdelta = od1 and reason = r1 and b2 instanceof ZeroBound
     or
diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
index be7f12920914..1336caac6544 100644
--- a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll
@@ -145,6 +145,9 @@ class ConstantStringExpr extends Expr {
   string getStringValue() { constantStringExpr(this, result) }
 }
 
+bindingset[f]
+private predicate okInt(float f) { -2.pow(31) <= f and f <= 2.pow(31) - 1 }
+
 /**
  * Gets an expression that equals `v - d`.
  */
@@ -153,14 +156,16 @@ Expr ssaRead(SsaVariable v, int delta) {
   or
   exists(int d1, ConstantIntegerExpr c |
     result.(AddExpr).hasOperands(ssaRead(v, d1), c) and
-    delta = d1 - c.getIntValue()
+    delta = d1 - c.getIntValue() and
+    okInt(d1.(float) - c.getIntValue().(float))
   )
   or
   exists(SubExpr sub, int d1, ConstantIntegerExpr c |
     result = sub and
     sub.getLeftOperand() = ssaRead(v, d1) and
     sub.getRightOperand() = c and
-    delta = d1 + c.getIntValue()
+    delta = d1 + c.getIntValue() and
+    okInt(d1.(float) + c.getIntValue().(float))
   )
   or
   v.(SsaExplicitUpdate).getDefiningExpr().(PreIncExpr) = result and delta = 0
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/BoundSpecific.qll b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/BoundSpecific.qll
index f7fca3a184f6..0af549f1f7ee 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/BoundSpecific.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/BoundSpecific.qll
@@ -10,6 +10,8 @@ class SsaVariable = Ssa::SsaVariable;
 
 class Expr = J::Expr;
 
+class Location = J::Location;
+
 class IntegralType = J::IntegralType;
 
 class ConstantIntegerExpr = RU::ConstantIntegerExpr;

From 2592c94c5472089d95d84b763b29fe033285f9df Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Wed, 18 Oct 2023 15:15:13 +0200
Subject: [PATCH 11/14] Java: Replace range analysis with shared version.

---
 .../code/java/dataflow/RangeAnalysis.qll      | 849 +-----------------
 1 file changed, 4 insertions(+), 845 deletions(-)

diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
index b7630bccd5e8..cd7a2c9c6e6c 100644
--- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
@@ -424,276 +424,13 @@ module Overflow implements OverflowSig<Sem, IntDelta> {
 module Range =
   RangeStage<Location, Sem, IntDelta, Bounds, Overflow, JavaLangImpl, SignInp, Modulus, Utils>;
 
-cached
-private module RangeAnalysisCache {
-  cached
-  module RangeAnalysisPublic {
-    /**
-     * Holds if `b + delta` is a valid bound for `e`.
-     * - `upper = true`  : `e <= b + delta`
-     * - `upper = false` : `e >= b + delta`
-     *
-     * The reason for the bound is given by `reason` and may be either a condition
-     * or `NoReason` if the bound was proven directly without the use of a bounding
-     * condition.
-     */
-    cached
-    predicate bounded(Expr e, Bound b, int delta, boolean upper, Reason reason) {
-      bounded(e, b, delta, upper, _, _, reason) and
-      bestBound(e, b, delta, upper)
-    }
-  }
+predicate bounded = Range::semBounded/5;
 
-  /**
-   * Holds if `guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)`.
-   */
-  cached
-  predicate possibleReason(Guard guard) {
-    guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)
-  }
-}
-
-private import RangeAnalysisCache
-import RangeAnalysisPublic
-
-/**
- * Holds if `b + delta` is a valid bound for `e` and this is the best such delta.
- * - `upper = true`  : `e <= b + delta`
- * - `upper = false` : `e >= b + delta`
- */
-private predicate bestBound(Expr e, Bound b, int delta, boolean upper) {
-  delta = min(int d | bounded(e, b, d, upper, _, _, _)) and upper = true
-  or
-  delta = max(int d | bounded(e, b, d, upper, _, _, _)) and upper = false
-}
+class Reason = Range::SemReason;
 
-/**
- * Holds if `comp` corresponds to:
- * - `upper = true`  : `v <= e + delta` or `v < e + delta`
- * - `upper = false` : `v >= e + delta` or `v > e + delta`
- */
-private predicate boundCondition(
-  ComparisonExpr comp, SsaVariable v, Expr e, int delta, boolean upper
-) {
-  comp.getLesserOperand() = ssaRead(v, delta) and e = comp.getGreaterOperand() and upper = true
-  or
-  comp.getGreaterOperand() = ssaRead(v, delta) and e = comp.getLesserOperand() and upper = false
-  or
-  exists(SubExpr sub, ConstantIntegerExpr c, int d |
-    // (v - d) - e < c
-    comp.getLesserOperand() = sub and
-    comp.getGreaterOperand() = c and
-    sub.getLeftOperand() = ssaRead(v, d) and
-    sub.getRightOperand() = e and
-    upper = true and
-    delta = d + c.getIntValue() and
-    okInt(d.(float) + c.getIntValue().(float))
-    or
-    // (v - d) - e > c
-    comp.getGreaterOperand() = sub and
-    comp.getLesserOperand() = c and
-    sub.getLeftOperand() = ssaRead(v, d) and
-    sub.getRightOperand() = e and
-    upper = false and
-    delta = d + c.getIntValue() and
-    okInt(d.(float) + c.getIntValue().(float))
-    or
-    // e - (v - d) < c
-    comp.getLesserOperand() = sub and
-    comp.getGreaterOperand() = c and
-    sub.getLeftOperand() = e and
-    sub.getRightOperand() = ssaRead(v, d) and
-    upper = false and
-    delta = d - c.getIntValue() and
-    okInt(d.(float) - c.getIntValue().(float))
-    or
-    // e - (v - d) > c
-    comp.getGreaterOperand() = sub and
-    comp.getLesserOperand() = c and
-    sub.getLeftOperand() = e and
-    sub.getRightOperand() = ssaRead(v, d) and
-    upper = true and
-    delta = d - c.getIntValue() and
-    okInt(d.(float) - c.getIntValue().(float))
-  )
-}
+class NoReason = Range::SemNoReason;
 
-/**
- * Holds if `comp` is a comparison between `x` and `y` for which `y - x` has a
- * fixed value modulo some `mod > 1`, such that the comparison can be
- * strengthened by `strengthen` when evaluating to `testIsTrue`.
- */
-private predicate modulusComparison(ComparisonExpr comp, boolean testIsTrue, int strengthen) {
-  exists(
-    Bound b, int v1, int v2, int mod1, int mod2, int mod, boolean resultIsStrict, int d, int k
-  |
-    // If `x <= y` and `x =(mod) b + v1` and `y =(mod) b + v2` then
-    // `0 <= y - x =(mod) v2 - v1`. By choosing `k =(mod) v2 - v1` with
-    // `0 <= k < mod` we get `k <= y - x`. If the resulting comparison is
-    // strict then the strengthening amount is instead `k - 1` modulo `mod`:
-    // `x < y` means `0 <= y - x - 1 =(mod) k - 1` so `k - 1 <= y - x - 1` and
-    // thus `k - 1 < y - x` with `0 <= k - 1 < mod`.
-    exprModulus(comp.getLesserOperand(), b, v1, mod1) and
-    exprModulus(comp.getGreaterOperand(), b, v2, mod2) and
-    mod = mod1.gcd(mod2) and
-    mod != 1 and
-    (testIsTrue = true or testIsTrue = false) and
-    (
-      if comp.isStrict()
-      then resultIsStrict = testIsTrue
-      else resultIsStrict = testIsTrue.booleanNot()
-    ) and
-    (
-      resultIsStrict = true and d = 1
-      or
-      resultIsStrict = false and d = 0
-    ) and
-    (
-      testIsTrue = true and k = v2 - v1
-      or
-      testIsTrue = false and k = v1 - v2
-    ) and
-    strengthen = (((k - d) % mod) + mod) % mod
-  )
-}
-
-/**
- * Gets a condition that tests whether `v` is bounded by `e + delta`.
- *
- * If the condition evaluates to `testIsTrue`:
- * - `upper = true`  : `v <= e + delta`
- * - `upper = false` : `v >= e + delta`
- */
-private Guard boundFlowCond(SsaVariable v, Expr e, int delta, boolean upper, boolean testIsTrue) {
-  exists(
-    ComparisonExpr comp, int d1, int d2, int d3, int strengthen, boolean compIsUpper,
-    boolean resultIsStrict
-  |
-    comp = result and
-    boundCondition(comp, v, e, d1, compIsUpper) and
-    (testIsTrue = true or testIsTrue = false) and
-    upper = compIsUpper.booleanXor(testIsTrue.booleanNot()) and
-    (
-      if comp.isStrict()
-      then resultIsStrict = testIsTrue
-      else resultIsStrict = testIsTrue.booleanNot()
-    ) and
-    (
-      if v.getSourceVariable().getType() instanceof IntegralType
-      then
-        upper = true and strengthen = -1
-        or
-        upper = false and strengthen = 1
-      else strengthen = 0
-    ) and
-    (
-      exists(int k | modulusComparison(comp, testIsTrue, k) and d2 = strengthen * k)
-      or
-      not modulusComparison(comp, testIsTrue, _) and d2 = 0
-    ) and
-    // A strict inequality `x < y` can be strengthened to `x <= y - 1`.
-    (
-      resultIsStrict = true and d3 = strengthen
-      or
-      resultIsStrict = false and d3 = 0
-    ) and
-    delta = d1 + d2 + d3 and
-    okInt(d1.(float) + d2.(float) + d3.(float))
-  )
-  or
-  exists(boolean testIsTrue0 |
-    implies_v2(result, testIsTrue, boundFlowCond(v, e, delta, upper, testIsTrue0), testIsTrue0)
-  )
-  or
-  result = eqFlowCond(v, e, delta, true, testIsTrue) and
-  (upper = true or upper = false)
-  or
-  // guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
-  // exists a guard `guardEq` such that `v = v2 - d1 + d2`.
-  exists(SsaVariable v2, int d |
-    // equality needs to control guard
-    result.getBasicBlock() = eqSsaCondDirectlyControls(v, v2, d) and
-    result = boundFlowCond(v2, e, delta - d, upper, testIsTrue) and
-    okInt((delta - d).(float) + d.(float))
-  )
-}
-
-/**
- * Gets a basic block in which `v1` equals `v2 + delta`.
- */
-pragma[nomagic]
-private BasicBlock eqSsaCondDirectlyControls(SsaVariable v1, SsaVariable v2, int delta) {
-  exists(Guard guardEq, int d1, int d2, boolean eqIsTrue |
-    guardEq = eqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
-    delta = d2 - d1 and
-    guardEq.directlyControls(result, eqIsTrue) and
-    okInt(d2.(float) - d1.(float))
-  )
-}
-
-private newtype TReason =
-  TNoReason() or
-  TCondReason(Guard guard) { possibleReason(guard) }
-
-/**
- * A reason for an inferred bound. This can either be `CondReason` if the bound
- * is due to a specific condition, or `NoReason` if the bound is inferred
- * without going through a bounding condition.
- */
-abstract class Reason extends TReason {
-  /** Gets a textual representation of this reason. */
-  abstract string toString();
-}
-
-/**
- * A reason for an inferred bound that indicates that the bound is inferred
- * without going through a bounding condition.
- */
-class NoReason extends Reason, TNoReason {
-  override string toString() { result = "NoReason" }
-}
-
-/** A reason for an inferred bound pointing to a condition. */
-class CondReason extends Reason, TCondReason {
-  /** Gets the condition that is the reason for the bound. */
-  Guard getCond() { this = TCondReason(result) }
-
-  override string toString() { result = this.getCond().toString() }
-}
-
-/**
- * Holds if `e + delta` is a valid bound for `v` at `pos`.
- * - `upper = true`  : `v <= e + delta`
- * - `upper = false` : `v >= e + delta`
- */
-private predicate boundFlowStepSsa(
-  SsaVariable v, SsaReadPosition pos, Expr e, int delta, boolean upper, Reason reason
-) {
-  ssaUpdateStep(v, e, delta) and
-  pos.hasReadOfVar(v) and
-  (upper = true or upper = false) and
-  reason = TNoReason()
-  or
-  exists(Guard guard, boolean testIsTrue |
-    pos.hasReadOfVar(v) and
-    guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
-    guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
-    reason = TCondReason(guard)
-  )
-}
-
-/** Holds if `v != e + delta` at `pos` and `v` is of integral type. */
-private predicate unequalFlowStepIntegralSsa(
-  SsaVariable v, SsaReadPosition pos, Expr e, int delta, Reason reason
-) {
-  v.getSourceVariable().getType() instanceof IntegralType and
-  exists(Guard guard, boolean testIsTrue |
-    pos.hasReadOfVar(v) and
-    guard = eqFlowCond(v, e, delta, false, testIsTrue) and
-    guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
-    reason = TCondReason(guard)
-  )
-}
+class CondReason = Range::SemCondReason;
 
 /**
  * Holds if a cast from `fromtyp` to `totyp` can be ignored for the purpose of
@@ -722,581 +459,3 @@ private predicate safeCast(Type fromtyp, Type totyp) {
   or
   safeCast(fromtyp, totyp.(BoxedType).getPrimitiveType())
 }
-
-/**
- * A cast that can be ignored for the purpose of range analysis.
- */
-private class RangeAnalysisSafeCastingExpr extends CastingExpr {
-  RangeAnalysisSafeCastingExpr() {
-    safeCast(this.getExpr().getType(), this.getType()) or
-    this instanceof ImplicitCastExpr or
-    this instanceof ImplicitNotNullExpr or
-    this instanceof ImplicitCoercionToUnitExpr
-  }
-}
-
-/**
- * Holds if `typ` is a small integral type with the given lower and upper bounds.
- */
-private predicate typeBound(Type typ, int lowerbound, int upperbound) {
-  typ.(PrimitiveType).hasName("byte") and lowerbound = -128 and upperbound = 127
-  or
-  typ.(PrimitiveType).hasName("short") and lowerbound = -32768 and upperbound = 32767
-  or
-  typ.(PrimitiveType).hasName("char") and lowerbound = 0 and upperbound = 65535
-  or
-  typeBound(typ.(BoxedType).getPrimitiveType(), lowerbound, upperbound)
-}
-
-/**
- * A cast to a small integral type that may overflow or underflow.
- */
-private class NarrowingCastingExpr extends CastingExpr {
-  NarrowingCastingExpr() {
-    not this instanceof RangeAnalysisSafeCastingExpr and
-    typeBound(this.getType(), _, _)
-  }
-
-  /** Gets the lower bound of the resulting type. */
-  int getLowerBound() { typeBound(this.getType(), result, _) }
-
-  /** Gets the upper bound of the resulting type. */
-  int getUpperBound() { typeBound(this.getType(), _, result) }
-}
-
-/** Holds if `e >= 1` as determined by sign analysis. */
-private predicate strictlyPositiveIntegralExpr(Expr e) {
-  strictlyPositive(e) and e.getType() instanceof IntegralType
-}
-
-/** Holds if `e <= -1` as determined by sign analysis. */
-private predicate strictlyNegativeIntegralExpr(Expr e) {
-  strictlyNegative(e) and e.getType() instanceof IntegralType
-}
-
-/**
- * Holds if `e1 + delta` is a valid bound for `e2`.
- * - `upper = true`  : `e2 <= e1 + delta`
- * - `upper = false` : `e2 >= e1 + delta`
- */
-private predicate boundFlowStep(Expr e2, Expr e1, int delta, boolean upper) {
-  valueFlowStep(e2, e1, delta) and
-  (upper = true or upper = false)
-  or
-  e2.(RangeAnalysisSafeCastingExpr).getExpr() = e1 and
-  delta = 0 and
-  (upper = true or upper = false)
-  or
-  exists(Expr x |
-    exists(SubExpr sub |
-      e2 = sub and
-      sub.getLeftOperand() = e1 and
-      sub.getRightOperand() = x
-    )
-    or
-    exists(AssignSubExpr sub |
-      e2 = sub and
-      sub.getDest() = e1 and
-      sub.getRhs() = x
-    )
-  |
-    // `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
-    not x instanceof ConstantIntegerExpr and
-    if strictlyPositiveIntegralExpr(x)
-    then upper = true and delta = -1
-    else
-      if positive(x)
-      then upper = true and delta = 0
-      else
-        if strictlyNegativeIntegralExpr(x)
-        then upper = false and delta = 1
-        else
-          if negative(x)
-          then upper = false and delta = 0
-          else none()
-  )
-  or
-  e2.(RemExpr).getRightOperand() = e1 and positive(e1) and delta = -1 and upper = true
-  or
-  e2.(RemExpr).getLeftOperand() = e1 and positive(e1) and delta = 0 and upper = true
-  or
-  e2.(AssignRemExpr).getRhs() = e1 and positive(e1) and delta = -1 and upper = true
-  or
-  e2.(AssignRemExpr).getDest() = e1 and positive(e1) and delta = 0 and upper = true
-  or
-  e2.(AndBitwiseExpr).getAnOperand() = e1 and positive(e1) and delta = 0 and upper = true
-  or
-  e2.(AssignAndExpr).getSource() = e1 and positive(e1) and delta = 0 and upper = true
-  or
-  e2.(OrBitwiseExpr).getAnOperand() = e1 and positive(e2) and delta = 0 and upper = false
-  or
-  e2.(AssignOrExpr).getSource() = e1 and positive(e2) and delta = 0 and upper = false
-  or
-  exists(RandomDataSource rds |
-    e2 = rds.getOutput() and
-    (
-      e1 = rds.getUpperBoundExpr() and
-      delta = -1 and
-      upper = true
-      or
-      e1 = rds.getLowerBoundExpr() and
-      delta = 0 and
-      upper = false
-    )
-  )
-  or
-  exists(MethodCall ma, Method m |
-    e2 = ma and
-    ma.getMethod() = m and
-    (
-      m.hasName("max") and upper = false
-      or
-      m.hasName("min") and upper = true
-    ) and
-    m.getDeclaringType().hasQualifiedName("java.lang", "Math") and
-    e1 = ma.getAnArgument() and
-    delta = 0
-  )
-}
-
-/** Holds if `e2 = e1 * factor` and `factor > 0`. */
-private predicate boundFlowStepMul(Expr e2, Expr e1, int factor) {
-  exists(ConstantIntegerExpr c, int k | k = c.getIntValue() and k > 0 |
-    e2.(MulExpr).hasOperands(e1, c) and factor = k
-    or
-    exists(AssignMulExpr e | e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = k)
-    or
-    exists(AssignMulExpr e | e = e2 and e.getDest() = c and e.getRhs() = e1 and factor = k)
-    or
-    exists(LeftShiftExpr e |
-      e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)
-    )
-    or
-    exists(AssignLeftShiftExpr e |
-      e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = 2.pow(k)
-    )
-  )
-}
-
-/**
- * Holds if `e2 = e1 / factor` and `factor > 0`.
- *
- * This conflates division, right shift, and unsigned right shift and is
- * therefore only valid for non-negative numbers.
- */
-private predicate boundFlowStepDiv(Expr e2, Expr e1, int factor) {
-  e2.getType() instanceof IntegralType and
-  exists(ConstantIntegerExpr c, int k | k = c.getIntValue() and k > 0 |
-    exists(DivExpr e |
-      e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = k
-    )
-    or
-    exists(AssignDivExpr e | e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = k)
-    or
-    exists(RightShiftExpr e |
-      e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)
-    )
-    or
-    exists(AssignRightShiftExpr e |
-      e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = 2.pow(k)
-    )
-    or
-    exists(UnsignedRightShiftExpr e |
-      e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)
-    )
-    or
-    exists(AssignUnsignedRightShiftExpr e |
-      e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = 2.pow(k)
-    )
-  )
-}
-
-/**
- * Holds if `b + delta` is a valid bound for `v` at `pos`.
- * - `upper = true`  : `v <= b + delta`
- * - `upper = false` : `v >= b + delta`
- */
-private predicate boundedSsa(
-  SsaVariable v, SsaReadPosition pos, Bound b, int delta, boolean upper, boolean fromBackEdge,
-  int origdelta, Reason reason
-) {
-  exists(Expr mid, int d1, int d2, Reason r1, Reason r2 |
-    boundFlowStepSsa(v, pos, mid, d1, upper, r1) and
-    bounded(mid, b, d2, upper, fromBackEdge, origdelta, r2) and
-    // upper = true:  v <= mid + d1 <= b + d1 + d2 = b + delta
-    // upper = false: v >= mid + d1 >= b + d1 + d2 = b + delta
-    delta = d1 + d2 and
-    (if r1 instanceof NoReason then reason = r2 else reason = r1) and
-    okInt(d1.(float) + d2.(float))
-  )
-  or
-  exists(int d, Reason r1, Reason r2 |
-    boundedSsa(v, pos, b, d, upper, fromBackEdge, origdelta, r2) or
-    boundedPhi(v, b, d, upper, fromBackEdge, origdelta, r2)
-  |
-    unequalIntegralSsa(v, pos, b, d, r1) and
-    (
-      upper = true and delta = d - 1
-      or
-      upper = false and delta = d + 1
-    ) and
-    (
-      reason = r1
-      or
-      reason = r2 and not r2 instanceof NoReason
-    )
-  )
-}
-
-/**
- * Holds if `v != b + delta` at `pos` and `v` is of integral type.
- */
-private predicate unequalIntegralSsa(
-  SsaVariable v, SsaReadPosition pos, Bound b, int delta, Reason reason
-) {
-  exists(Expr e, int d1, int d2 |
-    unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
-    bounded(e, b, d2, true, _, _, _) and
-    bounded(e, b, d2, false, _, _, _) and
-    delta = d2 + d1
-  )
-}
-
-/** Weakens a delta to lie in the range `[-1..1]`. */
-bindingset[delta, upper]
-private int weakenDelta(boolean upper, int delta) {
-  delta in [-1 .. 1] and result = delta
-  or
-  upper = true and result = -1 and delta < -1
-  or
-  upper = false and result = 1 and delta > 1
-}
-
-/**
- * Holds if `b + delta` is a valid bound for `inp` when used as an input to
- * `phi` along `edge`.
- * - `upper = true`  : `inp <= b + delta`
- * - `upper = false` : `inp >= b + delta`
- */
-private predicate boundedPhiInp(
-  SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, Bound b, int delta,
-  boolean upper, boolean fromBackEdge, int origdelta, Reason reason
-) {
-  edge.phiInput(phi, inp) and
-  exists(int d, boolean fromBackEdge0 |
-    boundedSsa(inp, edge, b, d, upper, fromBackEdge0, origdelta, reason)
-    or
-    boundedPhi(inp, b, d, upper, fromBackEdge0, origdelta, reason)
-    or
-    b.(SsaBound).getSsa() = inp and
-    d = 0 and
-    (upper = true or upper = false) and
-    fromBackEdge0 = false and
-    origdelta = 0 and
-    reason = TNoReason()
-  |
-    if backEdge(phi, inp, edge)
-    then
-      fromBackEdge = true and
-      (
-        fromBackEdge0 = true and delta = weakenDelta(upper, d - origdelta) + origdelta
-        or
-        fromBackEdge0 = false and delta = d
-      )
-    else (
-      delta = d and fromBackEdge = fromBackEdge0
-    )
-  )
-}
-
-/** Holds if `boundedPhiInp(phi, inp, edge, b, delta, upper, _, _, _)`. */
-pragma[noinline]
-private predicate boundedPhiInp1(
-  SsaPhiNode phi, Bound b, boolean upper, SsaVariable inp, SsaReadPositionPhiInputEdge edge,
-  int delta
-) {
-  boundedPhiInp(phi, inp, edge, b, delta, upper, _, _, _)
-}
-
-/**
- * Holds if `phi` is a valid bound for `inp` when used as an input to `phi`
- * along `edge`.
- * - `upper = true`  : `inp <= phi`
- * - `upper = false` : `inp >= phi`
- */
-private predicate selfBoundedPhiInp(
-  SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, boolean upper
-) {
-  exists(int d, SsaBound phibound |
-    phibound.getSsa() = phi and
-    boundedPhiInp(phi, inp, edge, phibound, d, upper, _, _, _) and
-    (
-      upper = true and d <= 0
-      or
-      upper = false and d >= 0
-    )
-  )
-}
-
-/**
- * Holds if `b + delta` is a valid bound for some input, `inp`, to `phi`, and
- * thus a candidate bound for `phi`.
- * - `upper = true`  : `inp <= b + delta`
- * - `upper = false` : `inp >= b + delta`
- */
-pragma[noinline]
-private predicate boundedPhiCand(
-  SsaPhiNode phi, boolean upper, Bound b, int delta, boolean fromBackEdge, int origdelta,
-  Reason reason
-) {
-  boundedPhiInp(phi, _, _, b, delta, upper, fromBackEdge, origdelta, reason)
-}
-
-/**
- * Holds if the candidate bound `b + delta` for `phi` is valid for the phi input
- * `inp` along `edge`.
- */
-private predicate boundedPhiCandValidForEdge(
-  SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
-  Reason reason, SsaVariable inp, SsaReadPositionPhiInputEdge edge
-) {
-  boundedPhiCand(phi, upper, b, delta, fromBackEdge, origdelta, reason) and
-  (
-    exists(int d | boundedPhiInp1(phi, b, upper, inp, edge, d) | upper = true and d <= delta)
-    or
-    exists(int d | boundedPhiInp1(phi, b, upper, inp, edge, d) | upper = false and d >= delta)
-    or
-    selfBoundedPhiInp(phi, inp, edge, upper)
-  )
-}
-
-/**
- * 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`
- * - `upper = false` : `phi >= b + delta`
- */
-private predicate boundedPhi(
-  SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
-  Reason reason
-) {
-  exists(int r |
-    boundedPhiStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, r) and
-    maxPhiInputRank(phi, r)
-  )
-}
-
-/**
- * Holds if `e` has a lower bound of zero.
- */
-private predicate lowerBoundZero(Expr e) {
-  e.(MethodCall).getMethod() instanceof StringLengthMethod or
-  e.(MethodCall).getMethod() instanceof CollectionSizeMethod or
-  e.(MethodCall).getMethod() instanceof MapSizeMethod or
-  e.(FieldRead).getField() instanceof ArrayLengthField or
-  positive(e.(AndBitwiseExpr).getAnOperand())
-}
-
-/**
- * Holds if `e` has an upper (for `upper = true`) or lower
- * (for `upper = false`) bound of `b`.
- */
-private predicate baseBound(Expr e, int b, boolean upper) {
-  lowerBoundZero(e) and b = 0 and upper = false
-  or
-  exists(Method read |
-    e.(MethodCall).getMethod().overrides*(read) and
-    read.getDeclaringType() instanceof TypeInputStream and
-    read.hasName("read") and
-    read.getNumberOfParameters() = 0
-  |
-    upper = true and b = 255
-    or
-    upper = false and b = -1
-  )
-}
-
-/**
- * Holds if the value being cast has an upper (for `upper = true`) or lower
- * (for `upper = false`) bound within the bounds of the resulting type.
- * For `upper = true` this means that the cast will not overflow and for
- * `upper = false` this means that the cast will not underflow.
- */
-private predicate safeNarrowingCast(NarrowingCastingExpr cast, boolean upper) {
-  exists(int bound | bounded(cast.getExpr(), any(ZeroBound zb), bound, upper, _, _, _) |
-    upper = true and bound <= cast.getUpperBound()
-    or
-    upper = false and bound >= cast.getLowerBound()
-  )
-}
-
-pragma[noinline]
-private predicate boundedCastExpr(
-  NarrowingCastingExpr cast, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
-  Reason reason
-) {
-  bounded(cast.getExpr(), b, delta, upper, fromBackEdge, origdelta, reason)
-}
-
-bindingset[f]
-private predicate okInt(float f) { -2.pow(31) <= f and f <= 2.pow(31) - 1 }
-
-/**
- * Holds if `b + delta` is a valid bound for `e`.
- * - `upper = true`  : `e <= b + delta`
- * - `upper = false` : `e >= b + delta`
- */
-private predicate bounded(
-  Expr e, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta, Reason reason
-) {
-  e = b.getExpr(delta) and
-  (upper = true or upper = false) and
-  fromBackEdge = false and
-  origdelta = delta and
-  reason = TNoReason()
-  or
-  baseBound(e, delta, upper) and
-  b instanceof ZeroBound and
-  fromBackEdge = false and
-  origdelta = delta and
-  reason = TNoReason()
-  or
-  exists(SsaVariable v, SsaReadPositionBlock bb |
-    boundedSsa(v, bb, b, delta, upper, fromBackEdge, origdelta, reason) and
-    e = v.getAUse() and
-    bb.getBlock() = e.getBasicBlock()
-  )
-  or
-  exists(Expr mid, int d1, int d2 |
-    boundFlowStep(e, mid, d1, upper) and
-    // Constants have easy, base-case bounds, so let's not infer any recursive bounds.
-    not e instanceof ConstantIntegerExpr and
-    bounded(mid, b, d2, upper, fromBackEdge, origdelta, reason) and
-    // upper = true:  e <= mid + d1 <= b + d1 + d2 = b + delta
-    // upper = false: e >= mid + d1 >= b + d1 + d2 = b + delta
-    delta = d1 + d2 and
-    okInt(d1.(float) + d2.(float))
-  )
-  or
-  exists(SsaPhiNode phi |
-    boundedPhi(phi, b, delta, upper, fromBackEdge, origdelta, reason) and
-    e = phi.getAUse()
-  )
-  or
-  exists(Expr mid, int factor, int d |
-    boundFlowStepMul(e, mid, factor) and
-    not e instanceof ConstantIntegerExpr and
-    bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
-    b instanceof ZeroBound and
-    delta = d * factor and
-    okInt(d.(float) * factor.(float))
-  )
-  or
-  exists(Expr mid, int factor, int d |
-    boundFlowStepDiv(e, mid, factor) and
-    not e instanceof ConstantIntegerExpr and
-    bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
-    b instanceof ZeroBound and
-    d >= 0 and
-    delta = d / factor
-  )
-  or
-  exists(NarrowingCastingExpr cast |
-    cast = e and
-    safeNarrowingCast(cast, upper.booleanNot()) and
-    boundedCastExpr(cast, b, delta, upper, fromBackEdge, origdelta, reason)
-  )
-  or
-  exists(
-    ConditionalExpr cond, int d1, int d2, boolean fbe1, boolean fbe2, int od1, int od2, Reason r1,
-    Reason r2
-  |
-    cond = e and
-    boundedConditionalExpr(cond, b, upper, true, d1, fbe1, od1, r1) and
-    boundedConditionalExpr(cond, b, upper, false, d2, fbe2, od2, r2) and
-    (
-      delta = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1
-      or
-      delta = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2
-    )
-  |
-    upper = true and delta = d1.maximum(d2)
-    or
-    upper = false and delta = d1.minimum(d2)
-  )
-  or
-  exists(
-    Bound b1, Bound b2, int d1, int d2, boolean fbe1, boolean fbe2, int od1, int od2, Reason r1,
-    Reason r2
-  |
-    boundedAddition(e, upper, b1, true, d1, fbe1, od1, r1) and
-    boundedAddition(e, upper, b2, false, d2, fbe2, od2, r2) and
-    delta = d1 + d2 and
-    fromBackEdge = fbe1.booleanOr(fbe2) and
-    okInt(d1.(float) + d2.(float))
-  |
-    b = b1 and origdelta = od1 and reason = r1 and b2 instanceof ZeroBound
-    or
-    b = b2 and origdelta = od2 and reason = r2 and b1 instanceof ZeroBound
-  )
-}
-
-private predicate boundedConditionalExpr(
-  ConditionalExpr cond, Bound b, boolean upper, boolean branch, int delta, boolean fromBackEdge,
-  int origdelta, Reason reason
-) {
-  bounded(cond.getBranchExpr(branch), b, delta, upper, fromBackEdge, origdelta, reason)
-}
-
-private predicate nonConstAdd(Expr add, Expr operand, boolean isLeft) {
-  exists(Expr other |
-    add.(AddExpr).getLeftOperand() = operand and
-    add.(AddExpr).getRightOperand() = other and
-    isLeft = true
-    or
-    add.(AddExpr).getLeftOperand() = other and
-    add.(AddExpr).getRightOperand() = operand and
-    isLeft = false
-    or
-    add.(AssignAddExpr).getDest() = operand and
-    add.(AssignAddExpr).getRhs() = other and
-    isLeft = true
-    or
-    add.(AssignAddExpr).getDest() = other and
-    add.(AssignAddExpr).getRhs() = operand and
-    isLeft = false
-  |
-    // `ConstantIntegerExpr` is covered by valueFlowStep
-    not other instanceof ConstantIntegerExpr and
-    not operand instanceof ConstantIntegerExpr
-  )
-}
-
-private predicate boundedAddition(
-  Expr add, boolean upper, Bound b, boolean isLeft, int delta, boolean fromBackEdge, int origdelta,
-  Reason reason
-) {
-  exists(Expr op |
-    nonConstAdd(add, op, isLeft) and
-    bounded(op, b, delta, upper, fromBackEdge, origdelta, reason)
-  )
-}

From 283d6efdf8d92e2abb4a2ab580155a225a3fe6a4 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Wed, 25 Oct 2023 14:06:35 +0200
Subject: [PATCH 12/14] Rangeanalysis/Java/C++: Address some ql4ql findings.

---
 .../semantic/analysis/SignAnalysisCommon.qll       |  4 ++--
 .../semmle/code/java/dataflow/RangeAnalysis.qll    | 14 +++++++-------
 .../codeql/rangeanalysis/RangeAnalysis.qll         |  4 ++--
 3 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
index 26e72d33e722..20ada012c2a4 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll
@@ -511,13 +511,13 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
 
   /**
    * Holds if `e` may have positive values. This does not rule out the
-   * possibilty for negative values.
+   * possibility for negative values.
    */
   predicate semMayBePositive(SemExpr e) { semExprSign(e) = TPos() }
 
   /**
    * Holds if `e` may have negative values. This does not rule out the
-   * possibilty for positive values.
+   * possibility for positive values.
    */
   predicate semMayBeNegative(SemExpr e) { semExprSign(e) = TNeg() }
 }
diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
index cd7a2c9c6e6c..2b2b539d5488 100644
--- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
@@ -81,7 +81,7 @@ module Sem implements Semantic {
   private import java as J
   private import SSA as SSA
   private import RangeUtils as RU
-  private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SSAReadPos
+  private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SsaReadPos
   private import semmle.code.java.controlflow.internal.GuardsLogic as GL
 
   class Expr = J::Expr;
@@ -230,18 +230,18 @@ module Sem implements Semantic {
 
   class SsaExplicitUpdate extends SsaVariable instanceof SSA::SsaExplicitUpdate { }
 
-  final private class FinalSsaReadPosition = SSAReadPos::SsaReadPosition;
+  final private class FinalSsaReadPosition = SsaReadPos::SsaReadPosition;
 
   class SsaReadPosition extends FinalSsaReadPosition {
     predicate hasReadOfVar(SsaVariable v) { super.hasReadOfVar(v) }
   }
 
-  class SsaReadPositionPhiInputEdge extends SsaReadPosition instanceof SSAReadPos::SsaReadPositionPhiInputEdge
+  class SsaReadPositionPhiInputEdge extends SsaReadPosition instanceof SsaReadPos::SsaReadPositionPhiInputEdge
   {
     predicate phiInput(SsaPhiNode phi, SsaVariable inp) { super.phiInput(phi, inp) }
   }
 
-  class SsaReadPositionBlock extends SsaReadPosition instanceof SSAReadPos::SsaReadPositionBlock {
+  class SsaReadPositionBlock extends SsaReadPosition instanceof SsaReadPos::SsaReadPositionBlock {
     BasicBlock getBlock() { result = super.getBlock() }
   }
 
@@ -374,7 +374,7 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
 
 module Utils implements UtilSig<Sem, IntDelta> {
   private import RangeUtils as RU
-  private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SSAReadPos
+  private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SsaReadPos
 
   Sem::Expr semSsaRead(Sem::SsaVariable v, int delta) { result = RU::ssaRead(v, delta) }
 
@@ -399,10 +399,10 @@ module Utils implements UtilSig<Sem, IntDelta> {
   predicate rankedPhiInput(
     Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, int r
   ) {
-    SSAReadPos::rankedPhiInput(phi, inp, edge, r)
+    SsaReadPos::rankedPhiInput(phi, inp, edge, r)
   }
 
-  predicate maxPhiInputRank(Sem::SsaPhiNode phi, int rix) { SSAReadPos::maxPhiInputRank(phi, rix) }
+  predicate maxPhiInputRank(Sem::SsaPhiNode phi, int rix) { SsaReadPos::maxPhiInputRank(phi, rix) }
 }
 
 module Bounds implements BoundSig<Location, Sem, IntDelta> {
diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
index b9ac86b3d3b0..50c0130ffcdb 100644
--- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
+++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
@@ -202,13 +202,13 @@ signature module SignAnalysisSig<Semantic Sem> {
 
   /**
    * Holds if `e` may have positive values. This does not rule out the
-   * possibilty for negative values.
+   * possibility for negative values.
    */
   predicate semMayBePositive(Sem::Expr e);
 
   /**
    * Holds if `e` may have negative values. This does not rule out the
-   * possibilty for positive values.
+   * possibility for positive values.
    */
   predicate semMayBeNegative(Sem::Expr e);
 }

From 5ded55cd9f7ae20fc2d1fe0930b348be2a742678 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Wed, 25 Oct 2023 14:08:48 +0200
Subject: [PATCH 13/14] C#: Sync Bound.qll

---
 .../lib/semmle/code/csharp/dataflow/Bound.qll | 22 +++++--------------
 1 file changed, 6 insertions(+), 16 deletions(-)

diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/Bound.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/Bound.qll
index b881161f66f5..08826b7ae8f1 100644
--- a/csharp/ql/lib/semmle/code/csharp/dataflow/Bound.qll
+++ b/csharp/ql/lib/semmle/code/csharp/dataflow/Bound.qll
@@ -25,16 +25,8 @@ abstract class Bound extends TBound {
   /** Gets an expression that equals this bound. */
   Expr getExpr() { result = this.getExpr(0) }
 
-  /**
-   * Holds if this element is at the specified location.
-   * The location spans column `sc` of line `sl` to
-   * column `ec` of line `el` in file `path`.
-   * For more information, see
-   * [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
-   */
-  predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
-    path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
-  }
+  /** Gets the location of this bound. */
+  abstract Location getLocation();
 }
 
 /**
@@ -45,6 +37,8 @@ class ZeroBound extends Bound, TBoundZero {
   override string toString() { result = "0" }
 
   override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }
+
+  override Location getLocation() { result.hasLocationInfo("", 0, 0, 0, 0) }
 }
 
 /**
@@ -58,9 +52,7 @@ class SsaBound extends Bound, TBoundSsa {
 
   override Expr getExpr(int delta) { result = this.getSsa().getAUse() and delta = 0 }
 
-  override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
-    this.getSsa().getLocation().hasLocationInfo(path, sl, sc, el, ec)
-  }
+  override Location getLocation() { result = this.getSsa().getLocation() }
 }
 
 /**
@@ -72,7 +64,5 @@ class ExprBound extends Bound, TBoundExpr {
 
   override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }
 
-  override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
-    this.getExpr().getLocation().hasLocationInfo(path, sl, sc, el, ec)
-  }
+  override Location getLocation() { result = this.getExpr().getLocation() }
 }

From 688250439711a09d828c4a21df2352948438b289 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Wed, 25 Oct 2023 14:31:49 +0200
Subject: [PATCH 14/14] C#: Fix compilation

---
 .../csharp/dataflow/internal/rangeanalysis/BoundSpecific.qll    | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/BoundSpecific.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/BoundSpecific.qll
index 3515f2f96c82..3885c11afd14 100644
--- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/BoundSpecific.qll
+++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/BoundSpecific.qll
@@ -12,6 +12,8 @@ class SsaVariable = SU::SsaVariable;
 
 class Expr = CS::ControlFlow::Nodes::ExprNode;
 
+class Location = CS::Location;
+
 class IntegralType = CS::IntegralType;
 
 class ConstantIntegerExpr = CU::ConstantIntegerExpr;