From f7b803da0c4e34ba630ab5646e2843f8ff5a01ec Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Fri, 27 Mar 2026 11:50:37 +0100 Subject: [PATCH] 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