@@ -4008,7 +4008,7 @@ module Impl<FullStateConfigSig Config> {
4008
4008
ap = TPartialNil ( ) and
4009
4009
exists ( explorationLimit ( ) )
4010
4010
or
4011
- partialPathNodeMk0 ( node , state , cc , sc1 , sc2 , sc3 , sc4 , t , ap ) and
4011
+ partialPathStep ( _ , node , state , cc , sc1 , sc2 , sc3 , sc4 , t , ap ) and
4012
4012
distSrc ( node .getEnclosingCallable ( ) ) <= explorationLimit ( )
4013
4013
} or
4014
4014
TPartialPathNodeRev (
@@ -4034,21 +4034,40 @@ module Impl<FullStateConfigSig Config> {
4034
4034
}
4035
4035
4036
4036
pragma [ nomagic]
4037
- private predicate partialPathNodeMk0 (
4038
- NodeEx node , FlowState state , CallContext cc , TSummaryCtx1 sc1 , TSummaryCtx2 sc2 ,
4039
- TSummaryCtx3 sc3 , TSummaryCtx4 sc4 , DataFlowType t , PartialAccessPath ap
4037
+ private predicate partialPathStep (
4038
+ PartialPathNodeFwd mid , NodeEx node , FlowState state , CallContext cc , TSummaryCtx1 sc1 ,
4039
+ TSummaryCtx2 sc2 , TSummaryCtx3 sc3 , TSummaryCtx4 sc4 , DataFlowType t , PartialAccessPath ap
4040
+ ) {
4041
+ partialPathStep1 ( mid , node , state , cc , sc1 , sc2 , sc3 , sc4 , _, t , ap )
4042
+ }
4043
+
4044
+ pragma [ nomagic]
4045
+ private predicate partialPathStep1 (
4046
+ PartialPathNodeFwd mid , NodeEx node , FlowState state , CallContext cc , TSummaryCtx1 sc1 ,
4047
+ TSummaryCtx2 sc2 , TSummaryCtx3 sc3 , TSummaryCtx4 sc4 , DataFlowType t0 , DataFlowType t ,
4048
+ PartialAccessPath ap
4040
4049
) {
4041
- partialPathStep ( _ , node , state , cc , sc1 , sc2 , sc3 , sc4 , t , ap ) and
4050
+ partialPathStep0 ( mid , node , state , cc , sc1 , sc2 , sc3 , sc4 , t0 , ap ) and
4042
4051
not fullBarrier ( node ) and
4043
4052
not stateBarrier ( node , state ) and
4044
4053
not clearsContentEx ( node , ap .getHead ( ) ) and
4045
4054
(
4046
4055
notExpectsContent ( node ) or
4047
4056
expectsContentEx ( node , ap .getHead ( ) )
4048
4057
) and
4049
- if node .asNode ( ) instanceof CastingNode
4050
- then compatibleTypes ( node .getDataFlowType ( ) , t )
4051
- else any ( )
4058
+ if castingNodeEx ( node )
4059
+ then
4060
+ exists ( DataFlowType nt | nt = node .getDataFlowType ( ) |
4061
+ if typeStrongerThan ( nt , t0 ) then t = nt else ( compatibleTypes ( nt , t0 ) and t = t0 )
4062
+ )
4063
+ else t = t0
4064
+ }
4065
+
4066
+ pragma [ nomagic]
4067
+ private predicate partialPathTypeStrengthen (
4068
+ DataFlowType t0 , PartialAccessPath ap , DataFlowType t
4069
+ ) {
4070
+ partialPathStep1 ( _, _, _, _, _, _, _, _, t0 , t , ap ) and t0 != t
4052
4071
}
4053
4072
4054
4073
/**
@@ -4227,7 +4246,7 @@ module Impl<FullStateConfigSig Config> {
4227
4246
}
4228
4247
}
4229
4248
4230
- private predicate partialPathStep (
4249
+ private predicate partialPathStep0 (
4231
4250
PartialPathNodeFwd mid , NodeEx node , FlowState state , CallContext cc , TSummaryCtx1 sc1 ,
4232
4251
TSummaryCtx2 sc2 , TSummaryCtx3 sc3 , TSummaryCtx4 sc4 , DataFlowType t , PartialAccessPath ap
4233
4252
) {
@@ -4353,6 +4372,11 @@ module Impl<FullStateConfigSig Config> {
4353
4372
DataFlowType t1 , PartialAccessPath ap1 , Content c , DataFlowType t2 , PartialAccessPath ap2
4354
4373
) {
4355
4374
partialPathStoreStep ( _, t1 , ap1 , c , _, t2 , ap2 )
4375
+ or
4376
+ exists ( DataFlowType t0 |
4377
+ partialPathTypeStrengthen ( t0 , ap2 , t2 ) and
4378
+ apConsFwd ( t1 , ap1 , c , t0 , ap2 )
4379
+ )
4356
4380
}
4357
4381
4358
4382
pragma [ nomagic]
0 commit comments