@@ -82,7 +82,9 @@ private newtype TAssocFunctionType =
8282 // through `i`. This ensures that `parent` is either a supertrait of `i` or
8383 // `i` in an `impl` block implementing `parent`.
8484 ( parent = i or BaseTypes:: rootTypesSatisfaction ( _, TTrait ( parent ) , i , _, _) ) and
85- exists ( pos .getTypeMention ( f ) )
85+ // We always include the `self` position, even for non-methods, where it is used
86+ // to match type qualifiers against the `impl` or trait type, such as in `Vec::new`.
87+ ( exists ( pos .getTypeMention ( f ) ) or pos .isSelf ( ) )
8688 }
8789
8890bindingset [ abs, constraint, tp]
@@ -116,6 +118,22 @@ Type getAssocFunctionTypeAt(Function f, ImplOrTraitItemNode i, FunctionPosition
116118 )
117119}
118120
121+ /**
122+ * Same as `getAssocFunctionTypeAt`, but also includes types at the `self` position
123+ * for non-methods.
124+ */
125+ pragma [ nomagic]
126+ Type getAssocFunctionTypeInclNonMethodSelfAt (
127+ Function f , ImplOrTraitItemNode i , FunctionPosition pos , TypePath path
128+ ) {
129+ result = getAssocFunctionTypeAt ( f , i , pos , path )
130+ or
131+ f = i .getASuccessor ( _) and
132+ not f .hasSelfParam ( ) and
133+ pos .isSelf ( ) and
134+ result = resolveImplOrTraitType ( i , path )
135+ }
136+
119137/**
120138 * The type of an associated function at a given position, when its implicit
121139 * `Self` type parameter is specialized to a given trait or `impl` block.
@@ -174,7 +192,7 @@ class AssocFunctionType extends MkAssocFunctionType {
174192 Type getTypeAt ( TypePath path ) {
175193 exists ( Function f , FunctionPosition pos , ImplOrTraitItemNode i , Type t |
176194 this .appliesTo ( f , i , pos ) and
177- t = getAssocFunctionTypeAt ( f , i , pos , path )
195+ t = getAssocFunctionTypeInclNonMethodSelfAt ( f , i , pos , path )
178196 |
179197 not t instanceof SelfTypeParameter and
180198 result = t
@@ -184,9 +202,12 @@ class AssocFunctionType extends MkAssocFunctionType {
184202 }
185203
186204 private TypeMention getTypeMention ( ) {
187- exists ( Function f , FunctionPosition pos |
188- this .appliesTo ( f , _, pos ) and
205+ exists ( Function f , ImplOrTraitItemNode i , FunctionPosition pos | this .appliesTo ( f , i , pos ) |
189206 result = pos .getTypeMention ( f )
207+ or
208+ pos .isSelf ( ) and
209+ not f .hasSelfParam ( ) and
210+ result = [ i .( Impl ) .getSelfTy ( ) .( TypeMention ) , i .( TypeMention ) ]
190211 )
191212 }
192213
@@ -294,10 +315,15 @@ module ArgIsInstantiationOf<
294315 */
295316signature module ArgsAreInstantiationsOfInputSig {
296317 /**
297- * Holds if types need to be matched against the type `t` at position `pos` of
298- * `f` inside `i`.
318+ * Holds if `f` inside `i` needs to have the type corresponding to type parameter
319+ * `tp` checked.
320+ *
321+ * If `i` is an inherent implementation, `tp` is a type parameter of the type being
322+ * implemented, otherwise `tp` is a type parameter of the trait (being implemented).
323+ *
324+ * `pos` is one of the positions in `f` in which the relevant type occours.
299325 */
300- predicate toCheck ( ImplOrTraitItemNode i , Function f , FunctionPosition pos , AssocFunctionType t ) ;
326+ predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos ) ;
301327
302328 /** A call whose argument types are to be checked. */
303329 class Call {
@@ -318,23 +344,27 @@ signature module ArgsAreInstantiationsOfInputSig {
318344 */
319345module ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInputSig Input> {
320346 pragma [ nomagic]
321- private predicate toCheckRanked ( ImplOrTraitItemNode i , Function f , FunctionPosition pos , int rnk ) {
322- Input:: toCheck ( i , f , pos , _) and
323- pos =
324- rank [ rnk + 1 ] ( FunctionPosition pos0 , int j |
325- Input:: toCheck ( i , f , pos0 , _) and
326- (
327- j = pos0 .asPosition ( )
328- or
329- pos0 .isSelf ( ) and j = - 1
330- or
331- pos0 .isReturn ( ) and j = - 2
332- )
347+ private predicate toCheckRanked (
348+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos , int rnk
349+ ) {
350+ Input:: toCheck ( i , f , tp , pos ) and
351+ tp =
352+ rank [ rnk + 1 ] ( TypeParameter tp0 , int j |
353+ Input:: toCheck ( i , f , tp0 , _) and
354+ j = getTypeParameterId ( tp0 )
333355 |
334- pos0 order by j
356+ tp0 order by j
335357 )
336358 }
337359
360+ pragma [ nomagic]
361+ private predicate toCheck (
362+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos , AssocFunctionType t
363+ ) {
364+ Input:: toCheck ( i , f , tp , pos ) and
365+ t .appliesTo ( f , i , pos )
366+ }
367+
338368 private newtype TCallAndPos =
339369 MkCallAndPos ( Input:: Call call , FunctionPosition pos ) { exists ( call .getArgType ( pos , _) ) }
340370
@@ -356,36 +386,34 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
356386 string toString ( ) { result = call .toString ( ) + " [arg " + pos + "]" }
357387 }
358388
389+ pragma [ nomagic]
390+ private predicate potentialInstantiationOf0 (
391+ CallAndPos cp , Input:: Call call , TypeParameter tp , FunctionPosition pos , Function f ,
392+ TypeAbstraction abs , AssocFunctionType constraint
393+ ) {
394+ cp = MkCallAndPos ( call , pragma [ only_bind_into ] ( pos ) ) and
395+ call .hasTargetCand ( abs , f ) and
396+ toCheck ( abs , f , tp , pragma [ only_bind_into ] ( pos ) , constraint )
397+ }
398+
359399 private module ArgIsInstantiationOfToIndexInput implements
360400 IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
361401 {
362- pragma [ nomagic]
363- private predicate potentialInstantiationOf0 (
364- CallAndPos cp , Input:: Call call , FunctionPosition pos , int rnk , Function f ,
365- TypeAbstraction abs , AssocFunctionType constraint
366- ) {
367- cp = MkCallAndPos ( call , pragma [ only_bind_into ] ( pos ) ) and
368- call .hasTargetCand ( abs , f ) and
369- toCheckRanked ( abs , f , pragma [ only_bind_into ] ( pos ) , rnk ) and
370- Input:: toCheck ( abs , f , pragma [ only_bind_into ] ( pos ) , constraint )
371- }
372-
373402 pragma [ nomagic]
374403 predicate potentialInstantiationOf (
375404 CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
376405 ) {
377- exists ( Input:: Call call , int rnk , Function f |
378- potentialInstantiationOf0 ( cp , call , _, rnk , f , abs , constraint )
406+ exists ( Input:: Call call , TypeParameter tp , FunctionPosition pos , int rnk , Function f |
407+ potentialInstantiationOf0 ( cp , call , tp , pos , f , abs , constraint ) and
408+ toCheckRanked ( abs , f , tp , pos , rnk )
379409 |
380410 rnk = 0
381411 or
382412 argsAreInstantiationsOfToIndex ( call , abs , f , rnk - 1 )
383413 )
384414 }
385415
386- predicate relevantConstraint ( AssocFunctionType constraint ) {
387- Input:: toCheck ( _, _, _, constraint )
388- }
416+ predicate relevantConstraint ( AssocFunctionType constraint ) { toCheck ( _, _, _, _, constraint ) }
389417 }
390418
391419 private module ArgIsInstantiationOfToIndex =
@@ -398,39 +426,63 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
398426 exists ( FunctionPosition pos |
399427 ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPos ( call , pos ) , i , _) and
400428 call .hasTargetCand ( i , f ) and
401- toCheckRanked ( i , f , pos , rnk )
429+ toCheckRanked ( i , f , _, pos , rnk )
430+ |
431+ rnk = 0
432+ or
433+ argsAreInstantiationsOfToIndex ( call , i , f , rnk - 1 )
402434 )
403435 }
404436
405437 /**
406438 * Holds if all arguments of `call` have types that are instantiations of the
407439 * types of the corresponding parameters of `f` inside `i`.
440+ *
441+ * TODO: Check type parameter constraints as well.
408442 */
409443 pragma [ nomagic]
410444 predicate argsAreInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
411445 exists ( int rnk |
412446 argsAreInstantiationsOfToIndex ( call , i , f , rnk ) and
413- rnk = max ( int r | toCheckRanked ( i , f , _, r ) )
447+ rnk = max ( int r | toCheckRanked ( i , f , _, _ , r ) )
414448 )
415449 }
416450
451+ private module ArgsAreNotInstantiationOfInput implements
452+ IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
453+ {
454+ pragma [ nomagic]
455+ predicate potentialInstantiationOf (
456+ CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
457+ ) {
458+ potentialInstantiationOf0 ( cp , _, _, _, _, abs , constraint )
459+ }
460+
461+ predicate relevantConstraint ( AssocFunctionType constraint ) { toCheck ( _, _, _, _, constraint ) }
462+ }
463+
464+ private module ArgsAreNotInstantiationOf =
465+ ArgIsInstantiationOf< CallAndPos , ArgsAreNotInstantiationOfInput > ;
466+
417467 pragma [ nomagic]
418468 private predicate argsAreNotInstantiationsOf0 (
419469 Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i
420470 ) {
421- ArgIsInstantiationOfToIndex :: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
471+ ArgsAreNotInstantiationOf :: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
422472 }
423473
424474 /**
425475 * Holds if _some_ argument of `call` has a type that is not an instantiation of the
426476 * type of the corresponding parameter of `f` inside `i`.
477+ *
478+ * TODO: Check type parameter constraints as well.
427479 */
428480 pragma [ nomagic]
429481 predicate argsAreNotInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
430482 exists ( FunctionPosition pos |
431483 argsAreNotInstantiationsOf0 ( call , pos , i ) and
432484 call .hasTargetCand ( i , f ) and
433- Input:: toCheck ( i , f , pos , _ )
485+ Input:: toCheck ( i , f , _ , pos )
434486 )
435487 }
436488}
0 commit comments