Merge pull request github#12599 from rdmarsh2/rdmarsh2/range-analysis-overflow

C++: add overflow detection to new range analysis

Author: MathiasVP

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/SimpleRangeAnalysis.qll

@@ -8,6 +8,8 @@ private import semmle.code.cpp.ir.IR
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticBound
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
+private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysisImpl
+private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
 
 /**
  * Gets the lower bound of the expression.
@@ -22,8 +24,10 @@ private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.Rang
  *    `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, _)
   )
 }
 
@@ -40,8 +44,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, _)
   )
 }
 
@@ -90,7 +96,15 @@ predicate defMightOverflow(RangeSsaDefinition def, StackVariable v) {
  * does not consider the possibility that the expression might overflow
  * due to a conversion.
  */
-predicate exprMightOverflowNegatively(Expr expr) { none() }
+predicate exprMightOverflowNegatively(Expr expr) {
+  lowerBound(expr) < exprMinVal(expr)
+  or
+  exists(SemanticExprConfig::Expr semExpr |
+    semExpr.getUnconverted().getAst() = expr and
+    ConstantStage::potentiallyOverflowingExpr(false, semExpr) and
+    not ConstantStage::initialBounded(semExpr, _, _, false, _, _, _)
+  )
+}
 
 /**
  * Holds if the expression might overflow negatively. Conversions
@@ -108,7 +122,15 @@ predicate convertedExprMightOverflowNegatively(Expr expr) {
  * does not consider the possibility that the expression might overflow
  * due to a conversion.
  */
-predicate exprMightOverflowPositively(Expr expr) { none() }
+predicate exprMightOverflowPositively(Expr expr) {
+  upperBound(expr) > exprMaxVal(expr)
+  or
+  exists(SemanticExprConfig::Expr semExpr |
+    semExpr.getUnconverted().getAst() = expr and
+    ConstantStage::potentiallyOverflowingExpr(true, semExpr) and
+    not ConstantStage::initialBounded(semExpr, _, _, true, _, _, _)
+  )
+}
 
 /**
  * Holds if the expression might overflow positively. Conversions

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

@@ -1,4 +1,5 @@
 private import RangeAnalysisStage
+private import RangeAnalysisImpl
 
 module FloatDelta implements DeltaSig {
   class Delta = float;
@@ -18,3 +19,36 @@ module FloatDelta implements DeltaSig {
   bindingset[f]
   Delta fromFloat(float f) { result = f }
 }
+
+module FloatOverflow implements OverflowSig<FloatDelta> {
+  predicate semExprDoesNotOverflow(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, _,
+        _, _)
+    |
+      positively = true and delta < ub
+      or
+      positively = false and delta > lb
+    )
+  }
+
+  additional 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
+  }
+}

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

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

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

@@ -6,7 +6,7 @@ private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
 private import RangeAnalysisStage
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
 
-module CppLangImpl implements LangSig<FloatDelta> {
+module CppLangImplConstant implements LangSig<FloatDelta> {
   /**
    * Holds if the specified expression should be excluded from the result of `ssaRead()`.
    *

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

@@ -1,5 +1,6 @@
 private import RangeAnalysisStage
-private import RangeAnalysisSpecific
+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.SemanticBound as SemanticBound
@@ -28,7 +29,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 }
 
@@ -46,11 +47,13 @@ private module RelativeBounds implements BoundSig<FloatDelta> {
   }
 }
 
-private module ConstantStage =
-  RangeStage<FloatDelta, ConstantBounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
+module ConstantStage =
+  RangeStage<FloatDelta, ConstantBounds, FloatOverflow, CppLangImplConstant,
+    RangeUtil<FloatDelta, CppLangImplConstant>>;
 
-private module RelativeStage =
-  RangeStage<FloatDelta, RelativeBounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
+module RelativeStage =
+  RangeStage<FloatDelta, RelativeBounds, FloatOverflow, CppLangImplRelative,
+    RangeUtil<FloatDelta, CppLangImplRelative>>;
 
 private newtype TSemReason =
   TSemNoReason() or
@@ -60,48 +63,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()
 }
 
-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))
+import Public
+
+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/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll

@@ -0,0 +1,126 @@
+/**
+ * C++-specific implementation of range analysis.
+ */
+
+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
+
+module CppLangImplRelative 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() }
+}