@@ -753,7 +753,6 @@ private predicate exploratoryFlowStep(
753753 DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
754754) {
755755 basicFlowStepNoBarrier ( pred , succ , _, cfg ) or
756- exploratoryStoreStep ( pred , succ , cfg ) or
757756 exploratoryLoadStep ( pred , succ , cfg ) or
758757 isAdditionalLoadStoreStep ( pred , succ , _, _, cfg ) or
759758 // the following three disjuncts taken together over-approximate flow through
@@ -835,7 +834,7 @@ private string getAPropertyUsedInLoadStore(DataFlow::Configuration cfg) {
835834 * Holds if there exists a store-step from `pred` to `succ` under configuration `cfg`,
836835 * and somewhere in the program there exists a load-step that could possibly read the stored value.
837836 */
838- predicate exploratoryStoreStep (
837+ predicate exploratoryForwardStoreStep (
839838 DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
840839) {
841840 exists ( string prop |
@@ -848,6 +847,35 @@ predicate exploratoryStoreStep(
848847 )
849848}
850849
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+
851879/**
852880 * Holds if `nd` may be reachable from a source under `cfg`.
853881 *
@@ -856,7 +884,10 @@ predicate exploratoryStoreStep(
856884private predicate isRelevantForward ( DataFlow:: Node nd , DataFlow:: Configuration cfg ) {
857885 isSource ( nd , cfg , _) and isLive ( )
858886 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+ )
860891}
861892
862893/**
@@ -875,7 +906,10 @@ private predicate isRelevant(DataFlow::Node nd, DataFlow::Configuration cfg) {
875906 */
876907predicate isRelevantBackStep ( DataFlow:: Node mid , DataFlow:: Node nd , DataFlow:: Configuration cfg ) {
877908 isRelevantForward ( nd , cfg ) and
878- exploratoryFlowStep ( nd , mid , cfg )
909+ (
910+ exploratoryFlowStep ( nd , mid , cfg ) or
911+ exploratoryBackwardStoreStep ( nd , mid , cfg )
912+ )
879913}
880914
881915/**
0 commit comments