From c03343666806db7d32954f6e67e51e9933b59250 Mon Sep 17 00:00:00 2001 From: Pialex99 Date: Wed, 11 Jan 2023 10:46:32 +0100 Subject: [PATCH] Pull request reviews --- docs/dev-guide/src/config/flags.md | 9 +++++ .../vir/optimizations/functions/simplifier.rs | 7 ++-- .../src/vir/optimizations/methods/mod.rs | 4 +-- .../vir/optimizations/methods/simplifier.rs | 9 +++-- .../predicates/delete_unused_predicates.rs | 8 ++--- prusti-common/src/vir/to_viper.rs | 3 +- .../verify/fail/time-resources/array_cmp.rs | 4 ++- .../tests/verify/fail/time-resources/loop.rs | 26 ++++++++++---- .../fail/time-resources/only_lower_bound.rs | 13 +++---- .../verify/pass/time-resources/array_2d.rs | 6 ++-- .../verify/pass/time-resources/array_cmp.rs | 35 ++++++++++--------- .../time-resources/ensures_time_credits.rs | 3 +- .../tests/verify/pass/time-resources/flag.rs | 18 ---------- .../tests/verify/pass/time-resources/impl.rs | 4 +-- .../tests/verify/pass/time-resources/loop.rs | 16 +++++---- .../tests/verify/pass/time-resources/rec.rs | 12 ++++--- .../tests/verify/pass/time-resources/res.rs | 3 +- prusti-utils/src/config.rs | 9 +++-- .../src/encoder/errors/error_manager.rs | 14 ++++---- .../src/encoder/foldunfold/requirements.rs | 10 ++---- .../mir/pure/specifications/encoder_poly.rs | 18 ++++------ .../mir/pure/specifications/interface.rs | 11 ++++-- prusti-viper/src/encoder/procedure_encoder.rs | 3 +- vir/defs/polymorphic/ast/common.rs | 2 +- vir/defs/polymorphic/ast/expr.rs | 1 - vir/src/legacy/ast/expr.rs | 1 - 26 files changed, 134 insertions(+), 115 deletions(-) delete mode 100644 prusti-tests/tests/verify/pass/time-resources/flag.rs diff --git a/docs/dev-guide/src/config/flags.md b/docs/dev-guide/src/config/flags.md index 4087f0d856a..ecc6ab1f726 100644 --- a/docs/dev-guide/src/config/flags.md +++ b/docs/dev-guide/src/config/flags.md @@ -70,6 +70,7 @@ | [`SMT_SOLVER_WRAPPER_PATH`](#smt_solver_wrapper_path) | `Option` | `None` | A | | [`SMT_UNIQUE_TRIGGERS_BOUND`](#smt_unique_triggers_bound) | `Option` | `None` | A | | [`SMT_UNIQUE_TRIGGERS_BOUND_TOTAL`](#smt_unique_triggers_bound_total) | `Option` | `None` | A | +| [`TIME_REASONING`](#time_reasoning) | `bool` | `false` | A | | [`UNSAFE_CORE_PROOF`](#unsafe_core_proof) | `bool` | `false` | A | | [`USE_MORE_COMPLETE_EXHALE`](#use_more_complete_exhale) | `bool` | `true` | A | | [`USE_SMT_WRAPPER`](#use_smt_wrapper) | `bool` | `false` | A | @@ -320,6 +321,7 @@ Comma-separated list of optimizations to enable, or `"all"` to enable all. Possi - `"purify_vars"` - `"fix_quantifiers"` - `"fix_unfoldings"` +- `"simplify_exprs"` - `"remove_unused_vars"` - `"remove_trivial_assertions"` - `"clean_cfg"` @@ -439,6 +441,13 @@ If not `None`, checks that the total number of unique triggers reported by the S > **Note:** Requires `USE_SMT_WRAPPER` to be `true`. +## `TIME_REASONING` + +When enabled, the `time_credits` and `time_receipts` predicates are usable and functions' and loops' bodies will concume time credits and produce time receipts. + +> **Note:** This is an experimental feature. +> **Note:** Requires `SIMPLIFY_ENCODING` to be `true` and the `simplify_exprs` optimization to be enabled. + ## `UNSAFE_CORE_PROOF` When enabled, the new core proof is used, suitable for unsafe code diff --git a/prusti-common/src/vir/optimizations/functions/simplifier.rs b/prusti-common/src/vir/optimizations/functions/simplifier.rs index 115a0d8af33..1d2e83e6177 100644 --- a/prusti-common/src/vir/optimizations/functions/simplifier.rs +++ b/prusti-common/src/vir/optimizations/functions/simplifier.rs @@ -99,8 +99,7 @@ impl ExprSimplifier { } else { Into::::into(false).set_pos(inner_pos) } - .set_default_pos(pos) - .set_default_pos(inner_pos), + .set_default_pos(pos), ast::Expr::BinOp(ast::BinOp { op_kind: ast::BinaryOpKind::Or, left: @@ -125,8 +124,7 @@ impl ExprSimplifier { } else { disjunct } - .set_default_pos(pos) - .set_default_pos(inner_pos), + .set_default_pos(pos), ast::Expr::BinOp(ast::BinOp { op_kind: ast::BinaryOpKind::Implies, left: guard, @@ -160,7 +158,6 @@ impl ExprSimplifier { } else { Into::::into(true).set_pos(inner_pos) } - .set_default_pos(inner_pos) .set_default_pos(pos), ast::Expr::BinOp(ast::BinOp { op_kind: ast::BinaryOpKind::And, diff --git a/prusti-common/src/vir/optimizations/methods/mod.rs b/prusti-common/src/vir/optimizations/methods/mod.rs index be75e899679..e80c6984448 100644 --- a/prusti-common/src/vir/optimizations/methods/mod.rs +++ b/prusti-common/src/vir/optimizations/methods/mod.rs @@ -21,7 +21,7 @@ use crate::{config::Optimizations, vir::polymorphic_vir::cfg::CfgMethod}; use self::{ assert_remover::remove_trivial_assertions, cfg_cleaner::clean_cfg, empty_if_remover::remove_empty_if, purifier::purify_vars, quantifier_fixer::fix_quantifiers, - simplifier::simplify_expr, unfolding_fixer::fix_unfoldings, var_remover::remove_unused_vars, + simplifier::simplify_exprs, unfolding_fixer::fix_unfoldings, var_remover::remove_unused_vars, }; #[allow(clippy::let_and_return)] @@ -58,7 +58,7 @@ pub fn optimize_method_encoding( }; let cfg = apply!(fix_unfoldings, cfg); let cfg = apply!(fix_quantifiers, cfg); - let cfg = apply!(simplify_expr, cfg); + let cfg = apply!(simplify_exprs, cfg); let cfg = apply!(remove_empty_if, cfg); let cfg = apply!(remove_unused_vars, cfg); let cfg = apply!(remove_trivial_assertions, cfg); diff --git a/prusti-common/src/vir/optimizations/methods/simplifier.rs b/prusti-common/src/vir/optimizations/methods/simplifier.rs index 1db69a7f8ab..16c3ab4cbc6 100644 --- a/prusti-common/src/vir/optimizations/methods/simplifier.rs +++ b/prusti-common/src/vir/optimizations/methods/simplifier.rs @@ -10,10 +10,13 @@ use vir::polymorphic::*; use crate::vir::optimizations::functions::Simplifier; -/// This optimization transformes ors were the RHS is impure into implications. -/// This happens in the case of an implication with a resource access predicate in the RHS. +/// This optimization simplifies all expressions in a method. +/// It is required when resource access predicates appear on the RHS of +/// implications as implications are transformed into ors which need to be +/// transformed back into implications otherwise, we would have an impure +/// expression in ors which is disallowed in Viper. -pub fn simplify_expr(mut cfg: CfgMethod) -> CfgMethod { +pub fn simplify_exprs(mut cfg: CfgMethod) -> CfgMethod { debug!("Simplifying exprs in {}", cfg.name()); let mut sentinel_stmt = Stmt::comment("moved out stmt"); for block in &mut cfg.basic_blocks { diff --git a/prusti-common/src/vir/optimizations/predicates/delete_unused_predicates.rs b/prusti-common/src/vir/optimizations/predicates/delete_unused_predicates.rs index 687eeb4bfaa..797cac11b66 100644 --- a/prusti-common/src/vir/optimizations/predicates/delete_unused_predicates.rs +++ b/prusti-common/src/vir/optimizations/predicates/delete_unused_predicates.rs @@ -15,12 +15,12 @@ use log::debug; fn collect_info_from_methods_and_functions( methods: &[CfgMethod], functions: &[Function], - buildin_methods: &[BodylessMethod], + builtin_methods: &[BodylessMethod], ) -> UsedPredicateCollector { let mut collector = UsedPredicateCollector::new(); walk_methods(methods, &mut collector); walk_functions(functions, &mut collector); - walk_builtin_methods(buildin_methods, &mut collector); + walk_builtin_methods(builtin_methods, &mut collector); // DeadBorrowToken$ is a used predicate but it does not appear in VIR // becaue it is only created when viper code is created from VIR @@ -110,10 +110,10 @@ fn visit_predicate( pub fn delete_unused_predicates( methods: &[CfgMethod], functions: &[Function], - buildin_methods: &[BodylessMethod], + builtin_methods: &[BodylessMethod], mut predicates: Vec, ) -> Vec { - let collector = collect_info_from_methods_and_functions(methods, functions, buildin_methods); + let collector = collect_info_from_methods_and_functions(methods, functions, builtin_methods); let used_predicates_in_functions_and_methods = collector.used_predicates; let folded_predicates = collector.folded_predicates; let mut predicates_in_predicates_map = get_used_predicates_in_predicate_map(&predicates); diff --git a/prusti-common/src/vir/to_viper.rs b/prusti-common/src/vir/to_viper.rs index ae3889d1f49..af0eb8cac30 100644 --- a/prusti-common/src/vir/to_viper.rs +++ b/prusti-common/src/vir/to_viper.rs @@ -403,10 +403,9 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for Expr { pos.to_viper(context, ast), ), Expr::ResourceAccessPredicate(ref resource_name, ref amount, ref pos) => { - // Resource are encoded as a predicate with no arguments + // resources are encoded as predicates with no arguments ast.predicate_access_predicate_with_pos( ast.predicate_access(&[], resource_name), - // ast.int_perm_mul(amount.to_viper(context, ast), ast.full_perm()), ast.fractional_perm(amount.to_viper(context, ast), ast.int_lit(1)), pos.to_viper(context, ast), ) diff --git a/prusti-tests/tests/verify/fail/time-resources/array_cmp.rs b/prusti-tests/tests/verify/fail/time-resources/array_cmp.rs index 5a4e729f8d1..c2c756552a4 100644 --- a/prusti-tests/tests/verify/fail/time-resources/array_cmp.rs +++ b/prusti-tests/tests/verify/fail/time-resources/array_cmp.rs @@ -8,6 +8,8 @@ use prusti_contracts::*; fn opt_array_cmp(a: &[T], b: &[T]) -> bool { //~ ERROR Not enough time receipts at the end of the function. let mut i = 0; while i < a.len() { + body_invariant!(time_credits(a.len() - i)); + body_invariant!(time_receipts(i)); if a[i] != b[i] { return false; } @@ -17,4 +19,4 @@ fn opt_array_cmp(a: &[T], b: &[T]) -> bool { //~ ERROR Not enough time re } #[requires(time_credits(1))] -fn main() {} \ No newline at end of file +fn main() {} diff --git a/prusti-tests/tests/verify/fail/time-resources/loop.rs b/prusti-tests/tests/verify/fail/time-resources/loop.rs index 70ed3772324..3bbefeb89c5 100644 --- a/prusti-tests/tests/verify/fail/time-resources/loop.rs +++ b/prusti-tests/tests/verify/fail/time-resources/loop.rs @@ -2,8 +2,7 @@ use prusti_contracts::*; -// TODO: specify the error as: Not enough time receipts/credits - +#[requires(n > 0)] #[requires(time_credits(n as usize + 2))] #[ensures(time_receipts(n as usize + 1))] // This is also an error but the other is reported first. fn sum(n: u32) -> u32 { @@ -11,13 +10,25 @@ fn sum(n: u32) -> u32 { let mut res = 0; while 0 < i { body_invariant!(time_credits(i as usize)); //~ ERROR Not enough time receipts for invariant in the first loop iteration. - body_invariant!(time_receipts(1 + (n - i) as usize)); + body_invariant!(time_receipts((n - i) as usize)); res += i; i -= 1; } res } +#[requires(time_credits(3))] +fn sum2(n: usize) -> usize { + let mut i = 0; + let mut res = 0; + while i < n { + body_invariant!(time_credits(1)); //~ ERROR Not enough time credits + i += 1; + res += i; + } + res +} + #[requires(time_credits(1))] #[ensures(time_receipts(1))] fn foo() -> usize { @@ -30,7 +41,8 @@ fn loop_foo(n: usize) -> usize { let mut i = 0; let mut res = 0; while i < n { - body_invariant!(time_receipts(i + 1)); + body_invariant!(time_credits(n - i)); + body_invariant!(time_receipts(i)); res += i; i += 1; } @@ -44,13 +56,15 @@ fn loop_foo_loop(n: usize) -> usize { let mut i = 0; let mut res = 0; while i < n { - body_invariant!(time_receipts(i + 1)); + body_invariant!(time_credits(n - i)); + body_invariant!(time_receipts(i)); res += i; i += 1; } res += foo(); // this is also an error but the other is reported first. while 0 < i { - body_invariant!(time_receipts(2 * n - i + 2)); //~ ERROR Not enough time credits. + body_invariant!(time_receipts(n - i)); //~ ERROR Not enough time credits + body_invariant!(time_credits(i)); res += 1; i -= 1; } diff --git a/prusti-tests/tests/verify/fail/time-resources/only_lower_bound.rs b/prusti-tests/tests/verify/fail/time-resources/only_lower_bound.rs index 70c070b2968..b070f72ddf1 100644 --- a/prusti-tests/tests/verify/fail/time-resources/only_lower_bound.rs +++ b/prusti-tests/tests/verify/fail/time-resources/only_lower_bound.rs @@ -4,11 +4,8 @@ use prusti_contracts::*; // This tests that omitting the upper bound fails #[ensures(time_receipts(1))] -fn main() { //~ ERROR Not enough time credits. - let mut i = 0; - let mut _n = 0; - while i < 42 { - _n += 1; - i += 1; - } -} \ No newline at end of file +fn main() {//~ ERROR Not enough time credits. + let mut i = 0; + let mut _n = 0; + i += 42; +} diff --git a/prusti-tests/tests/verify/pass/time-resources/array_2d.rs b/prusti-tests/tests/verify/pass/time-resources/array_2d.rs index fb15f1f989a..8d34216a5f0 100644 --- a/prusti-tests/tests/verify/pass/time-resources/array_2d.rs +++ b/prusti-tests/tests/verify/pass/time-resources/array_2d.rs @@ -12,10 +12,12 @@ fn sum_2d(a: &[&[u32]]) -> u32 { let mut i = 0; let mut res = 0; while i < a.len() { - body_invariant!(time_receipts(i * a[i].len() + 1)); + body_invariant!(time_credits((a.len() - i) * a[i].len())); + body_invariant!(time_receipts(i * a[i].len())); let mut j = 0; while j < a[i].len() { - body_invariant!(time_receipts(i * a[i].len() + j + 1)); + body_invariant!(time_credits(a[i].len() - j)); + body_invariant!(time_receipts(j)); res += a[i][j]; j += 1; } diff --git a/prusti-tests/tests/verify/pass/time-resources/array_cmp.rs b/prusti-tests/tests/verify/pass/time-resources/array_cmp.rs index 32a9b05062e..d11e475ec80 100644 --- a/prusti-tests/tests/verify/pass/time-resources/array_cmp.rs +++ b/prusti-tests/tests/verify/pass/time-resources/array_cmp.rs @@ -6,29 +6,32 @@ use prusti_contracts::*; #[requires(time_credits(a.len() + 1))] #[ensures(time_receipts(a.len() + 1))] fn safe_array_cmp(a: &[T], b: &[T]) -> bool { - let mut i = 0; - let mut res = true; - while i < a.len() { - body_invariant!(time_receipts(i + 1)); - res &= a[i] == b[i]; - i += 1; - } - return res; + let mut i = 0; + let mut res = true; + while i < a.len() { + body_invariant!(time_credits(a.len() - i)); + body_invariant!(time_receipts(i)); + res &= a[i] == b[i]; + i += 1; + } + return res; } #[requires(a.len() == b.len())] #[requires(time_credits(a.len() + 1))] #[ensures(time_receipts(1))] fn opt_array_cmp(a: &[T], b: &[T]) -> bool { - let mut i = 0; - while i < a.len() { - if a[i] != b[i] { - return false; + let mut i = 0; + while i < a.len() { + body_invariant!(time_credits(a.len() - i)); + body_invariant!(time_receipts(i)); + if a[i] != b[i] { + return false; + } + i += 1; } - i += 1; - } - return true; + return true; } #[requires(time_credits(1))] -fn main() {} \ No newline at end of file +fn main() {} diff --git a/prusti-tests/tests/verify/pass/time-resources/ensures_time_credits.rs b/prusti-tests/tests/verify/pass/time-resources/ensures_time_credits.rs index 68dc5a175ae..012c0cb5de5 100644 --- a/prusti-tests/tests/verify/pass/time-resources/ensures_time_credits.rs +++ b/prusti-tests/tests/verify/pass/time-resources/ensures_time_credits.rs @@ -9,7 +9,8 @@ fn bounded_sum(a: &[usize], bound: usize) -> (usize, usize) { let mut i = 0; let mut sum = 0; while i < a.len() && i < bound { - body_invariant!(time_receipts(i + 1)); + body_invariant!(time_credits(bound - i)); + body_invariant!(time_receipts(i)); sum += a[i]; i += 1; } diff --git a/prusti-tests/tests/verify/pass/time-resources/flag.rs b/prusti-tests/tests/verify/pass/time-resources/flag.rs deleted file mode 100644 index 0902ea8ed9f..00000000000 --- a/prusti-tests/tests/verify/pass/time-resources/flag.rs +++ /dev/null @@ -1,18 +0,0 @@ -// compile-flags: -Ptime_reasoning=false - -use prusti_contracts::*; - -// This test checks that setting the time reasoning option to false ignores timing constrains -fn sum(n: u32) -> u32 { - let mut i = 0; - let mut res = 0; - while i < n { - res += i; - i += 1; - } - res -} - -fn main() { - sum(4); -} diff --git a/prusti-tests/tests/verify/pass/time-resources/impl.rs b/prusti-tests/tests/verify/pass/time-resources/impl.rs index 59a38479062..f66dfd3715a 100644 --- a/prusti-tests/tests/verify/pass/time-resources/impl.rs +++ b/prusti-tests/tests/verify/pass/time-resources/impl.rs @@ -9,7 +9,7 @@ fn sum(n: i32) -> i32 { let mut res = 0; while i < n { body_invariant!(time_credits((n - i) as usize)); - body_invariant!(time_receipts(i as usize + 1)); + body_invariant!(time_receipts(i as usize)); res += i; i += 1; } @@ -25,7 +25,7 @@ fn sum2(n: i32) -> i32 { let mut res = 0; while i < n { body_invariant!(time_credits((n - i) as usize)); - body_invariant!(time_receipts(i as usize + 1)); + body_invariant!(time_receipts(i as usize)); res += i; i += 1; } diff --git a/prusti-tests/tests/verify/pass/time-resources/loop.rs b/prusti-tests/tests/verify/pass/time-resources/loop.rs index 1249cf40d5a..02ac150f395 100644 --- a/prusti-tests/tests/verify/pass/time-resources/loop.rs +++ b/prusti-tests/tests/verify/pass/time-resources/loop.rs @@ -9,7 +9,7 @@ fn sum(n: u32) -> u32 { let mut res = 0; while i < n { body_invariant!(time_credits((n - i) as usize)); - body_invariant!(time_receipts(i as usize + 1)); + body_invariant!(time_receipts(i as usize)); res += i; i += 1; } @@ -23,7 +23,7 @@ fn sum2(n: u32) -> u32 { let mut res = 0; while 0 < i { body_invariant!(time_credits(i as usize)); - body_invariant!(time_receipts(1 + (n - i) as usize)); + body_invariant!(time_receipts((n - i) as usize)); res += i; i -= 1; } @@ -36,7 +36,8 @@ fn double_loop(n: usize) -> u32 { let mut i = 0; let mut res = 0; while i < n { - body_invariant!(time_receipts(i * (n + 2) + 1)); + body_invariant!(time_credits((n - i) * (n + 2))); + body_invariant!(time_receipts(i * (n + 2))); res += sum(n as u32); i += 1; } @@ -55,7 +56,8 @@ fn loop_foo(n: usize) -> usize { let mut i = 0; let mut res = 0; while i < n { - body_invariant!(time_receipts(i + 1)); + body_invariant!(time_credits(n - i)); + body_invariant!(time_receipts(i)); res += i; i += 1; } @@ -70,13 +72,15 @@ fn loop_foo_loop_foo(n: usize) -> usize { let mut i = 0; let mut res = 0; while i < n { - body_invariant!(time_receipts(i + 1)); + body_invariant!(time_credits(n - i)); + body_invariant!(time_receipts(i)); res += i; i += 1; } res += foo(); while 0 < i { - body_invariant!(time_receipts(2 * n - i + 2)); + body_invariant!(time_credits(i)); + body_invariant!(time_receipts(n - i)); res += 1; i -= 1; } diff --git a/prusti-tests/tests/verify/pass/time-resources/rec.rs b/prusti-tests/tests/verify/pass/time-resources/rec.rs index 361eb29d677..2789666154f 100644 --- a/prusti-tests/tests/verify/pass/time-resources/rec.rs +++ b/prusti-tests/tests/verify/pass/time-resources/rec.rs @@ -6,9 +6,8 @@ use prusti_contracts::*; impl usize { #[pure] #[ensures(self.pow(n) * self == self.pow(n + 1))] - #[ensures(2_usize.pow(n) + 2_usize.pow(n) == 2_usize.pow(n + 1))] - #[ensures(2_usize.pow(n) + 2_usize.pow(n + 1) <= 2_usize.pow(n + 2))] - #[ensures(result >= 1)] + #[ensures(self >= 1 ==> result >= 1)] + #[ensures(self >= 1 ==> self.pow(0) == 1)] fn pow(self, n: u32) -> usize; } @@ -21,5 +20,8 @@ fn fib(n: usize) -> usize { } } -#[requires(time_credits(1))] -fn main() {} +#[requires(time_credits(50))] +fn main() { + // consumes 32 credits + fib(5); +} diff --git a/prusti-tests/tests/verify/pass/time-resources/res.rs b/prusti-tests/tests/verify/pass/time-resources/res.rs index f4ee8b132c0..317ba3ec431 100644 --- a/prusti-tests/tests/verify/pass/time-resources/res.rs +++ b/prusti-tests/tests/verify/pass/time-resources/res.rs @@ -10,7 +10,8 @@ fn bounded_sum(a: &[usize], bound: usize) -> (usize, usize) { let mut i = 0; let mut sum = 0; while i < a.len() && i < bound { - body_invariant!(time_receipts(i + 1)); + body_invariant!(time_credits(bound - i)); + body_invariant!(time_receipts(i)); sum += a[i]; i += 1; } diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index 13faa841e11..40e827f0530 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -23,7 +23,7 @@ pub struct Optimizations { pub purify_vars: bool, pub fix_quantifiers: bool, pub fix_unfoldings: bool, - pub simplify_expr: bool, + pub simplify_exprs: bool, pub remove_unused_vars: bool, pub remove_trivial_assertions: bool, pub clean_cfg: bool, @@ -39,7 +39,7 @@ impl Optimizations { purify_vars: false, fix_quantifiers: false, fix_unfoldings: false, - simplify_expr: false, + simplify_exprs: false, remove_unused_vars: false, remove_trivial_assertions: false, clean_cfg: false, @@ -56,7 +56,7 @@ impl Optimizations { fix_quantifiers: true, // Disabled because https://github.com/viperproject/prusti-dev/issues/892 has been fixed fix_unfoldings: false, - simplify_expr: true, + simplify_exprs: true, remove_unused_vars: true, remove_trivial_assertions: true, clean_cfg: true, @@ -369,6 +369,7 @@ pub fn check_panics() -> bool { } /// When enabled, the time reasoning constrains are verified. Otherwise they are ignored. +/// Note that this is an experimental feature. pub fn time_reasoning() -> bool { read_setting("time_reasoning") } @@ -705,6 +706,7 @@ pub fn verify_only_basic_block_path() -> Vec { /// - `"purify_vars"` /// - `"fix_quantifiers"` /// - `"fix_unfoldings"` +/// - `"simplify_exprs"` /// - `"remove_unused_vars"` /// - `"remove_trivial_assertions"` /// - `"clean_cfg"` @@ -724,6 +726,7 @@ pub fn optimizations() -> Optimizations { "purify_vars" => opt.purify_vars = true, "fix_quantifiers" => opt.fix_quantifiers = true, "fix_unfoldings" => opt.fix_unfoldings = true, + "simplify_exprs" => opt.simplify_exprs = true, "remove_unused_vars" => opt.remove_unused_vars = true, "remove_trivial_assertions" => opt.remove_trivial_assertions = true, "clean_cfg" => opt.clean_cfg = true, diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index 11f39eb8f3c..24440370972 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -177,7 +177,7 @@ pub enum ErrorCtxt { /// The state that fold-unfold algorithm deduced as unreachable, is actually /// reachable. UnreachableFoldingState, - // There is not enough time credtis to execute this code. + // There is not enough time credits to execute this code. NotEnoughTimeCredits, // The code did not create enough time receipts. NotEnoughTimeReceipts, @@ -350,8 +350,8 @@ impl<'tcx> ErrorManager<'tcx> { ) .set_help( "This could be caused by too small assertion timeout. \ - Try increasing it by setting the configuration parameter \ - ASSERT_TIMEOUT to a larger value.", + Try increasing it by setting the configuration parameter \ + ASSERT_TIMEOUT to a larger value.", ), None => PrustiError::internal( format!( @@ -362,8 +362,8 @@ impl<'tcx> ErrorManager<'tcx> { ) .set_help( "This could be caused by too small assertion timeout. \ - Try increasing it by setting the configuration parameter \ - ASSERT_TIMEOUT to a larger value.", + Try increasing it by setting the configuration parameter \ + ASSERT_TIMEOUT to a larger value.", ), } } @@ -722,7 +722,9 @@ impl<'tcx> ErrorManager<'tcx> { PrustiError::verification("Not enough time receipts.".to_string(), error_span) } - // TODO: this is a temporary fix for detecting time credits/receipts errors + // TODO: this is a temporary fix for detecting time credits/receipts errors. + // Ideally time credits/receipts errors should have the `NotEnoughTimeCredits`/`NotEnoughTimeReceipts` error context and would be + // handled by the previous cases. For this we need to be able to debug the positions that are given to Viper. ("exhale.failed:insufficient.permission", ErrorCtxt::ExhaleMethodPrecondition) if ver_error.message.contains("There might be insufficient permission to access time_credits()") => { PrustiError::verification("Not enough time credits to call function.".to_string(), error_span) } diff --git a/prusti-viper/src/encoder/foldunfold/requirements.rs b/prusti-viper/src/encoder/foldunfold/requirements.rs index 9f677677624..bbb5c96d099 100644 --- a/prusti-viper/src/encoder/foldunfold/requirements.rs +++ b/prusti-viper/src/encoder/foldunfold/requirements.rs @@ -91,17 +91,13 @@ impl RequiredStmtPermissionsGetter for vir::Stmt { ref targets, .. }) => { - // Preconditions and postconditions are empty or does not require permissions - let arguments_perm = arguments - .iter() - .map(|expr| expr.get_required_stmt_permissions(predicates).into_iter()) - .flatten(); + // Preconditions and postconditions are empty + assert!(arguments.is_empty()); FxHashSet::from_iter( targets .iter() .cloned() - .map(|v| Acc(vir::Expr::local(v), PermAmount::Write)) - .chain(arguments_perm), + .map(|v| Acc(vir::Expr::local(v), PermAmount::Write)), ) } diff --git a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs index 9d655642789..bde1486aa41 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs @@ -127,13 +127,6 @@ pub(super) fn inline_spec_item<'tcx>( .replace_multiple_places(&body_replacements)) } -fn error_ctxt(resource_type: &vir_crate::polymorphic::ResourceType) -> ErrorCtxt { - match resource_type { - vir_crate::polymorphic::ResourceType::TimeCredits => ErrorCtxt::NotEnoughTimeCredits, - vir_crate::polymorphic::ResourceType::TimeReceipts => ErrorCtxt::NotEnoughTimeReceipts, - } -} - pub(super) fn encode_time_specifications<'tcx>( encoder: &Encoder<'_, 'tcx>, amount: &vir_crate::polymorphic::Expr, @@ -141,10 +134,13 @@ pub(super) fn encode_time_specifications<'tcx>( parent_def_id: DefId, span: Span, ) -> vir_crate::polymorphic::Expr { - let pos = - encoder - .error_manager() - .register_error(span, error_ctxt(&resource_type), parent_def_id); + let error_ctxt = match resource_type { + vir_crate::polymorphic::ResourceType::TimeCredits => ErrorCtxt::NotEnoughTimeCredits, + vir_crate::polymorphic::ResourceType::TimeReceipts => ErrorCtxt::NotEnoughTimeReceipts, + }; + let pos = encoder + .error_manager() + .register_error(span, error_ctxt, parent_def_id); let amount_non_negative = vir_crate::polymorphic::Expr::ge_cmp(amount.clone(), 0.into()); let resource_access_predicate = vir_crate::polymorphic::Expr::resource_access_predicate(resource_type, amount.clone()) diff --git a/prusti-viper/src/encoder/mir/pure/specifications/interface.rs b/prusti-viper/src/encoder/mir/pure/specifications/interface.rs index a639687dfbc..f20935913aa 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/interface.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/interface.rs @@ -5,7 +5,7 @@ // file, You can obtain one at http://mozilla.org/MPL/2.0/. use crate::encoder::{ - errors::{SpannedEncodingResult, WithSpan}, + errors::{SpannedEncodingError, SpannedEncodingResult, WithSpan}, mir::{ places::PlacesEncoderInterface, pure::{ @@ -268,7 +268,14 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod span, )) } else { - Ok(true.into()) + let mut error = SpannedEncodingError::unsupported( + "Time reasoning is disabled but found a call to a time_credits/time_receipts predicate.", + span + ); + error.set_help( + "To enable time reasoning set the TIME_REASONING option to true.", + ); + Err(error) } } _ => unimplemented!(), diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 7b184697171..6f541bb83e2 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -476,7 +476,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { self.encode_preconditions(start_cfg_block, precondition_weakening)?; if config::time_reasoning() { - // If time reasoning is enabled, add a call to tick after preconditions + // consume a time credits and produce a time receipt in the body of the function self.cfg_method.add_stmts(start_cfg_block, self.get_tick_call(self.mir.span, 1)); } @@ -943,6 +943,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { let (mut stmts, fnspec_span) = self.encode_loop_invariant_inhale_fnspec_stmts(loop_head, before_invariant_block, false)?; if config::time_reasoning() { + // consume a time credit and produce a time receipt at each iteration of the loop stmts.extend(self.get_tick_call(fnspec_span.clone(), 1).into_iter()); } self.cfg_method.add_stmts(inv_post_block_fnspc, stmts); fnspec_span diff --git a/vir/defs/polymorphic/ast/common.rs b/vir/defs/polymorphic/ast/common.rs index f83a4d54f47..615d7698e69 100644 --- a/vir/defs/polymorphic/ast/common.rs +++ b/vir/defs/polymorphic/ast/common.rs @@ -512,7 +512,7 @@ impl ResourceType { "prusti_contracts::time_credits" => ResourceType::TimeCredits, "prusti_contracts::time_receipts" => ResourceType::TimeReceipts, _ => unreachable!( - "Fonction name: {} does not match any resource type.", + "Function name: {} does not match any resource type.", function_name ), } diff --git a/vir/defs/polymorphic/ast/expr.rs b/vir/defs/polymorphic/ast/expr.rs index 5e25a29c188..8ebcc4633f1 100644 --- a/vir/defs/polymorphic/ast/expr.rs +++ b/vir/defs/polymorphic/ast/expr.rs @@ -634,7 +634,6 @@ impl Expr { pub fn is_only_permissions(&self) -> bool { match self { Expr::PredicateAccessPredicate(..) - // TODO check this not sure | Expr::ResourceAccessPredicate(..) | Expr::FieldAccessPredicate(..) => true, Expr::BinOp(BinOp { diff --git a/vir/src/legacy/ast/expr.rs b/vir/src/legacy/ast/expr.rs index 9c4996acf49..43f1505452f 100644 --- a/vir/src/legacy/ast/expr.rs +++ b/vir/src/legacy/ast/expr.rs @@ -786,7 +786,6 @@ impl Expr { pub fn is_only_permissions(&self) -> bool { match self { Expr::PredicateAccessPredicate(..) - // TODO check this not sure | Expr::ResourceAccessPredicate(..) | Expr::FieldAccessPredicate(..) => true, Expr::BinOp(BinaryOpKind::And, box lhs, box rhs, _) => {