Add critical unspecified behavior for signed integer overflow

MichaelRFairhurst · MichaelRFairhurst · commit 82234950dd14 · 2026-03-13T17:58:53.000-07:00
diff --git a/c/cert/src/rules/INT32-C/SignedIntegerOverflow.ql b/c/cert/src/rules/INT32-C/SignedIntegerOverflow.ql
@@ -19,24 +19,10 @@
 
 import cpp
 import codingstandards.c.cert
-import codingstandards.cpp.Overflow
-import semmle.code.cpp.controlflow.Guards
-import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+import codingstandards.cpp.rules.signedintegeroverflowshared.SignedIntegerOverflowShared
 
-from InterestingOverflowingOperation op
-where
-  not isExcluded(op, IntegerOverflowPackage::signedIntegerOverflowQuery()) and
-  (
-    // An operation that returns a signed integer type
-    op.getType().getUnderlyingType().(IntegralType).isSigned()
-    or
-    // The divide or rem expression on a signed integer
-    op.(DivOrRemOperation).getDividend().getType().getUnderlyingType().(IntegralType).isSigned()
-  ) and
-  // Not checked before the operation
-  not op.hasValidPreCheck() and
-  // Covered by INT34-C
-  not op instanceof LShiftExpr
-select op,
-  "Operation " + op.getOperator() + " of type " + op.getType().getUnderlyingType() +
-    " may overflow or underflow."
+module SignedIntegerOverflowConfig implements SignedIntegerOverflowSharedConfigSig {
+  Query getQuery() { result = IntegerOverflowPackage::signedIntegerOverflowQuery() }
+}
+
+import SignedIntegerOverflowShared<SignedIntegerOverflowConfig>
diff --git a/c/cert/test/rules/INT32-C/SignedIntegerOverflow.qlref b/c/cert/test/rules/INT32-C/SignedIntegerOverflow.qlref
diff --git a/c/cert/test/rules/INT32-C/SignedIntegerOverflow.testref b/c/cert/test/rules/INT32-C/SignedIntegerOverflow.testref
@@ -0,0 +1 @@
+c/common/test/rules/signedintegeroverflowshared/SignedIntegerOverflowShared.ql
diff --git a/c/common/test/rules/signedintegeroverflowshared/SignedIntegerOverflowShared.expected b/c/common/test/rules/signedintegeroverflowshared/SignedIntegerOverflowShared.expected
@@ -21,4 +21,4 @@
 | 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. |
 | test.c:173:3:173:6 | ... ++ | Operation ++ of type signed int may overflow or underflow. |
-| test.c:189:3:189:6 | ... -- | Operation -- of type signed int may overflow or underflow. |
+| test.c:189:3:189:6 | ... -- | Operation -- of type signed int may overflow or underflow. |
diff --git a/c/common/test/rules/signedintegeroverflowshared/SignedIntegerOverflowShared.ql b/c/common/test/rules/signedintegeroverflowshared/SignedIntegerOverflowShared.ql
@@ -0,0 +1,8 @@
+// GENERATED FILE - DO NOT MODIFY
+import codingstandards.cpp.rules.signedintegeroverflowshared.SignedIntegerOverflowShared
+
+module TestFileConfig implements SignedIntegerOverflowSharedConfigSig {
+  Query getQuery() { result instanceof TestQuery }
+}
+
+import SignedIntegerOverflowShared<TestFileConfig>
diff --git a/c/common/test/rules/signedintegeroverflowshared/test.c b/c/common/test/rules/signedintegeroverflowshared/test.c
diff --git a/change_notes/2026-03-13-share-signed-integer-overflow-query.md b/change_notes/2026-03-13-share-signed-integer-overflow-query.md
@@ -0,0 +1,2 @@
+ - `INT32-C` - `SignedIntegerOverflow.ql`:
+   - Refactored query logic into a shared library (`SignedIntegerOverflowShared.qll`) to enable reuse by MISRA C++ `RULE-4-1-3`. The query logic is unchanged and no visible changes to results or performance are expected.
diff --git a/cpp/common/src/codingstandards/cpp/exclusions/cpp/Undefined.qll b/cpp/common/src/codingstandards/cpp/exclusions/cpp/Undefined.qll
@@ -8,7 +8,8 @@ newtype UndefinedQuery =
   TCriticalUnspecifiedBehaviorQuery() or
   TUndefinedBehaviorAuditQuery() or
   TCriticalUnspecifiedBehaviorAuditQuery() or
