@@ -51,16 +51,6 @@ signature module InputSig<LocationSig Location> {
51
51
module Make< LocationSig Location, InputSig< Location > Input> {
52
52
private import Input
53
53
54
- private Node nodeGetAPredecessor ( Node node , SuccessorType s ) {
55
- nodeGetASuccessor ( result , s ) = node
56
- }
57
-
58
- /** Holds if this node has more than one predecessor. */
59
- private predicate nodeIsJoin ( Node node ) { strictcount ( nodeGetAPredecessor ( node , _) ) > 1 }
60
-
61
- /** Holds if this node has more than one successor. */
62
- private predicate nodeIsBranch ( Node node ) { strictcount ( nodeGetASuccessor ( node , _) ) > 1 }
63
-
64
54
/**
65
55
* A basic block, that is, a maximal straight-line sequence of control flow nodes
66
56
* without branches or joins.
@@ -76,9 +66,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
76
66
BasicBlock getASuccessor ( ) { result = this .getASuccessor ( _) }
77
67
78
68
/** Gets an immediate successor of this basic block of a given type, if any. */
79
- BasicBlock getASuccessor ( SuccessorType t ) {
80
- result .getFirstNode ( ) = nodeGetASuccessor ( this .getLastNode ( ) , t )
81
- }
69
+ BasicBlock getASuccessor ( SuccessorType t ) { bbSuccessor ( this , result , t ) }
82
70
83
71
/** Gets an immediate predecessor of this basic block, if any. */
84
72
BasicBlock getAPredecessor ( ) { result .getASuccessor ( _) = this }
@@ -287,6 +275,16 @@ module Make<LocationSig Location, InputSig<Location> Input> {
287
275
288
276
cached
289
277
private module Cached {
278
+ private Node nodeGetAPredecessor ( Node node , SuccessorType s ) {
279
+ nodeGetASuccessor ( result , s ) = node
280
+ }
281
+
282
+ /** Holds if this node has more than one predecessor. */
283
+ private predicate nodeIsJoin ( Node node ) { strictcount ( nodeGetAPredecessor ( node , _) ) > 1 }
284
+
285
+ /** Holds if this node has more than one successor. */
286
+ private predicate nodeIsBranch ( Node node ) { strictcount ( nodeGetASuccessor ( node , _) ) > 1 }
287
+
290
288
/**
291
289
* Internal representation of basic blocks. A basic block is represented
292
290
* by its first CFG node.
@@ -343,11 +341,19 @@ module Make<LocationSig Location, InputSig<Location> Input> {
343
341
cached
344
342
Node getNode ( BasicBlock bb , int pos ) { bbIndex ( bb .getFirstNode ( ) , result , pos ) }
345
343
344
+ /** Holds if `bb` is an entry basic block. */
345
+ private predicate entryBB ( BasicBlock bb ) { nodeIsDominanceEntry ( bb .getFirstNode ( ) ) }
346
+
347
+ cached
348
+ predicate bbSuccessor ( BasicBlock bb1 , BasicBlock bb2 , SuccessorType t ) {
349
+ bb2 .getFirstNode ( ) = nodeGetASuccessor ( bb1 .getLastNode ( ) , t )
350
+ }
351
+
346
352
/**
347
353
* Holds if the first node of basic block `succ` is a control flow
348
354
* successor of the last node of basic block `pred`.
349
355
*/
350
- private predicate succBB ( BasicBlock pred , BasicBlock succ ) { pred . getASuccessor ( _ ) = succ }
356
+ private predicate succBB ( BasicBlock pred , BasicBlock succ ) { bbSuccessor ( pred , succ , _ ) }
351
357
352
358
/** Holds if `dom` is an immediate dominator of `bb`. */
353
359
cached
@@ -367,7 +373,4 @@ module Make<LocationSig Location, InputSig<Location> Input> {
367
373
}
368
374
369
375
private import Cached
370
-
371
- /** Holds if `bb` is an entry basic block. */
372
- private predicate entryBB ( BasicBlock bb ) { nodeIsDominanceEntry ( bb .getFirstNode ( ) ) }
373
376
}
0 commit comments