From 5a2d39cccb3233259202d77209721b7230eb497c Mon Sep 17 00:00:00 2001 From: Jakub Janaszkiewicz Date: Fri, 21 Jul 2023 00:54:46 +0200 Subject: [PATCH] Fixes after merging master --- prusti-viper/src/encoder/mir_encoder/mod.rs | 23 +--- prusti-viper/src/encoder/procedure_encoder.rs | 101 +++++++----------- 2 files changed, 39 insertions(+), 85 deletions(-) diff --git a/prusti-viper/src/encoder/mir_encoder/mod.rs b/prusti-viper/src/encoder/mir_encoder/mod.rs index c439fcf1d41..16c83f11c11 100644 --- a/prusti-viper/src/encoder/mir_encoder/mod.rs +++ b/prusti-viper/src/encoder/mir_encoder/mod.rs @@ -6,27 +6,6 @@ use std::fmt::Debug; -use crate::encoder::errors::{ - ErrorCtxt, PanicCause, SpannedEncodingError, EncodingError, WithSpan, - SpannedEncodingResult, EncodingResult -}; -use crate::encoder::Encoder; -use crate::encoder::snapshot::interface::SnapshotEncoderInterface; -use crate::{utils, error_internal, error_unsupported}; -use prusti_common::vir_expr; -use vir_crate::{polymorphic as vir}; -use prusti_common::config; -use prusti_rustc_interface::target::abi; -use prusti_rustc_interface::hir::def_id::DefId; -use prusti_rustc_interface::middle::{mir, ty}; -use prusti_rustc_interface::index::IndexVec; -use prusti_rustc_interface::span::{Span, DUMMY_SP}; -use log::{trace, debug}; -use prusti_interface::environment::mir_utils::MirPlace; -use crate::encoder::mir::{ - sequences::MirSequencesEncoderInterface, - types::MirTypeEncoderInterface, -}; use super::high::types::HighTypeEncoderInterface; use crate::{ encoder::{ @@ -46,7 +25,7 @@ use prusti_interface::environment::mir_utils::MirPlace; use prusti_rustc_interface::{ errors::MultiSpan, hir::def_id::DefId, - index::vec::IndexVec, + index::IndexVec, middle::{mir, ty}, span::{Span, DUMMY_SP}, target::abi, diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 76111002c46..89c0a05fa2f 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -58,45 +58,22 @@ use prusti_interface::{ }, BasicBlockIndex, LoopAnalysisError, PermissionKind, Procedure, }, - PrustiError, -}; -use std::collections::{BTreeMap}; -use std::fmt::Debug; -use prusti_interface::utils; -use prusti_rustc_interface::index::IndexSlice; -use prusti_rustc_interface::middle::mir::Mutability; -use prusti_rustc_interface::middle::mir; -use prusti_rustc_interface::middle::mir::{TerminatorKind}; -use prusti_rustc_interface::middle::ty::{self, subst::SubstsRef}; -use prusti_rustc_interface::target::abi::{FieldIdx, Integer}; -use rustc_hash::{FxHashMap, FxHashSet}; -use prusti_rustc_interface::span::Span; -use prusti_rustc_interface::errors::MultiSpan; -use prusti_interface::specs::typed; -use ::log::{trace, debug}; -use prusti_interface::environment::borrowck::regions::PlaceRegionsError; -use crate::encoder::errors::EncodingErrorKind; -use std::convert::TryInto; -use prusti_interface::specs::typed::{Pledge, SpecificationItem}; -use vir_crate::polymorphic::Float; -use crate::utils::is_reference; -use crate::encoder::mir::{ - sequences::MirSequencesEncoderInterface, - contracts::{ - ContractsEncoderInterface, - ProcedureContract, + specs::{ + typed, + typed::{Pledge, SpecificationItem}, }, utils, PrustiError, }; use prusti_rustc_interface::{ errors::MultiSpan, + index::IndexSlice, middle::{ mir, mir::{Mutability, TerminatorKind}, ty::{self, subst::SubstsRef}, }, span::Span, - target::abi::Integer, + target::abi::{FieldIdx, Integer}, }; use rustc_hash::{FxHashMap, FxHashSet}; use std::{collections::BTreeMap, convert::TryInto, fmt::Debug}; @@ -1622,36 +1599,24 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { mir::Rvalue::Use(ref operand) => { self.encode_assign_operand(&encoded_lhs, operand, location)? } - mir::Rvalue::Aggregate(ref aggregate, ref operands) => { - self.encode_assign_aggregate( - &encoded_lhs, - ty, - aggregate, - operands.as_slice(), - location - )? - }, + mir::Rvalue::Aggregate(ref aggregate, ref operands) => self.encode_assign_aggregate( + &encoded_lhs, + ty, + aggregate, + operands.as_slice(), + location, + )?, mir::Rvalue::BinaryOp(op, box (ref left, ref right)) => { - self.encode_assign_binary_op( - op, - left, - right, - encoded_lhs, - ty, - location - )? + self.encode_assign_binary_op(op, left, right, encoded_lhs, ty, location)? + } + mir::Rvalue::CheckedBinaryOp(_, _) => { + todo!() } mir::Rvalue::UnaryOp(op, ref operand) => { self.encode_assign_unary_op(op, operand, encoded_lhs, ty, location)? } mir::Rvalue::NullaryOp(ref op, op_ty) => { - self.encode_assign_nullary_op( - op, - op_ty, - encoded_lhs, - ty, - location - )? + self.encode_assign_nullary_op(op, op_ty, encoded_lhs, ty, location)? } mir::Rvalue::Discriminant(src) => { self.encode_assign_discriminant(src, location, encoded_lhs, ty)? @@ -2227,9 +2192,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // Get the borrow information. if !self.procedure_contracts.contains_key(&loan_location) { return Err(SpannedEncodingError::internal( - format!("there is no procedure contract for loan {loan:?}. This could happen if you \ - are chaining pure functions, which is not fully supported."), - span + format!( + "there is no procedure contract for loan {loan:?}. This could happen if you \ + are chaining pure functions, which is not fully supported." + ), + span, )); } let (contract, fake_exprs) = self.procedure_contracts[&loan_location].clone(); @@ -2242,10 +2209,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { let borrow_infos = &contract.borrow_infos; match borrow_infos.len().cmp(&1) { std::cmp::Ordering::Less => (), - std::cmp::Ordering::Greater => return Err(SpannedEncodingError::internal( - format!("we require at most one magic wand in the postcondition. But we have {:?}", borrow_infos.len()), - span, - )), + std::cmp::Ordering::Greater => { + return Err(SpannedEncodingError::internal( + format!( + "we require at most one magic wand in the postcondition. But we have {:?}", + borrow_infos.len() + ), + span, + )) + } std::cmp::Ordering::Equal => { let borrow_info = &borrow_infos[0]; @@ -2874,7 +2846,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { }; // Check or assume the assertion - let (assert_msg, error_ctxt) = if let box mir::AssertKind::BoundsCheck { .. } = msg { + let (assert_msg, error_ctxt) = if let box mir::AssertKind::BoundsCheck { .. } = msg + { let mut s = String::new(); msg.fmt_assert_args(&mut s).unwrap(); (s, ErrorCtxt::BoundsCheckAssert) @@ -5790,9 +5763,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { } } else { // FIXME: why are we getting the MIR body for this? - let mir = self.encoder.env().body.get_impure_fn_body_identity( - containing_def_id.expect_local(), - ); + let mir = self + .encoder + .env() + .body + .get_impure_fn_body_identity(containing_def_id.expect_local()); let return_ty = mir.return_ty(); let arg_tys = mir.args_iter().map(|arg| mir.local_decls[arg].ty).collect(); FakeMirEncoder::new(self.encoder, arg_tys, return_ty)