IntegerOverflow: Add query for INT30-C

Adds a query for finding unsigned integer wraparound, based on the
`InterestingBinaryOverflowingExpr` class.

Author: lcartey

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

@@ -0,0 +1,16 @@
+# INT30-C: Ensure that unsigned integer operations do not wrap
+
+This query implements the CERT-C rule INT30-C:
+
+> Ensure that unsigned integer operations do not wrap
+## CERT
+
+** REPLACE THIS BY RUNNING THE SCRIPT `scripts/help/cert-help-extraction.py` **
+
+## Implementation notes
+
+None
+
+## References
+
+* CERT-C: [INT30-C: Ensure that unsigned integer operations do not wrap](https://wiki.sei.cmu.edu/confluence/display/c)

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

@@ -0,0 +1,35 @@
+/**
+ * @id c/cert/unsigned-integer-operations-wrap-around
+ * @name INT30-C: Ensure that unsigned integer operations do not wrap
+ * @description Unsigned integer expressions do not strictly overflow, but instead wrap around in a
+ *              modular way. If the size of the type is not sufficient, this can happen
+ *              unexpectedly.
+ * @kind problem
+ * @precision high
+ * @problem.severity error
+ * @tags external/cert/id/int30-c
+ *       correctness
+ *       security
+ *       external/cert/obligation/rule
+ */
+
+import cpp
+import codingstandards.c.cert
+import codingstandards.cpp.Overflow
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+/* TODO: review the table to restrict to only those operations that actually overflow */
+from InterestingBinaryOverflowingExpr bop
+where
+  not isExcluded(bop, IntegerOverflowPackage::unsignedIntegerOperationsWrapAroundQuery()) and
+  bop.getType().getUnderlyingType().(IntegralType).isUnsigned() and
+  // Not within a guard condition
+  not exists(GuardCondition gc | gc.getAChild*() = bop) and
+  // 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()
+select bop,
+  "Binary expression ..." + bop.getOperator() + "... of type " + bop.getType().getUnderlyingType() +
+    " may wrap."

c/cert/test/rules/INT30-C/UnsignedIntegerOperationsWrapAround.expected

@@ -0,0 +1,2 @@
+| test.c:4:3:4:9 | ... + ... | Binary expression ...+... of type unsigned int may wrap. |
+| test.c:48:3:48:9 | ... - ... | Binary expression ...-... of type unsigned int may wrap. |

c/cert/test/rules/INT30-C/UnsignedIntegerOperationsWrapAround.qlref

@@ -0,0 +1 @@
+rules/INT30-C/UnsignedIntegerOperationsWrapAround.ql

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

@@ -0,0 +1,64 @@
+#include <limits.h>
+
+void test_add_simple(unsigned int i1, unsigned int i2) {
+  i1 + i2; // NON_COMPLIANT - not bounds checked
+}
+
+void test_add_precheck(unsigned int i1, unsigned int i2) {
+  if (UINT_MAX - i1 < i2) {
+    // handle error
+  } else {
+    i1 + i2; // COMPLIANT - bounds checked
+  }
+}
+
+void test_add_precheck_2(unsigned int i1, unsigned int i2) {
+  if (i1 + i2 < i1) {
+    // handle error
+  } else {
+    i1 + i2; // COMPLIANT - bounds checked
+  }
+}
+
+void test_add_postcheck(unsigned int i1, unsigned int i2) {
+  unsigned int i3 = i1 + i2; // COMPLIANT - checked for overflow afterwards
+  if (i3 < i1) {
+    // handle error
+  }
+}
+
+void test_ex2(unsigned int i1, unsigned int i2) {
+  unsigned int ci1 = 2;
+  unsigned int ci2 = 3;
+  ci1 + ci2;     // COMPLIANT, compile time constants
+  i1 + 0;        // COMPLIANT
+  i1 - 0;        // COMPLIANT
+  UINT_MAX - i1; // COMPLIANT - cannot be smaller than 0
+  i1 * 1;        // COMPLIANT
+  if (0 <= i1 && i1 < 32) {
+    UINT_MAX >> i1; // COMPLIANT
+  }
+}
+
+void test_ex3(unsigned int i1, unsigned int i2) {
+  i1 << i2; // COMPLIANT - by EX3
+}
+
+void test_sub_simple(unsigned int i1, unsigned int i2) {
+  i1 - i2; // NON_COMPLIANT - not bounds checked
+}
+
+void test_sub_precheck(unsigned int i1, unsigned int i2) {
+  if (i1 < i2) {
+    // handle error
+  } else {
+    i1 - i2; // COMPLIANT - bounds checked
+  }
+}
+
+void test_sub_postcheck(unsigned int i1, unsigned int i2) {
+  unsigned int i3 = i1 - i2; // COMPLIANT - checked for wrap afterwards
+  if (i3 > i1) {
+    // handle error
+  }
+}

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

@@ -42,6 +42,22 @@ 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
+    )
+  }
+
   /**
    * Identifies a bad overflow check for this overflow expression.
    */