Skip to content

Commit 96317b6

Browse files
committed
Add query for RULE 13-2
1 parent 86540f5 commit 96317b6

File tree

4 files changed

+93
-0
lines changed

4 files changed

+93
-0
lines changed
Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
/**
2+
* @id c/misra/unsequenced-side-effects
3+
* @name RULE-13-2: The value of an expression and its persistent side effects depend on its evaluation order
4+
* @description The value of an expression and its persistent side effects are depending on the
5+
* evaluation order resulting in unpredictable behavior.
6+
* @kind problem
7+
* @precision very-high
8+
* @problem.severity error
9+
* @tags external/misra/id/rule-13-2
10+
* correctness
11+
* external/misra/obligation/required
12+
*/
13+
14+
import cpp
15+
import codingstandards.c.misra
16+
import codingstandards.c.Expr
17+
import codingstandards.c.SideEffects
18+
import codingstandards.c.Ordering
19+
20+
predicate isCandidatePair(Expr parentExpr, Expr e1, Expr e2) {
21+
parentExpr.getAChild+() = e1 and
22+
parentExpr.getAChild+() = e2
23+
}
24+
25+
class ConstituentExprOrdering extends Ordering::Configuration {
26+
ConstituentExprOrdering() { this = "ConstituentExprOrdering" }
27+
28+
override predicate isCandidate(Expr e1, Expr e2) {
29+
// Two different expressions part of the same full expression.
30+
// Compute differerence using successor relation to break the symmetry of the candidate relation.
31+
isCandidatePair(_, e1, e2)
32+
}
33+
}
34+
35+
from
36+
ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1,
37+
VariableEffect variableEffect2
38+
where
39+
not isExcluded(fullExpr, SideEffects3Package::unsequencedSideEffectsQuery()) and
40+
// If the effect is local we can directly check if it is unsequenced.
41+
// If the effect is not local (happens in a different function) we use the access as a proxy.
42+
orderingConfig.isUnsequenced(variableEffect1, variableEffect2) and
43+
fullExpr.getAChild+() = variableEffect1 and
44+
fullExpr.getAChild+() = variableEffect2 and
45+
// Both are evaluated
46+
not exists(ConditionalExpr ce |
47+
ce.getThen().getAChild*() = variableEffect1 and ce.getElse().getAChild*() = variableEffect2
48+
) and
49+
// Break the symmetry of the ordering relation by requiring that the first expression is located before the second.
50+
// This builds upon the assumption that the expressions are part of the same full expression as specified in the ordering configuration.
51+
exists(int offset1, int offset2 |
52+
variableEffect1.getLocation().charLoc(_, offset1, _) and
53+
variableEffect2.getLocation().charLoc(_, offset2, _) and
54+
offset1 < offset2
55+
)
56+
select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1,
57+
"side effect", variableEffect1.getAnAccess(), variableEffect1.getTarget().getName(),
58+
variableEffect2, "side effect", variableEffect2.getAnAccess(),
59+
variableEffect2.getTarget().getName()
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +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 |
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/test.c

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
void foo(int, int);
2+
3+
void unsequenced_sideeffects() {
4+
volatile int l1, l2;
5+
6+
int l3 = l1 + l1; // NON_COMPLIANT
7+
int l4 = l1 + l2; // NON_COMPLIANT
8+
9+
// Store value of volatile object in temporary non-volatile object.
10+
int l5 = l1;
11+
// Store value of volatile object in temporary non-volatile object.
12+
int l6 = l2;
13+
int l7 = l5 + l6; // COMPLIANT
14+
15+
int l8, l9;
16+
l1 = l1 & 0x80; // COMPLIANT
17+
l8 = l1 = l1 & 0x80; // NON_COMPLIANT
18+
19+
foo(l1, l2); // NON_COMPLIANT
20+
// Store value of volatile object in temporary non-volatile object.
21+
l8 = l1;
22+
// Store value of volatile object in temporary non-volatile object.
23+
l9 = l2;
24+
foo(l8, l9); // COMPLIANT
25+
foo(l8++, l9++); // NON_COMPLIANT
26+
27+
int l10 = l8++, l11 = l8++; // COMPLIANT
28+
}

0 commit comments

Comments
 (0)