@@ -876,9 +876,9 @@ private module Stage1 implements StageSig {
876
876
877
877
pragma [ nomagic]
878
878
private predicate revFlowOut ( ReturnPosition pos , Configuration config ) {
879
- exists ( DataFlowCall call , NodeEx out |
879
+ exists ( NodeEx out |
880
880
revFlow ( out , _, config ) and
881
- viableReturnPosOutNodeCandFwd1 ( call , pos , out , config )
881
+ viableReturnPosOutNodeCandFwd1 ( _ , pos , out , config )
882
882
)
883
883
}
884
884
@@ -1487,14 +1487,18 @@ private module MkStage<StageSig PrevStage> {
1487
1487
PrevStage:: readStepCand ( node1 , _, _, config )
1488
1488
}
1489
1489
1490
+ bindingset [ ap, c]
1491
+ pragma [ inline_late]
1492
+ private predicate hasHeadContent ( Ap ap , Content c ) { getHeadContent ( ap ) = c }
1493
+
1490
1494
pragma [ nomagic]
1491
1495
private predicate fwdFlowRead (
1492
1496
Ap ap , Content c , NodeEx node1 , NodeEx node2 , FlowState state , Cc cc ,
1493
1497
ParamNodeOption summaryCtx , ApOption argAp , Configuration config
1494
1498
) {
1495
1499
fwdFlowRead0 ( node1 , state , cc , summaryCtx , argAp , ap , config ) and
1496
1500
PrevStage:: readStepCand ( node1 , c , node2 , config ) and
1497
- getHeadContent ( ap ) = c
1501
+ hasHeadContent ( ap , c )
1498
1502
}
1499
1503
1500
1504
pragma [ nomagic]
@@ -1731,8 +1735,8 @@ private module MkStage<StageSig PrevStage> {
1731
1735
)
1732
1736
or
1733
1737
// 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
1736
1740
flowThroughIntoCall ( call , node , p , _, ap , innerReturnAp , config )
1737
1741
)
1738
1742
or
@@ -1901,8 +1905,8 @@ private module MkStage<StageSig PrevStage> {
1901
1905
1902
1906
pragma [ nomagic]
1903
1907
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
1906
1910
parameterFlowsThroughRev ( p , ap , pos , _, config )
1907
1911
)
1908
1912
}
@@ -1923,8 +1927,8 @@ private module MkStage<StageSig PrevStage> {
1923
1927
DataFlowCall call , ArgNodeEx arg , FlowState state , ReturnCtx returnCtx , ApOption returnAp ,
1924
1928
Ap ap , Configuration config
1925
1929
) {
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
1928
1932
flowThroughIntoCall ( call , arg , p , _, ap , innerReturnAp , config )
1929
1933
)
1930
1934
}
@@ -3749,8 +3753,8 @@ private predicate paramFlowsThrough(
3749
3753
ReturnKindExt kind , FlowState state , CallContextCall cc , SummaryCtxSome sc , AccessPath ap ,
3750
3754
AccessPathApprox apa , Configuration config
3751
3755
) {
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
3754
3758
kind = ret .getKind ( ) and
3755
3759
apa = ap .getApprox ( ) and
3756
3760
parameterFlowThroughAllowed ( sc .getParamNode ( ) , kind )
@@ -4212,37 +4216,33 @@ private module FlowExploration {
4212
4216
ap = TRevPartialNil ( ) and
4213
4217
exists ( config .explorationLimit ( ) )
4214
4218
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 ( )
4226
4228
}
4227
4229
4228
4230
pragma [ nomagic]
4229
4231
private predicate partialPathNodeMk0 (
4230
4232
NodeEx node , FlowState state , CallContext cc , TSummaryCtx1 sc1 , TSummaryCtx2 sc2 ,
4231
4233
TSummaryCtx3 sc3 , PartialAccessPath ap , Configuration config
4232
4234
) {
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 ( )
4246
4246
}
4247
4247
4248
4248
/**
0 commit comments