Implement OutOfBounds package

.vscode/tasks.json

@@ -249,6 +249,7 @@
                 "Null",
                 "OperatorInvariants",
                 "Operators",
+                "OutOfBounds",
                 "Pointers",
                 "Pointers1",
                 "Pointers2",

c/cert/src/rules/ARR30-C/DoNotFormOutOfBoundsPointersOrArraySubscripts.ql

@@ -0,0 +1,43 @@
+/**
+ * @id c/cert/do-not-form-out-of-bounds-pointers-or-array-subscripts
+ * @name ARR30-C: Do not form or use out-of-bounds pointers or array subscripts
+ * @description Forming or using an out-of-bounds pointer is undefined behavior and can result in
+ *              invalid memory accesses.
+ * @kind problem
+ * @precision high
+ * @problem.severity error
+ * @tags external/cert/id/arr30-c
+ *       correctness
+ *       security
+ *       external/cert/obligation/rule
+ */
+
+ import cpp
+ import codingstandards.c.cert
+ import codingstandards.c.OutOfBounds
+
+ from
+   OOB::BufferAccess ba, Expr bufferArg, Expr sizeArg, OOB::PointerToObjectSource bufferSource,
+   string message
+ where
+   not isExcluded(ba, OutOfBoundsPackage::doNotFormOutOfBoundsPointersOrArraySubscriptsQuery()) and
+   (
+     exists(int sizeArgValue, int bufferArgSize |
+      OOB::isSizeArgGreaterThanBufferSize(bufferArg, sizeArg, bufferSource, bufferArgSize, sizeArgValue, ba) and
+       message =
+         "Buffer accesses offset " + sizeArgValue + 
+         " which is greater than the fixed size " + bufferArgSize + " of the $@."
+     )
+     or
+     exists(int sizeArgUpperBound, int sizeMult, int bufferArgSize |
+       OOB::isSizeArgNotCheckedLessThanFixedBufferSize(bufferArg, sizeArg, bufferSource,
+         bufferArgSize, ba, sizeArgUpperBound, sizeMult) and
+       message =
+         "Buffer accesses may access up to offset " + sizeArgUpperBound + "*" + sizeMult +
+           " which is greater than the fixed size " + bufferArgSize + " of the $@."
+     )
+     or
+     OOB::isSizeArgNotCheckedGreaterThanZero(bufferArg, sizeArg, bufferSource, ba) and
+     message = "Buffer access may be to a negative index in the buffer."
+   )
+ select ba, message, bufferSource, "buffer"

c/cert/src/rules/ARR38-C/LibraryFunctionArgumentOutOfBounds.ql

@@ -0,0 +1,25 @@
+/**
+ * @id c/cert/library-function-argument-out-of-bounds
+ * @name ARR38-C: Guarantee that library functions do not form invalid pointers
+ * @description Passing out-of-bounds pointers or erroneous size arguments to standard library
+ *              functions can result in out-of-bounds accesses and other undefined behavior.
+ * @kind problem
+ * @precision high
+ * @problem.severity error
+ * @tags external/cert/id/arr38-c
+ *       correctness
+ *       security
+ *       external/cert/obligation/rule
+ */
+
+import cpp
+import codingstandards.c.cert
+import codingstandards.c.OutOfBounds
+
+from
+  OOB::BufferAccessLibraryFunctionCall fc, string message, Expr bufferArg, string bufferArgStr,
+  Expr sizeOrOtherBufferArg, string otherStr
+where
+  not isExcluded(fc, OutOfBoundsPackage::libraryFunctionArgumentOutOfBoundsQuery()) and
+  OOB::problems(fc, message, bufferArg, bufferArgStr, sizeOrOtherBufferArg, otherStr)
+select fc, message, bufferArg, bufferArgStr, sizeOrOtherBufferArg, otherStr

c/cert/test/rules/ARR30-C/DoNotFormOutOfBoundsPointersOrArraySubscripts.expected

@@ -0,0 +1,3 @@
+| test.c:8:3:8:11 | ... + ... | Buffer accesses offset 404 which is greater than the fixed size 400 of the $@. | test.c:8:3:8:5 | arr | buffer |
+| test.c:16:3:16:13 | ... + ... | Buffer access may be to a negative index in the buffer. | test.c:16:3:16:5 | arr | buffer |
+| test.c:21:5:21:15 | ... + ... | Buffer access may be to a negative index in the buffer. | test.c:21:5:21:7 | arr | buffer |

