@@ -490,7 +490,7 @@ module FlowVar_internal {
490490 exists ( VariableAccess va |
491491 va .getTarget ( ) = result and
492492 readAccess ( va ) and
493- bbNotInLoop ( va .getBasicBlock ( ) )
493+ exists ( BasicBlock bb | bb = va .getBasicBlock ( ) | not this . bbInLoop ( bb ) )
494494 )
495495 }
496496
@@ -513,10 +513,8 @@ module FlowVar_internal {
513513 bbInLoopCondition ( bb )
514514 }
515515
516- predicate bbNotInLoop ( BasicBlock bb ) {
517- not this .bbInLoop ( bb ) and
518- bb .getEnclosingFunction ( ) = this .getEnclosingFunction ( )
519- }
516+ /** Holds if `sbb` is inside this loop. */
517+ predicate sbbInLoop ( SubBasicBlock sbb ) { this .bbInLoop ( sbb .getBasicBlock ( ) ) }
520518
521519 /**
522520 * Holds if `bb` is a basic block inside this loop where `v` has not been
@@ -537,22 +535,19 @@ module FlowVar_internal {
537535 }
538536
539537 /**
540- * Holds if some loop always assigns to `v` before leaving through an edge
541- * from `bbInside` in its condition to `bbOutside` outside the loop, where
542- * (`sbbDef`, `v`) is a `BlockVar` defined outside the loop. Also, `v` must
543- * be used outside the loop.
538+ * Holds if `loop` always assigns to `v` before leaving through an edge
539+ * from `bbInside` in its condition to `bbOutside` outside the loop. Also,
540+ * `v` must be used outside the loop.
544541 */
545542 predicate skipLoop (
546- SubBasicBlock sbbInside , SubBasicBlock sbbOutside , SubBasicBlock sbbDef , Variable v
543+ SubBasicBlock sbbInside , SubBasicBlock sbbOutside , Variable v , AlwaysTrueUponEntryLoop loop
547544 ) {
548- exists ( AlwaysTrueUponEntryLoop loop , BasicBlock bbInside , BasicBlock bbOutside |
545+ exists ( BasicBlock bbInside , BasicBlock bbOutside |
549546 loop .alwaysAssignsBeforeLeavingCondition ( bbInside , bbOutside , v ) and
550547 bbInside = sbbInside .getBasicBlock ( ) and
551548 bbOutside = sbbOutside .getBasicBlock ( ) and
552549 sbbInside .lastInBB ( ) and
553- sbbOutside .firstInBB ( ) and
554- loop .bbNotInLoop ( sbbDef .getBasicBlock ( ) ) and
555- exists ( TBlockVar ( sbbDef , v ) )
550+ sbbOutside .firstInBB ( )
556551 )
557552 }
558553
@@ -571,7 +566,7 @@ module FlowVar_internal {
571566 start = TBlockVar ( sbbDef , v ) and
572567 result = mid .getASuccessor ( ) and
573568 variableLiveInSBB ( result , v ) and
574- not skipLoop ( mid , result , sbbDef , v ) and
569+ forall ( AlwaysTrueUponEntryLoop loop | skipLoop ( mid , result , v , loop ) | loop . sbbInLoop ( sbbDef ) ) and
575570 not assignmentLikeOperation ( result , v , _, _)
576571 )
577572 }
@@ -679,10 +674,11 @@ module FlowVar_internal {
679674 predicate dominatedByOverwrite ( UninitializedLocalVariable v , VariableAccess va ) {
680675 exists ( BasicBlock bb , int vaIndex |
681676 va = bb .getNode ( vaIndex ) and
682- va .getTarget ( ) = v
683- |
677+ va .getTarget ( ) = v and
684678 vaIndex > indexOfFirstOverwriteInBB ( v , bb )
685679 or
680+ va = bb .getNode ( vaIndex ) and
681+ va .getTarget ( ) = v and
686682 bbStrictlyDominates ( getAnOverwritingBB ( v ) , bb )
687683 )
688684 }
0 commit comments