@@ -77,32 +77,23 @@ pragma[nomagic]
7777private predicate implHasSibling ( ImplItemNode impl , Trait trait ) { implSiblings ( trait , impl , _) }
7878
7979/**
80- * Holds if type parameter `tp` of `trait` occurs in the function `f` with the name
81- * `functionName` at position `pos` and path `path`.
82- *
83- * Note that `pos` can also be the special `return` position, which is sometimes
84- * needed to disambiguate associated function calls like `Default::default()`
85- * (in this case, `tp` is the special `Self` type parameter).
80+ * Holds if `f` is a function declared inside `trait`, and the type of `f` at
81+ * `pos` and `path` is `traitTp`, which is a type parameter of `trait`.
8682 */
87- bindingset [ trait]
88- pragma [ inline_late]
83+ pragma [ nomagic]
8984predicate traitTypeParameterOccurrence (
9085 TraitItemNode trait , Function f , string functionName , FunctionPosition pos , TypePath path ,
91- TypeParameter tp
86+ TypeParameter traitTp
9287) {
93- f = trait .getASuccessor ( functionName ) and
94- tp = getAssocFunctionTypeAt ( f , trait , pos , path ) and
95- tp = trait .( TraitTypeAbstraction ) .getATypeParameter ( )
88+ f = trait .getAssocItem ( functionName ) and
89+ traitTp = getAssocFunctionTypeInclNonMethodSelfAt ( f , trait , pos , path ) and
90+ traitTp = trait .( TraitTypeAbstraction ) .getATypeParameter ( )
9691}
9792
98- /**
99- * Holds if resolving the function `f` in `impl` with the name `functionName`
100- * requires inspecting the type of applied _arguments_ at position `pos` in
101- * order to determine whether it is the correct resolution.
102- */
10393pragma [ nomagic]
104- predicate functionResolutionDependsOnArgument (
105- ImplItemNode impl , Function f , FunctionPosition pos , TypePath path , Type type
94+ private predicate functionResolutionDependsOnArgumentCand (
95+ ImplItemNode impl , Function f , string functionName , TypeParameter traitTp , FunctionPosition pos ,
96+ TypePath path
10697) {
10798 /*
10899 * As seen in the example below, when an implementation has a sibling for a
@@ -129,11 +120,114 @@ predicate functionResolutionDependsOnArgument(
129120 * method. In that case we will still resolve several methods.
130121 */
131122
132- exists ( TraitItemNode trait , string functionName |
123+ exists ( TraitItemNode trait |
133124 implHasSibling ( impl , trait ) and
134- traitTypeParameterOccurrence ( trait , _, functionName , pos , path , _) and
135- type = getAssocFunctionTypeAt ( f , impl , pos , path ) and
125+ traitTypeParameterOccurrence ( trait , _, functionName , pos , path , traitTp ) and
136126 f = impl .getASuccessor ( functionName ) and
127+ not pos .isSelf ( )
128+ )
129+ }
130+
131+ private predicate functionResolutionDependsOnPositionalArgumentCand (
132+ ImplItemNode impl , Function f , string functionName , TypeParameter traitTp
133+ ) {
134+ exists ( FunctionPosition pos |
135+ functionResolutionDependsOnArgumentCand ( impl , f , functionName , traitTp , pos , _) and
136+ pos .isPosition ( )
137+ )
138+ }
139+
140+ pragma [ nomagic]
141+ private Type getAssocFunctionNonTypeParameterTypeAt (
142+ ImplItemNode impl , Function f , FunctionPosition pos , TypePath path
143+ ) {
144+ result = getAssocFunctionTypeInclNonMethodSelfAt ( f , impl , pos , path ) and
145+ not result instanceof TypeParameter
146+ }
147+
148+ /**
149+ * Holds if `f` inside `impl` has a sibling implementation inside `sibling`, where
150+ * those two implementations agree on the instantiation of `traitTp`, which occurs
151+ * in a positional position inside `f`.
152+ */
153+ pragma [ nomagic]
154+ private predicate hasEquivalentPositionalSibling (
155+ ImplItemNode impl , ImplItemNode sibling , Function f , TypeParameter traitTp
156+ ) {
157+ exists ( string functionName , FunctionPosition pos , TypePath path |
158+ functionResolutionDependsOnArgumentCand ( impl , f , functionName , traitTp , pos , path ) and
137159 pos .isPosition ( )
160+ |
161+ exists ( Function f1 |
162+ implSiblings ( _, impl , sibling ) and
163+ f1 = sibling .getASuccessor ( functionName )
164+ |
165+ forall ( TypePath path0 , Type t |
166+ t = getAssocFunctionNonTypeParameterTypeAt ( impl , f , pos , path0 ) and
167+ path = path0 .getAPrefix ( )
168+ |
169+ t = getAssocFunctionNonTypeParameterTypeAt ( sibling , f1 , pos , path0 )
170+ ) and
171+ forall ( TypePath path0 , Type t |
172+ t = getAssocFunctionNonTypeParameterTypeAt ( sibling , f1 , pos , path0 ) and
173+ path = path0 .getAPrefix ( )
174+ |
175+ t = getAssocFunctionNonTypeParameterTypeAt ( impl , f , pos , path0 )
176+ )
177+ )
178+ )
179+ }
180+
181+ /**
182+ * Holds if resolving the function `f` in `impl` requires inspecting the type
183+ * of applied _arguments_ or possibly knowing the return type.
184+ *
185+ * `traitTp` is a type parameter of the trait being implemented by `impl`, and
186+ * we need to check that the type of `f` corresponding to `traitTp` is satisfied
187+ * at any one of the positions `pos` in which that type occurs in `f`.
188+ *
189+ * Type parameters that only occur in return positions are only included when
190+ * all other type parameters that occur in a positional position are insufficient
191+ * to disambiguate.
192+ *
193+ * Example:
194+ *
195+ * ```rust
196+ * trait Trait1<T1> {
197+ * fn f(self, x: T1) -> T1;
198+ * }
199+ *
200+ * impl Trait1<i32> for i32 {
201+ * fn f(self, x: i32) -> i32 { 0 } // f1
202+ * }
203+ *
204+ * impl Trait1<i64> for i32 {
205+ * fn f(self, x: i64) -> i64 { 0 } // f2
206+ * }
207+ * ```
208+ *
209+ * The type for `T1` above occurs in both a positional position and a return position
210+ * in `f`, so both may be used to disambiguate between `f1` and `f2`. That is, `f(0i32)`
211+ * is sufficient to resolve to `f1`, and so is `let y: i64 = f(Default::default())`.
212+ */
213+ pragma [ nomagic]
214+ predicate functionResolutionDependsOnArgument (
215+ ImplItemNode impl , Function f , TypeParameter traitTp , FunctionPosition pos
216+ ) {
217+ exists ( string functionName |
218+ functionResolutionDependsOnArgumentCand ( impl , f , functionName , traitTp , pos , _)
219+ |
220+ if functionResolutionDependsOnPositionalArgumentCand ( impl , f , functionName , traitTp )
221+ then any ( )
222+ else
223+ // `traitTp` only occurs in return position; check that it is indeed needed for disambiguation
224+ exists ( ImplItemNode sibling |
225+ implSiblings ( _, impl , sibling ) and
226+ forall ( TypeParameter otherTraitTp |
227+ functionResolutionDependsOnPositionalArgumentCand ( impl , f , functionName , otherTraitTp )
228+ |
229+ hasEquivalentPositionalSibling ( impl , sibling , f , otherTraitTp )
230+ )
231+ )
138232 )
139233}
0 commit comments