@@ -876,9 +876,9 @@ private module Stage1 implements StageSig {
876876
877877 pragma [ nomagic]
878878 private predicate revFlowOut ( ReturnPosition pos , Configuration config ) {
879- exists ( DataFlowCall call , NodeEx out |
879+ exists ( NodeEx out |
880880 revFlow ( out , _, config ) and
881- viableReturnPosOutNodeCandFwd1 ( call , pos , out , config )
881+ viableReturnPosOutNodeCandFwd1 ( _ , pos , out , config )
882882 )
883883 }
884884
@@ -1487,14 +1487,18 @@ private module MkStage<StageSig PrevStage> {
14871487 PrevStage:: readStepCand ( node1 , _, _, config )
14881488 }
14891489
1490+ bindingset [ ap, c]
1491+ pragma [ inline_late]
1492+ private predicate hasHeadContent ( Ap ap , Content c ) { getHeadContent ( ap ) = c }
1493+
14901494 pragma [ nomagic]
14911495 private predicate fwdFlowRead (
14921496 Ap ap , Content c , NodeEx node1 , NodeEx node2 , FlowState state , Cc cc ,
14931497 ParamNodeOption summaryCtx , ApOption argAp , Configuration config
14941498 ) {
14951499 fwdFlowRead0 ( node1 , state , cc , summaryCtx , argAp , ap , config ) and
14961500 PrevStage:: readStepCand ( node1 , c , node2 , config ) and
1497- getHeadContent ( ap ) = c
1501+ hasHeadContent ( ap , c )
14981502 }
14991503
15001504 pragma [ nomagic]
@@ -1731,8 +1735,8 @@ private module MkStage<StageSig PrevStage> {
17311735 )
17321736 or
17331737 // flow through a callable
1734- exists ( DataFlowCall call , ParamNodeEx p , ReturnPosition pos , Ap innerReturnAp |
1735- revFlowThrough ( call , returnCtx , p , state , pos , returnAp , ap , innerReturnAp , config ) and
1738+ exists ( DataFlowCall call , ParamNodeEx p , Ap innerReturnAp |
1739+ revFlowThrough ( call , returnCtx , p , state , _ , returnAp , ap , innerReturnAp , config ) and
17361740 flowThroughIntoCall ( call , node , p , _, ap , innerReturnAp , config )
17371741 )
17381742 or
@@ -1901,8 +1905,8 @@ private module MkStage<StageSig PrevStage> {
19011905
19021906 pragma [ nomagic]
19031907 predicate parameterMayFlowThrough ( ParamNodeEx p , Ap ap , Configuration config ) {
1904- exists ( RetNodeEx ret , ReturnPosition pos |
1905- returnFlowsThrough ( ret , pos , _, _, p , ap , _, config ) and
1908+ exists ( ReturnPosition pos |
1909+ returnFlowsThrough ( _ , pos , _, _, p , ap , _, config ) and
19061910 parameterFlowsThroughRev ( p , ap , pos , _, config )
19071911 )
19081912 }
@@ -1923,8 +1927,8 @@ private module MkStage<StageSig PrevStage> {
19231927 DataFlowCall call , ArgNodeEx arg , FlowState state , ReturnCtx returnCtx , ApOption returnAp ,
19241928 Ap ap , Configuration config
19251929 ) {
1926- exists ( ParamNodeEx p , ReturnPosition pos , Ap innerReturnAp |
1927- revFlowThrough ( call , returnCtx , p , state , pos , returnAp , ap , innerReturnAp , config ) and
1930+ exists ( ParamNodeEx p , Ap innerReturnAp |
1931+ revFlowThrough ( call , returnCtx , p , state , _ , returnAp , ap , innerReturnAp , config ) and
19281932 flowThroughIntoCall ( call , arg , p , _, ap , innerReturnAp , config )
19291933 )
19301934 }
@@ -3749,8 +3753,8 @@ private predicate paramFlowsThrough(
37493753 ReturnKindExt kind , FlowState state , CallContextCall cc , SummaryCtxSome sc , AccessPath ap ,
37503754 AccessPathApprox apa , Configuration config
37513755) {
3752- exists ( PathNodeMid mid , RetNodeEx ret |
3753- pathNode ( mid , ret , state , cc , sc , ap , config , _) and
3756+ exists ( RetNodeEx ret |
3757+ pathNode ( _ , ret , state , cc , sc , ap , config , _) and
37543758 kind = ret .getKind ( ) and
37553759 apa = ap .getApprox ( ) and
37563760 parameterFlowThroughAllowed ( sc .getParamNode ( ) , kind )
@@ -4212,37 +4216,33 @@ private module FlowExploration {
42124216 ap = TRevPartialNil ( ) and
42134217 exists ( config .explorationLimit ( ) )
42144218 or
4215- exists ( PartialPathNodeRev mid |
4216- revPartialPathStep ( mid , node , state , sc1 , sc2 , sc3 , ap , config ) and
4217- not clearsContentEx ( node , ap .getHead ( ) ) and
4218- (
4219- notExpectsContent ( node ) or
4220- expectsContentEx ( node , ap .getHead ( ) )
4221- ) and
4222- not fullBarrier ( node , config ) and
4223- not stateBarrier ( node , state , config ) and
4224- distSink ( node .getEnclosingCallable ( ) , config ) <= config .explorationLimit ( )
4225- )
4219+ revPartialPathStep ( _, node , state , sc1 , sc2 , sc3 , ap , config ) and
4220+ not clearsContentEx ( node , ap .getHead ( ) ) and
4221+ (
4222+ notExpectsContent ( node ) or
4223+ expectsContentEx ( node , ap .getHead ( ) )
4224+ ) and
4225+ not fullBarrier ( node , config ) and
4226+ not stateBarrier ( node , state , config ) and
4227+ distSink ( node .getEnclosingCallable ( ) , config ) <= config .explorationLimit ( )
42264228 }
42274229
42284230 pragma [ nomagic]
42294231 private predicate partialPathNodeMk0 (
42304232 NodeEx node , FlowState state , CallContext cc , TSummaryCtx1 sc1 , TSummaryCtx2 sc2 ,
42314233 TSummaryCtx3 sc3 , PartialAccessPath ap , Configuration config
42324234 ) {
4233- exists ( PartialPathNodeFwd mid |
4234- partialPathStep ( mid , node , state , cc , sc1 , sc2 , sc3 , ap , config ) and
4235- not fullBarrier ( node , config ) and
4236- not stateBarrier ( node , state , config ) and
4237- not clearsContentEx ( node , ap .getHead ( ) .getContent ( ) ) and
4238- (
4239- notExpectsContent ( node ) or
4240- expectsContentEx ( node , ap .getHead ( ) .getContent ( ) )
4241- ) and
4242- if node .asNode ( ) instanceof CastingNode
4243- then compatibleTypes ( node .getDataFlowType ( ) , ap .getType ( ) )
4244- else any ( )
4245- )
4235+ partialPathStep ( _, node , state , cc , sc1 , sc2 , sc3 , ap , config ) and
4236+ not fullBarrier ( node , config ) and
4237+ not stateBarrier ( node , state , config ) and
4238+ not clearsContentEx ( node , ap .getHead ( ) .getContent ( ) ) and
4239+ (
4240+ notExpectsContent ( node ) or
4241+ expectsContentEx ( node , ap .getHead ( ) .getContent ( ) )
4242+ ) and
4243+ if node .asNode ( ) instanceof CastingNode
4244+ then compatibleTypes ( node .getDataFlowType ( ) , ap .getType ( ) )
4245+ else any ( )
42464246 }
42474247
42484248 /**
0 commit comments