@@ -51,6 +51,11 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
51
51
*/
52
52
default predicate isAdditionalFlowStep ( Node node1 , Node node2 ) { none ( ) }
53
53
54
+ /**
55
+ * Holds if taint may propagate from `node1` to `node2` in addition to the normal data-flow steps.
56
+ */
57
+ default predicate isAdditionalTaintStep ( Node node1 , Node node2 ) { none ( ) }
58
+
54
59
/** Holds if data flow into `node` is prohibited. */
55
60
default predicate isBarrier ( Node node ) { none ( ) }
56
61
@@ -101,7 +106,7 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
101
106
predicate isAdditionalFlowStep ( Node node1 , FlowState state1 , Node node2 , FlowState state2 ) {
102
107
storeStep ( node1 , state1 , _, node2 , state2 ) or
103
108
readStep ( node1 , state1 , _, node2 , state2 ) or
104
- additionalStep ( node1 , state1 , node2 , state2 )
109
+ additionalTaintStep ( node1 , state1 , node2 , state2 )
105
110
}
106
111
107
112
predicate isAdditionalFlowStep = ContentConfig:: isAdditionalFlowStep / 2 ;
@@ -229,8 +234,8 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
229
234
)
230
235
}
231
236
232
- private predicate additionalStep ( Node node1 , State state1 , Node node2 , State state2 ) {
233
- ContentConfig:: isAdditionalFlowStep ( node1 , node2 ) and
237
+ private predicate additionalTaintStep ( Node node1 , State state1 , Node node2 , State state2 ) {
238
+ ContentConfig:: isAdditionalTaintStep ( node1 , node2 ) and
234
239
(
235
240
state1 instanceof InitState and
236
241
state2 .( InitState ) .decode ( false )
@@ -302,12 +307,16 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
302
307
// relation, when flow can reach a sink without going back out
303
308
Flow:: PathGraph:: subpaths ( pred , succ , _, _) and
304
309
not reachesSink ( succ )
305
- or
310
+ )
311
+ or
312
+ exists ( Node predNode , State predState , Node succNode , State succState |
313
+ succNodeAndState ( pred , predNode , predState , succ , succNode , succState )
314
+ |
306
315
// needed to record store steps
307
- storeStep ( pred . getNode ( ) , pred . getState ( ) , _, succ . getNode ( ) , succ . getState ( ) )
316
+ storeStep ( predNode , predState , _, succNode , succState )
308
317
or
309
318
// needed to record read steps
310
- readStep ( pred . getNode ( ) , pred . getState ( ) , _, succ . getNode ( ) , succ . getState ( ) )
319
+ readStep ( predNode , predState , _, succNode , succState )
311
320
)
312
321
}
313
322
0 commit comments