Bump rustc version

cli/driver/src/callbacks_wrapper.rs

@@ -22,12 +22,12 @@ impl<'a> Callbacks for CallbacksWrapper<'a> {
         }));
         self.sub.config(config)
     }
-    fn after_parsing<'tcx>(
+    fn after_crate_root_parsing<'tcx>(
         &mut self,
         compiler: &interface::Compiler,
         queries: &'tcx Queries<'tcx>,
     ) -> Compilation {
-        self.sub.after_parsing(compiler, queries)
+        self.sub.after_crate_root_parsing(compiler, queries)
     }
     fn after_expansion<'tcx>(
         &mut self,
@@ -38,10 +38,9 @@ impl<'a> Callbacks for CallbacksWrapper<'a> {
     }
     fn after_analysis<'tcx>(
         &mut self,
-        early_handler: &rustc_session::EarlyErrorHandler,
         compiler: &interface::Compiler,
         queries: &'tcx Queries<'tcx>,
     ) -> Compilation {
-        self.sub.after_analysis(early_handler, compiler, queries)
+        self.sub.after_analysis(compiler, queries)
     }
 }

cli/driver/src/exporter.rs

@@ -287,7 +287,7 @@ impl From<ExtractionCallbacks> for hax_frontend_exporter_options::Options {
 }
 
 impl Callbacks for ExtractionCallbacks {
-    fn after_parsing<'tcx>(
+    fn after_crate_root_parsing<'tcx>(
         &mut self,
         compiler: &Compiler,
         queries: &'tcx Queries<'tcx>,

cli/driver/src/linter.rs

@@ -16,7 +16,7 @@ impl LinterCallbacks {
 }
 
 impl Callbacks for LinterCallbacks {
-    fn after_parsing<'tcx>(
+    fn after_crate_root_parsing<'tcx>(
         &mut self,
         _compiler: &Compiler,
         queries: &'tcx Queries<'tcx>,

engine/lib/import_thir.ml

@@ -1064,7 +1064,7 @@ end) : EXPR = struct
 
   let c_clause_kind span id (kind : Thir.clause_kind) : impl_ident option =
     match kind with
-    | Trait { is_positive = true; is_const = _; trait_ref } ->
+    | Trait { is_positive = true; trait_ref } ->
         let args = List.map ~f:(c_generic_value span) trait_ref.generic_args in
         let trait = Concrete_ident.of_def_id Trait trait_ref.def_id in
         Some { goal = { trait; args }; name = id }
@@ -1301,13 +1301,13 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
     let c_body = if drop_body then c_expr_drop_body else c_expr in
     (* TODO: things might be unnamed (e.g. constants) *)
     match (item.kind : Thir.item_kind) with
-    | Const (_, body) ->
+    | Const (_, generics, body) ->
         mk
         @@ Fn
              {
                name =
                  Concrete_ident.of_def_id Value (Option.value_exn item.def_id);
-               generics = { params = []; constraints = [] };
+               generics = c_generics generics;
                body = c_body body;
                params = [];
              }

flake.nix

@@ -8,7 +8,11 @@
         flake-utils.follows = "flake-utils";
       };
     };
