@@ -1135,8 +1135,8 @@ module Impl<FullStateConfigSig Config> {
1135
1135
DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , boolean allowsFieldFlow
1136
1136
) ;
1137
1137
1138
- bindingset [ node, state, t , ap]
1139
- predicate filter ( NodeEx node , FlowState state , Typ t , Ap ap ) ;
1138
+ bindingset [ node, state, t0 , ap]
1139
+ predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) ;
1140
1140
1141
1141
bindingset [ typ, contentType]
1142
1142
predicate typecheckStore ( Typ typ , DataFlowType contentType ) ;
@@ -1199,17 +1199,21 @@ module Impl<FullStateConfigSig Config> {
1199
1199
NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
1200
1200
ApOption argAp , Typ t , Ap ap , ApApprox apa
1201
1201
) {
1202
- fwdFlow0 ( node , state , cc , summaryCtx , argT , argAp , t , ap , apa ) and
1203
- PrevStage:: revFlow ( node , state , apa ) and
1204
- filter ( node , state , t , ap )
1202
+ fwdFlow1 ( node , state , cc , summaryCtx , argT , argAp , _, t , ap , apa )
1205
1203
}
1206
1204
1207
- pragma [ inline]
1208
- additional predicate fwdFlow (
1205
+ private predicate fwdFlow1 (
1209
1206
NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
1210
- ApOption argAp , Typ t , Ap ap
1207
+ ApOption argAp , Typ t0 , Typ t , Ap ap , ApApprox apa
1211
1208
) {
1212
- fwdFlow ( node , state , cc , summaryCtx , argT , argAp , t , ap , _)
1209
+ fwdFlow0 ( node , state , cc , summaryCtx , argT , argAp , t0 , ap , apa ) and
1210
+ PrevStage:: revFlow ( node , state , apa ) and
1211
+ filter ( node , state , t0 , ap , t )
1212
+ }
1213
+
1214
+ pragma [ nomagic]
1215
+ private predicate typeStrengthen ( Typ t0 , Ap ap , Typ t ) {
1216
+ fwdFlow1 ( _, _, _, _, _, _, t0 , t , ap , _) and t0 != t
1213
1217
}
1214
1218
1215
1219
pragma [ assume_small_delta]
@@ -1339,6 +1343,11 @@ module Impl<FullStateConfigSig Config> {
1339
1343
private predicate fwdFlowConsCand ( Typ t2 , Ap cons , Content c , Typ t1 , Ap tail ) {
1340
1344
fwdFlowStore ( _, t1 , tail , c , t2 , _, _, _, _, _, _) and
1341
1345
cons = apCons ( c , t1 , tail )
1346
+ or
1347
+ exists ( Typ t0 |
1348
+ typeStrengthen ( t0 , cons , t2 ) and
1349
+ fwdFlowConsCand ( t0 , cons , c , t1 , tail )
1350
+ )
1342
1351
}
1343
1352
1344
1353
pragma [ nomagic]
@@ -1359,7 +1368,7 @@ module Impl<FullStateConfigSig Config> {
1359
1368
ParamNodeOption summaryCtx , TypOption argT , ApOption argAp
1360
1369
) {
1361
1370
exists ( ApHeadContent apc |
1362
- fwdFlow ( node1 , state , cc , summaryCtx , argT , argAp , t , ap ) and
1371
+ fwdFlow ( node1 , state , cc , summaryCtx , argT , argAp , t , ap , _ ) and
1363
1372
apc = getHeadContent ( ap ) and
1364
1373
readStepCand0 ( node1 , apc , c , node2 )
1365
1374
)
@@ -1520,14 +1529,14 @@ module Impl<FullStateConfigSig Config> {
1520
1529
NodeEx node , FlowState state , ReturnCtx returnCtx , ApOption returnAp , Ap ap
1521
1530
) {
1522
1531
revFlow0 ( node , state , returnCtx , returnAp , ap ) and
1523
- fwdFlow ( node , state , _, _, _, _, _, ap )
1532
+ fwdFlow ( node , state , _, _, _, _, _, ap , _ )
1524
1533
}
1525
1534
1526
1535
pragma [ nomagic]
1527
1536
private predicate revFlow0 (
1528
1537
NodeEx node , FlowState state , ReturnCtx returnCtx , ApOption returnAp , Ap ap
1529
1538
) {
1530
- fwdFlow ( node , state , _, _, _, _, _, ap ) and
1539
+ fwdFlow ( node , state , _, _, _, _, _, ap , _ ) and
1531
1540
sinkNode ( node , state ) and
1532
1541
(
1533
1542
if hasSinkCallCtx ( )
@@ -1780,13 +1789,13 @@ module Impl<FullStateConfigSig Config> {
1780
1789
boolean fwd , int nodes , int fields , int conscand , int states , int tuples
1781
1790
) {
1782
1791
fwd = true and
1783
- nodes = count ( NodeEx node | fwdFlow ( node , _, _, _, _, _, _, _) ) and
1792
+ nodes = count ( NodeEx node | fwdFlow ( node , _, _, _, _, _, _, _, _ ) ) and
1784
1793
fields = count ( Content f0 | fwdConsCand ( f0 , _, _) ) and
1785
1794
conscand = count ( Content f0 , Typ t , Ap ap | fwdConsCand ( f0 , t , ap ) ) and
1786
- states = count ( FlowState state | fwdFlow ( _, state , _, _, _, _, _, _) ) and
1795
+ states = count ( FlowState state | fwdFlow ( _, state , _, _, _, _, _, _, _ ) ) and
1787
1796
tuples =
1788
1797
count ( NodeEx n , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
1789
- ApOption argAp , Typ t , Ap ap | fwdFlow ( n , state , cc , summaryCtx , argT , argAp , t , ap ) )
1798
+ ApOption argAp , Typ t , Ap ap | fwdFlow ( n , state , cc , summaryCtx , argT , argAp , t , ap , _ ) )
1790
1799
or
1791
1800
fwd = false and
1792
1801
nodes = count ( NodeEx node | revFlow ( node , _, _, _, _) ) and
@@ -1963,10 +1972,10 @@ module Impl<FullStateConfigSig Config> {
1963
1972
)
1964
1973
}
1965
1974
1966
- bindingset [ node, state, t , ap]
1967
- predicate filter ( NodeEx node , FlowState state , Typ t , Ap ap ) {
1975
+ bindingset [ node, state, t0 , ap]
1976
+ predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
1968
1977
PrevStage:: revFlowState ( state ) and
1969
- exists ( t ) and
1978
+ t0 = t and
1970
1979
exists ( ap ) and
1971
1980
not stateBarrier ( node , state ) and
1972
1981
(
@@ -2197,8 +2206,8 @@ module Impl<FullStateConfigSig Config> {
2197
2206
import BooleanCallContext
2198
2207
2199
2208
predicate localStep (
2200
- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2201
- DataFlowType t , LocalCc lcc
2209
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue , Typ t ,
2210
+ LocalCc lcc
2202
2211
) {
2203
2212
localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _) and
2204
2213
exists ( lcc )
@@ -2218,10 +2227,16 @@ module Impl<FullStateConfigSig Config> {
2218
2227
)
2219
2228
}
2220
2229
2221
- bindingset [ node, state, t , ap]
2222
- predicate filter ( NodeEx node , FlowState state , Typ t , Ap ap ) {
2230
+ bindingset [ node, state, t0 , ap]
2231
+ predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
2223
2232
exists ( state ) and
2224
- ( if castingNodeEx ( node ) then compatibleTypes ( node .getDataFlowType ( ) , t ) else any ( ) ) and
2233
+ // We can get away with not using type strengthening here, since we aren't
2234
+ // going to use the tracked types in the construction of Stage 4 access
2235
+ // paths. For Stage 4 and onwards, the tracked types must be consistent as
2236
+ // the cons candidates including types are used to construct subsequent
2237
+ // access path approximations.
2238
+ t0 = t and
2239
+ ( if castingNodeEx ( node ) then compatibleTypes ( node .getDataFlowType ( ) , t0 ) else any ( ) ) and
2225
2240
(
2226
2241
notExpectsContent ( node )
2227
2242
or
@@ -2241,6 +2256,16 @@ module Impl<FullStateConfigSig Config> {
2241
2256
import MkStage< Stage2 > :: Stage< Stage3Param >
2242
2257
}
2243
2258
2259
+ bindingset [ node, t0]
2260
+ private predicate strengthenType ( NodeEx node , DataFlowType t0 , DataFlowType t ) {
2261
+ if castingNodeEx ( node )
2262
+ then
2263
+ exists ( DataFlowType nt | nt = node .getDataFlowType ( ) |
2264
+ if typeStrongerThan ( nt , t0 ) then t = nt else ( compatibleTypes ( nt , t0 ) and t = t0 )
2265
+ )
2266
+ else t = t0
2267
+ }
2268
+
2244
2269
private module Stage4Param implements MkStage< Stage3 > :: StageParam {
2245
2270
private module PrevStage = Stage3;
2246
2271
@@ -2274,8 +2299,8 @@ module Impl<FullStateConfigSig Config> {
2274
2299
2275
2300
pragma [ nomagic]
2276
2301
predicate localStep (
2277
- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2278
- DataFlowType t , LocalCc lcc
2302
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue , Typ t ,
2303
+ LocalCc lcc
2279
2304
) {
2280
2305
localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _) and
2281
2306
PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
@@ -2333,11 +2358,11 @@ module Impl<FullStateConfigSig Config> {
2333
2358
)
2334
2359
}
2335
2360
2336
- bindingset [ node, state, t , ap]
2337
- predicate filter ( NodeEx node , FlowState state , Typ t , Ap ap ) {
2361
+ bindingset [ node, state, t0 , ap]
2362
+ predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
2338
2363
exists ( state ) and
2339
2364
not clear ( node , ap ) and
2340
- ( if castingNodeEx ( node ) then compatibleTypes ( node . getDataFlowType ( ) , t ) else any ( ) ) and
2365
+ strengthenType ( node , t0 , t ) and
2341
2366
(
2342
2367
notExpectsContent ( node )
2343
2368
or
@@ -2365,7 +2390,7 @@ module Impl<FullStateConfigSig Config> {
2365
2390
exists ( AccessPathFront apf |
2366
2391
Stage4:: revFlow ( node , state , TReturnCtxMaybeFlowThrough ( _) , _, apf ) and
2367
2392
Stage4:: fwdFlow ( node , state , any ( Stage4:: CcCall ccc ) , _, _, TAccessPathFrontSome ( argApf ) , _,
2368
- apf )
2393
+ apf , _ )
2369
2394
)
2370
2395
}
2371
2396
@@ -2579,8 +2604,8 @@ module Impl<FullStateConfigSig Config> {
2579
2604
import LocalCallContext
2580
2605
2581
2606
predicate localStep (
2582
- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2583
- DataFlowType t , LocalCc lcc
2607
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue , Typ t ,
2608
+ LocalCc lcc
2584
2609
) {
2585
2610
localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc ) and
2586
2611
PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
@@ -2609,9 +2634,9 @@ module Impl<FullStateConfigSig Config> {
2609
2634
)
2610
2635
}
2611
2636
2612
- bindingset [ node, state, t , ap]
2613
- predicate filter ( NodeEx node , FlowState state , Typ t , Ap ap ) {
2614
- ( if castingNodeEx ( node ) then compatibleTypes ( node . getDataFlowType ( ) , t ) else any ( ) ) and
2637
+ bindingset [ node, state, t0 , ap]
2638
+ predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
2639
+ strengthenType ( node , t0 , t ) and
2615
2640
exists ( state ) and
2616
2641
exists ( ap )
2617
2642
}
@@ -2632,7 +2657,7 @@ module Impl<FullStateConfigSig Config> {
2632
2657
Stage5:: parameterMayFlowThrough ( p , _) and
2633
2658
Stage5:: revFlow ( n , state , TReturnCtxMaybeFlowThrough ( _) , _, apa0 ) and
2634
2659
Stage5:: fwdFlow ( n , state , any ( CallContextCall ccc ) , TParamNodeSome ( p .asNode ( ) ) , _,
2635
- TAccessPathApproxSome ( apa ) , _, apa0 )
2660
+ TAccessPathApproxSome ( apa ) , _, apa0 , _ )
2636
2661
)
2637
2662
}
2638
2663
@@ -2649,7 +2674,7 @@ module Impl<FullStateConfigSig Config> {
2649
2674
TSummaryCtxSome ( ParamNodeEx p , FlowState state , DataFlowType t , AccessPath ap ) {
2650
2675
exists ( AccessPathApprox apa | ap .getApprox ( ) = apa |
2651
2676
Stage5:: parameterMayFlowThrough ( p , apa ) and
2652
- Stage5:: fwdFlow ( p , state , _, _, _ , _, t , apa ) and
2677
+ Stage5:: fwdFlow ( p , state , _, _, Option < DataFlowType > :: some ( t ) , _, _ , apa , _ ) and
2653
2678
Stage5:: revFlow ( p , state , _)
2654
2679
)
2655
2680
}
@@ -2820,9 +2845,7 @@ module Impl<FullStateConfigSig Config> {
2820
2845
ap = TAccessPathNil ( )
2821
2846
or
2822
2847
// ... or a step from an existing PathNode to another node.
2823
- pathStep ( _, node , state , cc , sc , t , ap ) and
2824
- Stage5:: revFlow ( node , state , ap .getApprox ( ) ) and
2825
- ( if castingNodeEx ( node ) then compatibleTypes ( node .getDataFlowType ( ) , t ) else any ( ) )
2848
+ pathStep ( _, node , state , cc , sc , t , ap )
2826
2849
} or
2827
2850
TPathNodeSink ( NodeEx node , FlowState state ) {
2828
2851
exists ( PathNodeMid sink |
@@ -3340,13 +3363,24 @@ module Impl<FullStateConfigSig Config> {
3340
3363
ap = mid .getAp ( )
3341
3364
}
3342
3365
3366
+ private predicate pathStep (
3367
+ PathNodeMid mid , NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , DataFlowType t ,
3368
+ AccessPath ap
3369
+ ) {
3370
+ exists ( DataFlowType t0 |
3371
+ pathStep0 ( mid , node , state , cc , sc , t0 , ap ) and
3372
+ Stage5:: revFlow ( node , state , ap .getApprox ( ) ) and
3373
+ strengthenType ( node , t0 , t )
3374
+ )
3375
+ }
3376
+
3343
3377
/**
3344
3378
* Holds if data may flow from `mid` to `node`. The last step in or out of
3345
3379
* a callable is recorded by `cc`.
3346
3380
*/
3347
3381
pragma [ assume_small_delta]
3348
3382
pragma [ nomagic]
3349
- private predicate pathStep (
3383
+ private predicate pathStep0 (
3350
3384
PathNodeMid mid , NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , DataFlowType t ,
3351
3385
AccessPath ap
3352
3386
) {
@@ -3964,7 +3998,7 @@ module Impl<FullStateConfigSig Config> {
3964
3998
ap = TPartialNil ( ) and
3965
3999
exists ( explorationLimit ( ) )
3966
4000
or
3967
- partialPathNodeMk0 ( node , state , cc , sc1 , sc2 , sc3 , sc4 , t , ap ) and
4001
+ partialPathStep ( _ , node , state , cc , sc1 , sc2 , sc3 , sc4 , t , ap ) and
3968
4002
distSrc ( node .getEnclosingCallable ( ) ) <= explorationLimit ( )
3969
4003
} or
3970
4004
TPartialPathNodeRev (
@@ -3990,21 +4024,35 @@ module Impl<FullStateConfigSig Config> {
3990
4024
}
3991
4025
3992
4026
pragma [ nomagic]
3993
- private predicate partialPathNodeMk0 (
3994
- NodeEx node , FlowState state , CallContext cc , TSummaryCtx1 sc1 , TSummaryCtx2 sc2 ,
3995
- TSummaryCtx3 sc3 , TSummaryCtx4 sc4 , DataFlowType t , PartialAccessPath ap
4027
+ private predicate partialPathStep (
4028
+ PartialPathNodeFwd mid , NodeEx node , FlowState state , CallContext cc , TSummaryCtx1 sc1 ,
4029
+ TSummaryCtx2 sc2 , TSummaryCtx3 sc3 , TSummaryCtx4 sc4 , DataFlowType t , PartialAccessPath ap
3996
4030
) {
3997
- partialPathStep ( _, node , state , cc , sc1 , sc2 , sc3 , sc4 , t , ap ) and
4031
+ partialPathStep1 ( mid , node , state , cc , sc1 , sc2 , sc3 , sc4 , _, t , ap )
4032
+ }
4033
+
4034
+ pragma [ nomagic]
4035
+ private predicate partialPathStep1 (
4036
+ PartialPathNodeFwd mid , NodeEx node , FlowState state , CallContext cc , TSummaryCtx1 sc1 ,
4037
+ TSummaryCtx2 sc2 , TSummaryCtx3 sc3 , TSummaryCtx4 sc4 , DataFlowType t0 , DataFlowType t ,
4038
+ PartialAccessPath ap
4039
+ ) {
4040
+ partialPathStep0 ( mid , node , state , cc , sc1 , sc2 , sc3 , sc4 , t0 , ap ) and
3998
4041
not fullBarrier ( node ) and
3999
4042
not stateBarrier ( node , state ) and
4000
4043
not clearsContentEx ( node , ap .getHead ( ) ) and
4001
4044
(
4002
4045
notExpectsContent ( node ) or
4003
4046
expectsContentEx ( node , ap .getHead ( ) )
4004
4047
) and
4005
- if node .asNode ( ) instanceof CastingNode
4006
- then compatibleTypes ( node .getDataFlowType ( ) , t )
4007
- else any ( )
4048
+ strengthenType ( node , t0 , t )
4049
+ }
4050
+
4051
+ pragma [ nomagic]
4052
+ private predicate partialPathTypeStrengthen (
4053
+ DataFlowType t0 , PartialAccessPath ap , DataFlowType t
4054
+ ) {
4055
+ partialPathStep1 ( _, _, _, _, _, _, _, _, t0 , t , ap ) and t0 != t
4008
4056
}
4009
4057
4010
4058
/**
@@ -4183,7 +4231,8 @@ module Impl<FullStateConfigSig Config> {
4183
4231
}
4184
4232
}
4185
4233
4186
- private predicate partialPathStep (
4234
+ pragma [ nomagic]
4235
+ private predicate partialPathStep0 (
4187
4236
PartialPathNodeFwd mid , NodeEx node , FlowState state , CallContext cc , TSummaryCtx1 sc1 ,
4188
4237
TSummaryCtx2 sc2 , TSummaryCtx3 sc3 , TSummaryCtx4 sc4 , DataFlowType t , PartialAccessPath ap
4189
4238
) {
@@ -4309,6 +4358,11 @@ module Impl<FullStateConfigSig Config> {
4309
4358
DataFlowType t1 , PartialAccessPath ap1 , Content c , DataFlowType t2 , PartialAccessPath ap2
4310
4359
) {
4311
4360
partialPathStoreStep ( _, t1 , ap1 , c , _, t2 , ap2 )
4361
+ or
4362
+ exists ( DataFlowType t0 |
4363
+ partialPathTypeStrengthen ( t0 , ap2 , t2 ) and
4364
+ apConsFwd ( t1 , ap1 , c , t0 , ap2 )
4365
+ )
4312
4366
}
4313
4367
4314
4368
pragma [ nomagic]
0 commit comments