Update to toolchain 2023-06-29

cargo-creusot/src/bin/creusot-rustc.rs

@@ -4,6 +4,7 @@ extern crate lazy_static;
 extern crate rustc_driver;
 extern crate rustc_errors;
 extern crate rustc_interface;
+extern crate rustc_session;
 
 #[macro_use]
 extern crate log;
@@ -14,6 +15,7 @@ use creusot::callbacks::*;
 use rustc_driver::{RunCompiler, DEFAULT_LOCALE_RESOURCES};
 use rustc_errors::{emitter::EmitterWriter, TerminalUrl};
 use rustc_interface::interface::try_print_query_stack;
+use rustc_session::{config::ErrorOutputType, EarlyErrorHandler};
 use std::{env, panic, panic::PanicInfo, process::Command};
 
 const BUG_REPORT_URL: &'static str = &"https://github.com/xldenis/creusot/issues/new";
@@ -67,7 +69,8 @@ struct DefaultCallbacks;
 impl rustc_driver::Callbacks for DefaultCallbacks {}
 
 fn main() {
-    rustc_driver::init_rustc_env_logger();
+    let handler = EarlyErrorHandler::new(ErrorOutputType::default());
+    rustc_driver::init_rustc_env_logger(&handler);
     env_logger::init();
     lazy_static::initialize(&ICE_HOOK);
 

ci/rust-toolchain

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2023-05-26"
-components = [ "rustfmt", "rustc-dev", "llvm-tools-preview" ]
+channel = "nightly-2023-06-29"
+components = [ "rustfmt", "rustc-dev", "llvm-tools" ]

creusot-contracts-proc/src/invariant.rs

@@ -56,7 +56,7 @@ pub struct Loop {
 
 fn filter_invariants(attrs: &mut Vec<Attribute>) -> Vec<Attribute> {
     attrs
-        .drain_filter(|attr| attr.path().get_ident().map(|i| i == "invariant").unwrap_or(false))
+        .extract_if(|attr| attr.path().get_ident().map(|i| i == "invariant").unwrap_or(false))
         .collect()
 }
 

creusot-contracts-proc/src/lib.rs

@@ -1,4 +1,4 @@
-#![feature(box_patterns, drain_filter, extend_one, proc_macro_def_site)]
+#![feature(box_patterns, extract_if, extend_one, proc_macro_def_site)]
 extern crate proc_macro;
 use extern_spec::ExternSpecs;
 use pearlite_syn::*;

creusot/Cargo.toml

@@ -24,7 +24,6 @@ similar = "2.2"
 termcolor = "1.1"
 arraydeque = "0.4"
 creusot-contracts = { path = "../creusot-contracts", features = ["typechecker"] }
-cargo-creusot = { path = "../cargo-creusot" }
 escargot = { version = "0.5" }
 [[test]]
 name = "ui"

creusot/src/analysis.rs

@@ -111,7 +111,6 @@ pub(crate) fn categorize(context: PlaceContext) -> Option<DefUse> {
         PlaceContext::MutatingUse(MutatingUseContext::Borrow) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::SharedBorrow) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::ShallowBorrow) |
-        PlaceContext::NonMutatingUse(NonMutatingUseContext::UniqueBorrow) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::PlaceMention) |
         PlaceContext::MutatingUse(MutatingUseContext::AddressOf) |
         PlaceContext::NonMutatingUse(NonMutatingUseContext::AddressOf) |

creusot/src/analysis/frozen_locals.rs

@@ -121,15 +121,15 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
     type Idx = BorrowIndex;
 
     fn before_statement_effect(
-        &self,
+        &mut self,
         _trans: &mut impl GenKill<Self::Idx>,
         _statement: &mir::Statement<'tcx>,
         _location: Location,
     ) {
     }
 
     fn statement_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         stmt: &mir::Statement<'tcx>,
         location: Location,
@@ -184,15 +184,15 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
     }
 
     fn before_terminator_effect(
-        &self,
+        &mut self,
         _trans: &mut impl GenKill<Self::Idx>,
         _terminator: &mir::Terminator<'tcx>,
         _location: Location,
     ) {
     }
 
     fn terminator_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         terminator: &mir::Terminator<'tcx>,
         location: Location,
@@ -211,7 +211,7 @@ impl<'tcx> dataflow::GenKillAnalysis<'tcx> for Borrows<'_, 'tcx> {
     }
 
     fn call_return_effect(
-        &self,
+        &mut self,
         _trans: &mut impl GenKill<Self::Idx>,
         _block: mir::BasicBlock,
         _return_places: dataflow::CallReturnPlaces<'_, 'tcx>,

creusot/src/analysis/init_locals.rs

@@ -34,7 +34,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
     type Idx = Local;
 
     fn statement_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         statement: &mir::Statement<'tcx>,
         loc: Location,
@@ -43,7 +43,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
     }
 
     fn terminator_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         terminator: &Terminator<'tcx>,
         loc: Location,