c/cert/test/rules/ARR30-C/DoNotFormOutOfBoundsPointersOrArraySubscripts.qlref

@@ -0,0 +1 @@
+rules/ARR30-C/DoNotFormOutOfBoundsPointersOrArraySubscripts.ql

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

@@ -0,0 +1,35 @@
+
+
+enum { ARRAY_SIZE = 100 };
+
+static int arr[ARRAY_SIZE];
+
+void test_fixed_wrong() {
+  arr + 101; // NON_COMPLIANT
+}
+
+void test_fixed_right() {
+  arr + 2; // COMPLIANT
+}
+
+void test_no_check(int index) {
+  arr + index; // NON_COMPLIANT
+}
+
+void test_invalid_check(int index) {
+  if (index < ARRAY_SIZE) {
+    arr + index; // NON_COMPLIANT - `index` could be negative
+  }
+}
+
+void test_valid_check(int index) {
+  if (index > 0 && index < ARRAY_SIZE) {
+    arr + index; // COMPLIANT - `index` cannot be negative
+  }
+}
+
+void test_valid_check_by_type(unsigned int index) {
+  if (index < ARRAY_SIZE) {
+    arr + index; // COMPLIANT - `index` cannot be be negative
+  }
+}

c/cert/test/rules/ARR38-C/LibraryFunctionArgumentOutOfBounds.expected

