Skip to content

Commit

Permalink
Add results cursor
Browse files Browse the repository at this point in the history
JonasAlaif committed Apr 18, 2023

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
1 parent 0a533ae commit a64df48
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
@@ -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
@@ -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);
}
}
}
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
@@ -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
@@ -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.