Skip to content

Commit

Permalink
Format code
Browse files Browse the repository at this point in the history
  • Loading branch information
@fpoli
fpoli committed Jun 30, 2023
1 parent 08f4aaf commit fe877bd
Show file tree
Hide file tree
Showing 8 changed files with 207 additions and 85 deletions.
2 changes: 1 addition & 1 deletion Cargo.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

22 changes: 16 additions & 6 deletions prusti-interface/src/environment/mir_body/patch/compiler.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,10 @@ impl<'tcx> MirPatch<'tcx> {
Some(index) => self.new_blocks[index].statements.len(),
None => body[bb].statements.len(),
};
Location { block: bb, statement_index: offset }
Location {
block: bb,
statement_index: offset,
}
}

pub fn new_internal_with_info(
Expand Down Expand Up @@ -224,12 +227,19 @@ impl<'tcx> MirPatch<'tcx> {
delta = 0;
last_bb = loc.block;
}
debug!("MirPatch: adding statement {:?} at loc {:?}+{}", stmt, loc, delta);
debug!(
"MirPatch: adding statement {:?} at loc {:?}+{}",
stmt, loc, delta
);
loc.statement_index += delta;
let source_info = Self::source_info_for_index(&body[loc.block], loc);
body[loc.block]
.statements
.insert(loc.statement_index, Statement { source_info, kind: stmt });
body[loc.block].statements.insert(
loc.statement_index,
Statement {
source_info,
kind: stmt,
},
);
delta += 1;
}
}
Expand All @@ -248,4 +258,4 @@ impl<'tcx> MirPatch<'tcx> {
};
Self::source_info_for_index(data, loc)
}
}
}
126 changes: 94 additions & 32 deletions prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ use log::debug;
use prusti_interface::environment::mir_body::patch::MirPatch;
use prusti_rustc_interface::{
abi::{FieldIdx, VariantIdx, FIRST_VARIANT},
dataflow::elaborate_drops::{DropFlagState, DropFlagMode, DropStyle, Unwind},
dataflow::elaborate_drops::{DropFlagMode, DropFlagState, DropStyle, Unwind},
hir,
hir::lang_items::LangItem,
index::Idx,
Expand All @@ -25,8 +25,8 @@ use prusti_rustc_interface::{
ty::{self, subst::SubstsRef, util::IntTypeExt, Ty, TyCtxt},
},
};
use tracing::instrument;
use std::{fmt, iter};
use tracing::instrument;

