@@ -4,52 +4,49 @@ private import powershell
4
4
private import ControlFlowGraph
5
5
private import CfgNodes
6
6
private import SuccessorTypes
7
+ private import internal.ControlFlowGraphImpl as CfgImpl
8
+ private import CfgImpl:: BasicBlocks as BasicBlocksImpl
7
9
8
10
/**
9
11
* A basic block, that is, a maximal straight-line sequence of control flow nodes
10
12
* without branches or joins.
11
13
*/
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 {
16
15
/** Gets an immediate successor of this basic block, if any. */
17
- BasicBlock getASuccessor ( ) { result = this .getASuccessor ( _ ) }
16
+ BasicBlock getASuccessor ( ) { result = super .getASuccessor ( ) }
18
17
19
18
/** 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 ) }
23
20
24
21
/** Gets an immediate predecessor of this basic block, if any. */
25
- BasicBlock getAPredecessor ( ) { result . getASuccessor ( ) = this }
22
+ BasicBlock getAPredecessor ( ) { result = super . getAPredecessor ( ) }
26
23
27
24
/** 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 ) }
29
26
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 ) }
32
29
33
- /** Gets a control flow node in this basic block. */
34
- CfgNode getANode ( ) { result = this .getNode ( _) }
30
+ CfgNode getANode ( ) { result = super .getANode ( ) }
35
31
36
32
/** Gets the first control flow node in this basic block. */
37
- CfgNode getFirstNode ( ) { this = TBasicBlockStart ( result ) }
33
+ CfgNode getFirstNode ( ) { result = super . getFirstNode ( ) }
38
34
39
35
/** 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 ( ) }
44
37
45
38
/**
46
39
* Holds if this basic block immediately dominates basic block `bb`.
47
40
*
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.
51
48
*/
52
- predicate immediatelyDominates ( BasicBlock bb ) { bbIDominates ( this , bb ) }
49
+ predicate immediatelyDominates ( BasicBlock bb ) { super . immediatelyDominates ( bb ) }
53
50
54
51
/**
55
52
* Holds if this basic block strictly dominates basic block `bb`.
@@ -58,42 +55,35 @@ class BasicBlock extends TBasicBlockStart {
58
55
* basic block must go through this basic block (which must be different
59
56
* from `bb`).
60
57
*/
61
- predicate strictlyDominates ( BasicBlock bb ) { bbIDominates + ( this , bb ) }
58
+ predicate strictlyDominates ( BasicBlock bb ) { super . strictlyDominates ( bb ) }
62
59
63
60
/**
64
61
* Holds if this basic block dominates basic block `bb`.
65
62
*
66
63
* That is, all paths reaching basic block `bb` from some entry point
67
64
* basic block must go through this basic block.
68
65
*/
69
- predicate dominates ( BasicBlock bb ) {
70
- bb = this or
71
- this .strictlyDominates ( bb )
72
- }
66
+ predicate dominates ( BasicBlock bb ) { super .dominates ( bb ) }
73
67
74
68
/**
75
69
* Holds if `df` is in the dominance frontier of this basic block.
76
70
* That is, this basic block dominates a predecessor of `df`, but
77
71
* does not dominate `df` itself.
78
72
*/
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 ) }
88
74
89
75
/**
90
76
* Gets the basic block that immediately dominates this basic block, if any.
91
77
*
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.
95
85
*/
96
- BasicBlock getImmediateDominator ( ) { bbIDominates ( result , this ) }
86
+ BasicBlock getImmediateDominator ( ) { result = super . getImmediateDominator ( ) }
97
87
98
88
/**
99
89
* Holds if this basic block strictly post-dominates basic block `bb`.
@@ -102,158 +92,64 @@ class BasicBlock extends TBasicBlockStart {
102
92
* block `bb` must go through this basic block (which must be different
103
93
* from `bb`).
104
94
*/
105
- predicate strictlyPostDominates ( BasicBlock bb ) { bbIPostDominates + ( this , bb ) }
95
+ predicate strictlyPostDominates ( BasicBlock bb ) { super . strictlyPostDominates ( bb ) }
106
96
107
97
/**
108
98
* Holds if this basic block post-dominates basic block `bb`.
109
99
*
110
100
* That is, all paths reaching a normal exit point basic block from basic
111
101
* block `bb` must go through this basic block.
112
102
*/
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 ) }
126
104
}
127
105
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
-
203
106
/**
204
107
* An entry basic block, that is, a basic block whose first node is
205
108
* an entry node.
206
109
*/
207
- class EntryBasicBlock extends BasicBlock {
208
- EntryBasicBlock ( ) { entryBB ( this ) }
209
- }
110
+ final class EntryBasicBlock extends BasicBlock , BasicBlocksImpl:: EntryBasicBlock { }
210
111
211
112
/**
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.
214
115
*/
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 { }
228
117
229
118
/**
230
119
* An exit basic block, that is, a basic block whose last node is
231
120
* an exit node.
232
121
*/
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 ) }
235
127
}
236
128
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 { }
240
131
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 {
241
137
/**
242
138
* Holds if basic block `succ` is immediately controlled by this basic
243
139
* block with conditional value `s`. That is, `succ` is an immediate
244
140
* successor of this block, and `succ` can only be reached from
245
141
* the callable entry point by going via the `s` edge out of this basic block.
246
142
*/
247
143
predicate immediatelyControls ( BasicBlock succ , ConditionalSuccessor s ) {
248
- immediatelyControls ( this , succ , s )
144
+ super . immediatelyControls ( succ , s )
249
145
}
250
146
251
147
/**
252
148
* 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.
255
151
*/
256
152
predicate controls ( BasicBlock controlled , ConditionalSuccessor s ) {
257
- controls ( this , controlled , s )
153
+ super . controls ( controlled , s )
258
154
}
259
155
}
0 commit comments