Skip to content

Commit bd78e73

Browse files
hvitvedhvitved
committed
C#: Add tests for phi reads
1 parent 81a1fa1 commit bd78e73

File tree

6 files changed

+144
-49
lines changed

6 files changed

+144
-49
lines changed

‎csharp/ql/consistency-queries/SsaConsistency.ql

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
import csharp
2-
import semmle.code.csharp.dataflow.internal.SsaImpl::Consistency
2+
import semmle.code.csharp.dataflow.internal.SsaImpl as Impl
3+
import Impl::Consistency
34
import Ssa
45

56
class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
@@ -10,6 +11,14 @@ class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
1011
}
1112
}
1213

14+
class MyRelevantDefinitionExt extends RelevantDefinitionExt, Impl::DefinitionExt {
15+
override predicate hasLocationInfo(
16+
string filepath, int startline, int startcolumn, int endline, int endcolumn
17+
) {
18+
this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
19+
}
20+
}
21+
1322
query predicate localDeclWithSsaDef(LocalVariableDeclExpr d) {
1423
// Local variables in C# must be initialized before every use, so uninitialized
1524
// local variables should not have an SSA definition, as that would imply that

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

Lines changed: 12 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -138,25 +138,6 @@ module Ssa {
138138
}
139139
}
140140

