@@ -561,6 +561,20 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
561561 )
562562 }
563563
564+ pragma [ nomagic]
565+ private int getAnApLengthLowerBound ( Ap ap ) {
566+ accessPathLimit ( ) > 1 and // `accessPathLimit() <= 1` is already checked in stages 1 and 2
567+ ap instanceof ApNil and
568+ result = 0
569+ or
570+ exists ( Ap tail |
571+ fwdFlowConsCand ( _, ap , _, _, tail ) and
572+ ap != tail and // no need to report a longer length
573+ result = 1 + getAnApLengthLowerBound ( tail ) and
574+ result <= accessPathLimit ( )
575+ )
576+ }
577+
564578 pragma [ nomagic]
565579 private predicate fwdFlow0 (
566580 Nd node , Cc cc , SummaryCtx summaryCtx , Typ t , Ap ap , ApApprox apa , TypOption stored
@@ -594,7 +608,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
594608 exists ( Content c , Ap ap0 |
595609 fwdFlowStore ( _, _, ap0 , _, c , t , stored , node , cc , summaryCtx ) and
596610 ap = apCons ( c , ap0 ) and
597- apa = getApprox ( ap )
611+ apa = getApprox ( ap ) and
612+ if accessPathLimit ( ) > 1
613+ then getAnApLengthLowerBound ( ap0 ) < accessPathLimit ( )
614+ else any ( )
598615 )
599616 or
600617 // read
@@ -1320,6 +1337,20 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
13201337 fwdFlow ( node , _, _, _, ap , _)
13211338 }
13221339
1340+ pragma [ nomagic]
1341+ private int getAnApLengthLowerBoundRev ( Ap ap ) {
1342+ accessPathLimit ( ) > 1 and // `accessPathLimit() <= 1` is already checked in stages 1 and 2
1343+ ap instanceof ApNil and
1344+ result = 0
1345+ or
1346+ exists ( Ap tail |
1347+ revFlowConsCand ( ap , _, tail ) and
1348+ ap != tail and // no need to report a longer length
1349+ result = 1 + getAnApLengthLowerBoundRev ( tail ) and
1350+ result <= accessPathLimit ( )
1351+ )
1352+ }
1353+
13231354 pragma [ nomagic]
13241355 private predicate revFlow0 ( Nd node , ReturnCtx returnCtx , ApOption returnAp , Ap ap ) {
13251356 fwdFlow ( node , _, any ( SummaryCtx sinkCtx | sinkCtx .isASinkCtx ( ) ) , _, ap , _) and
@@ -1356,7 +1387,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
13561387 // read
13571388 exists ( Nd mid , Ap ap0 |
13581389 revFlow ( mid , returnCtx , returnAp , ap0 ) and
1359- readStepFwd ( node , ap , _, mid , ap0 )
1390+ readStepFwd ( node , ap , _, mid , ap0 ) and
1391+ if accessPathLimit ( ) > 1
1392+ then getAnApLengthLowerBoundRev ( ap0 ) < accessPathLimit ( )
1393+ else any ( )
13601394 )
13611395 or
13621396 // flow into a callable
0 commit comments