5
5
import java
6
6
import Dominance
7
7
8
+ cached
9
+ private module BasicBlockStage {
10
+ cached
11
+ predicate ref ( ) { any ( ) }
12
+
13
+ cached
14
+ predicate backref ( ) {
15
+ ( exists ( any ( BasicBlock bb ) .getABBSuccessor ( ) ) implies any ( ) ) and
16
+ ( exists ( any ( BasicBlock bb ) .getNode ( _) ) implies any ( ) ) and
17
+ ( exists ( any ( BasicBlock bb ) .length ( ) ) implies any ( ) )
18
+ }
19
+ }
20
+
8
21
/**
9
22
* A control-flow node that represents the start of a basic block.
10
23
*
11
24
* A basic block is a series of nodes with no control-flow branching, which can
12
25
* often be treated as a unit in analyses.
13
26
*/
14
27
class BasicBlock extends ControlFlowNode {
28
+ cached
15
29
BasicBlock ( ) {
16
- not exists ( this .getAPredecessor ( ) ) and exists ( this .getASuccessor ( ) )
30
+ BasicBlockStage:: ref ( ) and
31
+ not exists ( this .getAPredecessor ( ) ) and
32
+ exists ( this .getASuccessor ( ) )
17
33
or
18
34
strictcount ( this .getAPredecessor ( ) ) > 1
19
35
or
@@ -24,7 +40,10 @@ class BasicBlock extends ControlFlowNode {
24
40
25
41
/** Gets an immediate successor of this basic block. */
26
42
cached
27
- BasicBlock getABBSuccessor ( ) { result = this .getLastNode ( ) .getASuccessor ( ) }
43
+ BasicBlock getABBSuccessor ( ) {
44
+ BasicBlockStage:: ref ( ) and
45
+ result = this .getLastNode ( ) .getASuccessor ( )
46
+ }
28
47
29
48
/** Gets an immediate predecessor of this basic block. */
30
49
BasicBlock getABBPredecessor ( ) { result .getABBSuccessor ( ) = this }
@@ -35,7 +54,9 @@ class BasicBlock extends ControlFlowNode {
35
54
/** Gets the control-flow node at a specific (zero-indexed) position in this basic block. */
36
55
cached
37
56
ControlFlowNode getNode ( int pos ) {
38
- result = this and pos = 0
57
+ BasicBlockStage:: ref ( ) and
58
+ result = this and
59
+ pos = 0
39
60
or
40
61
exists ( ControlFlowNode mid , int mid_pos | pos = mid_pos + 1 |
41
62
this .getNode ( mid_pos ) = mid and
@@ -52,7 +73,10 @@ class BasicBlock extends ControlFlowNode {
52
73
53
74
/** Gets the number of control-flow nodes contained in this basic block. */
54
75
cached
55
- int length ( ) { result = strictcount ( this .getANode ( ) ) }
76
+ int length ( ) {
77
+ BasicBlockStage:: ref ( ) and
78
+ result = strictcount ( this .getANode ( ) )
79
+ }
56
80
57
81
/** Holds if this basic block strictly dominates `node`. */
58
82
predicate bbStrictlyDominates ( BasicBlock node ) { bbStrictlyDominates ( this , node ) }
0 commit comments