From f2ce33142a126cade932989e480b0474cf934519 Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Mon, 27 Mar 2023 21:57:38 -0700 Subject: [PATCH 01/20] Add SidePackage3 rule description and metadata --- .vscode/tasks.json | 5 +- .../cpp/exclusions/c/RuleMetadata.qll | 3 + .../cpp/exclusions/c/SideEffects3.qll | 61 +++++++++++++++++++ rule_packages/c/SideEffects3.json | 55 +++++++++++++++++ rules.csv | 4 +- 5 files changed, 124 insertions(+), 4 deletions(-) create mode 100644 cpp/common/src/codingstandards/cpp/exclusions/c/SideEffects3.qll create mode 100644 rule_packages/c/SideEffects3.json diff --git a/.vscode/tasks.json b/.vscode/tasks.json index 8cebadd0c3..57922779e3 100644 --- a/.vscode/tasks.json +++ b/.vscode/tasks.json @@ -203,8 +203,8 @@ "Concurrency1", "Concurrency2", "Concurrency3", - "Concurrency4", - "Concurrency5", + "Concurrency4", + "Concurrency5", "Conditionals", "Const", "DeadCode", @@ -255,6 +255,7 @@ "Scope", "SideEffects1", "SideEffects2", + "SideEffects3", "SmartPointers1", "SmartPointers2", "Strings", diff --git a/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll b/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll index f4aed38bab..4e3a26b98e 100644 --- a/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll +++ b/cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll @@ -50,6 +50,7 @@ import Preprocessor5 import Preprocessor6 import SideEffects1 import SideEffects2 +import SideEffects3 import SignalHandlers import StandardLibraryFunctionTypes import Statements1 @@ -113,6 +114,7 @@ newtype TCQuery = TPreprocessor6PackageQuery(Preprocessor6Query q) or TSideEffects1PackageQuery(SideEffects1Query q) or TSideEffects2PackageQuery(SideEffects2Query q) or + TSideEffects3PackageQuery(SideEffects3Query q) or TSignalHandlersPackageQuery(SignalHandlersQuery q) or TStandardLibraryFunctionTypesPackageQuery(StandardLibraryFunctionTypesQuery q) or TStatements1PackageQuery(Statements1Query q) or @@ -176,6 +178,7 @@ predicate isQueryMetadata(Query query, string queryId, string ruleId, string cat isPreprocessor6QueryMetadata(query, queryId, ruleId, category) or isSideEffects1QueryMetadata(query, queryId, ruleId, category) or isSideEffects2QueryMetadata(query, queryId, ruleId, category) or + isSideEffects3QueryMetadata(query, queryId, ruleId, category) or isSignalHandlersQueryMetadata(query, queryId, ruleId, category) or isStandardLibraryFunctionTypesQueryMetadata(query, queryId, ruleId, category) or isStatements1QueryMetadata(query, queryId, ruleId, category) or diff --git a/cpp/common/src/codingstandards/cpp/exclusions/c/SideEffects3.qll b/cpp/common/src/codingstandards/cpp/exclusions/c/SideEffects3.qll new file mode 100644 index 0000000000..7c1bedf6f7 --- /dev/null +++ b/cpp/common/src/codingstandards/cpp/exclusions/c/SideEffects3.qll @@ -0,0 +1,61 @@ +//** THIS FILE IS AUTOGENERATED, DO NOT MODIFY DIRECTLY. **/ +import cpp +import RuleMetadata +import codingstandards.cpp.exclusions.RuleMetadata + +newtype SideEffects3Query = + TSideEffectsInArgumentsToUnsafeMacrosQuery() or + TUnsequencedSideEffectsQuery() or + TMultipleObjectModificationsQuery() + +predicate isSideEffects3QueryMetadata(Query query, string queryId, string ruleId, string category) { + query = + // `Query` instance for the `sideEffectsInArgumentsToUnsafeMacros` query + SideEffects3Package::sideEffectsInArgumentsToUnsafeMacrosQuery() and + queryId = + // `@id` for the `sideEffectsInArgumentsToUnsafeMacros` query + "c/cert/side-effects-in-arguments-to-unsafe-macros" and + ruleId = "PRE31-C" and + category = "rule" + or + query = + // `Query` instance for the `unsequencedSideEffects` query + SideEffects3Package::unsequencedSideEffectsQuery() and + queryId = + // `@id` for the `unsequencedSideEffects` query + "c/misra/unsequenced-side-effects" and + ruleId = "RULE-13-2" and + category = "required" + or + query = + // `Query` instance for the `multipleObjectModifications` query + SideEffects3Package::multipleObjectModificationsQuery() and + queryId = + // `@id` for the `multipleObjectModifications` query + "c/misra/multiple-object-modifications" and + ruleId = "RULE-13-2" and + category = "required" +} + +module SideEffects3Package { + Query sideEffectsInArgumentsToUnsafeMacrosQuery() { + //autogenerate `Query` type + result = + // `Query` type for `sideEffectsInArgumentsToUnsafeMacros` query + TQueryC(TSideEffects3PackageQuery(TSideEffectsInArgumentsToUnsafeMacrosQuery())) + } + + Query unsequencedSideEffectsQuery() { + //autogenerate `Query` type + result = + // `Query` type for `unsequencedSideEffects` query + TQueryC(TSideEffects3PackageQuery(TUnsequencedSideEffectsQuery())) + } + + Query multipleObjectModificationsQuery() { + //autogenerate `Query` type + result = + // `Query` type for `multipleObjectModifications` query + TQueryC(TSideEffects3PackageQuery(TMultipleObjectModificationsQuery())) + } +} diff --git a/rule_packages/c/SideEffects3.json b/rule_packages/c/SideEffects3.json new file mode 100644 index 0000000000..6b9159ca24 --- /dev/null +++ b/rule_packages/c/SideEffects3.json @@ -0,0 +1,55 @@ +{ + "CERT-C": { + "PRE31-C": { + "properties": { + "obligation": "rule" + }, + "queries": [ + { + "description": "", + "kind": "problem", + "name": "Avoid side effects in arguments to unsafe macros", + "precision": "very-high", + "severity": "error", + "short_name": "SideEffectsInArgumentsToUnsafeMacros", + "tags": [ + "correctness" + ] + } + ], + "title": "Avoid side effects in arguments to unsafe macros" + } + }, + "MISRA-C-2012": { + "RULE-13-2": { + "properties": { + "obligation": "required" + }, + "queries": [ + { + "description": "The value of an expression and its persistent side effects are depending on the evaluation order resulting in unpredictable behavior.", + "kind": "problem", + "name": "The value of an expression and its persistent side effects depend on its evaluation order", + "precision": "very-high", + "severity": "error", + "short_name": "UnsequencedSideEffects", + "tags": [ + "correctness" + ] + }, + { + "description": "An object shall not be modified more than once between two adjacent sequence points or within any full expression.", + "kind": "problem", + "name": "No object shall be modified more than once", + "precision": "very-high", + "severity": "warning", + "short_name": "MultipleObjectModifications", + "tags": [ + "correctness" + ] + } + ], + "title": "The value of an expression and its persistent side effects shall be the same under all permitted evaluation orders" + } + } +} \ No newline at end of file diff --git a/rules.csv b/rules.csv index 35b1c7f44c..5c021ae1ed 100644 --- a/rules.csv +++ b/rules.csv @@ -586,7 +586,7 @@ c,CERT-C,POS52-C,OutOfScope,Rule,,,Do not perform operations that can block whil c,CERT-C,POS53-C,OutOfScope,Rule,,,Do not use more than one mutex for concurrent waiting operations on a condition variable,,,, c,CERT-C,POS54-C,OutOfScope,Rule,,,Detect and handle POSIX library errors,,,, c,CERT-C,PRE30-C,No,Rule,,,Do not create a universal character name through concatenation,,,Medium, -c,CERT-C,PRE31-C,Yes,Rule,,,Avoid side effects in arguments to unsafe macros,RULE-13-2,SideEffects,Medium, +c,CERT-C,PRE31-C,Yes,Rule,,,Avoid side effects in arguments to unsafe macros,RULE-13-2,SideEffects3,Medium, c,CERT-C,PRE32-C,Yes,Rule,,,Do not use preprocessor directives in invocations of function-like macros,,Preprocessor5,Hard, c,CERT-C,SIG30-C,Yes,Rule,,,Call only asynchronous-safe functions within signal handlers,,SignalHandlers,Medium, c,CERT-C,SIG31-C,Yes,Rule,,,Do not access shared objects in signal handlers,,SignalHandlers,Medium, @@ -688,7 +688,7 @@ c,MISRA-C-2012,RULE-12-3,Yes,Advisory,,,The comma operator should not be used,M5 c,MISRA-C-2012,RULE-12-4,Yes,Advisory,,,Evaluation of constant expressions should not lead to unsigned integer wrap-around,INT30-C,IntegerOverflow,Easy, c,MISRA-C-2012,RULE-12-5,Yes,Mandatory,,,The sizeof operator shall not have an operand which is a function parameter declared as �array of type�,,Types,Medium, c,MISRA-C-2012,RULE-13-1,Yes,Required,,,Initializer lists shall not contain persistent side effects,,SideEffects1,Medium, -c,MISRA-C-2012,RULE-13-2,Yes,Required,,,The value of an expression and its persistent side effects shall be the same under all permitted evaluation orders,PRE31-C,SideEffects,Medium, +c,MISRA-C-2012,RULE-13-2,Yes,Required,,,The value of an expression and its persistent side effects shall be the same under all permitted evaluation orders,PRE31-C,SideEffects3,Medium, c,MISRA-C-2012,RULE-13-3,Yes,Advisory,,,A full expression containing an increment (++) or decrement (--) operator should have no other potential side effects other than that caused by the increment or decrement operator,,SideEffects2,Medium, c,MISRA-C-2012,RULE-13-4,Yes,Advisory,,,The result of an assignment operator should not be used,M6-2-1,SideEffects1,Easy, c,MISRA-C-2012,RULE-13-5,Yes,Required,,,The right hand operand of a logical && or || operator shall not contain persistent side effects,M5-14-1,SideEffects1,Import, From ee8db1d633a04f07b732b83c7581796297e8303b Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Fri, 24 Mar 2023 16:44:48 -0700 Subject: [PATCH 02/20] Change the definition of a full expr to match the standard --- c/common/src/codingstandards/c/Expr.qll | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/c/common/src/codingstandards/c/Expr.qll b/c/common/src/codingstandards/c/Expr.qll index eadc870486..52a9f0719f 100644 --- a/c/common/src/codingstandards/c/Expr.qll +++ b/c/common/src/codingstandards/c/Expr.qll @@ -3,8 +3,19 @@ import cpp /* A full expression as defined in ISO/IEC 9899:2011 6.8 point 4 and Annex C point 1 item 5. */ class FullExpr extends Expr { FullExpr() { - not this.getParent() instanceof Expr and - not exists(Variable v | v.getInitializer().getExpr() = this) + exists(ExprStmt s | this = s.getExpr()) + or + exists(Loop l | this = l.getControllingExpr()) + or + exists(ConditionalStmt s | this = s.getControllingExpr()) + or + exists(ForStmt s | this = s.getUpdate()) + or + exists(ReturnStmt s | this = s.getExpr()) + or + this instanceof AggregateLiteral + or + this = any(Variable v).getInitializer().getExpr() } } From 25cee4fb23fe3c34dab5abae1167bb8c3b694bc5 Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Fri, 24 Mar 2023 16:46:09 -0700 Subject: [PATCH 03/20] Add full declarators case to ordering module --- c/common/src/codingstandards/c/Ordering.qll | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/c/common/src/codingstandards/c/Ordering.qll b/c/common/src/codingstandards/c/Ordering.qll index 955cba5e50..fd71c8c347 100644 --- a/c/common/src/codingstandards/c/Ordering.qll +++ b/c/common/src/codingstandards/c/Ordering.qll @@ -13,7 +13,6 @@ module Ordering { /** * Holds if `e1` is sequenced before `e2` as defined by Annex C in ISO/IEC 9899:2011 * This limits to expression and we do not consider the sequence points that are not amenable to modelling: - * - after a full declarator as described in 6.7.6 point 3. * - before a library function returns (see 7.1.4 point 3). * - after the actions associated with each formatted I/O function conversion specifier (see 7.21.6 point 1 & 7.29.2 point 1). * - between the expr before and after a call to a comparison function, @@ -68,6 +67,24 @@ module Ordering { // The side effect of updating the stored value of the left operand is sequenced after the value computations of the left and right operands. // See 6.5.16 e2.(Assignment).getAnOperand().getAChild*() = e1 + or + // There is a sequence point after a full declarator as described in 6.7.6 point 3. + exists(DeclStmt declStmt, int i, int j | i < j | + declStmt + .getDeclarationEntry(i) + .(VariableDeclarationEntry) + .getVariable() + .getInitializer() + .getExpr() + .getAChild*() = e1 and + declStmt + .getDeclarationEntry(j) + .(VariableDeclarationEntry) + .getVariable() + .getInitializer() + .getExpr() + .getAChild*() = e2 + ) ) } From 3e888082a6509069ccebb51471685cdd160f21d1 Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Fri, 24 Mar 2023 16:47:08 -0700 Subject: [PATCH 04/20] Consider children expression when determining ordering --- c/common/src/codingstandards/c/Ordering.qll | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/c/common/src/codingstandards/c/Ordering.qll b/c/common/src/codingstandards/c/Ordering.qll index fd71c8c347..ea7fa60115 100644 --- a/c/common/src/codingstandards/c/Ordering.qll +++ b/c/common/src/codingstandards/c/Ordering.qll @@ -27,12 +27,12 @@ module Ordering { // before the actual call. exists(Call call | ( - call.getAnArgument() = e1 + call.getAnArgument().getAChild*() = e1 or // Postfix expression designating the called function // We current only handle call through function pointers because the postfix expression // of regular function calls is not available. That is, identifying `f` in `f(...)` - call.(ExprCall).getExpr() = e1 + call.(ExprCall).getExpr().getAChild*() = e1 ) and call.getTarget() = e2.getEnclosingFunction() ) @@ -42,7 +42,7 @@ module Ordering { exists(BinaryLogicalOperation blop | blop instanceof LogicalAndExpr or blop instanceof LogicalOrExpr | - blop.getLeftOperand() = e1 and blop.getRightOperand() = e2 + blop.getLeftOperand().getAChild*() = e1 and blop.getRightOperand().getAChild*() = e2 ) or // 6.5.17 point 2 - There is a sequence pointt between the left operand and the right operand. @@ -50,13 +50,13 @@ module Ordering { lhs = ce.getLeftOperand() and rhs = ce.getRightOperand() | - lhs = e1.getParent*() and rhs = e2.getParent*() + lhs.getAChild*() = e1 and rhs.getAChild*() = e2 ) or // 6.5.15 point 4 - There is a sequence point between the first operand and the evaluation of the second or third. exists(ConditionalExpr cond | - cond.getCondition() = e1 and - (cond.getThen() = e2 or cond.getElse() = e2) + cond.getCondition().getAChild*() = e1 and + (cond.getThen().getAChild*() = e2 or cond.getElse().getAChild*() = e2) ) or // Between the evaluation of a full expression and the next to be evaluated full expression. From 19bebdd3d0198c0842635a981bb96184db72b07d Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Fri, 24 Mar 2023 16:47:38 -0700 Subject: [PATCH 05/20] Address typos --- c/common/src/codingstandards/c/Ordering.qll | 4 ++-- c/common/src/codingstandards/c/SideEffects.qll | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/c/common/src/codingstandards/c/Ordering.qll b/c/common/src/codingstandards/c/Ordering.qll index ea7fa60115..575dc6f3fd 100644 --- a/c/common/src/codingstandards/c/Ordering.qll +++ b/c/common/src/codingstandards/c/Ordering.qll @@ -37,7 +37,7 @@ module Ordering { call.getTarget() = e2.getEnclosingFunction() ) or - // 6.5.13 point 4 & 6.5.14 point 4 - The operators guarantee left-to-righ evaluation and there is + // 6.5.13 point 4 & 6.5.14 point 4 - The operators guarantee left-to-right evaluation and there is // a sequence point between the first and second operand if the latter is evaluated. exists(BinaryLogicalOperation blop | blop instanceof LogicalAndExpr or blop instanceof LogicalOrExpr @@ -45,7 +45,7 @@ module Ordering { blop.getLeftOperand().getAChild*() = e1 and blop.getRightOperand().getAChild*() = e2 ) or - // 6.5.17 point 2 - There is a sequence pointt between the left operand and the right operand. + // 6.5.17 point 2 - There is a sequence point between the left operand and the right operand. exists(CommaExpr ce, Expr lhs, Expr rhs | lhs = ce.getLeftOperand() and rhs = ce.getRightOperand() diff --git a/c/common/src/codingstandards/c/SideEffects.qll b/c/common/src/codingstandards/c/SideEffects.qll index 3cea568e3e..09bf672a30 100644 --- a/c/common/src/codingstandards/c/SideEffects.qll +++ b/c/common/src/codingstandards/c/SideEffects.qll @@ -26,7 +26,7 @@ private class VolatileAccess extends GlobalSideEffect::Range, VariableAccess { this.getTarget().isVolatile() and // Exclude value computation of an lvalue expression soley used to determine the identity // of the object. As noted in the footnote of 6.5.16 point 3 it is implementation dependend - // whether the value of the assignment expression deterived from the left operand after the assignment + // whether the value of the assignment expression derived from the left operand after the assignment // is determined by reading the object. We assume it is not for assignments that are a child of an // expression statement because the value is not used and is required for the compliant MISRA-C:2012 case: // `extern volatile int v; v = v & 0x80;` From 86540f589078a848d8cedd48b7fa6767d68b9bcb Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Fri, 24 Mar 2023 16:48:10 -0700 Subject: [PATCH 06/20] Remove unimplemented queries for RULE-13-2 from package. --- rule_packages/c/SideEffects3.json | 25 +------------------------ 1 file changed, 1 insertion(+), 24 deletions(-) diff --git a/rule_packages/c/SideEffects3.json b/rule_packages/c/SideEffects3.json index 6b9159ca24..1924ebf988 100644 --- a/rule_packages/c/SideEffects3.json +++ b/rule_packages/c/SideEffects3.json @@ -4,19 +4,7 @@ "properties": { "obligation": "rule" }, - "queries": [ - { - "description": "", - "kind": "problem", - "name": "Avoid side effects in arguments to unsafe macros", - "precision": "very-high", - "severity": "error", - "short_name": "SideEffectsInArgumentsToUnsafeMacros", - "tags": [ - "correctness" - ] - } - ], + "queries": [], "title": "Avoid side effects in arguments to unsafe macros" } }, @@ -36,17 +24,6 @@ "tags": [ "correctness" ] - }, - { - "description": "An object shall not be modified more than once between two adjacent sequence points or within any full expression.", - "kind": "problem", - "name": "No object shall be modified more than once", - "precision": "very-high", - "severity": "warning", - "short_name": "MultipleObjectModifications", - "tags": [ - "correctness" - ] } ], "title": "The value of an expression and its persistent side effects shall be the same under all permitted evaluation orders" From 96317b69bcc70cef5f827293e5b3a56bf992cbf5 Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Fri, 24 Mar 2023 16:51:28 -0700 Subject: [PATCH 07/20] Add query for RULE 13-2 --- .../rules/RULE-13-2/UnsequencedSideEffects.ql | 59 +++++++++++++++++++ .../RULE-13-2/UnsequencedSideEffects.expected | 5 ++ .../RULE-13-2/UnsequencedSideEffects.qlref | 1 + c/misra/test/rules/RULE-13-2/test.c | 28 +++++++++ 4 files changed, 93 insertions(+) create mode 100644 c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql create mode 100644 c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected create mode 100644 c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.qlref create mode 100644 c/misra/test/rules/RULE-13-2/test.c diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql new file mode 100644 index 0000000000..c019b2c37f --- /dev/null +++ b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql @@ -0,0 +1,59 @@ +/** + * @id c/misra/unsequenced-side-effects + * @name RULE-13-2: The value of an expression and its persistent side effects depend on its evaluation order + * @description The value of an expression and its persistent side effects are depending on the + * evaluation order resulting in unpredictable behavior. + * @kind problem + * @precision very-high + * @problem.severity error + * @tags external/misra/id/rule-13-2 + * correctness + * external/misra/obligation/required + */ + +import cpp +import codingstandards.c.misra +import codingstandards.c.Expr +import codingstandards.c.SideEffects +import codingstandards.c.Ordering + +predicate isCandidatePair(Expr parentExpr, Expr e1, Expr e2) { + parentExpr.getAChild+() = e1 and + parentExpr.getAChild+() = e2 +} + +class ConstituentExprOrdering extends Ordering::Configuration { + ConstituentExprOrdering() { this = "ConstituentExprOrdering" } + + override predicate isCandidate(Expr e1, Expr e2) { + // Two different expressions part of the same full expression. + // Compute differerence using successor relation to break the symmetry of the candidate relation. + isCandidatePair(_, e1, e2) + } +} + +from + ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1, + VariableEffect variableEffect2 +where + not isExcluded(fullExpr, SideEffects3Package::unsequencedSideEffectsQuery()) and + // If the effect is local we can directly check if it is unsequenced. + // If the effect is not local (happens in a different function) we use the access as a proxy. + orderingConfig.isUnsequenced(variableEffect1, variableEffect2) and + fullExpr.getAChild+() = variableEffect1 and + fullExpr.getAChild+() = variableEffect2 and + // Both are evaluated + not exists(ConditionalExpr ce | + ce.getThen().getAChild*() = variableEffect1 and ce.getElse().getAChild*() = variableEffect2 + ) and + // Break the symmetry of the ordering relation by requiring that the first expression is located before the second. + // This builds upon the assumption that the expressions are part of the same full expression as specified in the ordering configuration. + exists(int offset1, int offset2 | + variableEffect1.getLocation().charLoc(_, offset1, _) and + variableEffect2.getLocation().charLoc(_, offset2, _) and + offset1 < offset2 + ) +select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1, + "side effect", variableEffect1.getAnAccess(), variableEffect1.getTarget().getName(), + variableEffect2, "side effect", variableEffect2.getAnAccess(), + variableEffect2.getTarget().getName() diff --git a/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected b/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected new file mode 100644 index 0000000000..12ea5b578c --- /dev/null +++ b/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected @@ -0,0 +1,5 @@ +| test.c:6:12:6:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:6:12:6:13 | l1 | side effect | test.c:6:12:6:13 | l1 | l1 | test.c:6:17:6:18 | l1 | side effect | test.c:6:17:6:18 | l1 | l1 | +| test.c:7:12:7:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:7:12:7:13 | l1 | side effect | test.c:7:12:7:13 | l1 | l1 | test.c:7:17:7:18 | l2 | side effect | test.c:7:17:7:18 | l2 | l2 | +| test.c:17:3:17:21 | ... = ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:17:8:17:9 | l1 | side effect | test.c:17:8:17:9 | l1 | l1 | test.c:17:13:17:14 | l1 | side effect | test.c:17:13:17:14 | l1 | l1 | +| test.c:19:3:19:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:19:7:19:8 | l1 | side effect | test.c:19:7:19:8 | l1 | l1 | test.c:19:11:19:12 | l2 | side effect | test.c:19:11:19:12 | l2 | l2 | +| test.c:25:3:25:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:25:7:25:10 | ... ++ | side effect | test.c:25:7:25:8 | l8 | l8 | test.c:25:13:25:16 | ... ++ | side effect | test.c:25:13:25:14 | l9 | l9 | diff --git a/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.qlref b/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.qlref new file mode 100644 index 0000000000..0cb8d40dbb --- /dev/null +++ b/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.qlref @@ -0,0 +1 @@ +rules/RULE-13-2/UnsequencedSideEffects.ql \ No newline at end of file diff --git a/c/misra/test/rules/RULE-13-2/test.c b/c/misra/test/rules/RULE-13-2/test.c new file mode 100644 index 0000000000..d81559efe6 --- /dev/null +++ b/c/misra/test/rules/RULE-13-2/test.c @@ -0,0 +1,28 @@ +void foo(int, int); + +void unsequenced_sideeffects() { + volatile int l1, l2; + + int l3 = l1 + l1; // NON_COMPLIANT + int l4 = l1 + l2; // NON_COMPLIANT + + // Store value of volatile object in temporary non-volatile object. + int l5 = l1; + // Store value of volatile object in temporary non-volatile object. + int l6 = l2; + int l7 = l5 + l6; // COMPLIANT + + int l8, l9; + l1 = l1 & 0x80; // COMPLIANT + l8 = l1 = l1 & 0x80; // NON_COMPLIANT + + foo(l1, l2); // NON_COMPLIANT + // Store value of volatile object in temporary non-volatile object. + l8 = l1; + // Store value of volatile object in temporary non-volatile object. + l9 = l2; + foo(l8, l9); // COMPLIANT + foo(l8++, l9++); // NON_COMPLIANT + + int l10 = l8++, l11 = l8++; // COMPLIANT +} \ No newline at end of file From 3e94fd741f23f05f746f86a0f7d36f7d3dd27156 Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Fri, 24 Mar 2023 16:57:10 -0700 Subject: [PATCH 08/20] Correct comments --- c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql | 1 - 1 file changed, 1 deletion(-) diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql index c019b2c37f..b6b4cff2e8 100644 --- a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql +++ b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql @@ -27,7 +27,6 @@ class ConstituentExprOrdering extends Ordering::Configuration { override predicate isCandidate(Expr e1, Expr e2) { // Two different expressions part of the same full expression. - // Compute differerence using successor relation to break the symmetry of the candidate relation. isCandidatePair(_, e1, e2) } } From f0ee5b14746a812231c125ddf004c07165a0365b Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Sat, 25 Mar 2023 13:02:20 -0700 Subject: [PATCH 09/20] Attemp to optimize query --- .../rules/RULE-13-2/UnsequencedSideEffects.ql | 73 +++++++++++++++---- 1 file changed, 58 insertions(+), 15 deletions(-) diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql index b6b4cff2e8..f6286ef9ba 100644 --- a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql +++ b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql @@ -17,42 +17,85 @@ import codingstandards.c.Expr import codingstandards.c.SideEffects import codingstandards.c.Ordering -predicate isCandidatePair(Expr parentExpr, Expr e1, Expr e2) { - parentExpr.getAChild+() = e1 and - parentExpr.getAChild+() = e2 +predicate isOrHasSideEffect(Expr e) { + e instanceof VariableEffect or + any(VariableEffect ve).getAnAccess() = e +} + +predicate originatingInStatement(Expr e, FullExpr fe) { + isOrHasSideEffect(e) and + ( + e.(VariableEffect).getAnAccess() = fe.getAChild+() + or + e.(VariableAccess) = fe.getAChild+() + ) } class ConstituentExprOrdering extends Ordering::Configuration { ConstituentExprOrdering() { this = "ConstituentExprOrdering" } override predicate isCandidate(Expr e1, Expr e2) { - // Two different expressions part of the same full expression. - isCandidatePair(_, e1, e2) + exists(FullExpr fe | + originatingInStatement(e1, fe) and + originatingInStatement(e2, fe) + ) } } +pragma[noinline] +predicate sameFullExpr(FullExpr fe, Expr e1, Expr e2) { + originatingInStatement(e1, fe) and + originatingInStatement(e2, fe) +} + +predicate effect(VariableEffect ve, VariableAccess va, Variable v) { + ve.getAnAccess() = va and + va.getTarget() = v and + ve.getTarget() = v +} + from ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1, - VariableEffect variableEffect2 + VariableEffect variableEffect2, VariableAccess va1, VariableAccess va2, Variable v1, Variable v2 where not isExcluded(fullExpr, SideEffects3Package::unsequencedSideEffectsQuery()) and + sameFullExpr(fullExpr, va1, va2) and + effect(variableEffect1, va1, v1) and + effect(variableEffect2, va2, v2) and + variableEffect1 != variableEffect2 and // If the effect is local we can directly check if it is unsequenced. // If the effect is not local (happens in a different function) we use the access as a proxy. - orderingConfig.isUnsequenced(variableEffect1, variableEffect2) and - fullExpr.getAChild+() = variableEffect1 and - fullExpr.getAChild+() = variableEffect2 and + ( + va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and + va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and + orderingConfig.isUnsequenced(variableEffect1, variableEffect2) + or + va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and + not va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and + exists(Call call | + call.getAnArgument() = va2 and call.getEnclosingStmt() = va1.getEnclosingStmt() + | + orderingConfig.isUnsequenced(variableEffect1, call) + ) + or + not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and + va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and + exists(Call call | + call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt() + | + orderingConfig.isUnsequenced(call, variableEffect2) + ) + ) and // Both are evaluated not exists(ConditionalExpr ce | - ce.getThen().getAChild*() = variableEffect1 and ce.getElse().getAChild*() = variableEffect2 + ce.getThen().getAChild*() = va1 and ce.getElse().getAChild*() = va2 ) and // Break the symmetry of the ordering relation by requiring that the first expression is located before the second. // This builds upon the assumption that the expressions are part of the same full expression as specified in the ordering configuration. exists(int offset1, int offset2 | - variableEffect1.getLocation().charLoc(_, offset1, _) and - variableEffect2.getLocation().charLoc(_, offset2, _) and + va1.getLocation().charLoc(_, offset1, _) and + va2.getLocation().charLoc(_, offset2, _) and offset1 < offset2 ) select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1, - "side effect", variableEffect1.getAnAccess(), variableEffect1.getTarget().getName(), - variableEffect2, "side effect", variableEffect2.getAnAccess(), - variableEffect2.getTarget().getName() + "side effect", va1, v1.getName(), variableEffect2, "side effect", va2, v2.getName() From 84b1ad8ae026976007e4bb8c58e3e064175e7ad9 Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Sat, 25 Mar 2023 13:39:32 -0700 Subject: [PATCH 10/20] Add comments to explain steps --- c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql index f6286ef9ba..8edf4e2262 100644 --- a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql +++ b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql @@ -62,9 +62,11 @@ where sameFullExpr(fullExpr, va1, va2) and effect(variableEffect1, va1, v1) and effect(variableEffect2, va2, v2) and + // Exclude the same effect applying to different objects. + // This occurs when on is a subject of the other. + // For example, foo.bar = 1; where both foo and bar are objects modified by the assignment. variableEffect1 != variableEffect2 and - // If the effect is local we can directly check if it is unsequenced. - // If the effect is not local (happens in a different function) we use the access as a proxy. + // If the effect is not local (happens in a different function) we use the call with the access as a proxy. ( va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and From 962a64055834a622762d1cd4a910194d107312a9 Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Mon, 27 Mar 2023 14:29:20 -0700 Subject: [PATCH 11/20] Provide more useful predicate names --- .../rules/RULE-13-2/UnsequencedSideEffects.ql | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql index 8edf4e2262..102cac18df 100644 --- a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql +++ b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql @@ -22,7 +22,7 @@ predicate isOrHasSideEffect(Expr e) { any(VariableEffect ve).getAnAccess() = e } -predicate originatingInStatement(Expr e, FullExpr fe) { +predicate partOfFullExpr(Expr e, FullExpr fe) { isOrHasSideEffect(e) and ( e.(VariableEffect).getAnAccess() = fe.getAChild+() @@ -36,19 +36,19 @@ class ConstituentExprOrdering extends Ordering::Configuration { override predicate isCandidate(Expr e1, Expr e2) { exists(FullExpr fe | - originatingInStatement(e1, fe) and - originatingInStatement(e2, fe) + partOfFullExpr(e1, fe) and + partOfFullExpr(e2, fe) ) } } pragma[noinline] predicate sameFullExpr(FullExpr fe, Expr e1, Expr e2) { - originatingInStatement(e1, fe) and - originatingInStatement(e2, fe) + partOfFullExpr(e1, fe) and + partOfFullExpr(e2, fe) } -predicate effect(VariableEffect ve, VariableAccess va, Variable v) { +predicate destructureEffect(VariableEffect ve, VariableAccess va, Variable v) { ve.getAnAccess() = va and va.getTarget() = v and ve.getTarget() = v @@ -60,8 +60,8 @@ from where not isExcluded(fullExpr, SideEffects3Package::unsequencedSideEffectsQuery()) and sameFullExpr(fullExpr, va1, va2) and - effect(variableEffect1, va1, v1) and - effect(variableEffect2, va2, v2) and + destructureEffect(variableEffect1, va1, v1) and + destructureEffect(variableEffect2, va2, v2) and // Exclude the same effect applying to different objects. // This occurs when on is a subject of the other. // For example, foo.bar = 1; where both foo and bar are objects modified by the assignment. From 9deadab551a1800e32f357f354e7aa62d778b5da Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Mon, 27 Mar 2023 21:41:05 -0700 Subject: [PATCH 12/20] Change scope of RULE 13-2 - Only consider unsequenced side effects to the same objects, unless - the two unsequenced side effects target two different volatile objects. - Don't allow unsequenced modification and reading of the same object, unless the reading is part of establishing the value of the modification. --- .../rules/RULE-13-2/UnsequencedSideEffects.ql | 128 +++++++++++------- .../RULE-13-2/UnsequencedSideEffects.expected | 10 +- c/misra/test/rules/RULE-13-2/test.c | 4 +- 3 files changed, 87 insertions(+), 55 deletions(-) diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql index 102cac18df..4a2859c7cf 100644 --- a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql +++ b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql @@ -17,13 +17,15 @@ import codingstandards.c.Expr import codingstandards.c.SideEffects import codingstandards.c.Ordering -predicate isOrHasSideEffect(Expr e) { - e instanceof VariableEffect or - any(VariableEffect ve).getAnAccess() = e +class VariableEffectOrAccess extends Expr { + VariableEffectOrAccess() { + this instanceof VariableEffect or + this instanceof VariableAccess + } } -predicate partOfFullExpr(Expr e, FullExpr fe) { - isOrHasSideEffect(e) and +pragma[noinline] +predicate partOfFullExpr(VariableEffectOrAccess e, FullExpr fe) { ( e.(VariableEffect).getAnAccess() = fe.getAChild+() or @@ -42,62 +44,92 @@ class ConstituentExprOrdering extends Ordering::Configuration { } } -pragma[noinline] -predicate sameFullExpr(FullExpr fe, Expr e1, Expr e2) { - partOfFullExpr(e1, fe) and - partOfFullExpr(e2, fe) -} - -predicate destructureEffect(VariableEffect ve, VariableAccess va, Variable v) { - ve.getAnAccess() = va and - va.getTarget() = v and - ve.getTarget() = v +predicate sameFullExpr(FullExpr fe, VariableAccess va1, VariableAccess va2) { + partOfFullExpr(va1, fe) and + partOfFullExpr(va2, fe) and + va1 != va2 and + exists(Variable v1, Variable v2 | + // Use `pragma[only_bind_into]` to prevent CP between variable accesses. + va1.getTarget() = pragma[only_bind_into](v1) and va2.getTarget() = pragma[only_bind_into](v2) + | + v1.isVolatile() and v2.isVolatile() + or + not (v1.isVolatile() and v2.isVolatile()) and + v1 = v2 + ) } from ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1, - VariableEffect variableEffect2, VariableAccess va1, VariableAccess va2, Variable v1, Variable v2 + VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label where not isExcluded(fullExpr, SideEffects3Package::unsequencedSideEffectsQuery()) and + // The two access are scoped to the same full expression. sameFullExpr(fullExpr, va1, va2) and - destructureEffect(variableEffect1, va1, v1) and - destructureEffect(variableEffect2, va2, v2) and - // Exclude the same effect applying to different objects. - // This occurs when on is a subject of the other. - // For example, foo.bar = 1; where both foo and bar are objects modified by the assignment. - variableEffect1 != variableEffect2 and - // If the effect is not local (happens in a different function) we use the call with the access as a proxy. + // We are only interested in effects that change an object, + // i.e., exclude patterns suchs as `b->data[b->cursor++]` where `b` is considered modified and read or `foo.bar = 1` where `=` modifies to both `foo` and `bar`. + not variableEffect1.isPartial() and + variableEffect1.getAnAccess() = va1 and ( - va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and - va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and - orderingConfig.isUnsequenced(variableEffect1, variableEffect2) - or - va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and - not va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and - exists(Call call | - call.getAnArgument() = va2 and call.getEnclosingStmt() = va1.getEnclosingStmt() - | - orderingConfig.isUnsequenced(variableEffect1, call) + exists(VariableEffect variableEffect2 | + not variableEffect2.isPartial() and + variableEffect2.getAnAccess() = va2 and + // If the effect is not local (happens in a different function) we use the call with the access as a proxy. + ( + va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and + va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and + orderingConfig.isUnsequenced(variableEffect1, variableEffect2) + or + va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and + not va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and + exists(Call call | + call.getAnArgument() = va2 and call.getEnclosingStmt() = va1.getEnclosingStmt() + | + orderingConfig.isUnsequenced(variableEffect1, call) + ) + or + not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and + va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and + exists(Call call | + call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt() + | + orderingConfig.isUnsequenced(call, variableEffect2) + ) + ) and + // Break the symmetry of the ordering relation by requiring that the first expression is located before the second. + // This builds upon the assumption that the expressions are part of the same full expression as specified in the ordering configuration. + exists(int offset1, int offset2 | + va1.getLocation().charLoc(_, offset1, _) and + va2.getLocation().charLoc(_, offset2, _) and + offset1 < offset2 + ) and + placeHolder = variableEffect2 and + label = "side effect" ) or - not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and - va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and - exists(Call call | - call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt() - | - orderingConfig.isUnsequenced(call, variableEffect2) - ) + placeHolder = va2 and + label = "read" and + not exists(VariableEffect variableEffect2 | variableEffect1 != variableEffect2 | + variableEffect2.getAnAccess() = va2 + ) and + ( + va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and + orderingConfig.isUnsequenced(variableEffect1, va2) + or + not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and + exists(Call call | + call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt() + | + orderingConfig.isUnsequenced(call, va2) + ) + ) and + // The read is not used to compute the effect on the variable. + // E.g., exclude x = x + 1 + not variableEffect1.getAChild+() = va2 ) and // Both are evaluated not exists(ConditionalExpr ce | ce.getThen().getAChild*() = va1 and ce.getElse().getAChild*() = va2 - ) and - // Break the symmetry of the ordering relation by requiring that the first expression is located before the second. - // This builds upon the assumption that the expressions are part of the same full expression as specified in the ordering configuration. - exists(int offset1, int offset2 | - va1.getLocation().charLoc(_, offset1, _) and - va2.getLocation().charLoc(_, offset2, _) and - offset1 < offset2 ) select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1, - "side effect", va1, v1.getName(), variableEffect2, "side effect", va2, v2.getName() + "side effect", va1, va1.getTarget(), placeHolder, label, va2, va2.getTarget() diff --git a/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected b/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected index 12ea5b578c..de0c33907e 100644 --- a/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected +++ b/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected @@ -1,5 +1,5 @@ -| test.c:6:12:6:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:6:12:6:13 | l1 | side effect | test.c:6:12:6:13 | l1 | l1 | test.c:6:17:6:18 | l1 | side effect | test.c:6:17:6:18 | l1 | l1 | -| test.c:7:12:7:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:7:12:7:13 | l1 | side effect | test.c:7:12:7:13 | l1 | l1 | test.c:7:17:7:18 | l2 | side effect | test.c:7:17:7:18 | l2 | l2 | -| test.c:17:3:17:21 | ... = ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:17:8:17:9 | l1 | side effect | test.c:17:8:17:9 | l1 | l1 | test.c:17:13:17:14 | l1 | side effect | test.c:17:13:17:14 | l1 | l1 | -| test.c:19:3:19:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:19:7:19:8 | l1 | side effect | test.c:19:7:19:8 | l1 | l1 | test.c:19:11:19:12 | l2 | side effect | test.c:19:11:19:12 | l2 | l2 | -| test.c:25:3:25:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:25:7:25:10 | ... ++ | side effect | test.c:25:7:25:8 | l8 | l8 | test.c:25:13:25:16 | ... ++ | side effect | test.c:25:13:25:14 | l9 | l9 | +| test.c:6:12:6:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:6:12:6:13 | l1 | side effect | test.c:6:12:6:13 | l1 | test.c:4:16:4:17 | l1 | test.c:6:17:6:18 | l1 | side effect | test.c:6:17:6:18 | l1 | test.c:4:16:4:17 | l1 | +| test.c:7:12:7:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:7:12:7:13 | l1 | side effect | test.c:7:12:7:13 | l1 | test.c:4:16:4:17 | l1 | test.c:7:17:7:18 | l2 | side effect | test.c:7:17:7:18 | l2 | test.c:4:20:4:21 | l2 | +| test.c:17:3:17:21 | ... = ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:17:8:17:9 | l1 | side effect | test.c:17:8:17:9 | l1 | test.c:4:16:4:17 | l1 | test.c:17:13:17:14 | l1 | side effect | test.c:17:13:17:14 | l1 | test.c:4:16:4:17 | l1 | +| test.c:19:3:19:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:19:7:19:8 | l1 | side effect | test.c:19:7:19:8 | l1 | test.c:4:16:4:17 | l1 | test.c:19:11:19:12 | l2 | side effect | test.c:19:11:19:12 | l2 | test.c:4:20:4:21 | l2 | +| test.c:25:3:25:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:25:7:25:10 | ... ++ | side effect | test.c:25:7:25:8 | l8 | test.c:15:7:15:8 | l8 | test.c:25:13:25:14 | l8 | read | test.c:25:13:25:14 | l8 | test.c:15:7:15:8 | l8 | diff --git a/c/misra/test/rules/RULE-13-2/test.c b/c/misra/test/rules/RULE-13-2/test.c index d81559efe6..6fbc827c4f 100644 --- a/c/misra/test/rules/RULE-13-2/test.c +++ b/c/misra/test/rules/RULE-13-2/test.c @@ -21,8 +21,8 @@ void unsequenced_sideeffects() { l8 = l1; // Store value of volatile object in temporary non-volatile object. l9 = l2; - foo(l8, l9); // COMPLIANT - foo(l8++, l9++); // NON_COMPLIANT + foo(l8, l9); // COMPLIANT + foo(l8++, l8); // NON_COMPLIANT int l10 = l8++, l11 = l8++; // COMPLIANT } \ No newline at end of file From a3d046febd84cef0f90d094581466c32ae8f6886 Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Mon, 27 Mar 2023 21:59:20 -0700 Subject: [PATCH 13/20] Remove PRE31-C from side effects 3 --- rule_packages/c/SideEffects3.json | 9 --------- 1 file changed, 9 deletions(-) diff --git a/rule_packages/c/SideEffects3.json b/rule_packages/c/SideEffects3.json index 1924ebf988..2d67df6e2e 100644 --- a/rule_packages/c/SideEffects3.json +++ b/rule_packages/c/SideEffects3.json @@ -1,13 +1,4 @@ { - "CERT-C": { - "PRE31-C": { - "properties": { - "obligation": "rule" - }, - "queries": [], - "title": "Avoid side effects in arguments to unsafe macros" - } - }, "MISRA-C-2012": { "RULE-13-2": { "properties": { From bef7b9e675400a23fe4c0898d72269c57c7f3fa3 Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Wed, 29 Mar 2023 15:50:30 -0700 Subject: [PATCH 14/20] Address incorrect alert specification --- c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql index 4a2859c7cf..53eb49c05d 100644 --- a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql +++ b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql @@ -132,4 +132,4 @@ where ce.getThen().getAChild*() = va1 and ce.getElse().getAChild*() = va2 ) select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1, - "side effect", va1, va1.getTarget(), placeHolder, label, va2, va2.getTarget() + "side effect", va1, va1.getTarget().getName(), placeHolder, label, va2, va2.getTarget().getName() From dc026577e34054094232e88e1c621c621e3aba7a Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Wed, 29 Mar 2023 15:51:16 -0700 Subject: [PATCH 15/20] Add support for MISRA example case --- .../rules/RULE-13-2/UnsequencedSideEffects.ql | 101 +++++++++++++++++- .../RULE-13-2/UnsequencedSideEffects.expected | 11 +- c/misra/test/rules/RULE-13-2/test.c | 11 +- 3 files changed, 112 insertions(+), 11 deletions(-) diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql index 53eb49c05d..59b4bc660c 100644 --- a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql +++ b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql @@ -59,6 +59,101 @@ predicate sameFullExpr(FullExpr fe, VariableAccess va1, VariableAccess va2) { ) } +int getLeafCount(LeftRightOperation bop) { + if + not bop.getLeftOperand() instanceof BinaryOperation and + not bop.getRightOperand() instanceof BinaryOperation + then result = 2 + else + if + bop.getLeftOperand() instanceof BinaryOperation and + not bop.getRightOperand() instanceof BinaryOperation + then result = 1 + getLeafCount(bop.getLeftOperand()) + else + if + not bop.getLeftOperand() instanceof BinaryOperation and + bop.getRightOperand() instanceof BinaryOperation + then result = 1 + getLeafCount(bop.getRightOperand()) + else result = getLeafCount(bop.getLeftOperand()) + getLeafCount(bop.getRightOperand()) +} + +class LeftRightOperation extends Expr { + LeftRightOperation() { + this instanceof BinaryOperation or + this instanceof AssignOperation or + this instanceof AssignExpr + } + + Expr getLeftOperand() { + result = this.(BinaryOperation).getLeftOperand() + or + result = this.(AssignOperation).getLValue() + or + result = this.(AssignExpr).getLValue() + } + + Expr getRightOperand() { + result = this.(BinaryOperation).getRightOperand() + or + result = this.(AssignOperation).getRValue() + or + result = this.(AssignExpr).getRValue() + } + + Expr getAnOperand() { + result = getLeftOperand() or + result = getRightOperand() + } +} + +int getOperandIndexIn(FullExpr fullExpr, Expr operand) { + result = getOperandIndex(fullExpr, operand) + or + fullExpr.(Call).getArgument(result).getAChild*() = operand +} + +int getOperandIndex(LeftRightOperation binop, Expr operand) { + if operand = binop.getAnOperand() + then + operand = binop.getLeftOperand() and + result = 0 + or + operand = binop.getRightOperand() and + result = getLeafCount(binop.getLeftOperand()) + 1 + or + operand = binop.getRightOperand() and + not binop.getLeftOperand() instanceof LeftRightOperation and + result = 1 + else ( + // Child of left operand that is a binary operation. + result = getOperandIndex(binop.getLeftOperand(), operand) + or + // Child of left operand that is not a binary operation. + result = 0 and + not binop.getLeftOperand() instanceof LeftRightOperation and + binop.getLeftOperand().getAChild+() = operand + or + // Child of right operand and both left and right operands are binary operations. + result = + getLeafCount(binop.getLeftOperand()) + getOperandIndex(binop.getRightOperand(), operand) + or + // Child of right operand and left operand is not a binary operation. + result = 1 + getOperandIndex(binop.getRightOperand(), operand) and + not binop.getLeftOperand() instanceof LeftRightOperation + or + // Child of right operand that is not a binary operation and the left operand is a binary operation. + result = getLeafCount(binop.getLeftOperand()) + 1 and + binop.getRightOperand().getAChild+() = operand and + not binop.getRightOperand() instanceof LeftRightOperation + or + // Child of right operand that is not a binary operation and the left operand is not a binary operation. + result = 1 and + not binop.getLeftOperand() instanceof LeftRightOperation and + not binop.getRightOperand() instanceof LeftRightOperation and + binop.getRightOperand().getAChild+() = operand + ) +} + from ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1, VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label @@ -98,11 +193,7 @@ where ) and // Break the symmetry of the ordering relation by requiring that the first expression is located before the second. // This builds upon the assumption that the expressions are part of the same full expression as specified in the ordering configuration. - exists(int offset1, int offset2 | - va1.getLocation().charLoc(_, offset1, _) and - va2.getLocation().charLoc(_, offset2, _) and - offset1 < offset2 - ) and + getOperandIndexIn(fullExpr, va1) < getOperandIndexIn(fullExpr, va2) and placeHolder = variableEffect2 and label = "side effect" ) diff --git a/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected b/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected index de0c33907e..17b89c2f01 100644 --- a/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected +++ b/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected @@ -1,5 +1,6 @@ -| test.c:6:12:6:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:6:12:6:13 | l1 | side effect | test.c:6:12:6:13 | l1 | test.c:4:16:4:17 | l1 | test.c:6:17:6:18 | l1 | side effect | test.c:6:17:6:18 | l1 | test.c:4:16:4:17 | l1 | -| test.c:7:12:7:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:7:12:7:13 | l1 | side effect | test.c:7:12:7:13 | l1 | test.c:4:16:4:17 | l1 | test.c:7:17:7:18 | l2 | side effect | test.c:7:17:7:18 | l2 | test.c:4:20:4:21 | l2 | -| test.c:17:3:17:21 | ... = ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:17:8:17:9 | l1 | side effect | test.c:17:8:17:9 | l1 | test.c:4:16:4:17 | l1 | test.c:17:13:17:14 | l1 | side effect | test.c:17:13:17:14 | l1 | test.c:4:16:4:17 | l1 | -| test.c:19:3:19:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:19:7:19:8 | l1 | side effect | test.c:19:7:19:8 | l1 | test.c:4:16:4:17 | l1 | test.c:19:11:19:12 | l2 | side effect | test.c:19:11:19:12 | l2 | test.c:4:20:4:21 | l2 | -| test.c:25:3:25:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:25:7:25:10 | ... ++ | side effect | test.c:25:7:25:8 | l8 | test.c:15:7:15:8 | l8 | test.c:25:13:25:14 | l8 | read | test.c:25:13:25:14 | l8 | test.c:15:7:15:8 | l8 | +| test.c:6:12:6:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:6:12:6:13 | l1 | side effect | test.c:6:12:6:13 | l1 | l1 | test.c:6:17:6:18 | l1 | side effect | test.c:6:17:6:18 | l1 | l1 | +| test.c:7:12:7:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:7:12:7:13 | l1 | side effect | test.c:7:12:7:13 | l1 | l1 | test.c:7:17:7:18 | l2 | side effect | test.c:7:17:7:18 | l2 | l2 | +| test.c:17:3:17:21 | ... = ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:17:8:17:9 | l1 | side effect | test.c:17:8:17:9 | l1 | l1 | test.c:17:13:17:14 | l1 | side effect | test.c:17:13:17:14 | l1 | l1 | +| test.c:19:3:19:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:19:7:19:8 | l1 | side effect | test.c:19:7:19:8 | l1 | l1 | test.c:19:11:19:12 | l2 | side effect | test.c:19:11:19:12 | l2 | l2 | +| test.c:25:3:25:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:25:7:25:10 | ... ++ | side effect | test.c:25:7:25:8 | l8 | l8 | test.c:25:13:25:14 | l8 | read | test.c:25:13:25:14 | l8 | l8 | +| test.c:35:5:35:13 | ... = ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:35:10:35:12 | ... ++ | side effect | test.c:35:10:35:10 | i | i | test.c:35:10:35:12 | ... ++ | side effect | test.c:35:10:35:10 | i | i | diff --git a/c/misra/test/rules/RULE-13-2/test.c b/c/misra/test/rules/RULE-13-2/test.c index 6fbc827c4f..1bebec3775 100644 --- a/c/misra/test/rules/RULE-13-2/test.c +++ b/c/misra/test/rules/RULE-13-2/test.c @@ -1,6 +1,6 @@ void foo(int, int); -void unsequenced_sideeffects() { +void unsequenced_sideeffects1() { volatile int l1, l2; int l3 = l1 + l1; // NON_COMPLIANT @@ -25,4 +25,13 @@ void unsequenced_sideeffects() { foo(l8++, l8); // NON_COMPLIANT int l10 = l8++, l11 = l8++; // COMPLIANT +} + +int g1[], g2[]; +#define test(i) (g1[i] = g2[i]) +void unsequenced_sideeffects2() { + int i; + for (i = 0; i < 10; i++) { + test(i++); // NON_COMPLIANT + } } \ No newline at end of file From ca80465fb6edf80dc782319fed38385ce00951f3 Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Wed, 29 Mar 2023 16:57:00 -0700 Subject: [PATCH 16/20] Remove PRE31-C from side effects 3 --- rules.csv | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rules.csv b/rules.csv index 5c021ae1ed..a5fa7ceea0 100644 --- a/rules.csv +++ b/rules.csv @@ -586,7 +586,7 @@ c,CERT-C,POS52-C,OutOfScope,Rule,,,Do not perform operations that can block whil c,CERT-C,POS53-C,OutOfScope,Rule,,,Do not use more than one mutex for concurrent waiting operations on a condition variable,,,, c,CERT-C,POS54-C,OutOfScope,Rule,,,Detect and handle POSIX library errors,,,, c,CERT-C,PRE30-C,No,Rule,,,Do not create a universal character name through concatenation,,,Medium, -c,CERT-C,PRE31-C,Yes,Rule,,,Avoid side effects in arguments to unsafe macros,RULE-13-2,SideEffects3,Medium, +c,CERT-C,PRE31-C,Yes,Rule,,,Avoid side effects in arguments to unsafe macros,RULE-13-2,SideEffects,Medium, c,CERT-C,PRE32-C,Yes,Rule,,,Do not use preprocessor directives in invocations of function-like macros,,Preprocessor5,Hard, c,CERT-C,SIG30-C,Yes,Rule,,,Call only asynchronous-safe functions within signal handlers,,SignalHandlers,Medium, c,CERT-C,SIG31-C,Yes,Rule,,,Do not access shared objects in signal handlers,,SignalHandlers,Medium, From f0d8026b4d3959341fa9ff7f9bdd6eb85e802e77 Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Wed, 29 Mar 2023 17:00:39 -0700 Subject: [PATCH 17/20] Update FullExpr.expected --- c/common/test/library/expr/FullExpr.expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/c/common/test/library/expr/FullExpr.expected b/c/common/test/library/expr/FullExpr.expected index 4785b90024..c712793f8b 100644 --- a/c/common/test/library/expr/FullExpr.expected +++ b/c/common/test/library/expr/FullExpr.expected @@ -1,4 +1,4 @@ -| fullexpr.c:8:18:11:37 | temporary object | +| fullexpr.c:8:18:11:37 | {...} | | fullexpr.c:13:3:13:5 | ... ++ | | fullexpr.c:15:7:15:7 | i | | fullexpr.c:17:10:17:10 | i | From 3de4838ac448b27c376711e491ab17fa83aa719f Mon Sep 17 00:00:00 2001 From: Luke Cartey Date: Thu, 30 Mar 2023 10:52:32 +0100 Subject: [PATCH 18/20] Rule 13.2: Improve performance Avoid expensive cross-products on the ConditionalExpr case, and filter by partial expressions earlier in the predicate set. --- .../rules/RULE-13-2/UnsequencedSideEffects.ql | 24 +++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql index 59b4bc660c..1e1d7c568b 100644 --- a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql +++ b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql @@ -27,7 +27,7 @@ class VariableEffectOrAccess extends Expr { pragma[noinline] predicate partOfFullExpr(VariableEffectOrAccess e, FullExpr fe) { ( - e.(VariableEffect).getAnAccess() = fe.getAChild+() + exists(VariableEffect ve | e = ve and ve.getAnAccess() = fe.getAChild+() and not ve.isPartial()) or e.(VariableAccess) = fe.getAChild+() ) @@ -154,6 +154,24 @@ int getOperandIndex(LeftRightOperation binop, Expr operand) { ) } +predicate inConditionalThen(ConditionalExpr ce, Expr e) { + e = ce.getThen() + or + exists(Expr parent | + inConditionalThen(ce, parent) and + parent.getAChild() = e + ) +} + +predicate inConditionalElse(ConditionalExpr ce, Expr e) { + e = ce.getElse() + or + exists(Expr parent | + inConditionalElse(ce, parent) and + parent.getAChild() = e + ) +} + from ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1, VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label @@ -219,8 +237,6 @@ where not variableEffect1.getAChild+() = va2 ) and // Both are evaluated - not exists(ConditionalExpr ce | - ce.getThen().getAChild*() = va1 and ce.getElse().getAChild*() = va2 - ) + not exists(ConditionalExpr ce | inConditionalThen(ce, va1) and inConditionalElse(ce, va2)) select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1, "side effect", va1, va1.getTarget().getName(), placeHolder, label, va2, va2.getTarget().getName() From f9a808a80d154d0a31fa1ba63b007fb3c39e447f Mon Sep 17 00:00:00 2001 From: Luke Cartey Date: Thu, 30 Mar 2023 11:01:35 +0100 Subject: [PATCH 19/20] Rule 13.2: Further perf improvements Extract out the main computation from the exclusion mechanism, otherwise the exclusion mechanism runs on a potentially very large intermediate step (sameFullExpr). --- .../src/rules/RULE-13-2/UnsequencedSideEffects.ql | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql index 1e1d7c568b..c1ac4d4b40 100644 --- a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql +++ b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql @@ -172,11 +172,10 @@ predicate inConditionalElse(ConditionalExpr ce, Expr e) { ) } -from +predicate isUnsequencedEffect( ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1, VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label -where - not isExcluded(fullExpr, SideEffects3Package::unsequencedSideEffectsQuery()) and +) { // The two access are scoped to the same full expression. sameFullExpr(fullExpr, va1, va2) and // We are only interested in effects that change an object, @@ -238,5 +237,13 @@ where ) and // Both are evaluated not exists(ConditionalExpr ce | inConditionalThen(ce, va1) and inConditionalElse(ce, va2)) +} + +from + ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1, + VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label +where + not isExcluded(fullExpr, SideEffects3Package::unsequencedSideEffectsQuery()) and + isUnsequencedEffect(orderingConfig, fullExpr, variableEffect1, va1, va2, placeHolder, label) select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1, "side effect", va1, va1.getTarget().getName(), placeHolder, label, va2, va2.getTarget().getName() From 9eada214d668e66fb27fe501fb16816dc75b7702 Mon Sep 17 00:00:00 2001 From: Luke Cartey Date: Thu, 30 Mar 2023 11:12:53 +0100 Subject: [PATCH 20/20] SideEffects3: Update metadata. --- .../cpp/exclusions/c/SideEffects3.qll | 37 +------------------ 1 file changed, 1 insertion(+), 36 deletions(-) diff --git a/cpp/common/src/codingstandards/cpp/exclusions/c/SideEffects3.qll b/cpp/common/src/codingstandards/cpp/exclusions/c/SideEffects3.qll index 7c1bedf6f7..eff4f2caf9 100644 --- a/cpp/common/src/codingstandards/cpp/exclusions/c/SideEffects3.qll +++ b/cpp/common/src/codingstandards/cpp/exclusions/c/SideEffects3.qll @@ -3,21 +3,9 @@ import cpp import RuleMetadata import codingstandards.cpp.exclusions.RuleMetadata -newtype SideEffects3Query = - TSideEffectsInArgumentsToUnsafeMacrosQuery() or - TUnsequencedSideEffectsQuery() or - TMultipleObjectModificationsQuery() +newtype SideEffects3Query = TUnsequencedSideEffectsQuery() predicate isSideEffects3QueryMetadata(Query query, string queryId, string ruleId, string category) { - query = - // `Query` instance for the `sideEffectsInArgumentsToUnsafeMacros` query - SideEffects3Package::sideEffectsInArgumentsToUnsafeMacrosQuery() and - queryId = - // `@id` for the `sideEffectsInArgumentsToUnsafeMacros` query - "c/cert/side-effects-in-arguments-to-unsafe-macros" and - ruleId = "PRE31-C" and - category = "rule" - or query = // `Query` instance for the `unsequencedSideEffects` query SideEffects3Package::unsequencedSideEffectsQuery() and @@ -26,36 +14,13 @@ predicate isSideEffects3QueryMetadata(Query query, string queryId, string ruleId "c/misra/unsequenced-side-effects" and ruleId = "RULE-13-2" and category = "required" - or - query = - // `Query` instance for the `multipleObjectModifications` query - SideEffects3Package::multipleObjectModificationsQuery() and - queryId = - // `@id` for the `multipleObjectModifications` query - "c/misra/multiple-object-modifications" and - ruleId = "RULE-13-2" and - category = "required" } module SideEffects3Package { - Query sideEffectsInArgumentsToUnsafeMacrosQuery() { - //autogenerate `Query` type - result = - // `Query` type for `sideEffectsInArgumentsToUnsafeMacros` query - TQueryC(TSideEffects3PackageQuery(TSideEffectsInArgumentsToUnsafeMacrosQuery())) - } - Query unsequencedSideEffectsQuery() { //autogenerate `Query` type result = // `Query` type for `unsequencedSideEffects` query TQueryC(TSideEffects3PackageQuery(TUnsequencedSideEffectsQuery())) } - - Query multipleObjectModificationsQuery() { - //autogenerate `Query` type - result = - // `Query` type for `multipleObjectModifications` query - TQueryC(TSideEffects3PackageQuery(TMultipleObjectModificationsQuery())) - } }