Add target alignments for literal types

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.223"
+let supported_charon_version = "0.1.224"

charon-ml/src/generated/Generated_FullAst.ml

@@ -311,6 +311,9 @@ and target_info = {
   target_pointer_size : int;  (** The pointer size of the target in bytes. *)
   is_little_endian : bool;
       (** Whether the target platform uses little endian byte order. *)
+  c_enum_min_size : int;  (** The minimum size of a [[repr(C)]] enum. *)
+  primitive_alignments : (literal_type * int) list;
+      (** Alignments for primitive types. *)
 }
 
 (** The complete data of a Rust crate.

charon-ml/src/generated/Generated_OfJson.ml

@@ -2819,10 +2819,24 @@ and target_info_of_json (ctx : of_json_ctx) (js : json) :
         [
           ("target_pointer_size", target_pointer_size);
           ("is_little_endian", is_little_endian);
+          ("c_enum_min_size", c_enum_min_size);
+          ("primitive_alignments", primitive_alignments);
         ] ->
         let* target_pointer_size = int_of_json ctx target_pointer_size in
         let* is_little_endian = bool_of_json ctx is_little_endian in
-        Ok ({ target_pointer_size; is_little_endian } : target_info)
+        let* c_enum_min_size = int_of_json ctx c_enum_min_size in
+        let* primitive_alignments =
+          index_map_of_json literal_type_of_json int_of_json int_of_json ctx
+            primitive_alignments
+        in
+        Ok
+          ({
+             target_pointer_size;
+             is_little_endian;
+             c_enum_min_size;
+             primitive_alignments;
+           }
+            : target_info)
     | _ -> Error "")
 
 and trait_assoc_const_of_json (ctx : of_json_ctx) (js : json) :

charon-ml/src/generated/Generated_OfPostcard.ml

@@ -2377,7 +2377,19 @@ and target_info_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
   combine_error_msgs st __FUNCTION__
     (let* target_pointer_size = u64_of_postcard ctx st in
      let* is_little_endian = bool_of_postcard ctx st in
-     Ok ({ target_pointer_size; is_little_endian } : target_info))
+     let* c_enum_min_size = u64_of_postcard ctx st in
+     let* primitive_alignments =
+       index_map_of_postcard literal_type_of_postcard u64_of_postcard
+         int_of_postcard ctx st
+     in
+     Ok
+       ({
+          target_pointer_size;
+          is_little_endian;
+          c_enum_min_size;
+          primitive_alignments;
+        }
+         : target_info))
 
 and trait_assoc_const_of_postcard (ctx : of_postcard_ctx) (st : postcard_state)
     : (trait_assoc_const, string) result =

charon/Cargo.toml

@@ -25,7 +25,7 @@ tracing = { version = "0.1", features = ["max_level_trace"] }
 
 [package]
 name = "charon"
-version = "0.1.223"
+version = "0.1.224"
 authors.workspace = true
 edition.workspace = true
 license.workspace = true

charon/src/ast/krate.rs

@@ -201,6 +201,11 @@ pub struct TargetInfo {
     pub target_pointer_size: types::ByteCount,
     /// Whether the target platform uses little endian byte order.
     pub is_little_endian: bool,
+    /// The minimum size of a [`repr(C)`] enum.
+    pub c_enum_min_size: types::ByteCount,
+    /// Alignments for primitive types.
+    #[serde(with = "SeqHashMapToArray::<LiteralTy, ByteCount>")]
+    pub primitive_alignments: SeqHashMap<LiteralTy, ByteCount>,
 }
 
 #[derive(Default, Clone, Drive, DriveMut, SerializeState, DeserializeState)]

charon/src/bin/charon-driver/translate/translate_crate.rs

@@ -492,9 +492,55 @@ impl<'tcx> TranslateCtx<'tcx> {
     pub(crate) fn register_target_info(&mut self) {
         let target_data = &self.tcx.data_layout;
         let triple = self.get_target_triple();
+
+        let mut primitive_alignments = SeqHashMap::new();
+        primitive_alignments.insert(LiteralTy::Bool, target_data.i8_align.bytes());
+        primitive_alignments.insert(LiteralTy::Int(IntTy::I8), target_data.i8_align.bytes());
+        primitive_alignments.insert(LiteralTy::Int(IntTy::I16), target_data.i16_align.bytes());
+        primitive_alignments.insert(LiteralTy::Int(IntTy::I32), target_data.i32_align.bytes());
+        primitive_alignments.insert(LiteralTy::Int(IntTy::I64), target_data.i64_align.bytes());
+        primitive_alignments.insert(LiteralTy::Int(IntTy::I128), target_data.i128_align.bytes());
+        primitive_alignments.insert(
+            LiteralTy::Int(IntTy::Isize),
+            target_data.pointer_align().bytes(),
+        );
+        primitive_alignments.insert(LiteralTy::UInt(UIntTy::U8), target_data.i8_align.bytes());
+        primitive_alignments.insert(LiteralTy::UInt(UIntTy::U16), target_data.i16_align.bytes());
+        primitive_alignments.insert(LiteralTy::UInt(UIntTy::U32), target_data.i32_align.bytes());
+        primitive_alignments.insert(LiteralTy::UInt(UIntTy::U64), target_data.i64_align.bytes());
+        primitive_alignments.insert(
+            LiteralTy::UInt(UIntTy::U128),
+            target_data.i128_align.bytes(),
+        );
+        primitive_alignments.insert(
+            LiteralTy::UInt(UIntTy::Usize),
+            target_data.pointer_align().bytes(),
+        );
+        primitive_alignments.insert(
+            LiteralTy::Float(FloatTy::F16),
+            target_data.f16_align.bytes(),
+        );
+        primitive_alignments.insert(
+            LiteralTy::Float(FloatTy::F32),
+            target_data.f32_align.bytes(),
+        );
+        primitive_alignments.insert(
+            LiteralTy::Float(FloatTy::F64),
+            target_data.f64_align.bytes(),
+        );
+        primitive_alignments.insert(
+            LiteralTy::Float(FloatTy::F128),
+            target_data.f128_align.bytes(),
+        );
+        // INFO: This is not explicitly guaranteed by the reference, but by the implementation of rustc.
+        // https://doc.rust-lang.org/1.97.1/nightly-rustc/src/rustc_ty_utils/layout.rs.html#391
+        primitive_alignments.insert(LiteralTy::Char, target_data.i32_align.bytes());
+
         let info = krate::TargetInfo {
             target_pointer_size: target_data.pointer_size().bytes(),
             is_little_endian: matches!(target_data.endian, rustc_abi::Endian::Little),
+            c_enum_min_size: target_data.c_enum_min_size.size().bytes(),
+            primitive_alignments,
         };
         self.translated.target_information.insert(triple, info);
     }