Skip to content

Commit

Permalink
Restore config
Browse files Browse the repository at this point in the history
  • Loading branch information
@JakuJ
JakuJ committed Aug 18, 2023
1 parent 08e33a7 commit 03d9d61
Show file tree
Hide file tree
Showing 5 changed files with 63 additions and 47 deletions.
18 changes: 9 additions & 9 deletions prusti-utils/src/config.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ lazy_static::lazy_static! {

// 0. Default values
settings.set_default("be_rustc", false).unwrap();
settings.set_default("viper_backend", "Lithium").unwrap();
settings.set_default("viper_backend", "Silicon").unwrap();
settings.set_default::<Option<String>>("smt_solver_path", env::var("Z3_EXE").ok()).unwrap();
settings.set_default::<Option<String>>("smt_solver_wrapper_path", None).unwrap();
settings.set_default::<Option<String>>("boogie_path", env::var("BOOGIE_EXE").ok()).unwrap();
Expand All @@ -81,7 +81,7 @@ lazy_static::lazy_static! {
settings.set_default("check_overflows", true).unwrap();
settings.set_default("check_panics", true).unwrap();
settings.set_default("encode_unsigned_num_constraint", true).unwrap();
settings.set_default("encode_bitvectors", true).unwrap();
settings.set_default("encode_bitvectors", false).unwrap();
settings.set_default("simplify_encoding", true).unwrap();
settings.set_default("log", "").unwrap();
settings.set_default("log_style", "auto").unwrap();
Expand All @@ -92,7 +92,7 @@ lazy_static::lazy_static! {
settings.set_default("dump_debug_info_during_fold", false).unwrap();
settings.set_default("dump_nll_facts", false).unwrap();
settings.set_default("ignore_regions", false).unwrap();
settings.set_default("max_log_file_name_length", 240).unwrap();
settings.set_default("max_log_file_name_length", 60).unwrap();
settings.set_default("dump_path_ctxt_in_debug_info", false).unwrap();
settings.set_default("dump_reborrowing_dag_in_debug_info", false).unwrap();
settings.set_default("dump_borrowck_info", false).unwrap();
Expand All @@ -104,7 +104,7 @@ lazy_static::lazy_static! {
settings.set_default("assert_timeout", 10_000).unwrap();
settings.set_default("smt_qi_eager_threshold", 1000).unwrap();
settings.set_default("use_more_complete_exhale", true).unwrap();
settings.set_default("skip_unsupported_features", true).unwrap();
settings.set_default("skip_unsupported_features", false).unwrap();
settings.set_default("internal_errors_as_warnings", false).unwrap();
settings.set_default("allow_unreachable_unsupported_code", false).unwrap();
settings.set_default("no_verify", false).unwrap();
Expand All @@ -114,16 +114,16 @@ lazy_static::lazy_static! {
settings.set_default("json_communication", false).unwrap();
settings.set_default("optimizations", "all").unwrap();
settings.set_default("intern_names", true).unwrap();
settings.set_default("enable_purification_optimization", true).unwrap();
settings.set_default("enable_purification_optimization", false).unwrap();
// settings.set_default("enable_manual_axiomatization", false).unwrap();
settings.set_default("unsafe_core_proof", true).unwrap();
settings.set_default("verify_core_proof", false).unwrap();
settings.set_default("unsafe_core_proof", false).unwrap();
settings.set_default("verify_core_proof", true).unwrap();
settings.set_default("verify_specifications", true).unwrap();
settings.set_default("verify_types", false).unwrap();
settings.set_default("verify_specifications_with_core_proof", false).unwrap();
settings.set_default("verify_specifications_backend", "Lithium").unwrap();
settings.set_default("verify_specifications_backend", "Silicon").unwrap();
settings.set_default("use_eval_axioms", true).unwrap();
settings.set_default("inline_caller_for", true).unwrap();
settings.set_default("inline_caller_for", false).unwrap();
settings.set_default("check_no_drops", false).unwrap();
settings.set_default("enable_type_invariants", false).unwrap();
settings.set_default("use_new_encoder", true).unwrap();
Expand Down
1 change: 0 additions & 1 deletion prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -218,7 +218,6 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> {
state.check_consistency();
let actions = ensure_required_permissions(self, state, consumed_permissions.clone())?;
self.process_actions(actions)?;
// TODO: Remove permission reasoning
state.remove_permissions(&consumed_permissions)?;
state.insert_permissions(produced_permissions)?;
match &statement {
Expand Down
2 changes: 1 addition & 1 deletion prusti-viper/src/encoder/places.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
// file, You can obtain one at http://mozilla.org/MPL/2.0/.

use prusti_rustc_interface::{
index::vec::{Idx, IndexVec},
index::{Idx, IndexVec},
middle::{mir, ty::Ty},
};
use std::iter;
Expand Down
66 changes: 40 additions & 26 deletions prusti-viper/src/encoder/procedure_encoder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ use prusti_rustc_interface::{
middle::{
mir,
mir::{Mutability, TerminatorKind},
ty::{self, subst::SubstsRef},
ty::{self, GenericArgsRef},
},
span::Span,
target::abi::{FieldIdx, Integer},
Expand Down Expand Up @@ -1051,12 +1051,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
Some((mid_g, mid_b1))
} else {
// Cannot add loop guard to loop invariant
let fn_names: Vec<_> = preconds.iter().filter_map(|(name, _)| name.as_ref()).map(|name| {
if let Some(rust_name) = name.strip_prefix("f_") {
return rust_name
};
name.strip_prefix("m_").unwrap_or(name)
}).collect();
let fn_names: Vec<_> = preconds
.iter()
.filter_map(|(name, _)| name.as_ref())
.map(|name| {
if let Some(rust_name) = name.strip_prefix("f_") {
return rust_name;
};
name.strip_prefix("m_").unwrap_or(name)
})
.collect();
let warning_msg = if fn_names.is_empty() {
"the loop guard was not automatically added as a `body_invariant!(...)`, consider doing this manually".to_string()
} else {
Expand Down Expand Up @@ -1640,9 +1644,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
times,
ty,
location,
)?
}
mir::Rvalue::Cast(mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), ref operand, cast_ty) => {
)?,
mir::Rvalue::Cast(
mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
ref operand,
cast_ty,
) => {
let rhs_ty = self.mir_encoder.get_operand_ty(operand);
if rhs_ty.is_array_ref() && cast_ty.is_slice_ref() {
trace!("slice: operand={:?}, ty={:?}", operand, cast_ty);
Expand All @@ -1654,8 +1661,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
));
}
}
mir::Rvalue::Cast(mir::CastKind::PointerCoercion(_), _, _) |
mir::Rvalue::Cast(mir::CastKind::DynStar, _, _) => {
mir::Rvalue::Cast(mir::CastKind::PointerCoercion(_), _, _)
| mir::Rvalue::Cast(mir::CastKind::DynStar, _, _) => {
return Err(SpannedEncodingError::unsupported(
"raw pointers are not supported",
span,
Expand Down Expand Up @@ -1830,7 +1837,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
(expiring, Some(restored), false, stmts)
}

mir::Rvalue::Cast(mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), ref operand, ty) => {
mir::Rvalue::Cast(
mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
ref operand,
ty,
) => {
trace!("cast: operand={:?}, ty={:?}", operand, ty);
let place = match *operand {
mir::Operand::Move(place) => place,
Expand Down Expand Up @@ -1923,11 +1934,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
if let Some(stmt) = self.polonius_info().get_assignment_for_loan(loan)? {
Ok(match stmt.kind {
mir::StatementKind::Assign(box (_, ref rhs)) => match rhs {
&mir::Rvalue::Ref(_, mir::BorrowKind::Shared, _) |
&mir::Rvalue::Use(mir::Operand::Copy(_)) => false,
&mir::Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, _) |
&mir::Rvalue::Use(mir::Operand::Move(_)) => true,
&mir::Rvalue::Cast(mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), _, _ty) => false,
&mir::Rvalue::Ref(_, mir::BorrowKind::Shared, _)
| &mir::Rvalue::Use(mir::Operand::Copy(_)) => false,
&mir::Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, _)
| &mir::Rvalue::Use(mir::Operand::Move(_)) => true,
&mir::Rvalue::Cast(
mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
_,
_ty,
) => false,
&mir::Rvalue::Use(mir::Operand::Constant(_)) => false,
x => unreachable!("{:?}", x),
},
Expand Down Expand Up @@ -3381,7 +3396,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {

// TODO: weird fix for closure call substitutions, we need to
// prepend the identity substs of the containing method ...
substs = self.encoder.env().tcx().mk_args_from_iter(self.substs.iter().chain(substs));
substs = self
.encoder
.env()
.tcx()
.mk_args_from_iter(self.substs.iter().chain(substs));
} else {
for (arg, encoded_operand) in mir_args.iter().zip(encoded_operands.iter_mut()) {
let arg_ty = self.mir_encoder.get_operand_ty(arg);
Expand Down Expand Up @@ -3990,13 +4009,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
&self,
contract: &ProcedureContract<'tcx>,
substs: GenericArgsRef<'tcx>,
override_spans: FxHashMap<Local, Span> // spans for fake locals
) -> SpannedEncodingResult<(
vir::Expr,
Vec<vir::Expr>,
vir::Expr,
vir::Expr,
)> {
override_spans: FxHashMap<Local, Span>, // spans for fake locals
) -> SpannedEncodingResult<(vir::Expr, Vec<vir::Expr>, vir::Expr, vir::Expr)> {
let borrow_infos = &contract.borrow_infos;
let maybe_blocked_paths = if !borrow_infos.is_empty() {
assert_eq!(
Expand Down
23 changes: 13 additions & 10 deletions prusti-viper/src/utils/type_visitor.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,13 @@
// License, v. 2.0. If a copy of the MPL was not distributed with this
// file, You can obtain one at http://mozilla.org/MPL/2.0/.

use prusti_rustc_interface::hir::Mutability;
use prusti_rustc_interface::middle::ty::{
AdtDef, FieldDef, List, ParamTy, Region, AliasKind, AliasTy, Ty, TyCtxt,
TypeFlags, TyKind, IntTy, UintTy, FloatTy, VariantDef, GenericArgsRef, Const
use prusti_rustc_interface::{
hir::Mutability,
middle::ty::{
AdtDef, AliasKind, AliasTy, Const, FieldDef, FloatTy, GenericArgsRef, IntTy, List, ParamTy,
Region, Ty, TyCtxt, TyKind, TypeFlags, UintTy, VariantDef,
},
span::def_id::DefId,
};

pub trait TypeVisitor<'tcx>: Sized {
Expand Down Expand Up @@ -87,7 +90,7 @@ pub trait TypeVisitor<'tcx>: Sized {
fn visit_adt(
&mut self,
adt_def: AdtDef<'tcx>,
substs: GenericArgsRef<'tcx>
substs: GenericArgsRef<'tcx>,
) -> Result<(), Self::Error> {
walk_adt(self, adt_def, substs)
}
Expand All @@ -99,7 +102,7 @@ pub trait TypeVisitor<'tcx>: Sized {
idx: prusti_rustc_interface::target::abi::VariantIdx,
variant: &VariantDef,
substs: GenericArgsRef<'tcx>,
) -> Result<(), Self::Error> {
) -> Result<(), Self::Error> {
walk_adt_variant(self, variant, substs)
}

Expand Down Expand Up @@ -143,7 +146,7 @@ pub trait TypeVisitor<'tcx>: Sized {
fn visit_closure(
&mut self,
def_id: DefId,
substs: GenericArgsRef<'tcx>
substs: GenericArgsRef<'tcx>,
) -> Result<(), Self::Error> {
walk_closure(self, def_id, substs)
}
Expand All @@ -152,7 +155,7 @@ pub trait TypeVisitor<'tcx>: Sized {
fn visit_fndef(
&mut self,
def_id: DefId,
substs: GenericArgsRef<'tcx>
substs: GenericArgsRef<'tcx>,
) -> Result<(), Self::Error> {
walk_fndef(self, def_id, substs)
}
Expand Down Expand Up @@ -232,7 +235,7 @@ pub fn walk_raw_ptr<'tcx, E, V: TypeVisitor<'tcx, Error = E>>(
pub fn walk_closure<'tcx, E, V: TypeVisitor<'tcx, Error = E>>(
visitor: &mut V,
_def_id: DefId,
substs: GenericArgsRef<'tcx>
substs: GenericArgsRef<'tcx>,
) -> Result<(), E> {
let cl_substs = substs.as_closure();
// TODO: when are there bound typevars? can type visitor deal with generics?
Expand All @@ -248,7 +251,7 @@ pub fn walk_closure<'tcx, E, V: TypeVisitor<'tcx, Error = E>>(
pub fn walk_fndef<'tcx, E, V: TypeVisitor<'tcx, Error = E>>(
visitor: &mut V,
_def_id: DefId,
substs: GenericArgsRef<'tcx>
substs: GenericArgsRef<'tcx>,
) -> Result<(), E> {
for ty in substs.types() {
visitor.visit_ty(ty)?;
Expand Down

0 comments on commit 03d9d61

Please sign in to comment.