Skip to content

Commit 8233e34

Browse files
hvitvedhvitved
committed
C#: Fix Boolean splitting for variables defined in a loop
1 parent 89d5daa commit 8233e34

File tree

8 files changed

+71
-222
lines changed

8 files changed

+71
-222
lines changed

‎csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll‎

Lines changed: 19 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -3476,6 +3476,12 @@ module ControlFlow {
34763476
this.correlatesConditions(any(ConditionBlock cb | cb.getLastElement() = cfe), _, _)
34773477
}
34783478

3479+
/**
3480+
* Holds if basic block `bb` can reach a condition correlated with a
3481+
* split of this kind.
3482+
*/
3483+
abstract predicate canReachCorrelatedCondition(PreBasicBlock bb);
3484+
34793485
/** Gets the callable that this Boolean split kind belongs to. */
34803486
abstract Callable getEnclosingCallable();
34813487

@@ -3553,6 +3559,17 @@ module ControlFlow {
35533559
)
35543560
}
35553561

3562+
override predicate canReachCorrelatedCondition(PreBasicBlock bb) {
3563+
this.correlatesConditions(_, bb, _) and
3564+
not def.getBasicBlock() = bb
3565+
or
3566+
exists(PreBasicBlock mid |
3567+
this.canReachCorrelatedCondition(mid) |
3568+
bb = mid.getAPredecessor() and
3569+
not def.getBasicBlock() = bb
3570+
)
3571+
}
3572+
35563573
override Callable getEnclosingCallable() {
35573574
result = def.getCallable()
35583575
}
@@ -3662,26 +3679,13 @@ module ControlFlow {
36623679
)
36633680
}
36643681

3665-
/**
3666-
* Holds if basic block `bb` can reach a condition correlated with the value
3667-
* recorded in this split.
3668-
*/
3669-
private predicate canReachCorrelatedCondition(PreBasicBlock bb) {
3670-
bb = this.getACorrelatedCondition(_)
3671-
or
3672-
exists(PreBasicBlock mid |
3673-
this.canReachCorrelatedCondition(mid) |
3674-
bb = mid.getAPredecessor()
3675-
)
3676-
}
3677-
36783682
override predicate hasExit(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
36793683
exists(PreBasicBlock bb |
36803684
this.appliesToBlock(bb, c) |
36813685
pred = bb.getLastElement() and
36823686
succ = succ(pred, c) and
36833687
// Exit this split if we can no longer reach a correlated condition
3684-
not this.canReachCorrelatedCondition(succ)
3688+
not this.getSubKind().canReachCorrelatedCondition(succ)
36853689
)
36863690
}
36873691

@@ -3702,7 +3706,7 @@ module ControlFlow {
37023706
pred = bb.getLastElement()
37033707
implies
37043708
// We must still be able to reach a correlated condition to stay in this split
3705-
this.canReachCorrelatedCondition(succ) and
3709+
this.getSubKind().canReachCorrelatedCondition(succ) and
37063710
c = c0
37073711
)
37083712
)

‎csharp/ql/test/library-tests/controlflow/graph/BasicBlock.expected‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -164,13 +164,13 @@
164164
| Conditions.cs:108:13:109:24 | [b (line 102): false] if (...) ... | Conditions.cs:109:17:109:23 | ... = ... | 9 |
165165
| Conditions.cs:108:13:109:24 | [b (line 102): true] if (...) ... | Conditions.cs:108:18:108:18 | [b (line 102): true] access to parameter b | 3 |
166166
| Conditions.cs:110:16:110:16 | access to local variable x | Conditions.cs:102:12:102:13 | exit M8 | 3 |
167-
| Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:116:24:116:38 | ... < ... | 14 |
167+
| Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:116:17:116:21 | Int32 i = ... | 10 |
168168
| Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:113:10:113:11 | exit M9 | 1 |
169-
| Conditions.cs:117:9:123:9 | [last (line 118): false] {...} | Conditions.cs:119:18:119:21 | [last (line 118): false] access to local variable last | 13 |
170-
| Conditions.cs:117:9:123:9 | [last (line 118): true] {...} | Conditions.cs:119:18:119:21 | [last (line 118): true] access to local variable last | 13 |
169+
| Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:116:24:116:38 | ... < ... | 4 |
170+
| Conditions.cs:116:41:116:41 | access to local variable i | Conditions.cs:116:41:116:43 | ...++ | 2 |
171171
| Conditions.cs:117:9:123:9 | {...} | Conditions.cs:119:18:119:21 | access to local variable last | 13 |
172-
| Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | Conditions.cs:116:24:116:38 | [last (line 118): false] ... < ... | 12 |
173-
| Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | Conditions.cs:116:24:116:38 | [last (line 118): true] ... < ... | 12 |
172+
| Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | Conditions.cs:121:17:121:20 | [last (line 118): false] access to local variable last | 6 |
173+
| Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | Conditions.cs:122:17:122:24 | ... = ... | 6 |
174174
| ExitMethods.cs:7:10:7:11 | enter M1 | ExitMethods.cs:7:10:7:11 | exit M1 | 7 |
175175
| ExitMethods.cs:13:10:13:11 | enter M2 | ExitMethods.cs:13:10:13:11 | exit M2 | 7 |
176176
| ExitMethods.cs:19:10:19:11 | enter M3 | ExitMethods.cs:19:10:19:11 | exit M3 | 6 |

