@@ -502,7 +502,7 @@ pragma[inline]
502
502
private predicate read ( NodeEx node1 , Content c , NodeEx node2 , Configuration config ) {
503
503
exists ( ContentSet cs |
504
504
readSet ( node1 , cs , node2 , config ) and
505
- c = cs .getAReadContent ( )
505
+ pragma [ only_bind_out ] ( c ) = pragma [ only_bind_into ] ( cs ) .getAReadContent ( )
506
506
)
507
507
}
508
508
@@ -511,10 +511,22 @@ pragma[inline]
511
511
private predicate clearsContentEx ( NodeEx n , Content c ) {
512
512
exists ( ContentSet cs |
513
513
clearsContentCached ( n .asNode ( ) , cs ) and
514
- c = cs .getAReadContent ( )
514
+ pragma [ only_bind_out ] ( c ) = pragma [ only_bind_into ] ( cs ) .getAReadContent ( )
515
+ )
516
+ }
517
+
518
+ // inline to reduce fan-out via `getAReadContent`
519
+ pragma [ inline]
520
+ private predicate expectsContentEx ( NodeEx n , Content c ) {
521
+ exists ( ContentSet cs |
522
+ expectsContentCached ( n .asNode ( ) , cs ) and
523
+ pragma [ only_bind_out ] ( c ) = pragma [ only_bind_into ] ( cs ) .getAReadContent ( )
515
524
)
516
525
}
517
526
527
+ pragma [ nomagic]
528
+ private predicate notExpectsContent ( NodeEx n ) { not expectsContentCached ( n .asNode ( ) , _) }
529
+
518
530
pragma [ nomagic]
519
531
private predicate store (
520
532
NodeEx node1 , TypedContent tc , NodeEx node2 , DataFlowType contentType , Configuration config
@@ -793,7 +805,7 @@ private module Stage1 {
793
805
* by `revFlow`.
794
806
*/
795
807
pragma [ nomagic]
796
- private predicate revFlowIsReadAndStored ( Content c , Configuration conf ) {
808
+ predicate revFlowIsReadAndStored ( Content c , Configuration conf ) {
797
809
revFlowConsCand ( c , conf ) and
798
810
revFlowStore ( c , _, _, conf )
799
811
}
@@ -891,7 +903,7 @@ private module Stage1 {
891
903
892
904
pragma [ nomagic]
893
905
predicate readStepCand ( NodeEx n1 , Content c , NodeEx n2 , Configuration config ) {
894
- revFlowIsReadAndStored ( pragma [ only_bind_into ] ( c ) , pragma [ only_bind_into ] ( config ) ) and
906
+ revFlowIsReadAndStored ( c , pragma [ only_bind_into ] ( config ) ) and
895
907
read ( n1 , c , n2 , pragma [ only_bind_into ] ( config ) ) and
896
908
revFlow ( n2 , pragma [ only_bind_into ] ( config ) )
897
909
}
@@ -1181,11 +1193,26 @@ private module Stage2 {
1181
1193
1182
1194
private predicate flowIntoCall = flowIntoCallNodeCand1 / 5 ;
1183
1195
1196
+ pragma [ nomagic]
1197
+ private predicate expectsContentCand ( NodeEx node , Configuration config ) {
1198
+ exists ( Content c |
1199
+ PrevStage:: revFlow ( node , pragma [ only_bind_into ] ( config ) ) and
1200
+ PrevStage:: revFlowIsReadAndStored ( c , pragma [ only_bind_into ] ( config ) ) and
1201
+ expectsContentEx ( node , c )
1202
+ )
1203
+ }
1204
+
1184
1205
bindingset [ node, state, ap, config]
1185
1206
private predicate filter ( NodeEx node , FlowState state , Ap ap , Configuration config ) {
1186
1207
PrevStage:: revFlowState ( state , pragma [ only_bind_into ] ( config ) ) and
1187
1208
exists ( ap ) and
1188
- not stateBarrier ( node , state , config )
1209
+ not stateBarrier ( node , state , config ) and
1210
+ (
1211
+ notExpectsContent ( node )
1212
+ or
1213
+ ap = true and
1214
+ expectsContentCand ( node , config )
1215
+ )
1189
1216
}
1190
1217
1191
1218
bindingset [ ap, contentType]
@@ -1740,7 +1767,8 @@ private module LocalFlowBigStep {
1740
1767
private class FlowCheckNode extends NodeEx {
1741
1768
FlowCheckNode ( ) {
1742
1769
castNode ( this .asNode ( ) ) or
1743
- clearsContentCached ( this .asNode ( ) , _)
1770
+ clearsContentCached ( this .asNode ( ) , _) or
1771
+ expectsContentCached ( this .asNode ( ) , _)
1744
1772
}
1745
1773
}
1746
1774
@@ -1979,6 +2007,16 @@ private module Stage3 {
1979
2007
clearContent ( node , ap .getHead ( ) .getContent ( ) , config )
1980
2008
}
1981
2009
2010
+ pragma [ nomagic]
2011
+ private predicate expectsContentCand ( NodeEx node , Ap ap , Configuration config ) {
2012
+ exists ( Content c |
2013
+ PrevStage:: revFlow ( node , pragma [ only_bind_into ] ( config ) ) and
2014
+ PrevStage:: readStepCand ( _, c , _, pragma [ only_bind_into ] ( config ) ) and
2015
+ expectsContentEx ( node , c ) and
2016
+ c = ap .getHead ( ) .getContent ( )
2017
+ )
2018
+ }
2019
+
1982
2020
pragma [ nomagic]
1983
2021
private predicate castingNodeEx ( NodeEx node ) { node .asNode ( ) instanceof CastingNode }
1984
2022
@@ -1987,7 +2025,12 @@ private module Stage3 {
1987
2025
exists ( state ) and
1988
2026
exists ( config ) and
1989
2027
not clear ( node , ap , config ) and
1990
- if castingNodeEx ( node ) then compatibleTypes ( node .getDataFlowType ( ) , ap .getType ( ) ) else any ( )
2028
+ ( if castingNodeEx ( node ) then compatibleTypes ( node .getDataFlowType ( ) , ap .getType ( ) ) else any ( ) ) and
2029
+ (
2030
+ notExpectsContent ( node )
2031
+ or
2032
+ expectsContentCand ( node , ap , config )
2033
+ )
1991
2034
}
1992
2035
1993
2036
bindingset [ ap, contentType]
@@ -4609,6 +4652,10 @@ private module FlowExploration {
4609
4652
exists ( PartialPathNodeRev mid |
4610
4653
revPartialPathStep ( mid , node , state , sc1 , sc2 , sc3 , ap , config ) and
4611
4654
not clearsContentEx ( node , ap .getHead ( ) ) and
4655
+ (
4656
+ notExpectsContent ( node ) or
4657
+ expectsContentEx ( node , ap .getHead ( ) )
4658
+ ) and
4612
4659
not fullBarrier ( node , config ) and
4613
4660
not stateBarrier ( node , state , config ) and
4614
4661
distSink ( node .getEnclosingCallable ( ) , config ) <= config .explorationLimit ( )
@@ -4625,6 +4672,10 @@ private module FlowExploration {
4625
4672
not fullBarrier ( node , config ) and
4626
4673
not stateBarrier ( node , state , config ) and
4627
4674
not clearsContentEx ( node , ap .getHead ( ) .getContent ( ) ) and
4675
+ (
4676
+ notExpectsContent ( node ) or
4677
+ expectsContentEx ( node , ap .getHead ( ) .getContent ( ) )
4678
+ ) and
4628
4679
if node .asNode ( ) instanceof CastingNode
4629
4680
then compatibleTypes ( node .getDataFlowType ( ) , ap .getType ( ) )
4630
4681
else any ( )
0 commit comments