From 1af955e135124f5704cd4bc203f7272b7fc7d793 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Tue, 22 Aug 2023 16:15:45 +0200 Subject: [PATCH] Initial experiments with coupling graph --- Cargo.lock | 8 + mir-state-analysis/Cargo.toml | 3 + .../src/coupling_graph/impl/cg.rs | 283 ++++++++++++++++ .../src/coupling_graph/impl/dot.rs | 192 +++++++++++ .../src/coupling_graph/impl/engine.rs | 316 ++++++++++++++++++ .../coupling_graph/impl/join_semi_lattice.rs | 62 ++++ .../src/coupling_graph/impl/mod.rs | 10 + mir-state-analysis/src/coupling_graph/mod.rs | 9 + .../src/free_pcs/impl/triple.rs | 3 +- .../src/free_pcs/results/repacks.rs | 3 + mir-state-analysis/src/lib.rs | 21 ++ mir-state-analysis/src/utils/display.rs | 156 +++++++++ mir-state-analysis/src/utils/mod.rs | 2 + mir-state-analysis/src/utils/mutable.rs | 2 +- mir-state-analysis/src/utils/repacker.rs | 40 ++- mir-state-analysis/src/utils/ty/mod.rs | 95 ++++++ mir-state-analysis/src/utils/ty/ty_rec.rs | 40 +++ prusti-interface/src/environment/body.rs | 19 +- .../src/environment/borrowck/facts.rs | 13 +- prusti-utils/src/config.rs | 5 + prusti/src/callbacks.rs | 15 +- 21 files changed, 1287 insertions(+), 10 deletions(-) create mode 100644 mir-state-analysis/src/coupling_graph/impl/cg.rs create mode 100644 mir-state-analysis/src/coupling_graph/impl/dot.rs create mode 100644 mir-state-analysis/src/coupling_graph/impl/engine.rs create mode 100644 mir-state-analysis/src/coupling_graph/impl/join_semi_lattice.rs create mode 100644 mir-state-analysis/src/coupling_graph/impl/mod.rs create mode 100644 mir-state-analysis/src/coupling_graph/mod.rs create mode 100644 mir-state-analysis/src/utils/display.rs create mode 100644 mir-state-analysis/src/utils/ty/mod.rs create mode 100644 mir-state-analysis/src/utils/ty/ty_rec.rs diff --git a/Cargo.lock b/Cargo.lock index 4991ced6d8f..75d7e241d71 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -905,6 +905,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" @@ -1894,6 +1900,8 @@ name = "mir-state-analysis" version = "0.1.0" dependencies = [ "derive_more", + "dot", + "prusti-interface", "prusti-rustc-interface", "reqwest", "serde", diff --git a/mir-state-analysis/Cargo.toml b/mir-state-analysis/Cargo.toml index 958fe750062..dbf4ee2bb71 100644 --- a/mir-state-analysis/Cargo.toml +++ b/mir-state-analysis/Cargo.toml @@ -8,6 +8,9 @@ edition = "2021" derive_more = "0.99" tracing = { path = "../tracing" } prusti-rustc-interface = { path = "../prusti-rustc-interface" } +dot = "0.1" +# TODO: remove +prusti-interface = { path = "../prusti-interface" } [dev-dependencies] reqwest = { version = "^0.11", features = ["blocking"] } diff --git a/mir-state-analysis/src/coupling_graph/impl/cg.rs b/mir-state-analysis/src/coupling_graph/impl/cg.rs new file mode 100644 index 00000000000..97f229467bd --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/impl/cg.rs @@ -0,0 +1,283 @@ +// © 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}, borrow::Cow}; + +use derive_more::{Deref, DerefMut}; +use prusti_interface::environment::borrowck::facts::{BorrowckFacts, BorrowckFacts2}; +use prusti_rustc_interface::{ + data_structures::fx::{FxHashMap, FxHashSet}, + index::bit_set::BitSet, + dataflow::fmt::DebugWithContext, index::IndexVec, middle::mir::Local, + borrowck::{borrow_set::BorrowData, consumers::BorrowIndex}, + middle::{mir::ConstraintCategory, ty::{RegionVid, TyKind}}, +}; + +use crate::{ + free_pcs::{ + engine::FreePlaceCapabilitySummary, CapabilityLocal, CapabilityProjections, RepackOp, + }, + utils::{PlaceRepacker, Place}, +}; + +use super::engine::CoupligGraph; + +#[derive(Clone)] +pub struct Regions<'a, 'tcx> { + pub borrows: FxHashMap, Vec<(Local, RegionVid)>)>, + pub(crate) subset: Vec<(RegionVid, RegionVid)>, + pub(crate) graph: Graph<'a, 'tcx>, +} + +pub type NodeId = usize; + +#[derive(Clone)] +pub struct Graph<'a, 'tcx> { + pub rp: PlaceRepacker<'a, 'tcx>, + pub facts: &'a BorrowckFacts, + pub facts2: &'a BorrowckFacts2<'tcx>, + pub nodes: Vec>>, + pub skip_empty_nodes: bool, + pub shared_borrows: Vec>, +} + +impl PartialEq for Graph<'_, '_> { + fn eq(&self, other: &Self) -> bool { + self.nodes == other.nodes + } +} + +impl<'a, 'tcx> Graph<'a, 'tcx> { + pub fn new(rp: PlaceRepacker<'a, 'tcx>, facts: &'a BorrowckFacts, facts2: &'a BorrowckFacts2<'tcx>) -> Self { + let mut result = Self { + rp, + facts, + facts2, + nodes: Vec::new(), + skip_empty_nodes: false, + shared_borrows: Vec::new(), + }; + // let input_facts = facts.input_facts.borrow(); + // for &(r1, r2) in &input_facts.as_ref().unwrap().known_placeholder_subset { + // result.outlives(r1, r2); + // } + let constraints = facts2.region_inference_context.outlives_constraints(); + for c in constraints { + if c.locations.from_location().is_none() { + result.outlives(c.sup, c.sub, c.category); + } + } + result + } + pub fn new_shared_borrow(&mut self, data: BorrowData<'tcx>) { + self.shared_borrows.push(data); + } + pub fn outlives(&mut self, r1: RegionVid, r2: RegionVid, reason: ConstraintCategory<'tcx>) { + let n1 = self.region_to_node(r1); + let n2 = self.region_to_node(r2); + if n1 == n2 { + return; + } + // println!("Adding outlives {r1:?} ({n1}): {r2:?} ({n2})"); + if let Some(path) = self.reachable(n1, n2) { + for other in path { + self.merge(other, n2); + } + } else { + self.blocks(n2, n1, reason); + } + } + // pub fn contained_by(&mut self, r: RegionVid, l: Local) { + // let n = self.region_to_node(r); + // self.get_node_mut(n).contained_by.push(l); + // } + pub fn kill(&mut self, r: RegionVid) { + let n = self.region_to_node(r); + self.kill_node(n) + } + pub fn remove(&mut self, r: RegionVid, maybe_already_removed: bool) { + for n in self.nodes.iter_mut() { + if let Some(n) = n { + if n.regions.contains(&r) { + n.regions.remove(&r); + if n.regions.is_empty() { + let id = n.id; + let n = self.remove_node(id); + for (&block, _) in &n.blocks { + for (&blocked_by, &edge) in &n.blocked_by { + self.blocks(blocked_by, block, edge.reason); + } + } + } + return; + } + } + } + assert!(maybe_already_removed, "Region {:?} not found in graph", r); + } + + fn reachable(&self, from: NodeId, to: NodeId) -> Option> { + // println!("Checking reachability from {} to {}", from, to); + let mut nodes = FxHashSet::default(); + if from == to { + return Some(nodes); + } + for (&next, _) in &self.get_node(from).blocks { + if let Some(others) = self.reachable(next, to) { + nodes.insert(from); + nodes.extend(others); + } + } + if nodes.is_empty() { + None + } else { + Some(nodes) + } + } + fn region_to_node(&mut self, r: RegionVid) -> NodeId { + let mut last_none = self.nodes.len(); + for (i, n) in self.nodes.iter().enumerate() { + if let Some(n) = n { + if n.regions.contains(&r) { + return i; + } + } else { + last_none = i; + } + } + if last_none == self.nodes.len() { + self.nodes.push(Some(Node::new(last_none, r))); + } else { + self.nodes[last_none] = Some(Node::new(last_none, r)); + } + last_none + } + fn merge(&mut self, n1: NodeId, n2: NodeId) { + assert_ne!(n1, n2); + let to_merge = self.remove_node(n1); + for (block, edge) in to_merge.blocks { + if block != n2 { + self.blocks(n2, block, edge.reason); + } + } + for (block_by, edge) in to_merge.blocked_by { + if block_by != n2 { + self.blocks(block_by, n2, edge.reason); + } + } + let n2 = self.get_node_mut(n2); + // n2.contained_by.extend(to_merge.contained_by); + n2.regions.extend(to_merge.regions); + } + fn kill_node(&mut self, n: NodeId) { + let removed = self.remove_node(n); + for (blocked_by, _) in removed.blocked_by { + self.kill_node(blocked_by); + } + } + fn remove_node(&mut self, n: NodeId) -> Node<'tcx> { + let to_remove = self.nodes[n].take().unwrap(); + for &block in to_remove.blocks.keys() { + let rem = self.get_node_mut(block).blocked_by.remove(&n); + assert!(rem.is_some()); + } + for &block_by in to_remove.blocked_by.keys() { + let rem = self.get_node_mut(block_by).blocks.remove(&n); + assert!(rem.is_some()); + } + to_remove + } + pub(crate) fn get_node(&self, n: NodeId) -> &Node<'tcx> { + self.nodes[n].as_ref().unwrap() + } + fn get_node_mut(&mut self, n: NodeId) -> &mut Node<'tcx> { + self.nodes[n].as_mut().unwrap() + } + fn blocks(&mut self, n1: NodeId, n2: NodeId, reason: ConstraintCategory<'tcx>) { + let block = Edge::new(n1, n2, reason); + self.get_node_mut(n1).blocks.insert(n2, block); + let blocked_by = Edge::new(n2, n1, reason); + self.get_node_mut(n2).blocked_by.insert(n1, blocked_by); + } +} + +#[derive(Clone, Debug, PartialEq)] +pub struct Node<'tcx> { + pub id: NodeId, + pub regions: FxHashSet, + pub blocks: FxHashMap>, + pub blocked_by: FxHashMap>, + // pub contained_by: Vec, +} + +#[derive(Copy, Clone, Debug, PartialEq)] +pub struct Edge<'tcx> { + pub from: NodeId, + pub to: NodeId, + pub reason: ConstraintCategory<'tcx>, +} + +impl<'tcx> Edge<'tcx> { + fn new(from: NodeId, to: NodeId, reason: ConstraintCategory<'tcx>) -> Self { + Self { from, to, reason } + } +} + +impl<'tcx> Node<'tcx> { + pub fn new(id: NodeId, r: RegionVid) -> Self { + Self { + id, + regions: [r].into_iter().collect(), + blocks: FxHashMap::default(), + blocked_by: FxHashMap::default(), + // contained_by: Vec::new(), + } + } +} + +#[derive(Clone)] +pub struct Cg<'a, 'tcx> { + pub(crate) repacker: PlaceRepacker<'a, 'tcx>, + // pub(crate) facts: &'a BorrowckFacts, + pub(crate) live: BitSet, + pub(crate) regions: Regions<'a, 'tcx>, + pub done: usize, +} +impl<'a, 'tcx> Cg<'a, 'tcx> { + pub(crate) fn new(repacker: PlaceRepacker<'a, 'tcx>, facts: &'a BorrowckFacts, facts2: &'a BorrowckFacts2<'tcx>) -> Self { + let live = BitSet::new_empty(facts2.borrow_set.location_map.len() * 2); + let regions = Regions { + borrows: FxHashMap::default(), + subset: Vec::new(), + graph: Graph::new(repacker, facts, facts2), + }; + Cg { repacker, live, regions, done: 0 } + } +} + +impl PartialEq for Cg<'_, '_> { + fn eq(&self, other: &Self) -> bool { + true + } +} +impl Eq for Cg<'_, '_> {} + +impl<'a, 'tcx> Debug for Cg<'a, 'tcx> { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + // self.summary.fmt(f) + Ok(()) + } +} +impl<'a, 'tcx> DebugWithContext> for Cg<'a, 'tcx> { + fn fmt_diff_with( + &self, + old: &Self, + _ctxt: &CoupligGraph<'a, 'tcx>, + f: &mut Formatter<'_>, + ) -> Result { + Ok(()) + } +} 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..0210ca9f040 --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/impl/dot.rs @@ -0,0 +1,192 @@ +// © 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::{ + data_structures::fx::{FxHashMap, FxHashSet}, + index::bit_set::BitSet, + dataflow::fmt::DebugWithContext, index::IndexVec, middle::mir::Local, + borrowck::consumers::BorrowIndex, + middle::{mir::{BorrowKind, ConstraintCategory}, ty::{RegionVid, TyKind}}, +}; + +use crate::utils::Place; + +use super::cg::{NodeId, Edge, Graph}; + +impl<'a, 'tcx> Graph<'a, 'tcx> { + fn get_corresponding_places(&self, n: NodeId) -> Vec>> { + let node = self.get_node(n); + let mut contained_by: Vec> = Vec::new(); + let input_facts = self.facts.input_facts.borrow(); + for &(l, r) in &input_facts.as_ref().unwrap().use_of_var_derefs_origin { + if node.regions.contains(&r) { + contained_by.push(Perms::AllIn(r, l.into())); + } + } + for (_, data) in &self.facts2.borrow_set.location_map { + if node.regions.contains(&data.region) { + contained_by.push(Perms::Exact(data.borrowed_place.into())); + } + } + for data in &self.shared_borrows { + if node.regions.contains(&data.region) { + contained_by.push(Perms::Exact(data.borrowed_place.into())); + } + } + contained_by + } + fn is_empty_node(&self, n: NodeId) -> bool { + self.get_corresponding_places(n).is_empty() + } + fn is_borrow_only(&self, n: NodeId) -> Option { + let node = self.get_node(n); + let input_facts = self.facts.input_facts.borrow(); + for &(_, r) in &input_facts.as_ref().unwrap().use_of_var_derefs_origin { + if node.regions.contains(&r) { + return None; + } + } + let mut is_borrow = None; + for (_, data) in &self.facts2.borrow_set.location_map { + if node.regions.contains(&data.region) { + if is_borrow.is_some() { + return None; + } + is_borrow = Some(data.kind); + } + } + for data in &self.shared_borrows { + if node.regions.contains(&data.region) { + if is_borrow.is_some() { + return None; + } + is_borrow = Some(data.kind); + } + } + is_borrow + } +} + +#[derive(Debug, Copy, Clone)] +enum Perms { + Exact(T), + AllIn(RegionVid, T), +} + +impl<'a, 'b, 'tcx> dot::Labeller<'a, NodeId, Edge<'tcx>> for Graph<'b, 'tcx> { + fn graph_id(&'a self) -> dot::Id<'a> { dot::Id::new("example1").unwrap() } + + fn node_id(&'a self, n: &NodeId) -> dot::Id<'a> { + dot::Id::new(format!("N_{n:?}")).unwrap() + } + + fn edge_end_arrow(&'a self, e: &Edge) -> dot::Arrow { + if self.is_borrow_only(e.from).is_some() { + dot::Arrow::from_arrow(dot::ArrowShape::Dot(dot::Fill::Filled)) + } else { + dot::Arrow::default() + } + } + fn edge_label(&'a self, e: &Edge<'tcx>) -> dot::LabelText<'a> { + let label = match e.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 => "boring", + ConstraintCategory::BoringNoLocation => "boring_nl", + ConstraintCategory::Internal => "internal", + }; + dot::LabelText::LabelStr(Cow::Borrowed(label)) + } + fn node_shape(&'a self, n: &NodeId) -> Option> { + self.is_borrow_only(*n).map(|kind| match 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("ellipse")), + }) + } + fn node_label(&'a self, n: &NodeId) -> dot::LabelText<'a> { + let process_place = |p: Place<'tcx>| p.to_string(self.rp); + let contained_by = self.get_corresponding_places(*n); + // let process_place = |p: Place<'tcx>| p; + let contained_by = contained_by.iter().map(|&l| { + match l { + Perms::Exact(p) => Perms::Exact(process_place(p)), + Perms::AllIn(r, mut p) => { + let mut ty = p.ty(self.rp).ty; + let mut made_precise = false; + while let TyKind::Ref(rr, inner_ty, _) = *ty.kind() { + ty = inner_ty; + p = p.mk_deref(self.rp); + if rr.is_var() && rr.as_var() == r { + made_precise = true; + break; + } + } + if made_precise { + Perms::Exact(process_place(p)) + } else { + Perms::AllIn(r, process_place(p)) + } + } + } + }).collect::>(); + let node = self.get_node(*n); + let label = format!("{:?}\n{:?}", node.regions, contained_by); + dot::LabelText::LabelStr(Cow::Owned(label)) + } +} + +impl<'a, 'b, 'tcx> dot::GraphWalk<'a, NodeId, Edge<'tcx>> for Graph<'b, 'tcx> { + fn nodes(&self) -> dot::Nodes<'a, NodeId> { + let nodes: Vec<_> = self.nodes + .iter() + .enumerate() + .filter_map(|(idx, n)| n.as_ref().map(|_| idx)) + .filter(|&idx| !self.skip_empty_nodes || !self.is_empty_node(idx)) + .collect(); + Cow::Owned(nodes) + } + + fn edges(&'a self) -> dot::Edges<'a, Edge<'tcx>> { + let mut edges = Vec::new(); + for (c, n) in self.nodes.iter().enumerate() { + if let Some(n) = n { + if self.skip_empty_nodes && self.is_empty_node(c) { + continue; + } + for (&b, &edge) in &n.blocks { + if self.skip_empty_nodes && self.is_empty_node(b) { + continue; + } + edges.push(edge); + } + } + } + Cow::Owned(edges) + } + + fn source(&self, e: &Edge<'tcx>) -> NodeId { e.from } + + fn target(&self, e: &Edge<'tcx>) -> NodeId { 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..bae30158213 --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/impl/engine.rs @@ -0,0 +1,316 @@ +// © 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; + +use prusti_interface::environment::borrowck::facts::{BorrowckFacts, BorrowckFacts2}; +use prusti_rustc_interface::{ + data_structures::fx::{FxIndexMap}, + borrowck::{ + borrow_set::{BorrowData, TwoPhaseActivation}, + consumers::{Borrows, BorrowIndex, RichLocation, calculate_borrows_out_of_scope_at_location}, + }, + dataflow::{Analysis, AnalysisDomain, CallReturnPlaces, ResultsCursor}, + index::{bit_set::{BitSet, HybridBitSet}, Idx}, + middle::{ + mir::{ + TerminatorKind, Operand, ConstantKind, StatementKind, Rvalue, + visit::Visitor, BasicBlock, Body, Local, Location, Statement, Terminator, RETURN_PLACE, + }, + ty::{RegionVid, TyCtxt}, + }, +}; + +use crate::{ + free_pcs::{CapabilityKind, CapabilityLocal, Fpcs}, + utils::PlaceRepacker, coupling_graph::cg::{Graph, Node}, +}; + +use super::cg::{Cg, Regions}; + +pub(crate) struct CoupligGraph<'a, 'tcx> { + pub(crate) repacker: PlaceRepacker<'a, 'tcx>, + pub(crate) facts: &'a BorrowckFacts, + pub(crate) facts2: &'a BorrowckFacts2<'tcx>, + pub(crate) flow_borrows: RefCell>>, + pub(crate) out_of_scope: FxIndexMap>, +} +impl<'a, 'tcx> CoupligGraph<'a, 'tcx> { + pub(crate) fn new(tcx: TyCtxt<'tcx>, body: &'a Body<'tcx>, facts: &'a BorrowckFacts, facts2: &'a BorrowckFacts2<'tcx>) -> Self { + std::fs::remove_dir_all("log/coupling").ok(); + std::fs::create_dir_all("log/coupling").unwrap(); + + let repacker = PlaceRepacker::new(body, tcx); + let regioncx = &*facts2.region_inference_context; + let borrow_set = &*facts2.borrow_set; + let out_of_scope = calculate_borrows_out_of_scope_at_location(body, regioncx, borrow_set); + let flow_borrows = Borrows::new(tcx, body, regioncx, borrow_set) + .into_engine(tcx, body) + .pass_name("borrowck") + .iterate_to_fixpoint() + .into_results_cursor(body); + CoupligGraph { repacker, facts, facts2, flow_borrows: RefCell::new(flow_borrows), out_of_scope } + } + + fn handle_diff(&self, state: &mut Regions<'_, 'tcx>, delta: BorrowDelta, location: Location) { + let input_facts = self.facts.input_facts.borrow(); + let input_facts = input_facts.as_ref().unwrap(); + let location_table = self.facts.location_table.borrow(); + let location_table = location_table.as_ref().unwrap(); + for idx in delta.set.iter() { + let loan_issued_at = &input_facts.loan_issued_at; + let (r, _, l) = loan_issued_at.iter().find(|(_, b, _)| idx == *b).copied().unwrap(); + let l = location_table.to_location(l); + let RichLocation::Mid(l) = l else { unreachable!() }; + assert_eq!(l, location); + let locals = input_facts.use_of_var_derefs_origin.iter().filter(|(_, ro)| r == *ro).map(|(l, _)| (*l, r)).collect::>(); + state.borrows.insert(idx, (vec![r], locals)); + } + state.subset.extend(input_facts.subset_base.iter().filter( + |(_, _, l)| rich_to_loc(location_table.to_location(*l)) == location + ).map(|(r1, r2, _)| (*r1, *r2))); + // TODO: do a proper fixpoint here + for _ in 0..10 { + for &(r1, r2) in &state.subset { + let locals = input_facts.use_of_var_derefs_origin.iter().filter(|(_, ro)| r2 == *ro).map(|(l, _)| (*l, r2)).collect::>(); + let mut did_push = false; + for (_, s) in state.borrows.iter_mut() { + if s.0.contains(&r1) { + did_push = true; + if !s.0.contains(&r2) { + s.0.push(r2); + s.1.extend(locals.iter().copied()); + } + } + } + // assert!(did_push, "r1: {:?}, r2: {:?}, location: {:?}, state: {:?}", r1, r2, location, state); + } + } + for r in delta.cleared.iter() { + let removed = state.borrows.remove(&r).unwrap(); + // for (_, s) in state.borrows.iter_mut() { + // s.0.retain(|r| !removed.0.contains(r)); + // s.1.retain(|l| !removed.1.contains(l)); + // } + } + // print!(" {:?}", state.borrows); + self.handle_graph(state, delta, location); + } + + fn handle_graph(&self, state: &mut Regions<'_, 'tcx>, delta: BorrowDelta, location: Location) { + let l = format!("{:?}", location).replace('[', "_").replace(']', ""); + + let input_facts = self.facts.input_facts.borrow(); + let input_facts = input_facts.as_ref().unwrap(); + let location_table = self.facts.location_table.borrow(); + let location_table = location_table.as_ref().unwrap(); + + // let input_facts = self.facts2.region_inference_context.borrow(); + + let oos = self.out_of_scope.get(&location); + if let Some(oos) = oos { + for bi in oos { + let (r, _, l) = input_facts.loan_issued_at.iter().find( + |(_, b, _)| bi == b + ).copied().unwrap(); + println!("UGHBJS region: {r:?} location: {l:?}"); + state.graph.kill(r); + let l = rich_to_loc(location_table.to_location(l)); + let borrow_data = self.facts2.borrow_set.location_map.get(&l).unwrap(); + let local = borrow_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:?}"); + state.graph.remove(region, true); + } + } + } + + // let mut f = std::fs::File::create(format!("log/coupling/{l}_a.dot")).unwrap(); + // dot::render(&state.graph, &mut f).unwrap(); + + for killed in delta.cleared.iter() { + if oos.map(|oos| oos.contains(&killed)).unwrap_or_default() { + continue; + } + let (r, _, l) = input_facts.loan_issued_at.iter().find( + |(_, b, _)| killed == *b + ).copied().unwrap(); + state.graph.remove(r, false); + let l = rich_to_loc(location_table.to_location(l)); + let borrow_data = self.facts2.borrow_set.location_map.get(&l).unwrap(); + let local = borrow_data.borrowed_place.local; + for region in input_facts.use_of_var_derefs_origin.iter().filter(|(l, _)| *l == local).map(|(_, r)| *r) { + state.graph.remove(region, true); + } + } + + // let mut f = std::fs::File::create(format!("log/coupling/{l}_b.dot")).unwrap(); + // dot::render(&state.graph, &mut f).unwrap(); + + // let new_subsets: Vec<_> = input_facts.subset_base.iter().filter( + // |(_, _, l)| rich_to_loc(location_table.to_location(*l)) == location + // ).map(|(r1, r2, _)| (*r1, *r2)).collect(); + // for (r1, r2) in new_subsets { + // state.graph.outlives(r1, r2); + // } + let constraints = self.facts2.region_inference_context.outlives_constraints(); + for c in constraints { + if let Some(from) = c.locations.from_location() { + if from == location { + state.graph.outlives(c.sup, c.sub, c.category); + } + } + } + + if !self.repacker.body().basic_blocks[location.block].is_cleanup { + let mut f = std::fs::File::create(format!("log/coupling/{l}_c.dot")).unwrap(); + dot::render(&state.graph, &mut f).unwrap(); + } + } +} + +impl<'a, 'tcx> AnalysisDomain<'tcx> for CoupligGraph<'a, 'tcx> { + type Domain = Cg<'a, 'tcx>; + const NAME: &'static str = "coupling_graph"; + + fn bottom_value(&self, _body: &Body<'tcx>) -> Self::Domain { + Cg::new(self.repacker, self.facts, self.facts2) + } + + fn initialize_start_block(&self, body: &Body<'tcx>, state: &mut Self::Domain) { + // println!("body: {body:?}"); + println!("\ninput_facts: {:?}", self.facts.input_facts); + println!("output_facts: {:#?}\n", self.facts.output_facts); + println!("location_map: {:#?}\n", self.facts2.borrow_set.location_map); + println!("activation_map: {:#?}\n", self.facts2.borrow_set.activation_map); + println!("local_map: {:#?}\n", self.facts2.borrow_set.local_map); + // println!("region_inference_context: {:#?}\n", self.facts2.region_inference_context); + // println!("locals_state_at_exit: {:#?}\n", self.facts2.borrow_set.locals_state_at_exit); + let lt = self.facts.location_table.borrow(); + let lt = lt.as_ref().unwrap(); + for pt in lt.all_points() { + println!("{pt:?} -> {:?} ({:?})", lt.to_location(pt), ""); //, self.facts.output_facts.origins_live_at(pt)); + } + println!("out_of_scope: {:?}", self.out_of_scope); + } +} + +impl<'a, 'tcx> Analysis<'tcx> for CoupligGraph<'a, 'tcx> { + fn apply_statement_effect( + &mut self, + state: &mut Self::Domain, + statement: &Statement<'tcx>, + location: Location, + ) { + if location.statement_index == 0 { + println!("\nblock: {:?}", location.block); + 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(); + // print!("{statement:?} ({other:?}):"); + let delta = calculate_diff(&other, &state.live); + if delta.set.is_empty() { + match statement.kind { + StatementKind::Assign(box (assigned_place, Rvalue::Ref(region, kind, borrowed_place))) => { + + state.regions.graph.new_shared_borrow(BorrowData { + reserve_location: location, + activation_location: TwoPhaseActivation::NotTwoPhase, + kind, + region: region.as_var(), + borrowed_place, + assigned_place, + }) + } + _ => (), + } + } + self.handle_diff(&mut state.regions, delta, location); + state.live = other; + // println!(); + } + + fn apply_terminator_effect( + &mut self, + state: &mut Self::Domain, + terminator: &Terminator<'tcx>, + location: Location, + ) { + if location.statement_index == 0 { + println!("\nblock: {:?}", location.block); + 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(); + if let TerminatorKind::Call { func, args, destination, target, fn_span, .. } = &terminator.kind { + if let Operand::Constant(c) = func { + println!("user_ty: {:?}", c.user_ty); + println!("call: {:?}", c.literal); + if let ConstantKind::Val(cv, ty) = c.literal { + println!("val: {:?}", cv); + println!("ty: {:?}", ty); + } + println!("\n\n\ncall: {:?}", func); + } + for arg in args { + match arg { + Operand::Copy(a) => println!("copy ({arg:?}): {:?}", a), + Operand::Move(b) => println!("move ({arg:?}): {:?}", b), + Operand::Constant(c) => println!("const ({arg:?}): {:?}", c.literal), + } + } + } + // print!("{terminator:?} ({other:?}):"); + let delta = calculate_diff(&other, &state.live); + self.handle_diff(&mut state.regions, delta, location); + state.live = other; + // println!(); + } + + fn apply_call_return_effect( + &mut self, + _state: &mut Self::Domain, + _block: BasicBlock, + _return_places: CallReturnPlaces<'_, 'tcx>, + ) { + // Nothing to do here + } +} + +struct BorrowDelta { + set: HybridBitSet, + 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, + } +} + +fn rich_to_loc(l: RichLocation) -> Location { + match l { + RichLocation::Start(l) => l, + RichLocation::Mid(l) => l, + } +} 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..27c10e8cc4c --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/impl/join_semi_lattice.rs @@ -0,0 +1,62 @@ +// © 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; + +use crate::{ + free_pcs::{ + CapabilityKind, CapabilityLocal, CapabilityProjections, CapabilitySummary, Fpcs, RepackOp, + }, + utils::{PlaceOrdering, PlaceRepacker}, +}; + +use super::cg::Cg; + +impl JoinSemiLattice for Cg<'_, '_> { + fn join(&mut self, other: &Self) -> bool { + if self.done == 2 { + return false; + } + self.done += 1; + let mut changed = self.live.union(&other.live); + for (idx, data) in other.regions.borrows.iter() { + match self.regions.borrows.entry(*idx) { + Entry::Occupied(mut o) => { + let (a, b) = o.get_mut(); + for r in &data.0 { + if !a.contains(r) { + changed = true; + a.push(*r); + } + } + for r in &data.1 { + if !b.contains(r) { + changed = true; + b.push(*r); + } + } + } + Entry::Vacant(v) => { + changed = true; + v.insert(data.clone()); + } + } + } + for s in &other.regions.subset { + if !self.regions.subset.contains(s) { + changed = true; + self.regions.subset.push(*s); + } + } + if self.regions.graph != other.regions.graph { + changed = true; + self.regions.graph = other.regions.graph.clone(); + } + changed + } +} 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..2c97c1ffdd6 --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/impl/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/. + +pub(crate) mod engine; +pub(crate) mod cg; +pub(crate) mod join_semi_lattice; +mod dot; 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..9456a304f3f --- /dev/null +++ b/mir-state-analysis/src/coupling_graph/mod.rs @@ -0,0 +1,9 @@ +// © 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; + +pub use r#impl::*; diff --git a/mir-state-analysis/src/free_pcs/impl/triple.rs b/mir-state-analysis/src/free_pcs/impl/triple.rs index c12e425e5fd..c40d20cb00a 100644 --- a/mir-state-analysis/src/free_pcs/impl/triple.rs +++ b/mir-state-analysis/src/free_pcs/impl/triple.rs @@ -42,7 +42,8 @@ impl<'tcx> Visitor<'tcx> for Fpcs<'_, 'tcx> { _ => unreachable!(), } } - &FakeRead(box (_, place)) => self.requires_read(place), + &FakeRead(box (_, place)) | + &PlaceMention(box place) => self.requires_read(place), &SetDiscriminant { box place, .. } => self.requires_exclusive(place), &Deinit(box place) => { // TODO: Maybe OK to also allow `Write` here? diff --git a/mir-state-analysis/src/free_pcs/results/repacks.rs b/mir-state-analysis/src/free_pcs/results/repacks.rs index bd725d390d7..80b38815eb9 100644 --- a/mir-state-analysis/src/free_pcs/results/repacks.rs +++ b/mir-state-analysis/src/free_pcs/results/repacks.rs @@ -44,6 +44,9 @@ pub enum RepackOp<'tcx> { /// 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 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 diff --git a/mir-state-analysis/src/lib.rs b/mir-state-analysis/src/lib.rs index 84c6fb4dcb2..c691d08237c 100644 --- a/mir-state-analysis/src/lib.rs +++ b/mir-state-analysis/src/lib.rs @@ -9,7 +9,9 @@ pub mod free_pcs; pub mod utils; +pub mod coupling_graph; +use prusti_interface::environment::borrowck::facts::{BorrowckFacts, BorrowckFacts2}; use prusti_rustc_interface::{ dataflow::Analysis, middle::{mir::Body, ty::TyCtxt}, @@ -31,3 +33,22 @@ pub fn test_free_pcs<'tcx>(mir: &Body<'tcx>, tcx: TyCtxt<'tcx>) { let analysis = run_free_pcs(mir, tcx); free_pcs::check(analysis); } + +pub fn run_coupling_graph<'mir, 'tcx>( + mir: &'mir Body<'tcx>, + facts: &'mir BorrowckFacts, + facts2: &'mir BorrowckFacts2<'tcx>, + tcx: TyCtxt<'tcx>, +) { + let fpcs = coupling_graph::engine::CoupligGraph::new(tcx, mir, facts, facts2); + let analysis = fpcs + .into_engine(tcx, mir) + .pass_name("coupling_graph") + .iterate_to_fixpoint(); + // free_pcs::FreePcsAnalysis::new(analysis.into_results_cursor(mir)) +} + +pub fn test_coupling_graph<'tcx>(mir: &Body<'tcx>, facts: &BorrowckFacts, facts2: &BorrowckFacts2<'tcx>, tcx: TyCtxt<'tcx>) { + let analysis = run_coupling_graph(mir, facts, facts2, tcx); + // free_pcs::check(analysis); +} diff --git a/mir-state-analysis/src/utils/display.rs b/mir-state-analysis/src/utils/display.rs new file mode 100644 index 00000000000..d7a61fef236 --- /dev/null +++ b/mir-state-analysis/src/utils/display.rs @@ -0,0 +1,156 @@ +// © 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}; + +pub enum PlaceDisplay<'tcx> { + Temporary(Place<'tcx>), + User(String), +} + +impl<'tcx> Debug for PlaceDisplay<'tcx> { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + match self { + PlaceDisplay::Temporary(place) => write!(f, "{place:?}"), + PlaceDisplay::User(s) => write!(f, "{s}"), + } + } +} + +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(full) + } +} diff --git a/mir-state-analysis/src/utils/mod.rs b/mir-state-analysis/src/utils/mod.rs index fb02d7b16ab..d983612fba0 100644 --- a/mir-state-analysis/src/utils/mod.rs +++ b/mir-state-analysis/src/utils/mod.rs @@ -6,8 +6,10 @@ pub mod place; pub(crate) mod repacker; +pub mod display; mod mutable; mod root_place; +pub mod ty; pub use mutable::*; pub use place::*; diff --git a/mir-state-analysis/src/utils/mutable.rs b/mir-state-analysis/src/utils/mutable.rs index a733acdc139..45e7bafa315 100644 --- a/mir-state-analysis/src/utils/mutable.rs +++ b/mir-state-analysis/src/utils/mutable.rs @@ -90,7 +90,7 @@ impl<'tcx> Place<'tcx> { Some((place_base, elem)) => { match elem { ProjectionElem::Deref => { - let base_ty = place_base.ty(repacker.body(), repacker.tcx).ty; + let base_ty = place_base.ty(repacker).ty; // Check the kind of deref to decide match base_ty.kind() { diff --git a/mir-state-analysis/src/utils/repacker.rs b/mir-state-analysis/src/utils/repacker.rs index 182fb09a46e..2810a6bb9c7 100644 --- a/mir-state-analysis/src/utils/repacker.rs +++ b/mir-state-analysis/src/utils/repacker.rs @@ -11,13 +11,15 @@ use prusti_rustc_interface::{ middle::{ mir::{ tcx::PlaceTy, Body, HasLocalDecls, Local, Mutability, Place as MirPlace, - ProjectionElem, + ProjectionElem, PlaceElem, }, - ty::{TyCtxt, TyKind}, + ty::{Ty, TyCtxt, TyKind, RegionVid}, }, target::abi::FieldIdx, }; +use crate::utils::ty::{DeepTypeVisitor, Stack, DeepTypeVisitable}; + use super::Place; #[derive(Debug, Clone, Copy)] @@ -68,6 +70,10 @@ impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { pub fn body(self) -> &'a Body<'tcx> { self.mir } + + pub fn tcx(self) -> TyCtxt<'tcx> { + self.tcx + } } impl<'tcx> Place<'tcx> { @@ -196,7 +202,7 @@ impl<'tcx> Place<'tcx> { (other_places, ProjectionRefKind::Other) } ProjectionElem::Deref => { - let typ = self.ty(repacker.mir, repacker.tcx); + let typ = self.ty(repacker); let kind = match typ.ty.kind() { TyKind::Ref(_, _, mutbl) => ProjectionRefKind::Ref(*mutbl), TyKind::RawPtr(ptr) => ProjectionRefKind::RawPtr(ptr.mutbl), @@ -223,7 +229,7 @@ impl<'tcx> Place<'tcx> { repacker: PlaceRepacker<'_, 'tcx>, ) -> Vec { let mut places = Vec::new(); - let typ = self.ty(repacker.mir, repacker.tcx); + let typ = self.ty(repacker); if !matches!(typ.ty.kind(), TyKind::Adt(..)) { assert!( typ.variant_index.is_none(), @@ -313,6 +319,9 @@ impl<'tcx> Place<'tcx> { // } 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; @@ -326,7 +335,7 @@ impl<'tcx> Place<'tcx> { /// Should only be called on a `Place` obtained from `RootPlace::get_parent`. pub fn get_ref_mutability(self, repacker: PlaceRepacker<'_, 'tcx>) -> Mutability { - let typ = self.ty(repacker.mir, repacker.tcx); + let typ = self.ty(repacker); if let TyKind::Ref(_, _, mutability) = typ.ty.kind() { *mutability } else { @@ -370,4 +379,25 @@ impl<'tcx> Place<'tcx> { } None } + + 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 { + let elems = repacker.tcx.mk_place_elems_from_iter( + self.projection.iter().copied().chain(std::iter::once(PlaceElem::Deref)) + ); + Self::new(self.local, elems) + } } 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..3f9a7927203 --- /dev/null +++ b/mir-state-analysis/src/utils/ty/mod.rs @@ -0,0 +1,95 @@ +// © 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, TyKind, TyCtxt}, + }, +}; + +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..bcd49bdb2ef --- /dev/null +++ b/mir-state-analysis/src/utils/ty/ty_rec.rs @@ -0,0 +1,40 @@ +// © 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, TyKind, TyCtxt}, + }, +}; + +use crate::utils::ty::{DeepTypeVisitor, DeepTypeVisitable, 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/prusti-interface/src/environment/body.rs b/prusti-interface/src/environment/body.rs index 48eea9e314a..326c0d2d5bd 100644 --- a/prusti-interface/src/environment/body.rs +++ b/prusti-interface/src/environment/body.rs @@ -10,7 +10,7 @@ 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 @@ -33,6 +33,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 @@ -138,10 +139,15 @@ 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)), borrowck_facts: Rc::new(facts), + borrowck_facts2: Rc::new(facts2), } } @@ -315,6 +321,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..314b3477da0 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, RichLocation, RustcFacts, RegionInferenceContext}, + }, 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-utils/src/config.rs b/prusti-utils/src/config.rs index 4cfc879a9e2..5941025b1ef 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -132,6 +132,7 @@ lazy_static::lazy_static! { 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("print_desugared_specs", false).unwrap(); settings.set_default("print_typeckd_specs", false).unwrap(); @@ -1037,3 +1038,7 @@ pub fn num_errors_per_function() -> u32 { pub fn test_free_pcs() -> bool { read_setting("test_free_pcs") } + +pub fn test_coupling_graph() -> bool { + read_setting("test_coupling_graph") +} diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index 172c4ff945f..16a67080f9f 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -1,5 +1,5 @@ use crate::verifier::verify; -use mir_state_analysis::test_free_pcs; +use mir_state_analysis::{test_coupling_graph, test_free_pcs}; use prusti_common::config; use prusti_interface::{ environment::{mir_storage, Environment}, @@ -168,6 +168,19 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls { let mir = current_procedure.get_mir_rc(); test_free_pcs(&mir, tcx); } + } else 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(); + test_coupling_graph(&*mir, &*facts, &*facts2, tcx); + } } else { verify(env, def_spec); }