Skip to content

Commit 9deadab

Browse files
rvermeulenrvermeulen
committed
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.
1 parent 962a640 commit 9deadab

File tree

3 files changed

+87
-55
lines changed

3 files changed

+87
-55
lines changed

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

Lines changed: 80 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -17,13 +17,15 @@ import codingstandards.c.Expr
1717
import codingstandards.c.SideEffects
1818
import codingstandards.c.Ordering
1919

20-
predicate isOrHasSideEffect(Expr e) {
21-
e instanceof VariableEffect or
22-
any(VariableEffect ve).getAnAccess() = e
20+
class VariableEffectOrAccess extends Expr {
21+
VariableEffectOrAccess() {
22+
this instanceof VariableEffect or
23+
this instanceof VariableAccess
24+
}
2325
}
2426

25-
predicate partOfFullExpr(Expr e, FullExpr fe) {
26-
isOrHasSideEffect(e) and
27+
pragma[noinline]
28+
predicate partOfFullExpr(VariableEffectOrAccess e, FullExpr fe) {
2729
(
2830
e.(VariableEffect).getAnAccess() = fe.getAChild+()
2931
or
@@ -42,62 +44,92 @@ class ConstituentExprOrdering extends Ordering::Configuration {
4244
}
4345
}
4446

45-
pragma[noinline]
46-
predicate sameFullExpr(FullExpr fe, Expr e1, Expr e2) {
47-
partOfFullExpr(e1, fe) and
48-
partOfFullExpr(e2, fe)
49-
}
50-
51-
predicate destructureEffect(VariableEffect ve, VariableAccess va, Variable v) {
52-
ve.getAnAccess() = va and
53-
va.getTarget() = v and
54-
ve.getTarget() = v
47+
predicate sameFullExpr(FullExpr fe, VariableAccess va1, VariableAccess va2) {
48+
partOfFullExpr(va1, fe) and
49+
partOfFullExpr(va2, fe) and
50+
va1 != va2 and
51+
exists(Variable v1, Variable v2 |
52+
// Use `pragma[only_bind_into]` to prevent CP between variable accesses.
53+
va1.getTarget() = pragma[only_bind_into](v1) and va2.getTarget() = pragma[only_bind_into](v2)
54+
|
55+
v1.isVolatile() and v2.isVolatile()
56+
or
57+
not (v1.isVolatile() and v2.isVolatile()) and
58+
v1 = v2
59+
)
5560
}
5661

5762
from
5863
ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1,
59-
VariableEffect variableEffect2, VariableAccess va1, VariableAccess va2, Variable v1, Variable v2
64+
VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label
6065
where
6166
not isExcluded(fullExpr, SideEffects3Package::unsequencedSideEffectsQuery()) and
67+
// The two access are scoped to the same full expression.
6268
sameFullExpr(fullExpr, va1, va2) and
63-
destructureEffect(variableEffect1, va1, v1) and
64-
destructureEffect(variableEffect2, va2, v2) and
65-
// Exclude the same effect applying to different objects.
66-
// This occurs when on is a subject of the other.
67-
// For example, foo.bar = 1; where both foo and bar are objects modified by the assignment.
68-
variableEffect1 != variableEffect2 and
69-
// If the effect is not local (happens in a different function) we use the call with the access as a proxy.
69+
// We are only interested in effects that change an object,
70+
// 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`.
71+
not variableEffect1.isPartial() and
72+
variableEffect1.getAnAccess() = va1 and
7073
(
71-
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
72-
va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
73-
orderingConfig.isUnsequenced(variableEffect1, variableEffect2)
74-
or
75-
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
76-
not va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
77-
exists(Call call |
78-
call.getAnArgument() = va2 and call.getEnclosingStmt() = va1.getEnclosingStmt()
79-
|
80-
orderingConfig.isUnsequenced(variableEffect1, call)
74+
exists(VariableEffect variableEffect2 |
75+
not variableEffect2.isPartial() and
76+
variableEffect2.getAnAccess() = va2 and
77+
// If the effect is not local (happens in a different function) we use the call with the access as a proxy.
78+
(
79+
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
80+
va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
81+
orderingConfig.isUnsequenced(variableEffect1, variableEffect2)
82+
or
83+
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
84+
not va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
85+
exists(Call call |
86+
call.getAnArgument() = va2 and call.getEnclosingStmt() = va1.getEnclosingStmt()
87+
|
88+
orderingConfig.isUnsequenced(variableEffect1, call)
89+
)
90+
or
91+
not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
92+
va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
93+
exists(Call call |
94+
call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt()
95+
|
96+
orderingConfig.isUnsequenced(call, variableEffect2)
97+
)
98+
) and
99+
// Break the symmetry of the ordering relation by requiring that the first expression is located before the second.
100+
// This builds upon the assumption that the expressions are part of the same full expression as specified in the ordering configuration.
101+
exists(int offset1, int offset2 |
102+
va1.getLocation().charLoc(_, offset1, _) and
103+
va2.getLocation().charLoc(_, offset2, _) and
104+
offset1 < offset2
105+
) and
106+
placeHolder = variableEffect2 and
107+
label = "side effect"
81108
)
82109
or
83-
not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
84-
va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
85-
exists(Call call |
86-
call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt()
87-
|
88-
orderingConfig.isUnsequenced(call, variableEffect2)
89-
)
110+
placeHolder = va2 and
111+
label = "read" and
112+
not exists(VariableEffect variableEffect2 | variableEffect1 != variableEffect2 |
113+
variableEffect2.getAnAccess() = va2
114+
) and
115+
(
116+
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
117+
orderingConfig.isUnsequenced(variableEffect1, va2)
118+
or
119+
not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
120+
exists(Call call |
121+
call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt()
122+
|
123+
orderingConfig.isUnsequenced(call, va2)
124+
)
125+
) and
126+
// The read is not used to compute the effect on the variable.
127+
// E.g., exclude x = x + 1
128+
not variableEffect1.getAChild+() = va2
90129
) and
91130
// Both are evaluated
92131
not exists(ConditionalExpr ce |
93132
ce.getThen().getAChild*() = va1 and ce.getElse().getAChild*() = va2
94-
) and
95-
// Break the symmetry of the ordering relation by requiring that the first expression is located before the second.
96-
// This builds upon the assumption that the expressions are part of the same full expression as specified in the ordering configuration.
97-
exists(int offset1, int offset2 |
98-
va1.getLocation().charLoc(_, offset1, _) and
99-
va2.getLocation().charLoc(_, offset2, _) and
100-
offset1 < offset2
101133
)
102134
select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1,
103-
"side effect", va1, v1.getName(), variableEffect2, "side effect", va2, v2.getName()
135+
"side effect", va1, va1.getTarget(), placeHolder, label, va2, va2.getTarget()

‎c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
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:16 | ... ++ | side effect | test.c:25:13:25:14 | l9 | l9 |
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 | 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 |
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 | 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 |
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 | 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 |
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 | 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 |
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 | 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 |

‎c/misra/test/rules/RULE-13-2/test.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,8 @@ void unsequenced_sideeffects() {
2121
l8 = l1;
2222
// Store value of volatile object in temporary non-volatile object.
2323
l9 = l2;
24-
foo(l8, l9); // COMPLIANT
25-
foo(l8++, l9++); // NON_COMPLIANT
24+
foo(l8, l9); // COMPLIANT
25+
foo(l8++, l8); // NON_COMPLIANT
2626

2727
int l10 = l8++, l11 = l8++; // COMPLIANT
2828
}

0 commit comments

Comments
 (0)