Bump rustc to remove ShallowInitBox

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.176"
+let supported_charon_version = "0.1.177"

charon-ml/src/PrintExpressions.ml

@@ -222,6 +222,4 @@ and rvalue_to_string (env : 'a fmt_env) (rv : rvalue) : string =
       "[" ^ operand_to_string env v ^ ";"
       ^ constant_expr_to_string env len
       ^ "]"
-  | ShallowInitBox (op, _) ->
-      "shallow-init-box(" ^ operand_to_string env op ^ ")"
   | Aggregate (akind, ops) -> aggregate_to_string env akind ops

charon-ml/src/generated/Generated_Expressions.ml

@@ -310,11 +310,6 @@ and rvalue =
       (** [Repeat(x, n)] creates an array where [x] is copied [n] times.
 
           We translate this to a function call for LLBC. *)
-  | ShallowInitBox of operand * ty
-      (** Transmutes a [*mut u8] (obtained from [malloc]) into
-          shallow-initialized [Box<T>]. This only appears as part of lowering
-          [Box::new()] in some cases. We reconstruct the original [Box::new()]
-          call, but sometimes may fail to do so, leaking the expression. *)
 
 (** Unary operation *)
 and unop =

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -295,6 +295,8 @@ and builtin_fun_id_of_json (ctx : of_json_ctx) (js : json) :
   combine_error_msgs js __FUNCTION__
     (match js with
     | `String "BoxNew" -> Ok BoxNew
+    | `String "BoxWrite" -> Ok BoxWrite
+    | `String "SliceIntoVec" -> Ok SliceIntoVec
     | `String "ArrayToSliceShared" -> Ok ArrayToSliceShared
     | `String "ArrayToSliceMut" -> Ok ArrayToSliceMut
     | `String "ArrayRepeat" -> Ok ArrayRepeat
@@ -1780,10 +1782,6 @@ and rvalue_of_json (ctx : of_json_ctx) (js : json) : (rvalue, string) result =
         let* x_1 = ty_of_json ctx x_1 in
         let* x_2 = box_of_json constant_expr_of_json ctx x_2 in
         Ok (Repeat (x_0, x_1, x_2))
-    | `Assoc [ ("ShallowInitBox", `List [ x_0; x_1 ]) ] ->
-        let* x_0 = operand_of_json ctx x_0 in
-        let* x_1 = ty_of_json ctx x_1 in
-        Ok (ShallowInitBox (x_0, x_1))
     | _ -> Error "")
 
 and scalar_value_of_json (ctx : of_json_ctx) (js : json) :

charon-ml/src/generated/Generated_Types.ml

@@ -175,6 +175,13 @@ and builtin_fun_id =
   | BoxNew
       (** Used instead of [alloc::boxed::Box::new] when [--treat-box-as-builtin]
           is set. *)
