Bump hax & rustc

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/hacspec/hax", branch = "main" }
+hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "update-rustc2" }
 # hax-frontend-exporter = { path = "../../hax/frontend/exporter" }
 macros = { path = "./macros" }
 

charon/src/ast/meta_utils.rs

@@ -3,7 +3,7 @@ use crate::meta::*;
 use hax_frontend_exporter as hax;
 use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
-use rustc_session::Session;
+use rustc_span::source_map::SourceMap;
 use std::cmp::Ordering;
 use std::iter::Iterator;
 use std::path::Component;
@@ -133,11 +133,7 @@ pub fn convert_loc(loc: hax::Loc) -> Loc {
 }
 
 // TODO: remove?
-pub fn span_to_string(sess: &Session, span: rustc_span::Span) -> String {
-    // Retrieve the source map, which contains information about the source file:
-    // we need it to be able to interpret the span.
-    let source_map = sess.source_map();
-
+pub fn span_to_string(source_map: &SourceMap, span: rustc_span::Span) -> String {
     // Convert the span to lines
     let (beg, end) = source_map.is_valid_span(span).unwrap();
 

charon/src/ast/names_utils.rs

@@ -250,7 +250,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
                         kind,
                     }));
                 }
-                DefPathData::ImplTrait => {
+                DefPathData::OpaqueTy => {
                     // TODO: do nothing for now
                 }
                 DefPathData::MacroNs(symbol) => {
@@ -263,7 +263,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
                     // instance to filter opaque modules.
                     name.push(PathElem::Ident(symbol.to_string(), disambiguator));
                 }
-                DefPathData::ClosureExpr => {
+                DefPathData::Closure => {
                     // TODO: this is not very satisfactory, but on the other hand
                     // we should be able to extract closures in local let-bindings
                     // (i.e., we shouldn't have to introduce top-level let-bindings).

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

@@ -9,7 +9,6 @@ use regex::Regex;
 use rustc_driver::{Callbacks, Compilation};
 use rustc_interface::{interface::Compiler, Queries};
 use rustc_middle::ty::TyCtxt;
-use rustc_session::Session;
 use std::fmt;
 use std::ops::Deref;
 use std::panic::{self, AssertUnwindSafe};
@@ -101,7 +100,7 @@ impl Callbacks for CharonCallbacks {
     /// possible (i.e., after parsing). See [charon_lib::get_mir].
     fn after_crate_root_parsing<'tcx>(
         &mut self,
-        c: &Compiler,
+        _c: &Compiler,
         queries: &'tcx Queries<'tcx>,
     ) -> Compilation {
         // Set up our own `DefId` debug routine.
@@ -113,8 +112,7 @@ impl Callbacks for CharonCallbacks {
             .unwrap()
             .get_mut()
             .enter(|tcx| {
-                let session = c.session();
-                let crate_data = translate(session, tcx, self)?;
+                let crate_data = translate(tcx, self)?;
                 self.crate_data = Some(crate_data);
                 Ok::<(), ()>(())
             })
@@ -208,11 +206,7 @@ pub fn get_args_crate_index<T: Deref<Target = str>>(args: &[T]) -> Option<usize>
 ///
 /// This function is a callback function for the Rust compiler.
 #[allow(clippy::result_unit_err)]
-pub fn translate(
-    sess: &Session,
-    tcx: TyCtxt,
-    internal: &mut CharonCallbacks,
-) -> Result<export::CrateData, ()> {
+pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> Result<export::CrateData, ()> {
     trace!();
     let options = &internal.options;
 
@@ -246,11 +240,10 @@ pub fn translate(
     // # Translate the declarations in the crate.
     // We translate the declarations in an ad-hoc order, and do not group
     // the mutually recursive groups - we do this in the next step.
-    let mut ctx =
-        match translate_crate_to_ullbc::translate(crate_name, options, sess, tcx, mir_level) {
-            Ok(ctx) => ctx,
-            Err(_) => return Err(()),
-        };
+    let mut ctx = match translate_crate_to_ullbc::translate(crate_name, options, tcx, mir_level) {
+        Ok(ctx) => ctx,
+        Err(_) => return Err(()),
+    };
 
     if options.print_ullbc {
         info!("# ULLBC after translation from MIR:\n\n{ctx}\n");

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

@@ -6,7 +6,6 @@ extern crate rustc_driver;
 extern crate rustc_hir;
 extern crate rustc_interface;
 extern crate rustc_middle;
-extern crate rustc_session;
 extern crate rustc_span;
 
 #[macro_use]

charon/src/lib.rs

@@ -26,10 +26,10 @@ extern crate rustc_ast;
 extern crate rustc_ast_pretty;
 extern crate rustc_attr;
 extern crate rustc_error_messages;
+extern crate rustc_errors;
 extern crate rustc_hir;
 extern crate rustc_index;
 extern crate rustc_middle;
-extern crate rustc_session;
 extern crate rustc_span;
 extern crate rustc_target;
 

charon/src/translate/translate_crate_to_ullbc.rs

@@ -9,7 +9,6 @@ use hax_frontend_exporter::SInto;
 use rustc_hir::def_id::DefId;
 use rustc_hir::{ForeignItemKind, ImplItemKind, Item, ItemKind};
 use rustc_middle::ty::TyCtxt;
-use rustc_session::Session;
 use std::collections::{HashMap, HashSet};
 
 impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
@@ -342,10 +341,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
 pub fn translate<'tcx, 'ctx>(
     crate_name: String,
     options: &CliOpts,
-    session: &'ctx Session,
     tcx: TyCtxt<'tcx>,
     mir_level: MirLevel,
-) -> Result<TransformCtx<'ctx>, Error> {
+) -> Result<TransformCtx<'tcx>, Error> {
     let hax_state = hax::state::State::new(
         tcx,
         hax::options::Options {
@@ -364,7 +362,7 @@ pub fn translate<'tcx, 'ctx>(
         errors: ErrorCtx {
             continue_on_failure: !options.abort_on_error,
             errors_as_warnings: options.errors_as_warnings,
-            session,
+            dcx: tcx.dcx(),
             decls_with_errors: HashSet::new(),
             ignored_failed_decls: HashSet::new(),
             dep_sources: HashMap::new(),
@@ -397,10 +395,8 @@ pub fn translate<'tcx, 'ctx>(
     let hir = tcx.hir();
     for item_id in hir.root_module().item_ids {
         let item_id = item_id.hir_id();
-        let node = hir.find(item_id).unwrap();
-        let item = match node {
-            rustc_hir::Node::Item(item) => item,
-            _ => unreachable!(),
+        let rustc_hir::Node::Item(item) = tcx.hir_node(item_id) else {
+            unreachable!()
         };
         ctx.register_local_hir_item(true, item)?;
     }

charon/src/translate/translate_ctx.rs

@@ -19,10 +19,10 @@ 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_hir::def_id::DefId;
 use rustc_hir::Node as HirNode;
 use rustc_middle::ty::TyCtxt;
-use rustc_session::Session;
 use serde::{Deserialize, Serialize};
 use std::cmp::{Ord, Ordering, PartialOrd};
 use std::collections::{BTreeMap, HashMap, HashSet, VecDeque};
@@ -251,7 +251,7 @@ pub struct ErrorCtx<'ctx> {
     pub errors_as_warnings: bool,
 
     /// The compiler session, used for displaying errors.
-    pub session: &'ctx Session,
+    pub dcx: &'ctx DiagCtxt,
     /// 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.
@@ -389,9 +389,9 @@ impl ErrorCtx<'_> {
     pub(crate) fn span_err_no_register<S: Into<MultiSpan>>(&self, span: S, msg: &str) {
         let msg = msg.to_string();
         if self.errors_as_warnings {
-            self.session.span_warn(span, msg);
+            self.dcx.span_warn(span, msg);
         } else {
-            self.session.span_err(span, msg);
+            self.dcx.span_err(span, msg);
         }
     }
 
@@ -596,9 +596,12 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
 
     /// Returns the attributes (`#[...]`) of this node.
     pub(crate) fn node_attributes(&self, id: DefId) -> &[rustc_ast::Attribute] {
-        let hir = self.tcx.hir();
         id.as_local()
-            .map(|local_def_id| hir.attrs(hir.local_def_id_to_hir_id(local_def_id)))
+            .map(|local_def_id| {
+                self.tcx
+                    .hir()
+                    .attrs(self.tcx.local_def_id_to_hir_id(local_def_id))
+            })
             .unwrap_or_default()
     }
 
@@ -684,7 +687,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
             | Ctor { .. }
             | ExternCrate
             | ForeignMod
-            | Coroutine
             | GlobalAsm
             | InlineConst
             | LifetimeParam
@@ -702,10 +704,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
 
     /// Whether this item is in an `extern { .. }` block, in which case it has no body.
     pub(crate) fn id_is_extern_item(&mut self, id: DefId) -> bool {
-        id.as_local().is_some_and(|local_def_id| {
-            let node = self.tcx.hir().find_by_def_id(local_def_id);
-            matches!(node, Some(HirNode::ForeignItem(_)))
-        })
+        self.tcx
+            .hir()
+            .get_if_local(id)
+            .is_some_and(|node| matches!(node, HirNode::ForeignItem(_)))
     }
 
     pub(crate) fn is_opaque_name(&self, name: &Name) -> bool {

charon/src/translate/translate_functions_to_ullbc.rs

@@ -824,7 +824,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
                         Ok(Rvalue::Aggregate(akind, operands_t))
                     }
-                    hax::AggregateKind::Coroutine(_def_id, _subst, _movability) => {
+                    hax::AggregateKind::Coroutine(..) => {
                         error_or_panic!(self, span, "Coroutines are not supported");
                     }
                 }
@@ -869,7 +869,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         // sometimes introduces very low-level functions, which we need to
         // catch early - in particular, before we start translating types and
         // arguments, because we won't be able to translate some of them.
-        if matches!(builtin_fun, Some(BuiltinFun::BoxFree)) {
+        let sfid = if matches!(builtin_fun, Some(BuiltinFun::BoxFree)) {
             assert!(!is_local);
 
             // This deallocates a box.
@@ -903,8 +903,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 func: FunIdOrTraitMethodRef::mk_assumed(AssumedFunId::BoxFree),
                 generics: GenericArgs::new_from_types(vec![t_ty]),
             };
-            let sfid = SubstFunId { func, args };
-            Ok(SubstFunIdOrPanic::Fun(sfid))
+            SubstFunId { func, args }
         } else {
             // Retrieve the lists of used parameters, in case of non-local
             // definitions
@@ -945,7 +944,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
             // Check if the function is considered primitive: primitive
             // functions benefit from special treatment.
-            if let Some(builtin_fun) = builtin_fun {
+            let func = if let Some(builtin_fun) = builtin_fun {
                 // Primitive function.
                 //
                 // Note that there are subtleties with regards to the way types parameters
@@ -992,22 +991,14 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     }
                 };
 
-                let func = FnPtr {
-                    func: FunIdOrTraitMethodRef::Fun(FunId::Assumed(aid)),
-                    generics,
-                };
-                let sfid = SubstFunId { func, args };
-                Ok(SubstFunIdOrPanic::Fun(sfid))
+                FunIdOrTraitMethodRef::Fun(FunId::Assumed(aid))
             } else {
                 // Two cases depending on whether we call a trait method or not
                 match trait_info {
                     None => {
                         // "Regular" function call
                         let def_id = self.register_fun_decl_id(span, rust_id);
-                        let func = FunIdOrTraitMethodRef::Fun(FunId::Regular(def_id));
-                        let func = FnPtr { func, generics };
-                        let sfid = SubstFunId { func, args };
-                        Ok(SubstFunIdOrPanic::Fun(sfid))
+                        FunIdOrTraitMethodRef::Fun(FunId::Regular(def_id))
                     }
                     Some(trait_info) => {
                         // Trait method
@@ -1023,18 +1014,16 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         let trait_method_fun_id = self.register_fun_decl_id(span, rust_id);
                         let method_name = self.t_ctx.translate_trait_item_name(rust_id)?;
 
-                        let func = FunIdOrTraitMethodRef::Trait(
-                            impl_expr,
-                            method_name,
-                            trait_method_fun_id,
-                        );
-                        let func = FnPtr { func, generics };
-                        let sfid = SubstFunId { func, args };
-                        Ok(SubstFunIdOrPanic::Fun(sfid))
+                        FunIdOrTraitMethodRef::Trait(impl_expr, method_name, trait_method_fun_id)
                     }
                 }
+            };
+            SubstFunId {
+                func: FnPtr { func, generics },
+                args,
             }
-        }
+        };
+        Ok(SubstFunIdOrPanic::Fun(sfid))
     }
 
     /// Translate a statement

charon/src/translate/translate_predicates.rs

@@ -537,10 +537,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             }
             PredicateKind::AliasRelate(..)
             | PredicateKind::Ambiguous
-            | PredicateKind::ClosureKind(_, _, _)
             | PredicateKind::Coerce(_)
             | PredicateKind::ConstEquate(_, _)
             | PredicateKind::ObjectSafe(_)
+            | PredicateKind::NormalizesTo(_)
             | PredicateKind::Subtype(_) => error_or_panic!(
                 self,
                 span,

charon/src/translate/translate_traits.rs

@@ -393,7 +393,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
         }
         if item_meta.opacity.is_opaque() {
             let ctx = bt_ctx.into_fmt();
-            bt_ctx.t_ctx.errors.session.span_warn(
+            bt_ctx.t_ctx.errors.dcx.span_warn(
                 item_meta.span,
                 format!(
                     "Trait declarations cannot be \"opaque\"; the trait `{}` will be translated as normal.",
@@ -598,7 +598,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
         }
         if item_meta.opacity.is_opaque() {
             let ctx = bt_ctx.into_fmt();
-            bt_ctx.t_ctx.errors.session.span_warn(
+            bt_ctx.t_ctx.errors.dcx.span_warn(
                 item_meta.span,
                 format!(
                     "Trait implementations cannot be \"opaque\"; the impl `{}` will be translated as normal.",