Skip to content

Commit da43673

Browse files
committed
Shared: Refactor type inference
1 parent 860ba2e commit da43673

File tree

1 file changed

+42
-111
lines changed

1 file changed

+42
-111
lines changed

shared/typeinference/codeql/typeinference/internal/TypeInference.qll

Lines changed: 42 additions & 111 deletions
Original file line numberDiff line numberDiff line change
@@ -268,10 +268,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
268268
private module BaseTypes {
269269
/**
270270
* Holds if `baseMention` is a (transitive) base type mention of `sub`,
271-
* and type parameter `tp` (belonging to `sub`) is mentioned (implicitly)
272-
* at `path` inside the type that `baseMention` resolves to.
273-
*
274-
* For example, in
271+
* and `t` is mentioned (implicitly) at `path` inside `baseMention`. For
272+
* example, in
275273
*
276274
* ```csharp
277275
* class C<T1> { }
@@ -283,88 +281,21 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
283281
* class Sub<T4> : Mid<C<T4>> { } // Sub<T4> extends Base<C<C<T4>>
284282
* ```
285283
*
286-
* - `T3` is mentioned at `0.0` for immediate base type mention `Base<C<T3>>`
284+
* - ``C`1`` is mentioned at `T2` for immediate base type mention `Base<C<T3>>`
287285
* of `Mid`,
288-
* - `T4` is mentioned at `0.0` for immediate base type mention `Mid<C<T4>>`
289-
* of `Sub`, and
290-
* - `T4` is mentioned implicitly at `0.0.0` for transitive base type mention
291-
* `Base<C<T3>>` of `Sub`.
292-
*/
293-
pragma[nomagic]
294-
predicate baseTypeMentionHasTypeParameterAt(
295-
Type sub, TypeMention baseMention, TypePath path, TypeParameter tp
296-
) {
297-
exists(TypeMention immediateBaseMention, TypePath pathToTypeParam |
298-
tp = sub.getATypeParameter() and
299-
immediateBaseMention = getABaseTypeMention(sub) and
300-
tp = immediateBaseMention.resolveTypeAt(pathToTypeParam)
301-
|
302-
// immediate base class
303-
baseMention = immediateBaseMention and
304-
path = pathToTypeParam
305-
or
306-
// transitive base class
307-
exists(Type immediateBase, TypePath prefix, TypePath suffix, TypeParameter mid |
308-
/*
309-
* Example:
310-
*
311-
* - `prefix = "0.0"`,
312-
* - `pathToTypeParam = "0.0"`,
313-
* - `suffix = "0"`,
314-
* - `path = "0.0.0"`
315-
*
316-
* ```csharp
317-
* class C<T1> { }
318-
*
319-
* class Base<T2> { }
320-
*
321-
* class Mid<T3> : Base<C<T3>> { }
322-
* // ^^^ `immediateBase`
323-
* // ^^ `mid`
324-
* // ^^^^^^^^^^^ `baseMention`
325-
*
326-
* class Sub<T4> : Mid<C<T4>> { }
327-
* // ^^^ `sub`
328-
* // ^^ `tp`
329-
* // ^^^^^^^^^^ `immediateBaseMention`
330-
* ```
331-
*/
332-
333-
immediateBase = resolveTypeMentionRoot(immediateBaseMention) and
334-
baseTypeMentionHasTypeParameterAt(immediateBase, baseMention, prefix, mid) and
335-
pathToTypeParam.isCons(mid, suffix) and
336-
path = prefix.append(suffix)
337-
)
338-
)
339-
}
340-
341-
/**
342-
* Holds if `baseMention` is a (transitive) base type mention of `sub`,
343-
* and `t`, which is not a type parameter of `sub`, is mentioned
344-
* (implicitly) at `path` inside `baseMention`. For example, in
345-
*
346-
* ```csharp
347-
* class C<T1> { }
348-
*
349-
* class Base<T2> { }
350-
*
351-
* class Mid<T3> : Base<C<T3>> { }
352-
*
353-
* class Sub<T4> : Mid<C<T4>> { } // Sub<T4> extends Base<C<C<T4>>
354-
* ```
355-
*
356-
* - ``C`1`` is mentioned at `0` for immediate base type mention `Base<C<T3>>`
286+
* - `T3` is mentioned at `T2.T1` for immediate base type mention `Base<C<T3>>`
357287
* of `Mid`,
358-
* - ``C`1`` is mentioned at `0` for immediate base type mention `Mid<C<T4>>`
288+
* - ``C`1`` is mentioned at `T3` for immediate base type mention `Mid<C<T4>>`
289+
* of `Sub`, and
290+
* - `T4` is mentioned at `T3.T1` for immediate base type mention `Mid<C<T4>>`
359291
* of `Sub`, and
360-
* - ``C`1`` is mentioned at `0` and implicitly at `0.0` for transitive base type
292+
* - ``C`1`` is mentioned at `T2` and implicitly at `T2.T1` for transitive base type
361293
* mention `Base<C<T3>>` of `Sub`.
294+
* - `T4` is mentioned implicitly at `T2.T1.T1` for transitive base type mention
295+
* `Base<C<T3>>` of `Sub`.
362296
*/
363297
pragma[nomagic]
364-
predicate baseTypeMentionHasNonTypeParameterAt(
365-
Type sub, TypeMention baseMention, TypePath path, Type t
366-
) {
367-
not t = sub.getATypeParameter() and
298+
predicate baseTypeMentionHasTypeAt(Type sub, TypeMention baseMention, TypePath path, Type t) {
368299
exists(TypeMention immediateBaseMention |
369300
pragma[only_bind_into](immediateBaseMention) =
370301
getABaseTypeMention(pragma[only_bind_into](sub))
@@ -375,16 +306,17 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
375306
or
376307
// transitive base class
377308
exists(Type immediateBase | immediateBase = resolveTypeMentionRoot(immediateBaseMention) |
378-
baseTypeMentionHasNonTypeParameterAt(immediateBase, baseMention, path, t)
309+
not t = immediateBase.getATypeParameter() and
310+
baseTypeMentionHasTypeAt(immediateBase, baseMention, path, t)
379311
or
380312
exists(TypePath path0, TypePath prefix, TypePath suffix, TypeParameter tp |
381313
/*
382314
* Example:
383315
*
384-
* - `prefix = "0.0"`,
385-
* - `path0 = "0"`,
316+
* - `prefix = "T2.T1"`,
317+
* - `path0 = "T3"`,
386318
* - `suffix = ""`,
387-
* - `path = "0.0"`
319+
* - `path = "T2.T1"`
388320
*
389321
* ```csharp
390322
* class C<T1> { }
@@ -403,7 +335,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
403335
* ```
404336
*/
405337

406-
baseTypeMentionHasTypeParameterAt(immediateBase, baseMention, prefix, tp) and
338+
baseTypeMentionHasTypeAt(immediateBase, baseMention, prefix, tp) and
339+
tp = immediateBase.getATypeParameter() and
407340
t = immediateBaseMention.resolveTypeAt(path0) and
408341
path0.isCons(tp, suffix) and
409342
path = prefix.append(suffix)
@@ -578,22 +511,27 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
578511
}
579512

580513
private module AccessBaseType {
581-
private predicate relevantAccess(Access a, AccessPosition apos) {
582-
exists(Declaration target |
583-
adjustedAccessType(a, apos, target, _, _) and
584-
target.getDeclaredType(_, _) instanceof TypeParameter
514+
/**
515+
* Holds if inferring types at `a` might depend on the type at `apos`
516+
* having `baseMention` as a transitive base type mention.
517+
*/
518+
private predicate relevantAccess(Access a, AccessPosition apos, TypeMention baseMention) {
519+
exists(Declaration target, DeclarationPosition dpos |
520+
a.getTarget() = target and
521+
accessDeclarationPositionMatch(apos, dpos) and
522+
declarationBaseType(target, dpos, baseMention, _, _)
585523
)
586524
}
587525

588526
pragma[nomagic]
589527
private Type inferRootType(Access a, AccessPosition apos) {
590-
relevantAccess(a, apos) and
528+
relevantAccess(a, apos, _) and
591529
result = a.getInferredType(apos, TypePath::nil())
592530
}
593531

594532
pragma[nomagic]
595533
private Type inferTypeAt(Access a, AccessPosition apos, TypeParameter tp, TypePath suffix) {
596-
relevantAccess(a, apos) and
534+
relevantAccess(a, apos, _) and
597535
exists(TypePath path0 |
598536
result = a.getInferredType(apos, path0) and
599537
path0.isCons(tp, suffix)
@@ -634,42 +572,33 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
634572
predicate hasBaseTypeMention(
635573
Access a, AccessPosition apos, TypeMention baseMention, TypePath path, Type t
636574
) {
575+
relevantAccess(a, apos, baseMention) and
637576
exists(Type sub | sub = inferRootType(a, apos) |
638-
baseTypeMentionHasNonTypeParameterAt(sub, baseMention, path, t)
577+
not t = sub.getATypeParameter() and
578+
baseTypeMentionHasTypeAt(sub, baseMention, path, t)
639579
or
640580
exists(TypePath prefix, TypePath suffix, TypeParameter tp |
641-
baseTypeMentionHasTypeParameterAt(sub, baseMention, prefix, tp) and
581+
tp = sub.getATypeParameter() and
582+
baseTypeMentionHasTypeAt(sub, baseMention, prefix, tp) and
642583
t = inferTypeAt(a, apos, tp, suffix) and
643584
path = prefix.append(suffix)
644585
)
645586
)
646587
}
647588
}
648589

649-
/**
650-
* Holds if the type of `a` at `apos` has the base type `base`, and when
651-
* viewed as an element of that type has the type `t` at `path`.
652-
*/
653-
pragma[nomagic]
654-
private predicate accessBaseType(
655-
Access a, AccessPosition apos, Type base, TypePath path, Type t
656-
) {
657-
exists(TypeMention tm |
658-
AccessBaseType::hasBaseTypeMention(a, apos, tm, path, t) and
659-
base = resolveTypeMentionRoot(tm)
660-
)
661-
}
662-
663590
/**
664591
* Holds if the declared type at `decl` for `dpos` at the `path` is `tp`
665592
* and `path` starts with a type parameter of `base`.
666593
*/
667594
pragma[nomagic]
668595
private predicate declarationBaseType(
669-
Declaration decl, DeclarationPosition dpos, Type base, TypePath path, TypeParameter tp
596+
Declaration decl, DeclarationPosition dpos, TypeMention base, TypePath path,
597+
TypeParameter tp
670598
) {
599+
base = getABaseTypeMention(_) and
671600
tp = decl.getDeclaredType(dpos, path) and
672-
path.isCons(base.getATypeParameter(), _)
601+
path.isCons(resolveTypeMentionRoot(base).getATypeParameter(), _)
673602
}
674603

675604
/**
@@ -710,8 +639,10 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
710639
) {
711640
not exists(getTypeArgument(a, target, tp, _)) and
712641
target = a.getTarget() and
713-
exists(AccessPosition apos, DeclarationPosition dpos, Type base, TypePath pathToTypeParam |
714-
accessBaseType(a, apos, base, pathToTypeParam.append(path), t) and
642+
exists(
643+
AccessPosition apos, DeclarationPosition dpos, TypeMention base, TypePath pathToTypeParam
644+
|
645+
AccessBaseType::hasBaseTypeMention(a, apos, base, pathToTypeParam.append(path), t) and
715646
declarationBaseType(target, dpos, base, pathToTypeParam, tp) and
716647
accessDeclarationPositionMatch(apos, dpos)
717648
)

0 commit comments

Comments
 (0)