Skip to content

Commit 902e953

Browse files
hvitvedhvitved
committed
wip
1 parent ca0fe44 commit 902e953

File tree

4 files changed

+158
-86
lines changed

4 files changed

+158
-86
lines changed

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

Lines changed: 82 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -13,78 +13,98 @@ private import TypeMention
1313
private import TypeInference
1414
private import FunctionType
1515

16-
pragma[nomagic]
17-
private Type resolveNonTypeParameterTypeAt(PreTypeMention tm, TypePath path) {
18-
result = tm.getTypeAt(path) and
19-
not result instanceof TypeParameter
20-
}
16+
signature Type resolveTypeMentionAtSig(AstNode tm, TypePath path);
2117

22-
bindingset[t1, t2]
23-
private predicate typeMentionEqual(PreTypeMention t1, PreTypeMention t2) {
24-
forex(TypePath path, Type type | resolveNonTypeParameterTypeAt(t1, path) = type |
25-
resolveNonTypeParameterTypeAt(t2, path) = type
26-
)
27-
}
18+
private module MkSiblingImpls<resolveTypeMentionAtSig/2 resolveTypeMentionAt> {
19+
pragma[nomagic]
20+
private Type resolveNonTypeParameterTypeAt(AstNode tm, TypePath path) {
21+
result = resolveTypeMentionAt(tm, path) and
22+
not result instanceof TypeParameter
23+
}
2824

29-
pragma[nomagic]
30-
private predicate implSiblingCandidate(
31-
Impl impl, TraitItemNode trait, Type rootType, PreTypeMention selfTy
32-
) {
33-
trait = impl.(ImplItemNode).resolveTraitTy() and
34-
selfTy = impl.getSelfTy() and
35-
rootType = selfTy.getType()
36-
}
25+
bindingset[t1, t2]
26+
private predicate typeMentionEqual(AstNode t1, AstNode t2) {
27+
forex(TypePath path, Type type | resolveNonTypeParameterTypeAt(t1, path) = type |
28+
resolveNonTypeParameterTypeAt(t2, path) = type
29+
)
30+
}
3731

38-
pragma[nomagic]
39-
private predicate blanketImplSiblingCandidate(ImplItemNode impl, Trait trait) {
40-
impl.isBlanketImplementation() and
41-
trait = impl.resolveTraitTy()
42-
}
32+
pragma[nomagic]
33+
private predicate implSiblingCandidate(
34+
Impl impl, TraitItemNode trait, Type rootType, AstNode selfTy
35+
) {
36+
trait = impl.(ImplItemNode).resolveTraitTy() and
37+
selfTy = impl.getSelfTy() and
38+
rootType = resolveTypeMentionAt(selfTy, TypePath::nil())
39+
}
4340

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, PreTypeMention selfTy1, PreTypeMention 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)
41+
pragma[nomagic]
42+
private predicate blanketImplSiblingCandidate(ImplItemNode impl, Trait trait) {
43+
impl.isBlanketImplementation() and
44+
trait = impl.resolveTraitTy()
45+
}
46+
47+
/**
48+
* Holds if `impl1` and `impl2` are a sibling implementations of `trait`. We
49+
* consider implementations to be siblings if they implement the same trait for
50+
* the same type. In that case `Self` is the same type in both implementations,
51+
* and method calls to the implementations cannot be resolved unambiguously
52+
* based only on the receiver type.
53+
*/
54+
pragma[inline]
55+
predicate implSiblings(TraitItemNode trait, Impl impl1, Impl impl2) {
56+
impl1 != impl2 and
57+
(
58+
exists(Type rootType, AstNode selfTy1, AstNode selfTy2 |
59+
implSiblingCandidate(impl1, trait, rootType, selfTy1) and
60+
implSiblingCandidate(impl2, trait, rootType, selfTy2) and
61+
// In principle the second conjunct below should be superflous, but we still
62+
// have ill-formed type mentions for types that we don't understand. For
63+
// those checking both directions restricts further. Note also that we check
64+
// syntactic equality, whereas equality up to renaming would be more
65+
// correct.
66+
typeMentionEqual(selfTy1, selfTy2) and
67+
typeMentionEqual(selfTy2, selfTy1)
68+
)
69+
or
70+
blanketImplSiblingCandidate(impl1, trait) and
71+
blanketImplSiblingCandidate(impl2, trait)
6572
)
66-
or
67-
blanketImplSiblingCandidate(impl1, trait) and
68-
blanketImplSiblingCandidate(impl2, trait)
69-
)
73+
}
74+
75+
/**
76+
* Holds if `impl` is an implementation of `trait` and if another implementation
77+
* exists for the same type.
78+
*/
79+
pragma[nomagic]
80+
predicate implHasSibling(ImplItemNode impl, Trait trait) { implSiblings(trait, impl, _) }
81+
82+
pragma[nomagic]
83+
predicate implHasAmbigousSiblingAt(ImplItemNode impl, Trait trait, TypePath path) {
84+
exists(ImplItemNode impl2, Type t |
85+
implSiblings(trait, impl, impl2) and
86+
t = resolveNonTypeParameterTypeAt(impl.getTraitPath(), path) and
87+
t != resolveNonTypeParameterTypeAt(impl2.getTraitPath(), path)
88+
)
89+
}
7090
}
7191

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, _) }
92+
private Type resolvePreTypeMention(AstNode tm, TypePath path) {
93+
result = tm.(PreTypeMention).getTypeAt(path)
94+
}
7895

