Skip to content

Commit 03d9d61

Browse files
JakuJJakuJ
committed
Restore config
1 parent 08e33a7 commit 03d9d61

File tree

5 files changed

+63
-47
lines changed

5 files changed

+63
-47
lines changed

‎prusti-utils/src/config.rs

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ lazy_static::lazy_static! {
6969

7070
// 0. Default values
7171
settings.set_default("be_rustc", false).unwrap();
72-
settings.set_default("viper_backend", "Lithium").unwrap();
72+
settings.set_default("viper_backend", "Silicon").unwrap();
7373
settings.set_default::<Option<String>>("smt_solver_path", env::var("Z3_EXE").ok()).unwrap();
7474
settings.set_default::<Option<String>>("smt_solver_wrapper_path", None).unwrap();
7575
settings.set_default::<Option<String>>("boogie_path", env::var("BOOGIE_EXE").ok()).unwrap();
@@ -81,7 +81,7 @@ lazy_static::lazy_static! {
8181
settings.set_default("check_overflows", true).unwrap();
8282
settings.set_default("check_panics", true).unwrap();
8383
settings.set_default("encode_unsigned_num_constraint", true).unwrap();
84-
settings.set_default("encode_bitvectors", true).unwrap();
84+
settings.set_default("encode_bitvectors", false).unwrap();
8585
settings.set_default("simplify_encoding", true).unwrap();
8686
settings.set_default("log", "").unwrap();
8787
settings.set_default("log_style", "auto").unwrap();
@@ -92,7 +92,7 @@ lazy_static::lazy_static! {
9292
settings.set_default("dump_debug_info_during_fold", false).unwrap();
9393
settings.set_default("dump_nll_facts", false).unwrap();
9494
settings.set_default("ignore_regions", false).unwrap();
95-
settings.set_default("max_log_file_name_length", 240).unwrap();
95+
settings.set_default("max_log_file_name_length", 60).unwrap();
9696
settings.set_default("dump_path_ctxt_in_debug_info", false).unwrap();
9797
settings.set_default("dump_reborrowing_dag_in_debug_info", false).unwrap();
9898
settings.set_default("dump_borrowck_info", false).unwrap();
@@ -104,7 +104,7 @@ lazy_static::lazy_static! {
104104
settings.set_default("assert_timeout", 10_000).unwrap();
105105
settings.set_default("smt_qi_eager_threshold", 1000).unwrap();
106106
settings.set_default("use_more_complete_exhale", true).unwrap();
107-
settings.set_default("skip_unsupported_features", true).unwrap();
107+
settings.set_default("skip_unsupported_features", false).unwrap();
108108
settings.set_default("internal_errors_as_warnings", false).unwrap();
109109
settings.set_default("allow_unreachable_unsupported_code", false).unwrap();
110110
settings.set_default("no_verify", false).unwrap();
@@ -114,16 +114,16 @@ lazy_static::lazy_static! {
114114
settings.set_default("json_communication", false).unwrap();
115115
settings.set_default("optimizations", "all").unwrap();
116116
settings.set_default("intern_names", true).unwrap();
117-
settings.set_default("enable_purification_optimization", true).unwrap();
117+
settings.set_default("enable_purification_optimization", false).unwrap();
118118
// settings.set_default("enable_manual_axiomatization", false).unwrap();
119-
settings.set_default("unsafe_core_proof", true).unwrap();
120-
settings.set_default("verify_core_proof", false).unwrap();
119+
settings.set_default("unsafe_core_proof", false).unwrap();
120+
settings.set_default("verify_core_proof", true).unwrap();
121121
settings.set_default("verify_specifications", true).unwrap();
122122
settings.set_default("verify_types", false).unwrap();
123123
settings.set_default("verify_specifications_with_core_proof", false).unwrap();
124-
settings.set_default("verify_specifications_backend", "Lithium").unwrap();
124+
settings.set_default("verify_specifications_backend", "Silicon").unwrap();
125125
settings.set_default("use_eval_axioms", true).unwrap();
126-
settings.set_default("inline_caller_for", true).unwrap();
126+
settings.set_default("inline_caller_for", false).unwrap();
127127
settings.set_default("check_no_drops", false).unwrap();
128128
settings.set_default("enable_type_invariants", false).unwrap();
129129
settings.set_default("use_new_encoder", true).unwrap();

‎prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -218,7 +218,6 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> {
218218
state.check_consistency();
219219
let actions = ensure_required_permissions(self, state, consumed_permissions.clone())?;
220220
self.process_actions(actions)?;
221-
// TODO: Remove permission reasoning
222221
state.remove_permissions(&consumed_permissions)?;
223222
state.insert_permissions(produced_permissions)?;
224223
match &statement {

‎prusti-viper/src/encoder/places.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
// file, You can obtain one at http://mozilla.org/MPL/2.0/.
66

77
use prusti_rustc_interface::{
8-
index::vec::{Idx, IndexVec},
8+
index::{Idx, IndexVec},
99
middle::{mir, ty::Ty},
1010
};
1111
use std::iter;

‎prusti-viper/src/encoder/procedure_encoder.rs

Lines changed: 40 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ use prusti_rustc_interface::{
7070
middle::{
7171
mir,
7272
mir::{Mutability, TerminatorKind},
73-
ty::{self, subst::SubstsRef},
73+
ty::{self, GenericArgsRef},
7474
},
7575
span::Span,
7676
target::abi::{FieldIdx, Integer},
@@ -1051,12 +1051,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
10511051
Some((mid_g, mid_b1))
10521052
} else {
10531053
// Cannot add loop guard to loop invariant
1054-
let fn_names: Vec<_> = preconds.iter().filter_map(|(name, _)| name.as_ref()).map(|name| {
1055-
if let Some(rust_name) = name.strip_prefix("f_") {
1056-
return rust_name
1057-
};
1058-
name.strip_prefix("m_").unwrap_or(name)
1059-
}).collect();
1054+
let fn_names: Vec<_> = preconds
1055+
.iter()
1056+
.filter_map(|(name, _)| name.as_ref())
1057+
.map(|name| {
1058+
if let Some(rust_name) = name.strip_prefix("f_") {
1059+
return rust_name;
1060+
};
1061+
name.strip_prefix("m_").unwrap_or(name)
1062+
})
1063+
.collect();
10601064
let warning_msg = if fn_names.is_empty() {
10611065
"the loop guard was not automatically added as a `body_invariant!(...)`, consider doing this manually".to_string()
10621066
} else {
@@ -1640,9 +1644,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
16401644
times,
16411645
ty,
16421646
location,
1643-
)?
1644-
}
1645-
mir::Rvalue::Cast(mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), ref operand, cast_ty) => {
1647+
)?,
1648+
mir::Rvalue::Cast(
1649+
mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
1650+
ref operand,
1651+
cast_ty,
1652+
) => {
16461653
let rhs_ty = self.mir_encoder.get_operand_ty(operand);
16471654
if rhs_ty.is_array_ref() && cast_ty.is_slice_ref() {
16481655
trace!("slice: operand={:?}, ty={:?}", operand, cast_ty);
@@ -1654,8 +1661,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
16541661
));
16551662
}
16561663
}
1657-
mir::Rvalue::Cast(mir::CastKind::PointerCoercion(_), _, _) |
1658-
mir::Rvalue::Cast(mir::CastKind::DynStar, _, _) => {
1664+
mir::Rvalue::Cast(mir::CastKind::PointerCoercion(_), _, _)
1665+
| mir::Rvalue::Cast(mir::CastKind::DynStar, _, _) => {
16591666
return Err(SpannedEncodingError::unsupported(
16601667
"raw pointers are not supported",
16611668
span,
@@ -1830,7 +1837,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
18301837
(expiring, Some(restored), false, stmts)
18311838
}
18321839

1833-
mir::Rvalue::Cast(mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), ref operand, ty) => {
1840+
mir::Rvalue::Cast(
1841+
mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
1842+
ref operand,
1843+
ty,
1844+
) => {
18341845
trace!("cast: operand={:?}, ty={:?}", operand, ty);
18351846
let place = match *operand {
18361847
mir::Operand::Move(place) => place,
@@ -1923,11 +1934,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
19231934
if let Some(stmt) = self.polonius_info().get_assignment_for_loan(loan)? {
19241935
Ok(match stmt.kind {
19251936
mir::StatementKind::Assign(box (_, ref rhs)) => match rhs {
1926-
&mir::Rvalue::Ref(_, mir::BorrowKind::Shared, _) |
1927-
&mir::Rvalue::Use(mir::Operand::Copy(_)) => false,
1928-
&mir::Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, _) |
1929-
&mir::Rvalue::Use(mir::Operand::Move(_)) => true,
1930-
&mir::Rvalue::Cast(mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), _, _ty) => false,
1937+
&mir::Rvalue::Ref(_, mir::BorrowKind::Shared, _)
1938+
| &mir::Rvalue::Use(mir::Operand::Copy(_)) => false,
1939+
&mir::Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, _)
1940+
| &mir::Rvalue::Use(mir::Operand::Move(_)) => true,
1941+
&mir::Rvalue::Cast(
1942+
mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
1943+
_,
1944+
_ty,
1945+
) => false,
19311946
&mir::Rvalue::Use(mir::Operand::Constant(_)) => false,
19321947
x => unreachable!("{:?}", x),
19331948
},
@@ -3381,7 +3396,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
33813396

33823397
// TODO: weird fix for closure call substitutions, we need to
33833398
// prepend the identity substs of the containing method ...
3384-
substs = self.encoder.env().tcx().mk_args_from_iter(self.substs.iter().chain(substs));
3399+
substs = self
3400+
.encoder
3401+
.env()
3402+
.tcx()
3403+
.mk_args_from_iter(self.substs.iter().chain(substs));
33853404
} else {
33863405
for (arg, encoded_operand) in mir_args.iter().zip(encoded_operands.iter_mut()) {
33873406
let arg_ty = self.mir_encoder.get_operand_ty(arg);
@@ -3990,13 +4009,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
39904009
&self,
39914010
contract: &ProcedureContract<'tcx>,
39924011
substs: GenericArgsRef<'tcx>,
3993-
override_spans: FxHashMap<Local, Span> // spans for fake locals
3994-
) -> SpannedEncodingResult<(
3995-
vir::Expr,
3996-
Vec<vir::Expr>,
3997-
vir::Expr,
3998-
vir::Expr,
3999-
)> {
4012+
override_spans: FxHashMap<Local, Span>, // spans for fake locals
4013+
) -> SpannedEncodingResult<(vir::Expr, Vec<vir::Expr>, vir::Expr, vir::Expr)> {
40004014
let borrow_infos = &contract.borrow_infos;
40014015
let maybe_blocked_paths = if !borrow_infos.is_empty() {
40024016
assert_eq!(

‎prusti-viper/src/utils/type_visitor.rs

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,13 @@
44
// License, v. 2.0. If a copy of the MPL was not distributed with this
55
// file, You can obtain one at http://mozilla.org/MPL/2.0/.
66

7-
use prusti_rustc_interface::hir::Mutability;
8-
use prusti_rustc_interface::middle::ty::{
9-
AdtDef, FieldDef, List, ParamTy, Region, AliasKind, AliasTy, Ty, TyCtxt,
10-
TypeFlags, TyKind, IntTy, UintTy, FloatTy, VariantDef, GenericArgsRef, Const
7+
use prusti_rustc_interface::{
8+
hir::Mutability,
9+
middle::ty::{
10+
AdtDef, AliasKind, AliasTy, Const, FieldDef, FloatTy, GenericArgsRef, IntTy, List, ParamTy,
11+
Region, Ty, TyCtxt, TyKind, TypeFlags, UintTy, VariantDef,
12+
},
13+
span::def_id::DefId,
1114
};
1215

1316
pub trait TypeVisitor<'tcx>: Sized {
@@ -87,7 +90,7 @@ pub trait TypeVisitor<'tcx>: Sized {
8790
fn visit_adt(
8891
&mut self,
8992
adt_def: AdtDef<'tcx>,
90-
substs: GenericArgsRef<'tcx>
93+
substs: GenericArgsRef<'tcx>,
9194
) -> Result<(), Self::Error> {
9295
walk_adt(self, adt_def, substs)
9396
}
@@ -99,7 +102,7 @@ pub trait TypeVisitor<'tcx>: Sized {
99102
idx: prusti_rustc_interface::target::abi::VariantIdx,
100103
variant: &VariantDef,
101104
substs: GenericArgsRef<'tcx>,
102-
) -> Result<(), Self::Error> {
105+
) -> Result<(), Self::Error> {
103106
walk_adt_variant(self, variant, substs)
104107
}
105108

@@ -143,7 +146,7 @@ pub trait TypeVisitor<'tcx>: Sized {
143146
fn visit_closure(
144147
&mut self,
145148
def_id: DefId,
146-
substs: GenericArgsRef<'tcx>
149+
substs: GenericArgsRef<'tcx>,
147150
) -> Result<(), Self::Error> {
148151
walk_closure(self, def_id, substs)
149152
}
@@ -152,7 +155,7 @@ pub trait TypeVisitor<'tcx>: Sized {
152155
fn visit_fndef(
153156
&mut self,
154157
def_id: DefId,
155-
substs: GenericArgsRef<'tcx>
158+
substs: GenericArgsRef<'tcx>,
156159
) -> Result<(), Self::Error> {
157160
walk_fndef(self, def_id, substs)
158161
}
@@ -232,7 +235,7 @@ pub fn walk_raw_ptr<'tcx, E, V: TypeVisitor<'tcx, Error = E>>(
232235
pub fn walk_closure<'tcx, E, V: TypeVisitor<'tcx, Error = E>>(
233236
visitor: &mut V,
234237
_def_id: DefId,
235-
substs: GenericArgsRef<'tcx>
238+
substs: GenericArgsRef<'tcx>,
236239
) -> Result<(), E> {
237240
let cl_substs = substs.as_closure();
238241
// TODO: when are there bound typevars? can type visitor deal with generics?
@@ -248,7 +251,7 @@ pub fn walk_closure<'tcx, E, V: TypeVisitor<'tcx, Error = E>>(
248251
pub fn walk_fndef<'tcx, E, V: TypeVisitor<'tcx, Error = E>>(
249252
visitor: &mut V,
250253
_def_id: DefId,
251-
substs: GenericArgsRef<'tcx>
254+
substs: GenericArgsRef<'tcx>,
252255
) -> Result<(), E> {
253256
for ty in substs.types() {
254257
visitor.visit_ty(ty)?;

0 commit comments

Comments
 (0)