@@ -2606,6 +2606,23 @@ 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+
26092626 /**
26102627 * Provides a big-step relation for local flow steps.
26112628 *
@@ -2614,25 +2631,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26142631 * reachable in this stage.
26152632 */
26162633 additional module LocalFlowBigStep< LocalFlowBigStepInputSig Input> {
2617- final private class NodeExFinal = NodeEx ;
2618-
2619- /**
2620- * A node where some checking is required, and hence the big-step relation
2621- * is not allowed to step over.
2622- */
2623- private class FlowCheckNode extends NodeExFinal {
2624- FlowCheckNode ( ) {
2625- revFlow ( this , _, _) and
2626- (
2627- castNode ( this .asNode ( ) ) or
2628- clearsContentCached ( this .asNode ( ) , _) or
2629- expectsContentCached ( this .asNode ( ) , _) or
2630- neverSkipInPathGraph ( this .asNode ( ) ) or
2631- Config:: neverSkip ( this .asNode ( ) )
2632- )
2633- }
2634- }
2635-
26362634 private predicate additionalLocalStateStep (
26372635 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , DataFlowType t ,
26382636 LocalCallContext lcc , string label
@@ -4414,15 +4412,19 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
44144412 private predicate smallStep = Stage3Param:: BigStepInput:: localStep / 8 ;
44154413
44164414 private predicate localStepCand (
4417- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2
4415+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue
44184416 ) {
4419- PrevStage :: revFlow ( node1 , state1 , _) and
4420- smallStep ( node1 , state1 , node2 , state2 , _ , _, _, _)
4417+ Stage5Param :: localStep ( node1 , state1 , _ , _ , _ , _ , _ , _) and
4418+ smallStep ( node1 , state1 , node2 , state2 , preservesValue , _, _, _)
44214419 or
44224420 exists ( FlowState midState , NodeEx midNode |
4423- localStepCand ( node1 , state1 , midNode , midState ) and
4421+ localStepCand ( node1 , state1 , midNode , midState , preservesValue ) and
44244422 smallStep ( midNode , midState , node2 , state2 , _, _, _, _) and
4425- not Stage5Param:: localStep ( midNode , midState , _, _, _, _, _, _)
4423+ not (
4424+ Stage5Param:: localStep ( midNode , midState , _, _, _, _, _, _) and
4425+ Stage5Param:: localStep ( _, _, midNode , midState , _, _, _, _)
4426+ ) and
4427+ not midNode instanceof Stage5:: FlowCheckNode
44264428 )
44274429 }
44284430
@@ -4439,7 +4441,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
44394441 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
44404442 DataFlowType t , LocalCallContext lcc , string label
44414443 ) {
4442- localStepCand ( node1 , state1 , node2 , state2 ) and
4444+ localStepCand ( node1 , state1 , node2 , state2 , preservesValue ) and
44434445 Stage5Param:: localStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
44444446 PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
44454447 PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
0 commit comments