Traduct globals body separately (WIP)

11 files changed, 208 insertions, 66 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index b89579b5..20b06bfa 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -26,6 +26,14 @@ type type_decl_qualif =
  *)
 type fun_decl_qualif = Let | LetRec | And | Val | AssumeVal
 
+let fun_decl_qualif_name (qualif : fun_decl_qualif) : string =
+  match qualif with
+  | Let -> "let"
+  | LetRec -> "let rec"
+  | And -> "and"
+  | Val -> "val"
+  | AssumeVal -> "assume val"
+
 (** Small helper to compute the name of an int type *)
 let fstar_int_name (int_ty : integer_type) =
   match int_ty with
@@ -305,11 +313,11 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     (* Concatenate the elements *)
     String.concat "_" fname
   in
-  let fun_name (_fid : A.fun_id) (fname : fun_name) (num_rgs : int)
+  let fun_name (_fid : A.fun_id) (fname : fun_name) (is_global : bool) (num_rgs : int)
       (rg : region_group_info option) (filter_info : bool * int) : string =
     let fname = fun_name_to_snake_case fname in
     (* Compute the suffix *)
-    let suffix = default_fun_suffix num_rgs rg filter_info in
+    let suffix = default_fun_suffix is_global num_rgs rg filter_info in
     (* Concatenate *)
     fname ^ suffix
   in
@@ -898,12 +906,14 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       match qualif.id with
       | Func fun_id ->
           extract_function_call ctx fmt inside fun_id qualif.type_args args
+      | Global global_id ->
+          let fid = A.global_to_fun_id ctx.trans_ctx.fun_context.gid_conv global_id in
+          let fun_id = Regular (A.Regular fid, None) in
+          extract_function_call ctx fmt inside fun_id qualif.type_args args
       | AdtCons adt_cons_id ->
           extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args
       | Proj proj ->
           extract_field_projector ctx fmt inside app proj qualif.type_args args
-      (* TODO | Global global_id ->
-          extract_global_ref ctx fmt inside global_id*)
     )
   | _ ->
       (* "Regular" expression *)
@@ -1358,14 +1368,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* > "let FUN_NAME" *)
   let is_opaque = Option.is_none def.body in
-  let qualif =
-    match qualif with
-    | Let -> "let"
-    | LetRec -> "let rec"
-    | And -> "and"
-    | Val -> "val"
-    | AssumeVal -> "assume val"
-  in
+  let qualif = fun_decl_qualif_name qualif in
   F.pp_print_string fmt (qualif ^ " " ^ def_name);
   F.pp_print_space fmt ();
   (* Open a box for "(PARAMS) : EFFECT =" *)
@@ -1474,6 +1477,108 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add breaks to insert new lines between definitions *)
   F.pp_print_break fmt 0 0
 
