diff options
| -rw-r--r-- | src/ExtractToFStar.ml | 12 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 63 | ||||
| -rw-r--r-- | src/Translate.ml | 4 |
3 files changed, 34 insertions, 45 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 0c77f48b..a28d8c6d 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -264,12 +264,12 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name)) in let fun_name (_fid : A.fun_id) (fname : name) (num_rgs : int) - (rg : region_group_info option) : string = + (rg : region_group_info option) (filter_info : bool * int) : string = let fname = get_fun_name fname in (* Converting to snake case should be a no-op, but it doesn't cost much *) let fname = to_snake_case fname in (* Compute the suffix *) - let suffix = default_fun_suffix num_rgs rg in + let suffix = default_fun_suffix num_rgs rg filter_info in (* Concatenate *) fname ^ suffix in @@ -632,14 +632,16 @@ let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) (** Compute the names for all the pure functions generated from a rust function (forward function and backward functions). *) -let extract_fun_def_register_names (ctx : extraction_ctx) +let extract_fun_def_register_names (ctx : extraction_ctx) (keep_fwd : bool) (def : pure_fun_translation) : extraction_ctx = let fwd, back_ls = def in (* Register the forward function name *) - let ctx = ctx_add_fun_def fwd ctx in + let ctx = ctx_add_fun_def (keep_fwd, def) fwd ctx in (* Register the backward functions' names *) let ctx = - List.fold_left (fun ctx back -> ctx_add_fun_def back ctx) ctx back_ls + List.fold_left + (fun ctx back -> ctx_add_fun_def (keep_fwd, def) back ctx) + ctx back_ls in (* Return *) ctx diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 04d65423..c61338b9 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -65,12 +65,18 @@ type formatter = { - type name *) type_name : name -> string; (** Provided a basename, compute a type name. *) - fun_name : A.fun_id -> name -> int -> region_group_info option -> string; + fun_name : + A.fun_id -> name -> int -> region_group_info option -> bool * int -> string; (** Inputs: - function id: this is especially useful to identify whether the function is an assumed function or a local function - function basename - number of region groups + - pair: + - do we generate the forward function (it may have been filtered)? + - the number of extracted backward functions (not necessarily equal + to the number of region groups, because we may have filtered + some of them) - region group information in case of a backward function (`None` if forward function) *) @@ -497,12 +503,15 @@ let ctx_add_struct (def : type_def) (ctx : extraction_ctx) : let ctx = ctx_add (StructId (AdtId def.def_id)) name ctx in (ctx, name) -let ctx_add_fun_def (def : fun_def) (ctx : extraction_ctx) : extraction_ctx = +let ctx_add_fun_def (trans_group : bool * pure_fun_translation) (def : fun_def) + (ctx : extraction_ctx) : extraction_ctx = (* Lookup the CFIM def to compute the region group information *) let def_id = def.def_id in let cfim_def = FunDefId.Map.find def_id ctx.trans_ctx.fun_context.fun_defs in let sg = cfim_def.signature in let num_rgs = List.length sg.regions_hierarchy in + let keep_fwd, (_, backs) = trans_group in + let num_backs = List.length backs in let rg_info = match def.back_id with | None -> None @@ -519,7 +528,9 @@ let ctx_add_fun_def (def : fun_def) (ctx : extraction_ctx) : extraction_ctx = Some { id = rg_id; region_names } in let def_id = A.Local def_id in - let name = ctx.fmt.fun_name def_id def.basename num_rgs rg_info in + let name = + ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs) + in let ctx = ctx_add (FunId (def_id, def.back_id)) name ctx in ctx @@ -588,13 +599,17 @@ let compute_type_def_name (fmt : formatter) (def : type_def) : string = TODO: move all those helpers. *) let default_fun_suffix (num_region_groups : int) (rg : region_group_info option) - : string = + ((keep_fwd, num_backs) : bool * int) : string = (* There are several cases: - [rg] is `Some`: this is a forward function: - we add "_fwd" - [rg] is `None`: this is a backward function: - - this function has one region group: we add "_back" - - this function has several backward function: we add "_back" and an + - this function has one extracted backward function: + - if the forward function has been filtered, we add "_fwd_back": + the forward function is useless, so the unique backward function + takes its place, in a way + - otherwise we add "_back" + - this function has several backward functions: we add "_back" and an additional suffix to identify the precise backward function Note that we always add a suffix (in case there are no region groups, we could not add the "_fwd" suffix) to prevent name clashes between @@ -603,9 +618,10 @@ let default_fun_suffix (num_region_groups : int) (rg : region_group_info option) match rg with | None -> "_fwd" | Some rg -> - assert (num_region_groups > 0); - if num_region_groups = 1 then (* Exactly one backward function *) - "_back" + assert (num_region_groups > 0 && num_backs > 0); + if num_backs = 1 then + (* Exactly one backward function *) + if not keep_fwd then "_fwd_back" else "_back" else if (* Several region groups/backward functions: - if all the regions in the group have names, we use those names @@ -617,32 +633,3 @@ let default_fun_suffix (num_region_groups : int) (rg : region_group_info option) "_back" ^ String.concat "" (List.map Option.get rg.region_names) else (* Use the region index *) "_back" ^ RegionGroupId.to_string rg.id - -(** Extract information from a function, and give this information to a - [formatter] to generate a function's name. - - Note that we need region information coming from CFIM (when generating - the name for a backward function, we try to use the names of the regions - to - *) -let compute_fun_def_name (ctx : trans_ctx) (fmt : formatter) (fun_id : A.fun_id) - (rg_id : RegionGroupId.id option) : string = - (* Lookup the function CFIM signature (we need the region information) *) - let sg = CfimAstUtils.lookup_fun_sig fun_id ctx.fun_context.fun_defs in - let basename = CfimAstUtils.lookup_fun_name fun_id ctx.fun_context.fun_defs in - (* Compute the regions information *) - let num_region_groups = List.length sg.regions_hierarchy in - let rg_info = - match rg_id with - | None -> None - | Some rg_id -> - let rg = RegionGroupId.nth sg.regions_hierarchy rg_id in - let regions = - List.map (fun rid -> RegionVarId.nth sg.region_params rid) rg.regions - in - let region_names = - List.map (fun (r : T.region_var) -> r.name) regions - in - Some { id = rg.id; region_names } - in - fmt.fun_name fun_id basename num_region_groups rg_info diff --git a/src/Translate.ml b/src/Translate.ml index 8084dc38..f86ef438 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -314,8 +314,8 @@ let translate_module (filename : string) (dest_dir : string) let extract_ctx = List.fold_left - (fun extract_ctx (_, def) -> - ExtractToFStar.extract_fun_def_register_names extract_ctx def) + (fun extract_ctx (keep_fwd, def) -> + ExtractToFStar.extract_fun_def_register_names extract_ctx keep_fwd def) extract_ctx trans_funs in |