Merge pull request #5715 from hvitved/csharp/ssa/perf-tweaks

C#: A few minor SSA performance tweaks
This commit is contained in:
Tom Hvitved
2021-04-21 09:59:12 +02:00
committed by GitHub
4 changed files with 120 additions and 48 deletions

View File

@@ -316,6 +316,15 @@ private module SsaDefReaches {
)
}
/**
* Holds if the reference to `def` at index `i` in basic block `bb` is the
* last reference to `v` inside `bb`.
*/
pragma[noinline]
predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v)
}
predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v) {
exists(ssaDefRank(def, v, bb, _, _))
}
@@ -351,8 +360,7 @@ private module SsaDefReaches {
*/
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
varBlockReaches(def, bb1, bb2) and
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1 and
variableRead(bb2, i2, _, _)
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1
}
}
@@ -434,15 +442,22 @@ predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2
bb2 = bb1
)
or
exists(SourceVariable v | ssaDefRank(def, v, bb1, i1, _) = maxSsaRefRank(bb1, v)) and
lastSsaRef(def, _, bb1, i1) and
defAdjacentRead(def, bb1, bb2, i2)
}
pragma[noinline]
private predicate adjacentDefRead(
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v
) {
adjacentDefRead(def, bb1, i1, bb2, i2) and
v = def.getSourceVariable()
}
private predicate adjacentDefReachesRead(
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
) {
adjacentDefRead(def, bb1, i1, bb2, i2) and
exists(SourceVariable v | v = def.getSourceVariable() |
exists(SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
ssaRef(bb1, i1, v, SsaDef())
or
variableRead(bb1, i1, v, true)
@@ -475,17 +490,19 @@ predicate adjacentDefNoUncertainReads(Definition def, BasicBlock bb1, int i1, Ba
*/
pragma[nomagic]
predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
exists(int rnk, SourceVariable v, int j | rnk = ssaDefRank(def, v, bb, i, _) |
exists(SourceVariable v |
// Next reference to `v` inside `bb` is a write
next.definesAt(v, bb, j) and
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
exists(int rnk, int j |
rnk = ssaDefRank(def, v, bb, i, _) and
next.definesAt(v, bb, j) and
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
)
or
// Can reach a write using one or more steps
rnk = maxSsaRefRank(bb, v) and
lastSsaRef(def, v, bb, i) and
exists(BasicBlock bb2 |
varBlockReaches(def, bb, bb2) and
next.definesAt(v, bb2, j) and
1 = ssaRefRank(bb2, j, v, SsaDef())
1 = ssaDefRank(next, v, bb2, _, SsaDef())
)
)
}
@@ -539,7 +556,8 @@ pragma[nomagic]
predicate lastRef(Definition def, BasicBlock bb, int i) {
lastRefRedef(def, bb, i, _)
or
exists(SourceVariable v | ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v) |
lastSsaRef(def, _, bb, i) and
(
// Can reach exit directly
bb instanceof ExitBasicBlock
or

View File

@@ -316,6 +316,15 @@ private module SsaDefReaches {
)
}
/**
* Holds if the reference to `def` at index `i` in basic block `bb` is the
* last reference to `v` inside `bb`.
*/
pragma[noinline]
predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v)
}
predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v) {
exists(ssaDefRank(def, v, bb, _, _))
}
@@ -351,8 +360,7 @@ private module SsaDefReaches {
*/
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
varBlockReaches(def, bb1, bb2) and
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1 and
variableRead(bb2, i2, _, _)
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1
}
}
@@ -434,15 +442,22 @@ predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2
bb2 = bb1
)
or
exists(SourceVariable v | ssaDefRank(def, v, bb1, i1, _) = maxSsaRefRank(bb1, v)) and
lastSsaRef(def, _, bb1, i1) and
defAdjacentRead(def, bb1, bb2, i2)
}
pragma[noinline]
private predicate adjacentDefRead(
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v
) {
adjacentDefRead(def, bb1, i1, bb2, i2) and
v = def.getSourceVariable()
}
private predicate adjacentDefReachesRead(
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
) {
adjacentDefRead(def, bb1, i1, bb2, i2) and
exists(SourceVariable v | v = def.getSourceVariable() |
exists(SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
ssaRef(bb1, i1, v, SsaDef())
or
variableRead(bb1, i1, v, true)
@@ -475,17 +490,19 @@ predicate adjacentDefNoUncertainReads(Definition def, BasicBlock bb1, int i1, Ba
*/
pragma[nomagic]
predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
exists(int rnk, SourceVariable v, int j | rnk = ssaDefRank(def, v, bb, i, _) |
exists(SourceVariable v |
// Next reference to `v` inside `bb` is a write
next.definesAt(v, bb, j) and
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
exists(int rnk, int j |
rnk = ssaDefRank(def, v, bb, i, _) and
next.definesAt(v, bb, j) and
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
)
or
// Can reach a write using one or more steps
rnk = maxSsaRefRank(bb, v) and
lastSsaRef(def, v, bb, i) and
exists(BasicBlock bb2 |
varBlockReaches(def, bb, bb2) and
next.definesAt(v, bb2, j) and
1 = ssaRefRank(bb2, j, v, SsaDef())
1 = ssaDefRank(next, v, bb2, _, SsaDef())
)
)
}
@@ -539,7 +556,8 @@ pragma[nomagic]
predicate lastRef(Definition def, BasicBlock bb, int i) {
lastRefRedef(def, bb, i, _)
or
exists(SourceVariable v | ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v) |
lastSsaRef(def, _, bb, i) and
(
// Can reach exit directly
bb instanceof ExitBasicBlock
or

View File

@@ -316,6 +316,15 @@ private module SsaDefReaches {
)
}
/**
* Holds if the reference to `def` at index `i` in basic block `bb` is the
* last reference to `v` inside `bb`.
*/
pragma[noinline]
predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v)
}
predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v) {
exists(ssaDefRank(def, v, bb, _, _))
}
@@ -351,8 +360,7 @@ private module SsaDefReaches {
*/
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
varBlockReaches(def, bb1, bb2) and
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1 and
variableRead(bb2, i2, _, _)
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1
}
}
@@ -434,15 +442,22 @@ predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2
bb2 = bb1
)
or
exists(SourceVariable v | ssaDefRank(def, v, bb1, i1, _) = maxSsaRefRank(bb1, v)) and
lastSsaRef(def, _, bb1, i1) and
defAdjacentRead(def, bb1, bb2, i2)
}
pragma[noinline]
private predicate adjacentDefRead(
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v
) {
adjacentDefRead(def, bb1, i1, bb2, i2) and
v = def.getSourceVariable()
}
private predicate adjacentDefReachesRead(
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
) {
adjacentDefRead(def, bb1, i1, bb2, i2) and
exists(SourceVariable v | v = def.getSourceVariable() |
exists(SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
ssaRef(bb1, i1, v, SsaDef())
or
variableRead(bb1, i1, v, true)
@@ -475,17 +490,19 @@ predicate adjacentDefNoUncertainReads(Definition def, BasicBlock bb1, int i1, Ba
*/
pragma[nomagic]
predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
exists(int rnk, SourceVariable v, int j | rnk = ssaDefRank(def, v, bb, i, _) |
exists(SourceVariable v |
// Next reference to `v` inside `bb` is a write
next.definesAt(v, bb, j) and
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
exists(int rnk, int j |
rnk = ssaDefRank(def, v, bb, i, _) and
next.definesAt(v, bb, j) and
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
)
or
// Can reach a write using one or more steps
rnk = maxSsaRefRank(bb, v) and
lastSsaRef(def, v, bb, i) and
exists(BasicBlock bb2 |
varBlockReaches(def, bb, bb2) and
next.definesAt(v, bb2, j) and
1 = ssaRefRank(bb2, j, v, SsaDef())
1 = ssaDefRank(next, v, bb2, _, SsaDef())
)
)
}
@@ -539,7 +556,8 @@ pragma[nomagic]
predicate lastRef(Definition def, BasicBlock bb, int i) {
lastRefRedef(def, bb, i, _)
or
exists(SourceVariable v | ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v) |
lastSsaRef(def, _, bb, i) and
(
// Can reach exit directly
bb instanceof ExitBasicBlock
or

View File

@@ -316,6 +316,15 @@ private module SsaDefReaches {
)
}
/**
* Holds if the reference to `def` at index `i` in basic block `bb` is the
* last reference to `v` inside `bb`.
*/
pragma[noinline]
predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v)
}
predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v) {
exists(ssaDefRank(def, v, bb, _, _))
}
@@ -351,8 +360,7 @@ private module SsaDefReaches {
*/
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
varBlockReaches(def, bb1, bb2) and
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1 and
variableRead(bb2, i2, _, _)
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1
}
}
@@ -434,15 +442,22 @@ predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2
bb2 = bb1
)
or
exists(SourceVariable v | ssaDefRank(def, v, bb1, i1, _) = maxSsaRefRank(bb1, v)) and
lastSsaRef(def, _, bb1, i1) and
defAdjacentRead(def, bb1, bb2, i2)
}
pragma[noinline]
private predicate adjacentDefRead(
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v
) {
adjacentDefRead(def, bb1, i1, bb2, i2) and
v = def.getSourceVariable()
}
private predicate adjacentDefReachesRead(
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
) {
adjacentDefRead(def, bb1, i1, bb2, i2) and
exists(SourceVariable v | v = def.getSourceVariable() |
exists(SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
ssaRef(bb1, i1, v, SsaDef())
or
variableRead(bb1, i1, v, true)
@@ -475,17 +490,19 @@ predicate adjacentDefNoUncertainReads(Definition def, BasicBlock bb1, int i1, Ba
*/
pragma[nomagic]
predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
exists(int rnk, SourceVariable v, int j | rnk = ssaDefRank(def, v, bb, i, _) |
exists(SourceVariable v |
// Next reference to `v` inside `bb` is a write
next.definesAt(v, bb, j) and
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
exists(int rnk, int j |
rnk = ssaDefRank(def, v, bb, i, _) and
next.definesAt(v, bb, j) and
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
)
or
// Can reach a write using one or more steps
rnk = maxSsaRefRank(bb, v) and
lastSsaRef(def, v, bb, i) and
exists(BasicBlock bb2 |
varBlockReaches(def, bb, bb2) and
next.definesAt(v, bb2, j) and
1 = ssaRefRank(bb2, j, v, SsaDef())
1 = ssaDefRank(next, v, bb2, _, SsaDef())
)
)
}
@@ -539,7 +556,8 @@ pragma[nomagic]
predicate lastRef(Definition def, BasicBlock bb, int i) {
lastRefRedef(def, bb, i, _)
or
exists(SourceVariable v | ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v) |
lastSsaRef(def, _, bb, i) and
(
// Can reach exit directly
bb instanceof ExitBasicBlock
or