55import java
66import Dominance
77
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+
821/**
922 * A control-flow node that represents the start of a basic block.
1023 *
1124 * A basic block is a series of nodes with no control-flow branching, which can
1225 * often be treated as a unit in analyses.
1326 */
1427class BasicBlock extends ControlFlowNode {
28+ cached
1529 BasicBlock ( ) {
16- not exists ( this .getAPredecessor ( ) ) and exists ( this .getASuccessor ( ) )
30+ BasicBlockStage:: ref ( ) and
31+ not exists ( this .getAPredecessor ( ) ) and
32+ exists ( this .getASuccessor ( ) )
1733 or
1834 strictcount ( this .getAPredecessor ( ) ) > 1
1935 or
@@ -24,7 +40,10 @@ class BasicBlock extends ControlFlowNode {
2440
2541 /** Gets an immediate successor of this basic block. */
2642 cached
27- BasicBlock getABBSuccessor ( ) { result = this .getLastNode ( ) .getASuccessor ( ) }
43+ BasicBlock getABBSuccessor ( ) {
44+ BasicBlockStage:: ref ( ) and
45+ result = this .getLastNode ( ) .getASuccessor ( )
46+ }
2847
2948 /** Gets an immediate predecessor of this basic block. */
3049 BasicBlock getABBPredecessor ( ) { result .getABBSuccessor ( ) = this }
@@ -35,7 +54,9 @@ class BasicBlock extends ControlFlowNode {
3554 /** Gets the control-flow node at a specific (zero-indexed) position in this basic block. */
3655 cached
3756 ControlFlowNode getNode ( int pos ) {
38- result = this and pos = 0
57+ BasicBlockStage:: ref ( ) and
58+ result = this and
59+ pos = 0
3960 or
4061 exists ( ControlFlowNode mid , int mid_pos | pos = mid_pos + 1 |
4162 this .getNode ( mid_pos ) = mid and
@@ -52,7 +73,10 @@ class BasicBlock extends ControlFlowNode {
5273
5374 /** Gets the number of control-flow nodes contained in this basic block. */
5475 cached
55- int length ( ) { result = strictcount ( this .getANode ( ) ) }
76+ int length ( ) {
77+ BasicBlockStage:: ref ( ) and
78+ result = strictcount ( this .getANode ( ) )
79+ }
5680
5781 /** Holds if this basic block strictly dominates `node`. */
5882 predicate bbStrictlyDominates ( BasicBlock node ) { bbStrictlyDominates ( this , node ) }
0 commit comments