Start implementing divergence, can_fail, statefullness analyses

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