@@ -616,6 +616,127 @@ private predicate bestTypeFlow(TypeFlowNode n, RefType t) {
616616 not irrelevantBound ( n , t )
617617}
618618
619+ private predicate bestTypeFlow ( TypeFlowNode n , RefType t , boolean exact ) {
620+ exactType ( n , t ) and exact = true
621+ or
622+ not exactType ( n , _) and bestTypeFlow ( n , t ) and exact = false
623+ }
624+
625+ private predicate bestTypeFlowOrTypeFlowBase ( TypeFlowNode n , RefType t , boolean exact ) {
626+ bestTypeFlow ( n , t , exact )
627+ or
628+ typeFlowBase ( n , t ) and
629+ exact = false and
630+ not bestTypeFlow ( n , _, _)
631+ }
632+
633+ /**
634+ * Holds if `n` has type `t` and this information is not propagated as a
635+ * universal bound to a subsequent node, such that `t` might form the basis for
636+ * a union type bound for that node.
637+ */
638+ private predicate unionTypeFlowBaseCand ( TypeFlowNode n , RefType t , boolean exact ) {
639+ exists ( TypeFlowNode next |
640+ joinStep ( n , next ) and
641+ bestTypeFlowOrTypeFlowBase ( n , t , exact ) and
642+ not bestTypeFlowOrTypeFlowBase ( next , t , exact ) and
643+ not exactType ( next , _)
644+ )
645+ }
646+
647+ /**
648+ * Holds if all incoming type flow can be traced back to a
649+ * `unionTypeFlowBaseCand`, such that we can compute a union type bound for `n`.
650+ * Disregards nodes for which we have an exact bound.
651+ */
652+ private predicate hasUnionTypeFlow ( TypeFlowNode n ) {
653+ not exactType ( n , _) and
654+ (
655+ forex ( TypeFlowNode mid | joinStep ( mid , n ) |
656+ unionTypeFlowBaseCand ( mid , _, _) or hasUnionTypeFlow ( mid )
657+ )
658+ or
659+ exists ( TypeFlowNode scc |
660+ sccRepr ( n , scc ) and
661+ forex ( TypeFlowNode mid | sccJoinStep ( mid , scc ) |
662+ unionTypeFlowBaseCand ( mid , _, _) or hasUnionTypeFlow ( mid )
663+ )
664+ )
665+ or
666+ exists ( TypeFlowNode mid | step ( mid , n ) and hasUnionTypeFlow ( mid ) )
667+ )
668+ }
669+
670+ pragma [ nomagic]
671+ private RefType getTypeBound ( TypeFlowNode n ) {
672+ bestTypeFlow ( n , result )
673+ or
674+ not bestTypeFlow ( n , _) and result = n .getType ( )
675+ }
676+
677+ pragma [ nomagic]
678+ private predicate unionTypeFlow0 ( TypeFlowNode n , RefType t , boolean exact ) {
679+ hasUnionTypeFlow ( n ) and
680+ exists ( TypeFlowNode mid | anyStep ( mid , n ) |
681+ unionTypeFlowBaseCand ( mid , t , exact ) or unionTypeFlow ( mid , t , exact )
682+ )
683+ }
684+
685+ /** Holds if we have a union type bound for `n` and `t` is one of its parts. */
686+ private predicate unionTypeFlow ( TypeFlowNode n , RefType t , boolean exact ) {
687+ unionTypeFlow0 ( n , t , exact ) and
688+ // filter impossible union parts:
689+ if exact = true
690+ then t .getErasure ( ) .( RefType ) .getASourceSupertype * ( ) = getTypeBound ( n ) .getErasure ( )
691+ else haveIntersection ( getTypeBound ( n ) , t )
692+ }
693+
694+ /**
695+ * Holds if the inferred union type bound for `n` contains the best universal
696+ * bound and thus is irrelevant.
697+ */
698+ private predicate irrelevantUnionType ( TypeFlowNode n ) {
699+ exists ( RefType t , RefType nt , RefType te , RefType nte |
700+ unionTypeFlow ( n , t , false ) and
701+ nt = getTypeBound ( n ) and
702+ te = t .getErasure ( ) and
703+ nte = nt .getErasure ( )
704+ |
705+ nt .getASupertype * ( ) = t
706+ or
707+ nte .getASourceSupertype + ( ) = te
708+ or
709+ nte = te and unbound ( t )
710+ )
711+ }
712+
713+ /**
714+ * Holds if `t` is an irrelevant part of the union type bound for `n` due to
715+ * being contained in another part of the union type bound.
716+ */
717+ private predicate irrelevantUnionTypePart ( TypeFlowNode n , RefType t , boolean exact ) {
718+ unionTypeFlow ( n , t , exact ) and
719+ not irrelevantUnionType ( n ) and
720+ exists ( RefType weaker |
721+ unionTypeFlow ( n , weaker , false ) and
722+ t .getASupertype * ( ) = weaker
723+ |
724+ exact = true or not weaker .getASupertype * ( ) = t
725+ )
726+ }
727+
728+ /**
729+ * Holds if the runtime type of `n` is bounded by a union type and if this
730+ * bound is likely to be better than the static type of `n`. The union type is
731+ * made up of the types `t` related to `n` by this predicate, and the flag
732+ * `exact` indicates whether `t` is an exact bound or merely an upper bound.
733+ */
734+ private predicate bestUnionType ( TypeFlowNode n , RefType t , boolean exact ) {
735+ unionTypeFlow ( n , t , exact ) and
736+ not irrelevantUnionType ( n ) and
737+ not irrelevantUnionTypePart ( n , t , exact )
738+ }
739+
619740cached
620741private module TypeFlowBounds {
621742 /**
@@ -627,11 +748,7 @@ private module TypeFlowBounds {
627748 predicate fieldTypeFlow ( Field f , RefType t , boolean exact ) {
628749 exists ( TypeFlowNode n |
629750 n .asField ( ) = f and
630- (
631- exactType ( n , t ) and exact = true
632- or
633- not exactType ( n , _) and bestTypeFlow ( n , t ) and exact = false
634- )
751+ bestTypeFlow ( n , t , exact )
635752 )
636753 }
637754
@@ -644,11 +761,21 @@ private module TypeFlowBounds {
644761 predicate exprTypeFlow ( Expr e , RefType t , boolean exact ) {
645762 exists ( TypeFlowNode n |
646763 n .asExpr ( ) = e and
647- (
648- exactType ( n , t ) and exact = true
649- or
650- not exactType ( n , _) and bestTypeFlow ( n , t ) and exact = false
651- )
764+ bestTypeFlow ( n , t , exact )
765+ )
766+ }
767+
768+ /**
769+ * Holds if the runtime type of `e` is bounded by a union type and if this
770+ * bound is likely to be better than the static type of `e`. The union type is
771+ * made up of the types `t` related to `e` by this predicate, and the flag
772+ * `exact` indicates whether `t` is an exact bound or merely an upper bound.
773+ */
774+ cached
775+ predicate exprUnionTypeFlow ( Expr e , RefType t , boolean exact ) {
776+ exists ( TypeFlowNode n |
777+ n .asExpr ( ) = e and
778+ bestUnionType ( n , t , exact )
652779 )
653780 }
654781}
0 commit comments