@@ -1235,10 +1235,19 @@ private module MethodCallResolution {
12351235 private predicate isNotCandidate (
12361236 ImplOrTraitItemNode i , FunctionPositionType self , string derefChainBorrow
12371237 ) {
1238- IsInstantiationOf< MethodCallCand , FunctionPositionType , MethodCallIsInstantiationOfInput2 > :: isNotInstantiationOf ( MkMethodCallCand ( this ,
1238+ IsInstantiationOf< MethodCallCand , FunctionPositionType , MethodCallIsInstantiationOfInput > :: isNotInstantiationOf ( MkMethodCallCand ( this ,
12391239 derefChainBorrow ) , i , self )
12401240 }
12411241
1242+ pragma [ nomagic]
1243+ predicate blah (
1244+ Type type , ImplOrTraitItemNode i , FunctionPositionType self , TypePath selfPath , Type selfType ,
1245+ string derefChainBorrow
1246+ ) {
1247+ selfType != this .getACandidateReceiverTypeAt ( selfPath , derefChainBorrow ) and
1248+ methodCallCandidate ( this , type , i , self , selfPath , selfType )
1249+ }
1250+
12421251 pragma [ nomagic]
12431252 private Type getACandidateReceiverTypeAtNoBorrowNoMatch ( TypePath path , string derefChain ) {
12441253 result = this .getACandidateReceiverTypeAtNoBorrow ( path , derefChain ) and
@@ -1247,9 +1256,11 @@ private module MethodCallResolution {
12471256 not derefChain .matches ( "%.ref" ) and // no need to try a borrow if the last thing we did was a deref
12481257 this .isMethodCall0 ( type , name , arity , derefChainBorrow )
12491258 |
1250- forall ( ImplOrTraitItemNode i , FunctionPositionType self |
1251- methodCallCandidate ( this , type , i , self , _ , _ )
1259+ forall ( ImplOrTraitItemNode i , FunctionPositionType self , TypePath selfPath , Type selfType |
1260+ methodCallCandidate ( this , type , i , self , selfPath , selfType )
12521261 |
1262+ this .blah ( type , i , self , selfPath , selfType , derefChainBorrow )
1263+ or
12531264 this .isNotCandidate ( i , self , derefChainBorrow )
12541265 )
12551266 )
@@ -1262,9 +1273,11 @@ private module MethodCallResolution {
12621273 derefChainBorrow = derefChain + ";borrow" and
12631274 this .isMethodCall0 ( type , name , arity , derefChainBorrow )
12641275 |
1265- forall ( ImplOrTraitItemNode i , FunctionPositionType self |
1266- methodCallCandidate ( this , type , i , self , _ , _ )
1276+ forall ( ImplOrTraitItemNode i , FunctionPositionType self , TypePath selfPath , Type selfType |
1277+ methodCallCandidate ( this , type , i , self , selfPath , selfType )
12671278 |
1279+ this .blah ( type , i , self , selfPath , selfType , derefChainBorrow )
1280+ or
12681281 this .isNotCandidate ( i , self , derefChainBorrow )
12691282 )
12701283 )
@@ -1384,9 +1397,16 @@ private module MethodCallResolution {
13841397
13851398 pragma [ nomagic]
13861399 private predicate isNotInherentTarget ( Impl impl ) {
1387- IsInstantiationOf< MethodCallCand , FunctionPositionType , MethodCallIsInstantiationOfInput2 > :: isNotInstantiationOf ( this ,
1388- impl , _) and
1389- not impl .hasTrait ( )
1400+ IsInstantiationOf< MethodCallCand , FunctionPositionType , MethodCallIsNotInstantiationOfInput > :: isNotInstantiationOf ( this ,
1401+ impl , _)
1402+ }
1403+
1404+ pragma [ nomagic]
1405+ private predicate blah (
1406+ Type type , Impl i , FunctionPositionType self , TypePath selfPath , Type selfType
1407+ ) {
1408+ not i .hasTrait ( ) and
1409+ mc_ .blah ( type , i , self , selfPath , selfType , derefChainBorrow )
13901410 }
13911411
13921412 /**
@@ -1397,11 +1417,18 @@ private module MethodCallResolution {
13971417 private predicate hasNoInherentTarget ( ) {
13981418 exists ( Type type , string name , int arity |
13991419 this .isMethodCall ( _, TypePath:: nil ( ) , type , name , arity ) and
1400- forall ( Impl impl |
1401- methodCandidate ( type , name , arity , impl , _ , _ , _ ) and
1402- not impl .hasTrait ( )
1420+ forall ( Impl i , FunctionPositionType self , TypePath selfPath , Type selfType |
1421+ methodCandidate ( type , name , arity , i , self , selfPath , selfType ) and
1422+ not i .hasTrait ( )
14031423 |
1404- this .isNotInherentTarget ( impl )
1424+ this .blah ( type , i , self , selfPath , selfType )
1425+ or
1426+ this .isNotInherentTarget ( i )
1427+ // forall(Impl impl |
1428+ // methodCandidate(type, name, arity, impl, _, _, _) and
1429+ // not impl.hasTrait()
1430+ // |
1431+ // this.isNotInherentTarget(impl)
14051432 )
14061433 )
14071434 }
@@ -1475,17 +1502,15 @@ private module MethodCallResolution {
14751502 }
14761503 }
14771504
1478- private module MethodCallIsInstantiationOfInput2 implements
1505+ private module MethodCallIsNotInstantiationOfInput implements
14791506 IsInstantiationOfInputSig< MethodCallCand , FunctionPositionType >
14801507 {
14811508 pragma [ nomagic]
14821509 predicate potentialInstantiationOf (
14831510 MethodCallCand mcc , TypeAbstraction abs , FunctionPositionType constraint
14841511 ) {
1485- exists ( MethodCall mc , Type type , string name , int arity |
1486- mcc .isMethodCall ( mc , TypePath:: nil ( ) , type , name , arity ) and
1487- methodCallCandidate ( mc , type , abs , constraint , _, _)
1488- )
1512+ MethodCallIsInstantiationOfInput:: potentialInstantiationOf ( mcc , abs , constraint ) and
1513+ abs = any ( Impl i | not i .hasTrait ( ) )
14891514 }
14901515
14911516 predicate relevantTypeMention ( FunctionPositionType constraint ) {
0 commit comments