|
1 | 1 | import cpp |
2 | | -import codingstandards.cpp.SideEffect |
3 | 2 | import codingstandards.c.Expr |
4 | 3 | import codingstandards.cpp.Variable |
5 | 4 |
|
6 | 5 | 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 |
10 | 8 |
|
11 | | - abstract predicate isCandidate(Expr e1, Expr e2); |
| 9 | + module CConfigBase { |
| 10 | + class EvaluationNode = Expr; |
12 | 11 |
|
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 | |
25 | 24 | ( |
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 |
55 | 26 | 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 | + ) |
96 | 83 | } |
97 | 84 | } |
0 commit comments