Skip to content

Commit 9c2318b

Browse files
Carolyn Zechcelinvalqinheping
authored
Fix codegen for rvalue aggregate raw pointer to an adt with slice tail (#3644)
Fix the codegen for a raw pointer to a dynamically-sized ADT. Traverse the type until we find the tail, which will either be a trait object or a slice, and generate the pointer accordingly. Resolves #3638, #3615 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Celina G. Val <celinval@amazon.com> Co-authored-by: Qinheping Hu <qinhh@amazon.com>
1 parent 6b2dea2 commit 9c2318b

File tree

6 files changed

+283
-20
lines changed

6 files changed

+283
-20
lines changed

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

Lines changed: 24 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace;
66
use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
77
use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
88
use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
9+
use crate::kani_middle::abi::LayoutOf;
910
use crate::kani_middle::coercion::{
1011
CoerceUnsizedInfo, CoerceUnsizedIterator, CoercionBaseStable, extract_unsize_casting_stable,
1112
};
@@ -710,21 +711,32 @@ impl GotocCtx<'_> {
710711
slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
711712
}
712713
TyKind::RigidTy(RigidTy::Adt(..)) => {
714+
let layout = LayoutOf::new(pointee_ty);
713715
let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
714716
let data_cast =
715717
data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) });
716-
let meta = self.codegen_operand_stable(&operands[1]);
717-
if meta.typ().sizeof(&self.symbol_table) == 0 {
718-
data_cast
719-
} else {
720-
let vtable_expr = meta
721-
.member("_vtable_ptr", &self.symbol_table)
722-
.member("pointer", &self.symbol_table)
723-
.cast_to(
724-
typ.lookup_field_type("vtable", &self.symbol_table).unwrap(),
725-
);
726-
dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table)
727-
}
718+
layout.unsized_tail().map_or(data_cast.clone(), |tail| {
719+
let meta = self.codegen_operand_stable(&operands[1]);
720+
match tail.kind().rigid().unwrap() {
721+
RigidTy::Foreign(..) => data_cast,
722+
RigidTy::Slice(..) | RigidTy::Str => {
723+
slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
724+
}
725+
RigidTy::Dynamic(..) => {
726+
let vtable_expr = meta
727+
.member("_vtable_ptr", &self.symbol_table)
728+
.member("pointer", &self.symbol_table)
729+
.cast_to(
730+
typ.lookup_field_type("vtable", &self.symbol_table)
731+
.unwrap(),
732+
);
733+
dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table)
734+
}
735+
_ => {
736+
unreachable!("Unexpected unsized tail: {tail:?}");
737+
}
738+
}
739+
})
728740
}
729741
TyKind::RigidTy(RigidTy::Dynamic(..)) => {
730742
let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1571,14 +1571,11 @@ impl<'tcx> GotocCtx<'tcx> {
15711571
return None;
15721572
}
15731573

1574-
let mut typ = struct_type;
1575-
while let ty::Adt(adt_def, adt_args) = typ.kind() {
1576-
assert_eq!(adt_def.variants().len(), 1, "Expected a single-variant ADT. Found {typ:?}");
1577-
let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields;
1578-
let last_field = fields.last_index().expect("Trait should be the last element.");
1579-
typ = fields[last_field].ty(self.tcx, adt_args);
1580-
}
1581-
if typ.is_trait() { Some(typ) } else { None }
1574+
let ty = rustc_internal::stable(struct_type);
1575+
rustc_internal::internal(
1576+
self.tcx,
1577+
crate::kani_middle::abi::LayoutOf::new(ty).unsized_tail(),
1578+
)
15821579
}
15831580

