@@ -1278,8 +1278,10 @@ module MakeImpl<InputSig Lang> {
1278
1278
bindingset [ node, ap]
1279
1279
predicate nodeMayFlowNotThrough ( NodeEx node , ApApprox ap ) ;
1280
1280
1281
- bindingset [ node, state, t0, ap, inSummaryCtx]
1282
- predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx ) ;
1281
+ bindingset [ node, state, origT, t0, ap, inSummaryCtx]
1282
+ predicate filter (
1283
+ NodeEx node , FlowState state , Typ origT , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx
1284
+ ) ;
1283
1285
1284
1286
bindingset [ typ, contentType]
1285
1287
predicate typecheckStore ( Typ typ , DataFlowType contentType ) ;
@@ -1367,7 +1369,13 @@ module MakeImpl<InputSig Lang> {
1367
1369
( cc instanceof CcNoCall or Param:: nodeMayFlowNotThrough ( node , apa ) ) and
1368
1370
inSummaryCtx = false
1369
1371
) and
1370
- filter ( node , state , t0 , ap , t , inSummaryCtx ) and
1372
+ exists ( Typ origT1 |
1373
+ origT1 = origT0 .asSome ( )
1374
+ or
1375
+ origT0 .isNone ( ) and origT1 = t0
1376
+ |
1377
+ filter ( node , state , origT1 , t0 , ap , t , inSummaryCtx )
1378
+ ) and
1371
1379
// origT.asSome() = t
1372
1380
if t != t0 and origT0 .isNone ( ) and not ap instanceof ApNil
1373
1381
then origT .asSome ( ) = t0
@@ -2395,20 +2403,33 @@ module MakeImpl<InputSig Lang> {
2395
2403
)
2396
2404
}
2397
2405
2406
+ pragma [ nomagic]
2407
+ private predicate nodeMayFlowThrough0 (
2408
+ ParamNode p , Ap argAp , ApOption argApO , ReturnPosition pos , Ap returnAp ,
2409
+ ApOption returnApO
2410
+ ) {
2411
+ // revFlow(node, _, TReturnCtxMaybeFlowThrough(_), _, ap)
2412
+ exists ( ParamNodeEx param |
2413
+ p = param .asNode ( ) and
2414
+ returnFlowsThrough ( _, pos , _, _, param , _, argAp , returnAp ) and
2415
+ parameterFlowsThroughRev ( param , argAp , pos , returnAp ) and
2416
+ argApO = apSome ( argAp ) and
2417
+ returnApO = apSome ( returnAp )
2418
+ )
2419
+ }
2420
+
2398
2421
// pragma[nomagic]
2399
2422
// predicate nodeMayFlowThrough(NodeEx node, Ap ap) {
2400
2423
// revFlow(node, _, TReturnCtxMaybeFlowThrough(_), _, ap)
2401
2424
// }
2402
2425
pragma [ nomagic]
2403
2426
additional predicate nodeMayFlowThrough ( ParamNode p , Ap argAp , NodeEx node , Ap ap ) {
2404
2427
// revFlow(node, _, TReturnCtxMaybeFlowThrough(_), _, ap)
2405
- exists ( ReturnPosition pos , Ap returnAp , ParamNodeEx param |
2406
- p = param .asNode ( ) and
2407
- returnFlowsThrough ( _, pos , _, _, param , _, argAp , returnAp ) and
2408
- parameterFlowsThroughRev ( param , argAp , pos , returnAp ) and
2409
- revFlow ( pragma [ only_bind_into ] ( node ) , _, TReturnCtxMaybeFlowThrough ( pos ) ,
2410
- apSome ( returnAp ) , pragma [ only_bind_into ] ( ap ) ) and
2411
- fwdFlow ( pragma [ only_bind_into ] ( node ) , _, _, TParamNodeSome ( p ) , _, apSome ( argAp ) , _, _,
2428
+ exists ( ApOption argApO , ReturnPosition pos , Ap returnAp , ApOption returnApO |
2429
+ nodeMayFlowThrough0 ( p , argAp , argApO , pos , returnAp , returnApO ) and
2430
+ revFlow ( pragma [ only_bind_into ] ( node ) , _, TReturnCtxMaybeFlowThrough ( pos ) , returnApO ,
2431
+ pragma [ only_bind_into ] ( ap ) ) and
2432
+ fwdFlow ( pragma [ only_bind_into ] ( node ) , _, _, TParamNodeSome ( p ) , _, argApO , _, _,
2412
2433
pragma [ only_bind_into ] ( ap ) , _)
2413
2434
)
2414
2435
}
@@ -2745,9 +2766,12 @@ module MakeImpl<InputSig Lang> {
2745
2766
)
2746
2767
}
2747
2768
2748
- bindingset [ node, state, t0, ap, inSummaryCtx]
2749
- predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx ) {
2769
+ bindingset [ node, state, origT, t0, ap, inSummaryCtx]
2770
+ predicate filter (
2771
+ NodeEx node , FlowState state , Typ origT , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx
2772
+ ) {
2750
2773
PrevStage:: revFlowState ( state ) and
2774
+ exists ( origT ) and
2751
2775
t0 = t and
2752
2776
exists ( ap ) and
2753
2777
not stateBarrier ( node , state ) and
@@ -3078,9 +3102,12 @@ module MakeImpl<InputSig Lang> {
3078
3102
)
3079
3103
}
3080
3104
3081
- bindingset [ node, state, t0, ap, inSummaryCtx]
3082
- predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx ) {
3105
+ bindingset [ node, state, origT, t0, ap, inSummaryCtx]
3106
+ predicate filter (
3107
+ NodeEx node , FlowState state , Typ origT , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx
3108
+ ) {
3083
3109
exists ( state ) and
3110
+ exists ( origT ) and
3084
3111
t0 = t and
3085
3112
exists ( ap ) and
3086
3113
not stateBarrier ( node , state ) and
@@ -3164,9 +3191,12 @@ module MakeImpl<InputSig Lang> {
3164
3191
)
3165
3192
}
3166
3193
3167
- bindingset [ node, state, t0, ap, inSummaryCtx]
3168
- predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx ) {
3194
+ bindingset [ node, state, origT, t0, ap, inSummaryCtx]
3195
+ predicate filter (
3196
+ NodeEx node , FlowState state , Typ origT , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx
3197
+ ) {
3169
3198
exists ( state ) and
3199
+ exists ( origT ) and
3170
3200
// We can get away with not using type strengthening here, since we aren't
3171
3201
// going to use the tracked types in the construction of Stage 4 access
3172
3202
// paths. For Stage 4 and onwards, the tracked types must be consistent as
@@ -3199,7 +3229,7 @@ module MakeImpl<InputSig Lang> {
3199
3229
3200
3230
bindingset [ node, t0, inSummaryCtx]
3201
3231
private predicate strengthenType (
3202
- NodeEx node , DataFlowType t0 , DataFlowType t , boolean inSummaryCtx
3232
+ NodeEx node , DataFlowType origT , DataFlowType t0 , DataFlowType t , boolean inSummaryCtx
3203
3233
) {
3204
3234
exists ( inSummaryCtx ) and
3205
3235
// if node instanceof RetNodeEx and inSummaryCtx = true
@@ -3224,7 +3254,11 @@ module MakeImpl<InputSig Lang> {
3224
3254
else (
3225
3255
compatibleTypes ( nt , t0 ) and
3226
3256
// t = t0
3227
- if inSummaryCtx = true and node instanceof ParamNodeEx then t = nt else t = t0
3257
+ if inSummaryCtx = true and node instanceof ParamNodeEx
3258
+ then
3259
+ t = nt and
3260
+ compatibleTypes ( origT , t )
3261
+ else t = t0
3228
3262
)
3229
3263
)
3230
3264
else t = t0
@@ -3311,9 +3345,12 @@ module MakeImpl<InputSig Lang> {
3311
3345
)
3312
3346
}
3313
3347
3314
- bindingset [ node, state, t0, ap, inSummaryCtx]
3315
- predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx ) {
3348
+ bindingset [ node, state, origT, t0, ap, inSummaryCtx]
3349
+ predicate filter (
3350
+ NodeEx node , FlowState state , Typ origT , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx
3351
+ ) {
3316
3352
exists ( state ) and
3353
+ exists ( origT ) and
3317
3354
not clear ( node , ap ) and
3318
3355
t0 = t and
3319
3356
( if castingNodeEx ( node ) then compatibleTypes ( node .getDataFlowType ( ) , t0 ) else any ( ) ) and
@@ -3415,11 +3452,13 @@ module MakeImpl<InputSig Lang> {
3415
3452
)
3416
3453
}
3417
3454
3418
- bindingset [ node, state, t0, ap, inSummaryCtx]
3419
- predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx ) {
3455
+ bindingset [ node, state, origT, t0, ap, inSummaryCtx]
3456
+ predicate filter (
3457
+ NodeEx node , FlowState state , Typ origT , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx
3458
+ ) {
3420
3459
exists ( state ) and
3421
3460
not clear ( node , ap ) and
3422
- strengthenType ( node , t0 , t , inSummaryCtx ) and
3461
+ strengthenType ( node , origT , t0 , t , inSummaryCtx ) and
3423
3462
(
3424
3463
notExpectsContent ( node )
3425
3464
or
@@ -3680,9 +3719,11 @@ module MakeImpl<InputSig Lang> {
3680
3719
PrevStage:: nodeMayFlowNotThrough ( node , ap )
3681
3720
}
3682
3721
3683
- bindingset [ node, state, t0, ap, inSummaryCtx]
3684
- predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx ) {
3685
- strengthenType ( node , t0 , t , inSummaryCtx ) and
3722
+ bindingset [ node, state, origT, t0, ap, inSummaryCtx]
3723
+ predicate filter (
3724
+ NodeEx node , FlowState state , Typ origT , Typ t0 , Ap ap , Typ t , boolean inSummaryCtx
3725
+ ) {
3726
+ strengthenType ( node , origT , t0 , t , inSummaryCtx ) and
3686
3727
exists ( state ) and
3687
3728
exists ( ap )
3688
3729
}
@@ -4434,7 +4475,7 @@ module MakeImpl<InputSig Lang> {
4434
4475
exists ( DataFlowType t0 , Stage5:: Ap apa , boolean inSummaryCtx |
4435
4476
pathStep0 ( mid , node , state , cc , sc , t0 , ap , apa ) and
4436
4477
Stage5:: revFlow ( node , state , apa ) and
4437
- strengthenType ( node , t0 , t , inSummaryCtx ) and
4478
+ strengthenType ( node , t0 , t0 , t , inSummaryCtx ) and
4438
4479
not inBarrier ( node , state )
4439
4480
|
4440
4481
exists ( ParamNodeEx p , ParamNode param , AccessPath argAp , Stage5:: Ap argApa |
@@ -5197,7 +5238,7 @@ module MakeImpl<InputSig Lang> {
5197
5238
) and
5198
5239
exists ( boolean inSummaryCtx |
5199
5240
( if sc1 = TSummaryCtx1None ( ) then inSummaryCtx = false else inSummaryCtx = true ) and
5200
- strengthenType ( node , t0 , t , inSummaryCtx )
5241
+ strengthenType ( node , t0 , t0 , t , inSummaryCtx )
5201
5242
)
5202
5243
}
5203
5244
0 commit comments