@@ -4008,7 +4008,7 @@ module Impl<FullStateConfigSig Config> {
40084008 ap = TPartialNil ( ) and
40094009 exists ( explorationLimit ( ) )
40104010 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
40124012 distSrc ( node .getEnclosingCallable ( ) ) <= explorationLimit ( )
40134013 } or
40144014 TPartialPathNodeRev (
@@ -4034,21 +4034,40 @@ module Impl<FullStateConfigSig Config> {
40344034 }
40354035
40364036 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
40404049 ) {
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
40424051 not fullBarrier ( node ) and
40434052 not stateBarrier ( node , state ) and
40444053 not clearsContentEx ( node , ap .getHead ( ) ) and
40454054 (
40464055 notExpectsContent ( node ) or
40474056 expectsContentEx ( node , ap .getHead ( ) )
40484057 ) 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
40524071 }
40534072
40544073 /**
@@ -4227,7 +4246,7 @@ module Impl<FullStateConfigSig Config> {
42274246 }
42284247 }
42294248
4230- private predicate partialPathStep (
4249+ private predicate partialPathStep0 (
42314250 PartialPathNodeFwd mid , NodeEx node , FlowState state , CallContext cc , TSummaryCtx1 sc1 ,
42324251 TSummaryCtx2 sc2 , TSummaryCtx3 sc3 , TSummaryCtx4 sc4 , DataFlowType t , PartialAccessPath ap
42334252 ) {
@@ -4353,6 +4372,11 @@ module Impl<FullStateConfigSig Config> {
43534372 DataFlowType t1 , PartialAccessPath ap1 , Content c , DataFlowType t2 , PartialAccessPath ap2
43544373 ) {
43554374 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+ )
43564380 }
43574381
43584382 pragma [ nomagic]
0 commit comments