Merge pull request #14757 from aschackmull/rangeanalysis/simplify

Rangeanalysis: Misc simplifications

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

@@ -22,8 +22,6 @@ class SemSsaExplicitUpdate extends SemSsaVariable {
 
   SemSsaExplicitUpdate() { Specific::explicitUpdate(this, sourceExpr) }
 
-  final SemExpr getSourceExpr() { result = sourceExpr }
-
   final SemExpr getDefiningExpr() { result = sourceExpr }
 }
 

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

@@ -14,7 +14,7 @@ private predicate constantIntegerExpr(SemExpr e, int val) {
   // Copy of another constant
   exists(SemSsaExplicitUpdate v, SemExpr src |
     e = v.getAUse() and
-    src = v.getSourceExpr() and
+    src = v.getDefiningExpr() and
     constantIntegerExpr(src, val)
   )
   or

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

@@ -22,25 +22,7 @@ module CppLangImplConstant implements LangSig<Sem, FloatDelta> {
   predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() }
 
   /**
-   * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).
+   * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`).
    */
-  predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() }
-
-  /**
-   * Gets the type that range analysis should use to track the result of the specified expression,
-   * if a type other than the original type of the expression is to be used.
-   *
-   * 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) { none() }
-
-  /**
-   * Gets the type that range analysis should use to track the result of the specified source
-   * variable, if a type other than the original type of the expression is to be used.
-   *
-   * 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) { none() }
+  predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() }
 }

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

@@ -1,7 +1,6 @@
 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
@@ -88,6 +87,10 @@ module Sem implements Semantic {
 
   class AddressType = SemAddressType;
 
+  SemType getExprType(SemExpr e) { result = e.getSemType() }
+
+  SemType getSsaType(SemSsaVariable var) { result = var.getType() }
+
   class SsaVariable = SemSsaVariable;
 
   class SsaPhiNode = SemSsaPhiNode;
@@ -103,7 +106,7 @@ module Sem implements Semantic {
 
 module SignAnalysis implements SignAnalysisSig<Sem> {
   private import SignAnalysisCommon as SA
-  import SA::SignAnalysis<FloatDelta, Util>
+  import SA::SignAnalysis<FloatDelta>
 }
 
 module ConstantBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
@@ -166,18 +169,16 @@ private module ModulusAnalysisInstantiated implements ModulusAnalysisSig<Sem> {
   class ModBound = AllBounds::SemBound;
 
   private import codeql.rangeanalysis.ModulusAnalysis as MA
-  import MA::ModulusAnalysis<SemLocation, Sem, FloatDelta, AllBounds, Util>
+  import MA::ModulusAnalysis<SemLocation, Sem, FloatDelta, AllBounds>
 }
 
-module Util = RangeUtil<FloatDelta, CppLangImplConstant>;
-
 module ConstantStage =
   RangeStage<SemLocation, Sem, FloatDelta, ConstantBounds, FloatOverflow, CppLangImplConstant,
-    SignAnalysis, ModulusAnalysisInstantiated, Util>;
+    SignAnalysis, ModulusAnalysisInstantiated>;
 
 module RelativeStage =
   RangeStage<SemLocation, Sem, FloatDelta, RelativeBounds, FloatOverflow, CppLangImplRelative,
-    SignAnalysis, ModulusAnalysisInstantiated, Util>;
+    SignAnalysis, ModulusAnalysisInstantiated>;
 
 private newtype TSemReason =
   TSemNoReason() or

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

@@ -54,25 +54,7 @@ module CppLangImplRelative implements LangSig<Sem, FloatDelta> {
   predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() }
 
   /**
-   * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).
+   * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`).
    */
