@@ -1068,6 +1068,42 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1068
1068
if label1 = "" then result = label2 else result = label1
1069
1069
}
1070
1070
1071
+ pragma [ nomagic]
1072
+ private predicate localStepNodeCand1 (
1073
+ NodeEx node1 , NodeEx node2 , boolean preservesValue , DataFlowType t , LocalCallContext lcc ,
1074
+ string label
1075
+ ) {
1076
+ Stage1:: revFlow ( node1 ) and
1077
+ Stage1:: revFlow ( node2 ) and
1078
+ (
1079
+ preservesValue = true and
1080
+ localFlowStepEx ( node1 , node2 , label ) and
1081
+ t = node1 .getDataFlowType ( )
1082
+ or
1083
+ preservesValue = false and
1084
+ additionalLocalFlowStep ( node1 , node2 , label ) and
1085
+ t = node2 .getDataFlowType ( )
1086
+ ) and
1087
+ lcc .relevantFor ( node1 .getEnclosingCallable ( ) ) and
1088
+ not isUnreachableInCall1 ( node1 , lcc ) and
1089
+ not isUnreachableInCall1 ( node2 , lcc )
1090
+ }
1091
+
1092
+ pragma [ nomagic]
1093
+ private predicate localStateStepNodeCand1 (
1094
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , DataFlowType t ,
1095
+ LocalCallContext lcc , string label
1096
+ ) {
1097
+ Stage1:: revFlow ( node1 ) and
1098
+ Stage1:: revFlow ( node2 ) and
1099
+ additionalLocalStateStep ( node1 , state1 , node2 , state2 ) and
1100
+ label = "Config" and
1101
+ t = node2 .getDataFlowType ( ) and
1102
+ lcc .relevantFor ( node1 .getEnclosingCallable ( ) ) and
1103
+ not isUnreachableInCall1 ( node1 , lcc ) and
1104
+ not isUnreachableInCall1 ( node2 , lcc )
1105
+ }
1106
+
1071
1107
pragma [ nomagic]
1072
1108
private predicate viableReturnPosOutNodeCand1 ( DataFlowCall call , ReturnPosition pos , NodeEx out ) {
1073
1109
Stage1:: revFlow ( out ) and
@@ -1364,6 +1400,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1364
1400
1365
1401
predicate instanceofCcNoCall ( CcNoCall cc ) ;
1366
1402
1403
+ class LocalCc ;
1404
+
1367
1405
DataFlowCallable viableImplCallContextReduced ( DataFlowCall call , CcCall ctx ) ;
1368
1406
1369
1407
bindingset [ call, ctx]
@@ -1380,13 +1418,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1380
1418
CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call ) ;
1381
1419
1382
1420
bindingset [ cc]
1383
- LocalCallContext getLocalCc ( Cc cc ) ;
1421
+ LocalCc getLocalCc ( Cc cc ) ;
1384
1422
1385
1423
bindingset [ node1, state1]
1386
1424
bindingset [ node2, state2]
1387
1425
predicate localStep (
1388
1426
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
1389
- DataFlowType t , LocalCallContext lcc , string label
1427
+ Typ t , LocalCc lcc , string label
1390
1428
) ;
1391
1429
1392
1430
bindingset [ node, state, t0, ap]
@@ -1489,18 +1527,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1489
1527
fwdFlow1 ( _, _, _, _, _, _, t0 , t , ap , _) and t0 != t
1490
1528
}
1491
1529
1492
- bindingset [ node1, state1]
1493
- bindingset [ node2, state2]
1494
- additional predicate localStep (
1495
- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
1496
- Typ t , LocalCallContext lcc , string label
1497
- ) {
1498
- exists ( DataFlowType type |
1499
- Param:: localStep ( node1 , state1 , node2 , state2 , preservesValue , type , lcc , label ) and
1500
- t = getTyp ( type )
1501
- )
1502
- }
1503
-
1504
1530
pragma [ nomagic]
1505
1531
private predicate fwdFlow0 (
1506
1532
NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
@@ -1515,7 +1541,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1515
1541
ap instanceof ApNil and
1516
1542
apa = getApprox ( ap )
1517
1543
or
1518
- exists ( NodeEx mid , FlowState state0 , Typ t0 , LocalCallContext localCc |
1544
+ exists ( NodeEx mid , FlowState state0 , Typ t0 , LocalCc localCc |
1519
1545
fwdFlow ( mid , state0 , cc , summaryCtx , argT , argAp , t0 , ap , apa ) and
1520
1546
localCc = getLocalCc ( cc )
1521
1547
|
@@ -2530,8 +2556,24 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2530
2556
callEdgeReturn ( call , c , _, _, _, _, _)
2531
2557
}
2532
2558
2533
- /** Provides a big-step relation for local flow steps. */
2534
- additional module LocalFlowBigStep {
2559
+ /** Provides the input to `LocalFlowBigStep`. */
2560
+ signature module LocalFlowBigStepInputSig {
2561
+ bindingset [ node1, state1]
2562
+ bindingset [ node2, state2]
2563
+ predicate localStep (
2564
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2565
+ DataFlowType t , LocalCallContext lcc , string label
2566
+ ) ;
2567
+ }
2568
+
2569
+ /**
2570
+ * Provides a big-step relation for local flow steps.
2571
+ *
2572
+ * The big-step releation is based on the `localStep` relation from the
2573
+ * input module, restricted to nodes that are forwards and backwards
2574
+ * reachable in this stage.
2575
+ */
2576
+ additional module LocalFlowBigStep< LocalFlowBigStepInputSig Input> {
2535
2577
final private class NodeExFinal = NodeEx ;
2536
2578
2537
2579
/**
@@ -2558,7 +2600,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2558
2600
exists ( ApNil nil |
2559
2601
revFlow ( node1 , state1 , pragma [ only_bind_into ] ( nil ) ) and
2560
2602
revFlow ( node2 , state2 , pragma [ only_bind_into ] ( nil ) ) and
2561
- Param :: localStep ( node1 , state1 , node2 , state2 , false , t , lcc , label ) and
2603
+ Input :: localStep ( node1 , state1 , node2 , state2 , false , t , lcc , label ) and
2562
2604
state1 != state2
2563
2605
)
2564
2606
}
@@ -2652,7 +2694,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2652
2694
not inBarrier ( node2 , state ) and
2653
2695
not outBarrier ( node1 , state ) and
2654
2696
exists ( NodeEx node0 , boolean preservesValue0 , DataFlowType t0 , string label0 , Ap ap |
2655
- Param :: localStep ( node0 , state , node2 , state , preservesValue0 , t0 , cc , label0 ) and
2697
+ Input :: localStep ( node0 , state , node2 , state , preservesValue0 , t0 , cc , label0 ) and
2656
2698
revFlow ( node2 , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( ap ) ) and
2657
2699
not outBarrier ( node0 , state ) and
2658
2700
( preservesValue = true or ap instanceof ApNil )
@@ -3053,7 +3095,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3053
3095
PathNodeImpl pn1 , NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx ,
3054
3096
TypOption argT , ApOption argAp , Typ t , Ap ap , string label , boolean isStoreStep
3055
3097
) {
3056
- exists ( NodeEx mid , FlowState state0 , Typ t0 , LocalCallContext localCc |
3098
+ exists ( NodeEx mid , FlowState state0 , Typ t0 , LocalCc localCc |
3057
3099
pn1 = TPathNodeMid ( mid , state0 , cc , summaryCtx , argT , argAp , t0 , ap ) and
3058
3100
localCc = getLocalCc ( cc ) and
3059
3101
isStoreStep = false
@@ -3523,13 +3565,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3523
3565
3524
3566
predicate instanceofCcNoCall ( CcNoCall cc ) { any ( ) }
3525
3567
3568
+ class LocalCc = Unit ;
3569
+
3526
3570
bindingset [ cc]
3527
- LocalCallContext getLocalCc ( Cc cc ) {
3528
- cc = ccSomeCall ( ) and
3529
- result instanceof LocalCallContextSpecificCall
3530
- or
3531
- result instanceof LocalCallContextAny
3532
- }
3571
+ LocalCc getLocalCc ( Cc cc ) { any ( ) }
3533
3572
3534
3573
DataFlowCallable viableImplCallContextReduced ( DataFlowCall call , CcCall ctx ) { none ( ) }
3535
3574
@@ -3585,63 +3624,23 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3585
3624
ApOption apSome ( Ap ap ) { result = TBooleanSome ( ap ) }
3586
3625
3587
3626
import CachedCallContextSensitivity
3588
- import LocalCallContext
3589
-
3590
- pragma [ noinline]
3591
- private predicate localFlowStepNodeCand1 ( NodeEx node1 , NodeEx node2 , string model ) {
3592
- Stage1:: revFlow ( node2 ) and
3593
- localFlowStepEx ( node1 , node2 , model )
3594
- }
3595
-
3596
- pragma [ nomagic]
3597
- private predicate additionalLocalFlowStepNodeCand1 ( NodeEx node1 , NodeEx node2 , string model ) {
3598
- Stage1:: revFlow ( node2 ) and
3599
- additionalLocalFlowStep ( node1 , node2 , model )
3600
- }
3601
-
3602
- pragma [ nomagic]
3603
- private predicate localStep (
3604
- NodeEx node1 , NodeEx node2 , boolean preservesValue , DataFlowType t , LocalCallContext lcc ,
3605
- string label
3606
- ) {
3607
- (
3608
- preservesValue = true and
3609
- localFlowStepNodeCand1 ( node1 , node2 , label ) and
3610
- t = node1 .getDataFlowType ( )
3611
- or
3612
- preservesValue = false and
3613
- additionalLocalFlowStepNodeCand1 ( node1 , node2 , label ) and
3614
- t = node2 .getDataFlowType ( )
3615
- ) and
3616
- lcc .relevantFor ( node1 .getEnclosingCallable ( ) ) and
3617
- not isUnreachableInCall1 ( node1 , lcc ) and
3618
- not isUnreachableInCall1 ( node2 , lcc )
3619
- }
3620
-
3621
- pragma [ nomagic]
3622
- private predicate localStateStep (
3623
- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3624
- DataFlowType t , LocalCallContext lcc , string label
3625
- ) {
3626
- preservesValue = false and
3627
- additionalLocalStateStep ( node1 , state1 , node2 , state2 ) and
3628
- label = "Config" and
3629
- t = node2 .getDataFlowType ( ) and
3630
- lcc .relevantFor ( node1 .getEnclosingCallable ( ) ) and
3631
- not isUnreachableInCall1 ( node1 , lcc ) and
3632
- not isUnreachableInCall1 ( node2 , lcc )
3633
- }
3627
+ import NoLocalCallContext
3634
3628
3635
3629
bindingset [ node1, state1]
3636
3630
bindingset [ node2, state2]
3637
3631
predicate localStep (
3638
3632
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3639
- DataFlowType t , LocalCallContext lcc , string label
3633
+ Typ t , LocalCc lcc , string label
3640
3634
) {
3641
- localStep ( node1 , node2 , preservesValue , t , lcc , label ) and
3642
- state1 = state2
3643
- or
3644
- localStateStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label )
3635
+ (
3636
+ localStepNodeCand1 ( node1 , node2 , preservesValue , _, _, label ) and
3637
+ state1 = state2
3638
+ or
3639
+ localStateStepNodeCand1 ( node1 , state1 , node2 , state2 , _, _, label ) and
3640
+ preservesValue = false
3641
+ ) and
3642
+ exists ( t ) and
3643
+ exists ( lcc )
3645
3644
}
3646
3645
3647
3646
pragma [ nomagic]
@@ -3725,9 +3724,41 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3725
3724
}
3726
3725
3727
3726
import CallContextSensitivity< CallContextSensitivityInput >
3728
- import LocalCallContext
3727
+ import NoLocalCallContext
3728
+
3729
+ private module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
3730
+ bindingset [ node1, state1]
3731
+ bindingset [ node2, state2]
3732
+ predicate localStep (
3733
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3734
+ DataFlowType t , LocalCallContext lcc , string label
3735
+ ) {
3736
+ localStepNodeCand1 ( node1 , node2 , preservesValue , t , lcc , label ) and
3737
+ state1 = state2
3738
+ or
3739
+ localStateStepNodeCand1 ( node1 , state1 , node2 , state2 , t , lcc , label ) and
3740
+ preservesValue = false
3741
+ }
3742
+ }
3729
3743
3730
- predicate localStep = PrevStage:: LocalFlowBigStep:: localFlowBigStep / 8 ;
3744
+ additional predicate localFlowBigStep (
3745
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3746
+ DataFlowType t , LocalCallContext lcc , string label
3747
+ ) {
3748
+ PrevStage:: LocalFlowBigStep< BigStepInput > :: localFlowBigStep ( node1 , state1 , node2 , state2 ,
3749
+ preservesValue , t , lcc , label )
3750
+ }
3751
+
3752
+ bindingset [ node1, state1]
3753
+ bindingset [ node2, state2]
3754
+ predicate localStep (
3755
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3756
+ Typ t , LocalCc lcc , string label
3757
+ ) {
3758
+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , _, _, label ) and
3759
+ exists ( t ) and
3760
+ exists ( lcc )
3761
+ }
3731
3762
3732
3763
pragma [ nomagic]
3733
3764
private predicate expectsContentCand ( NodeEx node , Ap ap ) {
@@ -3809,7 +3840,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3809
3840
3810
3841
import BooleanCallContext
3811
3842
3812
- predicate localStep = PrevStage:: LocalFlowBigStep:: localFlowBigStep / 8 ;
3843
+ pragma [ nomagic]
3844
+ predicate localStep (
3845
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3846
+ Typ t , LocalCc lcc , string label
3847
+ ) {
3848
+ Stage3Param:: localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _, label ) and
3849
+ PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
3850
+ PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _) and
3851
+ exists ( lcc )
3852
+ }
3813
3853
3814
3854
pragma [ nomagic]
3815
3855
private predicate clearSet ( NodeEx node , ContentSet c ) {
@@ -4113,7 +4153,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
4113
4153
import CallContextSensitivity< CallContextSensitivityInput >
4114
4154
import LocalCallContext
4115
4155
4116
- predicate localStep = PrevStage:: LocalFlowBigStep:: localFlowBigStep / 8 ;
4156
+ predicate localStep (
4157
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
4158
+ Typ t , LocalCc lcc , string label
4159
+ ) {
4160
+ Stage3Param:: localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
4161
+ PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
4162
+ PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
4163
+ }
4117
4164
4118
4165
bindingset [ node, state, t0, ap]
4119
4166
predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
@@ -4331,7 +4378,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
4331
4378
import CallContextSensitivity< CallContextSensitivityInput >
4332
4379
import LocalCallContext
4333
4380
4334
- predicate localStep = PrevStage:: LocalFlowBigStep:: localFlowBigStep / 8 ;
4381
+ private module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
4382
+ predicate localStep (
4383
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
4384
+ DataFlowType t , LocalCallContext lcc , string label
4385
+ ) {
4386
+ Stage3Param:: localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
4387
+ PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
4388
+ PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
4389
+ }
4390
+ }
4391
+
4392
+ predicate localStep = PrevStage:: LocalFlowBigStep< BigStepInput > :: localFlowBigStep / 8 ;
4335
4393
4336
4394
bindingset [ node, state, t0, ap]
4337
4395
predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
0 commit comments