diff --git a/Cargo.lock b/Cargo.lock index 81cec8515e9..beb20cf4bdc 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1891,6 +1891,7 @@ dependencies = [ "dot", "prusti-interface", "prusti-rustc-interface", + "regex", "reqwest", "serde", "serde_derive", diff --git a/mir-state-analysis/src/coupling_graph/impl/engine.rs b/mir-state-analysis/src/coupling_graph/impl/engine.rs index c37e35d3e93..794e908a4af 100644 --- a/mir-state-analysis/src/coupling_graph/impl/engine.rs +++ b/mir-state-analysis/src/coupling_graph/impl/engine.rs @@ -13,12 +13,12 @@ use prusti_rustc_interface::{ borrow_set::{BorrowData, TwoPhaseActivation}, consumers::{Borrows, BorrowIndex, RichLocation, PlaceConflictBias, places_conflict, calculate_borrows_out_of_scope_at_location}, }, - dataflow::{Analysis, AnalysisDomain, CallReturnPlaces, ResultsCursor}, + dataflow::{Analysis, AnalysisDomain, ResultsCursor}, index::{bit_set::{BitSet, HybridBitSet}, Idx}, middle::{ mir::{ TerminatorKind, Operand, ConstantKind, StatementKind, Rvalue, - visit::Visitor, BasicBlock, Body, Local, Place, Location, Statement, Terminator, RETURN_PLACE, + visit::Visitor, BasicBlock, Body, CallReturnPlaces, Local, Place, Location, Statement, Terminator, TerminatorEdges, RETURN_PLACE, }, ty::{RegionVid, TyCtxt}, }, @@ -368,12 +368,12 @@ impl<'a, 'tcx> Analysis<'tcx> for CoupligGraph<'a, 'tcx> { } } - fn apply_terminator_effect( + fn apply_terminator_effect<'mir>( &mut self, state: &mut Self::Domain, - terminator: &Terminator<'tcx>, + terminator: &'mir Terminator<'tcx>, location: Location, - ) { + ) -> TerminatorEdges<'mir, 'tcx> { let l = format!("{:?}", location).replace('[', "_").replace(']', ""); // println!("Location: {l}"); state.regions.graph.id = Some(l.clone()); @@ -434,6 +434,7 @@ impl<'a, 'tcx> Analysis<'tcx> for CoupligGraph<'a, 'tcx> { if cfg!(debug_assertions) && !self.repacker.body().basic_blocks[location.block].is_cleanup { state.regions.output_to_dot(format!("log/coupling/individual/{l}_v{}.dot", state.regions.version)); } + terminator.edges() } fn apply_call_return_effect( diff --git a/mir-state-analysis/src/free_pcs/impl/engine.rs b/mir-state-analysis/src/free_pcs/impl/engine.rs index 05d3a1040fd..9c74c5fa884 100644 --- a/mir-state-analysis/src/free_pcs/impl/engine.rs +++ b/mir-state-analysis/src/free_pcs/impl/engine.rs @@ -5,11 +5,11 @@ // file, You can obtain one at http://mozilla.org/MPL/2.0/. use prusti_rustc_interface::{ - dataflow::{Analysis, AnalysisDomain, CallReturnPlaces}, + dataflow::{Analysis, AnalysisDomain}, index::Idx, middle::{ mir::{ - visit::Visitor, BasicBlock, Body, Local, Location, Statement, Terminator, RETURN_PLACE, + visit::Visitor, BasicBlock, Body, CallReturnPlaces, Local, Location, Statement, Terminator, TerminatorEdges, RETURN_PLACE, }, ty::TyCtxt, }, @@ -74,14 +74,15 @@ impl<'a, 'tcx> Analysis<'tcx> for FreePlaceCapabilitySummary<'a, 'tcx> { state.visit_statement(statement, location); } - fn apply_terminator_effect( + fn apply_terminator_effect<'mir>( &mut self, state: &mut Self::Domain, - terminator: &Terminator<'tcx>, + terminator: &'mir Terminator<'tcx>, location: Location, - ) { + ) -> TerminatorEdges<'mir, 'tcx> { state.repackings.clear(); state.visit_terminator(terminator, location); + terminator.edges() } fn apply_call_return_effect( diff --git a/mir-state-analysis/src/free_pcs/impl/triple.rs b/mir-state-analysis/src/free_pcs/impl/triple.rs index a9d6c19cb2b..4fc1e66d9f1 100644 --- a/mir-state-analysis/src/free_pcs/impl/triple.rs +++ b/mir-state-analysis/src/free_pcs/impl/triple.rs @@ -69,8 +69,8 @@ impl<'tcx> Visitor<'tcx> for Fpcs<'_, 'tcx> { match &terminator.kind { Goto { .. } | SwitchInt { .. } - | Resume - | Terminate + | UnwindResume + | UnwindTerminate(_) | Unreachable | Assert { .. } | GeneratorDrop