IntegerOverflow: Implement INT33-C

Adds a query to find div/rem by zero errors.

Author: lcartey

c/cert/src/rules/INT33-C/DivOrRemByZero.md

@@ -0,0 +1,16 @@
+# INT33-C: Ensure that division and remainder operations do not result in divide-by-zero errors
+
+This query implements the CERT-C rule INT33-C:
+
+> Ensure that division and remainder operations do not result in divide-by-zero errors
+## CERT
+
+** REPLACE THIS BY RUNNING THE SCRIPT `scripts/help/cert-help-extraction.py` **
+
+## Implementation notes
+
+None
+
+## References
+
+* CERT-C: [INT33-C: Ensure that division and remainder operations do not result in divide-by-zero errors](https://wiki.sei.cmu.edu/confluence/display/c)

c/cert/src/rules/INT33-C/DivOrRemByZero.ql

@@ -0,0 +1,37 @@
+/**
+ * @id c/cert/div-or-rem-by-zero
+ * @name INT33-C: Ensure that division and remainder operations do not result in divide-by-zero errors
+ * @description Dividing or taking the remainder by zero is undefined behavior.
+ * @kind problem
+ * @precision high
+ * @problem.severity error
+ * @tags external/cert/id/int33-c
+ *       correctness
+ *       external/cert/obligation/rule
+ */
+
+import cpp
+import codingstandards.c.cert
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+from BinaryArithmeticOperation divOrMod, Expr divisor
+where
+  not isExcluded(divOrMod, IntegerOverflowPackage::divOrRemByZeroQuery()) and
+  divOrMod.getOperator() = ["/", "%"] and
+  divisor = divOrMod.getRightOperand() and
+  divisor.getType() instanceof IntegralType and
+  // Range includes 0
+  upperBound(divisor) >= 0 and
+  lowerBound(divisor) <= 0 and
+  // And an explicit check for 0 does not exist
+  not exists(GuardCondition gc, Expr left, Expr right |
+    gc.ensuresEq(left, right, 0, divOrMod.getBasicBlock(), false) and
+    globalValueNumber(left) = globalValueNumber(divisor) and
+    right.getValue().toInt() = 0
+  ) and
+  // Uninstantiated templates may not have an accurate reflection of the range
+  not divOrMod.getEnclosingFunction().isFromUninstantiatedTemplate(_)
+select divOrMod,
+  "Division or remainder expression with divisor that may be zero (divisor range " +
+    lowerBound(divisor) + "..." + upperBound(divisor) + ")."

c/cert/test/rules/INT33-C/DivOrRemByZero.expected

@@ -0,0 +1,4 @@
+| test.c:4:3:4:9 | ... / ... | Division or remainder expression with divisor that may be zero (divisor range -2147483648...2147483647). |
+| test.c:5:3:5:9 | ... % ... | Division or remainder expression with divisor that may be zero (divisor range -2147483648...2147483647). |
+| test.c:12:5:12:11 | ... / ... | Division or remainder expression with divisor that may be zero (divisor range -2147483648...2147483647). |
+| test.c:13:5:13:11 | ... % ... | Division or remainder expression with divisor that may be zero (divisor range -2147483648...2147483647). |

c/cert/test/rules/INT33-C/DivOrRemByZero.qlref

@@ -0,0 +1 @@
+rules/INT33-C/DivOrRemByZero.ql

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

@@ -0,0 +1,33 @@
+#include <limits.h>
+
+void test_simple(signed int i1, signed int i2) {
+  i1 / i2; // NON_COMPLIANT
+  i1 % i2; // NON_COMPLIANT
+}
+
+void test_incomplete_check(signed int i1, signed int i2) {
+  if (i1 == INT_MIN && i2 == -1) {
+    // handle error
+  } else {
+    i1 / i2; // NON_COMPLIANT
+    i1 % i2; // NON_COMPLIANT
+  }
+}
+
+void test_complete_check(signed int i1, signed int i2) {
+  if (i2 == 0 || (i1 == INT_MIN && i2 == -1)) {
+    // handle error
+  } else {
+    i1 / i2; // COMPLIANT
+    i1 % i2; // COMPLIANT
+  }
+}
+
+void test_unsigned(unsigned int i1, unsigned int i2) {
+  if (i2 == 0) {
+    // handle error
+  } else {
+    i1 / i2; // COMPLIANT
+    i1 % i2; // COMPLIANT
+  }
+}