IntegerOverflow: Further restrictions

 * Simplify the handling of div/rem exprs
 * Exclude rem from unsigned integer
 * Exclude left shift from signed integer overflow
 * Remove silly mulexpr "compliant" cases.
 * Fix div/rem checks to use the right max type
 * Remove getAGuardingGVN and unify under the hasValidPreCheck() case,
but only for unsigned addition.
 * Add guards check for div and rem

Author: lcartey

c/cert/src/rules/INT30-C/UnsignedIntegerOperationsWrapAround.ql

@@ -26,12 +26,13 @@ where
   // Not within a guard condition
   not exists(GuardCondition gc | gc.getAChild*() = op) and
   // Not guarded by a check, where the check is not an invalid overflow check
-  not op.getAGuardingGVN() = globalValueNumber(op.getAChild*()) and
+  not op.hasValidPreCheck() and
   // Is not checked after the operation
   not op.hasValidPostCheck() and
   // Permitted by exception 3
   not op instanceof LShiftExpr and
   // Permitted by exception 2 - zero case is handled in separate query
-  not op instanceof DivExpr
+  not op instanceof DivExpr and
+  not op instanceof RemExpr
 select op,
   "Operation " + op.getOperator() + " of type " + op.getType().getUnderlyingType() + " may wrap."

c/cert/src/rules/INT32-C/SignedIntegerOverflow.ql

@@ -26,22 +26,12 @@ where
     op.getType().getUnderlyingType().(IntegralType).isSigned()
     or
     // The divide or rem expression on a signed integer
-    (op instanceof DivExpr or op instanceof RemExpr) and
-    op.(BinaryOperation).getLeftOperand().getType().getUnderlyingType().(IntegralType).isSigned()
-    or
-    // The assign divide or rem expression on a signed integer
-    (op instanceof AssignDivExpr or op instanceof AssignRemExpr) and
-    op.(AssignArithmeticOperation)
-        .getLValue()
-        .getType()
-        .getUnderlyingType()
-        .(IntegralType)
-        .isSigned()
+    op.(DivOrRemOperation).getDividend().getType().getUnderlyingType().(IntegralType).isSigned()
   ) and
   // Not checked before the operation
   not op.hasValidPreCheck() and
-  // Not guarded by a check, where the check is not an invalid overflow check
-  not op.getAGuardingGVN() = globalValueNumber(op.getAChild*())
+  // Covered by INT34-C
+  not op instanceof LShiftExpr
 select op,
   "Operation " + op.getOperator() + " of type " + op.getType().getUnderlyingType() +
     " may overflow or underflow."

c/cert/test/rules/INT32-C/SignedIntegerOverflow.expected

@@ -11,10 +11,12 @@
 | test.c:62:3:62:10 | ... -= ... | Operation -= of type signed int may overflow or underflow. |
 | test.c:69:3:69:8 | ... * ... | Operation * of type int may overflow or underflow. |
 | test.c:70:3:70:10 | ... *= ... | Operation *= of type signed int may overflow or underflow. |
-| test.c:117:3:117:9 | ... / ... | Operation / of type int may overflow or underflow. |
-| test.c:118:3:118:10 | ... /= ... | Operation /= of type signed int may overflow or underflow. |
-| test.c:140:3:140:9 | ... % ... | Operation % of type int may overflow or underflow. |
-| test.c:141:3:141:10 | ... %= ... | Operation %= of type signed int may overflow or underflow. |
-| test.c:163:3:163:10 | ... << ... | Operation << of type signed int may overflow or underflow. |
-| test.c:164:3:164:11 | ... <<= ... | Operation <<= of type signed int may overflow or underflow. |
-| test.c:183:3:183:5 | - ... | Operation - of type signed int may overflow or underflow. |
+| test.c:115:3:115:9 | ... / ... | Operation / of type int may overflow or underflow. |
+| test.c:116:3:116:10 | ... /= ... | Operation /= of type signed int may overflow or underflow. |
+| test.c:123:5:123:11 | ... / ... | Operation / of type int may overflow or underflow. |
+| test.c:124:5:124:12 | ... /= ... | Operation /= of type signed int may overflow or underflow. |
+| test.c:138:3:138:9 | ... % ... | Operation % of type int may overflow or underflow. |
+| test.c:139:3:139:10 | ... %= ... | Operation %= of type signed int may overflow or underflow. |
+| test.c:146:5:146:11 | ... % ... | Operation % of type int may overflow or underflow. |
+| test.c:147:5:147:12 | ... %= ... | Operation %= of type signed int may overflow or underflow. |
+| test.c:161:3:161:5 | - ... | Operation - of type signed int may overflow or underflow. |

c/cert/test/rules/INT32-C/test.c

