@@ -1183,50 +1183,49 @@ private predicate loadStep(
11831183}
11841184
11851185/**
1186- * Holds if `rhs` is the right-hand side of a write to property `prop`, and `nd` is reachable
1187- * from the base of that write under configuration `cfg` (possibly through callees) along a
1188- * path summarized by `summary`.
1186+ * Holds if there is flow to `base.startProp`, and `base.startProp` flows to `nd.endProp` under `cfg/summary`.
11891187 */
11901188pragma [ nomagic]
11911189private predicate reachableFromStoreBase (
1192- string prop , DataFlow:: Node rhs , DataFlow:: Node nd , DataFlow:: Configuration cfg ,
1190+ string startProp , string endProp , DataFlow:: Node base , DataFlow:: Node nd , DataFlow:: Configuration cfg ,
11931191 PathSummary summary
11941192) {
1195- exists ( PathSummary s1 , PathSummary s2 |
1193+ exists ( PathSummary s1 , PathSummary s2 , DataFlow :: Node rhs |
11961194 reachableFromSource ( rhs , cfg , s1 )
11971195 or
1198- reachableFromStoreBase ( _, _, rhs , cfg , s1 )
1196+ reachableFromStoreBase ( _, _, _ , rhs , cfg , s1 )
11991197 |
1200- storeStep ( rhs , nd , prop , cfg , s2 ) and
1198+ storeStep ( rhs , nd , startProp , cfg , s2 ) and
1199+ endProp = startProp and
1200+ base = nd and
12011201 summary =
1202- MkPathSummary ( false , s1 .hasCall ( ) .booleanOr ( s2 .hasCall ( ) ) , s2 .getStartLabel ( ) ,
1203- s2 .getEndLabel ( ) )
1202+ MkPathSummary ( false , s1 .hasCall ( ) .booleanOr ( s2 .hasCall ( ) ) , DataFlow:: FlowLabel:: data ( ) , DataFlow:: FlowLabel:: data ( ) )
12041203 )
12051204 or
12061205 exists ( PathSummary newSummary , PathSummary oldSummary |
1207- reachableFromStoreBaseStep ( prop , rhs , nd , cfg , oldSummary , newSummary ) and
1206+ reachableFromStoreBaseStep ( startProp , endProp , base , nd , cfg , oldSummary , newSummary ) and
12081207 summary = oldSummary .appendValuePreserving ( newSummary )
12091208 )
12101209}
12111210
12121211/**
1213- * Holds if `rhs ` is the right-hand side of a write to property `prop`, and `nd` is reachable
1214- * from the base of that write under configuration `cfg` (possibly through callees) along a
1215- * path whose last step is summarized by `newSummary`, and the previous steps are summarized
1212+ * Holds if `base ` is the base of a write to property `prop`, and `nd` is reachable
1213+ * from ` base` under configuration `cfg` (possibly through callees) along a path whose
1214+ * last step is summarized by `newSummary`, and the previous steps are summarized
12161215 * by `oldSummary`.
12171216 */
12181217pragma [ noinline]
12191218private predicate reachableFromStoreBaseStep (
1220- string prop , DataFlow:: Node rhs , DataFlow:: Node nd , DataFlow:: Configuration cfg ,
1219+ string startProp , string endProp , DataFlow:: Node base , DataFlow:: Node nd , DataFlow:: Configuration cfg ,
12211220 PathSummary oldSummary , PathSummary newSummary
12221221) {
12231222 exists ( DataFlow:: Node mid |
1224- reachableFromStoreBase ( prop , rhs , mid , cfg , oldSummary ) and
1223+ reachableFromStoreBase ( startProp , endProp , base , mid , cfg , oldSummary ) and
12251224 flowStep ( mid , cfg , nd , newSummary )
12261225 or
12271226 exists ( string midProp |
1228- reachableFromStoreBase ( midProp , rhs , mid , cfg , oldSummary ) and
1229- isAdditionalLoadStoreStep ( mid , nd , midProp , prop , cfg ) and
1227+ reachableFromStoreBase ( startProp , midProp , base , mid , cfg , oldSummary ) and
1228+ isAdditionalLoadStoreStep ( mid , nd , midProp , endProp , cfg ) and
12301229 newSummary = PathSummary:: level ( )
12311230 )
12321231 )
@@ -1260,9 +1259,11 @@ private predicate storeToLoad(
12601259 DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg , PathSummary oldSummary ,
12611260 PathSummary newSummary
12621261) {
1263- exists ( string prop , DataFlow:: Node base |
1264- reachableFromStoreBase ( prop , pred , base , cfg , oldSummary ) and
1265- loadStep ( base , succ , prop , cfg , newSummary )
1262+ exists ( string storeProp , string loadProp , DataFlow:: Node storeBase , DataFlow:: Node loadBase , PathSummary s1 , PathSummary s2 |
1263+ storeStep ( pred , storeBase , storeProp , cfg , s1 ) and
1264+ reachableFromStoreBase ( storeProp , loadProp , storeBase , loadBase , cfg , s2 ) and
1265+ oldSummary = s1 .appendValuePreserving ( s2 ) and
1266+ loadStep ( loadBase , succ , loadProp , cfg , newSummary )
12661267 )
12671268}
12681269
0 commit comments