Skip to content

Commit 90b4bda

Browse files
lcarteylcartey
authored
Merge pull request #282 from github/lcartey/side-effects3-perf
Package `SideEffects3` with added performance fixes
2 parents 06cc7e3 + dd23ea5 commit 90b4bda

File tree

13 files changed

+390
-16
lines changed

13 files changed

+390
-16
lines changed

‎.vscode/tasks.json

+3-2
Original file line numberDiff line numberDiff line change
@@ -203,8 +203,8 @@
203203
"Concurrency1",
204204
"Concurrency2",
205205
"Concurrency3",
206-
"Concurrency4",
207-
"Concurrency5",
206+
"Concurrency4",
207+
"Concurrency5",
208208
"Conditionals",
209209
"Const",
210210
"DeadCode",
@@ -257,6 +257,7 @@
257257
"Scope",
258258
"SideEffects1",
259259
"SideEffects2",
260+
"SideEffects3",
260261
"SmartPointers1",
261262
"SmartPointers2",
262263
"Strings",

‎c/common/src/codingstandards/c/Expr.qll

+13-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,19 @@ import cpp
33
/* A full expression as defined in ISO/IEC 9899:2011 6.8 point 4 and Annex C point 1 item 5. */
44
class FullExpr extends Expr {
55
FullExpr() {
6-
not this.getParent() instanceof Expr and
7-
not exists(Variable v | v.getInitializer().getExpr() = this)
6+
exists(ExprStmt s | this = s.getExpr())
7+
or
8+
exists(Loop l | this = l.getControllingExpr())
9+
or
10+
exists(ConditionalStmt s | this = s.getControllingExpr())
11+
or
12+
exists(ForStmt s | this = s.getUpdate())
13+
or
14+
exists(ReturnStmt s | this = s.getExpr())
15+
or
16+
this instanceof AggregateLiteral
17+
or
18+
this = any(Variable v).getInitializer().getExpr()
819
}
920
}
1021

‎c/common/src/codingstandards/c/Ordering.qll

