@@ -244,10 +244,12 @@ module Consistency {
244244 }
245245}
246246
247+ /** A method, that is, a function with a `self` parameter. */
247248private class Method extends Function {
248249 Method ( ) { this .hasSelfParam ( ) }
249250}
250251
252+ /** A function without a `self` parameter. */
251253private class AssocFunction extends Function {
252254 AssocFunction ( ) { not this .hasSelfParam ( ) }
253255}
@@ -871,17 +873,133 @@ private module ArgIsInstantiationOf<
871873 }
872874 }
873875
874- predicate argIsInstanceOf ( Arg arg , ImplOrTraitItemNode i , FunctionType constraint ) {
876+ predicate argIsInstantiationOf ( Arg arg , ImplOrTraitItemNode i , FunctionType constraint ) {
875877 IsInstantiationOf< ArgSubst , FunctionType , IsInstantiationOfInput > :: isInstantiationOf ( arg , i ,
876878 constraint )
877879 }
878880
879- predicate argIsNotInstanceOf ( Arg arg , ImplOrTraitItemNode i , FunctionType constraint ) {
881+ predicate argIsNotInstantiationOf ( Arg arg , ImplOrTraitItemNode i , FunctionType constraint ) {
880882 IsInstantiationOf< ArgSubst , FunctionType , IsInstantiationOfInput > :: isNotInstantiationOf ( arg , i ,
881883 constraint )
882884 }
883885}
884886
887+ signature module ArgsAreInstantiationsOfInputSig {
888+ predicate toCheck ( ImplOrTraitItemNode i , Function f , FunctionTypePosition pos , FunctionType t ) ;
889+
890+ class Call {
891+ string toString ( ) ;
892+
893+ Location getLocation ( ) ;
894+
895+ Type getArgType ( FunctionTypePosition pos , TypePath path ) ;
896+
897+ predicate hasTargetCand ( ImplOrTraitItemNode i , Function f ) ;
898+ }
899+ }
900+
901+ /**
902+ * A wrapper around `IsInstantiationOf` which ensures to substitute in lookup
903+ * traits when checking whether argument types are instantiations of function
904+ * types.
905+ */
906+ private module ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInputSig Input> {
907+ pragma [ nomagic]
908+ private predicate toCheckRanked (
909+ ImplOrTraitItemNode i , Function f , FunctionTypePosition pos , int rnk
910+ ) {
911+ Input:: toCheck ( i , f , pos , _) and
912+ pos =
913+ rank [ rnk + 1 ] ( FunctionTypePosition pos0 , int j |
914+ Input:: toCheck ( i , f , pos0 , _) and
915+ (
916+ j = pos0 .asPositional ( )
917+ or
918+ pos0 .isSelf ( ) and j = - 1
919+ or
920+ pos0 .isReturn ( ) and j = - 2
921+ )
922+ |
923+ pos0 order by j
924+ )
925+ }
926+
927+ private newtype TCallAndPos =
928+ MkCallAndPos ( Input:: Call call , FunctionTypePosition pos ) {
929+ exists ( call .getArgType ( pos , _) )
930+ // exists(ImplOrTraitItemNode i, Function f |
931+ // Input::toCheck(i, f, pos, _) and
932+ // call.hasTargetCand(i, f)
933+ // )
934+ }
935+
936+ /** An associated function call tagged with a position. */
937+ private class CallAndPos extends MkCallAndPos {
938+ Input:: Call call ;
939+ FunctionTypePosition pos ;
940+
941+ CallAndPos ( ) { this = MkCallAndPos ( call , pos ) }
942+
943+ Input:: Call getCall ( ) { result = call }
944+
945+ FunctionTypePosition getPos ( ) { result = pos }
946+
947+ Location getLocation ( ) { result = call .getLocation ( ) }
948+
949+ Type getTypeAt ( TypePath path ) { result = call .getArgType ( pos , path ) }
950+
951+ string toString ( ) { result = call .toString ( ) + " [arg " + pos + "]" }
952+ }
953+
954+ private module ArgIsIsInstantiationOfInput implements
955+ IsInstantiationOfInputSig< CallAndPos , FunctionType >
956+ {
957+ pragma [ nomagic]
958+ private predicate potentialInstantiationOf0 (
959+ CallAndPos cp , Input:: Call call , FunctionTypePosition pos , int rnk , Function f ,
960+ TypeAbstraction abs , FunctionType constraint
961+ ) {
962+ cp = MkCallAndPos ( call , pos ) and
963+ call .hasTargetCand ( abs , f ) and
964+ toCheckRanked ( abs , f , pos , rnk ) and
965+ Input:: toCheck ( abs , f , pos , constraint )
966+ }
967+
968+ pragma [ nomagic]
969+ predicate potentialInstantiationOf ( CallAndPos cp , TypeAbstraction abs , FunctionType constraint ) {
970+ exists ( Input:: Call call , FunctionTypePosition pos , int rnk , Function f |
971+ potentialInstantiationOf0 ( cp , call , pos , rnk , f , abs , constraint )
972+ |
973+ rnk = 0
974+ or
975+ argsAreInstantiationsOfFromIndex ( call , abs , f , rnk - 1 )
976+ )
977+ }
978+
979+ predicate relevantTypeMention ( FunctionType constraint ) { Input:: toCheck ( _, _, _, constraint ) }
980+ }
981+
982+ pragma [ nomagic]
983+ private predicate argsAreInstantiationsOfFromIndex (
984+ Input:: Call call , ImplOrTraitItemNode i , Function f , int rnk
985+ ) {
986+ exists ( FunctionTypePosition pos |
987+ ArgIsInstantiationOf< CallAndPos , ArgIsIsInstantiationOfInput > :: argIsInstantiationOf ( MkCallAndPos ( call ,
988+ pos ) , i , _) and
989+ call .hasTargetCand ( i , f ) and
990+ toCheckRanked ( i , f , pos , rnk )
991+ )
992+ }
993+
994+ pragma [ nomagic]
995+ predicate argsAreInstantiationsOf ( Input:: Call call , ImplOrTraitItemNode i , Function f ) {
996+ exists ( int rnk |
997+ argsAreInstantiationsOfFromIndex ( call , i , f , rnk ) and
998+ rnk = max ( int r | toCheckRanked ( i , f , _, r ) )
999+ )
1000+ }
1001+ }
1002+
8851003/**
8861004 * Holds if the type path `path` pointing to `type` is stripped of any leading
8871005 * complex root type allowed for `self` parameters, such as `&`, `Box`, `Rc`,
@@ -1167,7 +1285,7 @@ private module MethodResolution {
11671285 */
11681286 pragma [ nomagic]
11691287 private predicate hasIncompatibleTarget ( ImplOrTraitItemNode i , string derefChainBorrow ) {
1170- ArgIsInstantiationOf< MethodCallCand , ReceiverIsInstanceOfSelfParamInput > :: argIsNotInstanceOf ( MkMethodCallCand ( this ,
1288+ ArgIsInstantiationOf< MethodCallCand , ReceiverIsInstanceOfSelfParamInput > :: argIsNotInstantiationOf ( MkMethodCallCand ( this ,
11711289 derefChainBorrow ) , i , _)
11721290 or
11731291 IsInstantiationOf< MethodCallCallExpr , TypeMentionTypeTree , TypeQualifierIsInstanceOfImplSelfInput > :: isNotInstantiationOf ( this ,
@@ -1455,7 +1573,7 @@ private module MethodResolution {
14551573 */
14561574 pragma [ nomagic]
14571575 private predicate hasIncompatibleInherentTarget ( Impl impl ) {
1458- ArgIsInstantiationOf< MethodCallCand , ReceiverIsNotInstanceOfInherentSelfParamInput > :: argIsNotInstanceOf ( this ,
1576+ ArgIsInstantiationOf< MethodCallCand , ReceiverIsNotInstanceOfInherentSelfParamInput > :: argIsNotInstantiationOf ( this ,
14591577 impl , _)
14601578 }
14611579
@@ -1483,9 +1601,9 @@ private module MethodResolution {
14831601 }
14841602
14851603 pragma [ nomagic]
1486- private predicate argIsInstanceOf ( ImplOrTraitItemNode i , string name , int arity ) {
1604+ private predicate argIsInstantiationOf ( ImplOrTraitItemNode i , string name , int arity ) {
14871605 (
1488- ArgIsInstantiationOf< MethodCallCand , ReceiverIsInstanceOfSelfParamInput > :: argIsInstanceOf ( this ,
1606+ ArgIsInstantiationOf< MethodCallCand , ReceiverIsInstanceOfSelfParamInput > :: argIsInstantiationOf ( this ,
14891607 i , _)
14901608 or
14911609 this .typeQualifierIsInstanceOf ( i )
@@ -1494,27 +1612,13 @@ private module MethodResolution {
14941612 }
14951613
14961614 pragma [ nomagic]
1497- private Method resolveCallTargetCand ( ImplOrTraitItemNode i ) {
1615+ Method resolveCallTargetCand ( ImplOrTraitItemNode i ) {
14981616 exists ( string name , int arity |
1499- this .argIsInstanceOf ( i , name , arity ) and
1617+ this .argIsInstantiationOf ( i , name , arity ) and
15001618 result = getMethodSuccessor ( i , name , arity )
15011619 )
15021620 }
15031621
1504- pragma [ nomagic]
1505- private Type inferPositionalArgumentType ( FunctionTypePosition pos , TypePath path ) {
1506- pos .isPositional ( ) and
1507- result = substituteLookupTraits ( inferType ( mc_ .getArgument ( pos .asArgumentPosition ( ) ) , path ) )
1508- }
1509-
1510- pragma [ nomagic]
1511- private Method resolveAmbigousCallTargetCand ( FunctionTypePosition pos , TypePath path , Type type ) {
1512- exists ( ImplOrTraitItemNode i |
1513- result = this .resolveCallTargetCand ( i ) and
1514- FunctionOverloading:: functionResolutionDependsOnArgument ( i , result , pos , path , type )
1515- )
1516- }
1517-
15181622 /** Gets a method that matches this method call. */
15191623 pragma [ nomagic]
15201624 Method resolveCallTarget ( ) {
@@ -1526,10 +1630,7 @@ private module MethodResolution {
15261630 )
15271631 )
15281632 or
1529- exists ( FunctionTypePosition pos , TypePath path , Type type |
1530- result = this .resolveAmbigousCallTargetCand ( pos , path , type ) and
1531- type = this .inferPositionalArgumentType ( pos , path )
1532- )
1633+ ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInput > :: argsAreInstantiationsOf ( this , _, result )
15331634 }
15341635
15351636 string toString ( ) { result = mc_ .toString ( ) + " [" + derefChainBorrow + "]" }
@@ -1650,6 +1751,27 @@ private module MethodResolution {
16501751 methodInfo ( _, _, _, _, constraint , _, _)
16511752 }
16521753 }
1754+
1755+ private module ArgsAreInstantiationsOfInput implements ArgsAreInstantiationsOfInputSig {
1756+ predicate toCheck ( ImplOrTraitItemNode i , Function f , FunctionTypePosition pos , FunctionType t ) {
1757+ exists ( TypePath path , Type t0 |
1758+ pos .isPositional ( ) and
1759+ FunctionOverloading:: functionResolutionDependsOnArgument ( i , f , pos , path , t0 ) and
1760+ t .appliesTo ( f , pos , i ) and
1761+ not t0 instanceof TypeParameter
1762+ )
1763+ }
1764+
1765+ class Call extends MethodCallCand {
1766+ Type getArgType ( FunctionTypePosition pos , TypePath path ) {
1767+ result = inferType ( mc_ .getNodeAt ( pos ) , path )
1768+ }
1769+
1770+ predicate hasTargetCand ( ImplOrTraitItemNode i , Function f ) {
1771+ f = this .resolveCallTargetCand ( i )
1772+ }
1773+ }
1774+ }
16531775}
16541776
16551777/**
@@ -1949,7 +2071,7 @@ private module AssocFunctionResolution {
19492071 * A configuration for matching the type of an argument against the type of
19502072 * a parameter that mentions a satisfied blanket type parameter.
19512073 */
1952- private module ArgIsInstanceOfBlanketParamInput implements
2074+ private module ArgIsInstantiationOfBlanketParamInput implements
19532075 IsInstantiationOfInputSig< AssocFunctionCallAndPos , FunctionType >
19542076 {
19552077 pragma [ nomagic]
@@ -1977,6 +2099,7 @@ private module AssocFunctionResolution {
19772099 forall ( Function f | f = CallExprImpl:: getResolvedFunction ( this ) | f instanceof AssocFunction )
19782100 }
19792101
2102+ pragma [ nomagic]
19802103 predicate hasNameAndArity ( string name , int arity ) {
19812104 name = CallExprImpl:: getFunctionPath ( this ) .getText ( ) and
19822105 arity = this .getArgList ( ) .getNumberOfArgs ( )
@@ -1987,32 +2110,31 @@ private module AssocFunctionResolution {
19872110 * if any.
19882111 */
19892112 private ItemNode getPathResolutionResolved ( ) {
1990- result = CallExprImpl:: getResolvedFunction ( this ) and
1991- not result .( Function ) .hasSelfParam ( )
2113+ result = CallExprImpl:: getResolvedFunction ( this )
19922114 }
19932115
19942116 /**
1995- * Gets the blanket function that this call resolves to, if any.
2117+ * Gets the blanket function that this call may resolve to, if any.
19962118 */
19972119 pragma [ nomagic]
1998- private ItemNode resolveCallTargetCand ( ) {
1999- not this .( Call ) .hasTrait ( ) and
2000- result = this .getPathResolutionResolved ( )
2001- or
2002- exists ( ImplItemNode impl , string name |
2003- this .hasNameAndArity ( name , _) and
2004- ArgIsInstantiationOf< AssocFunctionCallAndPos , ArgIsInstanceOfBlanketParamInput > :: argIsInstanceOf ( MkAssocFunctionCallAndPos ( this ,
2120+ private AssocFunction resolveCallTargetBlanketCand ( ImplItemNode impl ) {
2121+ exists ( string name |
2122+ this .hasNameAndArity ( pragma [ only_bind_into ] ( name ) , _) and
2123+ ArgIsInstantiationOf< AssocFunctionCallAndPos , ArgIsInstantiationOfBlanketParamInput > :: argIsInstantiationOf ( MkAssocFunctionCallAndPos ( this ,
20052124 _) , impl , _) and
2006- result = impl .getASuccessor ( name )
2125+ result = impl .getASuccessor ( pragma [ only_bind_into ] ( name ) )
20072126 )
20082127 }
20092128
20102129 pragma [ nomagic]
2011- private AssocFunction resolveAmbigousCallTargetCand (
2012- FunctionTypePosition pos , TypePath path , Type type
2013- ) {
2014- result = this .resolveCallTargetCand ( ) and
2015- functionResolutionDependsOnArgument ( _, result , pos , path , type )
2130+ AssocFunction foo ( ImplItemNode impl ) {
2131+ (
2132+ not this .( Call ) .hasTrait ( ) and
2133+ result = this .getPathResolutionResolved ( ) and
2134+ result = impl .getASuccessor ( _)
2135+ or
2136+ result = this .resolveCallTargetBlanketCand ( impl )
2137+ )
20162138 }
20172139
20182140 AstNode getNodeAt ( FunctionTypePosition pos ) {
@@ -2030,7 +2152,7 @@ private module AssocFunctionResolution {
20302152 }
20312153
20322154 pragma [ nomagic]
2033- private predicate hasTraitResolved (
2155+ predicate hasTraitResolved (
20342156 TraitItemNode trait , AssocFunction resolved , FunctionTypePosition pos , TypePath path ,
20352157 Type type
20362158 ) {
@@ -2041,19 +2163,48 @@ private module AssocFunctionResolution {
20412163
20422164 pragma [ nomagic]
20432165 ItemNode resolveCallTarget ( ) {
2044- result = this .resolveCallTargetCand ( ) and
2166+ (
2167+ not this .( Call ) .hasTrait ( ) and
2168+ result = this .getPathResolutionResolved ( )
2169+ or
2170+ result = this .resolveCallTargetBlanketCand ( _)
2171+ ) and
20452172 not functionResolutionDependsOnArgument ( _, result , _, _, _)
20462173 or
2047- exists ( FunctionTypePosition pos , TypePath path , Type type |
2048- result = this .resolveAmbigousCallTargetCand ( pos , path , type ) and
2049- type = this .inferArgumentType ( pos , path )
2174+ ArgsAreInstantiationsOf< ArgsAreInstantiationsOfInput > :: argsAreInstantiationsOf ( this , _, result )
2175+ }
2176+ }
2177+
2178+ private module ArgsAreInstantiationsOfInput implements ArgsAreInstantiationsOfInputSig {
2179+ predicate toCheck ( ImplOrTraitItemNode i , Function f , FunctionTypePosition pos , FunctionType t ) {
2180+ // FunctionOverloading::functionResolutionDependsOnArgument(i, f, pos, _, _) and
2181+ // t.appliesTo(f, pos, i)
2182+ exists ( Type t0 |
2183+ FunctionOverloading:: functionResolutionDependsOnArgument ( i , f , pos , _, t0 ) and
2184+ t .appliesTo ( f , pos , i ) and
2185+ not t0 instanceof TypeParameter
2186+ )
2187+ or
2188+ traitFunctionDependsOnArgument ( _, _, pos , f , _, _) and
2189+ t .appliesTo ( f , pos , i )
2190+ }
2191+
2192+ class Call extends AssocFunctionCall {
2193+ Type getArgType ( FunctionTypePosition pos , TypePath path ) {
2194+ result = inferType ( this .getNodeAt ( pos ) , path )
2195+ }
2196+
2197+ predicate hasTargetCand ( ImplOrTraitItemNode i , Function f ) {
2198+ f = this .foo ( i )
20502199 or
2051- // E.g. `Default::default()`
2052- exists ( TraitItemNode trait , AssocFunction resolved |
2053- this .hasTraitResolved ( trait , resolved , pos , path , type ) and
2054- traitFunctionDependsOnArgument ( trait , resolved , pos , result , path , type )
2200+ exists ( FunctionTypePosition pos |
2201+ exists ( TraitItemNode trait , AssocFunction resolved |
2202+ this .hasTraitResolved ( trait , resolved , pos , _, _) and
2203+ traitFunctionDependsOnArgument ( trait , resolved , pos , f , _, _) and
2204+ f = i .getASuccessor ( _)
2205+ )
20552206 )
2056- )
2207+ }
20572208 }
20582209 }
20592210}
0 commit comments