IntegerOverflow: clarify valid post-check

Only applicable to unsigned operations

Author: lcartey

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

@@ -29,7 +29,7 @@ where
   // Not guarded by a check, where the check is not an invalid overflow check
   not bop.getAGuardingGVN() = globalValueNumber(bop.getAChild*()) and
   // Is not checked after the operation
-  not bop.hasPostCheck()
+  not bop.hasValidPostCheck()
 select bop,
   "Binary expression ..." + bop.getOperator() + "... of type " + bop.getType().getUnderlyingType() +
     " may wrap."

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

@@ -42,19 +42,27 @@ class InterestingBinaryOverflowingExpr extends BinaryArithmeticOperation {
     )
   }
 
-  predicate hasPostCheck() {
-    exists(RelationalOperation ro |
-      DataFlow::localExprFlow(this, ro.getLesserOperand()) and
-      globalValueNumber(ro.getGreaterOperand()) = globalValueNumber(this.getAnOperand()) and
-      this instanceof AddExpr and
-      ro instanceof GuardCondition
-    )
-    or
-    exists(RelationalOperation ro |
-      DataFlow::localExprFlow(this, ro.getGreaterOperand()) and
-      globalValueNumber(ro.getLesserOperand()) = globalValueNumber(this.getAnOperand()) and
-      this instanceof SubExpr and
-      ro instanceof GuardCondition
+  /**
+   * Holds if there is a correct validity check after this expression which may overflow.
+   *
+   * Only holds for unsigned expressions, as signed overflow/underflow are undefined behavior.
+   */
+  predicate hasValidPostCheck() {
+    this.getType().(IntegralType).isUnsigned() and
+    (
+      exists(RelationalOperation ro |
+        DataFlow::localExprFlow(this, ro.getLesserOperand()) and
+        globalValueNumber(ro.getGreaterOperand()) = globalValueNumber(this.getAnOperand()) and
+        this instanceof AddExpr and
+        ro instanceof GuardCondition
+      )
+      or
+      exists(RelationalOperation ro |
+        DataFlow::localExprFlow(this, ro.getGreaterOperand()) and
+        globalValueNumber(ro.getLesserOperand()) = globalValueNumber(this.getAnOperand()) and
+        this instanceof SubExpr and
+        ro instanceof GuardCondition
+      )
     )
   }