@@ -585,12 +585,9 @@ private predicate exploratoryFlowStep(
585585 basicStoreStep ( pred , succ , _) or
586586 basicLoadStep ( pred , succ , _) or
587587
588- any ( AdditionalFlowStep s ) .store ( pred , succ , _) or
589- cfg .isAdditionalStoreStep ( pred , succ , _) or
590- any ( AdditionalFlowStep s ) .load ( pred , succ , _) or
591- cfg .isAdditionalLoadStep ( pred , succ , _) or
592- any ( AdditionalFlowStep s ) .copyProperty ( pred , succ , _) or
593- cfg .isAdditionalCopyPropertyStep ( pred , succ , _) or
588+ isAdditionalStoreStep ( pred , succ , _, cfg ) or
589+ isAdditionalLoadStep ( pred , succ , _, cfg ) or
590+ isAdditionalCopyPropertyStep ( pred , succ , _ , cfg ) or
594591 // the following two disjuncts taken together over-approximate flow through
595592 // higher-order calls
596593 callback ( pred , succ ) or
@@ -752,10 +749,7 @@ private predicate storeStep(
752749 basicStoreStep ( pred , succ , prop ) and
753750 summary = PathSummary:: level ( )
754751 or
755- any ( AdditionalFlowStep s ) .store ( pred , succ , prop ) and
756- summary = PathSummary:: level ( )
757- or
758- cfg .isAdditionalStoreStep ( pred , succ , prop ) and
752+ isAdditionalStoreStep ( pred , succ , prop , cfg ) and
759753 summary = PathSummary:: level ( )
760754 or
761755 exists ( Function f , DataFlow:: Node mid |
@@ -766,11 +760,7 @@ private predicate storeStep(
766760 returnedPropWrite ( f , _, prop , mid )
767761 or
768762 exists ( DataFlow:: SourceNode base |
769- (
770- any ( AdditionalFlowStep step ) .store ( mid , _, prop )
771- or
772- cfg .isAdditionalStoreStep ( mid , _, prop )
773- )
763+ isAdditionalStoreStep ( mid , _, prop , cfg )
774764 and
775765 base .flowsToExpr ( f .getAReturnedExpr ( ) )
776766 )
@@ -793,9 +783,7 @@ private predicate parameterPropRead(
793783 (
794784 read = parm .( DataFlow:: SourceNode ) .getAPropertyRead ( prop )
795785 or
796- any ( AdditionalFlowStep step ) .load ( parm , read , prop )
797- or
798- cfg .isAdditionalLoadStep ( parm , read , prop )
786+ isAdditionalLoadStep ( parm , read , prop , cfg )
799787 )
800788 )
801789}
@@ -818,6 +806,30 @@ private predicate reachesReturn(
818806 )
819807}
820808
809+ private predicate isAdditionalLoadStep ( DataFlow:: Node pred , DataFlow:: Node succ , string prop , DataFlow:: Configuration cfg ) {
810+ exists ( DataFlow:: Node obj | pred = obj .getALocalSource ( ) or pred = obj |
811+ any ( AdditionalFlowStep s ) .load ( obj , succ , prop )
812+ or
813+ cfg .isAdditionalLoadStep ( obj , succ , prop )
814+ )
815+ }
816+
817+ private predicate isAdditionalStoreStep ( DataFlow:: Node pred , DataFlow:: Node succ , string prop , DataFlow:: Configuration cfg ) {
818+ exists ( DataFlow:: Node obj | pred = obj .getALocalSource ( ) or pred = obj |
819+ any ( AdditionalFlowStep s ) .store ( obj , succ , prop )
820+ or
821+ cfg .isAdditionalStoreStep ( obj , succ , prop )
822+ )
823+ }
824+
825+ private predicate isAdditionalCopyPropertyStep ( DataFlow:: Node pred , DataFlow:: Node succ , string prop , DataFlow:: Configuration cfg ) {
826+ exists ( DataFlow:: Node obj | pred = obj .getALocalSource ( ) or pred = obj |
827+ any ( AdditionalFlowStep s ) .copyProperty ( obj , succ , prop )
828+ or
829+ cfg .isAdditionalCopyPropertyStep ( obj , succ , prop )
830+ )
831+ }
832+
821833/**
822834 * Holds if property `prop` of `pred` may flow into `succ` along a path summarized by
823835 * `summary`.
@@ -829,10 +841,7 @@ private predicate loadStep(
829841 basicLoadStep ( pred , succ , prop ) and
830842 summary = PathSummary:: level ( )
831843 or
832- any ( AdditionalFlowStep s ) .load ( pred , succ , prop ) and
833- summary = PathSummary:: level ( )
834- or
835- cfg .isAdditionalLoadStep ( pred , succ , prop ) and
844+ isAdditionalLoadStep ( pred , succ , prop , cfg ) and
836845 summary = PathSummary:: level ( )
837846 or
838847 exists ( Function f , DataFlow:: Node read |
@@ -874,7 +883,7 @@ private predicate flowThroughProperty(
874883) {
875884 exists ( string prop , DataFlow:: Node storeBase , DataFlow:: Node loadBase , PathSummary oldSummary , PathSummary newSummary |
876885 reachableFromStoreBase ( prop , pred , storeBase , cfg , oldSummary ) and
877- ( storeBase = loadBase or existsCopyProperty ( storeBase , loadBase , prop ) ) and
886+ ( storeBase = loadBase or existsCopyProperty ( storeBase , loadBase , prop , cfg ) ) and
878887 loadStep ( loadBase , succ , prop , cfg , newSummary ) and
879888 summary = oldSummary .append ( newSummary )
880889 )
@@ -886,11 +895,11 @@ private predicate flowThroughProperty(
886895 * The recursion of this predicate has been unfolded once compared to a naive implementation in order to avoid having no constraint on `prop`.
887896 * Therefore a caller of this predicate should also test whether the `toNode` and `fromNode` are equal.
888897 */
889- private predicate existsCopyProperty ( DataFlow:: Node fromNode , DataFlow:: Node toNode , string prop ) {
890- exists ( DataFlow:: AdditionalFlowStep step , DataFlow :: Node mid |
891- step . copyProperty ( fromNode , mid , prop ) and
898+ private predicate existsCopyProperty ( DataFlow:: Node fromNode , DataFlow:: Node toNode , string prop , DataFlow :: Configuration cfg ) {
899+ exists ( DataFlow:: Node mid |
900+ isAdditionalCopyPropertyStep ( fromNode , mid , prop , cfg ) and
892901 (
893- existsCopyProperty ( mid , toNode , prop )
902+ existsCopyProperty ( mid , toNode , prop , cfg )
894903 or
895904 mid = toNode
896905 )
0 commit comments