@@ -748,24 +748,21 @@ private predicate basicFlowStep(
748
748
* This predicate is field insensitive (it does not distinguish between `x` and `x.p`)
749
749
* and hence should only be used for purposes of approximation.
750
750
*/
751
+ pragma [ inline]
751
752
private predicate exploratoryFlowStep (
752
753
DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
753
754
) {
754
- isRelevantForward ( pred , cfg ) and
755
- isLive ( ) and
756
- (
757
- basicFlowStepNoBarrier ( pred , succ , _, cfg ) or
758
- basicStoreStep ( pred , succ , _) or
759
- basicLoadStep ( pred , succ , _) or
760
- isAdditionalStoreStep ( pred , succ , _, cfg ) or
761
- isAdditionalLoadStep ( pred , succ , _, cfg ) or
762
- isAdditionalLoadStoreStep ( pred , succ , _, _, cfg ) or
763
- // the following three disjuncts taken together over-approximate flow through
764
- // higher-order calls
765
- callback ( pred , succ ) or
766
- succ = pred .( DataFlow:: FunctionNode ) .getAParameter ( ) or
767
- exploratoryBoundInvokeStep ( pred , succ )
768
- )
755
+ basicFlowStepNoBarrier ( pred , succ , _, cfg ) or
756
+ basicStoreStep ( pred , succ , _) or
757
+ basicLoadStep ( pred , succ , _) or
758
+ isAdditionalStoreStep ( pred , succ , _, cfg ) or
759
+ isAdditionalLoadStep ( pred , succ , _, cfg ) or
760
+ isAdditionalLoadStoreStep ( pred , succ , _, _, cfg ) or
761
+ // the following three disjuncts taken together over-approximate flow through
762
+ // higher-order calls
763
+ callback ( pred , succ ) or
764
+ succ = pred .( DataFlow:: FunctionNode ) .getAParameter ( ) or
765
+ exploratoryBoundInvokeStep ( pred , succ )
769
766
}
770
767
771
768
/**
@@ -798,9 +795,9 @@ private predicate isSink(DataFlow::Node nd, DataFlow::Configuration cfg, FlowLab
798
795
* No call/return matching is done, so this is a relatively coarse over-approximation.
799
796
*/
800
797
private predicate isRelevantForward ( DataFlow:: Node nd , DataFlow:: Configuration cfg ) {
801
- isSource ( nd , cfg , _)
798
+ isSource ( nd , cfg , _) and isLive ( )
802
799
or
803
- exists ( DataFlow:: Node mid | isRelevantForward ( mid , cfg ) and exploratoryFlowStep ( mid , nd , cfg ) )
800
+ exists ( DataFlow:: Node mid | isRelevantForward ( mid , cfg ) | exploratoryFlowStep ( mid , nd , cfg ) )
804
801
}
805
802
806
803
/**
@@ -809,14 +806,17 @@ private predicate isRelevantForward(DataFlow::Node nd, DataFlow::Configuration c
809
806
* No call/return matching is done, so this is a relatively coarse over-approximation.
810
807
*/
811
808
private predicate isRelevant ( DataFlow:: Node nd , DataFlow:: Configuration cfg ) {
812
- isRelevantForward ( nd , cfg ) and
813
- isSink ( nd , cfg , _)
809
+ isRelevantForward ( nd , cfg ) and isSink ( nd , cfg , _)
814
810
or
815
- exists ( DataFlow:: Node mid |
816
- isRelevant ( mid , cfg ) and
817
- exploratoryFlowStep ( nd , mid , cfg ) and
818
- isRelevantForward ( nd , cfg )
819
- )
811
+ exists ( DataFlow:: Node mid | isRelevant ( mid , cfg ) | isRelevantBackStep ( mid , nd , cfg ) )
812
+ }
813
+
814
+ /**
815
+ * Holds if there is backwards data-flow step from `mid` to `nd` under `cfg`.
816
+ */
817
+ predicate isRelevantBackStep ( DataFlow:: Node mid , DataFlow:: Node nd , DataFlow:: Configuration cfg ) {
818
+ isRelevantForward ( nd , cfg ) and
819
+ exploratoryFlowStep ( nd , mid , cfg )
820
820
}
821
821
822
822
/**
0 commit comments