Cast any pointer to trait pointer

compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs

@@ -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());
@@ -1027,7 +1027,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);

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

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

rust-tests/cbmc-reg/FatPointers/boxslice1.rs

@@ -0,0 +1,15 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Casts boxed array to boxed slice (example taken from rust documentation)
+use std::str;
+
+fn main() {
+    // This vector of bytes is used to initialize a Box<[u8; 4]>
+    let sparkle_heart_vec = vec![240, 159, 146, 150];
+
+    // This transformer produces a Box<[u8>]
+    let _sparkle_heart_str = str::from_utf8(&sparkle_heart_vec);
+
+    // see boxslice2_fail.rs for an attempt to test sparkle_heart_str
+}

rust-tests/cbmc-reg/FatPointers/boxslice2_fail.rs

@@ -0,0 +1,23 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Casts boxed array to boxed slice (example taken from rust documentation)
+use std::str;
+
+fn main() {
+    // This vector of bytes is used to initialize a Box<[u8; 4]>
+    let sparkle_heart_vec = vec![240, 159, 146, 150];
+
+    // This transformer produces a Box<[u8>]
+    let sparkle_heart_str = str::from_utf8(&sparkle_heart_vec);
+
+    // This match statement generates failures even though
+    // the binary runs without failures.
+    match sparkle_heart_str {
+        Ok(string) => match string.bytes().nth(0) {
+            Some(b) => assert!(b == 240),
+            _ => assert!(true),
+        },
+        _ => assert!(true),
+    }
+}

rust-tests/cbmc-reg/FatPointers/boxtrait.rs

@@ -0,0 +1,34 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This is handled by the box to box case of unsized pointers
+
+pub trait Trait {
+    fn increment(&mut self);
+    fn get(&self) -> u32;
+}
+
+struct Concrete {
+    pub index: u32,
+}
+
+impl Concrete {
+    fn new() -> Self {
+        Concrete { index: 0 }
+    }
+}
+
+impl Trait for Concrete {
+    fn increment(&mut self) {
+        self.index = self.index + 1;
+    }
+    fn get(&self) -> u32 {
+        self.index
+    }
+}
+
+fn main() {
+    let mut x: Box<dyn Trait> = Box::new(Concrete::new());
+    x.increment();
+    assert!(x.get() == 1);
+}

rust-tests/cbmc-reg/FatPointers/slice1.rs

@@ -0,0 +1,9 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {
+    let array = [1, 2, 3, 4, 5, 6];
+    let slice: &[u32] = &array;
+    assert!(slice[0] == 1);
+    assert!(slice[5] == 6);
+}

rust-tests/cbmc-reg/FatPointers/slice2.rs

@@ -0,0 +1,9 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {
+    let array = [1, 2, 3, 4, 5, 6];
+    let slice = &array[2..5];
+    assert!(slice[0] == 3);
+    assert!(slice[2] == 5);
+}

rust-tests/cbmc-reg/FatPointers/slice3.rs

@@ -0,0 +1,9 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {
+    let array = [1, 2, 3, 4, 5, 6];
+    let slice1 = &array[2..5];
+    let slice2 = &slice1[1..2];
+    assert!(slice2[0] == 4);
+}

rust-tests/cbmc-reg/FatPointers/structslice.rs

@@ -0,0 +1,18 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+struct Concrete {
+    array: [u32; 4],
+}
+
+struct Abstract<'a> {
+    uints: &'a [u32],
+}
+
+fn main() {
+    let x = Concrete { array: [1, 2, 3, 4] };
+    assert!(x.array[0] == 1);
+    let y = Abstract { uints: &[10, 11, 12, 13] };
+    assert!(y.uints[0] == 10);
+    assert!(y.uints[3] == 13);
+}

rust-tests/cbmc-reg/FatPointers/trait1.rs

@@ -0,0 +1,31 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Cast a concrete ref to a trait ref.
+
+pub trait Subscriber {
+    fn process(&self) -> u32;
+}
+
+struct DummySubscriber {
+    val: u32,
+}
+
+impl DummySubscriber {
+    fn new() -> Self {
+        DummySubscriber { val: 0 }
+    }
+}
+
+impl Subscriber for DummySubscriber {
+    fn process(&self) -> u32 {
+        let DummySubscriber { val: v } = self;
+        *v + 1
+    }
+}
+
+fn main() {
+    let _d = DummySubscriber::new();
+    let _s = &_d as &dyn Subscriber;
+    assert!(_s.process() == 1);
+}

rust-tests/cbmc-reg/FatPointers/trait2.rs

