@@ -29,18 +29,20 @@ class FunctionPosition extends TFunctionPosition {
2929
3030 predicate isReturn ( ) { this = TReturnFunctionPosition ( ) }
3131
32+ /** Gets the corresponding position when function call syntax is used. */
33+ FunctionPosition getFunctionCallAdjusted ( ) {
34+ ( this .isReturn ( ) or this .isTypeQualifier ( ) ) and
35+ result = this
36+ or
37+ this .isSelf ( ) and result .asPosition ( ) = 0
38+ or
39+ result .asPosition ( ) = this .asPosition ( ) + 1
40+ }
41+
3242 /** Gets the corresponding position when `f` is invoked via a function call. */
3343 bindingset [ f]
3444 FunctionPosition getFunctionCallAdjusted ( Function f ) {
35- this .isReturn ( ) and
36- result = this
37- 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
45+ if f .hasSelfParam ( ) then result = this .getFunctionCallAdjusted ( ) else result = this
4446 }
4547
4648 TypeMention getTypeMention ( Function f ) {
@@ -197,8 +199,7 @@ class AssocFunctionType extends MkAssocFunctionType {
197199 exists ( Function f , ImplOrTraitItemNode i , FunctionPosition pos | this .appliesTo ( f , i , pos ) |
198200 result = pos .getTypeMention ( f )
199201 or
200- pos .isSelf ( ) and
201- not f .hasSelfParam ( ) and
202+ pos .isTypeQualifier ( ) and
202203 result = [ i .( Impl ) .getSelfTy ( ) .( AstNode ) , i .( Trait ) .getName ( ) ]
203204 )
204205 }
@@ -209,7 +210,7 @@ class AssocFunctionType extends MkAssocFunctionType {
209210}
210211
211212pragma [ nomagic]
212- private Trait getALookupTrait ( Type t ) {
213+ Trait getALookupTrait ( Type t ) {
213214 result = t .( TypeParamTypeParameter ) .getTypeParam ( ) .( TypeParamItemNode ) .resolveABound ( )
214215 or
215216 result = t .( SelfTypeParameter ) .getTrait ( )
@@ -313,17 +314,17 @@ signature module ArgsAreInstantiationsOfInputSig {
313314 * If `i` is an inherent implementation, `tp` is a type parameter of the type being
314315 * implemented, otherwise `tp` is a type parameter of the trait (being implemented).
315316 *
316- * `pos ` is one of the positions in `f` in which the relevant type occours .
317+ * `posAdj ` is one of the adjusted positions in `f` in which the relevant type occurs .
317318 */
318- predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos ) ;
319+ predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj ) ;
319320
320321 /** A call whose argument types are to be checked. */
321322 class Call {
322323 string toString ( ) ;
323324
324325 Location getLocation ( ) ;
325326
326- Type getArgType ( FunctionPosition pos , TypePath path ) ;
327+ Type getArgType ( FunctionPosition posAdj , TypePath path ) ;
327328
328329 predicate hasTargetCand ( ImplOrTraitItemNode i , Function f ) ;
329330 }
@@ -337,9 +338,9 @@ signature module ArgsAreInstantiationsOfInputSig {
337338module ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInputSig Input> {
338339 pragma [ nomagic]
339340 private predicate toCheckRanked (
340- ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos , int rnk
341+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj , int rnk
341342 ) {
342- Input:: toCheck ( i , f , tp , pos ) and
343+ Input:: toCheck ( i , f , tp , posAdj ) and
343344 tp =
344345 rank [ rnk + 1 ] ( TypeParameter tp0 , int j |
345346 Input:: toCheck ( i , f , tp0 , _) and
@@ -351,53 +352,59 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
351352
352353 pragma [ nomagic]
353354 private predicate toCheck (
354- ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos , AssocFunctionType t
355+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj ,
356+ AssocFunctionType t
355357 ) {
356- Input:: toCheck ( i , f , tp , pos ) and
357- t .appliesTo ( f , i , pos )
358+ exists ( FunctionPosition pos |
359+ Input:: toCheck ( i , f , tp , posAdj ) and
360+ t .appliesTo ( f , i , pos ) and
361+ posAdj = pos .getFunctionCallAdjusted ( f )
362+ )
358363 }
359364
360- private newtype TCallAndPos =
361- MkCallAndPos ( Input:: Call call , FunctionPosition pos ) { exists ( call .getArgType ( pos , _) ) }
365+ private newtype TCallAndPosAdj =
366+ MkCallAndPosAdj ( Input:: Call call , FunctionPosition posAdj ) {
367+ exists ( call .getArgType ( posAdj , _) )
368+ }
362369
363- /** A call tagged with a position. */
364- private class CallAndPos extends MkCallAndPos {
370+ /** A call tagged with an adjusted position. */
371+ private class CallAndPosAdj extends MkCallAndPosAdj {
365372 Input:: Call call ;
366- FunctionPosition pos ;
373+ FunctionPosition posAdj ;
367374
368- CallAndPos ( ) { this = MkCallAndPos ( call , pos ) }
375+ CallAndPosAdj ( ) { this = MkCallAndPosAdj ( call , posAdj ) }
369376
370377 Input:: Call getCall ( ) { result = call }
371378
372- FunctionPosition getPos ( ) { result = pos }
379+ FunctionPosition getPosAdj ( ) { result = posAdj }
373380
374381 Location getLocation ( ) { result = call .getLocation ( ) }
375382
376- Type getTypeAt ( TypePath path ) { result = call .getArgType ( pos , path ) }
383+ Type getTypeAt ( TypePath path ) { result = call .getArgType ( posAdj , path ) }
377384
378- string toString ( ) { result = call .toString ( ) + " [arg " + pos + "]" }
385+ string toString ( ) { result = call .toString ( ) + " [arg " + posAdj + "]" }
379386 }
380387
381388 pragma [ nomagic]
382389 private predicate potentialInstantiationOf0 (
383- CallAndPos cp , Input:: Call call , TypeParameter tp , FunctionPosition pos , Function f ,
390+ CallAndPosAdj cp , Input:: Call call , TypeParameter tp , FunctionPosition posAdj , Function f ,
384391 TypeAbstraction abs , AssocFunctionType constraint
385392 ) {
386- cp = MkCallAndPos ( call , pragma [ only_bind_into ] ( pos ) ) and
393+ cp = MkCallAndPosAdj ( call , pragma [ only_bind_into ] ( posAdj ) ) and
387394 call .hasTargetCand ( abs , f ) and
388- toCheck ( abs , f , tp , pragma [ only_bind_into ] ( pos ) , constraint )
395+ toCheck ( abs , f , tp , pragma [ only_bind_into ] ( posAdj ) , constraint )
389396 }
390397
391398 private module ArgIsInstantiationOfToIndexInput implements
392- IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
399+ IsInstantiationOfInputSig< CallAndPosAdj , AssocFunctionType >
393400 {
394401 pragma [ nomagic]
395402 predicate potentialInstantiationOf (
396- CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
403+ CallAndPosAdj cp , TypeAbstraction abs , AssocFunctionType constraint
397404 ) {
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 )
405+ exists ( Input:: Call call , TypeParameter tp , FunctionPosition posAdj , int rnk , Function f |
406+ potentialInstantiationOf0 ( cp , call , tp , posAdj , f , abs , constraint ) and
407+ toCheckRanked ( abs , f , tp , posAdj , rnk )
401408 |
402409 rnk = 0
403410 or
@@ -409,24 +416,25 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
409416 }
410417
411418 private module ArgIsInstantiationOfToIndex =
412- ArgIsInstantiationOf< CallAndPos , ArgIsInstantiationOfToIndexInput > ;
419+ ArgIsInstantiationOf< CallAndPosAdj , ArgIsInstantiationOfToIndexInput > ;
413420
414421 pragma [ nomagic]
415422 private predicate argIsInstantiationOf (
416- Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i , Function f , int rnk
423+ Input:: Call call , ImplOrTraitItemNode i , Function f , int rnk
417424 ) {
418- ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPos ( call , pos ) , i , _) and
419- toCheckRanked ( i , f , _, pos , rnk )
425+ exists ( FunctionPosition posAdj |
426+ ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPosAdj ( call , posAdj ) , i , _) and
427+ toCheckRanked ( i , f , _, posAdj , rnk )
428+ )
420429 }
421430
422431 pragma [ nomagic]
423432 private predicate argsAreInstantiationsOfToIndex (
424433 Input:: Call call , ImplOrTraitItemNode i , Function f , int rnk
425434 ) {
426- exists ( FunctionPosition pos |
427- argIsInstantiationOf ( call , pos , i , f , rnk ) and
428- call .hasTargetCand ( i , f )
429- |
435+ argIsInstantiationOf ( call , i , f , rnk ) and
436+ call .hasTargetCand ( i , f ) and
437+ (
430438 rnk = 0
431439 or
432440 argsAreInstantiationsOfToIndex ( call , i , f , rnk - 1 )
@@ -448,11 +456,11 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
448456 }
449457
450458 private module ArgsAreNotInstantiationOfInput implements
451- IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
459+ IsInstantiationOfInputSig< CallAndPosAdj , AssocFunctionType >
452460 {
453461 pragma [ nomagic]
454462 predicate potentialInstantiationOf (
455- CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
463+ CallAndPosAdj cp , TypeAbstraction abs , AssocFunctionType constraint
456464 ) {
457465 potentialInstantiationOf0 ( cp , _, _, _, _, abs , constraint )
458466 }
@@ -461,13 +469,13 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
461469 }
462470
463471 private module ArgsAreNotInstantiationOf =
464- ArgIsInstantiationOf< CallAndPos , ArgsAreNotInstantiationOfInput > ;
472+ ArgIsInstantiationOf< CallAndPosAdj , ArgsAreNotInstantiationOfInput > ;
465473
466474 pragma [ nomagic]
467475 private predicate argsAreNotInstantiationsOf0 (
468- Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i
476+ Input:: Call call , FunctionPosition posAdj , ImplOrTraitItemNode i
469477 ) {
470- ArgsAreNotInstantiationOf:: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
478+ ArgsAreNotInstantiationOf:: argIsNotInstantiationOf ( MkCallAndPosAdj ( call , posAdj ) , i , _, _)
471479 }
472480
473481 /**
@@ -478,10 +486,10 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
478486 */
479487 pragma [ nomagic]
480488 predicate argsAreNotInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
481- exists ( FunctionPosition pos |
482- argsAreNotInstantiationsOf0 ( call , pos , i ) and
489+ exists ( FunctionPosition posAdj |
490+ argsAreNotInstantiationsOf0 ( call , posAdj , i ) and
483491 call .hasTargetCand ( i , f ) and
484- Input:: toCheck ( i , f , _, pos )
492+ Input:: toCheck ( i , f , _, posAdj )
485493 )
486494 }
487495}
0 commit comments