Update rustc all at once

cli/driver/src/callbacks_wrapper.rs

@@ -14,7 +14,7 @@ pub struct CallbacksWrapper<'a> {
 impl<'a> Callbacks for CallbacksWrapper<'a> {
     fn config(&mut self, config: &mut interface::Config) {
         let options = self.options.clone();
-        config.parse_sess_created = Some(Box::new(move |parse_sess| {
+        config.psess_created = Some(Box::new(move |parse_sess| {
             parse_sess.env_depinfo.get_mut().insert((
                 Symbol::intern(hax_cli_options::ENV_VAR_OPTIONS_FRONTEND),
                 Some(Symbol::intern(&serde_json::to_string(&options).unwrap())),

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
             ))
@@ -55,17 +54,21 @@ fn write_files(
 
 type ThirBundle<'tcx> = (Rc<rustc_middle::thir::Thir<'tcx>>, ExprId);
 /// Generates a dummy THIR body with an error literal as first expression
-fn dummy_thir_body<'tcx>(tcx: TyCtxt<'tcx>, span: rustc_span::Span) -> ThirBundle<'tcx> {
+fn dummy_thir_body<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    span: rustc_span::Span,
+    guar: rustc_errors::ErrorGuaranteed,
+) -> ThirBundle<'tcx> {
     use rustc_middle::thir::*;
     let ty = tcx.mk_ty_from_kind(rustc_type_ir::TyKind::Never);
     let mut thir = Thir::new(BodyTy::Const(ty));
-    const ERR_LITERAL: &'static rustc_hir::Lit = &rustc_span::source_map::Spanned {
-        node: rustc_ast::ast::LitKind::Err,
+    let lit_err = tcx.hir_arena.alloc(rustc_span::source_map::Spanned {
+        node: rustc_ast::ast::LitKind::Err(guar),
         span: rustc_span::DUMMY_SP,
-    };
+    });
     let expr = thir.exprs.push(Expr {
         kind: ExprKind::Literal {
-            lit: ERR_LITERAL,
+            lit: lit_err,
             neg: false,
         },
         ty,
@@ -127,24 +130,24 @@ 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(
+                    let guar = tcx.dcx().span_err(
                         span,
                         "While trying to reach a body's THIR defintion, got a typechecking error.",
                     );
-                    return (ldid, dummy_thir_body(tcx, span));
+                    return (ldid, dummy_thir_body(tcx, span, guar));
                 }
             };
             let thir = match std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
                 thir.borrow().clone()
             })) {
                 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));
-                    return (ldid, dummy_thir_body(tcx, span));
+                    let guar = 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, guar));
                 }
             };
             tracing::debug!("✅ Type-checked THIR body for {:#?}", ldid);
@@ -298,7 +301,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),
@@ -362,29 +365,19 @@ impl Callbacks for ExtractionCallbacks {
                         include_extra,
                     };
                     mod from {
-                        pub use hax_cli_options::ExportBodyKind::{
-                            MirBuilt as MB, MirConst as MC, Thir as T,
-                        };
+                        pub use hax_cli_options::ExportBodyKind::{MirBuilt as MB, Thir as T};
                     }
                     mod to {
                         pub type T = hax_frontend_exporter::ThirBody;
                         pub type MB =
                             hax_frontend_exporter::MirBody<hax_frontend_exporter::mir_kinds::Built>;
-                        pub type MC =
-                            hax_frontend_exporter::MirBody<hax_frontend_exporter::mir_kinds::Const>;
                     }
                     kind.sort();
                     kind.dedup();
                     match kind.as_slice() {
                         [from::MB] => driver.to_json::<to::MB>(),
-                        [from::MC] => driver.to_json::<to::MC>(),
                         [from::T] => driver.to_json::<to::T>(),
-                        [from::MB, from::MC] => driver.to_json::<(to::MB, to::MC)>(),
                         [from::T, from::MB] => driver.to_json::<(to::MB, to::T)>(),
-                        [from::T, from::MC] => driver.to_json::<(to::MC, to::T)>(),
-                        [from::T, from::MB, from::MC] => {
-                            driver.to_json::<(to::MB, (to::MC, to::T))>()
-                        }
                         [] => driver.to_json::<()>(),
                         _ => panic!("Unsupported kind {:#?}", kind),
                     }
@@ -432,9 +425,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 +448,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 +459,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
     }

cli/options/src/lib.rs

@@ -360,7 +360,6 @@ pub enum ExporterCommand {
 pub enum ExportBodyKind {
     Thir,
     MirBuilt,
-    MirConst,
 }
 
 #[derive(JsonSchema, Subcommand, Debug, Clone, Serialize, Deserialize)]

engine/lib/ast.ml

@@ -78,9 +78,14 @@ let show_int_kind { size; signedness } =
     |> Option.map ~f:Int.to_string
     |> Option.value ~default:"size")
 
-type float_kind = F32 | F64 [@@deriving show, yojson, hash, compare, eq]
+type float_kind = F16 | F32 | F64 | F128
+[@@deriving show, yojson, hash, compare, eq]
 
-let show_float_kind = function F32 -> "f32" | F64 -> "f64"
+let show_float_kind = function
+  | F16 -> "f16"
+  | F32 -> "f32"
+  | F64 -> "f64"
+  | F128 -> "f128"
 
 type literal =
   | String of string

engine/lib/concrete_ident/concrete_ident.ml

@@ -15,11 +15,11 @@ module Imported = struct
     | ForeignMod
     | Use
     | GlobalAsm
-    | ClosureExpr
+    | Closure
     | Ctor
     | AnonConst
-    | ImplTrait
-    | ImplTraitAssocTy
+    | AnonAdt
+    | OpaqueTy
     | TypeNs of string
     | ValueNs of string
     | MacroNs of string
