Skip to content

Commit 7ad4a14

Browse files
committed
Cfg: Add dominance predicates to shared ControlFlowNode.
1 parent 4fef3e8 commit 7ad4a14

File tree

1 file changed

+66
-0
lines changed

1 file changed

+66
-0
lines changed

shared/controlflow/codeql/controlflow/ControlFlowGraph.qll

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1784,6 +1784,72 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
17841784
ControlFlowNode getAnExceptionSuccessor() {
17851785
result = this.getASuccessor(any(ExceptionSuccessor t))
17861786
}
1787+
1788+
/**
1789+
* Holds if this node dominates `that` node.
1790+
*
1791+
* That is, all paths reaching `that` node from the callable entry
1792+
* node (`EntryNode`) must go through this node.
1793+
*/
1794+
bindingset[this, that]
1795+
pragma[inline_late]
1796+
predicate dominates(ControlFlowNode that) {
1797+
this.strictlyDominates(that)
1798+
or
1799+
this = that
1800+
}
1801+
1802+
/**
1803+
* Holds if this node strictly dominates `that` node.
1804+
*
1805+
* That is, all paths reaching `that` node from the callable entry
1806+
* node (`EntryNode`) must go through this node (which must be
1807+
* different from `that` node).
1808+
*/
1809+
bindingset[this, that]
1810+
pragma[inline_late]
1811+
predicate strictlyDominates(ControlFlowNode that) {
1812+
this.getBasicBlock().strictlyDominates(that.getBasicBlock())
1813+
or
1814+
exists(BasicBlock bb, int i, int j |
1815+
bb.getNode(i) = this and
1816+
bb.getNode(j) = that and
1817+
i < j
1818+
)
1819+
}
1820+
1821+
/**
1822+
* Holds if this node post-dominates `that` node.
1823+
*
1824+
* That is, all paths reaching the normal callable exit node
1825+
* (`NormalExitNode`) from `that` node must go through this node.
1826+
*/
1827+
bindingset[this, that]
1828+
pragma[inline_late]
1829+
predicate postDominates(ControlFlowNode that) {
1830+
this.strictlyPostDominates(that)
1831+
or
1832+
this = that
1833+
}
1834+
1835+
/**
1836+
* Holds if this node strictly post-dominates `that` node.
1837+
*
1838+
* That is, all paths reaching the normal callable exit node
1839+
* (`NormalExitNode`) from `that` node must go through this node
1840+
* (which must be different from `that` node).
1841+
*/
1842+
bindingset[this, that]
1843+
pragma[inline_late]
1844+
predicate strictlyPostDominates(ControlFlowNode that) {
1845+
this.getBasicBlock().strictlyPostDominates(that.getBasicBlock())
1846+
or
1847+
exists(BasicBlock bb, int i, int j |
1848+
bb.getNode(i) = this and
1849+
bb.getNode(j) = that and
1850+
i > j
1851+
)
1852+
}
17871853
}
17881854

17891855
/** Provides additional classes for interacting with the control flow graph. */

0 commit comments

Comments
 (0)