Support unsize coercions

charon-ml/src/Expressions.ml

@@ -149,6 +149,7 @@ class ['self] map_constant_expr_base =
 type cast_kind =
   | CastScalar of literal_type * literal_type
   | CastFnPtr of ty * ty
+  | CastUnsize of ty * ty
 
 (* Remark: no `ArrayToSlice` variant: it gets eliminated in a micro-pass. *)
 and unop =

charon-ml/src/GAstOfJson.ml

@@ -764,6 +764,10 @@ let cast_kind_of_json (js : json) : (cast_kind, string) result =
         let* src_ty = ty_of_json src_ty in
         let* tgt_ty = ty_of_json tgt_ty in
         Ok (CastFnPtr (src_ty, tgt_ty))
+    | `Assoc [ ("Unsize", `List [ src_ty; tgt_ty ]) ] ->
+        let* src_ty = ty_of_json src_ty in
+        let* tgt_ty = ty_of_json tgt_ty in
+        Ok (CastUnsize (src_ty, tgt_ty))
     | _ -> Error "")
 
 let unop_of_json (js : json) : (unop, string) result =

charon-ml/src/PrintExpressions.ml

@@ -59,6 +59,8 @@ let cast_kind_to_string (env : ('a, 'b) fmt_env) (cast : cast_kind) : string =
       ^ ">"
   | CastFnPtr (src, tgt) ->
       "cast<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">"
+  | CastUnsize (src, tgt) ->
+      "unsize<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">"
 
 let unop_to_string (env : ('a, 'b) fmt_env) (unop : unop) : string =
   match unop with

charon/src/ast/expressions.rs

@@ -156,6 +156,12 @@ pub enum CastKind {
     /// Remark: for now we don't support conversions with Char.
     Scalar(LiteralTy, LiteralTy),
     FnPtr(Ty, Ty),
+    /// [Unsize coercion](https://doc.rust-lang.org/std/ops/trait.CoerceUnsized.html). This is
+    /// either `[T; N]` -> `[T]` or `T: Trait` -> `dyn Trait` coercions, behind a pointer
+    /// (reference, `Box`, or other type that implements `CoerceUnsized`).
+    ///
+    /// The special case of `&[T; N]` -> `&[T]` coercion is caught by `UnOp::ArrayToSlice`.
+    Unsize(Ty, Ty),
 }
 
 /// Binary operations.

charon/src/lib.rs

@@ -11,10 +11,12 @@
 //! we reconstructed the control-flow to have `if ... then ... else ...`,
 //! loops, etc. instead of `GOTO`s).
 
+#![expect(incomplete_features)]
 #![feature(rustc_private)]
-#![feature(box_patterns)]
 // For rustdoc: prevents overflows
 #![recursion_limit = "256"]
+#![feature(box_patterns)]
+#![feature(deref_patterns)]
 #![feature(if_let_guard)]
 #![feature(impl_trait_in_assoc_type)]
 #![feature(iter_array_chunks)]

charon/src/pretty/fmt_with_ctx.rs

