From 08f4aafeb806d26a250aa98ab4ab4622399c1922 Mon Sep 17 00:00:00 2001 From: Vytautas Astrauskas Date: Thu, 29 Jun 2023 22:06:18 +0200 Subject: [PATCH] Try to make Prusti compile. --- Cargo.toml | 1 + prusti-contracts/Cargo.toml | 1 + prusti-interface/src/environment/body.rs | 11 +- .../environment/mir_body/patch/compiler.rs | 165 +++++++++++------- prusti-interface/src/lib.rs | 1 + .../encoder/elaborate_drops/mir_dataflow.rs | 138 ++++++++++----- .../encoder/elaborate_drops/mir_transform.rs | 5 +- .../src/encoder/mir/procedures/encoder/mod.rs | 17 +- .../mir/pure/interpreter/interpreter_high.rs | 12 +- .../src/encoder/mir/types/const_parameters.rs | 16 +- prusti-viper/src/encoder/mir/types/encoder.rs | 9 +- .../src/encoder/mir/types/interface.rs | 28 +++ .../src/encoder/mir/types/lifetimes.rs | 16 +- prusti-viper/src/encoder/procedure_encoder.rs | 10 +- prusti-viper/src/utils/mod.rs | 1 + prusti/src/callbacks.rs | 5 +- prusti/src/driver.rs | 6 +- 17 files changed, 299 insertions(+), 143 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 35b669b8d23..fd6efd1f9dc 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -25,6 +25,7 @@ members = [ exclude = [ "docs/dummy" ] +resolver = "2" [profile.dev] debug = 1 diff --git a/prusti-contracts/Cargo.toml b/prusti-contracts/Cargo.toml index 2c8254cd48f..de39952ddb5 100644 --- a/prusti-contracts/Cargo.toml +++ b/prusti-contracts/Cargo.toml @@ -5,6 +5,7 @@ members = [ "prusti-specs", "prusti-std", ] +resolver = "2" # This should not be built as part of Prusti (instead being build by `prusti-contracts-build`) # It would require setting the `build.rustc-wrapper` in a `../.cargo/config.toml` correctly diff --git a/prusti-interface/src/environment/body.rs b/prusti-interface/src/environment/body.rs index df7f061ad71..b1ef2ca764e 100644 --- a/prusti-interface/src/environment/body.rs +++ b/prusti-interface/src/environment/body.rs @@ -168,12 +168,11 @@ impl<'tcx> EnvBody<'tcx> { { let monomorphised = if let Some(caller_def_id) = caller_def_id { let param_env = self.tcx.param_env(caller_def_id); - self.tcx - .subst_and_normalize_erasing_regions( - substs, - param_env, - ty::EarlyBinder::bind(body.0), - ) + self.tcx.subst_and_normalize_erasing_regions( + substs, + param_env, + ty::EarlyBinder::bind(body.0), + ) } else { ty::EarlyBinder::bind(body.0).subst(self.tcx, substs) }; diff --git a/prusti-interface/src/environment/mir_body/patch/compiler.rs b/prusti-interface/src/environment/mir_body/patch/compiler.rs index 085e5afc8f4..e50058a2a63 100644 --- a/prusti-interface/src/environment/mir_body/patch/compiler.rs +++ b/prusti-interface/src/environment/mir_body/patch/compiler.rs @@ -26,7 +26,11 @@ pub struct MirPatch<'tcx> { pub new_blocks: Vec>, pub new_statements: Vec<(Location, StatementKind<'tcx>)>, pub new_locals: Vec>, - pub resume_block: BasicBlock, + pub resume_block: Option, + // Only for unreachable in cleanup path. + pub unreachable_cleanup_block: Option, + pub terminate_block: Option, + pub body_span: Span, pub next_local: usize, } @@ -38,51 +42,87 @@ impl<'tcx> MirPatch<'tcx> { new_statements: vec![], new_locals: vec![], next_local: body.local_decls.len(), - resume_block: START_BLOCK, + resume_block: None, + unreachable_cleanup_block: None, + terminate_block: None, + body_span: body.span, }; - // make sure the MIR we create has a resume block. It is - // completely legal to convert jumps to the resume block - // to jumps to None, but we occasionally have to add - // instructions just before that. - - let mut resume_block = None; - let mut resume_stmt_block = None; for (bb, block) in body.basic_blocks.iter_enumerated() { - if let TerminatorKind::Resume = block.terminator().kind { - if !block.statements.is_empty() { - assert!(resume_stmt_block.is_none()); - resume_stmt_block = Some(bb); - } else { - resume_block = Some(bb); - } - break; + // Check if we already have a resume block + if let TerminatorKind::Resume = block.terminator().kind && block.statements.is_empty() { + result.resume_block = Some(bb); + continue; + } + + // Check if we already have an unreachable block + if let TerminatorKind::Unreachable = block.terminator().kind + && block.statements.is_empty() + && block.is_cleanup + { + result.unreachable_cleanup_block = Some(bb); + continue; } + + // Check if we already have a terminate block + if let TerminatorKind::Terminate = block.terminator().kind && block.statements.is_empty() { + result.terminate_block = Some(bb); + continue; + } + } + + result + } + + pub fn resume_block(&mut self) -> BasicBlock { + if let Some(bb) = self.resume_block { + return bb; } - let resume_block = resume_block.unwrap_or_else(|| { - result.new_block(BasicBlockData { - statements: vec![], - terminator: Some(Terminator { - source_info: SourceInfo::outermost(body.span), - kind: TerminatorKind::Resume, - }), - is_cleanup: true, - }) + + let bb = self.new_block(BasicBlockData { + statements: vec![], + terminator: Some(Terminator { + source_info: SourceInfo::outermost(self.body_span), + kind: TerminatorKind::Resume, + }), + is_cleanup: true, }); - result.resume_block = resume_block; - if let Some(resume_stmt_block) = resume_stmt_block { - result.patch_terminator( - resume_stmt_block, - TerminatorKind::Goto { - target: resume_block, - }, - ); + self.resume_block = Some(bb); + bb + } + + pub fn unreachable_cleanup_block(&mut self) -> BasicBlock { + if let Some(bb) = self.unreachable_cleanup_block { + return bb; } - result + + let bb = self.new_block(BasicBlockData { + statements: vec![], + terminator: Some(Terminator { + source_info: SourceInfo::outermost(self.body_span), + kind: TerminatorKind::Unreachable, + }), + is_cleanup: true, + }); + self.unreachable_cleanup_block = Some(bb); + bb } - pub fn resume_block(&self) -> BasicBlock { - self.resume_block + pub fn terminate_block(&mut self) -> BasicBlock { + if let Some(bb) = self.terminate_block { + return bb; + } + + let bb = self.new_block(BasicBlockData { + statements: vec![], + terminator: Some(Terminator { + source_info: SourceInfo::outermost(self.body_span), + kind: TerminatorKind::Terminate, + }), + is_cleanup: true, + }); + self.terminate_block = Some(bb); + bb } pub fn is_patched(&self, bb: BasicBlock) -> bool { @@ -94,10 +134,21 @@ 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( + &mut self, + ty: Ty<'tcx>, + span: Span, + local_info: LocalInfo<'tcx>, + ) -> Local { + let index = self.next_local; + self.next_local += 1; + let mut new_decl = LocalDecl::new(ty, span).internal(); + **new_decl.local_info.as_mut().assert_crate_local() = local_info; + self.new_locals.push(new_decl); + Local::new(index) } pub fn new_temp(&mut self, ty: Ty<'tcx>, span: Span) -> Local { @@ -114,7 +165,6 @@ impl<'tcx> MirPatch<'tcx> { Local::new(index) } - #[tracing::instrument(level = "debug", skip(self))] pub fn new_block(&mut self, data: BasicBlockData<'tcx>) -> BasicBlock { let block = BasicBlock::new(self.patch_map.len()); debug!("MirPatch: new_block: {:?}: {:?}", block, data); @@ -123,14 +173,14 @@ impl<'tcx> MirPatch<'tcx> { block } - #[tracing::instrument(level = "debug", skip(self))] pub fn patch_terminator(&mut self, block: BasicBlock, new: TerminatorKind<'tcx>) { assert!(self.patch_map[block].is_none()); + debug!("MirPatch: patch_terminator({:?}, {:?})", block, new); self.patch_map[block] = Some(new); } - #[tracing::instrument(level = "debug", skip(self))] pub fn add_statement(&mut self, loc: Location, stmt: StatementKind<'tcx>) { + debug!("MirPatch: add_statement({:?}, {:?})", loc, stmt); self.new_statements.push((loc, stmt)); } @@ -138,7 +188,6 @@ impl<'tcx> MirPatch<'tcx> { self.add_statement(loc, StatementKind::Assign(Box::new((place, rv)))); } - #[tracing::instrument(level = "debug", skip_all)] pub fn apply(self, body: &mut Body<'tcx>) { debug!( "MirPatch: {:?} new temps, starting from index {}: {:?}", @@ -151,12 +200,17 @@ impl<'tcx> MirPatch<'tcx> { self.new_blocks.len(), body.basic_blocks.len() ); - body.basic_blocks_mut().extend(self.new_blocks); + let bbs = if self.patch_map.is_empty() && self.new_blocks.is_empty() { + body.basic_blocks.as_mut_preserves_cfg() + } else { + body.basic_blocks.as_mut() + }; + bbs.extend(self.new_blocks); body.local_decls.extend(self.new_locals); for (src, patch) in self.patch_map.into_iter_enumerated() { if let Some(patch) = patch { debug!("MirPatch: patching block {:?}", src); - body[src].terminator_mut().kind = patch; + bbs[src].terminator_mut().kind = patch; } } @@ -170,19 +224,12 @@ 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; } } @@ -201,4 +248,4 @@ impl<'tcx> MirPatch<'tcx> { }; Self::source_info_for_index(data, loc) } -} +} \ No newline at end of file diff --git a/prusti-interface/src/lib.rs b/prusti-interface/src/lib.rs index 0b077ce0921..d1b7bdaf632 100644 --- a/prusti-interface/src/lib.rs +++ b/prusti-interface/src/lib.rs @@ -13,6 +13,7 @@ #![feature(box_patterns)] #![feature(control_flow_enum)] #![feature(min_specialization)] +#![feature(let_chains)] // We may want to remove this in the future. #![allow(clippy::needless_lifetimes)] 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 033160d81c5..3382dc2a01b 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 @@ -14,8 +14,8 @@ use log::debug; use prusti_interface::environment::mir_body::patch::MirPatch; use prusti_rustc_interface::{ - abi::{FIRST_VARIANT, FieldIdx}, - dataflow::elaborate_drops::{DropFlagMode, DropStyle, Unwind}, + abi::{FieldIdx, VariantIdx, FIRST_VARIANT}, + dataflow::elaborate_drops::{DropFlagState, DropFlagMode, DropStyle, Unwind}, hir, hir::lang_items::LangItem, index::Idx, @@ -24,8 +24,8 @@ use prusti_rustc_interface::{ traits::Reveal, ty::{self, subst::SubstsRef, util::IntTypeExt, Ty, TyCtxt}, }, - target::abi::VariantIdx, }; +use tracing::instrument; use std::{fmt, iter}; trait UnwindPublic { @@ -187,8 +187,8 @@ where // // FIXME: I think we should just control the flags externally, // and then we do not need this machinery. - #[tracing::instrument(level = "debug")] pub fn elaborate_drop(&mut self, bb: BasicBlock) { + debug!("elaborate_drop({:?}, {:?})", bb, self); let style = self.elaborator.drop_style(self.path, DropFlagMode::Deep); debug!("elaborate_drop({:?}, {:?}): live - {:?}", bb, self, style); match style { @@ -250,7 +250,6 @@ where .collect() } - #[tracing::instrument(level = "debug")] fn drop_subpath( &mut self, place: Place<'tcx>, @@ -331,13 +330,14 @@ where /// /// NOTE: this does not clear the master drop flag, so you need /// to point succ/unwind on a `drop_ladder_bottom`. - #[tracing::instrument(level = "debug")] fn drop_ladder( &mut self, fields: Vec<(Place<'tcx>, Option)>, succ: BasicBlock, unwind: Unwind, ) -> (BasicBlock, Unwind) { + debug!("drop_ladder({:?}, {:?})", self, fields); + let mut fields = fields; fields.retain(|&(place, _)| { self.place_ty(place).needs_drop(self.tcx(), self.elaborator.param_env()) @@ -358,8 +358,9 @@ where (*normal_ladder.last().unwrap(), *unwind_ladder.last().unwrap()) } - #[tracing::instrument(level = "debug")] fn open_drop_for_tuple(&mut self, tys: &[Ty<'tcx>]) -> BasicBlock { + debug!("open_drop_for_tuple({:?}, {:?})", self, tys); + let fields = tys .iter() .enumerate() @@ -375,15 +376,8 @@ where self.drop_ladder(fields, succ, unwind).0 } - /// Drops the T contained in a `Box` if it has not been moved out of - #[tracing::instrument(level = "debug")] - fn open_drop_for_box_contents( - &mut self, - adt: ty::AdtDef<'tcx>, - substs: SubstsRef<'tcx>, - succ: BasicBlock, - unwind: Unwind, - ) -> BasicBlock { + #[instrument(level = "debug", ret)] + fn open_drop_for_box(&mut self, adt: ty::AdtDef<'tcx>, substs: SubstsRef<'tcx>) -> BasicBlock { // drop glue is sent straight to codegen // box cannot be directly dereferenced let unique_ty = adt.non_enum_variant().fields[FieldIdx::new(0)].ty(self.tcx(), substs); @@ -398,10 +392,14 @@ where let interior_path = self.elaborator.deref_subpath(self.path); - self.drop_subpath(interior, interior_path, succ, unwind) + 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)); + + self.drop_subpath(interior, interior_path, succ, unwind_succ) } - #[tracing::instrument(level = "debug")] + #[instrument(level = "debug", ret)] fn open_drop_for_adt(&mut self, adt: ty::AdtDef<'tcx>, substs: SubstsRef<'tcx>) -> BasicBlock { if adt.variants().is_empty() { return self.elaborator.patch().new_block(BasicBlockData { @@ -422,15 +420,7 @@ where self.open_drop_for_adt_contents(adt, substs) }; - if adt.is_box() { - // we need to drop the inside of the box before running the destructor - let succ = self.destructor_call_block(contents_drop); - let unwind = contents_drop - .1 - .map(|unwind| self.destructor_call_block((unwind, Unwind::InCleanup))); - - self.open_drop_for_box_contents(adt, substs, succ, unwind) - } else if adt.has_dtor(self.tcx()) { + if adt.has_dtor(self.tcx()) { self.destructor_call_block(contents_drop) } else { contents_drop.0 @@ -604,7 +594,7 @@ where Place::from(ref_place), Rvalue::Ref( tcx.lifetimes.re_erased, - BorrowKind::Mut { kind: MutBorrowKind::Default }, + BorrowKind::Mut { allow_two_phase_borrow: false }, self.place, ), )], @@ -620,20 +610,14 @@ where destination: unit_temp, target: Some(succ), unwind: unwind.into_action(), - call_source: CallSource::Misc, + from_hir_call: true, fn_span: self.source_info.span, }, source_info: self.source_info, }), is_cleanup: unwind.is_cleanup(), }; - - let destructor_block = self.elaborator.patch().new_block(result); - - let block_start = Location { block: destructor_block, statement_index: 0 }; - self.elaborator.clear_drop_flag(block_start, self.path, DropFlagMode::Shallow); - - self.drop_flag_test_block(destructor_block, succ, unwind) + self.elaborator.patch().new_block(result) } /// Create a loop that drops an array: @@ -710,8 +694,8 @@ where loop_block } - #[tracing::instrument(level = "debug")] fn open_drop_for_array(&mut self, ety: Ty<'tcx>, opt_size: Option) -> BasicBlock { + debug!("open_drop_for_array({:?}, {:?})", ety, opt_size); let tcx = self.tcx(); if let Some(size) = opt_size { @@ -778,8 +762,8 @@ where /// Creates a pair of drop-loops of `place`, which drops its contents, even /// in the case of 1 panic. - #[tracing::instrument(level = "debug")] fn drop_loop_pair(&mut self, ety: Ty<'tcx>) -> BasicBlock { + debug!("drop_loop_pair({:?})", ety); let tcx = self.tcx(); let len = self.new_temp(tcx.types.usize); let cur = self.new_temp(tcx.types.usize); @@ -834,7 +818,13 @@ where self.open_drop_for_tuple(&tys) } ty::Tuple(fields) => self.open_drop_for_tuple(fields), - ty::Adt(def, substs) => self.open_drop_for_adt(*def, substs), + ty::Adt(def, substs) => { + if def.is_box() { + self.open_drop_for_box(*def, substs) + } else { + self.open_drop_for_adt(*def, substs) + } + } ty::Dynamic(..) => self.complete_drop(self.succ, self.unwind), ty::Array(ety, size) => { let size = size.try_eval_target_usize(self.tcx(), self.elaborator.param_env()); @@ -846,8 +836,9 @@ where } } - #[tracing::instrument(level = "debug")] fn complete_drop(&mut self, succ: BasicBlock, unwind: Unwind) -> BasicBlock { + debug!("complete_drop(succ={:?}, unwind={:?})", succ, unwind); + let drop_block = self.drop_block(succ, unwind); self.drop_flag_test_block(drop_block, succ, unwind) @@ -855,13 +846,14 @@ where /// Creates a block that resets the drop flag. If `mode` is deep, all children drop flags will /// also be cleared. - #[tracing::instrument(level = "debug")] fn drop_flag_reset_block( &mut self, mode: DropFlagMode, succ: BasicBlock, unwind: Unwind, ) -> BasicBlock { + debug!("drop_flag_reset_block({:?},{:?})", self, mode); + if unwind.is_cleanup() { // The drop flag isn't read again on the unwind path, so don't // bother setting it. @@ -873,13 +865,72 @@ where block } - #[tracing::instrument(level = "debug")] fn elaborated_drop_block(&mut self) -> BasicBlock { + debug!("elaborated_drop_block({:?})", self); let blk = self.drop_block(self.succ, self.unwind); self.elaborate_drop(blk); blk } + /// Creates a block that frees the backing memory of a `Box` if its drop is required (either + /// statically or by checking its drop flag). + /// + /// The contained value will not be dropped. + fn box_free_block( + &mut self, + adt: ty::AdtDef<'tcx>, + substs: SubstsRef<'tcx>, + target: BasicBlock, + unwind: Unwind, + ) -> BasicBlock { + let block = self.unelaborated_free_block(adt, substs, target, unwind); + self.drop_flag_test_block(block, target, unwind) + } + + /// Creates a block that frees the backing memory of a `Box` (without dropping the contained + /// value). + fn unelaborated_free_block( + &mut self, + adt: ty::AdtDef<'tcx>, + substs: SubstsRef<'tcx>, + target: BasicBlock, + unwind: Unwind, + ) -> BasicBlock { + let tcx = self.tcx(); + let unit_temp = Place::from(self.new_temp(tcx.mk_unit())); + let free_func = tcx.require_lang_item(LangItem::BoxFree, Some(self.source_info.span)); + let args = adt + .variant(FIRST_VARIANT) + .fields + .iter() + .enumerate() + .map(|(i, f)| { + let field = FieldIdx::new(i); + let field_ty = f.ty(tcx, substs); + Operand::Move(tcx.mk_place_field(self.place, field, field_ty)) + }) + .collect(); + + let call = TerminatorKind::Call { + func: Operand::function_handle(tcx, free_func, substs, self.source_info.span), + args, + destination: unit_temp, + target: Some(target), + unwind: if unwind.is_cleanup() { + UnwindAction::Terminate + } else { + UnwindAction::Continue + }, + from_hir_call: false, + fn_span: self.source_info.span, + }; // 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); + free_block + } + fn drop_block(&mut self, target: BasicBlock, unwind: Unwind) -> BasicBlock { let block = TerminatorKind::Drop { place: self.place, @@ -900,7 +951,6 @@ where /// Depending on the required `DropStyle`, this might be a generated block with an `if` /// terminator (for dynamic/open drops), or it might be `on_set` or `on_unset` itself, in case /// the drop can be statically determined. - #[tracing::instrument(level = "debug", skip_all)] fn drop_flag_test_block( &mut self, on_set: BasicBlock, @@ -950,4 +1000,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 8aac315d11e..ef03c0f0ac5 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 @@ -109,8 +109,7 @@ pub(in super::super) fn run_pass<'tcx>(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>) } .elaborate() }; - elaborate_patch.apply(body); - deref_finder(tcx, body); + elaborate_patch } /// Removes unwind edges which are known to be unreachable, because they are in `drop` terminators @@ -583,4 +582,4 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> { } } } -} +} \ No newline at end of file diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs b/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs index 5a2adb174e3..6261a12859f 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs @@ -1217,9 +1217,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { target, unwind, replace: _, - } => { - self.encode_terminator_drop(block_builder, location, span, *place, *target, *unwind)? - } + } => self.encode_terminator_drop( + block_builder, + location, + span, + *place, + *target, + *unwind, + )?, TerminatorKind::Call { func: mir::Operand::Constant(box mir::Constant { literal, .. }), args, @@ -1779,11 +1784,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { self.def_id, )?; cleanup_block_builder.add_statement(function_lifetime_return); - self.encode_lft_for_block( - cleanup_block, - location, - &mut cleanup_block_builder, - )?; + self.encode_lft_for_block(cleanup_block, location, &mut cleanup_block_builder)?; cleanup_block_builder.build(); block_builder.set_successor_jump(vir_high::Successor::NonDetChoice( diff --git a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs index b645cc89dd7..06168e916b5 100644 --- a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs +++ b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs @@ -182,7 +182,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> { } mir::Rvalue::Aggregate(aggregate, operands) => { debug!("Encode aggregate {:?}, {:?}", aggregate, operands); - self.apply_assign_aggregate(state, ty, &encoded_lhs, aggregate, operands.as_slice(), span)? + self.apply_assign_aggregate( + state, + ty, + &encoded_lhs, + aggregate, + operands.as_slice(), + span, + )? } mir::Rvalue::BinaryOp(op, box (left, right)) => { let encoded_left = self.encode_operand(left, span)?; @@ -440,7 +447,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> { // compose substitutions // TODO(tymap): do we need this? - let substs = ty::EarlyBinder::bind(*call_substs).subst(self.encoder.env().tcx(), self.substs); + let substs = + ty::EarlyBinder::bind(*call_substs).subst(self.encoder.env().tcx(), self.substs); let state = if let Some(target_block) = target { let encoded_lhs = self.encode_place(destination).with_span(span)?; diff --git a/prusti-viper/src/encoder/mir/types/const_parameters.rs b/prusti-viper/src/encoder/mir/types/const_parameters.rs index 5f4dc7b8796..a5de58e73d9 100644 --- a/prusti-viper/src/encoder/mir/types/const_parameters.rs +++ b/prusti-viper/src/encoder/mir/types/const_parameters.rs @@ -17,6 +17,17 @@ pub(super) fn extract_const_parameters_from_substs<'tcx>( Ok(()) } +pub(super) fn extract_const_parameters_from_types<'tcx>( + type_encoder: &impl super::MirTypeEncoderInterface<'tcx>, + types: impl IntoIterator>, + const_parameters: &mut Vec, +) -> SpannedEncodingResult<()> { + for ty in types { + extract_const_parameters_from_type(type_encoder, ty, const_parameters)?; + } + Ok(()) +} + pub(super) fn extract_const_parameters_from_type<'tcx>( type_encoder: &impl super::MirTypeEncoderInterface<'tcx>, ty: ty::Ty<'tcx>, @@ -35,7 +46,7 @@ pub(super) fn extract_const_parameters_from_type<'tcx>( | ty::TyKind::Dynamic(..) => {} ty::TyKind::Adt(_, substs) | ty::TyKind::Closure(_, substs) - | ty::TyKind::Alias(ty::AliasKind::Opaque, ty::AliasTy { substs, .. }) + | ty::TyKind::Alias(_, ty::AliasTy { substs, .. }) | ty::TyKind::FnDef(_, substs) => { extract_const_parameters_from_substs(type_encoder, substs, const_parameters)? } @@ -68,9 +79,6 @@ pub(super) fn extract_const_parameters_from_type<'tcx>( ty::TyKind::Param(_param_ty) => { // FIXME: extract const_parameters from TyKind::Param() } - ty::TyKind::Alias(ty::AliasKind::Projection, alias_ty) => { - extract_const_parameters_from_substs(type_encoder, alias_ty.substs, const_parameters)? - } ty::TyKind::Bound(_, _) | ty::TyKind::Placeholder(_) | ty::TyKind::Infer(_) diff --git a/prusti-viper/src/encoder/mir/types/encoder.rs b/prusti-viper/src/encoder/mir/types/encoder.rs index 61294995d8b..c6df1436f6f 100644 --- a/prusti-viper/src/encoder/mir/types/encoder.rs +++ b/prusti-viper/src/encoder/mir/types/encoder.rs @@ -272,7 +272,6 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> { | ty::TyKind::GeneratorWitnessMIR(..) | ty::TyKind::Never | ty::TyKind::Tuple(_) - | ty::TyKind::Alias(ty::AliasKind::Projection, _) | ty::TyKind::Param(_) | ty::TyKind::Bound(..) | ty::TyKind::Placeholder(_) @@ -283,7 +282,7 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> { | ty::TyKind::FnDef(did, _) | ty::TyKind::Closure(did, _) | ty::TyKind::Generator(did, _, _) - | ty::TyKind::Alias(ty::AliasKind::Opaque, ty::AliasTy { def_id: did, .. }) => { + | ty::TyKind::Alias(_, ty::AliasTy { def_id: did, .. }) => { self.encoder.env().query.get_def_span(did).into() } } @@ -412,10 +411,8 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> { ) } ty::TyKind::Tuple(elems) => { - let lifetimes = self.encoder.get_lifetimes_from_substs(elems)?; - let const_parameters = self - .encoder - .get_const_parameters_from_substs(elems)?; + let lifetimes = self.encoder.get_lifetimes_from_types(*elems)?; + let const_parameters = self.encoder.get_const_parameters_from_types(*elems)?; let arguments = elems .into_iter() .map(|ty| self.encoder.encode_type_high(ty)) diff --git a/prusti-viper/src/encoder/mir/types/interface.rs b/prusti-viper/src/encoder/mir/types/interface.rs index 1b26bdf00b8..e81e377755d 100644 --- a/prusti-viper/src/encoder/mir/types/interface.rs +++ b/prusti-viper/src/encoder/mir/types/interface.rs @@ -39,6 +39,10 @@ pub(crate) trait MirTypeEncoderInterface<'tcx> { declaration_span: Span, ) -> SpannedEncodingResult; fn encode_value_field_high(&self, ty: ty::Ty<'tcx>) -> EncodingResult; + fn get_lifetimes_from_types( + &self, + types: impl IntoIterator>, + ) -> SpannedEncodingResult>; fn get_lifetimes_from_substs( &self, substs: SubstsRef<'tcx>, @@ -47,6 +51,10 @@ pub(crate) trait MirTypeEncoderInterface<'tcx> { &self, substs: SubstsRef<'tcx>, ) -> SpannedEncodingResult>; + fn get_const_parameters_from_types( + &self, + types: impl IntoIterator>, + ) -> SpannedEncodingResult>; fn get_lifetimes_from_type_high( &self, ty: ty::Ty<'tcx>, @@ -183,6 +191,14 @@ impl<'v, 'tcx: 'v> MirTypeEncoderInterface<'tcx> for super::super::super::Encode super::lifetimes::extract_lifetimes_from_substs(self, substs, &mut lifetimes)?; Ok(lifetimes) } + fn get_lifetimes_from_types( + &self, + types: impl IntoIterator>, + ) -> SpannedEncodingResult> { + let mut lifetimes = Vec::new(); + super::lifetimes::extract_lifetimes_from_types(self, types, &mut lifetimes)?; + Ok(lifetimes) + } fn get_const_parameters_from_substs( &self, substs: SubstsRef<'tcx>, @@ -195,6 +211,18 @@ impl<'v, 'tcx: 'v> MirTypeEncoderInterface<'tcx> for super::super::super::Encode )?; Ok(const_parameters) } + fn get_const_parameters_from_types( + &self, + types: impl IntoIterator>, + ) -> SpannedEncodingResult> { + let mut const_parameters = Vec::new(); + super::const_parameters::extract_const_parameters_from_types( + self, + types, + &mut const_parameters, + )?; + Ok(const_parameters) + } /// FIXME: This method causes a lifetime clash in case the same lifetime is /// used in multiple places: diff --git a/prusti-viper/src/encoder/mir/types/lifetimes.rs b/prusti-viper/src/encoder/mir/types/lifetimes.rs index e63f9a7847b..9d6799ac827 100644 --- a/prusti-viper/src/encoder/mir/types/lifetimes.rs +++ b/prusti-viper/src/encoder/mir/types/lifetimes.rs @@ -25,6 +25,17 @@ pub(super) fn extract_lifetimes_from_substs<'tcx>( Ok(()) } +pub(super) fn extract_lifetimes_from_types<'tcx>( + type_encoder: &impl super::MirTypeEncoderInterface<'tcx>, + types: impl IntoIterator>, + lifetimes: &mut Vec, +) -> SpannedEncodingResult<()> { + for ty in types { + extract_lifetimes_from_type(type_encoder, ty, lifetimes)?; + } + Ok(()) +} + pub(super) fn extract_lifetimes_from_type<'tcx>( type_encoder: &impl super::MirTypeEncoderInterface<'tcx>, ty: ty::Ty<'tcx>, @@ -42,7 +53,7 @@ pub(super) fn extract_lifetimes_from_type<'tcx>( | ty::TyKind::Never => {} ty::TyKind::Adt(_, substs) | ty::TyKind::Closure(_, substs) - | ty::TyKind::Alias(ty::AliasKind::Opaque, ty::AliasTy { substs, .. }) + | ty::TyKind::Alias(_, ty::AliasTy { substs, .. }) | ty::TyKind::FnDef(_, substs) => { extract_lifetimes_from_substs(type_encoder, substs, lifetimes)? } @@ -79,9 +90,6 @@ pub(super) fn extract_lifetimes_from_type<'tcx>( ty::TyKind::Param(_param_ty) => { // FIXME: extract lifetimes from TyKind::Param() } - ty::TyKind::Alias(ty::AliasKind::Projection, alias_ty) => { - extract_lifetimes_from_substs(type_encoder, alias_ty.substs, lifetimes)? - } ty::TyKind::Bound(_, _) | ty::TyKind::Placeholder(_) | ty::TyKind::Infer(_) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index a4e24c4a6a7..95b5d53e43a 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -1555,7 +1555,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { location )? } - mir::Rvalue::NullaryOp(op, op_ty) => { + mir::Rvalue::NullaryOp(ref op, op_ty) => { self.encode_assign_nullary_op( op, op_ty, @@ -5988,7 +5988,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { #[tracing::instrument(level = "trace", skip(self))] fn encode_assign_nullary_op( &mut self, - op: mir::NullOp, + op: &mir::NullOp, op_ty: ty::Ty<'tcx>, encoded_lhs: vir::Expr, ty: ty::Ty<'tcx>, @@ -6007,6 +6007,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { mir::NullOp::SizeOf => layout.size().bytes(), // FIXME: abi or pref? mir::NullOp::AlignOf => layout.align().abi.bytes(), + mir::NullOp::OffsetOf(_) => { + return Err(SpannedEncodingError::internal( + format!("`OffsetOf` is not supported yet"), + self.mir.source_info(location).span, + )) + } }; let bytes_vir = vir::Expr::from(bytes); self.encode_copy_value_assign( diff --git a/prusti-viper/src/utils/mod.rs b/prusti-viper/src/utils/mod.rs index daa4f02a198..16afb3574f3 100644 --- a/prusti-viper/src/utils/mod.rs +++ b/prusti-viper/src/utils/mod.rs @@ -35,6 +35,7 @@ pub fn ty_to_string(typ: &ty::TyKind) -> String { &ty::TyKind::Tuple(_) => "tuple", &ty::TyKind::Alias(ty::AliasKind::Projection, _) => "projection", &ty::TyKind::Alias(ty::AliasKind::Opaque, _) => "opaque type", + &ty::TyKind::Alias(ty::AliasKind::Inherent, _) => "inherent alias type", &ty::TyKind::Param(_) => "type parameter", &ty::TyKind::Bound(_, _) => "bound type variable", &ty::TyKind::Placeholder(_) => "placeholder type", diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index d716fa6f474..251f79d5da2 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -11,9 +11,10 @@ use prusti_rustc_interface::{ interface::{interface::Compiler, Config, Queries}, middle::ty::{ self, - query::{query_values::mir_borrowck, ExternProviders, Providers}, TyCtxt, }, + middle::mir::BorrowCheckResult, + middle::query::{ExternProviders, Providers}, session::Session, }; @@ -25,7 +26,7 @@ pub struct PrustiCompilerCalls; #[allow(clippy::needless_lifetimes)] #[tracing::instrument(level = "debug", skip(tcx))] -fn mir_borrowck<'tcx>(tcx: TyCtxt<'tcx>, def_id: LocalDefId) -> mir_borrowck<'tcx> { +fn mir_borrowck<'tcx>(tcx: TyCtxt<'tcx>, def_id: LocalDefId) -> &BorrowCheckResult<'tcx> { // *Don't take MIR bodies with borrowck info if we won't need them* if !is_spec_fn(tcx, def_id.to_def_id()) { let def_kind = tcx.def_kind(def_id.to_def_id()); diff --git a/prusti/src/driver.rs b/prusti/src/driver.rs index 729476a40d6..c0e807ada78 100644 --- a/prusti/src/driver.rs +++ b/prusti/src/driver.rs @@ -86,14 +86,14 @@ fn report_prusti_ice(info: &panic::PanicInfo<'_>, bug_report_url: &str) { let version_info = get_prusti_version_info(); - let xs: Vec> = vec![ + let xs: Vec = vec![ "Prusti or the compiler unexpectedly panicked. This is a bug.".into(), format!("We would appreciate a bug report: {bug_report_url}").into(), format!("Prusti version: {version_info}").into(), ]; - for note in &xs { - handler.note_without_error(note.as_ref()); + for note in xs { + handler.note_without_error(note); } // If backtraces are enabled, also print the query stack