@@ -1129,6 +1129,7 @@ private module MethodCallResolution {
1129
1129
* Holds if method `f` with the name `name` and the arity `arity` exists in
1130
1130
* `i`, and the type of the `self` parameter is `selfType`.
1131
1131
*
1132
+ * TODO
1132
1133
* `rootType` is the root type of `selfType`, and `selfRootPath` points to
1133
1134
* `selfRootType` inside `selfType`, where `selfRootType` is either the type
1134
1135
* being implemented, when `i` is an `impl`, or the trait itself when `i` is
@@ -1137,7 +1138,7 @@ private module MethodCallResolution {
1137
1138
pragma [ nomagic]
1138
1139
predicate methodInfo (
1139
1140
Function f , string name , int arity , ImplOrTraitItemNode i , FunctionType selfType ,
1140
- TypePath rootTypePath , Type rootType , TypePath selfRootPath , Type selfRootType
1141
+ TypePath rootTypePath , Type rootType
1141
1142
) {
1142
1143
exists ( FunctionTypePosition pos |
1143
1144
f = i .getASuccessor ( name ) and
@@ -1151,19 +1152,14 @@ private module MethodCallResolution {
1151
1152
) and
1152
1153
selfType .appliesTo ( f , pos , i ) and
1153
1154
pos .isSelf ( ) and
1154
- selfType .getTypeAt ( selfRootPath ) = selfRootType and
1155
1155
not i .( ImplItemNode ) .isBlanket ( )
1156
- |
1157
- selfRootType = i .( Impl ) .getSelfTy ( ) .( TypeMention ) .resolveType ( )
1158
- or
1159
- selfRootType = TTrait ( i )
1160
1156
)
1161
1157
}
1162
1158
1163
1159
pragma [ nomagic]
1164
1160
private predicate traitMethodInfo ( string name , int arity , Trait trait ) {
1165
1161
exists ( ImplItemNode i |
1166
- methodInfo ( _, name , arity , i , _, _, _, _ , _ ) and
1162
+ methodInfo ( _, name , arity , i , _, _, _) and
1167
1163
trait = i .resolveTraitTy ( )
1168
1164
)
1169
1165
}
@@ -1173,7 +1169,7 @@ private module MethodCallResolution {
1173
1169
exists ( string name , int arity | mc .( MethodCall ) .isMethodCall ( name , arity ) |
1174
1170
traitMethodInfo ( name , arity , trait )
1175
1171
or
1176
- methodInfo ( _, name , arity , trait , _, _, _, _ , _ )
1172
+ methodInfo ( _, name , arity , trait , _, _, _)
1177
1173
)
1178
1174
}
1179
1175
@@ -1191,6 +1187,8 @@ private module MethodCallResolution {
1191
1187
* Holds if method call `mc` may target a method in `i` with `self` parameter having
1192
1188
* type `selfType`.
1193
1189
*
1190
+ * todo
1191
+ *
1194
1192
* `rootType` is the root type of `selfType`, and `selfRootPath` points to
1195
1193
* `selfRootType` inside `selfType`, where `selfRootType` is either the type
1196
1194
* being implemented, when `i` is an `impl`, or the trait itself when `i` is
@@ -1202,12 +1200,11 @@ private module MethodCallResolution {
1202
1200
*/
1203
1201
pragma [ inline]
1204
1202
private predicate methodCallCandidate (
1205
- MethodCall mc , ImplOrTraitItemNode i , FunctionType self , TypePath rootTypePath , Type rootType ,
1206
- TypePath selfRootPath , Type selfRootType
1203
+ MethodCall mc , ImplOrTraitItemNode i , FunctionType self , TypePath rootTypePath , Type rootType
1207
1204
) {
1208
1205
exists ( string name , int arity |
1209
1206
mc .isMethodCall ( name , arity ) and
1210
- methodInfo ( _, name , arity , i , self , rootTypePath , rootType , selfRootPath , selfRootType )
1207
+ methodInfo ( _, name , arity , i , self , rootTypePath , rootType )
1211
1208
|
1212
1209
i =
1213
1210
any ( Impl impl |
@@ -1223,15 +1220,6 @@ private module MethodCallResolution {
1223
1220
)
1224
1221
}
1225
1222
1226
- private int countmethodCallCandidate ( MethodCall mc ) {
1227
- result = strictcount ( ImplOrTraitItemNode i | methodCallCandidate ( mc , i , _, _, _, _, _) )
1228
- }
1229
-
1230
- private predicate countmethodCallMaxCandidate ( MethodCall mc , ImplOrTraitItemNode i ) {
1231
- methodCallCandidate ( mc , i , _, _, _, _, _) and
1232
- countmethodCallCandidate ( mc ) = max ( countmethodCallCandidate ( _) )
1233
- }
1234
-
1235
1223
/**
1236
1224
* A method call.
1237
1225
*
@@ -1292,16 +1280,8 @@ private module MethodCallResolution {
1292
1280
*/
1293
1281
pragma [ nomagic]
1294
1282
private predicate isNotCandidate ( ImplOrTraitItemNode i , string derefChainBorrow ) {
1295
- IsInstantiationOf< MethodCallCand , FunctionType , MethodCallIsInstantiationOfInput > :: isNotInstantiationOf ( MkMethodCallCand ( this ,
1283
+ IsInstantiationOf< MethodCallCand , FunctionType , MethodCallReceiverIsInstantiationOfInput > :: isNotInstantiationOf ( MkMethodCallCand ( this ,
1296
1284
derefChainBorrow ) , i , _)
1297
- or
1298
- exists ( TypePath rootTypePath , Type rootType , TypePath selfRootPath , Type selfRootType |
1299
- rootType =
1300
- this .getACandidateReceiverTypeAtSubstituteTraitBounds ( rootTypePath , derefChainBorrow ) and
1301
- methodCallCandidate ( this , i , _, rootTypePath , rootType , selfRootPath , selfRootType ) and
1302
- selfRootType !=
1303
- this .getACandidateReceiverTypeAtSubstituteTraitBounds ( selfRootPath , derefChainBorrow )
1304
- )
1305
1285
}
1306
1286
1307
1287
/**
@@ -1322,18 +1302,12 @@ private module MethodCallResolution {
1322
1302
rootTypePath = TypePath:: singleton ( TRefTypeParameter ( ) )
1323
1303
)
1324
1304
|
1325
- forall ( ImplOrTraitItemNode i |
1326
- methodCallCandidate ( this , i , _, rootTypePath , rootType , _, _)
1327
- |
1305
+ forall ( ImplOrTraitItemNode i | methodCallCandidate ( this , i , _, rootTypePath , rootType ) |
1328
1306
this .isNotCandidate ( i , derefChainBorrow )
1329
1307
)
1330
1308
)
1331
1309
}
1332
1310
1333
- // pragma[nomagic]
1334
- // private predicate hasRefCandidate(ImplOrTraitItemNode i) {
1335
- // methodCallCandidate(this, i, _, TRefType(), _, _)
1336
- // }
1337
1311
/**
1338
1312
* Holds if the candidate receiver type represented by `derefChain;borrow` does not
1339
1313
* have a matching method target.
@@ -1347,9 +1321,7 @@ private module MethodCallResolution {
1347
1321
this .getACandidateReceiverTypeAtSubstituteTraitBounds ( rootTypePath , derefChainBorrow ) and
1348
1322
rootTypePath = TypePath:: singleton ( TRefTypeParameter ( ) )
1349
1323
|
1350
- forall ( ImplOrTraitItemNode i |
1351
- methodCallCandidate ( this , i , _, rootTypePath , rootType , _, _)
1352
- |
1324
+ forall ( ImplOrTraitItemNode i | methodCallCandidate ( this , i , _, rootTypePath , rootType ) |
1353
1325
this .isNotCandidate ( i , derefChainBorrow )
1354
1326
)
1355
1327
)
@@ -1396,12 +1368,6 @@ private module MethodCallResolution {
1396
1368
result = substituteTraitBounds ( this .getACandidateReceiverTypeAt ( path , derefChainBorrow ) )
1397
1369
}
1398
1370
1399
- pragma [ nomagic]
1400
- private Type getACandidateReceiverTypeAtSubstituteTraitBounds ( string derefChainBorrow ) {
1401
- result =
1402
- this .getACandidateReceiverTypeAtSubstituteTraitBounds ( TypePath:: nil ( ) , derefChainBorrow )
1403
- }
1404
-
1405
1371
/**
1406
1372
* Gets a method that this call resolves to after having applied a sequence of
1407
1373
* dereferences and possibly a borrow on the receiver type, encoded in the string
@@ -1485,7 +1451,7 @@ private module MethodCallResolution {
1485
1451
*/
1486
1452
pragma [ nomagic]
1487
1453
private predicate isNotInherentCandidate ( Impl impl ) {
1488
- IsInstantiationOf< MethodCallCand , FunctionType , MethodCallIsNotInstantiationOfInput > :: isNotInstantiationOf ( this ,
1454
+ IsInstantiationOf< MethodCallCand , FunctionType , MethodCallReceiverIsInstantiationOfInherentInput > :: isNotInstantiationOf ( this ,
1489
1455
impl , _)
1490
1456
}
1491
1457
@@ -1503,8 +1469,8 @@ private module MethodCallResolution {
1503
1469
or
1504
1470
rootTypePath = TypePath:: singleton ( TRefTypeParameter ( ) )
1505
1471
) and
1506
- forall ( Impl i , FunctionType self , TypePath selfRootPath , Type selfRootType |
1507
- methodInfo ( _, name , arity , i , self , rootTypePath , rootType , selfRootPath , selfRootType ) and
1472
+ forall ( Impl i |
1473
+ methodInfo ( _, name , arity , i , _ , rootTypePath , rootType ) and
1508
1474
not i .hasTrait ( )
1509
1475
|
1510
1476
this .isNotInherentCandidate ( i )
@@ -1515,7 +1481,7 @@ private module MethodCallResolution {
1515
1481
pragma [ nomagic]
1516
1482
private Function resolveCallTargetCand ( ImplOrTraitItemNode i ) {
1517
1483
exists ( string name |
1518
- IsInstantiationOf< MethodCallCand , FunctionType , MethodCallIsInstantiationOfInput > :: isInstantiationOf ( this ,
1484
+ IsInstantiationOf< MethodCallCand , FunctionType , MethodCallReceiverIsInstantiationOfInput > :: isInstantiationOf ( this ,
1519
1485
i , _) and
1520
1486
mc_ .isMethodCall ( name , _) and
1521
1487
result = getMethodSuccessor ( i , name , _) and
@@ -1570,44 +1536,41 @@ private module MethodCallResolution {
1570
1536
* A configuration for matching the type of a receiver against the type of
1571
1537
* a `self` parameter.
1572
1538
*/
1573
- private module MethodCallIsInstantiationOfInput implements
1539
+ private module MethodCallReceiverIsInstantiationOfInput implements
1574
1540
IsInstantiationOfInputSig< MethodCallCand , FunctionType >
1575
1541
{
1576
1542
pragma [ nomagic]
1577
1543
predicate potentialInstantiationOf (
1578
1544
MethodCallCand mcc , TypeAbstraction abs , FunctionType constraint
1579
1545
) {
1580
- exists ( MethodCall mc , string name , int arity , TypePath selfRootPath , Type selfRootType |
1581
- mcc .isMethodCall ( mc , selfRootPath , selfRootType , name , arity ) and
1582
- methodCallCandidate ( mc , abs , constraint , _ , _ , selfRootPath , selfRootType )
1546
+ exists ( MethodCall mc , string name , int arity , TypePath rootTypePath , Type rootType |
1547
+ mcc .isMethodCall ( mc , rootTypePath , rootType , name , arity ) and
1548
+ methodCallCandidate ( mc , abs , constraint , rootTypePath , rootType )
1583
1549
)
1584
1550
}
1585
1551
1586
1552
predicate relevantTypeMention ( FunctionType constraint ) {
1587
- methodInfo ( _, _, _, _, constraint , _, _, _ , _ )
1553
+ methodInfo ( _, _, _, _, constraint , _, _)
1588
1554
}
1589
1555
}
1590
1556
1591
1557
/**
1592
1558
* A configuration for anti-matching the type of a receiver against the type of
1593
1559
* a `self` parameter in an inherent method.
1594
1560
*/
1595
- private module MethodCallIsNotInstantiationOfInput implements
1561
+ private module MethodCallReceiverIsInstantiationOfInherentInput implements
1596
1562
IsInstantiationOfInputSig< MethodCallCand , FunctionType >
1597
1563
{
1598
1564
pragma [ nomagic]
1599
1565
predicate potentialInstantiationOf (
1600
1566
MethodCallCand mcc , TypeAbstraction abs , FunctionType constraint
1601
1567
) {
1602
- abs = any ( Impl i | not i .hasTrait ( ) ) and
1603
- exists ( MethodCall mc , string name , int arity , TypePath rootTypePath , Type rootType |
1604
- mcc .isMethodCall ( mc , rootTypePath , rootType , name , arity ) and
1605
- methodCallCandidate ( mc , abs , constraint , rootTypePath , rootType , _, _)
1606
- )
1568
+ MethodCallReceiverIsInstantiationOfInput:: potentialInstantiationOf ( mcc , abs , constraint ) and
1569
+ abs = any ( Impl i | not i .hasTrait ( ) )
1607
1570
}
1608
1571
1609
1572
predicate relevantTypeMention ( FunctionType constraint ) {
1610
- methodInfo ( _, _, _, _, constraint , _, _, _ , _ )
1573
+ methodInfo ( _, _, _, _, constraint , _, _)
1611
1574
}
1612
1575
}
1613
1576
}
@@ -1915,11 +1878,11 @@ private module FunctionCallResolution {
1915
1878
FunctionCall call , TraitItemNode trait , ImplOrTraitItemNode i , FunctionType self ,
1916
1879
Function resolved , Function f
1917
1880
) {
1918
- exists ( TypePath selfRootPath , Type selfRootType |
1881
+ exists ( TypePath rootTypePath , Type rootType |
1919
1882
f = call .getPathResolutionResolvedFunctionOrImplementation ( resolved ) and
1920
1883
trait = call .( Call ) .getTrait ( ) and
1921
- MethodCallResolution:: methodInfo ( f , _, _, i , self , _ , _ , selfRootPath , selfRootType ) and
1922
- call .getTypeAt ( selfRootPath ) = selfRootType
1884
+ MethodCallResolution:: methodInfo ( f , _, _, i , self , rootTypePath , rootType ) and
1885
+ call .getTypeAt ( rootTypePath ) = rootType
1923
1886
)
1924
1887
}
1925
1888
@@ -1931,7 +1894,7 @@ private module FunctionCallResolution {
1931
1894
}
1932
1895
1933
1896
predicate relevantTypeMention ( FunctionType constraint ) {
1934
- MethodCallResolution:: methodInfo ( _, _, _, _, constraint , _, _, _ , _ )
1897
+ MethodCallResolution:: methodInfo ( _, _, _, _, constraint , _, _)
1935
1898
}
1936
1899
}
1937
1900
}
@@ -2216,10 +2179,9 @@ private module OperationResolution {
2216
2179
pragma [ nomagic]
2217
2180
private predicate methodInfo (
2218
2181
TypeAbstraction abs , FunctionType constraint , Trait trait , string name , int arity ,
2219
- TypePath selfRootPath , Type selfRootType
2182
+ TypePath rootTypePath , Type rootType
2220
2183
) {
2221
- MethodCallResolution:: methodInfo ( _, name , arity , abs , constraint , _, _, selfRootPath ,
2222
- selfRootType ) and
2184
+ MethodCallResolution:: methodInfo ( _, name , arity , abs , constraint , rootTypePath , rootType ) and
2223
2185
(
2224
2186
trait = abs .( ImplItemNode ) .resolveTraitTy ( )
2225
2187
or
@@ -2229,14 +2191,14 @@ private module OperationResolution {
2229
2191
2230
2192
pragma [ nomagic]
2231
2193
predicate potentialInstantiationOf ( Op op , TypeAbstraction abs , FunctionType constraint ) {
2232
- exists ( Trait trait , string name , int arity , TypePath selfRootPath , Type selfRootType |
2233
- op .isOperation ( selfRootPath , selfRootType , trait , name , arity ) and
2234
- methodInfo ( abs , constraint , trait , name , arity , selfRootPath , selfRootType )
2194
+ exists ( Trait trait , string name , int arity , TypePath rootTypePath , Type rootType |
2195
+ op .isOperation ( rootTypePath , rootType , trait , name , arity ) and
2196
+ methodInfo ( abs , constraint , trait , name , arity , rootTypePath , rootType )
2235
2197
)
2236
2198
}
2237
2199
2238
2200
predicate relevantTypeMention ( FunctionType constraint ) {
2239
- MethodCallResolution:: methodInfo ( _, _, _, _, constraint , _, _, _ , _ )
2201
+ MethodCallResolution:: methodInfo ( _, _, _, _, constraint , _, _)
2240
2202
}
2241
2203
}
2242
2204
}
0 commit comments