@@ -1807,66 +1807,36 @@ private module AssocFunctionResolution {
18071807 }
18081808
18091809 /**
1810- * Holds if the candidate receiver type represented by `derefChain` does not
1811- * have a matching call target at function-call adjusted position `selfPos`.
1810+ * Holds if the candidate receiver type represented by `derefChain` and `borrow`
1811+ * does not have a matching call target at function-call adjusted position `selfPos`.
18121812 */
1813- predicate hasNoCompatibleTargetNoBorrow ( FunctionPosition selfPos , DerefChain derefChain ) {
1814- NoCompatibleTarget:: Borrow:: hasNoCompatibleTarget ( this , selfPos , derefChain , _)
1813+ predicate hasNoCompatibleTarget (
1814+ FunctionPosition selfPos , DerefChain derefChain , BorrowKind borrow
1815+ ) {
1816+ NoCompatibleTarget:: Any:: hasNoCompatibleTarget ( this , selfPos , derefChain , borrow )
18151817 }
18161818
18171819 /**
18181820 * Holds if the candidate receiver type represented by `derefChain` does not have
18191821 * a matching non-blanket call target at function-call adjusted position `selfPos`.
18201822 */
1821- predicate hasNoCompatibleNonBlanketTargetNoBorrow (
1822- FunctionPosition selfPos , DerefChain derefChain
1823- ) {
1824- NoCompatibleTarget:: BorrowNonBlanket:: hasNoCompatibleNonBlanketTarget ( this , selfPos ,
1825- derefChain , _)
1826- }
1827-
1828- /**
1829- * Holds if the candidate receiver type represented by `derefChain`, followed
1830- * by a shared borrow, does not have a matching call target at function-call
1831- * adjusted position `selfPos`.
1832- */
1833- predicate hasNoCompatibleTargetSharedBorrow ( FunctionPosition selfPos , DerefChain derefChain ) {
1834- NoCompatibleTarget:: SharedBorrow:: hasNoCompatibleNonBlanketLikeTarget ( this , selfPos ,
1835- derefChain , _)
1836- }
1837-
1838- /**
1839- * Holds if the candidate receiver type represented by `derefChain`, followed
1840- * by a `mut` borrow, does not have a matching call target at function-call
1841- * adjusted position `selfPos`.
1842- */
1843- predicate hasNoCompatibleTargetMutBorrow ( FunctionPosition selfPos , DerefChain derefChain ) {
1844- NoCompatibleTarget:: MutBorrow:: hasNoCompatibleNonBlanketLikeTarget ( this , selfPos , derefChain ,
1845- _)
1846- }
1847-
1848- /**
1849- * Holds if the candidate receiver type represented by `derefChain`, followed
1850- * by a shared borrow, does not have a matching non-blanket call target at
1851- * function-call adjusted position `selfPos`.
1852- */
1853- predicate hasNoCompatibleNonBlanketTargetSharedBorrow (
1854- FunctionPosition selfPos , DerefChain derefChain
1823+ predicate hasNoCompatibleNonBlanketLikeTarget (
1824+ FunctionPosition selfPos , DerefChain derefChain , BorrowKind borrow
18551825 ) {
1856- NoCompatibleTarget:: SharedBorrowNonBlanket:: hasNoCompatibleNonBlanketTarget ( this , selfPos ,
1857- derefChain , _)
1826+ NoCompatibleTarget:: Any:: hasNoCompatibleNonBlanketLikeTarget ( this , selfPos , derefChain , borrow )
18581827 }
18591828
18601829 /**
1861- * Holds if the candidate receiver type represented by `derefChain`, followed
1862- * by a `mut` borrow, does not have a matching non-blanket call target at
1863- * function-call adjusted position `selfPos`.
1830+ * Holds if the candidate receiver type represented by `derefChain` and `borrow`
1831+ * does not have a matching non-blanket call target at function-call adjusted
1832+ * position `selfPos`.
18641833 */
1865- predicate hasNoCompatibleNonBlanketTargetMutBorrow (
1866- FunctionPosition selfPos , DerefChain derefChain
1834+ predicate hasNoCompatibleNonBlanketTarget (
1835+ FunctionPosition selfPos , DerefChain derefChain , BorrowKind borrow
18671836 ) {
1868- NoCompatibleTarget:: MutBorrowNonBlanket:: hasNoCompatibleNonBlanketTarget ( this , selfPos ,
1869- derefChain , _)
1837+ // NoCompatibleTarget::NonBlanket::hasNoCompatibleNonBlanketTarget(this, selfPos, derefChain,
1838+ // borrow)
1839+ NoCompatibleTarget:: Any:: hasNoCompatibleNonBlanketTarget ( this , selfPos , derefChain , borrow )
18701840 }
18711841
18721842 /**
@@ -1917,11 +1887,11 @@ private module AssocFunctionResolution {
19171887 or
19181888 exists ( RefType rt |
19191889 // first try shared borrow
1920- this .hasNoCompatibleTargetNoBorrow ( selfPos , derefChain ) and
1890+ this .hasNoCompatibleTarget ( selfPos , derefChain , TNoBorrowKind ( ) ) and
19211891 borrow .isSharedBorrow ( )
19221892 or
19231893 // then try mutable borrow
1924- this .hasNoCompatibleTargetSharedBorrow ( selfPos , derefChain ) and
1894+ this .hasNoCompatibleNonBlanketLikeTarget ( selfPos , derefChain , TSomeBorrowKind ( false ) ) and
19251895 borrow .isMutableBorrow ( )
19261896 |
19271897 rt = borrow .getRefType ( ) and
@@ -2298,20 +2268,30 @@ private module AssocFunctionResolution {
22982268 }
22992269 }
23002270
2301- bindingset [ derefChain ]
2302- private predicate borrowCand (
2271+ pragma [ nomagic ]
2272+ private predicate sharedBorrowCand (
23032273 AssocFunctionCall afc , FunctionPosition selfPos , DerefChain derefChain , BorrowKind borrow
23042274 ) {
2305- afc .supportsAutoDerefAndBorrow ( ) and
2306- afc .hasReceiverAtPos ( selfPos ) and
2307- exists ( derefChain ) and
2308- borrow = TNoBorrowKind ( )
2275+ exists ( BorrowKind prev |
2276+ afc .hasNoCompatibleTarget ( selfPos , derefChain , prev ) and
2277+ prev .isNoBorrow ( ) and
2278+ borrow .isSharedBorrow ( )
2279+ )
23092280 }
23102281
2311- module Borrow = Checks< borrowCand / 4 > ;
2282+ pragma [ nomagic]
2283+ private predicate mutBorrowCand (
2284+ AssocFunctionCall afc , FunctionPosition selfPos , DerefChain derefChain , BorrowKind borrow
2285+ ) {
2286+ exists ( BorrowKind prev |
2287+ afc .hasNoCompatibleNonBlanketLikeTarget ( selfPos , derefChain , prev ) and
2288+ prev .isSharedBorrow ( ) and
2289+ borrow .isMutableBorrow ( )
2290+ )
2291+ }
23122292
23132293 bindingset [ derefChain]
2314- private predicate borrowNonBlanketCand (
2294+ private predicate anyCand (
23152295 AssocFunctionCall afc , FunctionPosition selfPos , DerefChain derefChain , BorrowKind borrow
23162296 ) {
23172297 (
@@ -2327,50 +2307,56 @@ private module AssocFunctionResolution {
23272307 i .isBlanketImplementation ( )
23282308 )
23292309 ) and
2330- borrow = TNoBorrowKind ( )
2331- }
2332-
2333- module BorrowNonBlanket = Checks< borrowNonBlanketCand / 4 > ;
2334-
2335- pragma [ nomagic]
2336- private predicate sharedBorrowCand (
2337- AssocFunctionCall afc , FunctionPosition selfPos , DerefChain derefChain , BorrowKind borrow
2338- ) {
2339- afc .hasNoCompatibleTargetNoBorrow ( selfPos , derefChain ) and
2340- borrow = TSomeBorrowKind ( false )
2310+ borrow .isNoBorrow ( )
2311+ or
2312+ sharedBorrowCand ( afc , selfPos , derefChain , borrow )
2313+ or
2314+ mutBorrowCand ( afc , selfPos , derefChain , borrow )
23412315 }
23422316
2343- module SharedBorrow = Checks< sharedBorrowCand / 4 > ;
2317+ module Any = Checks< anyCand / 4 > ;
23442318
2345- pragma [ nomagic ]
2346- private predicate mutBorrowCand (
2319+ bindingset [ derefChain ]
2320+ private predicate nonBlanketCand (
23472321 AssocFunctionCall afc , FunctionPosition selfPos , DerefChain derefChain , BorrowKind borrow
23482322 ) {
2349- afc .hasNoCompatibleTargetSharedBorrow ( selfPos , derefChain ) and
2350- borrow = TSomeBorrowKind ( true )
2323+ (
2324+ afc .supportsAutoDerefAndBorrow ( ) and
2325+ afc .hasReceiverAtPos ( selfPos ) and
2326+ exists ( derefChain )
2327+ or
2328+ // needed for the `hasNoCompatibleNonBlanketTarget` check in
2329+ // `ArgSatisfiesBlanketLikeConstraintInput::hasBlanketCandidate`
2330+ exists ( ImplItemNode i |
2331+ derefChain .isEmpty ( ) and
2332+ blanketLikeCandidate ( afc , _, selfPos , i , _, _, _) and
2333+ i .isBlanketImplementation ( )
2334+ )
2335+ ) and
2336+ borrow .isNoBorrow ( )
2337+ or
2338+ sharedBorrowNonBlanketCand ( afc , selfPos , derefChain , borrow )
2339+ or
2340+ mutBorrowNonBlanketCand ( afc , selfPos , derefChain , borrow )
23512341 }
23522342
2353- module MutBorrow = Checks< mutBorrowCand / 4 > ;
2343+ module NonBlanket = Checks< nonBlanketCand / 4 > ;
23542344
23552345 pragma [ nomagic]
23562346 private predicate sharedBorrowNonBlanketCand (
23572347 AssocFunctionCall afc , FunctionPosition selfPos , DerefChain derefChain , BorrowKind borrow
23582348 ) {
2359- afc .hasNoCompatibleTargetNoBorrow ( selfPos , derefChain ) and
2349+ afc .hasNoCompatibleTarget ( selfPos , derefChain , TNoBorrowKind ( ) ) and
23602350 borrow = TSomeBorrowKind ( false )
23612351 }
23622352
2363- module SharedBorrowNonBlanket = Checks< sharedBorrowNonBlanketCand / 4 > ;
2364-
23652353 pragma [ nomagic]
23662354 private predicate mutBorrowNonBlanketCand (
23672355 AssocFunctionCall afc , FunctionPosition selfPos , DerefChain derefChain , BorrowKind borrow
23682356 ) {
2369- afc .hasNoCompatibleNonBlanketTargetSharedBorrow ( selfPos , derefChain ) and
2357+ afc .hasNoCompatibleNonBlanketTarget ( selfPos , derefChain , TSomeBorrowKind ( false ) ) and
23702358 borrow = TSomeBorrowKind ( true )
23712359 }
2372-
2373- module MutBorrowNonBlanket = Checks< mutBorrowNonBlanketCand / 4 > ;
23742360 }
23752361
23762362 pragma [ nomagic]
@@ -2409,14 +2395,7 @@ private module AssocFunctionResolution {
24092395
24102396 pragma [ nomagic]
24112397 predicate hasNoCompatibleNonBlanketTarget ( ) {
2412- afc_ .hasNoCompatibleNonBlanketTargetSharedBorrow ( selfPos_ , derefChain ) and
2413- borrow .isSharedBorrow ( )
2414- or
2415- afc_ .hasNoCompatibleNonBlanketTargetMutBorrow ( selfPos_ , derefChain ) and
2416- borrow .isMutableBorrow ( )
2417- or
2418- afc_ .hasNoCompatibleNonBlanketTargetNoBorrow ( selfPos_ , derefChain ) and
2419- borrow .isNoBorrow ( )
2398+ afc_ .hasNoCompatibleNonBlanketTarget ( selfPos_ , derefChain , borrow )
24202399 }
24212400
24222401 pragma [ nomagic]
@@ -2525,7 +2504,7 @@ private module AssocFunctionResolution {
25252504 MkCallDerefCand ( AssocFunctionCall afc , FunctionPosition selfPos , DerefChain derefChain ) {
25262505 afc .supportsAutoDerefAndBorrow ( ) and
25272506 afc .hasReceiverAtPos ( selfPos ) and
2528- afc .hasNoCompatibleTargetMutBorrow ( selfPos , derefChain ) and
2507+ afc .hasNoCompatibleNonBlanketLikeTarget ( selfPos , derefChain , TSomeBorrowKind ( true ) ) and
25292508 exists ( afc .getSelfTypeAtNoBorrow ( selfPos , derefChain , TypePath:: nil ( ) ) )
25302509 }
25312510
0 commit comments