Update rustc all at once

cli/driver/src/exporter.rs

@@ -54,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,
@@ -130,20 +134,20 @@ fn precompute_local_thir_bodies<'tcx>(
             let (thir, expr) = match tcx.thir_body(ldid) {
                 Ok(x) => x,
                 Err(e) => {
-                    tcx.dcx().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.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));
+                    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);

engine/lib/concrete_ident/concrete_ident.ml

@@ -18,6 +18,7 @@ module Imported = struct
     | Closure
     | Ctor
     | AnonConst
+    | AnonAdt
     | OpaqueTy
     | TypeNs of string
     | ValueNs of string
@@ -39,6 +40,7 @@ module Imported = struct
     | 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/import_thir.ml

@@ -161,7 +161,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."

engine/names/extract/build.rs

@@ -1,4 +1,3 @@
-use serde_json;
 use serde_json::Value;
 use std::process::{Command, Stdio};
 
@@ -50,6 +49,7 @@ fn def_path_item_to_str(path_item: DefPathItem) -> String {
         DefPathItem::Ctor => "Ctor".into(),
         DefPathItem::AnonConst => "AnonConst".into(),
         DefPathItem::OpaqueTy => "OpaqueTy".into(),
+        DefPathItem::AnonAdt => "AnonAdt".into(),
     }
 }
 

frontend/exporter/src/state.rs

@@ -99,7 +99,7 @@ macro_rules! mk {
 mod types {
     use crate::prelude::*;
     use std::cell::RefCell;
-    use std::collections::{HashMap, HashSet};
+    use std::collections::HashSet;
 
     pub struct LocalContextS {
         pub vars: HashMap<rustc_middle::thir::LocalVarId, String>,

frontend/exporter/src/traits.rs

@@ -403,7 +403,7 @@ pub fn super_clause_to_clause_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>(
         let s = &with_owner_id(s.base(), (), (), impl_trait_ref.def_id());
         clause.predicate_id(s)
     };
-    let new_clause = clause.subst_supertrait(tcx, &impl_trait_ref);
+    let new_clause = clause.instantiate_supertrait(tcx, &impl_trait_ref);
     let impl_expr = new_clause
         .as_predicate()
         .to_opt_poly_trait_pred()?

frontend/exporter/src/types/copied.rs

@@ -736,6 +736,7 @@ pub enum DesugaringKind {
     Await,
     ForLoop,
     WhileLoop,
+    BoundModifier,
 }
 
 /// Reflects [`rustc_span::hygiene::AstPass`]
@@ -1100,6 +1101,15 @@ pub enum TokenKind {
     Todo(String),
 }
 
+impl<S> SInto<S, bool> for rustc_ast::token::IdentIsRaw {
+    fn sinto(&self, _s: &S) -> bool {
+        match self {
+            Self::Yes => true,
+            Self::No => false,
+        }
+    }
+}
+
 /// Reflects [`rustc_ast::token::Token`]
 #[derive(AdtInto)]
 #[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_ast::token::Token, state: S as gstate)]
@@ -1179,7 +1189,7 @@ impl<'tcx, S: ExprState<'tcx>> SInto<S, Expr> for rustc_middle::thir::Expr<'tcx>
                     let contents = kind.sinto(s);
                     use crate::rustc_middle::ty::util::IntTypeExt;
                     let repr_type = tcx
-                        .repr_options_of_def(def.did())
+                        .repr_options_of_def(def.did().as_local().unwrap())
                         .discr_type()
                         .to_ty(s.base().tcx);
                     if repr_type == ty {
@@ -2033,7 +2043,7 @@ pub enum LitKind {
     Int(u128, LitIntType),
     Float(Symbol, LitFloatType),
     Bool(bool),
-    Err,
+    Err(ErrorGuaranteed),
 }
 
 impl<S> SInto<S, u128> for rustc_data_structures::packed::Pu128 {
@@ -3051,7 +3061,7 @@ pub enum ItemKind<Body: IsBody> {
         Generics<Body>,
         #[value({
             let tcx = s.base().tcx;
-            tcx.repr_options_of_def(s.owner_id()).sinto(s)
+            tcx.repr_options_of_def(s.owner_id().as_local().unwrap()).sinto(s)
         })]
         ReprOptions,
     ),

frontend/exporter/src/types/def_id.rs

@@ -61,4 +61,5 @@ pub enum DefPathItem {
     Ctor,
     AnonConst,
     OpaqueTy,
+    AnonAdt,
 }

frontend/exporter/src/types/mir.rs

@@ -900,6 +900,7 @@ pub enum AggregateKind {
     })]
     Closure(DefId, Vec<GenericArg>, Vec<ImplExpr>, MirPolyFnSig),
     Coroutine(DefId, Vec<GenericArg>),
