diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index b14cdfef3..b5f8e3708 100644 --- a/charon-ml/src/CharonVersion.ml +++ b/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" diff --git a/charon-ml/src/generated/Generated_FullAst.ml b/charon-ml/src/generated/Generated_FullAst.ml index 086645763..9b04b5184 100644 --- a/charon-ml/src/generated/Generated_FullAst.ml +++ b/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 diff --git a/charon-ml/src/generated/Generated_OfJson.ml b/charon-ml/src/generated/Generated_OfJson.ml index 1a5e3fff3..2b6b74ab2 100644 --- a/charon-ml/src/generated/Generated_OfJson.ml +++ b/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 "") diff --git a/charon-ml/src/generated/Generated_OfPostcard.ml b/charon-ml/src/generated/Generated_OfPostcard.ml index de9f4ec1c..a31da29b8 100644 --- a/charon-ml/src/generated/Generated_OfPostcard.ml +++ b/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) : diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index 6afea2ee6..58608687f 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/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 = diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 5a9f418ab..6c6bd0976 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -252,7 +252,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" [[package]] name = "charon" -version = "0.1.196" +version = "0.1.197" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index bde3b9aa3..ed03aa36b 100644 --- a/charon/Cargo.toml +++ b/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 diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 332fe84d2..13d297337 100644 --- a/charon/src/ast/types.rs +++ b/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, + /// 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, @@ -518,11 +522,6 @@ pub struct TypeDecl { pub layout: SeqHashMap, /// 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, } generate_index_type!(VariantId, "Variant"); diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 3166d14e8..be6f41af3 100644 --- a/charon/src/ast/types_utils.rs +++ b/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, 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 { diff --git a/charon/src/ast/visitor.rs b/charon/src/ast/visitor.rs index 3b226bc58..2f33b2255 100644 --- a/charon/src/ast/visitor.rs +++ b/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 Binder, 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, ) diff --git a/charon/src/bin/charon-driver/translate/translate_items.rs b/charon/src/bin/charon-driver/translate/translate_items.rs index e3797edc0..136cfb510 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/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 = 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) diff --git a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs index 569ca133a..b0a65aac1 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/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, }) } } diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 6dde2193e..63a20fc6c 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/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 { + pub fn translate_layout(&mut self, def: &hax::FullDef<'tcx>) -> Option { + 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!( diff --git a/charon/src/export/multi_target.rs b/charon/src/export/multi_target.rs index 184a7cad8..68ba12e54 100644 --- a/charon/src/export/multi_target.rs +++ b/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 { + // 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. diff --git a/charon/src/options.rs b/charon/src/options.rs index e1c0b3712..c94cd2fd0 100644 --- a/charon/src/options.rs +++ b/charon/src/options.rs @@ -164,7 +164,7 @@ pub struct CliOpts { #[clap(long, alias = "remove-associated-types")] #[serde(default)] pub lift_associated_types: Vec, - /// 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(); diff --git a/charon/tests/help-output.txt b/charon/tests/help-output.txt index d282a4163..dd724b5aa 100644 --- a/charon/tests/help-output.txt +++ b/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 diff --git a/charon/tests/layout.json b/charon/tests/layout.json index de9b3cfbc..f6e661855 100644 --- a/charon/tests/layout.json +++ b/charon/tests/layout.json @@ -16,7 +16,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::GenericStruct": null, "test_crate::UnsizedStruct": { @@ -35,7 +41,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::SimpleEnum": { "size": 1, @@ -121,7 +133,13 @@ ] ] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::SimpleAdt": { "size": 24, @@ -247,7 +265,13 @@ ] ] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::NicheAdt": { "size": 4, @@ -308,7 +332,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::IsAZST": { "size": 0, @@ -323,7 +353,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::GenericWithKnownLayout": { "size": 16, @@ -341,7 +377,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::Reordered": { "size": 8, @@ -360,7 +402,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::NotReordered": { "size": 12, @@ -379,7 +427,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "C", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::Packed": { "size": 6, @@ -398,7 +452,15 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": { + "Pack": 1 + }, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::UninhabitedVariant": { "size": 4, @@ -420,7 +482,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::UninhabitedVariant2": { "size": 8, @@ -482,7 +550,13 @@ ] ] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::Uninhabited": { "size": 0, @@ -499,7 +573,13 @@ "uninhabited": true, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::DiscriminantInNicheOfField": { "size": 16, @@ -560,7 +640,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::MaybeUninitInt": { "size": 4, @@ -578,7 +664,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::PackIntsUnion": { "size": 8, @@ -596,7 +688,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::NonZeroNiche": { "size": 4, @@ -691,7 +789,13 @@ ] ] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::ArbitraryDiscriminants": { "size": 32, @@ -815,7 +919,13 @@ ] ] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": true + } }, "test_crate::MyOrder": { "size": 1, @@ -935,7 +1045,13 @@ ] ] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": true + } }, "test_crate::WithNicheAndUninhabited": { "size": 4, @@ -1003,7 +1119,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::GenericUnsized": null, "test_crate::GenericButFixedSize": { @@ -1065,7 +1187,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::MaxBitsDiscr": { "size": 16, @@ -1151,7 +1279,13 @@ ] ] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": true + } }, "test_crate::SingleVariantButNonZero": { "size": 0, @@ -1173,7 +1307,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::NonAdtAlias": null, "test_crate::Tuple": { @@ -1192,7 +1332,13 @@ "uninhabited": false, "tagger": [] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::Usize": { "size": 8, @@ -1201,7 +1347,13 @@ "Known": 0 }, "uninhabited": false, - "variant_layouts": [] + "variant_layouts": [], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::Ref": { "size": 8, @@ -1210,7 +1362,13 @@ "Known": 0 }, "uninhabited": false, - "variant_layouts": [] + "variant_layouts": [], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } }, "test_crate::HasInvalidDiscr": { "size": 1, @@ -1332,6 +1490,12 @@ ] ] } - ] + ], + "repr": { + "repr_algo": "Rust", + "align_modif": null, + "transparent": false, + "explicit_discr_type": false + } } } \ No newline at end of file diff --git a/charon/tests/ui/hide-marker-traits.out b/charon/tests/ui/hide-marker-traits.out index 15b2e5677..511f66293 100644 --- a/charon/tests/ui/hide-marker-traits.out +++ b/charon/tests/ui/hide-marker-traits.out @@ -1,5 +1,17 @@ # Final LLBC before serialization: +// Full name: core::marker::Destruct +#[lang_item("destruct")] +pub trait Destruct +{ + fn drop_in_place = drop_in_place + non-dyn-compatible +} + +// Full name: core::marker::Destruct::drop_in_place +unsafe fn drop_in_place(_1: *mut Self) += + // Full name: test_crate::Idx trait Idx diff --git a/charon/tests/ui/multi-target/issue-1182-dedup-impls.out b/charon/tests/ui/multi-target/issue-1182-dedup-impls.out new file mode 100644 index 000000000..38fe9012f --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1182-dedup-impls.out @@ -0,0 +1,55 @@ +#[lang_item("meta_sized")] +pub trait core::marker::MetaSized + +pub trait test_crate::Foo +{ + parent_clause0 : [@TraitClause0]: core::marker::MetaSized + fn method = test_crate::Foo::method[Self] + non-dyn-compatible +} + +pub fn test_crate::Foo::method() -> u32 +where + [@TraitClause0]: test_crate::Foo, += + +pub struct test_crate::Struct {} + +pub fn test_crate::{impl test_crate::Foo for test_crate::Struct}::method::i686-unknown-linux-gnu() -> u32 +{ + let _0: u32; // return + + _0 = const 32 : u32 + return +} + +pub fn test_crate::{impl test_crate::Foo for test_crate::Struct}::method::x86_64-unknown-linux-gnu() -> u32 +{ + let _0: u32; // return + + _0 = const 64 : u32 + return +} + +pub fn test_crate::{impl test_crate::Foo for test_crate::Struct}::method() -> u32 += target_dispatch { + x86_64-unknown-linux-gnu => test_crate::{impl test_crate::Foo for test_crate::Struct}::method::x86_64-unknown-linux-gnu, + i686-unknown-linux-gnu => test_crate::{impl test_crate::Foo for test_crate::Struct}::method::i686-unknown-linux-gnu, +} + +// Full name: test_crate::{impl test_crate::Foo for test_crate::Struct} +impl test_crate::Foo for test_crate::Struct { + parent_clause0 = {built_in impl core::marker::MetaSized for test_crate::Struct} + fn method = test_crate::{impl test_crate::Foo for test_crate::Struct}::method + non-dyn-compatible +} + +pub fn test_crate::call_method() -> u32 +{ + let _0: u32; // return + + _0 = test_crate::{impl test_crate::Foo for test_crate::Struct}::method() + return +} + + diff --git a/charon/tests/ui/multi-target/issue-1182-dedup-impls.rs b/charon/tests/ui/multi-target/issue-1182-dedup-impls.rs new file mode 100644 index 000000000..75f28116f --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1182-dedup-impls.rs @@ -0,0 +1,24 @@ +//@ charon-args=--targets=x86_64-unknown-linux-gnu,i686-unknown-linux-gnu +pub trait Foo { + fn method() -> u32; +} + +pub struct Struct; + +#[cfg(target_pointer_width = "64")] +impl Foo for Struct { + fn method() -> u32 { + 64 + } +} + +#[cfg(target_pointer_width = "32")] +impl Foo for Struct { + fn method() -> u32 { + 32 + } +} + +pub fn call_method() -> u32 { + ::method() +} diff --git a/charon/tests/ui/multi-target/issue-1184-missing-type-var.out b/charon/tests/ui/multi-target/issue-1184-missing-type-var.out new file mode 100644 index 000000000..7c96197c3 --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1184-missing-type-var.out @@ -0,0 +1,33 @@ +#[lang_item("meta_sized")] +pub trait core::marker::MetaSized + +#[lang_item("sized")] +pub trait core::marker::Sized +{ + parent_clause0 : [@TraitClause0]: core::marker::MetaSized + non-dyn-compatible +} + +#[lang_item("phantom_data")] +pub struct core::marker::PhantomData {} + +pub struct test_crate::Foo +where + [@TraitClause0]: core::marker::Sized, +{ + core::marker::PhantomData, +} + +pub fn test_crate::{test_crate::Foo[@TraitClause0]}::bar() +where + [@TraitClause0]: core::marker::Sized, +{ + let _0: (); // return + + _0 = () + loop { + continue 0 + } +} + + diff --git a/charon/tests/ui/multi-target/issue-1184-missing-type-var.rs b/charon/tests/ui/multi-target/issue-1184-missing-type-var.rs new file mode 100644 index 000000000..1bde2f346 --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1184-missing-type-var.rs @@ -0,0 +1,8 @@ +//@ charon-args=--targets=x86_64-unknown-linux-gnu,i686-unknown-linux-gnu +pub struct Foo(core::marker::PhantomData); + +impl Foo { + pub fn bar() { + loop {} + } +} diff --git a/charon/tests/ui/multi-target/issue-1185-1-inline-const.out b/charon/tests/ui/multi-target/issue-1185-1-inline-const.out new file mode 100644 index 000000000..6c8c63874 --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1185-1-inline-const.out @@ -0,0 +1,29 @@ +pub fn core::num::{u32}::MAX() -> u32 += + +pub const core::num::{u32}::MAX: u32 = core::num::{u32}::MAX() + +pub fn test_crate::const_time_array_copy_mwe<'_0, const N : usize>(_a_1: &'_0 mut [u8; N]) +{ + let _0: (); // return + let _a_1: &'1 mut [u8; N]; // arg #1 + let _2: bool; // anonymous local + let _3: usize; // anonymous local + + storage_live(_2) + storage_live(_3) + _3 = cast(copy core::num::{u32}::MAX) + _2 = const N <= move _3 + if move _2 { + } else { + storage_dead(_3) + panic(core::panicking::panic) + } + storage_dead(_3) + storage_dead(_2) + _0 = () + _0 = () + return +} + + diff --git a/charon/tests/ui/multi-target/issue-1185-1-inline-const.rs b/charon/tests/ui/multi-target/issue-1185-1-inline-const.rs new file mode 100644 index 000000000..b6a9b42cb --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1185-1-inline-const.rs @@ -0,0 +1,6 @@ +//@ charon-args=--targets=x86_64-unknown-linux-gnu,i686-unknown-linux-gnu +pub fn const_time_array_copy_mwe(_a: &mut [u8; N]) { + const { + assert!(N <= u32::MAX as usize); + } +} diff --git a/charon/tests/ui/multi-target/issue-1185-2-generic-make.out b/charon/tests/ui/multi-target/issue-1185-2-generic-make.out new file mode 100644 index 000000000..70c1bba8d --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1185-2-generic-make.out @@ -0,0 +1,45 @@ +#[lang_item("destruct")] +pub trait core::marker::Destruct +{ + fn drop_in_place = core::marker::Destruct::drop_in_place + non-dyn-compatible +} + +unsafe fn core::marker::Destruct::drop_in_place(_1: *mut Self) += + +pub struct test_crate::State { + _h: H, +} + +unsafe fn test_crate::State::{impl core::marker::Destruct for test_crate::State}::drop_in_place(_1: *mut test_crate::State) += + +// Full name: test_crate::State::{impl core::marker::Destruct for test_crate::State} +impl core::marker::Destruct for test_crate::State { + fn drop_in_place = test_crate::State::{impl core::marker::Destruct for test_crate::State}::drop_in_place + non-dyn-compatible +} + +pub fn test_crate::caller(h_1: H) +{ + let _0: (); // return + let h_1: H; // arg #1 + let _2: test_crate::State; // anonymous local + let _3: H; // anonymous local + + _0 = () + storage_live(_2) + storage_live(_3) + _3 = move h_1 + _2 = test_crate::State { _h: move _3 } + conditional_drop[{built_in impl core::marker::Destruct for H}::drop_in_place] _3 + storage_dead(_3) + conditional_drop[test_crate::State::{impl core::marker::Destruct for test_crate::State}::drop_in_place] _2 + storage_dead(_2) + _0 = () + conditional_drop[{built_in impl core::marker::Destruct for H}::drop_in_place] h_1 + return +} + + diff --git a/charon/tests/ui/multi-target/issue-1185-2-generic-make.rs b/charon/tests/ui/multi-target/issue-1185-2-generic-make.rs new file mode 100644 index 000000000..84d2a6e19 --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1185-2-generic-make.rs @@ -0,0 +1,9 @@ +//@ charon-args=--targets=x86_64-unknown-linux-gnu,i686-unknown-linux-gnu +//@ charon-args=--hide-marker-traits +pub struct State { + _h: H, +} + +pub fn caller(h: H) { + let _ = State { _h: h }; +} diff --git a/charon/tests/ui/multi-target/issue-1185-3-box-drop-glue.out b/charon/tests/ui/multi-target/issue-1185-3-box-drop-glue.out new file mode 100644 index 000000000..9c20ce69b --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1185-3-box-drop-glue.out @@ -0,0 +1,20 @@ +#[lang_item("global_alloc_ty")] +pub struct alloc::alloc::Global {} + +unsafe fn alloc::boxed::Box::{impl core::marker::Destruct for alloc::boxed::Box}::drop_in_place(_1: *mut alloc::boxed::Box) += + +pub fn test_crate::mono() -> u32 +{ + let _0: u32; // return + let _b_1: alloc::boxed::Box; // local + + storage_live(_b_1) + _b_1 = @BoxNew(const 0 : u32) + _0 = const 0 : u32 + conditional_drop[alloc::boxed::Box::{impl core::marker::Destruct for alloc::boxed::Box}::drop_in_place] _b_1 + storage_dead(_b_1) + return +} + + diff --git a/charon/tests/ui/multi-target/issue-1185-3-box-drop-glue.rs b/charon/tests/ui/multi-target/issue-1185-3-box-drop-glue.rs new file mode 100644 index 000000000..d58f05e1b --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1185-3-box-drop-glue.rs @@ -0,0 +1,6 @@ +//@ charon-args=--targets=x86_64-unknown-linux-gnu,i686-unknown-linux-gnu +//@ charon-args=--hide-marker-traits +pub fn mono() -> u32 { + let _b = Box::new(0u32); + 0 +} diff --git a/charon/tests/ui/multi-target/issue-1185-4-wrapping-add.out b/charon/tests/ui/multi-target/issue-1185-4-wrapping-add.out new file mode 100644 index 000000000..69916f390 --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1185-4-wrapping-add.out @@ -0,0 +1,30 @@ +pub fn core::num::{u32}::wrapping_add(_1: u32, _2: u32) -> u32 += + +pub fn test_crate::mod_reduce(a_1: u32) -> u32 +{ + let _0: u32; // return + let a_1: u32; // arg #1 + let _2: bool; // anonymous local + let _3: u32; // anonymous local + let _4: u32; // anonymous local + + storage_live(_2) + storage_live(_3) + _3 = copy a_1 + _2 = move _3 < const 100 : u32 + if move _2 { + } else { + storage_dead(_3) + panic(core::panicking::panic) + } + storage_dead(_3) + storage_dead(_2) + storage_live(_4) + _4 = copy a_1 + _0 = core::num::{u32}::wrapping_add(move _4, const 1 : u32) + storage_dead(_4) + return +} + + diff --git a/charon/tests/ui/multi-target/issue-1185-4-wrapping-add.rs b/charon/tests/ui/multi-target/issue-1185-4-wrapping-add.rs new file mode 100644 index 000000000..5734be112 --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1185-4-wrapping-add.rs @@ -0,0 +1,5 @@ +//@ charon-args=--targets=x86_64-unknown-linux-gnu,i686-unknown-linux-gnu +pub fn mod_reduce(a: u32) -> u32 { + assert!(a < 100); + a.wrapping_add(1) +} diff --git a/charon/tests/ui/multi-target/issue-1186-conditional-repr.out b/charon/tests/ui/multi-target/issue-1186-conditional-repr.out new file mode 100644 index 000000000..998307cbf --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1186-conditional-repr.out @@ -0,0 +1,5 @@ +pub struct test_crate::Inner { + x: u32, +} + + diff --git a/charon/tests/ui/multi-target/issue-1186-conditional-repr.rs b/charon/tests/ui/multi-target/issue-1186-conditional-repr.rs new file mode 100644 index 000000000..2f9c733ae --- /dev/null +++ b/charon/tests/ui/multi-target/issue-1186-conditional-repr.rs @@ -0,0 +1,5 @@ +//@ charon-args=--targets=x86_64-unknown-linux-gnu,i686-unknown-linux-gnu +#[cfg_attr(target_arch = "x86_64", repr(align(16)))] +pub struct Inner { + pub x: u32, +} diff --git a/charon/tests/ui/simple/explicit_destruct_bound.out b/charon/tests/ui/simple/explicit_destruct_bound.out index 80db1cfab..cd0fad80d 100644 --- a/charon/tests/ui/simple/explicit_destruct_bound.out +++ b/charon/tests/ui/simple/explicit_destruct_bound.out @@ -1,7 +1,30 @@ -error: Error during trait resolution: Could not find a clause for `Binder { value: , bound_vars: [] }` in the item parameters - --> tests/ui/simple/explicit_destruct_bound.rs:6:29 - | -6 | fn drop(_: T) {} - | ^ +# Final LLBC before serialization: + +// Full name: core::marker::Destruct +#[lang_item("destruct")] +pub trait Destruct +{ + fn drop_in_place = drop_in_place + non-dyn-compatible +} + +// Full name: core::marker::Destruct::drop_in_place +unsafe fn drop_in_place(_1: *mut Self) += + +// Full name: test_crate::drop +fn drop(_1: T) +where + [@TraitClause0]: Destruct, +{ + let _0: (); // return + let _1: T; // arg #1 + + _0 = () + _0 = () + conditional_drop[@TraitClause0::drop_in_place] _1 + return +} + + -ERROR Charon failed to translate this code (1 errors) diff --git a/charon/tests/ui/simple/explicit_destruct_bound.rs b/charon/tests/ui/simple/explicit_destruct_bound.rs index 3f4101570..c815b926e 100644 --- a/charon/tests/ui/simple/explicit_destruct_bound.rs +++ b/charon/tests/ui/simple/explicit_destruct_bound.rs @@ -1,4 +1,3 @@ -//@ known-failure //@ charon-args=--hide-marker-traits #![feature(const_destruct)]