Skip to content

Add post-dominators #541

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jbj merged 2 commits into from
Nov 27, 2018
Merged

Add post-dominators #541

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
bc752e1
Add post-dominators.
kevinbackhouse Nov 24, 2018
4877659
Fix names.
kevinbackhouse Nov 26, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
70 changes: 70 additions & 0 deletions cpp/ql/src/semmle/code/cpp/controlflow/Dominance.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,19 +28,39 @@ predicate functionEntry(ControlFlowNode entry) {
and not hasMultiScopeNode(function))
}

/** Holds if `exit` is the exit node of a function. */
predicate functionExit(ControlFlowNode exit) {
exists (Function function |
function = exit
and not hasMultiScopeNode(function))
}

/**
* Holds if `dest` is an immediate successor of `src` in the control-flow graph.
*/
private predicate nodeSucc(ControlFlowNode src, ControlFlowNode dest) {
src.getASuccessor() = dest
}

/**
* Holds if `pred` is an immediate predecessor of `src` in the control-flow graph.
*/
private predicate nodePred(ControlFlowNode src, ControlFlowNode pred) {
src.getAPredecessor() = pred
}

/**
* Holds if `dominator` is an immediate dominator of `node` in the control-flow
* graph.
*/
predicate iDominates(ControlFlowNode dominator, ControlFlowNode node) = idominance(functionEntry/1,nodeSucc/2)(_, dominator, node)

/**
* Holds if `postDominator` is an immediate post-dominator of `node` in the control-flow
* graph.
*/
predicate iPostDominates(ControlFlowNode postDominator, ControlFlowNode node) = idominance(functionExit/1,nodePred/2)(_, postDominator, node)

/**
* Holds if `dominator` is a strict dominator of `node` in the control-flow
* graph. Being strict means that `dominator != node`.
Expand All @@ -49,6 +69,14 @@ predicate strictlyDominates(ControlFlowNode dominator, ControlFlowNode node) {
iDominates+(dominator, node)
}

/**
* Holds if `postDominator` is a strict post-dominator of `node` in the control-flow
* graph. Being strict means that `postDominator != node`.
*/
predicate strictlyPostDominates(ControlFlowNode postDominator, ControlFlowNode node) {
iPostDominates+(postDominator, node)
}

/**
* Holds if `dominator` is a dominator of `node` in the control-flow graph. This
* is reflexive.
Expand All @@ -57,6 +85,14 @@ predicate dominates(ControlFlowNode dominator, ControlFlowNode node) {
strictlyDominates(dominator, node) or dominator = node
}

/**
* Holds if `postDominator` is a post-dominator of `node` in the control-flow graph. This
* is reflexive.
*/
predicate postDominates(ControlFlowNode postDominator, ControlFlowNode node) {
strictlyPostDominates(postDominator, node) or postDominator = node
}

/*
* Dominance predicates for basic blocks.
*/
Expand All @@ -67,6 +103,25 @@ predicate dominates(ControlFlowNode dominator, ControlFlowNode node) {
*/
predicate bbIDominates(BasicBlock dom, BasicBlock node) = idominance(functionEntry/1, bb_successor/2)(_, dom, node)

/**
* Holds if `pred` is a predecessor of `succ` in the control-flow graph of
* basic blocks.
*/
private predicate bb_predecessor(BasicBlock succ, BasicBlock pred) {
bb_successor(pred, succ)
}

/** Holds if `exit` is an `ExitBasicBlock`. */
private predicate bb_exit(ExitBasicBlock exit) {
any()
}

/**
* Holds if `postDominator` is an immediate post-dominator of `node` in the control-flow
* graph of basic blocks.
*/
predicate bbIPostDominates(BasicBlock pDom, BasicBlock node) = idominance(bb_exit/1, bb_predecessor/2)(_, pDom, node)

/**
* Holds if `dominator` is a strict dominator of `node` in the control-flow
* graph of basic blocks. Being strict means that `dominator != node`.
Expand All @@ -75,6 +130,13 @@ predicate bbStrictlyDominates(BasicBlock dominator, BasicBlock node) {
bbIDominates+(dominator, node)
}

/**
* Holds if `postDominator` is a strict post-dominator of `node` in the control-flow
* graph of basic blocks. Being strict means that `postDominator != node`.
*/
predicate bbStrictlyPostDominates(BasicBlock postDominator, BasicBlock node) {
bbIPostDominates+(postDominator, node)
}

/**
* Holds if `dominator` is a dominator of `node` in the control-flow graph of
Expand All @@ -83,3 +145,11 @@ predicate bbStrictlyDominates(BasicBlock dominator, BasicBlock node) {
predicate bbDominates(BasicBlock dominator, BasicBlock node) {
bbStrictlyDominates(dominator, node) or dominator = node
}

/**
* Holds if `postDominator` is a post-dominator of `node` in the control-flow graph of
* basic blocks. This is reflexive.
*/
predicate bbPostDominates(BasicBlock postDominator, BasicBlock node) {
bbStrictlyPostDominates(postDominator, node) or postDominator = node
}