From a4e5c79c1af0cb5fd7fc7d9f6b241d476428839a 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 | 32 ++++- .../internal/typeinference/TypeInference.qll | 28 ++++- .../type-inference/type-inference.expected | 7 +- .../typeinference/internal/TypeInference.qll | 109 ++++++++++++++++-- 4 files changed, 152 insertions(+), 24 deletions(-) diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll index d217fc3760a9..1adedf0067de 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll @@ -84,9 +84,33 @@ 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 + predicate implHasAmbiguousSiblingAt( + ImplItemNode impl, ImplItemNode impl2, Trait trait, TypePath path + ) { + // impl.fromSource() and + exists(Type t1, Type t2 | + ( + implSiblings(trait, impl, impl2) + or + exists(Type rootType, AstNode selfTy1, AstNode selfTy2 | + implSiblingCandidate(impl, trait, rootType, selfTy1) and + implSiblingCandidate(impl2, trait, rootType, selfTy2) and + impl != impl2 + | + // 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. + forex(TypePath path1, Type t1_ | t1_ = resolveNonTypeParameterTypeAt(selfTy1, path1) | + not t1_ != resolveNonTypeParameterTypeAt(selfTy2, path1) + ) + or + forex(TypePath path2, Type t2_ | t2_ = resolveNonTypeParameterTypeAt(selfTy2, path2) | + not t2_ != resolveNonTypeParameterTypeAt(selfTy1, path2) + ) + ) + ) and t1 = resolveTypeMentionAt(impl.getTraitPath(), path) and t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) and t1 != t2 @@ -103,7 +127,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) diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll b/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll index c6a268be126f..f6d2b15b91ea 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 = @@ -2143,6 +2150,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 @@ -4034,7 +4052,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 4be703598427..690c40c174c6 100644 --- a/rust/ql/test/library-tests/type-inference/type-inference.expected +++ b/rust/ql/test/library-tests/type-inference/type-inference.expected @@ -15810,18 +15810,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 | @@ -15853,3 +15847,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 888ca65fa98a..4f406f6cf7dd 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