C++: Add overflow detection to new range analysis

Author: rdmarsh2

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

@@ -1,4 +1,5 @@
 private import RangeAnalysisStage
+private import RangeAnalysisImpl
 
 module FloatDelta implements DeltaSig {
   class Delta = float;
@@ -27,3 +28,44 @@ module FloatDelta implements DeltaSig {
       )
   }
 }
+
+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(), _, _, _)
+    |
+      positively = true and delta < ub
+      or
+      positively = false and delta > lb
+    )
+  }
+/*
+  predicate semExprOverflow(float delta, boolean upper, SemExpr expr) {
+    exists(float lb, float ub | typeBounds(expr.getSemType(), lb, ub) |
+      upper = false and delta < lb
+      or
+      upper = true and delta > ub
+    )
+  }
+  */
+
+  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/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisImpl.qll

@@ -1,4 +1,4 @@
-private import RangeAnalysisStage
+private import RangeAnalysisStage 
 private import RangeAnalysisSpecific
 private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
 private import RangeUtils
@@ -46,11 +46,11 @@ private module RelativeBounds implements BoundSig<FloatDelta> {
   }
 }
 
-private module ConstantStage =
-  RangeStage<FloatDelta, ConstantBounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
+module ConstantStage =
+  RangeStage<FloatDelta, ConstantBounds, FloatOverflow, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
 
-private module RelativeStage =
-  RangeStage<FloatDelta, RelativeBounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
+module RelativeStage =
+  RangeStage<FloatDelta, RelativeBounds, FloatOverflow, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
 
 private newtype TSemReason =
   TSemNoReason() or

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

@@ -243,11 +243,18 @@ signature module BoundSig<DeltaSig D> {
   }
 }
 
-module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<D> UtilParam> {
+signature module OverflowSig<DeltaSig D> {
+  predicate semExprDoesntOverflow(boolean positively, SemExpr expr);
+}
+
+module RangeStage<
+DeltaSig D, BoundSig<D> Bounds, OverflowSig<D> OverflowParam, LangSig<D> LangParam,
+UtilSig<D> UtilParam> {
   private import Bounds
   private import LangParam
   private import UtilParam
   private import D
+  private import OverflowParam
 
   /**
    * An expression that does conversion, boxing, or unboxing
@@ -941,6 +948,41 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
     bounded(cast.getOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
   }
 
+  predicate bounded(
+    SemExpr e, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge, D::Delta origdelta,
+    SemReason reason) {
+      initialBounded(e, b, delta, upper, fromBackEdge, origdelta, reason) and
+      (
+        semExprDoesntOverflow(upper.booleanNot(), e)
+        or
+        not potentiallyOverflowingExpr(upper.booleanNot(), e)
+      )
+  }
+
+  predicate potentiallyOverflowingExpr(boolean positively, SemExpr expr) {
+    positively in [true, false] and
+    (
+      expr.getOpcode() instanceof Opcode::Add or
+      expr.getOpcode() instanceof Opcode::PointerAdd or
+      expr.getOpcode() instanceof Opcode::Sub or
+      expr.getOpcode() instanceof Opcode::PointerSub or
+      expr.getOpcode() instanceof Opcode::Mul or
+      expr.getOpcode() instanceof Opcode::ShiftLeft
+    )
+    or
+    positively = false and
+    (
+      expr.getOpcode() instanceof Opcode::Negate or
+      expr.getOpcode() instanceof Opcode::SubOne
+    )
+    or
+    positively = false and
+    expr.(SemDivExpr).getSemType() instanceof SemFloatingPointType
+    or
+    positively = true and
+    expr.getOpcode() instanceof Opcode::AddOne
+  }
+
   /**
    * Computes a normal form of `x` where -0.0 has changed to +0.0. This can be
    * needed on the lesser side of a floating-point comparison or on both sides of
@@ -955,7 +997,7 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
    * - `upper = true`  : `e <= b + delta`
    * - `upper = false` : `e >= b + delta`
    */
-  private predicate bounded(
+  predicate initialBounded(
     SemExpr e, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge, D::Delta origdelta,
     SemReason reason
   ) {