@@ -753,8 +753,7 @@ private predicate exploratoryFlowStep(
753
753
DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
754
754
) {
755
755
basicFlowStepNoBarrier ( pred , succ , _, cfg ) or
756
- basicStoreStep ( pred , succ , _) or
757
- isAdditionalStoreStep ( pred , succ , _, cfg ) or
756
+ exploratoryStoreStep ( pred , succ , cfg ) or
758
757
exploratoryLoadStep ( pred , succ , cfg ) or
759
758
isAdditionalLoadStoreStep ( pred , succ , _, _, cfg ) or
760
759
// the following three disjuncts taken together over-approximate flow through
@@ -832,6 +831,23 @@ private string getAPropertyUsedInLoadStore(DataFlow::Configuration cfg) {
832
831
)
833
832
}
834
833
834
+ /**
835
+ * Holds if there exists a store-step from `pred` to `succ` under configuration `cfg`,
836
+ * and somewhere in the program there exists a load-step that could possibly read the stored value.
837
+ */
838
+ predicate exploratoryStoreStep (
839
+ DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
840
+ ) {
841
+ exists ( string prop |
842
+ basicLoadStep ( _, _, prop ) or
843
+ isAdditionalLoadStep ( _, _, prop , cfg ) or
844
+ prop = getAPropertyUsedInLoadStore ( cfg )
845
+ |
846
+ isAdditionalStoreStep ( pred , succ , prop , cfg ) or
847
+ basicStoreStep ( pred , succ , prop )
848
+ )
849
+ }
850
+
835
851
/**
836
852
* Holds if `nd` may be reachable from a source under `cfg`.
837
853
*
0 commit comments