Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Automatically add loop guards without preconditions as invariants #887

Merged
merged 24 commits into from
May 22, 2022
Merged
Changes from 1 commit
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
52af7c6
Add loop guards without preconditions to invariant
JonasAlaif Feb 28, 2022
1b9ed1a
Avoid unnecessary encoding
JonasAlaif Feb 28, 2022
fc978a9
Clippy fix and ignore AccessPredicate expressions
JonasAlaif Feb 28, 2022
9fc7dc0
Fix issue with resolving function calls
JonasAlaif Feb 28, 2022
d4fe137
Clippy fixes
JonasAlaif Feb 28, 2022
d334808
Remove unnecessary check of MethodCall
JonasAlaif Feb 28, 2022
af55365
Make use of ExprFolder
JonasAlaif Feb 28, 2022
50a77fd
Fix typo
JonasAlaif Feb 28, 2022
ddc7e82
Make warning function more general
JonasAlaif Feb 28, 2022
ef272f0
Fmt fix
JonasAlaif Feb 28, 2022
2b0306d
Fix comment
JonasAlaif Mar 1, 2022
2e91033
Merge branch 'master' into loop-inv-fix
JonasAlaif Mar 23, 2022
e1f3e66
Change asserts to assumes after unrolling
JonasAlaif Mar 23, 2022
2506646
Merge branch 'master' into loop-inv-fix
JonasAlaif Apr 22, 2022
6a3b715
Clippy fix
JonasAlaif Apr 22, 2022
df53a1e
Track pure functions preventing unrolling
JonasAlaif Apr 22, 2022
51f7312
Clippy fix
JonasAlaif Apr 22, 2022
e178ca1
Merge branch 'master' into loop-inv-fix
JonasAlaif Apr 27, 2022
4ada2cd
Only emit warning on verification failure
JonasAlaif Apr 27, 2022
283776b
Merge branch 'master' into loop-inv-fix
JonasAlaif May 13, 2022
4ed6b78
Distinguish between warning types
JonasAlaif May 13, 2022
0eddf8a
clippy fix
JonasAlaif May 13, 2022
df8ecd7
Merge branch 'master' into loop-inv-fix
JonasAlaif May 20, 2022
caee09b
Update test with new expected errors
JonasAlaif May 21, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Make use of ExprFolder
  • Loading branch information
JonasAlaif committed Feb 28, 2022

Unverified

No user is associated with the committer email.
commit af55365036ebdc4c4788b1dff0d6f0fc47f4c8c5
148 changes: 68 additions & 80 deletions prusti-viper/src/encoder/procedure_encoder.rs
Original file line number Diff line number Diff line change
@@ -32,7 +32,7 @@ use vir_crate::{
compute_identifier,
borrows::Borrow,
collect_assigned_vars,
CfgBlockIndex, Expr, ExprIterator, StmtWalker, Successor, Type},
CfgBlockIndex, Expr, ExprIterator, Successor, Type},
};
use prusti_interface::{
data::ProcedureDefId,
@@ -513,96 +513,84 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
}