-    rust-overlay.follows = "crane/rust-overlay";
+    rust-overlay = {
+      url = "github:oxalica/rust-overlay";
+      inputs.flake-utils.follows = "flake-utils";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
     fstar = {
       url = "github:FStarLang/FStar/v2024.01.13";
       inputs = {

frontend/exporter/src/constant_utils.rs

@@ -1,4 +1,5 @@
 use crate::prelude::*;
+use rustc_middle::{mir, ty};
 
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
@@ -188,7 +189,6 @@ pub(crate) fn scalar_int_to_constant_literal<'tcx, S: UnderOwnerState<'tcx>>(
     x: rustc_middle::ty::ScalarInt,
     ty: rustc_middle::ty::Ty,
 ) -> ConstantLiteral {
-    use rustc_middle::ty;
     match ty.kind() {
         ty::Char => ConstantLiteral::Char(
             char::try_from(x)
@@ -222,7 +222,6 @@ pub(crate) fn scalar_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
     span: rustc_span::Span,
 ) -> ConstantExpr {
     use rustc_middle::mir::Mutability;
-    use rustc_middle::ty;
     let cspan = span.sinto(s);
     // The documentation explicitly says not to match on a scalar.
     // We match on the type and use it to convert the value.
@@ -388,21 +387,23 @@ pub trait ConstantExt<'tcx>: Sized + std::fmt::Debug {
         }
     }
 }
-impl<'tcx> ConstantExt<'tcx> for rustc_middle::ty::Const<'tcx> {
+impl<'tcx> ConstantExt<'tcx> for ty::Const<'tcx> {
     fn eval_constant<S: UnderOwnerState<'tcx>>(&self, s: &S) -> Option<Self> {
-        let evaluated = self.eval(s.base().tcx, s.param_env());
+        let evaluated = self.eval(s.base().tcx, s.param_env(), None).ok()?;
+        let evaluated = ty::Const::new(s.base().tcx, ty::ConstKind::Value(evaluated), self.ty());
         (&evaluated != self).then_some(evaluated)
     }
 }
-impl<'tcx> ConstantExt<'tcx> for rustc_middle::mir::ConstantKind<'tcx> {
+impl<'tcx> ConstantExt<'tcx> for mir::ConstantKind<'tcx> {
     fn eval_constant<S: UnderOwnerState<'tcx>>(&self, s: &S) -> Option<Self> {
-        let evaluated = self.eval(s.base().tcx, s.param_env());
+        let evaluated = self.eval(s.base().tcx, s.param_env(), None).ok()?;
+        let evaluated = mir::ConstantKind::Val(evaluated, self.ty());
         (&evaluated != self).then_some(evaluated)
     }
 }
-impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for rustc_middle::ty::Const<'tcx> {
+impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx> {
     fn sinto(&self, s: &S) -> ConstantExpr {
-        use rustc_middle::{query::Key, ty};
+        use rustc_middle::query::Key;
         let span = self.default_span(s.base().tcx);
         let kind = match self.kind() {
             ty::ConstKind::Param(p) => ConstantExprKind::ConstRef { id: p.sinto(s) },
@@ -434,7 +435,6 @@ pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
     ty: rustc_middle::ty::Ty<'tcx>,
     span: rustc_span::Span,
 ) -> ConstantExpr {
-    use rustc_middle::ty;
     let kind = match (valtree, ty.kind()) {
         (_, ty::Ref(_, inner_ty, _)) => {
             ConstantExprKind::Borrow(valtree_to_constant_expr(s, valtree, *inner_ty, span))
@@ -537,7 +537,7 @@ pub fn const_value_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
     use rustc_middle::mir::interpret::ConstValue;
     match val {
         ConstValue::Scalar(scalar) => scalar_to_constant_expr(s, ty, &scalar, span),
-        ConstValue::ByRef { .. } => const_value_reference_to_constant_expr(s, ty, val, span),
+        ConstValue::Indirect { .. } => const_value_reference_to_constant_expr(s, ty, val, span),
         ConstValue::Slice { data, start, end } => {
             let start = start.try_into().unwrap();
             let end = end.try_into().unwrap();

frontend/exporter/src/state.rs

@@ -143,8 +143,8 @@ mod types {
                 macro_infos: Rc::new(HashMap::new()),
                 cached_thirs: Rc::new(HashMap::new()),
                 options: Rc::new(options),
-                /// Always prefer `s.owner_id()` to `s.base().opt_def_id`.
-                /// `opt_def_id` is used in `utils` for error reporting
+                // Always prefer `s.owner_id()` to `s.base().opt_def_id`.
+                // `opt_def_id` is used in `utils` for error reporting
                 opt_def_id: None,
                 local_ctx: Rc::new(RefCell::new(LocalContextS::new())),
                 exported_spans: Rc::new(RefCell::new(HashSet::new())),

frontend/exporter/src/traits.rs

@@ -130,8 +130,8 @@ pub(crate) mod search_clause {
         let erase_and_norm =
             |x| tcx.erase_regions(tcx.try_normalize_erasing_regions(param_env, x).unwrap_or(x));
         // Lifetime and constantness are irrelevant when resolving instances
-        let x = erase_and_norm(x).without_const(tcx);
-        let y = erase_and_norm(y).without_const(tcx);
+        let x = erase_and_norm(x);
+        let y = erase_and_norm(y);
         let sx = format!("{:?}", x.kind().skip_binder());
         let sy = format!("{:?}", y.kind().skip_binder());
         let result = sx == sy;
@@ -324,7 +324,7 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> {
                 generics: generics.sinto(s),
             }
             .with_args(impl_exprs(s, &nested), trait_ref),
-            ImplSource::Param(nested, _constness) => {
+            ImplSource::Param(nested) => {
                 use search_clause::TraitPredicateExt;
                 let tcx = s.base().tcx;
                 let predicates = &tcx.predicates_defined_on_or_above(s.owner_id());
@@ -362,22 +362,19 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> {
                     .with_args(impl_exprs(s, &nested), trait_ref)
                 }
             }
-            ImplSource::Object(data) => {
-                ImplExprAtom::Dyn.with_args(impl_exprs(s, &data.nested), trait_ref)
-            }
             // We ignore the contained obligations here. For example for `(): Send`, the
             // obligations contained would be `[(): Send]`, which leads to an infinite loop. There
             // might be important obligation shere inother cases; we'll have to see if that comes
             // up.
-            ImplSource::Builtin(_ignored) => ImplExprAtom::Builtin {
-                r#trait: self.skip_binder().sinto(s),
+            ImplSource::Builtin(source, _ignored) => {
+                let atom = match source {
+                    BuiltinImplSource::Object { .. } => ImplExprAtom::Dyn,
+                    _ => ImplExprAtom::Builtin {
+                        r#trait: self.skip_binder().sinto(s),
+                    },
+                };
+                atom.with_args(vec![], trait_ref)
             }
-            .with_args(vec![], trait_ref),
-            x => ImplExprAtom::Todo(format!(
-                "ImplExprAtom::Todo(see https://github.com/hacspec/hax/issues/381) {:#?}\n\n{:#?}",
-                x, self
-            ))
-            .with_args(vec![], trait_ref),
         }
     }
 }

frontend/exporter/src/types/copied.rs

@@ -461,6 +461,7 @@ pub enum CanonicalVarInfo {
     PlaceholderRegion(PlaceholderRegion),
     Const(UniverseIndex, Ty),
     PlaceholderConst(PlaceholderConst, Ty),
+    Effect,
 }
 
 /// Reflects [`rustc_middle::ty::UserSelfTy`]
@@ -1031,18 +1032,6 @@ pub struct Stmt {
     pub opt_destruction_scope: Option<Scope>,
 }
 
-/// Reflects [`rustc_ast::ast::MacDelimiter`]
-#[derive(AdtInto)]
-#[args(<S>, from: rustc_ast::ast::MacDelimiter, state: S as _s)]
-#[derive(
-    Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
-)]
-pub enum MacDelimiter {
-    Parenthesis,
-    Bracket,
-    Brace,
-}
-
 /// Reflects [`rustc_ast::token::Delimiter`]
 #[derive(AdtInto)]
 #[args(<S>, from: rustc_ast::token::Delimiter, state: S as _s)]
@@ -1164,7 +1153,7 @@ pub struct Token {
 )]
 pub struct DelimArgs {
     pub dspan: DelimSpan,
-    pub delim: MacDelimiter,
+    pub delim: Delimiter,
     pub tokens: TokenStream,
 }
 
@@ -1602,7 +1591,8 @@ impl Alias {
                 // emit a warning with a lot of debugging information.
                 let poly_trait_ref = if trait_ref.has_escaping_bound_vars() {
                     let trait_ref_and_generics = alias_ty.trait_ref_and_own_args(tcx);
-                    let rebased_generics = alias_ty.rebase_args_onto_impl(alias_ty.args, tcx);
+                    let rebased_generics =
+                        alias_ty.rebase_inherent_args_onto_impl(alias_ty.args, tcx);
                     let norm_rebased_generics = tcx.try_subst_and_normalize_erasing_regions(
                         rebased_generics,
                         s.param_env(),
@@ -2845,7 +2835,6 @@ pub struct Impl<Body: IsBody> {
     pub polarity: ImplPolarity,
     pub defaultness: Defaultness,
     pub defaultness_span: Option<Span>,
-    pub constness: Constness,
     pub generics: Generics<Body>,
     #[map({
         s.base().tcx.impl_trait_ref(s.owner_id()).sinto(s)
@@ -3031,7 +3020,7 @@ pub enum ItemKind<Body: IsBody> {
     ExternCrate(Option<Symbol>),
     Use(UsePath, UseKind),
     Static(Ty, Mutability, Body),
-    Const(Ty, Body),
+    Const(Ty, Generics<Body>, Body),
     #[custom_arm(
             rustc_hir::ItemKind::Fn(sig, generics, body) => {
                 ItemKind::Fn(generics.sinto(s), make_fn_def::<Body, _>(sig, body, s))
@@ -3229,9 +3218,6 @@ pub struct TraitRef {
 )]
 pub struct TraitPredicate {
     pub trait_ref: TraitRef,
-    #[from(constness)]
-    #[map(x.clone() == rustc_middle::ty::BoundConstness::ConstIfConst)]
-    pub is_const: bool,
     #[map(x.clone() == rustc_middle::ty::ImplPolarity::Positive)]
     #[from(polarity)]
     pub is_positive: bool,

frontend/exporter/src/types/mir.rs

@@ -529,8 +529,6 @@ pub enum TerminatorKind {
         discr: Operand,
         targets: SwitchTargets,
     },
-    Resume,
-    Terminate,
     Return,
     Unreachable,
     Drop {
@@ -581,6 +579,8 @@ pub enum TerminatorKind {
         real_target: BasicBlock,
         unwind: UnwindAction,
     },
+    UnwindResume,
+    UnwindTerminate(UnwindTerminateReason),
     InlineAsm {
         template: Vec<InlineAsmTemplatePiece>,
         operands: Vec<InlineAsmOperand>,
@@ -734,7 +734,7 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
                                 // of the the state captured by a closure.
                                 use crate::rustc_index::Idx;
                                 let generics = generics.as_closure();
-                                let upvar_tys: Vec<_> = generics.upvar_tys().collect();
+                                let upvar_tys = generics.upvar_tys();
                                 current_ty = upvar_tys[index.sinto(s).index()].clone();
                                 ProjectionElem::Field(ProjectionElemFieldKind::ClosureState(
                                     index.sinto(s),

frontend/exporter/src/types/mod.rs

@@ -1,3 +1,6 @@
+// There's a conflict between `mir::ScalarInt`and `todo::ScalarInt` but it doesn't matter.
+#![allow(ambiguous_glob_reexports)]
+
 mod copied;
 mod index;
 mod mir;

frontend/exporter/src/types/todo.rs

@@ -7,6 +7,7 @@ sinto_todo!(rustc_abi, IntegerType);
 sinto_todo!(rustc_abi, ReprFlags);
 sinto_todo!(rustc_abi, Align);
 sinto_todo!(rustc_middle::mir::interpret, ConstAllocation<'a>);
+sinto_todo!(rustc_middle::mir, UnwindTerminateReason);
 sinto_todo!(rustc_ast::tokenstream, DelimSpan);
 sinto_todo!(rustc_hir::def, DefKind);
 sinto_todo!(rustc_hir, GenericArgs<'a> as HirGenericArgs);

rust-toolchain.toml

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2023-07-15"
+channel = "nightly-2023-09-19"
 components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ]