Pull request reviews

docs/dev-guide/src/config/flags.md

@@ -70,6 +70,7 @@
 | [`SMT_SOLVER_WRAPPER_PATH`](#smt_solver_wrapper_path) | `Option<String>` | `None` | A |
 | [`SMT_UNIQUE_TRIGGERS_BOUND`](#smt_unique_triggers_bound) | `Option<u64>` | `None` | A |
 | [`SMT_UNIQUE_TRIGGERS_BOUND_TOTAL`](#smt_unique_triggers_bound_total) | `Option<u64>` | `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

prusti-common/src/vir/optimizations/functions/simplifier.rs

@@ -99,8 +99,7 @@ impl ExprSimplifier {
             } else {
                 Into::<ast::Expr>::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::<ast::Expr>::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,

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);

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 {

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<Predicate>,
 ) -> Vec<Predicate> {
-    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);

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),
                 )

prusti-tests/tests/verify/fail/time-resources/array_cmp.rs

@@ -8,6 +8,8 @@ use prusti_contracts::*;
 fn opt_array_cmp<T: Eq>(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<T: Eq>(a: &[T], b: &[T]) -> bool { //~ ERROR Not enough time re
 }
 
 #[requires(time_credits(1))]
-fn main() {}
+fn main() {}

prusti-tests/tests/verify/fail/time-resources/loop.rs

@@ -2,22 +2,33 @@
 
 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 {
     let mut i = 1; // To be correct it should be n
     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;
     }

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;
-  }
-}
+fn main() {//~ ERROR Not enough time credits.
+    let mut i = 0;
+    let mut _n = 0;
+    i += 42;
+}

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;
         }

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<T: Eq>(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<T: Eq>(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() {}
+fn main() {}

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;
     }

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;
     }

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;
     }