@@ -958,18 +958,31 @@ private predicate reachableFromStoreBase(
958
958
s2 .getEndLabel ( ) )
959
959
)
960
960
or
961
- exists ( DataFlow:: Node mid , PathSummary oldSummary , PathSummary newSummary |
962
- reachableFromStoreBase ( prop , rhs , mid , cfg , oldSummary ) and
963
- (
964
- flowStep ( mid , cfg , nd , newSummary )
965
- or
966
- isAdditionalLoadStoreStep ( mid , nd , prop , cfg ) and
967
- newSummary = PathSummary:: level ( )
968
- ) and
961
+ exists ( PathSummary oldSummary , PathSummary newSummary |
962
+ reachableFromStoreBaseStep ( prop , rhs , nd , cfg , oldSummary , newSummary ) and
969
963
summary = oldSummary .appendValuePreserving ( newSummary )
970
964
)
971
965
}
972
966
967
+ /**
968
+ * Holds if `rhs` is the right-hand side of a write to property `prop`, and `nd` is reachable
969
+ * from the base of that write under configuration `cfg` (possibly through callees) along a
970
+ * path whose last step is summarized by `newSummary`, and the previous steps are summarized
971
+ * by `oldSummary`.
972
+ */
973
+ pragma [ noinline]
974
+ private predicate reachableFromStoreBaseStep (
975
+ string prop , DataFlow:: Node rhs , DataFlow:: Node nd , DataFlow:: Configuration cfg ,
976
+ PathSummary oldSummary , PathSummary newSummary
977
+ ) {
978
+ exists ( DataFlow:: Node mid | reachableFromStoreBase ( prop , rhs , mid , cfg , oldSummary ) |
979
+ flowStep ( mid , cfg , nd , newSummary )
980
+ or
981
+ isAdditionalLoadStoreStep ( mid , nd , prop , cfg ) and
982
+ newSummary = PathSummary:: level ( )
983
+ )
984
+ }
985
+
973
986
/**
974
987
* Holds if the value of `pred` is written to a property of some base object, and that base
975
988
* object may flow into the base of property read `succ` under configuration `cfg` along
@@ -981,13 +994,29 @@ pragma[noinline]
981
994
private predicate flowThroughProperty (
982
995
DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg , PathSummary summary
983
996
) {
984
- exists ( string prop , DataFlow:: Node base , PathSummary oldSummary , PathSummary newSummary |
985
- reachableFromStoreBase ( prop , pred , base , cfg , oldSummary ) and
986
- loadStep ( base , succ , prop , cfg , newSummary ) and
997
+ exists ( PathSummary oldSummary , PathSummary newSummary |
998
+ storeToLoad ( pred , succ , cfg , oldSummary , newSummary ) and
987
999
summary = oldSummary .append ( newSummary )
988
1000
)
989
1001
}
990
1002
1003
+ /**
1004
+ * Holds if the value of `pred` is written to a property of some base object, and that base
1005
+ * object may flow into the base of property read `succ` under configuration `cfg` along
1006
+ * a path whose last step is summarized by `newSummary`, and the previous steps are summarized
1007
+ * by `oldSummary`.
1008
+ */
1009
+ pragma [ noinline]
1010
+ private predicate storeToLoad (
1011
+ DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg , PathSummary oldSummary ,
1012
+ PathSummary newSummary
1013
+ ) {
1014
+ exists ( string prop , DataFlow:: Node base |
1015
+ reachableFromStoreBase ( prop , pred , base , cfg , oldSummary ) and
1016
+ loadStep ( base , succ , prop , cfg , newSummary )
1017
+ )
1018
+ }
1019
+
991
1020
/**
992
1021
* Holds if `arg` and `cb` are passed as arguments to a function which in turn
993
1022
* invokes `cb`, passing `arg` as its `i`th argument.
0 commit comments