@@ -52,7 +52,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
     }
 
     fn call_return_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         _block: BasicBlock,
         return_places: dataflow::CallReturnPlaces<'_, 'tcx>,
@@ -62,7 +62,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeInitializedLocals {
 
     /// See `Analysis::apply_yield_resume_effect`.
     fn yield_resume_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         _resume_block: BasicBlock,
         resume_place: mir::Place<'tcx>,
@@ -114,7 +114,6 @@ where
                 | NonMutatingUseContext::Copy
                 | NonMutatingUseContext::SharedBorrow
                 | NonMutatingUseContext::ShallowBorrow
-                | NonMutatingUseContext::UniqueBorrow
                 | NonMutatingUseContext::AddressOf
                 | NonMutatingUseContext::PlaceMention
                 | NonMutatingUseContext::Projection,

creusot/src/analysis/liveness_no_drop.rs

@@ -35,7 +35,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
     type Idx = Local;
 
     fn statement_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         statement: &mir::Statement<'tcx>,
         location: Location,
@@ -44,7 +44,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
     }
 
     fn terminator_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         terminator: &mir::Terminator<'tcx>,
         location: Location,
@@ -53,7 +53,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
     }
 
     fn call_return_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         _block: mir::BasicBlock,
         return_places: CallReturnPlaces<'_, 'tcx>,
@@ -66,7 +66,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop {
     }
 
     fn yield_resume_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         _resume_block: mir::BasicBlock,
         resume_place: mir::Place<'tcx>,
@@ -196,8 +196,7 @@ impl DefUse {
                 | NonMutatingUseContext::Move
                 | NonMutatingUseContext::ShallowBorrow
                 | NonMutatingUseContext::SharedBorrow
-                | NonMutatingUseContext::PlaceMention
-                | NonMutatingUseContext::UniqueBorrow,
+                | NonMutatingUseContext::PlaceMention,
             ) => Some(DefUse::Use),
             PlaceContext::MutatingUse(MutatingUseContext::Drop) => None,
 

creusot/src/analysis/uninit_locals.rs

@@ -35,7 +35,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
     type Idx = Local;
 
     fn statement_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         statement: &mir::Statement<'tcx>,
         loc: Location,
@@ -44,7 +44,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
     }
 
     fn terminator_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         terminator: &Terminator<'tcx>,
         loc: Location,
@@ -53,7 +53,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
     }
 
     fn call_return_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         _block: BasicBlock,
         return_places: dataflow::CallReturnPlaces<'_, 'tcx>,
