@@ -116,7 +116,7 @@ abstract class Configuration extends string {
116
116
* Holds if an arbitrary number of implicit read steps of content `c` may be
117
117
* taken at `node`.
118
118
*/
119
- predicate allowImplicitRead ( Node node , Content c ) { none ( ) }
119
+ predicate allowImplicitRead ( Node node , ContentSet c ) { none ( ) }
120
120
121
121
/**
122
122
* Gets the virtual dispatch branching limit when calculating field flow.
@@ -485,8 +485,9 @@ private predicate additionalJumpStateStep(
485
485
)
486
486
}
487
487
488
- private predicate read ( NodeEx node1 , Content c , NodeEx node2 , Configuration config ) {
489
- read ( node1 .asNode ( ) , c , node2 .asNode ( ) ) and
488
+ pragma [ nomagic]
489
+ private predicate readSet ( NodeEx node1 , ContentSet c , NodeEx node2 , Configuration config ) {
490
+ readSet ( node1 .asNode ( ) , c , node2 .asNode ( ) ) and
490
491
stepFilter ( node1 , node2 , config )
491
492
or
492
493
exists ( Node n |
@@ -496,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
496
497
)
497
498
}
498
499
500
+ // inline to reduce fan-out via `getAReadContent`
501
+ pragma [ inline]
502
+ private predicate read ( NodeEx node1 , Content c , NodeEx node2 , Configuration config ) {
503
+ exists ( ContentSet cs |
504
+ readSet ( node1 , cs , node2 , config ) and
505
+ c = cs .getAReadContent ( )
506
+ )
507
+ }
508
+
509
+ // inline to reduce fan-out via `getAReadContent`
510
+ pragma [ inline]
511
+ private predicate clearsContentEx ( NodeEx n , Content c ) {
512
+ exists ( ContentSet cs |
513
+ clearsContentCached ( n .asNode ( ) , cs ) and
514
+ c = cs .getAReadContent ( )
515
+ )
516
+ }
517
+
518
+ pragma [ nomagic]
499
519
private predicate store (
500
520
NodeEx node1 , TypedContent tc , NodeEx node2 , DataFlowType contentType , Configuration config
501
521
) {
@@ -573,9 +593,9 @@ private module Stage1 {
573
593
)
574
594
or
575
595
// read
576
- exists ( Content c |
577
- fwdFlowRead ( c , node , cc , config ) and
578
- fwdFlowConsCand ( c , config )
596
+ exists ( ContentSet c |
597
+ fwdFlowReadSet ( c , node , cc , config ) and
598
+ fwdFlowConsCandSet ( c , _ , config )
579
599
)
580
600
or
581
601
// flow into a callable
@@ -599,10 +619,10 @@ private module Stage1 {
599
619
private predicate fwdFlow ( NodeEx node , Configuration config ) { fwdFlow ( node , _, config ) }
600
620
601
621
pragma [ nomagic]
602
- private predicate fwdFlowRead ( Content c , NodeEx node , Cc cc , Configuration config ) {
622
+ private predicate fwdFlowReadSet ( ContentSet c , NodeEx node , Cc cc , Configuration config ) {
603
623
exists ( NodeEx mid |
604
624
fwdFlow ( mid , cc , config ) and
605
- read ( mid , c , node , config )
625
+ readSet ( mid , c , node , config )
606
626
)
607
627
}
608
628
@@ -620,6 +640,16 @@ private module Stage1 {
620
640
)
621
641
}
622
642
643
+ /**
644
+ * Holds if `cs` may be interpreted in a read as the target of some store
645
+ * into `c`, in the flow covered by `fwdFlow`.
646
+ */
647
+ pragma [ nomagic]
648
+ private predicate fwdFlowConsCandSet ( ContentSet cs , Content c , Configuration config ) {
649
+ fwdFlowConsCand ( c , config ) and
650
+ c = cs .getAReadContent ( )
651
+ }
652
+
623
653
pragma [ nomagic]
624
654
private predicate fwdFlowReturnPosition ( ReturnPosition pos , Cc cc , Configuration config ) {
625
655
exists ( RetNodeEx ret |
@@ -712,9 +742,9 @@ private module Stage1 {
712
742
)
713
743
or
714
744
// read
715
- exists ( NodeEx mid , Content c |
716
- read ( node , c , mid , config ) and
717
- fwdFlowConsCand ( c , pragma [ only_bind_into ] ( config ) ) and
745
+ exists ( NodeEx mid , ContentSet c |
746
+ readSet ( node , c , mid , config ) and
747
+ fwdFlowConsCandSet ( c , _ , pragma [ only_bind_into ] ( config ) ) and
718
748
revFlow ( mid , toReturn , pragma [ only_bind_into ] ( config ) )
719
749
)
720
750
or
@@ -740,10 +770,10 @@ private module Stage1 {
740
770
*/
741
771
pragma [ nomagic]
742
772
private predicate revFlowConsCand ( Content c , Configuration config ) {
743
- exists ( NodeEx mid , NodeEx node |
773
+ exists ( NodeEx mid , NodeEx node , ContentSet cs |
744
774
fwdFlow ( node , pragma [ only_bind_into ] ( config ) ) and
745
- read ( node , c , mid , config ) and
746
- fwdFlowConsCand ( c , pragma [ only_bind_into ] ( config ) ) and
775
+ readSet ( node , cs , mid , config ) and
776
+ fwdFlowConsCandSet ( cs , c , pragma [ only_bind_into ] ( config ) ) and
747
777
revFlow ( pragma [ only_bind_into ] ( mid ) , _, pragma [ only_bind_into ] ( config ) )
748
778
)
749
779
}
@@ -762,6 +792,7 @@ private module Stage1 {
762
792
* Holds if `c` is the target of both a read and a store in the flow covered
763
793
* by `revFlow`.
764
794
*/
795
+ pragma [ nomagic]
765
796
private predicate revFlowIsReadAndStored ( Content c , Configuration conf ) {
766
797
revFlowConsCand ( c , conf ) and
767
798
revFlowStore ( c , _, _, conf )
@@ -860,9 +891,9 @@ private module Stage1 {
860
891
861
892
pragma [ nomagic]
862
893
predicate readStepCand ( NodeEx n1 , Content c , NodeEx n2 , Configuration config ) {
863
- revFlowIsReadAndStored ( c , pragma [ only_bind_into ] ( config ) ) and
864
- revFlow ( n2 , pragma [ only_bind_into ] ( config ) ) and
865
- read ( n1 , c , n2 , pragma [ only_bind_into ] ( config ) )
894
+ revFlowIsReadAndStored ( pragma [ only_bind_into ] ( c ) , pragma [ only_bind_into ] ( config ) ) and
895
+ read ( n1 , c , n2 , pragma [ only_bind_into ] ( config ) ) and
896
+ revFlow ( n2 , pragma [ only_bind_into ] ( config ) )
866
897
}
867
898
868
899
pragma [ nomagic]
@@ -1574,7 +1605,7 @@ private module Stage2 {
1574
1605
Configuration config
1575
1606
) {
1576
1607
exists ( Ap ap2 , Content c |
1577
- store ( node1 , tc , node2 , contentType , config ) and
1608
+ PrevStage :: storeStepCand ( node1 , _ , tc , node2 , contentType , config ) and
1578
1609
revFlowStore ( ap2 , c , ap1 , node1 , _, tc , node2 , _, _, config ) and
1579
1610
revFlowConsCand ( ap2 , c , ap1 , config )
1580
1611
)
@@ -1729,9 +1760,9 @@ private module LocalFlowBigStep {
1729
1760
or
1730
1761
node .asNode ( ) instanceof OutNodeExt
1731
1762
or
1732
- store ( _, _, node , _, config )
1763
+ Stage2 :: storeStepCand ( _ , _, _, node , _, config )
1733
1764
or
1734
- read ( _, _, node , config )
1765
+ Stage2 :: readStepCand ( _, _, node , config )
1735
1766
or
1736
1767
node instanceof FlowCheckNode
1737
1768
or
@@ -1752,8 +1783,8 @@ private module LocalFlowBigStep {
1752
1783
additionalJumpStep ( node , next , config ) or
1753
1784
flowIntoCallNodeCand1 ( _, node , next , config ) or
1754
1785
flowOutOfCallNodeCand1 ( _, node , next , config ) or
1755
- store ( node , _, next , _, config ) or
1756
- read ( node , _, next , config )
1786
+ Stage2 :: storeStepCand ( node , _ , _, next , _, config ) or
1787
+ Stage2 :: readStepCand ( node , _, next , config )
1757
1788
)
1758
1789
or
1759
1790
exists ( NodeEx next , FlowState s | Stage2:: revFlow ( next , s , config ) |
@@ -1926,7 +1957,24 @@ private module Stage3 {
1926
1957
private predicate flowIntoCall = flowIntoCallNodeCand2 / 5 ;
1927
1958
1928
1959
pragma [ nomagic]
1929
- private predicate clear ( NodeEx node , Ap ap ) { ap .isClearedAt ( node .asNode ( ) ) }
1960
+ private predicate clearSet ( NodeEx node , ContentSet c , Configuration config ) {
1961
+ PrevStage:: revFlow ( node , config ) and
1962
+ clearsContentCached ( node .asNode ( ) , c )
1963
+ }
1964
+
1965
+ pragma [ nomagic]
1966
+ private predicate clearContent ( NodeEx node , Content c , Configuration config ) {
1967
+ exists ( ContentSet cs |
1968
+ PrevStage:: readStepCand ( _, pragma [ only_bind_into ] ( c ) , _, pragma [ only_bind_into ] ( config ) ) and
1969
+ c = cs .getAReadContent ( ) and
1970
+ clearSet ( node , cs , pragma [ only_bind_into ] ( config ) )
1971
+ )
1972
+ }
1973
+
1974
+ pragma [ nomagic]
1975
+ private predicate clear ( NodeEx node , Ap ap , Configuration config ) {
1976
+ clearContent ( node , ap .getHead ( ) .getContent ( ) , config )
1977
+ }
1930
1978
1931
1979
pragma [ nomagic]
1932
1980
private predicate castingNodeEx ( NodeEx node ) { node .asNode ( ) instanceof CastingNode }
@@ -1935,7 +1983,7 @@ private module Stage3 {
1935
1983
private predicate filter ( NodeEx node , FlowState state , Ap ap , Configuration config ) {
1936
1984
exists ( state ) and
1937
1985
exists ( config ) and
1938
- not clear ( node , ap ) and
1986
+ not clear ( node , ap , config ) and
1939
1987
if castingNodeEx ( node ) then compatibleTypes ( node .getDataFlowType ( ) , ap .getType ( ) ) else any ( )
1940
1988
}
1941
1989
@@ -2363,7 +2411,7 @@ private module Stage3 {
2363
2411
Configuration config
2364
2412
) {
2365
2413
exists ( Ap ap2 , Content c |
2366
- store ( node1 , tc , node2 , contentType , config ) and
2414
+ PrevStage :: storeStepCand ( node1 , _ , tc , node2 , contentType , config ) and
2367
2415
revFlowStore ( ap2 , c , ap1 , node1 , _, tc , node2 , _, _, config ) and
2368
2416
revFlowConsCand ( ap2 , c , ap1 , config )
2369
2417
)
@@ -3190,7 +3238,7 @@ private module Stage4 {
3190
3238
Configuration config
3191
3239
) {
3192
3240
exists ( Ap ap2 , Content c |
3193
- store ( node1 , tc , node2 , contentType , config ) and
3241
+ PrevStage :: storeStepCand ( node1 , _ , tc , node2 , contentType , config ) and
3194
3242
revFlowStore ( ap2 , c , ap1 , node1 , _, tc , node2 , _, _, config ) and
3195
3243
revFlowConsCand ( ap2 , c , ap1 , config )
3196
3244
)
@@ -4202,7 +4250,7 @@ private module Subpaths {
4202
4250
exists ( NodeEx n1 , NodeEx n2 | n1 = n .getNodeEx ( ) and n2 = result .getNodeEx ( ) |
4203
4251
localFlowBigStep ( n1 , _, n2 , _, _, _, _, _) or
4204
4252
store ( n1 , _, n2 , _, _) or
4205
- read ( n1 , _, n2 , _)
4253
+ readSet ( n1 , _, n2 , _)
4206
4254
)
4207
4255
}
4208
4256
@@ -4557,7 +4605,7 @@ private module FlowExploration {
4557
4605
or
4558
4606
exists ( PartialPathNodeRev mid |
4559
4607
revPartialPathStep ( mid , node , state , sc1 , sc2 , sc3 , ap , config ) and
4560
- not clearsContentCached ( node . asNode ( ) , ap .getHead ( ) ) and
4608
+ not clearsContentEx ( node , ap .getHead ( ) ) and
4561
4609
not fullBarrier ( node , config ) and
4562
4610
not stateBarrier ( node , state , config ) and
4563
4611
distSink ( node .getEnclosingCallable ( ) , config ) <= config .explorationLimit ( )
@@ -4573,7 +4621,7 @@ private module FlowExploration {
4573
4621
partialPathStep ( mid , node , state , cc , sc1 , sc2 , sc3 , ap , config ) and
4574
4622
not fullBarrier ( node , config ) and
4575
4623
not stateBarrier ( node , state , config ) and
4576
- not clearsContentCached ( node . asNode ( ) , ap .getHead ( ) .getContent ( ) ) and
4624
+ not clearsContentEx ( node , ap .getHead ( ) .getContent ( ) ) and
4577
4625
if node .asNode ( ) instanceof CastingNode
4578
4626
then compatibleTypes ( node .getDataFlowType ( ) , ap .getType ( ) )
4579
4627
else any ( )
0 commit comments