Credit Specification Parsing & Encoding

prusti-common/src/config.rs

@@ -95,6 +95,9 @@ lazy_static! {
         settings.set_default("intern_names", true).unwrap();
         settings.set_default("enable_purification_optimization", false).unwrap();
         settings.set_default("enable_manual_axiomatization", false).unwrap();
+        settings.set_default("verify_credit_conversions", false).unwrap();
+        settings.set_default("conditional_cost_inference", true).unwrap();
+        settings.set_default("verify_finite_credits", true).unwrap();
 
         settings.set_default("print_desugared_specs", false).unwrap();
         settings.set_default("print_typeckd_specs", false).unwrap();
@@ -463,3 +466,19 @@ pub fn full_compilation() -> bool {
 pub fn intern_names() -> bool {
     read_setting("intern_names")
 }
+
+/// Verify the conversions of credits by assignments inside Viper.
+pub fn verify_credit_conversions() -> bool {
+    read_setting("verify_credit_conversions")
+}
+
+/// Enable the verification of different asymptotic bounds depending on a condition.
+/// Otherwise, the code will be verified against the highest (combined) asymptotic bound.
+pub fn conditional_cost_inference() -> bool {
+    read_setting("conditional_cost_inference")
+}
+
+/// Verify that only a finite amount of credits is consumed.
+pub fn verify_finite_credits() -> bool {
+    read_setting("verify_finite_credits")
+}

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

@@ -4,48 +4,50 @@ use crate::vir::{self, cfg};
 
 /// Merge consequitive basic blocks that are joined by only one edge.
 pub fn clean_cfg(mut method: cfg::CfgMethod) -> cfg::CfgMethod {
-    let predecessors = method.predecessors();
-    let traversal_order = method.get_topological_sort();
-    assert_eq!(traversal_order[0].block_index, 0, "The start block should be first.");
-    let mut new_basic_blocks = Vec::new();
-    let mut basic_blocks: HashMap<_, _> = method.basic_blocks.into_iter().enumerate().collect();
-    let mut new_indices = HashMap::new();
+    if !method.basic_blocks.is_empty() {
+        let predecessors = method.predecessors();
+        let traversal_order = method.get_topological_sort();
+        assert_eq!(traversal_order[0].block_index, 0, "The start block should be first.");
+        let mut new_basic_blocks = Vec::new();
+        let mut basic_blocks: HashMap<_, _> = method.basic_blocks.into_iter().enumerate().collect();
+        let mut new_indices = HashMap::new();
 
-    for cfg::CfgBlockIndex{ block_index, .. } in traversal_order {
-        if let Some(mut basic_block) = basic_blocks.remove(&block_index) {
-            let new_index = new_basic_blocks.len();
-            assert!(new_indices.insert(block_index, new_index).is_none());
-            while let vir::cfg::Successor::Goto(target) = &basic_block.successor {
-                // If the current basic block has only one successor.
-                if predecessors[&target.block_index].len() == 1 {
-                    // If the successor block has only one predecessor.
+        for cfg::CfgBlockIndex { block_index, .. } in traversal_order {
+            if let Some(mut basic_block) = basic_blocks.remove(&block_index) {
+                let new_index = new_basic_blocks.len();
+                assert!(new_indices.insert(block_index, new_index).is_none());
+                while let vir::cfg::Successor::Goto(target) = &basic_block.successor {
+                    // If the current basic block has only one successor.
+                    if predecessors[&target.block_index].len() == 1 {
+                        // If the successor block has only one predecessor.
 
-                    assert!(new_indices.insert(target.block_index, new_index).is_none());
-                    let target_block = basic_blocks.remove(&target.block_index).unwrap();
+                        assert!(new_indices.insert(target.block_index, new_index).is_none());
+                        let target_block = basic_blocks.remove(&target.block_index).unwrap();
 
-                    basic_block.stmts.extend(target_block.stmts);
-                    basic_block.successor = target_block.successor;
-                } else {
-                    break;
+                        basic_block.stmts.extend(target_block.stmts);
+                        basic_block.successor = target_block.successor;
+                    } else {
+                        break;
+                    }
                 }
+                new_basic_blocks.push(basic_block);
             }
-            new_basic_blocks.push(basic_block);
         }
-    }
-    for basic_block in &mut new_basic_blocks {
-        match &mut basic_block.successor {
-            vir::cfg::Successor::Undefined | vir::cfg::Successor::Return => {},
-            vir::cfg::Successor::Goto(target) => {
-                target.block_index = new_indices[&target.index()];
-            }
-            vir::cfg::Successor::GotoSwitch(conditional_targets, default_target) => {
-                default_target.block_index = new_indices[&default_target.index()];
-                for (_, target) in conditional_targets {
+        for basic_block in &mut new_basic_blocks {
+            match &mut basic_block.successor {
+                vir::cfg::Successor::Undefined | vir::cfg::Successor::Return => {},
+                vir::cfg::Successor::Goto(target) => {
                     target.block_index = new_indices[&target.index()];
                 }
+                vir::cfg::Successor::GotoSwitch(conditional_targets, default_target) => {
+                    default_target.block_index = new_indices[&default_target.index()];
+                    for (_, target) in conditional_targets {
+                        target.block_index = new_indices[&target.index()];
+                    }
+                }
             }
         }
+        method.basic_blocks = new_basic_blocks;
     }
-    method.basic_blocks = new_basic_blocks;
     method
 }

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

@@ -66,6 +66,7 @@ pub fn purify_vars(mut method: cfg::CfgMethod) -> cfg::CfgMethod {
         }
     };
     method.local_vars = method.local_vars.into_iter().map(fix_var).collect();
+//    method.viper_formal_args = method.viper_formal_args.into_iter().map(fix_var).collect();     //TODO: ?
     method
 }
 
@@ -204,7 +205,10 @@ impl ast::StmtWalker for VarCollector {
         if is_purifiable_method(method_name) {
             self.is_pure_context = true;
         }
-        assert!(args.is_empty());
+        //assert!(args.is_empty());
+        for arg in args {
+            self.walk_expr(arg);     //TODO: ?
+        }
         for target in targets {
             self.walk_local_var(target);
         }
@@ -418,23 +422,25 @@ impl ast::StmtFolder for VarPurifier {
         args: Vec<ast::Expr>,
         mut targets: Vec<ast::LocalVar>,
     ) -> ast::Stmt {
-        assert!(targets.len() == 1);
-        if self.pure_vars.contains(&targets[0]) {
-            let target = &targets[0];
-            let replacement = self
-                .replacements
-                .get(target)
-                .expect(&format!("key: {}", target))
-                .clone();
-            name = match replacement.typ {
-                ast::Type::Int => "builtin$havoc_int",
-                ast::Type::Bool => "builtin$havoc_bool",
-                ast::Type::TypedRef(_) => "builtin$havoc_ref",
-                ast::Type::Domain(_)
-                | ast::Type::Snapshot(_)
-                | ast::Type::Seq(_) => unreachable!(),
-            }.to_string();
-            targets = vec![replacement];
+        assert!(targets.len() <= 1);
+        if targets.len() == 1 {
+            if self.pure_vars.contains(&targets[0]) {
+                let target = &targets[0];
+                let replacement = self
+                    .replacements
+                    .get(target)
+                    .expect(&format!("key: {}", target))
+                    .clone();
+                name = match replacement.typ {
+                    ast::Type::Int => "builtin$havoc_int",
+                    ast::Type::Bool => "builtin$havoc_bool",
+                    ast::Type::TypedRef(_) => "builtin$havoc_ref",
+                    ast::Type::Domain(_)
+                    | ast::Type::Snapshot(_)
+                    | ast::Type::Seq(_) => unreachable!(),
+                }.to_string();
+                targets = vec![replacement];
+            }
         }
         ast::Stmt::MethodCall(
             name,

prusti-common/src/vir/optimizations/predicates/delete_unused_predicates.rs

@@ -67,6 +67,17 @@ fn get_used_predicates_in_predicate_map(
                 map.insert(p.name.clone(), res);
             }
             Predicate::Bodyless(_, _) => { /* ignore */ }
+            Predicate::CreditUnit(CreditUnitPredicate {
+                name,
+                body: Some(e),
+                ..
+            }) => {
+                ExprWalker::walk(&mut collector, e);
+                let mut res = BTreeSet::new();
+                std::mem::swap(&mut res, &mut collector.used_predicates);
+                map.insert(name.clone(), res);
+            }
+            Predicate::CreditUnit(CreditUnitPredicate { body: None, .. }) => { /* ignore */ }
         }
     }
     return map;
@@ -169,6 +180,13 @@ impl UsedPredicateCollector {
 }
 
 impl ExprWalker for UsedPredicateCollector {
+    fn walk_predicate_instance(&mut self, name: &str, args: &Vec<Expr>, _pos: &Position) {
+        self.used_predicates.insert(name.to_string());
+        for arg in args {
+            ExprWalker::walk(self, arg)
+        }
+    }
+
     fn walk_predicate_access_predicate(
         &mut self,
         name: &str,
@@ -180,6 +198,19 @@ impl ExprWalker for UsedPredicateCollector {
         ExprWalker::walk(self, arg);
     }
 
+    fn walk_credit_access_predicate(
+        &mut self,
+        name: &str,
+        args: &Vec<Expr>,
+        _frac_perm_amount: &FracPermAmount,
+        _pos: &Position
+    ) {
+        self.used_predicates.insert(name.to_string());
+        for arg in args {
+            ExprWalker::walk(self, arg);
+        }
+    }
+
     fn walk_unfolding(
         &mut self,
         name: &str,

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

@@ -71,7 +71,7 @@ fn purify_method(method: &mut CfgMethod, predicates: &[Predicate]) {
     }
 }
 
-/// This is a ExprWalkerand StmtWalker used to collect information about which
+/// This is a ExprWalker and StmtWalker used to collect information about which
 /// local variables can be purified.
 ///
 /// The current implementation is only for ints/bools. So to check if a