From 31cb24d9596468570dc3569cb17986f4d4b20b29 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 24 Oct 2024 17:13:11 -0400 Subject: [PATCH 1/5] fix codegen for rvalue aggregate raw pointer to an adt with slice tail --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 12 ++++- tests/kani/CodegenRawPtrADTSliceTail/main.rs | 49 +++++++++++++++++++ 2 files changed, 60 insertions(+), 1 deletion(-) create mode 100644 tests/kani/CodegenRawPtrADTSliceTail/main.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 7f578940d98e..efb592354cac 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -709,13 +709,23 @@ impl GotocCtx<'_> { let meta = self.codegen_operand_stable(&operands[1]); slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) } - TyKind::RigidTy(RigidTy::Adt(..)) => { + TyKind::RigidTy(RigidTy::Adt(_, generic_args)) => { 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 + // Case 1: Last field is a slice + } else if !generic_args.0.is_empty() + && generic_args.0.first().unwrap().expect_ty().kind().is_slice() + { + slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) + // Case 2: Last field is a trait object } else { let vtable_expr = meta .member("_vtable_ptr", &self.symbol_table) diff --git a/tests/kani/CodegenRawPtrADTSliceTail/main.rs b/tests/kani/CodegenRawPtrADTSliceTail/main.rs new file mode 100644 index 000000000000..c87101b44b5f --- /dev/null +++ b/tests/kani/CodegenRawPtrADTSliceTail/main.rs @@ -0,0 +1,49 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Test codegen for a raw pointer to a struct whose last field is a slice + +#![feature(layout_for_ptr)] +#![feature(ptr_metadata)] + +// https://github.com/model-checking/kani/issues/3615 +mod issue_3615 { + use std::ptr; + + #[derive(Clone, Copy, kani::Arbitrary)] + struct Wrapper { + _size: usize, + _value: T, + } + + #[kani::proof] + pub fn check_size_of_overflows() { + let var: Wrapper<[u64; 4]> = kani::any(); + let fat_ptr: *const Wrapper<[u64]> = &var as *const _; + let (thin_ptr, _) = fat_ptr.to_raw_parts(); + let new_size: usize = kani::any(); + let _new_ptr: *const Wrapper<[u64]> = ptr::from_raw_parts(thin_ptr, new_size); + } +} + +// https://github.com/model-checking/kani/issues/3638 +mod issue_3638 { + use std::ptr::NonNull; + + #[derive(kani::Arbitrary)] + struct Wrapper(usize, T); + + #[cfg(kani)] + #[kani::proof] + fn main() { + // Create a SampleTrait 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 + 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 + let _: NonNull> = NonNull::from_raw_parts(slice_ptr, metadata); + } +} From 857e32df23efff8ed8165dcac21f034fa4e787a3 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 11 Nov 2024 16:06:41 -0500 Subject: [PATCH 2/5] make slice the unconditional else case --- .../src/codegen_cprover_gotoc/codegen/rvalue.rs | 17 +++-------------- tests/kani/CodegenRawPtrADTSliceTail/main.rs | 11 ++++++++++- 2 files changed, 13 insertions(+), 15 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index efb592354cac..aa35b76916b2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -709,7 +709,7 @@ 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 pointee_goto_typ = self.codegen_ty_stable(pointee_ty); let data_cast = data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) }); @@ -719,21 +719,10 @@ impl GotocCtx<'_> { 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. + // The only way to construct such a DST is by making the type generic and having the last field be a slice, // c.f. https://doc.rust-lang.org/nomicon/exotic-sizes.html#dynamically-sized-types-dsts - // Case 1: Last field is a slice - } else if !generic_args.0.is_empty() - && generic_args.0.first().unwrap().expect_ty().kind().is_slice() - { - slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) - // Case 2: Last field is a trait object } 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) + slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) } } TyKind::RigidTy(RigidTy::Dynamic(..)) => { diff --git a/tests/kani/CodegenRawPtrADTSliceTail/main.rs b/tests/kani/CodegenRawPtrADTSliceTail/main.rs index c87101b44b5f..8d82ff0abdf3 100644 --- a/tests/kani/CodegenRawPtrADTSliceTail/main.rs +++ b/tests/kani/CodegenRawPtrADTSliceTail/main.rs @@ -16,13 +16,22 @@ mod issue_3615 { } #[kani::proof] - pub fn check_size_of_overflows() { + pub fn from_raw_parts_for_slices() { let var: Wrapper<[u64; 4]> = kani::any(); let fat_ptr: *const Wrapper<[u64]> = &var as *const _; let (thin_ptr, _) = fat_ptr.to_raw_parts(); let new_size: usize = kani::any(); let _new_ptr: *const Wrapper<[u64]> = ptr::from_raw_parts(thin_ptr, new_size); } + + #[kani::proof] + pub fn from_raw_parts_for_slices_nested() { + let var: Wrapper> = kani::any(); + let fat_ptr: *const Wrapper> = &var as *const _; + let (thin_ptr, _) = fat_ptr.to_raw_parts(); + let new_size: usize = kani::any(); + let _new_ptr: *const Wrapper> = ptr::from_raw_parts(thin_ptr, new_size); + } } // https://github.com/model-checking/kani/issues/3638 From bb7d7099ebe4a07f66487c68a1894b566ab66333 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 11 Nov 2024 16:48:55 -0500 Subject: [PATCH 3/5] traverse type --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 23 ++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index aa35b76916b2..69d45a9bb102 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -709,7 +709,7 @@ impl GotocCtx<'_> { let meta = self.codegen_operand_stable(&operands[1]); slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) } - TyKind::RigidTy(RigidTy::Adt(..)) => { + TyKind::RigidTy(RigidTy::Adt(_, generic_args)) => { let pointee_goto_typ = self.codegen_ty_stable(pointee_ty); let data_cast = data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) }); @@ -719,10 +719,27 @@ impl GotocCtx<'_> { 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. - // The only way to construct such a DST is by making the type generic and having the last field be a slice, // c.f. https://doc.rust-lang.org/nomicon/exotic-sizes.html#dynamically-sized-types-dsts } else { - slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) + 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) + } } } TyKind::RigidTy(RigidTy::Dynamic(..)) => { From ae455cf347c694f18c68e5c015d8efebeab1e174 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 14 Nov 2024 12:43:33 -0800 Subject: [PATCH 4/5] 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); } } From d79d2eefd738ba8e5c7cba9fc3bca92c4a22c83e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 14 Nov 2024 22:09:42 -0800 Subject: [PATCH 5/5] Apply suggestions from code review Co-authored-by: Qinheping Hu --- kani-compiler/src/kani_middle/abi.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/kani_middle/abi.rs b/kani-compiler/src/kani_middle/abi.rs index 08b3e34c3995..bb1e597638da 100644 --- a/kani-compiler/src/kani_middle/abi.rs +++ b/kani-compiler/src/kani_middle/abi.rs @@ -49,8 +49,9 @@ impl LayoutOf { /// 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 foreign types, return `None`. + /// For unsized types, this should return either a slice, a string slice, a dynamic type, + /// or a foreign type. /// For other types, this function will return `None`. pub fn unsized_tail(&self) -> Option { if self.layout.is_unsized() { @@ -68,7 +69,7 @@ impl LayoutOf { } } - /// Return the type of the elements of the array or slice at the unsized tail of this type. + /// Return the type of the elements of the slice or `str` 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 {