diff --git a/Cargo.lock b/Cargo.lock index e070c4b73aa..0c7a4b25ef7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1499,6 +1499,19 @@ dependencies = [ "tokio-rustls", ] +[[package]] +name = "hyper-tls" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d6183ddfa99b85da61a140bea0efc93fdf56ceaa041b37d553518030827f9905" +dependencies = [ + "bytes", + "hyper", + "native-tls", + "tokio", + "tokio-native-tls", +] + [[package]] name = "iana-time-zone" version = "0.1.57" @@ -1864,6 +1877,19 @@ dependencies = [ "windows-sys 0.42.0", ] +[[package]] +name = "mir-state-analysis" +version = "0.1.0" +dependencies = [ + "derive_more", + "prusti-rustc-interface", + "reqwest", + "serde", + "serde_derive", + "serde_json", + "tracing 0.1.0", +] + [[package]] name = "multer" version = "2.1.0" @@ -2266,6 +2292,7 @@ dependencies = [ "env_logger", "lazy_static", "log", + "mir-state-analysis", "prusti-common", "prusti-interface", "prusti-rustc-interface", @@ -2597,10 +2624,12 @@ dependencies = [ "http-body", "hyper", "hyper-rustls", + "hyper-tls", "ipnet", "js-sys", "log", "mime", + "native-tls", "once_cell", "percent-encoding", "pin-project-lite", @@ -2610,6 +2639,7 @@ dependencies = [ "serde_json", "serde_urlencoded", "tokio", + "tokio-native-tls", "tokio-rustls", "tower-service", "url", @@ -3335,6 +3365,16 @@ dependencies = [ "windows-sys 0.48.0", ] +[[package]] +name = "tokio-native-tls" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bbae76ab933c85776efabc971569dd6119c580d8f5d448769dec1764bf796ef2" +dependencies = [ + "native-tls", + "tokio", +] + [[package]] name = "tokio-rustls" version = "0.24.1" diff --git a/Cargo.toml b/Cargo.toml index d7c51520036..b896349ceed 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -7,6 +7,7 @@ members = [ "prusti-common", "prusti-utils", "tracing", + "mir-state-analysis", "prusti-interface", "prusti-viper", "prusti-server", diff --git a/analysis/tests/utils.rs b/analysis/tests/utils.rs index 397f53aeaa6..b9ef0a0cdd9 100644 --- a/analysis/tests/utils.rs +++ b/analysis/tests/utils.rs @@ -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(), } diff --git a/mir-state-analysis/Cargo.toml b/mir-state-analysis/Cargo.toml new file mode 100644 index 00000000000..958fe750062 --- /dev/null +++ b/mir-state-analysis/Cargo.toml @@ -0,0 +1,20 @@ +[package] +name = "mir-state-analysis" +version = "0.1.0" +authors = ["Prusti Devs "] +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 diff --git a/mir-state-analysis/src/free_pcs/check/checker.rs b/mir-state-analysis/src/free_pcs/check/checker.rs new file mode 100644 index 00000000000..77a9ffedea6 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/check/checker.rs @@ -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::>(); + + 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()); + } + } + } +} diff --git a/mir-state-analysis/src/free_pcs/check/consistency.rs b/mir-state-analysis/src/free_pcs/check/consistency.rs new file mode 100644 index 00000000000..af5f2fa7a84 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/check/consistency.rs @@ -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 { + 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::>(); + 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()); + } +} diff --git a/mir-state-analysis/src/free_pcs/check/mod.rs b/mir-state-analysis/src/free_pcs/check/mod.rs new file mode 100644 index 00000000000..6a308a2b833 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/check/mod.rs @@ -0,0 +1,10 @@ +// © 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/. + +mod checker; +mod consistency; + +pub(crate) use checker::check; diff --git a/mir-state-analysis/src/free_pcs/impl/engine.rs b/mir-state-analysis/src/free_pcs/impl/engine.rs new file mode 100644 index 00000000000..fdbcf85cc31 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/engine.rs @@ -0,0 +1,139 @@ +// © 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}, + index::Idx, + middle::{ + mir::{ + visit::Visitor, BasicBlock, Body, CallReturnPlaces, Local, Location, Statement, + Terminator, TerminatorEdges, RETURN_PLACE, + }, + ty::TyCtxt, + }, +}; + +use crate::{ + free_pcs::{CapabilityKind, CapabilityLocal, Fpcs}, + utils::PlaceRepacker, +}; + +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) { + state.bottom = false; + 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() { + assert!(cap.is_unallocated()); + let new_cap = if local == return_local { + CapabilityLocal::new(local, CapabilityKind::Write) + } else if local <= last_arg { + CapabilityLocal::new(local, CapabilityKind::Exclusive) + } 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 + }; + CapabilityLocal::new(local, al_cap) + } else { + CapabilityLocal::Unallocated + }; + *cap = new_cap; + } + } +} + +impl<'a, 'tcx> Analysis<'tcx> for FreePlaceCapabilitySummary<'a, 'tcx> { + #[tracing::instrument( + name = "FreePlaceCapabilitySummary::apply_before_statement_effect", + level = "debug", + skip(self) + )] + fn apply_before_statement_effect( + &mut self, + state: &mut Self::Domain, + statement: &Statement<'tcx>, + location: Location, + ) { + state.repackings.clear(); + state.apply_pre_effect = true; + state.visit_statement(statement, location); + } + #[tracing::instrument( + name = "FreePlaceCapabilitySummary::apply_statement_effect", + level = "debug", + skip(self) + )] + fn apply_statement_effect( + &mut self, + state: &mut Self::Domain, + statement: &Statement<'tcx>, + location: Location, + ) { + state.repackings.clear(); + state.apply_pre_effect = false; + state.visit_statement(statement, location); + } + + #[tracing::instrument( + name = "FreePlaceCapabilitySummary::apply_before_terminator_effect", + level = "debug", + skip(self) + )] + fn apply_before_terminator_effect( + &mut self, + state: &mut Self::Domain, + terminator: &Terminator<'tcx>, + location: Location, + ) { + state.repackings.clear(); + state.apply_pre_effect = true; + state.visit_terminator(terminator, location); + } + #[tracing::instrument( + name = "FreePlaceCapabilitySummary::apply_terminator_effect", + level = "debug", + skip(self) + )] + fn apply_terminator_effect<'mir>( + &mut self, + state: &mut Self::Domain, + terminator: &'mir Terminator<'tcx>, + location: Location, + ) -> TerminatorEdges<'mir, 'tcx> { + state.repackings.clear(); + state.apply_pre_effect = false; + state.visit_terminator(terminator, location); + terminator.edges() + } + + fn apply_call_return_effect( + &mut self, + _state: &mut Self::Domain, + _block: BasicBlock, + _return_places: CallReturnPlaces<'_, 'tcx>, + ) { + // Nothing to do here + } +} diff --git a/mir-state-analysis/src/free_pcs/impl/fpcs.rs b/mir-state-analysis/src/free_pcs/impl/fpcs.rs new file mode 100644 index 00000000000..966a3a855b4 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/fpcs.rs @@ -0,0 +1,143 @@ +// © 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::IndexVec, middle::mir::Local, +}; + +use crate::{ + free_pcs::{ + engine::FreePlaceCapabilitySummary, CapabilityLocal, CapabilityProjections, RepackOp, + }, + utils::PlaceRepacker, +}; + +#[derive(Clone)] +pub struct Fpcs<'a, 'tcx> { + pub(crate) repacker: PlaceRepacker<'a, 'tcx>, + pub(crate) bottom: bool, + pub(crate) apply_pre_effect: bool, + pub summary: CapabilitySummary<'tcx>, + pub repackings: Vec>, +} +impl<'a, 'tcx> Fpcs<'a, 'tcx> { + pub(crate) fn new(repacker: PlaceRepacker<'a, 'tcx>) -> Self { + let summary = CapabilitySummary::default(repacker.local_count()); + Self { + repacker, + bottom: true, + apply_pre_effect: true, + summary, + repackings: Vec::new(), + } + } +} + +impl PartialEq for Fpcs<'_, '_> { + fn eq(&self, other: &Self) -> bool { + self.bottom == other.bottom + && self.summary == other.summary + && self.repackings == other.repackings + } +} +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> for Fpcs<'a, 'tcx> { + fn fmt_diff_with( + &self, + old: &Self, + _ctxt: &FreePlaceCapabilitySummary<'a, 'tcx>, + f: &mut Formatter<'_>, + ) -> Result { + // let rp = self.repacker; + assert_eq!(self.summary.len(), old.summary.len()); + for op in &self.repackings { + writeln!(f, "{op}")?; + } + 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 nk == ok => (), + _ => { + new_set.insert(p, nk); + } + } + } + for (&p, &ok) in old.iter() { + match new.get(&p) { + Some(&nk) if nk == ok => (), + _ => { + 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(IndexVec); + +impl Debug for Summary { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + self.0.fmt(f) + } +} + +impl Summary { + 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>; diff --git a/mir-state-analysis/src/free_pcs/impl/join_semi_lattice.rs b/mir-state-analysis/src/free_pcs/impl/join_semi_lattice.rs new file mode 100644 index 00000000000..24536ef2a79 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/join_semi_lattice.rs @@ -0,0 +1,195 @@ +// © 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::{ + free_pcs::{ + CapabilityKind, CapabilityLocal, CapabilityProjections, CapabilitySummary, Fpcs, RepackOp, + }, + utils::{PlaceOrdering, PlaceRepacker}, +}; + +impl JoinSemiLattice for Fpcs<'_, '_> { + #[tracing::instrument(name = "Fpcs::join", level = "debug")] + fn join(&mut self, other: &Self) -> bool { + assert!(!other.bottom); + if self.bottom { + self.clone_from(other); + true + } else { + 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>; +} +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> { + let mut repacks = Vec::new(); + for (l, from) in self.iter_enumerated() { + let local_repacks = from.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> { + match (self, other) { + (CapabilityLocal::Unallocated, CapabilityLocal::Unallocated) => Vec::new(), + (CapabilityLocal::Allocated(from_places), CapabilityLocal::Allocated(to_places)) => { + from_places.bridge(to_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.collapse(cps.keys().copied().collect(), local.into(), repacker); + repacks.extend(packs); + }; + repacks.push(RepackOp::StorageDead(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); + let final_place = match related.relation { + PlaceOrdering::Prefix => { + let from = related.get_only_from(); + let joinable_place = if self[&from] != CapabilityKind::Exclusive { + // One cannot expand a `Write` or a `ShallowInit` capability + from + } else { + from.joinable_to(place) + }; + assert!(from.is_prefix(joinable_place)); + if joinable_place != from { + changed = true; + self.expand(from, joinable_place, repacker); + } + Some(joinable_place) + } + PlaceOrdering::Equal => Some(place), + PlaceOrdering::Suffix => { + // Downgrade the permission if needed + for &(p, k) in &related.from { + // Might not contain key if `p.projects_ptr(repacker)` + // returned `Some` in a previous iteration. + if !self.contains_key(&p) { + continue; + } + let collapse_to = if kind != CapabilityKind::Exclusive { + related.to + } else { + related.to.joinable_to(p) + }; + if collapse_to != p { + changed = true; + let mut from = related.get_from(); + from.retain(|&from| collapse_to.is_prefix(from)); + self.collapse(from, collapse_to, repacker); + } + if k > kind { + changed = true; + self.update_cap(collapse_to, kind); + } + } + None + } + PlaceOrdering::Both => { + changed = true; + + let cp = related.common_prefix(place); + self.collapse(related.get_from(), cp, repacker); + Some(cp) + } + }; + if let Some(place) = final_place { + // Downgrade the permission if needed + if self[&place] > kind { + changed = true; + self.update_cap(place, kind); + } + } + } + changed + } + fn bridge(&self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec> { + // TODO: remove need for clone + let mut from = self.clone(); + + let mut repacks = Vec::new(); + for (&place, &kind) in &**other { + let related = from.find_all_related(place, None); + match related.relation { + PlaceOrdering::Prefix => { + let from_place = related.get_only_from(); + // TODO: remove need for clone + let unpacks = from.expand(from_place, place, repacker); + repacks.extend(unpacks); + } + PlaceOrdering::Equal => (), + PlaceOrdering::Suffix => { + let packs = from.collapse(related.get_from(), related.to, repacker); + repacks.extend(packs); + } + PlaceOrdering::Both => unreachable!("{self:?}\n{from:?}\n{other:?}\n{related:?}"), + } + // Downgrade the permission if needed + let curr = from[&place]; + if curr != kind { + assert!(curr > kind); + from.insert(place, kind); + repacks.push(RepackOp::Weaken(place, curr, kind)); + } + } + repacks + } +} diff --git a/mir-state-analysis/src/free_pcs/impl/local.rs b/mir-state-analysis/src/free_pcs/impl/local.rs new file mode 100644 index 00000000000..b154e6b34a5 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/local.rs @@ -0,0 +1,228 @@ +// © 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::{ + free_pcs::{CapabilityKind, RelatedSet, RepackOp}, + utils::{Place, PlaceOrdering, PlaceRepacker}, +}; + +#[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 Default for CapabilityLocal<'_> { + fn default() -> Self { + Self::Unallocated + } +} + +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, 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 + } + + pub(crate) fn update_cap(&mut self, place: Place<'tcx>, cap: CapabilityKind) { + let old = self.insert(place, cap); + assert!(old.is_some()); + } + + /// 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", ret)] + pub(crate) fn find_all_related( + &self, + to: Place<'tcx>, + mut expected: Option, + ) -> RelatedSet<'tcx> { + // let mut minimum = None::; + let mut related = Vec::new(); + for (&from, &cap) in &**self { + if let Some(ord) = from.partial_cmp(to) { + // let cap_no_read = cap.read_as_exclusive(); + // minimum = if let Some(min) = minimum { + // Some(min.minimum(cap_no_read).unwrap()) + // } else { + // Some(cap_no_read) + // }; + if let Some(expected) = expected { + assert_eq!(ord, expected, "({self:?}) {from:?} {to:?}"); + } 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 expand( + &mut self, + from: Place<'tcx>, + to: Place<'tcx>, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> Vec> { + debug_assert!(!self.contains_key(&to)); + let (expanded, mut others) = from.expand(to, repacker); + let mut perm = self.remove(&from).unwrap(); + others.push(to); + let mut ops = Vec::new(); + for (from, to, kind) in expanded { + let others = others.extract_if(|other| !to.is_prefix(*other)); + self.extend(others.map(|p| (p, perm))); + if kind.is_box() && perm.is_shallow_exclusive() { + ops.push(RepackOp::DerefShallowInit(from, to)); + perm = CapabilityKind::Write; + } else { + ops.push(RepackOp::Expand(from, to, perm)); + } + } + self.extend(others.into_iter().map(|p| (p, perm))); + // assert!(self.contains_key(&to), "{self:?}\n{to:?}"); + ops + } + + // 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 collapse( + &mut self, + mut from: FxHashSet>, + to: Place<'tcx>, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> Vec> { + debug_assert!(!self.contains_key(&to), "{to:?} already exists in {self:?}"); + let mut old_caps: FxHashMap<_, _> = from + .iter() + .map(|&p| (p, self.remove(&p).unwrap())) + .collect(); + let collapsed = to.collapse(&mut from, repacker); + assert!(from.is_empty(), "{from:?} ({collapsed:?}) {to:?}"); + let mut exclusive_at = Vec::new(); + if !to.projects_shared_ref(repacker) { + for (to, _, kind) in &collapsed { + if kind.is_shared_ref() { + let mut is_prefixed = false; + exclusive_at + .extract_if(|old| { + let cmp = to.either_prefix(*old); + if matches!(cmp, Some(false)) { + is_prefixed = true; + } + cmp.unwrap_or_default() + }) + .for_each(drop); + if !is_prefixed { + exclusive_at.push(*to); + } + } + } + } + let mut ops = Vec::new(); + for (to, from, _) in collapsed { + let removed_perms: Vec<_> = old_caps.extract_if(|old, _| to.is_prefix(*old)).collect(); + let perm = removed_perms + .iter() + .fold(CapabilityKind::Exclusive, |acc, (_, p)| { + acc.minimum(*p).unwrap() + }); + for (from, from_perm) in removed_perms { + if perm != from_perm { + assert!(from_perm > perm); + ops.push(RepackOp::Weaken(from, from_perm, perm)); + } + } + old_caps.insert(to, perm); + ops.push(RepackOp::Collapse(to, from, perm)); + } + self.insert(to, old_caps[&to]); + ops + } +} diff --git a/mir-state-analysis/src/free_pcs/impl/mod.rs b/mir-state-analysis/src/free_pcs/impl/mod.rs new file mode 100644 index 00000000000..3ee083a3dc9 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/mod.rs @@ -0,0 +1,17 @@ +// © 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/. + +mod fpcs; +mod local; +mod place; +pub(crate) mod engine; +pub(crate) mod join_semi_lattice; +mod triple; +mod update; + +pub(crate) use fpcs::*; +pub(crate) use local::*; +pub use place::*; diff --git a/mir-state-analysis/src/free_pcs/impl/place.rs b/mir-state-analysis/src/free_pcs/impl/place.rs new file mode 100644 index 00000000000..259dd639036 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/place.rs @@ -0,0 +1,94 @@ +// © 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}, +}; + +use prusti_rustc_interface::data_structures::fx::FxHashSet; + +use crate::utils::{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> { + assert!(matches!( + self.relation, + PlaceOrdering::Suffix | PlaceOrdering::Both + )); + self.from.iter().map(|(p, _)| *p).collect() + } + pub fn get_only_from(&self) -> Place<'tcx> { + assert_eq!(self.from.len(), 1); + self.from[0].0 + } + pub fn common_prefix(&self, to: Place<'tcx>) -> Place<'tcx> { + self.from[0].0.common_prefix(to) + } +} + +#[derive(Copy, Clone, PartialEq, Eq, Hash)] +pub enum CapabilityKind { + Write, + Exclusive, + /// [`CapabilityKind::Exclusive`] for everything not through a dereference, + /// [`CapabilityKind::Write`] for everything through a dereference. + ShallowExclusive, +} +impl Debug for CapabilityKind { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + match self { + CapabilityKind::Write => write!(f, "W"), + CapabilityKind::Exclusive => write!(f, "E"), + CapabilityKind::ShallowExclusive => write!(f, "e"), + } + } +} + +impl PartialOrd for CapabilityKind { + #[tracing::instrument(name = "CapabilityKind::partial_cmp", level = "trace", ret)] + fn partial_cmp(&self, other: &Self) -> Option { + if *self == *other { + return Some(Ordering::Equal); + } + match (self, other) { + // W < E, W < e + (CapabilityKind::Write, CapabilityKind::Exclusive) + | (CapabilityKind::ShallowExclusive, CapabilityKind::Exclusive) + | (CapabilityKind::Write, CapabilityKind::ShallowExclusive) => Some(Ordering::Less), + // E > W, e > W + (CapabilityKind::Exclusive, CapabilityKind::Write) + | (CapabilityKind::Exclusive, CapabilityKind::ShallowExclusive) + | (CapabilityKind::ShallowExclusive, CapabilityKind::Write) => Some(Ordering::Greater), + _ => None, + } + } +} + +impl CapabilityKind { + pub fn is_exclusive(self) -> bool { + matches!(self, CapabilityKind::Exclusive) + } + pub fn is_write(self) -> bool { + matches!(self, CapabilityKind::Write) + } + pub fn is_shallow_exclusive(self) -> bool { + matches!(self, CapabilityKind::ShallowExclusive) + } + pub fn minimum(self, other: Self) -> Option { + match self.partial_cmp(&other)? { + Ordering::Greater => Some(other), + _ => Some(self), + } + } +} diff --git a/mir-state-analysis/src/free_pcs/impl/triple.rs b/mir-state-analysis/src/free_pcs/impl/triple.rs new file mode 100644 index 00000000000..c995adf2df5 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/triple.rs @@ -0,0 +1,179 @@ +// © 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::free_pcs::{CapabilityKind, 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) { + if self.apply_pre_effect { + self.super_statement(statement, location); + return; + } + use StatementKind::*; + match &statement.kind { + Assign(box (place, rvalue)) => { + self.requires_write(*place); + let ensures = rvalue.capability(); + match ensures { + CapabilityKind::Exclusive => self.ensures_exclusive(*place), + CapabilityKind::ShallowExclusive => self.ensures_shallow_exclusive(*place), + _ => unreachable!(), + } + } + &FakeRead(box (_, place)) | &PlaceMention(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) { + if self.apply_pre_effect { + self.super_terminator(terminator, location); + return; + } + use TerminatorKind::*; + match &terminator.kind { + Goto { .. } + | SwitchInt { .. } + | UnwindResume + | UnwindTerminate(_) + | 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 local == RETURN_PLACE { + self.requires_exclusive(RETURN_PLACE); + } else if always_live.contains(local) { + self.requires_write(local); + } else { + self.requires_unalloc(local); + } + } + } + &Drop { place, .. } => { + self.requires_write(place); + self.ensures_write(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(_, _) + | ShallowInitBox(_, _) => {} + + &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::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), + &CopyForDeref(place) => self.requires_read(place), + } + } +} + +trait ProducesCapability { + fn capability(&self) -> CapabilityKind; +} + +impl ProducesCapability for Rvalue<'_> { + fn capability(&self) -> CapabilityKind { + use Rvalue::*; + match self { + Use(_) + | Repeat(_, _) + | Ref(_, _, _) + | ThreadLocalRef(_) + | AddressOf(_, _) + | Len(_) + | Cast(_, _, _) + | BinaryOp(_, _) + | CheckedBinaryOp(_, _) + | NullaryOp(_, _) + | UnaryOp(_, _) + | Discriminant(_) + | Aggregate(_, _) + | CopyForDeref(_) => CapabilityKind::Exclusive, + ShallowInitBox(_, _) => CapabilityKind::ShallowExclusive, + } + } +} diff --git a/mir-state-analysis/src/free_pcs/impl/update.rs b/mir-state-analysis/src/free_pcs/impl/update.rs new file mode 100644 index 00000000000..1e59d315ecb --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/update.rs @@ -0,0 +1,117 @@ +// © 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::{ + free_pcs::{CapabilityKind, CapabilityLocal, CapabilityProjections, Fpcs, RepackOp}, + utils::{LocalMutationIsAllowed, Place, PlaceOrdering, PlaceRepacker}, +}; +use std::fmt::Debug; + +impl<'tcx> Fpcs<'_, 'tcx> { + #[tracing::instrument(name = "Fpcs::requires_unalloc", level = "trace")] + pub(crate) fn requires_unalloc(&mut self, local: Local) { + assert!( + self.summary[local].is_unallocated(), + "local: {local:?}, fpcs: {self:?}\n" + ); + } + #[tracing::instrument(name = "Fpcs::requires_unalloc_or_uninit", level = "trace")] + pub(crate) fn requires_unalloc_or_uninit(&mut self, local: Local) { + if !self.summary[local].is_unallocated() { + self.requires_write(local) + } else { + self.repackings.push(RepackOp::IgnoreStorageDead(local)) + } + } + #[tracing::instrument(name = "Fpcs::requires_read", level = "trace")] + pub(crate) fn requires_read(&mut self, place: impl Into> + Debug) { + self.requires(place, CapabilityKind::Exclusive) + } + /// May obtain write _or_ exclusive, if one should only have write afterwards, + /// make sure to also call `ensures_write`! + #[tracing::instrument(name = "Fpcs::requires_write", level = "trace")] + pub(crate) fn requires_write(&mut self, place: impl Into> + Debug) { + let place = place.into(); + // Cannot get write on a shared ref + assert!(place + .is_mutable(LocalMutationIsAllowed::Yes, self.repacker) + .is_ok()); + self.requires(place, CapabilityKind::Write) + } + #[tracing::instrument(name = "Fpcs::requires_write", level = "trace")] + pub(crate) fn requires_exclusive(&mut self, place: impl Into> + Debug) { + let place = place.into(); + // Cannot get exclusive on a shared ref + assert!(!place.projects_shared_ref(self.repacker)); + self.requires(place, CapabilityKind::Exclusive) + } + fn requires(&mut self, place: impl Into>, 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]; + if cap.is_write() { + // Requires write should deinit an exclusive + cp.insert(place, cap); + if kind != cap { + self.repackings.push(RepackOp::Weaken(place, kind, cap)); + } + }; + 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>, cap: CapabilityKind) { + let place = place.into(); + let cp: &mut CapabilityProjections = self.summary[place.local].get_allocated_mut(); + cp.update_cap(place, cap); + } + pub(crate) fn ensures_exclusive(&mut self, place: impl Into>) { + self.ensures_alloc(place, CapabilityKind::Exclusive) + } + pub(crate) fn ensures_shallow_exclusive(&mut self, place: impl Into>) { + self.ensures_alloc(place, CapabilityKind::ShallowExclusive) + } + pub(crate) fn ensures_write(&mut self, place: impl Into>) { + let place = place.into(); + // Cannot get uninitialize behind a ref (actually drop does this) + assert!(place.can_deinit(self.repacker), "{place:?}"); + self.ensures_alloc(place, CapabilityKind::Write) + } +} + +impl<'tcx> CapabilityProjections<'tcx> { + pub(super) fn repack( + &mut self, + to: Place<'tcx>, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> Vec> { + let related = self.find_all_related(to, None); + match related.relation { + PlaceOrdering::Prefix => self.expand(related.get_only_from(), related.to, repacker), + PlaceOrdering::Equal => Vec::new(), + PlaceOrdering::Suffix => self.collapse(related.get_from(), related.to, repacker), + PlaceOrdering::Both => { + let cp = related.common_prefix(to); + // Collapse + let mut ops = self.collapse(related.get_from(), cp, repacker); + // Expand + let unpacks = self.expand(cp, related.to, repacker); + ops.extend(unpacks); + ops + } + } + } +} diff --git a/mir-state-analysis/src/free_pcs/mod.rs b/mir-state-analysis/src/free_pcs/mod.rs new file mode 100644 index 00000000000..fe388adbc52 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/mod.rs @@ -0,0 +1,13 @@ +// © 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/. + +mod check; +mod r#impl; +mod results; + +pub(crate) use check::*; +pub use r#impl::*; +pub use results::*; diff --git a/mir-state-analysis/src/free_pcs/results/cursor.rs b/mir-state-analysis/src/free_pcs/results/cursor.rs new file mode 100644 index 00000000000..26615a30c6f --- /dev/null +++ b/mir-state-analysis/src/free_pcs/results/cursor.rs @@ -0,0 +1,146 @@ +// © 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::{ + free_pcs::{ + engine::FreePlaceCapabilitySummary, join_semi_lattice::RepackingJoinSemiLattice, + CapabilitySummary, RepackOp, + }, + utils::PlaceRepacker, +}; + +type Cursor<'mir, 'tcx> = ResultsCursor<'mir, 'tcx, FreePlaceCapabilitySummary<'mir, 'tcx>>; + +pub struct FreePcsAnalysis<'mir, 'tcx> { + cursor: Cursor<'mir, 'tcx>, + curr_stmt: Option, + end_stmt: Option, +} + +impl<'mir, 'tcx> FreePcsAnalysis<'mir, 'tcx> { + pub(crate) fn new(cursor: Cursor<'mir, 'tcx>) -> Self { + Self { + cursor, + curr_stmt: None, + end_stmt: None, + } + } + + pub fn analysis_for_bb(&mut self, block: BasicBlock) { + self.cursor.seek_to_block_start(block); + let end_stmt = self + .cursor + .analysis() + .0 + .body() + .terminator_loc(block) + .successor_within_block(); + self.curr_stmt = Some(Location { + block, + statement_index: 0, + }); + self.end_stmt = Some(end_stmt); + } + + fn body(&self) -> &'mir Body<'tcx> { + self.cursor.analysis().0.body() + } + pub(crate) fn repacker(&mut self) -> PlaceRepacker<'mir, 'tcx> { + self.cursor.results().analysis.0 + } + + pub fn initial_state(&self) -> &CapabilitySummary<'tcx> { + &self.cursor.get().summary + } + pub fn next(&mut self, exp_loc: Location) -> FreePcsLocation<'tcx> { + let location = self.curr_stmt.unwrap(); + assert_eq!(location, exp_loc); + assert!(location < self.end_stmt.unwrap()); + self.curr_stmt = Some(location.successor_within_block()); + + self.cursor.seek_before_primary_effect(location); + let repacks_middle = self.cursor.get().repackings.clone(); + self.cursor.seek_after_primary_effect(location); + let state = self.cursor.get(); + FreePcsLocation { + location, + state: state.summary.clone(), + repacks: state.repackings.clone(), + repacks_middle, + } + } + pub fn terminator(&mut self) -> FreePcsTerminator<'tcx> { + let location = self.curr_stmt.unwrap(); + assert!(location == self.end_stmt.unwrap()); + self.curr_stmt = None; + self.end_stmt = None; + + // TODO: cleanup + let rp: PlaceRepacker = self.repacker(); + let state = self.cursor.get().clone(); + let block = &self.body()[location.block]; + let succs = block + .terminator() + .successors() + .map(|succ| { + // Get repacks + let to = self.cursor.results().entry_set_for_block(succ); + FreePcsLocation { + location: Location { + block: succ, + statement_index: 0, + }, + state: to.summary.clone(), + repacks: state.summary.bridge(&to.summary, rp), + repacks_middle: Vec::new(), + } + }) + .collect(); + FreePcsTerminator { succs } + } + + /// Recommened interface. + /// Does *not* require that one calls `analysis_for_bb` first + pub fn get_all_for_bb(&mut self, block: BasicBlock) -> FreePcsBasicBlock<'tcx> { + self.analysis_for_bb(block); + let mut statements = Vec::new(); + while self.curr_stmt.unwrap() != self.end_stmt.unwrap() { + let stmt = self.next(self.curr_stmt.unwrap()); + statements.push(stmt); + } + let terminator = self.terminator(); + FreePcsBasicBlock { + statements, + terminator, + } + } +} + +pub struct FreePcsBasicBlock<'tcx> { + pub statements: Vec>, + pub terminator: FreePcsTerminator<'tcx>, +} + +#[derive(Debug)] +pub struct FreePcsLocation<'tcx> { + pub location: Location, + /// Repacks before the statement + pub repacks: Vec>, + /// Repacks in the middle of the statement + pub repacks_middle: Vec>, + /// State after the statement + pub state: CapabilitySummary<'tcx>, +} + +#[derive(Debug)] +pub struct FreePcsTerminator<'tcx> { + pub succs: Vec>, +} diff --git a/mir-state-analysis/src/free_pcs/results/mod.rs b/mir-state-analysis/src/free_pcs/results/mod.rs new file mode 100644 index 00000000000..3d949c4f182 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/results/mod.rs @@ -0,0 +1,11 @@ +// © 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/. + +mod repacks; +mod cursor; + +pub use cursor::*; +pub use repacks::*; diff --git a/mir-state-analysis/src/free_pcs/results/repacks.rs b/mir-state-analysis/src/free_pcs/results/repacks.rs new file mode 100644 index 00000000000..c32c45f5555 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/results/repacks.rs @@ -0,0 +1,74 @@ +// © 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::{Display, Formatter, Result}; + +use prusti_rustc_interface::middle::mir::Local; + +use crate::{free_pcs::CapabilityKind, utils::Place}; + +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +pub enum RepackOp<'tcx> { + /// Rust will sometimes join two BasicBlocks where a local is live in one and dead in the other. + /// Our analysis will join these two into a state where the local is dead, and this Op marks the + /// edge from where it was live. + /// + /// This is not an issue in the MIR since it generally has a + /// [`mir::StatementKind::StorageDead`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.StorageDead) + /// right after the merge point, which is fine in Rust semantics, since + /// [`mir::StatementKind::StorageDead`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.StorageDead) + /// is a no-op if the local is already (conditionally) dead. + /// + /// This Op only appears for edges between basic blocks. It is often emitted for edges to panic + /// handling blocks, but can also appear in regular code for example in the MIR of + /// [this function](https://github.com/dtolnay/syn/blob/3da56a712abf7933b91954dbfb5708b452f88504/src/attr.rs#L623-L628). + StorageDead(Local), + /// This Op only appears within a BasicBlock and is attached to a + /// [`mir::StatementKind::StorageDead`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.StorageDead) + /// statement. We emit it for any such statement where the local may already be dead. We + /// guarantee to have inserted a [`RepackOp::StorageDead`] before this Op so that one can + /// safely ignore the statement this is attached to. + IgnoreStorageDead(Local), + /// Instructs that the current capability to the place (first [`CapabilityKind`]) should + /// be weakened to the second given capability. We guarantee that `_.1 > _.2`. + /// + /// This Op is used prior to a [`RepackOp::Collapse`] to ensure that all packed up places have + /// the same capability. It can also appear at basic block join points, where one branch has + /// a weaker capability than the other. + Weaken(Place<'tcx>, CapabilityKind, CapabilityKind), + /// Instructs that one should unpack the first place with the capability. + /// We guarantee that the current state holds exactly the given capability for the given place. + /// The second place is the guide, denoting e.g. the enum variant to unpack to. One can use + /// [`Place::expand_one_level(_.0, _.1, ..)`](Place::expand_one_level) to get the set of all + /// places (except as noted in the documentation for that fn) which will be obtained by unpacking. + /// + /// Until rust-lang/rust#21232 lands, we guarantee that this will only have + /// [`CapabilityKind::Exclusive`]. + Expand(Place<'tcx>, Place<'tcx>, CapabilityKind), + /// Instructs that one should pack up to the given (first) place with the given capability. + /// The second place is the guide, denoting e.g. the enum variant to pack from. One can use + /// [`Place::expand_one_level(_.0, _.1, ..)`](Place::expand_one_level) to get the set of all + /// places which should be packed up. We guarantee that the current state holds exactly the + /// given capability for all places in this set. + Collapse(Place<'tcx>, Place<'tcx>, CapabilityKind), + /// TODO + DerefShallowInit(Place<'tcx>, Place<'tcx>), +} + +impl Display for RepackOp<'_> { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + match self { + RepackOp::StorageDead(place) => write!(f, "StorageDead({place:?})"), + RepackOp::IgnoreStorageDead(_) => write!(f, "IgnoreSD"), + RepackOp::Weaken(place, _, to) => { + write!(f, "Weaken({place:?}, {to:?})") + } + RepackOp::Collapse(to, _, kind) => write!(f, "CollapseTo({to:?}, {kind:?})"), + RepackOp::Expand(from, _, kind) => write!(f, "Expand({from:?}, {kind:?})"), + RepackOp::DerefShallowInit(from, _) => write!(f, "DerefShallowInit({from:?})"), + } + } +} diff --git a/mir-state-analysis/src/lib.rs b/mir-state-analysis/src/lib.rs new file mode 100644 index 00000000000..cd778866e60 --- /dev/null +++ b/mir-state-analysis/src/lib.rs @@ -0,0 +1,34 @@ +// © 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, hash_extract_if, extract_if)] + +pub mod free_pcs; +pub mod utils; + +use prusti_rustc_interface::{ + dataflow::Analysis, + middle::{mir::Body, ty::TyCtxt}, +}; + +#[tracing::instrument(name = "run_free_pcs", level = "debug", skip(tcx))] +pub fn run_free_pcs<'mir, 'tcx>( + mir: &'mir Body<'tcx>, + tcx: TyCtxt<'tcx>, +) -> free_pcs::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(); + free_pcs::FreePcsAnalysis::new(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); +} diff --git a/mir-state-analysis/src/utils/mod.rs b/mir-state-analysis/src/utils/mod.rs new file mode 100644 index 00000000000..fb02d7b16ab --- /dev/null +++ b/mir-state-analysis/src/utils/mod.rs @@ -0,0 +1,14 @@ +// © 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/. + +pub mod place; +pub(crate) mod repacker; +mod mutable; +mod root_place; + +pub use mutable::*; +pub use place::*; +pub use repacker::*; diff --git a/mir-state-analysis/src/utils/mutable.rs b/mir-state-analysis/src/utils/mutable.rs new file mode 100644 index 00000000000..45e7bafa315 --- /dev/null +++ b/mir-state-analysis/src/utils/mutable.rs @@ -0,0 +1,240 @@ +// © 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, + middle::{ + mir::{Mutability, ProjectionElem}, + ty::{CapturedPlace, TyKind, UpvarCapture}, + }, + target::abi::FieldIdx, +}; + +use super::{root_place::RootPlace, Place, PlaceRepacker}; + +struct Upvar<'tcx> { + pub(crate) place: CapturedPlace<'tcx>, + pub(crate) by_ref: bool, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum LocalMutationIsAllowed { + Yes, + ExceptUpvars, + No, +} + +impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { + fn upvars(self) -> Vec> { + let def = self.body().source.def_id().expect_local(); + self.tcx + .closure_captures(def) + .iter() + .map(|&captured_place| { + let capture = captured_place.info.capture_kind; + let by_ref = match capture { + UpvarCapture::ByValue => false, + UpvarCapture::ByRef(..) => true, + }; + Upvar { + place: captured_place.clone(), + by_ref, + } + }) + .collect() + } +} + +impl<'tcx> Place<'tcx> { + pub fn is_mutable( + self, + is_local_mutation_allowed: LocalMutationIsAllowed, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> Result, Self> { + let upvars = repacker.upvars(); + self.is_mutable_helper(is_local_mutation_allowed, &upvars, repacker) + } + + /// Whether this value can be written or borrowed mutably. + /// Returns the root place if the place passed in is a projection. + fn is_mutable_helper( + self, + is_local_mutation_allowed: LocalMutationIsAllowed, + upvars: &[Upvar<'tcx>], + repacker: PlaceRepacker<'_, 'tcx>, + ) -> Result, Self> { + match self.last_projection() { + None => { + let local = &repacker.body().local_decls[self.local]; + match local.mutability { + Mutability::Not => match is_local_mutation_allowed { + LocalMutationIsAllowed::Yes => Ok(RootPlace { + place: self, + is_local_mutation_allowed: LocalMutationIsAllowed::Yes, + }), + LocalMutationIsAllowed::ExceptUpvars => Ok(RootPlace { + place: self, + is_local_mutation_allowed: LocalMutationIsAllowed::ExceptUpvars, + }), + LocalMutationIsAllowed::No => Err(self), + }, + Mutability::Mut => Ok(RootPlace { + place: self, + is_local_mutation_allowed, + }), + } + } + Some((place_base, elem)) => { + match elem { + ProjectionElem::Deref => { + let base_ty = place_base.ty(repacker).ty; + + // Check the kind of deref to decide + match base_ty.kind() { + TyKind::Ref(_, _, mutbl) => { + match mutbl { + // Shared borrowed data is never mutable + hir::Mutability::Not => Err(self), + // Mutably borrowed data is mutable, but only if we have a + // unique path to the `&mut` + hir::Mutability::Mut => { + let mode = match self + .is_upvar_field_projection(upvars, repacker) + { + Some(field) if upvars[field.index()].by_ref => { + is_local_mutation_allowed + } + _ => LocalMutationIsAllowed::Yes, + }; + + place_base.is_mutable_helper(mode, upvars, repacker) + } + } + } + TyKind::RawPtr(tnm) => { + match tnm.mutbl { + // `*const` raw pointers are not mutable + hir::Mutability::Not => Err(self), + // `*mut` raw pointers are always mutable, regardless of + // context. The users have to check by themselves. + hir::Mutability::Mut => Ok(RootPlace { + place: self, + is_local_mutation_allowed, + }), + } + } + // `Box` owns its content, so mutable if its location is mutable + _ if base_ty.is_box() => place_base.is_mutable_helper( + is_local_mutation_allowed, + upvars, + repacker, + ), + // Deref should only be for reference, pointers or boxes + _ => panic!("Deref of unexpected type: {:?}", base_ty), + } + } + // All other projections are owned by their base path, so mutable if + // base path is mutable + ProjectionElem::Field(..) + | ProjectionElem::Index(..) + | ProjectionElem::ConstantIndex { .. } + | ProjectionElem::Subslice { .. } + | ProjectionElem::OpaqueCast { .. } + | ProjectionElem::Downcast(..) => { + let upvar_field_projection = + self.is_upvar_field_projection(upvars, repacker); + if let Some(field) = upvar_field_projection { + let upvar = &upvars[field.index()]; + match (upvar.place.mutability, is_local_mutation_allowed) { + ( + Mutability::Not, + LocalMutationIsAllowed::No + | LocalMutationIsAllowed::ExceptUpvars, + ) => Err(self), + (Mutability::Not, LocalMutationIsAllowed::Yes) + | (Mutability::Mut, _) => { + // Subtle: this is an upvar + // reference, so it looks like + // `self.foo` -- we want to double + // check that the location `*self` + // is mutable (i.e., this is not a + // `Fn` closure). But if that + // check succeeds, we want to + // *blame* the mutability on + // `place` (that is, + // `self.foo`). This is used to + // propagate the info about + // whether mutability declarations + // are used outwards, so that we register + // the outer variable as mutable. Otherwise a + // test like this fails to record the `mut` + // as needed: + // + // ``` + // fn foo(_f: F) { } + // fn main() { + // let var = Vec::new(); + // foo(move || { + // var.push(1); + // }); + // } + // ``` + let _ = place_base.is_mutable_helper( + is_local_mutation_allowed, + upvars, + repacker, + )?; + Ok(RootPlace { + place: self, + is_local_mutation_allowed, + }) + } + } + } else { + place_base.is_mutable_helper( + is_local_mutation_allowed, + upvars, + repacker, + ) + } + } + } + } + } + } + + /// If `place` is a field projection, and the field is being projected from a closure type, + /// then returns the index of the field being projected. Note that this closure will always + /// be `self` in the current MIR, because that is the only time we directly access the fields + /// of a closure type. + fn is_upvar_field_projection( + self, + upvars: &[Upvar<'tcx>], + repacker: PlaceRepacker<'_, 'tcx>, + ) -> Option { + let mut place_ref = *self; + let mut by_ref = false; + + if let Some((place_base, ProjectionElem::Deref)) = place_ref.last_projection() { + place_ref = place_base; + by_ref = true; + } + + match place_ref.last_projection() { + Some((place_base, ProjectionElem::Field(field, _ty))) => { + let base_ty = place_base.ty(repacker.body(), repacker.tcx).ty; + if (base_ty.is_closure() || base_ty.is_generator()) + && (!by_ref || upvars[field.index()].by_ref) + { + Some(field) + } else { + None + } + } + _ => None, + } + } +} diff --git a/mir-state-analysis/src/utils/place.rs b/mir-state-analysis/src/utils/place.rs new file mode 100644 index 00000000000..64cb9dc2b48 --- /dev/null +++ b/mir-state-analysis/src/utils/place.rs @@ -0,0 +1,403 @@ +// © 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}, + hash::{Hash, Hasher}, + mem::discriminant, +}; + +use derive_more::{Deref, DerefMut}; + +use prusti_rustc_interface::middle::mir::{ + Local, Place as MirPlace, PlaceElem, PlaceRef, ProjectionElem, +}; + +// #[derive(Clone, Copy, Deref, DerefMut, Hash, PartialEq, Eq)] +// pub struct RootPlace<'tcx>(Place<'tcx>); +// impl<'tcx> RootPlace<'tcx> { +// pub(super) fn new(place: Place<'tcx>) -> Self { +// assert!(place.projection.last().copied().map(Self::is_indirect).unwrap_or(true)); +// Self(place) +// } + +// pub fn is_indirect(p: ProjectionElem) -> bool { +// match p { +// ProjectionElem::Deref => true, + +// ProjectionElem::Field(_, _) +// | ProjectionElem::Index(_) +// | ProjectionElem::OpaqueCast(_) +// | ProjectionElem::ConstantIndex { .. } +// | ProjectionElem::Subslice { .. } +// | ProjectionElem::Downcast(_, _) => false, +// } +// } +// } +// impl Debug for RootPlace<'_> { +// fn fmt(&self, fmt: &mut Formatter) -> Result { +// self.0.fmt(fmt) +// } +// } +// impl From for RootPlace<'_> { +// fn from(local: Local) -> Self { +// Self(local.into()) +// } +// } + +#[derive(Clone, Copy, Deref, DerefMut)] +pub struct Place<'tcx>(PlaceRef<'tcx>); + +impl<'tcx> Place<'tcx> { + pub(crate) fn new(local: Local, projection: &'tcx [PlaceElem<'tcx>]) -> Self { + Self(PlaceRef { local, projection }) + } + + pub(crate) fn compare_projections( + self, + other: Self, + ) -> impl Iterator, PlaceElem<'tcx>)> { + let left = self.projection.iter().copied(); + let right = other.projection.iter().copied(); + left.zip(right).map(|(e1, e2)| (elem_eq((e1, e2)), e1, e2)) + } + + /// Check if the place `left` is a prefix of `right` or vice versa. For example: + /// + /// + `partial_cmp(x.f, y.f) == None` + /// + `partial_cmp(x.f, x.g) == None` + /// + `partial_cmp(x.f, x.f) == Some(Equal)` + /// + `partial_cmp(x.f.g, x.f) == Some(Suffix)` + /// + `partial_cmp(x.f, x.f.g) == Some(Prefix)` + /// + `partial_cmp(x as None, x as Some.0) == Some(Both)` + /// + /// The ultimate question this answers is: are the two places mutually + /// exclusive (i.e. can we have both or not)? + /// For example, all of the following are mutually exclusive: + /// - `x` and `x.f` + /// - `(x as Ok).0` and `(x as Err).0` + /// - `x[_1]` and `x[_2]` + /// - `x[2 of 11]` and `x[5 of 14]` + /// But the following are not: + /// - `x` and `y` + /// - `x.f` and `x.g.h` + /// - `x[3 of 6]` and `x[4 of 6]` + #[tracing::instrument(level = "trace", ret)] + pub(crate) fn partial_cmp(self, right: Self) -> Option { + if self.local != right.local { + return None; + } + let diff = self.compare_projections(right).find(|(eq, _, _)| !eq); + if let Some((_, left, right)) = diff { + use ProjectionElem::*; + fn is_index(elem: PlaceElem<'_>) -> bool { + matches!(elem, Index(_) | ConstantIndex { .. } | Subslice { .. }) + } + match (left, right) { + (Field(..), Field(..)) => None, + ( + ConstantIndex { + min_length: l, + from_end: lfe, + .. + }, + ConstantIndex { + min_length: r, + from_end: rfe, + .. + }, + ) if r == l && lfe == rfe => None, + (Downcast(_, _), Downcast(_, _)) | (OpaqueCast(_), OpaqueCast(_)) => { + Some(PlaceOrdering::Both) + } + (left, right) if is_index(left) && is_index(right) => Some(PlaceOrdering::Both), + diff => unreachable!("Unexpected diff: {diff:?}"), + } + } else { + Some(self.projection.len().cmp(&right.projection.len()).into()) + } + } + + /// Check if the place `self` is a prefix of `place`. For example: + /// + /// + `is_prefix(x.f, x.f) == true` + /// + `is_prefix(x.f, x.f.g) == true` + /// + `is_prefix(x.f.g, x.f) == false` + pub(crate) fn is_prefix(self, place: Self) -> bool { + Self::partial_cmp(self, place) + .map(|o| o == PlaceOrdering::Equal || o == PlaceOrdering::Prefix) + .unwrap_or(false) + } + + /// Check if the place `self` is an exact prefix of `place`. For example: + /// + /// + `is_prefix(x.f, x.f) == false` + /// + `is_prefix(x.f, x.f.g) == true` + /// + `is_prefix(x.f, x.f.g.h) == false` + pub(crate) fn is_prefix_exact(self, place: Self) -> bool { + self.0.projection.len() + 1 == place.0.projection.len() + && Self::partial_cmp(self, place) + .map(|o| o == PlaceOrdering::Prefix) + .unwrap_or(false) + } + + /// Check if the place `self` is a prefix of `place` or vice versa. For example: + /// + /// + `is_prefix(x.f, x.f) == None` + /// + `is_prefix(x.f, x.f.g) == Some(true)` + /// + `is_prefix(x.f.g, x.f) == Some(false)` + /// + `is_prefix(x.g, x.f) == None` + pub(crate) fn either_prefix(self, place: Self) -> Option { + Self::partial_cmp(self, place).and_then(|o| { + if o == PlaceOrdering::Prefix { + Some(true) + } else if o == PlaceOrdering::Suffix { + Some(false) + } else { + None + } + }) + } + + /// Returns `true` if either of the places can reach the other + /// with a series of expand/collapse operations. Note that + /// both operations are allowed and so e.g. + /// related_to(`_1[_4]`, `_1[_3]`) == true + pub fn related_to(self, right: Self) -> bool { + self.partial_cmp(right).is_some() + } + + pub fn projection_contains_deref(self) -> bool { + self.projection + .iter() + .any(|proj| matches!(proj, ProjectionElem::Deref)) + } + + #[tracing::instrument(level = "debug", ret, fields(lp = ?self.projection, rp = ?other.projection))] + pub fn common_prefix(self, other: Self) -> Self { + assert_eq!(self.local, other.local); + + let max_len = std::cmp::min(self.projection.len(), other.projection.len()); + let common_prefix = self + .compare_projections(other) + .position(|(eq, _, _)| !eq) + .unwrap_or(max_len); + Self::new(self.local, &self.projection[..common_prefix]) + } + + #[tracing::instrument(level = "info", ret)] + pub fn joinable_to(self, to: Self) -> Self { + assert!(self.is_prefix(to)); + let diff = to.projection.len() - self.projection.len(); + let to_proj = self.projection.len() + + to.projection[self.projection.len()..] + .iter() + .position(|p| !matches!(p, ProjectionElem::Deref | ProjectionElem::Field(..))) + .unwrap_or(diff); + Self::new(self.local, &to.projection[..to_proj]) + } + + pub fn last_projection(self) -> Option<(Self, PlaceElem<'tcx>)> { + self.0 + .last_projection() + .map(|(place, proj)| (place.into(), proj)) + } +} + +impl Debug for Place<'_> { + fn fmt(&self, fmt: &mut Formatter) -> Result { + for elem in self.projection.iter().rev() { + match elem { + ProjectionElem::OpaqueCast(_) | ProjectionElem::Downcast(_, _) => { + write!(fmt, "(").unwrap(); + } + ProjectionElem::Deref => { + write!(fmt, "(*").unwrap(); + } + ProjectionElem::Field(_, _) + | ProjectionElem::Index(_) + | ProjectionElem::ConstantIndex { .. } + | ProjectionElem::Subslice { .. } => {} + } + } + + write!(fmt, "{:?}", self.local)?; + + for &elem in self.projection.iter() { + match elem { + ProjectionElem::OpaqueCast(ty) => { + write!(fmt, "@{ty})")?; + } + ProjectionElem::Downcast(Some(name), _index) => { + write!(fmt, "@{name})")?; + } + ProjectionElem::Downcast(None, index) => { + write!(fmt, "@variant#{index:?})")?; + } + ProjectionElem::Deref => { + write!(fmt, ")")?; + } + ProjectionElem::Field(field, _ty) => { + write!(fmt, ".{:?}", field.index())?; + } + ProjectionElem::Index(ref index) => { + write!(fmt, "[{index:?}]")?; + } + ProjectionElem::ConstantIndex { + offset, + min_length, + from_end: false, + } => { + write!(fmt, "[{offset:?} of {min_length:?}]")?; + } + ProjectionElem::ConstantIndex { + offset, + min_length, + from_end: true, + } => { + write!(fmt, "[-{offset:?} of {min_length:?}]")?; + } + ProjectionElem::Subslice { + from, + to: 0, + from_end: true, + } => { + write!(fmt, "[{from:?}:]")?; + } + ProjectionElem::Subslice { + from: 0, + to, + from_end: true, + } => { + write!(fmt, "[:-{to:?}]")?; + } + ProjectionElem::Subslice { + from, + to, + from_end: true, + } => { + write!(fmt, "[{from:?}:-{to:?}]")?; + } + ProjectionElem::Subslice { + from, + to, + from_end: false, + } => { + write!(fmt, "[{from:?}..{to:?}]")?; + } + } + } + + Ok(()) + } +} + +fn elem_eq<'tcx>(to_cmp: (PlaceElem<'tcx>, PlaceElem<'tcx>)) -> bool { + use ProjectionElem::*; + match to_cmp { + (Field(left, _), Field(right, _)) => left == right, + (Downcast(_, left), Downcast(_, right)) => left == right, + (left, right) => left == right, + } +} + +impl PartialEq for Place<'_> { + fn eq(&self, other: &Self) -> bool { + self.local == other.local + && self.projection.len() == other.projection.len() + && self.compare_projections(*other).all(|(eq, _, _)| eq) + } +} +impl Eq for Place<'_> {} + +impl Hash for Place<'_> { + fn hash(&self, state: &mut H) { + self.0.local.hash(state); + let projection = self.0.projection; + for &pe in projection { + match pe { + ProjectionElem::Field(field, _) => { + discriminant(&pe).hash(state); + field.hash(state); + } + ProjectionElem::Downcast(_, variant) => { + discriminant(&pe).hash(state); + variant.hash(state); + } + _ => pe.hash(state), + } + } + } +} + +// impl<'tcx, T: Into>> From for Place<'tcx> { +// fn from(value: T) -> Self { +// Self(value.into()) +// } +// } +impl<'tcx> From> for Place<'tcx> { + fn from(value: PlaceRef<'tcx>) -> Self { + Self(value) + } +} +impl<'tcx> From> for Place<'tcx> { + fn from(value: MirPlace<'tcx>) -> Self { + Self(value.as_ref()) + } +} +impl<'tcx> From for Place<'tcx> { + fn from(value: Local) -> Self { + MirPlace::from(value).into() + } +} + +#[derive(Copy, Clone, Debug, PartialEq, Eq)] +pub enum PlaceOrdering { + // For example `x.f` to `x.f.g`. + Prefix, + // For example `x.f` and `x.f`. + Equal, + // For example `x.f.g` to `x.f`. + Suffix, + // For example `x[a]` and `x[b]` or `x as None` and `x as Some`. + Both, +} + +impl PlaceOrdering { + pub fn is_eq(self) -> bool { + matches!(self, PlaceOrdering::Equal) + } + pub fn is_prefix(self) -> bool { + matches!(self, PlaceOrdering::Prefix) + } + pub fn is_suffix(self) -> bool { + matches!(self, PlaceOrdering::Suffix) + } + pub fn is_both(self) -> bool { + matches!(self, PlaceOrdering::Both) + } +} + +impl From for PlaceOrdering { + fn from(ordering: Ordering) -> Self { + match ordering { + Ordering::Less => PlaceOrdering::Prefix, + Ordering::Equal => PlaceOrdering::Equal, + Ordering::Greater => PlaceOrdering::Suffix, + } + } +} +impl From for Option { + fn from(ordering: PlaceOrdering) -> Self { + match ordering { + PlaceOrdering::Prefix => Some(Ordering::Less), + PlaceOrdering::Equal => Some(Ordering::Equal), + PlaceOrdering::Suffix => Some(Ordering::Greater), + PlaceOrdering::Both => None, + } + } +} diff --git a/mir-state-analysis/src/utils/repacker.rs b/mir-state-analysis/src/utils/repacker.rs new file mode 100644 index 00000000000..2bf86bdec2a --- /dev/null +++ b/mir-state-analysis/src/utils/repacker.rs @@ -0,0 +1,397 @@ +// © 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, + dataflow::storage, + index::bit_set::BitSet, + middle::{ + mir::{ + tcx::PlaceTy, Body, HasLocalDecls, Local, Mutability, Place as MirPlace, PlaceRef, + ProjectionElem, + }, + ty::{TyCtxt, TyKind}, + }, + target::abi::FieldIdx, +}; + +use super::Place; + +#[derive(Debug, Clone, Copy)] +pub enum ProjectionRefKind { + Ref(Mutability), + RawPtr(Mutability), + Box, + Other, +} +impl ProjectionRefKind { + pub fn is_ref(self) -> bool { + matches!(self, ProjectionRefKind::Ref(_)) + } + pub fn is_raw_ptr(self) -> bool { + matches!(self, ProjectionRefKind::RawPtr(_)) + } + pub fn is_box(self) -> bool { + matches!(self, ProjectionRefKind::Box) + } + pub fn is_deref(self) -> bool { + self.is_ref() || self.is_raw_ptr() || self.is_box() + } + pub fn is_shared_ref(self) -> bool { + matches!(self, ProjectionRefKind::Ref(Mutability::Not)) + } +} + +#[derive(Copy, Clone)] +// TODO: modified version of fns taken from `prusti-interface/src/utils.rs`; deduplicate +pub struct PlaceRepacker<'a, 'tcx: 'a> { + pub(super) mir: &'a Body<'tcx>, + pub(super) tcx: TyCtxt<'tcx>, +} + +impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { + pub fn new(mir: &'a Body<'tcx>, tcx: TyCtxt<'tcx>) -> Self { + Self { mir, tcx } + } + + pub fn local_count(self) -> usize { + self.mir.local_decls().len() + } + + pub fn always_live_locals(self) -> BitSet { + storage::always_storage_live_locals(self.mir) + } + + pub fn body(self) -> &'a Body<'tcx> { + self.mir + } +} + +impl<'tcx> Place<'tcx> { + pub fn to_rust_place(self, repacker: PlaceRepacker<'_, 'tcx>) -> MirPlace<'tcx> { + MirPlace { + local: self.local, + projection: repacker.tcx.mk_place_elems(self.projection), + } + } + + /// Subtract the `to` place from the `self` place. The + /// subtraction is defined as set minus between `self` place replaced + /// with a set of places that are unrolled up to the same level as + /// `to` and the singleton `to` set. For example, + /// `expand(x.f, x.f.g.h)` is performed by unrolling `x.f` into + /// `{x.g, x.h, x.f.f, x.f.h, x.f.g.f, x.f.g.g, x.f.g.h}` and + /// subtracting `{x.f.g.h}` from it, which results into (`{x.f, x.f.g}`, `{x.g, x.h, + /// x.f.f, x.f.h, x.f.g.f, x.f.g.g}`). The first vector contains the chain of + /// places that were expanded along with the target to of each expansion. + #[tracing::instrument(level = "trace", skip(repacker), ret)] + pub fn expand( + mut self, + to: Self, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> (Vec<(Self, Self, ProjectionRefKind)>, Vec) { + assert!( + self.is_prefix(to), + "The minuend ({self:?}) must be the prefix of the subtrahend ({to:?})." + ); + let mut place_set = Vec::new(); + let mut expanded = Vec::new(); + while self.projection.len() < to.projection.len() { + let (new_minuend, places, kind) = self.expand_one_level(to, repacker); + expanded.push((self, new_minuend, kind)); + place_set.extend(places); + self = new_minuend; + } + (expanded, place_set) + } + + /// Try to collapse all places in `from` by following the + /// `guide_place`. This function is basically the reverse of + /// `expand`. + #[tracing::instrument(level = "trace", skip(repacker), ret)] + pub fn collapse( + self, + from: &mut FxHashSet, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> Vec<(Self, Self, ProjectionRefKind)> { + let mut collapsed = Vec::new(); + let mut guide_places = vec![self]; + while let Some(guide_place) = guide_places.pop() { + if !from.remove(&guide_place) { + let expand_guide = *from + .iter() + .find(|p| guide_place.is_prefix(**p)) + .unwrap_or_else(|| { + panic!( + "The `from` set didn't contain all \ + the places required to construct the \ + `guide_place`. Currently tried to find \ + `{guide_place:?}` in `{from:?}`." + ) + }); + let (expanded, new_places) = guide_place.expand(expand_guide, repacker); + // Doing `collapsed.extend(expanded)` would result in a reversed order. + // Could also change this to `collapsed.push(expanded)` and return Vec>. + collapsed.extend(expanded); + guide_places.extend(new_places); + from.remove(&expand_guide); + } + } + collapsed.reverse(); + collapsed + } + + /// Expand `self` one level down by following the `guide_place`. + /// Returns the new `self` and a vector containing other places that + /// could have resulted from the expansion. Note: this vector is always + /// incomplete when projecting with `Index` or `Subslice` and also when + /// projecting a slice type with `ConstantIndex`! + #[tracing::instrument(level = "trace", skip(repacker), ret)] + pub fn expand_one_level( + self, + guide_place: Self, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> (Self, Vec, ProjectionRefKind) { + let index = self.projection.len(); + let new_projection = repacker.tcx.mk_place_elems_from_iter( + self.projection + .iter() + .copied() + .chain([guide_place.projection[index]]), + ); + let new_current_place = Place::new(self.local, new_projection); + let (other_places, kind) = match guide_place.projection[index] { + ProjectionElem::Field(projected_field, _field_ty) => { + let other_places = self.expand_field(Some(projected_field.index()), repacker); + (other_places, ProjectionRefKind::Other) + } + ProjectionElem::ConstantIndex { + offset, + min_length, + from_end, + } => { + let range = if from_end { + 1..min_length + 1 + } else { + 0..min_length + }; + assert!(range.contains(&offset)); + let other_places = range + .filter(|&i| i != offset) + .map(|i| { + repacker + .tcx + .mk_place_elem( + self.to_rust_place(repacker), + ProjectionElem::ConstantIndex { + offset: i, + min_length, + from_end, + }, + ) + .into() + }) + .collect(); + (other_places, ProjectionRefKind::Other) + } + ProjectionElem::Deref => { + let typ = self.ty(repacker); + let kind = match typ.ty.kind() { + TyKind::Ref(_, _, mutbl) => ProjectionRefKind::Ref(*mutbl), + TyKind::RawPtr(ptr) => ProjectionRefKind::RawPtr(ptr.mutbl), + _ if typ.ty.is_box() => ProjectionRefKind::Box, + _ => unreachable!(), + }; + (Vec::new(), kind) + } + ProjectionElem::Index(..) + | ProjectionElem::Subslice { .. } + | ProjectionElem::Downcast(..) + | ProjectionElem::OpaqueCast(..) => (Vec::new(), ProjectionRefKind::Other), + }; + (new_current_place, other_places, kind) + } + + /// Expands a place `x.f.g` of type struct into a vector of places for + /// each of the struct's fields `{x.f.g.f, x.f.g.g, x.f.g.h}`. If + /// `without_field` is not `None`, then omits that field from the final + /// vector. + pub fn expand_field( + self, + without_field: Option, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> Vec { + let mut places = Vec::new(); + let typ = self.ty(repacker); + if !matches!(typ.ty.kind(), TyKind::Adt(..)) { + assert!( + typ.variant_index.is_none(), + "We have assumed that only enums can have variant_index set. Got {typ:?}." + ); + } + match typ.ty.kind() { + TyKind::Adt(def, substs) => { + let variant = typ + .variant_index + .map(|i| def.variant(i)) + .unwrap_or_else(|| def.non_enum_variant()); + for (index, field_def) in variant.fields.iter().enumerate() { + if Some(index) != without_field { + let field = FieldIdx::from_usize(index); + let field_place = repacker.tcx.mk_place_field( + self.to_rust_place(repacker), + field, + field_def.ty(repacker.tcx, substs), + ); + places.push(field_place.into()); + } + } + } + TyKind::Tuple(slice) => { + for (index, arg) in slice.iter().enumerate() { + if Some(index) != without_field { + let field = FieldIdx::from_usize(index); + let field_place = + repacker + .tcx + .mk_place_field(self.to_rust_place(repacker), field, arg); + places.push(field_place.into()); + } + } + } + TyKind::Closure(_, substs) => { + for (index, subst_ty) in substs.as_closure().upvar_tys().iter().enumerate() { + if Some(index) != without_field { + let field = FieldIdx::from_usize(index); + let field_place = repacker.tcx.mk_place_field( + self.to_rust_place(repacker), + field, + subst_ty, + ); + places.push(field_place.into()); + } + } + } + TyKind::Generator(_, substs, _) => { + for (index, subst_ty) in substs.as_generator().upvar_tys().iter().enumerate() { + if Some(index) != without_field { + let field = FieldIdx::from_usize(index); + let field_place = repacker.tcx.mk_place_field( + self.to_rust_place(repacker), + field, + subst_ty, + ); + places.push(field_place.into()); + } + } + } + ty => unreachable!("ty={:?}", ty), + } + places + } + + // /// Pop the last projection from the place and return the new place with the popped element. + // pub fn pop_one_level(self, place: Place<'tcx>) -> (PlaceElem<'tcx>, Place<'tcx>) { + // assert!(place.projection.len() > 0); + // let last_index = place.projection.len() - 1; + // let projection = self.tcx.intern_place_elems(&place.projection[..last_index]); + // ( + // place.projection[last_index], + // Place::new(place.local, projection), + // ) + // } +} + +// impl<'tcx> RootPlace<'tcx> { +// pub fn get_parent(self, repacker: PlaceRepacker<'_, 'tcx>) -> Place<'tcx> { +// assert!(self.projection.len() > 0); +// let idx = self.projection.len() - 1; +// let projection = repacker.tcx.intern_place_elems(&self.projection[..idx]); +// Place::new(self.local, projection) +// } +// } + +impl<'tcx> Place<'tcx> { + // pub fn get_root(self, repacker: PlaceRepacker<'_, 'tcx>) -> RootPlace<'tcx> { + // if let Some(idx) = self.projection.iter().rev().position(RootPlace::is_indirect) { + // let idx = self.projection.len() - idx; + // let projection = repacker.tcx.intern_place_elems(&self.projection[..idx]); + // let new = Self::new(self.local, projection); + // RootPlace::new(new) + // } else { + // RootPlace::new(self.local.into()) + // } + // } + + pub fn ty(self, repacker: PlaceRepacker<'_, 'tcx>) -> PlaceTy<'tcx> { + PlaceRef::ty(&self, repacker.mir, repacker.tcx) + } + + /// Should only be called on a `Place` obtained from `RootPlace::get_parent`. + pub fn get_ref_mutability(self, repacker: PlaceRepacker<'_, 'tcx>) -> Mutability { + let typ = self.ty(repacker); + if let TyKind::Ref(_, _, mutability) = typ.ty.kind() { + *mutability + } else { + unreachable!("get_ref_mutability called on non-ref type: {:?}", typ.ty); + } + } + + pub fn projects_shared_ref(self, repacker: PlaceRepacker<'_, 'tcx>) -> bool { + self.projects_ty( + |typ| { + typ.ty + .ref_mutability() + .map(|m| m.is_not()) + .unwrap_or_default() + }, + repacker, + ) + .is_some() + } + + #[tracing::instrument(name = "Place::projects_ptr", level = "trace", skip(repacker), ret)] + pub fn projects_ptr(self, repacker: PlaceRepacker<'_, 'tcx>) -> Option> { + self.projects_ty( + |typ| typ.ty.is_ref() || typ.ty.is_box() || typ.ty.is_unsafe_ptr(), + repacker, + ) + } + + pub fn can_deinit(self, repacker: PlaceRepacker<'_, 'tcx>) -> bool { + let mut projects_shared_ref = false; + self.projects_ty( + |typ| { + projects_shared_ref = projects_shared_ref + || typ + .ty + .ref_mutability() + .map(|m| m.is_not()) + .unwrap_or_default(); + projects_shared_ref = projects_shared_ref && !typ.ty.is_unsafe_ptr(); + false + }, + repacker, + ); + !projects_shared_ref + } + + pub fn projects_ty( + self, + mut predicate: impl FnMut(PlaceTy<'tcx>) -> bool, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> Option> { + let mut typ = PlaceTy::from_ty(repacker.mir.local_decls()[self.local].ty); + for (idx, elem) in self.projection.iter().enumerate() { + if predicate(typ) { + let projection = repacker.tcx.mk_place_elems(&self.projection[0..idx]); + return Some(Self::new(self.local, projection)); + } + typ = typ.projection_ty(repacker.tcx, *elem); + } + None + } +} diff --git a/mir-state-analysis/src/utils/root_place.rs b/mir-state-analysis/src/utils/root_place.rs new file mode 100644 index 00000000000..5a3d7f0912e --- /dev/null +++ b/mir-state-analysis/src/utils/root_place.rs @@ -0,0 +1,17 @@ +// © 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 derive_more::{Deref, DerefMut}; + +use super::{mutable::LocalMutationIsAllowed, Place}; + +#[derive(Debug, Clone, Copy, Deref, DerefMut)] +pub struct RootPlace<'tcx> { + #[deref] + #[deref_mut] + pub(super) place: Place<'tcx>, + pub is_local_mutation_allowed: LocalMutationIsAllowed, +} diff --git a/mir-state-analysis/tests/top_crates.rs b/mir-state-analysis/tests/top_crates.rs new file mode 100644 index 00000000000..65e4c1fdb5a --- /dev/null +++ b/mir-state-analysis/tests/top_crates.rs @@ -0,0 +1,143 @@ +use serde_derive::{Deserialize, Serialize}; +use std::path::PathBuf; + +#[test] +pub fn top_crates() { + top_crates_range(0..500) +} + +fn get(url: &str) -> reqwest::Result { + println!("Getting: {url}"); + reqwest::blocking::ClientBuilder::new() + .user_agent("Rust Corpus - Top Crates Scrapper") + .build()? + .get(url) + .send() +} + +pub fn top_crates_range(range: std::ops::Range) { + std::fs::create_dir_all("tmp").unwrap(); + let top_crates = CratesIter::top(range); + for (i, krate) in top_crates { + let version = krate.version.unwrap_or(krate.newest_version); + println!("Starting: {i} ({})", krate.name); + run_on_crate(&krate.name, &version); + } +} + +fn run_on_crate(name: &str, version: &str) { + 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/{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(); + } + println!("Unwrapping: {filename}"); + let status = std::process::Command::new("tar") + .args(["-xf", &filename, "-C", "./tmp/"]) + .status() + .unwrap(); + assert!(status.success()); + let mut file = std::fs::OpenOptions::new() + .write(true) + .append(true) + .open(format!("{dirname}/Cargo.toml")) + .unwrap(); + use std::io::Write; + writeln!(file, "\n[workspace]").unwrap(); + let cwd = std::env::current_dir().unwrap(); + assert!( + cfg!(debug_assertions), + "Must be run in debug mode, to enable full checking" + ); + let target = if cfg!(debug_assertions) { + "debug" + } else { + "release" + }; + let prusti = cwd.join( + ["..", "target", target, "cargo-prusti"] + .iter() + .collect::(), + ); + println!("Running: {prusti:?}"); + let exit = std::process::Command::new(prusti) + .env("PRUSTI_TEST_FREE_PCS", "true") + .env("PRUSTI_SKIP_UNSUPPORTED_FEATURES", "true") + // .env("PRUSTI_LOG", "debug") + .env("PRUSTI_NO_VERIFY_DEPS", "true") + .current_dir(&dirname) + .status() + .unwrap(); + assert!(exit.success()); + // std::fs::remove_dir_all(dirname).unwrap(); +} + +/// A create on crates.io. +#[derive(Debug, Deserialize, Serialize)] +struct Crate { + #[serde(rename = "id")] + name: String, + #[serde(rename = "max_stable_version")] + version: Option, + #[serde(rename = "newest_version")] + newest_version: String, +} + +/// The list of crates from crates.io +#[derive(Debug, Deserialize)] +struct CratesList { + crates: Vec, +} + +const PAGE_SIZE: usize = 100; +struct CratesIter { + curr_idx: usize, + curr_page: usize, + crates: Vec, +} + +impl CratesIter { + pub fn new(start: usize) -> Self { + Self { + curr_idx: start, + curr_page: start / PAGE_SIZE + 1, + crates: Vec::new(), + } + } + pub fn top(range: std::ops::Range) -> impl Iterator { + Self::new(range.start).take(range.len()) + } +} + +impl Iterator for CratesIter { + type Item = (usize, Crate); + fn next(&mut self) -> Option { + if self.crates.is_empty() { + let url = format!( + "https://crates.io/api/v1/crates?page={}&per_page={PAGE_SIZE}&sort=downloads", + self.curr_page, + ); + let resp = get(&url).expect("Could not fetch top crates"); + assert!( + resp.status().is_success(), + "Response status: {}", + resp.status() + ); + let page_crates: CratesList = match serde_json::from_reader(resp) { + Ok(page_crates) => page_crates, + Err(e) => panic!("Invalid JSON {e}"), + }; + assert_eq!(page_crates.crates.len(), PAGE_SIZE); + self.crates = page_crates.crates; + self.crates.reverse(); + self.crates + .truncate(self.crates.len() - self.curr_idx % PAGE_SIZE); + self.curr_page += 1; + } + self.curr_idx += 1; + Some((self.curr_idx - 1, self.crates.pop().unwrap())) + } +} diff --git a/prusti-interface/src/environment/body.rs b/prusti-interface/src/environment/body.rs index 90c7229d2d3..48eea9e314a 100644 --- a/prusti-interface/src/environment/body.rs +++ b/prusti-interface/src/environment/body.rs @@ -16,6 +16,11 @@ use crate::environment::{borrowck::facts::BorrowckFacts, mir_storage}; /// Prusti might want to work with. Cheap to clone #[derive(Clone, TyEncodable, TyDecodable)] pub struct MirBody<'tcx>(Rc>); +impl<'tcx> MirBody<'tcx> { + pub fn body(&self) -> Rc> { + self.0.clone() + } +} impl<'tcx> std::ops::Deref for MirBody<'tcx> { type Target = mir::Body<'tcx>; fn deref(&self) -> &Self::Target { diff --git a/prusti-interface/src/environment/procedure.rs b/prusti-interface/src/environment/procedure.rs index ee81c1d93d9..8dc9a90cab7 100644 --- a/prusti-interface/src/environment/procedure.rs +++ b/prusti-interface/src/environment/procedure.rs @@ -133,6 +133,10 @@ impl<'tcx> Procedure<'tcx> { &self.mir } + pub fn get_mir_rc(&self) -> std::rc::Rc> { + self.mir.body() + } + /// Get the typing context. pub fn get_tcx(&self) -> TyCtxt<'tcx> { self.tcx diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index b137f929c6e..4cfc879a9e2 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -130,6 +130,8 @@ lazy_static::lazy_static! { settings.set_default::>("number_of_parallel_verifiers", None).unwrap(); settings.set_default::>("min_prusti_version", None).unwrap(); settings.set_default("num_errors_per_function", 1).unwrap(); + // TODO: remove this option + settings.set_default("test_free_pcs", false).unwrap(); settings.set_default("print_desugared_specs", false).unwrap(); settings.set_default("print_typeckd_specs", false).unwrap(); @@ -1030,3 +1032,8 @@ pub fn enable_type_invariants() -> bool { pub fn num_errors_per_function() -> u32 { read_setting("num_errors_per_function") } + +// TODO: remove +pub fn test_free_pcs() -> bool { + read_setting("test_free_pcs") +} diff --git a/prusti/Cargo.toml b/prusti/Cargo.toml index 81900537208..c42681fc002 100644 --- a/prusti/Cargo.toml +++ b/prusti/Cargo.toml @@ -21,6 +21,7 @@ lazy_static = "1.4.0" tracing = { path = "../tracing" } tracing-subscriber = { version = "0.3", features = ["env-filter"] } tracing-chrome = "0.7" +mir-state-analysis = { path = "../mir-state-analysis" } [build-dependencies] chrono = { version = "0.4.22", default-features = false, features = ["clock"] } diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index b622a8b1ad0..a430b8255d3 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -1,4 +1,5 @@ use crate::verifier::verify; +use mir_state_analysis::test_free_pcs; use prusti_common::config; use prusti_interface::{ environment::{mir_storage, Environment}, @@ -34,7 +35,10 @@ fn mir_borrowck<'tcx>(tcx: TyCtxt<'tcx>, def_id: LocalDefId) -> &BorrowCheckResu // when calling `get_body_with_borrowck_facts`. TODO: figure out if we need // (anon) const bodies at all, and if so, how to get them? if !is_anon_const { - let consumer_opts = if is_spec_fn(tcx, def_id.to_def_id()) || config::no_verify() { + let consumer_opts = if is_spec_fn(tcx, def_id.to_def_id()) + || config::no_verify() + || config::test_free_pcs() + { consumers::ConsumerOptions::RegionInferenceContext } else { consumers::ConsumerOptions::PoloniusOutputFacts @@ -157,7 +161,18 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls { } CrossCrateSpecs::import_export_cross_crate(&mut env, &mut def_spec); if !config::no_verify() { - verify(env, def_spec); + if config::test_free_pcs() { + for proc_id in env.get_annotated_procedures_and_types().0.iter() { + let current_procedure = env.get_procedure(*proc_id); + let mir = current_procedure.get_mir_rc(); + + let name = env.name.get_unique_item_name(*proc_id); + println!("Calculating FPCS for: {name} ({:?})", mir.span); + test_free_pcs(&mir, tcx); + } + } else { + verify(env, def_spec); + } } });