Skip to content

Commit ea2726c

Browse files
authored
Merge pull request #1049 from github/michaelrfairhurst/sideffects-4-package-4-6-1
Michaelrfairhurst/sideffects 4 package 4 6 1
2 parents 4e60680 + 6a48e22 commit ea2726c

File tree

29 files changed

+522
-244
lines changed

29 files changed

+522
-244
lines changed

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

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -21,15 +21,14 @@ import codingstandards.c.cert
2121
import codingstandards.cpp.SideEffect
2222
import codingstandards.c.Ordering
2323
import codingstandards.c.orderofevaluation.VariableAccessOrdering
24+
import Ordering::Make<VariableAccessInFullExpressionOrdering> as FullExpressionOrdering
2425

25-
from
26-
VariableAccessInFullExpressionOrdering config, FullExpr e, ScalarVariable v, VariableEffect ve,
27-
VariableAccess va1, VariableAccess va2
26+
from FullExpr e, ScalarVariable v, VariableEffect ve, VariableAccess va1, VariableAccess va2
2827
where
2928
not isExcluded(e, SideEffects1Package::dependenceOnOrderOfScalarEvaluationForSideEffectsQuery()) and
3029
e = va1.(ConstituentExpr).getFullExpr() and
3130
va1 = ve.getAnAccess() and
32-
config.isUnsequenced(va1, va2) and
31+
FullExpressionOrdering::isUnsequenced(va1, va2) and
3332
v = va1.getTarget()
3433
select e, "Scalar object referenced by $@ has a $@ that is unsequenced in relative to another $@.",
3534
v, v.getName(), ve, "side-effect", va2, "side-effect or value computation"
Lines changed: 73 additions & 86 deletions
Original file line numberDiff line numberDiff line change
@@ -1,97 +1,84 @@
11
import cpp
2-
import codingstandards.cpp.SideEffect
32
import codingstandards.c.Expr
43
import codingstandards.cpp.Variable
54

