@@ -188,7 +188,7 @@ private predicate typePrefixContainsAux1(
188188 exists ( ParameterizedPrefix pps0 |
189189 typePrefixContains ( pps0 , ppt0 ) and
190190 pps = TTypeParam ( pps0 , s ) and
191- s instanceof Wildcard
191+ s instanceof Wildcard // manual magic, implied by `typeArgumentContains(_, s, t, _)`
192192 )
193193}
194194
@@ -197,6 +197,7 @@ private predicate typePrefixContainsAux2(
197197 ParameterizedPrefix ppt , ParameterizedPrefix ppt0 , RefType s
198198) {
199199 exists ( GenericType g , int n , RefType t |
200+ // Implies `ppt = TTypeParam(ppt0, t)`
200201 ppt .split ( g , ppt0 , t , n ) and
201202 typeArgumentContains ( g , s , t , n )
202203 )
@@ -268,24 +269,36 @@ private predicate wildcardExtendsObject(Wildcard wc) {
268269 wc .getUpperBound ( ) .getType ( ) instanceof TypeObject
269270}
270271
271- private predicate subtypeStarMagic1 ( RefType t ) { t = any ( Wildcard w ) .getUpperBound ( ) .getType ( ) }
272+ // manual magic for `hasSubtypeStar1`
273+ private predicate getAWildcardUpperBound ( RefType t ) {
274+ t = any ( Wildcard w ) .getUpperBound ( ) .getType ( )
275+ }
272276
273- private predicate subtypeStarMagic2 ( RefType t ) { t = any ( Wildcard w ) .getLowerBound ( ) .getType ( ) }
277+ // manual magic for `hasSubtypeStar2`
278+ private predicate getAWildcardLowerBound ( RefType t ) {
279+ t = any ( Wildcard w ) .getLowerBound ( ) .getType ( )
280+ }
274281
282+ /**
283+ * Holds if `hasSubtype*(t, sub)`, but manuel-magic'ed with `getAWildcardUpperBound(t)`.
284+ */
275285pragma [ nomagic]
276286private predicate hasSubtypeStar1 ( RefType t , RefType sub ) {
277- sub = t and subtypeStarMagic1 ( t )
287+ sub = t and getAWildcardUpperBound ( t )
278288 or
279- hasSubtype ( t , sub ) and subtypeStarMagic1 ( t )
289+ hasSubtype ( t , sub ) and getAWildcardUpperBound ( t )
280290 or
281291 exists ( RefType mid | hasSubtypeStar1 ( t , mid ) and hasSubtype ( mid , sub ) )
282292}
283293
294+ /**
295+ * Holds if `hasSubtype*(t, sub)`, but manuel-magic'ed with `getAWildcardLowerBound(sub)`.
296+ */
284297pragma [ nomagic]
285298private predicate hasSubtypeStar2 ( RefType t , RefType sub ) {
286- sub = t and subtypeStarMagic2 ( sub )
299+ sub = t and getAWildcardLowerBound ( sub )
287300 or
288- hasSubtype ( t , sub ) and subtypeStarMagic2 ( sub )
301+ hasSubtype ( t , sub ) and getAWildcardLowerBound ( sub )
289302 or
290303 exists ( RefType mid | hasSubtype ( t , mid ) and hasSubtypeStar2 ( mid , sub ) )
291304}
0 commit comments