@@ -4,52 +4,49 @@ private import powershell
44private import ControlFlowGraph
55private import CfgNodes
66private import SuccessorTypes
7+ private import internal.ControlFlowGraphImpl as CfgImpl
8+ private import CfgImpl:: BasicBlocks as BasicBlocksImpl
79
810/**
911 * A basic block, that is, a maximal straight-line sequence of control flow nodes
1012 * without branches or joins.
1113 */
12- class BasicBlock extends TBasicBlockStart {
13- /** Gets the scope of this basic block. */
14- final CfgScope getScope ( ) { result = this .getFirstNode ( ) .getScope ( ) }
15-
14+ final class BasicBlock extends BasicBlocksImpl:: BasicBlock {
1615 /** Gets an immediate successor of this basic block, if any. */
17- BasicBlock getASuccessor ( ) { result = this .getASuccessor ( _ ) }
16+ BasicBlock getASuccessor ( ) { result = super .getASuccessor ( ) }
1817
1918 /** Gets an immediate successor of this basic block of a given type, if any. */
20- BasicBlock getASuccessor ( SuccessorType t ) {
21- result .getFirstNode ( ) = this .getLastNode ( ) .getASuccessor ( t )
22- }
19+ BasicBlock getASuccessor ( SuccessorType t ) { result = super .getASuccessor ( t ) }
2320
2421 /** Gets an immediate predecessor of this basic block, if any. */
25- BasicBlock getAPredecessor ( ) { result . getASuccessor ( ) = this }
22+ BasicBlock getAPredecessor ( ) { result = super . getAPredecessor ( ) }
2623
2724 /** Gets an immediate predecessor of this basic block of a given type, if any. */
28- BasicBlock getAPredecessor ( SuccessorType t ) { result . getASuccessor ( t ) = this }
25+ BasicBlock getAPredecessor ( SuccessorType t ) { result = super . getAPredecessor ( t ) }
2926
30- /** Gets the control flow node at a specific (zero-indexed) position in this basic block. */
31- CfgNode getNode ( int pos ) { bbIndex ( this . getFirstNode ( ) , result , pos ) }
27+ // The overrides below are to use `CfgNode` instead of `CfgImpl::Node`
28+ CfgNode getNode ( int pos ) { result = super . getNode ( pos ) }
3229
33- /** Gets a control flow node in this basic block. */
34- CfgNode getANode ( ) { result = this .getNode ( _) }
30+ CfgNode getANode ( ) { result = super .getANode ( ) }
3531
3632 /** Gets the first control flow node in this basic block. */
37- CfgNode getFirstNode ( ) { this = TBasicBlockStart ( result ) }
33+ CfgNode getFirstNode ( ) { result = super . getFirstNode ( ) }
3834
3935 /** Gets the last control flow node in this basic block. */
40- CfgNode getLastNode ( ) { result = this .getNode ( this .length ( ) - 1 ) }
41-
42- /** Gets the length of this basic block. */
43- int length ( ) { result = strictcount ( this .getANode ( ) ) }
36+ CfgNode getLastNode ( ) { result = super .getLastNode ( ) }
4437
4538 /**
4639 * Holds if this basic block immediately dominates basic block `bb`.
4740 *
48- * That is, all paths reaching basic block `bb` from some entry point
49- * basic block must go through this basic block (which is an immediate
50- * predecessor of `bb`).
41+ * That is, this basic block is the unique basic block satisfying:
42+ * 1. This basic block strictly dominates `bb`
43+ * 2. There exists no other basic block that is strictly dominated by this
44+ * basic block and which strictly dominates `bb`.
45+ *
46+ * All basic blocks, except entry basic blocks, have a unique immediate
47+ * dominator.
5148 */
52- predicate immediatelyDominates ( BasicBlock bb ) { bbIDominates ( this , bb ) }
49+ predicate immediatelyDominates ( BasicBlock bb ) { super . immediatelyDominates ( bb ) }
5350
5451 /**
5552 * Holds if this basic block strictly dominates basic block `bb`.
@@ -58,42 +55,35 @@ class BasicBlock extends TBasicBlockStart {
5855 * basic block must go through this basic block (which must be different
5956 * from `bb`).
6057 */
61- predicate strictlyDominates ( BasicBlock bb ) { bbIDominates + ( this , bb ) }
58+ predicate strictlyDominates ( BasicBlock bb ) { super . strictlyDominates ( bb ) }
6259
6360 /**
6461 * Holds if this basic block dominates basic block `bb`.
6562 *
6663 * That is, all paths reaching basic block `bb` from some entry point
6764 * basic block must go through this basic block.
6865 */
69- predicate dominates ( BasicBlock bb ) {
70- bb = this or
71- this .strictlyDominates ( bb )
72- }
66+ predicate dominates ( BasicBlock bb ) { super .dominates ( bb ) }
7367
7468 /**
7569 * Holds if `df` is in the dominance frontier of this basic block.
7670 * That is, this basic block dominates a predecessor of `df`, but
7771 * does not dominate `df` itself.
7872 */
79- predicate inDominanceFrontier ( BasicBlock df ) {
80- this .dominatesPredecessor ( df ) and
81- not this .strictlyDominates ( df )
82- }
83-
84- /**
85- * Holds if this basic block dominates a predecessor of `df`.
86- */
87- private predicate dominatesPredecessor ( BasicBlock df ) { this .dominates ( df .getAPredecessor ( ) ) }
73+ predicate inDominanceFrontier ( BasicBlock df ) { super .inDominanceFrontier ( df ) }
8874
8975 /**
9076 * Gets the basic block that immediately dominates this basic block, if any.
9177 *
92- * That is, all paths reaching this basic block from some entry point
93- * basic block must go through the result, which is an immediate basic block
94- * predecessor of this basic block.
78+ * That is, the result is the unique basic block satisfying:
79+ * 1. The result strictly dominates this basic block.
80+ * 2. There exists no other basic block that is strictly dominated by the
81+ * result and which strictly dominates this basic block.
82+ *
83+ * All basic blocks, except entry basic blocks, have a unique immediate
84+ * dominator.
9585 */
96- BasicBlock getImmediateDominator ( ) { bbIDominates ( result , this ) }
86+ BasicBlock getImmediateDominator ( ) { result = super . getImmediateDominator ( ) }
9787
9888 /**
9989 * Holds if this basic block strictly post-dominates basic block `bb`.
@@ -102,158 +92,64 @@ class BasicBlock extends TBasicBlockStart {
10292 * block `bb` must go through this basic block (which must be different
10393 * from `bb`).
10494 */
105- predicate strictlyPostDominates ( BasicBlock bb ) { bbIPostDominates + ( this , bb ) }
95+ predicate strictlyPostDominates ( BasicBlock bb ) { super . strictlyPostDominates ( bb ) }
10696
10797 /**
10898 * Holds if this basic block post-dominates basic block `bb`.
10999 *
110100 * That is, all paths reaching a normal exit point basic block from basic
111101 * block `bb` must go through this basic block.
112102 */
113- predicate postDominates ( BasicBlock bb ) {
114- this .strictlyPostDominates ( bb ) or
115- this = bb
116- }
117-
118- /** Holds if this basic block is in a loop in the control flow graph. */
119- predicate inLoop ( ) { this .getASuccessor + ( ) = this }
120-
121- /** Gets a textual representation of this basic block. */
122- string toString ( ) { result = this .getFirstNode ( ) .toString ( ) }
123-
124- /** Gets the location of this basic block. */
125- Location getLocation ( ) { result = this .getFirstNode ( ) .getLocation ( ) }
103+ predicate postDominates ( BasicBlock bb ) { super .postDominates ( bb ) }
126104}
127105
128- cached
129- private module Cached {
130- /** Internal representation of basic blocks. */
131- cached
132- newtype TBasicBlock = TBasicBlockStart ( CfgNode cfn ) { startsBB ( cfn ) }
133-
134- /** Holds if `cfn` starts a new basic block. */
135- private predicate startsBB ( CfgNode cfn ) {
136- not exists ( cfn .getAPredecessor ( ) ) and exists ( cfn .getASuccessor ( ) )
137- or
138- cfn .isJoin ( )
139- or
140- cfn .getAPredecessor ( ) .isBranch ( )
141- or
142- exists ( cfn .getAPredecessor ( any ( SuccessorTypes:: ConditionalSuccessor s ) ) )
143- }
144-
145- /**
146- * Holds if `succ` is a control flow successor of `pred` within
147- * the same basic block.
148- */
149- private predicate intraBBSucc ( CfgNode pred , CfgNode succ ) {
150- succ = pred .getASuccessor ( ) and
151- not startsBB ( succ )
152- }
153-
154- /**
155- * Holds if `cfn` is the `i`th node in basic block `bb`.
156- *
157- * In other words, `i` is the shortest distance from a node `bb`
158- * that starts a basic block to `cfn` along the `intraBBSucc` relation.
159- */
160- cached
161- predicate bbIndex ( CfgNode bbStart , CfgNode cfn , int i ) =
162- shortestDistances( startsBB / 1 , intraBBSucc / 2 ) ( bbStart , cfn , i )
163-
164- /**
165- * Holds if the first node of basic block `succ` is a control flow
166- * successor of the last node of basic block `pred`.
167- */
168- private predicate succBB ( BasicBlock pred , BasicBlock succ ) { succ = pred .getASuccessor ( ) }
169-
170- /** Holds if `dom` is an immediate dominator of `bb`. */
171- cached
172- predicate bbIDominates ( BasicBlock dom , BasicBlock bb ) =
173- idominance( entryBB / 1 , succBB / 2 ) ( _, dom , bb )
174-
175- /** Holds if `pred` is a basic block predecessor of `succ`. */
176- private predicate predBB ( BasicBlock succ , BasicBlock pred ) { succBB ( pred , succ ) }
177-
178- /** Holds if `bb` is an exit basic block that represents normal exit. */
179- private predicate normalExitBB ( BasicBlock bb ) { bb .getANode ( ) .( AnnotatedExitNode ) .isNormal ( ) }
180-
181- /** Holds if `dom` is an immediate post-dominator of `bb`. */
182- cached
183- predicate bbIPostDominates ( BasicBlock dom , BasicBlock bb ) =
184- idominance( normalExitBB / 1 , predBB / 2 ) ( _, dom , bb )
185-
186- cached
187- predicate immediatelyControls ( ConditionBlock cb , BasicBlock succ , ConditionalSuccessor s ) {
188- succ = cb .getASuccessor ( s ) and
189- forall ( BasicBlock pred | pred = succ .getAPredecessor ( ) and pred != cb | succ .dominates ( pred ) )
190- }
191-
192- cached
193- predicate controls ( ConditionBlock cb , BasicBlock controlled , ConditionalSuccessor s ) {
194- exists ( BasicBlock succ | cb .immediatelyControls ( succ , s ) | succ .dominates ( controlled ) )
195- }
196- }
197-
198- private import Cached
199-
200- /** Holds if `bb` is an entry basic block. */
201- private predicate entryBB ( BasicBlock bb ) { bb .getFirstNode ( ) instanceof EntryNode }
202-
203106/**
204107 * An entry basic block, that is, a basic block whose first node is
205108 * an entry node.
206109 */
207- class EntryBasicBlock extends BasicBlock {
208- EntryBasicBlock ( ) { entryBB ( this ) }
209- }
110+ final class EntryBasicBlock extends BasicBlock , BasicBlocksImpl:: EntryBasicBlock { }
210111
211112/**
212- * An annotated exit basic block, that is, a basic block whose last node is
213- * an annotated exit node.
113+ * An annotated exit basic block, that is, a basic block that contains an
114+ * annotated exit node.
214115 */
215- class AnnotatedExitBasicBlock extends BasicBlock {
216- private boolean normal ;
217-
218- AnnotatedExitBasicBlock ( ) {
219- exists ( AnnotatedExitNode n |
220- n = this .getANode ( ) and
221- if n .isNormal ( ) then normal = true else normal = false
222- )
223- }
224-
225- /** Holds if this block represent a normal exit. */
226- final predicate isNormal ( ) { normal = true }
227- }
116+ final class AnnotatedExitBasicBlock extends BasicBlock , BasicBlocksImpl:: AnnotatedExitBasicBlock { }
228117
229118/**
230119 * An exit basic block, that is, a basic block whose last node is
231120 * an exit node.
232121 */
233- class ExitBasicBlock extends BasicBlock {
234- ExitBasicBlock ( ) { this .getLastNode ( ) instanceof ExitNode }
122+ final class ExitBasicBlock extends BasicBlock , BasicBlocksImpl:: ExitBasicBlock { }
123+
124+ /** A basic block with more than one predecessor. */
125+ final class JoinBlock extends BasicBlock , BasicBlocksImpl:: JoinBasicBlock {
126+ JoinBlockPredecessor getJoinBlockPredecessor ( int i ) { result = super .getJoinBlockPredecessor ( i ) }
235127}
236128
237- /** A basic block that terminates in a condition, splitting the subsequent control flow. */
238- class ConditionBlock extends BasicBlock {
239- ConditionBlock ( ) { this .getLastNode ( ) .isCondition ( ) }
129+ /** A basic block that is an immediate predecessor of a join block. */
130+ final class JoinBlockPredecessor extends BasicBlock , BasicBlocksImpl:: JoinPredecessorBasicBlock { }
240131
132+ /**
133+ * A basic block that terminates in a condition, splitting the subsequent
134+ * control flow.
135+ */
136+ final class ConditionBlock extends BasicBlock , BasicBlocksImpl:: ConditionBasicBlock {
241137 /**
242138 * Holds if basic block `succ` is immediately controlled by this basic
243139 * block with conditional value `s`. That is, `succ` is an immediate
244140 * successor of this block, and `succ` can only be reached from
245141 * the callable entry point by going via the `s` edge out of this basic block.
246142 */
247143 predicate immediatelyControls ( BasicBlock succ , ConditionalSuccessor s ) {
248- immediatelyControls ( this , succ , s )
144+ super . immediatelyControls ( succ , s )
249145 }
250146
251147 /**
252148 * Holds if basic block `controlled` is controlled by this basic block with
253- * conditional value `s`. That is, `controlled` can only be reached from
254- * the callable entry point by going via the `s` edge out of this basic block.
149+ * conditional value `s`. That is, `controlled` can only be reached from the
150+ * callable entry point by going via the `s` edge out of this basic block.
255151 */
256152 predicate controls ( BasicBlock controlled , ConditionalSuccessor s ) {
257- controls ( this , controlled , s )
153+ super . controls ( controlled , s )
258154 }
259155}
0 commit comments