diff --git a/creusot/src/analysis/not_final_places.rs b/creusot/src/analysis/not_final_places.rs index 2b49451fb5..0c55b85a3c 100644 --- a/creusot/src/analysis/not_final_places.rs +++ b/creusot/src/analysis/not_final_places.rs @@ -3,41 +3,160 @@ use std::collections::HashMap; // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at https://mozilla.org/MPL/2.0/. // +use crate::extended_location::ExtendedLocation; use rustc_index::bit_set::BitSet; use rustc_middle::mir::{ - self, AssertKind, BasicBlock, Location, NonDivergingIntrinsic, Operand, Place, PlaceElem, - Rvalue, Statement, StatementKind, Terminator, TerminatorKind, + self, visit::Visitor, BasicBlock, Location, Place, ProjectionElem, Statement, Terminator, }; use rustc_mir_dataflow::{ - fmt::DebugWithContext, AnalysisDomain, Backward, GenKill, GenKillAnalysis, + fmt::DebugWithContext, AnalysisDomain, Backward, GenKill, GenKillAnalysis, ResultsCursor, }; pub type PlaceId = usize; +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] +struct PlaceAsSLice<'tcx> { + local: mir::Local, + projection: &'tcx [mir::PlaceElem<'tcx>], +} +impl<'a, 'tcx> From<&'a Place<'tcx>> for PlaceAsSLice<'tcx> { + fn from(place: &'a Place<'tcx>) -> Self { + Self { local: place.local, projection: &place.projection } + } +} + +/// Analysis to determine "final" reborrows. +/// +/// # Final borrows +/// +/// A reborrow is considered final if the place it reborrows from is never read again. +/// In that case, the reborrow id can be inherited: +/// - If this is a reborrow of the same place (e.g. `let y = &mut *x`), the new id is the same. +/// - Else (e.g. `let y = &mut x.field`), the new id is deterministically derived from the old. +/// +/// # Example Usage +/// +/// Note that this analysis determines places that are **not** final. +/// +/// ```rust,ignore +/// let tcx: rustc_middle::ty::TyCtxt = /* */; +/// let body: rustc_middle::mir::Body = /* */; +/// let mut not_final_places = NotFinalPlaces::new(body) +/// .into_engine(tcx, body) +/// .iterate_to_fixpoint() +/// .into_results_cursor(body); +/// /* +/// ... +/// */ +/// let place: rustc_middle::mir::Place = /* place that we want to reborrow from */; +/// let location: rustc_middle::mir::Location = /* location of the reborrow in the MIR body */; +/// let is_final = NotFinalPlaces::is_final_at(not_final_borrows, place, location); +/// ``` +#[derive(Debug)] pub struct NotFinalPlaces<'tcx> { - pub places: HashMap, PlaceId>, + /// Mapping from a place to its ID + /// + /// This is necessary to use a `BitSet`. + places: HashMap, PlaceId>, + /// Used to ban unnesting (`**ref_ref_x = ...`) + /// + /// In practice, this means the underlying place has no `Deref`. + has_indirection: BitSet, + /// Maps each place to the set of its subplaces. + /// + /// A `p1` is a subplace of `p2` if they refer to the same local variable, and + /// `p2.projection` is a prefix of `p1.projection`. + subplaces: Vec>>, + /// Maps each place to the set of conflicting subplaces. + /// + /// Two places `p1` and `p2` are conflicting if one is a subplace of the other. + conflicting_places: Vec>>, } impl<'tcx> NotFinalPlaces<'tcx> { pub fn new(body: &mir::Body<'tcx>) -> Self { - let mut places = HashMap::new(); - let mut visit = |p: &Place<'tcx>, _| { - if p.projection.first() != Some(&PlaceElem::Deref) { - return; + struct VisitAllPlaces<'tcx>(HashMap, PlaceId>); + impl<'tcx> Visitor<'tcx> for VisitAllPlaces<'tcx> { + fn visit_place( + &mut self, + place: &Place<'tcx>, + _: mir::visit::PlaceContext, + _: Location, + ) { + let mut place_as_slice = PlaceAsSLice::from(place); + loop { + let idx = self.0.len(); + if let std::collections::hash_map::Entry::Vacant(entry) = + self.0.entry(place_as_slice) + { + entry.insert(idx); + } + if place_as_slice.projection.is_empty() { + break; + } + // Include all "superplace" of the place. + // This is needed, because in `is_final_at`, we might refer to such a + // place, even though it does not appear in the MIR. + place_as_slice.projection = + &place_as_slice.projection[..place_as_slice.projection.len() - 1] + } } - let idx = places.len(); - if let std::collections::hash_map::Entry::Vacant(entry) = places.entry(*p) { - entry.insert(idx); + } + + let mut visitor = VisitAllPlaces(HashMap::new()); + visitor.visit_body(body); + let places = visitor.0; + let mut contains_dereference = BitSet::new_empty(places.len()); + let mut subplaces = vec![Vec::new(); places.len()]; + let mut conflicting_places = vec![Vec::new(); places.len()]; + for (place, id) in &places { + if place.projection.get(1..).unwrap_or_default().contains(&ProjectionElem::Deref) { + contains_dereference.insert(*id); } - }; - // body.visit_with(/* PlaceVisitor */); - for bb in body.basic_blocks.iter() { - for s in &bb.statements { - visit_statement(&mut visit, s); + for (other_place, other_id) in &places { + if id == other_id || place.local != other_place.local { + continue; + } + if other_place.projection.get(..place.projection.len()) == Some(place.projection) { + subplaces[*id].push(*other_place); + conflicting_places[*id].push(*other_place); + conflicting_places[*other_id].push(*place); + } } - visit_terminator(&mut visit, bb.terminator()) } - Self { places } + Self { places, has_indirection: contains_dereference, subplaces, conflicting_places } + } + + /// Run the analysis right **after** `location`, and determines if `place` is a final reborrow. + pub fn is_final_at( + cursor: &mut ResultsCursor<'_, 'tcx, NotFinalPlaces<'tcx>>, + place: &Place<'tcx>, + location: Location, + ) -> bool { + let deref_position = + match place.projection.iter().position(|p| matches!(p, ProjectionElem::Deref)) { + Some(p) => p, + // This is not a reborrow + None => return false, + }; + if place.projection[deref_position + 1..].contains(&ProjectionElem::Deref) { + // unnesting + return false; + } + + ExtendedLocation::Start(location.successor_within_block()).seek_to(cursor); + let analysis: &Self = cursor.analysis(); + + let place_borrow = PlaceAsSLice { local: place.local, projection: &place.projection }; + + let id = analysis.places[&place_borrow]; + for place in std::iter::once(&place_borrow).chain(analysis.conflicting_places[id].iter()) { + let id = analysis.places[place]; + if cursor.contains(id) { + return false; + } + } + true } } @@ -51,10 +170,11 @@ impl<'tcx> AnalysisDomain<'tcx> for NotFinalPlaces<'tcx> { const NAME: &'static str = "not_final_places"; fn bottom_value(&self, _: &mir::Body<'tcx>) -> Self::Domain { - // bottom = empty + // start with every place "dead" BitSet::new_empty(self.places.len()) } + // no initialization, because we are doing backward analysis. fn initialize_start_block(&self, _: &mir::Body<'tcx>, _: &mut Self::Domain) {} } @@ -65,40 +185,20 @@ impl<'tcx> GenKillAnalysis<'tcx> for NotFinalPlaces<'tcx> { &mut self, trans: &mut impl GenKill, statement: &Statement<'tcx>, - _: Location, + location: Location, ) { - visit_statement( - |place, kind| { - if let Some(&idx) = self.places.get(place) { - match kind { - GenOrKill::Gen => trans.gen(idx), - GenOrKill::Kill => trans.kill(idx), - } - } - }, - statement, - ); + PlaceVisitor { mapping: self, trans, context: Context::Write } + .visit_statement(statement, location) } - - fn terminator_effect( &mut self, trans: &mut impl GenKill, terminator: &Terminator<'tcx>, - _: Location, + location: Location, ) { - visit_terminator( - |place, kind| { - if let Some(&idx) = self.places.get(place) { - match kind { - GenOrKill::Gen => trans.gen(idx), - GenOrKill::Kill => trans.kill(idx), - } - } - }, - terminator, - ); + PlaceVisitor { mapping: self, trans, context: Context::Write } + .visit_terminator(terminator, location) } fn call_return_effect( @@ -107,175 +207,73 @@ impl<'tcx> GenKillAnalysis<'tcx> for NotFinalPlaces<'tcx> { _block: BasicBlock, return_places: rustc_mir_dataflow::CallReturnPlaces<'_, 'tcx>, ) { - return_places.for_each(|place| { - if let Some(&idx) = self.places.get(&place) { - trans.kill(idx) - } - }); + return_places.for_each(|place| trans.gen(self.places[&(&place).into()])); } + // We use `before_*_effect` to ensure that reads are processed _before_ writes. fn before_statement_effect( &mut self, - _trans: &mut impl GenKill, - _statement: &mir::Statement<'tcx>, - _location: Location, + trans: &mut impl GenKill, + statement: &mir::Statement<'tcx>, + location: Location, ) { - // TODO: apply reads here, NOT in statement effect + PlaceVisitor { mapping: self, trans, context: Context::Read } + .visit_statement(statement, location) } fn before_terminator_effect( &mut self, - _trans: &mut impl GenKill, - _terminator: &mir::Terminator<'tcx>, - _location: Location, + trans: &mut impl GenKill, + terminator: &mir::Terminator<'tcx>, + location: Location, ) { - // TODO: same + PlaceVisitor { mapping: self, trans, context: Context::Read } + .visit_terminator(terminator, location) } } -#[derive(Debug)] -enum GenOrKill { - /// Used when a place is being read: meaning it has to be alive. - Gen, - /// Used when a place is being written: meaning it (the old value) can be dead. - Kill, +#[derive(Clone, Copy, Debug)] +enum Context { + Read, + Write, } -fn visit_statement<'tcx>( - mut visit: impl FnMut(&Place<'tcx>, GenOrKill), - statement: &Statement<'tcx>, -) { - match &statement.kind { - StatementKind::Assign(a) => { - let (l, r) = a.as_ref(); - visit(l, GenOrKill::Kill); - // TODO: Some of those should maybe not trigger a Gen - match r { - Rvalue::Use(op) - | Rvalue::Repeat(op, _) - | Rvalue::Cast(_, op, _) - | Rvalue::UnaryOp(_, op) - | Rvalue::ShallowInitBox(op, _) => { - if let Operand::Copy(place) | Operand::Move(place) = op { - visit(place, GenOrKill::Gen) - } - } - Rvalue::Ref(_, _, place) - | Rvalue::AddressOf(_, place) - | Rvalue::Discriminant(place) - | Rvalue::Len(place) - | Rvalue::CopyForDeref(place) => visit(place, GenOrKill::Gen), - Rvalue::BinaryOp(_, operands) | Rvalue::CheckedBinaryOp(_, operands) => { - let (l, r) = operands.as_ref(); - if let Operand::Copy(place) | Operand::Move(place) = l { - visit(place, GenOrKill::Gen) - } - if let Operand::Copy(place) | Operand::Move(place) = r { - visit(place, GenOrKill::Gen) - } - } - Rvalue::Aggregate(_, ops) => { - for op in ops { - if let Operand::Copy(place) | Operand::Move(place) = op { - visit(place, GenOrKill::Gen) - } - } - } - Rvalue::ThreadLocalRef(_) | Rvalue::NullaryOp(_, _) => {} - } - } - // TODO: maybe should be a gen ? - StatementKind::FakeRead(_) => {} - StatementKind::Deinit(place) - | StatementKind::PlaceMention(place) - | StatementKind::Retag(_, place) - | StatementKind::SetDiscriminant { place, variant_index: _ } => { - _ = place; - // TODO: maybe should be a kill ? - } - StatementKind::StorageLive(_) - | StatementKind::StorageDead(_) - | StatementKind::Coverage(_) - | StatementKind::ConstEvalCounter - | StatementKind::Nop - | StatementKind::AscribeUserType(_, _) => {} - StatementKind::Intrinsic(intrinsic) => match intrinsic.as_ref() { - NonDivergingIntrinsic::Assume(_) => {} - NonDivergingIntrinsic::CopyNonOverlapping(c) => { - if let Operand::Copy(place) | Operand::Move(place) = &c.src { - visit(place, GenOrKill::Gen) - } - if let Operand::Copy(place) | Operand::Move(place) = &c.dst { - visit(place, GenOrKill::Kill) - } - } - }, - } +struct PlaceVisitor<'a, 'tcx, T> { + mapping: &'a NotFinalPlaces<'tcx>, + trans: &'a mut T, + context: Context, } -fn visit_terminator<'tcx>( - mut visit: impl FnMut(&Place<'tcx>, GenOrKill), - terminator: &Terminator<'tcx>, -) { - match &terminator.kind { - TerminatorKind::SwitchInt { discr, targets: _ } => { - if let Operand::Copy(place) | Operand::Move(place) = discr { - visit(place, GenOrKill::Gen) - } - } - TerminatorKind::Goto { target: _ } - | TerminatorKind::Resume - | TerminatorKind::Terminate - | TerminatorKind::Return - | TerminatorKind::Unreachable - | TerminatorKind::GeneratorDrop - | TerminatorKind::FalseEdge { .. } - | TerminatorKind::FalseUnwind { .. } - | TerminatorKind::Drop { .. } => {} - TerminatorKind::Call { func, args, destination, .. } => { - if let Operand::Copy(place) | Operand::Move(place) = func { - visit(place, GenOrKill::Gen); - } - for arg in args { - if let Operand::Copy(place) | Operand::Move(place) = arg { - visit(place, GenOrKill::Gen); - } - } - visit(destination, GenOrKill::Kill); - } - TerminatorKind::Assert { cond, msg, .. } => { - if let Operand::Copy(place) | Operand::Move(place) = cond { - visit(place, GenOrKill::Gen); +impl<'a, 'tcx, T> Visitor<'tcx> for PlaceVisitor<'a, 'tcx, T> +where + T: GenKill, +{ + fn visit_place(&mut self, place: &Place<'tcx>, context: mir::visit::PlaceContext, _: Location) { + use mir::visit::{MutatingUseContext, PlaceContext}; + match (self.context, context) { + // TODO: should we really accept _all_ nonmutating uses ? + (Context::Read, PlaceContext::NonMutatingUse(_)) + // Note that a borrow is considered a read + | (Context::Read, PlaceContext::MutatingUse(MutatingUseContext::Borrow)) => { + self.trans.gen(self.mapping.places[&place.into()]) } - match msg.as_ref() { - AssertKind::BoundsCheck { len: op1, index: op2 } - | AssertKind::Overflow(_, op1, op2) - | AssertKind::MisalignedPointerDereference { required: op1, found: op2 } => { - if let Operand::Copy(place) | Operand::Move(place) = op1 { - visit(place, GenOrKill::Gen); - } - if let Operand::Copy(place) | Operand::Move(place) = op2 { - visit(place, GenOrKill::Gen); - } - } - AssertKind::OverflowNeg(op) - | AssertKind::DivisionByZero(op) - | AssertKind::RemainderByZero(op) => { - if let Operand::Copy(place) | Operand::Move(place) = op { - visit(place, GenOrKill::Gen); + ( + Context::Write, + PlaceContext::MutatingUse(MutatingUseContext::Drop | MutatingUseContext::Store), + ) => { + let id: usize = self.mapping.places[&place.into()]; + if !self.mapping.has_indirection.contains(id) { + self.trans.kill(id); + // Now, kill all subplaces of this place + for subplace in self.mapping.subplaces[id].iter() { + let subplace_id: usize = self.mapping.places[subplace]; + if !self.mapping.has_indirection.contains(subplace_id) { + self.trans.kill(subplace_id); + } } } - AssertKind::ResumedAfterReturn(_) | AssertKind::ResumedAfterPanic(_) => {} } - } - TerminatorKind::Yield { value, resume_arg, .. } => { - if let Operand::Copy(place) | Operand::Move(place) = value { - visit(place, GenOrKill::Gen); - } - visit(resume_arg, GenOrKill::Kill); - } - TerminatorKind::InlineAsm { .. } => { - panic!("unsupported") + _ => {} } } } diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs index ed22b28be6..6fb04df7ff 100644 --- a/creusot/src/backend/program.rs +++ b/creusot/src/backend/program.rs @@ -622,34 +622,36 @@ impl<'tcx> Place<'tcx> { } } -pub(crate) fn borrow_generated_id( +pub(crate) fn borrow_generated_id( original_borrow: Exp, projection: &[ProjectionElem], ) -> Exp { let mut borrow_id = Exp::Call( - Box::new(Exp::impure_qvar(QName::from_string("Borrow.get_id").unwrap())), - vec![original_borrow], + Box::new(Exp::pure_qvar(QName::from_string("Borrow.get_id").unwrap())), + vec![original_borrow], // TODO: should be "nested" (how ?) ); + // NOTE: no Deref should be present. for proj in projection { match proj { ProjectionElem::Deref => { - borrow_id = Exp::Call( - Box::new(Exp::impure_qvar(QName::from_string("Borrow.inherit_id").unwrap())), - vec![borrow_id, Exp::Const(Constant::Int(0, None))], - ); + unreachable!( + "the final borrow analysis should have garanteed that only one `Deref` appears" + ) } ProjectionElem::Field(idx, _) => { borrow_id = Exp::Call( - Box::new(Exp::impure_qvar(QName::from_string("Borrow.inherit_id").unwrap())), + Box::new(Exp::pure_qvar(QName::from_string("Borrow.inherit_id").unwrap())), vec![borrow_id, Exp::Const(Constant::Int(idx.as_u32() as i128 + 1, None))], ); } + ProjectionElem::Downcast(_, _) => { + // since only one variant can be active at a time, there is no need to change the borrow index further + } ProjectionElem::Index(_) | ProjectionElem::ConstantIndex { .. } | ProjectionElem::Subslice { .. } - | ProjectionElem::Downcast(_, _) | ProjectionElem::OpaqueCast(_) => { - todo!("not supported as final, fallback to borrow_mut") + todo!("{proj:?} not supported as final") } } } @@ -677,10 +679,15 @@ impl<'tcx> Statement<'tcx> { ] } Statement::Assignment(lhs, RValue::FinalBorrow(rhs)) => { - let borrow_id = borrow_generated_id( - Exp::impure_var(Ident::build(rhs.local.as_str())), - &rhs.projection[1..], - ); + let find_borrow = + rhs.projection.iter().position(|p| matches!(p, ProjectionElem::Deref)).unwrap(); + let original_borrow = Place { + local: rhs.local.clone(), + projection: rhs.projection[..find_borrow].to_vec(), + } + .as_rplace(ctx, names, locals); + let borrow_id = + borrow_generated_id(original_borrow, &rhs.projection[find_borrow + 1..]); let borrow = Exp::Call( Box::new(Exp::impure_qvar(QName::from_string("Borrow.borrow_final").unwrap())), vec![rhs.as_rplace(ctx, names, locals), borrow_id], diff --git a/creusot/src/backend/term.rs b/creusot/src/backend/term.rs index 1dda81a592..634ca3209a 100644 --- a/creusot/src/backend/term.rs +++ b/creusot/src/backend/term.rs @@ -249,11 +249,13 @@ impl<'tcx> Lower<'_, 'tcx> { } TermKind::Absurd => Exp::Absurd, TermKind::Reborrow { box term, projection } => { + // NOTE: reborrows in the logic are always considered "final" let ty = term.ty.builtin_deref(false).expect("expected reference type").ty; let inner = self.lower_term(term); self.names.import_prelude_module(PreludeModule::Borrow); let curr = Exp::Current(Box::new(inner.clone())); let fin = Exp::Final(Box::new(inner.clone())); + // the projection is already what we want: whatever happens after the _last_ dereference. let borrow_id = borrow_generated_id(inner, &projection); let proj: Vec<_> = map_projections(projection.into_iter(), |term| self.lower_term(term)).collect(); @@ -267,7 +269,6 @@ impl<'tcx> Lower<'_, 'tcx> { fields: vec![ ("current".into(), curr), ("final".into(), fin), - // FIXME: Generate the new id with inherit_id ("id".into(), borrow_id), ], } diff --git a/creusot/src/translation/function.rs b/creusot/src/translation/function.rs index e3dd57a6fe..fbf817f7af 100644 --- a/creusot/src/translation/function.rs +++ b/creusot/src/translation/function.rs @@ -236,6 +236,9 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> { self.current_block.1 = Some(t); } + /// # Parameters + /// + /// `is_final` signals that the emitted borrow should be final: see [`NotFinalPlaces`]. fn emit_borrow(&mut self, lhs: &Place<'tcx>, rhs: &Place<'tcx>, is_final: bool) { let p = self.translate_place(*rhs); self.emit_assignment( diff --git a/creusot/src/translation/function/statement.rs b/creusot/src/translation/function/statement.rs index 2d8a7971e7..f924c4631e 100644 --- a/creusot/src/translation/function/statement.rs +++ b/creusot/src/translation/function/statement.rs @@ -1,7 +1,6 @@ use super::BodyTranslator; use crate::{ analysis::NotFinalPlaces, - extended_location::ExtendedLocation, translation::{ fmir::{self, Expr, RValue}, specification::inv_subst, @@ -95,14 +94,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> { return; } - ExtendedLocation::Start(loc.successor_within_block()) - .seek_to(not_final_borrows); - let is_final = - if let Some(&pl_index) = not_final_borrows.analysis().places.get(pl) { - !not_final_borrows.contains(pl_index) - } else { - false - }; + let is_final = NotFinalPlaces::is_final_at(not_final_borrows, pl, loc); self.emit_borrow(place, pl, is_final); return; }