@@ -67,7 +67,7 @@ impl<'tcx> GenKillAnalysis<'tcx> for MaybeUninitializedLocals {
 
     /// See `Analysis::apply_yield_resume_effect`.
     fn yield_resume_effect(
-        &self,
+        &mut self,
         trans: &mut impl GenKill<Self::Idx>,
         _resume_block: BasicBlock,
         resume_place: mir::Place<'tcx>,
@@ -112,7 +112,6 @@ where
                 | NonMutatingUseContext::Copy
                 | NonMutatingUseContext::SharedBorrow
                 | NonMutatingUseContext::ShallowBorrow
-                | NonMutatingUseContext::UniqueBorrow
                 | NonMutatingUseContext::AddressOf
                 | NonMutatingUseContext::PlaceMention
                 | NonMutatingUseContext::Projection,

creusot/src/backend/dependency.rs

@@ -109,9 +109,9 @@ impl<'tcx> Dependency<'tcx> {
         };
 
         match &mut self {
-            Dependency::Item(_, s) => *s = EarlyBinder(*s).subst(tcx, substs),
+            Dependency::Item(_, s) => *s = EarlyBinder::bind(*s).subst(tcx, substs),
             Dependency::Type(ty) | Dependency::TyInv(ty) => {
-                *ty = EarlyBinder(*ty).subst(tcx, substs)
+                *ty = EarlyBinder::bind(*ty).subst(tcx, substs)
             }
         };
         self

creusot/src/backend/term.rs

@@ -414,7 +414,7 @@ pub(super) fn mk_binders(func: Exp, args: Vec<Exp>) -> Exp {
 fn is_identity_from<'tcx>(tcx: TyCtxt<'tcx>, id: DefId, subst: SubstsRef<'tcx>) -> bool {
     if tcx.def_path_str(id) == "std::convert::From::from" && subst.len() == 1 {
         let out_ty: Ty<'tcx> = tcx.fn_sig(id).no_bound_vars().unwrap().output().skip_binder();
-        return subst[0].expect_ty() == EarlyBinder(out_ty).subst(tcx, subst);
+        return subst[0].expect_ty() == EarlyBinder::bind(out_ty).subst(tcx, subst);
     }
     false
 }

creusot/src/ctx.rs

@@ -29,7 +29,10 @@ use rustc_infer::traits::{Obligation, ObligationCause};
 use rustc_middle::{
     mir::{Body, Promoted},
     thir,
-    ty::{subst::InternalSubsts, GenericArg, ParamEnv, SubstsRef, Ty, TyCtxt, Visibility},
+    ty::{
+        subst::InternalSubsts, Clause, GenericArg, ParamEnv, Predicate, SubstsRef, Ty, TyCtxt,
+        Visibility,
+    },
 };
 use rustc_span::{RealFileName, Span, Symbol, DUMMY_SP};
 use rustc_trait_selection::traits::SelectionContext;
@@ -222,25 +225,33 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
     }
 
     pub(crate) fn crash_and_error(&self, span: Span, msg: &str) -> ! {
-        self.tcx.sess.span_fatal_with_code(span, msg, DiagnosticId::Error(String::from("creusot")))
+        self.tcx.sess.span_fatal_with_code(
+            span,
+            msg.to_string(),
+            DiagnosticId::Error(String::from("creusot")),
+        )
     }
 
     pub(crate) fn fatal_error(&self, span: Span, msg: &str) -> DiagnosticBuilder<'tcx, !> {
         self.tcx.sess.struct_span_fatal_with_code(
             span,
-            msg,
+            msg.to_string(),
             DiagnosticId::Error(String::from("creusot")),
         )
     }
 
     pub(crate) fn error(&self, span: Span, msg: &str) {
-        self.tcx.sess.span_err_with_code(span, msg, DiagnosticId::Error(String::from("creusot")))
+        self.tcx.sess.span_err_with_code(
+            span,
+            msg.to_string(),
+            DiagnosticId::Error(String::from("creusot")),
+        )
     }
 
     pub(crate) fn warn(&self, span: Span, msg: &str) {
         self.tcx.sess.span_warn_with_code(
             span,
-            msg,
+            msg.to_string(),
             DiagnosticId::Lint {
                 name: String::from("creusot"),
                 has_future_breakage: false,
@@ -343,17 +354,28 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
                 for pred in es.predicates_for(self.tcx, subst) {
                     let obligation_cause = ObligationCause::dummy();
                     let obligation = Obligation::new(self.tcx, obligation_cause, param_env, pred);
-                    if !selcx.predicate_may_hold_fatal(&obligation) {
+                    if selcx.evaluate_root_obligation(&obligation).map_or(
+                        false, // Overflow has occurred, and treat the obligation as possibly holding.
+                        |result| !result.may_apply(),
+                    ) {
                         additional_predicates.push(
                             self.tcx.try_normalize_erasing_regions(base_env, pred).unwrap_or(pred),
                         )
                     }
                 }
             }
 
-            additional_predicates.extend(base_env.caller_bounds());
+            additional_predicates.extend::<Vec<Predicate>>(
+                base_env.caller_bounds().into_iter().map(Clause::as_predicate).collect(),
+            );
             ParamEnv::new(
-                self.mk_predicates(&additional_predicates),
+                self.mk_clauses(
+                    &(additional_predicates
+                        .into_iter()
+                        .map(Predicate::expect_clause)
+                        .collect::<Vec<Clause>>()
+                        .as_slice()),
+                ),
                 rustc_infer::traits::Reveal::UserFacing,
                 rustc_hir::Constness::NotConst,
             )

creusot/src/extended_location.rs

@@ -1,5 +1,5 @@
 use rustc_middle::mir::Location;
-use rustc_mir_dataflow::{self as dataflow, Analysis, Results, ResultsCursor};
+use rustc_mir_dataflow::{self as dataflow, Analysis, AnalysisResults, Results, ResultsCursor};
 use std::borrow::Borrow;
 
 // Dataflow locations
@@ -39,6 +39,7 @@ impl ExtendedLocation {
     where
         A: Analysis<'tcx, Direction = D>,
         D: Dir,
+        R: AnalysisResults<'tcx, A>,
         R: Borrow<Results<'tcx, A>>,
     {
         use ExtendedLocation::*;

creusot/src/lib.rs

@@ -1,5 +1,5 @@
 #![feature(rustc_private, register_tool)]
-#![feature(box_patterns, control_flow_enum, drain_filter)]
+#![feature(box_patterns, control_flow_enum, extract_if)]
 #![feature(let_chains, never_type, try_blocks)]
 
 #[macro_use]