From 0a533aea1540d4d82d437bbae829ec2024396988 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Tue, 18 Apr 2023 12:54:36 +0200 Subject: [PATCH] Switch to using rustc dataflow engine --- Cargo.lock | 33 +- Cargo.toml | 2 +- micromir/src/check/checker.rs | 136 ----- micromir/src/defs/body.rs | 143 ----- micromir/src/defs/operand.rs | 100 ---- micromir/src/defs/rvalue.rs | 95 ---- micromir/src/defs/statement.rs | 161 ------ micromir/src/defs/terminator.rs | 401 -------------- micromir/src/free_pcs/permission.rs | 517 ------------------ micromir/src/lib.rs | 36 -- micromir/src/repack/calculate.rs | 295 ---------- micromir/src/repack/repacker.rs | 294 ---------- micromir/src/repack/triple.rs | 124 ----- {micromir => mir-state-analysis}/Cargo.toml | 5 +- .../src/free_pcs/check/checker.rs | 159 ++++++ .../src/free_pcs/check/consistency.rs | 45 ++ .../src/free_pcs/check}/mod.rs | 5 +- .../src/free_pcs/impl/engine.rs | 96 ++++ mir-state-analysis/src/free_pcs/impl/fpcs.rs | 148 +++++ .../src/free_pcs/impl/join_semi_lattice.rs | 197 +++++++ mir-state-analysis/src/free_pcs/impl/local.rs | 163 ++++++ .../src/free_pcs/impl}/mod.rs | 20 +- mir-state-analysis/src/free_pcs/impl/place.rs | 92 ++++ .../src/free_pcs/impl/triple.rs | 148 +++++ .../src/free_pcs/impl/update.rs | 130 +++++ .../src/free_pcs}/mod.rs | 13 +- .../src/free_pcs/results}/mod.rs | 4 +- .../src/free_pcs/results/repacking.rs | 0 .../src/free_pcs/results/repacks.rs | 21 + mir-state-analysis/src/lib.rs | 28 + .../src/utils/mod.rs | 3 + .../src/utils/place.rs | 133 ++++- .../src/utils/repacker.rs | 263 +++++---- .../tests/top_crates.rs | 0 prusti/Cargo.toml | 2 +- prusti/src/callbacks.rs | 11 +- x.py | 2 +- 37 files changed, 1570 insertions(+), 2455 deletions(-) delete mode 100644 micromir/src/check/checker.rs delete mode 100644 micromir/src/defs/body.rs delete mode 100644 micromir/src/defs/operand.rs delete mode 100644 micromir/src/defs/rvalue.rs delete mode 100644 micromir/src/defs/statement.rs delete mode 100644 micromir/src/defs/terminator.rs delete mode 100644 micromir/src/free_pcs/permission.rs delete mode 100644 micromir/src/lib.rs delete mode 100644 micromir/src/repack/calculate.rs delete mode 100644 micromir/src/repack/repacker.rs delete mode 100644 micromir/src/repack/triple.rs rename {micromir => mir-state-analysis}/Cargo.toml (83%) create mode 100644 mir-state-analysis/src/free_pcs/check/checker.rs create mode 100644 mir-state-analysis/src/free_pcs/check/consistency.rs rename {micromir/src/free_pcs => mir-state-analysis/src/free_pcs/check}/mod.rs (79%) create mode 100644 mir-state-analysis/src/free_pcs/impl/engine.rs create mode 100644 mir-state-analysis/src/free_pcs/impl/fpcs.rs create mode 100644 mir-state-analysis/src/free_pcs/impl/join_semi_lattice.rs create mode 100644 mir-state-analysis/src/free_pcs/impl/local.rs rename {micromir/src/defs => mir-state-analysis/src/free_pcs/impl}/mod.rs (56%) create mode 100644 mir-state-analysis/src/free_pcs/impl/place.rs create mode 100644 mir-state-analysis/src/free_pcs/impl/triple.rs create mode 100644 mir-state-analysis/src/free_pcs/impl/update.rs rename {micromir/src/repack => mir-state-analysis/src/free_pcs}/mod.rs (63%) rename {micromir/src/check => mir-state-analysis/src/free_pcs/results}/mod.rs (87%) create mode 100644 mir-state-analysis/src/free_pcs/results/repacking.rs create mode 100644 mir-state-analysis/src/free_pcs/results/repacks.rs create mode 100644 mir-state-analysis/src/lib.rs rename {micromir => mir-state-analysis}/src/utils/mod.rs (81%) rename {micromir => mir-state-analysis}/src/utils/place.rs (63%) rename micromir/src/repack/place.rs => mir-state-analysis/src/utils/repacker.rs (55%) rename {micromir => mir-state-analysis}/tests/top_crates.rs (100%) diff --git a/Cargo.lock b/Cargo.lock index 8857aded314..3b35deb8326 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -633,9 +633,9 @@ dependencies = [ [[package]] name = "crossbeam-channel" -version = "0.5.7" +version = "0.5.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cf2b3e8478797446514c91ef04bafcb59faba183e621ad488df88983cc14128c" +checksum = "a33c2bf77f2df06183c3aa30d1e96c0695a313d4f9c453cc3762a6db39f99200" dependencies = [ "cfg-if", "crossbeam-utils", @@ -1695,20 +1695,6 @@ dependencies = [ "autocfg", ] -[[package]] -name = "micromir" -version = "0.1.0" -dependencies = [ - "derive_more", - "prusti-interface", - "prusti-rustc-interface", - "reqwest", - "serde", - "serde_derive", - "serde_json", - "tracing 0.1.0", -] - [[package]] name = "mime" version = "0.3.16" @@ -1761,6 +1747,19 @@ dependencies = [ "winapi", ] +[[package]] +name = "mir-state-analysis" +version = "0.1.0" +dependencies = [ + "derive_more", + "prusti-rustc-interface", + "reqwest", + "serde", + "serde_derive", + "serde_json", + "tracing 0.1.0", +] + [[package]] name = "multipart" version = "0.18.0" @@ -2134,7 +2133,7 @@ dependencies = [ "env_logger", "lazy_static", "log", - "micromir", + "mir-state-analysis", "prusti-common", "prusti-interface", "prusti-rustc-interface", diff --git a/Cargo.toml b/Cargo.toml index 74d88886b7d..2670d0c5e95 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -7,7 +7,7 @@ members = [ "prusti-common", "prusti-utils", "tracing", - "micromir", + "mir-state-analysis", "prusti-interface", "prusti-viper", "prusti-server", diff --git a/micromir/src/check/checker.rs b/micromir/src/check/checker.rs deleted file mode 100644 index 6fcf1a64575..00000000000 --- a/micromir/src/check/checker.rs +++ /dev/null @@ -1,136 +0,0 @@ -// © 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; - -use crate::{ - repack::triple::ModifiesFreeState, FreeState, MicroBasicBlocks, PermissionKind, - PermissionLocal, PlaceOrdering, PlaceRepacker, RepackOp, Repacks, -}; - -pub(crate) fn check<'tcx>(bbs: &MicroBasicBlocks<'tcx>, rp: PlaceRepacker<'_, 'tcx>) { - for bb in bbs.basic_blocks.iter() { - let mut curr_state = bb.get_start_state().clone(); - // Consistency - curr_state.consistency_check(rp); - for stmt in bb.statements.iter() { - // Pre-state - let pcs = stmt.repack_operands.as_ref().unwrap(); - assert_eq!(pcs.state(), &curr_state); - // Repacks - pcs.repacks().update_free(&mut curr_state, false, rp); - // Consistency - curr_state.consistency_check(rp); - // Statement - stmt.get_update(curr_state.len()) - .update_free(&mut curr_state); - // Consistency - curr_state.consistency_check(rp); - } - // Pre-state - let pcs = bb.terminator.repack_operands.as_ref().unwrap(); - assert_eq!(pcs.state(), &curr_state); - // Repacks - pcs.repacks().update_free(&mut curr_state, false, rp); - // Consistency - curr_state.consistency_check(rp); - // Terminator - bb.terminator - .get_update(curr_state.len()) - .update_free(&mut curr_state); - // Consistency - curr_state.consistency_check(rp); - // Join repacks - let pcs = bb.terminator.repack_join.as_ref().unwrap(); - assert_eq!(pcs.state(), &curr_state); - for succ in bb.terminator.original_kind.successors() { - let mut curr_state = curr_state.clone(); - // No repack means that `succ` only has one predecessor - if let Some(repack) = pcs.repacks().get(&succ) { - repack.update_free(&mut curr_state, bbs.basic_blocks[succ].is_cleanup, rp); - // Consistency - curr_state.consistency_check(rp); - } - assert_eq!( - bbs.basic_blocks[succ].get_start_state(), - &curr_state, - "{succ:?}" - ); - } - } -} - -impl<'tcx> Repacks<'tcx> { - #[tracing::instrument(level = "debug", skip(rp))] - fn update_free( - &self, - state: &mut FreeState<'tcx>, - can_dealloc: bool, - rp: PlaceRepacker<'_, 'tcx>, - ) { - for rpck in &**self { - match rpck { - RepackOp::Weaken(place, from, to) => { - let curr_state = state[place.local].get_allocated_mut(); - let old = curr_state.insert(*place, *to); - assert_eq!(old, Some(*from), "{rpck:?}, {curr_state:?}"); - } - &RepackOp::DeallocForCleanup(local) => { - assert!(can_dealloc); - let curr_state = state[local].get_allocated_mut(); - assert_eq!(curr_state.len(), 1); - assert_eq!(curr_state[&local.into()], PermissionKind::Uninit); - state[local] = PermissionLocal::Unallocated; - } - &RepackOp::DeallocUnknown(local) => { - assert!(!can_dealloc); - let curr_state = state[local].get_allocated_mut(); - assert_eq!(curr_state.len(), 1); - assert_eq!(curr_state[&local.into()], PermissionKind::Uninit); - state[local] = PermissionLocal::Unallocated; - } - RepackOp::Pack(place, guide, kind) => { - assert_eq!( - place.partial_cmp(*guide), - Some(PlaceOrdering::Prefix), - "{rpck:?}" - ); - let curr_state = state[place.local].get_allocated_mut(); - let mut removed = curr_state - .drain_filter(|p, _| place.related_to(*p)) - .collect::>(); - let (p, others) = rp.expand_one_level(*place, *guide); - assert!(others - .into_iter() - .chain(std::iter::once(p)) - .all(|p| removed.remove(&p).unwrap() == *kind)); - assert!(removed.is_empty(), "{rpck:?}, {removed:?}"); - - let old = curr_state.insert(*place, *kind); - assert_eq!(old, None); - } - RepackOp::Unpack(place, guide, kind) => { - assert_eq!( - place.partial_cmp(*guide), - Some(PlaceOrdering::Prefix), - "{rpck:?}" - ); - let curr_state = state[place.local].get_allocated_mut(); - assert_eq!( - curr_state.remove(place), - Some(*kind), - "{rpck:?} ({:?})", - &**curr_state - ); - - let (p, others) = rp.expand_one_level(*place, *guide); - curr_state.insert(p, *kind); - curr_state.extend(others.into_iter().map(|p| (p, *kind))); - } - } - } - } -} diff --git a/micromir/src/defs/body.rs b/micromir/src/defs/body.rs deleted file mode 100644 index 44d6f81e694..00000000000 --- a/micromir/src/defs/body.rs +++ /dev/null @@ -1,143 +0,0 @@ -// © 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 prusti_rustc_interface::{ - index::vec::IndexVec, - middle::{ - mir::{BasicBlock, BasicBlockData, Body}, - ty::TyCtxt, - }, -}; -use std::{ - fmt::{Display, Formatter, Result}, - rc::Rc, -}; - -use crate::{ - FreeState, MicroStatement, MicroTerminator, TermDebug, TerminatorPlaceCapabilitySummary, -}; - -#[derive(Clone, Debug, Deref, DerefMut)] -pub struct MicroBody<'tcx> { - pub(crate) done_repacking: bool, - pub basic_blocks: MicroBasicBlocks<'tcx>, - #[deref] - #[deref_mut] - pub body: Rc>, -} -impl<'tcx> MicroBody<'tcx> { - pub fn new(body: Rc>, tcx: TyCtxt<'tcx>) -> Self { - let mut body = Self::from(body); - body.calculate_repacking(tcx); - body - } -} - -impl<'tcx> From>> for MicroBody<'tcx> { - /// Clones a `mir::Body` into an identical `MicroBody`. - /// Doesn't calculate any repacking information. - fn from(body: Rc>) -> Self { - let basic_blocks = MicroBasicBlocks::from(&*body); - Self { - done_repacking: false, - basic_blocks, - body, - } - } -} - -#[derive(Clone, Debug)] -pub struct MicroBasicBlocks<'tcx> { - pub basic_blocks: IndexVec>, -} - -impl<'tcx> From<&Body<'tcx>> for MicroBasicBlocks<'tcx> { - #[tracing::instrument(level = "info", skip(body), fields(body = format!("{body:#?}")))] - fn from(body: &Body<'tcx>) -> Self { - Self { - basic_blocks: body - .basic_blocks - .iter() - .map(MicroBasicBlockData::from) - .collect(), - } - } -} - -impl Display for MicroBasicBlocks<'_> { - fn fmt(&self, f: &mut Formatter<'_>) -> Result { - for (bb, data) in self.basic_blocks.iter_enumerated() { - writeln!(f, "{bb:?}: {{")?; - for stmt in &data.statements { - let repack = stmt.repack_operands.as_ref().unwrap(); - writeln!(f, " // {}", repack.state())?; - for rpck in &**repack.repacks() { - writeln!(f, " {rpck:?};")?; - } - for (tmp, operand) in stmt.operands.iter_enumerated() { - writeln!(f, " {tmp:?} <- {operand:?};")?; - } - writeln!(f, " {:?};", stmt.kind)?; - } - let repack = data.terminator.repack_operands.as_ref().unwrap(); - writeln!(f, " // {}", repack.state())?; - for rpck in &**repack.repacks() { - writeln!(f, " {rpck:?};")?; - } - for (tmp, operand) in data.terminator.operands.iter_enumerated() { - writeln!(f, " {tmp:?} <- {operand:?};")?; - } - let display = TermDebug(&data.terminator.kind, &data.terminator.original_kind); - writeln!(f, " {display:?};")?; - let repack = data.terminator.repack_join.as_ref().unwrap(); - // writeln!(f, " // {}", repack.state())?; - for (bb, repacks) in repack.repacks().iter() { - if repacks.is_empty() { - continue; - } - writeln!(f, " {bb:?}:")?; - for rpck in &**repacks { - writeln!(f, " {rpck:?};")?; - } - } - writeln!(f, "}}")?; - } - Ok(()) - } -} - -#[derive(Clone, Debug)] -pub struct MicroBasicBlockData<'tcx> { - pub statements: Vec>, - pub terminator: MicroTerminator<'tcx>, - pub is_cleanup: bool, -} - -impl<'tcx> From<&BasicBlockData<'tcx>> for MicroBasicBlockData<'tcx> { - fn from(data: &BasicBlockData<'tcx>) -> Self { - Self { - statements: data.statements.iter().map(MicroStatement::from).collect(), - terminator: data.terminator().into(), - is_cleanup: data.is_cleanup, - } - } -} - -impl<'tcx> MicroBasicBlockData<'tcx> { - pub(crate) fn get_start_state(&self) -> &FreeState<'tcx> { - if self.statements.is_empty() { - self.terminator.repack_operands.as_ref().unwrap().state() - } else { - self.statements[0].repack_operands.as_ref().unwrap().state() - } - } - pub(crate) fn get_end_pcs_mut( - &mut self, - ) -> Option<&mut TerminatorPlaceCapabilitySummary<'tcx>> { - self.terminator.repack_join.as_mut() - } -} diff --git a/micromir/src/defs/operand.rs b/micromir/src/defs/operand.rs deleted file mode 100644 index 9eb60715523..00000000000 --- a/micromir/src/defs/operand.rs +++ /dev/null @@ -1,100 +0,0 @@ -// © 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 prusti_rustc_interface::{ - index::vec::{Idx, IndexVec}, - middle::mir::{Constant, Operand}, -}; -use std::fmt::{Debug, Formatter, Result}; - -use crate::Place; - -#[derive(Clone, Debug, PartialEq, Hash)] -pub enum MicroFullOperand<'tcx> { - Copy(Place<'tcx>), - Move(Place<'tcx>), - Constant(Box>), -} - -impl<'tcx> From<&Operand<'tcx>> for MicroFullOperand<'tcx> { - fn from(value: &Operand<'tcx>) -> Self { - match value { - &Operand::Copy(p) => MicroFullOperand::Copy(p.into()), - &Operand::Move(p) => MicroFullOperand::Move(p.into()), - Operand::Constant(c) => MicroFullOperand::Constant(c.clone()), - } - } -} - -/// Note that one can have the same `Local` multiple times in the `Operands` vector -/// for a single statement. For example in the following code: -/// ``` -/// struct S { a: bool, b: bool, c: bool } -/// fn true_a(s: &S) -> S { -/// S { a: true, .. *s } -/// } -/// ``` -#[derive(Clone, Debug, Deref, DerefMut)] -pub struct Operands<'tcx>(IndexVec>); -impl<'tcx> Operands<'tcx> { - pub(crate) fn new() -> Self { - Self(IndexVec::new()) - } - pub(crate) fn translate_operand(&mut self, operand: &Operand<'tcx>) -> MicroOperand { - let index = self.push(operand.into()); - MicroOperand::new(index) - } -} - -#[derive(Clone, Copy, Hash, Eq, PartialEq, Deref, DerefMut)] -pub struct MicroOperand(Temporary); -impl MicroOperand { - pub const fn new(value: Temporary) -> Self { - Self(value) - } -} -impl Debug for MicroOperand { - fn fmt(&self, f: &mut Formatter<'_>) -> Result { - write!(f, "{:?}", self.0) - } -} - -#[derive(Clone, Copy, Hash, Eq, PartialEq)] -pub struct Temporary { - private: u32, -} -impl Temporary { - pub const fn from_usize(value: usize) -> Self { - Self { - private: value as u32, - } - } - pub const fn from_u32(value: u32) -> Self { - Self { private: value } - } - pub const fn as_u32(self) -> u32 { - self.private - } - pub const fn as_usize(self) -> usize { - self.private as usize - } -} -impl Idx for Temporary { - fn new(value: usize) -> Self { - Self { - private: value as u32, - } - } - fn index(self) -> usize { - self.private as usize - } -} -impl Debug for Temporary { - fn fmt(&self, f: &mut Formatter<'_>) -> Result { - write!(f, "tmp{}", self.private) - } -} diff --git a/micromir/src/defs/rvalue.rs b/micromir/src/defs/rvalue.rs deleted file mode 100644 index 018fadbc6b6..00000000000 --- a/micromir/src/defs/rvalue.rs +++ /dev/null @@ -1,95 +0,0 @@ -// © 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 crate::{MicroOperand, Operands, Place}; -use prusti_rustc_interface::{ - middle::{ - mir::{AggregateKind, BinOp, BorrowKind, CastKind, Mutability, NullOp, Rvalue, UnOp}, - ty::{self, Region, Ty}, - }, - span::def_id::DefId, -}; - -#[derive(Clone, Debug, PartialEq, Hash)] -pub enum MicroNonDivergingIntrinsic { - Assume(MicroOperand), - CopyNonOverlapping(MicroCopyNonOverlapping), -} - -impl Display for MicroNonDivergingIntrinsic { - fn fmt(&self, f: &mut Formatter<'_>) -> Result { - match self { - Self::Assume(op) => write!(f, "assume({op:?})"), - Self::CopyNonOverlapping(MicroCopyNonOverlapping { src, dst, count }) => { - write!( - f, - "copy_nonoverlapping(dst = {dst:?}, src = {src:?}, count = {count:?})" - ) - } - } - } -} - -#[derive(Clone, Debug, PartialEq, Hash)] -pub struct MicroCopyNonOverlapping { - pub src: MicroOperand, - pub dst: MicroOperand, - pub count: MicroOperand, -} - -#[derive(Clone, Debug, PartialEq, Hash)] -pub enum MicroRvalue<'tcx> { - Use(MicroOperand), - Repeat(MicroOperand, ty::Const<'tcx>), - Ref(Region<'tcx>, BorrowKind, Place<'tcx>), - ThreadLocalRef(DefId), - AddressOf(Mutability, Place<'tcx>), - Len(Place<'tcx>), - Cast(CastKind, MicroOperand, Ty<'tcx>), - BinaryOp(BinOp, Box<(MicroOperand, MicroOperand)>), - CheckedBinaryOp(BinOp, Box<(MicroOperand, MicroOperand)>), - NullaryOp(NullOp, Ty<'tcx>), - UnaryOp(UnOp, MicroOperand), - Discriminant(Place<'tcx>), - Aggregate(Box>, Vec), - ShallowInitBox(MicroOperand, Ty<'tcx>), - CopyForDeref(Place<'tcx>), -} - -impl<'tcx> Operands<'tcx> { - pub(crate) fn translate_rvalue(&mut self, rvalue: &Rvalue<'tcx>) -> MicroRvalue<'tcx> { - match rvalue { - Rvalue::Use(o) => MicroRvalue::Use(self.translate_operand(o)), - Rvalue::Repeat(o, c) => MicroRvalue::Repeat(self.translate_operand(o), *c), - &Rvalue::Ref(r, bk, p) => MicroRvalue::Ref(r, bk, p.into()), - Rvalue::ThreadLocalRef(d) => MicroRvalue::ThreadLocalRef(*d), - &Rvalue::AddressOf(m, p) => MicroRvalue::AddressOf(m, p.into()), - &Rvalue::Len(p) => MicroRvalue::Len(p.into()), - Rvalue::Cast(ck, o, ty) => MicroRvalue::Cast(*ck, self.translate_operand(o), *ty), - Rvalue::BinaryOp(op, box (opa, opb)) => MicroRvalue::BinaryOp( - *op, - box (self.translate_operand(opa), self.translate_operand(opb)), - ), - Rvalue::CheckedBinaryOp(op, box (opa, opb)) => MicroRvalue::CheckedBinaryOp( - *op, - box (self.translate_operand(opa), self.translate_operand(opb)), - ), - Rvalue::NullaryOp(op, ty) => MicroRvalue::NullaryOp(*op, *ty), - Rvalue::UnaryOp(op, o) => MicroRvalue::UnaryOp(*op, self.translate_operand(o)), - &Rvalue::Discriminant(p) => MicroRvalue::Discriminant(p.into()), - Rvalue::Aggregate(ak, ops) => MicroRvalue::Aggregate( - ak.clone(), - ops.iter().map(|o| self.translate_operand(o)).collect(), - ), - Rvalue::ShallowInitBox(o, ty) => { - MicroRvalue::ShallowInitBox(self.translate_operand(o), *ty) - } - &Rvalue::CopyForDeref(p) => MicroRvalue::CopyForDeref(p.into()), - } - } -} diff --git a/micromir/src/defs/statement.rs b/micromir/src/defs/statement.rs deleted file mode 100644 index bec83324385..00000000000 --- a/micromir/src/defs/statement.rs +++ /dev/null @@ -1,161 +0,0 @@ -// © 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 core::fmt::{Debug, Formatter, Result}; -use prusti_rustc_interface::{ - middle::{ - mir::{ - Coverage, FakeReadCause, Local, NonDivergingIntrinsic, RetagKind, Statement, - StatementKind, UserTypeProjection, - }, - ty, - }, - target::abi::VariantIdx, -}; - -use crate::{ - MicroCopyNonOverlapping, MicroNonDivergingIntrinsic, MicroRvalue, Operands, Place, - PlaceCapabilitySummary, -}; - -#[derive(Clone)] -/// Note that in rare cases an operand and the target of kind can be the same place! -/// For example, the following function: -/// https://github.com/dtolnay/syn/blob/636509368ed9dbfad8bf3d15f84b0046804a1c14/src/bigint.rs#L13-L29 -/// generates a `MicroStatement { operands: [Copy(_5), Move(_22)], stmt: _5 = BinaryOp(BitOr, (tmp0, tmp1)) }` -pub struct MicroStatement<'tcx> { - pub repack_operands: Option>, - pub operands: Operands<'tcx>, - // pub repack_stmt: Option>, - pub kind: MicroStatementKind<'tcx>, -} - -#[derive(Clone, PartialEq, Hash)] -pub enum MicroStatementKind<'tcx> { - Assign(Box<(Place<'tcx>, MicroRvalue<'tcx>)>), - FakeRead(Box<(FakeReadCause, Place<'tcx>)>), - SetDiscriminant { - place: Box>, - variant_index: VariantIdx, - }, - Deinit(Box>), - StorageLive(Local), - StorageDead(Local), - Retag(RetagKind, Box>), - AscribeUserType(Box<(Place<'tcx>, UserTypeProjection)>, ty::Variance), - Coverage(Box), - Intrinsic(Box), - ConstEvalCounter, - Nop, -} - -impl<'tcx> From<&Statement<'tcx>> for MicroStatement<'tcx> { - fn from(stmt: &Statement<'tcx>) -> Self { - let mut operands = Operands::new(); - let kind = match &stmt.kind { - StatementKind::Assign(box (p, r)) => { - MicroStatementKind::Assign(box ((*p).into(), operands.translate_rvalue(r))) - } - &StatementKind::FakeRead(box (c, p)) => MicroStatementKind::FakeRead(box (c, p.into())), - &StatementKind::SetDiscriminant { - box place, - variant_index, - } => MicroStatementKind::SetDiscriminant { - place: box place.into(), - variant_index, - }, - &StatementKind::Deinit(box p) => MicroStatementKind::Deinit(box p.into()), - &StatementKind::StorageLive(l) => MicroStatementKind::StorageLive(l), - &StatementKind::StorageDead(l) => MicroStatementKind::StorageDead(l), - &StatementKind::Retag(k, box p) => MicroStatementKind::Retag(k, box p.into()), - StatementKind::AscribeUserType(box (p, ty), v) => { - MicroStatementKind::AscribeUserType(box ((*p).into(), ty.clone()), *v) - } - StatementKind::Coverage(box c) => MicroStatementKind::Coverage(box c.clone()), - StatementKind::Intrinsic(box NonDivergingIntrinsic::Assume(o)) => { - MicroStatementKind::Intrinsic(box MicroNonDivergingIntrinsic::Assume( - operands.translate_operand(o), - )) - } - StatementKind::Intrinsic(box NonDivergingIntrinsic::CopyNonOverlapping(c)) => { - MicroStatementKind::Intrinsic(box MicroNonDivergingIntrinsic::CopyNonOverlapping( - MicroCopyNonOverlapping { - src: operands.translate_operand(&c.src), - dst: operands.translate_operand(&c.dst), - count: operands.translate_operand(&c.count), - }, - )) - } - StatementKind::ConstEvalCounter => MicroStatementKind::ConstEvalCounter, - StatementKind::Nop => MicroStatementKind::Nop, - }; - MicroStatement { - repack_operands: None, - operands, - // repack_stmt: None, - kind, - } - } -} - -impl Debug for MicroStatement<'_> { - fn fmt(&self, fmt: &mut Formatter<'_>) -> Result { - let mut dbg = fmt.debug_struct("MicroStatement"); - if let Some(repack) = &self.repack_operands { - dbg.field("pcs", repack); - } - if self.operands.len() > 0 { - dbg.field("operands", &*self.operands); - } - dbg.field("stmt", &self.kind); - dbg.finish() - } -} - -impl Debug for MicroStatementKind<'_> { - fn fmt(&self, fmt: &mut Formatter<'_>) -> Result { - use MicroStatementKind::*; - match self { - Assign(box (ref place, ref rv)) => write!(fmt, "{place:?} = {rv:?}"), - FakeRead(box (ref cause, ref place)) => { - write!(fmt, "FakeRead({cause:?}, {place:?})") - } - Retag(ref kind, ref place) => write!( - fmt, - "Retag({}{:?})", - match kind { - RetagKind::FnEntry => "[fn entry] ", - RetagKind::TwoPhase => "[2phase] ", - RetagKind::Raw => "[raw] ", - RetagKind::Default => "", - }, - place, - ), - StorageLive(ref place) => write!(fmt, "StorageLive({place:?})"), - StorageDead(ref place) => write!(fmt, "StorageDead({place:?})"), - SetDiscriminant { - ref place, - variant_index, - } => { - write!(fmt, "discriminant({place:?}) = {variant_index:?}") - } - Deinit(ref place) => write!(fmt, "Deinit({place:?})"), - AscribeUserType(box (ref place, ref c_ty), ref variance) => { - write!(fmt, "AscribeUserType({place:?}, {variance:?}, {c_ty:?})") - } - Coverage(box self::Coverage { - ref kind, - code_region: Some(ref rgn), - }) => { - write!(fmt, "Coverage::{kind:?} for {rgn:?}") - } - Coverage(box ref coverage) => write!(fmt, "Coverage::{:?}", coverage.kind), - Intrinsic(box ref intrinsic) => write!(fmt, "{intrinsic}"), - ConstEvalCounter => write!(fmt, "ConstEvalCounter"), - Nop => write!(fmt, "nop"), - } - } -} diff --git a/micromir/src/defs/terminator.rs b/micromir/src/defs/terminator.rs deleted file mode 100644 index 36fa2f25b8c..00000000000 --- a/micromir/src/defs/terminator.rs +++ /dev/null @@ -1,401 +0,0 @@ -// © 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 core::fmt::{Debug, Formatter, Result, Write}; -use prusti_rustc_interface::{ - middle::mir::{AssertMessage, BasicBlock, SwitchTargets, Terminator, TerminatorKind}, - span::Span, -}; -use std::{borrow::Cow, iter}; - -use crate::{ - FreeState, MicroOperand, Operands, Place, PlaceCapabilitySummary, - TerminatorPlaceCapabilitySummary, -}; - -#[derive(Clone)] -pub struct MicroTerminator<'tcx> { - pub repack_operands: Option>, - pub operands: Operands<'tcx>, - pub kind: MicroTerminatorKind<'tcx>, - pub repack_join: Option>, - // TODO: debug only - pub previous_rjs: Vec>, - pub original_kind: TerminatorKind<'tcx>, -} - -#[derive(Clone, PartialEq, Hash)] -pub enum MicroTerminatorKind<'tcx> { - Goto { - target: BasicBlock, - }, - SwitchInt { - discr: MicroOperand, - targets: SwitchTargets, - }, - Resume, - Abort, - Return, - Unreachable, - Drop { - place: Place<'tcx>, - target: BasicBlock, - unwind: Option, - }, - DropAndReplace { - place: Place<'tcx>, - value: MicroOperand, - target: BasicBlock, - unwind: Option, - }, - Call { - func: MicroOperand, - args: Vec, - destination: Place<'tcx>, - target: Option, - cleanup: Option, - from_hir_call: bool, - fn_span: Span, - }, - Assert { - cond: MicroOperand, - expected: bool, - msg: AssertMessage<'tcx>, - target: BasicBlock, - cleanup: Option, - }, - Yield { - value: MicroOperand, - resume: BasicBlock, - resume_arg: Place<'tcx>, - drop: Option, - }, - GeneratorDrop, - FalseEdge { - real_target: BasicBlock, - imaginary_target: BasicBlock, - }, - FalseUnwind { - real_target: BasicBlock, - unwind: Option, - }, - // InlineAsm { - // template: &'tcx [InlineAsmTemplatePiece], - // operands: Vec>, - // options: InlineAsmOptions, - // line_spans: &'tcx [Span], - // destination: Option, - // cleanup: Option, - // }, -} - -impl<'tcx> From<&Terminator<'tcx>> for MicroTerminator<'tcx> { - fn from(term: &Terminator<'tcx>) -> Self { - let mut operands = Operands::new(); - let kind = match &term.kind { - &TerminatorKind::Goto { target } => MicroTerminatorKind::Goto { target }, - TerminatorKind::SwitchInt { discr, targets } => MicroTerminatorKind::SwitchInt { - discr: operands.translate_operand(discr), - targets: targets.clone(), - }, - TerminatorKind::Resume => MicroTerminatorKind::Resume, - TerminatorKind::Abort => MicroTerminatorKind::Abort, - TerminatorKind::Return => MicroTerminatorKind::Return, - TerminatorKind::Unreachable => MicroTerminatorKind::Unreachable, - &TerminatorKind::Drop { - place, - target, - unwind, - } => MicroTerminatorKind::Drop { - place: place.into(), - target, - unwind, - }, - TerminatorKind::DropAndReplace { - place, - value, - target, - unwind, - } => MicroTerminatorKind::DropAndReplace { - place: (*place).into(), - value: operands.translate_operand(value), - target: *target, - unwind: *unwind, - }, - TerminatorKind::Call { - func, - args, - destination, - target, - cleanup, - from_hir_call, - fn_span, - } => MicroTerminatorKind::Call { - func: operands.translate_operand(func), - args: args.iter().map(|a| operands.translate_operand(a)).collect(), - destination: (*destination).into(), - target: *target, - cleanup: *cleanup, - from_hir_call: *from_hir_call, - fn_span: *fn_span, - }, - TerminatorKind::Assert { - cond, - expected, - msg, - target, - cleanup, - } => MicroTerminatorKind::Assert { - cond: operands.translate_operand(cond), - expected: *expected, - msg: msg.clone(), - target: *target, - cleanup: *cleanup, - }, - TerminatorKind::Yield { - value, - resume, - resume_arg, - drop, - } => MicroTerminatorKind::Yield { - value: operands.translate_operand(value), - resume: *resume, - resume_arg: (*resume_arg).into(), - drop: *drop, - }, - TerminatorKind::GeneratorDrop => MicroTerminatorKind::GeneratorDrop, - &TerminatorKind::FalseEdge { - real_target, - imaginary_target, - } => MicroTerminatorKind::FalseEdge { - real_target, - imaginary_target, - }, - &TerminatorKind::FalseUnwind { - real_target, - unwind, - } => MicroTerminatorKind::FalseUnwind { - real_target, - unwind, - }, - TerminatorKind::InlineAsm { .. } => todo!(), - }; - MicroTerminator { - repack_operands: None, - operands, - kind, - repack_join: None, - previous_rjs: Vec::new(), - original_kind: term.kind.clone(), - } - } -} - -impl<'tcx> Debug for MicroTerminator<'tcx> { - fn fmt(&self, f: &mut Formatter<'_>) -> Result { - let mut dbg = f.debug_struct("MicroTerminator"); - if let Some(repack) = &self.repack_operands { - dbg.field("pcs", repack); - } - if self.operands.len() > 0 { - dbg.field("operands", &*self.operands); - } - dbg.field("term", &TermDebug(&self.kind, &self.original_kind)); - if let Some(repack) = &self.repack_join { - dbg.field("pcs_join", repack); - } - dbg.finish() - } -} - -pub(crate) struct TermDebug<'a, 'tcx>( - pub(crate) &'a MicroTerminatorKind<'tcx>, - pub(crate) &'a TerminatorKind<'tcx>, -); -impl<'a, 'tcx> Debug for TermDebug<'a, 'tcx> { - fn fmt(&self, fmt: &mut Formatter<'_>) -> Result { - self.0.fmt_head(fmt)?; - let successor_count = self.1.successors().count(); - let labels = self.0.fmt_successor_labels(); - assert_eq!(successor_count, labels.len()); - - match successor_count { - 0 => Ok(()), - 1 => write!(fmt, " -> {:?}", self.1.successors().next().unwrap()), - _ => { - write!(fmt, " -> [")?; - for (i, target) in self.1.successors().enumerate() { - if i > 0 { - write!(fmt, ", ")?; - } - write!(fmt, "{}: {:?}", labels[i], target)?; - } - write!(fmt, "]") - } - } - } -} - -impl<'tcx> MicroTerminatorKind<'tcx> { - pub fn fmt_head(&self, fmt: &mut W) -> Result { - use MicroTerminatorKind::*; - match self { - Goto { .. } => write!(fmt, "goto"), - SwitchInt { discr, .. } => write!(fmt, "switchInt({discr:?})"), - Return => write!(fmt, "return"), - GeneratorDrop => write!(fmt, "generator_drop"), - Resume => write!(fmt, "resume"), - Abort => write!(fmt, "abort"), - Yield { - value, resume_arg, .. - } => write!(fmt, "{resume_arg:?} = yield({value:?})"), - Unreachable => write!(fmt, "unreachable"), - Drop { place, .. } => write!(fmt, "drop({place:?})"), - DropAndReplace { place, value, .. } => { - write!(fmt, "replace({place:?} <- {value:?})") - } - Call { - func, - args, - destination, - .. - } => { - write!(fmt, "{destination:?} = ")?; - write!(fmt, "{func:?}(")?; - for (index, arg) in args.iter().enumerate() { - if index > 0 { - write!(fmt, ", ")?; - } - write!(fmt, "{arg:?}")?; - } - write!(fmt, ")") - } - Assert { - cond, - expected, - msg, - .. - } => { - write!(fmt, "assert(")?; - if !expected { - write!(fmt, "!")?; - } - write!(fmt, "{cond:?}, ")?; - msg.fmt_assert_args(fmt)?; - write!(fmt, ")") - } - FalseEdge { .. } => write!(fmt, "falseEdge"), - FalseUnwind { .. } => write!(fmt, "falseUnwind"), - // InlineAsm { template, ref operands, options, .. } => { - // write!(fmt, "asm!(\"{}\"", InlineAsmTemplatePiece::to_string(template))?; - // for op in operands { - // write!(fmt, ", ")?; - // let print_late = |&late| if late { "late" } else { "" }; - // match op { - // InlineAsmOperand::In { reg, value } => { - // write!(fmt, "in({}) {:?}", reg, value)?; - // } - // InlineAsmOperand::Out { reg, late, place: Some(place) } => { - // write!(fmt, "{}out({}) {:?}", print_late(late), reg, place)?; - // } - // InlineAsmOperand::Out { reg, late, place: None } => { - // write!(fmt, "{}out({}) _", print_late(late), reg)?; - // } - // InlineAsmOperand::InOut { - // reg, - // late, - // in_value, - // out_place: Some(out_place), - // } => { - // write!( - // fmt, - // "in{}out({}) {:?} => {:?}", - // print_late(late), - // reg, - // in_value, - // out_place - // )?; - // } - // InlineAsmOperand::InOut { reg, late, in_value, out_place: None } => { - // write!(fmt, "in{}out({}) {:?} => _", print_late(late), reg, in_value)?; - // } - // InlineAsmOperand::Const { value } => { - // write!(fmt, "const {:?}", value)?; - // } - // InlineAsmOperand::SymFn { value } => { - // write!(fmt, "sym_fn {:?}", value)?; - // } - // InlineAsmOperand::SymStatic { def_id } => { - // write!(fmt, "sym_static {:?}", def_id)?; - // } - // } - // } - // write!(fmt, ", options({:?}))", options) - // } - } - } - - pub fn fmt_successor_labels(&self) -> Vec> { - use MicroTerminatorKind::*; - match *self { - Return | Resume | Abort | Unreachable | GeneratorDrop => vec![], - Goto { .. } => vec!["".into()], - SwitchInt { ref targets, .. } => targets - .iter() - .map(|(u, _)| Cow::Owned(u.to_string())) - .chain(iter::once("otherwise".into())) - .collect(), - Call { - target: Some(_), - cleanup: Some(_), - .. - } => { - vec!["return".into(), "unwind".into()] - } - Call { - target: Some(_), - cleanup: None, - .. - } => vec!["return".into()], - Call { - target: None, - cleanup: Some(_), - .. - } => vec!["unwind".into()], - Call { - target: None, - cleanup: None, - .. - } => vec![], - Yield { drop: Some(_), .. } => vec!["resume".into(), "drop".into()], - Yield { drop: None, .. } => vec!["resume".into()], - DropAndReplace { unwind: None, .. } | Drop { unwind: None, .. } => { - vec!["return".into()] - } - DropAndReplace { - unwind: Some(_), .. - } - | Drop { - unwind: Some(_), .. - } => { - vec!["return".into(), "unwind".into()] - } - Assert { cleanup: None, .. } => vec!["".into()], - Assert { .. } => vec!["success".into(), "unwind".into()], - FalseEdge { .. } => vec!["real".into(), "imaginary".into()], - FalseUnwind { - unwind: Some(_), .. - } => vec!["real".into(), "cleanup".into()], - FalseUnwind { unwind: None, .. } => vec!["real".into()], - // InlineAsm { destination: Some(_), cleanup: Some(_), .. } => { - // vec!["return".into(), "unwind".into()] - // } - // InlineAsm { destination: Some(_), cleanup: None, .. } => vec!["return".into()], - // InlineAsm { destination: None, cleanup: Some(_), .. } => vec!["unwind".into()], - // InlineAsm { destination: None, cleanup: None, .. } => vec![], - } - } -} diff --git a/micromir/src/free_pcs/permission.rs b/micromir/src/free_pcs/permission.rs deleted file mode 100644 index 2b0b5422fd3..00000000000 --- a/micromir/src/free_pcs/permission.rs +++ /dev/null @@ -1,517 +0,0 @@ -// © 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, Display, Formatter, Result}, -}; - -use derive_more::{Deref, DerefMut}; - -use prusti_rustc_interface::{ - data_structures::fx::{FxHashMap, FxHashSet}, - index::vec::IndexVec, - middle::mir::Local, -}; - -use crate::{Place, PlaceOrdering, PlaceRepacker}; - -pub type FreeStateUpdate<'tcx> = LocalsState>; -#[derive(Clone, Debug, PartialEq, Eq, Deref, DerefMut, Default)] -pub struct LocalUpdate<'tcx>( - ( - Option>, - Option>, - ), -); - -#[derive(Clone, Debug, PartialEq, Eq, Deref, DerefMut, Default)] -pub struct LocalRequirement<'tcx> { - unalloc_allowed: bool, - #[deref] - #[deref_mut] - place_reqs: FxHashMap, FxHashSet>, -} - -impl<'tcx> LocalUpdate<'tcx> { - fn init_pre(&mut self) -> &mut LocalRequirement<'tcx> { - assert!(self.0 .0.is_none()); - self.0 .0 = Some(LocalRequirement::default()); - self.0 .0.as_mut().unwrap() - } - pub(crate) fn requires_unalloc_or_uninit(&mut self, local: Local) { - let req = self.init_pre(); - req.unalloc_allowed = true; - self.requires_alloc(local.into(), &[PermissionKind::Uninit]); - } - pub(crate) fn requires_alloc(&mut self, place: Place<'tcx>, perms: &[PermissionKind]) { - let req = if self.0 .0.is_none() { - self.init_pre() - } else { - self.0 .0.as_mut().unwrap() - }; - assert!( - req.keys().all(|other| !place.related_to(*other)), - "{req:?} {place:?} {perms:?}" - ); - req.insert(place, perms.iter().copied().collect()); - } - pub(crate) fn requires_unalloc(&mut self) { - let req = self.init_pre(); - req.unalloc_allowed = true; - } - pub(crate) fn requires_alloc_one(&mut self, place: Place<'tcx>, perm: PermissionKind) { - self.requires_alloc(place, &[perm]); - } - - pub(crate) fn ensures_unalloc(&mut self) { - assert!(self.0 .1.is_none()); - self.0 .1 = Some(PermissionLocal::Unallocated); - } - pub(crate) fn ensures_alloc(&mut self, place: Place<'tcx>, perm: PermissionKind) { - if let Some(pre) = &mut self.0 .1 { - let pre = pre.get_allocated_mut(); - assert!(pre.keys().all(|other| !place.related_to(*other))); - pre.insert(place, perm); - } else { - self.0 .1 = Some(PermissionLocal::Allocated( - PermissionProjections::new_update(place, perm), - )); - } - } - - /// Used for the edge case of assigning to the same place you copy from, do not use otherwise! - pub(crate) fn get_pre_for(&self, place: Place<'tcx>) -> Option<&FxHashSet> { - let pre = self.0 .0.as_ref()?; - pre.get(&place) - } - - pub(crate) fn get_pre(&self, state: &PermissionLocal<'tcx>) -> Option> { - let pre = self.0 .0.as_ref()?; - match state { - PermissionLocal::Unallocated => { - assert!(pre.unalloc_allowed); - Some(PermissionLocal::Unallocated) - } - PermissionLocal::Allocated(state) => { - let mut achievable = PermissionProjections(FxHashMap::default()); - for (place, allowed_perms) in pre.iter() { - let related_set = state.find_all_related(*place, None); - let mut perm = None; - for &ap in allowed_perms { - if related_set.minimum >= ap { - perm = Some(ap); - } - if related_set.minimum == ap { - break; - } - } - assert!( - perm.is_some(), - "{place:?}, {allowed_perms:?}, {state:?}, {:?}, {:?}", - related_set.minimum, - related_set.from - ); - achievable.insert(*place, perm.unwrap()); - } - Some(PermissionLocal::Allocated(achievable)) - } - } - } -} - -#[derive(Clone, Debug, PartialEq, Eq, Deref, DerefMut)] -/// Generic state of a set of locals -pub struct LocalsState(IndexVec); - -/// The free pcs of all locals -pub type FreeState<'tcx> = LocalsState>; - -impl FromIterator for LocalsState { - fn from_iter>(iter: I) -> Self { - Self(IndexVec::from_iter(iter)) - } -} -impl Display for FreeState<'_> { - fn fmt(&self, f: &mut Formatter<'_>) -> Result { - write!(f, "{{")?; - let mut first = true; - for state in self.iter() { - if let PermissionLocal::Allocated(state) = state { - if !first { - write!(f, ", ")?; - } - first = false; - for (i, (place, perm)) in state.iter().enumerate() { - if i != 0 { - write!(f, ", ")?; - } - write!(f, "{perm:?} {place:?}")?; - } - } - } - write!(f, "}}") - } -} - -impl<'tcx> LocalsState> { - pub fn initial(local_count: usize, initial: impl Fn(Local) -> Option) -> Self { - Self(IndexVec::from_fn_n( - |local: Local| { - if let Some(perm) = initial(local) { - let places = PermissionProjections::new(local, perm); - PermissionLocal::Allocated(places) - } else { - PermissionLocal::Unallocated - } - }, - local_count, - )) - } - #[tracing::instrument(level = "trace", skip(rp))] - pub(crate) fn consistency_check(&self, rp: PlaceRepacker<'_, 'tcx>) { - for p in self.iter() { - p.consistency_check(rp); - } - } -} -impl LocalsState { - pub fn default(local_count: usize) -> Self - where - T: Default + Clone, - { - Self(IndexVec::from_elem_n(T::default(), local_count)) - } - pub fn empty(local_count: usize, initial: T) -> Self - where - T: Clone, - { - Self(IndexVec::from_elem_n(initial, local_count)) - } -} -impl<'tcx> LocalsState> { - pub fn update_free(self, state: &mut FreeState<'tcx>) { - for (local, update) in self.0.into_iter_enumerated() { - if cfg!(debug_assertions) { - use PermissionLocal::*; - match (&state[local], update.get_pre(&state[local])) { - (_, None) => {} - (Unallocated, Some(Unallocated)) => {} - (Allocated(local_state), Some(Allocated(pre))) => { - for (place, required_perm) in pre.0 { - let perm = *local_state.get(&place).unwrap(); - let is_read = required_perm.is_shared() && perm.is_exclusive(); - assert!( - perm == required_perm || is_read, - "Have\n{state:#?}\n{place:#?}\n{perm:#?}\n{required_perm:#?}\n" - ); - } - } - _ => unreachable!(), - } - } - if let Some(post) = update.0 .1 { - match (post, &mut state[local]) { - (post @ PermissionLocal::Unallocated, _) - | (post, PermissionLocal::Unallocated) => state[local] = post, - (PermissionLocal::Allocated(post), PermissionLocal::Allocated(state)) => { - state.extend(post.0) - } - } - } - } - } -} - -#[derive(Clone, PartialEq, Eq)] -/// The permissions of a local -pub enum PermissionLocal<'tcx> { - Unallocated, - Allocated(PermissionProjections<'tcx>), -} -impl Debug for PermissionLocal<'_> { - fn fmt(&self, f: &mut Formatter<'_>) -> Result { - match self { - PermissionLocal::Unallocated => write!(f, "U"), - PermissionLocal::Allocated(a) => write!(f, "{a:?}"), - } - } -} - -impl<'tcx> PermissionLocal<'tcx> { - pub fn get_allocated(&self) -> &PermissionProjections<'tcx> { - match self { - PermissionLocal::Allocated(places) => places, - _ => panic!(), - } - } - pub fn get_allocated_mut(&mut self) -> &mut PermissionProjections<'tcx> { - match self { - PermissionLocal::Allocated(places) => places, - _ => panic!(), - } - } - - fn consistency_check(&self, rp: PlaceRepacker<'_, 'tcx>) { - match self { - PermissionLocal::Unallocated => {} - PermissionLocal::Allocated(places) => { - places.consistency_check(rp); - } - } - } -} - -#[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 PermissionProjections<'tcx>(FxHashMap, PermissionKind>); - -impl<'tcx> Debug for PermissionProjections<'tcx> { - fn fmt(&self, f: &mut Formatter<'_>) -> Result { - self.0.fmt(f) - } -} - -#[derive(Debug)] -pub(crate) struct RelatedSet<'tcx> { - pub(crate) from: Vec<(Place<'tcx>, PermissionKind)>, - pub(crate) to: Place<'tcx>, - pub(crate) minimum: PermissionKind, - 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() - } -} - -impl<'tcx> PermissionProjections<'tcx> { - pub fn new(local: Local, perm: PermissionKind) -> Self { - Self([(local.into(), perm)].into_iter().collect()) - } - pub fn new_uninit(local: Local) -> Self { - Self::new(local, PermissionKind::Uninit) - } - /// Should only be called when creating an update within `ModifiesFreeState` - pub(crate) fn new_update(place: Place<'tcx>, perm: PermissionKind) -> Self { - Self([(place, perm)].into_iter().collect()) - } - - /// 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 = "trace", 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, &perm) in &**self { - if let Some(ord) = from.partial_cmp(to) { - minimum = if let Some(min) = minimum { - Some(min.minimum(perm).unwrap()) - } else { - Some(perm) - }; - if let Some(expected) = expected { - assert_eq!(ord, expected); - } else { - expected = Some(ord); - } - related.push((from, perm)); - } - } - 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, - } - } - // pub fn all_related_with_minimum( - // &self, - // place: Place<'tcx>, - // ) -> (PermissionKind, PlaceOrdering, Vec<(Place<'tcx>, PermissionKind)>) { - // let mut ord = None; - // let related: Vec<_> = self - // .find_all_related(place, &mut ord) - // .map(|(_, p, k)| (p, k)) - // .collect(); - // let mut minimum = related.iter().map(|(_, k)| *k).reduce(|acc, k| { - // acc.minimum(k).unwrap() - // }); - // (minimum.unwrap(), ord.unwrap(), related) - // } - - #[tracing::instrument(name = "PermissionProjections::unpack", level = "trace", skip(rp), ret)] - pub(crate) fn unpack( - &mut self, - from: Place<'tcx>, - to: Place<'tcx>, - rp: PlaceRepacker<'_, 'tcx>, - ) -> Vec<(Place<'tcx>, Place<'tcx>)> { - debug_assert!(!self.contains_key(&to)); - let (expanded, others) = rp.expand(from, to); - let perm = self.remove(&from).unwrap(); - self.extend(others.into_iter().map(|p| (p, perm))); - self.insert(to, perm); - expanded - } - - // TODO: this could be implemented more efficiently, by assuming that a valid - // state can always be packed up to the root - #[tracing::instrument(name = "PermissionProjections::pack", level = "trace", skip(rp), ret)] - pub(crate) fn pack( - &mut self, - mut from: FxHashSet>, - to: Place<'tcx>, - perm: PermissionKind, - rp: PlaceRepacker<'_, 'tcx>, - ) -> Vec<(Place<'tcx>, Place<'tcx>)> { - debug_assert!(!self.contains_key(&to)); - for place in &from { - let p = self.remove(place).unwrap(); - assert_eq!(p, perm, "Cannot pack {place:?} with {p:?} into {to:?}"); - } - let collapsed = rp.collapse(to, &mut from); - assert!(from.is_empty()); - self.insert(to, perm); - collapsed - } - - #[tracing::instrument(name = "PermissionProjections::join", level = "info", skip(rp))] - pub(crate) fn join(&self, other: &mut Self, rp: PlaceRepacker<'_, 'tcx>) { - for (&place, &kind) in &**self { - let related = other.find_all_related(place, None); - match related.relation { - PlaceOrdering::Prefix => { - let from = related.from[0].0; - let joinable_place = rp.joinable_to(from, place); - if joinable_place != from { - other.unpack(from, joinable_place, rp); - } - // Downgrade the permission if needed - let new_min = kind.minimum(related.minimum).unwrap(); - if new_min != related.minimum { - other.insert(joinable_place, new_min); - } - } - PlaceOrdering::Equal => { - // Downgrade the permission if needed - let new_min = kind.minimum(related.minimum).unwrap(); - if new_min != related.minimum { - other.insert(place, new_min); - } - } - PlaceOrdering::Suffix => { - // Downgrade the permission if needed - for &(p, k) in &related.from { - let new_min = kind.minimum(k).unwrap(); - if new_min != k { - other.insert(p, new_min); - } - } - } - PlaceOrdering::Both => { - // Downgrade the permission if needed - let min = kind.minimum(related.minimum).unwrap(); - for &(p, k) in &related.from { - let new_min = min.minimum(k).unwrap(); - if new_min != k { - other.insert(p, new_min); - } - } - let cp = rp.common_prefix(related.from[0].0, place); - other.pack(related.get_from(), cp, min, rp); - } - } - } - } - - fn consistency_check(&self, rp: 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:?}",); - } - } - // Can always pack up to the root - let root: Place = self.iter().next().unwrap().0.local.into(); - let mut keys = self.keys().copied().collect(); - rp.collapse(root, &mut keys); - assert!(keys.is_empty()); - } -} - -#[derive(Copy, Clone, PartialEq, Eq, Hash)] -pub enum PermissionKind { - Shared, - Exclusive, - Uninit, -} - -impl Debug for PermissionKind { - fn fmt(&self, f: &mut Formatter<'_>) -> Result { - match self { - PermissionKind::Shared => write!(f, "s"), - PermissionKind::Exclusive => write!(f, "e"), - PermissionKind::Uninit => write!(f, "u"), - } - } -} - -impl PartialOrd for PermissionKind { - fn partial_cmp(&self, other: &Self) -> Option { - if *self == *other { - return Some(Ordering::Equal); - } - match (self, other) { - (PermissionKind::Shared, PermissionKind::Exclusive) - | (PermissionKind::Uninit, PermissionKind::Exclusive) => Some(Ordering::Less), - (PermissionKind::Exclusive, PermissionKind::Shared) - | (PermissionKind::Exclusive, PermissionKind::Uninit) => Some(Ordering::Greater), - (PermissionKind::Shared, PermissionKind::Uninit) - | (PermissionKind::Uninit, PermissionKind::Shared) => None, - _ => unreachable!(), - } - } -} - -impl PermissionKind { - pub fn is_shared(self) -> bool { - self == PermissionKind::Shared - } - pub fn is_exclusive(self) -> bool { - self == PermissionKind::Exclusive - } - pub fn is_uninit(self) -> bool { - self == PermissionKind::Uninit - } - pub fn minimum(self, other: Self) -> Option { - match self.partial_cmp(&other)? { - Ordering::Greater => Some(other), - _ => Some(self), - } - } -} diff --git a/micromir/src/lib.rs b/micromir/src/lib.rs deleted file mode 100644 index a40c4bccfcd..00000000000 --- a/micromir/src/lib.rs +++ /dev/null @@ -1,36 +0,0 @@ -// © 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_syntax, box_patterns)] -#![feature(drain_filter, hash_drain_filter)] -#![feature(type_alias_impl_trait)] - -mod check; -mod defs; -mod repack; -mod free_pcs; -mod utils; - -pub use defs::*; -pub use free_pcs::*; -pub use repack::*; -pub use utils::place::*; - -use prusti_interface::environment::Environment; - -pub fn test_free_pcs(env: &Environment) { - for proc_id in env.get_annotated_procedures_and_types().0.iter() { - let name = env.name.get_unique_item_name(*proc_id); - // if name != "syn::ty::parsing::ambig_ty" { - // continue; - // } - println!("id: {name}"); - let current_procedure = env.get_procedure(*proc_id); - let mir = current_procedure.get_mir_rc(); - let _ = MicroBody::new(mir, env.tcx()); - } -} diff --git a/micromir/src/repack/calculate.rs b/micromir/src/repack/calculate.rs deleted file mode 100644 index df626086e35..00000000000 --- a/micromir/src/repack/calculate.rs +++ /dev/null @@ -1,295 +0,0 @@ -// © 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, graph::WithStartNode}, - dataflow::storage, - index::vec::{Idx, IndexVec}, - middle::{ - mir::{BasicBlock, HasLocalDecls, Local, RETURN_PLACE}, - ty::TyCtxt, - }, -}; - -use crate::{ - check::checker, FreeState, MicroBasicBlockData, MicroBasicBlocks, MicroBody, MicroStatement, - MicroTerminator, PermissionKind, TerminatorPlaceCapabilitySummary, -}; - -use super::{place::PlaceRepacker, triple::ModifiesFreeState}; - -impl<'tcx> MicroBody<'tcx> { - fn initial_free_state(&self) -> FreeState<'tcx> { - let always_live = storage::always_storage_live_locals(&self.body); - let return_local = RETURN_PLACE; - let last_arg = Local::new(self.body.arg_count); - FreeState::initial(self.body.local_decls().len(), |local: Local| { - if local == return_local { - Some(PermissionKind::Uninit) - // TODO: figure out if `always_live` should start as `Uninit` or `Exclusive` - } else if local <= last_arg || always_live.contains(local) { - Some(PermissionKind::Exclusive) - } else { - None - } - }) - } - pub fn calculate_repacking(&mut self, tcx: TyCtxt<'tcx>) { - // Safety check - assert!(!self.done_repacking); - self.done_repacking = true; - - // Calculate initial state - let state = self.initial_free_state(); - let preds = self.body.basic_blocks.predecessors(); - let rp = PlaceRepacker::new(&self.body, tcx); - let start_node = self.body.basic_blocks.start_node(); - - // Do the actual repacking calculation - self.basic_blocks - .calculate_repacking(start_node, state, |bb| &preds[bb], rp); - - if cfg!(debug_assertions) { - // println!("--------\n{}\n--------", &self.basic_blocks); - checker::check(&self.basic_blocks, rp); - } - } -} - -#[derive(Debug)] -struct Queue { - queue: Vec, - dirty_queue: FxHashSet, - done: IndexVec, - can_redo: IndexVec, - recompute_count: IndexVec, -} -impl Queue { - fn new(start_node: BasicBlock, len: usize) -> Self { - let mut done = IndexVec::from_elem_n(false, len); - done[start_node] = true; - Self { - queue: Vec::new(), - dirty_queue: FxHashSet::default(), - done, - can_redo: IndexVec::from_elem_n(true, len), - recompute_count: IndexVec::from_elem_n(0, len), - } - } - fn add_succs<'a>( - &mut self, - term: &MicroTerminator, - preds: impl Fn(BasicBlock) -> &'a [BasicBlock], - ) { - for succ in term.original_kind.successors() { - if preds(succ).iter().all(|pred| self.done[*pred]) { - debug_assert!(!self.done[succ]); - self.queue.push(succ); - } else { - self.can_redo[succ] = true; - self.dirty_queue.insert(succ); - } - } - } - #[tracing::instrument(name = "Queue::pop", level = "warn", skip(min_by), ret)] - fn pop(&mut self, min_by: impl Fn(&BasicBlock) -> usize) -> Option { - if let Some(bb) = self.queue.pop() { - self.done[bb] = true; - Some(bb) - } else { - if self.dirty_queue.is_empty() { - debug_assert!((0..self.done.len()) - .map(BasicBlock::from_usize) - .all(|bb| self.done[bb] || !self.can_redo[bb])); - return None; - } - let bb = self - .dirty_queue - .iter() - .copied() - .filter(|bb| self.can_redo[*bb]) - .min_by_key(min_by) - .unwrap(); // Can this happen? If so probably a bug - self.can_redo[bb] = false; - self.dirty_queue.remove(&bb); - self.recompute_count[bb] += 1; - // TODO: assert that recompute count is low - assert!(self.recompute_count[bb] < 200); - Some(bb) - } - } -} - -impl<'tcx> MicroBasicBlocks<'tcx> { - pub(crate) fn calculate_repacking<'a>( - &mut self, - start_node: BasicBlock, - initial: FreeState<'tcx>, - preds: impl Fn(BasicBlock) -> &'a [BasicBlock], - rp: PlaceRepacker<'_, 'tcx>, - ) { - debug_assert!(self - .basic_blocks - .indices() - .all(|bb| bb == start_node || !preds(bb).is_empty())); - - self.basic_blocks[start_node].calculate_repacking(initial, rp); - let mut queue = Queue::new(start_node, self.basic_blocks.len()); - queue.add_succs(&self.basic_blocks[start_node].terminator, &preds); - while let Some(can_do) = queue.pop(|bb: &BasicBlock| { - let preds = preds(*bb); - preds.len() - self.get_valid_pred_count(preds) - }) { - // if can_do.as_u32() == 27 { - // tracing::warn!("IJOFD"); - // } - let is_cleanup = self.basic_blocks[can_do].is_cleanup; - let predecessors = self.get_pred_pcs(preds(can_do)); - let initial = if predecessors.len() == 1 { - predecessors[0].state().clone() - } else { - Self::calculate_join(can_do, predecessors, is_cleanup, rp) - }; - // TODO: A better way to do this might be to calculate a pre/post for entire basic blocks; - // start with pre/post of all `None` and walk over the statements collecting all the - // pre/posts, ignoring some (e.g. if we already have `x.f` in our pre then if we ran into - // `x.f.g` we'd ignore it, and if we ran into `x` we'd add `rp.expand(`x`, `x.f`).1`). - // And then calculate the fixpoint from that (rather than having to go through all the - // statements again each time). Then, once we have the state for the start and end of each - // bb, we simply calculate intermediate states along with repacking for all straight-line - // code within each bb. - let changed = self.basic_blocks[can_do].calculate_repacking(initial, rp); - if changed { - queue.add_succs(&self.basic_blocks[can_do].terminator, &preds); - } - } - } - - fn get_pred_pcs( - &mut self, - predecessors: &[BasicBlock], - ) -> Vec<&mut TerminatorPlaceCapabilitySummary<'tcx>> { - let predecessors = self - .basic_blocks - .iter_enumerated_mut() - .filter(|(bb, _)| predecessors.contains(bb)); - predecessors - .filter_map(|(_, bb)| bb.get_end_pcs_mut()) - .collect::>() - } - - fn get_valid_pred_count(&self, predecessors: &[BasicBlock]) -> usize { - predecessors - .iter() - .map(|bb| &self.basic_blocks[*bb]) - .filter(|bb| bb.terminator.repack_join.is_some()) - .count() - } - - #[tracing::instrument(level = "info", skip(rp))] - fn calculate_join( - bb: BasicBlock, - predecessors: Vec<&mut TerminatorPlaceCapabilitySummary<'tcx>>, - is_cleanup: bool, - rp: PlaceRepacker<'_, 'tcx>, - ) -> FreeState<'tcx> { - let mut join = predecessors[0].state().clone(); - for pred in predecessors.iter().skip(1) { - pred.state().join(&mut join, is_cleanup, rp); - if cfg!(debug_assertions) { - join.consistency_check(rp); - } - } - for pred in predecessors { - pred.join(&join, bb, is_cleanup, rp); - } - join - } -} - -impl<'tcx> MicroBasicBlockData<'tcx> { - #[tracing::instrument(level = "info", skip(rp))] - pub(crate) fn calculate_repacking( - &mut self, - mut incoming: FreeState<'tcx>, - rp: PlaceRepacker<'_, 'tcx>, - ) -> bool { - // Check that we haven't already calculated this - let pre_pcs = self - .statements - .first() - .map(|stmt| &stmt.repack_operands) - .unwrap_or_else(|| &self.terminator.repack_operands); - if pre_pcs - .as_ref() - .map(|pcs| pcs.state() == &incoming) - .unwrap_or_default() - { - return false; - } - // Do calculation for statements - for stmt in &mut self.statements { - incoming = stmt.calculate_repacking(incoming, rp); - } - // Do calculation for terminator - self.terminator.calculate_repacking(incoming, rp) - } -} - -impl<'tcx> MicroStatement<'tcx> { - #[tracing::instrument(level = "debug", skip(rp))] - pub(crate) fn calculate_repacking( - &mut self, - incoming: FreeState<'tcx>, - rp: PlaceRepacker<'_, 'tcx>, - ) -> FreeState<'tcx> { - let update = self.get_update(incoming.len()); - let (pcs, mut pre) = incoming.bridge(&update, rp); - if cfg!(debug_assertions) { - pre.consistency_check(rp); - } - self.repack_operands = Some(pcs); - update.update_free(&mut pre); - if cfg!(debug_assertions) { - pre.consistency_check(rp); - } - pre - } -} - -impl<'tcx> MicroTerminator<'tcx> { - #[tracing::instrument(level = "debug", skip(rp))] - pub(crate) fn calculate_repacking( - &mut self, - incoming: FreeState<'tcx>, - rp: PlaceRepacker<'_, 'tcx>, - ) -> bool { - let update = self.get_update(incoming.len()); - let (pcs, mut pre) = incoming.bridge(&update, rp); - if cfg!(debug_assertions) { - pre.consistency_check(rp); - } - self.repack_operands = Some(pcs); - update.update_free(&mut pre); - if cfg!(debug_assertions) { - pre.consistency_check(rp); - } - if let Some(pcs) = self.repack_join.as_mut() { - let changed = pcs.state() != ⪯ - debug_assert!(!(changed && self.previous_rjs.contains(&pre))); - if cfg!(debug_assertions) { - let old = std::mem::replace(pcs.state_mut(), pre); - self.previous_rjs.push(old); - } else { - *pcs.state_mut() = pre; - } - changed - } else { - self.repack_join = Some(TerminatorPlaceCapabilitySummary::empty(pre)); - true - } - } -} diff --git a/micromir/src/repack/repacker.rs b/micromir/src/repack/repacker.rs deleted file mode 100644 index eea39625c9a..00000000000 --- a/micromir/src/repack/repacker.rs +++ /dev/null @@ -1,294 +0,0 @@ -// © 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, - middle::mir::{BasicBlock, Local}, -}; - -use crate::{ - repack::place::PlaceRepacker, FreeState, FreeStateUpdate, PermissionKind, PermissionLocal, - PermissionProjections, Place, PlaceOrdering, RelatedSet, -}; - -#[derive(Clone, Default, Deref, DerefMut)] -pub struct Repacks<'tcx>(Vec>); -impl Debug for Repacks<'_> { - fn fmt(&self, f: &mut Formatter<'_>) -> Result { - self.0.fmt(f) - } -} - -#[derive(Clone)] -pub struct PlaceCapabilitySummary<'tcx> { - state_before: FreeState<'tcx>, - repacks: Repacks<'tcx>, -} - -impl Debug for PlaceCapabilitySummary<'_> { - fn fmt(&self, f: &mut Formatter<'_>) -> Result { - if self.repacks.len() == 0 { - write!(f, "{:?}", &self.state_before) - } else { - f.debug_struct("PCS") - .field("state", &self.state_before) - .field("repacks", &self.repacks) - .finish() - } - } -} - -impl<'tcx> PlaceCapabilitySummary<'tcx> { - pub fn state(&self) -> &FreeState<'tcx> { - &self.state_before - } - pub fn state_mut(&mut self) -> &mut FreeState<'tcx> { - &mut self.state_before - } - pub fn repacks(&self) -> &Repacks<'tcx> { - &self.repacks - } -} - -#[derive(Clone)] -pub struct TerminatorPlaceCapabilitySummary<'tcx> { - state_before: FreeState<'tcx>, - repacks: FxHashMap>, -} - -impl Debug for TerminatorPlaceCapabilitySummary<'_> { - fn fmt(&self, f: &mut Formatter<'_>) -> Result { - if self.repacks.is_empty() { - write!(f, "{:?}", &self.state_before) - } else { - f.debug_struct("PCS") - .field("state", &self.state_before) - .field("repacks", &self.repacks) - .finish() - } - } -} - -impl<'tcx> TerminatorPlaceCapabilitySummary<'tcx> { - pub(crate) fn empty(state_before: FreeState<'tcx>) -> Self { - Self { - state_before, - repacks: FxHashMap::default(), - } - } - pub fn state(&self) -> &FreeState<'tcx> { - &self.state_before - } - pub fn state_mut(&mut self) -> &mut FreeState<'tcx> { - &mut self.state_before - } - pub fn repacks(&self) -> &FxHashMap> { - &self.repacks - } - - #[tracing::instrument(name = "PCS::join", level = "debug", skip(rp))] - pub(crate) fn join( - &mut self, - to: &FreeState<'tcx>, - bb: BasicBlock, - is_cleanup: bool, - rp: PlaceRepacker<'_, 'tcx>, - ) { - let repacks = self.repacks.entry(bb).or_default(); - repacks.clear(); - for (l, to) in to.iter_enumerated() { - let new = - PermissionLocal::bridge(&self.state_before[l], Some(to), repacks, is_cleanup, rp); - debug_assert_eq!(&new, to); - } - } -} - -impl<'tcx> FreeState<'tcx> { - /// The `from` state should never contain any `DontCare` permissions - #[tracing::instrument(level = "debug", skip(rp), ret)] - pub(crate) fn bridge( - self, - update: &FreeStateUpdate<'tcx>, - rp: PlaceRepacker<'_, 'tcx>, - ) -> (PlaceCapabilitySummary<'tcx>, FreeState<'tcx>) { - let mut repacks = Repacks::default(); - let pre = update - .iter_enumerated() - .map(|(l, update)| { - PermissionLocal::bridge( - &self[l], - update.get_pre(&self[l]).as_ref(), - &mut repacks, - false, - rp, - ) - }) - .collect(); - ( - PlaceCapabilitySummary { - state_before: self, - repacks, - }, - pre, - ) - } - - #[tracing::instrument(name = "FreeState::join", level = "info", skip(rp))] - pub(crate) fn join(&self, to: &mut Self, is_cleanup: bool, rp: PlaceRepacker<'_, 'tcx>) { - for (l, to) in to.iter_enumerated_mut() { - PermissionLocal::join(&self[l], to, is_cleanup, rp); - } - } -} - -impl<'tcx> PermissionLocal<'tcx> { - #[tracing::instrument(level = "trace", skip(rp), ret)] - fn bridge( - &self, - to: Option<&PermissionLocal<'tcx>>, - repacks: &mut Repacks<'tcx>, - is_cleanup: bool, - rp: PlaceRepacker<'_, 'tcx>, - ) -> PermissionLocal<'tcx> { - use PermissionLocal::*; - match (self, to) { - (_, None) | (Unallocated, Some(Unallocated)) => self.clone(), - (Allocated(from_places), Some(Allocated(places))) => { - let mut from_places = from_places.clone(); - for (&to_place, &to_kind) in &**places { - from_places.repack_op(to_place, repacks, rp); - let from_kind = *from_places.get(&to_place).unwrap(); - assert!(from_kind >= to_kind, "!({from_kind:?} >= {to_kind:?})"); - if from_kind > to_kind { - from_places.insert(to_place, to_kind); - repacks.push(RepackOp::Weaken(to_place, from_kind, to_kind)); - } - } - Allocated(from_places) - } - (Allocated(a), Some(Unallocated)) => { - let local = a.iter().next().unwrap().0.local; - let root_place = local.into(); - let mut a = a.clone(); - a.repack_op(root_place, repacks, rp); - if a[&root_place] != PermissionKind::Uninit { - assert_eq!(a[&root_place], PermissionKind::Exclusive); - repacks.push(RepackOp::Weaken( - root_place, - a[&root_place], - PermissionKind::Uninit, - )); - } - if is_cleanup { - repacks.push(RepackOp::DeallocForCleanup(local)); - } else { - println!("TODO: figure out why this happens and if it's ok"); - repacks.push(RepackOp::DeallocUnknown(local)); - } - Unallocated - } - a @ (Unallocated, Some(Allocated(..))) => unreachable!("{:?}", a), - } - } - #[tracing::instrument(level = "info", skip(rp))] - fn join(&self, to: &mut Self, _is_cleanup: bool, rp: PlaceRepacker<'_, 'tcx>) { - match (self, &mut *to) { - (PermissionLocal::Unallocated, PermissionLocal::Unallocated) => (), - (PermissionLocal::Allocated(from_places), PermissionLocal::Allocated(places)) => { - from_places.join(places, rp); - } - // Can jump to a `is_cleanup` block with some paths being alloc and other not - (PermissionLocal::Allocated(..), PermissionLocal::Unallocated) => (), - (PermissionLocal::Unallocated, PermissionLocal::Allocated(..)) => { - *to = PermissionLocal::Unallocated - } - }; - } -} - -impl<'tcx> PermissionProjections<'tcx> { - #[tracing::instrument(level = "debug", skip(rp))] - pub(crate) fn repack_op( - &mut self, - to: Place<'tcx>, - repacks: &mut Vec>, - rp: PlaceRepacker<'_, 'tcx>, - ) { - let mut related = self.find_all_related(to, None); - match related.relation { - PlaceOrdering::Prefix => self.unpack_op(related, repacks, rp), - PlaceOrdering::Equal => {} - PlaceOrdering::Suffix => self.pack_op(related, repacks, rp), - PlaceOrdering::Both => { - let cp = rp.common_prefix(related.from[0].0, to); - let minimum = related.minimum; - // Pack - related.to = cp; - related.relation = PlaceOrdering::Both; - self.pack_op(related, repacks, rp); - // Unpack - let related = RelatedSet { - from: vec![(cp, minimum)], - to, - minimum, - relation: PlaceOrdering::Prefix, - }; - self.unpack_op(related, repacks, rp); - } - } - } - pub(crate) fn unpack_op( - &mut self, - related: RelatedSet<'tcx>, - repacks: &mut Vec>, - rp: PlaceRepacker<'_, 'tcx>, - ) { - let unpacks = self.unpack(related.from[0].0, related.to, rp); - repacks.extend( - unpacks - .into_iter() - .map(move |(place, to)| RepackOp::Unpack(place, to, related.minimum)), - ); - } - pub(crate) fn pack_op( - &mut self, - related: RelatedSet<'tcx>, - repacks: &mut Vec>, - rp: PlaceRepacker<'_, 'tcx>, - ) { - let more_than_min = related.from.iter().filter(|(_, k)| *k != related.minimum); - // TODO: This will replace `PermissionKind::Exclusive` with `PermissionKind::Shared` - // the exclusive permission will never be able to be recovered anymore! - for &(p, k) in more_than_min { - let old = self.insert(p, related.minimum); - assert_eq!(old, Some(k)); - repacks.push(RepackOp::Weaken(p, k, related.minimum)); - } - - let packs = self.pack(related.get_from(), related.to, related.minimum, rp); - repacks.extend( - packs - .into_iter() - .map(move |(place, to)| RepackOp::Pack(place, to, related.minimum)), - ); - } -} - -#[derive(Clone, Debug)] -pub enum RepackOp<'tcx> { - Weaken(Place<'tcx>, PermissionKind, PermissionKind), - // TODO: figure out when and why this happens - DeallocUnknown(Local), - DeallocForCleanup(Local), - // First place is packed up, second is guide place to pack up from - Pack(Place<'tcx>, Place<'tcx>, PermissionKind), - // First place is packed up, second is guide place to unpack to - Unpack(Place<'tcx>, Place<'tcx>, PermissionKind), -} diff --git a/micromir/src/repack/triple.rs b/micromir/src/repack/triple.rs deleted file mode 100644 index 048f7079083..00000000000 --- a/micromir/src/repack/triple.rs +++ /dev/null @@ -1,124 +0,0 @@ -// © 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::RETURN_PLACE; - -use crate::{ - FreeStateUpdate, MicroFullOperand, MicroStatement, MicroStatementKind, MicroTerminator, - MicroTerminatorKind, Operands, PermissionKind, -}; - -pub(crate) trait ModifiesFreeState<'tcx> { - fn get_update(&self, locals: usize) -> FreeStateUpdate<'tcx>; -} - -impl<'tcx> ModifiesFreeState<'tcx> for Operands<'tcx> { - #[tracing::instrument(level = "trace")] - fn get_update(&self, locals: usize) -> FreeStateUpdate<'tcx> { - let mut update = FreeStateUpdate::default(locals); - for operand in &**self { - match *operand { - MicroFullOperand::Copy(place) => { - update[place.local].requires_alloc( - place, - &[PermissionKind::Exclusive, PermissionKind::Shared], - ); - } - MicroFullOperand::Move(place) => { - update[place.local].requires_alloc_one(place, PermissionKind::Exclusive); - update[place.local].ensures_alloc(place, PermissionKind::Uninit); - } - MicroFullOperand::Constant(..) => (), - } - } - update - } -} - -impl<'tcx> ModifiesFreeState<'tcx> for MicroStatement<'tcx> { - #[tracing::instrument(level = "trace")] - fn get_update(&self, locals: usize) -> FreeStateUpdate<'tcx> { - let mut update = self.operands.get_update(locals); - match &self.kind { - &MicroStatementKind::Assign(box (place, _)) => { - if let Some(pre) = update[place.local].get_pre_for(place) { - assert_eq!(pre.len(), 2); - assert!(pre.contains(&PermissionKind::Exclusive)); - assert!(pre.contains(&PermissionKind::Shared)); - } else { - update[place.local].requires_alloc_one(place, PermissionKind::Uninit); - } - update[place.local].ensures_alloc(place, PermissionKind::Exclusive); - } - MicroStatementKind::FakeRead(box (_, place)) => update[place.local] - .requires_alloc(*place, &[PermissionKind::Exclusive, PermissionKind::Shared]), - MicroStatementKind::SetDiscriminant { box place, .. } => { - update[place.local].requires_alloc_one(*place, PermissionKind::Exclusive) - } - MicroStatementKind::Deinit(box place) => { - // TODO: Maybe OK to also allow `Uninit` here? - update[place.local].requires_alloc_one(*place, PermissionKind::Exclusive); - update[place.local].ensures_alloc(*place, PermissionKind::Uninit); - } - &MicroStatementKind::StorageLive(local) => { - update[local].requires_unalloc(); - update[local].ensures_alloc(local.into(), PermissionKind::Uninit); - } - &MicroStatementKind::StorageDead(local) => { - update[local].requires_unalloc_or_uninit(local); - update[local].ensures_unalloc(); - } - MicroStatementKind::Retag(_, box place) => { - update[place.local].requires_alloc_one(*place, PermissionKind::Exclusive) - } - MicroStatementKind::AscribeUserType(..) - | MicroStatementKind::Coverage(..) - | MicroStatementKind::Intrinsic(..) - | MicroStatementKind::ConstEvalCounter - | MicroStatementKind::Nop => (), - }; - update - } -} - -impl<'tcx> ModifiesFreeState<'tcx> for MicroTerminator<'tcx> { - #[tracing::instrument(level = "trace")] - fn get_update(&self, locals: usize) -> FreeStateUpdate<'tcx> { - let mut update = self.operands.get_update(locals); - match &self.kind { - MicroTerminatorKind::Goto { .. } - | MicroTerminatorKind::SwitchInt { .. } - | MicroTerminatorKind::Resume - | MicroTerminatorKind::Abort - | MicroTerminatorKind::Unreachable - | MicroTerminatorKind::Assert { .. } - | MicroTerminatorKind::GeneratorDrop - | MicroTerminatorKind::FalseEdge { .. } - | MicroTerminatorKind::FalseUnwind { .. } => (), - MicroTerminatorKind::Return => update[RETURN_PLACE] - .requires_alloc_one(RETURN_PLACE.into(), PermissionKind::Exclusive), - MicroTerminatorKind::Drop { place, .. } => { - update[place.local] - .requires_alloc(*place, &[PermissionKind::Exclusive, PermissionKind::Uninit]); - update[place.local].ensures_alloc(*place, PermissionKind::Uninit); - } - MicroTerminatorKind::DropAndReplace { place, .. } => { - update[place.local] - .requires_alloc(*place, &[PermissionKind::Exclusive, PermissionKind::Uninit]); - update[place.local].ensures_alloc(*place, PermissionKind::Exclusive); - } - MicroTerminatorKind::Call { destination, .. } => { - update[destination.local].requires_alloc_one(*destination, PermissionKind::Uninit); - update[destination.local].ensures_alloc(*destination, PermissionKind::Exclusive); - } - MicroTerminatorKind::Yield { resume_arg, .. } => { - update[resume_arg.local].requires_alloc_one(*resume_arg, PermissionKind::Uninit); - update[resume_arg.local].ensures_alloc(*resume_arg, PermissionKind::Exclusive); - } - }; - update - } -} diff --git a/micromir/Cargo.toml b/mir-state-analysis/Cargo.toml similarity index 83% rename from micromir/Cargo.toml rename to mir-state-analysis/Cargo.toml index 847715dface..958fe750062 100644 --- a/micromir/Cargo.toml +++ b/mir-state-analysis/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "micromir" +name = "mir-state-analysis" version = "0.1.0" authors = ["Prusti Devs "] edition = "2021" @@ -9,9 +9,6 @@ derive_more = "0.99" tracing = { path = "../tracing" } prusti-rustc-interface = { path = "../prusti-rustc-interface" } -# TODO: remove this dep -prusti-interface = { path = "../prusti-interface" } - [dev-dependencies] reqwest = { version = "^0.11", features = ["blocking"] } serde = "^1.0" 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..7e6e4cfa485 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/check/checker.rs @@ -0,0 +1,159 @@ +// © 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, + dataflow::Results, + middle::mir::{visit::Visitor, Location}, +}; + +use crate::{ + engine::FreePlaceCapabilitySummary, join_semi_lattice::RepackingJoinSemiLattice, + utils::PlaceRepacker, CapabilityKind, CapabilityLocal, CapabilitySummary, PlaceOrdering, + RepackOp, +}; + +use super::consistency::CapabilityConistency; + +pub(crate) fn check<'tcx>(results: Results<'tcx, FreePlaceCapabilitySummary<'_, 'tcx>>) { + let rp = results.analysis.0; + let body = rp.body(); + let mut cursor = results.into_results_cursor(body); + for (block, data) in body.basic_blocks.iter_enumerated() { + cursor.seek_to_block_start(block); + let mut fpcs = cursor.get().clone(); + // Consistency + fpcs.summary.consistency_check(rp); + for (statement_index, stmt) in data.statements.iter().enumerate() { + let loc = Location { + block, + statement_index, + }; + cursor.seek_after_primary_effect(loc); + let fpcs_after = cursor.get(); + // Repacks + for op in &fpcs_after.repackings { + op.update_free(&mut fpcs.summary, false, rp); + } + // Consistency + fpcs.summary.consistency_check(rp); + // Statement + assert!(fpcs.repackings.is_empty()); + 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(), + }; + cursor.seek_after_primary_effect(loc); + let fpcs_after = cursor.get(); + // Repacks + for op in &fpcs_after.repackings { + op.update_free(&mut fpcs.summary, false, rp); + } + // Consistency + fpcs.summary.consistency_check(rp); + // Statement + assert!(fpcs.repackings.is_empty()); + fpcs.visit_terminator(data.terminator(), loc); + assert!(fpcs.repackings.is_empty()); + // Consistency + fpcs.summary.consistency_check(rp); + assert_eq!(&fpcs, fpcs_after); + + for succ in data.terminator().successors() { + // Get repacks + let to = cursor.results().entry_set_for_block(succ); + let repacks = fpcs.summary.bridge(&to.summary, rp); + + // Repacks + let mut from = fpcs.clone(); + for op in repacks { + op.update_free(&mut from.summary, body.basic_blocks[succ].is_cleanup, rp); + } + assert_eq!(&from, to); + } + } +} + +impl<'tcx> RepackOp<'tcx> { + #[tracing::instrument(level = "debug", skip(rp))] + fn update_free( + &self, + state: &mut CapabilitySummary<'tcx>, + can_dealloc: bool, + rp: PlaceRepacker<'_, 'tcx>, + ) { + match self { + 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::DeallocForCleanup(local) => { + assert!(can_dealloc); + 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::DeallocUnknown(local) => { + // assert!(!can_dealloc); + // let curr_state = state[local].get_allocated_mut(); + // assert_eq!(curr_state.len(), 1); + // assert_eq!(curr_state[&local.into()], CapabilityKind::Write); + // state[local] = CapabilityLocal::Unallocated; + // } + RepackOp::Pack(place, guide, kind) => { + assert_eq!( + place.partial_cmp(*guide), + Some(PlaceOrdering::Prefix), + "{self:?}" + ); + let curr_state = state[place.local].get_allocated_mut(); + let mut removed = curr_state + .drain() + .filter(|(p, _)| place.related_to(*p)) + .collect::>(); + let (p, others) = place.expand_one_level(*guide, rp); + assert!(others + .into_iter() + .chain(std::iter::once(p)) + .all(|p| removed.remove(&p).unwrap() == *kind)); + assert!(removed.is_empty(), "{self:?}, {removed:?}"); + + let old = curr_state.insert(*place, *kind); + assert_eq!(old, None); + } + RepackOp::Unpack(place, guide, kind) => { + assert_eq!( + place.partial_cmp(*guide), + Some(PlaceOrdering::Prefix), + "{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))); + } + } + } +} 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..b5a77a5c693 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/check/consistency.rs @@ -0,0 +1,45 @@ +// © 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::{utils::PlaceRepacker, CapabilityLocal, CapabilityProjections, Place, Summary}; + +pub trait CapabilityConistency<'tcx> { + fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>); +} + +impl<'tcx, T: CapabilityConistency<'tcx>> CapabilityConistency<'tcx> for Summary { + fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>) { + for p in self.iter() { + p.consistency_check(repacker) + } + } +} + +impl<'tcx> CapabilityConistency<'tcx> for CapabilityLocal<'tcx> { + fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>) { + match self { + CapabilityLocal::Unallocated => {} + CapabilityLocal::Allocated(cp) => cp.consistency_check(repacker), + } + } +} + +impl<'tcx> CapabilityConistency<'tcx> for CapabilityProjections<'tcx> { + fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>) { + // All keys unrelated to each other + let keys = self.keys().copied().collect::>(); + for (i, p1) in keys.iter().enumerate() { + for p2 in keys[i + 1..].iter() { + assert!(!p1.related_to(*p2), "{p1:?} {p2:?}",); + } + } + // 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/micromir/src/free_pcs/mod.rs b/mir-state-analysis/src/free_pcs/check/mod.rs similarity index 79% rename from micromir/src/free_pcs/mod.rs rename to mir-state-analysis/src/free_pcs/check/mod.rs index 4d469804e68..6a308a2b833 100644 --- a/micromir/src/free_pcs/mod.rs +++ b/mir-state-analysis/src/free_pcs/check/mod.rs @@ -4,6 +4,7 @@ // 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 permission; +mod checker; +mod consistency; -pub use permission::*; +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..77230e0a37c --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/engine.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/. + +use prusti_rustc_interface::{ + dataflow::{Analysis, AnalysisDomain, CallReturnPlaces}, + index::vec::Idx, + middle::{ + mir::{ + visit::Visitor, BasicBlock, Body, Local, Location, Statement, Terminator, RETURN_PLACE, + }, + ty::TyCtxt, + }, +}; + +use crate::{utils::PlaceRepacker, CapabilityKind, CapabilityLocal, Fpcs}; + +pub(crate) struct FreePlaceCapabilitySummary<'a, 'tcx>(pub(crate) PlaceRepacker<'a, 'tcx>); +impl<'a, 'tcx> FreePlaceCapabilitySummary<'a, 'tcx> { + pub(crate) fn new(tcx: TyCtxt<'tcx>, body: &'a Body<'tcx>) -> Self { + let repacker = PlaceRepacker::new(body, tcx); + FreePlaceCapabilitySummary(repacker) + } +} + +impl<'a, 'tcx> AnalysisDomain<'tcx> for FreePlaceCapabilitySummary<'a, 'tcx> { + type Domain = Fpcs<'a, 'tcx>; + const NAME: &'static str = "free_pcs"; + + fn bottom_value(&self, _body: &Body<'tcx>) -> Self::Domain { + Fpcs::new(self.0) + } + + fn initialize_start_block(&self, body: &Body<'tcx>, state: &mut Self::Domain) { + 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() { + if local == return_local { + let old = cap + .get_allocated_mut() + .insert(local.into(), CapabilityKind::Write); + assert!(old.is_some()); + } else if local <= last_arg { + let old = cap + .get_allocated_mut() + .insert(local.into(), CapabilityKind::Exclusive); + assert!(old.is_some()); + } 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 + }; + let old = cap.get_allocated_mut().insert(local.into(), al_cap); + assert!(old.is_some()); + } else { + *cap = CapabilityLocal::Unallocated; + } + } + } +} + +impl<'a, 'tcx> Analysis<'tcx> for FreePlaceCapabilitySummary<'a, 'tcx> { + fn apply_statement_effect( + &self, + state: &mut Self::Domain, + statement: &Statement<'tcx>, + location: Location, + ) { + state.repackings.clear(); + state.visit_statement(statement, location); + } + + fn apply_terminator_effect( + &self, + state: &mut Self::Domain, + terminator: &Terminator<'tcx>, + location: Location, + ) { + state.repackings.clear(); + state.visit_terminator(terminator, location); + } + + fn apply_call_return_effect( + &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..952b5236243 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/fpcs.rs @@ -0,0 +1,148 @@ +// © 2023, ETH Zurich +// +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. + +use std::fmt::{Debug, Formatter, Result}; + +use derive_more::{Deref, DerefMut}; +use prusti_rustc_interface::{ + dataflow::fmt::DebugWithContext, index::vec::IndexVec, middle::mir::Local, +}; + +use crate::{ + engine::FreePlaceCapabilitySummary, utils::PlaceRepacker, CapabilityKind, CapabilityLocal, + CapabilityProjections, RepackOp, +}; + +#[derive(Clone)] +pub struct Fpcs<'a, 'tcx> { + pub(crate) repacker: PlaceRepacker<'a, 'tcx>, + pub summary: CapabilitySummary<'tcx>, + pub repackings: Vec>, +} +impl<'a, 'tcx> Fpcs<'a, 'tcx> { + pub(crate) fn new(repacker: PlaceRepacker<'a, 'tcx>) -> Self { + let summary = CapabilitySummary::bottom_value(repacker.local_count()); + Self { + repacker, + summary, + repackings: Vec::new(), + } + } +} + +impl PartialEq for Fpcs<'_, '_> { + fn eq(&self, other: &Self) -> bool { + self.summary == other.summary + } +} +impl Eq for Fpcs<'_, '_> {} + +impl<'a, 'tcx> Debug for Fpcs<'a, 'tcx> { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + self.summary.fmt(f) + } +} +impl<'a, 'tcx> DebugWithContext> for Fpcs<'a, 'tcx> { + fn fmt_diff_with( + &self, + old: &Self, + _ctxt: &FreePlaceCapabilitySummary<'a, 'tcx>, + f: &mut Formatter<'_>, + ) -> Result { + assert_eq!(self.summary.len(), old.summary.len()); + 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 let Some(d) = nk - ok { + new_set.insert(p, d); + } + } + None => { + new_set.insert(p, nk); + } + } + } + for (&p, &ok) in old.iter() { + match new.get(&p) { + Some(&nk) => { + if let Some(d) = ok - nk { + old_set.insert(p, d); + } + } + None => { + 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>; + +impl<'tcx> CapabilitySummary<'tcx> { + pub fn bottom_value(local_count: usize) -> Self { + Self(IndexVec::from_fn_n( + |local: Local| CapabilityLocal::new(local, CapabilityKind::Exclusive), + local_count, + )) + } +} 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..dff9066d09c --- /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::{ + utils::PlaceRepacker, CapabilityKind, CapabilityLocal, CapabilityProjections, + CapabilitySummary, Fpcs, PlaceOrdering, RepackOp, +}; + +impl JoinSemiLattice for Fpcs<'_, '_> { + fn join(&mut self, other: &Self) -> bool { + self.summary.join(&other.summary, self.repacker) + } +} + +pub trait RepackingJoinSemiLattice<'tcx> { + fn join(&mut self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> bool; + fn bridge(&self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec>; +} +impl<'tcx> RepackingJoinSemiLattice<'tcx> for CapabilitySummary<'tcx> { + fn join(&mut self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> bool { + let mut changed = false; + for (l, to) in self.iter_enumerated_mut() { + let local_changed = to.join(&other[l], repacker); + changed = changed || local_changed; + } + changed + } + fn bridge(&self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec> { + let mut repacks = Vec::new(); + for (l, to) in self.iter_enumerated() { + let local_repacks = to.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(to_places), CapabilityLocal::Allocated(from_places)) => { + to_places.bridge(from_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.pack_ops( + cps.keys().copied().collect(), + local.into(), + CapabilityKind::Write, + repacker, + ); + repacks.extend(packs); + }; + repacks.push(RepackOp::DeallocForCleanup(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); + match related.relation { + PlaceOrdering::Prefix => { + changed = true; + + let from = related.from[0].0; + let joinable_place = from.joinable_to(place, repacker); + if joinable_place != from { + self.unpack(from, joinable_place, repacker); + } + // Downgrade the permission if needed + let new_min = kind.minimum(related.minimum).unwrap(); + if new_min != related.minimum { + self.insert(joinable_place, new_min); + } + } + PlaceOrdering::Equal => { + // Downgrade the permission if needed + let new_min = kind.minimum(related.minimum).unwrap(); + if new_min != related.minimum { + changed = true; + self.insert(place, new_min); + } + } + PlaceOrdering::Suffix => { + // Downgrade the permission if needed + for &(p, k) in &related.from { + let new_min = kind.minimum(k).unwrap(); + if new_min != k { + changed = true; + self.insert(p, new_min); + } + } + } + PlaceOrdering::Both => { + changed = true; + + // Downgrade the permission if needed + let min = kind.minimum(related.minimum).unwrap(); + for &(p, k) in &related.from { + let new_min = min.minimum(k).unwrap(); + if new_min != k { + self.insert(p, new_min); + } + } + let cp = related.from[0].0.common_prefix(place, repacker); + self.pack(related.get_from(), cp, min, repacker); + } + } + } + changed + } + fn bridge(&self, other: &Self, repacker: PlaceRepacker<'_, 'tcx>) -> Vec> { + // TODO: remove need for clone + let mut cps = self.clone(); + + let mut repacks = Vec::new(); + for (&place, &kind) in &**other { + let related = cps.find_all_related(place, None); + match related.relation { + PlaceOrdering::Prefix => { + let from = related.from[0].0; + // TODO: remove need for clone + let unpacks = cps.unpack_ops(from, place, related.minimum, repacker); + repacks.extend(unpacks); + + // Downgrade the permission if needed + let new_min = kind.minimum(related.minimum).unwrap(); + if new_min != related.minimum { + cps.insert(place, new_min); + repacks.push(RepackOp::Weaken(place, related.minimum, new_min)); + } + } + PlaceOrdering::Equal => { + // Downgrade the permission if needed + let new_min = kind.minimum(related.minimum).unwrap(); + if new_min != related.minimum { + cps.insert(place, new_min); + repacks.push(RepackOp::Weaken(place, related.minimum, new_min)); + } + } + PlaceOrdering::Suffix => { + // Downgrade the permission if needed + for &(p, k) in &related.from { + let new_min = kind.minimum(k).unwrap(); + if new_min != k { + cps.insert(p, new_min); + repacks.push(RepackOp::Weaken(p, k, new_min)); + } + } + let packs = + cps.pack_ops(related.get_from(), related.to, related.minimum, repacker); + repacks.extend(packs); + } + PlaceOrdering::Both => unreachable!(), + } + } + 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..732be1d3909 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/local.rs @@ -0,0 +1,163 @@ +// © 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::{utils::PlaceRepacker, CapabilityKind, Place, PlaceOrdering, RelatedSet}; + +#[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<'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 + } + + /// 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", skip(self))] + 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) { + minimum = if let Some(min) = minimum { + Some(min.minimum(cap).unwrap()) + } else { + Some(cap) + }; + if let Some(expected) = expected { + assert_eq!(ord, expected); + } 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 unpack( + &mut self, + from: Place<'tcx>, + to: Place<'tcx>, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> Vec<(Place<'tcx>, Place<'tcx>)> { + debug_assert!(!self.contains_key(&to)); + let (expanded, others) = from.expand(to, repacker); + let perm = self.remove(&from).unwrap(); + self.extend(others.into_iter().map(|p| (p, perm))); + self.insert(to, perm); + expanded + } + + // 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 pack( + &mut self, + mut from: FxHashSet>, + to: Place<'tcx>, + perm: CapabilityKind, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> Vec<(Place<'tcx>, Place<'tcx>)> { + debug_assert!(!self.contains_key(&to), "{to:?} already exists in {self:?}"); + for place in &from { + let p = self.remove(place).unwrap(); + assert_eq!(p, perm, "Cannot pack {place:?} with {p:?} into {to:?}"); + } + let collapsed = to.collapse(&mut from, repacker); + assert!(from.is_empty()); + self.insert(to, perm); + collapsed + } +} diff --git a/micromir/src/defs/mod.rs b/mir-state-analysis/src/free_pcs/impl/mod.rs similarity index 56% rename from micromir/src/defs/mod.rs rename to mir-state-analysis/src/free_pcs/impl/mod.rs index 2cbc0dd6806..3ee083a3dc9 100644 --- a/micromir/src/defs/mod.rs +++ b/mir-state-analysis/src/free_pcs/impl/mod.rs @@ -4,14 +4,14 @@ // 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 operand; -mod rvalue; -mod terminator; -mod statement; -mod body; +mod fpcs; +mod local; +mod place; +pub(crate) mod engine; +pub(crate) mod join_semi_lattice; +mod triple; +mod update; -pub use body::*; -pub use operand::*; -pub use rvalue::*; -pub use statement::*; -pub use terminator::*; +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..edd9ab1a657 --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/place.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/. + +use std::{ + cmp::Ordering, + fmt::{Debug, Formatter, Result}, + ops::Sub, +}; + +use prusti_rustc_interface::data_structures::fx::FxHashSet; + +use crate::{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() + } +} + +#[derive(Copy, Clone, PartialEq, Eq, Hash)] +pub enum CapabilityKind { + Read, + Write, + Exclusive, +} +impl Debug for CapabilityKind { + fn fmt(&self, f: &mut Formatter<'_>) -> Result { + match self { + CapabilityKind::Read => write!(f, "R"), + CapabilityKind::Write => write!(f, "W"), + CapabilityKind::Exclusive => write!(f, "E"), + } + } +} + +impl PartialOrd for CapabilityKind { + fn partial_cmp(&self, other: &Self) -> Option { + if *self == *other { + return Some(Ordering::Equal); + } + match (self, other) { + (CapabilityKind::Read, CapabilityKind::Exclusive) + | (CapabilityKind::Write, CapabilityKind::Exclusive) => Some(Ordering::Less), + (CapabilityKind::Exclusive, CapabilityKind::Read) + | (CapabilityKind::Exclusive, CapabilityKind::Write) => Some(Ordering::Greater), + _ => None, + } + } +} + +impl Sub for CapabilityKind { + type Output = Option; + fn sub(self, other: Self) -> Self::Output { + match (self, other) { + (CapabilityKind::Exclusive, CapabilityKind::Read) => Some(CapabilityKind::Write), + (CapabilityKind::Exclusive, CapabilityKind::Write) => Some(CapabilityKind::Read), + _ => None, + } + } +} + +impl CapabilityKind { + pub fn is_read(self) -> bool { + matches!(self, CapabilityKind::Read) + } + pub fn is_exclusive(self) -> bool { + matches!(self, CapabilityKind::Exclusive) + } + pub fn is_write(self) -> bool { + matches!(self, CapabilityKind::Write) + } + pub fn minimum(self, other: Self) -> Option { + match self.partial_cmp(&other)? { + Ordering::Greater => Some(other), + _ => Some(self), + } + } +} diff --git a/mir-state-analysis/src/free_pcs/impl/triple.rs b/mir-state-analysis/src/free_pcs/impl/triple.rs new file mode 100644 index 00000000000..f9e34fd511f --- /dev/null +++ b/mir-state-analysis/src/free_pcs/impl/triple.rs @@ -0,0 +1,148 @@ +// © 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::Fpcs; + +impl<'tcx> Visitor<'tcx> for Fpcs<'_, 'tcx> { + fn visit_operand(&mut self, operand: &Operand<'tcx>, location: Location) { + self.super_operand(operand, location); + match *operand { + Operand::Copy(place) => { + self.requires_read(place); + } + Operand::Move(place) => { + self.requires_exclusive(place); + self.ensures_write(place); + } + Operand::Constant(..) => (), + } + } + + fn visit_statement(&mut self, statement: &Statement<'tcx>, location: Location) { + self.super_statement(statement, location); + use StatementKind::*; + match &statement.kind { + &Assign(box (place, _)) => { + self.requires_write(place); + self.ensures_exclusive(place); + } + &FakeRead(box (_, place)) => self.requires_read(place), + &SetDiscriminant { box place, .. } => self.requires_exclusive(place), + &Deinit(box place) => { + // TODO: Maybe OK to also allow `Write` here? + self.requires_exclusive(place); + self.ensures_write(place); + } + &StorageLive(local) => { + self.requires_unalloc(local); + self.ensures_allocates(local); + } + &StorageDead(local) => { + self.requires_unalloc_or_uninit(local); + self.ensures_unalloc(local); + } + &Retag(_, box place) => self.requires_exclusive(place), + AscribeUserType(..) | Coverage(..) | Intrinsic(..) | ConstEvalCounter | Nop => (), + }; + } + + fn visit_terminator(&mut self, terminator: &Terminator<'tcx>, location: Location) { + self.super_terminator(terminator, location); + use TerminatorKind::*; + match &terminator.kind { + Goto { .. } + | SwitchInt { .. } + | Resume + | Abort + | 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 always_live.contains(local) { + self.requires_write(local); + } else { + self.requires_unalloc(local); + } + } + self.requires_exclusive(RETURN_PLACE); + } + &Drop { place, .. } => { + self.requires_write(place); + self.ensures_write(place); + } + &DropAndReplace { place, .. } => { + self.requires_write(place); + self.ensures_exclusive(place); + } + &Call { destination, .. } => { + self.requires_write(destination); + self.ensures_exclusive(destination); + } + &Yield { resume_arg, .. } => { + self.requires_write(resume_arg); + self.ensures_exclusive(resume_arg); + } + InlineAsm { .. } => todo!("{terminator:?}"), + }; + } + + fn visit_rvalue(&mut self, rvalue: &Rvalue<'tcx>, location: Location) { + self.super_rvalue(rvalue, location); + use Rvalue::*; + match rvalue { + Use(_) + | Repeat(_, _) + | ThreadLocalRef(_) + | Cast(_, _, _) + | BinaryOp(_, _) + | CheckedBinaryOp(_, _) + | NullaryOp(_, _) + | UnaryOp(_, _) + | Aggregate(_, _) => {} + + &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::Unique => { + self.requires_exclusive(place); + // self.ensures_blocked_exclusive(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), + ShallowInitBox(_, _) => todo!(), + &CopyForDeref(place) => self.requires_read(place), + } + } +} 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..6c7f38d7fa3 --- /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::{data_structures::fx::FxHashSet, middle::mir::Local}; + +use crate::{ + utils::PlaceRepacker, CapabilityKind, CapabilityLocal, CapabilityProjections, Fpcs, Place, + PlaceOrdering, RelatedSet, RepackOp, +}; + +impl<'tcx> Fpcs<'_, 'tcx> { + pub(crate) fn requires_unalloc(&mut self, local: Local) { + assert!( + self.summary[local].is_unallocated(), + "local: {local:?}, fpcs: {self:?}\n" + ); + } + pub(crate) fn requires_unalloc_or_uninit(&mut self, local: Local) { + if !self.summary[local].is_unallocated() { + self.requires_write(local) + } + } + pub(crate) fn requires_read(&mut self, place: impl 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`! + pub(crate) fn requires_write(&mut self, place: impl Into>) { + self.requires(place, CapabilityKind::Write) + } + pub(crate) fn requires_exclusive(&mut self, place: impl Into>) { + self.requires(place, CapabilityKind::Exclusive) + } + fn requires(&mut self, place: impl Into>, cap: CapabilityKind) { + let place = place.into(); + let cp: &mut CapabilityProjections = self.summary[place.local].get_allocated_mut(); + let ops = cp.repack(place, self.repacker); + self.repackings.extend(ops); + let kind = (*cp)[&place]; + assert!(kind >= cap); + } + + pub(crate) fn ensures_unalloc(&mut self, local: Local) { + self.summary[local] = CapabilityLocal::Unallocated; + } + pub(crate) fn ensures_allocates(&mut self, local: Local) { + assert_eq!(self.summary[local], CapabilityLocal::Unallocated); + self.summary[local] = CapabilityLocal::Allocated(CapabilityProjections::new_uninit(local)); + } + fn ensures_alloc(&mut self, place: impl Into>, cap: CapabilityKind) { + let place = place.into(); + let cp: &mut CapabilityProjections = self.summary[place.local].get_allocated_mut(); + let old = cp.insert(place, cap); + assert!(old.is_some()); + } + pub(crate) fn ensures_exclusive(&mut self, place: impl Into>) { + self.ensures_alloc(place, CapabilityKind::Exclusive) + } + pub(crate) fn ensures_write(&mut self, place: impl Into>) { + self.ensures_alloc(place, CapabilityKind::Write) + } +} + +impl<'tcx> CapabilityProjections<'tcx> { + 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 + .unpack_ops(related.from[0].0, related.to, related.minimum, repacker) + .collect(), + PlaceOrdering::Equal => Vec::new(), + PlaceOrdering::Suffix => self + .pack_ops(related.get_from(), related.to, related.minimum, repacker) + .collect(), + PlaceOrdering::Both => { + let cp = related.from[0].0.common_prefix(to, repacker); + // Pack + let mut ops = self.weaken(&related); + let packs = self.pack_ops(related.get_from(), cp, related.minimum, repacker); + ops.extend(packs); + // Unpack + let unpacks = self.unpack_ops(cp, related.to, related.minimum, repacker); + ops.extend(unpacks); + ops + } + } + } + pub(crate) fn unpack_ops( + &mut self, + from: Place<'tcx>, + to: Place<'tcx>, + kind: CapabilityKind, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> impl Iterator> { + self.unpack(from, to, repacker) + .into_iter() + .map(move |(f, t)| RepackOp::Unpack(f, t, kind)) + } + pub(crate) fn pack_ops( + &mut self, + from: FxHashSet>, + to: Place<'tcx>, + perm: CapabilityKind, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> impl Iterator> { + self.pack(from, to, perm, repacker) + .into_iter() + .map(move |(f, t)| RepackOp::Pack(f, t, perm)) + } + + pub(crate) fn weaken(&mut self, related: &RelatedSet<'tcx>) -> Vec> { + let mut ops = Vec::new(); + let more_than_min = related.from.iter().filter(|(_, k)| *k != related.minimum); + // TODO: This will replace `PermissionKind::Exclusive` with `PermissionKind::Shared` + // the exclusive permission will never be able to be recovered anymore! + for &(p, k) in more_than_min { + let old = self.insert(p, related.minimum); + assert_eq!(old, Some(k)); + ops.push(RepackOp::Weaken(p, k, related.minimum)); + } + ops + } +} diff --git a/micromir/src/repack/mod.rs b/mir-state-analysis/src/free_pcs/mod.rs similarity index 63% rename from micromir/src/repack/mod.rs rename to mir-state-analysis/src/free_pcs/mod.rs index dd474de9c75..fe388adbc52 100644 --- a/micromir/src/repack/mod.rs +++ b/mir-state-analysis/src/free_pcs/mod.rs @@ -4,11 +4,10 @@ // 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 repacker; -mod calculate; -pub(crate) mod triple; -mod place; +mod check; +mod r#impl; +mod results; -pub use calculate::*; -pub(crate) use place::*; -pub use repacker::*; +pub(crate) use check::*; +pub use r#impl::*; +pub use results::*; diff --git a/micromir/src/check/mod.rs b/mir-state-analysis/src/free_pcs/results/mod.rs similarity index 87% rename from micromir/src/check/mod.rs rename to mir-state-analysis/src/free_pcs/results/mod.rs index a5f8a9cc024..7d5043c22da 100644 --- a/micromir/src/check/mod.rs +++ b/mir-state-analysis/src/free_pcs/results/mod.rs @@ -4,4 +4,6 @@ // 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 checker; +mod repacks; + +pub use repacks::*; diff --git a/mir-state-analysis/src/free_pcs/results/repacking.rs b/mir-state-analysis/src/free_pcs/results/repacking.rs new file mode 100644 index 00000000000..e69de29bb2d 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..9cb61b8027c --- /dev/null +++ b/mir-state-analysis/src/free_pcs/results/repacks.rs @@ -0,0 +1,21 @@ +// © 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::{CapabilityKind, Place}; + +#[derive(Clone, Debug, Eq, PartialEq)] +pub enum RepackOp<'tcx> { + Weaken(Place<'tcx>, CapabilityKind, CapabilityKind), + // TODO: figure out when and why this happens + // DeallocUnknown(Local), + DeallocForCleanup(Local), + // First place is packed up, second is guide place to pack up from + Pack(Place<'tcx>, Place<'tcx>, CapabilityKind), + // First place is packed up, second is guide place to unpack to + Unpack(Place<'tcx>, Place<'tcx>, CapabilityKind), +} diff --git a/mir-state-analysis/src/lib.rs b/mir-state-analysis/src/lib.rs new file mode 100644 index 00000000000..b03090e6103 --- /dev/null +++ b/mir-state-analysis/src/lib.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/. + +#![feature(rustc_private)] +#![feature(box_patterns)] + +mod free_pcs; +mod utils; + +pub use free_pcs::*; +pub use utils::place::*; + +use prusti_rustc_interface::{ + dataflow::Analysis, + middle::{mir::Body, ty::TyCtxt}, +}; + +pub fn test_free_pcs<'tcx>(mir: &Body<'tcx>, tcx: TyCtxt<'tcx>) { + let fpcs = free_pcs::engine::FreePlaceCapabilitySummary::new(tcx, mir); + let analysis = fpcs + .into_engine(tcx, mir) + .pass_name("free_pcs") + .iterate_to_fixpoint(); + free_pcs::check(analysis); +} diff --git a/micromir/src/utils/mod.rs b/mir-state-analysis/src/utils/mod.rs similarity index 81% rename from micromir/src/utils/mod.rs rename to mir-state-analysis/src/utils/mod.rs index 6f5a94a7085..e0bd10f8b91 100644 --- a/micromir/src/utils/mod.rs +++ b/mir-state-analysis/src/utils/mod.rs @@ -5,3 +5,6 @@ // file, You can obtain one at http://mozilla.org/MPL/2.0/. pub mod place; +pub(crate) mod repacker; + +pub(crate) use repacker::*; diff --git a/micromir/src/utils/place.rs b/mir-state-analysis/src/utils/place.rs similarity index 63% rename from micromir/src/utils/place.rs rename to mir-state-analysis/src/utils/place.rs index 672c7e5d5cd..139fa466c6c 100644 --- a/micromir/src/utils/place.rs +++ b/mir-state-analysis/src/utils/place.rs @@ -18,6 +18,38 @@ use prusti_rustc_interface::middle::{ ty::List, }; +// #[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()) +// } +// } + fn elem_eq<'tcx>(to_cmp: (PlaceElem<'tcx>, PlaceElem<'tcx>)) -> bool { use ProjectionElem::*; match to_cmp { @@ -144,8 +176,90 @@ impl<'tcx> Place<'tcx> { } impl Debug for Place<'_> { - fn fmt(&self, f: &mut Formatter) -> Result { - self.0.fmt(f) + 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, " as {})", ty)?; + } + ProjectionElem::Downcast(Some(name), _index) => { + write!(fmt, " as {})", name)?; + } + ProjectionElem::Downcast(None, index) => { + write!(fmt, " as 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, "[{:?} of {:?}]", offset, min_length)?; + } + ProjectionElem::ConstantIndex { + offset, + min_length, + from_end: true, + } => { + write!(fmt, "[-{:?} of {:?}]", offset, min_length)?; + } + ProjectionElem::Subslice { + from, + to, + from_end: true, + } if to == 0 => { + write!(fmt, "[{:?}:]", from)?; + } + ProjectionElem::Subslice { + from, + to, + from_end: true, + } if from == 0 => { + 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(()) } } @@ -214,6 +328,21 @@ pub enum PlaceOrdering { 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 { diff --git a/micromir/src/repack/place.rs b/mir-state-analysis/src/utils/repacker.rs similarity index 55% rename from micromir/src/repack/place.rs rename to mir-state-analysis/src/utils/repacker.rs index e4362cf7d8d..0ebd17a8eab 100644 --- a/micromir/src/repack/place.rs +++ b/mir-state-analysis/src/utils/repacker.rs @@ -6,8 +6,10 @@ use prusti_rustc_interface::{ data_structures::fx::FxHashSet, + dataflow::storage, + index::bit_set::BitSet, middle::{ - mir::{Body, Field, ProjectionElem}, + mir::{Body, Field, HasLocalDecls, Local, Mutability, ProjectionElem}, ty::{TyCtxt, TyKind}, }, }; @@ -16,7 +18,7 @@ use crate::Place; #[derive(Copy, Clone)] // TODO: modified version of fns taken from `prusti-interface/src/utils.rs`; deduplicate -pub(crate) struct PlaceRepacker<'a, 'tcx: 'a> { +pub struct PlaceRepacker<'a, 'tcx: 'a> { mir: &'a Body<'tcx>, tcx: TyCtxt<'tcx>, } @@ -26,26 +28,105 @@ impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { Self { mir, tcx } } - /// Expand `current_place` one level down by following the `guide_place`. - /// Returns the new `current_place` and a vector containing other places that + pub fn local_count(self) -> usize { + self.mir.local_decls().len() + } + + pub fn always_live_locals(self) -> BitSet { + storage::always_storage_live_locals(self.mir) + } + + pub fn body(self) -> &'a Body<'tcx> { + self.mir + } +} + +impl<'tcx> Place<'tcx> { + /// 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)>, 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() { + expanded.push((self, to)); + let (new_minuend, places) = self.expand_one_level(to, repacker); + self = new_minuend; + place_set.extend(places); + } + (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)> { + 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. - #[tracing::instrument(level = "trace", skip(self), ret)] + #[tracing::instrument(level = "trace", skip(repacker), ret)] pub(crate) fn expand_one_level( self, - current_place: Place<'tcx>, - guide_place: Place<'tcx>, - ) -> (Place<'tcx>, Vec>) { - let index = current_place.projection.len(); - let new_projection = self.tcx.mk_place_elems( - current_place - .projection + guide_place: Self, + repacker: PlaceRepacker<'_, 'tcx>, + ) -> (Self, Vec) { + let index = self.projection.len(); + let new_projection = repacker.tcx.mk_place_elems_from_iter( + self.projection .iter() .chain([guide_place.projection[index]]), ); - let new_current_place = Place::new(current_place.local, new_projection); + let new_current_place = Place::new(self.local, new_projection); let other_places = match guide_place.projection[index] { ProjectionElem::Field(projected_field, _field_ty) => { - self.expand_place(current_place, Some(projected_field.index())) + self.expand_field(Some(projected_field.index()), repacker) } ProjectionElem::ConstantIndex { offset, @@ -60,9 +141,10 @@ impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { } }) .map(|i| { - self.tcx + repacker + .tcx .mk_place_elem( - *current_place, + *self, ProjectionElem::ConstantIndex { offset: i, min_length, @@ -85,13 +167,13 @@ impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { /// 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_place( + pub fn expand_field( self, - place: Place<'tcx>, without_field: Option, - ) -> Vec> { + repacker: PlaceRepacker<'_, 'tcx>, + ) -> Vec { let mut places = Vec::new(); - let typ = place.ty(self.mir, self.tcx); + let typ = self.ty(repacker.mir, repacker.tcx); if !matches!(typ.ty.kind(), TyKind::Adt(..)) { assert!( typ.variant_index.is_none(), @@ -107,9 +189,11 @@ impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { for (index, field_def) in variant.fields.iter().enumerate() { if Some(index) != without_field { let field = Field::from_usize(index); - let field_place = - self.tcx - .mk_place_field(*place, field, field_def.ty(self.tcx, substs)); + let field_place = repacker.tcx.mk_place_field( + *self, + field, + field_def.ty(repacker.tcx, substs), + ); places.push(field_place.into()); } } @@ -118,7 +202,7 @@ impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { for (index, arg) in slice.iter().enumerate() { if Some(index) != without_field { let field = Field::from_usize(index); - let field_place = self.tcx.mk_place_field(*place, field, arg); + let field_place = repacker.tcx.mk_place_field(*self, field, arg); places.push(field_place.into()); } } @@ -127,7 +211,7 @@ impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { for (index, subst_ty) in substs.as_closure().upvar_tys().enumerate() { if Some(index) != without_field { let field = Field::from_usize(index); - let field_place = self.tcx.mk_place_field(*place, field, subst_ty); + let field_place = repacker.tcx.mk_place_field(*self, field, subst_ty); places.push(field_place.into()); } } @@ -136,7 +220,7 @@ impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { for (index, subst_ty) in substs.as_generator().upvar_tys().enumerate() { if Some(index) != without_field { let field = Field::from_usize(index); - let field_place = self.tcx.mk_place_field(*place, field, subst_ty); + let field_place = repacker.tcx.mk_place_field(*self, field, subst_ty); places.push(field_place.into()); } } @@ -146,72 +230,6 @@ impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { places } - /// Subtract the `subtrahend` place from the `minuend` place. The - /// subtraction is defined as set minus between `minuend` place replaced - /// with a set of places that are unrolled up to the same level as - /// `subtrahend` and the singleton `subtrahend` 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 subtrahend of each expansion. - #[tracing::instrument(level = "trace", skip(self), ret)] - pub fn expand( - self, - mut minuend: Place<'tcx>, - subtrahend: Place<'tcx>, - ) -> (Vec<(Place<'tcx>, Place<'tcx>)>, Vec>) { - assert!( - minuend.is_prefix(subtrahend), - "The minuend ({minuend:?}) must be the prefix of the subtrahend ({subtrahend:?})." - ); - let mut place_set = Vec::new(); - let mut expanded = Vec::new(); - while minuend.projection.len() < subtrahend.projection.len() { - expanded.push((minuend, subtrahend)); - let (new_minuend, places) = self.expand_one_level(minuend, subtrahend); - minuend = new_minuend; - place_set.extend(places); - } - (expanded, place_set) - } - - /// Try to collapse all places in `places` by following the - /// `guide_place`. This function is basically the reverse of - /// `expand`. - #[tracing::instrument(level = "trace", skip(self), ret)] - pub fn collapse( - self, - guide_place: Place<'tcx>, - places: &mut FxHashSet>, - ) -> Vec<(Place<'tcx>, Place<'tcx>)> { - let mut collapsed = Vec::new(); - let mut guide_places = vec![guide_place]; - while let Some(guide_place) = guide_places.pop() { - if !places.remove(&guide_place) { - let expand_guide = *places - .iter() - .find(|p| guide_place.is_prefix(**p)) - .unwrap_or_else(|| { - panic!( - "The `places` set didn't contain all \ - the places required to construct the \ - `guide_place`. Currently tried to find \ - `{guide_place:?}` in `{places:?}`." - ) - }); - let (expanded, new_places) = self.expand(guide_place, expand_guide); - // 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); - places.remove(&expand_guide); - } - } - collapsed.reverse(); - collapsed - } - // /// 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); @@ -222,23 +240,37 @@ impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { // 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) +// } +// } - #[tracing::instrument(level = "debug", skip(self), ret, fields(lp = ?left.projection, rp = ?right.projection))] - pub fn common_prefix(self, left: Place<'tcx>, right: Place<'tcx>) -> Place<'tcx> { - assert_eq!(left.local, right.local); +impl<'tcx> Place<'tcx> { + #[tracing::instrument(level = "debug", skip(repacker), ret, fields(lp = ?self.projection, rp = ?other.projection))] + pub fn common_prefix(self, other: Self, repacker: PlaceRepacker<'_, 'tcx>) -> Self { + assert_eq!(self.local, other.local); - let common_prefix = left - .compare_projections(right) + let common_prefix = self + .compare_projections(other) .take_while(|(eq, _, _)| *eq) .map(|(_, e1, _)| e1); - Place::new(left.local, self.tcx.mk_place_elems(common_prefix)) + Self::new( + self.local, + repacker.tcx.mk_place_elems_from_iter(common_prefix), + ) } - #[tracing::instrument(level = "info", skip(self), ret)] - pub fn joinable_to(self, from: Place<'tcx>, to: Place<'tcx>) -> Place<'tcx> { - assert!(from.is_prefix(to)); - let proj = from.projection.iter(); - let to_proj = to.projection[from.projection.len()..] + #[tracing::instrument(level = "info", skip(repacker), ret)] + pub fn joinable_to(self, to: Self, repacker: PlaceRepacker<'_, 'tcx>) -> Self { + assert!(self.is_prefix(to)); + let proj = self.projection.iter(); + let to_proj = to.projection[self.projection.len()..] .iter() .copied() .take_while(|p| { @@ -249,7 +281,28 @@ impl<'a, 'tcx: 'a> PlaceRepacker<'a, 'tcx> { | ProjectionElem::ConstantIndex { .. } ) }); - let projection = self.tcx.mk_place_elems(proj.chain(to_proj)); - Place::new(from.local, projection) + let projection = repacker.tcx.mk_place_elems_from_iter(proj.chain(to_proj)); + Self::new(self.local, projection) + } + + // 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.mir, repacker.tcx); + if let TyKind::Ref(_, _, mutability) = typ.ty.kind() { + *mutability + } else { + unreachable!("get_ref_mutability called on non-ref type: {:?}", typ.ty); + } } } diff --git a/micromir/tests/top_crates.rs b/mir-state-analysis/tests/top_crates.rs similarity index 100% rename from micromir/tests/top_crates.rs rename to mir-state-analysis/tests/top_crates.rs diff --git a/prusti/Cargo.toml b/prusti/Cargo.toml index 86a70addec0..c42681fc002 100644 --- a/prusti/Cargo.toml +++ b/prusti/Cargo.toml @@ -21,7 +21,7 @@ lazy_static = "1.4.0" tracing = { path = "../tracing" } tracing-subscriber = { version = "0.3", features = ["env-filter"] } tracing-chrome = "0.7" -micromir = { path = "../micromir" } +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 587f3b79be0..94eb61f7e5a 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -1,5 +1,5 @@ use crate::verifier::verify; -use micromir::test_free_pcs; +use mir_state_analysis::test_free_pcs; use prusti_common::config; use prusti_interface::{ environment::{mir_storage, Environment}, @@ -140,7 +140,14 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls { CrossCrateSpecs::import_export_cross_crate(&mut env, &mut def_spec); if !config::no_verify() { if config::test_free_pcs() { - test_free_pcs(&env); + for proc_id in env.get_annotated_procedures_and_types().0.iter() { + let name = env.name.get_unique_item_name(*proc_id); + println!("Calculating FPCS for: {name}"); + + let current_procedure = env.get_procedure(*proc_id); + let mir = current_procedure.get_mir_rc(); + test_free_pcs(&mir, tcx); + } } else { verify(env, def_spec); } diff --git a/x.py b/x.py index 8cba90906e7..4d02093296e 100755 --- a/x.py +++ b/x.py @@ -37,7 +37,7 @@ RUSTFMT_CRATES = [ 'analysis', 'jni-gen', - 'micromir', + 'mir-state-analysis', 'prusti', 'prusti-common', 'prusti-contracts/prusti-contracts',