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.45"
+let supported_charon_version = "0.1.47"

charon-ml/src/GAst.ml

@@ -26,10 +26,8 @@ type fun_id = Expressions.fun_id [@@deriving show, ord]
 type fun_id_or_trait_method_ref = Expressions.fun_id_or_trait_method_ref
 [@@deriving show, ord]
 
-type fun_decl_id = FunDeclId.id
-
 (** A variable *)
-and var = {
+type var = {
   index : var_id;  (** Unique index identifying the variable *)
   name : string option;
       (** Variable name - may be `None` if the variable was introduced by Rust
@@ -38,6 +36,8 @@ and var = {
   var_ty : ty;  (** The variable type *)
 }
 
+and fun_decl_id = FunDeclId.id
+
 (** The id of a translated item. *)
 and any_decl_id =
   | IdType of type_decl_id
@@ -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:
@@ -346,6 +358,10 @@ and fun_sig = {
           (the function in which the closure is defined)
         - the region variables are local to the closure
      *)
+  is_global_initializer : bool;
+      (** Whether this function is in fact the body of a constant/static that we turned into an
+        initializer function.
+     *)
   closure_info : closure_info option;
       (** Additional information if this is the signature of a closure. *)
   generics : generic_params;
@@ -398,30 +414,18 @@ type 'body gfun_decl = {
   signature : fun_sig;
   kind : item_kind;
   body : 'body gexpr_body option;
-  is_global_decl_body : bool;
-}
-[@@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

@@ -324,10 +324,6 @@ and aggregate_kind_of_json (js : json) : (aggregate_kind, string) result =
         Ok (AggregatedClosure (x_0, x_1))
     | _ -> Error "")
 
-and fun_decl_id_of_json (js : json) : (fun_decl_id, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with x -> FunDeclId.id_of_json x | _ -> Error "")
-
 and var_of_json (js : json) : (var, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
@@ -398,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
@@ -563,6 +581,26 @@ and assertion_of_json (js : json) : (assertion, string) result =
         Ok ({ cond; expected } : assertion)
     | _ -> Error "")
 
+and fun_decl_id_of_json (js : json) : (fun_decl_id, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with x -> FunDeclId.id_of_json x | _ -> Error "")
+
+and type_decl_id_of_json (js : json) : (type_decl_id, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with x -> TypeDeclId.id_of_json x | _ -> Error "")
+
+and global_decl_id_of_json (js : json) : (global_decl_id, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with x -> GlobalDeclId.id_of_json x | _ -> Error "")
+
+and trait_decl_id_of_json (js : json) : (trait_decl_id, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with x -> TraitDeclId.id_of_json x | _ -> Error "")
+
+and trait_impl_id_of_json (js : json) : (trait_impl_id, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with x -> TraitImplId.id_of_json x | _ -> Error "")
+
 and any_decl_id_of_json (js : json) : (any_decl_id, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
@@ -749,10 +787,6 @@ and type_var_id_of_json (js : json) : (type_var_id, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with x -> TypeVarId.id_of_json x | _ -> Error "")
 
-and type_decl_id_of_json (js : json) : (type_decl_id, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with x -> TypeDeclId.id_of_json x | _ -> Error "")
-
 and variant_id_of_json (js : json) : (variant_id, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with x -> VariantId.id_of_json x | _ -> Error "")
@@ -766,10 +800,6 @@ and const_generic_var_id_of_json (js : json) :
   combine_error_msgs js __FUNCTION__
     (match js with x -> ConstGenericVarId.id_of_json x | _ -> Error "")
 
-and global_decl_id_of_json (js : json) : (global_decl_id, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with x -> GlobalDeclId.id_of_json x | _ -> Error "")
-
 and type_var_of_json (js : json) : (type_var, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
@@ -993,14 +1023,6 @@ and trait_clause_id_of_json (js : json) : (trait_clause_id, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with x -> TraitClauseId.id_of_json x | _ -> Error "")
 
-and trait_decl_id_of_json (js : json) : (trait_decl_id, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with x -> TraitDeclId.id_of_json x | _ -> Error "")
-
-and trait_impl_id_of_json (js : json) : (trait_impl_id, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with x -> TraitImplId.id_of_json x | _ -> Error "")
-
 and trait_clause_of_json (id_to_file : id_to_file_map) (js : json) :
     (trait_clause, string) result =
   combine_error_msgs js __FUNCTION__
@@ -1278,6 +1300,7 @@ and fun_sig_of_json (id_to_file : id_to_file_map) (js : json) :
         [
           ("is_unsafe", is_unsafe);
           ("is_closure", is_closure);
+          ("is_global_initializer", is_global_initializer);
           ("closure_info", closure_info);
           ("generics", generics);
           ("parent_params_info", parent_params_info);
@@ -1286,6 +1309,7 @@ and fun_sig_of_json (id_to_file : id_to_file_map) (js : json) :
         ] ->
         let* is_unsafe = bool_of_json is_unsafe in
         let* is_closure = bool_of_json is_closure in
+        let* is_global_initializer = bool_of_json is_global_initializer in
         let* closure_info = option_of_json closure_info_of_json closure_info in
         let* generics = generic_params_of_json id_to_file generics in
         let* parent_params_info =
@@ -1297,6 +1321,7 @@ and fun_sig_of_json (id_to_file : id_to_file_map) (js : json) :
           ({
              is_unsafe;
              is_closure;
+             is_global_initializer;
              closure_info;
              generics;
              parent_params_info;
@@ -1450,42 +1475,7 @@ and gfun_decl_of_json (bodies : 'body gexpr_body option list)
         let* signature = fun_sig_of_json id_to_file signature in
         let* kind = item_kind_of_json kind in
         let* body = maybe_opaque_body_of_json bodies body in
-        Ok
-          {
-            def_id;
-            item_meta;
-            signature;
-            kind;
-            body;
-            is_global_decl_body = false;
-          }
-    | _ -> 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
+        Ok { def_id; item_meta; signature; kind; body }
     | _ -> Error "")
 
 (** Deserialize a map from file id to file name.
@@ -1512,17 +1502,17 @@ 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
         [
           ("crate_name", name);
           ("real_crate_name", _);
-          ("id_to_file", id_to_file);
           ("file_id_to_content", file_id_to_content);
           ("all_ids", _);
           ("item_names", _);
+          ("id_to_file", id_to_file);
           ("type_decls", types);
           ("fun_decls", functions);
           ("global_decls", globals);
@@ -1551,7 +1541,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 +1570,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 +1605,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/GAstUtils.ml

@@ -101,10 +101,10 @@ let split_declarations_to_group_maps (decls : declaration_group list) :
   let module G (M : Map.S) = struct
     let add_group (map : M.key g_declaration_group M.t)
         (group : M.key g_declaration_group) : M.key g_declaration_group M.t =
-      match group with
-      | NonRecGroup id -> M.add id group map
-      | RecGroup ids ->
-          List.fold_left (fun map id -> M.add id group map) map ids
+      List.fold_left
+        (fun map id -> M.add id group map)
+        map
+        (g_declaration_group_to_list group)
 
     let create_map (groups : M.key g_declaration_group list) :
         M.key g_declaration_group M.t =

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