15841581
/// This function provides an iterator that traverses the data path of a receiver type. I.e.:
Lines changed: 195 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,195 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
//! This module contains code for handling type abi information.
4+
5+
use stable_mir::abi::{FieldsShape, LayoutShape};
6+
use stable_mir::ty::{RigidTy, Ty, TyKind, UintTy};
7+
use tracing::debug;
8+
9+
/// A struct to encapsulate the layout information for a given type
10+
#[derive(Clone, Debug, PartialEq, Eq)]
11+
pub struct LayoutOf {
12+
ty: Ty,
13+
layout: LayoutShape,
14+
}
15+
16+
#[allow(dead_code)] // TODO: Remove this in https://github.com/model-checking/kani/pull/3687
17+
impl LayoutOf {
18+
/// Create the layout structure for the given type
19+
pub fn new(ty: Ty) -> LayoutOf {
20+
LayoutOf { ty, layout: ty.layout().unwrap().shape() }
21+
}
22+
23+
/// Return whether the type is sized.
24+
pub fn is_sized(&self) -> bool {
25+
self.layout.is_sized()
26+
}
27+
28+
/// Return whether the type is unsized and its tail is a foreign item.
29+
///
30+
/// This will also return `true` if the type is foreign.
31+
pub fn has_foreign_tail(&self) -> bool {
32+
self.unsized_tail()
33+
.map_or(false, |t| matches!(t.kind(), TyKind::RigidTy(RigidTy::Foreign(_))))
34+
}
35+
36+
/// Return whether the type is unsized and its tail is a trait object.
37+
pub fn has_trait_tail(&self) -> bool {
38+
self.unsized_tail().map_or(false, |t| t.kind().is_trait())
39+
}
40+
41+
/// Return whether the type is unsized and its tail is a slice.
42+
#[allow(dead_code)]
43+
pub fn has_slice_tail(&self) -> bool {
44+
self.unsized_tail().map_or(false, |tail| {
45+
let kind = tail.kind();
46+
kind.is_slice() | kind.is_str()
47+
})
48+
}
49+
50+
/// Return the unsized tail of the type if this is an unsized type.
51+
///
52+
/// For foreign types, return `None`.
53+
/// For unsized types, this should return either a slice, a string slice, a dynamic type,
54+
/// or a foreign type.
55+
/// For other types, this function will return `None`.
56+
pub fn unsized_tail(&self) -> Option<Ty> {
57+
if self.layout.is_unsized() {
58+
match self.ty.kind().rigid().unwrap() {
59+
RigidTy::Slice(..) | RigidTy::Dynamic(..) | RigidTy::Str => Some(self.ty),
60+
RigidTy::Adt(..) | RigidTy::Tuple(..) => {
61+
// Recurse the tail field type until we find the unsized tail.
62+
self.last_field_layout().unsized_tail()
63+
}
64+
RigidTy::Foreign(_) => Some(self.ty),
65+
_ => unreachable!("Expected unsized type but found `{}`", self.ty),
66+
}
67+
} else {
68+
None
69+
}
70+
}
71+
72+
/// Return the type of the elements of the slice or `str` at the unsized tail of this type.
73+
///
74+
/// For sized types and trait unsized type, this function will return `None`.
75+
pub fn unsized_tail_elem_ty(&self) -> Option<Ty> {
76+
self.unsized_tail().and_then(|tail| match tail.kind().rigid().unwrap() {
77+
RigidTy::Slice(elem_ty) => Some(*elem_ty),
78+
// String slices have the same layout as slices of u8.
79+
// https://doc.rust-lang.org/reference/type-layout.html#str-layout
80+
RigidTy::Str => Some(Ty::unsigned_ty(UintTy::U8)),
81+
_ => None,
82+
})
83+
}
84+
85+
/// Return the size of the sized portion of this type.
86+
///
87+
/// For a sized type, this function will return the size of the type.
88+
/// For an unsized type, this function will return the size of the sized portion including
89+
/// any padding bytes that lead to the unsized field.
90+
/// I.e.: the size of the type, excluding the trailing unsized portion.
91+
///
92+
/// For example, this function will return 2 as the sized portion of `*const (u8, [u16])`:
93+
pub fn size_of_head(&self) -> usize {
94+
if self.is_sized() {
95+
self.layout.size.bytes()
96+
} else {
97+
match self.ty.kind().rigid().unwrap() {
98+
RigidTy::Slice(_) | RigidTy::Str | RigidTy::Dynamic(..) | RigidTy::Foreign(..) => 0,
99+
RigidTy::Adt(..) | RigidTy::Tuple(..) => {
100+
let fields_sorted = self.layout.fields.fields_by_offset_order();
101+
let last = *fields_sorted.last().unwrap();
102+
let FieldsShape::Arbitrary { ref offsets } = self.layout.fields else {
103+
unreachable!()
104+
};
105+
106+
// We compute the size of the sized portion by taking the position of the
107+
// last element + the sized portion of that element.
108+
let unsized_offset_unadjusted = offsets[last].bytes();
109+
debug!(ty=?self.ty, ?unsized_offset_unadjusted, "size_of_sized_portion");
110+
unsized_offset_unadjusted + self.last_field_layout().size_of_head()
111+
}
112+
_ => {
113+
unreachable!("Expected sized type, but found: `{}`", self.ty)
114+
}
115+
}
116+
}
117+
}
118+
119+
/// Return the alignment of the fields that are sized from the head of the object.
120+
///
121+
/// For a sized type, this function will return the alignment of the type.
122+
///
123+
/// For an unsized type, this function will return the alignment of the sized portion.
124+
/// The alignment of the type will be the maximum of the alignment of the sized portion
125+
/// and the alignment of the unsized portion.
126+
///
127+
/// If there's no sized portion, this function will return the minimum alignment (i.e.: 1).
128+
pub fn align_of_head(&self) -> usize {
129+
if self.is_sized() {
130+
self.layout.abi_align.try_into().unwrap()
131+
} else {
132+
match self.ty.kind().rigid().unwrap() {
133+
RigidTy::Slice(_) | RigidTy::Str | RigidTy::Dynamic(..) | RigidTy::Foreign(..) => 1,
134+
RigidTy::Adt(..) | RigidTy::Tuple(..) => {
135+
// We have to recurse and get the maximum alignment of all sized portions.
136+
let field_layout = self.last_field_layout();
137+
field_layout.align_of_head().max(self.layout.abi_align.try_into().unwrap())
138+
}
139+
_ => {
140+
unreachable!("Expected sized type, but found: `{}`", self.ty);
141+
}
142+
}
143+
}
144+
}
145+
146+
/// Return the size of the type if it's known at compilation type.
147+
pub fn size_of(&self) -> Option<usize> {
148+
if self.is_sized() { Some(self.layout.size.bytes()) } else { None }
149+
}
150+
151+
/// Return the alignment of the type if it's know at compilation time.
152+
///
153+
/// The alignment is known at compilation type for sized types and types with slice tail.
154+
///
155+
/// Note: We assume u64 and usize are the same since Kani is only supported in 64bits machines.
156+
/// Add a configuration in case we ever decide to port this to a 32-bits machine.
157+
#[cfg(target_pointer_width = "64")]
158+
pub fn align_of(&self) -> Option<usize> {
159+
if self.is_sized() || self.has_slice_tail() {
160+
self.layout.abi_align.try_into().ok()
161+
} else {
162+
None
163+
}
164+
}
165+
166+
/// Return the layout of the last field of the type.
167+
///
168+
/// This function is used to get the layout of the last field of an unsized type.
169+
/// For example, if we have `*const (u8, [u16])`, the last field is `[u16]`.
170+
/// This function will return the layout of `[u16]`.
171+
///
172+
/// If the type is not a struct, an enum, or a tuple, with at least one field, this function
173+
/// will panic.
174+
fn last_field_layout(&self) -> LayoutOf {
175+
match self.ty.kind().rigid().unwrap() {
176+
RigidTy::Adt(adt_def, adt_args) => {
177+
let fields = adt_def.variants_iter().next().unwrap().fields();
178+
let fields_sorted = self.layout.fields.fields_by_offset_order();
179+
let last_field_idx = *fields_sorted.last().unwrap();
180+
LayoutOf::new(fields[last_field_idx].ty_with_args(adt_args))
181+
}
182+
RigidTy::Tuple(tys) => {
183+
// For tuples, the unsized field is currently the last declared.
184+
// To be on the safe side, we still get the sorted list by offset order.
185+
let fields_sorted = self.layout.fields.fields_by_offset_order();
186+
let last_field_idx = *fields_sorted.last().unwrap();
187+
let last_ty = tys[last_field_idx];
188+
LayoutOf::new(last_ty)
189+
}
190+
_ => {
191+
unreachable!("Expected struct, enum or tuple. Found: `{}`", self.ty);
192+
}
193+
}
194+
}
195+
}

