Skip to content

Commit c5af080

Browse files
committed
Rust: Disambiguate types inferred from trait bounds
1 parent 98d8cd1 commit c5af080

File tree

7 files changed

+417
-136
lines changed

7 files changed

+417
-136
lines changed

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

Lines changed: 91 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -13,68 +13,105 @@ private import TypeMention
1313
private import TypeInference
1414
private import FunctionType
1515

16-
pragma[nomagic]
17-
private Type resolveNonTypeParameterTypeAt(TypeMention tm, TypePath path) {
18-
result = tm.getTypeAt(path) and
19-
not result instanceof TypeParameter
20-
}
16+
private signature Type resolveTypeMentionAtSig(AstNode tm, TypePath path);
2117

22-
bindingset[t1, t2]
23-
private predicate typeMentionEqual(TypeMention t1, TypeMention t2) {
24-
forex(TypePath path, Type type | resolveNonTypeParameterTypeAt(t1, path) = type |
25-
resolveNonTypeParameterTypeAt(t2, path) = type
26-
)
27-
}
18+
/**
19+
* Provides logic for identifying sibling implementations, parameterized over
20+
* how to resolve type mentions (`PreTypeMention` vs. `TypeMention`).
21+
*/
22+
private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
23+
pragma[nomagic]
24+
private Type resolveNonTypeParameterTypeAt(AstNode tm, TypePath path) {
25+
result = resolveTypeMentionAt(tm, path) and
26+
not result instanceof TypeParameter
27+
}
2828

29-
pragma[nomagic]
30-
private predicate implSiblingCandidate(
31-
Impl impl, TraitItemNode trait, Type rootType, TypeMention selfTy
32-
) {
33-
trait = impl.(ImplItemNode).resolveTraitTy() and
34-
selfTy = impl.getSelfTy() and
35-
rootType = selfTy.getType()
29+
bindingset[t1, t2]
30+
private predicate typeMentionEqual(AstNode t1, AstNode t2) {
31+
forex(TypePath path, Type type | resolveNonTypeParameterTypeAt(t1, path) = type |
32+
resolveNonTypeParameterTypeAt(t2, path) = type
33+
)
34+
}
35+
36+
pragma[nomagic]
37+
private predicate implSiblingCandidate(
38+
Impl impl, TraitItemNode trait, Type rootType, AstNode selfTy
39+
) {
40+
trait = impl.(ImplItemNode).resolveTraitTy() and
41+
selfTy = impl.getSelfTy() and
42+
rootType = resolveTypeMentionAt(selfTy, TypePath::nil())
43+
}
44+
45+
pragma[nomagic]
46+
private predicate blanketImplSiblingCandidate(ImplItemNode impl, Trait trait) {
47+
impl.isBlanketImplementation() and
48+
trait = impl.resolveTraitTy()
49+
}
50+
51+
/**
52+
* Holds if `impl1` and `impl2` are a sibling implementations of `trait`. We
53+
* consider implementations to be siblings if they implement the same trait for
54+
* the same type. In that case `Self` is the same type in both implementations,
55+
* and method calls to the implementations cannot be resolved unambiguously
56+
* based only on the receiver type.
57+
*/
58+
pragma[inline]
59+
predicate implSiblings(TraitItemNode trait, Impl impl1, Impl impl2) {
60+
impl1 != impl2 and
61+
(
62+
exists(Type rootType, AstNode selfTy1, AstNode selfTy2 |
63+
implSiblingCandidate(impl1, trait, rootType, selfTy1) and
64+
implSiblingCandidate(impl2, trait, rootType, selfTy2) and
65+
// In principle the second conjunct below should be superflous, but we still
66+
// have ill-formed type mentions for types that we don't understand. For
67+
// those checking both directions restricts further. Note also that we check
68+
// syntactic equality, whereas equality up to renaming would be more
69+
// correct.
70+
typeMentionEqual(selfTy1, selfTy2) and
71+
typeMentionEqual(selfTy2, selfTy1)
72+
)
73+
or
74+
blanketImplSiblingCandidate(impl1, trait) and
75+
blanketImplSiblingCandidate(impl2, trait)
76+
)
77+
}
78+
79+
/**
80+
* Holds if `impl` is an implementation of `trait` and if another implementation
81+
* exists for the same type.
82+
*/
83+
pragma[nomagic]
84+
predicate implHasSibling(ImplItemNode impl, Trait trait) { implSiblings(trait, impl, _) }
85+
86+
pragma[nomagic]
87+
predicate implHasAmbiguousSiblingAt(ImplItemNode impl, Trait trait, TypePath path) {
88+
exists(ImplItemNode impl2, Type t1, Type t2 |
89+
implSiblings(trait, impl, impl2) and
90+
t1 = resolveTypeMentionAt(impl.getTraitPath(), path) and
91+
t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) and
92+
t1 != t2
93+
|
94+
not t1 instanceof TypeParameter or
95+
not t2 instanceof TypeParameter
96+
)
97+
}
3698
}
3799

