From ae455cf347c694f18c68e5c015d8efebeab1e174 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 14 Nov 2024 12:43:33 -0800 Subject: [PATCH] Fix aggregate and add new abi module --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 52 +++-- .../src/codegen_cprover_gotoc/codegen/typ.rs | 13 +- kani-compiler/src/kani_middle/abi.rs | 194 ++++++++++++++++++ kani-compiler/src/kani_middle/mod.rs | 1 + .../main.rs => AggregateRvalue/dyn_ptr.rs} | 0 .../main.rs => AggregateRvalue/slice_ptr.rs} | 8 +- 6 files changed, 228 insertions(+), 40 deletions(-) create mode 100644 kani-compiler/src/kani_middle/abi.rs rename tests/kani/{CodegenAggregateRawPtrTraitObject/main.rs => AggregateRvalue/dyn_ptr.rs} (100%) rename tests/kani/{CodegenRawPtrADTSliceTail/main.rs => AggregateRvalue/slice_ptr.rs} (88%) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 69d45a9bb102..c5f2f9fd2c08 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -6,6 +6,7 @@ use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace; use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable; use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr}; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; +use crate::kani_middle::abi::LayoutOf; use crate::kani_middle::coercion::{ CoerceUnsizedInfo, CoerceUnsizedIterator, CoercionBaseStable, extract_unsize_casting_stable, }; @@ -709,38 +710,33 @@ impl GotocCtx<'_> { let meta = self.codegen_operand_stable(&operands[1]); slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) } - TyKind::RigidTy(RigidTy::Adt(_, generic_args)) => { + TyKind::RigidTy(RigidTy::Adt(..)) => { + let layout = LayoutOf::new(pointee_ty); let pointee_goto_typ = self.codegen_ty_stable(pointee_ty); let data_cast = data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) }); - let meta = self.codegen_operand_stable(&operands[1]); - // This is a thin raw pointer; `pointee_ty` is a statically sized ADT and has zero-sized metadata. - if meta.typ().sizeof(&self.symbol_table) == 0 { - data_cast - // This is a wide raw pointer; `pointee_ty` is a DST and has non-zero-sized metadata. - // An ADT can be a DST if it is a struct and its last field is a DST. - // c.f. https://doc.rust-lang.org/nomicon/exotic-sizes.html#dynamically-sized-types-dsts - } else { - let mut dst_field = *generic_args.0.first().expect("To construct an ADT that is a DST, there must be a generic argument").expect_ty(); - while let TyKind::RigidTy(RigidTy::Adt(_, generic_args)) = - dst_field.kind() - { - dst_field = *generic_args.0.first().unwrap().expect_ty(); - } - - if dst_field.kind().is_slice() { - slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) - } else { - let vtable_expr = meta - .member("_vtable_ptr", &self.symbol_table) - .member("pointer", &self.symbol_table) - .cast_to( - typ.lookup_field_type("vtable", &self.symbol_table) - .unwrap(), - ); - dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table) + layout.unsized_tail().map_or(data_cast.clone(), |tail| { + let meta = self.codegen_operand_stable(&operands[1]); + match tail.kind().rigid().unwrap() { + RigidTy::Foreign(..) => data_cast, + RigidTy::Slice(..) | RigidTy::Str => { + slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) + } + RigidTy::Dynamic(..) => { + let vtable_expr = meta + .member("_vtable_ptr", &self.symbol_table) + .member("pointer", &self.symbol_table) + .cast_to( + typ.lookup_field_type("vtable", &self.symbol_table) + .unwrap(), + ); + dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table) + } + _ => { + unreachable!("Unexpected unsized tail: {tail:?}"); + } } - } + }) } TyKind::RigidTy(RigidTy::Dynamic(..)) => { let pointee_goto_typ = self.codegen_ty_stable(pointee_ty); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 7181ce36f18e..cc7f3655f51f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1571,14 +1571,11 @@ impl<'tcx> GotocCtx<'tcx> { return None; } - let mut typ = struct_type; - while let ty::Adt(adt_def, adt_args) = typ.kind() { - assert_eq!(adt_def.variants().len(), 1, "Expected a single-variant ADT. Found {typ:?}"); - let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields; - let last_field = fields.last_index().expect("Trait should be the last element."); - typ = fields[last_field].ty(self.tcx, adt_args); - } - if typ.is_trait() { Some(typ) } else { None } + let ty = rustc_internal::stable(struct_type); + rustc_internal::internal( + self.tcx, + crate::kani_middle::abi::LayoutOf::new(ty).unsized_tail(), + ) } /// This function provides an iterator that traverses the data path of a receiver type. I.e.: diff --git a/kani-compiler/src/kani_middle/abi.rs b/kani-compiler/src/kani_middle/abi.rs new file mode 100644 index 000000000000..08b3e34c3995 --- /dev/null +++ b/kani-compiler/src/kani_middle/abi.rs @@ -0,0 +1,194 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module contains code for handling type abi information. + +use stable_mir::abi::{FieldsShape, LayoutShape}; +use stable_mir::ty::{RigidTy, Ty, TyKind, UintTy}; +use tracing::debug; + +/// A struct to encapsulate the layout information for a given type +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct LayoutOf { + ty: Ty, + layout: LayoutShape, +} + +#[allow(dead_code)] // TODO: Remove this in https://github.com/model-checking/kani/pull/3687 +impl LayoutOf { + /// Create the layout structure for the given type + pub fn new(ty: Ty) -> LayoutOf { + LayoutOf { ty, layout: ty.layout().unwrap().shape() } + } + + /// Return whether the type is sized. + pub fn is_sized(&self) -> bool { + self.layout.is_sized() + } + + /// Return whether the type is unsized and its tail is a foreign item. + /// + /// This will also return `true` if the type is foreign. + pub fn has_foreign_tail(&self) -> bool { + self.unsized_tail() + .map_or(false, |t| matches!(t.kind(), TyKind::RigidTy(RigidTy::Foreign(_)))) + } + + /// Return whether the type is unsized and its tail is a trait object. + pub fn has_trait_tail(&self) -> bool { + self.unsized_tail().map_or(false, |t| t.kind().is_trait()) + } + + /// Return whether the type is unsized and its tail is a slice. + #[allow(dead_code)] + pub fn has_slice_tail(&self) -> bool { + self.unsized_tail().map_or(false, |tail| { + let kind = tail.kind(); + kind.is_slice() | kind.is_str() + }) + } + + /// Return the unsized tail of the type if this is an unsized type. + /// + /// For foreign types, return None. + /// For unsized types, this should return either a slice, a string slice, a dynamic type. + /// For other types, this function will return `None`. + pub fn unsized_tail(&self) -> Option { + if self.layout.is_unsized() { + match self.ty.kind().rigid().unwrap() { + RigidTy::Slice(..) | RigidTy::Dynamic(..) | RigidTy::Str => Some(self.ty), + RigidTy::Adt(..) | RigidTy::Tuple(..) => { + // Recurse the tail field type until we find the unsized tail. + self.last_field_layout().unsized_tail() + } + RigidTy::Foreign(_) => Some(self.ty), + _ => unreachable!("Expected unsized type but found `{}`", self.ty), + } + } else { + None + } + } + + /// Return the type of the elements of the array or slice at the unsized tail of this type. + /// + /// For sized types and trait unsized type, this function will return `None`. + pub fn unsized_tail_elem_ty(&self) -> Option { + self.unsized_tail().and_then(|tail| match tail.kind().rigid().unwrap() { + RigidTy::Slice(elem_ty) => Some(*elem_ty), + // String slices have the same layout as slices of u8. + // https://doc.rust-lang.org/reference/type-layout.html#str-layout + RigidTy::Str => Some(Ty::unsigned_ty(UintTy::U8)), + _ => None, + }) + } + + /// Return the size of the sized portion of this type. + /// + /// For a sized type, this function will return the size of the type. + /// For an unsized type, this function will return the size of the sized portion including + /// any padding bytes that lead to the unsized field. + /// I.e.: the size of the type, excluding the trailing unsized portion. + /// + /// For example, this function will return 2 as the sized portion of `*const (u8, [u16])`: + pub fn size_of_head(&self) -> usize { + if self.is_sized() { + self.layout.size.bytes() + } else { + match self.ty.kind().rigid().unwrap() { + RigidTy::Slice(_) | RigidTy::Str | RigidTy::Dynamic(..) | RigidTy::Foreign(..) => 0, + RigidTy::Adt(..) | RigidTy::Tuple(..) => { + let fields_sorted = self.layout.fields.fields_by_offset_order(); + let last = *fields_sorted.last().unwrap(); + let FieldsShape::Arbitrary { ref offsets } = self.layout.fields else { + unreachable!() + }; + + // We compute the size of the sized portion by taking the position of the + // last element + the sized portion of that element. + let unsized_offset_unadjusted = offsets[last].bytes(); + debug!(ty=?self.ty, ?unsized_offset_unadjusted, "size_of_sized_portion"); + unsized_offset_unadjusted + self.last_field_layout().size_of_head() + } + _ => { + unreachable!("Expected sized type, but found: `{}`", self.ty) + } + } + } + } + + /// Return the alignment of the fields that are sized from the head of the object. + /// + /// For a sized type, this function will return the alignment of the type. + /// + /// For an unsized type, this function will return the alignment of the sized portion. + /// The alignment of the type will be the maximum of the alignment of the sized portion + /// and the alignment of the unsized portion. + /// + /// If there's no sized portion, this function will return the minimum alignment (i.e.: 1). + pub fn align_of_head(&self) -> usize { + if self.is_sized() { + self.layout.abi_align.try_into().unwrap() + } else { + match self.ty.kind().rigid().unwrap() { + RigidTy::Slice(_) | RigidTy::Str | RigidTy::Dynamic(..) | RigidTy::Foreign(..) => 1, + RigidTy::Adt(..) | RigidTy::Tuple(..) => { + // We have to recurse and get the maximum alignment of all sized portions. + let field_layout = self.last_field_layout(); + field_layout.align_of_head().max(self.layout.abi_align.try_into().unwrap()) + } + _ => { + unreachable!("Expected sized type, but found: `{}`", self.ty); + } + } + } + } + + /// Return the size of the type if it's known at compilation type. + pub fn size_of(&self) -> Option { + if self.is_sized() { Some(self.layout.size.bytes()) } else { None } + } + + /// Return the alignment of the type if it's know at compilation time. + /// + /// The alignment is known at compilation type for sized types and types with slice tail. + /// + /// Note: We assume u64 and usize are the same since Kani is only supported in 64bits machines. + /// Add a configuration in case we ever decide to port this to a 32-bits machine. + #[cfg(target_pointer_width = "64")] + pub fn align_of(&self) -> Option { + if self.is_sized() || self.has_slice_tail() { + self.layout.abi_align.try_into().ok() + } else { + None + } + } + + /// Return the layout of the last field of the type. + /// + /// This function is used to get the layout of the last field of an unsized type. + /// For example, if we have `*const (u8, [u16])`, the last field is `[u16]`. + /// This function will return the layout of `[u16]`. + /// + /// If the type is not a struct, an enum, or a tuple, with at least one field, this function + /// will panic. + fn last_field_layout(&self) -> LayoutOf { + match self.ty.kind().rigid().unwrap() { + RigidTy::Adt(adt_def, adt_args) => { + let fields = adt_def.variants_iter().next().unwrap().fields(); + let fields_sorted = self.layout.fields.fields_by_offset_order(); + let last_field_idx = *fields_sorted.last().unwrap(); + LayoutOf::new(fields[last_field_idx].ty_with_args(adt_args)) + } + RigidTy::Tuple(tys) => { + // For tuples, the unsized field is currently the last declared. + // To be on the safe side, we still get the sorted list by offset order. + let fields_sorted = self.layout.fields.fields_by_offset_order(); + let last_field_idx = *fields_sorted.last().unwrap(); + let last_ty = tys[last_field_idx]; + LayoutOf::new(last_ty) + } + _ => { + unreachable!("Expected struct, enum or tuple. Found: `{}`", self.ty); + } + } + } +} diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 3e1c7e3b4fca..631de58f5915 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -26,6 +26,7 @@ use std::ops::ControlFlow; use self::attributes::KaniAttributes; +pub mod abi; pub mod analysis; pub mod attributes; pub mod codegen_units; diff --git a/tests/kani/CodegenAggregateRawPtrTraitObject/main.rs b/tests/kani/AggregateRvalue/dyn_ptr.rs similarity index 100% rename from tests/kani/CodegenAggregateRawPtrTraitObject/main.rs rename to tests/kani/AggregateRvalue/dyn_ptr.rs diff --git a/tests/kani/CodegenRawPtrADTSliceTail/main.rs b/tests/kani/AggregateRvalue/slice_ptr.rs similarity index 88% rename from tests/kani/CodegenRawPtrADTSliceTail/main.rs rename to tests/kani/AggregateRvalue/slice_ptr.rs index 8d82ff0abdf3..6df42475c618 100644 --- a/tests/kani/CodegenRawPtrADTSliceTail/main.rs +++ b/tests/kani/AggregateRvalue/slice_ptr.rs @@ -43,16 +43,16 @@ mod issue_3638 { #[cfg(kani)] #[kani::proof] - fn main() { - // Create a SampleTrait object from SampleStruct + fn slice_from_raw() { + // Create a SampleSlice object from SampleStruct let original: Wrapper<[u8; 10]> = kani::any(); let slice: &Wrapper<[u8]> = &original; - // Get the raw data pointer and metadata for the trait object + // Get the raw data pointer and metadata for the slice object let slice_ptr = NonNull::new(slice as *const _ as *mut ()).unwrap(); let metadata = std::ptr::metadata(slice); - // Create NonNull from the data pointer and metadata + // Create NonNull<[u8]> from the data pointer and metadata let _: NonNull> = NonNull::from_raw_parts(slice_ptr, metadata); } }