C++: SimpleRangeAnalysis wrapper uses constant stage

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/FloatDelta.qll

@@ -33,7 +33,7 @@ module FloatOverflow implements OverflowSig<FloatDelta> {
   predicate semExprDoesntOverflow(boolean positively, SemExpr expr) {
     exists(float lb, float ub, float delta |
       typeBounds(expr.getSemType(), lb, ub) and 
-      ConstantStage::initialBounded(expr, any(ConstantBounds::SemZeroBound b), delta, positively.booleanNot(), _, _, _)
+      ConstantStage::initialBounded(expr, any(ConstantBounds::SemZeroBound b), delta, positively, _, _, _)
     |
       positively = true and delta < ub
       or

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysis.qll

@@ -1,2 +1,3 @@
-import RangeAnalysisImpl
 import experimental.semmle.code.cpp.semantic.SemanticBound
+private import RangeAnalysisImpl as Impl
+import Impl::Public

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisImpl.qll

@@ -28,7 +28,7 @@ module ConstantBounds implements BoundSig<FloatDelta> {
   }
 }
 
-private module RelativeBounds implements BoundSig<FloatDelta> {
+module RelativeBounds implements BoundSig<FloatDelta> {
   class SemBound instanceof SemanticBound::SemBound {
     SemBound() { not this instanceof SemanticBound::SemZeroBound }
 
@@ -60,48 +60,52 @@ private newtype TSemReason =
     guard = any(RelativeStage::SemCondReason reason).getCond()
   }
 
-/**
- * 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 SemReason extends TSemReason {
-  /** 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 SemNoReason extends SemReason, TSemNoReason {
-  override string toString() { result = "NoReason" }
-}
-
-/** 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) }
-
-  override string toString() { result = getCond().toString() }
-}
-
-private ConstantStage::SemReason constantReason(SemReason reason) {
+ConstantStage::SemReason constantReason(SemReason reason) {
   result instanceof ConstantStage::SemNoReason and reason instanceof SemNoReason
   or
   result.(ConstantStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
 }
 
-private RelativeStage::SemReason relativeReason(SemReason reason) {
+RelativeStage::SemReason relativeReason(SemReason reason) {
   result instanceof RelativeStage::SemNoReason and reason instanceof SemNoReason
   or
   result.(RelativeStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
 }
+import Public
 
-predicate semBounded(
-  SemExpr e, SemanticBound::SemBound b, float delta, boolean upper, SemReason reason
-) {
-  ConstantStage::semBounded(e, b, delta, upper, constantReason(reason))
-  or
-  RelativeStage::semBounded(e, b, delta, upper, relativeReason(reason))
+module Public {
+  predicate semBounded(
+    SemExpr e, SemanticBound::SemBound b, float delta, boolean upper, SemReason reason
+  ) {
+    ConstantStage::semBounded(e, b, delta, upper, constantReason(reason))
+    or
+    RelativeStage::semBounded(e, b, delta, upper, relativeReason(reason))
+  }
+
+  /**
+   * 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 SemReason extends TSemReason {
+    /** 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 SemNoReason extends SemReason, TSemNoReason {
+    override string toString() { result = "NoReason" }
+  }
+
+  /** 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) }
+
+    override string toString() { result = getCond().toString() }
+  }
 }

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisSpecific2.qll

@@ -0,0 +1,127 @@
+/**
+ * C++-specific implementation of range analysis.
+ */
+
+private import experimental.semmle.code.cpp.semantic.Semantic
+private import RangeAnalysisStage
+private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
+private import experimental.semmle.code.cpp.semantic.analysis.IntDelta
+private import RangeAnalysisImpl
+private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
+
+module CppLangImpl2 implements LangSig<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.
+   *
+   * 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) {
+    exists(boolean upper, float delta, ConstantBounds::SemZeroBound b, float lb, float ub |
+      ConstantStage::semBounded(e, b, delta, upper, _) and
+      typeBounds(e.getSemType(), lb, ub) and
+      (
+        upper = false and
+        delta < lb or
+        upper = true and
+        delta > ub
+      )
+    )
+  }
+
+  
+private predicate typeBounds(SemType t, float lb, float ub) {
+  exists(SemIntegerType integralType, float limit |
+    integralType = t and limit = 2.pow(8 * integralType.getByteSize())
+  |
+    if integralType instanceof SemBooleanType
+    then lb = 0 and ub = 1
+    else
+      if integralType.isSigned()
+      then (
+        lb = -(limit / 2) and ub = (limit / 2) - 1
+      ) else (
+        lb = 0 and ub = limit - 1
+      )
+  )
+  or
+  // This covers all floating point types. The range is (-Inf, +Inf).
+  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`).
+   */
+  predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() }
+
+  /**
+   * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).
+   */
+  predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() }
+
+  /**
+   * Holds if the value of `dest` is known to be `src + delta`.
+   */
+  predicate additionalValueFlowStep(SemExpr dest, SemExpr src, float delta) { 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() }
+}

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/SimpleRangeAnalysis.qll

@@ -7,7 +7,7 @@ private import cpp
 private import semmle.code.cpp.ir.IR
 private import experimental.semmle.code.cpp.semantic.SemanticBound
 private import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
-private import RangeAnalysis
+private import RangeAnalysisImpl
 private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
 
 /**
@@ -23,8 +23,10 @@ private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
  *    `lowerBound(expr.getFullyConverted())`
  */
 float lowerBound(Expr expr) {
-  exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound |
-    semBounded(getSemanticExpr(i), b, result, false, _)
+  exists(Instruction i, ConstantBounds::SemBound b |
+    i.getAst() = expr and b instanceof ConstantBounds::SemZeroBound
+  |
+    ConstantStage::semBounded(getSemanticExpr(i), b, result, false, _)
   )
 }
 
@@ -41,8 +43,10 @@ float lowerBound(Expr expr) {
  *    `upperBound(expr.getFullyConverted())`
  */
 float upperBound(Expr expr) {
-  exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound |
-    semBounded(getSemanticExpr(i), b, result, true, _)
+  exists(Instruction i, ConstantBounds::SemBound b |
+    i.getAst() = expr and b instanceof ConstantBounds::SemZeroBound
+  |
+    ConstantStage::semBounded(getSemanticExpr(i), b, result, true, _)
   )
 }