@@ -667,23 +667,77 @@ private module Stage1 implements StageSig {
667
667
)
668
668
or
669
669
// flow into a callable
670
- exists ( NodeEx arg |
671
- fwdFlow ( arg , _, config ) and
672
- viableParamArgEx ( _, node , arg ) and
673
- cc = true and
674
- not fullBarrier ( node , config )
675
- )
670
+ fwdFlowIn ( _, _, _, node , config ) and
671
+ cc = true
676
672
or
677
673
// flow out of a callable
674
+ fwdFlowOut ( _, node , false , config ) and
675
+ cc = false
676
+ or
677
+ // flow through a callable
678
678
exists ( DataFlowCall call |
679
- fwdFlowOut ( call , node , false , config ) and
680
- cc = false
681
- or
682
679
fwdFlowOutFromArg ( call , node , config ) and
683
680
fwdFlowIsEntered ( call , cc , config )
684
681
)
685
682
}
686
683
684
+ // inline to reduce the number of iterations
685
+ pragma [ inline]
686
+ private predicate fwdFlowIn (
687
+ DataFlowCall call , NodeEx arg , Cc cc , ParamNodeEx p , Configuration config
688
+ ) {
689
+ // call context cannot help reduce virtual dispatch
690
+ fwdFlow ( arg , cc , config ) and
691
+ viableParamArgEx ( call , p , arg ) and
692
+ not fullBarrier ( p , config ) and
693
+ (
694
+ cc = false
695
+ or
696
+ not reducedViableImplInCallContext ( call , _, _)
697
+ )
698
+ or
699
+ // call context may help reduce virtual dispatch
700
+ exists ( DataFlowCallable target |
701
+ fwdFlowInReducedViableImplInSomeCallContext ( call , arg , p , target , config ) and
702
+ target = viableImplInSomeFwdFlowCallContextExt ( call , config ) and
703
+ cc = true
704
+ )
705
+ }
706
+
707
+ /**
708
+ * Holds if an argument to `call` is reached in the flow covered by `fwdFlow`.
709
+ */
710
+ pragma [ nomagic]
711
+ private predicate fwdFlowIsEntered ( DataFlowCall call , Cc cc , Configuration config ) {
712
+ fwdFlowIn ( call , _, cc , _, config )
713
+ }
714
+
715
+ pragma [ nomagic]
716
+ private predicate fwdFlowInReducedViableImplInSomeCallContext (
717
+ DataFlowCall call , NodeEx arg , ParamNodeEx p , DataFlowCallable target , Configuration config
718
+ ) {
719
+ fwdFlow ( arg , true , config ) and
720
+ viableParamArgEx ( call , p , arg ) and
721
+ reducedViableImplInCallContext ( call , _, _) and
722
+ target = p .getEnclosingCallable ( ) and
723
+ not fullBarrier ( p , config )
724
+ }
725
+
726
+ /**
727
+ * Gets a viable dispatch target of `call` in the context `ctx`. This is
728
+ * restricted to those `call`s for which a context might make a difference,
729
+ * and to `ctx`s that are reachable in `fwdFlow`.
730
+ */
731
+ pragma [ nomagic]
732
+ private DataFlowCallable viableImplInSomeFwdFlowCallContextExt (
733
+ DataFlowCall call , Configuration config
734
+ ) {
735
+ exists ( DataFlowCall ctx |
736
+ fwdFlowIsEntered ( ctx , _, config ) and
737
+ result = viableImplInCallContextExt ( call , ctx )
738
+ )
739
+ }
740
+
687
741
private predicate fwdFlow ( NodeEx node , Configuration config ) { fwdFlow ( node , _, config ) }
688
742
689
743
pragma [ nomagic]
@@ -726,7 +780,8 @@ private module Stage1 implements StageSig {
726
780
)
727
781
}
728
782
729
- pragma [ nomagic]
783
+ // inline to reduce the number of iterations
784
+ pragma [ inline]
730
785
private predicate fwdFlowOut ( DataFlowCall call , NodeEx out , Cc cc , Configuration config ) {
731
786
exists ( ReturnPosition pos |
732
787
fwdFlowReturnPosition ( pos , cc , config ) and
@@ -740,17 +795,6 @@ private module Stage1 implements StageSig {
740
795
fwdFlowOut ( call , out , true , config )
741
796
}
742
797
743
- /**
744
- * Holds if an argument to `call` is reached in the flow covered by `fwdFlow`.
745
- */
746
- pragma [ nomagic]
747
- private predicate fwdFlowIsEntered ( DataFlowCall call , Cc cc , Configuration config ) {
748
- exists ( ArgNodeEx arg |
749
- fwdFlow ( arg , cc , config ) and
750
- viableParamArgEx ( call , _, arg )
751
- )
752
- }
753
-
754
798
private predicate stateStepFwd ( FlowState state1 , FlowState state2 , Configuration config ) {
755
799
exists ( NodeEx node1 |
756
800
additionalLocalStateStep ( node1 , state1 , _, state2 , config ) or
@@ -817,20 +861,21 @@ private module Stage1 implements StageSig {
817
861
)
818
862
or
819
863
// flow into a callable
820
- exists ( DataFlowCall call |
821
- revFlowIn ( call , node , false , config ) and
822
- toReturn = false
823
- or
824
- revFlowInToReturn ( call , node , config ) and
825
- revFlowIsReturned ( call , toReturn , config )
826
- )
864
+ revFlowIn ( _, node , false , config ) and
865
+ toReturn = false
827
866
or
828
867
// flow out of a callable
829
868
exists ( ReturnPosition pos |
830
869
revFlowOut ( pos , config ) and
831
870
node .( RetNodeEx ) .getReturnPosition ( ) = pos and
832
871
toReturn = true
833
872
)
873
+ or
874
+ // flow through a callable
875
+ exists ( DataFlowCall call |
876
+ revFlowInToReturn ( call , node , config ) and
877
+ revFlowIsReturned ( call , toReturn , config )
878
+ )
834
879
}
835
880
836
881
/**
@@ -886,11 +931,11 @@ private module Stage1 implements StageSig {
886
931
additional predicate viableParamArgNodeCandFwd1 (
887
932
DataFlowCall call , ParamNodeEx p , ArgNodeEx arg , Configuration config
888
933
) {
889
- viableParamArgEx ( call , p , arg ) and
890
- fwdFlow ( arg , config )
934
+ fwdFlowIn ( call , arg , _, p , config )
891
935
}
892
936
893
- pragma [ nomagic]
937
+ // inline to reduce the number of iterations
938
+ pragma [ inline]
894
939
private predicate revFlowIn (
895
940
DataFlowCall call , ArgNodeEx arg , boolean toReturn , Configuration config
896
941
) {
0 commit comments