@@ -859,14 +859,14 @@ private predicate assocFunctionInfo(
859
859
860
860
/**
861
861
* Holds if function `f` with the name `name` and the arity `arity` exists in
862
- * blanket implementation `impl` of `trait`, and the type at position
862
+ * blanket (like) implementation `impl` of `trait`, and the type at position
863
863
* `pos` is `t`.
864
864
*
865
865
* `blanketPath` points to the type `blanketTypeParam` inside `t`, which
866
866
* is the type parameter used in the blanket implementation.
867
867
*/
868
868
pragma [ nomagic]
869
- private predicate functionInfoBlanket (
869
+ private predicate functionInfoBlanketLike (
870
870
Function f , string name , int arity , ImplItemNode impl , Trait trait , FunctionTypePosition pos ,
871
871
AssocFunctionType t , TypePath blanketPath , TypeParam blanketTypeParam
872
872
) {
@@ -985,19 +985,20 @@ private module MethodResolution {
985
985
986
986
/**
987
987
* Holds if method `m` with the name `name` and the arity `arity` exists in
988
- * blanket implementation `impl` of `trait`, and the type of the `self`
988
+ * blanket (like) implementation `impl` of `trait`, and the type of the `self`
989
989
* parameter is `selfType`.
990
990
*
991
991
* `blanketPath` points to the type `blanketTypeParam` inside `selfType`, which
992
992
* is the type parameter used in the blanket implementation.
993
993
*/
994
994
pragma [ nomagic]
995
- private predicate methodInfoBlanket (
995
+ private predicate methodInfoBlanketLike (
996
996
Method m , string name , int arity , ImplItemNode impl , Trait trait , AssocFunctionType selfType ,
997
997
TypePath blanketPath , TypeParam blanketTypeParam
998
998
) {
999
999
exists ( FunctionTypePosition pos |
1000
- functionInfoBlanket ( m , name , arity , impl , trait , pos , selfType , blanketPath , blanketTypeParam ) and
1000
+ functionInfoBlanketLike ( m , name , arity , impl , trait , pos , selfType , blanketPath ,
1001
+ blanketTypeParam ) and
1001
1002
pos .isSelf ( )
1002
1003
)
1003
1004
}
@@ -1071,8 +1072,8 @@ private module MethodResolution {
1071
1072
}
1072
1073
1073
1074
/**
1074
- * Holds if method call `mc` may target a method in blanket implementation `i`
1075
- * with `self` parameter having type `selfType`.
1075
+ * Holds if method call `mc` may target a method in blanket (like) implementation
1076
+ * `impl` with `self` parameter having type `selfType`.
1076
1077
*
1077
1078
* `blanketPath` points to the type `blanketTypeParam` inside `selfType`, which
1078
1079
* is the type parameter used in the blanket implementation.
@@ -1083,13 +1084,13 @@ private module MethodResolution {
1083
1084
*/
1084
1085
bindingset [ mc]
1085
1086
pragma [ inline_late]
1086
- private predicate methodCallBlanketCandidate (
1087
+ private predicate methodCallBlanketLikeCandidate (
1087
1088
MethodCall mc , Method m , ImplItemNode impl , AssocFunctionType self , TypePath blanketPath ,
1088
1089
TypeParam blanketTypeParam
1089
1090
) {
1090
1091
exists ( string name , int arity |
1091
1092
mc .hasNameAndArity ( name , arity ) and
1092
- methodInfoBlanket ( m , name , arity , impl , _, self , blanketPath , blanketTypeParam )
1093
+ methodInfoBlanketLike ( m , name , arity , impl , _, self , blanketPath , blanketTypeParam )
1093
1094
|
1094
1095
methodCallVisibleImplTraitCandidate ( mc , impl )
1095
1096
or
@@ -1145,7 +1146,7 @@ private module MethodResolution {
1145
1146
or
1146
1147
this .supportsAutoDerefAndBorrow ( ) and
1147
1148
exists ( TypePath path0 , Type t0 , string derefChain0 |
1148
- this .hasNoCompatibleTarget ( derefChain0 , _) and
1149
+ this .hasNoCompatibleTargetBorrow ( derefChain0 , _) and
1149
1150
t0 = this .getACandidateReceiverTypeAtNoBorrow ( path0 , derefChain0 )
1150
1151
|
1151
1152
path0 .isCons ( TRefTypeParameter ( ) , path ) and
@@ -1174,6 +1175,21 @@ private module MethodResolution {
1174
1175
derefChainBorrow = ";"
1175
1176
}
1176
1177
1178
+ /**
1179
+ * Holds if the method inside blanket-like implementation `i` with matching name
1180
+ * and arity can be ruled out as a target of this call, either because the candidate
1181
+ * receiver type represented by `derefChainBorrow` is incompatible with the `self`
1182
+ * parameter type, or because the blanket constraint is not satisfied.
1183
+ */
1184
+ pragma [ nomagic]
1185
+ private predicate hasIncompatibleBlanketLikeTarget ( ImplItemNode i , string derefChainBorrow ) {
1186
+ ReceiverIsNotInstantiationOfBlanketLikeSelfParam:: argIsNotInstantiationOf ( MkMethodCallCand ( this ,
1187
+ derefChainBorrow ) , i , _)
1188
+ or
1189
+ ReceiverSatisfiesBlanketLikeConstraint:: satisfiesNotBlanketConstraint ( MkMethodCallCand ( this ,
1190
+ derefChainBorrow ) , i )
1191
+ }
1192
+
1177
1193
/**
1178
1194
* Same as `getACandidateReceiverTypeAt`, but with traits substituted in for types
1179
1195
* with trait bounds.
@@ -1191,10 +1207,9 @@ private module MethodResolution {
1191
1207
}
1192
1208
1193
1209
bindingset [ strippedTypePath, strippedType, derefChainBorrow]
1194
- private predicate hasNoCompatibleTargetCheck (
1210
+ private predicate hasNoCompatibleNonBlanketLikeTargetCheck (
1195
1211
TypePath strippedTypePath , Type strippedType , string derefChainBorrow
1196
1212
) {
1197
- // todo: also check that all blanket implementation candidates are incompatible
1198
1213
forall ( ImplOrTraitItemNode i |
1199
1214
methodCallNonBlanketCandidate ( this , _, i , _, strippedTypePath , strippedType )
1200
1215
or
@@ -1204,6 +1219,28 @@ private module MethodResolution {
1204
1219
)
1205
1220
}
1206
1221
1222
+ bindingset [ strippedTypePath, strippedType, derefChainBorrow]
1223
+ private predicate hasNoCompatibleTargetCheck (
1224
+ TypePath strippedTypePath , Type strippedType , string derefChainBorrow
1225
+ ) {
1226
+ this .hasNoCompatibleNonBlanketLikeTargetCheck ( strippedTypePath , strippedType , derefChainBorrow ) and
1227
+ forall ( ImplItemNode i | methodCallBlanketLikeCandidate ( this , _, i , _, _, _) |
1228
+ this .hasIncompatibleBlanketLikeTarget ( i , derefChainBorrow )
1229
+ )
1230
+ }
1231
+
1232
+ bindingset [ strippedTypePath, strippedType, derefChainBorrow]
1233
+ private predicate hasNoCompatibleNonBlanketTargetCheck (
1234
+ TypePath strippedTypePath , Type strippedType , string derefChainBorrow
1235
+ ) {
1236
+ this .hasNoCompatibleNonBlanketLikeTargetCheck ( strippedTypePath , strippedType , derefChainBorrow ) and
1237
+ forall ( ImplItemNode i |
1238
+ methodCallBlanketLikeCandidate ( this , _, i , _, _, _) and not i .isBlanketImplementation ( )
1239
+ |
1240
+ this .hasIncompatibleBlanketLikeTarget ( i , derefChainBorrow )
1241
+ )
1242
+ }
1243
+
1207
1244
/**
1208
1245
* Holds if the candidate receiver type represented by
1209
1246
* `derefChainBorrow = derefChain;` does not have a matching method target.
@@ -1214,7 +1251,7 @@ private module MethodResolution {
1214
1251
this .supportsAutoDerefAndBorrow ( )
1215
1252
or
1216
1253
// needed for the `hasNoCompatibleTarget` check in
1217
- // `SatisfiesBlanketConstraintInput ::hasBlanketCandidate`
1254
+ // `ReceiverSatisfiesBlanketLikeConstraintInput ::hasBlanketCandidate`
1218
1255
derefChain = ""
1219
1256
) and
1220
1257
exists ( TypePath strippedTypePath , Type strippedType |
@@ -1225,13 +1262,35 @@ private module MethodResolution {
1225
1262
)
1226
1263
}
1227
1264
1265
+ /**
1266
+ * Holds if the candidate receiver type represented by
1267
+ * `derefChainBorrow = derefChain;` does not have a matching non-blanket
1268
+ * method target.
1269
+ */
1270
+ pragma [ nomagic]
1271
+ predicate hasNoCompatibleNonBlanketTargetNoBorrow ( string derefChain , string derefChainBorrow ) {
1272
+ (
1273
+ this .supportsAutoDerefAndBorrow ( )
1274
+ or
1275
+ // needed for the `hasNoCompatibleTarget` check in
1276
+ // `ReceiverSatisfiesBlanketLikeConstraintInput::hasBlanketCandidate`
1277
+ derefChain = ""
1278
+ ) and
1279
+ exists ( TypePath strippedTypePath , Type strippedType |
1280
+ derefChainBorrow = derefChain + ";" and
1281
+ not derefChain .matches ( "%.ref" ) and // no need to try a borrow if the last thing we did was a deref
1282
+ strippedType = this .getComplexStrippedType ( strippedTypePath , derefChainBorrow ) and
1283
+ this .hasNoCompatibleNonBlanketTargetCheck ( strippedTypePath , strippedType , derefChainBorrow )
1284
+ )
1285
+ }
1286
+
1228
1287
/**
1229
1288
* Holds if the candidate receiver type represented by
1230
1289
* `derefChainBorrow = derefChain;borrow` does not have a matching method
1231
1290
* target.
1232
1291
*/
1233
1292
pragma [ nomagic]
1234
- predicate hasNoCompatibleTarget ( string derefChain , string derefChainBorrow ) {
1293
+ predicate hasNoCompatibleTargetBorrow ( string derefChain , string derefChainBorrow ) {
1235
1294
exists ( TypePath strippedTypePath , Type strippedType |
1236
1295
derefChainBorrow = derefChain + ";borrow" and
1237
1296
this .hasNoCompatibleTargetNoBorrow ( derefChain , _) and
@@ -1240,6 +1299,21 @@ private module MethodResolution {
1240
1299
)
1241
1300
}
1242
1301
1302
+ /**
1303
+ * Holds if the candidate receiver type represented by
1304
+ * `derefChainBorrow = derefChain;borrow` does not have a matching non-blanket
1305
+ * method target.
1306
+ */
1307
+ pragma [ nomagic]
1308
+ predicate hasNoCompatibleNonBlanketTargetBorrow ( string derefChain , string derefChainBorrow ) {
1309
+ exists ( TypePath strippedTypePath , Type strippedType |
1310
+ derefChainBorrow = derefChain + ";borrow" and
1311
+ this .hasNoCompatibleTargetNoBorrow ( derefChain , _) and
1312
+ strippedType = this .getComplexStrippedType ( strippedTypePath , derefChainBorrow ) and
1313
+ this .hasNoCompatibleNonBlanketTargetCheck ( strippedTypePath , strippedType , derefChainBorrow )
1314
+ )
1315
+ }
1316
+
1243
1317
/**
1244
1318
* Gets a [candidate receiver type][1] of this method call at `path`.
1245
1319
*
@@ -1432,10 +1506,10 @@ private module MethodResolution {
1432
1506
}
1433
1507
1434
1508
pragma [ nomagic]
1435
- predicate hasNoCompatibleTarget ( ) {
1436
- mc_ .hasNoCompatibleTarget ( _, derefChainBorrow )
1509
+ predicate hasNoCompatibleNonBlanketTarget ( ) {
1510
+ mc_ .hasNoCompatibleNonBlanketTargetBorrow ( _, derefChainBorrow )
1437
1511
or
1438
- mc_ .hasNoCompatibleTargetNoBorrow ( _, derefChainBorrow )
1512
+ mc_ .hasNoCompatibleNonBlanketTargetNoBorrow ( _, derefChainBorrow )
1439
1513
}
1440
1514
1441
1515
pragma [ nomagic]
@@ -1518,20 +1592,20 @@ private module MethodResolution {
1518
1592
Location getLocation ( ) { result = mc_ .getLocation ( ) }
1519
1593
}
1520
1594
1521
- private module ReceiverSatisfiesBlanketConstraintInput implements
1595
+ private module ReceiverSatisfiesBlanketLikeConstraintInput implements
1522
1596
BlanketImplementation:: SatisfiesBlanketConstraintInputSig< MethodCallCand >
1523
1597
{
1524
1598
pragma [ nomagic]
1525
1599
predicate hasBlanketCandidate (
1526
1600
MethodCallCand mcc , ImplItemNode impl , TypePath blanketPath , TypeParam blanketTypeParam
1527
1601
) {
1528
- exists ( MethodCall mc , string name , int arity |
1529
- mcc . hasSignature ( mc , _ , _ , name , arity ) and
1530
- methodCallBlanketCandidate ( mc , _, impl , _, blanketPath , blanketTypeParam ) and
1602
+ exists ( MethodCall mc |
1603
+ mc = mcc . getMethodCall ( ) and
1604
+ methodCallBlanketLikeCandidate ( mc , _, impl , _, blanketPath , blanketTypeParam ) and
1531
1605
// Only apply blanket implementations when no other implementations are possible;
1532
1606
// this is to account for codebases that use the (unstable) specialization feature
1533
1607
// (https://rust-lang.github.io/rfcs/1210-impl-specialization.html)
1534
- mcc .hasNoCompatibleTarget ( )
1608
+ ( mcc .hasNoCompatibleNonBlanketTarget ( ) or not impl . isBlanketImplementation ( ) )
1535
1609
|
1536
1610
mcc .hasNoBorrow ( )
1537
1611
or
@@ -1540,9 +1614,9 @@ private module MethodResolution {
1540
1614
}
1541
1615
}
1542
1616
1543
- private module ReceiverSatisfiesBlanketConstraint =
1617
+ private module ReceiverSatisfiesBlanketLikeConstraint =
1544
1618
BlanketImplementation:: SatisfiesBlanketConstraint< MethodCallCand ,
1545
- ReceiverSatisfiesBlanketConstraintInput > ;
1619
+ ReceiverSatisfiesBlanketLikeConstraintInput > ;
1546
1620
1547
1621
/**
1548
1622
* A configuration for matching the type of a receiver against the type of
@@ -1563,8 +1637,8 @@ private module MethodResolution {
1563
1637
|
1564
1638
methodCallNonBlanketCandidate ( mc , m , i , selfType , strippedTypePath , strippedType )
1565
1639
or
1566
- methodCallBlanketCandidate ( mc , m , i , selfType , _, _) and
1567
- ReceiverSatisfiesBlanketConstraint :: satisfiesBlanketConstraint ( mcc , i )
1640
+ methodCallBlanketLikeCandidate ( mc , m , i , selfType , _, _) and
1641
+ ReceiverSatisfiesBlanketLikeConstraint :: satisfiesBlanketConstraint ( mcc , i )
1568
1642
)
1569
1643
}
1570
1644
@@ -1589,6 +1663,30 @@ private module MethodResolution {
1589
1663
private module ReceiverIsInstantiationOfSelfParam =
1590
1664
ArgIsInstantiationOf< MethodCallCand , ReceiverIsInstantiationOfSelfParamInput > ;
1591
1665
1666
+ /**
1667
+ * A configuration for anti-matching the type of a receiver against the type of
1668
+ * a `self` parameter belonging to a blanket (like) implementation.
1669
+ */
1670
+ private module ReceiverIsNotInstantiationOfBlanketLikeSelfParamInput implements
1671
+ IsInstantiationOfInputSig< MethodCallCand , AssocFunctionType >
1672
+ {
1673
+ pragma [ nomagic]
1674
+ predicate potentialInstantiationOf (
1675
+ MethodCallCand mcc , TypeAbstraction abs , AssocFunctionType constraint
1676
+ ) {
1677
+ methodCallBlanketLikeCandidate ( mcc .getMethodCall ( ) , _, abs , constraint , _, _) and
1678
+ if abs .( Impl ) .hasTrait ( )
1679
+ then
1680
+ // inherent methods take precedence over trait methods, so only allow
1681
+ // trait methods when there are no matching inherent methods
1682
+ mcc .hasNoInherentTarget ( )
1683
+ else any ( )
1684
+ }
1685
+ }
1686
+
1687
+ private module ReceiverIsNotInstantiationOfBlanketLikeSelfParam =
1688
+ ArgIsInstantiationOf< MethodCallCand , ReceiverIsNotInstantiationOfBlanketLikeSelfParamInput > ;
1689
+
1592
1690
/**
1593
1691
* A configuration for matching the type qualifier of a method call
1594
1692
* against the type being implemented in an `impl` block. For example,
@@ -1642,10 +1740,6 @@ private module MethodResolution {
1642
1740
ReceiverIsInstantiationOfSelfParamInput:: potentialInstantiationOf0 ( mcc , abs , constraint ) and
1643
1741
abs = any ( Impl i | not i .hasTrait ( ) )
1644
1742
}
1645
-
1646
- predicate relevantConstraint ( AssocFunctionType constraint ) {
1647
- methodInfo ( _, _, _, _, constraint , _, _)
1648
- }
1649
1743
}
1650
1744
1651
1745
private module ReceiverIsNotInstantiationOfInherentSelfParam =
@@ -1901,18 +1995,18 @@ private module NonMethodResolution {
1901
1995
}
1902
1996
1903
1997
pragma [ nomagic]
1904
- private predicate functionInfoBlanketRelevantPos (
1998
+ private predicate functionInfoBlanketLikeRelevantPos (
1905
1999
NonMethodFunction f , string name , int arity , ImplItemNode impl , Trait trait ,
1906
2000
FunctionTypePosition pos , AssocFunctionType t , TypePath blanketPath , TypeParam blanketTypeParam
1907
2001
) {
1908
- functionInfoBlanket ( f , name , arity , impl , trait , pos , t , blanketPath , blanketTypeParam ) and
2002
+ functionInfoBlanketLike ( f , name , arity , impl , trait , pos , t , blanketPath , blanketTypeParam ) and
1909
2003
(
1910
2004
not pos .isReturn ( )
1911
2005
or
1912
2006
// We only check that the context of the call provides relevant type information
1913
2007
// when no argument can
1914
2008
not exists ( FunctionTypePosition pos0 |
1915
- functionInfoBlanket ( f , name , arity , impl , trait , pos0 , _, _, _) and
2009
+ functionInfoBlanketLike ( f , name , arity , impl , trait , pos0 , _, _, _) and
1916
2010
not pos0 .isReturn ( )
1917
2011
)
1918
2012
)
@@ -1922,7 +2016,7 @@ private module NonMethodResolution {
1922
2016
private predicate blanketCallTraitCandidate ( Element fc , Trait trait ) {
1923
2017
exists ( string name , int arity |
1924
2018
fc .( NonMethodCall ) .hasNameAndArity ( name , arity ) and
1925
- functionInfoBlanketRelevantPos ( _, name , arity , _, trait , _, _, _, _)
2019
+ functionInfoBlanketLikeRelevantPos ( _, name , arity , _, trait , _, _, _, _)
1926
2020
|
1927
2021
not fc .( Call ) .hasTrait ( )
1928
2022
or
@@ -1998,7 +2092,7 @@ private module NonMethodResolution {
1998
2092
exists ( string name , int arity , Trait trait , AssocFunctionType t |
1999
2093
this .hasNameAndArity ( name , arity ) and
2000
2094
exists ( this .getTypeAt ( pos , blanketPath ) ) and
2001
- functionInfoBlanketRelevantPos ( _, name , arity , impl , trait , pos , t , blanketPath ,
2095
+ functionInfoBlanketLikeRelevantPos ( _, name , arity , impl , trait , pos , t , blanketPath ,
2002
2096
blanketTypeParam ) and
2003
2097
BlanketTraitIsVisible:: traitIsVisible ( this , trait )
2004
2098
)
@@ -2084,12 +2178,12 @@ private module NonMethodResolution {
2084
2178
exists ( FunctionTypePosition pos |
2085
2179
ArgSatisfiesBlanketConstraint:: satisfiesBlanketConstraint ( fcp , abs ) and
2086
2180
fcp = MkCallAndBlanketPos ( _, pos ) and
2087
- functionInfoBlanketRelevantPos ( _, _, _, abs , _, pos , constraint , _, _)
2181
+ functionInfoBlanketLikeRelevantPos ( _, _, _, abs , _, pos , constraint , _, _)
2088
2182
)
2089
2183
}
2090
2184
2091
2185
predicate relevantConstraint ( AssocFunctionType constraint ) {
2092
- functionInfoBlanketRelevantPos ( _, _, _, _, _, _, constraint , _, _)
2186
+ functionInfoBlanketLikeRelevantPos ( _, _, _, _, _, _, constraint , _, _)
2093
2187
}
2094
2188
}
2095
2189
0 commit comments