diff options
Diffstat (limited to 'compiler/ExtractBuiltin.ml')
| -rw-r--r-- | compiler/ExtractBuiltin.ml | 394 |
1 files changed, 134 insertions, 260 deletions
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index db942ff0..d15905a2 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<alloc::boxed::Box<T>> *) - fmt [ "alloc"; "boxed"; "Box" ] [ "core"; "ops"; "deref"; "Deref" ] (); - (* core::ops::DerefMut<alloc::boxed::Box<T>> *) - fmt [ "alloc"; "boxed"; "Box" ] [ "core"; "ops"; "deref"; "DerefMut" ] (); + fmt "core::ops::Deref<Box<@T>>" (); + (* core::ops::Deref<alloc::boxed::Box<T>> *) + fmt "core::ops::Deref<Box<@T>>" (); (* 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<Range<usize>> *) - fmt - [ "core"; "slice"; "index"; "private_slice_index"; "Range" ] - [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] - (); + fmt "core::slice::index::private_slice_index::Sealed<Range<usize>>" (); (* core::slice::index::SliceIndex<Range<usize>, [T]> *) - fmt - [ "core"; "slice"; "index"; "Range" ] - [ "core"; "slice"; "index"; "SliceIndex" ] - (); + fmt "core::slice::index::SliceIndex<Range<usize>, [@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<usize> *) - fmt - [ "core"; "slice"; "index"; "private_slice_index"; "usize" ] - [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] - (); + fmt "core::slice::index::private_slice_index::Sealed<usize>" (); (* core::slice::index::SliceIndex<usize, [T]> *) - fmt - [ "core"; "slice"; "index"; "usize" ] - [ "core"; "slice"; "index"; "SliceIndex" ] - (); - (* core::ops::index::Index<Vec<T>, T> *) - fmt [ "alloc"; "vec"; "Vec" ] - [ "core"; "ops"; "index"; "Index" ] + fmt "core::slice::index::SliceIndex<usize, [@T]>" (); + (* core::ops::index::Index<alloc::vec::Vec<T>, T> *) + fmt "core::ops::index::Index<alloc::vec::Vec<@T>, @T>" ~filter:(Some [ true; true; false ]) (); - (* core::ops::index::IndexMut<Vec<T>, T> *) - fmt [ "alloc"; "vec"; "Vec" ] - [ "core"; "ops"; "index"; "IndexMut" ] + (* core::ops::index::IndexMut<alloc::vec::Vec<T>, T> *) + fmt "core::ops::index::IndexMut<alloc::vec::Vec<@T>, @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 |