@@ -5,114 +5,51 @@ private import TypeAbstraction
55private import TypeMention
66private import TypeInference
77
8- private signature predicate includeSelfSig ( ) ;
9-
10- // We construct `FunctionPosition` and `FunctionPositionAdj` using two different underlying
11- // `newtype`s in order to prevent unintended mixing of the two
12- private module MkFunctionPosition< includeSelfSig / 0 includeSelf> {
13- private newtype TFunctionPosition =
14- TArgumentFunctionPosition ( ArgumentPosition pos ) {
15- if pos .isSelf ( ) then includeSelf ( ) else any ( )
16- } or
17- TReturnFunctionPosition ( )
18-
19- class FunctionPosition extends TFunctionPosition {
20- int asPosition ( ) { result = this .asArgumentPosition ( ) .asPosition ( ) }
21-
22- predicate isPosition ( ) { exists ( this .asPosition ( ) ) }
23-
24- ArgumentPosition asArgumentPosition ( ) { this = TArgumentFunctionPosition ( result ) }
25-
26- predicate isTypeQualifier ( ) { this .asArgumentPosition ( ) .isTypeQualifier ( ) }
27-
28- predicate isReturn ( ) { this = TReturnFunctionPosition ( ) }
29-
30- TypeMention getTypeMention ( Function f ) {
31- result = f .getParam ( this .asPosition ( ) ) .getTypeRepr ( )
32- or
33- this .isReturn ( ) and
34- result = getReturnTypeMention ( f )
35- }
36-
37- string toString ( ) {
38- result = this .asArgumentPosition ( ) .toString ( )
39- or
40- this .isReturn ( ) and
41- result = "(return)"
42- }
43- }
44- }
45-
46- private predicate any_ ( ) { any ( ) }
8+ private newtype TFunctionPosition =
9+ TArgumentFunctionPosition ( ArgumentPosition pos ) { not pos .isSelf ( ) } or
10+ TReturnFunctionPosition ( )
4711
4812/**
49- * A position of a type related to a function.
13+ * A function-call adjusted position of a type related to a function.
5014 *
51- * Either `self`, `return`, or a positional parameter index.
15+ * Either `return` or a positional parameter index, where `self` is translated
16+ * to position `0` and subsequent positional parameters at index `i` are
17+ * translated to position `i + 1`.
5218 */
53- final class FunctionPosition extends MkFunctionPosition < any_ / 0 > :: FunctionPosition {
54- predicate isSelf ( ) { this .asArgumentPosition ( ) .isSelf ( ) }
19+ class FunctionPosition extends TFunctionPosition {
20+ int asPosition ( ) { result = this .asArgumentPosition ( ) .asPosition ( ) }
5521
56- predicate isSelfOrTypeQualifier ( ) { this . isSelf ( ) or this .isTypeQualifier ( ) }
22+ predicate isPosition ( ) { exists ( this .asPosition ( ) ) }
5723
58- override TypeMention getTypeMention ( Function f ) {
59- result = super .getTypeMention ( f )
60- or
61- this .isSelf ( ) and
62- result = getSelfParamTypeMention ( f .getSelfParam ( ) )
63- }
24+ ArgumentPosition asArgumentPosition ( ) { this = TArgumentFunctionPosition ( result ) }
6425
65- /**
66- * Gets the corresponding position when function call syntax is used, assuming
67- * this position is for a method.
68- */
69- pragma [ nomagic]
70- FunctionPositionAdj getFunctionCallAdjusted ( ) {
71- this .isReturn ( ) and result .isReturn ( )
72- or
73- this .isTypeQualifier ( ) and
74- result .isTypeQualifier ( )
75- or
76- this .isSelf ( ) and result .asPosition ( ) = 0
77- or
78- result .asPosition ( ) = this .asPosition ( ) + 1
79- }
26+ predicate isTypeQualifier ( ) { this .asArgumentPosition ( ) .isTypeQualifier ( ) }
8027
81- /**
82- * Gets the corresponding position when function call syntax is used, assuming
83- * this position is _not_ for a method.
84- */
85- pragma [ nomagic]
86- FunctionPositionAdj asAdjusted ( ) {
87- this .isReturn ( ) and result .isReturn ( )
88- or
89- this .isTypeQualifier ( ) and
90- result .isTypeQualifier ( )
28+ predicate isReturn ( ) { this = TReturnFunctionPosition ( ) }
29+
30+ TypeMention getTypeMention ( Function f ) {
31+ (
32+ if f instanceof Method
33+ then
34+ result = f .getParam ( this .asPosition ( ) - 1 ) .getTypeRepr ( )
35+ or
36+ result = getSelfParamTypeMention ( f .getSelfParam ( ) ) and
37+ this .asPosition ( ) = 0
38+ else result = f .getParam ( this .asPosition ( ) ) .getTypeRepr ( )
39+ )
9140 or
92- result .asPosition ( ) = this .asPosition ( )
41+ this .isReturn ( ) and
42+ result = getReturnTypeMention ( f )
9343 }
9444
95- /**
96- * Gets the corresponding position when `f` is invoked via function call
97- * syntax.
98- */
99- bindingset [ f]
100- FunctionPositionAdj getFunctionCallAdjusted ( Function f ) {
101- if f .hasSelfParam ( ) then result = this .getFunctionCallAdjusted ( ) else result = this .asAdjusted ( )
45+ string toString ( ) {
46+ result = this .asArgumentPosition ( ) .toString ( )
47+ or
48+ this .isReturn ( ) and
49+ result = "(return)"
10250 }
10351}
10452
105- private predicate none_ ( ) { none ( ) }
106-
107- /**
108- * A function-call adjust position of a type related to a function.
109- *
110- * Either `return` or a positional parameter index.
111- */
112- final class FunctionPositionAdj extends MkFunctionPosition< none_ / 0 > :: FunctionPosition {
113- FunctionPosition asNonAdjusted ( ) { this = result .asAdjusted ( ) }
114- }
115-
11653/**
11754 * A helper module for implementing `Matching(WithEnvironment)InputSig` with
11855 * `DeclarationPosition = AccessPosition = FunctionPosition`.
@@ -127,20 +64,6 @@ module FunctionPositionMatchingInput {
12764 }
12865}
12966
130- /**
131- * A helper module for implementing `Matching(WithEnvironment)InputSig` with
132- * `DeclarationPosition = AccessPosition = FunctionPositionAdj`.
133- */
134- module FunctionPositionAdjMatchingInput {
135- class DeclarationPosition = FunctionPositionAdj ;
136-
137- class AccessPosition = DeclarationPosition ;
138-
139- predicate accessDeclarationPositionMatch ( AccessPosition apos , DeclarationPosition dpos ) {
140- apos = dpos
141- }
142- }
143-
14467private newtype TAssocFunctionType =
14568 /** An associated function `f` in `parent` should be specialized for `i` at `pos`. */
14669 MkAssocFunctionType (
@@ -378,18 +301,18 @@ signature module ArgsAreInstantiationsOfInputSig {
378301 * `tp` is a type parameter of the trait being implemented by `f` or the trait to which
379302 * `f` belongs.
380303 *
381- * `posAdj ` is one of the function-call adjusted positions in `f` in which the relevant
304+ * `pos ` is one of the function-call adjusted positions in `f` in which the relevant
382305 * type occurs.
383306 */
384- predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPositionAdj posAdj ) ;
307+ predicate toCheck ( ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos ) ;
385308
386309 /** A call whose argument types are to be checked. */
387310 class Call {
388311 string toString ( ) ;
389312
390313 Location getLocation ( ) ;
391314
392- Type getArgType ( FunctionPositionAdj posAdj , TypePath path ) ;
315+ Type getArgType ( FunctionPosition pos , TypePath path ) ;
393316
394317 predicate hasTargetCand ( ImplOrTraitItemNode i , Function f ) ;
395318 }
@@ -403,9 +326,9 @@ signature module ArgsAreInstantiationsOfInputSig {
403326module ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInputSig Input> {
404327 pragma [ nomagic]
405328 private predicate toCheckRanked (
406- ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPositionAdj posAdj , int rnk
329+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos , int rnk
407330 ) {
408- Input:: toCheck ( i , f , tp , posAdj ) and
331+ Input:: toCheck ( i , f , tp , pos ) and
409332 tp =
410333 rank [ rnk + 1 ] ( TypeParameter tp0 , int j |
411334 Input:: toCheck ( i , f , tp0 , _) and
@@ -417,59 +340,53 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
417340
418341 pragma [ nomagic]
419342 private predicate toCheck (
420- ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPositionAdj posAdj ,
421- AssocFunctionType t
343+ ImplOrTraitItemNode i , Function f , TypeParameter tp , FunctionPosition pos , AssocFunctionType t
422344 ) {
423- exists ( FunctionPosition pos |
424- Input:: toCheck ( i , f , tp , posAdj ) and
425- t .appliesTo ( f , i , pos ) and
426- posAdj = pos .getFunctionCallAdjusted ( f )
427- )
345+ Input:: toCheck ( i , f , tp , pos ) and
346+ t .appliesTo ( f , i , pos )
428347 }
429348
430- private newtype TCallAndPosAdj =
431- MkCallAndPosAdj ( Input:: Call call , FunctionPositionAdj posAdj ) {
432- exists ( call .getArgType ( posAdj , _) )
433- }
349+ private newtype TCallAndPos =
350+ MkCallAndPos ( Input:: Call call , FunctionPosition pos ) { exists ( call .getArgType ( pos , _) ) }
434351
435352 /** A call tagged with a function-call adjusted position. */
436- private class CallAndPosAdj extends MkCallAndPosAdj {
353+ private class CallAndPos extends MkCallAndPos {
437354 Input:: Call call ;
438- FunctionPositionAdj posAdj ;
355+ FunctionPosition pos ;
439356
440- CallAndPosAdj ( ) { this = MkCallAndPosAdj ( call , posAdj ) }
357+ CallAndPos ( ) { this = MkCallAndPos ( call , pos ) }
441358
442359 Input:: Call getCall ( ) { result = call }
443360
444- FunctionPositionAdj getPosAdj ( ) { result = posAdj }
361+ FunctionPosition getPos ( ) { result = pos }
445362
446363 Location getLocation ( ) { result = call .getLocation ( ) }
447364
448- Type getTypeAt ( TypePath path ) { result = call .getArgType ( posAdj , path ) }
365+ Type getTypeAt ( TypePath path ) { result = call .getArgType ( pos , path ) }
449366
450- string toString ( ) { result = call .toString ( ) + " [arg " + posAdj + "]" }
367+ string toString ( ) { result = call .toString ( ) + " [arg " + pos + "]" }
451368 }
452369
453370 pragma [ nomagic]
454371 private predicate potentialInstantiationOf0 (
455- CallAndPosAdj cp , Input:: Call call , TypeParameter tp , FunctionPositionAdj posAdj , Function f ,
372+ CallAndPos cp , Input:: Call call , TypeParameter tp , FunctionPosition pos , Function f ,
456373 TypeAbstraction abs , AssocFunctionType constraint
457374 ) {
458- cp = MkCallAndPosAdj ( call , pragma [ only_bind_into ] ( posAdj ) ) and
375+ cp = MkCallAndPos ( call , pragma [ only_bind_into ] ( pos ) ) and
459376 call .hasTargetCand ( abs , f ) and
460- toCheck ( abs , f , tp , pragma [ only_bind_into ] ( posAdj ) , constraint )
377+ toCheck ( abs , f , tp , pragma [ only_bind_into ] ( pos ) , constraint )
461378 }
462379
463380 private module ArgIsInstantiationOfToIndexInput implements
464- IsInstantiationOfInputSig< CallAndPosAdj , AssocFunctionType >
381+ IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
465382 {
466383 pragma [ nomagic]
467384 predicate potentialInstantiationOf (
468- CallAndPosAdj cp , TypeAbstraction abs , AssocFunctionType constraint
385+ CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
469386 ) {
470- exists ( Input:: Call call , TypeParameter tp , FunctionPositionAdj posAdj , int rnk , Function f |
471- potentialInstantiationOf0 ( cp , call , tp , posAdj , f , abs , constraint ) and
472- toCheckRanked ( abs , f , tp , posAdj , rnk )
387+ exists ( Input:: Call call , TypeParameter tp , FunctionPosition pos , int rnk , Function f |
388+ potentialInstantiationOf0 ( cp , call , tp , pos , f , abs , constraint ) and
389+ toCheckRanked ( abs , f , tp , pos , rnk )
473390 |
474391 rnk = 0
475392 or
@@ -481,15 +398,15 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
481398 }
482399
483400 private module ArgIsInstantiationOfToIndex =
484- ArgIsInstantiationOf< CallAndPosAdj , ArgIsInstantiationOfToIndexInput > ;
401+ ArgIsInstantiationOf< CallAndPos , ArgIsInstantiationOfToIndexInput > ;
485402
486403 pragma [ nomagic]
487404 private predicate argIsInstantiationOf (
488405 Input:: Call call , ImplOrTraitItemNode i , Function f , int rnk
489406 ) {
490- exists ( FunctionPositionAdj posAdj |
491- ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPosAdj ( call , posAdj ) , i , _) and
492- toCheckRanked ( i , f , _, posAdj , rnk )
407+ exists ( FunctionPosition pos |
408+ ArgIsInstantiationOfToIndex:: argIsInstantiationOf ( MkCallAndPos ( call , pos ) , i , _) and
409+ toCheckRanked ( i , f , _, pos , rnk )
493410 )
494411 }
495412
@@ -521,11 +438,11 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
521438 }
522439
523440 private module ArgsAreNotInstantiationOfInput implements
524- IsInstantiationOfInputSig< CallAndPosAdj , AssocFunctionType >
441+ IsInstantiationOfInputSig< CallAndPos , AssocFunctionType >
525442 {
526443 pragma [ nomagic]
527444 predicate potentialInstantiationOf (
528- CallAndPosAdj cp , TypeAbstraction abs , AssocFunctionType constraint
445+ CallAndPos cp , TypeAbstraction abs , AssocFunctionType constraint
529446 ) {
530447 potentialInstantiationOf0 ( cp , _, _, _, _, abs , constraint )
531448 }
@@ -534,13 +451,13 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
534451 }
535452
536453 private module ArgsAreNotInstantiationOf =
537- ArgIsInstantiationOf< CallAndPosAdj , ArgsAreNotInstantiationOfInput > ;
454+ ArgIsInstantiationOf< CallAndPos , ArgsAreNotInstantiationOfInput > ;
538455
539456 pragma [ nomagic]
540457 private predicate argsAreNotInstantiationsOf0 (
541- Input:: Call call , FunctionPositionAdj posAdj , ImplOrTraitItemNode i
458+ Input:: Call call , FunctionPosition pos , ImplOrTraitItemNode i
542459 ) {
543- ArgsAreNotInstantiationOf:: argIsNotInstantiationOf ( MkCallAndPosAdj ( call , posAdj ) , i , _, _)
460+ ArgsAreNotInstantiationOf:: argIsNotInstantiationOf ( MkCallAndPos ( call , pos ) , i , _, _)
544461 }
545462
546463 /**
@@ -551,10 +468,10 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
551468 */
552469 pragma [ nomagic]
553470 predicate argsAreNotInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
554- exists ( FunctionPositionAdj posAdj |
555- argsAreNotInstantiationsOf0 ( call , posAdj , i ) and
471+ exists ( FunctionPosition pos |
472+ argsAreNotInstantiationsOf0 ( call , pos , i ) and
556473 call .hasTargetCand ( i , f ) and
557- Input:: toCheck ( i , f , _, posAdj )
474+ Input:: toCheck ( i , f , _, pos )
558475 )
559476 }
560477}
0 commit comments