@@ -275,7 +275,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
275
275
276
276
private predicate outBarrier ( NodeEx node ) {
277
277
exists ( Node n |
278
- node .asNode ( ) = n and
278
+ node .asNodeOrImplicitRead ( ) = n and
279
279
Config:: isBarrierOut ( n )
280
280
|
281
281
Config:: isSink ( n , _)
@@ -287,7 +287,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
287
287
pragma [ nomagic]
288
288
private predicate outBarrier ( NodeEx node , FlowState state ) {
289
289
exists ( Node n |
290
- node .asNode ( ) = n and
290
+ node .asNodeOrImplicitRead ( ) = n and
291
291
Config:: isBarrierOut ( n , state )
292
292
|
293
293
Config:: isSink ( n , state )
@@ -333,7 +333,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
333
333
334
334
pragma [ nomagic]
335
335
private predicate sinkNodeWithState ( NodeEx node , FlowState state ) {
336
- Config:: isSink ( node .asNode ( ) , state ) and
336
+ Config:: isSink ( node .asNodeOrImplicitRead ( ) , state ) and
337
337
not fullBarrier ( node ) and
338
338
not stateBarrier ( node , state )
339
339
}
@@ -395,26 +395,19 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
395
395
*/
396
396
private predicate additionalLocalFlowStep ( NodeEx node1 , NodeEx node2 , string model ) {
397
397
exists ( Node n1 , Node n2 |
398
- node1 .asNode ( ) = n1 and
398
+ node1 .asNodeOrImplicitRead ( ) = n1 and
399
399
node2 .asNode ( ) = n2 and
400
400
Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , pragma [ only_bind_into ] ( n2 ) , model ) and
401
401
getNodeEnclosingCallable ( n1 ) = getNodeEnclosingCallable ( n2 ) and
402
402
stepFilter ( node1 , node2 )
403
403
)
404
- or
405
- exists ( Node n |
406
- node1 .isImplicitReadNode ( n , true ) and
407
- node2 .asNode ( ) = n and
408
- not fullBarrier ( node2 ) and
409
- model = ""
410
- )
411
404
}
412
405
413
406
private predicate additionalLocalStateStep (
414
407
NodeEx node1 , FlowState s1 , NodeEx node2 , FlowState s2
415
408
) {
416
409
exists ( Node n1 , Node n2 |
417
- node1 .asNode ( ) = n1 and
410
+ node1 .asNodeOrImplicitRead ( ) = n1 and
418
411
node2 .asNode ( ) = n2 and
419
412
Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , s1 , pragma [ only_bind_into ] ( n2 ) , s2 ) and
420
413
getNodeEnclosingCallable ( n1 ) = getNodeEnclosingCallable ( n2 ) and
@@ -440,7 +433,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
440
433
*/
441
434
private predicate additionalJumpStep ( NodeEx node1 , NodeEx node2 , string model ) {
442
435
exists ( Node n1 , Node n2 |
443
- node1 .asNode ( ) = n1 and
436
+ node1 .asNodeOrImplicitRead ( ) = n1 and
444
437
node2 .asNode ( ) = n2 and
445
438
Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , pragma [ only_bind_into ] ( n2 ) , model ) and
446
439
getNodeEnclosingCallable ( n1 ) != getNodeEnclosingCallable ( n2 ) and
@@ -451,7 +444,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
451
444
452
445
private predicate additionalJumpStateStep ( NodeEx node1 , FlowState s1 , NodeEx node2 , FlowState s2 ) {
453
446
exists ( Node n1 , Node n2 |
454
- node1 .asNode ( ) = n1 and
447
+ node1 .asNodeOrImplicitRead ( ) = n1 and
455
448
node2 .asNode ( ) = n2 and
456
449
Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , s1 , pragma [ only_bind_into ] ( n2 ) , s2 ) and
457
450
getNodeEnclosingCallable ( n1 ) != getNodeEnclosingCallable ( n2 ) and
@@ -744,7 +737,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
744
737
additional predicate sinkNode ( NodeEx node , FlowState state ) {
745
738
fwdFlow ( node ) and
746
739
fwdFlowState ( state ) and
747
- Config:: isSink ( node .asNode ( ) )
740
+ Config:: isSink ( node .asNodeOrImplicitRead ( ) )
748
741
or
749
742
fwdFlow ( node ) and
750
743
fwdFlowState ( state ) and
@@ -1067,7 +1060,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1067
1060
1068
1061
private predicate sinkModel ( NodeEx node , string model ) {
1069
1062
sinkNode ( node , _) and
1070
- exists ( Node n | n = node .asNode ( ) |
1063
+ exists ( Node n | n = node .asNodeOrImplicitRead ( ) |
1071
1064
knownSinkModel ( n , model )
1072
1065
or
1073
1066
not knownSinkModel ( n , _) and model = ""
@@ -4866,7 +4859,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
4866
4859
private predicate revSinkNode ( NodeEx node , FlowState state ) {
4867
4860
sinkNodeWithState ( node , state )
4868
4861
or
4869
- Config:: isSink ( node .asNode ( ) ) and
4862
+ Config:: isSink ( node .asNodeOrImplicitRead ( ) ) and
4870
4863
relevantState ( state ) and
4871
4864
not fullBarrier ( node ) and
4872
4865
not stateBarrier ( node , state )
0 commit comments