@@ -32,15 +32,15 @@ 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
     | LifetimeNs s -> LifetimeNs s
+    | AnonAdt -> AnonAdt
 
   let of_disambiguated_def_path_item :
       Types.disambiguated_def_path_item -> disambiguated_def_path_item =

engine/lib/generic_printer/generic_printer.ml

@@ -66,8 +66,7 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
             | Float { value; kind; negative } ->
                 string value
                 |> precede (if negative then minus else empty)
-                |> terminate
-                     (string (match kind with F32 -> "f32" | F64 -> "f64"))
+                |> terminate (string (show_float_kind kind))
             | Bool b -> OCaml.bool b
 
         method generic_value : generic_value fn =
@@ -101,8 +100,7 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
             in
             string signedness ^^ size
 
-        method ty_float : float_kind fn =
-          (function F32 -> "f32" | F64 -> "f64") >> string
+        method ty_float : float_kind fn = show_float_kind >> string
 
         method generic_values : generic_value list fn =
           function

engine/lib/import_thir.ml

@@ -79,12 +79,13 @@ let c_mutability (witness : 'a) : bool -> 'a Ast.mutability = function
 
 let c_borrow_kind span : Thir.borrow_kind -> borrow_kind = function
   | Shared -> Shared
-  | Fake -> unimplemented [ span ] "Shallow borrows"
+  | Fake _ -> unimplemented [ span ] "Shallow borrows"
   | Mut _ -> Mut W.mutable_reference
 
-let c_binding_mode span : Thir.binding_mode -> binding_mode = function
-  | ByValue -> ByValue
-  | ByRef k -> ByRef (c_borrow_kind span k, W.reference)
+let c_binding_mode : Thir.by_ref -> binding_mode = function
+  | No -> ByValue
+  | Yes true -> ByRef (Mut W.mutable_reference, W.reference)
+  | Yes false -> ByRef (Shared, W.reference)
 
 let unit_typ : ty = TApp { ident = `TupleType 0; args = [] }
 
@@ -161,7 +162,7 @@ let c_lit' span negative (lit : Thir.lit_kind) (ty : ty) : extended_literal =
       ^ "] instead.")
   in
   match lit with
-  | Err ->
+  | Err _ ->
       assertion_failure [ span ]
         "[import_thir:literal] got an error literal: this means the Rust \
          compiler or Hax's frontend probably reported errors above."
@@ -256,6 +257,9 @@ end) : EXPR = struct
       | Ge -> Core__cmp__PartialOrd__ge
       | Gt -> Core__cmp__PartialOrd__gt
       | Eq -> Core__cmp__PartialEq__eq
+      | Cmp ->
+          assertion_failure (Span.to_thir span)
+            "`Cmp` binary operator is not suppored"
       | Offset -> Core__ptr__const_ptr__Impl__offset
     in
     let primitive_names_of_binop : Thir.bin_op -> Concrete_ident.name = function
@@ -275,6 +279,9 @@ end) : EXPR = struct
       | Ge -> Rust_primitives__u128__ge
       | Gt -> Rust_primitives__u128__gt
       | Eq -> Rust_primitives__u128__eq
+      | Cmp ->
+          assertion_failure (Span.to_thir span)
+            "`Cmp` binary operator is not suppored"
       | Offset -> Rust_primitives__offset
     in
     let name =
@@ -317,7 +324,7 @@ end) : EXPR = struct
           | Rem -> both int
           | BitXor | BitAnd | BitOr -> both int <|> both bool
           | Shl | Shr -> int <*> int
-          | Lt | Le | Ne | Ge | Gt -> both int <|> both float
+          | Lt | Le | Ne | Ge | Gt | Cmp -> both int <|> both float
           | Eq -> both int <|> both float <|> both bool
           | Offset -> ("", fun _ -> Some "")
         in
@@ -800,13 +807,13 @@ end) : EXPR = struct
           let typ, typ_span = c_canonical_user_type_annotation annotation in
           let pat = c_pat subpattern in
           PAscription { typ; typ_span; pat }
-      | Binding { mode; mutability; subpattern; ty; var; _ } ->
-          let mut = c_mutability W.mutable_variable mutability in
+      | Binding { mode; subpattern; ty; var; _ } ->
+          let mut = c_mutability W.mutable_variable mode.mutability in
           let subpat =
             Option.map ~f:(c_pat &&& Fn.const W.as_pattern) subpattern
           in
           let typ = c_ty pat.span ty in
-          let mode = c_binding_mode pat.span mode in
+          let mode = c_binding_mode mode.by_ref in
           let var = local_ident Expr var in
           PBinding { mut; mode; var; typ; subpat }
       | Variant { info; subpatterns; _ } ->
@@ -844,6 +851,8 @@ 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"
+      | DerefPattern _ -> unimplemented [ pat.span ] "pat DerefPattern"
+      | Never -> unimplemented [ pat.span ] "pat Never"
       | Error _ -> unimplemented [ pat.span ] "pat Error"
     in
     { p = v; span; typ }
@@ -917,7 +926,9 @@ end) : EXPR = struct
     | Char -> TChar
     | Int k -> TInt (c_int_ty k)
     | Uint k -> TInt (c_uint_ty k)
-    | Float k -> TFloat (match k with F32 -> F32 | F64 -> F64)
+    | Float k ->
+        TFloat
+          (match k with F16 -> F16 | F32 -> F32 | F64 -> F64 | F128 -> F128)
     | Arrow value ->
         let ({ inputs; output; _ } : Thir.ty_fn_sig) = value.value in
         let inputs =
@@ -1359,19 +1370,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 +1428,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