@@ -179,6 +179,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
179
179
180
180
Node asNode ( ) { this = TNodeNormal ( result ) }
181
181
182
+ /** Gets the corresponding Node if this is a normal node or its post-implicit read node. */
183
+ Node asNodeOrImplicitRead ( ) {
184
+ this = TNodeNormal ( result ) or this = TNodeImplicitRead ( result , true )
185
+ }
186
+
182
187
predicate isImplicitReadNode ( Node n , boolean hasRead ) { this = TNodeImplicitRead ( n , hasRead ) }
183
188
184
189
ParameterNode asParamReturnNode ( ) { this = TParamReturnNode ( result , _) }
@@ -247,6 +252,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
247
252
ReturnKindExt getKind ( ) { result = pos .getKind ( ) }
248
253
}
249
254
255
+ /** If `node` corresponds to a sink, gets the normal node for that sink. */
256
+ pragma [ nomagic]
257
+ private NodeEx toNormalSinkNodeEx ( NodeEx node ) {
258
+ exists ( Node n |
259
+ node .asNodeOrImplicitRead ( ) = n and
260
+ ( Config:: isSink ( n ) or Config:: isSink ( n , _) ) and
261
+ result .asNode ( ) = n
262
+ )
263
+ }
264
+
250
265
private predicate inBarrier ( NodeEx node ) {
251
266
exists ( Node n |
252
267
node .asNode ( ) = n and
@@ -266,7 +281,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
266
281
267
282
private predicate outBarrier ( NodeEx node ) {
268
283
exists ( Node n |
269
- node .asNode ( ) = n and
284
+ node .asNodeOrImplicitRead ( ) = n and
270
285
Config:: isBarrierOut ( n )
271
286
|
272
287
Config:: isSink ( n , _)
@@ -278,7 +293,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
278
293
pragma [ nomagic]
279
294
private predicate outBarrier ( NodeEx node , FlowState state ) {
280
295
exists ( Node n |
281
- node .asNode ( ) = n and
296
+ node .asNodeOrImplicitRead ( ) = n and
282
297
Config:: isBarrierOut ( n , state )
283
298
|
284
299
Config:: isSink ( n , state )
@@ -324,7 +339,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
324
339
325
340
pragma [ nomagic]
326
341
private predicate sinkNodeWithState ( NodeEx node , FlowState state ) {
327
- Config:: isSink ( node .asNode ( ) , state ) and
342
+ Config:: isSink ( node .asNodeOrImplicitRead ( ) , state ) and
328
343
not fullBarrier ( node ) and
329
344
not stateBarrier ( node , state )
330
345
}
@@ -386,7 +401,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
386
401
*/
387
402
private predicate additionalLocalFlowStep ( NodeEx node1 , NodeEx node2 , string model ) {
388
403
exists ( Node n1 , Node n2 |
389
- node1 .asNode ( ) = n1 and
404
+ node1 .asNodeOrImplicitRead ( ) = n1 and
390
405
node2 .asNode ( ) = n2 and
391
406
Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , pragma [ only_bind_into ] ( n2 ) , model ) and
392
407
getNodeEnclosingCallable ( n1 ) = getNodeEnclosingCallable ( n2 ) and
@@ -395,8 +410,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
395
410
or
396
411
exists ( Node n |
397
412
node1 .isImplicitReadNode ( n , true ) and
398
- node2 .asNode ( ) = n and
399
- not fullBarrier ( node2 ) and
413
+ node2 .isImplicitReadNode ( n , false ) and
400
414
model = ""
401
415
)
402
416
}
@@ -405,7 +419,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
405
419
NodeEx node1 , FlowState s1 , NodeEx node2 , FlowState s2
406
420
) {
407
421
exists ( Node n1 , Node n2 |
408
- node1 .asNode ( ) = n1 and
422
+ node1 .asNodeOrImplicitRead ( ) = n1 and
409
423
node2 .asNode ( ) = n2 and
410
424
Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , s1 , pragma [ only_bind_into ] ( n2 ) , s2 ) and
411
425
getNodeEnclosingCallable ( n1 ) = getNodeEnclosingCallable ( n2 ) and
@@ -431,7 +445,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
431
445
*/
432
446
private predicate additionalJumpStep ( NodeEx node1 , NodeEx node2 , string model ) {
433
447
exists ( Node n1 , Node n2 |
434
- node1 .asNode ( ) = n1 and
448
+ node1 .asNodeOrImplicitRead ( ) = n1 and
435
449
node2 .asNode ( ) = n2 and
436
450
Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , pragma [ only_bind_into ] ( n2 ) , model ) and
437
451
getNodeEnclosingCallable ( n1 ) != getNodeEnclosingCallable ( n2 ) and
@@ -442,7 +456,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
442
456
443
457
private predicate additionalJumpStateStep ( NodeEx node1 , FlowState s1 , NodeEx node2 , FlowState s2 ) {
444
458
exists ( Node n1 , Node n2 |
445
- node1 .asNode ( ) = n1 and
459
+ node1 .asNodeOrImplicitRead ( ) = n1 and
446
460
node2 .asNode ( ) = n2 and
447
461
Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , s1 , pragma [ only_bind_into ] ( n2 ) , s2 ) and
448
462
getNodeEnclosingCallable ( n1 ) != getNodeEnclosingCallable ( n2 ) and
@@ -735,7 +749,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
735
749
additional predicate sinkNode ( NodeEx node , FlowState state ) {
736
750
fwdFlow ( node ) and
737
751
fwdFlowState ( state ) and
738
- Config:: isSink ( node .asNode ( ) )
752
+ Config:: isSink ( node .asNodeOrImplicitRead ( ) )
739
753
or
740
754
fwdFlow ( node ) and
741
755
fwdFlowState ( state ) and
@@ -1058,7 +1072,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1058
1072
1059
1073
private predicate sinkModel ( NodeEx node , string model ) {
1060
1074
sinkNode ( node , _) and
1061
- exists ( Node n | n = node .asNode ( ) |
1075
+ exists ( Node n | n = node .asNodeOrImplicitRead ( ) |
1062
1076
knownSinkModel ( n , model )
1063
1077
or
1064
1078
not knownSinkModel ( n , _) and model = ""
@@ -3931,7 +3945,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3931
3945
TPathNodeSink ( NodeEx node , FlowState state ) {
3932
3946
exists ( PathNodeMid sink |
3933
3947
sink .isAtSink ( _) and
3934
- node = sink .getNodeEx ( ) and
3948
+ node = toNormalSinkNodeEx ( sink .getNodeEx ( ) ) and
3935
3949
state = sink .getState ( )
3936
3950
)
3937
3951
} or
@@ -4416,7 +4430,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
4416
4430
4417
4431
PathNodeSink projectToSink ( string model ) {
4418
4432
this .isAtSink ( model ) and
4419
- result .getNodeEx ( ) = node and
4433
+ result .getNodeEx ( ) = toNormalSinkNodeEx ( node ) and
4420
4434
result .getState ( ) = state
4421
4435
}
4422
4436
}
@@ -5309,7 +5323,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
5309
5323
private predicate revSinkNode ( NodeEx node , FlowState state ) {
5310
5324
sinkNodeWithState ( node , state )
5311
5325
or
5312
- Config:: isSink ( node .asNode ( ) ) and
5326
+ Config:: isSink ( node .asNodeOrImplicitRead ( ) ) and
5313
5327
relevantState ( state ) and
5314
5328
not fullBarrier ( node ) and
5315
5329
not stateBarrier ( node , state )
0 commit comments