+    CoroutineClosure(DefId, Vec<GenericArg>),
 }
 
 #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)]
@@ -924,6 +925,7 @@ pub enum NullOp {
     SizeOf,
     AlignOf,
     OffsetOf(Vec<(usize, FieldIdx)>),
+    DebugAssertions,
 }
 
 #[derive(AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema)]

hax-lib-macros/src/quote.rs

@@ -13,7 +13,6 @@
 //!  - `:`, the antiquotation is a type.
 
 use crate::prelude::*;
-use quote::ToTokens;
 
 /// Marker that indicates a place where a antiquotation will be inserted
 const SPLIT_MARK: &str = "SPLIT_QUOTE";

hax-lib-macros/src/syn_ext.rs

@@ -7,15 +7,15 @@ pub struct ExprClosure1 {
     pub body: syn::Expr,
 }
 
-pub trait PatExt {
-    // Make sure to remove type ascriptions
-    fn untype(mut pat: syn::Pat) -> syn::Pat {
-        if let syn::Pat::Type(sub) = pat {
-            pat = *sub.pat.clone();
-        }
-        pat
-    }
-}
+// pub trait PatExt {
+//     // Make sure to remove type ascriptions
+//     fn untype(mut pat: syn::Pat) -> syn::Pat {
+//         if let syn::Pat::Type(sub) = pat {
+//             pat = *sub.pat.clone();
+//         }
+//         pat
+//     }
+// }
 
 impl Parse for ExprClosure1 {
     fn parse(ps: ParseStream) -> Result<Self> {

hax-lib-macros/src/utils.rs

@@ -1,19 +1,19 @@
 use crate::prelude::*;
 use crate::rewrite_self::*;
 
-pub trait BlockExt {
-    /// Bring in the scope of the block quantifiers helpers (the `forall` and `exists` functions)
-    fn make_quantifiers_available(&mut self);
-}
+// pub trait BlockExt {
+//     /// Bring in the scope of the block quantifiers helpers (the `forall` and `exists` functions)
+//     fn make_quantifiers_available(&mut self);
+// }
 
-impl BlockExt for Block {
-    fn make_quantifiers_available(&mut self) {
-        self.stmts.insert(
-            0,
-            Stmt::Item(Item::Verbatim(HaxQuantifiers.to_token_stream())),
-        );
-    }
-}
+// impl BlockExt for Block {
+//     fn make_quantifiers_available(&mut self) {
+//         self.stmts.insert(
+//             0,
+//             Stmt::Item(Item::Verbatim(HaxQuantifiers.to_token_stream())),
+//         );
+//     }
+// }
 
 /// `HaxQuantifiers` expands to the definition of the `forall` and `exists` functions
 pub struct HaxQuantifiers;

rust-toolchain.toml

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2024-02-01"
+channel = "nightly-2024-03-01"
 components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ]

test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap

@@ -25,7 +25,7 @@ info:
 exit = 0
 stderr = '''
 Compiling attribute-opaque v0.1.0 (WORKSPACE_ROOT/attribute-opaque)
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+    Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'''
 
 [stdout]
 diagnostics = []

test-harness/src/snapshots/toolchain__attributes into-fstar.snap

@@ -79,7 +79,7 @@ open FStar.Mul
 type t_Foo = | Foo : u8 -> t_Foo
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Ops.Arith.t_Add #t_Foo #t_Foo =
+let impl: Core.Ops.Arith.t_Add #t_Foo #t_Foo true =
   {
     f_Output = t_Foo;
     f_add_pre = (fun (self: t_Foo) (rhs: t_Foo) -> self._0 <. (255uy -! rhs._0 <: u8));

test-harness/src/snapshots/toolchain__enum-repr into-coq.snap

@@ -23,7 +23,7 @@ info:
 exit = 0
 stderr = '''
 Compiling enum-repr v0.1.0 (WORKSPACE_ROOT/enum-repr)
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+    Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'''
 
 [stdout]
 diagnostics = []

test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap

@@ -23,7 +23,7 @@ info:
 exit = 0
 stderr = '''
 Compiling enum-repr v0.1.0 (WORKSPACE_ROOT/enum-repr)
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+    Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'''
 
 [stdout]
 diagnostics = []

test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap

@@ -23,7 +23,7 @@ info:
 exit = 0
 stderr = '''
 Compiling enum-repr v0.1.0 (WORKSPACE_ROOT/enum-repr)
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+    Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'''
 
 [stdout]
 diagnostics = []

test-harness/src/snapshots/toolchain__fnmut lint-rust.snap

@@ -17,6 +17,8 @@ info:
     snapshot:
       stderr: true
       stdout: true
+    include_flag: ~
+    backend_options: ~
 ---
 exit = 0
 stderr = '''
@@ -33,6 +35,20 @@ warning: [Hax] FnMut is not supported
 16 |         F: FnMut(u32) -> u8,
    |            ^^^^^
 
-warning: `fnmut` (lib) generated 2 warnings
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+warning: trait `SomeTrait` is never used
+ --> lint/rust/fnmut/src/lib.rs:5:7
+  |
+5 | trait SomeTrait {
+  |       ^^^^^^^^^
+  |
+  = note: `#[warn(dead_code)]` on by default
+
+warning: struct `UpdatableStruct` is never constructed
+  --> lint/rust/fnmut/src/lib.rs:11:8
+   |
+11 | struct UpdatableStruct {}
+   |        ^^^^^^^^^^^^^^^
+
+warning: `fnmut` (lib) generated 4 warnings
+    Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'''
 stdout = ''

test-harness/src/snapshots/toolchain__generics into-fstar.snap

@@ -23,7 +23,7 @@ info:
 exit = 0
 stderr = '''
 Compiling generics v0.1.0 (WORKSPACE_ROOT/generics)
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+    Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'''
 
 [stdout]
 diagnostics = []

test-harness/src/snapshots/toolchain__interface-only into-fstar.snap

@@ -23,7 +23,7 @@ info:
 exit = 0
 stderr = '''
 Compiling interface-only v0.1.0 (WORKSPACE_ROOT/cli/interface-only)
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+    Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'''
 
 [stdout]
 diagnostics = []

test-harness/src/snapshots/toolchain__literals into-coq.snap

@@ -23,7 +23,7 @@ info:
 exit = 0
 stderr = '''
 Compiling literals v0.1.0 (WORKSPACE_ROOT/literals)
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+    Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'''
 
 [stdout]
 diagnostics = []

test-harness/src/snapshots/toolchain__literals into-fstar.snap

@@ -23,7 +23,7 @@ info:
 exit = 0
 stderr = '''
 Compiling literals v0.1.0 (WORKSPACE_ROOT/literals)
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+    Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'''
 
 [stdout]
 diagnostics = []

test-harness/src/snapshots/toolchain__loops into-fstar.snap

@@ -23,7 +23,7 @@ info:
 exit = 0
 stderr = '''
 Compiling loops v0.1.0 (WORKSPACE_ROOT/loops)
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+    Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'''
 
 [stdout]
 diagnostics = []

test-harness/src/snapshots/toolchain__mut_arg lint-hacspec.snap

@@ -17,6 +17,8 @@ info:
     snapshot:
       stderr: true
       stdout: true
+    include_flag: ~
+    backend_options: ~
 ---
 exit = 0
 stderr = '''
@@ -28,5 +30,5 @@ warning: [Hax] Mutable arguments are not supported
   |                       ^^^^^
 
 warning: `mut_arg` (lib) generated 1 warning
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+    Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'''
 stdout = ''

test-harness/src/snapshots/toolchain__pattern-or into-coq.snap

@@ -23,7 +23,7 @@ info:
 exit = 0
 stderr = '''
 Compiling pattern-or v0.1.0 (WORKSPACE_ROOT/pattern-or)
-    Finished dev [unoptimized + debuginfo] target(s) in XXs'''
+    Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'''
 
 [stdout]
 diagnostics = []