Skip to content

Commit 8263b24

Browse files
calumgrantcalumgrant
authored
Merge pull request #152 from hvitved/csharp/base-ssa
C#: Fix bug in BaseSsa library
2 parents 50b5a3b + 124a00b commit 8263b24

File tree

14 files changed

+155
-128
lines changed

14 files changed

+155
-128
lines changed

‎csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -119,11 +119,11 @@ module Ssa {
119119
ad.getAControlFlowNode() = bb.getNode(i)
120120
and
121121
// In cases like `(x, x) = (0, 1)`, we discard the first (dead) definition of `x`
122-
not exists(TupleAssignmentDefinition tdef, TupleAssignmentDefinition other |
123-
tdef = ad |
124-
other.getAssignment() = tdef.getAssignment() and
125-
other.getEvaluationOrder() > tdef.getEvaluationOrder() and
126-
other = v.getADefinition()
122+
not exists(TupleAssignmentDefinition first, TupleAssignmentDefinition second |
123+
first = ad |
124+
second.getAssignment() = first.getAssignment() and
125+
second.getEvaluationOrder() > first.getEvaluationOrder() and
126+
second = v.getADefinition()
127127
)
128128
and
129129
// In cases like `M(out x, out x)`, there is no inherent evaluation order, so we
@@ -1094,7 +1094,7 @@ module Ssa {
10941094

10951095
private module SimpleDelegateAnalysis {
10961096
private import semmle.code.csharp.dataflow.DelegateDataFlow
1097-
private import semmle.code.csharp.dataflow.DataFlowInternal
1097+
private import semmle.code.csharp.dataflow.internal.Steps
10981098
private import semmle.code.csharp.frameworks.system.linq.Expressions
10991099

11001100
/**
@@ -1124,7 +1124,7 @@ module Ssa {
11241124
}
11251125

11261126
private predicate delegateFlowStep(Expr pred, Expr succ) {
1127-
DataFlowInternal::stepClosed(pred, succ)
1127+
Steps::stepClosed(pred, succ)
11281128
or
11291129
exists(Call call, Callable callable |
11301130
callable.getSourceDeclaration().canReturn(pred) and

‎csharp/ql/src/semmle/code/csharp/dataflow/internal/BaseSSA.qll‎

Lines changed: 127 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
import csharp
2+
3+
/**
4+
* INTERNAL: Do not use.
5+
*
6+
* Provides a simple SSA implementation for local scope variables.
7+
*/
8+
module BaseSsa {
9+
private import ControlFlowGraph
10+
private import AssignableDefinitions
11+
12+
private class SimpleLocalScopeVariable extends LocalScopeVariable {
13+
SimpleLocalScopeVariable() {
14+
not exists(AssignableDefinition def1, AssignableDefinition def2 |
15+
def1.getTarget() = this and
16+
def2.getTarget() = this and
17+
def1.getEnclosingCallable() != def2.getEnclosingCallable()
18+
)
19+
}
20+
}
21+
22+
/**
23+
* Holds if the `i`th node of basic block `bb` is assignable definition `def`,
24+
* targeting local scope variable `v`.
25+
*/
26+
private predicate defAt(BasicBlock bb, int i, AssignableDefinition def, SimpleLocalScopeVariable v) {
27+
bb.getNode(i) = def.getAControlFlowNode() and
28+
v = def.getTarget() and
29+
// In cases like `(x, x) = (0, 1)`, we discard the first (dead) definition of `x`
30+
not exists(TupleAssignmentDefinition first, TupleAssignmentDefinition second |
31+
first = def |
32+
second.getAssignment() = first.getAssignment() and
33+
second.getEvaluationOrder() > first.getEvaluationOrder() and
34+
second.getTarget() = v
35+
)
36+
}
37+
38+
/**
39+
* Holds if basic block `bb` would need to start with a phi node for local scope
40+
* variable `v` in an SSA representation.
41+
*/
42+
private predicate needsPhiNode(BasicBlock bb, SimpleLocalScopeVariable v) {
43+
exists(BasicBlock def |
44+
def.inDominanceFrontier(bb) |
45+
defAt(def, _, _, v) or
46+
needsPhiNode(def, v)
47+
)
48+
}
49+
50+
private newtype SsaRefKind = SsaRead() or SsaDef()
51+
52+
/**
53+
* Holds if the `i`th node of basic block `bb` is a reference to `v`,
54+
* either a read (when `k` is `SsaRead()`) or a write including phi nodes
55+
* (when `k` is `SsaDef()`).
56+
*/
57+
private predicate ssaRef(BasicBlock bb, int i, SimpleLocalScopeVariable v, SsaRefKind k) {
58+
bb.getNode(i).getElement() = v.getAnAccess().(VariableRead) and
59+
k = SsaRead()
60+
or
61+
defAt(bb, i, _, v) and
62+
k = SsaDef()
63+
or
64+
needsPhiNode(bb, v) and
65+
i = -1 and
66+
k = SsaDef()
67+
}
68+
69+
/**
70+
* Gets the (1-based) rank of the reference to `v` at the `i`th node of basic
71+
* block `bb`, which has the given reference kind `k`.
72+
*/
73+
private int ssaRefRank(BasicBlock bb, int i, SimpleLocalScopeVariable v, SsaRefKind k) {
74+
i = rank[result](int j | ssaRef(bb, j, v, _)) and
75+
ssaRef(bb, i, v, k)
76+
}
77+
78+
/**
79+
* Holds if definition `def` of local scope variable `v` inside basic block
80+
* `bb` reaches the reference at rank `rnk`, without passing through another
81+
* definition of `v`, including phi nodes.
82+
*/
83+
private predicate defReachesRank(BasicBlock bb, AssignableDefinition def, SimpleLocalScopeVariable v, int rnk) {
84+
exists(int i |
85+
rnk = ssaRefRank(bb, i, v, SsaDef()) |
86+
defAt(bb, i, def, v)
87+
)
88+
or
89+
defReachesRank(bb, def, v, rnk - 1) and
90+
rnk = ssaRefRank(bb, _, v, SsaRead())
91+
}
92+
93+
/**
94+
* Holds if definition `def` of local scope variable `v` reaches the end of
95+
* basic block `bb` without passing through another definition of `v`, including
96+
* phi nodes.
97+
*/
98+
private predicate reachesEndOf(AssignableDefinition def, SimpleLocalScopeVariable v, BasicBlock bb) {
99+
exists(int rnk |
100+
defReachesRank(bb, def, v, rnk) and
101+
rnk = max(ssaRefRank(bb, _, v, _))
102+
)
103+
or
104+
exists(BasicBlock mid |
105+
reachesEndOf(def, v, mid) and
106+
not exists(ssaRefRank(mid, _, v, SsaDef())) and
107+
bb = mid.getASuccessor()
108+
)
109+
}
110+
111+
/**
112+
* Gets a read of the SSA definition for variable `v` at definition `def`. That is,
113+
* a read that is guaranteed to read the value assigned at definition `def`.
114+
*/
115+
cached AssignableRead getARead(AssignableDefinition def, SimpleLocalScopeVariable v) {
116+
exists(BasicBlock bb, int i, int rnk |
117+
result.getTarget() = v and
118+
result.getAControlFlowNode() = bb.getNode(i) and
119+
rnk = ssaRefRank(bb, i, v, SsaRead())
120+
|
121+
defReachesRank(bb, def, v, rnk)
122+
or
123+
reachesEndOf(def, v, bb.getAPredecessor()) and
124+
not ssaRefRank(bb, _, v, SsaDef()) < rnk
125+
)
126+
}
127+
}

csharp/ql/src/semmle/code/csharp/dataflow/DataFlowInternal.qll renamed to csharp/ql/src/semmle/code/csharp/dataflow/internal/Steps.qll

Lines changed: 4 additions & 105 deletions
Original file line numberDiff line numberDiff line change
@@ -1,108 +1,5 @@
11
import csharp
22

3-
private cached module MiniSsa {
4-
private import ControlFlowGraph
5-
6-
/**
7-
* Holds if the `i`th node of basic block `bb` is assignable definition `def`,
8-
* targeting local scope variable `v`.
9-
*/
10-
private predicate defAt(BasicBlock bb, int i, AssignableDefinition def, LocalScopeVariable v) {
11-
bb.getNode(i) = def.getAControlFlowNode() and
12-
v = def.getTarget()
13-
}
14-
15-
/**
16-
* Holds if basic block `bb` would need to start with a phi node for local scope
17-
* variable `v` in an SSA representation.
18-
*/
19-
private predicate needsPhiNode(BasicBlock bb, LocalScopeVariable v) {
20-
exists(BasicBlock def |
21-
def.inDominanceFrontier(bb) |
22-
defAt(def, _, _, v) or
23-
needsPhiNode(def, v)
24-
)
25-
}
26-
27-
private newtype SsaRefKind = SsaRead() or SsaDef()
28-
29-
/**
30-
* Holds if the `i`th node of basic block `bb` is a reference to `v`,
31-
* either a read (when `k` is `SsaRead()`) or a write including phi nodes
32-
* (when `k` is `SsaDef()`).
33-
*/
34-
private predicate ssaRef(BasicBlock bb, int i, LocalScopeVariable v, SsaRefKind k) {
35-
bb.getNode(i).getElement() = v.getAnAccess().(VariableRead) and
36-
k = SsaRead()
37-
or
38-
defAt(bb, i, _, v) and
39-
k = SsaDef()
40-
or
41-
needsPhiNode(bb, v) and
42-
i = -1 and
43-
k = SsaDef()
44-
}
45-
46-
/**
47-
* Gets the (1-based) rank of the reference to `v` at the `i`th node of basic
48-
* block `bb`, which has the given reference kind `k`.
49-
*/
50-
private int ssaRefRank(BasicBlock bb, int i, LocalScopeVariable v, SsaRefKind k) {
51-
i = rank[result](int j | ssaRef(bb, j, v, _)) and
52-
ssaRef(bb, i, v, k)
53-
}
54-
55-
/**
56-
* Holds if definition `def` of local scope variable `v` inside basic block
57-
* `bb` reaches the reference at rank `rnk`, without passing through another
58-
* definition of `v`, including phi nodes.
59-
*/
60-
private predicate defReachesRank(BasicBlock bb, AssignableDefinition def, LocalScopeVariable v, int rnk) {
61-
exists(int i |
62-
rnk = ssaRefRank(bb, i, v, SsaDef()) |
63-
defAt(bb, i, def, v)
64-
)
65-
or
66-
defReachesRank(bb, def, v, rnk - 1) and
67-
rnk = ssaRefRank(bb, _, v, SsaRead())
68-
}
69-
70-
/**
71-
* Holds if definition `def` of local scope variable `v` reaches the end of
72-
* basic block `bb` without passing through another definition of `v`, including
73-
* phi nodes.
74-
*/
75-
private predicate reachesEndOf(AssignableDefinition def, LocalScopeVariable v, BasicBlock bb) {
76-
exists(int rnk |
77-
defReachesRank(bb, def, v, rnk) and
78-
rnk = max(ssaRefRank(bb, _, v, _))
79-
)
80-
or
81-
exists(BasicBlock mid |
82-
reachesEndOf(def, v, mid) and
83-
not exists(ssaRefRank(mid, _, v, SsaDef())) and
84-
bb = mid.getASuccessor()
85-
)
86-
}
87-
88-
/**
89-
* Gets a read of the SSA definition for variable `v` at definition `def`. That is,
90-
* a read that is guaranteed to read the value assigned at definition `def`.
91-
*/
92-
cached AssignableRead getARead(AssignableDefinition def, LocalScopeVariable v) {
93-
exists(BasicBlock bb, int i, int rnk |
94-
result.getTarget() = v and
95-
result.getAControlFlowNode() = bb.getNode(i) and
96-
rnk = ssaRefRank(bb, i, v, SsaRead())
97-
|
98-
defReachesRank(bb, def, v, rnk)
99-
or
100-
reachesEndOf(def, v, bb.getAPredecessor()) and
101-
not ssaRefRank(bb, i, v, SsaDef()) < rnk
102-
)
103-
}
104-
}
105-
1063
/**
1074
* INTERNAL: Do not use.
1085
*
@@ -112,12 +9,14 @@ private cached module MiniSsa {
1129
* Instead, this library relies on a self-contained, minimalistic SSA-like
11310
* implementation.
11411
*/
115-
module DataFlowInternal {
12+
module Steps {
13+
private import semmle.code.csharp.dataflow.internal.BaseSSA
14+
11615
/**
11716
* Gets a read that is guaranteed to read the value assigned at definition `def`.
11817
*/
11918
private AssignableRead getARead(AssignableDefinition def) {
120-
result = MiniSsa::getARead(def, _)
19+
result = BaseSsa::getARead(def, _)
12120
or
12221
exists(LocalScopeVariable v |
12322
def.getTarget() = v |

‎csharp/ql/src/semmle/code/csharp/dispatch/Dispatch.qll‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ import csharp
99
private import RuntimeCallable
1010
private import OverridableCallable
1111
private import semmle.code.csharp.Conversion
12-
private import semmle.code.csharp.dataflow.DataFlowInternal
12+
private import semmle.code.csharp.dataflow.internal.Steps
1313
private import semmle.code.csharp.frameworks.System
1414
private import semmle.code.csharp.frameworks.system.Reflection
1515

@@ -145,8 +145,8 @@ private module Internal {
145145
* using simple data flow.
146146
*/
147147
private Expr getAMethodCallArgSource(MethodCallArg e) {
148-
DataFlowInternal::stepOpen*(result, e) and
149-
not DataFlowInternal::stepOpen(_, result)
148+
Steps::stepOpen*(result, e) and
149+
not Steps::stepOpen(_, result)
150150
}
151151

152152
/**
@@ -302,7 +302,7 @@ private module Internal {
302302
}
303303

304304
private predicate stepExpr0(Expr succ, Expr pred) {
305-
DataFlowInternal::stepOpen(pred, succ)
305+
Steps::stepOpen(pred, succ)
306306
or
307307
exists(Assignable a |
308308
a instanceof Field or

‎csharp/ql/test/library-tests/dataflow/ssa/BaseSsaConsistency.expected‎

Whitespace-only changes.

‎csharp/ql/test/library-tests/dataflow/ssa/BaseSsaConsistency.ql‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
import csharp
2+
import semmle.code.csharp.dataflow.internal.BaseSSA
3+
4+
from AssignableRead ar, AssignableDefinition def, LocalScopeVariable v
5+
where ar = BaseSsa::getARead(def, v)
6+
and not exists(Ssa::ExplicitDefinition edef |
7+
edef.getADefinition() = def and
8+
edef.getARead() = ar
9+
)
10+
select ar, def

‎csharp/ql/test/library-tests/dataflow/ssa/ReadAdjacentRead.expected‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
| Capture.cs:6:16:6:16 | i | Capture.cs:8:17:8:17 | access to parameter i | Capture.cs:33:13:33:13 | access to parameter i |
22
| Capture.cs:8:13:8:13 | x | Capture.cs:16:17:16:17 | access to local variable x | Capture.cs:17:21:17:21 | access to local variable x |
3+
| Capture.cs:8:13:8:13 | x | Capture.cs:45:13:45:13 | access to local variable x | Capture.cs:47:13:47:13 | access to local variable x |
34
| Capture.cs:10:16:10:16 | a | Capture.cs:38:9:38:9 | access to local variable a | Capture.cs:46:12:46:12 | access to local variable a |
45
| Capture.cs:65:45:65:51 | strings | Capture.cs:68:18:68:24 | access to parameter strings | Capture.cs:70:9:70:15 | access to parameter strings |
56
| Consistency.cs:5:9:5:13 | Field | Consistency.cs:26:13:26:19 | access to field Field | Consistency.cs:27:13:27:19 | access to field Field |

‎csharp/ql/test/library-tests/dataflow/ssa/SsaAdjacentUncertainRead.expected‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ WARNING: Predicate getAFirstUncertainRead has been deprecated and may be removed
1717
| Capture.cs:38:9:38:11 | SSA call def(x) | Capture.cs:40:13:40:13 | access to local variable x |
1818
| Capture.cs:43:9:43:13 | SSA def(x) | Capture.cs:44:11:44:11 | access to local variable x |
1919
| Capture.cs:44:9:44:12 | SSA call def(x) | Capture.cs:45:13:45:13 | access to local variable x |
20-
| Capture.cs:46:9:46:13 | SSA call def(x) | Capture.cs:47:13:47:13 | access to local variable x |
2120
| Capture.cs:50:20:50:20 | SSA param(a) | Capture.cs:54:9:54:9 | access to parameter a |
2221
| Capture.cs:52:16:52:43 | SSA def(b) | Capture.cs:53:9:53:9 | access to local variable b |
2322
| Capture.cs:53:9:53:11 | SSA call def(a) | Capture.cs:54:9:54:9 | access to parameter a |

‎csharp/ql/test/library-tests/dataflow/ssa/SsaCapturedVariableDef.expected‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,8 @@
11
| in | Capture.cs:6:16:6:16 | i | Capture.cs:6:16:6:16 | SSA param(i) | Capture.cs:10:20:27:9 | SSA capture def(i) | Capture.cs:38:9:38:11 | delegate call |
22
| in | Capture.cs:6:16:6:16 | i | Capture.cs:6:16:6:16 | SSA param(i) | Capture.cs:10:20:27:9 | SSA capture def(i) | Capture.cs:44:9:44:12 | call to method M |
3-
| in | Capture.cs:6:16:6:16 | i | Capture.cs:6:16:6:16 | SSA param(i) | Capture.cs:10:20:27:9 | SSA capture def(i) | Capture.cs:46:9:46:13 | call to method M2 |
43
| in | Capture.cs:8:13:8:13 | x | Capture.cs:8:13:8:17 | SSA def(x) | Capture.cs:19:24:23:13 | SSA capture def(x) | Capture.cs:38:9:38:11 | delegate call |
54
| in | Capture.cs:8:13:8:13 | x | Capture.cs:15:13:15:17 | SSA def(x) | Capture.cs:19:24:23:13 | SSA capture def(x) | Capture.cs:25:13:25:15 | delegate call |
65
| in | Capture.cs:8:13:8:13 | x | Capture.cs:43:9:43:13 | SSA def(x) | Capture.cs:19:24:23:13 | SSA capture def(x) | Capture.cs:44:9:44:12 | call to method M |
7-
| in | Capture.cs:8:13:8:13 | x | Capture.cs:43:9:43:13 | SSA def(x) | Capture.cs:19:24:23:13 | SSA capture def(x) | Capture.cs:46:9:46:13 | call to method M2 |
86
| in | Capture.cs:17:17:17:17 | y | Capture.cs:17:17:17:21 | SSA def(y) | Capture.cs:19:24:23:13 | SSA capture def(y) | Capture.cs:25:13:25:15 | delegate call |
97
| in | Capture.cs:59:13:59:13 | i | Capture.cs:59:13:59:17 | SSA def(i) | Capture.cs:60:31:60:38 | SSA capture def(i) | Capture.cs:61:9:61:25 | call to method Select |
108
| in | Capture.cs:67:13:67:13 | c | Capture.cs:67:13:67:19 | SSA def(c) | Capture.cs:68:32:68:49 | SSA capture def(c) | Capture.cs:68:18:68:50 | call to method Where |
@@ -31,7 +29,6 @@
3129
| out | Capture.cs:6:16:6:16 | i | Capture.cs:13:13:13:17 | SSA def(i) | Capture.cs:38:9:38:11 | SSA call def(i) | Capture.cs:38:9:38:11 | delegate call |
3230
| out | Capture.cs:8:13:8:13 | x | Capture.cs:15:13:15:17 | SSA def(x) | Capture.cs:38:9:38:11 | SSA call def(x) | Capture.cs:38:9:38:11 | delegate call |
3331
| out | Capture.cs:8:13:8:13 | x | Capture.cs:15:13:15:17 | SSA def(x) | Capture.cs:44:9:44:12 | SSA call def(x) | Capture.cs:44:9:44:12 | call to method M |
34-
| out | Capture.cs:8:13:8:13 | x | Capture.cs:15:13:15:17 | SSA def(x) | Capture.cs:46:9:46:13 | SSA call def(x) | Capture.cs:46:9:46:13 | call to method M2 |
3532
| out | Capture.cs:29:13:29:13 | z | Capture.cs:30:28:30:32 | SSA def(z) | Capture.cs:32:9:32:11 | SSA call def(z) | Capture.cs:32:9:32:11 | delegate call |
3633
| out | Capture.cs:50:20:50:20 | a | Capture.cs:52:28:52:40 | SSA def(a) | Capture.cs:53:9:53:11 | SSA call def(a) | Capture.cs:53:9:53:11 | delegate call |
3734
| out | Capture.cs:59:13:59:13 | i | Capture.cs:60:36:60:38 | SSA def(i) | Capture.cs:61:9:61:25 | SSA call def(i) | Capture.cs:61:9:61:25 | call to method Select |

‎csharp/ql/test/library-tests/dataflow/ssa/SsaDef.expected‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@
88
| Capture.cs:8:13:8:13 | x | Capture.cs:38:9:38:11 | SSA call def(x) |
99
| Capture.cs:8:13:8:13 | x | Capture.cs:43:9:43:13 | SSA def(x) |
1010
| Capture.cs:8:13:8:13 | x | Capture.cs:44:9:44:12 | SSA call def(x) |
11-
| Capture.cs:8:13:8:13 | x | Capture.cs:46:9:46:13 | SSA call def(x) |
1211
| Capture.cs:10:16:10:16 | a | Capture.cs:10:16:27:9 | SSA def(a) |
1312
| Capture.cs:17:17:17:17 | y | Capture.cs:17:17:17:21 | SSA def(y) |
1413
| Capture.cs:17:17:17:17 | y | Capture.cs:19:24:23:13 | SSA capture def(y) |

0 commit comments

Comments
 (0)