Time reasoning

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

@@ -69,6 +69,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 |
@@ -310,6 +311,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"`
@@ -429,6 +431,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/bitvectors/mod.rs

@@ -68,6 +68,7 @@ pub fn replace_all_ints(program: &mut vir_poly::Program) {
                 }
             }
             vir_poly::Predicate::Bodyless(..) => {}
+            vir_poly::Predicate::ResourceAccess(_) => {}
         }
     }
     let types = [

prusti-common/src/vir/optimizations/folding/expressions.rs

@@ -417,6 +417,13 @@ impl ast::FallibleExprFolder for ExprOptimizer {
         Err(())
     }
 
+    fn fallible_fold_resource_access_predicate(
+        &mut self,
+        _resource_access_predicate: vir::polymorphic::ResourceAccessPredicate,
+    ) -> Result<vir::polymorphic::Expr, Self::Error> {
+        Err(())
+    }
+
     fn fallible_fold_field_access_predicate(
         &mut self,
         _field_access_predicate: ast::FieldAccessPredicate,

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

@@ -20,8 +20,9 @@ impl Simplifier for ast::Function {
     /// <https://github.com/viperproject/silicon/issues/387>
     fn simplify(mut self) -> Self {
         trace!("[enter] simplify = {}", self);
-        let new_body = self.body.map(|b| b.simplify());
-        self.body = new_body;
+        self.body = self.body.map(|b| b.simplify());
+        self.posts = self.posts.into_iter().map(|p| p.simplify()).collect();
+        self.pres = self.pres.into_iter().map(|p| p.simplify()).collect();
         trace!("[exit] simplify = {}", self);
         self
     }
@@ -30,8 +31,11 @@ impl Simplifier for ast::Function {
 impl Simplifier for ast::Expr {
     #[must_use]
     fn simplify(self) -> Self {
+        trace!("[enter] simplify = {:?}", self);
         let mut folder = ExprSimplifier {};
-        folder.fold(self)
+        let res = folder.fold(self);
+        trace!("[exit] simplify = {:?}", res);
+        res
     }
 }
 
@@ -46,134 +50,115 @@ impl ExprSimplifier {
                 argument:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
                 position: pos,
             }) => ast::Expr::Const(ast::ConstExpr {
                 value: ast::Const::Bool(!b),
                 position: pos,
-            }),
+            })
+            .set_default_pos(inner_pos),
             ast::Expr::UnaryOp(ast::UnaryOp {
                 op_kind: ast::UnaryOpKind::Not,
                 argument:
                     box ast::Expr::BinOp(ast::BinOp {
                         op_kind: ast::BinaryOpKind::EqCmp,
                         box left,
                         box right,
-                        ..
+                        position: inner_pos,
                     }),
                 position: pos,
-            }) => ast::Expr::BinOp(ast::BinOp {
+            }) if !matches!(left.get_type(), ast::Type::Float(_)) => ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::NeCmp,
                 left: box left,
                 right: box right,
                 position: pos,
-            }),
-            ast::Expr::BinOp(ast::BinOp {
-                op_kind: ast::BinaryOpKind::And,
-                left:
-                    box ast::Expr::Const(ast::ConstExpr {
-                        value: ast::Const::Bool(b1),
-                        ..
-                    }),
-                right:
-                    box ast::Expr::Const(ast::ConstExpr {
-                        value: ast::Const::Bool(b2),
-                        ..
-                    }),
-                position: pos,
-            }) => ast::Expr::Const(ast::ConstExpr {
-                value: ast::Const::Bool(b1 && b2),
-                position: pos,
-            }),
+            })
+            .set_default_pos(inner_pos),
             ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::And,
                 left:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
                 right: box conjunct,
-                ..
+                position: pos,
             })
             | ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::And,
                 left: box conjunct,
                 right:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
-                ..
-            }) => {
-                if b {
-                    conjunct
-                } else {
-                    false.into()
-                }
+                position: pos,
+            }) => if b {
+                conjunct
+            } else {
+                Into::<ast::Expr>::into(false).set_pos(inner_pos)
             }
+            .set_default_pos(pos),
             ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::Or,
                 left:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
                 right: box disjunct,
