Skip to content

Commit 87447fb

Browse files
hvitvedhvitved
committed
wip3
1 parent 383e7b6 commit 87447fb

File tree

5 files changed

+57
-151
lines changed

5 files changed

+57
-151
lines changed

‎rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll‎

Lines changed: 32 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
4141
trait = impl.resolveTraitTy()
4242
}
4343

44-
private module FooIsInstantiationOfInput implements IsInstantiationOfInputSig<Tm, Tm> {
44+
private module ImplIsInstantiationOfSiblingInput implements IsInstantiationOfInputSig<Tm, Tm> {
4545
predicate potentialInstantiationOf(Tm cond, TypeAbstraction abs, Tm constraint) {
4646
exists(TraitItemNode trait, Type rootType |
4747
implSiblingCandidate(_, trait, rootType, cond) and
@@ -51,25 +51,40 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
5151
}
5252
}
5353

54-
private module FooIsInstantiationOf = IsInstantiationOf<Tm, Tm, FooIsInstantiationOfInput>;
54+
private module ImplIsInstantiationOfSibling =
55+
IsInstantiationOf<Tm, Tm, ImplIsInstantiationOfSiblingInput>;
5556

5657
/**
5758
* Holds if `impl1` and `impl2` are sibling implementations of `trait`. We
58-
* consider implementations to be siblings if they implement the same trait for
59-
* the same type. In that case `Self` is the same type in both implementations,
60-
* and method calls to the implementations cannot be resolved unambiguously
61-
* based only on the receiver type.
59+
* consider implementations to be siblings if they implement the same trait and
60+
* the type being implemented by one of the implementations is an instantiation
61+
* of the type being implemented by the other.
62+
*
63+
* For example, in
64+
*
65+
* ```rust
66+
* trait MyTrait<T> { ... }
67+
* impl MyTrait<i64> for i64 { ... } // I1
68+
* impl MyTrait<u64> for i64 { ... } // I2
69+
*
70+
* impl MyTrait<i64> for S<i64> { ... } // I3
71+
* impl MyTrait<u64> for S<u64> { ... } // I4
72+
* impl MyTrait<bool> for S<T> { ... } // I5
73+
* ```
74+
*
75+
* the pairs `(I1, I2)`, `(I3, I5)`, and `(I4, I5)` are siblings, but not `(I3, I4)`.
76+
*
77+
* Whenever an implementation has a sibling, calls to the implementations cannot be
78+
* resolved unambiguously based only on the `Self` type alone.
6279
*/
6380
pragma[inline]
64-
predicate implSiblings(TraitItemNode trait, Impl impl1, Impl impl2) {
65-
// impl1.fromSource() and
66-
// impl1 instanceof Builtins::BuiltinImpl and
81+
predicate implSiblings(TraitItemNode trait, ImplItemNode impl1, ImplItemNode impl2) {
6782
exists(Type rootType, AstNode selfTy1, AstNode selfTy2 |
6883
implSiblingCandidate(impl1, trait, rootType, selfTy1) and
6984
implSiblingCandidate(impl2, trait, rootType, selfTy2)
7085
|
71-
FooIsInstantiationOf::isInstantiationOf(selfTy1, impl2, selfTy2) or
72-
FooIsInstantiationOf::isInstantiationOf(selfTy2, impl1, selfTy1)
86+
ImplIsInstantiationOfSibling::isInstantiationOf(selfTy1, impl2, selfTy2) or
87+
ImplIsInstantiationOfSibling::isInstantiationOf(selfTy2, impl1, selfTy1)
7388
)
7489
or
7590
blanketImplSiblingCandidate(impl1, trait) and
@@ -85,11 +100,8 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
85100
predicate implHasSibling(ImplItemNode impl, Trait trait) { implSiblings(trait, impl, _) }
86101

87102
pragma[nomagic]
88-
predicate implHasAmbiguousSiblingAt(
89-
ImplItemNode impl, ImplItemNode impl2, Trait trait, TypePath path
90-
) {
91-
// impl instanceof Builtins::BuiltinImpl and
92-
exists(Type t1, Type t2 |
103+
predicate implHasAmbiguousSiblingAt(ImplItemNode impl, Trait trait, TypePath path) {
104+
exists(ImplItemNode impl2, Type t1, Type t2 |
93105
implSiblings(trait, impl, impl2) and
94106
t1 = resolveTypeMentionAt(impl.getTraitPath(), path) and
95107
t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) and
@@ -99,7 +111,9 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
99111
not t2 instanceof TypeParameter
100112
)
101113
or
102-
// todo: handle blanket/non-blanket siblings in `implSiblings`
114+
// Since we cannot resolve the `Output` types of certain built-in `Index` trait
115+
// implementations, we need to ensure that the type-specialized versions that we
116+
// ship do not apply unless there is an exact type match
103117
trait =
104118
any(IndexTrait it |
105119
implSiblingCandidate(impl, it, _, _) and
@@ -115,7 +129,7 @@ private Type resolvePreTypeMention(AstNode tm, TypePath path) {
115129

116130
private module PreSiblingImpls = MkSiblingImpls<resolvePreTypeMention/2>;
117131

118-
predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/4;
132+
predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/3;
119133

120134
private Type resolveTypeMention(AstNode tm, TypePath path) {
121135
result = tm.(TypeMention).getTypeAt(path)
@@ -259,7 +273,6 @@ pragma[nomagic]
259273
predicate functionResolutionDependsOnArgument(
260274
ImplItemNode impl, Function f, TypeParameter traitTp, FunctionPosition pos
261275
) {
262-
// impl.fromSource() and
263276
exists(string functionName |
264277
functionResolutionDependsOnArgumentCand(impl, f, functionName, traitTp, pos, _)
265278
|

‎rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll‎

Lines changed: 5 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -235,10 +235,9 @@ private module PreInput2 implements InputSig2<PreTypeMention> {
235235
}
236236

237237
predicate typeAbstractionHasAmbiguousConstraintAt(
238-
TypeAbstraction abs, Type constraint, TypeAbstraction other, TypePath path
238+
TypeAbstraction abs, Type constraint, TypePath path
239239
) {
240-
FunctionOverloading::preImplHasAmbiguousSiblingAt(abs, other, constraint.(TraitType).getTrait(),
241-
path)
240+
FunctionOverloading::preImplHasAmbiguousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
242241
}
243242

244243
predicate typeParameterIsFunctionallyDetermined =
@@ -262,10 +261,9 @@ private module Input2 implements InputSig2<TypeMention> {
262261
}
263262

264263
predicate typeAbstractionHasAmbiguousConstraintAt(
265-
TypeAbstraction abs, Type constraint, TypeAbstraction other, TypePath path
264+
TypeAbstraction abs, Type constraint, TypePath path
266265
) {
267-
FunctionOverloading::implHasAmbiguousSiblingAt(abs, other, constraint.(TraitType).getTrait(),
268-
path)
266+
FunctionOverloading::implHasAmbiguousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
269267
}
270268

271269
predicate typeParameterIsFunctionallyDetermined =
@@ -1932,17 +1930,6 @@ private module AssocFunctionResolution {
19321930
)
19331931
}
19341932

1935-
// private AssocFunctionDeclaration testresolveCallTarget(
1936-
// ImplOrTraitItemNode i, FunctionPosition selfPos, DerefChain derefChain, BorrowKind borrow,
1937-
// FunctionPosition pos, TypePath path, Type t
1938-
// ) {
1939-
// this = Debug::getRelevantLocatable() and
1940-
// exists(AssocFunctionCallCand afcc |
1941-
// afcc = MkAssocFunctionCallCand(this, selfPos, derefChain, borrow) and
1942-
// result = afcc.resolveCallTarget(i) and
1943-
// t = result.getParameterType(any(ImplOrTraitItemNodeOption o | o.asSome() = i), pos, path)
1944-
// )
1945-
// }
19461933
/**
19471934
* Holds if the argument `arg` of this call has been implicitly dereferenced
19481935
* and borrowed according to `derefChain` and `borrow`, in order to be able to
@@ -3960,7 +3947,7 @@ private module Debug {
39603947
exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
39613948
result.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
39623949
filepath.matches("%/main.rs") and
3963-
startline = 441
3950+
startline = 103
39643951
)
39653952
}
39663953

‎rust/ql/test/library-tests/type-inference/regressions.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ mod regression5 {
149149

150150
fn foo() -> S2<S1> {
151151
let x = S1.into(); // $ target=into
152-
x // $ SPURIOUS: type=x:T2.TRef.S1 -- happens because we currently do not consider the two `impl` blocks to be siblings
152+
x // $ type=x:T2.S1
153153
}
154154
}
155155

‎rust/ql/test/library-tests/type-inference/type-inference.expected‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15855,4 +15855,3 @@ inferType
1585515855
| regressions.rs:179:24:179:27 | S(...) | T | {EXTERNAL LOCATION} | i32 |
1585615856
| regressions.rs:179:26:179:26 | 1 | | {EXTERNAL LOCATION} | i32 |
1585715857
testFailures
15858-
| regressions.rs:152:11:152:127 | //... | Fixed spurious result: type=x:T2.TRef.S1 |

‎shared/typeinference/codeql/typeinference/internal/TypeInference.qll‎

Lines changed: 19 additions & 112 deletions
Original file line numberDiff line numberDiff line change
@@ -145,6 +145,10 @@ signature module InputSig1<LocationSig Location> {
145145
Location getLocation();
146146
}
147147

148+
/**
149+
* Holds if `t` is a pseudo type. Pseudo types are skipped when checking for
150+
* non-instantiations in `isNotInstantiationOf`.
151+
*/
148152
predicate isPseudoType(Type t);
149153

150154
/** A type parameter. */
@@ -415,7 +419,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
415419
* not at the path `"T2"`.
416420
*/
417421
predicate typeAbstractionHasAmbiguousConstraintAt(
418-
TypeAbstraction abs, Type constraint, TypeAbstraction other, TypePath path
422+
TypeAbstraction abs, Type constraint, TypePath path
419423
);
420424

421425
/**
@@ -639,7 +643,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
639643
}
640644

641645
pragma[nomagic]
642-
private Type getNonPseudoTypeAt2(
646+
private Type getNonPseudoTypeAtTypeParameter(
643647
App app, TypeAbstraction abs, Constraint constraint, TypeParameter tp, TypePath path
644648
) {
645649
hasTypeParameterAt(app, abs, constraint, path, tp) and
@@ -665,18 +669,19 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
665669
predicate isNotInstantiationOf(
666670
App app, TypeAbstraction abs, Constraint constraint, TypePath path
667671
) {
668-
// `app` and `constraint` differ on a concrete type
672+
// `app` and `constraint` differ on a non-pseudo concrete type
669673
exists(Type t, Type t2 |
670674
t = getTypeAt(app, abs, constraint, path) and
671675
not t = abs.getATypeParameter() and
672676
t2 = getNonPseudoTypeAt(app, path) and
673677
t2 != t
674678
)
675679
or
676-
// satisfiesConcreteTypes(app, abs, constraint) and
680+
// `app` has different instantiations of a type parameter mentioned at two
681+
// different paths
677682
exists(TypeParameter tp, TypePath path2, Type t, Type t2 |
678-
t = getNonPseudoTypeAt2(app, abs, constraint, tp, path) and
679-
t2 = getNonPseudoTypeAt2(app, abs, constraint, tp, path2) and
683+
t = getNonPseudoTypeAtTypeParameter(app, abs, constraint, tp, path) and
684+
t2 = getNonPseudoTypeAtTypeParameter(app, abs, constraint, tp, path2) and
680685
t != t2 and
681686
path != path2
682687
)
@@ -1027,122 +1032,24 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10271032
)
10281033
}
10291034

1030-
private module TermIsInstantiationOfConditionInput2 implements
1031-
IsInstantiationOfInputSig<Term, TypeMention>
1032-
{
1033-
predicate potentialInstantiationOf(Term term, TypeAbstraction abs, TypeMention cond) {
1034-
TermIsInstantiationOfConditionInput::potentialInstantiationOf(term, abs, cond) and
1035-
exists(
1036-
TypeMention sub, Type constraintRoot, TypeMention constraintMention,
1037-
TypeAbstraction abs2
1038-
|
1039-
hasConstraintMention(term, abs2, sub, _, constraintRoot, constraintMention) and
1040-
conditionSatisfiesConstraintTypeAt(abs2, sub, constraintMention, _, _) and
1041-
typeAbstractionHasAmbiguousConstraintAt(abs2, constraintRoot, abs, _)
1042-
)
1043-
}
1044-
1045-
predicate relevantConstraint(TypeMention constraint) {
1046-
TermIsInstantiationOfConditionInput::relevantConstraint(constraint)
1047-
}
1048-
}
1049-
1050-
private module TermIsInstantiationOfCondition2 =
1051-
IsInstantiationOf<Term, TypeMention, TermIsInstantiationOfConditionInput2>;
1052-
10531035
pragma[nomagic]
10541036
private predicate satisfiesConstraintTypeMention0(
10551037
Term term, Constraint constraint, TypeMention constraintMention, TypeAbstraction abs,
10561038
TypeMention sub, TypePath path, Type t, boolean ambiguous
10571039
) {
10581040
exists(Type constraintRoot |
10591041
hasConstraintMention(term, abs, sub, constraint, constraintRoot, constraintMention) and
1060-
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t)
1061-
|
1062-
exists(TypePath prefix, TypeAbstraction other |
1063-
typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1064-
prefix.isPrefixOf(path) and
1065-
TermIsInstantiationOfCondition2::isInstantiationOf(term, other, _)
1066-
// hasConstraintMention(term, other, _, _, constraintRoot, _)
1067-
) and
1068-
ambiguous = true
1069-
or
1070-
forall(TypePath prefix, TypeAbstraction other |
1071-
typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1072-
prefix.isPrefixOf(path)
1073-
|
1074-
TermIsInstantiationOfCondition2::isNotInstantiationOf(term, other, _, _)
1075-
) and
1076-
ambiguous = false
1042+
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t) and
1043+
if
1044+
exists(TypePath prefix |
1045+
typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, prefix) and
1046+
prefix.isPrefixOf(path)
1047+
)
1048+
then ambiguous = true
1049+
else ambiguous = false
10771050
)
10781051
}
10791052

1080-
// private predicate testsatisfiesConstraintTypeMention0(
1081-
// Term term, Constraint constraint, TypeMention constraintMention, TypeAbstraction abs,
1082-
// TypeMention sub, TypePath path, Type t, boolean ambiguous
1083-
// ) {
1084-
// exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
1085-
// term.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
1086-
// filepath.matches("%/main.rs") and
1087-
// startline = 435
1088-
// ) and
1089-
// satisfiesConstraintTypeMention0(term, constraint, constraintMention, abs, sub, path, t,
1090-
// ambiguous)
1091-
// }
1092-
// private predicate testsatisfiesConstraintTypeMention1(
1093-
// Term term, Constraint constraint, TypeMention constraintMention, TypeAbstraction abs,
1094-
// TypeMention sub, TypePath path, Type t, boolean ambiguous, TypePath prefix,
1095-
// TypeAbstraction other, TypePath path2
1096-
// ) {
1097-
// exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
1098-
// term.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
1099-
// filepath.matches("%/main.rs") and
1100-
// startline = 435
1101-
// ) and
1102-
// exists(Type constraintRoot |
1103-
// hasConstraintMention(term, abs, sub, constraint, constraintRoot, constraintMention) and
1104-
// conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t)
1105-
// |
1106-
// // if
1107-
// // exists(TypePath prefix, TypeAbstraction other |
1108-
// // typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1109-
// // prefix.isPrefixOf(path)
1110-
// // )
1111-
// // then ambiguous = true
1112-
// // else ambiguous = false
1113-
// typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1114-
// // isNotInstantiationOf(term, other, _, constraintRoot) and
1115-
// // TermIsInstantiationOfConditionInput::potentialInstantiationOf(term, other, _) and
1116-
// prefix.isPrefixOf(path) and
1117-
// TermIsInstantiationOfCondition::isNotInstantiationOf(term, other, _, path2) and
1118-
// // not isNotInstantiationOf(term, other, _, constraintRoot) and
1119-
// ambiguous = false
1120-
// // exists(TypePath prefix, TypeAbstraction other |
1121-
// // typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1122-
// // prefix.isPrefixOf(path) and
1123-
// // hasConstraintMention(term, other, _, _, constraintRoot, _)
1124-
// // ) and
1125-
// // ambiguous = true
1126-
// // or
1127-
// // forall(TypePath prefix, TypeAbstraction other |
1128-
// // typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix)
1129-
// // |
1130-
// // not prefix.isPrefixOf(path)
1131-
// // or
1132-
// // // exists(Type type | hasTypeConstraint(term, type, constraint, constraintRoot) |
1133-
// // // // countConstraintImplementations(type, constraintRoot) = 0
1134-
// // // // or
1135-
// // // // not rootTypesSatisfaction(type, constraintRoot, _, _, _)
1136-
// // // // or
1137-
// // // multipleConstraintImplementations(type, constraintRoot) and
1138-
// // // isNotInstantiationOf(term, other, _, constraintRoot)
1139-
// // // )
1140-
// // isNotInstantiationOf(term, other, _, constraintRoot)
1141-
// // // TermIsInstantiationOfCondition::isNotInstantiationOf(term, other, _, _)
1142-
// // ) and
1143-
// // ambiguous = false
1144-
// )
1145-
// }
11461053
pragma[nomagic]
11471054
private predicate conditionSatisfiesConstraintTypeAtForDisambiguation(
11481055
TypeAbstraction abs, TypeMention condition, TypeMention constraint, TypePath path, Type t

0 commit comments

Comments
 (0)