Skip to content

Commit

Permalink
Inherit the third field on "final" reborrows
Browse files Browse the repository at this point in the history
  • Loading branch information
arnaudgolfouse committed Nov 30, 2023
1 parent 4adfadd commit b3fd4ed
Show file tree
Hide file tree
Showing 11 changed files with 395 additions and 39 deletions.
2 changes: 2 additions & 0 deletions creusot/src/analysis.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,13 @@ use rustc_middle::mir::{
mod frozen_locals;
mod init_locals;
mod liveness_no_drop;
mod not_final_places;
mod uninit_locals;

pub use frozen_locals::*;
pub use init_locals::*;
pub use liveness_no_drop::*;
pub use not_final_places::NotFinalPlaces;
pub use uninit_locals::*;

pub struct NeverLive(BitSet<Local>);
Expand Down
281 changes: 281 additions & 0 deletions creusot/src/analysis/not_final_places.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,281 @@
use std::collections::HashMap;
// 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 https://mozilla.org/MPL/2.0/.
//
use rustc_index::bit_set::BitSet;
use rustc_middle::mir::{
self, AssertKind, BasicBlock, Location, NonDivergingIntrinsic, Operand, Place, PlaceElem,
Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
};
use rustc_mir_dataflow::{
fmt::DebugWithContext, AnalysisDomain, Backward, GenKill, GenKillAnalysis,
};

pub type PlaceId = usize;

pub struct NotFinalPlaces<'tcx> {
pub places: HashMap<Place<'tcx>, PlaceId>,
}

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;
}
let idx = places.len();
if let std::collections::hash_map::Entry::Vacant(entry) = places.entry(*p) {
entry.insert(idx);
}
};
// body.visit_with(/* PlaceVisitor */);
for bb in body.basic_blocks.iter() {
for s in &bb.statements {
visit_statement(&mut visit, s);
}
visit_terminator(&mut visit, bb.terminator())
}
Self { places }
}
}

impl<'tcx> DebugWithContext<NotFinalPlaces<'tcx>> for BitSet<PlaceId> {}

impl<'tcx> AnalysisDomain<'tcx> for NotFinalPlaces<'tcx> {
type Domain = BitSet<PlaceId>;

type Direction = Backward;

const NAME: &'static str = "not_final_places";

fn bottom_value(&self, _: &mir::Body<'tcx>) -> Self::Domain {
// bottom = empty
BitSet::new_empty(self.places.len())
}

fn initialize_start_block(&self, _: &mir::Body<'tcx>, _: &mut Self::Domain) {}
}

impl<'tcx> GenKillAnalysis<'tcx> for NotFinalPlaces<'tcx> {
type Idx = PlaceId;

fn statement_effect(
&mut self,
trans: &mut impl GenKill<Self::Idx>,
statement: &Statement<'tcx>,
_: 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,
);
}



fn terminator_effect(
&mut self,
trans: &mut impl GenKill<Self::Idx>,
terminator: &Terminator<'tcx>,
_: 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,
);
}

fn call_return_effect(
&mut self,
trans: &mut impl GenKill<Self::Idx>,
_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)
}
});
}

fn before_statement_effect(
&mut self,
_trans: &mut impl GenKill<Self::Idx>,
_statement: &mir::Statement<'tcx>,
_location: Location,
) {
// TODO: apply reads here, NOT in statement effect
}

fn before_terminator_effect(
&mut self,
_trans: &mut impl GenKill<Self::Idx>,
_terminator: &mir::Terminator<'tcx>,
_location: Location,
) {
// TODO: same
}
}

#[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,
}

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)
}
}
},
}
}

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);
}
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);
}
}
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")
}
}
}
4 changes: 2 additions & 2 deletions creusot/src/backend/optimization.rs
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ impl<'a, 'tcx> LocalUsage<'a, 'tcx> {
fn visit_rvalue(&mut self, r: &fmir::RValue<'tcx>) {
match r {
fmir::RValue::Ghost(t) => self.visit_term(t),
fmir::RValue::Borrow(p) => {
fmir::RValue::FinalBorrow(p) | fmir::RValue::Borrow(p) => {
self.read_place(p);
self.read_place(p)
}
Expand Down Expand Up @@ -266,7 +266,7 @@ impl<'tcx> SimplePropagator<'tcx> {
fn visit_rvalue(&mut self, r: &mut fmir::RValue<'tcx>) {
match r {
fmir::RValue::Ghost(t) => self.visit_term(t),
fmir::RValue::Borrow(p) => {
fmir::RValue::FinalBorrow(p) | fmir::RValue::Borrow(p) => {
assert!(self.prop.get(&p.local).is_none(), "Trying to propagate borrowed variable")
}
fmir::RValue::Expr(e) => self.visit_expr(e),
Expand Down
52 changes: 51 additions & 1 deletion creusot/src/backend/program.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ use crate::{
};
use rustc_hir::{def::DefKind, def_id::DefId, Unsafety};
use rustc_middle::{
mir::{BasicBlock, BinOp},
mir::{BasicBlock, BinOp, ProjectionElem},
ty::TyKind,
};
use rustc_span::DUMMY_SP;
Expand Down Expand Up @@ -622,6 +622,40 @@ impl<'tcx> Place<'tcx> {
}
}

pub(crate) fn borrow_generated_id<V, T>(
original_borrow: Exp,
projection: &[ProjectionElem<V, T>],
) -> Exp {
let mut borrow_id = Exp::Call(
Box::new(Exp::impure_qvar(QName::from_string("Borrow.get_id").unwrap())),
vec![original_borrow],
);
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))],
);
}
ProjectionElem::Field(idx, _) => {
borrow_id = Exp::Call(
Box::new(Exp::impure_qvar(QName::from_string("Borrow.inherit_id").unwrap())),
vec![borrow_id, Exp::Const(Constant::Int(idx.as_u32() as i128 + 1, None))],
);
}
ProjectionElem::Index(_)
| ProjectionElem::ConstantIndex { .. }
| ProjectionElem::Subslice { .. }
| ProjectionElem::Downcast(_, _)
| ProjectionElem::OpaqueCast(_) => {
todo!("not supported as final, fallback to borrow_mut")
}
}
}
borrow_id
}

impl<'tcx> Statement<'tcx> {
pub(crate) fn to_why(
self,
Expand All @@ -642,6 +676,22 @@ impl<'tcx> Statement<'tcx> {
place::create_assign_inner(ctx, names, locals, &rhs, reassign),
]
}
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 borrow = Exp::Call(
Box::new(Exp::impure_qvar(QName::from_string("Borrow.borrow_final").unwrap())),
vec![rhs.as_rplace(ctx, names, locals), borrow_id],
);
let reassign = Exp::Final(Box::new(lhs.as_rplace(ctx, names, locals)));

vec![
place::create_assign_inner(ctx, names, locals, &lhs, borrow),
place::create_assign_inner(ctx, names, locals, &rhs, reassign),
]
}
Statement::Assignment(lhs, RValue::Ghost(rhs)) => {
let ghost = lower_pure(ctx, names, rhs);

Expand Down
Loading

0 comments on commit b3fd4ed

Please sign in to comment.