@@ -1342,6 +1342,11 @@ module MakeImpl<InputSig Lang> {
1342
1342
fwdFlow1 ( node , state , cc , summaryCtx , argT , argAp , _, t , _, origT , ap , apa )
1343
1343
}
1344
1344
1345
+ pragma [ nomagic]
1346
+ private ApOption blah ( ApApprox apa ) {
1347
+ result = apSome ( any ( Ap argAp1 | apa = getApprox ( argAp1 ) ) )
1348
+ }
1349
+
1345
1350
pragma [ nomagic]
1346
1351
additional predicate fwdFlow1 (
1347
1352
NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , ArgTypOption argT ,
@@ -1353,7 +1358,7 @@ module MakeImpl<InputSig Lang> {
1353
1358
(
1354
1359
exists ( ParamNode p , ApApprox argApa |
1355
1360
summaryCtx = TParamNodeSome ( p ) and
1356
- argAp = apSome ( any ( Ap argAp1 | argApa = getApprox ( argAp1 ) ) ) and
1361
+ argAp = blah ( argApa ) and // apSome(any(Ap argAp1 | argApa = getApprox(argAp1))) and
1357
1362
Param:: nodeMayFlowThrough ( p , argApa , node , apa ) and
1358
1363
inSummaryCtx = true
1359
1364
)
@@ -3187,26 +3192,30 @@ module MakeImpl<InputSig Lang> {
3187
3192
3188
3193
private module Stage3 = MkStage< Stage2_5 > :: Stage< Stage3Param > ;
3189
3194
3190
- // private predicate mostBusyNodeFwd3 = Stage3::mostBusyNodeFwd/9;
3191
- // private predicate mostBusyNodeFwd3_5 = Stage3_5::mostBusyNodeFwd/9;
3192
- // private predicate mostBusyNodeFwd4 = Stage4::mostBusyNodeFwd/9;
3193
- // private predicate mostBusyNodeFwd5 = Stage5::mostBusyNodeFwd/9;
3195
+ // private predicate mostBusyNodeFwd3 = Stage3::mostBusyNodeFwd/10;
3196
+ // private predicate mostBusyNodeFwd3_5 = Stage3_5::mostBusyNodeFwd/10;
3197
+ // private predicate mostBusyNodeFwd4 = Stage4::mostBusyNodeFwd/10;
3198
+ private predicate mostBusyNodeFwd5 = Stage5:: mostBusyNodeFwd / 10 ;
3199
+
3194
3200
bindingset [ node, t0, inSummaryCtx]
3195
3201
private predicate strengthenType (
3196
3202
NodeEx node , DataFlowType t0 , DataFlowType t , boolean inSummaryCtx
3197
3203
) {
3198
3204
exists ( inSummaryCtx ) and
3199
- if castingNodeEx ( node )
3200
- then
3201
- exists ( DataFlowType nt | nt = node .getDataFlowType ( ) |
3202
- if inSummaryCtx = false and typeStrongerThan ( nt , t0 )
3203
- then t = nt
3204
- else (
3205
- compatibleTypes ( nt , t0 ) and
3206
- if inSummaryCtx = true and node instanceof ParamNodeEx then t = nt else t = t0
3205
+ if node instanceof RetNodeEx and inSummaryCtx = true
3206
+ then t = node .getDataFlowType ( ) and compatibleTypes ( t , t0 )
3207
+ else
3208
+ if castingNodeEx ( node )
3209
+ then
3210
+ exists ( DataFlowType nt | nt = node .getDataFlowType ( ) |
3211
+ if inSummaryCtx = false and typeStrongerThan ( nt , t0 )
3212
+ then t = nt
3213
+ else (
3214
+ compatibleTypes ( nt , t0 ) and
3215
+ if inSummaryCtx = true and node instanceof ParamNodeEx then t = nt else t = t0
3216
+ )
3207
3217
)
3208
- )
3209
- else t = t0
3218
+ else t = t0
3210
3219
}
3211
3220
3212
3221
private module Stage3_5Param implements MkStage< Stage3 > :: StageParam {
@@ -3630,11 +3639,12 @@ module MakeImpl<InputSig Lang> {
3630
3639
3631
3640
ApHeadContent projectToHeadContent ( Content c ) { result = c }
3632
3641
3633
- class ApOption = AccessPathApproxOption ;
3642
+ class ApOption = AccessPathFrontOption ;
3634
3643
3635
- ApOption apNone ( ) { result = TAccessPathApproxNone ( ) }
3644
+ // class ApOption = AccessPathApproxOption;
3645
+ ApOption apNone ( ) { result = TAccessPathFrontNone ( ) }
3636
3646
3637
- ApOption apSome ( Ap ap ) { result = TAccessPathApproxSome ( ap ) }
3647
+ ApOption apSome ( Ap ap ) { result = TAccessPathFrontSome ( ap . getFront ( ) ) }
3638
3648
3639
3649
import Level1CallContext
3640
3650
import LocalCallContext
@@ -3669,6 +3679,8 @@ module MakeImpl<InputSig Lang> {
3669
3679
predicate typecheckStore ( Typ typ , DataFlowType contentType ) {
3670
3680
compatibleTypes ( typ , contentType )
3671
3681
}
3682
+
3683
+ predicate enableTypeFlow ( ) { none ( ) }
3672
3684
}
3673
3685
3674
3686
private module Stage5 = MkStage< Stage4 > :: Stage< Stage5Param > ;
@@ -3681,7 +3693,7 @@ module MakeImpl<InputSig Lang> {
3681
3693
Stage5:: parameterMayFlowThrough ( p , _) and
3682
3694
Stage5:: revFlow ( n , state , TReturnCtxMaybeFlowThrough ( _) , _, apa0 ) and
3683
3695
Stage5:: fwdFlow ( n , state , any ( CallContextCall ccc ) , TParamNodeSome ( p .asNode ( ) ) , _,
3684
- TAccessPathApproxSome ( apa ) , _, _, apa0 , _)
3696
+ TAccessPathFrontSome ( apa . getFront ( ) ) , _, _, apa0 , _)
3685
3697
)
3686
3698
}
3687
3699
@@ -4407,28 +4419,22 @@ module MakeImpl<InputSig Lang> {
4407
4419
PathNodeMid mid , NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , DataFlowType t ,
4408
4420
AccessPath ap
4409
4421
) {
4410
- exists ( DataFlowType t0 , SummaryCtx sc0 , Stage5:: Ap apa , boolean inSummaryCtx |
4411
- pathStep0 ( mid , node , state , cc , sc0 , t0 , ap , apa ) and
4422
+ exists ( DataFlowType t0 , Stage5:: Ap apa , boolean inSummaryCtx |
4423
+ pathStep0 ( mid , node , state , cc , sc , t0 , ap , apa ) and
4412
4424
Stage5:: revFlow ( node , state , apa ) and
4413
4425
strengthenType ( node , t0 , t , inSummaryCtx ) and
4414
4426
not inBarrier ( node , state )
4415
4427
|
4416
4428
exists ( ParamNodeEx p , ParamNode param , AccessPath argAp , Stage5:: Ap argApa |
4417
- sc0 = TSummaryCtxSome ( p , _, _, argAp ) and
4429
+ sc = TSummaryCtxSome ( p , _, _, argAp ) and
4418
4430
param = p .asNode ( ) and
4419
4431
argApa = argAp .getApprox ( ) and
4420
- if Stage5:: nodeMayFlowThrough ( param , argApa , node , apa )
4421
- then
4422
- sc = sc0 and
4423
- inSummaryCtx = true
4424
- else (
4425
- sc = TSummaryCtxNone ( ) and
4426
- inSummaryCtx = false
4427
- )
4432
+ Stage5:: nodeMayFlowThrough ( param , argApa , node , apa ) and
4433
+ inSummaryCtx = true
4428
4434
)
4429
4435
or
4430
- sc0 = TSummaryCtxNone ( ) and
4431
- sc = sc0 and
4436
+ sc = TSummaryCtxNone ( ) and
4437
+ ( cc instanceof CallContextNoCall or Stage5 :: nodeMayFlowNotThrough ( node , apa ) ) and
4432
4438
inSummaryCtx = false
4433
4439
)
4434
4440
}
@@ -4581,14 +4587,15 @@ module MakeImpl<InputSig Lang> {
4581
4587
pragma [ noinline]
4582
4588
private predicate pathIntoArg (
4583
4589
PathNodeMid mid , ParameterPosition ppos , FlowState state , CallContext cc , DataFlowCall call ,
4584
- DataFlowType t , AccessPath ap , AccessPathApprox apa
4590
+ DataFlowType t , AccessPath ap , AccessPathApprox apa , boolean inSummaryCtx
4585
4591
) {
4586
- exists ( ArgNodeEx arg , ArgumentPosition apos |
4587
- pathNode ( mid , arg , state , cc , _ , t , ap , _) and
4592
+ exists ( ArgNodeEx arg , SummaryCtx sc , ArgumentPosition apos |
4593
+ pathNode ( mid , arg , state , cc , sc , t , ap , _) and
4588
4594
not outBarrier ( arg , state ) and
4589
4595
arg .asNode ( ) .( ArgNode ) .argumentOf ( call , apos ) and
4590
4596
apa = ap .getApprox ( ) and
4591
- parameterMatch ( ppos , apos )
4597
+ parameterMatch ( ppos , apos ) and
4598
+ if sc = TSummaryCtxNone ( ) then inSummaryCtx = false else inSummaryCtx = true
4592
4599
)
4593
4600
}
4594
4601
@@ -4607,11 +4614,11 @@ module MakeImpl<InputSig Lang> {
4607
4614
pragma [ nomagic]
4608
4615
private predicate pathIntoCallable0 (
4609
4616
PathNodeMid mid , DataFlowCallable callable , ParameterPosition pos , FlowState state ,
4610
- CallContext outercc , DataFlowCall call , DataFlowType t , AccessPath ap
4617
+ CallContext outercc , DataFlowCall call , DataFlowType t , AccessPath ap , boolean inSummaryCtx
4611
4618
) {
4612
4619
exists ( AccessPathApprox apa |
4613
4620
pathIntoArg ( mid , pragma [ only_bind_into ] ( pos ) , state , outercc , call , t , ap ,
4614
- pragma [ only_bind_into ] ( apa ) ) and
4621
+ pragma [ only_bind_into ] ( apa ) , inSummaryCtx ) and
4615
4622
callable = ResolveCall< parameterCandProj / 1 > :: resolveCall ( call , outercc ) and
4616
4623
parameterCand ( callable , pragma [ only_bind_into ] ( pos ) , pragma [ only_bind_into ] ( apa ) )
4617
4624
)
@@ -4627,13 +4634,17 @@ module MakeImpl<InputSig Lang> {
4627
4634
PathNodeMid mid , ParamNodeEx p , FlowState state , CallContext outercc , CallContextCall innercc ,
4628
4635
SummaryCtx sc , DataFlowCall call
4629
4636
) {
4630
- exists ( ParameterPosition pos , DataFlowCallable callable , DataFlowType t , AccessPath ap |
4631
- pathIntoCallable0 ( mid , callable , pos , state , outercc , call , t , ap ) and
4637
+ exists (
4638
+ ParameterPosition pos , DataFlowCallable callable , DataFlowType t , AccessPath ap ,
4639
+ boolean inSummaryCtx
4640
+ |
4641
+ pathIntoCallable0 ( mid , callable , pos , state , outercc , call , t , ap , inSummaryCtx ) and
4632
4642
p .isParameterOf ( callable , pos ) and
4633
4643
not inBarrier ( p , state ) and
4634
4644
(
4635
4645
sc = TSummaryCtxSome ( p , state , t , ap )
4636
4646
or
4647
+ inSummaryCtx = false and
4637
4648
// not exists(TSummaryCtxSome(p, state, t, ap)) and
4638
4649
Stage5:: nodeMayFlowNotThrough ( p , ap .getApprox ( ) ) and
4639
4650
sc = TSummaryCtxNone ( ) and
0 commit comments