diff --git a/mir-state-analysis/src/free_pcs/check/checker.rs b/mir-state-analysis/src/free_pcs/check/checker.rs index 7e6e4cfa485..3fe8bd1d03e 100644 --- a/mir-state-analysis/src/free_pcs/check/checker.rs +++ b/mir-state-analysis/src/free_pcs/check/checker.rs @@ -6,25 +6,26 @@ use prusti_rustc_interface::{ data_structures::fx::FxHashMap, - dataflow::Results, middle::mir::{visit::Visitor, Location}, }; use crate::{ - engine::FreePlaceCapabilitySummary, join_semi_lattice::RepackingJoinSemiLattice, - utils::PlaceRepacker, CapabilityKind, CapabilityLocal, CapabilitySummary, PlaceOrdering, - RepackOp, + utils::PlaceRepacker, CapabilityKind, CapabilityLocal, CapabilitySummary, Fpcs, + FreePcsAnalysis, PlaceOrdering, RepackOp, }; use super::consistency::CapabilityConistency; -pub(crate) fn check<'tcx>(results: Results<'tcx, FreePlaceCapabilitySummary<'_, 'tcx>>) { - let rp = results.analysis.0; +pub(crate) fn check(mut results: FreePcsAnalysis<'_, '_>) { + let rp = results.repacker(); let body = rp.body(); - let mut cursor = results.into_results_cursor(body); for (block, data) in body.basic_blocks.iter_enumerated() { - cursor.seek_to_block_start(block); - let mut fpcs = cursor.get().clone(); + let mut cursor = results.analysis_for_bb(block); + let mut fpcs = Fpcs { + summary: cursor.initial_state().clone(), + repackings: Vec::new(), + repacker: rp, + }; // Consistency fpcs.summary.consistency_check(rp); for (statement_index, stmt) in data.statements.iter().enumerate() { @@ -32,10 +33,10 @@ pub(crate) fn check<'tcx>(results: Results<'tcx, FreePlaceCapabilitySummary<'_, block, statement_index, }; - cursor.seek_after_primary_effect(loc); - let fpcs_after = cursor.get(); + let fpcs_after = cursor.next().unwrap(); + assert_eq!(fpcs_after.location, loc); // Repacks - for op in &fpcs_after.repackings { + for op in fpcs_after.repacks { op.update_free(&mut fpcs.summary, false, rp); } // Consistency @@ -51,10 +52,10 @@ pub(crate) fn check<'tcx>(results: Results<'tcx, FreePlaceCapabilitySummary<'_, block, statement_index: data.statements.len(), }; - cursor.seek_after_primary_effect(loc); - let fpcs_after = cursor.get(); + let fpcs_after = cursor.next().unwrap(); + assert_eq!(fpcs_after.location, loc); // Repacks - for op in &fpcs_after.repackings { + for op in fpcs_after.repacks { op.update_free(&mut fpcs.summary, false, rp); } // Consistency @@ -65,19 +66,23 @@ pub(crate) fn check<'tcx>(results: Results<'tcx, FreePlaceCapabilitySummary<'_, assert!(fpcs.repackings.is_empty()); // Consistency fpcs.summary.consistency_check(rp); - assert_eq!(&fpcs, fpcs_after); + assert_eq!(&fpcs.summary, fpcs_after.state); - for succ in data.terminator().successors() { - // Get repacks - let to = cursor.results().entry_set_for_block(succ); - let repacks = fpcs.summary.bridge(&to.summary, rp); + let Err(fpcs_end) = cursor.next() else { + panic!("Expected error at the end of the block"); + }; + for succ in fpcs_end.succs { // Repacks let mut from = fpcs.clone(); - for op in repacks { - op.update_free(&mut from.summary, body.basic_blocks[succ].is_cleanup, rp); + for op in succ.repacks { + op.update_free( + &mut from.summary, + body.basic_blocks[succ.location.block].is_cleanup, + rp, + ); } - assert_eq!(&from, to); + assert_eq!(&from.summary, succ.state); } } } diff --git a/mir-state-analysis/src/free_pcs/results/cursor.rs b/mir-state-analysis/src/free_pcs/results/cursor.rs new file mode 100644 index 00000000000..2258f739b62 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/results/cursor.rs @@ -0,0 +1,107 @@ +// © 2023, ETH Zurich +// +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. + +use prusti_rustc_interface::{ + dataflow::ResultsCursor, + middle::mir::{BasicBlock, Body, Location}, +}; + +use crate::{ + engine::FreePlaceCapabilitySummary, join_semi_lattice::RepackingJoinSemiLattice, + utils::PlaceRepacker, CapabilitySummary, RepackOp, +}; + +type Cursor<'mir, 'tcx> = ResultsCursor<'mir, 'tcx, FreePlaceCapabilitySummary<'mir, 'tcx>>; + +pub struct FreePcsAnalysis<'mir, 'tcx>(pub(crate) Cursor<'mir, 'tcx>); + +impl<'mir, 'tcx> FreePcsAnalysis<'mir, 'tcx> { + pub fn analysis_for_bb(&mut self, block: BasicBlock) -> FreePcsCursor<'_, 'mir, 'tcx> { + self.0.seek_to_block_start(block); + let end_stmt = self.0.analysis().0.body().terminator_loc(block); + FreePcsCursor { + analysis: self, + curr_stmt: Location { + block, + statement_index: 0, + }, + end_stmt, + } + } + + pub(crate) fn body(&self) -> &'mir Body<'tcx> { + self.0.analysis().0.body() + } + pub(crate) fn repacker(&self) -> PlaceRepacker<'mir, 'tcx> { + self.0.results().analysis.0 + } +} + +pub struct FreePcsCursor<'a, 'mir, 'tcx> { + analysis: &'a mut FreePcsAnalysis<'mir, 'tcx>, + curr_stmt: Location, + end_stmt: Location, +} + +impl<'a, 'mir, 'tcx> FreePcsCursor<'a, 'mir, 'tcx> { + pub fn initial_state(&self) -> &CapabilitySummary<'tcx> { + &self.analysis.0.get().summary + } + pub fn next<'b>( + &'b mut self, + ) -> Result, FreePcsTerminator<'b, 'tcx>> { + let location = self.curr_stmt; + assert!(location <= self.end_stmt); + self.curr_stmt = location.successor_within_block(); + + if location == self.end_stmt { + // TODO: cleanup + let cursor = &self.analysis.0; + let state = cursor.get(); + let rp = self.analysis.repacker(); + let block = &self.analysis.body()[location.block]; + let succs = block + .terminator() + .successors() + .map(|succ| { + // Get repacks + let to = cursor.results().entry_set_for_block(succ); + FreePcsLocation { + location: Location { + block: succ, + statement_index: 0, + }, + state: &to.summary, + repacks: state.summary.bridge(&to.summary, rp), + } + }) + .collect(); + Err(FreePcsTerminator { succs }) + } else { + self.analysis.0.seek_after_primary_effect(location); + let state = self.analysis.0.get(); + Ok(FreePcsLocation { + location, + state: &state.summary, + repacks: state.repackings.clone(), + }) + } + } +} + +#[derive(Debug)] +pub struct FreePcsLocation<'a, 'tcx> { + pub location: Location, + /// Repacks before the statement + pub repacks: Vec>, + /// State after the statement + pub state: &'a CapabilitySummary<'tcx>, +} + +#[derive(Debug)] +pub struct FreePcsTerminator<'a, 'tcx> { + pub succs: Vec>, +} diff --git a/mir-state-analysis/src/free_pcs/results/mod.rs b/mir-state-analysis/src/free_pcs/results/mod.rs index 7d5043c22da..3d949c4f182 100644 --- a/mir-state-analysis/src/free_pcs/results/mod.rs +++ b/mir-state-analysis/src/free_pcs/results/mod.rs @@ -5,5 +5,7 @@ // file, You can obtain one at http://mozilla.org/MPL/2.0/. mod repacks; +mod cursor; +pub use cursor::*; pub use repacks::*; diff --git a/mir-state-analysis/src/free_pcs/results/repacking.rs b/mir-state-analysis/src/free_pcs/results/repacking.rs deleted file mode 100644 index e69de29bb2d..00000000000 diff --git a/mir-state-analysis/src/lib.rs b/mir-state-analysis/src/lib.rs index b03090e6103..62ff756207e 100644 --- a/mir-state-analysis/src/lib.rs +++ b/mir-state-analysis/src/lib.rs @@ -18,11 +18,19 @@ use prusti_rustc_interface::{ middle::{mir::Body, ty::TyCtxt}, }; -pub fn test_free_pcs<'tcx>(mir: &Body<'tcx>, tcx: TyCtxt<'tcx>) { +pub fn run_free_pcs<'mir, 'tcx>( + mir: &'mir Body<'tcx>, + tcx: TyCtxt<'tcx>, +) -> FreePcsAnalysis<'mir, 'tcx> { let fpcs = free_pcs::engine::FreePlaceCapabilitySummary::new(tcx, mir); let analysis = fpcs .into_engine(tcx, mir) .pass_name("free_pcs") .iterate_to_fixpoint(); + FreePcsAnalysis(analysis.into_results_cursor(mir)) +} + +pub fn test_free_pcs<'tcx>(mir: &Body<'tcx>, tcx: TyCtxt<'tcx>) { + let analysis = run_free_pcs(mir, tcx); free_pcs::check(analysis); }