Merge pull request #1043 from creusot-rs/bump_rustc

Bump rustc

ci/rust-toolchain

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2024-05-15"
+channel = "nightly-2024-07-25"
 components = [ "rustfmt", "rustc-dev", "llvm-tools" ]

creusot-metadata/src/decoder.rs

@@ -139,7 +139,7 @@ impl SpanDecoder for MetadataDecoder<'_, '_> {
     // sessions, to map the old `DefId` to the new one.
     fn decode_def_id(&mut self) -> DefId {
         let def_path_hash = DefPathHash::decode(self);
-        self.tcx.def_path_hash_to_def_id(def_path_hash, &"Cannot resolve crate.")
+        self.tcx.def_path_hash_to_def_id(def_path_hash).expect("Cannot resolve crate.")
     }
 
     fn decode_attr_id(&mut self) -> AttrId {
@@ -174,7 +174,7 @@ impl<'a, 'tcx> TyDecoder for MetadataDecoder<'a, 'tcx> {
     where
         F: FnOnce(&mut Self) -> R,
     {
-        let new_decoder = MemDecoder::new(self.opaque.data(), pos);
+        let new_decoder = self.opaque.split_at(pos);
         let old_decoder = std::mem::replace(&mut self.opaque, new_decoder);
         let r = f(self);
         self.opaque = old_decoder;
@@ -191,16 +191,16 @@ pub fn decode_metadata<'tcx, T: for<'a> Decodable<MetadataDecoder<'a, 'tcx>>>(
     blob: &[u8],
 ) -> T {
     let footer = {
-        let mut decoder = MemDecoder::new(blob, 0);
+        let mut decoder = MemDecoder::new(blob, 0).unwrap();
         let footer_pos = decoder
-            .with_position(blob.len() - IntEncodedWithFixedSize::ENCODED_SIZE, |d| {
+            .with_position(decoder.len() - IntEncodedWithFixedSize::ENCODED_SIZE, |d| {
                 IntEncodedWithFixedSize::decode(d).0 as usize
             });
         decoder.with_position(footer_pos, |d| Footer::decode(d))
     };
 
     let mut decoder = MetadataDecoder {
-        opaque: MemDecoder::new(blob, 0),
+        opaque: MemDecoder::new(blob, 0).unwrap(),
         tcx,
         ty_rcache: Default::default(),
         file_index_to_stable_id: footer.file_index_to_stable_id,

creusot/src/analysis/frozen_locals.rs

@@ -155,7 +155,7 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
                             panic!("could not find BorrowIndex for location {:?}", location);
                         });
 
-                    trans.gen(index);
+                    trans.gen_(index);
                 }
 
                 // Make sure there are no remaining borrows for variables

creusot/src/analysis/init_locals.rs

@@ -58,7 +58,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
         _block: BasicBlock,
         return_places: CallReturnPlaces<'_, 'tcx>,
     ) {
-        return_places.for_each(|place| trans.gen(place.local));
+        return_places.for_each(|place| trans.gen_(place.local));
     }
 
     fn domain_size(&self, body: &mir::Body<'tcx>) -> usize {
@@ -95,7 +95,7 @@ where
             PlaceContext::MutatingUse(MutatingUseContext::Deinit) => self.trans.kill(local),
 
             // Otherwise, when a place is mutated, we must consider it possibly initialized.
-            PlaceContext::MutatingUse(_) => self.trans.gen(local),
+            PlaceContext::MutatingUse(_) => self.trans.gen_(local),
 
             // If the local is moved out of, or if it gets marked `StorageDead`, consider it no
             // longer initialized.

creusot/src/analysis/liveness_no_drop.rs

@@ -98,7 +98,7 @@ where
                     self.0.kill(place.local);
                 }
             }
-            Some(DefUse::Use) => self.0.gen(place.local),
+            Some(DefUse::Use) => self.0.gen_(place.local),
             None => {}
         }
 
@@ -126,7 +126,7 @@ impl DefUse {
     fn apply(trans: &mut impl GenKill<Local>, place: Place<'_>, context: PlaceContext) {
         match DefUse::for_place(place, context) {
             Some(DefUse::Def) => trans.kill(place.local),
-            Some(DefUse::Use) => trans.gen(place.local),
+            Some(DefUse::Use) => trans.gen_(place.local),
             None => {}
         }
     }

creusot/src/analysis/not_final_places.rs

@@ -123,7 +123,7 @@ impl<'tcx> NotFinalPlaces<'tcx> {
     /// # Returns
     /// - If the reborrow is final, return the position of the dereference of the
     /// original borrow in `place.projection`.
-    ///   
+    ///
     ///   For example, if the reborrow `&mut (*x.0)` is final, then the projections are
     /// `[Field(0), Deref]`, and so we return `Some(1)`.
     ///
@@ -533,16 +533,16 @@ where
             // let r2 = &mut *bor; // r1 is not final !
             // ```
             | PlaceContext::MutatingUse(MutatingUseContext::Borrow) => {
-                self.trans.gen(self.mapping.places[&place.as_ref()])
+                self.trans.gen_(self.mapping.places[&place.as_ref()])
             }
             PlaceContext::MutatingUse(MutatingUseContext::Store)
             | PlaceContext::MutatingUse(MutatingUseContext::Call)
             | PlaceContext::MutatingUse(MutatingUseContext::SetDiscriminant)
             | PlaceContext::MutatingUse(MutatingUseContext::AsmOutput) => {
                 let id = self.mapping.places[&place.as_ref()];
                 if self.mapping.has_dereference.contains(id) {
-                    // We are writing under a dereference, so this changes the prophecy of the underlying borrow. 
-                    self.trans.gen(id);
+                    // We are writing under a dereference, so this changes the prophecy of the underlying borrow.
+                    self.trans.gen_(id);
                 }
             }
             _ => {}

creusot/src/analysis/uninit_locals.rs

@@ -94,7 +94,7 @@ where
             // If the local is moved out of, or if it gets marked `StorageDead`, consider it no
             // longer initialized.
             PlaceContext::NonUse(NonUseContext::StorageDead) => {}
-            PlaceContext::NonMutatingUse(NonMutatingUseContext::Move) => self.trans.gen(local),
+            PlaceContext::NonMutatingUse(NonMutatingUseContext::Move) => self.trans.gen_(local),
 
             // All other uses do not affect this analysis.
             PlaceContext::NonUse(

creusot/src/backend/clone_map/elaborator.rs

@@ -199,14 +199,11 @@ impl<'tcx> SymbolElaborator<'tcx> {
             }
         } else if util::item_type(ctx.tcx, def_id) == ItemType::Constant {
             let uneval = ty::UnevaluatedConst::new(def_id, subst);
-            let constant = Const::new(
-                ctx.tcx,
-                ty::ConstKind::Unevaluated(uneval),
-                ctx.type_of(def_id).instantiate_identity(),
-            );
+            let constant = Const::new(ctx.tcx, ty::ConstKind::Unevaluated(uneval));
+            let ty = ctx.type_of(def_id).instantiate_identity();
 
             let span = ctx.def_span(def_id);
-            let res = crate::constant::from_ty_const(&mut ctx.ctx, constant, param_env, span);
+            let res = crate::constant::from_ty_const(&mut ctx.ctx, constant, ty, param_env, span);
 
             let res = lower_pure(ctx, names, &res);
             vec![Decl::ConstantDecl(Constant {

creusot/src/backend/constant.rs

@@ -17,15 +17,12 @@ impl<'tcx> Why3Generator<'tcx> {
     ) -> (TranslatedItem, CloneSummary<'tcx>) {
         let subst = GenericArgs::identity_for_item(self.tcx, def_id);
         let uneval = ty::UnevaluatedConst::new(def_id, subst);
-        let constant = Const::new(
-            self.tcx,
-            ty::ConstKind::Unevaluated(uneval),
-            self.type_of(def_id).instantiate_identity(),
-        );
+        let constant = Const::new(self.tcx, ty::ConstKind::Unevaluated(uneval));
+        let ty = self.tcx.type_of(def_id).instantiate(self.tcx, subst);
 
         let param_env = self.param_env(def_id);
         let span = self.def_span(def_id);
-        let res = from_ty_const(&mut self.ctx, constant, param_env, span);
+        let res = from_ty_const(&mut self.ctx, constant, ty, param_env, span);
         let mut names = Dependencies::new(self.tcx, [def_id]);
         let _ = lower_pure(self, &mut names, &res);
 

creusot/src/backend/program.rs

@@ -22,7 +22,7 @@ use crate::{
 };
 
 use petgraph::graphmap::DiGraphMap;
-use rustc_hir::{def_id::DefId, Unsafety};
+use rustc_hir::{def_id::DefId, Safety};
 use rustc_middle::{
     mir::{self, BasicBlock, BinOp, ProjectionElem, UnOp, START_BLOCK},
     ty::{AdtDef, GenericArgsRef, Ty, TyKind},
@@ -621,7 +621,7 @@ impl<'tcx> RValue<'tcx> {
                 Exp::var("_res")
             }
             RValue::Ghost(t) => lower_pure(lower.ctx, lower.names, &t),
-            RValue::Borrow(_, _) => todo!(),
+            RValue::Borrow(_, _) | RValue::UnaryOp(UnOp::PtrMetadata, _) => todo!(),
         };
 
         e
@@ -1170,7 +1170,7 @@ fn func_call_to_why3<'tcx>(
     let args: Vec<_> = if lower.ctx.is_closure_like(id) {
         assert!(args.len() == 2, "closures should only have two arguments (env, args)");
 
-        let real_sig = lower.ctx.signature_unclosure(subst.as_closure().sig(), Unsafety::Normal);
+        let real_sig = lower.ctx.signature_unclosure(subst.as_closure().sig(), Safety::Safe);
 
         let Operand::Move(pl) = args.remove(1) else { panic!() };
         let mut args = vec![coma::Arg::Term(args.remove(0).to_why(lower, istmts))];
@@ -1202,30 +1202,31 @@ pub(crate) fn binop_to_binop<'tcx, N: Namer<'tcx>>(names: &mut N, ty: Ty, op: mi
     names.import_prelude_module(prelude);
     let mut module = prelude.qname();
 
+    use BinOp::*;
     match op {
-        BinOp::Add => module.push_ident("add"),
-        BinOp::AddUnchecked => module.push_ident("add"),
-        BinOp::Sub => module.push_ident("sub"),
-        BinOp::SubUnchecked => module.push_ident("sub"),
-        BinOp::Mul => module.push_ident("mul"),
-        BinOp::MulUnchecked => module.push_ident("mul"),
-        BinOp::Div => module.push_ident("div"),
-        BinOp::Rem => module.push_ident("rem"),
-        BinOp::BitXor => module.push_ident("bw_xor"),
-        BinOp::BitAnd => module.push_ident("bw_and"),
-        BinOp::BitOr => module.push_ident("bw_or"),
-        BinOp::Shl => module.push_ident("shl"),
-        BinOp::ShlUnchecked => module.push_ident("shl"),
-        BinOp::Shr => module.push_ident("shr"),
-        BinOp::ShrUnchecked => module.push_ident("shr"),
-        BinOp::Eq => module.push_ident("eq"),
-        BinOp::Lt => module.push_ident("lt"),
-        BinOp::Le => module.push_ident("le"),
-        BinOp::Ne => module.push_ident("ne"),
-        BinOp::Ge => module.push_ident("ge"),
-        BinOp::Gt => module.push_ident("gt"),
-        BinOp::Cmp => todo!(),
-        BinOp::Offset => unimplemented!("pointer offsets are unsupported"),
+        Add => module.push_ident("add"),
+        AddUnchecked => module.push_ident("add"),
+        Sub => module.push_ident("sub"),
+        SubUnchecked => module.push_ident("sub"),
+        Mul => module.push_ident("mul"),
+        MulUnchecked => module.push_ident("mul"),
+        Div => module.push_ident("div"),
+        Rem => module.push_ident("rem"),
+        BitXor => module.push_ident("bw_xor"),
+        BitAnd => module.push_ident("bw_and"),
+        BitOr => module.push_ident("bw_or"),
+        Shl => module.push_ident("shl"),
+        ShlUnchecked => module.push_ident("shl"),
+        Shr => module.push_ident("shr"),
+        ShrUnchecked => module.push_ident("shr"),
+        Eq => module.push_ident("eq"),
+        Lt => module.push_ident("lt"),
+        Le => module.push_ident("le"),
+        Ne => module.push_ident("ne"),
+        Ge => module.push_ident("ge"),
+        Gt => module.push_ident("gt"),
+        Cmp | AddWithOverflow | SubWithOverflow | MulWithOverflow => todo!(),
+        Offset => unimplemented!("pointer offsets are unsupported"),
     };
 
     module = module.without_search_path();

creusot/src/lints/experimental_types.rs

@@ -40,21 +40,15 @@ impl<'tcx> LateLintPass<'tcx> for Experimental {
         }
 
         if is_str_ty(cx, e) {
-            cx.opt_span_lint(
-                EXPERIMENTAL,
-                Some(e.span),
-                "support for string types is limited and experimental",
-                |_lint| (),
-            );
+            cx.opt_span_lint(EXPERIMENTAL, Some(e.span), |lint| {
+                lint.primary_message("support for string types is limited and experimental");
+            });
         }
 
         if is_dyn_ty(cx, e) {
-            cx.opt_span_lint(
-                EXPERIMENTAL,
-                Some(e.span),
-                "support for trait objects (dyn) is limited and experimental",
-                |_lint| (),
-            );
+            cx.opt_span_lint(EXPERIMENTAL, Some(e.span), |lint| {
+                lint.primary_message("support for trait objects (dyn) is limited and experimental");
+            });
         }
     }
 }

creusot/src/lints/resolve_trait.rs

@@ -24,8 +24,9 @@ impl<'tcx> LateLintPass<'tcx> for ResolveTrait {
             cx.opt_span_lint(
                 RESOLVE_TRAIT,
                 Some(DUMMY_SP),
-                "the `creusot_contracts` crate is not loaded. You will not be able to verify any code using Creusot until you do so.",
-                |_lint| (),
+                |lint| {
+                    lint.primary_message("the `creusot_contracts` crate is not loaded. You will not be able to verify any code using Creusot until you do so.");
+                },
             );
         }
     }

creusot/src/translation/constant.rs

@@ -28,8 +28,8 @@ fn from_mir_constant_kind<'tcx>(
     env: ParamEnv<'tcx>,
     span: Span,
 ) -> fmir::Operand<'tcx> {
-    if let mir::Const::Ty(c) = ck {
-        return Operand::Constant(from_ty_const(ctx, c, env, span));
+    if let mir::Const::Ty(ty, c) = ck {
+        return Operand::Constant(from_ty_const(ctx, c, ty, env, span));
     }
 
     if ck.ty().is_unit() {
@@ -74,6 +74,7 @@ fn from_mir_constant_kind<'tcx>(
 pub(crate) fn from_ty_const<'tcx>(
     ctx: &mut TranslationCtx<'tcx>,
     c: Const<'tcx>,
+    ty: Ty<'tcx>,
     env: ParamEnv<'tcx>,
     span: Span,
 ) -> Term<'tcx> {
@@ -82,14 +83,14 @@ pub(crate) fn from_ty_const<'tcx>(
     if let ConstKind::Unevaluated(u) = c.kind()
         && let Some(_) = get_builtin(ctx.tcx, u.def)
     {
-        return Term { kind: TermKind::Lit(Literal::Function(u.def, u.args)), ty: c.ty(), span };
+        return Term { kind: TermKind::Lit(Literal::Function(u.def, u.args)), ty, span };
     };
 
     if let ConstKind::Param(_) = c.kind() {
         ctx.crash_and_error(span, "const generic parameters are not yet supported");
     }
 
-    return Term { kind: TermKind::Lit(try_to_bits(ctx, env, c.ty(), span, c)), ty: c.ty(), span };
+    return Term { kind: TermKind::Lit(try_to_bits(ctx, env, ty, span, c)), ty: ty, span };
 }
 
 fn try_to_bits<'tcx, C: ToBits<'tcx> + std::fmt::Debug>(

creusot/src/translation/function/statement.rs

@@ -14,9 +14,10 @@ use rustc_middle::{
         BinOp, BorrowKind::*, CastKind, Location, Operand::*, Place, Rvalue, SourceInfo, Statement,
         StatementKind,
     },
-    ty::adjustment::PointerCoercion,
+    ty::{adjustment::PointerCoercion, Ty},
 };
 use rustc_mir_dataflow::ResultsCursor;
+use rustc_type_ir::inherent::Ty as _;
 
 impl<'tcx> BodyTranslator<'_, 'tcx> {
     pub(crate) fn translate_statement(
@@ -110,7 +111,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
             Rvalue::BinaryOp(BinOp::BitAnd, box (l, _)) if !l.ty(self.body, self.tcx).is_bool() => {
                 self.ctx.crash_and_error(si.span, "bitwise operations are currently unsupported")
             }
-            Rvalue::BinaryOp(op, box (l, r)) | Rvalue::CheckedBinaryOp(op, box (l, r)) => {
+            Rvalue::BinaryOp(op, box (l, r)) => {
                 RValue::BinOp(*op, self.translate_operand(l), self.translate_operand(r))
             }
             Rvalue::UnaryOp(op, v) => RValue::UnaryOp(*op, self.translate_operand(v)),
@@ -169,6 +170,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                 Operand::Constant(crate::constant::from_ty_const(
                     self.ctx,
                     *len,
+                    self.ctx.tcx.types.usize,
                     self.param_env(),
                     si.span,
                 )),

creusot/src/translation/function/terminator.rs

@@ -13,7 +13,7 @@ use itertools::Itertools;
 use rustc_hir::def_id::DefId;
 use rustc_infer::{
     infer::{InferCtxt, TyCtxtInferExt},
-    traits::{FulfillmentError, Obligation, ObligationCause, TraitEngine},
+    traits::{Obligation, ObligationCause, TraitEngine},
 };
 use rustc_middle::{
     mir::{
@@ -23,7 +23,10 @@ use rustc_middle::{
     ty::{self, GenericArgKind, GenericArgsRef, ParamEnv, Predicate, Ty, TyKind},
 };
 use rustc_span::{Span, Symbol};
-use rustc_trait_selection::traits::{error_reporting::TypeErrCtxtExt, TraitEngineExt};
+use rustc_trait_selection::{
+    error_reporting::InferCtxtErrorExt,
+    traits::{FulfillmentError, TraitEngineExt},
+};
 use std::collections::HashMap;
 
 // Translate the terminator of a basic block.
@@ -167,7 +170,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
             FalseUnwind { real_target, .. } => {
                 self.emit_terminator(mk_goto(*real_target));
             }
-            CoroutineDrop | UnwindResume | Yield { .. } | InlineAsm { .. } => {
+            CoroutineDrop | UnwindResume | Yield { .. } | InlineAsm { .. } | TailCall { .. } => {
                 unreachable!("{:?}", terminator.kind)
             }
         }
@@ -237,15 +240,14 @@ pub(crate) fn evaluate_additional_predicates<'tcx>(
     param_env: ParamEnv<'tcx>,
     sp: Span,
 ) -> Result<(), Vec<FulfillmentError<'tcx>>> {
-    let mut fulfill_cx = <dyn TraitEngine<'tcx>>::new(infcx);
+    let mut fulfill_cx = <dyn TraitEngine<'tcx, _>>::new(infcx);
     for predicate in p {
         let predicate = infcx.tcx.erase_regions(predicate);
         let cause = ObligationCause::dummy_with_span(sp);
         let obligation = Obligation { cause, param_env, recursion_depth: 0, predicate };
         // holds &= infcx.predicate_may_hold(&obligation);
         fulfill_cx.register_predicate_obligation(&infcx, obligation);
     }
-    use rustc_infer::traits::TraitEngineExt;
     let errors = fulfill_cx.select_all_or_error(&infcx);
     if !errors.is_empty() {
         return Err(errors);