Update to 31/01/2024 rustc

ci/rust-toolchain

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

creusot-contracts/src/lib.rs

@@ -203,8 +203,6 @@ mod macros {
     /// This means you cannot `#[open]` a body which refers to a `pub(crate)` symbol.
     pub use creusot_contracts_dummy::open;
 
-    pub use creusot_contracts_proc::DeepModel;
-
     pub use creusot_contracts_proc::Resolve;
 }
 
@@ -251,6 +249,7 @@ pub mod resolve;
 pub mod util;
 pub mod well_founded;
 
+pub use macros::*;
 // We add some common things at the root of the creusot-contracts library
 pub use crate::{
     logic::{IndexLogic as _, Int, OrdLogic, Seq},
@@ -297,3 +296,7 @@ macro_rules! vec {
     );
     ($($x:expr,)*) => (vec![$($x),*])
 }
+
+// #[logic]
+// #[open]
+// pub fn foo() -> bool { true }

creusot-rustc/src/main.rs

@@ -14,9 +14,9 @@ extern crate log;
 use creusot::callbacks::*;
 use options::CreusotArgs;
 use rustc_driver::{RunCompiler, DEFAULT_LOCALE_RESOURCES};
-use rustc_errors::emitter::EmitterWriter;
+use rustc_errors::emitter::HumanEmitter;
 use rustc_interface::interface::try_print_query_stack;
-use rustc_session::{config::ErrorOutputType, EarlyErrorHandler};
+use rustc_session::{config::ErrorOutputType, EarlyDiagCtxt};
 use std::{env, panic, panic::PanicInfo, process::Command};
 
 const BUG_REPORT_URL: &'static str = &"https://github.com/xldenis/creusot/issues/new";
@@ -37,10 +37,10 @@ fn report_panic(info: &PanicInfo) {
     let fallback_bundle =
         rustc_errors::fallback_fluent_bundle(DEFAULT_LOCALE_RESOURCES.to_vec(), false);
 
-    let emitter = Box::new(EmitterWriter::stderr(rustc_errors::ColorConfig::Auto, fallback_bundle));
-    let handler = rustc_errors::Handler::with_emitter(emitter);
+    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_without_error("Creusot has panic-ed!");
+    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));
 
@@ -58,7 +58,7 @@ struct DefaultCallbacks;
 impl rustc_driver::Callbacks for DefaultCallbacks {}
 
 fn main() {
-    let handler = EarlyErrorHandler::new(ErrorOutputType::default());
+    let handler = EarlyDiagCtxt::new(ErrorOutputType::default());
     rustc_driver::init_rustc_env_logger(&handler);
     env_logger::init();
     lazy_static::initialize(&ICE_HOOK);
@@ -107,6 +107,7 @@ fn setup_plugin() {
         args.push("-Zcrate-attr=feature(rustc_attrs)".to_owned());
         args.push("-Zcrate-attr=feature(unsized_fn_params)".to_owned());
         args.push("--allow=internal_features".to_owned());
+        args.push("-Zdump-mir=speccleanup".to_owned());
         args.extend(["--cfg", "creusot"].into_iter().map(str::to_owned));
         debug!("creusot args={:?}", args);
 
@@ -137,7 +138,7 @@ fn _emit_warning(text: String) {
     let fallback_bundle =
         rustc_errors::fallback_fluent_bundle(DEFAULT_LOCALE_RESOURCES.to_vec(), false);
 
-    let emitter = Box::new(EmitterWriter::stderr(rustc_errors::ColorConfig::Auto, fallback_bundle));
-    let handler = rustc_errors::Handler::with_emitter(emitter);
+    let emitter = Box::new(HumanEmitter::stderr(rustc_errors::ColorConfig::Auto, fallback_bundle));
+    let handler = rustc_errors::DiagCtxt::with_emitter(emitter);
     handler.warn(text);
 }

creusot/src/analysis.rs

@@ -112,7 +112,7 @@ pub(crate) fn categorize(context: PlaceContext) -> Option<DefUse> {
         // cross suspension points so this behavior is unproblematic.
         PlaceContext::MutatingUse(MutatingUseContext::Borrow) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::SharedBorrow) |
-        PlaceContext::NonMutatingUse(NonMutatingUseContext::ShallowBorrow) |
+        PlaceContext::NonMutatingUse(NonMutatingUseContext::FakeBorrow) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::PlaceMention) |
         PlaceContext::MutatingUse(MutatingUseContext::AddressOf) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::AddressOf) |

