@@ -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 ( )
@@ -310,20 +311,21 @@ signature module ArgsAreInstantiationsOfInputSig {
310311 * Holds if `f` inside `i` needs to have the type corresponding to type parameter
311312 * `tp` checked.
312313 *
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) .
314+ * ` tp` is a type parameter of the trait being implemented by `f` or the trait to which
315+ * `f` belongs .
315316 *
316- * `pos` is one of the positions in `f` in which the relevant type occours.
317+ * `posAdj` is one of the function-call adjusted positions in `f` in which the relevant
318+ * type occurs.
317319 */
318- predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos ) ;
320+ predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj ) ;
319321
320322 /** A call whose argument types are to be checked. */
321323 class Call {
322324 string toString ( ) ;
323325
324326 Location getLocation ( ) ;
325327
326- Type getArgType ( FunctionPosition pos , TypePath path ) ;
328+ Type getArgType ( FunctionPosition posAdj , TypePath path ) ;
327329
328330 predicate hasTargetCand ( ImplOrTraitItemNode i , Function f ) ;
329331 }
@@ -337,9 +339,9 @@ signature module ArgsAreInstantiationsOfInputSig {
337339module ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInputSig Input> {
338340 pragma [ nomagic]
339341 private predicate toCheckRanked (
340- ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos , int rnk
342+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj , int rnk
341343 ) {
342- Input:: toCheck ( i , f , tp , pos ) and
344+ Input:: toCheck ( i , f , tp , posAdj ) and
343345 tp =
344346 rank [ rnk + 1 ] ( TypeParameter tp0 , int j |
345347 Input:: toCheck ( i , f , tp0 , _) and
@@ -351,53 +353,59 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
351353
352354 pragma [ nomagic]
353355 private predicate toCheck (
354- ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos , AssocFunctionType t
356+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition posAdj ,
357+ AssocFunctionType t
355358 ) {
356- Input:: toCheck ( i , f , tp , pos ) and
357- t .appliesTo ( f , i , pos )
359+ exists ( FunctionPosition pos |
360+ Input:: toCheck ( i , f , tp , posAdj ) and
361+ t .appliesTo ( f , i , pos ) and
362+ posAdj = pos .getFunctionCallAdjusted ( f )
363+ )
358364 }
359365
360- private newtype TCallAndPos =
361- MkCallAndPos ( Input:: Call call , FunctionPosition pos ) { exists ( call .getArgType ( pos , _) ) }
366+ private newtype TCallAndPosAdj =
367+ MkCallAndPosAdj ( Input:: Call call , FunctionPosition posAdj ) {
368+ exists ( call .getArgType ( posAdj , _) )
369+ }
362370
363- /** A call tagged with a position. */
364- private class CallAndPos extends MkCallAndPos {
371+ /** A call tagged with a function-call adjusted position. */
372+ private class CallAndPosAdj extends MkCallAndPosAdj {
365373 Input:: Call call ;
366- FunctionPosition pos ;
374+ FunctionPosition posAdj ;
367375
368- CallAndPos ( ) { this = MkCallAndPos ( call , pos ) }
376+ CallAndPosAdj ( ) { this = MkCallAndPosAdj ( call , posAdj ) }
369377
370378 Input:: Call getCall ( ) { result = call }
371379
372- FunctionPosition getPos ( ) { result = pos }
380+ FunctionPosition getPosAdj ( ) { result = posAdj }
373381
374382 Location getLocation ( ) { result = call .getLocation ( ) }
375383
376- Type getTypeAt ( TypePath path ) { result = call .getArgType ( pos , path ) }
384+ Type getTypeAt ( TypePath path ) { result = call .getArgType ( posAdj , path ) }
377385
378- string toString ( ) { result = call .toString ( ) + " [arg " + pos + "]" }
386+ string toString ( ) { result = call .toString ( ) + " [arg " + posAdj + "]" }
379387 }
380388
381389 pragma [ nomagic]
382390 private predicate potentialInstantiationOf0 (
383- CallAndPos cp , Input:: Call call , TypeParameter tp , FunctionPosition pos , Function f ,
391+ CallAndPosAdj cp , Input:: Call call , TypeParameter tp , FunctionPosition posAdj , Function f ,
384392 TypeAbstraction abs , AssocFunctionType constraint
385393 ) {
386- cp = MkCallAndPos ( call , pragma [ only_bind_into ] ( pos ) ) and
394+ cp = MkCallAndPosAdj ( call , pragma [ only_bind_into ] ( posAdj ) ) and
387395 call .hasTargetCand ( abs , f ) and
388- toCheck ( abs , f , tp , pragma [ only_bind_into ] ( pos ) , constraint )
396+ toCheck ( abs , f , tp , pragma [ only_bind_into ] ( posAdj ) , constraint )
389397 }
390398
391399 private module ArgIsInstantiationOfToIndexInput implements
392- IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
400+ IsInstantiationOfInputSig< CallAndPosAdj , AssocFunctionType >
393401 {
394402 pragma [ nomagic]
395403 predicate potentialInstantiationOf (
396- CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
404+ CallAndPosAdj cp , TypeAbstraction abs , AssocFunctionType constraint
397405 ) {
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 )
406+ exists ( Input:: Call call , TypeParameter tp , FunctionPosition posAdj , int rnk , Function f |
407+ potentialInstantiationOf0 ( cp , call , tp , posAdj , f , abs , constraint ) and
408+ toCheckRanked ( abs , f , tp , posAdj , rnk )
401409 |
402410 rnk = 0
403411 or
@@ -409,24 +417,25 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
409417 }
410418
411419 private module ArgIsInstantiationOfToIndex =
412- ArgIsInstantiationOf< CallAndPos , ArgIsInstantiationOfToIndexInput > ;
420+ ArgIsInstantiationOf< CallAndPosAdj , ArgIsInstantiationOfToIndexInput > ;
413421
414422 pragma [ nomagic]
415423 private predicate argIsInstantiationOf (
416- Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i , Function f , int rnk
424+ Input:: Call call , ImplOrTraitItemNode i , Function f , int rnk
417425 ) {
418- ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPos ( call , pos ) , i , _) and
419- toCheckRanked ( i , f , _, pos , rnk )
426+ exists ( FunctionPosition posAdj |
427+ ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPosAdj ( call , posAdj ) , i , _) and
428+ toCheckRanked ( i , f , _, posAdj , rnk )
429+ )
420430 }
421431
422432 pragma [ nomagic]
423433 private predicate argsAreInstantiationsOfToIndex (
424434 Input:: Call call , ImplOrTraitItemNode i , Function f , int rnk
425435 ) {
426- exists ( FunctionPosition pos |
427- argIsInstantiationOf ( call , pos , i , f , rnk ) and
428- call .hasTargetCand ( i , f )
429- |
436+ argIsInstantiationOf ( call , i , f , rnk ) and
437+ call .hasTargetCand ( i , f ) and
438+ (
430439 rnk = 0
431440 or
432441 argsAreInstantiationsOfToIndex ( call , i , f , rnk - 1 )
@@ -448,11 +457,11 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
448457 }
449458
450459 private module ArgsAreNotInstantiationOfInput implements
451- IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
460+ IsInstantiationOfInputSig< CallAndPosAdj , AssocFunctionType >
452461 {
453462 pragma [ nomagic]
454463 predicate potentialInstantiationOf (
455- CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
464+ CallAndPosAdj cp , TypeAbstraction abs , AssocFunctionType constraint
456465 ) {
457466 potentialInstantiationOf0 ( cp , _, _, _, _, abs , constraint )
458467 }
@@ -461,13 +470,13 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
461470 }
462471
463472 private module ArgsAreNotInstantiationOf =
464- ArgIsInstantiationOf< CallAndPos , ArgsAreNotInstantiationOfInput > ;
473+ ArgIsInstantiationOf< CallAndPosAdj , ArgsAreNotInstantiationOfInput > ;
465474
466475 pragma [ nomagic]
467476 private predicate argsAreNotInstantiationsOf0 (
468- Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i
477+ Input:: Call call , FunctionPosition posAdj , ImplOrTraitItemNode i
469478 ) {
470- ArgsAreNotInstantiationOf:: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
479+ ArgsAreNotInstantiationOf:: argIsNotInstantiationOf ( MkCallAndPosAdj ( call , posAdj ) , i , _, _)
471480 }
472481
473482 /**
@@ -478,10 +487,10 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
478487 */
479488 pragma [ nomagic]
480489 predicate argsAreNotInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
481- exists ( FunctionPosition pos |
482- argsAreNotInstantiationsOf0 ( call , pos , i ) and
490+ exists ( FunctionPosition posAdj |
491+ argsAreNotInstantiationsOf0 ( call , posAdj , i ) and
483492 call .hasTargetCand ( i , f ) and
484- Input:: toCheck ( i , f , _, pos )
493+ Input:: toCheck ( i , f , _, posAdj )
485494 )
486495 }
487496}
0 commit comments