@@ -13,68 +13,105 @@ private import TypeMention
1313private import TypeInference
1414private import FunctionType
1515
16- pragma [ nomagic]
17- private Type resolveNonTypeParameterTypeAt ( TypeMention tm , TypePath path ) {
18- result = tm .getTypeAt ( path ) and
19- not result instanceof TypeParameter
20- }
16+ private signature Type resolveTypeMentionAtSig ( AstNode tm , TypePath path ) ;
2117
22- bindingset [ t1, t2]
23- private predicate typeMentionEqual ( TypeMention t1 , TypeMention t2 ) {
24- forex ( TypePath path , Type type | resolveNonTypeParameterTypeAt ( t1 , path ) = type |
25- resolveNonTypeParameterTypeAt ( t2 , path ) = type
26- )
27- }
18+ /**
19+ * Provides logic for identifying sibling implementations, parameterized over
20+ * how to resolve type mentions (`PreTypeMention` vs. `TypeMention`).
21+ */
22+ private module MkSiblingImpls< resolveTypeMentionAtSig / 2 resolveTypeMentionAt> {
23+ pragma [ nomagic]
24+ private Type resolveNonTypeParameterTypeAt ( AstNode tm , TypePath path ) {
25+ result = resolveTypeMentionAt ( tm , path ) and
26+ not result instanceof TypeParameter
27+ }
2828
29- pragma [ nomagic]
30- private predicate implSiblingCandidate (
31- Impl impl , TraitItemNode trait , Type rootType , TypeMention selfTy
32- ) {
33- trait = impl .( ImplItemNode ) .resolveTraitTy ( ) and
34- selfTy = impl .getSelfTy ( ) and
35- rootType = selfTy .getType ( )
29+ bindingset [ t1, t2]
30+ private predicate typeMentionEqual ( AstNode t1 , AstNode t2 ) {
31+ forex ( TypePath path , Type type | resolveNonTypeParameterTypeAt ( t1 , path ) = type |
32+ resolveNonTypeParameterTypeAt ( t2 , path ) = type
33+ )
34+ }
35+
36+ pragma [ nomagic]
37+ private predicate implSiblingCandidate (
38+ Impl impl , TraitItemNode trait , Type rootType , AstNode selfTy
39+ ) {
40+ trait = impl .( ImplItemNode ) .resolveTraitTy ( ) and
41+ selfTy = impl .getSelfTy ( ) and
42+ rootType = resolveTypeMentionAt ( selfTy , TypePath:: nil ( ) )
43+ }
44+
45+ pragma [ nomagic]
46+ private predicate blanketImplSiblingCandidate ( ImplItemNode impl , Trait trait ) {
47+ impl .isBlanketImplementation ( ) and
48+ trait = impl .resolveTraitTy ( )
49+ }
50+
51+ /**
52+ * Holds if `impl1` and `impl2` are a sibling implementations of `trait`. We
53+ * consider implementations to be siblings if they implement the same trait for
54+ * the same type. In that case `Self` is the same type in both implementations,
55+ * and method calls to the implementations cannot be resolved unambiguously
56+ * based only on the receiver type.
57+ */
58+ pragma [ inline]
59+ predicate implSiblings ( TraitItemNode trait , Impl impl1 , Impl impl2 ) {
60+ impl1 != impl2 and
61+ (
62+ exists ( Type rootType , AstNode selfTy1 , AstNode selfTy2 |
63+ implSiblingCandidate ( impl1 , trait , rootType , selfTy1 ) and
64+ implSiblingCandidate ( impl2 , trait , rootType , selfTy2 ) and
65+ // In principle the second conjunct below should be superflous, but we still
66+ // have ill-formed type mentions for types that we don't understand. For
67+ // those checking both directions restricts further. Note also that we check
68+ // syntactic equality, whereas equality up to renaming would be more
69+ // correct.
70+ typeMentionEqual ( selfTy1 , selfTy2 ) and
71+ typeMentionEqual ( selfTy2 , selfTy1 )
72+ )
73+ or
74+ blanketImplSiblingCandidate ( impl1 , trait ) and
75+ blanketImplSiblingCandidate ( impl2 , trait )
76+ )
77+ }
78+
79+ /**
80+ * Holds if `impl` is an implementation of `trait` and if another implementation
81+ * exists for the same type.
82+ */
83+ pragma [ nomagic]
84+ predicate implHasSibling ( ImplItemNode impl , Trait trait ) { implSiblings ( trait , impl , _) }
85+
86+ pragma [ nomagic]
87+ predicate implHasAmbigousSiblingAt ( ImplItemNode impl , Trait trait , TypePath path ) {
88+ exists ( ImplItemNode impl2 , Type t1 , Type t2 |
89+ implSiblings ( trait , impl , impl2 ) and
90+ t1 = resolveTypeMentionAt ( impl .getTraitPath ( ) , path ) and
91+ t2 = resolveTypeMentionAt ( impl2 .getTraitPath ( ) , path ) and
92+ t1 != t2
93+ |
94+ not t1 instanceof TypeParameter or
95+ not t2 instanceof TypeParameter
96+ )
97+ }
3698}
3799
38- pragma [ nomagic]
39- private predicate blanketImplSiblingCandidate ( ImplItemNode impl , Trait trait ) {
40- impl .isBlanketImplementation ( ) and
41- trait = impl .resolveTraitTy ( )
100+ private Type resolvePreTypeMention ( AstNode tm , TypePath path ) {
101+ result = tm .( PreTypeMention ) .getTypeAt ( path )
42102}
43103
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 , TypeMention selfTy1 , TypeMention 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 )
65- )
66- or
67- blanketImplSiblingCandidate ( impl1 , trait ) and
68- blanketImplSiblingCandidate ( impl2 , trait )
69- )
104+ private module PreSiblingImpls = MkSiblingImpls< resolvePreTypeMention / 2 > ;
105+
106+ predicate preImplHasAmbigousSiblingAt = PreSiblingImpls:: implHasAmbigousSiblingAt / 3 ;
107+
108+ private Type resolveTypeMention ( AstNode tm , TypePath path ) {
109+ result = tm .( TypeMention ) .getTypeAt ( path )
70110}
71111
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 , _) }
112+ private module SiblingImpls = MkSiblingImpls< resolveTypeMention / 2 > ;
113+
114+ import SiblingImpls
78115
79116/**
80117 * Holds if `f` is a function declared inside `trait`, and the type of `f` at
0 commit comments