From 475d872ffb46485bcb6fc50f55cda5be47b723e7 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Thu, 17 Jul 2025 13:05:53 +0200 Subject: [PATCH 1/3] Shared, Rust: Adjust type inference predicates to better match use sites --- .../typeinference/internal/TypeInference.qll | 71 ++++++++----------- 1 file changed, 31 insertions(+), 40 deletions(-) diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index 0234d42e5e19..951cc02f8ad2 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -1229,11 +1229,8 @@ module Make1 Input1> { predicate relevantAccessConstraint( Access a, Declaration target, AccessPosition apos, TypePath path, Type constraint ) { - exists(DeclarationPosition dpos | - accessDeclarationPositionMatch(apos, dpos) and - target = a.getTarget() and - typeParameterConstraintHasTypeParameter(target, dpos, path, _, constraint, _, _) - ) + target = a.getTarget() and + typeParameterConstraintHasTypeParameter(target, apos, path, constraint, _, _) } private newtype TRelevantAccess = @@ -1276,12 +1273,11 @@ module Make1 Input1> { } predicate satisfiesConstraintType( - Access a, AccessPosition apos, TypePath prefix, Type constraint, TypePath path, Type t + Access a, Declaration target, AccessPosition apos, TypePath prefix, Type constraint, + TypePath path, Type t ) { - exists(RelevantAccess at | at = MkRelevantAccess(a, _, apos, prefix) | - SatisfiesConstraint::satisfiesConstraintType(at, - constraint, path, t) - ) + SatisfiesConstraint::satisfiesConstraintType(MkRelevantAccess(a, + target, apos, prefix), constraint, path, t) } } @@ -1370,37 +1366,38 @@ module Make1 Input1> { } /** - * Holds if `tp1` and `tp2` are distinct type parameters of `target`, the - * declared type at `dpos` mentions `tp1` at `path1`, `tp1` has a base - * type mention of type `constraint` that mentions `tp2` at the path - * `path2`. + * Holds if the declared type of `target` contains a type parameter at + * `apos` and `pathToConstrained` that must satisfy `constraint` and `tp` + * occurs at `pathToTp` in `constraint`. * - * For this example + * For example, in * ```csharp * interface IFoo { } * T1 M(T2 item) where T2 : IFoo { } * ``` - * with the method declaration being the target and the for the first - * parameter position, we have the following - * - `path1 = ""`, - * - `tp1 = T2`, + * with the method declaration being the target and with `apos` + * corresponding to `item`, we have the following + * - `pathToConstrained = ""`, + * - `tp = T1`, * - `constraint = IFoo`, - * - `path2 = "A"`, and - * - `tp2 = T1`. + * - `pathToTp = "A"`. */ pragma[nomagic] private predicate typeParameterConstraintHasTypeParameter( - Declaration target, DeclarationPosition dpos, TypePath path1, TypeParameter tp1, - Type constraint, TypePath path2, TypeParameter tp2 + Declaration target, AccessPosition apos, TypePath pathToConstrained, Type constraint, + TypePath pathToTp, TypeParameter tp ) { - tp1 = target.getTypeParameter(_) and - tp2 = target.getTypeParameter(_) and - tp1 != tp2 and - tp1 = target.getDeclaredType(dpos, path1) and - exists(TypeMention tm | - tm = getATypeParameterConstraint(tp1) and - tm.resolveTypeAt(path2) = tp2 and - constraint = resolveTypeMentionRoot(tm) + exists(DeclarationPosition dpos, TypeParameter constrainedTp | + accessDeclarationPositionMatch(apos, dpos) and + constrainedTp = target.getTypeParameter(_) and + tp = target.getTypeParameter(_) and + constrainedTp != tp and + constrainedTp = target.getDeclaredType(dpos, pathToConstrained) and + exists(TypeMention tm | + tm = getATypeParameterConstraint(constrainedTp) and + tm.resolveTypeAt(pathToTp) = tp and + constraint = resolveTypeMentionRoot(tm) + ) ) } @@ -1409,15 +1406,9 @@ module Make1 Input1> { Access a, Declaration target, TypePath path, Type t, TypeParameter tp ) { not exists(getTypeArgument(a, target, tp, _)) and - target = a.getTarget() and - exists( - Type constraint, AccessPosition apos, DeclarationPosition dpos, TypePath pathToTp, - TypePath pathToTp2 - | - accessDeclarationPositionMatch(apos, dpos) and - typeParameterConstraintHasTypeParameter(target, dpos, pathToTp2, _, constraint, pathToTp, - tp) and - AccessConstraint::satisfiesConstraintType(a, apos, pathToTp2, constraint, + exists(Type constraint, AccessPosition apos, TypePath pathToTp, TypePath pathToTp2 | + typeParameterConstraintHasTypeParameter(target, apos, pathToTp2, constraint, pathToTp, tp) and + AccessConstraint::satisfiesConstraintType(a, target, apos, pathToTp2, constraint, pathToTp.appendInverse(path), t) ) } From bdcecdfc2cf636d3f7455ca8a35cb270d11b8000 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Thu, 17 Jul 2025 13:55:04 +0200 Subject: [PATCH 2/3] Shared, Rust: Ensure that the constraints in `satisfiesConstraintType` are in `relevantConstraint` --- .../codeql/typeinference/internal/TypeInference.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index 951cc02f8ad2..7f78bea7d5da 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -989,7 +989,7 @@ module Make1 Input1> { path = prefix0.append(suffix) ) or - tt.getTypeAt(TypePath::nil()) = constraint and + hasTypeConstraint(tt, constraint, constraint) and t = tt.getTypeAt(path) } } From 43b2977cb48fd0c28fcf67d7e6015976aa08ce6c Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Thu, 17 Jul 2025 14:28:04 +0200 Subject: [PATCH 3/3] Shared, Rust: Reuse `hasTypeConstraint` in `potentialInstantiationOf` and factor out `multipleConstraintImplementations` --- .../typeinference/internal/TypeInference.qll | 29 ++++++++++++------- 1 file changed, 18 insertions(+), 11 deletions(-) diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index 7f78bea7d5da..1eaf6ef8e840 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -796,6 +796,14 @@ module Make1 Input1> { ) } + /** + * Holds if there is multiple ways in which a type with `conditionRoot` at + * the root can satisfy a constraint with `constraintRoot` at the root. + */ + predicate multipleConstraintImplementations(Type conditionRoot, Type constraintRoot) { + countConstraintImplementations(conditionRoot, constraintRoot) > 1 + } + /** * Holds if `baseMention` is a (transitive) base type mention of `sub`, * and `t` is mentioned (implicitly) at `path` inside `baseMention`. For @@ -902,14 +910,20 @@ module Make1 Input1> { { private import Input + /** Holds if the type tree has the type `type` and should satisfy `constraint`. */ + pragma[nomagic] + private predicate hasTypeConstraint(HasTypeTree term, Type type, Type constraint) { + type = term.getTypeAt(TypePath::nil()) and + relevantConstraint(term, constraint) + } + private module IsInstantiationOfInput implements IsInstantiationOfInputSig { predicate potentialInstantiationOf(HasTypeTree tt, TypeAbstraction abs, TypeMention cond) { exists(Type constraint, Type type | - type = tt.getTypeAt(TypePath::nil()) and - relevantConstraint(tt, constraint) and + hasTypeConstraint(tt, type, constraint) and rootTypesSatisfaction(type, constraint, abs, cond, _) and // We only need to check instantiations where there are multiple candidates. - countConstraintImplementations(type, constraint) > 1 + multipleConstraintImplementations(type, constraint) ) } @@ -918,13 +932,6 @@ module Make1 Input1> { } } - /** Holds if the type tree has the type `type` and should satisfy `constraint`. */ - pragma[nomagic] - private predicate hasTypeConstraint(HasTypeTree term, Type type, Type constraint) { - type = term.getTypeAt(TypePath::nil()) and - relevantConstraint(term, constraint) - } - /** * Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`. */ @@ -944,7 +951,7 @@ module Make1 Input1> { // When there are multiple ways the type could implement the // constraint we need to find the right implementation, which is the // one where the type instantiates the precondition. - if countConstraintImplementations(type, constraint) > 1 + if multipleConstraintImplementations(type, constraint) then IsInstantiationOf::isInstantiationOf(tt, abs, sub) else any()