Skip to content

Commit 4ab80bd

Browse files
hvitvedhvitved
committed
wip3
1 parent 383e7b6 commit 4ab80bd

File tree

3 files changed

+24
-127
lines changed

3 files changed

+24
-127
lines changed

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

Lines changed: 11 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
4141
trait = impl.resolveTraitTy()
4242
}
4343

44-
private module FooIsInstantiationOfInput implements IsInstantiationOfInputSig<Tm, Tm> {
44+
private module ImplIsInstantiationOfSiblingInput implements IsInstantiationOfInputSig<Tm, Tm> {
4545
predicate potentialInstantiationOf(Tm cond, TypeAbstraction abs, Tm constraint) {
4646
exists(TraitItemNode trait, Type rootType |
4747
implSiblingCandidate(_, trait, rootType, cond) and
@@ -51,25 +51,25 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
5151
}
5252
}
5353

54-
private module FooIsInstantiationOf = IsInstantiationOf<Tm, Tm, FooIsInstantiationOfInput>;
54+
private module ImplIsInstantiationOfSibling =
55+
IsInstantiationOf<Tm, Tm, ImplIsInstantiationOfSiblingInput>;
5556

5657
/**
5758
* Holds if `impl1` and `impl2` are sibling implementations of `trait`. We
58-
* consider implementations to be siblings if they implement the same trait for
59+
* consider implementations to be siblings if they implement the same trait and
60+
* one of the
5961
* the same type. In that case `Self` is the same type in both implementations,
6062
* and method calls to the implementations cannot be resolved unambiguously
6163
* based only on the receiver type.
6264
*/
6365
pragma[inline]
64-
predicate implSiblings(TraitItemNode trait, Impl impl1, Impl impl2) {
65-
// impl1.fromSource() and
66-
// impl1 instanceof Builtins::BuiltinImpl and
66+
predicate implSiblings(TraitItemNode trait, ImplItemNode impl1, ImplItemNode impl2) {
6767
exists(Type rootType, AstNode selfTy1, AstNode selfTy2 |
6868
implSiblingCandidate(impl1, trait, rootType, selfTy1) and
6969
implSiblingCandidate(impl2, trait, rootType, selfTy2)
7070
|
71-
FooIsInstantiationOf::isInstantiationOf(selfTy1, impl2, selfTy2) or
72-
FooIsInstantiationOf::isInstantiationOf(selfTy2, impl1, selfTy1)
71+
ImplIsInstantiationOfSibling::isInstantiationOf(selfTy1, impl2, selfTy2) or
72+
ImplIsInstantiationOfSibling::isInstantiationOf(selfTy2, impl1, selfTy1)
7373
)
7474
or
7575
blanketImplSiblingCandidate(impl1, trait) and
@@ -85,11 +85,8 @@ private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
8585
predicate implHasSibling(ImplItemNode impl, Trait trait) { implSiblings(trait, impl, _) }
8686

8787
pragma[nomagic]
88-
predicate implHasAmbiguousSiblingAt(
89-
ImplItemNode impl, ImplItemNode impl2, Trait trait, TypePath path
90-
) {
91-
// impl instanceof Builtins::BuiltinImpl and
92-
exists(Type t1, Type t2 |
88+
predicate implHasAmbiguousSiblingAt(ImplItemNode impl, Trait trait, TypePath path) {
89+
exists(ImplItemNode impl2, Type t1, Type t2 |
9390
implSiblings(trait, impl, impl2) and
9491
t1 = resolveTypeMentionAt(impl.getTraitPath(), path) and
9592
t2 = resolveTypeMentionAt(impl2.getTraitPath(), path) and
@@ -115,7 +112,7 @@ private Type resolvePreTypeMention(AstNode tm, TypePath path) {
115112

116113
private module PreSiblingImpls = MkSiblingImpls<resolvePreTypeMention/2>;
117114

118-
predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/4;
115+
predicate preImplHasAmbiguousSiblingAt = PreSiblingImpls::implHasAmbiguousSiblingAt/3;
119116

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

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

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -235,10 +235,9 @@ private module PreInput2 implements InputSig2<PreTypeMention> {
235235
}
236236

237237
predicate typeAbstractionHasAmbiguousConstraintAt(
238-
TypeAbstraction abs, Type constraint, TypeAbstraction other, TypePath path
238+
TypeAbstraction abs, Type constraint, TypePath path
239239
) {
240-
FunctionOverloading::preImplHasAmbiguousSiblingAt(abs, other, constraint.(TraitType).getTrait(),
241-
path)
240+
FunctionOverloading::preImplHasAmbiguousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
242241
}
243242

244243
predicate typeParameterIsFunctionallyDetermined =
@@ -262,10 +261,9 @@ private module Input2 implements InputSig2<TypeMention> {
262261
}
263262

264263
predicate typeAbstractionHasAmbiguousConstraintAt(
265-
TypeAbstraction abs, Type constraint, TypeAbstraction other, TypePath path
264+
TypeAbstraction abs, Type constraint, TypePath path
266265
) {
267-
FunctionOverloading::implHasAmbiguousSiblingAt(abs, other, constraint.(TraitType).getTrait(),
268-
path)
266+
FunctionOverloading::implHasAmbiguousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
269267
}
270268

271269
predicate typeParameterIsFunctionallyDetermined =

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

Lines changed: 9 additions & 107 deletions
Original file line numberDiff line numberDiff line change
@@ -415,7 +415,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
415415
* not at the path `"T2"`.
416416
*/
417417
predicate typeAbstractionHasAmbiguousConstraintAt(
418-
TypeAbstraction abs, Type constraint, TypeAbstraction other, TypePath path
418+
TypeAbstraction abs, Type constraint, TypePath path
419419
);
420420

421421
/**
@@ -1027,122 +1027,24 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10271027
)
10281028
}
10291029

1030-
private module TermIsInstantiationOfConditionInput2 implements
1031-
IsInstantiationOfInputSig<Term, TypeMention>
1032-
{
1033-
predicate potentialInstantiationOf(Term term, TypeAbstraction abs, TypeMention cond) {
1034-
TermIsInstantiationOfConditionInput::potentialInstantiationOf(term, abs, cond) and
1035-
exists(
1036-
TypeMention sub, Type constraintRoot, TypeMention constraintMention,
1037-
TypeAbstraction abs2
1038-
|
1039-
hasConstraintMention(term, abs2, sub, _, constraintRoot, constraintMention) and
1040-
conditionSatisfiesConstraintTypeAt(abs2, sub, constraintMention, _, _) and
1041-
typeAbstractionHasAmbiguousConstraintAt(abs2, constraintRoot, abs, _)
1042-
)
1043-
}
1044-
1045-
predicate relevantConstraint(TypeMention constraint) {
1046-
TermIsInstantiationOfConditionInput::relevantConstraint(constraint)
1047-
}
1048-
}
1049-
1050-
private module TermIsInstantiationOfCondition2 =
1051-
IsInstantiationOf<Term, TypeMention, TermIsInstantiationOfConditionInput2>;
1052-
10531030
pragma[nomagic]
10541031
private predicate satisfiesConstraintTypeMention0(
10551032
Term term, Constraint constraint, TypeMention constraintMention, TypeAbstraction abs,
10561033
TypeMention sub, TypePath path, Type t, boolean ambiguous
10571034
) {
10581035
exists(Type constraintRoot |
10591036
hasConstraintMention(term, abs, sub, constraint, constraintRoot, constraintMention) and
1060-
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t)
1061-
|
1062-
exists(TypePath prefix, TypeAbstraction other |
1063-
typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1064-
prefix.isPrefixOf(path) and
1065-
TermIsInstantiationOfCondition2::isInstantiationOf(term, other, _)
1066-
// hasConstraintMention(term, other, _, _, constraintRoot, _)
1067-
) and
1068-
ambiguous = true
1069-
or
1070-
forall(TypePath prefix, TypeAbstraction other |
1071-
typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1072-
prefix.isPrefixOf(path)
1073-
|
1074-
TermIsInstantiationOfCondition2::isNotInstantiationOf(term, other, _, _)
1075-
) and
1076-
ambiguous = false
1037+
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t) and
1038+
if
1039+
exists(TypePath prefix |
1040+
typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, prefix) and
1041+
prefix.isPrefixOf(path)
1042+
)
1043+
then ambiguous = true
1044+
else ambiguous = false
10771045
)
10781046
}
10791047

1080-
// private predicate testsatisfiesConstraintTypeMention0(
1081-
// Term term, Constraint constraint, TypeMention constraintMention, TypeAbstraction abs,
1082-
// TypeMention sub, TypePath path, Type t, boolean ambiguous
1083-
// ) {
1084-
// exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
1085-
// term.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
1086-
// filepath.matches("%/main.rs") and
1087-
// startline = 435
1088-
// ) and
1089-
// satisfiesConstraintTypeMention0(term, constraint, constraintMention, abs, sub, path, t,
1090-
// ambiguous)
1091-
// }
1092-
// private predicate testsatisfiesConstraintTypeMention1(
1093-
// Term term, Constraint constraint, TypeMention constraintMention, TypeAbstraction abs,
1094-
// TypeMention sub, TypePath path, Type t, boolean ambiguous, TypePath prefix,
1095-
// TypeAbstraction other, TypePath path2
1096-
// ) {
1097-
// exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
1098-
// term.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
1099-
// filepath.matches("%/main.rs") and
1100-
// startline = 435
1101-
// ) and
1102-
// exists(Type constraintRoot |
1103-
// hasConstraintMention(term, abs, sub, constraint, constraintRoot, constraintMention) and
1104-
// conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t)
1105-
// |
1106-
// // if
1107-
// // exists(TypePath prefix, TypeAbstraction other |
1108-
// // typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1109-
// // prefix.isPrefixOf(path)
1110-
// // )
1111-
// // then ambiguous = true
1112-
// // else ambiguous = false
1113-
// typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1114-
// // isNotInstantiationOf(term, other, _, constraintRoot) and
1115-
// // TermIsInstantiationOfConditionInput::potentialInstantiationOf(term, other, _) and
1116-
// prefix.isPrefixOf(path) and
1117-
// TermIsInstantiationOfCondition::isNotInstantiationOf(term, other, _, path2) and
1118-
// // not isNotInstantiationOf(term, other, _, constraintRoot) and
1119-
// ambiguous = false
1120-
// // exists(TypePath prefix, TypeAbstraction other |
1121-
// // typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix) and
1122-
// // prefix.isPrefixOf(path) and
1123-
// // hasConstraintMention(term, other, _, _, constraintRoot, _)
1124-
// // ) and
1125-
// // ambiguous = true
1126-
// // or
1127-
// // forall(TypePath prefix, TypeAbstraction other |
1128-
// // typeAbstractionHasAmbiguousConstraintAt(abs, constraintRoot, other, prefix)
1129-
// // |
1130-
// // not prefix.isPrefixOf(path)
1131-
// // or
1132-
// // // exists(Type type | hasTypeConstraint(term, type, constraint, constraintRoot) |
1133-
// // // // countConstraintImplementations(type, constraintRoot) = 0
1134-
// // // // or
1135-
// // // // not rootTypesSatisfaction(type, constraintRoot, _, _, _)
1136-
// // // // or
1137-
// // // multipleConstraintImplementations(type, constraintRoot) and
1138-
// // // isNotInstantiationOf(term, other, _, constraintRoot)
1139-
// // // )
1140-
// // isNotInstantiationOf(term, other, _, constraintRoot)
1141-
// // // TermIsInstantiationOfCondition::isNotInstantiationOf(term, other, _, _)
1142-
// // ) and
1143-
// // ambiguous = false
1144-
// )
1145-
// }
11461048
pragma[nomagic]
11471049
private predicate conditionSatisfiesConstraintTypeAtForDisambiguation(
11481050
TypeAbstraction abs, TypeMention condition, TypeMention constraint, TypePath path, Type t

0 commit comments

Comments
 (0)