@@ -2603,31 +2603,27 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26032603 callEdgeReturn ( call , c , _, _, _, _, _)
26042604 }
26052605
2606- /** Provides the input to `LocalFlowBigStep`. */
2607- signature module LocalFlowBigStepInputSig {
2608- bindingset [ node1, state1]
2609- bindingset [ node2, state2]
2610- predicate localStep (
2611- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2612- DataFlowType t , LocalCallContext lcc , string label
2613- ) ;
2614- }
2606+ /** Holds if `node1` can step to `node2` in one or more local steps. */
2607+ bindingset [ node1, state1]
2608+ bindingset [ node2, state2]
2609+ signature predicate localStepSig (
2610+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2611+ DataFlowType t , LocalCallContext lcc , string label
2612+ ) ;
26152613
26162614 /**
26172615 * Provides a big-step relation for local flow steps.
26182616 *
2619- * The big-step releation is based on the `localStep ` relation from the
2620- * input module, restricted to nodes that are forwards and backwards
2621- * reachable in this stage.
2617+ * The big-step releation is based on the `localStepInput ` relation,
2618+ * restricted to nodes that are forwards and backwards reachable in
2619+ * this stage.
26222620 */
2623- additional module LocalFlowBigStep< LocalFlowBigStepInputSig Input> {
2624- final private class NodeExFinal = NodeEx ;
2625-
2621+ additional module LocalFlowBigStep< localStepSig / 8 localStepInput> {
26262622 /**
26272623 * A node where some checking is required, and hence the big-step relation
26282624 * is not allowed to step over.
26292625 */
2630- private class FlowCheckNode extends NodeExFinal {
2626+ private class FlowCheckNode extends NodeEx {
26312627 FlowCheckNode ( ) {
26322628 revFlow ( this , _, _) and
26332629 (
@@ -2647,7 +2643,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26472643 exists ( ApNil nil |
26482644 revFlow ( node1 , state1 , pragma [ only_bind_into ] ( nil ) ) and
26492645 revFlow ( node2 , state2 , pragma [ only_bind_into ] ( nil ) ) and
2650- Input :: localStep ( node1 , state1 , node2 , state2 , false , t , lcc , label ) and
2646+ localStepInput ( node1 , state1 , node2 , state2 , false , t , lcc , label ) and
26512647 state1 != state2
26522648 )
26532649 }
@@ -2741,7 +2737,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
27412737 not inBarrier ( node2 , state ) and
27422738 not outBarrier ( node1 , state ) and
27432739 exists ( NodeEx mid , boolean preservesValue2 , DataFlowType t2 , string label2 , Ap ap |
2744- Input :: localStep ( mid , state , node2 , state , preservesValue2 , t2 , cc , label2 ) and
2740+ localStepInput ( mid , state , node2 , state , preservesValue2 , t2 , cc , label2 ) and
27452741 revFlow ( node2 , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( ap ) ) and
27462742 not outBarrier ( mid , state ) and
27472743 ( preservesValue = true or ap instanceof ApNil )
@@ -2776,6 +2772,33 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
27762772 exists ( Ap ap |
27772773 localFlowStepPlus ( node1 , state1 , node2 , preservesValue , t , callContext , label ) and
27782774 localFlowExit ( node2 , state1 , ap ) and
2775+ state1 = state2 and
2776+ node1 != node2
2777+ |
2778+ preservesValue = true or ap instanceof ApNil
2779+ )
2780+ or
2781+ additionalLocalStateStep ( node1 , state1 , node2 , state2 , t , callContext , label ) and
2782+ preservesValue = false
2783+ }
2784+
2785+ /**
2786+ * Holds if `node1` can step to `node2` in one or more local steps and this
2787+ * path can occur as a maximal subsequence of local steps in a dataflow path.
2788+ *
2789+ * This predicate should be used when `localStepInput` is already a big-step
2790+ * relation, which will do the same as `localFlowBigStep`, but avoids potential
2791+ * worst-case quadratic complexity.
2792+ */
2793+ pragma [ nomagic]
2794+ predicate localFlowBigStepTc (
2795+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2796+ DataFlowType t , LocalCallContext callContext , string label
2797+ ) {
2798+ exists ( Ap ap |
2799+ localFlowEntry ( node1 , pragma [ only_bind_into ] ( state1 ) , pragma [ only_bind_into ] ( ap ) ) and
2800+ localStepInput ( node1 , state1 , node2 , state2 , preservesValue , t , callContext , label ) and
2801+ localFlowExit ( node2 , pragma [ only_bind_into ] ( state2 ) , pragma [ only_bind_into ] ( ap ) ) and
27792802 state1 = state2
27802803 |
27812804 preservesValue = true or ap instanceof ApNil
@@ -3796,27 +3819,25 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
37963819 import CallContextSensitivity< CallContextSensitivityInput >
37973820 import NoLocalCallContext
37983821
3799- private module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
3800- bindingset [ node1, state1]
3801- bindingset [ node2, state2]
3802- predicate localStep (
3803- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3804- DataFlowType t , LocalCallContext lcc , string label
3805- ) {
3806- localStepNodeCand1 ( node1 , node2 , preservesValue , t , lcc , label ) and
3807- state1 = state2
3808- or
3809- localStateStepNodeCand1 ( node1 , state1 , node2 , state2 , t , lcc , label ) and
3810- preservesValue = false
3811- }
3822+ bindingset [ node1, state1]
3823+ bindingset [ node2, state2]
3824+ private predicate localStepInput (
3825+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3826+ DataFlowType t , LocalCallContext lcc , string label
3827+ ) {
3828+ localStepNodeCand1 ( node1 , node2 , preservesValue , t , lcc , label ) and
3829+ state1 = state2
3830+ or
3831+ localStateStepNodeCand1 ( node1 , state1 , node2 , state2 , t , lcc , label ) and
3832+ preservesValue = false
38123833 }
38133834
38143835 additional predicate localFlowBigStep (
38153836 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
38163837 DataFlowType t , LocalCallContext lcc , string label
38173838 ) {
3818- PrevStage:: LocalFlowBigStep< BigStepInput > :: localFlowBigStep ( node1 , state1 , node2 , state2 ,
3819- preservesValue , t , lcc , label )
3839+ PrevStage:: LocalFlowBigStep< localStepInput / 8 > :: localFlowBigStep ( node1 , state1 , node2 ,
3840+ state2 , preservesValue , t , lcc , label )
38203841 }
38213842
38223843 bindingset [ node1, state1]
@@ -4211,14 +4232,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
42114232 import CallContextSensitivity< CallContextSensitivityInput >
42124233 import LocalCallContext
42134234
4214- predicate localStep (
4215- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
4216- Typ t , LocalCc lcc , string label
4217- ) {
4218- Stage3Param:: localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
4219- PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
4220- PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
4221- }
4235+ predicate localStep =
4236+ PrevStage:: LocalFlowBigStep< Stage3Param:: localFlowBigStep / 8 > :: localFlowBigStepTc / 8 ;
42224237
42234238 bindingset [ node, state, t0, ap]
42244239 predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
@@ -4416,18 +4431,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
44164431 import CallContextSensitivity< CallContextSensitivityInput >
44174432 import LocalCallContext
44184433
4419- private module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
4420- predicate localStep (
4421- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
4422- DataFlowType t , LocalCallContext lcc , string label
4423- ) {
4424- Stage3Param:: localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
4425- PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
4426- PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
4427- }
4428- }
4429-
4430- predicate localStep = PrevStage:: LocalFlowBigStep< BigStepInput > :: localFlowBigStep / 8 ;
4434+ predicate localStep =
4435+ PrevStage:: LocalFlowBigStep< Stage5Param:: localStep / 8 > :: localFlowBigStepTc / 8 ;
44314436
44324437 bindingset [ node, state, t0, ap]
44334438 predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
0 commit comments