@@ -241,3 +241,163 @@ Type substituteLookupTraits(Type t) {
241241 or
242242 result = TTrait ( getALookupTrait ( t ) )
243243}
244+
245+ /**
246+ * A wrapper around `IsInstantiationOf` which ensures to substitute in lookup
247+ * traits when checking whether argument types are instantiations of function
248+ * types.
249+ */
250+ module ArgIsInstantiationOf< HasTypeTreeSig Arg, IsInstantiationOfInputSig< Arg , FunctionType > Input> {
251+ final private class ArgFinal = Arg ;
252+
253+ private class ArgSubst extends ArgFinal {
254+ Type getTypeAt ( TypePath path ) { result = substituteLookupTraits ( super .getTypeAt ( path ) ) }
255+ }
256+
257+ private module IsInstantiationOfInput implements IsInstantiationOfInputSig< ArgSubst , FunctionType >
258+ {
259+ pragma [ nomagic]
260+ predicate potentialInstantiationOf ( ArgSubst arg , TypeAbstraction abs , FunctionType constraint ) {
261+ Input:: potentialInstantiationOf ( arg , abs , constraint )
262+ }
263+
264+ predicate relevantTypeMention ( FunctionType constraint ) {
265+ Input:: relevantTypeMention ( constraint )
266+ }
267+ }
268+
269+ private module ArgSubstIsInstantiationOf =
270+ IsInstantiationOf< ArgSubst , FunctionType , IsInstantiationOfInput > ;
271+
272+ predicate argIsInstantiationOf ( Arg arg , ImplOrTraitItemNode i , FunctionType constraint ) {
273+ ArgSubstIsInstantiationOf:: isInstantiationOf ( arg , i , constraint )
274+ }
275+
276+ predicate argIsNotInstantiationOf ( Arg arg , ImplOrTraitItemNode i , FunctionType constraint ) {
277+ ArgSubstIsInstantiationOf:: isNotInstantiationOf ( arg , i , constraint )
278+ }
279+ }
280+
281+ /**
282+ * Provides the input for `ArgsAreInstantiationsOf`.
283+ */
284+ signature module ArgsAreInstantiationsOfInputSig {
285+ /**
286+ * Holds if types need to matched against the type `t` at position `pos` of
287+ * `f` inside `i`.
288+ */
289+ predicate toCheck ( ImplOrTraitItemNode i , Function f , FunctionTypePosition pos , FunctionType t ) ;
290+
291+ /** A call whose argument types are to be checked. */
292+ class Call {
293+ string toString ( ) ;
294+
295+ Location getLocation ( ) ;
296+
297+ Type getArgType ( FunctionTypePosition pos , TypePath path ) ;
298+
299+ predicate hasTargetCand ( ImplOrTraitItemNode i , Function f ) ;
300+ }
301+ }
302+
303+ /**
304+ * Provides logic for checking that a set of arguments have types that are
305+ * instantiations of the types at the corresponding positions in a function
306+ * type.
307+ */
308+ module ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInputSig Input> {
309+ pragma [ nomagic]
310+ private predicate toCheckRanked (
311+ ImplOrTraitItemNode i , Function f , FunctionTypePosition pos , int rnk
312+ ) {
313+ Input:: toCheck ( i , f , pos , _) and
314+ pos =
315+ rank [ rnk + 1 ] ( FunctionTypePosition pos0 , int j |
316+ Input:: toCheck ( i , f , pos0 , _) and
317+ (
318+ j = pos0 .asPositional ( )
319+ or
320+ pos0 .isSelf ( ) and j = - 1
321+ or
322+ pos0 .isReturn ( ) and j = - 2
323+ )
324+ |
325+ pos0 order by j
326+ )
327+ }
328+
329+ private newtype TCallAndPos =
330+ MkCallAndPos ( Input:: Call call , FunctionTypePosition pos ) { exists ( call .getArgType ( pos , _) ) }
331+
332+ /** A call tagged with a position. */
333+ private class CallAndPos extends MkCallAndPos {
334+ Input:: Call call ;
335+ FunctionTypePosition pos ;
336+
337+ CallAndPos ( ) { this = MkCallAndPos ( call , pos ) }
338+
339+ Input:: Call getCall ( ) { result = call }
340+
341+ FunctionTypePosition getPos ( ) { result = pos }
342+
343+ Location getLocation ( ) { result = call .getLocation ( ) }
344+
345+ Type getTypeAt ( TypePath path ) { result = call .getArgType ( pos , path ) }
346+
347+ string toString ( ) { result = call .toString ( ) + " [arg " + pos + "]" }
348+ }
349+
350+ private module ArgIsInstantiationOfInput implements
351+ IsInstantiationOfInputSig< CallAndPos , FunctionType >
352+ {
353+ pragma [ nomagic]
354+ private predicate potentialInstantiationOf0 (
355+ CallAndPos cp , Input:: Call call , FunctionTypePosition pos , int rnk , Function f ,
356+ TypeAbstraction abs , FunctionType constraint
357+ ) {
358+ cp = MkCallAndPos ( call , pos ) and
359+ call .hasTargetCand ( abs , f ) and
360+ toCheckRanked ( abs , f , pos , rnk ) and
361+ Input:: toCheck ( abs , f , pos , constraint )
362+ }
363+
364+ pragma [ nomagic]
365+ predicate potentialInstantiationOf ( CallAndPos cp , TypeAbstraction abs , FunctionType constraint ) {
366+ exists ( Input:: Call call , FunctionTypePosition pos , int rnk , Function f |
367+ potentialInstantiationOf0 ( cp , call , pos , rnk , f , abs , constraint )
368+ |
369+ rnk = 0
370+ or
371+ argsAreInstantiationsOfFromIndex ( call , abs , f , rnk - 1 )
372+ )
373+ }
374+
375+ predicate relevantTypeMention ( FunctionType constraint ) { Input:: toCheck ( _, _, _, constraint ) }
376+ }
377+
378+ private module ArgIsInstantiationOfFromIndex =
379+ ArgIsInstantiationOf< CallAndPos , ArgIsInstantiationOfInput > ;
380+
381+ pragma [ nomagic]
382+ private predicate argsAreInstantiationsOfFromIndex (
383+ Input:: Call call , ImplOrTraitItemNode i , Function f , int rnk
384+ ) {
385+ exists ( FunctionTypePosition pos |
386+ ArgIsInstantiationOfFromIndex:: argIsInstantiationOf ( MkCallAndPos ( call , pos ) , i , _) and
387+ call .hasTargetCand ( i , f ) and
388+ toCheckRanked ( i , f , pos , rnk )
389+ )
390+ }
391+
392+ /**
393+ * Holds if all arguments of `call` have types that are instantiations of the
394+ * types of the corresponding parameters of `f` inside `i`.
395+ */
396+ pragma [ nomagic]
397+ predicate argsAreInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
398+ exists ( int rnk |
399+ argsAreInstantiationsOfFromIndex ( call , i , f , rnk ) and
400+ rnk = max ( int r | toCheckRanked ( i , f , _, r ) )
401+ )
402+ }
403+ }
0 commit comments