Merge pull request #1001 from creusot-rs/update-nightly

Update rustc nightly

ci/rust-toolchain

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

creusot-contracts-proc/src/extern_spec.rs

@@ -30,6 +30,7 @@ pub struct ExternMod {
     ident: Ident,
     content: Vec<ExternSpec>,
 }
+#[allow(dead_code)]
 pub struct ExternTrait {
     pub unsafety: Option<Unsafe>,
     pub trait_token: Trait,
@@ -41,6 +42,7 @@ pub struct ExternTrait {
     pub items: Vec<ExternMethod>,
 }
 
+#[allow(dead_code)]
 pub struct ExternImpl {
     pub attrs: Vec<Attribute>,
     pub defaultness: Option<token::Default>,
@@ -52,6 +54,8 @@ pub struct ExternImpl {
     pub brace_token: Brace,
     pub items: Vec<ExternMethod>,
 }
+
+#[allow(dead_code)]
 pub struct ExternMethod {
     pub attrs: Vec<Attribute>,
     pub sig: Signature,

creusot-contracts-proc/src/lib.rs

@@ -23,7 +23,6 @@ trait FilterAttrs<'a> {
     type Ret: Iterator<Item = &'a Attribute>;
 
     fn outer(self) -> Self::Ret;
-    fn inner(self) -> Self::Ret;
 }
 
 impl<'a> FilterAttrs<'a> for &'a [Attribute] {
@@ -38,16 +37,6 @@ impl<'a> FilterAttrs<'a> for &'a [Attribute] {
         }
         self.iter().filter(is_outer)
     }
