@@ -2596,31 +2596,27 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2596
2596
callEdgeReturn ( call , c , _, _, _, _, _)
2597
2597
}
2598
2598
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
+ ) ;
2608
2606
2609
2607
/**
2610
2608
* Provides a big-step relation for local flow steps.
2611
2609
*
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.
2615
2613
*/
2616
- additional module LocalFlowBigStep< LocalFlowBigStepInputSig Input> {
2617
- final private class NodeExFinal = NodeEx ;
2618
-
2614
+ additional module LocalFlowBigStep< localStepSig / 8 localStepInput> {
2619
2615
/**
2620
2616
* A node where some checking is required, and hence the big-step relation
2621
2617
* is not allowed to step over.
2622
2618
*/
2623
- private class FlowCheckNode extends NodeExFinal {
2619
+ private class FlowCheckNode extends NodeEx {
2624
2620
FlowCheckNode ( ) {
2625
2621
revFlow ( this , _, _) and
2626
2622
(
@@ -2640,7 +2636,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2640
2636
exists ( ApNil nil |
2641
2637
revFlow ( node1 , state1 , pragma [ only_bind_into ] ( nil ) ) and
2642
2638
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
2644
2640
state1 != state2
2645
2641
)
2646
2642
}
@@ -2734,7 +2730,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2734
2730
not inBarrier ( node2 , state ) and
2735
2731
not outBarrier ( node1 , state ) and
2736
2732
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
2738
2734
revFlow ( node2 , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( ap ) ) and
2739
2735
not outBarrier ( mid , state ) and
2740
2736
( preservesValue = true or ap instanceof ApNil )
@@ -2769,6 +2765,33 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2769
2765
exists ( Ap ap |
2770
2766
localFlowStepPlus ( node1 , state1 , node2 , preservesValue , t , callContext , label ) and
2771
2767
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
2772
2795
state1 = state2
2773
2796
|
2774
2797
preservesValue = true or ap instanceof ApNil
@@ -3790,27 +3813,25 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3790
3813
import CallContextSensitivity< CallContextSensitivityInput >
3791
3814
import NoLocalCallContext
3792
3815
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
3806
3827
}
3807
3828
3808
3829
additional predicate localFlowBigStep (
3809
3830
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3810
3831
DataFlowType t , LocalCallContext lcc , string label
3811
3832
) {
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 )
3814
3835
}
3815
3836
3816
3837
bindingset [ node1, state1]
@@ -4205,14 +4226,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
4205
4226
import CallContextSensitivity< CallContextSensitivityInput >
4206
4227
import LocalCallContext
4207
4228
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 ;
4216
4231
4217
4232
bindingset [ node, state, t0, ap]
4218
4233
predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
@@ -4410,18 +4425,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
4410
4425
import CallContextSensitivity< CallContextSensitivityInput >
4411
4426
import LocalCallContext
4412
4427
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 ;
4425
4430
4426
4431
bindingset [ node, state, t0, ap]
4427
4432
predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
0 commit comments