Skip to content

Commit e14936f

Browse files
committed
Rust: Disambiguate types inferred from trait bounds
1 parent 1dcf645 commit e14936f

File tree

7 files changed

+273
-132
lines changed

7 files changed

+273
-132
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 implHasAmbigousSiblingAt(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 preImplHasAmbigousSiblingAt = PreSiblingImpls::implHasAmbigousSiblingAt/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: 66 additions & 24 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
@@ -124,10 +124,28 @@ private module Input implements InputSig1<Location>, InputSig2<PreTypeMention> {
124124
}
125125

126126
int getTypePathLimit() { result = 10 }
127+
}
127128

128-
PreTypeMention getABaseTypeMention(Type t) { none() }
129+
private import Input1
129130

130-
PreTypeMention getATypeParameterConstraint(TypeParameter tp) {
131+
private module M1 = Make1<Location, Input1>;
132+
133+
import M1
134+
135+
predicate getTypePathLimit = Input1::getTypePathLimit/0;
136+
137+
predicate getTypeParameterId = Input1::getTypeParameterId/1;
138+
139+
class TypePath = M1::TypePath;
140+
141+
module TypePath = M1::TypePath;
142+
143+
/**
144+
* Provides shared logic for implementing `InputSig2<PreTypeMention>` and
145+
* `InputSig2<TypeMention>`.
146+
*/
147+
private module Input2Common {
148+
AstNode getATypeParameterConstraint(TypeParameter tp) {
131149
result = tp.(TypeParamTypeParameter).getTypeParam().getATypeBound().getTypeRepr() or
132150
result = tp.(SelfTypeParameter).getTrait() or
133151
result =
@@ -146,7 +164,7 @@ private module Input implements InputSig1<Location>, InputSig2<PreTypeMention> {
146164
* inference module for more information.
147165
*/
148166
predicate conditionSatisfiesConstraint(
149-
TypeAbstraction abs, PreTypeMention condition, PreTypeMention constraint, boolean transitive
167+
TypeAbstraction abs, AstNode condition, AstNode constraint, boolean transitive
150168
) {
151169
// `impl` blocks implementing traits
152170
transitive = false and
@@ -196,21 +214,52 @@ private module Input implements InputSig1<Location>, InputSig2<PreTypeMention> {
196214
}
197215
}
198216

199-
private import Input
217+
private module PreInput2 implements InputSig2<PreTypeMention> {
218+
PreTypeMention getABaseTypeMention(Type t) { none() }
200219

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

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

205-
predicate getTypePathLimit = Input::getTypePathLimit/0;
230+
predicate typeAbstractionHasAmbigousConstraintAt(
231+
TypeAbstraction abs, Type constraint, TypePath path
232+
) {
233+
FunctionOverloading::preImplHasAmbigousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
234+
}
235+
}
206236

207-
predicate getTypeParameterId = Input::getTypeParameterId/1;
237+
/** Provides an instantiation of the shared type inference library for `PreTypeMention`s. */
238+
module PreM2 = Make2<PreTypeMention, PreInput2>;
208239

209-
class TypePath = M1::TypePath;
240+
private module Input2 implements InputSig2<TypeMention> {
241+
TypeMention getABaseTypeMention(Type t) { none() }
210242

211-
module TypePath = M1::TypePath;
243+
TypeMention getATypeParameterConstraint(TypeParameter tp) {
244+
result = Input2Common::getATypeParameterConstraint(tp)
245+
}
212246

213-
private module M2 = Make2<PreTypeMention, Input>;
247+
predicate conditionSatisfiesConstraint(
248+
TypeAbstraction abs, TypeMention condition, TypeMention constraint, boolean transitive
249+
) {
250+
Input2Common::conditionSatisfiesConstraint(abs, condition, constraint, transitive)
251+
}
252+
253+
predicate typeAbstractionHasAmbigousConstraintAt(
254+
TypeAbstraction abs, Type constraint, TypePath path
255+
) {
256+
FunctionOverloading::implHasAmbigousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
257+
}
258+
}
259+
260+
private import Input2
261+
262+
private module M2 = Make2<TypeMention, Input2>;
214263

215264
import M2
216265

@@ -1252,25 +1301,18 @@ private module ContextTyping {
12521301
AstNode n, FunctionPosition pos, boolean hasReceiver, TypePath path
12531302
) {
12541303
result = inferCallType(n, pos, hasReceiver, path) and
1255-
not pos.isReturn()
1256-
}
1257-
1258-
pragma[nomagic]
1259-
private Type inferCallNonReturnType(
1260-
AstNode n, FunctionPosition pos, boolean hasReceiver, TypePath prefix, TypePath path
1261-
) {
1262-
result = inferCallNonReturnType(n, pos, hasReceiver, path) and
12631304
hasUnknownType(n) and
1264-
prefix = path.getAPrefix()
1305+
not pos.isReturn()
12651306
}
12661307

12671308
pragma[nomagic]
12681309
Type check(AstNode n, TypePath path) {
12691310
result = inferCallType(n, any(FunctionPosition pos | pos.isReturn()), _, path)
12701311
or
12711312
exists(FunctionPosition pos, boolean hasReceiver, TypePath prefix |
1272-
result = inferCallNonReturnType(n, pos, hasReceiver, prefix, path) and
1273-
hasUnknownTypeAt(n, prefix)
1313+
result = inferCallNonReturnType(n, pos, hasReceiver, path) and
1314+
hasUnknownTypeAt(n, prefix) and
1315+
prefix.isPrefixOf(path)
12741316
|
12751317
// Never propagate type information directly into the receiver, since its type
12761318
// must already have been known in order to resolve the call
@@ -4137,7 +4179,7 @@ private module Debug {
41374179
TypeAbstraction abs, TypeMention condition, TypeMention constraint, boolean transitive
41384180
) {
41394181
abs = getRelevantLocatable() and
4140-
Input::conditionSatisfiesConstraint(abs, condition, constraint, transitive)
4182+
Input2::conditionSatisfiesConstraint(abs, condition, constraint, transitive)
41414183
}
41424184

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

0 commit comments

Comments
 (0)