@@ -1129,6 +1129,7 @@ private module MethodCallResolution {
11291129 * Holds if method `f` with the name `name` and the arity `arity` exists in
11301130 * `i`, and the type of the `self` parameter is `selfType`.
11311131 *
1132+ * TODO
11321133 * `rootType` is the root type of `selfType`, and `selfRootPath` points to
11331134 * `selfRootType` inside `selfType`, where `selfRootType` is either the type
11341135 * being implemented, when `i` is an `impl`, or the trait itself when `i` is
@@ -1137,7 +1138,7 @@ private module MethodCallResolution {
11371138 pragma [ nomagic]
11381139 predicate methodInfo (
11391140 Function f , string name , int arity , ImplOrTraitItemNode i , FunctionType selfType ,
1140- TypePath rootTypePath , Type rootType , TypePath selfRootPath , Type selfRootType
1141+ TypePath rootTypePath , Type rootType
11411142 ) {
11421143 exists ( FunctionTypePosition pos |
11431144 f = i .getASuccessor ( name ) and
@@ -1151,19 +1152,14 @@ private module MethodCallResolution {
11511152 ) and
11521153 selfType .appliesTo ( f , pos , i ) and
11531154 pos .isSelf ( ) and
1154- selfType .getTypeAt ( selfRootPath ) = selfRootType and
11551155 not i .( ImplItemNode ) .isBlanket ( )
1156- |
1157- selfRootType = i .( Impl ) .getSelfTy ( ) .( TypeMention ) .resolveType ( )
1158- or
1159- selfRootType = TTrait ( i )
11601156 )
11611157 }
11621158
11631159 pragma [ nomagic]
11641160 private predicate traitMethodInfo ( string name , int arity , Trait trait ) {
11651161 exists ( ImplItemNode i |
1166- methodInfo ( _, name , arity , i , _, _, _, _ , _ ) and
1162+ methodInfo ( _, name , arity , i , _, _, _) and
11671163 trait = i .resolveTraitTy ( )
11681164 )
11691165 }
@@ -1173,7 +1169,7 @@ private module MethodCallResolution {
11731169 exists ( string name , int arity | mc .( MethodCall ) .isMethodCall ( name , arity ) |
11741170 traitMethodInfo ( name , arity , trait )
11751171 or
1176- methodInfo ( _, name , arity , trait , _, _, _, _ , _ )
1172+ methodInfo ( _, name , arity , trait , _, _, _)
11771173 )
11781174 }
11791175
@@ -1191,6 +1187,8 @@ private module MethodCallResolution {
11911187 * Holds if method call `mc` may target a method in `i` with `self` parameter having
11921188 * type `selfType`.
11931189 *
1190+ * todo
1191+ *
11941192 * `rootType` is the root type of `selfType`, and `selfRootPath` points to
11951193 * `selfRootType` inside `selfType`, where `selfRootType` is either the type
11961194 * being implemented, when `i` is an `impl`, or the trait itself when `i` is
@@ -1202,12 +1200,11 @@ private module MethodCallResolution {
12021200 */
12031201 pragma [ inline]
12041202 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
12071204 ) {
12081205 exists ( string name , int arity |
12091206 mc .isMethodCall ( name , arity ) and
1210- methodInfo ( _, name , arity , i , self , rootTypePath , rootType , selfRootPath , selfRootType )
1207+ methodInfo ( _, name , arity , i , self , rootTypePath , rootType )
12111208 |
12121209 i =
12131210 any ( Impl impl |
@@ -1223,15 +1220,6 @@ private module MethodCallResolution {
12231220 )
12241221 }
12251222
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-
12351223 /**
12361224 * A method call.
12371225 *
@@ -1292,16 +1280,8 @@ private module MethodCallResolution {
12921280 */
12931281 pragma [ nomagic]
12941282 private predicate isNotCandidate ( ImplOrTraitItemNode i , string derefChainBorrow ) {
1295- IsInstantiationOf< MethodCallCand , FunctionType , MethodCallIsInstantiationOfInput > :: isNotInstantiationOf ( MkMethodCallCand ( this ,
1283+ IsInstantiationOf< MethodCallCand , FunctionType , MethodCallReceiverIsInstantiationOfInput > :: isNotInstantiationOf ( MkMethodCallCand ( this ,
12961284 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- )
13051285 }
13061286
13071287 /**
@@ -1322,18 +1302,12 @@ private module MethodCallResolution {
13221302 rootTypePath = TypePath:: singleton ( TRefTypeParameter ( ) )
13231303 )
13241304 |
1325- forall ( ImplOrTraitItemNode i |
1326- methodCallCandidate ( this , i , _, rootTypePath , rootType , _, _)
1327- |
1305+ forall ( ImplOrTraitItemNode i | methodCallCandidate ( this , i , _, rootTypePath , rootType ) |
13281306 this .isNotCandidate ( i , derefChainBorrow )
13291307 )
13301308 )
13311309 }
13321310
1333- // pragma[nomagic]
1334- // private predicate hasRefCandidate(ImplOrTraitItemNode i) {
1335- // methodCallCandidate(this, i, _, TRefType(), _, _)
1336- // }
13371311 /**
13381312 * Holds if the candidate receiver type represented by `derefChain;borrow` does not
13391313 * have a matching method target.
@@ -1347,9 +1321,7 @@ private module MethodCallResolution {
13471321 this .getACandidateReceiverTypeAtSubstituteTraitBounds ( rootTypePath , derefChainBorrow ) and
13481322 rootTypePath = TypePath:: singleton ( TRefTypeParameter ( ) )
13491323 |
1350- forall ( ImplOrTraitItemNode i |
1351- methodCallCandidate ( this , i , _, rootTypePath , rootType , _, _)
1352- |
1324+ forall ( ImplOrTraitItemNode i | methodCallCandidate ( this , i , _, rootTypePath , rootType ) |
13531325 this .isNotCandidate ( i , derefChainBorrow )
13541326 )
13551327 )
@@ -1396,12 +1368,6 @@ private module MethodCallResolution {
13961368 result = substituteTraitBounds ( this .getACandidateReceiverTypeAt ( path , derefChainBorrow ) )
13971369 }
13981370
1399- pragma [ nomagic]
1400- private Type getACandidateReceiverTypeAtSubstituteTraitBounds ( string derefChainBorrow ) {
1401- result =
1402- this .getACandidateReceiverTypeAtSubstituteTraitBounds ( TypePath:: nil ( ) , derefChainBorrow )
1403- }
1404-
14051371 /**
14061372 * Gets a method that this call resolves to after having applied a sequence of
14071373 * dereferences and possibly a borrow on the receiver type, encoded in the string
@@ -1485,7 +1451,7 @@ private module MethodCallResolution {
14851451 */
14861452 pragma [ nomagic]
14871453 private predicate isNotInherentCandidate ( Impl impl ) {
1488- IsInstantiationOf< MethodCallCand , FunctionType , MethodCallIsNotInstantiationOfInput > :: isNotInstantiationOf ( this ,
1454+ IsInstantiationOf< MethodCallCand , FunctionType , MethodCallReceiverIsInstantiationOfInherentInput > :: isNotInstantiationOf ( this ,
14891455 impl , _)
14901456 }
14911457
@@ -1503,8 +1469,8 @@ private module MethodCallResolution {
15031469 or
15041470 rootTypePath = TypePath:: singleton ( TRefTypeParameter ( ) )
15051471 ) 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
15081474 not i .hasTrait ( )
15091475 |
15101476 this .isNotInherentCandidate ( i )
@@ -1515,7 +1481,7 @@ private module MethodCallResolution {
15151481 pragma [ nomagic]
15161482 private Function resolveCallTargetCand ( ImplOrTraitItemNode i ) {
15171483 exists ( string name |
1518- IsInstantiationOf< MethodCallCand , FunctionType , MethodCallIsInstantiationOfInput > :: isInstantiationOf ( this ,
1484+ IsInstantiationOf< MethodCallCand , FunctionType , MethodCallReceiverIsInstantiationOfInput > :: isInstantiationOf ( this ,
15191485 i , _) and
15201486 mc_ .isMethodCall ( name , _) and
15211487 result = getMethodSuccessor ( i , name , _) and
@@ -1570,44 +1536,41 @@ private module MethodCallResolution {
15701536 * A configuration for matching the type of a receiver against the type of
15711537 * a `self` parameter.
15721538 */
1573- private module MethodCallIsInstantiationOfInput implements
1539+ private module MethodCallReceiverIsInstantiationOfInput implements
15741540 IsInstantiationOfInputSig< MethodCallCand , FunctionType >
15751541 {
15761542 pragma [ nomagic]
15771543 predicate potentialInstantiationOf (
15781544 MethodCallCand mcc , TypeAbstraction abs , FunctionType constraint
15791545 ) {
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 )
15831549 )
15841550 }
15851551
15861552 predicate relevantTypeMention ( FunctionType constraint ) {
1587- methodInfo ( _, _, _, _, constraint , _, _, _ , _ )
1553+ methodInfo ( _, _, _, _, constraint , _, _)
15881554 }
15891555 }
15901556
15911557 /**
15921558 * A configuration for anti-matching the type of a receiver against the type of
15931559 * a `self` parameter in an inherent method.
15941560 */
1595- private module MethodCallIsNotInstantiationOfInput implements
1561+ private module MethodCallReceiverIsInstantiationOfInherentInput implements
15961562 IsInstantiationOfInputSig< MethodCallCand , FunctionType >
15971563 {
15981564 pragma [ nomagic]
15991565 predicate potentialInstantiationOf (
16001566 MethodCallCand mcc , TypeAbstraction abs , FunctionType constraint
16011567 ) {
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 ( ) )
16071570 }
16081571
16091572 predicate relevantTypeMention ( FunctionType constraint ) {
1610- methodInfo ( _, _, _, _, constraint , _, _, _ , _ )
1573+ methodInfo ( _, _, _, _, constraint , _, _)
16111574 }
16121575 }
16131576}
@@ -1915,11 +1878,11 @@ private module FunctionCallResolution {
19151878 FunctionCall call , TraitItemNode trait , ImplOrTraitItemNode i , FunctionType self ,
19161879 Function resolved , Function f
19171880 ) {
1918- exists ( TypePath selfRootPath , Type selfRootType |
1881+ exists ( TypePath rootTypePath , Type rootType |
19191882 f = call .getPathResolutionResolvedFunctionOrImplementation ( resolved ) and
19201883 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
19231886 )
19241887 }
19251888
@@ -1931,7 +1894,7 @@ private module FunctionCallResolution {
19311894 }
19321895
19331896 predicate relevantTypeMention ( FunctionType constraint ) {
1934- MethodCallResolution:: methodInfo ( _, _, _, _, constraint , _, _, _ , _ )
1897+ MethodCallResolution:: methodInfo ( _, _, _, _, constraint , _, _)
19351898 }
19361899 }
19371900}
@@ -2216,10 +2179,9 @@ private module OperationResolution {
22162179 pragma [ nomagic]
22172180 private predicate methodInfo (
22182181 TypeAbstraction abs , FunctionType constraint , Trait trait , string name , int arity ,
2219- TypePath selfRootPath , Type selfRootType
2182+ TypePath rootTypePath , Type rootType
22202183 ) {
2221- MethodCallResolution:: methodInfo ( _, name , arity , abs , constraint , _, _, selfRootPath ,
2222- selfRootType ) and
2184+ MethodCallResolution:: methodInfo ( _, name , arity , abs , constraint , rootTypePath , rootType ) and
22232185 (
22242186 trait = abs .( ImplItemNode ) .resolveTraitTy ( )
22252187 or
@@ -2229,14 +2191,14 @@ private module OperationResolution {
22292191
22302192 pragma [ nomagic]
22312193 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 )
22352197 )
22362198 }
22372199
22382200 predicate relevantTypeMention ( FunctionType constraint ) {
2239- MethodCallResolution:: methodInfo ( _, _, _, _, constraint , _, _, _ , _ )
2201+ MethodCallResolution:: methodInfo ( _, _, _, _, constraint , _, _)
22402202 }
22412203 }
22422204}
0 commit comments