@@ -78,9 +78,7 @@ void test_mul_precheck(signed int i1, signed int i2) {
   if (tmp > INT_MAX || tmp < INT_MIN) {
     // handle error
   } else {
-    i1 *i2; // COMPLIANT - checked
     result = (signed int)tmp;
-    i1 *= i2; // COMPLIANT - checked
   }
 }
 
@@ -128,7 +126,7 @@ void test_simple_div_no_zero(signed int i1, signed int i2) {
 }
 
 void test_div_precheck(signed int i1, signed int i2) {
-  if ((i2 == 0) || ((i1 == LONG_MIN) && (i2 == -1))) {
+  if ((i2 == 0) || ((i1 == INT_MIN) && (i2 == -1))) {
     /* Handle error */
   } else {
     i1 / i2;  // COMPLIANT
@@ -151,34 +149,14 @@ void test_simple_rem_no_zero(signed int i1, signed int i2) {
 }
 
 void test_rem_precheck(signed int i1, signed int i2) {
-  if ((i2 == 0) || ((i1 == LONG_MIN) && (i2 == -1))) {
+  if ((i2 == 0) || ((i1 == INT_MIN) && (i2 == -1))) {
     /* Handle error */
   } else {
     i1 % i2;  // COMPLIANT
     i1 %= i2; // COMPLIANT
   }
 }
 
-void test_simple_left_shift(signed int i1, signed int i2) {
-  i1 << i2;  // NON_COMPLIANT
-  i1 <<= i2; // NON_COMPLIANT
-}
-
-/* Returns the number of set bits */
-size_t popcount(uintmax_t num);
-
-#define PRECISION(umax_value) popcount(umax_value)
-
-void test_left_shift_precheck(signed int i1, signed int i2) {
-  if ((i1 < 0) || (i2 < 0) || (i2 >= PRECISION(UINT_MAX)) ||
-      (i1 > (INT_MAX >> i2))) {
-    // handle error
-  } else {
-    i1 << i2;  // COMPLIANT
-    i1 <<= i2; // COMPLIANT
-  }
-}
-
 void test_simple_negate(signed int i1) {
   -i1; // NON_COMPLIANT
 }

cpp/autosar/src/rules/A4-7-1/IntegerExpressionLeadToDataLoss.ql

@@ -25,9 +25,10 @@ where
   // Not within a guard condition
   not exists(GuardCondition gc | gc.getAChild*() = e) and
   // Not guarded by a check, where the check is not an invalid overflow check
-  not e.getAGuardingGVN() = globalValueNumber(e.getAChild*()) and
+  not e.hasValidPreCheck() and
   // Covered by `IntMultToLong.ql` instead
   not e instanceof MulExpr and
   // Not covered by this query - overflow/underflow in division is rare
-  not e instanceof DivExpr
+  not e instanceof DivExpr and
+  not e instanceof RemExpr
 select e, "Binary expression ..." + e.getOperator() + "... may overflow."

cpp/common/src/codingstandards/cpp/Overflow.qll

@@ -21,20 +21,13 @@ class InterestingOverflowingOperation extends Operation {
       exprMightOverflowPositively(this)
       or
       // Division and remainder are not handled by the library
-      exists(Expr leftOperand, Expr rightOperand |
-        (this instanceof DivExpr or this instanceof RemExpr) and
-        leftOperand = this.(BinaryOperation).getLeftOperand() and
-        rightOperand = this.(BinaryOperation).getRightOperand()
-        or
-        (this instanceof AssignDivExpr or this instanceof AssignRemExpr) and
-        leftOperand = this.(AssignArithmeticOperation).getLValue() and
-        rightOperand = this.(AssignArithmeticOperation).getRValue()
-      |
+      exists(DivOrRemOperation divOrRem | divOrRem = this |
         // The right hand side could be -1
-        upperBound(rightOperand) >= -1.0 and
-        lowerBound(rightOperand) <= -1.0 and
+        upperBound(divOrRem.getDivisor()) >= -1.0 and
+        lowerBound(divOrRem.getDivisor()) <= -1.0 and
         // The left hand side could be the smallest possible integer value
-        lowerBound(leftOperand) <= typeLowerBound(leftOperand.getType().getUnderlyingType())
+        lowerBound(divOrRem.getDividend()) <=
+          typeLowerBound(divOrRem.getDividend().getType().getUnderlyingType())
       )
     ) and
     // Multiplication is not covered by the standard range analysis library, so implement our own
@@ -46,18 +39,6 @@ class InterestingOverflowingOperation extends Operation {
     not this instanceof PointerArithmeticOperation
   }
 
-  /**
-   * Get a `GVN` which guards this expression which may overflow.
-   */
-  GVN getAGuardingGVN() {
-    exists(GuardCondition gc, Expr e |
-      not gc = getABadOverflowCheck() and
-      TaintTracking::localTaint(DataFlow::exprNode(e), DataFlow::exprNode(gc.getAChild*())) and
-      gc.controls(this.getBasicBlock(), _) and
-      result = globalValueNumber(e)
-    )
-  }
-
   /**
    * Holds if there is a correct validity check after this expression which may overflow.
    */
@@ -70,6 +51,27 @@ class InterestingOverflowingOperation extends Operation {
       i1 = globalValueNumber(op1) and
       i2 = globalValueNumber(op2)
     |
+      // For unsigned integer addition, look for this pattern:
+      // if (x + y > x)
+      //  use(x + y)
+      // Ensuring it is not a bad overflow check
+      (this instanceof AddExpr or this instanceof AssignAddExpr) and
+      this.getType().getUnspecifiedType().(IntegralType).isUnsigned() and
+      exists(AddExpr ae, RelationalOperation relOp |
+        globalValueNumber(relOp.getAnOperand()) = i1 and
+        relOp.getAnOperand() = ae and
+        globalValueNumber(ae.getAnOperand()) = i1 and
+        globalValueNumber(ae.getAnOperand()) = i2
+      |
+        // At least one operand is not smaller than int
+        exists(Expr op | op = ae.getAnOperand() |
+          op.getType().getSize() >= any(IntType i).getSize()
+        )
+        or
+        // The result of the addition is explicitly converted to a smaller type before the comparison
+        ae.getExplicitlyConverted().getType().getSize() < any(IntType i).getSize()
+      )
+      or
       // The CERT rule for signed integer overflow has a very specific pattern it recommends
       // for checking for overflow. We try to match the pattern here.
       //   ((i2 > 0 && i1 > (INT_MAX - i2)) || (i2 < 0 && i1 < (INT_MIN - i2)))
@@ -156,6 +158,20 @@ class InterestingOverflowingOperation extends Operation {
         )
       )
       or
+      // CERT recommends checking for divisor != -1 and dividor != INT_MIN
+      this instanceof DivOrRemOperation and
+      exists(EqualityOperation eop |
+        // GuardCondition doesn't work in this case, so just confirm that this check dominates the overflow
+        globalValueNumber(eop.getAnOperand()) = i1 and
+        eop.getAnOperand().getValue().toFloat() =
+          typeLowerBound(this.(DivOrRemOperation).getDividend().getType().getUnderlyingType())
+      ) and
+      exists(EqualityOperation eop |
+        // GuardCondition doesn't work in this case, so just confirm that this check dominates the overflow
+        globalValueNumber(eop.getAnOperand()) = i2 and
+        eop.getAnOperand().getValue().toInt() = -1
+      )
+      or
       // The CERT rule for signed integer overflow has a very specific pattern it recommends
       // for checking for multiplication underflow/overflow. We just use a heuristic here,
       // which determines if at least 4 checks of the sort `a < INT_MAX / b` are present in the code.
@@ -193,36 +209,31 @@ class InterestingOverflowingOperation extends Operation {
       )
     )
   }
-
-  /**
-   * Identifies a bad overflow check for this overflow expression.
-   */
-  GuardCondition getABadOverflowCheck() {
-    exists(RelationalOperation relOp |
-      (this instanceof AddExpr or this instanceof AssignAddExpr) and
-      result = relOp and
-      // Looking for this pattern:
-      // if (x + y > x)
-      //  use(x + y)
-      //
-      globalValueNumber(relOp.getAnOperand()) = globalValueNumber(this) and
-      globalValueNumber(relOp.getAnOperand()) = globalValueNumber(this.getAnOperand())
-    |
-      // Signed overflow checks are insufficient
-      this.getUnspecifiedType().(IntegralType).isSigned()
-      or
-      // Unsigned overflow checks can still be bad, if the result is promoted.
-      forall(Expr op | op = this.getAnOperand() | op.getType().getSize() < any(IntType i).getSize()) and
-      // Not explicitly converted to a smaller type before the comparison
-      not this.getExplicitlyConverted().getType().getSize() < any(IntType i).getSize()
-    )
-  }
 }
 
 private class StrictRelationalOperation extends RelationalOperation {
   StrictRelationalOperation() { this.getOperator() = [">", "<"] }
 }
 
+class DivOrRemOperation extends Operation {
+  DivOrRemOperation() {
+    this instanceof DivExpr or
+    this instanceof RemExpr or
+    this instanceof AssignDivExpr or
+    this instanceof AssignRemExpr
+  }
+
+  Expr getDividend() {
+    result = this.(BinaryOperation).getLeftOperand() or
+    result = this.(AssignArithmeticOperation).getLValue()
+  }
+
+  Expr getDivisor() {
+    result = this.(BinaryOperation).getRightOperand() or
+    result = this.(AssignArithmeticOperation).getRValue()
+  }
+}
+
 /**
  * Module inspired by the IntMultToLong.ql query.
  */