Update hax and rustc

I also had to update cargo dependencies because of a nightly feature
change that broke `ahash`.

charon/Cargo.toml

@@ -55,7 +55,7 @@ tracing = { version = "0.1", features = [ "max_level_trace", "release_max_level_
 walkdir = "2.3.2"
 which = "6.0.1"
 
-hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "update-rustc2" }
+hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "update-rustc-madness" }
 # hax-frontend-exporter = { path = "../../hax/frontend/exporter" }
 macros = { path = "./macros" }
 

charon/src/bin/charon/main.rs

@@ -30,8 +30,6 @@
 //! deserialize them later and use them to guide the extraction in the
 //! callbacks.
 
-#![cfg_attr(feature = "deny-warnings", deny(warnings))]
-
 // Don't link with the `charon_lib` crate so that the `charon` binary doesn't have to dynamically
 // link to `librustc_driver.so` etc.
 #[path = "../../cli_options.rs"]

charon/src/deps_errors.rs

@@ -1,19 +1,41 @@
 //! Utilities to generate error reports about the external dependencies.
 use crate::translate_ctx::*;
+use macros::VariantIndexArity;
 use petgraph::algo::dijkstra::dijkstra;
 use petgraph::graphmap::DiGraphMap;
 use rustc_error_messages::MultiSpan;
 use rustc_hir::def_id::DefId;
 use rustc_span::Span;
 
 /// For error reporting
-#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, VariantIndexArity)]
 enum Node {
     External(DefId),
     /// We use the span information only for local references
     Local(DefId, Span),
 }
 
+impl Node {
+    /// Value with which we order `Node`s.
+    fn sort_key(&self) -> impl Ord {
+        let (variant_index, _) = self.variant_index_arity();
+        let (Self::External(def_id) | Self::Local(def_id, _)) = self;
+        (variant_index, def_id.index, def_id.krate)
+    }
+}
+
+/// Manual impls because `DefId` is not orderable.
+impl PartialOrd for Node {
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
+        Some(self.cmp(other))
+    }
+}
+impl Ord for Node {
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+        self.sort_key().cmp(&other.sort_key())
+    }
+}
+
 struct Graph {
     dgraph: DiGraphMap<Node, ()>,
 }

charon/src/lib.rs

@@ -15,12 +15,13 @@
 #![feature(box_patterns)]
 // For rustdoc: prevents overflows
 #![recursion_limit = "256"]
-#![feature(trait_alias)]
-#![feature(let_chains)]
 #![feature(if_let_guard)]
-#![feature(iter_array_chunks)]
 #![feature(impl_trait_in_assoc_type)]
+#![feature(iter_array_chunks)]
 #![feature(iterator_try_collect)]
+#![feature(let_chains)]
+#![feature(lint_reasons)]
+#![feature(trait_alias)]
 
 extern crate rustc_ast;
 extern crate rustc_ast_pretty;

charon/src/translate/translate_crate_to_ullbc.rs

@@ -101,8 +101,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
                 trace!("impl");
                 // Sanity checks
                 // TODO: make proper error messages
-                use rustc_hir::{Defaultness, ImplPolarity, Unsafety};
-                assert!(impl_block.unsafety == Unsafety::Normal);
+                use rustc_hir::{Defaultness, ImplPolarity, Safety};
+                assert!(impl_block.safety == Safety::Safe);
                 // About polarity:
                 // [https://doc.rust-lang.org/beta/unstable-book/language-features/negative-impls.html]
                 // Not sure about what I should do about it. Should I do anything, actually?

charon/src/translate/translate_ctx.rs

@@ -19,12 +19,12 @@ use hax_frontend_exporter::SInto;
 use linked_hash_set::LinkedHashSet;
 use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
 use rustc_error_messages::MultiSpan;
-use rustc_errors::DiagCtxt;
+use rustc_errors::DiagCtxtHandle;
 use rustc_hir::def_id::DefId;
 use rustc_hir::Node as HirNode;
 use rustc_middle::ty::TyCtxt;
 use serde::{Deserialize, Serialize};
-use std::cmp::{Ord, Ordering, PartialOrd};
+use std::cmp::{Ord, PartialOrd};
 use std::collections::{BTreeMap, HashMap, HashSet, VecDeque};
 use std::fmt;
 