38-
pragma[nomagic]
39-
private predicate blanketImplSiblingCandidate(ImplItemNode impl, Trait trait) {
40-
impl.isBlanketImplementation() and
41-
trait = impl.resolveTraitTy()
100+
private Type resolvePreTypeMention(AstNode tm, TypePath path) {
101+
result = tm.(PreTypeMention).getTypeAt(path)
42102
}
43103

44-
/**
45-
* Holds if `impl1` and `impl2` are a sibling implementations of `trait`. We
46-
* consider implementations to be siblings if they implement the same trait for
47-
* the same type. In that case `Self` is the same type in both implementations,
48-
* and method calls to the implementations cannot be resolved unambiguously
49-
* based only on the receiver type.
50-
*/
51-
pragma[inline]
52-
private predicate implSiblings(TraitItemNode trait, Impl impl1, Impl impl2) {
53-
impl1 != impl2 and
54-
(
55-
exists(Type rootType, TypeMention selfTy1, TypeMention selfTy2 |
56-
implSiblingCandidate(impl1, trait, rootType, selfTy1) and
57-
implSiblingCandidate(impl2, trait, rootType, selfTy2) and
58-
// In principle the second conjunct below should be superflous, but we still
59-
// have ill-formed type mentions for types that we don't understand. For
60-
// those checking both directions restricts further. Note also that we check
61-
// syntactic equality, whereas equality up to renaming would be more
62-
// correct.
63-
typeMentionEqual(selfTy1, selfTy2) and
64-
typeMentionEqual(selfTy2, selfTy1)
65-
)
66-
or
67-
blanketImplSiblingCandidate(impl1, trait) and
68-
blanketImplSiblingCandidate(impl2, trait)
69-
)
104+
private module PreSiblingImpls = MkSiblingImpls<resolvePreTypeMention/2>;
105+
106+
predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/3;
107+
108+
private Type resolveTypeMention(AstNode tm, TypePath path) {
109+
result = tm.(TypeMention).getTypeAt(path)
70110
}
71111

72-
/**
73-
* Holds if `impl` is an implementation of `trait` and if another implementation
74-
* exists for the same type.
75-
*/
76-
pragma[nomagic]
77-
private predicate implHasSibling(ImplItemNode impl, Trait trait) { implSiblings(trait, impl, _) }
112+
private module SiblingImpls = MkSiblingImpls<resolveTypeMention/2>;
113+
114+
import SiblingImpls
78115

79116
/**
80117
* Holds if `f` is a function declared inside `trait`, and the type of `f` at

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

Lines changed: 75 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ private newtype TTypeArgumentPosition =
3030
} or
3131
TTypeParamTypeArgumentPosition(TypeParam tp)
3232

33-
private module Input implements InputSig1<Location>, InputSig2<PreTypeMention> {
33+
private module Input1 implements InputSig1<Location> {
3434
private import Type as T
3535
private import codeql.rust.elements.internal.generated.Raw
3636
private import codeql.rust.elements.internal.generated.Synth
@@ -122,12 +122,28 @@ private module Input implements InputSig1<Location>, InputSig2<PreTypeMention> {
122122
tp0 order by kind, id1, id2
123123
)
124124
}
125+
}
125126

126-
int getTypePathLimit() { result = 10 }
127+
private import Input1
127128

128-
PreTypeMention getABaseTypeMention(Type t) { none() }
129+
private module M1 = Make1<Location, Input1>;
129130

130-
PreTypeMention getATypeParameterConstraint(TypeParameter tp) {
131+
import M1
132+
133+
predicate getTypePathLimit = Input1::getTypePathLimit/0;
134+
135+
predicate getTypeParameterId = Input1::getTypeParameterId/1;
136+
137+
class TypePath = M1::TypePath;
138+
139+
module TypePath = M1::TypePath;
140+
141+
/**
142+
* Provides shared logic for implementing `InputSig2<PreTypeMention>` and
143+
* `InputSig2<TypeMention>`.
144+
*/
145+
private module Input2Common {
146+
AstNode getATypeParameterConstraint(TypeParameter tp) {
131147
result = tp.(TypeParamTypeParameter).getTypeParam().getATypeBound().getTypeRepr() or
132148
result = tp.(SelfTypeParameter).getTrait() or
133149
result =
@@ -146,7 +162,7 @@ private module Input implements InputSig1<Location>, InputSig2<PreTypeMention> {
146162
* inference module for more information.
147163
*/
148164
predicate conditionSatisfiesConstraint(
149-
TypeAbstraction abs, PreTypeMention condition, PreTypeMention constraint, boolean transitive
165+
TypeAbstraction abs, AstNode condition, AstNode constraint, boolean transitive
150166
) {
151167
// `impl` blocks implementing traits
152168
transitive = false and
@@ -194,23 +210,64 @@ private module Input implements InputSig1<Location>, InputSig2<PreTypeMention> {
194210
)
195211
)
196212
}
213+
214+
predicate typeParameterIsFunctionallyDetermined(TypeParameter tp) {
215+
tp instanceof AssociatedTypeTypeParameter
216+
}
197217
}
198218

199-
private import Input
219+
private module PreInput2 implements InputSig2<PreTypeMention> {
220+
PreTypeMention getABaseTypeMention(Type t) { none() }
200221

201-
private module M1 = Make1<Location, Input>;
222+
PreTypeMention getATypeParameterConstraint(TypeParameter tp) {
223+
result = Input2Common::getATypeParameterConstraint(tp)
224+
}
202225

203-
import M1
226+
predicate conditionSatisfiesConstraint(
227+
TypeAbstraction abs, PreTypeMention condition, PreTypeMention constraint, boolean transitive
228+
) {
229+
Input2Common::conditionSatisfiesConstraint(abs, condition, constraint, transitive)
230+
}
204231

205-
predicate getTypePathLimit = Input::getTypePathLimit/0;
232+
predicate typeAbstractionHasAmbiguousConstraintAt(
233+
TypeAbstraction abs, Type constraint, TypePath path
234+
) {
235+
FunctionOverloading::preImplHasAmbiguousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
236+
}
206237

207-
predicate getTypeParameterId = Input::getTypeParameterId/1;
238+
predicate typeParameterIsFunctionallyDetermined =
239+
Input2Common::typeParameterIsFunctionallyDetermined/1;
240+
}
208241

209-
class TypePath = M1::TypePath;
242+
/** Provides an instantiation of the shared type inference library for `PreTypeMention`s. */
243+
module PreM2 = Make2<PreTypeMention, PreInput2>;
210244

211-
module TypePath = M1::TypePath;
245+
private module Input2 implements InputSig2<TypeMention> {
246+
TypeMention getABaseTypeMention(Type t) { none() }
247+
248+
TypeMention getATypeParameterConstraint(TypeParameter tp) {
249+
result = Input2Common::getATypeParameterConstraint(tp)
250+
}
251+
252+
predicate conditionSatisfiesConstraint(
253+
TypeAbstraction abs, TypeMention condition, TypeMention constraint, boolean transitive
254+
) {
255+
Input2Common::conditionSatisfiesConstraint(abs, condition, constraint, transitive)
256+
}
257+
258+
predicate typeAbstractionHasAmbiguousConstraintAt(
259+
TypeAbstraction abs, Type constraint, TypePath path
260+
) {
261+
FunctionOverloading::implHasAmbiguousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
262+
}
263+
264+
predicate typeParameterIsFunctionallyDetermined =
265+
Input2Common::typeParameterIsFunctionallyDetermined/1;
266+
}
267+
268+
private import Input2
212269

213-
private module M2 = Make2<PreTypeMention, Input>;
270+
private module M2 = Make2<TypeMention, Input2>;
214271

215272
import M2
216273

@@ -1070,25 +1127,18 @@ private module ContextTyping {
10701127
AstNode n, FunctionPosition pos, boolean hasReceiver, TypePath path
10711128
) {
10721129
result = inferCallType(n, pos, hasReceiver, path) and
1073-
not pos.isReturn()
1074-
}
1075-
1076-
pragma[nomagic]
1077-
private Type inferCallNonReturnType(
1078-
AstNode n, FunctionPosition pos, boolean hasReceiver, TypePath prefix, TypePath path
1079-
) {
1080-
result = inferCallNonReturnType(n, pos, hasReceiver, path) and
10811130
hasUnknownType(n) and
1082-
prefix = path.getAPrefix()
1131+
not pos.isReturn()
10831132
}
10841133

10851134
pragma[nomagic]
10861135
Type check(AstNode n, TypePath path) {
10871136
result = inferCallType(n, any(FunctionPosition pos | pos.isReturn()), _, path)
10881137
or
10891138
exists(FunctionPosition pos, boolean hasReceiver, TypePath prefix |
1090-
result = inferCallNonReturnType(n, pos, hasReceiver, prefix, path) and
1091-
hasUnknownTypeAt(n, prefix)
1139+
result = inferCallNonReturnType(n, pos, hasReceiver, path) and
1140+
hasUnknownTypeAt(n, prefix) and
1141+
prefix.isPrefixOf(path)
10921142
|
10931143
// Never propagate type information directly into the receiver, since its type
10941144
// must already have been known in order to resolve the call
@@ -3970,7 +4020,7 @@ private module Debug {
39704020
TypeAbstraction abs, TypeMention condition, TypeMention constraint, boolean transitive
39714021
) {
39724022
abs = getRelevantLocatable() and
3973-
Input::conditionSatisfiesConstraint(abs, condition, constraint, transitive)
4023+
Input2::conditionSatisfiesConstraint(abs, condition, constraint, transitive)
39744024
}
39754025

39764026
predicate debugInferShorthandSelfType(ShorthandSelfParameterMention self, TypePath path, Type t) {

0 commit comments

Comments
 (0)