-
-    fn inner(self) -> Self::Ret {
-        fn is_inner(attr: &&Attribute) -> bool {
-            match attr.style {
-                AttrStyle::Inner(_) => true,
-                AttrStyle::Outer => false,
-            }
-        }
-        self.iter().filter(is_inner)
-    }
 }
 
 fn generate_unique_ident(prefix: &str) -> Ident {

creusot-contracts/build.rs

@@ -0,0 +1,3 @@
+fn main() {
+    println!("cargo::rustc-check-cfg=cfg(creusot)");
+}

creusot-metadata/src/decoder.rs

@@ -38,7 +38,7 @@ impl<'a, 'tcx> MetadataDecoder<'a, 'tcx> {
                 let source_file_cnum =
                     self.tcx.stable_crate_id_to_crate_num(source_file_id.stable_crate_id);
 
-                self.tcx.cstore_untracked().import_source_files(self.tcx.sess, source_file_cnum);
+                self.tcx.import_source_files(source_file_cnum);
                 self.tcx
                     .sess
                     .source_map()
@@ -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, &mut || panic!("Cannot resolve crate."))
+        self.tcx.def_path_hash_to_def_id(def_path_hash, &"Cannot resolve crate.")
     }
 
     fn decode_attr_id(&mut self) -> AttrId {

creusot-metadata/src/encoder.rs

@@ -192,17 +192,11 @@ pub fn encode_metadata<'tcx, T: for<'a> Encodable<MetadataEncoder<'a, 'tcx>>>(
                 use rustc_span::FileName;
                 match file.name {
                     FileName::Real(ref original_file_name) => {
-                        let adapted_file_name = if tcx.sess.should_prefer_remapped_for_codegen() {
+                        let adapted_file_name =
                             source_map.path_mapping().to_embeddable_absolute_path(
                                 original_file_name.clone(),
                                 working_directory,
-                            )
-                        } else {
-                            source_map.path_mapping().to_local_embeddable_absolute_path(
-                                original_file_name.clone(),
-                                working_directory,
-                            )
-                        };
+                            );
 
                         adapted_source_file.name = FileName::Real(adapted_file_name);
                     }

creusot-rustc/src/main.rs

@@ -13,55 +13,26 @@ extern crate log;
 
 use creusot::callbacks::*;
 use options::CreusotArgs;
-use rustc_driver::{RunCompiler, DEFAULT_LOCALE_RESOURCES};
-use rustc_errors::emitter::HumanEmitter;
-use rustc_interface::interface::try_print_query_stack;
+use rustc_driver::RunCompiler;
 use rustc_session::{config::ErrorOutputType, EarlyDiagCtxt};
-use std::{env, panic, panic::PanicInfo, process::Command};
+use std::{env, panic, process::Command};
 
 const BUG_REPORT_URL: &'static str = &"https://github.com/creusot-rs/creusot/issues/new";
 
-lazy_static::lazy_static! {
-    static ref ICE_HOOK: Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static> = {
-        let hook = panic::take_hook();
-        panic::set_hook(Box::new(|info| report_panic(info)));
-        hook
-    };
-}
-
-fn report_panic(info: &PanicInfo) {
-    (*ICE_HOOK)(info);
-
-    // Separate the output with an empty line
-    eprintln!();
-    let fallback_bundle =
-        rustc_errors::fallback_fluent_bundle(DEFAULT_LOCALE_RESOURCES.to_vec(), false);
-
-    let emitter = Box::new(HumanEmitter::stderr(rustc_errors::ColorConfig::Auto, fallback_bundle));
-    let handler = rustc_errors::DiagCtxt::with_emitter(emitter);
-
-    let mut diagnostic = handler.struct_note("Creusot has panic-ed!");
-    diagnostic.note("Oops, that shouldn't have happened, sorry about that.");
-    diagnostic.note(format!("Please report this bug over here: {}", BUG_REPORT_URL));
-
-    diagnostic.emit();
-
-    // If backtraces are enabled, also print the query stack
-    let backtrace = env::var_os("RUST_BACKTRACE").map_or(false, |x| &x != "0");
-
-    if backtrace {
-        try_print_query_stack(&handler, None, None);
-    }
-}
-
 struct DefaultCallbacks;
 impl rustc_driver::Callbacks for DefaultCallbacks {}
 
 fn main() {
     let handler = EarlyDiagCtxt::new(ErrorOutputType::default());
+
+    // Rust verification tools crash too much for the ice hook to report `full` by default
+    if std::env::var_os("RUST_BACKTRACE").is_none() {
+        std::env::set_var("RUST_BACKTRACE", "0");
+    }
+    rustc_driver::install_ice_hook(BUG_REPORT_URL, |_| ());
+
     rustc_driver::init_rustc_env_logger(&handler);
     env_logger::init();
-    lazy_static::initialize(&ICE_HOOK);
 
     setup_plugin();
 }
@@ -136,12 +107,3 @@ fn sysroot_path() -> String {
 
     String::from_utf8(output.stdout).unwrap().trim().to_owned()
 }
-
-fn _emit_warning(text: String) {
-    let fallback_bundle =
-        rustc_errors::fallback_fluent_bundle(DEFAULT_LOCALE_RESOURCES.to_vec(), false);
-
-    let emitter = Box::new(HumanEmitter::stderr(rustc_errors::ColorConfig::Auto, fallback_bundle));
-    let handler = rustc_errors::DiagCtxt::with_emitter(emitter);
-    handler.warn(text);
-}

creusot/Cargo.toml

@@ -9,7 +9,9 @@ itertools = "*"
 log = "0.4"
 serde = { version = "1.0", features = ["derive"] }
 heck = "0.4"
-petgraph = "0.6"
+# Necessary as this introduces a version of `GraphMap` with no `Ord` bound.
+# If https://github.com/petgraph/petgraph/issues/646 is solved, go back to upstream.
+petgraph = { version = "0.6", git = "https://github.com/xldenis/petgraph", rev = "04cecb7" } 
 indexmap = { version = "1.7.0", features = ["serde"] }
 toml = "0.5.8"
 why3 = { path = "../why3", features = ["serialize"] }

creusot/src/analysis/liveness_no_drop.rs

@@ -116,22 +116,6 @@ where
     }
 }
 
