Skip to content

Commit 743c80d

Browse files
committed
The implementation of RULE-4-6-1 and RULE-13-2 should not be shared
1 parent c22c060 commit 743c80d

File tree

24 files changed

+249
-387
lines changed

24 files changed

+249
-387
lines changed

.vscode/settings.json

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
{
2+
"codeQL.cli.executablePath": "/Users/mauro/Desktop/CodeQL/bundles/codeql-2.14.6/codeql",
3+
"codeQL.runningQueries.numberOfThreads": 0,
4+
"codeQL.runningTests.numberOfThreads": 0
5+
}

c/cert/src/rules/EXP30-C/DependenceOnOrderOfScalarEvaluationForSideEffects.ql

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@
1414
import cpp
1515
import codingstandards.c.cert
1616
import codingstandards.cpp.SideEffect
17-
import codingstandards.cpp.COrdering
1817
import codingstandards.c.orderofevaluation.VariableAccessOrdering
1918

2019
from

cpp/common/src/codingstandards/cpp/COrdering.qll renamed to c/common/src/codingstandards/c/Ordering.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
import cpp
22
import codingstandards.cpp.SideEffect
3-
import codingstandards.cpp.CExpr
3+
import codingstandards.c.Expr
44
import codingstandards.cpp.Variable
55