trait UnwindPublic {
fn is_cleanup(self) -> bool;
Expand Down Expand Up @@ -153,7 +153,15 @@ pub fn elaborate_drop<'b, 'tcx, D>(
D: DropElaborator<'b, 'tcx>,
'tcx: 'b,
{
DropCtxt { elaborator, source_info, place, path, succ, unwind }.elaborate_drop(bb)
DropCtxt {
elaborator,
source_info,
place,
path,
succ,
unwind,
}
.elaborate_drop(bb)
}

impl<'l, 'b, 'tcx, D> DropCtxt<'l, 'b, 'tcx, D>
Expand Down Expand Up @@ -299,18 +307,27 @@ where
fields: &[(Place<'tcx>, Option<D::Path>)],
) -> Vec<BasicBlock> {
iter::once(succ)
.chain(fields.iter().rev().zip(unwind_ladder).map(|(&(place, path), &unwind_succ)| {
succ = self.drop_subpath(place, path, succ, unwind_succ);
succ
}))
.chain(
fields
.iter()
.rev()
.zip(unwind_ladder)
.map(|(&(place, path), &unwind_succ)| {
succ = self.drop_subpath(place, path, succ, unwind_succ);
succ
}),
)
.collect()
}

fn drop_ladder_bottom(&mut self) -> (BasicBlock, Unwind) {
// Clear the "master" drop flag at the end. This is needed
// because the "master" drop protects the ADT's discriminant,
// which is invalidated after the ADT is dropped.
(self.drop_flag_reset_block(DropFlagMode::Shallow, self.succ, self.unwind), self.unwind)
(
self.drop_flag_reset_block(DropFlagMode::Shallow, self.succ, self.unwind),
self.unwind,
)
}

/// Creates a full drop ladder, consisting of 2 connected half-drop-ladders
Expand Down Expand Up @@ -340,7 +357,8 @@ where

let mut fields = fields;
fields.retain(|&(place, _)| {
self.place_ty(place).needs_drop(self.tcx(), self.elaborator.param_env())
self.place_ty(place)
.needs_drop(self.tcx(), self.elaborator.param_env())
});

debug!("drop_ladder - fields needing drop: {:?}", fields);
Expand All @@ -355,7 +373,10 @@ where

let normal_ladder = self.drop_halfladder(&unwind_ladder, succ, &fields);

(*normal_ladder.last().unwrap(), *unwind_ladder.last().unwrap())
(
*normal_ladder.last().unwrap(),
*unwind_ladder.last().unwrap(),
)
}

fn open_drop_for_tuple(&mut self, tys: &[Ty<'tcx>]) -> BasicBlock {
Expand Down Expand Up @@ -385,16 +406,23 @@ where
let nonnull_ty = unique_variant.fields[FieldIdx::from_u32(0)].ty(self.tcx(), substs);
let ptr_ty = self.tcx().mk_imm_ptr(substs[0].expect_ty());

let unique_place = self.tcx().mk_place_field(self.place, FieldIdx::new(0), unique_ty);
let nonnull_place = self.tcx().mk_place_field(unique_place, FieldIdx::new(0), nonnull_ty);
let ptr_place = self.tcx().mk_place_field(nonnull_place, FieldIdx::new(0), ptr_ty);
let unique_place = self
.tcx()
.mk_place_field(self.place, FieldIdx::new(0), unique_ty);
let nonnull_place = self
.tcx()
.mk_place_field(unique_place, FieldIdx::new(0), nonnull_ty);
let ptr_place = self
.tcx()
.mk_place_field(nonnull_place, FieldIdx::new(0), ptr_ty);
let interior = self.tcx().mk_place_deref(ptr_place);

let interior_path = self.elaborator.deref_subpath(self.path);

let succ = self.box_free_block(adt, substs, self.succ, self.unwind);
let unwind_succ =
self.unwind.map(|unwind| self.box_free_block(adt, substs, unwind, Unwind::InCleanup));
let unwind_succ = self
.unwind
.map(|unwind| self.box_free_block(adt, substs, unwind, Unwind::InCleanup));

self.drop_subpath(interior, interior_path, succ, unwind_succ)
}
Expand Down Expand Up @@ -455,8 +483,11 @@ where
) -> (BasicBlock, Unwind) {
let mut values = Vec::with_capacity(adt.variants().len());
let mut normal_blocks = Vec::with_capacity(adt.variants().len());
let mut unwind_blocks =
if unwind.is_cleanup() { None } else { Some(Vec::with_capacity(adt.variants().len())) };
let mut unwind_blocks = if unwind.is_cleanup() {
None
} else {
Some(Vec::with_capacity(adt.variants().len()))
};

let mut have_otherwise_with_drop_glue = false;
let mut have_otherwise = false;
Expand Down Expand Up @@ -518,12 +549,18 @@ where
} else if !have_otherwise_with_drop_glue {
normal_blocks.push(self.goto_block(succ, unwind));
if let Unwind::To(unwind) = unwind {
unwind_blocks.as_mut().unwrap().push(self.goto_block(unwind, Unwind::InCleanup));
unwind_blocks
.as_mut()
.unwrap()
.push(self.goto_block(unwind, Unwind::InCleanup));
}
} else {
normal_blocks.push(self.drop_block(succ, unwind));
if let Unwind::To(unwind) = unwind {
unwind_blocks.as_mut().unwrap().push(self.drop_block(unwind, Unwind::InCleanup));
unwind_blocks
.as_mut()
.unwrap()
.push(self.drop_block(unwind, Unwind::InCleanup));
}
}

Expand Down Expand Up @@ -584,8 +621,13 @@ where
let drop_fn = tcx.associated_item_def_ids(drop_trait)[0];
let ty = self.place_ty(self.place);

let ref_ty =
tcx.mk_ref(tcx.lifetimes.re_erased, ty::TypeAndMut { ty, mutbl: hir::Mutability::Mut });
let ref_ty = tcx.mk_ref(
tcx.lifetimes.re_erased,
ty::TypeAndMut {
ty,
mutbl: hir::Mutability::Mut,
},
);
let ref_place = self.new_temp(ref_ty);
let unit_temp = Place::from(self.new_temp(tcx.mk_unit()));

Expand All @@ -594,7 +636,9 @@ where
Place::from(ref_place),
Rvalue::Ref(
tcx.lifetimes.re_erased,
BorrowKind::Mut { allow_two_phase_borrow: false },
BorrowKind::Mut {
allow_two_phase_borrow: false,
},
self.place,
),
)],
Expand Down Expand Up @@ -643,7 +687,10 @@ where
let move_ = |place: Place<'tcx>| Operand::Move(place);
let tcx = self.tcx();

