diff options
| -rw-r--r-- | compiler/ExtractBuiltin.ml | 40 | ||||
| -rw-r--r-- | compiler/FunsAnalysis.ml | 28 |
2 files changed, 44 insertions, 24 deletions
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index afa0dd6f..363955bf 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -350,7 +350,9 @@ let mk_builtin_funs_map () = let builtin_funs_map = mk_memoized mk_builtin_funs_map -let builtin_non_fallible_funs = +type effect_info = { can_fail : bool; stateful : bool } + +let builtin_fun_effects = let int_names = [ "usize"; @@ -377,19 +379,31 @@ let builtin_non_fallible_funs = int_names in let int_funs = List.concat int_funs in - [ - "alloc::vec::Vec::new"; - "alloc::vec::Vec::len"; - "alloc::boxed::Box::deref"; - "alloc::boxed::Box::deref_mut"; - "core::mem::replace"; - "core::mem::take"; - ] - @ int_funs + let no_fail_no_state_funs = + [ + "alloc::vec::Vec::new"; + "alloc::vec::Vec::len"; + "alloc::boxed::Box::deref"; + "alloc::boxed::Box::deref_mut"; + "core::mem::replace"; + "core::mem::take"; + ] + @ int_funs + in + let no_fail_no_state_funs = + List.map + (fun n -> (n, { can_fail = false; stateful = false })) + no_fail_no_state_funs + in + let no_state_funs = [ "alloc::vec::Vec::push" ] in + let no_state_funs = + List.map (fun n -> (n, { can_fail = true; stateful = false })) no_state_funs + in + no_fail_no_state_funs @ no_state_funs -let builtin_non_fallible_funs_set = - SimpleNameSet.of_list - (List.map string_to_simple_name builtin_non_fallible_funs) +let builtin_fun_effects_map = + SimpleNameMap.of_list + (List.map (fun (n, x) -> (string_to_simple_name n, x)) builtin_fun_effects) type builtin_trait_decl_info = { rust_name : string; diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 3ba5d35d..9eac3e6f 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -57,16 +57,16 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let stateful = ref false in let can_diverge = ref false in let is_rec = ref false in - let is_builtin_non_fallible_group = ref false in + let group_has_builtin_info = ref false in (* We have some specialized knowledge of some library functions; we don't have any more custom treatment than this, and these functions can be modeled suitably in Primitives.fst, rather than special-casing for them all the way. *) - let is_builtin_non_fallible (f : fun_decl) : bool = + let get_builtin_info (f : fun_decl) : ExtractBuiltin.effect_info option = let open ExtractBuiltin in let name = name_to_simple_name f.name in - SimpleNameSet.mem name builtin_non_fallible_funs_set + SimpleNameMap.find_opt name builtin_fun_effects_map in (* JP: Why not use a reduce visitor here with a tuple of the values to be @@ -119,16 +119,21 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) in (* Sanity check: global bodies don't contain stateful calls *) assert ((not f.is_global_decl_body) || not !stateful); - let is_builtin_non_fallible = is_builtin_non_fallible f in - is_builtin_non_fallible_group := - !is_builtin_non_fallible_group || is_builtin_non_fallible; + let builtin_info = get_builtin_info f in + let has_builtin_info = builtin_info <> None in + group_has_builtin_info := !group_has_builtin_info || has_builtin_info; match f.body with | None -> - obj#may_fail (not is_builtin_non_fallible); + let info_can_fail, info_stateful = + match builtin_info with + | None -> (true, false) + | Some { can_fail; stateful } -> (can_fail, stateful) + in + obj#may_fail info_can_fail; stateful := (not f.is_global_decl_body) && use_state - && not is_builtin_non_fallible + && not (has_builtin_info && not info_stateful) | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; @@ -136,7 +141,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) * 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); - assert ((not !is_builtin_non_fallible_group) || List.length d = 1); + assert ((not !group_has_builtin_info) || 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. @@ -144,8 +149,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) * builtin functions which are marked as non-fallible. * *) can_fail := - ((not is_global_decl_body) && not !is_builtin_non_fallible_group) - || !can_fail; + if is_global_decl_body then !can_fail + else if !group_has_builtin_info then !can_fail + else true; { can_fail = !can_fail; stateful = !stateful; |