79-
pragma[nomagic]
80-
predicate implHasAmbigousSiblingAt(ImplItemNode impl, Trait trait, TypePath path) {
81-
exists(ImplItemNode impl2 |
82-
implSiblings(trait, impl, impl2) and
83-
resolveNonTypeParameterTypeAt(impl.getTraitPath(), path) !=
84-
resolveNonTypeParameterTypeAt(impl2.getTraitPath(), path)
85-
)
96+
private module PreSiblingImpls = MkSiblingImpls<resolvePreTypeMention/2>;
97+
98+
predicate preImplHasAmbigousSiblingAt = PreSiblingImpls::implHasAmbigousSiblingAt/3;
99+
100+
private Type resolveTypeMention(AstNode tm, TypePath path) {
101+
result = tm.(TypeMention).getTypeAt(path)
86102
}
87103

104+
private module SiblingImpls = MkSiblingImpls<resolveTypeMention/2>;
105+
106+
import SiblingImpls
107+
88108
/**
89109
* Holds if `f` is a function declared inside `trait`, and the type of `f` at
90110
* `pos` and `path` is `traitTp`, which is a type parameter of `trait`.

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2827,6 +2827,7 @@ private module FunctionCallMatchingInput implements MatchingWithEnvironmentInput
28272827
}
28282828

28292829
abstract class Access extends ContextTyping::ContextTypedCallCand {
2830+
// Access() { this = Debug::getRelevantLocatable() }
28302831
abstract AstNode getNodeAt(FunctionPosition pos);
28312832

28322833
bindingset[derefChainBorrow]
@@ -4125,7 +4126,7 @@ private module Debug {
41254126
exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
41264127
result.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
41274128
filepath.matches("%/main.rs") and
4128-
startline = 103
4129+
startline = 1751
41294130
)
41304131
}
41314132

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

Lines changed: 11 additions & 3 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 FunctionOverloading
1011

1112
bindingset[trait, name]
1213
pragma[inline_late]
@@ -717,9 +718,9 @@ private class TraitOrTmTrait extends AstNode {
717718
* Holds if `path` accesses an associated type `alias` from `trait` on a
718719
* concrete type given by `tm`.
719720
*
720-
* `implOrTmTrait` is either the mention that resolves to `trait` when `path`
721-
* is of the form `<Type as Trait>::AssocType`, or the enclosing `impl` block
722-
* when `path` is of the form `Self::AssocType`.
721+
* `traitOrTmTrait` is either the mention that resolves to `trait` when `path`
722+
* is of the form `<Type as Trait>::AssocType`, or the trait being implemented
723+
* when `path` is of the form `Self::AssocType` within an `impl` block.
723724
*/
724725
private predicate pathConcreteTypeAssocType(
725726
Path path, PreTypeMention tm, TraitItemNode trait, TraitOrTmTrait traitOrTmTrait, TypeAlias alias
@@ -730,6 +731,7 @@ private predicate pathConcreteTypeAssocType(
730731
|
731732
// path of the form `<Type as Trait>::AssocType`
732733
// ^^^ tm ^^^^^^^^^ name
734+
// ^^^^^ traitOrTmTrait
733735
exists(string name |
734736
pathTypeAsTraitAssoc(path, tm, traitOrTmTrait, trait, name) and
735737
getTraitAssocType(trait, name) = alias
@@ -753,6 +755,12 @@ private module PathSatisfiesConstraintInput implements
753755
predicate relevantConstraint(PreTypeMention tm, TraitOrTmTrait constraint) {
754756
pathConcreteTypeAssocType(_, tm, _, constraint, _)
755757
}
758+
759+
predicate typeAbstractionHasAmbigousConstraintAtOverride(
760+
TypeAbstraction abs, Type constraint, TypePath path
761+
) {
762+
preImplHasAmbigousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
763+
}
756764
}
757765

758766
private module PathSatisfiesConstraint =

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

Lines changed: 63 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -853,6 +853,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
853853
signature module SatisfiesConstraintInputSig<HasTypeTreeSig Term, HasTypeTreeSig Constraint> {
854854
/** Holds if it is relevant to know if `term` satisfies `constraint`. */
855855
predicate relevantConstraint(Term term, Constraint constraint);
856+
857+
default Type foo(Term term, TypeParameter tp, TypePath path) { none() }
858+
859+
default predicate typeAbstractionHasAmbigousConstraintAtOverride(
860+
TypeAbstraction abs, Type constraint, TypePath path
861+
) {
862+
typeAbstractionHasAmbigousConstraintAt(abs, constraint, path)
863+
}
856864
}
857865

858866
module SatisfiesConstraint<
@@ -978,37 +986,68 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
978986
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t)
979987
}
980988

989+
pragma[nomagic]
990+
private predicate satisfiesConstraintTypeMention01(
991+
Term tt, Constraint constraint, TypeAbstraction abs, TypePath prefix, TypeParameter tp
992+
) {
993+
exists(Type constraintRoot |
994+
satisfiesConstraintTypeMention0(tt, constraint, constraintRoot, _, abs, _, _, _) and
995+
typeAbstractionHasAmbigousConstraintAtOverride(abs, constraintRoot, _) and
996+
tp = constraint.getTypeAt(prefix)
997+
)
998+
}
999+
1000+
bindingset[abs, path, t]
1001+
pragma[inline_late]
1002+
private predicate conditionSatisfiesConstraintTypeAtFilter(
1003+
TypeAbstraction abs, TypePath path, Type t
1004+
) {
1005+
conditionSatisfiesConstraintTypeAt(abs, _, _, path, t)
1006+
}
1007+
1008+
pragma[nomagic]
1009+
private Type getConstraintType(Term tt, Constraint constraint, TypePath path) {
1010+
exists(TypeAbstraction abs, TypePath prefix, TypeParameter tp, TypePath suffix |
1011+
satisfiesConstraintTypeMention01(tt, constraint, abs, prefix, tp) and
1012+
result = foo(tt, tp, suffix) and
1013+
path = prefix.append(suffix) and
1014+
conditionSatisfiesConstraintTypeAtFilter(abs, path, result)
1015+
)
1016+
}
1017+
9811018
pragma[nomagic]
9821019
private predicate satisfiesConstraintTypeMention1(
983-
Term tt, Constraint constraint, Type constraintRoot, TypeAbstraction abs, TypeMention sub,
984-
TypePath path, Type t
1020+
Term tt, Constraint constraint, TypeAbstraction abs, TypeMention sub, TypePath path, Type t
9851021
) {
986-
exists(TypeMention constraintMention |
1022+
exists(Type constraintRoot, TypeMention constraintMention |
9871023
satisfiesConstraintTypeMention0(tt, constraint, constraintRoot, constraintMention, abs,
9881024
sub, path, t)
9891025
|
990-
if typeAbstractionHasAmbigousConstraintAt(abs, constraintRoot, path.getAPrefix())
1026+
if typeAbstractionHasAmbigousConstraintAtOverride(abs, constraintRoot, path.getAPrefix())
9911027
then
9921028
// When the constraint is not uniquely satisfied, we check that the satisfying
9931029
// abstraction is not more specific than the constraint to be satisfied. For example,
9941030
// if the constraint is `MyTrait<i32>` and there is both `impl MyTrait<i32> for ...` and
9951031
// `impl MyTrait<i64> for ...`, then the latter will be filtered away
996-
not exists(TypePath path1, Type t1 |
1032+
forall(TypePath path1, Type t1 |
9971033
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path1, t1) and
998-
not t1 instanceof TypeParameter and
999-
t1 != constraint.getTypeAt(path1)
1034+
not t1 instanceof TypeParameter
1035+
|
1036+
not t1 != constraint.getTypeAt(path1)
1037+
or
1038+
t1 = getConstraintType(tt, constraint, path1)
10001039
)
10011040
else any()
10021041
)
10031042
}
10041043

10051044
pragma[inline]
10061045
private predicate satisfiesConstraintTypeMentionInline(
1007-
Term tt, Constraint constraint, Type constraintRoot, TypeAbstraction abs, TypePath path,
1046+
Term tt, Constraint constraint, TypeAbstraction abs, TypePath path,
10081047
TypePath pathToTypeParamInSub
10091048
) {
10101049
exists(TypeMention sub, TypeParameter tp |
1011-
satisfiesConstraintTypeMention1(tt, constraint, constraintRoot, abs, sub, path, tp) and
1050+
satisfiesConstraintTypeMention1(tt, constraint, abs, sub, path, tp) and
10121051
tp = abs.getATypeParameter() and
10131052
sub.getTypeAt(pathToTypeParamInSub) = tp
10141053
)
@@ -1018,24 +1057,22 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10181057
private predicate satisfiesConstraintTypeMention(
10191058
Term tt, Constraint constraint, TypePath path, TypePath pathToTypeParamInSub
10201059
) {
1021-
satisfiesConstraintTypeMentionInline(tt, constraint, _, _, path, pathToTypeParamInSub)
1060+
satisfiesConstraintTypeMentionInline(tt, constraint, _, path, pathToTypeParamInSub)
10221061
}
10231062

10241063
pragma[nomagic]
10251064
private predicate satisfiesConstraintTypeMentionThrough(
1026-
Term tt, TypeAbstraction abs, Constraint constraint, Type constraintRoot, TypePath path,
1065+
Term tt, TypeAbstraction abs, Constraint constraint, TypePath path,
10271066
TypePath pathToTypeParamInSub
10281067
) {
1029-
satisfiesConstraintTypeMentionInline(tt, constraint, constraintRoot, abs, path,
1030-
pathToTypeParamInSub)
1068+
satisfiesConstraintTypeMentionInline(tt, constraint, abs, path, pathToTypeParamInSub)
10311069
}
10321070

10331071
pragma[inline]
10341072
private predicate satisfiesConstraintTypeNonTypeParamInline(
1035-
Term tt, TypeAbstraction abs, Constraint constraint, Type constraintRoot, TypePath path,
1036-
Type t
1073+
Term tt, TypeAbstraction abs, Constraint constraint, TypePath path, Type t
10371074
) {
1038-
satisfiesConstraintTypeMention1(tt, constraint, constraintRoot, abs, _, path, t) and
1075+
satisfiesConstraintTypeMention1(tt, constraint, abs, _, path, t) and
10391076
not t = abs.getATypeParameter()
10401077
}
10411078

@@ -1052,7 +1089,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10521089
*/
10531090
pragma[nomagic]
10541091
predicate satisfiesConstraintType(Term tt, Constraint constraint, TypePath path, Type t) {
1055-
satisfiesConstraintTypeNonTypeParamInline(tt, _, constraint, _, path, t)
1092+
satisfiesConstraintTypeNonTypeParamInline(tt, _, constraint, path, t)
10561093
or
10571094
exists(TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix |
10581095
satisfiesConstraintTypeMention(tt, constraint, prefix0, pathToTypeParamInSub) and
@@ -1072,11 +1109,10 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10721109
predicate satisfiesConstraintTypeThrough(
10731110
Term tt, TypeAbstraction abs, Constraint constraint, TypePath path, Type t
10741111
) {
1075-
satisfiesConstraintTypeNonTypeParamInline(tt, abs, constraint, _, path, t)
1112+
satisfiesConstraintTypeNonTypeParamInline(tt, abs, constraint, path, t)
10761113
or
10771114
exists(TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix |
1078-
satisfiesConstraintTypeMentionThrough(tt, abs, constraint, _, prefix0,
1079-
pathToTypeParamInSub) and
1115+
satisfiesConstraintTypeMentionThrough(tt, abs, constraint, prefix0, pathToTypeParamInSub) and
10801116
getTypeAt(tt, pathToTypeParamInSub.appendInverse(suffix)) = t and
10811117
path = prefix0.append(suffix)
10821118
)
@@ -1405,6 +1441,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
14051441
predicate relevantConstraint(RelevantAccess at, TypeMention constraint) {
14061442
constraint = at.getConstraint(_)
14071443
}
1444+
1445+
Type foo(RelevantAccess at, TypeParameter tp, TypePath path) {
1446+
exists(Access a, AccessEnvironment e, Declaration target |
1447+
at = MkRelevantAccess(a, _, e, _) and
1448+
typeMatch(a, e, target, path, result, tp)
1449+
)
1450+
}
14081451
}
14091452

14101453
predicate satisfiesConstraintType(

0 commit comments

Comments
 (0)