@@ -3772,7 +3772,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
37723772 import CallContextSensitivity< CallContextSensitivityInput >
37733773 import NoLocalCallContext
37743774
3775- private module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
3775+ additional module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
37763776 bindingset [ node1, state1]
37773777 bindingset [ node2, state2]
37783778 predicate localStep (
@@ -4393,11 +4393,36 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
43934393 import LocalCallContext
43944394
43954395 private module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
4396+ private predicate smallStep = Stage3Param:: BigStepInput:: localStep / 8 ;
4397+
4398+ private predicate localStepCand (
4399+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2
4400+ ) {
4401+ PrevStage:: revFlow ( node1 , state1 , _) and
4402+ smallStep ( node1 , state1 , node2 , state2 , _, _, _, _)
4403+ or
4404+ exists ( FlowState midState , NodeEx midNode |
4405+ localStepCand ( node1 , state1 , midNode , midState ) and
4406+ smallStep ( midNode , midState , node2 , state2 , _, _, _, _) and
4407+ not PrevStage:: revFlow ( midNode , midState , _)
4408+ )
4409+ }
4410+
4411+ /**
4412+ * When calculating `localFlowBigStep` based on `Stage5Param::localStep`, which
4413+ * is already a big-step relation, we must be careful to avoid quadratic blowup.
4414+ *
4415+ * This is achieved by restricting `Stage5Param::localStep` to those node pairs
4416+ * reacheable via 1 or more `smallStep`s, where any intermediate node is not
4417+ * already part of `Stage5Param::localStep`.
4418+ */
4419+ pragma [ nomagic]
43964420 predicate localStep (
43974421 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
43984422 DataFlowType t , LocalCallContext lcc , string label
43994423 ) {
4400- Stage3Param:: localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
4424+ localStepCand ( node1 , state1 , node2 , state2 ) and
4425+ Stage5Param:: localStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
44014426 PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
44024427 PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
44034428 }
0 commit comments