@@ -2606,23 +2606,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26062606 ) ;
26072607 }
26082608
2609- /**
2610- * A node where some checking is required, and hence the big-step relation
2611- * is not allowed to step over.
2612- */
2613- additional class FlowCheckNode extends NodeEx {
2614- FlowCheckNode ( ) {
2615- revFlow ( this , _, _) and
2616- (
2617- castNode ( this .asNode ( ) ) or
2618- clearsContentCached ( this .asNode ( ) , _) or
2619- expectsContentCached ( this .asNode ( ) , _) or
2620- neverSkipInPathGraph ( this .asNode ( ) ) or
2621- Config:: neverSkip ( this .asNode ( ) )
2622- )
2623- }
2624- }
2625-
26262609 /**
26272610 * Provides a big-step relation for local flow steps.
26282611 *
@@ -2631,6 +2614,23 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26312614 * reachable in this stage.
26322615 */
26332616 additional module LocalFlowBigStep< LocalFlowBigStepInputSig Input> {
2617+ /**
2618+ * A node where some checking is required, and hence the big-step relation
2619+ * is not allowed to step over.
2620+ */
2621+ private class FlowCheckNode extends NodeEx {
2622+ FlowCheckNode ( ) {
2623+ revFlow ( this , _, _) and
2624+ (
2625+ castNode ( this .asNode ( ) ) or
2626+ clearsContentCached ( this .asNode ( ) , _) or
2627+ expectsContentCached ( this .asNode ( ) , _) or
2628+ neverSkipInPathGraph ( this .asNode ( ) ) or
2629+ Config:: neverSkip ( this .asNode ( ) )
2630+ )
2631+ }
2632+ }
2633+
26342634 private predicate additionalLocalStateStep (
26352635 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , DataFlowType t ,
26362636 LocalCallContext lcc , string label
@@ -2767,6 +2767,33 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
27672767 exists ( Ap ap |
27682768 localFlowStepPlus ( node1 , state1 , node2 , preservesValue , t , callContext , label ) and
27692769 localFlowExit ( node2 , state1 , ap ) and
2770+ state1 = state2 and
2771+ node1 != node2
2772+ |
2773+ preservesValue = true or ap instanceof ApNil
2774+ )
2775+ or
2776+ additionalLocalStateStep ( node1 , state1 , node2 , state2 , t , callContext , label ) and
2777+ preservesValue = false
2778+ }
2779+
2780+ /**
2781+ * Holds if `node1` can step to `node2` in one or more local steps and this
2782+ * path can occur as a maximal subsequence of local steps in a dataflow path.
2783+ *
2784+ * This predicate should be used when `Input::localStep` is already a big-step
2785+ * relation, which will do the same as `localFlowBigStep`, but avoids potential
2786+ * worst-case quadratic complexity.
2787+ */
2788+ pragma [ nomagic]
2789+ predicate localFlowBigStepTc (
2790+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2791+ DataFlowType t , LocalCallContext callContext , string label
2792+ ) {
2793+ exists ( Ap ap |
2794+ localFlowEntry ( node1 , state1 , ap ) and
2795+ Input:: localStep ( node1 , state1 , node2 , state2 , preservesValue , t , callContext , label ) and
2796+ localFlowExit ( node2 , state2 , ap ) and
27702797 state1 = state2
27712798 |
27722799 preservesValue = true or ap instanceof ApNil
@@ -3788,7 +3815,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
37883815 import CallContextSensitivity< CallContextSensitivityInput >
37893816 import NoLocalCallContext
37903817
3791- additional module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
3818+ private module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
37923819 bindingset [ node1, state1]
37933820 bindingset [ node2, state2]
37943821 predicate localStep (
@@ -4203,15 +4230,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
42034230 import CallContextSensitivity< CallContextSensitivityInput >
42044231 import LocalCallContext
42054232
4206- predicate localStep (
4207- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
4208- Typ t , LocalCc lcc , string label
4209- ) {
4210- Stage3Param:: localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
4211- PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
4212- PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
4233+ private module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
4234+ predicate localStep = Stage3Param:: localFlowBigStep / 8 ;
42134235 }
42144236
4237+ predicate localStep = PrevStage:: LocalFlowBigStep< BigStepInput > :: localFlowBigStepTc / 8 ;
4238+
42154239 bindingset [ node, state, t0, ap]
42164240 predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
42174241 strengthenType ( node , t0 , t ) and
@@ -4409,46 +4433,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
44094433 import LocalCallContext
44104434
44114435 private module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
4412- private predicate smallStep = Stage3Param:: BigStepInput:: localStep / 8 ;
4413-
4414- private predicate localStepCand (
4415- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue
4416- ) {
4417- Stage5Param:: localStep ( node1 , state1 , _, _, _, _, _, _) and
4418- smallStep ( node1 , state1 , node2 , state2 , preservesValue , _, _, _)
4419- or
4420- exists ( FlowState midState , NodeEx midNode |
4421- localStepCand ( node1 , state1 , midNode , midState , preservesValue ) and
4422- smallStep ( midNode , midState , node2 , state2 , _, _, _, _) and
4423- not (
4424- Stage5Param:: localStep ( midNode , midState , _, _, _, _, _, _) and
4425- Stage5Param:: localStep ( _, _, midNode , midState , _, _, _, _)
4426- ) and
4427- not midNode instanceof Stage5:: FlowCheckNode
4428- )
4429- }
4430-
4431- /**
4432- * When calculating `localFlowBigStep` based on `Stage5Param::localStep`, which
4433- * is already a big-step relation, we must be careful to avoid quadratic blowup.
4434- *
4435- * This is achieved by restricting `Stage5Param::localStep` to those node pairs
4436- * reacheable via 1 or more `smallStep`s, where any intermediate node is not
4437- * already part of `Stage5Param::localStep`.
4438- */
4439- pragma [ nomagic]
4440- predicate localStep (
4441- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
4442- DataFlowType t , LocalCallContext lcc , string label
4443- ) {
4444- localStepCand ( node1 , state1 , node2 , state2 , preservesValue ) and
4445- Stage5Param:: localStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
4446- PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
4447- PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
4448- }
4436+ predicate localStep = Stage5Param:: localStep / 8 ;
44494437 }
44504438
4451- predicate localStep = PrevStage:: LocalFlowBigStep< BigStepInput > :: localFlowBigStep / 8 ;
4439+ predicate localStep = PrevStage:: LocalFlowBigStep< BigStepInput > :: localFlowBigStepTc / 8 ;
44524440
44534441 bindingset [ node, state, t0, ap]
44544442 predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
0 commit comments