Skip to content

Commit be2a49b

Browse files
hvitvedhvitved
committed
wip
1 parent e14936f commit be2a49b

File tree

6 files changed

+141
-22
lines changed

6 files changed

+141
-22
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/lib/codeql/rust/internal/typeinference/TypeMention.qll‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ private import Type
77
private import TypeAbstraction
88
private import TypeInference
99
private import AssociatedType
10+
private import codeql.util.Unit
1011

1112
bindingset[trait, name]
1213
pragma[inline_late]
@@ -754,6 +755,10 @@ private module PathSatisfiesConstraintInput implements
754755
predicate relevantConstraint(PreTypeMention tm, TraitOrTmTrait constraint) {
755756
pathConcreteTypeAssocType(_, tm, _, constraint, _)
756757
}
758+
759+
class TypeMatchingContext = Unit;
760+
761+
TypeMatchingContext getTypeMatchingContext(PreTypeMention tm) { none() }
757762
}
758763

759764
private module PathSatisfiesConstraint =

‎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: 114 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -126,6 +126,7 @@ overlay[local?]
126126
module;
127127

128128
private import codeql.util.Location
129+
private import codeql.util.Unit
129130

130131
/** Provides the input to `Make1`. */
131132
signature module InputSig1<LocationSig Location> {
@@ -388,7 +389,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
388389

389390
/**
390391
* Holds if the constraint belonging to `abs` with root type `constraint` is
391-
* ambigous at `path`, meaning that there is _some_ other abstraction `abs2`
392+
* ambiguous at `path`, meaning that there is _some_ other abstraction `abs2`
392393
* with a structurally identical condition and same root constraint type
393394
* `constraint`, and where the constraints differ at `path`.
394395
*
@@ -412,9 +413,18 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
412413
* `condition` and `condition2`, and they differ at the path `"T1"`, but
413414
* not at the path `"T2"`.
414415
*/
415-
predicate typeAbstractionHasAmbigousConstraintAt(
416+
predicate typeAbstractionHasAmbiguousConstraintAt(
416417
TypeAbstraction abs, Type constraint, TypePath path
417418
);
419+
420+
/**
421+
* Holds if all instantiations of `tp` are functionally determined by the
422+
* instantiations of the other type parameters in the same abstraction.
423+
*
424+
* For example, in Rust all associated types act as functionally determined
425+
* type parameters.
426+
*/
427+
predicate typeParameterIsFunctionallyDetermined(TypeParameter tp);
418428
}
419429

420430
module Make2<HasTypeTreeSig TypeMention, InputSig2<TypeMention> Input2> {
@@ -691,6 +701,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
691701
* Holds if the type mention `condition` satisfies `constraint` with the
692702
* type `t` at the path `path`.
693703
*/
704+
pragma[nomagic]
694705
predicate conditionSatisfiesConstraintTypeAt(
695706
TypeAbstraction abs, TypeMention condition, TypeMention constraint, TypePath path, Type t
696707
) {
@@ -854,6 +865,19 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
854865
signature module SatisfiesConstraintInputSig<HasTypeTreeSig Term, HasTypeTreeSig Constraint> {
855866
/** Holds if it is relevant to know if `term` satisfies `constraint`. */
856867
predicate relevantConstraint(Term term, Constraint constraint);
868+
869+
class TypeMatchingContext;
870+
871+
TypeMatchingContext getTypeMatchingContext(Term t);
872+
873+
/**
874+
* Holds if `tp` can be matched with the type `t` at `path` in the context of `term`.
875+
*
876+
* This may be used to disambiguate between multiple constraints that `term` may satisfy.
877+
*/
878+
default predicate typeMatch(TypeMatchingContext ctx, TypeParameter tp, TypePath path, Type t) {
879+
none()
880+
}
857881
}
858882

859883
module SatisfiesConstraint<
@@ -975,18 +999,74 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
975999
pragma[nomagic]
9761000
private predicate satisfiesConstraintTypeMention0(
9771001
Term term, Constraint constraint, TypeMention constraintMention, TypeAbstraction abs,
978-
TypeMention sub, TypePath path, Type t, boolean ambigous
1002+
TypeMention sub, TypePath path, Type t, boolean ambiguous
9791003
) {
9801004
exists(Type constraintRoot |
9811005
hasConstraintMention(term, abs, sub, constraint, constraintRoot, constraintMention) and
9821006
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t) and
9831007
if
9841008
exists(TypePath prefix |
985-
typeAbstractionHasAmbigousConstraintAt(abs, constraintRoot, prefix) and
1009+
typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, prefix) and
9861010
prefix.isPrefixOf(path)
9871011
)
988-
then ambigous = true
989-
else ambigous = false
1012+
then ambiguous = true
1013+
else ambiguous = false
1014+
)
1015+
}
1016+
1017+
pragma[nomagic]
1018+
private predicate conditionSatisfiesConstraintTypeAtForDisambiguation(
1019+
TypeAbstraction abs, TypeMention condition, TypeMention constraint, TypePath path, Type t
1020+
) {
1021+
conditionSatisfiesConstraintTypeAt(abs, condition, constraint, path, t) and
1022+
not t instanceof TypeParameter and
1023+
not typeParameterIsFunctionallyDetermined(path.getHead())
1024+
}
1025+
1026+
pragma[nomagic]
1027+
private predicate constraintTypeMatchForDisambiguation0(
1028+
Term term, Constraint constraint, TypePath path, TypePath suffix, TypeParameter tp
1029+
) {
1030+
exists(
1031+
TypeMention constraintMention, TypeAbstraction abs, TypeMention sub, TypePath prefix
1032+
|
1033+
satisfiesConstraintTypeMention0(term, constraint, constraintMention, abs, sub, _, _, true) and
1034+
conditionSatisfiesConstraintTypeAtForDisambiguation(abs, sub, constraintMention, path, _) and
1035+
tp = constraint.getTypeAt(prefix) and
1036+
path = prefix.appendInverse(suffix)
1037+
)
1038+
}
1039+
1040+
pragma[nomagic]
1041+
private predicate constraintTypeMatchForDisambiguation1(
1042+
Term term, Constraint constraint, TypePath path, TypeMatchingContext ctx, TypePath suffix,
1043+
TypeParameter tp
1044+
) {
1045+
constraintTypeMatchForDisambiguation0(term, constraint, path, suffix, tp) and
1046+
ctx = getTypeMatchingContext(term)
1047+
}
1048+
1049+
/**
1050+
* Holds if the type of `constraint` at `path` is `t` because it is possible
1051+
* to match some type parameter that occurs in `constraint` at a prefix of
1052+
* `path` in the context of `term`.
1053+
*
1054+
* For example, if we have
1055+
*
1056+
* ```rust
1057+
* fn f<T1, T2: SomeTrait<T1>>(x: T1, y: T2) -> T2::Output { ... }
1058+
* ```
1059+
*
1060+
* then at a call like `f(true, ...)` the constraint `SomeTrait<T1>` has the
1061+
* type `bool` substituted for `T1`.
1062+
*/
1063+
pragma[nomagic]
1064+
private predicate constraintTypeMatchForDisambiguation(
1065+
Term term, Constraint constraint, TypePath path, Type t
1066+
) {
1067+
exists(TypeMatchingContext ctx, TypeParameter tp, TypePath suffix |
1068+
constraintTypeMatchForDisambiguation1(term, constraint, path, ctx, suffix, tp) and
1069+
typeMatch(ctx, tp, suffix, t)
9901070
)
9911071
}
9921072

@@ -995,20 +1075,24 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
9951075
Term term, Constraint constraint, TypeAbstraction abs, TypeMention sub, TypePath path,
9961076
Type t
9971077
) {
998-
exists(TypeMention constraintMention, boolean ambigous |
1078+
exists(TypeMention constraintMention, boolean ambiguous |
9991079
satisfiesConstraintTypeMention0(term, constraint, constraintMention, abs, sub, path, t,
1000-
ambigous)
1080+
ambiguous)
10011081
|
1002-
if ambigous = true
1082+
if ambiguous = true
10031083
then
10041084
// When the constraint is not uniquely satisfied, we check that the satisfying
10051085
// abstraction is not more specific than the constraint to be satisfied. For example,
10061086
// if the constraint is `MyTrait<i32>` and there is both `impl MyTrait<i32> for ...` and
10071087
// `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)
1088+
forall(TypePath path1, Type t1 |
1089+
conditionSatisfiesConstraintTypeAtForDisambiguation(abs, sub, constraintMention,
1090+
path1, t1)
1091+
|
1092+
t1 = constraint.getTypeAt(path1)
1093+
or
1094+
// The constraint may contain a type parameter, which we can match to the right type
1095+
constraintTypeMatchForDisambiguation(term, constraint, path1, t1)
10121096
)
10131097
else any()
10141098
)
@@ -1142,6 +1226,10 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
11421226
predicate relevantConstraint(Term term, TypeAsTypeTree constraint) {
11431227
Input::relevantConstraint(term, constraint)
11441228
}
1229+
1230+
class TypeMatchingContext = Unit;
1231+
1232+
TypeMatchingContext getTypeMatchingContext(Term t) { none() }
11451233
}
11461234