‎csharp/ql/test/library-tests/controlflow/graph/BasicBlockDominance.expected‎

Lines changed: 22 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -363,17 +363,23 @@
363363
| post | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:113:10:113:11 | enter M9 |
364364
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:113:10:113:11 | enter M9 |
365365
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:113:10:113:11 | exit M9 |
366-
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:117:9:123:9 | [last (line 118): false] {...} |
367-
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:117:9:123:9 | [last (line 118): true] {...} |
366+
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:116:24:116:24 | access to local variable i |
367+
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:116:41:116:41 | access to local variable i |
368368
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:117:9:123:9 | {...} |
369369
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
370370
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
371-
| post | Conditions.cs:117:9:123:9 | [last (line 118): false] {...} | Conditions.cs:117:9:123:9 | [last (line 118): false] {...} |
372-
| post | Conditions.cs:117:9:123:9 | [last (line 118): true] {...} | Conditions.cs:117:9:123:9 | [last (line 118): true] {...} |
371+
| post | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:113:10:113:11 | enter M9 |
372+
| post | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:116:24:116:24 | access to local variable i |
373+
| post | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:116:41:116:41 | access to local variable i |
374+
| post | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:117:9:123:9 | {...} |
375+
| post | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
376+
| post | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
377+
| post | Conditions.cs:116:41:116:41 | access to local variable i | Conditions.cs:116:41:116:41 | access to local variable i |
378+
| post | Conditions.cs:116:41:116:41 | access to local variable i | Conditions.cs:117:9:123:9 | {...} |
379+
| post | Conditions.cs:116:41:116:41 | access to local variable i | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
380+
| post | Conditions.cs:116:41:116:41 | access to local variable i | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
373381
| post | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:117:9:123:9 | {...} |
374-
| post | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | Conditions.cs:117:9:123:9 | [last (line 118): false] {...} |
375382
| post | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
376-
| post | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | Conditions.cs:117:9:123:9 | [last (line 118): true] {...} |
377383
| post | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
378384
| post | ExitMethods.cs:7:10:7:11 | enter M1 | ExitMethods.cs:7:10:7:11 | enter M1 |
379385
| post | ExitMethods.cs:13:10:13:11 | enter M2 | ExitMethods.cs:13:10:13:11 | enter M2 |
@@ -1722,22 +1728,24 @@
17221728
| pre | Conditions.cs:110:16:110:16 | access to local variable x | Conditions.cs:110:16:110:16 | access to local variable x |
17231729
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:113:10:113:11 | enter M9 |
17241730
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:113:10:113:11 | exit M9 |
1725-
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:117:9:123:9 | [last (line 118): false] {...} |
1726-
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:117:9:123:9 | [last (line 118): true] {...} |
1731+
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:116:24:116:24 | access to local variable i |
1732+
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:116:41:116:41 | access to local variable i |
17271733
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:117:9:123:9 | {...} |
17281734
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
17291735
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
17301736
| pre | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:113:10:113:11 | exit M9 |
1731-
| pre | Conditions.cs:117:9:123:9 | [last (line 118): false] {...} | Conditions.cs:117:9:123:9 | [last (line 118): false] {...} |
1732-
| pre | Conditions.cs:117:9:123:9 | [last (line 118): true] {...} | Conditions.cs:117:9:123:9 | [last (line 118): true] {...} |
1733-
| pre | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:117:9:123:9 | [last (line 118): false] {...} |
1734-
| pre | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:117:9:123:9 | [last (line 118): true] {...} |
1737+
| pre | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:113:10:113:11 | exit M9 |
1738+
| pre | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:116:24:116:24 | access to local variable i |
1739+
| pre | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:116:41:116:41 | access to local variable i |
1740+
| pre | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:117:9:123:9 | {...} |
1741+
| pre | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
1742+
| pre | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
1743+
| pre | Conditions.cs:116:41:116:41 | access to local variable i | Conditions.cs:116:41:116:41 | access to local variable i |
1744+
| pre | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:116:41:116:41 | access to local variable i |
17351745
| pre | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:117:9:123:9 | {...} |
17361746
| pre | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
17371747
| pre | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
1738-
| pre | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | Conditions.cs:117:9:123:9 | [last (line 118): false] {...} |
17391748
| pre | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
1740-
| pre | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | Conditions.cs:117:9:123:9 | [last (line 118): true] {...} |
17411749
| pre | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
17421750
| pre | ExitMethods.cs:7:10:7:11 | enter M1 | ExitMethods.cs:7:10:7:11 | enter M1 |
17431751
| pre | ExitMethods.cs:13:10:13:11 | enter M2 | ExitMethods.cs:13:10:13:11 | enter M2 |

