@@ -89,11 +89,6 @@ private ControlFlowNode captureNode(TrackedVar capturedvar, TrackedVar closureva
8989 )
9090}
9191
92- /** Holds if `VarAccess` `use` of `v` occurs in `b` at index `i`. */
93- private predicate variableUse ( TrackedVar v , VarRead use , BasicBlock b , int i ) {
94- v .getAnAccess ( ) = use and b .getNode ( i ) = use
95- }
96-
9792/** Holds if the value of `v` is captured in `b` at index `i`. */
9893private predicate variableCapture ( TrackedVar capturedvar , TrackedVar closurevar , BasicBlock b , int i ) {
9994 b .getNode ( i ) = captureNode ( capturedvar , closurevar )
@@ -177,66 +172,6 @@ class UntrackedDef extends Definition {
177172 Location getLocation ( ) { result = read .getLocation ( ) }
178173}
179174
180- pragma [ noinline]
181- private predicate adjacentDefRead (
182- Definition def , SsaInput:: BasicBlock bb1 , int i1 , SsaInput:: BasicBlock bb2 , int i2 ,
183- SsaInput:: SourceVariable v
184- ) {
185- Impl:: adjacentDefRead ( def , bb1 , i1 , bb2 , i2 ) and
186- v = def .getSourceVariable ( )
187- }
188-
189- pragma [ nomagic]
190- predicate adjacentDefReachesRead (
191- Definition def , SsaInput:: SourceVariable v , SsaInput:: BasicBlock bb1 , int i1 ,
192- SsaInput:: BasicBlock bb2 , int i2
193- ) {
194- adjacentDefRead ( def , bb1 , i1 , bb2 , i2 , v ) and
195- (
196- def .definesAt ( v , bb1 , i1 )
197- or
198- SsaInput:: variableRead ( bb1 , i1 , v , true )
199- )
200- or
201- exists ( SsaInput:: BasicBlock bb3 , int i3 |
202- adjacentDefReachesRead ( def , v , bb1 , i1 , bb3 , i3 ) and
203- SsaInput:: variableRead ( bb3 , i3 , _, false ) and
204- Impl:: adjacentDefRead ( def , bb3 , i3 , bb2 , i2 )
205- )
206- }
207-
208- /** Same as `adjacentDefRead`, but skips uncertain reads. */
209- pragma [ nomagic]
210- private predicate adjacentDefSkipUncertainReads (
211- Definition def , SsaInput:: BasicBlock bb1 , int i1 , SsaInput:: BasicBlock bb2 , int i2
212- ) {
213- exists ( SsaInput:: SourceVariable v |
214- adjacentDefReachesRead ( def , v , bb1 , i1 , bb2 , i2 ) and
215- SsaInput:: variableRead ( bb2 , i2 , v , true )
216- )
217- }
218-
219- pragma [ nomagic]
220- private predicate adjacentDefReachesUncertainRead (
221- Definition def , SsaInput:: BasicBlock bb1 , int i1 , SsaInput:: BasicBlock bb2 , int i2
222- ) {
223- exists ( SsaInput:: SourceVariable v |
224- adjacentDefReachesRead ( def , v , bb1 , i1 , bb2 , i2 ) and
225- SsaInput:: variableRead ( bb2 , i2 , v , false )
226- )
227- }
228-
229- pragma [ nomagic]
230- predicate lastRefBeforeRedef ( Definition def , BasicBlock bb , int i , Definition next ) {
231- Impl:: lastRefRedef ( def , bb , i , next ) and
232- not SsaInput:: variableRead ( bb , i , def .getSourceVariable ( ) , false )
233- or
234- exists ( SsaInput:: BasicBlock bb0 , int i0 |
235- Impl:: lastRefRedef ( def , bb0 , i0 , next ) and
236- adjacentDefReachesUncertainRead ( def , bb , i , bb0 , i0 )
237- )
238- }
239-
240175cached
241176private module Cached {
242177 cached
@@ -556,12 +491,27 @@ private module Cached {
556491 )
557492 }
558493
494+ pragma [ nomagic]
495+ private predicate captureDefReaches ( Definition def , SsaInput:: BasicBlock bb2 , int i2 ) {
496+ variableCapture ( def .getSourceVariable ( ) , _, _, _) and
497+ exists ( SsaInput:: BasicBlock bb1 , int i1 |
498+ Impl:: adjacentDefRead ( def , bb1 , i1 , bb2 , i2 ) and
499+ def .definesAt ( _, bb1 , i1 )
500+ )
501+ or
502+ exists ( SsaInput:: BasicBlock bb3 , int i3 |
503+ captureDefReaches ( def , bb3 , i3 ) and
504+ SsaInput:: variableRead ( bb3 , i3 , _, _) and
505+ Impl:: adjacentDefRead ( def , bb3 , i3 , bb2 , i2 )
506+ )
507+ }
508+
559509 /** Holds if `init` is a closure variable that captures the value of `capturedvar`. */
560510 cached
561511 predicate captures ( SsaImplicitInit init , SsaVariable capturedvar ) {
562- exists ( BasicBlock bb2 , int i2 |
563- adjacentDefReachesRead ( capturedvar , _ , _ , _ , bb2 , i2 ) and
564- variableCapture ( capturedvar .getSourceVariable ( ) , init .getSourceVariable ( ) , bb2 , i2 )
512+ exists ( BasicBlock bb , int i |
513+ captureDefReaches ( capturedvar , bb , i ) and
514+ variableCapture ( capturedvar .getSourceVariable ( ) , init .getSourceVariable ( ) , bb , i )
565515 )
566516 }
567517
@@ -574,16 +524,22 @@ private module Cached {
574524 Impl:: uncertainWriteDefinitionInput ( redef , def )
575525 }
576526
577- /**
578- * Holds if the value defined at SSA definition `def` can reach a read at `use`,
579- * without passing through any other read.
580- */
581527 pragma [ nomagic]
582- private predicate firstUseSameVar ( Definition def , VarRead use ) {
583- exists ( BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 |
584- def .definesAt ( _, bb1 , i1 ) and
585- adjacentDefSkipUncertainReads ( def , bb1 , i1 , bb2 , i2 ) and
586- use = bb2 .getNode ( i2 )
528+ private predicate defReaches ( Definition def , DataFlowIntegration:: Node node ) {
529+ exists ( DataFlowIntegration:: SsaDefinitionExtNode nodeFrom |
530+ nodeFrom .getDefinitionExt ( ) = def and
531+ DataFlowIntegrationImpl:: localFlowStep ( _, nodeFrom , node , false )
532+ )
533+ or
534+ exists ( DataFlowIntegration:: Node mid |
535+ defReaches ( def , mid ) and
536+ DataFlowIntegrationImpl:: localFlowStep ( _, mid , node , _)
537+ |
538+ // flow into phi input node
539+ mid instanceof DataFlowIntegration:: SsaInputNode
540+ or
541+ // flow into definition
542+ mid instanceof DataFlowIntegration:: SsaDefinitionExtNode
587543 )
588544 }
589545
@@ -593,14 +549,9 @@ private module Cached {
593549 */
594550 cached
595551 predicate firstUse ( Definition def , VarRead use ) {
596- firstUseSameVar ( def , use )
597- or
598- exists ( Definition redef , BasicBlock b1 , int i1 |
599- redef instanceof SsaUncertainImplicitUpdate or redef instanceof SsaPhiNode
600- |
601- lastRefBeforeRedef ( def , b1 , i1 , redef ) and
602- def .definesAt ( _, b1 , i1 ) and
603- firstUse ( redef , use )
552+ exists ( DataFlowIntegration:: ExprNode nodeTo |
553+ nodeTo .getExpr ( ) = use and
554+ defReaches ( def , nodeTo )
604555 )
605556 }
606557
@@ -646,17 +597,41 @@ private module Cached {
646597
647598 cached
648599 module SsaPublic {
600+ pragma [ nomagic]
601+ private predicate useReaches ( VarRead use , DataFlowIntegration:: Node node , boolean sameVar ) {
602+ exists ( DataFlowIntegration:: ExprNode nodeFrom |
603+ nodeFrom .getExpr ( ) = use and
604+ DataFlowIntegration:: localFlowStep ( _, nodeFrom , node , true ) and
605+ sameVar = true
606+ )
607+ or
608+ exists ( DataFlowIntegration:: Node mid , boolean sameVarMid |
609+ useReaches ( use , mid , sameVarMid ) and
610+ DataFlowIntegration:: localFlowStep ( _, mid , node , _)
611+ |
612+ // flow into phi input node
613+ mid instanceof DataFlowIntegration:: SsaInputNode and
614+ sameVar = false
615+ or
616+ // flow into definition
617+ exists ( Impl:: DefinitionExt def |
618+ def = mid .( DataFlowIntegration:: SsaDefinitionExtNode ) .getDefinitionExt ( )
619+ |
620+ if def instanceof Impl:: PhiReadNode then sameVar = sameVarMid else sameVar = false
621+ )
622+ )
623+ }
624+
649625 /**
650626 * Holds if `use1` and `use2` form an adjacent use-use-pair of the same SSA
651627 * variable, that is, the value read in `use1` can reach `use2` without passing
652628 * through any other use or any SSA definition of the variable.
653629 */
654630 cached
655631 predicate adjacentUseUseSameVar ( VarRead use1 , VarRead use2 ) {
656- exists ( TrackedVar v , BasicBlock b1 , int i1 , BasicBlock b2 , int i2 |
657- adjacentDefSkipUncertainReads ( _, b1 , i1 , b2 , i2 ) and
658- variableUse ( v , use1 , b1 , i1 ) and
659- variableUse ( v , use2 , b2 , i2 )
632+ exists ( DataFlowIntegration:: ExprNode nodeTo |
633+ nodeTo .getExpr ( ) = use2 and
634+ useReaches ( use1 , nodeTo , true )
660635 )
661636 }
662637
@@ -668,14 +643,9 @@ private module Cached {
668643 */
669644 cached
670645 predicate adjacentUseUse ( VarRead use1 , VarRead use2 ) {
671- adjacentUseUseSameVar ( use1 , use2 )
672- or
673- exists ( TrackedSsaDef def , BasicBlock b1 , int i1 |
674- lastRefBeforeRedef ( _, b1 , i1 , def ) and
675- variableUse ( _, use1 , b1 , i1 ) and
676- firstUse ( def , use2 )
677- |
678- def instanceof SsaUncertainImplicitUpdate or def instanceof SsaPhiNode
646+ exists ( DataFlowIntegration:: ExprNode nodeTo |
647+ nodeTo .getExpr ( ) = use2 and
648+ useReaches ( use1 , nodeTo , _)
679649 )
680650 }
681651 }
0 commit comments