Skip to content

Commit f7b803d

Browse files
hvitvedhvitved
committed
Rust: Refine implHasAmbiguousSiblingAt 
1 parent ee34e33 commit f7b803d

File tree

4 files changed

+178
-66
lines changed

4 files changed

+178
-66
lines changed

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

Lines changed: 54 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -28,11 +28,8 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
2828
not result instanceof TypeParameter
2929
}
3030

31-
bindingset[t1, t2]
32-
private predicate typeMentionEqual(AstNode t1, AstNode t2) {
33-
forex(TypePath path, Type type | resolveNonTypeParameterTypeAt(t1, path) = type |
34-
resolveNonTypeParameterTypeAt(t2, path) = type
35-
)
31+
private class Tm extends AstNode {
32+
Type getTypeAt(TypePath path) { result = resolveTypeMentionAt(this, path) }
3633
}
3734

3835
pragma[nomagic]
@@ -50,6 +47,18 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
5047
trait = impl.resolveTraitTy()
5148
}
5249

50+
private module FooIsInstantiationOfInput implements IsInstantiationOfInputSig<Tm, Tm> {
51+
predicate potentialInstantiationOf(Tm cond, TypeAbstraction abs, Tm constraint) {
52+
exists(TraitItemNode trait, Type rootType |
53+
implSiblingCandidate(_, trait, rootType, cond) and
54+
implSiblingCandidate(abs, trait, rootType, constraint) and
55+
cond != constraint
56+
)
57+
}
58+
}
59+
60+
private module FooIsInstantiationOf = IsInstantiationOf<Tm, Tm, FooIsInstantiationOfInput>;
61+
5362
/**
5463
* Holds if `impl1` and `impl2` are sibling implementations of `trait`. We
5564
* consider implementations to be siblings if they implement the same trait for
@@ -59,23 +68,19 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
5968
*/
6069
pragma[inline]
6170
predicate implSiblings(TraitItemNode trait, Impl impl1, Impl impl2) {
62-
impl1 != impl2 and
63-
(
64-
exists(Type rootType, AstNode selfTy1, AstNode selfTy2 |
65-
implSiblingCandidate(impl1, trait, rootType, selfTy1) and
66-
implSiblingCandidate(impl2, trait, rootType, selfTy2) and
67-
// In principle the second conjunct below should be superfluous, but we still
68-
// have ill-formed type mentions for types that we don't understand. For
69-
// those checking both directions restricts further. Note also that we check
70-
// syntactic equality, whereas equality up to renaming would be more
71-
// correct.
72-
typeMentionEqual(selfTy1, selfTy2) and
73-
typeMentionEqual(selfTy2, selfTy1)
74-
)
75-
or
76-
blanketImplSiblingCandidate(impl1, trait) and
77-
blanketImplSiblingCandidate(impl2, trait)
71+
// impl1.fromSource() and
72+
// impl1 instanceof Builtins::BuiltinImpl and
73+
exists(Type rootType, AstNode selfTy1, AstNode selfTy2 |
74+
implSiblingCandidate(impl1, trait, rootType, selfTy1) and
75+
implSiblingCandidate(impl2, trait, rootType, selfTy2)
76+
|
77+
FooIsInstantiationOf::isInstantiationOf(selfTy1, impl2, selfTy2) or
78+
FooIsInstantiationOf::isInstantiationOf(selfTy2, impl1, selfTy1)
7879
)
80+
or
81+
blanketImplSiblingCandidate(impl1, trait) and
82+
blanketImplSiblingCandidate(impl2, trait) and
83+
impl1 != impl2
7984
}
8085

8186
/**
@@ -86,24 +91,32 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
8691
predicate implHasSibling(ImplItemNode impl, Trait trait) { implSiblings(trait, impl, _) }
8792

8893
pragma[nomagic]
89-
predicate implHasAmbiguousSiblingAt(ImplItemNode impl, Trait trait, TypePath path) {
90-
exists(ImplItemNode impl2, Type t1, Type t2 |
91-
implSiblings(trait, impl, impl2) and
92-
t1 = resolveTypeMentionAt(impl.getTraitPath(), path) and
93-
t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) and
94-
t1 != t2
95-
|
96-
not t1 instanceof TypeParameter or
97-
not t2 instanceof TypeParameter
94+
predicate implHasAmbiguousSiblingAt(
95+
ImplItemNode impl, ImplItemNode impl2, Trait trait, TypePath path
96+
) {
97+
// impl instanceof Builtins::BuiltinImpl and
98+
exists(Type t | implSiblings(trait, impl, impl2) |
99+
t = resolveTypeMentionAt(impl.getTraitPath(), path) and
100+
not (t = resolveTypeMentionAt(impl2.getTraitPath(), path) and not t instanceof TypeParameter)
101+
or
102+
t = resolveTypeMentionAt(impl2.getTraitPath(), path) and
103+
not (t = resolveTypeMentionAt(impl.getTraitPath(), path) and not t instanceof TypeParameter)
104+
// and
105+
// t1 = resolveTypeMentionAt(impl.getTraitPath(), path) and
106+
// t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) and
107+
// t1 != t2
108+
// |
109+
// not t1 instanceof TypeParameter or
110+
// not t2 instanceof TypeParameter
98111
)
99-
or
100-
// todo: handle blanket/non-blanket siblings in `implSiblings`
101-
trait =
102-
any(IndexTrait it |
103-
implSiblingCandidate(impl, it, _, _) and
104-
impl instanceof Builtins::BuiltinImpl and
105-
path = TypePath::singleton(TAssociatedTypeTypeParameter(trait, it.getOutputType()))
106-
)
112+
// or
113+
// // todo: handle blanket/non-blanket siblings in `implSiblings`
114+
// trait =
115+
// any(IndexTrait it |
116+
// implSiblingCandidate(impl, it, _, _) and
117+
// impl instanceof Builtins::BuiltinImpl and
118+
// path = TypePath::singleton(TAssociatedTypeTypeParameter(trait, it.getOutputType()))
119+
// )
107120
}
108121
}
109122

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

114127
private module PreSiblingImpls = MkSiblingImpls<resolvePreTypeMention/2>;
115128

116-
predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/3;
129+
predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/4;
117130

118131
private Type resolveTypeMention(AstNode tm, TypePath path) {
119132
result = tm.(TypeMention).getTypeAt(path)
@@ -152,19 +165,14 @@ private predicate functionResolutionDependsOnArgumentCand(
152165
* ```rust
153166
* trait MyTrait<T> {
154167
* fn method(&self, value: Foo<T>) -> Self;
155-
* // ^^^^^^^^^^^^^ `pos` = 0
168+
* // ^^^^^^^^^^^^^ `pos` = 1
156169
* // ^ `path` = "T"
157170
* }
158171
* impl MyAdd<i64> for i64 {
159172
* fn method(&self, value: Foo<i64>) -> Self { ... }
160173
* // ^^^ `type` = i64
161174
* }
162175
* ```
163-
*
164-
* Note that we only check the root type symbol at the position. If the type
165-
* at that position is a type constructor (for instance `Vec<..>`) then
166-
* inspecting the entire type tree could be necessary to disambiguate the
167-
* method. In that case we will still resolve several methods.
168176
*/
169177

170178
exists(TraitItemNode trait |
@@ -262,6 +270,7 @@ pragma[nomagic]
262270
predicate functionResolutionDependsOnArgument(
263271
ImplItemNode impl, Function f, TypeParameter traitTp, FunctionPosition pos
264272
) {
273+
// impl.fromSource() and
265274
exists(string functionName |
266275
functionResolutionDependsOnArgumentCand(impl, f, functionName, traitTp, pos, _)
267276
|

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

Lines changed: 23 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,11 @@ private module Input1 implements InputSig1<Location> {
3737

3838
class Type = T::Type;
3939

40+
predicate isPseudoType(Type t) {
41+
t instanceof UnknownType or
42+
t instanceof NeverType
43+
}
44+
4045
class TypeParameter = T::TypeParameter;
4146

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

232237
predicate typeAbstractionHasAmbiguousConstraintAt(
233-
TypeAbstraction abs, Type constraint, TypePath path
238+
TypeAbstraction abs, Type constraint, TypeAbstraction other, TypePath path
234239
) {
235-
FunctionOverloading::preImplHasAmbiguousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
240+
FunctionOverloading::preImplHasAmbiguousSiblingAt(abs, other, constraint.(TraitType).getTrait(),
241+
path)
236242
}
237243

238244
predicate typeParameterIsFunctionallyDetermined =
@@ -256,9 +262,10 @@ private module Input2 implements InputSig2<TypeMention> {
256262
}
257263

258264
predicate typeAbstractionHasAmbiguousConstraintAt(
259-
TypeAbstraction abs, Type constraint, TypePath path
265+
TypeAbstraction abs, Type constraint, TypeAbstraction other, TypePath path
260266
) {
261-
FunctionOverloading::implHasAmbiguousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
267+
FunctionOverloading::implHasAmbiguousSiblingAt(abs, other, constraint.(TraitType).getTrait(),
268+
path)
262269
}
263270

264271
predicate typeParameterIsFunctionallyDetermined =
@@ -1925,6 +1932,17 @@ private module AssocFunctionResolution {
19251932
)
19261933
}
19271934

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+
// }
19281946
/**
19291947
* Holds if the argument `arg` of this call has been implicitly dereferenced
19301948
* and borrowed according to `derefChain` and `borrow`, in order to be able to
@@ -3942,7 +3960,7 @@ private module Debug {
39423960
exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
39433961
result.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
39443962
filepath.matches("%/main.rs") and
3945-
startline = 103
3963+
startline = 441
39463964
)
39473965
}
39483966

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

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -11605,7 +11605,6 @@ inferType
1160511605
| main.rs:2223:9:2223:31 | ... .my_add(...) | T | main.rs:2107:5:2107:19 | S |
1160611606
| main.rs:2223:9:2223:31 | ... .my_add(...) | T.T | main.rs:2109:10:2109:17 | T::Output[MyAdd] |
1160711607
| main.rs:2223:9:2223:31 | ... .my_add(...) | T.T | main.rs:2118:10:2118:17 | T::Output[MyAdd] |
11608-
| main.rs:2223:9:2223:31 | ... .my_add(...) | T.T | main.rs:2127:14:2127:14 | T::Output[MyAdd] |
1160911608
| main.rs:2223:11:2223:14 | 1i64 | | {EXTERNAL LOCATION} | i64 |
1161011609
| main.rs:2223:24:2223:30 | S(...) | | main.rs:2107:5:2107:19 | S |
1161111610
| main.rs:2223:24:2223:30 | S(...) | T | {EXTERNAL LOCATION} | i64 |
@@ -15818,18 +15817,12 @@ inferType
1581815817
| regressions.rs:150:24:153:5 | { ... } | | regressions.rs:136:5:136:22 | S2 |
1581915818
| regressions.rs:150:24:153:5 | { ... } | T2 | regressions.rs:135:5:135:14 | S1 |
1582015819
| regressions.rs:151:13:151:13 | x | | regressions.rs:136:5:136:22 | S2 |
15821-
| regressions.rs:151:13:151:13 | x | T2 | {EXTERNAL LOCATION} | & |
1582215820
| regressions.rs:151:13:151:13 | x | T2 | regressions.rs:135:5:135:14 | S1 |
15823-
| regressions.rs:151:13:151:13 | x | T2.TRef | regressions.rs:135:5:135:14 | S1 |
1582415821
| regressions.rs:151:17:151:18 | S1 | | regressions.rs:135:5:135:14 | S1 |
1582515822
| regressions.rs:151:17:151:25 | S1.into() | | regressions.rs:136:5:136:22 | S2 |
15826-
| regressions.rs:151:17:151:25 | S1.into() | T2 | {EXTERNAL LOCATION} | & |
1582715823
| regressions.rs:151:17:151:25 | S1.into() | T2 | regressions.rs:135:5:135:14 | S1 |
15828-
| regressions.rs:151:17:151:25 | S1.into() | T2.TRef | regressions.rs:135:5:135:14 | S1 |
1582915824
| regressions.rs:152:9:152:9 | x | | regressions.rs:136:5:136:22 | S2 |
15830-
| regressions.rs:152:9:152:9 | x | T2 | {EXTERNAL LOCATION} | & |
1583115825
| regressions.rs:152:9:152:9 | x | T2 | regressions.rs:135:5:135:14 | S1 |
15832-
| regressions.rs:152:9:152:9 | x | T2.TRef | regressions.rs:135:5:135:14 | S1 |
1583315826
| regressions.rs:164:16:164:19 | SelfParam | | regressions.rs:158:5:158:19 | S |
1583415827
| regressions.rs:164:16:164:19 | SelfParam | T | regressions.rs:160:10:160:10 | T |
1583515828
| regressions.rs:164:22:164:25 | _rhs | | regressions.rs:158:5:158:19 | S |
@@ -15861,3 +15854,4 @@ inferType
1586115854
| regressions.rs:179:24:179:27 | S(...) | T | {EXTERNAL LOCATION} | i32 |
1586215855
| regressions.rs:179:26:179:26 | 1 | | {EXTERNAL LOCATION} | i32 |
1586315856
testFailures
15857+
| regressions.rs:152:11:152:127 | //... | Fixed spurious result: type=x:T2.TRef.S1 |

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

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

148+
predicate isPseudoType(Type t);
149+
148150
/** A type parameter. */
149151
class TypeParameter extends Type;
150152

@@ -413,7 +415,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
413415
* not at the path `"T2"`.
414416
*/
415417
predicate typeAbstractionHasAmbiguousConstraintAt(
416-
TypeAbstraction abs, Type constraint, TypePath path
418+
TypeAbstraction abs, Type constraint, TypeAbstraction other, TypePath path
417419
);
418420

419421
/**
@@ -648,8 +650,22 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
648650
t = getTypeAt(app, abs, constraint, path) and
649651
not t = abs.getATypeParameter() and
650652
app.getTypeAt(path) = t2 and
653+
not isPseudoType(t2) and
651654
t2 != t
652655
)
656+
or
657+
// satisfiesConcreteTypes(app, abs, constraint) and
658+
exists(TypeParameter tp, TypePath path2, Type t, Type t2 |
659+
tp = getTypeAt(app, abs, constraint, path) and
660+
tp = getTypeAt(app, abs, constraint, path2) and
661+
tp = abs.getATypeParameter() and
662+
path != path2 and
663+
app.getTypeAt(path) = t and
664+
app.getTypeAt(path2) = t2 and
665+
not isPseudoType(t) and
666+
not isPseudoType(t2) and
667+
t != t2
668+
)
653669
}
654670
}
655671

@@ -1004,17 +1020,92 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10041020
) {
10051021
exists(Type constraintRoot |
10061022
hasConstraintMention(term, abs, sub, constraint, constraintRoot, constraintMention) and
1007-
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t) and
1008-
if
1009-
exists(TypePath prefix |
1010-
typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, prefix) and
1011-
prefix.isPrefixOf(path)
1012-
)
1013-
then ambiguous = true
1014-
else ambiguous = false
1023+
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t)
1024+
|
1025+
exists(TypePath prefix, TypeAbstraction other |
1026+
typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1027+
prefix.isPrefixOf(path) and
1028+
hasConstraintMention(term, other, _, _, constraintRoot, _)
1029+
) and
1030+
ambiguous = true
1031+
or
1032+
forall(TypePath prefix, TypeAbstraction other |
1033+
typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix)
1034+
|
1035+
not prefix.isPrefixOf(path)
1036+
or
1037+
TermIsInstantiationOfCondition::isNotInstantiationOf(term, other, _, _)
1038+
) and
1039+
ambiguous = false
10151040
)
10161041
}
10171042

1043+
// private predicate testsatisfiesConstraintTypeMention0(
1044+
// Term term, Constraint constraint, TypeMention constraintMention, TypeAbstraction abs,
1045+
// TypeMention sub, TypePath path, Type t, boolean ambiguous
1046+
// ) {
1047+
// exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
1048+
// term.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
1049+
// filepath.matches("%/main.rs") and
1050+
// startline = 435
1051+
// ) and
1052+
// satisfiesConstraintTypeMention0(term, constraint, constraintMention, abs, sub, path, t,
1053+
// ambiguous)
1054+
// }
1055+
// private predicate testsatisfiesConstraintTypeMention1(
1056+
// Term term, Constraint constraint, TypeMention constraintMention, TypeAbstraction abs,
1057+
// TypeMention sub, TypePath path, Type t, boolean ambiguous, TypePath prefix,
1058+
// TypeAbstraction other, TypePath path2
1059+
// ) {
1060+
// exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
1061+
// term.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
1062+
// filepath.matches("%/main.rs") and
1063+
// startline = 435
1064+
// ) and
1065+
// exists(Type constraintRoot |
1066+
// hasConstraintMention(term, abs, sub, constraint, constraintRoot, constraintMention) and
1067+
// conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t)
1068+
// |
1069+
// // if
1070+
// // exists(TypePath prefix, TypeAbstraction other |
1071+
// // typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1072+
// // prefix.isPrefixOf(path)
1073+
// // )
1074+
// // then ambiguous = true
1075+
// // else ambiguous = false
1076+
// typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1077+
// // isNotInstantiationOf(term, other, _, constraintRoot) and
1078+
// // TermIsInstantiationOfConditionInput::potentialInstantiationOf(term, other, _) and
1079+
// prefix.isPrefixOf(path) and
1080+
// TermIsInstantiationOfCondition::isNotInstantiationOf(term, other, _, path2) and
1081+
// // not isNotInstantiationOf(term, other, _, constraintRoot) and
1082+
// ambiguous = false
1083+
// // exists(TypePath prefix, TypeAbstraction other |
1084+
// // typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1085+
// // prefix.isPrefixOf(path) and
1086+
// // hasConstraintMention(term, other, _, _, constraintRoot, _)
1087+
// // ) and
1088+
// // ambiguous = true
1089+
// // or
1090+
// // forall(TypePath prefix, TypeAbstraction other |
1091+
// // typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix)
1092+
// // |
1093+
// // not prefix.isPrefixOf(path)
1094+
// // or
1095+
// // // exists(Type type | hasTypeConstraint(term, type, constraint, constraintRoot) |
1096+
// // // // countConstraintImplementations(type, constraintRoot) = 0
1097+
// // // // or
1098+
// // // // not rootTypesSatisfaction(type, constraintRoot, _, _, _)
1099+
// // // // or
1100+
// // // multipleConstraintImplementations(type, constraintRoot) and
1101+
// // // isNotInstantiationOf(term, other, _, constraintRoot)
1102+
// // // )
1103+
// // isNotInstantiationOf(term, other, _, constraintRoot)
1104+
// // // TermIsInstantiationOfCondition::isNotInstantiationOf(term, other, _, _)
1105+
// // ) and
1106+
// // ambiguous = false
1107+
// )
1108+
// }
10181109
pragma[nomagic]
10191110
private predicate conditionSatisfiesConstraintTypeAtForDisambiguation(
10201111
TypeAbstraction abs, TypeMention condition, TypeMention constraint, TypePath path, Type t

0 commit comments

Comments
 (0)