From 672ceef25203ebd5fcf5a55e294a4ebfe65648d6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 20 Nov 2023 21:58:25 +0100 Subject: [PATCH] Use the name matcher implemented in Charon --- compiler/Assumed.ml | 2 +- compiler/Extract.ml | 18 +- compiler/ExtractBase.ml | 3 +- compiler/ExtractBuiltin.ml | 394 ++++++++++------------------- compiler/ExtractName.ml | 177 +++++++++++++ compiler/ExtractTypes.ml | 106 ++------ compiler/FunsAnalysis.ml | 10 +- compiler/Interpreter.ml | 2 +- compiler/InterpreterExpressions.ml | 2 +- compiler/LlbcAstUtils.ml | 15 +- compiler/PrintPure.ml | 6 +- compiler/PureUtils.ml | 2 +- compiler/StringUtils.ml | 112 +------- compiler/Substitute.ml | 4 +- compiler/SymbolicAst.ml | 2 +- compiler/SymbolicToPure.ml | 4 +- compiler/Translate.ml | 25 +- compiler/TranslateCore.ml | 48 ++++ compiler/dune | 3 +- 19 files changed, 440 insertions(+), 495 deletions(-) create mode 100644 compiler/ExtractName.ml diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 6aec626a6..48b7ee2b3 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -42,7 +42,7 @@ module Sig = struct let tvar_id_0 = TypeVarId.of_int 0 let tvar_0 : ty = TVar tvar_id_0 let cgvar_id_0 = ConstGenericVarId.of_int 0 - let cgvar_0 : const_generic = CGVar cgvar_id_0 + let cgvar_0 : const_generic = CgVar cgvar_id_0 (** Region 'a of id 0 *) let region_param_0 : region_var = { index = rvar_id_0; name = Some "'a" } diff --git a/compiler/Extract.ml b/compiler/Extract.ml index cd62c15c3..fb3364f4d 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -27,8 +27,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) let builtin = let open ExtractBuiltin in let funs_map = builtin_funs_map () in - let sname = name_to_simple_name def.fwd.f.llbc_name in - SimpleNameMap.find_opt sname funs_map + match_name_find_opt ctx.trans_ctx def.fwd.f.llbc_name funs_map in (* Use the builtin names if necessary *) match builtin with @@ -2024,9 +2023,9 @@ let extract_trait_decl_register_names (ctx : extraction_ctx) (trait_decl : trait_decl) : extraction_ctx = (* Lookup the information if this is a builtin trait *) let open ExtractBuiltin in - let sname = name_to_simple_name trait_decl.llbc_name in let builtin_info = - SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) + match_name_find_opt ctx.trans_ctx trait_decl.llbc_name + (builtin_trait_decls_map ()) in let ctx = let trait_name, trait_constructor = @@ -2061,9 +2060,14 @@ let extract_trait_impl_register_names (ctx : extraction_ctx) (* Check if the trait implementation is builtin *) let builtin_info = let open ExtractBuiltin in - let type_sname = name_to_simple_name trait_impl.llbc_name in - let trait_sname = name_to_simple_name trait_decl.llbc_name in - SimpleNamePairMap.find_opt (type_sname, trait_sname) + (* Lookup the original Rust impl to retrieve the original trait ref (we + use it to derive the name)*) + let trait_impl = + TraitImplId.Map.find trait_impl.def_id ctx.crate.trait_impls + in + let decl_ref = trait_impl.impl_trait in + match_name_with_generics_find_opt ctx.trans_ctx trait_decl.llbc_name + decl_ref.decl_generics (builtin_trait_impls_map ()) in (* Register some builtin information (if necessary) *) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index ae5a9a224..f1ba35a27 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1085,8 +1085,7 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : (* Check if the global corresponds to an assumed global that we should map to a custom definition in our standard library (for instance, happens with "core::num::usize::MAX") *) - let sname = name_to_simple_name def.name in - match SimpleNameMap.find_opt sname builtin_globals_map with + match match_name_find_opt ctx.trans_ctx def.name builtin_globals_map with | Some name -> (* Yes: register the custom binding *) ctx_add decl name ctx diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index db942ff08..d15905a2a 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -5,38 +5,8 @@ *) open Config -open Types - -type simple_name = string list [@@deriving show, ord] - -(* TODO: update *) -let name_to_simple_name (s : name) : simple_name = - (* We simply ignore the disambiguators - TODO: update *) - List.map - (function - | PeIdent (id, _) -> id - | PeImpl i -> - (* TODO *) - show_impl_elem i) - s - -(** Small helper which cuts a string at the occurrences of "::" *) -let string_to_simple_name (s : string) : simple_name = - (* No function to split by using string separator?? *) - let name = String.split_on_char ':' s in - List.filter (fun s -> s <> "") name - -module SimpleNameOrd = struct - type t = simple_name - - let compare = compare_simple_name - let to_string = show_simple_name - let pp_t = pp_simple_name - let show_t = show_simple_name -end - -module SimpleNameMap = Collections.MakeMap (SimpleNameOrd) -module SimpleNameSet = Collections.MakeSet (SimpleNameOrd) +open Charon.NameMatcher (* TODO: include? *) +include ExtractName (* TODO: only open? *) (** Small utility to memoize some computations *) let mk_memoized (f : unit -> 'a) : unit -> 'a = @@ -51,6 +21,9 @@ let mk_memoized (f : unit -> 'a) : unit -> 'a = in g +let split_on_separator (s : string) : string list = + Str.split (Str.regexp "::") s + (** Switch between two values depending on the target backend. We often compute the same value (typically: a name) if the target @@ -62,36 +35,36 @@ let backend_choice (fstar_coq_hol4 : 'a) (lean : 'a) : 'a = let builtin_globals : (string * string) list = [ (* Min *) - ("core::num::usize::MIN", "core_usize_min"); - ("core::num::u8::MIN", "core_u8_min"); - ("core::num::u16::MIN", "core_u16_min"); - ("core::num::u32::MIN", "core_u32_min"); - ("core::num::u64::MIN", "core_u64_min"); - ("core::num::u128::MIN", "core_u128_min"); - ("core::num::isize::MIN", "core_isize_min"); - ("core::num::i8::MIN", "core_i8_min"); - ("core::num::i16::MIN", "core_i16_min"); - ("core::num::i32::MIN", "core_i32_min"); - ("core::num::i64::MIN", "core_i64_min"); - ("core::num::i128::MIN", "core_i128_min"); + ("core::num::{usize}::MIN", "core_usize_min"); + ("core::num::{u8}::MIN", "core_u8_min"); + ("core::num::{u16}::MIN", "core_u16_min"); + ("core::num::{u32}::MIN", "core_u32_min"); + ("core::num::{u64}::MIN", "core_u64_min"); + ("core::num::{u128}::MIN", "core_u128_min"); + ("core::num::{isize}::MIN", "core_isize_min"); + ("core::num::{i8}::MIN", "core_i8_min"); + ("core::num::{i16}::MIN", "core_i16_min"); + ("core::num::{i32}::MIN", "core_i32_min"); + ("core::num::{i64}::MIN", "core_i64_min"); + ("core::num::{i128}::MIN", "core_i128_min"); (* Max *) - ("core::num::usize::MAX", "core_usize_max"); - ("core::num::u8::MAX", "core_u8_max"); - ("core::num::u16::MAX", "core_u16_max"); - ("core::num::u32::MAX", "core_u32_max"); - ("core::num::u64::MAX", "core_u64_max"); - ("core::num::u128::MAX", "core_u128_max"); - ("core::num::isize::MAX", "core_isize_max"); - ("core::num::i8::MAX", "core_i8_max"); - ("core::num::i16::MAX", "core_i16_max"); - ("core::num::i32::MAX", "core_i32_max"); - ("core::num::i64::MAX", "core_i64_max"); - ("core::num::i128::MAX", "core_i128_max"); + ("core::num::{usize}::MAX", "core_usize_max"); + ("core::num::{u8}::MAX", "core_u8_max"); + ("core::num::{u16}::MAX", "core_u16_max"); + ("core::num::{u32}::MAX", "core_u32_max"); + ("core::num::{u64}::MAX", "core_u64_max"); + ("core::num::{u128}::MAX", "core_u128_max"); + ("core::num::{isize}::MAX", "core_isize_max"); + ("core::num::{i8}::MAX", "core_i8_max"); + ("core::num::{i16}::MAX", "core_i16_max"); + ("core::num::{i32}::MAX", "core_i32_max"); + ("core::num::{i64}::MAX", "core_i64_max"); + ("core::num::{i128}::MAX", "core_i128_max"); ] -let builtin_globals_map : string SimpleNameMap.t = - SimpleNameMap.of_list - (List.map (fun (x, y) -> (string_to_simple_name x, y)) builtin_globals) +let builtin_globals_map : string NameMatcherMap.t = + NameMatcherMap.of_list + (List.map (fun (x, y) -> (parse_pattern x, y)) builtin_globals) type builtin_variant_info = { fields : (string * string) list } [@@deriving show] @@ -111,7 +84,7 @@ type builtin_type_body_info = [@@deriving show] type builtin_type_info = { - rust_name : string list; + rust_name : pattern; extract_name : string; keep_params : bool list option; (** We might want to filter some of the type parameters. @@ -143,11 +116,11 @@ let mk_struct_constructor (type_name : string) : string = a type parameter for the allocator to use, which we want to filter. *) let builtin_types () : builtin_type_info list = - let mk_type (rust_name : string list) ?(keep_params : bool list option = None) + let mk_type (rust_name : string) ?(keep_params : bool list option = None) ?(kind : type_variant_kind = KOpaque) () : builtin_type_info = let extract_name = let sep = backend_choice "_" "." in - String.concat sep rust_name + String.concat sep (split_on_separator rust_name) in let body_info : builtin_type_body_info option = match kind with @@ -166,17 +139,17 @@ let builtin_types () : builtin_type_info list = Some (Struct (constructor, fields)) | KEnum -> raise (Failure "TODO") in + let rust_name = parse_pattern rust_name in { rust_name; extract_name; keep_params; body_info } in [ (* Alloc *) - mk_type [ "alloc"; "alloc"; "Global" ] (); + mk_type "alloc::alloc::Global" (); (* Vec *) - mk_type [ "alloc"; "vec"; "Vec" ] ~keep_params:(Some [ true; false ]) (); + mk_type "alloc::vec::Vec" ~keep_params:(Some [ true; false ]) (); (* Range *) - mk_type - [ "core"; "ops"; "range"; "Range" ] + mk_type "core::ops::range::Range" ~kind:(KStruct [ ("start", "start"); ("end", "end_") ]) (); (* Option @@ -185,7 +158,7 @@ let builtin_types () : builtin_type_info list = the target backend. *) { - rust_name = [ "core"; "option"; "Option" ]; + rust_name = parse_pattern "core::option::Option"; extract_name = (match !backend with | Lean -> "Option" @@ -218,7 +191,7 @@ let builtin_types () : builtin_type_info list = ] let mk_builtin_types_map () = - SimpleNameMap.of_list + NameMatcherMap.of_list (List.map (fun info -> (info.rust_name, info)) (builtin_types ())) let builtin_types_map = mk_memoized mk_builtin_types_map @@ -235,15 +208,22 @@ type builtin_fun_info = { parameters. For instance, in the case of the `Vec` functions, there is a type parameter for the allocator to use, which we want to filter. *) -let builtin_funs () : - (string list * bool list option * builtin_fun_info list) list = +let builtin_funs () : (pattern * bool list option * builtin_fun_info list) list + = let rg0 = Some Types.RegionGroupId.zero in (* Small utility *) - let mk_fun (name : string list) (extract_name : string list option) + let mk_fun (rust_name : string) (extract_name : string option) (filter : bool list option) (with_back : bool) (back_no_suffix : bool) : - string list * bool list option * builtin_fun_info list = + pattern * bool list option * builtin_fun_info list = + let rust_name = + try parse_pattern rust_name + with Failure _ -> + raise (Failure ("Could not parse pattern: " ^ rust_name)) + in let extract_name = - match extract_name with None -> name | Some name -> name + match extract_name with + | None -> pattern_to_fun_extract_name rust_name + | Some name -> split_on_separator name in let basename = match !backend with @@ -257,103 +237,55 @@ let builtin_funs () : if with_back then [ { rg = rg0; extract_name = basename ^ back_suffix } ] else [] in - (name, filter, fwd @ back) + (rust_name, filter, fwd @ back) in [ - mk_fun [ "core"; "mem"; "replace" ] None None true false; - mk_fun [ "alloc"; "vec"; "Vec"; "new" ] None None false false; - mk_fun - [ "alloc"; "vec"; "Vec"; "push" ] - None + mk_fun "core::mem::replace" None None true false; + mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::new" None None false false; + mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::push" None (Some [ true; false ]) true true; - mk_fun - [ "alloc"; "vec"; "Vec"; "insert" ] - None + mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::insert" None (Some [ true; false ]) true true; - mk_fun - [ "alloc"; "vec"; "Vec"; "len" ] - None + mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::len" None (Some [ true; false ]) true false; - mk_fun - [ "alloc"; "vec"; "Vec"; "index" ] - None + mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::index" None (Some [ true; true; false ]) true false; - mk_fun - [ "alloc"; "vec"; "Vec"; "index_mut" ] - None + mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::index_mut" None (Some [ true; true; false ]) true false; - mk_fun - [ "alloc"; "boxed"; "Box"; "deref" ] - None + mk_fun "alloc::boxed::{Box<@T>}::deref" None (Some [ true; false ]) true false; - mk_fun - [ "alloc"; "boxed"; "Box"; "deref_mut" ] - None + mk_fun "alloc::boxed::{Box<@T>}::deref_mut" None (Some [ true; false ]) true false; - (* TODO: fix the same like "[T]" below *) - mk_fun - [ "core"; "slice"; "index"; "[T]"; "index" ] - (Some [ "core"; "slice"; "index"; "Slice"; "index" ]) - None true false; - mk_fun - [ "core"; "slice"; "index"; "[T]"; "index_mut" ] - (Some [ "core"; "slice"; "index"; "Slice"; "index_mut" ]) - None true false; - mk_fun - [ "core"; "array"; "[T; N]"; "index" ] - (Some [ "core"; "array"; "Array"; "index" ]) - None true false; - mk_fun - [ "core"; "array"; "[T; N]"; "index_mut" ] - (Some [ "core"; "array"; "Array"; "index_mut" ]) - None true false; - mk_fun [ "core"; "slice"; "index"; "Range"; "get" ] None None true false; - mk_fun [ "core"; "slice"; "index"; "Range"; "get_mut" ] None None true false; - mk_fun [ "core"; "slice"; "index"; "Range"; "index" ] None None true false; - mk_fun - [ "core"; "slice"; "index"; "Range"; "index_mut" ] - None None true false; - mk_fun - [ "core"; "slice"; "index"; "Range"; "get_unchecked" ] - None None false false; - mk_fun - [ "core"; "slice"; "index"; "Range"; "get_unchecked_mut" ] - None None false false; - mk_fun - [ "core"; "slice"; "index"; "usize"; "get" ] - (Some [ "core"; "slice"; "index"; "Usize"; "get" ]) - None true false; - mk_fun - [ "core"; "slice"; "index"; "usize"; "get_mut" ] - (Some [ "core"; "slice"; "index"; "Usize"; "get_mut" ]) - None true false; - mk_fun - [ "core"; "slice"; "index"; "usize"; "get_unchecked" ] - (Some [ "core"; "slice"; "index"; "Usize"; "get_unchecked" ]) - None false false; - mk_fun - [ "core"; "slice"; "index"; "usize"; "get_unchecked_mut" ] - (Some [ "core"; "slice"; "index"; "Usize"; "get_unchecked_mut" ]) - None false false; - mk_fun - [ "core"; "slice"; "index"; "usize"; "index" ] - (Some [ "core"; "slice"; "index"; "Usize"; "index" ]) - None true false; - mk_fun - [ "core"; "slice"; "index"; "usize"; "index_mut" ] - (Some [ "core"; "slice"; "index"; "Usize"; "index_mut" ]) - None true false; + mk_fun "core::slice::index::{[@T]}::index" None None true false; + mk_fun "core::slice::index::{[@T]}::index_mut" None None true false; + mk_fun "core::array::{[@T; @C]}::index" None None true false; + mk_fun "core::array::{[@T; @C]}::index_mut" None None true false; + mk_fun "core::slice::index::{Range<@T>}::get" None None true false; + mk_fun "core::slice::index::{Range<@T>}::get_mut" None None true false; + mk_fun "core::slice::index::{Range<@T>}::index" None None true false; + mk_fun "core::slice::index::{Range<@T>}::index_mut" None None true false; + mk_fun "core::slice::index::{Range<@T>}::get_unchecked" None None false + false; + mk_fun "core::slice::index::{Range<@T>}::get_unchecked_mut" None None false + false; + mk_fun "core::slice::index::{usize}::get" None None true false; + mk_fun "core::slice::index::{usize}::get_mut" None None true false; + mk_fun "core::slice::index::{usize}::get_unchecked" None None false false; + mk_fun "core::slice::index::{usize}::get_unchecked_mut" None None false + false; + mk_fun "core::slice::index::{usize}::index" None None true false; + mk_fun "core::slice::index::{usize}::index_mut" None None true false; ] let mk_builtin_funs_map () = - SimpleNameMap.of_list + NameMatcherMap.of_list (List.map (fun (name, filter, info) -> (name, (filter, info))) (builtin_funs ())) @@ -385,17 +317,22 @@ let builtin_fun_effects = let int_funs = List.map (fun int_name -> - List.map (fun op -> "core::num::" ^ int_name ^ "::" ^ op) int_ops) + List.map + (fun op -> + "core::num::" ^ "{" + ^ StringUtils.capitalize_first_letter int_name + ^ "}::" ^ op) + int_ops) int_names in let int_funs = List.concat int_funs in let no_fail_no_state_funs = [ (* TODO: redundancy with the funs information below *) - "alloc::vec::Vec::new"; - "alloc::vec::Vec::len"; - "alloc::boxed::Box::deref"; - "alloc::boxed::Box::deref_mut"; + "alloc::vec::{alloc::vec::Vec<@T>}::new"; + "alloc::vec::{alloc::vec::Vec<@T>}::len"; + "alloc::boxed::{Box<@T>}::deref"; + "alloc::boxed::{Box<@T>}::deref_mut"; "core::mem::replace"; "core::mem::take"; ] @@ -409,10 +346,10 @@ let builtin_fun_effects = let no_state_funs = [ (* TODO: redundancy with the funs information below *) - "alloc::vec::Vec::push"; - "alloc::vec::Vec::index"; - "alloc::vec::Vec::index_mut"; - "alloc::vec::Vec::index_mut_back"; + "alloc::vec::{alloc::vec::Vec<@T>}::push"; + "alloc::vec::{alloc::vec::Vec<@T>}::index"; + "alloc::vec::{alloc::vec::Vec<@T>}::index_mut"; + "alloc::vec::{alloc::vec::Vec<@T>}::index_mut_back"; ] in let no_state_funs = @@ -421,11 +358,11 @@ let builtin_fun_effects = no_fail_no_state_funs @ no_state_funs let builtin_fun_effects_map = - SimpleNameMap.of_list - (List.map (fun (n, x) -> (string_to_simple_name n, x)) builtin_fun_effects) + NameMatcherMap.of_list + (List.map (fun (n, x) -> (parse_pattern n, x)) builtin_fun_effects) type builtin_trait_decl_info = { - rust_name : string; + rust_name : pattern; extract_name : string; constructor : string; parent_clauses : string list; @@ -441,13 +378,15 @@ type builtin_trait_decl_info = { let builtin_trait_decls_info () = let rg0 = Some Types.RegionGroupId.zero in - let mk_trait (rust_name : string list) ?(extract_name : string option = None) + let mk_trait (rust_name : string) ?(extract_name : string option = None) ?(parent_clauses : string list = []) ?(types : string list = []) ?(methods : (string * bool) list = []) () : builtin_trait_decl_info = + let rust_name = parse_pattern rust_name in let extract_name = match extract_name with | Some n -> n | None -> ( + let rust_name = pattern_to_fun_extract_name rust_name in match !backend with | Coq | FStar | HOL4 -> String.concat "_" rust_name | Lean -> String.concat "." rust_name) @@ -487,7 +426,6 @@ let builtin_trait_decls_info () = in List.map mk_method methods in - let rust_name = String.concat "::" rust_name in { rust_name; extract_name; @@ -500,34 +438,27 @@ let builtin_trait_decls_info () = in [ (* Deref *) - mk_trait - [ "core"; "ops"; "deref"; "Deref" ] - ~types:[ "Target" ] + mk_trait "core::ops::deref::Deref" ~types:[ "Target" ] ~methods:[ ("deref", true) ] (); (* DerefMut *) - mk_trait - [ "core"; "ops"; "deref"; "DerefMut" ] + mk_trait "core::ops::deref::DerefMut" ~parent_clauses:[ backend_choice "deref_inst" "derefInst" ] ~methods:[ ("deref_mut", true) ] (); (* Index *) - mk_trait - [ "core"; "ops"; "index"; "Index" ] - ~types:[ "Output" ] + mk_trait "core::ops::index::Index" ~types:[ "Output" ] ~methods:[ ("index", true) ] (); (* IndexMut *) - mk_trait - [ "core"; "ops"; "index"; "IndexMut" ] + mk_trait "core::ops::index::IndexMut" ~parent_clauses:[ backend_choice "index_inst" "indexInst" ] ~methods:[ ("index_mut", true) ] (); (* Sealed *) - mk_trait [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] (); + mk_trait "core::slice::index::private_slice_index::Sealed" (); (* SliceIndex *) - mk_trait - [ "core"; "slice"; "index"; "SliceIndex" ] + mk_trait "core::slice::index::SliceIndex" ~parent_clauses:[ backend_choice "sealed_inst" "sealedInst" ] ~types:[ "Output" ] ~methods: @@ -543,113 +474,56 @@ let builtin_trait_decls_info () = ] let mk_builtin_trait_decls_map () = - SimpleNameMap.of_list + NameMatcherMap.of_list (List.map - (fun info -> (string_to_simple_name info.rust_name, info)) + (fun info -> (info.rust_name, info)) (builtin_trait_decls_info ())) let builtin_trait_decls_map = mk_memoized mk_builtin_trait_decls_map -(* TODO: generalize this. - - For now, the key is: - - name of the impl (ex.: "alloc.boxed.Boxed") - - name of the implemented trait (ex.: "core.ops.deref.Deref" -*) -type simple_name_pair = simple_name * simple_name [@@deriving show, ord] - -module SimpleNamePairOrd = struct - type t = simple_name_pair - - let compare = compare_simple_name_pair - let to_string = show_simple_name_pair - let pp_t = pp_simple_name_pair - let show_t = show_simple_name_pair -end - -module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd) - -let builtin_trait_impls_info () : - ((string list * string list) * (bool list option * string)) list = - let fmt (type_name : string list) - ?(extract_type_name : string list option = None) - (trait_name : string list) ?(filter : bool list option = None) () : - (string list * string list) * (bool list option * string) = +let builtin_trait_impls_info () : (pattern * (bool list option * string)) list = + let fmt (rust_name : string) ?(filter : bool list option = None) () : + pattern * (bool list option * string) = + let rust_name = parse_pattern rust_name in let name = - let trait_name = String.concat "" trait_name ^ "Inst" in + let name = pattern_to_trait_impl_extract_name rust_name in let sep = backend_choice "_" "." in - let type_name = - match extract_type_name with - | Some type_name -> type_name - | None -> type_name - in - String.concat sep type_name ^ sep ^ trait_name + String.concat sep name in - ((type_name, trait_name), (filter, name)) + (rust_name, (filter, name)) in - (* TODO: fix the names like "[T]" below *) [ (* core::ops::Deref> *) - fmt [ "alloc"; "boxed"; "Box" ] [ "core"; "ops"; "deref"; "Deref" ] (); - (* core::ops::DerefMut> *) - fmt [ "alloc"; "boxed"; "Box" ] [ "core"; "ops"; "deref"; "DerefMut" ] (); + fmt "core::ops::Deref>" (); + (* core::ops::Deref> *) + fmt "core::ops::Deref>" (); (* core::ops::index::Index<[T], I> *) - fmt - [ "core"; "slice"; "index"; "[T]" ] - ~extract_type_name:(Some [ "core"; "slice"; "index"; "Slice" ]) - [ "core"; "ops"; "index"; "Index" ] - (); + fmt "core::ops::index::Index<[@T], @I>" (); (* core::ops::index::IndexMut<[T], I> *) - fmt - [ "core"; "slice"; "index"; "[T]" ] - ~extract_type_name:(Some [ "core"; "slice"; "index"; "Slice" ]) - [ "core"; "ops"; "index"; "IndexMut" ] - (); + fmt "core::ops::index::IndexMut<[@T], @I>" (); (* core::slice::index::private_slice_index::Sealed> *) - fmt - [ "core"; "slice"; "index"; "private_slice_index"; "Range" ] - [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] - (); + fmt "core::slice::index::private_slice_index::Sealed>" (); (* core::slice::index::SliceIndex, [T]> *) - fmt - [ "core"; "slice"; "index"; "Range" ] - [ "core"; "slice"; "index"; "SliceIndex" ] - (); + fmt "core::slice::index::SliceIndex, [@T]>" (); (* core::ops::index::Index<[T; N], I> *) - fmt - [ "core"; "array"; "[T; N]" ] - ~extract_type_name:(Some [ "core"; "array"; "Array" ]) - [ "core"; "ops"; "index"; "Index" ] - (); + fmt "core::ops::index::Index<[@T; @N], @I>" (); (* core::ops::index::IndexMut<[T; N], I> *) - fmt - [ "core"; "array"; "[T; N]" ] - ~extract_type_name:(Some [ "core"; "array"; "Array" ]) - [ "core"; "ops"; "index"; "IndexMut" ] - (); + fmt "core::ops::index::IndexMut<[@T; @N], @I>" (); (* core::slice::index::private_slice_index::Sealed *) - fmt - [ "core"; "slice"; "index"; "private_slice_index"; "usize" ] - [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] - (); + fmt "core::slice::index::private_slice_index::Sealed" (); (* core::slice::index::SliceIndex *) - fmt - [ "core"; "slice"; "index"; "usize" ] - [ "core"; "slice"; "index"; "SliceIndex" ] - (); - (* core::ops::index::Index, T> *) - fmt [ "alloc"; "vec"; "Vec" ] - [ "core"; "ops"; "index"; "Index" ] + fmt "core::slice::index::SliceIndex" (); + (* core::ops::index::Index, T> *) + fmt "core::ops::index::Index, @T>" ~filter:(Some [ true; true; false ]) (); - (* core::ops::index::IndexMut, T> *) - fmt [ "alloc"; "vec"; "Vec" ] - [ "core"; "ops"; "index"; "IndexMut" ] + (* core::ops::index::IndexMut, T> *) + fmt "core::ops::index::IndexMut, @T>" ~filter:(Some [ true; true; false ]) (); ] let mk_builtin_trait_impls_map () = - SimpleNamePairMap.of_list (builtin_trait_impls_info ()) + NameMatcherMap.of_list (builtin_trait_impls_info ()) let builtin_trait_impls_map = mk_memoized mk_builtin_trait_impls_map diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml new file mode 100644 index 000000000..4f5ca0d16 --- /dev/null +++ b/compiler/ExtractName.ml @@ -0,0 +1,177 @@ +(** Utilities for extracting names *) + +open Charon.NameMatcher + +module NameMatcherMap = struct + type 'a t = (pattern * 'a) list + + let config = { map_vars_to_vars = true } + + let find_opt (ctx : ctx) (name : Types.name) (m : 'a t) : 'a option = + match List.find_opt (fun (pat, _) -> match_name ctx config pat name) m with + | None -> None + | Some (_, v) -> Some v + + let find_with_generics_opt (ctx : ctx) (name : Types.name) + (g : Types.generic_args) (m : 'a t) : 'a option = + match + List.find_opt + (fun (pat, _) -> match_name_with_generics ctx config pat name g) + m + with + | None -> None + | Some (_, v) -> Some v + + let mem (ctx : ctx) (name : Types.name) (m : 'a t) : bool = + find_opt ctx name m <> None + + let of_list (ls : (pattern * 'a) list) : 'a t = ls +end + +(** Helper to convert name patterns to names for extraction. + + For impl blocks, we simply use the name of the type (without its arguments) + if all the arguments are variables. + *) +let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) : + string list = + let c = { tgt_kind = TkName } in + let is_var (g : generic_arg) : bool = + match g with + | GExpr (EVar _) -> true + | GRegion (RVar _) -> true + | _ -> false + in + let all_vars = List.for_all is_var in + let elem_to_string (e : pattern_elem) : string = + match e with + | PIdent _ -> pattern_elem_to_string c e + | PImpl ty -> ( + match ty with + | EComp id -> ( + (* Retrieve the last ident *) + let id = Collections.List.last id in + match id with + | PIdent (s, g) -> + if all_vars g then s else pattern_elem_to_string c id + | PImpl _ -> raise (Failure "Unreachable")) + | EPrimAdt (adt, g) -> + if all_vars g then + match adt with + | TTuple -> + let l = List.length g in + if l = 2 then "Pair" else expr_to_string c ty + | TArray -> "Array" + | TSlice -> "Slice" + else expr_to_string c ty + | ERef _ | EVar _ -> raise (Failure "")) + in + let rec pattern_to_string (n : pattern) : string list = + match n with + | [] -> raise (Failure "Unreachable") + | [ e ] -> + let e = elem_to_string e in + if is_trait_impl then [ e ^ "Inst" ] else [ e ] + | e :: n -> elem_to_string e :: pattern_to_string n + in + pattern_to_string name + +let pattern_to_fun_extract_name = pattern_to_extract_name false +let pattern_to_trait_impl_extract_name = pattern_to_extract_name true + +(* TODO: this is provisional. We just want to make sure that the extraction + names we derive from the patterns (for the builtin definitions) are + consistent with the extraction names we derive from the Rust names *) +let name_to_simple_name (ctx : ctx) (n : Types.name) : string list = + pattern_to_extract_name false (name_to_pattern ctx n) + +let name_with_generics_to_simple_name (ctx : ctx) (n : Types.name) + (p : Types.generic_params) (g : Types.generic_args) : string list = + pattern_to_extract_name true (name_with_generics_to_pattern ctx n p g) + +(* + (* Prepare a name. + The first id elem is always the crate: if it is the local crate, + we remove it. We ignore disambiguators (there may be collisions, but we + check if there are). + *) + let rec name_to_simple_name (name : llbc_name) : string list = + (* Rmk.: initially we only filtered the disambiguators equal to 0 *) + match name with + | (PeIdent (crate, _) as id) :: name -> + let name = if crate = crate_name then name else id :: name in + let open Types in + let name = + List.map + (function + | PeIdent (s, _) -> s + | PeImpl impl -> impl_elem_to_simple_name impl) + name + in + name + | _ -> + raise + (Failure + ("Unexpected name shape: " ^ TranslateCore.name_to_string ctx name)) + and impl_elem_to_simple_name (impl : Types.impl_elem) : string = + (* We do something simple for now. + TODO: we might want to do something different for impl elements which are + actually trait implementations, in order to prevent name collisions (it + is possible to define several times the same trait for the same type, + but with different instantiations of the type, or different trait + requirements *) + ty_to_simple_name impl.generics impl.ty + and ty_to_simple_name (generics : Types.generic_params) (ty : Types.ty) : + string = + (* We do something simple for now. + TODO: find a more principled way of converting types to names. + In particular, we might want to do something different for impl elements which are + actually trait implementations, in order to prevent name collisions (it + is possible to define several times the same trait for the same type, + but with different instantiations of the type, or different trait + requirements *) + match ty with + | TAdt (id, args) -> ( + match id with + | TAdtId id -> + let def = TypeDeclId.Map.find id ctx.type_ctx.type_decls in + name_last_elem_as_ident def.name + | TTuple -> + (* TODO *) + "Tuple" + ^ String.concat "" + (List.map (ty_to_simple_name generics) args.types) + | TAssumed id -> ( + match id with + | Types.TBox -> "Box" + | Types.TArray -> "Array" + | Types.TSlice -> "Slice" + | Types.TStr -> "Str")) + | TVar vid -> + (* Use the variable name *) + (List.find (fun (v : type_var) -> v.index = vid) generics.types).name + | TLiteral lty -> + StringUtils.capitalize_first_letter + (Print.Types.literal_type_to_string lty) + | TNever -> raise (Failure "Unreachable") + | TRef (_, rty, rk) -> ( + let rty = ty_to_simple_name generics rty in + match rk with + | RMut -> "MutBorrow" ^ rty + | RShared -> "SharedBorrow" ^ rty) + | TRawPtr (rty, rk) -> ( + let rty = ty_to_simple_name generics rty in + match rk with RMut -> "MutPtr" ^ rty | RShared -> "ConstPtr" ^ rty) + | TTraitType (tr, _, name) -> + (* TODO: this is way too simple *) + let trait_decl = + TraitDeclId.Map.find tr.trait_decl_ref.trait_decl_id + ctx.trait_decls_ctx.trait_decls + in + name_last_elem_as_ident trait_decl.name ^ name + | TArrow (inputs, output) -> + "Arrow" + ^ String.concat "" + (List.map (ty_to_simple_name generics) (inputs @ [ output ])) + in +*) diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index de4ec735b..a74bd5324 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -586,84 +586,16 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) we remove it. We ignore disambiguators (there may be collisions, but we check if there are). *) - let rec name_to_simple_name (name : llbc_name) : string list = + let name_to_simple_name (name : llbc_name) : string list = (* Rmk.: initially we only filtered the disambiguators equal to 0 *) match name with | (PeIdent (crate, _) as id) :: name -> let name = if crate = crate_name then name else id :: name in - let open Types in - let name = - List.map - (function - | PeIdent (s, _) -> s - | PeImpl impl -> impl_elem_to_simple_name impl) - name - in - name + name_to_simple_name ctx name | _ -> raise (Failure ("Unexpected name shape: " ^ TranslateCore.name_to_string ctx name)) - and impl_elem_to_simple_name (impl : Types.impl_elem) : string = - (* We do something simple for now. - TODO: we might want to do something different for impl elements which are - actually trait implementations, in order to prevent name collisions (it - is possible to define several times the same trait for the same type, - but with different instantiations of the type, or different trait - requirements *) - ty_to_simple_name impl.generics impl.ty - and ty_to_simple_name (generics : Types.generic_params) (ty : Types.ty) : - string = - (* We do something simple for now. - TODO: find a more principled way of converting types to names. - In particular, we might want to do something different for impl elements which are - actually trait implementations, in order to prevent name collisions (it - is possible to define several times the same trait for the same type, - but with different instantiations of the type, or different trait - requirements *) - match ty with - | TAdt (id, args) -> ( - match id with - | TAdtId id -> - let def = TypeDeclId.Map.find id ctx.type_ctx.type_decls in - name_last_elem_as_ident def.name - | TTuple -> - (* TODO *) - "Tuple" - ^ String.concat "" - (List.map (ty_to_simple_name generics) args.types) - | TAssumed id -> ( - match id with - | Types.TBox -> "Box" - | Types.TArray -> "Array" - | Types.TSlice -> "Slice" - | Types.TStr -> "Str")) - | TVar vid -> - (* Use the variable name *) - (List.find (fun (v : type_var) -> v.index = vid) generics.types).name - | TLiteral lty -> - StringUtils.capitalize_first_letter - (Print.Types.literal_type_to_string lty) - | TNever -> raise (Failure "Unreachable") - | TRef (_, rty, rk) -> ( - let rty = ty_to_simple_name generics rty in - match rk with - | RMut -> "MutBorrow" ^ rty - | RShared -> "SharedBorrow" ^ rty) - | TRawPtr (rty, rk) -> ( - let rty = ty_to_simple_name generics rty in - match rk with RMut -> "MutPtr" ^ rty | RShared -> "ConstPtr" ^ rty) - | TTraitType (tr, _, name) -> - (* TODO: this is way too simple *) - let trait_decl = - TraitDeclId.Map.find tr.trait_decl_ref.trait_decl_id - ctx.trait_decls_ctx.trait_decls - in - name_last_elem_as_ident trait_decl.name ^ name - | TArrow (inputs, output) -> - "Arrow" - ^ String.concat "" - (List.map (ty_to_simple_name generics) (inputs @ [ output ])) in let flatten_name (name : string list) : string = match !backend with @@ -747,17 +679,22 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) let trait_impl_name (trait_decl : trait_decl) (trait_impl : trait_impl) : string = - (* TODO: provisional: we concatenate the trait impl name (which is its type) - with the trait decl name *) - let trait_decl = - let name = trait_decl.llbc_name in - let name = get_type_name_no_suffix name ^ "Inst" in - (* Remove the occurrences of '.' *) - String.concat "" (String.split_on_char '.' name) - in + (* We derive the trait impl name from the implemented trait. + For instance, if this implementation is an instance of `trait::Trait` + for ``, we generate the name: "trait.TraitFooFooU32Inst". + Importantly, it is to be noted that the name is independent of the place + where the instance has been defined (it is indepedent of the file, etc.). + *) let name = - flatten_name (get_type_name trait_impl.llbc_name @ [ trait_decl ]) + (* We need to lookup the LLBC definitions, to have the original instantiation *) + let trait_impl = + TraitImplId.Map.find trait_impl.def_id ctx.trait_impls_ctx.trait_impls + in + let params = trait_impl.generics in + let args = trait_impl.impl_trait.decl_generics in + name_with_generics_to_simple_name ctx trait_decl.llbc_name params args in + let name = flatten_name name in match !backend with | FStar -> StringUtils.lowercase_first_letter name | Coq | HOL4 | Lean -> name @@ -1185,11 +1122,11 @@ let extract_arrow (fmt : F.formatter) () : unit = let extract_const_generic (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (cg : const_generic) : unit = match cg with - | CGGlobal id -> + | CgGlobal id -> let s = ctx_get_global id ctx in F.pp_print_string fmt s - | CGValue v -> ctx.fmt.extract_literal fmt inside v - | CGVar id -> + | CgValue v -> ctx.fmt.extract_literal fmt inside v + | CgVar id -> let s = ctx_get_const_generic_var id ctx in F.pp_print_string fmt s @@ -1492,8 +1429,9 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : extraction_ctx = (* Lookup the builtin information, if there is *) let open ExtractBuiltin in - let sname = name_to_simple_name def.llbc_name in - let info = SimpleNameMap.find_opt sname (builtin_types_map ()) in + let info = + match_name_find_opt ctx.trans_ctx def.llbc_name (builtin_types_map ()) + in (* Register the filtering information, if there is *) let ctx = match info with diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index a07ad35ae..9ae6ce867 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -58,6 +58,13 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let can_diverge = ref false in let is_rec = ref false in let group_has_builtin_info = ref false in + let name_matcher_ctx : Charon.NameMatcher.ctx = + { + type_decls = m.type_decls; + global_decls = m.global_decls; + trait_decls = m.trait_decls; + } + in (* We have some specialized knowledge of some library functions; we don't have any more custom treatment than this, and these functions can be modeled @@ -65,8 +72,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) way. *) let get_builtin_info (f : fun_decl) : ExtractBuiltin.effect_info option = let open ExtractBuiltin in - let name = name_to_simple_name f.name in - SimpleNameMap.find_opt name builtin_fun_effects_map + NameMatcherMap.find_opt name_matcher_ctx f.name builtin_fun_effects_map in (* JP: Why not use a reduce visitor here with a tuple of the values to be diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 5b2db90d2..c2e47da90 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -80,7 +80,7 @@ let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig) let regions = List.map (fun _ -> RErased) regions in let types = List.map (fun (v : type_var) -> TVar v.index) types in let const_generics = - List.map (fun (v : const_generic_var) -> CGVar v.index) const_generics + List.map (fun (v : const_generic_var) -> CgVar v.index) const_generics in (* Annoying that we have to generate this substitution here *) let r_subst _ = raise (Failure "Unexpected region") in diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 1e28fd4b0..38620be07 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -321,7 +321,7 @@ let eval_operand_no_reorganize (config : config) (op : operand) ( ctx0, None, value_as_symbolic v.value, - SymbolicAst.VaCGValue vid, + SymbolicAst.VaCgValue vid, e ))) | CFnPtr _ -> raise (Failure "TODO")) | Copy p -> diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 012161579..ffdce4810 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -31,21 +31,26 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : type_decl list * fun_decl list = let open ExtractBuiltin in + let ctx : Charon.NameMatcher.ctx = + { + type_decls = k.type_decls; + global_decls = k.global_decls; + trait_decls = k.trait_decls; + } + in let is_opaque_fun (d : fun_decl) : bool = - let sname = name_to_simple_name d.name in d.body = None (* Something to pay attention to: we must ignore trait method *declarations* (which don't have a body but must not be considered as opaque) *) && (match d.kind with TraitMethodDecl _ -> false | _ -> true) && ((not filter_assumed) - || (not (SimpleNameMap.mem sname builtin_globals_map)) - && not (SimpleNameMap.mem sname (builtin_funs_map ()))) + || (not (NameMatcherMap.mem ctx d.name builtin_globals_map)) + && not (NameMatcherMap.mem ctx d.name (builtin_funs_map ()))) in let is_opaque_type (d : type_decl) : bool = - let sname = name_to_simple_name d.name in d.kind = Opaque && ((not filter_assumed) - || not (SimpleNameMap.mem sname (builtin_types_map ()))) + || not (NameMatcherMap.mem ctx d.name (builtin_types_map ()))) in (* Note that by checking the function bodies we also the globals *) ( List.filter is_opaque_type (TypeDeclId.Map.values k.type_decls), diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index e66869513..a7ec93369 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -128,9 +128,9 @@ let type_id_to_string (env : fmt_env) (id : type_id) : string = (* TODO: duplicates Charon.PrintTypes.const_generic_to_string *) let const_generic_to_string (env : fmt_env) (cg : const_generic) : string = match cg with - | CGGlobal id -> global_decl_id_to_string env id - | CGVar id -> const_generic_var_id_to_string env id - | CGValue lit -> literal_to_string lit + | CgGlobal id -> global_decl_id_to_string env id + | CgVar id -> const_generic_var_id_to_string env id + | CgValue lit -> literal_to_string lit let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string = match ty with diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 5f92d18a2..062706211 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -111,7 +111,7 @@ let ty_substitute (subst : subst) (ty : ty) : ty = object inherit [_] map_ty method! visit_TVar _ var_id = subst.ty_subst var_id - method! visit_CGVar _ var_id = subst.cg_subst var_id + method! visit_CgVar _ var_id = subst.cg_subst var_id method! visit_Clause _ id = subst.tr_subst id method! visit_Self _ = subst.tr_self end diff --git a/compiler/StringUtils.ml b/compiler/StringUtils.ml index 161df27bb..3ab4e8088 100644 --- a/compiler/StringUtils.ml +++ b/compiler/StringUtils.ml @@ -1,111 +1 @@ -(** Utilities to work on strings, character per character. - - They operate on ASCII strings, and are used by the project to convert - Rust names: Rust names are not fancy, so it shouldn't be a problem. - - Rk.: the poor support of OCaml for char manipulation is really annoying... - *) - -let code_0 = 48 -let code_9 = 57 -let code_A = 65 -let code_Z = 90 -let code_a = 97 -let code_z = 122 - -let is_lowercase_ascii (c : char) : bool = - let c = Char.code c in - code_a <= c && c <= code_z - -let is_uppercase_ascii (c : char) : bool = - let c = Char.code c in - code_A <= c && c <= code_Z - -let is_letter_ascii (c : char) : bool = - is_lowercase_ascii c || is_uppercase_ascii c - -let is_digit_ascii (c : char) : bool = - let c = Char.code c in - code_0 <= c && c <= code_9 - -let lowercase_ascii = Char.lowercase_ascii -let uppercase_ascii = Char.uppercase_ascii - -(** Using buffers as per: - {{: https://stackoverflow.com/questions/29957418/how-to-convert-char-list-to-string-in-ocaml} stackoverflow} - *) -let string_of_chars (chars : char list) : string = - let buf = Buffer.create (List.length chars) in - List.iter (Buffer.add_char buf) chars; - Buffer.contents buf - -let string_to_chars (s : string) : char list = - let length = String.length s in - let rec apply i = - if i = length then [] else String.get s i :: apply (i + 1) - in - apply 0 - -(** This operates on ASCII *) -let to_camel_case (s : string) : string = - (* Note that we rebuild the string in reverse order *) - let apply ((prev_is_under, acc) : bool * char list) (c : char) : - bool * char list = - if c = '_' then (true, acc) - else - let c = if prev_is_under then uppercase_ascii c else c in - (false, c :: acc) - in - let _, chars = List.fold_left apply (true, []) (string_to_chars s) in - string_of_chars (List.rev chars) - -(** This operates on ASCII *) -let to_snake_case (s : string) : string = - (* Note that we rebuild the string in reverse order *) - let apply ((prev_is_low, prev_is_digit, acc) : bool * bool * char list) - (c : char) : bool * bool * char list = - let acc = - if c = '_' then acc - else if prev_is_digit then if is_letter_ascii c then '_' :: acc else acc - else if prev_is_low then - if (is_lowercase_ascii c || is_digit_ascii c) && c <> '_' then acc - else '_' :: acc - else acc - in - let prev_is_low = is_lowercase_ascii c in - let prev_is_digit = is_digit_ascii c in - let c = lowercase_ascii c in - (prev_is_low, prev_is_digit, c :: acc) - in - let _, _, chars = - List.fold_left apply (false, false, []) (string_to_chars s) - in - string_of_chars (List.rev chars) - -(** Applies a map operation. - - This is very inefficient, but shouldn't be used much. - *) -let map (f : char -> string) (s : string) : string = - let sl = List.map f (string_to_chars s) in - let sl = List.map string_to_chars sl in - string_of_chars (List.concat sl) - -let capitalize_first_letter (s : string) : string = - let s = string_to_chars s in - let s = match s with [] -> s | c :: s' -> uppercase_ascii c :: s' in - string_of_chars s - -let lowercase_first_letter (s : string) : string = - let s = string_to_chars s in - let s = match s with [] -> s | c :: s' -> lowercase_ascii c :: s' in - string_of_chars s - -(** Unit tests *) -let _ = - assert (to_camel_case "hello_world" = "HelloWorld"); - assert (to_snake_case "HelloWorld36Hello" = "hello_world36_hello"); - assert (to_snake_case "HELLO" = "hello"); - assert (to_snake_case "T1" = "t1"); - assert (to_camel_case "list" = "List"); - assert (to_snake_case "is_cons" = "is_cons") +include Charon.StringUtils diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index 01509decf..73e7f71dc 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -29,7 +29,7 @@ let st_substitute_visitor (subst : subst) = (* We should never get here because we reimplemented [visit_TypeVar] *) raise (Failure "Unexpected") - method! visit_CGVar _ id = subst.cg_subst id + method! visit_CgVar _ id = subst.cg_subst id method! visit_const_generic_var_id _ _ = (* We should never get here because we reimplemented [visit_Var] *) @@ -71,7 +71,7 @@ let erase_regions_subst : subst = { r_subst = (fun _ -> RErased); ty_subst = (fun vid -> TVar vid); - cg_subst = (fun id -> CGVar id); + cg_subst = (fun id -> CgVar id); tr_subst = (fun id -> Clause id); tr_self = Self; } diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index 7c5d28a71..c9820ba5b 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -240,7 +240,7 @@ and value_aggregate = | VaSingleValue of typed_value (** Regular case *) | VaArray of typed_value list (** This is used when introducing array aggregates *) - | VaCGValue of const_generic_var_id + | VaCgValue of const_generic_var_id (** This is used when evaluating a const generic value: in the interpreter, we introduce a fresh symbolic value. *) | VaTraitConstValue of trait_ref * generic_args * string diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 7dad54e1a..69ff4df13 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2475,7 +2475,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) { struct_id = TAssumed TArray; init = None; updates = values } in { e = StructUpdate su; ty = var.ty } - | VaCGValue cg_id -> { e = CVar cg_id; ty = var.ty } + | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty } | VaTraitConstValue (trait_ref, generics, const_name) -> let type_infos = ctx.type_context.type_infos in let trait_ref = translate_fwd_trait_ref type_infos trait_ref in @@ -2726,7 +2726,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = let types = List.map (fun (ty : T.type_var) -> TVar ty.T.index) types in let const_generics = List.map - (fun (cg : T.const_generic_var) -> T.CGVar cg.T.index) + (fun (cg : T.const_generic_var) -> T.CgVar cg.T.index) const_generics in let trait_refs = diff --git a/compiler/Translate.ml b/compiler/Translate.ml index cf23fd449..271d19ad3 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -477,8 +477,7 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) let types_map = builtin_types_map () in List.map (fun (def : Pure.type_decl) -> - let sname = name_to_simple_name def.llbc_name in - SimpleNameMap.find_opt sname types_map <> None) + match_name_find_opt ctx.trans_ctx def.llbc_name types_map <> None) defs in @@ -545,9 +544,9 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (* Check if it is a builtin global - if yes, we ignore it because we map the definition to one in the standard library *) let open ExtractBuiltin in - let sname = name_to_simple_name global.name in let extract = - extract && SimpleNameMap.find_opt sname builtin_globals_map = None + extract + && match_name_find_opt ctx.trans_ctx global.name builtin_globals_map = None in if extract then (* We don't wrap global declaration groups between calls to functions @@ -661,8 +660,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let funs_map = builtin_funs_map () in List.map (fun (trans : pure_fun_translation) -> - let sname = name_to_simple_name trans.fwd.f.llbc_name in - SimpleNameMap.find_opt sname funs_map <> None) + match_name_find_opt ctx.trans_ctx trans.fwd.f.llbc_name funs_map <> None) pure_ls in @@ -755,8 +753,11 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config) let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in (* Check if the trait declaration is builtin, in which case we ignore it *) let open ExtractBuiltin in - let sname = name_to_simple_name trait_decl.llbc_name in - if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then ( + if + match_name_find_opt ctx.trans_ctx trait_decl.llbc_name + (builtin_trait_decls_map ()) + = None + then ( let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in if extract_decl then Extract.extract_trait_decl ctx fmt trait_decl; if extract_extra_info then @@ -775,9 +776,11 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config) (* Check if the trait implementation is builtin *) let builtin_info = let open ExtractBuiltin in - let type_sname = name_to_simple_name trait_impl.llbc_name in - let trait_sname = name_to_simple_name trait_decl.llbc_name in - SimpleNamePairMap.find_opt (type_sname, trait_sname) + let trait_impl = + TraitImplId.Map.find trait_impl.def_id ctx.crate.trait_impls + in + match_name_with_generics_find_opt ctx.trans_ctx trait_decl.llbc_name + trait_impl.impl_trait.decl_generics (builtin_trait_impls_map ()) in match builtin_info with diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml index a974cdeec..f251e169d 100644 --- a/compiler/TranslateCore.ml +++ b/compiler/TranslateCore.ml @@ -1,6 +1,7 @@ (** Some utilities for the translation *) open Contexts +open ExtractName (** The local logger *) let log = Logging.translate_log @@ -29,3 +30,50 @@ let trans_ctx_to_pure_fmt_env (ctx : trans_ctx) : PrintPure.fmt_env = let name_to_string (ctx : trans_ctx) = Print.Types.name_to_string (trans_ctx_to_fmt_env ctx) + +let match_name_find_opt (ctx : trans_ctx) (name : Types.name) + (m : 'a NameMatcherMap.t) : 'a option = + let open Charon.NameMatcher in + let open ExtractBuiltin in + let mctx : ctx = + { + type_decls = ctx.type_ctx.type_decls; + global_decls = ctx.global_ctx.global_decls; + trait_decls = ctx.trait_decls_ctx.trait_decls; + } + in + NameMatcherMap.find_opt mctx name m + +let match_name_with_generics_find_opt (ctx : trans_ctx) (name : Types.name) + (generics : Types.generic_args) (m : 'a NameMatcherMap.t) : 'a option = + let open Charon.NameMatcher in + let open ExtractBuiltin in + let mctx : ctx = + { + type_decls = ctx.type_ctx.type_decls; + global_decls = ctx.global_ctx.global_decls; + trait_decls = ctx.trait_decls_ctx.trait_decls; + } + in + NameMatcherMap.find_with_generics_opt mctx name generics m + +let name_to_simple_name (ctx : trans_ctx) (n : Types.name) : string list = + let mctx : Charon.NameMatcher.ctx = + { + type_decls = ctx.type_ctx.type_decls; + global_decls = ctx.global_ctx.global_decls; + trait_decls = ctx.trait_decls_ctx.trait_decls; + } + in + name_to_simple_name mctx n + +let name_with_generics_to_simple_name (ctx : trans_ctx) (n : Types.name) + (p : Types.generic_params) (g : Types.generic_args) : string list = + let mctx : Charon.NameMatcher.ctx = + { + type_decls = ctx.type_ctx.type_decls; + global_decls = ctx.global_ctx.global_decls; + trait_decls = ctx.trait_decls_ctx.trait_decls; + } + in + name_with_generics_to_simple_name mctx n p g diff --git a/compiler/dune b/compiler/dune index 43ce86c84..39ad62608 100644 --- a/compiler/dune +++ b/compiler/dune @@ -10,7 +10,7 @@ (public_name aeneas) ;; The name as revealed to the projects importing this library (preprocess (pps ppx_deriving.show ppx_deriving.ord visitors.ppx)) - (libraries charon core_unix unionFind ocamlgraph) + (libraries charon core_unix unionFind ocamlgraph str) (modules AssociatedTypes Assumed @@ -24,6 +24,7 @@ Extract ExtractBase ExtractBuiltin + ExtractName ExtractTypes FunsAnalysis Identifiers