@@ -1029,6 +1029,10 @@ private class FunctionType extends TFunctionType {
10291029 this = MkInheritedFunctionType ( f , pos , parent , i )
10301030 }
10311031
1032+ /**
1033+ * Holds if this function type applies to the function `f` at position `pos`,
1034+ * when viewed as a member of the `impl` or trait item `i`.
1035+ */
10321036 predicate appliesTo ( Function f , FunctionTypePosition pos , ImplOrTraitItemNode i ) {
10331037 this .asFunctionType ( f , pos , i )
10341038 or
@@ -1110,33 +1114,38 @@ private Function getMethodSuccessor(ItemNode item, string name, int arity) {
11101114/** Provides logic for resolving method calls. */
11111115private module MethodCallResolution {
11121116 /**
1113- * Holds if a method for `type` with the name `name` and the arity `arity`
1114- * exists in `i`.
1117+ * Holds if method `f` with the name `name` and the arity `arity` exists in
1118+ * `i`, and the type of the `self` parameter is `selfType`.
1119+ *
1120+ * `rootType` is the root type of `selfType`, and `selfRootPath` points to
1121+ * `selfRootType` inside `selfType`, where `selfRootType` is either the type
1122+ * being implemented, when `i` is an `impl`, or the trait itself when `i` is
1123+ * a trait.
11151124 */
11161125 pragma [ nomagic]
1117- predicate methodCandidate (
1118- Function f , Type type , string name , int arity , ImplOrTraitItemNode i , FunctionType self ,
1119- TypePath selfPath , Type selfType
1126+ predicate methodInfo (
1127+ Function f , string name , int arity , ImplOrTraitItemNode i , FunctionType selfType , Type rootType ,
1128+ TypePath selfRootPath , Type selfRootType
11201129 ) {
11211130 exists ( FunctionTypePosition pos |
11221131 f = i .getASuccessor ( name ) and
11231132 arity = f .getParamList ( ) .getNumberOfParams ( ) and
1124- type = self .getTypeAt ( TypePath:: nil ( ) ) and
1125- self .appliesTo ( f , pos , i ) and
1133+ rootType = selfType .getTypeAt ( TypePath:: nil ( ) ) and
1134+ selfType .appliesTo ( f , pos , i ) and
11261135 pos .isSelf ( ) and
1127- self .getTypeAt ( selfPath ) = selfType and
1136+ selfType .getTypeAt ( selfRootPath ) = selfRootType and
11281137 not i .( ImplItemNode ) .isBlanket ( )
11291138 |
1130- selfType = i .( Impl ) .getSelfTy ( ) .( TypeMention ) .resolveType ( )
1139+ selfRootType = i .( Impl ) .getSelfTy ( ) .( TypeMention ) .resolveType ( )
11311140 or
1132- selfType = TTrait ( i )
1141+ selfRootType = TTrait ( i )
11331142 )
11341143 }
11351144
11361145 pragma [ nomagic]
1137- private predicate methodCandidateImplTrait ( string name , int arity , Trait trait ) {
1146+ private predicate traitMethodInfo ( string name , int arity , Trait trait ) {
11381147 exists ( ImplItemNode i |
1139- methodCandidate ( _, _ , name , arity , i , _, _, _) and
1148+ methodInfo ( _, name , arity , i , _ , _, _, _) and
11401149 trait = i .resolveTraitTy ( )
11411150 )
11421151 }
@@ -1145,7 +1154,7 @@ private module MethodCallResolution {
11451154 private predicate methodCallTraitCandidate ( Element mc , Trait trait ) {
11461155 exists ( string name , int arity |
11471156 mc .( MethodCall ) .isMethodCall ( name , arity ) and
1148- methodCandidateImplTrait ( name , arity , trait )
1157+ traitMethodInfo ( name , arity , trait )
11491158 )
11501159 }
11511160
@@ -1159,14 +1168,27 @@ private module MethodCallResolution {
11591168 methodCallVisibleTraitCandidate ( mc , impl .resolveTraitTy ( ) )
11601169 }
11611170
1171+ /**
1172+ * Holds if method call `mc` may target a method in `i` with `self` parameter having
1173+ * type `selfType`.
1174+ *
1175+ * `rootType` is the root type of `selfType`, and `selfRootPath` points to
1176+ * `selfRootType` inside `selfType`, where `selfRootType` is either the type
1177+ * being implemented, when `i` is an `impl`, or the trait itself when `i` is
1178+ * a trait.
1179+ *
1180+ * This predicate only checks for matching method names and arities, and whether
1181+ * the trait being implemented by `i` (when `i` is not a trait itself) is visible
1182+ * at `mc`.
1183+ */
11621184 pragma [ inline]
11631185 private predicate methodCallCandidate (
1164- MethodCall mc , Type type , ImplOrTraitItemNode i , FunctionType self , TypePath selfPath ,
1165- Type selfType
1186+ MethodCall mc , ImplOrTraitItemNode i , FunctionType self , Type rootType , TypePath selfRootPath ,
1187+ Type selfRootType
11661188 ) {
11671189 exists ( string name , int arity |
11681190 mc .isMethodCall ( name , arity ) and
1169- methodCandidate ( _, type , name , arity , i , self , selfPath , selfType )
1191+ methodInfo ( _, name , arity , i , self , rootType , selfRootPath , selfRootType )
11701192 |
11711193 not i .( Impl ) .hasTrait ( )
11721194 or
@@ -1236,12 +1258,12 @@ private module MethodCallResolution {
12361258 derefChainBorrow ) , i , _)
12371259 or
12381260 // not MethodCallIsInstantiationOfInput::potentialInstantiationOf(mcc, abs, constraint)
1239- exists ( Type rootType , TypePath selfPath , Type selfType |
1261+ exists ( Type rootType , TypePath selfRootPath , Type selfRootType |
12401262 rootType = this .getACandidateReceiverTypeAtSubstituteTraitBounds ( derefChainBorrow ) and
12411263 // mcc.isMethodCall(mc, selfPath, selfType, name, arity) and
1242- methodCallCandidate ( this , rootType , i , _, selfPath , selfType ) and
1243- selfType !=
1244- this .getACandidateReceiverTypeAtSubstituteTraitBounds ( selfPath , derefChainBorrow )
1264+ methodCallCandidate ( this , i , _, rootType , selfRootPath , selfRootType ) and
1265+ selfRootType !=
1266+ this .getACandidateReceiverTypeAtSubstituteTraitBounds ( selfRootPath , derefChainBorrow )
12451267 )
12461268 }
12471269
@@ -1252,7 +1274,7 @@ private module MethodCallResolution {
12521274 not derefChain .matches ( "%.ref" ) and // no need to try a borrow if the last thing we did was a deref
12531275 rootType = this .getACandidateReceiverTypeAtSubstituteTraitBounds ( derefChainBorrow )
12541276 |
1255- forall ( ImplOrTraitItemNode i | methodCallCandidate ( this , rootType , i , _, _, _) |
1277+ forall ( ImplOrTraitItemNode i | methodCallCandidate ( this , i , _, rootType , _, _) |
12561278 this .isNotCandidate ( i , derefChainBorrow )
12571279 )
12581280 )
@@ -1266,7 +1288,7 @@ private module MethodCallResolution {
12661288
12671289 pragma [ nomagic]
12681290 private predicate hasRefCandidate ( ImplOrTraitItemNode i ) {
1269- methodCallCandidate ( this , TRefType ( ) , i , _, _, _)
1291+ methodCallCandidate ( this , i , _, TRefType ( ) , _, _)
12701292 }
12711293
12721294 pragma [ nomagic]
@@ -1413,7 +1435,7 @@ private module MethodCallResolution {
14131435
14141436 // pragma[nomagic]
14151437 // private predicate blah(
1416- // Type type, Impl i, FunctionType self, TypePath selfPath , Type selfType
1438+ // Type type, Impl i, FunctionType self, TypePath selfRootPath , Type selfRootType
14171439 // ) {
14181440 // not i.hasTrait() and
14191441 // mc_.blah(type, i, self, selfPath, selfType, derefChainBorrow)
@@ -1426,15 +1448,15 @@ private module MethodCallResolution {
14261448 private predicate hasNoInherentTarget ( ) {
14271449 exists ( Type rootType , string name , int arity |
14281450 this .isMethodCall ( _, TypePath:: nil ( ) , rootType , name , arity ) and
1429- forall ( Impl i , FunctionType self , TypePath selfPath , Type selfType |
1430- methodCandidate ( _, rootType , name , arity , i , self , selfPath , selfType ) and
1451+ forall ( Impl i , FunctionType self , TypePath selfRootPath , Type selfRootType |
1452+ methodInfo ( _, name , arity , i , self , rootType , selfRootPath , selfRootType ) and
14311453 not i .hasTrait ( )
14321454 |
14331455 // this.blah(type, i, self, selfPath, selfType)
14341456 // or
14351457 this .isNotInherentTarget ( i )
14361458 // forall(Impl impl |
1437- // methodCandidate (type, name, arity, impl, _, _, _) and
1459+ // methodInfo (type, name, arity, impl, _, _, _) and
14381460 // not impl.hasTrait()
14391461 // |
14401462 // this.isNotInherentTarget(impl)
@@ -1503,15 +1525,15 @@ private module MethodCallResolution {
15031525 predicate potentialInstantiationOf (
15041526 MethodCallCand mcc , TypeAbstraction abs , FunctionType constraint
15051527 ) {
1506- exists ( MethodCall mc , string name , int arity , TypePath selfPath , Type selfType |
1507- mcc .isMethodCall ( mc , selfPath , selfType , name , arity ) and
1508- methodCallCandidate ( mc , _ , abs , constraint , selfPath , selfType )
1528+ exists ( MethodCall mc , string name , int arity , TypePath selfRootPath , Type selfRootType |
1529+ mcc .isMethodCall ( mc , selfRootPath , selfRootType , name , arity ) and
1530+ methodCallCandidate ( mc , abs , constraint , _ , selfRootPath , selfRootType )
15091531 // mc = Debug::getRelevantLocatable()
15101532 )
15111533 }
15121534
15131535 predicate relevantTypeMention ( FunctionType constraint ) {
1514- methodCandidate ( _, _, _, _, _ , constraint , _, _)
1536+ methodInfo ( _, _, _, _, constraint , _ , _, _)
15151537 }
15161538 }
15171539
@@ -1525,13 +1547,13 @@ private module MethodCallResolution {
15251547 abs = any ( Impl i | not i .hasTrait ( ) ) and
15261548 exists ( MethodCall mc , string name , int arity , Type rootType |
15271549 mcc .isMethodCall ( mc , TypePath:: nil ( ) , rootType , name , arity ) and
1528- methodCallCandidate ( mc , rootType , abs , constraint , _, _)
1550+ methodCallCandidate ( mc , abs , constraint , rootType , _, _)
15291551 // mc = Debug::getRelevantLocatable()
15301552 )
15311553 }
15321554
15331555 predicate relevantTypeMention ( FunctionType constraint ) {
1534- methodCandidate ( _, _, _, _, _ , constraint , _, _)
1556+ methodInfo ( _, _, _, _, constraint , _ , _, _)
15351557 }
15361558 }
15371559}
@@ -1779,11 +1801,11 @@ private module FunctionCallResolution {
17791801 Function getATraitCandidateMethod0 (
17801802 TraitItemNode trait , ImplOrTraitItemNode i , FunctionType self , Function resolved
17811803 ) {
1782- exists ( TypePath selfPath , Type selfType |
1804+ exists ( TypePath selfRootPath , Type selfRootType |
17831805 result = this .getPathResolutionResolvedFunctionOrImplementation ( resolved ) and
17841806 trait = this .( Call ) .getTrait ( ) and
1785- MethodCallResolution:: methodCandidate ( result , _, _, _ , i , self , selfPath , selfType ) and
1786- this .getTypeAt ( selfPath ) = selfType
1807+ MethodCallResolution:: methodInfo ( result , _, _, i , self , _ , selfRootPath , selfRootType ) and
1808+ this .getTypeAt ( selfRootPath ) = selfRootType
17871809 )
17881810 }
17891811
@@ -1867,7 +1889,7 @@ private module FunctionCallResolution {
18671889 }
18681890
18691891 predicate relevantTypeMention ( FunctionType constraint ) {
1870- MethodCallResolution:: methodCandidate ( _, _, _, _, _ , constraint , _, _)
1892+ MethodCallResolution:: methodInfo ( _, _, _, _, constraint , _ , _, _)
18711893 }
18721894 }
18731895}
@@ -2135,11 +2157,12 @@ private module OperationResolution {
21352157 IsInstantiationOfInputSig< Op , FunctionType >
21362158 {
21372159 pragma [ nomagic]
2138- private predicate methodCandidate (
2160+ private predicate methodInfo (
21392161 TypeAbstraction abs , FunctionType constraint , Trait trait , string name , int arity ,
2140- TypePath selfPath , Type selfType
2162+ TypePath selfRootPath , Type selfRootType
21412163 ) {
2142- MethodCallResolution:: methodCandidate ( _, _, name , arity , abs , constraint , selfPath , selfType ) and //and
2164+ MethodCallResolution:: methodInfo ( _, name , arity , abs , constraint , _, selfRootPath ,
2165+ selfRootType ) and //and
21432166 (
21442167 trait = abs .( ImplItemNode ) .resolveTraitTy ( )
21452168 or
@@ -2149,14 +2172,14 @@ private module OperationResolution {
21492172
21502173 pragma [ nomagic]
21512174 predicate potentialInstantiationOf ( Op op , TypeAbstraction abs , FunctionType constraint ) {
2152- exists ( Trait trait , string name , int arity , TypePath selfPath , Type selfType |
2153- op .isOperation ( selfPath , selfType , trait , name , arity ) and
2154- methodCandidate ( abs , constraint , trait , name , arity , selfPath , selfType )
2175+ exists ( Trait trait , string name , int arity , TypePath selfRootPath , Type selfRootType |
2176+ op .isOperation ( selfRootPath , selfRootType , trait , name , arity ) and
2177+ methodInfo ( abs , constraint , trait , name , arity , selfRootPath , selfRootType )
21552178 )
21562179 }
21572180
21582181 predicate relevantTypeMention ( FunctionType constraint ) {
2159- MethodCallResolution:: methodCandidate ( _, _, _, _, _ , constraint , _, _)
2182+ MethodCallResolution:: methodInfo ( _, _, _, _, constraint , _ , _, _)
21602183 }
21612184 }
21622185}
0 commit comments