creusot/src/analysis/frozen_locals.rs

@@ -185,7 +185,7 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
 
     fn before_terminator_effect(
         &mut self,
-        _trans: &mut impl GenKill<Self::Idx>,
+        _trans: &mut Self::Domain,
         _terminator: &mir::Terminator<'tcx>,
         _location: Location,
     ) {
@@ -213,7 +213,7 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
 
     fn call_return_effect(
         &mut self,
-        _trans: &mut impl GenKill<Self::Idx>,
+        _trans: &mut Self::Domain,
         _block: mir::BasicBlock,
         _return_places: CallReturnPlaces<'_, 'tcx>,
     ) {

creusot/src/analysis/init_locals.rs

@@ -54,7 +54,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
 
     fn call_return_effect(
         &mut self,
-        trans: &mut impl GenKill<Self::Idx>,
+        trans: &mut Self::Domain,
         _block: BasicBlock,
         return_places: CallReturnPlaces<'_, 'tcx>,
     ) {
@@ -108,7 +108,7 @@ where
                 NonMutatingUseContext::Inspect
                 | NonMutatingUseContext::Copy
                 | NonMutatingUseContext::SharedBorrow
-                | NonMutatingUseContext::ShallowBorrow
+                | NonMutatingUseContext::FakeBorrow
                 | NonMutatingUseContext::AddressOf
                 | NonMutatingUseContext::PlaceMention
                 | NonMutatingUseContext::Projection,

creusot/src/analysis/liveness_no_drop.rs

@@ -55,7 +55,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
 
     fn call_return_effect(
         &mut self,
-        trans: &mut impl GenKill<Self::Idx>,
+        trans: &mut Self::Domain,
         _block: mir::BasicBlock,
         return_places: CallReturnPlaces<'_, 'tcx>,
     ) {
@@ -186,7 +186,7 @@ impl DefUse {
                 | NonMutatingUseContext::Copy
                 | NonMutatingUseContext::Inspect
                 | NonMutatingUseContext::Move
-                | NonMutatingUseContext::ShallowBorrow
+                | NonMutatingUseContext::FakeBorrow
                 | NonMutatingUseContext::SharedBorrow
                 | NonMutatingUseContext::PlaceMention,
             ) => Some(DefUse::Use),

creusot/src/analysis/not_final_places.rs

@@ -478,7 +478,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for NotFinalPlaces<'tcx> {
 
     fn call_return_effect(
         &mut self,
-        _trans: &mut impl GenKill<Self::Idx>,
+        _trans: &mut Self::Domain,
         _block: BasicBlock,
         _return_places: CallReturnPlaces<'_, 'tcx>,
     ) {
@@ -496,7 +496,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for NotFinalPlaces<'tcx> {
 
     fn before_terminator_effect(
         &mut self,
-        trans: &mut impl GenKill<Self::Idx>,
+        trans: &mut Self::Domain,
         terminator: &mir::Terminator<'tcx>,
         location: Location,
     ) {

creusot/src/analysis/uninit_locals.rs

@@ -55,7 +55,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
 
     fn call_return_effect(
         &mut self,
-        trans: &mut impl GenKill<Self::Idx>,
+        trans: &mut Self::Domain,
         _block: BasicBlock,
         return_places: CallReturnPlaces<'_, 'tcx>,
     ) {
@@ -106,7 +106,7 @@ where
                 NonMutatingUseContext::Inspect
                 | NonMutatingUseContext::Copy
                 | NonMutatingUseContext::SharedBorrow
-                | NonMutatingUseContext::ShallowBorrow
+                | NonMutatingUseContext::FakeBorrow
                 | NonMutatingUseContext::AddressOf
                 | NonMutatingUseContext::PlaceMention
                 | NonMutatingUseContext::Projection,

creusot/src/backend.rs

@@ -258,9 +258,9 @@ impl<'tcx> Why3Generator<'tcx> {
             self.translate(adt_did);
         }
 
-        let (modl, deps) = ty_inv::build_inv_module(self, inv_kind);
+        let deps = ty_inv::build_inv_module(self, inv_kind);
         self.dependencies.insert(tid, deps);
-        self.functions.insert(tid, TranslatedItem::TyInv { modl });
+        self.functions.insert(tid, TranslatedItem::TyInv {});
     }
 
     // pub(crate) fn item(&self, def_id: DefId) -> Option<&TranslatedItem> {
@@ -413,7 +413,7 @@ pub(crate) fn closure_generic_decls(
     mut def_id: DefId,
 ) -> impl Iterator<Item = Decl> + '_ {
     loop {
-        if tcx.is_closure(def_id) {
+        if tcx.is_closure_or_coroutine(def_id) {
             def_id = tcx.parent(def_id);
         } else {
             break;

creusot/src/backend/clone_map.rs

@@ -140,7 +140,7 @@ impl<'tcx> Namer<'tcx> for CloneMap<'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(def_id) {
+        if self.tcx.is_closure_or_coroutine(def_id) {
             node = DepNode::Type(Ty::new_closure(self.tcx, def_id, subst));
         }
 
@@ -282,8 +282,10 @@ impl<'tcx> CloneNames<'tcx> {
     }
     fn insert(&mut self, key: DepNode<'tcx>) -> Kind {
         *self.names.entry(key).or_insert_with(|| {
-            if let DepNode::Type(ty) = key && !matches!(ty.kind(), TyKind::Alias(_, _)) {
-                let kind =  if let Some((did, _)) = key.did() {
+            if let DepNode::Type(ty) = key
+                && !matches!(ty.kind(), TyKind::Alias(_, _))
+            {
+                let kind = if let Some((did, _)) = key.did() {
                     let name = Symbol::intern(&*module_name(self.tcx, did));
                     Kind::Named(name)
                 } else {

creusot/src/backend/clone_map/elaborator.rs

@@ -289,7 +289,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(def_id) {
+        if self.tcx.is_closure_or_coroutine(def_id) {
             node = DepNode::Type(Ty::new_closure(self.tcx, def_id, subst));
         }
 

creusot/src/backend/clone_map/expander.rs

@@ -214,7 +214,9 @@ impl<'a, 'tcx> Expander<'a, 'tcx> {
             TyInvKind::from_ty(ctx.tcx, ty).unwrap_or(TyInvKind::Trivial)
         };
 
-        if let TransId::TyInv(self_kind) = self.self_id && self_kind == inv_kind {
+        if let TransId::TyInv(self_kind) = self.self_id
+            && self_kind == inv_kind
+        {
             return;
         }
 
@@ -238,7 +240,8 @@ impl<'a, 'tcx> Expander<'a, 'tcx> {
 
         // Dont clone laws into the trait / impl which defines them.
         if let Some(self_item) = ctx.tcx.opt_associated_item(self_did)
-            && self_item.container_id(ctx.tcx) == item.container_id(ctx.tcx) {
+            && self_item.container_id(ctx.tcx) == item.container_id(ctx.tcx)
+        {
             return;
         }
 

creusot/src/backend/dependency.rs

@@ -212,8 +212,9 @@ fn resolve_item<'tcx>(
     param_env: ParamEnv<'tcx>,
 ) -> Dependency<'tcx> {
     let resolved = if tcx.trait_of_item(item).is_some()
-        && let Some(resolved) = traits::resolve_opt(tcx, param_env, item, substs) {
-            resolved
+        && let Some(resolved) = traits::resolve_opt(tcx, param_env, item, substs)
+    {
+        resolved
     } else {
         (item, substs)
     };

creusot/src/backend/optimization.rs

@@ -274,14 +274,16 @@ impl<'tcx> SimplePropagator<'tcx> {
         match s {
             Statement::Assignment(_, r, _) => self.visit_rvalue(r),
             Statement::Resolve(_, _, p) => {
-              if let Some(l) = p.as_symbol() && self.dead.contains(&l) {
-
-              }
+                if let Some(l) = p.as_symbol()
+                    && self.dead.contains(&l)
+                {}
             }
             Statement::Assertion { cond, msg: _ } => self.visit_term(cond),
-            Statement::Call(_, _, _, args, _) => args.iter_mut().for_each(|a| self.visit_operand(a)),
-            Statement::AssumeBorrowInv(_) => {},
-            Statement::AssertTyInv( _) => {},
+            Statement::Call(_, _, _, args, _) => {
+                args.iter_mut().for_each(|a| self.visit_operand(a))
+            }
+            Statement::AssumeBorrowInv(_) => {}
+            Statement::AssertTyInv(_) => {}
         }
     }
 
@@ -312,10 +314,12 @@ impl<'tcx> SimplePropagator<'tcx> {
     fn visit_operand(&mut self, op: &mut Operand<'tcx>) {
         match op {
             Operand::Move(p) | Operand::Copy(p) => {
-              if let Some(l) = p.as_symbol() && let Some(v) = self.prop.remove(&l) {
-                *op = v;
-              }
-            },
+                if let Some(l) = p.as_symbol()
+                    && let Some(v) = self.prop.remove(&l)
+                {
+                    *op = v;
+                }
+            }
             Operand::Constant(_) => {}
         }
     }

creusot/src/backend/program.rs

@@ -128,7 +128,7 @@ pub(crate) fn translate_closure<'tcx>(
     ctx: &mut Why3Generator<'tcx>,
     def_id: DefId,
 ) -> (CloneSummary<'tcx>, Module, Option<Module>) {
-    assert!(ctx.is_closure(def_id));
+    assert!(ctx.is_closure_or_coroutine(def_id));
     let (summary, func) = translate_function(ctx, def_id);
     (summary, closure_ty(ctx, def_id), func)
 }
@@ -146,7 +146,7 @@ pub(crate) fn translate_function<'tcx, 'sess>(
     };
     let body = to_why(ctx, &mut names, body_ids[0]);
 
-    if ctx.tcx.is_closure(def_id) {
+    if ctx.tcx.is_closure_or_coroutine(def_id) {
         closure_aux_defs(ctx, def_id)
     };
 
@@ -206,7 +206,7 @@ fn lower_promoted<'tcx>(
     body_id: BodyId,
 ) -> Decl {
     let promoted = promoted::translate_promoted(ctx, body_id);
-    let (sig, fmir) = promoted.unwrap_or_else(|e| e.emit(ctx.tcx.sess));
+    let (sig, fmir) = promoted.unwrap_or_else(|e| e.emit(ctx.tcx));
 
     let mut sig = sig_to_why3(ctx, names, &sig, body_id.def_id());
     sig.name = format!("promoted{:?}", body_id.promoted.unwrap().as_usize()).into();
@@ -791,7 +791,7 @@ fn func_call_to_why3<'tcx>(
     let mut args: Vec<_> = args.into_iter().map(|a| a.to_why(ctx, names, locals)).collect();
     let fname = names.value(id, subst);
 
-    let exp = if ctx.is_closure(id) {
+    let exp = if ctx.is_closure_or_coroutine(id) {
         assert!(args.len() == 2, "closures should only have two arguments (env, args)");
 
         let real_sig = ctx.signature_unclosure(subst.as_closure().sig(), Unsafety::Normal);

creusot/src/backend/ty.rs

@@ -15,7 +15,7 @@ use rustc_middle::ty::{
     GenericArgsRef, ParamEnv, Ty, TyCtxt, TyKind,
 };
 use rustc_span::{Span, Symbol, DUMMY_SP};
-use rustc_type_ir::sty::TyKind::*;
+use rustc_type_ir::TyKind::*;
 use std::collections::VecDeque;
 use why3::{
     declaration::{
@@ -455,7 +455,7 @@ pub(crate) fn ty_param_names(
     mut def_id: DefId,
 ) -> impl Iterator<Item = Ident> + '_ {
     loop {
-        if tcx.is_closure(def_id) {
+        if tcx.is_closure_or_coroutine(def_id) {
             def_id = tcx.parent(def_id);
         } else {
             break;

creusot/src/backend/ty_inv.rs

@@ -18,7 +18,7 @@ use rustc_macros::{TypeFoldable, TypeVisitable};
 use rustc_middle::ty::{GenericArg, GenericArgsRef, ParamEnv, Ty, TyCtxt, TyKind};
 use rustc_span::{Symbol, DUMMY_SP};
 use why3::{
-    declaration::{Axiom, Decl, Module, TyDecl},
+    declaration::{Axiom, Decl, TyDecl},
     exp::{Exp, Trigger},
     Ident,
 };
@@ -403,7 +403,7 @@ impl<'tcx> InvariantElaborator<'tcx> {
 pub(crate) fn build_inv_module<'tcx>(
     ctx: &mut Why3Generator<'tcx>,
     inv_kind: TyInvKind,
-) -> (Module, CloneSummary<'tcx>) {
+) -> CloneSummary<'tcx> {
     let mut names = CloneMap::new(ctx.tcx, TransId::TyInv(inv_kind));
     let generics = inv_kind.generics(ctx.tcx);
     let inv_axiom =
@@ -434,7 +434,7 @@ pub(crate) fn build_inv_module<'tcx>(
 
     decls.push(Decl::Axiom(inv_axiom));
 
-    (Module { name: util::inv_module_name(ctx.tcx, inv_kind), decls }, summary)
+    summary
 }
 
 fn axiom_name(ctx: &Why3Generator<'_>, inv_kind: TyInvKind) -> Ident {