diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 614482482ae..a71392584bd 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -110,6 +110,29 @@ jobs: - name: Run quick tests run: python x.py test --all quick + top-crates: + runs-on: ubuntu-latest + env: + PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin + steps: + - name: Check out the repo + uses: actions/checkout@v3 + - name: Set up Java + uses: actions/setup-java@v3 + with: + java-version: '15' + distribution: 'zulu' + - name: Set up the environment + run: python x.py setup + - name: Cache cargo + uses: Swatinem/rust-cache@v2 + with: + shared-key: "shared" + - name: Build with cargo + run: python x.py build --all + - name: Run quick tests + run: python x.py test --package mir-state-analysis --test top_crates -- top_crates --exact --nocapture + # Run a subset of the tests with the purification optimization enabled # to ensure that we do not introduce regressions. purification-tests: diff --git a/Cargo.lock b/Cargo.lock index e070c4b73aa..76588def9b4 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -903,6 +903,12 @@ version = "0.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0688c2a7f92e427f44895cd63841bff7b29f8d7a1648b9e7e07a4a365b2e1257" +[[package]] +name = "dot" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a74b6c4d4a1cff5f454164363c16b72fa12463ca6b31f4b5f2035a65fa3d5906" + [[package]] name = "dunce" version = "1.0.4" @@ -1499,6 +1505,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 +1883,23 @@ dependencies = [ "windows-sys 0.42.0", ] +[[package]] +name = "mir-state-analysis" +version = "0.1.0" +dependencies = [ + "derive_more", + "dot", + "prusti-interface", + "prusti-rustc-interface", + "regex", + "reqwest", + "serde", + "serde_derive", + "serde_json", + "smallvec", + "tracing 0.1.0", +] + [[package]] name = "multer" version = "2.1.0" @@ -2266,6 +2302,7 @@ dependencies = [ "env_logger", "lazy_static", "log", + "mir-state-analysis", "prusti-common", "prusti-interface", "prusti-rustc-interface", @@ -2597,10 +2634,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 +2649,7 @@ dependencies = [ "serde_json", "serde_urlencoded", "tokio", + "tokio-native-tls", "tokio-rustls", "tower-service", "url", @@ -3335,6 +3375,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..64830293800 --- /dev/null +++ b/mir-state-analysis/Cargo.toml @@ -0,0 +1,25 @@ +[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" } +dot = "0.1" +smallvec = { version = "^1.11", features = ["union", "const_new"] } +# TODO: remove +prusti-interface = { path = "../prusti-interface" } +regex = "1" + +[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/coupling_graph/check/checker.rs b/mir-state-analysis/src/coupling_graph/check/checker.rs new file mode 100644 index 00000000000..73b66f621dc --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/check/checker.rs @@ -0,0 +1,417 @@ +// © 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::{ + ast::Mutability, + borrowck::borrow_set::BorrowData, + data_structures::fx::{FxHashMap, FxHashSet}, + index::IndexVec, + middle::{ + mir::{visit::Visitor, BorrowKind, Location, ProjectionElem, Statement}, + ty::RegionVid, + }, +}; + +use crate::{ + coupling_graph::{ + coupling::{Block, CouplingOp}, + cursor::CgAnalysis, + graph::Graph, + region_info::map::RegionKind, + CgContext, + }, + free_pcs::{ + consistency::CapabilityConsistency, CapabilityKind, CapabilityLocal, CapabilitySummary, + Fpcs, FpcsBound, FreePcsAnalysis, RepackOp, + }, + utils::{Place, PlaceRepacker}, +}; + +#[derive(Clone)] +struct CouplingState<'a, 'tcx> { + blocks: IndexVec>, + blocked_by: IndexVec>, + waiting_to_activate: FxHashSet, + cgx: &'a CgContext<'a, 'tcx>, +} + +impl<'a, 'tcx> std::fmt::Debug for CouplingState<'a, 'tcx> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_map() + .entries(self.blocks.iter_enumerated()) + .finish() + } +} + +#[tracing::instrument(name = "cg::check", level = "debug", skip(cg, fpcs_cursor))] +pub(crate) fn check<'tcx>( + mut cg: CgAnalysis<'_, '_, 'tcx>, + mut fpcs_cursor: FreePcsAnalysis<'_, 'tcx>, +) { + let cgx = cg.cgx(); + let rp: PlaceRepacker<'_, '_> = cgx.rp; + let body = rp.body(); + for (block, data) in body.basic_blocks.iter_enumerated() { + cg.analysis_for_bb(block); + fpcs_cursor.analysis_for_bb(block); + + let mut cg_state = CouplingState { + blocks: IndexVec::from_elem_n(FxHashSet::default(), cgx.region_info.map.region_len()), + blocked_by: IndexVec::from_elem_n( + FxHashSet::default(), + cgx.region_info.map.region_len(), + ), + waiting_to_activate: FxHashSet::default(), + cgx, + }; + cg_state.initialize(&cg.initial_state()); + assert!(cg_state.compare(&cg.initial_state())); // TODO: remove + + fpcs_cursor.set_bound_non_empty(); + let mut fpcs = Fpcs { + summary: fpcs_cursor.initial_state().clone(), + apply_pre_effect: false, + bottom: false, + repackings: Vec::new(), + repacker: rp, + bound: FpcsBound::empty(true), + }; + // Consistency + fpcs.summary.consistency_check(rp); + for (statement_index, stmt) in data.statements.iter().enumerate() { + let loc = Location { + block, + statement_index, + }; + cg_state.check_location(loc, stmt, &mut fpcs, &mut cg, &mut fpcs_cursor); + } + let loc = Location { + block, + statement_index: data.statements.len(), + }; + let cg_before = cg.before_next(loc); + // Couplings + for c in cg_before.couplings { + c.update_free(&mut cg_state, false); + } + + let bound: Box) -> CapabilityKind> = + Box::new(cg_state.mk_capability_upper_bound()); + fpcs_cursor.set_bound(unsafe { std::mem::transmute(bound) }); + let fpcs_after = fpcs_cursor.next(loc); + assert_eq!(fpcs_after.location, loc); + fpcs_cursor.unset_bound(); + + // Repacks + for op in fpcs_after.repacks_middle { + op.update_free(&mut fpcs.summary, false, true, rp); + } + // Couplings bound set + let bound: Box) -> CapabilityKind> = + Box::new(cg_state.mk_capability_upper_bound()); + fpcs.bound.borrow_mut().0 = Some(unsafe { std::mem::transmute(bound) }); + // Consistency + fpcs.summary.consistency_check(rp); + // Statement pre + assert!(fpcs.repackings.is_empty()); + fpcs.apply_pre_effect = true; + fpcs.visit_terminator(data.terminator(), loc); + // Repacks + for op in fpcs_after.repacks { + op.update_free(&mut fpcs.summary, false, true, rp); + } + // Statement post + assert!(fpcs.repackings.is_empty()); + fpcs.apply_pre_effect = false; + fpcs.visit_terminator(data.terminator(), loc); + assert!(fpcs.repackings.is_empty()); + // Consistency + fpcs.summary.consistency_check(rp); + // Couplings bound unset + fpcs.bound.borrow_mut().0 = None; + + assert_eq!(fpcs.summary, fpcs_after.state); + + let cg_after = cg.next(loc); + // Couplings + for c in cg_after.couplings { + c.update_free(&mut cg_state, false); + } + assert!(cg_state.compare(&cg_after.state), "{loc:?}"); + + let fpcs_end = fpcs_cursor.terminator(); + let cg_end = cg.terminator(); + + for (fpcs_succ, cg_succ) in fpcs_end.succs.into_iter().zip(cg_end.succs) { + assert_eq!(fpcs_succ.location, cg_succ.location); + // Repacks + let mut fpcs_from = fpcs.clone(); + for op in fpcs_succ.repacks { + op.update_free( + &mut fpcs_from.summary, + body.basic_blocks[fpcs_succ.location.block].is_cleanup, + false, + rp, + ); + } + assert_eq!(fpcs_from.summary, fpcs_succ.state); + + // Couplings + let mut cg_from = cg_state.clone(); + for op in cg_succ.couplings { + op.update_free(&mut cg_from, false); + } + assert!( + cg_from.compare(&cg_succ.state), + "{loc:?} -> {:?}", + cg_succ.location + ); + } + } +} + +impl<'a, 'tcx> CouplingState<'a, 'tcx> { + fn initialize(&mut self, graph: &Graph<'tcx>) { + for (sub, v) in graph.nodes.iter_enumerated() { + for sup in v.true_edges() { + self.blocks[sub].insert(sup); + self.blocked_by[sup].insert(sub); + } + } + self.waiting_to_activate = graph.inactive_loans.clone(); + } + + #[tracing::instrument( + name = "CouplingState::check_location", + level = "trace", + skip(self, stmt, cg, fpcs, fpcs_cursor) + )] + fn check_location( + &mut self, + loc: Location, + stmt: &Statement<'tcx>, + fpcs: &mut Fpcs<'_, 'tcx>, + cg: &mut CgAnalysis<'_, '_, 'tcx>, + fpcs_cursor: &mut FreePcsAnalysis<'_, 'tcx>, + ) { + let rp = self.cgx.rp; + + let cg_before = cg.before_next(loc); + // Couplings + for c in cg_before.couplings { + c.update_free(self, false); + } + + let bound: Box) -> CapabilityKind> = + Box::new(self.mk_capability_upper_bound()); + fpcs_cursor.set_bound(unsafe { std::mem::transmute(bound) }); + let fpcs_after = fpcs_cursor.next(loc); + assert_eq!(fpcs_after.location, loc); + fpcs_cursor.unset_bound(); + + // Repacks + for op in fpcs_after.repacks_middle { + op.update_free(&mut fpcs.summary, false, true, rp); + } + // Couplings bound set + let bound: Box) -> CapabilityKind> = + Box::new(self.mk_capability_upper_bound()); + fpcs.bound.borrow_mut().0 = Some(unsafe { std::mem::transmute(bound) }); // Extend lifetimes (safe since we unset it later) + // 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, false, true, rp); + } + // Statement post + assert!(fpcs.repackings.is_empty()); + fpcs.apply_pre_effect = false; + fpcs.visit_statement(stmt, loc); + assert!(fpcs.repackings.is_empty()); + // Consistency + fpcs.summary.consistency_check(rp); + // Couplings bound unset + fpcs.bound.borrow_mut().0 = None; + + // Only apply coupling ops after + let cg_after = cg.next(loc); + // Couplings + for c in cg_after.couplings { + c.update_free(self, false); + } + assert!(self.compare(&cg_after.state), "{loc:?}"); + } + + #[tracing::instrument(name = "CouplingState::compare", level = "trace")] + fn compare(&self, other: &Graph) -> bool { + // println!("Compare"); + for (sub, v) in self.blocks.iter_enumerated() { + let blocks: FxHashSet<_> = other.nodes[sub].true_edges().into_iter().collect(); + // println!("Compare {sub:?} blocks: {v:?} == {blocks:?}"); + if v != &blocks { + println!("{sub:?} blocks: {v:?} != {blocks:?}"); + return false; + } + } + true + } + + #[tracing::instrument(name = "mk_capability_upper_bound", level = "trace")] + fn mk_capability_upper_bound(&self) -> impl Fn(Place<'tcx>) -> CapabilityKind + '_ { + move |place| self.capability_upper_bound(place) + } + #[tracing::instrument(name = "capability_upper_bound", level = "debug")] + fn capability_upper_bound(&self, place: Place<'tcx>) -> CapabilityKind { + let mut upper_bound = CapabilityKind::Exclusive; + for proj in place.projection_refs(self.cgx.rp) { + match proj { + None => upper_bound = CapabilityKind::Exclusive, + Some((_, _, Mutability::Not)) => upper_bound = CapabilityKind::Read, + Some((region, _, Mutability::Mut)) => { + let r = region.as_var(); // Could this not be a var? + if self.has_real_blockers(r) { + return CapabilityKind::None; + } + } + } + } + tracing::debug!("upper_bound: {:?}", upper_bound); + for borrow in self.active_borrows() { + assert!(self.has_real_blockers(borrow.region)); + // Places related? + if let Some(bound) = upper_bound_borrow(place, borrow, self.cgx.rp) { + upper_bound = upper_bound.minimum(bound).unwrap(); + // Early return + if upper_bound.is_none() { + return upper_bound; + } + } + } + upper_bound + } + fn active_borrows(&self) -> impl Iterator> + '_ { + self.blocked_by + .iter_enumerated() + .filter(|(region, blockers)| { + !blockers.is_empty() && !self.waiting_to_activate.contains(region) + }) + .flat_map(move |(region, _)| self.cgx.region_info.map.get(region).get_borrow()) + } + fn has_real_blockers(&self, region: RegionVid) -> bool { + let scc = self.calculate_scc(region); + let fn_region = self.cgx.region_info.function_region; + scc.iter().any(|r| { + self.blocked_by[*r] + .iter() + .any(|blocker| !scc.contains(blocker) && *blocker != fn_region) + }) + // self.blocked_by[region].iter().copied().any(|r| { + // let r = self.cgx.region_info.map.get(r); + // !r.universal() && !r.is_borrow() + // }) + } + fn calculate_scc(&self, region: RegionVid) -> FxHashSet { + let mut visited_out: FxHashSet<_> = [region, self.cgx.region_info.static_region] + .into_iter() + .collect(); + let mut stack = vec![region, self.cgx.region_info.static_region]; + while let Some(next) = stack.pop() { + let blocks = self.blocks[next] + .iter() + .copied() + .filter(|r| visited_out.insert(*r)); + stack.extend(blocks); + } + let mut visited_in: FxHashSet<_> = [region].into_iter().collect(); + let mut stack = vec![region]; + while let Some(next) = stack.pop() { + let blocked_by = self.blocked_by[next] + .iter() + .copied() + .filter(|r| visited_in.insert(*r)); + stack.extend(blocked_by); + } + visited_out.intersection(&visited_in).copied().collect() + } +} + +#[tracing::instrument(name = "upper_bound_borrow", level = "trace", skip(rp), ret)] +fn upper_bound_borrow<'tcx>( + place: Place<'tcx>, + borrow: &BorrowData<'tcx>, + rp: PlaceRepacker<'_, 'tcx>, +) -> Option { + let borrowed = borrow.borrowed_place.into(); + place.partial_cmp(borrowed).map(|cmp| { + let lower_bound = if cmp.is_prefix() + && borrowed + .projection_tys(rp) + .skip(place.projection.len()) + .any(|(ty, _)| ty.ty.is_any_ptr()) + { + CapabilityKind::Write + } else { + CapabilityKind::None + }; + let kind = match borrow.kind { + BorrowKind::Shared => CapabilityKind::Read, + BorrowKind::Shallow if cmp.is_suffix() => CapabilityKind::Exclusive, + BorrowKind::Shallow => CapabilityKind::Read, + BorrowKind::Mut { .. } => CapabilityKind::None, + }; + lower_bound.sum(kind).unwrap() + }) +} + +impl CouplingOp { + #[tracing::instrument(name = "CouplingOp::update_free", level = "trace")] + fn update_free<'tcx>(&self, cg_state: &mut CouplingState, is_cleanup: bool) { + match self { + CouplingOp::Add(block) => block.update_free(cg_state, is_cleanup), + CouplingOp::Remove(remove, new_blocks) => { + Self::remove(cg_state, *remove); + for block in new_blocks { + block.update_free(cg_state, is_cleanup); + } + } + CouplingOp::Activate(region) => { + let contained = cg_state.waiting_to_activate.remove(region); + assert!(contained); + } + } + } + fn remove(cg_state: &mut CouplingState, remove: RegionVid) { + let blocks = std::mem::replace(&mut cg_state.blocks[remove], FxHashSet::default()); + for block in blocks { + cg_state.blocked_by[block].remove(&remove); + } + let blocked_by = std::mem::replace(&mut cg_state.blocked_by[remove], FxHashSet::default()); + for block_by in blocked_by { + cg_state.blocks[block_by].remove(&remove); + } + } +} + +impl Block { + fn update_free<'tcx>(self, cg_state: &mut CouplingState, is_cleanup: bool) { + let Block { + sup, + sub, + waiting_to_activate, + } = self; + assert!(!cg_state.cgx.region_info.map.get(sub).is_borrow()); + if waiting_to_activate && cg_state.waiting_to_activate.insert(sup) { + assert!(cg_state.blocked_by[sup].is_empty()); + } + cg_state.blocks[sub].insert(sup); + cg_state.blocked_by[sup].insert(sub); + } +} diff --git a/mir-state-analysis/src/coupling_graph/check/consistency.rs b/mir-state-analysis/src/coupling_graph/check/consistency.rs new file mode 100644 index 00000000000..cefaa488203 --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/check/consistency.rs @@ -0,0 +1,28 @@ +// © 2023, ETH Zurich +// +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. + +use crate::coupling_graph::{graph::Graph, triple::Cg, CgContext}; + +pub trait CouplingConsistency<'tcx> { + fn consistency_check(&self, cgx: &CgContext<'_, 'tcx>) -> Option; +} + +impl<'tcx> CouplingConsistency<'tcx> for Cg<'_, 'tcx> { + #[tracing::instrument(name = "Graph::consistency_check", level = "trace", skip(self, cgx))] + fn consistency_check(&self, cgx: &CgContext<'_, 'tcx>) -> Option { + for (sub, node) in self.graph.all_nodes() { + for (sup, edge) in node.blocks.iter() { + let sup_info = cgx.region_info.map.get(*sup); + let sub_info = cgx.region_info.map.get(sub); + + if sup_info.is_borrow() && self.graph.static_regions.contains(&sup) { + return Some(format!("Borrow is static: {sup:?}")); + } + } + } + None + } +} diff --git a/mir-state-analysis/src/coupling_graph/check/mod.rs b/mir-state-analysis/src/coupling_graph/check/mod.rs new file mode 100644 index 00000000000..0c96a032e19 --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/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; +pub mod consistency; + +pub(crate) use checker::check; diff --git a/mir-state-analysis/src/coupling_graph/context/mod.rs b/mir-state-analysis/src/coupling_graph/context/mod.rs new file mode 100644 index 00000000000..bbc702dfeab --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/context/mod.rs @@ -0,0 +1,84 @@ +// © 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::{cell::RefCell, fmt}; + +use self::{ + outlives_info::OutlivesInfo, region_info::RegionInfo, shared_borrow_set::SharedBorrowSet, +}; +use crate::{ + r#loop::LoopAnalysis, + utils::{Place, PlaceRepacker}, +}; +use prusti_interface::environment::borrowck::facts::{BorrowckFacts, BorrowckFacts2}; +use prusti_rustc_interface::{ + borrowck::consumers::{BorrowIndex, Borrows, OutlivesConstraint}, + data_structures::fx::FxHashMap, + dataflow::{Analysis, ResultsCursor}, + index::IndexVec, + middle::{ + mir::{Body, Location, Promoted, RETURN_PLACE}, + ty::{RegionVid, TyCtxt}, + }, +}; + +pub(crate) mod shared_borrow_set; +pub(crate) mod region_info; +pub(crate) mod outlives_info; + +pub struct CgContext<'a, 'tcx> { + pub rp: PlaceRepacker<'a, 'tcx>, + pub facts: &'a BorrowckFacts, + pub facts2: &'a BorrowckFacts2<'tcx>, + + pub sbs: SharedBorrowSet<'tcx>, + // pub region_map: FxHashMap>, + pub loops: LoopAnalysis, + + pub region_info: RegionInfo<'tcx>, + pub outlives_info: OutlivesInfo<'tcx>, +} + +impl fmt::Debug for CgContext<'_, '_> { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.debug_struct("CgContext") + .field("sbs", &self.sbs) + .field("region_info", &self.region_info) + .field("outlives_info", &self.outlives_info) + .finish() + } +} + +impl<'a, 'tcx> CgContext<'a, 'tcx> { + #[tracing::instrument(name = "CgContext::new", level = "debug", skip_all, ret)] + pub fn new( + tcx: TyCtxt<'tcx>, + body: &'a Body<'tcx>, + promoted: &'a IndexVec>, + facts: &'a BorrowckFacts, + facts2: &'a BorrowckFacts2<'tcx>, + ) -> Self { + let borrow_set = &facts2.borrow_set; + let sbs = SharedBorrowSet::build(tcx, body, borrow_set); + let rp = PlaceRepacker::new(body, promoted, tcx); + let input_facts = facts.input_facts.borrow(); + let input_facts = input_facts.as_ref().unwrap(); + let loops = LoopAnalysis::find_loops(body); + + let region_info = RegionInfo::new(rp, input_facts, facts2, &sbs); + let outlives_info = OutlivesInfo::new(input_facts, facts2, ®ion_info); + + Self { + rp, + facts, + facts2, + sbs, + loops, + region_info, + outlives_info, + } + } +} diff --git a/mir-state-analysis/src/coupling_graph/context/outlives_info/edge.rs b/mir-state-analysis/src/coupling_graph/context/outlives_info/edge.rs new file mode 100644 index 00000000000..7bf7ec1bedd --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/context/outlives_info/edge.rs @@ -0,0 +1,311 @@ +// © 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::{ + borrow::Cow, + fmt::{Debug, Display, Formatter, Result}, +}; + +use derive_more::{Deref, DerefMut}; +use prusti_interface::environment::borrowck::facts::{BorrowckFacts, BorrowckFacts2}; +use prusti_rustc_interface::{ + borrowck::{ + borrow_set::BorrowData, + consumers::{BorrowIndex, OutlivesConstraint}, + }, + data_structures::fx::{FxHashMap, FxHashSet, FxIndexMap, FxIndexSet}, + dataflow::fmt::DebugWithContext, + index::{bit_set::BitSet, IndexVec}, + middle::{ + mir::{ + BasicBlock, ConstraintCategory, Local, Location, Operand, Rvalue, StatementKind, + TerminatorKind, RETURN_PLACE, + }, + ty::{RegionVid, TyKind}, + }, +}; + +use crate::coupling_graph::CgContext; + +#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] +pub enum EdgeOrigin { + Rustc, + RustcUniversal, + Static, + Opaque, +} + +#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] +pub struct Edge<'tcx> { + pub info: EdgeInfo<'tcx>, + pub kind: EdgeKind, +} + +impl<'tcx> Edge<'tcx> { + pub fn sup(self) -> RegionVid { + self.info.sup + } + pub fn sub(self) -> RegionVid { + self.info.sub + } + pub fn is_opaque(self) -> bool { + matches!(self.info.origin, EdgeOrigin::Opaque) + } + pub fn is_blocking(edge: &Vec) -> bool { + edge.iter().any(|e| e.kind.is_blocking()) + } + + pub fn widen( + edge: &Vec, + top: impl Fn(RegionVid, RegionVid) -> Self, + needs_widening: impl Fn(Location) -> bool, + ) -> Vec { + let mut new_edge = Vec::new(); + let widen_edge: &mut Option<(RegionVid, RegionVid)> = &mut None; + for &e in edge { + if e.info + .creation + .map(|loc| needs_widening(loc)) + .unwrap_or_default() + { + match widen_edge { + Some((_, sup)) => *sup = e.info.sup, + None => *widen_edge = Some((e.info.sub, e.info.sup)), + } + } else { + if let Some((sub, sup)) = widen_edge.take() { + new_edge.push(top(sup, sub)); + } + new_edge.push(e); + } + } + if let Some((sub, sup)) = widen_edge.take() { + new_edge.push(top(sup, sub)); + } + new_edge + } + pub fn generalized_by(target: &Vec, by: &Vec) -> bool { + let mut looking_for = 0; + for elem in target.iter().copied() { + if looking_for == by.len() { + return false; + } else if by[looking_for].is_opaque() { + if looking_for == by.len() - 1 { + return true; + } else if by[looking_for + 1] == elem { + looking_for += 2; + } + } else if by[looking_for] == elem { + looking_for += 1; + } else { + return false; + } + } + looking_for == by.len() + } +} + +impl Display for Edge<'_> { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + let reason = if let Some(reason) = self.info.reason { + match reason { + ConstraintCategory::Return(_) => "return", + ConstraintCategory::Yield => "yield", + ConstraintCategory::UseAsConst => "const", + ConstraintCategory::UseAsStatic => "static", + ConstraintCategory::TypeAnnotation => "type", + ConstraintCategory::Cast => "cast", + ConstraintCategory::ClosureBounds => "closure", + ConstraintCategory::CallArgument(_) => "arg", + ConstraintCategory::CopyBound => "copy", + ConstraintCategory::SizedBound => "sized", + ConstraintCategory::Assignment => "assign", + ConstraintCategory::Usage => "use", + ConstraintCategory::OpaqueType => "opaque", + ConstraintCategory::ClosureUpvar(_) => "upvar", + ConstraintCategory::Predicate(_) => "pred", + ConstraintCategory::Boring => "?", + ConstraintCategory::BoringNoLocation => "? no_loc", + ConstraintCategory::Internal => "internal", + } + } else { + "other" + }; + let creation = self + .info + .creation + .map(|c| format!("{c:?}")) + .unwrap_or_else(|| "sig".to_string()); + match self.info.origin { + EdgeOrigin::Rustc => write!(f, "{creation} ({reason})"), + EdgeOrigin::RustcUniversal => { + assert!(self.info.reason.is_none() && self.info.creation.is_none()); + write!(f, "universal") + } + EdgeOrigin::Static => { + assert!(self.info.reason.is_none() && self.info.creation.is_none()); + write!(f, "promoted") + } + EdgeOrigin::Opaque => { + assert!(self.info.reason.is_none() && self.info.creation.is_some()); + write!(f, "{creation} (loop)") + } + } + } +} + +#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] +pub struct EdgeInfo<'tcx> { + /// The region which outlives (usually means blocked) + sup: RegionVid, + /// The region which is outlived (usually means blocking) + sub: RegionVid, + pub creation: Option, + pub reason: Option>, + pub origin: EdgeOrigin, +} + +impl<'tcx> EdgeInfo<'tcx> { + pub fn no_reason( + sup: RegionVid, + sub: RegionVid, + creation: Option, + origin: EdgeOrigin, + ) -> Self { + if !matches!(origin, EdgeOrigin::Opaque) { + assert_ne!(sup, sub); + } + Self { + sup, + sub, + creation, + reason: None, + origin, + } + } + #[tracing::instrument(name = "EdgeInfo::to_edge", level = "debug", skip_all, ret)] + pub fn to_edge(self, cgx: &CgContext<'_, 'tcx>) -> Edge<'tcx> { + let (sup_info, sub_info) = ( + cgx.region_info.map.get(self.sup), + cgx.region_info.map.get(self.sub), + ); + let stmt = self + .creation + .map(|location| cgx.rp.body().stmt_at(location)); + let term = stmt.and_then(|stmt| stmt.right()).map(|t| &t.kind); + let stmt = stmt.and_then(|stmt| stmt.left()).map(|s| &s.kind); + let kind = match (self.reason, self.origin, stmt, term) { + // (_, EdgeOrigin::Opaque, _, _) => EdgeKind::Opaque, + _ if sup_info.local() + && sub_info.universal() + && !matches!(self.origin, EdgeOrigin::Opaque) => + { + EdgeKind::UniversalToLocal + } + ( + Some(ConstraintCategory::BoringNoLocation), + _, + _, + Some(TerminatorKind::Call { .. }), + ) if sup_info.from_function_depth() > 0 && sub_info.from_function_depth() > 0 => { + EdgeKind::FnCallImplied + } + (Some(ConstraintCategory::Predicate(_)), _, _, _) => { + assert!(matches!(term.unwrap(), TerminatorKind::Call { .. })); + assert!(sup_info.from_function_depth() > 0 && sub_info.from_function_depth() > 0); + EdgeKind::FnCallPredicate + } + (Some(ConstraintCategory::CallArgument(_)), _, _, _) => { + assert!(matches!(term.unwrap(), TerminatorKind::Call { .. })); + // Can get a `Self::Static` outlives requirement from a function call + let static_eq = sup_info.is_static() ^ sub_info.is_static(); + let placeholders = sup_info.is_placeholder() && sub_info.is_placeholder(); + let sup_depth = sub_info.from_function_depth(); + let sub_depth = sup_info.from_function_depth(); + assert!( + static_eq + || placeholders + || (sup_depth + 1 == sub_depth) + || (sup_depth == sub_depth + 1), + "{sup_info:?} ({})\nand\n{sub_info:?} ({})\n({self:?})", + sup_info.from_function_depth(), + sub_info.from_function_depth() + ); + EdgeKind::FnCallArgument + } + (Some(ConstraintCategory::Assignment), _, _, Some(TerminatorKind::Call { .. })) => { + let static_eq = sup_info.is_static() ^ sub_info.is_static(); + // let placeholders = sup_info.is_placeholder() && sub_info.is_placeholder(); + let sup_depth = sub_info.from_function_depth(); + let sub_depth = sup_info.from_function_depth(); + assert!(static_eq || (sup_depth + 1 == sub_depth) || (sup_depth == sub_depth + 1)); + EdgeKind::FnCallReturn + } + _ if sub_info.is_borrow() || sub_info.is_projection_annotation() => { + // assert_ne!(self.origin, EdgeOrigin::Opaque); + // assert_eq!(sup_info.get_place().unwrap(), sub_info.get_borrow_or_projection_local().unwrap()); + EdgeKind::ContainedIn + } + _ if sub_info.get_place().is_some() + && sub_info.get_place() == sup_info.get_borrow_or_projection_local() => + { + // assert_ne!(self.origin, EdgeOrigin::Opaque); + // Edge from `_1.1: &mut T` to `AllIn(_1)` + EdgeKind::ContainedIn + } + _ => EdgeKind::Unknown, + }; + Edge { info: self, kind } + } +} + +impl<'tcx> From> for EdgeInfo<'tcx> { + fn from(c: OutlivesConstraint<'tcx>) -> Self { + Self { + sup: c.sup, + sub: c.sub, + creation: c.locations.from_location(), + reason: Some(c.category), + origin: EdgeOrigin::Rustc, + } + } +} + +#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] +pub enum EdgeKind { + /// An edge from `'a` to `'b` created when + /// re-borrowing `_ = &'a mut (*x).0` with `x: &'b mut (_, _)`. + ContainedIn, + /// An edge from `'a` to `'b` created when + /// calling `fn foo<'a, 'b>(x: &'a mut &'b mut _)`. + FnCallImplied, + /// An edge from `'a` to `'b` created when + /// calling `fn foo<'a, 'b: 'a>(_: &'b mut _) -> &'a mut _`. + FnCallPredicate, + /// An edge from `'a` to `'b` created when + /// calling `fn foo<'a>(_: &'a mut _)` with `x: &'b mut _`. + FnCallArgument, + /// An edge from `'a` to `'b` created when + /// calling `fn foo<'b>(_) -> &'b mut _` to `r: &'a mut = foo()`. + FnCallReturn, + UniversalToLocal, + /// Created from a loop. + Opaque, + Unknown, +} + +impl EdgeKind { + pub fn is_blocking(self) -> bool { + !matches!( + self, + EdgeKind::ContainedIn | EdgeKind::FnCallImplied | EdgeKind::UniversalToLocal + ) + } + + pub fn many_blocking(kinds: Vec) -> bool { + kinds.iter().any(|kind| kind.is_blocking()) + } +} diff --git a/mir-state-analysis/src/coupling_graph/context/outlives_info/mod.rs b/mir-state-analysis/src/coupling_graph/context/outlives_info/mod.rs new file mode 100644 index 00000000000..9ef7e4e140e --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/context/outlives_info/mod.rs @@ -0,0 +1,165 @@ +// © 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 edge; + +use prusti_interface::environment::borrowck::facts::{BorrowckFacts, BorrowckFacts2}; +use prusti_rustc_interface::{ + borrowck::{ + borrow_set::BorrowData, + consumers::{BorrowIndex, Borrows, OutlivesConstraint, PoloniusInput, RustcFacts}, + }, + data_structures::fx::{FxHashMap, FxHashSet}, + dataflow::{Analysis, ResultsCursor}, + index::IndexVec, + middle::{ + mir::{ + Body, ConstraintCategory, Local, Location, Operand, Place, StatementKind, + TerminatorKind, RETURN_PLACE, + }, + ty::{RegionVid, Ty, TyCtxt}, + }, +}; + +use super::region_info::RegionInfo; + +#[derive(Debug)] +pub struct OutlivesInfo<'tcx> { + pub universal_local_constraints: Vec>, + pub local_constraints: Vec>, // but with no location info + pub type_ascription_constraints: Vec>, + pub location_constraints: FxHashMap>>, + pub universal_constraints: Vec<(RegionVid, RegionVid)>, +} + +impl<'tcx> OutlivesInfo<'tcx> { + pub fn new( + input_facts: &PoloniusInput, + facts2: &BorrowckFacts2<'tcx>, + ri: &RegionInfo<'tcx>, + ) -> Self { + let mut universal_constraints = + FxHashSet::from_iter(input_facts.known_placeholder_subset.iter().copied()); + + let mut universal_local_constraints = Vec::new(); + let mut local_constraints = Vec::new(); + let mut type_ascription_constraints = Vec::new(); + let mut location_constraints: FxHashMap>> = + FxHashMap::default(); + for constraint in facts2.region_inference_context.outlives_constraints() { + if let Some(loc) = constraint.locations.from_location() { + location_constraints + .entry(loc) + .or_default() + .push(constraint); + } else if ri.map.is_universal(constraint.sup) || ri.map.is_universal(constraint.sub) { + if ri.map.is_universal(constraint.sup) && ri.map.is_universal(constraint.sub) { + // Not sure why the `region_inference_context` can rarely contain inter-universal constraints, + // but we should already have all of these in `universal_constraints`. + // Except for even more rare situations... + universal_constraints.insert((constraint.sup, constraint.sub)); + } else { + universal_local_constraints.push(constraint); + } + } else if matches!(constraint.category, ConstraintCategory::TypeAnnotation) { + type_ascription_constraints.push(constraint); + } else { + local_constraints.push(constraint); + } + } + Self { + universal_local_constraints, + local_constraints, + type_ascription_constraints, + location_constraints, + universal_constraints: universal_constraints.into_iter().collect(), + } + } + + fn location(&self, location: Location) -> &[OutlivesConstraint<'tcx>] { + self.location_constraints + .get(&location) + .map_or(&[], |v| v.as_slice()) + } + // #[tracing::instrument(name = "OutlivesInfo::pre_constraints", level = "debug", skip(self, ri))] + pub fn pre_constraints<'a>( + &'a self, + location: Location, + local: Option, + ri: &'a RegionInfo<'tcx>, + ) -> impl Iterator> + 'a { + self.location(location).iter().filter(move |c| { + if let Some(local) = local { + ri.map + .get(c.sub) + .get_place() + .map(|l| l != local) + .unwrap_or(true) + && ri + .map + .get(c.sup) + .get_place() + .map(|l| l != local) + .unwrap_or(true) + } else { + true + } + }) + } + // #[tracing::instrument(name = "OutlivesInfo::pre_constraints", level = "debug", skip(self, ri))] + pub fn post_constraints<'a>( + &'a self, + location: Location, + local: Option, + ri: &'a RegionInfo<'tcx>, + ) -> impl Iterator> + 'a { + self.location(location).iter().filter(move |c| { + !(if let Some(local) = local { + ri.map + .get(c.sub) + .get_place() + .map(|l| l != local) + .unwrap_or(true) + && ri + .map + .get(c.sup) + .get_place() + .map(|l| l != local) + .unwrap_or(true) + } else { + true + }) + }) + } +} + +pub trait AssignsToPlace<'tcx> { + fn assigns_to(&self) -> Option>; +} + +impl<'tcx> AssignsToPlace<'tcx> for StatementKind<'tcx> { + fn assigns_to(&self) -> Option> { + match self { + StatementKind::Assign(box (place, _)) => Some(*place), + &StatementKind::StorageDead(local) => Some(local.into()), + _ => None, + } + } +} +impl<'tcx> AssignsToPlace<'tcx> for TerminatorKind<'tcx> { + fn assigns_to(&self) -> Option> { + match self { + TerminatorKind::Drop { place, .. } + | TerminatorKind::Call { + destination: place, .. + } + | TerminatorKind::Yield { + resume_arg: place, .. + } => Some(*place), + _ => None, + } + } +} diff --git a/mir-state-analysis/src/coupling_graph/context/region_info/map.rs b/mir-state-analysis/src/coupling_graph/context/region_info/map.rs new file mode 100644 index 00000000000..b4c709f3d06 --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/context/region_info/map.rs @@ -0,0 +1,516 @@ +// © 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, marker::PhantomData}; + +use prusti_interface::environment::borrowck::facts::{BorrowckFacts, BorrowckFacts2}; +use prusti_rustc_interface::{ + borrowck::{ + borrow_set::BorrowData, + consumers::{BorrowIndex, Borrows, OutlivesConstraint}, + }, + data_structures::fx::FxHashMap, + dataflow::{Analysis, ResultsCursor}, + index::IndexVec, + infer::infer::{ + region_constraints::RegionVariableInfo, LateBoundRegionConversionTime, + NllRegionVariableOrigin, RegionVariableOrigin, + }, + middle::{ + mir::{ + Body, BorrowKind, Local, Location, Operand, PlaceElem, PlaceRef, Promoted, RETURN_PLACE, + }, + ty::{BoundRegionKind, PlaceholderRegion, RegionVid, Ty, TyCtxt, TyKind}, + }, + span::{def_id::DefId, Span, Symbol}, +}; + +use crate::{ + coupling_graph::CgContext, + utils::{Place, PlaceRepacker}, +}; + +#[derive(Debug)] +pub struct RegionInfoMap<'tcx> { + region_info: IndexVec>, + universal: usize, + constant_regions: Vec, +} + +#[derive(Debug, Clone, Copy)] +pub struct GenericArgRegion<'tcx> { + pub did: DefId, + pub gen_idx: usize, + pub full_ty: Option>, +} + +impl<'tcx> GenericArgRegion<'tcx> { + fn to_string(gars: &Vec, cgx: &CgContext<'_, 'tcx>) -> String { + gars.iter() + .map(|gar| { + let tcx = cgx.rp.tcx(); + let generic = tcx.generics_of(gar.did).param_at(gar.gen_idx, tcx); + assert_eq!(generic.kind.is_ty_or_const(), gar.full_ty.is_some()); + let ty = gar.full_ty.map(|ty| format!(" = {ty}")).unwrap_or_default(); + if tcx.is_closure(gar.did) { + format!(" closure::<{}{ty}>", generic.name.as_str()) + } else { + format!( + " {}::<{}{ty}>", + tcx.item_name(gar.did).as_str(), + generic.name.as_str() + ) + } + }) + .collect() + } +} + +#[derive(Debug, Clone, Copy)] +pub enum ConstRegionKind { + Const(Promote), + TyConst, + /// Crated constructing an Aggregate with internal regions, + /// for example a struct with reference-typed fields. + Aggregate(Promote), +} +impl Display for ConstRegionKind { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + ConstRegionKind::Const(p) => write!(f, "const{p}"), + ConstRegionKind::TyConst => write!(f, "tconst"), + ConstRegionKind::Aggregate(p) => write!(f, "aggregate{p}"), + } + } +} + +#[derive(Debug, Clone, Copy)] +pub enum OtherAnnotationKind { + UserTy, + YieldTy, + RvalueTy(Promote), +} +impl Display for OtherAnnotationKind { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + OtherAnnotationKind::UserTy => write!(f, "user"), + OtherAnnotationKind::YieldTy => write!(f, "yield"), + OtherAnnotationKind::RvalueTy(p) => write!(f, "rvalue{p}"), + } + } +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Promote { + NotPromoted, + Promoted(Promoted), +} +impl Display for Promote { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + Promote::NotPromoted => Ok(()), + Promote::Promoted(p) => write!(f, " @promoted[{}]", p.index()), + } + } +} + +#[derive(Debug, Clone)] +pub enum RegionKind<'tcx> { + // Universal regions (placeholders) + Static, + Param(ParamRegion), + Function, + UnknownUniversal, + // - update `fn universal` if a new one is added! + + // Local regions + ConstRef(ConstRegionKind, Vec>), + Place { + local: Local, + ty: Ty<'tcx>, + promoted: Promote, + fn_generic: Vec>, + }, + Borrow(BorrowData<'tcx>, Promote), + UnusedReturnBug(Promote), // TODO: remove once `https://github.com/rust-lang/rust/pull/116792` lands + + // AggregateGeneric(DefId, usize, Option>), + // FnGeneric(DefId, usize, Option>), + EarlyBound(Symbol), + LateBound { + // span: Span, + kind: BoundRegionKind, + ctime: LateBoundRegionConversionTime, + }, + Placeholder(Option), + ProjectionAnnotation(Place<'tcx>, Ty<'tcx>, Vec>), + OtherAnnotation(OtherAnnotationKind, Ty<'tcx>, Vec>), + MiscLocal, + UnknownLocal, +} + +impl<'tcx> RegionKind<'tcx> { + pub fn is_static(&self) -> bool { + matches!(self, Self::Static) + } + pub fn is_param(&self) -> bool { + matches!(self, Self::Param(..)) + } + pub fn is_function(&self) -> bool { + matches!(self, Self::Function) + } + pub fn is_unknown_universal(&self) -> bool { + matches!(self, Self::UnknownUniversal) + } + pub fn is_const_ref(&self) -> bool { + matches!(self, Self::ConstRef(..)) + } + pub fn is_place(&self) -> bool { + matches!(self, Self::Place { .. }) + } + pub fn is_borrow(&self) -> bool { + matches!(self, Self::Borrow(..)) + } + pub fn is_unused_return_bug(&self) -> bool { + matches!(self, Self::UnusedReturnBug(..)) + } + pub fn is_early_bound(&self) -> bool { + matches!(self, Self::EarlyBound(..)) + } + pub fn is_late_bound(&self) -> bool { + matches!(self, Self::LateBound { .. }) + } + pub fn is_placeholder(&self) -> bool { + matches!(self, Self::Placeholder(..)) + } + pub fn is_projection_annotation(&self) -> bool { + matches!(self, Self::ProjectionAnnotation(..)) + } + pub fn is_other_annotation(&self) -> bool { + matches!(self, Self::OtherAnnotation(..)) + } + pub fn is_misc_local(&self) -> bool { + matches!(self, Self::MiscLocal) + } + pub fn is_unknown_local(&self) -> bool { + matches!(self, Self::UnknownLocal) + } + + pub fn promoted(&self) -> bool { + matches!( + self, + Self::Place { + promoted: Promote::Promoted(..), + .. + } | Self::Borrow(_, Promote::Promoted(..)) + | Self::UnusedReturnBug(Promote::Promoted(..)) + | Self::OtherAnnotation(OtherAnnotationKind::RvalueTy(Promote::Promoted(..)), _, _) + | Self::ConstRef(ConstRegionKind::Const(Promote::Promoted(..)), _) + | Self::ConstRef(ConstRegionKind::Aggregate(Promote::Promoted(..)), _) + ) + } + pub fn unknown(&self) -> bool { + matches!(self, Self::UnknownUniversal | Self::UnknownLocal) + } + + pub fn universal(&self) -> bool { + matches!( + self, + Self::Static | Self::Param(..) | Self::Function | Self::UnknownUniversal + ) + } + pub fn local(&self) -> bool { + !self.universal() + } + + pub fn from_function_depth(&self) -> usize { + match self { + Self::LateBound { + ctime: LateBoundRegionConversionTime::FnCall, + .. + } => 1, + Self::ConstRef(_, fn_generic) + | Self::Place { fn_generic, .. } + | Self::ProjectionAnnotation(_, _, fn_generic) + | Self::OtherAnnotation(_, _, fn_generic) => fn_generic.len(), + _ => 0, + } + } + + pub fn set_fn_generic(&mut self, generic: GenericArgRegion<'tcx>) { + match self { + Self::ConstRef(_, fn_generic) + | Self::Place { fn_generic, .. } + | Self::ProjectionAnnotation(_, _, fn_generic) + | Self::OtherAnnotation(_, _, fn_generic) => fn_generic.push(generic), + _ => panic!("{self:?} ({generic:?})"), + } + } + pub fn unset_fn_generic(&mut self) { + match self { + Self::ConstRef(_, fn_generic) + | Self::Place { fn_generic, .. } + | Self::ProjectionAnnotation(_, _, fn_generic) + | Self::OtherAnnotation(_, _, fn_generic) => assert!(fn_generic.pop().is_some()), + _ => panic!(), + } + } + + // #[tracing::instrument(name = "RegionKind::get_place", level = "trace", ret)] + pub fn get_place(&self) -> Option { + match self { + Self::Place { + local, + promoted: Promote::NotPromoted, + .. + } => Some(*local), + _ => None, + } + } + pub fn get_borrow(&self) -> Option<&BorrowData<'tcx>> { + match self { + Self::Borrow(data, Promote::NotPromoted) => Some(data), + _ => None, + } + } + pub fn get_borrow_or_projection_local(&self) -> Option { + match self { + Self::Borrow(data, Promote::NotPromoted) => Some(data.borrowed_place.local), + Self::ProjectionAnnotation(place, _, _) => Some(place.local), + _ => None, + } + } + + pub fn to_string(&self, cgx: &CgContext<'_, 'tcx>) -> String { + match self { + Self::Static => "'static".to_string(), + Self::Param(ParamRegion { regions }) => { + let mut result = "old(".to_string(); + for (idx, r) in regions + .iter() + .map(|&r| cgx.region_info.map.get(r).to_string(cgx)) + .enumerate() + { + if idx != 0 { + result += " + "; + } + result += &r; + } + result += ")"; + result + } + Self::Function => "'fn".to_string(), + Self::UnknownUniversal => "'unknown".to_string(), + Self::ConstRef(kind, fn_generic) => { + format!("{kind}{}", GenericArgRegion::to_string(fn_generic, cgx)) + } + Self::Place { + local, + ty, + promoted, + fn_generic, + } => { + let place = Place::from(*local); + // let exact = place.deref_to_region(*region, cgx.rp); + // let display = exact.unwrap_or(place).to_string(cgx.rp); + // if exact.is_some() { + // format!("{display:?}{promoted}") + // } else { + format!("AllIn({:?} = {ty}){promoted}", place.to_string(cgx.rp)) + // } + } + Self::Borrow(b, promoted) => match b.kind { + BorrowKind::Shared => { + format!( + "& {:?}{promoted}", + Place::from(b.borrowed_place).to_string(cgx.rp) + ) + } + BorrowKind::Mut { .. } => { + format!( + "&mut {:?}{promoted}", + Place::from(b.borrowed_place).to_string(cgx.rp) + ) + } + BorrowKind::Shallow => { + format!( + "&sh {:?}{promoted}", + Place::from(b.borrowed_place).to_string(cgx.rp) + ) + } + }, + Self::EarlyBound(name) => name.as_str().to_string(), + Self::LateBound { kind, ctime } => { + let kind = match kind { + BoundRegionKind::BrAnon(..) => "'_", + BoundRegionKind::BrNamed(_, name) => name.as_str(), + BoundRegionKind::BrEnv => "'env", + }; + let ctime = match ctime { + LateBoundRegionConversionTime::FnCall => "fn", + LateBoundRegionConversionTime::HigherRankedType => "hrt", + LateBoundRegionConversionTime::AssocTypeProjection(_) => "atp", + }; + format!("{kind} ({ctime})") + } + Self::Placeholder(None) => "'for".to_string(), + Self::Placeholder(Some(p)) => { + let kind = match &p.bound.kind { + BoundRegionKind::BrAnon(..) => "'_", + BoundRegionKind::BrNamed(_, name) => name.as_str(), + BoundRegionKind::BrEnv => "'env", + }; + format!("{kind}@{:?}", p.universe) + } + Self::ProjectionAnnotation(place, ty, fn_generic) => format!( + "{:?}: {ty}{}", + place.to_string(cgx.rp), + GenericArgRegion::to_string(fn_generic, cgx) + ), + &Self::OtherAnnotation(kind, ty, ref fn_generic) => format!( + "{kind} {ty}{}", + GenericArgRegion::to_string(fn_generic, cgx) + ), + Self::MiscLocal => "?misc?".to_string(), + Self::UnusedReturnBug(..) => unreachable!(), + Self::UnknownLocal => "???".to_string(), + } + } +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct ParamRegion { + pub regions: Vec, +} + +impl<'tcx> RegionInfoMap<'tcx> { + pub fn new(universal: usize, total: usize) -> Self { + let region_info = IndexVec::from_fn_n( + |r: RegionVid| { + if r.index() < universal { + RegionKind::UnknownUniversal + } else { + RegionKind::UnknownLocal + } + }, + total, + ); + Self { + region_info, + universal, + constant_regions: Vec::new(), + } + } + + pub(super) fn check_already_local(&mut self, r: RegionVid, l: Local) { + let kind = self.get(r); + if kind.get_place().is_none() { + panic!("{r:?}: {:?} != {:?}", kind, l); + } + assert_eq!(kind.get_place().unwrap(), l); + } + pub(super) fn check_already_borrow(&mut self, r: RegionVid, b: &BorrowData<'tcx>) { + let data = self.get(r).get_borrow().unwrap(); + assert_eq!(data.to_string(), b.to_string()); + assert_eq!(data.reserve_location, b.reserve_location); + assert_eq!(data.activation_location, b.activation_location); + } + pub(super) fn set(&mut self, r: RegionVid, kind: RegionKind<'tcx>) { + match self.get(r) { + RegionKind::UnknownUniversal => assert!(kind.is_static() || kind.is_function()), + RegionKind::UnknownLocal => assert!( + kind.is_const_ref() + || kind.is_place() + || kind.is_borrow() + || kind.is_unused_return_bug() + || kind.is_early_bound() + || kind.is_late_bound() + || kind.is_placeholder() + || kind.is_projection_annotation() + || kind.is_other_annotation() + || kind.is_misc_local(), + "{kind:?}" + ), + other => panic!("{other:?} ({kind:?})"), + } + if kind.is_const_ref() && kind.from_function_depth() == 0 { + self.constant_regions.push(r); + } + self.region_info[r] = kind; + } + pub(super) fn set_param(&mut self, r: RegionVid, local: RegionVid) { + let info = &mut self.region_info[r]; + match info { + RegionKind::Param(ParamRegion { regions }) => regions.push(local), + RegionKind::UnknownUniversal => { + *info = RegionKind::Param(ParamRegion { + regions: vec![local], + }) + } + // Ignore equivalences between static and a local + RegionKind::Static => (), + _ => panic!("{info:?}"), + } + } + pub(super) fn set_region_info(&mut self, r: RegionVid, info: RegionVariableInfo) { + // TODO: figure out the universes stuff + // assert_eq!(info.universe.index(), 0); + match info.origin { + RegionVariableOrigin::MiscVariable(_) => self.set(r, RegionKind::MiscLocal), + RegionVariableOrigin::PatternRegion(_) => todo!(), + RegionVariableOrigin::AddrOfRegion(_) => todo!(), + RegionVariableOrigin::Autoref(_) => todo!(), + RegionVariableOrigin::Coercion(_) => todo!(), + RegionVariableOrigin::EarlyBoundRegion(_, name) => { + self.set(r, RegionKind::EarlyBound(name)); + todo!(); // Figure out how this compares to `FnGeneric` + } + RegionVariableOrigin::LateBoundRegion(_, kind, ctime) => { + self.set(r, RegionKind::LateBound { kind, ctime }) + } + RegionVariableOrigin::UpvarRegion(_, _) => todo!(), + RegionVariableOrigin::Nll(k) => match k { + NllRegionVariableOrigin::FreeRegion => { + assert!(self.get(r).universal()); + return; + } + NllRegionVariableOrigin::Placeholder(p) => { + self.set(r, RegionKind::Placeholder(Some(p))) + } + NllRegionVariableOrigin::Existential { from_forall: true } => { + self.set(r, RegionKind::Placeholder(None)) + } + NllRegionVariableOrigin::Existential { from_forall: false } => (), + }, + } + assert!(!self.get(r).universal()); + } + + // #[tracing::instrument(name = "RegionInfoMap::get", level = "trace", skip(self), ret)] + pub fn get(&self, r: RegionVid) -> &RegionKind<'tcx> { + &self.region_info[r] + } + pub fn is_universal(&self, r: RegionVid) -> bool { + r.index() < self.universal + } + pub(super) fn universal(&self) -> usize { + self.universal + } + + pub fn region_len(&self) -> usize { + self.region_info.len() + } + pub fn all_regions(&self) -> impl Iterator { + (0..self.region_info.len()).map(RegionVid::from) + } + pub fn for_local(&self, r: RegionVid, l: Local) -> bool { + self.get(r).get_place() == Some(l) + || self.get(r).get_borrow_or_projection_local() == Some(l) + } + pub fn const_regions(&self) -> &[RegionVid] { + &self.constant_regions + } +} diff --git a/mir-state-analysis/src/coupling_graph/context/region_info/mod.rs b/mir-state-analysis/src/coupling_graph/context/region_info/mod.rs new file mode 100644 index 00000000000..275d20a8a79 --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/context/region_info/mod.rs @@ -0,0 +1,491 @@ +// © 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::{marker::PhantomData, ops::ControlFlow}; + +use prusti_interface::environment::borrowck::facts::{BorrowckFacts, BorrowckFacts2}; +use prusti_rustc_interface::{ + borrowck::{ + borrow_set::{BorrowData, TwoPhaseActivation}, + consumers::{BorrowIndex, Borrows, OutlivesConstraint, PoloniusInput, RustcFacts}, + }, + data_structures::fx::FxHashMap, + dataflow::{Analysis, ResultsCursor}, + index::Idx, + middle::{ + mir::{ + visit::{PlaceContext, TyContext, Visitor}, + AggregateKind, Body, Constant, ConstantKind, Local, Location, Operand, + Place as MirPlace, PlaceElem, PlaceRef, ProjectionElem, Promoted, Rvalue, Terminator, + TerminatorKind, RETURN_PLACE, + }, + ty::{ + BoundVariableKind, Const, GenericArg, GenericArgKind, GenericArgsRef, Region, + RegionVid, Ty, TyCtxt, TyKind, TypeSuperVisitable, TypeVisitable, TypeVisitor, + }, + }, + span::{def_id::DefId, Span, Symbol}, +}; + +use crate::{ + coupling_graph::region_info::map::ParamRegion, + utils::{r#const::ConstEval, Place, PlaceRepacker}, +}; + +use self::map::{ + ConstRegionKind, GenericArgRegion, OtherAnnotationKind, Promote, RegionInfoMap, RegionKind, +}; + +use super::{shared_borrow_set::SharedBorrowSet, CgContext}; + +pub mod map; + +#[derive(Debug)] +pub struct RegionInfo<'tcx> { + pub map: RegionInfoMap<'tcx>, + pub static_region: RegionVid, + pub function_region: RegionVid, +} + +impl<'tcx> RegionInfo<'tcx> { + pub fn new( + rp: PlaceRepacker<'_, 'tcx>, + input_facts: &PoloniusInput, + facts2: &BorrowckFacts2<'tcx>, + sbs: &SharedBorrowSet<'tcx>, + ) -> Self { + let mut map = RegionInfoMap::new( + input_facts.universal_region.len(), + facts2.region_inference_context.var_infos.len(), + ); + // Assumption: universal regions are the first regions + debug_assert!(input_facts + .universal_region + .iter() + .all(|&r| map.is_universal(r))); + + // Init universals + let (static_region, function_region) = + Self::initialize_universals(&mut map, rp, input_facts, facts2); + + // Init consts + Self::initialize_consts(&mut map, rp, facts2); + + // Init locals + Self::initialize_locals(&mut map, rp, input_facts, facts2, sbs); + + // Init from `var_infos` + for r in map.all_regions() { + let info = facts2.region_inference_context.var_infos[r]; + map.set_region_info(r, info); + } + + // We should have figured out all local regions + for r in map.all_regions() { + // TODO: resolve all unknowns + assert!(!map.get(r).is_unknown_local(), "{r:?} is unknown: {map:?}"); + // assert!(!map.get(r).unknown(), "{r:?} is unknown: {map:?}"); + } + + Self { + map, + static_region, + function_region, + } + } + + pub fn initialize_universals( + map: &mut RegionInfoMap<'tcx>, + rp: PlaceRepacker<'_, 'tcx>, + input_facts: &PoloniusInput, + facts2: &BorrowckFacts2, + ) -> (RegionVid, RegionVid) { + let static_region = *input_facts.universal_region.first().unwrap(); + // Check that static is actually first + if cfg!(debug_symbols) { + // Static should outlive all other placeholders + let outlives = input_facts + .known_placeholder_subset + .iter() + .filter(|&&(sup, sub)| { + assert_ne!(static_region, sub); + static_region == sup + }); + assert_eq!(outlives.count(), map.universal() - 1); + } + let function_region = *input_facts.universal_region.last().unwrap(); + // Check that the function region is actually last + if cfg!(debug_symbols) { + // All other placeholders should outlive the function region + let outlives = input_facts + .known_placeholder_subset + .iter() + .filter(|&&(sup, sub)| { + assert_ne!(function_region, sup); + function_region == sub + }); + assert_eq!(outlives.count(), map.universal() - 1); + } + + // Collect equivalences between universal and local + let mut equivalence_map: FxHashMap<(RegionVid, RegionVid), u8> = FxHashMap::default(); + for c in facts2 + .region_inference_context + .outlives_constraints() + .filter(|o| { + o.locations.from_location().is_none() + && (map.is_universal(o.sup) || map.is_universal(o.sub)) + && !(map.is_universal(o.sup) && map.is_universal(o.sub)) + }) + { + let (universal, other, incr) = if map.is_universal(c.sup) { + (c.sup, c.sub, 1) + } else { + (c.sub, c.sup, 2) + }; + let entry = equivalence_map.entry((universal, other)).or_default(); + *entry |= incr; + // Note: Outlives constraints may be duplicated!! + // e.g. in `hashbrown-0.14.1` in `hashbrown::raw::RawTable::::clear::{closure#0}` at `src/raw/mod.rs:1021:37: 1021:66 (#0)` + } + + // Set the entries in the map + map.set(static_region, RegionKind::Static); + for ((universal, local), sum) in equivalence_map { + if sum == 3 { + map.set_param(universal, local); + } + } + map.set(function_region, RegionKind::Function); + (static_region, function_region) + } + + pub fn initialize_consts( + map: &mut RegionInfoMap<'tcx>, + rp: PlaceRepacker<'_, 'tcx>, + facts2: &BorrowckFacts2<'tcx>, + ) { + let mut collector = ConstantRegionCollector { + map, + inner_kind: None, + fn_ptr: false, + rp, + facts2, + return_ty: None, + promoted_idx: Promote::NotPromoted, + regions_set: None, + max_region: None, + }; + for (idx, promoted) in rp.promoted().iter_enumerated() { + collector.promoted_idx = Promote::Promoted(idx); + collector.visit_body(promoted); + } + collector.promoted_idx = Promote::NotPromoted; + collector.visit_body(rp.body()); + // for constant in &rp.body().required_consts { + // for r in constant.ty().walk().flat_map(|ga| ga.as_region()) { + // assert!(r.is_var(), "{r:?} in {constant:?}"); + // map.set(r.as_var(), RegionKind::ConstRef(ConstRegionKind::ExternalConst, Vec::new())); + // } + // } + } + + pub fn initialize_locals( + map: &mut RegionInfoMap<'tcx>, + rp: PlaceRepacker<'_, 'tcx>, + input_facts: &PoloniusInput, + facts2: &BorrowckFacts2<'tcx>, + sbs: &SharedBorrowSet<'tcx>, + ) { + for &(local, region) in &input_facts.use_of_var_derefs_origin { + // TODO: remove + map.check_already_local(region, local); + } + for data in sbs + .location_map + .values() + .chain(facts2.borrow_set.location_map.values()) + { + map.check_already_borrow(data.region, data); + } + } +} + +struct ConstantRegionCollector<'a, 'b, 'tcx> { + map: &'a mut RegionInfoMap<'tcx>, + inner_kind: Option>, + promoted_idx: Promote, + fn_ptr: bool, + rp: PlaceRepacker<'b, 'tcx>, + facts2: &'b BorrowckFacts2<'tcx>, + return_ty: Option>, + // Set this to start counting regions + regions_set: Option, + max_region: Option, +} +impl<'tcx> ConstantRegionCollector<'_, '_, 'tcx> { + fn with_kind(&mut self, kind: RegionKind<'tcx>, f: impl FnOnce(&mut Self) -> T) -> T { + let disc = std::mem::discriminant(&kind); + let old_kind = self.inner_kind.replace(kind); + assert!(old_kind.is_none()); + let t = f(self); + let kind = self.inner_kind.take(); + assert_eq!(std::mem::discriminant(&kind.unwrap()), disc); + self.inner_kind = old_kind; + t + } + + fn visit_generics_args(&mut self, did: DefId, generics: GenericArgsRef<'tcx>) { + for (gen_idx, arg) in generics.iter().enumerate() { + let inner_kind = self.inner_kind.as_mut().unwrap(); + inner_kind.set_fn_generic(GenericArgRegion { + did, + gen_idx, + full_ty: arg.as_type(), + }); + arg.visit_with(self); + self.inner_kind.as_mut().unwrap().unset_fn_generic(); + } + } + + fn set_region(&mut self, r: RegionVid, kind: RegionKind<'tcx>) { + assert!( + self.promoted_idx == Promote::NotPromoted || kind.promoted(), + "{kind:?} {r:?}" + ); + self.map.set(r, kind); + if let Some(regions_set) = &mut self.regions_set { + *regions_set += 1; + if let Some(max_region) = self.max_region { + assert_eq!(max_region.index() + 1, r.index()); + } + self.max_region = Some(r); + } + } +} + +impl<'tcx> Visitor<'tcx> for ConstantRegionCollector<'_, '_, 'tcx> { + #[tracing::instrument(name = "ConstantRegionCollector::visit_ty", level = "trace", skip(self), fields(promoted_idx = ?self.promoted_idx, inner_kind = ?self.inner_kind))] + fn visit_ty(&mut self, ty: Ty<'tcx>, ctx: TyContext) { + // println!("Ty ({ctx:?}): {ty:?}"); + match ctx { + TyContext::LocalDecl { local, .. } => { + if local == RETURN_PLACE { + assert!(self.regions_set.is_none() && self.max_region.is_none()); + self.regions_set = Some(0); + } + self.with_kind( + RegionKind::Place { + local, + ty, + promoted: self.promoted_idx, + fn_generic: Vec::new(), + }, + |this| ty.visit_with(this), + ); + if local == RETURN_PLACE { + // TODO: remove this once `https://github.com/rust-lang/rust/pull/116792` lands + let return_regions = self.regions_set.take().unwrap(); + if let Some(new_max) = self.max_region.take() { + for r in (0..return_regions).rev().map(|sub| { + RegionVid::from_usize(new_max.index() - return_regions - sub) + }) { + self.map + .set(r, RegionKind::UnusedReturnBug(self.promoted_idx)); + } + } + } + } + TyContext::ReturnTy(_) => { + assert_eq!(ty, self.return_ty.unwrap()) + } + TyContext::UserTy(_) => { + self.with_kind( + RegionKind::OtherAnnotation(OtherAnnotationKind::UserTy, ty, Vec::new()), + |this| ty.visit_with(this), + ); + } + TyContext::YieldTy(_) => { + self.with_kind( + RegionKind::OtherAnnotation(OtherAnnotationKind::YieldTy, ty, Vec::new()), + |this| ty.visit_with(this), + ); + } + TyContext::Location(_location) => { + assert!(self.inner_kind.is_some()); + ty.visit_with(self); + } + } + } + + #[tracing::instrument(name = "ConstantRegionCollector::visit_projection_elem", level = "trace", skip(self), fields(promoted_idx = ?self.promoted_idx, inner_kind = ?self.inner_kind))] + fn visit_projection_elem( + &mut self, + place_ref: PlaceRef<'tcx>, + elem: PlaceElem<'tcx>, + ctx: PlaceContext, + location: Location, + ) { + // println!("Projection elem ({ctx:?}): {place_ref:?} ({elem:?}) [{location:?}]"); + let place = Place::from(place_ref).mk_place_elem(elem, self.rp); + if let Some(ty) = place.last_projection_ty() { + assert!(matches!( + elem, + ProjectionElem::Field(..) | ProjectionElem::OpaqueCast(..) + )); + self.with_kind( + RegionKind::ProjectionAnnotation(place, ty, Vec::new()), + |this| this.super_projection_elem(place_ref, elem, ctx, location), + ) + } else { + self.super_projection_elem(place_ref, elem, ctx, location) + } + } + #[tracing::instrument(name = "ConstantRegionCollector::visit_ty_const", level = "trace", skip(self), fields(promoted_idx = ?self.promoted_idx, inner_kind = ?self.inner_kind))] + fn visit_ty_const(&mut self, ct: Const<'tcx>, _location: Location) { + // e.g. from `Rvalue::Repeat` + self.with_kind( + RegionKind::ConstRef(ConstRegionKind::TyConst, Vec::new()), + |this| { + ct.visit_with(this); + }, + ); + } + #[tracing::instrument(name = "ConstantRegionCollector::visit_constant", level = "trace", skip(self), fields(promoted_idx = ?self.promoted_idx, inner_kind = ?self.inner_kind))] + fn visit_constant(&mut self, constant: &Constant<'tcx>, _location: Location) { + // println!("Constant: {:?}", constant.ty()); + assert!(self.inner_kind.is_none()); + self.with_kind( + RegionKind::ConstRef(ConstRegionKind::Const(self.promoted_idx), Vec::new()), + |this| { + constant.visit_with(this); + }, + ); + } + #[tracing::instrument(name = "ConstantRegionCollector::visit_args", level = "trace", skip(self), fields(promoted_idx = ?self.promoted_idx, inner_kind = ?self.inner_kind))] + fn visit_args(&mut self, args: &GenericArgsRef<'tcx>, location: Location) { + // Do nothing since already handled by `Rvalue::Aggregate`. + } + #[tracing::instrument(name = "ConstantRegionCollector::visit_region", level = "trace", skip(self), fields(promoted_idx = ?self.promoted_idx, inner_kind = ?self.inner_kind))] + fn visit_region(&mut self, region: Region<'tcx>, location: Location) { + // Do nothing since already handled by `Rvalue::Ref`. + } + + #[tracing::instrument(name = "ConstantRegionCollector::visit_operand", level = "trace", skip(self), fields(promoted_idx = ?self.promoted_idx, inner_kind = ?self.inner_kind))] + fn visit_operand(&mut self, operand: &Operand<'tcx>, location: Location) { + // Temporarily remove `OtherAnnotationKind::RvalueTy` + let from_rvalue = matches!( + self.inner_kind, + Some(RegionKind::OtherAnnotation( + OtherAnnotationKind::RvalueTy(_), + _, + _ + )) + ); + if from_rvalue { + let kind = self.inner_kind.take(); + self.super_operand(operand, location); + self.inner_kind = kind; + } else { + self.super_operand(operand, location) + } + } + #[tracing::instrument(name = "ConstantRegionCollector::visit_assign", level = "trace", skip(self), fields(promoted_idx = ?self.promoted_idx, inner_kind = ?self.inner_kind))] + fn visit_assign(&mut self, place: &MirPlace<'tcx>, rvalue: &Rvalue<'tcx>, location: Location) { + match rvalue { + &Rvalue::Aggregate(box AggregateKind::Adt(did, _, generics, _, _), _) + | &Rvalue::Aggregate(box AggregateKind::Closure(did, generics), _) + | &Rvalue::Aggregate(box AggregateKind::Generator(did, generics, _), _) => { + self.with_kind( + RegionKind::ConstRef(ConstRegionKind::Aggregate(self.promoted_idx), Vec::new()), + |this| this.visit_generics_args(did, generics), + ); + self.super_assign(place, rvalue, location); // For the operand + } + &Rvalue::Ref(region, kind, borrowed_place) => { + let is_non_promoted = matches!(self.promoted_idx, Promote::NotPromoted); + let location_map = &self.facts2.borrow_set.location_map; + if is_non_promoted && location_map.contains_key(&location) { + let borrow = location_map.get(&location).unwrap(); + assert_eq!(borrow.region, region.as_var()); + self.set_region( + borrow.region, + RegionKind::Borrow(borrow.clone(), Promote::NotPromoted), + ) + } else { + let region = region.as_var(); + let borrow = BorrowData { + reserve_location: location, + activation_location: TwoPhaseActivation::NotTwoPhase, + kind, + region, + borrowed_place, + assigned_place: *place, + }; + self.set_region(borrow.region, RegionKind::Borrow(borrow, self.promoted_idx)) + } + self.super_assign(place, rvalue, location) + } + Rvalue::Aggregate(box AggregateKind::Array(ty), _) + | Rvalue::Cast(_, _, ty) + | Rvalue::NullaryOp(_, ty) + | Rvalue::ShallowInitBox(_, ty) => { + self.with_kind( + RegionKind::OtherAnnotation( + OtherAnnotationKind::RvalueTy(self.promoted_idx), + *ty, + Vec::new(), + ), + |this| this.super_assign(place, rvalue, location), + ); + } + _ => self.super_assign(place, rvalue, location), + } + } + #[tracing::instrument(name = "ConstantRegionCollector::visit_body", level = "trace", skip_all, fields(promoted_idx = ?self.promoted_idx, inner_kind = ?self.inner_kind))] + fn visit_body(&mut self, body: &Body<'tcx>) { + // println!("body: {body:#?}"); + self.return_ty = Some(body.local_decls[RETURN_PLACE].ty); + self.super_body(body); + self.return_ty = None; + } +} + +impl<'tcx> TypeVisitor> for ConstantRegionCollector<'_, '_, 'tcx> { + #[tracing::instrument(name = "ConstantRegionCollector::visit_region", level = "trace", skip(self), fields(promoted_idx = ?self.promoted_idx, inner_kind = ?self.inner_kind))] + fn visit_region(&mut self, r: Region<'tcx>) -> ControlFlow { + // println!("Region: {r:?}"); + if self.fn_ptr && !r.is_var() { + return ControlFlow::Continue(()); + } + let kind = self.inner_kind.clone().unwrap(); + self.set_region(r.as_var(), kind); + ControlFlow::Continue(()) + } + #[tracing::instrument(name = "ConstantRegionCollector::visit_ty", level = "trace", skip(self), fields(promoted_idx = ?self.promoted_idx, inner_kind = ?self.inner_kind))] + fn visit_ty(&mut self, ty: Ty<'tcx>) -> ControlFlow { + // println!("Ty inner: {ty:?}"); + match ty.kind() { + &TyKind::FnDef(did, generics) | &TyKind::Closure(did, generics) => { + self.visit_generics_args(did, generics); + ControlFlow::Continue(()) + } + TyKind::FnPtr(_) => { + self.fn_ptr = true; + let r = ty.super_visit_with(self); + self.fn_ptr = false; + r + } + // Maybe we want to handle the `region` here differently? + // TyKind::Dynamic(other, region, _) => todo!(), + TyKind::Generator(_, _, _) => todo!(), + TyKind::GeneratorWitness(_) => todo!(), + TyKind::GeneratorWitnessMIR(_, _) => todo!(), + TyKind::Bound(_, _) => todo!(), + _ => ty.super_visit_with(self), + } + } +} diff --git a/mir-state-analysis/src/coupling_graph/context/shared_borrow_set.rs b/mir-state-analysis/src/coupling_graph/context/shared_borrow_set.rs new file mode 100644 index 00000000000..45ddfd43d3a --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/context/shared_borrow_set.rs @@ -0,0 +1,108 @@ +// © 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::{ + borrowck::{ + borrow_set::{BorrowData, BorrowSet, LocalsStateAtExit, TwoPhaseActivation}, + consumers::{BorrowIndex, PlaceExt}, + }, + data_structures::fx::{FxHashMap, FxHashSet, FxIndexMap, FxIndexSet}, + dataflow::fmt::DebugWithContext, + index::{bit_set::BitSet, IndexVec}, + middle::{ + mir::{ + traversal, visit::Visitor, Body, ConstraintCategory, Local, Location, Place, Rvalue, + RETURN_PLACE, + }, + ty::TyCtxt, + }, +}; + +// Identical to `rustc_borrowck/src/borrow_set.rs` but for shared borrows +#[derive(Debug, Clone)] +pub struct SharedBorrowSet<'tcx> { + pub location_map: FxIndexMap>, + pub local_map: FxIndexMap>, +} + +impl<'tcx> SharedBorrowSet<'tcx> { + pub(crate) fn build(tcx: TyCtxt<'tcx>, body: &Body<'tcx>, borrows: &BorrowSet<'tcx>) -> Self { + let mut visitor = GatherBorrows { + tcx, + body: &body, + location_map: Default::default(), + local_map: Default::default(), + locals_state_at_exit: &borrows.locals_state_at_exit, + }; + + for (block, block_data) in traversal::preorder(&body) { + visitor.visit_basic_block_data(block, block_data); + } + + Self { + location_map: visitor.location_map, + local_map: visitor.local_map, + } + } +} + +struct GatherBorrows<'a, 'tcx> { + tcx: TyCtxt<'tcx>, + body: &'a Body<'tcx>, + location_map: FxIndexMap>, + local_map: FxIndexMap>, + locals_state_at_exit: &'a LocalsStateAtExit, +} + +impl<'a, 'tcx> Visitor<'tcx> for GatherBorrows<'a, 'tcx> { + fn visit_assign( + &mut self, + assigned_place: &Place<'tcx>, + rvalue: &Rvalue<'tcx>, + location: Location, + ) { + if let &Rvalue::Ref(region, kind, borrowed_place) = rvalue { + // Gather all borrows that the normal borrow-checker misses + if !borrowed_place.ignore_borrow(self.tcx, self.body, self.locals_state_at_exit) { + return; + } + + let region = region.as_var(); + + let borrow = BorrowData { + kind, + region, + reserve_location: location, + activation_location: TwoPhaseActivation::NotTwoPhase, + borrowed_place, + assigned_place: *assigned_place, + }; + let (idx, _) = self.location_map.insert_full(location, borrow); + let idx = BorrowIndex::from(idx); + + self.local_map + .entry(borrowed_place.local) + .or_default() + .insert(idx); + } + + self.super_assign(assigned_place, rvalue, location) + } + + fn visit_rvalue(&mut self, rvalue: &Rvalue<'tcx>, location: Location) { + if let &Rvalue::Ref(region, kind, place) = rvalue { + // double-check that we already registered a BorrowData for this + + let borrow_data = &self.location_map[&location]; + assert_eq!(borrow_data.reserve_location, location); + assert_eq!(borrow_data.kind, kind); + assert_eq!(borrow_data.region, region.as_var()); + assert_eq!(borrow_data.borrowed_place, place); + } + + self.super_rvalue(rvalue, location) + } +} diff --git a/mir-state-analysis/src/coupling_graph/impl/dot.rs b/mir-state-analysis/src/coupling_graph/impl/dot.rs new file mode 100644 index 00000000000..e0647f4af0e --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/impl/dot.rs @@ -0,0 +1,198 @@ +// © 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::borrow::Cow; + +use prusti_rustc_interface::{ + borrowck::consumers::BorrowIndex, + data_structures::fx::{FxHashMap, FxHashSet}, + dataflow::fmt::DebugWithContext, + index::{bit_set::BitSet, IndexVec}, + middle::{ + mir::{BasicBlock, BorrowKind, ConstraintCategory, Local}, + ty::{RegionVid, TyKind}, + }, +}; + +use crate::coupling_graph::outlives_info::edge::{Edge as CgEdge, EdgeInfo}; + +use super::triple::Cg; + +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Edge<'tcx> { + pub from: RegionVid, + pub to: RegionVid, + pub reasons: FxHashSet>>, +} + +impl<'tcx> Edge<'tcx> { + pub(crate) fn new( + from: RegionVid, + to: RegionVid, + reasons: FxHashSet>>, + ) -> Self { + Self { from, to, reasons } + } +} + +impl<'a, 'tcx> Cg<'a, 'tcx> { + fn get_id(&self) -> String { + if self.location.block == BasicBlock::MAX { + "start".to_string() + } else { + let pre = if self.is_pre { "_pre" } else { "" }; + format!("{:?}{pre}", self.location) + .replace('[', "_") + .replace(']', "") + } + } +} +impl<'a, 'tcx> Cg<'a, 'tcx> { + fn non_empty_edges( + &self, + sub: RegionVid, + start: RegionVid, + mut reasons: FxHashSet>>, + visited: &mut FxHashSet, + ) -> Vec> { + let mut edges = Vec::new(); + if !visited.insert(sub) { + return edges; + } + let sub_info = self.cgx.region_info.map.get(sub); + if (self.dot_node_filter)(sub_info) { + // Remove empty reasons + // reasons.retain(|reason| reason.iter().any(|r| r.creation.is_some()) || reason.reason.is_some()); + return vec![Edge::new(start, sub, reasons)]; + } + for (&sup, edge) in &self.graph.nodes[sub].blocks { + let sup_info = self.cgx.region_info.map.get(sup); + if !(self.dot_edge_filter)(sup_info, sub_info) { + continue; + } + let mut reasons = reasons.clone(); + reasons.extend(edge.clone()); + edges.extend(self.non_empty_edges(sup, start, reasons, visited)); + } + visited.remove(&sub); + edges + } +} + +impl<'a, 'b, 'tcx> dot::Labeller<'a, RegionVid, Edge<'tcx>> for Cg<'b, 'tcx> { + fn graph_id(&'a self) -> dot::Id<'a> { + dot::Id::new(self.get_id()).unwrap() + } + + fn node_id(&'a self, r: &RegionVid) -> dot::Id<'a> { + let r = format!("{r:?}").replace("'?", "N"); + let id = format!("{r}_{}", self.get_id()); + dot::Id::new(id).unwrap() + } + + fn edge_style(&'a self, e: &Edge<'tcx>) -> dot::Style { + let is_blocking = e.reasons.iter().any(|e| CgEdge::is_blocking(e)); + if is_blocking { + dot::Style::Solid + } else { + dot::Style::Dotted + } + } + fn edge_label(&'a self, e: &Edge<'tcx>) -> dot::LabelText<'a> { + let mut label = e + .reasons + .iter() + .map(|s| { + let line = s.into_iter().map(|s| format!("{s}, ")).collect::(); + format!("{}\n", &line[..line.len() - 2]) // `s.len() > 0` + }) + .collect::(); + if label.len() > 0 { + label = label[..label.len() - 1].to_string(); + } + dot::LabelText::LabelStr(Cow::Owned(label)) + } + fn node_color(&'a self, r: &RegionVid) -> Option> { + let kind = self.get_kind(*r); + if kind.universal() { + Some(dot::LabelText::LabelStr(Cow::Borrowed("red"))) + } else if self.graph.inactive_loans.contains(r) { + Some(dot::LabelText::LabelStr(Cow::Borrowed("blue"))) + } else { + None + } + } + fn node_shape(&'a self, r: &RegionVid) -> Option> { + if self.graph.static_regions.contains(&r) { + return Some(dot::LabelText::LabelStr(Cow::Borrowed("house"))); + } + // For regions created by `... = &'r ...`, find the kind of borrow. + self.cgx + .region_info + .map + .get(*r) + .get_borrow() + .map(|data| match data.kind { + BorrowKind::Shared => dot::LabelText::LabelStr(Cow::Borrowed("box")), + BorrowKind::Shallow => dot::LabelText::LabelStr(Cow::Borrowed("triangle")), + BorrowKind::Mut { kind } => dot::LabelText::LabelStr(Cow::Borrowed("polygon")), + }) + } + fn node_label(&'a self, r: &RegionVid) -> dot::LabelText<'a> { + if *r == RegionVid::MAX { + // return dot::LabelText::LabelStr(Cow::Owned()); + unimplemented!(); + } + let mut label = format!("{r:?}\n{}", self.get_kind(*r).to_string(&self.cgx)); + // Not super useful: the `origin` is always NLL. + // if let Some(region_info) = self.facts2.region_inference_context.var_infos.get(*r) { + // label += &format!("\n{:?}, {:?}", region_info.origin, region_info.universe); + // } + dot::LabelText::LabelStr(Cow::Owned(label)) + } +} + +impl<'a, 'b, 'tcx> dot::GraphWalk<'a, RegionVid, Edge<'tcx>> for Cg<'b, 'tcx> { + fn nodes(&self) -> dot::Nodes<'a, RegionVid> { + let mut nodes: Vec<_> = self + .graph + .all_nodes() + .filter(|(r, _)| (self.dot_node_filter)(self.cgx.region_info.map.get(*r))) + .map(|(r, _)| r) + .collect(); + // if self.static_regions.len() > 1 { + // nodes.push(usize::MAX); + // } + Cow::Owned(nodes) + } + + fn edges(&'a self) -> dot::Edges<'a, Edge<'tcx>> { + let mut edges = Vec::new(); + for (sub, n) in self.graph.all_nodes() { + let sub_info = self.cgx.region_info.map.get(sub); + if !(self.dot_node_filter)(sub_info) { + continue; + } + let visited = &mut FxHashSet::from_iter([sub]); + for (&sup, edge) in &n.blocks { + let sup_info = self.cgx.region_info.map.get(sup); + if !(self.dot_edge_filter)(sup_info, sub_info) { + continue; + } + edges.extend(self.non_empty_edges(sup, sub, edge.clone(), visited)); + } + } + Cow::Owned(edges) + } + + fn source(&self, e: &Edge<'tcx>) -> RegionVid { + e.from + } + + fn target(&self, e: &Edge<'tcx>) -> RegionVid { + e.to + } +} diff --git a/mir-state-analysis/src/coupling_graph/impl/engine.rs b/mir-state-analysis/src/coupling_graph/impl/engine.rs new file mode 100644 index 00000000000..bfc4cfdcd00 --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/impl/engine.rs @@ -0,0 +1,404 @@ +// © 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::cell::{Cell, RefCell}; + +use prusti_interface::environment::borrowck::facts::{BorrowckFacts, BorrowckFacts2}; +use prusti_rustc_interface::{ + borrowck::{ + borrow_set::{BorrowData, TwoPhaseActivation}, + consumers::{ + calculate_borrows_out_of_scope_at_location, places_conflict, BorrowIndex, Borrows, + OutlivesConstraint, PlaceConflictBias, RichLocation, + }, + }, + data_structures::fx::{FxHashSet, FxIndexMap}, + dataflow::{Analysis, AnalysisDomain, ResultsCursor}, + index::{ + bit_set::{BitSet, HybridBitSet}, + Idx, + }, + middle::{ + mir::{ + visit::Visitor, BasicBlock, Body, CallReturnPlaces, ConstantKind, Local, Location, + Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorEdges, + TerminatorKind, RETURN_PLACE, START_BLOCK, + }, + ty::{RegionVid, TyCtxt}, + }, +}; + +use crate::{ + coupling_graph::{ + consistency::CouplingConsistency, + graph::{Graph, Node}, + outlives_info::AssignsToPlace, + CgContext, + }, + free_pcs::{CapabilityKind, CapabilityLocal, Fpcs}, + utils::PlaceRepacker, +}; + +use super::triple::Cg; + +#[tracing::instrument(name = "draw_dots", level = "debug", skip(c))] +pub(crate) fn draw_dots<'tcx, 'a>(c: &mut ResultsCursor<'_, 'tcx, CouplingGraph<'a, 'tcx>>) { + let mut graph = Vec::new(); + let body = c.body(); + c.seek_to_block_start(START_BLOCK); + let mut g = c.get().clone(); + g.location.block = BasicBlock::MAX; + dot::render(&g, &mut graph).unwrap(); + + for (block, data) in body.basic_blocks.iter_enumerated() { + if data.is_cleanup { + continue; + } + c.seek_to_block_start(block); + let mut g = c.get().clone(); + g.dot_node_filter = |k| k.local(); + g.dot_edge_filter = |sup, sub| !(sup.local() && sub.universal()); + dot::render(&g, &mut graph).unwrap(); + drop(g); + for statement_index in 0..body.terminator_loc(block).statement_index { + let location = Location { + block, + statement_index, + }; + print_after_loc(c, location, &mut graph); + } + // Terminator + let location = Location { + block, + statement_index: body.terminator_loc(block).statement_index, + }; + if let TerminatorKind::Return = data.terminator().kind { + c.seek_before_primary_effect(location); + let mut g = c.get().clone(); + g.dot_node_filter = |k| !k.is_unknown_local(); + dot::render(&g, &mut graph).unwrap(); + c.seek_after_primary_effect(location); + let mut g = c.get().clone(); + g.location = location.successor_within_block(); + g.dot_node_filter = |k| !k.is_unknown_local(); + dot::render(&g, &mut graph).unwrap(); + } else { + print_after_loc(c, location, &mut graph); + } + } + let combined = std::str::from_utf8(graph.as_slice()).unwrap().to_string(); + + let regex = regex::Regex::new(r"digraph (([^ ])+) \{").unwrap(); + let combined = regex.replace_all(&combined, "subgraph cluster_$1 {\n label = \"$1\""); + + std::fs::write( + "log/coupling/all.dot", + format!("digraph root {{\n{combined}}}"), + ) + .expect("Unable to write file"); +} + +fn print_after_loc<'tcx, 'a>( + c: &mut ResultsCursor<'_, 'tcx, CouplingGraph<'a, 'tcx>>, + location: Location, + graph: &mut Vec, +) { + c.seek_after_primary_effect(location); + let mut g = c.get().clone(); + g.dot_node_filter = |k| k.local(); + g.dot_edge_filter = |sup, sub| !(sup.local() && sub.universal()); + dot::render(&g, graph).unwrap(); +} + +pub(crate) struct CouplingGraph<'a, 'tcx> { + pub(crate) cgx: &'a CgContext<'a, 'tcx>, + bb_index: Cell, + out_of_scope: FxIndexMap>, + flow_borrows: RefCell>>, + top_crates: bool, +} + +impl<'a, 'tcx> CouplingGraph<'a, 'tcx> { + pub(crate) fn new(cgx: &'a CgContext<'a, 'tcx>, top_crates: bool) -> Self { + if cfg!(debug_assertions) && !top_crates { + std::fs::remove_dir_all("log/coupling").ok(); + std::fs::create_dir_all("log/coupling/individual").unwrap(); + } + + let borrow_set = &cgx.facts2.borrow_set; + let regioncx = &*cgx.facts2.region_inference_context; + let out_of_scope = + calculate_borrows_out_of_scope_at_location(cgx.rp.body(), regioncx, borrow_set); + let flow_borrows = Borrows::new(cgx.rp.tcx(), cgx.rp.body(), regioncx, borrow_set) + .into_engine(cgx.rp.tcx(), cgx.rp.body()) + .pass_name("borrowck") + .iterate_to_fixpoint() + .into_results_cursor(cgx.rp.body()); + + if false && !top_crates { + println!("body: {:#?}", cgx.rp.body()); + println!("\ninput_facts: {:?}", cgx.facts.input_facts); + println!("output_facts: {:#?}\n", cgx.facts.output_facts); + println!("location_map: {:#?}\n", cgx.facts2.borrow_set.location_map); + println!( + "activation_map: {:#?}\n", + cgx.facts2.borrow_set.activation_map + ); + println!("local_map: {:?}\n", cgx.facts2.borrow_set.local_map); + // println!("locals_state_at_exit: {:#?}\n", facts2.borrow_set.locals_state_at_exit); + let lt = cgx.facts.location_table.borrow(); + let lt = lt.as_ref().unwrap(); + for pt in lt.all_points() { + println!("{pt:?} -> {:?} ({:?})", lt.to_location(pt), ""); //, facts.output_facts.origins_live_at(pt)); + } + println!("out_of_scope: {:?}", out_of_scope); + println!( + "outlives_constraints: {:#?}\n", + cgx.facts2 + .region_inference_context + .outlives_constraints() + .collect::>() + ); + println!("cgx: {:#?}\n", cgx); + for r in cgx.region_info.map.all_regions() { + println!( + "R: {r:?}: {:?}, {:?}", + cgx.facts2.region_inference_context.var_infos.get(r), + cgx.region_info.map.get(r), + ); + } + panic!(); + } + + Self { + cgx, + bb_index: Cell::new(START_BLOCK), + out_of_scope, + flow_borrows: RefCell::new(flow_borrows), + top_crates, + } + } +} + +impl<'a, 'tcx> AnalysisDomain<'tcx> for CouplingGraph<'a, 'tcx> { + type Domain = Cg<'a, 'tcx>; + const NAME: &'static str = "coupling_graph"; + + fn bottom_value(&self, _body: &Body<'tcx>) -> Self::Domain { + let block = self.bb_index.get(); + self.bb_index.set(block.plus(1)); + Cg::new( + self.cgx, + self.top_crates, + Location { + block, + statement_index: 0, + }, + ) + } + + fn initialize_start_block(&self, body: &Body<'tcx>, state: &mut Self::Domain) { + self.bb_index.set(START_BLOCK); + state.initialize_start_block() + } +} + +impl<'a, 'tcx> Analysis<'tcx> for CouplingGraph<'a, 'tcx> { + #[tracing::instrument( + name = "CouplingGraph::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.location = location; + state.reset_ops(); + + if location.statement_index == 0 { + state.is_pre = false; + // println!("\nblock: {:?}", location.block); + let l = format!("{location:?}").replace('[', "_").replace(']', ""); + state.output_to_dot( + format!( + "log/coupling/individual/{l}_v{}_start.dot", + state.sum_version() + ), + false, + ); + self.flow_borrows + .borrow_mut() + .seek_to_block_start(location.block); + state.live = self.flow_borrows.borrow().get().clone(); + } + self.flow_borrows + .borrow_mut() + .seek_after_primary_effect(location); + let other = self.flow_borrows.borrow().get().clone(); + let delta = calculate_diff(&other, &state.live); + state.live = other; + + let oos = self.out_of_scope.get(&location); + state.handle_kills(&delta, oos, location); + } + + #[tracing::instrument( + name = "CouplingGraph::apply_statement_effect", + level = "debug", + skip(self) + )] + fn apply_statement_effect( + &mut self, + state: &mut Self::Domain, + statement: &Statement<'tcx>, + location: Location, + ) { + state.reset_ops(); + state.handle_outlives(location, statement.kind.assigns_to()); + state.visit_statement(statement, location); + + let l = format!("{location:?}").replace('[', "_").replace(']', ""); + state.output_to_dot( + format!("log/coupling/individual/{l}_v{}.dot", state.sum_version()), + false, + ); + } + + #[tracing::instrument( + name = "CouplingGraph::apply_before_terminator_effect", + level = "debug", + skip(self) + )] + fn apply_before_terminator_effect( + &mut self, + state: &mut Self::Domain, + terminator: &Terminator<'tcx>, + location: Location, + ) { + // println!("Location: {l}"); + state.location = location; + state.reset_ops(); + + if location.statement_index == 0 { + state.is_pre = false; + // println!("\nblock: {:?}", location.block); + let l = format!("{location:?}").replace('[', "_").replace(']', ""); + state.output_to_dot( + format!( + "log/coupling/individual/{l}_v{}_start.dot", + state.sum_version() + ), + false, + ); + self.flow_borrows + .borrow_mut() + .seek_to_block_start(location.block); + state.live = self.flow_borrows.borrow().get().clone(); + } + self.flow_borrows + .borrow_mut() + .seek_after_primary_effect(location); + let other = self.flow_borrows.borrow().get().clone(); + + let delta = calculate_diff(&other, &state.live); + state.live = other; + + let oos = self.out_of_scope.get(&location); + state.handle_kills(&delta, oos, location); + } + + #[tracing::instrument( + name = "CouplingGraph::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.reset_ops(); + state.handle_outlives(location, terminator.kind.assigns_to()); + state.visit_terminator(terminator, location); + + match &terminator.kind { + TerminatorKind::Return => { + let l = format!("{location:?}").replace('[', "_").replace(']', ""); + state.output_to_dot( + format!( + "log/coupling/individual/{l}_v{}_pre.dot", + state.sum_version() + ), + false, + ); + // Pretend we have a storage dead for all `always_live_locals` other than the args/return + for l in self.cgx.rp.always_live_locals_non_args().iter() { + state.kill_shared_borrows_on_place(Some(location), l.into()); + } + // Kill all the intermediate borrows, i.e. turn `return -> x.0 -> x` into `return -> x` + for r in self + .cgx + .facts2 + .borrow_set + .location_map + .values() + .chain(self.cgx.sbs.location_map.values()) + { + state.remove(r.region, Some(location)); + } + + state.merge_for_return(location); + } + _ => (), + }; + + let l = format!("{:?}", location).replace('[', "_").replace(']', ""); + state.output_to_dot( + format!("log/coupling/individual/{l}_v{}.dot", state.sum_version()), + false, + ); + terminator.edges() + } + + fn apply_call_return_effect( + &mut self, + _state: &mut Self::Domain, + _block: BasicBlock, + _return_places: CallReturnPlaces<'_, 'tcx>, + ) { + // Nothing to do here + } +} + +#[derive(Debug)] +pub struct BorrowDelta { + set: HybridBitSet, + pub cleared: HybridBitSet, +} + +fn calculate_diff(curr: &BitSet, old: &BitSet) -> BorrowDelta { + let size = curr.domain_size(); + assert_eq!(size, old.domain_size()); + + let mut set_in_curr = HybridBitSet::new_empty(size); + let mut cleared_in_curr = HybridBitSet::new_empty(size); + + for i in (0..size).map(BorrowIndex::new) { + match (curr.contains(i), old.contains(i)) { + (true, false) => set_in_curr.insert(i), + (false, true) => cleared_in_curr.insert(i), + _ => continue, + }; + } + BorrowDelta { + set: set_in_curr, + cleared: cleared_in_curr, + } +} diff --git a/mir-state-analysis/src/coupling_graph/impl/graph.rs b/mir-state-analysis/src/coupling_graph/impl/graph.rs new file mode 100644 index 00000000000..761a6b43f44 --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/impl/graph.rs @@ -0,0 +1,281 @@ +// © 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::{ + borrow::Cow, + fmt::{Debug, Display, Formatter, Result}, +}; + +use derive_more::{Deref, DerefMut}; +use prusti_interface::environment::borrowck::facts::{BorrowckFacts, BorrowckFacts2}; +use prusti_rustc_interface::{ + borrowck::{ + borrow_set::BorrowData, + consumers::{BorrowIndex, OutlivesConstraint}, + }, + data_structures::fx::{FxHashMap, FxHashSet, FxIndexMap, FxIndexSet}, + dataflow::fmt::DebugWithContext, + index::{bit_set::BitSet, IndexVec}, + middle::{ + mir::{BasicBlock, ConstraintCategory, Local, Location, Operand, RETURN_PLACE}, + ty::{RegionVid, TyKind}, + }, +}; + +use crate::{ + coupling_graph::{ + outlives_info::edge::{Edge, EdgeKind, EdgeOrigin}, + CgContext, + }, + free_pcs::{ + engine::FreePlaceCapabilitySummary, CapabilityLocal, CapabilityProjections, RepackOp, + }, + utils::{Place, PlaceRepacker}, +}; + +use super::engine::CouplingGraph; + +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Graph<'tcx> { + pub nodes: IndexVec>, + // Regions equal to 'static + pub static_regions: FxHashSet, + // Two-phase loans waiting to activate + pub inactive_loans: FxHashSet, +} + +impl<'tcx> Graph<'tcx> { + #[tracing::instrument(name = "Graph::outlives", level = "trace", skip(self), ret)] + pub fn outlives(&mut self, edge: Edge<'tcx>) -> Option<(RegionVid, RegionVid, bool)> { + self.outlives_inner(vec![edge]) + } + // #[tracing::instrument(name = "Graph::outlives_placeholder", level = "trace", skip(self), ret)] + // pub fn outlives_placeholder(&mut self, sup: RegionVid, sub: RegionVid, origin: EdgeOrigin) -> Option<(RegionVid, RegionVid)> { + // let edge = EdgeInfo::no_reason(sup, sub, None, origin); + // self.outlives_inner(vec![edge]) + // } + + // sup outlives sub, or `sup: sub` (i.e. sup gets blocked) + #[tracing::instrument(name = "Graph::outlives_inner", level = "trace", skip(self), ret)] + fn outlives_inner(&mut self, edge: Vec>) -> Option<(RegionVid, RegionVid, bool)> { + let (sup, sub) = self.outlives_unwrap_edge(&edge); + self.nodes[sup].blocked_by.insert(sub); + let blocks = self.nodes[sub].blocks.entry(sup).or_default(); + let is_blocking = edge.iter().any(|edge| edge.kind.is_blocking()); + if blocks.insert(edge) { + Some((sup, sub, is_blocking)) + } else { + None + } + } + fn outlives_unwrap_edge(&mut self, edge: &Vec>) -> (RegionVid, RegionVid) { + let (sup, sub) = (edge.last().unwrap().sup(), edge.first().unwrap().sub()); + if self.static_regions.contains(&sub) { + Self::set_static_region(&self.nodes, &mut self.static_regions, sup); + } + (sup, sub) + } + + // sup outlives sub, or `sup: sub` (i.e. sup gets blocked) + #[tracing::instrument(name = "Graph::outlives_join", level = "trace", skip(self), ret)] + pub(super) fn outlives_join( + &mut self, + edge: Vec>, + ) -> Option<(RegionVid, RegionVid)> { + let (sup, sub) = self.outlives_unwrap_edge(&edge); + self.nodes[sup].blocked_by.insert(sub); + let blocks = self.nodes[sub].blocks.entry(sup).or_default(); + + if blocks + .iter() + .any(|other| Edge::generalized_by(&edge, other)) + { + None + } else { + blocks.retain(|other| !Edge::generalized_by(other, &edge)); + if blocks.insert(edge) { + Some((sup, sub)) + } else { + None + } + } + } + fn set_static_region( + nodes: &IndexVec>, + static_regions: &mut FxHashSet, + r: RegionVid, + ) { + if static_regions.insert(r) { + for &sup in nodes[r].blocks.keys() { + Self::set_static_region(nodes, static_regions, sup); + } + } + } + + #[tracing::instrument(name = "Graph::kill_borrow", level = "debug", skip(self))] + /// Remove borrow from graph and all nodes that block it and the node it blocks + pub fn kill_borrow(&mut self, data: &BorrowData<'tcx>) -> Vec { + self.kill(data.region) + } + + #[tracing::instrument(name = "Graph::kill", level = "trace", skip(self))] + fn kill(&mut self, r: RegionVid) -> Vec { + assert!(!self.static_regions.contains(&r)); + let (_, blocked_by) = self.remove_all_edges(r); + [r].into_iter() + .chain( + blocked_by + .iter() + .flat_map(|(blocked_by, _)| self.kill(*blocked_by)), + ) + .collect() + } + + #[tracing::instrument(name = "Graph::remove", level = "trace", ret)] + /// Remove node from graph and rejoin all blockers and blocked by. + // Set `remove_dangling_children` when removing regions which are not tracked by the regular borrowck, + // to remove in e.g. `let y: &'a i32 = &'b *x;` the region `'b` when removing `'a` (if `x: &'c i32`). + // NOTE: Maybe shouldn't be set, since it seems that the regular borrowck does not kill off `'b` this eagerly (if `x: &'c mut i32`). + pub fn remove( + &mut self, + r: RegionVid, + ) -> Option<(RegionVid, Vec<(RegionVid, RegionVid, bool)>)> { + let (blocks, blocked_by) = self.remove_all_edges(r); + let changed = !(blocks.is_empty() && blocked_by.is_empty()); + let mut rejoins = Vec::new(); + for (sup, sup_reasons) in blocks { + for (&sub, sub_reasons) in &blocked_by { + // Do not rejoin nodes in a loop to themselves + if sub != sup { + // TODO: change this so that we do not need to make opaque + assert!(sup_reasons.len() * sub_reasons.len() < 100); + let mut rejoined = None; + for sup_reason in &sup_reasons { + for sub_reason in sub_reasons { + let reasons = sub_reason.iter().chain(sup_reason).copied().collect(); + let new = self.outlives_inner(reasons); + if new.is_some() { + rejoined = new; + } + } + } + if let Some(rejoined) = rejoined { + rejoins.push(rejoined); + } + } + } + // if remove_dangling_children { + // let node = &self.nodes[block]; + // if node.blocked_by.is_empty() && self.cgx.sbs.location_map.values().any(|data| data.region == block) { + // self.remove(block, l, false, remove_dangling_children); + // } + // } + } + let was_static = self.static_regions.remove(&r); + debug_assert!(!was_static || changed); // Check that `was_static ==> changed` + if changed { + Some((r, rejoins)) + } else { + None + } + } + + #[tracing::instrument(name = "Graph::remove_many", level = "trace")] + pub fn remove_many( + &mut self, + rs: &FxHashSet, + ) -> Vec<(RegionVid, Vec<(RegionVid, RegionVid, bool)>)> { + for &r in rs { + if self.predecessors(r).iter().all(|pre| rs.contains(pre)) + || self.successors(r).iter().all(|suc| rs.contains(suc)) + { + self.static_regions.remove(&r); + self.remove_all_edges(r); + } + } + rs.iter().flat_map(|r| self.remove(*r)).collect() + } + + pub(crate) fn all_nodes(&self) -> impl Iterator)> { + self.nodes + .iter_enumerated() + .filter(|(_, n)| !n.blocked_by.is_empty() || !n.blocks.is_empty()) + } + + fn remove_all_edges( + &mut self, + r: RegionVid, + ) -> ( + FxHashMap>>>, + FxHashMap>>>, + ) { + let blocks = std::mem::replace(&mut self.nodes[r].blocks, FxHashMap::default()); + for block in blocks.keys() { + self.nodes[*block].blocked_by.remove(&r); + } + let blocked_by = std::mem::replace(&mut self.nodes[r].blocked_by, FxHashSet::default()); + let blocked_by = blocked_by + .into_iter() + .map(|bb| (bb, self.nodes[bb].blocks.remove(&r).unwrap())) + .collect(); + (blocks, blocked_by) + } + + fn predecessors(&self, r: RegionVid) -> FxHashSet { + let mut predecessors = FxHashSet::default(); + self.predecessors_helper(r, &mut predecessors); + predecessors + } + fn predecessors_helper(&self, r: RegionVid, visited: &mut FxHashSet) { + let tp: Vec<_> = self.nodes[r] + .blocked_by + .iter() + .copied() + .filter(|r| visited.insert(*r)) + .collect(); + for r in tp { + self.predecessors_helper(r, visited) + } + } + fn successors(&self, r: RegionVid) -> FxHashSet { + let mut successors = FxHashSet::default(); + self.successors_helper(r, &mut successors); + successors + } + fn successors_helper(&self, r: RegionVid, visited: &mut FxHashSet) { + let tp: Vec<_> = self.nodes[r] + .blocks + .iter() + .map(|(r, _)| *r) + .filter(|r| visited.insert(*r)) + .collect(); + for r in tp { + self.successors_helper(r, visited) + } + } +} + +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Node<'tcx> { + pub blocks: FxHashMap>>>, + pub blocked_by: FxHashSet, +} + +impl<'tcx> Node<'tcx> { + pub fn new() -> Self { + Self { + blocks: FxHashMap::default(), + blocked_by: FxHashSet::default(), + } + } + pub fn true_edges(&self) -> Vec { + self.blocks + .iter() + .filter(|(_, edges)| edges.iter().any(|edge| Edge::is_blocking(edge))) + .map(|(&r, _)| r) + .collect() + } +} diff --git a/mir-state-analysis/src/coupling_graph/impl/join_semi_lattice.rs b/mir-state-analysis/src/coupling_graph/impl/join_semi_lattice.rs new file mode 100644 index 00000000000..d7b635ab2ba --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/impl/join_semi_lattice.rs @@ -0,0 +1,77 @@ +// © 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::collections::hash_map::Entry; + +use prusti_rustc_interface::{dataflow::JoinSemiLattice, middle::mir::Location}; + +use crate::{ + coupling_graph::{ + consistency::CouplingConsistency, + coupling::{Block, CouplingOp}, + outlives_info::edge::{Edge, EdgeInfo, EdgeOrigin}, + }, + free_pcs::{ + CapabilityKind, CapabilityLocal, CapabilityProjections, CapabilitySummary, Fpcs, RepackOp, + }, + utils::{PlaceOrdering, PlaceRepacker}, +}; + +use super::{graph::Graph, triple::Cg}; + +impl JoinSemiLattice for Cg<'_, '_> { + #[tracing::instrument(name = "Cg::join", level = "debug", ret)] + fn join(&mut self, other: &Self) -> bool { + let version = self.version.entry(other.location.block).or_default(); + *version += 1; + assert!(*version < 20, "{:?} -> {:?}", other.location, self.location); + + let loop_head = self.cgx.loops.loop_head_of(self.location.block); + let top = |sup, sub| { + EdgeInfo::no_reason(sup, sub, Some(self.location), EdgeOrigin::Opaque).to_edge(self.cgx) + }; + let needs_widening = |loc: Location| { + loop_head + .map(|l| self.cgx.loops.in_loop(loc.block, l)) + .unwrap_or_default() + }; + // Are we looping back into the loop head from within the loop? + let loop_into = loop_head.map(|l| self.cgx.loops.in_loop(other.location.block, l)); + let mut changed = false; + for (_, node) in other.graph.all_nodes() { + for (_, edges) in node.blocks.iter() { + for edge in edges { + let edge = Edge::widen(edge, top, needs_widening); + let was_new = self.graph.outlives_join(edge); + changed = changed || was_new.is_some(); + } + } + } + let old_len = self.graph.inactive_loans.len(); + self.graph + .inactive_loans + .extend(other.graph.inactive_loans.iter().copied()); + changed = changed || old_len != self.graph.inactive_loans.len(); + changed + } +} + +impl Cg<'_, '_> { + #[tracing::instrument(name = "Cg::bridge", level = "debug", fields(self.graph = ?self.graph, other.graph = ?self.graph), ret)] + pub fn bridge(&self, other: &Self) -> Vec { + other + .graph + .all_nodes() + .flat_map(|(sub, node)| { + node.true_edges() + .into_iter() + .filter(move |sup| !self.graph.nodes[sub].blocks.contains_key(sup)) + .map(move |sup| self.outlives_to_block((sup, sub, true)).unwrap()) + .map(|block| CouplingOp::Add(block)) + }) + .collect() + } +} diff --git a/mir-state-analysis/src/coupling_graph/impl/mod.rs b/mir-state-analysis/src/coupling_graph/impl/mod.rs new file mode 100644 index 00000000000..0b18bc46fac --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/impl/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/. + +pub(crate) mod engine; +pub(crate) mod graph; +pub(crate) mod join_semi_lattice; +pub(crate) mod triple; +mod dot; diff --git a/mir-state-analysis/src/coupling_graph/impl/triple.rs b/mir-state-analysis/src/coupling_graph/impl/triple.rs new file mode 100644 index 00000000000..4b0343ab0fe --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/impl/triple.rs @@ -0,0 +1,455 @@ +// © 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::{ + borrow::Cow, + fmt::{Debug, Display, Formatter, Result}, +}; + +use derive_more::{Deref, DerefMut}; +use prusti_interface::environment::borrowck::facts::{BorrowckFacts, BorrowckFacts2}; +use prusti_rustc_interface::{ + borrowck::{ + borrow_set::{BorrowData, TwoPhaseActivation}, + consumers::{BorrowIndex, OutlivesConstraint, RichLocation}, + }, + data_structures::fx::{FxHashMap, FxHashSet, FxIndexMap, FxIndexSet}, + dataflow::fmt::DebugWithContext, + index::{bit_set::BitSet, IndexVec}, + middle::{ + mir::{ + interpret::{ConstValue, GlobalAlloc, Scalar}, + visit::Visitor, + BasicBlock, BorrowKind, ConstantKind, ConstraintCategory, Local, Location, Operand, + Place as MirPlace, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, + RETURN_PLACE, + }, + ty::{GenericArgKind, ParamEnv, RegionVid, TyKind}, + }, +}; + +use crate::{ + coupling_graph::{ + coupling::{Block, CouplingOp}, + outlives_info::edge::{EdgeInfo, EdgeOrigin}, + region_info::map::{Promote, RegionKind}, + CgContext, + }, + free_pcs::{ + engine::FreePlaceCapabilitySummary, CapabilityKind, CapabilityLocal, CapabilityProjections, + RepackOp, + }, + utils::{r#const::ConstEval, Place, PlaceRepacker}, +}; + +use super::{ + engine::{BorrowDelta, CouplingGraph}, + graph::{Graph, Node}, +}; + +#[derive(Clone)] +pub struct Cg<'a, 'tcx> { + pub location: Location, + pub is_pre: bool, + pub cgx: &'a CgContext<'a, 'tcx>, + + pub(crate) live: BitSet, + pub version: FxHashMap, + pub dot_node_filter: fn(&RegionKind<'_>) -> bool, + pub dot_edge_filter: fn(&RegionKind<'_>, &RegionKind<'_>) -> bool, + pub top_crates: bool, + + pub graph: Graph<'tcx>, + + pub couplings: Vec, + pub touched: FxHashSet, +} + +impl Debug for Cg<'_, '_> { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + f.debug_struct("Graph") + .field("location", &self.location) + .field("version", &self.version) + // .field("nodes", &self.graph) + .finish() + } +} + +impl PartialEq for Cg<'_, '_> { + fn eq(&self, other: &Self) -> bool { + self.graph == other.graph + } +} +impl Eq for Cg<'_, '_> {} + +impl<'a, 'tcx> DebugWithContext> for Cg<'a, 'tcx> { + fn fmt_diff_with( + &self, + old: &Self, + _ctxt: &CouplingGraph<'a, 'tcx>, + f: &mut Formatter<'_>, + ) -> Result { + for op in &self.couplings { + writeln!(f, "{op}")?; + } + Ok(()) + } +} + +impl<'a, 'tcx: 'a> Cg<'a, 'tcx> { + pub fn static_region(&self) -> RegionVid { + self.cgx.region_info.static_region + } + pub fn function_region(&self) -> RegionVid { + self.cgx.region_info.function_region + } + + #[tracing::instrument(name = "Cg::new", level = "trace", skip_all)] + pub fn new(cgx: &'a CgContext<'a, 'tcx>, top_crates: bool, location: Location) -> Self { + let graph = Graph { + nodes: IndexVec::from_elem_n(Node::new(), cgx.region_info.map.region_len()), + static_regions: FxHashSet::from_iter([cgx.region_info.static_region]), + inactive_loans: FxHashSet::default(), + }; + + let live = BitSet::new_empty(cgx.facts2.borrow_set.location_map.len()); + Self { + location, + is_pre: true, + cgx, + live, + version: FxHashMap::default(), + dot_node_filter: |_| true, + dot_edge_filter: |_, _| true, + top_crates, + graph, + couplings: Vec::new(), + touched: FxHashSet::default(), + } + } + pub fn initialize_start_block(&mut self) { + for c in &self.cgx.outlives_info.local_constraints { + self.outlives(*c); + } + for c in &self.cgx.outlives_info.universal_local_constraints { + self.outlives(*c); + } + for &(sup, sub) in &self.cgx.outlives_info.universal_constraints { + self.outlives_placeholder(sup, sub, EdgeOrigin::RustcUniversal); + } + for &const_region in self.cgx.region_info.map.const_regions() { + self.outlives_static(const_region, EdgeOrigin::Static); + } + // Remove all locals without capabilities from the initial graph + self.kill_shared_borrows_on_place(None, RETURN_PLACE.into()); + for local in self.cgx.rp.body().vars_and_temps_iter() { + self.kill_shared_borrows_on_place(None, local.into()); + } + } + pub fn sum_version(&self) -> usize { + self.version.values().copied().sum::() + } + + pub(crate) fn outlives(&mut self, c: OutlivesConstraint<'tcx>) { + let edge = EdgeInfo::from(c).to_edge(self.cgx); + let new = self.graph.outlives(edge); + self.outlives_op(new) + } + pub(crate) fn outlives_static(&mut self, r: RegionVid, origin: EdgeOrigin) { + let static_region = self.static_region(); + if r == static_region { + return; + } + self.outlives_placeholder(r, static_region, origin) + } + pub(crate) fn outlives_placeholder( + &mut self, + r: RegionVid, + placeholder: RegionVid, + origin: EdgeOrigin, + ) { + let edge = EdgeInfo::no_reason(r, placeholder, None, origin).to_edge(self.cgx); + // let new = self.graph.outlives_placeholder(r, placeholder, origin); + let new = self.graph.outlives(edge); + self.outlives_op(new) + } + #[tracing::instrument(name = "Cg::outlives_op", level = "trace", skip(self))] + fn outlives_op(&mut self, op: Option<(RegionVid, RegionVid, bool)>) { + if let Some(block) = op.and_then(|c| self.outlives_to_block(c)) { + self.couplings.push(CouplingOp::Add(block)); + } + } + + // TODO: remove + pub(crate) fn outlives_to_block(&self, op: (RegionVid, RegionVid, bool)) -> Option { + let (sup, sub, is_blocking) = op; + if is_blocking { + let waiting_to_activate = self.graph.inactive_loans.contains(&sup); + Some(Block { + sup, + sub, + waiting_to_activate, + }) + } else { + None + } + } + #[tracing::instrument(name = "Cg::remove", level = "debug", skip(self))] + pub(crate) fn remove(&mut self, r: RegionVid, l: Option) { + let remove = self.graph.remove(r); + if let Some(op) = remove { + self.remove_op(op); + } + } + #[tracing::instrument(name = "Cg::outlives_op", level = "trace", skip(self))] + fn remove_op(&mut self, op: (RegionVid, Vec<(RegionVid, RegionVid, bool)>)) { + let rejoins = + op.1.into_iter() + .flat_map(|c| self.outlives_to_block(c)) + .collect(); + self.couplings.push(CouplingOp::Remove(op.0, rejoins)); + } + #[tracing::instrument(name = "Cg::remove", level = "debug", skip(self), ret)] + pub(crate) fn remove_many(&mut self, mut r: FxHashSet) { + let ops = self.graph.remove_many(&r); + for op in ops { + r.remove(&op.0); + self.remove_op(op); + } + for removed in r { + self.couplings.push(CouplingOp::Remove(removed, Vec::new())); + } + // let rejoins = rejoins.into_iter().flat_map(|c| self.outlives_to_block(c)).collect(); + // self.couplings.push(CouplingOp::RemoveMany(removed, rejoins)); + } + #[tracing::instrument(name = "Cg::kill_borrow", level = "trace", skip(self))] + pub(crate) fn kill_borrow(&mut self, data: &BorrowData<'tcx>) { + let remove = self.graph.kill_borrow(data); + for removed in remove.into_iter().rev() { + self.couplings.push(CouplingOp::Remove(removed, Vec::new())); + } + } + pub(crate) fn reset_ops(&mut self) { + for c in self.couplings.drain(..) { + self.touched.extend(c.regions()); + } + } + + #[tracing::instrument(name = "get_associated_place", level = "trace", skip(self), ret)] + pub(crate) fn get_kind(&self, r: RegionVid) -> &RegionKind<'tcx> { + self.cgx.region_info.map.get(r) + } + #[tracing::instrument(name = "is_unknown_local", level = "trace", skip(self), ret)] + pub(crate) fn is_unknown_local(&self, r: RegionVid) -> bool { + self.get_kind(r).is_unknown_local() + } + + #[tracing::instrument(name = "handle_kills", level = "debug", skip(self))] + pub fn handle_kills( + &mut self, + delta: &BorrowDelta, + oos: Option<&Vec>, + location: Location, + ) { + let input_facts = self.cgx.facts.input_facts.borrow(); + let input_facts = input_facts.as_ref().unwrap(); + let location_table = self.cgx.facts.location_table.borrow(); + let location_table = location_table.as_ref().unwrap(); + + for bi in delta.cleared.iter() { + let data = &self.cgx.facts2.borrow_set[bi]; + // println!("killed: {r:?} {killed:?} {l:?}"); + if oos.map(|oos| oos.contains(&bi)).unwrap_or_default() { + if self.graph.static_regions.contains(&data.region) { + self.output_to_dot("log/coupling/kill.dot", true); + } + assert!( + !self.graph.static_regions.contains(&data.region), + "{data:?} {location:?} {:?}", + self.graph.static_regions + ); + self.kill_borrow(data); + } else { + self.remove(data.region, Some(location)); + } + + // // TODO: is this necessary? + // let local = data.borrowed_place.local; + // for region in input_facts.use_of_var_derefs_origin.iter().filter(|(l, _)| *l == local).map(|(_, r)| *r) { + // // println!("killed region: {region:?}"); + // state.output_to_dot("log/coupling/kill.dot"); + // let removed = state.remove(region, location, true, false); + // // assert!(!removed, "killed region: {region:?} at {location:?} (local: {local:?})"); + // } + } + + if let Some(oos) = oos { + for &bi in oos { + // What is the difference between the two (oos)? It's that `delta.cleared` may kill it earlier than `oos` + // imo we want to completely disregard `oos`. (TODO) + // assert!(delta.cleared.contains(bi), "Cleared borrow not in out of scope: {:?} vs {:?} (@ {location:?})", delta.cleared, oos); + if delta.cleared.contains(bi) { + continue; + } + + let data = &self.cgx.facts2.borrow_set[bi]; + self.kill_borrow(data); + + // // TODO: is this necessary? + // let local = data.assigned_place.local; + // for region in input_facts.use_of_var_derefs_origin.iter().filter(|(l, _)| *l == local).map(|(_, r)| *r) { + // // println!("IHUBJ local: {local:?} region: {region:?}"); + // let removed = state.remove(region, location, true, false); + // assert!(!removed); + // } + } + } + + if let Some(borrow) = self.cgx.facts2.borrow_set.location_map.get(&location) { + if let TwoPhaseActivation::ActivatedAt(_) = borrow.activation_location { + self.graph.inactive_loans.insert(borrow.region); + } + } + if let Some(activations) = self.cgx.facts2.borrow_set.activation_map.get(&location) { + for activated in activations { + let borrow = &self.cgx.facts2.borrow_set[*activated]; + let contained = self.graph.inactive_loans.remove(&borrow.region); + assert!(contained); + self.couplings.push(CouplingOp::Activate(borrow.region)); + } + } + } + + #[tracing::instrument(name = "handle_outlives", level = "debug", skip(self))] + pub fn handle_outlives(&mut self, location: Location, assigns_to: Option>) { + let local = assigns_to.map(|a| a.local); + for &c in self + .cgx + .outlives_info + .pre_constraints(location, local, &self.cgx.region_info) + { + self.outlives(c); + } + if let Some(place) = assigns_to { + self.kill_shared_borrows_on_place(Some(location), place); + } + for &c in self + .cgx + .outlives_info + .post_constraints(location, local, &self.cgx.region_info) + { + self.outlives(c); + } + } + + #[tracing::instrument(name = "kill_shared_borrows_on_place", level = "debug", skip(self))] + pub fn kill_shared_borrows_on_place( + &mut self, + location: Option, + place: MirPlace<'tcx>, + ) { + let Some(local) = place.as_local() else { + // Only remove nodes if assigned to the entire local (this is what rustc allows too) + return; + }; + for region in self.cgx.region_info.map.all_regions() { + if self.cgx.region_info.map.for_local(region, local) { + self.remove(region, location); + } + } + } +} + +impl<'tcx> Visitor<'tcx> for Cg<'_, 'tcx> { + fn visit_operand(&mut self, operand: &Operand<'tcx>, location: Location) { + self.super_operand(operand, location); + match operand { + Operand::Copy(_) => (), + &Operand::Move(place) => { + self.kill_shared_borrows_on_place(Some(location), place); + } + Operand::Constant(_) => (), + } + } + fn visit_statement(&mut self, statement: &Statement<'tcx>, location: Location) { + self.super_statement(statement, location); + match &statement.kind { + StatementKind::AscribeUserType(box (p, _), _) => { + for &c in self + .cgx + .outlives_info + .type_ascription_constraints + .iter() + .filter(|c| { + self.cgx.region_info.map.for_local(c.sup, p.local) + || self.cgx.region_info.map.for_local(c.sub, p.local) + }) + { + self.outlives(c); + } + } + _ => (), + } + } +} + +impl<'tcx> Cg<'_, 'tcx> { + #[tracing::instrument(name = "Cg::merge_for_return", level = "debug")] + pub fn merge_for_return(&mut self, location: Location) { + let regions: Vec<_> = self.graph.all_nodes().map(|(r, _)| r).collect(); + let mut to_remove = FxHashSet::default(); + for r in regions { + let kind = self.cgx.region_info.map.get(r); + match kind { + RegionKind::Static + | RegionKind::Param(_) + | RegionKind::UnknownUniversal + | RegionKind::Function => continue, + RegionKind::Place { + local, + promoted: Promote::NotPromoted, + .. + } => { + if local.index() > self.cgx.rp.body().arg_count { + self.output_to_dot("log/coupling/error.dot", true); + panic!("{r:?} ({location:?}) {:?}", self.graph.nodes[r]); + } + } + RegionKind::Borrow(_, Promote::NotPromoted) => { + // Should not have borrows left + self.output_to_dot("log/coupling/error.dot", true); + panic!("{r:?} {:?}", self.graph.nodes[r]); + } + // Ignore (and thus delete) early/late bound (mostly fn call) regions + RegionKind::UnusedReturnBug(..) => unreachable!(), + RegionKind::Place { + promoted: Promote::Promoted(..), + .. + } => (), + RegionKind::Borrow(_, Promote::Promoted(..)) => (), + RegionKind::ConstRef(..) => (), + RegionKind::EarlyBound(..) => (), + RegionKind::LateBound { .. } => (), + RegionKind::Placeholder(..) => (), + RegionKind::MiscLocal => (), + RegionKind::ProjectionAnnotation(..) => (), + RegionKind::OtherAnnotation(..) => (), + // Skip unknown empty nodes, we may want to figure out how to deal with them in the future + RegionKind::UnknownLocal => (), + } + to_remove.insert(r); + } + self.remove_many(to_remove); + } + #[tracing::instrument(name = "Cg::output_to_dot", level = "debug", skip_all)] + pub fn output_to_dot>(&self, path: P, error: bool) { + if cfg!(debug_assertions) && (!self.top_crates || error) { + std::fs::create_dir_all("log/coupling/individual").unwrap(); + let mut f = std::fs::File::create(path).unwrap(); + dot::render(self, &mut f).unwrap(); + } + } +} diff --git a/mir-state-analysis/src/coupling_graph/mod.rs b/mir-state-analysis/src/coupling_graph/mod.rs new file mode 100644 index 00000000000..5357a6596d6 --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/mod.rs @@ -0,0 +1,15 @@ +// © 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 r#impl; +mod context; +mod results; +mod check; + +pub use check::*; +pub use context::*; +pub use r#impl::*; +pub use results::*; diff --git a/mir-state-analysis/src/coupling_graph/results/coupling.rs b/mir-state-analysis/src/coupling_graph/results/coupling.rs new file mode 100644 index 00000000000..722bbb62b6c --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/results/coupling.rs @@ -0,0 +1,75 @@ +// © 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, ty::RegionVid}; + +use crate::{free_pcs::CapabilityKind, utils::Place}; + +#[derive(Clone, Debug, Eq, PartialEq)] +pub enum CouplingOp { + Add(Block), + Remove(RegionVid, Vec), + Activate(RegionVid), +} + +impl CouplingOp { + pub fn regions(&self) -> Box + '_> { + match self { + CouplingOp::Add(block) => Box::new([block.sup, block.sub].into_iter()), + CouplingOp::Remove(remove, block) => Box::new( + [*remove] + .into_iter() + .chain(block.iter().flat_map(|b| [b.sup, b.sub].into_iter())), + ), + CouplingOp::Activate(region) => Box::new([*region].into_iter()), + } + } +} + +impl Display for CouplingOp { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + match self { + CouplingOp::Add(block) => block.fmt(f), + CouplingOp::Remove(remove, patch) => { + write!(f, "Remove({remove:?}, {{")?; + for p in patch { + write!(f, "\n {p}")?; + } + if !patch.is_empty() { + write!(f, "\n")?; + } + write!(f, "}})") + } + CouplingOp::Activate(region) => write!(f, "Activate({region:?})"), + } + } +} + +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +pub struct Block { + /// The region that outlives (is blocked) + pub sup: RegionVid, + /// The region that must be outlived (is blocking) + pub sub: RegionVid, + // pub kind: CapabilityKind, + pub waiting_to_activate: bool, +} +impl Display for Block { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + let Block { + sup, + sub, + waiting_to_activate, + } = *self; + write!( + f, + "Block({sup:?}, {sub:?}){}", + if waiting_to_activate { "?" } else { "" } + ) + } +} diff --git a/mir-state-analysis/src/coupling_graph/results/cursor.rs b/mir-state-analysis/src/coupling_graph/results/cursor.rs new file mode 100644 index 00000000000..0ac4766aa35 --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/results/cursor.rs @@ -0,0 +1,166 @@ +// © 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::{ + coupling_graph::{engine::CouplingGraph, graph::Graph, CgContext}, + free_pcs::{ + engine::FreePlaceCapabilitySummary, join_semi_lattice::RepackingJoinSemiLattice, + CapabilitySummary, RepackOp, + }, + utils::PlaceRepacker, +}; + +use super::coupling::CouplingOp; + +type Cursor<'a, 'mir, 'tcx> = ResultsCursor<'mir, 'tcx, CouplingGraph<'a, 'tcx>>; + +pub struct CgAnalysis<'a, 'mir, 'tcx> { + cursor: Cursor<'a, 'mir, 'tcx>, + did_before: bool, + curr_stmt: Option, + end_stmt: Option, +} + +impl<'a, 'mir, 'tcx> CgAnalysis<'a, 'mir, 'tcx> { + pub(crate) fn new(cursor: Cursor<'a, 'mir, 'tcx>) -> Self { + Self { + cursor, + did_before: false, + 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() + .cgx + .rp + .body() + .terminator_loc(block) + .successor_within_block(); + self.curr_stmt = Some(Location { + block, + statement_index: 0, + }); + self.end_stmt = Some(end_stmt); + self.did_before = false; + } + + fn body(&self) -> &'a Body<'tcx> { + self.cursor.analysis().cgx.rp.body() + } + pub(crate) fn cgx(&mut self) -> &'a CgContext<'a, 'tcx> { + self.cursor.results().analysis.cgx + } + + pub fn initial_state(&self) -> &Graph<'tcx> { + &self.cursor.get().graph + } + pub fn initial_coupling(&self) -> &Vec { + &self.cursor.get().couplings + } + pub fn before_next(&mut self, exp_loc: Location) -> CgLocation<'tcx> { + let location = self.curr_stmt.unwrap(); + assert_eq!(location, exp_loc); + assert!(location <= self.end_stmt.unwrap()); + assert!(!self.did_before); + self.did_before = true; + self.cursor.seek_before_primary_effect(location); + let state = self.cursor.get(); + CgLocation { + location, + state: state.graph.clone(), + couplings: state.couplings.clone(), + } + } + pub fn next(&mut self, exp_loc: Location) -> CgLocation<'tcx> { + let location = self.curr_stmt.unwrap(); + assert_eq!(location, exp_loc); + assert!(location < self.end_stmt.unwrap()); + assert!(self.did_before); + self.did_before = false; + self.curr_stmt = Some(location.successor_within_block()); + + self.cursor.seek_after_primary_effect(location); + let state = self.cursor.get(); + CgLocation { + location, + state: state.graph.clone(), + couplings: state.couplings.clone(), + } + } + pub fn terminator(&mut self) -> CgTerminator<'tcx> { + let location = self.curr_stmt.unwrap(); + assert!(location == self.end_stmt.unwrap()); + assert!(!self.did_before); + self.curr_stmt = None; + self.end_stmt = None; + + // TODO: cleanup + 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); + CgLocation { + location: Location { + block: succ, + statement_index: 0, + }, + state: to.graph.clone(), + couplings: state.bridge(&to), + } + }) + .collect(); + CgTerminator { succs } + } + + /// Recommened interface. + /// Does *not* require that one calls `analysis_for_bb` first + pub fn get_all_for_bb(&mut self, block: BasicBlock) -> CgBasicBlock<'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(); + CgBasicBlock { + statements, + terminator, + } + } +} + +pub struct CgBasicBlock<'tcx> { + pub statements: Vec>, + pub terminator: CgTerminator<'tcx>, +} + +#[derive(Debug)] +pub struct CgLocation<'tcx> { + pub location: Location, + /// Couplings before the statement + pub couplings: Vec, + /// State after the statement + pub state: Graph<'tcx>, +} + +#[derive(Debug)] +pub struct CgTerminator<'tcx> { + pub succs: Vec>, +} diff --git a/mir-state-analysis/src/coupling_graph/results/mod.rs b/mir-state-analysis/src/coupling_graph/results/mod.rs new file mode 100644 index 00000000000..b36c4b4b0b7 --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/results/mod.rs @@ -0,0 +1,8 @@ +// © 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 coupling; +pub mod cursor; 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..ca5c728b7e5 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/check/checker.rs @@ -0,0 +1,205 @@ +// © 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, FpcsBound, FreePcsAnalysis, + RepackOp, + }, + utils::PlaceRepacker, +}; + +use super::consistency::CapabilityConsistency; + +#[tracing::instrument(name = "check", level = "debug", skip(cursor))] +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, + bound: FpcsBound::empty(false), + }; + // 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(name = "RepackOp::update_free", level = "debug", skip(rp))] + pub(crate) 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..a7492e4d7c6 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/check/consistency.rs @@ -0,0 +1,63 @@ +// © 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 CapabilityConsistency<'tcx> { + fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>); +} + +impl<'tcx, T: CapabilityConsistency<'tcx>> CapabilityConsistency<'tcx> for Summary { + #[tracing::instrument( + name = "Summary::consistency_check", + level = "trace", + skip(self, repacker) + )] + fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>) { + for p in self.iter() { + p.consistency_check(repacker) + } + } +} + +impl<'tcx> CapabilityConsistency<'tcx> for CapabilityLocal<'tcx> { + fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>) { + match self { + CapabilityLocal::Unallocated => {} + CapabilityLocal::Allocated(cp) => cp.consistency_check(repacker), + } + } +} + +impl<'tcx> CapabilityConsistency<'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..ab93cd14b65 --- /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; +pub(crate) 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..3f58b2c6bba --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/engine.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 prusti_rustc_interface::{ + dataflow::{Analysis, AnalysisDomain}, + index::{Idx, IndexVec}, + middle::{ + mir::{ + visit::Visitor, BasicBlock, Body, CallReturnPlaces, Local, Location, Promoted, + 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>, + promoted: &'a IndexVec>, + ) -> Self { + let repacker = PlaceRepacker::new(body, promoted, 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..b553a1052c9 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/fpcs.rs @@ -0,0 +1,182 @@ +// © 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::{ + cell::RefCell, + 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::{Place, PlaceRepacker}, +}; + +use super::CapabilityKind; + +pub struct FpcsBound<'tcx>( + pub Option) -> CapabilityKind>>, + pub bool, +); +impl FpcsBound<'_> { + pub fn empty(expect: bool) -> RefCell { + RefCell::new(Self(None, expect)) + } +} + +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>, + pub bound: RefCell>, +} +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(), + bound: FpcsBound::empty(false), + } + } + #[tracing::instrument(name = "Fpcs::bound", level = "trace", skip(self), ret)] + pub(crate) fn bound(&self, place: Place<'tcx>) -> CapabilityKind { + let bound = self.bound.borrow(); + assert_eq!(bound.1, bound.0.is_some()); + bound + .0 + .as_ref() + .map(|b| b(place)) + .unwrap_or(CapabilityKind::Exclusive) + } +} + +impl Clone for Fpcs<'_, '_> { + fn clone(&self) -> Self { + let expect_bound = self.bound.borrow().1; + Self { + repacker: self.repacker, + bottom: self.bottom, + apply_pre_effect: self.apply_pre_effect, + summary: self.summary.clone(), + repackings: self.repackings.clone(), + bound: FpcsBound::empty(expect_bound), + } + } +} +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 Debug for Fpcs<'_, '_> { + 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..0b98b36cb0b --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/join_semi_lattice.rs @@ -0,0 +1,197 @@ +// © 2023, ETH Zurich +// +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. + +use prusti_rustc_interface::dataflow::JoinSemiLattice; + +use crate::{ + 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 + } + + #[tracing::instrument(name = "CapabilitySummary::bridge", level = "trace", skip(repacker))] + 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..fb31c557c09 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/place.rs @@ -0,0 +1,116 @@ +// © 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, + + /// The capability was `Exclusive` but has been blocked by a shared borrow. + Read, + /// The capability was `Exclusive` but has been blocked by a mutable borrow. + None, +} +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"), + CapabilityKind::Read => write!(f, "R"), + CapabilityKind::None => write!(f, "N"), + } + } +} + +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::Exclusive) + | (CapabilityKind::None, _) + | (CapabilityKind::Write, CapabilityKind::ShallowExclusive) => Some(Ordering::Less), + // E > W, e > W + (CapabilityKind::Exclusive, _) + | (_, CapabilityKind::None) + | (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 is_read(self) -> bool { + matches!(self, CapabilityKind::Read) + } + pub fn is_none(self) -> bool { + matches!(self, CapabilityKind::None) + } + #[tracing::instrument(name = "CapabilityKind::minimum", level = "trace", ret)] + pub fn minimum(self, other: Self) -> Option { + match self.partial_cmp(&other)? { + Ordering::Greater => Some(other), + _ => Some(self), + } + } + #[tracing::instrument(name = "CapabilityKind::sum", level = "trace", ret)] + pub fn sum(self, other: Self) -> Option { + match (self, other) { + (other, CapabilityKind::None) | (CapabilityKind::None, other) => Some(other), + (CapabilityKind::Write, CapabilityKind::Read) => Some(CapabilityKind::Exclusive), + _ => None, + } + } +} 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..dcfe3a83e47 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/triple.rs @@ -0,0 +1,184 @@ +// © 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> { + #[tracing::instrument(name = "Fpcs::visit_operand", level = "debug", skip(self))] + 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(..) => (), + } + } + + #[tracing::instrument(name = "Fpcs::visit_statement", level = "debug", skip(self))] + 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)) => self.requires_read(place), + &PlaceMention(box place) => self.requires_alloc(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 => (), + }; + } + + #[tracing::instrument(name = "Fpcs::visit_terminator", level = "debug", skip(self))] + 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:?}"), + }; + } + + #[tracing::instrument(name = "Fpcs::visit_rvalue", level = "debug", skip(self))] + 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..7d276213cea --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/update.rs @@ -0,0 +1,130 @@ +// © 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)) + } + } + // TODO: make this work properly through references (i.e. check that the lifetime is live) + #[tracing::instrument(name = "Fpcs::requires_alloc", level = "trace")] + pub(crate) fn requires_alloc(&mut self, place: impl Into> + Debug) { + let place = place.into(); + self.requires(place, CapabilityKind::None) + } + #[tracing::instrument(name = "Fpcs::requires_read", level = "trace")] + pub(crate) fn requires_read(&mut self, place: impl Into> + Debug) { + let place = place.into(); + self.requires(place, CapabilityKind::Read) + } + /// 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: Place<'tcx>, cap: CapabilityKind) { + 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)); + } + }; + let bounded = self.bound(place).minimum(kind).unwrap(); + assert!(bounded >= 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> { + #[tracing::instrument( + name = "CapabilityProjections::repack", + level = "trace", + skip(repacker), + ret + )] + 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..f7f90adbf92 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/results/cursor.rs @@ -0,0 +1,155 @@ +// © 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, + CapabilityKind, CapabilitySummary, RepackOp, + }, + utils::{Place, 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 set_bound_non_empty(&self) { + self.cursor.get().bound.borrow_mut().1 = true; + } + pub fn set_bound(&self, bound: Box) -> CapabilityKind>) { + self.cursor.get().bound.borrow_mut().0 = Some(bound); + } + pub fn unset_bound(&self) { + self.cursor.get().bound.borrow_mut().0 = None; + } + 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..ea477109a7e --- /dev/null +++ b/mir-state-analysis/src/lib.rs @@ -0,0 +1,92 @@ +// © 2023, ETH Zurich +// +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. + +#![feature(rustc_private)] +#![feature(box_patterns, hash_extract_if, extract_if)] + +pub mod free_pcs; +pub mod utils; +pub mod coupling_graph; +pub mod r#loop; + +use prusti_interface::environment::borrowck::facts::{BorrowckFacts, BorrowckFacts2}; +use prusti_rustc_interface::{ + dataflow::Analysis, + index::IndexVec, + middle::{ + mir::{Body, Promoted, START_BLOCK}, + ty::TyCtxt, + }, +}; + +#[tracing::instrument(name = "run_free_pcs", level = "debug", skip(tcx))] +pub fn run_free_pcs<'mir, 'tcx>( + mir: &'mir Body<'tcx>, + promoted: &'mir IndexVec>, + tcx: TyCtxt<'tcx>, +) -> free_pcs::FreePcsAnalysis<'mir, 'tcx> { + let fpcs = free_pcs::engine::FreePlaceCapabilitySummary::new(tcx, mir, promoted); + 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>, + promoted: &IndexVec>, + tcx: TyCtxt<'tcx>, +) { + let analysis = run_free_pcs(mir, promoted, tcx); + free_pcs::check(analysis); +} + +#[tracing::instrument(name = "run_coupling_graph", level = "debug", skip(tcx))] +pub fn run_coupling_graph<'mir, 'tcx>( + mir: &'mir Body<'tcx>, + cgx: &'mir coupling_graph::CgContext<'mir, 'tcx>, + tcx: TyCtxt<'tcx>, + top_crates: bool, +) -> coupling_graph::cursor::CgAnalysis<'mir, 'mir, 'tcx> { + // if tcx.item_name(mir.source.def_id()).as_str().starts_with("main") { + // return; + // } + let fpcs = coupling_graph::engine::CouplingGraph::new(&cgx, top_crates); + let analysis = fpcs + .into_engine(tcx, mir) + .pass_name("coupling_graph") + .iterate_to_fixpoint(); + let mut c = analysis.into_results_cursor(mir); + if cfg!(debug_assertions) && !top_crates { + coupling_graph::engine::draw_dots(&mut c); + } + c.seek_to_block_start(START_BLOCK); + coupling_graph::cursor::CgAnalysis::new(c) +} + +pub fn test_coupling_graph<'tcx>( + mir: &Body<'tcx>, + promoted: &IndexVec>, + facts: &BorrowckFacts, + facts2: &BorrowckFacts2<'tcx>, + tcx: TyCtxt<'tcx>, + top_crates: bool, +) { + // println!("{:?}", mir.source.def_id()); + // if !format!("{:?}", mir.source.def_id()) + // .ends_with("parse_delimited)") + // { + // return; + // } + + let fpcs_analysis = run_free_pcs(mir, promoted, tcx); + let cgx = coupling_graph::CgContext::new(tcx, mir, promoted, facts, facts2); + let cg_analysis = run_coupling_graph(mir, &cgx, tcx, top_crates); + coupling_graph::check(cg_analysis, fpcs_analysis); + + // panic!() +} diff --git a/mir-state-analysis/src/loop/mod.rs b/mir-state-analysis/src/loop/mod.rs new file mode 100644 index 00000000000..c6a954e4895 --- /dev/null +++ b/mir-state-analysis/src/loop/mod.rs @@ -0,0 +1,175 @@ +// © 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::{ + index::{Idx, IndexVec}, + middle::mir::{BasicBlock, Body, START_BLOCK}, +}; + +#[derive(Clone, Debug)] +struct LoopSet { + // Tracks up to 64 loops inline + data: smallvec::SmallVec<[u8; 8]>, +} +impl LoopSet { + const OFFSET: usize = 8 * std::mem::size_of::(); + + fn new() -> Self { + Self { + data: smallvec::SmallVec::from_const([0; 8]), + } + } + fn add(&mut self, loop_idx: LoopId) { + let loop_idx = loop_idx.index(); + let idx = loop_idx / Self::OFFSET; + if idx >= self.data.len() { + self.data.resize(idx + 1, 0); + } + self.data[idx] |= 1 << (loop_idx % Self::OFFSET); + } + fn merge(&mut self, other: &Self) { + if other.data.len() > self.data.len() { + self.data.resize(other.data.len(), 0); + } + for (idx, val) in other.data.iter().enumerate() { + self.data[idx] |= val; + } + } + fn clear(&mut self, loop_idx: LoopId) { + let loop_idx = loop_idx.index(); + let idx = loop_idx / Self::OFFSET; + assert!(idx < self.data.len()); + self.data[idx] &= !(1 << (loop_idx % Self::OFFSET)); + } + fn contains(&self, loop_idx: LoopId) -> bool { + let loop_idx = loop_idx.index(); + let idx = loop_idx / Self::OFFSET; + if idx >= self.data.len() { + return false; + } + self.data[idx] & (1 << (loop_idx % Self::OFFSET)) != 0 + } + fn iter(&self) -> impl DoubleEndedIterator + '_ { + self.data.iter().enumerate().flat_map(|(idx, &val)| { + let to = if val == 0 { 0 } else { Self::OFFSET }; + (0..to) + .filter(move |&i| val & (1 << i) != 0) + .map(move |i| LoopId::new(idx * Self::OFFSET + i)) + }) + } +} + +#[derive(Debug)] +pub struct LoopAnalysis { + bb_data: IndexVec, + loop_heads: IndexVec, +} + +impl LoopAnalysis { + pub fn find_loops(body: &Body) -> Self { + let mut analysis = LoopAnalysis { + bb_data: IndexVec::from_elem_n(LoopSet::new(), body.basic_blocks.len()), + loop_heads: IndexVec::new(), + }; + let raw_bb_data: *const _ = &analysis.bb_data; + + let mut visited_bbs: IndexVec = + IndexVec::from_elem_n(false, body.basic_blocks.len()); + + let mut loop_head_bb_index: IndexVec = + IndexVec::from_elem_n(NO_LOOP, body.basic_blocks.len()); + for bb in body.basic_blocks.reverse_postorder().iter().copied().rev() { + let data = &mut analysis.bb_data[bb]; + for succ in body.basic_blocks[bb].terminator().successors() { + if visited_bbs[succ] { + // Merge in loops of this succ + assert_ne!(bb, succ); + // SAFETY: Index is different to mutably borrowed index + let other = unsafe { &(*raw_bb_data)[succ] }; + data.merge(other); + // If `succ` is a loop head, we are no longer in that loop + let loop_idx = loop_head_bb_index[succ]; + if loop_idx != NO_LOOP { + assert_eq!(analysis.loop_heads[loop_idx], succ); + data.clear(loop_idx); + } + } else { + // Create new loop + let loop_idx = &mut loop_head_bb_index[succ]; + if *loop_idx == NO_LOOP { + *loop_idx = LoopId::new(analysis.loop_heads.len()); + analysis.loop_heads.push(succ); + } + data.add(*loop_idx); + } + } + visited_bbs[bb] = true; + } + if cfg!(debug_assertions) { + analysis.consistency_check(); + } + analysis + } + pub fn in_loop(&self, bb: BasicBlock, l: LoopId) -> bool { + self.bb_data[bb].contains(l) + } + pub fn loops(&self, bb: BasicBlock) -> impl DoubleEndedIterator + '_ { + self.bb_data[bb].iter() + } + pub fn loop_depth(&self, bb: BasicBlock) -> usize { + self.loops(bb).count() + } + pub fn loop_nest_depth(&self, l: LoopId) -> usize { + self.loop_depth(self[l]) - 1 + } + /// Returns the loop which contains `bb` as well as all other loops of `bb`. + pub fn outermost_loop(&self, bb: BasicBlock) -> Option { + self.loops(bb).min_by_key(|l| self.loop_nest_depth(*l)) + } + /// Returns the loop which contains `bb` but no other loops of `bb`. + pub fn innermost_loop(&self, bb: BasicBlock) -> Option { + self.loops(bb).max_by_key(|l| self.loop_nest_depth(*l)) + } + /// If `bb` is a loop head, return the loop for which it is the head. + pub fn loop_head_of(&self, bb: BasicBlock) -> Option { + self.loops(bb).find(|l| self[*l] == bb) + } + + fn consistency_check(&self) { + // Start block can be in a maximum of one loop, of which it is the head + let mut start_loops: Vec<_> = self.loops(START_BLOCK).collect(); + if let Some(l) = start_loops.pop() { + assert_eq!(self[l], START_BLOCK); + } + assert!(start_loops.is_empty()); + // A bb can only be the loop head of a single loop + for lh in &self.loop_heads { + assert_eq!( + self.loop_heads.iter().filter(|other| *other == lh).count(), + 1 + ); + } + } +} + +impl std::ops::Index for LoopAnalysis { + type Output = BasicBlock; + fn index(&self, index: LoopId) -> &Self::Output { + &self.loop_heads[index] + } +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub struct LoopId(usize); +impl Idx for LoopId { + fn new(idx: usize) -> Self { + Self(idx) + } + fn index(self) -> usize { + self.0 + } +} +const NO_LOOP: LoopId = LoopId(usize::MAX); diff --git a/mir-state-analysis/src/utils/const/mod.rs b/mir-state-analysis/src/utils/const/mod.rs new file mode 100644 index 00000000000..a8ce58982d9 --- /dev/null +++ b/mir-state-analysis/src/utils/const/mod.rs @@ -0,0 +1,391 @@ +// © 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/. + +// This module is not used, and instead we use https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/struct.Promoted.html. +// I've kept this around as a skeleton for working with `ConstValue` and `ConstAlloc` if we ever need that in the future. + +use prusti_rustc_interface::{ + abi::{HasDataLayout, Size, TagEncoding, TargetDataLayout, VariantIdx, Variants}, + borrowck::{ + borrow_set::BorrowData, + consumers::{BorrowIndex, OutlivesConstraint, RichLocation}, + }, + data_structures::fx::{FxHashMap, FxHashSet, FxIndexMap, FxIndexSet}, + dataflow::fmt::DebugWithContext, + index::{bit_set::BitSet, IndexVec}, + middle::{ + mir::{ + interpret::{ + alloc_range, AllocId, AllocRange, Allocation, ConstAllocation, ConstValue, + GlobalAlloc, Scalar, + }, + visit::Visitor, + BasicBlock, Constant, ConstantKind, ConstraintCategory, Local, Location, Operand, + Place as MirPlace, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, + RETURN_PLACE, + }, + ty::{ + layout::{HasParamEnv, HasTyCtxt, LayoutError, TyAndLayout}, + FieldDef, FloatTy, GenericArgKind, Instance, ParamEnv, ParamEnvAnd, RegionVid, + ScalarInt, Ty, TyCtxt, TyKind, + }, + }, +}; + +use super::PlaceRepacker; + +/// Do not use, see note at the top of this module +pub struct EvaluatedConst<'tcx> { + ty: Ty<'tcx>, + kind: EcKind<'tcx>, +} + +impl<'tcx> std::fmt::Debug for EvaluatedConst<'tcx> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + self.kind.fmt(f) + } +} + +#[derive(Debug)] +pub enum EcKind<'tcx> { + // Primitive + Bool(bool), + Int(i128), + Uint(u128), // Note: Also includes `char` + Float(f64), // Note: it is lossless to store a `f32` in a `f64` + Str(&'tcx str), + // Other + ZeroSized, // Get info from `ty` + Function(Instance<'tcx>), + // Compound + Array(Vec>), + Adt(VariantIdx, Vec<(&'tcx FieldDef, EvaluatedConst<'tcx>)>), + // Reference/Pointer + Pointer(Option>>), +} + +impl<'tcx> EcKind<'tcx> { + pub fn to_bits(&self) -> Option { + match *self { + EcKind::Int(value) => Some(value as u128), + EcKind::Uint(value) => Some(value), + _ => None, + } + } +} + +pub trait ConstEval<'tcx> { + fn eval(self, rp: PlaceRepacker<'_, 'tcx>) -> EvaluatedConst<'tcx>; +} + +impl<'tcx> ConstEval<'tcx> for Constant<'tcx> { + fn eval(self, rp: PlaceRepacker<'_, 'tcx>) -> EvaluatedConst<'tcx> { + let param_env = rp.tcx().param_env(rp.body().source.def_id()); + let eval = self.literal.eval(rp.tcx(), param_env, None); + assert!(!(self.literal.try_to_scalar().is_some() && eval.is_err())); + // let eval = eval.ok()?; + // TODO: find a good way to resolve errors here + let eval = eval.unwrap(); + eval.eval(self.ty(), rp) + } +} + +pub trait ConstEvalTy<'tcx> { + fn eval(self, ty: Ty<'tcx>, rp: PlaceRepacker<'_, 'tcx>) -> EvaluatedConst<'tcx>; +} + +impl<'tcx> ConstEvalTy<'tcx> for ConstValue<'tcx> { + fn eval(self, ty: Ty<'tcx>, rp: PlaceRepacker<'_, 'tcx>) -> EvaluatedConst<'tcx> { + println!("const {self:?}, ty: {ty:?}"); + match self { + ConstValue::Scalar(scalar) => scalar.eval(ty, rp), + ConstValue::ZeroSized => EvaluatedConst { + ty, + kind: EcKind::ZeroSized, + }, + ConstValue::Slice { data, start, end } => { + let inner_ty = ty.builtin_deref(true).unwrap().ty; + let range = alloc_range(Size::from_bytes(start), Size::from_bytes(end - start)); + eval_range(data, range, inner_ty, rp) + } + ConstValue::Indirect { alloc_id, offset } => { + let alloc = rp.tcx().global_alloc(alloc_id).unwrap_memory(); + let size = alloc.inner().size() - offset; + eval_range(alloc, alloc_range(offset, size), ty, rp) + } + } + } +} + +impl<'tcx> ConstEvalTy<'tcx> for Scalar { + fn eval(self, ty: Ty<'tcx>, rp: PlaceRepacker<'_, 'tcx>) -> EvaluatedConst<'tcx> { + println!("scalar {self:?}, ty: {ty:?}"); + match self { + Scalar::Int(bytes) => bytes.eval(ty, rp), + Scalar::Ptr(ptr, _) => { + match rp.tcx().global_alloc(ptr.provenance) { + GlobalAlloc::Function(instance) => EvaluatedConst { + ty, + kind: EcKind::Function(instance), + }, + GlobalAlloc::VTable(_, _) => todo!(), + GlobalAlloc::Static(_) => todo!(), + GlobalAlloc::Memory(mem) => { + // If the `unwrap` ever panics we need a different way to get the inner type + // let inner_ty = ty.builtin_deref(true).map(|t| t.ty).unwrap_or(ty); + let inner_ty = ty.builtin_deref(true).unwrap().ty; + let inner = Box::new(mem.eval(inner_ty, rp)); + EvaluatedConst { + ty, + kind: EcKind::Pointer(Some(inner)), + } + } + } + } + } + } +} + +impl<'tcx> ConstEvalTy<'tcx> for ScalarInt { + fn eval(self, ty: Ty<'tcx>, _rp: PlaceRepacker<'_, 'tcx>) -> EvaluatedConst<'tcx> { + let kind = match ty.kind() { + TyKind::Bool => EcKind::Bool(self.try_to_bool().unwrap()), + TyKind::Int(_) => EcKind::Int(self.try_to_int(self.size()).unwrap()), + TyKind::Char | TyKind::Uint(_) => EcKind::Uint(self.try_to_uint(self.size()).unwrap()), + TyKind::Float(FloatTy::F32) => { + let float = f32::from_bits(self.try_to_u32().unwrap()); + EcKind::Float(f64::from(float)) // Lossless conversion, see https://doc.rust-lang.org/std/primitive.f32.html#method.from-3 + } + TyKind::Float(FloatTy::F64) => { + EcKind::Float(f64::from_bits(self.try_to_u64().unwrap())) + } + _ => unreachable!("ScalarInt::eval: {self:?}, ty: {ty:?}"), + }; + EvaluatedConst { ty, kind } + } +} + +impl<'tcx> ConstEvalTy<'tcx> for ConstAllocation<'tcx> { + fn eval(self, ty: Ty<'tcx>, rp: PlaceRepacker<'_, 'tcx>) -> EvaluatedConst<'tcx> { + let range = alloc_range(Size::ZERO, self.inner().size()); + eval_range(self, range, ty, rp) + } +} + +fn eval_range<'tcx>( + ca: ConstAllocation<'tcx>, + range: AllocRange, + ty: Ty<'tcx>, + rp: PlaceRepacker<'_, 'tcx>, +) -> EvaluatedConst<'tcx> { + println!("ca {ca:?}, ty: {ty:?}, range: {range:?}"); + match ty.kind() { + TyKind::Str => { + let peat = ParamEnvAnd { + param_env: ParamEnv::reveal_all(), + value: ty, + }; + let layout = rp.tcx().layout_of(peat).unwrap(); + println!("layout: {layout:?}"); + + // Cannot use `read_scalar` here: it panics if the allocation size is larger + // than can fit in u128 as it cannot create a `Scalar::Int` for the data. + let value = ca + .inner() + .get_bytes_strip_provenance(&rp.tcx(), range) + .unwrap(); + EvaluatedConst { + ty, + kind: EcKind::Str(std::str::from_utf8(value).unwrap()), + } + } + &TyKind::Array(elem_ty, _) | &TyKind::Slice(elem_ty) => { + let layout = layout_of(elem_ty, rp).unwrap(); + // println!("layout: {layout:?}"); + assert_eq!(range.size.bits() % layout.size.bits(), 0); + let elements = range.size.bits() / layout.size.bits(); + let values = (0..elements) + .map(|idx| layout.size.checked_mul(idx, &rp.tcx()).unwrap()) + .map(|offset| range.subrange(alloc_range(offset, layout.size))) + .map(|subrange| eval_range(ca, subrange, elem_ty, rp)) + .collect(); + EvaluatedConst { + ty, + kind: EcKind::Array(values), + } + } + // Always zero-sized, closures with captured state aren't const? + TyKind::FnDef(..) | TyKind::Closure(..) => { + assert_eq!(range.size.bits(), 0); + EvaluatedConst { + ty, + kind: EcKind::ZeroSized, + } + } + TyKind::Adt(adt, sub) if adt.variants().is_empty() => { + todo!() + } + TyKind::Adt(adt, sub) => { + if range.size.bits() == 0 { + return EvaluatedConst { + ty, + kind: EcKind::ZeroSized, + }; + } + let cx = &RevealAllEnv::from(rp); + let adt_layout = layout_of(ty, rp).unwrap(); + let index = match adt_layout.variants { + Variants::Single { index } => index, + Variants::Multiple { + tag, + ref tag_encoding, + tag_field, + ref variants, + } => { + let discr_type = ty.discriminant_ty(rp.tcx()); + // TODO: compare with `tag.primitive().to_int_ty(rp.tcx())` + + let discr_offset = adt_layout.fields.offset(tag_field); + let discr_layout = adt_layout.field(cx, tag_field); + // TODO: compare with `layout_of(discr_type, rp).unwrap()` + let discr_range = range.subrange(alloc_range(discr_offset, discr_layout.size)); + let discr_bits = eval_range(ca, discr_range, discr_type, rp); + let discr_bits = discr_bits.kind.to_bits().unwrap(); + match *tag_encoding { + TagEncoding::Direct => { + adt.discriminants(rp.tcx()) + .find(|(_, var)| var.val == discr_bits) + .unwrap() + .0 + } + TagEncoding::Niche { + untagged_variant, + ref niche_variants, + niche_start, + } => { + let variants_start = niche_variants.start().as_u32(); + let variants_end = niche_variants.end().as_u32(); + let variant_index_relative = discr_bits - niche_start; + if variant_index_relative <= u128::from(variants_end - variants_start) { + // We should now be within the `u32` range. + let variant_index_relative = + u32::try_from(variant_index_relative).unwrap(); + VariantIdx::from_u32( + variants_start.checked_add(variant_index_relative).unwrap(), + ) + } else { + untagged_variant + } + } + } + } + }; + let layout = adt_layout.for_variant(cx, index); + let variant = adt.variant(index); + let fields = variant + .fields + .iter_enumerated() + .map(|(idx, val)| { + let field = layout.field(cx, idx.as_usize()); + let range = range.subrange(alloc_range( + layout.fields.offset(idx.as_usize()), + field.size, + )); + (val, eval_range(ca, range, val.ty(rp.tcx(), sub), rp)) + }) + .collect(); + EvaluatedConst { + ty, + kind: EcKind::Adt(index, fields), + } + } + TyKind::Tuple(_) => todo!(), + // Note: `TyKind::FnPtr` will lead to `GlobalAlloc::Function` + _ => { + assert!( + range.size.bits() <= u128::BITS.into(), + "{ty:?}, {range:?}: {:?} / {:?}", + ca.inner().init_mask(), + ca.inner().provenance() + ); + let mut range = range; + let is_ptr = ty.is_any_ptr(); // !ca.inner().provenance().range_empty(range, &rp.tcx()); + if is_ptr { + let ptr_size = rp.tcx().data_layout().pointer_size; + if ptr_size != range.size { + // For some reason all pointer allocations get reported as + // `16 bytes` even though they are actually `8 bytes`. + assert_eq!(range.size.bits(), ptr_size.bits() * 2); + range.size = ptr_size; + } + if ca.inner().provenance().range_empty(range, &rp.tcx()) { + assert!(ty.is_unsafe_ptr()); + return EvaluatedConst { + ty, + kind: EcKind::Pointer(None), + }; + } + } + assert_eq!( + is_ptr, + ty.is_any_ptr(), + "({range:?}, {is_ptr}, {ty:?}): {:?} / {:?}", + ca.inner().init_mask(), + ca.inner().provenance() + ); + match ca.inner().read_scalar(&rp.tcx(), range, is_ptr) { + Ok(scalar) => scalar.eval(ty, rp), + Err(err) => panic!( + "{err:?} ({range:?}, {is_ptr}, {ty:?}): {:?} / {:?}", + ca.inner().init_mask(), + ca.inner().provenance() + ), + } + } + } + + // println!( + // "Range: {range:?}, is_ptr: {is_ptr}, pointer_size: {:?}", + // rp.tcx().data_layout().pointer_size + // ); + // let bytes = self.inspect_with_uninit_and_ptr_outside_interpreter(0..self.len()); + // let provenance = self.provenance(); + // println!("inner: {:?}, extra: {:?}, provenance {:?}", bytes, self.extra, provenance); + // for (_, ptr) in provenance.ptrs().iter() {} +} + +fn layout_of<'tcx>( + ty: Ty<'tcx>, + rp: PlaceRepacker<'_, 'tcx>, +) -> Result, &'tcx LayoutError<'tcx>> { + let peat = ParamEnvAnd { + param_env: ParamEnv::reveal_all(), + value: ty, + }; + rp.tcx().layout_of(peat) +} + +struct RevealAllEnv<'a, 'tcx>(PlaceRepacker<'a, 'tcx>); +impl HasDataLayout for RevealAllEnv<'_, '_> { + fn data_layout(&self) -> &TargetDataLayout { + self.0.tcx.data_layout() + } +} +impl<'tcx> HasTyCtxt<'tcx> for RevealAllEnv<'_, 'tcx> { + fn tcx(&self) -> TyCtxt<'tcx> { + self.0.tcx() + } +} +impl<'tcx> HasParamEnv<'tcx> for RevealAllEnv<'_, 'tcx> { + fn param_env(&self) -> ParamEnv<'tcx> { + ParamEnv::reveal_all() + } +} +impl<'a, 'tcx> From> for RevealAllEnv<'a, 'tcx> { + fn from(rp: PlaceRepacker<'a, 'tcx>) -> Self { + Self(rp) + } +} diff --git a/mir-state-analysis/src/utils/display.rs b/mir-state-analysis/src/utils/display.rs new file mode 100644 index 00000000000..e5bb5a3bede --- /dev/null +++ b/mir-state-analysis/src/utils/display.rs @@ -0,0 +1,168 @@ +// © 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::{ + borrow::Cow, + collections::VecDeque, + fmt::{Debug, Formatter, Result}, +}; + +use prusti_rustc_interface::{ + middle::{ + mir::{ + PlaceElem, PlaceRef, ProjectionElem, VarDebugInfo, VarDebugInfoContents, RETURN_PLACE, + }, + ty::{AdtKind, TyKind}, + }, + span::Span, +}; + +use super::{Place, PlaceRepacker}; + +#[derive(Clone)] +pub enum PlaceDisplay<'tcx> { + Temporary(Place<'tcx>), + User(Place<'tcx>, String), +} + +impl<'tcx> Debug for PlaceDisplay<'tcx> { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + match self { + PlaceDisplay::Temporary(place) => write!(f, "{place:?}"), + PlaceDisplay::User(place, s) => write!(f, "{place:?} = {s}"), + } + } +} + +impl<'tcx> PlaceDisplay<'tcx> { + pub fn is_user(&self) -> bool { + matches!(self, PlaceDisplay::User(..)) + } +} + +impl<'tcx> Place<'tcx> { + pub fn to_string(&self, repacker: PlaceRepacker<'_, 'tcx>) -> PlaceDisplay<'tcx> { + // Get the local's debug name from the Body's VarDebugInfo + let local_name = if self.local == RETURN_PLACE { + Cow::Borrowed("RETURN") + } else { + fn as_local(span: Span, outer_span: Span) -> Option { + // Before we call source_callsite, we check and see if the span is already local. + // This is important b/c in print!("{}", y) if the user selects `y`, the source_callsite + // of that span is the entire macro. + if outer_span.contains(span) { + return Some(span); + } else { + let sp = span.source_callsite(); + if outer_span.contains(sp) { + return Some(sp); + } + } + + None + } + + let get_local_name = |info: &VarDebugInfo<'tcx>| match info.value { + VarDebugInfoContents::Place(place) if place.local == self.local => { + as_local(info.source_info.span, repacker.mir.span) + .map(|_| info.name.to_string()) + } + _ => None, + }; + let Some(local_name) = repacker.mir.var_debug_info.iter().find_map(get_local_name) + else { + return PlaceDisplay::Temporary(*self); + }; + Cow::Owned(local_name) + }; + + #[derive(Copy, Clone)] + enum ElemPosition { + Prefix, + Suffix, + } + + // Turn each PlaceElem into a prefix (e.g. * for deref) or a suffix + // (e.g. .field for projection). + let elem_to_string = |(index, (place, elem)): ( + usize, + (PlaceRef<'tcx>, PlaceElem<'tcx>), + )| + -> (ElemPosition, Cow<'static, str>) { + match elem { + ProjectionElem::Deref => (ElemPosition::Prefix, "*".into()), + + ProjectionElem::Field(field, _) => { + let ty = place.ty(&repacker.mir.local_decls, repacker.tcx).ty; + + let field_name = match ty.kind() { + TyKind::Adt(def, _substs) => { + let fields = match def.adt_kind() { + AdtKind::Struct => &def.non_enum_variant().fields, + AdtKind::Enum => { + let Some(PlaceElem::Downcast(_, variant_idx)) = + self.projection.get(index - 1) + else { + unimplemented!() + }; + &def.variant(*variant_idx).fields + } + kind => unimplemented!("{kind:?}"), + }; + + fields[field].ident(repacker.tcx).to_string() + } + + TyKind::Tuple(_) => field.as_usize().to_string(), + + TyKind::Closure(def_id, _substs) => match def_id.as_local() { + Some(local_def_id) => { + let captures = repacker.tcx.closure_captures(local_def_id); + captures[field.as_usize()].var_ident.to_string() + } + None => field.as_usize().to_string(), + }, + + kind => unimplemented!("{kind:?}"), + }; + + (ElemPosition::Suffix, format!(".{field_name}").into()) + } + ProjectionElem::Downcast(sym, _) => { + let variant = sym.map(|s| s.to_string()).unwrap_or_else(|| "??".into()); + (ElemPosition::Suffix, format!("@{variant}",).into()) + } + + ProjectionElem::Index(_) => (ElemPosition::Suffix, "[_]".into()), + kind => unimplemented!("{kind:?}"), + } + }; + + let (positions, contents): (Vec<_>, Vec<_>) = self + .iter_projections() + .enumerate() + .map(elem_to_string) + .unzip(); + + // Combine the prefixes and suffixes into a corresponding sequence + let mut parts = VecDeque::from([local_name]); + for (i, string) in contents.into_iter().enumerate() { + match positions[i] { + ElemPosition::Prefix => { + parts.push_front(string); + if matches!(positions.get(i + 1), Some(ElemPosition::Suffix)) { + parts.push_front(Cow::Borrowed("(")); + parts.push_back(Cow::Borrowed(")")); + } + } + ElemPosition::Suffix => parts.push_back(string), + } + } + + let full = parts.make_contiguous().join(""); + PlaceDisplay::User(*self, full) + } +} diff --git a/mir-state-analysis/src/utils/mod.rs b/mir-state-analysis/src/utils/mod.rs new file mode 100644 index 00000000000..a271c0109d8 --- /dev/null +++ b/mir-state-analysis/src/utils/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/. + +pub mod place; +pub(crate) mod repacker; +pub mod display; +mod mutable; +mod root_place; +pub mod ty; +pub mod r#const; + +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..a58d95972f4 --- /dev/null +++ b/mir-state-analysis/src/utils/place.rs @@ -0,0 +1,415 @@ +// © 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}, + ty::Ty, +}; + +// #[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)) + } + + pub fn projects_exactly_one_deref(self) -> bool { + self.projection.len() == 1 && matches!(self.projection[0], ProjectionElem::Deref) + } + + pub fn last_projection_ty(self) -> Option> { + self.last_projection().and_then(|(_, proj)| match proj { + ProjectionElem::Field(_, ty) | ProjectionElem::OpaqueCast(ty) => Some(ty), + _ => None, + }) + } +} + +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..83b9d099b3a --- /dev/null +++ b/mir-state-analysis/src/utils/repacker.rs @@ -0,0 +1,508 @@ +// © 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, Idx, IndexVec}, + middle::{ + mir::{ + tcx::PlaceTy, Body, HasLocalDecls, Local, Mutability, Place as MirPlace, PlaceElem, + ProjectionElem, Promoted, + }, + ty::{Region, RegionVid, Ty, TyCtxt, TyKind}, + }, + target::abi::FieldIdx, +}; + +use crate::utils::ty::{DeepTypeVisitable, DeepTypeVisitor, Stack}; + +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) promoted: &'a IndexVec>, + pub(super) tcx: TyCtxt<'tcx>, +} + +impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { + pub fn new( + mir: &'a Body<'tcx>, + promoted: &'a IndexVec>, + tcx: TyCtxt<'tcx>, + ) -> Self { + Self { mir, promoted, 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 always_live_locals_non_args(self) -> BitSet { + let mut all = self.always_live_locals(); + for arg in 0..self.mir.arg_count + 1 { + // Includes `RETURN_PLACE` + all.remove(Local::new(arg)); + } + all + } + + pub fn body(self) -> &'a Body<'tcx> { + self.mir + } + + pub fn promoted(self) -> &'a IndexVec> { + self.promoted + } + + pub fn tcx(self) -> TyCtxt<'tcx> { + self.tcx + } +} + +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 ty(self, repacker: PlaceRepacker<'_, 'tcx>) -> PlaceTy<'tcx> { + (*self).ty(repacker.mir, repacker.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()) + // } + // } + + /// 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); + } + } + + /// Returns all `TyKind::Ref` and `TyKind::RawPtr` that `self` projects through. + /// The `Option` acts as an either where `TyKind::RawPtr` corresponds to a `None`. + #[tracing::instrument(name = "Place::projection_refs", level = "trace", skip(repacker))] + pub fn projection_refs( + self, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> impl Iterator, Ty<'tcx>, Mutability)>> { + self.projection_tys(repacker) + .filter_map(|(ty, _)| match ty.ty.kind() { + &TyKind::Ref(r, ty, m) => Some(Some((r, ty, m))), + &TyKind::RawPtr(_) => Some(None), + _ => None, + }) + } + + 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> { + // TODO: remove + let old_result = (|| { + 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 + })(); + let new_result = self + .projection_tys(repacker) + .find(|(typ, _)| predicate(*typ)) + .map(|(_, proj)| { + let projection = repacker.tcx.mk_place_elems(proj); + Self::new(self.local, projection) + }); + assert_eq!(old_result, new_result); + new_result + } + + #[tracing::instrument(name = "Place::projection_tys", level = "trace", skip(repacker), ret)] + pub fn projection_tys( + self, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> impl Iterator, &'tcx [PlaceElem<'tcx>])> { + let mut typ = PlaceTy::from_ty(repacker.mir.local_decls()[self.local].ty); + self.projection.iter().enumerate().map(move |(idx, elem)| { + let ret = (typ, &self.projection[0..idx]); + typ = typ.projection_ty(repacker.tcx, *elem); + ret + }) + } + + pub fn all_behind_region(self, r: RegionVid, repacker: PlaceRepacker<'_, 'tcx>) -> Vec { + struct AllBehindWalker<'tcx>(Place<'tcx>, Vec>, TyCtxt<'tcx>); + impl<'tcx> DeepTypeVisitor<'tcx> for AllBehindWalker<'tcx> { + fn tcx(&self) -> TyCtxt<'tcx> { + self.2 + } + + fn visit_rec(&mut self, ty: Ty<'tcx>, stack: &mut Stack<'tcx>) { + ty.visit_with(self, stack); + } + } + todo!() + } + + pub fn mk_deref(self, repacker: PlaceRepacker<'_, 'tcx>) -> Self { + self.mk_place_elem(PlaceElem::Deref, repacker) + } + + pub fn mk_place_elem(self, elem: PlaceElem<'tcx>, repacker: PlaceRepacker<'_, 'tcx>) -> Self { + let elems = repacker + .tcx + .mk_place_elems_from_iter(self.projection.iter().copied().chain([elem])); + Self::new(self.local, elems) + } + + pub fn deref_to_region( + mut self, + r: RegionVid, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> Option { + let mut ty = self.ty(repacker).ty; + while let TyKind::Ref(rr, inner_ty, _) = *ty.kind() { + ty = inner_ty; + self = self.mk_deref(repacker); + if rr.is_var() && rr.as_var() == r { + return Some(self); + } + } + None + } + + pub fn param_kind(self, repacker: PlaceRepacker<'_, 'tcx>) -> Option { + if self.local.as_usize() <= repacker.mir.arg_count { + Some(self.local) + } else { + 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/src/utils/ty/mod.rs b/mir-state-analysis/src/utils/ty/mod.rs new file mode 100644 index 00000000000..b1a5d1b036b --- /dev/null +++ b/mir-state-analysis/src/utils/ty/mod.rs @@ -0,0 +1,96 @@ +// © 2023, ETH Zurich +// +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. + +mod ty_rec; + +pub use ty_rec::*; + +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, ProjectionElem, + }, + ty::{Ty, TyCtxt, TyKind}, + }, +}; + +pub struct Stack<'tcx>(Vec>); + +impl<'tcx> Stack<'tcx> { + pub fn get(&self) -> &Vec> { + &self.0 + } +} + +pub trait DeepTypeVisitor<'tcx> { + fn tcx(&self) -> TyCtxt<'tcx>; + + fn visit(&mut self, ty: Ty<'tcx>) { + self.visit_rec(ty, &mut Stack(Vec::new())); + } + fn visit_rec(&mut self, ty: Ty<'tcx>, stack: &mut Stack<'tcx>); +} + +pub trait DeepTypeVisitable<'tcx> { + fn visit_with(&self, visitor: &mut impl DeepTypeVisitor<'tcx>, stack: &mut Stack<'tcx>); +} + +impl<'tcx> DeepTypeVisitable<'tcx> for Ty<'tcx> { + fn visit_with(&self, visitor: &mut impl DeepTypeVisitor<'tcx>, stack: &mut Stack<'tcx>) { + if stack.0.contains(self) { + return; + } + stack.0.push(*self); + match self.kind() { + TyKind::Bool + | TyKind::Char + | TyKind::Int(_) + | TyKind::Uint(_) + | TyKind::Float(_) + | TyKind::Str => (), + TyKind::Adt(def_id, substs) => { + for field in def_id.all_fields() { + let ty = field.ty(visitor.tcx(), substs); + visitor.visit_rec(ty, stack); + } + } + TyKind::Tuple(tys) => { + for ty in tys.iter() { + visitor.visit_rec(ty, stack); + } + } + TyKind::Ref(_, ty, _) => { + visitor.visit_rec(*ty, stack); + } + TyKind::Foreign(_) => todo!(), + TyKind::Array(_, _) => todo!(), + TyKind::Slice(_) => todo!(), + TyKind::RawPtr(_) => todo!(), + TyKind::FnDef(_, _) => todo!(), + TyKind::FnPtr(_) => todo!(), + TyKind::Dynamic(_, _, _) => todo!(), + TyKind::Closure(_, _) => todo!(), + TyKind::Generator(_, _, _) => todo!(), + TyKind::GeneratorWitness(_) => todo!(), + TyKind::GeneratorWitnessMIR(_, _) => todo!(), + TyKind::Never => todo!(), + TyKind::Alias(_, _) => todo!(), + TyKind::Param(_) => todo!(), + TyKind::Bound(_, _) => todo!(), + TyKind::Placeholder(_) => todo!(), + TyKind::Infer(_) => todo!(), + TyKind::Error(_) => todo!(), + } + stack.0.pop(); + } +} + +// pub fn is_ty_rec(ty: Ty) -> bool { +// let walker = ty.walk(); +// } diff --git a/mir-state-analysis/src/utils/ty/ty_rec.rs b/mir-state-analysis/src/utils/ty/ty_rec.rs new file mode 100644 index 00000000000..ece53c89a8c --- /dev/null +++ b/mir-state-analysis/src/utils/ty/ty_rec.rs @@ -0,0 +1,39 @@ +// © 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, ProjectionElem, + }, + ty::{Ty, TyCtxt, TyKind}, + }, +}; + +use crate::utils::ty::{DeepTypeVisitable, DeepTypeVisitor, Stack}; + +pub fn is_ty_rec<'tcx>(ty: Ty<'tcx>, tcx: TyCtxt<'tcx>) -> bool { + struct RecTyWalk<'tcx>(TyCtxt<'tcx>, bool); + impl<'tcx> DeepTypeVisitor<'tcx> for RecTyWalk<'tcx> { + fn tcx(&self) -> TyCtxt<'tcx> { + self.0 + } + + fn visit_rec(&mut self, ty: Ty<'tcx>, stack: &mut Stack<'tcx>) { + if stack.get().contains(&ty) { + self.1 = true; + return; + } + ty.visit_with(self, stack); + } + } + let mut walker = RecTyWalk(tcx, false); + walker.visit(ty); + walker.1 +} diff --git a/mir-state-analysis/tests/top_crates.rs b/mir-state-analysis/tests/top_crates.rs new file mode 100644 index 00000000000..561649a60c0 --- /dev/null +++ b/mir-state-analysis/tests/top_crates.rs @@ -0,0 +1,146 @@ +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_TEST_COUPLING_GRAPH", "true") + .env("PRUSTI_SKIP_UNSUPPORTED_FEATURES", "true") + // .env("PRUSTI_LOG", "debug") + .env("PRUSTI_NO_VERIFY_DEPS", "true") + .env("PRUSTI_CAP_LINTS", "allow") + .env("PRUSTI_TOP_CRATES", "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..9492cce70a4 100644 --- a/prusti-interface/src/environment/body.rs +++ b/prusti-interface/src/environment/body.rs @@ -1,4 +1,5 @@ use prusti_rustc_interface::{ + index::IndexVec, macros::{TyDecodable, TyEncodable}, middle::{ mir, @@ -10,12 +11,26 @@ use rustc_hash::FxHashMap; use rustc_middle::ty::GenericArgsRef; use std::{cell::RefCell, collections::hash_map::Entry, rc::Rc}; -use crate::environment::{borrowck::facts::BorrowckFacts, mir_storage}; +use crate::environment::{ + borrowck::facts::{BorrowckFacts, BorrowckFacts2}, + mir_storage, +}; /// Stores any possible MIR body (from the compiler) that /// Prusti might want to work with. Cheap to clone #[derive(Clone, TyEncodable, TyDecodable)] -pub struct MirBody<'tcx>(Rc>); +pub struct MirBody<'tcx>( + Rc>, + Rc>>, +); +impl<'tcx> MirBody<'tcx> { + pub fn body(&self) -> Rc> { + self.0.clone() + } + pub fn promoted(&self) -> Rc>> { + self.1.clone() + } +} impl<'tcx> std::ops::Deref for MirBody<'tcx> { type Target = mir::Body<'tcx>; fn deref(&self) -> &Self::Target { @@ -28,6 +43,7 @@ struct BodyWithBorrowckFacts<'tcx> { body: MirBody<'tcx>, /// Cached borrowck information. borrowck_facts: Rc, + borrowck_facts2: Rc>, } /// Bodies which need not be synched across crates and so can be @@ -133,10 +149,18 @@ impl<'tcx> EnvBody<'tcx> { output_facts: body_with_facts.output_facts, location_table: RefCell::new(body_with_facts.location_table), }; + let facts2 = BorrowckFacts2 { + borrow_set: body_with_facts.borrow_set, + region_inference_context: body_with_facts.region_inference_context, + }; BodyWithBorrowckFacts { - body: MirBody(Rc::new(body_with_facts.body)), + body: MirBody( + Rc::new(body_with_facts.body), + Rc::new(body_with_facts.promoted), + ), borrowck_facts: Rc::new(facts), + borrowck_facts2: Rc::new(facts2), } } @@ -145,8 +169,8 @@ impl<'tcx> EnvBody<'tcx> { fn load_local_mir(tcx: TyCtxt<'tcx>, def_id: LocalDefId) -> MirBody<'tcx> { // SAFETY: This is safe because we are feeding in the same `tcx` // that was used to store the data. - let body = unsafe { mir_storage::retrieve_promoted_mir_body(tcx, def_id) }; - MirBody(Rc::new(body)) + let (body, promoted) = unsafe { mir_storage::retrieve_promoted_mir_body(tcx, def_id) }; + MirBody(Rc::new(body), Rc::new(promoted)) } fn get_monomorphised( @@ -182,7 +206,8 @@ impl<'tcx> EnvBody<'tcx> { } else { ty::EarlyBinder::bind(body.0).instantiate(self.tcx, substs) }; - v.insert(MirBody(monomorphised)).clone() + // TODO: monomorphise promoted as well + v.insert(MirBody(monomorphised, body.1)).clone() } else { unreachable!() } @@ -310,6 +335,17 @@ impl<'tcx> EnvBody<'tcx> { .map(|body| body.borrowck_facts.clone()) } + #[tracing::instrument(level = "debug", skip(self))] + pub fn try_get_local_mir_borrowck_facts2( + &self, + def_id: LocalDefId, + ) -> Option>> { + self.local_impure_fns + .borrow() + .get(&def_id) + .map(|body| body.borrowck_facts2.clone()) + } + /// Ensures that the MIR body of a local spec is cached. This must be called on all specs, /// prior to requesting their bodies with `get_spec_body` or exporting with `CrossCrateBodies::from`! pub(crate) fn load_spec_body(&mut self, def_id: LocalDefId) { diff --git a/prusti-interface/src/environment/borrowck/facts.rs b/prusti-interface/src/environment/borrowck/facts.rs index 557c4a4fd7d..a3b5005f75a 100644 --- a/prusti-interface/src/environment/borrowck/facts.rs +++ b/prusti-interface/src/environment/borrowck/facts.rs @@ -5,7 +5,10 @@ // file, You can obtain one at http://mozilla.org/MPL/2.0/. use prusti_rustc_interface::{ - borrowck::consumers::{LocationTable, RichLocation, RustcFacts}, + borrowck::{ + borrow_set::BorrowSet, + consumers::{LocationTable, RegionInferenceContext, RichLocation, RustcFacts}, + }, middle::mir, polonius_engine::FactTypes, }; @@ -32,6 +35,14 @@ impl LocationTableExt for LocationTable { } } +pub struct BorrowckFacts2<'tcx> { + /// The set of borrows occurring in `body` with data about them. + pub borrow_set: Rc>, + /// Context generated during borrowck, intended to be passed to + /// [`OutOfScopePrecomputer`](dataflow::OutOfScopePrecomputer). + pub region_inference_context: Rc>, +} + pub struct BorrowckFacts { /// Polonius input facts. pub input_facts: RefCell>, diff --git a/prusti-interface/src/environment/mir_storage.rs b/prusti-interface/src/environment/mir_storage.rs index 1dd393bd421..dc9d490576e 100644 --- a/prusti-interface/src/environment/mir_storage.rs +++ b/prusti-interface/src/environment/mir_storage.rs @@ -10,6 +10,7 @@ use prusti_rustc_interface::{ borrowck::consumers::BodyWithBorrowckFacts, data_structures::fx::FxHashMap, hir::def_id::LocalDefId, + index::IndexVec, middle::{mir, ty::TyCtxt}, }; use std::{cell::RefCell, thread_local}; @@ -19,7 +20,7 @@ thread_local! { RefCell>> = RefCell::new(FxHashMap::default()); pub static SHARED_STATE_WITHOUT_FACTS: - RefCell>> = + RefCell, IndexVec>)>> = RefCell::new(FxHashMap::default()); } @@ -66,12 +67,15 @@ pub unsafe fn store_promoted_mir_body<'tcx>( _tcx: TyCtxt<'tcx>, def_id: LocalDefId, body: mir::Body<'tcx>, + promoted: IndexVec>, ) { // SAFETY: See the module level comment. let body: mir::Body<'static> = unsafe { std::mem::transmute(body) }; + let promoted: IndexVec> = + unsafe { std::mem::transmute(promoted) }; SHARED_STATE_WITHOUT_FACTS.with(|state| { let mut map = state.borrow_mut(); - assert!(map.insert(def_id, body).is_none()); + assert!(map.insert(def_id, (body, promoted)).is_none()); }); } @@ -79,8 +83,11 @@ pub unsafe fn store_promoted_mir_body<'tcx>( pub(super) unsafe fn retrieve_promoted_mir_body<'tcx>( _tcx: TyCtxt<'tcx>, def_id: LocalDefId, -) -> mir::Body<'tcx> { - let body_without_facts: mir::Body<'static> = SHARED_STATE_WITHOUT_FACTS.with(|state| { +) -> (mir::Body<'tcx>, IndexVec>) { + let body_without_facts: ( + mir::Body<'static>, + IndexVec>, + ) = SHARED_STATE_WITHOUT_FACTS.with(|state| { let mut map = state.borrow_mut(); map.remove(&def_id).unwrap() }); diff --git a/prusti-interface/src/environment/procedure.rs b/prusti-interface/src/environment/procedure.rs index ee81c1d93d9..a11c6a141b4 100644 --- a/prusti-interface/src/environment/procedure.rs +++ b/prusti-interface/src/environment/procedure.rs @@ -13,8 +13,11 @@ use log::{debug, trace}; use prusti_rustc_interface::{ data_structures::fx::{FxHashMap, FxHashSet}, hir::def_id, + index::IndexVec, middle::{ - mir::{self, AggregateKind, BasicBlock, BasicBlockData, Body, Rvalue, StatementKind}, + mir::{ + self, AggregateKind, BasicBlock, BasicBlockData, Body, Promoted, Rvalue, StatementKind, + }, ty::{Ty, TyCtxt}, }, span::Span, @@ -133,6 +136,14 @@ impl<'tcx> Procedure<'tcx> { &self.mir } + pub fn get_mir_rc(&self) -> std::rc::Rc> { + self.mir.body() + } + + pub fn get_promoted_rc(&self) -> std::rc::Rc>> { + self.mir.promoted() + } + /// 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..cc3f4522bfc 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -108,6 +108,7 @@ lazy_static::lazy_static! { settings.set_default("internal_errors_as_warnings", false).unwrap(); settings.set_default("allow_unreachable_unsupported_code", false).unwrap(); settings.set_default("no_verify", false).unwrap(); + settings.set_default::>("cap_lints", None).unwrap(); settings.set_default("no_verify_deps", false).unwrap(); settings.set_default("opt_in_verification", false).unwrap(); settings.set_default("full_compilation", false).unwrap(); @@ -130,6 +131,10 @@ 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("test_coupling_graph", false).unwrap(); + settings.set_default("top_crates", false).unwrap(); settings.set_default("print_desugared_specs", false).unwrap(); settings.set_default("print_typeckd_specs", false).unwrap(); @@ -985,6 +990,10 @@ pub fn set_no_verify(value: bool) { write_setting("no_verify", value); } +pub fn cap_lints() -> Option { + read_setting("cap_lints") +} + /// When enabled, verification is skipped for dependencies. pub fn no_verify_deps() -> bool { read_setting("no_verify_deps") @@ -1030,3 +1039,16 @@ 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") +} + +pub fn test_coupling_graph() -> bool { + read_setting("test_coupling_graph") +} + +pub fn top_crates() -> bool { + read_setting("top_crates") +} 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..6948f49ca02 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -1,4 +1,5 @@ use crate::verifier::verify; +use mir_state_analysis::{test_coupling_graph, test_free_pcs}; use prusti_common::config; use prusti_interface::{ environment::{mir_storage, Environment}, @@ -34,8 +35,13 @@ 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() && !config::test_coupling_graph()) + { consumers::ConsumerOptions::RegionInferenceContext + } else if config::test_coupling_graph() { + consumers::ConsumerOptions::PoloniusInputFacts } else { consumers::ConsumerOptions::PoloniusOutputFacts }; @@ -67,7 +73,12 @@ fn mir_promoted<'tcx>( // SAFETY: This is safe because we are feeding in the same `tcx` that is // going to be used as a witness when pulling out the data. unsafe { - mir_storage::store_promoted_mir_body(tcx, def_id, result.0.borrow().clone()); + mir_storage::store_promoted_mir_body( + tcx, + def_id, + result.0.borrow().clone(), + result.1.borrow().clone(), + ); } result } @@ -157,7 +168,44 @@ 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() && !config::test_coupling_graph() { + 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 promoted = current_procedure.get_promoted_rc(); + + let name = env.name.get_unique_item_name(*proc_id); + println!("Calculating FPCS for: {name} ({:?})", mir.span); + test_free_pcs(&mir, &promoted, tcx); + } + } + if config::test_coupling_graph() { + for proc_id in env.get_annotated_procedures_and_types().0.iter() { + let mir = env.body.get_impure_fn_body_identity(proc_id.expect_local()); + let facts = env + .body + .try_get_local_mir_borrowck_facts(proc_id.expect_local()) + .unwrap(); + let facts2 = env + .body + .try_get_local_mir_borrowck_facts2(proc_id.expect_local()) + .unwrap(); + + let name = env.name.get_unique_item_name(*proc_id); + println!("Calculating CG for: {name} ({:?})", mir.span); + test_coupling_graph( + &*mir.body(), + &*mir.promoted(), + &*facts, + &*facts2, + tcx, + config::top_crates(), + ); + } + } + if !config::test_free_pcs() && !config::test_coupling_graph() { + verify(env, def_spec); + } } }); diff --git a/prusti/src/driver.rs b/prusti/src/driver.rs index eb6744a4604..fe4aefcd6a4 100644 --- a/prusti/src/driver.rs +++ b/prusti/src/driver.rs @@ -104,8 +104,9 @@ fn main() { // Would `cargo check` not report errors for this crate? That is, are lints disabled // (i.e. is this a non-local crate) - let are_lints_disabled = - arg_value(&original_rustc_args, "--cap-lints", |val| val == "allow").is_some(); + let cap_lints = arg_value(&original_rustc_args, "--cap-lints", |_| true); + let cap_lints_any = cap_lints.is_some(); + let are_lints_disabled = cap_lints.map(|val| val == "allow").unwrap_or_default(); // Remote dependencies (e.g. from git/crates.io), or any dependencies if `no_verify_deps`, // are not verified. However, we still run Prusti on them to export potential specs. @@ -130,6 +131,12 @@ fn main() { rustc_args.push(arg); } } + if !cap_lints_any { + if let Some(new_cap) = config::cap_lints() { + rustc_args.push("--cap-lints".to_owned()); + rustc_args.push(new_cap); + } + } let exit_code = driver::catch_with_exit_code(move || { user::message(format!(