@@ -3790,7 +3790,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
37903790 import CallContextSensitivity< CallContextSensitivityInput >
37913791 import NoLocalCallContext
37923792
3793- private module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
3793+ additional module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
37943794 bindingset [ node1, state1]
37953795 bindingset [ node2, state2]
37963796 predicate localStep (
@@ -4411,11 +4411,36 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
44114411 import LocalCallContext
44124412
44134413 private module BigStepInput implements PrevStage:: LocalFlowBigStepInputSig {
4414+ private predicate smallStep = Stage3Param:: BigStepInput:: localStep / 8 ;
4415+
4416+ private predicate localStepCand (
4417+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2
4418+ ) {
4419+ PrevStage:: revFlow ( node1 , state1 , _) and
4420+ smallStep ( node1 , state1 , node2 , state2 , _, _, _, _)
4421+ or
4422+ exists ( FlowState midState , NodeEx midNode |
4423+ localStepCand ( node1 , state1 , midNode , midState ) and
4424+ smallStep ( midNode , midState , node2 , state2 , _, _, _, _) and
4425+ not Stage5Param:: localStep ( midNode , midState , _, _, _, _, _, _)
4426+ )
4427+ }
4428+
4429+ /**
4430+ * When calculating `localFlowBigStep` based on `Stage5Param::localStep`, which
4431+ * is already a big-step relation, we must be careful to avoid quadratic blowup.
4432+ *
4433+ * This is achieved by restricting `Stage5Param::localStep` to those node pairs
4434+ * reacheable via 1 or more `smallStep`s, where any intermediate node is not
4435+ * already part of `Stage5Param::localStep`.
4436+ */
4437+ pragma [ nomagic]
44144438 predicate localStep (
44154439 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
44164440 DataFlowType t , LocalCallContext lcc , string label
44174441 ) {
4418- Stage3Param:: localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
4442+ localStepCand ( node1 , state1 , node2 , state2 ) and
4443+ Stage5Param:: localStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
44194444 PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
44204445 PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
44214446 }
0 commit comments