Skip to content

Commit b5c6524

Browse files
markrtuttleMark R. Tuttle
authored andcommitted
Allow cast of any pointer to cast to a trait pointer (rust-lang#98)
* Allow cast of any pointer to cast to a trait pointer Also: * Add predicates `use_*_pointer(mir_type)` to use mir pointer metadata to identify the correct type of pointer to a mir type. * Use predicates `use_*_pointer(mir_type)` in fat pointer construction Resolves model-checking/kani#83 Co-authored-by: Mark R. Tuttle <[email protected]>
1 parent c967c07 commit b5c6524

File tree

3 files changed

+28
-19
lines changed

3 files changed

+28
-19
lines changed

compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs

Lines changed: 11 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -750,9 +750,9 @@ impl<'tcx> GotocCtx<'tcx> {
750750
fn codegen_vtable_size_and_align(&self, operand_type: Ty<'tcx>) -> (Expr, Expr) {
751751
debug!("vtable_size_and_align {:?}", operand_type.kind());
752752
let vtable_layout = match operand_type.kind() {
753-
ty::Ref(_region, inner_type, _mutability) => self.layout_of(inner_type), //DSN was operand type
754-
ty::Adt(..) => self.layout_of(operand_type),
755-
_ => unreachable!("We got a vtable type that wasn't a ref or adt."),
753+
ty::Ref(_, inner_type, ..) => self.layout_of(inner_type),
754+
ty::RawPtr(ty::TypeAndMut { ty: inner_type, .. }) => self.layout_of(inner_type),
755+
_ => self.layout_of(operand_type),
756756
};
757757
let vt_size = Expr::int_constant(vtable_layout.size.bytes(), Type::size_t());
758758
let vt_align = Expr::int_constant(vtable_layout.align.abi.bytes(), Type::size_t());
@@ -882,30 +882,29 @@ impl<'tcx> GotocCtx<'tcx> {
882882
let src_pointee_type = pointee_type(src_mir_type).unwrap();
883883
let dst_pointee_type = pointee_type(dst_mir_type).unwrap();
884884

885-
let dst_pointee_metadata_type = dst_pointee_type.ptr_metadata_ty(self.tcx);
886-
let unit = self.tcx.types.unit;
887-
let usize = self.tcx.types.usize;
888-
889-
if dst_pointee_metadata_type == unit {
885+
if self.use_thin_pointer(dst_pointee_type) {
890886
assert_eq!(src_pointee_type, dst_pointee_type);
891887
None
892-
} else if dst_pointee_metadata_type == usize {
888+
} else if self.use_slice_fat_pointer(dst_pointee_type) {
893889
self.cast_sized_pointer_to_slice_fat_pointer(
894890
src_goto_expr,
895891
src_mir_type,
896892
dst_mir_type,
897893
src_pointee_type,
898894
dst_pointee_type,
899895
)
900-
} else {
901-
// dst_pointee_metadata_type == std::ptr::DynMetadata<dyn trait> (a vtable is required)
896+
} else if self.use_vtable_fat_pointer(dst_pointee_type) {
902897
self.cast_sized_pointer_to_trait_fat_pointer(
903898
src_goto_expr,
904899
src_mir_type,
905900
dst_mir_type,
906901
src_pointee_type,
907902
dst_pointee_type,
908903
)
904+
} else {
905+
unreachable!(
906+
"A pointer is either a thin pointer, slice fat pointer, or vtable fat pointer."
907+
);
909908
}
910909
}
911910

@@ -1027,7 +1026,7 @@ impl<'tcx> GotocCtx<'tcx> {
10271026
dst_mir_type: Ty<'tcx>,
10281027
) -> Option<(Ty<'tcx>, Ty<'tcx>)> {
10291028
match (src_mir_type.kind(), dst_mir_type.kind()) {
1030-
(ty::Adt(..), ty::Dynamic(..)) => Some((src_mir_type.clone(), dst_mir_type.clone())),
1029+
(_, ty::Dynamic(..)) => Some((src_mir_type.clone(), dst_mir_type.clone())),
10311030
(ty::Adt(..), ty::Adt(..)) => {
10321031
let src_fields = self.mir_struct_field_types(src_mir_type);
10331032
let dst_fields = self.mir_struct_field_types(dst_mir_type);

compiler/rustc_codegen_llvm/src/gotoc/typ.rs

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1015,3 +1015,19 @@ pub fn pointee_type(pointer_type: Ty<'tcx>) -> Option<Ty<'tcx>> {
10151015
_ => None,
10161016
}
10171017
}
1018+
1019+
impl<'tcx> GotocCtx<'tcx> {
1020+
/// A pointer to the mir type should be a thin pointer.
1021+
pub fn use_thin_pointer(&self, mir_type: Ty<'tcx>) -> bool {
1022+
return mir_type.ptr_metadata_ty(self.tcx) == self.tcx.types.unit;
1023+
}
1024+
/// A pointer to the mir type should be a slice fat pointer.
1025+
pub fn use_slice_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool {
1026+
return mir_type.ptr_metadata_ty(self.tcx) == self.tcx.types.usize;
1027+
}
1028+
/// A pointer to the mir type should be a vtable fat pointer.
1029+
pub fn use_vtable_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool {
1030+
let metadata = mir_type.ptr_metadata_ty(self.tcx);
1031+
return metadata != self.tcx.types.unit && metadata != self.tcx.types.usize;
1032+
}
1033+
}

rust-tests/cbmc-reg/Closure/main.rs

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -2,17 +2,11 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
//! test that we implement closures correctly
44
5-
// Commenting out the test that induces the issue described in
6-
// https://github.com/model-checking/rmc/issues/83
7-
// until this issue is resolved.
8-
9-
/*
105
fn closure_with_empty_args() {
116
let bytes = vec![0];
127
let b = bytes.get(0).ok_or_else(|| ()).unwrap();
138
assert!(*b == 0);
149
}
15-
*/
1610

1711
fn closure_with_1_arg() {
1812
let b = Some(3);
@@ -45,7 +39,7 @@ fn test_env() {
4539
}
4640

4741
fn main() {
48-
// closure_with_empty_args();
42+
closure_with_empty_args();
4943
closure_with_1_arg();
5044
test_three_args();
5145
test_unit_args();

0 commit comments

Comments
 (0)