Update rustc

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.145"
+let supported_charon_version = "0.1.146"

charon-ml/src/PrintExpressions.ml

@@ -88,6 +88,8 @@ and nullop_to_string (env : 'a fmt_env) (op : nullop) : string =
   | AlignOf -> "align_of"
   | OffsetOf _ -> "offset_of(?)"
   | UbChecks -> "ub_checks"
+  | ContractChecks -> "contract_checks"
+  | OverflowChecks -> "overflow_checks"
 
 and unop_to_string (env : 'a fmt_env) (unop : unop) : string =
   match unop with

charon-ml/src/generated/Generated_Expressions.ml

@@ -216,7 +216,13 @@ and field_proj_kind =
 and local_id = (LocalId.id[@visitors.opaque])
 
 (** Nullary operation *)
-and nullop = SizeOf | AlignOf | OffsetOf of (int * field_id) list | UbChecks
+and nullop =
+  | SizeOf
+  | AlignOf
+  | OffsetOf of type_decl_ref * variant_id option * field_id
+  | UbChecks
+  | OverflowChecks
+  | ContractChecks
 
 and operand =
   | Copy of place

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -1295,12 +1295,14 @@ and nullop_of_json (ctx : of_json_ctx) (js : json) : (nullop, string) result =
     (match js with
     | `String "SizeOf" -> Ok SizeOf
     | `String "AlignOf" -> Ok AlignOf
-    | `Assoc [ ("OffsetOf", offset_of) ] ->
-        let* offset_of =
-          list_of_json (pair_of_json int_of_json field_id_of_json) ctx offset_of
-        in
-        Ok (OffsetOf offset_of)
+    | `Assoc [ ("OffsetOf", `List [ x_0; x_1; x_2 ]) ] ->
+        let* x_0 = type_decl_ref_of_json ctx x_0 in
+        let* x_1 = option_of_json variant_id_of_json ctx x_1 in
+        let* x_2 = field_id_of_json ctx x_2 in
+        Ok (OffsetOf (x_0, x_1, x_2))
     | `String "UbChecks" -> Ok UbChecks
+    | `String "OverflowChecks" -> Ok OverflowChecks
+    | `String "ContractChecks" -> Ok ContractChecks
     | _ -> Error "")
 
 and operand_of_json (ctx : of_json_ctx) (js : json) : (operand, string) result =

charon/Cargo.toml

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

charon/rust-toolchain

@@ -1,4 +1,4 @@
 [toolchain]
-channel = "nightly-2025-11-08"
+channel = "nightly-2025-11-23"
 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

@@ -176,9 +176,10 @@ pub enum UnOp {
 pub enum NullOp {
     SizeOf,
     AlignOf,
-    #[drive(skip)]
-    OffsetOf(Vec<(usize, FieldId)>),
+    OffsetOf(TypeDeclRef, Option<VariantId>, FieldId),
     UbChecks,
+    OverflowChecks,
+    ContractChecks,
 }
 
 /// For all the variants: the first type gives the source type, the second one gives

charon/src/ast/expressions_utils.rs

@@ -252,4 +252,19 @@ impl FnPtr {
             generics: generics.into(),
         }
     }
+
+    /// Get the generics for the pre-monomorphization item.
+    pub fn pre_mono_generics<'a>(&'a self, krate: &'a TranslatedCrate) -> &'a GenericArgs {
+        match *self.kind {
+            FnPtrKind::Fun(FunId::Regular(fun_id)) => krate
+                .item_name(fun_id)
+                .unwrap()
+                .mono_args()
+                .unwrap_or(&self.generics),
+            //  We don't mono builtins.
+            FnPtrKind::Fun(FunId::Builtin(..)) => &self.generics,
+            // Can't happen in mono mode.
+            FnPtrKind::Trait(..) => &self.generics,
+        }
+    }
 }

charon/src/ast/types_utils.rs

@@ -593,6 +593,12 @@ impl LiteralTy {
     }
 }
 
+impl From<LiteralTy> for Ty {
+    fn from(value: LiteralTy) -> Self {
+        TyKind::Literal(value).into_ty()
+    }
+}
+
 /// A value of type `T` bound by the generic parameters of item
 /// `item`. Used when dealing with multiple items at a time, to
 /// ensure we don't mix up generics.

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

@@ -542,23 +542,13 @@ impl BodyTransCtx<'_, '_, '_> {
                 self.translate_operand(span, left)?,
                 self.translate_operand(span, right)?,
             )),
