@@ -226,20 +226,18 @@ abstract class Configuration extends string {
226226
227227 /**
228228 * Holds if the `pred` should be stored in the object `succ` under the property `prop`.
229- *
230- * `succ` is a DataFlow::SourceNode, as this is assumed by the `isAdditionalCopyPropertyStep` predicate.
231229 */
232- predicate isAdditionalStoreStep ( DataFlow:: Node pred , DataFlow:: SourceNode succ , string prop ) { none ( ) }
230+ predicate isAdditionalStoreStep ( DataFlow:: Node pred , DataFlow:: Node succ , string prop ) { none ( ) }
233231
234232 /**
235233 * Holds if the property `prop` of the object `pred` should be loaded into `succ`.
236234 */
237235 predicate isAdditionalLoadStep ( DataFlow:: Node pred , DataFlow:: Node succ , string prop ) { none ( ) }
238236
239237 /**
240- * Holds if the property `prop` should be copied from the object `pred` to the object `succ`.
238+ * Holds if the property `prop` should be copied from the object `pred` to the object `succ`.
241239 */
242- predicate isAdditionalCopyPropertyStep ( DataFlow:: Node pred , DataFlow:: SourceNode succ , string prop ) { none ( ) }
240+ predicate isAdditionalCopyPropertyStep ( DataFlow:: Node pred , DataFlow:: Node succ , string prop ) { none ( ) }
243241}
244242
245243/**
@@ -470,11 +468,9 @@ abstract class AdditionalFlowStep extends DataFlow::Node {
470468
471469 /**
472470 * Holds if the `pred` should be stored in the object `succ` under the property `prop`.
473- *
474- * `succ` is a DataFlow::SourceNode, as this is assumed by the `copyProperty` predicate.
475471 */
476472 cached
477- predicate store ( DataFlow:: Node pred , DataFlow:: SourceNode succ , string prop ) { none ( ) }
473+ predicate store ( DataFlow:: Node pred , DataFlow:: Node succ , string prop ) { none ( ) }
478474
479475 /**
480476 * Holds if the property `prop` of the object `pred` should be loaded into `succ`.
@@ -486,7 +482,7 @@ abstract class AdditionalFlowStep extends DataFlow::Node {
486482 * Holds if the property `prop` should be copied from the object `pred` to the object `succ`.
487483 */
488484 cached
489- predicate copyProperty ( DataFlow:: Node pred , DataFlow:: SourceNode succ , string prop ) { none ( ) }
485+ predicate copyProperty ( DataFlow:: Node pred , DataFlow:: Node succ , string prop ) { none ( ) }
490486}
491487
492488/**
@@ -765,7 +761,7 @@ private predicate storeStep(
765761 returnedPropWrite ( f , _, prop , mid )
766762 or
767763 exists ( DataFlow:: SourceNode base |
768- isAdditionalStoreStep ( mid , _ , prop , cfg )
764+ isAdditionalStoreStep ( mid , base , prop , cfg )
769765 and
770766 base .flowsToExpr ( f .getAReturnedExpr ( ) )
771767 )
@@ -811,27 +807,31 @@ private predicate reachesReturn(
811807 )
812808}
813809
810+ /**
811+ * Holds if the property `prop` of the object `pred` should be loaded into `succ`.
812+ */
814813private predicate isAdditionalLoadStep ( DataFlow:: Node pred , DataFlow:: Node succ , string prop , DataFlow:: Configuration cfg ) {
815814 any ( AdditionalFlowStep s ) .load ( pred , succ , prop )
816815 or
817816 cfg .isAdditionalLoadStep ( pred , succ , prop )
818817}
819818
820- private predicate isAdditionalStoreStep ( DataFlow:: Node pred , DataFlow:: SourceNode succ , string prop , DataFlow:: Configuration cfg ) {
819+ /**
820+ * Holds if the `pred` should be stored in the object `succ` under the property `prop`.
821+ */
822+ private predicate isAdditionalStoreStep ( DataFlow:: Node pred , DataFlow:: Node succ , string prop , DataFlow:: Configuration cfg ) {
821823 any ( AdditionalFlowStep s ) .store ( pred , succ , prop )
822824 or
823825 cfg .isAdditionalStoreStep ( pred , succ , prop )
824826}
825827
826- private predicate isAdditionalCopyPropertyStep ( DataFlow:: SourceNode pred , DataFlow:: Node succ , string prop , DataFlow:: Configuration cfg ) {
827- exists ( DataFlow:: Node predNode , DataFlow:: SourceNode succNode |
828- pred = predNode .getALocalSource ( ) and
829- succ .getALocalSource ( ) = succNode
830- |
831- any ( AdditionalFlowStep s ) .copyProperty ( predNode , succNode , prop )
832- or
833- cfg .isAdditionalCopyPropertyStep ( predNode , succNode , prop )
834- )
828+ /**
829+ * Holds if the property `prop` should be copied from the object `pred` to the object `succ`.
830+ */
831+ private predicate isAdditionalCopyPropertyStep ( DataFlow:: Node pred , DataFlow:: Node succ , string prop , DataFlow:: Configuration cfg ) {
832+ any ( AdditionalFlowStep s ) .copyProperty ( pred , succ , prop )
833+ or
834+ cfg .isAdditionalCopyPropertyStep ( pred , succ , prop )
835835}
836836
837837/**
@@ -869,7 +869,12 @@ private predicate reachableFromStoreBase(
869869 or
870870 exists ( DataFlow:: Node mid , PathSummary oldSummary , PathSummary newSummary |
871871 reachableFromStoreBase ( prop , rhs , mid , cfg , oldSummary ) and
872- flowStep ( mid , cfg , nd , newSummary ) and
872+ (
873+ flowStep ( mid , cfg , nd , newSummary )
874+ or
875+ existsCopyProperty ( mid , nd , prop , cfg ) and
876+ newSummary = PathSummary:: level ( )
877+ ) and
873878 summary = oldSummary .appendValuePreserving ( newSummary )
874879 )
875880}
@@ -885,28 +890,33 @@ pragma[noinline]
885890private predicate flowThroughProperty (
886891 DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg , PathSummary summary
887892) {
888- exists ( string prop , DataFlow:: Node storeBase , DataFlow:: Node loadBase , PathSummary oldSummary , PathSummary newSummary |
889- reachableFromStoreBase ( prop , pred , storeBase , cfg , oldSummary ) and
890- ( storeBase = loadBase or existsCopyProperty ( storeBase , loadBase , prop , cfg ) ) and
891- loadStep ( loadBase , succ , prop , cfg , newSummary ) and
893+ exists ( string prop , DataFlow:: Node base , PathSummary oldSummary , PathSummary newSummary |
894+ reachableFromStoreBase ( prop , pred , base , cfg , oldSummary ) and
895+ loadStep ( base , succ , prop , cfg , newSummary ) and
892896 summary = oldSummary .append ( newSummary )
893897 )
894898}
895899
900+ /**
901+ * Holds if the property `prop` is copied from `fromNode` to `toNode`.
902+ */
903+ bindingset [ prop, cfg]
904+ private predicate existsCopyProperty ( DataFlow:: Node fromNode , DataFlow:: Node toNode , string prop , DataFlow:: Configuration cfg ) {
905+ fromNode = toNode
906+ or
907+ existsCopyPropertyRecursive ( fromNode , toNode , prop , cfg )
908+ }
909+
896910/**
897911 * Holds if the property `prop` is copied from `fromNode` to `toNode` using at least 1 step.
898912 *
899913 * The recursion of this predicate has been unfolded once compared to a naive implementation in order to avoid having no constraint on `prop`.
900914 * Therefore a caller of this predicate should also test whether the `toNode` and `fromNode` are equal.
901915 */
902- private predicate existsCopyProperty ( DataFlow:: Node fromNode , DataFlow:: Node toNode , string prop , DataFlow:: Configuration cfg ) {
916+ private predicate existsCopyPropertyRecursive ( DataFlow:: Node fromNode , DataFlow:: Node toNode , string prop , DataFlow:: Configuration cfg ) {
903917 exists ( DataFlow:: Node mid |
904918 isAdditionalCopyPropertyStep ( fromNode , mid , prop , cfg ) and
905- (
906- existsCopyProperty ( mid , toNode , prop , cfg )
907- or
908- mid = toNode
909- )
919+ existsCopyProperty ( mid , toNode , prop , cfg )
910920 )
911921}
912922
0 commit comments