@@ -753,7 +753,6 @@ private predicate exploratoryFlowStep(
753
753
DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
754
754
) {
755
755
basicFlowStepNoBarrier ( pred , succ , _, cfg ) or
756
- exploratoryStoreStep ( pred , succ , cfg ) or
757
756
exploratoryLoadStep ( pred , succ , cfg ) or
758
757
isAdditionalLoadStoreStep ( pred , succ , _, _, cfg ) or
759
758
// the following three disjuncts taken together over-approximate flow through
@@ -835,7 +834,7 @@ private string getAPropertyUsedInLoadStore(DataFlow::Configuration cfg) {
835
834
* Holds if there exists a store-step from `pred` to `succ` under configuration `cfg`,
836
835
* and somewhere in the program there exists a load-step that could possibly read the stored value.
837
836
*/
838
- predicate exploratoryStoreStep (
837
+ predicate exploratoryForwardStoreStep (
839
838
DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
840
839
) {
841
840
exists ( string prop |
@@ -848,6 +847,35 @@ predicate exploratoryStoreStep(
848
847
)
849
848
}
850
849
850
+ /**
851
+ * Holds if there exists a store-step from `pred` to `succ` under configuration `cfg`,
852
+ * and `succ` has been found to be relevant during the backwards exploratory flow,
853
+ * and the backwards exploratory flow has found a relevant load-step with the same property as the store-step.
854
+ */
855
+ private predicate exploratoryBackwardStoreStep (
856
+ DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
857
+ ) {
858
+ exists ( string prop | prop = getABackwardsRelevantStoreProperty ( cfg ) |
859
+ isAdditionalStoreStep ( pred , succ , prop , cfg ) or
860
+ basicStoreStep ( pred , succ , prop )
861
+ )
862
+ }
863
+
864
+ /**
865
+ * Gets a property where the backwards exploratory flow has found a relevant load-step with that property.
866
+ * The property is therefore relevant for store-steps in the backwards exploratory flow.
867
+ *
868
+ * This private predicate is only used in `exploratoryBackwardStoreStep`, and exists as a separate predicate to give the compiler a hint about join-ordering.
869
+ */
870
+ string getABackwardsRelevantStoreProperty ( DataFlow:: Configuration cfg ) {
871
+ exists ( DataFlow:: Node mid | isRelevant ( mid , cfg ) |
872
+ basicLoadStep ( mid , _, result ) or
873
+ isAdditionalLoadStep ( mid , _, result , cfg )
874
+ )
875
+ or
876
+ result = getAPropertyUsedInLoadStore ( cfg )
877
+ }
878
+
851
879
/**
852
880
* Holds if `nd` may be reachable from a source under `cfg`.
853
881
*
@@ -856,7 +884,10 @@ predicate exploratoryStoreStep(
856
884
private predicate isRelevantForward ( DataFlow:: Node nd , DataFlow:: Configuration cfg ) {
857
885
isSource ( nd , cfg , _) and isLive ( )
858
886
or
859
- exists ( DataFlow:: Node mid | isRelevantForward ( mid , cfg ) | exploratoryFlowStep ( mid , nd , cfg ) )
887
+ exists ( DataFlow:: Node mid | isRelevantForward ( mid , cfg ) |
888
+ exploratoryFlowStep ( mid , nd , cfg ) or
889
+ exploratoryForwardStoreStep ( mid , nd , cfg )
890
+ )
860
891
}
861
892
862
893
/**
@@ -875,7 +906,10 @@ private predicate isRelevant(DataFlow::Node nd, DataFlow::Configuration cfg) {
875
906
*/
876
907
predicate isRelevantBackStep ( DataFlow:: Node mid , DataFlow:: Node nd , DataFlow:: Configuration cfg ) {
877
908
isRelevantForward ( nd , cfg ) and
878
- exploratoryFlowStep ( nd , mid , cfg )
909
+ (
910
+ exploratoryFlowStep ( nd , mid , cfg ) or
911
+ exploratoryBackwardStoreStep ( nd , mid , cfg )
912
+ )
879
913
}
880
914
881
915
/**
0 commit comments