@@ -75,14 +75,18 @@ class SubBasicBlock extends ControlFlowNodeBase {
7575 * `bb`, where `bb` is equal to `getBasicBlock()`.
7676 */
7777 int getPosInBasicBlock ( BasicBlock bb ) {
78- exists ( int nodePos , int rnk |
79- bb = this .( ControlFlowNode ) .getBasicBlock ( ) and
80- this = bb .getNode ( nodePos ) and
81- nodePos = rank [ rnk ] ( int i | exists ( SubBasicBlock n | n = bb .getNode ( i ) ) ) and
78+ exists ( int thisIndexInBB , int rnk |
79+ thisIndexInBB = this .getIndexInBasicBlock ( bb ) and
80+ thisIndexInBB = rank [ rnk ] ( int i | i = any ( SubBasicBlock n ) .getIndexInBasicBlock ( bb ) ) and
8281 result = rnk - 1
8382 )
8483 }
8584
85+ pragma [ noinline]
86+ private int getIndexInBasicBlock ( BasicBlock bb ) {
87+ this = bb .getNode ( result )
88+ }
89+
8690 /** Gets a successor in the control-flow graph of `SubBasicBlock`s. */
8791 SubBasicBlock getASuccessor ( ) {
8892 this .lastInBB ( ) and
@@ -98,16 +102,22 @@ class SubBasicBlock extends ControlFlowNodeBase {
98102 * start from 0, and the node at position 0 always exists and compares equal
99103 * to `this`.
100104 */
105+ pragma [ nomagic]
101106 ControlFlowNode getNode ( int pos ) {
102- exists ( BasicBlock bb | bb = this .getBasicBlock ( ) |
103- exists ( int thisPos | this = bb .getNode ( thisPos ) |
104- result = bb .getNode ( thisPos + pos ) and
105- pos >= 0 and
106- pos < this .getNumberOfNodes ( )
107+ exists ( BasicBlock bb |
108+ exists ( int outerPos |
109+ result = bb .getNode ( outerPos ) and
110+ pos = outerPosToInnerPos ( bb , outerPos )
107111 )
108112 )
109113 }
110114
115+ pragma [ nomagic]
116+ private int outerPosToInnerPos ( BasicBlock bb , int posInBB ) {
117+ posInBB = result + this .getIndexInBasicBlock ( bb ) and
118+ result = [ 0 .. this .getNumberOfNodes ( ) - 1 ]
119+ }
120+
111121 /** Gets a control-flow node in this `SubBasicBlock`. */
112122 ControlFlowNode getANode ( ) {
113123 result = this .getNode ( _)
@@ -147,14 +157,20 @@ class SubBasicBlock extends ControlFlowNodeBase {
147157 * Gets the number of control-flow nodes in this `SubBasicBlock`. There is
148158 * always at least one.
149159 */
160+ pragma [ noopt]
150161 int getNumberOfNodes ( ) {
151162 exists ( BasicBlock bb | bb = this .getBasicBlock ( ) |
152163 exists ( int thisPos | this = bb .getNode ( thisPos ) |
153- this .lastInBB ( ) and
154- result = bb .length ( ) - thisPos
164+ exists ( int bbLength |
165+ this .lastInBB ( ) and
166+ bbLength = bb .length ( ) and
167+ result = bbLength - thisPos
168+ )
155169 or
156- exists ( SubBasicBlock succ , int succPos |
157- succ .getPosInBasicBlock ( bb ) = this .getPosInBasicBlock ( bb ) + 1 and
170+ exists ( SubBasicBlock succ , int succPos , int thisRank , int succRank |
171+ thisRank = this .getPosInBasicBlock ( bb ) and
172+ succRank = thisRank + 1 and
173+ succRank = succ .getPosInBasicBlock ( bb ) and
158174 bb .getNode ( succPos ) = succ and
159175 result = succPos - thisPos
160176 )
0 commit comments