Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix codegen for rvalue aggregate raw pointer to an adt with slice tail #3644

Merged
merged 7 commits into from
Nov 15, 2024
Merged
Show file tree
Hide file tree
Changes from 6 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 24 additions & 12 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
};
Expand Down Expand Up @@ -710,21 +711,32 @@ impl GotocCtx<'_> {
slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
}
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]);
if meta.typ().sizeof(&self.symbol_table) == 0 {
data_cast
} 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);
Expand Down
13 changes: 5 additions & 8 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.:
Expand Down
194 changes: 194 additions & 0 deletions kani-compiler/src/kani_middle/abi.rs
Original file line number Diff line number Diff line change
@@ -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.
celinval marked this conversation as resolved.
Show resolved Hide resolved
/// For unsized types, this should return either a slice, a string slice, a dynamic type.
celinval marked this conversation as resolved.
Show resolved Hide resolved
/// For other types, this function will return `None`.
pub fn unsized_tail(&self) -> Option<Ty> {
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()
qinheping marked this conversation as resolved.
Show resolved Hide resolved
}
RigidTy::Foreign(_) => Some(self.ty),
celinval marked this conversation as resolved.
Show resolved Hide resolved
_ => 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.
celinval marked this conversation as resolved.
Show resolved Hide resolved
///
/// For sized types and trait unsized type, this function will return `None`.
pub fn unsized_tail_elem_ty(&self) -> Option<Ty> {
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<usize> {
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<usize> {
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);
}
}
}
}
1 change: 1 addition & 0 deletions kani-compiler/src/kani_middle/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
58 changes: 58 additions & 0 deletions tests/kani/AggregateRvalue/slice_ptr.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
// 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 {
qinheping marked this conversation as resolved.
Show resolved Hide resolved
use std::ptr;

#[derive(Clone, Copy, kani::Arbitrary)]
struct Wrapper<T: ?Sized> {
_size: usize,
_value: T,
}

#[kani::proof]
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<Wrapper<[u8; 4]>> = kani::any();
let fat_ptr: *const Wrapper<Wrapper<[u8]>> = &var as *const _;
let (thin_ptr, _) = fat_ptr.to_raw_parts();
let new_size: usize = kani::any();
let _new_ptr: *const Wrapper<Wrapper<[u8]>> = 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<T: ?Sized>(usize, T);

#[cfg(kani)]
#[kani::proof]
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 slice object
let slice_ptr = NonNull::new(slice as *const _ as *mut ()).unwrap();
let metadata = std::ptr::metadata(slice);

// Create NonNull<[u8]> from the data pointer and metadata
let _: NonNull<Wrapper<[u8]>> = NonNull::from_raw_parts(slice_ptr, metadata);
}
}
Loading