Skip to content

Rust: Refine implHasAmbiguousSiblingAt #21703

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

Draft
hvitved wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

Rust: Refine implHasAmbiguousSiblingAt #21703

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
99 changes: 54 additions & 45 deletions rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,11 +28,8 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
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]
Expand All @@ -50,6 +47,18 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
trait = impl.resolveTraitTy()
}

private module FooIsInstantiationOfInput implements IsInstantiationOfInputSig<Tm, Tm> {
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<Tm, Tm, FooIsInstantiationOfInput>;

/**
* Holds if `impl1` and `impl2` are sibling implementations of `trait`. We
* consider implementations to be siblings if they implement the same trait for
Expand All @@ -59,23 +68,19 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
*/
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
}

/**
Expand All @@ -86,24 +91,32 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
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()))
// )
}
}

Expand All @@ -113,7 +126,7 @@ private Type resolvePreTypeMention(AstNode tm, TypePath path) {

private module PreSiblingImpls = MkSiblingImpls<resolvePreTypeMention/2>;

predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/3;
predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/4;

private Type resolveTypeMention(AstNode tm, TypePath path) {
result = tm.(TypeMention).getTypeAt(path)
Expand Down Expand Up @@ -152,19 +165,14 @@ private predicate functionResolutionDependsOnArgumentCand(
* ```rust
* trait MyTrait<T> {
* fn method(&self, value: Foo<T>) -> Self;
* // ^^^^^^^^^^^^^ `pos` = 0
* // ^^^^^^^^^^^^^ `pos` = 1
* // ^ `path` = "T"
* }
* impl MyAdd<i64> for i64 {
* fn method(&self, value: Foo<i64>) -> Self { ... }
* // ^^^ `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 |
Expand Down Expand Up @@ -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, _)
|
Expand Down
28 changes: 23 additions & 5 deletions rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,11 @@ private module Input1 implements InputSig1<Location> {

class Type = T::Type;

predicate isPseudoType(Type t) {
t instanceof UnknownType or
t instanceof NeverType
}

class TypeParameter = T::TypeParameter;

class TypeAbstraction = TA::TypeAbstraction;
Expand Down Expand Up @@ -230,9 +235,10 @@ private module PreInput2 implements InputSig2<PreTypeMention> {
}

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 =
Expand All @@ -256,9 +262,10 @@ private module Input2 implements InputSig2<TypeMention> {
}

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 =
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
)
}

Expand Down
8 changes: 1 addition & 7 deletions rust/ql/test/library-tests/type-inference/type-inference.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 |
Expand Down Expand Up @@ -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 |
Expand Down Expand Up @@ -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 |
109 changes: 100 additions & 9 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 @@ -145,6 +145,8 @@ signature module InputSig1<LocationSig Location> {
Location getLocation();
}

predicate isPseudoType(Type t);

/** A type parameter. */
class TypeParameter extends Type;

Expand Down Expand Up @@ -413,7 +415,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
* not at the path `"T2"`.
*/
predicate typeAbstractionHasAmbiguousConstraintAt(
TypeAbstraction abs, Type constraint, TypePath path
TypeAbstraction abs, Type constraint, TypeAbstraction other, TypePath path
);

/**
Expand Down Expand Up @@ -648,8 +650,22 @@ module Make1<LocationSig Location, InputSig1<Location> 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
)
}
}

Expand Down Expand Up @@ -1004,17 +1020,92 @@ module Make1<LocationSig Location, InputSig1<Location> 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
Expand Down
Loading