summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/ExtractBuiltin.ml40
-rw-r--r--compiler/FunsAnalysis.ml28
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;