From e1cc5f560387fe1f7ca0171b00d850a909035132 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Fri, 25 Jun 2021 09:32:03 -0400 Subject: [PATCH] Implement sizeof and tests --- .../src/gotoc/cbmc/goto_program/typ.rs | 24 ++++++++++----- .../rustc_codegen_llvm/src/gotoc/rvalue.rs | 1 + src/test/cbmc/DynTrait/dyn_fn_param.rs | 26 ++++++++++++++++ .../cbmc/DynTrait/dyn_fn_param_closure.rs | 19 ++++++++++++ .../DynTrait/dyn_fn_param_closure_capture.rs | 22 ++++++++++++++ .../dyn_fn_param_closure_capture_fail.rs | 23 ++++++++++++++ .../DynTrait/dyn_fn_param_closure_fail.rs | 20 +++++++++++++ .../cbmc/DynTrait/dyn_fn_param_fail_fixme.rs | 30 +++++++++++++++++++ src/test/cbmc/DynTrait/nested_boxes.rs | 9 ++---- src/test/cbmc/DynTrait/nested_boxes_fail.rs | 9 ++---- .../cbmc/DynTrait/vtable_size_align_drop.rs | 25 ++++++---------- .../DynTrait/vtable_size_align_drop_fail.rs | 23 +++++--------- src/test/cbmc/FatPointers/boxmuttrait.rs | 9 ++---- src/test/cbmc/Helpers/vtable_utils_ignore.rs | 22 +++++++++++++- 14 files changed, 203 insertions(+), 59 deletions(-) create mode 100644 src/test/cbmc/DynTrait/dyn_fn_param.rs create mode 100644 src/test/cbmc/DynTrait/dyn_fn_param_closure.rs create mode 100644 src/test/cbmc/DynTrait/dyn_fn_param_closure_capture.rs create mode 100644 src/test/cbmc/DynTrait/dyn_fn_param_closure_capture_fail.rs create mode 100644 src/test/cbmc/DynTrait/dyn_fn_param_closure_fail.rs create mode 100644 src/test/cbmc/DynTrait/dyn_fn_param_fail_fixme.rs diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs index 0340ff41a5e0..08d1cf1da7fa 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs @@ -252,18 +252,26 @@ impl Type { // base type. match self { Array { typ, size } => typ.sizeof_in_bits(st) * size, - Bool => unreachable!("Doesn't have a sizeof"), + Bool => unreachable!("Bool doesn't have a sizeof"), CBitField { .. } => todo!("implement sizeof for bitfields"), CInteger(t) => t.sizeof_in_bits(st), - Code { .. } => unreachable!("Doesn't have a sizeof"), - Constructor => unreachable!("Doesn't have a sizeof"), + + // We generate Code to put a reference to a Rust FnDef into a vtable; the definition + // itself has no size (data is empty, and the vtable itself contains fn pointers for + // Fn::call, etc). + // + // See Rust's implementation of layout_of, where FnDef is treated as a univariant + // type with no fields (and thus a size of 0 in the layout): + // FnDef case in layout_raw_uncached, compiler/rustc_middle/src/ty/layout.rs + Code { .. } => 0, + Constructor => unreachable!("Constructor doesn't have a sizeof"), Double => st.machine_model().double_width(), Empty => 0, FlexibleArray { .. } => 0, Float => st.machine_model().float_width(), - IncompleteStruct { .. } => unreachable!("Doesn't have a sizeof"), - IncompleteUnion { .. } => unreachable!("Doesn't have a sizeof"), - InfiniteArray { .. } => unreachable!("Doesn't have a sizeof"), + IncompleteStruct { .. } => unreachable!("IncompleteStruct doesn't have a sizeof"), + IncompleteUnion { .. } => unreachable!("IncompleteUnion doesn't have a sizeof"), + InfiniteArray { .. } => unreachable!("InfiniteArray doesn't have a sizeof"), Pointer { .. } => st.machine_model().pointer_width(), Signedbv { width } => *width, Struct { components, .. } => { @@ -275,7 +283,9 @@ impl Type { } UnionTag(tag) => st.lookup(tag).unwrap().typ.sizeof_in_bits(st), Unsignedbv { width } => *width, - VariadicCode { .. } => unreachable!("Doesn't have a sizeof"), + // It's possible this should also have size 0, like Code, but we have not been + // able to generate a unit test, so leaving it unreachable for now. + VariadicCode { .. } => unreachable!("VariadicCode doesn't have a sizeof"), Vector { typ, size } => typ.sizeof_in_bits(st) * size, } } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index ad94c432006f..79305cafd76a 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -809,6 +809,7 @@ 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 = self.layout_of(operand_type); + assert!(!vtable_layout.is_unsized(), "Can't create a vtable for an unsized 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()); diff --git a/src/test/cbmc/DynTrait/dyn_fn_param.rs b/src/test/cbmc/DynTrait/dyn_fn_param.rs new file mode 100644 index 000000000000..816143f6cbd0 --- /dev/null +++ b/src/test/cbmc/DynTrait/dyn_fn_param.rs @@ -0,0 +1,26 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that we can pass a dyn function pointer to a stand alone +// function definition + +#![feature(raw)] +#![allow(deprecated)] + +include!("../Helpers/vtable_utils_ignore.rs"); + +fn takes_dyn_fun(fun: &dyn Fn() -> u32) { + let x = fun(); + assert!(x == 5); + + /* The function dynamic object has no associated data */ + assert!(size_from_vtable(vtable!(fun)) == 0); +} + +pub fn unit_to_u32() -> u32 { + 5 as u32 +} + +fn main() { + takes_dyn_fun(&unit_to_u32) +} diff --git a/src/test/cbmc/DynTrait/dyn_fn_param_closure.rs b/src/test/cbmc/DynTrait/dyn_fn_param_closure.rs new file mode 100644 index 000000000000..b72964207c07 --- /dev/null +++ b/src/test/cbmc/DynTrait/dyn_fn_param_closure.rs @@ -0,0 +1,19 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that we can pass a dyn function pointer to a simple closure +#![feature(raw)] +#![allow(deprecated)] + +include!("../Helpers/vtable_utils_ignore.rs"); + +fn takes_dyn_fun(fun: &dyn Fn() -> i32) { + let x = fun(); + assert!(x == 5); + /* The closure does not capture anything and thus has zero size */ + assert!(size_from_vtable(vtable!(fun)) == 0); +} +fn main() { + let closure = || 5; + takes_dyn_fun(&closure) +} diff --git a/src/test/cbmc/DynTrait/dyn_fn_param_closure_capture.rs b/src/test/cbmc/DynTrait/dyn_fn_param_closure_capture.rs new file mode 100644 index 000000000000..4aeeff131164 --- /dev/null +++ b/src/test/cbmc/DynTrait/dyn_fn_param_closure_capture.rs @@ -0,0 +1,22 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that we can pass a dyn function pointer to a closure that captures +// some data +#![feature(raw)] +#![allow(deprecated)] + +include!("../Helpers/vtable_utils_ignore.rs"); + +fn takes_dyn_fun(fun: &dyn Fn() -> i32) { + let x = fun(); + assert!(x == 5); + /* The closure captures `a` and thus has nonzero size */ + assert!(size_from_vtable(vtable!(fun)) == 8); +} + +fn main() { + let a = vec![3]; + let closure = || a[0] + 2; + takes_dyn_fun(&closure) +} diff --git a/src/test/cbmc/DynTrait/dyn_fn_param_closure_capture_fail.rs b/src/test/cbmc/DynTrait/dyn_fn_param_closure_capture_fail.rs new file mode 100644 index 000000000000..ddfaf9358df1 --- /dev/null +++ b/src/test/cbmc/DynTrait/dyn_fn_param_closure_capture_fail.rs @@ -0,0 +1,23 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that we can pass a dyn function pointer to a closure that captures +// some data +#![feature(raw)] +#![allow(deprecated)] + +include!("../Helpers/vtable_utils_ignore.rs"); +include!("../../rmc-prelude.rs"); + +fn takes_dyn_fun(fun: &dyn Fn() -> i32) { + let x = fun(); + __VERIFIER_expect_fail(x != 5, "Wrong return"); + /* The closure captures `a` and thus is sized */ + __VERIFIER_expect_fail(size_from_vtable(vtable!(fun)) == 8, "Wrong size"); +} + +fn main() { + let a = vec![3]; + let closure = || a[0] + 2; + takes_dyn_fun(&closure) +} diff --git a/src/test/cbmc/DynTrait/dyn_fn_param_closure_fail.rs b/src/test/cbmc/DynTrait/dyn_fn_param_closure_fail.rs new file mode 100644 index 000000000000..50ece1eb2640 --- /dev/null +++ b/src/test/cbmc/DynTrait/dyn_fn_param_closure_fail.rs @@ -0,0 +1,20 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that we can pass a dyn function pointer to a simple closure +#![feature(raw)] +#![allow(deprecated)] + +include!("../Helpers/vtable_utils_ignore.rs"); +include!("../../rmc-prelude.rs"); + +fn takes_dyn_fun(fun: &dyn Fn() -> i32) { + let x = fun(); + __VERIFIER_expect_fail(x != 5, "Wrong return"); + /* The closure does not capture anything and thus has zero size */ + __VERIFIER_expect_fail(size_from_vtable(vtable!(fun)) != 0, "Wrong size"); +} +fn main() { + let closure = || 5; + takes_dyn_fun(&closure) +} diff --git a/src/test/cbmc/DynTrait/dyn_fn_param_fail_fixme.rs b/src/test/cbmc/DynTrait/dyn_fn_param_fail_fixme.rs new file mode 100644 index 000000000000..72008a5a8d16 --- /dev/null +++ b/src/test/cbmc/DynTrait/dyn_fn_param_fail_fixme.rs @@ -0,0 +1,30 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that we can pass a dyn function pointer to a stand alone +// function definition. Inverted negative test. + +// FIXME https://github.com/model-checking/rmc/issues/240 + +#![feature(raw)] +#![allow(deprecated)] + +include!("../Helpers/vtable_utils_ignore.rs"); +include!("../../rmc-prelude.rs"); + +fn takes_dyn_fun(fun: &dyn Fn() -> u32) { + let x = fun(); + __VERIFIER_expect_fail(x != 5, "Wrong return"); + + /* The function dynamic object has no associated data */ + __VERIFIER_expect_fail(size_from_vtable(vtable!(fun)) != 0, "Wrong size"); +} + +pub fn unit_to_u32() -> u32 { + assert!(false); + 5 as u32 +} + +fn main() { + takes_dyn_fun(&unit_to_u32) +} diff --git a/src/test/cbmc/DynTrait/nested_boxes.rs b/src/test/cbmc/DynTrait/nested_boxes.rs index 90ceb903bc98..4f3ecd259463 100644 --- a/src/test/cbmc/DynTrait/nested_boxes.rs +++ b/src/test/cbmc/DynTrait/nested_boxes.rs @@ -9,8 +9,6 @@ #![allow(deprecated)] use std::intrinsics::size_of; -use std::mem::transmute; -use std::raw::TraitObject; include!("../Helpers/vtable_utils_ignore.rs"); @@ -26,16 +24,15 @@ fn main() { // Do some unsafe magic to check that we generate the right three vtables unsafe { - let trait_object3: TraitObject = transmute(dyn_trait3); - // Outermost trait object // The size is 16, because the data is another fat pointer - let vtable3: *mut usize = trait_object3.vtable as *mut usize; + let dyn_3 = &*dyn_trait3 as &dyn Send; + let vtable3: *mut usize = vtable!(dyn_3); assert!(size_from_vtable(vtable3) == 16); assert!(align_from_vtable(vtable3) == 8); // Inspect the data pointer from dyn_trait3 - let data_ptr3 = trait_object3.data as *mut usize; + let data_ptr3 = data!(dyn_3) as *mut usize; // The second half of this fat pointer is another vtable, for dyn_trait2 let vtable2 = *(data_ptr3.offset(1) as *mut *mut usize); diff --git a/src/test/cbmc/DynTrait/nested_boxes_fail.rs b/src/test/cbmc/DynTrait/nested_boxes_fail.rs index 0c1095b4f1c6..ee0182717df6 100644 --- a/src/test/cbmc/DynTrait/nested_boxes_fail.rs +++ b/src/test/cbmc/DynTrait/nested_boxes_fail.rs @@ -9,10 +9,7 @@ #![feature(raw)] #![allow(deprecated)] -use std::fs::File; use std::intrinsics::size_of; -use std::mem::transmute; -use std::raw::TraitObject; include!("../Helpers/vtable_utils_ignore.rs"); @@ -28,16 +25,14 @@ fn main() { // Do some unsafe magic to check that we generate the right three vtables unsafe { - let trait_object3: TraitObject = transmute(dyn_trait3); - // Outermost trait object // The size is 16, because the data is another fat pointer - let vtable3: *mut usize = trait_object3.vtable as *mut usize; + let vtable3: *mut usize = vtable!(dyn_trait3); assert!(size_from_vtable(vtable3) != 16); assert!(align_from_vtable(vtable3) != 8); // Inspect the data pointer from dyn_trait3 - let data_ptr3 = trait_object3.data as *mut usize; + let data_ptr3 = data!(dyn_trait3) as *mut usize; // The second half of this fat pointer is another vtable, for dyn_trait2 let vtable2 = *(data_ptr3.offset(1) as *mut *mut usize); diff --git a/src/test/cbmc/DynTrait/vtable_size_align_drop.rs b/src/test/cbmc/DynTrait/vtable_size_align_drop.rs index 1db127c57708..ce7c0c0975e8 100644 --- a/src/test/cbmc/DynTrait/vtable_size_align_drop.rs +++ b/src/test/cbmc/DynTrait/vtable_size_align_drop.rs @@ -11,11 +11,10 @@ #![allow(deprecated)] use std::intrinsics::size_of; -use std::mem::transmute; use std::ptr::drop_in_place; -use std::raw::TraitObject; include!("../Helpers/vtable_utils_ignore.rs"); +include!("../../rmc-prelude.rs"); // Different sized data fields on each struct struct Sheep { @@ -66,21 +65,18 @@ fn main() { // Check layout/values for Sheep unsafe { - let animal_sheep = random_animal(1); - - // Unsafe cast to dynamic trait object fat pointer - let trait_object: TraitObject = transmute(animal_sheep); + let animal_sheep = &*random_animal(1); // Check that the struct's data is what we expect - let data_ptr = trait_object.data; + let data_ptr = data!(animal_sheep); // Note: i32 ptr cast assert!(*(data_ptr as *mut i32) == 7); // From Sheep - let vtable_ptr = trait_object.vtable as *mut usize; + let vtable_ptr = vtable!(animal_sheep); // Drop pointer - assert!(drop_from_vtrable(vtable_ptr) == drop_in_place:: as *mut ()); + assert!(drop_from_vtable(vtable_ptr) == drop_in_place:: as *mut ()); // Size and align as usizes assert!(size_from_vtable(vtable_ptr) == size_of::()); @@ -88,21 +84,18 @@ fn main() { } // Check layout/values for Cow unsafe { - let animal_cow = random_animal(6); - - // Unsafe cast to dynamic trait object fat pointer - let trait_object: TraitObject = transmute(animal_cow); + let animal_cow = &*random_animal(6); // Check that the struct's data is what we expect - let data_ptr = trait_object.data; + let data_ptr = data!(animal_cow); // Note: i8 ptr cast assert!(*(data_ptr as *mut i8) == 9); // From Cow - let vtable_ptr = trait_object.vtable as *mut usize; + let vtable_ptr = vtable!(animal_cow); // Drop pointer - assert!(drop_from_vtrable(vtable_ptr) == drop_in_place:: as *mut ()); + assert!(drop_from_vtable(vtable_ptr) == drop_in_place:: as *mut ()); // Size and align as usizes assert!(size_from_vtable(vtable_ptr) == size_of::()); diff --git a/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs b/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs index 8c094d428845..7af61f34b3a0 100644 --- a/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs +++ b/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs @@ -13,9 +13,6 @@ #![allow(deprecated)] use std::intrinsics::size_of; -use std::mem::transmute; -use std::ptr::drop_in_place; -use std::raw::TraitObject; include!("../Helpers/vtable_utils_ignore.rs"); include!("../../rmc-prelude.rs"); @@ -73,20 +70,17 @@ fn main() { unsafe { let animal_sheep = random_animal(1); - // Unsafe cast to dynamic trait object fat pointer - let trait_object: TraitObject = transmute(animal_sheep); - // Check that the struct's data is what we expect - let data_ptr = trait_object.data; + let data_ptr = data!(animal_sheep); // Note: i32 ptr cast __VERIFIER_expect_fail(*(data_ptr as *mut i32) != 7, "Wrong data"); // From Sheep - let vtable_ptr = trait_object.vtable as *mut usize; + let vtable_ptr = vtable!(animal_sheep); // Drop pointer __VERIFIER_expect_fail( - drop_from_vtrable(vtable_ptr) != drop_in_place:: as *mut (), + drop_from_vtable(vtable_ptr) != drop_in_place:: as *mut (), "Wrong drop", ); @@ -96,22 +90,19 @@ fn main() { } // Check layout/values for Cow unsafe { - let animal_cow = random_animal(6); - - // Unsafe cast to dynamic trait object fat pointer - let trait_object: TraitObject = transmute(animal_cow); + let animal_sheep = random_animal(1); // Check that the struct's data is what we expect - let data_ptr = trait_object.data; + let data_ptr = data!(animal_sheep); // Note: i8 ptr cast __VERIFIER_expect_fail(*(data_ptr as *mut i8) != 9, "Wrong data"); // From Cow - let vtable_ptr = trait_object.vtable as *mut usize; + let vtable_ptr = vtable!(animal_sheep); // Drop pointer __VERIFIER_expect_fail( - drop_from_vtrable(vtable_ptr) != drop_in_place:: as *mut (), + drop_from_vtable(vtable_ptr) != drop_in_place:: as *mut (), "Wrong drop", ); diff --git a/src/test/cbmc/FatPointers/boxmuttrait.rs b/src/test/cbmc/FatPointers/boxmuttrait.rs index 500b158ed8e8..d31e894dfc91 100644 --- a/src/test/cbmc/FatPointers/boxmuttrait.rs +++ b/src/test/cbmc/FatPointers/boxmuttrait.rs @@ -5,8 +5,6 @@ #![allow(deprecated)] use std::io::{sink, Write}; -use std::mem::transmute; -use std::raw::TraitObject; include!("../Helpers/vtable_utils_ignore.rs"); @@ -21,17 +19,16 @@ fn main() { // Do some unsafe magic to check that we generate the right two vtables unsafe { - let dest_trait_object: TraitObject = transmute(&*dest); - // The vtable has [&drop, size, align, ....] - let dest_vtable_ptr = dest_trait_object.vtable as *mut usize; + let dest_ptr = &*dest; + let dest_vtable_ptr = vtable!(dest_ptr); // The size is 16, because the data is another fat pointer assert!(size_from_vtable(dest_vtable_ptr) == 16); assert!(align_from_vtable(dest_vtable_ptr) == 8); // Inspect the data pointer from dest - let dest_data_ptr = dest_trait_object.data as *mut usize; + let dest_data_ptr = data!(dest_ptr) as *mut usize; // // The second half of this fat pointer is another vtable, for log let second_vtable_ptr = dest_data_ptr.offset(1) as *mut *mut usize; diff --git a/src/test/cbmc/Helpers/vtable_utils_ignore.rs b/src/test/cbmc/Helpers/vtable_utils_ignore.rs index 8c38d62d6ee7..2f600b7dc971 100644 --- a/src/test/cbmc/Helpers/vtable_utils_ignore.rs +++ b/src/test/cbmc/Helpers/vtable_utils_ignore.rs @@ -3,7 +3,27 @@ // Because each regression test does not share a crate, we just use // an import! to share this code across test directories. -fn drop_from_vtrable(vtable_ptr: *mut usize) -> *mut () { + +// Macro rules because we can't cast between incompatible dyn trait fat pointer types +macro_rules! vtable { + ($f:ident) => {{ + unsafe { + let trait_object: std::raw::TraitObject = std::mem::transmute($f); + trait_object.vtable as *mut usize + } + }}; +} + +macro_rules! data { + ($f:ident) => {{ + unsafe { + let trait_object: std::raw::TraitObject = std::mem::transmute($f); + trait_object.data as *mut () + } + }}; +} + +fn drop_from_vtable(vtable_ptr: *mut usize) -> *mut () { // 1st pointer-sized position unsafe { *vtable_ptr as *mut () } }