Skip to content

Commit c0868bc

Browse files
semmle-qlcisemmle-qlci
authored
Merge pull request #708 from hvitved/csharp/ssa-read-splitting
Approved by calumgrant
2 parents 8174fb5 + 2427f0a commit c0868bc

File tree

13 files changed

+276
-40
lines changed

13 files changed

+276
-40
lines changed

‎csharp/ql/src/semmle/code/csharp/Assignable.qll‎

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,10 @@ class AssignableRead extends AssignableAccess {
100100
* - The read of `this.Field` on line 11 is next to the read on line 10.
101101
*/
102102
AssignableRead getANextRead() {
103-
Ssa::Internal::adjacentReadPairSameVar(this, result)
103+
forex(ControlFlow::Node cfn |
104+
cfn = result.getAControlFlowNode() |
105+
Ssa::Internal::adjacentReadPairSameVar(this.getAControlFlowNode(), cfn)
106+
)
104107
}
105108

106109
/**
@@ -502,9 +505,12 @@ class AssignableDefinition extends TAssignableDefinition {
502505
* `AssignableRead.getANextRead()`.
503506
*/
504507
AssignableRead getAFirstRead() {
505-
exists(Ssa::ExplicitDefinition def |
506-
def.getADefinition() = this |
507-
result = def.getAFirstRead()
508+
forex(ControlFlow::Node cfn |
509+
cfn = result.getAControlFlowNode() |
510+
exists(Ssa::ExplicitDefinition def |
511+
result = def.getAFirstReadAtNode(cfn) |
512+
this = def.getADefinition()
513+
)
508514
)
509515
}
510516

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

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -423,20 +423,20 @@ private Ssa::Definition getAnUltimateDefinition(Ssa::Definition def) {
423423
}
424424

425425
/**
426-
* Holds if SSA definition `def` can reach a read `ar`, without passing
426+
* Holds if SSA definition `def` can reach a read at `cfn`, without passing
427427
* through an intermediate dereference that always (`always = true`) or
428428
* maybe (`always = false`) throws a null reference exception.
429429
*/
430-
private predicate defReaches(Ssa::Definition def, AssignableRead ar, boolean always) {
431-
ar = def.getAFirstRead() and
430+
private predicate defReaches(Ssa::Definition def, ControlFlow::Node cfn, boolean always) {
431+
exists(def.getAFirstReadAtNode(cfn)) and
432432
(always = true or always = false)
433433
or
434-
exists(AssignableRead mid |
434+
exists(ControlFlow::Node mid |
435435
defReaches(def, mid, always) |
436-
ar = mid.getANextRead() and
436+
Ssa::Internal::adjacentReadPairSameVar(mid, cfn) and
437437
not mid = any(Dereference d |
438438
if always = true then d.isAlwaysNull(def.getSourceVariable()) else d.isMaybeNull(def, _, _, _, _)
439-
)
439+
).getAControlFlowNode()
440440
)
441441
}
442442

@@ -528,7 +528,7 @@ class Dereference extends G::DereferenceableExpr {
528528
*/
529529
predicate isFirstAlwaysNull(Ssa::SourceVariable v) {
530530
this.isAlwaysNull(v) and
531-
defReaches(v.getAnSsaDefinition(), this, true)
531+
defReaches(v.getAnSsaDefinition(), this.getAControlFlowNode(), true)
532532
}
533533

534534
/**
@@ -551,6 +551,6 @@ class Dereference extends G::DereferenceableExpr {
551551
*/
552552
predicate isFirstMaybeNull(Ssa::Definition def, SourcePathNode source, SinkPathNode sink, string msg, Element reason) {
553553
this.isMaybeNull(def, source, sink, msg, reason) and
554-
defReaches(def, this, false)
554+
defReaches(def, this.getAControlFlowNode(), false)
555555
}
556556
}

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

Lines changed: 87 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -760,16 +760,16 @@ module Ssa {
760760

761761
private cached module Cached {
762762
/**
763-
* Holds if `read` is a last read of the non-trivial SSA definition `def`.
764-
* That is, `read` can reach the end of the enclosing callable, or another
763+
* Holds if `cfn` is a last read of the non-trivial SSA definition `def`.
764+
* That is, `cfn` can reach the end of the enclosing callable, or another
765765
* SSA definition for the underlying source variable, without passing through
766766
* another read.
767767
*/
768768
cached
769-
predicate lastRead(TrackedDefinition def, AssignableRead read) {
769+
predicate lastRead(TrackedDefinition def, ControlFlow::Node cfn) {
770770
exists(TrackedVar v, BasicBlock bb, int i, int rnk |
771-
read = def.getARead() and
772-
variableRead(bb, i, v, read.getAControlFlowNode(), _) and
771+
exists(def.getAReadAtNode(cfn)) and
772+
variableRead(bb, i, v, cfn, _) and
773773
rnk = ssaRefRank(bb, i, v, SsaRead()) |
774774
// Next reference to `v` inside `bb` is a write
775775
rnk + 1 = ssaRefRank(bb, _, v, SsaDef())
@@ -854,27 +854,29 @@ module Ssa {
854854
}
855855

856856
/**
857-
* Holds if the value defined at non-trivial SSA definition `def` can reach `read`
858-
* without passing through any other read.
857+
* Holds if the value defined at non-trivial SSA definition `def` can reach a
858+
* read at `cfn`, without passing through any other read.
859859
*/
860860
cached
861-
predicate firstReadSameVar(TrackedDefinition def, AssignableRead read) {
861+
predicate firstReadSameVar(TrackedDefinition def, ControlFlow::Node cfn) {
862862
exists(TrackedVar v, BasicBlock b1, int i1, BasicBlock b2, int i2 |
863863
adjacentVarRefs(v, b1, i1, b2, i2) and
864864
definesAt(def, b1, i1, v) and
865-
variableRead(b2, i2, v, read.getAControlFlowNode(), _)
865+
variableRead(b2, i2, v, cfn, _)
866866
)
867867
}
868868

869869
/**
870-
* INTERNAL: Use `AssignableRead.getANextRead()` instead.
870+
* Holds if the read at `cfn2` is a read of the same SSA definition as the
871+
* read at `cfn1`, and `cfn2` can be reached from `cfn1` without passing
872+
* through another read.
871873
*/
872874
cached
873-
predicate adjacentReadPairSameVar(AssignableRead read1, AssignableRead read2) {
875+
predicate adjacentReadPairSameVar(ControlFlow::Node cfn1, ControlFlow::Node cfn2) {
874876
exists(TrackedVar v, BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
875877
adjacentVarRefs(v, bb1, i1, bb2, i2) and
876-
variableRead(bb1, i1, v, read1.getAControlFlowNode(), _) and
877-
variableRead(bb2, i2, v, read2.getAControlFlowNode(), _)
878+
variableRead(bb1, i1, v, cfn1, _) and
879+
variableRead(bb2, i2, v, cfn2, _)
878880
)
879881
}
880882
}
@@ -2074,8 +2076,45 @@ module Ssa {
20742076
* Subsequent reads can be found by following the steps defined by
20752077
* `AssignableRead.getANextRead()`.
20762078
*/
2077-
AssignableRead getAFirstRead() {
2078-
firstReadSameVar(this, result)
2079+
AssignableRead getAFirstRead() { result = this.getAFirstReadAtNode(_) }
2080+
2081+
/**
2082+
* Gets a read of the source variable underlying this SSA definition at
2083+
* control flow node `cfn` that can be reached from this SSA definition
2084+
* without passing through any other SSA definition or read. Example:
2085+
*
2086+
* ```
2087+
* int Field;
2088+
*
2089+
* void SetField(int i) {
2090+
* this.Field = i;
2091+
* Use(this.Field);
2092+
* if (i > 0)
2093+
* this.Field = i - 1;
2094+
* else if (i < 0)
2095+
* SetField(1);
2096+
* Use(this.Field);
2097+
* Use(this.Field);
2098+
* }
2099+
* ```
2100+
*
2101+
* - The read of `i` on line 4 can be reached from the explicit SSA
2102+
* definition (wrapping an implicit entry definition) on line 3.
2103+
* - The reads of `i` on lines 6 and 7 are not the first reads of any SSA
2104+
* definition.
2105+
* - The read of `this.Field` on line 5 can be reached from the explicit SSA
2106+
* definition on line 4.
2107+
* - The read of `this.Field` on line 10 can be reached from the phi node
2108+
* between lines 9 and 10.
2109+
* - The read of `this.Field` on line 11 is not the first read of any SSA
2110+
* definition.
2111+
*
2112+
* Subsequent reads can be found by following the steps defined by
2113+
* `AssignableRead.getANextRead()`.
2114+
*/
2115+
AssignableRead getAFirstReadAtNode(ControlFlow::Node cfn) {
2116+
firstReadSameVar(this, cfn) and
2117+
result.getAControlFlowNode() = cfn
20792118
}
20802119

20812120
/**
@@ -2106,8 +2145,39 @@ module Ssa {
21062145
* - The read of `this.Field` on line 11 is a last read of the phi node
21072146
* between lines 9 and 10.
21082147
*/
2109-
AssignableRead getALastRead() {
2110-
lastRead(this, result)
2148+
AssignableRead getALastRead() { result = this.getALastReadAtNode(_) }
2149+
2150+
/**
2151+
* Gets a last read of the source variable underlying this SSA definition at
2152+
* control flow node `cfn`. That is, a read that can reach the end of the
2153+
* enclosing callable, or another SSA definition for the source variable,
2154+
* without passing through any other read. Example:
2155+
*
2156+
* ```
2157+
* int Field;
2158+
*
2159+
* void SetField(int i) {
2160+
* this.Field = i;
2161+
* Use(this.Field);
2162+
* if (i > 0)
2163+
* this.Field = i - 1;
2164+
* else if (i < 0)
2165+
* SetField(1);
2166+
* Use(this.Field);
2167+
* Use(this.Field);
2168+
* }
2169+
* ```
2170+
*
2171+
* - The reads of `i` on lines 7 and 8 are the last reads for the implicit
2172+
* parameter definition on line 3.
2173+
* - The read of `this.Field` on line 5 is a last read of the definition on
2174+
* line 4.
2175+
* - The read of `this.Field` on line 11 is a last read of the phi node
2176+
* between lines 9 and 10.
2177+
*/
2178+
AssignableRead getALastReadAtNode(ControlFlow::Node cfn) {
2179+
lastRead(this, cfn) and
2180+
result.getAControlFlowNode() = cfn
21112181
}
21122182

21132183
/**

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,13 @@
135135
| Properties.cs:74:23:74:23 | a | Properties.cs:74:23:74:54 | Action a = ... | Properties.cs:77:9:77:9 | access to local variable a |
136136
| Properties.cs:75:23:75:23 | b | Properties.cs:75:23:75:35 | Action b = ... | Properties.cs:80:9:80:9 | access to local variable b |
137137
| Properties.cs:106:37:106:37 | p | Properties.cs:106:37:106:37 | p | Properties.cs:106:42:106:42 | access to parameter p |
138+
| Splitting.cs:3:18:3:18 | b | Splitting.cs:3:18:3:18 | b | Splitting.cs:6:13:6:13 | access to parameter b |
139+
| Splitting.cs:5:13:5:13 | x | Splitting.cs:10:13:10:19 | ... = ... | Splitting.cs:11:13:11:13 | access to local variable x |
140+
| Splitting.cs:22:18:22:18 | b | Splitting.cs:22:18:22:18 | b | Splitting.cs:25:13:25:13 | access to parameter b |
141+
| Splitting.cs:24:13:24:13 | x | Splitting.cs:29:13:29:19 | ... = ... | Splitting.cs:30:13:30:13 | access to local variable x |
142+
| Splitting.cs:24:13:24:13 | x | Splitting.cs:32:9:32:15 | ... = ... | Splitting.cs:33:9:33:9 | access to local variable x |
143+
| Splitting.cs:42:18:42:18 | b | Splitting.cs:42:18:42:18 | b | Splitting.cs:45:13:45:13 | access to parameter b |
144+
| Splitting.cs:44:13:44:13 | x | Splitting.cs:49:13:49:19 | ... = ... | Splitting.cs:50:13:50:13 | access to local variable x |
138145
| Test.cs:3:9:3:13 | field | Test.cs:57:9:57:17 | ... = ... | Test.cs:58:13:58:17 | access to field field |
139146
| Test.cs:5:15:5:20 | param1 | Test.cs:5:15:5:20 | param1 | Test.cs:11:13:11:18 | access to parameter param1 |
140147
| Test.cs:5:67:5:72 | param2 | Test.cs:5:67:5:72 | param2 | Test.cs:39:27:39:32 | access to parameter param2 |

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

Lines changed: 33 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,19 @@
11
import csharp
22
import ControlFlow::Internal
33

4-
query predicate defReadInconsistency(
4+
class CallableWithSplitting extends Callable {
5+
CallableWithSplitting() {
6+
this = any(SplitControlFlowElement e).getEnclosingCallable()
7+
}
8+
}
9+
10+
query
11+
predicate defReadInconsistency(
512
AssignableRead ar, Expr e, PreSsa::SimpleAssignable a, boolean b
613
) {
14+
// Exclude definitions in callables with CFG splitting, as SSA definitions may be
15+
// very different from pre-SSA definitions
16+
not ar.getEnclosingCallable() instanceof CallableWithSplitting and
717
exists(AssignableDefinition def | e = def.getExpr() |
818
b = true and
919
exists(PreSsa::Definition ssaDef | ssaDef.getAssignable() = a |
@@ -31,21 +41,33 @@ query predicate defReadInconsistency(
3141
query predicate readReadInconsistency(
3242
LocalScopeVariableRead read1, LocalScopeVariableRead read2, PreSsa::SimpleAssignable a, boolean b
3343
) {
34-
b = true and
35-
a = read1.getTarget() and
36-
PreSsa::adjacentReadPairSameVar(read1, read2) and
37-
not Ssa::Internal::adjacentReadPairSameVar(read1, read2)
38-
or
39-
b = false and
40-
a = read1.getTarget() and
41-
Ssa::Internal::adjacentReadPairSameVar(read1, read2) and
42-
read1.getTarget() instanceof PreSsa::SimpleAssignable and
43-
not PreSsa::adjacentReadPairSameVar(read1, read2)
44+
// Exclude definitions in callables with CFG splitting, as SSA definitions may be
45+
// very different from pre-SSA definitions
46+
not read1.getEnclosingCallable() instanceof CallableWithSplitting and
47+
(
48+
b = true and
49+
a = read1.getTarget() and
50+
PreSsa::adjacentReadPairSameVar(read1, read2) and
51+
not Ssa::Internal::adjacentReadPairSameVar(read1.getAControlFlowNode(), read2.getAControlFlowNode())
52+
or
53+
b = false and
54+
a = read1.getTarget() and
55+
Ssa::Internal::adjacentReadPairSameVar(read1.getAControlFlowNode(), read2.getAControlFlowNode()) and
56+
read1.getTarget() instanceof PreSsa::SimpleAssignable and
57+
not PreSsa::adjacentReadPairSameVar(read1, read2) and
58+
// Exclude split CFG elements because SSA may be more precise than pre-SSA
59+
// in those cases
60+
not read1 instanceof SplitControlFlowElement and
61+
not read2 instanceof SplitControlFlowElement
62+
)
4463
}
4564

4665
query predicate phiInconsistency(
4766
ControlFlowElement cfe, Expr e, PreSsa::SimpleAssignable a, boolean b
4867
) {
68+
// Exclude definitions in callables with CFG splitting, as SSA definitions may be
69+
// very different from pre-SSA definitions
70+
not cfe.getEnclosingCallable() instanceof CallableWithSplitting and
4971
exists(AssignableDefinition adef | e = adef.getExpr() |
5072
b = true and
5173
exists(PreSsa::Definition def | a = def.getAssignable() |

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,14 @@
9898
| Properties.cs:104:16:104:20 | Props | Properties.cs:114:20:114:35 | access to field Props | Properties.cs:115:21:115:36 | access to field Props |
9999
| Properties.cs:104:16:104:20 | Props | Properties.cs:115:21:115:30 | access to field Props | Properties.cs:116:17:116:26 | access to field Props |
100100
| Properties.cs:104:16:104:20 | Props | Properties.cs:115:21:115:36 | access to field Props | Properties.cs:116:17:116:32 | access to field Props |
101+
| Splitting.cs:3:18:3:18 | b | Splitting.cs:6:13:6:13 | access to parameter b | Splitting.cs:15:13:15:13 | access to parameter b |
102+
| Splitting.cs:5:13:5:13 | x | Splitting.cs:13:9:13:9 | access to local variable x | Splitting.cs:14:9:14:9 | access to local variable x |
103+
| Splitting.cs:5:13:5:13 | x | Splitting.cs:14:9:14:9 | access to local variable x | Splitting.cs:17:13:17:13 | access to local variable x |
104+
| Splitting.cs:22:18:22:18 | b | Splitting.cs:25:13:25:13 | access to parameter b | Splitting.cs:35:13:35:13 | access to parameter b |
105+
| Splitting.cs:24:13:24:13 | x | Splitting.cs:33:9:33:9 | access to local variable x | Splitting.cs:34:9:34:9 | access to local variable x |
106+
| Splitting.cs:24:13:24:13 | x | Splitting.cs:34:9:34:9 | access to local variable x | Splitting.cs:37:13:37:13 | access to local variable x |
107+
| Splitting.cs:42:18:42:18 | b | Splitting.cs:45:13:45:13 | access to parameter b | Splitting.cs:52:13:52:13 | access to parameter b |
108+
| Splitting.cs:44:13:44:13 | x | Splitting.cs:54:9:54:9 | access to local variable x | Splitting.cs:55:9:55:9 | access to local variable x |
101109
| Test.cs:8:13:8:13 | x | Test.cs:25:16:25:16 | access to local variable x | Test.cs:25:16:25:16 | access to local variable x |
102110
| Test.cs:9:13:9:13 | y | Test.cs:25:20:25:20 | access to local variable y | Test.cs:31:13:31:13 | access to local variable y |
103111
| Test.cs:9:13:9:13 | y | Test.cs:25:20:25:20 | access to local variable y | Test.cs:43:20:43:20 | access to local variable y |

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,8 @@
3333
| Properties.cs:33:19:33:22 | Properties.stat | Properties.cs:50:9:50:17 | SSA phi(Properties.stat) | Properties.cs:49:17:49:32 | SSA call def(Properties.stat) |
3434
| Properties.cs:61:23:61:23 | i | Properties.cs:63:16:63:16 | SSA phi(i) | Properties.cs:61:23:61:23 | SSA param(i) |
3535
| Properties.cs:61:23:61:23 | i | Properties.cs:63:16:63:16 | SSA phi(i) | Properties.cs:63:16:63:18 | SSA def(i) |
36+
| Splitting.cs:44:13:44:13 | x | Splitting.cs:54:9:54:21 | SSA phi(x) | Splitting.cs:46:13:46:19 | [b (line 42): true] SSA def(x) |
37+
| Splitting.cs:44:13:44:13 | x | Splitting.cs:54:9:54:21 | SSA phi(x) | Splitting.cs:49:13:49:19 | [b (line 42): false] SSA def(x) |
3638
| Test.cs:5:15:5:20 | param1 | Test.cs:25:16:25:16 | SSA phi(param1) | Test.cs:5:15:5:20 | SSA param(param1) |
3739
| Test.cs:5:15:5:20 | param1 | Test.cs:25:16:25:16 | SSA phi(param1) | Test.cs:27:17:27:24 | SSA def(param1) |
3840
| Test.cs:5:15:5:20 | param1 | Test.cs:33:9:33:19 | SSA phi(param1) | Test.cs:25:16:25:16 | SSA phi(param1) |

‎csharp/ql/test/library-tests/dataflow/ssa/Splitting.cs‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
class Splitting
2+
{
3+
void M1(bool b)
4+
{
5+
var x = "";
6+
if (b)
7+
x = "a";
8+
else
9+
{
10+
x = "b";
11+
x.ToString();
12+
}
13+
x.ToString();
14+
x.ToString();
15+
if (b)
16+
{
17+
x.ToString();
18+
x = "c";
19+
}
20+
}
21+
22+
void M2(bool b)
23+
{
24+
var x = "";
25+
if (b)
26+
x = "a";
27+
else
28+
{
29+
x = "b";
30+
x.ToString();
31+
}
32+
x = "c";
33+
x.ToString();
34+
x.ToString();
35+
if (b)
36+
{
37+
x.ToString();
38+
x = "d";
39+
}
40+
}
41+
42+
void M3(bool b)
43+
{
44+
var x = "";
45+
if (b)
46+
x = "a";
47+
else
48+
{
49+
x = "b";
50+
x.ToString();
51+
}
52+
if (b)
53+
b = false;
54+
x.ToString();
55+
x.ToString();
56+
}
57+
}

0 commit comments

Comments
 (0)