@@ -748,24 +748,18 @@ 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
+ exploratoryLoadStep ( pred , succ , cfg ) or
757
+ isAdditionalLoadStoreStep ( pred , succ , _, _, cfg ) or
758
+ // the following three disjuncts taken together over-approximate flow through
759
+ // higher-order calls
760
+ callback ( pred , succ ) or
761
+ succ = pred .( DataFlow:: FunctionNode ) .getAParameter ( ) or
762
+ exploratoryBoundInvokeStep ( pred , succ )
769
763
}
770
764
771
765
/**
@@ -792,15 +786,106 @@ private predicate isSink(DataFlow::Node nd, DataFlow::Configuration cfg, FlowLab
792
786
cfg .isSink ( nd , lbl )
793
787
}
794
788
789
+ /**
790
+ * Holds if there exists a load-step from `pred` to `succ` under configuration `cfg`,
791
+ * and the forwards exploratory flow has found a relevant store-step with the same property as the load-step.
792
+ */
793
+ private predicate exploratoryLoadStep (
794
+ DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
795
+ ) {
796
+ exists ( string prop | prop = getAForwardRelevantLoadProperty ( cfg ) |
797
+ isAdditionalLoadStep ( pred , succ , prop , cfg )
798
+ or
799
+ basicLoadStep ( pred , succ , prop )
800
+ )
801
+ }
802
+
803
+ /**
804
+ * Gets a property where the forwards exploratory flow has found a relevant store-step with that property.
805
+ * The property is therefore relevant for load-steps in the forward exploratory flow.
806
+ *
807
+ * This private predicate is only used in `exploratoryLoadStep`, and exists as a separate predicate to give the compiler a hint about join-ordering.
808
+ */
809
+ private string getAForwardRelevantLoadProperty ( DataFlow:: Configuration cfg ) {
810
+ exists ( DataFlow:: Node previous | isRelevantForward ( previous , cfg ) |
811
+ basicStoreStep ( previous , _, result ) or
812
+ isAdditionalStoreStep ( previous , _, result , cfg )
813
+ )
814
+ or
815
+ result = getAPropertyUsedInLoadStore ( cfg )
816
+ }
817
+
818
+ /**
819
+ * Gets a property that is used in an `additionalLoadStoreStep` where the loaded and stored property are not the same.
820
+ *
821
+ * The properties from this predicate are used as a white-list of properties for load/store steps that should always be considered in the exploratory flow.
822
+ */
823
+ private string getAPropertyUsedInLoadStore ( DataFlow:: Configuration cfg ) {
824
+ exists ( string loadProp , string storeProp |
825
+ isAdditionalLoadStoreStep ( _, _, loadProp , storeProp , cfg ) and
826
+ storeProp != loadProp and
827
+ result = [ storeProp , loadProp ]
828
+ )
829
+ }
830
+
831
+ /**
832
+ * Holds if there exists a store-step from `pred` to `succ` under configuration `cfg`,
833
+ * and somewhere in the program there exists a load-step that could possibly read the stored value.
834
+ */
835
+ private predicate exploratoryForwardStoreStep (
836
+ DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
837
+ ) {
838
+ exists ( string prop |
839
+ basicLoadStep ( _, _, prop ) or
840
+ isAdditionalLoadStep ( _, _, prop , cfg ) or
841
+ prop = getAPropertyUsedInLoadStore ( cfg )
842
+ |
843
+ isAdditionalStoreStep ( pred , succ , prop , cfg ) or
844
+ basicStoreStep ( pred , succ , prop )
845
+ )
846
+ }
847
+
848
+ /**
849
+ * Holds if there exists a store-step from `pred` to `succ` under configuration `cfg`,
850
+ * and `succ` has been found to be relevant during the backwards exploratory flow,
851
+ * and the backwards exploratory flow has found a relevant load-step with the same property as the store-step.
852
+ */
853
+ private predicate exploratoryBackwardStoreStep (
854
+ DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
855
+ ) {
856
+ exists ( string prop | prop = getABackwardsRelevantStoreProperty ( cfg ) |
857
+ isAdditionalStoreStep ( pred , succ , prop , cfg ) or
858
+ basicStoreStep ( pred , succ , prop )
859
+ )
860
+ }
861
+
862
+ /**
863
+ * Gets a property where the backwards exploratory flow has found a relevant load-step with that property.
864
+ * The property is therefore relevant for store-steps in the backwards exploratory flow.
865
+ *
866
+ * This private predicate is only used in `exploratoryBackwardStoreStep`, and exists as a separate predicate to give the compiler a hint about join-ordering.
867
+ */
868
+ private string getABackwardsRelevantStoreProperty ( DataFlow:: Configuration cfg ) {
869
+ exists ( DataFlow:: Node mid | isRelevant ( mid , cfg ) |
870
+ basicLoadStep ( mid , _, result ) or
871
+ isAdditionalLoadStep ( mid , _, result , cfg )
872
+ )
873
+ or
874
+ result = getAPropertyUsedInLoadStore ( cfg )
875
+ }
876
+
795
877
/**
796
878
* Holds if `nd` may be reachable from a source under `cfg`.
797
879
*
798
880
* No call/return matching is done, so this is a relatively coarse over-approximation.
799
881
*/
800
882
private predicate isRelevantForward ( DataFlow:: Node nd , DataFlow:: Configuration cfg ) {
801
- isSource ( nd , cfg , _)
883
+ isSource ( nd , cfg , _) and isLive ( )
802
884
or
803
- exists ( DataFlow:: Node mid | isRelevantForward ( mid , cfg ) and exploratoryFlowStep ( mid , nd , cfg ) )
885
+ exists ( DataFlow:: Node mid | isRelevantForward ( mid , cfg ) |
886
+ exploratoryFlowStep ( mid , nd , cfg ) or
887
+ exploratoryForwardStoreStep ( mid , nd , cfg )
888
+ )
804
889
}
805
890
806
891
/**
@@ -809,13 +894,21 @@ private predicate isRelevantForward(DataFlow::Node nd, DataFlow::Configuration c
809
894
* No call/return matching is done, so this is a relatively coarse over-approximation.
810
895
*/
811
896
private predicate isRelevant ( DataFlow:: Node nd , DataFlow:: Configuration cfg ) {
812
- isRelevantForward ( nd , cfg ) and
813
- isSink ( nd , cfg , _)
897
+ isRelevantForward ( nd , cfg ) and isSink ( nd , cfg , _)
814
898
or
815
- exists ( DataFlow:: Node mid |
816
- isRelevant ( mid , cfg ) and
817
- exploratoryFlowStep ( nd , mid , cfg ) and
818
- isRelevantForward ( nd , cfg )
899
+ exists ( DataFlow:: Node mid | isRelevant ( mid , cfg ) | isRelevantBackStep ( mid , nd , cfg ) )
900
+ }
901
+
902
+ /**
903
+ * Holds if there is backwards data-flow step from `mid` to `nd` under `cfg`.
904
+ */
905
+ private predicate isRelevantBackStep (
906
+ DataFlow:: Node mid , DataFlow:: Node nd , DataFlow:: Configuration cfg
907
+ ) {
908
+ isRelevantForward ( nd , cfg ) and
909
+ (
910
+ exploratoryFlowStep ( nd , mid , cfg ) or
911
+ exploratoryBackwardStoreStep ( nd , mid , cfg )
819
912
)
820
913
}
821
914
0 commit comments