@@ -516,25 +516,12 @@ private predicate clearsContentEx(NodeEx n, Content c) {
516
516
}
517
517
518
518
pragma [ nomagic]
519
- private predicate storeSet (
520
- NodeEx node1 , ContentSet c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType ,
521
- Configuration config
522
- ) {
523
- storeSet ( node1 .asNode ( ) , c , node2 .asNode ( ) , contentType , containerType ) and
524
- stepFilter ( node1 , node2 , config ) and
525
- read ( _, c .getAStoreContent ( ) , _, config )
526
- }
527
-
528
- // inline to reduce fan-out via `getAStoreContent`
529
- pragma [ inline]
530
519
private predicate store (
531
- NodeEx node1 , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType ,
532
- Configuration config
520
+ NodeEx node1 , TypedContent tc , NodeEx node2 , DataFlowType contentType , Configuration config
533
521
) {
534
- exists ( ContentSet cs |
535
- storeSet ( node1 , cs , node2 , contentType , containerType , config ) and
536
- c = cs .getAStoreContent ( )
537
- )
522
+ store ( node1 .asNode ( ) , tc , node2 .asNode ( ) , contentType ) and
523
+ read ( _, tc .getContent ( ) , _, config ) and
524
+ stepFilter ( node1 , node2 , config )
538
525
}
539
526
540
527
pragma [ nomagic]
@@ -602,7 +589,7 @@ private module Stage1 {
602
589
exists ( NodeEx mid |
603
590
useFieldFlow ( config ) and
604
591
fwdFlow ( mid , cc , config ) and
605
- storeSet ( mid , _, node , _ , _, config )
592
+ store ( mid , _, node , _, config )
606
593
)
607
594
or
608
595
// read
@@ -644,11 +631,12 @@ private module Stage1 {
644
631
*/
645
632
pragma [ nomagic]
646
633
private predicate fwdFlowConsCand ( Content c , Configuration config ) {
647
- exists ( NodeEx mid , NodeEx node |
634
+ exists ( NodeEx mid , NodeEx node , TypedContent tc |
648
635
not fullBarrier ( node , config ) and
649
636
useFieldFlow ( config ) and
650
637
fwdFlow ( mid , _, config ) and
651
- store ( mid , c , node , _, _, config )
638
+ store ( mid , tc , node , _, config ) and
639
+ c = tc .getContent ( )
652
640
)
653
641
}
654
642
@@ -748,9 +736,9 @@ private module Stage1 {
748
736
)
749
737
or
750
738
// store
751
- exists ( ContentSet c |
752
- revFlowStoreSet ( c , node , toReturn , config ) and
753
- revFlowConsCandSet ( c , config )
739
+ exists ( Content c |
740
+ revFlowStore ( c , node , toReturn , config ) and
741
+ revFlowConsCand ( c , config )
754
742
)
755
743
or
756
744
// read
@@ -791,18 +779,12 @@ private module Stage1 {
791
779
}
792
780
793
781
pragma [ nomagic]
794
- private predicate revFlowConsCandSet ( ContentSet c , Configuration config ) {
795
- revFlowConsCand ( c .getAStoreContent ( ) , config )
796
- }
797
-
798
- pragma [ nomagic]
799
- private predicate revFlowStoreSet (
800
- ContentSet c , NodeEx node , boolean toReturn , Configuration config
801
- ) {
802
- exists ( NodeEx mid |
782
+ private predicate revFlowStore ( Content c , NodeEx node , boolean toReturn , Configuration config ) {
783
+ exists ( NodeEx mid , TypedContent tc |
803
784
revFlow ( mid , toReturn , pragma [ only_bind_into ] ( config ) ) and
804
- fwdFlowConsCandSet ( c , _, pragma [ only_bind_into ] ( config ) ) and
805
- storeSet ( node , c , mid , _, _, config )
785
+ fwdFlowConsCandSet ( _, c , pragma [ only_bind_into ] ( config ) ) and
786
+ store ( node , tc , mid , _, config ) and
787
+ c = tc .getContent ( )
806
788
)
807
789
}
808
790
@@ -812,11 +794,8 @@ private module Stage1 {
812
794
*/
813
795
pragma [ nomagic]
814
796
private predicate revFlowIsReadAndStored ( Content c , Configuration conf ) {
815
- revFlowConsCand ( c , pragma [ only_bind_into ] ( conf ) ) and
816
- exists ( ContentSet cs |
817
- revFlowStoreSet ( cs , _, _, pragma [ only_bind_into ] ( conf ) ) and
818
- c = cs .getAStoreContent ( )
819
- )
797
+ revFlowConsCand ( c , conf ) and
798
+ revFlowStore ( c , _, _, conf )
820
799
}
821
800
822
801
pragma [ nomagic]
@@ -901,11 +880,11 @@ private module Stage1 {
901
880
NodeEx node1 , Ap ap1 , TypedContent tc , NodeEx node2 , DataFlowType contentType ,
902
881
Configuration config
903
882
) {
904
- exists ( Content c , DataFlowType containerType |
905
- revFlowIsReadAndStored ( pragma [ only_bind_into ] ( c ) , pragma [ only_bind_into ] ( config ) ) and
906
- store ( node1 , c , node2 , contentType , containerType , config ) and
883
+ exists ( Content c |
884
+ revFlowIsReadAndStored ( c , pragma [ only_bind_into ] ( config ) ) and
907
885
revFlow ( node2 , pragma [ only_bind_into ] ( config ) ) and
908
- tc = MkTypedContent ( c , containerType ) and
886
+ store ( node1 , tc , node2 , contentType , config ) and
887
+ c = tc .getContent ( ) and
909
888
exists ( ap1 )
910
889
)
911
890
}
@@ -1978,7 +1957,7 @@ private module Stage3 {
1978
1957
private predicate flowIntoCall = flowIntoCallNodeCand2 / 5 ;
1979
1958
1980
1959
pragma [ nomagic]
1981
- predicate clearSet ( NodeEx node , ContentSet c , Configuration config ) {
1960
+ private predicate clearSet ( NodeEx node , ContentSet c , Configuration config ) {
1982
1961
PrevStage:: revFlow ( node , config ) and
1983
1962
clearsContentCached ( node .asNode ( ) , c )
1984
1963
}
@@ -4270,7 +4249,7 @@ private module Subpaths {
4270
4249
result .isHidden ( ) and
4271
4250
exists ( NodeEx n1 , NodeEx n2 | n1 = n .getNodeEx ( ) and n2 = result .getNodeEx ( ) |
4272
4251
localFlowBigStep ( n1 , _, n2 , _, _, _, _, _) or
4273
- storeSet ( n1 , _, n2 , _ , _, _) or
4252
+ store ( n1 , _, n2 , _, _) or
4274
4253
readSet ( n1 , _, n2 , _)
4275
4254
)
4276
4255
}
@@ -4921,11 +4900,10 @@ private module FlowExploration {
4921
4900
PartialPathNodeFwd mid , PartialAccessPath ap1 , TypedContent tc , NodeEx node ,
4922
4901
PartialAccessPath ap2
4923
4902
) {
4924
- exists ( NodeEx midNode , Content c , DataFlowType contentType , DataFlowType containerType |
4903
+ exists ( NodeEx midNode , DataFlowType contentType |
4925
4904
midNode = mid .getNodeEx ( ) and
4926
4905
ap1 = mid .getAp ( ) and
4927
- store ( midNode , c , node , contentType , containerType , mid .getConfiguration ( ) ) and
4928
- tc = MkTypedContent ( c , containerType ) and
4906
+ store ( midNode , tc , node , contentType , mid .getConfiguration ( ) ) and
4929
4907
ap2 .getHead ( ) = tc and
4930
4908
ap2 .len ( ) = unbindInt ( ap1 .len ( ) + 1 ) and
4931
4909
compatibleTypes ( ap1 .getType ( ) , contentType )
@@ -4947,11 +4925,10 @@ private module FlowExploration {
4947
4925
PartialPathNodeFwd mid , PartialAccessPath ap , TypedContent tc , NodeEx node , CallContext cc ,
4948
4926
Configuration config
4949
4927
) {
4950
- exists ( NodeEx midNode , Content c |
4928
+ exists ( NodeEx midNode |
4951
4929
midNode = mid .getNodeEx ( ) and
4952
4930
ap = mid .getAp ( ) and
4953
- read ( midNode , c , node , pragma [ only_bind_into ] ( config ) ) and
4954
- tc .getContent ( ) = c and
4931
+ read ( midNode , tc .getContent ( ) , node , pragma [ only_bind_into ] ( config ) ) and
4955
4932
ap .getHead ( ) = tc and
4956
4933
pragma [ only_bind_into ] ( config ) = mid .getConfiguration ( ) and
4957
4934
cc = mid .getCallContext ( )
@@ -5202,12 +5179,13 @@ private module FlowExploration {
5202
5179
private predicate revPartialPathStoreStep (
5203
5180
PartialPathNodeRev mid , RevPartialAccessPath ap , Content c , NodeEx node , Configuration config
5204
5181
) {
5205
- exists ( NodeEx midNode , DataFlowType contentType , DataFlowType containerType , TypedContent tc |
5182
+ exists ( NodeEx midNode , TypedContent tc |
5206
5183
midNode = mid .getNodeEx ( ) and
5207
5184
ap = mid .getAp ( ) and
5208
- store ( node , c , midNode , contentType , containerType , config ) and
5209
- tc = MkTypedContent ( c , containerType ) and
5210
- config = mid .getConfiguration ( )
5185
+ store ( node , tc , midNode , _, config ) and
5186
+ ap .getHead ( ) = c and
5187
+ config = mid .getConfiguration ( ) and
5188
+ tc .getContent ( ) = c
5211
5189
)
5212
5190
}
5213
5191
0 commit comments