Mitigate invalid transmute when checking memory initialization (rus…

…t-lang#3338)

This PR addresses another aspect of rust-lang#3324, where delayed UB could be
caused by transmuting a mutable pointer into the one of incompatible
padding. It also adds a check to error whenever transmuting between two
types of incompatible padding.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

kani-compiler/src/kani_middle/transform/check_uninit/mod.rs

@@ -142,9 +142,11 @@ impl UninitPass {
  operation: MemoryInitOp,
  skip_first: &mut HashSet<usize>,
  ) {
- if let MemoryInitOp::Unsupported { reason } = &operation {
+ if let MemoryInitOp::Unsupported { reason } | MemoryInitOp::TriviallyUnsafe { reason } =
+ &operation
+ {
  collect_skipped(&operation, body, skip_first);
- self.unsupported_check(tcx, body, source, operation.position(), reason);
+ self.inject_assert_false(tcx, body, source, operation.position(), reason);
  return;
  };
 
@@ -166,7 +168,7 @@ impl UninitPass {
  "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}.",
  );
  collect_skipped(&operation, body, skip_first);
- self.unsupported_check(tcx, body, source, operation.position(), &reason);
+ self.inject_assert_false(tcx, body, source, operation.position(), &reason);
  return;
  }
  }
@@ -181,7 +183,7 @@ impl UninitPass {
  | MemoryInitOp::SetRef { .. } => {
  self.build_set(tcx, body, source, operation, pointee_ty_info, skip_first)
  }
- MemoryInitOp::Unsupported { .. } => {
+ MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => {
  unreachable!()
  }
  }
@@ -266,7 +268,7 @@ impl UninitPass {
  PointeeLayout::TraitObject => {
  collect_skipped(&operation, body, skip_first);
  let reason = "Kani does not support reasoning about memory initialization of pointers to trait objects.";
- self.unsupported_check(tcx, body, source, operation.position(), reason);
+ self.inject_assert_false(tcx, body, source, operation.position(), reason);
  return;
  }
  };
@@ -392,7 +394,7 @@ impl UninitPass {
  };
  }
 
- fn unsupported_check(
+ fn inject_assert_false(
  &self,
  tcx: TyCtxt,
  body: &mut MutableBody,

kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs

@@ -37,6 +37,8 @@ pub enum MemoryInitOp {
  SetRef { operand: Operand, value: bool, position: InsertPosition },
  /// Unsupported memory initialization operation.
  Unsupported { reason: String },
+ /// Operation that trivially accesses uninitialized memory, results in injecting `assert!(false)`.
+ TriviallyUnsafe { reason: String },
 }
 
 impl MemoryInitOp {
@@ -63,7 +65,9 @@ impl MemoryInitOp {
  },
  projection: vec![],
  }),
- MemoryInitOp::Unsupported { .. } => unreachable!(),
+ MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => {
+ unreachable!()
+ }
  }
  }
 
@@ -74,7 +78,8 @@ impl MemoryInitOp {
  MemoryInitOp::Check { .. }
  | MemoryInitOp::Set { .. }
  | MemoryInitOp::SetRef { .. }
- | MemoryInitOp::Unsupported { .. } => unreachable!(),
+ | MemoryInitOp::Unsupported { .. }
+ | MemoryInitOp::TriviallyUnsafe { .. } => unreachable!(),
  }
  }
 
@@ -85,7 +90,8 @@ impl MemoryInitOp {
  | MemoryInitOp::SetRef { value, .. } => *value,
  MemoryInitOp::Check { .. }
  | MemoryInitOp::CheckSliceChunk { .. }
- | MemoryInitOp::Unsupported { .. } => unreachable!(),
+ | MemoryInitOp::Unsupported { .. }
+ | MemoryInitOp::TriviallyUnsafe { .. } => unreachable!(),
  }
  }
 
@@ -96,7 +102,8 @@ impl MemoryInitOp {
  | MemoryInitOp::SetRef { position, .. } => *position,
  MemoryInitOp::Check { .. }
  | MemoryInitOp::CheckSliceChunk { .. }
- | MemoryInitOp::Unsupported { .. } => InsertPosition::Before,
+ | MemoryInitOp::Unsupported { .. }
+ | MemoryInitOp::TriviallyUnsafe { .. } => InsertPosition::Before,
  }
  }
 }
@@ -581,6 +588,29 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
  }
  }
  }
+ CastKind::Transmute => {
+ let operand_ty = operand.ty(&self.locals).unwrap();
+ if let (
+ RigidTy::RawPtr(from_ty, Mutability::Mut),
+ RigidTy::RawPtr(to_ty, Mutability::Mut),
+ ) = (operand_ty.kind().rigid().unwrap(), ty.kind().rigid().unwrap())
+ {
+ if !tys_layout_compatible(from_ty, to_ty) {
+ // If casting from a mutable pointer to a mutable pointer with different
+ // layouts, delayed UB could occur.
+ self.push_target(MemoryInitOp::Unsupported {
+ reason: "Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB.".to_string(),
+ });
+ }
+ } else if !tys_layout_compatible(&operand_ty, &ty) {
+ // If transmuting between two types of incompatible layouts, padding
+ // bytes are exposed, which is UB.
+ self.push_target(MemoryInitOp::TriviallyUnsafe {
+ reason: "Transmuting between types of incompatible layouts."
+ .to_string(),
+ });
+ }
+ }
  _ => {}
  }
  };

tests/expected/uninit/delayed-ub-transmute/delayed-ub-transmute.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z uninit-checks
+
+/// Checks that Kani rejects mutable pointer casts between types of different padding.
+#[kani::proof]
+fn invalid_value() {
+ unsafe {
+ let mut value: u128 = 0;
+ let ptr: *mut (u8, u32, u64) = std::mem::transmute(&mut value as *mut _);
+ *ptr = (4, 4, 4); // This assignment itself does not cause UB...
+ let c: u128 = value; // ...but this reads a padding value!
+ }
+}

tests/expected/uninit/delayed-ub-transmute/expected

@@ -0,0 +1,5 @@
+Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB.
+
+VERIFICATION:- FAILED
+
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/expected/uninit/transmute-padding/expected

@@ -0,0 +1,5 @@
+Failed Checks: Transmuting between types of incompatible layouts.
+
+VERIFICATION:- FAILED
+
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/expected/uninit/transmute-padding/transmute_padding.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z uninit-checks
+
+// 5 bytes of data + 3 bytes of padding.
+#[repr(C)]
+#[derive(kani::Arbitrary)]
+struct S(u32, u8);
+
+/// Checks that Kani catches an attempt to access padding of a struct using transmute.
+#[kani::proof]
+fn check_uninit_padding() {
+ let s = kani::any();
+ access_padding(s);
+}
+
+fn access_padding(s: S) {
+ let _padding: u64 = unsafe { std::mem::transmute(s) }; // ~ERROR: padding bytes are uninitialized, so reading them is UB.
+}