kani-compiler/src/kani_middle/mod.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ use std::ops::ControlFlow;
2626

2727
use self::attributes::KaniAttributes;
2828

29+
pub mod abi;
2930
pub mod analysis;
3031
pub mod attributes;
3132
pub mod codegen_units;
Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
// Test codegen for a raw pointer to a struct whose last field is a slice
4+
5+
#![feature(layout_for_ptr)]
6+
#![feature(ptr_metadata)]
7+
8+
// https://github.com/model-checking/kani/issues/3615
9+
mod issue_3615 {
10+
use std::ptr;
11+
12+
#[derive(Clone, Copy, kani::Arbitrary)]
13+
struct Wrapper<T: ?Sized> {
14+
_size: usize,
15+
_value: T,
16+
}
17+
18+
#[kani::proof]
19+
pub fn from_raw_parts_for_slices() {
20+
let var: Wrapper<[u64; 4]> = kani::any();
21+
let fat_ptr: *const Wrapper<[u64]> = &var as *const _;
22+
let (thin_ptr, _) = fat_ptr.to_raw_parts();
23+
let new_size: usize = kani::any();
24+
let _new_ptr: *const Wrapper<[u64]> = ptr::from_raw_parts(thin_ptr, new_size);
25+
}
26+
27+
#[kani::proof]
28+
pub fn from_raw_parts_for_slices_nested() {
29+
let var: Wrapper<Wrapper<[u8; 4]>> = kani::any();
30+
let fat_ptr: *const Wrapper<Wrapper<[u8]>> = &var as *const _;
31+
let (thin_ptr, _) = fat_ptr.to_raw_parts();
32+
let new_size: usize = kani::any();
33+
let _new_ptr: *const Wrapper<Wrapper<[u8]>> = ptr::from_raw_parts(thin_ptr, new_size);
34+
}
35+
}
36+
37+
// https://github.com/model-checking/kani/issues/3638
38+
mod issue_3638 {
39+
use std::ptr::NonNull;
40+
41+
#[derive(kani::Arbitrary)]
42+
struct Wrapper<T: ?Sized>(usize, T);
43+
44+
#[cfg(kani)]
45+
#[kani::proof]
46+
fn slice_from_raw() {
47+
// Create a SampleSlice object from SampleStruct
48+
let original: Wrapper<[u8; 10]> = kani::any();
49+
let slice: &Wrapper<[u8]> = &original;
50+
51+
// Get the raw data pointer and metadata for the slice object
52+
let slice_ptr = NonNull::new(slice as *const _ as *mut ()).unwrap();
53+
let metadata = std::ptr::metadata(slice);
54+
55+
// Create NonNull<[u8]> from the data pointer and metadata
56+
let _: NonNull<Wrapper<[u8]>> = NonNull::from_raw_parts(slice_ptr, metadata);
57+
}
58+
}

0 commit comments

Comments
 (0)