Merge pull request #14656 from aschackmull/shared/range-utils

Rangeanalysis: Share ssaRead predicate

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

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

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

@@ -151,7 +151,7 @@ module ModulusAnalysis<DeltaSig D, BoundSig<SemLocation, Sem, D> Bounds, UtilSig
   ) {
     exists(Bounds::SemSsaBound phibound, int v, int m |
       edge.phiInput(phi, inp) and
-      phibound.getAVariable() = phi and
+      phibound.getVariable() = phi and
       ssaModulus(inp, edge, phibound, v, m) and
       mod = m.gcd(v) and
       mod != 1
@@ -233,7 +233,7 @@ module ModulusAnalysis<DeltaSig D, BoundSig<SemLocation, Sem, D> Bounds, UtilSig
   ) {
     phiModulus(v, b, val, mod) and pos.hasReadOfVar(v)
     or
-    b.(Bounds::SemSsaBound).getAVariable() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0
+    b.(Bounds::SemSsaBound).getVariable() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0
     or
     exists(SemExpr e, int val0, int delta |
       semExprModulus(e, b, val0, mod) and

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

@@ -8,14 +8,6 @@ private import RangeAnalysisImpl
 private import codeql.rangeanalysis.RangeAnalysis
 
 module CppLangImplConstant implements LangSig<Sem, FloatDelta> {
-  /**
-   * 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) { none() }
-
   /**
    * Ignore the bound on this expression.
    *
@@ -24,40 +16,6 @@ module CppLangImplConstant implements LangSig<Sem, FloatDelta> {
    */
   predicate ignoreExprBound(SemExpr e) { none() }
 
-  /**
-   * Ignore any inferred zero lower bound on this expression.
-   *
-   * 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) { none() }
-
-  /**
-   * 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 ignoreSsaReadArithmeticExpr(SemExpr e) { none() }
-
-  /**
-   * Holds if the specified variable 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 ignoreSsaReadAssignment(SemSsaVariable v) { none() }
-
-  /**
-   * Adds additional results to `ssaRead()` that are specific to Java.
-   *
-   * This predicate handles propagation of offsets for post-increment and post-decrement expressions
-   * in exactly the same way as the old Java implementation. Once the new implementation matches the
-   * 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, float delta) { none() }
-
   /**
    * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
    */

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

@@ -52,9 +52,21 @@ module Sem implements Semantic {
 
   class NegateExpr = SemNegateExpr;
 
-  class AddOneExpr = SemAddOneExpr;
+  class PreIncExpr = SemAddOneExpr;
 
-  class SubOneExpr = SemSubOneExpr;
+  class PreDecExpr = SemSubOneExpr;
+
+  class PostIncExpr extends SemUnaryExpr {
+    PostIncExpr() { none() }
+  }
+
+  class PostDecExpr extends SemUnaryExpr {
+    PostDecExpr() { none() }
+  }
+
+  class CopyValueExpr extends SemUnaryExpr {
+    CopyValueExpr() { this instanceof SemCopyValueExpr or this instanceof SemStoreExpr }
+  }
 
   class ConditionalExpr = SemConditionalExpr;
 
@@ -116,7 +128,7 @@ module ConstantBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
   class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { }
 
   class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound {
-    SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
+    SemSsaVariable getVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
   }
 }
 
@@ -134,7 +146,7 @@ module RelativeBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
   class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { }
 
   class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound {
-    SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
+    SemSsaVariable getVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
   }
 }
 
@@ -150,7 +162,7 @@ module AllBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
   class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { }
 
   class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound {
-    SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
+    SemSsaVariable getVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
   }
 }
 

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

@@ -9,14 +9,6 @@ private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
 private import codeql.rangeanalysis.RangeAnalysis
 
 module CppLangImplRelative implements LangSig<Sem, FloatDelta> {
-  /**
-   * 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) { none() }
-
   /**
    * Ignore the bound on this expression.
    *
@@ -56,40 +48,6 @@ module CppLangImplRelative implements LangSig<Sem, FloatDelta> {
     t instanceof SemFloatingPointType and lb = -(1.0 / 0.0) and ub = 1.0 / 0.0
   }
 
-  /**
-   * Ignore any inferred zero lower bound on this expression.
-   *
-   * 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) { none() }
-
-  /**
-   * 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 ignoreSsaReadArithmeticExpr(SemExpr e) { none() }
-
-  /**
-   * Holds if the specified variable 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 ignoreSsaReadAssignment(SemSsaVariable v) { none() }
-
-  /**
-   * Adds additional results to `ssaRead()` that are specific to Java.
-   *
-   * This predicate handles propagation of offsets for post-increment and post-decrement expressions
-   * in exactly the same way as the old Java implementation. Once the new implementation matches the
-   * 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, float delta) { none() }
-
   /**
    * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
    */

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

@@ -12,33 +12,27 @@ module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
   /**
    * Gets an expression that equals `v - d`.
    */
-  SemExpr semSsaRead(SemSsaVariable v, D::Delta delta) {
+  private SemExpr semSsaRead(SemSsaVariable v, D::Delta delta) {
     // There are various language-specific extension points that can be removed once we no longer
     // expect to match the original Java implementation's results exactly.
     result = v.getAUse() and delta = D::fromInt(0)
     or
     exists(D::Delta d1, SemConstantIntegerExpr c |
       result.(SemAddExpr).hasOperands(semSsaRead(v, d1), c) and
-      delta = D::fromFloat(D::toFloat(d1) - c.getIntValue()) and
+      delta = D::fromFloat(D::toFloat(d1) - c.getIntValue())
-      not Lang::ignoreSsaReadArithmeticExpr(result)
     )
     or
     exists(SemSubExpr sub, D::Delta d1, SemConstantIntegerExpr c |
       result = sub and
       sub.getLeftOperand() = semSsaRead(v, d1) and
       sub.getRightOperand() = c and
-      delta = D::fromFloat(D::toFloat(d1) + c.getIntValue()) and
+      delta = D::fromFloat(D::toFloat(d1) + c.getIntValue())
-      not Lang::ignoreSsaReadArithmeticExpr(result)
     )
     or
     result = v.(SemSsaExplicitUpdate).getSourceExpr() and
-    delta = D::fromFloat(0) and
+    delta = D::fromFloat(0)
-    not Lang::ignoreSsaReadAssignment(v)
     or
-    result = Lang::specificSsaRead(v, delta)
+    result.(SemCopyValueExpr).getOperand() = semSsaRead(v, delta)
-    or
-    result.(SemCopyValueExpr).getOperand() = semSsaRead(v, delta) and
-    not Lang::ignoreSsaReadCopy(result)
     or
     result.(SemStoreExpr).getOperand() = semSsaRead(v, delta)
   }

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

@@ -15,6 +15,8 @@ private import RangeUtils
 private import Sign
 
 module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
+  private import codeql.rangeanalysis.internal.RangeUtils::MakeUtils<Sem, D>
+
   /**
    * An SSA definition for which the analysis can compute the sign.
    *
@@ -297,12 +299,12 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
     |
       testIsTrue = true and
       comp.getLesserOperand() = lowerbound and
-      comp.getGreaterOperand() = Utils::semSsaRead(v, D::fromInt(0)) and
+      comp.getGreaterOperand() = ssaRead(v, D::fromInt(0)) and
       (if comp.isStrict() then isStrict = true else isStrict = false)
       or
       testIsTrue = false and
       comp.getGreaterOperand() = lowerbound and
-      comp.getLesserOperand() = Utils::semSsaRead(v, D::fromInt(0)) and
+      comp.getLesserOperand() = ssaRead(v, D::fromInt(0)) and
       (if comp.isStrict() then isStrict = false else isStrict = true)
     )
   }
@@ -321,12 +323,12 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
     |
       testIsTrue = true and
       comp.getGreaterOperand() = upperbound and
-      comp.getLesserOperand() = Utils::semSsaRead(v, D::fromInt(0)) and
+      comp.getLesserOperand() = ssaRead(v, D::fromInt(0)) and
       (if comp.isStrict() then isStrict = true else isStrict = false)
       or
       testIsTrue = false and
       comp.getLesserOperand() = upperbound and
-      comp.getGreaterOperand() = Utils::semSsaRead(v, D::fromInt(0)) and
+      comp.getGreaterOperand() = ssaRead(v, D::fromInt(0)) and
       (if comp.isStrict() then isStrict = false else isStrict = true)
     )
   }
@@ -342,7 +344,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
     exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e |
       pos.hasReadOfVar(pragma[only_bind_into](v)) and
       semGuardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
-      e = Utils::semSsaRead(pragma[only_bind_into](v), D::fromInt(0)) and
+      e = ssaRead(pragma[only_bind_into](v), D::fromInt(0)) and
       guard.isEquality(eqbound, e, polarity) and
       isEq = polarity.booleanXor(testIsTrue).booleanNot() and
       not unknownSign(eqbound)

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

@@ -150,6 +150,8 @@ module Sem implements Semantic {
     }
   }
 
+  predicate isAssignOp(BinaryExpr bin) { bin instanceof AssignOp }
+
   class RelationalExpr = J::ComparisonExpr;
 
   abstract class UnaryExpr extends Expr {
@@ -176,18 +178,34 @@ module Sem implements Semantic {
     override Expr getOperand() { result = super.getExpr() }
   }
 
-  // TODO: Implement once utils are properly shared
+  class PreIncExpr extends UnaryExpr instanceof J::PreIncExpr {
-  class AddOneExpr extends UnaryExpr {
+    override Expr getOperand() { result = super.getExpr() }
-    AddOneExpr() { none() }
-
-    override Expr getOperand() { none() }
   }
 
-  // TODO: Implement once utils are properly shared
+  class PreDecExpr extends UnaryExpr instanceof J::PreDecExpr {
-  class SubOneExpr extends UnaryExpr {
+    override Expr getOperand() { result = super.getExpr() }
-    SubOneExpr() { none() }
+  }
 
-    override Expr getOperand() { none() }
+  class PostIncExpr extends UnaryExpr instanceof J::PostIncExpr {
+    override Expr getOperand() { result = super.getExpr() }
+  }
+
+  class PostDecExpr extends UnaryExpr instanceof J::PostDecExpr {
+    override Expr getOperand() { result = super.getExpr() }
+  }
+
+  class CopyValueExpr extends UnaryExpr {
+    CopyValueExpr() {
+      this instanceof J::PlusExpr or
+      this instanceof J::AssignExpr or
+      this instanceof LocalVariableDeclExpr
+    }
+
+    override Expr getOperand() {
+      result = this.(J::PlusExpr).getExpr() or
+      result = this.(J::AssignExpr).getSource() or
+      result = this.(J::LocalVariableDeclExpr).getInit()
+    }
   }
 
   class ConditionalExpr = J::ConditionalExpr;
@@ -228,7 +246,9 @@ module Sem implements Semantic {
 
   class SsaPhiNode extends SsaVariable instanceof SSA::SsaPhiNode { }
 
-  class SsaExplicitUpdate extends SsaVariable instanceof SSA::SsaExplicitUpdate { }
+  class SsaExplicitUpdate extends SsaVariable instanceof SSA::SsaExplicitUpdate {
+    Expr getDefiningExpr() { result = super.getDefiningExpr() }
+  }
 
   final private class FinalSsaReadPosition = SsaReadPos::SsaReadPosition;
 
@@ -295,8 +315,6 @@ module IntDelta implements DeltaSig {
 }
 
 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`).
    */
@@ -355,14 +373,6 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
 
   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() }
@@ -376,8 +386,6 @@ 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
   ) {
@@ -411,7 +419,7 @@ module Bounds implements BoundSig<Location, Sem, IntDelta> {
   class SemZeroBound = ZeroBound;
 
   class SemSsaBound extends SsaBound {
-    Sem::SsaVariable getAVariable() { result = super.getSsa() }
+    Sem::SsaVariable getVariable() { result = super.getSsa() }
   }
 }
 

shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

@@ -106,6 +106,8 @@ signature module Semantic {
 
   class ShiftRightUnsignedExpr extends BinaryExpr;
 
+  default predicate isAssignOp(BinaryExpr bin) { none() }
+
   class RelationalExpr extends Expr {
     Expr getLesserOperand();
 
@@ -126,9 +128,15 @@ signature module Semantic {
 
   class NegateExpr extends UnaryExpr;
 
-  class AddOneExpr extends UnaryExpr;
+  class PreIncExpr extends UnaryExpr;
 
-  class SubOneExpr extends UnaryExpr;
+  class PreDecExpr extends UnaryExpr;
+
+  class PostIncExpr extends UnaryExpr;
+
+  class PostDecExpr extends UnaryExpr;
+
+  class CopyValueExpr extends UnaryExpr;
 
   class ConditionalExpr extends Expr {
     Expr getBranchExpr(boolean branch);
@@ -168,7 +176,9 @@ signature module Semantic {
 
   class SsaPhiNode extends SsaVariable;
 
-  class SsaExplicitUpdate extends SsaVariable;
+  class SsaExplicitUpdate extends SsaVariable {
+    Expr getDefiningExpr();
+  }
 
   class SsaReadPosition {
     predicate hasReadOfVar(SsaVariable v);
@@ -240,14 +250,6 @@ signature module DeltaSig {
 }
 
 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(Sem::Expr e);
-
   /**
    * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
    */
@@ -266,40 +268,6 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
    */
   predicate ignoreExprBound(Sem::Expr e);
 
-  /**
-   * Ignore any inferred zero lower bound on this expression.
-   *
-   * 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(Sem::Expr e);
-
-  /**
-   * 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 ignoreSsaReadArithmeticExpr(Sem::Expr e);
-
-  /**
-   * Holds if the specified variable 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 ignoreSsaReadAssignment(Sem::SsaVariable v);
-
-  /**
-   * Adds additional results to `ssaRead()` that are specific to Java.
-   *
-   * This predicate handles propagation of offsets for post-increment and post-decrement expressions
-   * in exactly the same way as the old Java implementation. Once the new implementation matches the
-   * 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.
-   */
-  Sem::Expr specificSsaRead(Sem::SsaVariable v, D::Delta delta);
-
   /**
    * Holds if the value of `dest` is known to be `src + delta`.
    */
@@ -327,8 +295,6 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
 }
 
 signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> {
-  Sem::Expr semSsaRead(Sem::SsaVariable v, DeltaParam::Delta delta);
-
   Sem::Guard semEqFlowCond(
     Sem::SsaVariable v, Sem::Expr e, DeltaParam::Delta delta, boolean isEq, boolean testIsTrue
   );
@@ -379,7 +345,7 @@ signature module BoundSig<LocationSig Location, Semantic Sem, DeltaSig D> {
   class SemZeroBound extends SemBound;
 
   class SemSsaBound extends SemBound {
-    Sem::SsaVariable getAVariable();
+    Sem::SsaVariable getVariable();
   }
 }
 
@@ -399,6 +365,7 @@ module RangeStage<
   private import OverflowParam
   private import SignAnalysis
   private import ModulusAnalysis
+  private import internal.RangeUtils::MakeUtils<Sem, D>
 
   /**
    * An expression that does conversion, boxing, or unboxing
@@ -512,11 +479,11 @@ module RangeStage<
   private predicate boundCondition(
     Sem::RelationalExpr comp, Sem::SsaVariable v, Sem::Expr e, D::Delta delta, boolean upper
   ) {
-    comp.getLesserOperand() = semSsaRead(v, delta) and
+    comp.getLesserOperand() = ssaRead(v, delta) and
     e = comp.getGreaterOperand() and
     upper = true
     or
-    comp.getGreaterOperand() = semSsaRead(v, delta) and
+    comp.getGreaterOperand() = ssaRead(v, delta) and
     e = comp.getLesserOperand() and
     upper = false
     or
@@ -524,7 +491,7 @@ module RangeStage<
       // (v - d) - e < c
       comp.getLesserOperand() = sub and
       comp.getGreaterOperand() = c and
-      sub.getLeftOperand() = semSsaRead(v, d) and
+      sub.getLeftOperand() = ssaRead(v, d) and
       sub.getRightOperand() = e and
       upper = true and
       delta = D::fromFloat(D::toFloat(d) + c.getIntValue())
@@ -532,7 +499,7 @@ module RangeStage<
       // (v - d) - e > c
       comp.getGreaterOperand() = sub and
       comp.getLesserOperand() = c and
-      sub.getLeftOperand() = semSsaRead(v, d) and
+      sub.getLeftOperand() = ssaRead(v, d) and
       sub.getRightOperand() = e and
       upper = false and
       delta = D::fromFloat(D::toFloat(d) + c.getIntValue())
@@ -541,7 +508,7 @@ module RangeStage<
       comp.getLesserOperand() = sub and
       comp.getGreaterOperand() = c and
       sub.getLeftOperand() = e and
-      sub.getRightOperand() = semSsaRead(v, d) and
+      sub.getRightOperand() = ssaRead(v, d) and
       upper = false and
       delta = D::fromFloat(D::toFloat(d) - c.getIntValue())
       or
@@ -549,7 +516,7 @@ module RangeStage<
       comp.getGreaterOperand() = sub and
       comp.getLesserOperand() = c and
       sub.getLeftOperand() = e and
-      sub.getRightOperand() = semSsaRead(v, d) and
+      sub.getRightOperand() = ssaRead(v, d) and
       upper = true and
       delta = D::fromFloat(D::toFloat(d) - c.getIntValue())
     )
@@ -667,7 +634,7 @@ module RangeStage<
     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
+      guardEq = semEqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
       delta = D::toFloat(d2) - D::toFloat(d1) and
       guardEq.directlyControls(result, eqIsTrue)
     )
@@ -950,7 +917,7 @@ module RangeStage<
       or
       boundedPhi(inp, b, d, upper, fromBackEdge0, origdelta, reason)
       or
-      b.(SemSsaBound).getAVariable() = inp and
+      b.(SemSsaBound).getVariable() = inp and
       d = D::fromFloat(0) and
       (upper = true or upper = false) and
       fromBackEdge0 = false and
@@ -1000,7 +967,7 @@ module RangeStage<
     Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, boolean upper
   ) {
     exists(D::Delta d, SemSsaBound phibound |
-      phibound.getAVariable() = phi and
+      phibound.getVariable() = phi and
       boundedPhiInp(phi, inp, edge, phibound, d, upper, _, _, _) and
       (
         upper = true and D::toFloat(d) <= 0
@@ -1091,9 +1058,7 @@ module RangeStage<
     or
     upper = false and
     b = D::fromInt(0) and
-    semPositive(e.(Sem::BitAndExpr).getAnOperand()) and
+    semPositive(e.(Sem::BitAndExpr).getAnOperand())
-    // REVIEW: We let the language opt out here to preserve original results.
-    not ignoreZeroLowerBound(e)
   }
 
   /**
@@ -1188,12 +1153,12 @@ module RangeStage<
     positively = false and
     (
       expr instanceof Sem::NegateExpr or
-      expr instanceof Sem::SubOneExpr or
+      expr instanceof Sem::PreDecExpr or
       getTrackedType(expr.(Sem::DivExpr)) instanceof Sem::FloatingPointType
     )
     or
     positively = true and
-    expr instanceof Sem::AddOneExpr
+    expr instanceof Sem::PreIncExpr
   }
 
   /**

shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll

@@ -0,0 +1,37 @@
+private import codeql.rangeanalysis.RangeAnalysis
+
+module MakeUtils<Semantic Lang, DeltaSig D> {
+  /**
+   * Gets an expression that equals `v - d`.
+   */
+  Lang::Expr ssaRead(Lang::SsaVariable v, D::Delta delta) {
+    result = v.getAUse() and delta = D::fromInt(0)
+    or
+    exists(D::Delta d1, Lang::ConstantIntegerExpr c |
+      result.(Lang::AddExpr).hasOperands(ssaRead(v, d1), c) and
+      delta = D::fromFloat(D::toFloat(d1) - c.getIntValue()) and
+      // In the scope of `x += ..`, which is SSA translated as `x2 = x1 + ..`,
+      // the variable `x1` is shadowed by `x2`, so there's no need to view this
+      // as a read of `x1`.
+      not Lang::isAssignOp(result)
+    )
+    or
+    exists(Lang::SubExpr sub, D::Delta d1, Lang::ConstantIntegerExpr c |
+      result = sub and
+      sub.getLeftOperand() = ssaRead(v, d1) and
+      sub.getRightOperand() = c and
+      delta = D::fromFloat(D::toFloat(d1) + c.getIntValue()) and
+      not Lang::isAssignOp(result)
+    )
+    or
+    result = v.(Lang::SsaExplicitUpdate).getDefiningExpr() and
+    if result instanceof Lang::PostIncExpr
+    then delta = D::fromFloat(1) // x++ === ++x - 1
+    else
+      if result instanceof Lang::PostDecExpr
+      then delta = D::fromFloat(-1) // x-- === --x + 1
+      else delta = D::fromFloat(0)
+    or
+    result.(Lang::CopyValueExpr).getOperand() = ssaRead(v, delta)
+  }
+}