Bump hax & rustc

charon/src/ast/names_utils.rs

@@ -197,16 +197,15 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
                     // Translate to hax types
                     let s1 = &hax::State::new_from_state_and_id(&self.hax_state, id);
                     let substs =
-                        rustc_middle::ty::subst::InternalSubsts::identity_for_item(tcx, id)
-                            .sinto(s1);
+                        rustc_middle::ty::GenericArgs::identity_for_item(tcx, id).sinto(s1);
                     // TODO: use the bounds
                     let _bounds: Vec<hax::Clause> = tcx
                         .predicates_of(id)
                         .predicates
                         .iter()
                         .map(|(x, _)| x.sinto(s1))
                         .collect();
-                    let ty = tcx.type_of(id).subst_identity().sinto(s1);
+                    let ty = tcx.type_of(id).instantiate_identity().sinto(s1);
 
                     // Translate from hax to LLBC
                     let mut bt_ctx = BodyTransCtx::new(id, self);

charon/src/export.rs

@@ -91,7 +91,7 @@ impl<FD: Serialize + Clone, GD: Serialize + Clone> GCrateData<FD, GD> {
         // Create the file.
         let std::io::Result::Ok(outfile) = File::create(target_filename.clone()) else {
             error!("Could not open: {:?}", target_filename);
-            return Err(())
+            return Err(());
         };
         // Write to the file.
         let std::result::Result::Ok(()) = serde_json::to_writer(&outfile, self) else {

charon/src/transform/remove_dynamic_checks.rs

@@ -16,7 +16,10 @@ fn remove_dynamic_checks(ctx: &mut TransformCtx, block: &mut BlockData) {
         cond: Operand::Move(cond),
         expected,
         target,
-    } = &block.terminator.content else { return };
+    } = &block.terminator.content
+    else {
+        return;
+    };
 
     // We return the statements we want to keep, which must be a prefix of `block.statements`.
     let statements_to_keep = match block.statements.as_mut_slice() {

charon/src/transform/remove_read_discriminant.rs

@@ -66,7 +66,7 @@ impl<'a, 'ctx> Visitor<'a, 'ctx> {
                         content: RawStatement::Nop,
                         meta: st.meta,
                     };
-                    return
+                    return;
                 };
 
                 // We look for a `SwitchInt` just after the discriminant read.
@@ -87,8 +87,11 @@ impl<'a, 'ctx> Visitor<'a, 'ctx> {
 
                 match maybe_switch {
                     Ok((meta2, switch, st3_opt)) => {
-                        let Switch::SwitchInt(Operand::Move(op_p), _int_ty, targets, otherwise) = switch
-                        else { unreachable!() };
+                        let Switch::SwitchInt(Operand::Move(op_p), _int_ty, targets, otherwise) =
+                            switch
+                        else {
+                            unreachable!()
+                        };
                         assert!(op_p.projection.is_empty() && op_p.var_id == dest.var_id);
 
                         // Convert between discriminants and variant indices. Remark: the discriminant can

charon/src/translate/translate_constants.rs

@@ -157,7 +157,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     trait_refs,
                     trait_info,
                 )?;
-                let SubstFunIdOrPanic::Fun(fn_id) = fn_id else  { unreachable!() };
+                let SubstFunIdOrPanic::Fun(fn_id) = fn_id else {
+                    unreachable!()
+                };
                 RawConstantExpr::FnPtr(fn_id.func)
             }
             ConstantExprKind::Todo(msg) => {

charon/src/translate/translate_ctx.rs

@@ -607,7 +607,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
             | ForeignMod
             | Generator
             | GlobalAsm
-            | ImplTraitPlaceholder
             | InlineConst
             | LifetimeParam
             | OpaqueTy

charon/src/translate/translate_functions_to_ullbc.rs

@@ -603,7 +603,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         ))
                     }
                     (
-                        hax::CastKind::Pointer(hax::PointerCast::Unsize),
+                        hax::CastKind::PointerCoercion(hax::PointerCoercion::Unsize),
                         Ty::Ref(_, t1, kind1),
                         Ty::Ref(_, t2, kind2),
                     ) => {
@@ -643,7 +643,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         }
                     }
                     (
-                        hax::CastKind::Pointer(hax::PointerCast::ClosureFnPointer(unsafety)),
+                        hax::CastKind::PointerCoercion(hax::PointerCoercion::ClosureFnPointer(
+                            unsafety,
+                        )),
                         src_ty @ Ty::Arrow(..),
                         tgt_ty @ Ty::Arrow(..),
                     ) => {
@@ -656,7 +658,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         ))
                     }
                     (
-                        hax::CastKind::Pointer(hax::PointerCast::ReifyFnPointer),
+                        hax::CastKind::PointerCoercion(hax::PointerCoercion::ReifyFnPointer),
                         src_ty @ Ty::Arrow(..),
                         tgt_ty @ Ty::Arrow(..),
                     ) => {
@@ -1207,7 +1209,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             },
             TerminatorKind::Call {
                 fun,
-                substs,
+                generics,
                 args,
                 destination,
                 target,
@@ -1219,7 +1221,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             } => self.translate_function_call(
                 span,
                 fun,
-                substs,
+                generics,
                 args,
                 destination,
                 target,
@@ -1326,7 +1328,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         &mut self,
         span: rustc_span::Span,
         fun: &hax::FunOperand,
-        substs: &Vec<hax::GenericArg>,
+        generics: &Vec<hax::GenericArg>,
         args: &Vec<hax::Operand>,
         destination: &hax::Place,
         target: &Option<hax::BasicBlock>,
@@ -1352,7 +1354,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     span,
                     erase_regions,
                     def_id,
-                    substs,
+                    generics,
                     Some(args),
                     trait_refs,
                     trait_info,
@@ -1369,7 +1371,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     }
                     SubstFunIdOrPanic::Fun(fid) => {
                         let next_block = target.unwrap_or_else(|| {
-                            panic!("Expected a next block after the call to {:?}.\n\nSubsts: {:?}\n\nArgs: {:?}:", rust_id, substs, args)
+                            panic!("Expected a next block after the call to {:?}.\n\nSubsts: {:?}\n\nArgs: {:?}:", rust_id, generics, args)
                         });
 
                         // Translate the target
@@ -1396,7 +1398,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
                 // Translate the target
                 let next_block = target.unwrap_or_else(|| {
-                    panic!("Expected a next block after the call to {:?}.\n\nSubsts: {:?}\n\nArgs: {:?}:", p, substs, args)
+                    panic!("Expected a next block after the call to {:?}.\n\nSubsts: {:?}\n\nArgs: {:?}:", p, generics, args)
                 });
                 let lval = self.translate_place(span, destination)?;
                 let next_block = self.translate_basic_block_id(next_block);
@@ -1487,7 +1489,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
         // Retrive the body
         let Some(body) = get_mir_for_def_id_and_level(tcx, rust_id, self.t_ctx.options.mir_level)
-        else { return Ok(None) };
+        else {
+            return Ok(None);
+        };
 
         // Here, we have to create a MIR state, which contains the body
         let state = hax::state::State::new_from_mir(
@@ -1561,7 +1565,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         ) = if is_closure {
             // Closures have a peculiar handling in Rust: we can't call
             // `TyCtxt::fn_sig`.
-            let fun_type = tcx.type_of(def_id).subst_identity();
+            let fun_type = tcx.type_of(def_id).instantiate_identity();
             let rsubsts = match fun_type.kind() {
                 ty::TyKind::Closure(_def_id, substs_ref) => substs_ref,
                 _ => {
@@ -1575,7 +1579,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             // Importantly, the type parameters necessarily come from the parents:
             // the closure can't itself be polymorphic, and the signature of
             // the closure only quantifies lifetimes.
-            let substs = closure.parent_substs();
+            let substs = closure.parent_args();
             trace!("closure.parent_substs: {:?}", substs);
             let sig = closure.sig();
             trace!("closure.sig: {:?}", sig);
@@ -1617,10 +1621,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             // There is an early binder for the early-bound regions, that
             // we ignore, and a binder for the late-bound regions, that we
             // keep.
-            let fn_sig = fn_sig.subst_identity();
+            let fn_sig = fn_sig.instantiate_identity();
 
             // Retrieve the early-bound parameters
-            let fun_type = tcx.type_of(def_id).subst_identity();
+            let fun_type = tcx.type_of(def_id).instantiate_identity();
             let substs: Vec<hax::GenericArg> = match fun_type.kind() {
                 ty::TyKind::FnDef(_def_id, substs_ref) => substs_ref.sinto(&self.hax_state),
                 ty::TyKind::Closure(_, _) => {
@@ -1904,7 +1908,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
         let name = bt_ctx.t_ctx.def_id_to_name(rust_id)?;
 
         trace!("Translating global type");
-        let mir_ty = bt_ctx.t_ctx.tcx.type_of(rust_id).subst_identity();
+        let mir_ty = bt_ctx.t_ctx.tcx.type_of(rust_id).instantiate_identity();
         let erase_regions = false; // This doesn't matter: there shouldn't be any regions
         let ty = bt_ctx.translate_ty(span, erase_regions, &mir_ty.sinto(hax_state))?;
 

charon/src/translate/translate_predicates.rs

@@ -516,9 +516,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         // directly? For now we just ignore it.
                         Ok(None)
                     }
-                    ClauseKind::WellFormed(_)
-                    | ClauseKind::ConstEvaluatable(_)
-                    | ClauseKind::TypeWellFormedFromEnv(_) => {
+                    ClauseKind::WellFormed(_) | ClauseKind::ConstEvaluatable(_) => {
                         error_or_panic!(self, span, format!("Unsupported clause: {:?}", kind))
                     }
                 }

charon/src/translate/translate_traits.rs

@@ -21,7 +21,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             tcx.def_span(item.def_id),
             erase_regions,
             &tcx.type_of(item.def_id)
-                .subst_identity()
+                .instantiate_identity()
                 .sinto(&self.hax_state),
         )
     }
@@ -46,7 +46,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         let span = tcx.def_span(trait_impl_def_id);
 
         // Lookup the trait clauses and substitute - TODO: not sure about the substitution
-        let subst = rust_impl_trait_ref.substs;
+        let subst = rust_impl_trait_ref.args;
         let bounds = tcx.item_bounds(decl_item.def_id);
         let param_env = tcx.param_env(trait_impl_def_id);
         let bounds = tcx.subst_and_normalize_erasing_regions(subst, param_env, bounds);
@@ -156,7 +156,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         // Retrieve the trait ref representing "self"
         let tcx = self.t_ctx.tcx;
         let rustc_middle::ty::ImplSubject::Trait(trait_ref) =
-            tcx.impl_subject(def_id).subst_identity() else { unreachable!() };
+            tcx.impl_subject(def_id).instantiate_identity()
+        else {
+            unreachable!()
+        };
 
         // Wrap it in a [TraitPredicate] so that when calling [sinto] we retrieve
         // the parent and item predicates.
@@ -335,7 +338,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
                     // Translating the predicates
                     {
                         // TODO: this is an ugly manip
-                        let bounds = tcx.item_bounds(item.def_id).subst_identity();
+                        let bounds = tcx.item_bounds(item.def_id).instantiate_identity();
                         use crate::rustc_middle::query::Key;
                         let span = bounds.default_span(tcx);
                         let bounds: Vec<_> = bounds
@@ -499,7 +502,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
             let trait_id = trait_id.unwrap();
 
             let rustc_middle::ty::ImplSubject::Trait(rust_trait_ref) =
-                    tcx.impl_subject(rust_id).subst_identity() else { unreachable!() };
+                tcx.impl_subject(rust_id).instantiate_identity()
+            else {
+                unreachable!()
+            };
             let trait_ref = rust_trait_ref.sinto(&bt_ctx.hax_state);
             let (regions, types, const_generics) =
                 bt_ctx.translate_substs(span, erase_regions, None, &trait_ref.generic_args)?;
@@ -508,7 +514,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
                 &bt_ctx.hax_state,
                 tcx.param_env(rust_id),
                 rust_trait_ref.def_id,
-                rust_trait_ref.substs,
+                rust_trait_ref.args,
                 None,
             );
             let parent_trait_refs: Vec<TraitRef> =

charon/src/translate/translate_types.rs

@@ -655,8 +655,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         // We could use: TyCtxt::generics_of(DefId)
         // But using the identity substitution is simpler. For instance, we can
         // easily retrieve the type for the const parameters.
-        let substs = rustc_middle::ty::subst::InternalSubsts::identity_for_item(tcx, def_id)
-            .sinto(&self.hax_state);
+        let substs =
+            rustc_middle::ty::GenericArgs::identity_for_item(tcx, def_id).sinto(&self.hax_state);
 
         self.translate_generic_params_from_hax(span, &substs)
     }

charon/tests/ui.rs

@@ -68,7 +68,9 @@ fn parse_magic_comments(input_path: &std::path::Path) -> anyhow::Result<MagicCom
         auxiliary_crates: Vec::new(),
     };
     for line in read_to_string(input_path)?.lines() {
-        let Some(line) = line.strip_prefix("//@") else { break };
+        let Some(line) = line.strip_prefix("//@") else {
+            break;
+        };
         let line = line.trim();
         if line == "known-panic" {
             comments.test_kind = TestKind::KnownPanic;

charon/tests/ui/issue-120-bare-discriminant-read.out

@@ -9,20 +9,17 @@ fn test_crate::call_is_some<T>(@1: core::option::Option<T>) -> bool
 {
     let @0: bool; // return
     let opt@1: core::option::Option<T>; // arg #1
-    let self@2: &'_ (core::option::Option<T>); // local
-    let @3: isize; // anonymous local
+    let @2: isize; // anonymous local
 
-    self@2 := &opt@1
-    match *(self@2) {
+    match opt@1 {
         0 => {
-            @3 := const (0 : isize)
+            @2 := const (0 : isize)
         },
         1 => {
-            @3 := const (1 : isize)
+            @2 := const (1 : isize)
         }
     }
-    @0 := copy (@3) == const (1 : isize)
-    drop self@2
+    @0 := copy (@2) == const (1 : isize)
     drop opt@1
     return
 }

charon/tests/ui/unsupported/issue-167-self-constructors.out

@@ -1,19 +1,9 @@
-[ ERROR charon_lib::ast::names_utils:274] [names_utils::<impl charon_lib::translate::translate_ctx::TranslateCtx>::def_id_to_name]:
-Unexpected DefPathData: DisambiguatedDefPathData { data: Ctor, disambiguator: 0 }
-thread 'rustc' panicked at 'internal error: entered unreachable code: Unexpected DefPathData: DisambiguatedDefPathData { data: Ctor, disambiguator: 0 }', src/ast/names_utils.rs:275:21
-note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
-error: Thread panicked when extracting body.
- --> tests/ui/unsupported/issue-167-self-constructors.rs:8:5
-  |
-8 |     pub fn b() -> Self {
-  |     ^^^^^^^^^^^^^^^^^^
-
 error: assertion failure: "user_annotation.is_none()"
   --> tests/ui/unsupported/issue-167-self-constructors.rs:19:9
    |
 19 |         Self { r }
    |         ^^^^^^^^^^
 
-error: aborting due to 2 previous errors
+error: aborting due to previous error
 
-[ ERROR charon_driver:200] The extraction encountered 2 errors
+[ ERROR charon_driver:200] The extraction encountered 1 errors

flake.nix

@@ -90,7 +90,7 @@
                 > $out
             '';
             # The rustc commit we use to get the tests. This should stay equal to `toolchain_commit`.
-            tests_commit = "5ea66686467d3ec5f8c81570e7f0f16ad8dd8cc3";
+            tests_commit = "ad963232d9b987d66a6f8e6ec4141f672b8b9900";
             rustc_tests = pkgs.runCommand "rustc-tests"
               {
                 src = pkgs.fetchFromGitHub {

rust-toolchain

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2023-06-28"
+channel = "nightly-2023-07-15"
 components = [ "rustc-dev", "llvm-tools-preview" ]