From 7e7d0d67de8285e1d6c589750191bce4f49aacb3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 27 Oct 2022 09:16:46 +0200 Subject: Reorganize a bit the project --- compiler/FunsAnalysis.ml | 143 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 143 insertions(+) create mode 100644 compiler/FunsAnalysis.ml (limited to 'compiler/FunsAnalysis.ml') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml new file mode 100644 index 00000000..248ad8b3 --- /dev/null +++ b/compiler/FunsAnalysis.ml @@ -0,0 +1,143 @@ +(** Compute various information, including: + - can a function fail (by having `Fail` in its body, or transitively + calling a function which can fail - this is false for globals) + - can a function diverge (by being recursive, containing a loop or + transitively calling a function which can diverge) + - does a function perform stateful operations (i.e., do we need a state + to translate it) + *) + +open LlbcAst +open Crates +module EU = ExpressionsUtils + +type fun_info = { + can_fail : bool; + (* Not used yet: all the extracted functions use an error monad *) + stateful : bool; + divergent : bool; (* Not used yet *) +} +[@@deriving show] +(** Various information about a function. + + Note that not all this information is used yet to adjust the extraction yet. + *) + +type modules_funs_info = fun_info FunDeclId.Map.t +(** Various information about a module's functions *) + +let analyze_module (m : llbc_crate) (funs_map : fun_decl FunDeclId.Map.t) + (globals_map : global_decl GlobalDeclId.Map.t) (use_state : bool) : + modules_funs_info = + let infos = ref FunDeclId.Map.empty in + + let register_info (id : FunDeclId.id) (info : fun_info) : unit = + assert (not (FunDeclId.Map.mem id !infos)); + infos := FunDeclId.Map.add id info !infos + in + + (* Analyze a group of mutually recursive functions. + * As the functions can call each other, we compute the same information + * for all of them (if one of the functions can fail, then all of them + * can fail, etc.). + * + * We simply check if the functions contains panic statements, loop statements, + * recursive calls, etc. We use the previously computed information in case + * of function calls. + *) + let analyze_fun_decls (fun_ids : FunDeclId.Set.t) (d : fun_decl list) : + fun_info = + let can_fail = ref false in + let stateful = ref false in + let divergent = ref false in + + let visit_fun (f : fun_decl) : unit = + let obj = + object (self) + inherit [_] iter_statement as super + method may_fail b = can_fail := !can_fail || b + + method! visit_Assert env a = + self#may_fail true; + super#visit_Assert env a + + method! visit_rvalue _env rv = + match rv with + | Use _ | Ref _ | Discriminant _ | Aggregate _ -> () + | UnaryOp (uop, _) -> can_fail := EU.unop_can_fail uop || !can_fail + | BinaryOp (bop, _, _) -> + can_fail := EU.binop_can_fail bop || !can_fail + + method! visit_Call env call = + (match call.func with + | Regular id -> + if FunDeclId.Set.mem id fun_ids then divergent := true + else + let info = FunDeclId.Map.find id !infos in + self#may_fail info.can_fail; + stateful := !stateful || info.stateful; + divergent := !divergent || info.divergent + | Assumed id -> + (* None of the assumed functions is stateful for now *) + can_fail := !can_fail || Assumed.assumed_can_fail id); + super#visit_Call env call + + method! visit_Panic env = + self#may_fail true; + super#visit_Panic env + + method! visit_Loop env loop = + divergent := true; + super#visit_Loop env loop + end + in + (* Sanity check: global bodies don't contain stateful calls *) + assert ((not f.is_global_decl_body) || not !stateful); + match f.body with + | None -> + (* Opaque function: we consider they fail by default *) + obj#may_fail true; + stateful := (not f.is_global_decl_body) && use_state + | Some body -> obj#visit_statement () body.body + in + List.iter visit_fun d; + (* We need to know if the declaration group contains a global - note that + * groups containing globals contain exactly one declaration *) + let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in + assert ((not is_global_decl_body) || List.length d == 1); + (* We ignore on purpose functions that cannot fail and consider they *can* + * fail: the result of the analysis is not used yet to adjust the translation + * so that the functions which syntactically can't fail don't use an error monad. + * However, we do keep the result of the analysis for global bodies. + * *) + can_fail := (not is_global_decl_body) || !can_fail; + { can_fail = !can_fail; stateful = !stateful; divergent = !divergent } + in + + let analyze_fun_decl_group (d : fun_declaration_group) : unit = + (* Retrieve the function declarations *) + let funs = match d with NonRec id -> [ id ] | Rec ids -> ids in + let funs = List.map (fun id -> FunDeclId.Map.find id funs_map) funs in + let fun_ids = List.map (fun (d : fun_decl) -> d.def_id) funs in + let fun_ids = FunDeclId.Set.of_list fun_ids in + let info = analyze_fun_decls fun_ids funs in + List.iter (fun (f : fun_decl) -> register_info f.def_id info) funs + in + + let rec analyze_decl_groups (decls : declaration_group list) : unit = + match decls with + | [] -> () + | Type _ :: decls' -> analyze_decl_groups decls' + | Fun decl :: decls' -> + analyze_fun_decl_group decl; + analyze_decl_groups decls' + | Global id :: decls' -> + (* Analyze a global by analyzing its body function *) + let global = GlobalDeclId.Map.find id globals_map in + analyze_fun_decl_group (NonRec global.body_id); + analyze_decl_groups decls' + in + + analyze_decl_groups m.declarations; + + !infos -- cgit v1.2.3