@@ -370,6 +370,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
370370 }
371371
372372 class Ap {
373+ /** Gets the tracked length of this access path, if any. */
374+ int length ( ) ;
375+
373376 string toString ( ) ;
374377 }
375378
@@ -563,10 +566,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
563566
564567 pragma [ nomagic]
565568 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+ accessPathLimit ( ) != 0 and // `accessPathLimit() = 0` is already checked in `useFieldFlow`
570+ result = ap .length ( )
569571 or
572+ not exists ( ap .length ( ) ) and
570573 exists ( Ap tail |
571574 fwdFlowConsCand ( _, ap , _, _, tail ) and
572575 ap != tail and // no need to report a longer length
@@ -609,7 +612,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
609612 fwdFlowStore ( _, _, ap0 , _, c , t , stored , node , cc , summaryCtx ) and
610613 ap = apCons ( c , ap0 ) and
611614 apa = getApprox ( ap ) and
612- if accessPathLimit ( ) > 1
615+ if accessPathLimit ( ) != 0
613616 then getAnApLengthLowerBound ( ap0 ) < accessPathLimit ( )
614617 else any ( )
615618 )
@@ -1339,10 +1342,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
13391342
13401343 pragma [ nomagic]
13411344 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+ accessPathLimit ( ) != 0 and // `accessPathLimit() = 0` is already checked in `useFieldFlow`
1346+ result = ap .length ( )
13451347 or
1348+ not exists ( ap .length ( ) ) and
13461349 exists ( Ap tail |
13471350 revFlowConsCand ( ap , _, tail ) and
13481351 ap != tail and // no need to report a longer length
@@ -1388,7 +1391,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
13881391 exists ( Nd mid , Ap ap0 |
13891392 revFlow ( mid , returnCtx , returnAp , ap0 ) and
13901393 readStepFwd ( node , ap , _, mid , ap0 ) and
1391- if accessPathLimit ( ) > 1
1394+ if accessPathLimit ( ) != 0
13921395 then getAnApLengthLowerBoundRev ( ap0 ) < accessPathLimit ( )
13931396 else any ( )
13941397 )
@@ -2770,7 +2773,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
27702773
27712774 class Typ = Unit ;
27722775
2773- class Ap = Boolean ;
2776+ class Ap extends Boolean {
2777+ int length ( ) { this = false and result = 0 }
2778+ }
27742779
27752780 class ApNil extends Ap {
27762781 ApNil ( ) { this = false }
@@ -2859,12 +2864,19 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
28592864 Typ getTyp ( Type t ) { any ( ) }
28602865
28612866 bindingset [ c, tail]
2862- Ap apCons ( Content c , Ap tail ) { result .getAHead ( ) = c and exists ( tail ) }
2867+ Ap apCons ( Content c , Ap tail ) {
2868+ exists ( int length | result .getAHead ( length ) = c |
2869+ length = 1 and
2870+ tail instanceof ApNil
2871+ or
2872+ tail = TApproxFrontHead ( _, length - 1 )
2873+ )
2874+ }
28632875
28642876 class ApHeadContent = ContentApprox ;
28652877
28662878 pragma [ noinline]
2867- ApHeadContent getHeadContent ( Ap ap ) { result = ap .getHead ( ) }
2879+ ApHeadContent getHeadContent ( Ap ap ) { result = ap .getHead ( _ ) }
28682880
28692881 predicate projectToHeadContent = getContentApproxCached / 1 ;
28702882
@@ -2910,7 +2922,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
29102922 PrevStage:: revFlow ( node ) and
29112923 PrevStage:: readStepCand ( _, c , _) and
29122924 Stage1:: expectsContentEx ( node , c ) and
2913- c = ap .getAHead ( )
2925+ c = ap .getAHead ( _ )
29142926 )
29152927 }
29162928
@@ -2961,12 +2973,19 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
29612973 Typ getTyp ( Type t ) { any ( ) }
29622974
29632975 bindingset [ c, tail]
2964- Ap apCons ( Content c , Ap tail ) { result .getHead ( ) = c and exists ( tail ) }
2976+ Ap apCons ( Content c , Ap tail ) {
2977+ exists ( int length | result .getHead ( length ) = c |
2978+ length = 1 and
2979+ tail instanceof ApNil
2980+ or
2981+ tail = TFrontHead ( _, length - 1 )
2982+ )
2983+ }
29652984
29662985 class ApHeadContent = Content ;
29672986
29682987 pragma [ noinline]
2969- ApHeadContent getHeadContent ( Ap ap ) { result = ap .getHead ( ) }
2988+ ApHeadContent getHeadContent ( Ap ap ) { result = ap .getHead ( _ ) }
29702989
29712990 ApHeadContent projectToHeadContent ( Content c ) { result = c }
29722991
@@ -3012,19 +3031,19 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
30123031 // When `node` is the target of a store, we interpret `clearsContent` as
30133032 // only pertaining to _earlier_ store steps. In this case, we need to postpone
30143033 // checking `clearsContent` to the step creation.
3015- clearContent ( node , ap .getHead ( ) , false )
3034+ clearContent ( node , ap .getHead ( _ ) , false )
30163035 }
30173036
30183037 pragma [ nomagic]
3019- private predicate clearExceptStore ( Nd node , Ap ap ) { clearContent ( node , ap .getHead ( ) , true ) }
3038+ private predicate clearExceptStore ( Nd node , Ap ap ) { clearContent ( node , ap .getHead ( _ ) , true ) }
30203039
30213040 pragma [ nomagic]
30223041 private predicate expectsContentCand ( Nd node , Ap ap ) {
30233042 exists ( Content c |
30243043 PrevStage:: revFlow ( node ) and
30253044 PrevStage:: readStepCand ( _, c , _) and
30263045 Stage1:: expectsContentEx ( node , c ) and
3027- c = ap .getHead ( )
3046+ c = ap .getHead ( _ )
30283047 )
30293048 }
30303049
@@ -3059,9 +3078,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
30593078 tails = strictcount ( AccessPathFront apf | Stage4:: consCand ( c , apf ) ) and
30603079 nodes =
30613080 strictcount ( Nd n |
3062- Stage4:: revFlow ( n , any ( AccessPathFrontHead apf | apf .getHead ( ) = c ) )
3081+ Stage4:: revFlow ( n , any ( AccessPathFrontHead apf | apf .getHead ( _ ) = c ) )
30633082 or
3064- Stage4:: nodeMayUseSummary ( n , any ( AccessPathFrontHead apf | apf .getHead ( ) = c ) )
3083+ Stage4:: nodeMayUseSummary ( n , any ( AccessPathFrontHead apf | apf .getHead ( _ ) = c ) )
30653084 ) and
30663085 accessPathApproxCostLimits ( apLimit , tupleLimit ) and
30673086 apLimit < tails and
@@ -3077,7 +3096,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
30773096 not expensiveLen2unfolding ( c )
30783097 } or
30793098 TConsCons ( Content c1 , Content c2 , int len ) {
3080- Stage4:: consCand ( c1 , TFrontHead ( c2 ) ) and
3099+ Stage4:: consCand ( c1 , TFrontHead ( c2 , _ ) ) and
30813100 len in [ 2 .. Config:: accessPathLimit ( ) ] and
30823101 not expensiveLen2unfolding ( c1 )
30833102 } or
@@ -3098,7 +3117,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
30983117
30993118 abstract Content getHead ( ) ;
31003119
3101- abstract int len ( ) ;
3120+ abstract int length ( ) ;
31023121
31033122 abstract AccessPathFront getFront ( ) ;
31043123
@@ -3111,7 +3130,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
31113130
31123131 override Content getHead ( ) { none ( ) }
31133132
3114- override int len ( ) { result = 0 }
3133+ override int length ( ) { result = 0 }
31153134
31163135 override AccessPathFront getFront ( ) { result = TFrontNil ( ) }
31173136
@@ -3129,9 +3148,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
31293148
31303149 override Content getHead ( ) { result = c }
31313150
3132- override int len ( ) { result = 1 }
3151+ override int length ( ) { result = 1 }
31333152
3134- override AccessPathFront getFront ( ) { result = TFrontHead ( c ) }
3153+ override AccessPathFront getFront ( ) { result = TFrontHead ( c , 1 ) }
31353154
31363155 override predicate isCons ( Content head , AccessPathApprox tail ) { head = c and tail = TNil ( ) }
31373156 }
@@ -3151,9 +3170,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
31513170
31523171 override Content getHead ( ) { result = c1 }
31533172
3154- override int len ( ) { result = len }
3173+ override int length ( ) { result = len }
31553174
3156- override AccessPathFront getFront ( ) { result = TFrontHead ( c1 ) }
3175+ override AccessPathFront getFront ( ) { result = TFrontHead ( c1 , len ) }
31573176
31583177 override predicate isCons ( Content head , AccessPathApprox tail ) {
31593178 head = c1 and
@@ -3182,14 +3201,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
31823201
31833202 override Content getHead ( ) { result = c }
31843203
3185- override int len ( ) { result = len }
3204+ override int length ( ) { result = len }
31863205
3187- override AccessPathFront getFront ( ) { result = TFrontHead ( c ) }
3206+ override AccessPathFront getFront ( ) { result = TFrontHead ( c , len ) }
31883207
31893208 override predicate isCons ( Content head , AccessPathApprox tail ) {
31903209 head = c and
31913210 (
3192- exists ( Content c2 | Stage4:: consCand ( c , TFrontHead ( c2 ) ) |
3211+ exists ( Content c2 | Stage4:: consCand ( c , TFrontHead ( c2 , len - 1 ) ) |
31933212 tail = TConsCons ( c2 , _, len - 1 )
31943213 or
31953214 len = 2 and
@@ -3288,7 +3307,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
32883307
32893308 pragma [ nomagic]
32903309 private predicate stage5ConsCand ( Content c , AccessPathFront apf , int len ) {
3291- Stage5:: consCand ( c , any ( AccessPathApprox ap | ap .getFront ( ) = apf and ap .len ( ) = len - 1 ) )
3310+ Stage5:: consCand ( c , any ( AccessPathApprox ap | ap .getFront ( ) = apf and ap .length ( ) = len - 1 ) )
32923311 }
32933312
32943313 /**
@@ -3297,7 +3316,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
32973316 private int count1to2unfold ( AccessPathApproxCons1 apa ) {
32983317 exists ( Content c , int len |
32993318 c = apa .getHead ( ) and
3300- len = apa .len ( ) and
3319+ len = apa .length ( ) and
33013320 result = strictcount ( AccessPathFront apf | stage5ConsCand ( c , apf , len ) )
33023321 )
33033322 }
@@ -3392,7 +3411,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
33923411 exists ( AccessPathApproxCons apa , AccessPathApprox tail |
33933412 evalUnfold ( apa , false ) and
33943413 not expensiveLen1to2unfolding ( apa ) and
3395- apa .len ( ) = len and
3414+ apa .length ( ) = len and
33963415 hasTail ( apa , tail ) and
33973416 head1 = apa .getHead ( ) and
33983417 head2 = tail .getHead ( )
@@ -3402,7 +3421,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
34023421 exists ( AccessPathApproxCons apa |
34033422 evalUnfold ( apa , false ) and
34043423 expensiveLen1to2unfolding ( apa ) and
3405- apa .len ( ) = len and
3424+ apa .length ( ) = len and
34063425 head = apa .getHead ( )
34073426 )
34083427 }
@@ -3531,7 +3550,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35313550
35323551 override predicate isCons ( Content head , AccessPath tail ) { head = head_ and tail = tail_ }
35333552
3534- override AccessPathFrontHead getFront ( ) { result = TFrontHead ( head_ ) }
3553+ override AccessPathFrontHead getFront ( ) { result = TFrontHead ( head_ , this . length ( ) ) }
35353554
35363555 override AccessPathApproxCons getApprox ( ) {
35373556 result = TConsNil ( head_ ) and tail_ = TAccessPathNil ( )
@@ -3586,7 +3605,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35863605 tail .length ( ) = len - 1
35873606 }
35883607
3589- override AccessPathFrontHead getFront ( ) { result = TFrontHead ( head1 ) }
3608+ override AccessPathFrontHead getFront ( ) { result = TFrontHead ( head1 , len ) }
35903609
35913610 override AccessPathApproxCons getApprox ( ) {
35923611 result = TConsCons ( head1 , head2 , len ) or
@@ -3618,7 +3637,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
36183637 tail .length ( ) = len - 1
36193638 }
36203639
3621- override AccessPathFrontHead getFront ( ) { result = TFrontHead ( head_ ) }
3640+ override AccessPathFrontHead getFront ( ) { result = TFrontHead ( head_ , len ) }
36223641
36233642 override AccessPathApproxCons getApprox ( ) { result = TCons1 ( head_ , len ) }
36243643
0 commit comments