Skip to content

Commit

Permalink
Refactoring and resolving clippy warnings
Browse files Browse the repository at this point in the history
  • Loading branch information
cedihegi committed Sep 6, 2023
1 parent de67aa4 commit 2fbeed9
Show file tree
Hide file tree
Showing 7 changed files with 40 additions and 88 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ use quote::ToTokens;
use rustc_hash::FxHashSet;
use syn::{self, parse_quote, parse_quote_spanned, spanned::Spanned, visit::Visit, BinOp};

type LoopBoundaries = ((String, syn::Type), syn::ExprRange);
pub(crate) struct BoundExtractor {
// the set of bound variables within that expression
pub name_set: FxHashSet<String>,
Expand All @@ -17,7 +18,7 @@ impl BoundExtractor {
pub(crate) fn manual_bounds(
expr: syn::ExprClosure,
bound_vars: Vec<(String, syn::Type)>,
) -> Option<syn::Result<Vec<((String, syn::Type), syn::ExprRange)>>> {
) -> Option<syn::Result<Vec<LoopBoundaries>>> {
let manual_bounds = get_attribute_contents(
"prusti :: runtime_quantifier_bounds".to_string(),
&expr.attrs,
Expand Down Expand Up @@ -61,7 +62,7 @@ impl BoundExtractor {
pub(crate) fn derive_ranges(
closure: syn::Expr,
args: Vec<(String, syn::Type)>,
) -> syn::Result<Vec<((String, syn::Type), syn::ExprRange)>> {
) -> syn::Result<Vec<LoopBoundaries>> {
if args.len() > 1 {
return Err(syn::Error::new(
closure.span(),
Expand Down
2 changes: 1 addition & 1 deletion prusti/src/callbacks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ pub(crate) fn mir_drops_elaborated(tcx: TyCtxt<'_>, def: LocalDefId) -> &Steal<m
let is_fn_like = tcx.def_kind(def).is_fn_like();
if is_fn_like {
// Do not compute the mir call graph without said call graph actually being used.
if inline::Inline.is_enabled(&tcx.sess) {
if inline::Inline.is_enabled(tcx.sess) {
tcx.ensure_with_value()
.mir_inliner_callees(ty::InstanceDef::Item(def.to_def_id()));
}
Expand Down
15 changes: 5 additions & 10 deletions prusti/src/modify_mir/mir_modify.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,20 +29,16 @@ pub(crate) fn insert_runtime_checks<'tcx>(
// we dont insert pledge checks for specification functions
if !is_spec_fn && !is_anon_const {
// insert pledge checks:
let mut pledge_inserter = passes::PledgeInserter::new(tcx, &mir_info, def_id, local_decls);
pledge_inserter.run(body);
passes::PledgeInserter::run(tcx, &mir_info, def_id, local_decls, body);
}

// insert a dummy goto block at the beginning of the body
prepend_dummy_block(body);
// insert preconditions
let mut precondition_inserter =
passes::PreconditionInserter::new(tcx, &mir_info, def_id, local_decls);
precondition_inserter.run(body);
passes::PreconditionInserter::run(tcx, &mir_info, def_id, local_decls, body);
// insert postconditions
let mut postcondition_inserter =
passes::PostconditionInserter::new(tcx, &mir_info, def_id, local_decls);
postcondition_inserter.run(body);
passes::PostconditionInserter::run(tcx, &mir_info, def_id, local_decls, body);

old_arg_replacer.clone_and_drop_variables(body);

// put specs and env back into globals
Expand All @@ -55,6 +51,5 @@ pub fn dead_code_elimination<'tcx>(tcx: TyCtxt<'tcx>, body: &mut mir::Body<'tcx>
if utils::has_spec_only_attr(attrs) {
return;
}
let mut remove_dead_blocks = passes::DeadCodeElimination::new(tcx, def_id);
remove_dead_blocks.run(body);
passes::DeadCodeElimination::run(tcx, def_id, body);
}
57 changes: 8 additions & 49 deletions prusti/src/modify_mir/passes/insert_pledge_checks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,6 @@ pub struct PledgeInserter<'tcx, 'a> {
body_info: &'a MirInfo<'tcx>,
patch_opt: Option<RefCell<MirPatch<'tcx>>>,
pledges_to_process: FxHashMap<mir::Place<'tcx>, PledgeToProcess<'tcx>>,
body_copy: Option<mir::Body<'tcx>>,
def_id: DefId,
local_decls: &'a IndexVec<mir::Local, mir::LocalDecl<'tcx>>,
/// For simplicity we use the same visitor twice, once to find all the
Expand Down Expand Up @@ -99,27 +98,26 @@ pub struct PledgeToProcess<'tcx> {
}

impl<'tcx, 'a> PledgeInserter<'tcx, 'a> {
pub fn new(
pub fn run(
tcx: TyCtxt<'tcx>,
body_info: &'a MirInfo<'tcx>,
def_id: DefId,
local_decls: &'a IndexVec<mir::Local, mir::LocalDecl<'tcx>>,
) -> Self {
Self {
body: &mut mir::Body<'tcx>,
) {
let mut inserter = Self {
tcx,
body_info,
patch_opt: None,
patch_opt: Some(MirPatch::new(body).into()),
pledges_to_process: Default::default(),
body_copy: None,
def_id,
local_decls,
first_pass: true,
}
};
inserter.modify(body);
}

pub fn run(&mut self, body: &mut mir::Body<'tcx>) {
self.body_copy = Some(body.clone());
self.patch_opt = Some(MirPatch::new(body).into());
fn modify(&mut self, body: &mut mir::Body<'tcx>) {
// find all calls to functions with pledges, and create local variables
// to store: old_values, before_expiry_place,
self.visit_body(body);
Expand Down Expand Up @@ -473,45 +471,6 @@ impl<'tcx, 'a> MutVisitor<'tcx> for PledgeInserter<'tcx, 'a> {
}
}
}
// mir::TerminatorKind::SwitchInt { targets, .. } => {
// // find switchInts with a check_only target.
// let switch_iter = targets.iter();
// if switch_iter.len() == 1 {
// // let (value, target) = switch_iter.next().unwrap();
// let otherwise = targets.otherwise();
// // check if target is a check_block:
// if let Some(kind) = self.body_info.check_blocks.get(&otherwise) {
// match kind {
// CheckBlockKind::PledgeExpires(local) => {
// // this check_block should terminate with a goto always!
// if let mir::TerminatorKind::Goto { ref target } =
// self.body_copy.as_ref().unwrap()[otherwise]
// .terminator
// .clone()
// .unwrap()
// .kind
// {
// let pledge = self.pledges_to_process.get(local).expect(
// "pledge expiration without an actual pledge,\
// seems like our assumption that calls of pledges are\
// always encountered before the expiration is wrong",
// );
// let start_block =
// self.create_pledge_call_chain(pledge, *target).unwrap();
//
// let new_terminator = mir::TerminatorKind::Goto {
// target: start_block,
// };
// // skip this check block and instead call checks-chain
// self.patcher().patch_terminator(otherwise, new_terminator);
// }
// }
// // nothing to do..
// CheckBlockKind::RuntimeAssertion => (),
// }
// }
// }
// }
}
}

Expand Down
21 changes: 9 additions & 12 deletions prusti/src/modify_mir/passes/insert_postconditions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,26 +18,23 @@ pub struct PostconditionInserter<'tcx, 'a> {
}

impl<'tcx, 'a> PostconditionInserter<'tcx, 'a> {
pub fn new(
pub fn run(
tcx: TyCtxt<'tcx>,
body_info: &'a MirInfo<'tcx>,
def_id: DefId,
local_decls: &'a IndexVec<mir::Local, mir::LocalDecl<'tcx>>,
) -> Self {
Self {
body: &mut mir::Body<'tcx>,
) {
let mut inserter = Self {
tcx,
body_info,
patch_opt: None,
patch_opt: Some(MirPatch::new(body).into()),
def_id,
local_decls,
}
}

pub fn run(&mut self, body: &mut mir::Body<'tcx>) {
let patch = MirPatch::new(body);
self.patch_opt = Some(patch.into());
self.visit_body(body);
let patch_ref = self.patch_opt.take().unwrap();
};
inserter.visit_body(body);
// apply the patch
let patch_ref = inserter.patch_opt.take().unwrap();
patch_ref.into_inner().apply(body);
}

Expand Down
13 changes: 8 additions & 5 deletions prusti/src/modify_mir/passes/insert_precondition_checks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,21 +24,24 @@ pub struct PreconditionInserter<'tcx, 'a> {
}

impl<'tcx, 'a> PreconditionInserter<'tcx, 'a> {
pub fn new(
pub fn run(
tcx: TyCtxt<'tcx>,
body_info: &'a MirInfo<'tcx>,
def_id: DefId,
local_decls: &'a IndexVec<mir::Local, mir::LocalDecl<'tcx>>,
) -> Self {
Self {
body: &mut mir::Body<'tcx>,
) {
let mut inserter = Self {
tcx,
body_info,
patch_opt: None,
def_id,
local_decls,
}
};
inserter.modify(body);
}
pub fn run(&mut self, body: &mut mir::Body<'tcx>) {

fn modify(&mut self, body: &mut mir::Body<'tcx>) {
let mut current_target = get_block_target(body, mir::START_BLOCK)
.expect("Bug: Body must start with a Goto block at this stage");
let patch = MirPatch::new(body);
Expand Down
15 changes: 6 additions & 9 deletions prusti/src/modify_mir/passes/remove_dead_code.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ pub struct DeadCodeElimination<'tcx> {
}

impl<'tcx> DeadCodeElimination<'tcx> {
pub fn new(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self {
pub fn run(tcx: TyCtxt<'tcx>, def_id: DefId, body: &mut mir::Body<'tcx>) {
// collect all the blocks that were inserted but didnt generate
// a verification error:
let reachability_map = globals::get_reachability_map(def_id).unwrap_or_default();
Expand All @@ -36,19 +36,16 @@ impl<'tcx> DeadCodeElimination<'tcx> {
.iter()
.filter_map(|(bb, verified)| verified.then_some(*bb))
.collect();
Self {
let mut modifier = Self {
tcx,
unreachable_blocks,
removable_assertions,
}
}

pub fn run(&mut self, body: &mut mir::Body<'tcx>) {
self.remove_assertions(body);
if self.unreachable_blocks.is_empty() {
};
modifier.remove_assertions(body);
if modifier.unreachable_blocks.is_empty() {
return;
}
self.visit_body(body);
modifier.visit_body(body);
}

fn remove_assertions(&self, body: &mut mir::Body<'tcx>) {
Expand Down

0 comments on commit 2fbeed9

Please sign in to comment.