@@ -1068,6 +1068,42 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
10681068 if label1 = "" then result = label2 else result = label1
10691069 }
10701070
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+
10711107 pragma [ nomagic]
10721108 private predicate viableReturnPosOutNodeCand1 ( DataFlowCall call , ReturnPosition pos , NodeEx out ) {
10731109 Stage1:: revFlow ( out ) and
@@ -1364,6 +1400,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
13641400
13651401 predicate instanceofCcNoCall ( CcNoCall cc ) ;
13661402
1403+ class LocalCc ;
1404+
13671405 DataFlowCallable viableImplCallContextReduced ( DataFlowCall call , CcCall ctx ) ;
13681406
13691407 bindingset [ call, ctx]
@@ -1380,13 +1418,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
13801418 CcNoCall getCallContextReturn ( DataFlowCallable c , DataFlowCall call ) ;
13811419
13821420 bindingset [ cc]
1383- LocalCallContext getLocalCc ( Cc cc ) ;
1421+ LocalCc getLocalCc ( Cc cc ) ;
13841422
13851423 bindingset [ node1, state1]
13861424 bindingset [ node2, state2]
13871425 predicate localStep (
13881426 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
1389- DataFlowType t , LocalCallContext lcc , string label
1427+ Typ t , LocalCc lcc , string label
13901428 ) ;
13911429
13921430 bindingset [ node, state, t0, ap]
@@ -1489,18 +1527,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
14891527 fwdFlow1 ( _, _, _, _, _, _, t0 , t , ap , _) and t0 != t
14901528 }
14911529
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-
15041530 pragma [ nomagic]
15051531 private predicate fwdFlow0 (
15061532 NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
@@ -1515,7 +1541,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
15151541 ap instanceof ApNil and
15161542 apa = getApprox ( ap )
15171543 or
1518- exists ( NodeEx mid , FlowState state0 , Typ t0 , LocalCallContext localCc |
1544+ exists ( NodeEx mid , FlowState state0 , Typ t0 , LocalCc localCc |
15191545 fwdFlow ( mid , state0 , cc , summaryCtx , argT , argAp , t0 , ap , apa ) and
15201546 localCc = getLocalCc ( cc )
15211547 |
@@ -2530,8 +2556,24 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
25302556 callEdgeReturn ( call , c , _, _, _, _, _)
25312557 }
25322558
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> {
25352577 final private class NodeExFinal = NodeEx ;
25362578
25372579 /**
@@ -2558,7 +2600,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
25582600 exists ( ApNil nil |
25592601 revFlow ( node1 , state1 , pragma [ only_bind_into ] ( nil ) ) and
25602602 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
25622604 state1 != state2
25632605 )
25642606 }
@@ -2652,7 +2694,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26522694 not inBarrier ( node2 , state ) and
26532695 not outBarrier ( node1 , state ) and
26542696 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
26562698 revFlow ( node2 , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( ap ) ) and
26572699 not outBarrier ( node0 , state ) and
26582700 ( preservesValue = true or ap instanceof ApNil )
@@ -3053,7 +3095,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
30533095 PathNodeImpl pn1 , NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx ,
30543096 TypOption argT , ApOption argAp , Typ t , Ap ap , string label , boolean isStoreStep
30553097 ) {
3056- exists ( NodeEx mid , FlowState state0 , Typ t0 , LocalCallContext localCc |
3098+ exists ( NodeEx mid , FlowState state0 , Typ t0 , LocalCc localCc |
30573099 pn1 = TPathNodeMid ( mid , state0 , cc , summaryCtx , argT , argAp , t0 , ap ) and
30583100 localCc = getLocalCc ( cc ) and
30593101 isStoreStep = false
@@ -3523,13 +3565,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35233565
35243566 predicate instanceofCcNoCall ( CcNoCall cc ) { any ( ) }
35253567
3568+ class LocalCc = Unit ;
3569+
35263570 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 ( ) }
35333572
35343573 DataFlowCallable viableImplCallContextReduced ( DataFlowCall call , CcCall ctx ) { none ( ) }
35353574
@@ -3585,63 +3624,23 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35853624 ApOption apSome ( Ap ap ) { result = TBooleanSome ( ap ) }
35863625
35873626 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
36343628
36353629 bindingset [ node1, state1]
36363630 bindingset [ node2, state2]
36373631 predicate localStep (
36383632 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3639- DataFlowType t , LocalCallContext lcc , string label
3633+ Typ t , LocalCc lcc , string label
36403634 ) {
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 )
36453644 }
36463645
36473646 pragma [ nomagic]
@@ -3725,9 +3724,41 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
37253724 }
37263725
37273726 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+ }
37293743
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+ }
37313762
37323763 pragma [ nomagic]
37333764 private predicate expectsContentCand ( NodeEx node , Ap ap ) {
@@ -3809,7 +3840,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
38093840
38103841 import BooleanCallContext
38113842
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+ }
38133853
38143854 pragma [ nomagic]
38153855 private predicate clearSet ( NodeEx node , ContentSet c ) {
@@ -4113,7 +4153,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
41134153 import CallContextSensitivity< CallContextSensitivityInput >
41144154 import LocalCallContext
41154155
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+ }
41174164
41184165 bindingset [ node, state, t0, ap]
41194166 predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
@@ -4331,7 +4378,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
43314378 import CallContextSensitivity< CallContextSensitivityInput >
43324379 import LocalCallContext
43334380
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 ;
43354393
43364394 bindingset [ node, state, t0, ap]
43374395 predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
0 commit comments