Skip to content

C#: Fix two bugs in Boolean CFG splitting #491

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
calumgrant merged 3 commits into from
Nov 21, 2018
Merged

C#: Fix two bugs in Boolean CFG splitting #491

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8412185
C#: Add CFG test
hvitved Nov 19, 2018
89d5daa
C#: Fix Boolean splitting negation bug
hvitved Nov 19, 2018
8233e34
C#: Fix Boolean splitting for variables defined in a loop
hvitved Nov 19, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 20 additions & 16 deletions csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3476,6 +3476,12 @@ module ControlFlow {
this.correlatesConditions(any(ConditionBlock cb | cb.getLastElement() = cfe), _, _)
}

/**
* Holds if basic block `bb` can reach a condition correlated with a
* split of this kind.
*/
abstract predicate canReachCorrelatedCondition(PreBasicBlock bb);

/** Gets the callable that this Boolean split kind belongs to. */
abstract Callable getEnclosingCallable();

Expand Down Expand Up @@ -3553,6 +3559,17 @@ module ControlFlow {
)
}

override predicate canReachCorrelatedCondition(PreBasicBlock bb) {
this.correlatesConditions(_, bb, _) and
not def.getBasicBlock() = bb
or
exists(PreBasicBlock mid |
this.canReachCorrelatedCondition(mid) |
bb = mid.getAPredecessor() and
not def.getBasicBlock() = bb
)
}

