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
32 changes: 28 additions & 4 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 @@ -84,9 +84,33 @@ 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
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
Expand All @@ -103,7 +127,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
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 @@ -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
Expand Down Expand Up @@ -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
)
}

Expand Down
7 changes: 1 addition & 6 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 @@ -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 |
Expand Down Expand Up @@ -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 |
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