+(* Change the suffix from "_c" to "_body" *)
+let global_decl_to_body_name (decl : string) : string =
+  (* The declaration length without the global suffix *)
+  let base_len = String.length decl - 2 in
+  (* TODO: Use String.ends_with instead when a more recent version of OCaml is used *)
+  assert (String.sub decl base_len 2 = "_c");
+  (String.sub decl 0 base_len) ^ "_body"
+
+(** Print a definition of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *)
+let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter)
+  (qualif : fun_decl_qualif) (name : string) (ty : ty)
+  (extract_body : (F.formatter -> unit) Option.t)
+    : unit =
+  let is_opaque = Option.is_none extract_body in
+
+  (* Open the definition box (depth=0) *)
+  F.pp_open_hvbox fmt ctx.indent_incr;
+
+  (* Open "QUALIF NAME : TYPE =" box (depth=1) *)
+  F.pp_open_hovbox fmt ctx.indent_incr;
+  (* Print "QUALIF NAME " *)
+  F.pp_print_string fmt (fun_decl_qualif_name qualif ^ " " ^ name);
+  F.pp_print_space  fmt ();
+
+  (* Open ": TYPE =" box (depth=2) *)
+  F.pp_open_hvbox fmt 0;
+  (* Print ": " *)
+  F.pp_print_string fmt ":";
+  F.pp_print_space fmt ();
+
+  (* Open "TYPE" box (depth=3) *)
+  F.pp_open_hovbox fmt ctx.indent_incr;
+  (* Print "TYPE" *)
+  extract_ty ctx fmt false ty;
+  (* Close "TYPE" box (depth=3) *)
+  F.pp_close_box fmt ();
+
+  if not is_opaque then (
+    (* Print " =" *)
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "=";
+  );
+  (* Close ": TYPE =" box (depth=2) *)
+  F.pp_close_box fmt ();
+  (* Close "QUALIF NAME : TYPE =" box (depth=1) *)
+  F.pp_close_box fmt ();
+
+  if not is_opaque then (
+    F.pp_print_space fmt ();
+    (* Open "BODY" box (depth=1) *)
+    F.pp_open_hvbox fmt 0;
+    (* Print "BODY" *)
+    (Option.get extract_body) fmt;
+    (* Close "BODY" box (depth=1) *)
+    F.pp_close_box fmt ()
+  );
+  (* Close the definition box (depth=0) *)
+  F.pp_close_box fmt ()
+
+(** Extract a global declaration.
+    This has similarity with the function extraction above (without parameters).
+    However, generate its body separately from its declaration to extract the result value.
+
+    For example,
+    `let x = 3`
+
+    will be translated to
+    `let x_body : result int = Return 3`
+    `let x_c : int = eval_global x_body`
+ *)
+let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
+  (qualif : fun_decl_qualif) (def : fun_decl)
+    : unit =
+  (* Sanity checks for globals *)
+  assert (def.is_global);
+  assert (Option.is_none def.back_id);
+  assert (List.length def.signature.inputs = 0);
+  assert (List.length def.signature.doutputs = 1);
+  assert (List.length def.signature.type_params = 0);
+  assert (not def.signature.info.effect_info.can_fail);
+
+  (* Add a break then the corresponding Rust definition *)
+  F.pp_print_break  fmt 0 0;
+  F.pp_print_string fmt ("(** [" ^ Print.fun_name_to_string def.basename ^ "] *)");
+  F.pp_print_space  fmt ();
+
+  let def_name = ctx_get_local_function def.def_id def.back_id ctx in
+  match def.body with
+  | None ->
+      extract_global_definition ctx fmt qualif def_name def.signature.output None
+  | Some body ->
+      let body_name = global_decl_to_body_name def_name in
+      let body_ty = mk_result_ty def.signature.output in
+      extract_global_definition ctx fmt qualif body_name body_ty (Some (fun fmt ->
+        extract_texpression ctx fmt false body.body
+      ));
+      F.pp_print_break fmt 0 0;
+      extract_global_definition ctx fmt qualif def_name def.signature.output (Some (fun fmt ->
+        F.pp_print_string fmt ("eval_global " ^ body_name)
+      ));
+  F.pp_print_break fmt 0 0
+
 (** Extract a unit test, if the function is a unit function (takes no
     parameters, returns unit).
     
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index dc205eb9..ca20352f 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -1,6 +1,6 @@
 (** Compute various information, including:
     - can a function fail (by having `Fail` in its body, or transitively
-      calling a function which can fail)
+      calling a function which can fail), false for globals
     - can a function diverge (bu 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
@@ -49,47 +49,56 @@ 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_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 =
+      print_endline ("@ fun: " ^ Print.fun_name_to_string f.name);
+      let obj =
+        object (self)
+          inherit [_] iter_statement as super
+
+          method may_fail b =
+            if f.is_global then () else
+            can_fail := !can_fail || b
+
+          method! visit_Assert env a =
+            self#may_fail true;
+            super#visit_Assert env a
+
+          method! visit_Call env call =
+            print_string "@ dep: ";
+            pp_fun_id Format.std_formatter call.func;
+            print_newline ();
+
+            (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
       match f.body with
       | None ->
           (* Opaque function *)
-          can_fail := true;
+          obj#may_fail true;
           stateful := use_state
       | Some body -> obj#visit_statement () body.body
     in
     List.iter visit_fun d;
+    print_endline ("@ can_fail: " ^ Bool.to_string !can_fail);
     { can_fail = !can_fail; stateful = !stateful; divergent = !divergent }
   in
 
diff --git a/src/Modules.ml b/src/Modules.ml
index b0e8878d..149de020 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -7,7 +7,8 @@ type 'id g_declaration_group = NonRec of 'id | Rec of 'id list
 type type_declaration_group = TypeDeclId.id g_declaration_group
 [@@deriving show]
 
-type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show]
+type fun_declaration_group = FunDeclId.id g_declaration_group
+[@@deriving show]
 
 (** Module declaration *)
 type declaration_group =
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index ea9bf2ab..c13f967f 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -44,6 +44,7 @@ type ast_formatter = {
     TypeDeclId.id -> VariantId.id option -> FieldId.id -> string option;
   adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option;
   fun_decl_id_to_string : A.FunDeclId.id -> string;
+  global_decl_id_to_string : A.GlobalDeclId.id -> string;
 }
 
 let ast_to_value_formatter (fmt : ast_formatter) : value_formatter =
@@ -85,7 +86,9 @@ let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
    while we only need those definitions to lookup proper names for the def ids.
 *)
 let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
-    (fun_decls : A.fun_decl A.FunDeclId.Map.t) (type_params : type_var list) :
+    (fun_decls : A.fun_decl A.FunDeclId.Map.t)
+    (gid_conv : A.global_id_converter)
+    (type_params : type_var list) :
     ast_formatter =
   let type_var_id_to_string vid =
     let var = T.TypeVarId.nth type_params vid in
@@ -112,6 +115,9 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
     let def = A.FunDeclId.Map.find def_id fun_decls in
     fun_name_to_string def.name
   in
+  let global_decl_id_to_string def_id =
+    fun_decl_id_to_string (A.global_to_fun_id gid_conv def_id)
+  in
   {
     type_var_id_to_string;
     type_decl_id_to_string;
@@ -120,6 +126,7 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
     adt_field_names;
     adt_field_to_string;
     fun_decl_id_to_string;
+    global_decl_id_to_string;
   }
 
 let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
@@ -480,6 +487,7 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
         let qualif_s =
           match qualif.id with
           | Func fun_id -> fun_id_to_string fmt fun_id
+          | Global global_id -> fmt.global_decl_id_to_string global_id
           | AdtCons adt_cons_id ->
               let variant_s =
                 adt_variant_to_string
diff --git a/src/Pure.ml b/src/Pure.ml
index 42f56fed..b3be2040 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -302,9 +302,9 @@ type projection = { adt_id : type_id; field_id : FieldId.id } [@@deriving show]
 
 type qualif_id =
   | Func of fun_id
+  | Global of A.GlobalDeclId.id
   | AdtCons of adt_cons_id  (** A function or ADT constructor identifier *)
   | Proj of projection  (** Field projector *)
-  (* TODO | Global of GlobalDeclId.id*)
 [@@deriving show]
 
 type qualif = { id : qualif_id; type_args : ty list } [@@deriving show]
@@ -575,5 +575,6 @@ type fun_decl = {
           (to identify the forward/backward functions) later.
        *)
   signature : fun_sig;
+  is_global : bool;
   body : fun_body option;
 }
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 826283ae..7927a068 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -611,7 +611,10 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
                     | Func (Unop _ | Binop _) ->
                         true (* primitive function call *)
                     | Func (Regular _) ->
