@@ -502,7 +502,7 @@ pragma[inline]
502502private predicate read ( NodeEx node1 , Content c , NodeEx node2 , Configuration config ) {
503503 exists ( ContentSet cs |
504504 readSet ( node1 , cs , node2 , config ) and
505- c = cs .getAReadContent ( )
505+ pragma [ only_bind_out ] ( c ) = pragma [ only_bind_into ] ( cs ) .getAReadContent ( )
506506 )
507507}
508508
@@ -511,10 +511,22 @@ pragma[inline]
511511private predicate clearsContentEx ( NodeEx n , Content c ) {
512512 exists ( ContentSet cs |
513513 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 ( )
515524 )
516525}
517526
527+ pragma [ nomagic]
528+ private predicate notExpectsContent ( NodeEx n ) { not expectsContentCached ( n .asNode ( ) , _) }
529+
518530pragma [ nomagic]
519531private predicate store (
520532 NodeEx node1 , TypedContent tc , NodeEx node2 , DataFlowType contentType , Configuration config
@@ -793,7 +805,7 @@ private module Stage1 {
793805 * by `revFlow`.
794806 */
795807 pragma [ nomagic]
796- private predicate revFlowIsReadAndStored ( Content c , Configuration conf ) {
808+ predicate revFlowIsReadAndStored ( Content c , Configuration conf ) {
797809 revFlowConsCand ( c , conf ) and
798810 revFlowStore ( c , _, _, conf )
799811 }
@@ -891,7 +903,7 @@ private module Stage1 {
891903
892904 pragma [ nomagic]
893905 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
895907 read ( n1 , c , n2 , pragma [ only_bind_into ] ( config ) ) and
896908 revFlow ( n2 , pragma [ only_bind_into ] ( config ) )
897909 }
@@ -1181,11 +1193,26 @@ private module Stage2 {
11811193
11821194 private predicate flowIntoCall = flowIntoCallNodeCand1 / 5 ;
11831195
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+
11841205 bindingset [ node, state, ap, config]
11851206 private predicate filter ( NodeEx node , FlowState state , Ap ap , Configuration config ) {
11861207 PrevStage:: revFlowState ( state , pragma [ only_bind_into ] ( config ) ) and
11871208 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+ )
11891216 }
11901217
11911218 bindingset [ ap, contentType]
@@ -1740,7 +1767,8 @@ private module LocalFlowBigStep {
17401767 private class FlowCheckNode extends NodeEx {
17411768 FlowCheckNode ( ) {
17421769 castNode ( this .asNode ( ) ) or
1743- clearsContentCached ( this .asNode ( ) , _)
1770+ clearsContentCached ( this .asNode ( ) , _) or
1771+ expectsContentCached ( this .asNode ( ) , _)
17441772 }
17451773 }
17461774
@@ -1979,6 +2007,16 @@ private module Stage3 {
19792007 clearContent ( node , ap .getHead ( ) .getContent ( ) , config )
19802008 }
19812009
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+
19822020 pragma [ nomagic]
19832021 private predicate castingNodeEx ( NodeEx node ) { node .asNode ( ) instanceof CastingNode }
19842022
@@ -1987,7 +2025,12 @@ private module Stage3 {
19872025 exists ( state ) and
19882026 exists ( config ) and
19892027 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+ )
19912034 }
19922035
19932036 bindingset [ ap, contentType]
@@ -4609,6 +4652,10 @@ private module FlowExploration {
46094652 exists ( PartialPathNodeRev mid |
46104653 revPartialPathStep ( mid , node , state , sc1 , sc2 , sc3 , ap , config ) and
46114654 not clearsContentEx ( node , ap .getHead ( ) ) and
4655+ (
4656+ notExpectsContent ( node ) or
4657+ expectsContentEx ( node , ap .getHead ( ) )
4658+ ) and
46124659 not fullBarrier ( node , config ) and
46134660 not stateBarrier ( node , state , config ) and
46144661 distSink ( node .getEnclosingCallable ( ) , config ) <= config .explorationLimit ( )
@@ -4625,6 +4672,10 @@ private module FlowExploration {
46254672 not fullBarrier ( node , config ) and
46264673 not stateBarrier ( node , state , config ) and
46274674 not clearsContentEx ( node , ap .getHead ( ) .getContent ( ) ) and
4675+ (
4676+ notExpectsContent ( node ) or
4677+ expectsContentEx ( node , ap .getHead ( ) .getContent ( ) )
4678+ ) and
46284679 if node .asNode ( ) instanceof CastingNode
46294680 then compatibleTypes ( node .getDataFlowType ( ) , ap .getType ( ) )
46304681 else any ( )
0 commit comments