override Callable getEnclosingCallable() {
result = def.getCallable()
}
Expand Down Expand Up @@ -3636,7 +3653,7 @@ module ControlFlow {
override predicate hasEntry(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
succ = succ(pred, c) and
this.getSubKind().startsSplit(pred) and
c = any(BooleanCompletion bc | bc.getOuterValue() = this.getBranch())
c = any(BooleanCompletion bc | bc.getInnerValue() = this.getBranch())
}

private ConditionBlock getACorrelatedCondition(boolean inverted) {
Expand All @@ -3662,26 +3679,13 @@ module ControlFlow {
)
}

/**
* Holds if basic block `bb` can reach a condition correlated with the value
* recorded in this split.
*/
private predicate canReachCorrelatedCondition(PreBasicBlock bb) {
bb = this.getACorrelatedCondition(_)
or
exists(PreBasicBlock mid |
this.canReachCorrelatedCondition(mid) |
bb = mid.getAPredecessor()
)
}

override predicate hasExit(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
exists(PreBasicBlock bb |
this.appliesToBlock(bb, c) |
pred = bb.getLastElement() and
succ = succ(pred, c) and
// Exit this split if we can no longer reach a correlated condition
not this.canReachCorrelatedCondition(succ)
not this.getSubKind().canReachCorrelatedCondition(succ)
)
}

Expand All @@ -3702,7 +3706,7 @@ module ControlFlow {
pred = bb.getLastElement()
implies
// We must still be able to reach a correlated condition to stay in this split
this.canReachCorrelatedCondition(succ) and
this.getSubKind().canReachCorrelatedCondition(succ) and
c = c0
)
)
Expand Down
7 changes: 7 additions & 0 deletions csharp/ql/test/library-tests/controlflow/graph/BasicBlock.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,13 @@
| Conditions.cs:108:13:109:24 | [b (line 102): false] if (...) ... | Conditions.cs:109:17:109:23 | ... = ... | 9 |
| 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 |
| Conditions.cs:110:16:110:16 | access to local variable x | Conditions.cs:102:12:102:13 | exit M8 | 3 |
| Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:116:17:116:21 | Int32 i = ... | 10 |
| Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:113:10:113:11 | exit M9 | 1 |
| Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:116:24:116:38 | ... < ... | 4 |
| Conditions.cs:116:41:116:41 | access to local variable i | Conditions.cs:116:41:116:43 | ...++ | 2 |
| Conditions.cs:117:9:123:9 | {...} | Conditions.cs:119:18:119:21 | access to local variable last | 13 |
| 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 |
| Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | Conditions.cs:122:17:122:24 | ... = ... | 6 |
| ExitMethods.cs:7:10:7:11 | enter M1 | ExitMethods.cs:7:10:7:11 | exit M1 | 7 |
| ExitMethods.cs:13:10:13:11 | enter M2 | ExitMethods.cs:13:10:13:11 | exit M2 | 7 |
| ExitMethods.cs:19:10:19:11 | enter M3 | ExitMethods.cs:19:10:19:11 | exit M3 | 6 |
Expand Down
42 changes: 42 additions & 0 deletions csharp/ql/test/library-tests/controlflow/graph/BasicBlockDominance.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -360,6 +360,27 @@
| post | Conditions.cs:110:16:110:16 | access to local variable x | Conditions.cs:108:13:109:24 | [b (line 102): false] if (...) ... |
| post | Conditions.cs:110:16:110:16 | access to local variable x | Conditions.cs:108:13:109:24 | [b (line 102): true] if (...) ... |
| post | Conditions.cs:110:16:110:16 | access to local variable x | Conditions.cs:110:16:110:16 | access to local variable x |
| post | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:113:10:113:11 | enter M9 |
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:113:10:113:11 | enter M9 |
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:113:10:113:11 | exit M9 |
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:116:24:116:24 | access to local variable i |
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:116:41:116:41 | access to local variable i |
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:117:9:123:9 | {...} |
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
| post | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
| post | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:113:10:113:11 | enter M9 |
| post | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:116:24:116:24 | access to local variable i |
| post | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:116:41:116:41 | access to local variable i |
| post | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:117:9:123:9 | {...} |
| post | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
| post | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
| post | Conditions.cs:116:41:116:41 | access to local variable i | Conditions.cs:116:41:116:41 | access to local variable i |
| post | Conditions.cs:116:41:116:41 | access to local variable i | Conditions.cs:117:9:123:9 | {...} |
| post | Conditions.cs:116:41:116:41 | access to local variable i | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
| post | Conditions.cs:116:41:116:41 | access to local variable i | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
| post | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:117:9:123:9 | {...} |
| post | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
| post | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
| post | ExitMethods.cs:7:10:7:11 | enter M1 | ExitMethods.cs:7:10:7:11 | enter M1 |
| post | ExitMethods.cs:13:10:13:11 | enter M2 | ExitMethods.cs:13:10:13:11 | enter M2 |
| post | ExitMethods.cs:19:10:19:11 | enter M3 | ExitMethods.cs:19:10:19:11 | enter M3 |
Expand Down Expand Up @@ -1705,6 +1726,27 @@
| pre | Conditions.cs:108:13:109:24 | [b (line 102): false] if (...) ... | Conditions.cs:108:13:109:24 | [b (line 102): false] if (...) ... |
| pre | Conditions.cs:108:13:109:24 | [b (line 102): true] if (...) ... | Conditions.cs:108:13:109:24 | [b (line 102): true] if (...) ... |
| pre | Conditions.cs:110:16:110:16 | access to local variable x | Conditions.cs:110:16:110:16 | access to local variable x |
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:113:10:113:11 | enter M9 |
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:113:10:113:11 | exit M9 |
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:116:24:116:24 | access to local variable i |
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:116:41:116:41 | access to local variable i |
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:117:9:123:9 | {...} |
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
| pre | Conditions.cs:113:10:113:11 | enter M9 | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
| pre | Conditions.cs:113:10:113:11 | exit M9 | Conditions.cs:113:10:113:11 | exit M9 |
| pre | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:113:10:113:11 | exit M9 |
| pre | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:116:24:116:24 | access to local variable i |
| pre | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:116:41:116:41 | access to local variable i |
| pre | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:117:9:123:9 | {...} |
| pre | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
| pre | Conditions.cs:116:24:116:24 | access to local variable i | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
| pre | Conditions.cs:116:41:116:41 | access to local variable i | Conditions.cs:116:41:116:41 | access to local variable i |
| pre | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:116:41:116:41 | access to local variable i |
| pre | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:117:9:123:9 | {...} |
| pre | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
| pre | Conditions.cs:117:9:123:9 | {...} | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
| pre | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
| pre | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
| pre | ExitMethods.cs:7:10:7:11 | enter M1 | ExitMethods.cs:7:10:7:11 | enter M1 |
| pre | ExitMethods.cs:13:10:13:11 | enter M2 | ExitMethods.cs:13:10:13:11 | enter M2 |
| pre | ExitMethods.cs:19:10:19:11 | enter M3 | ExitMethods.cs:19:10:19:11 | enter M3 |
Expand Down
8 changes: 8 additions & 0 deletions csharp/ql/test/library-tests/controlflow/graph/BooleanNode.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,3 +98,11 @@
| inc (line 3): true | Conditions.cs:7:9:8:16 | [inc (line 3): true] if (...) ... |
| inc (line 3): true | Conditions.cs:7:13:7:16 | [inc (line 3): true] !... |
| inc (line 3): true | Conditions.cs:7:14:7:16 | [inc (line 3): true] access to parameter inc |
| last (line 118): false | Conditions.cs:120:17:120:17 | [last (line 118): false] access to local variable s |
| last (line 118): false | Conditions.cs:120:17:120:22 | [last (line 118): false] ... = ... |
| last (line 118): false | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; |
| last (line 118): false | Conditions.cs:120:21:120:22 | [last (line 118): false] "" |
| last (line 118): false | Conditions.cs:121:13:122:25 | [last (line 118): false] if (...) ... |
| last (line 118): false | Conditions.cs:121:17:121:20 | [last (line 118): false] access to local variable last |
| last (line 118): true | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... |
| last (line 118): true | Conditions.cs:121:17:121:20 | [last (line 118): true] access to local variable last |
7 changes: 7 additions & 0 deletions csharp/ql/test/library-tests/controlflow/graph/ConditionBlock.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,13 @@
| Conditions.cs:105:13:105:13 | access to parameter b | Conditions.cs:108:13:109:24 | [b (line 102): true] if (...) ... | true |
| Conditions.cs:107:13:107:24 | [b (line 102): false] ... > ... | Conditions.cs:108:13:109:24 | [b (line 102): false] if (...) ... | true |
| Conditions.cs:107:13:107:24 | [b (line 102): true] ... > ... | Conditions.cs:108:13:109:24 | [b (line 102): true] if (...) ... | true |
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:113:10:113:11 | exit M9 | false |
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:116:41:116:41 | access to local variable i | true |
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:117:9:123:9 | {...} | true |
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | true |
| Conditions.cs:116:24:116:38 | ... < ... | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | true |
| Conditions.cs:119:18:119:21 | access to local variable last | Conditions.cs:120:17:120:23 | [last (line 118): false] ...; | false |
| Conditions.cs:119:18:119:21 | access to local variable last | Conditions.cs:121:13:122:25 | [last (line 118): true] if (...) ... | true |
| ExitMethods.cs:43:9:46:9 | [exception: Exception] catch (...) {...} | ExitMethods.cs:47:9:50:9 | [exception: Exception] catch (...) {...} | false |
| ExitMethods.cs:55:13:55:13 | access to parameter b | ExitMethods.cs:56:19:56:33 | object creation of type Exception | true |
| ExitMethods.cs:61:13:61:13 | access to parameter b | ExitMethods.cs:62:19:62:33 | object creation of type Exception | true |
Expand Down
6 changes: 6 additions & 0 deletions csharp/ql/test/library-tests/controlflow/graph/ConditionalFlow.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -187,10 +187,16 @@
| 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 | ...; |
| 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 |
| 110 | 20 | cflow.cs:110:20:110:23 | true | true | 111 | 13 | cflow.cs:111:13:113:13 | {...} |
| 116 | 24 | Conditions.cs:116:24:116:38 | ... < ... | false | 113 | 10 | Conditions.cs:113:10:113:11 | exit M9 |
| 116 | 24 | Conditions.cs:116:24:116:38 | ... < ... | true | 117 | 9 | Conditions.cs:117:9:123:9 | {...} |
| 117 | 25 | Switch.cs:117:25:117:32 | ... == ... | false | 118 | 13 | Switch.cs:118:13:118:33 | case ...: |
| 117 | 25 | Switch.cs:117:25:117:32 | ... == ... | true | 117 | 43 | Switch.cs:117:43:117:43 | 1 |
| 118 | 25 | Switch.cs:118:25:118:31 | ... == ... | false | 120 | 17 | Switch.cs:120:17:120:17 | 1 |
| 118 | 25 | Switch.cs:118:25:118:31 | ... == ... | true | 118 | 42 | Switch.cs:118:42:118:42 | 2 |
| 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] ...; |
| 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 (...) ... |
| 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 |
| 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 | ...; |
| 127 | 32 | cflow.cs:127:32:127:44 | ... == ... | false | 127 | 53 | cflow.cs:127:53:127:57 | this access |
| 127 | 32 | cflow.cs:127:32:127:44 | ... == ... | true | 127 | 48 | cflow.cs:127:48:127:49 | "" |
| 162 | 48 | cflow.cs:162:48:162:51 | [exception: Exception] true | true | 163 | 9 | cflow.cs:163:9:165:9 | {...} |
Expand Down
13 changes: 13 additions & 0 deletions csharp/ql/test/library-tests/controlflow/graph/Conditions.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -109,4 +109,17 @@ string M8(bool b)
x += "";
return x;
}

void M9(string[] args)
{
string s = null;
for(var i = 0; i < args.Length; i++)
{
var last = i == args.Length - 1;
if (!last)
s = "";
if (last)
s = null;
}
}
}
Loading