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
Show file tree
Hide file tree
Changes from all commits
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
40 changes: 40 additions & 0 deletions Cargo.lock

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

1 change: 1 addition & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ members = [
"prusti-common",
"prusti-utils",
"tracing",
"mir-state-analysis",
"prusti-interface",
"prusti-viper",
"prusti-server",
Expand Down
12 changes: 8 additions & 4 deletions analysis/tests/utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,12 +31,16 @@ pub fn find_compiled_executable(name: &str) -> PathBuf {
}

pub fn find_sysroot() -> String {
// Taken from https://github.com/Manishearth/rust-clippy/pull/911.
let home = option_env!("RUSTUP_HOME").or(option_env!("MULTIRUST_HOME"));
let toolchain = option_env!("RUSTUP_TOOLCHAIN").or(option_env!("MULTIRUST_TOOLCHAIN"));
// Taken from https://github.com/rust-lang/rust-clippy/commit/f5db351a1d502cb65f8807ec2c84f44756099ef3.
let home = std::env::var("RUSTUP_HOME")
.or_else(|_| std::env::var("MULTIRUST_HOME"))
.ok();
let toolchain = std::env::var("RUSTUP_TOOLCHAIN")
.or_else(|_| std::env::var("MULTIRUST_TOOLCHAIN"))
.ok();
match (home, toolchain) {
(Some(home), Some(toolchain)) => format!("{home}/toolchains/{toolchain}"),
_ => option_env!("RUST_SYSROOT")
_ => std::env::var("RUST_SYSROOT")
.expect("need to specify RUST_SYSROOT env var or use rustup or multirust")
.to_owned(),
}
Expand Down
20 changes: 20 additions & 0 deletions mir-state-analysis/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
[package]
name = "mir-state-analysis"
version = "0.1.0"
authors = ["Prusti Devs <[email protected]>"]
edition = "2021"

[dependencies]
derive_more = "0.99"
tracing = { path = "../tracing" }
prusti-rustc-interface = { path = "../prusti-rustc-interface" }

[dev-dependencies]
reqwest = { version = "^0.11", features = ["blocking"] }
serde = "^1.0"
serde_derive = "^1.0"
serde_json = "^1.0"

[package.metadata.rust-analyzer]
# This crate uses #[feature(rustc_private)]
rustc_private = true
202 changes: 202 additions & 0 deletions mir-state-analysis/src/free_pcs/check/checker.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,202 @@
// © 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,
middle::mir::{visit::Visitor, Location, ProjectionElem},
};

use crate::{
free_pcs::{
CapabilityKind, CapabilityLocal, CapabilitySummary, Fpcs, FreePcsAnalysis, RepackOp,
},
utils::PlaceRepacker,
};

use super::consistency::CapabilityConistency;

pub(crate) fn check(mut cursor: FreePcsAnalysis<'_, '_>) {
let rp = cursor.repacker();
let body = rp.body();
for (block, data) in body.basic_blocks.iter_enumerated() {
cursor.analysis_for_bb(block);
let mut fpcs = Fpcs {
summary: cursor.initial_state().clone(),
apply_pre_effect: true,
bottom: false,
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,
};
let fpcs_after = cursor.next(loc);
assert_eq!(fpcs_after.location, loc);
// Repacks
for &op in &fpcs_after.repacks_middle {
op.update_free(&mut fpcs.summary, data.is_cleanup, true, rp);
}
// Consistency
fpcs.summary.consistency_check(rp);
// Statement pre
assert!(fpcs.repackings.is_empty());
fpcs.apply_pre_effect = true;
fpcs.visit_statement(stmt, loc);
assert!(fpcs.repackings.is_empty());

// Repacks
for op in fpcs_after.repacks {
op.update_free(&mut fpcs.summary, data.is_cleanup, true, rp);
}
// Statement post
fpcs.apply_pre_effect = false;
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(),
};
let fpcs_after = cursor.next(loc);
assert_eq!(fpcs_after.location, loc);
// Repacks
for op in fpcs_after.repacks_middle {
op.update_free(&mut fpcs.summary, data.is_cleanup, true, rp);
}
// Consistency
fpcs.summary.consistency_check(rp);
// Statement pre
assert!(fpcs.repackings.is_empty());
fpcs.apply_pre_effect = true;
fpcs.visit_terminator(data.terminator(), loc);
assert!(fpcs.repackings.is_empty());

// Repacks
for op in fpcs_after.repacks {
op.update_free(&mut fpcs.summary, data.is_cleanup, true, rp);
}
// Statement post
fpcs.apply_pre_effect = false;
fpcs.visit_terminator(data.terminator(), loc);
assert!(fpcs.repackings.is_empty());
// Consistency
fpcs.summary.consistency_check(rp);
assert_eq!(fpcs.summary, fpcs_after.state);

let fpcs_end = cursor.terminator();

for succ in fpcs_end.succs {
// Repacks
let mut from = fpcs.clone();
for op in succ.repacks {
op.update_free(
&mut from.summary,
body.basic_blocks[succ.location.block].is_cleanup,
false,
rp,
);
}
assert_eq!(from.summary, succ.state);
}
}
}

