Michaelrfairhurst/package undefined behavior mismatched list delete

.github/workflows/validate-query-formatting.yml

@@ -9,7 +9,6 @@ on:
       - main
       - next
       - "rc/**"
-      - michaelrfairhurst/package-undefined-behavior
 
 env:
     XARGS_MAX_PROCS: 4

c/common/test/rules/possibledataracebetweenthreadsshared/PossibleDataRaceBetweenThreadsShared.expected

@@ -8,6 +8,7 @@
 | test.c:82:3:82:7 | call to srand | Threaded call to non-reentrant function $@ not synchronized from thread function $@ spawned from a loop. | test.c:82:3:82:7 | call to srand | srand | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs | test.c:82:3:82:7 | call to srand | concurrent call to non-reentrant function | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs |
 | test.c:83:3:83:8 | call to getenv | Threaded call to non-reentrant function $@ not synchronized from thread function $@ spawned from a loop. | test.c:83:3:83:8 | call to getenv | getenv | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs | test.c:83:3:83:8 | call to getenv | concurrent call to non-reentrant function | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs |
 | test.c:84:3:84:10 | call to getenv_s | Threaded call to non-reentrant function $@ not synchronized from thread function $@ spawned from a loop. | test.c:84:3:84:10 | call to getenv_s | getenv_s | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs | test.c:84:3:84:10 | call to getenv_s | concurrent call to non-reentrant function | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs |
+| test.c:85:3:85:8 | call to strtok | Threaded call to non-reentrant function $@ not synchronized from thread function $@ spawned from a loop. | test.c:85:3:85:8 | call to strtok | strtok | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs | test.c:85:3:85:8 | call to strtok | concurrent call to non-reentrant function | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs |
 | test.c:86:3:86:10 | call to strerror | Threaded call to non-reentrant function $@ not synchronized from thread function $@ spawned from a loop. | test.c:86:3:86:10 | call to strerror | strerror | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs | test.c:86:3:86:10 | call to strerror | concurrent call to non-reentrant function | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs |
 | test.c:87:3:87:9 | call to asctime | Threaded call to non-reentrant function $@ not synchronized from thread function $@ spawned from a loop. | test.c:87:3:87:9 | call to asctime | asctime | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs | test.c:87:3:87:9 | call to asctime | concurrent call to non-reentrant function | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs |
 | test.c:88:3:88:7 | call to ctime | Threaded call to non-reentrant function $@ not synchronized from thread function $@ spawned from a loop. | test.c:88:3:88:7 | call to ctime | ctime | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs | test.c:88:3:88:7 | call to ctime | concurrent call to non-reentrant function | test.c:78:6:78:43 | many_thread13_calls_nonreentrant_funcs | many_thread13_calls_nonreentrant_funcs |

change_notes/2026-03-13-share-array-delete-type-mismatch-query.md