@@ -71,12 +71,31 @@ pub(crate) use error_assert;
 /// dependencies, especially if some external dependencies don't extract:
 /// we use this information to tell the user what is the code which
 /// (transitively) lead to the extraction of those problematic dependencies.
-#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
 pub struct DepSource {
     pub src_id: DefId,
     pub span: rustc_span::Span,
 }
 
+impl DepSource {
+    /// Value with which we order `DepSource`s.
+    fn sort_key(&self) -> impl Ord {
+        (self.src_id.index, self.src_id.krate)
+    }
+}
+
+/// Manual impls because `DefId` is not orderable.
+impl PartialOrd for DepSource {
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
+        Some(self.cmp(other))
+    }
+}
+impl Ord for DepSource {
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+        self.sort_key().cmp(&other.sort_key())
+    }
+}
+
 impl DepSource {
     pub(crate) fn make(src_id: DefId, span: rustc_span::Span) -> Option<Self> {
         Some(DepSource { src_id, span })
@@ -174,23 +193,24 @@ impl OrdRustId {
     }
 }
 
-impl PartialOrd for OrdRustId {
-    fn partial_cmp(&self, other: &OrdRustId) -> Option<Ordering> {
-        let (vid0, _) = self.variant_index_arity();
-        let (vid1, _) = other.variant_index_arity();
-        if vid0 != vid1 {
-            Option::Some(vid0.cmp(&vid1))
-        } else {
-            let id0 = self.get_id();
-            let id1 = other.get_id();
-            Some(id0.cmp(&id1))
-        }
+impl OrdRustId {
+    /// Value with which we order values.
+    fn sort_key(&self) -> impl Ord {
+        let (variant_index, _) = self.variant_index_arity();
+        let def_id = self.get_id();
+        (variant_index, def_id.index, def_id.krate)
     }
 }
 
+/// Manual impls because `DefId` is not orderable.
+impl PartialOrd for OrdRustId {
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
+        Some(self.cmp(other))
+    }
+}
 impl Ord for OrdRustId {
-    fn cmp(&self, other: &OrdRustId) -> Ordering {
-        self.partial_cmp(other).unwrap()
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+        self.sort_key().cmp(&other.sort_key())
     }
 }
 
@@ -251,7 +271,7 @@ pub struct ErrorCtx<'ctx> {
     pub errors_as_warnings: bool,
 
     /// The compiler session, used for displaying errors.
-    pub dcx: &'ctx DiagCtxt,
+    pub dcx: DiagCtxtHandle<'ctx>,
     /// The ids of the declarations for which extraction we encountered errors.
     pub decls_with_errors: HashSet<DefId>,
     /// The ids of the declarations we completely failed to extract and had to ignore.

charon/src/translate/translate_functions_to_ullbc.rs

@@ -55,14 +55,17 @@ fn translate_borrow_kind(borrow_kind: hax::BorrowKind) -> BorrowKind {
             hax::MutBorrowKind::TwoPhaseBorrow => BorrowKind::TwoPhaseMut,
             hax::MutBorrowKind::ClosureCapture => unimplemented!(),
         },
-        hax::BorrowKind::Fake => BorrowKind::Shallow,
+        hax::BorrowKind::Fake(hax::FakeBorrowKind::Shallow) => BorrowKind::Shallow,
+        // This one is used only in deref patterns.
+        hax::BorrowKind::Fake(hax::FakeBorrowKind::Deep) => unimplemented!(),
     }
 }
 
 fn translate_unaryop_kind(binop: hax::UnOp) -> UnOp {
     match binop {
         hax::UnOp::Not => UnOp::Not,
         hax::UnOp::Neg => UnOp::Neg,
+        hax::UnOp::PtrMetadata => unimplemented!("Unop::PtrMetadata"),
     }
 }
 
