Audit for transmute

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

@@ -576,7 +576,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "sqrtf32" => unstable_codegen!(codegen_simple_intrinsic!(Sqrtf)),
             "sqrtf64" => unstable_codegen!(codegen_simple_intrinsic!(Sqrt)),
             "sub_with_overflow" => codegen_op_with_overflow!(sub_overflow),
-            "transmute" => self.codegen_intrinsic_transmute(fargs, ret_ty, p),
+            "transmute" => self.codegen_intrinsic_transmute(instance, fargs, ret_ty, p, span),
             "truncf32" => codegen_unimplemented_intrinsic!(
                 "https://github.com/model-checking/kani/issues/1025"
             ),
@@ -916,14 +916,41 @@ impl<'tcx> GotocCtx<'tcx> {
     /// }
     fn codegen_intrinsic_transmute(
         &mut self,
+        instance: Instance<'tcx>,
         mut fargs: Vec<Expr>,
         ret_ty: Ty<'tcx>,
         p: &Place<'tcx>,
+        span: Option<Span>,
     ) -> Stmt {
         assert!(fargs.len() == 1, "transmute had unexpected arguments {:?}", fargs);
+        let loc = self.codegen_span_option(span);
+
+        // Check that the argument type is properly aligned
         let arg = fargs.remove(0);
-        let expr = arg.transmute_to(self.codegen_ty(ret_ty), &self.symbol_table);
-        self.codegen_expr_to_place(p, expr)
+        let arg_typ = self.monomorphize(instance.substs.type_at(0));
+        let arg_align = self.is_aligned(arg_typ, arg.clone());
+        let arg_align_check = self.codegen_assert(
+            arg_align,
+            PropertyClass::DefaultAssertion,
+            "transmute: argument type is properly aligned",
+            loc.clone(),
+        );
+
+        // Check that the result type is properly aligned
+        let ret_expr = self.codegen_place(&p).unwrap().goto_expr;
+        let ret_align = self.is_aligned(ret_ty, ret_expr);
+        let ret_align_check = self.codegen_assert(
+            ret_align,
+            PropertyClass::DefaultAssertion,
+            "transmute: result type is properly aligned",
+            loc.clone(),
+        );
+
+        // Encode the actual transmute expression
+        let cbmc_ret_ty = self.codegen_ty(ret_ty);
+        let transmute_expr = arg.transmute_to(cbmc_ret_ty, &self.symbol_table);
+        let expr = self.codegen_expr_to_place(p, transmute_expr);
+        Stmt::block(vec![arg_align_check, ret_align_check, expr], loc)
     }
 
     // `raw_eq` determines whether the raw bytes of two values are equal.

tests/expected/transmute-arg-align/expected

@@ -0,0 +1,2 @@
+FAILURE\
+transmute: argument type is properly aligned

tests/expected/transmute-arg-align/main.rs

@@ -0,0 +1,17 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[repr(packed)]
+struct Packed {
+    _padding: u8,
+    unaligned: u32,
+}
+
+#[kani::proof]
+fn main() {
+    let packed: Packed = unsafe { std::mem::zeroed() };
+    unsafe {
+        let x = std::mem::transmute::<u32, u32>(packed.unaligned);
+        assert_eq!(x, 0);
+    }
+}