Skip to content

Commit fcf1b6d

Browse files
hvitvedhvitved
authored
Merge pull request #17657 from hvitved/rust/cfg-conditional-splitting
Rust: Implement `ConditionalCompletionSplitting`
2 parents 4ab9255 + cb1ca4c commit fcf1b6d

File tree

5 files changed

+226
-127
lines changed

5 files changed

+226
-127
lines changed

‎rust/ql/consistency-queries/CfgConsistency.ql

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,6 @@ query predicate nonPostOrderExpr(Expr e, string cls) {
1212
cls = e.getPrimaryQlClasses() and
1313
not e instanceof LetExpr and
1414
not e instanceof ParenExpr and
15-
not e instanceof LogicalAndExpr and // todo
16-
not e instanceof LogicalOrExpr and
1715
exists(AstNode last, Completion c |
1816
CfgImpl::last(e, last, c) and
1917
last != e and

‎rust/ql/lib/codeql/rust/controlflow/internal/Completion.qll

Lines changed: 11 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -62,11 +62,9 @@ abstract class ConditionalCompletion extends NormalCompletion {
6262
abstract ConditionalCompletion getDual();
6363
}
6464

65-
/** Holds if node `n` has the Boolean constant value `value`. */
66-
private predicate isBooleanConstant(AstNode n, Boolean value) {
67-
n.(LiteralExpr).getTextValue() = value.toString()
68-
or
69-
isBooleanConstant(n.(ParenExpr).getExpr(), value)
65+
/** Holds if node `le` has the Boolean constant value `value`. */
66+
private predicate isBooleanConstant(LiteralExpr le, Boolean value) {
67+
le.getTextValue() = value.toString()
7068
}
7169

7270
/**
@@ -83,29 +81,22 @@ class BooleanCompletion extends ConditionalCompletion, TBooleanCompletion {
8381
or
8482
any(MatchGuard guard).getCondition() = e
8583
or
86-
exists(BinaryExpr expr |
87-
expr.getOperatorName() = ["&&", "||"] and
88-
e = expr.getLhs()
89-
)
84+
e = any(BinaryLogicalOperation blo).getLhs()
9085
or
9186
exists(Expr parent | this.isValidForSpecific0(parent) |
9287
e = parent.(ParenExpr).getExpr()
9388
or
94-
parent =
95-
any(PrefixExpr expr |
96-
expr.getOperatorName() = "!" and
97-
e = expr.getExpr()
98-
)
89+
e = parent.(LogicalNotExpr).getExpr()
9990
or
100-
parent =
101-
any(BinaryExpr expr |
102-
expr.getOperatorName() = ["&&", "||"] and
103-
e = expr.getRhs()
104-
)
91+
e = parent.(BinaryLogicalOperation).getRhs()
10592
or
10693
parent = any(IfExpr ie | e = [ie.getThen(), ie.getElse()])
10794
or
108-
parent = any(BlockExpr be | e = be.getStmtList().getTailExpr())
95+
e = parent.(MatchExpr).getAnArm().getExpr()
96+
or
97+
e = parent.(BlockExpr).getStmtList().getTailExpr()
98+
or
99+
e = any(BreakExpr be | be.getTarget() = parent).getExpr()
109100
)
110101
}
111102

‎rust/ql/lib/codeql/rust/controlflow/internal/ControlFlowGraphImpl.qll

Lines changed: 28 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -44,9 +44,6 @@ private module CfgInput implements InputSig<Location> {
4444
/** Hold if `t` represents a conditional successor type. */
4545
predicate successorTypeIsCondition(SuccessorType t) { t instanceof Cfg::BooleanSuccessor }
4646

47-
/** Gets the maximum number of splits allowed for a given node. */
48-
int maxSplits() { result = 0 }
49-
5047
/** Holds if `first` is first executed when entering `scope`. */
5148
predicate scopeFirst(CfgScope scope, AstNode first) { scope.scopeFirst(first) }
5249

@@ -86,53 +83,49 @@ class BinaryOpExprTree extends StandardPostOrderTree instanceof BinaryExpr {
8683
}
8784
}
8885

89-
class LogicalOrBinaryOpExprTree extends PreOrderTree, LogicalOrExpr {
86+
class LogicalOrTree extends PostOrderTree, LogicalOrExpr {
9087
final override predicate propagatesAbnormal(AstNode child) { child = this.getAnOperand() }
9188

89+
override predicate first(AstNode node) { first(this.getLhs(), node) }
90+
9291
override predicate succ(AstNode pred, AstNode succ, Completion c) {
93-
// Edge to the first node in the lhs
94-
pred = this and
95-
first(this.getLhs(), succ) and
96-
completionIsSimple(c)
92+
// Edge from lhs to rhs
93+
last(this.getLhs(), pred, c) and
94+
c.(BooleanCompletion).failed() and
95+
first(this.getRhs(), succ)
9796
or
98-
// Edge from the last node in the lhs to the first node in the rhs
97+
// Edge from lhs to this
9998
last(this.getLhs(), pred, c) and
100-
first(this.getRhs(), succ) and
101-
c.(BooleanCompletion).failed()
102-
}
103-
104-
override predicate last(AstNode node, Completion c) {
105-
// Lhs. as the last node
106-
last(this.getLhs(), node, c) and
107-
c.(BooleanCompletion).succeeded()
99+
c.(BooleanCompletion).succeeded() and
100+
succ = this
108101
or
109-
// Rhs. as the last node
110-
last(this.getRhs(), node, c)
102+
// Edge from rhs to this
103+
last(this.getRhs(), pred, c) and
104+
succ = this and
105+
completionIsNormal(c)
111106
}
112107
}
113108

114-
class LogicalAndBinaryOpExprTree extends PreOrderTree, LogicalAndExpr {
109+
class LogicalAndTree extends PostOrderTree, LogicalAndExpr {
115110
final override predicate propagatesAbnormal(AstNode child) { child = this.getAnOperand() }
116111

112+
override predicate first(AstNode node) { first(this.getLhs(), node) }
113+
117114
override predicate succ(AstNode pred, AstNode succ, Completion c) {
118-
// Edge to the first node in the lhs
119-
pred = this and
120-
first(this.getLhs(), succ) and
121-
completionIsSimple(c)
115+
// Edge from lhs to rhs
116+
last(this.getLhs(), pred, c) and
117+
c.(BooleanCompletion).succeeded() and
118+
first(this.getRhs(), succ)
122119
or
123-
// Edge from the last node in the lhs to the first node in the rhs
120+
// Edge from lhs to this
124121
last(this.getLhs(), pred, c) and
125-
first(this.getRhs(), succ) and
126-
c.(BooleanCompletion).succeeded()
127-
}
128-
129-
override predicate last(AstNode node, Completion c) {
130-
// Lhs. as the last node
131-
last(this.getLhs(), node, c) and
132-
c.(BooleanCompletion).failed()
122+
c.(BooleanCompletion).failed() and
123+
succ = this
133124
or
134-
// Rhs. as the last node
135-
last(this.getRhs(), node, c)
125+
// Edge from rhs to this
126+
last(this.getRhs(), pred, c) and
127+
succ = this and
128+
completionIsNormal(c)
136129
}
137130
}
138131

‎rust/ql/lib/codeql/rust/controlflow/internal/Splitting.qll

Lines changed: 103 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,115 @@
1+
private import rust
2+
private import ControlFlowGraphImpl
3+
private import Scope
4+
15
cached
26
private module Cached {
3-
// Not using CFG splitting, so the following are just placeholder types.
47
cached
5-
newtype TSplitKind = TSplitKindUnit()
8+
newtype TSplitKind = TConditionalCompletionSplitKind()
69

710
cached
8-
newtype TSplit = TSplitUnit()
11+
newtype TSplit = TConditionalCompletionSplit(ConditionalCompletion c)
912
}
1013

1114
import Cached
1215

1316
/** A split for a control flow node. */
14-
class Split extends TSplit {
17+
abstract private class Split_ extends TSplit {
1518
/** Gets a textual representation of this split. */
16-
string toString() { none() }
19+
abstract string toString();
20+
}
21+
22+
final class Split = Split_;
23+
24+
private module ConditionalCompletionSplitting {
25+
/**
26+
* A split for conditional completions. For example, in
27+
*
28+
* ```rust
29+
* if x && !y {
30+
* // ...
31+
* }
32+
* ```
33+
*
34+
* we record whether `x`, `y`, and `!y` evaluate to `true` or `false`, and restrict
35+
* the edges out of `!y` and `x && !y` accordingly.
36+
*/
37+
class ConditionalCompletionSplit extends Split_, TConditionalCompletionSplit {
38+
ConditionalCompletion completion;
39+
40+
ConditionalCompletionSplit() { this = TConditionalCompletionSplit(completion) }
41+
42+
override string toString() { result = completion.toString() }
43+
}
44+
45+
private class ConditionalCompletionSplitKind extends SplitKind, TConditionalCompletionSplitKind {
46+
override int getListOrder() { result = 0 }
47+
48+
override predicate isEnabled(AstNode cfe) { this.appliesTo(cfe) }
49+
50+
override string toString() { result = "ConditionalCompletion" }
51+
}
52+
53+
private class ConditionalCompletionSplitImpl extends SplitImpl instanceof ConditionalCompletionSplit
54+
{
55+
ConditionalCompletion completion;
56+
57+
ConditionalCompletionSplitImpl() { this = TConditionalCompletionSplit(completion) }
58+
59+
override ConditionalCompletionSplitKind getKind() { any() }
60+
61+
override predicate hasEntry(AstNode pred, AstNode succ, Completion c) {
62+
succ(pred, succ, c) and
63+
last(succ, _, completion) and
64+
(
65+
last(succ.(LogicalNotExpr).getExpr(), pred, c) and
66+
completion.(BooleanCompletion).getDual() = c
67+
or
68+
last(succ.(BinaryLogicalOperation).getAnOperand(), pred, c) and
69+
completion = c
70+
or
71+
succ =
72+
any(IfExpr ie |
73+
last([ie.getThen(), ie.getElse()], pred, c) and
74+
completion = c
75+
)
76+
or
77+
last(succ.(MatchExpr).getAnArm().getExpr(), pred, c) and
78+
completion = c
79+
or
80+
last(succ.(BlockExpr).getStmtList().getTailExpr(), pred, c) and
81+
completion = c
82+
)
83+
or
84+
succ(pred, succ, c) and
85+
last(succ.(BreakExpr).getExpr(), pred, c) and
86+
exists(AstNode target |
87+
succ(succ, target, _) and
88+
last(target, _, completion)
89+
) and
90+
completion = c
91+
}
92+
93+
override predicate hasEntryScope(CfgScope scope, AstNode first) { none() }
94+
95+
override predicate hasExit(AstNode pred, AstNode succ, Completion c) {
96+
this.appliesTo(pred) and
97+
succ(pred, succ, c) and
98+
if c instanceof ConditionalCompletion
99+
then completion = c
100+
else not this.hasSuccessor(pred, succ, c)
101+
}
102+
103+
override predicate hasExitScope(CfgScope scope, AstNode last, Completion c) {
104+
this.appliesTo(last) and
105+
scope.scopeLast(last, c) and
106+
if c instanceof ConditionalCompletion then completion = c else any()
107+
}
108+
109+
override predicate hasSuccessor(AstNode pred, AstNode succ, Completion c) {
110+
this.appliesTo(pred) and
111+
succ(pred, succ, c) and
112+
not c instanceof ConditionalCompletion
113+
}
114+
}
17115
}

0 commit comments

Comments
 (0)