@@ -945,18 +945,31 @@ private predicate reachableFromStoreBase(
945945 s2 .getEndLabel ( ) )
946946 )
947947 or
948- exists ( DataFlow:: Node mid , PathSummary oldSummary , PathSummary newSummary |
949- reachableFromStoreBase ( prop , rhs , mid , cfg , oldSummary ) and
950- (
951- flowStep ( mid , cfg , nd , newSummary )
952- or
953- isAdditionalLoadStoreStep ( mid , nd , prop , cfg ) and
954- newSummary = PathSummary:: level ( )
955- ) and
948+ exists ( PathSummary oldSummary , PathSummary newSummary |
949+ reachableFromStoreBaseStep ( prop , rhs , nd , cfg , oldSummary , newSummary ) and
956950 summary = oldSummary .appendValuePreserving ( newSummary )
957951 )
958952}
959953
954+ /**
955+ * Holds if `rhs` is the right-hand side of a write to property `prop`, and `nd` is reachable
956+ * from the base of that write under configuration `cfg` (possibly through callees) along a
957+ * path whose last step is summarized by `newSummary`, and the previous steps are summarized
958+ * by `oldSummary`.
959+ */
960+ pragma [ noinline]
961+ private predicate reachableFromStoreBaseStep (
962+ string prop , DataFlow:: Node rhs , DataFlow:: Node nd , DataFlow:: Configuration cfg ,
963+ PathSummary oldSummary , PathSummary newSummary
964+ ) {
965+ exists ( DataFlow:: Node mid | reachableFromStoreBase ( prop , rhs , mid , cfg , oldSummary ) |
966+ flowStep ( mid , cfg , nd , newSummary )
967+ or
968+ isAdditionalLoadStoreStep ( mid , nd , prop , cfg ) and
969+ newSummary = PathSummary:: level ( )
970+ )
971+ }
972+
960973/**
961974 * Holds if the value of `pred` is written to a property of some base object, and that base
962975 * object may flow into the base of property read `succ` under configuration `cfg` along
@@ -968,13 +981,29 @@ pragma[noinline]
968981private predicate flowThroughProperty (
969982 DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg , PathSummary summary
970983) {
971- exists ( string prop , DataFlow:: Node base , PathSummary oldSummary , PathSummary newSummary |
972- reachableFromStoreBase ( prop , pred , base , cfg , oldSummary ) and
973- loadStep ( base , succ , prop , cfg , newSummary ) and
984+ exists ( PathSummary oldSummary , PathSummary newSummary |
985+ storeToLoad ( pred , succ , cfg , oldSummary , newSummary ) and
974986 summary = oldSummary .append ( newSummary )
975987 )
976988}
977989
990+ /**
991+ * Holds if the value of `pred` is written to a property of some base object, and that base
992+ * object may flow into the base of property read `succ` under configuration `cfg` along
993+ * a path whose last step is summarized by `newSummary`, and the previous steps are summarized
994+ * by `oldSummary`.
995+ */
996+ pragma [ noinline]
997+ private predicate storeToLoad (
998+ DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg , PathSummary oldSummary ,
999+ PathSummary newSummary
1000+ ) {
1001+ exists ( string prop , DataFlow:: Node base |
1002+ reachableFromStoreBase ( prop , pred , base , cfg , oldSummary ) and
1003+ loadStep ( base , succ , prop , cfg , newSummary )
1004+ )
1005+ }
1006+
9781007/**
9791008 * Holds if `arg` and `cb` are passed as arguments to a function which in turn
9801009 * invokes `cb`, passing `arg` as its `i`th argument.
0 commit comments