141-
private string getSplitString(Definition def) {
142-
exists(ControlFlow::BasicBlock bb, int i, ControlFlow::Node cfn |
143-
def.definesAt(_, bb, i) and
144-
result = cfn.(ControlFlow::Nodes::ElementNode).getSplitsString()
145-
|
146-
cfn = bb.getNode(i)
147-
or
148-
not exists(bb.getNode(i)) and
149-
cfn = bb.getFirstNode()
150-
)
151-
}
152-
153-
private string getToStringPrefix(Definition def) {
154-
result = "[" + getSplitString(def) + "] "
155-
or
156-
not exists(getSplitString(def)) and
157-
result = ""
158-
}
159-
160141
/**
161142
* A static single assignment (SSA) definition. Either an explicit variable
162143
* definition (`ExplicitDefinition`), an implicit variable definition
@@ -521,8 +502,8 @@ module Ssa {
521502

522503
override string toString() {
523504
if this.getADefinition() instanceof AssignableDefinitions::ImplicitParameterDefinition
524-
then result = getToStringPrefix(this) + "SSA param(" + this.getSourceVariable() + ")"
525-
else result = getToStringPrefix(this) + "SSA def(" + this.getSourceVariable() + ")"
505+
then result = SsaImpl::getToStringPrefix(this) + "SSA param(" + this.getSourceVariable() + ")"
506+
else result = SsaImpl::getToStringPrefix(this) + "SSA def(" + this.getSourceVariable() + ")"
526507
}
527508

528509
override Location getLocation() { result = ad.getLocation() }
@@ -570,8 +551,12 @@ module Ssa {
570551

571552
override string toString() {
572553
if this.getSourceVariable().getAssignable() instanceof LocalScopeVariable
573-
then result = getToStringPrefix(this) + "SSA capture def(" + this.getSourceVariable() + ")"
574-
else result = getToStringPrefix(this) + "SSA entry def(" + this.getSourceVariable() + ")"
554+
then
555+
result =
556+
SsaImpl::getToStringPrefix(this) + "SSA capture def(" + this.getSourceVariable() + ")"
557+
else
558+
result =
559+
SsaImpl::getToStringPrefix(this) + "SSA entry def(" + this.getSourceVariable() + ")"
575560
}
576561

577562
override Location getLocation() { result = this.getCallable().getLocation() }
@@ -612,7 +597,7 @@ module Ssa {
612597
}
613598

614599
override string toString() {
615-
result = getToStringPrefix(this) + "SSA call def(" + this.getSourceVariable() + ")"
600+
result = SsaImpl::getToStringPrefix(this) + "SSA call def(" + this.getSourceVariable() + ")"
616601
}
617602

618603
override Location getLocation() { result = this.getCall().getLocation() }
@@ -640,7 +625,8 @@ module Ssa {
640625
final Definition getQualifierDefinition() { result = q }
641626

642627
override string toString() {
643-
result = getToStringPrefix(this) + "SSA qualifier def(" + this.getSourceVariable() + ")"
628+
result =
629+
SsaImpl::getToStringPrefix(this) + "SSA qualifier def(" + this.getSourceVariable() + ")"
644630
}
645631

646632
override Location getLocation() { result = this.getQualifierDefinition().getLocation() }
@@ -682,7 +668,7 @@ module Ssa {
682668
}
683669

684670
override string toString() {
685-
result = getToStringPrefix(this) + "SSA phi(" + this.getSourceVariable() + ")"
671+
result = SsaImpl::getToStringPrefix(this) + "SSA phi(" + this.getSourceVariable() + ")"
686672
}
687673

688674
/*

‎csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll

Lines changed: 77 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,23 @@ private module SsaInput implements SsaImplCommon::InputSig {
4949
}
5050
}
5151

52-
import SsaImplCommon::Make<SsaInput>
52+
private import SsaImplCommon::Make<SsaInput> as Impl
53+
54+
class Definition = Impl::Definition;
55+
56+
class WriteDefinition = Impl::WriteDefinition;
57+
58+
class UncertainWriteDefinition = Impl::UncertainWriteDefinition;
59+
60+
class PhiNode = Impl::PhiNode;
61+
62+
module Consistency = Impl::Consistency;
63+
64+
module ExposedForTestingOnly {
65+
predicate ssaDefReachesReadExt = Impl::ssaDefReachesReadExt/4;
66+
67+
predicate phiHasInputFromBlockExt = Impl::phiHasInputFromBlockExt/3;
68+
}
5369

5470
/**
5571
* Holds if the `i`th node of basic block `bb` reads source variable `v`.
@@ -1072,7 +1088,7 @@ private predicate adjacentDefRead(
10721088
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2,
10731089
SsaInput::SourceVariable v
10741090
) {
1075-
adjacentDefRead(def, bb1, i1, bb2, i2) and
1091+
Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and
10761092
v = def.getSourceVariable()
10771093
}
10781094

@@ -1088,7 +1104,7 @@ private predicate adjacentDefReachesRead(
10881104
exists(SsaInput::BasicBlock bb3, int i3 |
10891105
adjacentDefReachesRead(def, bb1, i1, bb3, i3) and
10901106
SsaInput::variableRead(bb3, i3, _, false) and
1091-
adjacentDefRead(def, bb3, i3, bb2, i2)
1107+
Impl::adjacentDefRead(def, bb3, i3, bb2, i2)
10921108
)
10931109
}
10941110

@@ -1111,11 +1127,11 @@ private predicate adjacentDefReachesUncertainRead(
11111127
/** Same as `lastRefRedef`, but skips uncertain reads. */
11121128
pragma[nomagic]
11131129
private predicate lastRefSkipUncertainReads(Definition def, SsaInput::BasicBlock bb, int i) {
1114-
lastRef(def, bb, i) and
1130+
Impl::lastRef(def, bb, i) and
11151131
not SsaInput::variableRead(bb, i, def.getSourceVariable(), false)
11161132
or
11171133
exists(SsaInput::BasicBlock bb0, int i0 |
1118-
lastRef(def, bb0, i0) and
1134+
Impl::lastRef(def, bb0, i0) and
11191135
adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
11201136
)
11211137
}
@@ -1237,7 +1253,7 @@ private module Cached {
12371253
v = def.getSourceVariable() and
12381254
capturedReadIn(_, _, v, edef.getSourceVariable(), c, additionalCalls) and
12391255
def = def0.getAnUltimateDefinition() and
1240-
ssaDefReachesRead(_, def0, bb, i) and
1256+
Impl::ssaDefReachesRead(_, def0, bb, i) and
12411257
capturedReadIn(bb, i, v, _, _, _) and
12421258
c = bb.getNode(i)
12431259
)
@@ -1264,18 +1280,18 @@ private module Cached {
12641280

12651281
cached
12661282
predicate isLiveAtEndOfBlock(Definition def, ControlFlow::BasicBlock bb) {
1267-
ssaDefReachesEndOfBlock(bb, def, _)
1283+
Impl::ssaDefReachesEndOfBlock(bb, def, _)
12681284
}
12691285

12701286
cached
1271-
Definition phiHasInputFromBlock(PhiNode phi, ControlFlow::BasicBlock bb) {
1272-
phiHasInputFromBlock(phi, result, bb)
1287+
Definition phiHasInputFromBlock(Ssa::PhiNode phi, ControlFlow::BasicBlock bb) {
1288+
Impl::phiHasInputFromBlock(phi, result, bb)
12731289
}
12741290

12751291
cached
12761292
AssignableRead getAReadAtNode(Definition def, ControlFlow::Node cfn) {
12771293
exists(Ssa::SourceVariable v, ControlFlow::BasicBlock bb, int i |
1278-
ssaDefReachesRead(v, def, bb, i) and
1294+
Impl::ssaDefReachesRead(v, def, bb, i) and
12791295
variableReadActual(bb, i, v) and
12801296
cfn = bb.getNode(i) and
12811297
result.getAControlFlowNode() = cfn
@@ -1313,11 +1329,11 @@ private module Cached {
13131329
/** Same as `lastRefRedef`, but skips uncertain reads. */
13141330
cached
13151331
predicate lastRefBeforeRedef(Definition def, ControlFlow::BasicBlock bb, int i, Definition next) {
1316-
lastRefRedef(def, bb, i, next) and
1332+
Impl::lastRefRedef(def, bb, i, next) and
13171333
not SsaInput::variableRead(bb, i, def.getSourceVariable(), false)
13181334
or
13191335
exists(SsaInput::BasicBlock bb0, int i0 |
1320-
lastRefRedef(def, bb0, i0, next) and
1336+
Impl::lastRefRedef(def, bb0, i0, next) and
13211337
adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
13221338
)
13231339
}
@@ -1333,7 +1349,7 @@ private module Cached {
13331349

13341350
cached
13351351
Definition uncertainWriteDefinitionInput(UncertainWriteDefinition def) {
1336-
uncertainWriteDefinitionInput(def, result)
1352+
Impl::uncertainWriteDefinitionInput(def, result)
13371353
}
13381354

13391355
cached
@@ -1343,10 +1359,57 @@ private module Cached {
13431359
v = def.getSourceVariable() and
13441360
p = v.getAssignable() and
13451361
def = def0.getAnUltimateDefinition() and
1346-
ssaDefReachesRead(_, def0, bb, i) and
1362+
Impl::ssaDefReachesRead(_, def0, bb, i) and
13471363
outRefExitRead(bb, i, v)
13481364
)
13491365
}
13501366
}
13511367

13521368
import Cached
1369+
1370+
private string getSplitString(DefinitionExt def) {
1371+
exists(ControlFlow::BasicBlock bb, int i, ControlFlow::Node cfn |
1372+
def.definesAt(_, bb, i, _) and
1373+
result = cfn.(ControlFlow::Nodes::ElementNode).getSplitsString()
1374+
|
1375+
cfn = bb.getNode(i)
1376+
or
1377+
not exists(bb.getNode(i)) and
1378+
cfn = bb.getFirstNode()
1379+
)
1380+
}
1381+
1382+
string getToStringPrefix(DefinitionExt def) {
1383+
result = "[" + getSplitString(def) + "] "
1384+
or
1385+
not exists(getSplitString(def)) and
1386+
result = ""
1387+
}
1388+
1389+
/**
1390+
* An extended static single assignment (SSA) definition.
1391+
*
1392+
* This is either a normal SSA definition (`Definition`) or a
1393+
* phi-read node (`PhiReadNode`).
1394+
*
1395+
* Only intended for internal use.
1396+
*/
1397+
class DefinitionExt extends Impl::DefinitionExt {
1398+
override string toString() { result = this.(Ssa::Definition).toString() }
1399+
1400+
/** Gets the location of this definition. */
1401+
Location getLocation() { result = this.(Ssa::Definition).getLocation() }
1402+
}
1403+
1404+
/**
1405+
* A phi-read node.
1406+
*
1407+
* Only intended for internal use.
1408+
*/
1409+
class PhiReadNode extends DefinitionExt, Impl::PhiReadNode {
1410+
override string toString() {
1411+
result = getToStringPrefix(this) + "SSA phi read(" + this.getSourceVariable() + ")"
1412+
}
1413+
1414+
override Location getLocation() { result = this.getBasicBlock().getLocation() }
1415+
}

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

Lines changed: 30 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,30 @@
1-
| DefUse.cs:63:9:63:14 | this.Field2 | DefUse.cs:80:30:80:31 | access to local variable x1 |
2-
| Fields.cs:65:24:65:32 | this.LoopField | Fields.cs:63:16:63:28 | this access |
3-
| Properties.cs:65:24:65:31 | this.LoopProp | Properties.cs:63:16:63:16 | access to parameter i |
4-
| Test.cs:78:13:78:13 | x | Test.cs:90:9:97:9 | if (...) ... |
1+
phiReadNode
2+
| DefUse.cs:80:30:80:31 | SSA phi read(this.Field2) | DefUse.cs:63:9:63:14 | this.Field2 |
3+
| Fields.cs:63:16:63:28 | SSA phi read(this.LoopField) | Fields.cs:65:24:65:32 | this.LoopField |
4+
| Patterns.cs:20:9:38:9 | SSA phi read(o) | Patterns.cs:7:16:7:16 | o |
5+
| Properties.cs:63:16:63:16 | SSA phi read(this.LoopProp) | Properties.cs:65:24:65:31 | this.LoopProp |
6+
| Test.cs:25:16:25:16 | SSA phi read(x) | Test.cs:8:13:8:13 | x |
7+
| Test.cs:90:9:97:9 | SSA phi read(x) | Test.cs:78:13:78:13 | x |
8+
| Test.cs:99:9:99:15 | SSA phi read(x) | Test.cs:78:13:78:13 | x |
9+
phiReadNodeRead
10+
| DefUse.cs:80:30:80:31 | SSA phi read(this.Field2) | DefUse.cs:63:9:63:14 | this.Field2 | DefUse.cs:80:37:80:42 | access to field Field2 |
11+
| Fields.cs:63:16:63:28 | SSA phi read(this.LoopField) | Fields.cs:65:24:65:32 | this.LoopField | Fields.cs:65:24:65:32 | access to field LoopField |
12+
| Patterns.cs:20:9:38:9 | SSA phi read(o) | Patterns.cs:7:16:7:16 | o | Patterns.cs:20:17:20:17 | access to local variable o |
13+
| Properties.cs:63:16:63:16 | SSA phi read(this.LoopProp) | Properties.cs:65:24:65:31 | this.LoopProp | Properties.cs:65:24:65:31 | access to property LoopProp |
14+
| Test.cs:25:16:25:16 | SSA phi read(x) | Test.cs:8:13:8:13 | x | Test.cs:25:16:25:16 | access to local variable x |
15+
| Test.cs:90:9:97:9 | SSA phi read(x) | Test.cs:78:13:78:13 | x | Test.cs:92:17:92:17 | access to local variable x |
16+
| Test.cs:90:9:97:9 | SSA phi read(x) | Test.cs:78:13:78:13 | x | Test.cs:96:17:96:17 | access to local variable x |
17+
| Test.cs:99:9:99:15 | SSA phi read(x) | Test.cs:78:13:78:13 | x | Test.cs:99:13:99:13 | access to local variable x |
18+
| Test.cs:99:9:99:15 | SSA phi read(x) | Test.cs:78:13:78:13 | x | Test.cs:104:17:104:17 | access to local variable x |
19+
phiReadInput
20+
| DefUse.cs:80:30:80:31 | SSA phi read(this.Field2) | DefUse.cs:63:9:63:18 | SSA def(this.Field2) |
21+
| DefUse.cs:80:30:80:31 | SSA phi read(this.Field2) | DefUse.cs:80:30:80:31 | SSA phi read(this.Field2) |
22+
| Fields.cs:63:16:63:28 | SSA phi read(this.LoopField) | Fields.cs:61:17:61:17 | SSA entry def(this.LoopField) |
23+
| Fields.cs:63:16:63:28 | SSA phi read(this.LoopField) | Fields.cs:63:16:63:28 | SSA phi read(this.LoopField) |
24+
| Patterns.cs:20:9:38:9 | SSA phi read(o) | Patterns.cs:7:16:7:23 | SSA def(o) |
25+
| Properties.cs:63:16:63:16 | SSA phi read(this.LoopProp) | Properties.cs:61:17:61:17 | SSA entry def(this.LoopProp) |
26+
| Properties.cs:63:16:63:16 | SSA phi read(this.LoopProp) | Properties.cs:63:16:63:16 | SSA phi read(this.LoopProp) |
27+
| Test.cs:25:16:25:16 | SSA phi read(x) | Test.cs:24:9:24:15 | SSA phi(x) |
28+
| Test.cs:25:16:25:16 | SSA phi read(x) | Test.cs:25:16:25:16 | SSA phi read(x) |
29+
| Test.cs:90:9:97:9 | SSA phi read(x) | Test.cs:78:13:78:17 | SSA def(x) |
30+
| Test.cs:99:9:99:15 | SSA phi read(x) | Test.cs:90:9:97:9 | SSA phi read(x) |

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

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,17 @@
11
import csharp
22
import semmle.code.csharp.dataflow.internal.SsaImpl
3+
import ExposedForTestingOnly
34

4-
from Ssa::SourceVariable v, ControlFlow::BasicBlock bb
5-
where phiReadExposedForTesting(bb, v)
6-
select v, bb
5+
query predicate phiReadNode(PhiReadNode phi, Ssa::SourceVariable v) { phi.getSourceVariable() = v }
6+
7+
query predicate phiReadNodeRead(PhiReadNode phi, Ssa::SourceVariable v, ControlFlow::Node read) {
8+
phi.getSourceVariable() = v and
9+
exists(ControlFlow::BasicBlock bb, int i |
10+
ssaDefReachesReadExt(v, phi, bb, i) and
11+
read = bb.getNode(i)
12+
)
13+
}
14+
15+
query predicate phiReadInput(PhiReadNode phi, DefinitionExt inp) {
16+
phiHasInputFromBlockExt(phi, inp, _)
17+
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,7 @@ void phiReads(bool b1, bool b2, bool b3, bool b4, bool b5, bool b6)
9595
{
9696
use(x);
9797
}
98-
// no phi_use for `x`, because actual use exists in the block
98+
// phi_use for `x`, even though there is an actual use in the block
9999
use(x);
100100

101101

0 commit comments

Comments
 (0)