-  predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() }
-
-  /**
-   * Gets the type that range analysis should use to track the result of the specified expression,
-   * if a type other than the original type of the expression is to be used.
-   *
-   * 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) { none() }
-
-  /**
-   * Gets the type that range analysis should use to track the result of the specified source
-   * variable, if a type other than the original type of the expression is to be used.
-   *
-   * 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) { none() }
+  predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() }
 }

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

@@ -1,35 +0,0 @@
-/**
- * Provides utility predicates for range analysis.
- */
-
-private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
-private import RangeAnalysisRelativeSpecific
-private import codeql.rangeanalysis.RangeAnalysis
-private import RangeAnalysisImpl
-private import ConstantAnalysis
-
-module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
-  /**
-   * Gets the type used to track the specified expression's range information.
-   *
-   * 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) {
-    result = Lang::getAlternateType(e)
-    or
-    not exists(Lang::getAlternateType(e)) and result = e.getSemType()
-  }
-
-  /**
-   * Gets the type used to track the specified source variable's range information.
-   *
-   * 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) {
-    result = Lang::getAlternateTypeForSsaVariable(var)
-    or
-    not exists(Lang::getAlternateTypeForSsaVariable(var)) and result = var.getType()
-  }
-}

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

@@ -11,10 +11,9 @@ 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<Sem, D> Utils> {
+module SignAnalysis<DeltaSig D> {
   private import codeql.rangeanalysis.internal.RangeUtils::MakeUtils<Sem, D>
 
   /**
@@ -39,7 +38,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
 
   /** An SSA definition whose sign is determined by the sign of that definitions source expression. */
   private class ExplicitSignDef extends FlowSignDef instanceof SemSsaExplicitUpdate {
-    final override Sign getSign() { result = semExprSign(super.getSourceExpr()) }
+    final override Sign getSign() { result = semExprSign(super.getDefiningExpr()) }
   }
 
   /** An SSA Phi definition, whose sign is the union of the signs of its inputs. */
