@@ -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, pos, f, abs, constraint) and
385+ toCheckRanked(abs, f, traitTp, 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,39 +403,63 @@ 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
405414 /**
406415 * Holds if all arguments of `call` have types that are instantiations of the
407416 * types of the corresponding parameters of `f` inside `i`.
417+ *
418+ * TODO: Check type parameter constraints as well.
408419 */
409420 pragma[nomagic]
410421 predicate argsAreInstantiationsOf(Input::Call call, ImplOrTraitItemNode i, Function f) {
411422 exists(int rnk |
412423 argsAreInstantiationsOfToIndex(call, i, f, rnk) and
413- rnk = max(int r | toCheckRanked(i, f, _, r))
424+ rnk = max(int r | toCheckRanked(i, f, _, _, r))
414425 )
415426 }
416427
428+ private module ArgsAreNotInstantiationOfInput implements
429+ IsInstantiationOfInputSig<CallAndPos, AssocFunctionType>
430+ {
431+ pragma[nomagic]
432+ predicate potentialInstantiationOf(
433+ CallAndPos cp, TypeAbstraction abs, AssocFunctionType constraint
434+ ) {
435+ potentialInstantiationOf0(cp, _, _, _, _, abs, constraint)
436+ }
437+
438+ predicate relevantConstraint(AssocFunctionType constraint) { toCheck(_, _, _, _, constraint) }
439+ }
440+
441+ private module ArgsAreNotInstantiationOf =
442+ ArgIsInstantiationOf<CallAndPos, ArgsAreNotInstantiationOfInput>;
443+
417444 pragma[nomagic]
418445 private predicate argsAreNotInstantiationsOf0(
419446 Input::Call call, FunctionPosition pos, ImplOrTraitItemNode i
420447 ) {
421- ArgIsInstantiationOfToIndex ::argIsNotInstantiationOf(MkCallAndPos(call, pos), i, _, _)
448+ ArgsAreNotInstantiationOf ::argIsNotInstantiationOf(MkCallAndPos(call, pos), i, _, _)
422449 }
423450
424451 /**
425452 * Holds if _some_ argument of `call` has a type that is not an instantiation of the
426453 * type of the corresponding parameter of `f` inside `i`.
454+ *
455+ * TODO: Check type parameter constraints as well.
427456 */
428457 pragma[nomagic]
429458 predicate argsAreNotInstantiationsOf(Input::Call call, ImplOrTraitItemNode i, Function f) {
430459 exists(FunctionPosition pos |
431460 argsAreNotInstantiationsOf0(call, pos, i) and
432461 call.hasTargetCand(i, f) and
433- Input::toCheck(i, f, pos, _ )
462+ Input::toCheck(i, f, _, pos )
434463 )
435464 }
436465}
0 commit comments