@@ -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,7 @@ private predicate flowStep(
11481153 // Flow into higher-order call
11491154 flowIntoHigherOrderCall ( pred , succ , cfg , summary )
11501155 ) and
1151- isRelevant ( succ , cfg ) and
1156+ isRelevant ( pred , cfg ) and
11521157 not cfg .isBarrier ( succ ) and
11531158 not isBarrierEdge ( cfg , pred , succ ) and
11541159 not isLabeledBarrierEdge ( cfg , pred , succ , summary .getEndLabel ( ) ) and
0 commit comments