‎csharp/ql/test/library-tests/controlflow/graph/BooleanNode.expected‎

Lines changed: 0 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -98,53 +98,11 @@
9898
| inc (line 3): true | Conditions.cs:7:9:8:16 | [inc (line 3): true] if (...) ... |
9999
| inc (line 3): true | Conditions.cs:7:13:7:16 | [inc (line 3): true] !... |
100100
| inc (line 3): true | Conditions.cs:7:14:7:16 | [inc (line 3): true] access to parameter inc |
101-
| last (line 118): false | Conditions.cs:116:24:116:24 | [last (line 118): false] access to local variable i |
102-
| last (line 118): false | Conditions.cs:116:24:116:38 | [last (line 118): false] ... < ... |
103-
| last (line 118): false | Conditions.cs:116:28:116:31 | [last (line 118): false] access to parameter args |
104-
| last (line 118): false | Conditions.cs:116:28:116:38 | [last (line 118): false] access to property Length |
105-
| last (line 118): false | Conditions.cs:116:41:116:41 | [last (line 118): false] access to local variable i |
106-
| last (line 118): false | Conditions.cs:116:41:116:43 | [last (line 118): false] ...++ |
107-
| last (line 118): false | Conditions.cs:117:9:123:9 | [last (line 118): false] {...} |
108-
| last (line 118): false | Conditions.cs:118:13:118:44 | [last (line 118): false] ... ...; |
109-
| last (line 118): false | Conditions.cs:118:17:118:20 | [last (line 118): false] access to local variable last |
110-
| last (line 118): false | Conditions.cs:118:17:118:43 | [last (line 118): false] Boolean last = ... |
111-
| last (line 118): false | Conditions.cs:118:24:118:24 | [last (line 118): false] access to local variable i |
112-
| last (line 118): false | Conditions.cs:118:24:118:43 | [last (line 118): false] ... == ... |
113-
| last (line 118): false | Conditions.cs:118:29:118:32 | [last (line 118): false] access to parameter args |
114-
| last (line 118): false | Conditions.cs:118:29:118:39 | [last (line 118): false] access to property Length |
115-
| last (line 118): false | Conditions.cs:118:29:118:43 | [last (line 118): false] ... - ... |
116-
| last (line 118): false | Conditions.cs:118:43:118:43 | [last (line 118): false] 1 |
117-
| last (line 118): false | Conditions.cs:119:13:120:23 | [last (line 118): false] if (...) ... |
118-
| last (line 118): false | Conditions.cs:119:17:119:21 | [last (line 118): false] !... |
119-
| last (line 118): false | Conditions.cs:119:18:119:21 | [last (line 118): false] access to local variable last |
120101
| last (line 118): false | Conditions.cs:120:17:120:17 | [last (line 118): false] access to local variable s |
121102
| last (line 118): false | Conditions.cs:120:17:120:22 | [last (line 118): false] ... = ... |
122103
| last (line 118): false | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
123104
| last (line 118): false | Conditions.cs:120:21:120:22 | [last (line 118): false] "" |
124105
| last (line 118): false | Conditions.cs:121:13:122:25 | [last (line 118): false] if (...) ... |
125106
| last (line 118): false | Conditions.cs:121:17:121:20 | [last (line 118): false] access to local variable last |
126-
| last (line 118): true | Conditions.cs:116:24:116:24 | [last (line 118): true] access to local variable i |
127-
| last (line 118): true | Conditions.cs:116:24:116:38 | [last (line 118): true] ... < ... |
128-
| last (line 118): true | Conditions.cs:116:28:116:31 | [last (line 118): true] access to parameter args |
129-
| last (line 118): true | Conditions.cs:116:28:116:38 | [last (line 118): true] access to property Length |
130-
| last (line 118): true | Conditions.cs:116:41:116:41 | [last (line 118): true] access to local variable i |
131-
| last (line 118): true | Conditions.cs:116:41:116:43 | [last (line 118): true] ...++ |
132-
| last (line 118): true | Conditions.cs:117:9:123:9 | [last (line 118): true] {...} |
133-
| last (line 118): true | Conditions.cs:118:13:118:44 | [last (line 118): true] ... ...; |
134-
| last (line 118): true | Conditions.cs:118:17:118:20 | [last (line 118): true] access to local variable last |
135-
| last (line 118): true | Conditions.cs:118:17:118:43 | [last (line 118): true] Boolean last = ... |
136-
| last (line 118): true | Conditions.cs:118:24:118:24 | [last (line 118): true] access to local variable i |
137-
| last (line 118): true | Conditions.cs:118:24:118:43 | [last (line 118): true] ... == ... |
138-
| last (line 118): true | Conditions.cs:118:29:118:32 | [last (line 118): true] access to parameter args |
139-
| last (line 118): true | Conditions.cs:118:29:118:39 | [last (line 118): true] access to property Length |
140-
| last (line 118): true | Conditions.cs:118:29:118:43 | [last (line 118): true] ... - ... |
141-
| last (line 118): true | Conditions.cs:118:43:118:43 | [last (line 118): true] 1 |
142-
| last (line 118): true | Conditions.cs:119:13:120:23 | [last (line 118): true] if (...) ... |
143-
| last (line 118): true | Conditions.cs:119:17:119:21 | [last (line 118): true] !... |
144-
| last (line 118): true | Conditions.cs:119:18:119:21 | [last (line 118): true] access to local variable last |
145107
| last (line 118): true | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
146108
| last (line 118): true | Conditions.cs:121:17:121:20 | [last (line 118): true] access to local variable last |
147-
| last (line 118): true | Conditions.cs:122:17:122:17 | [last (line 118): true] access to local variable s |
148-
| last (line 118): true | Conditions.cs:122:17:122:24 | [last (line 118): true] ... = ... |
149-
| last (line 118): true | Conditions.cs:122:17:122:25 | [last (line 118): true] ...; |
150-
| last (line 118): true | Conditions.cs:122:21:122:24 | [last (line 118): true] null |

