From 81d4e46ec99a88bd8dd9e7c8b8f16ff0fea1ffa6 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Thu, 16 Feb 2023 01:40:30 -0800
Subject: [PATCH 01/28] (`c2rust-analyze`) Support ptr-to-ptr casts between
 safely transmutable types, for now limited to same-sized integers.

This introduces the concept of equivalent/compatible/safely transmutable types.
This forms an equivalence class among types, as the safe transmutability must be mutual
(i.e. transmutable in both directions; no prefix-transmutability).

Thus, we can now allow ptr-to-ptr casts between safely transmutable pointee types,
whereas previously they were only allowed for equal types.
Equal types could have their `PointerId`s unified as they had the same structure,
which is still of safely transmutability types,
which are safely transmutability because they have the same structure/layout.

As safe transmutability is difficult to check abstractly for any two types,
for now we limit it to commonly transmuted types that we know are definitely transmutable:
same-sized integer types (with potentially different signedness).

Thus, this enables support for string casts like
`b"" as *const u8 as *const core::ffi::c_char`, where `c_char = i8`,
which fixes #840.

Note that the above cast (#833) is still not supported due to the string literal `b""` (#837),
but the cast itself (in `string_casts.rs` in `fn cast_only`) works.
---
 c2rust-analyze/src/context.rs                | 33 +++++++--------
 c2rust-analyze/src/dataflow/type_check.rs    | 12 +++---
 c2rust-analyze/src/util.rs                   | 44 +++++++++++++++++++-
 c2rust-analyze/tests/analyze/string_casts.rs |  1 -
 4 files changed, 66 insertions(+), 24 deletions(-)

diff --git a/c2rust-analyze/src/context.rs b/c2rust-analyze/src/context.rs
index 7e78cf51b..5ae0c5813 100644
--- a/c2rust-analyze/src/context.rs
+++ b/c2rust-analyze/src/context.rs
@@ -3,7 +3,7 @@ use crate::pointer_id::{
     GlobalPointerTable, LocalPointerTable, NextGlobalPointerId, NextLocalPointerId, PointerTable,
     PointerTableMut,
 };
-use crate::util::{self, describe_rvalue, RvalueDesc};
+use crate::util::{self, are_transmutable_ptrs, describe_rvalue, RvalueDesc};
 use crate::AssignPointerIds;
 use bitflags::bitflags;
 use rustc_hir::def_id::DefId;
@@ -349,23 +349,22 @@ impl<'a, 'tcx> AnalysisCtxt<'a, 'tcx> {
             Rvalue::Cast(_, ref op, ty) => {
                 let op_lty = self.type_of(op);
 
-                // We support this category of pointer casts as a special case.
-                let op_is_ptr = matches!(op_lty.ty.kind(), TyKind::Ref(..) | TyKind::RawPtr(..));
-                let op_pointee = op_is_ptr.then(|| op_lty.args[0]);
-                let ty_pointee = match *ty.kind() {
-                    TyKind::Ref(_, ty, _) => Some(ty),
-                    TyKind::RawPtr(tm) => Some(tm.ty),
-                    _ => None,
-                };
-                if op_pointee.is_some() && op_pointee.map(|lty| lty.ty) == ty_pointee {
-                    // The source and target types are both pointers, and they have identical
-                    // pointee types.  We label the target type with the same `PointerId`s as the
-                    // source type in all positions.  This works because the two types have the
-                    // same structure.
-                    return self.lcx().mk(ty, op_lty.args, op_lty.label);
+                // We only support pointer casts when:
+                // * both types are pointers
+                // * they have compatible (safely transmutable) pointee types
+                // Safe transmutability is difficult to check abstractly,
+                // so we limit it to integer types of the same size
+                // (but potentially different signedness).
+                // In particular, this allows casts from `*u8` to `*core::ffi::c_char`.
+                let from_ty = op_lty.ty;
+                let to_ty = ty;
+                match are_transmutable_ptrs(from_ty, to_ty) {
+                    // Label the to type with the same [`PointerId`]s as the from type in all positions.
+                    // This works because the two types have the same structure.
+                    Some(true) => self.lcx().mk(ty, op_lty.args, op_lty.label),
+                    Some(false) => todo!("unsupported ptr-to-ptr cast between pointee types not yet supported as safely transmutable: `{from_ty:?} as {to_ty:?}`"),
+                    None => label_no_pointers(self, ty),
                 }
-
-                label_no_pointers(self, ty)
             }
             Rvalue::Len(..)
             | Rvalue::BinaryOp(..)
diff --git a/c2rust-analyze/src/dataflow/type_check.rs b/c2rust-analyze/src/dataflow/type_check.rs
index 3d74a0482..867f47567 100644
--- a/c2rust-analyze/src/dataflow/type_check.rs
+++ b/c2rust-analyze/src/dataflow/type_check.rs
@@ -1,6 +1,6 @@
 use super::DataflowConstraints;
 use crate::context::{AnalysisCtxt, LTy, PermissionSet, PointerId};
-use crate::util::{self, describe_rvalue, Callee, RvalueDesc};
+use crate::util::{self, are_transmutable, describe_rvalue, Callee, RvalueDesc};
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::{
     AggregateKind, BinOp, Body, Location, Mutability, Operand, Place, PlaceRef, ProjectionElem,
@@ -207,10 +207,12 @@ impl<'tcx> TypeChecker<'tcx, '_> {
     /// that position.  For example, given `lty1 = *mut /*l1*/ *const /*l2*/ u8` and `lty2 = *mut
     /// /*l3*/ *const /*l4*/ u8`, this function will unify `l1` with `l3` and `l2` with `l4`.
     fn do_unify(&mut self, lty1: LTy<'tcx>, lty2: LTy<'tcx>) {
-        assert_eq!(
-            self.acx.tcx().erase_regions(lty1.ty),
-            self.acx.tcx().erase_regions(lty2.ty)
-        );
+        let ty1 = lty1.ty;
+        let ty2 = lty2.ty;
+        assert!(are_transmutable(
+            self.acx.tcx().erase_regions(ty1),
+            self.acx.tcx().erase_regions(ty2),
+        ), "types not transmutable (compatible), so PointerId unification cannot be done: {ty1:?} !~ {ty2:?}");
         for (sub_lty1, sub_lty2) in lty1.iter().zip(lty2.iter()) {
             eprintln!("equate {:?} = {:?}", sub_lty1, sub_lty2);
             if sub_lty1.label != PointerId::NONE || sub_lty2.label != PointerId::NONE {
diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index 1c6e35590..b69a68209 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -4,7 +4,8 @@ use rustc_hir::def_id::DefId;
 use rustc_middle::mir::{
     Field, Local, Mutability, Operand, PlaceElem, PlaceRef, ProjectionElem, Rvalue,
 };
-use rustc_middle::ty::{AdtDef, DefIdTree, SubstsRef, Ty, TyCtxt, TyKind, UintTy};
+use rustc_middle::ty::{self, AdtDef, DefIdTree, SubstsRef, Ty, TyCtxt, TyKind, UintTy};
+use rustc_type_ir::IntTy;
 use std::fmt::Debug;
 
 #[derive(Debug)]
@@ -305,3 +306,44 @@ pub fn lty_project<'tcx, L: Debug>(
         ProjectionElem::Downcast(..) => todo!("type_of Downcast"),
     }
 }
+
+/// Determine if two types are safe to transmute to each other.
+///
+/// Safe transmutability is difficult to check abstractly,
+/// so here it is limited to integer types of the same size
+/// (but potentially different signedness).
+///
+/// Thus, [`true`] means it is definitely transmutable,
+/// while [`false`] means it may not be transmutable.
+pub fn are_transmutable<'tcx>(a: Ty<'tcx>, b: Ty<'tcx>) -> bool {
+    let transmutable_ints = {
+        use IntTy::*;
+        use UintTy::*;
+        match (a.kind(), b.kind()) {
+            (ty::Uint(u), ty::Int(i)) | (ty::Int(i), ty::Uint(u)) => {
+                matches!((u, i), |(Usize, Isize)| (U8, I8)
+                    | (U16, I16)
+                    | (U32, I32)
+                    | (U64, I64))
+            }
+            _ => false,
+        }
+    };
+
+    // only check for transmutable ints so far
+    a == b || transmutable_ints
+}
+
+/// Determine if two types (e.x. in a cast) are pointers,
+/// and if they are, if the pointee types are compatible,
+/// i.e. they are safely transmutable to each other.
+///
+/// This returns [`Some`]`(is_transmutable)` if they're both pointers,
+/// and [`None`] if its some other types.
+///
+/// See [`are_transmutable`] for the definition of safe transmutability.
+pub fn are_transmutable_ptrs<'tcx>(a: Ty<'tcx>, b: Ty<'tcx>) -> Option<bool> {
+    let a = a.builtin_deref(true)?.ty;
+    let b = b.builtin_deref(true)?.ty;
+    Some(are_transmutable(a, b))
+}
diff --git a/c2rust-analyze/tests/analyze/string_casts.rs b/c2rust-analyze/tests/analyze/string_casts.rs
index 99a650237..9c959e76b 100644
--- a/c2rust-analyze/tests/analyze/string_casts.rs
+++ b/c2rust-analyze/tests/analyze/string_casts.rs
@@ -1,4 +1,3 @@
-#[cfg(any())]
 pub fn cast_only(s: *const u8) {
     s as *const core::ffi::c_char;
 }

From 68461db7a4e58a7a9d7cce5be35584cbe82bc594 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Thu, 16 Feb 2023 14:17:56 -0800
Subject: [PATCH 02/28] (`c2rust-analyze`) Clarified that `do_unify` now
 requires only compatible/safetly transmutable types, not identical.

---
 c2rust-analyze/src/dataflow/type_check.rs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/c2rust-analyze/src/dataflow/type_check.rs b/c2rust-analyze/src/dataflow/type_check.rs
index 867f47567..df158b982 100644
--- a/c2rust-analyze/src/dataflow/type_check.rs
+++ b/c2rust-analyze/src/dataflow/type_check.rs
@@ -202,8 +202,9 @@ impl<'tcx> TypeChecker<'tcx, '_> {
 
     /// Unify corresponding `PointerId`s in `lty1` and `lty2`.
     ///
-    /// The two inputs must have identical underlying types.  For any position where the underlying
-    /// type has a pointer, this function unifies the `PointerId`s that `lty1` and `lty2` have at
+    /// The two inputs must have compatible ([safely transmutable](are_transmutable)) underlying types.
+    /// For any position where the underlying type has a pointer,
+    /// this function unifies the `PointerId`s that `lty1` and `lty2` have at
     /// that position.  For example, given `lty1 = *mut /*l1*/ *const /*l2*/ u8` and `lty2 = *mut
     /// /*l3*/ *const /*l4*/ u8`, this function will unify `l1` with `l3` and `l2` with `l4`.
     fn do_unify(&mut self, lty1: LTy<'tcx>, lty2: LTy<'tcx>) {

From da4d9612d1dc156892e6eead253becf291c85c9f Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Fri, 17 Feb 2023 15:14:09 -0800
Subject: [PATCH 03/28] (`c2rust-analyze`) Support deeper levels of ptr
 transmutability (e.x. `a ~ b` => `*a ~ *b` for all `a`, `b`).

---
 c2rust-analyze/src/util.rs                   | 7 +++++--
 c2rust-analyze/tests/analyze/string_casts.rs | 4 ++++
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index b69a68209..ecb7123a1 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -313,10 +313,13 @@ pub fn lty_project<'tcx, L: Debug>(
 /// so here it is limited to integer types of the same size
 /// (but potentially different signedness).
 ///
+/// Extra (but equal) levels of pointer/reference indirection are allowed,
+/// i.e. `u8 ~ i8` implies `**u8 ~ **i8`.
+///
 /// Thus, [`true`] means it is definitely transmutable,
 /// while [`false`] means it may not be transmutable.
 pub fn are_transmutable<'tcx>(a: Ty<'tcx>, b: Ty<'tcx>) -> bool {
-    let transmutable_ints = {
+    let transmutable_ints = || {
         use IntTy::*;
         use UintTy::*;
         match (a.kind(), b.kind()) {
@@ -331,7 +334,7 @@ pub fn are_transmutable<'tcx>(a: Ty<'tcx>, b: Ty<'tcx>) -> bool {
     };
 
     // only check for transmutable ints so far
-    a == b || transmutable_ints
+    a == b || are_transmutable_ptrs(a, b).unwrap_or(false) || transmutable_ints()
 }
 
 /// Determine if two types (e.x. in a cast) are pointers,
diff --git a/c2rust-analyze/tests/analyze/string_casts.rs b/c2rust-analyze/tests/analyze/string_casts.rs
index 9c959e76b..538183aae 100644
--- a/c2rust-analyze/tests/analyze/string_casts.rs
+++ b/c2rust-analyze/tests/analyze/string_casts.rs
@@ -2,6 +2,10 @@ pub fn cast_only(s: *const u8) {
     s as *const core::ffi::c_char;
 }
 
+pub fn deep_cast(x: *const *const u8) {
+    x as *const *const i8;
+}
+
 #[cfg(any())]
 pub fn cast_from_literal() {
     b"" as *const u8 as *const core::ffi::c_char;

From 62ec8dca9c831a2d17d2ab622c4daac7baa6a755 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Fri, 17 Feb 2023 15:27:37 -0800
Subject: [PATCH 04/28] (`c2rust-analyze`) Formally defined the safe
 transmutability definition.

---
 c2rust-analyze/src/util.rs | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index ecb7123a1..3f5aca913 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -318,6 +318,16 @@ pub fn lty_project<'tcx, L: Debug>(
 ///
 /// Thus, [`true`] means it is definitely transmutable,
 /// while [`false`] means it may not be transmutable.
+///
+/// Formally, safe transmutability defines
+/// an equivalence relation on types, named `~` here.
+/// `A ~ B` iff `*(a as *const B)` and `*(b as *const A)` are safe,
+/// where `a: *const A` and `b: *const B`.
+///
+/// And the current incomplete implementation is defined as:
+/// * `A = B => A ~ B`
+/// * `A ~ B => *A ~ *B`
+/// * `uN ~ iN`, where `N` is an integer width
 pub fn are_transmutable<'tcx>(a: Ty<'tcx>, b: Ty<'tcx>) -> bool {
     let transmutable_ints = || {
         use IntTy::*;

From 0d88d7aa431e9858476f1b81d122ea1a1e8d7249 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Thu, 16 Feb 2023 12:45:02 -0800
Subject: [PATCH 05/28] (`c2rust-analyze`) Relaxed the transmutable checks from
 two-way to one-way, now allowing for arrays and slices to decay.

This expands the definition of safe transmutability to be one-way.
That is, it checks if `*T as *U` is safe, rather than also `*U as *T`.

Thus, we can now allow for casts decaying
pointers to arrays and slices to pointers to their element type.

`do_unify` is modified to also be one-way,
which it was already in all call sites.

New tests are also added to `string_casts.rs`
for all the types of ptr-to-ptr casts.

Out of the full string cast, `b"" as *const u8 as *const core::ffi::c_char`,
this adds support for the `as *const u8` (from `&[u8; _]`),
so only support for the string literal itself remains.
---
 c2rust-analyze/src/context.rs                |  4 +-
 c2rust-analyze/src/dataflow/type_check.rs    | 20 +++++-----
 c2rust-analyze/src/util.rs                   | 40 ++++++++++++--------
 c2rust-analyze/tests/analyze/string_casts.rs | 16 +++++++-
 4 files changed, 50 insertions(+), 30 deletions(-)

diff --git a/c2rust-analyze/src/context.rs b/c2rust-analyze/src/context.rs
index 5ae0c5813..592fb5742 100644
--- a/c2rust-analyze/src/context.rs
+++ b/c2rust-analyze/src/context.rs
@@ -3,7 +3,7 @@ use crate::pointer_id::{
     GlobalPointerTable, LocalPointerTable, NextGlobalPointerId, NextLocalPointerId, PointerTable,
     PointerTableMut,
 };
-use crate::util::{self, are_transmutable_ptrs, describe_rvalue, RvalueDesc};
+use crate::util::{self, describe_rvalue, is_transmutable_ptr_cast, RvalueDesc};
 use crate::AssignPointerIds;
 use bitflags::bitflags;
 use rustc_hir::def_id::DefId;
@@ -358,7 +358,7 @@ impl<'a, 'tcx> AnalysisCtxt<'a, 'tcx> {
                 // In particular, this allows casts from `*u8` to `*core::ffi::c_char`.
                 let from_ty = op_lty.ty;
                 let to_ty = ty;
-                match are_transmutable_ptrs(from_ty, to_ty) {
+                match is_transmutable_ptr_cast(from_ty, to_ty) {
                     // Label the to type with the same [`PointerId`]s as the from type in all positions.
                     // This works because the two types have the same structure.
                     Some(true) => self.lcx().mk(ty, op_lty.args, op_lty.label),
diff --git a/c2rust-analyze/src/dataflow/type_check.rs b/c2rust-analyze/src/dataflow/type_check.rs
index df158b982..78fb1aded 100644
--- a/c2rust-analyze/src/dataflow/type_check.rs
+++ b/c2rust-analyze/src/dataflow/type_check.rs
@@ -1,6 +1,6 @@
 use super::DataflowConstraints;
 use crate::context::{AnalysisCtxt, LTy, PermissionSet, PointerId};
-use crate::util::{self, are_transmutable, describe_rvalue, Callee, RvalueDesc};
+use crate::util::{self, describe_rvalue, is_transmutable_to, Callee, RvalueDesc};
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::{
     AggregateKind, BinOp, Body, Location, Mutability, Operand, Place, PlaceRef, ProjectionElem,
@@ -202,19 +202,19 @@ impl<'tcx> TypeChecker<'tcx, '_> {
 
     /// Unify corresponding `PointerId`s in `lty1` and `lty2`.
     ///
-    /// The two inputs must have compatible ([safely transmutable](are_transmutable)) underlying types.
+    /// The two inputs must have compatible ([safely transmutable](is_transmutable_to)) underlying types.
     /// For any position where the underlying type has a pointer,
     /// this function unifies the `PointerId`s that `lty1` and `lty2` have at
     /// that position.  For example, given `lty1 = *mut /*l1*/ *const /*l2*/ u8` and `lty2 = *mut
     /// /*l3*/ *const /*l4*/ u8`, this function will unify `l1` with `l3` and `l2` with `l4`.
-    fn do_unify(&mut self, lty1: LTy<'tcx>, lty2: LTy<'tcx>) {
-        let ty1 = lty1.ty;
-        let ty2 = lty2.ty;
-        assert!(are_transmutable(
-            self.acx.tcx().erase_regions(ty1),
-            self.acx.tcx().erase_regions(ty2),
-        ), "types not transmutable (compatible), so PointerId unification cannot be done: {ty1:?} !~ {ty2:?}");
-        for (sub_lty1, sub_lty2) in lty1.iter().zip(lty2.iter()) {
+    fn do_unify(&mut self, pl_lty: LTy<'tcx>, rv_lty: LTy<'tcx>) {
+        let rv_ty = self.acx.tcx().erase_regions(rv_lty.ty);
+        let pl_ty = self.acx.tcx().erase_regions(pl_lty.ty);
+        assert!(
+            is_transmutable_to(rv_ty, pl_ty),
+            "types not transmutable (compatible), so PointerId unification cannot be done: *{rv_ty:?} as *{pl_ty:?}",
+        );
+        for (sub_lty1, sub_lty2) in pl_lty.iter().zip(rv_lty.iter()) {
             eprintln!("equate {:?} = {:?}", sub_lty1, sub_lty2);
             if sub_lty1.label != PointerId::NONE || sub_lty2.label != PointerId::NONE {
                 assert!(sub_lty1.label != PointerId::NONE);
diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index 3f5aca913..0552ac89d 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -307,18 +307,22 @@ pub fn lty_project<'tcx, L: Debug>(
     }
 }
 
-/// Determine if two types are safe to transmute to each other.
+/// Determine if `from_ty` can be safely transmuted to `to_ty`.
 ///
 /// Safe transmutability is difficult to check abstractly,
-/// so here it is limited to integer types of the same size
-/// (but potentially different signedness).
+/// so here it is limited to
+/// * integer types of the same size (but potentially different signedness)
+///     * e.x. `*u8 as *i8`
+/// * decaying arrays and slices to their element type
+///     * e.x. `*[u8; 0] as *u8`
+///     * e.x. `*[u8] as *u8`
 ///
 /// Extra (but equal) levels of pointer/reference indirection are allowed,
 /// i.e. `u8 ~ i8` implies `**u8 ~ **i8`.
 ///
 /// Thus, [`true`] means it is definitely transmutable,
 /// while [`false`] means it may not be transmutable.
-///
+/// 
 /// Formally, safe transmutability defines
 /// an equivalence relation on types, named `~` here.
 /// `A ~ B` iff `*(a as *const B)` and `*(b as *const A)` are safe,
@@ -328,11 +332,11 @@ pub fn lty_project<'tcx, L: Debug>(
 /// * `A = B => A ~ B`
 /// * `A ~ B => *A ~ *B`
 /// * `uN ~ iN`, where `N` is an integer width
-pub fn are_transmutable<'tcx>(a: Ty<'tcx>, b: Ty<'tcx>) -> bool {
+pub fn is_transmutable_to<'tcx>(from_ty: Ty<'tcx>, to_ty: Ty<'tcx>) -> bool {
     let transmutable_ints = || {
         use IntTy::*;
         use UintTy::*;
-        match (a.kind(), b.kind()) {
+        match (from_ty.kind(), to_ty.kind()) {
             (ty::Uint(u), ty::Int(i)) | (ty::Int(i), ty::Uint(u)) => {
                 matches!((u, i), |(Usize, Isize)| (U8, I8)
                     | (U16, I16)
@@ -343,20 +347,24 @@ pub fn are_transmutable<'tcx>(a: Ty<'tcx>, b: Ty<'tcx>) -> bool {
         }
     };
 
-    // only check for transmutable ints so far
-    a == b || are_transmutable_ptrs(a, b).unwrap_or(false) || transmutable_ints()
+    let one_way_transmutable = || match from_ty.kind() {
+        &ty::Array(from_ty, _) | &ty::Slice(from_ty) => is_transmutable_to(from_ty, to_ty),
+        _ => false,
+    };
+
+    from_ty == to_ty || is_transmutable_ptr_cast(from_ty, to_ty).unwrap_or(false) || transmutable_ints() || one_way_transmutable()
 }
 
-/// Determine if two types (e.x. in a cast) are pointers,
-/// and if they are, if the pointee types are compatible,
-/// i.e. they are safely transmutable to each other.
+/// Determine if the `from_ty as to_ty` is a ptr-to-ptr cast.
+/// and if it is, if the pointee types are compatible,
+/// i.e. they are safely transmutable.
 ///
 /// This returns [`Some`]`(is_transmutable)` if they're both pointers,
 /// and [`None`] if its some other types.
 ///
-/// See [`are_transmutable`] for the definition of safe transmutability.
-pub fn are_transmutable_ptrs<'tcx>(a: Ty<'tcx>, b: Ty<'tcx>) -> Option<bool> {
-    let a = a.builtin_deref(true)?.ty;
-    let b = b.builtin_deref(true)?.ty;
-    Some(are_transmutable(a, b))
+/// See [`is_transmutable_to`] for the definition of safe transmutability.
+pub fn is_transmutable_ptr_cast<'tcx>(from_ty: Ty<'tcx>, to_ty: Ty<'tcx>) -> Option<bool> {
+    let from_ty = from_ty.builtin_deref(true)?.ty;
+    let to_ty = to_ty.builtin_deref(true)?.ty;
+    Some(is_transmutable_to(from_ty, to_ty))
 }
diff --git a/c2rust-analyze/tests/analyze/string_casts.rs b/c2rust-analyze/tests/analyze/string_casts.rs
index 538183aae..abe0fbb86 100644
--- a/c2rust-analyze/tests/analyze/string_casts.rs
+++ b/c2rust-analyze/tests/analyze/string_casts.rs
@@ -1,11 +1,23 @@
-pub fn cast_only(s: *const u8) {
+pub fn cast_ptr_to_ptr(s: *const u8) {
     s as *const core::ffi::c_char;
 }
 
-pub fn deep_cast(x: *const *const u8) {
+pub fn deep_cast_ptr_to_ptr(x: *const *const u8) {
     x as *const *const i8;
 }
 
+pub fn cast_slice_ptr_to_ptr(s: *const [u8]) {
+    s as *const u8;
+}
+
+pub fn cast_array_to_slice_ptr(s: &[u8; 0]) {
+    s as *const [u8];
+}
+
+pub fn cast_array_to_ptr(s: &[u8; 0]) {
+    s as *const u8;
+}
+
 #[cfg(any())]
 pub fn cast_from_literal() {
     b"" as *const u8 as *const core::ffi::c_char;

From a148146e9c6e39642f3d2a81d2916e8db085a1db Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Thu, 16 Feb 2023 14:54:40 -0800
Subject: [PATCH 06/28] (`c2rust-analyze`) Updated `do_unify` docs after the
 renaming.

---
 c2rust-analyze/src/dataflow/type_check.rs | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/c2rust-analyze/src/dataflow/type_check.rs b/c2rust-analyze/src/dataflow/type_check.rs
index 78fb1aded..31909d9d7 100644
--- a/c2rust-analyze/src/dataflow/type_check.rs
+++ b/c2rust-analyze/src/dataflow/type_check.rs
@@ -200,13 +200,21 @@ impl<'tcx> TypeChecker<'tcx, '_> {
         }
     }
 
-    /// Unify corresponding `PointerId`s in `lty1` and `lty2`.
+    /// Unify corresponding [`PointerId`]s in `pl_lty` and `rv_lty`.
     ///
     /// The two inputs must have compatible ([safely transmutable](is_transmutable_to)) underlying types.
     /// For any position where the underlying type has a pointer,
-    /// this function unifies the `PointerId`s that `lty1` and `lty2` have at
-    /// that position.  For example, given `lty1 = *mut /*l1*/ *const /*l2*/ u8` and `lty2 = *mut
-    /// /*l3*/ *const /*l4*/ u8`, this function will unify `l1` with `l3` and `l2` with `l4`.
+    /// this function unifies the [`PointerId`]s that `pl_lty` and `rv_lty` have at that position.
+    /// For example, given
+    ///
+    /// ```
+    /// # fn(
+    /// pl_lty: *mut /*l1*/ *const /*l2*/ u8,
+    /// rv_lty: *mut /*l3*/ *const /*l4*/ u8,
+    /// # ) {}
+    /// ```
+    ///
+    /// this function will unify `l1` with `l3` and `l2` with `l4`.
     fn do_unify(&mut self, pl_lty: LTy<'tcx>, rv_lty: LTy<'tcx>) {
         let rv_ty = self.acx.tcx().erase_regions(rv_lty.ty);
         let pl_ty = self.acx.tcx().erase_regions(pl_lty.ty);

From 26a42754d07bed09659c3431cf748754571bb9c3 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Fri, 17 Feb 2023 16:51:12 -0800
Subject: [PATCH 07/28] (`c2rust-analyze`) Fix the `is_transmutable_to` docs,
 formalizing the expanded defintion of safe transmutability.

---
 c2rust-analyze/src/util.rs | 61 +++++++++++++++++++-------------------
 1 file changed, 30 insertions(+), 31 deletions(-)

diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index 0552ac89d..c2efebf91 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -307,36 +307,33 @@ pub fn lty_project<'tcx, L: Debug>(
     }
 }
 
-/// Determine if `from_ty` can be safely transmuted to `to_ty`.
+/// Determine if `from` can be safely transmuted to `to`,
+/// which is defined as `*(from as *const To)` being a safe operation,
+/// where `from: *const From` and assuming `*from` already was safe.
 ///
-/// Safe transmutability is difficult to check abstractly,
-/// so here it is limited to
-/// * integer types of the same size (but potentially different signedness)
-///     * e.x. `*u8 as *i8`
-/// * decaying arrays and slices to their element type
-///     * e.x. `*[u8; 0] as *u8`
-///     * e.x. `*[u8] as *u8`
+/// Note that this is one-way, and is slightly different from [`core::mem::transmute`],
+/// and more similar to [`core::mem::transmute_copy`].
 ///
-/// Extra (but equal) levels of pointer/reference indirection are allowed,
-/// i.e. `u8 ~ i8` implies `**u8 ~ **i8`.
+/// This forms a non-symmetric (one-way) equivalence relation, named `~` below.
+/// Formally, `A ~ B` iff `*a` and `*(a as *const B)` are safe, where `a: *const A`.
 ///
-/// Thus, [`true`] means it is definitely transmutable,
-/// while [`false`] means it may not be transmutable.
-/// 
-/// Formally, safe transmutability defines
-/// an equivalence relation on types, named `~` here.
-/// `A ~ B` iff `*(a as *const B)` and `*(b as *const A)` are safe,
-/// where `a: *const A` and `b: *const B`.
+/// However, safe transmutability is difficult to check completely,
+/// so this function only checks a subset of it,
+/// with these formal rules for all types `A`, `B`:
 ///
-/// And the current incomplete implementation is defined as:
 /// * `A = B => A ~ B`
 /// * `A ~ B => *A ~ *B`
-/// * `uN ~ iN`, where `N` is an integer width
-pub fn is_transmutable_to<'tcx>(from_ty: Ty<'tcx>, to_ty: Ty<'tcx>) -> bool {
+/// * `uN ~ iN`, `iN ~ uN`, where `N` is an integer width
+/// * `[A] ~ A`
+/// * `[A; N] ~ A`, where `const N: usize`
+///
+/// Thus, [`true`] means it is definitely transmutable,
+/// while [`false`] means it may not be transmutable.
+pub fn is_transmutable_to<'tcx>(from: Ty<'tcx>, to: Ty<'tcx>) -> bool {
     let transmutable_ints = || {
         use IntTy::*;
         use UintTy::*;
-        match (from_ty.kind(), to_ty.kind()) {
+        match (from.kind(), to.kind()) {
             (ty::Uint(u), ty::Int(i)) | (ty::Int(i), ty::Uint(u)) => {
                 matches!((u, i), |(Usize, Isize)| (U8, I8)
                     | (U16, I16)
@@ -347,24 +344,26 @@ pub fn is_transmutable_to<'tcx>(from_ty: Ty<'tcx>, to_ty: Ty<'tcx>) -> bool {
         }
     };
 
-    let one_way_transmutable = || match from_ty.kind() {
-        &ty::Array(from_ty, _) | &ty::Slice(from_ty) => is_transmutable_to(from_ty, to_ty),
+    let one_way_transmutable = || match from.kind() {
+        &ty::Array(from, _) | &ty::Slice(from) => is_transmutable_to(from, to),
         _ => false,
     };
 
-    from_ty == to_ty || is_transmutable_ptr_cast(from_ty, to_ty).unwrap_or(false) || transmutable_ints() || one_way_transmutable()
+    from == to
+        || is_transmutable_ptr_cast(from, to).unwrap_or(false)
+        || transmutable_ints()
+        || one_way_transmutable()
 }
 
-/// Determine if the `from_ty as to_ty` is a ptr-to-ptr cast.
-/// and if it is, if the pointee types are compatible,
-/// i.e. they are safely transmutable.
+/// Determine if `from as to` is a ptr-to-ptr cast.
+/// and if it is, if the pointee types are [safely transmutable](is_transmutable_to).
 ///
 /// This returns [`Some`]`(is_transmutable)` if they're both pointers,
 /// and [`None`] if its some other types.
 ///
 /// See [`is_transmutable_to`] for the definition of safe transmutability.
-pub fn is_transmutable_ptr_cast<'tcx>(from_ty: Ty<'tcx>, to_ty: Ty<'tcx>) -> Option<bool> {
-    let from_ty = from_ty.builtin_deref(true)?.ty;
-    let to_ty = to_ty.builtin_deref(true)?.ty;
-    Some(is_transmutable_to(from_ty, to_ty))
+pub fn is_transmutable_ptr_cast<'tcx>(from: Ty<'tcx>, to: Ty<'tcx>) -> Option<bool> {
+    let from = from.builtin_deref(true)?.ty;
+    let to = to.builtin_deref(true)?.ty;
+    Some(is_transmutable_to(from, to))
 }

From 182b0b5d0fe486a6e05f97462e1076249f2af739 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Sun, 30 Apr 2023 18:15:00 -0700
Subject: [PATCH 08/28] (`c2rust-analyze`) Expand transmutability to unsizing
 casts (`[A] => [A; N]`, `[A; N] => [A]`).

This fixes transmutability-related crashes in `tests/analyze/string_casts.rs`
(which weren't being actually run pre-`merge master` for some reason, and so were untested).
---
 c2rust-analyze/src/util.rs | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index d660c24d1..5e1cb3de1 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -369,9 +369,11 @@ impl<'a, T: ?Sized> PhantomLifetime<'a> for T {}
 ///
 /// * `A = B => A ~ B`
 /// * `A ~ B => *A ~ *B`
+/// * `A ~ B => [A] ~ B`
+/// * `A ~ B => [A; N] ~ B`, where `const N: usize`
+/// * `A ~ B => [A] ~ [B; N]`, where `const N: usize`
+/// * `A ~ B => [A; N] ~ [B]`, where `const N: usize`
 /// * `uN ~ iN`, `iN ~ uN`, where `N` is an integer width
-/// * `[A] ~ A`
-/// * `[A; N] ~ A`, where `const N: usize`
 ///
 /// Thus, [`true`] means it is definitely transmutable,
 /// while [`false`] means it may not be transmutable.
@@ -390,15 +392,19 @@ pub fn is_transmutable_to<'tcx>(from: Ty<'tcx>, to: Ty<'tcx>) -> bool {
         }
     };
 
-    let one_way_transmutable = || match from.kind() {
-        &ty::Array(from, _) | &ty::Slice(from) => is_transmutable_to(from, to),
-        _ => false,
+    let unsizing_transmutable = || {
+        let from = from.builtin_index()?;
+        let transmutable = is_transmutable_to(from, to) || {
+            let to = to.builtin_index()?;
+            is_transmutable_to(from, to)
+        };
+        Some(transmutable)
     };
 
     from == to
         || is_transmutable_ptr_cast(from, to).unwrap_or(false)
         || transmutable_ints()
-        || one_way_transmutable()
+        || unsizing_transmutable().unwrap_or(false)
 }
 
 /// Determine if `from as to` is a ptr-to-ptr cast.

From 32ca464347bf0a3fda80058a960ef080b068e300 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Sun, 30 Apr 2023 18:18:46 -0700
Subject: [PATCH 09/28] (`c2rust-analyze/tests`) Enable the `cast_from_literal`
 test now that string literals are also working (#886, #902).

---
 c2rust-analyze/tests/analyze/string_casts.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/c2rust-analyze/tests/analyze/string_casts.rs b/c2rust-analyze/tests/analyze/string_casts.rs
index abe0fbb86..fbb20a20f 100644
--- a/c2rust-analyze/tests/analyze/string_casts.rs
+++ b/c2rust-analyze/tests/analyze/string_casts.rs
@@ -18,7 +18,6 @@ pub fn cast_array_to_ptr(s: &[u8; 0]) {
     s as *const u8;
 }
 
-#[cfg(any())]
 pub fn cast_from_literal() {
     b"" as *const u8 as *const core::ffi::c_char;
 }

From 9a7c50118f95d5fc081e8fc67a3ab1a7602c5ab1 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Sun, 30 Apr 2023 18:28:23 -0700
Subject: [PATCH 10/28] (`c2rust-analyze`) Revert the use of
 `is_transmutable_to` in `TypeChecker::do_unify` (back to strict equality) as
 #883 resolved this
 (https://github.com/immunant/c2rust/pull/839#discussion_r1115160479).

---
 c2rust-analyze/src/dataflow/type_check.rs | 22 +++++++++-------------
 1 file changed, 9 insertions(+), 13 deletions(-)

diff --git a/c2rust-analyze/src/dataflow/type_check.rs b/c2rust-analyze/src/dataflow/type_check.rs
index 7a4478c66..cb0123ef5 100644
--- a/c2rust-analyze/src/dataflow/type_check.rs
+++ b/c2rust-analyze/src/dataflow/type_check.rs
@@ -2,8 +2,7 @@ use super::DataflowConstraints;
 use crate::c_void_casts::CVoidCastDirection;
 use crate::context::{AnalysisCtxt, LTy, PermissionSet, PointerId};
 use crate::util::{
-    describe_rvalue, is_null_const, is_transmutable_ptr_cast, is_transmutable_to, ty_callee,
-    Callee, RvalueDesc,
+    describe_rvalue, is_null_const, is_transmutable_ptr_cast, ty_callee, Callee, RvalueDesc,
 };
 use assert_matches::assert_matches;
 use rustc_hir::def_id::DefId;
@@ -276,7 +275,7 @@ impl<'tcx> TypeChecker<'tcx, '_> {
 
     /// Unify corresponding [`PointerId`]s in `pl_lty` and `rv_lty`.
     ///
-    /// The two inputs must have compatible ([safely transmutable](is_transmutable_to)) underlying types.
+    /// The two inputs must have identical underlying types.
     /// For any position where the underlying type has a pointer,
     /// this function unifies the [`PointerId`]s that `pl_lty` and `rv_lty` have at that position.
     /// For example, given
@@ -292,16 +291,13 @@ impl<'tcx> TypeChecker<'tcx, '_> {
     fn do_unify(&mut self, pl_lty: LTy<'tcx>, rv_lty: LTy<'tcx>) {
         let rv_ty = self.acx.tcx().erase_regions(rv_lty.ty);
         let pl_ty = self.acx.tcx().erase_regions(pl_lty.ty);
-        assert!(
-            is_transmutable_to(rv_ty, pl_ty),
-            "types not transmutable (compatible), so PointerId unification cannot be done: *{rv_ty:?} as *{pl_ty:?}",
-        );
-        for (sub_lty1, sub_lty2) in pl_lty.iter().zip(rv_lty.iter()) {
-            eprintln!("equate {:?} = {:?}", sub_lty1, sub_lty2);
-            if sub_lty1.label != PointerId::NONE || sub_lty2.label != PointerId::NONE {
-                assert!(sub_lty1.label != PointerId::NONE);
-                assert!(sub_lty2.label != PointerId::NONE);
-                self.add_equiv(sub_lty1.label, sub_lty2.label);
+        assert_eq!(rv_ty, pl_ty);
+        for (sub_pl_lty, sub_rv_lty) in pl_lty.iter().zip(rv_lty.iter()) {
+            eprintln!("equate {:?} = {:?}", sub_pl_lty, sub_rv_lty);
+            if sub_pl_lty.label != PointerId::NONE || sub_rv_lty.label != PointerId::NONE {
+                assert!(sub_pl_lty.label != PointerId::NONE);
+                assert!(sub_rv_lty.label != PointerId::NONE);
+                self.add_equiv(sub_pl_lty.label, sub_rv_lty.label);
             }
         }
     }

From 2d45f80693e630470ea505f89b5e2479c5a49439 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Mon, 1 May 2023 13:52:42 -0700
Subject: [PATCH 11/28] (`c2rust-analyze`) Add back the unsizing cast dataflow
 constraint from #883.  It's not complete, but fixes the crash in `as_ptr.rs`.

---
 c2rust-analyze/src/dataflow/type_check.rs | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/c2rust-analyze/src/dataflow/type_check.rs b/c2rust-analyze/src/dataflow/type_check.rs
index cb0123ef5..9b54745e1 100644
--- a/c2rust-analyze/src/dataflow/type_check.rs
+++ b/c2rust-analyze/src/dataflow/type_check.rs
@@ -10,6 +10,7 @@ use rustc_middle::mir::{
     AggregateKind, BinOp, Body, CastKind, Location, Mutability, Operand, Place, PlaceRef,
     ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
 };
+use rustc_middle::ty::adjustment::PointerCast;
 use rustc_middle::ty::{SubstsRef, Ty, TyKind};
 
 /// Visitor that walks over the MIR, computing types of rvalues/operands/places and generating
@@ -111,11 +112,15 @@ impl<'tcx> TypeChecker<'tcx, '_> {
                 }
             }
             _ => {
-                // TODO add dataflow constraints
                 match is_transmutable_ptr_cast(from_ty, to_ty) {
-                    Some(true) => {},
+                    Some(true) => {
+                        if cast_kind == CastKind::Pointer(PointerCast::Unsize) {
+                            self.do_assign_pointer_ids(to_lty.label, from_lty.label)
+                        }
+                        // TODO add other dataflow constraints
+                    },
                     Some(false) => ::log::error!("TODO: unsupported ptr-to-ptr cast between pointee types not yet supported as safely transmutable: `{from_ty:?} as {to_ty:?}`"),
-                    None => {}, // not a ptr cast; let rustc typeck this
+                    None => {}, // not a ptr cast (no dataflow constraints needed); let rustc typeck this
                 };
             }
         }

From 14824a1f7d57b8a26348fe2bdb538f2a5e1ca154 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Tue, 2 May 2023 02:27:34 -0700
Subject: [PATCH 12/28] (`c2rust-analyze/tests`) Disable the failing string
 casts tests.

---
 c2rust-analyze/tests/analyze/string_casts.rs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/c2rust-analyze/tests/analyze/string_casts.rs b/c2rust-analyze/tests/analyze/string_casts.rs
index fbb20a20f..ea8e08172 100644
--- a/c2rust-analyze/tests/analyze/string_casts.rs
+++ b/c2rust-analyze/tests/analyze/string_casts.rs
@@ -10,14 +10,17 @@ pub fn cast_slice_ptr_to_ptr(s: *const [u8]) {
     s as *const u8;
 }
 
+#[cfg(any())]
 pub fn cast_array_to_slice_ptr(s: &[u8; 0]) {
     s as *const [u8];
 }
 
+#[cfg(any())]
 pub fn cast_array_to_ptr(s: &[u8; 0]) {
     s as *const u8;
 }
 
+#[cfg(any())]
 pub fn cast_from_literal() {
     b"" as *const u8 as *const core::ffi::c_char;
 }

From 95767c34eb61eee8619236fe27e676af06af136a Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Tue, 2 May 2023 02:28:41 -0700
Subject: [PATCH 13/28] (`c2rust-analyze/tests`) Add an explicit (in terms of
 `addr_of!`) version of the `cast_array_to_ptr` test.  The other disabled
 tests still didn't work with the same approach.

---
 c2rust-analyze/tests/analyze/string_casts.rs | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/c2rust-analyze/tests/analyze/string_casts.rs b/c2rust-analyze/tests/analyze/string_casts.rs
index ea8e08172..a2784312e 100644
--- a/c2rust-analyze/tests/analyze/string_casts.rs
+++ b/c2rust-analyze/tests/analyze/string_casts.rs
@@ -20,6 +20,19 @@ pub fn cast_array_to_ptr(s: &[u8; 0]) {
     s as *const u8;
 }
 
+/// An explicit version of `cast_array_to_ptr` above
+/// where we use an explicit `std::ptr::addr_of!`
+/// instead of having one inserted.
+/// The rewriter can only currently handle explicit ones.
+///
+/// Also note that `addr_of!` (with a `use std::ptr::addr_of`)
+/// and `::core::ptr::addr_of!` don't work either,
+/// though `std::ptr::addr_of`, `::std::ptr::addr_of!`,
+/// and `core::ptr::addr_of!` do work.
+pub fn cast_array_to_ptr_explicit(s: &[u8; 0]) {
+    std::ptr::addr_of!(*s) as *const u8;
+}
+
 #[cfg(any())]
 pub fn cast_from_literal() {
     b"" as *const u8 as *const core::ffi::c_char;

From e41cec17c237135bd767bd94e01d1e2e552d9779 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Tue, 2 May 2023 11:52:02 -0700
Subject: [PATCH 14/28] (`c2rust-analyze/tests`) Add an explicit version of the
 `cast_from_literal` test.

---
 c2rust-analyze/tests/analyze/string_casts.rs | 22 ++++++++++++--------
 1 file changed, 13 insertions(+), 9 deletions(-)

diff --git a/c2rust-analyze/tests/analyze/string_casts.rs b/c2rust-analyze/tests/analyze/string_casts.rs
index a2784312e..3d6e1cc3d 100644
--- a/c2rust-analyze/tests/analyze/string_casts.rs
+++ b/c2rust-analyze/tests/analyze/string_casts.rs
@@ -10,6 +10,15 @@ pub fn cast_slice_ptr_to_ptr(s: *const [u8]) {
     s as *const u8;
 }
 
+/// For the below disabled (`#[cfg(any())]`ed) tests, they currently crash in the rewriter
+/// due to it not being able to handle implicitly inserted `std::ptr::addr_of!`s yet.
+/// Thus, they also have `*_explicit` versions where the `addr_of!` is made explicit.
+///
+/// Also note that `addr_of!` (with a `use std::ptr::addr_of`)
+/// and `::core::ptr::addr_of!` don't work either,
+/// though `std::ptr::addr_of`, `::std::ptr::addr_of!`,
+/// and `core::ptr::addr_of!` do work.
+
 #[cfg(any())]
 pub fn cast_array_to_slice_ptr(s: &[u8; 0]) {
     s as *const [u8];
@@ -20,15 +29,6 @@ pub fn cast_array_to_ptr(s: &[u8; 0]) {
     s as *const u8;
 }
 
-/// An explicit version of `cast_array_to_ptr` above
-/// where we use an explicit `std::ptr::addr_of!`
-/// instead of having one inserted.
-/// The rewriter can only currently handle explicit ones.
-///
-/// Also note that `addr_of!` (with a `use std::ptr::addr_of`)
-/// and `::core::ptr::addr_of!` don't work either,
-/// though `std::ptr::addr_of`, `::std::ptr::addr_of!`,
-/// and `core::ptr::addr_of!` do work.
 pub fn cast_array_to_ptr_explicit(s: &[u8; 0]) {
     std::ptr::addr_of!(*s) as *const u8;
 }
@@ -37,3 +37,7 @@ pub fn cast_array_to_ptr_explicit(s: &[u8; 0]) {
 pub fn cast_from_literal() {
     b"" as *const u8 as *const core::ffi::c_char;
 }
+
+pub fn cast_from_literal_explicit() {
+    std::ptr::addr_of!(*b"") as *const u8 as *const core::ffi::c_char;
+}

From 2915b8d0c71add21dee1f9d540958ea863478212 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Tue, 2 May 2023 11:55:04 -0700
Subject: [PATCH 15/28] (`c2rust-analyze/tests`) Add a disabled
 `cast_array_to_slice_ptr_explicit` test b/c it still doesn't work even
 explicitly.

---
 c2rust-analyze/tests/analyze/string_casts.rs | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/c2rust-analyze/tests/analyze/string_casts.rs b/c2rust-analyze/tests/analyze/string_casts.rs
index 3d6e1cc3d..c7a0bfa94 100644
--- a/c2rust-analyze/tests/analyze/string_casts.rs
+++ b/c2rust-analyze/tests/analyze/string_casts.rs
@@ -24,6 +24,13 @@ pub fn cast_array_to_slice_ptr(s: &[u8; 0]) {
     s as *const [u8];
 }
 
+/// Unlike the other `*_explicit` tests, this one
+/// still doesn't work even with an explicit `std::ptr::addr_of!`.
+#[cfg(any())]
+pub fn cast_array_to_slice_ptr_explicit(s: &[u8; 0]) {
+    std::ptr::addr_of!(*s) as *const [u8];
+}
+
 #[cfg(any())]
 pub fn cast_array_to_ptr(s: &[u8; 0]) {
     s as *const u8;

From 11bf3514929133cd5ee44fe4eb5956bb0e4c07e8 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Tue, 2 May 2023 12:06:31 -0700
Subject: [PATCH 16/28] (`c2rust-analyze/test`) Reword explanation of explicit
 string cast tests to specify `&raw` MIR statements, inserted with
 `addr_of!`s.

---
 c2rust-analyze/tests/analyze/string_casts.rs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/c2rust-analyze/tests/analyze/string_casts.rs b/c2rust-analyze/tests/analyze/string_casts.rs
index c7a0bfa94..99043ea39 100644
--- a/c2rust-analyze/tests/analyze/string_casts.rs
+++ b/c2rust-analyze/tests/analyze/string_casts.rs
@@ -11,8 +11,9 @@ pub fn cast_slice_ptr_to_ptr(s: *const [u8]) {
 }
 
 /// For the below disabled (`#[cfg(any())]`ed) tests, they currently crash in the rewriter
-/// due to it not being able to handle implicitly inserted `std::ptr::addr_of!`s yet.
-/// Thus, they also have `*_explicit` versions where the `addr_of!` is made explicit.
+/// due to it not being able to handle implicitly inserted `&raw` MIR statements yet.
+/// Thus, they also have `*_explicit` versions where
+/// a `std::ptr::addr_of!` is used to make the `&raw` explicit.
 ///
 /// Also note that `addr_of!` (with a `use std::ptr::addr_of`)
 /// and `::core::ptr::addr_of!` don't work either,

From 65e51406868ad4829d8c93a12ba4743c16c4821b Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Fri, 5 May 2023 11:27:08 -0700
Subject: [PATCH 17/28] (`c2rust-analyze`) Remove the leading `|` in a
 `matches!` so `rustfmt` formats it reasonably.

---
 c2rust-analyze/src/util.rs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index 5e1cb3de1..72478a290 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -383,10 +383,10 @@ pub fn is_transmutable_to<'tcx>(from: Ty<'tcx>, to: Ty<'tcx>) -> bool {
         use UintTy::*;
         match (from.kind(), to.kind()) {
             (ty::Uint(u), ty::Int(i)) | (ty::Int(i), ty::Uint(u)) => {
-                matches!((u, i), |(Usize, Isize)| (U8, I8)
-                    | (U16, I16)
-                    | (U32, I32)
-                    | (U64, I64))
+                matches!(
+                    (u, i),
+                    (Usize, Isize) | (U8, I8) | (U16, I16) | (U32, I32) | (U64, I64)
+                )
             }
             _ => false,
         }

From 44ac9f497b0d073104e625c228a8cedf20f11ac9 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Fri, 5 May 2023 11:31:46 -0700
Subject: [PATCH 18/28] (`c2rust-analyze`) Replace "equivalance relation" with
 "reflexive, transitive" since it's non-symmetric, and equivalance relations
 are symmetric.

---
 c2rust-analyze/src/util.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index 72478a290..ba02707ab 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -360,7 +360,7 @@ impl<'a, T: ?Sized> PhantomLifetime<'a> for T {}
 /// Note that this is one-way, and is slightly different from [`core::mem::transmute`],
 /// and more similar to [`core::mem::transmute_copy`].
 ///
-/// This forms a non-symmetric (one-way) equivalence relation, named `~` below.
+/// This forms a reflexive, transitive, and non-symmetric (one-way) relation, named `~` below.
 /// Formally, `A ~ B` iff `*a` and `*(a as *const B)` are safe, where `a: *const A`.
 ///
 /// However, safe transmutability is difficult to check completely,

From 4bbb3065d6f8aa4961701fdab5cb6ffae21a823f Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Mon, 22 May 2023 13:32:06 -0700
Subject: [PATCH 19/28] (`c2rust-analyze`) Separate handling of `CastKind`s and
 only check safe transmutability for `CastKind::Misc`, which are the only
 non-type-checked ptr casts.

Note that `CastKind::Pointer(PointerCast::Unsize)` needs different rules than safe transmutability.
These rules are implemented by typeck, so there's no reason re-implementing that,
but we can't include them in transmutability (will be removed in the next commit).
---
 c2rust-analyze/src/dataflow/type_check.rs | 31 ++++++++++++++++++++---
 1 file changed, 27 insertions(+), 4 deletions(-)

diff --git a/c2rust-analyze/src/dataflow/type_check.rs b/c2rust-analyze/src/dataflow/type_check.rs
index 9b54745e1..4b7eef134 100644
--- a/c2rust-analyze/src/dataflow/type_check.rs
+++ b/c2rust-analyze/src/dataflow/type_check.rs
@@ -111,12 +111,35 @@ impl<'tcx> TypeChecker<'tcx, '_> {
                     panic!("Creating non-null pointers from exposed addresses not supported");
                 }
             }
-            _ => {
+            CastKind::PointerExposeAddress => {
+                // Allow, as [`CastKind::PointerFromExposedAddress`] is the dangerous one,
+                // and we'll catch (not allow) that above.
+                // This becomes no longer a pointer, so we don't need to add any dataflow constraints
+                // (until we try to handle [`CastKind::PointerFromExposedAddress`], if we do).
+            }
+            CastKind::Pointer(ptr_cast) => {
+                // All of these [`PointerCast`]s are type checked by rustc already.
+                // They don't involve arbitrary raw ptr to raw ptr casts
+                // ([PointerCast::MutToConstPointer`] doesn't allow changing types),
+                // which we need to check for safe transmutability,
+                // and which are (currently) covered in [`CastKind::Misc`].
+                // That's why there's a `match` here that does nothing;
+                // it ensures if [`PointerCast`] is changed in a future `rustc` version,
+                // this won't compile until we've checked that this reasoning is still accurate.
+                match ptr_cast {
+                    PointerCast::ReifyFnPointer => {}
+                    PointerCast::UnsafeFnPointer => {}
+                    PointerCast::ClosureFnPointer(_) => {}
+                    PointerCast::MutToConstPointer => {}
+                    PointerCast::ArrayToPointer => {}
+                    PointerCast::Unsize => {}
+                }
+                self.do_assign_pointer_ids(to_lty.label, from_lty.label)
+                // TODO add other dataflow constraints
+            }
+            CastKind::Misc => {
                 match is_transmutable_ptr_cast(from_ty, to_ty) {
                     Some(true) => {
-                        if cast_kind == CastKind::Pointer(PointerCast::Unsize) {
-                            self.do_assign_pointer_ids(to_lty.label, from_lty.label)
-                        }
                         // TODO add other dataflow constraints
                     },
                     Some(false) => ::log::error!("TODO: unsupported ptr-to-ptr cast between pointee types not yet supported as safely transmutable: `{from_ty:?} as {to_ty:?}`"),

From 720c2fbb841a4cf83460c59db64b18256c280ebc Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Mon, 22 May 2023 13:32:31 -0700
Subject: [PATCH 20/28] Revert "(`c2rust-analyze`) Expand transmutability to
 unsizing casts (`[A] => [A; N]`, `[A; N] => [A]`)."

This reverts commit 182b0b5d0fe486a6e05f97462e1076249f2af739.
---
 c2rust-analyze/src/util.rs | 18 ++++++------------
 1 file changed, 6 insertions(+), 12 deletions(-)

diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index ba02707ab..8d8c574a0 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -369,11 +369,9 @@ impl<'a, T: ?Sized> PhantomLifetime<'a> for T {}
 ///
 /// * `A = B => A ~ B`
 /// * `A ~ B => *A ~ *B`
-/// * `A ~ B => [A] ~ B`
-/// * `A ~ B => [A; N] ~ B`, where `const N: usize`
-/// * `A ~ B => [A] ~ [B; N]`, where `const N: usize`
-/// * `A ~ B => [A; N] ~ [B]`, where `const N: usize`
 /// * `uN ~ iN`, `iN ~ uN`, where `N` is an integer width
+/// * `[A] ~ A`
+/// * `[A; N] ~ A`, where `const N: usize`
 ///
 /// Thus, [`true`] means it is definitely transmutable,
 /// while [`false`] means it may not be transmutable.
@@ -392,19 +390,15 @@ pub fn is_transmutable_to<'tcx>(from: Ty<'tcx>, to: Ty<'tcx>) -> bool {
         }
     };
 
-    let unsizing_transmutable = || {
-        let from = from.builtin_index()?;
-        let transmutable = is_transmutable_to(from, to) || {
-            let to = to.builtin_index()?;
-            is_transmutable_to(from, to)
-        };
-        Some(transmutable)
+    let one_way_transmutable = || match from.kind() {
+        &ty::Array(from, _) | &ty::Slice(from) => is_transmutable_to(from, to),
+        _ => false,
     };
 
     from == to
         || is_transmutable_ptr_cast(from, to).unwrap_or(false)
         || transmutable_ints()
-        || unsizing_transmutable().unwrap_or(false)
+        || one_way_transmutable()
 }
 
 /// Determine if `from as to` is a ptr-to-ptr cast.

From df1d63d4928592028b185548a3f5f7d38ebdd366 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Mon, 22 May 2023 13:35:01 -0700
Subject: [PATCH 21/28] (`c2rust-analyze/tests`) Remove the
 `cast_array_to_slice_ptr` tests as that cast is unsound and has been removed
 from transmutability in the last commit.

---
 c2rust-analyze/tests/analyze/string_casts.rs | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/c2rust-analyze/tests/analyze/string_casts.rs b/c2rust-analyze/tests/analyze/string_casts.rs
index 99043ea39..ea0b79fde 100644
--- a/c2rust-analyze/tests/analyze/string_casts.rs
+++ b/c2rust-analyze/tests/analyze/string_casts.rs
@@ -20,18 +20,6 @@ pub fn cast_slice_ptr_to_ptr(s: *const [u8]) {
 /// though `std::ptr::addr_of`, `::std::ptr::addr_of!`,
 /// and `core::ptr::addr_of!` do work.
 
-#[cfg(any())]
-pub fn cast_array_to_slice_ptr(s: &[u8; 0]) {
-    s as *const [u8];
-}
-
-/// Unlike the other `*_explicit` tests, this one
-/// still doesn't work even with an explicit `std::ptr::addr_of!`.
-#[cfg(any())]
-pub fn cast_array_to_slice_ptr_explicit(s: &[u8; 0]) {
-    std::ptr::addr_of!(*s) as *const [u8];
-}
-
 #[cfg(any())]
 pub fn cast_array_to_ptr(s: &[u8; 0]) {
     s as *const u8;

From a73e64d53985c42fda66b55030ce7fecdd3a37e4 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Thu, 8 Jun 2023 12:31:12 -0700
Subject: [PATCH 22/28] (`c2rust-analyze`) Adjust wording on safe
 transmutability definition to use well-defined instead of safe and to use
 "implies" instead of "and".

---
 c2rust-analyze/src/util.rs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index 372c8c587..70ecbe6ca 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -363,7 +363,8 @@ impl<'a, T: ?Sized> PhantomLifetime<'a> for T {}
 /// and more similar to [`core::mem::transmute_copy`].
 ///
 /// This forms a reflexive, transitive, and non-symmetric (one-way) relation, named `~` below.
-/// Formally, `A ~ B` iff `*a` and `*(a as *const B)` are safe, where `a: *const A`.
+/// Formally, `A ~ B` iff whenever `*a` is well-defined (i.e., not UB),
+/// `*(a as *const B)` is also well-defined, where `a: *const A`.
 ///
 /// However, safe transmutability is difficult to check completely,
 /// so this function only checks a subset of it,

From 435e399677662f5bc8a9ae4846b55f8626affeb4 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Thu, 8 Jun 2023 12:37:19 -0700
Subject: [PATCH 23/28] (`c2rust-analyze`) Revert the arg names of `do_unify`
 to `lty{1,2}` from `{pl,rv}_lty`, as they are interchangeable.

---
 c2rust-analyze/src/dataflow/type_check.rs | 29 ++++++++++++-----------
 1 file changed, 15 insertions(+), 14 deletions(-)

diff --git a/c2rust-analyze/src/dataflow/type_check.rs b/c2rust-analyze/src/dataflow/type_check.rs
index 4c7b9291a..5472bb9b9 100644
--- a/c2rust-analyze/src/dataflow/type_check.rs
+++ b/c2rust-analyze/src/dataflow/type_check.rs
@@ -302,31 +302,32 @@ impl<'tcx> TypeChecker<'tcx, '_> {
         }
     }
 
-    /// Unify corresponding [`PointerId`]s in `pl_lty` and `rv_lty`.
+    /// Unify corresponding [`PointerId`]s in `lty1` and `lty2`.
     ///
     /// The two inputs must have identical underlying types.
     /// For any position where the underlying type has a pointer,
-    /// this function unifies the [`PointerId`]s that `pl_lty` and `rv_lty` have at that position.
+    /// this function unifies the [`PointerId`]s that `lty1` and `lty2` have at that position.
     /// For example, given
     ///
     /// ```
     /// # fn(
-    /// pl_lty: *mut /*l1*/ *const /*l2*/ u8,
-    /// rv_lty: *mut /*l3*/ *const /*l4*/ u8,
+    /// lty1: *mut /*l1*/ *const /*l2*/ u8,
+    /// lty2: *mut /*l3*/ *const /*l4*/ u8,
     /// # ) {}
     /// ```
     ///
     /// this function will unify `l1` with `l3` and `l2` with `l4`.
-    fn do_unify(&mut self, pl_lty: LTy<'tcx>, rv_lty: LTy<'tcx>) {
-        let rv_ty = self.acx.tcx().erase_regions(rv_lty.ty);
-        let pl_ty = self.acx.tcx().erase_regions(pl_lty.ty);
-        assert_eq!(rv_ty, pl_ty);
-        for (sub_pl_lty, sub_rv_lty) in pl_lty.iter().zip(rv_lty.iter()) {
-            eprintln!("equate {:?} = {:?}", sub_pl_lty, sub_rv_lty);
-            if sub_pl_lty.label != PointerId::NONE || sub_rv_lty.label != PointerId::NONE {
-                assert!(sub_pl_lty.label != PointerId::NONE);
-                assert!(sub_rv_lty.label != PointerId::NONE);
-                self.add_equiv(sub_pl_lty.label, sub_rv_lty.label);
+    fn do_unify(&mut self, lty1: LTy<'tcx>, lty2: LTy<'tcx>) {
+        assert_eq!(
+            self.acx.tcx().erase_regions(lty1.ty),
+            self.acx.tcx().erase_regions(lty2.ty)
+        );
+        for (sub_lty1, sub_lty2) in lty1.iter().zip(lty2.iter()) {
+            eprintln!("equate {:?} = {:?}", sub_lty1, sub_lty2);
+            if sub_lty1.label != PointerId::NONE || sub_lty2.label != PointerId::NONE {
+                assert!(sub_lty1.label != PointerId::NONE);
+                assert!(sub_lty2.label != PointerId::NONE);
+                self.add_equiv(sub_lty1.label, sub_lty2.label);
             }
         }
     }

From 1317e034b6c8fe847ff693e8f8f44ce74a4bc83b Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Thu, 8 Jun 2023 12:54:25 -0700
Subject: [PATCH 24/28] (`c2rust-analyze`) Update safe transmutability rules to
 add `A ~ B =>` to the slice and array rules.

---
 c2rust-analyze/src/util.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index 70ecbe6ca..6d8c90c15 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -373,8 +373,8 @@ impl<'a, T: ?Sized> PhantomLifetime<'a> for T {}
 /// * `A = B => A ~ B`
 /// * `A ~ B => *A ~ *B`
 /// * `uN ~ iN`, `iN ~ uN`, where `N` is an integer width
-/// * `[A] ~ A`
-/// * `[A; N] ~ A`, where `const N: usize`
+/// * `A ~ B => [A] ~ B`
+/// * `A ~ B => [A; N] ~ B`, where `const N: usize`
 ///
 /// Thus, [`true`] means it is definitely transmutable,
 /// while [`false`] means it may not be transmutable.

From 60a4376536205b2003dff277231193cc5a2ed88d Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Thu, 8 Jun 2023 13:27:28 -0700
Subject: [PATCH 25/28] (`c2rust-analyze`) For the array safe transmutability
 rule, require than `N > 0` to avoid ZSTs, as then the rule would be unsound.

---
 c2rust-analyze/src/util.rs                   | 16 +++++++++++++---
 c2rust-analyze/tests/analyze/string_casts.rs |  8 ++++----
 c2rust-analyze/tests/filecheck/addr_of.rs    |  4 ++--
 3 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index 6d8c90c15..fd25803fb 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -374,7 +374,7 @@ impl<'a, T: ?Sized> PhantomLifetime<'a> for T {}
 /// * `A ~ B => *A ~ *B`
 /// * `uN ~ iN`, `iN ~ uN`, where `N` is an integer width
 /// * `A ~ B => [A] ~ B`
-/// * `A ~ B => [A; N] ~ B`, where `const N: usize`
+/// * `A ~ B, N > 0 => [A; N] ~ B`, where `const N: usize`
 ///
 /// Thus, [`true`] means it is definitely transmutable,
 /// while [`false`] means it may not be transmutable.
@@ -393,8 +393,18 @@ pub fn is_transmutable_to<'tcx>(from: Ty<'tcx>, to: Ty<'tcx>) -> bool {
         }
     };
 
-    let one_way_transmutable = || match from.kind() {
-        &ty::Array(from, _) | &ty::Slice(from) => is_transmutable_to(from, to),
+    let one_way_transmutable = || match *from.kind() {
+        ty::Array(from, n) => {
+            is_transmutable_to(from, to) && {
+                let is_zero = n
+                    .kind()
+                    .try_to_scalar_int()
+                    .map(|i| i.is_null())
+                    .unwrap_or(false);
+                !is_zero
+            }
+        }
+        ty::Slice(from) => is_transmutable_to(from, to),
         _ => false,
     };
 
diff --git a/c2rust-analyze/tests/analyze/string_casts.rs b/c2rust-analyze/tests/analyze/string_casts.rs
index ea0b79fde..164f9f33d 100644
--- a/c2rust-analyze/tests/analyze/string_casts.rs
+++ b/c2rust-analyze/tests/analyze/string_casts.rs
@@ -21,19 +21,19 @@ pub fn cast_slice_ptr_to_ptr(s: *const [u8]) {
 /// and `core::ptr::addr_of!` do work.
 
 #[cfg(any())]
-pub fn cast_array_to_ptr(s: &[u8; 0]) {
+pub fn cast_array_to_ptr(s: &[u8; 1]) {
     s as *const u8;
 }
 
-pub fn cast_array_to_ptr_explicit(s: &[u8; 0]) {
+pub fn cast_array_to_ptr_explicit(s: &[u8; 1]) {
     std::ptr::addr_of!(*s) as *const u8;
 }
 
 #[cfg(any())]
 pub fn cast_from_literal() {
-    b"" as *const u8 as *const core::ffi::c_char;
+    b"\0" as *const u8 as *const core::ffi::c_char;
 }
 
 pub fn cast_from_literal_explicit() {
-    std::ptr::addr_of!(*b"") as *const u8 as *const core::ffi::c_char;
+    std::ptr::addr_of!(*b"\0") as *const u8 as *const core::ffi::c_char;
 }
diff --git a/c2rust-analyze/tests/filecheck/addr_of.rs b/c2rust-analyze/tests/filecheck/addr_of.rs
index fdc3b2fbf..ca6823e1c 100644
--- a/c2rust-analyze/tests/filecheck/addr_of.rs
+++ b/c2rust-analyze/tests/filecheck/addr_of.rs
@@ -25,8 +25,8 @@ fn shared_ref_with_struct() {
     let y = std::ptr::addr_of!(x.a);
 }
 
-// CHECK-LABEL: fn cast_array_to_ptr_explicit(s: &[u8; 0]) {
-pub fn cast_array_to_ptr_explicit(s: &[u8; 0]) {
+// CHECK-LABEL: fn cast_array_to_ptr_explicit(s: &[u8; 1]) {
+pub fn cast_array_to_ptr_explicit(s: &[u8; 1]) {
     // For now, this doesn't get rewritten - we're just checking that the analysis doesn't panic.
     // CHECK-DAG: std::ptr::addr_of!(*s) as *const u8
     std::ptr::addr_of!(*s) as *const u8;

From 9b43bd63297694fc08ff4fff94f03322a0eb5bef Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Thu, 8 Jun 2023 13:32:22 -0700
Subject: [PATCH 26/28] (`c2rust-analyze`) Remove the slice rule for safe
 transmutability, as it's only sound for non-empty slices, but we can't check
 that at compile-time.

---
 c2rust-analyze/src/util.rs                   | 5 +++--
 c2rust-analyze/tests/analyze/string_casts.rs | 4 ----
 2 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index fd25803fb..b78eb72e1 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -373,9 +373,11 @@ impl<'a, T: ?Sized> PhantomLifetime<'a> for T {}
 /// * `A = B => A ~ B`
 /// * `A ~ B => *A ~ *B`
 /// * `uN ~ iN`, `iN ~ uN`, where `N` is an integer width
-/// * `A ~ B => [A] ~ B`
 /// * `A ~ B, N > 0 => [A; N] ~ B`, where `const N: usize`
 ///
+/// Note: `A ~ B => [A] ~ B` is not a rule because it would be unsound for zero-length slices,
+/// which we cannot check unlike for arrays, which we need for translated string literals.
+///
 /// Thus, [`true`] means it is definitely transmutable,
 /// while [`false`] means it may not be transmutable.
 pub fn is_transmutable_to<'tcx>(from: Ty<'tcx>, to: Ty<'tcx>) -> bool {
@@ -404,7 +406,6 @@ pub fn is_transmutable_to<'tcx>(from: Ty<'tcx>, to: Ty<'tcx>) -> bool {
                 !is_zero
             }
         }
-        ty::Slice(from) => is_transmutable_to(from, to),
         _ => false,
     };
 
diff --git a/c2rust-analyze/tests/analyze/string_casts.rs b/c2rust-analyze/tests/analyze/string_casts.rs
index 164f9f33d..ea0c837a5 100644
--- a/c2rust-analyze/tests/analyze/string_casts.rs
+++ b/c2rust-analyze/tests/analyze/string_casts.rs
@@ -6,10 +6,6 @@ pub fn deep_cast_ptr_to_ptr(x: *const *const u8) {
     x as *const *const i8;
 }
 
-pub fn cast_slice_ptr_to_ptr(s: *const [u8]) {
-    s as *const u8;
-}
-
 /// For the below disabled (`#[cfg(any())]`ed) tests, they currently crash in the rewriter
 /// due to it not being able to handle implicitly inserted `&raw` MIR statements yet.
 /// Thus, they also have `*_explicit` versions where

From 355b56bb756c62c5a53032c0947ee3269ce2dcd8 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Fri, 9 Jun 2023 00:07:40 -0700
Subject: [PATCH 27/28] (`c2rust-analyze`) `.unwrap()` on
 `.try_to_scalar_int()` for array length `Const`s.

---
 c2rust-analyze/src/util.rs | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index b78eb72e1..c45847165 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -398,11 +398,7 @@ pub fn is_transmutable_to<'tcx>(from: Ty<'tcx>, to: Ty<'tcx>) -> bool {
     let one_way_transmutable = || match *from.kind() {
         ty::Array(from, n) => {
             is_transmutable_to(from, to) && {
-                let is_zero = n
-                    .kind()
-                    .try_to_scalar_int()
-                    .map(|i| i.is_null())
-                    .unwrap_or(false);
+                let is_zero = n.kind().try_to_scalar_int().unwrap().is_null();
                 !is_zero
             }
         }

From 7f87dc1ece162561e675d185a25e9ede4b3bf459 Mon Sep 17 00:00:00 2001
From: Khyber Sen <kkysen@gmail.com>
Date: Fri, 9 Jun 2023 00:25:13 -0700
Subject: [PATCH 28/28] (`c2rust-analyze`) Add fat ptr analysis/proof to safe
 transmutability docs.

---
 c2rust-analyze/src/util.rs | 25 ++++++++++++++++++++-----
 1 file changed, 20 insertions(+), 5 deletions(-)

diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs
index c45847165..0975ccc47 100644
--- a/c2rust-analyze/src/util.rs
+++ b/c2rust-analyze/src/util.rs
@@ -370,16 +370,31 @@ impl<'a, T: ?Sized> PhantomLifetime<'a> for T {}
 /// so this function only checks a subset of it,
 /// with these formal rules for all types `A`, `B`:
 ///
-/// * `A = B => A ~ B`
-/// * `A ~ B => *A ~ *B`
-/// * `uN ~ iN`, `iN ~ uN`, where `N` is an integer width
-/// * `A ~ B, N > 0 => [A; N] ~ B`, where `const N: usize`
+/// 1. `A = B => A ~ B`
+/// 2. `A ~ B => *A ~ *B`
+/// 3. `uN ~ iN`, `iN ~ uN`, where `N` is an integer width
+/// 4. `A ~ B, N > 0 => [A; N] ~ B`, where `const N: usize`
 ///
-/// Note: `A ~ B => [A] ~ B` is not a rule because it would be unsound for zero-length slices,
+/// Note: 5. `A ~ B => [A] ~ B` is not a rule because it would be unsound for zero-length slices,
 /// which we cannot check unlike for arrays, which we need for translated string literals.
 ///
 /// Thus, [`true`] means it is definitely transmutable,
 /// while [`false`] means it may not be transmutable.
+///
+/// Also note that for `A ~ B`, we need at least
+/// * `size_of::<A>() >= size_of::<B>()`
+/// * `align_of::<A>() >= align_of::<B>()`
+///
+/// For rules 1 and 3, this obviously holds.
+/// For rule 2, this holds as long as
+/// `A ~ B` implies that (`*B` is a fat ptr implies `*A` is a fat ptr).
+///
+/// For rule 1, this holds trivially.  
+/// For rule 2, this holds because `**A` and `**B` are always thin ptrs.  
+/// For rule 3, this holds trivially.  
+/// For rule 4, this holds because  if `*A` is a fat ptr,
+/// `A` is unsized, and thus `[A; N]` is ill-formed to begin with.  
+/// For (almost) rule 5, this holds because `*[A]` is always a fat ptr.
 pub fn is_transmutable_to<'tcx>(from: Ty<'tcx>, to: Ty<'tcx>) -> bool {
     let transmutable_ints = || {
         use IntTy::*;