Skip to content

Commit 7080b25

Browse files
hvitvedhvitved
authored
Merge pull request github#5715 from hvitved/csharp/ssa/perf-tweaks
C#: A few minor SSA performance tweaks
2 parents def62e8 + 9128ec7 commit 7080b25

File tree

4 files changed

+120
-48
lines changed

4 files changed

+120
-48
lines changed

‎csharp/ql/src/semmle/code/cil/internal/SsaImplCommon.qll

Lines changed: 30 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -316,6 +316,15 @@ private module SsaDefReaches {
316316
)
317317
}
318318

319+
/**
320+
* Holds if the reference to `def` at index `i` in basic block `bb` is the
321+
* last reference to `v` inside `bb`.
322+
*/
323+
pragma[noinline]
324+
predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
325+
ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v)
326+
}
327+
319328
predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v) {
320329
exists(ssaDefRank(def, v, bb, _, _))
321330
}
@@ -351,8 +360,7 @@ private module SsaDefReaches {
351360
*/
352361
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
353362
varBlockReaches(def, bb1, bb2) and
354-
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1 and
355-
variableRead(bb2, i2, _, _)
363+
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1
356364
}
357365
}
358366

@@ -434,15 +442,22 @@ predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2
434442
bb2 = bb1
435443
)
436444
or
437-
exists(SourceVariable v | ssaDefRank(def, v, bb1, i1, _) = maxSsaRefRank(bb1, v)) and
445+
lastSsaRef(def, _, bb1, i1) and
438446
defAdjacentRead(def, bb1, bb2, i2)
439447
}
440448

449+
pragma[noinline]
450+
private predicate adjacentDefRead(
451+
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v
452+
) {
453+
adjacentDefRead(def, bb1, i1, bb2, i2) and
454+
v = def.getSourceVariable()
455+
}
456+
441457
private predicate adjacentDefReachesRead(
442458
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
443459
) {
444-
adjacentDefRead(def, bb1, i1, bb2, i2) and
445-
exists(SourceVariable v | v = def.getSourceVariable() |
460+
exists(SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
446461
ssaRef(bb1, i1, v, SsaDef())
447462
or
448463
variableRead(bb1, i1, v, true)
@@ -475,17 +490,19 @@ predicate adjacentDefNoUncertainReads(Definition def, BasicBlock bb1, int i1, Ba
475490
*/
476491
pragma[nomagic]
477492
predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
478-
exists(int rnk, SourceVariable v, int j | rnk = ssaDefRank(def, v, bb, i, _) |
493+
exists(SourceVariable v |
479494
// Next reference to `v` inside `bb` is a write
480-
next.definesAt(v, bb, j) and
481-
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
495+
exists(int rnk, int j |
496+
rnk = ssaDefRank(def, v, bb, i, _) and
497+
next.definesAt(v, bb, j) and
498+
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
499+
)
482500
or
483501
// Can reach a write using one or more steps
484-
rnk = maxSsaRefRank(bb, v) and
502+
lastSsaRef(def, v, bb, i) and
485503
exists(BasicBlock bb2 |
486504
varBlockReaches(def, bb, bb2) and
487-
next.definesAt(v, bb2, j) and
488-
1 = ssaRefRank(bb2, j, v, SsaDef())
505+
1 = ssaDefRank(next, v, bb2, _, SsaDef())
489506
)
490507
)
491508
}
@@ -539,7 +556,8 @@ pragma[nomagic]
539556
predicate lastRef(Definition def, BasicBlock bb, int i) {
540557
lastRefRedef(def, bb, i, _)
541558
or
542-
exists(SourceVariable v | ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v) |
559+
lastSsaRef(def, _, bb, i) and
560+
(
543561
// Can reach exit directly
544562
bb instanceof ExitBasicBlock
545563
or

‎csharp/ql/src/semmle/code/csharp/controlflow/internal/pressa/SsaImplCommon.qll

Lines changed: 30 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -316,6 +316,15 @@ private module SsaDefReaches {
316316
)
317317
}
318318

319+
/**
320+
* Holds if the reference to `def` at index `i` in basic block `bb` is the
321+
* last reference to `v` inside `bb`.
322+
*/
323+
pragma[noinline]
324+
predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
325+
ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v)
326+
}
327+
319328
predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v) {
320329
exists(ssaDefRank(def, v, bb, _, _))
321330
}
@@ -351,8 +360,7 @@ private module SsaDefReaches {
351360
*/
352361
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
353362
varBlockReaches(def, bb1, bb2) and
354-
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1 and
355-
variableRead(bb2, i2, _, _)
363+
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1
356364
}
357365
}
358366

@@ -434,15 +442,22 @@ predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2
434442
bb2 = bb1
435443
)
436444
or
437-
exists(SourceVariable v | ssaDefRank(def, v, bb1, i1, _) = maxSsaRefRank(bb1, v)) and
445+
lastSsaRef(def, _, bb1, i1) and
438446
defAdjacentRead(def, bb1, bb2, i2)
439447
}
440448

449+
pragma[noinline]
450+
private predicate adjacentDefRead(
451+
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v
452+
) {
453+
adjacentDefRead(def, bb1, i1, bb2, i2) and
454+
v = def.getSourceVariable()
455+
}
456+
441457
private predicate adjacentDefReachesRead(
442458
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
443459
) {
444-
adjacentDefRead(def, bb1, i1, bb2, i2) and
445-
exists(SourceVariable v | v = def.getSourceVariable() |
460+
exists(SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
446461
ssaRef(bb1, i1, v, SsaDef())
447462
or
448463
variableRead(bb1, i1, v, true)
@@ -475,17 +490,19 @@ predicate adjacentDefNoUncertainReads(Definition def, BasicBlock bb1, int i1, Ba
475490
*/
476491
pragma[nomagic]
477492
predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
478-
exists(int rnk, SourceVariable v, int j | rnk = ssaDefRank(def, v, bb, i, _) |
493+
exists(SourceVariable v |
479494
// Next reference to `v` inside `bb` is a write
480-
next.definesAt(v, bb, j) and
481-
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
495+
exists(int rnk, int j |
496+
rnk = ssaDefRank(def, v, bb, i, _) and
497+
next.definesAt(v, bb, j) and
498+
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
499+
)
482500
or
483501
// Can reach a write using one or more steps
484-
rnk = maxSsaRefRank(bb, v) and
502+
lastSsaRef(def, v, bb, i) and
485503
exists(BasicBlock bb2 |
486504
varBlockReaches(def, bb, bb2) and
487-
next.definesAt(v, bb2, j) and
488-
1 = ssaRefRank(bb2, j, v, SsaDef())
505+
1 = ssaDefRank(next, v, bb2, _, SsaDef())
489506
)
490507
)
491508
}
@@ -539,7 +556,8 @@ pragma[nomagic]
539556
predicate lastRef(Definition def, BasicBlock bb, int i) {
540557
lastRefRedef(def, bb, i, _)
541558
or
542-
exists(SourceVariable v | ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v) |
559+
lastSsaRef(def, _, bb, i) and
560+
(
543561
// Can reach exit directly
544562
bb instanceof ExitBasicBlock
545563
or

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

Lines changed: 30 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -316,6 +316,15 @@ private module SsaDefReaches {
316316
)
317317
}
318318

319+
/**
320+
* Holds if the reference to `def` at index `i` in basic block `bb` is the
321+
* last reference to `v` inside `bb`.
322+
*/
323+
pragma[noinline]
324+
predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
325+
ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v)
326+
}
327+
319328
predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v) {
320329
exists(ssaDefRank(def, v, bb, _, _))
321330
}
@@ -351,8 +360,7 @@ private module SsaDefReaches {
351360
*/
352361
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
353362
varBlockReaches(def, bb1, bb2) and
354-
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1 and
355-
variableRead(bb2, i2, _, _)
363+
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1
356364
}
357365
}
358366

@@ -434,15 +442,22 @@ predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2
434442
bb2 = bb1
435443
)
436444
or
437-
exists(SourceVariable v | ssaDefRank(def, v, bb1, i1, _) = maxSsaRefRank(bb1, v)) and
445+
lastSsaRef(def, _, bb1, i1) and
438446
defAdjacentRead(def, bb1, bb2, i2)
439447
}
440448

