@@ -2603,31 +2603,27 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2603
2603
callEdgeReturn ( call , c , _, _, _, _, _)
2604
2604
}
2605
2605
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
+ ) ;
2615
2613
2616
2614
/**
2617
2615
* Provides a big-step relation for local flow steps.
2618
2616
*
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.
2622
2620
*/
2623
- additional module LocalFlowBigStep< LocalFlowBigStepInputSig Input> {
2624
- final private class NodeExFinal = NodeEx ;
2625
-
2621
+ additional module LocalFlowBigStep< localStepSig / 8 localStepInput> {
2626
2622
/**
2627
2623
* A node where some checking is required, and hence the big-step relation
2628
2624
* is not allowed to step over.
2629
2625
*/
2630
- private class FlowCheckNode extends NodeExFinal {
2626
+ private class FlowCheckNode extends NodeEx {
2631
2627
FlowCheckNode ( ) {
2632
2628
revFlow ( this , _, _) and
2633
2629
(
@@ -2647,7 +2643,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2647
2643
exists ( ApNil nil |
2648
2644
revFlow ( node1 , state1 , pragma [ only_bind_into ] ( nil ) ) and
2649
2645
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
2651
2647
state1 != state2
2652
2648
)
2653
2649
}
@@ -2741,7 +2737,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2741
2737
not inBarrier ( node2 , state ) and
2742
2738
not outBarrier ( node1 , state ) and
2743
2739
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
2745
2741
revFlow ( node2 , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( ap ) ) and
2746
2742
not outBarrier ( mid , state ) and
2747
2743
( preservesValue = true or ap instanceof ApNil )
@@ -2776,6 +2772,33 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2776
2772
exists ( Ap ap |
2777
2773
localFlowStepPlus ( node1 , state1 , node2 , preservesValue , t , callContext , label ) and
2778
2774
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
2779
2802
state1 = state2
2780
2803
|
2781
2804
preservesValue = true or ap instanceof ApNil
@@ -3796,27 +3819,25 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3796
3819
import CallContextSensitivity< CallContextSensitivityInput >
3797
3820
import NoLocalCallContext
3798
3821
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
3812
3833
}
3813
3834
3814
3835
additional predicate localFlowBigStep (
3815
3836
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3816
3837
DataFlowType t , LocalCallContext lcc , string label
3817
3838
) {
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 )
3820
3841
}
3821
3842
3822
3843
bindingset [ node1, state1]
@@ -4211,14 +4232,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
4211
4232
import CallContextSensitivity< CallContextSensitivityInput >
4212
4233
import LocalCallContext
4213
4234
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 ;
4222
4237
4223
4238
bindingset [ node, state, t0, ap]
4224
4239
predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
@@ -4416,18 +4431,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
4416
4431
import CallContextSensitivity< CallContextSensitivityInput >
4417
4432
import LocalCallContext
4418
4433
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 ;
4431
4436
4432
4437
bindingset [ node, state, t0, ap]
4433
4438
predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
0 commit comments