@@ -754,9 +754,8 @@ private predicate exploratoryFlowStep(
754
754
) {
755
755
basicFlowStepNoBarrier ( pred , succ , _, cfg ) or
756
756
basicStoreStep ( pred , succ , _) or
757
- basicLoadStep ( pred , succ , _) or
758
757
isAdditionalStoreStep ( pred , succ , _, cfg ) or
759
- isAdditionalLoadStep ( pred , succ , _ , cfg ) or
758
+ exploratoryLoadStep ( pred , succ , cfg ) or
760
759
isAdditionalLoadStoreStep ( pred , succ , _, _, cfg ) or
761
760
// the following three disjuncts taken together over-approximate flow through
762
761
// higher-order calls
@@ -789,6 +788,50 @@ private predicate isSink(DataFlow::Node nd, DataFlow::Configuration cfg, FlowLab
789
788
cfg .isSink ( nd , lbl )
790
789
}
791
790
791
+ /**
792
+ * Holds if there exists a load-step from `pred` to `succ` under configuration `cfg`,
793
+ * and the forwards exploratory flow has found a relevant store-step with the same property as the load-step.
794
+ */
795
+ private predicate exploratoryLoadStep (
796
+ DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
797
+ ) {
798
+ exists ( string prop | prop = getAForwardRelevantLoadProperty ( cfg ) |
799
+ isAdditionalLoadStep ( pred , succ , prop , cfg )
800
+ or
801
+ basicLoadStep ( pred , succ , prop )
802
+ )
803
+ }
804
+
805
+ /**
806
+ * Gets a property where the forwards exploratory flow has found a relevant store-step with that property.
807
+ * The property is therefore relevant for load-steps in the forward exploratory flow.
808
+ *
809
+ * This private predicate is only used in `exploratoryLoadStep`, and exists as a separate predicate to give the compiler a hint about join-ordering.
810
+ */
811
+ private string getAForwardRelevantLoadProperty ( DataFlow:: Configuration cfg ) {
812
+ exists ( DataFlow:: Node previous | isRelevantForward ( previous , cfg ) |
813
+ basicStoreStep ( previous , _, result ) or
814
+ isAdditionalStoreStep ( previous , _, result , cfg )
815
+ )
816
+ or
817
+ result = getAPropertyUsedInLoadStore ( cfg )
818
+ }
819
+
820
+ /**
821
+ * Gets a property that is used in an `additionalLoadStoreStep` where the loaded and stored property are not the same.
822
+ *
823
+ * 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.
824
+ */
825
+ private string getAPropertyUsedInLoadStore ( DataFlow:: Configuration cfg ) {
826
+ exists ( string loadProp | not loadProp = result |
827
+ isAdditionalLoadStoreStep ( _, _, loadProp , result , cfg )
828
+ )
829
+ or
830
+ exists ( string storeProp | not storeProp = result |
831
+ isAdditionalLoadStoreStep ( _, _, result , storeProp , cfg )
832
+ )
833
+ }
834
+
792
835
/**
793
836
* Holds if `nd` may be reachable from a source under `cfg`.
794
837
*
0 commit comments