Skip to content

Commit dc02657

Browse files
committed
Add support for MISRA example case
1 parent bef7b9e commit dc02657

File tree

3 files changed

+112
-11
lines changed

3 files changed

+112
-11
lines changed

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

Lines changed: 96 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,101 @@ predicate sameFullExpr(FullExpr fe, VariableAccess va1, VariableAccess va2) {
5959
)
6060
}
6161

62+
int getLeafCount(LeftRightOperation bop) {
63+
if
64+
not bop.getLeftOperand() instanceof BinaryOperation and
65+
not bop.getRightOperand() instanceof BinaryOperation
66+
then result = 2
67+
else
68+
if
69+
bop.getLeftOperand() instanceof BinaryOperation and
70+
not bop.getRightOperand() instanceof BinaryOperation
71+
then result = 1 + getLeafCount(bop.getLeftOperand())
72+
else
73+
if
74+
not bop.getLeftOperand() instanceof BinaryOperation and
75+
bop.getRightOperand() instanceof BinaryOperation
76+
then result = 1 + getLeafCount(bop.getRightOperand())
77+
else result = getLeafCount(bop.getLeftOperand()) + getLeafCount(bop.getRightOperand())
78+
}
79+
80+
class LeftRightOperation extends Expr {
81+
LeftRightOperation() {
82+
this instanceof BinaryOperation or
83+
this instanceof AssignOperation or
84+
this instanceof AssignExpr
85+
}
86+
87+
Expr getLeftOperand() {
88+
result = this.(BinaryOperation).getLeftOperand()
89+
or
90+
result = this.(AssignOperation).getLValue()
91+
or
92+
result = this.(AssignExpr).getLValue()
93+
}
94+
95+
Expr getRightOperand() {
96+
result = this.(BinaryOperation).getRightOperand()
97+
or
98+
result = this.(AssignOperation).getRValue()
99+
or
100+
result = this.(AssignExpr).getRValue()
101+
}
102+
103+
Expr getAnOperand() {
104+
result = getLeftOperand() or
105+
result = getRightOperand()
106+
}
107+
}
108+
109+
int getOperandIndexIn(FullExpr fullExpr, Expr operand) {
110+
result = getOperandIndex(fullExpr, operand)
111+
or
112+
fullExpr.(Call).getArgument(result).getAChild*() = operand
113+
}
114+
115+
int getOperandIndex(LeftRightOperation binop, Expr operand) {
116+
if operand = binop.getAnOperand()
117+
then
118+
operand = binop.getLeftOperand() and
119+
result = 0
120+
or
121+
operand = binop.getRightOperand() and
122+
result = getLeafCount(binop.getLeftOperand()) + 1
123+
or
124+
operand = binop.getRightOperand() and
125+
not binop.getLeftOperand() instanceof LeftRightOperation and
126+
result = 1
127+
else (
128+
// Child of left operand that is a binary operation.
129+
result = getOperandIndex(binop.getLeftOperand(), operand)
130+
or
131+
// Child of left operand that is not a binary operation.
132+
result = 0 and
133+
not binop.getLeftOperand() instanceof LeftRightOperation and
134+
binop.getLeftOperand().getAChild+() = operand
135+
or
136+
// Child of right operand and both left and right operands are binary operations.
137+
result =
138+
getLeafCount(binop.getLeftOperand()) + getOperandIndex(binop.getRightOperand(), operand)
139+
or
140+
// Child of right operand and left operand is not a binary operation.
141+
result = 1 + getOperandIndex(binop.getRightOperand(), operand) and
142+
not binop.getLeftOperand() instanceof LeftRightOperation
143+
or
144+
// Child of right operand that is not a binary operation and the left operand is a binary operation.
145+
result = getLeafCount(binop.getLeftOperand()) + 1 and
146+
binop.getRightOperand().getAChild+() = operand and
147+
not binop.getRightOperand() instanceof LeftRightOperation
148+
or
149+
// Child of right operand that is not a binary operation and the left operand is not a binary operation.
150+
result = 1 and
151+
not binop.getLeftOperand() instanceof LeftRightOperation and
152+
not binop.getRightOperand() instanceof LeftRightOperation and
153+
binop.getRightOperand().getAChild+() = operand
154+
)
155+
}
156+
62157
from
63158
ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1,
64159
VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label
@@ -98,11 +193,7 @@ where
98193
) and
99194
// Break the symmetry of the ordering relation by requiring that the first expression is located before the second.
100195
// 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
196+
getOperandIndexIn(fullExpr, va1) < getOperandIndexIn(fullExpr, va2) and
106197
placeHolder = variableEffect2 and
107198
label = "side effect"
108199
)
Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +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 | 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 |
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 |

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

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
void foo(int, int);
22

3-
void unsequenced_sideeffects() {
3+
void unsequenced_sideeffects1() {
44
volatile int l1, l2;
55

66
int l3 = l1 + l1; // NON_COMPLIANT
@@ -25,4 +25,13 @@ void unsequenced_sideeffects() {
2525
foo(l8++, l8); // NON_COMPLIANT
2626

2727
int l10 = l8++, l11 = l8++; // COMPLIANT
28+
}
29+
30+
int g1[], g2[];
31+
#define test(i) (g1[i] = g2[i])
32+
void unsequenced_sideeffects2() {
33+
int i;
34+
for (i = 0; i < 10; i++) {
35+
test(i++); // NON_COMPLIANT
36+
}
2837
}

0 commit comments

Comments
 (0)