diff options
Diffstat (limited to 'compiler/LlbcAstUtils.ml')
-rw-r--r-- | compiler/LlbcAstUtils.ml | 61 |
1 files changed, 1 insertions, 60 deletions
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 46711d0a..1111c297 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -1,25 +1,5 @@ open LlbcAst -open Utils -module T = Types - -(** Check if a {!type:LlbcAst.statement} contains loops *) -let statement_has_loops (st : statement) : bool = - let obj = - object - inherit [_] iter_statement - method! visit_Loop _ _ = raise Found - end - in - try - obj#visit_statement () st; - false - with Found -> true - -(** Check if a {!type:LlbcAst.fun_decl} contains loops *) -let fun_decl_has_loops (fd : fun_decl) : bool = - match fd.body with - | Some body -> statement_has_loops body.body - | None -> false +include Charon.LlbcAstUtils let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : fun_sig = @@ -32,42 +12,3 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : match fun_id with | Regular id -> (FunDeclId.Map.find id fun_decls).name | Assumed aid -> Assumed.get_assumed_name aid - -(** Small utility: list the transitive parents of a region var group. - We don't do that in an efficient manner, but it doesn't matter. - - TODO: rename to "list_ancestors_..." - - This list *doesn't* include the current region. - *) -let rec list_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) : - T.RegionGroupId.Set.t = - let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in - let parents = - List.fold_left - (fun s gid -> - (* Compute the parents *) - let parents = list_parent_region_groups sg gid in - (* Parents U current region *) - let parents = T.RegionGroupId.Set.add gid parents in - (* Make the union with the accumulator *) - T.RegionGroupId.Set.union s parents) - T.RegionGroupId.Set.empty rg.parents - in - parents - -(** Small utility: same as {!list_parent_region_groups}, but returns an ordered list. *) -let list_ordered_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) - : T.RegionGroupId.id list = - let pset = list_parent_region_groups sg gid in - let parents = - List.filter - (fun (rg : T.region_var_group) -> T.RegionGroupId.Set.mem rg.id pset) - sg.regions_hierarchy - in - let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in - parents - -let fun_body_get_input_vars (fbody : fun_body) : var list = - let locals = List.tl fbody.locals in - Collections.List.prefix fbody.arg_count locals |