@@ -1167,11 +1167,29 @@ private module MethodCallResolution {
11671167 }
11681168
11691169 pragma [ nomagic]
1170- private predicate isMethodCall0 ( Type rootType , string name , int arity , string derefChainBorrow ) {
1170+ predicate isMethodCall0 ( Type rootType , string name , int arity , string derefChainBorrow ) {
11711171 rootType = this .getACandidateReceiverTypeAt ( TypePath:: nil ( ) , derefChainBorrow ) and
11721172 this .isMethodCall ( name , arity )
11731173 }
11741174
1175+ pragma [ nomagic]
1176+ private predicate isNot (
1177+ ImplOrTraitItemNode i , FunctionPositionType self , string derefChainBorrow
1178+ ) {
1179+ IsInstantiationOf< MethodCallCand , FunctionPositionType , MethodCallIsInstantiationOfInput > :: isNotInstantiationOf ( MkMethodCallCand ( this ,
1180+ derefChainBorrow ) , i , self )
1181+ or
1182+ exists ( Trait trait |
1183+ relevantTraitVisible0 ( i , self , derefChainBorrow , this , trait ) and
1184+ TraitIsVisible< relevantTraitVisible1 / 2 > :: traitIsNotVisible ( this ,
1185+ pragma [ only_bind_into ] ( trait ) ) and
1186+ not (
1187+ this instanceof IndexExpr and
1188+ trait instanceof IndexTrait
1189+ )
1190+ )
1191+ }
1192+
11751193 pragma [ nomagic]
11761194 private Type getACandidateReceiverTypeAtNoBorrowNoMatch ( TypePath path , string derefChain ) {
11771195 result = this .getACandidateReceiverTypeAtNoBorrow ( path , derefChain ) and
@@ -1180,11 +1198,12 @@ private module MethodCallResolution {
11801198 not derefChain .matches ( "%.ref" ) and // no need to try a borrow if the last thing we did was a deref
11811199 this .isMethodCall0 ( rootType , name , arity , derefChainBorrow )
11821200 |
1183- forall ( Impl impl , FunctionPositionType self |
1184- methodCandidate ( rootType , name , arity , impl , self )
1201+ forall ( ImplOrTraitItemNode i , FunctionPositionType self |
1202+ methodCandidate ( rootType , name , arity , i , self )
11851203 |
1186- IsInstantiationOf< MethodCallCand , FunctionPositionType , MethodCallIsInstantiationOfInput > :: isNotInstantiationOf ( MkMethodCallCand ( this ,
1187- derefChainBorrow ) , impl , self )
1204+ this .isNot ( i , self , derefChainBorrow )
1205+ // IsInstantiationOf<MethodCallCand, FunctionPositionType, MethodCallIsInstantiationOfInput>::isNotInstantiationOf(MkMethodCallCand(this,
1206+ // derefChainBorrow), i, self)
11881207 )
11891208 )
11901209 }
@@ -1196,11 +1215,12 @@ private module MethodCallResolution {
11961215 derefChainBorrow = derefChain + ";borrow" and
11971216 this .isMethodCall0 ( rootType , name , arity , derefChainBorrow )
11981217 |
1199- forall ( Impl impl , FunctionPositionType self |
1200- methodCandidate ( rootType , name , arity , impl , self )
1218+ forall ( ImplOrTraitItemNode i , FunctionPositionType self |
1219+ methodCandidate ( rootType , name , arity , i , self )
12011220 |
1202- IsInstantiationOf< MethodCallCand , FunctionPositionType , MethodCallIsInstantiationOfInput > :: isNotInstantiationOf ( MkMethodCallCand ( this ,
1203- derefChainBorrow ) , impl , self )
1221+ // IsInstantiationOf<MethodCallCand, FunctionPositionType, MethodCallIsInstantiationOfInput>::isNotInstantiationOf(MkMethodCallCand(this,
1222+ // derefChainBorrow), i, self)
1223+ this .isNot ( i , self , derefChainBorrow )
12041224 )
12051225 )
12061226 }
@@ -1256,6 +1276,20 @@ private module MethodCallResolution {
12561276 }
12571277 }
12581278
1279+ private predicate relevantTraitVisible0 (
1280+ ImplItemNode i , FunctionPositionType self , string derefChainBorrow , MethodCall mc , Trait trait
1281+ ) {
1282+ exists ( Type rootType , string name , int arity |
1283+ mc .( MethodCall ) .isMethodCall0 ( rootType , name , arity , derefChainBorrow ) and
1284+ methodCandidate ( rootType , name , arity , i , self ) and
1285+ trait = i .resolveTraitTy ( )
1286+ )
1287+ }
1288+
1289+ private predicate relevantTraitVisible1 ( Element mc , Trait trait ) {
1290+ relevantTraitVisible0 ( _, _, _, mc , trait )
1291+ }
1292+
12591293 private class MethodCallMethodCallExpr extends MethodCall , MethodCallExpr {
12601294 pragma [ nomagic]
12611295 override predicate isMethodCall ( string name , int arity ) {
0 commit comments