+  | BoxWrite
+      (** Used instead of [alloc::boxed::Box::write] when rewriting [vec!]
+          lowering. Writes into a [Box<MaybeUninit<T>>] and returns a [Box<T>].
+      *)
+  | SliceIntoVec
+      (** Used instead of [alloc::slice::into_vec] when rewriting [vec!]
+          lowering. Takes a [Box<[T]>] and returns a [Vec<T>]. *)
   | ArrayToSliceShared
       (** Cast [&[T; N]] to [&[T]].
 

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.176"
+version = "0.1.177"
 authors = [
     "Son Ho <hosonmarc@gmail.com>",
     "Guillaume Boisseau <nadrieril+git@gmail.com>",

charon/hax-frontend/src/lib.rs

@@ -1,5 +1,4 @@
 #![allow(rustdoc::private_intra_doc_links)]
-#![feature(if_let_guard)]
 #![feature(macro_metavar_expr)]
 #![feature(rustc_private)]
 #![feature(sized_hierarchy)]

charon/rust-toolchain

@@ -1,4 +1,4 @@
 [toolchain]
-channel = "nightly-2026-02-07"
+channel = "nightly-2026-02-22"
 components = [ "rustc-dev", "llvm-tools-preview", "rust-src", "miri" ]
 targets = [ "x86_64-apple-darwin", "i686-unknown-linux-gnu", "powerpc64-unknown-linux-gnu", "riscv64gc-unknown-none-elf" ]

charon/src/ast/expressions.rs

@@ -428,6 +428,12 @@ impl From<BuiltinFunId> for FunId {
 pub enum BuiltinFunId {
     /// Used instead of `alloc::boxed::Box::new` when `--treat-box-as-builtin` is set.
     BoxNew,
+    /// Used instead of `alloc::boxed::Box::write` when rewriting `vec!` lowering.
+    /// Writes into a `Box<MaybeUninit<T>>` and returns a `Box<T>`.
+    BoxWrite,
+    /// Used instead of `alloc::slice::into_vec` when rewriting `vec!` lowering.
+    /// Takes a `Box<[T]>` and returns a `Vec<T>`.
+    SliceIntoVec,
     /// Cast `&[T; N]` to `&[T]`.
     ///
     /// This is used instead of unsizing coercions when `--ops-to-function-calls` is set.
@@ -761,10 +767,6 @@ pub enum Rvalue {
     ///
     /// We translate this to a function call for LLBC.
     Repeat(Operand, Ty, Box<ConstantExpr>),
-    /// Transmutes a `*mut u8` (obtained from `malloc`) into shallow-initialized `Box<T>`. This
-    /// only appears as part of lowering `Box::new()` in some cases. We reconstruct the original
-    /// `Box::new()` call, but sometimes may fail to do so, leaking the expression.
-    ShallowInitBox(Operand, Ty),
 }
 
 /// An aggregated ADT.

charon/src/ast/hash_cons.rs

@@ -60,7 +60,6 @@ mod intern_table {
 
     pub fn intern<T: HashConsable>(inner: T) -> HashConsed<T> {
         // Fast read-only check.
-        #[expect(irrefutable_let_patterns)] // https://github.com/rust-lang/rust/issues/139369
         let arc = if let read_guard = INTERNED.read().unwrap()
             && let Some(set) = read_guard.get::<T>()
             && let Some(arc) = set.get(&inner)

charon/src/ast/types_utils.rs

@@ -760,6 +760,10 @@ impl Ty {
         }
     }
 
+    pub fn as_adt_id(&self) -> Option<TypeDeclId> {
+        self.kind().as_adt().and_then(|a| a.id.as_adt().cloned())
+    }
+
     pub fn get_ptr_metadata(&self, translated: &TranslatedCrate) -> PtrMetadata {
         let ref ty_decls = translated.type_decls;
         match self.kind() {

charon/src/bin/charon-driver/main.rs

@@ -4,7 +4,6 @@
 #![expect(incomplete_features)]
 #![feature(box_patterns)]
 #![feature(deref_patterns)]
-#![feature(if_let_guard)]
 #![feature(iter_array_chunks)]
 #![feature(iterator_try_collect)]
 

charon/src/bin/charon-driver/translate/translate_bodies.rs

@@ -895,11 +895,6 @@ impl<'tcx> BlockTransCtx<'tcx, '_, '_, '_> {
                     }
                 }
             }
-            mir::Rvalue::ShallowInitBox(op, ty) => {
-                let op = self.translate_operand(span, op)?;
-                let ty = self.translate_rustc_ty(span, ty)?;
-                Ok(Rvalue::ShallowInitBox(op, ty))
-            }
             mir::Rvalue::ThreadLocalRef(_) => {
                 raise_error!(
                     self,

charon/src/bin/generate-ml/main.rs

@@ -6,7 +6,6 @@
 //!
 //! To run it, call `cargo run --bin generate-ml`. It is also run by `make generate-ml` in the
 //! crate root. Don't forget to format the output code after regenerating.
-#![feature(if_let_guard)]
 
 use anyhow::{Context, Result, bail};
 use assert_cmd::cargo::CommandCargoExt;

charon/src/lib.rs

@@ -14,11 +14,9 @@
 // For rustdoc: prevents overflows
 #![recursion_limit = "256"]
 #![expect(incomplete_features)]
-#![feature(assert_matches)]
 #![feature(box_patterns)]
 #![feature(deref_patterns)]
 #![feature(deref_pure_trait)]
-#![feature(if_let_guard)]
 #![feature(impl_trait_in_assoc_type)]
 #![feature(iterator_try_collect)]
 #![feature(register_tool)]

charon/src/pretty/fmt_with_ctx.rs

@@ -269,6 +269,8 @@ impl Display for BuiltinFunId {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> std::result::Result<(), fmt::Error> {
         let name = match *self {
             BuiltinFunId::BoxNew => "BoxNew",
+            BuiltinFunId::BoxWrite => "BoxWrite",
+            BuiltinFunId::SliceIntoVec => "SliceIntoVec",
             BuiltinFunId::ArrayToSliceShared => "ArrayToSliceShared",
             BuiltinFunId::ArrayToSliceMut => "ArrayToSliceMut",
             BuiltinFunId::ArrayRepeat => "ArrayRepeat",
@@ -1534,14 +1536,6 @@ impl<C: AstFormatter> FmtWithCtx<C> for Rvalue {
             Rvalue::Repeat(op, _ty, cg) => {
                 write!(f, "[{}; {}]", op.with_ctx(ctx), cg.with_ctx(ctx))
             }
-            Rvalue::ShallowInitBox(op, ty) => {
-                write!(
-                    f,
-                    "shallow_init_box::<{}>({})",
-                    ty.with_ctx(ctx),
-                    op.with_ctx(ctx)
-                )
-            }
         }
     }
 }

charon/src/transform/mod.rs

@@ -34,10 +34,10 @@ pub mod resugar {
     pub mod inline_local_panic_functions;
     pub mod move_asserts_to_statements;
     pub mod reconstruct_asserts;
-    pub mod reconstruct_boxes;
     pub mod reconstruct_fallible_operations;
     pub mod reconstruct_intrinsics;
     pub mod reconstruct_matches;
+    pub mod reconstruct_vec_boxes;
 }
 
 /// Passes that make the output simpler/easier to consume.
@@ -143,12 +143,11 @@ pub static ULLBC_PASSES: &[Pass] = &[
     // Recognize calls to the `offset_of` intrinsics and replace them with the corresponding
     // `NullOp`.
     UnstructuredBody(&resugar::reconstruct_intrinsics::Transform),
-    // # Micro-pass: reconstruct the special `Box::new` operations inserted e.g. in the `vec![]`
-    // macro.
+    // # Micro-pass: reconstruct `vec![x]` lowering to avoid unsafe operations.
     // **WARNING**: this pass relies on a precise structure of the MIR statements. Because of this,
     // it must happen before passes that insert statements like [simplify_constants].
     // **WARNING**: this pass works across calls, hence must happen after `merge_goto_chains`,
-    UnstructuredBody(&resugar::reconstruct_boxes::Transform),
+    UnstructuredBody(&resugar::reconstruct_vec_boxes::Transform),
     // # Micro-pass: reconstruct the asserts
     UnstructuredBody(&resugar::reconstruct_asserts::Transform),
     // # Micro-pass: `panic!()` expands to a new function definition each time. This pass cleans