Skip to content

Commit

Permalink
Add results cursor
Browse files Browse the repository at this point in the history
  • Loading branch information
JonasAlaif committed Apr 18, 2023
1 parent 0a533ae commit a64df48
Show file tree
Hide file tree
Showing 5 changed files with 152 additions and 24 deletions.
51 changes: 28 additions & 23 deletions mir-state-analysis/src/free_pcs/check/checker.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,36 +6,37 @@

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() {
let loc = Location {
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
Expand All @@ -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
Expand All @@ -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);
}
}
}
Expand Down
113 changes: 113 additions & 0 deletions mir-state-analysis/src/free_pcs/results/cursor.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,113 @@
// © 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)
.successor_within_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<FreePcsLocation<'b, 'tcx>, 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<RepackOp<'tcx>>,
/// State after the statement
pub state: &'a CapabilitySummary<'tcx>,
}

#[derive(Debug)]
pub struct FreePcsTerminator<'a, 'tcx> {
pub succs: Vec<FreePcsLocation<'a, 'tcx>>,
}
2 changes: 2 additions & 0 deletions mir-state-analysis/src/free_pcs/results/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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::*;
Empty file.
10 changes: 9 additions & 1 deletion mir-state-analysis/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}

0 comments on commit a64df48

Please sign in to comment.