Mono Name-Matcher

charon-ml/name_matcher_parser/Ast.ml

@@ -55,6 +55,7 @@ and pattern_elem =
           In order to not use disambiguators everywhere in patterns, we allow
           omitting the disambiguator when it is equal to 0. *)
   | PImpl of expr
+  | PWild  (** A wildcard pattern, that matches anything *)
 
 (** An expression can be a type or a trait ref.
 

charon-ml/name_matcher_parser/Lexer.mll

@@ -18,6 +18,7 @@ rule token = parse
   | ''' { REGION (index lexbuf) }
   | "true" { TRUE }
   | "false" { FALSE }
+  | "_" { WILDCARD }
   | ident { IDENT (Lexing.lexeme lexbuf) }
   | digit { INT (Z.of_string (Lexing.lexeme lexbuf)) }
   | '(' { LEFT_BRACKET }

charon-ml/name_matcher_parser/Parser.mly

@@ -6,6 +6,7 @@ open Ast
 %token <Ast.var option> VAR // For types and const generics
 %token <Ast.var option> REGION
 %token <Z.t> INT
+%token WILDCARD
 %token STATIC_REGION
 %token SEP TRUE FALSE
 %token LEFT_BRACKET RIGHT_BRACKET
@@ -38,6 +39,7 @@ pattern:
   | e=pattern_elem SEP n=pattern { e :: n }
 
 pattern_elem:
+  | WILDCARD { PWild }
   // (Instantiated) identifier
   | id=IDENT { PIdent (id, 0, []) }
   | id=IDENT; HASH; disamb=INT { PIdent (id, Z.to_int disamb, []) }

charon-ml/src/NameMatcher.ml

@@ -123,6 +123,7 @@ and pattern_elem_to_string (c : print_config) (e : pattern_elem) : string =
       match c.tgt with
       | TkPattern | TkPretty -> "{" ^ ty ^ "}"
       | TkName -> ty)
+  | PWild -> "_"
 
 and expr_to_string (c : print_config) (e : expr) : string =
   match e with
@@ -436,13 +437,35 @@ let match_literal (pl : literal) (l : Values.literal) : bool =
 let rec match_name_with_generics (ctx : 'fun_body ctx) (c : match_config)
     ?(m : maps = mk_empty_maps ()) (p : pattern) (n : T.name)
     (g : T.generic_args) : bool =
+  (* Handle monomorphized matching: if the name ends with a PeMonomorphized
+     element, use the monomorphized args and continue matching without that
+     element *)
+  let n, g =
+    match List.rev n with
+    | PeMonomorphized mono_args :: rest_rev ->
+        (* In this case, we may still have some late-bound generics in `g`, this could ONLY happen for regions *)
+        let regions_count, types_count, const_generics_count, trait_refs_count =
+          TypesUtils.generic_args_lengths g
+        in
+        assert (
+          types_count = 0 && const_generics_count = 0 && trait_refs_count = 0);
+        (* We additionally append the regions from `g` to the monomorphized args, so that we can match against them. *)
+        let merged_args =
+          if regions_count > 0 then begin
+            (* Late-bound regions are appended after the monomorphized ones. *)
+            { mono_args with regions = mono_args.regions @ g.regions }
+          end
+          else mono_args
+        in
+        (List.rev rest_rev, merged_args)
+    | _ -> (n, g)
+  in
   match (p, n) with
   | [], [] ->
       raise
         (Failure
            "match_name_with_generics: attempt to match empty names and patterns")
       (* We shouldn't get there: the names/patterns should be non empty *)
-  | [], [ PeMonomorphized _ ] -> true (* We ignored monomorphizeds *)
   | [ PIdent (pid, pd, pg) ], [ PeIdent (id, d) ] ->
       log#ldebug
         (lazy
@@ -484,6 +507,9 @@ let rec match_name_with_generics (ctx : 'fun_body ctx) (c : match_config)
       | ImplElemTrait impl_id ->
           match_expr_with_trait_impl_id ctx c pty impl_id
           && match_name_with_generics ctx c p n g)
+  | PWild :: p, _ :: n ->
+      (* Wildcard: skip this element in the name *)
+      match_name_with_generics ctx c p n g
   | _ -> false
 
 and match_name (ctx : 'fun_body ctx) (c : match_config) (p : pattern)
@@ -719,10 +745,14 @@ let match_fn_ptr (ctx : 'fun_body ctx) (c : match_config) (p : pattern)
           let name = builtin_fun_id_to_string fid in
           match_name_with_generics ctx c p (to_name [ name ]) func.generics)
   | FunId (FRegular fid) ->
+      (* Lookup the function decl *)
       let d = Types.FunDeclId.Map.find fid ctx.crate.fun_decls in
       (* 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
+        let ret =
+          match_name_with_generics ctx c p d.item_meta.name func.generics
+        in
+        ret
       in
       (* Match the pattern on the trait implementation and method name, if applicable. *)
       let match_trait_ref =
@@ -934,7 +964,10 @@ and path_elem_with_generic_args_to_pattern (ctx : 'fun_body ctx)
       | Some args -> [ PIdent (s, d, args) ]
     end
   | PeImpl impl -> [ impl_elem_to_pattern ctx c impl ]
-  | PeMonomorphized _ -> []
+  | PeMonomorphized _ ->
+      (* In pattern generation, we skip monomorphized elements since patterns
+         are meant to match the logical structure, not the instantiation details *)
+      []
 
 and impl_elem_to_pattern (ctx : 'fun_body ctx) (c : to_pat_config)
     (impl : T.impl_elem) : pattern_elem =
@@ -1441,6 +1474,9 @@ module NameMatcherMap = struct
     (* Check if we reached the destination *)
     match name with
     | [] | [ PeMonomorphized _ ] ->
+        (* For tree search, we also consider monomorphized elements as terminal
+           since they represent instantiation details, not logical structure.
+           The monomorphized matching is always handled by the calling context. *)
         if g = TypesUtils.empty_generic_args then node_v else None
     | _ ->
         (* Explore the children *)

charon-ml/tests/Test_NameMatcher.ml

@@ -69,17 +69,19 @@ module PatternTest = struct
 
   type env = {
     ctx : LlbcAst.block ctx;
+    file_name : string;
     match_config : match_config;
     fmt_env : PrintLlbcAst.fmt_env;
     print_config : print_config;
     to_pat_config : to_pat_config;
   }
 
-  let mk_env (ctx : LlbcAst.block ctx) : env =
+  let mk_env (ctx : LlbcAst.block ctx) file_name : env =
     let tgt = TkPattern in
     let match_with_trait_decl_refs = true in
     {
       ctx;
+      file_name;
       match_config = { map_vars_to_vars = false; match_with_trait_decl_refs };
       print_config = { tgt };
       fmt_env = ctx_to_fmt_env ctx;
@@ -156,11 +158,12 @@ module PatternTest = struct
       match_fn_ptr env.ctx env.match_config test.pattern fn_ptr
     in
     if test.success && not match_success then (
-      log#error "Pattern %s failed to match function %s\n"
+      log#error "Pattern %s failed to match function %s (in `%s`)\n"
         (pattern_to_string env.print_config test.pattern)
         (pattern_to_string env.print_config
            (fn_ptr_to_pattern env.ctx env.to_pat_config decl.signature.generics
-              fn_ptr));
+              fn_ptr))
+        env.file_name;
       false)
     else if (not test.success) && match_success then (
       log#error "Pattern %s matches function %s but shouldn't\n"
@@ -188,7 +191,7 @@ let annotated_rust_tests test_file =
 
   (* We look through all declarations for our special attributes and check each case. *)
   let ctx = ctx_from_crate crate in
-  let env = PatternTest.mk_env ctx in
+  let env = PatternTest.mk_env ctx test_file in
   let all_pass =
     T.FunDeclId.Map.for_all
       (fun _ (decl : fun_decl) ->

charon-ml/tests/Tests.ml

@@ -15,3 +15,6 @@ let () =
 (* llbc files are copied into the `_build` dir by the `(deps)` rule in `./dune`. *)
 let () = Test_Deserialize.run_tests "test-outputs"
 let () = Test_NameMatcher.run_tests "test-outputs/ml-name-matcher-tests.llbc"
+
+let () =
+  Test_NameMatcher.run_tests "test-outputs/ml-mono-name-matcher-tests.llbc"

charon/rustfmt.toml

@@ -0,0 +1 @@
+style_edition = "2024"

charon/src/name_matcher/mod.rs

@@ -3,7 +3,7 @@ use std::cmp::Ordering;
 use itertools::{EitherOrBoth, Itertools};
 use serde::{Deserialize, Serialize};
 
-use crate::ast::*;
+use crate::{ast::*, formatter::IntoFormatter, pretty::FmtWithCtx};
 
 mod parser;
 
@@ -65,6 +65,28 @@ impl Pattern {
         args: Option<&GenericArgs>,
     ) -> bool {
         let mut scrutinee_elems = name.name.as_slice();
+        let mut args = args.cloned();
+        if let [prefix @ .., PathElem::Monomorphized(mono_args)] = scrutinee_elems {
+            // In this case, we may still have some late-bound generics in `args`, this could ONLY happen for regions
+            assert!(
+                args.is_none()
+                    || args.as_ref().unwrap().len() == args.as_ref().unwrap().regions.elem_count(),
+                "In pattern \"{}\" matching against name \"{}\": we have both monomorphized generics {} and regular generics {}",
+                self,
+                name.with_ctx(&ctx.into_fmt()),
+                mono_args.with_ctx(&ctx.into_fmt()),
+                args.unwrap().with_ctx(&ctx.into_fmt())
+            );
+            // We additionally append the regions from `args` to the monomorphized args, so that we can match against them.
+            let mut mono_args = (**mono_args).clone();
+            if let Some(args) = args {
+                // Late-bound regions are appended after the monomorphized ones.
+                mono_args.regions.extend(args.regions.into_iter());
+            }
+            scrutinee_elems = prefix;
+            args = Some(mono_args);
+        };
+        let args = args.as_ref();
         // Patterns that start with an impl block match that impl block anywhere. In such a case we
         // truncate the scrutinee name to start with the rightmost impl in its name. This isn't
         // fully precise in case of impls within impls, but we'll ignore that.

charon/tests/test-rust-name-matcher.rs

@@ -30,9 +30,7 @@ fn parse_pattern_attr(a: &Attribute) -> Option<(bool, Pattern)> {
     }
 }
 
-#[test]
-fn test_name_matcher() -> anyhow::Result<()> {
-    let crate_data = util::translate_rust_text(&std::fs::read_to_string(TEST_FILE)?, &[])?;
+fn test_crate_data(crate_data: &TranslatedCrate) -> anyhow::Result<()> {
     let fmt_ctx = &crate_data.into_fmt();
 
     for item in crate_data.all_items() {
@@ -64,3 +62,12 @@ fn test_name_matcher() -> anyhow::Result<()> {
 
     Ok(())
 }
+
+#[test]
+fn test_name_matcher() -> anyhow::Result<()> {
+    let code = &std::fs::read_to_string(TEST_FILE)?;
+    let crate_data = util::translate_rust_text(code, &[])?;
+    test_crate_data(&crate_data)?;
+    let mono_crate_data = util::translate_rust_text(code, &["--monomorphize"])?;
+    test_crate_data(&mono_crate_data)
+}