@@ -294,10 +294,14 @@ 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.
301+ *
302+ * For example, i
299303 */
300- predicate toCheck ( ImplOrTraitItemNode i , Function f , FunctionPosition pos , AssocFunctionType t ) ;
304+ predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter traitTp , FunctionPosition pos ) ;
301305
302306 /** A call whose argument types are to be checked. */
303307 class Call {
@@ -318,23 +322,28 @@ signature module ArgsAreInstantiationsOfInputSig {
318322 */
319323module ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInputSig Input> {
320324 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- )
325+ private predicate toCheckRanked (
326+ ImplOrTraitItemNode i , Function f , TypeParameter traitTp , FunctionPosition pos , int rnk
327+ ) {
328+ Input:: toCheck ( i , f , traitTp , pos ) and
329+ traitTp =
330+ rank [ rnk + 1 ] ( TypeParameter traitTp0 , int j |
331+ Input:: toCheck ( i , f , traitTp0 , _) and
332+ j = getTypeParameterId ( traitTp0 )
333333 |
334- pos0 order by j
334+ traitTp0 order by j
335335 )
336336 }
337337
338+ pragma [ nomagic]
339+ private predicate toCheck (
340+ ImplOrTraitItemNode i , Function f , TypeParameter traitTp , FunctionPosition pos ,
341+ AssocFunctionType t
342+ ) {
343+ Input:: toCheck ( i , f , traitTp , pos ) and
344+ t .appliesTo ( f , i , pos )
345+ }
346+
338347 private newtype TCallAndPos =
339348 MkCallAndPos ( Input:: Call call , FunctionPosition pos ) { exists ( call .getArgType ( pos , _) ) }
340349
@@ -356,36 +365,34 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
356365 string toString ( ) { result = call .toString ( ) + " [arg " + pos + "]" }
357366 }
358367
368+ pragma [ nomagic]
369+ private predicate potentialInstantiationOf0 (
370+ CallAndPos cp , Input:: Call call , TypeParameter traitTp , FunctionPosition pos , Function f ,
371+ TypeAbstraction abs , AssocFunctionType constraint
372+ ) {
373+ cp = MkCallAndPos ( call , pragma [ only_bind_into ] ( pos ) ) and
374+ call .hasTargetCand ( abs , f ) and
375+ toCheck ( abs , f , traitTp , pragma [ only_bind_into ] ( pos ) , constraint )
376+ }
377+
359378 private module ArgIsInstantiationOfToIndexInput implements
360379 IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
361380 {
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-
373381 pragma [ nomagic]
374382 predicate potentialInstantiationOf (
375383 CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
376384 ) {
377- exists ( Input:: Call call , int rnk , Function f |
378- potentialInstantiationOf0 ( cp , call , _, rnk , f , abs , constraint )
385+ exists ( Input:: Call call , TypeParameter traitTp , FunctionPosition pos , int rnk , Function f |
386+ potentialInstantiationOf0 ( cp , call , traitTp , pragma [ only_bind_into ] ( pos ) , f , abs , constraint ) and
387+ toCheckRanked ( abs , f , traitTp , pragma [ only_bind_into ] ( pos ) , rnk )
379388 |
380389 rnk = 0
381390 or
382391 argsAreInstantiationsOfToIndex ( call , abs , f , rnk - 1 )
383392 )
384393 }
385394
386- predicate relevantConstraint ( AssocFunctionType constraint ) {
387- Input:: toCheck ( _, _, _, constraint )
388- }
395+ predicate relevantConstraint ( AssocFunctionType constraint ) { toCheck ( _, _, _, _, constraint ) }
389396 }
390397
391398 private module ArgIsInstantiationOfToIndex =
@@ -398,39 +405,63 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
398405 exists ( FunctionPosition pos |
399406 ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPos ( call , pos ) , i , _) and
400407 call .hasTargetCand ( i , f ) and
401- toCheckRanked ( i , f , pos , rnk )
408+ toCheckRanked ( i , f , _, pos , rnk )
409+ |
410+ rnk = 0
411+ or
412+ argsAreInstantiationsOfToIndex ( call , i , f , rnk - 1 )
402413 )
403414 }
404415
405416 /**
406417 * Holds if all arguments of `call` have types that are instantiations of the
407418 * types of the corresponding parameters of `f` inside `i`.
419+ *
420+ * TODO: Check type parameter constraints as well.
408421 */
409422 pragma [ nomagic]
410423 predicate argsAreInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
411424 exists ( int rnk |
412425 argsAreInstantiationsOfToIndex ( call , i , f , rnk ) and
413- rnk = max ( int r | toCheckRanked ( i , f , _, r ) )
426+ rnk = max ( int r | toCheckRanked ( i , f , _, _ , r ) )
414427 )
415428 }
416429
430+ private module ArgsAreNotInstantiationOfInput implements
431+ IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
432+ {
433+ pragma [ nomagic]
434+ predicate potentialInstantiationOf (
435+ CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
436+ ) {
437+ potentialInstantiationOf0 ( cp , _, _, _, _, abs , constraint )
438+ }
439+
440+ predicate relevantConstraint ( AssocFunctionType constraint ) { toCheck ( _, _, _, _, constraint ) }
441+ }
442+
443+ private module ArgsAreNotInstantiationOf =
444+ ArgIsInstantiationOf< CallAndPos , ArgsAreNotInstantiationOfInput > ;
445+
417446 pragma [ nomagic]
418447 private predicate argsAreNotInstantiationsOf0 (
419448 Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i
420449 ) {
421- ArgIsInstantiationOfToIndex :: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
450+ ArgsAreNotInstantiationOf :: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
422451 }
423452
424453 /**
425454 * Holds if _some_ argument of `call` has a type that is not an instantiation of the
426455 * type of the corresponding parameter of `f` inside `i`.
456+ *
457+ * TODO: Check type parameter constraints as well.
427458 */
428459 pragma [ nomagic]
429460 predicate argsAreNotInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
430461 exists ( FunctionPosition pos |
431462 argsAreNotInstantiationsOf0 ( call , pos , i ) and
432463 call .hasTargetCand ( i , f ) and
433- Input:: toCheck ( i , f , pos , _ )
464+ Input:: toCheck ( i , f , _ , pos )
434465 )
435466 }
436467}
0 commit comments