Translate global body as a separate initializer function

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.46"
+let supported_charon_version = "0.1.47"

charon-ml/src/GAst.ml

@@ -159,6 +159,18 @@ and item_kind =
           item is a copy of the default item.
        *)
 
+(** A global variable definition (constant or static). *)
+and global_decl = {
+  def_id : global_decl_id;
+  item_meta : item_meta;  (** The meta data associated with the declaration. *)
+  generics : generic_params;
+  ty : ty;
+  kind : item_kind;
+      (** The global kind: "regular" function, trait const declaration, etc. *)
+  body : fun_decl_id;
+      (** The initializer function used to compute the initial value for this constant/static. *)
+}
+
 (** A trait **declaration**.
 
     For instance:
@@ -402,26 +414,15 @@ type 'body gfun_decl = {
 }
 [@@deriving show]
 
-(* Hand-written because the rust equivalent isn't generic *)
-type 'body gglobal_decl = {
-  def_id : GlobalDeclId.id;
-  item_meta : item_meta;
-  generics : generic_params;
-  ty : ty;
-  kind : item_kind;
-  body : 'body;
-}
-[@@deriving show]
-
 (* Hand-written because the rust equivalent isn't generic *)
 
 (** A crate *)
-type ('fun_body, 'global_body) gcrate = {
+type 'fun_body gcrate = {
   name : string;
   declarations : declaration_group list;
   type_decls : type_decl TypeDeclId.Map.t;
   fun_decls : 'fun_body gfun_decl FunDeclId.Map.t;
-  global_decls : 'global_body gglobal_decl GlobalDeclId.Map.t;
+  global_decls : global_decl GlobalDeclId.Map.t;
   trait_decls : trait_decl TraitDeclId.Map.t;
   trait_impls : trait_impl TraitImplId.Map.t;
   source_files : string FileNameMap.t;

charon-ml/src/GAstOfJson.ml

@@ -394,6 +394,28 @@ and item_kind_of_json (js : json) : (item_kind, string) result =
         Ok (TraitImplItem (impl_id, trait_id, item_name, reuses_default))
     | _ -> Error "")
 
+and global_decl_of_json (id_to_file : id_to_file_map) (js : json) :
+    (global_decl, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc
+        [
+          ("def_id", def_id);
+          ("item_meta", item_meta);
+          ("generics", generics);
+          ("ty", ty);
+          ("kind", kind);
+          ("init", init);
+        ] ->
+        let* def_id = global_decl_id_of_json def_id in
+        let* item_meta = item_meta_of_json id_to_file item_meta in
+        let* generics = generic_params_of_json id_to_file generics in
+        let* ty = ty_of_json ty in
+        let* kind = item_kind_of_json kind in
+        let* body = fun_decl_id_of_json init in
+        Ok ({ def_id; item_meta; generics; ty; kind; body } : global_decl)
+    | _ -> Error "")
+
 and global_decl_ref_of_json (js : json) : (global_decl_ref, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
@@ -1461,33 +1483,6 @@ and gfun_decl_of_json (bodies : 'body gexpr_body option list)
           }
     | _ -> Error "")
 
-(* This is written by hand because the corresponding rust type is not type-generic. *)
-and gglobal_decl_of_json (bodies : 'body gexpr_body option list)
-    (id_to_file : id_to_file_map) (js : json) :
-    ('body gexpr_body option gglobal_decl, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc
-        [
-          ("def_id", def_id);
-          ("item_meta", item_meta);
-          ("generics", generics);
-          ("ty", ty);
-          ("kind", kind);
-          ("body", body);
-        ] ->
-        let* global_id = GlobalDeclId.id_of_json def_id in
-        let* item_meta = item_meta_of_json id_to_file item_meta in
-        let* generics = generic_params_of_json id_to_file generics in
-        let* ty = ty_of_json ty in
-        let* kind = item_kind_of_json kind in
-        let* body = maybe_opaque_body_of_json bodies body in
-        let global =
-          { def_id = global_id; item_meta; body; generics; ty; kind }
-        in
-        Ok global
-    | _ -> Error "")
-
 (** Deserialize a map from file id to file name.
 
     In the serialized LLBC, the files in the loc spans are refered to by their
@@ -1512,7 +1507,7 @@ and id_to_file_of_json (js : json) : (id_to_file_map, string) result =
 (* This is written by hand because the corresponding rust type is not type-generic. *)
 and gtranslated_crate_of_json
     (body_of_json : id_to_file_map -> json -> ('body gexpr_body, string) result)
-    (js : json) : (('body, 'body gexpr_body option) gcrate, string) result =
+    (js : json) : ('body gcrate, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc
@@ -1551,7 +1546,7 @@ and gtranslated_crate_of_json
         in
         let* globals =
           vector_of_json global_decl_id_of_json
-            (gglobal_decl_of_json bodies id_to_file)
+            (global_decl_of_json id_to_file)
             globals
         in
         let* trait_decls =
@@ -1580,9 +1575,7 @@ and gtranslated_crate_of_json
         in
         let global_decls =
           GlobalDeclId.Map.of_list
-            (List.map
-               (fun (d : 'body gexpr_body option gglobal_decl) -> (d.def_id, d))
-               globals)
+            (List.map (fun (d : global_decl) -> (d.def_id, d)) globals)
         in
         let trait_decls =
           TraitDeclId.Map.of_list
@@ -1617,7 +1610,7 @@ and gtranslated_crate_of_json
 
 and gcrate_of_json
     (body_of_json : id_to_file_map -> json -> ('body gexpr_body, string) result)
-    (js : json) : (('body, 'body gexpr_body option) gcrate, string) result =
+    (js : json) : ('body gcrate, string) result =
   match js with
   | `Assoc [ ("charon_version", charon_version); ("translated", translated) ] ->
       (* Ensure the version is the one we support. *)

charon-ml/src/LlbcAst.ml

@@ -93,8 +93,5 @@ type expr_body = statement gexpr_body [@@deriving show]
 type fun_body = expr_body [@@deriving show]
 type fun_decl = statement gfun_decl [@@deriving show]
 
-(* TODO: the function id should be an option *)
-type global_decl = FunDeclId.id gglobal_decl [@@deriving show]
-
 (** LLBC crate *)
-type crate = (statement, FunDeclId.id) gcrate
+type crate = statement gcrate

charon-ml/src/LlbcOfJson.ml

@@ -141,97 +141,5 @@ let expr_body_of_json (id_to_file : id_to_file_map) (js : json) :
         Ok body
     | _ -> Error "")
 
-(** Strict type for the number of function declarations (see {!global_to_fun_id} below) *)
-type global_id_converter = { max_fun_id : int } [@@deriving show]
-
-(** Converts a global id to its corresponding function id.
-    To do so, it adds the global id to the number of function declarations :
-    We have the bijection [global_fun_id <=> global_id + fun_id_count].
-*)
-let global_to_fun_id (conv : global_id_converter) (gid : GlobalDeclId.id) :
-    FunDeclId.id =
-  FunDeclId.of_int (GlobalDeclId.to_int gid + conv.max_fun_id)
-
-(** Deserialize a global declaration, and decompose it into a global declaration
-    and a function declaration.
- *)
-let split_global (gid_conv : global_id_converter) global :
-    global_decl * fun_decl =
-  (* Deserialize the global declaration *)
-  let { def_id = global_id; item_meta; body; generics; ty; kind } = global in
-  (* Decompose into a global and a function *)
-  let fun_id = global_to_fun_id gid_conv global.def_id in
-  let signature : fun_sig =
-    {
-      (* Not sure about `is_unsafe` actually *)
-      is_unsafe = false;
-      is_closure = false;
-      closure_info = None;
-      generics;
-      parent_params_info = None;
-      inputs = [];
-      output = ty;
-    }
-  in
-  let global_decl : global_decl =
-    { def_id = global_id; item_meta; body = fun_id; generics; ty; kind }
-  in
-  let fun_decl : fun_decl =
-    {
-      def_id = fun_id;
-      item_meta;
-      signature;
-      kind = RegularItem;
-      body;
-      is_global_decl_body = true;
-    }
-  in
-  (global_decl, fun_decl)
-
 let crate_of_json (js : json) : (crate, string) result =
-  begin
-    let* crate = gcrate_of_json expr_body_of_json js in
-    (* When deserializing the globals, we split the global declarations
-     * between the globals themselves and their bodies, which are simply
-     * functions with no arguments. We add the global bodies to the list
-     * of function declarations; we give fresh ids to these new bodies
-     * by incrementing from the last function id recorded *)
-    let gid_conv =
-      {
-        max_fun_id =
-          List.fold_left
-            (fun acc (id, _) -> max acc (1 + FunDeclId.to_int id))
-            0
-            (FunDeclId.Map.bindings crate.fun_decls);
-      }
-    in
-    let globals, global_bodies =
-      List.split
-        (List.map
-           (fun (_, g) -> split_global gid_conv g)
-           (GlobalDeclId.Map.bindings crate.global_decls))
-    in
-
-    (* Add the global bodies to the list of functions *)
-    let fun_decls =
-      List.fold_left
-        (fun m (d : fun_decl) -> FunDeclId.Map.add d.def_id d m)
-        crate.fun_decls global_bodies
-    in
-    let global_decls =
-      GlobalDeclId.Map.of_list
-        (List.map (fun (d : global_decl) -> (d.def_id, d)) globals)
-    in
-
-    Ok
-      {
-        name = crate.name;
-        declarations = crate.declarations;
-        type_decls = crate.type_decls;
-        fun_decls;
-        global_decls;
-        trait_decls = crate.trait_decls;
-        trait_impls = crate.trait_impls;
-        source_files = crate.source_files;
-      }
-  end
+  gcrate_of_json expr_body_of_json js

charon-ml/src/PrintExpressions.ml

@@ -14,16 +14,16 @@ let var_to_string (v : var) : string =
   | None -> var_id_to_pretty_string v.index
   | Some name -> name ^ "^" ^ VarId.to_string v.index
 
-let var_id_to_string (env : ('a, 'b) fmt_env) (id : VarId.id) : string =
+let var_id_to_string (env : 'a fmt_env) (id : VarId.id) : string =
   match List.find_opt (fun (i, _) -> i = id) env.locals with
   | None -> var_id_to_pretty_string id
   | Some (_, name) -> (
       match name with
       | None -> var_id_to_pretty_string id
       | Some name -> name ^ "^" ^ VarId.to_string id)
 
-let rec projection_to_string (env : ('a, 'b) fmt_env) (s : string)
-    (p : projection) : string =
+let rec projection_to_string (env : 'a fmt_env) (s : string) (p : projection) :
+    string =
   match p with
   | [] -> s
   | pe :: p' ->
@@ -47,11 +47,11 @@ let rec projection_to_string (env : ('a, 'b) fmt_env) (s : string)
       in
       projection_to_string env s p'
 
-let place_to_string (env : ('a, 'b) fmt_env) (p : place) : string =
+let place_to_string (env : 'a fmt_env) (p : place) : string =
   let var = var_id_to_string env p.var_id in
   projection_to_string env var p.projection
 
-let cast_kind_to_string (env : ('a, 'b) fmt_env) (cast : cast_kind) : string =
+let cast_kind_to_string (env : 'a fmt_env) (cast : cast_kind) : string =
   match cast with
   | CastScalar (src, tgt) ->
       "cast<" ^ literal_type_to_string src ^ "," ^ literal_type_to_string tgt
@@ -61,14 +61,14 @@ let cast_kind_to_string (env : ('a, 'b) fmt_env) (cast : cast_kind) : string =
   | CastUnsize (src, tgt) ->
       "unsize<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">"
 
-let nullop_to_string (env : ('a, 'b) fmt_env) (op : nullop) : string =
+let nullop_to_string (env : 'a fmt_env) (op : nullop) : string =
   match op with
   | SizeOf -> "size_of"
   | AlignOf -> "align_of"
   | OffsetOf _ -> "offset_of(?)"
   | UbChecks -> "ub_checks"
 
-let unop_to_string (env : ('a, 'b) fmt_env) (unop : unop) : string =
+let unop_to_string (env : 'a fmt_env) (unop : unop) : string =
   match unop with
   | Not -> "¬"
   | Neg -> "-"
@@ -108,24 +108,23 @@ let assumed_fun_id_to_string (aid : assumed_fun_id) : string =
       let mutability = ref_kind_to_string mutability in
       "@" ^ ty ^ op ^ mutability
 
-let fun_id_to_string (env : ('a, 'b) fmt_env) (fid : fun_id) : string =
+let fun_id_to_string (env : 'a fmt_env) (fid : fun_id) : string =
   match fid with
   | FRegular fid -> fun_decl_id_to_string env fid
   | FAssumed aid -> assumed_fun_id_to_string aid
 
-let fun_id_or_trait_method_ref_to_string (env : ('a, 'b) fmt_env)
+let fun_id_or_trait_method_ref_to_string (env : 'a fmt_env)
     (r : fun_id_or_trait_method_ref) : string =
   match r with
   | TraitMethod (trait_ref, method_name, _) ->
       trait_ref_to_string env trait_ref ^ "::" ^ method_name
   | FunId fid -> fun_id_to_string env fid
 
-let fn_ptr_to_string (env : ('a, 'b) fmt_env) (ptr : fn_ptr) : string =
+let fn_ptr_to_string (env : 'a fmt_env) (ptr : fn_ptr) : string =
   let generics = generic_args_to_string env ptr.generics in
   fun_id_or_trait_method_ref_to_string env ptr.func ^ generics
 
-let constant_expr_to_string (env : ('a, 'b) fmt_env) (cv : constant_expr) :
-    string =
+let constant_expr_to_string (env : 'a fmt_env) (cv : constant_expr) : string =
   match cv.value with
   | CLiteral lit ->
       "(" ^ literal_to_string lit ^ " : " ^ ty_to_string env cv.ty ^ ")"
@@ -135,13 +134,13 @@ let constant_expr_to_string (env : ('a, 'b) fmt_env) (cv : constant_expr) :
       trait_ref ^ const_name
   | CFnPtr fn_ptr -> fn_ptr_to_string env fn_ptr
 
-let operand_to_string (env : ('a, 'b) fmt_env) (op : operand) : string =
+let operand_to_string (env : 'a fmt_env) (op : operand) : string =
   match op with
   | Copy p -> "copy " ^ place_to_string env p
   | Move p -> "move " ^ place_to_string env p
   | Constant cv -> constant_expr_to_string env cv
 
-let rvalue_to_string (env : ('a, 'b) fmt_env) (rv : rvalue) : string =
+let rvalue_to_string (env : 'a fmt_env) (rv : rvalue) : string =
   match rv with
   | Use op -> operand_to_string env op
   | RvRef (p, bk) -> begin