diff options
| -rw-r--r-- | src/Collections.ml | 8 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 188 | ||||
| -rw-r--r-- | src/PureUtils.ml | 18 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 18 | ||||
| -rw-r--r-- | src/Translate.ml | 4 |
5 files changed, 116 insertions, 120 deletions
diff --git a/src/Collections.ml b/src/Collections.ml index 80345e14..bb7c37f1 100644 --- a/src/Collections.ml +++ b/src/Collections.ml @@ -193,7 +193,7 @@ end identifiers to names (i.e., strings) when generating code, in order to make sure that we don't have potentially dangerous collisions. *) -module type MapInj = sig +module type InjMap = sig type key type elem @@ -271,9 +271,9 @@ module type MapInj = sig val of_list : (key * elem) list -> t end -(** See [MapInj] *) -module MakeMapInj (Key : OrderedType) (Elem : OrderedType) : - MapInj with type key = Key.t with type elem = Elem.t = struct +(** See [InjMap] *) +module MakeInjMap (Key : OrderedType) (Elem : OrderedType) : + InjMap with type key = Key.t with type elem = Elem.t = struct module Map = MakeMap (Key) module Set = MakeSet (Elem) diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index b9f5a9a1..d5fd4432 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -25,18 +25,6 @@ type extraction_ctx = { functions, etc. *) -(** We use identifiers to look for name clashes *) -type id = - | FunId of FunDefId.id * RegionGroupId.id option - | TypeId of TypeDefId.id - | VarId of VarId.id - | UnknownId - (** Used for stored various strings like keywords, definitions which - should always be in context, etc. and which can't be linked to one - of the above. - *) -[@@deriving show, ord] - type region_group_info = { id : RegionGroupId.id; (** The id of the region group. @@ -49,6 +37,9 @@ type region_group_info = { *) } +module StringSet = Collections.MakeSet (Collections.OrderedString) +module StringMap = Collections.MakeMap (Collections.OrderedString) + type name = Identifiers.name type name_formatter = { @@ -66,11 +57,18 @@ type name_formatter = { - region group information in case of a backward function (`None` if forward function) *) - var_basename : name -> string; + var_basename : StringSet.t -> ty -> string; (** Generates a variable basename. + + Inputs: + - the set of names used in the context so far + - the type of the variable (can be useful for heuristics, in order + not to always use "x" for instance, whenever naming anonymous + variables) Note that once the formatter generated a basename, we add an index - if necessary to prevent name clashes. + if necessary to prevent name clashes: the burden of name clashes checks + is thus on the caller's side. *) } (** A name formatter's role is to come up with name suggestions. @@ -148,84 +146,84 @@ let compute_fun_def_name (ctx : extraction_ctx) (fmt : name_formatter) in fmt.fun_name fun_id basename num_region_groups rg_info -(* - let name_to_string (n : name) : string = show_name n - - module NameOrderedType = struct - type t = name - - let compare = compare_name - - let to_string = name_to_string - - let pp_t = pp_name - - let show_t = show_name - end - - module NameMap = Collections.MakeMapInj (NameOrderedType) (Id.NameOrderedType) - (** Notice that we use the *injective* map to map identifiers to names. - - Of course, even if those names (which are string lists) don't collide, - when converting them to strings we can still introduce collisions: we - check that later. - - Note that we use injective maps for sanity: though we write the name - generation with collision in mind, it is always good to have such checks. - *)*) - -(*let translate_fun_name (fdef : A.fun_def) (bid : T.RegionGroupId.id option) : - Id.name = - let sg = fdef.signature in - (* General function to generate a suffix for a region group - * (i.e., an abstraction)*) - let rg_to_string (rg : T.region_var_group) : string = - (* We are just a little bit smart: - - if there is exactly one region id in the region group and this region - has a name, we use this name - - otherwise, we use the region number (note that region names shouldn't - start with numbers) - *) - match rg.T.regions with - | [ rid ] -> ( - let rvar = T.RegionVarId.nth sg.region_params rid in - match rvar.name with - | None -> T.RegionGroupId.to_string rg.T.id - | Some name -> name) - | _ -> T.RegionGroupId.to_string rg.T.id - in - (* There are several cases: - - this is a forward function: we add "_fwd" - - this is a backward function: - - this function has one backward function: we add "_back" - - this function has several backward function: we add "_back" and an - additional suffix to identify the precise backward function - *) - let suffix = - match bid with - | None -> "_fwd" - | Some bid -> ( - match sg.regions_hierarchy with - | [] -> - failwith "Unreachable" - (* we can't get there if we ask for a back function *) - | [ _ ] -> - (* Exactly one backward function *) - "_back" - | _ -> - (* Several backward functions *) - let rg = T.RegionGroupId.nth sg.regions_hierarchy bid in - "_back" ^ rg_to_string rg) - in - (* Final name *) - let rec add_to_last (n : Id.name) : Id.name = - match n with - | [] -> failwith "Unreachable" - | [ x ] -> [ x ^ suffix ] - | x :: n -> x :: add_to_last n - in - add_to_last fdef.name - - (** Generates a name for a type (simply reuses the name in the definition) *) - let translate_type_name (def : T.type_def) : Id.name = def.T.name -*) +(** We use identifiers to look for name clashes *) +type id = + | FunId of A.fun_id * RegionGroupId.id option + | TypeId of type_id + | VarId of VarId.id + | UnknownId + (** Used for stored various strings like keywords, definitions which + should always be in context, etc. and which can't be linked to one + of the above. + *) +[@@deriving show, ord] + +module IdOrderedType = struct + type t = id + + let compare = compare_id + + let to_string = show_id + + let pp_t = pp_id + + let show_t = show_id +end + +module IdMap = Collections.MakeMap (IdOrderedType) + +type names_map = { + id_to_name : string IdMap.t; + name_to_id : id StringMap.t; + (** The name to id map is used to look for name clashes, and generate nice + debugging messages: if there is a name clash, it is useful to know + precisely which identifiers are mapped to the same name... + *) + names_set : StringSet.t; +} +(** The names map stores the mappings from names to identifiers and vice-versa. + + We use it for lookups (during the translation) and to check for name clashes. + *) + +let names_map_add (id : id) (name : string) (nm : names_map) : names_map = + (* Sanity check: no clashes *) + assert (not (StringSet.mem name nm.names_set)); + (* Insert *) + let id_to_name = IdMap.add id name nm.id_to_name in + let name_to_id = StringMap.add name id nm.name_to_id in + let names_set = StringSet.add name nm.names_set in + { id_to_name; name_to_id; names_set } + +let names_map_find (id : id) (nm : names_map) : string = + IdMap.find id nm.id_to_name + +let names_map_find_function (id : A.fun_id) (rg : RegionGroupId.id option) + (nm : names_map) : string = + names_map_find (FunId (id, rg)) nm + +let names_map_find_local_function (id : FunDefId.id) + (rg : RegionGroupId.id option) (nm : names_map) : string = + names_map_find_function (A.Local id) rg nm + +let names_map_find_type (id : type_id) (nm : names_map) : string = + assert (id <> Tuple); + names_map_find (TypeId id) nm + +let names_map_find_local_type (id : TypeDefId.id) (nm : names_map) : string = + names_map_find_type (AdtId id) nm + +(** Make a basename unique (by adding an index). + + We do this in an inefficient manner (by testing all indices starting from + 0) but it shouldn't be a bottleneck. + + [add_index]: concatenates a given index to the variable's basename. + *) +let var_basename_to_unique (names_set : StringSet.t) (add_index : int -> string) + : string = + let rec gen (i : int) : string = + let s = add_index i in + if StringSet.mem s names_set then gen (i + 1) else s + in + gen 0 diff --git a/src/PureUtils.ml b/src/PureUtils.ml index dd072d23..1a227e51 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -1,5 +1,23 @@ open Pure +type regular_fun_id = A.fun_id * T.RegionGroupId.id option +[@@deriving show, ord] +(** We use this type as a key for lookups *) + +module RegularFunIdOrderedType = struct + type t = regular_fun_id + + let compare = compare_regular_fun_id + + let to_string = show_regular_fun_id + + let pp_t = pp_regular_fun_id + + let show_t = show_regular_fun_id +end + +module RegularFunIdMap = Collections.MakeMap (RegularFunIdOrderedType) + (* TODO : move *) let binop_can_fail (binop : E.binop) : bool = match binop with diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index d48f732d..09db7b9c 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -12,24 +12,6 @@ module PP = PrintPure (** The local logger *) let log = L.symbolic_to_pure_log -type regular_fun_id = A.fun_id * T.RegionGroupId.id option -[@@deriving show, ord] -(** We use this type as a key for lookups *) - -module RegularFunIdOrderedType = struct - type t = regular_fun_id - - let compare = compare_regular_fun_id - - let to_string = show_regular_fun_id - - let pp_t = pp_regular_fun_id - - let show_t = show_regular_fun_id -end - -module RegularFunIdMap = Collections.MakeMap (RegularFunIdOrderedType) - type type_context = { cfim_type_defs : T.type_def TypeDefId.Map.t; types_infos : TA.type_infos; (* TODO: rename to type_infos *) diff --git a/src/Translate.ml b/src/Translate.ml index de408a24..dafa2f99 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -60,8 +60,7 @@ let translate_function_to_symbolics (config : C.partial_config) *) let translate_function_to_pure (config : C.partial_config) (trans_ctx : trans_ctx) - (fun_sigs : - SymbolicToPure.fun_sig_named_outputs SymbolicToPure.RegularFunIdMap.t) + (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdMap.t) (fdef : A.fun_def) : pure_fun_translation = (* Debug *) log#ldebug @@ -78,7 +77,6 @@ let translate_function_to_pure (config : C.partial_config) (* Convert the symbolic ASTs to pure ASTs: *) (* Initialize the context *) - let module RegularFunIdMap = SymbolicToPure.RegularFunIdMap in let forward_sig = RegularFunIdMap.find (A.Local def_id, None) fun_sigs in let forward_ret_ty = match forward_sig.sg.outputs with |