@@ -561,6 +561,21 @@ 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 ( Content c , Ap tail |
571+ ap = apCons ( c , tail ) and
572+ fwdFlowConsCand ( _, ap , c , _, tail ) and
573+ ap != tail and // no need to report a longer length
574+ result = 1 + getAnApLengthLowerBound ( tail ) and
575+ result <= accessPathLimit ( )
576+ )
577+ }
578+
564579 pragma [ nomagic]
565580 private predicate fwdFlow0 (
566581 Nd node , Cc cc , SummaryCtx summaryCtx , Typ t , Ap ap , ApApprox apa , TypOption stored
@@ -594,7 +609,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
594609 exists ( Content c , Ap ap0 |
595610 fwdFlowStore ( _, _, ap0 , _, c , t , stored , node , cc , summaryCtx ) and
596611 ap = apCons ( c , ap0 ) and
597- apa = getApprox ( ap )
612+ apa = getApprox ( ap ) and
613+ if accessPathLimit ( ) > 1
614+ then getAnApLengthLowerBound ( ap0 ) < accessPathLimit ( )
615+ else any ( )
598616 )
599617 or
600618 // read
@@ -1320,6 +1338,20 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
13201338 fwdFlow ( node , _, _, _, ap , _)
13211339 }
13221340
1341+ pragma [ nomagic]
1342+ private int getAnApLengthLowerBoundRev ( Ap ap ) {
1343+ accessPathLimit ( ) > 1 and // `accessPathLimit() <= 1` is already checked in stages 1 and 2
1344+ ap instanceof ApNil and
1345+ result = 0
1346+ or
1347+ exists ( Ap tail |
1348+ revFlowConsCand ( ap , _, tail ) and
1349+ ap != tail and // no need to report a longer length
1350+ result = 1 + getAnApLengthLowerBoundRev ( tail ) and
1351+ result <= accessPathLimit ( )
1352+ )
1353+ }
1354+
13231355 pragma [ nomagic]
13241356 private predicate revFlow0 ( Nd node , ReturnCtx returnCtx , ApOption returnAp , Ap ap ) {
13251357 fwdFlow ( node , _, any ( SummaryCtx sinkCtx | sinkCtx .isASinkCtx ( ) ) , _, ap , _) and
@@ -1356,7 +1388,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
13561388 // read
13571389 exists ( Nd mid , Ap ap0 |
13581390 revFlow ( mid , returnCtx , returnAp , ap0 ) and
1359- readStepFwd ( node , ap , _, mid , ap0 )
1391+ readStepFwd ( node , ap , _, mid , ap0 ) and
1392+ if accessPathLimit ( ) > 1
1393+ then getAnApLengthLowerBoundRev ( ap0 ) < accessPathLimit ( )
1394+ else any ( )
13601395 )
13611396 or
13621397 // flow into a callable
0 commit comments