@@ -2666,9 +2666,12 @@ module Impl<FullStateConfigSig Config> {
2666
2666
2667
2667
private newtype TSummaryCtx =
2668
2668
TSummaryCtxNone ( ) or
2669
- TSummaryCtxSome ( ParamNodeEx p , FlowState state , AccessPath ap ) {
2670
- Stage5:: parameterMayFlowThrough ( p , ap .getApprox ( ) ) and
2671
- Stage5:: revFlow ( p , state , _)
2669
+ TSummaryCtxSome ( ParamNodeEx p , FlowState state , DataFlowType t , AccessPath ap ) {
2670
+ exists ( AccessPathApprox apa | ap .getApprox ( ) = apa |
2671
+ Stage5:: parameterMayFlowThrough ( p , apa ) and
2672
+ Stage5:: fwdFlow ( p , state , _, _, _, t , apa ) and
2673
+ Stage5:: revFlow ( p , state , _)
2674
+ )
2672
2675
}
2673
2676
2674
2677
/**
@@ -2690,9 +2693,10 @@ module Impl<FullStateConfigSig Config> {
2690
2693
private class SummaryCtxSome extends SummaryCtx , TSummaryCtxSome {
2691
2694
private ParamNodeEx p ;
2692
2695
private FlowState s ;
2696
+ private DataFlowType t ;
2693
2697
private AccessPath ap ;
2694
2698
2695
- SummaryCtxSome ( ) { this = TSummaryCtxSome ( p , s , ap ) }
2699
+ SummaryCtxSome ( ) { this = TSummaryCtxSome ( p , s , t , ap ) }
2696
2700
2697
2701
ParameterPosition getParameterPos ( ) { p .isParameterOf ( _, result ) }
2698
2702
@@ -2823,16 +2827,17 @@ module Impl<FullStateConfigSig Config> {
2823
2827
2824
2828
private newtype TPathNode =
2825
2829
pragma [ assume_small_delta]
2826
- TPathNodeMid ( NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , AccessPath ap ) {
2830
+ TPathNodeMid ( NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , DataFlowType t , AccessPath ap ) {
2827
2831
// A PathNode is introduced by a source ...
2828
2832
Stage5:: revFlow ( node , state ) and
2829
2833
sourceNode ( node , state ) and
2830
2834
sourceCallCtx ( cc ) and
2831
2835
sc instanceof SummaryCtxNone and
2832
- ap = TAccessPathNil ( node .getDataFlowType ( ) )
2836
+ t = node .getDataFlowType ( ) and
2837
+ ap = TAccessPathNil ( t )
2833
2838
or
2834
2839
// ... or a step from an existing PathNode to another node.
2835
- pathStep ( _, node , state , cc , sc , ap ) and
2840
+ pathStep ( _, node , state , cc , sc , t , ap ) and
2836
2841
Stage5:: revFlow ( node , state , ap .getApprox ( ) )
2837
2842
} or
2838
2843
TPathNodeSink ( NodeEx node , FlowState state ) {
@@ -3215,9 +3220,10 @@ module Impl<FullStateConfigSig Config> {
3215
3220
FlowState state ;
3216
3221
CallContext cc ;
3217
3222
SummaryCtx sc ;
3223
+ DataFlowType t ;
3218
3224
AccessPath ap ;
3219
3225
3220
- PathNodeMid ( ) { this = TPathNodeMid ( node , state , cc , sc , ap ) }
3226
+ PathNodeMid ( ) { this = TPathNodeMid ( node , state , cc , sc , t , ap ) }
3221
3227
3222
3228
override NodeEx getNodeEx ( ) { result = node }
3223
3229
@@ -3227,11 +3233,13 @@ module Impl<FullStateConfigSig Config> {
3227
3233
3228
3234
SummaryCtx getSummaryCtx ( ) { result = sc }
3229
3235
3236
+ DataFlowType getType ( ) { result = t }
3237
+
3230
3238
AccessPath getAp ( ) { result = ap }
3231
3239
3232
3240
private PathNodeMid getSuccMid ( ) {
3233
3241
pathStep ( this , result .getNodeEx ( ) , result .getState ( ) , result .getCallContext ( ) ,
3234
- result .getSummaryCtx ( ) , result .getAp ( ) )
3242
+ result .getSummaryCtx ( ) , result .getType ( ) , result . getAp ( ) )
3235
3243
}
3236
3244
3237
3245
override PathNodeImpl getASuccessorImpl ( ) {
@@ -3246,7 +3254,8 @@ module Impl<FullStateConfigSig Config> {
3246
3254
sourceNode ( node , state ) and
3247
3255
sourceCallCtx ( cc ) and
3248
3256
sc instanceof SummaryCtxNone and
3249
- ap = TAccessPathNil ( node .getDataFlowType ( ) )
3257
+ t = node .getDataFlowType ( ) and
3258
+ ap = TAccessPathNil ( t )
3250
3259
}
3251
3260
3252
3261
predicate isAtSink ( ) {
@@ -3343,7 +3352,7 @@ module Impl<FullStateConfigSig Config> {
3343
3352
}
3344
3353
3345
3354
private predicate pathNode (
3346
- PathNodeMid mid , NodeEx midnode , FlowState state , CallContext cc , SummaryCtx sc , AccessPath ap ,
3355
+ PathNodeMid mid , NodeEx midnode , FlowState state , CallContext cc , SummaryCtx sc , DataFlowType t , AccessPath ap ,
3347
3356
LocalCallContext localCC
3348
3357
) {
3349
3358
midnode = mid .getNodeEx ( ) and
@@ -3353,6 +3362,7 @@ module Impl<FullStateConfigSig Config> {
3353
3362
localCC =
3354
3363
getLocalCallContext ( pragma [ only_bind_into ] ( pragma [ only_bind_out ] ( cc ) ) ,
3355
3364
midnode .getEnclosingCallable ( ) ) and
3365
+ t = mid .getType ( ) and
3356
3366
ap = mid .getAp ( )
3357
3367
}
3358
3368
@@ -3363,49 +3373,56 @@ module Impl<FullStateConfigSig Config> {
3363
3373
pragma [ assume_small_delta]
3364
3374
pragma [ nomagic]
3365
3375
private predicate pathStep (
3366
- PathNodeMid mid , NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , AccessPath ap
3376
+ PathNodeMid mid , NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , DataFlowType t , AccessPath ap
3367
3377
) {
3368
3378
exists ( NodeEx midnode , FlowState state0 , LocalCallContext localCC |
3369
- pathNode ( mid , midnode , state0 , cc , sc , ap , localCC ) and
3379
+ pathNode ( mid , midnode , state0 , cc , sc , t , ap , localCC ) and
3370
3380
localFlowBigStep ( midnode , state0 , node , state , true , _, localCC )
3371
3381
)
3372
3382
or
3373
3383
exists ( AccessPath ap0 , NodeEx midnode , FlowState state0 , LocalCallContext localCC |
3374
- pathNode ( mid , midnode , state0 , cc , sc , ap0 , localCC ) and
3375
- localFlowBigStep ( midnode , state0 , node , state , false , ap .( AccessPathNil ) .getType ( ) , localCC ) and
3384
+ pathNode ( mid , midnode , state0 , cc , sc , _, ap0 , localCC ) and
3385
+ localFlowBigStep ( midnode , state0 , node , state , false , t , localCC ) and
3386
+ ap .( AccessPathNil ) .getType ( ) = t and
3376
3387
ap0 instanceof AccessPathNil
3377
3388
)
3378
3389
or
3379
3390
jumpStepEx ( mid .getNodeEx ( ) , node ) and
3380
3391
state = mid .getState ( ) and
3381
3392
cc instanceof CallContextAny and
3382
3393
sc instanceof SummaryCtxNone and
3394
+ t = mid .getType ( ) and
3383
3395
ap = mid .getAp ( )
3384
3396
or
3385
3397
additionalJumpStep ( mid .getNodeEx ( ) , node ) and
3386
3398
state = mid .getState ( ) and
3387
3399
cc instanceof CallContextAny and
3388
3400
sc instanceof SummaryCtxNone and
3389
3401
mid .getAp ( ) instanceof AccessPathNil and
3390
- ap = TAccessPathNil ( node .getDataFlowType ( ) )
3402
+ t = node .getDataFlowType ( ) and
3403
+ ap = TAccessPathNil ( t )
3391
3404
or
3392
3405
additionalJumpStateStep ( mid .getNodeEx ( ) , mid .getState ( ) , node , state ) and
3393
3406
cc instanceof CallContextAny and
3394
3407
sc instanceof SummaryCtxNone and
3395
3408
mid .getAp ( ) instanceof AccessPathNil and
3396
- ap = TAccessPathNil ( node .getDataFlowType ( ) )
3409
+ t = node .getDataFlowType ( ) and
3410
+ ap = TAccessPathNil ( t )
3397
3411
or
3398
- exists ( TypedContent tc | pathStoreStep ( mid , node , state , ap .pop ( tc ) , tc , cc ) ) and
3412
+ exists ( TypedContent tc | pathStoreStep ( mid , node , state , ap .pop ( tc ) , tc , t , cc ) ) and
3399
3413
sc = mid .getSummaryCtx ( )
3400
3414
or
3401
3415
exists ( TypedContent tc | pathReadStep ( mid , node , state , ap .push ( tc ) , tc , cc ) ) and
3416
+ // TODO: replace push/pop with isCons
3417
+ // ap0.isCons(tc, t, ap)
3418
+ exists ( t ) and
3402
3419
sc = mid .getSummaryCtx ( )
3403
3420
or
3404
- pathIntoCallable ( mid , node , state , _, cc , sc , _) and ap = mid .getAp ( )
3421
+ pathIntoCallable ( mid , node , state , _, cc , sc , _) and t = mid . getType ( ) and ap = mid .getAp ( )
3405
3422
or
3406
- pathOutOfCallable ( mid , node , state , cc ) and ap = mid .getAp ( ) and sc instanceof SummaryCtxNone
3423
+ pathOutOfCallable ( mid , node , state , cc ) and t = mid . getType ( ) and ap = mid .getAp ( ) and sc instanceof SummaryCtxNone
3407
3424
or
3408
- pathThroughCallable ( mid , node , state , cc , ap ) and sc = mid .getSummaryCtx ( )
3425
+ pathThroughCallable ( mid , node , state , cc , t , ap ) and sc = mid .getSummaryCtx ( )
3409
3426
}
3410
3427
3411
3428
pragma [ nomagic]
@@ -3421,10 +3438,10 @@ module Impl<FullStateConfigSig Config> {
3421
3438
3422
3439
pragma [ nomagic]
3423
3440
private predicate pathStoreStep (
3424
- PathNodeMid mid , NodeEx node , FlowState state , AccessPath ap0 , TypedContent tc , CallContext cc
3441
+ PathNodeMid mid , NodeEx node , FlowState state , AccessPath ap0 , TypedContent tc , DataFlowType t , CallContext cc
3425
3442
) {
3426
3443
ap0 = mid .getAp ( ) and
3427
- Stage5:: storeStepCand ( mid .getNodeEx ( ) , _, tc , _, node , _, _ ) and
3444
+ Stage5:: storeStepCand ( mid .getNodeEx ( ) , _, tc , _, node , _, t ) and
3428
3445
state = mid .getState ( ) and
3429
3446
cc = mid .getCallContext ( )
3430
3447
}
@@ -3478,10 +3495,10 @@ module Impl<FullStateConfigSig Config> {
3478
3495
pragma [ noinline]
3479
3496
private predicate pathIntoArg (
3480
3497
PathNodeMid mid , ParameterPosition ppos , FlowState state , CallContext cc , DataFlowCall call ,
3481
- AccessPath ap , AccessPathApprox apa
3498
+ DataFlowType t , AccessPath ap , AccessPathApprox apa
3482
3499
) {
3483
3500
exists ( ArgNodeEx arg , ArgumentPosition apos |
3484
- pathNode ( mid , arg , state , cc , _, ap , _) and
3501
+ pathNode ( mid , arg , state , cc , _, t , ap , _) and
3485
3502
arg .asNode ( ) .( ArgNode ) .argumentOf ( call , apos ) and
3486
3503
apa = ap .getApprox ( ) and
3487
3504
parameterMatch ( ppos , apos )
@@ -3501,10 +3518,10 @@ module Impl<FullStateConfigSig Config> {
3501
3518
pragma [ nomagic]
3502
3519
private predicate pathIntoCallable0 (
3503
3520
PathNodeMid mid , DataFlowCallable callable , ParameterPosition pos , FlowState state ,
3504
- CallContext outercc , DataFlowCall call , AccessPath ap
3521
+ CallContext outercc , DataFlowCall call , DataFlowType t , AccessPath ap
3505
3522
) {
3506
3523
exists ( AccessPathApprox apa |
3507
- pathIntoArg ( mid , pragma [ only_bind_into ] ( pos ) , state , outercc , call , ap ,
3524
+ pathIntoArg ( mid , pragma [ only_bind_into ] ( pos ) , state , outercc , call , t , ap ,
3508
3525
pragma [ only_bind_into ] ( apa ) ) and
3509
3526
callable = resolveCall ( call , outercc ) and
3510
3527
parameterCand ( callable , pragma [ only_bind_into ] ( pos ) , pragma [ only_bind_into ] ( apa ) )
@@ -3521,13 +3538,13 @@ module Impl<FullStateConfigSig Config> {
3521
3538
PathNodeMid mid , ParamNodeEx p , FlowState state , CallContext outercc , CallContextCall innercc ,
3522
3539
SummaryCtx sc , DataFlowCall call
3523
3540
) {
3524
- exists ( ParameterPosition pos , DataFlowCallable callable , AccessPath ap |
3525
- pathIntoCallable0 ( mid , callable , pos , state , outercc , call , ap ) and
3541
+ exists ( ParameterPosition pos , DataFlowCallable callable , DataFlowType t , AccessPath ap |
3542
+ pathIntoCallable0 ( mid , callable , pos , state , outercc , call , t , ap ) and
3526
3543
p .isParameterOf ( callable , pos ) and
3527
3544
(
3528
- sc = TSummaryCtxSome ( p , state , ap )
3545
+ sc = TSummaryCtxSome ( p , state , t , ap )
3529
3546
or
3530
- not exists ( TSummaryCtxSome ( p , state , ap ) ) and
3547
+ not exists ( TSummaryCtxSome ( p , state , t , ap ) ) and
3531
3548
sc = TSummaryCtxNone ( ) and
3532
3549
// When the call contexts of source and sink needs to match then there's
3533
3550
// never any reason to enter a callable except to find a summary. See also
@@ -3544,11 +3561,11 @@ module Impl<FullStateConfigSig Config> {
3544
3561
/** Holds if data may flow from a parameter given by `sc` to a return of kind `kind`. */
3545
3562
pragma [ nomagic]
3546
3563
private predicate paramFlowsThrough (
3547
- ReturnKindExt kind , FlowState state , CallContextCall cc , SummaryCtxSome sc , AccessPath ap ,
3564
+ ReturnKindExt kind , FlowState state , CallContextCall cc , SummaryCtxSome sc , DataFlowType t , AccessPath ap ,
3548
3565
AccessPathApprox apa
3549
3566
) {
3550
3567
exists ( RetNodeEx ret |
3551
- pathNode ( _, ret , state , cc , sc , ap , _) and
3568
+ pathNode ( _, ret , state , cc , sc , t , ap , _) and
3552
3569
kind = ret .getKind ( ) and
3553
3570
apa = ap .getApprox ( ) and
3554
3571
parameterFlowThroughAllowed ( sc .getParamNode ( ) , kind )
@@ -3559,11 +3576,11 @@ module Impl<FullStateConfigSig Config> {
3559
3576
pragma [ nomagic]
3560
3577
private predicate pathThroughCallable0 (
3561
3578
DataFlowCall call , PathNodeMid mid , ReturnKindExt kind , FlowState state , CallContext cc ,
3562
- AccessPath ap , AccessPathApprox apa
3579
+ DataFlowType t , AccessPath ap , AccessPathApprox apa
3563
3580
) {
3564
3581
exists ( CallContext innercc , SummaryCtx sc |
3565
3582
pathIntoCallable ( mid , _, _, cc , innercc , sc , call ) and
3566
- paramFlowsThrough ( kind , state , innercc , sc , ap , apa )
3583
+ paramFlowsThrough ( kind , state , innercc , sc , t , ap , apa )
3567
3584
)
3568
3585
}
3569
3586
@@ -3573,10 +3590,10 @@ module Impl<FullStateConfigSig Config> {
3573
3590
*/
3574
3591
pragma [ noinline]
3575
3592
private predicate pathThroughCallable (
3576
- PathNodeMid mid , NodeEx out , FlowState state , CallContext cc , AccessPath ap
3593
+ PathNodeMid mid , NodeEx out , FlowState state , CallContext cc , DataFlowType t , AccessPath ap
3577
3594
) {
3578
3595
exists ( DataFlowCall call , ReturnKindExt kind , AccessPathApprox apa |
3579
- pathThroughCallable0 ( call , mid , kind , state , cc , ap , apa ) and
3596
+ pathThroughCallable0 ( call , mid , kind , state , cc , t , ap , apa ) and
3580
3597
out = getAnOutNodeFlow ( kind , call , apa )
3581
3598
)
3582
3599
}
@@ -3589,12 +3606,12 @@ module Impl<FullStateConfigSig Config> {
3589
3606
pragma [ nomagic]
3590
3607
private predicate subpaths01 (
3591
3608
PathNodeImpl arg , ParamNodeEx par , SummaryCtxSome sc , CallContext innercc , ReturnKindExt kind ,
3592
- NodeEx out , FlowState sout , AccessPath apout
3609
+ NodeEx out , FlowState sout , DataFlowType t , AccessPath apout
3593
3610
) {
3594
- pathThroughCallable ( arg , out , pragma [ only_bind_into ] ( sout ) , _, pragma [ only_bind_into ] ( apout ) ) and
3611
+ pathThroughCallable ( arg , out , pragma [ only_bind_into ] ( sout ) , _, pragma [ only_bind_into ] ( t ) , pragma [ only_bind_into ] ( apout ) ) and
3595
3612
pathIntoCallable ( arg , par , _, _, innercc , sc , _) and
3596
3613
paramFlowsThrough ( kind , pragma [ only_bind_into ] ( sout ) , innercc , sc ,
3597
- pragma [ only_bind_into ] ( apout ) , _) and
3614
+ pragma [ only_bind_into ] ( t ) , pragma [ only_bind_into ] ( apout ) , _) and
3598
3615
not arg .isHidden ( )
3599
3616
}
3600
3617
@@ -3605,9 +3622,9 @@ module Impl<FullStateConfigSig Config> {
3605
3622
pragma [ nomagic]
3606
3623
private predicate subpaths02 (
3607
3624
PathNodeImpl arg , ParamNodeEx par , SummaryCtxSome sc , CallContext innercc , ReturnKindExt kind ,
3608
- NodeEx out , FlowState sout , AccessPath apout
3625
+ NodeEx out , FlowState sout , DataFlowType t , AccessPath apout
3609
3626
) {
3610
- subpaths01 ( arg , par , sc , innercc , kind , out , sout , apout ) and
3627
+ subpaths01 ( arg , par , sc , innercc , kind , out , sout , t , apout ) and
3611
3628
out .asNode ( ) = kind .getAnOutNode ( _)
3612
3629
}
3613
3630
@@ -3617,11 +3634,11 @@ module Impl<FullStateConfigSig Config> {
3617
3634
pragma [ nomagic]
3618
3635
private predicate subpaths03 (
3619
3636
PathNodeImpl arg , ParamNodeEx par , PathNodeMid ret , NodeEx out , FlowState sout ,
3620
- AccessPath apout
3637
+ DataFlowType t , AccessPath apout
3621
3638
) {
3622
3639
exists ( SummaryCtxSome sc , CallContext innercc , ReturnKindExt kind , RetNodeEx retnode |
3623
- subpaths02 ( arg , par , sc , innercc , kind , out , sout , apout ) and
3624
- pathNode ( ret , retnode , sout , innercc , sc , apout , _) and
3640
+ subpaths02 ( arg , par , sc , innercc , kind , out , sout , t , apout ) and
3641
+ pathNode ( ret , retnode , sout , innercc , sc , t , apout , _) and
3625
3642
kind = retnode .getKind ( )
3626
3643
)
3627
3644
}
@@ -3648,12 +3665,12 @@ module Impl<FullStateConfigSig Config> {
3648
3665
* `ret -> out` is summarized as the edge `arg -> out`.
3649
3666
*/
3650
3667
predicate subpaths ( PathNodeImpl arg , PathNodeImpl par , PathNodeImpl ret , PathNodeImpl out ) {
3651
- exists ( ParamNodeEx p , NodeEx o , FlowState sout , AccessPath apout , PathNodeMid out0 |
3668
+ exists ( ParamNodeEx p , NodeEx o , FlowState sout , DataFlowType t , AccessPath apout , PathNodeMid out0 |
3652
3669
pragma [ only_bind_into ] ( arg ) .getANonHiddenSuccessor ( ) = pragma [ only_bind_into ] ( out0 ) and
3653
- subpaths03 ( pragma [ only_bind_into ] ( arg ) , p , localStepToHidden * ( ret ) , o , sout , apout ) and
3670
+ subpaths03 ( pragma [ only_bind_into ] ( arg ) , p , localStepToHidden * ( ret ) , o , sout , t , apout ) and
3654
3671
hasSuccessor ( pragma [ only_bind_into ] ( arg ) , par , p ) and
3655
3672
not ret .isHidden ( ) and
3656
- pathNode ( out0 , o , sout , _, _, apout , _)
3673
+ pathNode ( out0 , o , sout , _, _, t , apout , _)
3657
3674
|
3658
3675
out = out0 or out = out0 .projectToSink ( )
3659
3676
)
0 commit comments