From f7213759f7192926eea5e89be22ea46e61651191 Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Fri, 27 Mar 2026 11:50:37 +0100 Subject: [PATCH 1/3] Rust: Refine `implHasAmbiguousSiblingAt` --- .../typeinference/FunctionOverloading.qll | 99 ++++++++-------- .../internal/typeinference/TypeInference.qll | 28 ++++- .../type-inference/type-inference.expected | 8 +- .../typeinference/internal/TypeInference.qll | 109 ++++++++++++++++-- 4 files changed, 178 insertions(+), 66 deletions(-) diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll index ec0152c7ecae..6e6c538543d6 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll @@ -28,11 +28,8 @@ private module MkSiblingImpls { not result instanceof TypeParameter } - bindingset[t1, t2] - private predicate typeMentionEqual(AstNode t1, AstNode t2) { - forex(TypePath path, Type type | resolveNonTypeParameterTypeAt(t1, path) = type | - resolveNonTypeParameterTypeAt(t2, path) = type - ) + private class Tm extends AstNode { + Type getTypeAt(TypePath path) { result = resolveTypeMentionAt(this, path) } } pragma[nomagic] @@ -50,6 +47,18 @@ private module MkSiblingImpls { trait = impl.resolveTraitTy() } + private module FooIsInstantiationOfInput implements IsInstantiationOfInputSig { + predicate potentialInstantiationOf(Tm cond, TypeAbstraction abs, Tm constraint) { + exists(TraitItemNode trait, Type rootType | + implSiblingCandidate(_, trait, rootType, cond) and + implSiblingCandidate(abs, trait, rootType, constraint) and + cond != constraint + ) + } + } + + private module FooIsInstantiationOf = IsInstantiationOf; + /** * Holds if `impl1` and `impl2` are sibling implementations of `trait`. We * consider implementations to be siblings if they implement the same trait for @@ -59,23 +68,19 @@ private module MkSiblingImpls { */ pragma[inline] predicate implSiblings(TraitItemNode trait, Impl impl1, Impl impl2) { - impl1 != impl2 and - ( - exists(Type rootType, AstNode selfTy1, AstNode selfTy2 | - implSiblingCandidate(impl1, trait, rootType, selfTy1) and - implSiblingCandidate(impl2, trait, rootType, selfTy2) and - // In principle the second conjunct below should be superfluous, but we still - // have ill-formed type mentions for types that we don't understand. For - // those checking both directions restricts further. Note also that we check - // syntactic equality, whereas equality up to renaming would be more - // correct. - typeMentionEqual(selfTy1, selfTy2) and - typeMentionEqual(selfTy2, selfTy1) - ) - or - blanketImplSiblingCandidate(impl1, trait) and - blanketImplSiblingCandidate(impl2, trait) + // impl1.fromSource() and + // impl1 instanceof Builtins::BuiltinImpl and + exists(Type rootType, AstNode selfTy1, AstNode selfTy2 | + implSiblingCandidate(impl1, trait, rootType, selfTy1) and + implSiblingCandidate(impl2, trait, rootType, selfTy2) + | + FooIsInstantiationOf::isInstantiationOf(selfTy1, impl2, selfTy2) or + FooIsInstantiationOf::isInstantiationOf(selfTy2, impl1, selfTy1) ) + or + blanketImplSiblingCandidate(impl1, trait) and + blanketImplSiblingCandidate(impl2, trait) and + impl1 != impl2 } /** @@ -86,24 +91,32 @@ private module MkSiblingImpls { predicate implHasSibling(ImplItemNode impl, Trait trait) { implSiblings(trait, impl, _) } pragma[nomagic] - predicate implHasAmbiguousSiblingAt(ImplItemNode impl, Trait trait, TypePath path) { - exists(ImplItemNode impl2, Type t1, Type t2 | - implSiblings(trait, impl, impl2) and - t1 = resolveTypeMentionAt(impl.getTraitPath(), path) and - t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) and - t1 != t2 - | - not t1 instanceof TypeParameter or - not t2 instanceof TypeParameter + predicate implHasAmbiguousSiblingAt( + ImplItemNode impl, ImplItemNode impl2, Trait trait, TypePath path + ) { + // impl instanceof Builtins::BuiltinImpl and + exists(Type t | implSiblings(trait, impl, impl2) | + t = resolveTypeMentionAt(impl.getTraitPath(), path) and + not (t = resolveTypeMentionAt(impl2.getTraitPath(), path) and not t instanceof TypeParameter) + or + t = resolveTypeMentionAt(impl2.getTraitPath(), path) and + not (t = resolveTypeMentionAt(impl.getTraitPath(), path) and not t instanceof TypeParameter) + // and + // t1 = resolveTypeMentionAt(impl.getTraitPath(), path) and + // t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) and + // t1 != t2 + // | + // not t1 instanceof TypeParameter or + // not t2 instanceof TypeParameter ) - or - // todo: handle blanket/non-blanket siblings in `implSiblings` - trait = - any(IndexTrait it | - implSiblingCandidate(impl, it, _, _) and - impl instanceof Builtins::BuiltinImpl and - path = TypePath::singleton(TAssociatedTypeTypeParameter(trait, it.getOutputType())) - ) + // or + // // todo: handle blanket/non-blanket siblings in `implSiblings` + // trait = + // any(IndexTrait it | + // implSiblingCandidate(impl, it, _, _) and + // impl instanceof Builtins::BuiltinImpl and + // path = TypePath::singleton(TAssociatedTypeTypeParameter(trait, it.getOutputType())) + // ) } } @@ -113,7 +126,7 @@ private Type resolvePreTypeMention(AstNode tm, TypePath path) { private module PreSiblingImpls = MkSiblingImpls; -predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/3; +predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/4; private Type resolveTypeMention(AstNode tm, TypePath path) { result = tm.(TypeMention).getTypeAt(path) @@ -152,7 +165,7 @@ private predicate functionResolutionDependsOnArgumentCand( * ```rust * trait MyTrait { * fn method(&self, value: Foo) -> Self; - * // ^^^^^^^^^^^^^ `pos` = 0 + * // ^^^^^^^^^^^^^ `pos` = 1 * // ^ `path` = "T" * } * impl MyAdd for i64 { @@ -160,11 +173,6 @@ private predicate functionResolutionDependsOnArgumentCand( * // ^^^ `type` = i64 * } * ``` - * - * Note that we only check the root type symbol at the position. If the type - * at that position is a type constructor (for instance `Vec<..>`) then - * inspecting the entire type tree could be necessary to disambiguate the - * method. In that case we will still resolve several methods. */ exists(TraitItemNode trait | @@ -262,6 +270,7 @@ pragma[nomagic] predicate functionResolutionDependsOnArgument( ImplItemNode impl, Function f, TypeParameter traitTp, FunctionPosition pos ) { + // impl.fromSource() and exists(string functionName | functionResolutionDependsOnArgumentCand(impl, f, functionName, traitTp, pos, _) | diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll b/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll index 6c0034c2b9c7..cd8d3c281da6 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll @@ -37,6 +37,11 @@ private module Input1 implements InputSig1 { class Type = T::Type; + predicate isPseudoType(Type t) { + t instanceof UnknownType or + t instanceof NeverType + } + class TypeParameter = T::TypeParameter; class TypeAbstraction = TA::TypeAbstraction; @@ -230,9 +235,10 @@ private module PreInput2 implements InputSig2 { } predicate typeAbstractionHasAmbiguousConstraintAt( - TypeAbstraction abs, Type constraint, TypePath path + TypeAbstraction abs, Type constraint, TypeAbstraction other, TypePath path ) { - FunctionOverloading::preImplHasAmbiguousSiblingAt(abs, constraint.(TraitType).getTrait(), path) + FunctionOverloading::preImplHasAmbiguousSiblingAt(abs, other, constraint.(TraitType).getTrait(), + path) } predicate typeParameterIsFunctionallyDetermined = @@ -256,9 +262,10 @@ private module Input2 implements InputSig2 { } predicate typeAbstractionHasAmbiguousConstraintAt( - TypeAbstraction abs, Type constraint, TypePath path + TypeAbstraction abs, Type constraint, TypeAbstraction other, TypePath path ) { - FunctionOverloading::implHasAmbiguousSiblingAt(abs, constraint.(TraitType).getTrait(), path) + FunctionOverloading::implHasAmbiguousSiblingAt(abs, other, constraint.(TraitType).getTrait(), + path) } predicate typeParameterIsFunctionallyDetermined = @@ -1925,6 +1932,17 @@ private module AssocFunctionResolution { ) } + // private AssocFunctionDeclaration testresolveCallTarget( + // ImplOrTraitItemNode i, FunctionPosition selfPos, DerefChain derefChain, BorrowKind borrow, + // FunctionPosition pos, TypePath path, Type t + // ) { + // this = Debug::getRelevantLocatable() and + // exists(AssocFunctionCallCand afcc | + // afcc = MkAssocFunctionCallCand(this, selfPos, derefChain, borrow) and + // result = afcc.resolveCallTarget(i) and + // t = result.getParameterType(any(ImplOrTraitItemNodeOption o | o.asSome() = i), pos, path) + // ) + // } /** * Holds if the argument `arg` of this call has been implicitly dereferenced * and borrowed according to `derefChain` and `borrow`, in order to be able to @@ -3942,7 +3960,7 @@ private module Debug { exists(string filepath, int startline, int startcolumn, int endline, int endcolumn | result.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and filepath.matches("%/main.rs") and - startline = 103 + startline = 441 ) } diff --git a/rust/ql/test/library-tests/type-inference/type-inference.expected b/rust/ql/test/library-tests/type-inference/type-inference.expected index 5e870ae6ca5d..c846a1368e7d 100644 --- a/rust/ql/test/library-tests/type-inference/type-inference.expected +++ b/rust/ql/test/library-tests/type-inference/type-inference.expected @@ -11605,7 +11605,6 @@ inferType | main.rs:2223:9:2223:31 | ... .my_add(...) | T | main.rs:2107:5:2107:19 | S | | main.rs:2223:9:2223:31 | ... .my_add(...) | T.T | main.rs:2109:10:2109:17 | T::Output[MyAdd] | | main.rs:2223:9:2223:31 | ... .my_add(...) | T.T | main.rs:2118:10:2118:17 | T::Output[MyAdd] | -| main.rs:2223:9:2223:31 | ... .my_add(...) | T.T | main.rs:2127:14:2127:14 | T::Output[MyAdd] | | main.rs:2223:11:2223:14 | 1i64 | | {EXTERNAL LOCATION} | i64 | | main.rs:2223:24:2223:30 | S(...) | | main.rs:2107:5:2107:19 | S | | main.rs:2223:24:2223:30 | S(...) | T | {EXTERNAL LOCATION} | i64 | @@ -15818,18 +15817,12 @@ inferType | regressions.rs:150:24:153:5 | { ... } | | regressions.rs:136:5:136:22 | S2 | | regressions.rs:150:24:153:5 | { ... } | T2 | regressions.rs:135:5:135:14 | S1 | | regressions.rs:151:13:151:13 | x | | regressions.rs:136:5:136:22 | S2 | -| regressions.rs:151:13:151:13 | x | T2 | {EXTERNAL LOCATION} | & | | regressions.rs:151:13:151:13 | x | T2 | regressions.rs:135:5:135:14 | S1 | -| regressions.rs:151:13:151:13 | x | T2.TRef | regressions.rs:135:5:135:14 | S1 | | regressions.rs:151:17:151:18 | S1 | | regressions.rs:135:5:135:14 | S1 | | regressions.rs:151:17:151:25 | S1.into() | | regressions.rs:136:5:136:22 | S2 | -| regressions.rs:151:17:151:25 | S1.into() | T2 | {EXTERNAL LOCATION} | & | | regressions.rs:151:17:151:25 | S1.into() | T2 | regressions.rs:135:5:135:14 | S1 | -| regressions.rs:151:17:151:25 | S1.into() | T2.TRef | regressions.rs:135:5:135:14 | S1 | | regressions.rs:152:9:152:9 | x | | regressions.rs:136:5:136:22 | S2 | -| regressions.rs:152:9:152:9 | x | T2 | {EXTERNAL LOCATION} | & | | regressions.rs:152:9:152:9 | x | T2 | regressions.rs:135:5:135:14 | S1 | -| regressions.rs:152:9:152:9 | x | T2.TRef | regressions.rs:135:5:135:14 | S1 | | regressions.rs:164:16:164:19 | SelfParam | | regressions.rs:158:5:158:19 | S | | regressions.rs:164:16:164:19 | SelfParam | T | regressions.rs:160:10:160:10 | T | | regressions.rs:164:22:164:25 | _rhs | | regressions.rs:158:5:158:19 | S | @@ -15861,3 +15854,4 @@ inferType | regressions.rs:179:24:179:27 | S(...) | T | {EXTERNAL LOCATION} | i32 | | regressions.rs:179:26:179:26 | 1 | | {EXTERNAL LOCATION} | i32 | testFailures +| regressions.rs:152:11:152:127 | //... | Fixed spurious result: type=x:T2.TRef.S1 | diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index 9f4be49d878a..42f2503b4d31 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -145,6 +145,8 @@ signature module InputSig1 { Location getLocation(); } + predicate isPseudoType(Type t); + /** A type parameter. */ class TypeParameter extends Type; @@ -413,7 +415,7 @@ module Make1 Input1> { * not at the path `"T2"`. */ predicate typeAbstractionHasAmbiguousConstraintAt( - TypeAbstraction abs, Type constraint, TypePath path + TypeAbstraction abs, Type constraint, TypeAbstraction other, TypePath path ); /** @@ -648,8 +650,22 @@ module Make1 Input1> { t = getTypeAt(app, abs, constraint, path) and not t = abs.getATypeParameter() and app.getTypeAt(path) = t2 and + not isPseudoType(t2) and t2 != t ) + or + // satisfiesConcreteTypes(app, abs, constraint) and + exists(TypeParameter tp, TypePath path2, Type t, Type t2 | + tp = getTypeAt(app, abs, constraint, path) and + tp = getTypeAt(app, abs, constraint, path2) and + tp = abs.getATypeParameter() and + path != path2 and + app.getTypeAt(path) = t and + app.getTypeAt(path2) = t2 and + not isPseudoType(t) and + not isPseudoType(t2) and + t != t2 + ) } } @@ -1004,17 +1020,92 @@ module Make1 Input1> { ) { exists(Type constraintRoot | hasConstraintMention(term, abs, sub, constraint, constraintRoot, constraintMention) and - conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t) and - if - exists(TypePath prefix | - typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, prefix) and - prefix.isPrefixOf(path) - ) - then ambiguous = true - else ambiguous = false + conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t) + | + exists(TypePath prefix, TypeAbstraction other | + typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and + prefix.isPrefixOf(path) and + hasConstraintMention(term, other, _, _, constraintRoot, _) + ) and + ambiguous = true + or + forall(TypePath prefix, TypeAbstraction other | + typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) + | + not prefix.isPrefixOf(path) + or + TermIsInstantiationOfCondition::isNotInstantiationOf(term, other, _, _) + ) and + ambiguous = false ) } + // private predicate testsatisfiesConstraintTypeMention0( + // Term term, Constraint constraint, TypeMention constraintMention, TypeAbstraction abs, + // TypeMention sub, TypePath path, Type t, boolean ambiguous + // ) { + // exists(string filepath, int startline, int startcolumn, int endline, int endcolumn | + // term.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and + // filepath.matches("%/main.rs") and + // startline = 435 + // ) and + // satisfiesConstraintTypeMention0(term, constraint, constraintMention, abs, sub, path, t, + // ambiguous) + // } + // private predicate testsatisfiesConstraintTypeMention1( + // Term term, Constraint constraint, TypeMention constraintMention, TypeAbstraction abs, + // TypeMention sub, TypePath path, Type t, boolean ambiguous, TypePath prefix, + // TypeAbstraction other, TypePath path2 + // ) { + // exists(string filepath, int startline, int startcolumn, int endline, int endcolumn | + // term.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and + // filepath.matches("%/main.rs") and + // startline = 435 + // ) and + // exists(Type constraintRoot | + // hasConstraintMention(term, abs, sub, constraint, constraintRoot, constraintMention) and + // conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t) + // | + // // if + // // exists(TypePath prefix, TypeAbstraction other | + // // typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and + // // prefix.isPrefixOf(path) + // // ) + // // then ambiguous = true + // // else ambiguous = false + // typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and + // // isNotInstantiationOf(term, other, _, constraintRoot) and + // // TermIsInstantiationOfConditionInput::potentialInstantiationOf(term, other, _) and + // prefix.isPrefixOf(path) and + // TermIsInstantiationOfCondition::isNotInstantiationOf(term, other, _, path2) and + // // not isNotInstantiationOf(term, other, _, constraintRoot) and + // ambiguous = false + // // exists(TypePath prefix, TypeAbstraction other | + // // typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and + // // prefix.isPrefixOf(path) and + // // hasConstraintMention(term, other, _, _, constraintRoot, _) + // // ) and + // // ambiguous = true + // // or + // // forall(TypePath prefix, TypeAbstraction other | + // // typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) + // // | + // // not prefix.isPrefixOf(path) + // // or + // // // exists(Type type | hasTypeConstraint(term, type, constraint, constraintRoot) | + // // // // countConstraintImplementations(type, constraintRoot) = 0 + // // // // or + // // // // not rootTypesSatisfaction(type, constraintRoot, _, _, _) + // // // // or + // // // multipleConstraintImplementations(type, constraintRoot) and + // // // isNotInstantiationOf(term, other, _, constraintRoot) + // // // ) + // // isNotInstantiationOf(term, other, _, constraintRoot) + // // // TermIsInstantiationOfCondition::isNotInstantiationOf(term, other, _, _) + // // ) and + // // ambiguous = false + // ) + // } pragma[nomagic] private predicate conditionSatisfiesConstraintTypeAtForDisambiguation( TypeAbstraction abs, TypeMention condition, TypeMention constraint, TypePath path, Type t From 5b1d0a42b227d36d68d5dd48f874ff06610b156f Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Thu, 16 Apr 2026 19:59:30 +0200 Subject: [PATCH 2/3] wip --- .../typeinference/FunctionOverloading.qll | 11 +++- .../type-inference/type-inference.expected | 3 ++ .../typeinference/internal/TypeInference.qll | 52 ++++++++++++++----- 3 files changed, 50 insertions(+), 16 deletions(-) diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll index 6e6c538543d6..784fced0c237 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll @@ -97,10 +97,17 @@ private module MkSiblingImpls { // impl instanceof Builtins::BuiltinImpl and exists(Type t | implSiblings(trait, impl, impl2) | t = resolveTypeMentionAt(impl.getTraitPath(), path) and - not (t = resolveTypeMentionAt(impl2.getTraitPath(), path) and not t instanceof TypeParameter) + forall(Type t2 | t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) | + t != t2 and + (not t instanceof TypeParameter or not t2 instanceof TypeParameter) + ) or t = resolveTypeMentionAt(impl2.getTraitPath(), path) and - not (t = resolveTypeMentionAt(impl.getTraitPath(), path) and not t instanceof TypeParameter) + // not (t = resolveTypeMentionAt(impl.getTraitPath(), path) and not t instanceof TypeParameter) + forall(Type t2 | t2 = resolveTypeMentionAt(impl.getTraitPath(), path) | + t != t2 and + (not t instanceof TypeParameter or not t2 instanceof TypeParameter) + ) // and // t1 = resolveTypeMentionAt(impl.getTraitPath(), path) and // t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) and diff --git a/rust/ql/test/library-tests/type-inference/type-inference.expected b/rust/ql/test/library-tests/type-inference/type-inference.expected index c846a1368e7d..7541d47c9e2f 100644 --- a/rust/ql/test/library-tests/type-inference/type-inference.expected +++ b/rust/ql/test/library-tests/type-inference/type-inference.expected @@ -11605,6 +11605,7 @@ inferType | main.rs:2223:9:2223:31 | ... .my_add(...) | T | main.rs:2107:5:2107:19 | S | | main.rs:2223:9:2223:31 | ... .my_add(...) | T.T | main.rs:2109:10:2109:17 | T::Output[MyAdd] | | main.rs:2223:9:2223:31 | ... .my_add(...) | T.T | main.rs:2118:10:2118:17 | T::Output[MyAdd] | +| main.rs:2223:9:2223:31 | ... .my_add(...) | T.T | main.rs:2127:14:2127:14 | T::Output[MyAdd] | | main.rs:2223:11:2223:14 | 1i64 | | {EXTERNAL LOCATION} | i64 | | main.rs:2223:24:2223:30 | S(...) | | main.rs:2107:5:2107:19 | S | | main.rs:2223:24:2223:30 | S(...) | T | {EXTERNAL LOCATION} | i64 | @@ -11899,8 +11900,10 @@ inferType | main.rs:2311:26:2311:27 | .. | | {EXTERNAL LOCATION} | RangeFull | | main.rs:2312:9:2312:51 | for ... in ... { ... } | | {EXTERNAL LOCATION} | () | | main.rs:2312:18:2312:48 | &... | | {EXTERNAL LOCATION} | & | +| main.rs:2312:18:2312:48 | &... | TRef | {EXTERNAL LOCATION} | i64 | | main.rs:2312:19:2312:36 | [...] | | {EXTERNAL LOCATION} | [;] | | main.rs:2312:19:2312:36 | [...] | TArray | {EXTERNAL LOCATION} | i64 | +| main.rs:2312:19:2312:48 | ...[range_full] | | {EXTERNAL LOCATION} | i64 | | main.rs:2312:20:2312:23 | 1i64 | | {EXTERNAL LOCATION} | i64 | | main.rs:2312:26:2312:29 | 2i64 | | {EXTERNAL LOCATION} | i64 | | main.rs:2312:32:2312:35 | 3i64 | | {EXTERNAL LOCATION} | i64 | diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index 42f2503b4d31..dc74c20b5835 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -626,6 +626,37 @@ module Make1 Input1> { ) } + pragma[nomagic] + private predicate hasTypeParameterAt( + App app, TypeAbstraction abs, Constraint constraint, TypePath path, TypeParameter tp + ) { + tp = getTypeAt(app, abs, constraint, path) and + tp = abs.getATypeParameter() + } + + pragma[nomagic] + private predicate hasTypeParameterAt2( + App app, TypeAbstraction abs, Constraint constraint, TypePath path1, TypePath path2 + ) { + exists(TypeParameter tp | + hasTypeParameterAt(app, abs, constraint, path1, tp) and + hasTypeParameterAt(app, abs, constraint, path2, tp) and + path1 != path2 + ) + } + + private Type getNonPseudoTypeAt(App app, TypePath path) { + result = app.getTypeAt(path) and not isPseudoType(result) + } + + pragma[nomagic] + private Type getNonPseudoTypeAt2( + App app, TypeAbstraction abs, Constraint constraint, TypeParameter tp, TypePath path + ) { + hasTypeParameterAt(app, abs, constraint, path, tp) and + result = getNonPseudoTypeAt(app, path) + } + /** * Holds if `app` is _not_ a possible instantiation of `constraint`, because `app` * and `constraint` differ on concrete types at `path`. @@ -649,22 +680,16 @@ module Make1 Input1> { exists(Type t, Type t2 | t = getTypeAt(app, abs, constraint, path) and not t = abs.getATypeParameter() and - app.getTypeAt(path) = t2 and - not isPseudoType(t2) and + t2 = getNonPseudoTypeAt(app, path) and t2 != t ) or // satisfiesConcreteTypes(app, abs, constraint) and exists(TypeParameter tp, TypePath path2, Type t, Type t2 | - tp = getTypeAt(app, abs, constraint, path) and - tp = getTypeAt(app, abs, constraint, path2) and - tp = abs.getATypeParameter() and - path != path2 and - app.getTypeAt(path) = t and - app.getTypeAt(path2) = t2 and - not isPseudoType(t) and - not isPseudoType(t2) and - t != t2 + t = getNonPseudoTypeAt2(app, abs, constraint, tp, path) and + t2 = getNonPseudoTypeAt2(app, abs, constraint, tp, path2) and + t != t2 and + path != path2 ) } } @@ -1030,10 +1055,9 @@ module Make1 Input1> { ambiguous = true or forall(TypePath prefix, TypeAbstraction other | - typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) + typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and + prefix.isPrefixOf(path) | - not prefix.isPrefixOf(path) - or TermIsInstantiationOfCondition::isNotInstantiationOf(term, other, _, _) ) and ambiguous = false From 383e7b6d103b8b275198cd196bfcb3efa184980c Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Mon, 20 Apr 2026 15:17:53 +0200 Subject: [PATCH 3/3] wip2 --- .../typeinference/FunctionOverloading.qll | 50 ++++++------------- .../type-inference/type-inference.expected | 2 - .../typeinference/internal/TypeInference.qll | 39 ++++++++++----- 3 files changed, 42 insertions(+), 49 deletions(-) diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll index 784fced0c237..f152bb7052dd 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll @@ -22,12 +22,6 @@ private signature Type resolveTypeMentionAtSig(AstNode tm, TypePath path); * how to resolve type mentions (`PreTypeMention` vs. `TypeMention`). */ private module MkSiblingImpls { - pragma[nomagic] - private Type resolveNonTypeParameterTypeAt(AstNode tm, TypePath path) { - result = resolveTypeMentionAt(tm, path) and - not result instanceof TypeParameter - } - private class Tm extends AstNode { Type getTypeAt(TypePath path) { result = resolveTypeMentionAt(this, path) } } @@ -95,35 +89,23 @@ private module MkSiblingImpls { ImplItemNode impl, ImplItemNode impl2, Trait trait, TypePath path ) { // impl instanceof Builtins::BuiltinImpl and - exists(Type t | implSiblings(trait, impl, impl2) | - t = resolveTypeMentionAt(impl.getTraitPath(), path) and - forall(Type t2 | t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) | - t != t2 and - (not t instanceof TypeParameter or not t2 instanceof TypeParameter) - ) - or - t = resolveTypeMentionAt(impl2.getTraitPath(), path) and - // not (t = resolveTypeMentionAt(impl.getTraitPath(), path) and not t instanceof TypeParameter) - forall(Type t2 | t2 = resolveTypeMentionAt(impl.getTraitPath(), path) | - t != t2 and - (not t instanceof TypeParameter or not t2 instanceof TypeParameter) - ) - // and - // t1 = resolveTypeMentionAt(impl.getTraitPath(), path) and - // t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) and - // t1 != t2 - // | - // not t1 instanceof TypeParameter or - // not t2 instanceof TypeParameter + exists(Type t1, Type t2 | + implSiblings(trait, impl, impl2) and + t1 = resolveTypeMentionAt(impl.getTraitPath(), path) and + t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) and + t1 != t2 + | + not t1 instanceof TypeParameter or + not t2 instanceof TypeParameter ) - // or - // // todo: handle blanket/non-blanket siblings in `implSiblings` - // trait = - // any(IndexTrait it | - // implSiblingCandidate(impl, it, _, _) and - // impl instanceof Builtins::BuiltinImpl and - // path = TypePath::singleton(TAssociatedTypeTypeParameter(trait, it.getOutputType())) - // ) + or + // todo: handle blanket/non-blanket siblings in `implSiblings` + trait = + any(IndexTrait it | + implSiblingCandidate(impl, it, _, _) and + impl instanceof Builtins::BuiltinImpl and + path = TypePath::singleton(TAssociatedTypeTypeParameter(trait, it.getOutputType())) + ) } } diff --git a/rust/ql/test/library-tests/type-inference/type-inference.expected b/rust/ql/test/library-tests/type-inference/type-inference.expected index 7541d47c9e2f..7aa649184949 100644 --- a/rust/ql/test/library-tests/type-inference/type-inference.expected +++ b/rust/ql/test/library-tests/type-inference/type-inference.expected @@ -11900,10 +11900,8 @@ inferType | main.rs:2311:26:2311:27 | .. | | {EXTERNAL LOCATION} | RangeFull | | main.rs:2312:9:2312:51 | for ... in ... { ... } | | {EXTERNAL LOCATION} | () | | main.rs:2312:18:2312:48 | &... | | {EXTERNAL LOCATION} | & | -| main.rs:2312:18:2312:48 | &... | TRef | {EXTERNAL LOCATION} | i64 | | main.rs:2312:19:2312:36 | [...] | | {EXTERNAL LOCATION} | [;] | | main.rs:2312:19:2312:36 | [...] | TArray | {EXTERNAL LOCATION} | i64 | -| main.rs:2312:19:2312:48 | ...[range_full] | | {EXTERNAL LOCATION} | i64 | | main.rs:2312:20:2312:23 | 1i64 | | {EXTERNAL LOCATION} | i64 | | main.rs:2312:26:2312:29 | 2i64 | | {EXTERNAL LOCATION} | i64 | | main.rs:2312:32:2312:35 | 3i64 | | {EXTERNAL LOCATION} | i64 | diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index dc74c20b5835..aae70ae8ecc5 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -634,17 +634,6 @@ module Make1 Input1> { tp = abs.getATypeParameter() } - pragma[nomagic] - private predicate hasTypeParameterAt2( - App app, TypeAbstraction abs, Constraint constraint, TypePath path1, TypePath path2 - ) { - exists(TypeParameter tp | - hasTypeParameterAt(app, abs, constraint, path1, tp) and - hasTypeParameterAt(app, abs, constraint, path2, tp) and - path1 != path2 - ) - } - private Type getNonPseudoTypeAt(App app, TypePath path) { result = app.getTypeAt(path) and not isPseudoType(result) } @@ -1038,6 +1027,29 @@ module Make1 Input1> { ) } + private module TermIsInstantiationOfConditionInput2 implements + IsInstantiationOfInputSig + { + predicate potentialInstantiationOf(Term term, TypeAbstraction abs, TypeMention cond) { + TermIsInstantiationOfConditionInput::potentialInstantiationOf(term, abs, cond) and + exists( + TypeMention sub, Type constraintRoot, TypeMention constraintMention, + TypeAbstraction abs2 + | + hasConstraintMention(term, abs2, sub, _, constraintRoot, constraintMention) and + conditionSatisfiesConstraintTypeAt(abs2, sub, constraintMention, _, _) and + typeAbstractionHasAmbiguousConstraintAt(abs2, constraintRoot, abs, _) + ) + } + + predicate relevantConstraint(TypeMention constraint) { + TermIsInstantiationOfConditionInput::relevantConstraint(constraint) + } + } + + private module TermIsInstantiationOfCondition2 = + IsInstantiationOf; + pragma[nomagic] private predicate satisfiesConstraintTypeMention0( Term term, Constraint constraint, TypeMention constraintMention, TypeAbstraction abs, @@ -1050,7 +1062,8 @@ module Make1 Input1> { exists(TypePath prefix, TypeAbstraction other | typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and prefix.isPrefixOf(path) and - hasConstraintMention(term, other, _, _, constraintRoot, _) + TermIsInstantiationOfCondition2::isInstantiationOf(term, other, _) + // hasConstraintMention(term, other, _, _, constraintRoot, _) ) and ambiguous = true or @@ -1058,7 +1071,7 @@ module Make1 Input1> { typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and prefix.isPrefixOf(path) | - TermIsInstantiationOfCondition::isNotInstantiationOf(term, other, _, _) + TermIsInstantiationOfCondition2::isNotInstantiationOf(term, other, _, _) ) and ambiguous = false )