@@ -390,10 +390,10 @@ module Impl<FullStateConfigSig Config> {
390
390
private predicate hasReadStep ( Content c ) { read ( _, c , _) }
391
391
392
392
pragma [ nomagic]
393
- private predicate storeEx ( NodeEx node1 , TypedContent tc , NodeEx node2 , DataFlowType contentType ) {
394
- store ( pragma [ only_bind_into ] ( node1 .asNode ( ) ) , tc , pragma [ only_bind_into ] ( node2 .asNode ( ) ) ,
395
- contentType ) and
396
- hasReadStep ( tc . getContent ( ) ) and
393
+ private predicate storeEx ( NodeEx node1 , TypedContent tc , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType ) {
394
+ store ( pragma [ only_bind_into ] ( node1 .asNode ( ) ) , tc , c , pragma [ only_bind_into ] ( node2 .asNode ( ) ) ,
395
+ contentType , containerType ) and
396
+ hasReadStep ( c ) and
397
397
stepFilter ( node1 , node2 )
398
398
}
399
399
@@ -478,7 +478,7 @@ module Impl<FullStateConfigSig Config> {
478
478
exists ( NodeEx mid |
479
479
useFieldFlow ( ) and
480
480
fwdFlow ( mid , cc ) and
481
- storeEx ( mid , _, node , _)
481
+ storeEx ( mid , _, _ , node , _ , _)
482
482
)
483
483
or
484
484
// read
@@ -570,12 +570,11 @@ module Impl<FullStateConfigSig Config> {
570
570
pragma [ assume_small_delta]
571
571
pragma [ nomagic]
572
572
private predicate fwdFlowConsCand ( Content c ) {
573
- exists ( NodeEx mid , NodeEx node , TypedContent tc |
573
+ exists ( NodeEx mid , NodeEx node |
574
574
not fullBarrier ( node ) and
575
575
useFieldFlow ( ) and
576
576
fwdFlow ( mid , _) and
577
- storeEx ( mid , tc , node , _) and
578
- c = tc .getContent ( )
577
+ storeEx ( mid , _, c , node , _, _)
579
578
)
580
579
}
581
580
@@ -709,11 +708,10 @@ module Impl<FullStateConfigSig Config> {
709
708
710
709
pragma [ nomagic]
711
710
private predicate revFlowStore ( Content c , NodeEx node , boolean toReturn ) {
712
- exists ( NodeEx mid , TypedContent tc |
711
+ exists ( NodeEx mid |
713
712
revFlow ( mid , toReturn ) and
714
713
fwdFlowConsCand ( c ) and
715
- storeEx ( node , tc , mid , _) and
716
- c = tc .getContent ( )
714
+ storeEx ( node , _, c , mid , _, _)
717
715
)
718
716
}
719
717
@@ -803,15 +801,12 @@ module Impl<FullStateConfigSig Config> {
803
801
804
802
pragma [ nomagic]
805
803
predicate storeStepCand (
806
- NodeEx node1 , Ap ap1 , TypedContent tc , NodeEx node2 , DataFlowType contentType
804
+ NodeEx node1 , Ap ap1 , TypedContent tc , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
807
805
) {
808
- exists ( Content c |
809
- revFlowIsReadAndStored ( c ) and
810
- revFlow ( node2 ) and
811
- storeEx ( node1 , tc , node2 , contentType ) and
812
- c = tc .getContent ( ) and
813
- exists ( ap1 )
814
- )
806
+ revFlowIsReadAndStored ( c ) and
807
+ revFlow ( node2 ) and
808
+ storeEx ( node1 , tc , c , node2 , contentType , containerType ) and
809
+ exists ( ap1 )
815
810
}
816
811
817
812
pragma [ nomagic]
@@ -1053,7 +1048,7 @@ module Impl<FullStateConfigSig Config> {
1053
1048
predicate returnMayFlowThrough ( RetNodeEx ret , Ap argAp , Ap ap , ReturnKindExt kind ) ;
1054
1049
1055
1050
predicate storeStepCand (
1056
- NodeEx node1 , Ap ap1 , TypedContent tc , NodeEx node2 , DataFlowType contentType
1051
+ NodeEx node1 , Ap ap1 , TypedContent tc , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
1057
1052
) ;
1058
1053
1059
1054
predicate readStepCand ( NodeEx n1 , Content c , NodeEx n2 ) ;
@@ -1306,7 +1301,7 @@ module Impl<FullStateConfigSig Config> {
1306
1301
) {
1307
1302
exists ( DataFlowType contentType , ApApprox apa1 |
1308
1303
fwdFlow ( node1 , state , cc , summaryCtx , argAp , ap1 , apa1 ) and
1309
- PrevStage:: storeStepCand ( node1 , apa1 , tc , node2 , contentType ) and
1304
+ PrevStage:: storeStepCand ( node1 , apa1 , tc , _ , node2 , contentType , _ ) and
1310
1305
typecheckStore ( ap1 , contentType )
1311
1306
)
1312
1307
}
@@ -1659,10 +1654,10 @@ module Impl<FullStateConfigSig Config> {
1659
1654
1660
1655
pragma [ nomagic]
1661
1656
predicate storeStepCand (
1662
- NodeEx node1 , Ap ap1 , TypedContent tc , NodeEx node2 , DataFlowType contentType
1657
+ NodeEx node1 , Ap ap1 , TypedContent tc , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
1663
1658
) {
1664
- exists ( Ap ap2 , Content c |
1665
- PrevStage:: storeStepCand ( node1 , _, tc , node2 , contentType ) and
1659
+ exists ( Ap ap2 |
1660
+ PrevStage:: storeStepCand ( node1 , _, tc , c , node2 , contentType , containerType ) and
1666
1661
revFlowStore ( ap2 , c , ap1 , node1 , _, tc , node2 , _, _) and
1667
1662
revFlowConsCand ( ap2 , c , ap1 )
1668
1663
)
@@ -1688,7 +1683,7 @@ module Impl<FullStateConfigSig Config> {
1688
1683
1689
1684
private predicate fwdConsCand ( TypedContent tc , Ap ap ) { storeStepFwd ( _, ap , tc , _, _) }
1690
1685
1691
- private predicate revConsCand ( TypedContent tc , Ap ap ) { storeStepCand ( _, ap , tc , _, _) }
1686
+ private predicate revConsCand ( TypedContent tc , Ap ap ) { storeStepCand ( _, ap , tc , _, _, _ , _ ) }
1692
1687
1693
1688
private predicate validAp ( Ap ap ) {
1694
1689
revFlow ( _, _, _, _, ap ) and ap instanceof ApNil
@@ -2003,7 +1998,7 @@ module Impl<FullStateConfigSig Config> {
2003
1998
or
2004
1999
node .asNode ( ) instanceof OutNodeExt
2005
2000
or
2006
- Stage2:: storeStepCand ( _, _, _, node , _)
2001
+ Stage2:: storeStepCand ( _, _, _, _ , node , _ , _)
2007
2002
or
2008
2003
Stage2:: readStepCand ( _, _, node )
2009
2004
or
@@ -2026,7 +2021,7 @@ module Impl<FullStateConfigSig Config> {
2026
2021
additionalJumpStep ( node , next ) or
2027
2022
flowIntoCallNodeCand2 ( _, node , next , _) or
2028
2023
flowOutOfCallNodeCand2 ( _, node , _, next , _) or
2029
- Stage2:: storeStepCand ( node , _, _, next , _) or
2024
+ Stage2:: storeStepCand ( node , _, _, _ , next , _ , _) or
2030
2025
Stage2:: readStepCand ( node , _, next )
2031
2026
)
2032
2027
or
@@ -3386,7 +3381,7 @@ module Impl<FullStateConfigSig Config> {
3386
3381
PathNodeMid mid , NodeEx node , FlowState state , AccessPath ap0 , TypedContent tc , CallContext cc
3387
3382
) {
3388
3383
ap0 = mid .getAp ( ) and
3389
- Stage5:: storeStepCand ( mid .getNodeEx ( ) , _, tc , node , _) and
3384
+ Stage5:: storeStepCand ( mid .getNodeEx ( ) , _, tc , _ , node , _ , _) and
3390
3385
state = mid .getState ( ) and
3391
3386
cc = mid .getCallContext ( )
3392
3387
}
@@ -3593,7 +3588,7 @@ module Impl<FullStateConfigSig Config> {
3593
3588
result .isHidden ( ) and
3594
3589
exists ( NodeEx n1 , NodeEx n2 | n1 = n .getNodeEx ( ) and n2 = result .getNodeEx ( ) |
3595
3590
localFlowBigStep ( n1 , _, n2 , _, _, _, _) or
3596
- storeEx ( n1 , _, n2 , _) or
3591
+ storeEx ( n1 , _, _ , n2 , _ , _) or
3597
3592
readSetEx ( n1 , _, n2 )
3598
3593
)
3599
3594
}
@@ -4271,7 +4266,7 @@ module Impl<FullStateConfigSig Config> {
4271
4266
exists ( NodeEx midNode , DataFlowType contentType |
4272
4267
midNode = mid .getNodeEx ( ) and
4273
4268
ap1 = mid .getAp ( ) and
4274
- storeEx ( midNode , tc , node , contentType ) and
4269
+ storeEx ( midNode , tc , _ , node , contentType , _ ) and
4275
4270
ap2 .getHead ( ) = tc and
4276
4271
ap2 .len ( ) = unbindInt ( ap1 .len ( ) + 1 ) and
4277
4272
compatibleTypes ( ap1 .getType ( ) , contentType )
@@ -4522,12 +4517,11 @@ module Impl<FullStateConfigSig Config> {
4522
4517
private predicate revPartialPathStoreStep (
4523
4518
PartialPathNodeRev mid , RevPartialAccessPath ap , Content c , NodeEx node
4524
4519
) {
4525
- exists ( NodeEx midNode , TypedContent tc |
4520
+ exists ( NodeEx midNode |
4526
4521
midNode = mid .getNodeEx ( ) and
4527
4522
ap = mid .getAp ( ) and
4528
- storeEx ( node , tc , midNode , _) and
4529
- ap .getHead ( ) = c and
4530
- tc .getContent ( ) = c
4523
+ storeEx ( node , _, c , midNode , _, _) and
4524
+ ap .getHead ( ) = c
4531
4525
)
4532
4526
}
4533
4527
0 commit comments