@@ -173,6 +173,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
173
173
174
174
Node asNode ( ) { this = TNodeNormal ( result ) }
175
175
176
+ /** Gets the corresponding Node if this is a normal node or its post-implicit read node. */
177
+ Node asNodeOrImplicitRead ( ) {
178
+ this = TNodeNormal ( result ) or this = TNodeImplicitRead ( result , true )
179
+ }
180
+
176
181
predicate isImplicitReadNode ( Node n , boolean hasRead ) { this = TNodeImplicitRead ( n , hasRead ) }
177
182
178
183
ParameterNode asParamReturnNode ( ) { this = TParamReturnNode ( result , _) }
@@ -241,6 +246,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
241
246
ReturnKindExt getKind ( ) { result = pos .getKind ( ) }
242
247
}
243
248
249
+ /** If `node` corresponds to a sink, gets the normal node for that sink. */
250
+ pragma [ nomagic]
251
+ private NodeEx toNormalSinkNodeEx ( NodeEx node ) {
252
+ exists ( Node n |
253
+ node .asNodeOrImplicitRead ( ) = n and
254
+ ( Config:: isSink ( n ) or Config:: isSink ( n , _) ) and
255
+ result .asNode ( ) = n
256
+ )
257
+ }
258
+
244
259
private predicate inBarrier ( NodeEx node ) {
245
260
exists ( Node n |
246
261
node .asNode ( ) = n and
@@ -260,7 +275,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
260
275
261
276
private predicate outBarrier ( NodeEx node ) {
262
277
exists ( Node n |
263
- node .asNode ( ) = n and
278
+ node .asNodeOrImplicitRead ( ) = n and
264
279
Config:: isBarrierOut ( n )
265
280
|
266
281
Config:: isSink ( n , _)
@@ -272,7 +287,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
272
287
pragma [ nomagic]
273
288
private predicate outBarrier ( NodeEx node , FlowState state ) {
274
289
exists ( Node n |
275
- node .asNode ( ) = n and
290
+ node .asNodeOrImplicitRead ( ) = n and
276
291
Config:: isBarrierOut ( n , state )
277
292
|
278
293
Config:: isSink ( n , state )
@@ -318,7 +333,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
318
333
319
334
pragma [ nomagic]
320
335
private predicate sinkNodeWithState ( NodeEx node , FlowState state ) {
321
- Config:: isSink ( node .asNode ( ) , state ) and
336
+ Config:: isSink ( node .asNodeOrImplicitRead ( ) , state ) and
322
337
not fullBarrier ( node ) and
323
338
not stateBarrier ( node , state )
324
339
}
@@ -380,26 +395,19 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
380
395
*/
381
396
private predicate additionalLocalFlowStep ( NodeEx node1 , NodeEx node2 , string model ) {
382
397
exists ( Node n1 , Node n2 |
383
- node1 .asNode ( ) = n1 and
398
+ node1 .asNodeOrImplicitRead ( ) = n1 and
384
399
node2 .asNode ( ) = n2 and
385
400
Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , pragma [ only_bind_into ] ( n2 ) , model ) and
386
401
getNodeEnclosingCallable ( n1 ) = getNodeEnclosingCallable ( n2 ) and
387
402
stepFilter ( node1 , node2 )
388
403
)
389
- or
390
- exists ( Node n |
391
- node1 .isImplicitReadNode ( n , true ) and
392
- node2 .asNode ( ) = n and
393
- not fullBarrier ( node2 ) and
394
- model = ""
395
- )
396
404
}
397
405
398
406
private predicate additionalLocalStateStep (
399
407
NodeEx node1 , FlowState s1 , NodeEx node2 , FlowState s2
400
408
) {
401
409
exists ( Node n1 , Node n2 |
402
- node1 .asNode ( ) = n1 and
410
+ node1 .asNodeOrImplicitRead ( ) = n1 and
403
411
node2 .asNode ( ) = n2 and
404
412
Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , s1 , pragma [ only_bind_into ] ( n2 ) , s2 ) and
405
413
getNodeEnclosingCallable ( n1 ) = getNodeEnclosingCallable ( n2 ) and
@@ -425,7 +433,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
425
433
*/
426
434
private predicate additionalJumpStep ( NodeEx node1 , NodeEx node2 , string model ) {
427
435
exists ( Node n1 , Node n2 |
428
- node1 .asNode ( ) = n1 and
436
+ node1 .asNodeOrImplicitRead ( ) = n1 and
429
437
node2 .asNode ( ) = n2 and
430
438
Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , pragma [ only_bind_into ] ( n2 ) , model ) and
431
439
getNodeEnclosingCallable ( n1 ) != getNodeEnclosingCallable ( n2 ) and
@@ -436,7 +444,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
436
444
437
445
private predicate additionalJumpStateStep ( NodeEx node1 , FlowState s1 , NodeEx node2 , FlowState s2 ) {
438
446
exists ( Node n1 , Node n2 |
439
- node1 .asNode ( ) = n1 and
447
+ node1 .asNodeOrImplicitRead ( ) = n1 and
440
448
node2 .asNode ( ) = n2 and
441
449
Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , s1 , pragma [ only_bind_into ] ( n2 ) , s2 ) and
442
450
getNodeEnclosingCallable ( n1 ) != getNodeEnclosingCallable ( n2 ) and
@@ -729,7 +737,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
729
737
additional predicate sinkNode ( NodeEx node , FlowState state ) {
730
738
fwdFlow ( node ) and
731
739
fwdFlowState ( state ) and
732
- Config:: isSink ( node .asNode ( ) )
740
+ Config:: isSink ( node .asNodeOrImplicitRead ( ) )
733
741
or
734
742
fwdFlow ( node ) and
735
743
fwdFlowState ( state ) and
@@ -1052,7 +1060,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1052
1060
1053
1061
private predicate sinkModel ( NodeEx node , string model ) {
1054
1062
sinkNode ( node , _) and
1055
- exists ( Node n | n = node .asNode ( ) |
1063
+ exists ( Node n | n = node .asNodeOrImplicitRead ( ) |
1056
1064
knownSinkModel ( n , model )
1057
1065
or
1058
1066
not knownSinkModel ( n , _) and model = ""
@@ -2549,7 +2557,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2549
2557
TPathNodeSink ( NodeEx node , FlowState state ) {
2550
2558
exists ( PathNodeMid sink |
2551
2559
sink .isAtSink ( ) and
2552
- node = sink .getNodeEx ( ) and
2560
+ node = toNormalSinkNodeEx ( sink .getNodeEx ( ) ) and
2553
2561
state = sink .getState ( )
2554
2562
)
2555
2563
} or
@@ -2772,7 +2780,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2772
2780
PathNodeSink projectToSink ( string model ) {
2773
2781
this .isAtSink ( ) and
2774
2782
sinkModel ( node , model ) and
2775
- result .getNodeEx ( ) = node and
2783
+ result .getNodeEx ( ) = toNormalSinkNodeEx ( node ) and
2776
2784
result .getState ( ) = state
2777
2785
}
2778
2786
}
@@ -4851,7 +4859,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
4851
4859
private predicate revSinkNode ( NodeEx node , FlowState state ) {
4852
4860
sinkNodeWithState ( node , state )
4853
4861
or
4854
- Config:: isSink ( node .asNode ( ) ) and
4862
+ Config:: isSink ( node .asNodeOrImplicitRead ( ) ) and
4855
4863
relevantState ( state ) and
4856
4864
not fullBarrier ( node ) and
4857
4865
not stateBarrier ( node , state )
0 commit comments