let ptr_ty = tcx.mk_ptr(ty::TypeAndMut { ty: ety, mutbl: hir::Mutability::Mut });
let ptr_ty = tcx.mk_ptr(ty::TypeAndMut {
ty: ety,
mutbl: hir::Mutability::Mut,
});
let ptr = Place::from(self.new_temp(ptr_ty));
let can_go = Place::from(self.new_temp(tcx.types.bool));
let one = self.constant_usize(1);
Expand Down Expand Up @@ -671,7 +718,10 @@ where
let loop_block = BasicBlockData {
statements: vec![self.assign(
can_go,
Rvalue::BinaryOp(BinOp::Eq, Box::new((copy(Place::from(cur)), copy(len.into())))),
Rvalue::BinaryOp(
BinOp::Eq,
Box::new((copy(Place::from(cur)), copy(len.into()))),
),
)],
is_cleanup: unwind.is_cleanup(),
terminator: Some(Terminator {
Expand Down Expand Up @@ -768,8 +818,9 @@ where
let len = self.new_temp(tcx.types.usize);
let cur = self.new_temp(tcx.types.usize);

let unwind =
self.unwind.map(|unwind| self.drop_loop(unwind, cur, len, ety, Unwind::InCleanup));
let unwind = self
.unwind
.map(|unwind| self.drop_loop(unwind, cur, len, ety, Unwind::InCleanup));

let loop_block = self.drop_loop(self.succ, cur, len, ety, unwind);

Expand Down Expand Up @@ -860,8 +911,12 @@ where
return succ;
}
let block = self.new_block(unwind, TerminatorKind::Goto { target: succ });
let block_start = Location { block, statement_index: 0 };
self.elaborator.clear_drop_flag(block_start, self.path, mode);
let block_start = Location {
block,
statement_index: 0,
};
self.elaborator
.clear_drop_flag(block_start, self.path, mode);
block
}

Expand Down Expand Up @@ -926,8 +981,12 @@ where
}; // FIXME(#43234)
let free_block = self.new_block(unwind, call);

let block_start = Location { block: free_block, statement_index: 0 };
self.elaborator.clear_drop_flag(block_start, self.path, DropFlagMode::Shallow);
let block_start = Location {
block: free_block,
statement_index: 0,
};
self.elaborator
.clear_drop_flag(block_start, self.path, DropFlagMode::Shallow);
free_block
}

Expand Down Expand Up @@ -977,7 +1036,10 @@ where
fn new_block(&mut self, unwind: Unwind, k: TerminatorKind<'tcx>) -> BasicBlock {
self.elaborator.patch().new_block(BasicBlockData {
statements: vec![],
terminator: Some(Terminator { source_info: self.source_info, kind: k }),
terminator: Some(Terminator {
source_info: self.source_info,
kind: k,
}),
is_cleanup: unwind.is_cleanup(),
})
}
Expand All @@ -1000,4 +1062,4 @@ where
kind: StatementKind::Assign(Box::new((lhs, rhs))),
}
}
}
}
Loading

0 comments on commit fe877bd

Please sign in to comment.