-struct YieldResumeEffect<'a, T>(&'a mut T);
-
-impl<'tcx, T> Visitor<'tcx> for YieldResumeEffect<'_, T>
-where
-    T: GenKill<Local>,
-{
-    fn visit_place(&mut self, place: &mir::Place<'tcx>, context: PlaceContext, location: Location) {
-        DefUse::apply(self.0, *place, context);
-        self.visit_projection(place.as_ref(), context, location);
-    }
-
-    fn visit_local(&mut self, local: Local, context: PlaceContext, _: Location) {
-        DefUse::apply(self.0, local.into(), context);
-    }
-}
-
 #[derive(Eq, PartialEq, Clone)]
 enum DefUse {
     Def,

creusot/src/backend.rs

@@ -38,7 +38,7 @@ pub(crate) mod traits;
 pub(crate) mod ty;
 pub(crate) mod ty_inv;
 
-#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
+#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
 pub(crate) enum TransId {
     Item(DefId),
     TyInv(TyInvKind),
@@ -422,7 +422,7 @@ pub(crate) fn closure_generic_decls(
     mut def_id: DefId,
 ) -> impl Iterator<Item = Decl> + '_ {
     loop {
-        if tcx.is_closure_or_coroutine(def_id) {
+        if tcx.is_closure_like(def_id) {
             def_id = tcx.parent(def_id);
         } else {
             break;
@@ -440,7 +440,7 @@ pub(crate) fn all_generic_decls_for(tcx: TyCtxt, def_id: DefId) -> impl Iterator
 
 pub(crate) fn own_generic_decls_for(tcx: TyCtxt, def_id: DefId) -> impl Iterator<Item = Decl> + '_ {
     let generics = tcx.generics_of(def_id);
-    generic_decls(generics.params.iter())
+    generic_decls(generics.own_params.iter())
 }
 
 fn generic_decls<'tcx, I: Iterator<Item = &'tcx GenericParamDef> + 'tcx>(

creusot/src/backend/clone_map.rs

@@ -132,7 +132,7 @@ impl<'tcx> Namer<'tcx> for Dependencies<'tcx> {
     fn ty(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
         let mut node = DepNode::new(self.tcx, (def_id, subst));
 
-        if self.tcx.is_closure_or_coroutine(def_id) {
+        if self.tcx.is_closure_like(def_id) {
             node = DepNode::Type(Ty::new_closure(self.tcx, def_id, subst));
         }
 
@@ -624,7 +624,7 @@ struct TyVisitor<'tcx, F: FnMut(Ty<'tcx>)> {
 }
 
 impl<'tcx, F: FnMut(Ty<'tcx>)> TypeVisitor<TyCtxt<'tcx>> for TyVisitor<'tcx, F> {
-    fn visit_ty(&mut self, t: Ty<'tcx>) -> std::ops::ControlFlow<Self::BreakTy> {
+    fn visit_ty(&mut self, t: Ty<'tcx>) {
         let t = match t.kind() {
             // Box<T, A> is treated as T, the A param is ignored
             TyKind::Adt(adt_def, adt_subst) if adt_def.is_box() => adt_subst.type_at(0),

creusot/src/backend/clone_map/elaborator.rs

@@ -306,7 +306,7 @@ impl<'tcx> Namer<'tcx> for SymNamer<'tcx> {
     fn ty(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
         let mut node = DepNode::new(self.tcx, (def_id, subst));
 
-        if self.tcx.is_closure_or_coroutine(def_id) {
+        if self.tcx.is_closure_like(def_id) {
             node = DepNode::Type(Ty::new_closure(self.tcx, def_id, subst));
         }
 

creusot/src/backend/clone_map/expander.rs

@@ -12,7 +12,7 @@ use petgraph::Direction;
 use rustc_hir::def_id::DefId;
 use rustc_middle::{
     mir::Mutability,
-    ty::{AliasKind, GenericArgsRef, ParamEnv, Ty, TyKind},
+    ty::{AliasTyKind, GenericArgsRef, ParamEnv, Ty, TyKind},
 };
 
 use super::*;
@@ -150,7 +150,7 @@ impl<'a, 'tcx> Expander<'a, 'tcx> {
         // Check the substitution for node dependencies on closures
         walk_types(key_subst, |t| {
             let node = match t.kind() {
-                TyKind::Alias(AliasKind::Projection, pty) => {
+                TyKind::Alias(AliasTyKind::Projection, pty) => {
                     let node = DepNode::new(ctx.tcx, (pty.def_id, pty.args));
                     Some(self.resolve_dep(ctx, node))
                 }
@@ -159,7 +159,7 @@ impl<'a, 'tcx> Expander<'a, 'tcx> {
                 TyKind::Int(ity) => Some(DepNode::Builtin(int_to_prelude(*ity))),
                 TyKind::Uint(uty) => Some(DepNode::Builtin(uint_to_prelude(*uty))),
                 TyKind::Slice(_) => Some(DepNode::Builtin(PreludeModule::Slice)),
-                TyKind::RawPtr(_) => Some(DepNode::Builtin(PreludeModule::Opaque)),
+                TyKind::RawPtr(_, _) => Some(DepNode::Builtin(PreludeModule::Opaque)),
                 TyKind::Adt(_, _) => Some(DepNode::Type(t)),
                 _ => None,
             };

creusot/src/backend/dependency.rs

@@ -1,9 +1,10 @@
 use heck::ToSnakeCase;
+use rustc_ast_ir::visit::VisitorResult;
 use rustc_hir::{def::DefKind, def_id::DefId};
 use rustc_macros::{TypeFoldable, TypeVisitable};
 use rustc_middle::ty::{EarlyBinder, GenericArgs, GenericArgsRef, ParamEnv, Ty, TyCtxt, TyKind};
 use rustc_span::Symbol;
-use rustc_type_ir::{fold::TypeFoldable, visit::TypeVisitable, AliasKind, Interner};
+use rustc_type_ir::{fold::TypeFoldable, visit::TypeVisitable, AliasTyKind, Interner};
 
 use crate::{
     ctx::TranslationCtx,
@@ -19,7 +20,7 @@ use super::{ty_inv::TyInvKind, PreludeModule, TransId};
 /// These should be used both to power the cloning system and to order the overall translation of items in Creusot.
 ///
 
-#[derive(Copy, Clone, PartialEq, Eq, Debug, Hash, PartialOrd, Ord, TypeVisitable, TypeFoldable)]
+#[derive(Copy, Clone, PartialEq, Eq, Debug, Hash, TypeVisitable, TypeFoldable)]
 pub(crate) enum Dependency<'tcx> {
     Type(Ty<'tcx>),
     Item(DefId, GenericArgsRef<'tcx>),
@@ -42,11 +43,8 @@ pub(crate) enum ExtendedId {
 }
 
 impl<'tcx, I: Interner> TypeVisitable<I> for ExtendedId {
-    fn visit_with<V: rustc_type_ir::visit::TypeVisitor<I>>(
-        &self,
-        _: &mut V,
-    ) -> std::ops::ControlFlow<V::BreakTy> {
-        std::ops::ControlFlow::Continue(())
+    fn visit_with<V: rustc_type_ir::visit::TypeVisitor<I>>(&self, _: &mut V) -> V::Result {
+        V::Result::output()
     }
 }
 
@@ -123,7 +121,7 @@ impl<'tcx> Dependency<'tcx> {
             Dependency::Type(t) | Dependency::TyInv(t, _) => match t.kind() {
                 TyKind::Adt(def, substs) => Some((def.did(), substs)),
                 TyKind::Closure(id, substs) => Some((*id, substs)),
-                TyKind::Alias(AliasKind::Projection, aty) => Some((aty.def_id, aty.args)),
+                TyKind::Alias(AliasTyKind::Projection, aty) => Some((aty.def_id, aty.args)),
                 _ => None,
             },
             Dependency::Hacked(_, id, substs) => Some((id, substs)),

creusot/src/backend/logic/vcgen.rs

@@ -187,6 +187,7 @@ pub enum VCError<'tcx> {
     /// Same here...
     Closure(Span),
     /// Variants are currently restricted to `Int`
+    #[allow(dead_code)] // this lint is too agressive
     UnsupportedVariant(Ty<'tcx>, Span),
 }
 

creusot/src/backend/place.rs

@@ -84,10 +84,8 @@ fn create_assign_rec<'tcx>(
     use ProjectionElem::*;
     match &proj[proj_ix] {
         Deref => {
-            use rustc_hir::Mutability::*;
-
-            let mutability = place_ty.ty.builtin_deref(false).expect("raw pointer").mutbl;
-            if mutability == Mut {
+            let mutable = place_ty.ty.is_mutable_ptr();
+            if mutable {
                 RecUp {
                     record: Box::new(translate_rplace(ctx, names, locals, base, &proj[..proj_ix])),
                     updates: vec![("current".into(), inner)],
@@ -182,9 +180,8 @@ pub(crate) fn translate_rplace<'tcx, N: Namer<'tcx>>(
     for elem in proj {
         match elem {
             Deref => {
-                use rustc_hir::Mutability::*;
-                let mutability = place_ty.ty.builtin_deref(false).expect("raw pointer").mutbl;
-                if mutability == Mut {
+                let mutable = place_ty.ty.is_mutable_ptr();
+                if mutable {
                     inner = Current(Box::new(inner))
                 }
             }