11471235
import SatisfiesConstraint<Term, TypeAsTypeTree, SatisfiesConstraintInput>
@@ -1367,7 +1455,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
13671455
}
13681456

13691457
private module AccessConstraint {
1370-
predicate relevantAccessConstraint(
1458+
private predicate relevantAccessConstraint(
13711459
Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath path,
13721460
TypeMention constraint
13731461
) {
@@ -1392,6 +1480,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
13921480

13931481
RelevantAccess() { this = MkRelevantAccess(a, apos, e, path) }
13941482

1483+
pragma[nomagic]
13951484
Type getTypeAt(TypePath suffix) {
13961485
result = a.getInferredType(e, apos, path.appendInverse(suffix))
13971486
}
@@ -1414,6 +1503,17 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
14141503
predicate relevantConstraint(RelevantAccess at, TypeMention constraint) {
14151504
constraint = at.getConstraint(_)
14161505
}
1506+
1507+
class TypeMatchingContext = Access;
1508+
1509+
TypeMatchingContext getTypeMatchingContext(RelevantAccess at) {
1510+
at = MkRelevantAccess(result, _, _, _)
1511+
}
1512+
1513+
pragma[nomagic]
1514+
predicate typeMatch(TypeMatchingContext ctx, TypeParameter tp, TypePath path, Type t) {
1515+
typeMatch(ctx, _, _, path, t, tp)
1516+
}
14171517
}
14181518

14191519
private module SatisfiesTypeParameterConstraint =

0 commit comments

Comments
 (0)