Skip to content

Commit

Permalink
Fixes after merging master
Browse files Browse the repository at this point in the history
  • Loading branch information
@JakuJ
JakuJ committed Jul 20, 2023
1 parent 2670d47 commit 5a2d39c
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 85 deletions.
23 changes: 1 addition & 22 deletions prusti-viper/src/encoder/mir_encoder/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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::{
Expand All @@ -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,
Expand Down
101 changes: 38 additions & 63 deletions prusti-viper/src/encoder/procedure_encoder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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)?
Expand Down Expand Up @@ -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();
Expand All @@ -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];

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit 5a2d39c

Please sign in to comment.