diff options
Diffstat (limited to 'compiler/ExtractBase.ml')
| -rw-r--r-- | compiler/ExtractBase.ml | 243 |
1 files changed, 45 insertions, 198 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 5aa8323e..591e8aab 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -167,11 +167,7 @@ type id = | TraitImplId of TraitImplId.id | LocalTraitClauseId of TraitClauseId.id | TraitDeclConstructorId of TraitDeclId.id - | TraitMethodId of TraitDeclId.id * string * T.RegionGroupId.id option - (** Something peculiar with trait methods: because we have to take into - account forward/backward functions, we may need to generate fields - items per method. - *) + | TraitMethodId of TraitDeclId.id * string | TraitItemId of TraitDeclId.id * string (** A trait associated item which is not a method *) | TraitParentClauseId of TraitDeclId.id * TraitClauseId.id @@ -353,8 +349,6 @@ let basename_to_unique (names_set : StringSet.t) in if StringSet.mem basename names_set then gen 1 else basename -type fun_name_info = { keep_fwd : bool; num_backs : int } - type names_maps = { names_map : names_map; (** The map for id to names, where we forbid name collisions @@ -384,7 +378,7 @@ let allow_collisions (id : id) : bool = | FieldId _ | TraitItemClauseId _ | TraitParentClauseId _ | TraitItemId _ | TraitMethodId _ -> !Config.record_fields_short_names - | FunId (Pure _ | FromLlbc (FunId (FAssumed _), _, _)) -> + | FunId (Pure _ | FromLlbc (FunId (FAssumed _), _)) -> (* We map several assumed functions to the same id *) true | _ -> false @@ -471,8 +465,7 @@ type names_map_init = { assumed_adts : (assumed_ty * string) list; assumed_structs : (assumed_ty * string) list; assumed_variants : (assumed_ty * VariantId.id * string) list; - assumed_llbc_functions : - (A.assumed_fun_id * RegionGroupId.id option * string) list; + assumed_llbc_functions : (A.assumed_fun_id * string) list; assumed_pure_functions : (pure_assumed_fun_id * string) list; } @@ -550,15 +543,6 @@ type extraction_ctx = { -- makes the if then else dependent ]} *) - fun_name_info : fun_name_info PureUtils.RegularFunIdMap.t; - (** Information used to filter and name functions - we use it - to print comments in the generated code, to help link - the generated code to the original code (information such - as: "this function is the backward function of ...", or - "this function is the merged forward/backward function of ..." - in case a Rust function only has one backward translation - and we filter the forward function because it returns unit. - *) trait_decl_id : trait_decl_id option; (** If we are extracting a trait declaration, identifies it *) is_provided_method : bool; @@ -669,14 +653,8 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = ^ TraitClauseId.to_string clause_id | TraitItemId (id, name) -> "trait_item_id: " ^ trait_decl_id_to_string id ^ ", type name: " ^ name - | TraitMethodId (trait_decl_id, fun_name, rg_id) -> - let fwd_back_kind = - match rg_id with - | None -> "forward" - | Some rg_id -> "backward " ^ RegionGroupId.to_string rg_id - in - trait_decl_id_to_string trait_decl_id - ^ ", method name (" ^ fwd_back_kind ^ "): " ^ fun_name + | TraitMethodId (trait_decl_id, fun_name) -> + trait_decl_id_to_string trait_decl_id ^ ", method name: " ^ fun_name | TraitSelfClauseId -> "trait_self_clause" let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx = @@ -695,8 +673,8 @@ let ctx_get_function (id : fun_id) (ctx : extraction_ctx) : string = ctx_get (FunId id) ctx let ctx_get_local_function (id : A.FunDeclId.id) (lp : LoopId.id option) - (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = - ctx_get_function (FromLlbc (FunId (FRegular id), lp, rg)) ctx + (ctx : extraction_ctx) : string = + ctx_get_function (FromLlbc (FunId (FRegular id), lp)) ctx let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string = assert (id <> TTuple); @@ -734,8 +712,8 @@ let ctx_get_trait_type (id : trait_decl_id) (item_name : string) ctx_get_trait_item id item_name ctx let ctx_get_trait_method (id : trait_decl_id) (item_name : string) - (rg_id : T.RegionGroupId.id option) (ctx : extraction_ctx) : string = - ctx_get (TraitMethodId (id, item_name, rg_id)) ctx + (ctx : extraction_ctx) : string = + ctx_get (TraitMethodId (id, item_name)) ctx let ctx_get_trait_parent_clause (id : trait_decl_id) (clause : trait_clause_id) (ctx : extraction_ctx) : string = @@ -1052,63 +1030,28 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = (* No Fuel::Succ on purpose *) ] -let assumed_llbc_functions () : - (A.assumed_fun_id * T.RegionGroupId.id option * string) list = - let rg0 = Some T.RegionGroupId.zero in - let regular : (A.assumed_fun_id * T.RegionGroupId.id option * string) list = - match !backend with - | FStar | Coq | HOL4 -> - [ - (ArrayIndexShared, None, "array_index_usize"); - (ArrayToSliceShared, None, "array_to_slice"); - (ArrayRepeat, None, "array_repeat"); - (SliceIndexShared, None, "slice_index_usize"); - ] - | Lean -> - [ - (ArrayIndexShared, None, "Array.index_usize"); - (ArrayToSliceShared, None, "Array.to_slice"); - (ArrayRepeat, None, "Array.repeat"); - (SliceIndexShared, None, "Slice.index_usize"); - ] - in - let mut_funs : (A.assumed_fun_id * T.RegionGroupId.id option * string) list = - if !Config.return_back_funs then - match !backend with - | FStar | Coq | HOL4 -> - [ - (ArrayIndexMut, None, "array_index_mut_usize"); - (ArrayToSliceMut, None, "array_to_slice_mut"); - (SliceIndexMut, None, "slice_index_mut_usize"); - ] - | Lean -> - [ - (ArrayIndexMut, None, "Array.index_mut_usize"); - (ArrayToSliceMut, None, "Array.to_slice_mut"); - (SliceIndexMut, None, "Slice.index_mut_usize"); - ] - else - match !backend with - | FStar | Coq | HOL4 -> - [ - (ArrayIndexMut, None, "array_index_usize"); - (ArrayIndexMut, rg0, "array_update_usize"); - (ArrayToSliceMut, None, "array_to_slice"); - (ArrayToSliceMut, rg0, "array_from_slice"); - (SliceIndexMut, None, "slice_index_usize"); - (SliceIndexMut, rg0, "slice_update_usize"); - ] - | Lean -> - [ - (ArrayIndexMut, None, "Array.index_usize"); - (ArrayIndexMut, rg0, "Array.update_usize"); - (ArrayToSliceMut, None, "Array.to_slice"); - (ArrayToSliceMut, rg0, "Array.from_slice"); - (SliceIndexMut, None, "Slice.index_usize"); - (SliceIndexMut, rg0, "Slice.update_usize"); - ] - in - regular @ mut_funs +let assumed_llbc_functions () : (A.assumed_fun_id * string) list = + match !backend with + | FStar | Coq | HOL4 -> + [ + (ArrayIndexShared, "array_index_usize"); + (ArrayIndexMut, "array_index_mut_usize"); + (ArrayToSliceShared, "array_to_slice"); + (ArrayToSliceMut, "array_to_slice_mut"); + (ArrayRepeat, "array_repeat"); + (SliceIndexShared, "slice_index_usize"); + (SliceIndexMut, "slice_index_mut_usize"); + ] + | Lean -> + [ + (ArrayIndexShared, "Array.index_usize"); + (ArrayIndexMut, "Array.index_mut_usize"); + (ArrayToSliceShared, "Array.to_slice"); + (ArrayToSliceMut, "Array.to_slice_mut"); + (ArrayRepeat, "Array.repeat"); + (SliceIndexShared, "Slice.index_usize"); + (SliceIndexMut, "Slice.index_mut_usize"); + ] let assumed_pure_functions () : (pure_assumed_fun_id * string) list = match !backend with @@ -1200,8 +1143,7 @@ let initialize_names_maps () : names_maps = in let assumed_functions = List.map - (fun (fid, rg, name) -> - (FromLlbc (Pure.FunId (FAssumed fid), None, rg), name)) + (fun (fid, name) -> (FromLlbc (Pure.FunId (FAssumed fid), None), name)) init.assumed_llbc_functions @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions in @@ -1444,61 +1386,12 @@ let default_fun_loop_suffix (num_loops : int) (loop_id : LoopId.id option) : If this function admits only one loop, we omit it. *) if num_loops = 1 then "_loop" else "_loop" ^ LoopId.to_string loop_id -(** A helper function: generates a function suffix from a region group - information. +(** A helper function: generates a function suffix. TODO: move all those helpers. *) -let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) - (num_region_groups : int) (rg : region_group_info option) - ((keep_fwd, num_backs) : bool * int) : string = - let lp_suff = default_fun_loop_suffix num_loops loop_id in - - (* 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 extracted backward function: - - if the forward function has been filtered, we add nothing: - the forward function is useless, so the unique backward function - takes its place, in a way (in effect, we "merge" the forward - and the backward functions). - - 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 - definitions (in particular between type and function definitions). - *) - let rg_suff = - (* TODO: make all the backends match what is done for Lean *) - match rg with - | None -> - if - (* In order to avoid name conflicts: - * - if the forward is eliminated, we add the suffix "_fwd" (it won't be used) - * - otherwise, no suffix (because the backward functions will have a suffix) - *) - num_backs = 1 && not keep_fwd - then "_fwd" - else "" - | Some rg -> - assert (num_region_groups > 0 && num_backs > 0); - if num_backs = 1 then - (* Exactly one backward function *) - if not keep_fwd then "" else "_back" - else if - (* Several region groups/backward functions: - - if all the regions in the group have names, we use those names - - otherwise we use an index - *) - List.for_all Option.is_some rg.region_names - then - (* Concatenate the region names *) - "_back" ^ String.concat "" (List.map Option.get rg.region_names) - else (* Use the region index *) - "_back" ^ RegionGroupId.to_string rg.id - in - lp_suff ^ rg_suff +let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) : string = + (* We only generate a suffix for the functions we generate from the loops *) + default_fun_loop_suffix num_loops loop_id (** Compute the name of a regular (non-assumed) function. @@ -1508,24 +1401,13 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) indices to derive unique names for the loops for instance - if there is exactly one loop, we don't need to use indices) - loop id (if pertinent) - - number of region groups - - region group information in case of a backward function - ([None] if forward function) - - pair: - - do we generate the forward function (it may have been filtered)? - - the number of *extracted backward functions* (same comment as for - the number of loops) - The number of extracted backward functions if not necessarily - equal to the number of region groups, because we may have - filtered some of them. TODO: use the fun id for the assumed functions. *) let ctx_compute_fun_name (ctx : extraction_ctx) (fname : llbc_name) - (num_loops : int) (loop_id : LoopId.id option) (num_rgs : int) - (rg : region_group_info option) (filter_info : bool * int) : string = + (num_loops : int) (loop_id : LoopId.id option) : string = let fname = ctx_compute_fun_name_no_suffix ctx fname in (* Compute the suffix *) - let suffix = default_fun_suffix num_loops loop_id num_rgs rg filter_info in + let suffix = default_fun_suffix num_loops loop_id in (* Concatenate *) fname ^ suffix @@ -1999,61 +1881,26 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : | None -> (* Not the case: "standard" registration *) let name = ctx_compute_global_name ctx def.name in - let body = FunId (FromLlbc (FunId (FRegular def.body), None, None)) in + let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in let ctx = ctx_add decl (name ^ "_c") ctx in let ctx = ctx_add body (name ^ "_body") ctx in ctx -let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl) - (ctx : extraction_ctx) : string = - (* Lookup the LLBC def to compute the region group information *) - let def_id = def.def_id in - let llbc_def = A.FunDeclId.Map.find def_id ctx.trans_ctx.fun_ctx.fun_decls in - let sg = llbc_def.signature in - let regions_hierarchy = - LlbcAstUtils.FunIdMap.find (FRegular def_id) - ctx.trans_ctx.fun_ctx.regions_hierarchies - in - let num_rgs = List.length regions_hierarchy in - let { keep_fwd; fwd = _; backs } = trans_group in - let num_backs = List.length backs in - let rg_info = - match def.back_id with - | None -> None - | Some rg_id -> - let rg = T.RegionGroupId.nth regions_hierarchy rg_id in - let region_names = - List.map - (fun rid -> (T.RegionVarId.nth sg.generics.regions rid).name) - rg.regions - in - Some { id = rg_id; region_names } - in +let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string = (* Add the function name *) - ctx_compute_fun_name ctx def.llbc_name def.num_loops def.loop_id num_rgs - rg_info (keep_fwd, num_backs) + ctx_compute_fun_name ctx def.llbc_name def.num_loops def.loop_id (* TODO: move to Extract *) -let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl) - (ctx : extraction_ctx) : extraction_ctx = +let ctx_add_fun_decl (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = (* Sanity check: the function should not be a global body - those are handled * separately *) assert (not def.is_global_decl_body); (* Lookup the LLBC def to compute the region group information *) let def_id = def.def_id in - let { keep_fwd; fwd = _; backs } = trans_group in - let num_backs = List.length backs in (* Add the function name *) - let def_name = ctx_compute_fun_name trans_group def ctx in - let fun_id = (Pure.FunId (FRegular def_id), def.loop_id, def.back_id) in - let ctx = ctx_add (FunId (FromLlbc fun_id)) def_name ctx in - (* Add the name info *) - { - ctx with - fun_name_info = - PureUtils.RegularFunIdMap.add fun_id { keep_fwd; num_backs } - ctx.fun_name_info; - } + let def_name = ctx_compute_fun_name def ctx in + let fun_id = (Pure.FunId (FRegular def_id), def.loop_id) in + ctx_add (FunId (FromLlbc fun_id)) def_name ctx let ctx_compute_type_decl_name (ctx : extraction_ctx) (def : type_decl) : string = |