Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Prusti 2.0: Free PCS #1398

Open
wants to merge 36 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
36 commits
Select commit Hold shift + click to select a range
9a8e1f0
Start work on MicroMir
JonasAlaif Feb 23, 2023
9c967ed
More work on MicroMir
JonasAlaif Mar 1, 2023
d86eabb
More work on MicroMir
JonasAlaif Mar 6, 2023
aa67674
Clippy/fmt fix
JonasAlaif Mar 8, 2023
18a6a0e
Merge branch 'master' into free-pcs
JonasAlaif Apr 17, 2023
0a533ae
Switch to using rustc dataflow engine
JonasAlaif Apr 18, 2023
a64df48
Add results cursor
JonasAlaif Apr 18, 2023
d85ed76
Display repacks in graphviz
JonasAlaif Apr 18, 2023
b914d79
Add `ShallowExclusive` capability
JonasAlaif Apr 19, 2023
d176fb8
Update
JonasAlaif Apr 24, 2023
2f8fbba
Bugfix
JonasAlaif Apr 25, 2023
330e61a
More changes
JonasAlaif Apr 25, 2023
9cebf2c
Merge branch 'master' into free-pcs-engine
JonasAlaif Aug 22, 2023
adf559b
Merge update fixes
JonasAlaif Aug 22, 2023
0900cef
Merge branch 'master' into free-pcs-engine
JonasAlaif Sep 27, 2023
5933a00
fmt
JonasAlaif Sep 27, 2023
496ebe1
Fix merge issues
JonasAlaif Sep 27, 2023
66f7ea2
Clippy fixes
JonasAlaif Sep 27, 2023
362788c
Bugfix for shallow exclusive
JonasAlaif Sep 28, 2023
813c87f
Remove check
JonasAlaif Sep 28, 2023
55bd039
fmt
JonasAlaif Sep 28, 2023
135065c
Bugfix
JonasAlaif Sep 28, 2023
a7a892b
Fix `PlaceMention` triple
JonasAlaif Sep 28, 2023
878b7da
Merge branch 'master' into free-pcs-engine
JonasAlaif Sep 28, 2023
62f8e62
Fix `can_deinit` check
JonasAlaif Sep 28, 2023
17ed9fe
fmt
JonasAlaif Sep 29, 2023
210d37a
Fix bug in `ConstantIndex` unpacking
JonasAlaif Oct 12, 2023
4047beb
Ensure that we never expand a Write capability
JonasAlaif Oct 12, 2023
4467796
fmt
JonasAlaif Oct 12, 2023
8e4030c
Add weakens before write
JonasAlaif Oct 20, 2023
7e12a2e
Bugfix to support other capabilities
JonasAlaif Oct 25, 2023
786a22d
Add pre and post distinction
JonasAlaif Oct 25, 2023
87d41e8
Add `ty` utility function
JonasAlaif Oct 25, 2023
09dcd1e
fmt and clippy
JonasAlaif Nov 13, 2023
54651c9
Make top crates iterator
JonasAlaif Nov 13, 2023
b9ba878
Disallow expanding through `Projection` at edges
JonasAlaif Nov 13, 2023
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Clippy/fmt fix
  • Loading branch information
JonasAlaif committed Mar 22, 2023
commit aa67674cf448fa221d8e399d7fccd677da0e0793
41 changes: 41 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