@@ -72,27 +75,33 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
         span: rustc_span::Span,
         binop: hax::BinOp,
     ) -> Result<BinOp, Error> {
-        match binop {
-            hax::BinOp::BitXor => Ok(BinOp::BitXor),
-            hax::BinOp::BitAnd => Ok(BinOp::BitAnd),
-            hax::BinOp::BitOr => Ok(BinOp::BitOr),
-            hax::BinOp::Eq => Ok(BinOp::Eq),
-            hax::BinOp::Lt => Ok(BinOp::Lt),
-            hax::BinOp::Le => Ok(BinOp::Le),
-            hax::BinOp::Ne => Ok(BinOp::Ne),
-            hax::BinOp::Ge => Ok(BinOp::Ge),
-            hax::BinOp::Gt => Ok(BinOp::Gt),
-            hax::BinOp::Div => Ok(BinOp::Div),
-            hax::BinOp::Rem => Ok(BinOp::Rem),
-            hax::BinOp::Add => Ok(BinOp::Add),
-            hax::BinOp::Sub => Ok(BinOp::Sub),
-            hax::BinOp::Mul => Ok(BinOp::Mul),
-            hax::BinOp::Shl => Ok(BinOp::Shl),
-            hax::BinOp::Shr => Ok(BinOp::Shr),
+        Ok(match binop {
+            hax::BinOp::BitXor => BinOp::BitXor,
+            hax::BinOp::BitAnd => BinOp::BitAnd,
+            hax::BinOp::BitOr => BinOp::BitOr,
+            hax::BinOp::Eq => BinOp::Eq,
+            hax::BinOp::Lt => BinOp::Lt,
+            hax::BinOp::Le => BinOp::Le,
+            hax::BinOp::Ne => BinOp::Ne,
+            hax::BinOp::Ge => BinOp::Ge,
+            hax::BinOp::Gt => BinOp::Gt,
+            hax::BinOp::Div => BinOp::Div,
+            hax::BinOp::Rem => BinOp::Rem,
+            hax::BinOp::Add => BinOp::Add,
+            hax::BinOp::Sub => BinOp::Sub,
+            hax::BinOp::Mul => BinOp::Mul,
+            hax::BinOp::AddWithOverflow => BinOp::CheckedAdd,
+            hax::BinOp::SubWithOverflow => BinOp::CheckedSub,
+            hax::BinOp::MulWithOverflow => BinOp::CheckedMul,
+            hax::BinOp::Shl => BinOp::Shl,
+            hax::BinOp::Shr => BinOp::Shr,
+            hax::BinOp::Cmp => {
+                error_or_panic!(self, span, "Unsupported binary operation: Cmp")
+            }
             hax::BinOp::Offset => {
                 error_or_panic!(self, span, "Unsupported binary operation: offset")
             }
-        }
+        })
     }
 
     pub(crate) fn get_item_kind(
@@ -644,12 +653,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     }
                     (
                         hax::CastKind::PointerCoercion(hax::PointerCoercion::ClosureFnPointer(
-                            unsafety,
+                            safety,
                         )),
                         src_ty @ Ty::Arrow(..),
                         tgt_ty @ Ty::Arrow(..),
                     ) => {
-                        assert!(*unsafety == hax::Unsafety::Normal);
+                        assert!(*safety == hax::Safety::Safe);
                         let src_ty = src_ty.clone();
                         let tgt_ty = tgt_ty.clone();
                         Ok(Rvalue::UnaryOp(
@@ -686,21 +695,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 self.translate_operand(span, left)?,
                 self.translate_operand(span, right)?,
             )),
-            hax::Rvalue::CheckedBinaryOp(binop, (left, right)) => {
-                let binop = match binop {
-                    hax::BinOp::Add => BinOp::CheckedAdd,
-                    hax::BinOp::Sub => BinOp::CheckedSub,
-                    hax::BinOp::Mul => BinOp::CheckedMul,
-                    _ => {
-                        error_or_panic!(self, span, "Only Add, Sub and Mul are supported as checked binary operations, found {binop:?}");
-                    }
-                };
-                Ok(Rvalue::BinaryOp(
-                    binop,
-                    self.translate_operand(span, left)?,
-                    self.translate_operand(span, right)?,
-                ))
-            }
             hax::Rvalue::NullaryOp(nullop, _ty) => {
                 trace!("NullOp: {:?}", nullop);
                 // Nullary operations are very low-level and shouldn't be necessary
@@ -824,7 +818,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
                         Ok(Rvalue::Aggregate(akind, operands_t))
                     }
-                    hax::AggregateKind::Coroutine(..) => {
+                    hax::AggregateKind::RawPtr(..) => {
+                        error_or_panic!(self, span, "Raw pointers are not supported");
+                    }
+                    hax::AggregateKind::Coroutine(..)
+                    | hax::AggregateKind::CoroutineClosure(..) => {
                         error_or_panic!(self, span, "Coroutines are not supported");
                     }
                 }
@@ -852,7 +850,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         erase_regions: bool,
         def_id: &hax::DefId,
         substs: &Vec<hax::GenericArg>,
-        args: Option<&Vec<hax::Operand>>,
+        args: Option<&Vec<hax::Spanned<hax::Operand>>>,
         trait_refs: &Vec<hax::ImplExpr>,
         trait_info: &Option<hax::ImplExpr>,
     ) -> Result<SubstFunIdOrPanic, Error> {
@@ -892,7 +890,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     // Translate the first argument - note that we use a special
                     // function to translate it: the operand should be of the form:
                     // `move b.0`, and if it is the case it will return `move b`
-                    let arg = &args[0];
+                    let arg = &args[0].node;
                     let t_arg = self.translate_move_box_first_projector_operand(span, arg)?;
                     Ok(vec![t_arg])
                 })
