@@ -294,10 +294,12 @@ module ArgIsInstantiationOf<
294294 */
295295signature module ArgsAreInstantiationsOfInputSig {
296296 /**
297- * Holds if types need to be matched against the type `t` at position `pos` of
298- * `f` inside `i`.
297+ * Holds if `f` implements a trait function with type parameter `traitTp`, where
298+ * we need to check that the type of `f` for `traitTp` is satisfied.
299+ *
300+ * `pos` is one of the positions in `f` in which the relevant type occours.
299301 */
300- predicate toCheck ( ImplOrTraitItemNode i , Function f , FunctionPosition pos , AssocFunctionType t ) ;
302+ predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter traitTp , FunctionPosition pos ) ;
301303
302304 /** A call whose argument types are to be checked. */
303305 class Call {
@@ -318,23 +320,28 @@ signature module ArgsAreInstantiationsOfInputSig {
318320 */
319321module ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInputSig Input> {
320322 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- )
323+ private predicate toCheckRanked (
324+ ImplOrTraitItemNode i , Function f , TypeParameter traitTp , FunctionPosition pos , int rnk
325+ ) {
326+ Input:: toCheck ( i , f , traitTp , pos ) and
327+ traitTp =
328+ rank [ rnk + 1 ] ( TypeParameter traitTp0 , int j |
329+ Input:: toCheck ( i , f , traitTp0 , _) and
330+ j = getTypeParameterId ( traitTp0 )
333331 |
334- pos0 order by j
332+ traitTp0 order by j
335333 )
336334 }
337335
336+ pragma [ nomagic]
337+ private predicate toCheck (
338+ ImplOrTraitItemNode i , Function f , TypeParameter traitTp , FunctionPosition pos ,
339+ AssocFunctionType t
340+ ) {
341+ Input:: toCheck ( i , f , traitTp , pos ) and
342+ t .appliesTo ( f , i , pos )
343+ }
344+
338345 private newtype TCallAndPos =
339346 MkCallAndPos ( Input:: Call call , FunctionPosition pos ) { exists ( call .getArgType ( pos , _) ) }
340347
@@ -356,36 +363,34 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
356363 string toString ( ) { result = call .toString ( ) + " [arg " + pos + "]" }
357364 }
358365
366+ pragma [ nomagic]
367+ private predicate potentialInstantiationOf0 (
368+ CallAndPos cp , Input:: Call call , TypeParameter traitTp , FunctionPosition pos , Function f ,
369+ TypeAbstraction abs , AssocFunctionType constraint
370+ ) {
371+ cp = MkCallAndPos ( call , pragma [ only_bind_into ] ( pos ) ) and
372+ call .hasTargetCand ( abs , f ) and
373+ toCheck ( abs , f , traitTp , pragma [ only_bind_into ] ( pos ) , constraint )
374+ }
375+
359376 private module ArgIsInstantiationOfToIndexInput implements
360377 IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
361378 {
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-
373379 pragma [ nomagic]
374380 predicate potentialInstantiationOf (
375381 CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
376382 ) {
377- exists ( Input:: Call call , int rnk , Function f |
378- potentialInstantiationOf0 ( cp , call , _, rnk , f , abs , constraint )
383+ exists ( Input:: Call call , TypeParameter traitTp , FunctionPosition pos , int rnk , Function f |
384+ potentialInstantiationOf0 ( cp , call , traitTp , pragma [ only_bind_into ] ( pos ) , f , abs , constraint ) and
385+ toCheckRanked ( abs , f , traitTp , pragma [ only_bind_into ] ( pos ) , rnk )
379386 |
380387 rnk = 0
381388 or
382389 argsAreInstantiationsOfToIndex ( call , abs , f , rnk - 1 )
383390 )
384391 }
385392
386- predicate relevantConstraint ( AssocFunctionType constraint ) {
387- Input:: toCheck ( _, _, _, constraint )
388- }
393+ predicate relevantConstraint ( AssocFunctionType constraint ) { toCheck ( _, _, _, _, constraint ) }
389394 }
390395
391396 private module ArgIsInstantiationOfToIndex =
@@ -398,7 +403,11 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
398403 exists ( FunctionPosition pos |
399404 ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPos ( call , pos ) , i , _) and
400405 call .hasTargetCand ( i , f ) and
401- toCheckRanked ( i , f , pos , rnk )
406+ toCheckRanked ( i , f , _, pos , rnk )
407+ |
408+ rnk = 0
409+ or
410+ argsAreInstantiationsOfToIndex ( call , i , f , rnk - 1 )
402411 )
403412 }
404413
@@ -410,15 +419,31 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
410419 predicate argsAreInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
411420 exists ( int rnk |
412421 argsAreInstantiationsOfToIndex ( call , i , f , rnk ) and
413- rnk = max ( int r | toCheckRanked ( i , f , _, r ) )
422+ rnk = max ( int r | toCheckRanked ( i , f , _, _ , r ) )
414423 )
415424 }
416425
426+ private module ArgsAreNotInstantiationOfInput implements
427+ IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
428+ {
429+ pragma [ nomagic]
430+ predicate potentialInstantiationOf (
431+ CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
432+ ) {
433+ potentialInstantiationOf0 ( cp , _, _, _, _, abs , constraint )
434+ }
435+
436+ predicate relevantConstraint ( AssocFunctionType constraint ) { toCheck ( _, _, _, _, constraint ) }
437+ }
438+
439+ private module ArgsAreNotInstantiationOf =
440+ ArgIsInstantiationOf< CallAndPos , ArgsAreNotInstantiationOfInput > ;
441+
417442 pragma [ nomagic]
418443 private predicate argsAreNotInstantiationsOf0 (
419444 Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i
420445 ) {
421- ArgIsInstantiationOfToIndex :: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
446+ ArgsAreNotInstantiationOf :: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
422447 }
423448
424449 /**
@@ -430,7 +455,7 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
430455 exists ( FunctionPosition pos |
431456 argsAreNotInstantiationsOf0 ( call , pos , i ) and
432457 call .hasTargetCand ( i , f ) and
433- Input:: toCheck ( i , f , pos , _ )
458+ Input:: toCheck ( i , f , _ , pos )
434459 )
435460 }
436461}
0 commit comments