@@ -32,15 +32,29 @@ private cached module Cached {
3232 startsBasicBlock ( firstInstr )
3333 }
3434
35+ /** Holds if `i2` follows `i1` in a `IRBlock`. */
36+ private predicate adjacentInBlock ( Instruction i1 , Instruction i2 ) {
37+ exists ( GotoEdge edgeKind | i2 = i1 .getSuccessor ( edgeKind ) ) and
38+ not startsBasicBlock ( i2 )
39+ }
40+
41+ /** Gets the index of `i` in its `IRBlock`. */
42+ private int getMemberIndex ( Instruction i ) {
43+ startsBasicBlock ( i ) and
44+ result = 0
45+ or
46+ exists ( Instruction iPrev |
47+ adjacentInBlock ( iPrev , i ) and
48+ result = getMemberIndex ( iPrev ) + 1
49+ )
50+ }
51+
52+ /** Holds if `i` is the `index`th instruction in `block`. */
3553 cached Instruction getInstruction ( TIRBlock block , int index ) {
36- index = 0 and block = MkIRBlock ( result ) or
37- (
38- index > 0 and
39- not startsBasicBlock ( result ) and
40- exists ( Instruction predecessor , GotoEdge edge |
41- predecessor = getInstruction ( block , index - 1 ) and
42- result = predecessor .getSuccessor ( edge )
43- )
54+ exists ( Instruction first |
55+ block = MkIRBlock ( first ) and
56+ index = getMemberIndex ( result ) and
57+ adjacentInBlock * ( first , result )
4458 )
4559 }
4660
0 commit comments