@@ -229,18 +229,17 @@ module Make<LocationSig Location, InputSig<Location> Input> {
229
229
}
230
230
231
231
/**
232
- * Holds if variable `v` is live in basic block `bb` at index `i`.
233
- * The rank of `i` is `rnk` as defined by `refRank()`.
232
+ * Holds if variable `v` is live in basic block `bb` at rank `rnk`.
234
233
*/
235
- private predicate liveAtRank ( BasicBlock bb , int i , SourceVariable v , int rnk ) {
236
- exists ( RefKind kind | rnk = refRank ( bb , i , v , kind ) |
234
+ private predicate liveAtRank ( BasicBlock bb , SourceVariable v , int rnk ) {
235
+ exists ( RefKind kind | rnk = refRank ( bb , _ , v , kind ) |
237
236
rnk = maxRefRank ( bb , v ) and
238
237
liveAtExit ( bb , v )
239
238
or
240
239
kind = Read ( )
241
240
or
242
241
exists ( RefKind nextKind |
243
- liveAtRank ( bb , _ , v , rnk + 1 ) and
242
+ liveAtRank ( bb , v , rnk + 1 ) and
244
243
rnk + 1 = refRank ( bb , _, v , nextKind ) and
245
244
nextKind != Write ( true )
246
245
)
@@ -252,7 +251,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
252
251
* index `i` inside basic block `bb`.
253
252
*/
254
253
predicate liveAfterWrite ( BasicBlock bb , int i , SourceVariable v ) {
255
- exists ( int rnk | rnk = refRank ( bb , i , v , Write ( _) ) | liveAtRank ( bb , i , v , rnk ) )
254
+ exists ( int rnk | rnk = refRank ( bb , i , v , Write ( _) ) | liveAtRank ( bb , v , rnk ) )
256
255
}
257
256
}
258
257
0 commit comments