-            hax::Rvalue::NullaryOp(nullop, ty) => {
-                trace!("NullOp: {:?}", nullop);
-                let ty = self.translate_ty(span, ty)?;
-                let op = match nullop {
-                    hax::NullOp::OffsetOf(fields) => NullOp::OffsetOf(
-                        fields
-                            .iter()
-                            .copied()
-                            .map(|(n, idx)| (n, translate_field_id(idx)))
-                            .collect(),
-                    ),
-                    hax::NullOp::UbChecks => NullOp::UbChecks,
-                    hax::NullOp::ContractChecks => {
-                        raise_error!(self, span, "charon does not support contracts");
-                    }
+            hax::Rvalue::NullaryOp(hax::NullOp::RuntimeChecks(check)) => {
+                let op = match check {
+                    hax::RuntimeChecks::UbChecks => NullOp::UbChecks,
+                    hax::RuntimeChecks::OverflowChecks => NullOp::OverflowChecks,
+                    hax::RuntimeChecks::ContractChecks => NullOp::ContractChecks,
                 };
-                Ok(Rvalue::NullaryOp(op, ty))
+                Ok(Rvalue::NullaryOp(op, LiteralTy::Bool.into()))
             }
             hax::Rvalue::UnaryOp(unop, operand) => {
                 let operand = self.translate_operand(span, operand)?;

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

@@ -351,11 +351,14 @@ impl ItemTransCtx<'_, '_> {
                 // arg-N, rest...
                 // We then add N statements of the form `locals[N+3] := move locals[2].N`,
                 // to destructure the arguments.
-                let GExprBody {
+                let Body::Unstructured(GExprBody {
                     locals,
                     body: blocks,
                     ..
-                } = body.as_unstructured_mut().unwrap();
+                }) = &mut body
+                else {
+                    return Ok(body);
+                };
 
                 blocks.dyn_visit_mut(|local: &mut LocalId| {
                     if local.index() >= 2 {

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

@@ -92,15 +92,19 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
                     .try_collect()?;
                 expressions::ConstantExprKind::Adt(None, fields)
             }
-            ConstantExprKind::TraitConst { impl_expr, name } => {
-                let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
-                let name = TraitItemName(name.into());
-                expressions::ConstantExprKind::TraitConst(trait_ref, name)
-            }
-            ConstantExprKind::GlobalName(item) => {
-                let global_ref = self.translate_global_decl_ref(span, item)?;
-                expressions::ConstantExprKind::Global(global_ref)
-            }
+            ConstantExprKind::NamedGlobal(item) => match &item.in_trait {
+                Some(impl_expr) => {
+                    let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
+                    // Trait consts can't have their own generics.
+                    assert!(item.generic_args.is_empty());
+                    let name = self.translate_trait_item_name(&item.def_id)?;
+                    expressions::ConstantExprKind::TraitConst(trait_ref, name)
+                }
+                None => {
+                    let global_ref = self.translate_global_decl_ref(span, item)?;
+                    expressions::ConstantExprKind::Global(global_ref)
+                }
+            },
             ConstantExprKind::Borrow(v)
                 if let ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)) =
                     v.contents.as_ref() =>

charon/src/pretty/fmt_with_ctx.rs

@@ -972,12 +972,24 @@ impl<C: AstFormatter> FmtWithCtx<C> for Name {
 }
 
 impl<C: AstFormatter> FmtWithCtx<C> for NullOp {
-    fn fmt_with_ctx(&self, _ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+    fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         let op = match self {
             NullOp::SizeOf => "size_of",
             NullOp::AlignOf => "align_of",
-            NullOp::OffsetOf(_) => "offset_of(?)",
+            &NullOp::OffsetOf(ref ty, variant, field) => {
+                let tid = *ty.id.as_adt().expect("found offset_of of a non-adt type");
+                write!(f, "offset_of({}.", ty.with_ctx(ctx))?;
+                if let Some(variant) = variant {
+                    ctx.format_enum_variant_name(f, tid, variant)?;
+                    write!(f, ".")?;
+                }
+                ctx.format_field_name(f, tid, variant, field)?;
+                write!(f, ")")?;
+                return Ok(());
+            }
             NullOp::UbChecks => "ub_checks",
+            NullOp::OverflowChecks => "overflow_checks",
+            NullOp::ContractChecks => "contract_checks",
         };
         write!(f, "{op}")
     }

charon/src/pretty/formatter.rs

@@ -53,7 +53,7 @@ pub trait AstFormatter: Sized {
     where
         GenericParams: HasVectorOf<Id, Output = T>;
 
-    fn format_enum_variant(
+    fn format_enum_variant_name(
         &self,
         f: &mut fmt::Formatter<'_>,
         type_id: TypeDeclId,
@@ -67,7 +67,17 @@ pub trait AstFormatter: Sized {
         } else {
             &variant_id.to_pretty_string()
         };
-        write!(f, "{}::{variant}", type_id.with_ctx(self))
+        write!(f, "{variant}")
+    }
+    fn format_enum_variant(
+        &self,
+        f: &mut fmt::Formatter<'_>,
+        type_id: TypeDeclId,
+        variant_id: VariantId,
+    ) -> fmt::Result {
+        write!(f, "{}::", type_id.with_ctx(self))?;
+        self.format_enum_variant_name(f, type_id, variant_id)?;
+        Ok(())
     }
 
     fn format_field_name(

charon/src/transform/mod.rs

@@ -35,6 +35,7 @@ pub mod resugar {
     pub mod reconstruct_asserts;
     pub mod reconstruct_boxes;
     pub mod reconstruct_fallible_operations;
+    pub mod reconstruct_intrinsics;
     pub mod reconstruct_matches;
 }
 
@@ -133,6 +134,9 @@ pub static ULLBC_PASSES: &[Pass] = &[
     // **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].
     UnstructuredBody(&resugar::reconstruct_fallible_operations::Transform),
+    // 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.
     // **WARNING**: this pass relies on a precise structure of the MIR statements. Because of this,

charon/src/transform/resugar/reconstruct_intrinsics.rs

@@ -0,0 +1,54 @@
+use crate::transform::TransformCtx;
+use crate::transform::ctx::{BodyTransformCtx, UllbcPass};
+use crate::ullbc_ast::*;
+
+pub struct Transform;
+impl UllbcPass for Transform {
+    fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) {
+        decl.transform_ullbc_terminators(ctx, |ctx, term| {
+            let TerminatorKind::Call { call, target, .. } = &term.kind else {
+                return;
+            };
+            let FnOperand::Regular(fn_ptr) = &call.func else {
+                return;
+            };
+            let FnPtrKind::Fun(FunId::Regular(fun_id)) = &fn_ptr.kind else {
+                return;
+            };
+            let Some(fun_decl) = ctx.ctx.translated.fun_decls.get(*fun_id) else {
+                return;
+            };
+            if fun_decl.item_meta.lang_item.as_deref() == Some("offset_of")
+                && let generics = fn_ptr.pre_mono_generics(&ctx.ctx.translated)
+                && let Some(ty) = generics.types.get(TypeVarId::ZERO)
+                && let TyKind::Adt(tref) = ty.kind()
+                && let TypeId::Adt(type_id) = tref.id
+                && let [Operand::Const(arg0), Operand::Const(arg1)] = call.args.as_slice()
+                && let ConstantExprKind::Literal(Literal::Scalar(ScalarValue::Unsigned(
+                    UIntTy::U32,
+                    variant_id,
+                ))) = &arg0.kind
+                && let ConstantExprKind::Literal(Literal::Scalar(ScalarValue::Unsigned(
+                    UIntTy::U32,
+                    field_id,
+                ))) = &arg1.kind
+                && let Some(tdecl) = ctx.ctx.translated.type_decls.get(type_id)
+            {
+                // TODO: move into a pass, maybe also size_of/align_of? or remove the nullops.
+                // maybe this is a constant also.
+                let variant_id = if tdecl.kind.is_enum() {
+                    Some(VariantId::from_usize(*variant_id as usize))
+                } else {
+                    None
+                };
+                let field_id = FieldId::from_usize(*field_id as usize);
+                let rval = Rvalue::NullaryOp(
+                    NullOp::OffsetOf(tref.clone(), variant_id, field_id),
+                    Ty::mk_usize(),
+                );
+                ctx.insert_assn_stmt(call.dest.clone(), rval);
+                term.kind = TerminatorKind::Goto { target: *target };
+            }
+        });
+    }
+}

charon/src/transform/simplify_output/hide_marker_traits.rs

@@ -76,6 +76,7 @@ impl TransformPass for Transform {
                 "core::marker::Send",
                 "core::marker::Sync",
                 "core::marker::Unpin",
+                "core::clone::TrivialClone",
             ]
         } else {
             vec![]

charon/tests/cargo/dependencies.out

@@ -3,8 +3,6 @@
 // Full name: core::fmt::Arguments
 #[lang_item("format_arguments")]
 pub opaque type Arguments<'a>
-where
-    'a : 'a,
 
 // Full name: core::marker::MetaSized
 #[lang_item("meta_sized")]