From 3e53003e441f545c43f3b04eb110ff0c0b7f0b74 Mon Sep 17 00:00:00 2001 From: Florian Sextl Date: Thu, 7 Aug 2025 20:16:02 +0200 Subject: [PATCH 1/7] compute layouts or hints on demand --- charon/Cargo.lock | 3 + charon/Cargo.toml | 2 +- charon/src/ast/layout_computer.rs | 436 ++++++++++++++ charon/src/ast/mod.rs | 1 + charon/src/ast/types_utils.rs | 160 +++++ charon/tests/layout.rs | 25 +- charon/tests/layouts_and_hints.json | 899 ++++++++++++++++++++++++++++ 7 files changed, 1524 insertions(+), 2 deletions(-) create mode 100644 charon/src/ast/layout_computer.rs create mode 100644 charon/tests/layouts_and_hints.json diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 31c46227b..df4f3686c 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -494,6 +494,9 @@ name = "either" version = "1.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "48c757948c5ede0e46177b7add2e67155f70e33c07fea8284df6576da70b3719" +dependencies = [ + "serde", +] [[package]] name = "encoding_rs" diff --git a/charon/Cargo.toml b/charon/Cargo.toml index cf48fc182..4372e2e10 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -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"] } diff --git a/charon/src/ast/layout_computer.rs b/charon/src/ast/layout_computer.rs new file mode 100644 index 000000000..fc9edf991 --- /dev/null +++ b/charon/src/ast/layout_computer.rs @@ -0,0 +1,436 @@ +use std::{cmp::max, collections::HashMap}; + +use either::Either; +use serde::Serialize; + +use crate::ast::{ + BuiltinTy, ByteCount, DeBruijnVar, Field, FieldId, Layout, TranslatedCrate, Ty, TyKind, + TypeDeclKind, TypeDeclRef, TypeId, TypeVarId, VariantLayout, Vector, +}; + +/// A utility to compute/lookup layouts of types from the crate's data. +/// Uses memoization to not re-compute already requested type layouts. +/// Should be constructed exactly once and kept around as long as the crate is used. +/// +/// WARNING: Using this will lead to leaked memory to guarantee that computed layouts stay available. +/// Since any crate should only have finitely many types, the memory usage is bounded. +pub struct LayoutComputer<'a> { + memoized_layouts: HashMap>, + krate: &'a TranslatedCrate, +} + +/// Minimal information about a type's layout that can be known without +/// querying the rustc type layout algorithm. +#[derive(Debug, Clone, Copy, Serialize)] +pub struct LayoutHint { + /// The minimal size of the type. + /// + /// Includes the minimal sizes of all its fields (if known), but doesn't take + /// alignment and possible padding, or wide pointers into consideration. + pub min_size: ByteCount, + /// The minimal alignment. + /// + /// Corresponds to the greatest known alignment of the types fields. + pub min_alignment: ByteCount, + /// Whether thy type might be uninhabited. + /// This can be the case if there are type variables as parameters that + /// have influence on the layout of the type. + /// + /// Will only be set to false, if its guaranteed that it is inhabited. + pub possibly_uninhabited: bool, +} + +impl<'a> LayoutComputer<'a> { + pub fn new<'b: 'a>(krate: &'b TranslatedCrate) -> Self { + Self { + memoized_layouts: HashMap::new(), + krate, + } + } + + /// Compute the layout of a tuple as precise as possible. + /// + /// If the elements have different sizes and thus might need padding, + /// it returns a hint, otherwise the precise layout. + fn get_layout_of_tuple<'c, 't>( + &'c mut self, + type_decl_ref: &'t TypeDeclRef, + ) -> Option> { + let mut total_min_size = 0; + let mut max_align = 1; + let mut uninhabited_part = false; + let mut possibly_same_size = None; + let mut must_have_same_size = true; + + for ty_arg in type_decl_ref.generics.types.iter() { + uninhabited_part |= ty_arg.is_possibly_uninhabited(); + match self.get_layout_of(ty_arg) { + Some(Either::Left(l)) => { + if let Some(size) = l.size { + total_min_size += size; + match possibly_same_size { + Some(other_size) => { + if size != other_size { + must_have_same_size = false; + } + } + None => possibly_same_size = Some(size), + } + } + if let Some(align) = l.align { + max_align = max(max_align, align); + } + } + Some(Either::Right(h)) => { + total_min_size += h.min_size; + max_align = max(max_align, h.min_alignment); + must_have_same_size = false; + } + None => (), + } + } + // If all elements have the same size, there is cannot be any padding between the elements + // and we are guaranteed to get a layout (we just don't know the order of elements). + Some( + if must_have_same_size && let Some(size) = possibly_same_size { + let new_layout = Layout::mk_uniform_tuple( + size, + type_decl_ref.generics.types.elem_count(), + max_align, + ); + let layout_ref = Box::leak(Box::new(new_layout)); + Either::Left(layout_ref) + } else { + Either::Right(LayoutHint { + min_size: total_min_size, + min_alignment: max_align, + possibly_uninhabited: uninhabited_part, + }) + }, + ) + } + + /// Approximate a layout for a struct (or enum variant) based on the fields. + fn compute_layout_from_fields( + &mut self, + fields: &Vector, + ty_var_map: &HashMap, + ) -> Option> { + let mut total_min_size = 0; + let mut max_align = 1; + let mut uninhabited_part = false; + + // If it is a new-type struct, we should be able to get a layout. + if fields.elem_count() == 1 { + let field = fields.get(FieldId::from_raw(0)).unwrap(); + let ty = if field.ty.is_type_var() { + let bound_ty_var = field.ty.as_type_var().unwrap(); + match bound_ty_var { + DeBruijnVar::Bound(_, id) | DeBruijnVar::Free(id) => ty_var_map.get(id)?, + } + } else { + &field.ty + }; + + match self.get_layout_of(ty) { + Some(Either::Left(l)) => { + // Simply exchange the field_offsets and variants. + let new_layout = Layout { + variant_layouts: [VariantLayout { + field_offsets: [0].into(), + uninhabited: false, + tag: None, + }] + .into(), + ..l.clone() + }; + let layout_ref = Box::leak(Box::new(new_layout)); + Some(Either::Left(layout_ref)) + } + r => r, + } + } else { + for field in fields { + let ty = if field.ty.is_type_var() { + let bound_ty_var = field.ty.as_type_var().unwrap(); + match bound_ty_var { + DeBruijnVar::Bound(_, id) => ty_var_map.get(id)?, + DeBruijnVar::Free(_) => unreachable!(), + } + } else { + &field.ty + }; + + uninhabited_part |= ty.is_possibly_uninhabited(); + match self.get_layout_of(ty) { + Some(Either::Left(l)) => { + if let Some(size) = l.size { + total_min_size += size; + } + if let Some(align) = l.align { + max_align = max(max_align, align); + } + } + Some(Either::Right(h)) => { + total_min_size += h.min_size; + max_align = max(max_align, h.min_alignment); + } + None => (), + } + } + Some(Either::Right(LayoutHint { + min_size: total_min_size, + min_alignment: max_align, + possibly_uninhabited: uninhabited_part, + })) + } + } + + /// Tries to compute a layout hint for otherwise generic ADTs with the given type arguments. + /// + /// Most of time, we can't compute a full layout due to potential reordering and padding bytes. + fn get_layout_hint_for_generic_adt( + &mut self, + type_decl_ref: &TypeDeclRef, + ) -> Option> { + let generics = &*type_decl_ref.generics; + let type_decl_id = type_decl_ref.id.as_adt()?; + let type_decl = self.krate.type_decls.get(*type_decl_id)?; + + // If we certainly can't instantiate all relevant type parameters, fail. + if generics.types.elem_count() != type_decl.generics.types.elem_count() + || generics.types.iter().find(|ty| ty.is_type_var()).is_some() + { + return None; + } + + // Map the generic type parameter variables to the given instantiations. + let ty_var_map: HashMap = type_decl + .generics + .types + .iter() + .map(|ty_var| ty_var.index) + .zip(generics.types.iter().cloned()) + .collect(); + + match &type_decl.kind { + TypeDeclKind::Struct(fields) => { + self.compute_layout_from_fields(fields, &ty_var_map) + } + TypeDeclKind::Enum(variants) => { + // Assume that there could be a niche and ignore the discriminant for the hint. + let variant_layouts: Vec>> = variants.iter().map(|variant| self.compute_layout_from_fields(&variant.fields, &ty_var_map)).collect(); + // If all variants have at least a layout hint, combine them. + if variant_layouts.iter().all(|l| l.is_some()) { + let mut max_variant_size = 0; + let mut max_variant_align = 1; + let mut all_variants_inhabited = variants.elem_count() == 0; + for variant_layout in variant_layouts { + match variant_layout { + Some(Either::Left(l)) => { + all_variants_inhabited &= !l.uninhabited; + if let Some(size) = l.size { + max_variant_size = max(max_variant_size,size); + } + if let Some(align) = l.align { + max_variant_align = max(max_variant_align, align); + } + } + Some(Either::Right(h)) => { + max_variant_size = max(max_variant_size,h.min_size); + max_variant_align = max(max_variant_align, h.min_alignment); + all_variants_inhabited &= !h.possibly_uninhabited; + } + None => (), + }; + } + Some(Either::Right(LayoutHint { + min_size: max_variant_size, + min_alignment: max_variant_align, + // Enums are only considered uninhabited if they have no variants or all are uninhabited. + possibly_uninhabited: all_variants_inhabited, + })) + } else { + None + } + }, + TypeDeclKind::Union(_) // No idea about unions + | TypeDeclKind::Opaque // TODO: maybe hardcode layouts for some opaque types from std? + | TypeDeclKind::Alias(_) + | TypeDeclKind::Error(_) => None, + } + } + + /// Computes or looks up layout of given type if possible or tries to produce a layout hint instead. + /// + /// If the layout was not already available, it will be computed and leaked to guarantee + /// that it stays available. + pub fn get_layout_of<'c, 't>( + &'c mut self, + ty: &'t Ty, + ) -> Option> { + // Check memoization. + if let Some(layout) = self.memoized_layouts.get(ty) { + return Some(*layout); + } + + let res: Option> = match ty { + TyKind::Adt(type_decl_ref) => { + match type_decl_ref.id { + TypeId::Adt(type_decl_id) => self + .krate + .type_decls + .get(type_decl_id) + .unwrap() + .layout + .as_ref() + .map(|l| Either::Left(l)) + .or_else(|| self.get_layout_hint_for_generic_adt(type_decl_ref)), + // Without recreating the layout computation mechanism from rustc, we cannot know the layout of a tuple, other than for the unit type. + TypeId::Tuple => { + if ty.is_unit() { + let new_layout = Layout::mk_1zst_layout(); + let layout_ref = Box::leak(Box::new(new_layout)); + Some(Either::Left(layout_ref)) + } else { + self.get_layout_of_tuple(type_decl_ref) + } + } + TypeId::Builtin(builtin_ty) => { + match builtin_ty { + BuiltinTy::Box => { + // Box has only two type parameters: the first is the boxed type, the second is the allocator. + let boxed_ty = type_decl_ref + .generics + .types + .get(TypeVarId::from_usize(0)) + .unwrap(); + Some(match boxed_ty.needs_metadata(&self.krate.type_decls) { + Some(true) => { + let new_layout = Layout::mk_ptr_layout_with_metadata( + self.krate.target_information.target_pointer_size, + ); + let layout_ref = Box::leak(Box::new(new_layout)); + Either::Left(layout_ref) + } + Some(false) => { + let new_layout = Layout::mk_ptr_layout_wo_metadata( + self.krate.target_information.target_pointer_size, + ); + let layout_ref = Box::leak(Box::new(new_layout)); + Either::Left(layout_ref) + } + None => Either::Right(LayoutHint { + min_size: self.krate.target_information.target_pointer_size, + min_alignment: self + .krate + .target_information + .target_pointer_size, + possibly_uninhabited: false, + }), + }) + } + // Slices are non-sized and can be handled as such. + BuiltinTy::Slice | BuiltinTy::Str => { + let new_layout = Layout::mk_unsized_layout(); + let layout_ref = Box::leak(Box::new(new_layout)); + Some(Either::Left(layout_ref)) + } + BuiltinTy::Array => None, + } + } + } + } + TyKind::Literal(literal_ty) => { + let size = + literal_ty.target_size(self.krate.target_information.target_pointer_size); + let new_layout = Layout::mk_simple_layout(size as u64); + let layout_ref = Box::leak(Box::new(new_layout)); + Some(Either::Left(layout_ref)) + } + TyKind::Ref(_, ty, _) | TyKind::RawPtr(ty, _) => { + Some(match ty.needs_metadata(&self.krate.type_decls) { + Some(true) => { + let new_layout = Layout::mk_ptr_layout_with_metadata( + self.krate.target_information.target_pointer_size, + ); + let layout_ref = Box::leak(Box::new(new_layout)); + Either::Left(layout_ref) + } + Some(false) => { + let new_layout = Layout::mk_ptr_layout_wo_metadata( + self.krate.target_information.target_pointer_size, + ); + let layout_ref = Box::leak(Box::new(new_layout)); + Either::Left(layout_ref) + } + None => Either::Right(LayoutHint { + min_size: self.krate.target_information.target_pointer_size, + min_alignment: self.krate.target_information.target_pointer_size, + possibly_uninhabited: false, + }), + }) + } + TyKind::DynTrait(_) => { + let new_layout = Layout::mk_unsized_layout(); + let layout_ref = Box::leak(Box::new(new_layout)); + Some(Either::Left(layout_ref)) + } + // We cannot get a layout for TypeVar, TraitType, Never, DynTrait, Error, FnPtr (probably?), and FnDef (probably?) + _ => None, + }; + + // Update memoization. + if let Some(layout) = res { + self.memoized_layouts.insert(ty.clone(), layout); + } + + res + } + + /// Checks whether the type is known to be a ZST. + /// Computes the layout first if necessary. + pub fn is_known_zst(&mut self, ty: &Ty) -> bool { + match self.get_layout_of(ty) { + Some(Either::Left(l)) => { + if let Some(size) = l.size { + size == 0 + } else { + false + } + } + // Since the hint could have min_size == 0 but not be a ZST, we also return false for it. + _ => false, + } + } + + /// Checks whether the type is known to be uninhabited. + /// Computes the layout first if necessary. + pub fn is_known_uninhabited(&mut self, ty: &Ty) -> bool { + if ty.is_never() { + true + } else { + match self.get_layout_of(ty) { + Some(Either::Left(l)) => l.uninhabited, + // Since the hint can only tell whether a type is guarantee to be inhabited, + // we can never be sure that it is uninhabited. + Some(Either::Right(_)) => false, + None => false, + } + } + } + + /// Checks whether the type is known to be inhabited. + /// Computes the layout first if necessary. + pub fn is_known_inhabited(&mut self, ty: &Ty) -> bool { + if ty.is_never() { + false + } else { + match self.get_layout_of(ty) { + Some(Either::Left(l)) => !l.uninhabited, + Some(Either::Right(h)) => !h.possibly_uninhabited, + None => false, + } + } + } +} diff --git a/charon/src/ast/mod.rs b/charon/src/ast/mod.rs index e0601aff3..a1a7f76ec 100644 --- a/charon/src/ast/mod.rs +++ b/charon/src/ast/mod.rs @@ -4,6 +4,7 @@ pub mod expressions_utils; pub mod gast; pub mod gast_utils; pub mod krate; +pub mod layout_computer; pub mod llbc_ast; pub mod llbc_ast_utils; pub mod meta; diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index d4470594a..875f7f1f4 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -717,6 +717,69 @@ impl Ty { pub fn as_adt(&self) -> Option<&TypeDeclRef> { self.kind().as_adt() } + + /// Whether the types is guaranteed to need pointers to it to be wide. + /// If the result is `None`, then it could not be determined. + pub fn needs_metadata(&self, ctx: &Vector) -> Option { + match self { + TyKind::Adt(type_decl_ref) => match type_decl_ref.id { + TypeId::Adt(type_decl_id) => match ctx.get(type_decl_id).unwrap().ptr_metadata { + Some(PtrMetadata::Length) | Some(PtrMetadata::VTable(_)) => Some(true), + _ => Some(false), + }, + TypeId::Tuple => Some(false), + TypeId::Builtin(builtin_ty) => Some(!matches!(builtin_ty, BuiltinTy::Box)), + }, + TyKind::DynTrait(_) => Some(true), + TyKind::Literal(_) + | TyKind::Never + | TyKind::Ref(_, _, _) + | TyKind::RawPtr(_, _) + | TyKind::FnPtr(_) => Some(false), + TyKind::TraitType(_, _) | TyKind::TypeVar(_) | TyKind::FnDef(_) | TyKind::Error(_) => { + None + } + } + } + + /// Whether the type is not guaranteed to be inhabited. + /// + /// This is the case if the type is [`!`], contains [`!`], or could + /// either of these (but is not known to, e.g. because it is an uninstantiated type variable). + pub fn is_possibly_uninhabited(&self) -> bool { + match self { + /* Adts of any kind can only be uninhabited if they would store + anything of an uninhabited type. In many cases, this can only + happen if any type argument could be uninhabited. + We don't traverse all the fields in the Adt since having an uninhabited field + that doesn't relate to a type parameter seems very uncommon. + + Important to note: pointers such as Box are always inhabited! + */ + TyKind::Adt(type_decl_ref) => { + if let TypeId::Builtin(b) = type_decl_ref.id + && b.is_box() + { + false + } else { + type_decl_ref + .generics + .types + .iter() + .find(|arg0: &&Self| Self::is_possibly_uninhabited(*arg0)) + .is_some() + } + } + TyKind::TypeVar(_) | TyKind::Never | TyKind::TraitType(_, _) => true, + TyKind::Literal(_) + | TyKind::Ref(_, _, _) + | TyKind::RawPtr(_, _) + | TyKind::DynTrait(_) + | TyKind::FnPtr(_) + | TyKind::FnDef(_) + | TyKind::Error(_) => false, + } + } } impl TyKind { @@ -1114,6 +1177,103 @@ impl Layout { false } } + + /// Construct a simple layout with a single variant and a single field of `size`. + /// + /// Assumes that the alignment is the same as the size. + pub fn mk_simple_layout(size: ByteCount) -> Self { + Self { + size: Some(size), + align: Some(size), + discriminant_layout: None, + uninhabited: false, + variant_layouts: [VariantLayout { + field_offsets: [0].into(), + uninhabited: false, + tag: None, + }] + .into(), + } + } + + /// Constructs the layout of a thin pointer. + pub fn mk_ptr_layout_wo_metadata(ptr_size: ByteCount) -> Self { + Self::mk_simple_layout(ptr_size) + } + + /// Constructs the layout of a wide pointer. + /// + /// Assumes that the metadata is pointer-sized. + pub fn mk_ptr_layout_with_metadata(ptr_size: ByteCount) -> Self { + Self { + // I just hope that all kinds of meta data is ptr sized? + size: Some(2 * ptr_size), + align: Some(ptr_size), + discriminant_layout: None, + uninhabited: false, + variant_layouts: [VariantLayout { + field_offsets: [0, ptr_size].into(), + uninhabited: false, + tag: None, + }] + .into(), + } + } + + /// Constructs the layout of a 1ZST, i.e. a zero-sized type with alignment 1. + pub fn mk_1zst_layout() -> Self { + Self { + size: Some(0), + align: Some(1), + discriminant_layout: None, + uninhabited: false, + variant_layouts: [VariantLayout { + field_offsets: [0].into(), + uninhabited: false, + tag: None, + }] + .into(), + } + } + + /// Creates the layout of a tuple where all fields are of the same size. + /// + /// Assumes that they are ordered linearly. + pub fn mk_uniform_tuple(elem_size: ByteCount, elem_count: usize, align: ByteCount) -> Self { + let mut field_offsets = Vector::with_capacity(elem_count); + for elem in 0..elem_count { + field_offsets.push(elem_size * elem as u64); + } + Self { + size: Some(elem_size * elem_count as u64), + align: Some(align), + discriminant_layout: None, + uninhabited: false, + variant_layouts: [VariantLayout { + field_offsets, + uninhabited: false, + tag: None, + }] + .into(), + } + } + + /// Constructs the layout of an unsized type with a single variant, + /// e.g. [`BuiltinTy::Slice`] or [`TyKind::DynTrait`]. + pub fn mk_unsized_layout() -> Self { + Self { + size: None, + align: None, + discriminant_layout: None, + uninhabited: false, + variant_layouts: [VariantLayout { + field_offsets: [0].into(), + uninhabited: false, + tag: None, + }] + .into(), + } + } } impl TyVisitable for T {} diff --git a/charon/tests/layout.rs b/charon/tests/layout.rs index 6f283b955..4baec29c2 100644 --- a/charon/tests/layout.rs +++ b/charon/tests/layout.rs @@ -3,7 +3,10 @@ use std::path::PathBuf; use indexmap::IndexMap; -use charon_lib::ast::*; +use charon_lib::{ + ast::{layout_computer::LayoutComputer, *}, + pretty::{self, FmtWithCtx}, +}; mod util; use util::*; @@ -130,6 +133,7 @@ fn type_layout() -> anyhow::Result<()> { Second(&'a T), } + #[derive(Debug)] enum GenericButFixedSize<'a, T: Sized> { First, Second(&'a T), @@ -177,6 +181,20 @@ fn type_layout() -> anyhow::Result<()> { } } + let mut layout_computer = LayoutComputer::new(&crate_data); + let mut layouts_hints = IndexMap::new(); + let mut ctx = pretty::formatter::FmtCtx::new(); + ctx.translated = Some(&crate_data); + { + let mut visitor = DynVisitor::new_shared(|ty: &Ty| { + let layout = layout_computer.get_layout_of(ty); + let id = ty.to_string_with_ctx(&ctx); + layouts_hints.insert(id, layout); + }); + let _ = crate_data.drive(&mut visitor); + } + let layouts_hints_str = serde_json::to_string_pretty(&layouts_hints)?; + let layouts: IndexMap> = crate_data .type_decls .iter() @@ -196,5 +214,10 @@ fn type_layout() -> anyhow::Result<()> { Action::Overwrite }; compare_or_overwrite(action, layouts_str, &PathBuf::from("./tests/layout.json"))?; + compare_or_overwrite( + action, + layouts_hints_str, + &PathBuf::from("./tests/layouts_and_hints.json"), + )?; Ok(()) } diff --git a/charon/tests/layouts_and_hints.json b/charon/tests/layouts_and_hints.json new file mode 100644 index 000000000..c640e140c --- /dev/null +++ b/charon/tests/layouts_and_hints.json @@ -0,0 +1,899 @@ +{ + "Formatter<'_0_0>": { + "Left": { + "size": 24, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 16, + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "u32": { + "Left": { + "size": 4, + "align": 4, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "@Type0": null, + "usize": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "Slice": { + "Left": { + "size": null, + "align": null, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "NonZero[Sized, {impl ZeroablePrimitive for u32}]": null, + "(dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : 'static)": { + "Left": { + "size": null, + "align": null, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "@Type1_0": null, + "@Type0_0": null, + "alloc::boxed::Box<@Type0, Global>[@TraitClause0::parent_clause0, Sized, {impl Allocator for Global}]": { + "Right": { + "min_size": 8, + "min_alignment": 8, + "possibly_uninhabited": false + } + }, + "Global": { + "Left": { + "size": 0, + "align": 1, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [], + "uninhabited": false, + "tag": null + } + ] + } + }, + "u8": { + "Left": { + "size": 1, + "align": 1, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "!": null, + "(usize, &'_0 (@Type0))": { + "Right": { + "min_size": 16, + "min_alignment": 8, + "possibly_uninhabited": false + } + }, + "&'_0 (@Type0)": { + "Right": { + "min_size": 8, + "min_alignment": 8, + "possibly_uninhabited": false + } + }, + "(u32, u32)": { + "Left": { + "size": 8, + "align": 4, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 4 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "u64": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "char": { + "Left": { + "size": 4, + "align": 4, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "String": { + "Left": { + "size": 24, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "fn(*mut (dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_))": null, + "*mut (dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)": { + "Left": { + "size": 16, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 8 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "(dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)": { + "Left": { + "size": null, + "align": null, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "()": { + "Left": { + "size": 0, + "align": 1, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "fn<'_0, '_1, '_2>(&'_0 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)), &'_1 mut (Formatter<'_2>)) -> Result<(), Error>[Sized<()>, Sized]": null, + "&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_))": { + "Left": { + "size": 16, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 8 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_0_1 mut (Formatter<'_0_2>)": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "Formatter<'_0_2>": { + "Left": { + "size": 24, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 16, + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "Result<(), Error>[Sized<()>, Sized]": { + "Right": { + "min_size": 0, + "min_alignment": 1, + "possibly_uninhabited": false + } + }, + "Error": { + "Left": { + "size": 0, + "align": 1, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [], + "uninhabited": false, + "tag": null + } + ] + } + }, + "@Type1": null, + "&'_1 (GenericButFixedSize<'_0, @Type0>[@TraitClause0])": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "GenericButFixedSize<'_0, @Type0>[@TraitClause0]": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": { + "offset": 0, + "tag_ty": { + "Signed": "Isize" + }, + "encoding": { + "Niche": { + "untagged_variant": 1 + } + } + }, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [], + "uninhabited": false, + "tag": { + "Signed": [ + "Isize", + "0" + ] + } + }, + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_2 mut (Formatter<'_3>)": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "Formatter<'_3>": { + "Left": { + "size": 24, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 16, + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_ (GenericButFixedSize<'_, @Type0>[@TraitClause0])": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "GenericButFixedSize<'_, @Type0>[@TraitClause0]": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": { + "offset": 0, + "tag_ty": { + "Signed": "Isize" + }, + "encoding": { + "Niche": { + "untagged_variant": 1 + } + } + }, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [], + "uninhabited": false, + "tag": { + "Signed": [ + "Isize", + "0" + ] + } + }, + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_ mut (Formatter<'_>)": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "Formatter<'_>": { + "Left": { + "size": 24, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 16, + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_ (Str)": { + "Left": { + "size": 16, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 8 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "Str": { + "Left": { + "size": null, + "align": null, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_ (&'_ (@Type0))": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_ (@Type0)": { + "Right": { + "min_size": 8, + "min_alignment": 8, + "possibly_uninhabited": false + } + }, + "&'_ ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_))": { + "Left": { + "size": 16, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 8 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_ (&'_ (&'_ (@Type0)))": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_1 mut (Formatter<'_2>)": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "Formatter<'_2>": { + "Left": { + "size": 24, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 16, + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_1 mut (Formatter<'_0>)": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "Formatter<'_0>": { + "Left": { + "size": 24, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 16, + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_2 (Str)": { + "Left": { + "size": 16, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 8 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_3 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : missing('_3)))": { + "Left": { + "size": 16, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 8 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "(dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : missing('_3))": { + "Left": { + "size": null, + "align": null, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "Layout": { + "Left": { + "size": 16, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 8, + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "Result>, AllocError>[Sized>>, Sized]": null, + "NonNull>": null, + "Slice": { + "Left": { + "size": null, + "align": null, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "AllocError": { + "Left": { + "size": 0, + "align": 1, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [], + "uninhabited": false, + "tag": null + } + ] + } + }, + "NonNull": null, + "&'_0 (NonZeroU32Inner)": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "NonZeroU32Inner": { + "Left": { + "size": 4, + "align": 4, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_0 (u32)": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_1 (&'_0 (@Type0))": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "core::fmt::Debug::{vtable}": { + "Left": { + "size": 32, + "align": 32, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 8, + 16, + 24 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_0 (Global)": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "Self::NonZeroInner": null +} \ No newline at end of file From 5ace54dca0955c2a96e915ff205a9ab51ca40865 Mon Sep 17 00:00:00 2001 From: Florian Sextl Date: Tue, 19 Aug 2025 11:46:04 +0200 Subject: [PATCH 2/7] add heuristic to use trait clause for layout computation of pointers --- charon/src/ast/layout_computer.rs | 142 +++++++++++++--------------- charon/src/ast/types_utils.rs | 66 +++++++++++-- charon/tests/layout.json | 3 +- charon/tests/layout.rs | 119 ++++++++++++++++++++++- charon/tests/layouts_and_hints.json | 47 ++++++++- 5 files changed, 289 insertions(+), 88 deletions(-) diff --git a/charon/src/ast/layout_computer.rs b/charon/src/ast/layout_computer.rs index fc9edf991..c1da79b59 100644 --- a/charon/src/ast/layout_computer.rs +++ b/charon/src/ast/layout_computer.rs @@ -4,10 +4,12 @@ use either::Either; use serde::Serialize; use crate::ast::{ - BuiltinTy, ByteCount, DeBruijnVar, Field, FieldId, Layout, TranslatedCrate, Ty, TyKind, + BuiltinTy, ByteCount, Field, FieldId, GenericParams, Layout, TranslatedCrate, Ty, TyKind, TypeDeclKind, TypeDeclRef, TypeId, TypeVarId, VariantLayout, Vector, }; +type GenericCtx<'a> = Option<&'a GenericParams>; + /// A utility to compute/lookup layouts of types from the crate's data. /// Uses memoization to not re-compute already requested type layouts. /// Should be constructed exactly once and kept around as long as the crate is used. @@ -15,10 +17,12 @@ use crate::ast::{ /// WARNING: Using this will lead to leaked memory to guarantee that computed layouts stay available. /// Since any crate should only have finitely many types, the memory usage is bounded. pub struct LayoutComputer<'a> { - memoized_layouts: HashMap>, + memoized_layouts: HashMap<(Ty, Option), Either<&'a Layout, LayoutHint>>, krate: &'a TranslatedCrate, } +// TODO: use `repr` information + /// Minimal information about a type's layout that can be known without /// querying the rustc type layout algorithm. #[derive(Debug, Clone, Copy, Serialize)] @@ -55,6 +59,7 @@ impl<'a> LayoutComputer<'a> { fn get_layout_of_tuple<'c, 't>( &'c mut self, type_decl_ref: &'t TypeDeclRef, + generic_ctx: GenericCtx, ) -> Option> { let mut total_min_size = 0; let mut max_align = 1; @@ -64,7 +69,7 @@ impl<'a> LayoutComputer<'a> { for ty_arg in type_decl_ref.generics.types.iter() { uninhabited_part |= ty_arg.is_possibly_uninhabited(); - match self.get_layout_of(ty_arg) { + match self.get_layout_of(ty_arg, generic_ctx) { Some(Either::Left(l)) => { if let Some(size) = l.size { total_min_size += size; @@ -115,6 +120,7 @@ impl<'a> LayoutComputer<'a> { &mut self, fields: &Vector, ty_var_map: &HashMap, + generic_ctx: GenericCtx, ) -> Option> { let mut total_min_size = 0; let mut max_align = 1; @@ -124,15 +130,13 @@ impl<'a> LayoutComputer<'a> { if fields.elem_count() == 1 { let field = fields.get(FieldId::from_raw(0)).unwrap(); let ty = if field.ty.is_type_var() { - let bound_ty_var = field.ty.as_type_var().unwrap(); - match bound_ty_var { - DeBruijnVar::Bound(_, id) | DeBruijnVar::Free(id) => ty_var_map.get(id)?, - } + let id = field.ty.as_type_var().unwrap().get_raw(); + ty_var_map.get(id)? } else { &field.ty }; - match self.get_layout_of(ty) { + match self.get_layout_of(ty, generic_ctx) { Some(Either::Left(l)) => { // Simply exchange the field_offsets and variants. let new_layout = Layout { @@ -152,17 +156,14 @@ impl<'a> LayoutComputer<'a> { } else { for field in fields { let ty = if field.ty.is_type_var() { - let bound_ty_var = field.ty.as_type_var().unwrap(); - match bound_ty_var { - DeBruijnVar::Bound(_, id) => ty_var_map.get(id)?, - DeBruijnVar::Free(_) => unreachable!(), - } + let id = field.ty.as_type_var().unwrap().get_raw(); + ty_var_map.get(id)? } else { &field.ty }; uninhabited_part |= ty.is_possibly_uninhabited(); - match self.get_layout_of(ty) { + match self.get_layout_of(ty, generic_ctx) { Some(Either::Left(l)) => { if let Some(size) = l.size { total_min_size += size; @@ -215,11 +216,11 @@ impl<'a> LayoutComputer<'a> { match &type_decl.kind { TypeDeclKind::Struct(fields) => { - self.compute_layout_from_fields(fields, &ty_var_map) + self.compute_layout_from_fields(fields, &ty_var_map, None) } TypeDeclKind::Enum(variants) => { // Assume that there could be a niche and ignore the discriminant for the hint. - let variant_layouts: Vec>> = variants.iter().map(|variant| self.compute_layout_from_fields(&variant.fields, &ty_var_map)).collect(); + let variant_layouts: Vec>> = variants.iter().map(|variant| self.compute_layout_from_fields(&variant.fields, &ty_var_map,None)).collect(); // If all variants have at least a layout hint, combine them. if variant_layouts.iter().all(|l| l.is_some()) { let mut max_variant_size = 0; @@ -261,16 +262,53 @@ impl<'a> LayoutComputer<'a> { } } + /// Computes the layout of pointers. + /// + /// Tries to use information about whether the pointee is sized, + /// if it's a type variable. + fn get_layout_of_ptr_type<'c, 't>( + &'c mut self, + pointee: &'t Ty, + generic_ctx: GenericCtx, + ) -> Either<&'a Layout, LayoutHint> { + match pointee.needs_metadata(&self.krate, generic_ctx) { + Some(true) => { + let new_layout = Layout::mk_ptr_layout_with_metadata( + self.krate.target_information.target_pointer_size, + ); + let layout_ref = Box::leak(Box::new(new_layout)); + Either::Left(layout_ref) + } + Some(false) => { + let new_layout = Layout::mk_ptr_layout_wo_metadata( + self.krate.target_information.target_pointer_size, + ); + let layout_ref = Box::leak(Box::new(new_layout)); + Either::Left(layout_ref) + } + None => Either::Right(LayoutHint { + min_size: self.krate.target_information.target_pointer_size, + min_alignment: self.krate.target_information.target_pointer_size, + possibly_uninhabited: false, + }), + } + } + /// Computes or looks up layout of given type if possible or tries to produce a layout hint instead. /// /// If the layout was not already available, it will be computed and leaked to guarantee /// that it stays available. + /// + /// The generic context is used to obtain more information about the type and should correspond + /// to where the type occurs, e.g. the generic context of a function signature for one of its argument's types. pub fn get_layout_of<'c, 't>( &'c mut self, ty: &'t Ty, + generic_ctx: GenericCtx<'_>, ) -> Option> { // Check memoization. - if let Some(layout) = self.memoized_layouts.get(ty) { + let key = (ty.clone(), generic_ctx.cloned()); + if let Some(layout) = self.memoized_layouts.get(&key) { return Some(*layout); } @@ -286,49 +324,22 @@ impl<'a> LayoutComputer<'a> { .as_ref() .map(|l| Either::Left(l)) .or_else(|| self.get_layout_hint_for_generic_adt(type_decl_ref)), - // Without recreating the layout computation mechanism from rustc, we cannot know the layout of a tuple, other than for the unit type. TypeId::Tuple => { if ty.is_unit() { let new_layout = Layout::mk_1zst_layout(); let layout_ref = Box::leak(Box::new(new_layout)); Some(Either::Left(layout_ref)) } else { - self.get_layout_of_tuple(type_decl_ref) + self.get_layout_of_tuple(type_decl_ref, generic_ctx) } } TypeId::Builtin(builtin_ty) => { match builtin_ty { BuiltinTy::Box => { - // Box has only two type parameters: the first is the boxed type, the second is the allocator. - let boxed_ty = type_decl_ref - .generics - .types - .get(TypeVarId::from_usize(0)) - .unwrap(); - Some(match boxed_ty.needs_metadata(&self.krate.type_decls) { - Some(true) => { - let new_layout = Layout::mk_ptr_layout_with_metadata( - self.krate.target_information.target_pointer_size, - ); - let layout_ref = Box::leak(Box::new(new_layout)); - Either::Left(layout_ref) - } - Some(false) => { - let new_layout = Layout::mk_ptr_layout_wo_metadata( - self.krate.target_information.target_pointer_size, - ); - let layout_ref = Box::leak(Box::new(new_layout)); - Either::Left(layout_ref) - } - None => Either::Right(LayoutHint { - min_size: self.krate.target_information.target_pointer_size, - min_alignment: self - .krate - .target_information - .target_pointer_size, - possibly_uninhabited: false, - }), - }) + // Box has only one relevant type parameters: the boxed type. + let boxed_ty = + type_decl_ref.generics.types.get(TypeVarId::ZERO).unwrap(); + Some(self.get_layout_of_ptr_type(boxed_ty, generic_ctx)) } // Slices are non-sized and can be handled as such. BuiltinTy::Slice | BuiltinTy::Str => { @@ -349,27 +360,7 @@ impl<'a> LayoutComputer<'a> { Some(Either::Left(layout_ref)) } TyKind::Ref(_, ty, _) | TyKind::RawPtr(ty, _) => { - Some(match ty.needs_metadata(&self.krate.type_decls) { - Some(true) => { - let new_layout = Layout::mk_ptr_layout_with_metadata( - self.krate.target_information.target_pointer_size, - ); - let layout_ref = Box::leak(Box::new(new_layout)); - Either::Left(layout_ref) - } - Some(false) => { - let new_layout = Layout::mk_ptr_layout_wo_metadata( - self.krate.target_information.target_pointer_size, - ); - let layout_ref = Box::leak(Box::new(new_layout)); - Either::Left(layout_ref) - } - None => Either::Right(LayoutHint { - min_size: self.krate.target_information.target_pointer_size, - min_alignment: self.krate.target_information.target_pointer_size, - possibly_uninhabited: false, - }), - }) + Some(self.get_layout_of_ptr_type(ty, generic_ctx)) } TyKind::DynTrait(_) => { let new_layout = Layout::mk_unsized_layout(); @@ -382,7 +373,7 @@ impl<'a> LayoutComputer<'a> { // Update memoization. if let Some(layout) = res { - self.memoized_layouts.insert(ty.clone(), layout); + self.memoized_layouts.insert(key, layout); } res @@ -391,7 +382,8 @@ impl<'a> LayoutComputer<'a> { /// Checks whether the type is known to be a ZST. /// Computes the layout first if necessary. pub fn is_known_zst(&mut self, ty: &Ty) -> bool { - match self.get_layout_of(ty) { + // The generic context cannot change whether a type is a ZST. + match self.get_layout_of(ty, None) { Some(Either::Left(l)) => { if let Some(size) = l.size { size == 0 @@ -410,7 +402,8 @@ impl<'a> LayoutComputer<'a> { if ty.is_never() { true } else { - match self.get_layout_of(ty) { + // The generic context cannot change whether a type is uninhabited. + match self.get_layout_of(ty, None) { Some(Either::Left(l)) => l.uninhabited, // Since the hint can only tell whether a type is guarantee to be inhabited, // we can never be sure that it is uninhabited. @@ -426,7 +419,8 @@ impl<'a> LayoutComputer<'a> { if ty.is_never() { false } else { - match self.get_layout_of(ty) { + // The generic context cannot change whether a type is uninhabited. + match self.get_layout_of(ty, None) { Some(Either::Left(l)) => !l.uninhabited, Some(Either::Right(h)) => !h.possibly_uninhabited, None => false, diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 875f7f1f4..b67671034 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -720,13 +720,22 @@ impl Ty { /// Whether the types is guaranteed to need pointers to it to be wide. /// If the result is `None`, then it could not be determined. - pub fn needs_metadata(&self, ctx: &Vector) -> Option { + /// + /// The function needs additional context to approximate this information as + /// precisely as possible. + pub fn needs_metadata( + &self, + krate: &TranslatedCrate, + generic_ctx: Option<&GenericParams>, + ) -> Option { match self { TyKind::Adt(type_decl_ref) => match type_decl_ref.id { - TypeId::Adt(type_decl_id) => match ctx.get(type_decl_id).unwrap().ptr_metadata { - Some(PtrMetadata::Length) | Some(PtrMetadata::VTable(_)) => Some(true), - _ => Some(false), - }, + TypeId::Adt(type_decl_id) => { + match krate.type_decls.get(type_decl_id).unwrap().ptr_metadata { + Some(PtrMetadata::Length) | Some(PtrMetadata::VTable(_)) => Some(true), + _ => Some(false), + } + } TypeId::Tuple => Some(false), TypeId::Builtin(builtin_ty) => Some(!matches!(builtin_ty, BuiltinTy::Box)), }, @@ -736,8 +745,42 @@ impl Ty { | TyKind::Ref(_, _, _) | TyKind::RawPtr(_, _) | TyKind::FnPtr(_) => Some(false), - TyKind::TraitType(_, _) | TyKind::TypeVar(_) | TyKind::FnDef(_) | TyKind::Error(_) => { - None + TyKind::TraitType(_, _) | TyKind::FnDef(_) | TyKind::Error(_) => None, + TyKind::TypeVar(tvar) => { + // Try to figure out whether the type variable is bound to be `Sized` + let tvar = tvar.get_raw(); + if let Some(generic_params) = generic_ctx { + generic_params + .trait_clauses + .iter() + .find(|clause| { + // Check the first argument of the trait clause, i.e. + // the `T` in `T: Trait`. + if let Some(ty) = clause + .trait_ + .skip_binder + .generics + .types + .get(TypeVarId::ZERO) + { + ty.is_type_var() + && tvar == ty.as_type_var().unwrap().get_raw() + // Check whether the trait is indeed `Sized` + && krate + .trait_decls + .get(clause.trait_.skip_binder.id) + .unwrap() + .item_meta + .lang_item + == Some("sized".to_owned()) + } else { + false + } + }) + .map(|_| false) + } else { + None + } } } } @@ -1276,6 +1319,15 @@ impl Layout { } } +impl DeBruijnVar { + /// Get's the contained value and ignores binding information. + pub fn get_raw(&self) -> &T { + match self { + DeBruijnVar::Bound(_, var) | DeBruijnVar::Free(var) => var, + } + } +} + impl TyVisitable for T {} impl Eq for TraitClause {} diff --git a/charon/tests/layout.json b/charon/tests/layout.json index 9a4136129..01b448314 100644 --- a/charon/tests/layout.json +++ b/charon/tests/layout.json @@ -587,5 +587,6 @@ } } ] - } + }, + "test_crate::NestedPointers": null } \ No newline at end of file diff --git a/charon/tests/layout.rs b/charon/tests/layout.rs index 4baec29c2..5037d7354 100644 --- a/charon/tests/layout.rs +++ b/charon/tests/layout.rs @@ -1,10 +1,10 @@ -#![feature(box_patterns)] use std::path::PathBuf; use indexmap::IndexMap; use charon_lib::{ ast::{layout_computer::LayoutComputer, *}, + formatter::AstFormatter, pretty::{self, FmtWithCtx}, }; @@ -144,6 +144,11 @@ fn type_layout() -> anyhow::Result<()> { First = 42, Second = 18446744073709551615, } + + struct NestedPointers { + x: (Box, Box), + n: N + } "#, &[], )?; @@ -186,12 +191,28 @@ fn type_layout() -> anyhow::Result<()> { let mut ctx = pretty::formatter::FmtCtx::new(); ctx.translated = Some(&crate_data); { - let mut visitor = DynVisitor::new_shared(|ty: &Ty| { - let layout = layout_computer.get_layout_of(ty); + // Visit all types without context. + let mut ty_visitor = DynVisitor::new_shared(|ty: &Ty| { + let layout = layout_computer.get_layout_of(ty, None); let id = ty.to_string_with_ctx(&ctx); - layouts_hints.insert(id, layout); + let _ = layouts_hints.insert(id, layout); }); - let _ = crate_data.drive(&mut visitor); + let _ = crate_data.drive(&mut ty_visitor); + } + { + // Visit all type declarations with the corresponding context. + let mut tdecl_visitor = DynVisitor::new_shared(|tdecl: &TypeDecl| { + let generic_ctx = Some(&tdecl.generics); + let ctx = ctx.set_generics(&tdecl.generics); + if tdecl.kind.is_struct() { + for arg in tdecl.kind.as_struct().unwrap() { + let layout = layout_computer.get_layout_of(&arg.ty, generic_ctx); + let id = arg.ty.to_string_with_ctx(&ctx); + let _ = layouts_hints.insert(id, layout); + } + } + }); + let _ = crate_data.drive(&mut tdecl_visitor); } let layouts_hints_str = serde_json::to_string_pretty(&layouts_hints)?; @@ -221,3 +242,91 @@ fn type_layout() -> anyhow::Result<()> { )?; Ok(()) } + +#[test] +// Tests that the generic context of a declaration is correctly used to determine that pointers +// need no metadata for type variables that are (implicitly) `Sized`. +fn metadata() -> anyhow::Result<()> { + let crate_data = translate_rust_text( + r#" + struct HasSizedParams<'a, T,S> { + x: u32, + y: Box, + z: &'a S + } + + fn has_sized_params<'a,T: Sized,S>(_x: u32, y: Box, _z: &'a S) -> &T {&*Box::leak(y)} + "#, + &[], + )?; + + let mut layout_computer = LayoutComputer::new(&crate_data); + { + let mut tdecl_visitor = DynVisitor::new_shared(|tdecl: &TypeDecl| { + let generic_ctx = Some(&tdecl.generics); + if tdecl.kind.is_struct() { + for arg in tdecl.kind.as_struct().unwrap() { + if arg.ty.is_box() { + let tvar = arg + .ty + .as_adt() + .unwrap() + .generics + .types + .get(TypeVarId::ZERO) + .unwrap(); + assert!(tvar.is_type_var()); + assert_eq!(tvar.needs_metadata(&crate_data, generic_ctx), Some(false)); + let arg_layout = layout_computer.get_layout_of(&arg.ty, generic_ctx); + assert!(arg_layout.is_some_and(|e| e.is_left())); + } else if arg.ty.is_ref() { + let tvar = arg.ty.as_ref().unwrap().1; + assert!(tvar.is_type_var()); + assert_eq!(tvar.needs_metadata(&crate_data, generic_ctx), Some(false)); + let arg_layout = layout_computer.get_layout_of(&arg.ty, generic_ctx); + assert!(arg_layout.is_some_and(|e| e.is_left())); + } + assert_eq!(arg.ty.needs_metadata(&crate_data, generic_ctx), Some(false)); + } + } + }); + let _ = crate_data.drive(&mut tdecl_visitor); + } + + let mut fun_sig_visitor = DynVisitor::new_shared(|fun_decl: &FunDecl| { + if fun_decl.item_meta.name.name[0].as_ident().unwrap().0 == "test_crate" { + let fun_sig = &fun_decl.signature; + let generic_ctx = Some(&fun_sig.generics); + for arg in &fun_sig.inputs { + if arg.is_box() { + let tvar = arg + .as_adt() + .unwrap() + .generics + .types + .get(TypeVarId::ZERO) + .unwrap(); + assert!(tvar.is_type_var()); + assert_eq!(tvar.needs_metadata(&crate_data, generic_ctx), Some(false)); + let arg_layout = layout_computer.get_layout_of(arg, generic_ctx); + assert!(arg_layout.is_some_and(|e| e.is_left())); + } else if arg.is_ref() { + let tvar = arg.as_ref().unwrap().1; + assert!(tvar.is_type_var()); + assert_eq!(tvar.needs_metadata(&crate_data, generic_ctx), Some(false)); + let arg_layout = layout_computer.get_layout_of(arg, generic_ctx); + assert!(arg_layout.is_some_and(|e| e.is_left())); + } + assert_eq!(arg.needs_metadata(&crate_data, generic_ctx), Some(false)); + } + let tvar = fun_sig.output.as_ref().unwrap().1; + assert!(tvar.is_type_var()); + assert_eq!(tvar.needs_metadata(&crate_data, generic_ctx), Some(false)); + let ret_layout = layout_computer.get_layout_of(&fun_sig.output, generic_ctx); + assert!(ret_layout.is_some_and(|e| e.is_left())); + } + }); + let _ = crate_data.drive(&mut fun_sig_visitor); + + Ok(()) +} diff --git a/charon/tests/layouts_and_hints.json b/charon/tests/layouts_and_hints.json index c640e140c..21efcc897 100644 --- a/charon/tests/layouts_and_hints.json +++ b/charon/tests/layouts_and_hints.json @@ -212,6 +212,13 @@ ] } }, + "(alloc::boxed::Box<@Type0, Global>[@TraitClause0::parent_clause0, Sized, {impl Allocator for Global}], alloc::boxed::Box<@Type0, Global>[@TraitClause0::parent_clause0, Sized, {impl Allocator for Global}])": { + "Right": { + "min_size": 16, + "min_alignment": 8, + "possibly_uninhabited": false + } + }, "fn(*mut (dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_))": null, "*mut (dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)": { "Left": { @@ -895,5 +902,43 @@ ] } }, - "Self::NonZeroInner": null + "Self::NonZeroInner": null, + "T": null, + "alloc::boxed::Box[@TraitClause0::parent_clause0, Sized, {impl Allocator for Global}]": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "(alloc::boxed::Box[@TraitClause0::parent_clause0, Sized, {impl Allocator for Global}], alloc::boxed::Box[@TraitClause0::parent_clause0, Sized, {impl Allocator for Global}])": { + "Left": { + "size": 16, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 8 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "N": null, + "fn<'_0, '_1, '_2>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)), &'_0_1 mut (Formatter<'_0_2>)) -> Result<(), Error>[Sized<()>, Sized]": null } \ No newline at end of file From 2ea54549f21bcd0a8955088cc8cafaf02a03bf03 Mon Sep 17 00:00:00 2001 From: Florian Sextl Date: Wed, 20 Aug 2025 11:53:22 +0200 Subject: [PATCH 3/7] add representation options to typedecls --- .../src/generated/Generated_GAstOfJson.ml | 33 ++++++++++++++++++- charon-ml/src/generated/Generated_Types.ml | 27 +++++++++++++-- charon/src/ast/types.rs | 27 +++++++++++++-- charon/src/ast/types_utils.rs | 15 +++++++++ .../translate/translate_items.rs | 2 ++ .../translate/translate_trait_objects.rs | 1 + .../translate/translate_types.rs | 17 ++++++++++ 7 files changed, 115 insertions(+), 7 deletions(-) diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index 8d6e7cc6c..fb23140fd 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/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 "") diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index 214e348c3..5db259043 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/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]) diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 9e12bd827..8f494e4b3 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -368,7 +368,6 @@ pub struct Layout { #[drive(skip)] pub align: Option, /// The discriminant's layout, if any. Only relevant for types with multiple variants. - /// #[drive(skip)] pub discriminant_layout: Option, /// Whether the type is uninhabited, i.e. has any valid value at all. @@ -402,6 +401,24 @@ pub enum PtrMetadata { VTable(VTable), } +/// 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. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct ReprOptions { + pub align: Option, + pub pack: Option, + pub c: bool, + pub transparent: bool, + pub explicit_discr_type: bool, +} + /// A type declaration. /// /// Types can be opaque or transparent. @@ -436,6 +453,10 @@ pub struct TypeDecl { /// but due to some limitation to be fixed, we are unable to obtain the info. /// See `translate_types::{impl ItemTransCtx}::translate_ptr_metadata` for more details. pub ptr_metadata: Option, + /// The representation options of this type declaration as annotated by the user. + /// Is `None` for foreign type declarations. + #[drive(skip)] + pub repr: Option, } generate_index_type!(VariantId, "Variant"); @@ -469,8 +490,8 @@ pub struct Variant { #[drive(skip)] pub name: String, pub fields: Vector, - /// 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`). + /// The discriminant value outputted by `std::mem::discriminant` for this variant. + /// This can be different than the discriminant stored in memory (called `tag`). /// That one is described by [`DiscriminantLayout`] and [`TagEncoding`]. pub discriminant: ScalarValue, } diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index b67671034..def48c3df 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -737,6 +737,7 @@ impl Ty { } } TypeId::Tuple => Some(false), + // All builtins but box need metadata! TypeId::Builtin(builtin_ty) => Some(!matches!(builtin_ty, BuiltinTy::Box)), }, TyKind::DynTrait(_) => Some(true), @@ -1210,6 +1211,10 @@ impl TypeDecl { TagEncoding::Niche { untagged_variant } => variant_for_tag.or(Some(*untagged_variant)), } } + + pub fn is_c_repr(&self) -> bool { + self.repr.as_ref().is_some_and(|repr| repr.c) + } } impl Layout { @@ -1328,6 +1333,16 @@ impl DeBruijnVar { } } +impl ReprOptions { + /// Whether this representation options guarantee a fixed + /// field ordering for the type. + /// + /// Cf. `rustc_abi::ReprOptions::inhibit_struct_field_reordering`. + pub fn guarantees_fixed_field_order(&self) -> bool { + self.c || self.explicit_discr_type + } +} + impl TyVisitable for T {} impl Eq for TraitClause {} diff --git a/charon/src/bin/charon-driver/translate/translate_items.rs b/charon/src/bin/charon-driver/translate/translate_items.rs index ea72a69ea..2a3b3e990 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/charon/src/bin/charon-driver/translate/translate_items.rs @@ -345,6 +345,7 @@ impl ItemTransCtx<'_, '_> { }; let layout = self.translate_layout(def.this()); let ptr_metadata = self.translate_ptr_metadata(def.this()); + let repr = self.translate_repr_options(def.this()); let type_def = TypeDecl { def_id: trans_id, item_meta, @@ -353,6 +354,7 @@ impl ItemTransCtx<'_, '_> { 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 0214061ad..cdb887dc8 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -431,6 +431,7 @@ impl ItemTransCtx<'_, '_> { kind, layout: Some(layout), ptr_metadata: 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 65606e8c3..cafe60595 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -748,4 +748,21 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { let int_ty = ty.kind().as_literal().unwrap().to_integer_ty().unwrap(); Ok(ScalarValue::from_bits(int_ty, discr.val)) } + + pub fn translate_repr_options(&mut self, item: &hax::ItemRef) -> Option { + let rdefid = item.def_id.as_rust_def_id().unwrap(); + if let Some(local_rdefid) = rdefid.as_local() { + let tcx = self.t_ctx.tcx; + let r_repr = tcx.repr_options_of_def(local_rdefid); + Some(ReprOptions { + align: r_repr.align.map(|a| a.bytes()), + pack: r_repr.pack.map(|a| a.bytes()), + c: r_repr.c(), + transparent: r_repr.transparent(), + explicit_discr_type: r_repr.int.is_some(), + }) + } else { + None + } + } } From 35aed1f11e402f0f3f7bb76bb9f65573cf0a6c35 Mon Sep 17 00:00:00 2001 From: Florian Sextl Date: Wed, 20 Aug 2025 16:03:27 +0200 Subject: [PATCH 4/7] compute layouts for #[repr(C)] structs --- charon/src/ast/layout_computer.rs | 124 +++++++++++++++-- charon/tests/layout.json | 39 +++++- charon/tests/layout.rs | 21 +++ charon/tests/layouts_and_hints.json | 199 ++++++++++++++++++++++------ 4 files changed, 331 insertions(+), 52 deletions(-) diff --git a/charon/src/ast/layout_computer.rs b/charon/src/ast/layout_computer.rs index c1da79b59..c26e5ccb0 100644 --- a/charon/src/ast/layout_computer.rs +++ b/charon/src/ast/layout_computer.rs @@ -21,11 +21,11 @@ pub struct LayoutComputer<'a> { krate: &'a TranslatedCrate, } -// TODO: use `repr` information +// TODO: use `repr` information, add FFI-safety information where possible /// Minimal information about a type's layout that can be known without /// querying the rustc type layout algorithm. -#[derive(Debug, Clone, Copy, Serialize)] +#[derive(Debug, Clone, Copy, Serialize, PartialEq, Eq)] pub struct LayoutHint { /// The minimal size of the type. /// @@ -120,7 +120,7 @@ impl<'a> LayoutComputer<'a> { &mut self, fields: &Vector, ty_var_map: &HashMap, - generic_ctx: GenericCtx, + generic_ctx: GenericCtx<'_>, ) -> Option> { let mut total_min_size = 0; let mut max_align = 1; @@ -187,23 +187,125 @@ impl<'a> LayoutComputer<'a> { } } + /// Computes the layout based on the simple algorithm for C types. + fn compute_c_layout_from_fields( + &mut self, + fields: &Vector, + ty_var_map: &HashMap, + generic_ctx: GenericCtx<'_>, + ) -> Either<&'a Layout, LayoutHint> { + let mut total_min_size = 0; + let mut max_align = 1; + let mut uninhabited_part = false; + let mut only_hint = false; + + let field_infos: Vec<(Option, Option)> = fields + .iter() + .map(|field| { + let ty = if field.ty.is_type_var() { + let id = field.ty.as_type_var().unwrap().get_raw(); + ty_var_map.get(id).unwrap() + } else { + &field.ty + }; + uninhabited_part |= ty.is_possibly_uninhabited(); + let field_info = match self.get_layout_of(ty, generic_ctx) { + Some(Either::Left(l)) => { + if let Some(size) = l.size { + total_min_size += size; + } else { + only_hint = true; + } + if let Some(align) = l.align { + max_align = max(max_align, align); + } else { + only_hint = true; + } + (l.size, l.align) + } + Some(Either::Right(h)) => { + total_min_size += h.min_size; + max_align = max(max_align, h.min_alignment); + only_hint = true; + (None, None) + } + None => { + only_hint = true; + (None, None) + } + }; + field_info + }) + .collect(); + + if only_hint { + Either::Right(LayoutHint { + min_size: total_min_size, + min_alignment: max_align, + possibly_uninhabited: uninhabited_part, + }) + } else { + let mut size_sum = 0; + let mut field_offsets: Vector = + Vector::with_capacity(fields.elem_count()); + + for field_info in field_infos { + let field_size = field_info.0.unwrap(); + let field_align = field_info.1.unwrap(); + + if size_sum % field_align == 0 { + field_offsets.push(size_sum); + size_sum += field_size; + } else { + // floor(size_sum / field_align) is n, s.t. n*field_align < size_sum < (n+1)*field_align + let last_aligned = (size_sum / field_align) * field_align; + let next_align = last_aligned + field_align; + size_sum = next_align; + field_offsets.push(size_sum); + size_sum += field_size; + } + } + if size_sum % max_align != 0 { + let last_aligned = (size_sum / max_align) * max_align; + let next_align = last_aligned + max_align; + size_sum = next_align + } + + let new_layout = Layout { + size: Some(size_sum), + align: Some(max_align), + discriminant_layout: None, + uninhabited: uninhabited_part, + variant_layouts: vec![VariantLayout { + field_offsets, + uninhabited: uninhabited_part, + tag: None, + }] + .into(), + }; + let layout_ref = Box::leak(Box::new(new_layout)); + Either::Left(layout_ref) + } + } + /// Tries to compute a layout hint for otherwise generic ADTs with the given type arguments. /// /// Most of time, we can't compute a full layout due to potential reordering and padding bytes. fn get_layout_hint_for_generic_adt( &mut self, type_decl_ref: &TypeDeclRef, + generic_ctx: GenericCtx<'_>, ) -> Option> { let generics = &*type_decl_ref.generics; let type_decl_id = type_decl_ref.id.as_adt()?; let type_decl = self.krate.type_decls.get(*type_decl_id)?; // If we certainly can't instantiate all relevant type parameters, fail. - if generics.types.elem_count() != type_decl.generics.types.elem_count() + /* if generics.types.elem_count() != type_decl.generics.types.elem_count() || generics.types.iter().find(|ty| ty.is_type_var()).is_some() { return None; - } + } */ // Map the generic type parameter variables to the given instantiations. let ty_var_map: HashMap = type_decl @@ -216,11 +318,15 @@ impl<'a> LayoutComputer<'a> { match &type_decl.kind { TypeDeclKind::Struct(fields) => { - self.compute_layout_from_fields(fields, &ty_var_map, None) + if type_decl.is_c_repr() { + Some(self.compute_c_layout_from_fields(fields, &ty_var_map, generic_ctx)) + } else { + self.compute_layout_from_fields(fields, &ty_var_map, generic_ctx) + } } TypeDeclKind::Enum(variants) => { // Assume that there could be a niche and ignore the discriminant for the hint. - let variant_layouts: Vec>> = variants.iter().map(|variant| self.compute_layout_from_fields(&variant.fields, &ty_var_map,None)).collect(); + let variant_layouts: Vec>> = variants.iter().map(|variant| self.compute_layout_from_fields(&variant.fields, &ty_var_map, generic_ctx)).collect(); // If all variants have at least a layout hint, combine them. if variant_layouts.iter().all(|l| l.is_some()) { let mut max_variant_size = 0; @@ -323,7 +429,9 @@ impl<'a> LayoutComputer<'a> { .layout .as_ref() .map(|l| Either::Left(l)) - .or_else(|| self.get_layout_hint_for_generic_adt(type_decl_ref)), + .or_else(|| { + self.get_layout_hint_for_generic_adt(type_decl_ref, generic_ctx) + }), TypeId::Tuple => { if ty.is_unit() { let new_layout = Layout::mk_1zst_layout(); diff --git a/charon/tests/layout.json b/charon/tests/layout.json index 01b448314..8f67f72f7 100644 --- a/charon/tests/layout.json +++ b/charon/tests/layout.json @@ -588,5 +588,42 @@ } ] }, - "test_crate::NestedPointers": null + "test_crate::NestedPointers": null, + "test_crate::GenericC": null, + "test_crate::Instance": { + "size": 8, + "align": 4, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 1, + 4 + ], + "uninhabited": false, + "tag": null + } + ] + }, + "test_crate::InstanceGen": { + "size": 32, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 8, + 16 + ], + "uninhabited": false, + "tag": null + } + ] + }, + "test_crate::InstanceGen2": null, + "test_crate::InstanceGen3": null } \ No newline at end of file diff --git a/charon/tests/layout.rs b/charon/tests/layout.rs index 5037d7354..b20b862e7 100644 --- a/charon/tests/layout.rs +++ b/charon/tests/layout.rs @@ -1,5 +1,6 @@ use std::path::PathBuf; +use either::Either; use indexmap::IndexMap; use charon_lib::{ @@ -149,6 +150,18 @@ fn type_layout() -> anyhow::Result<()> { x: (Box, Box), n: N } + + #[repr(C)] + struct GenericC { + a: A, + c: u8, + b: B + } + + type Instance = GenericC; + type InstanceGen<'a,T> = GenericC<&'a T,&'static str>; + type InstanceGen2<'a,T: Sized> = GenericC<&'a T,T>; + type InstanceGen3<'a,T: ?Sized> = GenericC<&'a T,i32>; "#, &[], )?; @@ -210,6 +223,14 @@ fn type_layout() -> anyhow::Result<()> { let id = arg.ty.to_string_with_ctx(&ctx); let _ = layouts_hints.insert(id, layout); } + } else if tdecl.kind.is_alias() + && let Some(ref layout) = tdecl.layout + { + let aliased_ty = tdecl.kind.as_alias().unwrap(); + let aliased_layout = layout_computer.get_layout_of(aliased_ty, generic_ctx); + assert_eq!(Some(Either::Left(layout)), aliased_layout); + let id = aliased_ty.to_string_with_ctx(&ctx); + let _ = layouts_hints.insert(id, aliased_layout); } }); let _ = crate_data.drive(&mut tdecl_visitor); diff --git a/charon/tests/layouts_and_hints.json b/charon/tests/layouts_and_hints.json index 21efcc897..f72fcdcfb 100644 --- a/charon/tests/layouts_and_hints.json +++ b/charon/tests/layouts_and_hints.json @@ -219,6 +219,141 @@ "possibly_uninhabited": false } }, + "@Type1": null, + "GenericC[Sized, Sized]": { + "Left": { + "size": 8, + "align": 4, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 1, + 4 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "bool": { + "Left": { + "size": 1, + "align": 1, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "GenericC<&'_0 (@Type0), &'static (Str)>[Sized<&'_ (missing(@Type0))>, Sized<&'_ (Str)>]": { + "Right": { + "min_size": 25, + "min_alignment": 8, + "possibly_uninhabited": false + } + }, + "&'static (Str)": { + "Left": { + "size": 16, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 8 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "Str": { + "Left": { + "size": null, + "align": null, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "&'_ (@Type0)": { + "Right": { + "min_size": 8, + "min_alignment": 8, + "possibly_uninhabited": false + } + }, + "&'_ (Str)": { + "Left": { + "size": 16, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 8 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "GenericC<&'_0 (@Type0), @Type0>[Sized<&'_ (missing(@Type0))>, @TraitClause0]": { + "Right": { + "min_size": 9, + "min_alignment": 8, + "possibly_uninhabited": true + } + }, + "GenericC<&'_0 (@Type0), i32>[Sized<&'_ (missing(@Type0))>, Sized]": { + "Right": { + "min_size": 13, + "min_alignment": 8, + "possibly_uninhabited": false + } + }, + "i32": { + "Left": { + "size": 4, + "align": 4, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, "fn(*mut (dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_))": null, "*mut (dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)": { "Left": { @@ -348,7 +483,6 @@ ] } }, - "@Type1": null, "&'_1 (GenericButFixedSize<'_0, @Type0>[@TraitClause0])": { "Left": { "size": 8, @@ -527,41 +661,6 @@ ] } }, - "&'_ (Str)": { - "Left": { - "size": 16, - "align": 8, - "discriminant_layout": null, - "uninhabited": false, - "variant_layouts": [ - { - "field_offsets": [ - 0, - 8 - ], - "uninhabited": false, - "tag": null - } - ] - } - }, - "Str": { - "Left": { - "size": null, - "align": null, - "discriminant_layout": null, - "uninhabited": false, - "variant_layouts": [ - { - "field_offsets": [ - 0 - ], - "uninhabited": false, - "tag": null - } - ] - } - }, "&'_ (&'_ (@Type0))": { "Left": { "size": 8, @@ -579,13 +678,6 @@ ] } }, - "&'_ (@Type0)": { - "Right": { - "min_size": 8, - "min_alignment": 8, - "possibly_uninhabited": false - } - }, "&'_ ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_))": { "Left": { "size": 16, @@ -940,5 +1032,26 @@ } }, "N": null, + "A": null, + "B": null, + "GenericC<&'a (T), &'static (Str)>[Sized<&'_ (T)>, Sized<&'_ (Str)>]": { + "Left": { + "size": 32, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0, + 8, + 16 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, "fn<'_0, '_1, '_2>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)), &'_0_1 mut (Formatter<'_0_2>)) -> Result<(), Error>[Sized<()>, Sized]": null } \ No newline at end of file From 41ef21e9a1aaaf8059267dfe92b63a6b15c76314 Mon Sep 17 00:00:00 2001 From: Florian Sextl Date: Tue, 16 Sep 2025 09:54:49 +0200 Subject: [PATCH 5/7] improve layout computation --- charon/src/ast/layout_computer.rs | 302 +++++++++--------- charon/src/ast/types_utils.rs | 67 ++-- .../translate/translate_items.rs | 20 +- .../translate/translate_types.rs | 35 +- charon/tests/layout.json | 15 + charon/tests/layout.rs | 10 +- charon/tests/layouts_and_hints.json | 254 +++++---------- 7 files changed, 301 insertions(+), 402 deletions(-) diff --git a/charon/src/ast/layout_computer.rs b/charon/src/ast/layout_computer.rs index c26e5ccb0..e2caf988d 100644 --- a/charon/src/ast/layout_computer.rs +++ b/charon/src/ast/layout_computer.rs @@ -1,11 +1,15 @@ -use std::{cmp::max, collections::HashMap}; +use std::{ + cmp::{max, min}, + collections::HashMap, +}; use either::Either; use serde::Serialize; use crate::ast::{ - BuiltinTy, ByteCount, Field, FieldId, GenericParams, Layout, TranslatedCrate, Ty, TyKind, - TypeDeclKind, TypeDeclRef, TypeId, TypeVarId, VariantLayout, Vector, + AlignRepr, BuiltinTy, ByteCount, ConstGeneric, ConstGenericVarId, Field, FieldId, + GenericParams, Layout, TranslatedCrate, Ty, TyKind, TypeDeclKind, TypeDeclRef, TypeId, + TypeVarId, VariantLayout, Vector, }; type GenericCtx<'a> = Option<&'a GenericParams>; @@ -21,8 +25,6 @@ pub struct LayoutComputer<'a> { krate: &'a TranslatedCrate, } -// TODO: use `repr` information, add FFI-safety information where possible - /// Minimal information about a type's layout that can be known without /// querying the rustc type layout algorithm. #[derive(Debug, Clone, Copy, Serialize, PartialEq, Eq)] @@ -52,67 +54,44 @@ impl<'a> LayoutComputer<'a> { } } - /// Compute the layout of a tuple as precise as possible. - /// - /// If the elements have different sizes and thus might need padding, - /// it returns a hint, otherwise the precise layout. + /// Compute a layout hint for a tuple. fn get_layout_of_tuple<'c, 't>( &'c mut self, type_decl_ref: &'t TypeDeclRef, generic_ctx: GenericCtx, - ) -> Option> { + ) -> LayoutHint { let mut total_min_size = 0; let mut max_align = 1; let mut uninhabited_part = false; let mut possibly_same_size = None; - let mut must_have_same_size = true; for ty_arg in type_decl_ref.generics.types.iter() { - uninhabited_part |= ty_arg.is_possibly_uninhabited(); match self.get_layout_of(ty_arg, generic_ctx) { Some(Either::Left(l)) => { if let Some(size) = l.size { total_min_size += size; - match possibly_same_size { - Some(other_size) => { - if size != other_size { - must_have_same_size = false; - } - } - None => possibly_same_size = Some(size), - } + if let None = possibly_same_size { + possibly_same_size = Some(size) + }; } if let Some(align) = l.align { max_align = max(max_align, align); } + uninhabited_part |= l.uninhabited; } Some(Either::Right(h)) => { total_min_size += h.min_size; max_align = max(max_align, h.min_alignment); - must_have_same_size = false; + uninhabited_part |= h.possibly_uninhabited; } - None => (), + None => uninhabited_part |= ty_arg.is_possibly_uninhabited(), } } - // If all elements have the same size, there is cannot be any padding between the elements - // and we are guaranteed to get a layout (we just don't know the order of elements). - Some( - if must_have_same_size && let Some(size) = possibly_same_size { - let new_layout = Layout::mk_uniform_tuple( - size, - type_decl_ref.generics.types.elem_count(), - max_align, - ); - let layout_ref = Box::leak(Box::new(new_layout)); - Either::Left(layout_ref) - } else { - Either::Right(LayoutHint { - min_size: total_min_size, - min_alignment: max_align, - possibly_uninhabited: uninhabited_part, - }) - }, - ) + LayoutHint { + min_size: total_min_size, + min_alignment: max_align, + possibly_uninhabited: uninhabited_part, + } } /// Approximate a layout for a struct (or enum variant) based on the fields. @@ -121,13 +100,16 @@ impl<'a> LayoutComputer<'a> { fields: &Vector, ty_var_map: &HashMap, generic_ctx: GenericCtx<'_>, + is_transparent: bool, + align_repr: Option, + is_variant: bool, ) -> Option> { let mut total_min_size = 0; let mut max_align = 1; let mut uninhabited_part = false; - // If it is a new-type struct, we should be able to get a layout. - if fields.elem_count() == 1 { + // If it is a transparent new-type struct, we should be able to get a layout. + if fields.elem_count() == 1 && is_transparent { let field = fields.get(FieldId::from_raw(0)).unwrap(); let ty = if field.ty.is_type_var() { let id = field.ty.as_type_var().unwrap().get_raw(); @@ -157,12 +139,17 @@ impl<'a> LayoutComputer<'a> { for field in fields { let ty = if field.ty.is_type_var() { let id = field.ty.as_type_var().unwrap().get_raw(); - ty_var_map.get(id)? + if let Some(ty) = ty_var_map.get(id) { + ty + } else { + // Don't know about tape variables. + uninhabited_part = true; + continue; + } } else { &field.ty }; - uninhabited_part |= ty.is_possibly_uninhabited(); match self.get_layout_of(ty, generic_ctx) { Some(Either::Left(l)) => { if let Some(size) = l.size { @@ -171,17 +158,36 @@ impl<'a> LayoutComputer<'a> { if let Some(align) = l.align { max_align = max(max_align, align); } + uninhabited_part |= l.uninhabited; } Some(Either::Right(h)) => { total_min_size += h.min_size; max_align = max(max_align, h.min_alignment); + uninhabited_part |= h.possibly_uninhabited; } - None => (), + None => uninhabited_part |= ty.is_possibly_uninhabited(), } } + + let min_alignment = match align_repr { + None => max_align, + // For `repr(align(n))`, the alignment is at least n. + Some(AlignRepr::Align(n)) => n, + // For `repr(packed(n))`, the alignment is at most n. + Some(AlignRepr::Packed(n)) => min(max_align, n), + }; + + // For uninhabited variants, the size can be 0 (seemingly only for variants with a single uninhabited field). + // As far as I can tell, the alignment stays the same as computed above. + let min_size = if is_variant && uninhabited_part { + 0 + } else { + total_min_size + }; + Some(Either::Right(LayoutHint { - min_size: total_min_size, - min_alignment: max_align, + min_size: min_size, + min_alignment, possibly_uninhabited: uninhabited_part, })) } @@ -193,98 +199,42 @@ impl<'a> LayoutComputer<'a> { fields: &Vector, ty_var_map: &HashMap, generic_ctx: GenericCtx<'_>, - ) -> Either<&'a Layout, LayoutHint> { + ) -> LayoutHint { let mut total_min_size = 0; let mut max_align = 1; let mut uninhabited_part = false; - let mut only_hint = false; - let field_infos: Vec<(Option, Option)> = fields - .iter() - .map(|field| { - let ty = if field.ty.is_type_var() { - let id = field.ty.as_type_var().unwrap().get_raw(); - ty_var_map.get(id).unwrap() - } else { - &field.ty - }; - uninhabited_part |= ty.is_possibly_uninhabited(); - let field_info = match self.get_layout_of(ty, generic_ctx) { - Some(Either::Left(l)) => { - if let Some(size) = l.size { - total_min_size += size; - } else { - only_hint = true; - } - if let Some(align) = l.align { - max_align = max(max_align, align); - } else { - only_hint = true; - } - (l.size, l.align) - } - Some(Either::Right(h)) => { - total_min_size += h.min_size; - max_align = max(max_align, h.min_alignment); - only_hint = true; - (None, None) + for field in fields { + let ty = if field.ty.is_type_var() { + let id = field.ty.as_type_var().unwrap().get_raw(); + ty_var_map.get(id).unwrap() + } else { + &field.ty + }; + + match self.get_layout_of(ty, generic_ctx) { + Some(Either::Left(l)) => { + if let Some(size) = l.size { + total_min_size += size; } - None => { - only_hint = true; - (None, None) + if let Some(align) = l.align { + max_align = max(max_align, align); } - }; - field_info - }) - .collect(); - - if only_hint { - Either::Right(LayoutHint { - min_size: total_min_size, - min_alignment: max_align, - possibly_uninhabited: uninhabited_part, - }) - } else { - let mut size_sum = 0; - let mut field_offsets: Vector = - Vector::with_capacity(fields.elem_count()); - - for field_info in field_infos { - let field_size = field_info.0.unwrap(); - let field_align = field_info.1.unwrap(); - - if size_sum % field_align == 0 { - field_offsets.push(size_sum); - size_sum += field_size; - } else { - // floor(size_sum / field_align) is n, s.t. n*field_align < size_sum < (n+1)*field_align - let last_aligned = (size_sum / field_align) * field_align; - let next_align = last_aligned + field_align; - size_sum = next_align; - field_offsets.push(size_sum); - size_sum += field_size; + uninhabited_part |= l.uninhabited; } - } - if size_sum % max_align != 0 { - let last_aligned = (size_sum / max_align) * max_align; - let next_align = last_aligned + max_align; - size_sum = next_align - } - - let new_layout = Layout { - size: Some(size_sum), - align: Some(max_align), - discriminant_layout: None, - uninhabited: uninhabited_part, - variant_layouts: vec![VariantLayout { - field_offsets, - uninhabited: uninhabited_part, - tag: None, - }] - .into(), + Some(Either::Right(h)) => { + total_min_size += h.min_size; + max_align = max(max_align, h.min_alignment); + uninhabited_part |= h.possibly_uninhabited; + } + None => uninhabited_part |= ty.is_possibly_uninhabited(), }; - let layout_ref = Box::leak(Box::new(new_layout)); - Either::Left(layout_ref) + } + + LayoutHint { + min_size: total_min_size, + min_alignment: max_align, + possibly_uninhabited: uninhabited_part, } } @@ -319,23 +269,25 @@ impl<'a> LayoutComputer<'a> { match &type_decl.kind { TypeDeclKind::Struct(fields) => { if type_decl.is_c_repr() { - Some(self.compute_c_layout_from_fields(fields, &ty_var_map, generic_ctx)) + Some(Either::Right(self.compute_c_layout_from_fields(fields, &ty_var_map, generic_ctx))) } else { - self.compute_layout_from_fields(fields, &ty_var_map, generic_ctx) + self.compute_layout_from_fields(fields, &ty_var_map, generic_ctx, type_decl.is_transparent(), type_decl.forced_alignment(), false) } } TypeDeclKind::Enum(variants) => { // Assume that there could be a niche and ignore the discriminant for the hint. - let variant_layouts: Vec>> = variants.iter().map(|variant| self.compute_layout_from_fields(&variant.fields, &ty_var_map, generic_ctx)).collect(); + let variant_layouts: Vec>> = variants.iter().map(|variant| + self.compute_layout_from_fields(&variant.fields, &ty_var_map, generic_ctx, false,type_decl.forced_alignment(), true) + ).collect(); // If all variants have at least a layout hint, combine them. if variant_layouts.iter().all(|l| l.is_some()) { let mut max_variant_size = 0; let mut max_variant_align = 1; - let mut all_variants_inhabited = variants.elem_count() == 0; + let mut all_variants_uninhabited = variants.elem_count() == 0; for variant_layout in variant_layouts { match variant_layout { Some(Either::Left(l)) => { - all_variants_inhabited &= !l.uninhabited; + all_variants_uninhabited &= !l.uninhabited; if let Some(size) = l.size { max_variant_size = max(max_variant_size,size); } @@ -346,7 +298,7 @@ impl<'a> LayoutComputer<'a> { Some(Either::Right(h)) => { max_variant_size = max(max_variant_size,h.min_size); max_variant_align = max(max_variant_align, h.min_alignment); - all_variants_inhabited &= !h.possibly_uninhabited; + all_variants_uninhabited &= !h.possibly_uninhabited; } None => (), }; @@ -355,15 +307,15 @@ impl<'a> LayoutComputer<'a> { min_size: max_variant_size, min_alignment: max_variant_align, // Enums are only considered uninhabited if they have no variants or all are uninhabited. - possibly_uninhabited: all_variants_inhabited, + possibly_uninhabited: all_variants_uninhabited, })) } else { None } }, + TypeDeclKind::Alias(aliased_ty) => self.get_layout_of(aliased_ty, generic_ctx), TypeDeclKind::Union(_) // No idea about unions | TypeDeclKind::Opaque // TODO: maybe hardcode layouts for some opaque types from std? - | TypeDeclKind::Alias(_) | TypeDeclKind::Error(_) => None, } } @@ -378,13 +330,6 @@ impl<'a> LayoutComputer<'a> { generic_ctx: GenericCtx, ) -> Either<&'a Layout, LayoutHint> { match pointee.needs_metadata(&self.krate, generic_ctx) { - Some(true) => { - let new_layout = Layout::mk_ptr_layout_with_metadata( - self.krate.target_information.target_pointer_size, - ); - let layout_ref = Box::leak(Box::new(new_layout)); - Either::Left(layout_ref) - } Some(false) => { let new_layout = Layout::mk_ptr_layout_wo_metadata( self.krate.target_information.target_pointer_size, @@ -392,6 +337,12 @@ impl<'a> LayoutComputer<'a> { let layout_ref = Box::leak(Box::new(new_layout)); Either::Left(layout_ref) } + Some(true) => Either::Right(LayoutHint { + // All metadata is pointer sized + min_size: self.krate.target_information.target_pointer_size * 2, + min_alignment: self.krate.target_information.target_pointer_size, + possibly_uninhabited: false, + }), None => Either::Right(LayoutHint { min_size: self.krate.target_information.target_pointer_size, min_alignment: self.krate.target_information.target_pointer_size, @@ -400,6 +351,47 @@ impl<'a> LayoutComputer<'a> { } } + /// Computes the trivial layout of an array, unless it's zero-sized (cf. https://github.com/rust-lang/rust/issues/81996). + fn get_layout_of_array( + &mut self, + elem_ty: &Ty, + elem_num: &ConstGeneric, + generic_ctx: GenericCtx, + ) -> Option> { + let elem_num = elem_num.as_value()?.as_scalar()?.as_uint().ok()? as u64; + match self.get_layout_of(elem_ty, generic_ctx) { + Some(Either::Left(l)) => { + // If the array is zero-sized, only give a hint. + if l.size == Some(0) || elem_num == 0 { + Some(Either::Right(LayoutHint { + min_size: 0, + min_alignment: l.align?, + possibly_uninhabited: l.uninhabited, + })) + } else { + let array_layout = Layout { + size: l.size.map(|s| s * elem_num), + discriminant_layout: None, + variant_layouts: [VariantLayout { + field_offsets: [].into(), + uninhabited: false, + tag: None, + }] + .into(), + ..l.clone() + }; + let layout_ref = Box::leak(Box::new(array_layout)); + Some(Either::Left(layout_ref)) + } + } + Some(Either::Right(h)) => Some(Either::Right(LayoutHint { + min_size: h.min_size * elem_num, + ..h + })), + None => None, + } + } + /// Computes or looks up layout of given type if possible or tries to produce a layout hint instead. /// /// If the layout was not already available, it will be computed and leaked to guarantee @@ -438,7 +430,9 @@ impl<'a> LayoutComputer<'a> { let layout_ref = Box::leak(Box::new(new_layout)); Some(Either::Left(layout_ref)) } else { - self.get_layout_of_tuple(type_decl_ref, generic_ctx) + Some(Either::Right( + self.get_layout_of_tuple(type_decl_ref, generic_ctx), + )) } } TypeId::Builtin(builtin_ty) => { @@ -455,7 +449,17 @@ impl<'a> LayoutComputer<'a> { let layout_ref = Box::leak(Box::new(new_layout)); Some(Either::Left(layout_ref)) } - BuiltinTy::Array => None, + BuiltinTy::Array => { + // Arrays have one type parameter and one const parameter. + let elem_ty = + type_decl_ref.generics.types.get(TypeVarId::ZERO).unwrap(); + let elem_num = type_decl_ref + .generics + .const_generics + .get(ConstGenericVarId::ZERO) + .unwrap(); + self.get_layout_of_array(elem_ty, elem_num, generic_ctx) + } } } } diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index def48c3df..12d8f2d4b 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -790,7 +790,10 @@ impl Ty { /// /// This is the case if the type is [`!`], contains [`!`], or could /// either of these (but is not known to, e.g. because it is an uninstantiated type variable). - pub fn is_possibly_uninhabited(&self) -> bool { + /// + /// This should mostly only be called for non-Adts, otherwise checking the layout should be the + /// better way to check for inhabitedness. + pub(crate) fn is_possibly_uninhabited(&self) -> bool { match self { /* Adts of any kind can only be uninhabited if they would store anything of an uninhabited type. In many cases, this can only @@ -1178,6 +1181,11 @@ pub trait TyVisitable: Sized + AstVisitable { } } +pub enum AlignRepr { + Packed(u64), + Align(u64), +} + impl TypeDecl { /// Looks up the variant corresponding to the tag (i.e. the in-memory bytes that represent the discriminant). /// Returns `None` for types that don't have a relevant discriminant (e.g. uninhabited types). @@ -1215,6 +1223,20 @@ impl TypeDecl { pub fn is_c_repr(&self) -> bool { self.repr.as_ref().is_some_and(|repr| repr.c) } + + pub fn is_transparent(&self) -> bool { + self.repr.as_ref().is_some_and(|repr| repr.transparent) + } + + /// Looks up whether the representation annotations of the type + /// decl force the type's alignment to be related to a specified number. + pub fn forced_alignment(&self) -> Option { + self.repr.as_ref().and_then(|repr| { + repr.pack + .map(AlignRepr::Packed) + .or(repr.align.map(AlignRepr::Align)) + }) + } } impl Layout { @@ -1249,25 +1271,6 @@ impl Layout { Self::mk_simple_layout(ptr_size) } - /// Constructs the layout of a wide pointer. - /// - /// Assumes that the metadata is pointer-sized. - pub fn mk_ptr_layout_with_metadata(ptr_size: ByteCount) -> Self { - Self { - // I just hope that all kinds of meta data is ptr sized? - size: Some(2 * ptr_size), - align: Some(ptr_size), - discriminant_layout: None, - uninhabited: false, - variant_layouts: [VariantLayout { - field_offsets: [0, ptr_size].into(), - uninhabited: false, - tag: None, - }] - .into(), - } - } - /// Constructs the layout of a 1ZST, i.e. a zero-sized type with alignment 1. pub fn mk_1zst_layout() -> Self { Self { @@ -1284,28 +1287,6 @@ impl Layout { } } - /// Creates the layout of a tuple where all fields are of the same size. - /// - /// Assumes that they are ordered linearly. - pub fn mk_uniform_tuple(elem_size: ByteCount, elem_count: usize, align: ByteCount) -> Self { - let mut field_offsets = Vector::with_capacity(elem_count); - for elem in 0..elem_count { - field_offsets.push(elem_size * elem as u64); - } - Self { - size: Some(elem_size * elem_count as u64), - align: Some(align), - discriminant_layout: None, - uninhabited: false, - variant_layouts: [VariantLayout { - field_offsets, - uninhabited: false, - tag: None, - }] - .into(), - } - } - /// Constructs the layout of an unsized type with a single variant, /// e.g. [`BuiltinTy::Slice`] or [`TyKind::DynTrait`]. pub fn mk_unsized_layout() -> Self { @@ -1315,7 +1296,7 @@ impl Layout { discriminant_layout: None, uninhabited: false, variant_layouts: [VariantLayout { - field_offsets: [0].into(), + field_offsets: [].into(), uninhabited: false, tag: None, }] diff --git a/charon/src/bin/charon-driver/translate/translate_items.rs b/charon/src/bin/charon-driver/translate/translate_items.rs index 2a3b3e990..f40baa996 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/charon/src/bin/charon-driver/translate/translate_items.rs @@ -325,27 +325,29 @@ impl ItemTransCtx<'_, '_> { // Translate type body let kind = match &def.kind { - _ if item_meta.opacity.is_opaque() => Ok(TypeDeclKind::Opaque), - hax::FullDefKind::OpaqueTy | hax::FullDefKind::ForeignTy => Ok(TypeDeclKind::Opaque), + _ if item_meta.opacity.is_opaque() => Ok((TypeDeclKind::Opaque, None)), + hax::FullDefKind::OpaqueTy | hax::FullDefKind::ForeignTy => { + Ok((TypeDeclKind::Opaque, None)) + } hax::FullDefKind::TyAlias { ty, .. } => { // Don't error on missing trait refs. self.error_on_impl_expr_error = false; - self.translate_ty(span, ty).map(TypeDeclKind::Alias) + self.translate_ty(span, ty) + .map(|x| (TypeDeclKind::Alias(x), None)) } hax::FullDefKind::Adt { .. } => self.translate_adt_def(trans_id, span, &item_meta, def), - hax::FullDefKind::Closure { args, .. } => { - self.translate_closure_adt(trans_id, span, &args) - } + hax::FullDefKind::Closure { args, .. } => self + .translate_closure_adt(trans_id, span, &args) + .map(|k| (k, None)), _ => panic!("Unexpected item when translating types: {def:?}"), }; - let kind = match kind { + let (kind, repr) = match kind { Ok(kind) => kind, - Err(err) => TypeDeclKind::Error(err.msg), + Err(err) => (TypeDeclKind::Error(err.msg), None), }; let layout = self.translate_layout(def.this()); let ptr_metadata = self.translate_ptr_metadata(def.this()); - let repr = self.translate_repr_options(def.this()); let type_def = TypeDecl { def_id: trans_id, item_meta, diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index cafe60595..1304a13dc 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -607,17 +607,20 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { def_span: Span, item_meta: &ItemMeta, def: &hax::FullDef, - ) -> Result { + ) -> Result<(TypeDeclKind, Option), Error> { use hax::AdtKind; let hax::FullDefKind::Adt { - adt_kind, variants, .. + adt_kind, + variants, + repr, + .. } = def.kind() else { unreachable!() }; if item_meta.opacity.is_opaque() { - return Ok(TypeDeclKind::Opaque); + return Ok((TypeDeclKind::Opaque, None)); } trace!("{}", trans_id); @@ -643,7 +646,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { .with_content_visibility(contents_are_public) .is_opaque() { - return Ok(TypeDeclKind::Opaque); + return Ok((TypeDeclKind::Opaque, None)); } // The type is transparent: explore the variants @@ -735,8 +738,9 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { AdtKind::Enum => TypeDeclKind::Enum(translated_variants), AdtKind::Union => TypeDeclKind::Union(translated_variants[0].fields.clone()), }; + let repr = Self::translate_repr_options(repr); - Ok(type_def_kind) + Ok((type_def_kind, Some(repr))) } fn translate_discriminant( @@ -749,20 +753,13 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { Ok(ScalarValue::from_bits(int_ty, discr.val)) } - pub fn translate_repr_options(&mut self, item: &hax::ItemRef) -> Option { - let rdefid = item.def_id.as_rust_def_id().unwrap(); - if let Some(local_rdefid) = rdefid.as_local() { - let tcx = self.t_ctx.tcx; - let r_repr = tcx.repr_options_of_def(local_rdefid); - Some(ReprOptions { - align: r_repr.align.map(|a| a.bytes()), - pack: r_repr.pack.map(|a| a.bytes()), - c: r_repr.c(), - transparent: r_repr.transparent(), - explicit_discr_type: r_repr.int.is_some(), - }) - } else { - None + pub fn translate_repr_options(hax_repr: &hax::ReprOptions) -> ReprOptions { + ReprOptions { + align: hax_repr.align.clone().map(|a| a.bytes), + pack: hax_repr.pack.clone().map(|a| a.bytes), + c: hax_repr.flags.is_c, + transparent: hax_repr.flags.is_transparent, + explicit_discr_type: hax_repr.int_specified, } } } diff --git a/charon/tests/layout.json b/charon/tests/layout.json index 8f67f72f7..6b454b8a7 100644 --- a/charon/tests/layout.json +++ b/charon/tests/layout.json @@ -590,6 +590,21 @@ }, "test_crate::NestedPointers": null, "test_crate::GenericC": null, + "test_crate::HasArray": { + "size": 32, + "align": 4, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + }, "test_crate::Instance": { "size": 8, "align": 4, diff --git a/charon/tests/layout.rs b/charon/tests/layout.rs index b20b862e7..cbe40ff62 100644 --- a/charon/tests/layout.rs +++ b/charon/tests/layout.rs @@ -1,6 +1,5 @@ use std::path::PathBuf; -use either::Either; use indexmap::IndexMap; use charon_lib::{ @@ -158,6 +157,10 @@ fn type_layout() -> anyhow::Result<()> { b: B } + struct HasArray { + a: [u32; 8] + } + type Instance = GenericC; type InstanceGen<'a,T> = GenericC<&'a T,&'static str>; type InstanceGen2<'a,T: Sized> = GenericC<&'a T,T>; @@ -223,12 +226,9 @@ fn type_layout() -> anyhow::Result<()> { let id = arg.ty.to_string_with_ctx(&ctx); let _ = layouts_hints.insert(id, layout); } - } else if tdecl.kind.is_alias() - && let Some(ref layout) = tdecl.layout - { + } else if tdecl.kind.is_alias() { let aliased_ty = tdecl.kind.as_alias().unwrap(); let aliased_layout = layout_computer.get_layout_of(aliased_ty, generic_ctx); - assert_eq!(Some(Either::Left(layout)), aliased_layout); let id = aliased_ty.to_string_with_ctx(&ctx); let _ = layouts_hints.insert(id, aliased_layout); } diff --git a/charon/tests/layouts_and_hints.json b/charon/tests/layouts_and_hints.json index f72fcdcfb..c4cf1700e 100644 --- a/charon/tests/layouts_and_hints.json +++ b/charon/tests/layouts_and_hints.json @@ -60,9 +60,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -78,9 +76,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -144,21 +140,10 @@ } }, "(u32, u32)": { - "Left": { - "size": 8, - "align": 4, - "discriminant_layout": null, - "uninhabited": false, - "variant_layouts": [ - { - "field_offsets": [ - 0, - 4 - ], - "uninhabited": false, - "tag": null - } - ] + "Right": { + "min_size": 8, + "min_alignment": 4, + "possibly_uninhabited": false } }, "u64": { @@ -220,25 +205,28 @@ } }, "@Type1": null, - "GenericC[Sized, Sized]": { + "Array": { "Left": { - "size": 8, + "size": 32, "align": 4, "discriminant_layout": null, "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0, - 1, - 4 - ], + "field_offsets": [], "uninhabited": false, "tag": null } ] } }, + "GenericC[Sized, Sized]": { + "Right": { + "min_size": 6, + "min_alignment": 4, + "possibly_uninhabited": false + } + }, "bool": { "Left": { "size": 1, @@ -264,21 +252,10 @@ } }, "&'static (Str)": { - "Left": { - "size": 16, - "align": 8, - "discriminant_layout": null, - "uninhabited": false, - "variant_layouts": [ - { - "field_offsets": [ - 0, - 8 - ], - "uninhabited": false, - "tag": null - } - ] + "Right": { + "min_size": 16, + "min_alignment": 8, + "possibly_uninhabited": false } }, "Str": { @@ -289,9 +266,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -306,21 +281,10 @@ } }, "&'_ (Str)": { - "Left": { - "size": 16, - "align": 8, - "discriminant_layout": null, - "uninhabited": false, - "variant_layouts": [ - { - "field_offsets": [ - 0, - 8 - ], - "uninhabited": false, - "tag": null - } - ] + "Right": { + "min_size": 16, + "min_alignment": 8, + "possibly_uninhabited": false } }, "GenericC<&'_0 (@Type0), @Type0>[Sized<&'_ (missing(@Type0))>, @TraitClause0]": { @@ -356,21 +320,10 @@ }, "fn(*mut (dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_))": null, "*mut (dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)": { - "Left": { - "size": 16, - "align": 8, - "discriminant_layout": null, - "uninhabited": false, - "variant_layouts": [ - { - "field_offsets": [ - 0, - 8 - ], - "uninhabited": false, - "tag": null - } - ] + "Right": { + "min_size": 16, + "min_alignment": 8, + "possibly_uninhabited": false } }, "(dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)": { @@ -381,9 +334,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -409,21 +360,10 @@ }, "fn<'_0, '_1, '_2>(&'_0 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)), &'_1 mut (Formatter<'_2>)) -> Result<(), Error>[Sized<()>, Sized]": null, "&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_))": { - "Left": { - "size": 16, - "align": 8, - "discriminant_layout": null, - "uninhabited": false, - "variant_layouts": [ - { - "field_offsets": [ - 0, - 8 - ], - "uninhabited": false, - "tag": null - } - ] + "Right": { + "min_size": 16, + "min_alignment": 8, + "possibly_uninhabited": false } }, "&'_0_1 mut (Formatter<'_0_2>)": { @@ -679,21 +619,10 @@ } }, "&'_ ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_))": { - "Left": { - "size": 16, - "align": 8, - "discriminant_layout": null, - "uninhabited": false, - "variant_layouts": [ - { - "field_offsets": [ - 0, - 8 - ], - "uninhabited": false, - "tag": null - } - ] + "Right": { + "min_size": 16, + "min_alignment": 8, + "possibly_uninhabited": false } }, "&'_ (&'_ (&'_ (@Type0)))": { @@ -784,39 +713,17 @@ } }, "&'_2 (Str)": { - "Left": { - "size": 16, - "align": 8, - "discriminant_layout": null, - "uninhabited": false, - "variant_layouts": [ - { - "field_offsets": [ - 0, - 8 - ], - "uninhabited": false, - "tag": null - } - ] + "Right": { + "min_size": 16, + "min_alignment": 8, + "possibly_uninhabited": false } }, "&'_3 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : missing('_3)))": { - "Left": { - "size": 16, - "align": 8, - "discriminant_layout": null, - "uninhabited": false, - "variant_layouts": [ - { - "field_offsets": [ - 0, - 8 - ], - "uninhabited": false, - "tag": null - } - ] + "Right": { + "min_size": 16, + "min_alignment": 8, + "possibly_uninhabited": false } }, "(dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : missing('_3))": { @@ -827,9 +734,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -854,7 +759,13 @@ ] } }, - "Result>, AllocError>[Sized>>, Sized]": null, + "Result>, AllocError>[Sized>>, Sized]": { + "Right": { + "min_size": 0, + "min_alignment": 1, + "possibly_uninhabited": false + } + }, "NonNull>": null, "Slice": { "Left": { @@ -864,9 +775,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -1014,43 +923,34 @@ } }, "(alloc::boxed::Box[@TraitClause0::parent_clause0, Sized, {impl Allocator for Global}], alloc::boxed::Box[@TraitClause0::parent_clause0, Sized, {impl Allocator for Global}])": { - "Left": { - "size": 16, - "align": 8, - "discriminant_layout": null, - "uninhabited": false, - "variant_layouts": [ - { - "field_offsets": [ - 0, - 8 - ], - "uninhabited": false, - "tag": null - } - ] + "Right": { + "min_size": 16, + "min_alignment": 8, + "possibly_uninhabited": false } }, "N": null, "A": null, "B": null, "GenericC<&'a (T), &'static (Str)>[Sized<&'_ (T)>, Sized<&'_ (Str)>]": { - "Left": { - "size": 32, - "align": 8, - "discriminant_layout": null, - "uninhabited": false, - "variant_layouts": [ - { - "field_offsets": [ - 0, - 8, - 16 - ], - "uninhabited": false, - "tag": null - } - ] + "Right": { + "min_size": 25, + "min_alignment": 8, + "possibly_uninhabited": false + } + }, + "GenericC<&'a (T), T>[Sized<&'_ (T)>, @TraitClause0]": { + "Right": { + "min_size": 9, + "min_alignment": 8, + "possibly_uninhabited": true + } + }, + "GenericC<&'a (T), i32>[Sized<&'_ (T)>, Sized]": { + "Right": { + "min_size": 13, + "min_alignment": 8, + "possibly_uninhabited": false } }, "fn<'_0, '_1, '_2>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)), &'_0_1 mut (Formatter<'_0_2>)) -> Result<(), Error>[Sized<()>, Sized]": null From 63405a84e8d2eda18e36b76e250f56520c4f61d8 Mon Sep 17 00:00:00 2001 From: Florian Sextl Date: Wed, 17 Sep 2025 15:01:00 +0200 Subject: [PATCH 6/7] add Box handling and other fixes --- charon/src/ast/layout_computer.rs | 117 ++++++++++---------- charon/src/ast/types_utils.rs | 46 ++++++-- charon/tests/layout.json | 6 +- charon/tests/layout.rs | 12 +- charon/tests/layouts_and_hints.json | 166 ++++++++++++++++------------ 5 files changed, 202 insertions(+), 145 deletions(-) diff --git a/charon/src/ast/layout_computer.rs b/charon/src/ast/layout_computer.rs index e2caf988d..b1d1b9129 100644 --- a/charon/src/ast/layout_computer.rs +++ b/charon/src/ast/layout_computer.rs @@ -7,9 +7,9 @@ use either::Either; use serde::Serialize; use crate::ast::{ - AlignRepr, BuiltinTy, ByteCount, ConstGeneric, ConstGenericVarId, Field, FieldId, - GenericParams, Layout, TranslatedCrate, Ty, TyKind, TypeDeclKind, TypeDeclRef, TypeId, - TypeVarId, VariantLayout, Vector, + AlignRepr, AttrInfo, BuiltinTy, ByteCount, ConstGeneric, ConstGenericVarId, Field, FieldId, + GenericParams, Layout, Span, TranslatedCrate, Ty, TyKind, TyVisitable, TypeDeclKind, + TypeDeclRef, TypeId, TypeVarId, VariantLayout, Vector, }; type GenericCtx<'a> = Option<&'a GenericParams>; @@ -98,7 +98,6 @@ impl<'a> LayoutComputer<'a> { fn compute_layout_from_fields( &mut self, fields: &Vector, - ty_var_map: &HashMap, generic_ctx: GenericCtx<'_>, is_transparent: bool, align_repr: Option, @@ -110,15 +109,9 @@ impl<'a> LayoutComputer<'a> { // If it is a transparent new-type struct, we should be able to get a layout. if fields.elem_count() == 1 && is_transparent { - let field = fields.get(FieldId::from_raw(0)).unwrap(); - let ty = if field.ty.is_type_var() { - let id = field.ty.as_type_var().unwrap().get_raw(); - ty_var_map.get(id)? - } else { - &field.ty - }; + let field = fields.get(FieldId::ZERO).unwrap(); - match self.get_layout_of(ty, generic_ctx) { + match self.get_layout_of(&field.ty, generic_ctx) { Some(Either::Left(l)) => { // Simply exchange the field_offsets and variants. let new_layout = Layout { @@ -137,20 +130,7 @@ impl<'a> LayoutComputer<'a> { } } else { for field in fields { - let ty = if field.ty.is_type_var() { - let id = field.ty.as_type_var().unwrap().get_raw(); - if let Some(ty) = ty_var_map.get(id) { - ty - } else { - // Don't know about tape variables. - uninhabited_part = true; - continue; - } - } else { - &field.ty - }; - - match self.get_layout_of(ty, generic_ctx) { + match self.get_layout_of(&field.ty, generic_ctx) { Some(Either::Left(l)) => { if let Some(size) = l.size { total_min_size += size; @@ -165,7 +145,7 @@ impl<'a> LayoutComputer<'a> { max_align = max(max_align, h.min_alignment); uninhabited_part |= h.possibly_uninhabited; } - None => uninhabited_part |= ty.is_possibly_uninhabited(), + None => uninhabited_part |= field.ty.is_possibly_uninhabited(), } } @@ -197,7 +177,6 @@ impl<'a> LayoutComputer<'a> { fn compute_c_layout_from_fields( &mut self, fields: &Vector, - ty_var_map: &HashMap, generic_ctx: GenericCtx<'_>, ) -> LayoutHint { let mut total_min_size = 0; @@ -205,14 +184,7 @@ impl<'a> LayoutComputer<'a> { let mut uninhabited_part = false; for field in fields { - let ty = if field.ty.is_type_var() { - let id = field.ty.as_type_var().unwrap().get_raw(); - ty_var_map.get(id).unwrap() - } else { - &field.ty - }; - - match self.get_layout_of(ty, generic_ctx) { + match self.get_layout_of(&field.ty, generic_ctx) { Some(Either::Left(l)) => { if let Some(size) = l.size { total_min_size += size; @@ -227,7 +199,7 @@ impl<'a> LayoutComputer<'a> { max_align = max(max_align, h.min_alignment); uninhabited_part |= h.possibly_uninhabited; } - None => uninhabited_part |= ty.is_possibly_uninhabited(), + None => uninhabited_part |= field.ty.is_possibly_uninhabited(), }; } @@ -249,35 +221,21 @@ impl<'a> LayoutComputer<'a> { let generics = &*type_decl_ref.generics; let type_decl_id = type_decl_ref.id.as_adt()?; let type_decl = self.krate.type_decls.get(*type_decl_id)?; + // Substitute the generic arguments for the generic parameters. + let subst_kind = type_decl.kind.clone().substitute_frees(generics); - // If we certainly can't instantiate all relevant type parameters, fail. - /* if generics.types.elem_count() != type_decl.generics.types.elem_count() - || generics.types.iter().find(|ty| ty.is_type_var()).is_some() - { - return None; - } */ - - // Map the generic type parameter variables to the given instantiations. - let ty_var_map: HashMap = type_decl - .generics - .types - .iter() - .map(|ty_var| ty_var.index) - .zip(generics.types.iter().cloned()) - .collect(); - - match &type_decl.kind { + match &subst_kind { TypeDeclKind::Struct(fields) => { if type_decl.is_c_repr() { - Some(Either::Right(self.compute_c_layout_from_fields(fields, &ty_var_map, generic_ctx))) + Some(Either::Right(self.compute_c_layout_from_fields(fields, generic_ctx))) } else { - self.compute_layout_from_fields(fields, &ty_var_map, generic_ctx, type_decl.is_transparent(), type_decl.forced_alignment(), false) + self.compute_layout_from_fields(fields, generic_ctx, type_decl.is_transparent(), type_decl.forced_alignment(), false) } } TypeDeclKind::Enum(variants) => { // Assume that there could be a niche and ignore the discriminant for the hint. let variant_layouts: Vec>> = variants.iter().map(|variant| - self.compute_layout_from_fields(&variant.fields, &ty_var_map, generic_ctx, false,type_decl.forced_alignment(), true) + self.compute_layout_from_fields(&variant.fields, generic_ctx, false,type_decl.forced_alignment(), true) ).collect(); // If all variants have at least a layout hint, combine them. if variant_layouts.iter().all(|l| l.is_some()) { @@ -351,7 +309,7 @@ impl<'a> LayoutComputer<'a> { } } - /// Computes the trivial layout of an array, unless it's zero-sized (cf. https://github.com/rust-lang/rust/issues/81996). + /// Computes the trivial layout of an array, unless it's zero-sized (cf. ). fn get_layout_of_array( &mut self, elem_ty: &Ty, @@ -438,10 +396,47 @@ impl<'a> LayoutComputer<'a> { TypeId::Builtin(builtin_ty) => { match builtin_ty { BuiltinTy::Box => { - // Box has only one relevant type parameters: the boxed type. + // Box has two type parameters, the first is the contained type, the second is the allocator. let boxed_ty = type_decl_ref.generics.types.get(TypeVarId::ZERO).unwrap(); - Some(self.get_layout_of_ptr_type(boxed_ty, generic_ctx)) + let allocator_ty = + type_decl_ref.generics.types.get(TypeVarId::new(1)).unwrap(); + + if let Some(TypeDeclRef { + id: TypeId::Adt(alloc_td_id), + .. + }) = allocator_ty.as_adt() + && let Some(alloc_td) = self.krate.type_decls.get(*alloc_td_id) + && alloc_td.item_meta.lang_item + == Some("global_alloc_ty".to_owned()) + { + // If the allocator is `Global`, Box behaves as a pointer. + Some(self.get_layout_of_ptr_type(boxed_ty, generic_ctx)) + } else { + // Otherwise, it needs to be handled as if it was a struct with two fields (the allocator might be a ZST). + let pseudo_fields = [ + Field { + span: Span::dummy(), + attr_info: AttrInfo::default(), + name: None, + ty: boxed_ty.clone(), + }, + Field { + span: Span::dummy(), + attr_info: AttrInfo::default(), + name: None, + ty: allocator_ty.clone(), + }, + ] + .into(); + self.compute_layout_from_fields( + &pseudo_fields, + generic_ctx, + false, + None, + false, + ) + } } // Slices are non-sized and can be handled as such. BuiltinTy::Slice | BuiltinTy::Str => { @@ -467,7 +462,7 @@ impl<'a> LayoutComputer<'a> { TyKind::Literal(literal_ty) => { let size = literal_ty.target_size(self.krate.target_information.target_pointer_size); - let new_layout = Layout::mk_simple_layout(size as u64); + let new_layout = Layout::mk_literal_layout(size as u64); let layout_ref = Box::leak(Box::new(new_layout)); Some(Either::Left(layout_ref)) } diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 12d8f2d4b..4d90d7bcd 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -963,10 +963,19 @@ pub trait VarsVisitor { pub(crate) struct SubstVisitor<'a> { generics: &'a GenericArgs, self_ref: &'a TraitRefKind, + subst_frees: bool, } impl<'a> SubstVisitor<'a> { - pub(crate) fn new(generics: &'a GenericArgs, self_ref: &'a TraitRefKind) -> Self { - Self { generics, self_ref } + pub(crate) fn new( + generics: &'a GenericArgs, + self_ref: &'a TraitRefKind, + subst_frees: bool, + ) -> Self { + Self { + generics, + self_ref, + subst_frees, + } } /// Returns the value for this variable, if any. @@ -985,7 +994,13 @@ impl<'a> SubstVisitor<'a> { get(varid).clone() }) } - DeBruijnVar::Free(..) => None, + DeBruijnVar::Free(varid) => { + if self.subst_frees { + Some(get(varid).clone()) + } else { + None + } + } } } } @@ -1093,7 +1108,20 @@ pub trait TyVisitable: Sized + AstVisitable { } fn substitute_with_self(mut self, generics: &GenericArgs, self_ref: &TraitRefKind) -> Self { - let _ = self.visit_vars(&mut SubstVisitor::new(generics, self_ref)); + let _ = self.visit_vars(&mut SubstVisitor::new(generics, self_ref, false)); + self + } + + fn substitute_frees(self, generics: &GenericArgs) -> Self { + self.substitute_with_self_frees(generics, &TraitRefKind::SelfId) + } + + fn substitute_with_self_frees( + mut self, + generics: &GenericArgs, + self_ref: &TraitRefKind, + ) -> Self { + let _ = self.visit_vars(&mut SubstVisitor::new(generics, self_ref, true)); self } @@ -1248,17 +1276,17 @@ impl Layout { } } - /// Construct a simple layout with a single variant and a single field of `size`. + /// Construct a simple layout with a single variant and no fields. /// /// Assumes that the alignment is the same as the size. - pub fn mk_simple_layout(size: ByteCount) -> Self { + pub fn mk_literal_layout(size: ByteCount) -> Self { Self { size: Some(size), align: Some(size), discriminant_layout: None, uninhabited: false, variant_layouts: [VariantLayout { - field_offsets: [0].into(), + field_offsets: [].into(), uninhabited: false, tag: None, }] @@ -1268,7 +1296,7 @@ impl Layout { /// Constructs the layout of a thin pointer. pub fn mk_ptr_layout_wo_metadata(ptr_size: ByteCount) -> Self { - Self::mk_simple_layout(ptr_size) + Self::mk_literal_layout(ptr_size) } /// Constructs the layout of a 1ZST, i.e. a zero-sized type with alignment 1. @@ -1279,7 +1307,7 @@ impl Layout { discriminant_layout: None, uninhabited: false, variant_layouts: [VariantLayout { - field_offsets: [0].into(), + field_offsets: [].into(), uninhabited: false, tag: None, }] diff --git a/charon/tests/layout.json b/charon/tests/layout.json index 6b454b8a7..18d4329c5 100644 --- a/charon/tests/layout.json +++ b/charon/tests/layout.json @@ -591,13 +591,14 @@ "test_crate::NestedPointers": null, "test_crate::GenericC": null, "test_crate::HasArray": { - "size": 32, - "align": 4, + "size": 40, + "align": 8, "discriminant_layout": null, "uninhabited": false, "variant_layouts": [ { "field_offsets": [ + 8, 0 ], "uninhabited": false, @@ -605,6 +606,7 @@ } ] }, + "test_crate::HasBoxWAlloc": null, "test_crate::Instance": { "size": 8, "align": 4, diff --git a/charon/tests/layout.rs b/charon/tests/layout.rs index cbe40ff62..c8218d7e3 100644 --- a/charon/tests/layout.rs +++ b/charon/tests/layout.rs @@ -16,8 +16,11 @@ fn type_layout() -> anyhow::Result<()> { let crate_data = translate_rust_text( r#" #![feature(never_type)] + #![feature(allocator_api)] use std::num::NonZero; + use std::ptr::NonNull; use std::fmt::Debug; + use std::alloc::Allocator; struct SimpleStruct { x: u32, @@ -158,7 +161,12 @@ fn type_layout() -> anyhow::Result<()> { } struct HasArray { - a: [u32; 8] + a: [u32; 8], + b: NonNull, + } + + struct HasBoxWAlloc { + b: Box } type Instance = GenericC; @@ -166,7 +174,7 @@ fn type_layout() -> anyhow::Result<()> { type InstanceGen2<'a,T: Sized> = GenericC<&'a T,T>; type InstanceGen3<'a,T: ?Sized> = GenericC<&'a T,i32>; "#, - &[], + &["--include=core::ptr::non_null::*"], )?; // Check whether niche discriminant computations are correct, i.e. reversible. diff --git a/charon/tests/layouts_and_hints.json b/charon/tests/layouts_and_hints.json index c4cf1700e..8f3f3ac4a 100644 --- a/charon/tests/layouts_and_hints.json +++ b/charon/tests/layouts_and_hints.json @@ -25,9 +25,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -43,9 +41,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -115,9 +111,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -154,9 +148,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -171,9 +163,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -220,6 +210,48 @@ ] } }, + "NonNull": { + "Left": { + "size": 8, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, + "alloc::boxed::Box[MetaSized, @TraitClause0, @TraitClause1]": { + "Right": { + "min_size": 40, + "min_alignment": 8, + "possibly_uninhabited": true + } + }, + "HasArray": { + "Left": { + "size": 40, + "align": 8, + "discriminant_layout": null, + "uninhabited": false, + "variant_layouts": [ + { + "field_offsets": [ + 8, + 0 + ], + "uninhabited": false, + "tag": null + } + ] + } + }, "GenericC[Sized, Sized]": { "Right": { "min_size": 6, @@ -235,9 +267,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -309,9 +339,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -349,9 +377,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -374,9 +400,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -423,6 +447,13 @@ ] } }, + "*const @Type0": { + "Right": { + "min_size": 8, + "min_alignment": 8, + "possibly_uninhabited": false + } + }, "&'_1 (GenericButFixedSize<'_0, @Type0>[@TraitClause0])": { "Left": { "size": 8, @@ -431,9 +462,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -485,9 +514,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -520,9 +547,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -574,9 +599,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -609,9 +632,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -633,9 +654,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -650,9 +669,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -685,9 +702,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -761,12 +776,18 @@ }, "Result>, AllocError>[Sized>>, Sized]": { "Right": { - "min_size": 0, - "min_alignment": 1, + "min_size": 16, + "min_alignment": 8, + "possibly_uninhabited": false + } + }, + "NonNull>": { + "Right": { + "min_size": 16, + "min_alignment": 8, "possibly_uninhabited": false } }, - "NonNull>": null, "Slice": { "Left": { "size": null, @@ -797,7 +818,6 @@ ] } }, - "NonNull": null, "&'_0 (NonZeroU32Inner)": { "Left": { "size": 8, @@ -806,9 +826,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -840,9 +858,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -857,9 +873,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -894,9 +908,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -913,9 +925,7 @@ "uninhabited": false, "variant_layouts": [ { - "field_offsets": [ - 0 - ], + "field_offsets": [], "uninhabited": false, "tag": null } @@ -932,6 +942,13 @@ "N": null, "A": null, "B": null, + "alloc::boxed::Box[MetaSized, @TraitClause0, @TraitClause1]": { + "Right": { + "min_size": 40, + "min_alignment": 8, + "possibly_uninhabited": true + } + }, "GenericC<&'a (T), &'static (Str)>[Sized<&'_ (T)>, Sized<&'_ (Str)>]": { "Right": { "min_size": 25, @@ -953,5 +970,12 @@ "possibly_uninhabited": false } }, - "fn<'_0, '_1, '_2>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)), &'_0_1 mut (Formatter<'_0_2>)) -> Result<(), Error>[Sized<()>, Sized]": null + "fn<'_0, '_1, '_2>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Debug<_dyn> + _dyn : '_)), &'_0_1 mut (Formatter<'_0_2>)) -> Result<(), Error>[Sized<()>, Sized]": null, + "*const T": { + "Right": { + "min_size": 8, + "min_alignment": 8, + "possibly_uninhabited": false + } + } } \ No newline at end of file From 6250f6371a692cff5b28b1a1ae89e64340547ae0 Mon Sep 17 00:00:00 2001 From: Florian Sextl Date: Thu, 18 Sep 2025 08:39:48 +0200 Subject: [PATCH 7/7] add new docs for TyVisitable --- charon-ml/src/CharonVersion.ml | 2 +- charon/Cargo.lock | 2 +- charon/Cargo.toml | 2 +- charon/src/ast/types_utils.rs | 2 ++ 4 files changed, 5 insertions(+), 3 deletions(-) diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index b4e50e3fc..60b944b15 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.127" +let supported_charon_version = "0.1.128" diff --git a/charon/Cargo.lock b/charon/Cargo.lock index df4f3686c..e94807957 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -201,7 +201,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" [[package]] name = "charon" -version = "0.1.127" +version = "0.1.128" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 4372e2e10..60907c760 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.127" +version = "0.1.128" authors = [ "Son Ho ", "Guillaume Boisseau ", diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 4d90d7bcd..ac88739b2 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -1103,6 +1103,7 @@ pub trait TyVisitable: Sized + AstVisitable { }); } + /// Substitutes all bound variables with the corresponding arguments. fn substitute(self, generics: &GenericArgs) -> Self { self.substitute_with_self(generics, &TraitRefKind::SelfId) } @@ -1112,6 +1113,7 @@ pub trait TyVisitable: Sized + AstVisitable { self } + /// Same as [`TyVisitable::substitute`], but also substitutes free variables. fn substitute_frees(self, generics: &GenericArgs) -> Self { self.substitute_with_self_frees(generics, &TraitRefKind::SelfId) }