Merge pull request #13783 from MathiasVP/type-bounds-for-new-range-analysis

C++: Constant type-bounds in the new range analysis

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

@@ -307,3 +307,8 @@ class SemConditionalExpr extends SemKnownExpr {
     branch = false and result = falseResult
   }
 }
+
+/** Holds if `upper = true` and `e <= bound` or `upper = false` and `e >= bound`. */
+predicate semHasConstantBoundConstantSpecific(SemExpr e, float bound, boolean upper) {
+  Specific::hasConstantBoundConstantSpecific(e, bound, upper)
+}

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

@@ -434,6 +434,50 @@ module SemanticExprConfig {
 
   /** Gets the expression associated with `instr`. */
   SemExpr getSemanticExpr(IR::Instruction instr) { result = Equiv::getEquivalenceClass(instr) }
+
+  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
+  }
+
+  /**
+   * Holds if `upper = true` and `e <= bound` or `upper = false` and `e >= bound` based
+   * only on type information.
+   */
+  predicate hasConstantBoundConstantSpecific(Expr e, float bound, boolean upper) {
+    exists(
+      SemType converted, SemType unconverted, float unconvertedLb, float convertedLb,
+      float unconvertedUb, float convertedUb
+    |
+      unconverted = getSemanticType(e.getUnconverted().getResultIRType()) and
+      converted = getSemanticType(e.getConverted().getResultIRType()) and
+      typeBounds(unconverted, unconvertedLb, unconvertedUb) and
+      typeBounds(converted, convertedLb, convertedUb) and
+      (
+        upper = true and
+        unconvertedUb < convertedUb and
+        bound = unconvertedUb
+        or
+        upper = false and
+        unconvertedLb > convertedLb and
+        bound = unconvertedLb
+      )
+    )
+  }
 }
 
 predicate getSemanticExpr = SemanticExprConfig::getSemanticExpr/1;
@@ -457,3 +501,5 @@ IRBound::Bound getCppBound(SemBound bound) { bound = result }
 SemGuard getSemanticGuard(IRGuards::IRGuardCondition guard) { result = guard }
 
 IRGuards::IRGuardCondition getCppGuard(SemGuard guard) { guard = result }
+
+predicate hasConstantBoundConstantSpecific = SemanticExprConfig::hasConstantBoundConstantSpecific/3;

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

@@ -74,7 +74,10 @@ module CppLangImplConstant implements LangSig<FloatDelta> {
   /**
    * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
    */
-  predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() }
+  predicate hasConstantBound(SemExpr e, float bound, boolean upper, SemReason reason) {
+    semHasConstantBoundConstantSpecific(e, bound, upper) and
+    reason instanceof SemTypeReason
+  }
 
   /**
    * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).

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

@@ -110,7 +110,7 @@ module CppLangImplRelative implements LangSig<FloatDelta> {
   /**
    * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
    */
-  predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() }
+  predicate hasConstantBound(SemExpr e, float bound, boolean upper, SemReason reason) { none() }
 
   /**
    * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).

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

@@ -155,7 +155,7 @@ signature module LangSig<DeltaSig D> {
   /**
    * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
    */
-  predicate hasConstantBound(SemExpr e, D::Delta bound, boolean upper);
+  predicate hasConstantBound(SemExpr e, D::Delta bound, boolean upper, SemReason reason);
 
   /**
    * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).
@@ -920,14 +920,15 @@ 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) {
-    hasConstantBound(e, b, upper)
+  private predicate baseBound(SemExpr e, D::Delta b, boolean upper, SemReason reason) {
+    hasConstantBound(e, b, upper, reason)
     or
     upper = false and
     b = D::fromInt(0) and
     semPositive(e.(SemBitAndExpr).getAnOperand()) and
     // REVIEW: We let the language opt out here to preserve original results.
-    not ignoreZeroLowerBound(e)
+    not ignoreZeroLowerBound(e) and
+    reason instanceof SemNoReason
   }
 
   /**
@@ -1055,11 +1056,10 @@ module RangeStage<
       origdelta = delta and
       reason instanceof SemNoReason
       or
-      baseBound(e, delta, upper) and
+      baseBound(e, delta, upper, reason) and
       b instanceof SemZeroBound and
       fromBackEdge = false and
-      origdelta = delta and
-      reason instanceof SemNoReason
+      origdelta = delta
       or
       exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
         boundedSsa(v, bb, b, delta, upper, fromBackEdge, origdelta, reason) and

cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/RangeAnalysisUtil.qll

@@ -20,7 +20,8 @@ private Instruction getABoundIn(SemBound b, IRFunction func) {
 pragma[inline]
 private predicate boundedImpl(Instruction i, Instruction b, int delta) {
   exists(SemBound bound, IRFunction func |
-    semBounded(getSemanticExpr(i), bound, delta, true, _) and
+    semBounded(getSemanticExpr(i), bound, delta, true,
+      any(SemReason reason | not reason instanceof SemTypeReason)) and
     b = getABoundIn(bound, func) and
     i.getEnclosingIRFunction() = func
   )