@@ -89,11 +89,6 @@ private ControlFlowNode captureNode(TrackedVar capturedvar, TrackedVar closureva
89
89
)
90
90
}
91
91
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
-
97
92
/** Holds if the value of `v` is captured in `b` at index `i`. */
98
93
private predicate variableCapture ( TrackedVar capturedvar , TrackedVar closurevar , BasicBlock b , int i ) {
99
94
b .getNode ( i ) = captureNode ( capturedvar , closurevar )
@@ -177,66 +172,6 @@ class UntrackedDef extends Definition {
177
172
Location getLocation ( ) { result = read .getLocation ( ) }
178
173
}
179
174
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
-
240
175
cached
241
176
private module Cached {
242
177
cached
@@ -556,12 +491,27 @@ private module Cached {
556
491
)
557
492
}
558
493
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
+
559
509
/** Holds if `init` is a closure variable that captures the value of `capturedvar`. */
560
510
cached
561
511
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 )
565
515
)
566
516
}
567
517
@@ -574,16 +524,22 @@ private module Cached {
574
524
Impl:: uncertainWriteDefinitionInput ( redef , def )
575
525
}
576
526
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
- */
581
527
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
587
543
)
588
544
}
589
545
@@ -593,14 +549,9 @@ private module Cached {
593
549
*/
594
550
cached
595
551
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 )
604
555
)
605
556
}
606
557
@@ -646,17 +597,41 @@ private module Cached {
646
597
647
598
cached
648
599
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
+
649
625
/**
650
626
* Holds if `use1` and `use2` form an adjacent use-use-pair of the same SSA
651
627
* variable, that is, the value read in `use1` can reach `use2` without passing
652
628
* through any other use or any SSA definition of the variable.
653
629
*/
654
630
cached
655
631
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 )
660
635
)
661
636
}
662
637
@@ -668,14 +643,9 @@ private module Cached {
668
643
*/
669
644
cached
670
645
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 , _)
679
649
)
680
650
}
681
651
}
0 commit comments