-
Notifications
You must be signed in to change notification settings - Fork 109
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Switch to using rustc dataflow engine
1 parent
18a6a0e
commit d26c0fb
Showing
37 changed files
with
1,572 additions
and
2,455 deletions.
There are no files selected for viewing
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,159 @@ | ||
// © 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::{ | ||
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, | ||
}; | ||
|
||
use super::consistency::CapabilityConistency; | ||
|
||
pub(crate) fn check<'tcx>(results: Results<'tcx, FreePlaceCapabilitySummary<'_, 'tcx>>) { | ||
let rp = results.analysis.0; | ||
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(); | ||
// 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(); | ||
// Repacks | ||
for op in &fpcs_after.repackings { | ||
op.update_free(&mut fpcs.summary, false, rp); | ||
} | ||
// Consistency | ||
fpcs.summary.consistency_check(rp); | ||
// Statement | ||
assert!(fpcs.repackings.is_empty()); | ||
fpcs.visit_statement(stmt, loc); | ||
assert!(fpcs.repackings.is_empty()); | ||
// Consistency | ||
fpcs.summary.consistency_check(rp); | ||
} | ||
let loc = Location { | ||
block, | ||
statement_index: data.statements.len(), | ||
}; | ||
cursor.seek_after_primary_effect(loc); | ||
let fpcs_after = cursor.get(); | ||
// Repacks | ||
for op in &fpcs_after.repackings { | ||
op.update_free(&mut fpcs.summary, false, rp); | ||
} | ||
// Consistency | ||
fpcs.summary.consistency_check(rp); | ||
// Statement | ||
assert!(fpcs.repackings.is_empty()); | ||
fpcs.visit_terminator(data.terminator(), loc); | ||
assert!(fpcs.repackings.is_empty()); | ||
// Consistency | ||
fpcs.summary.consistency_check(rp); | ||
assert_eq!(&fpcs, fpcs_after); | ||
|
||
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); | ||
|
||
// Repacks | ||
let mut from = fpcs.clone(); | ||
for op in repacks { | ||
op.update_free(&mut from.summary, body.basic_blocks[succ].is_cleanup, rp); | ||
} | ||
assert_eq!(&from, to); | ||
} | ||
} | ||
} | ||
|
||
impl<'tcx> RepackOp<'tcx> { | ||
#[tracing::instrument(level = "debug", skip(rp))] | ||
fn update_free( | ||
&self, | ||
state: &mut CapabilitySummary<'tcx>, | ||
can_dealloc: bool, | ||
rp: PlaceRepacker<'_, 'tcx>, | ||
) { | ||
match self { | ||
RepackOp::Weaken(place, from, to) => { | ||
assert!(from >= to, "{self:?}"); | ||
let curr_state = state[place.local].get_allocated_mut(); | ||
let old = curr_state.insert(*place, *to); | ||
assert_eq!(old, Some(*from), "{self:?}, {curr_state:?}"); | ||
} | ||
&RepackOp::DeallocForCleanup(local) => { | ||
assert!(can_dealloc); | ||
let curr_state = state[local].get_allocated_mut(); | ||
assert_eq!(curr_state.len(), 1); | ||
assert!( | ||
curr_state.contains_key(&local.into()), | ||
"{self:?}, {curr_state:?}" | ||
); | ||
assert_eq!(curr_state[&local.into()], CapabilityKind::Write); | ||
state[local] = CapabilityLocal::Unallocated; | ||
} | ||
// &RepackOp::DeallocUnknown(local) => { | ||
// assert!(!can_dealloc); | ||
// let curr_state = state[local].get_allocated_mut(); | ||
// assert_eq!(curr_state.len(), 1); | ||
// assert_eq!(curr_state[&local.into()], CapabilityKind::Write); | ||
// state[local] = CapabilityLocal::Unallocated; | ||
// } | ||
RepackOp::Pack(place, guide, kind) => { | ||
assert_eq!( | ||
place.partial_cmp(*guide), | ||
Some(PlaceOrdering::Prefix), | ||
"{self:?}" | ||
); | ||
let curr_state = state[place.local].get_allocated_mut(); | ||
let mut removed = curr_state | ||
.drain() | ||
.filter(|(p, _)| place.related_to(*p)) | ||
.collect::<FxHashMap<_, _>>(); | ||
let (p, others) = place.expand_one_level(*guide, rp); | ||
assert!(others | ||
.into_iter() | ||
.chain(std::iter::once(p)) | ||
.all(|p| removed.remove(&p).unwrap() == *kind)); | ||
assert!(removed.is_empty(), "{self:?}, {removed:?}"); | ||
|
||
let old = curr_state.insert(*place, *kind); | ||
assert_eq!(old, None); | ||
} | ||
RepackOp::Unpack(place, guide, kind) => { | ||
assert_eq!( | ||
place.partial_cmp(*guide), | ||
Some(PlaceOrdering::Prefix), | ||
"{self:?}" | ||
); | ||
let curr_state = state[place.local].get_allocated_mut(); | ||
assert_eq!( | ||
curr_state.remove(place), | ||
Some(*kind), | ||
"{self:?} ({:?})", | ||
&**curr_state | ||
); | ||
|
||
let (p, others) = place.expand_one_level(*guide, rp); | ||
curr_state.insert(p, *kind); | ||
curr_state.extend(others.into_iter().map(|p| (p, *kind))); | ||
} | ||
} | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,45 @@ | ||
// © 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 crate::{utils::PlaceRepacker, CapabilityLocal, CapabilityProjections, Place, Summary}; | ||
|
||
pub trait CapabilityConistency<'tcx> { | ||
fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>); | ||
} | ||
|
||
impl<'tcx, T: CapabilityConistency<'tcx>> CapabilityConistency<'tcx> for Summary<T> { | ||
fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>) { | ||
for p in self.iter() { | ||
p.consistency_check(repacker) | ||
} | ||
} | ||
} | ||
|
||
impl<'tcx> CapabilityConistency<'tcx> for CapabilityLocal<'tcx> { | ||
fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>) { | ||
match self { | ||
CapabilityLocal::Unallocated => {} | ||
CapabilityLocal::Allocated(cp) => cp.consistency_check(repacker), | ||
} | ||
} | ||
} | ||
|
||
impl<'tcx> CapabilityConistency<'tcx> for CapabilityProjections<'tcx> { | ||
fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>) { | ||
// All keys unrelated to each other | ||
let keys = self.keys().copied().collect::<Vec<_>>(); | ||
for (i, p1) in keys.iter().enumerate() { | ||
for p2 in keys[i + 1..].iter() { | ||
assert!(!p1.related_to(*p2), "{p1:?} {p2:?}",); | ||
} | ||
} | ||
// Can always pack up to the root | ||
let root: Place = self.get_local().into(); | ||
let mut keys = self.keys().copied().collect(); | ||
root.collapse(&mut keys, repacker); | ||
assert!(keys.is_empty()); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,96 @@ | ||
// © 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::{Analysis, AnalysisDomain, CallReturnPlaces}, | ||
index::vec::Idx, | ||
middle::{ | ||
mir::{ | ||
visit::Visitor, BasicBlock, Body, Local, Location, Statement, Terminator, RETURN_PLACE, | ||
}, | ||
ty::TyCtxt, | ||
}, | ||
}; | ||
|
||
use crate::{utils::PlaceRepacker, CapabilityKind, CapabilityLocal, Fpcs}; | ||
|
||
pub(crate) struct FreePlaceCapabilitySummary<'a, 'tcx>(pub(crate) PlaceRepacker<'a, 'tcx>); | ||
impl<'a, 'tcx> FreePlaceCapabilitySummary<'a, 'tcx> { | ||
pub(crate) fn new(tcx: TyCtxt<'tcx>, body: &'a Body<'tcx>) -> Self { | ||
let repacker = PlaceRepacker::new(body, tcx); | ||
FreePlaceCapabilitySummary(repacker) | ||
} | ||
} | ||
|
||
impl<'a, 'tcx> AnalysisDomain<'tcx> for FreePlaceCapabilitySummary<'a, 'tcx> { | ||
type Domain = Fpcs<'a, 'tcx>; | ||
const NAME: &'static str = "free_pcs"; | ||
|
||
fn bottom_value(&self, _body: &Body<'tcx>) -> Self::Domain { | ||
Fpcs::new(self.0) | ||
} | ||
|
||
fn initialize_start_block(&self, body: &Body<'tcx>, state: &mut Self::Domain) { | ||
let always_live = self.0.always_live_locals(); | ||
let return_local = RETURN_PLACE; | ||
let last_arg = Local::new(body.arg_count); | ||
for (local, cap) in state.summary.iter_enumerated_mut() { | ||
if local == return_local { | ||
let old = cap | ||
.get_allocated_mut() | ||
.insert(local.into(), CapabilityKind::Write); | ||
assert!(old.is_some()); | ||
} else if local <= last_arg { | ||
let old = cap | ||
.get_allocated_mut() | ||
.insert(local.into(), CapabilityKind::Exclusive); | ||
assert!(old.is_some()); | ||
} else if always_live.contains(local) { | ||
// TODO: figure out if `always_live` should start as `Uninit` or `Exclusive` | ||
let al_cap = if true { | ||
CapabilityKind::Write | ||
} else { | ||
CapabilityKind::Exclusive | ||
}; | ||
let old = cap.get_allocated_mut().insert(local.into(), al_cap); | ||
assert!(old.is_some()); | ||
} else { | ||
*cap = CapabilityLocal::Unallocated; | ||
} | ||
} | ||
} | ||
} | ||
|
||
impl<'a, 'tcx> Analysis<'tcx> for FreePlaceCapabilitySummary<'a, 'tcx> { | ||
fn apply_statement_effect( | ||
&self, | ||
state: &mut Self::Domain, | ||
statement: &Statement<'tcx>, | ||
location: Location, | ||
) { | ||
state.repackings.clear(); | ||
state.visit_statement(statement, location); | ||
} | ||
|
||
fn apply_terminator_effect( | ||
&self, | ||
state: &mut Self::Domain, | ||
terminator: &Terminator<'tcx>, | ||
location: Location, | ||
) { | ||
state.repackings.clear(); | ||
state.visit_terminator(terminator, location); | ||
} | ||
|
||
fn apply_call_return_effect( | ||
&self, | ||
_state: &mut Self::Domain, | ||
_block: BasicBlock, | ||
_return_places: CallReturnPlaces<'_, 'tcx>, | ||
) { | ||
// Nothing to do here | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,148 @@ | ||
// © 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 std::fmt::{Debug, Formatter, Result}; | ||
|
||
use derive_more::{Deref, DerefMut}; | ||
use prusti_rustc_interface::{ | ||
dataflow::fmt::DebugWithContext, index::vec::IndexVec, middle::mir::Local, | ||
}; | ||
|
||
use crate::{ | ||
engine::FreePlaceCapabilitySummary, utils::PlaceRepacker, CapabilityKind, CapabilityLocal, | ||
CapabilityProjections, RepackOp, | ||
}; | ||
|
||
#[derive(Clone)] | ||
pub struct Fpcs<'a, 'tcx> { | ||
pub(crate) repacker: PlaceRepacker<'a, 'tcx>, | ||
pub summary: CapabilitySummary<'tcx>, | ||
pub repackings: Vec<RepackOp<'tcx>>, | ||
} | ||
impl<'a, 'tcx> Fpcs<'a, 'tcx> { | ||
pub(crate) fn new(repacker: PlaceRepacker<'a, 'tcx>) -> Self { | ||
let summary = CapabilitySummary::bottom_value(repacker.local_count()); | ||
Self { | ||
repacker, | ||
summary, | ||
repackings: Vec::new(), | ||
} | ||
} | ||
} | ||
|
||
impl PartialEq for Fpcs<'_, '_> { | ||
fn eq(&self, other: &Self) -> bool { | ||
self.summary == other.summary | ||
} | ||
} | ||
impl Eq for Fpcs<'_, '_> {} | ||
|
||
impl<'a, 'tcx> Debug for Fpcs<'a, 'tcx> { | ||
fn fmt(&self, f: &mut Formatter<'_>) -> Result { | ||
self.summary.fmt(f) | ||
} | ||
} | ||
impl<'a, 'tcx> DebugWithContext<FreePlaceCapabilitySummary<'a, 'tcx>> for Fpcs<'a, 'tcx> { | ||
fn fmt_diff_with( | ||
&self, | ||
old: &Self, | ||
_ctxt: &FreePlaceCapabilitySummary<'a, 'tcx>, | ||
f: &mut Formatter<'_>, | ||
) -> Result { | ||
assert_eq!(self.summary.len(), old.summary.len()); | ||
for (new, old) in self.summary.iter().zip(old.summary.iter()) { | ||
let changed = match (new, old) { | ||
(CapabilityLocal::Unallocated, CapabilityLocal::Unallocated) => false, | ||
(CapabilityLocal::Unallocated, CapabilityLocal::Allocated(a)) => { | ||
write!(f, "\u{001f}-{:?}", a.get_local())?; | ||
true | ||
} | ||
(CapabilityLocal::Allocated(a), CapabilityLocal::Unallocated) => { | ||
write!(f, "\u{001f}+{a:?}")?; | ||
true | ||
} | ||
(CapabilityLocal::Allocated(new), CapabilityLocal::Allocated(old)) => { | ||
if new != old { | ||
let mut new_set = CapabilityProjections::empty(); | ||
let mut old_set = CapabilityProjections::empty(); | ||
for (&p, &nk) in new.iter() { | ||
match old.get(&p) { | ||
Some(&ok) => { | ||
if let Some(d) = nk - ok { | ||
new_set.insert(p, d); | ||
} | ||
} | ||
None => { | ||
new_set.insert(p, nk); | ||
} | ||
} | ||
} | ||
for (&p, &ok) in old.iter() { | ||
match new.get(&p) { | ||
Some(&nk) => { | ||
if let Some(d) = ok - nk { | ||
old_set.insert(p, d); | ||
} | ||
} | ||
None => { | ||
old_set.insert(p, ok); | ||
} | ||
} | ||
} | ||
if !new_set.is_empty() { | ||
write!(f, "\u{001f}+{new_set:?}")? | ||
} | ||
if !old_set.is_empty() { | ||
write!(f, "\u{001f}-{old_set:?}")? | ||
} | ||
true | ||
} else { | ||
false | ||
} | ||
} | ||
}; | ||
if changed { | ||
if f.alternate() { | ||
writeln!(f)?; | ||
} else { | ||
write!(f, "\t")?; | ||
} | ||
} | ||
} | ||
Ok(()) | ||
} | ||
} | ||
|
||
#[derive(Clone, PartialEq, Eq, Deref, DerefMut)] | ||
/// Generic state of a set of locals | ||
pub struct Summary<T>(IndexVec<Local, T>); | ||
|
||
impl<T: Debug> Debug for Summary<T> { | ||
fn fmt(&self, f: &mut Formatter<'_>) -> Result { | ||
self.0.fmt(f) | ||
} | ||
} | ||
|
||
// impl<T> Summary<T> { | ||
// pub fn default(local_count: usize) -> Self | ||
// where | ||
// T: Default + Clone, | ||
// { | ||
// Self(IndexVec::from_elem_n(T::default(), local_count)) | ||
// } | ||
// } | ||
|
||
/// The free pcs of all locals | ||
pub type CapabilitySummary<'tcx> = Summary<CapabilityLocal<'tcx>>; | ||
|
||
impl<'tcx> CapabilitySummary<'tcx> { | ||
pub fn bottom_value(local_count: usize) -> Self { | ||
Self(IndexVec::from_fn_n( | ||
|local: Local| CapabilityLocal::new(local, CapabilityKind::Exclusive), | ||
local_count, | ||
)) | ||
} | ||
} |
197 changes: 197 additions & 0 deletions
197
mir-state-analysis/src/free_pcs/impl/join_semi_lattice.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,197 @@ | ||
// © 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::JoinSemiLattice; | ||
|
||
use crate::{ | ||
utils::PlaceRepacker, CapabilityKind, CapabilityLocal, CapabilityProjections, | ||
CapabilitySummary, Fpcs, PlaceOrdering, RepackOp, | ||
}; | ||
|
||
impl JoinSemiLattice for Fpcs<'_, '_> { | ||
fn join(&mut self, other: &Self) -> bool { | ||
self.summary.join(&other.summary, self.repacker) | ||
} | ||
} | ||
|
||
pub trait RepackingJoinSemiLattice<'tcx> { | ||
fn join(&mut self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> bool; | ||
fn bridge(&self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<RepackOp<'tcx>>; | ||
} | ||
impl<'tcx> RepackingJoinSemiLattice<'tcx> for CapabilitySummary<'tcx> { | ||
fn join(&mut self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> bool { | ||
let mut changed = false; | ||
for (l, to) in self.iter_enumerated_mut() { | ||
let local_changed = to.join(&other[l], repacker); | ||
changed = changed || local_changed; | ||
} | ||
changed | ||
} | ||
fn bridge(&self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<RepackOp<'tcx>> { | ||
let mut repacks = Vec::new(); | ||
for (l, to) in self.iter_enumerated() { | ||
let local_repacks = to.bridge(&other[l], repacker); | ||
repacks.extend(local_repacks); | ||
} | ||
repacks | ||
} | ||
} | ||
|
||
impl<'tcx> RepackingJoinSemiLattice<'tcx> for CapabilityLocal<'tcx> { | ||
#[tracing::instrument(name = "CapabilityLocal::join", level = "debug", skip(repacker))] | ||
fn join(&mut self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> bool { | ||
match (&mut *self, other) { | ||
(CapabilityLocal::Unallocated, CapabilityLocal::Unallocated) => false, | ||
(CapabilityLocal::Allocated(to_places), CapabilityLocal::Allocated(from_places)) => { | ||
to_places.join(from_places, repacker) | ||
} | ||
(CapabilityLocal::Allocated(..), CapabilityLocal::Unallocated) => { | ||
*self = CapabilityLocal::Unallocated; | ||
true | ||
} | ||
// Can jump to a `is_cleanup` block with some paths being alloc and other not | ||
(CapabilityLocal::Unallocated, CapabilityLocal::Allocated(..)) => false, | ||
} | ||
} | ||
fn bridge(&self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<RepackOp<'tcx>> { | ||
match (self, other) { | ||
(CapabilityLocal::Unallocated, CapabilityLocal::Unallocated) => Vec::new(), | ||
(CapabilityLocal::Allocated(to_places), CapabilityLocal::Allocated(from_places)) => { | ||
to_places.bridge(from_places, repacker) | ||
} | ||
(CapabilityLocal::Allocated(cps), CapabilityLocal::Unallocated) => { | ||
// TODO: remove need for clone | ||
let mut cps = cps.clone(); | ||
let local = cps.get_local(); | ||
let mut repacks = Vec::new(); | ||
for (&p, k) in cps.iter_mut() { | ||
if *k > CapabilityKind::Write { | ||
repacks.push(RepackOp::Weaken(p, *k, CapabilityKind::Write)); | ||
*k = CapabilityKind::Write; | ||
} | ||
} | ||
if !cps.contains_key(&local.into()) { | ||
let packs = cps.pack_ops( | ||
cps.keys().copied().collect(), | ||
local.into(), | ||
CapabilityKind::Write, | ||
repacker, | ||
); | ||
repacks.extend(packs); | ||
}; | ||
repacks.push(RepackOp::DeallocForCleanup(local)); | ||
repacks | ||
} | ||
(CapabilityLocal::Unallocated, CapabilityLocal::Allocated(..)) => unreachable!(), | ||
} | ||
} | ||
} | ||
|
||
impl<'tcx> RepackingJoinSemiLattice<'tcx> for CapabilityProjections<'tcx> { | ||
#[tracing::instrument(name = "CapabilityProjections::join", level = "trace", skip(repacker))] | ||
fn join(&mut self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> bool { | ||
let mut changed = false; | ||
for (&place, &kind) in &**other { | ||
let related = self.find_all_related(place, None); | ||
match related.relation { | ||
PlaceOrdering::Prefix => { | ||
changed = true; | ||
|
||
let from = related.from[0].0; | ||
let joinable_place = from.joinable_to(place, repacker); | ||
if joinable_place != from { | ||
self.unpack(from, joinable_place, repacker); | ||
} | ||
// Downgrade the permission if needed | ||
let new_min = kind.minimum(related.minimum).unwrap(); | ||
if new_min != related.minimum { | ||
self.insert(joinable_place, new_min); | ||
} | ||
} | ||
PlaceOrdering::Equal => { | ||
// Downgrade the permission if needed | ||
let new_min = kind.minimum(related.minimum).unwrap(); | ||
if new_min != related.minimum { | ||
changed = true; | ||
self.insert(place, new_min); | ||
} | ||
} | ||
PlaceOrdering::Suffix => { | ||
// Downgrade the permission if needed | ||
for &(p, k) in &related.from { | ||
let new_min = kind.minimum(k).unwrap(); | ||
if new_min != k { | ||
changed = true; | ||
self.insert(p, new_min); | ||
} | ||
} | ||
} | ||
PlaceOrdering::Both => { | ||
changed = true; | ||
|
||
// Downgrade the permission if needed | ||
let min = kind.minimum(related.minimum).unwrap(); | ||
for &(p, k) in &related.from { | ||
let new_min = min.minimum(k).unwrap(); | ||
if new_min != k { | ||
self.insert(p, new_min); | ||
} | ||
} | ||
let cp = related.from[0].0.common_prefix(place, repacker); | ||
self.pack(related.get_from(), cp, min, repacker); | ||
} | ||
} | ||
} | ||
changed | ||
} | ||
fn bridge(&self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec<RepackOp<'tcx>> { | ||
// TODO: remove need for clone | ||
let mut cps = self.clone(); | ||
|
||
let mut repacks = Vec::new(); | ||
for (&place, &kind) in &**other { | ||
let related = cps.find_all_related(place, None); | ||
match related.relation { | ||
PlaceOrdering::Prefix => { | ||
let from = related.from[0].0; | ||
// TODO: remove need for clone | ||
let unpacks = cps.unpack_ops(from, place, related.minimum, repacker); | ||
repacks.extend(unpacks); | ||
|
||
// Downgrade the permission if needed | ||
let new_min = kind.minimum(related.minimum).unwrap(); | ||
if new_min != related.minimum { | ||
cps.insert(place, new_min); | ||
repacks.push(RepackOp::Weaken(place, related.minimum, new_min)); | ||
} | ||
} | ||
PlaceOrdering::Equal => { | ||
// Downgrade the permission if needed | ||
let new_min = kind.minimum(related.minimum).unwrap(); | ||
if new_min != related.minimum { | ||
cps.insert(place, new_min); | ||
repacks.push(RepackOp::Weaken(place, related.minimum, new_min)); | ||
} | ||
} | ||
PlaceOrdering::Suffix => { | ||
// Downgrade the permission if needed | ||
for &(p, k) in &related.from { | ||
let new_min = kind.minimum(k).unwrap(); | ||
if new_min != k { | ||
cps.insert(p, new_min); | ||
repacks.push(RepackOp::Weaken(p, k, new_min)); | ||
} | ||
} | ||
let packs = | ||
cps.pack_ops(related.get_from(), related.to, related.minimum, repacker); | ||
repacks.extend(packs); | ||
} | ||
PlaceOrdering::Both => unreachable!(), | ||
} | ||
} | ||
repacks | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,163 @@ | ||
// © 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 std::fmt::{Debug, Formatter, Result}; | ||
|
||
use derive_more::{Deref, DerefMut}; | ||
use prusti_rustc_interface::{ | ||
data_structures::fx::{FxHashMap, FxHashSet}, | ||
middle::mir::Local, | ||
}; | ||
|
||
use crate::{utils::PlaceRepacker, CapabilityKind, Place, PlaceOrdering, RelatedSet}; | ||
|
||
#[derive(Clone, PartialEq, Eq)] | ||
/// The permissions of a local, each key in the hashmap is a "root" projection of the local | ||
/// Examples of root projections are: `_1`, `*_1.f`, `*(*_.f).g` (i.e. either a local or a deref) | ||
pub enum CapabilityLocal<'tcx> { | ||
Unallocated, | ||
Allocated(CapabilityProjections<'tcx>), | ||
} | ||
|
||
impl Debug for CapabilityLocal<'_> { | ||
fn fmt(&self, f: &mut Formatter<'_>) -> Result { | ||
match self { | ||
Self::Unallocated => write!(f, "U"), | ||
Self::Allocated(cps) => write!(f, "{cps:?}"), | ||
} | ||
} | ||
} | ||
|
||
impl<'tcx> CapabilityLocal<'tcx> { | ||
pub fn get_allocated_mut(&mut self) -> &mut CapabilityProjections<'tcx> { | ||
let Self::Allocated(cps) = self else { panic!("Expected allocated local") }; | ||
cps | ||
} | ||
pub fn new(local: Local, perm: CapabilityKind) -> Self { | ||
Self::Allocated(CapabilityProjections::new(local, perm)) | ||
} | ||
pub fn is_unallocated(&self) -> bool { | ||
matches!(self, Self::Unallocated) | ||
} | ||
} | ||
|
||
#[derive(Clone, PartialEq, Eq, Deref, DerefMut)] | ||
/// The permissions for all the projections of a place | ||
// We only need the projection part of the place | ||
pub struct CapabilityProjections<'tcx>(FxHashMap<Place<'tcx>, CapabilityKind>); | ||
|
||
impl<'tcx> Debug for CapabilityProjections<'tcx> { | ||
fn fmt(&self, f: &mut Formatter<'_>) -> Result { | ||
self.0.fmt(f) | ||
} | ||
} | ||
|
||
impl<'tcx> CapabilityProjections<'tcx> { | ||
pub fn new(local: Local, perm: CapabilityKind) -> Self { | ||
Self([(local.into(), perm)].into_iter().collect()) | ||
} | ||
pub fn new_uninit(local: Local) -> Self { | ||
Self::new(local, CapabilityKind::Write) | ||
} | ||
/// Should only be called when creating an update within `ModifiesFreeState` | ||
pub(crate) fn empty() -> Self { | ||
Self(FxHashMap::default()) | ||
} | ||
|
||
pub(crate) fn get_local(&self) -> Local { | ||
self.iter().next().unwrap().0.local | ||
} | ||
|
||
/// Returns all related projections of the given place that are contained in this map. | ||
/// A `Ordering::Less` means that the given `place` is a prefix of the iterator place. | ||
/// For example: find_all_related(x.f.g) = [(Less, x.f.g.h), (Greater, x.f)] | ||
/// It also checks that the ordering conforms to the expected ordering (the above would | ||
/// fail in any situation since all orderings need to be the same) | ||
#[tracing::instrument(level = "debug", skip(self))] | ||
pub(crate) fn find_all_related( | ||
&self, | ||
to: Place<'tcx>, | ||
mut expected: Option<PlaceOrdering>, | ||
) -> RelatedSet<'tcx> { | ||
let mut minimum = None::<CapabilityKind>; | ||
let mut related = Vec::new(); | ||
for (&from, &cap) in &**self { | ||
if let Some(ord) = from.partial_cmp(to) { | ||
minimum = if let Some(min) = minimum { | ||
Some(min.minimum(cap).unwrap()) | ||
} else { | ||
Some(cap) | ||
}; | ||
if let Some(expected) = expected { | ||
assert_eq!(ord, expected); | ||
} else { | ||
expected = Some(ord); | ||
} | ||
related.push((from, cap)); | ||
} | ||
} | ||
assert!( | ||
!related.is_empty(), | ||
"Cannot find related of {to:?} in {self:?}" | ||
); | ||
let relation = expected.unwrap(); | ||
if matches!(relation, PlaceOrdering::Prefix | PlaceOrdering::Equal) { | ||
assert_eq!(related.len(), 1); | ||
} | ||
RelatedSet { | ||
from: related, | ||
to, | ||
minimum: minimum.unwrap(), | ||
relation, | ||
} | ||
} | ||
|
||
#[tracing::instrument( | ||
name = "CapabilityProjections::unpack", | ||
level = "trace", | ||
skip(repacker), | ||
ret | ||
)] | ||
pub(crate) fn unpack( | ||
&mut self, | ||
from: Place<'tcx>, | ||
to: Place<'tcx>, | ||
repacker: PlaceRepacker<'_, 'tcx>, | ||
) -> Vec<(Place<'tcx>, Place<'tcx>)> { | ||
debug_assert!(!self.contains_key(&to)); | ||
let (expanded, others) = from.expand(to, repacker); | ||
let perm = self.remove(&from).unwrap(); | ||
self.extend(others.into_iter().map(|p| (p, perm))); | ||
self.insert(to, perm); | ||
expanded | ||
} | ||
|
||
// TODO: this could be implemented more efficiently, by assuming that a valid | ||
// state can always be packed up to the root | ||
#[tracing::instrument( | ||
name = "CapabilityProjections::pack", | ||
level = "trace", | ||
skip(repacker), | ||
ret | ||
)] | ||
pub(crate) fn pack( | ||
&mut self, | ||
mut from: FxHashSet<Place<'tcx>>, | ||
to: Place<'tcx>, | ||
perm: CapabilityKind, | ||
repacker: PlaceRepacker<'_, 'tcx>, | ||
) -> Vec<(Place<'tcx>, Place<'tcx>)> { | ||
debug_assert!(!self.contains_key(&to), "{to:?} already exists in {self:?}"); | ||
for place in &from { | ||
let p = self.remove(place).unwrap(); | ||
assert_eq!(p, perm, "Cannot pack {place:?} with {p:?} into {to:?}"); | ||
} | ||
let collapsed = to.collapse(&mut from, repacker); | ||
assert!(from.is_empty()); | ||
self.insert(to, perm); | ||
collapsed | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,92 @@ | ||
// © 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 std::{ | ||
cmp::Ordering, | ||
fmt::{Debug, Formatter, Result}, | ||
ops::Sub, | ||
}; | ||
|
||
use prusti_rustc_interface::data_structures::fx::FxHashSet; | ||
|
||
use crate::{Place, PlaceOrdering}; | ||
|
||
#[derive(Debug)] | ||
pub(crate) struct RelatedSet<'tcx> { | ||
pub(crate) from: Vec<(Place<'tcx>, CapabilityKind)>, | ||
pub(crate) to: Place<'tcx>, | ||
pub(crate) minimum: CapabilityKind, | ||
pub(crate) relation: PlaceOrdering, | ||
} | ||
impl<'tcx> RelatedSet<'tcx> { | ||
pub fn get_from(&self) -> FxHashSet<Place<'tcx>> { | ||
assert!(matches!( | ||
self.relation, | ||
PlaceOrdering::Suffix | PlaceOrdering::Both | ||
)); | ||
self.from.iter().map(|(p, _)| *p).collect() | ||
} | ||
} | ||
|
||
#[derive(Copy, Clone, PartialEq, Eq, Hash)] | ||
pub enum CapabilityKind { | ||
Read, | ||
Write, | ||
Exclusive, | ||
} | ||
impl Debug for CapabilityKind { | ||
fn fmt(&self, f: &mut Formatter<'_>) -> Result { | ||
match self { | ||
CapabilityKind::Read => write!(f, "R"), | ||
CapabilityKind::Write => write!(f, "W"), | ||
CapabilityKind::Exclusive => write!(f, "E"), | ||
} | ||
} | ||
} | ||
|
||
impl PartialOrd for CapabilityKind { | ||
fn partial_cmp(&self, other: &Self) -> Option<Ordering> { | ||
if *self == *other { | ||
return Some(Ordering::Equal); | ||
} | ||
match (self, other) { | ||
(CapabilityKind::Read, CapabilityKind::Exclusive) | ||
| (CapabilityKind::Write, CapabilityKind::Exclusive) => Some(Ordering::Less), | ||
(CapabilityKind::Exclusive, CapabilityKind::Read) | ||
| (CapabilityKind::Exclusive, CapabilityKind::Write) => Some(Ordering::Greater), | ||
_ => None, | ||
} | ||
} | ||
} | ||
|
||
impl Sub for CapabilityKind { | ||
type Output = Option<Self>; | ||
fn sub(self, other: Self) -> Self::Output { | ||
match (self, other) { | ||
(CapabilityKind::Exclusive, CapabilityKind::Read) => Some(CapabilityKind::Write), | ||
(CapabilityKind::Exclusive, CapabilityKind::Write) => Some(CapabilityKind::Read), | ||
_ => None, | ||
} | ||
} | ||
} | ||
|
||
impl CapabilityKind { | ||
pub fn is_read(self) -> bool { | ||
matches!(self, CapabilityKind::Read) | ||
} | ||
pub fn is_exclusive(self) -> bool { | ||
matches!(self, CapabilityKind::Exclusive) | ||
} | ||
pub fn is_write(self) -> bool { | ||
matches!(self, CapabilityKind::Write) | ||
} | ||
pub fn minimum(self, other: Self) -> Option<Self> { | ||
match self.partial_cmp(&other)? { | ||
Ordering::Greater => Some(other), | ||
_ => Some(self), | ||
} | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,148 @@ | ||
// © 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::{ | ||
hir::Mutability, | ||
middle::mir::{ | ||
visit::Visitor, BorrowKind, Local, Location, Operand, Rvalue, Statement, StatementKind, | ||
Terminator, TerminatorKind, RETURN_PLACE, | ||
}, | ||
}; | ||
|
||
use crate::Fpcs; | ||
|
||
impl<'tcx> Visitor<'tcx> for Fpcs<'_, 'tcx> { | ||
fn visit_operand(&mut self, operand: &Operand<'tcx>, location: Location) { | ||
self.super_operand(operand, location); | ||
match *operand { | ||
Operand::Copy(place) => { | ||
self.requires_read(place); | ||
} | ||
Operand::Move(place) => { | ||
self.requires_exclusive(place); | ||
self.ensures_write(place); | ||
} | ||
Operand::Constant(..) => (), | ||
} | ||
} | ||
|
||
fn visit_statement(&mut self, statement: &Statement<'tcx>, location: Location) { | ||
self.super_statement(statement, location); | ||
use StatementKind::*; | ||
match &statement.kind { | ||
&Assign(box (place, _)) => { | ||
self.requires_write(place); | ||
self.ensures_exclusive(place); | ||
} | ||
&FakeRead(box (_, place)) => self.requires_read(place), | ||
&SetDiscriminant { box place, .. } => self.requires_exclusive(place), | ||
&Deinit(box place) => { | ||
// TODO: Maybe OK to also allow `Write` here? | ||
self.requires_exclusive(place); | ||
self.ensures_write(place); | ||
} | ||
&StorageLive(local) => { | ||
self.requires_unalloc(local); | ||
self.ensures_allocates(local); | ||
} | ||
&StorageDead(local) => { | ||
self.requires_unalloc_or_uninit(local); | ||
self.ensures_unalloc(local); | ||
} | ||
&Retag(_, box place) => self.requires_exclusive(place), | ||
AscribeUserType(..) | Coverage(..) | Intrinsic(..) | ConstEvalCounter | Nop => (), | ||
}; | ||
} | ||
|
||
fn visit_terminator(&mut self, terminator: &Terminator<'tcx>, location: Location) { | ||
self.super_terminator(terminator, location); | ||
use TerminatorKind::*; | ||
match &terminator.kind { | ||
Goto { .. } | ||
| SwitchInt { .. } | ||
| Resume | ||
| Abort | ||
| Unreachable | ||
| Assert { .. } | ||
| GeneratorDrop | ||
| FalseEdge { .. } | ||
| FalseUnwind { .. } => (), | ||
Return => { | ||
let always_live = self.repacker.always_live_locals(); | ||
for local in 0..self.repacker.local_count() { | ||
let local = Local::from_usize(local); | ||
if always_live.contains(local) { | ||
self.requires_write(local); | ||
} else { | ||
self.requires_unalloc(local); | ||
} | ||
} | ||
self.requires_exclusive(RETURN_PLACE); | ||
} | ||
&Drop { place, .. } => { | ||
self.requires_write(place); | ||
self.ensures_write(place); | ||
} | ||
&DropAndReplace { place, .. } => { | ||
self.requires_write(place); | ||
self.ensures_exclusive(place); | ||
} | ||
&Call { destination, .. } => { | ||
self.requires_write(destination); | ||
self.ensures_exclusive(destination); | ||
} | ||
&Yield { resume_arg, .. } => { | ||
self.requires_write(resume_arg); | ||
self.ensures_exclusive(resume_arg); | ||
} | ||
InlineAsm { .. } => todo!("{terminator:?}"), | ||
}; | ||
} | ||
|
||
fn visit_rvalue(&mut self, rvalue: &Rvalue<'tcx>, location: Location) { | ||
self.super_rvalue(rvalue, location); | ||
use Rvalue::*; | ||
match rvalue { | ||
Use(_) | ||
| Repeat(_, _) | ||
| ThreadLocalRef(_) | ||
| Cast(_, _, _) | ||
| BinaryOp(_, _) | ||
| CheckedBinaryOp(_, _) | ||
| NullaryOp(_, _) | ||
| UnaryOp(_, _) | ||
| Aggregate(_, _) => {} | ||
|
||
&Ref(_, bk, place) => match bk { | ||
BorrowKind::Shared => { | ||
self.requires_read(place); | ||
// self.ensures_blocked_read(place); | ||
} | ||
// TODO: this should allow `Shallow Shared` as well | ||
BorrowKind::Shallow => { | ||
self.requires_read(place); | ||
// self.ensures_blocked_read(place); | ||
} | ||
BorrowKind::Unique => { | ||
self.requires_exclusive(place); | ||
// self.ensures_blocked_exclusive(place); | ||
} | ||
BorrowKind::Mut { .. } => { | ||
self.requires_exclusive(place); | ||
// self.ensures_blocked_exclusive(place); | ||
} | ||
}, | ||
&AddressOf(m, place) => match m { | ||
Mutability::Not => self.requires_read(place), | ||
Mutability::Mut => self.requires_exclusive(place), | ||
}, | ||
&Len(place) => self.requires_read(place), | ||
&Discriminant(place) => self.requires_read(place), | ||
ShallowInitBox(_, _) => todo!(), | ||
&CopyForDeref(place) => self.requires_read(place), | ||
} | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,132 @@ | ||
// © 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::{data_structures::fx::FxHashSet, middle::mir::Local}; | ||
|
||
use crate::{ | ||
utils::PlaceRepacker, CapabilityKind, CapabilityLocal, CapabilityProjections, Fpcs, Place, | ||
PlaceOrdering, RelatedSet, RepackOp, | ||
}; | ||
|
||
impl<'tcx> Fpcs<'_, 'tcx> { | ||
pub(crate) fn requires_unalloc(&mut self, local: Local) { | ||
assert!( | ||
self.summary[local].is_unallocated(), | ||
"local: {local:?}, fpcs: {self:?}\n" | ||
); | ||
} | ||
pub(crate) fn requires_unalloc_or_uninit(&mut self, local: Local) { | ||
if !self.summary[local].is_unallocated() { | ||
self.requires_write(local) | ||
} else { | ||
panic!() | ||
} | ||
} | ||
pub(crate) fn requires_read(&mut self, place: impl Into<Place<'tcx>>) { | ||
self.requires(place, CapabilityKind::Read) | ||
} | ||
/// May obtain write _or_ exclusive, if one should only have write afterwards, | ||
/// make sure to also call `ensures_write`! | ||
pub(crate) fn requires_write(&mut self, place: impl Into<Place<'tcx>>) { | ||
self.requires(place, CapabilityKind::Write) | ||
} | ||
pub(crate) fn requires_exclusive(&mut self, place: impl Into<Place<'tcx>>) { | ||
self.requires(place, CapabilityKind::Exclusive) | ||
} | ||
fn requires(&mut self, place: impl Into<Place<'tcx>>, cap: CapabilityKind) { | ||
let place = place.into(); | ||
let cp: &mut CapabilityProjections = self.summary[place.local].get_allocated_mut(); | ||
let ops = cp.repack(place, self.repacker); | ||
self.repackings.extend(ops); | ||
let kind = (*cp)[&place]; | ||
assert!(kind >= cap); | ||
} | ||
|
||
pub(crate) fn ensures_unalloc(&mut self, local: Local) { | ||
self.summary[local] = CapabilityLocal::Unallocated; | ||
} | ||
pub(crate) fn ensures_allocates(&mut self, local: Local) { | ||
assert_eq!(self.summary[local], CapabilityLocal::Unallocated); | ||
self.summary[local] = CapabilityLocal::Allocated(CapabilityProjections::new_uninit(local)); | ||
} | ||
fn ensures_alloc(&mut self, place: impl Into<Place<'tcx>>, cap: CapabilityKind) { | ||
let place = place.into(); | ||
let cp: &mut CapabilityProjections = self.summary[place.local].get_allocated_mut(); | ||
let old = cp.insert(place, cap); | ||
assert!(old.is_some()); | ||
} | ||
pub(crate) fn ensures_exclusive(&mut self, place: impl Into<Place<'tcx>>) { | ||
self.ensures_alloc(place, CapabilityKind::Exclusive) | ||
} | ||
pub(crate) fn ensures_write(&mut self, place: impl Into<Place<'tcx>>) { | ||
self.ensures_alloc(place, CapabilityKind::Write) | ||
} | ||
} | ||
|
||
impl<'tcx> CapabilityProjections<'tcx> { | ||
fn repack( | ||
&mut self, | ||
to: Place<'tcx>, | ||
repacker: PlaceRepacker<'_, 'tcx>, | ||
) -> Vec<RepackOp<'tcx>> { | ||
let related = self.find_all_related(to, None); | ||
match related.relation { | ||
PlaceOrdering::Prefix => self | ||
.unpack_ops(related.from[0].0, related.to, related.minimum, repacker) | ||
.collect(), | ||
PlaceOrdering::Equal => Vec::new(), | ||
PlaceOrdering::Suffix => self | ||
.pack_ops(related.get_from(), related.to, related.minimum, repacker) | ||
.collect(), | ||
PlaceOrdering::Both => { | ||
let cp = related.from[0].0.common_prefix(to, repacker); | ||
// Pack | ||
let mut ops = self.weaken(&related); | ||
let packs = self.pack_ops(related.get_from(), cp, related.minimum, repacker); | ||
ops.extend(packs); | ||
// Unpack | ||
let unpacks = self.unpack_ops(cp, related.to, related.minimum, repacker); | ||
ops.extend(unpacks); | ||
ops | ||
} | ||
} | ||
} | ||
pub(crate) fn unpack_ops( | ||
&mut self, | ||
from: Place<'tcx>, | ||
to: Place<'tcx>, | ||
kind: CapabilityKind, | ||
repacker: PlaceRepacker<'_, 'tcx>, | ||
) -> impl Iterator<Item = RepackOp<'tcx>> { | ||
self.unpack(from, to, repacker) | ||
.into_iter() | ||
.map(move |(f, t)| RepackOp::Unpack(f, t, kind)) | ||
} | ||
pub(crate) fn pack_ops( | ||
&mut self, | ||
from: FxHashSet<Place<'tcx>>, | ||
to: Place<'tcx>, | ||
perm: CapabilityKind, | ||
repacker: PlaceRepacker<'_, 'tcx>, | ||
) -> impl Iterator<Item = RepackOp<'tcx>> { | ||
self.pack(from, to, perm, repacker) | ||
.into_iter() | ||
.map(move |(f, t)| RepackOp::Pack(f, t, perm)) | ||
} | ||
|
||
pub(crate) fn weaken(&mut self, related: &RelatedSet<'tcx>) -> Vec<RepackOp<'tcx>> { | ||
let mut ops = Vec::new(); | ||
let more_than_min = related.from.iter().filter(|(_, k)| *k != related.minimum); | ||
// TODO: This will replace `PermissionKind::Exclusive` with `PermissionKind::Shared` | ||
// the exclusive permission will never be able to be recovered anymore! | ||
for &(p, k) in more_than_min { | ||
let old = self.insert(p, related.minimum); | ||
assert_eq!(old, Some(k)); | ||
ops.push(RepackOp::Weaken(p, k, related.minimum)); | ||
} | ||
ops | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,21 @@ | ||
// © 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::middle::mir::Local; | ||
|
||
use crate::{CapabilityKind, Place}; | ||
|
||
#[derive(Clone, Debug, Eq, PartialEq)] | ||
pub enum RepackOp<'tcx> { | ||
Weaken(Place<'tcx>, CapabilityKind, CapabilityKind), | ||
// TODO: figure out when and why this happens | ||
// DeallocUnknown(Local), | ||
DeallocForCleanup(Local), | ||
// First place is packed up, second is guide place to pack up from | ||
Pack(Place<'tcx>, Place<'tcx>, CapabilityKind), | ||
// First place is packed up, second is guide place to unpack to | ||
Unpack(Place<'tcx>, Place<'tcx>, CapabilityKind), | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,28 @@ | ||
// © 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/. | ||
|
||
#![feature(rustc_private)] | ||
#![feature(box_patterns)] | ||
|
||
mod free_pcs; | ||
mod utils; | ||
|
||
pub use free_pcs::*; | ||
pub use utils::place::*; | ||
|
||
use prusti_rustc_interface::{ | ||
dataflow::Analysis, | ||
middle::{mir::Body, ty::TyCtxt}, | ||
}; | ||
|
||
pub fn test_free_pcs<'tcx>(mir: &Body<'tcx>, tcx: TyCtxt<'tcx>) { | ||
let fpcs = free_pcs::engine::FreePlaceCapabilitySummary::new(tcx, &mir); | ||
let analysis = fpcs | ||
.into_engine(tcx, &mir) | ||
.pass_name("free_pcs") | ||
.iterate_to_fixpoint(); | ||
free_pcs::check(analysis); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.