@@ -173,6 +173,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
173173
174174 Node asNode ( ) { this = TNodeNormal ( result ) }
175175
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+
176181 predicate isImplicitReadNode ( Node n , boolean hasRead ) { this = TNodeImplicitRead ( n , hasRead ) }
177182
178183 ParameterNode asParamReturnNode ( ) { this = TParamReturnNode ( result , _) }
@@ -241,6 +246,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
241246 ReturnKindExt getKind ( ) { result = pos .getKind ( ) }
242247 }
243248
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+
244259 private predicate inBarrier ( NodeEx node ) {
245260 exists ( Node n |
246261 node .asNode ( ) = n and
@@ -260,7 +275,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
260275
261276 private predicate outBarrier ( NodeEx node ) {
262277 exists ( Node n |
263- node .asNode ( ) = n and
278+ node .asNodeOrImplicitRead ( ) = n and
264279 Config:: isBarrierOut ( n )
265280 |
266281 Config:: isSink ( n , _)
@@ -272,7 +287,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
272287 pragma [ nomagic]
273288 private predicate outBarrier ( NodeEx node , FlowState state ) {
274289 exists ( Node n |
275- node .asNode ( ) = n and
290+ node .asNodeOrImplicitRead ( ) = n and
276291 Config:: isBarrierOut ( n , state )
277292 |
278293 Config:: isSink ( n , state )
@@ -318,7 +333,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
318333
319334 pragma [ nomagic]
320335 private predicate sinkNodeWithState ( NodeEx node , FlowState state ) {
321- Config:: isSink ( node .asNode ( ) , state ) and
336+ Config:: isSink ( node .asNodeOrImplicitRead ( ) , state ) and
322337 not fullBarrier ( node ) and
323338 not stateBarrier ( node , state )
324339 }
@@ -380,26 +395,19 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
380395 */
381396 private predicate additionalLocalFlowStep ( NodeEx node1 , NodeEx node2 , string model ) {
382397 exists ( Node n1 , Node n2 |
383- node1 .asNode ( ) = n1 and
398+ node1 .asNodeOrImplicitRead ( ) = n1 and
384399 node2 .asNode ( ) = n2 and
385400 Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , pragma [ only_bind_into ] ( n2 ) , model ) and
386401 getNodeEnclosingCallable ( n1 ) = getNodeEnclosingCallable ( n2 ) and
387402 stepFilter ( node1 , node2 )
388403 )
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- )
396404 }
397405
398406 private predicate additionalLocalStateStep (
399407 NodeEx node1 , FlowState s1 , NodeEx node2 , FlowState s2
400408 ) {
401409 exists ( Node n1 , Node n2 |
402- node1 .asNode ( ) = n1 and
410+ node1 .asNodeOrImplicitRead ( ) = n1 and
403411 node2 .asNode ( ) = n2 and
404412 Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , s1 , pragma [ only_bind_into ] ( n2 ) , s2 ) and
405413 getNodeEnclosingCallable ( n1 ) = getNodeEnclosingCallable ( n2 ) and
@@ -425,7 +433,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
425433 */
426434 private predicate additionalJumpStep ( NodeEx node1 , NodeEx node2 , string model ) {
427435 exists ( Node n1 , Node n2 |
428- node1 .asNode ( ) = n1 and
436+ node1 .asNodeOrImplicitRead ( ) = n1 and
429437 node2 .asNode ( ) = n2 and
430438 Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , pragma [ only_bind_into ] ( n2 ) , model ) and
431439 getNodeEnclosingCallable ( n1 ) != getNodeEnclosingCallable ( n2 ) and
@@ -436,7 +444,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
436444
437445 private predicate additionalJumpStateStep ( NodeEx node1 , FlowState s1 , NodeEx node2 , FlowState s2 ) {
438446 exists ( Node n1 , Node n2 |
439- node1 .asNode ( ) = n1 and
447+ node1 .asNodeOrImplicitRead ( ) = n1 and
440448 node2 .asNode ( ) = n2 and
441449 Config:: isAdditionalFlowStep ( pragma [ only_bind_into ] ( n1 ) , s1 , pragma [ only_bind_into ] ( n2 ) , s2 ) and
442450 getNodeEnclosingCallable ( n1 ) != getNodeEnclosingCallable ( n2 ) and
@@ -729,7 +737,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
729737 additional predicate sinkNode ( NodeEx node , FlowState state ) {
730738 fwdFlow ( node ) and
731739 fwdFlowState ( state ) and
732- Config:: isSink ( node .asNode ( ) )
740+ Config:: isSink ( node .asNodeOrImplicitRead ( ) )
733741 or
734742 fwdFlow ( node ) and
735743 fwdFlowState ( state ) and
@@ -1052,7 +1060,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
10521060
10531061 private predicate sinkModel ( NodeEx node , string model ) {
10541062 sinkNode ( node , _) and
1055- exists ( Node n | n = node .asNode ( ) |
1063+ exists ( Node n | n = node .asNodeOrImplicitRead ( ) |
10561064 knownSinkModel ( n , model )
10571065 or
10581066 not knownSinkModel ( n , _) and model = ""
@@ -2549,7 +2557,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
25492557 TPathNodeSink ( NodeEx node , FlowState state ) {
25502558 exists ( PathNodeMid sink |
25512559 sink .isAtSink ( ) and
2552- node = sink .getNodeEx ( ) and
2560+ node = toNormalSinkNodeEx ( sink .getNodeEx ( ) ) and
25532561 state = sink .getState ( )
25542562 )
25552563 } or
@@ -2772,7 +2780,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
27722780 PathNodeSink projectToSink ( string model ) {
27732781 this .isAtSink ( ) and
27742782 sinkModel ( node , model ) and
2775- result .getNodeEx ( ) = node and
2783+ result .getNodeEx ( ) = toNormalSinkNodeEx ( node ) and
27762784 result .getState ( ) = state
27772785 }
27782786 }
@@ -4851,7 +4859,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
48514859 private predicate revSinkNode ( NodeEx node , FlowState state ) {
48524860 sinkNodeWithState ( node , state )
48534861 or
4854- Config:: isSink ( node .asNode ( ) ) and
4862+ Config:: isSink ( node .asNodeOrImplicitRead ( ) ) and
48554863 relevantState ( state ) and
48564864 not fullBarrier ( node ) and
48574865 not stateBarrier ( node , state )
0 commit comments