@@ -945,18 +945,31 @@ private predicate reachableFromStoreBase(
945
945
s2 .getEndLabel ( ) )
946
946
)
947
947
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
956
950
summary = oldSummary .appendValuePreserving ( newSummary )
957
951
)
958
952
}
959
953
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
+
960
973
/**
961
974
* Holds if the value of `pred` is written to a property of some base object, and that base
962
975
* object may flow into the base of property read `succ` under configuration `cfg` along
@@ -968,13 +981,29 @@ pragma[noinline]
968
981
private predicate flowThroughProperty (
969
982
DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg , PathSummary summary
970
983
) {
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
974
986
summary = oldSummary .append ( newSummary )
975
987
)
976
988
}
977
989
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
+
978
1007
/**
979
1008
* Holds if `arg` and `cb` are passed as arguments to a function which in turn
980
1009
* invokes `cb`, passing `arg` as its `i`th argument.
0 commit comments