Improve the handling of saved function effects in ExtractBuiltin.ml

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;