65
module Ordering {
7-
abstract class Configuration extends string {
8-
bindingset[this]
9-
Configuration() { any() }
6+
private import codingstandards.cpp.Ordering as CppCommonOrdering
7+
import CppCommonOrdering::OrderingBase
108

11-
abstract predicate isCandidate(Expr e1, Expr e2);
9+
module CConfigBase {
10+
class EvaluationNode = Expr;
1211

13-
/**
14-
* Holds if `e1` is sequenced before `e2` as defined by Annex C in ISO/IEC 9899:2011
15-
* This limits to expression and we do not consider the sequence points that are not amenable to modelling:
16-
* - before a library function returns (see 7.1.4 point 3).
17-
* - after the actions associated with each formatted I/O function conversion specifier (see 7.21.6 point 1 & 7.29.2 point 1).
18-
* - between the expr before and after a call to a comparison function,
19-
* between any call to a comparison function, and any movement of the objects passed
20-
* as arguments to that call (see 7.22.5 point 5).
21-
*/
22-
predicate isSequencedBefore(Expr e1, Expr e2) {
23-
isCandidate(e1, e2) and
24-
not e1 = e2 and
12+
pragma[inline]
13+
Expr toExpr(Expr e) { result = e }
14+
15+
pragma[inline]
16+
predicate sequencingEdge(Expr e1, Expr e2) { c11Ordering(e1, e2) }
17+
}
18+
19+
pragma[inline]
20+
predicate c11Ordering(Expr e1, Expr e2) {
21+
// 6.5.2.2 point 10 - The evaluation of the function designator and the actual arguments are sequenced
22+
// before the actual call.
23+
exists(Call call |
2524
(
26-
// 6.5.2.2 point 10 - The evaluation of the function designator and the actual arguments are sequenced
27-
// before the actual call.
28-
exists(Call call |
29-
(
30-
call.getAnArgument().getAChild*() = e1
31-
or
32-
// Postfix expression designating the called function
33-
// We current only handle call through function pointers because the postfix expression
34-
// of regular function calls is not available. That is, identifying `f` in `f(...)`
35-
call.(ExprCall).getExpr().getAChild*() = e1
36-
) and
37-
call.getTarget() = e2.getEnclosingFunction()
38-
)
39-
or
40-
// 6.5.13 point 4 & 6.5.14 point 4 - The operators guarantee left-to-right evaluation and there is
41-
// a sequence point between the first and second operand if the latter is evaluated.
42-
exists(BinaryLogicalOperation blop |
43-
blop instanceof LogicalAndExpr or blop instanceof LogicalOrExpr
44-
|
45-
blop.getLeftOperand().getAChild*() = e1 and blop.getRightOperand().getAChild*() = e2
46-
)
47-
or
48-
// 6.5.17 point 2 - There is a sequence point between the left operand and the right operand.
49-
exists(CommaExpr ce, Expr lhs, Expr rhs |
50-
lhs = ce.getLeftOperand() and
51-
rhs = ce.getRightOperand()
52-
|
53-
lhs.getAChild*() = e1 and rhs.getAChild*() = e2
54-
)
25+
call.getAnArgument().getAChild*() = e1
5526
or
56-
// 6.5.15 point 4 - There is a sequence point between the first operand and the evaluation of the second or third.
57-
exists(ConditionalExpr cond |
58-
cond.getCondition().getAChild*() = e1 and
59-
(cond.getThen().getAChild*() = e2 or cond.getElse().getAChild*() = e2)
60-
)
61-
or
62-
// Between the evaluation of a full expression and the next to be evaluated full expression.
63-
// Note we don't strictly check if `e2` is the next to be evaluated full expression and rely on the
64-
// `isCandidate` configuration to minimze the scope or related full expressions.
65-
e1 instanceof FullExpr and e2 instanceof FullExpr
66-
or
67-
// The side effect of updating the stored value of the left operand is sequenced after the value computations of the left and right operands.
68-
// See 6.5.16
69-
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-
)
88-
)
89-
}
90-
91-
predicate isUnsequenced(Expr e1, Expr e2) {
92-
isCandidate(e1, e2) and
93-
not isSequencedBefore(e1, e2) and
94-
not isSequencedBefore(e2, e1)
95-
}
27+
// Postfix expression designating the called function
28+
// We current only handle call through function pointers because the postfix expression
29+
// of regular function calls is not available. That is, identifying `f` in `f(...)`
30+
call.(ExprCall).getExpr().getAChild*() = e1
31+
) and
32+
call.getTarget() = e2.getEnclosingFunction()
33+
)
34+
or
35+
// 6.5.13 point 4 & 6.5.14 point 4 - The operators guarantee left-to-right evaluation and there is
36+
// a sequence point between the first and second operand if the latter is evaluated.
37+
exists(BinaryLogicalOperation blop |
38+
blop instanceof LogicalAndExpr or blop instanceof LogicalOrExpr
39+
|
40+
blop.getLeftOperand().getAChild*() = e1 and blop.getRightOperand().getAChild*() = e2
41+
)
42+
or
43+
// 6.5.17 point 2 - There is a sequence point between the left operand and the right operand.
44+
exists(CommaExpr ce, Expr lhs, Expr rhs |
45+
lhs = ce.getLeftOperand() and
46+
rhs = ce.getRightOperand()
47+
|
48+
lhs.getAChild*() = e1 and rhs.getAChild*() = e2
49+
)
50+
or
51+
// 6.5.15 point 4 - There is a sequence point between the first operand and the evaluation of the second or third.
52+
exists(ConditionalExpr cond |
53+
cond.getCondition().getAChild*() = e1 and
54+
(cond.getThen().getAChild*() = e2 or cond.getElse().getAChild*() = e2)
55+
)
56+
or
57+
// Between the evaluation of a full expression and the next to be evaluated full expression.
58+
// Note we don't strictly check if `e2` is the next to be evaluated full expression and rely on the
59+
// `isCandidate` configuration to minimze the scope or related full expressions.
60+
e1 instanceof FullExpr and e2 instanceof FullExpr
61+
or
62+
// The side effect of updating the stored value of the left operand is sequenced after the value computations of the left and right operands.
63+
// See 6.5.16
64+
e2.(Assignment).getAnOperand().getAChild*() = e1
65+
or
66+
// There is a sequence point after a full declarator as described in 6.7.6 point 3.
67+
exists(DeclStmt declStmt, int i, int j | i < j |
68+
declStmt
69+
.getDeclarationEntry(i)
70+
.(VariableDeclarationEntry)
71+
.getVariable()
72+
.getInitializer()
73+
.getExpr()
74+
.getAChild*() = e1 and
75+
declStmt
76+
.getDeclarationEntry(j)
77+
.(VariableDeclarationEntry)
78+
.getVariable()
79+
.getInitializer()
80+
.getExpr()
81+
.getAChild*() = e2
82+
)
9683
}
9784
}

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

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
11
import cpp
22
import codingstandards.c.Ordering
3+
import codingstandards.c.SideEffects
34

