Compute layouts on demand

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.127"
+let supported_charon_version = "0.1.128"

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -1436,6 +1436,26 @@ and region_var_of_json (ctx : of_json_ctx) (js : json) :
         Ok ({ index; name } : region_var)
     | _ -> Error "")
 
+and repr_options_of_json (ctx : of_json_ctx) (js : json) :
+    (repr_options, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc
+        [
+          ("align", align);
+          ("pack", pack);
+          ("c", c);
+          ("transparent", transparent);
+          ("explicit_discr_type", explicit_discr_type);
+        ] ->
+        let* align = option_of_json int_of_json ctx align in
+        let* pack = option_of_json int_of_json ctx pack in
+        let* c = bool_of_json ctx c in
+        let* transparent = bool_of_json ctx transparent in
+        let* explicit_discr_type = bool_of_json ctx explicit_discr_type in
+        Ok ({ align; pack; c; transparent; explicit_discr_type } : repr_options)
+    | _ -> Error "")
+
 and rvalue_of_json (ctx : of_json_ctx) (js : json) : (rvalue, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
@@ -1884,6 +1904,7 @@ and type_decl_of_json (ctx : of_json_ctx) (js : json) :
           ("kind", kind);
           ("layout", layout);
           ("ptr_metadata", ptr_metadata);
+          ("repr", repr);
         ] ->
         let* def_id = type_decl_id_of_json ctx def_id in
         let* item_meta = item_meta_of_json ctx item_meta in
@@ -1894,8 +1915,18 @@ and type_decl_of_json (ctx : of_json_ctx) (js : json) :
         let* ptr_metadata =
           option_of_json ptr_metadata_of_json ctx ptr_metadata
         in
+        let* repr = option_of_json repr_options_of_json ctx repr in
         Ok
-          ({ def_id; item_meta; generics; src; kind; layout; ptr_metadata }
+          ({
+             def_id;
+             item_meta;
+             generics;
+             src;
+             kind;
+             layout;
+             ptr_metadata;
+             repr;
+           }
             : type_decl)
     | _ -> Error "")
 

charon-ml/src/generated/Generated_Types.ml

@@ -846,6 +846,24 @@ and ptr_metadata =
       (** Metadata for [dyn Trait] and user-defined types that directly or
           indirectly contain a [dyn Trait]. *)
 
+(** The representation options as annotated by the user.
+
+    If all are false/None, then this is equivalent to [#[repr(Rust)]]. Some
+    combinations are ruled out by the compiler, e.g. align and pack.
+
+    NOTE: This does not include less common/unstable representations such as
+    [#[repr(simd)]] or the compiler internal [#[repr(linear)]]. Similarly, enum
+    discriminant representations are encoded in [[Variant::discriminant]] and
+    [[DiscriminantLayout]] instead. This only stores whether the discriminant
+    type was derived from an explicit annotation. *)
+and repr_options = {
+  align : int option;
+  pack : int option;
+  c : bool;
+  transparent : bool;
+  explicit_discr_type : bool;
+}
+
 (** Describes how we represent the active enum variant in memory. *)
 and tag_encoding =
   | Direct
@@ -891,6 +909,9 @@ and type_decl = {
           are unable to obtain the info. See
           [translate_types::{impl ItemTransCtx}::translate_ptr_metadata] for
           more details. *)
+  repr : repr_options option;
+      (** The representation options of this type declaration as annotated by
+          the user. Is [None] for foreign type declarations. *)
 }
 
 and type_decl_kind =
@@ -919,9 +940,9 @@ and variant = {
   fields : field list;
   discriminant : scalar_value;
       (** The discriminant value outputted by [std::mem::discriminant] for this
-          variant. This is different than the discriminant stored in memory (the
-          one controlled by [repr]). That one is described by
-          [[DiscriminantLayout]] and [[TagEncoding]]. *)
+          variant. This can be different than the discriminant stored in memory
+          (called [tag]). That one is described by [[DiscriminantLayout]] and
+          [[TagEncoding]]. *)
 }
 
 and variant_id = (VariantId.id[@visitors.opaque])

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.127"
+version = "0.1.128"
 authors = [
     "Son Ho <[email protected]>",
     "Guillaume Boisseau <[email protected]>",
@@ -49,7 +49,7 @@ colored = "2.0.4"
 convert_case = "0.6.0"
 crates_io_api = { version = "0.11.0", optional = true }
 derive_generic_visitor = "0.2.0"
-either = "1.15.0"
+either = { version = "1.15.0", features = ["serde"] }
 env_logger = { version = "0.11", features = ["color"] }
 flate2 = { version = "1.0.34", optional = true }
 indexmap = { version = "2.7.1", features = ["serde"] }