@@ -33,6 +33,11 @@ module MakeImpl<DataFlowParameter Lang> {
33
33
*/
34
34
predicate isSink ( Node sink , FlowState state ) ;
35
35
36
+ /**
37
+ * Holds if `sink` is a relevant data flow sink for any state.
38
+ */
39
+ predicate isSink ( Node sink ) ;
40
+
36
41
/**
37
42
* Holds if data flow through `node` is prohibited. This completely removes
38
43
* `node` from the data flow graph.
@@ -216,8 +221,11 @@ module MakeImpl<DataFlowParameter Lang> {
216
221
private predicate outBarrier ( NodeEx node ) {
217
222
exists ( Node n |
218
223
node .asNode ( ) = n and
219
- Config:: isBarrierOut ( n ) and
224
+ Config:: isBarrierOut ( n )
225
+ |
220
226
Config:: isSink ( n , _)
227
+ or
228
+ Config:: isSink ( n )
221
229
)
222
230
}
223
231
@@ -230,7 +238,8 @@ module MakeImpl<DataFlowParameter Lang> {
230
238
not Config:: isSource ( n , _)
231
239
or
232
240
Config:: isBarrierOut ( n ) and
233
- not Config:: isSink ( n , _)
241
+ not Config:: isSink ( n , _) and
242
+ not Config:: isSink ( n )
234
243
)
235
244
}
236
245
@@ -247,7 +256,7 @@ module MakeImpl<DataFlowParameter Lang> {
247
256
}
248
257
249
258
pragma [ nomagic]
250
- private predicate sinkNode ( NodeEx node , FlowState state ) {
259
+ private predicate sinkNodeWithState ( NodeEx node , FlowState state ) {
251
260
Config:: isSink ( node .asNode ( ) , state ) and
252
261
not fullBarrier ( node ) and
253
262
not stateBarrier ( node , state )
@@ -645,6 +654,16 @@ module MakeImpl<DataFlowParameter Lang> {
645
654
)
646
655
}
647
656
657
+ additional predicate sinkNode ( NodeEx node , FlowState state ) {
658
+ fwdFlow ( node ) and
659
+ fwdFlowState ( state ) and
660
+ Config:: isSink ( node .asNode ( ) )
661
+ or
662
+ fwdFlow ( node ) and
663
+ fwdFlowState ( state ) and
664
+ sinkNodeWithState ( node , state )
665
+ }
666
+
648
667
/**
649
668
* Holds if `node` is part of a path from a source to a sink.
650
669
*
@@ -659,12 +678,8 @@ module MakeImpl<DataFlowParameter Lang> {
659
678
660
679
pragma [ nomagic]
661
680
private predicate revFlow0 ( NodeEx node , boolean toReturn ) {
662
- exists ( FlowState state |
663
- fwdFlow ( node ) and
664
- sinkNode ( node , state ) and
665
- fwdFlowState ( state ) and
666
- if hasSinkCallCtx ( ) then toReturn = true else toReturn = false
667
- )
681
+ sinkNode ( node , _) and
682
+ if hasSinkCallCtx ( ) then toReturn = true else toReturn = false
668
683
or
669
684
exists ( NodeEx mid | revFlow ( mid , toReturn ) |
670
685
localFlowStepEx ( node , mid ) or
@@ -920,6 +935,8 @@ module MakeImpl<DataFlowParameter Lang> {
920
935
/* End: Stage 1 logic. */
921
936
}
922
937
938
+ private predicate sinkNode = Stage1:: sinkNode / 2 ;
939
+
923
940
pragma [ noinline]
924
941
private predicate localFlowStepNodeCand1 ( NodeEx node1 , NodeEx node2 ) {
925
942
Stage1:: revFlow ( node2 ) and
@@ -3894,7 +3911,10 @@ module MakeImpl<DataFlowParameter Lang> {
3894
3911
}
3895
3912
3896
3913
private predicate interestingCallableSink ( DataFlowCallable c ) {
3897
- exists ( Node n | Config:: isSink ( n , _) and c = getNodeEnclosingCallable ( n ) )
3914
+ exists ( Node n | c = getNodeEnclosingCallable ( n ) |
3915
+ Config:: isSink ( n , _) or
3916
+ Config:: isSink ( n )
3917
+ )
3898
3918
or
3899
3919
exists ( DataFlowCallable mid | interestingCallableSink ( mid ) and callableStep ( c , mid ) )
3900
3920
}
@@ -3926,8 +3946,10 @@ module MakeImpl<DataFlowParameter Lang> {
3926
3946
or
3927
3947
exists ( Node n |
3928
3948
ce2 = TCallableSink ( ) and
3929
- Config:: isSink ( n , _) and
3930
3949
ce1 = TCallable ( getNodeEnclosingCallable ( n ) )
3950
+ |
3951
+ Config:: isSink ( n , _) or
3952
+ Config:: isSink ( n )
3931
3953
)
3932
3954
}
3933
3955
0 commit comments