11/**
2- * Provides a language-independant implementation of static single assignment
2+ * Provides a language-independent implementation of static single assignment
33 * (SSA) form.
44 */
55
@@ -316,15 +316,23 @@ private module SsaDefReaches {
316316 )
317317 }
318318
319+ /**
320+ * Holds if the reference to `def` at index `i` in basic block `bb` is the
321+ * last reference to `v` inside `bb`.
322+ */
323+ pragma [ noinline]
324+ predicate lastSsaRef ( Definition def , SourceVariable v , BasicBlock bb , int i ) {
325+ ssaDefRank ( def , v , bb , i , _) = maxSsaRefRank ( bb , v )
326+ }
327+
319328 predicate defOccursInBlock ( Definition def , BasicBlock bb , SourceVariable v ) {
320329 exists ( ssaDefRank ( def , v , bb , _, _) )
321330 }
322331
323332 pragma [ noinline]
324- private BasicBlock getAMaybeLiveSuccessor ( Definition def , BasicBlock bb ) {
325- result = getABasicBlockSuccessor ( bb ) and
326- not defOccursInBlock ( _, bb , def .getSourceVariable ( ) ) and
327- ssaDefReachesEndOfBlock ( bb , def , _)
333+ private predicate ssaDefReachesThroughBlock ( Definition def , BasicBlock bb ) {
334+ ssaDefReachesEndOfBlock ( bb , def , _) and
335+ not defOccursInBlock ( _, bb , def .getSourceVariable ( ) )
328336 }
329337
330338 /**
@@ -337,7 +345,11 @@ private module SsaDefReaches {
337345 defOccursInBlock ( def , bb1 , _) and
338346 bb2 = getABasicBlockSuccessor ( bb1 )
339347 or
340- exists ( BasicBlock mid | varBlockReaches ( def , bb1 , mid ) | bb2 = getAMaybeLiveSuccessor ( def , mid ) )
348+ exists ( BasicBlock mid |
349+ varBlockReaches ( def , bb1 , mid ) and
350+ ssaDefReachesThroughBlock ( def , mid ) and
351+ bb2 = getABasicBlockSuccessor ( mid )
352+ )
341353 }
342354
343355 /**
@@ -348,24 +360,16 @@ private module SsaDefReaches {
348360 */
349361 predicate defAdjacentRead ( Definition def , BasicBlock bb1 , BasicBlock bb2 , int i2 ) {
350362 varBlockReaches ( def , bb1 , bb2 ) and
351- ssaRefRank ( bb2 , i2 , def .getSourceVariable ( ) , SsaRead ( ) ) = 1 and
352- variableRead ( bb2 , i2 , _, _)
363+ ssaRefRank ( bb2 , i2 , def .getSourceVariable ( ) , SsaRead ( ) ) = 1
353364 }
354365}
355366
356367private import SsaDefReaches
357368
358- pragma [ noinline]
359- private predicate ssaDefReachesEndOfBlockRec ( BasicBlock bb , Definition def , SourceVariable v ) {
360- exists ( BasicBlock idom | ssaDefReachesEndOfBlock ( idom , def , v ) |
361- // The construction of SSA form ensures that each read of a variable is
362- // dominated by its definition. An SSA definition therefore reaches a
363- // control flow node if it is the _closest_ SSA definition that dominates
364- // the node. If two definitions dominate a node then one must dominate the
365- // other, so therefore the definition of _closest_ is given by the dominator
366- // tree. Thus, reaching definitions can be calculated in terms of dominance.
367- idom = getImmediateBasicBlockDominator ( bb )
368- )
369+ pragma [ nomagic]
370+ predicate liveThrough ( BasicBlock bb , SourceVariable v ) {
371+ liveAtExit ( bb , v ) and
372+ not ssaRef ( bb , _, v , SsaDef ( ) )
369373}
370374
371375/**
@@ -382,9 +386,14 @@ predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable
382386 liveAtExit ( bb , v )
383387 )
384388 or
385- ssaDefReachesEndOfBlockRec ( bb , def , v ) and
386- liveAtExit ( bb , v ) and
387- not ssaRef ( bb , _, v , SsaDef ( ) )
389+ // The construction of SSA form ensures that each read of a variable is
390+ // dominated by its definition. An SSA definition therefore reaches a
391+ // control flow node if it is the _closest_ SSA definition that dominates
392+ // the node. If two definitions dominate a node then one must dominate the
393+ // other, so therefore the definition of _closest_ is given by the dominator
394+ // tree. Thus, reaching definitions can be calculated in terms of dominance.
395+ ssaDefReachesEndOfBlock ( getImmediateBasicBlockDominator ( bb ) , def , pragma [ only_bind_into ] ( v ) ) and
396+ liveThrough ( bb , pragma [ only_bind_into ] ( v ) )
388397}
389398
390399/**
@@ -433,15 +442,22 @@ predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2
433442 bb2 = bb1
434443 )
435444 or
436- exists ( SourceVariable v | ssaDefRank ( def , v , bb1 , i1 , _ ) = maxSsaRefRank ( bb1 , v ) ) and
445+ lastSsaRef ( def , _ , bb1 , i1 ) and
437446 defAdjacentRead ( def , bb1 , bb2 , i2 )
438447}
439448
449+ pragma [ noinline]
450+ private predicate adjacentDefRead (
451+ Definition def , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 , SourceVariable v
452+ ) {
453+ adjacentDefRead ( def , bb1 , i1 , bb2 , i2 ) and
454+ v = def .getSourceVariable ( )
455+ }
456+
440457private predicate adjacentDefReachesRead (
441458 Definition def , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2
442459) {
443- adjacentDefRead ( def , bb1 , i1 , bb2 , i2 ) and
444- exists ( SourceVariable v | v = def .getSourceVariable ( ) |
460+ exists ( SourceVariable v | adjacentDefRead ( def , bb1 , i1 , bb2 , i2 , v ) |
445461 ssaRef ( bb1 , i1 , v , SsaDef ( ) )
446462 or
447463 variableRead ( bb1 , i1 , v , true )
@@ -474,17 +490,19 @@ predicate adjacentDefNoUncertainReads(Definition def, BasicBlock bb1, int i1, Ba
474490 */
475491pragma [ nomagic]
476492predicate lastRefRedef ( Definition def , BasicBlock bb , int i , Definition next ) {
477- exists ( int rnk , SourceVariable v , int j | rnk = ssaDefRank ( def , v , bb , i , _ ) |
493+ exists ( SourceVariable v |
478494 // Next reference to `v` inside `bb` is a write
479- next .definesAt ( v , bb , j ) and
480- rnk + 1 = ssaRefRank ( bb , j , v , SsaDef ( ) )
495+ exists ( int rnk , int j |
496+ rnk = ssaDefRank ( def , v , bb , i , _) and
497+ next .definesAt ( v , bb , j ) and
498+ rnk + 1 = ssaRefRank ( bb , j , v , SsaDef ( ) )
499+ )
481500 or
482501 // Can reach a write using one or more steps
483- rnk = maxSsaRefRank ( bb , v ) and
502+ lastSsaRef ( def , v , bb , i ) and
484503 exists ( BasicBlock bb2 |
485504 varBlockReaches ( def , bb , bb2 ) and
486- next .definesAt ( v , bb2 , j ) and
487- 1 = ssaRefRank ( bb2 , j , v , SsaDef ( ) )
505+ 1 = ssaDefRank ( next , v , bb2 , _, SsaDef ( ) )
488506 )
489507 )
490508}
@@ -538,7 +556,8 @@ pragma[nomagic]
538556predicate lastRef ( Definition def , BasicBlock bb , int i ) {
539557 lastRefRedef ( def , bb , i , _)
540558 or
541- exists ( SourceVariable v | ssaDefRank ( def , v , bb , i , _) = maxSsaRefRank ( bb , v ) |
559+ lastSsaRef ( def , _, bb , i ) and
560+ (
542561 // Can reach exit directly
543562 bb instanceof ExitBasicBlock
544563 or
0 commit comments