impl<'tcx> RepackOp<'tcx> {
#[tracing::instrument(level = "debug", skip(rp))]
fn update_free(
self,
state: &mut CapabilitySummary<'tcx>,
is_cleanup: bool,
can_downcast: bool,
rp: PlaceRepacker<'_, 'tcx>,
) {
match self {
RepackOp::StorageDead(local) => {
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::IgnoreStorageDead(local) => {
assert_eq!(state[local], CapabilityLocal::Unallocated);
// Add write permission so that the `mir::StatementKind::StorageDead` can
// deallocate without producing any repacks, which would cause the
// `assert!(fpcs.repackings.is_empty());` above to fail.
state[local] = CapabilityLocal::new(local, CapabilityKind::Write);
}
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::Expand(place, guide, kind) => {
assert_eq!(kind, CapabilityKind::Exclusive, "{self:?}");
assert!(place.is_prefix_exact(guide), "{self:?}");
assert!(
can_downcast
|| !matches!(
guide.projection.last().unwrap(),
ProjectionElem::Downcast(..)
),
"{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)));
}
RepackOp::Collapse(place, guide, kind) => {
assert_ne!(kind, CapabilityKind::ShallowExclusive, "{self:?}");
assert!(place.is_prefix_exact(guide), "{self:?}");
let curr_state = state[place.local].get_allocated_mut();
let mut removed = curr_state
.extract_if(|p, _| place.related_to(*p))
.collect::<FxHashMap<_, _>>();

let (p, mut others, _) = place.expand_one_level(guide, rp);
others.push(p);
for other in others {
assert_eq!(removed.remove(&other), Some(kind), "{self:?}");
}
assert!(removed.is_empty(), "{self:?}, {removed:?}");
let old = curr_state.insert(place, kind);
assert_eq!(old, None);
}
RepackOp::DerefShallowInit(place, guide) => {
assert!(place.is_prefix_exact(guide), "{self:?}");
assert_eq!(*guide.projection.last().unwrap(), ProjectionElem::Deref);
let curr_state = state[place.local].get_allocated_mut();
assert_eq!(
curr_state.remove(&place),
Some(CapabilityKind::ShallowExclusive),
"{self:?} ({curr_state:?})"
);

let (p, others, pkind) = place.expand_one_level(guide, rp);
assert!(pkind.is_box());
curr_state.insert(p, CapabilityKind::Write);
assert!(others.is_empty());
}
}
}
}
58 changes: 58 additions & 0 deletions mir-state-analysis/src/free_pcs/check/consistency.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
// © 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::{
free_pcs::{CapabilityKind, CapabilityLocal, CapabilityProjections, Summary},
utils::{Place, PlaceRepacker},
};

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:?}",);
}
// Cannot be inside of uninitialized pointers.
if !p1.can_deinit(repacker) {
assert!(matches!(self[p1], CapabilityKind::Exclusive), "{self:?}");
}
// Cannot have Read or None here
assert!(self[p1] >= CapabilityKind::Write);
// Can only have `ShallowExclusive` for box typed places
if self[p1].is_shallow_exclusive() {
assert!(p1.ty(repacker).ty.is_box());
}
}
// 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());
}
}
Loading
Loading