Update rustc

cli/driver/src/exporter.rs

@@ -11,27 +11,26 @@ use rustc_middle::{
     thir,
     thir::{Block, BlockId, Expr, ExprId, ExprKind, Pat, PatKind, Stmt, StmtId, StmtKind, Thir},
 };
-use rustc_session::parse::ParseSess;
 use rustc_span::symbol::Symbol;
 use serde::Serialize;
 use std::cell::RefCell;
 use std::collections::{HashMap, HashSet};
 use std::rc::Rc;
 
 fn report_diagnostics(
+    tcx: TyCtxt<'_>,
     output: &hax_cli_options_engine::Output,
-    session: &rustc_session::Session,
     mapping: &Vec<(hax_frontend_exporter::Span, rustc_span::Span)>,
 ) {
     for d in &output.diagnostics {
         use hax_diagnostics::*;
-        session.span_hax_err(d.convert(mapping).into());
+        tcx.dcx().span_hax_err(d.convert(mapping).into());
     }
 }
 
 fn write_files(
+    tcx: TyCtxt<'_>,
     output: &hax_cli_options_engine::Output,
-    session: &rustc_session::Session,
     backend: hax_cli_options::Backend,
 ) {
     let manifest_dir = std::env::var("CARGO_MANIFEST_DIR").unwrap();
@@ -43,9 +42,9 @@ fn write_files(
     for file in output.files.clone() {
         let path = out_dir.join(&file.path);
         std::fs::create_dir_all(&path.parent().unwrap()).unwrap();
-        session.note_without_error(format!("Writing file {:#?}", path));
+        tcx.dcx().note(format!("Writing file {:#?}", path));
         std::fs::write(&path, file.contents).unwrap_or_else(|e| {
-            session.fatal(format!(
+            tcx.dcx().fatal(format!(
                 "Unable to write to file {:#?}. Error: {:#?}",
                 path, e
             ))
@@ -127,11 +126,11 @@ fn precompute_local_thir_bodies<'tcx>(
         .filter(|ldid| hir.maybe_body_owned_by(*ldid).is_some())
         .map(|ldid| {
             tracing::debug!("⏳ Type-checking THIR body for {:#?}", ldid);
-            let span = hir.span(hir.local_def_id_to_hir_id(ldid));
+            let span = hir.span(tcx.local_def_id_to_hir_id(ldid));
             let (thir, expr) = match tcx.thir_body(ldid) {
                 Ok(x) => x,
                 Err(e) => {
-                    tcx.sess.span_err(
+                    tcx.dcx().span_err(
                         span,
                         "While trying to reach a body's THIR defintion, got a typechecking error.",
                     );
@@ -143,7 +142,7 @@ fn precompute_local_thir_bodies<'tcx>(
             })) {
                 Ok(x) => x,
                 Err(e) => {
-                    tcx.sess.span_err(span, format!("The THIR body of item {:?} was stolen.\nThis is not supposed to happen.\nThis is a bug in Hax's frontend.\nThis is discussed in issue https://github.com/hacspec/hax/issues/27.\nPlease comment this issue if you see this error message!", ldid));
+                    tcx.dcx().span_err(span, format!("The THIR body of item {:?} was stolen.\nThis is not supposed to happen.\nThis is a bug in Hax's frontend.\nThis is discussed in issue https://github.com/hacspec/hax/issues/27.\nPlease comment this issue if you see this error message!", ldid));
                     return (ldid, dummy_thir_body(tcx, span));
                 }
             };
@@ -298,7 +297,7 @@ impl Callbacks for ExtractionCallbacks {
             .into_iter()
             .map(|(k, v)| {
                 use hax_frontend_exporter::*;
-                let sess = compiler.session();
+                let sess = &compiler.sess;
                 (
                     translate_span(k, sess),
                     translate_span(argument_span_of_mac_call(&v), sess),
@@ -432,9 +431,8 @@ impl Callbacks for ExtractionCallbacks {
                     .unwrap();
 
                     let out = engine_subprocess.wait_with_output().unwrap();
-                    let session = compiler.session();
                     if !out.status.success() {
-                        session.fatal(format!(
+                        tcx.dcx().fatal(format!(
                             "{} exited with non-zero code {}\nstdout: {}\n stderr: {}",
                             ENGINE_BINARY_NAME,
                             out.status.code().unwrap_or(-1),
@@ -456,8 +454,8 @@ impl Callbacks for ExtractionCallbacks {
                     let state =
                         hax_frontend_exporter::state::State::new(tcx, options_frontend.clone());
                     report_diagnostics(
+                        tcx,
                         &output,
-                        &session,
                         &spans
                             .into_iter()
                             .map(|span| (span.sinto(&state), span.clone()))
@@ -467,7 +465,7 @@ impl Callbacks for ExtractionCallbacks {
                         serde_json::to_writer(std::io::BufWriter::new(std::io::stdout()), &output)
                             .unwrap()
                     } else {
-                        write_files(&output, &session, backend.backend);
+                        write_files(tcx, &output, backend.backend);
                     }
                     if let Some(debug_json) = &output.debug_json {
                         use hax_cli_options::DebugEngineMode;

cli/driver/src/linter.rs

@@ -28,11 +28,10 @@ impl Callbacks for LinterCallbacks {
         compiler: &Compiler,
         queries: &'tcx Queries<'tcx>,
     ) -> Compilation {
-        let session = compiler.session();
         queries
             .global_ctxt()
             .unwrap()
-            .enter(|tcx| hax_lint::Linter::register(tcx, session, self.ltype));
+            .enter(|tcx| hax_lint::Linter::register(tcx, self.ltype));
 
         Compilation::Continue
     }

engine/lib/concrete_ident/concrete_ident.ml

@@ -15,11 +15,10 @@ module Imported = struct
     | ForeignMod
     | Use
     | GlobalAsm
-    | ClosureExpr
+    | Closure
     | Ctor
     | AnonConst
-    | ImplTrait
-    | ImplTraitAssocTy
+    | OpaqueTy
     | TypeNs of string
     | ValueNs of string
     | MacroNs of string
@@ -32,11 +31,10 @@ module Imported = struct
     | ForeignMod -> ForeignMod
     | Use -> Use
     | GlobalAsm -> GlobalAsm
-    | ClosureExpr -> ClosureExpr
+    | Closure -> Closure
     | Ctor -> Ctor
     | AnonConst -> AnonConst
-    | ImplTrait -> ImplTrait
-    | ImplTraitAssocTy -> ImplTraitAssocTy
+    | OpaqueTy -> OpaqueTy
     | TypeNs s -> TypeNs s
     | ValueNs s -> ValueNs s
     | MacroNs s -> MacroNs s

engine/lib/import_thir.ml

@@ -844,6 +844,7 @@ end) : EXPR = struct
       | Or { pats } -> POr { subpats = List.map ~f:c_pat pats }
       | Slice _ -> unimplemented [ pat.span ] "pat Slice"
       | Range _ -> unimplemented [ pat.span ] "pat Range"
+      | Never -> unimplemented [ pat.span ] "pat Never"
       | Error _ -> unimplemented [ pat.span ] "pat Error"
     in
     { p = v; span; typ }
@@ -1359,19 +1360,21 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
           List.for_all
             ~f:(fun { data; _ } ->
               match data with
-              | Unit _ | Tuple ([], _, _) | Struct ([], _) -> true
+              | Unit _ | Tuple ([], _, _) | Struct { fields = []; _ } -> true
               | _ -> false)
             variants
         in
         let variants =
           List.map
             ~f:
               (fun ({ data; def_id = variant_id; attributes; _ } as original) ->
-              let is_record = [%matches? Types.Struct (_ :: _, _)] data in
+              let is_record =
+                [%matches? Types.Struct { fields = _ :: _; _ }] data
+              in
               let name = Concrete_ident.of_def_id kind variant_id in
               let arguments =
                 match data with
-                | Tuple (fields, _, _) | Struct (fields, _) ->
+                | Tuple (fields, _, _) | Struct { fields; _ } ->
                     List.map
                       ~f:(fun { def_id = id; ty; span; attributes; _ } ->
                         ( Concrete_ident.of_def_id Field id,
@@ -1415,7 +1418,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
           in
           match v with
           | Tuple (fields, _, _) -> mk fields false
-          | Struct ((_ :: _ as fields), _) -> mk fields true
+          | Struct { fields = _ :: _ as fields; _ } -> mk fields true
           | _ -> { name; arguments = []; is_record = false; attrs }
         in
         let variants = [ v ] in

engine/names/extract/build.rs

@@ -46,11 +46,10 @@ fn def_path_item_to_str(path_item: DefPathItem) -> String {
         DefPathItem::ForeignMod => "ForeignMod".into(),
         DefPathItem::Use => "Use".into(),
         DefPathItem::GlobalAsm => "GlobalAsm".into(),
-        DefPathItem::ClosureExpr => "ClosureExpr".into(),
+        DefPathItem::Closure => "Closure".into(),
         DefPathItem::Ctor => "Ctor".into(),
         DefPathItem::AnonConst => "AnonConst".into(),
-        DefPathItem::ImplTrait => "ImplTrait".into(),
-        DefPathItem::ImplTraitAssocTy => "ImplTraitAssocTy".into(),
+        DefPathItem::OpaqueTy => "OpaqueTy".into(),
     }
 }
 

frontend/diagnostics/src/error.rs

@@ -1,21 +1,16 @@
 // rustc errors
 extern crate rustc_errors;
-use rustc_errors::DiagnosticId;
-
-// rustc session
-extern crate rustc_session;
-use rustc_session::Session;
+use rustc_errors::{DiagCtxt, DiagnosticId};
 
 // rustc data_structures
 extern crate rustc_data_structures;
-use rustc_data_structures::sync::Lrc;
 
 // rustc span
 extern crate rustc_span;
 use rustc_span::Span;
 
-pub fn explicit_lifetime(session: &Lrc<Session>, span: Span) {
-    session.span_warn_with_code(
+pub fn explicit_lifetime(dcx: &DiagCtxt, span: Span) {
+    dcx.span_warn_with_code(
         span,
         "[Hax] Explicit lifetimes are not supported",
         DiagnosticId::Lint {
@@ -26,8 +21,8 @@ pub fn explicit_lifetime(session: &Lrc<Session>, span: Span) {
     );
 }
 
-pub fn mut_borrow_let(session: &Lrc<Session>, span: Span) {
-    session.span_warn_with_code(
+pub fn mut_borrow_let(dcx: &DiagCtxt, span: Span) {
+    dcx.span_warn_with_code(
         span,
         "[Hax] Mutable borrows are not supported",
         DiagnosticId::Lint {
@@ -38,8 +33,8 @@ pub fn mut_borrow_let(session: &Lrc<Session>, span: Span) {
     );
 }
 
-pub fn extern_crate(session: &Lrc<Session>, span: Span) {
-    session.span_warn_with_code(
+pub fn extern_crate(dcx: &DiagCtxt, span: Span) {
+    dcx.span_warn_with_code(
         span,
         "[Hax] External items need a model",
         DiagnosticId::Lint {
@@ -50,8 +45,8 @@ pub fn extern_crate(session: &Lrc<Session>, span: Span) {
     );
 }
 
-pub fn no_trait_objects(session: &Lrc<Session>, span: Span) {
-    session.span_warn_with_code(
+pub fn no_trait_objects(dcx: &DiagCtxt, span: Span) {
+    dcx.span_warn_with_code(
         span,
         "[Hax] Trait objects are not supported",
         DiagnosticId::Lint {
@@ -62,8 +57,8 @@ pub fn no_trait_objects(session: &Lrc<Session>, span: Span) {
     );
 }
 
-pub fn no_mut_self(session: &Lrc<Session>, span: Span) {
-    session.span_warn_with_code(
+pub fn no_mut_self(dcx: &DiagCtxt, span: Span) {
+    dcx.span_warn_with_code(
         span,
         "[Hax] Mutable self is not supported",
         DiagnosticId::Lint {
@@ -74,8 +69,8 @@ pub fn no_mut_self(session: &Lrc<Session>, span: Span) {
     );
 }
 
-pub fn no_mut(session: &Lrc<Session>, span: Span) {
-    session.span_warn_with_code(
+pub fn no_mut(dcx: &DiagCtxt, span: Span) {
+    dcx.span_warn_with_code(
         span,
         "[Hax] Mutable arguments are not supported",
         DiagnosticId::Lint {
@@ -86,8 +81,8 @@ pub fn no_mut(session: &Lrc<Session>, span: Span) {
     );
 }
 
-pub fn no_assoc_items(session: &Lrc<Session>, span: Span) {
-    session.span_warn_with_code(
+pub fn no_assoc_items(dcx: &DiagCtxt, span: Span) {
+    dcx.span_warn_with_code(
         span,
         "[Hax] Associated items are not supported",
         DiagnosticId::Lint {
@@ -98,8 +93,8 @@ pub fn no_assoc_items(session: &Lrc<Session>, span: Span) {
     );
 }
 
-pub fn unsupported_item(session: &Lrc<Session>, span: Span, ident: String) {
-    session.span_warn_with_code(
+pub fn unsupported_item(dcx: &DiagCtxt, span: Span, ident: String) {
+    dcx.span_warn_with_code(
         span,
         format!("[Hax] {ident:?} is not supported"),
         DiagnosticId::Lint {
@@ -110,8 +105,8 @@ pub fn unsupported_item(session: &Lrc<Session>, span: Span, ident: String) {
     );
 }
 
-pub fn no_fn_mut(session: &Lrc<Session>, span: Span) {
-    session.span_warn_with_code(
+pub fn no_fn_mut(dcx: &DiagCtxt, span: Span) {
+    dcx.span_warn_with_code(
         span,
         "[Hax] FnMut is not supported",
         DiagnosticId::Lint {
@@ -122,8 +117,8 @@ pub fn no_fn_mut(session: &Lrc<Session>, span: Span) {
     );
 }
 
-pub fn no_where_predicate(session: &Lrc<Session>, span: Span) {
-    session.span_warn_with_code(
+pub fn no_where_predicate(dcx: &DiagCtxt, span: Span) {
+    dcx.span_warn_with_code(
         span,
         "[Hax] Where predicates are not supported",
         DiagnosticId::Lint {
@@ -134,8 +129,8 @@ pub fn no_where_predicate(session: &Lrc<Session>, span: Span) {
     );
 }
 
-pub fn no_async_await(session: &Lrc<Session>, span: Span) {
-    session.span_warn_with_code(
+pub fn no_async_await(dcx: &DiagCtxt, span: Span) {
+    dcx.span_warn_with_code(
         span,
         "[Hax] Async and await are not supported",
         DiagnosticId::Lint {
@@ -146,8 +141,8 @@ pub fn no_async_await(session: &Lrc<Session>, span: Span) {
     );
 }
 
-pub fn no_unsafe(session: &Lrc<Session>, span: Span) {
-    session.span_warn_with_code(
+pub fn no_unsafe(dcx: &DiagCtxt, span: Span) {
+    dcx.span_warn_with_code(
         span,
         "[Hax] Unsafe code is not supported",
         DiagnosticId::Lint {
@@ -158,8 +153,8 @@ pub fn no_unsafe(session: &Lrc<Session>, span: Span) {
     );
 }
 
-pub fn unsupported_loop(session: &Lrc<Session>, span: Span) {
-    session.span_warn_with_code(
+pub fn unsupported_loop(dcx: &DiagCtxt, span: Span) {
+    dcx.span_warn_with_code(
         span,
         "[Hax] loop and while are not supported",
         DiagnosticId::Lint {
@@ -170,8 +165,8 @@ pub fn unsupported_loop(session: &Lrc<Session>, span: Span) {
     );
 }
 
-pub fn no_union(session: &Lrc<Session>, span: Span) {
-    session.span_warn_with_code(
+pub fn no_union(dcx: &DiagCtxt, span: Span) {
+    dcx.span_warn_with_code(
         span,
         "[Hax] Unions are not supported",
         DiagnosticId::Lint {
@@ -182,8 +177,8 @@ pub fn no_union(session: &Lrc<Session>, span: Span) {
     );
 }
 
-pub fn derive_external_trait(session: &Lrc<Session>, span: Span, trait_name: String) {
-    session.span_warn_with_code(
+pub fn derive_external_trait(dcx: &DiagCtxt, span: Span, trait_name: String) {
+    dcx.span_warn_with_code(
         span,
         format!("[Hax] Implementation of external trait {trait_name} will require a model"),
         DiagnosticId::Lint {

frontend/diagnostics/src/lib.rs

@@ -14,7 +14,8 @@ use serde::{Deserialize, Serialize};
 pub trait SessionExtTrait {
     fn span_hax_err<S: Into<MultiSpan> + Clone>(&self, diag: Diagnostics<S>);
 }
-impl SessionExtTrait for rustc_session::Session {
+
+impl SessionExtTrait for rustc_errors::DiagCtxt {
     fn span_hax_err<S: Into<MultiSpan> + Clone>(&self, diag: Diagnostics<S>) {
         let span: MultiSpan = diag.span.clone().into();
         let diag = diag.set_span(span.clone());

frontend/exporter/src/constant_utils.rs

@@ -246,7 +246,7 @@ pub(crate) fn scalar_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
                 )
             });
             use rustc_middle::mir::interpret::GlobalAlloc;
-            let contents = match tcx.global_alloc(pointer.provenance.s_unwrap(s)) {
+            let contents = match tcx.global_alloc(pointer.provenance.s_unwrap(s).alloc_id()) {
                 GlobalAlloc::Static(did) => ConstantExprKind::GlobalName { id: did.sinto(s), generics: Vec::new(), trait_refs: Vec::new() },
                 GlobalAlloc::Memory(alloc) => {
                     let values = alloc.inner().get_bytes_unchecked(rustc_middle::mir::interpret::AllocRange {