Skip to content
Merged
Show file tree
Hide file tree
Changes from all 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
23 changes: 11 additions & 12 deletions compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -750,9 +750,9 @@ impl<'tcx> GotocCtx<'tcx> {
fn codegen_vtable_size_and_align(&self, operand_type: Ty<'tcx>) -> (Expr, Expr) {
debug!("vtable_size_and_align {:?}", operand_type.kind());
let vtable_layout = match operand_type.kind() {
ty::Ref(_region, inner_type, _mutability) => self.layout_of(inner_type), //DSN was operand type
ty::Adt(..) => self.layout_of(operand_type),
_ => unreachable!("We got a vtable type that wasn't a ref or adt."),
ty::Ref(_, inner_type, ..) => self.layout_of(inner_type),
ty::RawPtr(ty::TypeAndMut { ty: inner_type, .. }) => self.layout_of(inner_type),
_ => self.layout_of(operand_type),
};
let vt_size = Expr::int_constant(vtable_layout.size.bytes(), Type::size_t());
let vt_align = Expr::int_constant(vtable_layout.align.abi.bytes(), Type::size_t());
Expand Down Expand Up @@ -882,30 +882,29 @@ impl<'tcx> GotocCtx<'tcx> {
let src_pointee_type = pointee_type(src_mir_type).unwrap();
let dst_pointee_type = pointee_type(dst_mir_type).unwrap();

let dst_pointee_metadata_type = dst_pointee_type.ptr_metadata_ty(self.tcx);
let unit = self.tcx.types.unit;
let usize = self.tcx.types.usize;

if dst_pointee_metadata_type == unit {
if self.use_thin_pointer(dst_pointee_type) {
assert_eq!(src_pointee_type, dst_pointee_type);
None
} else if dst_pointee_metadata_type == usize {
} else if self.use_slice_fat_pointer(dst_pointee_type) {
self.cast_sized_pointer_to_slice_fat_pointer(
src_goto_expr,
src_mir_type,
dst_mir_type,
src_pointee_type,
dst_pointee_type,
)
} else {
// dst_pointee_metadata_type == std::ptr::DynMetadata<dyn trait> (a vtable is required)
} else if self.use_vtable_fat_pointer(dst_pointee_type) {
self.cast_sized_pointer_to_trait_fat_pointer(
src_goto_expr,
src_mir_type,
dst_mir_type,
src_pointee_type,
dst_pointee_type,
)
} else {
unreachable!(
"A pointer is either a thin pointer, slice fat pointer, or vtable fat pointer."
);
}
}

Expand Down Expand Up @@ -1027,7 +1026,7 @@ impl<'tcx> GotocCtx<'tcx> {
dst_mir_type: Ty<'tcx>,
) -> Option<(Ty<'tcx>, Ty<'tcx>)> {
match (src_mir_type.kind(), dst_mir_type.kind()) {
(ty::Adt(..), ty::Dynamic(..)) => Some((src_mir_type.clone(), dst_mir_type.clone())),
(_, ty::Dynamic(..)) => Some((src_mir_type.clone(), dst_mir_type.clone())),
(ty::Adt(..), ty::Adt(..)) => {
let src_fields = self.mir_struct_field_types(src_mir_type);
let dst_fields = self.mir_struct_field_types(dst_mir_type);
Expand Down
16 changes: 16 additions & 0 deletions compiler/rustc_codegen_llvm/src/gotoc/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1015,3 +1015,19 @@ pub fn pointee_type(pointer_type: Ty<'tcx>) -> Option<Ty<'tcx>> {
_ => None,
}
}

impl<'tcx> GotocCtx<'tcx> {
/// A pointer to the mir type should be a thin pointer.
pub fn use_thin_pointer(&self, mir_type: Ty<'tcx>) -> bool {
return mir_type.ptr_metadata_ty(self.tcx) == self.tcx.types.unit;
}
/// A pointer to the mir type should be a slice fat pointer.
pub fn use_slice_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool {
return mir_type.ptr_metadata_ty(self.tcx) == self.tcx.types.usize;
}
/// A pointer to the mir type should be a vtable fat pointer.
pub fn use_vtable_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool {
let metadata = mir_type.ptr_metadata_ty(self.tcx);
return metadata != self.tcx.types.unit && metadata != self.tcx.types.usize;
}
}
8 changes: 1 addition & 7 deletions rust-tests/cbmc-reg/Closure/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,17 +2,11 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! test that we implement closures correctly

// Commenting out the test that induces the issue described in
// https://github.com/model-checking/rmc/issues/83
// until this issue is resolved.

/*
fn closure_with_empty_args() {
let bytes = vec![0];
let b = bytes.get(0).ok_or_else(|| ()).unwrap();
assert!(*b == 0);
}
*/

fn closure_with_1_arg() {
let b = Some(3);
Expand Down Expand Up @@ -45,7 +39,7 @@ fn test_env() {
}

fn main() {
// closure_with_empty_args();
closure_with_empty_args();
closure_with_1_arg();
test_three_args();
test_unit_args();
Expand Down