@@ -29,18 +29,26 @@ class FunctionPosition extends TFunctionPosition {
2929
3030 predicate isReturn ( ) { this = TReturnFunctionPosition ( ) }
3131
32- /** Gets the corresponding position when `f` is invoked via a function call. */
33- bindingset [ f]
34- FunctionPosition getFunctionCallAdjusted ( Function f ) {
35- this .isReturn ( ) and
32+ /**
33+ * Gets the corresponding position when function call syntax is used, assuming
34+ * this position is for a method.
35+ */
36+ FunctionPosition getFunctionCallAdjusted ( ) {
37+ ( this .isReturn ( ) or this .isTypeQualifier ( ) ) and
3638 result = this
3739 or
38- if f .hasSelfParam ( )
39- then
40- this .isSelf ( ) and result .asPosition ( ) = 0
41- or
42- result .asPosition ( ) = this .asPosition ( ) + 1
43- else result = this
40+ this .isSelf ( ) and result .asPosition ( ) = 0
41+ or
42+ result .asPosition ( ) = this .asPosition ( ) + 1
43+ }
44+
45+ /**
46+ * Gets the corresponding position when `f` is invoked via function call
47+ * syntax.
48+ */
49+ bindingset [ f]
50+ FunctionPosition getFunctionCallAdjusted ( Function f ) {
51+ if f .hasSelfParam ( ) then result = this .getFunctionCallAdjusted ( ) else result = this
4452 }
4553
4654 TypeMention getTypeMention ( Function f ) {
@@ -197,8 +205,7 @@ class AssocFunctionType extends MkAssocFunctionType {
197205 exists ( Function f , ImplOrTraitItemNode i , FunctionPosition pos | this .appliesTo ( f , i , pos ) |
198206 result = pos .getTypeMention ( f )
199207 or
200- pos .isSelf ( ) and
201- not f .hasSelfParam ( ) and
208+ pos .isTypeQualifier ( ) and
202209 result = [ i .( Impl ) .getSelfTy ( ) .( AstNode ) , i .( Trait ) .getName ( ) ]
203210 )
204211 }
@@ -209,7 +216,7 @@ class AssocFunctionType extends MkAssocFunctionType {
209216}
210217
211218pragma [ nomagic]
212- private Trait getALookupTrait ( Type t ) {
219+ Trait getALookupTrait ( Type t ) {
213220 result = t .( TypeParamTypeParameter ) .getTypeParam ( ) .( TypeParamItemNode ) .resolveABound ( )
214221 or
215222 result = t .( SelfTypeParameter ) .getTrait ( )
@@ -310,20 +317,21 @@ signature module ArgsAreInstantiationsOfInputSig {
310317 * Holds if `f` inside `i` needs to have the type corresponding to type parameter
311318 * `tp` checked.
312319 *
313- * If `i` is an inherent implementation, ` tp` is a type parameter of the type being
314- * implemented, otherwise `tp` is a type parameter of the trait (being implemented) .
320+ * ` tp` is a type parameter of the trait being implemented by `f` or the trait to which
321+ * `f` belongs .
315322 *
316- * `pos` is one of the positions in `f` in which the relevant type occours.
323+ * `posAdj` is one of the function-call adjusted positions in `f` in which the relevant
324+ * type occurs.
317325 */
318- predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos ) ;
326+ predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj ) ;
319327
320328 /** A call whose argument types are to be checked. */
321329 class Call {
322330 string toString ( ) ;
323331
324332 Location getLocation ( ) ;
325333
326- Type getArgType ( FunctionPosition pos , TypePath path ) ;
334+ Type getArgType ( FunctionPosition posAdj , TypePath path ) ;
327335
328336 predicate hasTargetCand ( ImplOrTraitItemNode i , Function f ) ;
329337 }
@@ -337,9 +345,9 @@ signature module ArgsAreInstantiationsOfInputSig {
337345module ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInputSig Input> {
338346 pragma [ nomagic]
339347 private predicate toCheckRanked (
340- ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos , int rnk
348+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj , int rnk
341349 ) {
342- Input:: toCheck ( i , f , tp , pos ) and
350+ Input:: toCheck ( i , f , tp , posAdj ) and
343351 tp =
344352 rank [ rnk + 1 ] ( TypeParameter tp0 , int j |
345353 Input:: toCheck ( i , f , tp0 , _) and
@@ -351,53 +359,59 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
351359
352360 pragma [ nomagic]
353361 private predicate toCheck (
354- ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos , AssocFunctionType t
362+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj ,
363+ AssocFunctionType t
355364 ) {
356- Input:: toCheck ( i , f , tp , pos ) and
357- t .appliesTo ( f , i , pos )
365+ exists ( FunctionPosition pos |
366+ Input:: toCheck ( i , f , tp , posAdj ) and
367+ t .appliesTo ( f , i , pos ) and
368+ posAdj = pos .getFunctionCallAdjusted ( f )
369+ )
358370 }
359371
360- private newtype TCallAndPos =
361- MkCallAndPos ( Input:: Call call , FunctionPosition pos ) { exists ( call .getArgType ( pos , _) ) }
372+ private newtype TCallAndPosAdj =
373+ MkCallAndPosAdj ( Input:: Call call , FunctionPosition posAdj ) {
374+ exists ( call .getArgType ( posAdj , _) )
375+ }
362376
363- /** A call tagged with a position. */
364- private class CallAndPos extends MkCallAndPos {
377+ /** A call tagged with a function-call adjusted position. */
378+ private class CallAndPosAdj extends MkCallAndPosAdj {
365379 Input:: Call call ;
366- FunctionPosition pos ;
380+ FunctionPosition posAdj ;
367381
368- CallAndPos ( ) { this = MkCallAndPos ( call , pos ) }
382+ CallAndPosAdj ( ) { this = MkCallAndPosAdj ( call , posAdj ) }
369383
370384 Input:: Call getCall ( ) { result = call }
371385
372- FunctionPosition getPos ( ) { result = pos }
386+ FunctionPosition getPosAdj ( ) { result = posAdj }
373387
374388 Location getLocation ( ) { result = call .getLocation ( ) }
375389
376- Type getTypeAt ( TypePath path ) { result = call .getArgType ( pos , path ) }
390+ Type getTypeAt ( TypePath path ) { result = call .getArgType ( posAdj , path ) }
377391
378- string toString ( ) { result = call .toString ( ) + " [arg " + pos + "]" }
392+ string toString ( ) { result = call .toString ( ) + " [arg " + posAdj + "]" }
379393 }
380394
381395 pragma [ nomagic]
382396 private predicate potentialInstantiationOf0 (
383- CallAndPos cp , Input:: Call call , TypeParameter tp , FunctionPosition pos , Function f ,
397+ CallAndPosAdj cp , Input:: Call call , TypeParameter tp , FunctionPosition posAdj , Function f ,
384398 TypeAbstraction abs , AssocFunctionType constraint
385399 ) {
386- cp = MkCallAndPos ( call , pragma [ only_bind_into ] ( pos ) ) and
400+ cp = MkCallAndPosAdj ( call , pragma [ only_bind_into ] ( posAdj ) ) and
387401 call .hasTargetCand ( abs , f ) and
388- toCheck ( abs , f , tp , pragma [ only_bind_into ] ( pos ) , constraint )
402+ toCheck ( abs , f , tp , pragma [ only_bind_into ] ( posAdj ) , constraint )
389403 }
390404
391405 private module ArgIsInstantiationOfToIndexInput implements
392- IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
406+ IsInstantiationOfInputSig< CallAndPosAdj , AssocFunctionType >
393407 {
394408 pragma [ nomagic]
395409 predicate potentialInstantiationOf (
396- CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
410+ CallAndPosAdj cp , TypeAbstraction abs , AssocFunctionType constraint
397411 ) {
398- exists ( Input:: Call call , TypeParameter tp , FunctionPosition pos , int rnk , Function f |
399- potentialInstantiationOf0 ( cp , call , tp , pos , f , abs , constraint ) and
400- toCheckRanked ( abs , f , tp , pos , rnk )
412+ exists ( Input:: Call call , TypeParameter tp , FunctionPosition posAdj , int rnk , Function f |
413+ potentialInstantiationOf0 ( cp , call , tp , posAdj , f , abs , constraint ) and
414+ toCheckRanked ( abs , f , tp , posAdj , rnk )
401415 |
402416 rnk = 0
403417 or
@@ -409,24 +423,25 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
409423 }
410424
411425 private module ArgIsInstantiationOfToIndex =
412- ArgIsInstantiationOf< CallAndPos , ArgIsInstantiationOfToIndexInput > ;
426+ ArgIsInstantiationOf< CallAndPosAdj , ArgIsInstantiationOfToIndexInput > ;
413427
414428 pragma [ nomagic]
415429 private predicate argIsInstantiationOf (
416- Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i , Function f , int rnk
430+ Input:: Call call , ImplOrTraitItemNode i , Function f , int rnk
417431 ) {
418- ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPos ( call , pos ) , i , _) and
419- toCheckRanked ( i , f , _, pos , rnk )
432+ exists ( FunctionPosition posAdj |
433+ ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPosAdj ( call , posAdj ) , i , _) and
434+ toCheckRanked ( i , f , _, posAdj , rnk )
435+ )
420436 }
421437
422438 pragma [ nomagic]
423439 private predicate argsAreInstantiationsOfToIndex (
424440 Input:: Call call , ImplOrTraitItemNode i , Function f , int rnk
425441 ) {
426- exists ( FunctionPosition pos |
427- argIsInstantiationOf ( call , pos , i , f , rnk ) and
428- call .hasTargetCand ( i , f )
429- |
442+ argIsInstantiationOf ( call , i , f , rnk ) and
443+ call .hasTargetCand ( i , f ) and
444+ (
430445 rnk = 0
431446 or
432447 argsAreInstantiationsOfToIndex ( call , i , f , rnk - 1 )
@@ -448,11 +463,11 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
448463 }
449464
450465 private module ArgsAreNotInstantiationOfInput implements
451- IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
466+ IsInstantiationOfInputSig< CallAndPosAdj , AssocFunctionType >
452467 {
453468 pragma [ nomagic]
454469 predicate potentialInstantiationOf (
455- CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
470+ CallAndPosAdj cp , TypeAbstraction abs , AssocFunctionType constraint
456471 ) {
457472 potentialInstantiationOf0 ( cp , _, _, _, _, abs , constraint )
458473 }
@@ -461,13 +476,13 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
461476 }
462477
463478 private module ArgsAreNotInstantiationOf =
464- ArgIsInstantiationOf< CallAndPos , ArgsAreNotInstantiationOfInput > ;
479+ ArgIsInstantiationOf< CallAndPosAdj , ArgsAreNotInstantiationOfInput > ;
465480
466481 pragma [ nomagic]
467482 private predicate argsAreNotInstantiationsOf0 (
468- Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i
483+ Input:: Call call , FunctionPosition posAdj , ImplOrTraitItemNode i
469484 ) {
470- ArgsAreNotInstantiationOf:: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
485+ ArgsAreNotInstantiationOf:: argIsNotInstantiationOf ( MkCallAndPosAdj ( call , posAdj ) , i , _, _)
471486 }
472487
473488 /**
@@ -478,10 +493,10 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
478493 */
479494 pragma [ nomagic]
480495 predicate argsAreNotInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
481- exists ( FunctionPosition pos |
482- argsAreNotInstantiationsOf0 ( call , pos , i ) and
496+ exists ( FunctionPosition posAdj |
497+ argsAreNotInstantiationsOf0 ( call , posAdj , i ) and
483498 call .hasTargetCand ( i , f ) and
484- Input:: toCheck ( i , f , _, pos )
499+ Input:: toCheck ( i , f , _, posAdj )
485500 )
486501 }
487502}
0 commit comments