hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-22 23:35:14 +02:00
Code Issues Packages Projects Releases Wiki Activity

SSA: Fold getImmediateBasicBlockDominator into loop-invariant predicate.

Browse Source
This commit is contained in:
Anders Schack-Mulligen
2025-02-17 12:36:18 +01:00
parent 77ccff6be8
commit 7e441d9eca
1 changed files with 16 additions and 9 deletions
Download Patch File Download Diff File Expand all files Collapse all files

25
shared/ssa/codeql/ssa/Ssa.qll
View File

@@ -424,8 +424,13 @@ module Make<LocationSig Location, InputSig<Location> Input> {
rnk = ssaRefRank(bb, _, v, SsaActualRead())
}
/**
* Holds if `v` is live at the end of basic block `bb` with the same value as at
* the end of the immediate dominator, `idom`, of `bb`.
*/
pragma[nomagic]
private predicate liveThrough(BasicBlock bb, SourceVariable v) {
private predicate liveThrough(BasicBlock idom, BasicBlock bb, SourceVariable v) {
idom = getImmediateBasicBlockDominator(bb) and
liveAtExit(bb, v) and
not ssaRef(bb, _, v, SsaDef())
}
@@ -443,14 +448,16 @@ module Make<LocationSig Location, InputSig<Location> Input> {
liveAtExit(bb, v)
)
or
// The construction of SSA form ensures that each read of a variable is
// dominated by its definition. An SSA definition therefore reaches a
// control flow node if it is the _closest_ SSA definition that dominates
// the node. If two definitions dominate a node then one must dominate the
// other, so therefore the definition of _closest_ is given by the dominator
// tree. Thus, reaching definitions can be calculated in terms of dominance.
ssaDefReachesEndOfBlock(getImmediateBasicBlockDominator(bb), def, pragma[only_bind_into](v)) and
liveThrough(bb, pragma[only_bind_into](v))
exists(BasicBlock idom |
// The construction of SSA form ensures that each read of a variable is
// dominated by its definition. An SSA definition therefore reaches a
// control flow node if it is the _closest_ SSA definition that dominates
// the node. If two definitions dominate a node then one must dominate the
// other, so therefore the definition of _closest_ is given by the dominator
// tree. Thus, reaching definitions can be calculated in terms of dominance.
ssaDefReachesEndOfBlock(idom, def, v) and
liveThrough(idom, bb, v)
)
}
/**