Remove restriction to double fat pointer projection (rust-lang#1065)

We were restricting projections to only go through a max of one fat
pointer dereference. This is not always the case, however, each
projection should only care about the outer most fat pointer.

Added tests to ensure this works as expected.

It looks like size_of_val is returning the wrong values for the
projection of traits. I'm adding fixme test cases for those here and
I'll create a new issue for them.

Author: celinval

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

@@ -318,19 +318,16 @@ impl<'tcx> GotocCtx<'tcx> {
 
                 let inner_mir_typ_and_mut = base_type.builtin_deref(true).unwrap();
                 let fat_ptr_mir_typ = if self.is_box_of_unsized(base_type) {
-                    assert!(before.fat_ptr_mir_typ.is_none());
                     // If we have a box, its fat pointer typ is a pointer to the boxes inner type.
                     Some(self.tcx.mk_ptr(inner_mir_typ_and_mut))
                 } else if self.is_ref_of_unsized(base_type) {
-                    assert!(before.fat_ptr_mir_typ.is_none());
                     Some(before.mir_typ_or_variant.expect_type())
                 } else {
                     before.fat_ptr_mir_typ
                 };
 
                 let fat_ptr_goto_expr =
                     if self.is_box_of_unsized(base_type) || self.is_ref_of_unsized(base_type) {
-                        assert!(before.fat_ptr_goto_expr.is_none());
                         Some(inner_goto_expr.clone())
                     } else {
                         before.fat_ptr_goto_expr

tests/kani/Intrinsics/SizeOfVal/fixme_size_of_fat_ptr.rs

@@ -0,0 +1,52 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --unwind 3
+
+//! This test case checks the behavior of size_of_val for traits.
+use std::mem::size_of_val;
+
+trait T {}
+
+struct A {}
+
+impl T for A {}
+
+#[cfg_attr(kani, kani::proof)]
+fn check_size_simple() {
+    let a = A {};
+    let t: &dyn T = &a;
+    assert_eq!(size_of_val(t), 0);
+    assert_eq!(size_of_val(&t), 16);
+}
+
+trait Wrapper<T: ?Sized> {
+    fn inner(&self) -> &T;
+}
+
+struct Concrete<'a, T: ?Sized> {
+    inner: &'a T,
+}
+
+impl<T: ?Sized> Wrapper<T> for Concrete<'_, T> {
+    fn inner(&self) -> &T {
+        self.inner
+    }
+}
+
+#[cfg_attr(kani, kani::proof)]
+fn check_size_inner() {
+    let val = 10u8;
+    let conc_wrapper: Concrete<u8> = Concrete { inner: &val };
+    let trait_wrapper = &conc_wrapper as &dyn Wrapper<u8>;
+
+    assert_eq!(size_of_val(conc_wrapper.inner()), 1); // This is the size of val.
+    assert_eq!(size_of_val(&conc_wrapper), 8); // This is the size of Concrete.
+    assert_eq!(size_of_val(trait_wrapper), 8); // This is also the size of Concrete.
+    assert_eq!(size_of_val(&trait_wrapper), 16); // This is the size of the fat pointer.
+}
+
+// This can be run with rustc for comparison.
+fn main() {
+    check_size_simple();
+    check_size_inner();
+}

tests/kani/Projection/fixme_dyn_dyn_projection.rs

@@ -0,0 +1,49 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --unwind 3
+
+//! This test case checks the usage of dyn Trait<dyn Trait>.
+use std::mem::size_of_val;
+
+trait Wrapper<T: ?Sized> {
+    fn inner(&self) -> &T;
+}
+
+struct Concrete<'a, T: ?Sized> {
+    inner: &'a T,
+}
+
+impl<T: ?Sized> Wrapper<T> for Concrete<'_, T> {
+    fn inner(&self) -> &T {
+        self.inner
+    }
+}
+
+#[cfg_attr(kani, kani::proof)]
+fn check_val() {
+    let val = 20;
+    let inner: Concrete<u8> = Concrete { inner: &val };
+    let trait_inner: &dyn Wrapper<u8> = &inner;
+    let original: Concrete<dyn Wrapper<u8>> = Concrete { inner: trait_inner };
+    let wrapper = &original as &dyn Wrapper<dyn Wrapper<u8>>;
+    assert_eq!(*wrapper.inner().inner(), val);
+}
+
+#[cfg_attr(kani, kani::proof)]
+fn check_size() {
+    let val = 10u8;
+    let inner: Concrete<u8> = Concrete { inner: &val };
+    let trait_inner: &dyn Wrapper<u8> = &inner;
+    let original: Concrete<dyn Wrapper<u8>> = Concrete { inner: trait_inner };
+    let wrapper = &original as &dyn Wrapper<dyn Wrapper<u8>>;
+
+    assert_eq!(size_of_val(wrapper), 16);
+    assert_eq!(size_of_val(&wrapper.inner()), 16);
+    assert_eq!(size_of_val(wrapper.inner()), 8);
+}
+
+// For easy comparison, this allow us to run with rustc.
+fn main() {
+    check_val();
+    check_size();
+}

tests/kani/Projection/fixme_dyn_slice_projection.rs

