Fix a bunch of multi-target bugs

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.196"
+let supported_charon_version = "0.1.197"

charon-ml/src/generated/Generated_FullAst.ml

@@ -133,8 +133,8 @@ and cli_options = {
           This takes a list of name patterns of the traits to transform, using
           the same syntax as [--include]. *)
   hide_marker_traits : bool;
-      (** Whether to hide various marker traits such as [Sized], [Sync], [Send]
-          and [Destruct] anywhere they show up. This can considerably speed up
+      (** Whether to hide various marker traits such as [Sized], [Sync], and
+          [Send] anywhere they show up. This can considerably speed up
           translation. *)
   remove_adt_clauses : bool;
       (** Remove trait clauses from type declarations. Must be combined with

charon-ml/src/generated/Generated_OfJson.ml

@@ -2551,6 +2551,7 @@ and layout_of_json (ctx : of_json_ctx) (js : json) : (layout, string) result =
           ("discriminator", discriminator);
           ("uninhabited", uninhabited);
           ("variant_layouts", variant_layouts);
+          ("repr", repr);
         ] ->
         let* size = option_of_json int_of_json ctx size in
         let* align = option_of_json int_of_json ctx align in
@@ -2562,8 +2563,9 @@ and layout_of_json (ctx : of_json_ctx) (js : json) : (layout, string) result =
           index_vec_of_json variant_id_of_json variant_layout_of_json ctx
             variant_layouts
         in
+        let* repr = repr_options_of_json ctx repr in
         Ok
-          ({ size; align; discriminator; uninhabited; variant_layouts }
+          ({ size; align; discriminator; uninhabited; variant_layouts; repr }
             : layout)
     | _ -> Error "")
 
@@ -2997,7 +2999,6 @@ 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
@@ -3008,18 +3009,8 @@ and type_decl_of_json (ctx : of_json_ctx) (js : json) :
           index_map_of_json string_of_json layout_of_json int_of_json ctx layout
         in
         let* ptr_metadata = 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;
-             repr;
-           }
+          ({ def_id; item_meta; generics; src; kind; layout; ptr_metadata }
             : type_decl)
     | _ -> Error "")
 

charon-ml/src/generated/Generated_OfPostcard.ml

@@ -2169,7 +2169,10 @@ and layout_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
        index_vec_of_postcard variant_id_of_postcard variant_layout_of_postcard
          ctx st
      in
-     Ok ({ size; align; discriminator; uninhabited; variant_layouts } : layout))
+     let* repr = repr_options_of_postcard ctx st in
+     Ok
+       ({ size; align; discriminator; uninhabited; variant_layouts; repr }
+         : layout))
 
 and local_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
     (local, string) result =
@@ -2512,9 +2515,8 @@ and type_decl_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
          int_of_postcard ctx st
      in
      let* ptr_metadata = ptr_metadata_of_postcard ctx st in
-     let* repr = option_of_postcard repr_options_of_postcard ctx st in
      Ok
-       ({ def_id; item_meta; generics; src; kind; layout; ptr_metadata; repr }
+       ({ def_id; item_meta; generics; src; kind; layout; ptr_metadata }
          : type_decl))
 
 and type_decl_kind_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :

charon-ml/src/generated/Generated_Types.ml