4-
class VariableAccessInFullExpressionOrdering extends Ordering::Configuration {
5-
VariableAccessInFullExpressionOrdering() { this = "VariableAccessInFullExpressionOrdering" }
5+
module VariableAccessInFullExpressionOrdering implements Ordering::ConfigSig {
6+
import Ordering::CConfigBase
67

7-
override predicate isCandidate(Expr e1, Expr e2) { isCandidate(_, e1, e2) }
8+
predicate isCandidate(Expr e1, Expr e2) { isCandidate(_, e1, e2) }
89
}
910

1011
pragma[noinline]

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

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -19,10 +19,10 @@ import codingstandards.c.Ordering
1919
import codingstandards.c.orderofevaluation.VariableAccessOrdering
2020
import codingstandards.cpp.StdFunctionOrMacro
2121

22-
class AtomicAccessInFullExpressionOrdering extends Ordering::Configuration {
23-
AtomicAccessInFullExpressionOrdering() { this = "AtomicAccessInFullExpressionOrdering" }
22+
module AtomicAccessInFullExpressionOrdering implements Ordering::ConfigSig {
23+
import Ordering::CConfigBase
2424

25-
override predicate isCandidate(Expr e1, Expr e2) {
25+
predicate isCandidate(Expr e1, Expr e2) {
2626
exists(AtomicVariableAccess a, AtomicVariableAccess b, FullExpr e | a = e1 and b = e2 |
2727
a.getTarget() = b.getTarget() and
2828
a.getARead().(ConstituentExpr).getFullExpr() = e and
@@ -91,9 +91,11 @@ class AtomicVariableAccess extends VariableAccess {
9191
}
9292
}
9393

94+
import Ordering::Make<AtomicAccessInFullExpressionOrdering> as AtomicOrdering
95+
9496
from
95-
AtomicAccessInFullExpressionOrdering config, FullExpr e, Variable v, AtomicVariableAccess va1,
96-
AtomicVariableAccess va2, Expr va1Read, Expr va2Read
97+
FullExpr e, Variable v, AtomicVariableAccess va1, AtomicVariableAccess va2, Expr va1Read,
98+
Expr va2Read
9799
where
98100
not isExcluded(e, SideEffects3Package::unsequencedAtomicReadsQuery()) and
99101
va1Read = va1.getARead() and
@@ -103,7 +105,7 @@ where
103105
// for instance in gcc where atomic functions expand to StmtExprs, which have clear sequences.
104106
// In this case, the result of `getARead()` for a pair of atomic function calls may be
105107
// unsequenced even though the `VariableAccess`es within those calls are not.
106-
config.isUnsequenced(va1Read, va2Read) and
108+
AtomicOrdering::isUnsequenced(va1Read, va2Read) and
107109
v = va1.getTarget() and
108110
v = va2.getTarget() and
109111
// Exclude cases where the variable is assigned a value tainted by the other variable access.

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

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -33,10 +33,10 @@ predicate partOfFullExpr(VariableEffectOrAccess e, FullExpr fe) {
3333
)
3434
}
3535

36-
class ConstituentExprOrdering extends Ordering::Configuration {
37-
ConstituentExprOrdering() { this = "ConstituentExprOrdering" }
36+
module ConstituentExprOrderingConfig implements Ordering::ConfigSig {
37+
import Ordering::CConfigBase
3838

39-
override predicate isCandidate(Expr e1, Expr e2) {
39+
predicate isCandidate(Expr e1, Expr e2) {
4040
exists(FullExpr fe |
4141
partOfFullExpr(e1, fe) and
4242
partOfFullExpr(e2, fe)
@@ -172,9 +172,11 @@ predicate inConditionalElse(ConditionalExpr ce, Expr e) {
172172
)
173173
}
174174

175+
import Ordering::Make<ConstituentExprOrderingConfig> as ConstituentExprOrdering
176+
175177
predicate isUnsequencedEffect(
176-
ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1,
177-
VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label
178+
FullExpr fullExpr, VariableEffect variableEffect1, VariableAccess va1, VariableAccess va2,
179+
Locatable placeHolder, string label
178180
) {
179181
// The two access are scoped to the same full expression.
180182
sameFullExpr(fullExpr, va1, va2) and
@@ -190,22 +192,22 @@ predicate isUnsequencedEffect(
190192
(
191193
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
192194
va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
193-
orderingConfig.isUnsequenced(variableEffect1, variableEffect2)
195+
ConstituentExprOrdering::isUnsequenced(variableEffect1, variableEffect2)
194196
or
195197
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
196198
not va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
197199
exists(Call call |
198200
call.getAnArgument() = va2 and call.getEnclosingStmt() = va1.getEnclosingStmt()
199201
|
200-
orderingConfig.isUnsequenced(variableEffect1, call)
202+
ConstituentExprOrdering::isUnsequenced(variableEffect1, call)
201203
)
202204
or
203205
not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
204206
va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
205207
exists(Call call |
206208
call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt()
207209
|
208-
orderingConfig.isUnsequenced(call, variableEffect2)
210+
ConstituentExprOrdering::isUnsequenced(call, variableEffect2)
209211
)
210212
) and
211213
// Break the symmetry of the ordering relation by requiring that the first expression is located before the second.
@@ -222,13 +224,13 @@ predicate isUnsequencedEffect(
222224
) and
223225
(
224226
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
225-
orderingConfig.isUnsequenced(variableEffect1, va2)
227+
ConstituentExprOrdering::isUnsequenced(variableEffect1, va2)
226228
or
227229
not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
228230
exists(Call call |
229231
call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt()
230232
|
231-
orderingConfig.isUnsequenced(call, va2)
233+
ConstituentExprOrdering::isUnsequenced(call, va2)
232234
)
233235
) and
234236
// The read is not used to compute the effect on the variable.
@@ -240,10 +242,10 @@ predicate isUnsequencedEffect(
240242
}
241243

242244
from
243-
ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1,
244-
VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label
245+
FullExpr fullExpr, VariableEffect variableEffect1, VariableAccess va1, VariableAccess va2,
246+
Locatable placeHolder, string label
245247
where
246248
not isExcluded(fullExpr, SideEffects3Package::unsequencedSideEffectsQuery()) and
247-
isUnsequencedEffect(orderingConfig, fullExpr, variableEffect1, va1, va2, placeHolder, label)
249+
isUnsequencedEffect(fullExpr, variableEffect1, va1, va2, placeHolder, label)
248250
select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1,
249251
"side effect", va1, va1.getTarget().getName(), placeHolder, label, va2, va2.getTarget().getName()
Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:112,31-39)
2-
WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:112,67-75)
3-
WARNING: module 'TaintTracking' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:112,5-18)
1+
WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:114,31-39)
2+
WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:114,67-75)
3+
WARNING: module 'TaintTracking' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:114,5-18)
44
| test.c:44:12:44:18 | ... + ... | Atomic variable $@ has a $@ that is unsequenced with $@. | test.c:42:15:42:16 | a1 | a1 | test.c:44:12:44:13 | a1 | previous read | test.c:44:17:44:18 | a1 | another read |
55
| test.c:46:3:46:37 | ... + ... | Atomic variable $@ has a $@ that is unsequenced with $@. | test.c:42:15:42:16 | a1 | a1 | test.c:46:16:46:17 | a1 | previous read | test.c:46:35:46:36 | a1 | another read |
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
- `A5-0-1`, `EXP50-CPP` - `ExpressionShouldNotRelyONOrderOfEvaluation.ql`, `DoNotDependOnTheOrderOfScalarObjectEvaluationForSideEffects.ql`:
2+
- Fixed a bug where some sequenced operations were not detected as such due to an error in the "candidate selection" process. This could have complex effects on results, but should mostly fix false positives. Some unsequenced operations that previously reported one alert may now report two, due to the extra candidates being considered.
3+
- Sequencing between full expressions no longer requires that the expressions are sequential; expressions in separate if statements, for instance, are not necessarily sequential, but they are still ordered. It is unclear if this change will have any effect on results, but it should be more accurate to the standard.
4+
- `RULE-13-2`, `A5-0-1`, `EXP50-CPP`, `EXP30-C` - `UnsequencedSideEffects.ql`, `UnsequencedAtomicReads.ql`, `ExpressionShouldNotRelyONOrderOfEvaluation.ql`, `DoNotDependOnTheOrderOfScalarObjectEvaluationForSideEffects.ql`, `DependenceOnOrderOfScalarEvaluationForSideEffects.ql`:
5+
- Implementation of ordering has been refactored to share more code across specifications (C11-C17, C++14, and C++17 sequencing rules). No change in results is expected from this refactor.

cpp/autosar/src/rules/A5-0-1/ExpressionShouldNotRelyOnOrderOfEvaluation.ql

Lines changed: 15 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -15,20 +15,21 @@
1515

1616
import cpp
1717
import codingstandards.cpp.autosar
18-
import codingstandards.cpp.SideEffect
19-
import codingstandards.cpp.sideeffect.DefaultEffects
18+
import codingstandards.cpp.rules.expressionwithunsequencedsideeffects.ExpressionWithUnsequencedSideEffects
2019
import codingstandards.cpp.Ordering
2120
import codingstandards.cpp.orderofevaluation.VariableAccessOrdering
21+
import Ordering::Make<Cpp14VariableAccessInFullExpressionOrdering> as FullExprOrdering
2222

23-
from
24-
VariableAccessInFullExpressionOrdering config, FullExpr e, VariableEffect ve, VariableAccess va1,
25-
VariableAccess va2, Variable v
26-
where
27-
not isExcluded(e, OrderOfEvaluationPackage::expressionShouldNotRelyOnOrderOfEvaluationQuery()) and
28-
e = va1.(ConstituentExpr).getFullExpr() and
29-
va1 = ve.getAnAccess() and
30-
config.isUnsequenced(va1, va2) and
31-
v = va1.getTarget()
32-
select e,
33-
"The evaluation is depended on the order of evaluation of $@, that is modified by $@ and $@, that both access $@.",
34-
va1, "sub-expression", ve, "expression", va2, "sub-expression", v, v.getName()
23+
module ExpressionShouldNotRelyOnOrderOfEvaluationConfig implements
24+
ExpressionWithUnsequencedSideEffectsConfigSig
25+
{
26+
Query getQuery() {
27+
result = OrderOfEvaluationPackage::expressionShouldNotRelyOnOrderOfEvaluationQuery()
28+
}
29+
30+
predicate isUnsequenced(VariableAccess va1, VariableAccess va2) {
31+
FullExprOrdering::isUnsequenced(va1, va2)
32+
}
33+
}
34+
35+
import ExpressionWithUnsequencedSideEffects<ExpressionShouldNotRelyOnOrderOfEvaluationConfig>

0 commit comments

Comments
 (0)