@@ -97,9 +97,16 @@ impl<C: AstFormatter> FmtWithCtx<C> for gast::Body {
 impl<C: AstFormatter> FmtWithCtx<C> for CastKind {
     fn fmt_with_ctx(&self, ctx: &C) -> String {
         match self {
-            CastKind::Scalar(src, tgt) => format!("cast<{src},{tgt}>"),
+            CastKind::Scalar(src, tgt) => format!("cast<{src}, {tgt}>"),
             CastKind::FnPtr(src, tgt) => {
-                format!("cast<{},{}>", src.fmt_with_ctx(ctx), tgt.fmt_with_ctx(ctx))
+                format!("cast<{}, {}>", src.fmt_with_ctx(ctx), tgt.fmt_with_ctx(ctx))
+            }
+            CastKind::Unsize(src, tgt) => {
+                format!(
+                    "unsize_cast<{}, {}>",
+                    src.fmt_with_ctx(ctx),
+                    tgt.fmt_with_ctx(ctx)
+                )
             }
         }
     }

charon/src/translate/translate_functions_to_ullbc.rs

@@ -598,7 +598,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 let tgt_ty = self.translate_ty(span, erase_regions, tgt_ty)?;
 
                 // Translate the operand
-                let (op, src_ty) = self.translate_operand_with_type(span, operand)?;
+                let (operand, src_ty) = self.translate_operand_with_type(span, operand)?;
 
                 match (cast_kind, &src_ty, &tgt_ty) {
                     (hax::CastKind::IntToInt, _, _) => {
@@ -608,48 +608,43 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
                         Ok(Rvalue::UnaryOp(
                             UnOp::Cast(CastKind::Scalar(src_ty, tgt_ty)),
-                            op,
+                            operand,
                         ))
                     }
                     (
                         hax::CastKind::PointerCoercion(hax::PointerCoercion::Unsize),
-                        Ty::Ref(_, t1, kind1),
-                        Ty::Ref(_, t2, kind2),
+                        Ty::Ref(
+                            _,
+                            deref!(Ty::Adt(TypeId::Assumed(AssumedTy::Array), generics)),
+                            kind1,
+                        ),
+                        Ty::Ref(
+                            _,
+                            deref!(Ty::Adt(TypeId::Assumed(AssumedTy::Slice), generics1)),
+                            kind2,
+                        ),
                     ) => {
                         // In MIR terminology, we go from &[T; l] to &[T] which means we
                         // effectively "unsize" the type, as `l` no longer appears in the
                         // destination type. At runtime, the converse happens: the length
                         // materializes into the fat pointer.
-                        match (&**t1, &**t2) {
-                            (
-                                Ty::Adt(TypeId::Assumed(AssumedTy::Array), generics),
-                                Ty::Adt(TypeId::Assumed(AssumedTy::Slice), generics1),
-                            ) => {
-                                assert!(
-                                    generics.types.len() == 1 && generics.const_generics.len() == 1
-                                );
-                                assert!(generics.types[0] == generics1.types[0]);
-                                assert!(kind1 == kind2);
-                                Ok(Rvalue::UnaryOp(
-                                    UnOp::ArrayToSlice(
-                                        *kind1,
-                                        generics.types[0].clone(),
-                                        generics.const_generics[0].clone(),
-                                    ),
-                                    op,
-                                ))
-                            }
-                            _ => {
-                                error_or_panic!(
-                                    self,
-                                    span,
-                                    format!(
-                                        "Unsupported cast:\n\n- rvalue: {:?}\n\n- src={:?}\n\n- dst={:?}",
-                                        rvalue, src_ty, tgt_ty
-                                    )
-                                )
-                            }
-                        }
+                        assert!(generics.types.len() == 1 && generics.const_generics.len() == 1);
+                        assert!(generics.types[0] == generics1.types[0]);
+                        assert!(kind1 == kind2);
+                        Ok(Rvalue::UnaryOp(
+                            UnOp::ArrayToSlice(
+                                *kind1,
+                                generics.types[0].clone(),
+                                generics.const_generics[0].clone(),
+                            ),
+                            operand,
+                        ))
+                    }
+                    (hax::CastKind::PointerCoercion(hax::PointerCoercion::Unsize), _, _) => {
+                        Ok(Rvalue::UnaryOp(
+                            UnOp::Cast(CastKind::Unsize(src_ty.clone(), tgt_ty.clone())),
+                            operand,
+                        ))
                     }
                     (
                         hax::CastKind::PointerCoercion(hax::PointerCoercion::ClosureFnPointer(
@@ -663,7 +658,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         let tgt_ty = tgt_ty.clone();
                         Ok(Rvalue::UnaryOp(
                             UnOp::Cast(CastKind::FnPtr(src_ty, tgt_ty)),
-                            op,
+                            operand,
                         ))
                     }
                     (
@@ -675,7 +670,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         let tgt_ty = tgt_ty.clone();
                         Ok(Rvalue::UnaryOp(
                             UnOp::Cast(CastKind::FnPtr(src_ty, tgt_ty)),
-                            op,
+                            operand,
                         ))
                     }
                     _ => {

charon/tests/ui/closures.out

@@ -141,7 +141,7 @@ fn test_crate::test_closure_u32(@1: u32) -> u32
     let @5: u32; // anonymous local
 
     @3 := {test_crate::test_closure_u32::closure} {}
-    f@2 := cast<fn(u32) -> u32,fn(u32) -> u32>(move (@3))
+    f@2 := cast<fn(u32) -> u32, fn(u32) -> u32>(move (@3))
     drop @3
     @fake_read(f@2)
     @4 := copy (f@2)
@@ -174,7 +174,7 @@ fn test_crate::test_closure_ref_u32<'a>(@1: &'a (u32)) -> &'a (u32)
     let @6: &'_ (u32); // anonymous local
 
     @3 := {test_crate::test_closure_ref_u32::closure} {}
-    f@2 := cast<fn<'_1_0>(&'_1_0 (u32)) -> &'_1_0 (u32),fn<'_1_0>(&'_1_0 (u32)) -> &'_1_0 (u32)>(move (@3))
+    f@2 := cast<fn<'_1_0>(&'_1_0 (u32)) -> &'_1_0 (u32), fn<'_1_0>(&'_1_0 (u32)) -> &'_1_0 (u32)>(move (@3))
     drop @3
     @fake_read(f@2)
     @5 := copy (f@2)
@@ -209,7 +209,7 @@ fn test_crate::test_closure_ref_param<'_0, T>(@1: &'_0 (T)) -> &'_0 (T)
     let @6: &'_ (T); // anonymous local
 
     @3 := {test_crate::test_closure_ref_param::closure<T>} {}
-    f@2 := cast<fn<'_1_0>(&'_1_0 (T)) -> &'_1_0 (T),fn<'_1_0>(&'_1_0 (T)) -> &'_1_0 (T)>(move (@3))
+    f@2 := cast<fn<'_1_0>(&'_1_0 (T)) -> &'_1_0 (T), fn<'_1_0>(&'_1_0 (T)) -> &'_1_0 (T)>(move (@3))
     drop @3
     @fake_read(f@2)
     @5 := copy (f@2)
@@ -246,7 +246,7 @@ fn test_crate::test_map_option2(@1: core::option::Option<u32>) -> core::option::
     let @5: fn(u32) -> u32; // anonymous local
 
     @3 := {test_crate::test_map_option2::closure} {}
-    f@2 := cast<fn(u32) -> u32,fn(u32) -> u32>(move (@3))
+    f@2 := cast<fn(u32) -> u32, fn(u32) -> u32>(move (@3))
     drop @3
     @fake_read(f@2)
     @4 := copy (x@1)
@@ -337,7 +337,7 @@ fn test_crate::test_id_clone(@1: u32) -> u32
     let @3: fn(u32) -> u32; // anonymous local
     let @4: u32; // anonymous local
 
-    f@2 := cast<fn(u32) -> u32,fn(u32) -> u32>(const (test_crate::id_clone<u32>[core::clone::impls::{impl core::clone::Clone for u32#8}]))
+    f@2 := cast<fn(u32) -> u32, fn(u32) -> u32>(const (test_crate::id_clone<u32>[core::clone::impls::{impl core::clone::Clone for u32#8}]))
     @fake_read(f@2)
     @3 := copy (f@2)
     @4 := copy (x@1)
@@ -358,7 +358,7 @@ where
     let @3: fn(T) -> T; // anonymous local
     let @4: T; // anonymous local
 
-    f@2 := cast<fn(T) -> T,fn(T) -> T>(const (test_crate::id_clone<T>[@TraitClause0]))
+    f@2 := cast<fn(T) -> T, fn(T) -> T>(const (test_crate::id_clone<T>[@TraitClause0]))
     @fake_read(f@2)
     @3 := copy (f@2)
     @4 := move (x@1)
@@ -431,7 +431,7 @@ fn test_crate::test_regions<'a>(@1: &'a (u32)) -> u32
     let @6: &'_ (&'_ (u32)); // anonymous local
 
     @3 := {test_crate::test_regions::closure} {}
-    f@2 := cast<fn<'_1_0>(&'_1_0 (&'_ (u32))) -> u32,fn<'_1_0>(&'_1_0 (&'_ (u32))) -> u32>(move (@3))
+    f@2 := cast<fn<'_1_0>(&'_1_0 (&'_ (u32))) -> u32, fn<'_1_0>(&'_1_0 (&'_ (u32))) -> u32>(move (@3))
     drop @3
     @fake_read(f@2)
     @4 := copy (f@2)

charon/tests/ui/issue-114-opaque-bodies.out

@@ -101,7 +101,7 @@ fn core::convert::num::{impl core::convert::From<i32> for i64#83}::from(@1: i32)
     let @0: i64; // return
     let small@1: i32; // arg #1
 
-    @0 := cast<i32,i64>(copy (small@1))
+    @0 := cast<i32, i64>(copy (small@1))
     return
 }
 

charon/tests/ui/no_nested_borrows.out

@@ -118,7 +118,7 @@ fn test_crate::cast_u32_to_i32(@1: u32) -> i32
     let @2: u32; // anonymous local
 
     @2 := copy (x@1)
-    @0 := cast<u32,i32>(move (@2))
+    @0 := cast<u32, i32>(move (@2))
     drop @2
     return
 }
@@ -130,7 +130,7 @@ fn test_crate::cast_bool_to_i32(@1: bool) -> i32
     let @2: bool; // anonymous local
 
     @2 := copy (x@1)
-    @0 := cast<bool,i32>(move (@2))
+    @0 := cast<bool, i32>(move (@2))
     drop @2
     return
 }