@@ -1069,6 +1069,9 @@ and layout = {
   variant_layouts : variant_layout list;
       (** Map from [VariantId] to the corresponding field layouts. Structs are
           modeled as having exactly one variant, unions as having no variant. *)
+  repr : repr_options;
+      (** The representation options of this type declaration as annotated by
+          the user. *)
 }
 
 (** An item name/path
@@ -1189,9 +1192,6 @@ and type_decl = {
           layout, the target has no entry. *)
   ptr_metadata : ptr_metadata;
       (** The metadata associated with a pointer to the type. *)
-  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 =

charon/Cargo.toml

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

charon/src/ast/types.rs

@@ -401,7 +401,6 @@ pub enum Discriminator {
 /// some of the layout parts are not available.
 #[derive(
     Debug,
-    Default,
     Clone,
     PartialEq,
     Eq,
@@ -431,6 +430,10 @@ pub struct Layout {
     /// Map from `VariantId` to the corresponding field layouts. Structs are modeled as having
     /// exactly one variant, unions as having no variant.
     pub variant_layouts: IndexVec<VariantId, VariantLayout>,
+    /// The representation options of this type declaration as annotated by the user.
+    #[drive(skip)]
+    #[serde_state(stateless)]
+    pub repr: ReprOptions,
 }
 
 /// The metadata stored in a pointer. That's the information stored in pointers alongside
@@ -458,9 +461,10 @@ pub enum PtrMetadata {
 
 /// Describes which layout algorithm is used for representing the corresponding type.
 /// Depends on the `#[repr(...)]` used.
-#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+#[derive(Debug, Default, Clone, PartialEq, Eq, Serialize, Deserialize)]
 pub enum ReprAlgorithm {
     /// The default layout algorithm. Used without an explicit `ŗepr` or for `repr(Rust)`.
+    #[default]
     Rust,
     /// The C layout algorithm as enforced by `repr(C)`.
     C,
@@ -480,7 +484,7 @@ pub enum AlignmentModifier {
 /// or the compiler internal `#[repr(linear)]`. Similarly, enum discriminant representations
 /// are encoded in [`Variant::discriminant`] and [`Discriminator`] instead.
 /// This only stores whether the discriminant type was derived from an explicit annotation.
-#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+#[derive(Debug, Default, Clone, PartialEq, Eq, Serialize, Deserialize)]
 pub struct ReprOptions {
     pub repr_algo: ReprAlgorithm,
     pub align_modif: Option<AlignmentModifier>,
@@ -518,11 +522,6 @@ pub struct TypeDecl {
     pub layout: SeqHashMap<TargetTriple, Layout>,
     /// The metadata associated with a pointer to the type.
     pub ptr_metadata: PtrMetadata,
-    /// The representation options of this type declaration as annotated by the user.
-    /// Is `None` for foreign type declarations.
-    #[drive(skip)]
-    #[serde_state(stateless)]
-    pub repr: Option<ReprOptions>,
 }
 
 generate_index_type!(VariantId, "Variant");

charon/src/ast/types_utils.rs

@@ -1426,12 +1426,6 @@ impl<'a, T> Substituted<'a, T> {
 }
 
 impl TypeDecl {
-    pub fn is_c_repr(&self) -> bool {
-        self.repr
-            .as_ref()
-            .is_some_and(|repr| repr.repr_algo == ReprAlgorithm::C)
-    }
-
     pub fn get_field(&self, variant: Option<VariantId>, field: FieldId) -> Option<&Field> {
         let fields = match &self.kind {
             TypeDeclKind::Struct(fields) | TypeDeclKind::Union(fields) => fields,
@@ -1507,6 +1501,10 @@ impl Layout {
             false
         }
     }
+
+    pub fn is_c_repr(&self) -> bool {
+        self.repr.repr_algo == ReprAlgorithm::C
+    }
 }
 
 impl ReprOptions {

charon/src/ast/visitor.rs

@@ -43,7 +43,7 @@ use derive_generic_visitor::*;
     skip((), String, bool),
     // Types that we unconditionally explore.
     drive(
-        AbortKind, Assert, BinOp, BorrowKind, BuiltinAssertKind, BuiltinFunId, BuiltinIndexOp, BuiltinTy,
+        Assert, BinOp, BorrowKind, BuiltinAssertKind, BuiltinFunId, BuiltinIndexOp, BuiltinTy,
         Call, CastKind, ClosureInfo, ClosureKind, ConstGenericParam, ConstGenericVarId,
         Disambiguator, DynPredicate, Field, FieldId, FieldProjKind, File, FloatTy, FloatValue,
         FnOperand, FunId, FnPtrKind, FunSig, IntegerTy, IntTy, UIntTy, Literal, LiteralTy,
@@ -79,7 +79,7 @@ use derive_generic_visitor::*;
         for<T: AstVisitable> Binder<T>,
         llbc_block: llbc_ast::Block, llbc_statement: llbc_ast::Statement,
         ullbc_statement: ullbc_ast::Statement, ullbc_terminator: ullbc_ast::Terminator,
-        AggregateKind, FnPtr, ItemSource, ItemMeta, Name, Span, ConstantExpr, ProjectionElem,
+        AbortKind, AggregateKind, FnPtr, ItemSource, ItemMeta, Name, Span, ConstantExpr, ProjectionElem,
         FunDeclId, GlobalDeclId, TypeDeclId, TraitDeclId, TraitImplId, FileId,
         FunDecl, GlobalDecl, TypeDecl, TraitDecl, TraitImpl,
     )

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

@@ -436,8 +436,6 @@ impl<'tcx> ItemTransCtx<'tcx, '_> {
         // Get the kind of the type decl -- is it a closure?
         let src = self.get_item_source(span, def)?;
 
-        let mut repr: Option<ReprOptions> = None;
-
         // Translate type body
         let kind = match &def.kind {
             _ if item_meta.opacity.is_opaque() => Ok(TypeDeclKind::Opaque),
@@ -447,10 +445,7 @@ impl<'tcx> ItemTransCtx<'tcx, '_> {
                 self.error_on_impl_expr_error = false;
                 self.translate_ty(span, ty).map(TypeDeclKind::Alias)
             }
-            hax::FullDefKind::Adt { repr: hax_repr, .. } => {
-                repr = Some(self.translate_repr_options(hax_repr));
-                self.translate_adt_def(trans_id, span, &item_meta, def)
-            }
+            hax::FullDefKind::Adt { .. } => self.translate_adt_def(trans_id, span, &item_meta, def),
             hax::FullDefKind::Closure { args, .. } => self.translate_closure_adt(span, args),
             _ => panic!("Unexpected item when translating types: {def:?}"),
         };
@@ -460,7 +455,7 @@ impl<'tcx> ItemTransCtx<'tcx, '_> {
             Err(err) => TypeDeclKind::Error(err.msg),
         };
         let layout = self
-            .translate_layout(def.this())
+            .translate_layout(def)
             .into_iter()
             .map(|l| (self.get_target_triple(), l))
             .collect();
@@ -473,7 +468,6 @@ impl<'tcx> ItemTransCtx<'tcx, '_> {
             src,
             layout,
             ptr_metadata,
-            repr,
         };
 
         Ok(type_def)

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

@@ -607,7 +607,6 @@ impl<'tcx> ItemTransCtx<'tcx, '_> {
             layout,
             // A vtable struct is always sized
             ptr_metadata: PtrMetadata::None,
-            repr: None,
         })
     }
 }

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

@@ -460,7 +460,8 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
     /// Translates the layout as queried from rustc into
     /// the more restricted [`Layout`].
     #[tracing::instrument(skip(self))]
-    pub fn translate_layout(&self, item: &hax::ItemRef) -> Option<Layout> {
+    pub fn translate_layout(&mut self, def: &hax::FullDef<'tcx>) -> Option<Layout> {
+        let item = def.this();
         use rustc_abi as r_abi;
 
         fn translate_variant_layout(
@@ -651,12 +652,18 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
             r_abi::Variants::Empty => (None, IndexVec::new()),
         };
 
+        let repr = match &def.kind {
+            hax::FullDefKind::Adt { repr: hax_repr, .. } => self.translate_repr_options(hax_repr),
+            _ => ReprOptions::default(),
+        };
+
         Some(Layout {
             size,
             align,
             discriminator,
             uninhabited: layout.is_uninhabited(),
             variant_layouts,
+            repr,
         })
     }
 
@@ -691,6 +698,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
                         tagger: vec![],
                         uninhabited: false,
                     }]),
