Audit for transmute (#1104)

* Audit for `transmute`

* Add tests and minor fix

* remove `mut` from `packed`

* Restore original transmute codegen

* Fixes transmute restoration

* Remove alignment test

* Add tests for transmute

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

@@ -945,6 +945,10 @@ impl<'tcx> GotocCtx<'tcx> {
     ///     bitpattern = *((unsigned int *)&temp_0);
     ///     assert(bitpattern == 0x3F800000);
     /// }
+    ///
+    /// Note(std): An earlier attempt to add alignment checks for both the argument and result types
+    /// had catastrophic results in the regression. Hence, we don't perform any additional checks
+    /// and only encode the transmute operation here.
     fn codegen_intrinsic_transmute(
         &mut self,
         mut fargs: Vec<Expr>,
@@ -953,7 +957,8 @@ impl<'tcx> GotocCtx<'tcx> {
     ) -> Stmt {
         assert!(fargs.len() == 1, "transmute had unexpected arguments {:?}", fargs);
         let arg = fargs.remove(0);
-        let expr = arg.transmute_to(self.codegen_ty(ret_ty), &self.symbol_table);
+        let cbmc_ret_ty = self.codegen_ty(ret_ty);
+        let expr = arg.transmute_to(cbmc_ret_ty, &self.symbol_table);
         self.codegen_expr_to_place(p, expr)
     }
 

tests/kani/Intrinsics/Transmute/arr_to_struct.rs

@@ -0,0 +1,18 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `transmute` works as expected when turning an array into
+// a struct.
+
+struct Pair {
+    fst: u16,
+    snd: u16,
+}
+
+#[kani::proof]
+fn main() {
+    let arr = [0; 4];
+    let pair = unsafe { std::mem::transmute::<[u8; 4], Pair>(arr) };
+    assert_eq!(pair.fst, 0);
+    assert_eq!(pair.snd, 0);
+}

tests/kani/Intrinsics/Transmute/bytes_to_u32.rs

@@ -0,0 +1,15 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `transmute` works as expected when turning raw bytes into
+// a `u32`.
+
+// This test is a modified version of the example found in
+// https://doc.rust-lang.org/std/intrinsics/fn.transmute.html
+
+#[kani::proof]
+fn main() {
+    let raw_bytes = [0x78, 0x56, 0x34, 0x12];
+    let num = unsafe { std::mem::transmute::<[u8; 4], u32>(raw_bytes) };
+    assert_eq!(num, 0x12345678);
+}

tests/kani/Intrinsics/Transmute/ptr_to_fn_ptr.rs

@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `transmute` works as expected when turning a pointer into
+// a function pointer.
+
+// This test is a modified version of the example found in
+// https://doc.rust-lang.org/std/intrinsics/fn.transmute.html
+
+fn foo() -> i32 {
+    0
+}
+
+#[kani::proof]
+fn main() {
+    let pointer = foo as *const ();
+    let function = unsafe { std::mem::transmute::<*const (), fn() -> i32>(pointer) };
+    assert_eq!(function(), 0);
+}

tests/kani/Intrinsics/Transmute/str_to_slice.rs

@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `transmute` works as expected when turning a `str` into
+// `&[u8]`.
+
+// This test is a modified version of the example found in
+// https://doc.rust-lang.org/std/intrinsics/fn.transmute.html
+
+#[kani::proof]
+fn main() {
+    let slice = unsafe { std::mem::transmute::<&str, &[u8]>("Rust") };
+    assert_eq!(slice, &[82, 117, 115, 116]);
+}