-  TPossibleDataRaceBetweenThreadsQuery()
+  TPossibleDataRaceBetweenThreadsQuery() or
+  TSignedIntegerOverflowQuery()
 
 predicate isUndefinedQueryMetadata(Query query, string queryId, string ruleId, string category) {
   query =
@@ -55,6 +56,15 @@ predicate isUndefinedQueryMetadata(Query query, string queryId, string ruleId, s
     "cpp/misra/possible-data-race-between-threads" and
   ruleId = "RULE-4-1-3" and
   category = "required"
+  or
+  query =
+    // `Query` instance for the `signedIntegerOverflow` query
+    UndefinedPackage::signedIntegerOverflowQuery() and
+  queryId =
+    // `@id` for the `signedIntegerOverflow` query
+    "cpp/misra/signed-integer-overflow" and
+  ruleId = "RULE-4-1-3" and
+  category = "required"
 }
 
 module UndefinedPackage {
@@ -92,4 +102,11 @@ module UndefinedPackage {
       // `Query` type for `possibleDataRaceBetweenThreads` query
       TQueryCPP(TUndefinedPackageQuery(TPossibleDataRaceBetweenThreadsQuery()))
   }
+
+  Query signedIntegerOverflowQuery() {
+    //autogenerate `Query` type
+    result =
+      // `Query` type for `signedIntegerOverflow` query
+      TQueryCPP(TUndefinedPackageQuery(TSignedIntegerOverflowQuery()))
+  }
 }
diff --git a/cpp/common/src/codingstandards/cpp/rules/signedintegeroverflowshared/SignedIntegerOverflowShared.qll b/cpp/common/src/codingstandards/cpp/rules/signedintegeroverflowshared/SignedIntegerOverflowShared.qll
@@ -0,0 +1,37 @@
+/**
+ * Provides a configurable module SignedIntegerOverflowShared with a `problems` predicate
+ * for the following issue:
+ * The multiplication of two signed integers can lead to underflow or overflow and
+ * therefore undefined behavior.
+ */
+
+import cpp
+import codingstandards.cpp.Customizations
+import codingstandards.cpp.Exclusions
+import codingstandards.cpp.Overflow
+import semmle.code.cpp.controlflow.Guards
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
+
+signature module SignedIntegerOverflowSharedConfigSig {
+  Query getQuery();
+}
+
+module SignedIntegerOverflowShared<SignedIntegerOverflowSharedConfigSig Config> {
+  query predicate problems(InterestingOverflowingOperation op, string message) {
+    not isExcluded(op, Config::getQuery()) and
+    (
+      // An operation that returns a signed integer type
+      op.getType().getUnderlyingType().(IntegralType).isSigned()
+      or
+      // The divide or rem expression on a signed integer
+      op.(DivOrRemOperation).getDividend().getType().getUnderlyingType().(IntegralType).isSigned()
+    ) and
+    // Not checked before the operation
+    not op.hasValidPreCheck() and
+    // Left shift overflow is covered by separate queries (e.g. INT34-C)
+    not op instanceof LShiftExpr and
+    message =
+      "Operation " + op.getOperator() + " of type " + op.getType().getUnderlyingType() +
+        " may overflow or underflow."
+  }
+}
diff --git a/cpp/common/test/rules/signedintegeroverflowshared/SignedIntegerOverflowShared.expected b/cpp/common/test/rules/signedintegeroverflowshared/SignedIntegerOverflowShared.expected
@@ -0,0 +1,24 @@
+| test.cpp:6:3:6:9 | ... + ... | Operation + of type int may overflow or underflow. |
+| test.cpp:7:3:7:10 | ... += ... | Operation += of type signed int may overflow or underflow. |
+| test.cpp:22:7:22:13 | ... + ... | Operation + of type int may overflow or underflow. |
+| test.cpp:25:5:25:11 | ... + ... | Operation + of type int may overflow or underflow. |
+| test.cpp:26:5:26:12 | ... += ... | Operation += of type signed int may overflow or underflow. |
+| test.cpp:31:19:31:25 | ... + ... | Operation + of type int may overflow or underflow. |
+| test.cpp:36:3:36:10 | ... += ... | Operation += of type signed int may overflow or underflow. |
+| test.cpp:43:3:43:9 | ... - ... | Operation - of type int may overflow or underflow. |
+| test.cpp:44:3:44:10 | ... -= ... | Operation -= of type signed int may overflow or underflow. |
+| test.cpp:58:19:58:25 | ... - ... | Operation - of type int may overflow or underflow. |
+| test.cpp:62:3:62:10 | ... -= ... | Operation -= of type signed int may overflow or underflow. |
+| test.cpp:69:3:69:8 | ... * ... | Operation * of type int may overflow or underflow. |
+| test.cpp:70:3:70:10 | ... *= ... | Operation *= of type signed int may overflow or underflow. |
+| test.cpp:115:3:115:9 | ... / ... | Operation / of type int may overflow or underflow. |
+| test.cpp:116:3:116:10 | ... /= ... | Operation /= of type signed int may overflow or underflow. |
+| test.cpp:123:5:123:11 | ... / ... | Operation / of type int may overflow or underflow. |
+| test.cpp:124:5:124:12 | ... /= ... | Operation /= of type signed int may overflow or underflow. |
+| test.cpp:138:3:138:9 | ... % ... | Operation % of type int may overflow or underflow. |
+| test.cpp:139:3:139:10 | ... %= ... | Operation %= of type signed int may overflow or underflow. |
+| test.cpp:146:5:146:11 | ... % ... | Operation % of type int may overflow or underflow. |
+| test.cpp:147:5:147:12 | ... %= ... | Operation %= of type signed int may overflow or underflow. |
+| test.cpp:161:3:161:5 | - ... | Operation - of type signed int may overflow or underflow. |
+| test.cpp:173:3:173:6 | ... ++ | Operation ++ of type signed int may overflow or underflow. |
+| test.cpp:189:3:189:6 | ... -- | Operation -- of type signed int may overflow or underflow. |
diff --git a/cpp/common/test/rules/signedintegeroverflowshared/SignedIntegerOverflowShared.ql b/cpp/common/test/rules/signedintegeroverflowshared/SignedIntegerOverflowShared.ql
@@ -0,0 +1,8 @@
+// GENERATED FILE - DO NOT MODIFY
+import codingstandards.cpp.rules.signedintegeroverflowshared.SignedIntegerOverflowShared
+
+module TestFileConfig implements SignedIntegerOverflowSharedConfigSig {
+  Query getQuery() { result instanceof TestQuery }
+}
+
+import SignedIntegerOverflowShared<TestFileConfig>
diff --git a/cpp/common/test/rules/signedintegeroverflowshared/test.cpp b/cpp/common/test/rules/signedintegeroverflowshared/test.cpp
@@ -0,0 +1,202 @@
+#include <limits.h>
+#include <cstddef>
+#include <cstdint>
+
+void test_add_simple(signed int i1, signed int i2) {
+  i1 + i2;  // NON_COMPLIANT - not bounds checked
+  i1 += i2; // NON_COMPLIANT - not bounds checked
+}
+
+void test_add_precheck(signed int i1, signed int i2) {
+  // Style recommended by CERT
+  if (((i2 > 0) && (i1 > (INT_MAX - i2))) ||
+      ((i2 < 0) && (i1 < (INT_MIN - i2)))) {
+    // handle error
+  } else {
+    i1 + i2;  // COMPLIANT - bounds appropriately checked
+    i1 += i2; // COMPLIANT - bounds appropriately checked
+  }
+}
+
+void test_add_precheck_2(signed int i1, signed int i2) {
+  if (i1 + i2 < i1) { // NON_COMPLIANT - bad overflow check - undefined behavior
+    // handle error
+  } else {
+    i1 + i2;  // NON_COMPLIANT
+    i1 += i2; // NON_COMPLIANT
+  }
+}
+
+void test_add_postcheck(signed int i1, signed int i2) {
+  signed int i3 = i1 + i2; // NON_COMPLIANT - signed overflow is undefined
+                           // behavior, so checking afterwards is not sufficient
+  if (i3 < i1) {
+    // handle error
+  }
+  i1 += i2; // NON_COMPLIANT
+  if (i1 < i2) {
+    // handle error
+  }
+}
+
+void test_sub_simple(signed int i1, signed int i2) {
+  i1 - i2;  // NON_COMPLIANT - not bounds checked
+  i1 -= i2; // NON_COMPLIANT - not bounds checked
+}
+
+void test_sub_precheck(signed int i1, signed int i2) {
+  // Style recomended by CERT
+  if ((i2 > 0 && i1 < INT_MIN + i2) || (i2 < 0 && i1 > INT_MAX + i2)) {
+    // handle error
+  } else {
+    i1 - i2;  // COMPLIANT - bounds checked
+    i1 -= i2; // COMPLIANT - bounds checked
+  }
+}
+
+void test_sub_postcheck(signed int i1, signed int i2) {
+  signed int i3 = i1 - i2; // NON_COMPLIANT - underflow is undefined behavior.
+  if (i3 > i1) {
+    // handle error
+  }
+  i1 -= i2; // NON_COMPLIANT - underflow is undefined behavior.
+  if (i1 > i2) {
+    // handle error
+  }
+}
+
+void test_mul_simple(signed int i1, signed int i2) {
+  i1 *i2;   // NON_COMPLIANT
+  i1 *= i2; // NON_COMPLIANT
+}
+
+void test_mul_precheck(signed int i1, signed int i2) {
+  signed long long tmp =
+      (signed long long)i1 * (signed long long)i2; // COMPLIANT
+  signed int result;
+
+  if (tmp > INT_MAX || tmp < INT_MIN) {
+    // handle error
+  } else {
+    result = (signed int)tmp;
+  }
+}
+
+void test_mul_precheck_2(signed int i1, signed int i2) {
+  if (i1 > 0) {
+    if (i2 > 0) {
+      if (i1 > (INT_MAX / i2)) {
+        return; // handle error
+      }
+    } else {
+      if (i2 < (INT_MIN / i1)) {
+        // handle error
+        return; // handle error
+      }
+    }
+  } else {
+    if (i2 > 0) {
+      if (i1 < (INT_MIN / i2)) {
+        // handle error
+        return; // handle error
+      }
+    } else {
+      if ((i1 != 0) && (i2 < (INT_MAX / i1))) {
+        // handle error
+        return; // handle error
+      }
+    }
+  }
+  i1 *i2;   // COMPLIANT
+  i1 *= i2; // COMPLIANT
+}
+
+void test_simple_div(signed int i1, signed int i2) {
+  i1 / i2;  // NON_COMPLIANT
+  i1 /= i2; // NON_COMPLIANT
+}
+
+void test_simple_div_no_zero(signed int i1, signed int i2) {
+  if (i2 == 0) {
+    // handle error
+  } else {
+    i1 / i2;  // NON_COMPLIANT
+    i1 /= i2; // NON_COMPLIANT
+  }
+}
+
+void test_div_precheck(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_simple_rem(signed int i1, signed int i2) {
+  i1 % i2;  // NON_COMPLIANT
+  i1 %= i2; // NON_COMPLIANT
+}
+
+void test_simple_rem_no_zero(signed int i1, signed int i2) {
+  if (i2 == 0) {
+    // handle error
+  } else {
+    i1 % i2;  // NON_COMPLIANT
+    i1 %= i2; // NON_COMPLIANT
+  }
+}
+
+void test_rem_precheck(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_simple_negate(signed int i1) {
+  -i1; // NON_COMPLIANT
+}
+
+void test_negate_precheck(signed int i1) {
+  if (i1 == INT_MIN) {
+    // handle error
+  } else {
+    -i1; // COMPLIANT
+  }
+}
+
+void test_inc(signed int i1) {
+  i1++; // NON_COMPLIANT
+}
+
+void test_inc_guard(signed int i1) {
+  if (i1 < INT_MAX) {
+    i1++; // COMPLIANT
+  }
+}
+
+void test_inc_loop_guard() {
+  for (signed int i1 = 0; i1 < 10; i1++) { // COMPLIANT
+    // ...
+  }
+}
+
+void test_dec(signed int i1) {
+  i1--; // NON_COMPLIANT
+}
+
+void test_dec_guard(signed int i1) {
+  if (i1 > INT_MIN) {
+    i1--; // COMPLIANT
+  }
+}
+
+void test_dec_loop_guard() {
+  for (signed int i1 = 10; i1 > 0; i1--) { // COMPLIANT
+    // ...
+  }
+}
diff --git a/cpp/misra/src/rules/RULE-4-1-3/SignedIntegerOverflow.ql b/cpp/misra/src/rules/RULE-4-1-3/SignedIntegerOverflow.ql
@@ -0,0 +1,24 @@
+/**
+ * @id cpp/misra/signed-integer-overflow
+ * @name RULE-4-1-3: Signed integer overflow leads to critical unspecified behavior
+ * @description Signed integer overflow or underflow from arithmetic operations results in critical
+ *              unspecified behavior.
+ * @kind problem
+ * @precision medium
+ * @problem.severity error
+ * @tags external/misra/id/rule-4-1-3
+ *       correctness
+ *       scope/system
+ *       external/misra/enforcement/undecidable
+ *       external/misra/obligation/required
+ */
+
+import cpp
+import codingstandards.cpp.misra
+import codingstandards.cpp.rules.signedintegeroverflowshared.SignedIntegerOverflowShared
+
+module SignedIntegerOverflowConfig implements SignedIntegerOverflowSharedConfigSig {
+  Query getQuery() { result = UndefinedPackage::signedIntegerOverflowQuery() }
+}
+
+import SignedIntegerOverflowShared<SignedIntegerOverflowConfig>
diff --git a/cpp/misra/test/rules/RULE-4-1-3/SignedIntegerOverflow.testref b/cpp/misra/test/rules/RULE-4-1-3/SignedIntegerOverflow.testref
@@ -0,0 +1 @@
+cpp/common/test/rules/signedintegeroverflowshared/SignedIntegerOverflowShared.ql
diff --git a/rule_packages/c/IntegerOverflow.json b/rule_packages/c/IntegerOverflow.json
diff --git a/rule_packages/cpp/Undefined.json b/rule_packages/cpp/Undefined.json

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1 @@`
	`1`	`+c/common/test/rules/signedintegeroverflowshared/SignedIntegerOverflowShared.ql`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,2 @@`
	`1`	+ - `INT32-C` - `SignedIntegerOverflow.ql`:
	`2`	+ - Refactored query logic into a shared library (`SignedIntegerOverflowShared.qll`) to enable reuse by MISRA C++ `RULE-4-1-3`. The query logic is unchanged and no visible changes to results or performance are expected.