+                    repr: ReprOptions::default(),
                 })
             }
             _ => raise_error!(

charon/src/export/multi_target.rs

@@ -125,6 +125,10 @@ impl CrateMerger {
                 fn enter_trait_impl_id(&mut self, id: &mut TraitImplId) {
                     *id += self.trait_impl_offset;
                 }
+                fn visit_abort_kind(&mut self, _x: &mut AbortKind) -> ControlFlow<Self::Break> {
+                    // Don't modify the name found there
+                    ControlFlow::Continue(())
+                }
                 fn enter_name(&mut self, name: &mut Name) {
                     name.name.push(PathElem::Target(self.target.clone()));
                 }
@@ -571,7 +575,10 @@ fn normalize_item(
         .retain(|elem| !matches!(elem, PathElem::Target(_)));
 
     strip_unstable_attributes(&mut item);
-    // Don't compare source text: span is enough, and it can have OS-specific line endings.
+    // Ignore source text and spans: if the items are otherwise identical, it's ok to just pick one
+    // of the identical instances wrt spans/source.
+    item.as_mut()
+        .dyn_visit_mut(|span: &mut Span| *span = Span::dummy());
     item.as_mut().item_meta().source_text = None;
     if let ItemByVal::Type(ty_decl) = &mut item {
         // Layouts are allowed to differ per-target.

charon/src/options.rs

@@ -164,7 +164,7 @@ pub struct CliOpts {
     #[clap(long, alias = "remove-associated-types")]
     #[serde(default)]
     pub lift_associated_types: Vec<String>,
-    /// Whether to hide various marker traits such as `Sized`, `Sync`, `Send` and `Destruct`
+    /// Whether to hide various marker traits such as `Sized`, `Sync`, and `Send`
     /// anywhere they show up. This can considerably speed up translation.
     #[clap(long)]
     #[serde(default)]
@@ -683,10 +683,6 @@ impl TranslateOptions {
             ])
             .into_iter()
             .flatten()
-            .chain(
-                (options.hide_marker_traits && !options.precise_drops)
-                    .then_some("core::marker::Destruct"),
-            )
             .chain(options.hide_allocator.then_some("core::alloc::Allocator"))
             .filter_map(|s| parse_pattern(s).ok())
             .collect_vec();

charon/tests/help-output.txt

@@ -96,7 +96,7 @@ Options:
           Transform the associate types of traits to be type parameters instead. This takes a list of name patterns of the traits to transform, using the same syntax as `--include`
 
       --hide-marker-traits
-          Whether to hide various marker traits such as `Sized`, `Sync`, `Send` and `Destruct` anywhere they show up. This can considerably speed up translation
+          Whether to hide various marker traits such as `Sized`, `Sync`, and `Send` anywhere they show up. This can considerably speed up translation
 
       --remove-adt-clauses
           Remove trait clauses from type declarations. Must be combined with `--lift-associated-types` for type declarations that use trait associated types in their fields, otherwise this will result in errors