Skip to content

Commit 98a7ca6

Browse files
hvitvedhvitved
committed
wip
1 parent e14936f commit 98a7ca6

File tree

5 files changed

+116
-26
lines changed

5 files changed

+116
-26
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
8484
predicate implHasSibling(ImplItemNode impl, Trait trait) { implSiblings(trait, impl, _) }
8585

8686
pragma[nomagic]
87-
predicate implHasAmbigousSiblingAt(ImplItemNode impl, Trait trait, TypePath path) {
87+
predicate implHasAmbiguousSiblingAt(ImplItemNode impl, Trait trait, TypePath path) {
8888
exists(ImplItemNode impl2, Type t1, Type t2 |
8989
implSiblings(trait, impl, impl2) and
9090
t1 = resolveTypeMentionAt(impl.getTraitPath(), path) and
@@ -103,7 +103,7 @@ private Type resolvePreTypeMention(AstNode tm, TypePath path) {
103103

104104
private module PreSiblingImpls = MkSiblingImpls<resolvePreTypeMention/2>;
105105

106-
predicate preImplHasAmbigousSiblingAt = PreSiblingImpls::implHasAmbigousSiblingAt/3;
106+
predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/3;
107107

108108
private Type resolveTypeMention(AstNode tm, TypePath path) {
109109
result = tm.(TypeMention).getTypeAt(path)

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

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -212,6 +212,10 @@ private module Input2Common {
212212
)
213213
)
214214
}
215+
216+
predicate typeParameterIsFunctionallyDetermined(TypeParameter tp) {
217+
tp instanceof AssociatedTypeTypeParameter
218+
}
215219
}
216220

217221
private module PreInput2 implements InputSig2<PreTypeMention> {
@@ -227,11 +231,14 @@ private module PreInput2 implements InputSig2<PreTypeMention> {
227231
Input2Common::conditionSatisfiesConstraint(abs, condition, constraint, transitive)
228232
}
229233

230-
predicate typeAbstractionHasAmbigousConstraintAt(
234+
predicate typeAbstractionHasAmbiguousConstraintAt(
231235
TypeAbstraction abs, Type constraint, TypePath path
232236
) {
233-
FunctionOverloading::preImplHasAmbigousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
237+
FunctionOverloading::preImplHasAmbiguousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
234238
}
239+
240+
predicate typeParameterIsFunctionallyDetermined =
241+
Input2Common::typeParameterIsFunctionallyDetermined/1;
235242
}
236243

237244
/** Provides an instantiation of the shared type inference library for `PreTypeMention`s. */
@@ -250,11 +257,14 @@ private module Input2 implements InputSig2<TypeMention> {
250257
Input2Common::conditionSatisfiesConstraint(abs, condition, constraint, transitive)
251258
}
252259

253-
predicate typeAbstractionHasAmbigousConstraintAt(
260+
predicate typeAbstractionHasAmbiguousConstraintAt(
254261
TypeAbstraction abs, Type constraint, TypePath path
255262
) {
256-
FunctionOverloading::implHasAmbigousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
263+
FunctionOverloading::implHasAmbiguousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
257264
}
265+
266+
predicate typeParameterIsFunctionallyDetermined =
267+
Input2Common::typeParameterIsFunctionallyDetermined/1;
258268
}
259269

260270
private import Input2

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -516,8 +516,8 @@ mod trait_bound_impl_overlap {
516516
let y = call_f::<i32, _>(x); // $ target=call_f type=y:i32
517517

518518
let x = S(0);
519-
let y = call_f2(S(0i32), x); // $ target=call_f2 $ MISSING: type=y:i32
519+
let y = call_f2(S(0i32), x); // $ target=call_f2 type=y:i32
520520
let x = S(0);
521-
let y = call_f2(S(0i64), x); // $ target=call_f2 $ MISSING: type=y:i64
521+
let y = call_f2(S(0i64), x); // $ target=call_f2 type=y:i64
522522
}
523523
}

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12948,6 +12948,8 @@ inferType
1294812948
| overloading.rs:518:17:518:20 | S(...) | | overloading.rs:464:5:464:19 | S |
1294912949
| overloading.rs:518:17:518:20 | S(...) | T | {EXTERNAL LOCATION} | i32 |
1295012950
| overloading.rs:518:19:518:19 | 0 | | {EXTERNAL LOCATION} | i32 |
12951+
| overloading.rs:519:13:519:13 | y | | {EXTERNAL LOCATION} | i32 |
12952+
| overloading.rs:519:17:519:35 | call_f2(...) | | {EXTERNAL LOCATION} | i32 |
1295112953
| overloading.rs:519:25:519:31 | S(...) | | overloading.rs:464:5:464:19 | S |
1295212954
| overloading.rs:519:25:519:31 | S(...) | T | {EXTERNAL LOCATION} | i32 |
1295312955
| overloading.rs:519:27:519:30 | 0i32 | | {EXTERNAL LOCATION} | i32 |
@@ -12958,6 +12960,8 @@ inferType
1295812960
| overloading.rs:520:17:520:20 | S(...) | | overloading.rs:464:5:464:19 | S |
1295912961
| overloading.rs:520:17:520:20 | S(...) | T | {EXTERNAL LOCATION} | i32 |
1296012962
| overloading.rs:520:19:520:19 | 0 | | {EXTERNAL LOCATION} | i32 |
12963+
| overloading.rs:521:13:521:13 | y | | {EXTERNAL LOCATION} | i64 |
12964+
| overloading.rs:521:17:521:35 | call_f2(...) | | {EXTERNAL LOCATION} | i64 |
1296112965
| overloading.rs:521:25:521:31 | S(...) | | overloading.rs:464:5:464:19 | S |
1296212966
| overloading.rs:521:25:521:31 | S(...) | T | {EXTERNAL LOCATION} | i64 |
1296312967
| overloading.rs:521:27:521:30 | 0i64 | | {EXTERNAL LOCATION} | i64 |

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

Lines changed: 94 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -388,7 +388,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
388388

389389
/**
390390
* Holds if the constraint belonging to `abs` with root type `constraint` is
391-
* ambigous at `path`, meaning that there is _some_ other abstraction `abs2`
391+
* ambiguous at `path`, meaning that there is _some_ other abstraction `abs2`
392392
* with a structurally identical condition and same root constraint type
393393
* `constraint`, and where the constraints differ at `path`.
394394
*
@@ -412,9 +412,18 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
412412
* `condition` and `condition2`, and they differ at the path `"T1"`, but
413413
* not at the path `"T2"`.
414414
*/
415-
predicate typeAbstractionHasAmbigousConstraintAt(
415+
predicate typeAbstractionHasAmbiguousConstraintAt(
416416
TypeAbstraction abs, Type constraint, TypePath path
417417
);
418+
419+
/**
420+
* Holds if all instantiations of `tp` are functionally determined by the
421+
* instantiations of the other type parameters in the same abstraction.
422+
*
423+
* For example, in Rust all associated types act as functionally determined
424+
* type parameters.
425+
*/
426+
predicate typeParameterIsFunctionallyDetermined(TypeParameter tp);
418427
}
419428

420429
module Make2<HasTypeTreeSig TypeMention, InputSig2<TypeMention> Input2> {
@@ -691,6 +700,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
691700
* Holds if the type mention `condition` satisfies `constraint` with the
692701
* type `t` at the path `path`.
693702
*/
703+
pragma[nomagic]
694704
predicate conditionSatisfiesConstraintTypeAt(
695705
TypeAbstraction abs, TypeMention condition, TypeMention constraint, TypePath path, Type t
696706
) {
@@ -854,6 +864,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
854864
signature module SatisfiesConstraintInputSig<HasTypeTreeSig Term, HasTypeTreeSig Constraint> {
855865
/** Holds if it is relevant to know if `term` satisfies `constraint`. */
856866
predicate relevantConstraint(Term term, Constraint constraint);
867+
868+
/**
869+
* Holds if `tp` can be matched with the type `t` at `path` in the context of `term`.
870+
*
871+
* This may be used to disambiguate between multiple constraints that `term` may satisfy.
872+
*/
873+
bindingset[term, tp]
874+
default predicate typeMatch(Term term, TypeParameter tp, TypePath path, Type t) { none() }
857875
}
858876

859877
module SatisfiesConstraint<
@@ -975,18 +993,63 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
975993
pragma[nomagic]
976994
private predicate satisfiesConstraintTypeMention0(
977995
Term term, Constraint constraint, TypeMention constraintMention, TypeAbstraction abs,
978-
TypeMention sub, TypePath path, Type t, boolean ambigous
996+
TypeMention sub, TypePath path, Type t, boolean ambiguous
979997
) {
980998
exists(Type constraintRoot |
981999
hasConstraintMention(term, abs, sub, constraint, constraintRoot, constraintMention) and
9821000
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t) and
9831001
if
9841002
exists(TypePath prefix |
985-
typeAbstractionHasAmbigousConstraintAt(abs, constraintRoot, prefix) and
1003+
typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, prefix) and
9861004
prefix.isPrefixOf(path)
9871005
)
988-
then ambigous = true
989-
else ambigous = false
1006+
then ambiguous = true
1007+
else ambiguous = false
1008+
)
1009+
}
1010+
1011+
pragma[nomagic]
1012+
private predicate conditionSatisfiesConstraintTypeAtForDisambiguation(
1013+
TypeAbstraction abs, TypeMention condition, TypeMention constraint, TypePath path, Type t
1014+
) {
1015+
conditionSatisfiesConstraintTypeAt(abs, condition, constraint, path, t) and
1016+
not t instanceof TypeParameter and
1017+
not typeParameterIsFunctionallyDetermined(path.getHead())
1018+
}
1019+
1020+
pragma[nomagic]
1021+
private predicate constraintTypeMatchForDisambiguation0(
1022+
Term term, Constraint constraint, TypePath path
1023+
) {
1024+
exists(TypeMention constraintMention, TypeAbstraction abs, TypeMention sub |
1025+
satisfiesConstraintTypeMention0(term, constraint, constraintMention, abs, sub, _, _, true) and
1026+
conditionSatisfiesConstraintTypeAtForDisambiguation(abs, sub, constraintMention, path, _)
1027+
)
1028+
}
1029+
1030+
/**
1031+
* Holds if the type of `constraint` at `path` is `t` because it is possible
1032+
* to match some type parameter that occurs in `constraint` at a prefix of
1033+
* `path` in the context of `term`.
1034+
*
1035+
* For example, if we have
1036+
*
1037+
* ```rust
1038+
* fn f<T1, T2: SomeTrait<T1>>(x: T1, y: T2) -> T2::Output { ... }
1039+
* ```
1040+
*
1041+
* then at a call like `f(true, ...)` the constraint `SomeTrait<T1>` has the
1042+
* type `bool` substituted for `T1`.
1043+
*/
1044+
pragma[nomagic]
1045+
private predicate constraintTypeMatchForDisambiguation(
1046+
Term term, Constraint constraint, TypePath path, Type t
1047+
) {
1048+
constraintTypeMatchForDisambiguation0(term, constraint, path) and
1049+
exists(TypeParameter tp, TypePath prefix, TypePath suffix |
1050+
tp = constraint.getTypeAt(prefix) and
1051+
typeMatch(term, tp, suffix, t) and
1052+
path = prefix.append(suffix)
9901053
)
9911054
}
9921055

@@ -995,20 +1058,24 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
9951058
Term term, Constraint constraint, TypeAbstraction abs, TypeMention sub, TypePath path,
9961059
Type t
9971060
) {
998-
exists(TypeMention constraintMention, boolean ambigous |
1061+
exists(TypeMention constraintMention, boolean ambiguous |
9991062
satisfiesConstraintTypeMention0(term, constraint, constraintMention, abs, sub, path, t,
1000-
ambigous)
1063+
ambiguous)
10011064
|
1002-
if ambigous = true
1065+
if ambiguous = true
10031066
then
10041067
// When the constraint is not uniquely satisfied, we check that the satisfying
10051068
// abstraction is not more specific than the constraint to be satisfied. For example,
10061069
// if the constraint is `MyTrait<i32>` and there is both `impl MyTrait<i32> for ...` and
10071070
// `impl MyTrait<i64> for ...`, then the latter will be filtered away
1008-
not exists(TypePath path1, Type t1 |
1009-
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path1, t1) and
1010-
not t1 instanceof TypeParameter and
1011-
t1 != constraint.getTypeAt(path1)
1071+
forall(TypePath path1, Type t1 |
1072+
conditionSatisfiesConstraintTypeAtForDisambiguation(abs, sub, constraintMention,
1073+
path1, t1)
1074+
|
1075+
t1 = constraint.getTypeAt(path1)
1076+
or
1077+
// The constraint may contain a type parameter, which we can match to the right type
1078+
constraintTypeMatchForDisambiguation(term, constraint, path1, t1)
10121079
)
10131080
else any()
10141081
)
@@ -1367,7 +1434,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
13671434
}
13681435

13691436
private module AccessConstraint {
1370-
predicate relevantAccessConstraint(
1437+
private predicate relevantAccessConstraint(
13711438
Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath path,
13721439
TypeMention constraint
13731440
) {
@@ -1376,7 +1443,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
13761443
}
13771444

13781445
private newtype TRelevantAccess =
1379-
MkRelevantAccess(Access a, AccessPosition apos, AccessEnvironment e, TypePath path) {
1446+
MkRelevantAccess(Access a, AccessEnvironment e, AccessPosition apos, TypePath path) {
13801447
relevantAccessConstraint(a, e, _, apos, path, _)
13811448
}
13821449

@@ -1386,12 +1453,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
13861453
*/
13871454
private class RelevantAccess extends MkRelevantAccess {
13881455
Access a;
1389-
AccessPosition apos;
13901456
AccessEnvironment e;
1457+
AccessPosition apos;
13911458
TypePath path;
13921459

1393-
RelevantAccess() { this = MkRelevantAccess(a, apos, e, path) }
1460+
RelevantAccess() { this = MkRelevantAccess(a, e, apos, path) }
13941461

1462+
pragma[nomagic]
13951463
Type getTypeAt(TypePath suffix) {
13961464
result = a.getInferredType(e, apos, path.appendInverse(suffix))
13971465
}
@@ -1414,6 +1482,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
14141482
predicate relevantConstraint(RelevantAccess at, TypeMention constraint) {
14151483
constraint = at.getConstraint(_)
14161484
}
1485+
1486+
bindingset[at, tp]
1487+
predicate typeMatch(RelevantAccess at, TypeParameter tp, TypePath path, Type t) {
1488+
exists(Access a, AccessEnvironment e |
1489+
at = MkRelevantAccess(a, e, _, _) and
1490+
typeMatch(a, e, _, path, t, tp)
1491+
)
1492+
}
14171493
}
14181494

14191495
private module SatisfiesTypeParameterConstraint =
@@ -1424,7 +1500,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
14241500
TypeMention constraint, TypePath path, Type t
14251501
) {
14261502
exists(RelevantAccess ra |
1427-
ra = MkRelevantAccess(a, apos, e, prefix) and
1503+
ra = MkRelevantAccess(a, e, apos, prefix) and
14281504
SatisfiesTypeParameterConstraint::satisfiesConstraintType(ra, constraint, path, t) and
14291505
constraint = ra.getConstraint(target)
14301506
)

0 commit comments

Comments
 (0)