fn stmt_preconditions(&self, stmt: &vir::Stmt) -> Vec<vir::Expr> {
struct FindFnApps<'a, 'b, 'c>(Vec<vir::Expr>, &'a Encoder<'b, 'c>);
use vir::{ExprFolder, StmtWalker};
struct FindFnApps<'a, 'b, 'c> {
recurse: bool,
preconds: Vec<vir::Expr>,
encoder: &'a Encoder<'b, 'c>,
}
fn is_const_true(expr: &vir::Expr) -> bool {
matches!(
expr,
vir::Expr::Const(vir::ConstExpr {
value: vir::Const::Bool(true), ..
})
)
}
impl<'a, 'b, 'c> StmtWalker for FindFnApps<'a, 'b, 'c> {
fn walk_exhale(&mut self, statement: &vir::Exhale) {
self.0.push(statement.expr.clone());
let expr = self.fold(statement.expr.clone());
self.preconds.push(expr);
}
fn walk_assert(&mut self, statement: &vir::Assert) {
self.0.push(statement.expr.clone());
}
fn walk_method_call(&mut self, statement: &vir::MethodCall) {
// Note: We know that in Prusti method's preconditions and postconditions are empty
for arg in &statement.arguments {
self.walk_expr(arg);
}
let expr = self.fold(statement.expr.clone());
self.preconds.push(expr);
}
fn walk_expr(&mut self, expr: &vir::Expr) {
JonasAlaif marked this conversation as resolved.
Show resolved Hide resolved
match expr {
vir::Expr::Local(_) |
vir::Expr::Const(_) |
vir::Expr::MagicWand(_) => {}, // TODO: Is this correct?

vir::Expr::Variant(vir::Variant { base, .. }) |
vir::Expr::Field(vir::FieldExpr { base, .. }) |
vir::Expr::AddrOf(vir::AddrOf { base, .. }) |
vir::Expr::LabelledOld(vir::LabelledOld { base, .. }) |
vir::Expr::FieldAccessPredicate(vir::FieldAccessPredicate { base, .. }) |
vir::Expr::Unfolding(vir::Unfolding { base, .. }) |
vir::Expr::SnapApp(vir::SnapApp { base, .. }) |
vir::Expr::Cast(vir::Cast { base, .. }) => self.walk_expr(&*base),

vir::Expr::PredicateAccessPredicate(vir::PredicateAccessPredicate { argument, .. }) |
vir::Expr::UnaryOp(vir::UnaryOp { argument, .. }) =>
self.walk_expr(&*argument),

vir::Expr::BinOp(vir::BinOp { left, right, .. }) |
vir::Expr::ContainerOp(vir::ContainerOp { left, right, .. }) => {
self.walk_expr(&*left);
self.walk_expr(&*right);
}

vir::Expr::Cond(vir::Cond { guard, then_expr, else_expr, .. }) => {
self.walk_expr(&*guard);
self.walk_expr(&*then_expr);
self.walk_expr(&*else_expr);
}
vir::Expr::ForAll(vir::ForAll { body, .. }) |
vir::Expr::Exists(vir::Exists { body, .. }) => self.walk_expr(&*body),
vir::Expr::LetExpr(vir::LetExpr { def, body, ..}) => {
self.walk_expr(&*def);
self.walk_expr(&*body);
}
vir::Expr::FuncApp(vir::FuncApp { function_name, type_arguments, arguments, formal_arguments, return_type, .. }) => {
let identifier: vir::FunctionIdentifier =
compute_identifier(function_name, type_arguments, formal_arguments, return_type).into();
self.0.extend(self.1.get_function(&identifier).unwrap().pres.clone());
for expr in arguments {
self.walk_expr(expr);
}
},
vir::Expr::DomainFuncApp(vir::DomainFuncApp { arguments, .. }) => {
for expr in arguments {
self.walk_expr(expr);
}
}
vir::Expr::InhaleExhale(ie) => {
self.0.push((*ie.exhale_expr).clone());
}
vir::Expr::Seq(vir::Seq { elements, .. }) => {
for expr in elements {
self.walk_expr(expr);
}
}
vir::Expr::Downcast(vir::DowncastExpr { enum_place, base, .. }) => {
self.walk_expr(&*enum_place);
self.walk_expr(&*base);
self.fold(expr.clone());
}
}
impl<'a, 'b, 'c> ExprFolder for FindFnApps<'a, 'b, 'c> {
fn fold_func_app(&mut self, expr: vir::FuncApp) -> vir::Expr {
let vir::FuncApp { function_name, type_arguments, arguments, formal_arguments, return_type, .. } = expr;
if self.recurse {
let identifier: vir::FunctionIdentifier =
compute_identifier(&function_name, &type_arguments, &formal_arguments, &return_type).into();
let pres = self.encoder.get_function(&identifier).unwrap().pres.clone();
// Avoid recursively collecting preconditions: they should be self-framing anyway
self.recurse = false;
let pres = pres.into_iter().map(|expr| self.fold(expr)).collect::<Vec<_>>();
self.recurse = true;
self.preconds.extend(pres);

for arg in arguments {
self.fold(arg);
}
}
true.into()
}
fn fold_inhale_exhale(&mut self, expr: vir::InhaleExhale) -> vir::Expr {
// We only care about the exhale part (e.g. for `walk_exhale`)
self.fold(*expr.exhale_expr)
}
fn fold_predicate_access_predicate(&mut self, expr: vir::PredicateAccessPredicate) -> vir::Expr {
self.fold(*expr.argument);
true.into()
}
fn fold_field_access_predicate(&mut self, expr: vir::FieldAccessPredicate) -> vir::Expr {
self.fold(*expr.base);
true.into()
}
fn fold_bin_op(&mut self, expr: vir::BinOp) -> vir::Expr {
let vir::BinOp { op_kind, left, right, position } = expr;
let left = self.fold_boxed(left);
let right = self.fold_boxed(right);
match op_kind {
vir::BinaryOpKind::And if is_const_true(&*left) => *right,
vir::BinaryOpKind::And if is_const_true(&*right) => *left,
vir::BinaryOpKind::Or if is_const_true(&*left) => *left,
vir::BinaryOpKind::Or if is_const_true(&*right) => *right,
_ => vir::Expr::BinOp(vir::BinOp {
op_kind, left, right, position,
}),
}
}
}
let mut walker = FindFnApps(Vec::new(), self.encoder);
let mut walker = FindFnApps {
recurse: true, preconds: Vec::new(), encoder: self.encoder
};
walker.walk(stmt);
walker.0.into_iter().filter(|exp| !matches!(
exp,
// Note: This doesn't remove e.g. `true && acc(Pred(...), ...)`
vir::Expr::Const(vir::ConstExpr {
value: vir::Const::Bool(true), ..
})
| vir::Expr::PredicateAccessPredicate(_)
| vir::Expr::FieldAccessPredicate(_)
)
).collect()
walker.preconds.into_iter().filter(|exp| !is_const_true(exp)).collect()
}
fn block_preconditions(&self, block: &CfgBlockIndex) -> Vec<vir::Expr> {
let bb = &self.cfg_method.basic_blocks[block.block_index];