Update dependencies (rustc nightly-2023-02-01, viper v-2023-01-31-0912)

analysis/src/bin/analysis-driver.rs

@@ -161,7 +161,7 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
 
         println!(
             "Analyzing file {} using {}...",
-            compiler.input().source_name().prefer_local(),
+            compiler.session().io.input.source_name().prefer_local(),
             abstract_domain
         );
 

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

@@ -155,7 +155,7 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
                     // Skip functions that are in an external file.
                     let source_file = session.source_map().lookup_source_file(mir_span.data().lo);
                     if let FileName::Real(filename) = &source_file.name {
-                        if session.local_crate_source_file
+                        if session.local_crate_source_file()
                             != filename.local_path().map(PathBuf::from)
                         {
                             return None;

prusti-interface/src/environment/collect_closure_defs_visitor.rs

@@ -39,9 +39,13 @@ impl<'env, 'tcx> Visitor<'tcx> for CollectClosureDefsVisitor<'env, 'tcx> {
     }
 
     fn visit_expr(&mut self, expr: &'tcx hir::Expr<'tcx>) {
-        if let hir::ExprKind::Closure { .. } = expr.kind {
-            if !has_spec_only_attr(self.env.query.get_local_attributes(expr.hir_id)) {
-                let def_id = self.map.local_def_id(expr.hir_id).to_def_id();
+        if let hir::ExprKind::Closure(hir::Closure {
+            def_id: local_def_id,
+            ..
+        }) = expr.kind
+        {
+            let def_id = local_def_id.to_def_id();
+            if !has_spec_only_attr(self.env.query.get_attributes(def_id)) {
                 let item_def_path = self.env.name.get_item_def_path(def_id);
                 trace!("Add {} to result", item_def_path);
                 self.result.push(def_id);

prusti-interface/src/environment/loops.rs

@@ -259,7 +259,7 @@ impl ProcedureLoops {
         let mut back_edges: FxHashSet<(_, _)> = FxHashSet::default();
         for bb in mir.basic_blocks.indices() {
             for successor in real_edges.successors(bb) {
-                if dominators.is_dominated_by(bb, *successor) {
+                if dominators.dominates(*successor, bb) {
                     back_edges.insert((bb, *successor));
                     debug!("Loop head: {:?}", successor);
                 }
@@ -475,7 +475,7 @@ impl ProcedureLoops {
 
     /// Check if ``block`` is inside a given loop.
     pub fn is_block_in_loop(&self, loop_head: BasicBlockIndex, block: BasicBlockIndex) -> bool {
-        self.dominators.is_dominated_by(block, loop_head)
+        self.dominators.dominates(loop_head, block)
     }
 
     /// Compute what paths that are accessed inside the loop.

prusti-interface/src/environment/name.rs

@@ -16,7 +16,7 @@ impl<'tcx> EnvName<'tcx> {
 
     /// Returns the path of the source that is being compiled
     pub fn source_path(self) -> PathBuf {
-        self.tcx.sess.local_crate_source_file.clone().unwrap()
+        self.tcx.sess.local_crate_source_file().unwrap()
     }
 
     /// Returns the file name of the source that is being compiled

prusti-interface/src/environment/procedure.rs

@@ -236,7 +236,7 @@ pub fn is_marked_specification_block(env_query: EnvQuery, bb_data: &BasicBlockDa
             Rvalue::Aggregate(box AggregateKind::Closure(def_id, _), _),
         )) = &stmt.kind
         {
-            if is_spec_closure(env_query, def_id.to_def_id()) {
+            if is_spec_closure(env_query, *def_id) {
                 return true;
             }
         }
@@ -257,13 +257,13 @@ pub fn get_loop_invariant<'tcx>(
             Rvalue::Aggregate(box AggregateKind::Closure(def_id, substs), _),
         )) = &stmt.kind
         {
-            if is_spec_closure(env_query, def_id.to_def_id())
+            if is_spec_closure(env_query, *def_id)
                 && crate::utils::has_prusti_attr(
-                    env_query.get_attributes(def_id.to_def_id()),
+                    env_query.get_attributes(def_id),
                     "loop_body_invariant_spec",
                 )
             {
-                return Some((def_id.to_def_id(), substs));
+                return Some((*def_id, substs));
             }
         }
     }
@@ -293,8 +293,8 @@ fn is_spec_block_kind(env_query: EnvQuery, bb_data: &BasicBlockData, kind: &str)
             Rvalue::Aggregate(box AggregateKind::Closure(def_id, _), _),
         )) = &stmt.kind
         {
-            if is_spec_closure(env_query, def_id.to_def_id())
-                && crate::utils::has_prusti_attr(env_query.get_attributes(def_id.to_def_id()), kind)
+            if is_spec_closure(env_query, *def_id)
+                && crate::utils::has_prusti_attr(env_query.get_attributes(def_id), kind)
             {
                 return true;
             }
@@ -338,7 +338,7 @@ fn blocks_dominated_by(mir: &Body, dominator: BasicBlock) -> FxHashSet<BasicBloc
     let dominators = mir.basic_blocks.dominators();
     let mut blocks = FxHashSet::default();
     for bb in mir.basic_blocks.indices() {
-        if dominators.is_dominated_by(bb, dominator) {
+        if dominators.dominates(dominator, bb) {
             blocks.insert(bb);
         }
     }
@@ -378,7 +378,7 @@ fn build_nonspec_basic_blocks(
 
     for source in mir.basic_blocks.indices() {
         for &target in real_edges.successors(source) {
-            if dominators.is_dominated_by(source, target) {
+            if dominators.dominates(target, source) {
                 loop_heads.insert(target);
             }
         }

prusti-interface/src/environment/query.rs

@@ -140,7 +140,10 @@ impl<'tcx> EnvQuery<'tcx> {
 
     /// Returns true iff `def_id` is an unsafe function.
     pub fn is_unsafe_function(self, def_id: impl IntoParam<ProcedureDefId>) -> bool {
-        self.tcx.fn_sig(def_id.into_param()).unsafety()
+        self.tcx
+            .fn_sig(def_id.into_param())
+            .subst_identity()
+            .unsafety()
             == prusti_rustc_interface::hir::Unsafety::Unsafe
     }
 
@@ -152,11 +155,11 @@ impl<'tcx> EnvQuery<'tcx> {
     ) -> ty::PolyFnSig<'tcx> {
         let def_id = def_id.into_param();
         let sig = if self.tcx.is_closure(def_id) {
-            substs.as_closure().sig()
+            ty::EarlyBinder(substs.as_closure().sig())
         } else {
             self.tcx.fn_sig(def_id)
         };
-        ty::EarlyBinder(sig).subst(self.tcx, substs)
+        sig.subst(self.tcx, substs)
     }
 
     /// Computes the signature of the function with subst applied and associated types resolved.
@@ -531,8 +534,8 @@ mod sealed {
     }
     impl<'tcx> IntoParamTcx<'tcx, LocalDefId> for HirId {
         #[inline(always)]
-        fn into_param(self, tcx: TyCtxt<'tcx>) -> LocalDefId {
-            tcx.hir().local_def_id(self)
+        fn into_param(self, _tcx: TyCtxt<'tcx>) -> LocalDefId {
+            self.owner.def_id
         }
     }
     impl<'tcx> IntoParamTcx<'tcx, ParamEnv<'tcx>> for DefId {

prusti-interface/src/specs/checker/common.rs

@@ -2,6 +2,7 @@ use crate::{environment::Environment, utils::has_spec_only_attr, PrustiError};
 use prusti_rustc_interface::{
     hir::{
         self as hir,
+        def_id::LocalDefId,
         intravisit::{self, Visitor},
     },
     middle::{hir::map::Map, ty::TyCtxt},
@@ -77,14 +78,15 @@ impl<'tcx, T: NonSpecExprVisitor<'tcx>> Visitor<'tcx> for NonSpecExprVisitorWrap
         fd: &'tcx hir::FnDecl<'tcx>,
         b: hir::BodyId,
         _s: Span,
-        id: hir::HirId,
+        local_id: LocalDefId,
     ) {
         // Stop checking inside `prusti::spec_only` functions
-        let attrs = self.wrapped.tcx().hir().attrs(id);
+        let tcx = self.wrapped.tcx();
+        let attrs = tcx.hir().attrs(tcx.local_def_id_to_hir_id(local_id));
         if has_spec_only_attr(attrs) {
             return;
         }
 
-        intravisit::walk_fn(self, fk, fd, b, id);
+        intravisit::walk_fn(self, fk, fd, b, local_id);
     }
 }

prusti-interface/src/specs/checker/predicate_checks.rs

@@ -8,7 +8,11 @@ use log::debug;
 use prusti_rustc_interface::{
     data_structures::fx::{FxHashMap, FxHashSet},
     errors::MultiSpan,
-    hir::{self as hir, def_id::DefId, intravisit},
+    hir::{
+        self as hir,
+        def_id::{DefId, LocalDefId},
+        intravisit,
+    },
     middle::{hir::map::Map, ty::TyCtxt},
     span::Span,
 };
@@ -106,16 +110,16 @@ impl<'tcx> intravisit::Visitor<'tcx> for CollectPredicatesVisitor<'tcx> {
         fd: &'tcx hir::FnDecl<'tcx>,
         b: hir::BodyId,
         s: Span,
-        id: hir::HirId,
+        local_id: LocalDefId,
     ) {
         // collect this fn's DefId if predicate function
-        let attrs = self.env_query.get_local_attributes(id);
+        let attrs = self.env_query.get_local_attributes(local_id);
         if has_prusti_attr(attrs, "pred_spec_id_ref") {
-            let def_id = self.env_query.as_local_def_id(id).to_def_id();
+            let def_id = local_id.to_def_id();
             self.predicates.insert(def_id, s);
         }
 
-        intravisit::walk_fn(self, fk, fd, b, id);
+        intravisit::walk_fn(self, fk, fd, b, local_id);
     }
 
     fn visit_trait_item(&mut self, ti: &'tcx hir::TraitItem<'tcx>) {

prusti-interface/src/specs/external.rs

@@ -1,7 +1,7 @@
 use prusti_rustc_interface::{
     errors::MultiSpan,
     hir::{
-        def_id::DefId,
+        def_id::{DefId, LocalDefId},
         intravisit::{self, Visitor},
     },
     middle::hir::map::Map,
@@ -130,15 +130,15 @@ impl<'tcx> ExternSpecResolver<'tcx> {
         fn_decl: &'tcx prusti_rustc_interface::hir::FnDecl,
         body_id: prusti_rustc_interface::hir::BodyId,
         span: Span,
-        id: prusti_rustc_interface::hir::hir_id::HirId,
+        local_id: LocalDefId,
         extern_spec_kind: ExternSpecKind,
     ) {
         let mut visitor = ExternSpecVisitor {
             env_query: self.env_query,
             spec_found: None,
         };
-        visitor.visit_fn(fn_kind, fn_decl, body_id, span, id);
-        let current_def_id = self.env_query.as_local_def_id(id).to_def_id();
+        visitor.visit_fn(fn_kind, fn_decl, body_id, span, local_id);
+        let current_def_id = local_id.to_def_id();
         if let Some((target_def_id, substs, span)) = visitor.spec_found {
             let extern_spec_decl =
                 ExternSpecDeclaration::from_method_call(target_def_id, substs, self.env_query);

prusti-interface/src/specs/mod.rs

@@ -411,13 +411,12 @@ impl<'a, 'tcx> intravisit::Visitor<'tcx> for SpecCollector<'a, 'tcx> {
         fn_decl: &'tcx prusti_rustc_interface::hir::FnDecl,
         body_id: prusti_rustc_interface::hir::BodyId,
         span: Span,
-        id: prusti_rustc_interface::hir::hir_id::HirId,
+        local_id: LocalDefId,
     ) {
-        intravisit::walk_fn(self, fn_kind, fn_decl, body_id, id);
+        intravisit::walk_fn(self, fn_kind, fn_decl, body_id, local_id);
 
-        let local_id = self.env.query.as_local_def_id(id);
         let def_id = local_id.to_def_id();
-        let attrs = self.env.query.get_local_attributes(id);
+        let attrs = self.env.query.get_local_attributes(local_id);
 
         // Collect spec functions
         if let Some(raw_spec_id) = read_prusti_attr("spec_id", attrs) {
@@ -497,7 +496,7 @@ impl<'a, 'tcx> intravisit::Visitor<'tcx> for SpecCollector<'a, 'tcx> {
                 let attr = read_prusti_attr("extern_spec", attrs).unwrap_or_default();
                 let kind = prusti_specs::ExternSpecKind::try_from(attr).unwrap();
                 self.extern_resolver
-                    .add_extern_fn(fn_kind, fn_decl, body_id, span, id, kind);
+                    .add_extern_fn(fn_kind, fn_decl, body_id, span, local_id, kind);
             }
 
             // Collect procedure specifications

prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs

@@ -193,7 +193,13 @@ impl<'ce, 'tcx, 'v> CounterexampleTranslator<'ce, 'tcx, 'v> {
         let typ = self
             .encoder
             .get_proc_def_id(pure_fn.name.trim_start_matches("caller_for$").to_string())
-            .map(|fn_proc_id| self.tcx.fn_sig(fn_proc_id).skip_binder().output());
+            .map(|fn_proc_id| {
+                self.tcx
+                    .fn_sig(fn_proc_id)
+                    .subst_identity()
+                    .skip_binder()
+                    .output()
+            });
         let sil_arguments = pure_fn
             .args
             .iter()

prusti-viper/src/encoder/mir/procedures/encoder/loops.rs

@@ -35,7 +35,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> super::ProcedureEncoder<'p, 'v, 'tcx> {
                     ),
                 )) = statement.kind
                 {
-                    let specification = self.encoder.get_loop_specs(cl_def_id.to_def_id()).unwrap();
+                    let specification = self.encoder.get_loop_specs(cl_def_id).unwrap();
                     let (spec, encoding_vec, err_ctxt) = match specification {
                         LoopSpecification::Invariant(inv) => {
                             (inv, &mut encoded_invariant_specs, ErrorCtxt::LoopInvariant)
@@ -65,7 +65,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> super::ProcedureEncoder<'p, 'v, 'tcx> {
             let dominators = self.mir.basic_blocks.dominators();
             predecessors[loop_head]
                 .iter()
-                .filter(|predecessor| dominators.is_dominated_by(**predecessor, loop_head))
+                .filter(|predecessor| dominators.dominates(loop_head, **predecessor))
                 .map(|back_edge| self.encode_basic_block_label(*back_edge))
                 .collect()
         };

prusti-viper/src/encoder/mir/procedures/encoder/mod.rs

@@ -1967,7 +1967,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, cl_substs), _),
             )) = stmt.kind
             {
-                let assertion = match self.encoder.get_prusti_assertion(cl_def_id.to_def_id()) {
+                let assertion = match self.encoder.get_prusti_assertion(cl_def_id) {
                     Some(spec) => spec,
                     None => return Ok(false),
                 };
@@ -2016,7 +2016,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, cl_substs), _),
             )) = stmt.kind
             {
-                let assumption = match self.encoder.get_prusti_assumption(cl_def_id.to_def_id()) {
+                let assumption = match self.encoder.get_prusti_assumption(cl_def_id) {
                     Some(spec) => spec,
                     None => return Ok(false),
                 };
@@ -2063,11 +2063,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, _), _),
             )) = stmt.kind
             {
-                let is_begin = self
-                    .encoder
-                    .get_ghost_begin(cl_def_id.to_def_id())
-                    .is_some();
-                let is_end = self.encoder.get_ghost_end(cl_def_id.to_def_id()).is_some();
+                let is_begin = self.encoder.get_ghost_begin(cl_def_id).is_some();
+                let is_end = self.encoder.get_ghost_end(cl_def_id).is_some();
                 return Ok(is_begin || is_end);
             }
         }

prusti-viper/src/encoder/mir/procedures/encoder/specification_blocks.rs

@@ -49,7 +49,7 @@ impl SpecificationBlocks {
         let dominators = body.basic_blocks.dominators();
         for specification_block in specification_blocks.clone() {
             for bb in body.basic_blocks.indices() {
-                if dominators.is_dominated_by(bb, specification_block) {
+                if dominators.dominates(specification_block, bb) {
                     specification_blocks.insert(bb);
                 }
             }

prusti-viper/src/encoder/mir/pure/specifications/interface.rs

@@ -201,7 +201,7 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod
         // inline invariant body
         let encoded_invariant = inline_closure_high(
             self,
-            inv_def_id.to_def_id(),
+            inv_def_id,
             closure_expression_borrow,
             vec![],
             parent_def_id,
@@ -341,7 +341,7 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod
         // inline invariant body
         let encoded_invariant = inline_closure(
             self,
-            inv_def_id.to_def_id(),
+            inv_def_id,
             inv_cl_expr_encoded.try_into_expr().unwrap(),
             vec![],
             parent_def_id,

prusti-viper/src/encoder/mir/types/const_parameters.rs

@@ -75,7 +75,8 @@ pub(super) fn extract_const_parameters_from_type<'tcx>(
         | ty::TyKind::Placeholder(_)
         | ty::TyKind::Infer(_)
         | ty::TyKind::Generator(..)
-        | ty::TyKind::GeneratorWitness(_) => {
+        | ty::TyKind::GeneratorWitness(_)
+        | ty::TyKind::GeneratorWitnessMIR(..) => {
             return Err(SpannedEncodingError::unsupported(
                 format!(
                     "unsupported type to extract const_parameters: {:?}",

prusti-viper/src/encoder/mir/types/encoder.rs

@@ -266,6 +266,7 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> {
             | ty::TyKind::FnPtr(_)
             | ty::TyKind::Dynamic(..)
             | ty::TyKind::GeneratorWitness(..)
+            | ty::TyKind::GeneratorWitnessMIR(..)
             | ty::TyKind::Never
             | ty::TyKind::Tuple(_)
             | ty::TyKind::Alias(ty::AliasKind::Projection, _)

prusti-viper/src/encoder/mir/types/lifetimes.rs

@@ -86,7 +86,8 @@ pub(super) fn extract_lifetimes_from_type<'tcx>(
         | ty::TyKind::Placeholder(_)
         | ty::TyKind::Infer(_)
         | ty::TyKind::Generator(..)
-        | ty::TyKind::GeneratorWitness(_) => {
+        | ty::TyKind::GeneratorWitness(_)
+        | ty::TyKind::GeneratorWitnessMIR(..) => {
             return Err(SpannedEncodingError::unsupported(
                 format!("unsupported type to extract lifetimes: {:?}", ty.kind()),
                 type_encoder.get_type_definition_span(ty),