@@ -0,0 +1,3 @@
+ - `EXP51-CPP` - `DoNotDeleteAnArrayThroughAPointerOfTheIncorrectType.ql`:
+   - Refactored query logic into a shared library (`DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared.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.
+   - The query now uses a `query predicate problems` instead of a `from/where/select`. In path-problem BQRS output, the results section header changes from `#select` to `problems`. Alert results and their content are otherwise identical.

cpp/cert/src/rules/EXP51-CPP/DoNotDeleteAnArrayThroughAPointerOfTheIncorrectType.ql

@@ -18,29 +18,18 @@
 
 import cpp
 import codingstandards.cpp.cert
-import semmle.code.cpp.dataflow.DataFlow
-import AllocationToDeleteFlow::PathGraph
+import codingstandards.cpp.rules.donotdeleteanarraythroughapointeroftheincorrecttypeshared.DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared
 
-module AllocationToDeleteConfig implements DataFlow::ConfigSig {
-  predicate isSource(DataFlow::Node source) { source.asExpr() instanceof NewArrayExpr }
-
-  predicate isSink(DataFlow::Node sink) {
-    exists(DeleteArrayExpr dae | dae.getExpr() = sink.asExpr())
+module DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeConfig implements
+  DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeSharedConfigSig
+{
+  Query getQuery() {
+    result = FreedPackage::doNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeQuery()
   }
 }
 
-module AllocationToDeleteFlow = DataFlow::Global<AllocationToDeleteConfig>;
+module Shared =
+  DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared<DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeConfig>;
 
-from
-  AllocationToDeleteFlow::PathNode source, AllocationToDeleteFlow::PathNode sink,
-  NewArrayExpr newArray, DeleteArrayExpr deleteArray
-where
-  not isExcluded(deleteArray.getExpr(),
-    FreedPackage::doNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeQuery()) and
-  AllocationToDeleteFlow::flowPath(source, sink) and
-  newArray = source.getNode().asExpr() and
-  deleteArray.getExpr() = sink.getNode().asExpr() and
-  not newArray.getType().getUnspecifiedType() = deleteArray.getExpr().getType().getUnspecifiedType()
-select sink, source, sink,
-  "Array of type " + newArray.getType() + " is deleted through a pointer of type " +
-    deleteArray.getExpr().getType() + "."
+import Shared::PathGraph
+import Shared

cpp/cert/test/rules/EXP51-CPP/DoNotDeleteAnArrayThroughAPointerOfTheIncorrectType.testref

@@ -0,0 +1 @@
+cpp/common/test/rules/donotdeleteanarraythroughapointeroftheincorrecttypeshared/DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared.ql

cpp/common/src/codingstandards/cpp/exclusions/cpp/Undefined.qll

@@ -5,6 +5,7 @@ import codingstandards.cpp.exclusions.RuleMetadata
 
 newtype UndefinedQuery =
   TPossibleDataRaceBetweenThreadsQuery() or
+  TArrayDeletedThroughPointerOfIncorrectTypeQuery() or
   TSignedIntegerOverflowQuery() or
   TDivisionByZeroUndefinedBehaviorQuery() or
   TDeallocationTypeMismatchQuery() or
@@ -24,6 +25,15 @@ predicate isUndefinedQueryMetadata(Query query, string queryId, string ruleId, s
   ruleId = "RULE-4-1-3" and
   category = "required"
   or
+  query =
+    // `Query` instance for the `arrayDeletedThroughPointerOfIncorrectType` query
+    UndefinedPackage::arrayDeletedThroughPointerOfIncorrectTypeQuery() and
+  queryId =
+    // `@id` for the `arrayDeletedThroughPointerOfIncorrectType` query
+    "cpp/misra/array-deleted-through-pointer-of-incorrect-type" and
+  ruleId = "RULE-4-1-3" and
+  category = "required"
+  or
   query =
     // `Query` instance for the `signedIntegerOverflow` query
     UndefinedPackage::signedIntegerOverflowQuery() and
@@ -105,6 +115,13 @@ module UndefinedPackage {
       TQueryCPP(TUndefinedPackageQuery(TPossibleDataRaceBetweenThreadsQuery()))
   }
 
+  Query arrayDeletedThroughPointerOfIncorrectTypeQuery() {
+    //autogenerate `Query` type
+    result =
+      // `Query` type for `arrayDeletedThroughPointerOfIncorrectType` query
+      TQueryCPP(TUndefinedPackageQuery(TArrayDeletedThroughPointerOfIncorrectTypeQuery()))
+  }
+
   Query signedIntegerOverflowQuery() {
     //autogenerate `Query` type
     result =

cpp/common/src/codingstandards/cpp/rules/donotdeleteanarraythroughapointeroftheincorrecttypeshared/DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared.qll

@@ -0,0 +1,48 @@
+/**
+ * Provides a configurable module DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared
+ * with a `problems` predicate for the following issue:
+ * Deleting an array through a pointer of an incorrect type leads to undefined behavior.
+ */
+
+import cpp
+import codingstandards.cpp.Customizations
+import codingstandards.cpp.Exclusions
+import semmle.code.cpp.dataflow.DataFlow
+
+signature module DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeSharedConfigSig {
+  Query getQuery();
+}
+
+module DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared<
+  DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeSharedConfigSig Config>
+{
+  private module AllocationToDeleteConfig implements DataFlow::ConfigSig {
+    predicate isSource(DataFlow::Node source) { source.asExpr() instanceof NewArrayExpr }
+
+    predicate isSink(DataFlow::Node sink) {
+      exists(DeleteArrayExpr dae | dae.getExpr() = sink.asExpr())
+    }
+  }
+
+  module AllocationToDeleteFlow = DataFlow::Global<AllocationToDeleteConfig>;
+
+  module PathGraph = AllocationToDeleteFlow::PathGraph;
+
+  query predicate problems(
+    Expr deleteExpr, AllocationToDeleteFlow::PathNode source, AllocationToDeleteFlow::PathNode sink,
+    string message
+  ) {
+    exists(NewArrayExpr newArray, DeleteArrayExpr deleteArray |
+      not isExcluded(deleteArray.getExpr(), Config::getQuery()) and
+      AllocationToDeleteFlow::flowPath(source, sink) and
+      newArray = source.getNode().asExpr() and
+      deleteArray.getExpr() = sink.getNode().asExpr() and
+      not newArray.getType().getUnspecifiedType() =
+        deleteArray.getExpr().getType().getUnspecifiedType() and
+      deleteExpr = sink.getNode().asExpr() and
+      message =
+        "Array of type " + newArray.getType() + " is deleted through a pointer of type " +
+          deleteArray.getExpr().getType() + "."
+    )
+  }
+}

cpp/common/test/rules/donotdeleteanarraythroughapointeroftheincorrecttypeshared/DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared.expected

@@ -0,0 +1,11 @@
+problems
+| test.cpp:9:12:9:13 | l1 | test.cpp:6:19:6:37 | new[] | test.cpp:9:12:9:13 | l1 | Array of type DerivedClass * is deleted through a pointer of type BaseClass *. |
+edges
+| test.cpp:6:19:6:37 | new[] | test.cpp:9:12:9:13 | l1 | provenance |  |
+| test.cpp:7:22:7:40 | new[] | test.cpp:10:12:10:13 | l2 | provenance |  |
+nodes
+| test.cpp:6:19:6:37 | new[] | semmle.label | new[] |
+| test.cpp:7:22:7:40 | new[] | semmle.label | new[] |
+| test.cpp:9:12:9:13 | l1 | semmle.label | l1 |
+| test.cpp:10:12:10:13 | l2 | semmle.label | l2 |
+subpaths

cpp/common/test/rules/donotdeleteanarraythroughapointeroftheincorrecttypeshared/DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared.ql

@@ -0,0 +1,11 @@
+// GENERATED FILE - DO NOT MODIFY
+import codingstandards.cpp.rules.donotdeleteanarraythroughapointeroftheincorrecttypeshared.DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared
+
+module TestFileConfig implements DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeSharedConfigSig {
+  Query getQuery() { result instanceof TestQuery }
+}
+
+module Shared = DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared<TestFileConfig>;
+
+import Shared::PathGraph
+import Shared

cpp/cert/test/rules/EXP51-CPP/test.cpp → cpp/common/test/rules/donotdeleteanarraythroughapointeroftheincorrecttypeshared/test.cpp

@@ -8,4 +8,4 @@ void test() {
 
   delete[] l1; // NON_COMPLIANT - pointer to base class
   delete[] l2; // COMPLIANT - pointer to derived class
-}
+}

cpp/misra/src/rules/RULE-4-1-3/ArrayDeletedThroughPointerOfIncorrectType.ql

@@ -0,0 +1,30 @@
+/**
+ * @id cpp/misra/array-deleted-through-pointer-of-incorrect-type
+ * @name RULE-4-1-3: Array deleted through pointer of incorrect type leads to undefined behavior
+ * @description Deleting an array through a pointer of an incorrect type leads to undefined
+ *              behavior.
+ * @kind path-problem
+ * @precision high
+ * @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.donotdeleteanarraythroughapointeroftheincorrecttypeshared.DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared
+
+module ArrayDeletedThroughPointerOfIncorrectTypeConfig implements
+  DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeSharedConfigSig
+{
+  Query getQuery() { result = UndefinedPackage::arrayDeletedThroughPointerOfIncorrectTypeQuery() }
+}
+
+module Shared =
+  DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared<ArrayDeletedThroughPointerOfIncorrectTypeConfig>;
+
+import Shared::PathGraph
+import Shared

cpp/misra/test/rules/RULE-4-1-3/ArrayDeletedThroughPointerOfIncorrectType.testref

@@ -0,0 +1 @@
+cpp/common/test/rules/donotdeleteanarraythroughapointeroftheincorrecttypeshared/DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared.ql

rule_packages/cpp/Freed.json

@@ -109,6 +109,7 @@
           "name": "Do not delete an array through a pointer of the incorrect type",
           "precision": "high",
           "severity": "error",
+          "shared_implementation_short_name": "DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared",
           "short_name": "DoNotDeleteAnArrayThroughAPointerOfTheIncorrectType",
           "tags": [
             "correctness",

rule_packages/cpp/Undefined.json

@@ -20,6 +20,19 @@
             "scope/system"
           ]
         },
+        {
+          "description": "Deleting an array through a pointer of an incorrect type leads to undefined behavior.",
+          "kind": "path-problem",
+          "name": "Array deleted through pointer of incorrect type leads to undefined behavior",
+          "precision": "high",
+          "severity": "error",
+          "shared_implementation_short_name": "DoNotDeleteAnArrayThroughAPointerOfTheIncorrectTypeShared",
+          "short_name": "ArrayDeletedThroughPointerOfIncorrectType",
+          "tags": [
+            "correctness",
+            "scope/system"
+          ]
+        },
         {
           "description": "Signed integer overflow or underflow from arithmetic operations results in critical unspecified behavior.",
           "kind": "problem",