From 133a75fcbb8bfbac892903db9f1052aa988758da Mon Sep 17 00:00:00 2001 From: mimo31 Date: Fri, 14 Jul 2023 14:48:53 +0200 Subject: [PATCH] More misplaced impr. checks; move QR desugaring to a separate module --- prusti-common/src/vir/fixes/mod.rs | 3 +- .../src/vir/fixes/quantified_resources.rs | 197 ++++++++++++++++++ .../vir/optimizations/functions/simplifier.rs | 90 -------- .../fail/obligations/misplaced_impure.rs | 31 ++- .../pass/obligations/impure_placement.rs | 19 ++ .../errors/misplaced_impure_checker.rs | 59 +++++- prusti-viper/src/verifier.rs | 4 +- 7 files changed, 299 insertions(+), 104 deletions(-) create mode 100644 prusti-common/src/vir/fixes/quantified_resources.rs create mode 100644 prusti-tests/tests/verify/pass/obligations/impure_placement.rs diff --git a/prusti-common/src/vir/fixes/mod.rs b/prusti-common/src/vir/fixes/mod.rs index 721d26c9150..2e1103c2af9 100644 --- a/prusti-common/src/vir/fixes/mod.rs +++ b/prusti-common/src/vir/fixes/mod.rs @@ -6,6 +6,7 @@ //! Fix the potentially broken encoding. -pub use self::ghost_vars::fix_ghost_vars; +pub use self::{ghost_vars::fix_ghost_vars, quantified_resources::desugar_quantified_resources}; mod ghost_vars; +mod quantified_resources; diff --git a/prusti-common/src/vir/fixes/quantified_resources.rs b/prusti-common/src/vir/fixes/quantified_resources.rs new file mode 100644 index 00000000000..3b81dac2fea --- /dev/null +++ b/prusti-common/src/vir/fixes/quantified_resources.rs @@ -0,0 +1,197 @@ +// © 2023, ETH Zurich +// +// This Source Code Form is subject to the terms of the Mozilla Public +// 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/. + +//! Desugar quantified permissions syntax. + +use crate::vir::polymorphic_vir::{ + ast, + ast::{ExprFolder, StmtFolder}, + Program, +}; + +/// During the translation step from the parse AST to real Viper AST, +/// Silver desugars the quantified permissions syntax so that all +/// quantified permissions quantifiers have the form forall xs :: +/// c(xs) ==> acc(...) for some condition c and access acc(...). +/// Backend verifiers rely on this and crash otherwise. Since we +/// directly generate Viper AST and in Silver, this desugaring step +/// is built into the Translator (so we can't call it in Silver as a +/// separate pass), we do the desugaring ourselves here. + +pub fn desugar_quantified_resources(program: Program) -> Program { + // add other parts of the Viper program to desugar if needed + let Program { + functions, methods, .. + } = program; + + let desugared_functions = functions + .into_iter() + .map(|f| { + let ast::Function { body, .. } = f; + ast::Function { + body: body.map(|expr| ExprFolder::fold(&mut Desugarer {}, expr)), + ..f + } + }) + .collect::>(); + + let desugared_methods = methods + .into_iter() + .map(|m| m.patch_statements(|stmt| Ok(StmtFolder::fold(&mut Desugarer {}, stmt)))) + .collect::, ()>>() + .unwrap(); + + Program { + functions: desugared_functions, + methods: desugared_methods, + ..program + } +} + +struct Desugarer; + +impl Desugarer { + fn desugar(e: ast::Expr) -> ast::Expr { + match e { + // transform (forall A) into (forall true ==> A) if A is not an implication + ast::Expr::ForAll(ast::ForAll { + variables, + triggers, + body: box body, + position, + }) if !body.is_pure() + && !matches!( + body, + ast::Expr::BinOp(ast::BinOp { + op_kind: ast::BinaryOpKind::Implies, + .. + }) + ) => + { + Self::desugar( + ast::Expr::forall( + variables, + triggers, + ast::Expr::implies(true.into(), body.clone()).set_pos(body.pos()), + ) + .set_pos(position), + ) + } + // transform (forall A ==> B ==> C) into (forall (A && B) ==> C) + ast::Expr::ForAll(ast::ForAll { + variables, + triggers, + body: + box ast::Expr::BinOp(ast::BinOp { + op_kind: ast::BinaryOpKind::Implies, + left: box c0, + right: + box ast::Expr::BinOp(ast::BinOp { + op_kind: ast::BinaryOpKind::Implies, + left: box c1, + right: box ex, + .. + }), + position: pos_body, + }), + position: pos_quant, + }) if !ex.is_pure() => Self::desugar( + ast::Expr::forall( + variables, + triggers, + ast::Expr::implies(ast::Expr::and(c0, c1).set_pos(pos_body), ex) + .set_pos(pos_body), + ) + .set_pos(pos_quant), + ), + // transform (forall A ==> (B ? C : D)) into (forall A ==> ((B ==> C) && (!B ==> D))) + ast::Expr::ForAll(ast::ForAll { + variables, + triggers, + body: + box ast::Expr::BinOp(ast::BinOp { + op_kind: ast::BinaryOpKind::Implies, + left: box filter, + right: + box ast::Expr::Cond(ast::Cond { + guard: box guard, + then_expr: box then_expr, + else_expr: box else_expr, + position: pos_cond, + }), + position: pos_body, + }), + position: pos_quant, + }) if !then_expr.is_pure() || !else_expr.is_pure() => Self::desugar( + ast::Expr::forall( + variables, + triggers, + ast::Expr::implies( + filter, + ast::Expr::and( + ast::Expr::implies(guard.clone(), then_expr).set_pos(pos_cond), + ast::Expr::implies(ast::Expr::not(guard).set_pos(pos_cond), else_expr), + ) + .set_pos(pos_cond), + ) + .set_pos(pos_body), + ) + .set_pos(pos_quant), + ), + // transform (forall A ==> (B && C)) into ((forall A ==> B) && (forall A ==> C)) + ast::Expr::ForAll(ast::ForAll { + variables, + triggers, + body: + box ast::Expr::BinOp(ast::BinOp { + op_kind: ast::BinaryOpKind::Implies, + left: box cond, + right: + box ast::Expr::BinOp(ast::BinOp { + op_kind: ast::BinaryOpKind::And, + left: box part0, + right: box part1, + .. + }), + position: pos_body, + }), + position: pos_quant, + }) if !part0.is_pure() || !part1.is_pure() => ast::Expr::and( + Self::desugar( + ast::Expr::forall( + variables.clone(), + triggers.clone(), + ast::Expr::implies(cond.clone(), part0).set_pos(pos_body), + ) + .set_pos(pos_quant), + ), + Self::desugar( + ast::Expr::forall( + variables, + triggers, + ast::Expr::implies(cond, part1).set_pos(pos_body), + ) + .set_pos(pos_quant), + ), + ) + .set_pos(pos_quant), + r => r, + } + } +} + +impl ExprFolder for Desugarer { + fn fold(&mut self, e: ast::Expr) -> ast::Expr { + let folded_expr = ast::default_fold_expr(self, e); + Self::desugar(folded_expr) + } +} + +impl StmtFolder for Desugarer { + fn fold_expr(&mut self, e: ast::Expr) -> ast::Expr { + ExprFolder::fold(self, e) + } +} diff --git a/prusti-common/src/vir/optimizations/functions/simplifier.rs b/prusti-common/src/vir/optimizations/functions/simplifier.rs index 98a691eee27..876663d3774 100644 --- a/prusti-common/src/vir/optimizations/functions/simplifier.rs +++ b/prusti-common/src/vir/optimizations/functions/simplifier.rs @@ -207,96 +207,6 @@ impl ExprSimplifier { right: Box::new(Self::apply_rules(op2)), position: pos, }), - // the following transformations of foralls are necessary because the verifier backends rely on them (they are normally done by Silver when traslating the parse AST into real Viper AST); - // alternatively, consider calling the Silver functions that do this - // transform (forall A ==> B ==> C) into (forall (A && B) ==> C) - ast::Expr::ForAll(ast::ForAll { - variables, - triggers, - body: - box ast::Expr::BinOp(ast::BinOp { - op_kind: ast::BinaryOpKind::Implies, - left: box c0, - right: - box ast::Expr::BinOp(ast::BinOp { - op_kind: ast::BinaryOpKind::Implies, - left: box c1, - right: box ex, - .. - }), - position: pos_body, - }), - position: pos_quant, - }) if !ex.is_pure() => Self::apply_rules( - ast::Expr::forall( - variables, - triggers, - ast::Expr::implies(ast::Expr::and(c0, c1).set_pos(pos_body), ex) - .set_pos(pos_body), - ) - .set_pos(pos_quant), - ), - // transform (forall A) into (forall true ==> A) if A is not an implication - ast::Expr::ForAll(ast::ForAll { - variables, - triggers, - body: box body, - position, - }) if !body.is_pure() - && !matches!( - body, - ast::Expr::BinOp(ast::BinOp { - op_kind: ast::BinaryOpKind::Implies, - .. - }) - ) => - { - Self::apply_rules( - ast::Expr::forall( - variables, - triggers, - ast::Expr::implies(true.into(), body.clone()).set_pos(body.pos()), - ) - .set_pos(position), - ) - } - // transform (forall A ==> (B && C)) into ((forall A ==> B) && (forall A ==> C)) - ast::Expr::ForAll(ast::ForAll { - variables, - triggers, - body: - box ast::Expr::BinOp(ast::BinOp { - op_kind: ast::BinaryOpKind::Implies, - left: box cond, - right: - box ast::Expr::BinOp(ast::BinOp { - op_kind: ast::BinaryOpKind::And, - left: box part0, - right: box part1, - .. - }), - position: pos_body, - }), - position: pos_quant, - }) if !part0.is_pure() || !part1.is_pure() => ast::Expr::and( - Self::apply_rules( - ast::Expr::forall( - variables.clone(), - triggers.clone(), - ast::Expr::implies(cond.clone(), part0).set_pos(pos_body), - ) - .set_pos(pos_quant), - ), - Self::apply_rules( - ast::Expr::forall( - variables, - triggers, - ast::Expr::implies(cond, part1).set_pos(pos_body), - ) - .set_pos(pos_quant), - ), - ) - .set_pos(pos_quant), r => r, } } diff --git a/prusti-tests/tests/verify/fail/obligations/misplaced_impure.rs b/prusti-tests/tests/verify/fail/obligations/misplaced_impure.rs index 62ebede776c..8cbe2e9b56f 100644 --- a/prusti-tests/tests/verify/fail/obligations/misplaced_impure.rs +++ b/prusti-tests/tests/verify/fail/obligations/misplaced_impure.rs @@ -4,6 +4,15 @@ obligation! { fn alloced(amount: usize, loc: usize); } +#[pure] +fn f(flag: bool) -> bool { + true +} + +resource! { + fn rsrc(amount: usize, flag: bool); +} + #[ensures((result > 0) | alloced(1, 1))] //~ ERROR resource access is illegal inside disjunctions fn f1() -> i32 { 0 } @@ -22,6 +31,26 @@ fn f5() -> i32 { 0 } #[ensures((result > 0) != alloced(1, 1))] //~ ERROR resource access is illegal inside equality comparisons fn f6() -> i32 { 0 } -// TODO add obligations in conditionals to this test +#[ensures(!alloced(1, 1))] //~ ERROR resource access is illegal inside negations +fn f7() -> i32 { 0 } + +#[ensures(f(alloced(1, 1)))] //~ ERROR resource access is illegal inside function arguments +fn f8() -> i32 { 0 } + +#[ensures(rsrc(1, alloced(1, 1)))] //~ ERROR resource access is illegal inside resource access arguments +fn f9() -> i32 { 0 } + +#[ensures(exists(|loc: usize| alloced(1, loc)))] //~ ERROR resource access is illegal inside existential quantifiers +fn f10() -> i32 { 0 } + +// FIXME the following tests report confusing places for where the impurity is + +// TODO add test for resource access in the guard of a conditional when the error messages there are made to work properly in future + +#[ensures(alloced(1, 1) || result > 0)] //~ ERROR resource access is illegal inside +fn f11() -> i32 { 0 } + +#[ensures(alloced(1, 1) && result > 0)] //~ ERROR resource access is illegal inside +fn f12() -> i32 { 0 } fn main() {} diff --git a/prusti-tests/tests/verify/pass/obligations/impure_placement.rs b/prusti-tests/tests/verify/pass/obligations/impure_placement.rs new file mode 100644 index 00000000000..e04dede1fad --- /dev/null +++ b/prusti-tests/tests/verify/pass/obligations/impure_placement.rs @@ -0,0 +1,19 @@ +use prusti_contracts::*; + +obligation! { + fn alloced(amount: usize, loc: usize); +} + +#[requires(a > 0 || alloced(1, 1))] +#[ensures(a > 0 || alloced(1, 1))] +fn f1(a: i32) {} + +#[ensures(a > 0 && alloced(1, 1))] +#[requires(a > 0 && alloced(1, 1))] +fn f2(a: i32) -> i32 { 0 } + +#[ensures(if a > 0 { alloced(1, 1) } else { alloced(33, 42) })] +#[requires(if a > 0 { alloced(1, 1) } else { alloced(33, 42) })] +fn f3(a: i32) -> i32 { 0 } + +fn main() {} diff --git a/prusti-viper/src/encoder/errors/misplaced_impure_checker.rs b/prusti-viper/src/encoder/errors/misplaced_impure_checker.rs index cccbde7ad0f..b3bcb346ab2 100644 --- a/prusti-viper/src/encoder/errors/misplaced_impure_checker.rs +++ b/prusti-viper/src/encoder/errors/misplaced_impure_checker.rs @@ -6,7 +6,7 @@ use std::fmt::Debug; -use vir_crate::polymorphic::{Position, program::Program, CfgMethod, ExprWalker, Expr, BinaryOpKind, BinOp, UnaryOpKind, UnaryOp, Cond, PredicateAccessPredicate, FieldAccessPredicate, ResourceAccessPredicate}; +use vir_crate::polymorphic::{Position, program::Program, CfgMethod, ExprWalker, Expr, BinaryOpKind, BinOp, UnaryOpKind, UnaryOp, Cond, PredicateAccessPredicate, FieldAccessPredicate, ResourceAccessPredicate, FuncApp, ResourceAccess, DomainFuncApp, Exists}; use crate::encoder::errors::PositionManager; use prusti_interface::PrustiError; @@ -51,6 +51,7 @@ impl MisplacedImpureChecker { } fn check_program(&mut self, program: &Program) { + // add other parts of the program to check if needed for method in &program.methods { self.check_method(method); } @@ -64,13 +65,13 @@ impl MisplacedImpureChecker { checker.errors.into_iter().map(|e| e.into_prusti_error(position_manager)).collect() } - fn walk_and_check_for_impurities(&mut self, expr: &Expr, outer_pos: &Position, message: &str) { + fn walk_and_check_for_impurities(&mut self, expr: &Expr, outer_pos: &Position, illegal_inside: &str) { let err_count_before = self.errors.len(); self.walk(expr); let err_count_after = self.errors.len(); if err_count_before == err_count_after { if let Some(impurity_pos) = ImpurityFinder::find_impurity(expr) { - self.errors.push(MisplacedImpureError::new(impurity_pos, *outer_pos, message.to_string())); + self.errors.push(MisplacedImpureError::new(impurity_pos, *outer_pos, format!("resource access is illegal inside {}", illegal_inside))); } } } @@ -80,16 +81,16 @@ impl ExprWalker for MisplacedImpureChecker { fn walk_bin_op(&mut self, BinOp { op_kind, left, right, position }: &BinOp) { match op_kind { BinaryOpKind::Or => { - self.walk_and_check_for_impurities(left, position, "resource access is illegal inside disjunctions"); - self.walk_and_check_for_impurities(right, position, "resource access is illegal inside disjunctions"); + self.walk_and_check_for_impurities(left, position, "disjunctions"); + self.walk_and_check_for_impurities(right, position, "disjunctions"); } BinaryOpKind::Implies => { - self.walk_and_check_for_impurities(left, position, "resource access is illegal on the left-hand side of implications"); + self.walk_and_check_for_impurities(left, position, "the antecedents of implications"); self.walk(right) } BinaryOpKind::EqCmp | BinaryOpKind::NeCmp => { - self.walk_and_check_for_impurities(left, position, "resource access is illegal inside equality comparisons"); - self.walk_and_check_for_impurities(right, position, "resource access is illegal inside equality comparisons"); + self.walk_and_check_for_impurities(left, position, "equality comparisons"); + self.walk_and_check_for_impurities(right, position, "equality comparisons"); } _ => { self.walk(left); @@ -101,7 +102,7 @@ impl ExprWalker for MisplacedImpureChecker { fn walk_unary_op(&mut self, UnaryOp { op_kind, argument, position }: &UnaryOp) { match op_kind { UnaryOpKind::Not => { - self.walk_and_check_for_impurities(argument, position, "resource access is illegal inside negations"); + self.walk_and_check_for_impurities(argument, position, "negations"); } _ => { self.walk(argument); @@ -110,10 +111,48 @@ impl ExprWalker for MisplacedImpureChecker { } fn walk_cond(&mut self, Cond { guard, then_expr, else_expr, position }: &Cond) { - self.walk_and_check_for_impurities(guard, position, "resource access is illegal in guards of conditionals"); + self.walk_and_check_for_impurities(guard, position, "guards of conditionals"); self.walk(then_expr); self.walk(else_expr); } + + fn walk_func_app(&mut self, FuncApp { + arguments, + position, + .. + }: &FuncApp) { + for arg in arguments { + self.walk_and_check_for_impurities(arg, position, "function arguments"); + } + } + + fn walk_domain_func_app(&mut self, DomainFuncApp { + arguments, + position, + .. + }: &DomainFuncApp) { + for arg in arguments { + self.walk_and_check_for_impurities(arg, position, "function arguments"); + } + } + + fn walk_resource_access(&mut self, ResourceAccess { + args, + position, + .. + }: &ResourceAccess) { + for arg in args { + self.walk_and_check_for_impurities(arg, position, "resource access arguments"); + } + } + + fn walk_exists(&mut self, Exists { + body, + position, + .. + }: &Exists) { + self.walk_and_check_for_impurities(body, position, "existential quantifiers"); + } } struct ImpurityFinder { diff --git a/prusti-viper/src/verifier.rs b/prusti-viper/src/verifier.rs index 04b52f4c4a6..77c20a863c4 100644 --- a/prusti-viper/src/verifier.rs +++ b/prusti-viper/src/verifier.rs @@ -13,7 +13,7 @@ use once_cell::sync::Lazy; use prusti_common::{ config, report::log, - vir::{optimizations::optimize_program, program::Program}, + vir::{optimizations::optimize_program, fixes::desugar_quantified_resources, program::Program}, Stopwatch, }; use prusti_interface::{ @@ -100,7 +100,7 @@ impl<'v, 'tcx> Verifier<'v, 'tcx> { } let mut programs: Vec = optimized_polymorphic_programs.into_iter() - .map(|program| Program::Legacy(program.into())) + .map(|program| Program::Legacy(desugar_quantified_resources(program).into())) .collect(); programs.extend(self.encoder.get_core_proof_programs());