Skip to content

Commit a4e5c79

Browse files
hvitvedhvitved
committed
Rust: Refine implHasAmbiguousSiblingAt 
1 parent 33cc887 commit a4e5c79

File tree

4 files changed

+152
-24
lines changed

4 files changed

+152
-24
lines changed

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

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

8686
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
87+
predicate implHasAmbiguousSiblingAt(
88+
ImplItemNode impl, ImplItemNode impl2, Trait trait, TypePath path
89+
) {
90+
// impl.fromSource() and
91+
exists(Type t1, Type t2 |
92+
(
93+
implSiblings(trait, impl, impl2)
94+
or
95+
exists(Type rootType, AstNode selfTy1, AstNode selfTy2 |
96+
implSiblingCandidate(impl, trait, rootType, selfTy1) and
97+
implSiblingCandidate(impl2, trait, rootType, selfTy2) and
98+
impl != impl2
99+
|
100+
// In principle the second conjunct below should be superfluous, but we still
101+
// have ill-formed type mentions for types that we don't understand. For
102+
// those checking both directions restricts further. Note also that we check
103+
// syntactic equality, whereas equality up to renaming would be more
104+
// correct.
105+
forex(TypePath path1, Type t1_ | t1_ = resolveNonTypeParameterTypeAt(selfTy1, path1) |
106+
not t1_ != resolveNonTypeParameterTypeAt(selfTy2, path1)
107+
)
108+
or
109+
forex(TypePath path2, Type t2_ | t2_ = resolveNonTypeParameterTypeAt(selfTy2, path2) |
110+
not t2_ != resolveNonTypeParameterTypeAt(selfTy1, path2)
111+
)
112+
)
113+
) and
90114
t1 = resolveTypeMentionAt(impl.getTraitPath(), path) and
91115
t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) and
92116
t1 != t2
@@ -103,7 +127,7 @@ private Type resolvePreTypeMention(AstNode tm, TypePath path) {
103127

104128
private module PreSiblingImpls = MkSiblingImpls<resolvePreTypeMention/2>;
105129

106-
predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/3;
130+
predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/4;
107131

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

‎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 =
@@ -2143,6 +2150,17 @@ private module AssocFunctionResolution {
21432150
)
21442151
}
21452152

2153+
// private AssocFunctionDeclaration testresolveCallTarget(
2154+
// ImplOrTraitItemNode i, FunctionPosition selfPos, DerefChain derefChain, BorrowKind borrow,
2155+
// FunctionPosition pos, TypePath path, Type t
2156+
// ) {
2157+
// this = Debug::getRelevantLocatable() and
2158+
// exists(AssocFunctionCallCand afcc |
2159+
// afcc = MkAssocFunctionCallCand(this, selfPos, derefChain, borrow) and
2160+
// result = afcc.resolveCallTarget(i) and
2161+
// t = result.getParameterType(any(ImplOrTraitItemNodeOption o | o.asSome() = i), pos, path)
2162+
// )
2163+
// }
21462164
/**
21472165
* Holds if the argument `arg` of this call has been implicitly dereferenced
21482166
* and borrowed according to `derefChain` and `borrow`, in order to be able to
@@ -4034,7 +4052,7 @@ private module Debug {
40344052
exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
40354053
result.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
40364054
filepath.matches("%/main.rs") and
4037-
startline = 103
4055+
startline = 441
40384056
)
40394057
}
40404058

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

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -15810,18 +15810,12 @@ inferType
1581015810
| regressions.rs:150:24:153:5 | { ... } | | regressions.rs:136:5:136:22 | S2 |
1581115811
| regressions.rs:150:24:153:5 | { ... } | T2 | regressions.rs:135:5:135:14 | S1 |
1581215812
| regressions.rs:151:13:151:13 | x | | regressions.rs:136:5:136:22 | S2 |
15813-
| regressions.rs:151:13:151:13 | x | T2 | {EXTERNAL LOCATION} | & |
1581415813
| regressions.rs:151:13:151:13 | x | T2 | regressions.rs:135:5:135:14 | S1 |
15815-
| regressions.rs:151:13:151:13 | x | T2.TRef | regressions.rs:135:5:135:14 | S1 |
1581615814
| regressions.rs:151:17:151:18 | S1 | | regressions.rs:135:5:135:14 | S1 |
1581715815
| regressions.rs:151:17:151:25 | S1.into() | | regressions.rs:136:5:136:22 | S2 |
15818-
| regressions.rs:151:17:151:25 | S1.into() | T2 | {EXTERNAL LOCATION} | & |
1581915816
| regressions.rs:151:17:151:25 | S1.into() | T2 | regressions.rs:135:5:135:14 | S1 |
15820-
| regressions.rs:151:17:151:25 | S1.into() | T2.TRef | regressions.rs:135:5:135:14 | S1 |
1582115817
| regressions.rs:152:9:152:9 | x | | regressions.rs:136:5:136:22 | S2 |
15822-
| regressions.rs:152:9:152:9 | x | T2 | {EXTERNAL LOCATION} | & |
1582315818
| regressions.rs:152:9:152:9 | x | T2 | regressions.rs:135:5:135:14 | S1 |
15824-
| regressions.rs:152:9:152:9 | x | T2.TRef | regressions.rs:135:5:135:14 | S1 |
1582515819
| regressions.rs:164:16:164:19 | SelfParam | | regressions.rs:158:5:158:19 | S |
1582615820
| regressions.rs:164:16:164:19 | SelfParam | T | regressions.rs:160:10:160:10 | T |
1582715821
| regressions.rs:164:22:164:25 | _rhs | | regressions.rs:158:5:158:19 | S |
@@ -15853,3 +15847,4 @@ inferType
1585315847
| regressions.rs:179:24:179:27 | S(...) | T | {EXTERNAL LOCATION} | i32 |
1585415848
| regressions.rs:179:26:179:26 | 1 | | {EXTERNAL LOCATION} | i32 |
1585515849
testFailures
15850+
| 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)