@@ -297,7 +297,10 @@ signature module ArgsAreInstantiationsOfInputSig {
297297 * Holds if types need to be matched against the type `t` at position `pos` of
298298 * `f` inside `i`.
299299 */
300- predicate toCheck ( ImplOrTraitItemNode i , Function f , FunctionPosition pos , AssocFunctionType t ) ;
300+ predicate toCheck (
301+ ImplOrTraitItemNode i , Function f , TypeParameter traitTp , FunctionPosition pos ,
302+ AssocFunctionType t
303+ ) ;
301304
302305 /** A call whose argument types are to be checked. */
303306 class Call {
@@ -318,20 +321,16 @@ signature module ArgsAreInstantiationsOfInputSig {
318321 */
319322module ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInputSig Input> {
320323 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- )
324+ private predicate toCheckRanked (
325+ ImplOrTraitItemNode i , Function f , TypeParameter traitTp , FunctionPosition pos , int rnk
326+ ) {
327+ Input:: toCheck ( i , f , traitTp , pos , _) and
328+ traitTp =
329+ rank [ rnk + 1 ] ( TypeParameter traitTp0 , int j |
330+ Input:: toCheck ( i , f , traitTp0 , _, _) and
331+ j = getTypeParameterId ( traitTp0 )
333332 |
334- pos0 order by j
333+ traitTp0 order by j
335334 )
336335 }
337336
@@ -361,21 +360,21 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
361360 {
362361 pragma [ nomagic]
363362 private predicate potentialInstantiationOf0 (
364- CallAndPos cp , Input:: Call call , FunctionPosition pos , int rnk , Function f ,
365- TypeAbstraction abs , AssocFunctionType constraint
363+ CallAndPos cp , Input:: Call call , TypeParameter traitTp , FunctionPosition pos , int rnk ,
364+ Function f , TypeAbstraction abs , AssocFunctionType constraint
366365 ) {
367366 cp = MkCallAndPos ( call , pragma [ only_bind_into ] ( pos ) ) and
368367 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 )
368+ toCheckRanked ( abs , f , traitTp , pragma [ only_bind_into ] ( pos ) , rnk ) and
369+ Input:: toCheck ( abs , f , traitTp , pragma [ only_bind_into ] ( pos ) , constraint )
371370 }
372371
373372 pragma [ nomagic]
374373 predicate potentialInstantiationOf (
375374 CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
376375 ) {
377376 exists ( Input:: Call call , int rnk , Function f |
378- potentialInstantiationOf0 ( cp , call , _, rnk , f , abs , constraint )
377+ potentialInstantiationOf0 ( cp , call , _, _ , rnk , f , abs , constraint )
379378 |
380379 rnk = 0
381380 or
@@ -384,7 +383,7 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
384383 }
385384
386385 predicate relevantConstraint ( AssocFunctionType constraint ) {
387- Input:: toCheck ( _, _, _, constraint )
386+ Input:: toCheck ( _, _, _, _ , constraint )
388387 }
389388 }
390389
@@ -398,7 +397,11 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
398397 exists ( FunctionPosition pos |
399398 ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPos ( call , pos ) , i , _) and
400399 call .hasTargetCand ( i , f ) and
401- toCheckRanked ( i , f , pos , rnk )
400+ toCheckRanked ( i , f , _, pos , rnk )
401+ |
402+ rnk = 0
403+ or
404+ argsAreInstantiationsOfToIndex ( call , i , f , rnk - 1 )
402405 )
403406 }
404407
@@ -410,15 +413,49 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
410413 predicate argsAreInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
411414 exists ( int rnk |
412415 argsAreInstantiationsOfToIndex ( call , i , f , rnk ) and
413- rnk = max ( int r | toCheckRanked ( i , f , _, r ) )
416+ rnk = max ( int r | toCheckRanked ( i , f , _, _ , r ) )
414417 )
415418 }
416419
420+ private module ArgsAreNotInstantiationOfInput implements
421+ IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
422+ {
423+ pragma [ nomagic]
424+ private predicate potentialInstantiationOf0 (
425+ CallAndPos cp , Input:: Call call , TypeParameter traitTp , FunctionPosition pos , Function f ,
426+ TypeAbstraction abs , AssocFunctionType constraint
427+ ) {
428+ cp = MkCallAndPos ( call , pragma [ only_bind_into ] ( pos ) ) and
429+ call .hasTargetCand ( abs , f ) and
430+ Input:: toCheck ( abs , f , traitTp , pragma [ only_bind_into ] ( pos ) , constraint )
431+ }
432+
433+ pragma [ nomagic]
434+ predicate potentialInstantiationOf (
435+ CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
436+ ) {
437+ // exists(Input::Call call, int rnk, Function f |
438+ potentialInstantiationOf0 ( cp , _, _, _, _, abs , constraint )
439+ // |
440+ // rnk = 0
441+ // or
442+ // argsAreInstantiationsOfToIndex(call, abs, f, rnk - 1)
443+ // )
444+ }
445+
446+ predicate relevantConstraint ( AssocFunctionType constraint ) {
447+ Input:: toCheck ( _, _, _, _, constraint )
448+ }
449+ }
450+
451+ private module ArgsAreNotInstantiationOf =
452+ ArgIsInstantiationOf< CallAndPos , ArgsAreNotInstantiationOfInput > ;
453+
417454 pragma [ nomagic]
418455 private predicate argsAreNotInstantiationsOf0 (
419456 Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i
420457 ) {
421- ArgIsInstantiationOfToIndex :: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
458+ ArgsAreNotInstantiationOf :: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
422459 }
423460
424461 /**
@@ -430,7 +467,7 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
430467 exists ( FunctionPosition pos |
431468 argsAreNotInstantiationsOf0 ( call , pos , i ) and
432469 call .hasTargetCand ( i , f ) and
433- Input:: toCheck ( i , f , pos , _)
470+ Input:: toCheck ( i , f , _ , pos , _)
434471 )
435472 }
436473}
0 commit comments