@@ -306,6 +306,38 @@ private module Internal {
306306 exists ( getDefReachingEndOf ( b , v ) )
307307 }
308308
309+ /**
310+ * Holds if `v` occurs in `b1` and `b2` is one of `b1`'s successors.
311+ *
312+ * Factored out of `varBlockReaches` to force join order compared to the larger
313+ * set `blockPrecedesVar(v, b2)`.
314+ */
315+ pragma [ noinline]
316+ private predicate varBlockReachesBaseCand (
317+ SsaSourceVariable v , ReachableBasicBlock b1 , ReachableBasicBlock b2
318+ ) {
319+ varOccursInBlock ( v , b1 ) and
320+ b2 = b1 .getASuccessor ( )
321+ }
322+
323+ /**
324+ * Holds if `b2` is a transitive successor of `b1` and `v` occurs in `b1` and
325+ * in `b2` or one of its transitive successors but not in any block on the path
326+ * between `b1` and `b2`. Unlike `varBlockReaches` this may include blocks `b2`
327+ * where `v` is dead.
328+ *
329+ * Factored out of `varBlockReaches` to force join order compared to the larger
330+ * set `blockPrecedesVar(v, b2)`.
331+ */
332+ pragma [ noinline]
333+ private predicate varBlockReachesRecCand (
334+ SsaSourceVariable v , ReachableBasicBlock b1 , ReachableBasicBlock mid , ReachableBasicBlock b2
335+ ) {
336+ varBlockReaches ( v , b1 , mid ) and
337+ not varOccursInBlock ( v , mid ) and
338+ b2 = mid .getASuccessor ( )
339+ }
340+
309341 /**
310342 * Holds if `b2` is a transitive successor of `b1` and `v` occurs in `b1` and
311343 * in `b2` or one of its transitive successors but not in any block on the path
@@ -314,14 +346,11 @@ private module Internal {
314346 private predicate varBlockReaches (
315347 SsaSourceVariable v , ReachableBasicBlock b1 , ReachableBasicBlock b2
316348 ) {
317- varOccursInBlock ( v , b1 ) and
318- b2 = b1 .getASuccessor ( ) and
349+ varBlockReachesBaseCand ( v , b1 , b2 ) and
319350 blockPrecedesVar ( v , b2 )
320351 or
321352 exists ( ReachableBasicBlock mid |
322- varBlockReaches ( v , b1 , mid ) and
323- b2 = mid .getASuccessor ( ) and
324- not varOccursInBlock ( v , mid ) and
353+ varBlockReachesRecCand ( v , b1 , mid , b2 ) and
325354 blockPrecedesVar ( v , b2 )
326355 )
327356 }
0 commit comments