name matcher: match method fn pointers through the trait ref if enabled

charon-ml/src/NameMatcher.ml

@@ -670,7 +670,24 @@ let match_fn_ptr (ctx : ctx) (c : match_config) (p : pattern) (func : E.fn_ptr)
           match_name_with_generics ctx c p (to_name [ name ]) func.generics)
   | FunId (FRegular fid) ->
       let d = A.FunDeclId.Map.find fid ctx.fun_decls in
-      match_name_with_generics ctx c p d.item_meta.name func.generics
+      (* Match the pattern on the name of the function. *)
+      let match_function_name =
+        match_name_with_generics ctx c p d.item_meta.name func.generics
+      in
+      (* Match the pattern on the trait implementation and method name, if applicable. *)
+      let match_trait_ref =
+        match d.kind with
+        | TraitImplItem (impl_id, _, method_name, _)
+          when c.match_with_trait_decl_refs ->
+            let impl = T.TraitImplId.Map.find impl_id ctx.trait_impls in
+            (* The first half of `func.generics` is generics for the impl.
+               TODO: substitute these args into `impl.impl_trait`. *)
+            match_trait_decl_ref_item ctx c (mk_empty_maps ()) p
+              { binder_value = impl.impl_trait; binder_regions = [] }
+              method_name func.generics
+        | _ -> false
+      in
+      match_function_name || match_trait_ref
   | TraitMethod (tr, method_name, _) ->
       match_trait_decl_ref_item ctx c (mk_empty_maps ()) p tr.trait_decl_ref
         method_name func.generics

charon/tests/ui/ml-name-matcher-tests.rs

@@ -28,7 +28,7 @@ impl<T> Trait<Option<T>> for Box<T> {
         "test_crate::{test_crate::Trait<alloc::boxed::Box<@T>, core::option::Option<@U>>}::method"
     )]
     #[pattern::pass("test_crate::{test_crate::Trait<@T, @U>}::method")]
-    #[pattern::fail("test_crate::Trait<@T, @U>::method")]
+    #[pattern::pass("test_crate::Trait<@T, @U>::method")]
     fn method<U>() {}
 }