Merge pull request #1 from AeneasVerif/constants-v2

Implement support for globals

1 files changed, 63 insertions, 45 deletions

diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index b8dd17d8..615f45b3 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -1,7 +1,7 @@
 (** 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 (bu being recursive, containing a loop or
+      calling a function which can fail - this is false for globals)
+    - can a function diverge (by being recursive, containing a loop or
       transitively calling a function which can diverge)
     - does a function perform stateful operations (i.e., do we need a state
       to translate it)
@@ -27,7 +27,8 @@ 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 =
+    (globals_map : global_decl GlobalDeclId.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 =
@@ -50,54 +51,66 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
     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_rvalue _env rv =
-          match rv with
-          | Use _ | Ref _ | Discriminant _ | Aggregate _ -> ()
-          | UnaryOp (uop, _) -> can_fail := EU.unop_can_fail uop || !can_fail
-          | BinaryOp (bop, _, _) ->
-              can_fail := EU.binop_can_fail bop || !can_fail
-
-        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 =
+      let obj =
+        object (self)
+          inherit [_] iter_statement as super
+          method may_fail b = can_fail := !can_fail || b
+
+          method! visit_Assert env a =
+            self#may_fail true;
+            super#visit_Assert env a
+
+          method! visit_rvalue _env rv =
+            match rv with
+            | Use _ | Ref _ | Discriminant _ | Aggregate _ -> ()
+            | UnaryOp (uop, _) -> can_fail := EU.unop_can_fail uop || !can_fail
+            | BinaryOp (bop, _, _) ->
+                can_fail := EU.binop_can_fail bop || !can_fail
+
+          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
+                  self#may_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 =
+            self#may_fail true;
+            super#visit_Panic env
+
+          method! visit_Loop env loop =
+            divergent := true;
+            super#visit_Loop env loop
+        end
+      in
+      (* Sanity check: global bodies don't contain stateful calls *)
+      assert ((not f.is_global_decl_body) || not !stateful);
       match f.body with
       | None ->
-          (* Opaque function *)
-          can_fail := true;
-          stateful := use_state
+          (* Opaque function: we consider they fail by default *)
+          obj#may_fail true;
+          stateful := (not f.is_global_decl_body) && use_state
       | Some body -> obj#visit_statement () body.body
     in
     List.iter visit_fun d;
+    (* We need to know if the declaration group contains a global - note that
+     * 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);
+    (* 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.
+     * *)
+    can_fail := (not is_global_decl_body) || !can_fail;
     { can_fail = !can_fail; stateful = !stateful; divergent = !divergent }
   in
 
@@ -118,6 +131,11 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
     | Fun decl :: decls' ->
         analyze_fun_decl_group decl;
         analyze_decl_groups decls'
+    | Global 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_decl_groups decls'
   in
 
   analyze_decl_groups m.declarations;