@@ -609,32 +609,28 @@ pragma[inline]
609
609
private predicate basicFlowStepNoBarrier (
610
610
DataFlow:: Node pred , DataFlow:: Node succ , PathSummary summary , DataFlow:: Configuration cfg
611
611
) {
612
- isLive ( ) and
613
- isRelevantForward ( pred , cfg ) and
614
- (
615
- // Local flow
616
- exists ( FlowLabel predlbl , FlowLabel succlbl |
617
- localFlowStep ( pred , succ , cfg , predlbl , succlbl ) and
618
- not cfg .isBarrierEdge ( pred , succ ) and
619
- summary = MkPathSummary ( false , false , predlbl , succlbl )
620
- )
621
- or
622
- // Flow through properties of objects
623
- propertyFlowStep ( pred , succ ) and
624
- summary = PathSummary:: level ( )
625
- or
626
- // Flow through global variables
627
- globalFlowStep ( pred , succ ) and
628
- summary = PathSummary:: level ( )
629
- or
630
- // Flow into function
631
- callStep ( pred , succ ) and
632
- summary = PathSummary:: call ( )
633
- or
634
- // Flow out of function
635
- returnStep ( pred , succ ) and
636
- summary = PathSummary:: return ( )
612
+ // Local flow
613
+ exists ( FlowLabel predlbl , FlowLabel succlbl |
614
+ localFlowStep ( pred , succ , cfg , predlbl , succlbl ) and
615
+ not cfg .isBarrierEdge ( pred , succ ) and
616
+ summary = MkPathSummary ( false , false , predlbl , succlbl )
637
617
)
618
+ or
619
+ // Flow through properties of objects
620
+ propertyFlowStep ( pred , succ ) and
621
+ summary = PathSummary:: level ( )
622
+ or
623
+ // Flow through global variables
624
+ globalFlowStep ( pred , succ ) and
625
+ summary = PathSummary:: level ( )
626
+ or
627
+ // Flow into function
628
+ callStep ( pred , succ ) and
629
+ summary = PathSummary:: call ( )
630
+ or
631
+ // Flow out of function
632
+ returnStep ( pred , succ ) and
633
+ summary = PathSummary:: return ( )
638
634
}
639
635
640
636
/**
@@ -647,6 +643,7 @@ private predicate basicFlowStep(
647
643
DataFlow:: Node pred , DataFlow:: Node succ , PathSummary summary , DataFlow:: Configuration cfg
648
644
) {
649
645
basicFlowStepNoBarrier ( pred , succ , summary , cfg ) and
646
+ isRelevant ( pred , cfg ) and
650
647
not isLabeledBarrierEdge ( cfg , pred , succ , summary .getStartLabel ( ) ) and
651
648
not isBarrierEdge ( cfg , pred , succ )
652
649
}
@@ -661,17 +658,21 @@ private predicate basicFlowStep(
661
658
private predicate exploratoryFlowStep (
662
659
DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
663
660
) {
664
- basicFlowStepNoBarrier ( pred , succ , _, cfg ) or
665
- basicStoreStep ( pred , succ , _) or
666
- basicLoadStep ( pred , succ , _) or
667
- isAdditionalStoreStep ( pred , succ , _, cfg ) or
668
- isAdditionalLoadStep ( pred , succ , _, cfg ) or
669
- isAdditionalLoadStoreStep ( pred , succ , _, cfg ) or
670
- // the following three disjuncts taken together over-approximate flow through
671
- // higher-order calls
672
- callback ( pred , succ ) or
673
- succ = pred .( DataFlow:: FunctionNode ) .getAParameter ( ) or
674
- exploratoryBoundInvokeStep ( pred , succ )
661
+ isRelevantForward ( pred , cfg ) and
662
+ isLive ( ) and
663
+ (
664
+ basicFlowStepNoBarrier ( pred , succ , _, cfg ) or
665
+ basicStoreStep ( pred , succ , _) or
666
+ basicLoadStep ( pred , succ , _) or
667
+ isAdditionalStoreStep ( pred , succ , _, cfg ) or
668
+ isAdditionalLoadStep ( pred , succ , _, cfg ) or
669
+ isAdditionalLoadStoreStep ( pred , succ , _, cfg ) or
670
+ // the following three disjuncts taken together over-approximate flow through
671
+ // higher-order calls
672
+ callback ( pred , succ ) or
673
+ succ = pred .( DataFlow:: FunctionNode ) .getAParameter ( ) or
674
+ exploratoryBoundInvokeStep ( pred , succ )
675
+ )
675
676
}
676
677
677
678
/**
@@ -826,9 +827,11 @@ private predicate storeStep(
826
827
DataFlow:: Node pred , DataFlow:: Node succ , string prop , DataFlow:: Configuration cfg ,
827
828
PathSummary summary
828
829
) {
830
+ isRelevant ( pred , cfg ) and
829
831
basicStoreStep ( pred , succ , prop ) and
830
832
summary = PathSummary:: level ( )
831
833
or
834
+ isRelevant ( pred , cfg ) and
832
835
isAdditionalStoreStep ( pred , succ , prop , cfg ) and
833
836
summary = PathSummary:: level ( )
834
837
or
@@ -925,9 +928,11 @@ private predicate loadStep(
925
928
DataFlow:: Node pred , DataFlow:: Node succ , string prop , DataFlow:: Configuration cfg ,
926
929
PathSummary summary
927
930
) {
931
+ isRelevant ( pred , cfg ) and
928
932
basicLoadStep ( pred , succ , prop ) and
929
933
summary = PathSummary:: level ( )
930
934
or
935
+ isRelevant ( pred , cfg ) and
931
936
isAdditionalLoadStep ( pred , succ , prop , cfg ) and
932
937
summary = PathSummary:: level ( )
933
938
or
@@ -1148,7 +1153,6 @@ private predicate flowStep(
1148
1153
// Flow into higher-order call
1149
1154
flowIntoHigherOrderCall ( pred , succ , cfg , summary )
1150
1155
) and
1151
- isRelevant ( succ , cfg ) and
1152
1156
not cfg .isBarrier ( succ ) and
1153
1157
not isBarrierEdge ( cfg , pred , succ ) and
1154
1158
not isLabeledBarrierEdge ( cfg , pred , succ , summary .getEndLabel ( ) ) and
@@ -1202,12 +1206,25 @@ private predicate onPath(DataFlow::Node nd, DataFlow::Configuration cfg, PathSum
1202
1206
not cfg .isLabeledBarrier ( nd , summary .getEndLabel ( ) )
1203
1207
or
1204
1208
exists ( DataFlow:: Node mid , PathSummary stepSummary |
1205
- reachableFromSource ( nd , cfg , summary ) and
1206
- flowStep ( nd , id ( cfg ) , mid , stepSummary ) and
1209
+ onPathStep ( nd , cfg , summary , stepSummary , mid ) and
1207
1210
onPath ( mid , id ( cfg ) , summary .append ( stepSummary ) )
1208
1211
)
1209
1212
}
1210
1213
1214
+ /**
1215
+ * Holds if `nd` can be reached from a source under `cfg`,
1216
+ * and there is a flowStep from `nd` (with summary `summary`) to `mid` (with summary `stepSummary`).
1217
+ *
1218
+ * This predicate has been outlined from `onPath` to give the optimizer a hint about join-ordering.
1219
+ */
1220
+ private predicate onPathStep (
1221
+ DataFlow:: Node nd , DataFlow:: Configuration cfg , PathSummary summary , PathSummary stepSummary ,
1222
+ DataFlow:: Node mid
1223
+ ) {
1224
+ reachableFromSource ( nd , cfg , summary ) and
1225
+ flowStep ( nd , id ( cfg ) , mid , stepSummary )
1226
+ }
1227
+
1211
1228
/**
1212
1229
* Holds if there is a configuration that has at least one source and at least one sink.
1213
1230
*/
0 commit comments