Skip to content

Shared, type inference: Add inference for type parameters with constraints (base type mentions) #19102

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
paldepind merged 8 commits into from
Mar 28, 2025
Merged

Shared, type inference: Add inference for type parameters with constraints (base type mentions) #19102

Changes from 1 commit
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
ba9edf8
Shared: Refactor type inference
paldepind Mar 24, 2025
831413b
Rust: Expand on type parameter bounds type inference test
paldepind Mar 25, 2025
06c8963
Shared: Infer types for type parameters with contraints
paldepind Mar 25, 2025
54e7bb7
Rust: Fix a bad join by adding bindingset to resolveTypeMentionRoot
paldepind Mar 25, 2025
efcffc5
Merge branch 'main' into rust-ti-refactor
paldepind Mar 25, 2025
520e27c
Shared: Fix typos in qldoc
paldepind Mar 25, 2025
623bc23
Rust: Address PR comments
paldepind Mar 28, 2025
989c144
Rust: Minor doc tweaks based on PR comments
paldepind Mar 28, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 29 additions & 17 deletions shared/typeinference/codeql/typeinference/internal/TypeInference.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -287,11 +287,11 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
* - `T3` is mentioned at `T2.T1` for immediate base type mention `Base<C<T3>>`
* of `Mid`,
* - ``C`1`` is mentioned at `T3` for immediate base type mention `Mid<C<T4>>`
* of `Sub`, and
* of `Sub`,
* - `T4` is mentioned at `T3.T1` for immediate base type mention `Mid<C<T4>>`
* of `Sub`, and
* of `Sub`,
* - ``C`1`` is mentioned at `T2` and implicitly at `T2.T1` for transitive base type
* mention `Base<C<T3>>` of `Sub`.
* mention `Base<C<T3>>` of `Sub`, and
* - `T4` is mentioned implicitly at `T2.T1.T1` for transitive base type mention
* `Base<C<T3>>` of `Sub`.
*/
Expand All @@ -307,8 +307,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
or
// transitive base class
exists(Type immediateBase | immediateBase = resolveTypeMentionRoot(immediateBaseMention) |
not t = immediateBase.getATypeParameter() and
baseTypeMentionHasTypeAt(immediateBase, baseMention, path, t)
baseTypeMentionHasNonTypeParameterAt(immediateBase, baseMention, path, t)
or
exists(TypePath path0, TypePath prefix, TypePath suffix, TypeParameter tp |
/*
Expand Down Expand Up @@ -336,15 +335,29 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
* ```
*/

baseTypeMentionHasTypeAt(immediateBase, baseMention, prefix, tp) and
tp = immediateBase.getATypeParameter() and
baseTypeMentionHasTypeParameterAt(immediateBase, baseMention, prefix, tp) and
t = immediateBaseMention.resolveTypeAt(path0) and
path0.isCons(tp, suffix) and
path = prefix.append(suffix)
)
)
)
}

/** Similar to `baseTypeMentionHasTypeAt` but FIXME: */
Copy link
Copy Markdown
Contributor

@hvitved hvitved Mar 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should be fixed ;-)

Copy link
Copy Markdown
Contributor

@hvitved hvitved Mar 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fine to simply the remove the QL doc.

Copy link
Copy Markdown
Contributor Author

@paldepind paldepind Mar 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oops 😅

pragma[inline]
predicate baseTypeMentionHasNonTypeParameterAt(
Type sub, TypeMention baseMention, TypePath path, Type t
) {
not t = sub.getATypeParameter() and baseTypeMentionHasTypeAt(sub, baseMention, path, t)
}

pragma[inline]
predicate baseTypeMentionHasTypeParameterAt(
Type sub, TypeMention baseMention, TypePath path, TypeParameter tp
) {
tp = sub.getATypeParameter() and baseTypeMentionHasTypeAt(sub, baseMention, path, tp)
}
}

private import BaseTypes
Expand Down Expand Up @@ -514,7 +527,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
private module AccessBaseType {
/**
* Holds if inferring types at `a` might depend on the type at `path` of
* `apos` having `baseMention` as a transitive base type mention.
* `apos` having `base` as a transitive base type mention.
Copy link
Copy Markdown
Contributor

@hvitved hvitved Mar 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

remove mention.

*/
private predicate relevantAccess(Access a, AccessPosition apos, TypePath path, Type base) {
exists(Declaration target, DeclarationPosition dpos |
Expand Down Expand Up @@ -557,8 +570,9 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
* // ^^^^^^^^^^^^^^^^^^^^^^^^^ `a`
* ```
*
* where the method call is an access and `new Sub<int>()` is at an
* access position, which is the receiver of a method call, we have:
* where the method call is an access, `new Sub<int>()` is at the access
* position which is the receiver of a method call, and `pathToSub` is
* `""` we have:
*
* `baseMention` | `path` | `t`
* ------------- | ------------ | ---
Expand All @@ -575,12 +589,10 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
) {
relevantAccess(a, apos, pathToSub, resolveTypeMentionRoot(baseMention)) and
exists(Type sub | sub = a.getInferredType(apos, pathToSub) |
not t = sub.getATypeParameter() and
baseTypeMentionHasTypeAt(sub, baseMention, path, t)
baseTypeMentionHasNonTypeParameterAt(sub, baseMention, path, t)
or
exists(TypePath prefix, TypePath suffix, TypeParameter tp |
tp = sub.getATypeParameter() and
baseTypeMentionHasTypeAt(sub, baseMention, prefix, tp) and
baseTypeMentionHasTypeParameterAt(sub, baseMention, prefix, tp) and
t = inferTypeAt(a, apos, pathToSub, tp, suffix) and
path = prefix.append(suffix)
)
Expand Down Expand Up @@ -681,15 +693,15 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
* For this example
* ```csharp
* interface IFoo<A> { }
* void M<T1, T2>(T2 item) where T2 : IFoo<T1> { }
* T1 M<T1, T2>(T2 item) where T2 : IFoo<T1> { }
* ```
* with the method declaration being the target and the for the first
* parameter position, we have the following
* - `path1 = ""`,
* - `tp1 = T2`,
* - `constraint = IFoo`,
* - `path2 = "A"`,
* - `tp2 = T1`
* - `path2 = "A"`, and
* - `tp2 = T1`.
*/
pragma[nomagic]
private predicate typeParameterConstraintHasTypeParameter(
Expand Down
Loading