Update dependencies (rustc nightly-2023-07-15, viper v-2023-07-05-0730)

analysis/src/bin/analysis-driver.rs

@@ -16,14 +16,15 @@ use prusti_rustc_interface::{
     borrowck::consumers::{self, BodyWithBorrowckFacts},
     data_structures::fx::FxHashMap,
     driver::Compilation,
+    errors,
     hir::def_id::{DefId, LocalDefId},
     interface::{interface, Config, Queries},
     middle::{
         query::{queries::mir_borrowck::ProvidedValue, ExternProviders, Providers},
         ty,
     },
     polonius_engine::{Algorithm, Output},
-    session::{Attribute, Session},
+    session::{self, Attribute, EarlyErrorHandler, Session},
 };
 use std::{cell::RefCell, rc::Rc};
 
@@ -146,6 +147,7 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
 
     fn after_analysis<'tcx>(
         &mut self,
+        _error_handler: &EarlyErrorHandler,
         compiler: &interface::Compiler,
         queries: &'tcx Queries<'tcx>,
     ) -> Compilation {
@@ -288,7 +290,10 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
 /// --analysis=ReachingDefsState or --analysis=DefinitelyInitializedAnalysis
 fn main() {
     env_logger::init();
-    prusti_rustc_interface::driver::init_rustc_env_logger();
+    let error_handler = EarlyErrorHandler::new(session::config::ErrorOutputType::HumanReadable(
+        errors::emitter::HumanReadableErrorType::Default(errors::emitter::ColorConfig::Auto),
+    ));
+    prusti_rustc_interface::driver::init_rustc_env_logger(&error_handler);
     let mut compiler_args = Vec::new();
     let mut callback_args = Vec::new();
     for arg in std::env::args() {

analysis/src/bin/gen-accessibility-driver.rs

@@ -9,15 +9,15 @@ use prusti_rustc_interface::{
     borrowck::consumers::{self, BodyWithBorrowckFacts},
     data_structures::fx::FxHashMap,
     driver::Compilation,
-    hir,
+    errors, hir,
     hir::def_id::LocalDefId,
     interface::{interface, Config, Queries},
     middle::{
         query::{queries::mir_borrowck::ProvidedValue, ExternProviders, Providers},
         ty,
     },
     polonius_engine::{Algorithm, Output},
-    session::Session,
+    session::{self, EarlyErrorHandler, Session},
     span::FileName,
 };
 use std::{cell::RefCell, path::PathBuf, rc::Rc};
@@ -99,6 +99,7 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
 
     fn after_analysis<'tcx>(
         &mut self,
+        _error_handler: &EarlyErrorHandler,
         compiler: &interface::Compiler,
         queries: &'tcx Queries<'tcx>,
     ) -> Compilation {
@@ -212,7 +213,10 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
 /// Run an analysis by calling like it rustc
 fn main() {
     env_logger::init();
-    prusti_rustc_interface::driver::init_rustc_env_logger();
+    let error_handler = EarlyErrorHandler::new(session::config::ErrorOutputType::HumanReadable(
+        errors::emitter::HumanReadableErrorType::Default(errors::emitter::ColorConfig::Auto),
+    ));
+    prusti_rustc_interface::driver::init_rustc_env_logger(&error_handler);
     let mut compiler_args = Vec::new();
     let mut callback_args = Vec::new();
     for arg in std::env::args() {

analysis/tests/test_analysis.rs

@@ -13,7 +13,7 @@ fn run_tests(mode: &str, path: &str, custom_args: Vec<String>) {
     let mut flags = Vec::new();
     flags.push("--edition 2018".to_owned());
     flags.push(format!("--sysroot {}", find_sysroot()));
-    flags.extend(custom_args.into_iter());
+    flags.extend(custom_args);
     config.target_rustcflags = Some(flags.join(" "));
     config.mode = mode.parse().expect("Invalid mode");
     config.rustc_path = find_compiled_executable("analysis-driver");

jni-gen/src/generators/module.rs

@@ -41,7 +41,7 @@ pub fn generate_module(class_names: Vec<&ClassName>) -> String {
         })
         .unwrap_or_else(|| "// No modules".to_string());
 
-    vec![
+    [
         "//! Automatically generated code\n".to_string(),
         "#![allow(non_snake_case)]\n".to_string(),
         "pub mod builtins;\n".to_string(),

prusti-common/src/vir/optimizations/folding/expressions.rs

@@ -163,7 +163,7 @@ fn check_requirements_conflict(
                 conflict_set.insert(base1);
             } else if base1 == base2 && !place1.has_prefix(place2) && !place2.has_prefix(place1) {
                 // Check if we have different variants.
-                for (part1, part2) in components1.into_iter().zip(components2.into_iter()) {
+                for (part1, part2) in components1.into_iter().zip(components2) {
                     match (part1, part2) {
                         (
                             ast::PlaceComponent::Variant(ast::Field { name: name1, .. }, _),

prusti-common/src/vir/optimizations/methods/purifier.rs

@@ -274,7 +274,13 @@ impl VarPurifier {
         }
     }
     fn get_replacement(&self, expr: &ast::Expr) -> ast::Expr {
-        let ast::Expr::Local(ast::Local {variable: var, position: pos}) = expr else { unreachable!() };
+        let ast::Expr::Local(ast::Local {
+            variable: var,
+            position: pos,
+        }) = expr
+        else {
+            unreachable!()
+        };
         let replacement = self
             .replacements
             .get(var)

prusti-common/src/vir/to_viper.rs

@@ -316,7 +316,9 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for Stmt {
                 )
             }
             Stmt::ApplyMagicWand(ref wand, ref pos) => {
-                let Expr::MagicWand(_, _, Some(borrow), _) = wand else { unreachable!() };
+                let Expr::MagicWand(_, _, Some(borrow), _) = wand else {
+                    unreachable!()
+                };
                 let borrow: usize = borrow_id(*borrow);
                 let borrow: Expr = borrow.into();
                 let inhale = ast.inhale(
@@ -618,7 +620,9 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for Expr {
                 ContainerOpKind::SeqLen => ast.seq_length(left.to_viper(context, ast)),
             },
             Expr::Seq(ty, elems, _pos) => {
-                let Type::Seq(box elem_ty) = ty else { unreachable!() };
+                let Type::Seq(box elem_ty) = ty else {
+                    unreachable!()
+                };
                 let viper_elem_ty = elem_ty.to_viper(context, ast);
                 if elems.is_empty() {
                     ast.empty_seq(viper_elem_ty)
@@ -631,7 +635,9 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for Expr {
                 }
             }
             Expr::Map(ty, elems, _pos) => {
-                let Type::Map(box key_ty, box val_ty) = ty else { unreachable!() };
+                let Type::Map(box key_ty, box val_ty) = ty else {
+                    unreachable!()
+                };
                 let viper_key_ty = key_ty.to_viper(context, ast);
                 let viper_val_ty = val_ty.to_viper(context, ast);
                 if elems.is_empty() {

prusti-contracts/prusti-contracts-proc-macros/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "prusti-contracts-proc-macros"
-version = "0.1.9"
+version = "0.1.10"
 authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 license = "MPL-2.0"
@@ -15,7 +15,7 @@ categories = ["development-tools", "development-tools::testing"]
 proc-macro = true
 
 [dependencies]
-prusti-specs = { path = "../prusti-specs", version = "0.1.9", optional = true }
+prusti-specs = { path = "../prusti-specs", version = "0.1.10", optional = true }
 proc-macro2 = { version = "1.0", optional = true }
 
 [features]

prusti-contracts/prusti-contracts/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "prusti-contracts"
-version = "0.1.9"
+version = "0.1.10"
 authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 license = "MPL-2.0"
@@ -12,7 +12,7 @@ keywords = ["prusti", "contracts", "verification", "formal", "specifications"]
 categories = ["development-tools", "development-tools::testing"]
 
 [dependencies]
-prusti-contracts-proc-macros = { path = "../prusti-contracts-proc-macros", version = "0.1.9" }
+prusti-contracts-proc-macros = { path = "../prusti-contracts-proc-macros", version = "0.1.10" }
 
 [dev-dependencies]
 trybuild = "1.0"

prusti-contracts/prusti-specs/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "prusti-specs"
-version = "0.1.9"
+version = "0.1.10"
 authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 license = "MPL-2.0"

prusti-contracts/prusti-specs/src/lib.rs

@@ -1,5 +1,5 @@
 #![deny(unused_must_use)]
-#![feature(drain_filter)]
+#![feature(extract_if)]
 #![feature(box_patterns)]
 #![feature(proc_macro_span)]
 #![feature(if_let_guard)]
@@ -78,7 +78,9 @@ fn extract_prusti_attributes(
                         // tokens identical to the ones passed by the native procedural
                         // macro call.
                         let mut iter = attr.tokens.into_iter();
-                        let TokenTree::Group(group) = iter.next().unwrap() else { unreachable!() };
+                        let TokenTree::Group(group) = iter.next().unwrap() else {
+                            unreachable!()
+                        };
                         assert!(iter.next().is_none(), "Unexpected shape of an attribute.");
                         group.stream()
                     }
@@ -597,10 +599,14 @@ pub fn refine_trait_spec(_attr: TokenStream, tokens: TokenStream) -> TokenStream
                 let parsed_predicate =
                     handle_result!(predicate::parse_predicate_in_impl(makro.mac.tokens.clone()));
 
-                let ParsedPredicate::Impl(predicate) = parsed_predicate else { unreachable!() };
+                let ParsedPredicate::Impl(predicate) = parsed_predicate else {
+                    unreachable!()
+                };
 
                 // Patch spec function: Rewrite self with _self: <SpecStruct>
-                let syn::Item::Fn(spec_function) = predicate.spec_function else { unreachable!() };
+                let syn::Item::Fn(spec_function) = predicate.spec_function else {
+                    unreachable!()
+                };
                 generated_spec_items.push(spec_function);
 
                 // Add patched predicate function to new items
@@ -883,7 +889,9 @@ fn extract_prusti_attributes_for_types(
                         // tokens identical to the ones passed by the native procedural
                         // macro call.
                         let mut iter = attr.tokens.into_iter();
-                        let TokenTree::Group(group) = iter.next().unwrap() else { unreachable!() };
+                        let TokenTree::Group(group) = iter.next().unwrap() else {
+                            unreachable!()
+                        };
                         group.stream()
                     }
                 };

prusti-contracts/prusti-specs/src/parse_closure_macro.rs

@@ -16,16 +16,16 @@ impl Parse for ClosureWithSpec {
 
         // collect and remove any specification attributes
         // leave other attributes intact
-        attrs.drain_filter(|attr| {
+        attrs.retain(|attr| {
             if let Some(id) = attr.path.get_ident() {
                 match id.to_string().as_ref() {
                     "requires" => pres.push(syn::parse2(attr.tokens.clone())),
                     "ensures" => posts.push(syn::parse2(attr.tokens.clone())),
-                    _ => return false,
+                    _ => return true,
                 }
-                true
-            } else {
                 false
+            } else {
+                true
             }
         });
         cl.attrs = attrs;

prusti-contracts/prusti-specs/src/specifications/preparser.rs

@@ -221,8 +221,7 @@ impl PrustiTokenStream {
                     PrustiToken::BinOp(span, PrustiBinaryOp::Rust(op)) => Ok(op.to_tokens(span)),
                     _ => err(token.span(), "unexpected Prusti syntax"),
                 })
-                .collect::<Result<Vec<_>, _>>()?
-                .into_iter(),
+                .collect::<Result<Vec<_>, _>>()?,
         ))
     }
 

prusti-contracts/prusti-std/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "prusti-std"
-version = "0.1.9"
+version = "0.1.10"
 authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 license = "MPL-2.0"
@@ -12,7 +12,7 @@ keywords = ["prusti", "contracts", "verification", "formal", "specifications"]
 categories = ["development-tools", "development-tools::testing"]
 
 [dependencies]
-prusti-contracts = { path = "../prusti-contracts", version = "0.1.9" }
+prusti-contracts = { path = "../prusti-contracts", version = "0.1.10" }
 
 # Forward "prusti" flag
 [features]

prusti-interface/src/environment/body.rs

@@ -2,11 +2,12 @@ use prusti_rustc_interface::{
     macros::{TyDecodable, TyEncodable},
     middle::{
         mir,
-        ty::{self, subst::SubstsRef, TyCtxt},
+        ty::{self, TyCtxt},
     },
     span::def_id::{DefId, LocalDefId},
 };
 use rustc_hash::FxHashMap;
+use rustc_middle::ty::GenericArgsRef;
 use std::{cell::RefCell, collections::hash_map::Entry, rc::Rc};
 
 use crate::environment::{borrowck::facts::BorrowckFacts, mir_storage};
@@ -80,7 +81,7 @@ impl<'tcx> PreLoadedBodies<'tcx> {
 /// - we are encoding an impure function, where the method is encoded only once
 ///   and calls are performed indirectly via contract exhale/inhale; or
 /// - when the caller is unknown, e.g. to check a pure function definition.
-type MonomorphKey<'tcx> = (DefId, SubstsRef<'tcx>, Option<DefId>);
+type MonomorphKey<'tcx> = (DefId, GenericArgsRef<'tcx>, Option<DefId>);
 
 /// Store for all the `mir::Body` which we've taken out of the compiler
 /// or imported from external crates, all of which are indexed by DefId
@@ -151,7 +152,7 @@ impl<'tcx> EnvBody<'tcx> {
     fn get_monomorphised(
         &self,
         def_id: DefId,
-        substs: SubstsRef<'tcx>,
+        substs: GenericArgsRef<'tcx>,
         caller_def_id: Option<DefId>,
     ) -> Option<MirBody<'tcx>> {
         self.monomorphised_bodies
@@ -162,7 +163,7 @@ impl<'tcx> EnvBody<'tcx> {
     fn set_monomorphised(
         &self,
         def_id: DefId,
-        substs: SubstsRef<'tcx>,
+        substs: GenericArgsRef<'tcx>,
         caller_def_id: Option<DefId>,
         body: MirBody<'tcx>,
     ) -> MirBody<'tcx> {
@@ -179,7 +180,7 @@ impl<'tcx> EnvBody<'tcx> {
                     ty::EarlyBinder::bind(body.0),
                 )
             } else {
-                ty::EarlyBinder::bind(body.0).subst(self.tcx, substs)
+                ty::EarlyBinder::bind(body.0).instantiate(self.tcx, substs)
             };
             v.insert(MirBody(monomorphised)).clone()
         } else {
@@ -201,7 +202,11 @@ impl<'tcx> EnvBody<'tcx> {
     /// with the given type substitutions.
     ///
     /// FIXME: This function is called only in pure contexts???
-    pub fn get_impure_fn_body(&self, def_id: LocalDefId, substs: SubstsRef<'tcx>) -> MirBody<'tcx> {
+    pub fn get_impure_fn_body(
+        &self,
+        def_id: LocalDefId,
+        substs: GenericArgsRef<'tcx>,
+    ) -> MirBody<'tcx> {
         if let Some(body) = self.get_monomorphised(def_id.to_def_id(), substs, None) {
             return body;
         }
@@ -231,7 +236,7 @@ impl<'tcx> EnvBody<'tcx> {
     pub fn get_closure_body(
         &self,
         def_id: DefId,
-        substs: SubstsRef<'tcx>,
+        substs: GenericArgsRef<'tcx>,
         caller_def_id: DefId,
     ) -> MirBody<'tcx> {
         if let Some(body) = self.get_monomorphised(def_id, substs, Some(caller_def_id)) {
@@ -246,7 +251,7 @@ impl<'tcx> EnvBody<'tcx> {
     pub fn get_pure_fn_body(
         &self,
         def_id: DefId,
-        substs: SubstsRef<'tcx>,
+        substs: GenericArgsRef<'tcx>,
         caller_def_id: DefId,
     ) -> MirBody<'tcx> {
         if let Some(body) = self.get_monomorphised(def_id, substs, Some(caller_def_id)) {
@@ -261,7 +266,7 @@ impl<'tcx> EnvBody<'tcx> {
     pub fn get_expression_body(
         &self,
         def_id: DefId,
-        substs: SubstsRef<'tcx>,
+        substs: GenericArgsRef<'tcx>,
         caller_def_id: DefId,
     ) -> MirBody<'tcx> {
         if let Some(body) = self.get_monomorphised(def_id, substs, Some(caller_def_id)) {
@@ -279,7 +284,7 @@ impl<'tcx> EnvBody<'tcx> {
     pub fn get_spec_body(
         &self,
         def_id: DefId,
-        substs: SubstsRef<'tcx>,
+        substs: GenericArgsRef<'tcx>,
         caller_def_id: DefId,
     ) -> MirBody<'tcx> {
         if let Some(body) = self.get_monomorphised(def_id, substs, Some(caller_def_id)) {