Add post-dominators.

cpp/ql/src/semmle/code/cpp/controlflow/Dominance.qll

@@ -28,6 +28,13 @@ 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.
  */
@@ -35,12 +42,25 @@ 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`.
@@ -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.
@@ -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.
  */
@@ -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` 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 dom, BasicBlock node) = idominance(bb_exit/1, bb_predecessor/2)(_, dom, node)
+
 /**
  * Holds if `dominator` is a strict dominator of `node` in the control-flow
  * graph of basic blocks. Being strict means that `dominator != node`.
@@ -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
@@ -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
+}