@@ -1297,7 +1295,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         span: rustc_span::Span,
         fun: &hax::FunOperand,
         generics: &Vec<hax::GenericArg>,
-        args: &Vec<hax::Operand>,
+        args: &Vec<hax::Spanned<hax::Operand>>,
         destination: &hax::Place,
         target: &Option<hax::BasicBlock>,
         trait_refs: &Vec<hax::ImplExpr>,
@@ -1388,13 +1386,14 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         &mut self,
         span: rustc_span::Span,
         used_args: Option<Vec<bool>>,
-        args: &Vec<hax::Operand>,
+        args: &Vec<hax::Spanned<hax::Operand>>,
     ) -> Result<Vec<Operand>, Error> {
+        let unspanned_args = args.iter().map(|x| &x.node);
         let args: Vec<&hax::Operand> = match used_args {
-            None => args.iter().collect(),
+            None => unspanned_args.collect(),
             Some(used_args) => {
                 assert!(args.len() == used_args.len());
-                args.iter()
+                unspanned_args
                     .zip(used_args.into_iter())
                     .filter_map(|(param, used)| if used { Some(param) } else { None })
                     .collect()
@@ -1503,7 +1502,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         let tcx = self.t_ctx.tcx;
         let erase_regions = false;
         let span = self.t_ctx.tcx.def_span(def_id);
-        let is_closure = tcx.is_closure(def_id);
+        let is_closure = tcx.is_closure_like(def_id);
         let dep_src = DepSource::make(def_id, span);
 
         // The parameters (and in particular the lifetimes) are split between
@@ -1558,10 +1557,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
             trace!("closure.sig_as_fn_ptr_ty: {:?}", closure.sig_as_fn_ptr_ty());
             trace!("closure.kind_ty: {:?}", closure.kind_ty());
-            trace!(
-                "closure.print_as_impl_trait: {:?}",
-                closure.print_as_impl_trait()
-            );
 
             // Sanity check: the parent subst only contains types and generics
             error_assert!(
@@ -1610,9 +1605,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         //
         // Add the *late-bound* parameters (bound in the signature, can only be lifetimes)
         //
-        let is_unsafe = match signature.value.unsafety {
-            hax::Unsafety::Unsafe => true,
-            hax::Unsafety::Normal => false,
+        let is_unsafe = match signature.value.safety {
+            hax::Safety::Unsafe => true,
+            hax::Safety::Safe => false,
         };
         let bvar_names = signature
             .bound_vars

charon/src/translate/translate_predicates.rs

@@ -58,7 +58,7 @@ impl NonLocalTraitClause {
 
 #[derive(Debug, Clone, EnumIsA, EnumAsGetters, EnumToGetters)]
 pub(crate) enum Predicate {
-    Trait(TraitClauseId),
+    Trait(#[expect(dead_code)] TraitClauseId),
     TypeOutlives(TypeOutlives),
     RegionOutlives(RegionOutlives),
     TraitType(TraitTypeConstraint),