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

.github/workflows/test.yml

@@ -295,6 +295,7 @@ jobs:
     strategy:
       matrix:
         shard_index: [0, 1, 2, 3]
+      fail-fast: false
     steps:
       - name: Check out the repo
         uses: actions/checkout@v2
@@ -315,4 +316,4 @@ jobs:
       - name: Build with cargo --release
         run: python x.py build --release --all
       - name: Test Prusti on a collection of crates
-        run: ./target/release/test-crates --fail-fast --num-shards=4 --shard-index=${{ matrix.shard_index }}
+        run: ./target/release/test-crates --num-shards=4 --shard-index=${{ matrix.shard_index }}

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-rustc-interface/src/lib.rs

@@ -8,6 +8,7 @@ extern crate rustc_smir;
 
 pub extern crate polonius_engine as polonius_engine;
 pub extern crate rustc_ast as ast;
+pub extern crate rustc_ast_pretty as ast_pretty;
 pub extern crate rustc_attr as attr;
 pub extern crate rustc_data_structures as data_structures;
 pub extern crate rustc_driver as driver;

prusti-tests/tests/parse/ui/predicates-visibility.stdout

@@ -35,9 +35,8 @@ mod foo {
     #[prusti::pred_spec_id_ref = "$(NUM_UUID)"]
     #[prusti::specs_version = $(SPECS_VERSION)]
     pub fn pred1(a: bool) -> bool {
-        ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "],
-                &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"],
-                                        &[]))]))
+        ::core::panicking::panic_fmt(format_args!("not implemented: {0}",
+                format_args!("predicate")))
     }
 }
 #[allow(unused_must_use, unused_parens, unused_variables, dead_code,

prusti-tests/tests/parse/ui/predicates.stdout

@@ -36,9 +36,8 @@ fn prusti_pred_item_pred1_$(NUM_UUID)(a: bool) -> bool {
 #[prusti::pred_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
 fn pred1(a: bool) -> bool {
-    ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "],
-            &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"],
-                                    &[]))]))
+    ::core::panicking::panic_fmt(format_args!("not implemented: {0}",
+            format_args!("predicate")))
 }
 #[allow(unused_must_use, unused_parens, unused_variables, dead_code,
 non_snake_case)]
@@ -64,9 +63,8 @@ fn prusti_pred_item_pred2_$(NUM_UUID)(a: bool) -> bool {
 #[prusti::pred_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
 fn pred2(a: bool) -> bool {
-    ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "],
-            &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"],
-                                    &[]))]))
+    ::core::panicking::panic_fmt(format_args!("not implemented: {0}",
+            format_args!("predicate")))
 }
 #[allow(unused_must_use, unused_parens, unused_variables, dead_code,
 non_snake_case)]
@@ -94,9 +92,8 @@ fn prusti_pred_item_forall_implication_$(NUM_UUID)()
 #[prusti::pred_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
 fn forall_implication() -> bool {
-    ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "],
-            &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"],
-                                    &[]))]))
+    ::core::panicking::panic_fmt(format_args!("not implemented: {0}",
+            format_args!("predicate")))
 }
 #[allow(unused_must_use, unused_parens, unused_variables, dead_code,
 non_snake_case)]
@@ -114,9 +111,8 @@ fn prusti_pred_item_exists_implication_$(NUM_UUID)()
 #[prusti::pred_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
 fn exists_implication() -> bool {
-    ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "],
-            &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"],
-                                    &[]))]))
+    ::core::panicking::panic_fmt(format_args!("not implemented: {0}",
+            format_args!("predicate")))
 }
 fn main() {}
 ProcedureSpecification { source: DefId(0:7 ~ predicates[$(CRATE_ID)]::pred1), kind: Inherent(Predicate(Some(DefId(0:5 ~ predicates[$(CRATE_ID)]::prusti_pred_item_pred1_$(NUM_UUID))))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(false), terminates: Inherent(None), purity: Inherent(None) }

prusti-tests/tests/parse/ui/unbalanced.stderr

@@ -2,7 +2,9 @@ error: unexpected closing delimiter: `]`
  --> $DIR/unbalanced.rs:3:18
   |
 3 | #[requires(true))]
-  |                  ^ unexpected closing delimiter
+  |                 -^ unexpected closing delimiter
+  |                 |
+  |                 missing open `(` for this delimiter
 
 error: mismatched closing delimiter: `)`
  --> $DIR/unbalanced.rs:3:2