‎csharp/ql/test/library-tests/controlflow/graph/ConditionBlock.expected‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -155,15 +155,11 @@
155155
| Conditions.cs:105:13:105:13 | access to parameter b | Conditions.cs:108:13:109:24 | [b (line 102): true] if (...) ... | true |
156156
| Conditions.cs:107:13:107:24 | [b (line 102): false] ... > ... | Conditions.cs:108:13:109:24 | [b (line 102): false] if (...) ... | true |
157157
| Conditions.cs:107:13:107:24 | [b (line 102): true] ... > ... | Conditions.cs:108:13:109:24 | [b (line 102): true] if (...) ... | true |
158-
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:117:9:123:9 | [last (line 118): false] {...} | true |
159-
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:117:9:123:9 | [last (line 118): true] {...} | true |
158+
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:113:10:113:11 | exit M9 | false |
159+
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:116:41:116:41 | access to local variable i | true |
160160
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:117:9:123:9 | {...} | true |
161161
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | true |
162162
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | true |
163-
| Conditions.cs:116:24:116:38 | [last (line 118): false] ... < ... | Conditions.cs:117:9:123:9 | [last (line 118): false] {...} | true |
164-
| Conditions.cs:116:24:116:38 | [last (line 118): true] ... < ... | Conditions.cs:117:9:123:9 | [last (line 118): true] {...} | true |
165-
| Conditions.cs:119:18:119:21 | access to local variable last | Conditions.cs:117:9:123:9 | [last (line 118): false] {...} | false |
166-
| Conditions.cs:119:18:119:21 | access to local variable last | Conditions.cs:117:9:123:9 | [last (line 118): true] {...} | true |
167163
| Conditions.cs:119:18:119:21 | access to local variable last | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | false |
168164
| Conditions.cs:119:18:119:21 | access to local variable last | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | true |
169165
| ExitMethods.cs:43:9:46:9 | [exception: Exception] catch (...) {...} | ExitMethods.cs:47:9:50:9 | [exception: Exception] catch (...) {...} | false |

0 commit comments

Comments
 (0)