diff options
| -rw-r--r-- | src/Assumed.ml | 28 | ||||
| -rw-r--r-- | src/CfimOfJson.ml | 25 | ||||
| -rw-r--r-- | src/ExtractToFStar.ml | 11 | ||||
| -rw-r--r-- | src/Names.ml | 93 | ||||
| -rw-r--r-- | src/Print.ml | 14 |
5 files changed, 114 insertions, 57 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml index 2bf7cd7c..6f53c302 100644 --- a/src/Assumed.ml +++ b/src/Assumed.ml @@ -247,22 +247,28 @@ let assumed_infos : assumed_info list = let vec_pre = [ "alloc"; "vec"; "Vec" ] in let index_pre = [ "core"; "ops"; "index" ] in [ - (Replace, Sig.mem_replace_sig, false, [ "core"; "mem"; "replace" ]); - (BoxNew, Sig.box_new_sig, false, [ "alloc"; "boxed"; "Box"; "new" ]); - (BoxDeref, Sig.box_deref_shared_sig, false, deref_pre @ [ "Deref"; "deref" ]); + (A.Replace, Sig.mem_replace_sig, false, to_name [ "core"; "mem"; "replace" ]); + (BoxNew, Sig.box_new_sig, false, to_name [ "alloc"; "boxed"; "Box"; "new" ]); + ( BoxDeref, + Sig.box_deref_shared_sig, + false, + to_name (deref_pre @ [ "Deref"; "deref" ]) ); ( BoxDerefMut, Sig.box_deref_mut_sig, false, - deref_pre @ [ "DerefMut"; "deref_mut" ] ); - (VecNew, Sig.vec_new_sig, false, vec_pre @ [ "new" ]); - (VecPush, Sig.vec_push_sig, true, vec_pre @ [ "push" ]); - (VecInsert, Sig.vec_insert_sig, true, vec_pre @ [ "insert" ]); - (VecLen, Sig.vec_len_sig, false, vec_pre @ [ "len" ]); - (VecIndex, Sig.vec_index_shared_sig, true, index_pre @ [ "Index"; "index" ]); + to_name (deref_pre @ [ "DerefMut"; "deref_mut" ]) ); + (VecNew, Sig.vec_new_sig, false, to_name (vec_pre @ [ "new" ])); + (VecPush, Sig.vec_push_sig, true, to_name (vec_pre @ [ "push" ])); + (VecInsert, Sig.vec_insert_sig, true, to_name (vec_pre @ [ "insert" ])); + (VecLen, Sig.vec_len_sig, false, to_name (vec_pre @ [ "len" ])); + ( VecIndex, + Sig.vec_index_shared_sig, + true, + to_name (index_pre @ [ "Index"; "index" ]) ); ( VecIndexMut, Sig.vec_index_mut_sig, true, - index_pre @ [ "IndexMut"; "index_mut" ] ); + to_name (index_pre @ [ "IndexMut"; "index_mut" ]) ); ] let get_assumed_info (id : A.assumed_fun_id) : assumed_info = @@ -274,7 +280,7 @@ let get_assumed_sig (id : A.assumed_fun_id) : A.fun_sig = let get_assumed_name (id : A.assumed_fun_id) : fun_name = let _, _, _, name = get_assumed_info id in - Regular name + name let assumed_is_monadic (id : A.assumed_fun_id) : bool = let _, _, b, _ = get_assumed_info id in diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index d1108913..43ca1074 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -21,21 +21,22 @@ module A = CfimAst (* The default logger *) let log = Logging.cfim_of_json_logger +let path_elem_of_json (js : json) : (path_elem, string) result = + combine_error_msgs js "path_elem_of_json" + (match js with + | `Assoc [ ("Ident", name) ] -> + let* name = string_of_json name in + Ok (Ident name) + | `Assoc [ ("Disambiguator", d) ] -> + let* d = Disambiguator.id_of_json d in + Ok (Disambiguator d) + | _ -> Error "") + let name_of_json (js : json) : (name, string) result = - combine_error_msgs js "name_of_json" (list_of_json string_of_json js) + combine_error_msgs js "name_of_json" (list_of_json path_elem_of_json js) let fun_name_of_json (js : json) : (fun_name, string) result = - combine_error_msgs js "fun_name_of_json" - (match js with - | `Assoc [ ("Regular", name) ] -> - let* name = name_of_json name in - Ok (Regular name) - | `Assoc [ ("Impl", `List [ type_name; impl_id; ident ]) ] -> - let* type_name = name_of_json type_name in - let* impl_id = ImplId.id_of_json impl_id in - let* ident = string_of_json ident in - Ok (Impl (type_name, impl_id, ident)) - | _ -> Error "") + combine_error_msgs js "fun_name_of_json" (name_of_json js) let type_var_of_json (js : json) : (T.type_var, string) result = combine_error_msgs js "type_var_of_json" diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index d8d14ddf..8bf02bd0 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -221,7 +221,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : *) let get_type_name (name : name) : string = match name with - | [ _module; name ] -> name + | [ Ident _module; Ident name ] -> name | _ -> raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name)) in @@ -258,8 +258,9 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : *) let get_fun_name (name : fun_name) : string = match name with - | Regular [ _module; name ] -> name - | Impl ([ _module; ty ], _, name) -> to_snake_case ty ^ "_" ^ name + | [ Ident _module_name; Ident name ] -> name + | [ Ident _module_name; Ident ty; Disambiguator _; Ident name ] -> + to_snake_case ty ^ "_" ^ name | _ -> raise (Failure ("Unexpected name shape: " ^ Print.fun_name_to_string name)) @@ -1098,8 +1099,8 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) it is useful for the decrease clause. *) let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) - (qualif : fun_decl_qualif) (has_decreases_clause : bool) (fwd_def : fun_decl) - (def : fun_decl) : unit = + (qualif : fun_decl_qualif) (has_decreases_clause : bool) + (fwd_def : fun_decl) (def : fun_decl) : unit = (* Retrieve the function name *) let def_name = ctx_get_local_function def.def_id def.back_id ctx in (* (* Add the type parameters - note that we need those bindings only for the diff --git a/src/Names.ml b/src/Names.ml index fff98be9..054c84ad 100644 --- a/src/Names.ml +++ b/src/Names.ml @@ -1,39 +1,86 @@ open Identifiers -type name = string list [@@deriving show, ord] +module Disambiguator = IdGen () + +(** See the comments for [Name] *) +type path_elem = Ident of string | Disambiguator of Disambiguator.id +[@@deriving show, ord] + +type name = path_elem list [@@deriving show, ord] (** A name such as: `std::collections::vector` (which would be represented as - [["std"; "collections"; "vector"]]) *) + [[Ident "std"; Ident "collections"; Ident "vector"]]) + -(* TODO: remove? *) -module NameOrderedType : C.OrderedType with type t = name = struct - type t = name + A name really is a list of strings. However, we sometimes need to + introduce unique indices to disambiguate. This mostly happens because + of "impl" blocks in Rust: + ``` + impl<T> List<T> { + ... + } + ``` + + A type in Rust can have several "impl" blocks, and those blocks can + contain items with similar names. For this reason, we need to disambiguate + them with unique indices. Rustc calls those "disambiguators". In rustc, this + gives names like this: + - `betree_main::betree::NodeIdCounter{impl#0}::new` + - note that impl blocks can be nested, and macros sometimes generate + weird names (which require disambiguation): + `betree_main::betree_utils::_#1::{impl#0}::deserialize::{impl#0}` + + Finally, the paths used by rustc are a lot more precise and explicit than + those we expose in LLBC: for instance, every identifier belongs to a specific + namespace (value namespace, type namespace, etc.), and is coupled with a + disambiguator. + + On our side, we want to stay high-level and simple: we use string identifiers + as much as possible, insert disambiguators only when necessary (whenever + we find an "impl" block, typically) and check that the disambiguator is useless + in the other situations (i.e., the disambiguator is always equal to 0). + + Moreover, the items are uniquely disambiguated by their (integer) ids + (`TypeDeclId.id`, etc.), and when extracting the code we have to deal with + name clashes anyway. Still, we might want to be more precise in the future. + + Also note that the first path element in the name is always the crate name. + *) - let compare = compare_name +let to_name (ls : string list) : name = List.map (fun s -> Ident s) ls - let to_string = String.concat "::" +(*(* TODO: remove? *) + module NameOrderedType : C.OrderedType with type t = name = struct + type t = name - let pp_t = pp_name + let compare = compare_name - let show_t = show_name -end + let to_string = String.concat "::" -module NameMap = C.MakeMap (NameOrderedType) -module NameSet = C.MakeSet (NameOrderedType) + let pp_t = pp_name + + let show_t = show_name + end + + module NameMap = C.MakeMap (NameOrderedType) + module NameSet = C.MakeSet (NameOrderedType) +*) type module_name = name [@@deriving show, ord] type type_name = name [@@deriving show, ord] -module ImplId = IdGen () +type fun_name = name [@@deriving show, ord] -(** A function name *) -type fun_name = - | Regular of name (** "Regular" function name *) - | Impl of type_name * ImplId.id * string - (** The function comes from an "impl" block. +(*module ImplId = IdGen () - As we may have several "impl" blocks for one type, we need to use - a block id to disambiguate the functions (in rustc, this identifier - is called a "disambiguator"). - *) -[@@deriving show, ord] + (** A function name *) + type fun_name = + | Regular of name (** "Regular" function name *) + | Impl of type_name * ImplId.id * string + (** The function comes from an "impl" block. + + As we may have several "impl" blocks for one type, we need to use + a block id to disambiguate the functions (in rustc, this identifier + is called a "disambiguator"). + *) + [@@deriving show, ord]*) diff --git a/src/Print.ml b/src/Print.ml index f8b8ff85..e03efd94 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -11,13 +11,15 @@ module M = Modules let option_to_string (to_string : 'a -> string) (x : 'a option) : string = match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None" -let name_to_string (name : name) : string = String.concat "::" name +let path_elem_to_string (pe : path_elem) : string = + match pe with + | Ident s -> s + | Disambiguator d -> "{" ^ Disambiguator.to_string d ^ "}" -let fun_name_to_string (name : fun_name) : string = - match name with - | Regular name -> name_to_string name - | Impl (type_name, impl_id, ident) -> - name_to_string type_name ^ "{" ^ ImplId.to_string impl_id ^ "}::" ^ ident +let name_to_string (name : name) : string = + String.concat "::" (List.map path_elem_to_string name) + +let fun_name_to_string (name : fun_name) : string = name_to_string name (** Pretty-printing for types *) module Types = struct |