@@ -1444,6 +1444,21 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1444
1444
)
1445
1445
}
1446
1446
1447
+ pragma [ nomagic]
1448
+ private predicate compatibleContainer0 ( ApHeadContent apc , DataFlowType containerType ) {
1449
+ exists ( DataFlowType containerType0 , Content c |
1450
+ PrevStage:: storeStepCand ( _, _, c , _, _, containerType0 ) and
1451
+ compatibleTypesCached ( containerType0 , containerType ) and
1452
+ apc = projectToHeadContent ( c )
1453
+ )
1454
+ }
1455
+
1456
+ bindingset [ apc, containerType]
1457
+ pragma [ inline_late]
1458
+ private predicate compatibleContainer ( ApHeadContent apc , DataFlowType containerType ) {
1459
+ compatibleContainer0 ( apc , containerType )
1460
+ }
1461
+
1447
1462
/**
1448
1463
* Holds if `node` is reachable with access path `ap` from a source.
1449
1464
*
@@ -1465,7 +1480,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1465
1480
) {
1466
1481
fwdFlow0 ( node , state , cc , summaryCtx , argT , argAp , t0 , ap , apa ) and
1467
1482
PrevStage:: revFlow ( node , state , apa ) and
1468
- filter ( node , state , t0 , ap , t )
1483
+ filter ( node , state , t0 , ap , t ) and
1484
+ (
1485
+ if castingNodeEx ( node )
1486
+ then
1487
+ ap instanceof ApNil or compatibleContainer ( getHeadContent ( ap ) , node .getDataFlowType ( ) )
1488
+ else any ( )
1489
+ )
1469
1490
}
1470
1491
1471
1492
pragma [ nomagic]
@@ -2860,15 +2881,15 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2860
2881
private module Stage3Param implements MkStage< Stage2 > :: StageParam {
2861
2882
private module PrevStage = Stage2;
2862
2883
2863
- class Typ = DataFlowType ;
2884
+ class Typ = Unit ;
2864
2885
2865
2886
class Ap = ApproxAccessPathFront ;
2866
2887
2867
2888
class ApNil = ApproxAccessPathFrontNil ;
2868
2889
2869
2890
PrevStage:: Ap getApprox ( Ap ap ) { result = ap .toBoolNonEmpty ( ) }
2870
2891
2871
- Typ getTyp ( DataFlowType t ) { result = t }
2892
+ Typ getTyp ( DataFlowType t ) { any ( ) }
2872
2893
2873
2894
bindingset [ c, t, tail]
2874
2895
Ap apCons ( Content c , Typ t , Ap tail ) { result .getAHead ( ) = c and exists ( t ) and exists ( tail ) }
@@ -2905,7 +2926,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2905
2926
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2906
2927
Typ t , LocalCc lcc
2907
2928
) {
2908
- localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _, _) and
2929
+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , _, _, _) and
2930
+ exists ( t ) and
2909
2931
exists ( lcc )
2910
2932
}
2911
2933
@@ -2928,7 +2950,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2928
2950
// the cons candidates including types are used to construct subsequent
2929
2951
// access path approximations.
2930
2952
t0 = t and
2931
- ( if castingNodeEx ( node ) then compatibleTypesFilter ( node .getDataFlowType ( ) , t0 ) else any ( ) ) and
2932
2953
(
2933
2954
notExpectsContent ( node )
2934
2955
or
@@ -2937,11 +2958,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2937
2958
}
2938
2959
2939
2960
bindingset [ typ, contentType]
2940
- predicate typecheckStore ( Typ typ , DataFlowType contentType ) {
2941
- // We need to typecheck stores here, since reverse flow through a getter
2942
- // might have a different type here compared to inside the getter.
2943
- compatibleTypesFilter ( typ , contentType )
2944
- }
2961
+ predicate typecheckStore ( Typ typ , DataFlowType contentType ) { any ( ) }
2945
2962
}
2946
2963
2947
2964
private module Stage3 = MkStage< Stage2 > :: Stage< Stage3Param > ;
0 commit comments