449+
pragma[noinline]
450+
private predicate adjacentDefRead(
451+
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v
452+
) {
453+
adjacentDefRead(def, bb1, i1, bb2, i2) and
454+
v = def.getSourceVariable()
455+
}
456+
441457
private predicate adjacentDefReachesRead(
442458
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
443459
) {
444-
adjacentDefRead(def, bb1, i1, bb2, i2) and
445-
exists(SourceVariable v | v = def.getSourceVariable() |
460+
exists(SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
446461
ssaRef(bb1, i1, v, SsaDef())
447462
or
448463
variableRead(bb1, i1, v, true)
@@ -475,17 +490,19 @@ predicate adjacentDefNoUncertainReads(Definition def, BasicBlock bb1, int i1, Ba
475490
*/
476491
pragma[nomagic]
477492
predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
478-
exists(int rnk, SourceVariable v, int j | rnk = ssaDefRank(def, v, bb, i, _) |
493+
exists(SourceVariable v |
479494
// Next reference to `v` inside `bb` is a write
480-
next.definesAt(v, bb, j) and
481-
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
495+
exists(int rnk, int j |
496+
rnk = ssaDefRank(def, v, bb, i, _) and
497+
next.definesAt(v, bb, j) and
498+
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
499+
)
482500
or
483501
// Can reach a write using one or more steps
484-
rnk = maxSsaRefRank(bb, v) and
502+
lastSsaRef(def, v, bb, i) and
485503
exists(BasicBlock bb2 |
486504
varBlockReaches(def, bb, bb2) and
487-
next.definesAt(v, bb2, j) and
488-
1 = ssaRefRank(bb2, j, v, SsaDef())
505+
1 = ssaDefRank(next, v, bb2, _, SsaDef())
489506
)
490507
)
491508
}
@@ -539,7 +556,8 @@ pragma[nomagic]
539556
predicate lastRef(Definition def, BasicBlock bb, int i) {
540557
lastRefRedef(def, bb, i, _)
541558
or
542-
exists(SourceVariable v | ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v) |
559+
lastSsaRef(def, _, bb, i) and
560+
(
543561
// Can reach exit directly
544562
bb instanceof ExitBasicBlock
545563
or

‎csharp/ql/src/semmle/code/csharp/dataflow/internal/basessa/SsaImplCommon.qll

Lines changed: 30 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -316,6 +316,15 @@ private module SsaDefReaches {
316316
)
317317
}
318318

319+
/**
320+
* Holds if the reference to `def` at index `i` in basic block `bb` is the
321+
* last reference to `v` inside `bb`.
322+
*/
323+
pragma[noinline]
324+
predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
325+
ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v)
326+
}
327+
319328
predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v) {
320329
exists(ssaDefRank(def, v, bb, _, _))
321330
}
@@ -351,8 +360,7 @@ private module SsaDefReaches {
351360
*/
352361
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
353362
varBlockReaches(def, bb1, bb2) and
354-
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1 and
355-
variableRead(bb2, i2, _, _)
363+
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1
356364
}
357365
}
358366

@@ -434,15 +442,22 @@ predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2
434442
bb2 = bb1
435443
)
436444
or
437-
exists(SourceVariable v | ssaDefRank(def, v, bb1, i1, _) = maxSsaRefRank(bb1, v)) and
445+
lastSsaRef(def, _, bb1, i1) and
438446
defAdjacentRead(def, bb1, bb2, i2)
439447
}
440448

449+
pragma[noinline]
450+
private predicate adjacentDefRead(
451+
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v
452+
) {
453+
adjacentDefRead(def, bb1, i1, bb2, i2) and
454+
v = def.getSourceVariable()
455+
}
456+
441457
private predicate adjacentDefReachesRead(
442458
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
443459
) {
444-
adjacentDefRead(def, bb1, i1, bb2, i2) and
445-
exists(SourceVariable v | v = def.getSourceVariable() |
460+
exists(SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
446461
ssaRef(bb1, i1, v, SsaDef())
447462
or
448463
variableRead(bb1, i1, v, true)
@@ -475,17 +490,19 @@ predicate adjacentDefNoUncertainReads(Definition def, BasicBlock bb1, int i1, Ba
475490
*/
476491
pragma[nomagic]
477492
predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
478-
exists(int rnk, SourceVariable v, int j | rnk = ssaDefRank(def, v, bb, i, _) |
493+
exists(SourceVariable v |
479494
// Next reference to `v` inside `bb` is a write
480-
next.definesAt(v, bb, j) and
481-
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
495+
exists(int rnk, int j |
496+
rnk = ssaDefRank(def, v, bb, i, _) and
497+
next.definesAt(v, bb, j) and
498+
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
499+
)
482500
or
483501
// Can reach a write using one or more steps
484-
rnk = maxSsaRefRank(bb, v) and
502+
lastSsaRef(def, v, bb, i) and
485503
exists(BasicBlock bb2 |
486504
varBlockReaches(def, bb, bb2) and
487-
next.definesAt(v, bb2, j) and
488-
1 = ssaRefRank(bb2, j, v, SsaDef())
505+
1 = ssaDefRank(next, v, bb2, _, SsaDef())
489506
)
490507
)
491508
}
@@ -539,7 +556,8 @@ pragma[nomagic]
539556
predicate lastRef(Definition def, BasicBlock bb, int i) {
540557
lastRefRedef(def, bb, i, _)
541558
or
542-
exists(SourceVariable v | ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v) |
559+
lastSsaRef(def, _, bb, i) and
560+
(
543561
// Can reach exit directly
544562
bb instanceof ExitBasicBlock
545563
or

0 commit comments

Comments
 (0)