@@ -858,6 +858,7 @@ private module Stage1 {
858
858
pragma [ nomagic]
859
859
predicate revFlow ( NodeEx node , Configuration config ) { revFlow ( node , _, config ) }
860
860
861
+ bindingset [ node, state, config]
861
862
predicate revFlow (
862
863
NodeEx node , FlowState state , boolean toReturn , ApOption returnAp , Ap ap , Configuration config
863
864
) {
@@ -1110,6 +1111,8 @@ private module Stage2 {
1110
1111
bindingset [ node, cc, config]
1111
1112
private LocalCc getLocalCc ( NodeEx node , Cc cc , Configuration config ) { any ( ) }
1112
1113
1114
+ bindingset [ node1, state1, config]
1115
+ bindingset [ node2, state2, config]
1113
1116
private predicate localStep (
1114
1117
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
1115
1118
ApNil ap , Configuration config , LocalCc lcc
@@ -1145,6 +1148,7 @@ private module Stage2 {
1145
1148
private predicate typecheckStore ( Ap ap , DataFlowType contentType ) { any ( ) }
1146
1149
1147
1150
/* Begin: Stage 2 logic. */
1151
+ bindingset [ node, state, config]
1148
1152
private predicate flowCand ( NodeEx node , FlowState state , ApApprox apa , Configuration config ) {
1149
1153
PrevStage:: revFlow ( node , state , _, _, apa , config )
1150
1154
}
@@ -1907,6 +1911,7 @@ private module Stage3 {
1907
1911
}
1908
1912
1909
1913
/* Begin: Stage 3 logic. */
1914
+ bindingset [ node, state, config]
1910
1915
private predicate flowCand ( NodeEx node , FlowState state , ApApprox apa , Configuration config ) {
1911
1916
PrevStage:: revFlow ( node , state , _, _, apa , config )
1912
1917
}
@@ -2732,6 +2737,7 @@ private module Stage4 {
2732
2737
private predicate typecheckStore ( Ap ap , DataFlowType contentType ) { any ( ) }
2733
2738
2734
2739
/* Begin: Stage 4 logic. */
2740
+ bindingset [ node, state, config]
2735
2741
private predicate flowCand ( NodeEx node , FlowState state , ApApprox apa , Configuration config ) {
2736
2742
PrevStage:: revFlow ( node , state , _, _, apa , config )
2737
2743
}
@@ -4452,13 +4458,22 @@ private module FlowExploration {
4452
4458
}
4453
4459
}
4454
4460
4461
+ private predicate relevantState ( FlowState state ) {
4462
+ sourceNode ( _, state , _) or
4463
+ sinkNode ( _, state , _) or
4464
+ additionalLocalStateStep ( _, state , _, _, _) or
4465
+ additionalLocalStateStep ( _, _, _, state , _) or
4466
+ additionalJumpStateStep ( _, state , _, _, _) or
4467
+ additionalJumpStateStep ( _, _, _, state , _)
4468
+ }
4469
+
4455
4470
private newtype TSummaryCtx1 =
4456
4471
TSummaryCtx1None ( ) or
4457
4472
TSummaryCtx1Param ( ParamNodeEx p )
4458
4473
4459
4474
private newtype TSummaryCtx2 =
4460
4475
TSummaryCtx2None ( ) or
4461
- TSummaryCtx2Some ( FlowState s )
4476
+ TSummaryCtx2Some ( FlowState s ) { relevantState ( s ) }
4462
4477
4463
4478
private newtype TSummaryCtx3 =
4464
4479
TSummaryCtx3None ( ) or
@@ -4470,7 +4485,7 @@ private module FlowExploration {
4470
4485
4471
4486
private newtype TRevSummaryCtx2 =
4472
4487
TRevSummaryCtx2None ( ) or
4473
- TRevSummaryCtx2Some ( FlowState s )
4488
+ TRevSummaryCtx2Some ( FlowState s ) { relevantState ( s ) }
4474
4489
4475
4490
private newtype TRevSummaryCtx3 =
4476
4491
TRevSummaryCtx3None ( ) or
0 commit comments