@@ -148,7 +147,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
       not this instanceof ConstantSignExpr and
       (
         // Only track numeric types.
-        Utils::getTrackedType(this) instanceof SemNumericType
+        Sem::getExprType(this) instanceof SemNumericType
         or
         // Unless the language says to track this expression anyway.
         Specific::trackUnknownNonNumericExpr(this)
@@ -203,7 +202,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
 
   /** An expression of an unsigned type. */
   private class UnsignedExpr extends FlowSignExpr {
-    UnsignedExpr() { Utils::getTrackedType(this) instanceof SemUnsignedIntegerType }
+    UnsignedExpr() { Sem::getExprType(this) instanceof SemUnsignedIntegerType }
 
     override Sign getSignRestriction() {
       result = TPos() or
@@ -276,7 +275,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
     override SemUnboxExpr cast;
 
     UnboxSignExpr() {
-      exists(SemType fromType | fromType = Utils::getTrackedType(cast.getOperand()) |
+      exists(SemType fromType | fromType = Sem::getExprType(cast.getOperand()) |
         // Only numeric source types are handled here.
         fromType instanceof SemNumericType
       )
@@ -471,7 +470,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
   Sign semExprSign(SemExpr e) {
     exists(Sign s | s = e.(SignExpr).getSign() |
       if
-        Utils::getTrackedType(e) instanceof SemUnsignedIntegerType and
+        Sem::getExprType(e) instanceof SemUnsignedIntegerType and
         s = TNeg() and
         not Specific::ignoreTypeRestrictions(e)
       then result = TPos()

cpp/ql/test/library-tests/ir/modulus-analysis/ModulusAnalysis.ql

@@ -2,7 +2,6 @@ import cpp
 import codeql.rangeanalysis.ModulusAnalysis
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticLocation
-import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeUtils
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysisRelativeSpecific
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysisImpl
@@ -10,9 +9,7 @@ import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
 import semmle.code.cpp.ir.IR as IR
 import TestUtilities.InlineExpectationsTest
 
-module ModulusAnalysisInstantiated =
-  ModulusAnalysis<SemLocation, Sem, FloatDelta, ConstantBounds,
-    RangeUtil<FloatDelta, CppLangImplRelative>>;
+module ModulusAnalysisInstantiated = ModulusAnalysis<SemLocation, Sem, FloatDelta, ConstantBounds>;
 
 module ModulusAnalysisTest implements TestSig {
   string getARelevantTag() { result = "mod" }

cpp/ql/test/library-tests/ir/sign-analysis/SignAnalysis.ql

@@ -1,15 +1,13 @@
 import cpp
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.SignAnalysisCommon
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
-import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeUtils
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysisRelativeSpecific
 import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
 import semmle.code.cpp.ir.IR as IR
 import TestUtilities.InlineExpectationsTest
 
-module SignAnalysisInstantiated =
-  SignAnalysis<FloatDelta, RangeUtil<FloatDelta, CppLangImplRelative>>;
+module SignAnalysisInstantiated = SignAnalysis<FloatDelta>;
 
 module SignAnalysisTest implements TestSig {
   string getARelevantTag() { result = "sign" }

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

@@ -6,7 +6,6 @@ import java
 import SSA
 private import semmle.code.java.controlflow.internal.GuardsLogic
 private import semmle.code.java.frameworks.apache.Collections
-private import RangeUtils
 private import IntegerGuards
 
 /** Gets an expression that is always `null`. */

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

@@ -241,6 +241,10 @@ module Sem implements Semantic {
     AddressType() { none() }
   }
 
+  Type getExprType(Expr e) { result = e.getType() }
+
+  Type getSsaType(SsaVariable var) { result = var.getSourceVariable().getType() }
+
   final private class FinalSsaVariable = SSA::SsaVariable;
 
   class SsaVariable extends FinalSsaVariable {
@@ -281,7 +285,7 @@ module Modulus implements ModulusAnalysisSig<Sem> {
   class ModBound = Bound;
 
   private import codeql.rangeanalysis.ModulusAnalysis as Mod
-  import Mod::ModulusAnalysis<Location, Sem, IntDelta, Bounds, Utils>
+  import Mod::ModulusAnalysis<Location, Sem, IntDelta, Bounds>
 }
 
 module IntDelta implements DeltaSig {
@@ -332,7 +336,7 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
   /**
    * 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) {
+  predicate additionalBoundFlowStep(Sem::Expr e2, Sem::Expr e1, int delta, boolean upper) {
     exists(RandomDataSource rds |
       e2 = rds.getOutput() and
       (
@@ -362,21 +366,9 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
 
   predicate ignoreExprBound(Sem::Expr e) { none() }
 
-  Sem::Type getAlternateType(Sem::Expr e) { none() }
-
-  Sem::Type getAlternateTypeForSsaVariable(Sem::SsaVariable var) { none() }
-
   predicate javaCompatibility() { any() }
 }
 
-module Utils implements UtilSig<Sem, IntDelta> {
-  Sem::Type getTrackedTypeForSsaVariable(Sem::SsaVariable var) {
-    result = var.getSourceVariable().getType()
-  }
-
-  Sem::Type getTrackedType(Sem::Expr e) { result = e.getType() }
-}
-
 module Bounds implements BoundSig<Location, Sem, IntDelta> {
   class SemBound = Bound;
 
@@ -394,7 +386,7 @@ module Overflow implements OverflowSig<Sem, IntDelta> {
 }
 
 module Range =
-  RangeStage<Location, Sem, IntDelta, Bounds, Overflow, JavaLangImpl, SignInp, Modulus, Utils>;
+  RangeStage<Location, Sem, IntDelta, Bounds, Overflow, JavaLangImpl, SignInp, Modulus>;
 
 predicate bounded = Range::semBounded/5;
 

shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll

@@ -14,8 +14,7 @@ private import codeql.util.Location
 private import RangeAnalysis
 
 module ModulusAnalysis<
-  LocationSig Location, Semantic Sem, DeltaSig D, BoundSig<Location, Sem, D> Bounds,
-  UtilSig<Sem, D> U>
+  LocationSig Location, Semantic Sem, DeltaSig D, BoundSig<Location, Sem, D> Bounds>
 {
   private import internal.RangeUtils::MakeUtils<Sem, D>
 
@@ -254,8 +253,7 @@ module ModulusAnalysis<
     or
     exists(Sem::SsaVariable v, SsaReadPositionBlock bb |
       ssaModulus(v, bb, b, val, mod) and
-      e = v.getAUse() and
-      bb.getBlock() = e.getBasicBlock()
+      bb.getAnSsaRead(v) = e
     )
     or
     exists(Sem::Expr mid, int val0, int delta |

shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

@@ -188,6 +188,12 @@ signature module Semantic {
 
   class AddressType extends Type;
 
+  /** Gets the type of an SSA variable. */
+  Type getSsaType(SsaVariable var);
+
+  /** Gets the type of an expression. */
+  Type getExprType(Expr e);
+
   class SsaVariable {
     Expr getAUse();
 
@@ -270,9 +276,9 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
   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`).
+   * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`).
    */
-  predicate hasBound(Sem::Expr e, Sem::Expr bound, D::Delta delta, boolean upper);
+  predicate additionalBoundFlowStep(Sem::Expr e2, Sem::Expr e1, D::Delta delta, boolean upper);
 
   /**
    * Ignore the bound on this expression.
@@ -282,45 +288,9 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
    */
   predicate ignoreExprBound(Sem::Expr e);
 
-  /**
-   * Gets the type that range analysis should use to track the result of the specified expression,
-   * if a type other than the original type of the expression is to be used.
-   *
-   * 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.
-   */
-  Sem::Type getAlternateType(Sem::Expr e);
-
-  /**
-   * Gets the type that range analysis should use to track the result of the specified source
-   * variable, if a type other than the original type of the expression is to be used.
-   *
-   * 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.
-   */
-  Sem::Type getAlternateTypeForSsaVariable(Sem::SsaVariable var);
-
   default predicate javaCompatibility() { none() }
 }
 
-signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> {
-  /**
-   * Gets the type used to track the specified source variable's range information.
-   *
-   * Usually, this just `e.getType()`, but the language can override this to track immutable boxed
-   * primitive types as the underlying primitive type.
-   */
-  Sem::Type getTrackedTypeForSsaVariable(Sem::SsaVariable var);
-
-  /**
-   * Gets the type used to track the specified expression's range information.
-   *
-   * Usually, this just `e.getSemType()`, but the language can override this to track immutable boxed
-   * primitive types as the underlying primitive type.
-   */
-  Sem::Type getTrackedType(Sem::Expr e);
-}
-
 signature module BoundSig<LocationSig Location, Semantic Sem, DeltaSig D> {
   class SemBound {
     string toString();
@@ -344,11 +314,10 @@ signature module OverflowSig<Semantic Sem, DeltaSig D> {
 module RangeStage<
   LocationSig Location, Semantic Sem, DeltaSig D, BoundSig<Location, Sem, D> Bounds,
   OverflowSig<Sem, D> OverflowParam, LangSig<Sem, D> LangParam, SignAnalysisSig<Sem> SignAnalysis,
-  ModulusAnalysisSig<Sem> ModulusAnalysisParam, UtilSig<Sem, D> UtilParam>
+  ModulusAnalysisSig<Sem> ModulusAnalysisParam>
 {
   private import Bounds
   private import LangParam
-  private import UtilParam
   private import D
   private import OverflowParam
   private import SignAnalysis
@@ -393,8 +362,8 @@ module RangeStage<
    */
   private class SafeCastExpr extends ConvertOrBoxExpr {
     SafeCastExpr() {
-      Sem::conversionCannotOverflow(getTrackedType(pragma[only_bind_into](this.getOperand())),
-        pragma[only_bind_out](getTrackedType(this)))
+      Sem::conversionCannotOverflow(Sem::getExprType(pragma[only_bind_into](this.getOperand())),
+        pragma[only_bind_out](Sem::getExprType(this)))
     }
   }
 
@@ -404,14 +373,14 @@ module RangeStage<
   private class NarrowingCastExpr extends ConvertOrBoxExpr {
     NarrowingCastExpr() {
       not this instanceof SafeCastExpr and
-      typeBound(getTrackedType(this), _, _)
+      typeBound(Sem::getExprType(this), _, _)
     }
 
     /** Gets the lower bound of the resulting type. */
-    float getLowerBound() { typeBound(getTrackedType(this), result, _) }
+    float getLowerBound() { typeBound(Sem::getExprType(this), result, _) }
 
     /** Gets the upper bound of the resulting type. */
-    float getUpperBound() { typeBound(getTrackedType(this), _, result) }
+    float getUpperBound() { typeBound(Sem::getExprType(this), _, result) }
   }
 
   cached
@@ -574,8 +543,8 @@ module RangeStage<
       ) and
       (
         if
-          getTrackedTypeForSsaVariable(v) instanceof Sem::IntegerType or
-          getTrackedTypeForSsaVariable(v) instanceof Sem::AddressType
+          Sem::getSsaType(v) instanceof Sem::IntegerType or
+          Sem::getSsaType(v) instanceof Sem::AddressType
         then
           upper = true and strengthen = -1
           or
@@ -684,7 +653,7 @@ module RangeStage<
   private predicate unequalFlowStepIntegralSsa(
     Sem::SsaVariable v, SsaReadPosition pos, Sem::Expr e, D::Delta delta, SemReason reason
   ) {
-    getTrackedTypeForSsaVariable(v) instanceof Sem::IntegerType and
+    Sem::getSsaType(v) instanceof Sem::IntegerType and
     exists(Sem::Guard guard, boolean testIsTrue |
       pos.hasReadOfVar(v) and
       guard = eqFlowCond(v, e, delta, false, testIsTrue) and
@@ -695,12 +664,12 @@ 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
+    semStrictlyPositive(e) and Sem::getExprType(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
+    semStrictlyNegative(e) and Sem::getExprType(e) instanceof Sem::IntegerType
   }
 
   /**
@@ -758,7 +727,7 @@ module RangeStage<
     delta = D::fromInt(0) and
     upper = false
     or
-    hasBound(e2, e1, delta, upper)
+    additionalBoundFlowStep(e2, e1, delta, upper)
   }
 
   /** Holds if `e2 = e1 * factor` and `factor > 0`. */
@@ -782,7 +751,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
+    Sem::getExprType(e2) instanceof Sem::IntegerType and
     exists(Sem::ConstantIntegerExpr c, D::Delta k |
       k = D::fromInt(c.getIntValue()) and D::toFloat(k) > 0
     |
@@ -825,11 +794,9 @@ module RangeStage<
     )
     or
     exists(D::Delta d, SemReason r1, SemReason r2 |
-      boundedSsa(pragma[only_bind_into](v), pragma[only_bind_into](b), pragma[only_bind_into](d),
-        pragma[only_bind_into](pos), upper, fromBackEdge, origdelta, r2)
+      boundedSsa(v, b, d, pos, upper, fromBackEdge, origdelta, r2)
       or
-      boundedPhi(pragma[only_bind_into](v), pragma[only_bind_into](b), pragma[only_bind_into](d),
-        upper, fromBackEdge, origdelta, r2)
+      boundedPhi(v, b, d, upper, fromBackEdge, origdelta, r2)
     |
       unequalIntegralSsa(v, b, d, pos, r1) and
       (
@@ -853,32 +820,12 @@ module RangeStage<
   ) {
     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
+      bounded(e, b, d2, true, _, _, _) and
+      bounded(e, b, d2, false, _, _, _) and
       delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2))
     )
   }
 
-  /**
-   * Holds if `b + delta` is an upper bound for `e`.
-   *
-   * This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
-   */
-  pragma[nomagic]
-  private predicate boundedUpper(Sem::Expr e, SemBound b, D::Delta delta) {
-    bounded(e, b, delta, true, _, _, _)
-  }
-
-  /**
-   * Holds if `b + delta` is a lower bound for `e`.
-   *
-   * This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
-   */
-  pragma[nomagic]
-  private predicate boundedLower(Sem::Expr e, SemBound b, D::Delta delta) {
-    bounded(e, b, delta, false, _, _, _)
-  }
-
   /** Weakens a delta to lie in the range `[-1..1]`. */
   bindingset[delta, upper]
   private D::Delta weakenDelta(boolean upper, D::Delta delta) {
@@ -1141,7 +1088,7 @@ module RangeStage<
     (
       expr instanceof Sem::NegateExpr or
       expr instanceof Sem::PreDecExpr or
-      getTrackedType(expr.(Sem::DivExpr)) instanceof Sem::FloatingPointType
+      Sem::getExprType(expr.(Sem::DivExpr)) instanceof Sem::FloatingPointType
     )
     or
     positively = true and
@@ -1185,8 +1132,7 @@ module RangeStage<
       or
       exists(Sem::SsaVariable v, SsaReadPositionBlock bb |
         boundedSsa(v, b, delta, bb, upper, fromBackEdge, origdelta, reason) and
-        e = v.getAUse() and
-        bb.getBlock() = e.getBasicBlock()
+        bb.getAnSsaRead(v) = e
       )
       or
       exists(Sem::Expr mid, D::Delta d1, D::Delta d2 |