-                        false (* non-primitive function call *))
+                        false (* non-primitive function call *)
+                    | Global _ ->
+                        true (* Global constant or static *)
+                  )
                 | _ -> filter
               else false
             in
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 195eb879..e58fec2a 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -74,6 +74,7 @@ type formatter = {
   fun_name :
     A.fun_id ->
     fun_name ->
+    bool ->
     int ->
     region_group_info option ->
     bool * int ->
@@ -440,11 +441,13 @@ let ctx_get (id : id) (ctx : extraction_ctx) : string =
       log#serror ("Could not find: " ^ id_to_string id ctx);
       raise Not_found
 
-let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option)
+let ctx_get_function (id : A.fun_id)
+    (rg : RegionGroupId.id option)
     (ctx : extraction_ctx) : string =
   ctx_get (FunId (id, rg)) ctx
 
-let ctx_get_local_function (id : A.FunDeclId.id) (rg : RegionGroupId.id option)
+let ctx_get_local_function (id : A.FunDeclId.id)
+    (rg : RegionGroupId.id option)
     (ctx : extraction_ctx) : string =
   ctx_get_function (A.Regular id) rg ctx
 
@@ -596,7 +599,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
   in
   let def_id = A.Regular def_id in
   let name =
-    ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs)
+    ctx.fmt.fun_name def_id def.basename def.is_global num_rgs rg_info (keep_fwd, num_backs)
   in
   (* Add the function name *)
   let ctx = ctx_add (FunId (def_id, def.back_id)) name ctx in
