diff --git a/change_notes/2026-03-16-share-divisor-equal-to-zero-query.md b/change_notes/2026-03-16-share-divisor-equal-to-zero-query.md new file mode 100644 index 0000000000..e874e89843 --- /dev/null +++ b/change_notes/2026-03-16-share-divisor-equal-to-zero-query.md @@ -0,0 +1,2 @@ + - `A5-6-1` - `DivisorEqualToZero.ql`: + - Refactored query logic into a shared library (`DivisorEqualToZeroShared.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/autosar/src/rules/A5-6-1/DivisorEqualToZero.ql b/cpp/autosar/src/rules/A5-6-1/DivisorEqualToZero.ql index 6cffbb3f63..44c62fa61f 100644 --- a/cpp/autosar/src/rules/A5-6-1/DivisorEqualToZero.ql +++ b/cpp/autosar/src/rules/A5-6-1/DivisorEqualToZero.ql @@ -15,10 +15,10 @@ import cpp import codingstandards.cpp.autosar +import codingstandards.cpp.rules.divisorequaltozeroshared.DivisorEqualToZeroShared -from BinaryArithmeticOperation bao -where - not isExcluded(bao, ExpressionsPackage::divisorEqualToZeroQuery()) and - (bao instanceof DivExpr or bao instanceof RemExpr) and - bao.getRightOperand().getValue().toFloat() = 0 // `toFloat()` holds for both integer and float literals. -select bao, "Divisor is zero." +module DivisorEqualToZeroConfig implements DivisorEqualToZeroSharedConfigSig { + Query getQuery() { result = ExpressionsPackage::divisorEqualToZeroQuery() } +} + +import DivisorEqualToZeroShared diff --git a/cpp/autosar/test/rules/A5-6-1/DivisorEqualToZero.qlref b/cpp/autosar/test/rules/A5-6-1/DivisorEqualToZero.qlref deleted file mode 100644 index 4752fae796..0000000000 --- a/cpp/autosar/test/rules/A5-6-1/DivisorEqualToZero.qlref +++ /dev/null @@ -1 +0,0 @@ -rules/A5-6-1/DivisorEqualToZero.ql \ No newline at end of file diff --git a/cpp/autosar/test/rules/A5-6-1/DivisorEqualToZero.testref b/cpp/autosar/test/rules/A5-6-1/DivisorEqualToZero.testref new file mode 100644 index 0000000000..b809f4ac0e --- /dev/null +++ b/cpp/autosar/test/rules/A5-6-1/DivisorEqualToZero.testref @@ -0,0 +1 @@ +cpp/common/test/rules/divisorequaltozeroshared/DivisorEqualToZeroShared.ql \ No newline at end of file diff --git a/cpp/common/src/codingstandards/cpp/exclusions/cpp/Undefined.qll b/cpp/common/src/codingstandards/cpp/exclusions/cpp/Undefined.qll index 37ae63fa53..950ea1064c 100644 --- 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 + TDivisionByZeroUndefinedBehaviorQuery() 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 `divisionByZeroUndefinedBehavior` query + UndefinedPackage::divisionByZeroUndefinedBehaviorQuery() and + queryId = + // `@id` for the `divisionByZeroUndefinedBehavior` query + "cpp/misra/division-by-zero-undefined-behavior" 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 divisionByZeroUndefinedBehaviorQuery() { + //autogenerate `Query` type + result = + // `Query` type for `divisionByZeroUndefinedBehavior` query + TQueryCPP(TUndefinedPackageQuery(TDivisionByZeroUndefinedBehaviorQuery())) + } } diff --git a/cpp/common/src/codingstandards/cpp/rules/divisorequaltozeroshared/DivisorEqualToZeroShared.qll b/cpp/common/src/codingstandards/cpp/rules/divisorequaltozeroshared/DivisorEqualToZeroShared.qll new file mode 100644 index 0000000000..fd7fe022ac --- /dev/null +++ b/cpp/common/src/codingstandards/cpp/rules/divisorequaltozeroshared/DivisorEqualToZeroShared.qll @@ -0,0 +1,23 @@ +/** + * Provides a configurable module DivisorEqualToZeroShared with a `problems` predicate + * for the following issue: + * The result is undefined if the right hand operand of the integer division or the + * remainder operator is zero. + */ + +import cpp +import codingstandards.cpp.Customizations +import codingstandards.cpp.Exclusions + +signature module DivisorEqualToZeroSharedConfigSig { + Query getQuery(); +} + +module DivisorEqualToZeroShared { + query predicate problems(BinaryArithmeticOperation bao, string message) { + not isExcluded(bao, Config::getQuery()) and + (bao instanceof DivExpr or bao instanceof RemExpr) and + bao.getRightOperand().getValue().toFloat() = 0 and // `toFloat()` holds for both integer and float literals. + message = "Divisor is zero." + } +} diff --git a/cpp/autosar/test/rules/A5-6-1/DivisorEqualToZero.expected b/cpp/common/test/rules/divisorequaltozeroshared/DivisorEqualToZeroShared.expected similarity index 92% rename from cpp/autosar/test/rules/A5-6-1/DivisorEqualToZero.expected rename to cpp/common/test/rules/divisorequaltozeroshared/DivisorEqualToZeroShared.expected index 7f089cf73d..bc6373b73f 100644 --- a/cpp/autosar/test/rules/A5-6-1/DivisorEqualToZero.expected +++ b/cpp/common/test/rules/divisorequaltozeroshared/DivisorEqualToZeroShared.expected @@ -10,4 +10,4 @@ | test.cpp:28:11:28:18 | ... / ... | Divisor is zero. | | test.cpp:29:11:29:18 | ... % ... | Divisor is zero. | | test.cpp:30:11:30:18 | ... / ... | Divisor is zero. | -| test.cpp:31:11:31:18 | ... % ... | Divisor is zero. | +| test.cpp:31:11:31:18 | ... % ... | Divisor is zero. | \ No newline at end of file diff --git a/cpp/common/test/rules/divisorequaltozeroshared/DivisorEqualToZeroShared.ql b/cpp/common/test/rules/divisorequaltozeroshared/DivisorEqualToZeroShared.ql new file mode 100644 index 0000000000..74ac3ee746 --- /dev/null +++ b/cpp/common/test/rules/divisorequaltozeroshared/DivisorEqualToZeroShared.ql @@ -0,0 +1,8 @@ +// GENERATED FILE - DO NOT MODIFY +import codingstandards.cpp.rules.divisorequaltozeroshared.DivisorEqualToZeroShared + +module TestFileConfig implements DivisorEqualToZeroSharedConfigSig { + Query getQuery() { result instanceof TestQuery } +} + +import DivisorEqualToZeroShared diff --git a/cpp/autosar/test/rules/A5-6-1/test.cpp b/cpp/common/test/rules/divisorequaltozeroshared/test.cpp similarity index 99% rename from cpp/autosar/test/rules/A5-6-1/test.cpp rename to cpp/common/test/rules/divisorequaltozeroshared/test.cpp index eecff86e0c..1690cc95a3 100644 --- a/cpp/autosar/test/rules/A5-6-1/test.cpp +++ b/cpp/common/test/rules/divisorequaltozeroshared/test.cpp @@ -35,4 +35,4 @@ void test_macro() { int f = 1 % ONE; // COMPLIANT int g = 1 / ID(1); // COMPLIANT int h = 1 % ID(1); // COMPLIANT -} \ No newline at end of file +} diff --git a/cpp/misra/src/rules/RULE-4-1-3/DivisionByZeroUndefinedBehavior.ql b/cpp/misra/src/rules/RULE-4-1-3/DivisionByZeroUndefinedBehavior.ql new file mode 100644 index 0000000000..a7ec573981 --- /dev/null +++ b/cpp/misra/src/rules/RULE-4-1-3/DivisionByZeroUndefinedBehavior.ql @@ -0,0 +1,23 @@ +/** + * @id cpp/misra/division-by-zero-undefined-behavior + * @name RULE-4-1-3: Division or modulo by zero leads to undefined behavior + * @description Division or remainder by zero results in undefined behavior. + * @kind 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.divisorequaltozeroshared.DivisorEqualToZeroShared + +module DivisionByZeroUndefinedBehaviorConfig implements DivisorEqualToZeroSharedConfigSig { + Query getQuery() { result = UndefinedPackage::divisionByZeroUndefinedBehaviorQuery() } +} + +import DivisorEqualToZeroShared diff --git a/cpp/misra/test/rules/RULE-4-1-3/DivisionByZeroUndefinedBehavior.testref b/cpp/misra/test/rules/RULE-4-1-3/DivisionByZeroUndefinedBehavior.testref new file mode 100644 index 0000000000..b809f4ac0e --- /dev/null +++ b/cpp/misra/test/rules/RULE-4-1-3/DivisionByZeroUndefinedBehavior.testref @@ -0,0 +1 @@ +cpp/common/test/rules/divisorequaltozeroshared/DivisorEqualToZeroShared.ql \ No newline at end of file diff --git a/rule_packages/cpp/Expressions.json b/rule_packages/cpp/Expressions.json index 10f85237de..a0d1f92aee 100644 --- a/rule_packages/cpp/Expressions.json +++ b/rule_packages/cpp/Expressions.json @@ -62,6 +62,7 @@ "name": "The right operand of the integer division or remainder operators shall not be equal to zero", "precision": "high", "severity": "error", + "shared_implementation_short_name": "DivisorEqualToZeroShared", "short_name": "DivisorEqualToZero", "tags": [ "correctness" diff --git a/rule_packages/cpp/Undefined.json b/rule_packages/cpp/Undefined.json index bc0b10af3d..79743b0037 100644 --- a/rule_packages/cpp/Undefined.json +++ b/rule_packages/cpp/Undefined.json @@ -69,6 +69,19 @@ "concurrency", "scope/system" ] + }, + { + "description": "Division or remainder by zero results in undefined behavior.", + "kind": "problem", + "name": "Division or modulo by zero leads to undefined behavior", + "precision": "high", + "severity": "error", + "shared_implementation_short_name": "DivisorEqualToZeroShared", + "short_name": "DivisionByZeroUndefinedBehavior", + "tags": [ + "correctness", + "scope/system" + ] } ], "title": "There shall be no occurrence of undefined or critical unspecified behaviour"