diff options
| -rw-r--r-- | src/FunsAnalysis.ml | 111 | ||||
| -rw-r--r-- | src/PureUtils.ml | 34 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 12 | ||||
| -rw-r--r-- | src/Translate.ml | 3 | ||||
| -rw-r--r-- | src/TranslateCore.ml | 11 |
5 files changed, 135 insertions, 36 deletions
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml new file mode 100644 index 00000000..f187184a --- /dev/null +++ b/src/FunsAnalysis.ml @@ -0,0 +1,111 @@ +(** Compute various information, including: + - can a function fail (by having `Fail` in its body, or transitively + calling a function which can fail) + - can a function diverge + - does a function perform stateful operations (i.e., do we need a state + to translate it) + *) + +open LlbcAst +open Modules + +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_module) (funs_map : fun_decl FunDeclId.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. + *) + 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 obj = + object + inherit [_] iter_statement as super + + method! visit_Assert env a = + can_fail := true; + super#visit_Assert env a + + 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 + can_fail := !can_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 = + can_fail := true; + super#visit_Panic env + + method! visit_Loop env loop = + divergent := true; + super#visit_Loop env loop + end + in + + let visit_fun (f : fun_decl) : unit = + match f.body with + | None -> + (* Opaque function *) + can_fail := true; + stateful := use_state + | Some body -> obj#visit_statement () body.body + in + List.iter visit_fun d; + { 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' + in + + analyze_decl_groups m.declarations; + + !infos diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 032d65d0..992b8cb8 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -453,39 +453,5 @@ let mk_result_return_pattern (v : typed_pattern) : typed_pattern = in { value; ty } -let opt_destruct_state_monad_result (ty : ty) : ty option = - (* Checking: - * ty == state -> result (state & _) ? *) - match ty with - | Arrow (ty0, ty1) -> - (* ty == ty0 -> ty1 - * Checking: ty0 == state ? - * *) - if ty0 = mk_state_ty then - (* Checking: ty1 == result (state & _) *) - match opt_destruct_result ty1 with - | None -> None - | Some ty2 -> ( - (* Checking: ty2 == state & _ *) - match opt_destruct_tuple ty2 with - | Some [ ty3; ty4 ] -> if ty3 = mk_state_ty then Some ty4 else None - | _ -> None) - else None - | _ -> None - let opt_unmeta_mplace (e : texpression) : mplace option * texpression = match e.e with Meta (MPlace mp, e) -> (Some mp, e) | _ -> (None, e) - -let get_fun_effect_info (use_state : bool) (fun_id : A.fun_id) - (gid : T.RegionGroupId.id option) : fun_effect_info = - match fun_id with - | A.Regular _ -> - let input_state = use_state in - let output_state = input_state && gid = None in - { can_fail = true; input_state; output_state } - | A.Assumed aid -> - { - can_fail = Assumed.assumed_can_fail aid; - input_state = false; - output_state = false; - } diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index a9bf0a9d..41b4cdeb 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -475,7 +475,17 @@ let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) : (** Small utility. *) let get_fun_effect_info (config : config) (fun_id : A.fun_id) (gid : T.RegionGroupId.id option) : fun_effect_info = - PureUtils.get_fun_effect_info config.use_state fun_id gid + match fun_id with + | A.Regular _ -> + let input_state = config.use_state in + let output_state = input_state && gid = None in + { can_fail = true; input_state; output_state } + | A.Assumed aid -> + { + can_fail = Assumed.assumed_can_fail aid; + input_state = false; + output_state = false; + } (** Translate a function signature. diff --git a/src/Translate.ml b/src/Translate.ml index 2390dd69..13715865 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -64,6 +64,7 @@ let translate_function_to_symbolics (config : C.partial_config) ^ Print.fun_name_to_string fdef.A.name)); let { type_context; fun_context } = trans_ctx in + let fun_context = { C.fun_decls = fun_context.fun_decls } in match fdef.body with | None -> None @@ -281,6 +282,8 @@ let translate_module_to_pure (config : C.partial_config) (* Compute the type and function contexts *) let type_context, fun_context = compute_type_fun_contexts m in + let fun_infos = FA.analyze_module m fun_context.C.fun_decls use_state in + let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in let trans_ctx = { type_context; fun_context } in (* Translate all the type definitions *) diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index 6e5204f6..17c35cbf 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -6,11 +6,20 @@ module T = Types module A = LlbcAst module M = Modules module SA = SymbolicAst +module FA = FunsAnalysis (** The local logger *) let log = L.translate_log -type trans_ctx = { type_context : C.type_context; fun_context : C.fun_context } +type type_context = C.type_context [@@deriving show] + +type fun_context = { + fun_decls : A.fun_decl A.FunDeclId.Map.t; + fun_infos : FA.fun_info A.FunDeclId.Map.t; +} +[@@deriving show] + +type trans_ctx = { type_context : type_context; fun_context : fun_context } type pure_fun_translation = Pure.fun_decl * Pure.fun_decl list |