Skip to content

Commit 1b12e84

Browse files
calumgrantcalumgrant
authored
Merge pull request #491 from hvitved/csharp/cfg/split-negation
C#: Fix two bugs in Boolean CFG splitting
2 parents f177e34 + 8233e34 commit 1b12e84

File tree

13 files changed

+350
-16
lines changed

13 files changed

+350
-16
lines changed

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

Lines changed: 20 additions & 16 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
}
@@ -3636,7 +3653,7 @@ module ControlFlow {
36363653
override predicate hasEntry(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
36373654
succ = succ(pred, c) and
36383655
this.getSubKind().startsSplit(pred) and
3639-
c = any(BooleanCompletion bc | bc.getOuterValue() = this.getBranch())
3656+
c = any(BooleanCompletion bc | bc.getInnerValue() = this.getBranch())
36403657
}
36413658

36423659
private ConditionBlock getACorrelatedCondition(boolean inverted) {
@@ -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: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -164,6 +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:17:116:21 | Int32 i = ... | 10 |
168+
| Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:113:10:113:11 | exit M9 | 1 |
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 |
171+
| 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: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 |
167174
| ExitMethods.cs:7:10:7:11 | enter M1 | ExitMethods.cs:7:10:7:11 | exit M1 | 7 |
168175
| ExitMethods.cs:13:10:13:11 | enter M2 | ExitMethods.cs:13:10:13:11 | exit M2 | 7 |
169176
| 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: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -360,6 +360,27 @@
360360
| post | Conditions.cs:110:16:110:16 | access to local variable x | Conditions.cs:108:13:109:24 | [b (line 102): false] if (...) ... |
361361
| post | Conditions.cs:110:16:110:16 | access to local variable x | Conditions.cs:108:13:109:24 | [b (line 102): true] if (...) ... |
362362
| post | Conditions.cs:110:16:110:16 | access to local variable x | Conditions.cs:110:16:110:16 | access to local variable x |
363+
| post | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:113:10:113:11 | enter M9 |
364+
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:113:10:113:11 | enter M9 |
365+
| 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: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 |
368+
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:117:9:123:9 | {...} |
369+
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
370+
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
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 (...) ... |
381+
| post | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:117:9:123:9 | {...} |
382+
| post | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
383+
| post | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
363384
| post | ExitMethods.cs:7:10:7:11 | enter M1 | ExitMethods.cs:7:10:7:11 | enter M1 |
364385
| post | ExitMethods.cs:13:10:13:11 | enter M2 | ExitMethods.cs:13:10:13:11 | enter M2 |
365386
| post | ExitMethods.cs:19:10:19:11 | enter M3 | ExitMethods.cs:19:10:19:11 | enter M3 |
@@ -1705,6 +1726,27 @@
17051726
| pre | Conditions.cs:108:13:109:24 | [b (line 102): false] if (...) ... | Conditions.cs:108:13:109:24 | [b (line 102): false] if (...) ... |
17061727
| pre | Conditions.cs:108:13:109:24 | [b (line 102): true] if (...) ... | Conditions.cs:108:13:109:24 | [b (line 102): true] if (...) ... |
17071728
| pre | Conditions.cs:110:16:110:16 | access to local variable x | Conditions.cs:110:16:110:16 | access to local variable x |
1729+
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:113:10:113:11 | enter M9 |
1730+
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:113:10:113:11 | exit M9 |
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 |
1733+
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:117:9:123:9 | {...} |
1734+
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
1735+
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
1736+
| pre | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:113:10:113:11 | exit M9 |
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 |
1745+
| pre | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:117:9:123:9 | {...} |
1746+
| pre | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
1747+
| pre | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
1748+
| pre | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
1749+
| pre | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
17081750
| pre | ExitMethods.cs:7:10:7:11 | enter M1 | ExitMethods.cs:7:10:7:11 | enter M1 |
17091751
| pre | ExitMethods.cs:13:10:13:11 | enter M2 | ExitMethods.cs:13:10:13:11 | enter M2 |
17101752
| pre | ExitMethods.cs:19:10:19:11 | enter M3 | ExitMethods.cs:19:10:19:11 | enter M3 |

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,3 +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:120:17:120:17 | [last (line 118): false] access to local variable s |
102+
| last (line 118): false | Conditions.cs:120:17:120:22 | [last (line 118): false] ... = ... |
103+
| last (line 118): false | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
104+
| last (line 118): false | Conditions.cs:120:21:120:22 | [last (line 118): false] "" |
105+
| last (line 118): false | Conditions.cs:121:13:122:25 | [last (line 118): false] if (...) ... |
106+
| last (line 118): false | Conditions.cs:121:17:121:20 | [last (line 118): false] access to local variable last |
107+
| last (line 118): true | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
108+
| last (line 118): true | Conditions.cs:121:17:121:20 | [last (line 118): true] access to local variable last |

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,13 @@
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: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 |
160+
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:117:9:123:9 | {...} | true |
161+
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | true |
162+
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | true |
163+
| Conditions.cs:119:18:119:21 | access to local variable last | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | false |
164+
| Conditions.cs:119:18:119:21 | access to local variable last | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | true |
158165
| ExitMethods.cs:43:9:46:9 | [exception: Exception] catch (...) {...} | ExitMethods.cs:47:9:50:9 | [exception: Exception] catch (...) {...} | false |
159166
| ExitMethods.cs:55:13:55:13 | access to parameter b | ExitMethods.cs:56:19:56:33 | object creation of type Exception | true |
160167
| ExitMethods.cs:61:13:61:13 | access to parameter b | ExitMethods.cs:62:19:62:33 | object creation of type Exception | true |

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -187,10 +187,16 @@
187187
| 108 | 18 | Conditions.cs:108:18:108:18 | [b (line 102): false] access to parameter b | false | 109 | 17 | Conditions.cs:109:17:109:24 | ...; |
188188
| 108 | 18 | Conditions.cs:108:18:108:18 | [b (line 102): true] access to parameter b | true | 110 | 16 | Conditions.cs:110:16:110:16 | access to local variable x |
189189
| 110 | 20 | cflow.cs:110:20:110:23 | true | true | 111 | 13 | cflow.cs:111:13:113:13 | {...} |
190+
| 116 | 24 | Conditions.cs:116:24:116:38 | ... < ... | false | 113 | 10 | Conditions.cs:113:10:113:11 | exit M9 |
191+
| 116 | 24 | Conditions.cs:116:24:116:38 | ... < ... | true | 117 | 9 | Conditions.cs:117:9:123:9 | {...} |
190192
| 117 | 25 | Switch.cs:117:25:117:32 | ... == ... | false | 118 | 13 | Switch.cs:118:13:118:33 | case ...: |
191193
| 117 | 25 | Switch.cs:117:25:117:32 | ... == ... | true | 117 | 43 | Switch.cs:117:43:117:43 | 1 |
192194
| 118 | 25 | Switch.cs:118:25:118:31 | ... == ... | false | 120 | 17 | Switch.cs:120:17:120:17 | 1 |
193195
| 118 | 25 | Switch.cs:118:25:118:31 | ... == ... | true | 118 | 42 | Switch.cs:118:42:118:42 | 2 |
196+
| 119 | 18 | Conditions.cs:119:18:119:21 | access to local variable last | false | 120 | 17 | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
197+
| 119 | 18 | Conditions.cs:119:18:119:21 | access to local variable last | true | 121 | 13 | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
198+
| 121 | 17 | Conditions.cs:121:17:121:20 | [last (line 118): false] access to local variable last | false | 116 | 41 | Conditions.cs:116:41:116:41 | access to local variable i |
199+
| 121 | 17 | Conditions.cs:121:17:121:20 | [last (line 118): true] access to local variable last | true | 122 | 17 | Conditions.cs:122:17:122:25 | ...; |
194200
| 127 | 32 | cflow.cs:127:32:127:44 | ... == ... | false | 127 | 53 | cflow.cs:127:53:127:57 | this access |
195201
| 127 | 32 | cflow.cs:127:32:127:44 | ... == ... | true | 127 | 48 | cflow.cs:127:48:127:49 | "" |
196202
| 162 | 48 | cflow.cs:162:48:162:51 | [exception: Exception] true | true | 163 | 9 | cflow.cs:163:9:165:9 | {...} |

‎csharp/ql/test/library-tests/controlflow/graph/Conditions.cs‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -109,4 +109,17 @@ string M8(bool b)
109109
x += "";
110110
return x;
111111
}
112+
113+
void M9(string[] args)
114+
{
115+
string s = null;
116+
for(var i = 0; i < args.Length; i++)
117+
{
118+
var last = i == args.Length - 1;
119+
if (!last)
120+
s = "";
121+
if (last)
122+
s = null;
123+
}
124+
}
112125
}

0 commit comments

Comments
 (0)