Merge branch 'main' into afromher_shifts

1 files changed, 59 insertions, 18 deletions

diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index b72fa078..9ae6ce86 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -8,7 +8,7 @@
  *)
 
 open LlbcAst
-module EU = ExpressionsUtils
+open ExpressionsUtils
 
 (** Various information about a function.
 
@@ -57,12 +57,32 @@ 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 group_has_builtin_info = ref false in
+    let name_matcher_ctx : Charon.NameMatcher.ctx =
+      {
+        type_decls = m.type_decls;
+        global_decls = m.global_decls;
+        trait_decls = m.trait_decls;
+      }
+    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 get_builtin_info (f : fun_decl) : ExtractBuiltin.effect_info option =
+      let open ExtractBuiltin in
+      NameMatcherMap.find_opt name_matcher_ctx f.name builtin_fun_effects_map
+    in
 
+    (* JP: Why not use a reduce visitor here with a tuple of the values to be
+       computed? *)
     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 maybe_stateful b = stateful := !stateful || b
 
           method! visit_Assert env a =
             self#may_fail true;
@@ -70,14 +90,14 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
 
           method! visit_rvalue _env rv =
             match rv with
-            | Use _ | Ref _ | Global _ | Discriminant _ | Aggregate _ -> ()
-            | UnaryOp (uop, _) -> can_fail := EU.unop_can_fail uop || !can_fail
+            | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ -> ()
+            | UnaryOp (uop, _) -> can_fail := unop_can_fail uop || !can_fail
             | BinaryOp (bop, _, _) ->
-                can_fail := EU.binop_can_fail bop || !can_fail
+                can_fail := binop_can_fail bop || !can_fail
 
           method! visit_Call env call =
-            (match call.func with
-            | Regular id ->
+            (match call.func.func with
+            | FunId (FRegular id) ->
                 if FunDeclId.Set.mem id fun_ids then (
                   can_diverge := true;
                   is_rec := true)
@@ -86,9 +106,14 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
                   self#may_fail info.can_fail;
                   stateful := !stateful || info.stateful;
                   can_diverge := !can_diverge || info.can_diverge
-            | Assumed id ->
+            | FunId (FAssumed id) ->
                 (* None of the assumed functions can diverge nor are considered stateful *)
-                can_fail := !can_fail || Assumed.assumed_can_fail id);
+                can_fail := !can_fail || Assumed.assumed_fun_can_fail id
+            | TraitMethod _ ->
+                (* We consider trait functions can fail, but can not diverge and are not stateful.
+                   TODO: this may cause issues if we use use a fuel parameter.
+                *)
+                can_fail := true);
             super#visit_Call env call
 
           method! visit_Panic env =
@@ -102,11 +127,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 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 ->
-          (* Opaque function: we consider they fail by default *)
-          obj#may_fail true;
-          stateful := (not f.is_global_decl_body) && use_state
+          let info_can_fail, info_stateful =
+            match builtin_info with
+            | None -> (true, use_state)
+            | Some { can_fail; stateful } -> (can_fail, stateful)
+          in
+          obj#may_fail info_can_fail;
+          obj#maybe_stateful
+            (if f.is_global_decl_body then false
+             else if not use_state then false
+             else info_stateful)
       | Some body -> obj#visit_statement () body.body
     in
     List.iter visit_fun d;
@@ -114,12 +149,17 @@ 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 !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.
-     * However, we do keep the result of the analysis for global bodies.
+     * However, we do keep the result of the analysis for global bodies and for
+     * builtin functions which are marked as non-fallible.
      * *)
-    can_fail := (not is_global_decl_body) || !can_fail;
+    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;
@@ -130,7 +170,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
 
   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 = match d with NonRecGroup id -> [ id ] | RecGroup 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
@@ -141,14 +181,15 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
   let rec analyze_decl_groups (decls : declaration_group list) : unit =
     match decls with
     | [] -> ()
-    | Type _ :: decls' -> analyze_decl_groups decls'
-    | Fun decl :: decls' ->
+    | (TypeGroup _ | TraitDeclGroup _ | TraitImplGroup _) :: decls' ->
+        analyze_decl_groups decls'
+    | FunGroup decl :: decls' ->
         analyze_fun_decl_group decl;
         analyze_decl_groups decls'
-    | Global id :: decls' ->
+    | GlobalGroup 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_fun_decl_group (NonRecGroup global.body);
         analyze_decl_groups decls'
   in