Update dependencies (rustc nightly-2023-09-01, viper v-2023-08-26-212…

…5) (#1451) Co-authored-by: fpoli <fpoli@users.noreply.github.com> Co-authored-by: Jonáš Fiala <jonas.fiala@inf.ethz.ch>
viperproject · Sep 6, 2023 · 2258146 · 2258146
1 parent cfefd8d
commit 2258146
Show file tree

Hide file tree

Showing 25 changed files with 194 additions and 219 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/analysis/tests/test_cases/definitely_accessible/expired.stdout b/analysis/tests/test_cases/definitely_accessible/expired.stdout
@@ -438,7 +438,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> [return: bb6, unwind terminate]",
+    "terminator: drop(_1) -> [return: bb6, unwind terminate(cleanup)]",
     {
       "bb6": [
         "state:",

diff --git a/analysis/tests/test_cases/definitely_accessible/fields.stdout b/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) -> [return: bb13, unwind terminate]",
+    "terminator: drop(_11) -> [return: bb13, unwind terminate(cleanup)]",
     {
       "bb13": [
         "state:",
@@ -918,7 +918,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_13) -> [return: bb13, unwind terminate]",
+    "terminator: drop(_13) -> [return: bb13, unwind terminate(cleanup)]",
     {
       "bb13": [
         "state:",
@@ -936,7 +936,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_3) -> [return: bb13, unwind terminate]",
+    "terminator: drop(_3) -> [return: bb13, unwind terminate(cleanup)]",
     {
       "bb13": [
         "state:",
@@ -954,7 +954,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> [return: bb14, unwind terminate]",
+    "terminator: drop(_1) -> [return: bb14, unwind terminate(cleanup)]",
     {
       "bb14": [
         "state:",

diff --git a/analysis/tests/test_cases/definitely_accessible/infinite_list.stdout b/analysis/tests/test_cases/definitely_accessible/infinite_list.stdout
@@ -164,7 +164,7 @@ Result for function test1():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> [return: bb4, unwind terminate]",
+    "terminator: drop(_1) -> [return: bb4, unwind terminate(cleanup)]",
     {
       "bb4": [
         "state:",
@@ -316,7 +316,7 @@ Result for function test2():
         "_1"
       ]
     },
-    "terminator: drop(_2) -> [return: bb5, unwind terminate]",
+    "terminator: drop(_2) -> [return: bb5, unwind terminate(cleanup)]",
     {
       "bb5": [
         "state:",
@@ -412,7 +412,7 @@ Result for function test2():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> [return: bb6, unwind terminate]",
+    "terminator: drop(_1) -> [return: bb6, unwind terminate(cleanup)]",
     {
       "bb6": [
         "state:",

diff --git a/analysis/tests/test_cases/definitely_accessible/ref_field.stdout b/analysis/tests/test_cases/definitely_accessible/ref_field.stdout
@@ -939,7 +939,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_16) -> [return: bb10, unwind terminate]",
+    "terminator: drop(_16) -> [return: bb10, unwind terminate(cleanup)]",
     {
       "bb10": [
         "state:",
@@ -957,7 +957,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> [return: bb12, unwind terminate]",
+    "terminator: drop(_1) -> [return: bb12, unwind terminate(cleanup)]",
     {
       "bb12": [
         "state:",
@@ -975,7 +975,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_2) -> [return: bb12, unwind terminate]",
+    "terminator: drop(_2) -> [return: bb12, unwind terminate(cleanup)]",
     {
       "bb12": [
         "state:",

diff --git a/analysis/tests/test_cases/definitely_initialized/array.stdout b/analysis/tests/test_cases/definitely_initialized/array.stdout
@@ -284,7 +284,7 @@ Result for function main():
     [],
     "state before terminator:",
     [],
-    "terminator: drop(_7) -> [return: bb7, unwind terminate]",
+    "terminator: drop(_7) -> [return: bb7, unwind terminate(cleanup)]",
     {
       "bb7": [
         "state:",
@@ -296,7 +296,7 @@ Result for function main():
     [],
     "state before terminator:",
     [],
-    "terminator: drop(_4) -> [return: bb8, unwind terminate]",
+    "terminator: drop(_4) -> [return: bb8, unwind terminate(cleanup)]",
     {
       "bb8": [
         "state:",

diff --git a/analysis/tests/test_cases/definitely_initialized/fields.stdout b/analysis/tests/test_cases/definitely_initialized/fields.stdout
@@ -478,7 +478,7 @@ Result for function main():
     [
       "(_1.0: std::boxed::Box<u32>)"
     ],
-    "terminator: drop(_11) -> [return: bb13, unwind terminate]",
+    "terminator: drop(_11) -> [return: bb13, unwind terminate(cleanup)]",
     {
       "bb13": [
         "state:",
@@ -653,7 +653,7 @@ Result for function main():
     [],
     "state before terminator:",
     [],
-    "terminator: drop(_13) -> [return: bb13, unwind terminate]",
+    "terminator: drop(_13) -> [return: bb13, unwind terminate(cleanup)]",
     {
       "bb13": [
         "state:",
@@ -665,7 +665,7 @@ Result for function main():
     [],
     "state before terminator:",
     [],
-    "terminator: drop(_3) -> [return: bb13, unwind terminate]",
+    "terminator: drop(_3) -> [return: bb13, unwind terminate(cleanup)]",
     {
       "bb13": [
         "state:",
@@ -677,7 +677,7 @@ Result for function main():
     [],
     "state before terminator:",
     [],
-    "terminator: drop(_1) -> [return: bb14, unwind terminate]",
+    "terminator: drop(_1) -> [return: bb14, unwind terminate(cleanup)]",
     {
       "bb14": [
         "state:",

diff --git a/analysis/tests/test_cases/framing/ref_field.stdout b/analysis/tests/test_cases/framing/ref_field.stdout
@@ -529,7 +529,7 @@ Result for function main():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_9) -> [return: bb10, unwind terminate]",
+    "terminator: drop(_9) -> [return: bb10, unwind terminate(cleanup)]",
     {
       "bb10": [
         "state:",
@@ -547,7 +547,7 @@ Result for function main():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_1) -> [return: bb12, unwind terminate]",
+    "terminator: drop(_1) -> [return: bb12, unwind terminate(cleanup)]",
     {
       "bb12": [
         "state:",
@@ -565,7 +565,7 @@ Result for function main():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_2) -> [return: bb12, unwind terminate]",
+    "terminator: drop(_2) -> [return: bb12, unwind terminate(cleanup)]",
     {
       "bb12": [
         "state:",

diff --git a/analysis/tests/test_cases/framing/rust_issue_63787.stdout b/analysis/tests/test_cases/framing/rust_issue_63787.stdout
@@ -350,7 +350,7 @@ Result for function break_it():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_7) -> [return: bb8, unwind terminate]",
+    "terminator: drop(_7) -> [return: bb8, unwind terminate(cleanup)]",
     {
       "bb8": [
         "state:",
@@ -368,7 +368,7 @@ Result for function break_it():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_4) -> [return: bb8, unwind terminate]",
+    "terminator: drop(_4) -> [return: bb8, unwind terminate(cleanup)]",
     {
       "bb8": [
         "state:",
@@ -386,7 +386,7 @@ Result for function break_it():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_2) -> [return: bb9, unwind terminate]",
+    "terminator: drop(_2) -> [return: bb9, unwind terminate(cleanup)]",
     {
       "bb9": [
         "state:",
@@ -688,7 +688,7 @@ Result for function main():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_4) -> [return: bb5, unwind terminate]",
+    "terminator: drop(_4) -> [return: bb5, unwind terminate(cleanup)]",
     {
       "bb5": [
         "state:",

diff --git a/analysis/tests/test_cases/maybe_borrowed/linked_list.stdout b/analysis/tests/test_cases/maybe_borrowed/linked_list.stdout
@@ -162,7 +162,7 @@ Result for function borrow_fields():
       "frozen": [],
       "blocked": []
     },
-    "terminator: drop(_1) -> [return: bb4, unwind terminate]",
+    "terminator: drop(_1) -> [return: bb4, unwind terminate(cleanup)]",
     {
       "bb4": [
         "state:",

diff --git a/prusti-interface/src/environment/mir_body/graphviz.rs b/prusti-interface/src/environment/mir_body/graphviz.rs
@@ -173,10 +173,10 @@ fn visit_terminator(graph: &mut Graph, bb: mir::BasicBlock, terminator: &mir::Te
                 graph.add_regular_edge(bb.to_text(), target.to_text());
             }
         }
-        TerminatorKind::Resume => {
+        TerminatorKind::UnwindResume => {
             graph.add_exit_edge(bb.to_text(), "resume".to_text());
         }
-        TerminatorKind::Terminate => {
+        TerminatorKind::UnwindTerminate(..) => {
             graph.add_exit_edge(bb.to_text(), "terminate".to_text());
         }
         TerminatorKind::Return => {

diff --git a/prusti-interface/src/environment/mir_body/patch/compiler.rs b/prusti-interface/src/environment/mir_body/patch/compiler.rs
@@ -50,7 +50,7 @@ impl<'tcx> MirPatch<'tcx> {
 
         for (bb, block) in body.basic_blocks.iter_enumerated() {
             // Check if we already have a resume block
-            if let TerminatorKind::Resume = block.terminator().kind && block.statements.is_empty() {
+            if let TerminatorKind::UnwindResume = block.terminator().kind && block.statements.is_empty() {
                 result.resume_block = Some(bb);
                 continue;
             }
@@ -65,7 +65,7 @@ impl<'tcx> MirPatch<'tcx> {
             }
 
             // Check if we already have a terminate block
-            if let TerminatorKind::Terminate = block.terminator().kind && block.statements.is_empty() {
+            if let TerminatorKind::UnwindTerminate(..) = block.terminator().kind && block.statements.is_empty() {
                 result.terminate_block = Some(bb);
                 continue;
             }
@@ -83,7 +83,7 @@ impl<'tcx> MirPatch<'tcx> {
             statements: vec![],
             terminator: Some(Terminator {
                 source_info: SourceInfo::outermost(self.body_span),
-                kind: TerminatorKind::Resume,
+                kind: TerminatorKind::UnwindResume,
             }),
             is_cleanup: true,
         });
@@ -108,7 +108,7 @@ impl<'tcx> MirPatch<'tcx> {
         bb
     }
 
-    pub fn terminate_block(&mut self) -> BasicBlock {
+    pub fn terminate_block(&mut self, reason: UnwindTerminateReason) -> BasicBlock {
         if let Some(bb) = self.terminate_block {
             return bb;
         }
@@ -117,7 +117,7 @@ impl<'tcx> MirPatch<'tcx> {
             statements: vec![],
             terminator: Some(Terminator {
                 source_info: SourceInfo::outermost(self.body_span),
-                kind: TerminatorKind::Terminate,
+                kind: TerminatorKind::UnwindTerminate(reason),
             }),
             is_cleanup: true,
         });

diff --git a/prusti-interface/src/environment/mir_utils/real_edges.rs b/prusti-interface/src/environment/mir_utils/real_edges.rs
@@ -52,8 +52,8 @@ fn real_targets(terminator: &mir::Terminator) -> Vec<mir::BasicBlock> {
 
         TerminatorKind::SwitchInt { ref targets, .. } => targets.all_targets().to_vec(),
 
-        TerminatorKind::Resume
-        | TerminatorKind::Terminate
+        TerminatorKind::UnwindResume
+        | TerminatorKind::UnwindTerminate(..)
         | TerminatorKind::Return
         | TerminatorKind::GeneratorDrop
         | TerminatorKind::Unreachable => vec![],

diff --git a/prusti-utils/Cargo.toml b/prusti-utils/Cargo.toml
@@ -19,7 +19,7 @@ walkdir = "2.0"
 toml = "0.7"
 
 [target.'cfg(unix)'.dependencies]
-nix = "0.26"
+nix = "0.27"
 ctrlc = "3.1"
 
 [target.'cfg(windows)'.dependencies]

diff --git a/prusti-viper/src/encoder/foldunfold/mod.rs b/prusti-viper/src/encoder/foldunfold/mod.rs
@@ -590,7 +590,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> vir::CfgReplacer<PathCtxt<'p>, ActionVec> for FoldUnf
         {
             let all_perms = stmt.get_required_permissions(pctxt.predicates());
             let pred_permissions: Vec<_> =
-                all_perms.iter().cloned().filter(|p| p.is_pred()).collect();
+                all_perms.iter().filter(|p| p.is_pred()).cloned().collect();
 
             let acc_permissions: Vec<_> = all_perms
                 .into_iter()

diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs
@@ -47,7 +47,7 @@ impl UnwindPublic for Unwind {
     fn into_action(self) -> UnwindAction {
         match self {
             Unwind::To(bb) => UnwindAction::Cleanup(bb),
-            Unwind::InCleanup => UnwindAction::Terminate,
+            Unwind::InCleanup => UnwindAction::Terminate(UnwindTerminateReason::InCleanup),
         }
     }
 

diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs
@@ -454,8 +454,13 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> {
                                     UnwindAction::Unreachable => {
                                         Unwind::To(self.patch.unreachable_cleanup_block())
                                     }
-                                    UnwindAction::Terminate => {
-                                        Unwind::To(self.patch.terminate_block())
+                                    UnwindAction::Terminate(reason) => {
+                                        debug_assert_ne!(
+                                            reason,
+                                            UnwindTerminateReason::InCleanup,
+                                            "we are not in a cleanup block, InCleanup reason should be impossible"
+                                        );
+                                        Unwind::To(self.patch.terminate_block(reason))
                                     }
                                 }
                             };
@@ -572,7 +577,7 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> {
                             // drop elaboration should handle that by itself
                             continue;
                         }
-                        TerminatorKind::Resume => {
+                        TerminatorKind::UnwindResume => {
                             // It is possible for `Resume` to be patched
                             // (in particular it can be patched to be replaced with
                             // a Goto; see `MirPatch::new`).
@@ -601,7 +606,8 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> {
             if let TerminatorKind::Call {
                 destination,
                 target: Some(_),
-                unwind: UnwindAction::Continue | UnwindAction::Unreachable | UnwindAction::Terminate,
+                unwind:
+                    UnwindAction::Continue | UnwindAction::Unreachable | UnwindAction::Terminate(..),
                 ..
             } = data.terminator().kind
             {

diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/lifetimes.rs b/prusti-viper/src/encoder/mir/procedures/encoder/lifetimes.rs
@@ -1063,13 +1063,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> LifetimesEncoder<'tcx> for ProcedureEncoder<'p, 'v, '
         for component in identical_lifetimes {
             let existing_component_lifetims: BTreeSet<String> = component
                 .iter()
-                .cloned()
                 .filter(|lft| existing_lifetimes.contains(&lft[..]))
+                .cloned()
                 .collect();
             let non_existing_component_lifetimes: BTreeSet<String> = component
                 .iter()
-                .cloned()
                 .filter(|lft| !existing_lifetimes.contains(&lft[..]))
+                .cloned()
                 .collect();
             for lifetime in non_existing_component_lifetimes {
                 let identical_existing_lifetime = existing_component_lifetims.iter().next();

diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs b/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs
@@ -1195,7 +1195,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     switch_ty,
                 )?
             }
-            TerminatorKind::Resume => SuccessorBuilder::exit_resume_panic(),
+            TerminatorKind::UnwindResume => SuccessorBuilder::exit_resume_panic(),
             // TerminatorKind::Abort => {
             //     graph.add_exit_edge(bb, "abort");
             // }

diff --git a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs
@@ -897,7 +897,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx>
                 )
             }
 
-            TerminatorKind::Terminate | TerminatorKind::Resume { .. } => {
+            TerminatorKind::UnwindTerminate(..) | TerminatorKind::UnwindResume { .. } => {
                 assert!(states.is_empty());
                 let pos = self
                     .encoder

diff --git a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs
@@ -267,7 +267,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx>
                 )
             }
 
-            TerminatorKind::Terminate | TerminatorKind::Resume { .. } => {
+            TerminatorKind::UnwindTerminate(..) | TerminatorKind::UnwindResume { .. } => {
                 assert!(states.is_empty());
                 let pos = self.encoder.error_manager().register_error(
                     term.source_info.span,