@@ -0,0 +1,31 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Cast a concrete ref to a trait raw pointer.
+
+pub trait Subscriber {
+    fn process(&self) -> u32;
+}
+
+struct DummySubscriber {
+    val: u32,
+}
+
+impl DummySubscriber {
+    fn new() -> Self {
+        DummySubscriber { val: 0 }
+    }
+}
+
+impl Subscriber for DummySubscriber {
+    fn process(&self) -> u32 {
+        let DummySubscriber { val: v } = self;
+        *v + 1
+    }
+}
+
+fn main() {
+    let _d = DummySubscriber::new();
+    let _s = &_d as *const dyn Subscriber;
+    assert!(unsafe { _s.as_ref().unwrap().process() } == 1);
+}

rust-tests/cbmc-reg/FatPointers/trait3.rs

@@ -0,0 +1,45 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Cast a concrete ref to
+//   concrete raw pointer
+//   trait ref
+//   trait raw pointer
+// Cast a trait ref to a trait raw pointer
+
+pub trait Subscriber {
+    fn process(&self) -> u32;
+}
+
+struct DummySubscriber {
+    val: u32,
+}
+
+impl DummySubscriber {
+    fn new() -> Self {
+        DummySubscriber { val: 0 }
+    }
+}
+
+impl Subscriber for DummySubscriber {
+    fn process(&self) -> u32 {
+        let DummySubscriber { val: v } = self;
+        *v + 1
+    }
+}
+
+fn main() {
+    let d = DummySubscriber::new();
+
+    let d1 = &d as *const DummySubscriber;
+    assert!(unsafe { d1.as_ref().unwrap().process() } == 1);
+
+    let s = &d as &dyn Subscriber;
+    assert!(s.process() == 1);
+
+    let s1 = &d as *const dyn Subscriber;
+    assert!(unsafe { s1.as_ref().unwrap().process() } == 1);
+
+    let x = s as *const dyn Subscriber;
+    assert!(unsafe { x.as_ref().unwrap().process() } == 1);
+}

rust-tests/cbmc-reg/Transparent/transparent1.rs

@@ -0,0 +1,9 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {
+    let mut x: u32 = 4;
+    let pointer0: std::ptr::NonNull<u32> = std::ptr::NonNull::new(&mut x).unwrap();
+    let y = unsafe { *pointer0.as_ptr() };
+    assert!(y == 4);
+}

rust-tests/cbmc-reg/Transparent/transparent2.rs

@@ -0,0 +1,36 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[derive(Clone, Copy)]
+struct Target {
+    x: u32,
+    y: u32,
+}
+
+struct Container<T> {
+    ptr: std::ptr::NonNull<T>,
+}
+
+impl<T> Container<T>
+where
+    T: Copy,
+{
+    fn new(val: &mut T) -> Self {
+        return Container { ptr: std::ptr::NonNull::new(val).unwrap() };
+    }
+    fn get(&self) -> T {
+        return unsafe { *self.ptr.as_ptr() };
+    }
+}
+
+fn main() {
+    let mut x: u32 = 4;
+    let container = Container::new(&mut x);
+    let _y = container.get();
+    assert_eq!(_y, 4);
+
+    let mut target: Target = Target { x: 3, y: 4 };
+    let cont = Container::new(&mut target);
+    assert!((unsafe { *cont.ptr.as_ptr() }).x == 3);
+    assert!((unsafe { *cont.ptr.as_ptr() }).y == 4);
+}

rust-tests/cbmc-reg/Transparent/transparent3.rs

@@ -0,0 +1,20 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//#repr(transparent)]
+pub struct Pointer<T> {
+    pointer: *const T,
+}
+
+pub struct Container<T> {
+    container: Pointer<T>,
+}
+
+fn main() {
+    let x: u32 = 4;
+    let my_pointer = Pointer { pointer: &x };
+    let my_container = Container { container: my_pointer };
+
+    let y: u32 = unsafe { *my_container.container.pointer };
+    assert!(y == 4);
+}

rust-tests/cbmc-reg/Transparent/transparent4.rs

@@ -0,0 +1,27 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[repr(transparent)]
+pub struct Pointer<T> {
+    pointer: *const T,
+}
+
+#[repr(transparent)]
+pub struct Wrapper<T>(T);
+
+pub struct Container<T> {
+    container: Pointer<T>,
+}
+
+fn main() {
+    let x: u32 = 4;
+    let my_container = Container { container: Pointer { pointer: &x } };
+
+    let y: u32 = unsafe { *my_container.container.pointer };
+    assert!(y == 4);
+
+    let w: Wrapper<u32> = Wrapper(4);
+
+    let Wrapper(c) = w;
+    assert!(c == 4);
+}