From fe877bde7f40e69f9caa66e04e2a530def6579c8 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Fri, 30 Jun 2023 10:55:50 +0200 Subject: [PATCH] Format code --- Cargo.lock | 2 +- .../environment/mir_body/patch/compiler.rs | 22 ++- .../encoder/elaborate_drops/mir_dataflow.rs | 126 +++++++++++++----- .../encoder/elaborate_drops/mir_transform.rs | 121 ++++++++++++----- .../src/encoder/mir/types/const_parameters.rs | 2 +- .../src/encoder/mir/types/interface.rs | 8 +- .../src/encoder/mir/types/lifetimes.rs | 2 +- prusti/src/callbacks.rs | 9 +- 8 files changed, 207 insertions(+), 85 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 1b70fb2d4f3..0ab3c6c8738 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2158,7 +2158,7 @@ dependencies = [ [[package]] name = "prusti-specs" -version = "0.1.7" +version = "0.1.8" dependencies = [ "itertools", "proc-macro2", diff --git a/prusti-interface/src/environment/mir_body/patch/compiler.rs b/prusti-interface/src/environment/mir_body/patch/compiler.rs index e50058a2a63..ca85b91fdb5 100644 --- a/prusti-interface/src/environment/mir_body/patch/compiler.rs +++ b/prusti-interface/src/environment/mir_body/patch/compiler.rs @@ -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( @@ -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; } } @@ -248,4 +258,4 @@ impl<'tcx> MirPatch<'tcx> { }; Self::source_info_for_index(data, loc) } -} \ No newline at end of file +} diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs index 3382dc2a01b..27b5c694604 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs @@ -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, @@ -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; @@ -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> @@ -299,10 +307,16 @@ where fields: &[(Place<'tcx>, Option)], ) -> Vec { 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() } @@ -310,7 +324,10 @@ where // 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 @@ -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); @@ -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 { @@ -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) } @@ -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; @@ -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)); } } @@ -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())); @@ -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, ), )], @@ -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); @@ -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 { @@ -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); @@ -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 } @@ -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 } @@ -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(), }) } @@ -1000,4 +1062,4 @@ where kind: StatementKind::Assign(Box::new((lhs, rhs))), } } -} \ No newline at end of file +} diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs index ef03c0f0ac5..0a59eb3defc 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs @@ -76,9 +76,15 @@ pub(in super::super) fn run_pass<'tcx>(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>) (Default::default(), move_data) } }; - let un_derefer = UnDerefer { tcx: tcx, derefer_sidetable: side_table }; + let un_derefer = UnDerefer { + tcx: tcx, + derefer_sidetable: side_table, + }; let elaborate_patch = { - let env = MoveDataParamEnv { move_data, param_env }; + let env = MoveDataParamEnv { + move_data, + param_env, + }; remove_dead_unwinds(tcx, body, &env, &un_derefer); let inits = MaybeInitializedPlaces::new(tcx, body, &env) @@ -131,9 +137,11 @@ pub(in super::super) fn remove_dead_unwinds<'tcx>( .into_results_cursor(body); for (bb, bb_data) in body.basic_blocks.iter_enumerated() { let place = match bb_data.terminator().kind { - TerminatorKind::Drop { ref place, unwind: UnwindAction::Cleanup(_), .. } => { - und.derefer(place.as_ref(), body).unwrap_or(*place) - } + TerminatorKind::Drop { + ref place, + unwind: UnwindAction::Cleanup(_), + .. + } => und.derefer(place.as_ref(), body).unwrap_or(*place), _ => continue, }; @@ -264,34 +272,55 @@ impl<'a, 'tcx> DropElaborator<'a, 'tcx> for Elaborator<'a, '_, 'tcx> { } fn field_subpath(&self, path: Self::Path, field: FieldIdx) -> Option { - prusti_rustc_interface::dataflow::move_path_children_matching(self.ctxt.move_data(), path, |e| match e { - ProjectionElem::Field(idx, _) => idx == field, - _ => false, - }) + prusti_rustc_interface::dataflow::move_path_children_matching( + self.ctxt.move_data(), + path, + |e| match e { + ProjectionElem::Field(idx, _) => idx == field, + _ => false, + }, + ) } fn array_subpath(&self, path: Self::Path, index: u64, size: u64) -> Option { - prusti_rustc_interface::dataflow::move_path_children_matching(self.ctxt.move_data(), path, |e| match e { - ProjectionElem::ConstantIndex { offset, min_length, from_end } => { - debug_assert!(size == min_length, "min_length should be exact for arrays"); - assert!(!from_end, "from_end should not be used for array element ConstantIndex"); - offset == index - } - _ => false, - }) + prusti_rustc_interface::dataflow::move_path_children_matching( + self.ctxt.move_data(), + path, + |e| match e { + ProjectionElem::ConstantIndex { + offset, + min_length, + from_end, + } => { + debug_assert!(size == min_length, "min_length should be exact for arrays"); + assert!( + !from_end, + "from_end should not be used for array element ConstantIndex" + ); + offset == index + } + _ => false, + }, + ) } fn deref_subpath(&self, path: Self::Path) -> Option { - prusti_rustc_interface::dataflow::move_path_children_matching(self.ctxt.move_data(), path, |e| { - e == ProjectionElem::Deref - }) + prusti_rustc_interface::dataflow::move_path_children_matching( + self.ctxt.move_data(), + path, + |e| e == ProjectionElem::Deref, + ) } fn downcast_subpath(&self, path: Self::Path, variant: VariantIdx) -> Option { - prusti_rustc_interface::dataflow::move_path_children_matching(self.ctxt.move_data(), path, |e| match e { - ProjectionElem::Downcast(_, idx) => idx == variant, - _ => false, - }) + prusti_rustc_interface::dataflow::move_path_children_matching( + self.ctxt.move_data(), + path, + |e| match e { + ProjectionElem::Downcast(_, idx) => idx == variant, + _ => false, + }, + ) } fn get_drop_flag(&mut self, path: Self::Path) -> Option> { @@ -352,16 +381,20 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> { } let terminator = data.terminator(); let place = match terminator.kind { - TerminatorKind::Drop { ref place, .. } => { - self.un_derefer.derefer(place.as_ref(), self.body).unwrap_or(*place) - } + TerminatorKind::Drop { ref place, .. } => self + .un_derefer + .derefer(place.as_ref(), self.body) + .unwrap_or(*place), _ => continue, }; self.init_data.seek_before(self.body.terminator_loc(bb)); let path = self.move_data().rev_lookup.find(place.as_ref()); - debug!("collect_drop_flags: {:?}, place {:?} ({:?})", bb, place, path); + debug!( + "collect_drop_flags: {:?}, place {:?} ({:?})", + bb, place, path + ); let path = match path { LookupResult::Exact(e) => e, @@ -407,11 +440,19 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> { if !self.reachable.contains(bb) { continue; } - let loc = Location { block: bb, statement_index: data.statements.len() }; + let loc = Location { + block: bb, + statement_index: data.statements.len(), + }; let terminator = data.terminator(); match terminator.kind { - TerminatorKind::Drop { mut place, target, unwind, replace } => { + TerminatorKind::Drop { + mut place, + target, + unwind, + replace, + } => { if let Some(new_place) = self.un_derefer.derefer(place.as_ref(), self.body) { place = new_place; } @@ -483,7 +524,8 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> { let span = self.patch.source_info_for_location(self.body, loc).span; let false_ = self.constant_bool(span, false); for flag in self.drop_flags.iter().flatten() { - self.patch.add_assign(loc, Place::from(*flag), false_.clone()); + self.patch + .add_assign(loc, Place::from(*flag), false_.clone()); } } @@ -501,7 +543,10 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> { { assert!(!self.patch.is_patched(bb)); - let loc = Location { block: tgt, statement_index: 0 }; + let loc = Location { + block: tgt, + statement_index: 0, + }; let path = self.move_data().rev_lookup.find(destination.as_ref()); on_lookup_result_bits(self.tcx, self.body, self.move_data(), path, |child| { self.set_drop_flag(loc, child, DropFlagState::Present) @@ -552,7 +597,10 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> { } } } - let loc = Location { block: bb, statement_index: i }; + let loc = Location { + block: bb, + statement_index: i, + }; prusti_rustc_interface::dataflow::drop_flag_effects_for_location( self.tcx, self.body, @@ -574,7 +622,10 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> { { assert!(!self.patch.is_patched(bb)); - let loc = Location { block: bb, statement_index: data.statements.len() }; + let loc = Location { + block: bb, + statement_index: data.statements.len(), + }; let path = self.move_data().rev_lookup.find(destination.as_ref()); on_lookup_result_bits(self.tcx, self.body, self.move_data(), path, |child| { self.set_drop_flag(loc, child, DropFlagState::Present) @@ -582,4 +633,4 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> { } } } -} \ No newline at end of file +} diff --git a/prusti-viper/src/encoder/mir/types/const_parameters.rs b/prusti-viper/src/encoder/mir/types/const_parameters.rs index a5de58e73d9..e472c9132a8 100644 --- a/prusti-viper/src/encoder/mir/types/const_parameters.rs +++ b/prusti-viper/src/encoder/mir/types/const_parameters.rs @@ -19,7 +19,7 @@ pub(super) fn extract_const_parameters_from_substs<'tcx>( pub(super) fn extract_const_parameters_from_types<'tcx>( type_encoder: &impl super::MirTypeEncoderInterface<'tcx>, - types: impl IntoIterator>, + types: impl IntoIterator>, const_parameters: &mut Vec, ) -> SpannedEncodingResult<()> { for ty in types { diff --git a/prusti-viper/src/encoder/mir/types/interface.rs b/prusti-viper/src/encoder/mir/types/interface.rs index e81e377755d..28ca979996a 100644 --- a/prusti-viper/src/encoder/mir/types/interface.rs +++ b/prusti-viper/src/encoder/mir/types/interface.rs @@ -41,7 +41,7 @@ pub(crate) trait MirTypeEncoderInterface<'tcx> { fn encode_value_field_high(&self, ty: ty::Ty<'tcx>) -> EncodingResult; fn get_lifetimes_from_types( &self, - types: impl IntoIterator>, + types: impl IntoIterator>, ) -> SpannedEncodingResult>; fn get_lifetimes_from_substs( &self, @@ -53,7 +53,7 @@ pub(crate) trait MirTypeEncoderInterface<'tcx> { ) -> SpannedEncodingResult>; fn get_const_parameters_from_types( &self, - types: impl IntoIterator>, + types: impl IntoIterator>, ) -> SpannedEncodingResult>; fn get_lifetimes_from_type_high( &self, @@ -193,7 +193,7 @@ impl<'v, 'tcx: 'v> MirTypeEncoderInterface<'tcx> for super::super::super::Encode } fn get_lifetimes_from_types( &self, - types: impl IntoIterator>, + types: impl IntoIterator>, ) -> SpannedEncodingResult> { let mut lifetimes = Vec::new(); super::lifetimes::extract_lifetimes_from_types(self, types, &mut lifetimes)?; @@ -213,7 +213,7 @@ impl<'v, 'tcx: 'v> MirTypeEncoderInterface<'tcx> for super::super::super::Encode } fn get_const_parameters_from_types( &self, - types: impl IntoIterator>, + types: impl IntoIterator>, ) -> SpannedEncodingResult> { let mut const_parameters = Vec::new(); super::const_parameters::extract_const_parameters_from_types( diff --git a/prusti-viper/src/encoder/mir/types/lifetimes.rs b/prusti-viper/src/encoder/mir/types/lifetimes.rs index 9d6799ac827..f53b1762fa3 100644 --- a/prusti-viper/src/encoder/mir/types/lifetimes.rs +++ b/prusti-viper/src/encoder/mir/types/lifetimes.rs @@ -27,7 +27,7 @@ pub(super) fn extract_lifetimes_from_substs<'tcx>( pub(super) fn extract_lifetimes_from_types<'tcx>( type_encoder: &impl super::MirTypeEncoderInterface<'tcx>, - types: impl IntoIterator>, + types: impl IntoIterator>, lifetimes: &mut Vec, ) -> SpannedEncodingResult<()> { for ty in types { diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index 251f79d5da2..2e89981581e 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -9,12 +9,11 @@ use prusti_rustc_interface::{ driver::Compilation, hir::{def::DefKind, def_id::LocalDefId}, interface::{interface::Compiler, Config, Queries}, - middle::ty::{ - self, - TyCtxt, + middle::{ + mir::BorrowCheckResult, + query::{ExternProviders, Providers}, + ty::{self, TyCtxt}, }, - middle::mir::BorrowCheckResult, - middle::query::{ExternProviders, Providers}, session::Session, };