@@ -666,8 +669,12 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string =
     information.
     TODO: move all those helpers.
 *)
-let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
-    ((keep_fwd, num_backs) : bool * int) : string =
+let default_fun_suffix
+    (is_global : bool)
+    (num_region_groups : int)
+    (rg : region_group_info option)
+    ((keep_fwd, num_backs) : bool * int)
+    : string =
   (* There are several cases:
      - [rg] is `Some`: this is a forward function:
        - we add "_fwd"
@@ -683,6 +690,7 @@ let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
      we could not add the "_fwd" suffix) to prevent name clashes between
      definitions (in particular between type and function definitions).
   *)
+  if is_global then "_c" else
   match rg with
   | None -> "_fwd"
   | Some rg ->
diff --git a/src/PureTypeCheck.ml b/src/PureTypeCheck.ml
index 8848ff20..90b9ab09 100644
--- a/src/PureTypeCheck.ml
+++ b/src/PureTypeCheck.ml
@@ -111,7 +111,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
       check_texpression ctx body
   | Qualif qualif -> (
       match qualif.id with
-      | Func _ -> () (* TODO *)
+      | Func _ | Global _ -> () (* TODO *)
       | Proj { adt_id = proj_adt_id; field_id } ->
           (* Note we can only project fields of structures (not enumerations) *)
           (* Deconstruct the projector type *)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 927684bc..84536005 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -144,7 +144,8 @@ let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
   let type_params = ctx.fun_decl.signature.type_params in
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
-  PrintPure.mk_ast_formatter type_decls fun_decls type_params
+  let gid_conv = ctx.fun_context.gid_conv in
+  PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params
 
 let ty_to_string (ctx : bs_ctx) (ty : ty) : string =
   let fmt = bs_ctx_to_pp_ast_formatter ctx in
@@ -165,14 +166,16 @@ let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string =
   let type_params = sg.type_params in
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
-  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in
+  let gid_conv = ctx.fun_context.gid_conv in
+  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in
   PrintPure.fun_sig_to_string fmt sg
 
 let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
   let type_params = def.signature.type_params in
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
-  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in
+  let gid_conv = ctx.fun_context.gid_conv in
+  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in
   PrintPure.fun_decl_to_string fmt def
 
 (* TODO: move *)
@@ -482,7 +485,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
       let info = A.FunDeclId.Map.find fid fun_infos in
       let input_state = info.stateful in
       let output_state = input_state && gid = None in
-      { can_fail = true; input_state; output_state }
+      { can_fail = info.can_fail; input_state; output_state }
   | A.Assumed aid ->
       {
         can_fail = Assumed.assumed_can_fail aid;
@@ -1663,6 +1666,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
   (* Lookup the signature *)
   let signature = bs_ctx_lookup_local_function_sig def_id bid ctx in
   (* Translate the body, if there is *)
+  let is_global = def.A.is_global in
   let body =
     match body with
     | None -> None
@@ -1723,7 +1727,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
         Some { inputs; inputs_lvs; body }
   in
   (* Assemble the declaration *)
-  let def = { def_id; back_id = bid; basename; signature; body } in
+  let def = { def_id; back_id = bid; basename; signature; is_global; body } in
   (* Debugging *)
   log#ldebug
     (lazy
diff --git a/src/Translate.ml b/src/Translate.ml
index d4d79355..9412b8b8 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -495,9 +495,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
          if
            ((not is_opaque) && config.extract_transparent)
            || (is_opaque && config.extract_opaque)
-         then
-           ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif
-             has_decr_clause def)
+         then if def.is_global
+          then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt qualif def
+          else ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def
+        )
        fls);
     (* Insert unit tests if necessary *)
     if config.test_unit_functions then
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index ccaa9e22..047219ad 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -40,14 +40,16 @@ let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
   let type_params = sg.type_params in
   let type_decls = ctx.type_context.type_decls in
   let fun_decls = ctx.fun_context.fun_decls in
-  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in
+  let gid_conv = ctx.fun_context.gid_conv in
+  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in
   PrintPure.fun_sig_to_string fmt sg
 
 let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
   let type_params = def.signature.type_params in
   let type_decls = ctx.type_context.type_decls in
   let fun_decls = ctx.fun_context.fun_decls in
-  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in
+  let gid_conv = ctx.fun_context.gid_conv in
+  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in
   PrintPure.fun_decl_to_string fmt def
 
 let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string =