66
module Ordering {

c/common/src/codingstandards/c/orderofevaluation/VariableAccessOrdering.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
import cpp
2-
import codingstandards.cpp.COrdering
2+
import codingstandards.c.Ordering
33

44
class VariableAccessInFullExpressionOrdering extends Ordering::Configuration {
55
VariableAccessInFullExpressionOrdering() { this = "VariableAccessInFullExpressionOrdering" }

c/common/test/rules/memoryoperationsnotsequencedappropriately/MemoryOperationsNotSequencedAppropriately.expected

Lines changed: 0 additions & 6 deletions
This file was deleted.

c/common/test/rules/memoryoperationsnotsequencedappropriately/MemoryOperationsNotSequencedAppropriately.ql

Lines changed: 0 additions & 4 deletions
This file was deleted.

c/misra/src/rules/RULE-12-1/ImplicitPrecedenceOfOperatorsInExpression.ql

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@
1414

1515
import cpp
1616
import codingstandards.c.misra
17-
import codingstandards.cpp.CExpr
17+
import codingstandards.c.Expr
1818

1919
int getPrecedence(Expr e) {
2020
e instanceof PrimaryExpr and result = 16

c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql

Lines changed: 231 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,236 @@
1313

1414
import cpp
1515
import codingstandards.c.misra
16-
import codingstandards.cpp.rules.memoryoperationsnotsequencedappropriately.MemoryOperationsNotSequencedAppropriately
16+
import codingstandards.c.Ordering
17+
import codingstandards.cpp.SideEffects
1718

18-
class UnsequencedSideEffectsQuery extends MemoryOperationsNotSequencedAppropriatelySharedQuery {
19-
UnsequencedSideEffectsQuery() { this = SideEffects3Package::unsequencedSideEffectsQuery() }
19+
class VariableEffectOrAccess extends Expr {
20+
VariableEffectOrAccess() {
21+
this instanceof VariableEffect or
22+
this instanceof VariableAccess
23+
}
2024
}
25+
26+
pragma[noinline]
27+
predicate partOfFullExpr(VariableEffectOrAccess e, FullExpr fe) {
28+
(
29+
exists(VariableEffect ve | e = ve and ve.getAnAccess() = fe.getAChild+() and not ve.isPartial())
30+
or
31+
e.(VariableAccess) = fe.getAChild+()
32+
)
33+
}
34+
35+
class ConstituentExprOrdering extends Ordering::Configuration {
36+
ConstituentExprOrdering() { this = "ConstituentExprOrdering" }
37+
38+
override predicate isCandidate(Expr e1, Expr e2) {
39+
exists(FullExpr fe |
40+
partOfFullExpr(e1, fe) and
41+
partOfFullExpr(e2, fe)
42+
)
43+
}
44+
}
45+
46+
predicate sameFullExpr(FullExpr fe, VariableAccess va1, VariableAccess va2) {
47+
partOfFullExpr(va1, fe) and
48+
partOfFullExpr(va2, fe) and
49+
va1 != va2 and
50+
exists(Variable v1, Variable v2 |
51+
// Use `pragma[only_bind_into]` to prevent CP between variable accesses.
52+
va1.getTarget() = pragma[only_bind_into](v1) and va2.getTarget() = pragma[only_bind_into](v2)
53+
|
54+
v1.isVolatile() and v2.isVolatile()
55+
or
56+
not (v1.isVolatile() and v2.isVolatile()) and
57+
v1 = v2
58+
)
59+
}
60+
61+
int getLeafCount(LeftRightOperation bop) {
62+
if
63+
not bop.getLeftOperand() instanceof BinaryOperation and
64+
not bop.getRightOperand() instanceof BinaryOperation
65+
then result = 2
66+
else
67+
if
68+
bop.getLeftOperand() instanceof BinaryOperation and
69+
not bop.getRightOperand() instanceof BinaryOperation
70+
then result = 1 + getLeafCount(bop.getLeftOperand())
71+
else
72+
if
73+
not bop.getLeftOperand() instanceof BinaryOperation and
74+
bop.getRightOperand() instanceof BinaryOperation
75+
then result = 1 + getLeafCount(bop.getRightOperand())
76+
else result = getLeafCount(bop.getLeftOperand()) + getLeafCount(bop.getRightOperand())
77+
}
78+
79+
class LeftRightOperation extends Expr {
80+
LeftRightOperation() {
81+
this instanceof BinaryOperation or
82+
this instanceof AssignOperation or
83+
this instanceof AssignExpr
84+
}
85+
86+
Expr getLeftOperand() {
87+
result = this.(BinaryOperation).getLeftOperand()
88+
or
89+
result = this.(AssignOperation).getLValue()
90+
or
91+
result = this.(AssignExpr).getLValue()
92+
}
93+
94+
Expr getRightOperand() {
95+
result = this.(BinaryOperation).getRightOperand()
96+
or
97+
result = this.(AssignOperation).getRValue()
98+
or
99+
result = this.(AssignExpr).getRValue()
100+
}
101+
102+
Expr getAnOperand() {
103+
result = getLeftOperand() or
104+
result = getRightOperand()
105+
}
106+
}
107+
108+
int getOperandIndexIn(FullExpr fullExpr, Expr operand) {
109+
result = getOperandIndex(fullExpr, operand)
110+
or
111+
fullExpr.(Call).getArgument(result).getAChild*() = operand
112+
}
113+
114+
int getOperandIndex(LeftRightOperation binop, Expr operand) {
115+
if operand = binop.getAnOperand()
116+
then
117+
operand = binop.getLeftOperand() and
118+
result = 0
119+
or
120+
operand = binop.getRightOperand() and
121+
result = getLeafCount(binop.getLeftOperand()) + 1
122+
or
123+
operand = binop.getRightOperand() and
124+
not binop.getLeftOperand() instanceof LeftRightOperation and
125+
result = 1
126+
else (
127+
// Child of left operand that is a binary operation.
128+
result = getOperandIndex(binop.getLeftOperand(), operand)
129+
or
130+
// Child of left operand that is not a binary operation.
131+
result = 0 and
132+
not binop.getLeftOperand() instanceof LeftRightOperation and
133+
binop.getLeftOperand().getAChild+() = operand
134+
or
135+
// Child of right operand and both left and right operands are binary operations.
136+
result =
137+
getLeafCount(binop.getLeftOperand()) + getOperandIndex(binop.getRightOperand(), operand)
138+
or
139+
// Child of right operand and left operand is not a binary operation.
140+
result = 1 + getOperandIndex(binop.getRightOperand(), operand) and
141+
not binop.getLeftOperand() instanceof LeftRightOperation
142+
or
143+
// Child of right operand that is not a binary operation and the left operand is a binary operation.
144+
result = getLeafCount(binop.getLeftOperand()) + 1 and
145+
binop.getRightOperand().getAChild+() = operand and
146+
not binop.getRightOperand() instanceof LeftRightOperation
147+
or
148+
// Child of right operand that is not a binary operation and the left operand is not a binary operation.
149+
result = 1 and
150+
not binop.getLeftOperand() instanceof LeftRightOperation and
151+
not binop.getRightOperand() instanceof LeftRightOperation and
152+
binop.getRightOperand().getAChild+() = operand
153+
)
154+
}
155+
156+
predicate inConditionalThen(ConditionalExpr ce, Expr e) {
157+
e = ce.getThen()
158+
or
159+
exists(Expr parent |
160+
inConditionalThen(ce, parent) and
161+
parent.getAChild() = e
162+
)
163+
}
164+
165+
predicate inConditionalElse(ConditionalExpr ce, Expr e) {
166+
e = ce.getElse()
167+
or
168+
exists(Expr parent |
169+
inConditionalElse(ce, parent) and
170+
parent.getAChild() = e
171+
)
172+
}
173+
174+
predicate isUnsequencedEffect(
175+
ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1,
176+
VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label
177+
) {
178+
// The two access are scoped to the same full expression.
179+
sameFullExpr(fullExpr, va1, va2) and
180+
// We are only interested in effects that change an object,
181+
// 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`.
182+
not variableEffect1.isPartial() and
183+
variableEffect1.getAnAccess() = va1 and
184+
(
185+
exists(VariableEffect variableEffect2 |
186+
not variableEffect2.isPartial() and
187+
variableEffect2.getAnAccess() = va2 and
188+
// If the effect is not local (happens in a different function) we use the call with the access as a proxy.
189+
(
190+
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
191+
va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
192+
orderingConfig.isUnsequenced(variableEffect1, variableEffect2)
193+
or
194+
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
195+
not va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
196+
exists(Call call |
197+
call.getAnArgument() = va2 and call.getEnclosingStmt() = va1.getEnclosingStmt()
198+
|
199+
orderingConfig.isUnsequenced(variableEffect1, call)
200+
)
201+
or
202+
not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
203+
va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
204+
exists(Call call |
205+
call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt()
206+
|
207+
orderingConfig.isUnsequenced(call, variableEffect2)
208+
)
209+
) and
210+
// Break the symmetry of the ordering relation by requiring that the first expression is located before the second.
211+
// This builds upon the assumption that the expressions are part of the same full expression as specified in the ordering configuration.
212+
getOperandIndexIn(fullExpr, va1) < getOperandIndexIn(fullExpr, va2) and
213+
placeHolder = variableEffect2 and
214+
label = "side effect"
215+
)
216+
or
217+
placeHolder = va2 and
218+
label = "read" and
219+
not exists(VariableEffect variableEffect2 | variableEffect1 != variableEffect2 |
220+
variableEffect2.getAnAccess() = va2
221+
) and
222+
(
223+
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
224+
orderingConfig.isUnsequenced(variableEffect1, va2)
225+
or
226+
not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
227+
exists(Call call |
228+
call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt()
229+
|
230+
orderingConfig.isUnsequenced(call, va2)
231+
)
232+
) and
233+
// The read is not used to compute the effect on the variable.
234+
// E.g., exclude x = x + 1
235+
not variableEffect1.getAChild+() = va2
236+
) and
237+
// Both are evaluated
238+
not exists(ConditionalExpr ce | inConditionalThen(ce, va1) and inConditionalElse(ce, va2))
239+
}
240+
241+
from
242+
ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1,
243+
VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label
244+
where
245+
not isExcluded(fullExpr, SideEffects3Package::unsequencedSideEffectsQuery()) and
246+
isUnsequencedEffect(orderingConfig, fullExpr, variableEffect1, va1, va2, placeHolder, label)
247+
select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1,
248+
"side effect", va1, va1.getTarget().getName(), placeHolder, label, va2, va2.getTarget().getName()

c/misra/src/rules/RULE-13-3/SideEffectAndCrementInFullExpression.ql

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@
1515

1616
import cpp
1717
import codingstandards.c.misra
18-
import codingstandards.cpp.CExpr
18+
import codingstandards.c.Expr
1919
import codingstandards.cpp.SideEffects
2020

2121
from FullExpr e, SideEffect se, CrementOperation op
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
| 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 |
2+
| 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 |
3+
| 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 |
4+
| 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 |
5+
| 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 |
6+
| 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 |
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
rules/RULE-13-2/UnsequencedSideEffects.ql

c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.testref

Lines changed: 0 additions & 1 deletion
This file was deleted.
Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
// NOTICE: THE TEST CASES BELOW ARE ALSO INCLUDED IN THE C++ TEST CASE AND
2-
// CHANGES SHOULD BE REFLECTED THERE AS WELL.
31
void foo(int, int);
42

53
void unsequenced_sideeffects1() {
@@ -29,7 +27,7 @@ void unsequenced_sideeffects1() {
2927
int l10 = l8++, l11 = l8++; // COMPLIANT
3028
}
3129

32-
int g1[10], g2[10];
30+
int g1[], g2[];
3331
#define test(i) (g1[i] = g2[i])
3432
void unsequenced_sideeffects2() {
3533
int i;

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

Lines changed: 0 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,6 @@ newtype ImportMisra23Query =
6161
TCstdioFunctionsShallNotBeUsedQuery() or
6262
TCstdioMacrosShallNotBeUsedQuery() or
6363
TCstdioTypesShallNotBeUsedQuery() or
64-
TMemoryOperationsNotSequencedAppropriatelyQuery() or
6564
TBackslashCharacterMisuseQuery() or
6665
TNonTerminatedEscapeSequencesQuery() or
6766
TOctalConstantsUsedQuery() or
@@ -604,15 +603,6 @@ predicate isImportMisra23QueryMetadata(Query query, string queryId, string ruleI
604603
ruleId = "RULE-30-0-1" and
605604
category = "required"
606605
or
607-
query =
608-
// `Query` instance for the `memoryOperationsNotSequencedAppropriately` query
609-
ImportMisra23Package::memoryOperationsNotSequencedAppropriatelyQuery() and
610-
queryId =
611-
// `@id` for the `memoryOperationsNotSequencedAppropriately` query
612-
"cpp/misra/memory-operations-not-sequenced-appropriately" and
613-
ruleId = "RULE-4-6-1" and
614-
category = "required"
615-
or
616606
query =
617607
// `Query` instance for the `backslashCharacterMisuse` query
618608
ImportMisra23Package::backslashCharacterMisuseQuery() and
@@ -1257,13 +1247,6 @@ module ImportMisra23Package {
12571247
TQueryCPP(TImportMisra23PackageQuery(TCstdioTypesShallNotBeUsedQuery()))
12581248
}
12591249

1260-
Query memoryOperationsNotSequencedAppropriatelyQuery() {
1261-
//autogenerate `Query` type
1262-
result =
1263-
// `Query` type for `memoryOperationsNotSequencedAppropriately` query
1264-
TQueryCPP(TImportMisra23PackageQuery(TMemoryOperationsNotSequencedAppropriatelyQuery()))
1265-
}
1266-
12671250
Query backslashCharacterMisuseQuery() {
12681251
//autogenerate `Query` type
12691252
result =

0 commit comments

Comments
 (0)