@@ -748,24 +748,18 @@ private predicate basicFlowStep(
748748 * This predicate is field insensitive (it does not distinguish between `x` and `x.p`)
749749 * and hence should only be used for purposes of approximation.
750750 */
751+ pragma [ inline]
751752private predicate exploratoryFlowStep (
752753 DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
753754) {
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 )
769763}
770764
771765/**
@@ -792,15 +786,106 @@ private predicate isSink(DataFlow::Node nd, DataFlow::Configuration cfg, FlowLab
792786 cfg .isSink ( nd , lbl )
793787}
794788
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+
795877/**
796878 * Holds if `nd` may be reachable from a source under `cfg`.
797879 *
798880 * No call/return matching is done, so this is a relatively coarse over-approximation.
799881 */
800882private predicate isRelevantForward ( DataFlow:: Node nd , DataFlow:: Configuration cfg ) {
801- isSource ( nd , cfg , _)
883+ isSource ( nd , cfg , _) and isLive ( )
802884 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+ )
804889}
805890
806891/**
@@ -809,13 +894,21 @@ private predicate isRelevantForward(DataFlow::Node nd, DataFlow::Configuration c
809894 * No call/return matching is done, so this is a relatively coarse over-approximation.
810895 */
811896private 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 , _)
814898 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 )
819912 )
820913}
821914
0 commit comments