@@ -1226,7 +1226,9 @@ private module MethodCallResolution {
12261226 * `i`, and the type of the `self` parameter is `selfType`.
12271227 *
12281228 * `strippedTypePath` points to the type `strippedType` inside `selfType`,
1229- * which is the (possibly complex-stripped) root type of `selfType`.
1229+ * which is the (possibly complex-stripped) root type of `selfType`. For example,
1230+ * if `m` has a `&self` parameter, then `strippedTypePath` is `TRefTypeParameter()`
1231+ * and `strippedType` is the type inside the reference.
12301232 */
12311233 pragma [ nomagic]
12321234 predicate methodInfo (
@@ -1252,11 +1254,12 @@ private module MethodCallResolution {
12521254 }
12531255
12541256 /**
1255- * Same as `methodInfo`, but allows for any `strippedType` when the
1256- * corresponding type inside `m` is a type parameter.
1257+ * Same as `methodInfo`, but restricted to non-blanket implementations, and
1258+ * allowing for any `strippedType` when the corresponding type inside `m` is
1259+ * a type parameter.
12571260 */
12581261 pragma [ inline]
1259- predicate methodInfoNonBlanketMatch (
1262+ predicate methodInfoNonBlanket (
12601263 Function m , string name , int arity , ImplOrTraitItemNode i , FunctionType selfType ,
12611264 TypePath strippedTypePath , Type strippedType
12621265 ) {
@@ -1268,11 +1271,17 @@ private module MethodCallResolution {
12681271 }
12691272
12701273 /**
1271- * Same as `methodInfo`, but allows for any `strippedType` when the
1272- * corresponding type inside `m` is a type parameter.
1274+ * Holds if method `m` with the name `name` and the arity `arity` exists in
1275+ * [blanket implementation][1] `i` and the type of the `self` parameter is
1276+ * `selfType`.
1277+ *
1278+ * `blanketPath` points to the type `blanketTypeParam` inside `selfType`, which
1279+ * is the type parameter used in the blanket implementation.
1280+ *
1281+ * [1]: https://doc.rust-lang.org/book/ch10-02-traits.html#using-trait-bounds-to-conditionally-implement-methods
12731282 */
12741283 pragma [ nomagic]
1275- predicate methodInfoBlanketMatch (
1284+ predicate methodInfoBlanket (
12761285 Function m , string name , int arity , ImplItemNode i , FunctionType selfType , TypePath blanketPath ,
12771286 TypeParam blanketTypeParam
12781287 ) {
@@ -1327,7 +1336,7 @@ private module MethodCallResolution {
13271336 ) {
13281337 exists ( string name , int arity |
13291338 mc .hasNameAndArity ( name , arity ) and
1330- methodInfoNonBlanketMatch ( m , name , arity , i , self , strippedTypePath , strippedType )
1339+ methodInfoNonBlanket ( m , name , arity , i , self , strippedTypePath , strippedType )
13311340 |
13321341 i =
13331342 any ( Impl impl |
@@ -1344,11 +1353,11 @@ private module MethodCallResolution {
13441353 }
13451354
13461355 /**
1347- * Holds if method call `mc` may target a method in `i` with `self` parameter having
1348- * type `selfType`.
1356+ * Holds if method call `mc` may target a method in blanket implementation `i`
1357+ * with `self` parameter having type `selfType`.
13491358 *
1350- * `strippedTypePath ` points to the type `strippedType ` inside `selfType`,
1351- * which is the (possibly complex-stripped) root type of `selfType` .
1359+ * `blanketPath ` points to the type `blanketTypeParam ` inside `selfType`, which
1360+ * is the type parameter used in the blanket implementation .
13521361 *
13531362 * This predicate only checks for matching method names and arities, and whether
13541363 * the trait being implemented by `i` (when `i` is not a trait itself) is visible
@@ -1362,7 +1371,7 @@ private module MethodCallResolution {
13621371 ) {
13631372 exists ( string name , int arity |
13641373 mc .hasNameAndArity ( name , arity ) and
1365- methodInfoBlanketMatch ( m , name , arity , i , self , blanketPath , blanketTypeParam )
1374+ methodInfoBlanket ( m , name , arity , i , self , blanketPath , blanketTypeParam )
13661375 |
13671376 methodCallVisibleImplTraitCandidate ( mc , i )
13681377 or
@@ -1450,6 +1459,7 @@ private module MethodCallResolution {
14501459 not derefChain .matches ( "%.ref" ) and // no need to try a borrow if the last thing we did was a deref
14511460 strippedType = this .getComplexstrippedType ( strippedTypePath , derefChainBorrow )
14521461 |
1462+ // todo: also check that all blanket implementation candidates are incompatible
14531463 forall ( ImplOrTraitItemNode i |
14541464 methodCallNonBlanketCandidate ( this , _, i , _, strippedTypePath , strippedType )
14551465 |
@@ -1469,6 +1479,7 @@ private module MethodCallResolution {
14691479 this .hasNoCompatibleTargetNoBorrow ( derefChain ) and
14701480 strippedType = this .getComplexstrippedType ( strippedTypePath , derefChainBorrow )
14711481 |
1482+ // todo: also check that all blanket implementation candidates are incompatible
14721483 forall ( ImplOrTraitItemNode i |
14731484 methodCallNonBlanketCandidate ( this , _, i , _, strippedTypePath , strippedType )
14741485 |
@@ -1516,7 +1527,8 @@ private module MethodCallResolution {
15161527 */
15171528 pragma [ nomagic]
15181529 Function resolveCallTarget ( string derefChainBorrow ) {
1519- exists ( MethodCallCand mcc | mcc = MkMethodCallCand ( this , derefChainBorrow ) |
1530+ exists ( MethodCallCand mcc |
1531+ mcc = MkMethodCallCand ( this , derefChainBorrow ) and
15201532 result = mcc .resolveCallTarget ( )
15211533 )
15221534 }
@@ -1610,7 +1622,7 @@ private module MethodCallResolution {
16101622 exists ( TypePath strippedTypePath , Type strippedType , string name , int arity |
16111623 this .hasInfo ( _, strippedTypePath , strippedType , name , arity ) and
16121624 forall ( Impl i |
1613- methodInfoNonBlanketMatch ( _, name , arity , i , _, strippedTypePath , strippedType ) and
1625+ methodInfoNonBlanket ( _, name , arity , i , _, strippedTypePath , strippedType ) and
16141626 not i .hasTrait ( )
16151627 |
16161628 this .hasIncompatibleInherentTarget ( i )
@@ -2413,12 +2425,12 @@ private module OperationResolution {
24132425 {
24142426 // todo
24152427 bindingset [ strippedTypePath]
2416- private predicate methodInfoNonBlanketMatch (
2428+ private predicate methodInfoNonBlanket (
24172429 TypeAbstraction abs , FunctionType constraint , Trait trait , string name , int arity ,
24182430 TypePath strippedTypePath , Type strippedType
24192431 ) {
2420- MethodCallResolution:: methodInfoNonBlanketMatch ( _, name , arity , abs , constraint ,
2421- strippedTypePath , strippedType ) and
2432+ MethodCallResolution:: methodInfoNonBlanket ( _, name , arity , abs , constraint , strippedTypePath ,
2433+ strippedType ) and
24222434 not abs .( ImplItemNode ) .isBlanketImplementation ( ) and
24232435 (
24242436 trait = abs .( ImplItemNode ) .resolveTraitTy ( )
@@ -2431,8 +2443,7 @@ private module OperationResolution {
24312443 predicate potentialInstantiationOf ( Op op , TypeAbstraction abs , FunctionType constraint ) {
24322444 exists ( Trait trait , string name , int arity , TypePath strippedTypePath , Type strippedType |
24332445 op .hasInfo ( strippedTypePath , strippedType , trait , name , arity ) and
2434- methodInfoNonBlanketMatch ( abs , constraint , trait , name , arity , strippedTypePath ,
2435- strippedType )
2446+ methodInfoNonBlanket ( abs , constraint , trait , name , arity , strippedTypePath , strippedType )
24362447 )
24372448 }
24382449
0 commit comments