1
1
/**
2
- * This modules provides an implementation of a basic block class based based
3
- * on a control flow graph implementation.
2
+ * This modules provides an implementation of a basic block class based on a
3
+ * control flow graph implementation.
4
4
*
5
5
* INTERNAL use only. This is an experimental API subject to change without
6
6
* notice.
7
7
*/
8
8
9
+ private import codeql.util.Location
10
+
9
11
/** Provides the language-specific input specification. */
10
- signature module InputSig {
12
+ signature module InputSig< LocationSig Location > {
11
13
class SuccessorType ;
12
14
13
15
/** Hold if `t` represents a conditional successor type. */
@@ -16,21 +18,31 @@ signature module InputSig {
16
18
/** The class of control flow nodes. */
17
19
class Node {
18
20
string toString ( ) ;
21
+
22
+ /** Gets the location of this control flow node. */
23
+ Location getLocation ( ) ;
19
24
}
20
25
26
+ /** Gets an immediate successor of this node. */
21
27
Node nodeGetASuccessor ( Node node , SuccessorType t ) ;
22
28
23
- /** Holds if `node` is the beginning of an entry basic block. */
24
- predicate nodeIsEntry ( Node node ) ;
29
+ /**
30
+ * Holds if `node` represents an entry node to be used when calculating
31
+ * dominance.
32
+ */
33
+ predicate nodeIsDominanceEntry ( Node node ) ;
25
34
26
- /** Holds if `node` is the beginning of an entry basic block. */
27
- predicate nodeIsExit ( Node node ) ;
35
+ /**
36
+ * Holds if `node` represents an exit node to be used when calculating
37
+ * post dominance.
38
+ */
39
+ predicate nodeIsPostDominanceExit ( Node node ) ;
28
40
}
29
41
30
42
/**
31
43
* Provides a basic block construction on top of a control flow graph.
32
44
*/
33
- module Make< InputSig Input> {
45
+ module Make< LocationSig Location , InputSig< Location > Input> {
34
46
private import Input
35
47
36
48
final class BasicBlock = BasicBlockImpl ;
@@ -42,13 +54,17 @@ module Make<InputSig Input> {
42
54
/** Holds if this node has more than one predecessor. */
43
55
private predicate nodeIsJoin ( Node node ) { strictcount ( nodeGetAPredecessor ( node , _) ) > 1 }
44
56
57
+ /** Holds if this node has more than one successor. */
45
58
private predicate nodeIsBranch ( Node node ) { strictcount ( nodeGetASuccessor ( node , _) ) > 1 }
46
59
47
60
/**
48
61
* A basic block, that is, a maximal straight-line sequence of control flow nodes
49
62
* without branches or joins.
50
63
*/
51
64
private class BasicBlockImpl extends TBasicBlockStart {
65
+ /** Gets the location of this basic block. */
66
+ Location getLocation ( ) { result = this .getFirstNode ( ) .getLocation ( ) }
67
+
52
68
/** Gets an immediate successor of this basic block, if any. */
53
69
BasicBlock getASuccessor ( ) { result = this .getASuccessor ( _) }
54
70
@@ -64,6 +80,7 @@ module Make<InputSig Input> {
64
80
BasicBlock getAPredecessor ( SuccessorType t ) { result .getASuccessor ( t ) = this }
65
81
66
82
/** Gets the control flow node at a specific (zero-indexed) position in this basic block. */
83
+ cached
67
84
Node getNode ( int pos ) { bbIndex ( this .getFirstNode ( ) , result , pos ) }
68
85
69
86
/** Gets a control flow node in this basic block. */
@@ -166,52 +183,6 @@ module Make<InputSig Input> {
166
183
cached
167
184
newtype TBasicBlock = TBasicBlockStart ( Node cfn ) { startsBB ( cfn ) }
168
185
169
- /** Holds if `cfn` starts a new basic block. */
170
- private predicate startsBB ( Node cfn ) {
171
- not exists ( nodeGetAPredecessor ( cfn , _) ) and exists ( nodeGetASuccessor ( cfn , _) )
172
- or
173
- nodeIsJoin ( cfn )
174
- or
175
- nodeIsBranch ( nodeGetAPredecessor ( cfn , _) )
176
- or
177
- // In cases such as
178
- //
179
- // ```rb
180
- // if x or y
181
- // foo
182
- // else
183
- // bar
184
- // ```
185
- //
186
- // we have a CFG that looks like
187
- //
188
- // x --false--> [false] x or y --false--> bar
189
- // \ |
190
- // --true--> y --false--
191
- // \
192
- // --true--> [true] x or y --true--> foo
193
- //
194
- // and we want to ensure that both `foo` and `bar` start a new basic block.
195
- exists ( nodeGetAPredecessor ( cfn , any ( SuccessorType s | successorTypeIsCondition ( s ) ) ) )
196
- }
197
-
198
- /**
199
- * Holds if `succ` is a control flow successor of `pred` within
200
- * the same basic block.
201
- */
202
- private predicate intraBBSucc ( Node pred , Node succ ) {
203
- succ = nodeGetASuccessor ( pred , _) and
204
- not startsBB ( succ )
205
- }
206
-
207
- /**
208
- * Holds if `bbStart` is the first node in a basic block and `cfn` is the
209
- * `i`th node in the same basic block.
210
- */
211
- cached
212
- predicate bbIndex ( Node bbStart , Node cfn , int i ) =
213
- shortestDistances( startsBB / 1 , intraBBSucc / 2 ) ( bbStart , cfn , i )
214
-
215
186
/**
216
187
* Holds if the first node of basic block `succ` is a control flow
217
188
* successor of the last node of basic block `pred`.
@@ -227,7 +198,7 @@ module Make<InputSig Input> {
227
198
private predicate predBB ( BasicBlock succ , BasicBlock pred ) { succBB ( pred , succ ) }
228
199
229
200
/** Holds if `bb` is an exit basic block that represents normal exit. */
230
- private predicate exitBB ( BasicBlock bb ) { nodeIsExit ( bb .getANode ( ) ) }
201
+ private predicate exitBB ( BasicBlock bb ) { nodeIsPostDominanceExit ( bb .getANode ( ) ) }
231
202
232
203
/** Holds if `dom` is an immediate post-dominator of `bb`. */
233
204
cached
@@ -237,6 +208,51 @@ module Make<InputSig Input> {
237
208
238
209
private import Cached
239
210
211
+ /** Holds if `cfn` starts a new basic block. */
212
+ private predicate startsBB ( Node cfn ) {
213
+ not exists ( nodeGetAPredecessor ( cfn , _) ) and exists ( nodeGetASuccessor ( cfn , _) )
214
+ or
215
+ nodeIsJoin ( cfn )
216
+ or
217
+ nodeIsBranch ( nodeGetAPredecessor ( cfn , _) )
218
+ or
219
+ // In cases such as
220
+ //
221
+ // ```rb
222
+ // if x or y
223
+ // foo
224
+ // else
225
+ // bar
226
+ // ```
227
+ //
228
+ // we have a CFG that looks like
229
+ //
230
+ // x --false--> [false] x or y --false--> bar
231
+ // \ |
232
+ // --true--> y --false--
233
+ // \
234
+ // --true--> [true] x or y --true--> foo
235
+ //
236
+ // and we want to ensure that both `foo` and `bar` start a new basic block.
237
+ exists ( nodeGetAPredecessor ( cfn , any ( SuccessorType s | successorTypeIsCondition ( s ) ) ) )
238
+ }
239
+
240
+ /**
241
+ * Holds if `succ` is a control flow successor of `pred` within
242
+ * the same basic block.
243
+ */
244
+ predicate intraBBSucc ( Node pred , Node succ ) {
245
+ succ = nodeGetASuccessor ( pred , _) and
246
+ not startsBB ( succ )
247
+ }
248
+
249
+ /**
250
+ * Holds if `bbStart` is the first node in a basic block and `cfn` is the
251
+ * `i`th node in the same basic block.
252
+ */
253
+ private predicate bbIndex ( Node bbStart , Node cfn , int i ) =
254
+ shortestDistances( startsBB / 1 , intraBBSucc / 2 ) ( bbStart , cfn , i )
255
+
240
256
/** Holds if `bb` is an entry basic block. */
241
- private predicate entryBB ( BasicBlock bb ) { nodeIsEntry ( bb .getFirstNode ( ) ) }
257
+ private predicate entryBB ( BasicBlock bb ) { nodeIsDominanceEntry ( bb .getFirstNode ( ) ) }
242
258
}
0 commit comments