22 changes: 9 additions & 13 deletions micromir/src/defs/statement.rs
Original file line number Diff line number Diff line change
@@ -65,7 +65,7 @@ impl<'tcx> From<&Statement<'tcx>> for MicroStatement<'tcx> {
variant_index,
} => MicroStatementKind::SetDiscriminant {
place: box place.into(),
variant_index: variant_index,
variant_index,
},
&StatementKind::Deinit(box p) => MicroStatementKind::Deinit(box p.into()),
&StatementKind::StorageLive(l) => MicroStatementKind::StorageLive(l),
@@ -119,9 +119,9 @@ impl Debug for MicroStatementKind<'_> {
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result {
use MicroStatementKind::*;
match self {
Assign(box (ref place, ref rv)) => write!(fmt, "{:?} = {:?}", place, rv),
Assign(box (ref place, ref rv)) => write!(fmt, "{place:?} = {rv:?}"),
FakeRead(box (ref cause, ref place)) => {
write!(fmt, "FakeRead({:?}, {:?})", cause, place)
write!(fmt, "FakeRead({cause:?}, {place:?})")
}
Retag(ref kind, ref place) => write!(
fmt,
@@ -134,27 +134,23 @@ impl Debug for MicroStatementKind<'_> {
},
place,
),
StorageLive(ref place) => write!(fmt, "StorageLive({:?})", place),
StorageDead(ref place) => write!(fmt, "StorageDead({:?})", place),
StorageLive(ref place) => write!(fmt, "StorageLive({place:?})"),
StorageDead(ref place) => write!(fmt, "StorageDead({place:?})"),
SetDiscriminant {
ref place,
variant_index,
} => {
write!(fmt, "discriminant({:?}) = {:?}", place, variant_index)
write!(fmt, "discriminant({place:?}) = {variant_index:?}")
}
Deinit(ref place) => write!(fmt, "Deinit({:?})", place),
Deinit(ref place) => write!(fmt, "Deinit({place:?})"),
AscribeUserType(box (ref place, ref c_ty), ref variance) => {
write!(
fmt,
"AscribeUserType({:?}, {:?}, {:?})",
place, variance, c_ty
)
write!(fmt, "AscribeUserType({place:?}, {variance:?}, {c_ty:?})")
}
Coverage(box self::Coverage {
ref kind,
code_region: Some(ref rgn),
}) => {
write!(fmt, "Coverage::{:?} for {:?}", kind, rgn)
write!(fmt, "Coverage::{kind:?} for {rgn:?}")
}
Coverage(box ref coverage) => write!(fmt, "Coverage::{:?}", coverage.kind),
Intrinsic(box ref intrinsic) => write!(fmt, "{intrinsic}"),
16 changes: 8 additions & 8 deletions micromir/src/defs/terminator.rs
Original file line number Diff line number Diff line change
@@ -244,32 +244,32 @@ impl<'tcx> MicroTerminatorKind<'tcx> {
use MicroTerminatorKind::*;
match self {
Goto { .. } => write!(fmt, "goto"),
SwitchInt { discr, .. } => write!(fmt, "switchInt({:?})", discr),
SwitchInt { discr, .. } => write!(fmt, "switchInt({discr:?})"),
Return => write!(fmt, "return"),
GeneratorDrop => write!(fmt, "generator_drop"),
Resume => write!(fmt, "resume"),
Abort => write!(fmt, "abort"),
Yield {
value, resume_arg, ..
} => write!(fmt, "{:?} = yield({:?})", resume_arg, value),
} => write!(fmt, "{resume_arg:?} = yield({value:?})"),
Unreachable => write!(fmt, "unreachable"),
Drop { place, .. } => write!(fmt, "drop({:?})", place),
Drop { place, .. } => write!(fmt, "drop({place:?})"),
DropAndReplace { place, value, .. } => {
write!(fmt, "replace({:?} <- {:?})", place, value)
write!(fmt, "replace({place:?} <- {value:?})")
}
Call {
func,
args,
destination,
..
} => {
write!(fmt, "{:?} = ", destination)?;
write!(fmt, "{:?}(", func)?;
write!(fmt, "{destination:?} = ")?;
write!(fmt, "{func:?}(")?;
for (index, arg) in args.iter().enumerate() {
if index > 0 {
write!(fmt, ", ")?;
}
write!(fmt, "{:?}", arg)?;
write!(fmt, "{arg:?}")?;
}
write!(fmt, ")")
}
@@ -283,7 +283,7 @@ impl<'tcx> MicroTerminatorKind<'tcx> {
if !expected {
write!(fmt, "!")?;
}
write!(fmt, "{:?}, ", cond)?;
write!(fmt, "{cond:?}, ")?;
msg.fmt_assert_args(fmt)?;
write!(fmt, ")")
}
2 changes: 1 addition & 1 deletion micromir/src/free_pcs/permission.rs
Original file line number Diff line number Diff line change
@@ -94,7 +94,7 @@ impl<'tcx> LocalUpdate<'tcx> {
match state {
PermissionLocal::Unallocated => {
assert!(pre.unalloc_allowed);
return Some(PermissionLocal::Unallocated);
Some(PermissionLocal::Unallocated)
}
PermissionLocal::Allocated(state) => {
let mut achievable = PermissionProjections(FxHashMap::default());
10 changes: 4 additions & 6 deletions micromir/src/repack/calculate.rs
Original file line number Diff line number Diff line change
@@ -29,9 +29,8 @@ impl<'tcx> MicroBody<'tcx> {
FreeState::initial(self.body.local_decls().len(), |local: Local| {
if local == return_local {
Some(PermissionKind::Uninit)
} else if always_live.contains(local) {
Some(PermissionKind::Exclusive)
} else if local <= last_arg {
// TODO: figure out if `always_live` should start as `Uninit` or `Exclusive`
} else if local <= last_arg || always_live.contains(local) {
Some(PermissionKind::Exclusive)
} else {
None
@@ -46,7 +45,7 @@ impl<'tcx> MicroBody<'tcx> {
// Calculate initial state
let state = self.initial_free_state();
let preds = self.body.basic_blocks.predecessors();
let rp = PlaceRepacker::new(&*self.body, tcx);
let rp = PlaceRepacker::new(&self.body, tcx);
let start_node = self.body.basic_blocks.start_node();

// Do the actual repacking calculation
@@ -101,9 +100,8 @@ impl Queue {
self.done[bb] = true;
Some(bb)
} else {
if self.dirty_queue.len() == 0 {
if self.dirty_queue.is_empty() {
debug_assert!((0..self.done.len())
.into_iter()
.map(BasicBlock::from_usize)
.all(|bb| self.done[bb] || !self.can_redo[bb]));
return None;
4 changes: 2 additions & 2 deletions micromir/src/repack/mod.rs
Original file line number Diff line number Diff line change
@@ -4,11 +4,11 @@
// 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/.

mod repack;
mod repacker;
mod calculate;
pub(crate) mod triple;
mod place;

pub use calculate::*;
pub(crate) use place::*;
pub use repack::*;
pub use repacker::*;
1 change: 0 additions & 1 deletion micromir/src/repack/place.rs
Original file line number Diff line number Diff line change
@@ -52,7 +52,6 @@ impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> {
min_length,
from_end,
} => (0..min_length)
.into_iter()
.filter(|&i| {
if from_end {
i != min_length - offset
Original file line number Diff line number Diff line change
@@ -17,18 +17,13 @@ use crate::{
PermissionProjections, Place, PlaceOrdering, RelatedSet,
};

#[derive(Clone, Deref, DerefMut)]
#[derive(Clone, Default, Deref, DerefMut)]
pub struct Repacks<'tcx>(Vec<RepackOp<'tcx>>);
impl Debug for Repacks<'_> {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
self.0.fmt(f)
}
}
impl<'tcx> Repacks<'tcx> {
pub fn new() -> Self {
Self(Vec::new())
}
}

#[derive(Clone)]
pub struct PlaceCapabilitySummary<'tcx> {
@@ -69,7 +64,7 @@ pub struct TerminatorPlaceCapabilitySummary<'tcx> {

impl Debug for TerminatorPlaceCapabilitySummary<'_> {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
if self.repacks.len() == 0 {
if self.repacks.is_empty() {
write!(f, "{:?}", &self.state_before)
} else {
f.debug_struct("PCS")
@@ -105,7 +100,7 @@ impl<'tcx> TerminatorPlaceCapabilitySummary<'tcx> {
is_cleanup: bool,
rp: PlaceRepacker<'_, 'tcx>,
) {
let repacks = self.repacks.entry(bb).or_insert_with(Repacks::new);
let repacks = self.repacks.entry(bb).or_default();
repacks.clear();
for (l, to) in to.iter_enumerated() {
let new =
@@ -123,7 +118,7 @@ impl<'tcx> FreeState<'tcx> {
update: &FreeStateUpdate<'tcx>,
rp: PlaceRepacker<'_, 'tcx>,
) -> (PlaceCapabilitySummary<'tcx>, FreeState<'tcx>) {
let mut repacks = Repacks::new();
let mut repacks = Repacks::default();
let pre = update
.iter_enumerated()
.map(|(l, update)| {
10 changes: 3 additions & 7 deletions micromir/tests/top_crates.rs
Original file line number Diff line number Diff line change
@@ -26,13 +26,10 @@ pub fn top_crates_range(range: std::ops::Range<usize>) {
}

fn run_on_crate(name: &str, version: &str) {
let dirname = format!("./tmp/{}-{}", name, version);
let dirname = format!("./tmp/{name}-{version}");
let filename = format!("{dirname}.crate");
if !std::path::PathBuf::from(&filename).exists() {
let dl = format!(
"https://crates.io/api/v1/crates/{}/{}/download",
name, version
);
let dl = format!("https://crates.io/api/v1/crates/{name}/{version}/download");
let mut resp = get(&dl).expect("Could not fetch top crates");
let mut file = std::fs::File::create(&filename).unwrap();
resp.copy_to(&mut file).unwrap();
@@ -102,8 +99,7 @@ fn top_crates_by_download_count(mut count: usize) -> Vec<Crate> {
let mut sources = Vec::new();
for page in 1..page_count {
let url = format!(
"https://crates.io/api/v1/crates?page={}&per_page={}&sort=downloads",
page, PAGE_SIZE
"https://crates.io/api/v1/crates?page={page}&per_page={PAGE_SIZE}&sort=downloads"
);
let resp = get(&url).expect("Could not fetch top crates");
assert!(