@@ -122,17 +122,25 @@ private cached module Internal {
122122 }
123123 or TPhi ( ReachableJoinBlock bb , SsaSourceVariable v ) {
124124 liveAtEntry ( bb , v ) and
125- exists ( ReachableBasicBlock defbb , SsaDefinition def |
126- def .definesAt ( defbb , _, v ) and
127- bb .inDominanceFrontierOf ( defbb )
128- )
125+ inDefDominanceFrontier ( bb , v )
129126 }
130127 or TRefinement ( ReachableBasicBlock bb , int i , GuardControlFlowNode guard , SsaSourceVariable v ) {
131128 bb .getNode ( i ) = guard and
132129 guard .getTest ( ) .( Refinement ) .getRefinedVar ( ) = v and
133130 liveAtEntry ( bb , v )
134131 }
135132
133+ /**
134+ * Holds if `bb` is in the dominance frontier of a block containing a definition of `v`.
135+ */
136+ pragma [ noinline]
137+ private predicate inDefDominanceFrontier ( ReachableJoinBlock bb , SsaSourceVariable v ) {
138+ exists ( ReachableBasicBlock defbb , SsaDefinition def |
139+ def .definesAt ( defbb , _, v ) and
140+ bb .inDominanceFrontierOf ( defbb )
141+ )
142+ }
143+
136144 /**
137145 * Holds if `v` is a captured variable which is declared in `declContainer` and read in
138146 * `useContainer`.
@@ -216,6 +224,13 @@ private cached module Internal {
216224 ref ( bb , i , v , tp )
217225 }
218226
227+ /**
228+ * Gets the maximum rank among all references to `v` in basic block `bb`.
229+ */
230+ private int maxRefRank ( ReachableBasicBlock bb , SsaSourceVariable v ) {
231+ result = max ( refRank ( bb , _, v , _) )
232+ }
233+
219234 /**
220235 * Holds if variable `v` is live after the `i`th node of basic block `bb`, where
221236 * `i` is the index of a node that may assign or capture `v`.
@@ -230,8 +245,8 @@ private cached module Internal {
230245 or
231246 // this is the last reference to `v` inside `bb`, but `v` is live at entry
232247 // to a successor basic block of `bb`
233- r = max ( refRank ( bb , _ , v , _ ) ) and
234- liveAtEntry ( bb . getASuccessor ( ) , v )
248+ r = maxRefRank ( bb , v ) and
249+ liveAtSuccEntry ( bb , v )
235250 )
236251 }
237252
@@ -248,6 +263,13 @@ private cached module Internal {
248263 // there is no reference to `v` inside `bb`, but `v` is live at entry
249264 // to a successor basic block of `bb`
250265 not exists ( refRank ( bb , _, v , _) ) and
266+ liveAtSuccEntry ( bb , v )
267+ }
268+
269+ /**
270+ * Holds if `v` is live at the beginning of any successor of basic block `bb`.
271+ */
272+ private predicate liveAtSuccEntry ( ReachableBasicBlock bb , SsaSourceVariable v ) {
251273 liveAtEntry ( bb .getASuccessor ( ) , v )
252274 }
253275
@@ -311,25 +333,32 @@ private cached module Internal {
311333 )
312334 }
313335
336+ /**
337+ * Gets an SSA definition of `v` that reaches the end of the immediate dominator of `bb`.
338+ */
339+ pragma [ noinline]
340+ private SsaDefinition getDefReachingEndOfImmediateDominator ( ReachableBasicBlock bb , SsaSourceVariable v ) {
341+ result = getDefReachingEndOf ( bb .getImmediateDominator ( ) , v )
342+ }
343+
314344 /**
315345 * Gets an SSA definition of `v` that reaches the end of basic block `bb`.
316346 */
317347 cached SsaDefinition getDefReachingEndOf ( ReachableBasicBlock bb , SsaSourceVariable v ) {
318- bb .getASuccessor ( ) .localIsLiveAtEntry ( v ) and
319- (
320- exists ( int lastRef | lastRef = max ( int i | ssaRef ( bb , i , v , _) ) |
321- result = getLocalDefinition ( bb , lastRef , v )
322- or
323- result .definesAt ( bb , lastRef , v )
324- )
348+ exists ( int lastRef | lastRef = max ( int i | ssaRef ( bb , i , v , _) ) |
349+ result = getLocalDefinition ( bb , lastRef , v )
325350 or
326- /* In SSA form, the (unique) reaching definition of a use is the closest
327- * definition that dominates the use. If two definitions dominate a node
328- * then one must dominate the other, so we can find the reaching definition
329- * by following the idominance relation backwards. */
330- result = getDefReachingEndOf ( bb .getImmediateDominator ( ) , v ) and
331- not exists ( SsaDefinition ssa | ssa .definesAt ( bb , _, v ) )
351+ result .definesAt ( bb , lastRef , v ) and
352+ liveAtSuccEntry ( bb , v )
332353 )
354+ or
355+ /* In SSA form, the (unique) reaching definition of a use is the closest
356+ * definition that dominates the use. If two definitions dominate a node
357+ * then one must dominate the other, so we can find the reaching definition
358+ * by following the idominance relation backwards. */
359+ result = getDefReachingEndOfImmediateDominator ( bb , v ) and
360+ not exists ( SsaDefinition ssa | ssa .definesAt ( bb , _, v ) ) and
361+ liveAtSuccEntry ( bb , v )
333362 }
334363
335364 /**
0 commit comments