-                ..
+                position: pos,
             })
             | ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::Or,
                 left: box disjunct,
                 right:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
-                ..
-            }) => {
-                if b {
-                    true.into()
-                } else {
-                    disjunct
-                }
+                position: pos,
+            }) => if b {
+                Into::<ast::Expr>::into(true).set_pos(inner_pos)
+            } else {
+                disjunct
             }
+            .set_default_pos(pos),
             ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::Implies,
                 left: guard,
                 right:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
                 position: pos,
-            }) => {
-                if b {
-                    true.into()
-                } else {
-                    ast::Expr::UnaryOp(ast::UnaryOp {
-                        op_kind: ast::UnaryOpKind::Not,
-                        argument: guard,
-                        position: pos,
-                    })
-                }
+            }) => if b {
+                Into::<ast::Expr>::into(true).set_pos(pos)
+            } else {
+                ast::Expr::UnaryOp(ast::UnaryOp {
+                    op_kind: ast::UnaryOpKind::Not,
+                    argument: guard,
+                    position: pos,
+                })
             }
+            .set_default_pos(inner_pos),
             ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::Implies,
                 left:
                     box ast::Expr::Const(ast::ConstExpr {
                         value: ast::Const::Bool(b),
-                        ..
+                        position: inner_pos,
                     }),
                 right: box body,
-                ..
-            }) => {
-                if b {
-                    body
-                } else {
-                    true.into()
-                }
+                position: pos,
+            }) => if b {
+                body
+            } else {
+                Into::<ast::Expr>::into(true).set_pos(inner_pos)
             }
+            .set_default_pos(pos),
             ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::And,
                 left: box op1,

prusti-common/src/vir/optimizations/methods/mod.rs

@@ -13,14 +13,15 @@ mod purifier;
 mod quantifier_fixer;
 mod unfolding_fixer;
 mod var_remover;
+mod simplifier;
 
 use super::log_method;
 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,
-    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)]
@@ -57,6 +58,7 @@ pub fn optimize_method_encoding(
     };
     let cfg = apply!(fix_unfoldings, cfg);
     let cfg = apply!(fix_quantifiers, 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/purifier.rs

@@ -214,7 +214,9 @@ impl ast::StmtWalker for VarCollector {
         if is_purifiable_method(method_name) {
             self.is_pure_context = true;
         }
-        assert!(arguments.is_empty());
+        for arg in arguments {
+            self.walk_expr(arg);
+        }
         for target in targets {
             self.walk_local_var(target);
         }
@@ -464,8 +466,7 @@ impl ast::StmtFolder for VarPurifier {
             mut targets,
         }: ast::MethodCall,
     ) -> ast::Stmt {
-        assert!(targets.len() == 1);
-        if self.pure_vars.contains(&targets[0]) {
+        if targets.len() == 1 && self.pure_vars.contains(&targets[0]) {
             let target = &targets[0];
             let replacement = self
                 .replacements

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

@@ -0,0 +1,45 @@
+// © 2022, 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/.
+
+use log::debug;
+use std::mem;
+use vir::polymorphic::*;
+
+use crate::vir::optimizations::functions::Simplifier;
+
+/// 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_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 {
+        for stmt in &mut block.stmts {
+            mem::swap(&mut sentinel_stmt, stmt);
+            sentinel_stmt = sentinel_stmt.simplify();
+            mem::swap(&mut sentinel_stmt, stmt);
+        }
+    }
+    cfg
+}
+
+struct StmtSimplifier;
+
+impl Simplifier for Stmt {
+    fn simplify(self) -> Self {
+        let mut folder = StmtSimplifier;
+        folder.fold(self)
+    }
+}
+
+impl StmtFolder for StmtSimplifier {
+    fn fold_expr(&mut self, expr: Expr) -> Expr {
+        expr.simplify()
+    }
+}

prusti-common/src/vir/optimizations/mod.rs

@@ -122,6 +122,7 @@ pub fn optimize_program(p: Program, source_file_name: &str) -> Program {
         program.viper_predicates = predicates::delete_unused_predicates(
             &program.methods,
             &program.functions,
+            &program.builtin_methods,
             program.viper_predicates,
         );
     }