@@ -0,0 +1,75 @@
+| test.c:40:3:40:8 | call to strchr | The $@ passed to strchr might not be null-terminated. | test.c:40:10:40:16 | ca5_bad | argument | test.c:40:10:40:16 | ca5_bad |  |
+| test.c:42:3:42:8 | call to strchr | The $@ passed to strchr is 5 bytes, but an offset of 5 bytes is used to access it. | test.c:42:10:42:21 | ... + ... | read buffer | test.c:42:10:42:21 | ... + ... |  |
+| test.c:46:5:46:10 | call to strcpy | The size of the $@ passed to strcpy is 6 bytes, but the size of the $@ is only 5 bytes. | test.c:46:22:46:28 | test1 | read buffer | test.c:46:12:46:19 | ca5_good | write buffer |
+| test.c:53:5:53:10 | call to strcpy | The $@ passed to strcpy might not be null-terminated. | test.c:53:24:53:30 | ca5_bad | argument | test.c:53:24:53:30 | ca5_bad |  |
+| test.c:54:5:54:10 | call to strcpy | The size of the $@ passed to strcpy is 6 bytes, but the size of the $@ is only 5 bytes. | test.c:54:24:54:31 | ca6_good | read buffer | test.c:54:12:54:19 | call to get_ca_5 | write buffer |
+| test.c:59:5:59:10 | call to strcpy | The size of the $@ passed to strcpy is 6 bytes, but the size of the $@ is only 5 bytes. | test.c:59:22:59:29 | ca6_good | read buffer | test.c:59:12:59:19 | ca5_good | write buffer |
+| test.c:62:5:62:10 | call to strcpy | The $@ passed to strcpy might not be null-terminated. | test.c:62:22:62:28 | ca6_bad | argument | test.c:62:22:62:28 | ca6_bad |  |
+| test.c:62:5:62:10 | call to strcpy | The size of the $@ passed to strcpy is 6 bytes, but the size of the $@ is only 5 bytes. | test.c:62:22:62:28 | ca6_bad | read buffer | test.c:62:12:62:19 | ca5_good | write buffer |
+| test.c:65:5:65:10 | call to strcpy | The size of the $@ passed to strcpy is 6 bytes, but the size of the $@ is only 5 bytes. | test.c:65:21:65:28 | ca6_good | read buffer | test.c:65:12:65:18 | ca5_bad | write buffer |
+| test.c:71:5:71:10 | call to strcpy | The $@ passed to strcpy might not be null-terminated. | test.c:71:21:71:27 | ca5_bad | argument | test.c:71:21:71:27 | ca5_bad |  |
+| test.c:77:5:77:10 | call to strcpy | The $@ passed to strcpy might not be null-terminated. | test.c:77:24:77:30 | ca5_bad | argument | test.c:77:24:77:30 | ca5_bad |  |
+| test.c:80:5:80:10 | call to strcpy | The size of the $@ passed to strcpy is 6 bytes, but the size of the $@ is only 5 bytes. | test.c:80:24:80:31 | ca6_good | read buffer | test.c:80:12:80:19 | call to get_ca_5 | write buffer |
+| test.c:103:5:103:11 | call to strncpy | The size of the $@ passed to strncpy is 5 bytes, but the $@ is 6 bytes. | test.c:103:13:103:19 | ca5_bad | write buffer | test.c:103:32:103:32 | 6 | size argument |
+| test.c:127:5:127:10 | call to memcpy | The $@ passed to memcpy is accessed at an excessive offset of 1 element(s) from the $@. | test.c:127:12:127:13 | p2 | write buffer | test.c:120:21:120:26 | call to strlen | allocation size base |
+| test.c:153:5:153:10 | call to strcat | The $@ passed to strcat might not be null-terminated. | test.c:153:12:153:15 | buf1 | argument | test.c:153:12:153:15 | buf1 |  |
+| test.c:158:5:158:10 | call to strcat | The size of the $@ passed to strcat is 6 bytes, but the size of the $@ is only 5 bytes. | test.c:158:24:158:30 | 12345 | read buffer | test.c:158:12:158:19 | call to get_ca_5 | write buffer |
+| test.c:160:5:160:10 | call to strcat | The size of the $@ passed to strcat is 5 bytes, but the size of the $@ is only 4 bytes. | test.c:160:28:160:33 | 1234 | read buffer | test.c:160:12:160:25 | ... + ... | write buffer |
+| test.c:183:5:183:11 | call to wcsncat | The size of the $@ passed to wcsncat is 24 bytes, but the size of the $@ is only 5 bytes. | test.c:183:25:183:32 | 12345 | read buffer | test.c:183:13:183:20 | call to get_ca_5 | write buffer |
+| test.c:184:5:184:11 | call to wcsncat | The size of the $@ passed to wcsncat is 20 bytes, but the size of the $@ is only 5 bytes. | test.c:184:25:184:31 | 1234 | read buffer | test.c:184:13:184:20 | call to get_ca_5 | write buffer |
+| test.c:185:5:185:11 | call to wcsncat | The size of the $@ passed to wcsncat is 20 bytes, but the size of the $@ is only 1 bytes. | test.c:185:29:185:35 | 1234 | read buffer | test.c:185:13:185:26 | ... + ... | write buffer |
+| test.c:186:5:186:11 | call to wcsncat | The size of the $@ passed to wcsncat is 12 bytes, but the size of the $@ is only 5 bytes. | test.c:186:25:186:29 | 12 | read buffer | test.c:186:13:186:20 | call to get_ca_5 | write buffer |
+| test.c:191:5:191:10 | call to strcmp | The $@ passed to strcmp might not be null-terminated. | test.c:191:22:191:28 | ca5_bad | argument | test.c:191:22:191:28 | ca5_bad |  |
+| test.c:193:5:193:10 | call to strcmp | The $@ passed to strcmp might not be null-terminated. | test.c:193:12:193:18 | ca5_bad | argument | test.c:193:12:193:18 | ca5_bad |  |
+| test.c:202:5:202:11 | call to strncmp | The size of the $@ passed to strncmp is 5 bytes, but the $@ is 6 bytes. | test.c:202:13:202:20 | ca5_good | write buffer | test.c:202:32:202:32 | 6 | size argument |
+| test.c:202:5:202:11 | call to strncmp | The size of the $@ passed to strncmp is 5 bytes, but the $@ is 6 bytes. | test.c:202:23:202:29 | ca5_bad | read buffer | test.c:202:32:202:32 | 6 | size argument |
+| test.c:213:5:213:9 | call to fgets | The size of the $@ passed to fgets is 128 bytes, but the $@ is 129 bytes. | test.c:213:11:213:13 | buf | write buffer | test.c:213:16:213:30 | ... + ... | size argument |
+| test.c:216:5:216:9 | call to fgets | The size of the $@ passed to fgets is 127 bytes, but the $@ is 128 bytes. | test.c:216:11:216:17 | ... + ... | write buffer | test.c:216:20:216:30 | sizeof(<expr>) | size argument |
+| test.c:222:5:222:10 | call to fgetws | The size of the $@ passed to fgetws is 512 bytes, but the $@ is 2048 bytes. | test.c:222:12:222:15 | wbuf | write buffer | test.c:222:18:222:29 | sizeof(<expr>) | size argument |
+| test.c:225:5:225:10 | call to fgetws | The size of the $@ passed to fgetws is 512 bytes, but the $@ is 516 bytes. | test.c:225:12:225:15 | wbuf | write buffer | test.c:225:18:225:49 | ... + ... | size argument |
+| test.c:228:5:228:10 | call to fgetws | The size of the $@ passed to fgetws is 508 bytes, but the $@ is 512 bytes. | test.c:228:12:228:19 | ... + ... | write buffer | test.c:228:22:228:49 | ... / ... | size argument |
+| test.c:237:5:237:12 | call to mbstowcs | The size of the $@ passed to mbstowcs is 512 bytes, but the $@ is 2048 bytes. | test.c:237:14:237:17 | wbuf | write buffer | test.c:237:26:237:37 | sizeof(<expr>) | size argument |
+| test.c:239:5:239:12 | call to mbstowcs | The $@ passed to mbstowcs might not be null-terminated. | test.c:239:20:239:23 | buf2 | argument | test.c:239:20:239:23 | buf2 |  |
+| test.c:249:5:249:12 | call to wcstombs | The size of the $@ passed to wcstombs is 128 bytes, but the $@ is 512 bytes. | test.c:249:14:249:16 | buf | write buffer | test.c:249:25:249:36 | sizeof(<expr>) | size argument |
+| test.c:249:5:249:12 | call to wcstombs | The size of the $@ passed to wcstombs is 512 bytes, but the size of the $@ is only 128 bytes. | test.c:249:19:249:22 | wbuf | read buffer | test.c:249:14:249:16 | buf | write buffer |
+| test.c:252:5:252:12 | call to wcstombs | The size of the $@ passed to wcstombs is 127 bytes, but the $@ is 128 bytes. | test.c:252:14:252:20 | ... + ... | write buffer | test.c:252:33:252:43 | sizeof(<expr>) | size argument |
+| test.c:252:5:252:12 | call to wcstombs | The size of the $@ passed to wcstombs is 508 bytes, but the size of the $@ is only 127 bytes. | test.c:252:23:252:30 | ... + ... | read buffer | test.c:252:14:252:20 | ... + ... | write buffer |
+| test.c:261:5:261:10 | call to mbtowc | The size of the $@ passed to mbtowc is 2 bytes, but the $@ is 3 bytes. | test.c:261:16:261:18 | buf | read buffer | test.c:261:21:261:35 | ... + ... | size argument |
+| test.c:269:5:269:9 | call to mblen | The size of the $@ passed to mblen is 3 bytes, but the $@ is 4 bytes. | test.c:269:11:269:13 | buf | read buffer | test.c:269:16:269:30 | ... + ... | size argument |
+| test.c:270:5:270:9 | call to mblen | The size of the $@ passed to mblen is 5 bytes, but the $@ is 6 bytes. | test.c:270:19:270:24 | call to malloc | read buffer | test.c:270:30:270:44 | ... * ... | size argument |
+| test.c:278:5:278:10 | call to memchr | The size of the $@ passed to memchr is 128 bytes, but the $@ is 129 bytes. | test.c:278:12:278:14 | buf | read buffer | test.c:278:20:278:34 | ... + ... | size argument |
+| test.c:279:5:279:10 | call to memset | The size of the $@ passed to memset is 128 bytes, but the $@ is 129 bytes. | test.c:279:12:279:14 | buf | write buffer | test.c:279:20:279:34 | ... + ... | size argument |
+| test.c:281:5:281:10 | call to memchr | The $@ passed to memchr is null. | test.c:281:12:281:15 | 0 | argument | test.c:281:12:281:15 | 0 |  |
+| test.c:288:5:288:12 | call to strftime | The size of the $@ passed to strftime is 128 bytes, but the $@ is 129 bytes. | test.c:288:14:288:16 | buf | write buffer | test.c:288:19:288:33 | ... + ... | size argument |
+| test.c:290:5:290:12 | call to strftime | The size of the $@ passed to strftime is 127 bytes, but the $@ is 128 bytes. | test.c:290:14:290:20 | ... + ... | write buffer | test.c:290:23:290:33 | sizeof(<expr>) | size argument |
+| test.c:299:5:299:12 | call to wcsftime | The size of the $@ passed to wcsftime is 512 bytes, but the $@ is 520 bytes. | test.c:299:14:299:17 | wbuf | write buffer | test.c:299:20:299:53 | ... + ... | size argument |
+| test.c:305:5:305:12 | call to wcsftime | The size of the $@ passed to wcsftime is 508 bytes, but the $@ is 512 bytes. | test.c:305:14:305:21 | ... + ... | write buffer | test.c:305:24:305:53 | ... / ... | size argument |
+| test.c:307:5:307:12 | call to wcsftime | The size of the $@ passed to wcsftime is 512 bytes, but the $@ is 2048 bytes. | test.c:307:14:307:17 | wbuf | write buffer | test.c:307:20:307:31 | sizeof(<expr>) | size argument |
+| test.c:315:5:315:11 | call to strxfrm | The size of the $@ passed to strxfrm is 64 bytes, but the $@ is 65 bytes. | test.c:315:13:315:15 | buf | write buffer | test.c:315:25:315:39 | ... + ... | size argument |
+| test.c:317:5:317:11 | call to strxfrm | The $@ passed to strxfrm might not be null-terminated. | test.c:317:22:317:25 | buf2 | argument | test.c:317:22:317:25 | buf2 |  |
+| test.c:326:5:326:11 | call to wcsxfrm | The size of the $@ passed to wcsxfrm is 256 bytes, but the $@ is 260 bytes. | test.c:326:13:326:16 | wbuf | write buffer | test.c:326:27:326:60 | ... + ... | size argument |
+| test.c:338:5:338:12 | call to snprintf | The size of the $@ passed to snprintf is 64 bytes, but the $@ is 65 bytes. | test.c:338:14:338:16 | buf | write buffer | test.c:338:19:338:33 | ... + ... | size argument |
+| test.c:346:5:346:11 | call to setvbuf | The size of the $@ passed to setvbuf is 64 bytes, but the $@ is 65 bytes. | test.c:346:16:346:18 | buf | read buffer | test.c:346:29:346:43 | ... + ... | size argument |
+| test.c:348:5:348:11 | call to setvbuf | The size of the $@ passed to setvbuf is 63 bytes, but the $@ is 64 bytes. | test.c:348:16:348:22 | ... + ... | read buffer | test.c:348:33:348:43 | sizeof(<expr>) | size argument |
+| test.c:362:5:362:10 | call to memcpy | The size of the $@ passed to memcpy is 64 bytes, but the $@ is 65 bytes. | test.c:362:12:362:14 | buf | write buffer | test.c:362:23:362:37 | ... + ... | size argument |
+| test.c:362:5:362:10 | call to memcpy | The size of the $@ passed to memcpy is 64 bytes, but the $@ is 65 bytes. | test.c:362:17:362:20 | buf2 | read buffer | test.c:362:23:362:37 | ... + ... | size argument |
+| test.c:364:5:364:10 | call to memcpy | The size of the $@ passed to memcpy is 63 bytes, but the $@ is 64 bytes. | test.c:364:12:364:18 | ... + ... | write buffer | test.c:364:27:364:37 | sizeof(<expr>) | size argument |
+| test.c:364:5:364:10 | call to memcpy | The size of the $@ passed to memcpy is 64 bytes, but the size of the $@ is only 63 bytes. | test.c:364:21:364:24 | buf2 | read buffer | test.c:364:12:364:18 | ... + ... | write buffer |
+| test.c:365:5:365:10 | call to memcpy | The size of the $@ passed to memcpy is 63 bytes, but the $@ is 128 bytes. | test.c:365:17:365:24 | ... + ... | read buffer | test.c:365:27:365:41 | ... * ... | size argument |
+| test.c:365:5:365:10 | call to memcpy | The size of the $@ passed to memcpy is 64 bytes, but the $@ is 128 bytes. | test.c:365:12:365:14 | buf | write buffer | test.c:365:27:365:41 | ... * ... | size argument |
+| test.c:374:5:374:11 | call to wmemcpy | The size of the $@ passed to wmemcpy is 256 bytes, but the $@ is 512 bytes. | test.c:374:22:374:27 | wbuf64 | read buffer | test.c:375:13:375:45 | ... / ... | size argument |
+| test.c:377:5:377:11 | call to wmemcpy | The size of the $@ passed to wmemcpy is 252 bytes, but the $@ is 256 bytes. | test.c:377:13:377:22 | ... + ... | write buffer | test.c:378:13:378:44 | ... / ... | size argument |
+| test.c:377:5:377:11 | call to wmemcpy | The size of the $@ passed to wmemcpy is 256 bytes, but the size of the $@ is only 252 bytes. | test.c:377:25:377:30 | wbuf64 | read buffer | test.c:377:13:377:22 | ... + ... | write buffer |
+| test.c:379:5:379:11 | call to wmemcpy | The size of the $@ passed to wmemcpy is 252 bytes, but the $@ is 256 bytes. | test.c:379:13:379:22 | ... + ... | write buffer | test.c:380:13:380:44 | ... / ... | size argument |
+| test.c:379:5:379:11 | call to wmemcpy | The size of the $@ passed to wmemcpy is 252 bytes, but the $@ is 256 bytes. | test.c:379:25:379:34 | ... + ... | read buffer | test.c:380:13:380:44 | ... / ... | size argument |
+| test.c:401:5:401:11 | call to bsearch | The $@ passed to bsearch is null. | test.c:401:19:401:22 | 0 | argument | test.c:401:19:401:22 | 0 |  |
+| test.c:411:5:411:9 | call to qsort | The size of the $@ passed to qsort is 40 bytes, but the $@ is 44 bytes. | test.c:411:11:411:13 | arr | write buffer | test.c:411:16:411:44 | ... + ... | size argument |
+| test.c:425:3:425:7 | call to fread | The size of the $@ passed to fread is 64 bytes, but the $@ is 65 bytes. | test.c:425:9:425:11 | buf | write buffer | test.c:425:31:425:31 | 1 | size argument |
+| test.c:427:3:427:7 | call to fread | The $@ passed to fread is 64 bytes, but an offset of 64 bytes is used to access it. | test.c:427:9:427:15 | ... + ... | write buffer | test.c:427:9:427:15 | ... + ... |  |
+| test.c:427:3:427:7 | call to fread | The size of the $@ passed to fread is 0 bytes, but the $@ is 64 bytes. | test.c:427:9:427:15 | ... + ... | write buffer | test.c:427:31:427:31 | 1 | size argument |
+| test.c:428:3:428:7 | call to fread | The size of the $@ passed to fread is 64 bytes, but the $@ is 128 bytes. | test.c:428:9:428:11 | buf | write buffer | test.c:428:31:428:31 | 1 | size argument |
+| test.c:430:3:430:8 | call to fwrite | The size of the $@ passed to fwrite is 64 bytes, but the $@ is 65 bytes. | test.c:430:10:430:12 | buf | read buffer | test.c:430:32:430:32 | 1 | size argument |
+| test.c:432:3:432:8 | call to fwrite | The $@ passed to fwrite is 64 bytes, but an offset of 64 bytes is used to access it. | test.c:432:10:432:16 | ... + ... | read buffer | test.c:432:10:432:16 | ... + ... |  |
+| test.c:432:3:432:8 | call to fwrite | The size of the $@ passed to fwrite is 0 bytes, but the $@ is 64 bytes. | test.c:432:10:432:16 | ... + ... | read buffer | test.c:432:32:432:32 | 1 | size argument |
+| test.c:433:3:433:8 | call to fwrite | The size of the $@ passed to fwrite is 64 bytes, but the $@ is 128 bytes. | test.c:433:10:433:12 | buf | read buffer | test.c:433:32:433:32 | 1 | size argument |
+| test.c:464:3:464:8 | call to memcpy | The $@ passed to memcpy is accessed at an excessive offset of 1 element(s) from the $@. | test.c:464:10:464:10 | p | write buffer | test.c:462:21:462:41 | ... * ... | allocation size base |

c/cert/test/rules/ARR38-C/LibraryFunctionArgumentOutOfBounds.qlref

@@ -0,0 +1 @@
+rules/ARR38-C/LibraryFunctionArgumentOutOfBounds.ql