@@ -609,32 +609,28 @@ pragma[inline]
609609private predicate basicFlowStepNoBarrier (
610610 DataFlow:: Node pred , DataFlow:: Node succ , PathSummary summary , DataFlow:: Configuration cfg
611611) {
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 )
637617 )
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 ( )
638634}
639635
640636/**
@@ -647,6 +643,7 @@ private predicate basicFlowStep(
647643 DataFlow:: Node pred , DataFlow:: Node succ , PathSummary summary , DataFlow:: Configuration cfg
648644) {
649645 basicFlowStepNoBarrier ( pred , succ , summary , cfg ) and
646+ isRelevant ( pred , cfg ) and
650647 not isLabeledBarrierEdge ( cfg , pred , succ , summary .getStartLabel ( ) ) and
651648 not isBarrierEdge ( cfg , pred , succ )
652649}
@@ -661,17 +658,21 @@ private predicate basicFlowStep(
661658private predicate exploratoryFlowStep (
662659 DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
663660) {
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+ )
675676}
676677
677678/**
@@ -826,9 +827,11 @@ private predicate storeStep(
826827 DataFlow:: Node pred , DataFlow:: Node succ , string prop , DataFlow:: Configuration cfg ,
827828 PathSummary summary
828829) {
830+ isRelevant ( pred , cfg ) and
829831 basicStoreStep ( pred , succ , prop ) and
830832 summary = PathSummary:: level ( )
831833 or
834+ isRelevant ( pred , cfg ) and
832835 isAdditionalStoreStep ( pred , succ , prop , cfg ) and
833836 summary = PathSummary:: level ( )
834837 or
@@ -925,9 +928,11 @@ private predicate loadStep(
925928 DataFlow:: Node pred , DataFlow:: Node succ , string prop , DataFlow:: Configuration cfg ,
926929 PathSummary summary
927930) {
931+ isRelevant ( pred , cfg ) and
928932 basicLoadStep ( pred , succ , prop ) and
929933 summary = PathSummary:: level ( )
930934 or
935+ isRelevant ( pred , cfg ) and
931936 isAdditionalLoadStep ( pred , succ , prop , cfg ) and
932937 summary = PathSummary:: level ( )
933938 or
@@ -1148,7 +1153,6 @@ private predicate flowStep(
11481153 // Flow into higher-order call
11491154 flowIntoHigherOrderCall ( pred , succ , cfg , summary )
11501155 ) and
1151- isRelevant ( succ , cfg ) and
11521156 not cfg .isBarrier ( succ ) and
11531157 not isBarrierEdge ( cfg , pred , succ ) and
11541158 not isLabeledBarrierEdge ( cfg , pred , succ , summary .getEndLabel ( ) ) and
@@ -1202,12 +1206,25 @@ private predicate onPath(DataFlow::Node nd, DataFlow::Configuration cfg, PathSum
12021206 not cfg .isLabeledBarrier ( nd , summary .getEndLabel ( ) )
12031207 or
12041208 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
12071210 onPath ( mid , id ( cfg ) , summary .append ( stepSummary ) )
12081211 )
12091212}
12101213
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+
12111228/**
12121229 * Holds if there is a configuration that has at least one source and at least one sink.
12131230 */
0 commit comments