+26-9
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ module Ordering {
1313
/**
1414
* Holds if `e1` is sequenced before `e2` as defined by Annex C in ISO/IEC 9899:2011
1515
* This limits to expression and we do not consider the sequence points that are not amenable to modelling:
16-
* - after a full declarator as described in 6.7.6 point 3.
1716
* - before a library function returns (see 7.1.4 point 3).
1817
* - after the actions associated with each formatted I/O function conversion specifier (see 7.21.6 point 1 & 7.29.2 point 1).
1918
* - between the expr before and after a call to a comparison function,
@@ -28,36 +27,36 @@ module Ordering {
2827
// before the actual call.
2928
exists(Call call |
3029
(
31-
call.getAnArgument() = e1
30+
call.getAnArgument().getAChild*() = e1
3231
or
3332
// Postfix expression designating the called function
3433
// We current only handle call through function pointers because the postfix expression
3534
// of regular function calls is not available. That is, identifying `f` in `f(...)`
36-
call.(ExprCall).getExpr() = e1
35+
call.(ExprCall).getExpr().getAChild*() = e1
3736
) and
3837
call.getTarget() = e2.getEnclosingFunction()
3938
)
4039
or
41-
// 6.5.13 point 4 & 6.5.14 point 4 - The operators guarantee left-to-righ evaluation and there is
40+
// 6.5.13 point 4 & 6.5.14 point 4 - The operators guarantee left-to-right evaluation and there is
4241
// a sequence point between the first and second operand if the latter is evaluated.
4342
exists(BinaryLogicalOperation blop |
4443
blop instanceof LogicalAndExpr or blop instanceof LogicalOrExpr
4544
|
46-
blop.getLeftOperand() = e1 and blop.getRightOperand() = e2
45+
blop.getLeftOperand().getAChild*() = e1 and blop.getRightOperand().getAChild*() = e2
4746
)
4847
or
49-
// 6.5.17 point 2 - There is a sequence pointt between the left operand and the right operand.
48+
// 6.5.17 point 2 - There is a sequence point between the left operand and the right operand.
5049
exists(CommaExpr ce, Expr lhs, Expr rhs |
5150
lhs = ce.getLeftOperand() and
5251
rhs = ce.getRightOperand()
5352
|
54-
lhs = e1.getParent*() and rhs = e2.getParent*()
53+
lhs.getAChild*() = e1 and rhs.getAChild*() = e2
5554
)
5655
or
5756
// 6.5.15 point 4 - There is a sequence point between the first operand and the evaluation of the second or third.
5857
exists(ConditionalExpr cond |
59-
cond.getCondition() = e1 and
60-
(cond.getThen() = e2 or cond.getElse() = e2)
58+
cond.getCondition().getAChild*() = e1 and
59+
(cond.getThen().getAChild*() = e2 or cond.getElse().getAChild*() = e2)
6160
)
6261
or
6362
// Between the evaluation of a full expression and the next to be evaluated full expression.
@@ -68,6 +67,24 @@ module Ordering {
6867
// The side effect of updating the stored value of the left operand is sequenced after the value computations of the left and right operands.
6968
// See 6.5.16
7069
e2.(Assignment).getAnOperand().getAChild*() = e1
70+
or
71+
// There is a sequence point after a full declarator as described in 6.7.6 point 3.
72+
exists(DeclStmt declStmt, int i, int j | i < j |
73+
declStmt
74+
.getDeclarationEntry(i)
75+
.(VariableDeclarationEntry)
76+
.getVariable()
77+
.getInitializer()
78+
.getExpr()
79+
.getAChild*() = e1 and
80+
declStmt
81+
.getDeclarationEntry(j)
82+
.(VariableDeclarationEntry)
83+
.getVariable()
84+
.getInitializer()
85+
.getExpr()
86+
.getAChild*() = e2
87+
)
7188
)
7289
}
7390

‎c/common/src/codingstandards/c/SideEffects.qll

+1-1
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ private class VolatileAccess extends GlobalSideEffect::Range, VariableAccess {
2626
this.getTarget().isVolatile() and
2727
// Exclude value computation of an lvalue expression soley used to determine the identity
2828
// of the object. As noted in the footnote of 6.5.16 point 3 it is implementation dependend
29-
// whether the value of the assignment expression deterived from the left operand after the assignment
29+
// whether the value of the assignment expression derived from the left operand after the assignment
3030
// is determined by reading the object. We assume it is not for assignments that are a child of an
3131
// expression statement because the value is not used and is required for the compliant MISRA-C:2012 case:
3232
// `extern volatile int v; v = v & 0x80;`

‎c/common/test/library/expr/FullExpr.expected

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
| fullexpr.c:8:18:11:37 | temporary object |
1+
| fullexpr.c:8:18:11:37 | {...} |
22
| fullexpr.c:13:3:13:5 | ... ++ |
33
| fullexpr.c:15:7:15:7 | i |
44
| fullexpr.c:17:10:17:10 | i |

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

+249
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,249 @@
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+
class VariableEffectOrAccess extends Expr {
21+
VariableEffectOrAccess() {
22+
this instanceof VariableEffect or
23+
this instanceof VariableAccess
24+
}
25+
}
26+
27+
pragma[noinline]
28+
predicate partOfFullExpr(VariableEffectOrAccess e, FullExpr fe) {
29+
(
30+
exists(VariableEffect ve | e = ve and ve.getAnAccess() = fe.getAChild+() and not ve.isPartial())
31+
or
32+
e.(VariableAccess) = fe.getAChild+()
33+
)
34+
}
35+
36+
class ConstituentExprOrdering extends Ordering::Configuration {
37+
ConstituentExprOrdering() { this = "ConstituentExprOrdering" }
38+
39+
override predicate isCandidate(Expr e1, Expr e2) {
40+
exists(FullExpr fe |
41+
partOfFullExpr(e1, fe) and
42+
partOfFullExpr(e2, fe)
43+
)
44+
}
45+
}
46+
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+
)
60+
}
61+
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+
157+
predicate inConditionalThen(ConditionalExpr ce, Expr e) {
158+
e = ce.getThen()
159+
or
160+
exists(Expr parent |
161+
inConditionalThen(ce, parent) and
162+
parent.getAChild() = e
163+
)
164+
}
165+
166+
predicate inConditionalElse(ConditionalExpr ce, Expr e) {
167+
e = ce.getElse()
168+
or
169+
exists(Expr parent |
170+
inConditionalElse(ce, parent) and
171+
parent.getAChild() = e
172+
)
173+
}
174+
175+
predicate isUnsequencedEffect(
176+
ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1,
177+
VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label
178+
) {
179+
// The two access are scoped to the same full expression.
180+
sameFullExpr(fullExpr, va1, va2) and
181+
// We are only interested in effects that change an object,
182+
// 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`.
183+
not variableEffect1.isPartial() and
184+
variableEffect1.getAnAccess() = va1 and
185+
(
186+
exists(VariableEffect variableEffect2 |
187+
not variableEffect2.isPartial() and
188+
variableEffect2.getAnAccess() = va2 and
189+
// If the effect is not local (happens in a different function) we use the call with the access as a proxy.
190+
(
191+
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
192+
va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
193+
orderingConfig.isUnsequenced(variableEffect1, variableEffect2)
194+
or
195+
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
196+
not va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
197+
exists(Call call |
198+
call.getAnArgument() = va2 and call.getEnclosingStmt() = va1.getEnclosingStmt()
199+
|
200+
orderingConfig.isUnsequenced(variableEffect1, call)
201+
)
202+
or
203+
not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
204+
va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
205+
exists(Call call |
206+
call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt()
207+
|
208+
orderingConfig.isUnsequenced(call, variableEffect2)
209+
)
210+
) and
211+
// Break the symmetry of the ordering relation by requiring that the first expression is located before the second.
212+
// This builds upon the assumption that the expressions are part of the same full expression as specified in the ordering configuration.
213+
getOperandIndexIn(fullExpr, va1) < getOperandIndexIn(fullExpr, va2) and
214+
placeHolder = variableEffect2 and
215+
label = "side effect"
216+
)
217+
or
218+
placeHolder = va2 and
219+
label = "read" and
220+
not exists(VariableEffect variableEffect2 | variableEffect1 != variableEffect2 |
221+
variableEffect2.getAnAccess() = va2
222+
) and
223+
(
224+
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
225+
orderingConfig.isUnsequenced(variableEffect1, va2)
226+
or
227+
not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
228+
exists(Call call |
229+
call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt()
230+
|
231+
orderingConfig.isUnsequenced(call, va2)
232+
)
233+
) and
234+
// The read is not used to compute the effect on the variable.
235+
// E.g., exclude x = x + 1
236+
not variableEffect1.getAChild+() = va2
237+
) and
238+
// Both are evaluated
239+
not exists(ConditionalExpr ce | inConditionalThen(ce, va1) and inConditionalElse(ce, va2))
240+
}
241+
242+
from
243+
ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1,
244+
VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label
245+
where
246+
not isExcluded(fullExpr, SideEffects3Package::unsequencedSideEffectsQuery()) and
247+
isUnsequencedEffect(orderingConfig, fullExpr, variableEffect1, va1, va2, placeHolder, label)
248+
select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1,
249+
"side effect", va1, va1.getTarget().getName(), placeHolder, label, va2, va2.getTarget().getName()

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

+6
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 |

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

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
rules/RULE-13-2/UnsequencedSideEffects.ql

0 commit comments

Comments
 (0)