Update dependencies (rustc nightly-2023-06-15, viper v-2023-05-17-0733)

Cargo.toml

@@ -25,6 +25,7 @@ members = [
 exclude = [
     "docs/dummy"
 ]
+resolver = "2"
 
 [profile.dev]
 debug = 1

analysis/Cargo.toml

@@ -15,7 +15,7 @@ prusti-rustc-interface = { path = "../prusti-rustc-interface" }
 tracing = { path = "../tracing" }
 
 [dev-dependencies]
-compiletest_rs = "0.9"
+compiletest_rs = "0.10"
 glob = "0.3"
 
 [package.metadata.rust-analyzer]

analysis/src/bin/analysis-driver.rs

@@ -13,14 +13,14 @@ use analysis::{
 };
 use prusti_rustc_interface::{
     ast::ast,
-    borrowck::BodyWithBorrowckFacts,
+    borrowck::consumers::{self, BodyWithBorrowckFacts},
     data_structures::fx::FxHashMap,
     driver::Compilation,
     hir::def_id::{DefId, LocalDefId},
     interface::{interface, Config, Queries},
     middle::{
+        query::{queries::mir_borrowck::ProvidedValue, ExternProviders, Providers},
         ty,
-        ty::query::{query_values::mir_borrowck, ExternProviders, Providers},
     },
     polonius_engine::{Algorithm, Output},
     session::{Attribute, Session},
@@ -116,10 +116,11 @@ mod mir_storage {
 }
 
 #[allow(clippy::needless_lifetimes)]
-fn mir_borrowck<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: LocalDefId) -> mir_borrowck<'tcx> {
-    let body_with_facts = prusti_rustc_interface::borrowck::consumers::get_body_with_borrowck_facts(
+fn mir_borrowck<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: LocalDefId) -> ProvidedValue<'tcx> {
+    let body_with_facts = consumers::get_body_with_borrowck_facts(
         tcx,
-        ty::WithOptConstParam::unknown(def_id),
+        def_id,
+        consumers::ConsumerOptions::PoloniusOutputFacts,
     );
     // SAFETY: This is safe because we are feeding in the same `tcx` that is
     // going to be used as a witness when pulling out the data.
@@ -190,12 +191,17 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
                 // that was used to store the data.
                 let mut body_with_facts =
                     unsafe { self::mir_storage::retrieve_mir_body(tcx, local_def_id) };
-                body_with_facts.output_facts = Rc::new(Output::compute(
-                    &body_with_facts.input_facts,
+                body_with_facts.output_facts = Some(Rc::new(Output::compute(
+                    body_with_facts.input_facts.as_ref().unwrap(),
                     Algorithm::Naive,
                     true,
-                ));
-                assert!(!body_with_facts.input_facts.cfg_edge.is_empty());
+                )));
+                assert!(!body_with_facts
+                    .input_facts
+                    .as_ref()
+                    .unwrap()
+                    .cfg_edge
+                    .is_empty());
                 let body = &body_with_facts.body;
 
                 match abstract_domain {

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

@@ -6,15 +6,15 @@
 
 use analysis::domains::DefinitelyAccessibleAnalysis;
 use prusti_rustc_interface::{
-    borrowck::BodyWithBorrowckFacts,
+    borrowck::consumers::{self, BodyWithBorrowckFacts},
     data_structures::fx::FxHashMap,
     driver::Compilation,
     hir,
     hir::def_id::LocalDefId,
     interface::{interface, Config, Queries},
     middle::{
+        query::{queries::mir_borrowck::ProvidedValue, ExternProviders, Providers},
         ty,
-        ty::query::{query_values::mir_borrowck, ExternProviders, Providers},
     },
     polonius_engine::{Algorithm, Output},
     session::Session,
@@ -69,10 +69,11 @@ mod mir_storage {
 }
 
 #[allow(clippy::needless_lifetimes)]
-fn mir_borrowck<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: LocalDefId) -> mir_borrowck<'tcx> {
-    let body_with_facts = prusti_rustc_interface::borrowck::consumers::get_body_with_borrowck_facts(
+fn mir_borrowck<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: LocalDefId) -> ProvidedValue<'tcx> {
+    let body_with_facts = consumers::get_body_with_borrowck_facts(
         tcx,
-        ty::WithOptConstParam::unknown(def_id),
+        def_id,
+        consumers::ConsumerOptions::PoloniusOutputFacts,
     );
     // SAFETY: This is safe because we are feeding in the same `tcx` that is
     // going to be used as a witness when pulling out the data.
@@ -135,11 +136,11 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
                     // that was used to store the data.
                     let mut body_with_facts =
                         unsafe { self::mir_storage::retrieve_mir_body(tcx, local_def_id) };
-                    body_with_facts.output_facts = Rc::new(Output::compute(
-                        &body_with_facts.input_facts,
+                    body_with_facts.output_facts = Some(Rc::new(Output::compute(
+                        body_with_facts.input_facts.as_ref().unwrap(),
                         Algorithm::Naive,
                         true,
-                    ));
+                    )));
 
                     // Skip macro expansions
                     let mir_span = body_with_facts.body.span;
@@ -175,7 +176,12 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
 
             // Generate and print the programs with the additional statements to check accessibility.
             for (num, (local_def_id, body_with_facts)) in def_ids_with_body.iter().enumerate() {
-                assert!(!body_with_facts.input_facts.cfg_edge.is_empty());
+                assert!(!body_with_facts
+                    .input_facts
+                    .as_ref()
+                    .unwrap()
+                    .cfg_edge
+                    .is_empty());
                 let body = &body_with_facts.body;
 
                 if num > 0 {

analysis/src/domains/definitely_accessible/analysis.rs

@@ -14,7 +14,7 @@ use crate::{
     PointwiseState,
 };
 use prusti_rustc_interface::{
-    borrowck::BodyWithBorrowckFacts,
+    borrowck::consumers::BodyWithBorrowckFacts,
     data_structures::fx::{FxHashMap, FxHashSet},
     middle::{mir, ty::TyCtxt},
     span::def_id::DefId,
@@ -48,8 +48,8 @@ impl<'mir, 'tcx: 'mir> DefinitelyAccessibleAnalysis<'mir, 'tcx> {
         let borrowed_analysis = MaybeBorrowedAnalysis::new(self.tcx, self.body_with_facts);
         let def_init = def_init_analysis.run_fwd_analysis()?;
         let borrowed = borrowed_analysis.run_analysis()?;
-        let location_table = &self.body_with_facts.location_table;
-        let borrowck_out_facts = self.body_with_facts.output_facts.as_ref();
+        let location_table = self.body_with_facts.location_table.as_ref().unwrap();
+        let borrowck_out_facts = self.body_with_facts.output_facts.as_ref().unwrap().as_ref();
         let var_live_on_entry: FxHashMap<_, _> = borrowck_out_facts
             .var_live_on_entry
             .iter()

analysis/src/domains/definitely_initialized/state.rs

@@ -261,11 +261,12 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {
                 place,
                 target,
                 unwind,
+                ..
             } => {
                 new_state.set_place_uninitialised(place);
                 res_vec.push((target, new_state));
 
-                if let Some(bb) = unwind {
+                if let mir::UnwindAction::Cleanup(bb) = unwind {
                     // imprecision for error states
                     res_vec.push((bb, Self::new_top(self.def_id, self.mir, self.tcx)));
                 }
@@ -275,7 +276,7 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {
                 ref args,
                 destination,
                 target,
-                cleanup,
+                unwind,
                 ..
             } => {
                 for arg in args.iter() {
@@ -287,21 +288,21 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {
                     res_vec.push((bb, new_state));
                 }
 
-                if let Some(bb) = cleanup {
+                if let mir::UnwindAction::Cleanup(bb) = unwind {
                     // imprecision for error states
                     res_vec.push((bb, Self::new_top(self.def_id, self.mir, self.tcx)));
                 }
             }
             mir::TerminatorKind::Assert {
                 ref cond,
                 target,
-                cleanup,
+                unwind,
                 ..
             } => {
                 new_state.apply_operand_effect(cond, move_out_copy_types);
                 res_vec.push((target, new_state));
 
-                if let Some(bb) = cleanup {
+                if let mir::UnwindAction::Cleanup(bb) = unwind {
                     // imprecision for error states
                     res_vec.push((bb, Self::new_top(self.def_id, self.mir, self.tcx)));
                 }

analysis/src/domains/framing/analysis.rs

@@ -11,7 +11,7 @@ use crate::{
     PointwiseState,
 };
 use prusti_rustc_interface::{
-    borrowck::BodyWithBorrowckFacts,
+    borrowck::consumers::BodyWithBorrowckFacts,
     middle::{
         mir,
         mir::visit::{NonMutatingUseContext, PlaceContext, Visitor},
@@ -105,7 +105,6 @@ impl<'mir, 'tcx: 'mir> Visitor<'tcx> for ComputeFramingState<'mir, 'tcx> {
     ) {
         let place = (*place).into();
         match context {
-            PlaceContext::NonMutatingUse(NonMutatingUseContext::UniqueBorrow) => todo!(),
             PlaceContext::MutatingUse(_)
             | PlaceContext::NonMutatingUse(NonMutatingUseContext::Move) => {
                 // No permission can be framed

analysis/src/domains/maybe_borrowed/analysis.rs

@@ -10,7 +10,7 @@ use crate::{
 };
 use log::{error, trace};
 use prusti_rustc_interface::{
-    borrowck::{consumers::RichLocation, BodyWithBorrowckFacts},
+    borrowck::consumers::{BodyWithBorrowckFacts, RichLocation},
     data_structures::fx::FxHashMap,
     middle::{mir, ty::TyCtxt},
 };
@@ -33,9 +33,9 @@ impl<'mir, 'tcx: 'mir> MaybeBorrowedAnalysis<'mir, 'tcx> {
         &self,
     ) -> AnalysisResult<PointwiseState<'mir, 'tcx, MaybeBorrowedState<'tcx>>> {
         let body = &self.body_with_facts.body;
-        let location_table = &self.body_with_facts.location_table;
-        let borrowck_in_facts = &self.body_with_facts.input_facts;
-        let borrowck_out_facts = self.body_with_facts.output_facts.as_ref();
+        let location_table = self.body_with_facts.location_table.as_ref().unwrap();
+        let borrowck_in_facts = self.body_with_facts.input_facts.as_ref().unwrap();
+        let borrowck_out_facts = self.body_with_facts.output_facts.as_ref().unwrap().as_ref();
         let loan_issued_at = &borrowck_in_facts.loan_issued_at;
         let loan_live_at = &borrowck_out_facts.loan_live_at;
         let loan_issued_at_location: FxHashMap<_, mir::Location> = loan_issued_at

analysis/src/domains/reaching_definitions/state.rs

@@ -128,7 +128,7 @@ impl<'mir, 'tcx: 'mir> ReachingDefsState<'mir, 'tcx> {
             mir::TerminatorKind::Call {
                 ref destination,
                 target,
-                cleanup,
+                unwind,
                 ..
             } => {
                 if let Some(bb) = target {
@@ -144,7 +144,7 @@ impl<'mir, 'tcx: 'mir> ReachingDefsState<'mir, 'tcx> {
                     res_vec.push((bb, dest_state));
                 }
 
-                if let Some(bb) = cleanup {
+                if let mir::UnwindAction::Cleanup(bb) = unwind {
                     let mut cleanup_state = self.clone();
                     // error state -> be conservative & add destination as possible reaching def
                     // while keeping all others

analysis/tests/test_cases/definitely_accessible/expired.stdout

@@ -438,7 +438,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> bb6",
+    "terminator: drop(_1) -> [return: bb6, unwind terminate]",
     {
       "bb6": [
         "state:",

analysis/tests/test_cases/definitely_accessible/fields.rs

@@ -1,3 +1,5 @@
+#![allow(dropping_references)]
+
 #[derive(Clone, Default)]
 struct T {
     // Wrap in Box to have non-Copy types

analysis/tests/test_cases/definitely_accessible/fields.stdout

@@ -685,7 +685,7 @@ Result for function main():
         "(_1.0: std::boxed::Box<u32>)"
       ]
     },
-    "terminator: drop(_11) -> bb13",
+    "terminator: drop(_11) -> [return: bb13, unwind terminate]",
     {
       "bb13": [
         "state:",
@@ -918,7 +918,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_13) -> bb13",
+    "terminator: drop(_13) -> [return: bb13, unwind terminate]",
     {
       "bb13": [
         "state:",
@@ -936,7 +936,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_3) -> bb13",
+    "terminator: drop(_3) -> [return: bb13, unwind terminate]",
     {
       "bb13": [
         "state:",
@@ -954,7 +954,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> bb14",
+    "terminator: drop(_1) -> [return: bb14, unwind terminate]",
     {
       "bb14": [
         "state:",

analysis/tests/test_cases/definitely_accessible/infinite_list.stdout

@@ -164,7 +164,7 @@ Result for function test1():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> bb4",
+    "terminator: drop(_1) -> [return: bb4, unwind terminate]",
     {
       "bb4": [
         "state:",
@@ -316,7 +316,7 @@ Result for function test2():
         "_1"
       ]
     },
-    "terminator: drop(_2) -> bb5",
+    "terminator: drop(_2) -> [return: bb5, unwind terminate]",
     {
       "bb5": [
         "state:",
@@ -412,7 +412,7 @@ Result for function test2():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> bb6",
+    "terminator: drop(_1) -> [return: bb6, unwind terminate]",
     {
       "bb6": [
         "state:",

analysis/tests/test_cases/definitely_accessible/ref_field.stdout

@@ -939,7 +939,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_16) -> bb10",
+    "terminator: drop(_16) -> [return: bb10, unwind terminate]",
     {
       "bb10": [
         "state:",
@@ -957,7 +957,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> bb12",
+    "terminator: drop(_1) -> [return: bb12, unwind terminate]",
     {
       "bb12": [
         "state:",
@@ -975,7 +975,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_2) -> bb12",
+    "terminator: drop(_2) -> [return: bb12, unwind terminate]",
     {
       "bb12": [
         "state:",

analysis/tests/test_cases/definitely_initialized/array.rs

@@ -1,3 +1,5 @@
+#![allow(dropping_copy_types)]
+
 #[analyzer::run]
 fn main() {
     let x = [1, 2, 3];

analysis/tests/test_cases/definitely_initialized/array.stdout

@@ -284,7 +284,7 @@ Result for function main():
     [],
     "state before terminator:",
     [],
-    "terminator: drop(_7) -> bb7",
+    "terminator: drop(_7) -> [return: bb7, unwind terminate]",
     {
       "bb7": [
         "state:",
@@ -296,7 +296,7 @@ Result for function main():
     [],
     "state before terminator:",
     [],
-    "terminator: drop(_4) -> bb8",
+    "terminator: drop(_4) -> [return: bb8, unwind terminate]",
     {
       "bb8": [
         "state:",

analysis/tests/test_cases/definitely_initialized/fields.rs

@@ -1,3 +1,5 @@
+#![allow(dropping_references)]
+
 #[derive(Clone, Default)]
 struct T {
     // Wrap in box to have non-Copy types