@@ -0,0 +1,47 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --unwind 3
+
+//! This test case checks the usage of dyn Trait<[u8]>.
+use std::mem::size_of_val;
+
+trait Wrapper<T: ?Sized> {
+    fn inner(&self) -> &T;
+}
+
+struct Concrete<'a, T: ?Sized> {
+    inner: &'a T,
+}
+
+impl<T: ?Sized> Wrapper<T> for Concrete<'_, T> {
+    fn inner(&self) -> &T {
+        self.inner
+    }
+}
+
+#[cfg_attr(kani, kani::proof)]
+fn check_size() {
+    let original: Concrete<[u8]> = Concrete { inner: &[1u8, 2u8] };
+    let wrapper = &original as &dyn Wrapper<[u8]>;
+    let mut sum = 0u8;
+    for next in wrapper.inner() {
+        sum += next;
+    }
+    assert_eq!(sum, 3);
+}
+
+#[cfg_attr(kani, kani::proof)]
+fn check_iterator() {
+    let original: Concrete<[u8]> = Concrete { inner: &[1u8, 2u8] };
+    let wrapper = &original as &dyn Wrapper<[u8]>;
+    assert_eq!(size_of_val(wrapper), 16);
+    assert_eq!(size_of_val(&wrapper.inner()), 16);
+    assert_eq!(size_of_val(wrapper.inner()), 2);
+    assert_eq!(wrapper.inner().len(), 2);
+}
+
+// Leave this here so it's easy to run with rustc.
+fn main() {
+    check_iterator();
+    check_size();
+}

tests/kani/Projection/slice_dyn_projection.rs

@@ -0,0 +1,48 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --unwind 3
+
+//! Check that nested fat pointers work. This used to trigger an issue.
+//! The projection should only keep track of the inner most dereferenced
+//! element.
+//!
+//! See: https://github.com/model-checking/kani/issues/378
+
+trait Trait {
+    fn id(&self) -> u8;
+}
+
+struct Concrete {
+    pub id: u8,
+}
+
+impl Trait for Concrete {
+    fn id(&self) -> u8 {
+        self.id
+    }
+}
+
+#[kani::proof]
+fn check_slice_boxed() {
+    let boxed_t: &[Box<dyn Trait>] = &[Box::new(Concrete { id: 0 }), Box::new(Concrete { id: 1 })];
+
+    assert_eq!(boxed_t[0].id(), 0);
+    assert_eq!(boxed_t[1].id(), 1);
+}
+
+#[kani::proof]
+#[kani::unwind(3)]
+fn check_slice_boxed_iterator() {
+    let boxed_t: &[Box<dyn Trait>] = &[Box::new(Concrete { id: 0 }), Box::new(Concrete { id: 1 })];
+
+    // Check iterator
+    let mut sum = 0;
+    let mut count = 0;
+    for obj in boxed_t {
+        sum += obj.id();
+        count += 1;
+    }
+    assert_eq!(sum, 1);
+    assert_eq!(count, 2);
+}

tests/kani/Projection/slice_slice_projection.rs

@@ -0,0 +1,59 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --unwind 5
+
+//! This test case checks the usage of slices of slices (&[&[T]]).
+use std::mem::size_of_val;
+
+/// Structure with a raw string (i.e.: [char]).
+struct MyStr {
+    header: u16,
+    data: str,
+}
+
+impl MyStr {
+    /// This creates a MyStr from a byte slice.
+    fn new(original: &mut String) -> &mut Self {
+        let buf = original.get_mut(..).unwrap();
+        assert!(size_of_val(buf) > 2, "This requires at least 2 bytes");
+        let unsized_len = buf.len() - 2;
+        let ptr = std::ptr::slice_from_raw_parts_mut(buf.as_mut_ptr(), unsized_len);
+        unsafe { &mut *(ptr as *mut Self) }
+    }
+}
+
+#[kani::proof]
+fn sanity_check_my_str() {
+    let mut buf = String::from("123456");
+    let my_str = MyStr::new(&mut buf);
+    my_str.header = 0;
+
+    assert_eq!(size_of_val(my_str), 6);
+    assert_eq!(my_str.data.len(), 4);
+    assert_eq!(my_str.data.chars().nth(0), Some('3'));
+    assert_eq!(my_str.data.chars().nth(3), Some('6'));
+}
+
+#[kani::proof]
+fn check_slice_my_str() {
+    let mut buf_0 = String::from("000");
+    let mut buf_1 = String::from("001");
+    let my_slice = &[MyStr::new(&mut buf_0), MyStr::new(&mut buf_1)];
+    assert_eq!(my_slice.len(), 2);
+
+    assert_eq!(my_slice[0].data.len(), 1);
+    assert_eq!(my_slice[1].data.len(), 1);
+
+    assert_eq!(my_slice[0].data.chars().nth(0), Some('0'));
+    assert_eq!(my_slice[1].data.chars().nth(0), Some('1'));
+}
+
+#[kani::proof]
+fn check_size_of_val() {
+    let mut buf_0 = String::from("000");
+    let mut buf_1 = String::from("001");
+    let my_slice = &[MyStr::new(&mut buf_0), MyStr::new(&mut buf_1)];
+    assert_eq!(size_of_val(my_slice), 32); // Slice of 2 fat pointers.
+    assert_eq!(size_of_val(my_slice[0]), 4); // Size of a fat pointer.
+    assert_eq!(size_of_val(&my_slice[0].data), 1); // Size of str.
+}