@@ -2596,31 +2596,27 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
25962596 callEdgeReturn ( call , c , _, _, _, _, _)
25972597 }
25982598
2599- /** Provides the input to `LocalFlowBigStep`. */
2600- signature module LocalFlowBigStepInputSig {
2601- bindingset [ node1, state1]
2602- bindingset [ node2, state2]
2603- predicate localStep (
2604- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2605- DataFlowType t , LocalCallContext lcc , string label
2606- ) ;
2607- }
2599+ /** Holds if `node1` can step to `node2` in one or more local steps. */
2600+ bindingset [ node1, state1]
2601+ bindingset [ node2, state2]
2602+ signature predicate localStepSig (
2603+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2604+ DataFlowType t , LocalCallContext lcc , string label
2605+ ) ;
26082606
26092607 /**
26102608 * Provides a big-step relation for local flow steps.
26112609 *
2612- * The big-step releation is based on the `localStep ` relation from the
2613- * input module, restricted to nodes that are forwards and backwards
2614- * reachable in this stage.
2610+ * The big-step releation is based on the `localStepInput ` relation,
2611+ * restricted to nodes that are forwards and backwards reachable in
2612+ * this stage.
26152613 */
2616- additional module LocalFlowBigStep< LocalFlowBigStepInputSig Input> {
2617- final private class NodeExFinal = NodeEx ;
2618-
2614+ additional module LocalFlowBigStep< localStepSig / 8 localStepInput> {
26192615 /**
26202616 * A node where some checking is required, and hence the big-step relation
26212617 * is not allowed to step over.
26222618 */
2623- private class FlowCheckNode extends NodeExFinal {
2619+ private class FlowCheckNode extends NodeEx {
26242620 FlowCheckNode ( ) {
26252621 revFlow ( this , _, _) and
26262622 (
@@ -2640,7 +2636,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26402636 exists ( ApNil nil |
26412637 revFlow ( node1 , state1 , pragma [ only_bind_into ] ( nil ) ) and
26422638 revFlow ( node2 , state2 , pragma [ only_bind_into ] ( nil ) ) and
2643- Input :: localStep ( node1 , state1 , node2 , state2 , false , t , lcc , label ) and
2639+ localStepInput ( node1 , state1 , node2 , state2 , false , t , lcc , label ) and
26442640 state1 != state2
26452641 )
26462642 }
@@ -2734,7 +2730,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
27342730 not inBarrier ( node2 , state ) and
27352731 not outBarrier ( node1 , state ) and
27362732 exists ( NodeEx mid , boolean preservesValue2 , DataFlowType t2 , string label2 , Ap ap |
2737- Input :: localStep ( mid , state , node2 , state , preservesValue2 , t2 , cc , label2 ) and
2733+ localStepInput ( mid , state , node2 , state , preservesValue2 , t2 , cc , label2 ) and
27382734 revFlow ( node2 , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( ap ) ) and
27392735 not outBarrier ( mid , state ) and
27402736 ( preservesValue = true or ap instanceof ApNil )
@@ -2769,6 +2765,33 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
27692765 exists ( Ap ap |
27702766 localFlowStepPlus ( node1 , state1 , node2 , preservesValue , t , callContext , label ) and
27712767 localFlowExit ( node2 , state1 , ap ) and
2768+ state1 = state2 and
2769+ node1 != node2
2770+ |
2771+ preservesValue = true or ap instanceof ApNil
2772+ )
2773+ or
2774+ additionalLocalStateStep ( node1 , state1 , node2 , state2 , t , callContext , label ) and
2775+ preservesValue = false
2776+ }
2777+
2778+ /**
2779+ * Holds if `node1` can step to `node2` in one or more local steps and this
2780+ * path can occur as a maximal subsequence of local steps in a dataflow path.
2781+ *
2782+ * This predicate should be used when `localStepInput` is already a big-step
2783+ * relation, which will do the same as `localFlowBigStep`, but avoids potential
2784+ * worst-case quadratic complexity.
2785+ */
2786+ pragma [ nomagic]
2787+ predicate localFlowBigStepTc (
2788+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2789+ DataFlowType t , LocalCallContext callContext , string label
2790+ ) {
2791+ exists ( Ap ap |
2792+ localFlowEntry ( node1 , pragma [ only_bind_into ] ( state1 ) , pragma [ only_bind_into ] ( ap ) ) and
2793+ localStepInput ( node1 , state1 , node2 , state2 , preservesValue , t , callContext , label ) and
2794+ localFlowExit ( node2 , pragma [ only_bind_into ] ( state2 ) , pragma [ only_bind_into ] ( ap ) ) and
27722795 state1 = state2
27732796 |
27742797 preservesValue = true or ap instanceof ApNil
@@ -3790,27 +3813,25 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
37903813 import CallContextSensitivity< CallContextSensitivityInput >
37913814 import NoLocalCallContext
37923815
3793- private module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
3794- bindingset [ node1, state1]
3795- bindingset [ node2, state2]
3796- predicate localStep (
3797- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3798- DataFlowType t , LocalCallContext lcc , string label
3799- ) {
3800- localStepNodeCand1 ( node1 , node2 , preservesValue , t , lcc , label ) and
3801- state1 = state2
3802- or
3803- localStateStepNodeCand1 ( node1 , state1 , node2 , state2 , t , lcc , label ) and
3804- preservesValue = false
3805- }
3816+ bindingset [ node1, state1]
3817+ bindingset [ node2, state2]
3818+ private predicate localStepInput (
3819+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3820+ DataFlowType t , LocalCallContext lcc , string label
3821+ ) {
3822+ localStepNodeCand1 ( node1 , node2 , preservesValue , t , lcc , label ) and
3823+ state1 = state2
3824+ or
3825+ localStateStepNodeCand1 ( node1 , state1 , node2 , state2 , t , lcc , label ) and
3826+ preservesValue = false
38063827 }
38073828
38083829 additional predicate localFlowBigStep (
38093830 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
38103831 DataFlowType t , LocalCallContext lcc , string label
38113832 ) {
3812- PrevStage:: LocalFlowBigStep< BigStepInput > :: localFlowBigStep ( node1 , state1 , node2 , state2 ,
3813- preservesValue , t , lcc , label )
3833+ PrevStage:: LocalFlowBigStep< localStepInput / 8 > :: localFlowBigStep ( node1 , state1 , node2 ,
3834+ state2 , preservesValue , t , lcc , label )
38143835 }
38153836
38163837 bindingset [ node1, state1]
@@ -4205,14 +4226,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
42054226 import CallContextSensitivity< CallContextSensitivityInput >
42064227 import LocalCallContext
42074228
4208- predicate localStep (
4209- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
4210- Typ t , LocalCc lcc , string label
4211- ) {
4212- Stage3Param:: localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
4213- PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
4214- PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
4215- }
4229+ predicate localStep =
4230+ PrevStage:: LocalFlowBigStep< Stage3Param:: localFlowBigStep / 8 > :: localFlowBigStepTc / 8 ;
42164231
42174232 bindingset [ node, state, t0, ap]
42184233 predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
@@ -4410,18 +4425,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
44104425 import CallContextSensitivity< CallContextSensitivityInput >
44114426 import LocalCallContext
44124427
4413- private module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
4414- predicate localStep (
4415- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
4416- DataFlowType t , LocalCallContext lcc , string label
4417- ) {
4418- Stage3Param:: localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
4419- PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
4420- PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
4421- }
4422- }
4423-
4424- predicate localStep = PrevStage:: LocalFlowBigStep< BigStepInput > :: localFlowBigStep / 8 ;
4428+ predicate localStep =
4429+ PrevStage:: LocalFlowBigStep< Stage5Param:: localStep / 8 > :: localFlowBigStepTc / 8 ;
44254430
44264431 bindingset [ node, state, t0, ap]
44274432 predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
0 commit comments