diff --git a/prusti-contracts/prusti-specs/src/runtime_checks/boundary_extraction.rs b/prusti-contracts/prusti-specs/src/runtime_checks/boundary_extraction.rs index 998d1f95d34..c05e65930f6 100644 --- a/prusti-contracts/prusti-specs/src/runtime_checks/boundary_extraction.rs +++ b/prusti-contracts/prusti-specs/src/runtime_checks/boundary_extraction.rs @@ -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, @@ -17,7 +18,7 @@ impl BoundExtractor { pub(crate) fn manual_bounds( expr: syn::ExprClosure, bound_vars: Vec<(String, syn::Type)>, - ) -> Option>> { + ) -> Option>> { let manual_bounds = get_attribute_contents( "prusti :: runtime_quantifier_bounds".to_string(), &expr.attrs, @@ -61,7 +62,7 @@ impl BoundExtractor { pub(crate) fn derive_ranges( closure: syn::Expr, args: Vec<(String, syn::Type)>, - ) -> syn::Result> { + ) -> syn::Result> { if args.len() > 1 { return Err(syn::Error::new( closure.span(), diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index 95315327847..190406bbcd2 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -115,7 +115,7 @@ pub(crate) fn mir_drops_elaborated(tcx: TyCtxt<'_>, def: LocalDefId) -> &Steal( // 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 @@ -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); } diff --git a/prusti/src/modify_mir/passes/insert_pledge_checks.rs b/prusti/src/modify_mir/passes/insert_pledge_checks.rs index 258c1000bd9..1f8dd275904 100644 --- a/prusti/src/modify_mir/passes/insert_pledge_checks.rs +++ b/prusti/src/modify_mir/passes/insert_pledge_checks.rs @@ -27,7 +27,6 @@ pub struct PledgeInserter<'tcx, 'a> { body_info: &'a MirInfo<'tcx>, patch_opt: Option>>, pledges_to_process: FxHashMap, PledgeToProcess<'tcx>>, - body_copy: Option>, def_id: DefId, local_decls: &'a IndexVec>, /// For simplicity we use the same visitor twice, once to find all the @@ -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>, - ) -> 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); @@ -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 => (), - // } - // } - // } - // } } } diff --git a/prusti/src/modify_mir/passes/insert_postconditions.rs b/prusti/src/modify_mir/passes/insert_postconditions.rs index 8a7e18d1885..3dfdb2c0c47 100644 --- a/prusti/src/modify_mir/passes/insert_postconditions.rs +++ b/prusti/src/modify_mir/passes/insert_postconditions.rs @@ -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>, - ) -> 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); } diff --git a/prusti/src/modify_mir/passes/insert_precondition_checks.rs b/prusti/src/modify_mir/passes/insert_precondition_checks.rs index dea8271bcd3..6551b41715b 100644 --- a/prusti/src/modify_mir/passes/insert_precondition_checks.rs +++ b/prusti/src/modify_mir/passes/insert_precondition_checks.rs @@ -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>, - ) -> 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); diff --git a/prusti/src/modify_mir/passes/remove_dead_code.rs b/prusti/src/modify_mir/passes/remove_dead_code.rs index 62bf1505329..892d5cc8259 100644 --- a/prusti/src/modify_mir/passes/remove_dead_code.rs +++ b/prusti/src/modify_mir/passes/remove_dead_code.rs @@ -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(); @@ -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>) {