Implement sizeof for Code for vtable generation (fix crash)

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,
         }
     }

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());
 

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)
+}

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)
+}

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)
+}

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)
+}

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)
+}

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)
+}

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);

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);

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,43 +65,37 @@ 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::<Sheep> as *mut ());
+        assert!(drop_from_vtable(vtable_ptr) == drop_in_place::<Sheep> as *mut ());
 
         // Size and align as usizes
         assert!(size_from_vtable(vtable_ptr) == size_of::<i32>());
         assert!(align_from_vtable(vtable_ptr) == size_of::<i32>());
     }
     // 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::<Cow> as *mut ());
+        assert!(drop_from_vtable(vtable_ptr) == drop_in_place::<Cow> as *mut ());
 
         // Size and align as usizes
         assert!(size_from_vtable(vtable_ptr) == size_of::<i8>());

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::<Sheep> as *mut (),
+            drop_from_vtable(vtable_ptr) != drop_in_place::<Sheep> 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::<Cow> as *mut (),
+            drop_from_vtable(vtable_ptr) != drop_in_place::<Cow> as *mut (),
             "Wrong drop",
         );